mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-05-20 16:42:51 -06:00
started a directory of grammars testing testgf3 features
This commit is contained in:
10
examples/features/Param.gf
Normal file
10
examples/features/Param.gf
Normal file
@@ -0,0 +1,10 @@
|
|||||||
|
resource Param = {
|
||||||
|
|
||||||
|
param Bool = True | False ;
|
||||||
|
|
||||||
|
oper and : Bool -> Bool -> Bool = \x,y -> case x of {
|
||||||
|
True => y ;
|
||||||
|
_ => False
|
||||||
|
} ;
|
||||||
|
|
||||||
|
}
|
||||||
@@ -316,8 +316,10 @@ resource ResEng = ParamX ** open Prelude in {
|
|||||||
agrVerb (verb.s ! VPres) (verb.s ! VInf) ;
|
agrVerb (verb.s ! VPres) (verb.s ! VInf) ;
|
||||||
|
|
||||||
infVP : Bool -> VP -> Agr -> Str = \isAux,vp,a ->
|
infVP : Bool -> VP -> Agr -> Str = \isAux,vp,a ->
|
||||||
if_then_Str isAux [] "to" ++
|
case isAux of {True => [] ; False => "to"} ++
|
||||||
vp.inf ++ vp.s2 ! a ;
|
vp.inf ++ vp.s2 ! a ;
|
||||||
|
--- if_then_Str isAux [] "to" ++
|
||||||
|
--- vp.inf ++ vp.s2 ! a ;
|
||||||
|
|
||||||
agrVerb : Str -> Str -> Agr -> Str = \has,have,agr ->
|
agrVerb : Str -> Str -> Agr -> Str = \has,have,agr ->
|
||||||
case agr of {
|
case agr of {
|
||||||
|
|||||||
@@ -516,6 +516,8 @@ inferLType gr trm = case trm of
|
|||||||
|
|
||||||
Empty -> return (trm, typeStr)
|
Empty -> return (trm, typeStr)
|
||||||
|
|
||||||
|
EParam _ cos -> return (trm, typePType) ---- check cos
|
||||||
|
|
||||||
C s1 s2 ->
|
C s1 s2 ->
|
||||||
check2 (flip justCheck typeStr) C s1 s2 typeStr
|
check2 (flip justCheck typeStr) C s1 s2 typeStr
|
||||||
|
|
||||||
|
|||||||
@@ -114,7 +114,7 @@ resOverload tts = resOperDef (Overload tts)
|
|||||||
-- param p = ci gi is encoded as p : ((ci : gi) -> p) -> Type
|
-- param p = ci gi is encoded as p : ((ci : gi) -> p) -> Type
|
||||||
-- we use EData instead of p to make circularity check easier
|
-- we use EData instead of p to make circularity check easier
|
||||||
resParam :: Ident -> [(Ident,Context)] -> Judgement
|
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:
|
-- to enable constructor type lookup:
|
||||||
-- create an oper for each constructor p = c g, as c : g -> p = EData
|
-- create an oper for each constructor p = c g, as c : g -> p = EData
|
||||||
|
|||||||
@@ -71,7 +71,7 @@ trAnyDef (i,ju) = let
|
|||||||
---- JFun ty EData -> [P.DefFunData [P.FunDef [i'] (trt ty)]]
|
---- JFun ty EData -> [P.DefFunData [P.FunDef [i'] (trt ty)]]
|
||||||
JParam -> [P.DefPar [
|
JParam -> [P.DefPar [
|
||||||
P.ParDefDir i0 [
|
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
|
JOper -> case jdef ju of
|
||||||
Overload tysts ->
|
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]
|
Alts (t, tt) -> P.EPre (trt t) [P.Alt (trt v) (trt c) | (v,c) <- tt]
|
||||||
FV ts -> P.EVariants $ map trt ts
|
FV ts -> P.EVariants $ map trt ts
|
||||||
EData -> P.EData
|
EData -> P.EData
|
||||||
|
EParam t _ -> trt t
|
||||||
|
|
||||||
_ -> error $ "not yet" +++ show trm ----
|
_ -> error $ "not yet" +++ show trm ----
|
||||||
|
|
||||||
trp :: Patt -> P.Patt
|
trp :: Patt -> P.Patt
|
||||||
|
|||||||
@@ -109,7 +109,7 @@ data Term =
|
|||||||
| EPatt Patt
|
| EPatt Patt
|
||||||
| EPattType Term
|
| 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 ; ... }@
|
| FV [Term] -- ^ free variation: @variants { s ; ... }@
|
||||||
|
|
||||||
|
|||||||
@@ -61,18 +61,14 @@ lookupOverload gr m c = do
|
|||||||
|
|
||||||
lookupParams :: GF -> Ident -> Ident -> Err [(Ident,Context)]
|
lookupParams :: GF -> Ident -> Ident -> Err [(Ident,Context)]
|
||||||
lookupParams gf m c = do
|
lookupParams gf m c = do
|
||||||
ty <- lookupJField jtype gf m c
|
EParam _ ty <- lookupJField jdef gf m c
|
||||||
return [(k,contextOfType t) | (k,t) <- contextOfType ty]
|
return ty
|
||||||
|
|
||||||
lookupParamConstructor :: GF -> Ident -> Ident -> Err Type
|
lookupParamConstructor :: GF -> Ident -> Ident -> Err Type
|
||||||
lookupParamConstructor = lookupJField jtype
|
lookupParamConstructor = lookupJField jtype
|
||||||
|
|
||||||
lookupParamValues :: GF -> Ident -> Ident -> Err [Term]
|
lookupParamValues :: GF -> Ident -> Ident -> Err [Term]
|
||||||
lookupParamValues gf m c = do
|
lookupParamValues gf m c = do
|
||||||
d <- lookupJField jdef gf m c
|
|
||||||
case d of
|
|
||||||
---- V _ ts -> return ts
|
|
||||||
_ -> do
|
|
||||||
ps <- lookupParams gf m c
|
ps <- lookupParams gf m c
|
||||||
liftM concat $ mapM mkPar ps
|
liftM concat $ mapM mkPar ps
|
||||||
where
|
where
|
||||||
|
|||||||
@@ -259,9 +259,10 @@ composOp co trm = case trm of
|
|||||||
Eqs cc ->
|
Eqs cc ->
|
||||||
do cc' <- mapPairListM (co . snd) cc
|
do cc' <- mapPairListM (co . snd) cc
|
||||||
return (Eqs cc')
|
return (Eqs cc')
|
||||||
EParam cos ->
|
EParam ty cos ->
|
||||||
do cos' <- mapPairListM (mapPairListM (co . snd) . snd) cos
|
do ty' <- co ty
|
||||||
return (EParam cos')
|
cos' <- mapPairListM (mapPairListM (co . snd) . snd) cos
|
||||||
|
return (EParam ty' cos')
|
||||||
V ty vs ->
|
V ty vs ->
|
||||||
do ty' <- co ty
|
do ty' <- co ty
|
||||||
vs' <- mapM co vs
|
vs' <- mapM co vs
|
||||||
|
|||||||
Reference in New Issue
Block a user