git.iko.soy/Idris-dev
on master help sign in
Shift core TT into a separate directory (for ease of reuse)
0ae24f1Edwin Brady
miniidris.cabal+3−3
compare with master
unifiedsplit
@@ -17,9 +17,9 @@ Build-type: Simple
17Executable miniidris
17Executable miniidris
18 Main-is: Main.hs
18 Main-is: Main.hs
19 hs-source-dirs: src
19 hs-source-dirs: src
20− Other-modules: Core, Evaluate, Typecheck, ProofState,
20+ Other-modules: Core.Core, Core.Evaluate, Core.Typecheck,
21− ProofState, CoreParser, ShellParser,
21+ Core.ProofShell, Core.ProofState, Core.CoreParser,
22− Unify, Elaborate
22+ Core.ShellParser, Core.Unify, Core.Elaborate
23
23
24 Build-depends: base>=4 && <5, parsec, mtl, Cabal, readline,
24 Build-depends: base>=4 && <5, parsec, mtl, Cabal, readline,
25 containers
25 containers
src/Core.hs → src/Core/Core.hsrenamed+1−1
@@ -1,6 +1,6 @@
1{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveFunctor #-}
1{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveFunctor #-}
2
2
3−module Core where
3+module Core.Core where
4
4
5import Control.Monad.State
5import Control.Monad.State
6import Debug.Trace
6import Debug.Trace
src/CoreParser.hs → src/Core/CoreParser.hsrenamed+2−2
@@ -1,8 +1,8 @@
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
2
2
3−module CoreParser(parseTerm, parseFile, parseDef, pTerm, iName) where
3+module Core.CoreParser(parseTerm, parseFile, parseDef, pTerm, iName) where
4
4
5−import Core
5+import Core.Core
6
6
7import Text.ParserCombinators.Parsec
7import Text.ParserCombinators.Parsec
8import Text.ParserCombinators.Parsec.Expr
8import Text.ParserCombinators.Parsec.Expr
src/Elaborate.hs → src/Core/Elaborate.hsrenamed+6−5
@@ -8,12 +8,13 @@
8 tactics out of the primitives.
8 tactics out of the primitives.
9-}
9-}
10
10
11−module Elaborate(module Elaborate, module ProofState) where
11+module Core.Elaborate(module Core.Elaborate,
12+ module Core.ProofState) where
12
13
13−import ProofState
14+import Core.ProofState
14−import Core
15+import Core.Core
15−import Evaluate
16+import Core.Evaluate
16−import Typecheck
17+import Core.Typecheck
17
18
18import Control.Monad.State
19import Control.Monad.State
19import Data.Char
20import Data.Char
src/Evaluate.hs → src/Core/Evaluate.hsrenamed+2−2
@@ -1,13 +1,13 @@
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
2
2
3−module Evaluate(normalise,
3+module Core.Evaluate(normalise,
4 Fun(..), Def(..), Context, toAlist,
4 Fun(..), Def(..), Context, toAlist,
5 emptyContext, addToCtxt, addConstant, addDatatype,
5 emptyContext, addToCtxt, addConstant, addDatatype,
6 lookupTy, lookupP, lookupDef, lookupVal, lookupTyEnv) where
6 lookupTy, lookupP, lookupDef, lookupVal, lookupTyEnv) where
7
7
8import qualified Data.Map as Map
8import qualified Data.Map as Map
9import Debug.Trace
9import Debug.Trace
10−import Core
10+import Core.Core
11
11
12-- VALUES (as HOAS) ---------------------------------------------------------
12-- VALUES (as HOAS) ---------------------------------------------------------
13
13
src/ProofShell.hs → src/Core/ProofShell.hsrenamed+6−6
@@ -1,12 +1,12 @@
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
2
2
3−module ProofShell where
3+module Core.ProofShell where
4
4
5−import Typecheck
5+import Core.Typecheck
6−import Evaluate
6+import Core.Evaluate
7−import Core
7+import Core.Core
8−import ShellParser
8+import Core.ShellParser
9−import Elaborate
9+import Core.Elaborate
10
10
11import Control.Monad.State
11import Control.Monad.State
12import System.Console.Readline
12import System.Console.Readline
src/ProofState.hs → src/Core/ProofState.hsrenamed+5−5
@@ -4,13 +4,13 @@
4 proofs, and some high level commands for introducing new theorems,
4 proofs, and some high level commands for introducing new theorems,
5 evaluation/checking inside the proof system, etc. --}
5 evaluation/checking inside the proof system, etc. --}
6
6
7−module ProofState(ProofState(..), newProof, envAtFocus, goalAtFocus,
7+module Core.ProofState(ProofState(..), newProof, envAtFocus, goalAtFocus,
8 Tactic(..), processTactic) where
8 Tactic(..), processTactic) where
9
9
10−import Typecheck
10+import Core.Typecheck
11−import Evaluate
11+import Core.Evaluate
12−import Core
12+import Core.Core
13−import Unify
13+import Core.Unify
14
14
15import Control.Monad.State
15import Control.Monad.State
16import Control.Applicative
16import Control.Applicative
src/ShellParser.hs → src/Core/ShellParser.hsrenamed+4−4
@@ -1,10 +1,10 @@
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
2
2
3−module ShellParser(parseCommand, parseTactic) where
3+module Core.ShellParser(parseCommand, parseTactic) where
4
4
5−import Core
5+import Core.Core
6−import Elaborate
6+import Core.Elaborate
7−import CoreParser
7+import Core.CoreParser
8
8
9import Text.ParserCombinators.Parsec
9import Text.ParserCombinators.Parsec
10import Text.ParserCombinators.Parsec.Expr
10import Text.ParserCombinators.Parsec.Expr
src/Test.hs → src/Core/Test.hsrenamed

The content is the same.

src/Typecheck.hs → src/Core/Typecheck.hsrenamed+3−3
@@ -1,12 +1,12 @@
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor #-}
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor #-}
2
2
3−module Typecheck where
3+module Core.Typecheck where
4
4
5import Control.Monad.State
5import Control.Monad.State
6import Debug.Trace
6import Debug.Trace
7
7
8−import Core
8+import Core.Core
9−import Evaluate
9+import Core.Evaluate
10
10
11-- To check conversion, normalise each term wrt the current environment.
11-- To check conversion, normalise each term wrt the current environment.
12-- Since we haven't converted everything to de Bruijn indices yet, we'll have to
12-- Since we haven't converted everything to de Bruijn indices yet, we'll have to
src/Unify.hs → src/Core/Unify.hsrenamed+3−3
@@ -1,9 +1,9 @@
1{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveFunctor #-}
1{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveFunctor #-}
2
2
3−module Unify(unify) where
3+module Core.Unify(unify) where
4
4
5−import Core
5+import Core.Core
6−import Evaluate
6+import Core.Evaluate
7
7
8import Control.Monad
8import Control.Monad
9
9
src/Main.hs+6−6
@@ -1,11 +1,11 @@
1module Main where
1module Main where
2
2
3−import CoreParser
3+import Core.CoreParser
4−import ShellParser
4+import Core.ShellParser
5−import Core
5+import Core.Core
6−import Typecheck
6+import Core.Typecheck
7−import ProofShell
7+import Core.ProofShell
8−import Evaluate
8+import Core.Evaluate
9
9
10main = do f <- readFile "test.mi"
10main = do f <- readFile "test.mi"
11 case parseFile f of
11 case parseFile f of
src/test.mideleted−13
@@ -1,13 +0,0 @@
1−N : Set 0;
2−O : N;
3−S : N -> N;
4−
5−one : N = S O;
6−two : N = S (S O);
7−three : N = S two;
8−
9−data Vect : (A:Set 0) -> (n:N) -> Set 0 where
10− Nil : (A:Set 0) -> (Vect A O)
11− | Cons : (A:Set 0) -> (k:N) -> (a:A) -> (Vect A k) -> (Vect A (S k));
12−
13−vtail : (A:Set 0) -> (k:N) -> (Vect A (S k)) -> (Vect A k);
test.minew file+29
@@ -0,0 +1,29 @@
1+data N : Set 0 where
2+ | O : N
3+ | S : N -> N;
4+
5+one : N = S O;
6+two : N = S (S O);
7+three : N = S two;
8+
9+plus : N -> N -> N;
10+
11+data Parity : N -> Set where
12+ | even : (n:N) -> (Parity (plus n n))
13+ | odd : (n:N) -> (Parity (S (plus n n)));
14+
15+data Vect : (A:Set 0) -> (n:N) -> Set 0 where
16+ | Nil : (A:Set 0) -> (Vect A O)
17+ | Cons : (A:Set 0) -> (k:N) -> (a:A) -> (Vect A k) -> (Vect A (S k));
18+
19+vtail : (A:Set 0) -> (k:N) -> (Vect A (S k)) -> (Vect A k);
20+vappend : (A:Set) -> (m:N) -> (n:N) -> (Vect A m) -> (Vect A n) -> (Vect A (plus m n));
21+vadd : (m:N) -> (Vect N m) -> (Vect N m) -> (Vect N m);
22+
23+data Infer : Set 0 where
24+ | MkInf : (A : Set) -> A -> Infer;
25+
26+data PClause : Set 0 where
27+ | MkP : (A : Set) -> A -> A -> PClause;
28+
29+npar : (n:N) -> (p:Parity n) -> N;