From be080aff39f3b7047978182055e029a179e2db76 Mon Sep 17 00:00:00 2001 From: aarne Date: Wed, 28 Nov 2007 22:11:47 +0000 Subject: [PATCH] judgement construction after parsing --- src/GF/Devel/Judgements.hs | 50 ++------------------------- src/GF/Devel/Lookup.hs | 21 ++++++++++-- src/GF/Devel/MkJudgements.hs | 66 ++++++++++++++++++++++++++++++++++++ src/GF/Devel/Terms.hs | 2 -- 4 files changed, 86 insertions(+), 53 deletions(-) create mode 100644 src/GF/Devel/MkJudgements.hs diff --git a/src/GF/Devel/Judgements.hs b/src/GF/Devel/Judgements.hs index 36ff90e68..9d2afdc6a 100644 --- a/src/GF/Devel/Judgements.hs +++ b/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 - diff --git a/src/GF/Devel/Lookup.hs b/src/GF/Devel/Lookup.hs index c2f60f743..13e854480 100644 --- a/src/GF/Devel/Lookup.hs +++ b/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" diff --git a/src/GF/Devel/MkJudgements.hs b/src/GF/Devel/MkJudgements.hs new file mode 100644 index 000000000..070e2ad6f --- /dev/null +++ b/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 + diff --git a/src/GF/Devel/Terms.hs b/src/GF/Devel/Terms.hs index 0a173833e..c2a6022c7 100644 --- a/src/GF/Devel/Terms.hs +++ b/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