Permalink
Browse files

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

  • Loading branch information...
1 parent ac25f15 commit 0ae24f1b5b9746bbfe07f736c324d46fe76e166a Edwin Brady committed Oct 3, 2011
View
@@ -17,9 +17,9 @@ Build-type: Simple
Executable miniidris
Main-is: Main.hs
hs-source-dirs: src
- Other-modules: Core, Evaluate, Typecheck, ProofState,
- ProofState, CoreParser, ShellParser,
- Unify, Elaborate
+ Other-modules: Core.Core, Core.Evaluate, Core.Typecheck,
+ Core.ProofShell, Core.ProofState, Core.CoreParser,
+ Core.ShellParser, Core.Unify, Core.Elaborate
Build-depends: base>=4 && <5, parsec, mtl, Cabal, readline,
containers
@@ -1,6 +1,6 @@
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveFunctor #-}
-module Core where
+module Core.Core where
import Control.Monad.State
import Debug.Trace
@@ -1,8 +1,8 @@
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
-module CoreParser(parseTerm, parseFile, parseDef, pTerm, iName) where
+module Core.CoreParser(parseTerm, parseFile, parseDef, pTerm, iName) where
-import Core
+import Core.Core
import Text.ParserCombinators.Parsec
import Text.ParserCombinators.Parsec.Expr
@@ -8,12 +8,13 @@
tactics out of the primitives.
-}
-module Elaborate(module Elaborate, module ProofState) where
+module Core.Elaborate(module Core.Elaborate,
+ module Core.ProofState) where
-import ProofState
-import Core
-import Evaluate
-import Typecheck
+import Core.ProofState
+import Core.Core
+import Core.Evaluate
+import Core.Typecheck
import Control.Monad.State
import Data.Char
@@ -1,13 +1,13 @@
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
-module Evaluate(normalise,
+module Core.Evaluate(normalise,
Fun(..), Def(..), Context, toAlist,
emptyContext, addToCtxt, addConstant, addDatatype,
lookupTy, lookupP, lookupDef, lookupVal, lookupTyEnv) where
import qualified Data.Map as Map
import Debug.Trace
-import Core
+import Core.Core
-- VALUES (as HOAS) ---------------------------------------------------------
@@ -1,12 +1,12 @@
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
-module ProofShell where
+module Core.ProofShell where
-import Typecheck
-import Evaluate
-import Core
-import ShellParser
-import Elaborate
+import Core.Typecheck
+import Core.Evaluate
+import Core.Core
+import Core.ShellParser
+import Core.Elaborate
import Control.Monad.State
import System.Console.Readline
@@ -4,13 +4,13 @@
proofs, and some high level commands for introducing new theorems,
evaluation/checking inside the proof system, etc. --}
-module ProofState(ProofState(..), newProof, envAtFocus, goalAtFocus,
+module Core.ProofState(ProofState(..), newProof, envAtFocus, goalAtFocus,
Tactic(..), processTactic) where
-import Typecheck
-import Evaluate
-import Core
-import Unify
+import Core.Typecheck
+import Core.Evaluate
+import Core.Core
+import Core.Unify
import Control.Monad.State
import Control.Applicative
@@ -1,10 +1,10 @@
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
-module ShellParser(parseCommand, parseTactic) where
+module Core.ShellParser(parseCommand, parseTactic) where
-import Core
-import Elaborate
-import CoreParser
+import Core.Core
+import Core.Elaborate
+import Core.CoreParser
import Text.ParserCombinators.Parsec
import Text.ParserCombinators.Parsec.Expr
File renamed without changes.
@@ -1,12 +1,12 @@
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor #-}
-module Typecheck where
+module Core.Typecheck where
import Control.Monad.State
import Debug.Trace
-import Core
-import Evaluate
+import Core.Core
+import Core.Evaluate
-- To check conversion, normalise each term wrt the current environment.
-- Since we haven't converted everything to de Bruijn indices yet, we'll have to
@@ -1,9 +1,9 @@
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveFunctor #-}
-module Unify(unify) where
+module Core.Unify(unify) where
-import Core
-import Evaluate
+import Core.Core
+import Core.Evaluate
import Control.Monad
View
@@ -1,11 +1,11 @@
module Main where
-import CoreParser
-import ShellParser
-import Core
-import Typecheck
-import ProofShell
-import Evaluate
+import Core.CoreParser
+import Core.ShellParser
+import Core.Core
+import Core.Typecheck
+import Core.ProofShell
+import Core.Evaluate
main = do f <- readFile "test.mi"
case parseFile f of
View
@@ -1,13 +0,0 @@
-N : Set 0;
-O : N;
-S : N -> N;
-
-one : N = S O;
-two : N = S (S O);
-three : N = S two;
-
-data Vect : (A:Set 0) -> (n:N) -> Set 0 where
- Nil : (A:Set 0) -> (Vect A O)
- | Cons : (A:Set 0) -> (k:N) -> (a:A) -> (Vect A k) -> (Vect A (S k));
-
-vtail : (A:Set 0) -> (k:N) -> (Vect A (S k)) -> (Vect A k);
View
@@ -0,0 +1,29 @@
+data N : Set 0 where
+ | O : N
+ | S : N -> N;
+
+one : N = S O;
+two : N = S (S O);
+three : N = S two;
+
+plus : N -> N -> N;
+
+data Parity : N -> Set where
+ | even : (n:N) -> (Parity (plus n n))
+ | odd : (n:N) -> (Parity (S (plus n n)));
+
+data Vect : (A:Set 0) -> (n:N) -> Set 0 where
+ | Nil : (A:Set 0) -> (Vect A O)
+ | Cons : (A:Set 0) -> (k:N) -> (a:A) -> (Vect A k) -> (Vect A (S k));
+
+vtail : (A:Set 0) -> (k:N) -> (Vect A (S k)) -> (Vect A k);
+vappend : (A:Set) -> (m:N) -> (n:N) -> (Vect A m) -> (Vect A n) -> (Vect A (plus m n));
+vadd : (m:N) -> (Vect N m) -> (Vect N m) -> (Vect N m);
+
+data Infer : Set 0 where
+ | MkInf : (A : Set) -> A -> Infer;
+
+data PClause : Set 0 where
+ | MkP : (A : Set) -> A -> A -> PClause;
+
+npar : (n:N) -> (p:Parity n) -> N;

0 comments on commit 0ae24f1

Please sign in to comment.