judgement construction after parsing

src/GF/Devel/Judgements.hs

@@ -3,16 +3,11 @@ module GF.Devel.Judgements where
 import GF.Devel.Terms
 import GF.Infra.Ident
 
-import GF.Data.Operations
-
-import Control.Monad
-import Data.Map
-
 data Judgement = Judgement {
   jform :: JudgementForm,  -- cat         fun        oper    param
-  jtype :: Type,           -- context     type       type    type
+  jtype :: Type,           -- context     type       type    constructors
   jdef  :: Term,           -- lindef      def        -       values
-  jlin  :: Term,           -- lincat      lin        def     constructors
+  jlin  :: Term,           -- lincat      lin        def     -
   jprintname :: Term       -- printname   printname  -       -
   }
 
@@ -23,44 +18,3 @@ data JudgementForm =
   | JParam
   deriving Eq
 
--- constructing judgements from parse tree
-
-emptyJudgement :: JudgementForm -> Judgement
-emptyJudgement form = Judgement form meta meta meta meta where
-  meta = Meta 0
-
-absCat :: Context -> Judgement
-absCat co = (emptyJudgement JCat) {jtype = Sort "Type"} ---- works for empty co
-
-absFun :: Type -> Judgement
-absFun ty = (emptyJudgement JFun) {jtype = ty}
-
-cncCat :: Type -> Judgement
-cncCat ty = (emptyJudgement JCat) {jlin = ty}
-
-cncFun :: Term -> Judgement
-cncFun tr = (emptyJudgement JFun) {jlin = tr}
-
-resOperType :: Type -> Judgement
-resOperType ty = (emptyJudgement JOper) {jtype = ty}
-
-resOperDef :: Term -> Judgement
-resOperDef tr = (emptyJudgement JOper) {jlin = tr}
-
-resOper :: Type -> Term -> Judgement
-resOper ty tr = (emptyJudgement JOper) {jtype = ty, jlin = tr}
-
--- unifying contents of judgements
-
-unifyJudgement :: Judgement -> Judgement -> Err Judgement
-unifyJudgement old new = do
-  testErr (jform old == jform new) "different judment forms"
-  [jty,jde,jli,jpri] <- mapM unifyField [jtype,jdef,jlin,jprintname]
-  return $ old{jtype = jty, jdef = jde, jlin = jli, jprintname = jpri}
- where
-   unifyField field = unifyTerm (field old) (field new)
-   unifyTerm oterm nterm = case (oterm,nterm) of
-     (Meta _,t) -> return t
-     (t,Meta _) -> return t
-     _ -> testErr (nterm == oterm) "incompatible fields" >> return nterm
-

src/GF/Devel/Lookup.hs

@@ -2,6 +2,7 @@ module GF.Devel.Lookup where
 
 import GF.Devel.Modules
 import GF.Devel.Judgements
+import GF.Devel.Macros
 import GF.Devel.Terms
 import GF.Infra.Ident
 
@@ -24,7 +25,7 @@ lookupJForm = lookupJField jform
 lookupCatContext :: GF -> Ident -> Ident -> Err Context
 lookupCatContext gf m c = do
   ty <- lookupJField jtype gf m c
-  return [] ---- context of ty
+  return $ contextOfType ty
 
 lookupFunType :: GF -> Ident -> Ident -> Err Term
 lookupFunType = lookupJField jtype 
@@ -35,10 +36,24 @@ lookupLin = lookupJField jlin
 lookupLincat :: GF -> Ident -> Ident -> Err Term
 lookupLincat = lookupJField jlin
 
+lookupOperType :: GF -> Ident -> Ident -> Err Term
+lookupOperType = lookupJField jtype 
+
+lookupOperDef :: GF -> Ident -> Ident -> Err Term
+lookupOperDef = lookupJField jlin
+
+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]
+
+lookupParamConstructor :: GF -> Ident -> Ident -> Err Type
+lookupParamConstructor = lookupJField jlin
+
 lookupParamValues :: GF -> Ident -> Ident -> Err [Term]
 lookupParamValues gf m c = do
-  j <- lookupJudgement gf m c
-  case jdef j of
+  d <- lookupJField jdef gf m c
+  case d of
     V _ ts -> return ts
     _ -> raise "no parameter values"
 

src/GF/Devel/MkJudgements.hs

@@ -0,0 +1,66 @@
+module GF.Devel.MkJudgements where
+
+import GF.Devel.Macros
+import GF.Devel.Judgements
+import GF.Devel.Terms
+import GF.Infra.Ident
+
+import GF.Data.Operations
+
+import Control.Monad
+import Data.Map
+
+-- constructing judgements from parse tree
+
+emptyJudgement :: JudgementForm -> Judgement
+emptyJudgement form = Judgement form meta meta meta meta where
+  meta = Meta 0
+
+absCat :: Context -> Judgement
+absCat co = (emptyJudgement JCat) {jtype = mkProd co typeType}
+
+absFun :: Type -> Judgement
+absFun ty = (emptyJudgement JFun) {jtype = ty}
+
+cncCat :: Type -> Judgement
+cncCat ty = (emptyJudgement JCat) {jlin = ty}
+
+cncFun :: Term -> Judgement
+cncFun tr = (emptyJudgement JFun) {jlin = tr}
+
+resOperType :: Type -> Judgement
+resOperType ty = (emptyJudgement JOper) {jtype = ty}
+
+resOperDef :: Term -> Judgement
+resOperDef tr = (emptyJudgement JOper) {jlin = tr}
+
+resOper :: Type -> Term -> Judgement
+resOper ty tr = (emptyJudgement JOper) {jtype = ty, jlin = tr}
+
+-- param m.p = c g  is encoded as p : (ci : gi -> EData) -> Type
+-- we use EData instead of m.p to make circularity check easier  
+resParam :: Ident -> Ident -> [(Ident,Context)] -> Judgement
+resParam m p cos = (emptyJudgement JParam) {
+  jtype = mkProd [(c,mkProd co EData) | (c,co) <- cos] typeType
+  }
+
+-- to enable constructor type lookup:
+-- create an oper for each constructor m.p = c g, as c : g -> m.p = EData
+paramConstructors :: Ident -> Ident -> [(Ident,Context)] -> [(Ident,Judgement)]
+paramConstructors m p cs = 
+  [(c,resOper (mkProd co (QC m p)) EData) | (c,co) <- cs]
+
+-- unifying contents of judgements
+
+unifyJudgement :: Judgement -> Judgement -> Err Judgement
+unifyJudgement old new = do
+  testErr (jform old == jform new) "different judment forms"
+  [jty,jde,jli,jpri] <- mapM unifyField [jtype,jdef,jlin,jprintname]
+  return $ old{jtype = jty, jdef = jde, jlin = jli, jprintname = jpri}
+ where
+   unifyField field = unifyTerm (field old) (field new)
+   unifyTerm oterm nterm = case (oterm,nterm) of
+     (Meta _,t) -> return t
+     (t,Meta _) -> return t
+     _ -> testErr (nterm == oterm) "incompatible fields" >> return nterm
+

src/GF/Devel/Terms.hs

@@ -1,8 +1,6 @@
 module GF.Devel.Terms where
 
-import GF.Data.Str
 import GF.Infra.Ident
-import GF.Infra.Option ---
 import GF.Infra.Modules
 
 import GF.Data.Operations