forked from GitHub/gf-core
testgf3 in progress; fixed VP type in ExtraEng
This commit is contained in:
@@ -272,7 +272,7 @@ transResDef x = case x of
|
||||
mkParamDefs (p,pars) =
|
||||
if null pars
|
||||
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
|
||||
(_,G.App keyw (G.R fs@(_:_:_))) | isOverloading keyw c fs ->
|
||||
|
||||
@@ -10,7 +10,7 @@ import Data.Map
|
||||
import Debug.Trace (trace)
|
||||
|
||||
------------------
|
||||
-- abstractions on Grammar
|
||||
-- abstractions on Grammar, constructing objects
|
||||
------------------
|
||||
|
||||
-- abstractions on GF
|
||||
@@ -111,17 +111,15 @@ resOper ty tr = addJDef tr (resOperType ty)
|
||||
resOverload :: [(Type,Term)] -> Judgement
|
||||
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
|
||||
resParam :: [(Ident,Context)] -> Judgement
|
||||
resParam cos = addJType constrs (emptyJudgement JParam) where
|
||||
constrs = mkProd [(c,mkProd co EData) | (c,co) <- cos] typeType
|
||||
resParam :: Ident -> [(Ident,Context)] -> Judgement
|
||||
resParam p cos = addJDef (EParam cos) (emptyJudgement JParam)
|
||||
|
||||
-- to enable constructor type lookup:
|
||||
-- create an oper for each constructor p = c g, as c : g -> p = EData
|
||||
paramConstructors :: Ident -> [(Ident,Context)] -> [(Ident,Judgement)]
|
||||
paramConstructors p cs =
|
||||
[(c,resOper (mkProd co (Con p)) EData) | (c,co) <- cs]
|
||||
paramConstructors p cs = [(c,resOper (mkProd co (Con p)) EData) | (c,co) <- cs]
|
||||
|
||||
-- unifying contents of judgements
|
||||
|
||||
|
||||
@@ -71,10 +71,8 @@ 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) |
|
||||
(c,co) <- [(k,contextOfType t) | (k,t) <- contextOfType (jtype ju)]
|
||||
]
|
||||
]]
|
||||
P.ParConstr (tri c) (map trDecl co) | let EParam cos = jdef ju, (c,co) <- cos]
|
||||
]]
|
||||
JOper -> case jdef ju of
|
||||
Overload tysts ->
|
||||
[P.DefOper [P.DDef [i'] (
|
||||
@@ -89,13 +87,6 @@ trAnyDef (i,ju) = let
|
||||
[P.DefLin [trDef i (Meta 0) (jdef ju)]]
|
||||
---- ++ [P.DefPrintFun [P.DDef [mkName i] (trt pr)] | Yes pr <- [ppr]]
|
||||
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 i pty ptr = case (pty,ptr) of
|
||||
|
||||
@@ -51,7 +51,8 @@ data Judgement = Judgement {
|
||||
jprintname :: Term, -- - - prname prname - -
|
||||
jlink :: Ident,
|
||||
jposition :: Int
|
||||
}
|
||||
}
|
||||
deriving Show
|
||||
|
||||
data JudgementForm =
|
||||
JCat
|
||||
@@ -61,7 +62,7 @@ data JudgementForm =
|
||||
| JOper
|
||||
| JParam
|
||||
| JLink
|
||||
deriving Eq
|
||||
deriving (Eq,Show)
|
||||
|
||||
type Type = Term
|
||||
|
||||
@@ -108,6 +109,8 @@ data Term =
|
||||
| EPatt Patt
|
||||
| EPattType Term
|
||||
|
||||
| EParam [(Ident,Context)] -- to encode parameter constructor sets
|
||||
|
||||
| FV [Term] -- ^ free variation: @variants { s ; ... }@
|
||||
|
||||
| Alts (Term, [(Term, Term)]) -- ^ prefix-dependent: @pre {t ; s\/c ; ...}@
|
||||
|
||||
@@ -44,7 +44,7 @@ lookupOperType gr m c = do
|
||||
case jform ju of
|
||||
JParam -> return typePType
|
||||
_ -> 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
|
||||
---- can't be just lookupJField jtype
|
||||
|
||||
|
||||
@@ -259,6 +259,9 @@ 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')
|
||||
V ty vs ->
|
||||
do ty' <- co ty
|
||||
vs' <- mapM co vs
|
||||
|
||||
Reference in New Issue
Block a user