remove some more old code

9 files changed, 37 insertions, 353 deletions

diff --git a/src/compiler/GF/Command/Importing.hs b/src/compiler/GF/Command/Importing.hs
index e7b9a076c..1b520cfc8 100644
--- a/src/compiler/GF/Command/Importing.hs
+++ b/src/compiler/GF/Command/Importing.hs
@@ -10,7 +10,7 @@ import GF.Grammar (SourceGrammar) -- for cc command
 import GF.Grammar.CFG
 import GF.Grammar.EBNF
 import GF.Compile.CFGtoPGF
-import GF.Infra.UseIO(die,tryIOE,useIOE)
+import GF.Infra.UseIO(die,tryIOE)
 import GF.Infra.Option
 import GF.Data.ErrM
 
diff --git a/src/compiler/GF/Compile/Compute/Abstract.hs b/src/compiler/GF/Compile/Compute/Abstract.hs
index c374a80b4..5ba2eeb21 100644
--- a/src/compiler/GF/Compile/Compute/Abstract.hs
+++ b/src/compiler/GF/Compile/Compute/Abstract.hs
@@ -35,16 +35,16 @@ import GF.Text.Pretty
 tracd m t = t 
 -- tracd = trace
 
-compute :: SourceGrammar -> Exp -> Err Exp
+compute :: SourceGrammar -> Term -> Err Term
 compute = computeAbsTerm
 
-computeAbsTerm :: SourceGrammar -> Exp -> Err Exp
+computeAbsTerm :: SourceGrammar -> Term -> Err Term
 computeAbsTerm gr = computeAbsTermIn (lookupAbsDef gr) []
 
 -- | a hack to make compute work on source grammar as well
 type LookDef = Ident -> Ident -> Err (Maybe Int,Maybe [Equation])
 
-computeAbsTermIn :: LookDef -> [Ident] -> Exp -> Err Exp
+computeAbsTermIn :: LookDef -> [Ident] -> Term -> Err Term
 computeAbsTermIn lookd xs e = errIn (render (text "computing" <+> ppTerm Unqualified 0 e)) $ compt xs e where
   compt vv t = case t of
 --    Prod x a b  -> liftM2 (Prod x) (compt vv a) (compt (x:vv) b)
diff --git a/src/compiler/GF/Compile/TypeCheck/Abstract.hs b/src/compiler/GF/Compile/TypeCheck/Abstract.hs
index aa52b5724..196e1a646 100644
--- a/src/compiler/GF/Compile/TypeCheck/Abstract.hs
+++ b/src/compiler/GF/Compile/TypeCheck/Abstract.hs
@@ -41,7 +41,7 @@ initTCEnv gamma =
 type2val :: Type -> Val
 type2val = VClos []
 
-cont2exp :: Context -> Exp
+cont2exp :: Context -> Term
 cont2exp c = mkProd c eType [] -- to check a context
 
 cont2val :: Context -> Val
@@ -49,7 +49,7 @@ cont2val = type2val . cont2exp
 
 -- some top-level batch-mode checkers for the compiler
 
-justTypeCheck :: SourceGrammar -> Exp -> Val -> Err Constraints
+justTypeCheck :: SourceGrammar -> Term -> Val -> Err Constraints
 justTypeCheck gr e v = do
   (_,constrs0) <- checkExp (grammar2theory gr) (initTCEnv []) e v
   (constrs1,_) <- unifyVal constrs0
diff --git a/src/compiler/GF/Compile/TypeCheck/TC.hs b/src/compiler/GF/Compile/TypeCheck/TC.hs
index 570a07275..c5924d1bc 100644
--- a/src/compiler/GF/Compile/TypeCheck/TC.hs
+++ b/src/compiler/GF/Compile/TypeCheck/TC.hs
@@ -59,7 +59,7 @@ lookupConst :: Theory -> QIdent -> Err Val
 lookupConst th f = th f
 
 lookupVar :: Env -> Ident -> Err Val
-lookupVar g x = maybe (Bad (render ("unknown variable" <+> x))) return $ lookup x ((identW,uVal):g)
+lookupVar g x = maybe (Bad (render ("unknown variable" <+> x))) return $ lookup x ((identW,VClos [] (Meta 0)):g)
 -- wild card IW: no error produced, ?0 instead.
 
 type TCEnv = (Int,Env,Env)
@@ -82,7 +82,7 @@ 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 -> Term -> Err Val
 eval env e = ---- errIn ("eval" +++ prt e +++ "in" +++ prEnv env) $ 
              case e of
   Vr x    -> lookupVar env x
@@ -115,10 +115,10 @@ eqVal k u1 u2 = ---- errIn (prt u1 +++ "<>" +++ prBracket (show k) +++ prt u2) $
     _ -> return [(w1,w2) | w1 /= w2]
 -- invariant: constraints are in whnf
 
-checkType :: Theory -> TCEnv -> Exp -> Err (AExp,[(Val,Val)])
+checkType :: Theory -> TCEnv -> Term -> Err (AExp,[(Val,Val)])
 checkType th tenv e = checkExp th tenv e vType
 
-checkExp :: Theory -> TCEnv -> Exp -> Val -> Err (AExp, [(Val,Val)])
+checkExp :: Theory -> TCEnv -> Term -> Val -> Err (AExp, [(Val,Val)])
 checkExp th tenv@(k,rho,gamma) e ty = do
   typ <- whnf ty
   let v = VGen k
@@ -169,13 +169,13 @@ checkExp th tenv@(k,rho,gamma) e ty = do
                    return (AGlue x y,cs1++cs2++cs3)
     _ -> checkInferExp th tenv e typ
 
-checkInferExp :: Theory -> TCEnv -> Exp -> Val -> Err (AExp, [(Val,Val)])
+checkInferExp :: Theory -> TCEnv -> Term -> 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 :: Theory -> TCEnv -> Term -> 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) | m == cPredefAbs && isPredefCat c
@@ -231,7 +231,7 @@ checkAssign th tenv@(k,rho,gamma) typs (lbl,(Nothing,exp)) = do
     Just val -> do (aexp,cs) <- checkExp th tenv exp val
                    return ((lbl,(val,aexp)),cs)
 
-checkBranch :: Theory -> TCEnv -> Equation -> Val -> Err (([Exp],AExp),[(Val,Val)])
+checkBranch :: Theory -> TCEnv -> Equation -> Val -> Err (([Term],AExp),[(Val,Val)])
 checkBranch th tenv b@(ps,t) ty = errIn ("branch" +++ show b) $ 
                                   chB tenv' ps' ty 
  where 
@@ -276,7 +276,7 @@ checkBranch th tenv b@(ps,t) ty = errIn ("branch" +++ show b) $
   upd x k g = (x, VGen k x) : g --- hack to recognize pattern variables
 
 
-checkPatt :: Theory -> TCEnv -> Exp -> Val -> Err (Binds,[(Val,Val)])
+checkPatt :: Theory -> TCEnv -> Term -> Val -> Err (Binds,[(Val,Val)])
 checkPatt th tenv exp val = do
   (aexp,_,cs) <- checkExpP tenv exp val
   let binds = extrBinds aexp
diff --git a/src/compiler/GF/Grammar.hs b/src/compiler/GF/Grammar.hs
index 58f514971..92bf60c9f 100644
--- a/src/compiler/GF/Grammar.hs
+++ b/src/compiler/GF/Grammar.hs
@@ -16,7 +16,6 @@ module GF.Grammar
            ( module GF.Grammar.Grammar,
              module GF.Grammar.Values,
              module GF.Grammar.Macros,
-             module GF.Grammar.MMacros,
              module GF.Grammar.Printer,
              module GF.Infra.Ident
            ) where
@@ -24,6 +23,5 @@ module GF.Grammar
 import GF.Grammar.Grammar
 import GF.Grammar.Values
 import GF.Grammar.Macros
-import GF.Grammar.MMacros
 import GF.Grammar.Printer
 import GF.Infra.Ident
diff --git a/src/compiler/GF/Grammar/MMacros.hs b/src/compiler/GF/Grammar/MMacros.hs
deleted file mode 100644
index a86cf501a..000000000
--- a/src/compiler/GF/Grammar/MMacros.hs
+++ /dev/null
@@ -1,280 +0,0 @@
-----------------------------------------------------------------------
--- |
--- Module      : MMacros
--- Maintainer  : AR
--- Stability   : (stable)
--- Portability : (portable)
---
--- > CVS $Date: 2005/05/10 12:49:13 $ 
--- > CVS $Author: aarne $
--- > CVS $Revision: 1.9 $
---
--- some more abstractions on grammars, esp. for Edit
------------------------------------------------------------------------------
-
-module GF.Grammar.MMacros where
-
-import GF.Data.Operations
---import GF.Data.Zipper
-
-import GF.Grammar.Grammar
-import GF.Grammar.Printer
-import GF.Infra.Ident
---import GF.Compile.Refresh
-import GF.Grammar.Values
-----import GrammarST
-import GF.Grammar.Macros
-
-import Control.Monad
-import GF.Text.Pretty
-
--- ** Some more abstractions on grammars, esp. for Edit
-
-{-
-nodeTree :: Tree -> TrNode
-argsTree :: Tree -> [Tree]
-
-nodeTree (Tr (n,_)) = n
-argsTree (Tr (_,ts)) = ts
-
-isFocusNode    :: TrNode -> Bool
-bindsNode      :: TrNode -> Binds
-atomNode       :: TrNode -> Atom
-valNode        :: TrNode -> Val
-constrsNode    :: TrNode -> Constraints
-metaSubstsNode :: TrNode -> MetaSubst
-
-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 :: Tree -> Atom
-valTree  :: Tree -> Val
-
-atomTree = atomNode . nodeTree 
-valTree  = valNode  . nodeTree
-
-mkNode :: Binds -> Atom -> Val -> (Constraints, MetaSubst) -> TrNode
-mkNode binds atom vtyp cs = N (binds,atom,vtyp,cs,False)
-
-metasTree :: Tree ->  [MetaId]
-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
--}
-
-type Var = Ident
-
-uVal :: Val
-uVal = vClos uExp
-
-vClos :: Exp -> Val
-vClos = VClos []
-
-uExp :: Exp
-uExp = Meta meta0
-
-mExp, mExp0 :: Exp
-mExp  = Meta meta0
-mExp0 = mExp
-
-meta2exp :: MetaId -> Exp
-meta2exp = Meta
-{-
-atomC :: Fun -> Atom
-atomC = AtC
-
-funAtom :: Atom -> Err Fun
-funAtom a = case a of
-  AtC f -> return f
-  _ -> prtBad "not function head" a
-
-atomIsMeta :: Atom -> Bool
-atomIsMeta atom = case atom of
-  AtM _ -> True
-  _   -> False
-
-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 (Q cat) [Meta i | i <- [1..length cont]]
-
-val2cat :: Val -> Err Cat
-val2cat v = liftM valCat (val2exp v)
-
-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 b x t   -> let y = mkFreshVarX ss x in 
-                   Abs b y (substTerm (y:ss) ((x, Vr y):g) t)
-  Prod b x a t  -> let y = mkFreshVarX ss x in 
-                   Prod b y (substTerm ss g a) (substTerm (y:ss) ((x,Vr y):g) t)
-  _           -> c
-
-metaSubstExp :: MetaSubst -> [(MetaId,Exp)]
-metaSubstExp msubst = [(m, fromErr (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
-
--- | done in a state monad
---alphaFreshAll :: [Var] -> [Exp] -> Err [Exp]
---alphaFreshAll vs = mapM $ alphaFresh vs
-
--- | for display
-val2exp :: Val -> Err Exp
-val2exp = val2expP False 
-
--- | for type checking
-val2expSafe :: Val -> Err Exp
-val2expSafe = val2expP True  
-
-val2expP :: Bool -> Val -> Err Exp
-val2expP safe v = case v of
-
-  VClos g@(_:_) e@(Meta _) -> if safe 
-                              then Bad (render ("unsafe value substitution" <+> ppValue Unqualified 0 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 $ Q c
-  VGen i x  -> if safe 
-               then Bad (render ("unsafe val2exp" <+> ppValue Unqualified 0 v))
-               else return $ Vr $ x  --- in editing, no alpha conversions presentv
-  VRecType xs->do xs <- mapM (\(l,v) -> val2expP safe v >>= \e -> return (l,e)) xs
-                  return (RecType xs)
-  VType     -> return typeType
- 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 Explicit)) 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
-
-int2var :: Int -> Ident
-int2var = identS . ('$':) . show
-
-meta0 :: MetaId
-meta0 = 0
-
-termMeta0 :: Term
-termMeta0 = Meta meta0
-
-identVar :: Term -> Err Ident
-identVar (Vr x) = return x
-identVar _ = Bad "not a variable"
-
-
--- | light-weight rename for user interaction; also change names of internal vars
-qualifTerm :: ModuleName -> Term -> Term
-qualifTerm m  = qualif [] where
-  qualif xs t = case t of
-    Abs b x t -> let x' = chV x in Abs b x' $ qualif (x':xs) t
-    Prod b x a t -> Prod b x (qualif xs a) $ qualif (x:xs) t
-    Vr x -> let x' = chV x in if (elem x' xs) then (Vr x') else (Q (m,x))
-    Cn c  -> Q (m,c)
-    Con c -> QC (m,c)
-    _ -> composSafeOp (qualif xs) t
-  chV x = string2var $ ident2raw x
-    
-string2var :: RawIdent -> Ident
-string2var s = case showRawIdent s of
-  c:'_':i -> identV (rawIdentS [c]) (readIntArg i) ---
-  _       -> identC s
-
--- | reindex variables so that they tell nesting depth level
-reindexTerm :: Term -> Term
-reindexTerm = qualif (0,[]) where
-  qualif dg@(d,g) t = case t of
-    Abs b x t    -> let x' = ind x d in Abs b x' $ qualif (d+1, (x,x'):g) t
-    Prod b x a t -> let x' = ind x d in Prod b x' (qualif dg a) $ qualif (d+1, (x,x'):g) t
-    Vr x       -> Vr $ look x g
-    _ -> composSafeOp (qualif dg) t
-  look x  = maybe x id . lookup x --- if x is not in scope it is unchanged
-  ind x d = identC $ ident2raw x `prefixRawIdent` rawIdentS "_" `prefixRawIdent` rawIdentS (show d)
-
-{-
--- this method works for context-free abstract syntax
--- and is meant to be used in simple embedded GF applications
-
-exp2tree :: Exp -> Err Tree
-exp2tree e = do
-  (bs,f,xs) <- termForm e
-  cont <- case bs of
-    [] -> return []
-    _  -> prtBad "cannot convert bindings in" e
-  at <- case f of
-    Q  m c -> return $ AtC (m,c)
-    QC m c -> return $ AtC (m,c)
-    Meta m -> return $ AtM m
-    K s    -> return $ AtL s
-    EInt n -> return $ AtI n
-    EFloat n -> return $ AtF n
-    _ -> prtBad "cannot convert to atom" f
-  ts <- mapM exp2tree xs
-  return $ Tr (N (cont,at,uVal,([],[]),True),ts)
--}
diff --git a/src/compiler/GF/Grammar/Macros.hs b/src/compiler/GF/Grammar/Macros.hs
index 98d784fda..011e5be9d 100644
--- a/src/compiler/GF/Grammar/Macros.hs
+++ b/src/compiler/GF/Grammar/Macros.hs
@@ -565,7 +565,6 @@ strsFromTerm t = case t of
 stringFromTerm :: Term -> String
 stringFromTerm = err id (ifNull "" (sstr . head)) . strsFromTerm
 
-
 getTableType :: TInfo -> Err Type
 getTableType i = case i of
   TTyped ty -> return ty
@@ -646,14 +645,3 @@ topoSortJments2 (m,mi) = do
            (topoTest2 (allDependencies (==m) (jments mi)))
   return
     [[(i,info) | i<-is,Ok info<-[lookupTree showIdent i (jments mi)]] | is<-iss]
-{-
--- | Smart constructor for PSeq
-pSeq p1 p2 =
-  case (p1,p2) of
-    (PString s1,PString s2) -> PString (s1++s2)
-    (PSeq p11 (PString s1),PString s2) -> PSeq p11 (PString (s1++s2))
-    (PString s1,PSeq (PString s2) p22) -> PSeq (PString (s1++s2)) p22
-    (PSeq p11 (PString s1),PSeq (PString s2) p22) ->
-        PSeq p11 (PSeq (PString (s1++s2)) p22)
-    _ -> PSeq p1 p2
--}
diff --git a/src/compiler/GF/Grammar/Unify.hs b/src/compiler/GF/Grammar/Unify.hs
index b4960b635..3a7f0edef 100644
--- a/src/compiler/GF/Grammar/Unify.hs
+++ b/src/compiler/GF/Grammar/Unify.hs
@@ -27,8 +27,8 @@ unifyVal :: Constraints -> Err (Constraints,MetaSubst)
 unifyVal cs0 = do
   let (cs1,cs2) = partition notSolvable cs0 
   let (us,vs) = unzip cs2
-  us' <- mapM val2exp us
-  vs' <- mapM val2exp vs
+  let us' = map val2term us
+  let vs' = map val2term vs
   let (ms,cs) = unifyAll (zip us' vs') []
   return (cs1 ++ [(VClos [] t, VClos [] u) | (t,u) <- cs], 
           [(m,          VClos [] t) | (m,t) <- ms])
@@ -88,6 +88,16 @@ substMetas subst trm = case trm of
      _ -> trm
    _ -> composSafeOp (substMetas subst) trm
 
+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 b x t   -> let y = mkFreshVarX ss x in 
+                   Abs b y (substTerm (y:ss) ((x, Vr y):g) t)
+  Prod b x a t  -> let y = mkFreshVarX ss x in 
+                   Prod b y (substTerm ss g a) (substTerm (y:ss) ((x,Vr y):g) t)
+  _           -> c
+
 occCheck :: MetaId -> Term -> Bool
 occCheck s u = case u of
     Meta v  -> s == v
@@ -95,3 +105,11 @@ occCheck s u = case u of
     Abs _ x b -> occCheck s b
     _       -> False
 
+val2term :: Val -> Term
+val2term v = case v of
+  VClos g e   -> substTerm [] (map (\(x,v) -> (x,val2term v)) g) e
+  VApp f c    -> App (val2term f) (val2term c)
+  VCn c       -> Q c
+  VGen i x    -> Vr x
+  VRecType xs -> RecType (map (\(l,v) -> (l,val2term v)) xs)
+  VType       -> typeType
diff --git a/src/compiler/GF/Grammar/Values.hs b/src/compiler/GF/Grammar/Values.hs
index 7bfc8a24b..3cfd79ad7 100644
--- a/src/compiler/GF/Grammar/Values.hs
+++ b/src/compiler/GF/Grammar/Values.hs
@@ -13,45 +13,26 @@
 -----------------------------------------------------------------------------
 
 module GF.Grammar.Values (-- ** Values used in TC type checking
-	       Exp, Val(..), Env,
+	       Val(..), Env,
 	       -- ** Annotated tree used in editing
---Z	       Tree, TrNode(..), Atom(..), 
                Binds, Constraints, MetaSubst,
 	       -- ** For TC
 	       valAbsInt, valAbsFloat, valAbsString, vType,
 	       isPredefCat,
 	       eType, 
---Z tree2exp, loc2treeFocus
 	      ) where
 
---import GF.Data.Operations
----Z import GF.Data.Zipper
-
 import GF.Infra.Ident
 import GF.Grammar.Grammar
 import GF.Grammar.Predef
 
 -- values used in TC type checking
 
-type Exp = Term
-
-data Val = VGen Int Ident | VApp Val Val | VCn QIdent | VRecType [(Label,Val)] | VType | VClos Env Exp 
+data Val = VGen Int Ident | VApp Val Val | VCn QIdent | VRecType [(Label,Val)] | VType | VClos Env Term
   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 MetaId | AtV Ident | AtL String | AtI Integer | AtF Double
-  deriving (Eq,Show)
--}
 type Binds = [(Ident,Val)]
 type Constraints = [(Val,Val)]
 type MetaSubst = [(MetaId,Val)]
@@ -71,26 +52,5 @@ valAbsString = VCn (cPredefAbs, cString)
 vType :: Val
 vType = VType
 
-eType :: Exp
+eType :: Term
 eType = Sort cType
-
-{-
-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
-    AtF s -> EFloat s
-  bi' = map fst bi
-  ts' = map tree2exp ts
-
-loc2treeFocus :: Loc TrNode -> Tree
-loc2treeFocus (Loc (Tr (a,ts),p)) = 
-  loc2tree (Loc (Tr (mark a, map (mapTr nomark) ts), mapPath nomark p)) 
- where 
-   (mark, nomark) = (\(N (a,b,c,d,_)) -> N(a,b,c,d,True), 
-                     \(N (a,b,c,d,_)) -> N(a,b,c,d,False))
--}