forked from GitHub/gf-core
refactor the PGF.Expr type and the evaluation of abstract expressions
This commit is contained in:
krasimir
2
GF.cabal
2
GF.cabal
@@ -47,7 +47,6 @@ library
|
||||
PGF.Expr
|
||||
PGF.Type
|
||||
PGF.PMCFG
|
||||
PGF.AbsCompute
|
||||
PGF.Paraphrase
|
||||
PGF.TypeCheck
|
||||
PGF.Binary
|
||||
@@ -165,7 +164,6 @@ executable gf
|
||||
PGF.Parsing.FCFG.Active
|
||||
PGF.Parsing.FCFG
|
||||
PGF.Binary
|
||||
PGF.AbsCompute
|
||||
PGF.Paraphrase
|
||||
PGF.TypeCheck
|
||||
PGF.Binary
|
||||
|
||||
@@ -600,11 +600,11 @@ allCommands cod env@(pgf, mos) = Map.fromList [
|
||||
exec = \opts arg -> do
|
||||
case arg of
|
||||
[Fun id []] -> case Map.lookup id (funs (abstract pgf)) of
|
||||
Just (ty,def) -> return $ fromString $
|
||||
Just (ty,eqs) -> return $ fromString $
|
||||
render (text "fun" <+> text (prCId id) <+> colon <+> ppType 0 ty $$
|
||||
if def == EEq []
|
||||
if null eqs
|
||||
then empty
|
||||
else text "def" <+> text (prCId id) <+> char '=' <+> ppExpr 0 def)
|
||||
else text "def" <+> vcat [text (prCId id) <+> hsep (map (ppPatt 9) patts) <+> char '=' <+> ppExpr 0 res | Equ patts res <- eqs])
|
||||
Nothing -> case Map.lookup id (cats (abstract pgf)) of
|
||||
Just hyps -> do return $ fromString $
|
||||
render (text "cat" <+> text (prCId id) <+> hsep (map ppHypo hyps) $$
|
||||
|
||||
@@ -4,10 +4,8 @@ module GF.Command.TreeOperations (
|
||||
) where
|
||||
|
||||
import GF.Compile.TypeCheck
|
||||
import PGF (compute,paraphrase,typecheck)
|
||||
import PGF
|
||||
|
||||
-- for conversions
|
||||
import PGF.Data
|
||||
--import GF.Compile.GrammarToGFCC (mkType,mkExp)
|
||||
import qualified GF.Grammar.Grammar as G
|
||||
import qualified GF.Grammar.Macros as M
|
||||
@@ -22,7 +20,7 @@ treeOp pgf f = fmap snd $ lookup f $ allTreeOps pgf
|
||||
allTreeOps :: PGF -> [(String,(String,TreeOp))]
|
||||
allTreeOps pgf = [
|
||||
("compute",("compute by using semantic definitions (def)",
|
||||
map (compute pgf))),
|
||||
map (expr2tree pgf . tree2expr))),
|
||||
("paraphrase",("paraphrase by using semantic definitions (def)",
|
||||
nub . concatMap (paraphrase pgf))),
|
||||
("smallest",("sort trees from smallest to largest, in number of nodes",
|
||||
|
||||
@@ -42,7 +42,7 @@ computeAbsTerm :: Grammar -> Exp -> Err Exp
|
||||
computeAbsTerm gr = computeAbsTermIn (lookupAbsDef gr) []
|
||||
|
||||
-- | a hack to make compute work on source grammar as well
|
||||
type LookDef = Ident -> Ident -> Err (Maybe Term)
|
||||
type LookDef = Ident -> Ident -> Err (Maybe [Equation])
|
||||
|
||||
computeAbsTermIn :: LookDef -> [Ident] -> Exp -> Err Exp
|
||||
computeAbsTermIn lookd xs e = errIn ("computing" +++ prt e) $ compt xs e where
|
||||
@@ -55,7 +55,7 @@ computeAbsTermIn lookd xs e = errIn ("computing" +++ prt e) $ compt xs e where
|
||||
let vv' = yy ++ vv
|
||||
aa' <- mapM (compt vv') aa
|
||||
case look f of
|
||||
Just (Eqs eqs) -> tracd ("\nmatching" +++ prt f) $
|
||||
Just eqs -> tracd ("\nmatching" +++ prt f) $
|
||||
case findMatch eqs aa' of
|
||||
Ok (d,g) -> do
|
||||
--- let (xs,ts) = unzip g
|
||||
@@ -67,19 +67,14 @@ computeAbsTermIn lookd xs e = errIn ("computing" +++ prt e) $ compt xs e where
|
||||
do
|
||||
let v = mkApp f aa'
|
||||
return $ mkAbs yy $ v
|
||||
Just d -> tracd ("define" +++ prt t') $ do
|
||||
da <- compt vv' $ mkApp d aa'
|
||||
return $ mkAbs yy $ da
|
||||
_ -> do
|
||||
let t2 = mkAbs yy $ mkApp f aa'
|
||||
tracd ("not defined" +++ prt_ t2) $ return t2
|
||||
|
||||
look t = case t of
|
||||
(Q m f) -> case lookd m f of
|
||||
Ok (Just EData) -> Nothing -- canonical --- should always be QC
|
||||
Ok md -> md
|
||||
_ -> Nothing
|
||||
Eqs _ -> return t ---- for nested fn
|
||||
_ -> Nothing
|
||||
|
||||
beta :: [Ident] -> Exp -> Exp
|
||||
|
||||
@@ -124,16 +124,14 @@ checkAbsInfo st m mo (c,info) = do
|
||||
AbsCat (Just cont) _ -> mkCheck "category" $
|
||||
checkContext st cont ---- also cstrs
|
||||
AbsFun (Just typ0) md -> do
|
||||
typ <- compAbsTyp [] typ0 -- to calculate let definitions
|
||||
mkCheck "type of function" $ checkTyp st typ
|
||||
md' <- case md of
|
||||
Just d -> do
|
||||
let d' = elimTables d
|
||||
---- mkCheckWarn "definition of function" $ checkEquation st (m,c) d'
|
||||
mkCheck "definition of function" $ checkEquation st (m,c) d'
|
||||
return $ Just d'
|
||||
_ -> return md
|
||||
return $ (c,AbsFun (Just typ) md')
|
||||
typ <- compAbsTyp [] typ0 -- to calculate let definitions
|
||||
mkCheck "type of function" $
|
||||
checkTyp st typ
|
||||
case md of
|
||||
Just eqs -> mkCheck "definition of function" $
|
||||
checkDef st (m,c) typ eqs
|
||||
Nothing -> return (c,info)
|
||||
return $ (c,AbsFun (Just typ) md)
|
||||
_ -> return (c,info)
|
||||
where
|
||||
mkCheck cat ss = case ss of
|
||||
@@ -161,17 +159,6 @@ checkAbsInfo st m mo (c,info) = do
|
||||
Abs _ _ -> return t
|
||||
_ -> composOp (compAbsTyp g) t
|
||||
|
||||
elimTables e = case e of
|
||||
S t a -> elimSel (elimTables t) (elimTables a)
|
||||
T _ cs -> Eqs [(elimPatt p, elimTables t) | (p,t) <- cs]
|
||||
_ -> composSafeOp elimTables e
|
||||
elimPatt p = case p of
|
||||
PR lps -> map snd lps
|
||||
_ -> [p]
|
||||
elimSel t a = case a of
|
||||
R fs -> mkApp t (map (snd . snd) fs)
|
||||
_ -> mkApp t [a]
|
||||
|
||||
checkCompleteGrammar :: SourceGrammar -> SourceModInfo -> SourceModInfo -> Check (BinTree Ident Info)
|
||||
checkCompleteGrammar gr abs cnc = do
|
||||
let jsa = jments abs
|
||||
|
||||
@@ -34,7 +34,7 @@ pgf2js pgf =
|
||||
abstract2js :: String -> Abstr -> JS.Expr
|
||||
abstract2js start ds = new "GFAbstract" [JS.EStr start, JS.EObj $ map absdef2js (Map.assocs (funs ds))]
|
||||
|
||||
absdef2js :: (CId,(Type,Expr)) -> JS.Property
|
||||
absdef2js :: (CId,(Type,[Equation])) -> JS.Property
|
||||
absdef2js (f,(typ,_)) =
|
||||
let (args,cat) = M.catSkeleton typ in
|
||||
JS.Prop (JS.IdentPropName (JS.Ident (prCId f))) (new "Type" [JS.EArray [JS.EStr (prCId x) | x <- args], JS.EStr (prCId cat)])
|
||||
|
||||
@@ -71,17 +71,17 @@ plCat (cat, hypos) = plFact "cat" (plTypeWithHypos typ)
|
||||
args = reverse [EVar x | (_,x) <- subst]
|
||||
typ = wildcardUnusedVars $ DTyp hypos' cat args
|
||||
|
||||
plFun :: (CId, (Type, Expr)) -> String
|
||||
plFun :: (CId, (Type, [Equation])) -> String
|
||||
plFun (fun, (typ, _)) = plFact "fun" (plp fun : plTypeWithHypos typ')
|
||||
where typ' = wildcardUnusedVars $ snd $ alphaConvert emptyEnv typ
|
||||
|
||||
plTypeWithHypos :: Type -> [String]
|
||||
plTypeWithHypos (DTyp hypos cat args) = [plTerm (plp cat) (map plp args), plp hypos]
|
||||
|
||||
plFundef :: (CId, (Type, Expr)) -> [String]
|
||||
plFundef (fun, (_, EEq [])) = []
|
||||
plFundef (fun, (_, fundef)) = [plFact "def" [plp fun, plp fundef']]
|
||||
where fundef' = snd $ alphaConvert emptyEnv fundef
|
||||
plFundef :: (CId, (Type, [Equation])) -> [String]
|
||||
plFundef (fun, (_, [])) = []
|
||||
plFundef (fun, (_, eqs)) = [plFact "def" [plp fun, plp fundef']]
|
||||
where fundef' = snd $ alphaConvert emptyEnv eqs
|
||||
|
||||
|
||||
----------------------------------------------------------------------
|
||||
@@ -122,8 +122,14 @@ instance PLPrint Expr where
|
||||
plp (EApp e e') = plOper " * " (plp e) (plp e')
|
||||
plp (ELit lit) = plp lit
|
||||
plp (EMeta n) = "Meta_" ++ show n
|
||||
plp (EEq eqs) = plList [plOper ":" (plp patterns) (plp result) |
|
||||
Equ patterns result <- eqs]
|
||||
|
||||
instance PLPrint Patt where
|
||||
plp (PVar x) = plp x
|
||||
plp (PApp f ps) = plOper " * " (plp f) (plp ps)
|
||||
plp (PLit lit) = plp lit
|
||||
|
||||
instance PLPrint Equation where
|
||||
plp (Equ patterns result) = plOper ":" (plp patterns) (plp result)
|
||||
|
||||
instance PLPrint Term where
|
||||
plp (S terms) = plTerm "s" [plp terms]
|
||||
@@ -267,17 +273,14 @@ instance AlphaConvert Expr where
|
||||
where (env', e1') = alphaConvert env e1
|
||||
(env'', e2') = alphaConvert env' e2
|
||||
alphaConvert env expr@(EVar i) = (env, maybe expr EVar (lookup i (snd env)))
|
||||
alphaConvert env (EEq eqs) = (env', EEq eqs')
|
||||
where (env', eqs') = alphaConvert env eqs
|
||||
alphaConvert env expr = (env, expr)
|
||||
|
||||
-- pattern variables are not alpha converted
|
||||
-- (but they probably should be...)
|
||||
instance AlphaConvert Equation where
|
||||
alphaConvert env@(_,subst) (Equ patterns result)
|
||||
= ((ctr,subst), Equ patterns' result')
|
||||
where (env', patterns') = alphaConvert env patterns
|
||||
((ctr,_), result') = alphaConvert env' result
|
||||
= ((ctr,subst), Equ patterns result')
|
||||
where ((ctr,_), result') = alphaConvert env result
|
||||
|
||||
----------------------------------------------------------------------
|
||||
-- translate unused variables to wildcards
|
||||
@@ -295,6 +298,4 @@ wildcardUnusedVars typ@(DTyp hypos cat args) = DTyp hypos' cat args
|
||||
unusedInExpr x (EAbs y e) = unusedInExpr x e
|
||||
unusedInExpr x (EApp e e') = unusedInExpr x e && unusedInExpr x e'
|
||||
unusedInExpr x (EVar y) = x/=y
|
||||
unusedInExpr x (EEq eqs) = and [all (unusedInExpr x) (result:patterns) |
|
||||
Equ patterns result <- eqs]
|
||||
unusedInExpr x expr = True
|
||||
|
||||
@@ -43,7 +43,7 @@ convertConcrete abs cnc = fixHoasFuns $ convert abs_defs' conc' cats'
|
||||
cats = lincats cnc
|
||||
(abs_defs',conc',cats') = expandHOAS abs_defs conc cats
|
||||
|
||||
expandHOAS :: [(CId,(Type,Expr))] -> TermMap -> TermMap -> ([(CId,(Type,Expr))],TermMap,TermMap)
|
||||
expandHOAS :: [(CId,(Type,[Equation]))] -> TermMap -> TermMap -> ([(CId,(Type,[Equation]))],TermMap,TermMap)
|
||||
expandHOAS funs lins lincats = (funs' ++ hoFuns ++ varFuns,
|
||||
Map.unions [lins, hoLins, varLins],
|
||||
Map.unions [lincats, hoLincats, varLincat])
|
||||
@@ -59,14 +59,14 @@ expandHOAS funs lins lincats = (funs' ++ hoFuns ++ varFuns,
|
||||
hoCats = sortNub (map snd hoTypes)
|
||||
-- for each Cat with N bindings, we add a new category _NCat
|
||||
-- each new category contains a single function __NCat : Cat -> _Var -> ... -> _Var -> _NCat
|
||||
hoFuns = [(funName ty,(cftype (c : replicate n varCat) (catName ty),EEq [])) | ty@(n,c) <- hoTypes]
|
||||
hoFuns = [(funName ty,(cftype (c : replicate n varCat) (catName ty),[])) | ty@(n,c) <- hoTypes]
|
||||
-- lincats for the new categories
|
||||
hoLincats = Map.fromList [(catName ty, modifyRec (++ replicate n (S [])) (lincatOf c)) | ty@(n,c) <- hoTypes]
|
||||
-- linearizations of the new functions, lin __NCat v_0 ... v_n-1 x = { s1 = x.s1; ...; sk = x.sk; $0 = v_0.s ...
|
||||
hoLins = Map.fromList [ (funName ty, mkLin c n) | ty@(n,c) <- hoTypes]
|
||||
where mkLin c n = modifyRec (\fs -> [P (V 0) (C j) | j <- [0..length fs-1]] ++ [P (V i) (C 0) | i <- [1..n]]) (lincatOf c)
|
||||
-- for each Cat, we a add a fun _Var_Cat : _Var -> Cat
|
||||
varFuns = [(varFunName cat, (cftype [varCat] cat,EEq [])) | cat <- hoCats]
|
||||
varFuns = [(varFunName cat, (cftype [varCat] cat,[])) | cat <- hoCats]
|
||||
-- linearizations of the _Var_Cat functions
|
||||
varLins = Map.fromList [(varFunName cat, R [P (V 0) (C 0)]) | cat <- hoCats]
|
||||
-- lincat for the _Var category
|
||||
@@ -98,7 +98,7 @@ fixHoasFuns pinfo = pinfo{functions=mkArray [FFun (fixName n) prof lins | FFun n
|
||||
| BS.pack "_Var_" `BS.isPrefixOf` n = wildCId
|
||||
fixName n = n
|
||||
|
||||
convert :: [(CId,(Type,Expr))] -> TermMap -> TermMap -> ParserInfo
|
||||
convert :: [(CId,(Type,[Equation]))] -> TermMap -> TermMap -> ParserInfo
|
||||
convert abs_defs cnc_defs cat_defs = getParserInfo (loop grammarEnv)
|
||||
where
|
||||
srules = [
|
||||
|
||||
@@ -38,7 +38,7 @@ convertConcrete abs cnc = convert abs_defs conc cats
|
||||
conc = Map.union (opers cnc) (lins cnc) -- "union big+small most efficient"
|
||||
cats = lincats cnc
|
||||
|
||||
convert :: [(CId,(Type,Expr))] -> TermMap -> TermMap -> ParserInfo
|
||||
convert :: [(CId,(Type,[Equation]))] -> TermMap -> TermMap -> ParserInfo
|
||||
convert abs_defs cnc_defs cat_defs =
|
||||
let env = expandHOAS abs_defs cnc_defs cat_defs (emptyGrammarEnv cnc_defs cat_defs)
|
||||
in getParserInfo (List.foldl' (convertRule cnc_defs) env pfrules)
|
||||
|
||||
@@ -68,9 +68,9 @@ canon2gfcc opts pars cgr@(M.MGrammar ((a,abm):cms)) =
|
||||
abs = D.Abstr aflags funs cats catfuns
|
||||
gflags = Map.empty
|
||||
aflags = Map.fromList [(mkCId f,x) | (f,x) <- optionsPGF (M.flags abm)]
|
||||
mkDef pty = case pty of
|
||||
Just t -> mkExp t
|
||||
_ -> CM.primNotion
|
||||
|
||||
mkDef (Just eqs) = [C.Equ (map mkPatt ps) (mkExp e) | (ps,e) <- eqs]
|
||||
mkDef Nothing = []
|
||||
|
||||
-- concretes
|
||||
lfuns = [(f', (mkType ty, mkDef pty)) |
|
||||
@@ -119,9 +119,7 @@ mkType t = case GM.typeForm t of
|
||||
Ok (hyps,(_,cat),args) -> C.DTyp (mkContext hyps) (i2i cat) (map mkExp args)
|
||||
|
||||
mkExp :: A.Term -> C.Expr
|
||||
mkExp t = case t of
|
||||
A.Eqs eqs -> C.EEq [C.Equ (map mkPatt ps) (mkExp e) | (ps,e) <- eqs]
|
||||
_ -> case GM.termForm t of
|
||||
mkExp t = case GM.termForm t of
|
||||
Ok (xs,c,args) -> mkAbs xs (mkApp c (map mkExp args))
|
||||
where
|
||||
mkAbs xs t = foldr (C.EAbs . i2i) t xs
|
||||
@@ -134,11 +132,15 @@ mkExp t = case t of
|
||||
K s -> C.ELit (C.LStr s)
|
||||
Meta (MetaSymb i) -> C.EMeta i
|
||||
_ -> C.EMeta 0
|
||||
mkPatt p = case p of
|
||||
A.PP _ c ps -> foldl C.EApp (C.EVar (i2i c)) (map mkPatt ps)
|
||||
A.PV x -> C.EVar (i2i x)
|
||||
A.PW -> C.EVar wildCId
|
||||
A.PInt i -> C.ELit (C.LInt i)
|
||||
|
||||
mkPatt p = case p of
|
||||
A.PP _ c ps -> C.PApp (i2i c) (map mkPatt ps)
|
||||
A.PV x -> C.PVar (i2i x)
|
||||
A.PW -> C.PWild
|
||||
A.PInt i -> C.PLit (C.LInt i)
|
||||
A.PFloat f -> C.PLit (C.LFlt f)
|
||||
A.PString s -> C.PLit (C.LStr s)
|
||||
|
||||
|
||||
mkContext :: A.Context -> [C.Hypo]
|
||||
mkContext hyps = [C.Hyp (i2i x) (mkType ty) | (x,ty) <- hyps]
|
||||
|
||||
@@ -31,7 +31,7 @@ prCat :: CId -> [Hypo] -> Doc
|
||||
prCat c h | isLiteralCat c = empty
|
||||
| otherwise = text "cat" <+> text (prCId c)
|
||||
|
||||
prFun :: CId -> (Type,Expr) -> Doc
|
||||
prFun :: CId -> (Type,[Equation]) -> Doc
|
||||
prFun f (t,_) = text "fun" <+> text (prCId f) <+> text ":" <+> prType t
|
||||
|
||||
prType :: Type -> Doc
|
||||
|
||||
@@ -116,7 +116,7 @@ renameIdentPatt env p = do
|
||||
|
||||
info2status :: Maybe Ident -> (Ident,Info) -> StatusInfo
|
||||
info2status mq (c,i) = case i of
|
||||
AbsFun _ (Just EData) -> maybe Con QC mq
|
||||
AbsFun _ Nothing -> maybe Con QC mq
|
||||
ResValue _ -> maybe Con QC mq
|
||||
ResParam _ -> maybe Con QC mq
|
||||
AnyInd True m -> maybe Con (const (QC m)) mq
|
||||
@@ -156,8 +156,7 @@ renameInfo mo status (i,info) = errIn
|
||||
liftM ((,) i) $ case info of
|
||||
AbsCat pco pfs -> liftM2 AbsCat (renPerh (renameContext status) pco)
|
||||
(renPerh (mapM rent) pfs)
|
||||
AbsFun pty ptr -> liftM2 AbsFun (ren pty) (ren ptr)
|
||||
|
||||
AbsFun pty ptr -> liftM2 AbsFun (ren pty) (renPerh (mapM (renameEquation status [])) ptr)
|
||||
ResOper pty ptr -> liftM2 ResOper (ren pty) (ren ptr)
|
||||
ResOverload os tysts ->
|
||||
liftM (ResOverload os) (mapM (pairM rent) tysts)
|
||||
@@ -191,7 +190,6 @@ renameTerm env vars = ren vars where
|
||||
Con _ -> renid trm
|
||||
Q _ _ -> renid trm
|
||||
QC _ _ -> renid trm
|
||||
Eqs eqs -> liftM Eqs $ mapM (renameEquation env vars) eqs
|
||||
T i cs -> do
|
||||
i' <- case i of
|
||||
TTyped ty -> liftM TTyped $ ren vs ty -- the only annotation in source
|
||||
|
||||
@@ -16,6 +16,7 @@ module GF.Compile.TC (AExp(..),
|
||||
Theory,
|
||||
checkExp,
|
||||
inferExp,
|
||||
checkBranch,
|
||||
eqVal,
|
||||
whnf
|
||||
) where
|
||||
@@ -122,7 +123,6 @@ checkExp th tenv@(k,rho,gamma) e ty = do
|
||||
let v = VGen k
|
||||
case e of
|
||||
Meta m -> return $ (AMeta m typ,[])
|
||||
EData -> return $ (AData typ,[])
|
||||
|
||||
Abs x t -> case typ of
|
||||
VClos env (Prod y a b) -> do
|
||||
@@ -132,11 +132,6 @@ checkExp th tenv@(k,rho,gamma) e ty = do
|
||||
return (AAbs x a' t', cs)
|
||||
_ -> prtBad ("function type expected for" +++ prt e +++ "instead of") typ
|
||||
|
||||
Eqs es -> do
|
||||
bcs <- mapM (\b -> checkBranch th tenv b typ) es
|
||||
let (bs,css) = unzip bcs
|
||||
return (AEqs bs, concat css)
|
||||
|
||||
Prod x a b -> do
|
||||
testErr (typ == vType) "expected Type"
|
||||
(a',csa) <- checkType th tenv a
|
||||
|
||||
@@ -15,7 +15,7 @@
|
||||
module GF.Compile.TypeCheck (-- * top-level type checking functions; TC should not be called directly.
|
||||
checkContext,
|
||||
checkTyp,
|
||||
checkEquation,
|
||||
checkDef,
|
||||
checkConstrs,
|
||||
) where
|
||||
|
||||
@@ -71,11 +71,12 @@ checkContext st = checkTyp st . cont2exp
|
||||
checkTyp :: Grammar -> Type -> [String]
|
||||
checkTyp gr typ = err singleton prConstrs $ justTypeCheck gr typ vType
|
||||
|
||||
checkEquation :: Grammar -> Fun -> Term -> [String]
|
||||
checkEquation gr (m,fun) def = err singleton prConstrs $ do
|
||||
typ <- lookupFunType gr m fun
|
||||
cs <- justTypeCheck gr def (vClos typ)
|
||||
return $ filter notJustMeta cs
|
||||
checkDef :: Grammar -> Fun -> Type -> [Equation] -> [String]
|
||||
checkDef gr (m,fun) typ eqs = err singleton prConstrs $ do
|
||||
bcs <- mapM (\b -> checkBranch (grammar2theory gr) (initTCEnv []) b (type2val typ)) eqs
|
||||
let (bs,css) = unzip bcs
|
||||
(constrs,_) <- unifyVal (concat css)
|
||||
return $ filter notJustMeta constrs
|
||||
|
||||
checkConstrs :: Grammar -> Cat -> [Ident] -> [String]
|
||||
checkConstrs gr cat _ = [] ---- check constructors!
|
||||
|
||||
@@ -163,7 +163,7 @@ extendMod gr isCompl (name,cond) base old new = foldM try new $ Map.toList old
|
||||
(b,n') = case info of
|
||||
ResValue _ -> (True,n)
|
||||
ResParam _ -> (True,n)
|
||||
AbsFun _ (Just EData) -> (True,n)
|
||||
AbsFun _ Nothing -> (True,n)
|
||||
AnyInd b k -> (b,k)
|
||||
_ -> (False,n) ---- canonical in Abs
|
||||
|
||||
@@ -203,13 +203,11 @@ unifMaybe (Just p1) (Just p2)
|
||||
| p1==p2 = return (Just p1)
|
||||
| otherwise = fail ""
|
||||
|
||||
unifAbsDefs :: Maybe Term -> Maybe Term -> Err (Maybe Term)
|
||||
unifAbsDefs p1 p2 = case (p1,p2) of
|
||||
(Nothing, _) -> return p2
|
||||
(_, Nothing) -> return p1
|
||||
(Just (Eqs bs), Just (Eqs ds))
|
||||
-> return $ Just $ Eqs $ bs ++ ds --- order!
|
||||
_ -> fail "definitions"
|
||||
unifAbsDefs :: Maybe [Equation] -> Maybe [Equation] -> Err (Maybe [Equation])
|
||||
unifAbsDefs Nothing Nothing = return Nothing
|
||||
unifAbsDefs (Just _ ) Nothing = fail ""
|
||||
unifAbsDefs Nothing (Just _ ) = fail ""
|
||||
unifAbsDefs (Just xs) (Just ys) = return (Just (xs ++ ys))
|
||||
|
||||
unifConstrs :: Maybe [Term] -> Maybe [Term] -> Err (Maybe [Term])
|
||||
unifConstrs p1 p2 = case (p1,p2) of
|
||||
|
||||
@@ -115,7 +115,6 @@ instance Binary Term where
|
||||
put (Vr x) = putWord8 0 >> put x
|
||||
put (Cn x) = putWord8 1 >> put x
|
||||
put (Con x) = putWord8 2 >> put x
|
||||
put (EData) = putWord8 3
|
||||
put (Sort x) = putWord8 4 >> put x
|
||||
put (EInt x) = putWord8 5 >> put x
|
||||
put (EFloat x) = putWord8 6 >> put x
|
||||
@@ -125,7 +124,6 @@ instance Binary Term where
|
||||
put (Abs x y) = putWord8 10 >> put (x,y)
|
||||
put (Meta x) = putWord8 11 >> put x
|
||||
put (Prod x y z) = putWord8 12 >> put (x,y,z)
|
||||
put (Eqs x) = putWord8 13 >> put x
|
||||
put (Typed x y) = putWord8 14 >> put (x,y)
|
||||
put (Example x y) = putWord8 15 >> put (x,y)
|
||||
put (RecType x) = putWord8 16 >> put x
|
||||
@@ -155,7 +153,6 @@ instance Binary Term where
|
||||
0 -> get >>= \x -> return (Vr x)
|
||||
1 -> get >>= \x -> return (Cn x)
|
||||
2 -> get >>= \x -> return (Con x)
|
||||
3 -> return (EData)
|
||||
4 -> get >>= \x -> return (Sort x)
|
||||
5 -> get >>= \x -> return (EInt x)
|
||||
6 -> get >>= \x -> return (EFloat x)
|
||||
@@ -165,7 +162,6 @@ instance Binary Term where
|
||||
10 -> get >>= \(x,y) -> return (Abs x y)
|
||||
11 -> get >>= \x -> return (Meta x)
|
||||
12 -> get >>= \(x,y,z) -> return (Prod x y z)
|
||||
13 -> get >>= \x -> return (Eqs x)
|
||||
14 -> get >>= \(x,y) -> return (Typed x y)
|
||||
15 -> get >>= \(x,y) -> return (Example x y)
|
||||
16 -> get >>= \x -> return (RecType x)
|
||||
|
||||
@@ -81,7 +81,7 @@ type PValues = [Term]
|
||||
data Info =
|
||||
-- judgements in abstract syntax
|
||||
AbsCat (Maybe Context) (Maybe [Term]) -- ^ (/ABS/) constructors; must be 'Id' or 'QId'
|
||||
| AbsFun (Maybe Type) (Maybe Term) -- ^ (/ABS/) 'Yes f' = canonical
|
||||
| AbsFun (Maybe Type) (Maybe [Equation]) -- ^ (/ABS/)
|
||||
|
||||
-- judgements in resource
|
||||
| ResParam (Maybe ([Param],Maybe PValues)) -- ^ (/RES/)
|
||||
@@ -108,7 +108,6 @@ data Term =
|
||||
Vr Ident -- ^ variable
|
||||
| Cn Ident -- ^ constant
|
||||
| Con Ident -- ^ constructor
|
||||
| EData -- ^ to mark in definition that a fun is a constructor
|
||||
| Sort Ident -- ^ basic type
|
||||
| EInt Integer -- ^ integer literal
|
||||
| EFloat Double -- ^ floating point literal
|
||||
@@ -119,8 +118,6 @@ data Term =
|
||||
| Abs Ident Term -- ^ abstraction: @\x -> b@
|
||||
| Meta MetaSymb -- ^ metavariable: @?i@ (only parsable: ? = ?0)
|
||||
| Prod Ident Term Term -- ^ function type: @(x : A) -> B@
|
||||
| Eqs [Equation] -- ^ abstraction by cases: @fn {x y -> b ; z u -> c}@
|
||||
-- only used in internal representation
|
||||
| Typed Term Term -- ^ type-annotated term
|
||||
--
|
||||
-- /below this, the constructors are only for concrete syntax/
|
||||
|
||||
@@ -227,7 +227,7 @@ qualifAnnotPar m t = case t of
|
||||
Con c -> QC m c
|
||||
_ -> composSafeOp (qualifAnnotPar m) t
|
||||
|
||||
lookupAbsDef :: SourceGrammar -> Ident -> Ident -> Err (Maybe Term)
|
||||
lookupAbsDef :: SourceGrammar -> Ident -> Ident -> Err (Maybe [Equation])
|
||||
lookupAbsDef gr m c = errIn ("looking up absdef of" +++ prt c) $ do
|
||||
mo <- lookupModule gr m
|
||||
info <- lookupIdentInfo mo c
|
||||
|
||||
@@ -593,10 +593,6 @@ composOp co trm =
|
||||
i' <- changeTableType co i
|
||||
return (TSh i' cc')
|
||||
|
||||
Eqs cc ->
|
||||
do cc' <- mapPairListM (co . snd) cc
|
||||
return (Eqs cc')
|
||||
|
||||
V ty vs ->
|
||||
do ty' <- co ty
|
||||
vs' <- mapM co vs
|
||||
|
||||
@@ -72,7 +72,6 @@ import GF.Compile.Update (buildAnyTree)
|
||||
'data' { T_data }
|
||||
'def' { T_def }
|
||||
'flags' { T_flags }
|
||||
'fn' { T_fn }
|
||||
'fun' { T_fun }
|
||||
'in' { T_in }
|
||||
'incomplete' { T_incomplete}
|
||||
@@ -241,19 +240,19 @@ CatDef
|
||||
|
||||
FunDef :: { [(Ident,SrcSpan,Info)] }
|
||||
FunDef
|
||||
: Posn ListIdent ':' Exp Posn { [(fun, ($1,$5), AbsFun (Just $4) Nothing) | fun <- $2] }
|
||||
: Posn ListIdent ':' Exp Posn { [(fun, ($1,$5), AbsFun (Just $4) (Just [])) | fun <- $2] }
|
||||
|
||||
DefDef :: { [(Ident,SrcSpan,Info)] }
|
||||
DefDef
|
||||
: Posn ListName '=' Exp Posn { [(f, ($1,$5),AbsFun Nothing (Just $4)) | f <- $2] }
|
||||
| Posn Name ListPatt '=' Exp Posn { [($2,($1,$6),AbsFun Nothing (Just (Eqs [($3,$5)])))] }
|
||||
: Posn ListName '=' Exp Posn { [(f, ($1,$5),AbsFun Nothing (Just [([],$4)])) | f <- $2] }
|
||||
| Posn Name ListPatt '=' Exp Posn { [($2,($1,$6),AbsFun Nothing (Just [($3,$5)]))] }
|
||||
|
||||
DataDef :: { [(Ident,SrcSpan,Info)] }
|
||||
DataDef
|
||||
: Posn Ident '=' ListDataConstr Posn { ($2, ($1,$5), AbsCat Nothing (Just (map Cn $4))) :
|
||||
[(fun, ($1,$5), AbsFun Nothing (Just EData)) | fun <- $4] }
|
||||
| Posn ListIdent ':' Exp Posn { [(cat, ($1,$5), AbsCat Nothing (Just (map Cn $2))) | Ok (_,cat) <- [valCat $4]] ++
|
||||
[(fun, ($1,$5), AbsFun (Just $4) (Just EData)) | fun <- $2] }
|
||||
: Posn Ident '=' ListDataConstr Posn { ($2, ($1,$5), AbsCat Nothing (Just (map Cn $4))) :
|
||||
[(fun, ($1,$5), AbsFun Nothing Nothing) | fun <- $4] }
|
||||
| Posn ListIdent ':' Exp Posn { [(cat, ($1,$5), AbsCat Nothing (Just (map Cn $2))) | Ok (_,cat) <- [valCat $4]] ++
|
||||
[(fun, ($1,$5), AbsFun (Just $4) Nothing) | fun <- $2] }
|
||||
|
||||
ParamDef :: { [(Ident,SrcSpan,Info)] }
|
||||
ParamDef
|
||||
@@ -385,7 +384,6 @@ Exp
|
||||
| Exp3 'where' '{' ListLocDef '}' {%
|
||||
do defs <- mapM tryLoc $4
|
||||
return $ mkLet defs $1 }
|
||||
| 'fn' '{' ListEquation '}' { Eqs $3 }
|
||||
| 'in' Exp5 String { Example $2 $3 }
|
||||
| Exp1 { $1 }
|
||||
|
||||
@@ -441,7 +439,6 @@ Exp6
|
||||
| Double { EFloat $1 }
|
||||
| '?' { Meta (int2meta 0) }
|
||||
| '[' ']' { Empty }
|
||||
| 'data' { EData }
|
||||
| '[' Ident Exps ']' { foldl App (Vr (mkListId $2)) $3 }
|
||||
| '[' String ']' { case $2 of
|
||||
[] -> Empty
|
||||
@@ -486,7 +483,6 @@ Patt2
|
||||
| '#' Ident '.' Ident { PM $2 $4 }
|
||||
| '_' { wildPatt }
|
||||
| Ident { PV $1 }
|
||||
| '{' Ident '}' { PC $2 [] }
|
||||
| Ident '.' Ident { PP $1 $3 [] }
|
||||
| Integer { PInt $1 }
|
||||
| Double { PFloat $1 }
|
||||
@@ -569,15 +565,6 @@ ListCase
|
||||
: Case { [$1] }
|
||||
| Case ';' ListCase { $1 : $3 }
|
||||
|
||||
Equation :: { Equation }
|
||||
Equation
|
||||
: ListPatt '->' Exp { ($1,$3) }
|
||||
|
||||
ListEquation :: { [Equation] }
|
||||
ListEquation
|
||||
: Equation { (:[]) $1 }
|
||||
| Equation ';' ListEquation { (:) $1 $3 }
|
||||
|
||||
Altern :: { (Term,Term) }
|
||||
Altern
|
||||
: Exp '/' Exp { ($1,$3) }
|
||||
@@ -621,9 +608,9 @@ listCatDef id pos cont size = [catd,nilfund,consfund]
|
||||
baseId = mkBaseId id
|
||||
consId = mkConsId id
|
||||
|
||||
catd = (listId, pos, AbsCat (Just cont') (Just [Cn baseId,Cn consId]))
|
||||
nilfund = (baseId, pos, AbsFun (Just niltyp) (Just EData))
|
||||
consfund = (consId, pos, AbsFun (Just constyp) (Just EData))
|
||||
catd = (listId, pos, AbsCat (Just cont') (Just [Cn baseId,Cn consId]))
|
||||
nilfund = (baseId, pos, AbsFun (Just niltyp) Nothing)
|
||||
consfund = (consId, pos, AbsFun (Just constyp) Nothing)
|
||||
|
||||
cont' = [(mkId x i,ty) | (i,(x,ty)) <- zip [0..] cont]
|
||||
xs = map (Vr . fst) cont'
|
||||
|
||||
@@ -84,10 +84,8 @@ ppJudgement q (id, AbsFun ptype pexp) =
|
||||
Just typ -> text "fun" <+> ppIdent id <+> colon <+> ppTerm q 0 typ <+> semi
|
||||
Nothing -> empty) $$
|
||||
(case pexp of
|
||||
Just EData -> empty
|
||||
Just (Eqs [(ps,e)]) -> text "def" <+> ppIdent id <+> hcat (map (ppPatt q 2) ps) <+> equals <+> ppTerm q 0 e <+> semi
|
||||
Just exp -> text "def" <+> ppIdent id <+> equals <+> ppTerm q 0 exp <+> semi
|
||||
Nothing -> empty)
|
||||
Just eqs -> text "def" <+> vcat [ppIdent id <+> hsep (map (ppPatt q 2) ps) <+> equals <+> ppTerm q 0 e <+> semi | (ps,e) <- eqs]
|
||||
Nothing -> empty)
|
||||
ppJudgement q (id, ResParam pparams) =
|
||||
text "param" <+> ppIdent id <+>
|
||||
(case pparams of
|
||||
@@ -145,9 +143,6 @@ ppTerm q d (Prod x a b)= if x == identW
|
||||
ppTerm q d (Table kt vt)=prec d 0 (ppTerm q 3 kt <+> text "=>" <+> ppTerm q 0 vt)
|
||||
ppTerm q d (Let l e) = let (ls,e') = getLet e
|
||||
in prec d 0 (text "let" <+> vcat (map (ppLocDef q) (l:ls)) $$ text "in" <+> ppTerm q 0 e')
|
||||
ppTerm q d (Eqs es) = text "fn" <+> lbrace $$
|
||||
nest 2 (vcat (map (\e -> ppEquation q e <+> semi) es)) $$
|
||||
rbrace
|
||||
ppTerm q d (Example e s)=prec d 0 (text "in" <+> ppTerm q 5 e <+> text (show s))
|
||||
ppTerm q d (C e1 e2) =prec d 1 (ppTerm q 2 e1 <+> text "++" <+> ppTerm q 1 e2)
|
||||
ppTerm q d (Glue e1 e2) =prec d 2 (ppTerm q 3 e1 <+> char '+' <+> ppTerm q 2 e2)
|
||||
@@ -182,7 +177,6 @@ ppTerm q d (EInt n) = integer n
|
||||
ppTerm q d (EFloat f) = double f
|
||||
ppTerm q d (Meta _) = char '?'
|
||||
ppTerm q d (Empty) = text "[]"
|
||||
ppTerm q d (EData) = text "data"
|
||||
ppTerm q d (R xs) = braces (fsep (punctuate semi [ppLabel l <+>
|
||||
fsep [case mb_t of {Just t -> colon <+> ppTerm q 0 t; Nothing -> empty},
|
||||
equals <+> ppTerm q 0 e] | (l,(mb_t,e)) <- xs]))
|
||||
|
||||
@@ -75,10 +75,9 @@ mkTopDefs ds = ds
|
||||
trAnyDef :: (Ident,Info) -> [P.TopDef]
|
||||
trAnyDef (i,info) = let i' = tri i in case info of
|
||||
AbsCat (Just co) pd -> [P.DefCat [P.SimpleCatDef i' (map trDecl co)]]
|
||||
AbsFun (Just ty) (Just EData) -> [P.DefFunData [P.FunDef [i'] (trt ty)]]
|
||||
AbsFun (Just ty) pt -> [P.DefFun [P.FunDef [i'] (trt ty)]] ++ case pt of
|
||||
Just t -> [P.DefDef [P.DDef [mkName i'] (trt t)]]
|
||||
Nothing -> []
|
||||
AbsFun (Just ty) Nothing -> [P.DefFunData [P.FunDef [i'] (trt ty)]]
|
||||
AbsFun (Just ty) (Just eqs) -> [P.DefFun [P.FunDef [i'] (trt ty)]] ++
|
||||
[P.DefDef [P.DPatt (mkName i') (map trp patts) (trt res)] | (patts,res) <- eqs]
|
||||
|
||||
ResOper pty ptr -> [P.DefOper [trDef i' pty ptr]]
|
||||
ResParam pp -> [P.DefPar [case pp of
|
||||
@@ -129,7 +128,6 @@ trt trm = case trm of
|
||||
error $ "not yet sort " +++ show trm
|
||||
App c a -> P.EApp (trt c) (trt a)
|
||||
Abs x b -> P.EAbstr [trb x] (trt b)
|
||||
Eqs pts -> P.EEqs [P.Equ (map trp ps) (trt t) | (ps,t) <- pts]
|
||||
Meta m -> P.EMeta
|
||||
Prod x a b | isWildIdent x -> P.EProd (P.DExp (trt a)) (trt b)
|
||||
Prod x a b -> P.EProd (P.DDec [trb x] (trt a)) (trt b)
|
||||
@@ -178,7 +176,6 @@ trt trm = case trm of
|
||||
Alts (t, tt) -> P.EPre (trt t) [P.Alt (trt v) (trt c) | (v,c) <- tt]
|
||||
FV ts -> P.EVariants $ map trt ts
|
||||
Strs tt -> P.EStrs $ map trt tt
|
||||
EData -> P.EData
|
||||
Val te _ _ -> trt te ----
|
||||
_ -> error $ "not yet" +++ show trm ----
|
||||
|
||||
|
||||
10
src/PGF.hs
10
src/PGF.hs
@@ -48,7 +48,7 @@ module PGF(
|
||||
parse, canParse, parseAllLang, parseAll,
|
||||
|
||||
-- ** Evaluation
|
||||
tree2expr, expr2tree, compute, paraphrase, typecheck,
|
||||
tree2expr, PGF.expr2tree, paraphrase, typecheck,
|
||||
|
||||
-- ** Word Completion (Incremental Parsing)
|
||||
complete,
|
||||
@@ -62,7 +62,6 @@ module PGF(
|
||||
import PGF.CId
|
||||
import PGF.Linearize
|
||||
import PGF.Generate
|
||||
import PGF.AbsCompute
|
||||
import PGF.TypeCheck
|
||||
import PGF.Paraphrase
|
||||
import PGF.Macros
|
||||
@@ -287,3 +286,10 @@ complete pgf from typ input =
|
||||
| null ws = ([],"")
|
||||
| otherwise = (init ws, last ws)
|
||||
where ws = words s
|
||||
|
||||
-- | Converts an expression to tree. The expression
|
||||
-- is first reduced to beta-eta-alfa normal form and
|
||||
-- after that converted to tree. The function definitions
|
||||
-- are used in the computation.
|
||||
expr2tree :: PGF -> Expr -> Tree
|
||||
expr2tree pgf = PGF.Data.expr2tree (funs (abstract pgf))
|
||||
|
||||
@@ -1,106 +0,0 @@
|
||||
----------------------------------------------------------------------
|
||||
-- |
|
||||
-- Module : AbsCompute
|
||||
-- Maintainer : AR
|
||||
-- Stability : (stable)
|
||||
-- Portability : (portable)
|
||||
--
|
||||
-- computation in abstract syntax with def definitions.
|
||||
--
|
||||
-- modified from src GF computation
|
||||
-----------------------------------------------------------------------------
|
||||
|
||||
module PGF.AbsCompute (
|
||||
compute
|
||||
) where
|
||||
|
||||
import PGF.Data
|
||||
import PGF.Macros (lookDef,isData)
|
||||
import PGF.Expr
|
||||
import PGF.CId
|
||||
|
||||
compute :: PGF -> Tree -> Tree
|
||||
compute pgf = computeAbsTermIn pgf []
|
||||
|
||||
computeAbsTermIn :: PGF -> [CId] -> Tree -> Tree
|
||||
computeAbsTermIn pgf vv = expr2tree . compt vv . tree2expr where
|
||||
compt vv t =
|
||||
let
|
||||
t' = beta vv t
|
||||
(yy,f,aa) = exprForm t'
|
||||
vv' = yy ++ vv
|
||||
aa' = map (compt vv') aa
|
||||
in
|
||||
mkAbs yy $ case look f of
|
||||
Left (EEq eqs) -> case match eqs aa' of
|
||||
Just (d,g) -> compt vv' $ subst vv' g d
|
||||
_ -> mkApp f aa'
|
||||
Left (EMeta _) -> mkApp f aa' -- canonical or primitive
|
||||
Left d -> compt vv' $ mkApp d aa'
|
||||
_ -> mkApp f aa' -- literal
|
||||
look f = case f of
|
||||
EVar c -> Left $ lookDef pgf c
|
||||
_ -> Right f
|
||||
match = findMatch pgf
|
||||
|
||||
beta :: [CId] -> Expr -> Expr
|
||||
beta vv c = case c of
|
||||
EApp f a ->
|
||||
let (a',f') = (beta vv a, beta vv f) in
|
||||
case f' of
|
||||
EAbs x b -> beta vv $ subst vv [(x,a')] (beta (x:vv) b)
|
||||
_ -> (if a'==a && f'==f then id else beta vv) $ EApp f' a'
|
||||
EAbs x b -> EAbs x (beta (x:vv) b)
|
||||
_ -> c
|
||||
|
||||
|
||||
subst :: [CId] -> Subst -> Expr -> Expr
|
||||
subst xs g e = case e of
|
||||
EAbs x b -> EAbs x (subst (x:xs) g e) ---- TODO: refresh variables
|
||||
EApp f a -> EApp (substg f) (substg a)
|
||||
EVar x -> maybe e id $ lookup x g
|
||||
_ -> e
|
||||
where
|
||||
substg = subst xs g
|
||||
|
||||
type Subst = [(CId,Expr)]
|
||||
type Patt = Expr
|
||||
|
||||
|
||||
exprForm :: Expr -> ([CId],Expr,[Expr])
|
||||
exprForm exp = upd ([],exp,[]) where
|
||||
upd (xs,f,es) = case f of
|
||||
EAbs x b -> upd (x:xs,b,es)
|
||||
EApp c a -> upd (xs,c,a:es)
|
||||
_ -> (reverse xs,f,es)
|
||||
|
||||
mkAbs xs b = foldr EAbs b xs
|
||||
mkApp f es = foldl EApp f es
|
||||
|
||||
-- special version of pattern matching, to deal with comp under lambda
|
||||
|
||||
findMatch :: PGF -> [Equation] -> [Expr] -> Maybe (Expr, Subst)
|
||||
findMatch pgf cases terms = case cases of
|
||||
[] -> Nothing
|
||||
(Equ patts _):_ | length patts /= length terms -> Nothing
|
||||
(Equ patts val):cc -> case mapM tryMatch (zip patts terms) of
|
||||
Just substs -> return (val, concat substs)
|
||||
_ -> findMatch pgf cc terms
|
||||
where
|
||||
|
||||
tryMatch (p,t) = case (exprForm p, exprForm t) of
|
||||
(([],EVar c,[]),_) | constructor c -> if p==t then return [] else Nothing
|
||||
(([],EVar x,[]),_) | notMeta t -> return [(x,t)]
|
||||
(([],p, pp), ([], f, tt)) | p == f && length pp == length tt -> do
|
||||
matches <- mapM tryMatch (zip pp tt)
|
||||
return (concat matches)
|
||||
_ -> if p==t then return [] else Nothing
|
||||
|
||||
notMeta e = case e of
|
||||
EMeta _ -> False
|
||||
EApp f a -> notMeta f && notMeta a
|
||||
EAbs _ b -> notMeta b
|
||||
_ -> True
|
||||
|
||||
constructor = isData pgf
|
||||
|
||||
@@ -109,7 +109,6 @@ instance Binary Expr where
|
||||
put (ELit (LFlt d)) = putWord8 4 >> put d
|
||||
put (ELit (LInt i)) = putWord8 5 >> put i
|
||||
put (EMeta i) = putWord8 6 >> put i
|
||||
put (EEq eqs) = putWord8 7 >> put eqs
|
||||
get = do tag <- getWord8
|
||||
case tag of
|
||||
0 -> liftM2 EAbs get get
|
||||
@@ -119,9 +118,25 @@ instance Binary Expr where
|
||||
4 -> liftM (ELit . LFlt) get
|
||||
5 -> liftM (ELit . LInt) get
|
||||
6 -> liftM EMeta get
|
||||
7 -> liftM EEq get
|
||||
_ -> decodingError
|
||||
|
||||
|
||||
instance Binary Patt where
|
||||
put (PApp f ps) = putWord8 0 >> put (f,ps)
|
||||
put (PVar x) = putWord8 1 >> put x
|
||||
put PWild = putWord8 2
|
||||
put (PLit (LStr s)) = putWord8 3 >> put s
|
||||
put (PLit (LFlt d)) = putWord8 4 >> put d
|
||||
put (PLit (LInt i)) = putWord8 5 >> put i
|
||||
get = do tag <- getWord8
|
||||
case tag of
|
||||
0 -> liftM2 PApp get get
|
||||
1 -> liftM PVar get
|
||||
2 -> return PWild
|
||||
3 -> liftM (PLit . LStr) get
|
||||
4 -> liftM (PLit . LFlt) get
|
||||
5 -> liftM (PLit . LInt) get
|
||||
_ -> decodingError
|
||||
|
||||
instance Binary Equation where
|
||||
put (Equ ps e) = put (ps,e)
|
||||
get = liftM2 Equ get get
|
||||
|
||||
@@ -24,7 +24,7 @@ data PGF = PGF {
|
||||
|
||||
data Abstr = Abstr {
|
||||
aflags :: Map.Map CId String, -- value of a flag
|
||||
funs :: Map.Map CId (Type,Expr), -- type and def of a fun
|
||||
funs :: Map.Map CId (Type,[Equation]), -- type and def of a fun
|
||||
cats :: Map.Map CId [Hypo], -- context of a cat
|
||||
catfuns :: Map.Map CId [CId] -- funs to a cat (redundant, for fast lookup)
|
||||
}
|
||||
|
||||
151
src/PGF/Expr.hs
151
src/PGF/Expr.hs
@@ -1,13 +1,13 @@
|
||||
module PGF.Expr(Tree(..), Literal(..),
|
||||
readTree, showTree, pTree, ppTree,
|
||||
|
||||
Expr(..), Equation(..),
|
||||
readExpr, showExpr, pExpr, ppExpr,
|
||||
Expr(..), Patt(..), Equation(..),
|
||||
readExpr, showExpr, pExpr, ppExpr, ppPatt,
|
||||
|
||||
tree2expr, expr2tree,
|
||||
|
||||
-- needed in the typechecker
|
||||
Value(..), Env, eval, apply,
|
||||
Value(..), Env, eval, apply, eqValue,
|
||||
|
||||
-- helpers
|
||||
pStr,pFactor,
|
||||
@@ -17,6 +17,7 @@ module PGF.Expr(Tree(..), Literal(..),
|
||||
) where
|
||||
|
||||
import PGF.CId
|
||||
import PGF.Type
|
||||
|
||||
import Data.Char
|
||||
import Data.Maybe
|
||||
@@ -29,7 +30,7 @@ data Literal =
|
||||
LStr String -- ^ string constant
|
||||
| LInt Integer -- ^ integer constant
|
||||
| LFlt Double -- ^ floating point constant
|
||||
deriving (Eq,Ord,Show)
|
||||
deriving (Eq,Ord)
|
||||
|
||||
-- | The tree is an evaluated expression in the abstract syntax
|
||||
-- of the grammar. The type is especially restricted to not
|
||||
@@ -53,17 +54,24 @@ data Expr =
|
||||
| ELit Literal -- ^ literal
|
||||
| EMeta Int -- ^ meta variable
|
||||
| EVar CId -- ^ variable or function reference
|
||||
| EEq [Equation] -- ^ lambda function defined as a set of equations with pattern matching
|
||||
| EPi CId Expr Expr -- ^ dependent function type
|
||||
deriving (Eq,Ord)
|
||||
|
||||
-- | The pattern is used to define equations in the abstract syntax of the grammar.
|
||||
data Patt =
|
||||
PApp CId [Patt] -- ^ application. The identifier should be constructor i.e. defined with 'data'
|
||||
| PLit Literal -- ^ literal
|
||||
| PVar CId -- ^ variable
|
||||
| PWild -- ^ wildcard
|
||||
deriving (Eq,Ord)
|
||||
|
||||
-- | The equation is used to define lambda function as a sequence
|
||||
-- of equations with pattern matching. The list of 'Expr' represents
|
||||
-- the patterns and the second 'Expr' is the function body for this
|
||||
-- equation.
|
||||
data Equation =
|
||||
Equ [Expr] Expr
|
||||
deriving (Eq,Ord,Show)
|
||||
Equ [Patt] Expr
|
||||
deriving (Eq,Ord)
|
||||
|
||||
-- | parses 'String' as an expression
|
||||
readTree :: String -> Maybe Tree
|
||||
@@ -120,24 +128,13 @@ pTree isNested = RP.skipSpaces >> (pParen RP.<++ pAbs RP.<++ pApp RP.<++ fmap Li
|
||||
return (Meta n)
|
||||
|
||||
pExpr :: RP.ReadP Expr
|
||||
pExpr = RP.skipSpaces >> (pAbs RP.<++ pTerm RP.<++ pEqs)
|
||||
pExpr = RP.skipSpaces >> (pAbs RP.<++ pTerm)
|
||||
where
|
||||
pTerm = fmap (foldl1 EApp) (RP.sepBy1 pFactor RP.skipSpaces)
|
||||
|
||||
pAbs = do xs <- RP.between (RP.char '\\') (RP.skipSpaces >> RP.string "->") (RP.sepBy1 (RP.skipSpaces >> pCId) (RP.skipSpaces >> RP.char ','))
|
||||
e <- pExpr
|
||||
return (foldr EAbs e xs)
|
||||
|
||||
pEqs = fmap EEq $
|
||||
RP.between (RP.skipSpaces >> RP.char '{')
|
||||
(RP.skipSpaces >> RP.char '}')
|
||||
(RP.sepBy1 (RP.skipSpaces >> pEq)
|
||||
(RP.skipSpaces >> RP.string ";"))
|
||||
|
||||
pEq = do pats <- (RP.sepBy1 pExpr RP.skipSpaces)
|
||||
RP.skipSpaces >> RP.string "=>"
|
||||
e <- pExpr
|
||||
return (Equ pats e)
|
||||
|
||||
pFactor = fmap EVar pCId
|
||||
RP.<++ fmap ELit pLit
|
||||
@@ -176,6 +173,7 @@ ppTree d (Meta n) = PP.char '?' PP.<> PP.int n
|
||||
ppTree d (Var id) = PP.text (prCId id)
|
||||
|
||||
|
||||
ppExpr :: Int -> Expr -> PP.Doc
|
||||
ppExpr d (EAbs x e) = let (xs,e1) = getVars (EAbs x e)
|
||||
in ppParens (d > 0) (PP.char '\\' PP.<>
|
||||
PP.hsep (PP.punctuate PP.comma (map (PP.text . prCId) xs)) PP.<+>
|
||||
@@ -188,9 +186,11 @@ ppExpr d (EApp e1 e2) = ppParens (d > 1) ((ppExpr 1 e1) PP.<+> (ppExpr 2 e2))
|
||||
ppExpr d (ELit l) = ppLit l
|
||||
ppExpr d (EMeta n) = PP.char '?' PP.<+> PP.int n
|
||||
ppExpr d (EVar f) = PP.text (prCId f)
|
||||
ppExpr d (EEq eqs) = PP.braces (PP.sep (PP.punctuate PP.semi (map ppEquation eqs)))
|
||||
|
||||
ppEquation (Equ pats e) = PP.hsep (map (ppExpr 2) pats) PP.<+> PP.text "=>" PP.<+> ppExpr 0 e
|
||||
ppPatt d (PApp f ps) = ppParens (d > 1) (PP.text (prCId f) PP.<+> PP.hsep (map (ppPatt 2) ps))
|
||||
ppPatt d (PLit l) = ppLit l
|
||||
ppPatt d (PVar f) = PP.text (prCId f)
|
||||
ppPatt d PWild = PP.char '_'
|
||||
|
||||
ppLit (LStr s) = PP.text (show s)
|
||||
ppLit (LInt n) = PP.integer n
|
||||
@@ -212,46 +212,97 @@ tree2expr (Meta n) = EMeta n
|
||||
tree2expr (Abs xs t) = foldr EAbs (tree2expr t) xs
|
||||
tree2expr (Var x) = EVar x
|
||||
|
||||
-- | Converts an expression to tree. If the expression
|
||||
-- contains unevaluated applications they will be applied.
|
||||
expr2tree :: Expr -> Tree
|
||||
expr2tree e = value2tree (eval Map.empty e) [] []
|
||||
-- | Converts an expression to tree. The expression
|
||||
-- is first reduced to beta-eta-alfa normal form and
|
||||
-- after that converted to tree.
|
||||
expr2tree :: Funs -> Expr -> Tree
|
||||
expr2tree funs e = value2tree [] (eval funs Map.empty e)
|
||||
where
|
||||
value2tree (VApp v1 v2) xs ts = value2tree v1 xs (value2tree v2 [] []:ts)
|
||||
value2tree (VVar x) xs ts = ret xs (fun xs x ts)
|
||||
value2tree (VMeta n) xs [] = ret xs (Meta n)
|
||||
value2tree (VLit l) xs [] = ret xs (Lit l)
|
||||
value2tree (VClosure env (EAbs x e)) xs [] = value2tree (eval (Map.insert x (VVar x) env) e) (x:xs) []
|
||||
|
||||
fun xs x ts
|
||||
| x `elem` xs = Var x
|
||||
| otherwise = Fun x ts
|
||||
value2tree xs (VApp f vs) = case Map.lookup f funs of
|
||||
Just (DTyp hyps _ _,_) -> -- eta conversion
|
||||
let a1 = length hyps
|
||||
a2 = length vs
|
||||
a = a1 - a2
|
||||
i = length xs
|
||||
xs' = [var i | i <- [i..i+a-1]]
|
||||
in ret (reverse xs'++xs)
|
||||
(Fun f (map (value2tree []) vs++map Var xs'))
|
||||
Nothing -> error ("unknown variable "++prCId f)
|
||||
value2tree xs (VGen i) = ret xs (Var (var i))
|
||||
value2tree xs (VMeta n) = ret xs (Meta n)
|
||||
value2tree xs (VLit l) = ret xs (Lit l)
|
||||
value2tree xs (VClosure env (EAbs x e)) = let i = length xs
|
||||
in value2tree (var i:xs) (eval funs (Map.insert x (VGen i) env) e)
|
||||
|
||||
var i = mkCId ('v':show i)
|
||||
|
||||
ret [] t = t
|
||||
ret xs t = Abs (reverse xs) t
|
||||
|
||||
data Value
|
||||
= VGen Int
|
||||
| VApp Value Value
|
||||
| VVar CId
|
||||
| VMeta Int
|
||||
= VApp CId [Value]
|
||||
| VLit Literal
|
||||
| VMeta Int
|
||||
| VGen Int
|
||||
| VClosure Env Expr
|
||||
deriving (Show,Eq,Ord)
|
||||
deriving (Eq,Ord)
|
||||
|
||||
type Env = Map.Map CId Value
|
||||
type Funs = Map.Map CId (Type,[Equation]) -- type and def of a fun
|
||||
type Env = Map.Map CId Value
|
||||
|
||||
eval :: Env -> Expr -> Value
|
||||
eval env (EVar x) = fromMaybe (VVar x) (Map.lookup x env)
|
||||
eval env (EApp e1 e2) = apply (eval env e1) (eval env e2)
|
||||
eval env (EAbs x e) = VClosure env (EAbs x e)
|
||||
eval env (EMeta k) = VMeta k
|
||||
eval env (ELit l) = VLit l
|
||||
eval env e = VClosure env e
|
||||
eval :: Funs -> Env -> Expr -> Value
|
||||
eval funs env (EVar x) = case Map.lookup x env of
|
||||
Just v -> v
|
||||
Nothing -> case Map.lookup x funs of
|
||||
Just (_,eqs) -> case eqs of
|
||||
Equ [] e : _ -> eval funs env e
|
||||
[] -> VApp x []
|
||||
Nothing -> error ("unknown variable "++prCId x)
|
||||
eval funs env (EApp e1 e2) = apply funs env e1 [eval funs env e2]
|
||||
eval funs env (EAbs x e) = VClosure env (EAbs x e)
|
||||
eval funs env (EMeta k) = VMeta k
|
||||
eval funs env (ELit l) = VLit l
|
||||
|
||||
apply :: Value -> Value -> Value
|
||||
apply (VClosure env (EAbs x e)) v = eval (Map.insert x v env) e
|
||||
apply v0 v = VApp v0 v
|
||||
apply :: Funs -> Env -> Expr -> [Value] -> Value
|
||||
apply funs env e [] = eval funs env e
|
||||
apply funs env (EVar x) vs = case Map.lookup x env of
|
||||
Just v -> case (v,vs) of
|
||||
(VClosure env (EAbs x e),v:vs) -> apply funs (Map.insert x v env) e vs
|
||||
Nothing -> case Map.lookup x funs of
|
||||
Just (_,eqs) -> case match eqs vs of
|
||||
Just (e,vs,env) -> apply funs env e vs
|
||||
Nothing -> VApp x vs
|
||||
Nothing -> error ("unknown variable "++prCId x)
|
||||
apply funs env (EAbs x e) (v:vs) = apply funs (Map.insert x v env) e vs
|
||||
apply funs env (EApp e1 e2) vs = apply funs env e1 (eval funs env e2 : vs)
|
||||
|
||||
match :: [Equation] -> [Value] -> Maybe (Expr, [Value], Env)
|
||||
match eqs vs =
|
||||
case eqs of
|
||||
[] -> Nothing
|
||||
(Equ ps res):eqs -> let (as,vs') = splitAt (length ps) vs
|
||||
in case zipWithM tryMatch ps as of
|
||||
Just envs -> Just (res, vs', Map.unions envs)
|
||||
Nothing -> match eqs vs
|
||||
where
|
||||
tryMatch p v = case (p, v) of
|
||||
(PVar x, _ ) -> Just (Map.singleton x v)
|
||||
(PApp f ps, VApp fe vs) | f == fe -> do envs <- zipWithM tryMatch ps vs
|
||||
return (Map.unions envs)
|
||||
(PLit l, VLit le ) | l == le -> Just Map.empty
|
||||
_ -> Nothing
|
||||
|
||||
eqValue :: Int -> Value -> Value -> [(Value,Value)]
|
||||
eqValue k v1 v2 =
|
||||
case (v1,v2) of
|
||||
(VApp f1 vs1, VApp f2 vs2) | f1 == f2 -> concat (zipWith (eqValue k) vs1 vs2)
|
||||
(VLit l1, VLit l2 ) | l1 == l2 -> []
|
||||
(VMeta i, VMeta j ) | i == j -> []
|
||||
(VGen i, VGen j ) | i == j -> []
|
||||
(VClosure env1 (EAbs x1 e1), VClosure env2 (EAbs x2 e2)) ->
|
||||
let v = VGen k
|
||||
in eqValue (k+1) (VClosure (Map.insert x1 v env1) e1) (VClosure (Map.insert x2 v env2) e2)
|
||||
_ -> [(v1,v2)]
|
||||
|
||||
--- use composOp and state monad...
|
||||
newMetas :: Expr -> Expr
|
||||
|
||||
13
src/PGF/Expr.hs-boot
Normal file
13
src/PGF/Expr.hs-boot
Normal file
@@ -0,0 +1,13 @@
|
||||
module PGF.Expr where
|
||||
|
||||
import qualified Text.PrettyPrint as PP
|
||||
import qualified Text.ParserCombinators.ReadP as RP
|
||||
|
||||
data Expr
|
||||
|
||||
instance Eq Expr
|
||||
instance Ord Expr
|
||||
|
||||
pFactor :: RP.ReadP Expr
|
||||
|
||||
ppExpr :: Int -> Expr -> PP.Doc
|
||||
@@ -37,14 +37,15 @@ lookType :: PGF -> CId -> Type
|
||||
lookType pgf f =
|
||||
fst $ lookMap (error $ "lookType " ++ show f) f (funs (abstract pgf))
|
||||
|
||||
lookDef :: PGF -> CId -> Expr
|
||||
lookDef :: PGF -> CId -> [Equation]
|
||||
lookDef pgf f =
|
||||
snd $ lookMap (error $ "lookDef " ++ show f) f (funs (abstract pgf))
|
||||
|
||||
isData :: PGF -> CId -> Bool
|
||||
isData pgf f = case Map.lookup f (funs (abstract pgf)) of
|
||||
Just (_,EMeta 0) -> True ---- the encoding of data constrs
|
||||
_ -> False
|
||||
isData pgf f =
|
||||
case Map.lookup f (funs (abstract pgf)) of
|
||||
Just (_,[]) -> True -- the encoding of data constrs
|
||||
_ -> False
|
||||
|
||||
lookValCat :: PGF -> CId -> CId
|
||||
lookValCat pgf = valCat . lookType pgf
|
||||
@@ -120,9 +121,6 @@ contextLength :: Type -> Int
|
||||
contextLength ty = case ty of
|
||||
DTyp hyps _ _ -> length hyps
|
||||
|
||||
primNotion :: Expr
|
||||
primNotion = EEq []
|
||||
|
||||
term0 :: CId -> Term
|
||||
term0 = TM . prCId
|
||||
|
||||
|
||||
@@ -49,13 +49,8 @@ fromDef pgf t@(Fun f ts) = defDown t ++ defUp t where
|
||||
[(ps,p) | (p,d@(Fun g ps)) <- equs, g==f,
|
||||
isClosed d || (length equs == 1 && isLinear d)]
|
||||
|
||||
equss = [(f,[(Fun f (map expr2tree ps), expr2tree d) | (Equ ps d) <- eqs]) |
|
||||
(f,(_,d)) <- Map.assocs (funs (abstract pgf)), eqs <- defs d]
|
||||
|
||||
defs d = case d of
|
||||
EEq eqs -> [eqs]
|
||||
EMeta _ -> []
|
||||
_ -> [[Equ [] d]]
|
||||
equss = [(f,[(Fun f (map patt2tree ps), expr2tree (funs (abstract pgf)) d) | (Equ ps d) <- eqs]) |
|
||||
(f,(_,eqs)) <- Map.assocs (funs (abstract pgf)), not (null eqs)]
|
||||
|
||||
trequ s f e = True ----trace (s ++ ": " ++ show f ++ " " ++ show e) True
|
||||
|
||||
@@ -86,8 +81,6 @@ isLinear = nodup . vars where
|
||||
nodup = all ((<2) . length) . group . sort
|
||||
|
||||
|
||||
-- special version of AbsCompute.findMatch, working on Tree
|
||||
|
||||
match :: [([Tree],Tree)] -> [Tree] -> [(Tree, Subst)]
|
||||
match cases terms = case cases of
|
||||
[] -> []
|
||||
@@ -108,3 +101,9 @@ match cases terms = case cases of
|
||||
Fun f ts -> all notMeta ts
|
||||
_ -> True
|
||||
|
||||
-- | Converts a pattern to tree.
|
||||
patt2tree :: Patt -> Tree
|
||||
patt2tree (PApp f ps) = Fun f (map patt2tree ps)
|
||||
patt2tree (PLit l) = Lit l
|
||||
patt2tree (PVar x) = Var x
|
||||
patt2tree PWild = Meta 0
|
||||
|
||||
@@ -3,7 +3,7 @@ module PGF.Type ( Type(..), Hypo(..),
|
||||
pType, ppType, ppHypo ) where
|
||||
|
||||
import PGF.CId
|
||||
import PGF.Expr
|
||||
import {-# SOURCE #-} PGF.Expr
|
||||
import Data.Char
|
||||
import qualified Text.PrettyPrint as PP
|
||||
import qualified Text.ParserCombinators.ReadP as RP
|
||||
|
||||
@@ -17,7 +17,6 @@ module PGF.TypeCheck (
|
||||
import PGF.Data
|
||||
import PGF.Macros (lookDef,isData)
|
||||
import PGF.Expr
|
||||
import PGF.AbsCompute
|
||||
import PGF.CId
|
||||
|
||||
import GF.Data.ErrM
|
||||
@@ -29,7 +28,7 @@ import Debug.Trace
|
||||
|
||||
typecheck :: PGF -> Tree -> [Tree]
|
||||
typecheck pgf t = case inferExpr pgf (newMetas (tree2expr t)) of
|
||||
Ok t -> [expr2tree t]
|
||||
Ok t -> [expr2tree (funs (abstract pgf)) t]
|
||||
Bad s -> trace s []
|
||||
|
||||
inferExpr :: PGF -> Expr -> Err Expr
|
||||
@@ -50,26 +49,24 @@ infer pgf tenv@(k,rho,gamma) e = case e of
|
||||
-- K i -> return (AStr i, valAbsString, [])
|
||||
|
||||
EApp f t -> do
|
||||
(f',w,csf) <- infer pgf tenv f
|
||||
typ <- whnf w
|
||||
(f',typ,csf) <- infer pgf tenv f
|
||||
case typ of
|
||||
VClosure env (EPi x a b) -> do
|
||||
(a',csa) <- checkExp pgf tenv t (VClosure env a)
|
||||
b' <- whnf $ VClosure (eins x (VClosure rho t) env) b
|
||||
let b' = eval (funs (abstract pgf)) (eins x (VClosure rho t) env) b
|
||||
return $ (EApp f' a', b', csf ++ csa)
|
||||
_ -> Bad ("function type expected for function " ++ show f)
|
||||
_ -> Bad ("cannot infer type of expression" ++ show e)
|
||||
|
||||
|
||||
checkExp :: PGF -> TCEnv -> Expr -> Value -> Err (Expr, [(Value,Value)])
|
||||
checkExp pgf tenv@(k,rho,gamma) e ty = do
|
||||
typ <- whnf ty
|
||||
checkExp pgf tenv@(k,rho,gamma) e typ = do
|
||||
let v = VGen k
|
||||
case e of
|
||||
EMeta m -> return $ (e,[])
|
||||
EAbs x t -> case typ of
|
||||
VClosure env (EPi y a b) -> do
|
||||
a' <- whnf $ VClosure env a
|
||||
let a' = eval (funs (abstract pgf)) env a
|
||||
(t',cs) <- checkExp pgf (k+1,eins x v rho, eins x a' gamma) t
|
||||
(VClosure (eins y v env) b)
|
||||
return (EAbs x t', cs)
|
||||
@@ -79,7 +76,7 @@ checkExp pgf tenv@(k,rho,gamma) e ty = do
|
||||
checkInferExp :: PGF -> TCEnv -> Expr -> Value -> Err (Expr, [(Value,Value)])
|
||||
checkInferExp pgf tenv@(k,_,_) e typ = do
|
||||
(e',w,cs1) <- infer pgf tenv e
|
||||
cs2 <- eqValue k w typ
|
||||
let cs2 = eqValue k w typ
|
||||
return (e',cs1 ++ cs2)
|
||||
|
||||
lookupEVar :: PGF -> TCEnv -> CId -> Err Value
|
||||
@@ -100,40 +97,12 @@ eins = Map.insert
|
||||
emptyTCEnv :: TCEnv
|
||||
emptyTCEnv = (0,eempty,eempty)
|
||||
|
||||
whnf :: Value -> Err Value
|
||||
whnf v = case v of
|
||||
VApp u w -> do
|
||||
u' <- whnf u
|
||||
w' <- whnf w
|
||||
return $ apply u' w'
|
||||
VClosure env e -> return $ eval env e
|
||||
_ -> return v
|
||||
|
||||
eqValue :: Int -> Value -> Value -> Err [(Value,Value)]
|
||||
eqValue k u1 u2 = do
|
||||
w1 <- whnf u1
|
||||
w2 <- whnf u2
|
||||
let v = VGen k
|
||||
case (w1,w2) of
|
||||
(VApp f1 a1, VApp f2 a2) -> liftM2 (++) (eqValue k f1 f2) (eqValue k a1 a2)
|
||||
(VClosure env1 (EAbs x1 e1), VClosure env2 (EAbs x2 e2)) ->
|
||||
eqValue (k+1) (VClosure (eins x1 v env1) e1) (VClosure (eins x2 v env2) e2)
|
||||
(VClosure env1 (EPi x1 a1 b1), VClosure env2 (EPi x2 a2 b2)) ->
|
||||
liftM2 (++)
|
||||
(eqValue k (VClosure env1 a1) (VClosure env2 a2))
|
||||
(eqValue (k+1) (VClosure (eins x1 v env1) b1) (VClosure (eins x2 v env2) b2))
|
||||
(VGen i, VGen j) -> return [(w1,w2) | i /= j]
|
||||
(VVar i, VVar j) -> return [(w1,w2) | i /= j]
|
||||
_ -> return [(w1,w2) | w1 /= w2]
|
||||
-- invariant: constraints are in whnf
|
||||
|
||||
|
||||
-- this is not given in Expr
|
||||
prValue = showExpr . value2expr
|
||||
|
||||
value2expr v = case v of
|
||||
VApp v u -> EApp (value2expr v) (value2expr u)
|
||||
VVar x -> EVar x
|
||||
VApp f vs -> foldl EApp (EVar f) (map value2expr vs)
|
||||
VMeta i -> EMeta i
|
||||
VClosure g e -> e ----
|
||||
VLit l -> ELit l
|
||||
|
||||
Reference in New Issue
Block a user