forked from GitHub/gf-core
testgf3 in progress; fixed VP type in ExtraEng
This commit is contained in:
@@ -35,7 +35,6 @@ concrete CatEng of Cat = CommonX ** open ResEng, Prelude in {
|
|||||||
-- Verb
|
-- Verb
|
||||||
|
|
||||||
VP = ResEng.VP ;
|
VP = ResEng.VP ;
|
||||||
|
|
||||||
Comp = {s : Agr => Str} ;
|
Comp = {s : Agr => Str} ;
|
||||||
|
|
||||||
-- Adjective
|
-- Adjective
|
||||||
|
|||||||
@@ -28,7 +28,7 @@ concrete ExtraEng of ExtraEngAbs = CatEng **
|
|||||||
ConsVPI = consrTable2 VPIForm Agr comma ;
|
ConsVPI = consrTable2 VPIForm Agr comma ;
|
||||||
|
|
||||||
MkVPI vp = {
|
MkVPI vp = {
|
||||||
s = \\v,a => vp.ad ++ vp.inf ++ vp.s2 ! a
|
s = \\v,a => vp.inf ++ vp.s2 ! a
|
||||||
} ;
|
} ;
|
||||||
ConjVPI = conjunctTable2 VPIForm Agr ;
|
ConjVPI = conjunctTable2 VPIForm Agr ;
|
||||||
ComplVPIVV vv vpi =
|
ComplVPIVV vv vpi =
|
||||||
|
|||||||
@@ -272,7 +272,7 @@ transResDef x = case x of
|
|||||||
mkParamDefs (p,pars) =
|
mkParamDefs (p,pars) =
|
||||||
if null pars
|
if null pars
|
||||||
then [(p,addJType M.meta0 (emptyJudgement G.JParam))] -- in an interface
|
then [(p,addJType M.meta0 (emptyJudgement G.JParam))] -- in an interface
|
||||||
else (p,resParam pars) : paramConstructors p pars
|
else (p,resParam p pars) : paramConstructors p pars
|
||||||
|
|
||||||
mkOverload (c,j) = case (G.jtype j, G.jdef j) of
|
mkOverload (c,j) = case (G.jtype j, G.jdef j) of
|
||||||
(_,G.App keyw (G.R fs@(_:_:_))) | isOverloading keyw c fs ->
|
(_,G.App keyw (G.R fs@(_:_:_))) | isOverloading keyw c fs ->
|
||||||
|
|||||||
@@ -10,7 +10,7 @@ import Data.Map
|
|||||||
import Debug.Trace (trace)
|
import Debug.Trace (trace)
|
||||||
|
|
||||||
------------------
|
------------------
|
||||||
-- abstractions on Grammar
|
-- abstractions on Grammar, constructing objects
|
||||||
------------------
|
------------------
|
||||||
|
|
||||||
-- abstractions on GF
|
-- abstractions on GF
|
||||||
@@ -111,17 +111,15 @@ resOper ty tr = addJDef tr (resOperType ty)
|
|||||||
resOverload :: [(Type,Term)] -> Judgement
|
resOverload :: [(Type,Term)] -> Judgement
|
||||||
resOverload tts = resOperDef (Overload tts)
|
resOverload tts = resOperDef (Overload tts)
|
||||||
|
|
||||||
-- param p = ci gi is encoded as p : ((ci : gi) -> EData) -> 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,Context)] -> Judgement
|
resParam :: Ident -> [(Ident,Context)] -> Judgement
|
||||||
resParam cos = addJType constrs (emptyJudgement JParam) where
|
resParam p cos = addJDef (EParam cos) (emptyJudgement JParam)
|
||||||
constrs = mkProd [(c,mkProd co EData) | (c,co) <- cos] typeType
|
|
||||||
|
|
||||||
-- 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
|
||||||
paramConstructors :: Ident -> [(Ident,Context)] -> [(Ident,Judgement)]
|
paramConstructors :: Ident -> [(Ident,Context)] -> [(Ident,Judgement)]
|
||||||
paramConstructors p cs =
|
paramConstructors p cs = [(c,resOper (mkProd co (Con p)) EData) | (c,co) <- cs]
|
||||||
[(c,resOper (mkProd co (Con p)) EData) | (c,co) <- cs]
|
|
||||||
|
|
||||||
-- unifying contents of judgements
|
-- unifying contents of judgements
|
||||||
|
|
||||||
|
|||||||
@@ -71,9 +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) |
|
P.ParConstr (tri c) (map trDecl co) | let EParam cos = jdef ju, (c,co) <- cos]
|
||||||
(c,co) <- [(k,contextOfType t) | (k,t) <- contextOfType (jtype ju)]
|
|
||||||
]
|
|
||||||
]]
|
]]
|
||||||
JOper -> case jdef ju of
|
JOper -> case jdef ju of
|
||||||
Overload tysts ->
|
Overload tysts ->
|
||||||
@@ -89,13 +87,6 @@ trAnyDef (i,ju) = let
|
|||||||
[P.DefLin [trDef i (Meta 0) (jdef ju)]]
|
[P.DefLin [trDef i (Meta 0) (jdef ju)]]
|
||||||
---- ++ [P.DefPrintFun [P.DDef [mkName i] (trt pr)] | Yes pr <- [ppr]]
|
---- ++ [P.DefPrintFun [P.DDef [mkName i] (trt pr)] | Yes pr <- [ppr]]
|
||||||
JLink -> []
|
JLink -> []
|
||||||
{-
|
|
||||||
---- encoding of AnyInd without changing syntax. AR 20/9/2007
|
|
||||||
AnyInd s b ->
|
|
||||||
[P.DefOper [P.DDef [mkName i]
|
|
||||||
(P.EApp (P.EInt (if s then 1 else 0)) (P.EIdent (tri b)))]]
|
|
||||||
-}
|
|
||||||
|
|
||||||
|
|
||||||
trDef :: Ident -> Type -> Term -> P.Def
|
trDef :: Ident -> Type -> Term -> P.Def
|
||||||
trDef i pty ptr = case (pty,ptr) of
|
trDef i pty ptr = case (pty,ptr) of
|
||||||
|
|||||||
@@ -52,6 +52,7 @@ data Judgement = Judgement {
|
|||||||
jlink :: Ident,
|
jlink :: Ident,
|
||||||
jposition :: Int
|
jposition :: Int
|
||||||
}
|
}
|
||||||
|
deriving Show
|
||||||
|
|
||||||
data JudgementForm =
|
data JudgementForm =
|
||||||
JCat
|
JCat
|
||||||
@@ -61,7 +62,7 @@ data JudgementForm =
|
|||||||
| JOper
|
| JOper
|
||||||
| JParam
|
| JParam
|
||||||
| JLink
|
| JLink
|
||||||
deriving Eq
|
deriving (Eq,Show)
|
||||||
|
|
||||||
type Type = Term
|
type Type = Term
|
||||||
|
|
||||||
@@ -108,6 +109,8 @@ data Term =
|
|||||||
| EPatt Patt
|
| EPatt Patt
|
||||||
| EPattType Term
|
| EPattType Term
|
||||||
|
|
||||||
|
| EParam [(Ident,Context)] -- to encode parameter constructor sets
|
||||||
|
|
||||||
| FV [Term] -- ^ free variation: @variants { s ; ... }@
|
| FV [Term] -- ^ free variation: @variants { s ; ... }@
|
||||||
|
|
||||||
| Alts (Term, [(Term, Term)]) -- ^ prefix-dependent: @pre {t ; s\/c ; ...}@
|
| Alts (Term, [(Term, Term)]) -- ^ prefix-dependent: @pre {t ; s\/c ; ...}@
|
||||||
|
|||||||
@@ -44,7 +44,7 @@ lookupOperType gr m c = do
|
|||||||
case jform ju of
|
case jform ju of
|
||||||
JParam -> return typePType
|
JParam -> return typePType
|
||||||
_ -> case jtype ju of
|
_ -> case jtype ju of
|
||||||
Meta _ -> fail ("no type given to " ++ prIdent m ++ "." ++ prIdent c)
|
Meta _ -> fail ("no type given to " ++ prIdent m ++ "." ++ prIdent c ++ " in " ++ show ju)
|
||||||
ty -> return ty
|
ty -> return ty
|
||||||
---- can't be just lookupJField jtype
|
---- can't be just lookupJField jtype
|
||||||
|
|
||||||
|
|||||||
@@ -259,6 +259,9 @@ 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 ->
|
||||||
|
do cos' <- mapPairListM (mapPairListM (co . snd) . snd) cos
|
||||||
|
return (EParam 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