From 6fef03ed019e900a6382cac8564d9d2a8d10a107 Mon Sep 17 00:00:00 2001 From: aarne Date: Wed, 28 Nov 2007 11:58:47 +0000 Subject: [PATCH] new definitions of term and judgement syntax --- src/GF/Devel/Judgements.hs | 66 ++++++++++++++++++++ src/GF/Devel/Modules.hs | 52 +++++++++++----- src/GF/Devel/Terms.hs | 119 +++++++++++++++++++++++++++++++++++++ 3 files changed, 223 insertions(+), 14 deletions(-) create mode 100644 src/GF/Devel/Judgements.hs create mode 100644 src/GF/Devel/Terms.hs diff --git a/src/GF/Devel/Judgements.hs b/src/GF/Devel/Judgements.hs new file mode 100644 index 000000000..36ff90e68 --- /dev/null +++ b/src/GF/Devel/Judgements.hs @@ -0,0 +1,66 @@ +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 + jdef :: Term, -- lindef def - values + jlin :: Term, -- lincat lin def constructors + jprintname :: Term -- printname printname - - + } + +data JudgementForm = + JCat + | JFun + | JOper + | 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/Modules.hs b/src/GF/Devel/Modules.hs index bf45f86c3..1b7a2bca5 100644 --- a/src/GF/Devel/Modules.hs +++ b/src/GF/Devel/Modules.hs @@ -1,10 +1,12 @@ module GF.Devel.Modules where -import GF.Grammar.Grammar +import GF.Devel.Judgements +import GF.Devel.Terms import GF.Infra.Ident import GF.Data.Operations +import Control.Monad import Data.Map @@ -45,23 +47,45 @@ data MInclude = | MIExcept [Ident] | MIOnly [Ident] -data Judgement = Judgement { - jform :: JudgementForm, -- cat fun oper param - jtype :: Type, -- context type type type - jdef :: Term, -- lindef def - values - jlin :: Term, -- lincat lin def constructors - jprintname :: Term -- printname printname - - - } -data JudgementForm = - JCat - | JFun - | JOper - | JParam +-- look up fields for a constant in a grammar +lookupJField :: (Judgement -> a) -> GF -> Ident -> Ident -> Err a +lookupJField field gf m c = do + j <- lookupJudgement gf m c + return $ field j + +lookupJForm :: GF -> Ident -> Ident -> Err JudgementForm +lookupJForm = lookupJField jform + +-- the following don't (need to) check that the jment form is adequate + +lookupCatContext :: GF -> Ident -> Ident -> Err Context +lookupCatContext gf m c = do + ty <- lookupJField jtype gf m c + return [] ---- context of ty + +lookupFunType :: GF -> Ident -> Ident -> Err Term +lookupFunType = lookupJField jtype + +lookupLin :: GF -> Ident -> Ident -> Err Term +lookupLin = lookupJField jlin + +lookupLincat :: GF -> Ident -> Ident -> Err Term +lookupLincat = lookupJField jlin + +lookupParamValues :: GF -> Ident -> Ident -> Err [Term] +lookupParamValues gf m c = do + j <- lookupJudgement gf m c + case jdef j of + V _ ts -> return ts + _ -> raise "no parameter values" + +-- infrastructure for lookup + lookupIdent :: GF -> Ident -> Ident -> Err (Either Judgement Ident) lookupIdent gf m c = do - mo <- maybe (Bad "module not found") return $ mlookup m (gfmodules gf) + mo <- maybe (raise "module not found") return $ mlookup m (gfmodules gf) maybe (Bad "constant not found") return $ mlookup c (mjments mo) lookupJudgement :: GF -> Ident -> Ident -> Err Judgement diff --git a/src/GF/Devel/Terms.hs b/src/GF/Devel/Terms.hs new file mode 100644 index 000000000..0a173833e --- /dev/null +++ b/src/GF/Devel/Terms.hs @@ -0,0 +1,119 @@ +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 + +type Type = Term +type Cat = QIdent +type Fun = QIdent + +type QIdent = (Ident,Ident) + +data Term = + Vr Ident -- ^ variable + | Con Ident -- ^ constructor + | EData -- ^ to mark in definition that a fun is a constructor + | Sort String -- ^ predefined type + | EInt Integer -- ^ integer literal + | EFloat Double -- ^ floating point literal + | K String -- ^ string literal or token: @\"foo\"@ + | Empty -- ^ the empty string @[]@ + + | App Term Term -- ^ application: @f a@ + | Abs Ident Term -- ^ abstraction: @\x -> b@ + | Meta MetaSymb -- ^ metavariable: @?i@ (only parsable: ? = ?0) + | Prod Ident Term Term -- ^ function type: @(x : A) -> B@ + | Eqs [Equation] -- ^ abstraction by cases: @fn {x y -> b ; z u -> c}@ + -- only used in internal representation + | Typed Term Term -- ^ type-annotated term +-- +-- /below this, the constructors are only for concrete syntax/ + | Example Term String -- ^ example-based term: @in M.C "foo" + | RecType [Labelling] -- ^ record type: @{ p : A ; ...}@ + | R [Assign] -- ^ record: @{ p = a ; ...}@ + | P Term Label -- ^ projection: @r.p@ + | PI Term Label Int -- ^ index-annotated projection + | ExtR Term Term -- ^ extension: @R ** {x : A}@ (both types and terms) + + | Table Term Term -- ^ table type: @P => A@ + | T TInfo [Case] -- ^ table: @table {p => c ; ...}@ + | V Type [Term] -- ^ course of values: @table T [c1 ; ... ; cn]@ + | S Term Term -- ^ selection: @t ! p@ + | Val Type Int -- ^ parameter value number: @T # i# + + | Let LocalDef Term -- ^ local definition: @let {t : T = a} in b@ + + | Q Ident Ident -- ^ qualified constant from a module + | QC Ident Ident -- ^ qualified constructor from a module + + | C Term Term -- ^ concatenation: @s ++ t@ + | Glue Term Term -- ^ agglutination: @s + t@ + + | FV [Term] -- ^ free variation: @variants { s ; ... }@ + + | Alts (Term, [(Term, Term)]) -- ^ prefix-dependent: @pre {t ; s\/c ; ...}@ + + deriving (Read, Show, Eq, Ord) + +data Patt = + PC Ident [Patt] -- ^ constructor pattern: @C p1 ... pn@ @C@ + | PP Ident Ident [Patt] -- ^ qualified constr patt: @P.C p1 ... pn@ @P.C@ + | PV Ident -- ^ variable pattern: @x@ + | PW -- ^ wild card pattern: @_@ + | PR [(Label,Patt)] -- ^ record pattern: @{r = p ; ...}@ + | PString String -- ^ string literal pattern: @\"foo\"@ + | PInt Integer -- ^ integer literal pattern: @12@ + | PFloat Double -- ^ float literal pattern: @1.2@ + | PT Type Patt -- ^ type-annotated pattern + | PAs Ident Patt -- ^ as-pattern: x@p + + -- regular expression patterns + | PNeg Patt -- ^ negated pattern: -p + | PAlt Patt Patt -- ^ disjunctive pattern: p1 | p2 + | PSeq Patt Patt -- ^ sequence of token parts: p + q + | PRep Patt -- ^ repetition of token part: p* + + deriving (Read, Show, Eq, Ord) + +-- | to guide computation and type checking of tables +data TInfo = + TRaw -- ^ received from parser; can be anything + | TTyped Type -- ^ type annotated, but can be anything + | TComp Type -- ^ expanded + | TWild Type -- ^ just one wild card pattern, no need to expand + deriving (Read, Show, Eq, Ord) + +-- | record label +data Label = + LIdent String + | LVar Int + deriving (Read, Show, Eq, Ord) + +type MetaSymb = Int + +type Decl = (Ident,Term) -- (x:A) (_:A) A +type Context = [Decl] -- (x:A)(y:B) (x,y:A) (_,_:A) +type Substitution = [(Ident, Term)] +type Equation = ([Patt],Term) + +type Labelling = (Label, Term) +type Assign = (Label, (Maybe Type, Term)) +type Case = (Patt, Term) +type LocalDef = (Ident, (Maybe Type, Term)) + + +-- | branches à la Alfa +newtype Branch = Branch (Con,([Ident],Term)) deriving (Eq, Ord,Show,Read) +type Con = Ident --- + +varLabel :: Int -> Label +varLabel = LVar + +wildPatt :: Patt +wildPatt = PW + +type Trm = Term