started a directory of grammars testing testgf3 features

This commit is contained in:
aarne
2008-02-22 15:17:50 +00:00
parent 9e6064709f
commit 2faba90119
7 changed files with 25 additions and 14 deletions

View File

@@ -0,0 +1,10 @@
resource Param = {
param Bool = True | False ;
oper and : Bool -> Bool -> Bool = \x,y -> case x of {
True => y ;
_ => False
} ;
}

View File

@@ -516,6 +516,8 @@ inferLType gr trm = case trm of
Empty -> return (trm, typeStr)
EParam _ cos -> return (trm, typePType) ---- check cos
C s1 s2 ->
check2 (flip justCheck typeStr) C s1 s2 typeStr

View File

@@ -114,7 +114,7 @@ resOverload tts = resOperDef (Overload tts)
-- param p = ci gi is encoded as p : ((ci : gi) -> p) -> Type
-- we use EData instead of p to make circularity check easier
resParam :: Ident -> [(Ident,Context)] -> Judgement
resParam p cos = addJDef (EParam cos) (emptyJudgement JParam)
resParam p cos = addJDef (EParam (Con p) cos) (addJType typePType (emptyJudgement JParam))
-- to enable constructor type lookup:
-- create an oper for each constructor p = c g, as c : g -> p = EData

View File

@@ -71,7 +71,7 @@ trAnyDef (i,ju) = let
---- JFun ty EData -> [P.DefFunData [P.FunDef [i'] (trt ty)]]
JParam -> [P.DefPar [
P.ParDefDir i0 [
P.ParConstr (tri c) (map trDecl co) | let EParam cos = jdef ju, (c,co) <- cos]
P.ParConstr (tri c) (map trDecl co) | let EParam _ cos = jdef ju, (c,co) <- cos]
]]
JOper -> case jdef ju of
Overload tysts ->
@@ -160,6 +160,8 @@ 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
EData -> P.EData
EParam t _ -> trt t
_ -> error $ "not yet" +++ show trm ----
trp :: Patt -> P.Patt

View File

@@ -109,7 +109,7 @@ data Term =
| EPatt Patt
| EPattType Term
| EParam [(Ident,Context)] -- to encode parameter constructor sets
| EParam Term [(Ident,Context)] -- to encode parameter constructor sets
| FV [Term] -- ^ free variation: @variants { s ; ... }@

View File

@@ -61,20 +61,16 @@ lookupOverload gr m c = do
lookupParams :: GF -> Ident -> Ident -> Err [(Ident,Context)]
lookupParams gf m c = do
ty <- lookupJField jtype gf m c
return [(k,contextOfType t) | (k,t) <- contextOfType ty]
EParam _ ty <- lookupJField jdef gf m c
return ty
lookupParamConstructor :: GF -> Ident -> Ident -> Err Type
lookupParamConstructor = lookupJField jtype
lookupParamValues :: GF -> Ident -> Ident -> Err [Term]
lookupParamValues gf m c = do
d <- lookupJField jdef gf m c
case d of
---- V _ ts -> return ts
_ -> do
ps <- lookupParams gf m c
liftM concat $ mapM mkPar ps
ps <- lookupParams gf m c
liftM concat $ mapM mkPar ps
where
mkPar (f,co) = do
vs <- liftM combinations $ mapM (\ (_,ty) -> allParamValues gf ty) co

View File

@@ -259,9 +259,10 @@ composOp co trm = case trm of
Eqs cc ->
do cc' <- mapPairListM (co . snd) cc
return (Eqs cc')
EParam cos ->
do cos' <- mapPairListM (mapPairListM (co . snd) . snd) cos
return (EParam cos')
EParam ty cos ->
do ty' <- co ty
cos' <- mapPairListM (mapPairListM (co . snd) . snd) cos
return (EParam ty' cos')
V ty vs ->
do ty' <- co ty
vs' <- mapM co vs