ff5f762 · Idris-dev · git.iko.soy

miniidris.cabal+1−1

compare with master

unifiedsplit

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

17Executable miniidris

18 Main-is: Main.hs

19 hs-source-dirs: src

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

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

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

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

23

src/Core/CoreParser.hs+1−1

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

2

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

4

5−import Core.Core

5+import Core.TT

6

7import Text.ParserCombinators.Parsec

8import Text.ParserCombinators.Parsec.Expr

src/Core/Elaborate.hs+1−1

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

12 module Core.ProofState) where

13

14import Core.ProofState

15−import Core.Core

15+import Core.TT

16import Core.Evaluate

17import Core.Typecheck

18

src/Core/Evaluate.hs+1−1

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

7

8import qualified Data.Map as Map

9import Debug.Trace

10−import Core.Core

10+import Core.TT

11

12-- VALUES (as HOAS) ---------------------------------------------------------

13

src/Core/ProofShell.hs+1−1

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

4

5import Core.Typecheck

6import Core.Evaluate

7−import Core.Core

7+import Core.TT

8import Core.ShellParser

9import Core.Elaborate

10

src/Core/ProofState.hs+1−1

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

9

10import Core.Typecheck

11import Core.Evaluate

12−import Core.Core

12+import Core.TT

13import Core.Unify

14

15import Control.Monad.State

src/Core/ShellParser.hs+1−1

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

2

3module Core.ShellParser(parseCommand, parseTactic) where

4

5−import Core.Core

5+import Core.TT

6import Core.Elaborate

7import Core.CoreParser

8

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

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

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

2

3−module Core.Core where

3+module Core.TT where

4

5import Control.Monad.State

6import 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

5import Control.Monad.State

6import Debug.Trace

7

8−import Core.Core

8+import Core.TT

9import Core.Evaluate

10

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

src/Core/Unify.hs+1−1

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

2

3module Core.Unify(unify) where

4

5−import Core.Core

5+import Core.TT

6import Core.Evaluate

7

8import Control.Monad

src/Main.hs+1−1

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

2

3import Core.CoreParser

4import Core.ShellParser

5−import Core.Core

5+import Core.TT

6import Core.Typecheck

7import Core.ProofShell

8import Core.Evaluate