0ae24f1 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Shift core TT into a separate directory (for ease of reuse)

commit0ae24f1b5b9746bbfe07f736c324d46fe76e166a authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateMon 3 Oct 2011, 14:39 (15 years ago) parentac25f15

14 files changed+70−53

compare with master

unifiedsplit

miniidris.cabal+3−3 src/Core.hs → src/Core/Core.hs+1−1 src/CoreParser.hs → src/Core/CoreParser.hs+2−2 src/Elaborate.hs → src/Core/Elaborate.hs+6−5 src/Evaluate.hs → src/Core/Evaluate.hs+2−2 src/ProofShell.hs → src/Core/ProofShell.hs+6−6 src/ProofState.hs → src/Core/ProofState.hs+5−5 src/ShellParser.hs → src/Core/ShellParser.hs+4−4 src/Test.hs → src/Core/Test.hs src/Typecheck.hs → src/Core/Typecheck.hs+3−3 src/Unify.hs → src/Core/Unify.hs+3−3 src/Main.hs+6−6 src/test.mi−13 test.mi+29

miniidris.cabal+3−3

@@ -17,9 +17,9 @@ Build-type: Simple

1717Executable miniidris

1818 Main-is: Main.hs

1919 hs-source-dirs: src

20− Other-modules: Core, Evaluate, Typecheck, ProofState,

21− ProofState, CoreParser, ShellParser,

22− Unify, Elaborate

20+ Other-modules: Core.Core, Core.Evaluate, Core.Typecheck,

21+ Core.ProofShell, Core.ProofState, Core.CoreParser,

22+ Core.ShellParser, Core.Unify, Core.Elaborate

2323

2424 Build-depends: base>=4 && <5, parsec, mtl, Cabal, readline,

2525 containers

src/Core.hs → src/Core/Core.hsrenamed+1−1

@@ -1,6 +1,6 @@

11{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveFunctor #-}

3−module Core where

3+module Core.Core where

55import Control.Monad.State

66import Debug.Trace

src/CoreParser.hs → src/Core/CoreParser.hsrenamed+2−2

@@ -1,8 +1,8 @@

11{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}

3−module CoreParser(parseTerm, parseFile, parseDef, pTerm, iName) where

3+module Core.CoreParser(parseTerm, parseFile, parseDef, pTerm, iName) where

5−import Core

5+import Core.Core

77import Text.ParserCombinators.Parsec

88import Text.ParserCombinators.Parsec.Expr

src/Elaborate.hs → src/Core/Elaborate.hsrenamed+6−5

@@ -8,12 +8,13 @@

88 tactics out of the primitives.

99-}

1010

11−module Elaborate(module Elaborate, module ProofState) where

11+module Core.Elaborate(module Core.Elaborate,

12+ module Core.ProofState) where

1213

13−import ProofState

14−import Core

15−import Evaluate

16−import Typecheck

14+import Core.ProofState

15+import Core.Core

16+import Core.Evaluate

17+import Core.Typecheck

1718

1819import Control.Monad.State

1920import Data.Char

src/Evaluate.hs → src/Core/Evaluate.hsrenamed+2−2

@@ -1,13 +1,13 @@

11{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}

3−module Evaluate(normalise,

3+module Core.Evaluate(normalise,

44 Fun(..), Def(..), Context, toAlist,

55 emptyContext, addToCtxt, addConstant, addDatatype,

66 lookupTy, lookupP, lookupDef, lookupVal, lookupTyEnv) where

88import qualified Data.Map as Map

99import Debug.Trace

10−import Core

10+import Core.Core

1111

1212-- VALUES (as HOAS) ---------------------------------------------------------

1313

src/ProofShell.hs → src/Core/ProofShell.hsrenamed+6−6

@@ -1,12 +1,12 @@

11{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}

3−module ProofShell where

3+module Core.ProofShell where

5−import Typecheck

6−import Evaluate

7−import Core

8−import ShellParser

9−import Elaborate

5+import Core.Typecheck

6+import Core.Evaluate

7+import Core.Core

8+import Core.ShellParser

9+import Core.Elaborate

1010

1111import Control.Monad.State

1212import System.Console.Readline

src/ProofState.hs → src/Core/ProofState.hsrenamed+5−5

@@ -4,13 +4,13 @@

44 proofs, and some high level commands for introducing new theorems,

55 evaluation/checking inside the proof system, etc. --}

7−module ProofState(ProofState(..), newProof, envAtFocus, goalAtFocus,

7+module Core.ProofState(ProofState(..), newProof, envAtFocus, goalAtFocus,

88 Tactic(..), processTactic) where

10−import Typecheck

11−import Evaluate

12−import Core

13−import Unify

10+import Core.Typecheck

11+import Core.Evaluate

12+import Core.Core

13+import Core.Unify

1414

1515import Control.Monad.State

1616import Control.Applicative

src/ShellParser.hs → src/Core/ShellParser.hsrenamed+4−4

@@ -1,10 +1,10 @@

11{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}

3−module ShellParser(parseCommand, parseTactic) where

3+module Core.ShellParser(parseCommand, parseTactic) where

5−import Core

6−import Elaborate

7−import CoreParser

5+import Core.Core

6+import Core.Elaborate

7+import Core.CoreParser

99import Text.ParserCombinators.Parsec

1010import 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 @@

11{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor #-}

3−module Typecheck where

3+module Core.Typecheck where

55import Control.Monad.State

66import Debug.Trace

8−import Core

9−import Evaluate

8+import Core.Core

9+import Core.Evaluate

1010

1111-- To check conversion, normalise each term wrt the current environment.

1212-- 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 @@

11{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveFunctor #-}

3−module Unify(unify) where

3+module Core.Unify(unify) where

5−import Core

6−import Evaluate

5+import Core.Core

6+import Core.Evaluate

88import Control.Monad

src/Main.hs+6−6

@@ -1,11 +1,11 @@

11module Main where

3−import CoreParser

4−import ShellParser

5−import Core

6−import Typecheck

7−import ProofShell

8−import Evaluate

3+import Core.CoreParser

4+import Core.ShellParser

5+import Core.Core

6+import Core.Typecheck

7+import Core.ProofShell

8+import Core.Evaluate

1010main = do f <- readFile "test.mi"

1111 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;

5+one : N = S O;

6+two : N = S (S O);

7+three : N = S two;

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;