ff5f762 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Rename Core to TT

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

12 files changed+11−22

compare with master

unifiedsplit

miniidris.cabal+1−1 src/Core/CoreParser.hs+1−1 src/Core/Elaborate.hs+1−1 src/Core/Evaluate.hs+1−1 src/Core/ProofShell.hs+1−1 src/Core/ProofState.hs+1−1 src/Core/ShellParser.hs+1−1 src/Core/Core.hs → src/Core/TT.hs+1−1 src/Core/Test.hs−11 src/Core/Typecheck.hs+1−1 src/Core/Unify.hs+1−1 src/Main.hs+1−1

miniidris.cabal+1−1

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

1717Executable miniidris

1818 Main-is: Main.hs

1919 hs-source-dirs: src

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

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

2121 Core.ProofShell, Core.ProofState, Core.CoreParser,

2222 Core.ShellParser, Core.Unify, Core.Elaborate

2323

src/Core/CoreParser.hs+1−1

@@ -2,7 +2,7 @@

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

5−import Core.Core

5+import Core.TT

77import Text.ParserCombinators.Parsec

88import Text.ParserCombinators.Parsec.Expr

src/Core/Elaborate.hs+1−1

@@ -12,7 +12,7 @@ module Core.Elaborate(module Core.Elaborate,

1212 module Core.ProofState) where

1313

1414import Core.ProofState

15−import Core.Core

15+import Core.TT

1616import Core.Evaluate

1717import Core.Typecheck

1818

src/Core/Evaluate.hs+1−1

@@ -7,7 +7,7 @@ module Core.Evaluate(normalise,

88import qualified Data.Map as Map

99import Debug.Trace

10−import Core.Core

10+import Core.TT

1111

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

1313

src/Core/ProofShell.hs+1−1

@@ -4,7 +4,7 @@ module Core.ProofShell where

55import Core.Typecheck

66import Core.Evaluate

7−import Core.Core

7+import Core.TT

88import Core.ShellParser

99import Core.Elaborate

1010

src/Core/ProofState.hs+1−1

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

1010import Core.Typecheck

1111import Core.Evaluate

12−import Core.Core

12+import Core.TT

1313import Core.Unify

1414

1515import Control.Monad.State

src/Core/ShellParser.hs+1−1

@@ -2,7 +2,7 @@

33module Core.ShellParser(parseCommand, parseTactic) where

5−import Core.Core

5+import Core.TT

66import Core.Elaborate

77import Core.CoreParser

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

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

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

3−module Core.Core where

3+module Core.TT where

55import Control.Monad.State

66import Debug.Trace

src/Core/Test.hsdeleted−11

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

1−module Test where

2−

3−import Parser

4−import Core

5−import Typecheck

6−

7−test = do f <- readFile "test.mi"

8− let Right defs = parseFile f

9− print defs

10− let ctxt = checkProgram [] defs

11− print ctxt

src/Core/Typecheck.hs+1−1

@@ -5,7 +5,7 @@ module Core.Typecheck where

55import Control.Monad.State

66import Debug.Trace

8−import Core.Core

8+import Core.TT

99import Core.Evaluate

1010

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

src/Core/Unify.hs+1−1

@@ -2,7 +2,7 @@

33module Core.Unify(unify) where

5−import Core.Core

5+import Core.TT

66import Core.Evaluate

88import Control.Monad

src/Main.hs+1−1

@@ -2,7 +2,7 @@ module Main where

33import Core.CoreParser

44import Core.ShellParser

5−import Core.Core

5+import Core.TT

66import Core.Typecheck

77import Core.ProofShell

88import Core.Evaluate