1
0
forked from GitHub/gf-core

refactoring in GF.Grammar.Macros

This commit is contained in:
krasimir
2009-09-21 06:56:39 +00:00
parent 96786c1136
commit af831e01a7
11 changed files with 74 additions and 112 deletions

View File

@@ -163,7 +163,7 @@ checkCompleteGrammar gr abs cnc = do
_ -> False _ -> False
checkOne js i@(c,info) = case info of checkOne js i@(c,info) = case info of
AbsFun (Just ty) _ _ -> do let mb_def = do AbsFun (Just ty) _ _ -> do let mb_def = do
(cxt,(_,i),_) <- typeForm ty let (cxt,(_,i),_) = typeForm ty
info <- lookupIdent i js info <- lookupIdent i js
info <- case info of info <- case info of
(AnyInd _ m) -> do (m,info) <- lookupOrigInfo gr m i (AnyInd _ m) -> do (m,info) <- lookupOrigInfo gr m i
@@ -224,7 +224,7 @@ checkResInfo gr mo mm c info = do
--- this can only be a partial guarantee, since matching --- this can only be a partial guarantee, since matching
--- with value type is only possible if expected type is given --- with value type is only possible if expected type is given
checkUniq $ checkUniq $
sort [t : map (\(b,x,t) -> t) xs | (_,x) <- tysts1, Ok (xs,t) <- [typeFormCnc x]] sort [let (xs,t) = typeFormCnc x in t : map (\(b,x,t) -> t) xs | (_,x) <- tysts1]
return (ResOverload os [(y,x) | (x,y) <- tysts']) return (ResOverload os [(y,x) | (x,y) <- tysts'])
ResParam (Just (pcs,_)) -> chIn "parameter type" $ do ResParam (Just (pcs,_)) -> chIn "parameter type" $ do
@@ -255,7 +255,7 @@ checkCncInfo gr m mo (a,abs) c info = do
CncFun _ (Just trm) mpr -> chIn "linearization of" $ do CncFun _ (Just trm) mpr -> chIn "linearization of" $ do
typ <- checkErr $ lookupFunType gr a c typ <- checkErr $ lookupFunType gr a c
cat0 <- checkErr $ valCat typ let cat0 = valCat typ
(cont,val) <- linTypeOfType gr m typ -- creates arg vars (cont,val) <- linTypeOfType gr m typ -- creates arg vars
(trm',_) <- check trm (mkFunType (map (\(_,_,ty) -> ty) cont) val) -- erases arg vars (trm',_) <- check trm (mkFunType (map (\(_,_,ty) -> ty) cont) val) -- erases arg vars
checkPrintname gr mpr checkPrintname gr mpr
@@ -574,7 +574,7 @@ inferLType gr trm = case trm of
_ -> False _ -> False
inferPatt p = case p of inferPatt p = case p of
PP q c ps | q /= cPredef -> checkErr $ lookupResType gr q c >>= valTypeCnc PP q c ps | q /= cPredef -> checkErr $ liftM valTypeCnc (lookupResType gr q c)
PAs _ p -> inferPatt p PAs _ p -> inferPatt p
PNeg p -> inferPatt p PNeg p -> inferPatt p
PAlt p q -> checks [inferPatt p, inferPatt q] PAlt p q -> checks [inferPatt p, inferPatt q]
@@ -830,7 +830,7 @@ pattContext env typ p = case p of
PV x -> return [(Explicit,x,typ)] PV x -> return [(Explicit,x,typ)]
PP q c ps | q /= cPredef -> do ---- why this /=? AR 6/1/2006 PP q c ps | q /= cPredef -> do ---- why this /=? AR 6/1/2006
t <- checkErr $ lookupResType cnc q c t <- checkErr $ lookupResType cnc q c
(cont,v) <- checkErr $ typeFormCnc t let (cont,v) = typeFormCnc t
checkCond (text "wrong number of arguments for constructor in" <+> ppPatt Unqualified 0 p) checkCond (text "wrong number of arguments for constructor in" <+> ppPatt Unqualified 0 p)
(length cont == length ps) (length cont == length ps)
checkEqLType env typ v (patt2term p) checkEqLType env typ v (patt2term p)
@@ -998,7 +998,7 @@ ppType env ty =
-- | linearization types and defaults -- | linearization types and defaults
linTypeOfType :: SourceGrammar -> Ident -> Type -> Check (Context,Type) linTypeOfType :: SourceGrammar -> Ident -> Type -> Check (Context,Type)
linTypeOfType cnc m typ = do linTypeOfType cnc m typ = do
(cont,cat) <- checkErr $ typeSkeleton typ let (cont,cat) = typeSkeleton typ
val <- lookLin cat val <- lookLin cat
args <- mapM mkLinArg (zip [0..] cont) args <- mapM mkLinArg (zip [0..] cont)
return (args, val) return (args, val)

View File

@@ -126,8 +126,8 @@ b2b A.Implicit = C.Implicit
mkType :: [Ident] -> A.Type -> C.Type mkType :: [Ident] -> A.Type -> C.Type
mkType scope t = mkType scope t =
case GM.typeForm t of case GM.typeForm t of
Ok (hyps,(_,cat),args) -> let (scope',hyps') = mkContext scope hyps (hyps,(_,cat),args) -> let (scope',hyps') = mkContext scope hyps
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 = case GM.termForm t of

View File

@@ -127,7 +127,7 @@ evalCncInfo opts gr cnc abs (c,info) = do
return (CncCat ptyp pde' ppr') return (CncCat ptyp pde' ppr')
CncFun (mt@(Just (_,ty@(cont,val)))) pde ppr -> --trace (prt c) $ CncFun (mt@(Just (_,ty@(cont,val)))) pde ppr -> --trace (prt c) $
eIn (text "linearization in type" <+> ppTerm Unqualified 0 (mkProd (cont,val,[])) $$ text "of function") $ do eIn (text "linearization in type" <+> ppTerm Unqualified 0 (mkProd cont val []) $$ text "of function") $ do
pde' <- case pde of pde' <- case pde of
Just de -> liftM Just $ pEval ty de Just de -> liftM Just $ pEval ty de
Nothing -> return pde Nothing -> return pde

View File

@@ -239,7 +239,7 @@ checkBranch th tenv b@(ps,t) ty = errIn ("branch" +++ show b) $
PString s -> (K s : ps, i, g, k) PString s -> (K s : ps, i, g, k)
PInt n -> (EInt n : ps, i, g, k) PInt n -> (EInt n : ps, i, g, k)
PFloat n -> (EFloat n : ps, i, g, k) PFloat n -> (EFloat n : ps, i, g, k)
PP m c xs -> (mkApp (qq (m,c)) xss : ps, j, g',k') PP m c xs -> (mkApp (Q m c) xss : ps, j, g',k')
where (xss,j,g',k') = foldr p2t ([],i,g,k) xs where (xss,j,g',k') = foldr p2t ([],i,g,k) xs
_ -> error $ render (text "undefined p2t case" <+> ppPatt Unqualified 0 p <+> text "in checkBranch") _ -> error $ render (text "undefined p2t case" <+> ppPatt Unqualified 0 p <+> text "in checkBranch")

View File

@@ -42,7 +42,7 @@ type2val :: Type -> Val
type2val = VClos [] type2val = VClos []
cont2exp :: Context -> Exp cont2exp :: Context -> Exp
cont2exp c = mkProd (c, eType, []) -- to check a context cont2exp c = mkProd c eType [] -- to check a context
cont2val :: Context -> Val cont2val :: Context -> Val
cont2val = type2val . cont2exp cont2val = type2val . cont2exp

View File

@@ -50,11 +50,11 @@ typPredefined f
| f == cPlus = return $ mkFunType [typeInt,typeInt] (typeInt) | f == cPlus = return $ mkFunType [typeInt,typeInt] (typeInt)
---- "read" -> (P : Type) -> Tok -> P ---- "read" -> (P : Type) -> Tok -> P
| f == cShow = return $ mkProd -- (P : PType) -> P -> Tok | f == cShow = return $ mkProd -- (P : PType) -> P -> Tok
([(Explicit,varP,typePType),(Explicit,identW,Vr varP)],typeStr,[]) [(Explicit,varP,typePType),(Explicit,identW,Vr varP)] typeStr []
| f == cToStr = return $ mkProd -- (L : Type) -> L -> Str | f == cToStr = return $ mkProd -- (L : Type) -> L -> Str
([(Explicit,varL,typeType),(Explicit,identW,Vr varL)],typeStr,[]) [(Explicit,varL,typeType),(Explicit,identW,Vr varL)] typeStr []
| f == cMapStr = return $ mkProd -- (L : Type) -> (Str -> Str) -> L -> L | f == cMapStr = return $ mkProd -- (L : Type) -> (Str -> Str) -> L -> L
([(Explicit,varL,typeType),(Explicit,identW,mkFunType [typeStr] typeStr),(Explicit,identW,Vr varL)],Vr varL,[]) [(Explicit,varL,typeType),(Explicit,identW,mkFunType [typeStr] typeStr),(Explicit,identW,Vr varL)] (Vr varL) []
| f == cTake = return $ mkFunType [typeInt,typeTok] typeTok | f == cTake = return $ mkFunType [typeInt,typeTok] typeTok
| f == cTk = return $ mkFunType [typeInt,typeTok] typeTok | f == cTk = return $ mkFunType [typeInt,typeTok] typeTok
| otherwise = Bad (render (text "unknown in Predef:" <+> ppIdent f)) | otherwise = Bad (render (text "unknown in Predef:" <+> ppIdent f))

View File

@@ -110,7 +110,7 @@ cf2cat (_,(cat, items)) = map identS $ cat : [c | Left c <- items]
cf2rule :: CFRule -> ((Ident,Info),(Ident,Info)) cf2rule :: CFRule -> ((Ident,Info),(Ident,Info))
cf2rule (fun, (cat, items)) = (def,ldef) where cf2rule (fun, (cat, items)) = (def,ldef) where
f = identS fun f = identS fun
def = (f, AbsFun (Just (mkProd (args', Cn (identS cat), []))) Nothing Nothing) def = (f, AbsFun (Just (mkProd args' (Cn (identS cat)) [])) Nothing Nothing)
args0 = zip (map (identS . ("x" ++) . show) [0..]) items args0 = zip (map (identS . ("x" ++) . show) [0..]) items
args = [((Explicit,v), Cn (identS c)) | (v, Left c) <- args0] args = [((Explicit,v), Cn (identS c)) | (v, Left c) <- args0]
args' = [(Explicit,identS "_", Cn (identS c)) | (_, Left c) <- args0] args' = [(Explicit,identS "_", Cn (identS c)) | (_, Left c) <- args0]

View File

@@ -111,7 +111,7 @@ lookupResType gr m c = do
CncCat _ _ _ -> return typeType CncCat _ _ _ -> return typeType
CncFun (Just (cat,(cont@(_:_),val))) _ _ -> do CncFun (Just (cat,(cont@(_:_),val))) _ _ -> do
val' <- lock cat val val' <- lock cat val
return $ mkProd (cont, val', []) return $ mkProd cont val' []
CncFun _ _ _ -> lookFunType m m c CncFun _ _ _ -> lookFunType m m c
AnyInd _ n -> lookupResType gr n c AnyInd _ n -> lookupResType gr n c
ResParam _ -> return $ typePType ResParam _ -> return $ typePType
@@ -137,8 +137,8 @@ lookupOverload gr m c = do
case info of case info of
ResOverload os tysts -> do ResOverload os tysts -> do
tss <- mapM (\x -> lookupOverload gr x c) os tss <- mapM (\x -> lookupOverload gr x c) os
return $ [(map (\(b,x,t) -> t) args,(val,tr)) | return $ [let (args,val) = typeFormCnc ty in (map (\(b,x,t) -> t) args,(val,tr)) |
(ty,tr) <- tysts, Ok (args,val) <- [typeFormCnc ty]] ++ (ty,tr) <- tysts] ++
concat tss concat tss
AnyInd _ n -> lookupOverload gr n c AnyInd _ n -> lookupOverload gr n c
@@ -279,14 +279,12 @@ opersForType gr orig val =
opers i m val = opers i m val =
[(f,ty) | [(f,ty) |
(f,ResOper (Just ty) _) <- tree2list $ jments m, (f,ResOper (Just ty) _) <- tree2list $ jments m,
Ok valt <- [valTypeCnc ty], elem (valTypeCnc ty) [val,orig]
elem valt [val,orig]
] ++ ] ++
let cat = err error snd (valCat orig) in --- ignore module let cat = snd (valCat orig) in --- ignore module
[(f,ty) | [(f,ty) |
Ok a <- [abstractOfConcrete gr i >>= lookupModule gr], Ok a <- [abstractOfConcrete gr i >>= lookupModule gr],
(f, AbsFun (Just ty0) _ _) <- tree2list $ jments a, (f, AbsFun (Just ty0) _ _) <- tree2list $ jments a,
let ty = redirectTerm i ty0, let ty = redirectTerm i ty0,
Ok valt <- [valCat ty], cat == snd (valCat ty) ---
cat == snd valt ---
] ]

View File

@@ -134,10 +134,10 @@ getMetaAtom a = case a of
_ -> Bad "the active node is not meta" _ -> Bad "the active node is not meta"
-} -}
cat2val :: Context -> Cat -> Val cat2val :: Context -> Cat -> Val
cat2val cont cat = vClos $ mkApp (qq cat) [Meta i | i <- [1..length cont]] cat2val cont cat = vClos $ mkApp (uncurry Q cat) [Meta i | i <- [1..length cont]]
val2cat :: Val -> Err Cat val2cat :: Val -> Err Cat
val2cat v = val2exp v >>= valCat val2cat v = liftM valCat (val2exp v)
substTerm :: [Ident] -> Substitution -> Term -> Term substTerm :: [Ident] -> Substitution -> Term -> Term
substTerm ss g c = case c of substTerm ss g c = case c of
@@ -183,7 +183,7 @@ val2expP safe v = case v of
else substVal g e else substVal g e
VClos g e -> substVal g e VClos g e -> substVal g e
VApp f c -> liftM2 App (val2expP safe f) (val2expP safe c) VApp f c -> liftM2 App (val2expP safe f) (val2expP safe c)
VCn c -> return $ qq c VCn c -> return $ uncurry Q c
VGen i x -> if safe VGen i x -> if safe
then Bad (render (text "unsafe val2exp" <+> ppValue Unqualified 0 v)) then Bad (render (text "unsafe val2exp" <+> ppValue Unqualified 0 v))
else return $ Vr $ x --- in editing, no alpha conversions presentv else return $ Vr $ x --- in editing, no alpha conversions presentv
@@ -214,9 +214,6 @@ freeVarsExp e = case e of
Prod _ x a b -> freeVarsExp a ++ filter (/=x) (freeVarsExp b) Prod _ x a b -> freeVarsExp a ++ filter (/=x) (freeVarsExp b)
_ -> [] --- thus applies to abstract syntax only _ -> [] --- thus applies to abstract syntax only
mkJustProd :: Context -> Term -> Term
mkJustProd cont typ = mkProd (cont,typ,[])
int2var :: Int -> Ident int2var :: Int -> Ident
int2var = identC . BS.pack . ('$':) . show int2var = identC . BS.pack . ('$':) . show

View File

@@ -31,89 +31,56 @@ import Data.Char (isDigit)
import Data.List (sortBy) import Data.List (sortBy)
import Text.PrettyPrint import Text.PrettyPrint
firstTypeForm :: Type -> Err (Context, Type) typeForm :: Type -> (Context, Cat, [Term])
firstTypeForm t = case t of typeForm t =
Prod b x a t -> do case t of
(x', val) <- firstTypeForm t Prod b x a t ->
return ((b,x,a):x',val) let (x', cat, args) = typeForm t
_ -> return ([],t) in ((b,x,a):x', cat, args)
App c a ->
let (_, cat, args) = typeForm c
in ([],cat,args ++ [a])
Q m c -> ([],(m,c),[])
QC m c -> ([],(m,c),[])
Sort c -> ([],(identW, c),[])
_ -> error (render (text "no normal form of type" <+> ppTerm Unqualified 0 t))
qTypeForm :: Type -> Err (Context, Cat, [Term]) typeFormCnc :: Type -> (Context, Type)
qTypeForm t = case t of typeFormCnc t =
Prod b x a t -> do case t of
(x', cat, args) <- qTypeForm t Prod b x a t -> let (x', v) = typeFormCnc t
return ((b,x,a):x', cat, args) in ((b,x,a):x',v)
App c a -> do _ -> ([],t)
(_,cat, args) <- qTypeForm c
return ([],cat,args ++ [a])
Q m c ->
return ([],(m,c),[])
QC m c ->
return ([],(m,c),[])
_ ->
Bad (render (text "no normal form of type" <+> ppTerm Unqualified 0 t))
qq :: QIdent -> Term valCat :: Type -> Cat
qq (m,c) = Q m c
typeForm :: Type -> Err (Context, Cat, [Term])
typeForm = qTypeForm ---- no need to distinguish any more
typeFormCnc :: Type -> Err (Context, Type)
typeFormCnc t = case t of
Prod b x a t -> do
(x', v) <- typeFormCnc t
return ((b,x,a):x',v)
_ -> return ([],t)
valCat :: Type -> Err Cat
valCat typ = valCat typ =
do (_,cat,_) <- typeForm typ let (_,cat,_) = typeForm typ
return cat in cat
valType :: Type -> Err Type valType :: Type -> Type
valType typ = valType typ =
do (_,cat,xx) <- typeForm typ --- not optimal to do in this way let (_,cat,xx) = typeForm typ --- not optimal to do in this way
return $ mkApp (qq cat) xx in mkApp (uncurry Q cat) xx
valTypeCnc :: Type -> Err Type valTypeCnc :: Type -> Type
valTypeCnc typ = valTypeCnc typ = snd (typeFormCnc typ)
do (_,ty) <- typeFormCnc typ
return ty
typeRawSkeleton :: Type -> Err ([(Int,Type)],Type) typeSkeleton :: Type -> ([(Int,Cat)],Cat)
typeRawSkeleton typ = typeSkeleton typ =
do (cont,typ) <- typeFormCnc typ let (cont,cat,_) = typeForm typ
args <- mapM (\(b,x,t) -> typeRawSkeleton t) cont args = map (\(b,x,t) -> typeSkeleton t) cont
return ([(length c, v) | (c,v) <- args], typ) in ([(length c, v) | (c,v) <- args], cat)
type MCat = (Ident,Ident) catSkeleton :: Type -> ([Cat],Cat)
getMCat :: Term -> Err MCat
getMCat t = case t of
Q m c -> return (m,c)
QC m c -> return (m,c)
Sort c -> return (identW, c)
App f _ -> getMCat f
_ -> Bad (render (text "no qualified constant" <+> ppTerm Unqualified 0 t))
typeSkeleton :: Type -> Err ([(Int,MCat)],MCat)
typeSkeleton typ = do
(cont,val) <- typeRawSkeleton typ
cont' <- mapPairsM getMCat cont
val' <- getMCat val
return (cont',val')
catSkeleton :: Type -> Err ([MCat],MCat)
catSkeleton typ = catSkeleton typ =
do (args,val) <- typeSkeleton typ let (args,val) = typeSkeleton typ
return (map snd args, val) in (map snd args, val)
funsToAndFrom :: Type -> (MCat, [(MCat,[Int])]) funsToAndFrom :: Type -> (Cat, [(Cat,[Int])])
funsToAndFrom t = errVal undefined $ do --- funsToAndFrom t =
(cs,v) <- catSkeleton t let (cs,v) = catSkeleton t
let cis = zip cs [0..] cis = zip cs [0..]
return $ (v, [(c,[i | (c',i) <- cis, c' == c]) | c <- cs]) in (v, [(c,[i | (c',i) <- cis, c' == c]) | c <- cs])
typeFormConcrete :: Type -> Err (Context, Type) typeFormConcrete :: Type -> Err (Context, Type)
typeFormConcrete t = case t of typeFormConcrete t = case t of
@@ -123,9 +90,9 @@ typeFormConcrete t = case t of
_ -> return ([],t) _ -> return ([],t)
isRecursiveType :: Type -> Bool isRecursiveType :: Type -> Bool
isRecursiveType t = errVal False $ do isRecursiveType t =
(cc,c) <- catSkeleton t -- thus recursivity on Cat level let (cc,c) = catSkeleton t -- thus recursivity on Cat level
return $ any (== c) cc in any (== c) cc
isHigherOrderType :: Type -> Bool isHigherOrderType :: Type -> Bool
isHigherOrderType t = errVal True $ do -- pessimistic choice isHigherOrderType t = errVal True $ do -- pessimistic choice
@@ -159,11 +126,11 @@ appForm t = case t of
_ -> (t,[]) _ -> (t,[])
mkProdSimple :: Context -> Term -> Term mkProdSimple :: Context -> Term -> Term
mkProdSimple c t = mkProd (c,t,[]) mkProdSimple c t = mkProd c t []
mkProd :: (Context, Term, [Term]) -> Term mkProd :: Context -> Term -> [Term] -> Term
mkProd ([], typ, args) = mkApp typ args mkProd [] typ args = mkApp typ args
mkProd ((b,x,a):dd, typ, args) = Prod b x a (mkProd (dd, typ, args)) mkProd ((b,x,a):dd) typ args = Prod b x a (mkProd dd typ args)
mkTerm :: ([(BindType,Ident)], Term, [Term]) -> Term mkTerm :: ([(BindType,Ident)], Term, [Term]) -> Term
mkTerm (xx,t,aa) = mkAbs xx (mkApp t aa) mkTerm (xx,t,aa) = mkAbs xx (mkApp t aa)
@@ -293,7 +260,7 @@ mkWildCases :: Term -> Term
mkWildCases = mkCases identW mkWildCases = mkCases identW
mkFunType :: [Type] -> Type -> Type mkFunType :: [Type] -> Type -> Type
mkFunType tt t = mkProd ([(Explicit,identW, ty) | ty <- tt], t, []) -- nondep prod mkFunType tt t = mkProd [(Explicit,identW, ty) | ty <- tt] t [] -- nondep prod
plusRecType :: Type -> Type -> Err Type plusRecType :: Type -> Type -> Err Type
plusRecType t1 t2 = case (t1, t2) of plusRecType t1 t2 = case (t1, t2) of

View File

@@ -249,7 +249,7 @@ DataDef :: { [(Ident,SrcSpan,Info)] }
DataDef DataDef
: Posn Ident '=' ListDataConstr Posn { ($2, ($1,$5), AbsCat Nothing (Just (map Cn $4))) : : Posn Ident '=' ListDataConstr Posn { ($2, ($1,$5), AbsCat Nothing (Just (map Cn $4))) :
[(fun, ($1,$5), AbsFun Nothing Nothing Nothing) | fun <- $4] } [(fun, ($1,$5), AbsFun Nothing Nothing Nothing) | fun <- $4] }
| Posn ListIdent ':' Exp Posn { [(cat, ($1,$5), AbsCat Nothing (Just (map Cn $2))) | Ok (_,cat) <- [valCat $4]] ++ | Posn ListIdent ':' Exp Posn { -- (snd (valCat $4), ($1,$5), AbsCat Nothing (Just (map Cn $2))) :
[(fun, ($1,$5), AbsFun (Just $4) Nothing Nothing) | fun <- $2] } [(fun, ($1,$5), AbsFun (Just $4) Nothing Nothing) | fun <- $2] }
ParamDef :: { [(Ident,SrcSpan,Info)] } ParamDef :: { [(Ident,SrcSpan,Info)] }