forked from GitHub/gf-core
new definitions of term and judgement syntax
This commit is contained in:
aarne
66
src/GF/Devel/Judgements.hs
Normal file
66
src/GF/Devel/Judgements.hs
Normal file
@@ -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
|
||||
|
||||
@@ -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
|
||||
|
||||
119
src/GF/Devel/Terms.hs
Normal file
119
src/GF/Devel/Terms.hs
Normal file
@@ -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
|
||||
Reference in New Issue
Block a user