new definitions of term and judgement syntax

3 files changed, 223 insertions, 14 deletions

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