msyds/gf-core
1
0
Fork 0
forked from GitHub/gf-core
Code Pull Requests Activity

operations in the abstract syntax

Browse Source
This commit is contained in:
krasimir
2010-11-12 19:37:19 +00:00
parent 75323ff56c
commit fe1205059b
16 changed files with 96 additions and 62 deletions
Download Patch File Download Diff File Expand all files Collapse all files

8
examples/nqueens/Nat.gf
View File

@@ -11,8 +11,8 @@ data zNE : (i,j : Nat) -> NE i j -> NE (succ i) (succ j) ;
lNE : (j : Nat) -> NE zero (succ j) ;
rNE : (j : Nat) -> NE (succ j) zero ;
fun plus : Nat -> Nat -> Nat ;
def plus zero n = n ;
plus (succ m) n = succ (plus m n) ;
oper plus : Nat -> Nat -> Nat ;
def plus zero n = n ;
plus (succ m) n = succ (plus m n) ;
}
}

8
src/compiler/GF/Compile/CheckGrammar.hs
View File

@@ -94,7 +94,7 @@ checkCompleteGrammar gr (am,abs) (cm,cnc) = do
where
checkAbs js i@(c,info) =
case info of
AbsFun (Just (L loc ty)) _ _
AbsFun (Just (L loc ty)) _ _ _
-> do let mb_def = do
let (cxt,(_,i),_) = typeForm ty
info <- lookupIdent i js
@@ -138,7 +138,7 @@ checkCompleteGrammar gr (am,abs) (cm,cnc) = do
checkCnc js i@(c,info) =
case info of
CncFun _ d pn -> case lookupOrigInfo gr (am,c) of
Ok (_,AbsFun (Just (L _ ty)) _ _) ->
Ok (_,AbsFun (Just (L _ ty)) _ _ _) ->
do (cont,val) <- linTypeOfType gr cm ty
let linty = (snd (valCat ty),cont,val)
return $ updateTree (c,CncFun (Just linty) d pn) js
@@ -161,7 +161,7 @@ checkInfo ms (m,mo) c info = do
mkCheck loc "category" $
checkContext gr cont
AbsFun (Just (L loc typ0)) ma md -> do
AbsFun (Just (L loc typ0)) ma md moper -> do
typ <- compAbsTyp [] typ0 -- to calculate let definitions
mkCheck loc "type of function" $
checkTyp gr typ
@@ -169,7 +169,7 @@ checkInfo ms (m,mo) c info = do
Just eqs -> mapM_ (\(L loc eq) -> mkCheck loc "definition of function" $
checkDef gr (m,c) typ eq) eqs
Nothing -> return ()
return (AbsFun (Just (L loc typ)) ma md)
return (AbsFun (Just (L loc typ)) ma md moper)
CncFun linty@(Just (cat,cont,val)) (Just (L loc trm)) mpr -> chIn loc "linearization of" $ do
(trm',_) <- checkLType gr [] trm (mkFunType (map (\(_,_,ty) -> ty) cont) val) -- erases arg vars

4
src/compiler/GF/Compile/GrammarToPGF.hs
View File

@@ -58,14 +58,14 @@ canon2pgf opts gr cgr@(M.MGrammar (am:cms)) = do
flags = Map.fromList [(mkCId f,C.LStr x) | (f,x) <- optionsPGF (M.flags abm)]
funs = Map.fromAscList [(i2i f, (mkType [] ty, mkArrity ma, mkDef pty, 0)) |
(f,AbsFun (Just (L _ ty)) ma pty) <- Map.toAscList (M.jments abm)]
(f,AbsFun (Just (L _ ty)) ma pty _) <- Map.toAscList (M.jments abm)]
cats = Map.fromAscList [(i2i c, (snd (mkContext [] cont),catfuns c)) |
(c,AbsCat (Just (L _ cont))) <- Map.toAscList (M.jments abm)]
catfuns cat =
(map (\x -> (0,snd x)) . sortBy (compare `on` fst))
[(loc,i2i f) | (f,AbsFun (Just (L loc ty)) _ _) <- tree2list (M.jments abm), snd (GM.valCat ty) == cat]
[(loc,i2i f) | (f,AbsFun (Just (L loc ty)) _ _ (Just True)) <- tree2list (M.jments abm), snd (GM.valCat ty) == cat]
mkConcr am cm@(lang,mo) = do
cnc <- convertConcrete opts gr am cm

4
src/compiler/GF/Compile/Rename.hs
View File

@@ -105,7 +105,7 @@ renameIdentTerm env@(act,imps) t =
info2status :: Maybe Ident -> (Ident,Info) -> StatusInfo
info2status mq (c,i) = case i of
AbsFun _ _ Nothing -> maybe Con (curry QC) mq
AbsFun _ _ Nothing _ -> maybe Con (curry QC) mq
ResValue _ -> maybe Con (curry QC) mq
ResParam _ _ -> maybe Con (curry QC) mq
AnyInd True m -> maybe Con (const (curry QC m)) mq
@@ -141,7 +141,7 @@ renameInfo :: Status -> Ident -> Ident -> Info -> Check Info
renameInfo status m i info =
case info of
AbsCat pco -> liftM AbsCat (renPerh (renameContext status) pco)
AbsFun pty pa ptr -> liftM3 AbsFun (renTerm pty) (return pa) (renMaybe (mapM (renLoc (renEquation status))) ptr)
AbsFun pty pa ptr poper -> liftM4 AbsFun (renTerm pty) (return pa) (renMaybe (mapM (renLoc (renEquation status))) ptr) (return poper)
ResOper pty ptr -> liftM2 ResOper (renTerm pty) (renTerm ptr)
ResOverload os tysts -> liftM (ResOverload os) (mapM (renPair (renameTerm status [])) tysts)
ResParam (Just pp) m -> do

6
src/compiler/GF/Compile/Update.hs
View File

@@ -161,7 +161,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 _ _ Nothing -> (True,n)
AbsFun _ _ Nothing _ -> (True,n)
AnyInd b k -> (b,k)
_ -> (False,n) ---- canonical in Abs
@@ -169,8 +169,8 @@ unifyAnyInfo :: Ident -> Info -> Info -> Err Info
unifyAnyInfo m i j = case (i,j) of
(AbsCat mc1, AbsCat mc2) ->
liftM AbsCat (unifMaybeL mc1 mc2)
(AbsFun mt1 ma1 md1, AbsFun mt2 ma2 md2) ->
liftM3 AbsFun (unifMaybeL mt1 mt2) (unifAbsArrity ma1 ma2) (unifAbsDefs md1 md2) -- adding defs
(AbsFun mt1 ma1 md1 moper1, AbsFun mt2 ma2 md2 moper2) ->
liftM4 AbsFun (unifMaybeL mt1 mt2) (unifAbsArrity ma1 ma2) (unifAbsDefs md1 md2) (unifMaybe moper1 moper2) -- adding defs
(ResParam mt1 mv1, ResParam mt2 mv2) ->
liftM2 ResParam (unifMaybe mt1 mt2) (unifMaybe mv1 mv2)

20
src/compiler/GF/Grammar/Binary.hs
View File

@@ -88,7 +88,7 @@ instance Binary Options where
instance Binary Info where
put (AbsCat x) = putWord8 0 >> put x
put (AbsFun x y z) = putWord8 1 >> put (x,y,z)
put (AbsFun w x y z) = putWord8 1 >> put (w,x,y,z)
put (ResParam x y) = putWord8 2 >> put (x,y)
put (ResValue x) = putWord8 3 >> put x
put (ResOper x y) = putWord8 4 >> put (x,y)
@@ -98,15 +98,15 @@ instance Binary Info where
put (AnyInd x y) = putWord8 8 >> put (x,y)
get = do tag <- getWord8
case tag of
0 -> get >>= \x -> return (AbsCat x)
1 -> get >>= \(x,y,z) -> return (AbsFun x y z)
2 -> get >>= \(x,y) -> return (ResParam x y)
3 -> get >>= \x -> return (ResValue x)
4 -> get >>= \(x,y) -> return (ResOper x y)
5 -> get >>= \(x,y) -> return (ResOverload x y)
6 -> get >>= \(x,y,z) -> return (CncCat x y z)
7 -> get >>= \(x,y,z) -> return (CncFun x y z)
8 -> get >>= \(x,y) -> return (AnyInd x y)
0 -> get >>= \x -> return (AbsCat x)
1 -> get >>= \(w,x,y,z) -> return (AbsFun w x y z)
2 -> get >>= \(x,y) -> return (ResParam x y)
3 -> get >>= \x -> return (ResValue x)
4 -> get >>= \(x,y) -> return (ResOper x y)
5 -> get >>= \(x,y) -> return (ResOverload x y)
6 -> get >>= \(x,y,z) -> return (CncCat x y z)
7 -> get >>= \(x,y,z) -> return (CncFun x y z)
8 -> get >>= \(x,y) -> return (AnyInd x y)
_ -> decodingError
instance Binary a => Binary (L a) where

2
src/compiler/GF/Grammar/CF.hs
View File

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

4
src/compiler/GF/Grammar/Grammar.hs
View File

@@ -76,8 +76,8 @@ mapSourceModule f (i,mi) = (i, f mi)
-- and indirection to module (/INDIR/)
data Info =
-- judgements in abstract syntax
AbsCat (Maybe (L Context)) -- ^ (/ABS/) context of a category
| AbsFun (Maybe (L Type)) (Maybe Int) (Maybe [L Equation]) -- ^ (/ABS/) type, arrity and definition of a function
AbsCat (Maybe (L Context)) -- ^ (/ABS/) context of a category
| AbsFun (Maybe (L Type)) (Maybe Int) (Maybe [L Equation]) (Maybe Bool) -- ^ (/ABS/) type, arrity and definition of a function
-- judgements in resource
| ResParam (Maybe [L Param]) (Maybe [Term]) -- ^ (/RES/) the second parameter is list of all possible values

12
src/compiler/GF/Grammar/Lookup.hs
View File

@@ -156,9 +156,9 @@ lookupAbsDef gr m c = errIn (render (text "looking up absdef of" <+> ppIdent c))
mo <- lookupModule gr m
info <- lookupIdentInfo mo c
case info of
AbsFun _ a d -> return (a,fmap (map unLoc) d)
AnyInd _ n -> lookupAbsDef gr n c
_ -> return (Nothing,Nothing)
AbsFun _ a d _ -> return (a,fmap (map unLoc) d)
AnyInd _ n -> lookupAbsDef gr n c
_ -> return (Nothing,Nothing)
lookupLincat :: SourceGrammar -> Ident -> Ident -> Err Type
lookupLincat gr m c | isPredefCat c = return defLinType --- ad hoc; not needed?
@@ -176,9 +176,9 @@ lookupFunType gr m c = do
mo <- lookupModule gr m
info <- lookupIdentInfo mo c
case info of
AbsFun (Just (L _ t)) _ _ -> return t
AnyInd _ n -> lookupFunType gr n c
_ -> Bad (render (text "cannot find type of" <+> ppIdent c))
AbsFun (Just (L _ t)) _ _ _ -> return t
AnyInd _ n -> lookupFunType gr n c
_ -> Bad (render (text "cannot find type of" <+> ppIdent c))
-- | this is needed at compile time
lookupCatContext :: SourceGrammar -> Ident -> Ident -> Err Context

2
src/compiler/GF/Grammar/Macros.hs
View File

@@ -624,7 +624,7 @@ allDependencies ism b =
ResParam (Just ps) _ -> [Just (L loc t) | L loc (_,cont) <- ps, (_,_,t) <- cont]
CncCat pty _ _ -> [pty]
CncFun _ pt _ -> [pt] ---- (Maybe (Ident,(Context,Type))
AbsFun pty _ ptr -> [pty] --- ptr is def, which can be mutual
AbsFun pty _ ptr _ -> [pty] --- ptr is def, which can be mutual
AbsCat (Just (L loc co)) -> [Just (L loc ty) | (_,_,ty) <- co]
_ -> []

48
src/compiler/GF/Grammar/Parser.y
View File

@@ -112,7 +112,7 @@ ModDef
(mtype,id) = $2
(extends,with,content) = $4
(opens,jments,opts) = case content of { Just c -> c; Nothing -> ([],[],noOptions) }
mapM_ (checkInfoType mtype) jments
jments <- mapM (checkInfoType mtype) jments
defs <- case buildAnyTree id jments of
Ok x -> return x
Bad msg -> fail msg
@@ -233,19 +233,19 @@ CatDef
FunDef :: { [(Ident,Info)] }
FunDef
: Posn ListIdent ':' Exp Posn { [(fun, AbsFun (Just (mkL $1 $5 $4)) Nothing (Just [])) | fun <- $2] }
: Posn ListIdent ':' Exp Posn { [(fun, AbsFun (Just (mkL $1 $5 $4)) Nothing (Just []) (Just True)) | fun <- $2] }
DefDef :: { [(Ident,Info)] }
DefDef
: Posn ListName '=' Exp Posn { [(f, AbsFun Nothing (Just 0) (Just [mkL $1 $5 ([],$4)])) | f <- $2] }
| Posn Name ListPatt '=' Exp Posn { [($2,AbsFun Nothing (Just (length $3)) (Just [mkL $1 $6 ($3,$5)]))] }
: Posn ListName '=' Exp Posn { [(f, AbsFun Nothing (Just 0) (Just [mkL $1 $5 ([],$4)]) Nothing) | f <- $2] }
| Posn Name ListPatt '=' Exp Posn { [($2,AbsFun Nothing (Just (length $3)) (Just [mkL $1 $6 ($3,$5)]) Nothing)] }
DataDef :: { [(Ident,Info)] }
DataDef
: Posn Ident '=' ListDataConstr Posn { ($2, AbsCat Nothing) :
[(fun, AbsFun Nothing Nothing Nothing) | fun <- $4] }
[(fun, AbsFun Nothing Nothing Nothing (Just True)) | fun <- $4] }
| Posn ListIdent ':' Exp Posn { -- (snd (valCat $4), AbsCat Nothing) :
[(fun, AbsFun (Just (mkL $1 $5 $4)) Nothing Nothing) | fun <- $2] }
[(fun, AbsFun (Just (mkL $1 $5 $4)) Nothing Nothing (Just True)) | fun <- $2] }
ParamDef :: { [(Ident,Info)] }
ParamDef
@@ -620,8 +620,8 @@ listCatDef (L loc (id,cont,size)) = [catd,nilfund,consfund]
consId = mkConsId id
catd = (listId, AbsCat (Just (L loc cont')))
nilfund = (baseId, AbsFun (Just (L loc niltyp)) Nothing Nothing)
consfund = (consId, AbsFun (Just (L loc constyp)) Nothing Nothing)
nilfund = (baseId, AbsFun (Just (L loc niltyp)) Nothing Nothing (Just True))
consfund = (consId, AbsFun (Just (L loc constyp)) Nothing Nothing (Just True))
cont' = [(b,mkId x i,ty) | (i,(b,x,ty)) <- zip [0..] cont]
xs = map (\(b,x,t) -> Vr x) cont'
@@ -671,34 +671,34 @@ isOverloading t =
Vr keyw | showIdent keyw == "overload" -> True -- overload is a "soft keyword"
_ -> False
checkInfoType mt (id,info) =
checkInfoType mt jment@(id,info) =
case info of
AbsCat pcont -> ifAbstract mt (locPerh pcont)
AbsFun pty _ pde -> ifAbstract mt (locPerh pty ++ maybe [] locAll pde)
CncCat pty pd ppn -> ifConcrete mt (locPerh pty ++ locPerh pd ++ locPerh ppn)
CncFun _ pd ppn -> ifConcrete mt (locPerh pd ++ locPerh ppn)
ResParam pparam _ -> ifResource mt (maybe [] locAll pparam)
ResValue ty -> ifResource mt (locL ty)
ResOper pty pt -> ifResource mt (locPerh pty ++ locPerh pt)
ResOverload _ xs -> ifResource mt (concat [[loc1,loc2] | (L loc1 _,L loc2 _) <- xs])
AbsCat pcont -> ifAbstract mt (locPerh pcont)
AbsFun pty _ pde _ -> ifAbstract mt (locPerh pty ++ maybe [] locAll pde)
CncCat pty pd ppn -> ifConcrete mt (locPerh pty ++ locPerh pd ++ locPerh ppn)
CncFun _ pd ppn -> ifConcrete mt (locPerh pd ++ locPerh ppn)
ResParam pparam _ -> ifResource mt (maybe [] locAll pparam)
ResValue ty -> ifResource mt (locL ty)
ResOper pty pt -> return (id,AbsFun pty (fmap (const 0) pt) (Just (maybe [] (\(L l t) -> [L l ([],t)]) pt)) (Just False))
ResOverload _ xs -> ifResource mt (concat [[loc1,loc2] | (L loc1 _,L loc2 _) <- xs])
where
locPerh = maybe [] locL
locAll xs = [loc | L loc x <- xs]
locL (L loc x) = [loc]
illegal ((s,e):_) = failLoc (Pn s 0) "illegal definition"
illegal _ = return ()
illegal _ = return jment
ifAbstract MTAbstract locs = return ()
ifAbstract MTAbstract locs = return jment
ifAbstract _ locs = illegal locs
ifConcrete (MTConcrete _) locs = return ()
ifConcrete (MTConcrete _) locs = return jment
ifConcrete _ locs = illegal locs
ifResource (MTConcrete _) locs = return ()
ifResource (MTInstance _) locs = return ()
ifResource MTInterface locs = return ()
ifResource MTResource locs = return ()
ifResource (MTConcrete _) locs = return jment
ifResource (MTInstance _) locs = return jment
ifResource MTInterface locs = return jment
ifResource MTResource locs = return jment
ifResource _ locs = illegal locs
mkAlts cs = case cs of

8
src/compiler/GF/Grammar/Printer.hs
View File

@@ -78,9 +78,13 @@ ppJudgement q (id, AbsCat pcont ) =
(case pcont of
Just (L _ cont) -> hsep (map (ppDecl q) cont)
Nothing -> empty) <+> semi
ppJudgement q (id, AbsFun ptype _ pexp) =
ppJudgement q (id, AbsFun ptype _ pexp poper) =
let kind | isNothing pexp = "data"
| poper == Just False = "oper"
| otherwise = "fun"
in
(case ptype of
Just (L _ typ) -> text (if isNothing pexp then "data" else "fun") <+> ppIdent id <+> colon <+> ppTerm q 0 typ <+> semi
Just (L _ typ) -> text kind <+> ppIdent id <+> colon <+> ppTerm q 0 typ <+> semi
Nothing -> empty) $$
(case pexp of
Just [] -> empty

1
src/runtime/haskell/PGF/Generate.hs
View File

@@ -86,7 +86,6 @@ prove dp scope (TTyp env1 (DTyp hypos1 cat es1)) = do
vs1 <- mapM (PGF.TypeCheck.eval env1) es1
let scope' = exScope scope env1 hypos1
(fe,TTyp env2 (DTyp hypos2 _ es2)) <- select cat scope' dp
if fe == EFun (mkCId "plus") then mzero else return ()
case dp of
Just 0 | not (null hypos2) -> mzero
_ -> return ()

13
testsuite/compiler/check/abstract-operations/Nat.gf Normal file
View File

@@ -0,0 +1,13 @@
abstract Nat = {
cat Nat ;
data zero : Nat ;
succ : Nat -> Nat ;
oper plus : Nat -> Nat -> Nat ;
def plus zero y = y ;
plus (succ x) y = succ (plus x y) ;
oper twice : Nat -> Nat = \x -> plus x x ;
}

5
testsuite/compiler/check/abstract-operations/abstract-operations.gfs Normal file
View File

@@ -0,0 +1,5 @@
-- here we test that the abstract operations are not used for proof search
i testsuite\compiler\check\abstract-operations\Nat.gf
gt -cat=Nat -number=10 -depth=10
pt -compute (twice (succ zero))

13
testsuite/compiler/check/abstract-operations/abstract-operations.gfs.gold Normal file
View File

@@ -0,0 +1,13 @@
zero
succ zero
succ (succ zero)
succ (succ (succ zero))
succ (succ (succ (succ zero)))
succ (succ (succ (succ (succ zero))))
succ (succ (succ (succ (succ (succ zero)))))
succ (succ (succ (succ (succ (succ (succ zero))))))
succ (succ (succ (succ (succ (succ (succ (succ zero)))))))
succ (succ (succ (succ (succ (succ (succ (succ (succ zero))))))))
succ (succ zero)