summaryrefslogtreecommitdiff
path: root/src/GF/Grammar
diff options
context:
space:
mode:
Diffstat (limited to 'src/GF/Grammar')
-rw-r--r--src/GF/Grammar/AbsCompute.hs64
-rw-r--r--src/GF/Grammar/Abstract.hs24
-rw-r--r--src/GF/Grammar/AppPredefined.hs51
-rw-r--r--src/GF/Grammar/Compute.hs238
-rw-r--r--src/GF/Grammar/Grammar.hs154
-rw-r--r--src/GF/Grammar/LookAbs.hs125
-rw-r--r--src/GF/Grammar/Lookup.hs393
-rw-r--r--src/GF/Grammar/MMacros.hs261
-rw-r--r--src/GF/Grammar/Macros.hs634
-rw-r--r--src/GF/Grammar/PatternMatch.hs98
-rw-r--r--src/GF/Grammar/PrGrammar.hs189
-rw-r--r--src/GF/Grammar/Refresh.hs105
-rw-r--r--src/GF/Grammar/ReservedWords.hs32
-rw-r--r--src/GF/Grammar/TC.hs210
-rw-r--r--src/GF/Grammar/TypeCheck.hs231
-rw-r--r--src/GF/Grammar/Unify.hs84
-rw-r--r--src/GF/Grammar/Values.hs52
17 files changed, 2945 insertions, 0 deletions
diff --git a/src/GF/Grammar/AbsCompute.hs b/src/GF/Grammar/AbsCompute.hs
new file mode 100644
index 000000000..52a2ca678
--- /dev/null
+++ b/src/GF/Grammar/AbsCompute.hs
@@ -0,0 +1,64 @@
+module AbsCompute where
+
+import Operations
+
+import Abstract
+import PrGrammar
+import LookAbs
+import PatternMatch
+import Compute
+
+import Monad (liftM, liftM2)
+
+-- computation in abstract syntax w.r.t. explicit definitions.
+--- old GF computation; to be updated
+
+compute :: GFCGrammar -> Exp -> Err Exp
+compute = computeAbsTerm
+
+computeAbsTerm :: GFCGrammar -> Exp -> Err Exp
+computeAbsTerm gr = computeAbsTermIn gr []
+
+computeAbsTermIn :: GFCGrammar -> [Ident] -> Exp -> Err Exp
+computeAbsTermIn gr = compt where
+ compt vv t = case t of
+ Prod x a b -> liftM2 (Prod x) (compt vv a) (compt (x:vv) b)
+ Abs x b -> liftM (Abs x) (compt (x:vv) b)
+ _ -> do
+ let t' = beta vv t
+ (yy,f,aa) <- termForm t'
+ let vv' = yy ++ vv
+ aa' <- mapM (compt vv') aa
+ case look f of
+ Just (Eqs eqs) -> case findMatch eqs aa' of
+ Ok (d,g) -> do
+ let (xs,ts) = unzip g
+ ts' <- alphaFreshAll vv' ts ---
+ let g' = zip xs ts'
+ d' <- compt vv' $ substTerm vv' g' d
+ return $ mkAbs yy $ d'
+ _ -> do
+ return $ mkAbs yy $ mkApp f aa'
+ Just d -> do
+ d' <- compt vv' d
+ da <- ifNull (return d') (compt vv' . mkApp d') aa'
+ return $ mkAbs yy $ da
+ _ -> do
+ return $ mkAbs yy $ mkApp f aa'
+
+ look (Q m f) = case lookupAbsDef gr m f of
+ Ok (Just (Eqs [])) -> Nothing -- canonical
+ Ok md -> md
+ _ -> Nothing
+ look _ = Nothing
+
+beta :: [Ident] -> Exp -> Exp
+beta vv c = case c of
+ App (Abs x b) a -> beta vv $ substTerm vv [xvv] (beta (x:vv) b)
+ where xvv = (x,beta vv a)
+ App f a -> let (a',f') = (beta vv a, beta vv f) in
+ (if a'==a && f'==f then id else beta vv) $ App f' a'
+ Prod x a b -> Prod x (beta vv a) (beta (x:vv) b)
+ Abs x b -> Abs x (beta (x:vv) b)
+ _ -> c
+
diff --git a/src/GF/Grammar/Abstract.hs b/src/GF/Grammar/Abstract.hs
new file mode 100644
index 000000000..538fff90b
--- /dev/null
+++ b/src/GF/Grammar/Abstract.hs
@@ -0,0 +1,24 @@
+module Abstract (
+
+module Grammar,
+module Values,
+module Macros,
+module Ident,
+module MMacros,
+module PrGrammar,
+
+Grammar
+
+ ) where
+
+import Grammar
+import Values
+import Macros
+import Ident
+import MMacros
+import PrGrammar
+
+type Grammar = SourceGrammar ---
+
+
+
diff --git a/src/GF/Grammar/AppPredefined.hs b/src/GF/Grammar/AppPredefined.hs
new file mode 100644
index 000000000..f59c910b0
--- /dev/null
+++ b/src/GF/Grammar/AppPredefined.hs
@@ -0,0 +1,51 @@
+module AppPredefined where
+
+import Operations
+import Grammar
+import Ident
+import PrGrammar (prt)
+---- import PGrammar (pTrm)
+
+-- predefined function definitions. AR 12/3/2003.
+-- Type checker looks at signatures in predefined.gf
+
+appPredefined :: Term -> Term
+appPredefined t = case t of
+
+ App f x -> case f of
+
+ -- one-place functions
+ Q (IC "Predef") (IC f) -> case (f, appPredefined x) of
+ ("length", K s) -> EInt $ length s
+ _ -> t
+
+ -- two-place functions
+ App (Q (IC "Predef") (IC f)) z -> case (f, appPredefined z, appPredefined x) of
+ ("drop", EInt i, K s) -> K (drop i s)
+ ("take", EInt i, K s) -> K (take i s)
+ ("tk", EInt i, K s) -> K (take (max 0 (length s - i)) s)
+ ("dp", EInt i, K s) -> K (drop (max 0 (length s - i)) s)
+ ("eqStr",K s, K t) -> if s == t then predefTrue else predefFalse
+ ("eqInt",EInt i, EInt j) -> if i==j then predefTrue else predefFalse
+ ("plus", EInt i, EInt j) -> EInt $ i+j
+ ("show", _, t) -> K $ prt t
+ ("read", _, K s) -> str2tag s --- because of K, only works for atomic tags
+ _ -> t
+ _ -> t
+ _ -> t
+
+-- read makes variables into constants
+
+str2tag :: String -> Term
+str2tag s = case s of
+---- '\'' : cs -> mkCn $ pTrm $ init cs
+ _ -> Cn $ IC s ---
+ where
+ mkCn t = case t of
+ Vr i -> Cn i
+ App c a -> App (mkCn c) (mkCn a)
+ _ -> t
+
+
+predefTrue = Q (IC "Predef") (IC "PTrue")
+predefFalse = Q (IC "Predef") (IC "PFalse")
diff --git a/src/GF/Grammar/Compute.hs b/src/GF/Grammar/Compute.hs
new file mode 100644
index 000000000..1f1eba28c
--- /dev/null
+++ b/src/GF/Grammar/Compute.hs
@@ -0,0 +1,238 @@
+module Compute where
+
+import Operations
+import Grammar
+import Ident
+import Str
+import PrGrammar
+import Modules
+import Macros
+import Lookup
+import Refresh
+import PatternMatch
+
+import AppPredefined
+
+import List (nub,intersperse)
+import Monad (liftM2, liftM)
+
+-- computation of concrete syntax terms into normal form
+-- used mainly for partial evaluation
+
+computeConcrete :: SourceGrammar -> Term -> Err Term
+computeConcrete g t = {- refreshTerm t >>= -} computeTerm g [] t
+
+computeTerm :: SourceGrammar -> Substitution -> Term -> Err Term
+computeTerm gr = comp where
+
+ comp g t = --- errIn ("subterm" +++ prt t) $ --- for debugging
+ case t of
+
+ Q (IC "Predef") _ -> return t
+ Q p c -> look p c
+
+ -- if computed do nothing
+ Computed t' -> return $ unComputed t'
+
+ Vr x -> do
+ t' <- maybe (prtBad ("no value given to variable") x) return $ lookup x g
+ case t' of
+ _ | t == t' -> return t
+ _ -> comp g t'
+
+ Abs x b -> do
+ b' <- comp (ext x (Vr x) g) b
+ return $ Abs x b'
+
+ Let (x,(_,a)) b -> do
+ a' <- comp g a
+ comp (ext x a' g) b
+
+ Prod x a b -> do
+ a' <- comp g a
+ b' <- comp (ext x (Vr x) g) b
+ return $ Prod x a' b'
+
+ -- beta-convert
+ App f a -> do
+ f' <- comp g f
+ a' <- comp g a
+ case (f',a') of
+ (Abs x b,_) -> comp (ext x a' g) b
+ (FV fs, _) -> mapM (\c -> comp g (App c a')) fs >>= return . FV
+ (_, FV as) -> mapM (\c -> comp g (App f' c)) as >>= return . FV
+
+ (Alias _ _ d, _) -> comp g (App d a')
+
+ (S (T i cs) e,_) -> prawitz g i (flip App a') cs e
+
+ _ -> returnC $ appPredefined $ App f' a'
+ P t l -> do
+ t' <- comp g t
+ case t' of
+ FV rs -> mapM (\c -> comp g (P c l)) rs >>= returnC . FV
+ R r -> maybe (prtBad "no value for label" l) (comp g . snd) $ lookup l r
+
+ ExtR (R a) b -> -- NOT POSSIBLE both a and b records!
+ case comp g (P (R a) l) of
+ Ok v -> return v
+ _ -> comp g (P b l)
+ ExtR a (R b) ->
+ case comp g (P (R b) l) of
+ Ok v -> return v
+ _ -> comp g (P a l)
+
+ Alias _ _ r -> comp g (P r l)
+
+ S (T i cs) e -> prawitz g i (flip P l) cs e
+
+ _ -> returnC $ P t' l
+
+ S t v -> do
+ t' <- comp g t
+ v' <- comp g v
+ case t' of
+ T _ [(PV IW,c)] -> comp g c --- an optimization
+ T _ [(PT _ (PV IW),c)] -> comp g c
+
+ T _ [(PV z,c)] -> comp (ext z v' g) c --- another optimization
+ T _ [(PT _ (PV z),c)] -> comp (ext z v' g) c
+
+ FV ccs -> mapM (\c -> comp g (S c v')) ccs >>= returnC . FV
+
+ T _ cc -> case v' of
+ FV vs -> mapM (\c -> comp g (S t' c)) vs >>= returnC . FV
+ _ -> case matchPattern cc v' of
+ Ok (c,g') -> comp (g' ++ g) c
+ _ | isCan v' -> prtBad ("missing case" +++ prt v' +++ "in") t
+ _ -> return $ S t' v' -- if v' is not canonical
+
+ Alias _ _ d -> comp g (S d v')
+
+ S (T i cs) e -> prawitz g i (flip S v') cs e
+
+ _ -> returnC $ S t' v'
+
+ -- glue if you can
+ Glue x0 y0 -> do
+ x <- comp g x0
+ y <- comp g y0
+ case (x,y) of
+ (Alias _ _ d, y) -> comp g $ Glue d y
+ (x, Alias _ _ d) -> comp g $ Glue x d
+
+ (S (T i cs) e, s) -> prawitz g i (flip Glue s) cs e
+ (s, S (T i cs) e) -> prawitz g i (Glue s) cs e
+ (_,K "") -> return x
+ (K "",_) -> return y
+ (K a, K b) -> return $ K (a ++ b)
+ (K a, Alts (d,vs)) -> do
+ let glx = Glue x
+ comp g $ Alts (glx d, [(glx v,c) | (v,c) <- vs])
+ (Alts _, K a) -> do
+ x' <- strsFromTerm x
+ return $ variants [
+ foldr1 C (map K (str2strings (glueStr v (str a)))) | v <- x']
+ _ -> do
+ mapM_ checkNoArgVars [x,y]
+ r <- composOp (comp g) t
+ returnC r
+
+ Alts _ -> do
+ r <- composOp (comp g) t
+ returnC r
+
+ -- remove empty
+ C a b -> do
+ a' <- comp g a
+ b' <- comp g b
+ returnC $ case (a',b') of
+ (Empty,_) -> b'
+ (_,Empty) -> a'
+ _ -> C a' b'
+
+ -- reduce free variation as much as you can
+ FV [t] -> comp g t
+
+ -- merge record extensions if you can
+ ExtR r s -> do
+ r' <- comp g r
+ s' <- comp g s
+ case (r',s') of
+ (Alias _ _ d, _) -> comp g $ ExtR d s'
+ (_, Alias _ _ d) -> comp g $ Glue r' d
+
+ (R rs, R ss) -> return $ R (rs ++ ss)
+ (RecType rs, RecType ss) -> return $ RecType (rs ++ ss)
+ _ -> return $ ExtR r' s'
+
+ -- case-expand tables
+ T i cs -> do
+ pty0 <- getTableType i
+ ptyp <- comp g pty0
+ case allParamValues gr ptyp of
+ Ok vs -> do
+
+ cs' <- mapM (compBranchOpt g) cs
+ sts <- mapM (matchPattern cs') vs
+ ts <- mapM (\ (c,g') -> comp (g' ++ g) c) sts
+ ps <- mapM term2patt vs
+ let ps' = ps --- PT ptyp (head ps) : tail ps
+ return $ T (TComp ptyp) (zip ps' ts)
+ _ -> do
+ cs' <- mapM (compBranch g) cs
+ return $ T i cs' -- happens with variable types
+
+ Alias c a d -> do
+ d' <- comp g d
+ return $ Alias c a d' -- alias only disappears in certain redexes
+
+ -- otherwise go ahead
+ _ -> composOp (comp g) t >>= returnC
+
+ where
+
+ look = lookupResDef gr
+
+ ext x a g = (x,a):g
+
+ returnC = return --- . computed
+
+ variants [t] = t
+ variants ts = FV ts
+
+ isCan v = case v of
+ Con _ -> True
+ QC _ _ -> True
+ App f a -> isCan f && isCan a
+ R rs -> all (isCan . snd . snd) rs
+ _ -> False
+
+ compBranch g (p,v) = do
+ let g' = contP p ++ g
+ v' <- comp g' v
+ return (p,v')
+
+ compBranchOpt g c@(p,v) = case contP p of
+ [] -> return c
+ _ -> err (const (return c)) return $ compBranch g c
+
+ contP p = case p of
+ PV x -> [(x,Vr x)]
+ PC _ ps -> concatMap contP ps
+ PP _ _ ps -> concatMap contP ps
+ PT _ p -> contP p
+ PR rs -> concatMap (contP . snd) rs
+ _ -> []
+
+ prawitz g i f cs e = do
+ cs' <- mapM (compBranch g) [(p, f v) | (p,v) <- cs]
+ return $ S (T i cs') e
+
+-- argument variables cannot be glued
+
+checkNoArgVars :: Term -> Err Term
+checkNoArgVars t = case t of
+ Vr (IA _) -> prtBad "cannot glue (+) term with run-time variable" t
+ Vr (IAV _) -> prtBad "cannot glue (+) term with run-time variable" t
+ _ -> composOp checkNoArgVars t
diff --git a/src/GF/Grammar/Grammar.hs b/src/GF/Grammar/Grammar.hs
new file mode 100644
index 000000000..1ee5425c4
--- /dev/null
+++ b/src/GF/Grammar/Grammar.hs
@@ -0,0 +1,154 @@
+module Grammar where
+
+import Str
+import Ident
+import Option ---
+import Modules
+
+import Operations
+
+-- AR 23/1/2000 -- 30/5/2001 -- 4/5/2003
+
+-- grammar as presented to the compiler
+
+type SourceGrammar = MGrammar Ident Option Info
+
+type SourceModInfo = ModInfo Ident Option Info
+
+type SourceModule = (Ident, SourceModInfo)
+
+type SourceAbs = Module Ident Option Info
+type SourceRes = Module Ident Option Info
+type SourceCnc = Module Ident Option Info
+
+-- judgements in abstract syntax
+
+data Info =
+ AbsCat (Perh Context) (Perh [Fun]) -- constructors
+ | AbsFun (Perh Type) (Perh Term) -- Yes f = canonical
+ | AbsTrans Ident
+
+-- judgements in resource
+ | ResParam (Perh [Param])
+ | ResValue (Perh Type) -- to mark parameter constructors for lookup
+ | ResOper (Perh Type) (Perh Term)
+
+-- judgements in concrete syntax
+ | CncCat (Perh Type) (Perh Term) MPr -- lindef ini'zed,
+ | CncFun (Maybe (Ident,(Context,Type))) (Perh Term) MPr -- type info added at TC
+
+-- indirection to module Ident; the Bool says if canonical
+ | AnyInd Bool Ident
+ deriving (Read, Show)
+
+type Perh a = Perhaps a Ident -- to express indirection to other module
+
+type MPr = Perhaps Term Ident -- printname
+
+type Type = Term
+type Cat = QIdent
+type Fun = QIdent
+
+type QIdent = (Ident,Ident)
+
+data Term =
+ Vr Ident -- variable
+ | Cn Ident -- constant
+ | Con Ident -- constructor
+ | Sort String -- basic type
+ | EInt Int -- integer 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
+
+ | ECase Term [Branch] -- case expression in abstract syntax à la Alfa
+
+-- below this only for concrete syntax
+ | RecType [Labelling] -- record type: { p : A ; ...}
+ | R [Assign] -- record: { p = a ; ...}
+ | P Term Label -- projection: r.p
+ | 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 ; ...}
+ | S Term Term -- selection: t ! p
+
+ | Let LocalDef Term -- local definition: let {t : T = a} in b
+
+ | Alias Ident Type Term -- constant and its definition, used in inlining
+
+ | Q Ident Ident -- qualified constant from a package
+ | QC Ident Ident -- qualified constructor from a package
+
+ | C Term Term -- concatenation: s ++ t
+ | Glue Term Term -- agglutination: s + t
+
+ | FV [Term] -- alternatives in free variation: variants { s ; ... }
+
+ | Alts (Term, [(Term, Term)]) -- alternatives by prefix: pre {t ; s/c ; ...}
+ | Strs [Term] -- conditioning prefix strings: strs {s ; ...}
+
+ --- these three are obsolete
+ | LiT Ident -- linearization type
+ | Ready Str -- result of compiling; not to be parsed ...
+ | Computed Term -- result of computing: not to be reopened nor parsed
+
+ deriving (Read, Show, Eq, Ord)
+
+data Patt =
+ PC Ident [Patt] -- constructor pattern: C p1 ... pn C
+ | PP Ident Ident [Patt] -- package constructor pattern: P.C p1 ... pn P.C
+ | PV Ident -- variable pattern: x
+ | PW -- wild card pattern: _
+ | PR [(Label,Patt)] -- record pattern: {r = p ; ...} -- only concrete
+ | PString String -- string literal pattern: "foo" -- only abstract
+ | PInt Int -- integer literal pattern: 12 -- only abstract
+ | PT Type Patt -- type-annotated pattern
+ 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 annontated, but can be anything
+ | TComp Type -- expanded
+ | TWild Type -- just one wild card pattern, no need to expand
+ deriving (Read, Show, Eq, Ord)
+
+data Label =
+ LIdent String
+ | LVar Int
+ deriving (Read, Show, Eq, Ord) -- record label
+
+newtype MetaSymb = MetaSymb Int deriving (Read, Show, Eq, Ord)
+
+type Decl = (Ident,Term) -- (x:A) (_:A) A
+type Context = [Decl] -- (x:A)(y:B) (x,y:A) (_,_:A)
+type Equation = ([Patt],Term)
+
+type Labelling = (Label, Term)
+type Assign = (Label, (Maybe Type, Term))
+type Case = (Patt, Term)
+type LocalDef = (Ident, (Maybe Type, Term))
+
+type Param = (Ident, Context)
+type Altern = (Term, [(Term, Term)])
+
+type Substitution = [(Ident, Term)]
+
+-- branches à la Alfa
+newtype Branch = Branch (Con,([Ident],Term)) deriving (Eq, Ord,Show,Read)
+type Con = Ident ---
+
+varLabel = LVar
+
+wildPatt :: Patt
+wildPatt = PV wildIdent
+
+type Trm = Term
diff --git a/src/GF/Grammar/LookAbs.hs b/src/GF/Grammar/LookAbs.hs
new file mode 100644
index 000000000..5e0994d46
--- /dev/null
+++ b/src/GF/Grammar/LookAbs.hs
@@ -0,0 +1,125 @@
+module LookAbs where
+
+import Operations
+import qualified GFC as C
+import Abstract
+import Ident
+
+import Modules
+
+import List (nub)
+import Monad
+
+type GFCGrammar = C.CanonGrammar
+
+lookupAbsDef :: GFCGrammar -> Ident -> Ident -> Err (Maybe Term)
+lookupAbsDef gr m c = do
+ mi <- lookupModule gr m
+ case mi of
+ ModMod mo -> do
+ info <- lookupInfo mo c
+ case info of
+ C.AbsFun _ t -> return $ return t
+ C.AnyInd _ n -> lookupAbsDef gr n c
+ _ -> return Nothing
+ _ -> Bad $ prt m +++ "is not an abstract module"
+
+lookupFunType :: GFCGrammar -> Ident -> Ident -> Err Type
+lookupFunType gr m c = do
+ mi <- lookupModule gr m
+ case mi of
+ ModMod mo -> do
+ info <- lookupInfo mo c
+ case info of
+ C.AbsFun t _ -> return t
+ C.AnyInd _ n -> lookupFunType gr n c
+ _ -> prtBad "cannot find type of" c
+ _ -> Bad $ prt m +++ "is not an abstract module"
+
+lookupCatContext :: GFCGrammar -> Ident -> Ident -> Err Context
+lookupCatContext gr m c = do
+ mi <- lookupModule gr m
+ case mi of
+ ModMod mo -> do
+ info <- lookupInfo mo c
+ case info of
+ C.AbsCat co _ -> return co
+ C.AnyInd _ n -> lookupCatContext gr n c
+ _ -> prtBad "unknown category" c
+ _ -> Bad $ prt m +++ "is not an abstract module"
+
+---- should be revised (20/9/2003)
+isPrimitiveFun :: GFCGrammar -> Fun -> Bool
+isPrimitiveFun gr (m,c) = case lookupAbsDef gr m c of
+ Ok (Just (Eqs [])) -> True -- is canonical
+ Ok (Just _) -> False -- has defining clauses
+ _ -> True -- has no definition
+
+
+-- looking up refinement terms
+
+lookupRef :: GFCGrammar -> Binds -> Term -> Err Val
+lookupRef gr binds at = case at of
+ Q m f -> lookupFunType gr m f >>= return . vClos
+ Vr i -> maybeErr ("unknown variable" +++ prt at) $ lookup i binds
+ _ -> prtBad "cannot refine with complex term" at ---
+
+refsForType :: (Val -> Type -> Bool) -> GFCGrammar -> Binds -> Val -> [(Term,Val)]
+refsForType compat gr binds val =
+ [(vr i, t) | (i,t) <- binds, Ok ty <- [val2exp t], compat val ty] ++
+ [(qq f, vClos t) | (f,t) <- funsForType compat gr val]
+
+
+funRulesOf :: GFCGrammar -> [(Fun,Type)]
+funRulesOf gr =
+---- funRulesForLiterals ++
+ [((i,f),typ) | (i, ModMod m) <- modules gr,
+ mtype m == MTAbstract,
+ (f, C.AbsFun typ _) <- tree2list (jments m)]
+
+allCatsOf :: GFCGrammar -> [(Cat,Context)]
+allCatsOf gr =
+ [((i,c),cont) | (i, ModMod m) <- modules gr,
+ isModAbs m,
+ (c, C.AbsCat cont _) <- tree2list (jments m)]
+
+funsForType :: (Val -> Type -> Bool) -> GFCGrammar -> Val -> [(Fun,Type)]
+funsForType compat gr val = [(fun,typ) | (fun,typ) <- funRulesOf gr,
+ compat val typ]
+
+funsOnType :: (Val -> Type -> Bool) -> GFCGrammar -> Val -> [((Fun,Int),Type)]
+funsOnType compat gr = funsOnTypeFs compat (funRulesOf gr)
+
+funsOnTypeFs :: (Val -> Type -> Bool) -> [(Fun,Type)] -> Val -> [((Fun,Int),Type)]
+funsOnTypeFs compat fs val = [((fun,i),typ) |
+ (fun,typ) <- fs,
+ Ok (args,_,_) <- [typeForm typ],
+ (i,arg) <- zip [0..] (map snd args),
+ compat val arg]
+
+
+-- this is needed at compile time
+
+lookupFunTypeSrc :: Grammar -> Ident -> Ident -> Err Type
+lookupFunTypeSrc gr m c = do
+ mi <- lookupModule gr m
+ case mi of
+ ModMod mo -> do
+ info <- lookupInfo mo c
+ case info of
+ AbsFun (Yes t) _ -> return t
+ AnyInd _ n -> lookupFunTypeSrc gr n c
+ _ -> prtBad "cannot find type of" c
+ _ -> Bad $ prt m +++ "is not an abstract module"
+
+lookupCatContextSrc :: Grammar -> Ident -> Ident -> Err Context
+lookupCatContextSrc gr m c = do
+ mi <- lookupModule gr m
+ case mi of
+ ModMod mo -> do
+ info <- lookupInfo mo c
+ case info of
+ AbsCat (Yes co) _ -> return co
+ AnyInd _ n -> lookupCatContextSrc gr n c
+ _ -> prtBad "unknown category" c
+ _ -> Bad $ prt m +++ "is not an abstract module"
diff --git a/src/GF/Grammar/Lookup.hs b/src/GF/Grammar/Lookup.hs
new file mode 100644
index 000000000..b8afbc21e
--- /dev/null
+++ b/src/GF/Grammar/Lookup.hs
@@ -0,0 +1,393 @@
+module Lookup where
+
+import Operations
+import Abstract
+import Modules
+
+import List (nub)
+import Monad
+
+-- lookup in resource and concrete in compiling; for abstract, use Look
+
+lookupResDef :: SourceGrammar -> Ident -> Ident -> Err Term
+lookupResDef gr m c = do
+ mi <- lookupModule gr m
+ case mi of
+ ModMod mo -> do
+ info <- lookupInfo mo c
+ case info of
+ ResOper _ (Yes t) -> return $ qualifAnnot m t
+ AnyInd _ n -> lookupResDef gr n c
+ ResParam _ -> return $ QC m c
+ ResValue _ -> return $ QC m c
+ _ -> Bad $ prt c +++ "is not defined in resource" +++ prt m
+ _ -> Bad $ prt m +++ "is not a resource"
+
+lookupResType :: SourceGrammar -> Ident -> Ident -> Err Type
+lookupResType gr m c = do
+ mi <- lookupModule gr m
+ case mi of
+ ModMod mo -> do
+ info <- lookupInfo mo c
+ case info of
+ ResOper (Yes t) _ -> return $ qualifAnnot m t
+ AnyInd _ n -> lookupResType gr n c
+ ResParam _ -> return $ typePType
+ ResValue (Yes t) -> return $ qualifAnnotPar m t
+ _ -> Bad $ prt c +++ "has no type defined in resource" +++ prt m
+ _ -> Bad $ prt m +++ "is not a resource"
+
+lookupParams :: SourceGrammar -> Ident -> Ident -> Err [Param]
+lookupParams gr m c = do
+ mi <- lookupModule gr m
+ case mi of
+ ModMod mo -> do
+ info <- lookupInfo mo c
+ case info of
+ ResParam (Yes ps) -> return ps
+ AnyInd _ n -> lookupParams gr n c
+ _ -> Bad $ prt c +++ "has no parameters defined in resource" +++ prt m
+ _ -> Bad $ prt m +++ "is not a resource"
+
+lookupParamValues :: SourceGrammar -> Ident -> Ident -> Err [Term]
+lookupParamValues gr m c = do
+ ps <- lookupParams gr m c
+ liftM concat $ mapM mkPar ps
+ where
+ mkPar (f,co) = do
+ vs <- liftM combinations $ mapM (\ (_,ty) -> allParamValues gr ty) co
+ return $ map (mkApp (QC m f)) vs
+
+lookupFirstTag :: SourceGrammar -> Ident -> Ident -> Err Term
+lookupFirstTag gr m c = do
+ vs <- lookupParamValues gr m c
+ case vs of
+ v:_ -> return v
+ _ -> prtBad "no parameter values given to type" c
+
+allParamValues :: SourceGrammar -> Type -> Err [Term]
+allParamValues cnc ptyp = case ptyp of
+ QC p c -> lookupParamValues cnc p c
+ RecType r -> do
+ let (ls,tys) = unzip r
+ tss <- mapM allPV tys
+ return [R (zipAssign ls ts) | ts <- combinations tss]
+ _ -> prtBad "cannot find parameter values for" ptyp
+ where
+ allPV = allParamValues cnc
+
+qualifAnnot :: Ident -> Term -> Term
+qualifAnnot _ = id
+-- Using this we wouldn't have to annotate constants defined in a module itself.
+-- But things are simpler if we do (cf. Zinc).
+-- Change Rename.self2status to change this behaviour.
+
+-- we need this for lookup in ResVal
+qualifAnnotPar m t = case t of
+ Cn c -> Q m c
+ Con c -> QC m c
+ _ -> composSafeOp (qualifAnnotPar m) t
+
+
+lookupLincat :: SourceGrammar -> Ident -> Ident -> Err Type
+lookupLincat gr m c = do
+ mi <- lookupModule gr m
+ case mi of
+ ModMod mo -> do
+ info <- lookupInfo mo c
+ case info of
+ CncCat (Yes t) _ _ -> return t
+ AnyInd _ n -> lookupLincat gr n c
+ _ -> Bad $ prt c +++ "has no linearization type in" +++ prt m
+ _ -> Bad $ prt m +++ "is not concrete"
+
+
+
+{-
+-- the type of oper may have to be inferred at TC, so it may be junk before it
+
+lookupResIdent :: Ident -> [(Ident, SourceRes)] -> Err (Term,Type)
+lookupResIdent c ms = case lookupWhich ms c of
+ Ok (i,info) -> case info of
+ ResOper (Yes t) _ -> return (Q i c, t)
+ ResOper _ _ -> return (Q i c, undefined) ----
+ ResParam _ -> return (Q i c, typePType)
+ ResValue (Yes t) -> return (QC i c, t)
+ _ -> Bad $ "not found in resource" +++ prt c
+
+-- NB we only have to look up cnc in canonical!
+
+-- you may want to strip the qualification if the module is the current one
+
+stripMod :: Ident -> Term -> Term
+stripMod m t = case t of
+ Q n c | n==m -> Cn c
+ QC n c | n==m -> Con c
+ _ -> t
+
+-- what you want may be a pattern and not a term. Then use Macros.term2patt
+
+
+
+
+-- an auxiliary for making ordered search through a list of modules
+
+lookups :: Ord i => (i -> m -> Err (Perhaps a m)) -> i -> [m] -> Err (Perhaps a m)
+lookups look c [] = Bad "not found in any module"
+lookups look c (m:ms) = case look c m of
+ Ok (Yes v) -> return $ Yes v
+ Ok (May m') -> look c m'
+ _ -> lookups look c ms
+
+
+lookupAbstract :: AbstractST -> Ident -> Err AbsInfo
+lookupAbstract g i = errIn ("not found in abstract" +++ prt i) $ lookupTree prt i g
+
+lookupFunsToCat :: AbstractST -> Ident -> Err [Fun]
+lookupFunsToCat g c = errIn ("looking up functions to category" +++ prt c) $ do
+ info <- lookupAbstract g c
+ case info of
+ AbsCat _ _ fs _ -> return fs
+ _ -> prtBad "not category" c
+
+allFunsWithValCat ab = [(f,c) | (c, AbsCat _ _ fs _) <- abstr2list ab, f <- fs]
+
+allDefs ab = [(f,d) | (f,AbsFun _ (Just d)) <- abstr2list ab]
+
+lookupCatContext :: AbstractST -> Ident -> Err Context
+lookupCatContext g c = errIn "context of category" $ do
+ info <- lookupAbstract g c
+ case info of
+ AbsCat c _ _ _ -> return c
+ _ -> prtBad "not category" c
+
+lookupFunType :: AbstractST -> Ident -> Err Term
+lookupFunType g c = errIn "looking up type of function" $ case c of
+ IL s -> lookupLiteral s >>= return . fst
+ _ -> do
+ info <- lookupAbstract g c
+ case info of
+ AbsFun t _ -> return t
+ AbsType t -> return typeType
+ _ -> prtBad "not function" c
+
+lookupFunArity :: AbstractST -> Ident -> Err Int
+lookupFunArity g c = do
+ typ <- lookupFunType g c
+ ctx <- contextOfType typ
+ return $ length ctx
+
+lookupAbsDef :: AbstractST -> Ident -> Err (Maybe Term)
+lookupAbsDef g c = errIn "looking up definition in abstract syntax" $ do
+ info <- lookupAbstract g c
+ case info of
+ AbsFun _ t -> return t
+ AbsType t -> return $ Just t
+ _ -> return $ Nothing -- constant found and accepted as primitive
+
+
+allCats :: AbstractST -> [Ident]
+allCats abstr = [c | (c, AbsCat _ _ _ _) <- abstr2list abstr]
+
+allIndepCats :: AbstractST -> [Ident]
+allIndepCats abstr = [c | (c, AbsCat [] _ _ _) <- abstr2list abstr]
+
+lookupConcrete :: ConcreteST -> Ident -> Err CncInfo
+lookupConcrete g i = errIn ("not found in concrete" +++ prt i) $ lookupTree prt i g
+
+lookupPackage :: ConcreteST -> Ident -> Err ([Ident], ConcreteST)
+lookupPackage g p = do
+ info <- lookupConcrete g p
+ case info of
+ CncPackage ps ins -> return (ps,ins)
+ _ -> prtBad "not package" p
+
+lookupInPackage :: ConcreteST -> (Ident,Ident) -> Err CncInfo
+lookupInPackage = lookupLift (flip (lookupTree prt))
+
+lookupInAll :: [BinTree (Ident,b)] -> Ident -> Err b
+lookupInAll = lookInAll (flip (lookupTree prt))
+
+lookInAll :: (BinTree (Ident,c) -> Ident -> Err b) ->
+ [BinTree (Ident,c)] -> Ident -> Err b
+lookInAll look ts c = case ts of
+ t : ts' -> err (const $ lookInAll look ts' c) return $ look t c
+ [] -> prtBad "not found in any package" c
+
+lookupLift :: (ConcreteST -> Ident -> Err b) ->
+ ConcreteST -> (Ident,Ident) -> Err b
+lookupLift look g (p,f) = do
+ (ps,ins) <- lookupPackage g p
+ ps' <- mapM (lookupPackage g) ps
+ lookInAll look (ins : reverse (map snd ps')) f
+
+termFromPackage :: ConcreteST -> Ident -> Term -> Err Term
+termFromPackage g p = termFP where
+ termFP t = case t of
+ Cn c -> return $ if isInPack c
+ then Q p c
+ else Cn c
+ T (TTyped t) cs -> do
+ t' <- termFP t
+ liftM (T (TTyped t')) $ mapM branchInPack cs
+ T i cs -> liftM (T i) $ mapM branchInPack cs
+ _ -> composOp termFP t
+ isInPack c = case lookupInPackage g (p,c) of
+ Ok _ -> True
+ _ -> False
+ branchInPack (q,t) = do
+ p' <- pattInPack q
+ t' <- termFP t
+ return (p',t')
+ pattInPack q = case q of
+ PC c ps -> do
+ let pc = if isInPack c
+ then PP p c
+ else PC c
+ ps' <- mapM pattInPack ps
+ return $ pc ps'
+ _ -> return q
+
+lookupCncDef :: ConcreteST -> Ident -> Err Term
+lookupCncDef g t@(IL _) = return $ cn t
+lookupCncDef g c = errIn "looking up defining term" $ do
+ info <- lookupConcrete g c
+ case info of
+ CncOper _ t _ -> return t -- the definition
+ CncCat t _ _ _ -> return t -- the linearization type
+ _ -> return $ Cn c -- constant found and accepted
+
+lookupOperDef :: ConcreteST -> Ident -> Err Term
+lookupOperDef g c = errIn "looking up defining term of oper" $ do
+ info <- lookupConcrete g c
+ case info of
+ CncOper _ t _ -> return t
+ _ -> prtBad "not oper" c
+
+lookupLincat :: ConcreteST -> Ident -> Err Term
+lookupLincat g c = return $ errVal defaultLinType $ do
+ info <- lookupConcrete g c
+ case info of
+ CncCat t _ _ _ -> return t
+ _ -> prtBad "not category" c
+
+lookupLindef :: ConcreteST -> Ident -> Err Term
+lookupLindef g c = return $ errVal linDefStr $ do
+ info <- lookupConcrete g c
+ case info of
+ CncCat _ (Just t) _ _ -> return t
+ CncCat _ _ _ _ -> return $ linDefStr --- wrong: this is only sof {s:Str}
+ _ -> prtBad "not category" c
+
+lookupLinType :: ConcreteST -> Ident -> Err Type
+lookupLinType g c = errIn "looking up type in concrete syntax" $ do
+ info <- lookupConcrete g c
+ case info of
+ CncParType _ _ _ -> return typeType
+ CncParam ty _ -> return ty
+ CncOper (Just ty) _ _ -> return ty
+ _ -> prtBad "no type found for" c
+
+lookupLin :: ConcreteST -> Ident -> Err Term
+lookupLin g c = errIn "looking up linearization rule" $ do
+ info <- lookupConcrete g c
+ case info of
+ CncFun t _ -> return t
+ _ -> prtBad "not category" c
+
+lookupFirstTag :: ConcreteST -> Ident -> Err Term
+lookupFirstTag g c = do
+ vs <- lookupParamValues g c
+ case vs of
+ v:_ -> return v
+ _ -> prtBad "empty parameter type" c
+
+lookupPrintname :: ConcreteST -> Ident -> Err String
+lookupPrintname g c = case lookupConcrete g c of
+ Ok info -> case info of
+ CncCat _ _ _ m -> mpr m
+ CncFun _ m -> mpr m
+ CncParType _ _ m -> mpr m
+ CncOper _ _ m -> mpr m
+ _ -> Bad "no possible printname"
+ Bad s -> Bad s
+ where
+ mpr = maybe (Bad "no printname") (return . stringFromTerm)
+
+-- this variant succeeds even if there's only abstr syntax
+lookupPrintname' g c = case lookupConcrete g c of
+ Bad _ -> return $ prt c
+ Ok info -> case info of
+ CncCat _ _ _ m -> mpr m
+ CncFun _ m -> mpr m
+ CncParType _ _ m -> mpr m
+ CncOper _ _ m -> mpr m
+ _ -> return $ prt c
+ where
+ mpr = return . maybe (prt c) stringFromTerm
+
+allOperDefs :: ConcreteST -> [(Ident,CncInfo)]
+allOperDefs cnc = [d | d@(_, CncOper _ _ _) <- concr2list cnc]
+
+allPackageDefs :: ConcreteST -> [(Ident,CncInfo)]
+allPackageDefs cnc = [d | d@(_, CncPackage _ _) <- concr2list cnc]
+
+allOperDependencies :: ConcreteST -> [(Ident,[Ident])]
+allOperDependencies cnc =
+ [(f, filter (/= f) $ -- package name may occur in the package itself
+ nub (concatMap (opersInCncInfo cnc f . snd) (tree2list ds))) |
+ (f, CncPackage _ ds) <- allPackageDefs cnc] ++
+ [(f, nub (opersInTerm cnc t)) |
+ (f, CncOper _ t _) <- allOperDefs cnc]
+
+opersInTerm :: ConcreteST -> Term -> [Ident]
+opersInTerm cnc t = case t of
+ Cn c -> [c | isOper c]
+ Q p c -> [p]
+ _ -> collectOp ops t
+ where
+ isOper (IL _) = False
+ isOper c = errVal False $ lookupOperDef cnc c >>= return . const True
+ ops = opersInTerm cnc
+
+-- this is used inside packages, to find references to outside the package
+opersInCncInfo :: ConcreteST -> Ident -> CncInfo -> [Ident]
+opersInCncInfo cnc p i = case i of
+ CncOper _ t _-> filter (not . internal) $ opersInTerm cnc t
+ _ -> []
+ where
+ internal c = case lookupInPackage cnc (p,c) of
+ Ok _ -> True
+ _ -> False
+
+opersUsedInLins :: ConcreteST -> [(Ident,[Ident])] -> [Ident]
+opersUsedInLins cnc deps = do
+ let ops0 = concat [opersInTerm cnc t | (_, CncFun t _) <- concr2list cnc]
+ nub $ closure ops0
+ where
+ closure ops = case [g | (f,fs) <- deps, elem f ops, g <- fs, notElem g ops] of
+ [] -> ops
+ ops' -> ops ++ closure ops'
+ -- presupposes deps are not circular: check this first!
+
+
+
+
+-- create refinement and wrapping lists
+
+
+varOrConst :: AbstractST -> Ident -> Err Term
+varOrConst abstr c = case lookupFunType abstr c of
+ Ok _ -> return $ Cn c --- bindings cannot overshadow constants
+ _ -> case c of
+ IL _ -> return $ Cn c
+ _ -> return $ Vr c
+
+-- a rename operation for parsing term input; for abstract syntax and parameters
+renameTrm :: (Ident -> Err a) -> Term -> Term
+renameTrm look = ren [] where
+ ren vars t = case t of
+ Vr x | notElem x vars && isNotError (look x) -> Cn x
+ Abs x b -> Abs x $ ren (x:vars) b
+ _ -> composSafeOp (ren vars) t
+-}
diff --git a/src/GF/Grammar/MMacros.hs b/src/GF/Grammar/MMacros.hs
new file mode 100644
index 000000000..4078221dc
--- /dev/null
+++ b/src/GF/Grammar/MMacros.hs
@@ -0,0 +1,261 @@
+module MMacros where
+
+import Operations
+import Zipper
+
+import Grammar
+import PrGrammar
+import Ident
+import Refresh
+import Values
+----import GrammarST
+import Macros
+
+import Monad
+
+-- some more abstractions on grammars, esp. for Edit
+
+nodeTree (Tr (n,_)) = n
+argsTree (Tr (_,ts)) = ts
+
+isFocusNode (N (_,_,_,_,b)) = b
+bindsNode (N (b,_,_,_,_)) = b
+atomNode (N (_,a,_,_,_)) = a
+valNode (N (_,_,v,_,_)) = v
+constrsNode (N (_,_,_,(c,_),_)) = c
+metaSubstsNode (N (_,_,_,(_,m),_)) = m
+
+atomTree = atomNode . nodeTree
+valTree = valNode . nodeTree
+
+mkNode binds atom vtyp cs = N (binds,atom,vtyp,cs,False)
+
+type Var = Ident
+type Meta = MetaSymb
+
+metasTree :: Tree -> [Meta]
+metasTree = concatMap metasNode . scanTree where
+ metasNode n = [m | AtM m <- [atomNode n]] ++ map fst (metaSubstsNode n)
+
+varsTree :: Tree -> [(Var,Val)]
+varsTree t = [(x,v) | N (_,AtV x,v,_,_) <- scanTree t]
+
+constrsTree :: Tree -> Constraints
+constrsTree = constrsNode . nodeTree
+
+allConstrsTree :: Tree -> Constraints
+allConstrsTree = concatMap constrsNode . scanTree
+
+changeConstrs :: (Constraints -> Constraints) -> TrNode -> TrNode
+changeConstrs f (N (b,a,v,(c,m),x)) = N (b,a,v,(f c, m),x)
+
+changeMetaSubst :: (MetaSubst -> MetaSubst) -> TrNode -> TrNode
+changeMetaSubst f (N (b,a,v,(c,m),x)) = N (b,a,v,(c, f m),x)
+
+changeAtom :: (Atom -> Atom) -> TrNode -> TrNode
+changeAtom f (N (b,a,v,(c,m),x)) = N (b,f a,v,(c, m),x)
+
+------ on the way to Edit
+
+uTree :: Tree
+uTree = Tr (uNode, []) -- unknown tree
+
+uNode :: TrNode
+uNode = mkNode [] uAtom uVal ([],[])
+
+
+uAtom :: Atom
+uAtom = AtM meta0
+
+mAtom :: Atom
+mAtom = AtM meta0
+
+uVal :: Val
+uVal = vClos uExp
+
+vClos :: Exp -> Val
+vClos = VClos []
+
+uExp :: Exp
+uExp = Meta meta0
+
+mExp :: Exp
+mExp = Meta meta0
+
+mExp0 = mExp
+
+meta2exp :: MetaSymb -> Exp
+meta2exp = Meta
+
+atomC = AtC
+
+funAtom :: Atom -> Err Fun
+funAtom a = case a of
+ AtC f -> return f
+ _ -> prtBad "not function head" a
+
+uBoundVar :: Ident
+uBoundVar = zIdent "#h" -- used for suppressed bindings
+
+atomIsMeta :: Atom -> Bool
+atomIsMeta atom = case atom of
+ AtM _ -> True
+ _ -> False
+
+getMetaAtom a = case a of
+ AtM m -> return m
+ _ -> Bad "the active node is not meta"
+
+cat2val :: Context -> Cat -> Val
+cat2val cont cat = vClos $ mkApp (qq cat) [mkMeta i | i <- [1..length cont]]
+
+val2cat :: Val -> Err Cat
+val2cat v = val2exp v >>= valCat
+
+substTerm :: [Ident] -> Substitution -> Term -> Term
+substTerm ss g c = case c of
+ Vr x -> maybe c id $ lookup x g
+ App f a -> App (substTerm ss g f) (substTerm ss g a)
+ Abs x b -> let y = mkFreshVarX ss x in
+ Abs y (substTerm (y:ss) ((x, Vr y):g) b)
+ Prod x a b -> let y = mkFreshVarX ss x in
+ Prod y (substTerm ss g a) (substTerm (y:ss) ((x,Vr y):g) b)
+ _ -> c
+
+metaSubstExp :: MetaSubst -> [(Meta,Exp)]
+metaSubstExp msubst = [(m, errVal (meta2exp m) (val2expSafe v)) | (m,v) <- msubst]
+
+-- belong here rather than to computation
+
+substitute :: [Var] -> Substitution -> Exp -> Err Exp
+substitute v s = return . substTerm v s
+
+alphaConv :: [Var] -> (Var,Var) -> Exp -> Err Exp ---
+alphaConv oldvars (x,x') = substitute (x:x':oldvars) [(x,Vr x')]
+
+alphaFresh :: [Var] -> Exp -> Err Exp
+alphaFresh vs = refreshTermN $ maxVarIndex vs
+
+alphaFreshAll :: [Var] -> [Exp] -> Err [Exp]
+alphaFreshAll vs = mapM $ alphaFresh vs -- done in a state monad
+
+
+val2exp = val2expP False -- for display
+val2expSafe = val2expP True -- for type checking
+
+val2expP :: Bool -> Val -> Err Exp
+val2expP safe v = case v of
+
+ VClos g@(_:_) e@(Meta _) -> if safe
+ then prtBad "unsafe value substitution" v
+ else substVal g e
+ VClos g e -> substVal g e
+ VApp f c -> liftM2 App (val2expP safe f) (val2expP safe c)
+ VCn c -> return $ qq c
+ VGen i x -> if safe
+ then prtBad "unsafe val2exp" v
+ else return $ vr $ x --- in editing, no alpha conversions presentv
+ where
+ substVal g e = mapPairsM (val2expP safe) g >>= return . (\s -> substTerm [] s e)
+
+isConstVal :: Val -> Bool
+isConstVal v = case v of
+ VApp f c -> isConstVal f && isConstVal c
+ VCn _ -> True
+ VClos [] e -> null $ freeVarsExp e
+ _ -> False --- could be more liberal
+
+mkProdVal :: Binds -> Val -> Err Val ---
+mkProdVal bs v = do
+ bs' <- mapPairsM val2exp bs
+ v' <- val2exp v
+ return $ vClos $ foldr (uncurry Prod) v' bs'
+
+freeVarsExp :: Exp -> [Ident]
+freeVarsExp e = case e of
+ Vr x -> [x]
+ App f c -> freeVarsExp f ++ freeVarsExp c
+ Abs x b -> filter (/=x) (freeVarsExp b)
+ Prod x a b -> freeVarsExp a ++ filter (/=x) (freeVarsExp b)
+ _ -> [] --- thus applies to abstract syntax only
+
+ident2string = prIdent
+
+tree :: (TrNode,[Tree]) -> Tree
+tree = Tr
+
+eqCat :: Cat -> Cat -> Bool
+eqCat = (==)
+
+addBinds :: Binds -> Tree -> Tree
+addBinds b (Tr (N (b0,at,t,c,x),ts)) = Tr (N (b ++ b0,at,t,c,x),ts)
+
+bodyTree :: Tree -> Tree
+bodyTree (Tr (N (_,a,t,c,x),ts)) = Tr (N ([],a,t,c,x),ts)
+
+refreshMetas :: [Meta] -> Exp -> Exp
+refreshMetas metas = fst . rms minMeta where
+ rms meta trm = case trm of
+ Meta m -> (Meta meta, nextMeta meta)
+ App f a -> let (f',msf) = rms meta f
+ (a',msa) = rms msf a
+ in (App f' a', msa)
+ Prod x a b ->
+ let (a',msa) = rms meta a
+ (b',msb) = rms msa b
+ in (Prod x a' b', msb)
+ Abs x b -> let (b',msb) = rms meta b in (Abs x b', msb)
+ _ -> (trm,meta)
+ minMeta = int2meta $
+ if null metas then 0 else (maximum (map metaSymbInt metas) + 1)
+
+ref2exp :: [Var] -> Type -> Ref -> Err Exp
+ref2exp bounds typ ref = do
+ cont <- contextOfType typ
+ xx0 <- mapM (typeSkeleton . snd) cont
+ let (xxs,cs) = unzip [(length hs, c) | (hs,c) <- xx0]
+ args = [mkAbs xs mExp | i <- xxs, let xs = mkFreshVars i bounds]
+ return $ mkApp ref args
+ -- no refreshment of metas
+
+type Ref = Exp -- invariant: only Con or Var
+
+fun2wrap :: [Var] -> ((Fun,Int),Type) -> Exp -> Err Exp
+fun2wrap oldvars ((fun,i),typ) exp = do
+ cont <- contextOfType typ
+ args <- mapM mkArg (zip [0..] (map snd cont))
+ return $ mkApp (qq fun) args
+ where
+ mkArg (n,c) = do
+ cont <- contextOfType c
+ let vars = mkFreshVars (length cont) oldvars
+ return $ mkAbs vars $ if n==i then exp else mExp
+
+---
+
+mkJustProd cont typ = mkProd (cont,typ,[])
+
+int2var :: Int -> Ident
+int2var = zIdent . ('$':) . show
+
+meta0 :: Meta
+meta0 = int2meta 0
+
+termMeta0 :: Term
+termMeta0 = Meta meta0
+
+identVar (Vr x) = return x
+identVar _ = Bad "not a variable"
+
+
+-- light-weight rename for user interaction
+
+qualifTerm :: Ident -> Term -> Term
+qualifTerm m = qualif [] where
+ qualif xs t = case t of
+ Abs x b -> Abs x $ qualif (x:xs) b
+ Prod x a b -> Prod x (qualif xs a) $ qualif (x:xs) b
+ Vr x | notElem x xs -> Q m x
+ Cn c -> Q m c
+ Con c -> QC m c
+ _ -> composSafeOp (qualif xs) t
diff --git a/src/GF/Grammar/Macros.hs b/src/GF/Grammar/Macros.hs
new file mode 100644
index 000000000..e6906f985
--- /dev/null
+++ b/src/GF/Grammar/Macros.hs
@@ -0,0 +1,634 @@
+module Macros where
+
+import Operations
+import Str
+import Grammar
+import Ident
+import PrGrammar
+
+import Monad (liftM)
+import Char (isDigit)
+
+-- AR 7/12/1999 - 9/5/2000 -- 4/6/2001
+
+-- operations on terms and types not involving lookup in or reference to grammars
+
+firstTypeForm :: Type -> Err (Context, Type)
+firstTypeForm t = case t of
+ Prod x a b -> do
+ (x', val) <- firstTypeForm b
+ return ((x,a):x',val)
+ _ -> return ([],t)
+
+qTypeForm :: Type -> Err (Context, Cat, [Term])
+qTypeForm t = case t of
+ Prod x a b -> do
+ (x', cat, args) <- qTypeForm b
+ return ((x,a):x', cat, args)
+ App c a -> do
+ (_,cat, args) <- qTypeForm c
+ return ([],cat,args ++ [a])
+ Q m c ->
+ return ([],(m,c),[])
+ QC m c ->
+ return ([],(m,c),[])
+ _ ->
+ prtBad "no normal form of type" t
+
+qq :: QIdent -> Term
+qq (m,c) = Q m c
+
+typeForm = qTypeForm ---- no need to dist any more
+
+typeFormCnc :: Type -> Err (Context, Type)
+typeFormCnc t = case t of
+ Prod x a b -> do
+ (x', v) <- typeFormCnc b
+ return ((x,a):x',v)
+ _ -> return ([],t)
+
+valCat :: Type -> Err Cat
+valCat typ =
+ do (_,cat,_) <- typeForm typ
+ return cat
+
+valType :: Type -> Err Type
+valType typ =
+ do (_,cat,xx) <- typeForm typ --- not optimal to do in this way
+ return $ mkApp (qq cat) xx
+
+valTypeCnc :: Type -> Err Type
+valTypeCnc typ =
+ do (_,ty) <- typeFormCnc typ
+ return ty
+
+typeRawSkeleton :: Type -> Err ([(Int,Type)],Type)
+typeRawSkeleton typ =
+ do (cont,typ) <- typeFormCnc typ
+ args <- mapM (typeRawSkeleton . snd) cont
+ return ([(length c, v) | (c,v) <- args], typ)
+
+type MCat = (Ident,Ident)
+
+sortMCat :: String -> MCat
+sortMCat s = (zIdent "_", zIdent s)
+
+getMCat :: Term -> Err MCat
+getMCat t = case t of
+ Q m c -> return (m,c)
+ QC m c -> return (m,c)
+ Sort s -> return $ sortMCat s
+ App f _ -> getMCat f
+ _ -> prtBad "no qualified constant" t
+
+typeSkeleton :: Type -> Err ([(Int,MCat)],MCat)
+typeSkeleton typ = do
+ (cont,val) <- typeRawSkeleton typ
+ cont' <- mapPairsM getMCat cont
+ val' <- getMCat val
+ return (cont',val')
+
+catSkeleton :: Type -> Err ([MCat],MCat)
+catSkeleton typ =
+ do (args,val) <- typeSkeleton typ
+ return (map snd args, val)
+
+funsToAndFrom :: Type -> (MCat, [(MCat,[Int])])
+funsToAndFrom t = errVal undefined $ do ---
+ (cs,v) <- catSkeleton t
+ let cis = zip cs [0..]
+ return $ (v, [(c,[i | (c',i) <- cis, c' == c]) | c <- cs])
+
+typeFormConcrete :: Type -> Err (Context, Type)
+typeFormConcrete t = case t of
+ Prod x a b -> do
+ (x', typ) <- typeFormConcrete b
+ return ((x,a):x', typ)
+ _ -> return ([],t)
+
+isRecursiveType :: Type -> Bool
+isRecursiveType t = errVal False $ do
+ (cc,c) <- catSkeleton t -- thus recursivity on Cat level
+ return $ any (== c) cc
+
+
+contextOfType :: Type -> Err Context
+contextOfType typ = case typ of
+ Prod x a b -> liftM ((x,a):) $ contextOfType b
+ _ -> return []
+
+unComputed :: Term -> Term
+unComputed t = case t of
+ Computed v -> unComputed v
+ _ -> t --- composSafeOp unComputed t
+
+computed = Computed
+
+termForm :: Term -> Err ([(Ident)], Term, [Term])
+termForm t = case t of
+ Abs x b ->
+ do (x', fun, args) <- termForm b
+ return (x:x', fun, args)
+ App c a ->
+ do (_,fun, args) <- termForm c
+ return ([],fun,args ++ [a])
+ _ ->
+ return ([],t,[])
+
+appForm :: Term -> (Term, [Term])
+appForm t = case t of
+ App c a -> (fun, args ++ [a]) where (fun, args) = appForm c
+ _ -> (t,[])
+
+varsOfType :: Type -> [Ident]
+varsOfType t = case t of
+ Prod x _ b -> x : varsOfType b
+ _ -> []
+
+mkProdSimple :: Context -> Term -> Term
+mkProdSimple c t = mkProd (c,t,[])
+
+mkProd :: (Context, Term, [Term]) -> Term
+mkProd ([],typ,args) = mkApp typ args
+mkProd ((x,a):dd, typ, args) = Prod x a (mkProd (dd, typ, args))
+
+mkTerm :: ([(Ident)], Term, [Term]) -> Term
+mkTerm (xx,t,aa) = mkAbs xx (mkApp t aa)
+
+mkApp :: Term -> [Term] -> Term
+mkApp = foldl App
+
+mkAbs :: [Ident] -> Term -> Term
+mkAbs xx t = foldr Abs t xx
+
+appCons :: Ident -> [Term] -> Term
+appCons = mkApp . Cn
+
+appc :: String -> [Term] -> Term
+appc = appCons . zIdent
+
+mkLet :: [LocalDef] -> Term -> Term
+mkLet defs t = foldr Let t defs
+
+isVariable (Vr _ ) = True
+isVariable _ = False
+
+eqIdent :: Ident -> Ident -> Bool
+eqIdent = (==)
+
+zIdent :: String -> Ident
+zIdent s = identC s
+
+uType :: Type
+uType = Cn (zIdent "UndefinedType")
+
+assign :: Label -> Term -> Assign
+assign l t = (l,(Nothing,t))
+
+assignT :: Label -> Type -> Term -> Assign
+assignT l a t = (l,(Just a,t))
+
+unzipR :: [Assign] -> ([Label],[Term])
+unzipR r = (ls, map snd ts) where (ls,ts) = unzip r
+
+mkAssign :: [(Label,Term)] -> [Assign]
+mkAssign lts = [assign l t | (l,t) <- lts]
+
+zipAssign :: [Label] -> [Term] -> [Assign]
+zipAssign ls ts = [assign l t | (l,t) <- zip ls ts]
+
+ident2label :: Ident -> Label
+ident2label c = LIdent (prIdent c)
+
+label2ident :: Label -> Ident
+label2ident = identC . prLabel
+
+prLabel :: Label -> String
+prLabel = prt
+
+mapAssignM :: Monad m => (Term -> m c) -> [Assign] -> m [(Label,(Maybe c,c))]
+mapAssignM f ltvs = do
+ let (ls,tvs) = unzip ltvs
+ (ts, vs) = unzip tvs
+ ts' <- mapM (\t -> case t of
+ Nothing -> return Nothing
+ Just y -> f y >>= return . Just) ts
+ vs' <- mapM f vs
+ return (zip ls (zip ts' vs'))
+
+mkRecordN :: Int -> (Int -> Label) -> [Term] -> Term
+mkRecordN int lab typs = R [ assign (lab i) t | (i,t) <- zip [int..] typs]
+
+mkRecord :: (Int -> Label) -> [Term] -> Term
+mkRecord = mkRecordN 0
+
+mkRecTypeN :: Int -> (Int -> Label) -> [Type] -> Type
+mkRecTypeN int lab typs = RecType [ (lab i, t) | (i,t) <- zip [int..] typs]
+
+mkRecType :: (Int -> Label) -> [Type] -> Type
+mkRecType = mkRecTypeN 0
+
+typeType = srt "Type"
+typePType = srt "PType"
+typeStr = srt "Str"
+typeTok = srt "Tok"
+typeStrs = srt "Strs"
+
+typeString = constPredefRes "String"
+typeInt = constPredefRes "Int"
+
+constPredefRes s = Q (IC "Predef") (zIdent s)
+
+isPredefConstant t = case t of
+ Q (IC "Predef") _ -> True
+ _ -> False
+
+mkSelects :: Term -> [Term] -> Term
+mkSelects t tt = foldl S t tt
+
+mkTable :: [Term] -> Term -> Term
+mkTable tt t = foldr Table t tt
+
+mkCTable :: [Ident] -> Term -> Term
+mkCTable ids v = foldr ccase v ids where
+ ccase x t = T TRaw [(PV x,t)]
+
+mkDecl :: Term -> Decl
+mkDecl typ = (wildIdent, typ)
+
+eqStrIdent :: Ident -> Ident -> Bool
+eqStrIdent = (==)
+
+tupleLabel i = LIdent $ "p" ++ show i
+linLabel i = LIdent $ "s" ++ show i
+
+tuple2record :: [Term] -> [Assign]
+tuple2record ts = [assign (tupleLabel i) t | (i,t) <- zip [1..] ts]
+
+tuple2recordType :: [Term] -> [Labelling]
+tuple2recordType ts = [(tupleLabel i, t) | (i,t) <- zip [1..] ts]
+
+tuple2recordPatt :: [Patt] -> [(Label,Patt)]
+tuple2recordPatt ts = [(tupleLabel i, t) | (i,t) <- zip [1..] ts]
+
+mkCases :: Ident -> Term -> Term
+mkCases x t = T TRaw [(PV x, t)]
+
+mkWildCases :: Term -> Term
+mkWildCases = mkCases wildIdent
+
+mkFunType :: [Type] -> Type -> Type
+mkFunType tt t = mkProd ([(wildIdent, ty) | ty <- tt], t, []) -- nondep prod
+
+plusRecType :: Type -> Type -> Err Type
+plusRecType t1 t2 = case (unComputed t1, unComputed t2) of
+ (RecType r1, RecType r2) -> return (RecType (r1 ++ r2))
+ _ -> Bad ("cannot add record types" +++ prt t1 +++ "and" +++ prt t2)
+
+plusRecord :: Term -> Term -> Err Term
+plusRecord t1 t2 =
+ case (t1,t2) of
+ (R r1, R r2 ) -> return (R (r1 ++ r2))
+ (_, FV rs) -> mapM (plusRecord t1) rs >>= return . FV
+ (FV rs,_ ) -> mapM (`plusRecord` t2) rs >>= return . FV
+ _ -> Bad ("cannot add records" +++ prt t1 +++ "and" +++ prt t2)
+
+-- default linearization type
+
+defLinType = RecType [(LIdent "s", typeStr)]
+
+-- refreshing variables
+
+varX :: Int -> Ident
+varX i = identV (i,"x")
+
+mkFreshVar :: [Ident] -> Ident
+mkFreshVar olds = varX (maxVarIndex olds + 1)
+
+-- trying to preserve a given symbol
+mkFreshVarX :: [Ident] -> Ident -> Ident
+mkFreshVarX olds x = if (elem x olds) then (varX (maxVarIndex olds + 1)) else x
+
+maxVarIndex :: [Ident] -> Int
+maxVarIndex = maximum . ((-1):) . map varIndex
+
+mkFreshVars :: Int -> [Ident] -> [Ident]
+mkFreshVars n olds = [varX (maxVarIndex olds + i) | i <- [1..n]]
+
+--- quick hack for refining with var in editor
+freshAsTerm :: String -> Term
+freshAsTerm s = Vr (varX (readIntArg s))
+
+-- create a terminal for concrete syntax
+string2term :: String -> Term
+string2term = ccK
+
+ccK = K
+ccC = C
+
+-- create a terminal from identifier
+ident2terminal :: Ident -> Term
+ident2terminal = ccK . prIdent
+
+-- create a constant
+string2CnTrm :: String -> Term
+string2CnTrm = Cn . zIdent
+
+symbolOfIdent :: Ident -> String
+symbolOfIdent = prIdent
+
+symid = symbolOfIdent
+
+vr = Vr
+cn = Cn
+srt = Sort
+meta = Meta
+cnIC = cn . IC
+
+justIdentOf (Vr x) = Just x
+justIdentOf (Cn x) = Just x
+justIdentOf _ = Nothing
+
+isMeta (Meta _) = True
+isMeta _ = False
+mkMeta = Meta . MetaSymb
+
+nextMeta :: MetaSymb -> MetaSymb
+nextMeta = int2meta . succ . metaSymbInt
+
+int2meta = MetaSymb
+
+metaSymbInt :: MetaSymb -> Int
+metaSymbInt (MetaSymb k) = k
+
+freshMeta :: [MetaSymb] -> MetaSymb
+freshMeta ms = MetaSymb (minimum [n | n <- [0..length ms],
+ notElem n (map metaSymbInt ms)])
+
+mkFreshMetasInTrm :: [MetaSymb] -> Trm -> Trm
+mkFreshMetasInTrm metas = fst . rms minMeta where
+ rms meta trm = case trm of
+ Meta m -> (Meta (MetaSymb meta), meta + 1)
+ App f a -> let (f',msf) = rms meta f
+ (a',msa) = rms msf a
+ in (App f' a', msa)
+ Prod x a b ->
+ let (a',msa) = rms meta a
+ (b',msb) = rms msa b
+ in (Prod x a' b', msb)
+ Abs x b -> let (b',msb) = rms meta b in (Abs x b', msb)
+ _ -> (trm,meta)
+ minMeta = if null metas then 0 else (maximum (map metaSymbInt metas) + 1)
+
+-- decides that a term has no metavariables
+isCompleteTerm :: Term -> Bool
+isCompleteTerm t = case t of
+ Meta _ -> False
+ Abs _ b -> isCompleteTerm b
+ App f a -> isCompleteTerm f && isCompleteTerm a
+ _ -> True
+
+linTypeStr :: Type
+linTypeStr = mkRecType linLabel [typeStr] -- default lintype {s :: Str}
+
+linAsStr :: String -> Term
+linAsStr s = mkRecord linLabel [K s] -- default linearization {s = s}
+
+linDefStr :: Term
+linDefStr = Abs s (R [assign (linLabel 0) (Vr s)]) where s = zIdent "s"
+
+term2patt :: Term -> Err Patt
+term2patt trm = case termForm trm of
+ Ok ([], Vr x, []) -> return (PV x)
+ Ok ([], Con c, aa) -> do
+ aa' <- mapM term2patt aa
+ return (PC c aa')
+ Ok ([], QC p c, aa) -> do
+ aa' <- mapM term2patt aa
+ return (PP p c aa')
+ Ok ([], R r, []) -> do
+ let (ll,aa) = unzipR r
+ aa' <- mapM term2patt aa
+ return (PR (zip ll aa'))
+ Ok ([],EInt i,[]) -> return $ PInt i
+ Ok ([],K s, []) -> return $ PString s
+ _ -> prtBad "no pattern corresponds to term" trm
+
+patt2term :: Patt -> Term
+patt2term pt = case pt of
+ PV x -> Vr x
+ PW -> Vr wildIdent --- not parsable, should not occur
+ PC c pp -> mkApp (Con c) (map patt2term pp)
+ PP p c pp -> mkApp (QC p c) (map patt2term pp)
+ PR r -> R [assign l (patt2term p) | (l,p) <- r]
+ PT _ p -> patt2term p
+ PInt i -> EInt i
+ PString s -> K s
+
+-- to gather s-fields; assumes term in normal form, preserves label
+allLinFields :: Term -> Err [[(Label,Term)]]
+allLinFields trm = case unComputed trm of
+---- R rs -> return [[(l,t) | (l,(Just ty,t)) <- rs, isStrType ty]] -- good
+ R rs -> return [[(l,t) | (l,(_,t)) <- rs, isLinLabel l]] ---- bad
+ FV ts -> do
+ lts <- mapM allLinFields ts
+ return $ concat lts
+ _ -> prtBad "fields can only be sought in a record not in" trm
+
+---- deprecated
+isLinLabel l = case l of
+ LIdent ('s':cs) | all isDigit cs -> True
+ _ -> False
+
+-- to gather ultimate cases in a table; preserves pattern list
+allCaseValues :: Term -> [([Patt],Term)]
+allCaseValues trm = case unComputed trm of
+ T _ cs -> [(p:ps, t) | (p,t0) <- cs, (ps,t) <- allCaseValues t0]
+ _ -> [([],trm)]
+
+-- to gather all linearizations; assumes normal form, preserves label and args
+allLinValues :: Term -> Err [[(Label,[([Patt],Term)])]]
+allLinValues trm = do
+ lts <- allLinFields trm
+ mapM (mapPairsM (return . allCaseValues)) lts
+
+-- to mark str parts of fields in a record f by a function f
+markLinFields :: (Term -> Term) -> Term -> Term
+markLinFields f t = case t of
+ R r -> R $ map mkField r
+ _ -> t
+ where
+ mkField (l,(_,t)) = if (isLinLabel l) then (assign l (mkTbl t)) else (assign l t)
+ mkTbl t = case t of
+ T i cs -> T i [(p, mkTbl v) | (p,v) <- cs]
+ _ -> f t
+
+-- to get a string from a term that represents a sequence of terminals
+strsFromTerm :: Term -> Err [Str]
+strsFromTerm t = case unComputed t of
+ K s -> return [str s]
+ C s t -> do
+ s' <- strsFromTerm s
+ t' <- strsFromTerm t
+ return [plusStr x y | x <- s', y <- t']
+ Glue s t -> do
+ s' <- strsFromTerm s
+ t' <- strsFromTerm t
+ return [glueStr x y | x <- s', y <- t']
+ Alts (d,vs) -> do
+ d0 <- strsFromTerm d
+ v0 <- mapM (strsFromTerm . fst) vs
+ c0 <- mapM (strsFromTerm . snd) vs
+ let vs' = zip v0 c0
+ return [strTok (str2strings def) vars |
+ def <- d0,
+ vars <- [[(str2strings v, map sstr c) | (v,c) <- zip vv c0] |
+ vv <- combinations v0]
+ ]
+ FV ts -> mapM strsFromTerm ts >>= return . concat
+ Strs ts -> mapM strsFromTerm ts >>= return . concat
+ Ready ss -> return [ss]
+ Alias _ _ d -> strsFromTerm d --- should not be needed...
+ _ -> prtBad "cannot get Str from term" t
+
+-- to print an Str-denoting term as a string; if the term is of wrong type, the error msg
+stringFromTerm :: Term -> String
+stringFromTerm = err id (ifNull "" (sstr . head)) . strsFromTerm
+
+
+-- to define compositional term functions
+
+composSafeOp :: (Term -> Term) -> Term -> Term
+composSafeOp op trm = case composOp (mkMonadic op) trm of
+ Ok t -> t
+ _ -> error "the operation is safe isn't it ?"
+ where
+ mkMonadic f = return . f
+
+composOp :: Monad m => (Term -> m Term) -> Term -> m Term
+composOp co trm =
+ case trm of
+ App c a ->
+ do c' <- co c
+ a' <- co a
+ return (App c' a')
+ Abs x b ->
+ do b' <- co b
+ return (Abs x b')
+ Prod x a b ->
+ do a' <- co a
+ b' <- co b
+ return (Prod x a' b')
+ S c a ->
+ do c' <- co c
+ a' <- co a
+ return (S c' a')
+ Table a c ->
+ do a' <- co a
+ c' <- co c
+ return (Table a' c')
+ R r ->
+ do r' <- mapAssignM co r
+ return (R r')
+ RecType r ->
+ do r' <- mapPairListM (co . snd) r
+ return (RecType r')
+ P t i ->
+ do t' <- co t
+ return (P t' i)
+ ExtR a c ->
+ do a' <- co a
+ c' <- co c
+ return (ExtR a' c')
+
+ T i cc ->
+ do cc' <- mapPairListM (co . snd) cc
+ i' <- changeTableType co i
+ return (T i' cc')
+ Let (x,(mt,a)) b ->
+ do a' <- co a
+ mt' <- case mt of
+ Just t -> co t >>= (return . Just)
+ _ -> return mt
+ b' <- co b
+ return (Let (x,(mt',a')) b')
+ Alias c ty d ->
+ do v <- co d
+ ty' <- co ty
+ return $ Alias c ty' v
+ C s1 s2 ->
+ do v1 <- co s1
+ v2 <- co s2
+ return (C v1 v2)
+ Glue s1 s2 ->
+ do v1 <- co s1
+ v2 <- co s2
+ return (Glue v1 v2)
+ Alts (t,aa) ->
+ do t' <- co t
+ aa' <- mapM (pairM co) aa
+ return (Alts (t',aa'))
+ FV ts -> mapM co ts >>= return . FV
+ Strs tt -> mapM co tt >>= return . Strs
+ _ -> return trm -- covers K, Vr, Cn, Sort
+
+getTableType :: TInfo -> Err Type
+getTableType i = case i of
+ TTyped ty -> return ty
+ TComp ty -> return ty
+ TWild ty -> return ty
+ _ -> Bad "the table is untyped"
+
+changeTableType :: Monad m => (Type -> m Type) -> TInfo -> m TInfo
+changeTableType co i = case i of
+ TTyped ty -> co ty >>= return . TTyped
+ TComp ty -> co ty >>= return . TComp
+ TWild ty -> co ty >>= return . TWild
+ _ -> return i
+
+collectOp :: (Term -> [a]) -> Term -> [a]
+collectOp co trm = case trm of
+ App c a -> co c ++ co a
+ Abs _ b -> co b
+ Prod _ a b -> co a ++ co b
+ S c a -> co c ++ co a
+ Table a c -> co a ++ co c
+ ExtR a c -> co a ++ co c
+ R r -> concatMap (\ (_,(mt,a)) -> maybe [] co mt ++ co a) r
+ RecType r -> concatMap (co . snd) r
+ P t i -> co t
+ T _ cc -> concatMap (co . snd) cc -- not from patterns --- nor from type annot
+ Let (x,(mt,a)) b -> maybe [] co mt ++ co a ++ co b
+ C s1 s2 -> co s1 ++ co s2
+ Glue s1 s2 -> co s1 ++ co s2
+ Alts (t,aa) -> let (x,y) = unzip aa in co t ++ concatMap co (x ++ y)
+ FV ts -> concatMap co ts
+ Strs tt -> concatMap co tt
+ _ -> [] -- covers K, Vr, Cn, Sort, Ready
+
+-- to find the word items in a term
+
+wordsInTerm :: Term -> [String]
+wordsInTerm trm = filter (not . null) $ case trm of
+ K s -> [s]
+ S c _ -> wo c
+ Alts (t,aa) -> wo t ++ concatMap (wo . fst) aa
+ Ready s -> allItems s
+ _ -> collectOp wo trm
+ where wo = wordsInTerm
+
+noExist = FV []
+
+defaultLinType :: Type
+defaultLinType = mkRecType linLabel [typeStr]
+
+metaTerms :: [Term]
+metaTerms = map (Meta . MetaSymb) [0..]
+
+-- from GF1, 20/9/2003
+
+isInOneType :: Type -> Bool
+isInOneType t = case t of
+ Prod _ a b -> a == b
+ _ -> False
+
diff --git a/src/GF/Grammar/PatternMatch.hs b/src/GF/Grammar/PatternMatch.hs
new file mode 100644
index 000000000..2ca8b21de
--- /dev/null
+++ b/src/GF/Grammar/PatternMatch.hs
@@ -0,0 +1,98 @@
+module PatternMatch where
+
+import Operations
+import Grammar
+import Ident
+import Macros
+import PrGrammar
+
+import List
+import Monad
+
+-- pattern matching for both concrete and abstract syntax. AR -- 16/6/2003
+
+
+matchPattern :: [(Patt,Term)] -> Term -> Err (Term, Substitution)
+matchPattern pts term =
+ errIn ("trying patterns" +++ unwords (intersperse "," (map (prt . fst) pts))) $
+ findMatch [([p],t) | (p,t) <- pts] [term]
+
+testOvershadow :: [Patt] -> [Term] -> Err [Patt]
+testOvershadow pts vs = do
+ let numpts = zip pts [0..]
+ let cases = [(p,EInt i) | (p,i) <- numpts]
+ ts <- mapM (liftM fst . matchPattern cases) vs
+ return $ [p | (p,i) <- numpts, notElem i [i | EInt i <- ts] ]
+
+findMatch :: [([Patt],Term)] -> [Term] -> Err (Term, Substitution)
+findMatch cases terms = case cases of
+ [] -> Bad $"no applicable case for" +++ unwords (intersperse "," (map prt terms))
+ (patts,_):_ | length patts /= length terms ->
+ Bad ("wrong number of args for patterns :" +++
+ unwords (map prt patts) +++ "cannot take" +++ unwords (map prt terms))
+ (patts,val):cc -> case mapM tryMatch (zip patts terms) of
+ Ok substs -> return (val, concat substs)
+ _ -> findMatch cc terms
+
+tryMatch :: (Patt, Term) -> Err [(Ident, Term)]
+tryMatch (p,t) = do
+ t' <- termForm t
+ trym p t'
+ where
+ trym p t' =
+ case (p,t') of
+ (PV IW, _) | isInConstantForm t -> return [] -- optimization with wildcard
+ (PV x, _) | isInConstantForm t -> return [(x,t)]
+ (PString s, ([],K i,[])) | s==i -> return []
+ (PInt s, ([],EInt i,[])) | s==i -> return []
+ (PC p pp, ([], Con f, tt)) |
+ p `eqStrIdent` f && length pp == length tt ->
+ do matches <- mapM tryMatch (zip pp tt)
+ return (concat matches)
+ (PP q p pp, ([], QC r f, tt)) |
+ q `eqStrIdent` r && p `eqStrIdent` f && length pp == length tt ->
+ do matches <- mapM tryMatch (zip pp tt)
+ return (concat matches)
+ ---- hack for AppPredef bug
+ (PP q p pp, ([], Q r f, tt)) |
+ q `eqStrIdent` r && p `eqStrIdent` f && length pp == length tt ->
+ do matches <- mapM tryMatch (zip pp tt)
+ return (concat matches)
+
+ (PR r, ([],R r',[])) |
+ all (`elem` map fst r') (map fst r) ->
+ do matches <- mapM tryMatch
+ [(p,snd a) | (l,p) <- r, let Just a = lookup l r']
+ return (concat matches)
+ (PT _ p',_) -> trym p' t'
+ (_, ([],Alias _ _ d,[])) -> tryMatch (p,d)
+ _ -> prtBad "no match in case expr for" t
+
+isInConstantForm :: Term -> Bool
+isInConstantForm trm = case trm of
+ Cn _ -> True
+ Con _ -> True
+ Q _ _ -> True
+ QC _ _ -> True
+ Abs _ _ -> True
+ App c a -> isInConstantForm c && isInConstantForm a
+ R r -> all (isInConstantForm . snd . snd) r
+ Alias _ _ t -> isInConstantForm t
+ _ -> False ---- isInArgVarForm trm
+
+varsOfPatt :: Patt -> [Ident]
+varsOfPatt p = case p of
+ PV x -> [x | not (isWildIdent x)]
+ PC _ ps -> concat $ map varsOfPatt ps
+ PP _ _ ps -> concat $ map varsOfPatt ps
+ PR r -> concat $ map (varsOfPatt . snd) r
+ PT _ q -> varsOfPatt q
+ _ -> []
+
+-- to search matching parameter combinations in tables
+isMatchingForms :: [Patt] -> [Term] -> Bool
+isMatchingForms ps ts = all match (zip ps ts') where
+ match (PC c cs, (Cn d, ds)) = c == d && isMatchingForms cs ds
+ match _ = True
+ ts' = map appForm ts
+
diff --git a/src/GF/Grammar/PrGrammar.hs b/src/GF/Grammar/PrGrammar.hs
new file mode 100644
index 000000000..03197ea02
--- /dev/null
+++ b/src/GF/Grammar/PrGrammar.hs
@@ -0,0 +1,189 @@
+module PrGrammar where
+
+import Operations
+import Zipper
+import Grammar
+import Modules
+import qualified PrintGF as P
+import qualified PrintGFC as C
+import qualified AbsGFC as A
+import Values
+import GrammarToSource
+import Ident
+import Str
+
+import List (intersperse)
+
+-- AR 7/12/1999 - 1/4/2000 - 10/5/2003
+
+-- printing and prettyprinting class
+
+class Print a where
+ prt :: a -> String
+ prt2 :: a -> String -- printing with parentheses, if needed
+ prpr :: a -> [String] -- pretty printing
+ prt_ :: a -> String -- printing without ident qualifications
+ prt2 = prt
+ prt_ = prt
+ prpr = return . prt
+
+-- to show terms etc in error messages
+prtBad :: Print a => String -> a -> Err b
+prtBad s a = Bad (s +++ prt a)
+
+prGrammar = P.printTree . trGrammar
+prModule = P.printTree . trModule
+
+instance Print Term where
+ prt = P.printTree . trt
+ prt_ = prExp
+
+instance Print Ident where
+ prt = P.printTree . tri
+
+instance Print Patt where
+ prt = P.printTree . trp
+
+instance Print Label where
+ prt = P.printTree . trLabel
+
+instance Print MetaSymb where
+ prt (MetaSymb i) = "?" ++ show i
+
+prParam :: Param -> String
+prParam (c,co) = prt c +++ prContext co
+
+prContext :: Context -> String
+prContext co = unwords $ map prParenth [prt x +++ ":" +++ prt t | (x,t) <- co]
+
+-- some GFC notions
+
+instance Print A.Exp where prt = C.printTree
+instance Print A.Term where prt = C.printTree
+instance Print A.Patt where prt = C.printTree
+instance Print A.Case where prt = C.printTree
+instance Print A.Atom where prt = C.printTree
+instance Print A.CIdent where prt = C.printTree
+instance Print A.CType where prt = C.printTree
+instance Print A.Label where prt = C.printTree
+instance Print A.Module where prt = C.printTree
+instance Print A.Sort where prt = C.printTree
+
+
+-- printing values and trees in editing
+
+instance Print a => Print (Tr a) where
+ prt (Tr (n, trees)) = prt n +++ unwords (map prt2 trees)
+ prt2 t@(Tr (_,args)) = if null args then prt t else prParenth (prt t)
+
+-- we cannot define the method prt_ in this way
+prt_Tree :: Tree -> String
+prt_Tree = prt_ . tree2exp
+
+instance Print TrNode where
+ prt (N (bi,at,vt,(cs,ms),_)) =
+ prBinds bi ++
+ prt at +++ ":" +++ prt vt
+ +++ prConstraints cs +++ prMetaSubst ms
+
+prMarkedTree :: Tr (TrNode,Bool) -> [String]
+prMarkedTree = prf 1 where
+ prf ind t@(Tr (node, trees)) =
+ prNode ind node : concatMap (prf (ind + 2)) trees
+ prNode ind node = case node of
+ (n, False) -> indent ind (prt n)
+ (n, _) -> '*' : indent (ind - 1) (prt n)
+
+prTree :: Tree -> [String]
+prTree = prMarkedTree . mapTr (\n -> (n,False))
+
+--- to get rig of brackets
+prRefinement :: Term -> String
+prRefinement t = case t of
+ Q m c -> prQIdent (m,c)
+ QC m c -> prQIdent (m,c)
+ _ -> prt t
+
+-- a pretty-printer for parsable output
+tree2string = unlines . prprTree
+
+prprTree :: Tree -> [String]
+prprTree = prf False where
+ prf par t@(Tr (node, trees)) =
+ parIf par (prn node : concat [prf (ifPar t) t | t <- trees])
+ prn (N (bi,at,_,_,_)) = prb bi ++ prt at
+ prb [] = ""
+ prb bi = "\\" ++ concat (intersperse "," (map (prt . fst) bi)) ++ " -> "
+ parIf par (s:ss) = map (indent 2) $
+ if par
+ then ('(':s) : ss ++ [")"]
+ else s:ss
+ ifPar (Tr (N ([],_,_,_,_), [])) = False
+ ifPar _ = True
+
+
+-- auxiliaries
+
+prConstraints :: Constraints -> String
+prConstraints = concat . prConstrs
+
+prMetaSubst :: MetaSubst -> String
+prMetaSubst = concat . prMSubst
+
+prEnv :: Env -> String
+---- prEnv [] = prCurly "" ---- for debugging
+prEnv e = concatMap (\ (x,t) -> prCurly (prt x ++ ":=" ++ prt t)) e
+
+prConstrs :: Constraints -> [String]
+prConstrs = map (\ (v,w) -> prCurly (prt v ++ "<>" ++ prt w))
+
+prMSubst :: MetaSubst -> [String]
+prMSubst = map (\ (m,e) -> prCurly ("?" ++ show m ++ "=" ++ prt e))
+
+prBinds bi = if null bi
+ then []
+ else "\\" ++ concat (intersperse "," (map prValDecl bi)) +++ "-> "
+ where
+ prValDecl (x,t) = prParenth (prt x +++ ":" +++ prt t)
+
+instance Print Val where
+ prt (VGen i x) = prt x ---- ++ "-$" ++ show i ---- latter part for debugging
+ prt (VApp u v) = prt u +++ prv1 v
+ prt (VCn mc) = prQIdent mc
+ prt (VClos env e) = case e of
+ Meta _ -> prt e ++ prEnv env
+ _ -> prt e ---- ++ prEnv env ---- for debugging
+
+prv1 v = case v of
+ VApp _ _ -> prParenth $ prt v
+ VClos _ _ -> prParenth $ prt v
+ _ -> prt v
+
+instance Print Atom where
+ prt (AtC f) = prQIdent f
+ prt (AtM i) = prt i
+ prt (AtV i) = prt i
+ prt (AtL s) = s
+ prt (AtI i) = show i
+
+prQIdent :: QIdent -> String
+prQIdent (m,f) = prt m ++ "." ++ prt f
+
+-- print terms without qualifications
+
+prExp :: Term -> String
+prExp e = case e of
+ App f a -> pr1 f +++ pr2 a
+ Abs x b -> "\\" ++ prt x +++ "->" +++ prExp b
+ Prod x a b -> "(\\" ++ prt x +++ ":" +++ prExp a ++ ")" +++ "->" +++ prExp b
+ Q _ c -> prt c
+ QC _ c -> prt c
+ _ -> prt e
+ where
+ pr1 e = case e of
+ Abs _ _ -> prParenth $ prExp e
+ Prod _ _ _ -> prParenth $ prExp e
+ _ -> prExp e
+ pr2 e = case e of
+ App _ _ -> prParenth $ prExp e
+ _ -> pr1 e
diff --git a/src/GF/Grammar/Refresh.hs b/src/GF/Grammar/Refresh.hs
new file mode 100644
index 000000000..8b33444d0
--- /dev/null
+++ b/src/GF/Grammar/Refresh.hs
@@ -0,0 +1,105 @@
+module Refresh where
+
+import Operations
+import Grammar
+import Ident
+import Modules
+import Macros
+import Monad
+
+refreshTerm :: Term -> Err Term
+refreshTerm = refreshTermN 0
+
+refreshTermN :: Int -> Term -> Err Term
+refreshTermN i e = liftM snd $ refreshTermKN i e
+
+refreshTermKN :: Int -> Term -> Err (Int,Term)
+refreshTermKN i e = liftM (\ (t,(_,i)) -> (i,t)) $
+ appSTM (refresh e) (initIdStateN i)
+
+refresh :: Term -> STM IdState Term
+refresh e = case e of
+
+ Vr x -> liftM Vr (lookVar x)
+ Abs x b -> liftM2 Abs (refVarPlus x) (refresh b)
+
+ Prod x a b -> do
+ a' <- refresh a
+ x' <- refVar x
+ b' <- refresh b
+ return $ Prod x' a' b'
+
+ Let (x,(mt,a)) b -> do
+ a' <- refresh a
+ mt' <- case mt of
+ Just t -> refresh t >>= (return . Just)
+ _ -> return mt
+ x' <- refVar x
+ b' <- refresh b
+ return (Let (x',(mt',a')) b')
+
+ R r -> liftM R $ refreshRecord r
+
+ ExtR r s -> liftM2 ExtR (refresh r) (refresh s)
+
+ T i cc -> liftM2 T (refreshTInfo i) (mapM refreshCase cc)
+
+ _ -> composOp refresh e
+
+refreshCase :: (Patt,Term) -> STM IdState (Patt,Term)
+refreshCase (p,t) = liftM2 (,) (refreshPatt p) (refresh t)
+
+refreshPatt p = case p of
+ PV x -> liftM PV (refVar x)
+ PC c ps -> liftM (PC c) (mapM refreshPatt ps)
+ PP q c ps -> liftM (PP q c) (mapM refreshPatt ps)
+ PR r -> liftM PR (mapPairsM refreshPatt r)
+ PT t p' -> liftM2 PT (refresh t) (refreshPatt p')
+ _ -> return p
+
+refreshRecord r = case r of
+ [] -> return r
+ (x,(mt,a)):b -> do
+ a' <- refresh a
+ mt' <- case mt of
+ Just t -> refresh t >>= (return . Just)
+ _ -> return mt
+ b' <- refreshRecord b
+ return $ (x,(mt',a')) : b'
+
+refreshTInfo i = case i of
+ TTyped t -> liftM TTyped $ refresh t
+ TComp t -> liftM TComp $ refresh t
+ TWild t -> liftM TWild $ refresh t
+ _ -> return i
+
+-- for abstract syntax
+
+refreshEquation :: Equation -> Err ([Patt],Term)
+refreshEquation pst = err Bad (return . fst) (appSTM (refr pst) initIdState) where
+ refr (ps,t) = liftM2 (,) (mapM refreshPatt ps) (refresh t)
+
+-- for concrete and resource in grammar, before optimizing
+
+refreshGrammar :: SourceGrammar -> Err SourceGrammar
+refreshGrammar = liftM (MGrammar . snd) . foldM refreshModule (0,[]) . modules
+
+refreshModule :: (Int,[SourceModule]) -> SourceModule -> Err (Int,[SourceModule])
+refreshModule (k,ms) mi@(i,m) = case m of
+ ModMod mo@(Module mt fs me ops js) | (isModCnc mo || mt == MTResource) -> do
+ (k',js') <- foldM refreshRes (k,[]) $ tree2list js
+ return (k', (i, ModMod(Module mt fs me ops (buildTree js'))) : ms)
+ _ -> return (k, mi:ms)
+ where
+ refreshRes (k,cs) ci@(c,info) = case info of
+ ResOper ptyp (Yes trm) -> do ---- refresh ptyp
+ (k',trm') <- refreshTermKN k trm
+ return $ (k', (c, ResOper ptyp (Yes trm')):cs)
+ CncCat mt (Yes trm) pn -> do ---- refresh mt, pn
+ (k',trm') <- refreshTermKN k trm
+ return $ (k', (c, CncCat mt (Yes trm') pn):cs)
+ CncFun mt (Yes trm) pn -> do ---- refresh pn
+ (k',trm') <- refreshTermKN k trm
+ return $ (k', (c, CncFun mt (Yes trm') pn):cs)
+ _ -> return (k, ci:cs)
+
diff --git a/src/GF/Grammar/ReservedWords.hs b/src/GF/Grammar/ReservedWords.hs
new file mode 100644
index 000000000..43738989f
--- /dev/null
+++ b/src/GF/Grammar/ReservedWords.hs
@@ -0,0 +1,32 @@
+module ReservedWords (isResWord, isResWordGFC) where
+
+import List
+
+-- reserved words of GF. (c) Aarne Ranta 19/3/2002 under Gnu GPL
+-- modified by Markus Forsberg 9/4.
+-- modified by AR 12/6/2003 for GF2 and GFC
+
+
+isResWord :: String -> Bool
+isResWord s = isInTree s resWordTree
+
+resWordTree :: BTree
+resWordTree =
+-- mapTree fst $ sorted2tree $ flip zip (repeat ()) $ sort allReservedWords
+ B "let" (B "concrete" (B "Tok" (B "Str" (B "PType" (B "Lin" N N) N) (B "Strs" N N)) (B "case" (B "abstract" (B "Type" N N) N) (B "cat" N N))) (B "fun" (B "flags" (B "def" (B "data" N N) N) (B "fn" N N)) (B "in" (B "grammar" N N) (B "include" N N)))) (B "pattern" (B "of" (B "lindef" (B "lincat" (B "lin" N N) N) (B "lintype" N N)) (B "out" (B "oper" (B "open" N N) N) (B "param" N N))) (B "strs" (B "resource" (B "printname" (B "pre" N N) N) (B "reuse" N N)) (B "transfer" (B "table" N N) (B "variants" N N))))
+
+
+isResWordGFC :: String -> Bool
+isResWordGFC s = isInTree s $
+ B "of" (B "fun" (B "concrete" (B "cat" (B "abstract" N N) N) (B "flags" N N)) (B "lin" (B "in" N N) (B "lincat" N N))) (B "resource" (B "param" (B "oper" (B "open" N N) N) (B "pre" N N)) (B "table" (B "strs" N N) (B "variants" N N)))
+
+data BTree = N | B String BTree BTree deriving (Show)
+
+isInTree :: String -> BTree -> Bool
+isInTree x tree = case tree of
+ N -> False
+ B a left right
+ | x < a -> isInTree x left
+ | x > a -> isInTree x right
+ | x == a -> True
+
diff --git a/src/GF/Grammar/TC.hs b/src/GF/Grammar/TC.hs
new file mode 100644
index 000000000..ce9da979d
--- /dev/null
+++ b/src/GF/Grammar/TC.hs
@@ -0,0 +1,210 @@
+module TC where
+
+import Operations
+import Abstract
+import AbsCompute
+
+import Monad
+
+-- Thierry Coquand's type checking algorithm that creates a trace
+
+data AExp =
+ AVr Ident Val
+ | ACn QIdent Val
+ | AType
+ | AInt Int
+ | AStr String
+ | AMeta MetaSymb Val
+ | AApp AExp AExp Val
+ | AAbs Ident Val AExp
+ | AProd Ident AExp AExp
+ | AEqs [([Exp],AExp)] ---
+ deriving (Eq,Show)
+
+type Theory = QIdent -> Err Val
+
+lookupConst :: Theory -> QIdent -> Err Val
+lookupConst th f = th f
+
+lookupVar :: Env -> Ident -> Err Val
+lookupVar g x = maybe (prtBad "unknown variable" x) return $ lookup x ((IW,uVal):g)
+-- wild card IW: no error produced, ?0 instead.
+
+type TCEnv = (Int,Env,Env)
+
+emptyTCEnv :: TCEnv
+emptyTCEnv = (0,[],[])
+
+whnf :: Val -> Err Val
+whnf v = ---- errIn ("whnf" +++ prt v) $ ---- debug
+ case v of
+ VApp u w -> do
+ u' <- whnf u
+ w' <- whnf w
+ app u' w'
+ VClos env e -> eval env e
+ _ -> return v
+
+app :: Val -> Val -> Err Val
+app u v = case u of
+ VClos env (Abs x e) -> eval ((x,v):env) e
+ _ -> return $ VApp u v
+
+eval :: Env -> Exp -> Err Val
+eval env e = ---- errIn ("eval" +++ prt e +++ "in" +++ prEnv env) $
+ case e of
+ Vr x -> lookupVar env x
+ Q m c -> return $ VCn (m,c)
+ Sort c -> return $ VType --- the only sort is Type
+ App f a -> join $ liftM2 app (eval env f) (eval env a)
+ _ -> return $ VClos env e
+
+eqVal :: Int -> Val -> Val -> Err [(Val,Val)]
+eqVal k u1 u2 = ---- errIn (prt u1 +++ "<>" +++ prBracket (show k) +++ prt u2) $
+ do
+ w1 <- whnf u1
+ w2 <- whnf u2
+ let v = VGen k
+ case (w1,w2) of
+ (VApp f1 a1, VApp f2 a2) -> liftM2 (++) (eqVal k f1 f2) (eqVal k a1 a2)
+ (VClos env1 (Abs x1 e1), VClos env2 (Abs x2 e2)) ->
+ eqVal (k+1) (VClos ((x1,v x1):env1) e1) (VClos ((x2,v x1):env2) e2)
+ (VClos env1 (Prod x1 a1 e1), VClos env2 (Prod x2 a2 e2)) ->
+ liftM2 (++)
+ (eqVal k (VClos env1 a1) (VClos env2 a2))
+ (eqVal (k+1) (VClos ((x1,v x1):env1) e1) (VClos ((x2,v x1):env2) e2))
+ (VGen i _, VGen j _) -> return [(w1,w2) | i /= j]
+ _ -> return [(w1,w2) | w1 /= w2]
+-- invariant: constraints are in whnf
+
+checkType :: Theory -> TCEnv -> Exp -> Err (AExp,[(Val,Val)])
+checkType th tenv e = checkExp th tenv e vType
+
+checkExp :: Theory -> TCEnv -> Exp -> Val -> Err (AExp, [(Val,Val)])
+checkExp th tenv@(k,rho,gamma) e ty = do
+ typ <- whnf ty
+ let v = VGen k
+ case e of
+ Meta m -> return $ (AMeta m typ,[])
+
+ Abs x t -> case typ of
+ VClos env (Prod y a b) -> do
+ a' <- whnf $ VClos env a ---
+ (t',cs) <- checkExp th
+ (k+1,(x,v x):rho, (x,a'):gamma) t (VClos ((y,v x):env) b)
+ return (AAbs x a' t', cs)
+ _ -> prtBad ("function type expected for" +++ prt e +++ "instead of") typ
+
+ Eqs es -> do
+ bcs <- mapM (\b -> checkBranch th tenv b typ) es
+ let (bs,css) = unzip bcs
+ return (AEqs bs, concat css)
+
+ Prod x a b -> do
+ testErr (typ == vType) "expected Type"
+ (a',csa) <- checkType th tenv a
+ (b',csb) <- checkType th (k+1, (x,v x):rho, (x,VClos rho a):gamma) b
+ return (AProd x a' b', csa ++ csb)
+
+ _ -> checkInferExp th tenv e typ
+
+checkInferExp :: Theory -> TCEnv -> Exp -> Val -> Err (AExp, [(Val,Val)])
+checkInferExp th tenv@(k,_,_) e typ = do
+ (e',w,cs1) <- inferExp th tenv e
+ cs2 <- eqVal k w typ
+ return (e',cs1 ++ cs2)
+
+inferExp :: Theory -> TCEnv -> Exp -> Err (AExp, Val, [(Val,Val)])
+inferExp th tenv@(k,rho,gamma) e = case e of
+ Vr x -> mkAnnot (AVr x) $ noConstr $ lookupVar gamma x
+ Q m c -> mkAnnot (ACn (m,c)) $ noConstr $ lookupConst th (m,c)
+ Sort _ -> return (AType, vType, [])
+ App f t -> do
+ (f',w,csf) <- inferExp th tenv f
+ typ <- whnf w
+ case typ of
+ VClos env (Prod x a b) -> do
+ (a',csa) <- checkExp th tenv t (VClos env a)
+ b' <- whnf $ VClos ((x,VClos rho t):env) b
+ return $ (AApp f' a' b', b', csf ++ csa)
+ _ -> prtBad ("Prod expected for function" +++ prt f +++ "instead of") typ
+ _ -> prtBad "cannot infer type of expression" e
+
+checkBranch :: Theory -> TCEnv -> Equation -> Val -> Err (([Exp],AExp),[(Val,Val)])
+checkBranch th tenv b@(ps,t) ty = errIn ("branch" +++ show b) $
+ chB tenv' ps' ty
+ where
+
+ (ps',_,rho2,_) = ps2ts k ps
+ tenv' = (k,rho2++rho, gamma)
+ (k,rho,gamma) = tenv
+
+ chB tenv@(k,rho,gamma) ps ty = case ps of
+ p:ps2 -> do
+ typ <- whnf ty
+ case typ of
+ VClos env (Prod y a b) -> do
+ a' <- whnf $ VClos env a
+ (p', sigma, binds, cs1) <- checkP tenv p y a'
+ let tenv' = (length binds, sigma ++ rho, binds ++ gamma)
+ ((ps',exp),cs2) <- chB tenv' ps2 (VClos ((y,p'):env) b)
+ return ((p:ps',exp), cs1 ++ cs2) -- don't change the patt
+ _ -> prtBad ("Product expected for definiens" +++prt t +++ "instead of") typ
+ [] -> do
+ (e,cs) <- checkExp th tenv t ty
+ return (([],e),cs)
+ checkP env@(k,rho,gamma) t x a = do
+ (delta,cs) <- checkPatt th env t a
+ let sigma = [(x, VGen i x) | ((x,_),i) <- zip delta [k..]]
+ return (VClos sigma t, sigma, delta, cs)
+
+ ps2ts k = foldr p2t ([],0,[],k)
+ p2t p (ps,i,g,k) = case p of
+ PV IW -> (meta (MetaSymb i) : ps, i+1,g,k)
+ PV x -> (vr x : ps, i, upd x k g,k+1)
+---- PL s -> (cn s : ps, i, g, k)
+ PP m c xs -> (mkApp (qq (m,c)) xss : ps, j, g',k')
+ where (xss,j,g',k') = foldr p2t ([],i,g,k) xs
+ _ -> error $ "undefined p2t case" +++ prt p +++ "in checkBranch"
+
+ upd x k g = (x, VGen k x) : g --- hack to recognize pattern variables
+
+checkPatt :: Theory -> TCEnv -> Exp -> Val -> Err (Binds,[(Val,Val)])
+checkPatt th tenv exp val = do
+ (aexp,_,cs) <- checkExpP tenv exp val
+ let binds = extrBinds aexp
+ return (binds,cs)
+ where
+ extrBinds aexp = case aexp of
+ AVr i v -> [(i,v)]
+ AApp f a _ -> extrBinds f ++ extrBinds a
+ _ -> [] -- no other cases are possible
+
+--- ad hoc, to find types of variables
+ checkExpP tenv@(k,rho,gamma) exp val = case exp of
+ Meta m -> return $ (AMeta m val, val, [])
+ Vr x -> return $ (AVr x val, val, [])
+ Q m c -> do
+ typ <- lookupConst th (m,c)
+ return $ (ACn (m,c) typ, typ, [])
+ App f t -> do
+ (f',w,csf) <- checkExpP tenv f val
+ typ <- whnf w
+ case typ of
+ VClos env (Prod x a b) -> do
+ (a',_,csa) <- checkExpP tenv t (VClos env a)
+ b' <- whnf $ VClos ((x,VClos rho t):env) b
+ return $ (AApp f' a' b', b', csf ++ csa)
+ _ -> prtBad ("Prod expected for function" +++ prt f +++ "instead of") typ
+ _ -> prtBad "cannot typecheck pattern" exp
+
+-- auxiliaries
+
+noConstr :: Err Val -> Err (Val,[(Val,Val)])
+noConstr er = er >>= (\v -> return (v,[]))
+
+mkAnnot :: (Val -> AExp) -> Err (Val,[(Val,Val)]) -> Err (AExp,Val,[(Val,Val)])
+mkAnnot a ti = do
+ (v,cs) <- ti
+ return (a v, v, cs)
+
diff --git a/src/GF/Grammar/TypeCheck.hs b/src/GF/Grammar/TypeCheck.hs
new file mode 100644
index 000000000..c97bdd362
--- /dev/null
+++ b/src/GF/Grammar/TypeCheck.hs
@@ -0,0 +1,231 @@
+module TypeCheck where
+
+import Operations
+import Zipper
+
+import Abstract
+import AbsCompute
+import Refresh
+import LookAbs
+
+import TC
+
+import Unify ---
+
+import Monad (foldM, liftM, liftM2)
+
+-- top-level type checking functions; TC should not be called directly.
+
+annotate :: GFCGrammar -> Exp -> Err Tree
+annotate gr exp = annotateIn gr [] exp Nothing
+
+-- type check in empty context, return a list of constraints
+justTypeCheck :: GFCGrammar -> Exp -> Val -> Err Constraints
+justTypeCheck gr e v = do
+ (_,constrs0) <- checkExp (grammar2theory gr) (initTCEnv []) e v
+ constrs1 <- reduceConstraints gr 0 constrs0
+ return $ fst $ splitConstraints constrs1
+
+-- type check in empty context, return the expression itself if valid
+checkIfValidExp :: GFCGrammar -> Exp -> Err Exp
+checkIfValidExp gr e = do
+ (_,_,constrs0) <- inferExp (grammar2theory gr) (initTCEnv []) e
+ constrs1 <- reduceConstraints gr 0 constrs0
+ ifNull (return e) (Bad . unwords . prConstrs) constrs1
+
+annotateIn :: GFCGrammar -> Binds -> Exp -> Maybe Val -> Err Tree
+annotateIn gr gamma exp = maybe (infer exp) (check exp) where
+ infer e = do
+ (a,_,cs) <- inferExp theory env e
+ aexp2treeC (a,cs)
+ check e v = do
+ (a,cs) <- checkExp theory env e v
+ aexp2treeC (a,cs)
+ env = initTCEnv gamma
+ theory = grammar2theory gr
+ aexp2treeC (a,c) = do
+ c' <- reduceConstraints gr (length gamma) c
+ aexp2tree (a,c')
+
+-- invariant way of creating TCEnv from context
+initTCEnv gamma =
+ (length gamma,[(x,VGen i x) | ((x,_),i) <- zip gamma [0..]], gamma)
+
+-- process constraints after eqVal by computing by defs
+reduceConstraints :: GFCGrammar -> Int -> Constraints -> Err Constraints
+reduceConstraints gr i = liftM concat . mapM redOne where
+ redOne (u,v) = do
+ u' <- computeVal gr u
+ v' <- computeVal gr v
+ eqVal i u' v'
+
+computeVal :: GFCGrammar -> Val -> Err Val
+computeVal gr v = case v of
+ VClos g@(_:_) e -> do
+ e' <- compt (map fst g) e --- bindings of g in e?
+ whnf $ VClos g e'
+ VApp f c -> liftM2 VApp (compv f) (compv c) >>= whnf
+ _ -> whnf v
+ where
+ compt = computeAbsTermIn gr
+ compv = computeVal gr
+
+-- take apart constraints that have the form (? <> t), usable as solutions
+splitConstraints :: Constraints -> (Constraints,MetaSubst)
+splitConstraints cs = csmsu where
+
+ csmsu = unif (csf,msf) -- alternative: filter first
+ (csf,msf) = foldr mkOne ([],[]) cs
+
+ csmsf = foldr mkOne ([],msu) csu
+ (csu,msu) = unif (cs,[]) -- alternative: unify first
+
+ mkOne (u,v) = case (u,v) of
+ (VClos g (Meta m), v) | null g -> sub m v
+ (v, VClos g (Meta m)) | null g -> sub m v
+ -- do nothing if meta has nonempty closure; null g || isConstVal v WAS WRONG
+ c -> con c
+ con c (cs,ms) = (c:cs,ms)
+ sub m v (cs,ms) = (cs,(m,v):ms)
+
+ unifo = id -- alternative: don't use unification
+
+ unif cm@(cs,ms) = errVal cm $ do --- alternative: use unification
+ (cs',ms') <- unifyVal cs
+ return (cs', ms' ++ ms)
+
+performMetaSubstNode :: MetaSubst -> TrNode -> TrNode
+performMetaSubstNode subst n@(N (b,a,v,(c,m),s)) = let
+ v' = metaSubstVal v
+ b' = [(x,metaSubstVal v) | (x,v) <- b]
+ c' = [(u',v') | (u,v) <- c,
+ let (u',v') = (metaSubstVal u, metaSubstVal v), u' /= v']
+ in N (b',a,v',(c',m),s)
+ where
+ metaSubstVal u = errVal u $ whnf $ case u of
+ VApp f a -> VApp (metaSubstVal f) (metaSubstVal a)
+ VClos g e -> VClos [(x,metaSubstVal v) | (x,v) <- g] (metaSubstExp e)
+ _ -> u
+ metaSubstExp e = case e of
+ Meta m -> errVal e $ maybe (return e) val2expSafe $ lookup m subst
+ _ -> composSafeOp metaSubstExp e
+
+-- weak heuristic to narrow down menus; not used for TC. 15/11/2001
+-- the age-old method from GF 0.9
+possibleConstraints :: GFCGrammar -> Constraints -> Bool
+possibleConstraints gr = and . map (possibleConstraint gr)
+
+possibleConstraint :: GFCGrammar -> (Val,Val) -> Bool
+possibleConstraint gr (u,v) = errVal True $ do
+ u' <- val2exp u >>= compute gr
+ v' <- val2exp v >>= compute gr
+ return $ cts u' v'
+ where
+ cts t u = case (t,u) of
+ (Q m c, Q n d) -> c == d || notCan (m,c) || notCan (n,d)
+ (App f a, App g b) -> cts f g && cts a b
+ (Abs x b, Abs y c) -> cts b c
+ (Prod x a f, Prod y b g) -> cts a b && cts f g
+ (_ , _) -> isUnknown t || isUnknown u
+
+ isUnknown t = case t of
+ Vr _ -> True
+ Meta _ -> True
+ _ -> False
+
+ notCan = not . isPrimitiveFun gr
+
+-- interface to TC type checker
+
+type2val :: Type -> Val
+type2val = VClos []
+
+aexp2tree :: (AExp,[(Val,Val)]) -> Err Tree
+aexp2tree (aexp,cs) = do
+ (bi,at,vt,ts) <- treeForm aexp
+ ts' <- mapM aexp2tree [(t,[]) | t <- ts]
+ return $ Tr (N (bi,at,vt,(cs,[]),False),ts')
+ where
+ treeForm a = case a of
+ AAbs x v b -> do
+ (bi, at, vt, args) <- treeForm b
+ v' <- whnf v ---- should not be needed...
+ return ((x,v') : bi, at, vt, args)
+ AApp c a v -> do
+ (_,at,_,args) <- treeForm c
+ v' <- whnf v ----
+ return ([],at,v',args ++ [a])
+ AVr x v -> do
+ v' <- whnf v ----
+ return ([],AtV x,v',[])
+ ACn c v -> do
+ v' <- whnf v ----
+ return ([],AtC c,v',[])
+ AMeta m v -> do
+ v' <- whnf v ----
+ return ([],AtM m,v',[])
+ _ -> Bad "illegal tree" -- AProd
+
+grammar2theory :: GFCGrammar -> Theory
+grammar2theory gr (m,f) = case lookupFunType gr m f of
+ Ok t -> return $ type2val t
+ Bad s -> case lookupCatContext gr m f of
+ Ok cont -> return $ cont2val cont
+ _ -> Bad s
+
+cont2exp :: Context -> Exp
+cont2exp c = mkProd (c, eType, []) -- to check a context
+
+cont2val :: Context -> Val
+cont2val = type2val . cont2exp
+
+-- some top-level batch-mode checkers for the compiler
+
+justTypeCheckSrc :: Grammar -> Exp -> Val -> Err Constraints
+justTypeCheckSrc gr e v = do
+ (_,constrs0) <- checkExp (grammar2theorySrc gr) (initTCEnv []) e v
+----- constrs1 <- reduceConstraints gr 0 constrs0
+ return $ fst $ splitConstraints constrs0
+
+grammar2theorySrc :: Grammar -> Theory
+grammar2theorySrc gr (m,f) = case lookupFunTypeSrc gr m f of
+ Ok t -> return $ type2val t
+ Bad s -> case lookupCatContextSrc gr m f of
+ Ok cont -> return $ cont2val cont
+ _ -> Bad s
+
+checkContext :: Grammar -> Context -> [String]
+checkContext st = checkTyp st . cont2exp
+
+checkTyp :: Grammar -> Type -> [String]
+checkTyp gr typ = err singleton prConstrs $ justTypeCheckSrc gr typ vType
+
+checkEquation :: Grammar -> Fun -> Trm -> [String]
+checkEquation gr (m,fun) def = err singleton id $ do
+ typ <- lookupFunTypeSrc gr m fun
+ cs <- justTypeCheckSrc gr def (vClos typ)
+ let cs1 = cs ----- filter (not . possibleConstraint gr) cs ----
+ return $ ifNull [] (singleton . prConstraints) cs1
+
+checkConstrs :: Grammar -> Cat -> [Ident] -> [String]
+checkConstrs gr cat _ = [] ---- check constructors!
+
+
+
+
+
+
+{- ----
+err singleton concat . mapM checkOne where
+ checkOne con = do
+ typ <- lookupFunType gr con
+ typ' <- computeAbsTerm gr typ
+ vcat <- valCat typ'
+ return $ if (cat == vcat) then [] else ["wrong type in constructor" +++ prt con]
+-}
+
+editAsTermCommand :: GFCGrammar -> (Loc TrNode -> Err (Loc TrNode)) -> Exp -> [Exp]
+editAsTermCommand gr c e = err (const []) singleton $ do
+ t <- annotate gr $ refreshMetas [] e
+ t' <- c $ tree2loc t
+ return $ tree2exp $ loc2tree t'
diff --git a/src/GF/Grammar/Unify.hs b/src/GF/Grammar/Unify.hs
new file mode 100644
index 000000000..a39087c62
--- /dev/null
+++ b/src/GF/Grammar/Unify.hs
@@ -0,0 +1,84 @@
+module Unify where
+
+import Abstract
+
+import Operations
+
+import List (partition)
+
+-- (c) Petri Mäenpää & Aarne Ranta, 1998--2001
+
+-- brute-force adaptation of the old-GF program AR 21/12/2001 ---
+-- the only use is in TypeCheck.splitConstraints
+
+unifyVal :: Constraints -> Err (Constraints,MetaSubst)
+unifyVal cs0 = do
+ let (cs1,cs2) = partition notSolvable cs0
+ let (us,vs) = unzip cs1
+ us' <- mapM val2exp us
+ vs' <- mapM val2exp vs
+ let (ms,cs) = unifyAll (zip us' vs') []
+ return (cs1 ++ [(VClos [] t, VClos [] u) | (t,u) <- cs],
+ [(m, VClos [] t) | (m,t) <- ms])
+ where
+ notSolvable (v,w) = case (v,w) of -- don't consider nonempty closures
+ (VClos (_:_) _,_) -> True
+ (_,VClos (_:_) _) -> True
+ _ -> False
+
+type Unifier = [(MetaSymb, Trm)]
+type Constrs = [(Trm, Trm)]
+
+unifyAll :: Constrs -> Unifier -> (Unifier,Constrs)
+unifyAll [] g = (g, [])
+unifyAll ((a@(s, t)) : l) g =
+ let (g1, c) = unifyAll l g
+ in case unify s t g1 of
+ Ok g2 -> (g2, c)
+ _ -> (g1, a : c)
+
+unify :: Trm -> Trm -> Unifier -> Err Unifier
+unify e1 e2 g =
+ case (e1, e2) of
+ (Meta s, t) -> do
+ tg <- subst_all g t
+ let sg = maybe e1 id (lookup s g)
+ if (sg == Meta s) then extend g s tg else unify sg tg g
+ (t, Meta s) -> unify e2 e1 g
+ (Q _ a, Q _ b) | (a == b) -> return g ---- qualif?
+ (QC _ a, QC _ b) | (a == b) -> return g ----
+ (Vr x, Vr y) | (x == y) -> return g
+ (Abs x b, Abs y c) -> do let c' = substTerm [x] [(y,Vr x)] c
+ unify b c' g
+ (App c a, App d b) -> case unify c d g of
+ Ok g1 -> unify a b g1
+ _ -> prtBad "fail unify" e1
+ _ -> prtBad "fail unify" e1
+
+extend :: Unifier -> MetaSymb -> Trm -> Err Unifier
+extend g s t | (t == Meta s) = return g
+ | occCheck s t = prtBad "occurs check" t
+ | True = return ((s, t) : g)
+
+subst_all :: Unifier -> Trm -> Err Trm
+subst_all s u =
+ case (s,u) of
+ ([], t) -> return t
+ (a : l, t) -> do
+ t' <- (subst_all l t) --- successive substs - why ?
+ return $ substMetas [a] t'
+
+substMetas :: [(MetaSymb,Trm)] -> Trm -> Trm
+substMetas subst trm = case trm of
+ Meta x -> case lookup x subst of
+ Just t -> t
+ _ -> trm
+ _ -> composSafeOp (substMetas subst) trm
+
+occCheck :: MetaSymb -> Trm -> Bool
+occCheck s u = case u of
+ Meta v -> s == v
+ App c a -> occCheck s c || occCheck s a
+ Abs x b -> occCheck s b
+ _ -> False
+
diff --git a/src/GF/Grammar/Values.hs b/src/GF/Grammar/Values.hs
new file mode 100644
index 000000000..7b02d187a
--- /dev/null
+++ b/src/GF/Grammar/Values.hs
@@ -0,0 +1,52 @@
+module Values where
+
+import Operations
+import Zipper
+
+import Grammar
+import Ident
+
+-- values used in TC type checking
+
+type Exp = Term
+
+data Val = VGen Int Ident | VApp Val Val | VCn QIdent | VType | VClos Env Exp
+ deriving (Eq,Show)
+
+type Env = [(Ident,Val)]
+
+-- annotated tree used in editing
+
+type Tree = Tr TrNode
+
+newtype TrNode = N (Binds,Atom,Val,(Constraints,MetaSubst),Bool)
+ deriving (Eq,Show)
+
+data Atom = AtC Fun | AtM MetaSymb | AtV Ident | AtL String | AtI Int
+ deriving (Eq,Show)
+
+type Binds = [(Ident,Val)]
+type Constraints = [(Val,Val)]
+type MetaSubst = [(MetaSymb,Val)]
+
+-- for TC
+
+vType :: Val
+vType = VType
+
+cType :: Ident
+cType = identC "Type" --- #0
+
+eType :: Exp
+eType = Sort "Type"
+
+tree2exp :: Tree -> Exp
+tree2exp (Tr (N (bi,at,_,_,_),ts)) = foldr Abs (foldl App at' ts') bi' where
+ at' = case at of
+ AtC (m,c) -> Q m c
+ AtV i -> Vr i
+ AtM m -> Meta m
+ AtL s -> K s
+ AtI s -> EInt s
+ bi' = map fst bi
+ ts' = map tree2exp ts
generated by cgit v1.2.3 (git 2.39.1) at 2026-05-20 19:02:18 +0000