ivor 0.1.11 → 0.1.12
raw patch · 16 files changed
+143/−40 lines, 16 files
Files
- Ivor/Datatype.lhs +2/−2
- Ivor/Errors.lhs +1/−0
- Ivor/Evaluator.lhs +10/−1
- Ivor/Nobby.lhs +6/−0
- Ivor/Overloading.lhs +35/−0
- Ivor/PatternDefs.lhs +13/−6
- Ivor/Prefix.hs +0/−1
- Ivor/Shell.lhs +3/−2
- Ivor/TT.lhs +9/−0
- Ivor/TTCore.lhs +8/−0
- Ivor/Tactics.lhs +21/−7
- Ivor/Typecheck.lhs +13/−7
- Ivor/Unify.lhs +9/−7
- Ivor/Values.lhs +1/−0
- Ivor/ViewTerm.lhs +2/−0
- ivor.cabal +10/−7
Ivor/Datatype.lhs view
@@ -63,8 +63,8 @@ > (ev, _) <- typecheck gamma'' erty > (cv, _) <- typecheck gamma'' crty > -- let gamma''' = extend gamma'' (er,G (ElimRule dummyRule) ev defplicit)-> ([(_, esch, _)], _, _) <- checkDef gamma'' er erty eschemes False False-> ([(_, csch, _)], _, _) <- checkDef gamma'' cr crty cschemes False False+> ([(_, esch, _)], _, _) <- checkDef gamma'' er erty eschemes False False Nothing+> ([(_, csch, _)], _, _) <- checkDef gamma'' cr crty cschemes False False Nothing > return (Data (ty,G (TCon (arity gamma kv) erdata) kv defplicit) consv numps > (er,ev) (cr,cv) (Just esch) (Just csch) eschemes cschemes)
Ivor/Errors.lhs view
@@ -12,6 +12,7 @@ > | INoSuchVar Name > | ICantInfer Name (Indexed Name) > | IContext String IError+> | IAmbiguousName [Name] > deriving (Show, Eq) > instance Error IError where
Ivor/Evaluator.lhs view
@@ -1,6 +1,7 @@ > {-# OPTIONS_GHC -fglasgow-exts #-} -> module Ivor.Evaluator(eval_whnf, eval_nf, eval_nf_without, eval_nf_limit,+> module Ivor.Evaluator(eval_whnf, eval_nf, eval_nf_env,+> eval_nf_without, eval_nf_limit, > eval_nfEnv, tidyNames) where > import Ivor.TTCore@@ -25,6 +26,14 @@ > eval_nf :: Gamma Name -> Indexed Name -> Indexed Name > eval_nf gam (Ind tm) = let res = makePs (evaluate True gam tm Nothing Nothing) > in finalise (Ind res)++> eval_nf_env :: Env Name -> Gamma Name -> Indexed Name -> Indexed Name+> eval_nf_env 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 > eval_nf_without :: Gamma Name -> Indexed Name -> [Name] -> Indexed Name > eval_nf_without gam tm [] = eval_nf gam tm
Ivor/Nobby.lhs view
@@ -70,6 +70,8 @@ > eval stage gamma g (Con tag n i) = (MB (BCon tag n i, pty n) Empty) > eval stage gamma g (TyCon n 0) = (MR (RTyCon n Empty)) > eval stage gamma g (TyCon n i) = (MB (BTyCon n i, pty n) Empty)+> eval stage gamma g (Meta n ty) = (MB (BMeta n bty, bty) Empty)+> where bty = eval stage gamma g ty > eval stage gamma g (Const x) = (MR (RdConst x)) > eval stage gamma g Star = MR RdStar > eval stage gamma (VG g) (Bind n (B Lambda ty) (Sc sc)) =@@ -99,6 +101,7 @@ > getelim y = error $ show n ++ > " is not an elimination rule. Something went wrong." ++ show y > eval stage gamma g (Stage s) = evalStage stage gamma g s+> eval stage gamma g x = error $ "eval, can't happen: " ++ show x > evalcomp stage gamma g (Comp n ts) = MComp n (map (eval stage gamma g) ts) @@ -261,6 +264,7 @@ > weakenp i (BPatDef p n) = BPatDef p n > weakenp i (BRec n v) = BRec n v > weakenp i (BPrimOp e n) = BPrimOp e n+> weakenp i (BMeta n ty) = BMeta n (weakenp i ty) > weakenp i (BP n) = BP n > weakenp i (BV j) = BV (weakenp i j) > weakenp i (BEval t ty) = BEval (weakenp i t) (weakenp i ty)@@ -309,6 +313,7 @@ > instance Quote (Blocked Kripke) (Blocked Scope) where > quote' ns (BCon t n j) = BCon t n j > quote' ns (BTyCon n j) = BTyCon n j+> quote' ns (BMeta n t) = BMeta n (quote' ns t) > quote' ns (BElim e n) = BElim e n > quote' ns (BPatDef p n) = BPatDef p n > quote' ns (BRec n v) = BRec n v@@ -372,6 +377,7 @@ > forget (BPatDef p n) = P n > forget (BRec n v) = P n > forget (BPrimOp f n) = P n+> forget (BMeta n t) = Meta n (forget t) > forget (BP n) = P n > forget (BV i) = V i > forget (BEval t ty) = Stage (Eval (forget t) (forget ty))
+ Ivor/Overloading.lhs view
@@ -0,0 +1,35 @@+Facilities for handling overloading. This is currently a bodge - terms+contain 'ROpts' which are variables which could be one of several things.+We convert such terms to a list of terms which contain all the possible +combinations of 'Var', typecheck them all, and if only one succeeds, that's+the right overloading. If more than one succeeds, there is an ambiguous name.++> module Ivor.Overloading where++> import Ivor.TTCore++> getTerms :: Raw -> [Raw]+> getTerms (Var n) = return $ Var n+> getTerms (ROpts ns) = do n <- ns+> return $ Var n+> getTerms (RApp f a) = do f' <- getTerms f+> a' <- getTerms a+> return $ RApp f' a'+> getTerms (RBind n (B b t) sc)+> = do b' <- gtb b+> t' <- getTerms t+> sc' <- getTerms sc+> return $ RBind n (B b' t') sc'+> where gtb Lambda = return Lambda+> gtb Pi = return Pi+> gtb (Let t) = do t' <- getTerms t+> return $ Let t'+> gtb Hole = return Hole+> gtb (Guess t) = do t' <- getTerms t+> return $ Guess t'+> gtb (Pattern t) = do t' <- getTerms t+> return $ Guess t'+> gtb MatchAny = return MatchAny+> getTerms (RFileLoc f l t) = do t' <- getTerms t+> return (RFileLoc f l t')+> getTerms t = return t
Ivor/PatternDefs.lhs view
@@ -9,6 +9,7 @@ > import Ivor.Unify > import Ivor.Errors > import Ivor.Values+> import Ivor.Evaluator > import Debug.Trace > import Data.List@@ -24,8 +25,9 @@ > checkDef :: Gamma Name -> Name -> Raw -> [PMRaw] -> > Bool -> -- Check for coverage > Bool -> -- Check for well-foundedness+> Maybe [(Name, Int)] -> -- Names to specialise > IvorM ([(Name, PMFun Name, Indexed Name)], [(Name, Indexed Name)], Bool)-> checkDef gam fn tyin pats cover wellfounded = do+> checkDef gam fn tyin pats cover wellfounded spec = do > --x <- expandCon gam (mkapp (Var (UN "S")) [mkapp (Var (UN "S")) [Var (UN "x")]]) > --x <- expandCon gam (mkapp (Var (UN "vcons")) [RInfer,RInfer,RInfer,mkapp (Var (UN "vnil")) [Var (UN "foo")]]) > clausesIn <- mapM (expandClause gam) pats@@ -37,7 +39,7 @@ > checkNotExists fn gam > gam' <- gInsert fn (G Undefined ty defplicit) gam > clauses' <- validClauses gam' fn ty clauses'-> (pmdefs, newdefs, covers) <- matchClauses gam' fn pats tyin ty cover clauses'+> (pmdefs, newdefs, covers) <- matchClauses gam' fn pats tyin ty cover clauses' spec > wf <- return True > {- if wellfounded then > do checkWellFounded gam fn [0..arity-1] pmdef@@ -175,13 +177,14 @@ Match up the inferred arguments to the names (so getting the types of the names bound in patterns) then type check the right hand side. -Each clause may generate auxiliary definitions, so return all definitons created.+Each clause may generate auxiliary definitions, so return all definitions created. > matchClauses :: Gamma Name -> Name -> [PMRaw] -> Raw -> Indexed Name -> > Bool -> -- Check coverage > [(Indexed Name, Indexed Name)] -> +> Maybe [(Name, Int)] -> > IvorM ([(Name, PMFun Name, Indexed Name)], [(Name, Indexed Name)], Bool)-> matchClauses gam fn pats tyin ty@(Ind ty') cover gen = do+> matchClauses gam fn pats tyin ty@(Ind ty') cover gen spec = do > let raws = zip (map mkRaw pats) (map getRet pats) > (checkpats, newdefs, aux, covers) <- mytypechecks gam raws [] [] [] True > cv <- if cover then @@ -217,7 +220,11 @@ > let namesbound = getNames (Sc tmtt) > checkAllBound (fileLine ret) namesret namesbound (Ind rtmtt') tmtt rty pty > -- trace (show env) $-> return ((tm, Ind rtmtt', env), [], newdefs, True)+> let specrtm = case spec of+> Nothing -> Ind rtmtt'+> Just [] -> eval_nf gam (Ind rtmtt')+> Just ns -> eval_nf_limit gam (Ind rtmtt') ns+> return ((tm, specrtm, 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@@ -244,7 +251,7 @@ > let gam' = insertGam newname (G Undefined newfnTy 0) gam > 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+> (auxdefs', newdefs, covers) <- checkDef gam' newname (forget newfnTy) newpdef False cover spec > return (chk, auxdefs++auxdefs', newdefs, covers) > addLastArg (RBind n (B Pi arg) x) ty scr addprf
− Ivor/Prefix.hs
@@ -1,1 +0,0 @@-module Ivor.Prefix where prefix = "/Users/edwin"
Ivor/Shell.lhs view
@@ -26,13 +26,14 @@ > import Ivor.Equality > import Ivor.Gadgets > import Ivor.Primitives-> import qualified Ivor.Prefix > import Ivor.Plugin+> import Paths_ivor > import System.Exit > import System.Environment > import System.Directory > import System.IO+> import System.IO.Unsafe > import Data.Char > import Debug.Trace @@ -388,7 +389,7 @@ > -- | Get the install prefix of the library > prefix :: FilePath-> prefix = Ivor.Prefix.prefix+> prefix = unsafePerformIO getDataDir -- Yes, yes, I know. If the given file is already loaded, do nothing.
Ivor/TT.lhs view
@@ -189,6 +189,7 @@ > | NoSuchVar Name > | CantInfer Name ViewTerm > | ErrContext String TTError+> | AmbiguousName [Name] > instance Show TTError where > show (CantUnify t1 t2) = "Can't unify " ++ show t1 ++ " and " ++ show t2@@ -199,6 +200,7 @@ > " = " ++ 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 (AmbiguousName ns) = "Ambiguous name " ++ show ns > show (ErrContext c err) = c ++ show err > instance Error TTError where@@ -226,6 +228,7 @@ > names > getError (ICantInfer nm tm) = CantInfer nm (view (Term (tm, Ind TTCore.Star))) > getError (INoSuchVar n) = NoSuchVar n+> getError (IAmbiguousName ns) = AmbiguousName ns > getError (IContext s e) = ErrContext s (getError e) > -- | Quickly convert a 'ViewTerm' into a real 'Term'.@@ -308,6 +311,7 @@ > data PattOpt = Partial -- ^ No need to cover all cases > | GenRec -- ^ No termination checking > | Holey -- ^ Allow metavariables in the definition, which will become theorems which need to be proved.+> | Specialise [(Name, Int)] -- ^ Specialise the right hand side > deriving Eq > -- |Add a new definition to the global state.@@ -329,6 +333,7 @@ > <- tt $ checkDef ndefs n inty (map mkRawClause clauses) > (not (elem Ivor.TT.Partial opts)) > (not (elem GenRec opts))+> (getSpec opts) > (ndefs',vnewnames) > <- if (null newnames) then return (ndefs, []) > else do when (not (Holey `elem` opts)) $ @@ -346,6 +351,10 @@ > 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.++> getSpec [] = Nothing+> getSpec (Specialise fns:_) = Just fns+> getSpec (_:xs) = getSpec xs > -- |Add a new definition, with its type to the global state. > -- These definitions can be recursive, so use with care.
Ivor/TTCore.lhs view
@@ -17,6 +17,7 @@ > data Raw > = Var Name+> | ROpts [Name] > | RApp Raw Raw > | RBind Name (Binder Raw) Raw > | forall c.(Constant c) => RConst !c@@ -676,6 +677,12 @@ > (==) (Elim x) (Elim y) = x==y > (==) (App f a) (App f' a') = f==f' && a==a' > (==) (Bind _ b sc) (Bind _ b' sc') = b==b' && sc==sc'++Eta equality:++> (==) (Bind x (B Lambda ty) (Sc (App t (V 0)))) t' = t == t'+> (==) t' (Bind x (B Lambda ty) (Sc (App t (V 0)))) = t == t'+ > (==) (Proj _ i x) (Proj _ j y) = i==j && x==y > (==) (Const x) (Const y) = case cast x of > Just x' -> x'==y@@ -708,6 +715,7 @@ > forget x = fPrec 10 x where > fPrec :: Int -> Raw -> String > fPrec _ (Var n) = forget n+> fPrec _ (ROpts n) = show n > fPrec x (RApp f a) = bracket x 1 $ fPrec 1 f ++ " " ++ fPrec 0 a > fPrec x (RBind n (B Lambda t) sc) = bracket x 2 $ > "["++forget n ++":"++fPrec 10 t++"]" ++ fPrec 10 sc
Ivor/Tactics.lhs view
@@ -3,6 +3,7 @@ > import Ivor.TTCore > import Ivor.Typecheck > import Ivor.Nobby+> import Ivor.Evaluator > import Ivor.Gadgets > import Ivor.Unify > import Ivor.Errors@@ -263,19 +264,32 @@ > let (Ind nty) = normaliseEnv (ptovenv env) gam (Ind ntyin) > let bvin = makePsEnv (map fst env) bv > -- let (Just (Ind nty)) = lookuptype n gam++Get the names and types of the arguments to be passed to the thing +we're refining by.+ > let claimTypes = getClaims (makePsEnv (map fst env) nty) > let rawapp = mkapp rtm (map (\_ -> RInfer) claimTypes)++Normalise the goal.+ > let (Ind tyin') = finalise (normaliseEnv (ptovenv env) gam (Ind ty))++Type check the application we've just built, with the placeholders, some of +which may have been solved.+ > (Ind rtch, rtych, ev) <- checkAndBind gam (ptovenv env) rawapp (Just (Ind tyin'))-> let argguesses = getArgs rtch-> -- So we'll have an application, some of the arguments with inferred-> -- names. Let's record which ones...+> let argguesses = -- trace (show rawapp ++ "\n" ++ show tyin' ++ "\n" ++ show rtch ++ "\n" ++ show rtych ++ "\nNew env: " ++ show ev) $ +> getArgs rtch++So we'll have an application, some of the arguments with inferred+names. Let's record which ones...+ > let claims = uniqifyClaims x env claimTypes > let claimGuesses = zip claims (map appVar argguesses)-> (tm',_) <- {- trace (show claimGuesses) $ -} doClaims x claimGuesses gam env tm+> (tm',_) <- doClaims x claimGuesses gam env tm > let guess = (mkGuess claimGuesses [] (forget bvin))-> (filled, unified) <- runtacticEnv gam env x tm'-> (fill guess)+> (filled, unified) <- runtacticEnv gam env x tm' (fill guess) > -- (filled, solved) <- solveUnified [] unified filled > -- filled <- tryDefaults defaults claims filled > -- (tm', _) <- trace (show claims) $ tidy gam env filled@@ -386,7 +400,7 @@ > evalGoal :: Tactic > evalGoal gam env (Ind (Bind x (B Hole ty) sc)) =-> do let (Ind nty) = normaliseEnv (ptovenv env) gam (finalise (Ind ty))+> do let (Ind nty) = eval_nf_env (ptovenv env) gam (finalise (Ind ty)) > tacret $ Ind (Bind x (B Hole nty) sc) > evalGoal _ _ (Ind (Bind x _ _)) = fail $ "evalGoal: " ++ show x ++ " Not a hole" > evalGoal _ _ _ = fail "evalGoal: Can't happen"
Ivor/Typecheck.lhs view
@@ -14,6 +14,7 @@ > import Ivor.Errors > import Ivor.Evaluator > import Ivor.Values+> import Ivor.Overloading > import Control.Monad.State > import Data.List@@ -112,13 +113,13 @@ > Indexed Name -> Indexed Name -> > IvorM (Indexed Name, Indexed Name) > doConversion raw gam constraints (Ind tm) (Ind ty) =-> -- trace ("Finishing checking " ++ show tm ++ " with " ++ show (length constraints) ++ " equations") $ +> -- trace ("Finishing checking " ++ show tm ++ " with " ++ show (length constraints) ++ " equations\n" ++ showeqn (map (\x -> (True,x)) constraints)) $ > -- Unify twice; first time collect the substitutions, second > -- time do them. Because we don't know what order we can solve > -- constraints in and they might depend on each other... > do let cs = nub constraints > (subst, nms) <- mkSubst $ (map (\x -> (True,x)) cs) ++-> (map (\x -> (False,x)) (reverse cs))+> (map (\x -> (False,x)) cs) > let tm' = papp subst tm > let ty' = papp subst ty > return (Ind tm',Ind ty')@@ -139,7 +140,7 @@ > let x' = papp s' x > 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+> Right uns -> return uns > Left err -> {- trace (showeqn all) $ -} > ifail (errCtxt fc (ICantUnify (Ind y') (Ind x'))) @@ -178,6 +179,7 @@ > IvorM (Indexed Name, Indexed Name, Env Name) > checkAndBind gam env tm mty = do > ((v,t), (next,inf,e,convs,_,_)) <- lvlcheck 0 True 0 gam env tm mty+> e <- convertAllEnv gam convs e > (v'@(Ind vtm),t') <- doConversion tm gam convs v t -- (normalise gam t1') > return (v',t',e) @@ -303,7 +305,8 @@ > Maybe (Indexed Name) -> > IvorM ((Indexed Name, Indexed Name), CheckState) > lvlcheck lvl infer next gamma env tm exp -> = do runStateT (tcfixupTop env lvl tm exp) (next, infer, [], [], [], Nothing) +> = -- let tms = getTerms tm in+> runStateT (tcfixupTop env lvl tm exp) (next, infer, [], [], [], Nothing) > where Do the typechecking, then unify all the inferred terms.@@ -378,6 +381,8 @@ > else lift $ ifail (errCtxt fc (INoSuchVar n)) > Just (B Pi t) -> return (Ind (P n), Ind t) +> tc env lvl (ROpts ns) Nothing = fail $ "Need a type for overloaded names"+> tc env lvl (ROpts ns) (Just exp) = fail $ "Overloading not implemented (" ++ show ns ++ " : " ++ show exp ++ ")" > tc env lvl (RApp f a) exp = do > (Ind fv, Ind ft) <- tcfixup env lvl f Nothing > let fnfng = normaliseEnv env emptyGam (Ind ft)@@ -398,11 +403,12 @@ > let tt' = (normaliseEnv env gamma (Ind tt)) > return (Ind (App fv av), (normaliseEnv env gamma (Ind tt))) > _ -> fail $ "Cannot apply a non function type " ++ show ft ++ " to " ++ show a-> return (rv,rt)+> -- return (rv,rt) > case exp of > Nothing -> return (rv,rt)-> Just expt -> do checkConvSt env gamma rt expt-> return (rv,rt)+> Just expt -> -- trace ("Checking " ++ show (rv, rt, expt)) $+> do checkConvSt env gamma rt expt+> return (rv,rt) > tc env lvl (RConst x) _ = lift $ tcConst x > tc env lvl RStar _ = return (Ind Star, Ind Star) > tc env lvl (RFileLoc f l t) exp =
Ivor/Unify.lhs view
@@ -42,8 +42,8 @@ > {- trace (show (x,y) ++ "\n" ++ > show (p (normalise (gam' gam) x)) ++ "\n" ++ > show (p (normalise (gam' gam) x))) $-}-> case unifynferr i env (p x)-> (p y) of+> case unifynferr False env (p x)+> (p y) of > (Right x) -> return x > _ -> {- trace (dbgtt x ++ ", " ++ dbgtt y ++"\n") $ -}@@ -115,11 +115,13 @@ > else ifail $ ICantUnify (Ind x) (Ind y) > where funify (P x) (P y) > | x==y = True-> | otherwise = hole envl x || hole envl y-> funify (Con _ _ _) (P x) = hole envr x-> funify (P x) (Con _ _ _) = hole envl x-> funify (TyCon _ _) (P x) = hole envr x-> funify (P x) (TyCon _ _) = hole envl x+> | otherwise = False -- hole envl x || hole envl y+> funify (Con _ _ _) (P x) = False -- hole envr x+> funify (P x) (Con _ _ _) = False -- hole envl x+> funify (TyCon _ _) (P x) = False -- hole envr x+> funify (P x) (TyCon _ _) = False -- hole envl x+> funify (P x) (App _ _) = False+> funify (App _ _) (P x) = False > funify _ _ = True -- unify normally > un envl envr (Proj _ i t) (Proj _ i' t') acc > | i == i' = un envl envr t t' acc
Ivor/Values.lhs view
@@ -195,6 +195,7 @@ > | BPrimOp PrimOp Name > | BRec Name Value > | BP Name+> | BMeta Name (Model s) > | BV Int > | BEval (Model s) (Model s) > | BEscape (Model s) (Model s)
Ivor/ViewTerm.lhs view
@@ -63,6 +63,7 @@ > data ViewTerm > = Name { nametype :: NameType, var :: Name }+> | Overloaded { vars :: [Name] } -- ^ on input only, list of possible names, to be resolved to one by the type checker. > | App { fun :: ViewTerm, arg :: ViewTerm } > | Lambda { var :: Name, vartype :: ViewTerm, scope :: ViewTerm } > | Forall { var :: Name, vartype :: ViewTerm, scope :: ViewTerm }@@ -131,6 +132,7 @@ > constructors :: [(Name,ViewTerm)] } > instance Forget ViewTerm Raw where+> forget (Overloaded vs) = ROpts vs > forget (Ivor.ViewTerm.App f a) = RApp (forget f) (forget a) > forget (Ivor.ViewTerm.Lambda v ty sc) = RBind v > (B TTCore.Lambda (forget ty))
ivor.cabal view
@@ -1,5 +1,5 @@ Name: ivor-Version: 0.1.11+Version: 0.1.12 Author: Edwin Brady License: BSD3 License-file: LICENSE@@ -45,16 +45,17 @@ papers/ivor/ivor.tex, papers/ivor/corett.tex, papers/ivor/conclusions.tex, papers/ivor/intro.tex, papers/ivor/llncs.cls, papers/ivor/tactics.tex, papers/ivor/library.ltx, papers/ivor/dtp.bib, papers/ivor/alink.bib,- papers/ivor/Makefile, papers/ivor/embounded.bib+ papers/ivor/Makefile, papers/ivor/embounded.bib,+ lib/nat.tt, lib/lt.tt, lib/list.tt, lib/eq.tt,+ lib/basics.tt, lib/logic.tt, lib/vect.tt, lib/fin.tt+ Extra-source-files: emacs/ivor-mode.el, examplett/staged.tt, examplett/test.c, examplett/partial.tt, examplett/nat.tt, examplett/vec.tt, examplett/lt.tt, examplett/Test.hs, examplett/plus.tt, examplett/jmeq.tt, examplett/eq.tt, examplett/logic.tt, examplett/interp.tt, examplett/stageplus.tt, examplett/Nat.hs, examplett/general.tt, examplett/natsimpl.tt, examplett/test.tt, examplett/vect.tt, examplett/fin.tt, examplett/ack.tt,- IOvor/IOPrims.lhs, IOvor/Main.lhs, IOvor/iobasics.tt, Jones/Main.lhs,- lib/nat.tt, lib/lt.tt, lib/list.tt, lib/eq.tt,- lib/basics.tt, lib/logic.tt, lib/vect.tt, lib/fin.tt+ IOvor/IOPrims.lhs, IOvor/Main.lhs, IOvor/iobasics.tt, Jones/Main.lhs @@ -77,5 +78,7 @@ Ivor.CodegenC, Ivor.Datatype, Ivor.Display, Ivor.ICompile, Ivor.MakeData, Ivor.Unify, Ivor.Grouper, Ivor.ShellParser, Ivor.Constant,- Ivor.RunTT, Ivor.Compiler, Ivor.Prefix, Ivor.Errors,- Ivor.PatternDefs, Ivor.ShellState, Ivor.Scopecheck+ Ivor.RunTT, Ivor.Compiler, Ivor.Errors,+ Ivor.PatternDefs, Ivor.ShellState, Ivor.Scopecheck,+ Ivor.Overloading,+ Paths_ivor