packages feed

ivor 0.1.9 → 0.1.10

raw patch · 20 files changed

+671/−375 lines, 20 filesdep +binary

Dependencies added: binary

Files

Ivor/Datatype.lhs view
@@ -6,6 +6,7 @@ > import Ivor.Nobby > import Ivor.PatternDefs > import Ivor.Errors+> import Ivor.Values  > import Debug.Trace @@ -42,8 +43,8 @@ >	        } >       deriving Show -> getPat (Sch p i) = p-> getRed (Sch p i) = i+> getPat (Sch p _ i) = p+> getRed (Sch p _ i) = i  > getArity [] = 2 -- empty data type should have elim rule of arity 2! >                 -- (actually not if they're dependent. Fix this.)@@ -102,7 +103,7 @@ >     do let ps = map (mkPat gamma) pats >	 let rhsvars = getPatVars gamma ps >        let rhs = substVars gamma n rhsvars ret->	 return (Sch (reverse ps) (Ind rhs))+>	 return (Sch (reverse ps) [] (Ind rhs))  Make a pattern from a raw term. Anything weird, just make it a "PTerm".
Ivor/Display.lhs view
@@ -8,6 +8,7 @@ > import Ivor.TTCore > import Ivor.Typecheck > import Ivor.Nobby+> import Ivor.Values  > displayHoleContext :: Gamma Name -> [Name] -> Name -> Indexed Name -> String > displayHoleContext gam hidden h tm =
Ivor/Errors.lhs view
@@ -10,6 +10,7 @@ >             | IMessage String >             | IUnbound (Indexed Name) (Indexed Name) (Indexed Name) (Indexed Name) [Name] >             | INoSuchVar Name+>             | ICantInfer Name (Indexed Name) >             | IContext String IError >   deriving (Show, Eq) @@ -20,3 +21,12 @@ > type IvorM = Either IError  > ifail = Left++Generic error checking can go here:++Check that all the names are real rather than implicit and inferred++> checkRealNames :: [Name] -> Indexed Name -> IvorM ()+> checkRealNames [] tm = return ()+> checkRealNames (nm@(MN ("INFER", n)): ns) tm = ifail (ICantInfer nm tm)+> checkRealNames (_:ns) tm = checkRealNames ns tm
Ivor/Evaluator.lhs view
@@ -1,28 +1,42 @@ > {-# OPTIONS_GHC -fglasgow-exts #-} -> module Ivor.Evaluator(eval_whnf, eval_nf) where+> module Ivor.Evaluator(eval_whnf, eval_nf, eval_nf_without, eval_nf_limit,+>                       eval_nfEnv, tidyNames) where  > import Ivor.TTCore > import Ivor.Gadgets > import Ivor.Constant-> import Ivor.Nobby-> import Ivor.Typecheck+> import Ivor.Values  > import Debug.Trace > import Data.Typeable+> import Control.Monad.State+> import List+> import qualified Data.Map as Map   data Machine = Machine { term :: (TT Name),                           mstack :: [TT Name],                           menv :: [(Name, Binder (TT Name))] }  > eval_whnf :: Gamma Name -> Indexed Name -> Indexed Name-> eval_whnf gam (Ind tm) = let res = makePs (evaluate False gam tm)+> eval_whnf gam (Ind tm) = let res = makePs (evaluate False gam tm Nothing Nothing) >                              in finalise (Ind res)  > eval_nf :: Gamma Name -> Indexed Name -> Indexed Name-> eval_nf gam (Ind tm) = let res = makePs (evaluate True gam tm)+> eval_nf gam (Ind tm) = let res = makePs (evaluate True gam tm Nothing Nothing) >                            in finalise (Ind res) +> eval_nf_without :: Gamma Name -> Indexed Name -> [Name] -> Indexed Name+> eval_nf_without gam tm [] = eval_nf gam tm+> eval_nf_without gam (Ind tm) ns = let res = makePs (evaluate True gam tm (Just ns) Nothing)+>                                       in finalise (Ind res)++> eval_nf_limit :: Gamma Name -> Indexed Name -> [(Name, Int)] -> Indexed Name+> eval_nf_limit gam tm [] = eval_nf gam tm+> eval_nf_limit gam (Ind tm) ns +>     = let res = makePs (evaluate True gam tm Nothing (Just ns))+>           in finalise (Ind res)+ > type Stack = [TT Name] > type SEnv = [(Name, TT Name, TT Name)] @@ -40,82 +54,137 @@ [[let x = t in e]]	xs	es	[[e]], xs, (Let x t: es)  > evaluate :: Bool -> -- under binders? 'False' gives WHNF->             Gamma Name -> TT Name -> TT Name-> evaluate open gam tm = eval tm [] [] []+>             Gamma Name -> TT Name -> +>             Maybe [Name] ->  -- Names not to reduce+>             Maybe [(Name, Int)] -> -- Names to reduce a maximum number+>             TT Name+> evaluate open gam tm jns maxns = -- trace ("EVALUATING: " ++ debugTT tm) $ +>                                  let res = evalState (eval tm [] [] []) maxns+>                                      in {- trace ("RESULT: " ++ debugTT res) -} +>                                         res >   where->     eval :: TT Name -> Stack -> SEnv -> [(Name, TT Name)] -> TT Name->     eval (P x) xs env pats ->         = case lookup x pats of->              Nothing -> evalP x (lookupval x gam) xs env pats->              Just val -> eval val xs env pats->     eval (V i) xs env pats = if (length env>i) ->                                then eval (getEnv i env) xs env pats->                                else unload (V i) xs pats env -- blocked, so unload->     eval (App f a) xs env pats = eval f ((eval a [] env pats):xs) env pats->     eval (Bind n (B Lambda ty) (Sc sc)) xs env pats =->         let ty' = eval ty [] env pats in->             evalScope n ty' sc xs env pats->     eval (Bind n (B Pi ty) (Sc sc)) xs env pats =->         let ty' = eval ty [] env pats in->            unload (Bind n (B Pi ty') (Sc sc)) [] pats env->     eval (Bind n (B (Let val) ty) (Sc sc)) xs env pats =->         eval sc xs ((n,ty,eval val [] env pats):env) pats->     eval (Bind n (B bt ty) (Sc sc)) xs env pats =->         let ty' = eval ty [] env pats in->            unload (Bind n (B bt ty') (Sc sc)) [] pats env->     eval x stk env pats = unload x stk pats env+>     eval :: TT Name -> Stack -> SEnv -> +>             [(Name, TT Name)] -> State (Maybe [(Name, Int)]) (TT Name)+>     eval tm stk env pats = {- trace (show (tm, stk, env, pats)) $ -} eval' tm stk env pats +>     eval' (P x) xs env pats +>         = do mns <- get+>              let (use, mns') = usename x jns mns+>              put mns'+>              case lookup x pats of+>                 Nothing -> if use then evalP x (lookupval x gam) xs env pats+>                                   else evalP x Nothing xs env pats+>                 Just val -> eval val xs env (removep x pats)+>        where removep n [] = []+>              removep n ((x,t):xs) | n==x = removep n xs+>                                   | otherwise = (x,t):(removep n xs)+>     eval' (V i) xs env pats +>              = if (length env>i) +>                   then eval (getEnv i env) xs env pats+>                   else unload (V i) xs pats env -- blocked, so unload+>     eval' (App f a) xs env pats +>        = do a' <- eval a [] env pats+>             eval f (a':xs) env pats+>     eval' (Bind n (B Lambda ty) (Sc sc)) xs env pats+>        = do ty' <- eval ty [] env pats+>             evalScope Lambda n ty' sc xs env pats+>     eval' (Bind n (B Pi ty) (Sc sc)) xs env pats+>        = do ty' <- eval ty [] env pats+>             evalScope Pi n ty' sc xs env pats+>            -- unload (Bind n (B Pi ty') (Sc sc)) [] pats env+>     eval' (Bind n (B (Let val) ty) (Sc sc)) xs env pats +>        = do val' <- eval val [] env pats+>             eval sc xs ((n,ty,val'):env) pats+>     eval' (Bind n (B bt ty) (Sc sc)) xs env pats+>        = do ty' <- eval ty [] env pats+>             unload (Bind n (B bt ty') (Sc sc)) [] pats env+>     eval' x stk env pats = unload x stk pats env+ >     evalP n (Just v) xs env pats  >        = case v of >             Fun opts (Ind v) -> eval v xs env pats->             PatternDef p _ -> pmatch n p xs env pats+>             PatternDef p _ _ -> pmatch n p xs env pats >             PrimOp _ f -> case f xs of >                             Nothing -> unload (P n) xs pats env >                             Just v -> eval v [] env pats >             _ -> unload (P n) xs pats env >     evalP n Nothing xs env pats = unload (P n) xs pats env -- blocked, so unload stack ->     evalScope n ty sc (x:xs) env pats = eval sc xs ((n,ty,x):env) pats->     evalScope n ty sc [] env pats->       | open = let n' = uniqify n (map sfst env)->                    newsc = pToV n' (eval sc [] ((n',ty,P n'):env) pats) in->                    buildenv env $ unload (Bind n' (B Lambda ty) newsc)->                                          [] pats env+>     evalScope b n ty sc (x:xs) env pats = eval sc xs ((n,ty,x):env) pats+>     evalScope b n ty sc [] env pats+>       | open = do let n' = uniqify' n (map sfst env ++ map fst pats)+>                   let  tmpname = (MN ("E", length env))+>                   sc' <- eval sc [] ((n',ty,P tmpname):env) pats+>                   let newsc = pToV tmpname sc'+>                   u' <- unload (Bind n' (B b ty) newsc) [] pats env+>                   return $ buildenv env u' >       | otherwise ->          = buildenv env $ unload (Bind n (B Lambda ty) (Sc sc)) [] pats env -- in Whnf+>          = do let n' = uniqify' n (map sfst env ++ map fst pats)+>               u' <-  unload (Bind n' (B Lambda ty) (Sc sc)) [] pats env -- in Whnf+>               return $ buildenv env u' >     unload x [] pats env ->                = foldl (\tm (n,val) -> substName n val (Sc tm)) x pats+>                = return $ foldl (\tm (n,val) -> substName n val (Sc tm)) x pats >     unload x (a:as) pats env = unload (App x a) as pats env+>+>     uniqify' u@(UN n) ns = uniqify (MN (n,0)) ns+>     uniqify' n ns = uniqify n ns +>     usename x Nothing Nothing = (True, Nothing)+>     usename x _ (Just ys) = case lookup x ys of+>                               Just 0 -> (False, Just ys)+>                               Just n -> (True, Just (update x (n-1) ys))+>                               _ -> (True, Just ys)+>     usename x (Just xs) m = (not (elem x xs), m)++>     update x v [] = []+>     update x v ((k,_):xs) | x == k = ((x,v):xs)+>     update x v (kv:xs) = kv : update x v xs+ >     buildenv [] t = t >     buildenv ((n,ty,tm):xs) t  >                 = buildenv xs (subst tm (Sc t)) >     --            = buildenv xs (Bind n (B (Let tm) ty) (Sc t)) +>     renameRHS pbinds rhs env = rrhs [] [] (nub pbinds) rhs where+>       rrhs namemap pbinds' [] rhs = {-trace ("BEFORE " ++ show (rhs, pbinds, pbinds')) $ -}+>                                     (pbinds', substNames namemap rhs)+>       rrhs namemap pbinds ((n,t):ns) rhs+>          = let n' = uniqify' (UN (show n)) (map sfst env ++ map fst pbinds ++ map fst ns) in+>                rrhs ((n,P n'):namemap) ((n',t):pbinds) ns rhs++>     substNames [] rhs = {-trace ("AFTER " ++ show rhs) $ -} rhs+>     substNames ((n,t):ns) rhs = substNames ns (substName n t (Sc rhs))+ >     pmatch n (PMFun i clauses) xs env pats = ->         case matches clauses xs env pats of->           Nothing -> unload (P n) xs pats env->           Just (rhs, pbinds, stk) -> eval rhs stk env pbinds+>         do cm <- matches clauses xs env pats+>            case cm of+>              Nothing -> unload (P n) xs pats env+>              Just (rhs, pbinds, stk) -> +>                    let (pbinds', rhs') = renameRHS pbinds rhs env in+>                        eval rhs' stk env pbinds' ->     matches [] xs env pats = Nothing+>     matches [] xs env pats = return Nothing >     matches (c:cs) xs env pats ->        = case (match c xs env pats) of->            Just v -> Just v->            Nothing -> matches cs xs env pats+>        = do cm <- (match c xs env pats)+>             case cm of+>               Just v -> return $ Just v+>               Nothing -> matches cs xs env pats ->     match :: Scheme Name -> [TT Name] -> SEnv -> [(Name, TT Name)] ->->              Maybe (TT Name, [(Name, TT Name)], Stack)->     match (Sch pats rhs) xs env patvars ->               = matchargs pats xs rhs env patvars->     matchargs [] xs (Ind rhs) env patvars = Just (rhs, patvars, xs)->     matchargs (p:ps) (x:xs) rhs env patvars->               = case matchPat p (eval x [] env patvars) patvars of->                   Just patvars' -> matchargs ps xs rhs env patvars'->                   Nothing -> Nothing->     matchargs _ _ _ _ _ = Nothing+>     match :: Scheme Name -> [TT Name] -> SEnv -> +>              [(Name, TT Name)] ->+>              State (Maybe [(Name, Int)]) (Maybe (TT Name, [(Name, TT Name)], Stack))+>     match (Sch pats _ rhs) xs env patvars +>               = matchargs pats xs rhs env patvars []+>     matchargs [] xs (Ind rhs) env patvars pv' = return $ Just (rhs, pv', xs)+>     matchargs (p:ps) (x:xs) rhs env patvars pv'+>               = do x' <- (eval x [] env patvars) +>                    case matchPat p x' pv' of+>                      Just patvars' -> matchargs ps xs rhs env patvars patvars'+>                      Nothing -> return Nothing+>     matchargs _ _ _ _ _ _ = return Nothing  >     matchPat PTerm x patvars = Just patvars->     matchPat (PVar n) x patvars = Just ((n,x):patvars)+>     matchPat (PVar n) x patvars = Just ((n,x):patvars) -- (filter (\ (x,y) -> x/=n) patvars)) >     matchPat (PConst t) (Const t') patvars >                  = do tc <- cast t >                       if (tc == t') then Just patvars@@ -134,3 +203,25 @@ >     getConArgs (Con t _ _) args = Just (t, args) >     getConArgs (App f a) args = getConArgs f (a:args) >     getConArgs _ _ = Nothing++++> eval_nfEnv :: Env Name -> Gamma Name -> Indexed Name -> Indexed Name+> eval_nfEnv env g t+>     = eval_nf (addenv env g) t+>   where addenv [] g = g+>         addenv ((n,B (Let v) ty):xs) (Gam g)+>             = addenv xs (Gam (Map.insert n (G (Fun [] (Ind v)) (Ind ty) defplicit) g))+>         addenv (_:xs) g = addenv xs g++Turn MN to UN, if they are unique, so that they look nicer.++> tidyNames :: Indexed Name -> Indexed Name+> tidyNames (Ind tm) = Ind (tidy' [] tm)+>   where tidy' ns (Bind (MN (n,i)) (B b t) (Sc tm)) = +>             let n' = uniqify (UN n) ns in+>                 Bind n' (B b (tidy' ns t)) (Sc (tidy' (n':ns) tm))+>         tidy' ns (Bind x (B b t) (Sc tm)) +>               = Bind x (B b (tidy' ns t)) (Sc (tidy' (x:ns) tm))+>         tidy' ns (App f a) = App (tidy' ns f) (tidy' ns a)+>         tidy' ns x = x
Ivor/ICompile.lhs view
@@ -1,9 +1,12 @@+FIXME: I don't believe this is used. Make it go away.+ > module Ivor.ICompile where  > import Ivor.TTCore > import Ivor.Datatype > import Ivor.Nobby > import Ivor.Gadgets+> import Ivor.Values  > import Data.List > import Debug.Trace@@ -31,8 +34,8 @@ >			 let top = map schhead ss' >			     rest = map schtail ss' in >			 icomp' top rest es'->          schhead (Sch x red) = (head x, red)->          schtail (Sch x red) = Sch (tail x) red+>          schhead (Sch x bs red) = (head x, red)+>          schtail (Sch x bs red) = Sch (tail x) bs red >          icomp' x xs (e:es) | allDisjoint (map fst x) = doCase1 e x >		              | otherwise = error "Can't find a scrutinee" >          orderPatts = sortBy cmpPat@@ -43,7 +46,7 @@ > mangleArgOrder :: [Scheme Name] -> [Int] -> [Scheme Name] > mangleArgOrder [] _ = [] > mangleArgOrder (x:xs) es = (ma' x es):(mangleArgOrder xs es)->    where ma' (Sch ps ired) es = Sch (reorder ps es) ired+>    where ma' (Sch ps bs ired) es = Sch (reorder ps es) bs ired >          reorder ps xs = foldl (\ih x -> (ps!!x):ih) [] xs  > allDisjoint ps = numDisjoint ps == length ps
Ivor/Nobby.lhs view
@@ -5,6 +5,7 @@ > import Ivor.TTCore > import Ivor.Gadgets > import Ivor.Constant+> import Ivor.Values  > import Data.List > import Control.Monad@@ -13,200 +14,6 @@  > import Debug.Trace -To begin, we need to define the context in which normalisation takes place.-The context maps names to user defined functions, constructors and-elimination rules.--Global represents all possible global names --- if it's a user defined-name, hold its definition, otherwise hold what it is so we know what-to do with it, when the time comes.--> data Global n->     = Fun [FunOptions] (Indexed n)    -- User defined function->     | Partial (Indexed n) [n] -- Unfinished definition->     | PatternDef (PMFun n) Bool -- Pattern matching definition, totality->     | ElimRule ElimRule  -- Elimination Rule->     | PrimOp PrimOp EvPrim     -- Primitive function->     | DCon Int Int       -- Data Constructor, tag and arity->     | TCon Int (Elims n) -- Type Constructor and arity, elim rule name->     | Unreducible        -- Unreducible name->     | Undefined          -- Declared but undefined name--> data Elims n = Elims { elimRuleName :: n,->                        caseRuleName :: n,->                        constructors :: [n] }->              | NoConstructorsYet--> data FunOptions = Frozen | Recursive | Total->   deriving Eq--> instance Show n => Show (Global n) where->     show (Fun opts t) = "Fun " ++ show t->     show (ElimRule _) = "<<elim rule>>"->     show (PrimOp _ _) = "<<primitive operator>>"->     show (DCon x t) = "DCon " ++ show x ++ "," ++show t->     show (TCon x (Elims e c cons)) = "TCon " ++ show x->     show Unreducible = "Unreducible"->     show Undefined = "Undefined"--> type Plicity = Int--> defplicit = 0--> data Ord n => Gval n = G (Global n) (Indexed n) Plicity->    deriving Show--> getglob (G v t p) = v-> gettype (G v t p) = t-> getplicity (G v t p) = p--> newtype Ord n => Gamma n = Gam (Map.Map n (Gval n))->     deriving Show--> extend (Gam x) (n,v) = Gam (Map.insert n v x)--> emptyGam :: Ord n => Gamma n-> emptyGam = Gam Map.empty--> getAList :: Ord n => Gamma n -> [(n,(Gval n))]-> getAList (Gam n) = Map.toAscList n--> lookupval :: (Ord n, Eq n) => n -> Gamma n -> Maybe (Global n)-> lookupval n (Gam xs) = fmap getglob (Map.lookup n xs)--> lookuptype :: (Ord n, Eq n) => n -> Gamma n -> Maybe (Indexed n)-> lookuptype n (Gam xs) = fmap gettype (Map.lookup n xs)--> glookup ::  (Ord n, Eq n) => n -> Gamma n -> Maybe (Global n,Indexed n)-> glookup n (Gam xs) = fmap (\x -> (getglob x,gettype x)) (Map.lookup n xs)--Get a type name from the context--> getTyName :: Monad m => Gamma Name -> Name -> m Name-> getTyName  gam n = case lookuptype n gam of->                            Just (Ind ty) -> return $ getFnName ty->                            Nothing -> fail $ "No such name " ++ show n->   where getFnName (TyCon x _) = x->         getFnName (App f x) = getFnName f->         getFnName (Bind _ _ (Sc x)) = getFnName x->         getFnName x = MN ("Dunno: "++show x, 0)--Return whether a name is a recursive constructor (i.e, its family name-occurs anywhere in its arguments).--> recCon :: Name -> Gamma Name -> Bool-> recCon n gam = case glookup n gam of->                  (Just (DCon _ t, Ind ty)) ->->                      checkRec (conFamily ty) (map snd (getExpected ty))->                  _ -> False->    where conFamily t = fname (getFun (getReturnType t))->          fname (TyCon n _) = n->          fname _ = MN ("ERROR!",0)->          checkRec n [] = False->          checkRec n (x:xs) = nameOccurs n (forget x) || checkRec n xs--> insertGam :: Ord n => n -> Gval n -> Gamma n -> Gamma n-> insertGam nm val (Gam gam) = Gam $ Map.insert nm val gam--> concatGam :: Ord n => Gamma n -> Gamma n -> Gamma n-> concatGam (Gam x) (Gam y) = Gam (Map.union x y)--> setFrozen :: (Ord n, Eq n) => n -> Bool -> Gamma n -> Gamma n-> setFrozen n freeze (Gam xs) = Gam $ Map.mapWithKey sf xs where->    sf p (G (Fun opts v) ty plicit)->        | n == p = (G (Fun (doFreeze freeze opts) v) ty plicit)->    sf _ x = x->    doFreeze True opts = nub (Frozen:opts)->    doFreeze False opts = opts \\ [Frozen]--> setRec :: (Ord n, Eq n) => n -> Bool -> Gamma n -> Gamma n-> setRec n frec (Gam xs) = Gam $ Map.mapWithKey sf xs where->    sf p (G (Fun opts v) ty plicit)->        | n == p = (G (Fun (doFrec frec opts) v) ty plicit)->    sf _ x = x->    doFrec True opts = nub (Recursive:opts)->    doFrec False opts = opts \\ [Recursive]---> freeze :: (Ord n, Eq n) => n -> Gamma n -> Gamma n-> freeze n gam = setFrozen n True gam--> thaw :: (Ord n, Eq n) => n -> Gamma n -> Gamma n-> thaw n gam = setFrozen n False gam--Remove a name from the middle of the context - should only be valid-if it's a partial definition or an axiom which is about to be replaced.--> remove :: (Ord n, Eq n) => n -> Gamma n -> Gamma n-> remove n (Gam xs) = Gam $ Map.delete n xs--Insert a name into the context. If the name is already there, this-is an error *unless* the old definition was 'Undefined', in which case-the name is replaced.--> gInsert :: (Monad m, Ord n, Eq n, Show n) => ->            n -> Gval n -> Gamma n -> m (Gamma n)-> gInsert nm val (Gam xs) = case Map.lookup nm xs of->         -- FIXME: Check ty against val->       Nothing -> return $ Gam (Map.insert nm val xs)->       Just (G Undefined ty _) -> return $ Gam (Map.insert nm val xs)->       Just (G (TCon _ NoConstructorsYet) ty _) -> ->                                  return $ Gam (Map.insert nm val xs)->       Just _ -> fail $ "Name " ++ show nm ++ " is already defined"--An ElimRule is a Haskell implementation of the iota reductions of-a family.--> type ElimRule = Spine Value -> Maybe Value--A PrimOp is an external operation--> type PrimOp = Spine Value -> Maybe Value-> type EvPrim = [TT Name] -> Maybe (TT Name) -- same, but with tt terms rather than values--Model represents normal forms, including Ready (reducible) and Blocked-(non-reducible) forms.--> data Model s = MR (Ready s)->              | MB (Blocked s, Model s) (Spine (Model s))--> data Ready s->     = RdBind Name (Binder (Model s)) (s (Model s))->     | RCon Int Name (Spine (Model s))->     | RTyCon Name (Spine (Model s))->     | forall c. Constant c => RdConst c->     | RdStar->     | RdLabel (Model s) (MComp s)->     | RdCall (MComp s) (Model s)->     | RdReturn (Model s)->     | RdCode (Model s)->     | RdQuote (Model s) -- (TT Name)->     | RdInfer--> data Blocked s->     = BCon Int Name Int->     | BTyCon Name Int->     | BElim ElimRule Name->     | BPatDef (PMFun Name) Name->     | BPrimOp PrimOp Name->     | BRec Name Value->     | BP Name->     | BV Int->     | BEval (Model s) (Model s)->     | BEscape (Model s) (Model s)--> data MComp s = MComp Name [Model s]--> newtype Weakening = Wk Int--Second weakening is cached to prevent function composition in the weaken-class.--> newtype Kripke x = Kr (Weakening -> x -> x, Weakening)--> type Value = Model Kripke-> type Normal = Model Scope- > newtype Ctxt = VG [Value]  > type PatVals = [(Name, Value)]@@ -240,11 +47,11 @@ >           Nothing -> evalP (lookupval n gamma) >    where evalP (Just Unreducible) = (MB (BP n,pty n) Empty) >          evalP (Just Undefined) = (MB (BP n, pty n) Empty)->          evalP (Just (PatternDef p@(PMFun 0 pats) _)) =+>          evalP (Just (PatternDef p@(PMFun 0 pats) _ _)) = >              case patmatch gamma g pats [] of >                 Nothing ->  (MB (BPatDef p n, pty n) Empty) >                 Just v -> v->          evalP (Just (PatternDef p _)) = (MB (BPatDef p n, pty n) Empty)+>          evalP (Just (PatternDef p _ _)) = (MB (BPatDef p n, pty n) Empty) >          evalP (Just (Partial (Ind v) _)) = (MB (BP n, pty n) Empty) >          evalP (Just (PrimOp f _)) = (MB (BPrimOp f n, pty n) Empty) >          evalP (Just (Fun opts (Ind v)))@@ -361,7 +168,7 @@  > patmatch :: Gamma Name -> Ctxt -> [PMDef Name] -> [Value] -> Maybe Value > patmatch gam g [] _ = Nothing-> patmatch gam g ((Sch pats ret):ps) vs = case pm gam g pats vs ret [] of+> patmatch gam g ((Sch pats _ ret):ps) vs = case pm gam g pats vs ret [] of >                         Nothing -> patmatch gam g ps vs >                         Just v -> Just v
Ivor/PatternDefs.lhs view
@@ -8,6 +8,7 @@ > import Ivor.Typecheck > import Ivor.Unify > import Ivor.Errors+> import Ivor.Values  > import Debug.Trace > import Data.List@@ -31,6 +32,7 @@ >   let clauses = nub (concat clausesIn) >   let clauses' = filter (mostSpecClause clauses) clauses >   (ty@(Ind ty'),_) <- typecheck gam tyin+>   checkRealNames (getNames (Sc ty')) ty >   let arity = length (getExpected ty') >   checkNotExists fn gam >   gam' <- gInsert fn (G Undefined ty defplicit) gam@@ -85,7 +87,7 @@  Check for definition 1 above: one argument position is well founded ->         wfClause args (Sch pats (Ind t)) = do+>         wfClause args (Sch pats _ (Ind t)) = do >            let recs = findRec [] t >            case recs of >               [] -> return args@@ -94,7 +96,7 @@ Check for definition 2 above: all recursive calls have a decreasing argument and no increasing arguments ->         allDec (Sch pats (Ind t)) err = do+>         allDec (Sch pats _ (Ind t)) err = do >            let recs = findRec [] t >            case allRecDec pats recs of >              Success v -> return v@@ -214,33 +216,47 @@ >                let namesret = filter (notGlobal gam') $ getNames (Sc rtmtt') >                let namesbound = getNames (Sc tmtt) >                checkAllBound (fileLine ret) namesret namesbound (Ind rtmtt') tmtt rty pty->                -- trace (show (unified, rtmtt, tm, rtmtt')) $ ->                return ((tm, Ind rtmtt', newdefs), [], newdefs, True)->         mytypecheck gam (clause, (RWith scr pats)) i =+>                -- trace (show env) $+>                return ((tm, Ind rtmtt', env), [], newdefs, True)+>         mytypecheck gam (clause, (RWith addprf scr pats)) i = >             do -- Get the type of scrutinee, construct the type of the auxiliary definition >                (tm@(Ind clausett), clausety, _, scrty@(Ind stt), env) <- checkAndBindWith gam clause scr fn >                let args = getRawArgs clause->                let restTyin = addLastArg tyin (forget scrty)+>                -- let restTyin = addLastArg tyin (forget scrty) scr >                margs <- getMatches tm tm >                let margNames = nub (map fst margs) >                let newargs = filter (\ (x,ty) -> x `elem` margNames) env >                newpats <- mapM (getNewPat tm 1) pats->                let newfntyin = mkNewTy (newargs ++ [(UN "__scr", B Pi stt)]) clausety->                (newfnTy, _) <- check gam env (forget newfntyin) (Just (Ind Star))+>                let newfntyin = forget (mkNewTy newargs clausety)+>                let newfntyin' = addLastArg newfntyin (forget stt) scr addprf+>                   --(newargs ++ [(UN "__scr", B Pi stt),+>                   --                                (UN "__scrEq", B Pi (screq (UN "__scr") scr))]) clausety+>                (newfnTy, _) <- check gam env newfntyin' (Just (Ind Star)) >                -- Make a name for the new function, clauses in 'pats' need the new name, >                -- and form a definition of type restTy >                let newname = mkNewName fn i >                -- TODO: All pats have to match against args ++ [_]->                -- Final clause returns newname applied to args++scrutinee->                let ret = rawApp (Var newname) ((map Var (map fst newargs)) ++ [scr])+>                -- Final clause returns newname applied to args++scrutinee++refl+>                let ret = rawApp (Var newname) ((map Var (map fst newargs)) ++ +>                              [scr] ++ if addprf then +>                                           [RApp (RApp (Var (UN "refl")) RInfer) RInfer]+>                                          else []) >                let gam' = insertGam newname (G Undefined newfnTy 0) gam->                newpdef <- mapM (newp tm newargs 1) (zip newpats pats)+>                newpdef <- mapM (newp tm newargs 1 addprf) (zip newpats pats) >                (chk, auxdefs, _, _) <- mytypecheck gam' (clause, (RWRet ret)) i >                (auxdefs', newdefs, covers) <- checkDef gam' newname (forget newfnTy) newpdef False cover >                return (chk, auxdefs++auxdefs', newdefs, covers) ->         addLastArg (RBind n (B Pi arg) x) ty = RBind n (B Pi arg) (addLastArg x ty)->         addLastArg x ty = RBind (UN "X") (B Pi ty) x+>         addLastArg (RBind n (B Pi arg) x) ty scr addprf +>                        = RBind n (B Pi arg) (addLastArg x ty scr addprf)+>         addLastArg x ty scr addprf +>            = RBind (UN "__scr") (B Pi ty) +>                 (if addprf then (RBind (UN "__scrEq") (B Pi (screq (UN "__scr") scr)) x)+>                     else x)++>         screq scrname scr = RApp (RApp (RApp (RApp (Var (UN "Eq")) RInfer) RInfer)+>                                scr) (Var scrname)+ >         rawApp f [] = f >         rawApp f (a:as) = rawApp (RApp f a) as @@ -255,13 +271,14 @@ >             (argv, argt, _) <- checkAndBind gam [] pargs Nothing >             getMatches argv proto ->         newp proto newargs i (newps, RSch args ret) = do+>         newp proto newargs i addprf (newps, RSch args ret) = do >             ret' <- newpRet ret->             return $ RSch ((getAuxPats (map fst newargs) newps)++(lastn i args)) ret'->                 where newpRet (RWith v schs) = +>             return $ RSch ((getAuxPats (map fst newargs) newps)++(lastn i args) +++>                              (if addprf then [RInfer] else [])) ret'+>                 where newpRet (RWith prf v schs) =  >                          do newpats <- mapM (getNewPat proto (i+1)) schs->                             newpdef <- mapM (newp proto newargs (i+1)) (zip newpats schs)->                             return (RWith v newpdef)+>                             newpdef <- mapM (newp proto newargs (i+1) prf) (zip newpats schs)+>                             return (RWith prf v newpdef) >                       newpRet r = return r  >         lastn i xs = reverse $ take i (reverse xs)@@ -282,7 +299,7 @@ >         addContext (Just (f,l)) err = IContext (f ++ ":" ++ show l ++ ":") err  > mkScheme :: Gamma Name -> (Indexed Name, Indexed Name) -> PMDef Name-> mkScheme gam (Ind pat, ret) = Sch (map mkpat (getPatArgs pat)) ret+> mkScheme gam (Ind pat, ret) = Sch (map mkpat (getPatArgs pat)) [] ret >   where mkpat (P n) = PVar n >         mkpat (App f a) = addPatArg (mkpat f) (mkpat a) >         mkpat (Con i nm ar) = mkPatV nm (lookupval nm gam)
Ivor/RunTT.lhs view
@@ -2,6 +2,8 @@  > module Ivor.RunTT where +FIXME: We don't use this. Got to go.+ Representation of the run-time language. Used for spitting out GHC core. @@ -9,6 +11,7 @@ > import Ivor.Gadgets > import Ivor.ICompile > import Ivor.Nobby+> import Ivor.Values  When we compile, we need to know the term as well as bits of info about its type, ie its arity and emptiness.
Ivor/Scopecheck.lhs view
@@ -5,6 +5,7 @@ > import Ivor.TTCore > import Ivor.Nobby > import Ivor.Typecheck+> import Ivor.Values  Typechecking on terms we assume to be okay - in other words, just convert  bound names to a de Bruijn index.
Ivor/Shell.lhs view
@@ -158,9 +158,9 @@ >                         (Name DataCon _) -> return (respondLn st "Data constructor") >                         _ -> fail "Unknown definition" >     where printPats (Patterns cs) = unlines (map printClause cs)->           printClause (PClause args ret) = n ++ " " ++->                                            unwords (map argshow args) ++->                                            " = " ++ show ret+>           printClause (PClause args _ ret) = n ++ " " +++>                                              unwords (map argshow args) +++>                                              " = " ++ show ret >           argshow x | ' ' `elem` show x = "(" ++ show x ++ ")" >                     | otherwise = show x
Ivor/ShellParser.lhs view
@@ -131,7 +131,7 @@ > pclauseret :: [ViewTerm] -> Maybe (Parser ViewTerm) -> Parser PClause > pclauseret args ext = do lchar '=' >                          ret <- pTerm ext->                          return $ PClause args ret+>                          return $ PClause args [] ret  > pclausewith :: String -> [ViewTerm] -> Maybe (Parser ViewTerm) -> Parser PClause > pclausewith nm args ext = do lchar '|'@@ -139,7 +139,7 @@ >                              lchar '{' >                              pats <- ppatterns nm ext >                              lchar '}'->                              return $ PWithClause args scr pats+>                              return $ PWithClause False args scr pats  > ppatterns :: String -> Maybe (Parser ViewTerm) -> Parser Patterns > ppatterns name ext
Ivor/State.lhs view
@@ -1,4 +1,4 @@-> {-# OPTIONS_GHC -fglasgow-exts #-}+\> {-# OPTIONS_GHC -fglasgow-exts #-}  > module Ivor.State where @@ -17,6 +17,7 @@ > import Ivor.Display > import Ivor.Unify > import Ivor.Errors+> import Ivor.Values  > import System.Environment > import Data.List@@ -107,7 +108,7 @@ >              gInsert n gl ctxt >          addElim ctxt erule schemes = do >            newdefs <- gInsert (fst erule)->                               (G (PatternDef schemes True) (snd erule) defplicit)+>                               (G (PatternDef schemes True False) (snd erule) defplicit) >                               ctxt >            return newdefs
Ivor/TT.lhs view
@@ -35,8 +35,8 @@ >               proofterm, getGoals, getGoal, uniqueName, -- getActions >               allSolved,qed, >               -- * Examining the Context->               eval, whnf, evalnew, evalCtxt, getDef, defined, getPatternDef,->               getAllTypes, getAllDefs, getAllPatternDefs, getConstructors,+>               eval, whnf, evalnew, evalnewWithout, evalnewLimit, evalCtxt, getDef, defined, getPatternDef,+>               getAllTypes, getAllDefs, getAllPatternDefs, isAuxPattern, getConstructors, >               getInductive, getAllInductives, getType, >               Rule(..), getElimRule, nameType, getConstructorTag, >               getConstructorArity,@@ -113,6 +113,7 @@ > import Ivor.CodegenC > import Ivor.PatternDefs > import Ivor.Errors+> import Ivor.Values  > import Data.List > import Debug.Trace@@ -188,6 +189,7 @@ >              | Message String >              | Unbound ViewTerm ViewTerm ViewTerm ViewTerm [Name] >              | NoSuchVar Name+>              | CantInfer Name ViewTerm >              | ErrContext String TTError  > instance Show TTError where@@ -197,6 +199,7 @@ >     show (Unbound clause clty rhs rhsty ns)  >        = show ns ++ " unbound in clause " ++ show clause ++ " : " ++ show clty ++  >                     " = " ++ show rhs+>     show (CantInfer  n tm) = "Can't infer value for " ++ show n ++ " in " ++ show tm >     show (NoSuchVar n) = "No such name as " ++ show n >     show (ErrContext c err) = c ++ show err @@ -223,6 +226,7 @@ >                        (view (Term (rhs, Ind TTCore.Star))) >                        (view (Term (rhsty, Ind TTCore.Star))) >                        names+> getError (ICantInfer nm tm) = CantInfer nm (view (Term (tm, Ind TTCore.Star))) > getError (INoSuchVar n) = NoSuchVar n > getError (IContext s e) = ErrContext s (getError e) @@ -263,9 +267,11 @@  > data PClause = PClause { >                         arguments :: [ViewTerm],+>                         boundnames :: [(Name, ViewTerm)], >                         returnval :: ViewTerm >                        } >              | PWithClause {+>                         eqproof :: Bool, >                         arguments :: [ViewTerm], >                         scrutinee :: ViewTerm, >                         patterns :: Patterns@@ -276,10 +282,10 @@ >    deriving Show  > mkRawClause :: PClause -> RawScheme-> mkRawClause (PClause args ret) =+> mkRawClause (PClause args _ ret) = >     RSch (map forget args) (RWRet (forget ret))-> mkRawClause (PWithClause args scr (Patterns rest)) = ->     RSch (map forget args) (RWith (forget scr) (map mkRawClause rest))+> mkRawClause (PWithClause prf args scr (Patterns rest)) = +>     RSch (map forget args) (RWith prf (forget scr) (map mkRawClause rest))  > -- ^ Convert a term to matchable pattern form; i.e. the only names allowed > -- are variables and constructors. Any arbitrary function application is@@ -339,8 +345,9 @@ >         return (Ctxt st { defs = newdefs }, vnewnames) >   where insertAll [] gam tot = return gam >         insertAll ((nm, def, ty):xs) gam tot = ->             do gam' <- gInsert nm (G (PatternDef def tot) ty defplicit) gam+>             do gam' <- gInsert nm (G (PatternDef def tot (gen nm)) ty defplicit) gam >                insertAll xs gam' tot+>         gen nm = nm /= n -- generated if it's not the provided name.  > -- |Add a new definition, with its type to the global state. > -- These definitions can be recursive, so use with care.@@ -480,8 +487,9 @@ >        t <- raw tm >        let Gam ctxt = defs st >        case (typecheck (defs st) t) of->           (Right (t, ty)) ->->              do tt $ checkConv (defs st) ty (Ind TTCore.Star) (IMessage "Not a type")+>           (Right (t@(Ind t'), ty)) ->+>              do tt $ checkRealNames (getNames (Sc t')) t+>                 tt $ checkConv (defs st) ty (Ind TTCore.Star) (IMessage "Not a type") >                 -- let newdefs = Gam ((n, (G und (finalise t))):ctxt) >                 newdefs <- gInsert n (G und (finalise t) defplicit) (Gam ctxt) >                 return $ Ctxt st { defs = newdefs }@@ -704,9 +712,9 @@ > resume :: Context -> Name -> TTM Context > resume ctxt@(Ctxt st) n = >     case glookup n (defs st) of->         Just ((Ivor.Nobby.Partial _ _),_) -> do let (Ctxt st) = suspend ctxt->                                                 st' <- tt$ resumeProof st n->                                                 return (Ctxt st')+>         Just ((Ivor.Values.Partial _ _),_) -> do let (Ctxt st) = suspend ctxt+>                                                  st' <- tt$ resumeProof st n+>                                                  return (Ctxt st') >         Just (Unreducible,ty) -> >             do let st' = st { defs = remove n (defs st) } >                theorem (Ctxt st') n (Term (ty, Ind TTCore.Star))@@ -721,7 +729,7 @@ > freeze (Ctxt st) n >      = case glookup n (defs st) of >           Nothing -> fail $ show n ++ " is not defined"->           _ -> return $ Ctxt st { defs = Ivor.Nobby.freeze n (defs st) }+>           _ -> return $ Ctxt st { defs = Ivor.Values.freeze n (defs st) }  > -- | Unfreeze a name (i.e., allow it to reduce). > -- Fails if the name does not exist.@@ -729,7 +737,7 @@ > thaw (Ctxt st) n >      = case glookup n (defs st) of >           Nothing -> fail $ show n ++ " is not defined"->           _ -> return $ Ctxt st { defs = Ivor.Nobby.thaw n (defs st) }+>           _ -> return $ Ctxt st { defs = Ivor.Values.thaw n (defs st) }   > -- | Save the state (e.g. for Undo)@@ -773,9 +781,21 @@  > -- |Reduce a term and its type to Normal Form (using new evaluator) > evalnew :: Context -> Term -> Term-> evalnew (Ctxt st) (Term (tm,ty)) = Term (eval_nf (defs st) tm,->                                          eval_nf (defs st) ty)+> evalnew (Ctxt st) (Term (tm,ty)) = Term (tidyNames (eval_nf (defs st) tm),+>                                          tidyNames (eval_nf (defs st) ty)) +> -- |Reduce a term and its type to Normal Form (using new evaluator, not+> -- reducing given names)+> evalnewWithout :: Context -> Term -> [Name] -> Term+> evalnewWithout (Ctxt st) (Term (tm,ty)) ns = Term (tidyNames (eval_nf_without (defs st) tm ns),+>                                                    tidyNames (eval_nf_without (defs st) ty ns))++> -- |Reduce a term and its type to Normal Form (using new evaluator, reducing+> -- given names a maximum number of times)+> evalnewLimit :: Context -> Term -> [(Name, Int)] -> Term+> evalnewLimit (Ctxt st) (Term (tm,ty)) ns = Term (eval_nf_limit (defs st) tm ns,+>                                                  eval_nf_limit (defs st) ty ns)+ > -- |Check a term in the context of the given goal > checkCtxt :: (IsTerm a) => Context -> Goal -> a -> TTM Term > checkCtxt (Ctxt st) goal tm =@@ -877,7 +897,7 @@ > getPatternDef :: Context -> Name -> TTM (ViewTerm, Patterns) > getPatternDef (Ctxt st) n >     = case glookup n (defs st) of->           Just ((PatternDef pmf _),ty) ->+>           Just ((PatternDef pmf _ _),ty) -> >               return $ (view (Term (ty, Ind TTCore.Star)),  >                         Patterns (map mkPat (getPats pmf))) >           Just ((Fun _ ind), ty) ->@@ -885,8 +905,12 @@ >                         Patterns [mkCAFpat ind]) >           _ -> fail "Not a pattern matching definition" >    where getPats (PMFun _ ps) = ps->          mkPat (Sch ps ret) = PClause (map viewPat ps) (view (Term (ret, (Ind TTCore.Star))))->          mkCAFpat tm = PClause [] (view (Term (tm, (Ind TTCore.Star))))+>          mkPat (Sch ps bs ret) +>               = PClause (map viewPat ps) +>                         (map (\ (n, B _ t) -> +>                            (n, (view (Term (Ind t, (Ind TTCore.Star)))))) bs)+>                 (view (Term (ret, (Ind TTCore.Star))))+>          mkCAFpat tm = PClause [] [] (view (Term (tm, (Ind TTCore.Star)))) >          viewPat (PVar n) = Name Bound n --(name (show n)) >          viewPat (PCon t n ty ts) = VTerm.apply (Name Bound (name (show n))) (map viewPat ts) >          viewPat (PConst c) = Constant c@@ -908,6 +932,14 @@ >                          Right d -> (x,d):(getPD xs) >                          _ -> getPD xs +> -- |Is the name an auxiliary function of a pattern definition (e.g. generated by a with+> -- clause?+> isAuxPattern :: Context -> Name -> Bool+> isAuxPattern (Ctxt st) n = case glookup n (defs st) of+>           Just ((PatternDef pmf _ gen),ty) -> gen+>           _ -> False++ > -- |Get all the inductive type definitions in the context. > getAllInductives :: Context -> [(Name,Inductive)] > getAllInductives ctxt @@ -971,7 +1003,7 @@ >             elim <- lookupM rule (eliminators st) >             return $ Patterns $ map mkRed (fst $ snd elim) >       Nothing -> fail $ (show nm) ++ " is not a type constructor"->  where mkRed (RSch pats (RWRet ret)) = PClause (map viewRaw pats) (viewRaw ret)+>  where mkRed (RSch pats (RWRet ret)) = PClause (map viewRaw pats) [] (viewRaw ret) >         -- a reduction will only have variables and applications >        viewRaw (Var n) = Name Free n >        viewRaw (RApp f a) = VTerm.App (viewRaw f) (viewRaw a)
Ivor/TTCore.lhs view
@@ -9,6 +9,7 @@ > import Data.Char > import Control.Monad.State > import Data.Typeable+> import Data.Binary hiding (get,put) > import Debug.Trace  Raw terms are those read in directly from the user, and may be badly typed.@@ -149,8 +150,8 @@  Data declarations and pattern matching -> data RawWith = RWith Raw [RawScheme] -- match with an extra arg, add new schemes->              | RWRet Raw+> data RawWith = RWith Bool Raw [RawScheme] -- match with an extra arg, add new schemes+>              | RWRet Raw                  -- if Bool is true, add an equality proof >   deriving Show   data With = With [Indexed n]@@ -161,7 +162,7 @@ > data RawScheme = RSch [Raw] RawWith >   deriving Show -> data Scheme n = Sch [Pattern n] {- With -} (Indexed n)+> data Scheme n = Sch [Pattern n] (Env n) (Indexed n) >         deriving Show  > type PMRaw = RawScheme@@ -742,6 +743,7 @@ >       fPrec _ (RInfer) = "_" >       fPrec _ (RMeta n) = "?"++forget n >       fPrec p (RFileLoc f l t) = fPrec p t+>       fPrec p (RAnnot s) = "[" ++ s ++ "]" >       bracket outer inner str | inner>outer = "("++str++")" >                               | otherwise = str @@ -940,3 +942,32 @@ >        forgetTT (Stage (Escape t _)) = RStage (REscape (forgetTT t)) >        forgetTT (Const x) = RConst x >        forgetTT Star = RStar++> pToV :: Eq n => n -> (TT n) -> (Scope (TT n))+> pToV = pToV2 0++> pToV2 v p (P n) | p==n = Sc (V v)+>                 | otherwise = Sc (P n)+> pToV2 v p (V w) = Sc (V w)+> pToV2 v p (Con t n i) = Sc (Con t n i)+> pToV2 v p (TyCon n i) = Sc (TyCon n i)+> pToV2 v p (Meta n t) = Sc (Meta n (getSc (pToV2 v p t)))+>				where getSc (Sc a) = a+> pToV2 v p (Elim n) = Sc (Elim n)+> pToV2 v p (Bind n b (Sc sc)) = Sc (Bind n (fmap (getSc.(pToV2 v p)) b)+>                                    (pToV2 (v+1) p sc))+>				where getSc (Sc a) = a+> pToV2 v p (App f a) = Sc $ App (getSc (pToV2 v p f))+>                               (getSc (pToV2 v p a))+>				where getSc (Sc a) = a+> pToV2 v p (Label t (Comp n ts)) = Sc $ Label (getSc (pToV2 v p t))+>                                         (Comp n (map (getSc.(pToV2 v p)) ts))+> pToV2 v p (Call (Comp n ts) t) = Sc $ Call +>                                        (Comp n (map (getSc.(pToV2 v p)) ts))+>                                        (getSc (pToV2 v p t))+> pToV2 v p (Return t) = Sc $ Return (getSc (pToV2 v p t))+> pToV2 v p (Proj n i t) = Sc $ Proj n i (getSc (pToV2 v p t))+>				where getSc (Sc a) = a+> pToV2 v p (Stage t) = Sc $ Stage (sLift (getSc.(pToV2 v p)) t)+> pToV2 v p (Const x) = Sc (Const x)+> pToV2 v p Star = Sc Star
Ivor/Tactics.lhs view
@@ -8,6 +8,7 @@ > import Ivor.Gadgets > import Ivor.Unify > import Ivor.Errors+> import Ivor.Values  > import Data.List > import Data.Maybe@@ -471,9 +472,10 @@  > casetac :: Bool -> Raw -> Tactic > casetac rec scrutinee gam env tm@(Ind (Bind x (B Hole ty) sc)) =->     do (Ind bv,bt) <- check gam (ptovenv env) scrutinee Nothing+>     do (bv,bt) <- check gam (ptovenv env) scrutinee Nothing >        let (Ind btnorm) = (normaliseEnv (ptovenv env) gam bt)->        let bvin = makePsEnv (map fst env) bv+>        let (Ind bvnorm) = (normaliseEnv (ptovenv env) gam bv)+>        let bvin = makePsEnv (map fst env) bvnorm >        let btin = makePsEnv (map fst env) btnorm >        let indices = getArgs btin >        let ty = getFun btin
Ivor/Typecheck.lhs view
@@ -12,6 +12,8 @@ > import Ivor.Unify > import Ivor.Constant > import Ivor.Errors+> import Ivor.Evaluator+> import Ivor.Values  > import Control.Monad.State > import Data.List@@ -93,7 +95,7 @@ > type Level = Int  > data FileContext = FC FilePath Int->   deriving Eq+>   deriving (Show, Eq)  > errCtxt :: Maybe FileContext -> IError -> IError > errCtxt (Just (FC f l)) err = IContext (f ++ ":" ++ show l ++ ":") err@@ -121,20 +123,25 @@ >          let ty' = papp subst ty >          return (Ind tm',Ind ty') ->    where mkSubst xs = mkSubst' (P,[]) xs->          mkSubst' acc [] = return acc->          mkSubst' acc (q:xs) ->             = do acc' <- mkSubstQ acc q->                  mkSubst' acc' xs+Handy to pass through all the variables, for tracing purposes when debugging.++>    where mkSubst xs = mkSubst' (P,[]) xs xs+>          mkSubst' acc [] all = return acc+>          mkSubst' acc (q:xs) all+>             = do acc' <- mkSubstQ acc q all+>                  mkSubst' acc' xs all >->          mkSubstQ (s',nms) (ok, (env,Ind x,Ind y,fc))+>          eqn (ok, (env, x, y, fc)) = if ok then (x,y,fc) else (x,y,Nothing)+>          showeqn all = concat $ map ((++"\n").show.eqn) all++>          mkSubstQ (s',nms) (ok, (env,Ind x,Ind y,fc)) all >             = do -- (s',nms) <- mkSubst xs >                  let x' = papp s' x->                  let (Ind y') = normalise gam (Ind (papp s' y))->                  uns <- ->                         case unifyenvErr ok gam env (Ind x') (Ind y') of->                           Right x' -> return x'->                           Left err -> ifail (errCtxt fc err)+>                  let (Ind y') = eval_nf gam (Ind (papp s' y))+>                  uns <- case unifyenvErr ok gam env (Ind y') (Ind x') of+>                           Right uns -> {- trace (show (y', x', uns)) $ -} return uns+>                           Left err -> {- trace (showeqn all) $ -} +>                                       ifail (errCtxt fc (ICantUnify (Ind y') (Ind x')))                           Failure err -> fail $ err ++"\n" ++ show nms ++"\n" ++ show constraints -- $ -} ++ " Can't convert "++show x'++" and "++show y' ++ "\n" ++ show constraints ++ "\n" ++ show nms @@ -150,6 +157,15 @@ >          delta n ty n' | n == n' = ty >                        | otherwise = P n' +> convertAllEnv :: Gamma Name -> +>                  [(Env Name, Indexed Name, Indexed Name,Maybe FileContext)] ->+>                  Env Name -> IvorM (Env Name)+> convertAllEnv gam constraints [] = return []+> convertAllEnv gam constraints ((n,B b t):xs) +>       = do (Ind t', _) <- doConversion RStar gam constraints (Ind t) (Ind Star)+>            xs' <- convertAllEnv gam constraints xs+>            return ((n,B b t'):xs')+ > check :: Gamma Name -> Env Name -> Raw -> Maybe (Indexed Name) ->  >          IvorM (Indexed Name, Indexed Name) > check gam env tm mty = do@@ -175,7 +191,11 @@ >    -- rename all the 'inferred' things to another generated name, >    -- so that they actually get properly checked on the rhs >    let realNames = mkNames next+>    -- The environment will need the conversions applying, to fill in any implicit+>    -- variables in the pattern+>    e <- convertAllEnv gam bs e >    e' <- renameB gam realNames (renameBinders e)+>    (v1, t1) <- doConversion tm1 gam bs v1 t1 >    (v1', t1') <- fixupGam gam realNames (v1, t1) >    (v1''@(Ind vtm),t1'') <- doConversion tm1 gam bs v1' t1' -- (normalise gam t1')  >    -- Drop names out of e' that don't appear in v1'' as a result of the@@ -212,7 +232,11 @@ >    -- rename all the 'inferred' things to another generated name, >    -- so that they actually get properly checked on the rhs >    let realNames = mkNames next+>    -- The environment will need the conversions applying, to fill in any implicit+>    -- variables in the pattern+>    e <- convertAllEnv gam bs e >    e' <- renameB gam realNames (renameBinders e)+>    (v1, t1) <- doConversion tm1 gam bs v1 t1 >    (v1', t1') <- fixupGam gam realNames (v1, t1) >    (v1''@(Ind vtm),t1'') <- doConversion tm1 gam bs v1' t1' -- (normalise gam t1')  >    -- Drop names out of e' that don't appear in v1'' as a result of the@@ -292,7 +316,7 @@ >     -- Then check the resulting type matches the expected type. >     if infer then (case exp of >              Nothing -> return ()->              Just expty -> checkConvSt env gamma expty tmty )+>              Just expty -> checkConvSt env gamma tmty expty ) >       else return () >     -- Then fill in any remained inferred values we got by knowing the >     -- expected type@@ -330,7 +354,7 @@ >    where mkTT (Just (i, B _ t)) _ = return (Ind (P n), Ind t) >          mkTT Nothing (Just ((Fun _ _),t)) = return (Ind (P n), t) >          mkTT Nothing (Just ((Partial _ _),t)) = return (Ind (P n), t)->          mkTT Nothing (Just ((PatternDef _ _),t)) = return (Ind (P n), t)+>          mkTT Nothing (Just ((PatternDef _ _ _),t)) = return (Ind (P n), t) >          mkTT Nothing (Just (Unreducible,t)) = return (Ind (P n), t) >          mkTT Nothing (Just (Undefined,t)) = return (Ind (P n), t) >          mkTT Nothing (Just ((ElimRule _),t)) = return (Ind (Elim n), t)@@ -345,12 +369,14 @@  >          defaultResult = do >              (next, infer, bindings, errs, mvs, fc) <- get->              if infer->                 then case exp of+>              case lookup n bindings of+>                Nothing -> +>                 if infer then case exp of >                        Nothing -> lift $ ifail (errCtxt fc (INoSuchVar n)) >                        Just (Ind t) -> do put (next, infer, (n, B Pi t):bindings, errs, mvs, fc) >                                           return (Ind (P n), Ind t)->                 else lift $ ifail (errCtxt fc (INoSuchVar n))+>                          else lift $ ifail (errCtxt fc (INoSuchVar n))+>                Just (B Pi t) -> return (Ind (P n), Ind t)  >  tc env lvl (RApp f a) exp = do >     (Ind fv, Ind ft) <- tcfixup env lvl f Nothing@@ -360,10 +386,10 @@ >       case (fnfng,fnf) of >        ((Ind (Bind _ (B Pi s) (Sc t))),_) -> do >          (Ind av,Ind at) <- tcfixup env lvl a (Just (Ind s))->          let sty = (normaliseEnv env emptyGam (Ind s))+>          let sty = (normaliseEnv env gamma (Ind s)) >          let tt = (Bind (MN ("x",0)) (B (Let av) at) (Sc t)) >          let tmty = (normaliseEnv env emptyGam (Ind tt))->          checkConvSt env gamma (Ind at) (Ind s)+>          checkConvSt env gamma (Ind at) sty >          return (Ind (App fv av), tmty) >        (_, (Ind (Bind _ (B Pi s) (Sc t)))) -> do >          (Ind av,Ind at) <- tcfixup env lvl a (Just (Ind s))@@ -520,18 +546,23 @@ >  checkbinder gamma env lvl n (B Lambda t) = do >     (Ind tv,Ind tt) <- tcfixup env lvl t (Just (Ind Star)) >     let ttnf = normaliseEnv env gamma (Ind tt)+>     let (Ind tvnf) = normaliseEnv env gamma (Ind tv) >     case ttnf of->       (Ind Star) -> return (B Lambda tv)->       (Ind (P (MN ("INFER",_)))) -> return (B Lambda tv)+>       (Ind Star) -> return (B Lambda tvnf)+>       (Ind (P (MN ("INFER",_)))) -> return (B Lambda tvnf) >       _ -> fail $ "The type of the binder " ++ show n ++ " must be *" >  checkbinder gamma env lvl n (B Pi t) = do >     (Ind tv,Ind tt) <- tcfixup env lvl t (Just (Ind Star))->     let ttnf = normaliseEnv env gamma (Ind tt)->     case ttnf of->       (Ind Star) -> return (B Pi tv)->       (Ind (P (MN ("INFER",_)))) -> return (B Pi tv)->       _ -> fail $ "The type of the binder " ++ show n ++ " must be *"+>     let (Ind tvnf) = normaliseEnv env gamma (Ind tv)+>     -- let ttnf = normaliseEnv env gamma (Ind tt)+>     checkConvSt env gamma (Ind tt) (Ind Star)+>     return (B Pi tvnf) +     case ttnf of+       (Ind Star) -> return (B Pi tv)+       (Ind (P (MN ("INFER",_)))) -> return (B Pi tv)+       _ -> fail $ "The type of the binder " ++ show n ++ " must be *"+ >  checkbinder gamma env lvl n (B (Let v) RInfer) = do >     (Ind vv,Ind vt) <- tcfixup env lvl v Nothing >     return (B (Let vv) vt)@@ -705,35 +736,6 @@ > checkNotHoley i (Bind _ _ (Sc s)) = checkNotHoley (i+1) s > checkNotHoley i (Proj _ _ t) = checkNotHoley i t > checkNotHoley _ _ = return ()--> pToV :: Eq n => n -> (TT n) -> (Scope (TT n))-> pToV = pToV2 0--> pToV2 v p (P n) | p==n = Sc (V v)->                 | otherwise = Sc (P n)-> pToV2 v p (V w) = Sc (V w)-> pToV2 v p (Con t n i) = Sc (Con t n i)-> pToV2 v p (TyCon n i) = Sc (TyCon n i)-> pToV2 v p (Meta n t) = Sc (Meta n (getSc (pToV2 v p t)))->				where getSc (Sc a) = a-> pToV2 v p (Elim n) = Sc (Elim n)-> pToV2 v p (Bind n b (Sc sc)) = Sc (Bind n (fmap (getSc.(pToV2 v p)) b)->                                    (pToV2 (v+1) p sc))->				where getSc (Sc a) = a-> pToV2 v p (App f a) = Sc $ App (getSc (pToV2 v p f))->                               (getSc (pToV2 v p a))->				where getSc (Sc a) = a-> pToV2 v p (Label t (Comp n ts)) = Sc $ Label (getSc (pToV2 v p t))->                                         (Comp n (map (getSc.(pToV2 v p)) ts))-> pToV2 v p (Call (Comp n ts) t) = Sc $ Call ->                                        (Comp n (map (getSc.(pToV2 v p)) ts))->                                        (getSc (pToV2 v p t))-> pToV2 v p (Return t) = Sc $ Return (getSc (pToV2 v p t))-> pToV2 v p (Proj n i t) = Sc $ Proj n i (getSc (pToV2 v p t))->				where getSc (Sc a) = a-> pToV2 v p (Stage t) = Sc $ Stage (sLift (getSc.(pToV2 v p)) t)-> pToV2 v p (Const x) = Sc (Const x)-> pToV2 v p Star = Sc Star   checkR g t = (typecheck g t):: (Result (Indexed Name, Indexed Name))
Ivor/Unify.lhs view
@@ -5,6 +5,8 @@ > import Ivor.Nobby > import Ivor.TTCore > import Ivor.Errors+> import Ivor.Evaluator+> import Ivor.Values  > import Data.List @@ -43,10 +45,17 @@ >     case unifynferr i env (p x) >                           (p y) of >           (Right x) -> return x->           _ -> unifynferr i env (p (normalise (gam' gam) x))->                                 (p (normalise (gam' gam) y))->    where p (Ind t) = Ind (makePs t)++>           _ -> {- trace (dbgtt x ++ ", " ++ dbgtt y ++"\n") $ -}+>                unifynferr i env (p (eval_nf (gam' gam) x))+>                                 (p (eval_nf (gam' gam) y))++           _ -> unifynferr i env (p (normalise (gam' gam) x))+                                 (p (normalise (gam' gam) y))++>    where p (Ind t) = Ind t --(makePs t) >          gam' g = concatGam g (envToGamHACK env)+>          dbgtt (Ind x) = show x -- debugTT x  Make the local environment something that Nobby knows about. Very hacky... @@ -75,6 +84,15 @@ >              | x == y = return acc >              | loc x envl == loc y envr && loc x envl >=0 >                  = return acc+>              | hole envl x && hole envl y = return ((x, (P y)): acc)+>          un envl envr (Bind x (B Lambda ty) (Sc (App scl (P x')))) y acc+>                | x == x' = un envl envr scl y acc+>          un envl envr y (Bind x (B Lambda ty) (Sc (App scr (P x')))) acc+>                | x == x' = un envl envr y scr acc+>          un envl envr (Bind x (B Lambda ty) (Sc (App scl (V 0)))) y acc+>                = un envl envr y scl acc+>          un envl envr y (Bind x (B Lambda ty) (Sc (App scr (V 0)))) acc+>                = un envl envr y scr acc >          un envl envr (P x) t acc | hole envl x = return ((x,t):acc) >          un envl envr t (P x) acc | hole envl x = return ((x,t):acc) >          un envl envr (Bind x b@(B Hole ty) (Sc sc)) t acc@@ -82,6 +100,10 @@ >          un envl envr (Bind x b (Sc sc)) (Bind x' b' (Sc sc')) acc = >              do acc' <- unb envl envr b b' acc >                 un ((x,b):envl) ((x',b'):envr) sc sc' acc'+>          un envl envr (Bind x b@(B (Let v) ty) (Sc sc)) t acc+>             = un ((x,b):envl) envr sc t acc+>          un envl envr t (Bind x b@(B (Let v) ty) (Sc sc)) acc+>             = un envl ((x,b):envr) t sc acc >                 -- combine bu scu >          -- if unifying the functions fails because the names are different, >          -- unifying the arguments is going to be a waste of time bec
+ Ivor/Values.lhs view
@@ -0,0 +1,212 @@+> {-# OPTIONS_GHC -fglasgow-exts #-}++FIXME: Most of this stuff and Ivor.Nobby have GOT TO GO!!!++> module Ivor.Values where++> import Ivor.TTCore+> import Ivor.Gadgets+> import Ivor.Constant++> import Debug.Trace+> import Data.Typeable+> import Control.Monad.State+> import List+> import qualified Data.Map as Map++To begin, we need to define the context in which normalisation takes place.+The context maps names to user defined functions, constructors and+elimination rules.++Global represents all possible global names --- if it's a user defined+name, hold its definition, otherwise hold what it is so we know what+to do with it, when the time comes.++> data Global n+>     = Fun [FunOptions] (Indexed n)    -- User defined function+>     | Partial (Indexed n) [n] -- Unfinished definition+>     | PatternDef (PMFun n) Bool Bool -- Pattern matching definition, totality, generated+>     | ElimRule ElimRule  -- Elimination Rule+>     | PrimOp PrimOp EvPrim     -- Primitive function+>     | DCon Int Int       -- Data Constructor, tag and arity+>     | TCon Int (Elims n) -- Type Constructor and arity, elim rule name+>     | Unreducible        -- Unreducible name+>     | Undefined          -- Declared but undefined name++> data Elims n = Elims { elimRuleName :: n,+>                        caseRuleName :: n,+>                        constructors :: [n] }+>              | NoConstructorsYet++> data FunOptions = Frozen | Recursive | Total+>   deriving Eq++> instance Show n => Show (Global n) where+>     show (Fun opts t) = "Fun " ++ show t+>     show (ElimRule _) = "<<elim rule>>"+>     show (PrimOp _ _) = "<<primitive operator>>"+>     show (DCon x t) = "DCon " ++ show x ++ "," ++show t+>     show (TCon x (Elims e c cons)) = "TCon " ++ show x+>     show Unreducible = "Unreducible"+>     show Undefined = "Undefined"++> type Plicity = Int++> defplicit :: Int+> defplicit = 0++> data Ord n => Gval n = G (Global n) (Indexed n) Plicity+>    deriving Show++> getglob (G v t p) = v+> gettype (G v t p) = t+> getplicity (G v t p) = p++> newtype Ord n => Gamma n = Gam (Map.Map n (Gval n))+>     deriving Show++> extend (Gam x) (n,v) = Gam (Map.insert n v x)++> emptyGam :: Ord n => Gamma n+> emptyGam = Gam Map.empty++> getAList :: Ord n => Gamma n -> [(n,(Gval n))]+> getAList (Gam n) = Map.toAscList n++> lookupval :: (Ord n, Eq n) => n -> Gamma n -> Maybe (Global n)+> lookupval n (Gam xs) = fmap getglob (Map.lookup n xs)++> lookuptype :: (Ord n, Eq n) => n -> Gamma n -> Maybe (Indexed n)+> lookuptype n (Gam xs) = fmap gettype (Map.lookup n xs)++> glookup ::  (Ord n, Eq n) => n -> Gamma n -> Maybe (Global n,Indexed n)+> glookup n (Gam xs) = fmap (\x -> (getglob x,gettype x)) (Map.lookup n xs)++Get a type name from the context++> getTyName :: Monad m => Gamma Name -> Name -> m Name+> getTyName  gam n = case lookuptype n gam of+>                            Just (Ind ty) -> return $ getFnName ty+>                            Nothing -> fail $ "No such name " ++ show n+>   where getFnName (TyCon x _) = x+>         getFnName (App f x) = getFnName f+>         getFnName (Bind _ _ (Sc x)) = getFnName x+>         getFnName x = MN ("Dunno: "++show x, 0)++Return whether a name is a recursive constructor (i.e, its family name+occurs anywhere in its arguments).++> recCon :: Name -> Gamma Name -> Bool+> recCon n gam = case glookup n gam of+>                  (Just (DCon _ t, Ind ty)) ->+>                      checkRec (conFamily ty) (map snd (getExpected ty))+>                  _ -> False+>    where conFamily t = fname (getFun (getReturnType t))+>          fname (TyCon n _) = n+>          fname _ = MN ("ERROR!",0)+>          checkRec n [] = False+>          checkRec n (x:xs) = nameOccurs n (forget x) || checkRec n xs++> insertGam :: Ord n => n -> Gval n -> Gamma n -> Gamma n+> insertGam nm val (Gam gam) = Gam $ Map.insert nm val gam++> concatGam :: Ord n => Gamma n -> Gamma n -> Gamma n+> concatGam (Gam x) (Gam y) = Gam (Map.union x y)++> setFrozen :: (Ord n, Eq n) => n -> Bool -> Gamma n -> Gamma n+> setFrozen n freeze (Gam xs) = Gam $ Map.mapWithKey sf xs where+>    sf p (G (Fun opts v) ty plicit)+>        | n == p = (G (Fun (doFreeze freeze opts) v) ty plicit)+>    sf _ x = x+>    doFreeze True opts = nub (Frozen:opts)+>    doFreeze False opts = opts \\ [Frozen]++> setRec :: (Ord n, Eq n) => n -> Bool -> Gamma n -> Gamma n+> setRec n frec (Gam xs) = Gam $ Map.mapWithKey sf xs where+>    sf p (G (Fun opts v) ty plicit)+>        | n == p = (G (Fun (doFrec frec opts) v) ty plicit)+>    sf _ x = x+>    doFrec True opts = nub (Recursive:opts)+>    doFrec False opts = opts \\ [Recursive]+++> freeze :: (Ord n, Eq n) => n -> Gamma n -> Gamma n+> freeze n gam = setFrozen n True gam++> thaw :: (Ord n, Eq n) => n -> Gamma n -> Gamma n+> thaw n gam = setFrozen n False gam++Remove a name from the middle of the context - should only be valid+if it's a partial definition or an axiom which is about to be replaced.++> remove :: (Ord n, Eq n) => n -> Gamma n -> Gamma n+> remove n (Gam xs) = Gam $ Map.delete n xs++Insert a name into the context. If the name is already there, this+is an error *unless* the old definition was 'Undefined', in which case+the name is replaced.++> gInsert :: (Monad m, Ord n, Eq n, Show n) => +>            n -> Gval n -> Gamma n -> m (Gamma n)+> gInsert nm val (Gam xs) = case Map.lookup nm xs of+>         -- FIXME: Check ty against val+>       Nothing -> return $ Gam (Map.insert nm val xs)+>       Just (G Undefined ty _) -> return $ Gam (Map.insert nm val xs)+>       Just (G (TCon _ NoConstructorsYet) ty _) -> +>                                  return $ Gam (Map.insert nm val xs)+>       Just _ -> fail $ "Name " ++ show nm ++ " is already defined"+++An ElimRule is a Haskell implementation of the iota reductions of+a family.++> type ElimRule = Spine Value -> Maybe Value++A PrimOp is an external operation++> type PrimOp = Spine Value -> Maybe Value+> type EvPrim = [TT Name] -> Maybe (TT Name) -- same, but with tt terms rather than values+++Model represents normal forms, including Ready (reducible) and Blocked+(non-reducible) forms.++> data Model s = MR (Ready s)+>              | MB (Blocked s, Model s) (Spine (Model s))++> data Ready s+>     = RdBind Name (Binder (Model s)) (s (Model s))+>     | RCon Int Name (Spine (Model s))+>     | RTyCon Name (Spine (Model s))+>     | forall c. Constant c => RdConst c+>     | RdStar+>     | RdLabel (Model s) (MComp s)+>     | RdCall (MComp s) (Model s)+>     | RdReturn (Model s)+>     | RdCode (Model s)+>     | RdQuote (Model s) -- (TT Name)+>     | RdInfer++> data Blocked s+>     = BCon Int Name Int+>     | BTyCon Name Int+>     | BElim ElimRule Name+>     | BPatDef (PMFun Name) Name+>     | BPrimOp PrimOp Name+>     | BRec Name Value+>     | BP Name+>     | BV Int+>     | BEval (Model s) (Model s)+>     | BEscape (Model s) (Model s)++> data MComp s = MComp Name [Model s]++> newtype Weakening = Wk Int++Second weakening is cached to prevent function composition in the weaken+class.++> newtype Kripke x = Kr (Weakening -> x -> x, Weakening)++> type Value = Model Kripke+> type Normal = Model Scope
Ivor/ViewTerm.lhs view
@@ -18,7 +18,7 @@ >                        Term(..), ViewTerm(..), Annot(..), apply, >                        view, viewType, ViewConst, typeof,  >                        freeIn, namesIn, occursIn, subst, getApp, ->                        Ivor.ViewTerm.getFnArgs,+>                        Ivor.ViewTerm.getFnArgs, transform, >                        getArgTypes, Ivor.ViewTerm.getReturnType, >                        dbgshow, >                        -- * Inductive types@@ -32,6 +32,9 @@  > import Data.Typeable > import Data.List+> import Data.Binary+> import Control.Monad+> import Debug.Trace  > name :: String -> Name > name = UN@@ -51,7 +54,7 @@ > -- is for.  > data NameType = Bound | Free | DataCon | TypeCon | ElimOp  >               | Unknown -- ^ Use for sending to typechecker.->   deriving Show+>   deriving (Show, Enum)  > -- | Construct a term representing a variable > mkVar :: String -- ^ Variable name@@ -81,6 +84,8 @@  > data Annot = FileLoc FilePath Int -- ^ source file, line number ++ > instance Eq ViewTerm where >     (==) (Name _ x) (Name _ y) = x == y >     (==) (Ivor.ViewTerm.App f a) (Ivor.ViewTerm.App f' a') = f == f' && a == a'@@ -102,6 +107,8 @@ >     (==) (Ivor.ViewTerm.Eval t) (Ivor.ViewTerm.Eval t') = t==t' >     (==) (Ivor.ViewTerm.Escape t) (Ivor.ViewTerm.Escape t') = t==t' >     (==) (Annotation _ t) (Annotation _ t') = t == t'+>     (==) (Annotation _ t) t' = t == t'+>     (==) t (Annotation _ t') = t == t' >     (==) _ _ = False  > -- | Haskell types which can be used as constants@@ -203,6 +210,7 @@ >         = Ivor.ViewTerm.Eval (vtaux ctxt tm) >     vtaux ctxt (Stage (TTCore.Escape tm _))  >         = Ivor.ViewTerm.Escape (vtaux ctxt tm)+>     vtaux ctxt (Meta n _) = Metavar n >     vtaux _ t = error $ "Can't happen vtaux " ++ debugTT t  > -- | Return whether the name occurs free in the term.@@ -295,15 +303,17 @@ > -- | Match the second argument against the first, returning a list of > -- the names in the first paired with their matches in the second. Returns > -- Nothing if there is a match failure. There is no searching under binders.-> match :: ViewTerm -> ViewTerm -> Maybe [(Name, ViewTerm)]-> match t1 t2 = do acc <- m' t1 t2 []->                  checkDups acc [] where->   m' (Name _ n) t acc = return ((n,t):acc)+> matchMeta :: ViewTerm -> ViewTerm -> Maybe [(Name, ViewTerm)]+> matchMeta t1 t2 = do acc <- m' t1 t2 []+>                      checkDups acc [] where+>   m' (Metavar n) t acc = return ((n,t):acc)+>   m' Placeholder t acc = return acc >   m' (Ivor.ViewTerm.App f a) (Ivor.ViewTerm.App f' a') acc  >       = do acc' <- m' f f' acc >            m' a a' acc' >   m' (Annotation _ t) t' acc = m' t t' acc >   m' t (Annotation _ t') acc = m' t t' acc+>   m' (Name _ x) (Name _ y) acc | x == y = return acc >   m' x y acc | x == y = return acc >              | otherwise = fail $"Mismatch " ++ show x ++ " and " ++ show y @@ -314,6 +324,16 @@ >                                else fail $ "Mismatch on " ++ show x >          Nothing -> checkDups xs ((x,t):acc) +> replaceMeta :: [(Name, ViewTerm)] -> ViewTerm -> ViewTerm+> replaceMeta ms (Metavar n) = case lookup n ms of+>                                Just t -> t+>                                _ -> Metavar n+> replaceMeta ms (Ivor.ViewTerm.App f a)+>             = Ivor.ViewTerm.App (replaceMeta ms f) (replaceMeta ms a)+> replaceMeta ms (Annotation a t) = Annotation a (replaceMeta ms t)+> replaceMeta ms x = x++ > -- |Substitute a name n with a value v in a term f  > subst :: Name -> ViewTerm -> ViewTerm -> ViewTerm > subst n v nm@(Name _ p) | p == n = v@@ -346,3 +366,43 @@ > subst n v (Annotation a t) = Annotation a (subst n v t) > subst n v t = t +> -- |Transform a term according to a rewrite rule.+> transform :: ViewTerm -- ^ Left hand side, with metavariables+>           -> ViewTerm -- ^ Right hand side, with metavariables+>           -> ViewTerm -- ^ Term to rewrite+>           -> ViewTerm+> transform lhs rhs term = tr' term where+>     tr' (Ivor.ViewTerm.App f a) +>             = doTr $ Ivor.ViewTerm.App (tr' f) (tr' a)+>     tr' (Ivor.ViewTerm.Lambda v t sc) +>             = doTr $ Ivor.ViewTerm.Lambda v (tr' t) (tr' sc)+>     tr' (Ivor.ViewTerm.Forall v t sc) +>             = doTr $ Ivor.ViewTerm.Forall v (tr' t) (tr' sc)+>     tr' (Ivor.ViewTerm.Let v t val sc) +>             = doTr $ Ivor.ViewTerm.Let v (tr' t) (tr' val) (tr' sc)+>     tr' (Annotation a t) = doTr $ Annotation a (tr' t)+>     tr' x = doTr x++>     doTr x = case matchMeta lhs x of+>                 Just vars -> replaceMeta vars rhs+>                 Nothing -> x++> instance Binary Name where+>     put (UN s) = do put (0 :: Word8); put s+>     put (MN s) = do put (1 :: Word8); put s++>     get = do tag <- getWord8+>              case tag of+>                0 -> liftM UN get+>                1 -> liftM MN get++> instance Binary NameType where+>     put x = put (fromEnum x)+>     get = do t <- get+>              return (toEnum t)++> instance Binary Annot where+>     put (FileLoc p i) = do put p; put i+>     get = do p <- get+>              i <- get+>              return (FileLoc p i)
ivor.cabal view
@@ -1,5 +1,5 @@ Name:		ivor-Version:	0.1.9+Version:	0.1.10 Author:		Edwin Brady License:	BSD3 License-file:	LICENSE@@ -58,7 +58,7 @@   -Build-depends:  base >=3 && <5, parsec, mtl, directory+Build-depends:  base >=3 && <5, parsec, mtl, directory, binary Build-type:     Simple  Extensions:     MultiParamTypeClasses, FunctionalDependencies,@@ -72,7 +72,7 @@ 		Ivor.Plugin, Ivor.Construction Other-modules:	Ivor.Nobby, Ivor.TTCore, Ivor.State, 		Ivor.Tactics, Ivor.Typecheck, Ivor.Evaluator-		Ivor.Gadgets, Ivor.SC, Ivor.Bytecode,+		Ivor.Gadgets, Ivor.SC, Ivor.Bytecode, Ivor.Values, 		Ivor.CodegenC, Ivor.Datatype, Ivor.Display, 		Ivor.ICompile, Ivor.MakeData, Ivor.Unify, 		Ivor.Grouper, Ivor.ShellParser, Ivor.Constant,