Permalink
Browse files

Rename Core to TT

  • Loading branch information...
1 parent 0ae24f1 commit ff5f76217d31987abf328f3904d17daec2e5441a Edwin Brady committed Oct 3, 2011
View
@@ -17,7 +17,7 @@ Build-type: Simple
Executable miniidris
Main-is: Main.hs
hs-source-dirs: src
- Other-modules: Core.Core, Core.Evaluate, Core.Typecheck,
+ Other-modules: Core.TT, Core.Evaluate, Core.Typecheck,
Core.ProofShell, Core.ProofState, Core.CoreParser,
Core.ShellParser, Core.Unify, Core.Elaborate
View
@@ -2,7 +2,7 @@
module Core.CoreParser(parseTerm, parseFile, parseDef, pTerm, iName) where
-import Core.Core
+import Core.TT
import Text.ParserCombinators.Parsec
import Text.ParserCombinators.Parsec.Expr
View
@@ -12,7 +12,7 @@ module Core.Elaborate(module Core.Elaborate,
module Core.ProofState) where
import Core.ProofState
-import Core.Core
+import Core.TT
import Core.Evaluate
import Core.Typecheck
View
@@ -7,7 +7,7 @@ module Core.Evaluate(normalise,
import qualified Data.Map as Map
import Debug.Trace
-import Core.Core
+import Core.TT
-- VALUES (as HOAS) ---------------------------------------------------------
View
@@ -4,7 +4,7 @@ module Core.ProofShell where
import Core.Typecheck
import Core.Evaluate
-import Core.Core
+import Core.TT
import Core.ShellParser
import Core.Elaborate
View
@@ -9,7 +9,7 @@ module Core.ProofState(ProofState(..), newProof, envAtFocus, goalAtFocus,
import Core.Typecheck
import Core.Evaluate
-import Core.Core
+import Core.TT
import Core.Unify
import Control.Monad.State
View
@@ -2,7 +2,7 @@
module Core.ShellParser(parseCommand, parseTactic) where
-import Core.Core
+import Core.TT
import Core.Elaborate
import Core.CoreParser
@@ -1,6 +1,6 @@
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveFunctor #-}
-module Core.Core where
+module Core.TT where
import Control.Monad.State
import Debug.Trace
View
@@ -1,11 +0,0 @@
-module Test where
-
-import Parser
-import Core
-import Typecheck
-
-test = do f <- readFile "test.mi"
- let Right defs = parseFile f
- print defs
- let ctxt = checkProgram [] defs
- print ctxt
View
@@ -5,7 +5,7 @@ module Core.Typecheck where
import Control.Monad.State
import Debug.Trace
-import Core.Core
+import Core.TT
import Core.Evaluate
-- To check conversion, normalise each term wrt the current environment.
View
@@ -2,7 +2,7 @@
module Core.Unify(unify) where
-import Core.Core
+import Core.TT
import Core.Evaluate
import Control.Monad
View
@@ -2,7 +2,7 @@ module Main where
import Core.CoreParser
import Core.ShellParser
-import Core.Core
+import Core.TT
import Core.Typecheck
import Core.ProofShell
import Core.Evaluate

0 comments on commit ff5f762

Please sign in to comment.