----------------------------------------------------------------------
-- |
-- Module      : PGFtoProlog
-- Maintainer  : Peter Ljunglöf
--
-- exports a GF grammar into a Prolog module
-----------------------------------------------------------------------------

module GF.Compile.PGFtoProlog (grammar2prolog) where

import PGF(mkCId,wildCId,showCId)
import PGF.Internal
--import PGF.Macros

import GF.Data.Operations

import qualified Data.Array.IArray as Array
import qualified Data.Set as Set
import qualified Data.Map as Map
import qualified Data.IntMap as IntMap
import Data.Char (isAlphaNum, isAscii, isAsciiLower, isAsciiUpper, ord)
import Data.List (isPrefixOf, mapAccumL)

grammar2prolog :: PGF -> String
grammar2prolog :: PGF -> String
grammar2prolog PGF
pgf
    = (String
"%% This file was automatically generated by GF" String -> String -> String
+++++
       String
":- style_check(-singleton)." String -> String -> String
+++++
       CId -> String -> Int -> String -> [[String]] -> String
plFacts CId
wildCId String
"abstract" Int
1 String
"(?AbstractName)"
                   [[CId -> String
forall a. PLPrint a => a -> String
plp CId
name]] String -> String -> String
++++
       CId -> String -> Int -> String -> [[String]] -> String
plFacts CId
wildCId String
"concrete" Int
2 String
"(?AbstractName, ?ConcreteName)" 
                   [[CId -> String
forall a. PLPrint a => a -> String
plp CId
name, CId -> String
forall a. PLPrint a => a -> String
plp CId
cncname] | 
                    CId
cncname <- Map CId Concr -> [CId]
forall k a. Map k a -> [k]
Map.keys (PGF -> Map CId Concr
concretes PGF
pgf)] String -> String -> String
++++
       CId -> String -> Int -> String -> [[String]] -> String
plFacts CId
wildCId String
"flag" Int
2 String
"(?Flag, ?Value): global flags" 
                   [[CId -> String
forall a. PLPrint a => a -> String
plp CId
f, Literal -> String
forall a. PLPrint a => a -> String
plp Literal
v] | 
                    (CId
f, Literal
v) <- Map CId Literal -> [(CId, Literal)]
forall k a. Map k a -> [(k, a)]
Map.assocs (PGF -> Map CId Literal
gflags PGF
pgf)] String -> String -> String
++++
       CId -> Abstr -> String
plAbstract CId
name (PGF -> Abstr
abstract PGF
pgf) String -> String -> String
++++
       [String] -> String
unlines (((CId, Concr) -> String) -> [(CId, Concr)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (CId, Concr) -> String
plConcrete (Map CId Concr -> [(CId, Concr)]
forall k a. Map k a -> [(k, a)]
Map.assocs (PGF -> Map CId Concr
concretes PGF
pgf)))
      )
    where name :: CId
name = PGF -> CId
absname PGF
pgf

----------------------------------------------------------------------
-- abstract syntax

plAbstract :: CId -> Abstr -> String
plAbstract :: CId -> Abstr -> String
plAbstract CId
name Abstr
abs 
    = (String -> String
plHeader String
"Abstract syntax" String -> String -> String
++++
       CId -> String -> Int -> String -> [[String]] -> String
plFacts CId
name String
"flag" Int
2 String
"(?Flag, ?Value): flags for abstract syntax"
                   [[CId -> String
forall a. PLPrint a => a -> String
plp CId
f, Literal -> String
forall a. PLPrint a => a -> String
plp Literal
v] | 
                    (CId
f, Literal
v) <- Map CId Literal -> [(CId, Literal)]
forall k a. Map k a -> [(k, a)]
Map.assocs (Abstr -> Map CId Literal
aflags Abstr
abs)] String -> String -> String
++++
       CId -> String -> Int -> String -> [[String]] -> String
plFacts CId
name String
"cat" Int
2 String
"(?Type, ?[X:Type,...])"
                   [[CId -> [Expr] -> String
forall a a. (PLPrint a, PLPrint a) => a -> [a] -> String
plType CId
cat [Expr]
args, [(BindType, CId, Type)] -> String
forall a a a. (PLPrint a, PLPrint a) => [(a, a, a)] -> String
plHypos [(BindType, CId, Type)]
hypos'] |
                    (CId
cat, ([(BindType, CId, Type)]
hypos,[(Double, CId)]
_,Double
_)) <- Map CId ([(BindType, CId, Type)], [(Double, CId)], Double)
-> [(CId, ([(BindType, CId, Type)], [(Double, CId)], Double))]
forall k a. Map k a -> [(k, a)]
Map.assocs (Abstr -> Map CId ([(BindType, CId, Type)], [(Double, CId)], Double)
cats Abstr
abs),
                    let ((Int
_, [(CId, CId)]
subst), [(BindType, CId, Type)]
hypos') = ((Int, [(CId, CId)])
 -> (BindType, CId, Type)
 -> ((Int, [(CId, CId)]), (BindType, CId, Type)))
-> (Int, [(CId, CId)])
-> [(BindType, CId, Type)]
-> ((Int, [(CId, CId)]), [(BindType, CId, Type)])
forall (t :: * -> *) a b c.
Traversable t =>
(a -> b -> (a, c)) -> a -> t b -> (a, t c)
mapAccumL (Int, [(CId, CId)])
-> (BindType, CId, Type)
-> ((Int, [(CId, CId)]), (BindType, CId, Type))
forall c a.
AlphaConvert c =>
(Int, [(CId, CId)])
-> (a, CId, c) -> ((Int, [(CId, CId)]), (a, CId, c))
alphaConvertHypo (Int, [(CId, CId)])
emptyEnv [(BindType, CId, Type)]
hypos,
                        let args :: [Expr]
args = [Expr] -> [Expr]
forall a. [a] -> [a]
reverse [CId -> Expr
EFun CId
x | (CId
_,CId
x) <- [(CId, CId)]
subst]] String -> String -> String
++++
       CId -> String -> Int -> String -> [[String]] -> String
plFacts CId
name String
"fun" Int
3 String
"(?Fun, ?Type, ?[X:Type,...])"
                   [[CId -> String
forall a. PLPrint a => a -> String
plp CId
fun, CId -> [Expr] -> String
forall a a. (PLPrint a, PLPrint a) => a -> [a] -> String
plType CId
cat [Expr]
args, [(BindType, CId, Type)] -> String
forall a a a. (PLPrint a, PLPrint a) => [(a, a, a)] -> String
plHypos [(BindType, CId, Type)]
hypos] |
                    (CId
fun, (Type
typ, Int
_, Maybe ([Equation], [[Instr]])
_, Double
_)) <- Map CId (Type, Int, Maybe ([Equation], [[Instr]]), Double)
-> [(CId, (Type, Int, Maybe ([Equation], [[Instr]]), Double))]
forall k a. Map k a -> [(k, a)]
Map.assocs (Abstr -> Map CId (Type, Int, Maybe ([Equation], [[Instr]]), Double)
funs Abstr
abs),
                    let ((Int, [(CId, CId)])
_, DTyp [(BindType, CId, Type)]
hypos CId
cat [Expr]
args) = (Int, [(CId, CId)]) -> Type -> ((Int, [(CId, CId)]), Type)
forall a.
AlphaConvert a =>
(Int, [(CId, CId)]) -> a -> ((Int, [(CId, CId)]), a)
alphaConvert (Int, [(CId, CId)])
emptyEnv Type
typ] String -> String -> String
++++
       CId -> String -> Int -> String -> [[String]] -> String
plFacts CId
name String
"def" Int
2 String
"(?Fun, ?Expr)" 
                   [[CId -> String
forall a. PLPrint a => a -> String
plp CId
fun, [Equation] -> String
forall a. PLPrint a => a -> String
plp [Equation]
expr] |
                    (CId
fun, (Type
_, Int
_, Just ([Equation]
eqs,[[Instr]]
_), Double
_)) <- Map CId (Type, Int, Maybe ([Equation], [[Instr]]), Double)
-> [(CId, (Type, Int, Maybe ([Equation], [[Instr]]), Double))]
forall k a. Map k a -> [(k, a)]
Map.assocs (Abstr -> Map CId (Type, Int, Maybe ([Equation], [[Instr]]), Double)
funs Abstr
abs),
                    let ((Int, [(CId, CId)])
_, [Equation]
expr) = (Int, [(CId, CId)])
-> [Equation] -> ((Int, [(CId, CId)]), [Equation])
forall a.
AlphaConvert a =>
(Int, [(CId, CId)]) -> a -> ((Int, [(CId, CId)]), a)
alphaConvert (Int, [(CId, CId)])
emptyEnv [Equation]
eqs]
      )
    where plType :: a -> [a] -> String
plType a
cat [a]
args = String -> [String] -> String
plTerm (a -> String
forall a. PLPrint a => a -> String
plp a
cat) ((a -> String) -> [a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map a -> String
forall a. PLPrint a => a -> String
plp [a]
args)
          plHypos :: [(a, a, a)] -> String
plHypos [(a, a, a)]
hypos = [String] -> String
plList [String -> String -> String -> String
plOper String
":" (a -> String
forall a. PLPrint a => a -> String
plp a
x) (a -> String
forall a. PLPrint a => a -> String
plp a
ty) | (a
_, a
x, a
ty) <- [(a, a, a)]
hypos]

----------------------------------------------------------------------
-- concrete syntax

plConcrete :: (CId, Concr) -> String
plConcrete :: (CId, Concr) -> String
plConcrete (CId
name, Concr
cnc) 
    = (String -> String
plHeader (String
"Concrete syntax: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CId -> String
forall a. PLPrint a => a -> String
plp CId
name) String -> String -> String
++++
       CId -> String -> Int -> String -> [[String]] -> String
plFacts CId
name String
"flag" Int
2 String
"(?Flag, ?Value): flags for concrete syntax"
                   [[CId -> String
forall a. PLPrint a => a -> String
plp CId
f, Literal -> String
forall a. PLPrint a => a -> String
plp Literal
v] | 
                    (CId
f, Literal
v) <- Map CId Literal -> [(CId, Literal)]
forall k a. Map k a -> [(k, a)]
Map.assocs (Concr -> Map CId Literal
cflags Concr
cnc)] String -> String -> String
++++
       CId -> String -> Int -> String -> [[String]] -> String
plFacts CId
name String
"printname" Int
2 String
"(?AbsFun/AbsCat, ?Atom)"
                   [[CId -> String
forall a. PLPrint a => a -> String
plp CId
f, String -> String
forall a. PLPrint a => a -> String
plp String
n] | 
                    (CId
f, String
n) <- Map CId String -> [(CId, String)]
forall k a. Map k a -> [(k, a)]
Map.assocs (Concr -> Map CId String
printnames Concr
cnc)] String -> String -> String
++++
       CId -> String -> Int -> String -> [[String]] -> String
plFacts CId
name String
"lindef" Int
2 String
"(?CncCat, ?CncFun)"
                   [[Int -> String
plCat Int
cat, Int -> String
plFun Int
fun] | 
                    (Int
cat, [Int]
funs) <- IntMap [Int] -> [(Int, [Int])]
forall a. IntMap a -> [(Int, a)]
IntMap.assocs (Concr -> IntMap [Int]
lindefs Concr
cnc),
                    Int
fun <- [Int]
funs] String -> String -> String
++++
       CId -> String -> Int -> String -> [[String]] -> String
plFacts CId
name String
"prod" Int
3 String
"(?CncCat, ?CncFun, ?[CncCat])"
                   [[Int -> String
plCat Int
cat, String
fun, String -> [String] -> String
plTerm String
"c" ((Int -> String) -> [Int] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Int -> String
plCat [Int]
args)] |
                    (Int
cat, Set Production
set) <- IntMap (Set Production) -> [(Int, Set Production)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList (Concr -> IntMap (Set Production)
productions Concr
cnc),
                    (String
fun, [Int]
args) <- (Production -> (String, [Int]))
-> [Production] -> [(String, [Int])]
forall a b. (a -> b) -> [a] -> [b]
map Production -> (String, [Int])
plProduction (Set Production -> [Production]
forall a. Set a -> [a]
Set.toList Set Production
set)] String -> String -> String
++++
       CId -> String -> Int -> String -> [[String]] -> String
plFacts CId
name String
"cncfun" Int
3 String
"(?CncFun, ?[Seq,...], ?AbsFun)"
                   [[Int -> String
plFun Int
fun, String -> [String] -> String
plTerm String
"s" ((Int -> String) -> [Int] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Int -> String
plSeq (UArray Int Int -> [Int]
forall (a :: * -> * -> *) e i. (IArray a e, Ix i) => a i e -> [e]
Array.elems UArray Int Int
lins)), CId -> String
forall a. PLPrint a => a -> String
plp CId
absfun] |
                    (Int
fun, CncFun CId
absfun UArray Int Int
lins) <- Array Int CncFun -> [(Int, CncFun)]
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> [(i, e)]
Array.assocs (Concr -> Array Int CncFun
cncfuns Concr
cnc)] String -> String -> String
++++
       CId -> String -> Int -> String -> [[String]] -> String
plFacts CId
name String
"seq" Int
2 String
"(?Seq, ?[Term])"
                   [[Int -> String
plSeq Int
seq, [Symbol] -> String
forall a. PLPrint a => a -> String
plp (Array Int Symbol -> [Symbol]
forall (a :: * -> * -> *) e i. (IArray a e, Ix i) => a i e -> [e]
Array.elems Array Int Symbol
symbols)] |
                    (Int
seq, Array Int Symbol
symbols) <- Array Int (Array Int Symbol) -> [(Int, Array Int Symbol)]
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> [(i, e)]
Array.assocs (Concr -> Array Int (Array Int Symbol)
sequences Concr
cnc)] String -> String -> String
++++
       CId -> String -> Int -> String -> [[String]] -> String
plFacts CId
name String
"cnccat" Int
2 String
"(?AbsCat, ?[CnCCat])" 
                   [[CId -> String
forall a. PLPrint a => a -> String
plp CId
cat, [String] -> String
plList ((Int -> String) -> [Int] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Int -> String
plCat [Int
start..Int
end])] |
                    (CId
cat, CncCat Int
start Int
end Array Int String
_) <- Map CId CncCat -> [(CId, CncCat)]
forall k a. Map k a -> [(k, a)]
Map.assocs (Concr -> Map CId CncCat
cnccats Concr
cnc)]
      )
    where plProduction :: Production -> (String, [Int])
plProduction (PCoerce Int
arg)       = (String
"-", [Int
arg])
          plProduction (PApply Int
funid [PArg]
args) = (Int -> String
plFun Int
funid, [Int
fid | PArg [(Int, Int)]
hypos Int
fid <- [PArg]
args])

----------------------------------------------------------------------
-- prolog-printing pgf datatypes

instance PLPrint Type where
    plp :: Type -> String
plp (DTyp [(BindType, CId, Type)]
hypos CId
cat [Expr]
args) 
        | [(BindType, CId, Type)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(BindType, CId, Type)]
hypos = String
result
        | Bool
otherwise  = String -> String -> String -> String
plOper String
" -> " String
plHypos String
result
        where result :: String
result = String -> [String] -> String
plTerm (CId -> String
forall a. PLPrint a => a -> String
plp CId
cat) ((Expr -> String) -> [Expr] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> String
forall a. PLPrint a => a -> String
plp [Expr]
args)
              plHypos :: String
plHypos = [String] -> String
plList [String -> String -> String -> String
plOper String
":" (CId -> String
forall a. PLPrint a => a -> String
plp CId
x) (Type -> String
forall a. PLPrint a => a -> String
plp Type
ty) | (BindType
_,CId
x,Type
ty) <- [(BindType, CId, Type)]
hypos]

instance PLPrint Expr where
    plp :: Expr -> String
plp (EFun CId
x)    = CId -> String
forall a. PLPrint a => a -> String
plp CId
x
    plp (EAbs BindType
_ CId
x Expr
e)= String -> String -> String -> String
plOper String
"^" (CId -> String
forall a. PLPrint a => a -> String
plp CId
x) (Expr -> String
forall a. PLPrint a => a -> String
plp Expr
e)
    plp (EApp Expr
e Expr
e') = String -> String -> String -> String
plOper String
" * " (Expr -> String
forall a. PLPrint a => a -> String
plp Expr
e) (Expr -> String
forall a. PLPrint a => a -> String
plp Expr
e')
    plp (ELit Literal
lit)  = Literal -> String
forall a. PLPrint a => a -> String
plp Literal
lit
    plp (EMeta Int
n)   = String
"Meta_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n

instance PLPrint Patt where
    plp :: Patt -> String
plp (PVar CId
x)    = CId -> String
forall a. PLPrint a => a -> String
plp CId
x
    plp (PApp CId
f [Patt]
ps) = String -> String -> String -> String
plOper String
" * " (CId -> String
forall a. PLPrint a => a -> String
plp CId
f) ([Patt] -> String
forall a. PLPrint a => a -> String
plp [Patt]
ps)
    plp (PLit Literal
lit)  = Literal -> String
forall a. PLPrint a => a -> String
plp Literal
lit

instance PLPrint Equation where
    plp :: Equation -> String
plp (Equ [Patt]
patterns Expr
result) = String -> String -> String -> String
plOper String
":" ([Patt] -> String
forall a. PLPrint a => a -> String
plp [Patt]
patterns) (Expr -> String
forall a. PLPrint a => a -> String
plp Expr
result)

instance PLPrint CId where
    plp :: CId -> String
plp CId
cid | String -> Bool
isLogicalVariable String
str Bool -> Bool -> Bool
|| CId
cid CId -> CId -> Bool
forall a. Eq a => a -> a -> Bool
== CId
wildCId = String -> String
plVar String
str
            | Bool
otherwise = String -> String
plAtom String
str
        where str :: String
str = CId -> String
showCId CId
cid

instance PLPrint Literal where
    plp :: Literal -> String
plp (LStr String
s) = String -> String
forall a. PLPrint a => a -> String
plp String
s
    plp (LInt Int
n) = String -> String
forall a. PLPrint a => a -> String
plp (Int -> String
forall a. Show a => a -> String
show Int
n)
    plp (LFlt Double
f) = String -> String
forall a. PLPrint a => a -> String
plp (Double -> String
forall a. Show a => a -> String
show Double
f)

instance PLPrint Symbol where
    plp :: Symbol -> String
plp (SymCat Int
n Int
l)    = String -> String -> String -> String
plOper String
":" (Int -> String
forall a. Show a => a -> String
show Int
n) (Int -> String
forall a. Show a => a -> String
show Int
l)
    plp (SymLit Int
n Int
l)    = String -> [String] -> String
plTerm String
"lit" [Int -> String
forall a. Show a => a -> String
show Int
n, Int -> String
forall a. Show a => a -> String
show Int
l]
    plp (SymVar Int
n Int
l)    = String -> [String] -> String
plTerm String
"var" [Int -> String
forall a. Show a => a -> String
show Int
n, Int -> String
forall a. Show a => a -> String
show Int
l]
    plp (SymKS String
t)       = String -> String
plAtom String
t
    plp (SymKP [Symbol]
ts [([Symbol], [String])]
alts) = String -> [String] -> String
plTerm String
"pre" [[String] -> String
plList ((Symbol -> String) -> [Symbol] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Symbol -> String
forall a. PLPrint a => a -> String
plp [Symbol]
ts), [String] -> String
plList ((([Symbol], [String]) -> String)
-> [([Symbol], [String])] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ([Symbol], [String]) -> String
forall a. PLPrint a => ([a], [String]) -> String
plAlt [([Symbol], [String])]
alts)]
        where plAlt :: ([a], [String]) -> String
plAlt ([a]
ps,[String]
ts) = String -> String -> String -> String
plOper String
"/" ([String] -> String
plList ((a -> String) -> [a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map a -> String
forall a. PLPrint a => a -> String
plp [a]
ps)) ([String] -> String
plList ((String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map String -> String
plAtom [String]
ts))

class PLPrint a where
    plp :: a -> String
    plps :: [a] -> String
    plps = [String] -> String
plList ([String] -> String) -> ([a] -> [String]) -> [a] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> String) -> [a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map a -> String
forall a. PLPrint a => a -> String
plp

instance PLPrint Char where
    plp :: Char -> String
plp  Char
c = String -> String
plAtom [Char
c]
    plps :: String -> String
plps String
s = String -> String
plAtom String
s

instance PLPrint a => PLPrint [a] where
    plp :: [a] -> String
plp = [a] -> String
forall a. PLPrint a => [a] -> String
plps

----------------------------------------------------------------------
-- other prolog-printing functions

plCat :: Int -> String
plCat :: Int -> String
plCat Int
n = String -> String
plAtom (Char
'c' Char -> String -> String
forall a. a -> [a] -> [a]
: Int -> String
forall a. Show a => a -> String
show Int
n)

plFun :: Int -> String
plFun :: Int -> String
plFun Int
n = String -> String
plAtom (Char
'f' Char -> String -> String
forall a. a -> [a] -> [a]
: Int -> String
forall a. Show a => a -> String
show Int
n)

plSeq :: Int -> String
plSeq :: Int -> String
plSeq Int
n = String -> String
plAtom (Char
's' Char -> String -> String
forall a. a -> [a] -> [a]
: Int -> String
forall a. Show a => a -> String
show Int
n)

plHeader :: String -> String
plHeader :: String -> String
plHeader String
hdr = String
"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n%% " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
hdr String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n"

plFacts :: CId -> String -> Int -> String -> [[String]] -> String
plFacts :: CId -> String -> Int -> String -> [[String]] -> String
plFacts CId
mod String
pred Int
arity String
comment [[String]]
facts = String
"%% " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
pred String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
comment String -> String -> String
++++ String
clauses
    where clauses :: String
clauses = (if [[String]]
facts [[String]] -> [[String]] -> Bool
forall a. Eq a => a -> a -> Bool
== [] then String
":- dynamic " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
pred String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"/" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
arity String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".\n"
                     else [String] -> String
unlines [String
mod' String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
plTerm String
pred [String]
args String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"." | [String]
args <- [[String]]
facts])
          mod' :: String
mod' = if CId
mod CId -> CId -> Bool
forall a. Eq a => a -> a -> Bool
== CId
wildCId then String
"" else CId -> String
forall a. PLPrint a => a -> String
plp CId
mod String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": "

plTerm :: String -> [String] -> String
plTerm :: String -> [String] -> String
plTerm String
fun [String]
args = String -> String
plAtom String
fun String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
prParenth (String -> [String] -> String
prTList String
", " [String]
args)

plList :: [String] -> String
plList :: [String] -> String
plList [String]
xs = String -> String
prBracket (String -> [String] -> String
prTList String
"," [String]
xs)

plOper :: String -> String -> String -> String
plOper :: String -> String -> String -> String
plOper String
op String
a String
b = String -> String
prParenth (String
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
op String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
b)

plVar :: String -> String
plVar :: String -> String
plVar = String -> String
varPrefix  (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> String) -> String -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Char -> String
changeNonAlphaNum 
    where varPrefix :: String -> String
varPrefix var :: String
var@(Char
c:String
_) | Char -> Bool
isAsciiUpper Char
c Bool -> Bool -> Bool
|| Char
cChar -> Char -> Bool
forall a. Eq a => a -> a -> Bool
==Char
'_' = String
var
                              | Bool
otherwise = String
"_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
var
          changeNonAlphaNum :: Char -> String
changeNonAlphaNum Char
c | Char -> Bool
isAlphaNumUnderscore Char
c = [Char
c]
                              | Bool
otherwise = String
"_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Char -> Int
ord Char
c) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_"

plAtom :: String -> String
plAtom :: String -> String
plAtom String
"" = String
"''"
plAtom atom :: String
atom@(Char
c:String
cs) | Char -> Bool
isAsciiLower Char
c Bool -> Bool -> Bool
&& (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isAlphaNumUnderscore String
cs 
                     Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'\'' Bool -> Bool -> Bool
&& String
cs String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= String
"" Bool -> Bool -> Bool
&& String -> Char
forall a. [a] -> a
last String
cs Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'\''   = String
atom
                   | Bool
otherwise = String
"'" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
changeQuote String
atom String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'"
    where changeQuote :: String -> String
changeQuote (Char
'\'':String
cs) = Char
'\\' Char -> String -> String
forall a. a -> [a] -> [a]
: Char
'\'' Char -> String -> String
forall a. a -> [a] -> [a]
: String -> String
changeQuote String
cs
          changeQuote (Char
'\\':String
cs) = Char
'\\' Char -> String -> String
forall a. a -> [a] -> [a]
: Char
'\\' Char -> String -> String
forall a. a -> [a] -> [a]
: String -> String
changeQuote String
cs
          changeQuote (Char
c:String
cs) = Char
c Char -> String -> String
forall a. a -> [a] -> [a]
: String -> String
changeQuote String
cs
          changeQuote String
"" = String
""

isAlphaNumUnderscore :: Char -> Bool
isAlphaNumUnderscore :: Char -> Bool
isAlphaNumUnderscore Char
c = (Char -> Bool
isAscii Char
c Bool -> Bool -> Bool
&& Char -> Bool
isAlphaNum Char
c) Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'_'

----------------------------------------------------------------------
-- prolog variables 

createLogicalVariable :: Int -> CId
createLogicalVariable :: Int -> CId
createLogicalVariable Int
n = String -> CId
mkCId (String
logicalVariablePrefix String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n)

isLogicalVariable :: String -> Bool
isLogicalVariable :: String -> Bool
isLogicalVariable = String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf String
logicalVariablePrefix 

logicalVariablePrefix :: String 
logicalVariablePrefix :: String
logicalVariablePrefix = String
"X"

----------------------------------------------------------------------
-- alpha convert variables to (unique) logical variables
-- * this is needed if we want to translate variables to Prolog variables
-- * used for abstract syntax, not concrete
-- * not (yet?) used for variables bound in pattern equations

type ConvertEnv = (Int, [(CId,CId)])

emptyEnv :: ConvertEnv
emptyEnv :: (Int, [(CId, CId)])
emptyEnv = (Int
0, [])

class AlphaConvert a where
    alphaConvert :: ConvertEnv -> a -> (ConvertEnv, a)

instance AlphaConvert a => AlphaConvert [a] where
    alphaConvert :: (Int, [(CId, CId)]) -> [a] -> ((Int, [(CId, CId)]), [a])
alphaConvert (Int, [(CId, CId)])
env [] = ((Int, [(CId, CId)])
env, [])
    alphaConvert (Int, [(CId, CId)])
env (a
a:[a]
as) = ((Int, [(CId, CId)])
env'', a
a'a -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
as')
        where ((Int, [(CId, CId)])
env',  a
a')  = (Int, [(CId, CId)]) -> a -> ((Int, [(CId, CId)]), a)
forall a.
AlphaConvert a =>
(Int, [(CId, CId)]) -> a -> ((Int, [(CId, CId)]), a)
alphaConvert (Int, [(CId, CId)])
env  a
a
              ((Int, [(CId, CId)])
env'', [a]
as') = (Int, [(CId, CId)]) -> [a] -> ((Int, [(CId, CId)]), [a])
forall a.
AlphaConvert a =>
(Int, [(CId, CId)]) -> a -> ((Int, [(CId, CId)]), a)
alphaConvert (Int, [(CId, CId)])
env' [a]
as

instance AlphaConvert Type where
    alphaConvert :: (Int, [(CId, CId)]) -> Type -> ((Int, [(CId, CId)]), Type)
alphaConvert env :: (Int, [(CId, CId)])
env@(Int
_,[(CId, CId)]
subst) (DTyp [(BindType, CId, Type)]
hypos CId
cat [Expr]
args) 
        = ((Int
ctr,[(CId, CId)]
subst), [(BindType, CId, Type)] -> CId -> [Expr] -> Type
DTyp [(BindType, CId, Type)]
hypos' CId
cat [Expr]
args')
        where ((Int, [(CId, CId)])
env',   [(BindType, CId, Type)]
hypos') = ((Int, [(CId, CId)])
 -> (BindType, CId, Type)
 -> ((Int, [(CId, CId)]), (BindType, CId, Type)))
-> (Int, [(CId, CId)])
-> [(BindType, CId, Type)]
-> ((Int, [(CId, CId)]), [(BindType, CId, Type)])
forall (t :: * -> *) a b c.
Traversable t =>
(a -> b -> (a, c)) -> a -> t b -> (a, t c)
mapAccumL (Int, [(CId, CId)])
-> (BindType, CId, Type)
-> ((Int, [(CId, CId)]), (BindType, CId, Type))
forall c a.
AlphaConvert c =>
(Int, [(CId, CId)])
-> (a, CId, c) -> ((Int, [(CId, CId)]), (a, CId, c))
alphaConvertHypo (Int, [(CId, CId)])
env [(BindType, CId, Type)]
hypos
              ((Int
ctr,[(CId, CId)]
_), [Expr]
args') = (Int, [(CId, CId)]) -> [Expr] -> ((Int, [(CId, CId)]), [Expr])
forall a.
AlphaConvert a =>
(Int, [(CId, CId)]) -> a -> ((Int, [(CId, CId)]), a)
alphaConvert (Int, [(CId, CId)])
env' [Expr]
args

alphaConvertHypo :: (Int, [(CId, CId)])
-> (a, CId, c) -> ((Int, [(CId, CId)]), (a, CId, c))
alphaConvertHypo (Int, [(CId, CId)])
env (a
b,CId
x,c
typ) = ((Int
ctrInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1,(CId
x,CId
x')(CId, CId) -> [(CId, CId)] -> [(CId, CId)]
forall a. a -> [a] -> [a]
:[(CId, CId)]
subst), (a
b,CId
x',c
typ'))
    where ((Int
ctr,[(CId, CId)]
subst), c
typ') = (Int, [(CId, CId)]) -> c -> ((Int, [(CId, CId)]), c)
forall a.
AlphaConvert a =>
(Int, [(CId, CId)]) -> a -> ((Int, [(CId, CId)]), a)
alphaConvert (Int, [(CId, CId)])
env c
typ
          x' :: CId
x' = Int -> CId
createLogicalVariable Int
ctr

instance AlphaConvert Expr where
    alphaConvert :: (Int, [(CId, CId)]) -> Expr -> ((Int, [(CId, CId)]), Expr)
alphaConvert (Int
ctr,[(CId, CId)]
subst) (EAbs BindType
b CId
x Expr
e) = ((Int
ctr',[(CId, CId)]
subst), BindType -> CId -> Expr -> Expr
EAbs BindType
b CId
x' Expr
e')
        where ((Int
ctr',[(CId, CId)]
_), Expr
e') = (Int, [(CId, CId)]) -> Expr -> ((Int, [(CId, CId)]), Expr)
forall a.
AlphaConvert a =>
(Int, [(CId, CId)]) -> a -> ((Int, [(CId, CId)]), a)
alphaConvert (Int
ctrInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1,(CId
x,CId
x')(CId, CId) -> [(CId, CId)] -> [(CId, CId)]
forall a. a -> [a] -> [a]
:[(CId, CId)]
subst) Expr
e
              x' :: CId
x' = Int -> CId
createLogicalVariable Int
ctr
    alphaConvert (Int, [(CId, CId)])
env (EApp Expr
e1 Expr
e2) = ((Int, [(CId, CId)])
env'', Expr -> Expr -> Expr
EApp Expr
e1' Expr
e2')
        where ((Int, [(CId, CId)])
env',  Expr
e1') = (Int, [(CId, CId)]) -> Expr -> ((Int, [(CId, CId)]), Expr)
forall a.
AlphaConvert a =>
(Int, [(CId, CId)]) -> a -> ((Int, [(CId, CId)]), a)
alphaConvert (Int, [(CId, CId)])
env  Expr
e1
              ((Int, [(CId, CId)])
env'', Expr
e2') = (Int, [(CId, CId)]) -> Expr -> ((Int, [(CId, CId)]), Expr)
forall a.
AlphaConvert a =>
(Int, [(CId, CId)]) -> a -> ((Int, [(CId, CId)]), a)
alphaConvert (Int, [(CId, CId)])
env' Expr
e2
    alphaConvert (Int, [(CId, CId)])
env expr :: Expr
expr@(EFun CId
i) = ((Int, [(CId, CId)])
env, Expr -> (CId -> Expr) -> Maybe CId -> Expr
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Expr
expr CId -> Expr
EFun (CId -> [(CId, CId)] -> Maybe CId
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup CId
i ((Int, [(CId, CId)]) -> [(CId, CId)]
forall a b. (a, b) -> b
snd (Int, [(CId, CId)])
env)))
    alphaConvert (Int, [(CId, CId)])
env Expr
expr = ((Int, [(CId, CId)])
env, Expr
expr)

-- pattern variables are not alpha converted
-- (but they probably should be...)
instance AlphaConvert Equation where
    alphaConvert :: (Int, [(CId, CId)]) -> Equation -> ((Int, [(CId, CId)]), Equation)
alphaConvert env :: (Int, [(CId, CId)])
env@(Int
_,[(CId, CId)]
subst) (Equ [Patt]
patterns Expr
result)
        = ((Int
ctr,[(CId, CId)]
subst), [Patt] -> Expr -> Equation
Equ [Patt]
patterns Expr
result')
        where ((Int
ctr,[(CId, CId)]
_), Expr
result') = (Int, [(CId, CId)]) -> Expr -> ((Int, [(CId, CId)]), Expr)
forall a.
AlphaConvert a =>
(Int, [(CId, CId)]) -> a -> ((Int, [(CId, CId)]), a)
alphaConvert (Int, [(CId, CId)])
env Expr
result