diff --git a/AST.hs b/AST.hs
--- a/AST.hs
+++ b/AST.hs
@@ -1,67 +1,102 @@
 {-# LANGUAGE
  FlexibleInstances,
- PatternGuards,
  BangPatterns,
  FlexibleContexts,
- TupleSections
+ TemplateHaskell,
+ NoMonomorphismRestriction
  #-}
-
 module AST where
 
 import qualified Data.Foldable as F
-import Data.List
-import Data.Maybe
-import Data.Monoid
 import Data.Functor
-import qualified Data.Map as M
-import Data.Map (Map)
 import qualified Data.Set as S
-import Control.Monad.RWS (RWST)
-import Control.Monad.State.Class (MonadState(), get, modify)
+import qualified Data.Map as M
+import Data.Maybe
+import Data.Monoid
+import Data.List
 
-import Choice
+import Control.Lens
 
------------------------------
----  abstract syntax tree ---
------------------------------
 
 type Name = String
 
-infixr 0 ~>
-infixr 0 ~~>
-(~>) = forall ""
-(~~>) = imp_forall ""
-
 data Spine = Spine Name [Type]
            | Abs Name Type Spine 
            deriving (Eq)
+                    
+instance Monoid Spine where 
+  mempty  = undefined
+  mappend = undefined
+instance Monoid Bool where 
+  mempty  = undefined
+  mappend = undefined
 
+type Kind = Spine
 type Type = Spine
 type Term = Spine
+data Decl = Predicate { _declIsSound :: !Bool
+                      , _declName :: !Name
+                      , _declType :: !Type
+                      , _declConstructors :: ![(Bool,(Name,Type))] 
+                      }
+          | Query { _declName :: !Name
+                  , _declType :: !Type
+                  }
+          | Define { _declIsSound :: !Bool
+                   , _declName :: !Name
+                   , _declValue :: !Term
+                   , _declType :: !Type
+                   }
+          deriving (Eq)
 
-data Predicate = Predicate { predIsSound :: !Bool, predName :: !Name, predType :: !Type, predConstructors :: ![(Bool,(Name,Type))] }
-               | Query { predName :: !Name, predType :: !Spine}
-               | Define { predIsSound :: !Bool, predName :: !Name, predValue :: !Spine, predType :: !Type}
-               deriving (Eq)
 
-class ValueTracker c where
-  putValue :: Integer -> c -> c
-  takeValue :: c -> Integer
+data PredData = PredData { _dataFamily :: Maybe Name
+                         , _dataSequential :: Bool
+                         , _dataPriority :: Integer
+                         , _dataSound :: Bool
+                         } 
 
-instance ValueTracker Integer where
-  putValue _ i = i
-  takeValue i = i
+data FlatPred = FlatPred { _predData :: PredData
+                         , _predName :: Name
+                         , _predType :: Type
+                         , _predKind :: Kind
+                         }
+$(makeLenses ''PredData)
+$(makeLenses ''FlatPred)
+$(makeLenses ''Decl)
 
-getNew :: (Functor m, MonadState c m, ValueTracker c) => m String
-getNew = do
-  st <- takeValue <$> get
-  let n = 1 + st
-  modify $ putValue n
-  return $ show n
-  
-getNewWith :: (Functor f, MonadState c f, ValueTracker c) => String -> f String
-getNewWith s = {- (++s) <$> -} getNew
+predFamily = predData . dataFamily
+predSequential = predData . dataSequential
+predPriority = predData . dataPriority
+predSound = predData . dataSound
 
+-------------------------
+---  Constraint types ---
+-------------------------
+
+data Quant = Forall | Exists deriving (Eq) 
+
+infix 2 :=:  
+infix 2 :@:  
+infixr 1 :&:
+
+-- we can make this data structure mostly strict since the only time we don't 
+-- traverse it is when we fail, and in order to fail, we always have to traverse
+-- the lhs!
+data SCons = !Term :@: !Type
+           | !Spine :=: !Spine
+           deriving (Eq)
+data Constraint = SCons [SCons]
+                  -- we don't necessarily have to traverse the rhs of a combination
+                  -- so we can make it lazy
+                | !Constraint :&: Constraint 
+                | Bind !Quant !Name !Type !Constraint
+                deriving (Eq)
+
+
+-------------------------
+---  Pretty Printing  ---
+-------------------------
 showWithParens t = if (case t of
                           Abs{} -> True
                           Spine "#infer#" _ -> True
@@ -78,7 +113,6 @@
 isOperator ('#':_) = False
 isOperator (a:_) = not $ elem a ('_':['a'..'z']++['A'..'Z']++['0'..'9'])
 
-
 instance Show Spine where
   show (Spine ['\'',c,'\''] []) = show c
   show (Spine "#infer#" [_, Abs nm t t']) = "<"++nm++" : "++show t++"> "++show t'
@@ -92,209 +126,32 @@
   show (Spine "#imp_abs#" [_,Abs nm ty t]) = "?λ "++nm++" : "++showWithParens ty++" . "++show t
   show (Spine nm l@[_ , Abs _ _ _]) | isOperator nm = "("++nm++") "++show (Spine "" l)
   show (Spine nm (t:t':l)) | isOperator nm = "( "++showWithParens t++" "++nm++" "++ show t'++" )"++show (Spine "" l)
-  show (Spine h l) = h++concatMap showWithParens' l
-     where showWithParens' t = " "++if case t of
+  show (Spine h l) = h++concatMap showWithParens l
+     where showWithParens t = " "++if case t of
                           Abs{} -> True
                           Spine "#tycon#" _ -> False
                           Spine _ lst -> not $ null lst
                       then "("++show t++")" else show t 
   show (Abs nm ty t) = "λ "++nm++" : "++showWithParens ty++" . "++show t
 
-showT True = "defn "
-showT False = "unsound "
 
-instance Show Predicate where
-  show (Predicate s nm ty []) = showT s ++ nm ++ " : " ++ show ty
-  show (Predicate s nm ty (a:cons)) =
-    showT s++ nm ++ " : " ++ show ty++showSingle a ++ concatMap (\x-> showSingle x) cons
-      where showSingle (b,(nm,ty)) = (if b then "\n  >| " else "\n   | ") ++nm ++ " = " ++ show ty
-  show (Query nm val) = "query " ++ nm ++ " = " ++ show val
-  show (Define s nm val ty) = showT s ++ nm ++ " : " ++ show ty ++"\n as "++show val
-                                               
-var !nm = Spine nm []
-atomName = "prop"
-tipeName = "type"
-kindName = "#kind#"
 
-atom = var atomName
-ty_hole = var "#hole#"
-tipe = var tipeName
-kind = var kindName  -- can be either a type or an atom
-ascribe a t = Spine ("#ascribe#") [t, a]
-dontcheck t = Spine ("#dontcheck#") [t]
-forall x tyA v = Spine ("#forall#") [tyA, Abs x tyA v]
-exists x tyA v = Spine ("#exists#") [tyA, Abs x tyA v]
-pack e tau imp tp interface = Spine "pack" [tp, Abs imp tp interface, tau, e]
-open cl (imp,ty) (p,iface) cty inexp = Spine "#open#" [cl, ty,Abs imp ty iface, Abs imp ty (Abs p iface cty), Abs imp ty (Abs p iface inexp)] 
-infer x tyA v = Spine ("#infer#") [tyA, Abs x tyA v]
-
-imp_forall x tyA v = Spine ("#imp_forall#") [tyA, Abs x tyA v]
-imp_abs x tyA v = Spine ("#imp_abs#") [tyA, Abs x tyA v]
-tycon nm val = Spine "#tycon#" [Spine nm [val]]
----------------------
----  substitution ---
----------------------
-
-type Substitution = M.Map Name Spine
-
-infixr 1 |->
-infixr 0 ***
-m1 *** m2 = M.union m2 $ subst m2 <$> m1
-(|->) = M.singleton
-(!) = flip M.lookup
-
-
-findTyconInPrefix nm = fip []
-  where fip l (Spine "#tycon#" [Spine nm' [v]]:r) | nm == nm' = Just (v, reverse l++r)
-        fip l (a@(Spine "#tycon#" [Spine _ [_]]):r) = fip (a:l) r
-        fip _ _ = Nothing
-
-apply :: Spine -> Spine -> Spine
-apply !a !l = rebuildSpine a [l]
-
-rebuildSpine :: Spine -> [Spine] -> Spine
-rebuildSpine s [] = s
-rebuildSpine (Spine "#imp_abs#" [_, Abs nm ty rst]) apps = case findTyconInPrefix nm apps of 
-  Just (v, apps) -> rebuildSpine (Abs nm ty rst) (v:apps)
-  Nothing -> seq sp $ if ty == atom && S.notMember nm (freeVariables rs) then rs else irs 
-                      -- proof irrelevance hack
-                      -- we know we can prove that type "prop" is inhabited
-                      -- irs - the proof doesn't matter
-                      -- rs - the proof matters
-                      -- irs - here, the proof might matter, but we don't know if we can prove the thing, 
-                      -- so we need to try
-     where nm' = newNameFor nm $ freeVariables apps
-           sp = subst (nm |-> var nm') rst
-           rs = rebuildSpine sp apps
-           irs = infer nm ty rs
-rebuildSpine (Spine c apps) apps' = Spine c $ apps ++ apps'
-rebuildSpine (Abs nm _ rst) (a:apps') = let sp = subst (nm |-> a) $ rst
-                                        in seq sp $ rebuildSpine sp apps'
-
-newNameFor :: Name -> S.Set Name -> Name
-newNameFor nm fv = nm'
-  where nm' = fromJust $ find free $ nm:map (\s -> show s ++ "/?") [0..]
-        free k = not $ S.member k fv
-        
-newName :: Name -> Map Name Spine -> S.Set Name -> (Name, Map Name Spine, S.Set Name)
-newName "" so fo = ("",so,fo)
-newName nm so fo = (nm',s',f')
-  where s = M.delete nm so  
-        -- could reduce the size of the free variable set here, but for efficiency it is not really necessary
-        -- for beautification of output it is
-        (s',f') = if nm == nm' then (s,fo) else (M.insert nm (var nm') s , S.insert nm' fo)
-        nm' = fromJust $ find free $ nm:map (\s -> show s ++ "/") [0..]
-        fv = mappend (M.keysSet s) (freeVariables s)
-        free k = not $ S.member k fv
-
-class Subst a where
-  substFree :: Substitution -> S.Set Name -> a -> a
-  
-
-getImpliedFamilies s = S.intersection fs $ gif s
-  where fs = freeVariables s
-        gif (Spine "#imp_forall#" [ty,a]) = (case getFamilyM ty of
-          Nothing -> id
-          Just f -> S.insert f) $ gif ty `S.union` gif a 
-        gif (Spine a l) = mconcat $ gif <$> l
-        gif (Abs _ ty l) = S.union (gif ty) (gif l)
-        
-subst s = substFree s $ freeVariables s
-
-class Alpha a where  
-  alphaConvert :: S.Set Name -> a -> a
-  rebuildFromMem :: Map Name Name -> a -> a  
-  
-instance Subst a => Subst [a] where
-  substFree s f t = substFree s f <$> t
-  
-instance Alpha a => Alpha [a] where  
-  alphaConvert s l = alphaConvert s <$> l
-  rebuildFromMem s l = rebuildFromMem s <$> l
-  
-instance (Subst a, Subst b) => Subst (a,b) where
-  substFree s f ~(a,b) = (substFree s f a , substFree s f b)
-  
-instance Subst Spine where
-  substFree s f sp@(Spine "#imp_forall#" [_, Abs nm tp rst]) = case "" /= nm && S.member nm f && not (S.null $ S.intersection (M.keysSet s) $ freeVariables sp) of
-    False -> imp_forall nm (substFree s f tp) $ substFree (M.delete nm s) f rst
-    True -> error $ 
-            "can not capture free variables because implicits quantifiers can not alpha convert: "++ show sp 
-            ++ "\n\tfor: "++show s
-  substFree s f sp@(Spine "#imp_abs#" [_, Abs nm tp rst]) = case "" /= nm && S.member nm f && not (S.null $ S.intersection (M.keysSet s) $ freeVariables sp) of
-    False  -> imp_abs nm (substFree s f tp) $ substFree (M.delete nm s) f rst 
-    True   -> error $ 
-              "can not capture free variables because implicit binds can not alpha convert: "++ show sp
-              ++ "\n\tfor: "++show s
-  substFree s f (Abs nm tp rst) = Abs nm' (substFree s f tp) $ substFree s' f' rst
-    where (nm',s',f') = newName nm s f
-  substFree s f (Spine "#tycon#" [Spine c [v]]) = Spine "#tycon#" [Spine c [substFree s f v]]
-  substFree s f (Spine nm apps) = let apps' = substFree s f <$> apps  in
-    case s ! nm of
-      Just nm -> rebuildSpine nm apps'
-      _ -> Spine nm apps'
-      
-instance Alpha Spine where
-  alphaConvert s (Spine "#imp_forall#" [_,Abs a ty r]) = imp_forall a ty $ alphaConvert (S.insert a s) r
-  alphaConvert s (Spine "#imp_abs#" [_,Abs a ty r]) = imp_abs a ty $ alphaConvert (S.insert a s) r
-  alphaConvert s (Abs nm ty r) = Abs nm' (alphaConvert s ty) $ alphaConvert (S.insert nm' s) r
-    where nm' = newNameFor nm s
-  alphaConvert s (Spine a l) = Spine a $ alphaConvert s l
-  
-  rebuildFromMem s (Spine "#imp_forall#" [_,Abs a ty r]) = imp_forall a (rebuildFromMem s ty) $ rebuildFromMem (M.delete a s) r
-  rebuildFromMem s (Spine "#imp_abs#" [_,Abs a ty r]) = imp_abs a (rebuildFromMem s ty) $ rebuildFromMem (M.delete a s) r
-  rebuildFromMem s (Abs nm ty r) = Abs (fromMaybe nm $ M.lookup nm s) (rebuildFromMem s ty) $ rebuildFromMem s r
-  rebuildFromMem s (Spine a l) = Spine a' $ rebuildFromMem s l
-    where a' = fromMaybe a $ M.lookup a s
-                                 
-  
-instance Subst Predicate where
-  substFree sub f (Predicate s nm ty cons) = Predicate s nm (substFree sub f ty) ((\(b,(nm,t)) -> (b,(nm,substFree sub f t))) <$> cons)
-  substFree sub f (Query nm ty) = Query nm (substFree sub f ty)
-  substFree sub f (Define s nm val ty) = Define s nm (substFree sub f val) (substFree sub f ty)
-  
-class FV a where         
-  freeVariables :: a -> S.Set Name
-instance (FV a, F.Foldable f) => FV (f a) where
-  freeVariables m = F.foldMap freeVariables m
-instance FV Spine where
-  freeVariables t = case t of
-    Abs nm t p -> (S.delete nm $ freeVariables p) `mappend` freeVariables t
-    Spine "#tycon#" [Spine nm [v]] -> freeVariables v
-    Spine "#dontcheck#" [v] -> freeVariables v
-    Spine ['\'',_,'\''] [] -> mempty
-    Spine head others -> mappend (S.singleton head) $ mconcat $ map freeVariables others
+instance Show Decl where
+  show a = case a of
+    Predicate s nm ty [] -> showDef s ++ nm ++ " : " ++ show ty
+    Predicate s nm ty (a:cons) ->
+      showDef s++ nm ++ " : " ++ show ty++showSingle a ++ concatMap (\x-> showSingle x) cons
+      where showSingle (b,(nm,ty)) = (if b then "\n  >| " else "\n   | ") ++nm ++ " = " ++ show ty
+    Query nm val -> "query " ++ nm ++ " = " ++ show val
+    Define s nm val ty -> showDef s ++ nm ++ " : " ++ show ty ++"\n as "++show val
+    where showDef True = "defn "
+          showDef False = "unsound "
 
 
-  
--------------------------
----  Constraint types ---
--------------------------
-
-data Quant = Forall | Exists deriving (Eq) 
-
 instance Show Quant where
   show Forall = "∀"
-  show Exists = "∃"
-
--- as ineficient as it is, I'll make this the constraint representation.
-infix 2 :=:  
-infix 2 :@:  
-infixr 1 :&:
-
--- we can make this data structure mostly strict since the only time we don't 
--- traverse it is when we fail, and in order to fail, we always have to traverse
--- the lhs!
-data SCons = !Term :@: !Type
-           | !Spine :=: !Spine
-           deriving (Eq)
-data Constraint = SCons [SCons]
-                  -- we don't necessarily have to traverse the rhs of a combination
-                  -- so we can make it lazy
-                | !Constraint :&: Constraint 
-                | Bind !Quant !Name !Type !Constraint
-                deriving (Eq)
-                         
+  show Exists = "∃"  
+  
 instance Show SCons where
   show (a :=: b) = show a++" ≐ "++show b
   show (a :@: b) = show a++" ∈ "++show b
@@ -308,11 +165,12 @@
     where showWithParens Bind{} = show c
           showWithParens _ = "( "++show c++" )"
 
+-----------------------------
+--- Constraint Properties ---          
+-----------------------------          
 instance Monoid Constraint where
   mempty = SCons []
-  
   mappend (SCons []) b = b
-
   mappend a (SCons []) = a
   mappend (SCons a) (SCons b) = SCons $ a++b
   mappend a b = a :&: b
@@ -325,115 +183,54 @@
  "memptymappend" flip mappend mempty = id
  #-}
 
-instance Subst SCons where
-  substFree s f c = case c of
-    s1 :@: s2 -> subq s f (:@:) s1 s2
-    s1 :=: s2 -> subq s f (:=:) s1 s2
-    
-instance Subst Constraint where
-  substFree s f c = case c of
-    SCons l -> SCons $ map (substFree s f) l
-    s1 :&: s2 -> subq s f (:&:) s1 s2
-    Bind q nm t c -> Bind q nm' (substFree s f t) $ substFree s' f' c
-      where (nm',s',f') = newName nm s f
-            
-subq s f e c1 c2 = e (substFree s f c1) (substFree s f c2)
 
-(∃) = Bind Exists
-(∀) = Bind Forall
-  
-infixr 0 <<$>
-(<<$>) f m = ( \(a,b) -> (f a, b)) <$> m
-
-regenM e a b = do
-  (a',s1) <- regenWithMem a 
-  (b',s2) <- regenWithMem b 
-  return $ (e a' b', M.union s1 s2)
-regen e a b = do
-  a' <- regenAbsVars a 
-  b' <- regenAbsVars b 
-  return $ e a' b'  
-  
-class RegenAbsVars a where
-  regenAbsVars :: (Functor f, MonadState c f, ValueTracker c) => a -> f a
-  regenWithMem :: (Functor f, MonadState c f, ValueTracker c) => a -> f (a, Map Name Name)
-  
-instance RegenAbsVars l => RegenAbsVars [l] where
-  regenAbsVars cons = mapM regenAbsVars cons
-  
-  regenWithMem cons = together <$> mapM regenWithMem cons
-    where together f = (l',foldr M.union mempty ss)
-            where (l',ss) = unzip f
-  
+----------------------
+--- Free Variables ---
+----------------------
+class FV a where         
+  freeVariables :: a -> S.Set Name
+instance (FV a, F.Foldable f) => FV (f a) where
+  freeVariables m = F.foldMap freeVariables m
+instance FV Spine where
+  freeVariables t = case t of
+    Abs nm t p -> (S.delete nm $ freeVariables p) `mappend` freeVariables t
+    Spine "#tycon#" [Spine nm [v]] -> freeVariables v
+    Spine "#dontcheck#" [v] -> freeVariables v
+    Spine ['\'',_,'\''] [] -> mempty
+    Spine head others -> mappend (S.singleton head) $ mconcat $ map freeVariables others
 
-  
-instance RegenAbsVars Spine where  
-  regenAbsVars (Spine "#imp_forall#" [_,Abs a ty r]) = imp_forall a ty <$> regenAbsVars r
-  regenAbsVars (Spine "#imp_abs#" [_,Abs a ty r]) = imp_abs a ty <$> regenAbsVars r
-  regenAbsVars (Abs a ty r) = do
-    a' <- getNewWith $ "@rega"
-    ty' <- regenAbsVars ty
-    r' <- regenAbsVars $ subst (a |-> var a') r
-    return $ Abs a' ty' r'
-  regenAbsVars (Spine a l) = Spine a <$> regenAbsVars l
+instance FV FlatPred where
+  freeVariables p = freeVariables (p^.predType) `S.union` freeVariables (p^.predKind)
   
-  regenWithMem (Spine "#imp_forall#" [_,Abs a ty r]) = imp_forall a ty <<$> regenWithMem r
-  regenWithMem (Spine "#imp_abs#" [_,Abs a ty r]) = imp_abs a ty <<$> regenWithMem r
-  regenWithMem (Abs a ty r) = do
-    a' <- getNewWith $ "@regm"
-    (ty',s1) <- regenWithMem ty
-    (r', s2) <- regenWithMem $ subst (a |-> var a') r
-    return $ (Abs a' ty' r', M.insert a' a $ M.union s1 s2)
-  regenWithMem (Spine a l) = Spine a <<$> regenWithMem l
-
+--------------------------------
+--- Builtin Spines and types ---
+--------------------------------
+infixr 0 ~>
+infixr 0 ~~>
+(~>) = forall ""
+(~~>) = imp_forall ""
 
+var !nm = Spine nm []
 
-instance RegenAbsVars SCons where
-  regenAbsVars cons = case cons of
-    a :=: b -> regen (:=:) a b
-    a :@: b -> regen (:@:) a b
-    
-  regenWithMem cons = case cons of
-    a :=: b -> regenM (:=:) a b
-    a :@: b -> regenM (:@:) a b    
-      
-instance RegenAbsVars Constraint where  
-  regenAbsVars cons = case cons of
-    Bind q nm ty cons -> do
-      ty' <- regenAbsVars ty
-      case nm of
-        "" -> do
-          nm' <- getNewWith "@newer"
-          let sub = nm |-> var nm'
-          Bind q nm' ty' <$> regenAbsVars (subst sub cons)
-        _ -> Bind q nm ty' <$> regenAbsVars cons
-    SCons l -> SCons <$> regenAbsVars l
-    a :&: b -> regen (:&:) a b
-    
-  regenWithMem cons = case cons of
-    Bind q nm ty cons -> do
-      (ty',s1) <- regenWithMem ty
-      nm' <- getNewWith "@regm'"
-      let sub = nm |-> var nm'
-      (cons',s2) <- regenWithMem $ subst sub cons
-      return (Bind q nm' ty' cons', M.insert nm' nm $ M.union s1 s2)
-    SCons l -> SCons <<$> regenWithMem l
-    a :&: b -> regenM (:&:) a b    
-  
-getFamily v = fromMaybe (error ("values don't have families: "++show v)) $ getFamilyM v
+atomName = "prop"
+tipeName = "type"
+kindName = "#kind#"
 
-getFamilyM (Spine "#infer#" [_, Abs _ _ lm]) = getFamilyM lm
-getFamilyM (Spine "#ascribe#"  (_:v:l)) = getFamilyM (rebuildSpine v l)
-getFamilyM (Spine "#dontcheck#"  [v]) = getFamilyM v
-getFamilyM (Spine "#forall#" [_, Abs _ _ lm]) = getFamilyM lm
-getFamilyM (Spine "#imp_forall#" [_, Abs _ _ lm]) = getFamilyM lm
-getFamilyM (Spine "#exists#" [_, Abs _ _ lm]) = getFamilyM lm
-getFamilyM (Spine "#open#" (_:_:c:_)) = getFamilyM c
-getFamilyM (Spine "open" (_:_:c:_)) = getFamilyM c
-getFamilyM (Spine "pack" [_,_,_,e]) = getFamilyM e
-getFamilyM (Spine nm' _) = Just nm'
-getFamilyM v = Nothing
+atom = var atomName
+ty_hole = var "#hole#"
+tipe = var tipeName
+kind = var kindName  -- can be either a type or an atom
+ascribe a t = Spine ("#ascribe#") [t, a]
+dontcheck t = Spine ("#dontcheck#") [t]
+forall x tyA v = Spine ("#forall#") [tyA, Abs x tyA v]
+exists x tyA v = Spine ("#exists#") [tyA, Abs x tyA v]
+pack e tau imp tp interface = Spine "pack" [tp, Abs imp tp interface, tau, e]
+open cl (imp,ty) (p,iface) cty inexp = Spine "#open#" [cl, ty,Abs imp ty iface, Abs imp ty (Abs p iface cty), Abs imp ty (Abs p iface inexp)] 
+infer x tyA v = Spine ("#infer#") [tyA, Abs x tyA v]
 
+imp_forall x tyA v = Spine ("#imp_forall#") [tyA, Abs x tyA v]
+imp_abs x tyA v = Spine ("#imp_abs#") [tyA, Abs x tyA v]
+tycon nm val = Spine "#tycon#" [Spine nm [val]]
 
 consts = [ (atomName , tipe)
          , (tipeName , kind)
@@ -467,7 +264,7 @@
          ]
 
 
-anonymous ty = ((False,100),ty)
+anonymous ty = ((False,10000),ty)
 
 envSet = S.fromList $ map fst consts
 
diff --git a/Context.hs b/Context.hs
--- a/Context.hs
+++ b/Context.hs
@@ -4,6 +4,7 @@
 module Context where
 
 import AST
+import Substitution
 import Data.Monoid
 import Data.Functor
 import qualified Data.Map as M
diff --git a/HOU.hs b/HOU.hs
--- a/HOU.hs
+++ b/HOU.hs
@@ -9,6 +9,7 @@
 
 import Choice
 import AST
+import Substitution
 import Context
 import TopoSortAxioms
 import Control.Monad.State (StateT, forM_,runStateT, modify, get,put, State, runState)
@@ -20,28 +21,31 @@
 import qualified Data.Foldable as F
 import Data.Foldable (foldlM)
 import Data.List
-import Data.Char (isUpper)
 import Data.Maybe
 import Data.Monoid
 import qualified Data.Map as M
 import qualified Data.Set as S
 import Debug.Trace
 
+import Control.Lens hiding (Choice(..))
+
 import System.IO.Unsafe
+import Data.IORef
 
-{-# INLINE level #-}
-level = 0
+{-# NOINLINE levelVar #-}
+levelVar :: IORef Int
+levelVar = unsafePerformIO $ newIORef 0
 
-{-# INLINE vtrace #-}
+{-# NOINLINE level #-}
+level = unsafePerformIO $ readIORef levelVar
+
 vtrace !i | i < level = trace
 vtrace !i = const id
 
-{-# INLINE vtraceShow #-}
 vtraceShow !i1 !i2 s v | i2 < level = trace $ s ++" : "++show v
 vtraceShow !i1 !i2 s v | i1 < level = trace s
 vtraceShow !i1 !i2 s v = id
 
-{-# INLINE throwTrace #-}
 throwTrace !i s = vtrace i s $ throwError s
 
 mtrace True = trace
@@ -62,21 +66,22 @@
   return $ l1 ++ l2
 flatten (SCons l) = return l
 
-type UnifyResult = Maybe (Substitution, [SCons])
+type UnifyResult = Maybe (Substitution, [SCons], Bool)
 
 unify :: Constraint -> Env Substitution
 unify cons =  do
   cons <- vtrace 5 ("CONSTRAINTS1: "++show cons) $ regenAbsVars cons
   cons <- vtrace 5 ("CONSTRAINTS2: "++show cons) $ flatten cons
   let uniWhile :: Substitution -> [SCons] -> Env (Substitution, [SCons])
-      uniWhile !sub !c' = fail "" <|> do
+      uniWhile !sub c' = fail "" <|> do
         exists <- getExists       
         c <- regenAbsVars c'     
-        let uniWith !wth !backup = searchIn c []
+        let uniWith !wth backup = searchIn c []
               where searchIn [] r = finish Nothing
                     searchIn (next:l) r = 
                       wth next $ \c1' -> case c1' of
-                            Just (sub',next') -> finish $ Just (sub', subst sub' (reverse r)++next'++subst sub' l)
+                            Just (sub',next',b) -> finish $ Just (sub', subst sub' (reverse r)++
+                                                                        (if b then (++next') else (next'++)) (subst sub' l))
                             Nothing -> searchIn l $ next:r
                     finish Nothing = backup
                     finish (Just (!sub', c')) = do
@@ -106,7 +111,7 @@
 
 newReturn return cons = return $ case cons of
   Nothing -> Nothing
-  Just cons -> Just (mempty, cons)
+  Just cons -> Just (mempty, cons, False)
 
 unifySearchAtom :: SCons -> CONT_T b Env UnifyResult
 unifySearchAtom (a :@: b) return = rightSearch a b $ newReturn return
@@ -123,43 +128,43 @@
 unifyOne _ return = return Nothing
 
 unifyEq cons@(a :=: b) = case (a,b) of 
-  (Spine "#ascribe#" (ty:v:l), b) -> return $ Just (mempty, [rebuildSpine v l :=: b])
-  (b,Spine "#ascribe#" (ty:v:l)) -> return $ Just (mempty, [b :=: rebuildSpine v l])
+  (Spine "#ascribe#" (ty:v:l), b) -> return $ Just (mempty, [rebuildSpine v l :=: b], False)
+  (b,Spine "#ascribe#" (ty:v:l)) -> return $ Just (mempty, [b :=: rebuildSpine v l], False)
   
   (Spine "#imp_forall#" [ty, l], b) -> vtrace 1 "-implicit-" $ do
     a' <- getNewWith "@aL"
     modifyCtxt $ addToTail "-implicit-" Exists a' ty
-    return $ Just (mempty, [l `apply` var a' :=: b , var a' :@: ty])
+    return $ Just (mempty, [l `apply` var a' :=: b , var a' :@: ty], False)
   (b, Spine "#imp_forall#" [ty, l]) -> vtrace 1 "-implicit-" $ do
     a' <- getNewWith "@aR"
     modifyCtxt $ addToTail "-implicit-" Exists a' ty
-    return $ Just (mempty,  [b :=: l `apply` var a' , var a' :@: ty])
+    return $ Just (mempty,  [b :=: l `apply` var a' , var a' :@: ty], False)
 
   (Spine "#imp_abs#" (ty:l:r), b) -> vtrace 1 ("-imp_abs- : "++show a ++ "\n\t"++show b) $ do
     a <- getNewWith "@iaL"
     modifyCtxt $ addToTail "-imp_abs-" Exists a ty
-    return $ Just (mempty, [rebuildSpine l (var a:r) :=: b , var a :@: ty])
+    return $ Just (mempty, [rebuildSpine l (var a:r) :=: b , var a :@: ty], False)
   (b, Spine "#imp_abs#" (ty:l:r)) -> vtrace 1 "-imp_abs-" $ do
     a <- getNewWith "@iaR"
     modifyCtxt $ addToTail "-imp_abs-" Exists a ty
-    return $ Just (mempty, [b :=: rebuildSpine l (var a:r) , var a :@: ty])
+    return $ Just (mempty, [b :=: rebuildSpine l (var a:r) , var a :@: ty], False)
 
   (Spine "#tycon#" [Spine nm [_]], Spine "#tycon#" [Spine nm' [_]]) | nm /= nm' -> throwTrace 0 $ "different type constraints: "++show cons
   (Spine "#tycon#" [Spine nm [val]], Spine "#tycon#" [Spine nm' [val']]) | nm == nm' -> 
-    return $ Just (mempty, [val :=: val'])
+    return $ Just (mempty, [val :=: val'], False)
 
   (Abs nm ty s , Abs nm' ty' s') -> vtrace 1 "-aa-" $ do
     modifyCtxt $ addToTail "-aa-" Forall nm ty
-    return $ Just (mempty, [ty :=: ty' , s :=: subst (nm' |-> var nm) s'])
+    return $ Just (mempty, [ty :=: ty' , s :=: subst (nm' |-> var nm) s'], False)
   (Abs nm ty s , s') -> vtraceShow 1 2 "-asL-" cons $ do
     modifyCtxt $ addToTail "-asL-" Forall nm ty
-    return $ Just (mempty, [s :=: s' `apply` var nm])
+    return $ Just (mempty, [s :=: s' `apply` var nm], False)
 
   (s, Abs nm ty s' ) -> vtraceShow 1 2 "-asR-" cons $ do
     modifyCtxt $ addToTail "-asR-" Forall nm ty
-    return $ Just (mempty, [s `apply` var nm :=: s'])
+    return $ Just (mempty, [s `apply` var nm :=: s'], False)
 
-  (s , s') | s == s' -> vtrace 1 "-eq-" $ return $ Just (mempty, [])
+  (s , s') | s == s' -> vtrace 1 "-eq-" $ return $ Just (mempty, [], False)
   (s@(Spine x yl), s') -> vtrace 4 "-ss-" $ do
     bind <- getElm ("all: "++show cons) x
     case bind of
@@ -170,9 +175,9 @@
               bind' <- getElm ("gvar-blah: "++show cons) x' 
               case bind' of
                 Right ty' -> vtraceShow 1 2 "-gc-" cons $ -- gvar-const
-                  --if allElementsAreVariables yl
-                  --then gvar_const (Spine x yl, ty) (Spine x' y'l, ty')  
-                  -- else return Nothing
+--                  if allElementsAreVariables yl
+--                  then gvar_const (Spine x yl, ty) (Spine x' y'l, ty')  
+--                   else return Nothing
                   gvar_const (Spine x yl, ty) (Spine x' y'l, ty') 
                 Left Binding{ elmQuant = Forall } | not $ S.member x' $ freeVariables yl -> 
                   throwTrace 0 $ "CANT: gvar-uvar-depends: "++show (a :=: b)
@@ -210,7 +215,7 @@
               match _ _ = throwTrace 0 $ "CANT: different numbers of arguments on constant: "++show cons
 
           cons <- match yl yl'
-          return $ Just (mempty, cons)
+          return $ Just (mempty, cons, False)
         _ -> throwTrace 0 $ "CANT: uvar against a pi WITH CONS "++show cons
             
 allElementsAreVariables :: [Spine] -> Bool
@@ -236,12 +241,12 @@
       ty' = foldr (\(nm,ty) a -> forall nm ty a) ty hl
         
       addSub Nothing = return Nothing
-      addSub (Just (sub',cons)) = do
+      addSub (Just (sub',cons,b)) = do
         -- we need to solve subst twice because we might reify twice
         let sub'' = ((subst sub' <$> sub) *** sub') 
 
         modifyCtxt $ subst sub'
-        return $ Just (sub'', cons)
+        return $ Just (sub'', cons,b)
         
   modifyCtxt $ addToHead "-rtt-" Exists x' ty' . removeFromContext x
   vtrace 3 ("RAISING: "++x' ++" +@+ "++ show newx_args ++ " ::: "++show ty'
@@ -278,7 +283,7 @@
       
   modifyCtxt $ addToHead "-ggs-" Exists xN xNty -- THIS IS DIFFERENT FROM THE PAPER!!!!
   
-  return $ Just (sub, []) -- var xN :@: xNty])
+  return $ Just (sub, [], False) -- var xN :@: xNty])
   
 gvar_gvar_same _ _ = error "gvar-gvar-same is not made for this case"
 
@@ -313,7 +318,8 @@
 
   modifyCtxt $ addToHead "-ggd-" Exists xN xNty -- THIS IS DIFFERENT FROM THE PAPER!!!!
   
-  vtrace 3 ("SUBST: -ggd- "++show sub) $ return $ Just (sub, []) -- var xN :@: xNty])
+  vtrace 3 ("SUBST: -ggd- "++show sub) $ 
+    return $ Just (sub, [] {- var xN :@: xNty] -}, False)
   
 gvar_uvar_inside a@(Spine _ yl, _) b@(Spine y _, _) = 
   case elemIndex (var y) $ reverse yl of
@@ -325,7 +331,7 @@
   case elemIndex (var y) $ yl of 
     Nothing -> gvar_fixed a b $ var . const y
     Just _ -> do
-     gvar_uvar_outside a b <|> gvar_fixed a b (var . const y) 
+      gvar_uvar_outside a b <|> gvar_fixed a b (var . const y)
 
 gvar_const _ _ = error "gvar-const is not made for this case"
 
@@ -388,8 +394,11 @@
       addExists s t = vtrace 3 ("adding: "++show s++" ::: "++show t) $ addToHead "-gf-" Exists s t
   modifyCtxt $ flip (foldr ($)) $ uncurry addExists <$> substBty mempty bty xm  
   modifyCtxt $ subst sub
-  
-  return $ Just (sub, [subst sub $ a :=: b])
+  vtrace 4 ("RES: -gg- "++(show $ subst sub $ a :=: b)) $ 
+    vtrace 4 ("FROM: -gg- "++(show $ a :=: b)) $ 
+    return $ Just (sub, [ subst sub $ a :=: b -- this ensures that the function resolves to the intended output
+                          
+                     ], False)
 
 gvar_fixed _ _ _ = error "gvar-fixed is not made for this case"
 
@@ -439,7 +448,8 @@
           where srch r1 r2 = r1 $ F.asum $ r2 . Just . return . (m :=:) <$> [atom , tipe] -- for breadth first
                 breadth = srch (ret =<<) return
                 depth = srch id (appendErr "" . ret)
-          
+    Spine nm [] | nm == tipeName -> 
+      ret $ Just [m :=: atom]
     Spine nm _ -> do
       constants <- getConstants
       foralls <- getForalls
@@ -464,6 +474,7 @@
       targets <- case mfam of
         Just (nm,t) -> return $ [(nm,t)]
         Nothing -> do
+          {-
           let excludes = S.toList $ S.intersection (M.keysSet exists) $ freeVariables m
           searchMaps <- mapM getVariablesBeforeExists excludes
           
@@ -471,9 +482,12 @@
               searchMap = M.union env $ case searchMaps of
                 [] -> mempty
                 a:l -> foldr (M.intersection) a l
-                
+              
           return $ filter sameFamily $ M.toList searchMap
-      
+          -}
+          
+          return $ filter sameFamily $ M.toList constants ++ M.toList foralls
+          
       if all isFixed $ S.toList $ S.union (freeVariables m) (freeVariables goal)
         then ret $ Just []
         else case targets of
@@ -530,7 +544,7 @@
   k <- getNewWith "@k"
   addToEnv (∃) k kind $ do
     r <- m $ var k
-    var k .@. kind
+    var k .@. kind    
     return r
 
 check v x = if x == "13@regm+f" then trace ("FOUND AT: "++ v) x else x
@@ -540,6 +554,7 @@
 checkType sp ty = case sp of
   Spine "#hole#" [] -> do
     x' <- getNewWith "@hole"
+    
     addToEnv (∃) x' ty $ do
       var x' .@. ty
       return $ var x'
@@ -701,7 +716,7 @@
       else return prev''
            
 getGenTys sp = S.filter isGen $ freeVariables sp
-  where isGen (c:s) = isUpper c
+  where isGen (c:s) = elem c ['A'..'Z']
         
 generateBinding sp = foldr (\a b -> imp_forall a ty_hole b) sp orderedgens
   where genset = getGenTys sp
@@ -714,13 +729,14 @@
 ----------------------
 typeInfer :: ContextMap -> ((Bool,Integer),Name,Spine,Type) -> Choice (Term,Type, ContextMap)
 typeInfer env (seqi,nm,val,ty) = (\r -> (\(a,_,_) -> a) <$> runRWST r (M.union envConsts env) emptyState) $ do
-  ty <- return $ alphaConvert mempty ty
-  val <- return $ alphaConvert mempty val
+  ty <- return $ alphaConvert mempty mempty ty
+  val <- return $ alphaConvert mempty mempty val
   
   (ty,mem') <- regenWithMem ty
-  (val,mem) <- regenWithMem val
+  (val,mem) <- vtrace 1 ("ALPHAD TO: "++show val) $ regenWithMem val
   
-  (val,constraint) <- checkFullType val ty
+  (val,constraint) <- vtrace 1 ("REGENED TO: "++show val) $ 
+                      checkFullType val ty
   
   sub <- appendErr ("which became: "++show val ++ "\n\t :  " ++ show ty) $ 
          unify constraint
@@ -740,26 +756,34 @@
 --- the public interface ---
 ----------------------------
 
-type FlatPred = [(Maybe Name,(Bool,Integer,Bool),Name,Term,Type)]
-typeCheckAxioms :: Bool -> FlatPred -> Choice Substitution
+-- type FlatPred = [((Maybe Name,Bool,Integer,Bool),Name,Type,Kind)]
+
+typeCheckAxioms :: Bool -> [FlatPred] -> Choice Substitution
 typeCheckAxioms verbose lst = do
   
   -- check the closedness of families.  this gets done
   -- after typechecking since family checking needs to evaluate a little bit
   -- in order to allow defs in patterns
-  let notval (_,_,'#':'v':':':_,_,_) = False
-      notval (_,_,_,_,_) = True 
+  let notval p = case p ^. predName of 
+        '#':'v':':':_ -> False
+        _ -> True
       
-      unsound (_,(_,_,s),_,_,_) = not s
+      unsound = not . (^. predSound)
       
-      tys = M.fromList $ map (\(_,(b,i,_),nm,ty,_) -> (nm,((b,i),ty))) $ filter notval lst
-      uns = S.fromList $ map (\(_,_,nm,ty,_) -> nm) $ filter unsound $ filter notval lst
+      tys = M.fromList $ map (\p -> ( p^.predName, ((p^.predSequential,p^.predPriority),p^.predType))) $ filter notval lst
+      uns = S.fromList $ map (^.predName) $ filter unsound $ filter notval lst
       
-      inferAll :: (ContextMap, FlatPred, FlatPred) -> Choice (FlatPred,ContextMap)
+      inferAll :: (ContextMap, [FlatPred], [FlatPred]) -> Choice ([FlatPred],ContextMap)
       inferAll (l , r, []) = return (r,l)
-      inferAll (_ , r, (_,_,nm,_,_):_) | nm == tipeName = throwTrace 0 $ tipeName++" can not be overloaded"
-      inferAll (_ , r, (_,_,nm,_,_):_) | nm == atomName = throwTrace 0 $ atomName++" can not be overloaded"
-      inferAll (l , r, (fam,(b,i,s),nm,val,ty):toplst) = do
+      inferAll (_ , r, p:_) | p^.predName == tipeName = throwTrace 0 $ tipeName++" can not be overloaded"
+      inferAll (_ , r, p:_) | p^.predName == atomName = throwTrace 0 $ atomName++" can not be overloaded"
+      inferAll (l , r, p:toplst) = do
+        let fam = p^.predFamily
+            b = p^.predSequential
+            i = p^.predPriority
+            nm = p^.predName
+            val = p^.predType
+            ty = p^.predKind
         (val,ty,l') <- appendErr ("can not infer type for: "++nm++" : "++show val) $ 
                        mtrace verbose ("Checking: " ++nm) $ 
                        vtrace 0 ("\tVAL: " ++show val  
@@ -770,20 +794,22 @@
         unless (fam == Nothing || Just (getFamily val) == fam)
           $ throwTrace 0 $ "not the right family: need "++show fam++" for "++nm ++ " = " ++show val                    
           
+        let resp = p & predType .~ val & predKind .~ ty
         inferAll $ case nm of
-          '#':'v':':':nm' -> (sub' <$> l', (fam,(b,i,s),nm,val,ty):r , fsub <$> toplst) 
+          '#':'v':':':nm' -> (sub' <$> l', resp:r , sub <$> toplst) 
             where sub' (b,a)= (b, sub a)
+                  sub :: Subst a => a -> a
                   sub = subst $ nm' |-> ascribe val (dontcheck ty) 
-                        -- the ascription isn't necessary because we don't have unbound variables, 
-                        -- and we already know that val : ty, but it pauses computation
-                        -- ascribe val ty 
-                  fsub (fam,s,nm,val,ty) = (fam,s,nm, sub val, sub ty)
-          _ -> (l', (fam,(b,i,s),nm,val,ty):r, toplst)
+          _ -> (l', resp:r, toplst)
 
   (lst',l) <- inferAll (tys, [], topoSortAxioms lst)
   
   let doubleCheckAll _ [] = return ()
-      doubleCheckAll l ((_,_,nm,val,ty):r) = do
+      doubleCheckAll l (p:r) = do
+        let nm = p^.predName
+            val = p^.predType
+            ty = p^.predKind
+        
         let usedvars = freeVariables val `S.union` freeVariables ty
         unless (S.isSubsetOf usedvars l)
           $ throwTrace 0 $ "Circular type:"
@@ -799,15 +825,16 @@
   return $ snd <$> l 
 
 
-topoSortAxioms :: [(Maybe Name, (Bool,Integer,Bool), Name,Term,Type)] -> [(Maybe Name, (Bool,Integer,Bool), Name,Term,Type)]
-topoSortAxioms axioms = topoSortComp (\(fam,s,nm,val,ty) -> (nm,) 
-                                                            $ S.union (getImplieds nm)
-                                                            $ S.fromList 
-                                                            $ concatMap (\nm -> [nm,"#v:"++nm])
-                                                            $ filter (not . flip elem (map fst consts)) 
-                                                            $ S.toList $ freeVariables val `S.union` freeVariables ty ) axioms
+topoSortAxioms :: [FlatPred] -> [FlatPred]
+topoSortAxioms axioms = topoSortComp (\p -> (p^.predName,) 
+                                            -- unsound can mean this causes extra cyclical things to occur
+                                            $ (if p^.predSound then S.union (getImplieds $ p^.predName) else id)
+                                            $ S.fromList 
+                                            $ concatMap (\nm -> [nm,"#v:"++nm])
+                                            $ filter (not . flip elem (map fst consts)) 
+                                            $ S.toList $ freeVariables p ) axioms
                         
-  where nm2familyLst  = catMaybes $ (\(fam,_,nm,_,_) -> (nm,) <$> fam) <$> axioms
+  where nm2familyLst  = catMaybes $ (\p -> (p^.predName,) <$> (p^.predFamily)) <$> axioms
 
         
         family2nmsMap = foldr (\(fam,nm) m -> M.insert nm (case M.lookup nm m of
@@ -815,17 +842,18 @@
                                   Just s -> S.insert fam s) m
                                 )  mempty nm2familyLst
         
-        family2impliedsMap = M.fromList $ (\(_,_,nm,val,_) -> (nm, 
-                                                               mconcat 
-                                                               $ catMaybes 
-                                                               $ map (`M.lookup` family2nmsMap) 
-                                                               $ S.toList 
-                                                               $ getImpliedFamilies val 
-                                                              )) <$> axioms        
+        family2impliedsMap = M.fromList $ (\p -> (p^.predName, 
+                                                  mconcat 
+                                                  $ catMaybes 
+                                                  $ map (`M.lookup` family2nmsMap) 
+                                                  $ S.toList 
+                                                  $ getImpliedFamilies 
+                                                  $ p^.predType
+                                                 )) <$> axioms        
         
         getImplieds nm = fromMaybe mempty (M.lookup nm family2impliedsMap)
 
-typeCheckAll :: Bool -> [Predicate] -> Choice [Predicate]
+typeCheckAll :: Bool -> [Decl] -> Choice [Decl]
 typeCheckAll verbose preds = do
   
   tyMap <- typeCheckAxioms verbose $ toAxioms True preds
@@ -836,20 +864,23 @@
   
   return $ newPreds <$> preds
 
-toAxioms :: Bool -> [Predicate] -> [(Maybe [Char], (Bool, Integer, Bool), Name, Type, Spine)]  
+toAxioms :: Bool -> [Decl] -> [FlatPred]
 toAxioms b = concat . zipWith toAxioms' [0..]
-  where toAxioms' j (Predicate s nm ty cs) = (Just $ atomName,(False,j,s),nm,ty,tipe):zipWith (\(sequ,(nm',ty')) i -> (Just nm,(sequ,i,False), nm',ty',atom)) cs [0..]
-        toAxioms' j (Query nm val) = [(Nothing, (False,j,False),nm,val,atom)]
-        toAxioms' j (Define s nm val ty) = (if b then ((Nothing,(False,j,s), "#v:"++nm,val,ty):) else id)
-                                           [(Nothing,(False,j,False), nm,ty,kind)] 
+  where toAxioms' j (Predicate s nm ty cs) = 
+          (FlatPred (PredData (Just $ atomName) False j s) nm ty tipe)
+          :zipWith (\(sequ,(nm',ty')) i -> (FlatPred (PredData (Just nm) sequ i False) nm' ty' atom)) cs [0..]
+        toAxioms' j (Query nm val) = [(FlatPred (PredData Nothing False j False) nm val atom)]
+        toAxioms' j (Define s nm val ty) = (if b then ((FlatPred (PredData Nothing False j s) ("#v:"++nm) val ty):) else id)
+                                           [(FlatPred (PredData Nothing False j False) nm ty kind)] 
   
-toSimpleAxioms :: [Predicate] -> ContextMap
-toSimpleAxioms l = M.fromList $ (\(_,(seqi,i,_),nm,t,_) -> (nm,((seqi,i),t))) <$> toAxioms False l
+toSimpleAxioms :: [Decl] -> ContextMap
+toSimpleAxioms l = M.fromList $ (\p -> (p^.predName, ((p^.predSequential, p^.predPriority), p^.predType))) 
+                   <$> toAxioms False l
 
 solver :: ContextMap -> Type -> Either String [(Name, Term)]
 solver axioms tp = case runError $ runRWST (search tp) (M.union envConsts axioms) emptyState of
   Right ((_,tm),_,_) -> Right $ [("query", tm)]
   Left s -> Left $ "reification not possible: "++s
 
-reduceDecsByName :: [Predicate] -> [Predicate]
-reduceDecsByName decs = map snd $ M.toList $ M.fromList $ map (\a -> (predName a,a)) decs
+reduceDecsByName :: [Decl] -> [Decl]
+reduceDecsByName decs = map snd $ M.toList $ M.fromList $ map (\a -> (a ^. declName,a)) decs
diff --git a/Main.hs b/Main.hs
--- a/Main.hs
+++ b/Main.hs
@@ -1,18 +1,22 @@
+
 module Main where
 
+import Options
 import AST
+import Substitution
+
 import Choice
 import HOU
 import Parser
 import System.Environment
-import Data.Functor
 import Data.Foldable as F (forM_)
 import Data.List (partition)
-import Text.Parsec
 import Data.Monoid
 import Control.Monad (when)
-import Control.Arrow (first)
 
+import Data.IORef
+
+import Control.Lens ((^.), (.~), (&))
 import Language.Preprocessor.Cpphs
 
 -----------------------------------------------------------------------
@@ -33,7 +37,7 @@
         Define {} -> True
         _ -> False
       
-      sub = subst $ foldr (\a r -> r *** (predName a |-> subst r (predValue a))) mempty defs
+      sub = subst $ foldr (\a r -> r *** ((a^.declName) |-> subst r (a^.declValue))) mempty defs
       (predicates, targets) = flip partition others $ \x -> case x of
         Predicate {} -> True
         _ -> False
@@ -53,14 +57,18 @@
   
   forM_ targets' $ \target -> do
     when verbose $ putStrLn $ "\nTARGET: \n"++show target
-    case solver axioms $ predType target of
+    case solver axioms $ target ^. declType of
       Left e -> putStrLn $ "ERROR: "++e
       Right sub -> when verbose $ putStrLn $ "SOLVED WITH:\n"
                    ++concatMap (\(a,b) -> a++" => "++show b++"\n") sub
 
 
-processFile :: Bool -> String -> IO ()
-processFile verbose fname = do
+processFile :: Options -> IO ()
+processFile options = do
+  let fname = options ^. optFile
+      
+  writeIORef levelVar $ options ^. optVerbose
+  
   file <- readFile fname
   
   file <- runCpphs 
@@ -78,12 +86,12 @@
   decs <- case mError of
     Left e -> error $ show e
     Right l -> return l
-  checkAndRun verbose $ reduceDecsByName decs
-
+  checkAndRun (not $ options ^. optIO_Only) $ reduceDecsByName decs
+          
 main = do
-  fnames <- getArgs
-  case fnames of
-    [] -> putStrLn "No file specified. Usage is \"caledon [--io-only] file.ncc\""
-    [fname] -> processFile True fname
-    ["--io-only", fname] -> processFile False fname
-    _ -> putStrLn "Unrecognized arguments. Usage is \"caledon [--io-only] file.ncc\""
+  (options, files) <- compilerOpts =<< getArgs
+  
+  processFile $ options & case files of
+    [] -> id
+    [fname] -> optFile .~ fname
+    _ -> error $ "Too many file arguments."++header
diff --git a/Options.hs b/Options.hs
new file mode 100644
--- /dev/null
+++ b/Options.hs
@@ -0,0 +1,52 @@
+{-# LANGUAGE 
+ TemplateHaskell,
+ FlexibleContexts
+ #-}
+module Options where
+
+import Data.Maybe
+import Control.Lens (makeLenses, (.~))
+import System.Console.GetOpt
+
+data Options = Options 
+               { _optIO_Only :: Bool
+               , _optVerbose :: Int
+               , _optFile :: String
+               } 
+$(makeLenses ''Options)     
+
+defaultOptions = Options 
+               { _optIO_Only  = False
+               , _optVerbose  = 0
+               , _optFile     = ""
+               }
+
+
+options :: [OptDescr (Options -> Options)]
+options = 
+  [ Option ['i'] ["io-only"]
+    (NoArg $ optIO_Only .~ True)
+    "don't print out typechecking info"
+  , Option ['v'] ["verbosity"]
+    (OptArg ((optVerbose .~) . fromMaybe 0 . fmap read) "VERBOSITY")
+    "a number describing how much debugging information to print"
+  , Option ['f'] ["file", "infile", "input"]
+    (ReqArg (optFile .~) "INFILE")
+    "the file to interpret and typecheck"
+  ]
+
+helpMessage = "Usage is \"caledon [--io-only] file.ncc\""
+
+arg_lst = [ ["--io-only", "-i"]
+          , ["--verbosity", "-V"]
+          , ["--help", "-h"]
+          , ["--file", "-f"]
+          ]
+  
+compilerOpts :: [String] -> IO (Options,[String])
+compilerOpts argv = 
+  case getOpt Permute options argv of
+    (o,n,[] ) -> return (foldl (flip id) defaultOptions o, n)
+    (_,_,errs) -> ioError $ userError $ concat errs ++ usageInfo header options
+
+header = "Usage: caledon [OPTIONS] file.ncc"
diff --git a/Parser.hs b/Parser.hs
--- a/Parser.hs
+++ b/Parser.hs
@@ -1,15 +1,23 @@
 {-# LANGUAGE
- RecordWildCards
+ RecordWildCards,
+ TemplateHaskell,
+ FlexibleContexts,
+ IncoherentInstances,
+ TypeSynonymInstances,
+ FlexibleInstances,
+ MultiParamTypeClasses
  #-}
 
 module Parser (parseCaledon) where
 
 import AST
-
+import Substitution
+import Control.Applicative (Applicative(..))
 import Data.Functor
 import Data.Functor.Identity
 import Text.Parsec
 import Control.Monad (unless)
+import Control.Monad.State.Class
 import Text.Parsec.Language (haskellDef)
 import Text.Parsec.Expr 
 import Data.List
@@ -20,98 +28,102 @@
 import Debug.Trace
 import qualified Data.Foldable as F
 
-
+import Control.Lens 
 
 -----------------------------------------------------------------------
 -------------------------- PARSER -------------------------------------
 -----------------------------------------------------------------------
 
--- | `parseCaledon` is the external interface
-parseCaledon :: SourceName -> String -> Either ParseError [Predicate]
-parseCaledon = runP decls emptyState
+data Fixity = FixLeft | FixRight | FixNone
 
-data ParseState = ParseState { currentVar :: Integer
-                             , currentSet :: S.Set Name
-                             , currentTable :: FixityTable 
-                             , currentOps :: [Name]
+data FixityTable = FixityTable { _fixityBinary :: [(Integer,String, Assoc)] 
+                               , _fixityPrefix :: [(Integer, String, Assoc)]
+                               , _fixityPostfix :: [(Integer, String, Assoc)]
+                               , _opLambdas :: [String]
+                               , _strLambdas :: [String]
+                               , _binds :: [(String,String,String)]
+                               }
+                   
+                   
+data ParseState = ParseState { _currentVar :: Integer
+                             , _currentSet :: S.Set Name
+                             , _currentTable :: FixityTable 
+                             , _currentOps :: [Name]
                              }
+$(makeLenses ''FixityTable)                  
+$(makeLenses ''ParseState)
 
-data Fixity = FixLeft | FixRight | FixNone
 
-data FixityTable = FixityTable { fixityBinary :: [(Integer,String, Assoc)] 
-                               , fixityPrefix :: [(Integer, String, Assoc)]
-                               , fixityPostfix :: [(Integer, String, Assoc)]
-                               , opLambdas :: [String]
-                               , strLambdas :: [String]
-                               , binds :: [(String,String,String)]
-                               }
 
+-- | `parseCaledon` is the external interface
+parseCaledon :: SourceName -> String -> Either ParseError [Decl]
+parseCaledon = runP decls emptyState
+
+
 emptyTable = FixityTable [] [] [] [] [] []
 emptyState = (ParseState 0 mempty emptyTable [])
 
 type Parser = ParsecT String ParseState Identity
 
-modifySet :: (S.Set Name -> S.Set Name) -> ParseState -> ParseState
-modifySet f s = s { currentSet = f $ currentSet s }
+instance MonadState ParseState Parser where
+  get = getState
+  put = putState
 
-modifyVar :: (Integer -> Integer) -> ParseState -> ParseState
-modifyVar f s = s { currentVar = f $ currentVar s }
 
 getNextVar :: Parser String
 getNextVar = do
-  v <- currentVar <$> getState
-  modifyState $ modifyVar (+1)
+  v <- use currentVar
+  currentVar %= (+1)
   return $ show v++"'"
 
-decls :: Parser [Predicate]
+decls :: Parser [Decl]
 decls = do
   whiteSpace
   lst <- many (topLevel <?> "declaration")
   eof
-  return lst
-
-topLevel = fixityDef <|> query <|> defn
+  return $ catMaybes lst
 
-fixityDef = do 
+topLevel = Nothing <$ fixityDef 
+       <|> Just <$> query 
+       <|> Just <$> defn 
+       <* optional (many semi)
+  
+fixityDef = do
   reserved "fixity"
   infixDef <|> lamDef
-  topLevel
                                                                     
 lamDef = do
   reserved "lambda"
   opLam <|> strLam
 
-opLam = do  
-  op <- operator
-  modifyState $ \b -> b { currentTable = let ct = currentTable b in ct { opLambdas = op:opLambdas ct} }
-                                                                    
-strLam = do
-  op <- identifier
-  modifyState $ \b -> b { currentTable = let ct = currentTable b in ct { strLambdas = op:strLambdas ct} }
-                                                                    
+opLam = addOpLam operator opLambdas
+strLam = addOpLam identifier strLambdas
+
+addOpLam ident lens = do
+  op <- ident
+  currentTable.lens %= (op:)
+  
 infixDef = do  
-  -- I wish template haskell worked with record wild cards!
-  (setFixity) <- (reserved "left" >> return (\b c -> b { fixityBinary = c AssocLeft $ fixityBinary b} )) 
-             <|> (reserved "none" >> return (\b c -> b { fixityBinary = c AssocNone $ fixityBinary b} )) 
-             <|> (reserved "right" >> return (\b c -> b { fixityBinary = c AssocRight $ fixityBinary b} )) 
-             <|> (reserved "pre" >> return (\b c -> b { fixityPrefix = c undefined $ fixityPrefix b}))
-             <|> (reserved "post" >> return (\b c -> b { fixityPostfix = c undefined $ fixityPostfix b}))
+  setFixity <- (reserved "left" >> return (\b c -> over fixityBinary (c AssocLeft) b))
+           <|> (reserved "none" >> return (\b c -> over fixityBinary (c AssocNone) b))
+           <|> (reserved "right" >> return (\b c -> over fixityBinary (c AssocRight) b))
+           <|> (reserved "pre" >> return (\b c -> over fixityPrefix (c undefined) b))
+           <|> (reserved "post" >> return (\b c -> over fixityPostfix (c undefined) b))
   n <- integer
-  op <- operator -- <|> identifier
+  op <- operator
   
   let modify assoc = insertBy (\(n,_,_) (m,_,_) -> compare n m) (n,op, assoc)
-  modifyState $ \b -> b { currentTable = setFixity (currentTable b) modify
-                        , currentOps = op:currentOps b}
   
+  currentTable %= flip setFixity modify
+  currentOps %= (op:)
+  
 
-query :: Parser Predicate
+query :: Parser Decl
 query = do
-  reserved "query"
-  (nm,ty) <- named decPred
-  optional semi
-  return $ Query nm ty
+  reserved "query" 
+  uncurry Query <$> named decPred
 
-defn :: Parser Predicate
+defn :: Parser Decl
 defn = sound <|> unsound
   
 sound = do
@@ -131,11 +143,8 @@
                       <|> (reservedOp ">|" >> return True)
                    (nm,t) <- named decPred
                    return (seqi,(nm,t))
-                        
-                 optional semi
                  return $ Predicate s nm ty lst
-      none = do optional semi
-                return $ Predicate s nm ty []
+      none = do return $ Predicate s nm ty []
       letbe = do reserved "as"
                  val <- pTipe
                  return $ Define s nm val ty
@@ -168,11 +177,11 @@
 
 tmpState :: String -> Parser a -> Parser a
 tmpState nm m = do
-  s <- currentSet <$> getState
+  s <- use currentSet
   let b = S.member nm s
-  modifyState $ modifySet (S.insert nm)
+  currentSet %= S.insert nm
   r <- m
-  unless b $ modifyState $ modifySet $ S.delete nm
+  unless b $ currentSet %= S.delete nm
   return r
 
 
@@ -183,7 +192,7 @@
 
 
 pTipe = do
-  FixityTable bin prefix postfix opLams strLams binds <- currentTable <$> getState 
+  FixityTable bin prefix postfix opLams strLams binds <- use currentTable
   
   let getSnd [] = []
       getSnd (a:l) = l
@@ -218,13 +227,14 @@
                    (parens anonNamed <|> anonNamed)
         return $ \input -> foldr (flip out tp) input nml
       
+      
       table = [ [ altPostfix ["λ", "\\"] ["lambda"] Abs
                 , altPostfix ["?λ", "?\\"] ["?lambda"] imp_abs
                 , altPostfix ["∃"] ["exists"] exists
                 , regPostfix angles ["??"] ["infer"] infer
                 , regPostfix brackets ["∀"] ["forall"] forall
                 , regPostfix braces ["?∀"] ["?forall"] imp_forall
-                ]++[ altPostfix [op] [] (\nm t s -> Spine op [t,Abs nm ty_hole s] ) | op <- opLams ]
+                ]++[ altPostfix [op] [] (\nm t s -> Spine op [t, Abs nm ty_hole s] ) | op <- opLams ]
                 ++[ altPostfix [] [op] (\nm t s -> Spine op [t,Abs nm ty_hole s] ) | op <- strLams ]
               , [ binary (forall) AssocRight $ reservedOp "->" <|> reservedOp "→" 
                 , binary (const (~~>)) AssocRight $ reservedOp "=>" <|> reservedOp "⇒"
@@ -276,7 +286,7 @@
               return $ ascribe v t
         (asc <|> return v <?> "function") 
         
-      pOp = do operators <- currentOps <$> getState 
+      pOp = do operators <- use currentOps
                choice $ flip map operators $ \nm -> do reserved nm 
                                                        return $ var nm
          <?> "operator"      
@@ -291,11 +301,9 @@
          <|> pString
          <?> "atom"
 
-      pTycon = braces $ do
-        (nm,ty) <- named decVar
-        return $ tycon nm ty
+      pTycon = braces $ uncurry tycon <$> named decVar
       
-      myParens s m = between (symbol "(" <?> ("("++s)) (symbol ")" <?> (s++")")) m
+      myParens s m = (symbol "(" <?> ("("++s)) *> m <*  (symbol ")" <?> (s++")"))
       
   ptipe <?> "tipe"
 
@@ -326,3 +334,5 @@
 
 getId :: Parser Char -> Parser String
 getId start = P.identifier $ P.makeTokenParser mydef { P.identStart = start }
+
+
diff --git a/Substitution.hs b/Substitution.hs
new file mode 100644
--- /dev/null
+++ b/Substitution.hs
@@ -0,0 +1,291 @@
+{-# LANGUAGE
+ FlexibleInstances,
+ PatternGuards,
+ BangPatterns,
+ FlexibleContexts,
+ TupleSections
+ #-}
+
+module Substitution where
+
+import AST
+
+import qualified Data.Foldable as F
+import Data.List
+import Data.Maybe
+import Data.Monoid
+import Data.Functor
+import qualified Data.Map as M
+import Data.Map (Map)
+import qualified Data.Set as S
+import Control.Monad.RWS (RWST)
+import Control.Monad.State.Class (MonadState(), get, modify)
+
+import Control.Lens hiding (Choice(..))
+---------------------
+--- New Variables ---
+---------------------
+
+class ValueTracker c where
+  putValue :: Integer -> c -> c
+  takeValue :: c -> Integer
+
+instance ValueTracker Integer where
+  putValue _ i = i
+  takeValue i = i
+
+getNew :: (Functor m, MonadState c m, ValueTracker c) => m String
+getNew = do
+  st <- takeValue <$> get
+  let n = 1 + st
+  modify $ putValue n
+  return $ show n
+  
+getNewWith :: (Functor f, MonadState c f, ValueTracker c) => String -> f String
+getNewWith s = {- (++s) <$> -} getNew
+
+                               
+---------------------
+---  substitution ---
+---------------------
+
+type Substitution = M.Map Name Spine
+
+infixr 1 |->
+infixr 0 ***
+m1 *** m2 = M.union m2 $ subst m2 <$> m1
+(|->) = M.singleton
+(!) = flip M.lookup
+
+
+findTyconInPrefix nm = fip []
+  where fip l (Spine "#tycon#" [Spine nm' [v]]:r) | nm == nm' = Just (v, reverse l++r)
+        fip l (a@(Spine "#tycon#" [Spine _ [_]]):r) = fip (a:l) r
+        fip _ _ = Nothing
+
+apply :: Spine -> Spine -> Spine
+apply !a !l = rebuildSpine a [l]
+
+rebuildSpine :: Spine -> [Spine] -> Spine
+rebuildSpine s [] = s
+rebuildSpine (Spine "#imp_abs#" [_, Abs nm ty rst]) apps = case findTyconInPrefix nm apps of 
+  Just (v, apps) -> rebuildSpine (Abs nm ty rst) (v:apps)
+  Nothing -> seq sp $ if ty == atom && S.notMember nm (freeVariables rs) then rs else irs 
+                      -- proof irrelevance hack
+                      -- we know we can prove that type "prop" is inhabited
+                      -- irs - the proof doesn't matter
+                      -- rs - the proof matters
+                      -- irs - here, the proof might matter, but we don't know if we can prove the thing, 
+                      -- so we need to try
+     where nm' = newNameFor nm $ freeVariables apps
+           sp = subst (nm |-> var nm') rst
+           rs = rebuildSpine sp apps
+           irs = infer nm ty rs
+rebuildSpine (Spine c apps) apps' = Spine c $ apps ++ apps'
+rebuildSpine (Abs nm _ rst) (a:apps') = let sp = subst (nm |-> a) $ rst
+                                        in seq sp $ rebuildSpine sp apps'
+
+newNameFor :: Name -> S.Set Name -> Name
+newNameFor nm fv = nm'
+  where nm' = fromJust $ find free $ nm:map (\s -> show s ++ "/?") [0..]
+        free k = not $ S.member k fv
+        
+newName :: Name -> Map Name Spine -> S.Set Name -> (Name, Map Name Spine, S.Set Name)
+newName "" so fo = ("",so,fo)
+newName nm so fo = (nm',s',f')
+  where s = M.delete nm so  
+        -- could reduce the size of the free variable set here, but for efficiency it is not really necessary
+        -- for beautification of output it is
+        (s',f') = if nm == nm' then (s,fo) else (M.insert nm (var nm') s , S.insert nm' fo)
+        nm' = fromJust $ find free $ nm:map (\s -> show s ++ "/") [0..]
+        fv = mappend (M.keysSet s) (freeVariables s)
+        free k = not $ S.member k fv
+
+class Subst a where
+  substFree :: Substitution -> S.Set Name -> a -> a
+  
+
+getImpliedFamilies s = S.intersection fs $ gif s
+  where fs = freeVariables s
+        gif (Spine "#imp_forall#" [ty,a]) = (case getFamilyM ty of
+          Nothing -> id
+          Just f -> S.insert f) $ gif ty `S.union` gif a 
+        gif (Spine a l) = mconcat $ gif <$> l
+        gif (Abs _ ty l) = S.union (gif ty) (gif l)
+
+subst :: Subst a => Substitution -> a -> a
+subst s = substFree s $ freeVariables s
+
+class Alpha a where  
+  alphaConvert :: S.Set Name -> Map Name Name -> a -> a
+  rebuildFromMem :: Map Name Name -> a -> a  
+  
+instance Subst a => Subst [a] where
+  substFree s f t = substFree s f <$> t
+  
+instance Alpha a => Alpha [a] where  
+  alphaConvert s m l = alphaConvert s m <$> l
+  rebuildFromMem s l = rebuildFromMem s <$> l
+  
+instance (Subst a, Subst b) => Subst (a,b) where
+  substFree s f ~(a,b) = (substFree s f a , substFree s f b)
+  
+instance Subst Spine where
+  substFree s f sp@(Spine "#imp_forall#" [_, Abs nm tp rst]) = case "" /= nm && S.member nm f && not (S.null $ S.intersection (M.keysSet s) $ freeVariables sp) of
+    False -> imp_forall nm (substFree s f tp) $ substFree (M.delete nm s) f rst
+    True -> error $ 
+            "can not capture free variables because implicits quantifiers can not alpha convert: "++ show sp 
+            ++ "\n\tfor: "++show s
+  substFree s f sp@(Spine "#imp_abs#" [_, Abs nm tp rst]) = case "" /= nm && S.member nm f && not (S.null $ S.intersection (M.keysSet s) $ freeVariables sp) of
+    False  -> imp_abs nm (substFree s f tp) $ substFree (M.delete nm s) f rst 
+    True   -> error $ 
+              "can not capture free variables because implicit binds can not alpha convert: "++ show sp
+              ++ "\n\tfor: "++show s
+  substFree s f (Abs nm tp rst) = Abs nm' (substFree s f tp) $ substFree s' f' rst
+    where (nm',s',f') = newName nm s f
+  substFree s f (Spine "#tycon#" [Spine c [v]]) = Spine "#tycon#" [Spine c [substFree s f v]]
+  substFree s f (Spine nm apps) = let apps' = substFree s f <$> apps  in
+    case s ! nm of
+      Just nm -> rebuildSpine nm apps'
+      _ -> Spine nm apps'
+      
+instance Alpha Spine where
+  alphaConvert s m (Spine "#imp_forall#" [_,Abs a ty r]) = imp_forall a ty $ alphaConvert (S.insert a s) (M.delete a m) r
+  alphaConvert s m (Spine "#imp_abs#" [_,Abs a ty r]) = imp_abs a ty $ alphaConvert (S.insert a s) (M.delete a m) r
+  alphaConvert s m (Abs nm ty r) = Abs nm' (alphaConvert s m ty) $ alphaConvert (S.insert nm' s) (M.insert nm nm' m) r
+    where nm' = newNameFor nm s
+  alphaConvert s m (Spine "#tycon#" [Spine c [v]]) = tycon c $ alphaConvert s m v          
+  alphaConvert s m (Spine a l) = Spine (fromMaybe a (m ! a)) $ alphaConvert s m l
+  
+  rebuildFromMem s (Spine "#imp_forall#" [_,Abs a ty r]) = imp_forall a (rebuildFromMem s ty) $ rebuildFromMem (M.delete a s) r
+  rebuildFromMem s (Spine "#imp_abs#" [_,Abs a ty r]) = imp_abs a (rebuildFromMem s ty) $ rebuildFromMem (M.delete a s) r
+  rebuildFromMem s (Abs nm ty r) = Abs (fromMaybe nm $ M.lookup nm s) (rebuildFromMem s ty) $ rebuildFromMem s r
+  rebuildFromMem s (Spine a l) = Spine a' $ rebuildFromMem s l
+    where a' = fromMaybe a $ M.lookup a s
+                                 
+  
+instance Subst Decl where
+  substFree sub f (Predicate s nm ty cons) = Predicate s nm (substFree sub f ty) ((\(b,(nm,t)) -> (b,(nm,substFree sub f t))) <$> cons)
+  substFree sub f (Query nm ty) = Query nm (substFree sub f ty)
+  substFree sub f (Define s nm val ty) = Define s nm (substFree sub f val) (substFree sub f ty)
+
+
+instance Subst FlatPred where
+  substFree sub f p = p & predType %~ substFree sub f
+                        & predKind %~ substFree sub f
+
+  
+-------------------------
+---  Constraint types ---
+-------------------------
+
+instance Subst SCons where
+  substFree s f c = case c of
+    s1 :@: s2 -> subq s f (:@:) s1 s2
+    s1 :=: s2 -> subq s f (:=:) s1 s2
+    
+instance Subst Constraint where
+  substFree s f c = case c of
+    SCons l -> SCons $ map (substFree s f) l
+    s1 :&: s2 -> subq s f (:&:) s1 s2
+    Bind q nm t c -> Bind q nm' (substFree s f t) $ substFree s' f' c
+      where (nm',s',f') = newName nm s f
+            
+
+subq s f e c1 c2 = e (substFree s f c1) (substFree s f c2)
+
+(∃) = Bind Exists
+(∀) = Bind Forall
+  
+infixr 0 <<$>
+(<<$>) f m = ( \(a,b) -> (f a, b)) <$> m
+
+regenM e a b = do
+  (a',s1) <- regenWithMem a 
+  (b',s2) <- regenWithMem b 
+  return $ (e a' b', M.union s1 s2)
+regen e a b = do
+  a' <- regenAbsVars a 
+  b' <- regenAbsVars b 
+  return $ e a' b'  
+  
+class RegenAbsVars a where
+  regenAbsVars :: (Functor f, MonadState c f, ValueTracker c) => a -> f a
+  regenWithMem :: (Functor f, MonadState c f, ValueTracker c) => a -> f (a, Map Name Name)
+  
+instance RegenAbsVars l => RegenAbsVars [l] where
+  regenAbsVars cons = mapM regenAbsVars cons
+  
+  regenWithMem cons = together <$> mapM regenWithMem cons
+    where together f = (l',foldr M.union mempty ss)
+            where (l',ss) = unzip f
+  
+
+  
+instance RegenAbsVars Spine where  
+  regenAbsVars (Spine "#imp_forall#" [_,Abs a ty r]) = imp_forall a ty <$> regenAbsVars r
+  regenAbsVars (Spine "#imp_abs#" [_,Abs a ty r]) = imp_abs a ty <$> regenAbsVars r
+  regenAbsVars (Abs a ty r) = do
+    a' <- getNewWith $ "@rega"
+    ty' <- regenAbsVars ty
+    r' <- regenAbsVars $ subst (a |-> var a') r
+    return $ Abs a' ty' r'
+  regenAbsVars (Spine a l) = Spine a <$> regenAbsVars l
+  
+  regenWithMem (Spine "#imp_forall#" [_,Abs a ty r]) = imp_forall a ty <<$> regenWithMem r
+  regenWithMem (Spine "#imp_abs#" [_,Abs a ty r]) = imp_abs a ty <<$> regenWithMem r
+  regenWithMem (Abs a ty r) = do
+    a' <- getNewWith $ "@regm"
+    (ty',s1) <- regenWithMem ty
+    (r', s2) <- regenWithMem $ subst (a |-> var a') r
+    return $ (Abs a' ty' r', M.insert a' a $ M.union s1 s2)
+  regenWithMem (Spine a l) = Spine a <<$> regenWithMem l
+
+
+
+instance RegenAbsVars SCons where
+  regenAbsVars cons = case cons of
+    a :=: b -> regen (:=:) a b
+    a :@: b -> regen (:@:) a b
+    
+  regenWithMem cons = case cons of
+    a :=: b -> regenM (:=:) a b
+    a :@: b -> regenM (:@:) a b    
+      
+instance RegenAbsVars Constraint where  
+  regenAbsVars cons = case cons of
+    Bind q nm ty cons -> do
+      ty' <- regenAbsVars ty
+      case nm of
+        "" -> do
+          nm' <- getNewWith "@newer"
+          let sub = nm |-> var nm'
+          Bind q nm' ty' <$> regenAbsVars (subst sub cons)
+        _ -> Bind q nm ty' <$> regenAbsVars cons
+    SCons l -> SCons <$> regenAbsVars l
+    a :&: b -> regen (:&:) a b
+    
+  regenWithMem cons = case cons of
+    Bind q nm ty cons -> do
+      (ty',s1) <- regenWithMem ty
+      nm' <- getNewWith "@regm'"
+      let sub = nm |-> var nm'
+      (cons',s2) <- regenWithMem $ subst sub cons
+      return (Bind q nm' ty' cons', M.insert nm' nm $ M.union s1 s2)
+    SCons l -> SCons <<$> regenWithMem l
+    a :&: b -> regenM (:&:) a b    
+
+
+getFamily v = fromMaybe (error ("values don't have families: "++show v)) $ getFamilyM v
+
+getFamilyM (Spine "#infer#" [_, Abs _ _ lm]) = getFamilyM lm
+getFamilyM (Spine "#ascribe#"  (_:v:l)) = getFamilyM (rebuildSpine v l)
+getFamilyM (Spine "#dontcheck#"  [v]) = getFamilyM v
+getFamilyM (Spine "#forall#" [_, Abs _ _ lm]) = getFamilyM lm
+getFamilyM (Spine "#imp_forall#" [_, Abs _ _ lm]) = getFamilyM lm
+getFamilyM (Spine "#exists#" [_, Abs _ _ lm]) = getFamilyM lm
+getFamilyM (Spine "#open#" (_:_:c:_)) = getFamilyM c
+getFamilyM (Spine "open" (_:_:c:_)) = getFamilyM c
+getFamilyM (Spine "pack" [_,_,_,e]) = getFamilyM e
+getFamilyM (Spine nm' _) = Just nm'
+getFamilyM v = Nothing
diff --git a/caledon.cabal b/caledon.cabal
--- a/caledon.cabal
+++ b/caledon.cabal
@@ -1,6 +1,6 @@
 Name: caledon
 
-Version: 3.0.0.0
+Version: 3.1.0.0
 
 Description:         a dependently typed, polymorphic, higher order logic programming language based on the calculus of constructions designed for easier metaprogramming capabilities. 
 
@@ -28,21 +28,25 @@
 
 executable caledon
   main-is: Main.hs
-  other-modules: HOU, Choice, Parser, AST, TopoSortAxioms, Context
+  other-modules: HOU, Choice, Parser, 
+                 AST, TopoSortAxioms, 
+                 Context, Options, Substitution
 
   Build-depends: base >= 4.0 && < 5.0,
                  mtl >= 2.0 && < 3.0,
                  parsec >= 3.0 && < 4.0, 
                  containers >= 0.4 && < 1.0, 
                  transformers >= 0.3 && < 1.0,
-                 cpphs >= 1.0 && < 2.0
+                 cpphs >= 1.0 && < 2.0,
+                 lens >= 3.0 && < 4.0
 
   Extensions: FlexibleContexts,
               FlexibleInstances,
               MultiParamTypeClasses,
               RecordWildCards,
               BangPatterns,
-              TypeSynonymInstances
+              TypeSynonymInstances,
+              TemplateHaskell
               
   ghc-options:  -O2 -optc-O3 -funfolding-use-threshold=16 -fspec-constr-count=10 -fdo-lambda-eta-expansion
   
diff --git a/examples/#test.ncc# b/examples/#test.ncc#
new file mode 100644
--- /dev/null
+++ b/examples/#test.ncc#
@@ -0,0 +1,25 @@
+#include "../prelude/prelude.ncc"
+
+query add0 = add (succ zero) zero (succ zero)
+
+query add1 = succ zero ++ zero == succ zero
+
+query add2 = exists A : natural . add (succ zero) zero A
+
+query add3 = any $ add (succ zero) zero
+
+query findSat1 = succ zero =< succ (succ zero)
+
+query findSat2 = succ zero =< succ (succ zero) /\ zero =< succ (succ zero)
+
+query findSat0 = free A : natural . A =:= zero
+
+
+defn ismain : prop 
+  as run $ do 
+         , putStr "hey!\n"
+         , readLine (\A . do 
+   	 , putStr A
+         , putStr "\nbye!\n")
+
+query main = ismain
diff --git a/examples/coc.ncc b/examples/coc.ncc
--- a/examples/coc.ncc
+++ b/examples/coc.ncc
@@ -1,10 +1,10 @@
-fixity lambda .λ
+fixity lambda lam
 fixity lambda Π
 
 defn tm : prop
    | p = tm
    | t = tm
-   | .λ = tm → (tm → tm) → tm
+   | lam = tm → (tm → tm) → tm
    | Π = tm → (tm → tm) → tm
 
 fixity none 0 ::
@@ -12,4 +12,4 @@
    | p_t = p :: t
    | lam_pi =  [A : tm][T : tm -> tm][B : tm -> tm]
       ([x] x :: A -> T x :: B x )
-      -> (.λ x : A . T x) :: (Π x : A . B x) 
+      -> (lam x : A . T x) :: (Π x : A . B x) 
diff --git a/examples/readlinein.ncc b/examples/readlinein.ncc
--- a/examples/readlinein.ncc
+++ b/examples/readlinein.ncc
@@ -1,5 +1,15 @@
-#include <prelude.ncc>
+#include "../prelude/prelude.ncc"
 
 -- switching the direction of the output to be input with unification!
+
 defn readLineIn : string -> prop
-  as \S . readLine $ \R . do , S =:= R
+  as \S . readLine $ \R . do , R =:= S
+
+defn main : prop
+   | mainImp = [S] main 
+                   <- putStrLn "hi"
+		   <- S =:= "FOO"
+               	   <- putStrLn S
+                   <- putStrLn "ho"
+
+query main1 = main
diff --git a/examples/universe.ncc b/examples/universe.ncc
--- a/examples/universe.ncc
+++ b/examples/universe.ncc
@@ -1,11 +1,10 @@
-fixity right 0 $
-defn $ : {a b:prop} (a -> b) -> a -> b
-  as ?\At Bt :prop . \ F . \A . F A  
+#include "../prelude/combinators.ncc"
 
 fixity pre 1 ♢
 fixity lambda Π 
 fixity lambda lam 
 
+
 {-
 for the moment, circularly defined types are allowed!  this violates consistency.  
 If a dependency analysis is done, and types are checked in order, this will become safe!
@@ -19,12 +18,12 @@
 unsound tm : {S : tm ty} tm S → prop
    | ty  = tm ty
    | ♢   = tm ty -> tm ty
-   | Π   = [T : tm ty] (tm T → tm T) → tm $ ♢ T
+   | Π   = [T : tm ty] (tm T → tm T) → tm $ ♢  T
+   | raise = {T : tm ty} tm T → tm $ ♢  T
    | lam = [T : tm ty][F : tm T → tm T] tm {S = ♢ T} (Π A : T . F A)
-   | raise = {T : tm ty} tm T → tm $ ♢ T
 
-defn isTm : {S : tm ty} {A : tm S} tm A -> prop
+defn isTm : {Kind : tm ty} {Ty : tm Kind} tm Ty -> prop
    | hasValue = [S : tm ty][T : tm S][V : tm T] isTm V
 
-query whattype0 = isTm (Π A : ty . A)
+query whattype0 = isTm { Kind = ty } { Ty = ♢ ty } ( Π A : ty . A)
 query whattype1 = isTm (lam A : ty . A)
diff --git a/prelude/concatable.ncc b/prelude/concatable.ncc
--- a/prelude/concatable.ncc
+++ b/prelude/concatable.ncc
@@ -6,13 +6,13 @@
 --------------
 
 defn concatable : [M : prop] (M -> M -> M -> prop) -> prop
-   | concatableNat = concatable natural add
-   | concatableList = [A] concatable (list A) concatList
+  >| concatableNat = concatable natural add
+  >| concatableList = concatable (list A) concatList
 
 -- it correctly infers 169, and M (but it eta expands Foo when it infers it) !!
 fixity right 3 ++
 defn ++ : {M}{Foo}{cm : concatable M Foo} M -> M -> M -> prop
-  >| ppimp = [M][Foo : M -> M -> M -> prop][M1 M2 M3 : M] 
-              (++) {Foo = Foo} M1 M2 M3 
+   | ppimp = [M][Foo : M -> M -> M -> prop][M1 M2 M3 : M] 
+               (++) {Foo = Foo} M1 M2 M3 
             <- concatable M Foo 
             <- Foo M1 M2 M3 
diff --git a/prelude/io.ncc b/prelude/io.ncc
--- a/prelude/io.ncc
+++ b/prelude/io.ncc
@@ -1,4 +1,5 @@
 #include <strings.ncc>
+#include <combinators.ncc>
 
 ---------------
 -- builtins ---
@@ -31,3 +32,8 @@
    | putStr_Cons = putStr (cons V L)
                    <- putChar V
                    <- putStr L
+
+defn putStrLn : string -> prop
+  as \S . run $ do 
+              , putStr S
+              , putChar '\n'
diff --git a/prelude/list.ncc b/prelude/list.ncc
--- a/prelude/list.ncc
+++ b/prelude/list.ncc
@@ -2,8 +2,8 @@
 --- Lists ---
 -------------
 defn list : prop -> prop
-   | nil  = list A
-   | cons = A -> list A -> list A
+  >| nil  = list A
+  >| cons = A -> list A -> list A
 
 defn concatList : list A -> list A -> list A -> prop
   >| concatListNil  = concatList {A = T} nil L L
diff --git a/prelude/logic.ncc b/prelude/logic.ncc
--- a/prelude/logic.ncc
+++ b/prelude/logic.ncc
@@ -20,7 +20,7 @@
 -------------------
 fixity none 5 =:=
 defn =:= : Q -> Q -> prop
-  >| eq = (=:=) {Q = A} B B
+  >| eq = (B : A) =:= B
 
 -- searching for these is SLOW
 fixity none 0 /\
diff --git a/prelude/strings.ncc b/prelude/strings.ncc
--- a/prelude/strings.ncc
+++ b/prelude/strings.ncc
@@ -3,7 +3,7 @@
 ---------------
 -- builtins ---
 ---------------
-defn char : prop  -- builtin
+defn char : prop
 
 defn string : prop
   as list char