diff --git a/src/GF/Compile/GrammarToGFCC.hs b/src/GF/Compile/GrammarToGFCC.hs index a2b03ab63..aa84f820c 100644 --- a/src/GF/Compile/GrammarToGFCC.hs +++ b/src/GF/Compile/GrammarToGFCC.hs @@ -139,7 +139,7 @@ mkExp scope t = case GM.termForm t of EInt i -> C.ELit (C.LInt i) EFloat f -> C.ELit (C.LFlt f) K s -> C.ELit (C.LStr s) - Meta (MetaSymb i) -> C.EMeta i + Meta i -> C.EMeta i _ -> C.EMeta 0 mkPatt scope p = diff --git a/src/GF/Compile/TC.hs b/src/GF/Compile/TC.hs index 7ee3e9755..3999c223b 100644 --- a/src/GF/Compile/TC.hs +++ b/src/GF/Compile/TC.hs @@ -37,7 +37,7 @@ data AExp = | AInt Integer | AFloat Double | AStr String - | AMeta MetaSymb Val + | AMeta MetaId Val | AApp AExp AExp Val | AAbs Ident Val AExp | AProd Ident AExp AExp @@ -234,7 +234,7 @@ checkBranch th tenv b@(ps,t) ty = errIn ("branch" +++ show b) $ ps2ts k = foldr p2t ([],0,[],k) p2t p (ps,i,g,k) = case p of - PW -> (Meta (MetaSymb i) : ps, i+1,g,k) + PW -> (Meta i : ps, i+1,g,k) PV x -> (Vr x : ps, i, upd x k g,k+1) PString s -> (K s : ps, i, g, k) PInt n -> (EInt n : ps, i, g, k) diff --git a/src/GF/Grammar/Binary.hs b/src/GF/Grammar/Binary.hs index 83f96c025..31e4ea222 100644 --- a/src/GF/Grammar/Binary.hs +++ b/src/GF/Grammar/Binary.hs @@ -254,10 +254,6 @@ instance Binary Label where 1 -> fmap LVar get _ -> decodingError -instance Binary MetaSymb where - put (MetaSymb m) = put m - get = fmap MetaSymb get - decodeModHeader :: FilePath -> IO SourceModule decodeModHeader fpath = do (m,mtype,mstatus,flags,extend,mwith,opens,med) <- decodeFile fpath diff --git a/src/GF/Grammar/Grammar.hs b/src/GF/Grammar/Grammar.hs index a1d1ce8ab..8cfc397af 100644 --- a/src/GF/Grammar/Grammar.hs +++ b/src/GF/Grammar/Grammar.hs @@ -29,7 +29,7 @@ module GF.Grammar.Grammar (SourceGrammar, Patt(..), TInfo(..), Label(..), - MetaSymb(..), + MetaId, Hypo, Context, Equation, @@ -115,7 +115,7 @@ data Term = | App Term Term -- ^ application: @f a@ | Abs Ident Term -- ^ abstraction: @\x -> b@ - | Meta MetaSymb -- ^ metavariable: @?i@ (only parsable: ? = ?0) + | Meta {-# UNPACK #-} !MetaId -- ^ metavariable: @?i@ (only parsable: ? = ?0) | Prod Ident Term Term -- ^ function type: @(x : A) -> B@ | Typed Term Term -- ^ type-annotated term -- @@ -198,7 +198,7 @@ data Label = | LVar Int deriving (Show, Eq, Ord) -newtype MetaSymb = MetaSymb Int deriving (Show, Eq, Ord) +type MetaId = Int type Hypo = (Ident,Term) -- (x:A) (_:A) A type Context = [Hypo] -- (x:A)(y:B) (x,y:A) (_,_:A) diff --git a/src/GF/Grammar/MMacros.hs b/src/GF/Grammar/MMacros.hs index 15e18231e..0a6c721ed 100644 --- a/src/GF/Grammar/MMacros.hs +++ b/src/GF/Grammar/MMacros.hs @@ -59,7 +59,7 @@ valTree = valNode . nodeTree mkNode :: Binds -> Atom -> Val -> (Constraints, MetaSubst) -> TrNode mkNode binds atom vtyp cs = N (binds,atom,vtyp,cs,False) -metasTree :: Tree -> [Meta] +metasTree :: Tree -> [MetaId] metasTree = concatMap metasNode . scanTree where metasNode n = [m | AtM m <- [atomNode n]] ++ map fst (metaSubstsNode n) @@ -98,7 +98,6 @@ mAtom = AtM meta0 -} type Var = Ident -type Meta = MetaSymb uVal :: Val uVal = vClos uExp @@ -113,7 +112,7 @@ mExp, mExp0 :: Exp mExp = Meta meta0 mExp0 = mExp -meta2exp :: MetaSymb -> Exp +meta2exp :: MetaId -> Exp meta2exp = Meta {- atomC :: Fun -> Atom @@ -129,13 +128,13 @@ atomIsMeta atom = case atom of AtM _ -> True _ -> False -getMetaAtom :: Atom -> Err Meta +getMetaAtom :: Atom -> Err MetaId 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]] +cat2val cont cat = vClos $ mkApp (qq cat) [Meta i | i <- [1..length cont]] val2cat :: Val -> Err Cat val2cat v = val2exp v >>= valCat @@ -150,7 +149,7 @@ substTerm ss g c = case c of Prod y (substTerm ss g a) (substTerm (y:ss) ((x,Vr y):g) b) _ -> c -metaSubstExp :: MetaSubst -> [(Meta,Exp)] +metaSubstExp :: MetaSubst -> [(MetaId,Exp)] metaSubstExp msubst = [(m, errVal (meta2exp m) (val2expSafe v)) | (m,v) <- msubst] -- * belong here rather than to computation @@ -230,21 +229,6 @@ 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 @@ -284,8 +268,8 @@ mkJustProd cont typ = mkProd (cont,typ,[]) int2var :: Int -> Ident int2var = identC . BS.pack . ('$':) . show -meta0 :: Meta -meta0 = int2meta 0 +meta0 :: MetaId +meta0 = 0 termMeta0 :: Term termMeta0 = Meta meta0 diff --git a/src/GF/Grammar/Macros.hs b/src/GF/Grammar/Macros.hs index 72f0eb10a..84a217b26 100644 --- a/src/GF/Grammar/Macros.hs +++ b/src/GF/Grammar/Macros.hs @@ -364,49 +364,6 @@ justIdentOf (Vr x) = Just x justIdentOf (Cn x) = Just x justIdentOf _ = Nothing -isMeta :: Term -> Bool -isMeta (Meta _) = True -isMeta _ = False - -mkMeta :: Int -> Term -mkMeta = Meta . MetaSymb - -nextMeta :: MetaSymb -> MetaSymb -nextMeta = int2meta . succ . metaSymbInt - -int2meta :: Int -> MetaSymb -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] -> Term -> Term -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} @@ -696,9 +653,6 @@ 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 diff --git a/src/GF/Grammar/Parser.y b/src/GF/Grammar/Parser.y index 90e035a02..76458209c 100644 --- a/src/GF/Grammar/Parser.y +++ b/src/GF/Grammar/Parser.y @@ -437,7 +437,7 @@ Exp6 | String { K $1 } | Integer { EInt $1 } | Double { EFloat $1 } - | '?' { Meta (int2meta 0) } + | '?' { Meta 0 } | '[' ']' { Empty } | '[' Ident Exps ']' { foldl App (Vr (mkListId $2)) $3 } | '[' String ']' { case $2 of diff --git a/src/GF/Grammar/Unify.hs b/src/GF/Grammar/Unify.hs index b48301186..8ac5351e1 100644 --- a/src/GF/Grammar/Unify.hs +++ b/src/GF/Grammar/Unify.hs @@ -38,7 +38,7 @@ unifyVal cs0 = do (_,VClos (_:_) _) -> True _ -> False -type Unifier = [(MetaSymb, Term)] +type Unifier = [(MetaId, Term)] type Constrs = [(Term, Term)] unifyAll :: Constrs -> Unifier -> (Unifier,Constrs) @@ -68,7 +68,7 @@ unify e1 e2 g = (RecType xs,RecType ys) | xs == ys -> return g _ -> Bad (render (text "fail unify" <+> ppTerm Unqualified 0 e1)) -extend :: Unifier -> MetaSymb -> Term -> Err Unifier +extend :: Unifier -> MetaId -> Term -> Err Unifier extend g s t | (t == Meta s) = return g | occCheck s t = Bad (render (text "occurs check" <+> ppTerm Unqualified 0 t)) | True = return ((s, t) : g) @@ -81,14 +81,14 @@ subst_all s u = t' <- (subst_all l t) --- successive substs - why ? return $ substMetas [a] t' -substMetas :: [(MetaSymb,Term)] -> Term -> Term +substMetas :: [(MetaId,Term)] -> Term -> Term substMetas subst trm = case trm of Meta x -> case lookup x subst of Just t -> t _ -> trm _ -> composSafeOp (substMetas subst) trm -occCheck :: MetaSymb -> Term -> Bool +occCheck :: MetaId -> Term -> Bool occCheck s u = case u of Meta v -> s == v App c a -> occCheck s c || occCheck s a diff --git a/src/GF/Grammar/Values.hs b/src/GF/Grammar/Values.hs index 9782db730..1a68ddc89 100644 --- a/src/GF/Grammar/Values.hs +++ b/src/GF/Grammar/Values.hs @@ -49,12 +49,12 @@ newtype TrNode = N (Binds,Atom,Val,(Constraints,MetaSubst),Bool) deriving (Eq,Show) data Atom = - AtC Fun | AtM MetaSymb | AtV Ident | AtL String | AtI Integer | AtF Double + AtC Fun | AtM MetaId | AtV Ident | AtL String | AtI Integer | AtF Double deriving (Eq,Show) -} type Binds = [(Ident,Val)] type Constraints = [(Val,Val)] -type MetaSubst = [(MetaSymb,Val)] +type MetaSubst = [(MetaId,Val)] -- for TC