forked from GitHub/gf-core
bugfix in GrammarToPGF related to the compilation of def rules
This commit is contained in:
@@ -121,21 +121,20 @@ mkType scope t =
|
|||||||
in C.DTyp hyps' (i2i cat) (map (mkExp scope') args)
|
in C.DTyp hyps' (i2i cat) (map (mkExp scope') args)
|
||||||
|
|
||||||
mkExp :: [Ident] -> A.Term -> C.Expr
|
mkExp :: [Ident] -> A.Term -> C.Expr
|
||||||
mkExp scope t = case GM.termForm t of
|
mkExp scope t =
|
||||||
Ok (xs,c,args) -> mkAbs xs (mkApp (map snd (reverse xs)++scope) c (map (mkExp scope) args))
|
case t of
|
||||||
where
|
Q _ c -> C.EFun (i2i c)
|
||||||
mkAbs xs t = foldr (\(b,v) -> C.EAbs (b2b b) (i2i v)) t xs
|
QC _ c -> C.EFun (i2i c)
|
||||||
mkApp scope c args = case c of
|
Vr x -> case lookup x (zip scope [0..]) of
|
||||||
Q _ c -> foldl C.EApp (C.EFun (i2i c)) args
|
Just i -> C.EVar i
|
||||||
QC _ c -> foldl C.EApp (C.EFun (i2i c)) args
|
Nothing -> C.EMeta 0
|
||||||
Vr x -> case lookup x (zip scope [0..]) of
|
Abs b x t-> C.EAbs (b2b b) (i2i x) (mkExp (x:scope) t)
|
||||||
Just i -> foldl C.EApp (C.EVar i) args
|
App t1 t2-> C.EApp (mkExp scope t1) (mkExp scope t2)
|
||||||
Nothing -> foldl C.EApp (C.EMeta 0) args
|
EInt i -> C.ELit (C.LInt (fromIntegral i))
|
||||||
EInt i -> C.ELit (C.LInt (fromIntegral i))
|
EFloat f -> C.ELit (C.LFlt f)
|
||||||
EFloat f -> C.ELit (C.LFlt f)
|
K s -> C.ELit (C.LStr s)
|
||||||
K s -> C.ELit (C.LStr s)
|
Meta i -> C.EMeta i
|
||||||
Meta i -> C.EMeta i
|
_ -> C.EMeta 0
|
||||||
_ -> C.EMeta 0
|
|
||||||
|
|
||||||
mkPatt scope p =
|
mkPatt scope p =
|
||||||
case p of
|
case p of
|
||||||
|
|||||||
Reference in New Issue
Block a user