diff --git a/src/compiler/GF/Compile/PGFtoLProlog.hs b/src/compiler/GF/Compile/PGFtoLProlog.hs index 41d258b3b..418eff2a4 100644 --- a/src/compiler/GF/Compile/PGFtoLProlog.hs +++ b/src/compiler/GF/Compile/PGFtoLProlog.hs @@ -17,7 +17,9 @@ grammar2lambdaprolog_mod pgf = render $ where ppClauses cat fns = text "/*" <+> ppCId cat <+> text "*/" $$ - vcat [ppClause 0 1 [] f ty <> dot | (f,(ty,_,_)) <- fns] $$ + vcat [snd (ppClause (abstract pgf) 0 1 [] f ty) <> dot | (f,(ty,_,Nothing)) <- fns] $$ + space $$ + vcat [vcat (map (\eq -> equation2clause (abstract pgf) f eq <> dot) eqs) | (f,(_,_,Just eqs)) <- fns] $$ space grammar2lambdaprolog_sig pgf = render $ @@ -25,9 +27,10 @@ grammar2lambdaprolog_sig pgf = render $ space $$ vcat [ppCat c hyps <> dot | (c,(hyps,_)) <- Map.toList (cats (abstract pgf))] $$ space $$ - vcat [ppFun f ty <> dot | (f,(ty,_,_)) <- Map.toList (funs (abstract pgf))] $$ + vcat [ppFun f ty <> dot | (f,(ty,_,Nothing)) <- Map.toList (funs (abstract pgf))] $$ space $$ - vcat [ppExport c hyps <> dot | (c,(hyps,_)) <- Map.toList (cats (abstract pgf))] + vcat [ppExport c hyps <> dot | (c,(hyps,_)) <- Map.toList (cats (abstract pgf))] $$ + vcat [ppFunPred f (hyps ++ [(Explicit,wildCId,DTyp [] c es)]) <> dot | (f,(DTyp hyps c es,_,Just _)) <- Map.toList (funs (abstract pgf))] ppCat :: CId -> [Hypo] -> Doc ppCat c hyps = text "kind" <+> ppKind c <+> text "type" @@ -40,34 +43,53 @@ ppExport c hyps = text "exportdef" <+> ppPred c <+> foldr (\hyp doc -> ppHypo 1 where hyp = (Explicit,wildCId,DTyp [] c []) -ppClause :: Int -> Int -> [CId] -> CId -> Type -> Doc -ppClause d i scope f ty@(DTyp hyps cat args) +ppFunPred :: CId -> [Hypo] -> Doc +ppFunPred c hyps = text "exportdef" <+> ppCId c <+> foldr (\hyp doc -> ppHypo 1 hyp <+> text "->" <+> doc) (text "o") hyps + +ppClause :: Abstr -> Int -> Int -> [CId] -> CId -> Type -> (Int,Doc) +ppClause abstr d i scope f ty@(DTyp hyps cat args) | null hyps = let res = EFun f - in ppRes i scope cat (res : args) + (goals,i',head) = ppRes i scope cat (res : args) + in (i',(if null goals + then empty + else hsep (punctuate comma (map (ppExpr 0 i' scope) goals)) <> comma) + <+> + head) | otherwise = let (i',vars,scope',hdocs) = ppHypos i [] scope hyps (depType [] ty) res = foldl EApp (EFun f) (map EFun (reverse vars)) quants = if d > 0 then hsep (map (\v -> text "pi" <+> ppCId v <+> char '\\') vars) else empty - in ppParens (d > 0) (quants <+> ppRes i' scope' cat (res : args) <+> - (if null hdocs - then empty - else text ":-" <+> hsep (punctuate comma hdocs))) + (goals,i'',head) = ppRes i' scope' cat (res : args) + in (i'',(if null goals + then empty + else hsep (punctuate comma (map (ppExpr 0 i'' scope') goals)) <> comma) + <+> + (ppParens (d > 0) (quants <+> head <+> + (if null hdocs + then empty + else text ":-" <+> hsep (punctuate comma hdocs))))) where - ppRes i scope cat es = ppParens (d > 3) (ppPred cat <+> hsep (map (ppExpr 4 i scope) es)) + ppRes i scope cat es = + let ((goals,i'),es') = mapAccumL (\(goals,i) e -> let (goals',i',e') = expr2goal abstr scope goals i e [] + in ((goals',i'),e')) ([],i) es + in (goals,i',ppParens (d > 3) (ppPred cat <+> hsep (map (ppExpr 4 i' scope) es'))) ppHypos :: Int -> [CId] -> [CId] -> [(BindType,CId,Type)] -> [Int] -> (Int,[CId],[CId],[Doc]) ppHypos i vars scope [] [] = (i,vars,scope,[]) ppHypos i vars scope ((_,x,typ):hyps) (c:cs) - | x /= wildCId = let v = mkCId ("X_"++show i) - (i',vars',scope',docs) = ppHypos (i+1) (v:vars) (v:scope) hyps cs - in (i',vars',scope',if c == 0 then ppClause 1 (i+1) scope v typ : docs else docs) + | x /= wildCId = let v = mkVar i + (i',doc) = ppClause abstr 1 (i+1) scope v typ + (i'',vars',scope',docs) = ppHypos i' (v:vars) (v:scope) hyps cs + in (i'',vars',scope',if c == 0 then doc : docs else docs) ppHypos i vars scope ((_,x,typ):hyps) cs - = let v = mkCId ("X_"++show i) - (i',vars',scope',docs) = ppHypos (i+1) (v:vars) scope hyps cs - in (i',vars',scope',ppClause 1 (i+1) scope v typ : docs) - + = let v = mkVar i + (i',doc) = ppClause abstr 1 (i+1) scope v typ + (i'',vars',scope',docs) = ppHypos i' (v:vars) scope hyps cs + in (i'',vars',scope',doc : docs) + +mkVar i = mkCId ("X_"++show i) ppPred :: CId -> Doc ppPred cat = text "p_" <> ppCId cat @@ -82,7 +104,7 @@ ppType d (DTyp hyps cat args) ppHypo d (_,_,typ) = ppType d typ -ppExpr d i scope (EAbs b x e) = let v = mkCId ("X_"++show i) +ppExpr d i scope (EAbs b x e) = let v = mkVar i in ppParens (d > 1) (ppCId v <+> char '\\' <+> ppExpr 1 (i+1) (v:scope) e) ppExpr d i scope (EApp e1 e2) = ppParens (d > 3) ((ppExpr 3 i scope e1) <+> (ppExpr 4 i scope e2)) ppExpr d i scope (ELit l) = ppLit l @@ -110,3 +132,36 @@ depExpr counts (EVar j) = let (xs,c:ys) = splitAt j counts in xs++(c+1):ys depExpr counts (ETyped e ty)= depExpr counts e depExpr counts (EImplArg e) = depExpr counts e + +equation2clause abstr f (Equ ps e) = + let scope0 = foldl pattScope [] ps + scope = [mkVar i | i <- [0..n-1]] + n = length scope0 + + es = map (patt2expr scope0) ps + + (goals,_,goal) = expr2goal abstr scope [] n e [] + + in ppCId f <+> hsep (map (ppExpr 4 n scope) (es++[goal])) <+> + if null goals + then empty + else text ":-" <+> hsep (punctuate comma (map (ppExpr 0 n scope) (reverse goals))) + + +patt2expr scope (PApp f ps) = foldl EApp (EFun f) (map (patt2expr scope) ps) +patt2expr scope (PLit l) = ELit l +patt2expr scope (PVar x) = case findIndex (==x) scope of + Just i -> EVar i + Nothing -> error ("unknown variable "++showCId x) +patt2expr scope (PImplArg p)= EImplArg (patt2expr scope p) + +expr2goal abstr scope goals i (EApp e1 e2) args = + let (goals',i',e2') = expr2goal abstr scope goals i e2 [] + in expr2goal abstr scope goals' i' e1 (e2':args) +expr2goal abstr scope goals i (EFun f) args = + case Map.lookup f (funs abstr) of + Just (_,_,Just _) -> let e = EFun (mkVar i) + in (foldl EApp (EFun f) (args++[e]) : goals, i+1, e) + _ -> (goals,i,foldl EApp (EFun f) args) +expr2goal abstr scope goals i (EVar j) args = + (goals,i,foldl EApp (EVar j) args)