diff --git a/Makefile b/Makefile
--- a/Makefile
+++ b/Makefile
@@ -14,15 +14,15 @@
$(CABAL) build $(CABALFLAGS)
test:
- make -C test IDRIS=../dist/build/idris
+ $(MAKE) -C test IDRIS=../dist/build/idris
test_java:
- make -C test IDRIS=../dist/build/idris test_java
+ $(MAKE) -C test IDRIS=../dist/build/idris test_java
relib:
- make -C lib IDRIS=../dist/build/idris/idris RTS=../dist/build/rts/libidris_rts clean
- make -C effects IDRIS=../dist/build/idris/idris RTS=../dist/build/rts/libidris_rts DIST=../dist/build clean
- make -C javascript IDRIS=../dist/build/idris/idris RTS=../dist/build/rts/libidris_rts DIST=../dist/build clean
+ $(MAKE) -C lib IDRIS=../dist/build/idris/idris RTS=../dist/build/rts/libidris_rts clean
+ $(MAKE) -C effects IDRIS=../dist/build/idris/idris RTS=../dist/build/rts/libidris_rts DIST=../dist/build clean
+ $(MAKE) -C javascript IDRIS=../dist/build/idris/idris RTS=../dist/build/rts/libidris_rts DIST=../dist/build clean
$(CABAL) install $(CABALFLAGS)
linecount:
diff --git a/config.mk b/config.mk
--- a/config.mk
+++ b/config.mk
@@ -1,6 +1,7 @@
GMP_INCLUDE_DIR :=
CC :=gcc
CABAL :=cabal
+CFLAGS :=-O2 -Wall $(CFLAGS)
#CABALFLAGS :=
## Disable building of Effects
#CABALFLAGS :=-f NoEffects
diff --git a/idris.cabal b/idris.cabal
--- a/idris.cabal
+++ b/idris.cabal
@@ -1,5 +1,5 @@
Name: idris
-Version: 0.9.9
+Version: 0.9.9.1
License: BSD3
License-file: LICENSE
Author: Edwin Brady
@@ -227,6 +227,12 @@
test/test028/run
test/test028/*.idr
test/test028/expected
+ test/test029/run
+ test/test029/*.idr
+ test/test029/expected
+ test/test030/run
+ test/test030/*.idr
+ test/test030/expected
source-repository head
@@ -250,15 +256,16 @@
Core.ShellParser, Core.Unify, Core.Elaborate,
Core.CaseTree, Core.Constraints,
- Idris.AbsSyntax, Idris.AbsSyntaxTree,
+ Idris.AbsSyntax, Idris.AbsSyntaxTree, Idris.Colours,
Idris.Parser, Idris.Help, Idris.IdeSlave, Idris.REPL,
Idris.REPLParser, Idris.ElabDecls, Idris.Error,
Idris.Delaborate, Idris.Primitives, Idris.Imports,
- Idris.Compiler, Idris.Prover, Idris.ElabTerm,
+ Idris.Prover, Idris.ElabTerm,
Idris.Coverage, Idris.IBC, Idris.Unlit,
Idris.DataOpts, Idris.Transforms, Idris.DSL,
Idris.UnusedArgs, Idris.Docs, Idris.Completion,
- Idris.PartialEval, Idris.Providers,
+ Idris.PartialEval, Idris.Providers, Idris.Chaser,
+ Idris.Inliner,
Util.Pretty, Util.System, Util.DynamicLinker,
Pkg.Package, Pkg.PParser,
@@ -273,11 +280,12 @@
Paths_idris
Build-depends: base>=4 && <5, parsec>=3, mtl, Cabal,
- haskeline>=0.7, split, directory,
+ haskeline>=0.7, split, directory>=1.2,
+ time>=1.4,
containers, process, transformers, filepath,
directory, binary, bytestring, text, pretty,
language-java>=0.2.2, libffi,
- vector, vector-binary-instances
+ vector, vector-binary-instances, ansi-terminal
Extensions: MultiParamTypeClasses, FunctionalDependencies,
FlexibleInstances, TemplateHaskell
diff --git a/java/executable_pom.xml b/java/executable_pom.xml
--- a/java/executable_pom.xml
+++ b/java/executable_pom.xml
@@ -15,7 +15,7 @@
org.idris-lang
idris
- 0.9.9
+ 0.9.10-alpha-1
$DEPENDENCIES$
@@ -44,7 +44,7 @@
org.apache.maven.plugins
maven-shade-plugin
- 2.0
+ 2.1
package
diff --git a/java/executable_pom_template.xml b/java/executable_pom_template.xml
--- a/java/executable_pom_template.xml
+++ b/java/executable_pom_template.xml
@@ -15,7 +15,7 @@
org.idris-lang
idris
- $RTS-VERSION$
+ 0.9.10-alpha-1
$DEPENDENCIES$
@@ -44,7 +44,7 @@
org.apache.maven.plugins
maven-shade-plugin
- 2.0
+ 2.1
package
diff --git a/javascript/JavaScript.idr b/javascript/JavaScript.idr
--- a/javascript/JavaScript.idr
+++ b/javascript/JavaScript.idr
@@ -2,12 +2,11 @@
%access public
--- TODO: Get rid of this hack, and find a better way.
private
isUndefined : Ptr -> IO Bool
isUndefined p = do
res <- mkForeign (
- FFun "(function(arg) { return arg === undefined;})" [FPtr] FString) p
+ FFun "%0 === undefined" [FPtr] FString) p
if res == "false"
then (return False)
else (return True)
@@ -28,15 +27,15 @@
setText : Element -> String -> IO ()
setText (MkElem p) s =
- mkForeign (FFun ".textContent=" [FPtr, FString] FUnit) p s
+ mkForeign (FFun "%0.textContent=%1" [FPtr, FString] FUnit) p s
setOnClick : Element -> (Event -> IO Bool) -> IO ()
setOnClick (MkElem e) f =
mkForeign (
- FFun "['onclick']=" [ FPtr
- , FFunction (FAny Event) (FAny (IO Bool))
- ] FUnit) e f
+ FFun "%0['onclick']=%1" [ FPtr
+ , FFunction (FAny Event) (FAny (IO Bool))
+ ] FUnit) e f
--------------------------------------------------------------------------------
-- Nodelists
--------------------------------------------------------------------------------
@@ -46,7 +45,9 @@
elemAt : NodeList -> Nat -> IO (Maybe Element)
elemAt (MkNodeList p) i = do
- e <- mkForeign (FFun ".item" [FPtr, FInt] FPtr) p (prim__truncBigInt_Int (cast i))
+ e <- mkForeign (FFun "%0.item(%1)" [FPtr, FInt] FPtr) p (
+ prim__truncBigInt_Int (cast i)
+ )
d <- isUndefined e
if d
then return $ Just (MkElem e)
@@ -62,12 +63,13 @@
setInterval : (() -> IO ()) -> Float -> IO Interval
setInterval f t = do
e <- mkForeign (
- FFun "setInterval" [FFunction FUnit (FAny (IO ())), FFloat] FPtr) f t
+ FFun "setInterval(%0,%1)" [FFunction FUnit (FAny (IO ())), FFloat] FPtr
+ ) f t
return (MkInterval e)
clearInterval : Interval -> IO ()
clearInterval (MkInterval p) =
- mkForeign (FFun "clearInterval" [FPtr] FUnit) p
+ mkForeign (FFun "clearInterval(%0)" [FPtr] FUnit) p
--------------------------------------------------------------------------------
-- Timeouts
@@ -78,24 +80,25 @@
setTimeout : (() -> IO ()) -> Float -> IO Timeout
setTimeout f t = do
e <- mkForeign (
- FFun "setTimeout" [FFunction FUnit (FAny (IO ())), FFloat] FPtr) f t
+ FFun "setTimeout(%0,%1)" [FFunction FUnit (FAny (IO ())), FFloat] FPtr
+ ) f t
return (MkTimeout e)
clearTimeout : Timeout -> IO ()
clearTimeout (MkTimeout p) =
- mkForeign (FFun "clearTimeout" [FPtr] FUnit) p
+ mkForeign (FFun "clearTimeout(%0)" [FPtr] FUnit) p
--------------------------------------------------------------------------------
-- Basic IO
--------------------------------------------------------------------------------
alert : String -> IO ()
alert msg =
- mkForeign (FFun "alert" [FString] FUnit) msg
+ mkForeign (FFun "alert(%0)" [FString] FUnit) msg
--------------------------------------------------------------------------------
-- DOM
--------------------------------------------------------------------------------
query : String -> IO NodeList
query q = do
- e <- mkForeign (FFun "document.querySelectorAll" [FString] FPtr) q
+ e <- mkForeign (FFun "document.querySelectorAll(%0)" [FString] FPtr) q
return (MkNodeList e)
diff --git a/js/Runtime-common.js b/js/Runtime-common.js
--- a/js/Runtime-common.js
+++ b/js/Runtime-common.js
@@ -14,17 +14,26 @@
/** @constructor */
var __IDRRT__Tailcall = function(f) { this.f = f };
+
var __IDRRT__ffiWrap = function(fid) {
- return function(arg) {
- return __IDRRT__tailcall(function(){
- return __IDR__APPLY0(fid, arg);
- });
- };
+ return function(){
+ var res = fid;
+ var i = 0;
+ var arg;
+ while (res instanceof __IDRRT__Con){
+ arg = arguments[i];
+ res = __IDRRT__tailcall(function(){
+ return __IDR__mAPPLY0(res, arg);
+ });
+ ++i;
+ }
+ return res;
+ }
};
/** @constructor */
-var __IDRRT__Con = function(i,vars) {
- this.i = i;
+var __IDRRT__Con = function(tag,vars) {
+ this.tag = tag;
this.vars = vars;
};
diff --git a/lib/Builtins.idr b/lib/Builtins.idr
--- a/lib/Builtins.idr
+++ b/lib/Builtins.idr
@@ -34,11 +34,11 @@
trace_malloc : a -> a
trace_malloc x = x -- compiled specially
-abstract
+abstract %assert_total -- need to pretend
believe_me : a -> b -- compiled specially as id, use with care!
believe_me x = prim__believe_me _ _ x
-public -- reduces at compile time, use with extreme care!
+public %assert_total -- reduces at compile time, use with extreme care!
really_believe_me : a -> b
really_believe_me x = prim__believe_me _ _ x
@@ -188,28 +188,27 @@
min x y = if (x < y) then x else y
-
instance Ord Int where
compare x y = if (x == y) then EQ else
- if (boolOp prim__ltInt x y) then LT else
+ if (boolOp prim__sltInt x y) then LT else
GT
instance Ord Integer where
compare x y = if (x == y) then EQ else
- if (boolOp prim__ltBigInt x y) then LT else
+ if (boolOp prim__sltBigInt x y) then LT else
GT
instance Ord Float where
compare x y = if (x == y) then EQ else
- if (boolOp prim__ltFloat x y) then LT else
+ if (boolOp prim__sltFloat x y) then LT else
GT
instance Ord Char where
compare x y = if (x == y) then EQ else
- if (boolOp prim__ltChar x y) then LT else
+ if (boolOp prim__sltChar x y) then LT else
GT
diff --git a/lib/Data/Bits.idr b/lib/Data/Bits.idr
--- a/lib/Data/Bits.idr
+++ b/lib/Data/Bits.idr
@@ -1,5 +1,7 @@
module Data.Bits
+import Prelude
+
%default total
divCeil : Nat -> Nat -> Nat
@@ -307,6 +309,7 @@
complement (MkBits x) = MkBits (complement' x)
-- TODO: Prove
+%assert_total -- can't verify coverage of with block
zext' : machineTy (nextBytes n) -> machineTy (nextBytes (n+m))
zext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
| (Z, Z) = believe_me x
@@ -362,6 +365,7 @@
-- cast x = MkBits (zeroUnused (natToBits n))
-- TODO: Prove
+%assert_total -- can't verify coverage of with block
sext' : machineTy (nextBytes n) -> machineTy (nextBytes (n+m))
sext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
| (Z, Z) = let pad = getPad {n=0} n in
@@ -396,6 +400,7 @@
--signExtend {m=m} (MkBits x) = MkBits (zeroUnused (sext' x))
-- TODO: Prove
+%assert_total -- can't verify coverage of with block
trunc' : machineTy (nextBytes (n+m)) -> machineTy (nextBytes n)
trunc' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
| (Z, Z) = believe_me x
diff --git a/lib/Data/BoundedList.idr b/lib/Data/BoundedList.idr
--- a/lib/Data/BoundedList.idr
+++ b/lib/Data/BoundedList.idr
@@ -1,5 +1,7 @@
module Data.BoundedList
+import Prelude
+
%access public
%default total
diff --git a/lib/Data/Morphisms.idr b/lib/Data/Morphisms.idr
--- a/lib/Data/Morphisms.idr
+++ b/lib/Data/Morphisms.idr
@@ -1,6 +1,6 @@
module Data.Morphisms
-import Builtins
+import Prelude
%access public
diff --git a/lib/Data/SortedMap.idr b/lib/Data/SortedMap.idr
--- a/lib/Data/SortedMap.idr
+++ b/lib/Data/SortedMap.idr
@@ -1,5 +1,6 @@
module Data.SortedMap
+import Prelude
-- TODO: write merge and split
data Tree : Nat -> Type -> Type -> Type where
diff --git a/lib/Data/SortedSet.idr b/lib/Data/SortedSet.idr
--- a/lib/Data/SortedSet.idr
+++ b/lib/Data/SortedSet.idr
@@ -1,5 +1,6 @@
module Data.SortedSet
+import Prelude
import Data.SortedMap
-- TODO: add intersection, union, difference
diff --git a/lib/Data/Vect/Quantifiers.idr b/lib/Data/Vect/Quantifiers.idr
--- a/lib/Data/Vect/Quantifiers.idr
+++ b/lib/Data/Vect/Quantifiers.idr
@@ -1,5 +1,7 @@
module Data.Vect.Quantifiers
+import Prelude
+
data Any : (P : a -> Type) -> Vect n a -> Type where
Here : {P : a -> Type} -> {xs : Vect n a} -> P x -> Any P (x :: xs)
There : {P : a -> Type} -> {xs : Vect n a} -> Any P xs -> Any P (x :: xs)
diff --git a/lib/Debug/Trace.idr b/lib/Debug/Trace.idr
--- a/lib/Debug/Trace.idr
+++ b/lib/Debug/Trace.idr
@@ -1,5 +1,6 @@
module Debug.Trace
+import Prelude
import IO
trace : String -> a -> a
diff --git a/lib/Decidable/Equality.idr b/lib/Decidable/Equality.idr
--- a/lib/Decidable/Equality.idr
+++ b/lib/Decidable/Equality.idr
@@ -1,6 +1,6 @@
module Decidable.Equality
-import Builtins
+import Prelude
--------------------------------------------------------------------------------
-- Utility lemmas
diff --git a/lib/IO.idr b/lib/IO.idr
--- a/lib/IO.idr
+++ b/lib/IO.idr
@@ -2,24 +2,27 @@
%access public
-abstract data IO a = prim__IO a
+abstract data PrimIO a = prim__IO a
-abstract
-io_bind : IO a -> (a -> IO b) -> IO b
-io_bind (prim__IO v) k = k v
+abstract data World = TheWorld
-unsafePerformIO : IO a -> a
--- compiled as primitive
+abstract WorldRes : Type -> Type
+WorldRes x = x
+-- abstract data WorldRes a = MkWR a World
+
+abstract data IO a = MkIO (World -> PrimIO (WorldRes a))
+
abstract
-io_return : a -> IO a
-io_return x = prim__IO x
+prim_io_bind : PrimIO a -> (a -> PrimIO b) -> PrimIO b
+prim_io_bind (prim__IO v) k = k v
--- This may seem pointless, but we can use it to force an
--- evaluation of main that Epic wouldn't otherwise do...
+unsafePerformPrimIO : PrimIO a -> a
+-- compiled as primitive
-run__IO : IO () -> IO ()
-run__IO v = io_bind v (\v' => io_return v')
+abstract
+prim_io_return : a -> PrimIO a
+prim_io_return x = prim__IO x
data IntTy = ITChar | ITNative | IT8 | IT16 | IT32 | IT64 | IT8x16 | IT16x8 | IT32x4 | IT64x2
data FTy = FIntT IntTy
@@ -89,7 +92,7 @@
interpFTy (FFunction a b) = interpFTy a -> interpFTy b
ForeignTy : (xs:List FTy) -> (t:FTy) -> Type
-ForeignTy Nil rt = IO (interpFTy rt)
+ForeignTy Nil rt = World -> PrimIO (interpFTy rt)
ForeignTy (t::ts) rt = interpFTy t -> ForeignTy ts rt
@@ -97,11 +100,50 @@
FFun : String -> (xs:List FTy) -> (t:FTy) ->
Foreign (ForeignTy xs t)
-mkForeign : Foreign x -> x
-mkLazyForeign : Foreign x -> x
+mkForeignPrim : Foreign x -> x
+mkLazyForeignPrim : Foreign x -> x
-- mkForeign and mkLazyForeign compiled as primitives
+abstract
+io_bind : IO a -> (a -> IO b) -> IO b
+io_bind (MkIO fn) k
+ = MkIO (\w => prim_io_bind (fn w)
+ (\ b => case k b of
+ MkIO fkb => fkb w))
+
+abstract
+io_return : a -> IO a
+io_return x = MkIO (\w => prim_io_return x)
+
+liftPrimIO : (World -> PrimIO a) -> IO a
+liftPrimIO f = MkIO (\w => prim_io_bind (f w)
+ (\x => prim_io_return x))
+
+run__IO : IO () -> PrimIO ()
+run__IO (MkIO f) = prim_io_bind (f TheWorld)
+ (\ b => prim_io_return b)
+
+run__provider : IO a -> PrimIO a
+run__provider (MkIO f) = prim_io_bind (f TheWorld)
+ (\ b => prim_io_return b)
+
+-- io_bind v (\v' => io_return v')
+
+prim_fork : |(thread:PrimIO ()) -> PrimIO Ptr
+prim_fork x = prim_io_return prim__vm -- compiled specially
+
fork : |(thread:IO ()) -> IO Ptr
-fork x = io_return prim__vm -- compiled specially
+fork (MkIO f) = MkIO (\w => prim_io_bind
+ (prim_fork (prim_io_bind (f w)
+ (\ x => prim_io_return x)))
+ (\x => prim_io_return x))
+
+partial
+prim_fread : Ptr -> IO String
+prim_fread h = MkIO (\w => prim_io_return (prim__readString h))
+
+unsafePerformIO : IO a -> a
+unsafePerformIO (MkIO f) = unsafePerformPrimIO
+ (prim_io_bind (f TheWorld) (\ b => prim_io_return b))
diff --git a/lib/Language/Reflection.idr b/lib/Language/Reflection.idr
--- a/lib/Language/Reflection.idr
+++ b/lib/Language/Reflection.idr
@@ -1,6 +1,6 @@
module Language.Reflection
-import Prelude.Vect
+import Prelude
%access public
@@ -98,17 +98,27 @@
map f (PVar x) = PVar (f x)
map f (PVTy x) = PVTy (f x)
-total
-traverse : (Applicative f) => (a -> f b) -> Binder a -> f (Binder b)
-traverse f (Lam x) = [| Lam (f x) |]
-traverse f (Pi x) = [| Pi (f x) |]
-traverse f (Let x y) = [| Let (f x) (f y) |]
-traverse f (NLet x y) = [| NLet (f x) (f y) |]
-traverse f (Hole x) = [| Hole (f x) |]
-traverse f (GHole x) = [| GHole (f x) |]
-traverse f (Guess x y) = [| Guess (f x) (f y) |]
-traverse f (PVar x) = [| PVar (f x) |]
-traverse f (PVTy x) = [| PVTy (f x) |]
+instance Foldable Binder where
+ foldr f z (Lam x) = f x z
+ foldr f z (Pi x) = f x z
+ foldr f z (Let x y) = f x (f y z)
+ foldr f z (NLet x y) = f x (f y z)
+ foldr f z (Hole x) = f x z
+ foldr f z (GHole x) = f x z
+ foldr f z (Guess x y) = f x (f y z)
+ foldr f z (PVar x) = f x z
+ foldr f z (PVTy x) = f x z
+
+instance Traversable Binder where
+ traverse f (Lam x) = [| Lam (f x) |]
+ traverse f (Pi x) = [| Pi (f x) |]
+ traverse f (Let x y) = [| Let (f x) (f y) |]
+ traverse f (NLet x y) = [| NLet (f x) (f y) |]
+ traverse f (Hole x) = [| Hole (f x) |]
+ traverse f (GHole x) = [| GHole (f x) |]
+ traverse f (Guess x y) = [| Guess (f x) (f y) |]
+ traverse f (PVar x) = [| PVar (f x) |]
+ traverse f (PVTy x) = [| PVTy (f x) |]
-- | Reflection of the well typed core language
diff --git a/lib/Language/Reflection/Utils.idr b/lib/Language/Reflection/Utils.idr
--- a/lib/Language/Reflection/Utils.idr
+++ b/lib/Language/Reflection/Utils.idr
@@ -1,5 +1,8 @@
module Language.Reflection.Utils
+import Prelude
+import Language.Reflection
+
--------------------------------------------------------
-- Tactic construction conveniences
--------------------------------------------------------
diff --git a/lib/Prelude.idr b/lib/Prelude.idr
--- a/lib/Prelude.idr
+++ b/lib/Prelude.idr
@@ -15,6 +15,7 @@
import Prelude.Vect
import Prelude.Strings
import Prelude.Chars
+import Prelude.Traversable
%access public
%default total
@@ -180,8 +181,11 @@
---- Functor instances
+instance Functor PrimIO where
+ map f io = prim_io_bind io (prim_io_return . f)
+
instance Functor IO where
- map f io = io_bind io (io_return . f)
+ map f io = io_bind io (\b => io_return (f b))
instance Functor Maybe where
map f (Just x) = Just (f x)
@@ -193,11 +197,17 @@
---- Applicative instances
-instance Applicative IO where
- pure = io_return
+instance Applicative PrimIO where
+ pure = prim_io_return
- am <$> bm = io_bind am (\f => io_bind bm (io_return . f))
+ am <$> bm = prim_io_bind am (\f => prim_io_bind bm (prim_io_return . f))
+instance Applicative IO where
+ pure x = io_return x
+ f <$> a = io_bind f (\f' =>
+ io_bind a (\a' =>
+ io_return (f' a')))
+
instance Applicative Maybe where
pure = Just
@@ -236,7 +246,10 @@
---- Monad instances
-instance Monad IO where
+instance Monad PrimIO where
+ b >>= k = prim_io_bind b k
+
+instance Monad IO where
b >>= k = io_bind b k
instance Monad Maybe where
@@ -253,6 +266,20 @@
instance Monad (Vect n) where
m >>= f = diag (map f m)
+---- Traversable instances
+
+instance Traversable Maybe where
+ traverse f Nothing = pure Nothing
+ traverse f (Just x) = [| Just (f x) |]
+
+instance Traversable List where
+ traverse f [] = pure List.Nil
+ traverse f (x::xs) = [| List.(::) (f x) (traverse f xs) |]
+
+instance Traversable (Vect n) where
+ traverse f [] = pure Vect.Nil
+ traverse f (x::xs) = [| Vect.(::) (f x) (traverse f xs) |]
+
---- some mathematical operations
%include C "math.h"
@@ -333,12 +360,6 @@
---- More utilities
-sum : Num a => List a -> a
-sum = foldl (+) 0
-
-prod : Num a => List a -> a
-prod = foldl (*) 1
-
curry : ((a, b) -> c) -> a -> b -> c
curry f a b = f (a, b)
@@ -373,7 +394,7 @@
partial
getLine : IO String
-getLine = return (prim__readString prim__stdin)
+getLine = prim_fread prim__stdin
partial
putChar : Char -> IO ()
@@ -392,7 +413,8 @@
stdin = FHandle prim__stdin
do_fopen : String -> String -> IO Ptr
-do_fopen f m = mkForeign (FFun "fileOpen" [FString, FString] FPtr) f m
+do_fopen f m
+ = mkForeign (FFun "fileOpen" [FString, FString] FPtr) f m
fopen : String -> String -> IO File
fopen f m = do h <- do_fopen f m
@@ -417,15 +439,19 @@
partial
do_fread : Ptr -> IO String
-do_fread h = return (prim__readString h)
+do_fread h = prim_fread h
+-- mkForeign (FFun "idris_readStr" [FPtr, FPtr] (FAny String))
+-- prim__vm h
+
partial
fread : File -> IO String
fread (FHandle h) = do_fread h
partial
do_fwrite : Ptr -> String -> IO ()
-do_fwrite h s = mkForeign (FFun "fputStr" [FPtr, FString] FUnit) h s
+do_fwrite h s
+ = mkForeign (FFun "fputStr" [FPtr, FString] FUnit) h s
partial
fwrite : File -> String -> IO ()
diff --git a/lib/Prelude/Applicative.idr b/lib/Prelude/Applicative.idr
--- a/lib/Prelude/Applicative.idr
+++ b/lib/Prelude/Applicative.idr
@@ -29,18 +29,3 @@
when : Applicative f => Bool -> f () -> f ()
when a f = if a then f else pure ()
-
-sequence : Applicative f => List (f a) -> f (List a)
-sequence [] = pure []
-sequence (x :: xs) = map (::) x <$> sequence xs
-
-sequence_ : Applicative f => List (f a) -> f ()
-sequence_ [] = pure ()
-sequence_ (x :: xs) = x $> sequence_ xs
-
-traverse : Applicative f => (a -> f b) -> List a -> f (List b)
-traverse f xs = sequence (map f xs)
-
-traverse_ : Applicative f => (a -> f b) -> List a -> f ()
-traverse_ f (x :: xs) = f x $> traverse_ f xs
-traverse_ f [] = pure ()
diff --git a/lib/Prelude/Foldable.idr b/lib/Prelude/Foldable.idr
new file mode 100644
--- /dev/null
+++ b/lib/Prelude/Foldable.idr
@@ -0,0 +1,38 @@
+module Prelude.Foldable
+
+import Builtins
+import Prelude.Algebra
+
+%access public
+%default total
+
+class Foldable (t : Type -> Type) where
+ foldr : (elt -> acc -> acc) -> acc -> t elt -> acc
+
+foldl : Foldable t => (acc -> elt -> acc) -> acc -> t elt -> acc
+foldl f z t = foldr (flip (.) . flip f) id t z
+
+concat : (Foldable t, Monoid a) => t a -> a
+concat = foldr (<+>) neutral
+
+concatMap : (Foldable t, Monoid m) => (a -> m) -> t a -> m
+concatMap f = foldr ((<+>) . f) neutral
+
+and : Foldable t => t Bool -> Bool
+and = foldr (&&) True
+
+or : Foldable t => t Bool -> Bool
+or = foldr (||) False
+
+any : Foldable t => (a -> Bool) -> t a -> Bool
+any p = foldr ((||) . p) False
+
+all : Foldable t => (a -> Bool) -> t a -> Bool
+all p = foldr ((&&) . p) True
+
+sum : (Foldable t, Num a) => t a -> a
+sum = foldr (+) 0
+
+product : (Foldable t, Num a) => t a -> a
+product = foldr (*) 1
+
diff --git a/lib/Prelude/Heap.idr b/lib/Prelude/Heap.idr
--- a/lib/Prelude/Heap.idr
+++ b/lib/Prelude/Heap.idr
@@ -106,7 +106,7 @@
where
%assert_total -- relies on deleteMinimum making heap smaller
toList' : Ord a => (h : MaxiphobicHeap a) -> (isEmpty h = False) -> List a
- toList' heap p = findMinimum heap p :: (toList (deleteMinimum heap p))
+ toList' heap p = findMinimum heap p :: (Heap.toList (deleteMinimum heap p))
fromList : Ord a => List a -> MaxiphobicHeap a
fromList = foldr insert empty
diff --git a/lib/Prelude/List.idr b/lib/Prelude/List.idr
--- a/lib/Prelude/List.idr
+++ b/lib/Prelude/List.idr
@@ -3,6 +3,7 @@
import Builtins
import Prelude.Algebra
+import Prelude.Foldable
import Prelude.Functor
import Prelude.Maybe
import Prelude.Nat
@@ -217,40 +218,16 @@
-- Folds
--------------------------------------------------------------------------------
-foldl : (a -> b -> a) -> a -> List b -> a
-foldl f e [] = e
-foldl f e (x::xs) = foldl f (f e x) xs
-
-foldr : (a -> b -> b) -> b -> List a -> b
-foldr f e [] = e
-foldr f e (x::xs) = f x (foldr f e xs)
+instance Foldable List where
+ foldr f e [] = e
+ foldr f e (x::xs) = f x (foldr f e xs)
--------------------------------------------------------------------------------
-- Special folds
--------------------------------------------------------------------------------
-mconcat : Monoid a => List a -> a
-mconcat = foldr (<+>) neutral
-
-concat : List (List a) -> List a
-concat [] = []
-concat (x::xs) = x ++ concat xs
-
-concatMap : (a -> List b) -> List a -> List b
-concatMap f [] = []
-concatMap f (x::xs) = f x ++ concatMap f xs
-
-and : List Bool -> Bool
-and = foldr (&&) True
-
-or : List Bool -> Bool
-or = foldr (||) False
-
-any : (a -> Bool) -> List a -> Bool
-any p = or . map p
-
-all : (a -> Bool) -> List a -> Bool
-all p = and . map p
+toList : Foldable t => t a -> List a
+toList = foldr (::) []
--------------------------------------------------------------------------------
-- Transformations
diff --git a/lib/Prelude/Maybe.idr b/lib/Prelude/Maybe.idr
--- a/lib/Prelude/Maybe.idr
+++ b/lib/Prelude/Maybe.idr
@@ -3,6 +3,7 @@
import Builtins
import Prelude.Algebra
import Prelude.Cast
+import Prelude.Foldable
%access public
%default total
@@ -81,3 +82,7 @@
instance (Monoid a) => Cast (Maybe a) a where
cast = lowerMaybe
+
+instance Foldable Maybe where
+ foldr _ z Nothing = z
+ foldr f z (Just x) = f x z
diff --git a/lib/Prelude/Nat.idr b/lib/Prelude/Nat.idr
--- a/lib/Prelude/Nat.idr
+++ b/lib/Prelude/Nat.idr
@@ -36,6 +36,19 @@
mult Z right = Z
mult (S left) right = plus right $ mult left right
+%assert_total
+fromIntegerNat : Integer -> Nat
+fromIntegerNat 0 = Z
+fromIntegerNat n =
+ if (n > 0) then
+ S (fromIntegerNat (n - 1))
+ else
+ Z
+
+toIntegerNat : Nat -> Integer
+toIntegerNat Z = 0
+toIntegerNat (S k) = 1 + toIntegerNat k
+
total minus : Nat -> Nat -> Nat
minus Z right = Z
minus left Z = left
@@ -108,8 +121,7 @@
_ == _ = False
instance Cast Nat Integer where
- cast Z = 0
- cast (S k) = 1 + cast k
+ cast = toIntegerNat
instance Ord Nat where
compare Z Z = EQ
@@ -124,16 +136,7 @@
abs x = x
- fromInteger x = fromInteger' x
- where
- %assert_total
- fromInteger' : Integer -> Nat
- fromInteger' 0 = Z
- fromInteger' n =
- if (n > 0) then
- S (fromInteger' (n - 1))
- else
- Z
+ fromInteger = fromIntegerNat
instance Cast Integer Nat where
cast = fromInteger
diff --git a/lib/Prelude/Traversable.idr b/lib/Prelude/Traversable.idr
new file mode 100644
--- /dev/null
+++ b/lib/Prelude/Traversable.idr
@@ -0,0 +1,16 @@
+module Prelude.Traversable
+
+import Prelude.Applicative
+import Prelude.Foldable
+
+traverse_ : (Foldable t, Applicative f) => (a -> f b) -> t a -> f ()
+traverse_ f = foldr (($>) . f) (pure ())
+
+sequence_ : (Foldable t, Applicative f) => t (f a) -> f ()
+sequence_ = foldr ($>) (pure ())
+
+class (Functor t, Foldable t) => Traversable (t : Type -> Type) where
+ traverse : Applicative f => (a -> f b) -> t a -> f (t b)
+
+sequence : (Traversable t, Applicative f) => t (f a) -> f (t a)
+sequence = traverse id
diff --git a/lib/Prelude/Vect.idr b/lib/Prelude/Vect.idr
--- a/lib/Prelude/Vect.idr
+++ b/lib/Prelude/Vect.idr
@@ -1,6 +1,7 @@
module Prelude.Vect
import Prelude.Fin
+import Prelude.Foldable
import Prelude.Functor
import Prelude.List
import Prelude.Nat
@@ -62,13 +63,9 @@
drop (fS k) (x::xs) = drop k xs
--------------------------------------------------------------------------------
--- Conversions to and from list
+-- Conversion from list (toList is provided by Foldable)
--------------------------------------------------------------------------------
-toList : Vect n a -> List a
-toList [] = []
-toList (x::xs) = x :: toList xs
-
fromList : (l : List a) -> Vect (length l) a
fromList [] = []
fromList (x::xs) = x :: fromList xs
@@ -123,13 +120,9 @@
-- Folds
--------------------------------------------------------------------------------
-total foldl : (a -> b -> a) -> a -> Vect m b -> a
-foldl f e [] = e
-foldl f e (x::xs) = foldl f (f e x) xs
-
-total foldr : (a -> b -> b) -> b -> Vect m a -> b
-foldr f e [] = e
-foldr f e (x::xs) = f x (foldr f e xs)
+instance Foldable (Vect n) where
+ foldr f e [] = e
+ foldr f e (x::xs) = f x (foldr f e xs)
--------------------------------------------------------------------------------
-- Special folds
@@ -138,18 +131,6 @@
concat : Vect m (Vect n a) -> Vect (m * n) a
concat [] = []
concat (v::vs) = v ++ concat vs
-
-total and : Vect m Bool -> Bool
-and = foldr (&&) True
-
-total or : Vect m Bool -> Bool
-or = foldr (||) False
-
-total any : (a -> Bool) -> Vect m a -> Bool
-any p = Vect.or . map p
-
-total all : (a -> Bool) -> Vect m a -> Bool
-all p = Vect.and . map p
--------------------------------------------------------------------------------
-- Transformations
diff --git a/lib/Uninhabited.idr b/lib/Uninhabited.idr
--- a/lib/Uninhabited.idr
+++ b/lib/Uninhabited.idr
@@ -1,5 +1,7 @@
module Uninhabited
+import Prelude
+
class Uninhabited t where
total uninhabited : t -> _|_
diff --git a/lib/base.ipkg b/lib/base.ipkg
--- a/lib/base.ipkg
+++ b/lib/base.ipkg
@@ -6,7 +6,8 @@
Prelude.Algebra, Prelude.Cast, Prelude.Nat, Prelude.Fin,
Prelude.List, Prelude.Maybe, Prelude.Monad, Prelude.Applicative,
Prelude.Either, Prelude.Vect, Prelude.Strings, Prelude.Chars,
- Prelude.Heap, Prelude.Complex, Prelude.Functor,
+ Prelude.Heap, Prelude.Complex, Prelude.Functor, Prelude.Foldable,
+ Prelude.Traversable,
Network.Cgi,
Debug.Trace,
diff --git a/llvm/Makefile b/llvm/Makefile
--- a/llvm/Makefile
+++ b/llvm/Makefile
@@ -1,6 +1,6 @@
include ../config.mk
-CFLAGS=-c -O2 -Wall -Wextra -fPIC -Wno-unused-parameter
+CFLAGS:=-Wextra -fPIC -Wno-unused-parameter $(CFLAGS)
SOURCES=defs.c
OBJECTS=$(SOURCES:.c=.o)
LIB=libidris_rts.a
@@ -12,7 +12,7 @@
ranlib $@
.c.o:
- $(CC) $(CFLAGS) $< -o $@
+ $(CC) -c $(CFLAGS) $< -o $@
install: $(LIB) .PHONY
mkdir -p $(TARGET)
diff --git a/rts/Makefile b/rts/Makefile
--- a/rts/Makefile
+++ b/rts/Makefile
@@ -2,8 +2,7 @@
OBJS = idris_rts.o idris_heap.o idris_gc.o idris_gmp.o idris_stdfgn.o idris_bitstring.o idris_opts.o idris_stats.o
HDRS = idris_rts.h idris_heap.h idris_gc.h idris_gmp.h idris_stdfgn.h idris_bitstring.h idris_opts.h idris_stats.h
-CFLAGS = -O2 -Wall -fPIC
-
+CFLAGS:=-fPIC $(CFLAGS)
ifneq ($(GMP_INCLUDE_DIR),)
CFLAGS += -isystem $(GMP_INCLUDE_DIR)
endif
diff --git a/rts/idris_gmp.c b/rts/idris_gmp.c
--- a/rts/idris_gmp.c
+++ b/rts/idris_gmp.c
@@ -10,9 +10,9 @@
VAL MKBIGC(VM* vm, char* val) {
mpz_t* bigint;
- VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*) +
+ VAL cl = allocate(vm, sizeof(Closure) +
sizeof(mpz_t), 0);
- bigint = (mpz_t*)(((char*)cl) + sizeof(ClosureType) + sizeof(void*));
+ bigint = (mpz_t*)(((char*)cl) + sizeof(Closure));
mpz_init(*bigint);
mpz_set_str(*bigint, val, 10);
@@ -25,9 +25,9 @@
VAL MKBIGM(VM* vm, void* big) {
mpz_t* bigint;
- VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*) +
+ VAL cl = allocate(vm, sizeof(Closure) +
sizeof(mpz_t), 0);
- bigint = (mpz_t*)(((char*)cl) + sizeof(ClosureType) + sizeof(void*));
+ bigint = (mpz_t*)(((char*)cl) + sizeof(Closure));
mpz_init(*bigint);
mpz_set(*bigint, *((mpz_t*)big));
@@ -40,9 +40,9 @@
VAL MKBIGMc(VM* vm, void* big) {
mpz_t* bigint;
- VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*) +
+ VAL cl = allocate(vm, sizeof(Closure) +
sizeof(mpz_t), 0);
- bigint = (mpz_t*)(((char*)cl) + sizeof(ClosureType) + sizeof(void*));
+ bigint = (mpz_t*)(((char*)cl) + sizeof(Closure));
mpz_init_set(*bigint, *((mpz_t*)big));
@@ -54,9 +54,8 @@
VAL MKBIGUI(VM* vm, unsigned long val) {
mpz_t* bigint;
- VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*) +
- sizeof(mpz_t), 0);
- bigint = (mpz_t*)(((char*)cl) + sizeof(ClosureType) + sizeof(void*));
+ VAL cl = allocate(vm, sizeof(Closure) + sizeof(mpz_t), 0);
+ bigint = (mpz_t*)(((char*)cl) + sizeof(Closure));
mpz_init_set_ui(*bigint, val);
@@ -68,9 +67,8 @@
VAL MKBIGSI(VM* vm, signed long val) {
mpz_t* bigint;
- VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*) +
- sizeof(mpz_t), 0);
- bigint = (mpz_t*)(((char*)cl) + sizeof(ClosureType) + sizeof(void*));
+ VAL cl = allocate(vm, sizeof(Closure) + sizeof(mpz_t), 0);
+ bigint = (mpz_t*)(((char*)cl) + sizeof(Closure));
mpz_init_set_si(*bigint, val);
@@ -83,9 +81,8 @@
VAL GETBIG(VM * vm, VAL x) {
if (ISINT(x)) {
mpz_t* bigint;
- VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*) +
- sizeof(mpz_t), 0);
- bigint = (mpz_t*)(((char*)cl) + sizeof(ClosureType) + sizeof(void*));
+ VAL cl = allocate(vm, sizeof(Closure) + sizeof(mpz_t), 0);
+ bigint = (mpz_t*)(((char*)cl) + sizeof(Closure));
mpz_init(*bigint);
mpz_set_si(*bigint, GETINT(x));
@@ -101,9 +98,8 @@
VAL bigAdd(VM* vm, VAL x, VAL y) {
mpz_t* bigint;
- VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*) +
- sizeof(mpz_t), 0);
- bigint = (mpz_t*)(((char*)cl) + sizeof(ClosureType) + sizeof(void*));
+ VAL cl = allocate(vm, sizeof(Closure) + sizeof(mpz_t), 0);
+ bigint = (mpz_t*)(((char*)cl) + sizeof(Closure));
mpz_add(*bigint, GETMPZ(x), GETMPZ(y));
SETTY(cl, BIGINT);
cl -> info.ptr = (void*)bigint;
@@ -112,9 +108,8 @@
VAL bigSub(VM* vm, VAL x, VAL y) {
mpz_t* bigint;
- VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*) +
- sizeof(mpz_t), 0);
- bigint = (mpz_t*)(((char*)cl) + sizeof(ClosureType) + sizeof(void*));
+ VAL cl = allocate(vm, sizeof(Closure) + sizeof(mpz_t), 0);
+ bigint = (mpz_t*)(((char*)cl) + sizeof(Closure));
mpz_sub(*bigint, GETMPZ(x), GETMPZ(y));
SETTY(cl, BIGINT);
cl -> info.ptr = (void*)bigint;
@@ -123,9 +118,8 @@
VAL bigMul(VM* vm, VAL x, VAL y) {
mpz_t* bigint;
- VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*) +
- sizeof(mpz_t), 0);
- bigint = (mpz_t*)(((char*)cl) + sizeof(ClosureType) + sizeof(void*));
+ VAL cl = allocate(vm, sizeof(Closure) + sizeof(mpz_t), 0);
+ bigint = (mpz_t*)(((char*)cl) + sizeof(Closure));
mpz_mul(*bigint, GETMPZ(x), GETMPZ(y));
SETTY(cl, BIGINT);
cl -> info.ptr = (void*)bigint;
@@ -134,9 +128,8 @@
VAL bigDiv(VM* vm, VAL x, VAL y) {
mpz_t* bigint;
- VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*) +
- sizeof(mpz_t), 0);
- bigint = (mpz_t*)(((char*)cl) + sizeof(ClosureType) + sizeof(void*));
+ VAL cl = allocate(vm, sizeof(Closure) + sizeof(mpz_t), 0);
+ bigint = (mpz_t*)(((char*)cl) + sizeof(Closure));
mpz_div(*bigint, GETMPZ(x), GETMPZ(y));
SETTY(cl, BIGINT);
cl -> info.ptr = (void*)bigint;
@@ -145,9 +138,8 @@
VAL bigMod(VM* vm, VAL x, VAL y) {
mpz_t* bigint;
- VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*) +
- sizeof(mpz_t), 0);
- bigint = (mpz_t*)(((char*)cl) + sizeof(ClosureType) + sizeof(void*));
+ VAL cl = allocate(vm, sizeof(Closure) + sizeof(mpz_t), 0);
+ bigint = (mpz_t*)(((char*)cl) + sizeof(Closure));
mpz_mod(*bigint, GETMPZ(x), GETMPZ(y));
SETTY(cl, BIGINT);
cl -> info.ptr = (void*)bigint;
@@ -320,9 +312,8 @@
double val = GETFLOAT(f);
mpz_t* bigint;
- VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*) +
- sizeof(mpz_t), 0);
- bigint = (mpz_t*)(((char*)cl) + sizeof(ClosureType) + sizeof(void*));
+ VAL cl = allocate(vm, sizeof(Closure) + sizeof(mpz_t), 0);
+ bigint = (mpz_t*)(((char*)cl) + sizeof(Closure));
mpz_init_set_d(*bigint, val);
diff --git a/rts/idris_rts.c b/rts/idris_rts.c
--- a/rts/idris_rts.c
+++ b/rts/idris_rts.c
@@ -382,6 +382,7 @@
}
VAL str = MKSTR(vm, line_buf);
+// printf("DBG: %s\n", line_buf);
free(line_buf);
return str;
}
diff --git a/rts/idris_stdfgn.h b/rts/idris_stdfgn.h
--- a/rts/idris_stdfgn.h
+++ b/rts/idris_stdfgn.h
@@ -8,6 +8,8 @@
void* fileOpen(char* f, char* mode);
void fileClose(void* h);
+int fileEOF(void* h);
+int fileError(void* h);
void fputStr(void*h, char* str);
int isNull(void* ptr);
diff --git a/src/Core/CaseTree.hs b/src/Core/CaseTree.hs
--- a/src/Core/CaseTree.hs
+++ b/src/Core/CaseTree.hs
@@ -27,7 +27,9 @@
type SC = SC' Term
data CaseAlt' t = ConCase Name Int [Name] (SC' t)
+ | FnCase Name [Name] (SC' t) -- ^ reflection function
| ConstCase Const (SC' t)
+ | SucCase Name (SC' t)
| DefaultCase (SC' t)
deriving (Show, Eq, Ord, Functor)
{-!
@@ -52,8 +54,13 @@
showA i (ConCase n t args sc)
= show n ++ "(" ++ showSep (", ") (map show args) ++ ") => "
++ show' (i+1) sc
+ showA i (FnCase n args sc)
+ = "FN " ++ show n ++ "(" ++ showSep (", ") (map show args) ++ ") => "
+ ++ show' (i+1) sc
showA i (ConstCase t sc)
= show t ++ " => " ++ show' (i+1) sc
+ showA i (SucCase n sc)
+ = show n ++ "+1 => " ++ show' (i+1) sc
showA i (DefaultCase sc)
= "_ => " ++ show' (i+1) sc
@@ -70,7 +77,9 @@
instance TermSize CaseAlt where
termsize n (ConCase _ _ _ s) = termsize n s
+ termsize n (FnCase _ _ s) = termsize n s
termsize n (ConstCase _ s) = termsize n s
+ termsize n (SucCase _ s) = termsize n s
termsize n (DefaultCase s) = termsize n s
-- simple terms can be inlined trivially - good for primitives in particular
@@ -91,7 +100,9 @@
nu' ps _ = []
nua ps (ConCase n i args sc) = nub (nu' (ps ++ args) sc) \\ args
+ nua ps (FnCase n args sc) = nub (nu' (ps ++ args) sc) \\ args
nua ps (ConstCase _ sc) = nu' ps sc
+ nua ps (SucCase _ sc) = nu' ps sc
nua ps (DefaultCase sc) = nu' ps sc
nut ps (P _ n _) | n `elem` ps = []
@@ -114,7 +125,9 @@
nu' ps _ = []
nua ps (ConCase n i args sc) = nub (nu' (ps ++ args) sc)
+ nua ps (FnCase n args sc) = nub (nu' (ps ++ args) sc)
nua ps (ConstCase _ sc) = nu' ps sc
+ nua ps (SucCase _ sc) = nu' ps sc
nua ps (DefaultCase sc) = nu' ps sc
nut ps (P Ref n _) | n `elem` ps = []
@@ -157,7 +170,9 @@
nu' _ = []
nua (ConCase n i args sc) = nu' sc
+ nua (FnCase n args sc) = nu' sc
nua (ConstCase _ sc) = nu' sc
+ nua (SucCase _ sc) = nu' sc
nua (DefaultCase sc) = nu' sc
data Phase = CompileTime | RunTime
@@ -166,9 +181,10 @@
-- Generate a simple case tree
-- Work Right to Left
-simpleCase :: Bool -> Bool -> Phase -> FC -> [([Name], Term, Term)] ->
+simpleCase :: Bool -> Bool -> Bool ->
+ Phase -> FC -> [([Name], Term, Term)] ->
TC CaseDef
-simpleCase tc cover phase fc cs
+simpleCase tc cover reflect phase fc cs
= sc' tc cover phase fc (filter (\(_, _, r) ->
case r of
Impossible -> False
@@ -179,7 +195,7 @@
sc' tc cover phase fc cs
= let proj = phase == RunTime
pats = map (\ (avs, l, r) ->
- (avs, toPats tc l, (l, r))) cs
+ (avs, toPats reflect tc l, (l, r))) cs
chkPats = mapM chkAccessible pats in
case chkPats of
OK pats ->
@@ -196,34 +212,42 @@
defaultCase False = UnmatchedCase "Error"
chkAccessible (avs, l, c)
- | phase == RunTime = return (l, c)
+ | phase == RunTime || reflect = return (l, c)
| otherwise = do mapM_ (acc l) avs
return (l, c)
acc [] n = Error (Inaccessible n)
acc (PV x : xs) n | x == n = OK ()
acc (PCon _ _ ps : xs) n = acc (ps ++ xs) n
+ acc (PSuc p : xs) n = acc (p : xs) n
acc (_ : xs) n = acc xs n
data Pat = PCon Name Int [Pat]
| PConst Const
| PV Name
+ | PSuc Pat -- special case for n+1 on Integer
+ | PReflected Name [Pat]
| PAny
deriving Show
-- If there are repeated variables, take the *last* one (could be name shadowing
-- in a where clause, so take the most recent).
-toPats :: Bool -> Term -> [Pat]
-toPats tc f = reverse (toPat tc (getArgs f)) where
+toPats :: Bool -> Bool -> Term -> [Pat]
+toPats reflect tc f = reverse (toPat reflect tc (getArgs f)) where
getArgs (App f a) = a : getArgs f
getArgs _ = []
-toPat :: Bool -> [Term] -> [Pat]
-toPat tc tms = evalState (mapM (\x -> toPat' x []) tms) []
+toPat :: Bool -> Bool -> [Term] -> [Pat]
+toPat reflect tc tms = evalState (mapM (\x -> toPat' x []) tms) []
where
toPat' (P (DCon t a) n _) args = do args' <- mapM (\x -> toPat' x []) args
return $ PCon n t args'
+ -- n + 1
+ toPat' (P _ (UN "prim__addBigInt") _)
+ [p, Constant (BI 1)]
+ = do p' <- toPat' p []
+ return $ PSuc p'
-- Typecase
toPat' (P (TCon t a) n _) args | tc
= do args' <- mapM (\x -> toPat' x []) args
@@ -245,6 +269,13 @@
return (PV n)
toPat' (App f a) args = toPat' f (a : args)
toPat' (Constant x) [] = return $ PConst x
+ toPat' (Bind n (Pi t) sc) [] | reflect && noOccurrence n sc
+ = do t' <- toPat' t []
+ sc' <- toPat' sc []
+ return $ PReflected (UN "->") (t':sc':[])
+ toPat' (P _ n _) args | reflect
+ = do args' <- mapM (\x -> toPat' x []) args
+ return $ PReflected n args'
toPat' _ _ = return PAny
fixedN IT8 = "Bits8"
@@ -262,6 +293,8 @@
isVarPat _ = False
isConPat (PCon _ _ _ : ps, _) = True
+isConPat (PReflected _ _ : ps, _) = True
+isConPat (PSuc _ : ps, _) = True
isConPat (PConst _ : ps, _) = True
isConPat _ = False
@@ -319,10 +352,14 @@
varRule vs ms fallthrough
data ConType = CName Name Int -- named constructor
+ | CFn Name -- reflected function name
+ | CSuc -- n+1
| CConst Const -- constant, not implemented yet
+ deriving (Show, Eq)
data Group = ConGroup ConType -- Constructor
[([Pat], Clause)] -- arguments and rest of alternative
+ deriving Show
conRule :: [Name] -> [Clause] -> SC -> State CS SC
conRule (v:vs) cs err = do groups <- groupCons cs
@@ -337,6 +374,14 @@
= do g <- altGroup n i args
rest <- altGroups cs
return (g : rest)
+ altGroups (ConGroup (CFn n) args : cs)
+ = do g <- altFnGroup n args
+ rest <- altGroups cs
+ return (g : rest)
+ altGroups (ConGroup CSuc args : cs)
+ = do g <- altSucGroup args
+ rest <- altGroups cs
+ return (g : rest)
altGroups (ConGroup (CConst c) args : cs)
= do g <- altConstGroup c args
rest <- altGroups cs
@@ -345,6 +390,12 @@
altGroup n i gs = do (newArgs, nextCs) <- argsToAlt gs
matchCs <- match (newArgs ++ vs) nextCs err
return $ ConCase n i newArgs matchCs
+ altFnGroup n gs = do (newArgs, nextCs) <- argsToAlt gs
+ matchCs <- match (newArgs ++ vs) nextCs err
+ return $ FnCase n newArgs matchCs
+ altSucGroup gs = do ([newArg], nextCs) <- argsToAlt gs
+ matchCs <- match (newArg:vs) nextCs err
+ return $ SucCase newArg matchCs
altConstGroup n gs = do (_, nextCs) <- argsToAlt gs
matchCs <- match vs nextCs err
return $ ConstCase n matchCs
@@ -382,19 +433,23 @@
do acc' <- addGroup p ps res acc
gc acc' cs
addGroup p ps res acc = case p of
- PCon con i args -> return $ addg con i args (ps, res) acc
+ PCon con i args -> return $ addg (CName con i) args (ps, res) acc
PConst cval -> return $ addConG cval (ps, res) acc
+ PSuc n -> return $ addg CSuc [n] (ps, res) acc
+ PReflected fn args -> return $ addg (CFn fn) args (ps, res) acc
pat -> fail $ show pat ++ " is not a constructor or constant (can't happen)"
- addg con i conargs res [] = [ConGroup (CName con i) [(conargs, res)]]
- addg con i conargs res (g@(ConGroup (CName n j) cs):gs)
- | i == j = ConGroup (CName n i) (cs ++ [(conargs, res)]) : gs
- | otherwise = g : addg con i conargs res gs
+ addg c conargs res []
+ = [ConGroup c [(conargs, res)]]
+ addg c conargs res (g@(ConGroup c' cs):gs)
+ | c == c' = ConGroup c (cs ++ [(conargs, res)]) : gs
+ | otherwise = g : addg c conargs res gs
addConG con res [] = [ConGroup (CConst con) [([], res)]]
addConG con res (g@(ConGroup (CConst n) cs) : gs)
| con == n = ConGroup (CConst n) (cs ++ [([], res)]) : gs
- | otherwise = g : addConG con res gs
+-- | otherwise = g : addConG con res gs
+ addConG con res (g : gs) = g : addConG con res gs
varRule :: [Name] -> [Clause] -> SC -> State CS SC
varRule (v : vs) alts err =
@@ -416,7 +471,10 @@
dpa ms x (ConCase n i args sc)
= ConCase n i args (dp ((x, (n, args)) : ms) sc)
+ dpa ms x (FnCase n args sc)
+ = FnCase n args (dp ((x, (n, args)) : ms) sc)
dpa ms x (ConstCase c sc) = ConstCase c (dp ms sc)
+ dpa ms x (SucCase n sc) = SucCase n (dp ms sc)
dpa ms x (DefaultCase sc) = DefaultCase (dp ms sc)
applyMaps ms f@(App _ _)
@@ -443,9 +501,15 @@
[] -> ImpossibleCase
as@[ConCase cn i args sc] -> if proj then mkProj n 0 args sc
else Case n as
+ -- Bit of a hack here! The default case will always be 0, make sure
+ -- it gets caught first.
+ [s@(SucCase _ _), DefaultCase dc]
+ -> Case n [ConstCase (BI 0) dc, s]
as -> Case n as
where pruneAlt (ConCase cn i ns sc) = ConCase cn i ns (prune proj sc)
+ pruneAlt (FnCase cn ns sc) = FnCase cn ns (prune proj sc)
pruneAlt (ConstCase c sc) = ConstCase c (prune proj sc)
+ pruneAlt (SucCase n sc) = SucCase n (prune proj sc)
pruneAlt (DefaultCase sc) = DefaultCase (prune proj sc)
notErased (DefaultCase (STerm Erased)) = False
@@ -467,8 +531,12 @@
projRepAlt arg n i (ConCase cn t args rhs)
= ConCase cn t args (projRep arg n i rhs)
+ projRepAlt arg n i (FnCase cn args rhs)
+ = FnCase cn args (projRep arg n i rhs)
projRepAlt arg n i (ConstCase t rhs)
= ConstCase t (projRep arg n i rhs)
+ projRepAlt arg n i (SucCase sn rhs)
+ = SucCase sn (projRep arg n i rhs)
projRepAlt arg n i (DefaultCase rhs)
= DefaultCase (projRep arg n i rhs)
diff --git a/src/Core/CoreParser.hs b/src/Core/CoreParser.hs
--- a/src/Core/CoreParser.hs
+++ b/src/Core/CoreParser.hs
@@ -35,6 +35,7 @@
"where", "with", "syntax", "proof", "postulate",
"using", "namespace", "class", "instance",
"public", "private", "abstract", "implicit",
+ "quoteGoal",
"Int", "Integer", "Float", "Char", "String", "Ptr",
"Bits8", "Bits16", "Bits32", "Bits64",
"Bits8x16", "Bits16x8", "Bits32x4", "Bits64x2"]
diff --git a/src/Core/Elaborate.hs b/src/Core/Elaborate.hs
--- a/src/Core/Elaborate.hs
+++ b/src/Core/Elaborate.hs
@@ -59,6 +59,15 @@
Just st -> put st
_ -> fail "Nothing to undo"
+errAt :: String -> Name -> Elab' aux a -> Elab' aux a
+errAt thing n elab = do s <- get
+ case runStateT elab s of
+ OK (a, s') -> do put s'
+ return a
+ Error (At f e) ->
+ lift $ Error (At f (Elaborating thing n e))
+ Error e -> lift $ Error (Elaborating thing n e)
+
erun :: FC -> Elab' aux a -> Elab' aux a
erun f elab = do s <- get
case runStateT elab s of
@@ -263,6 +272,9 @@
compute :: Elab' aux ()
compute = processTactic' Compute
+computeLet :: Name -> Elab' aux ()
+computeLet n = processTactic' (ComputeLet n)
+
simplify :: Elab' aux ()
simplify = processTactic' Simplify
@@ -382,6 +394,7 @@
mkMN n@(MN _ _) = n
mkMN n@(UN x) = MN 1000 x
+ mkMN n@(SN s) = MN 1000 (show s)
mkMN (NS n xs) = NS (mkMN n) xs
rebind hs (Bind n t sc)
diff --git a/src/Core/Evaluate.hs b/src/Core/Evaluate.hs
--- a/src/Core/Evaluate.hs
+++ b/src/Core/Evaluate.hs
@@ -3,12 +3,13 @@
module Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,
simplify, specialise, hnf, convEq, convEq',
- Def(..), Accessibility(..), Totality(..), PReason(..),
+ Def(..), CaseInfo(..), CaseDefs(..),
+ Accessibility(..), Totality(..), PReason(..),
Context, initContext, ctxtAlist, uconstraints, next_tvar,
addToCtxt, setAccess, setTotal, addCtxtDef, addTyDecl,
addDatatype, addCasedef, simplifyCasedef, addOperator,
lookupNames, lookupTy, lookupP, lookupDef, lookupVal,
- lookupTotal, lookupTyEnv, isConName, isFnName,
+ lookupTotal, lookupTyEnv, isDConName, isTConName, isConName, isFnName,
Value(..), Quote(..), evalState, initEval) where
import Debug.Trace
@@ -24,7 +25,10 @@
type Eval a = State EvalState a
-data EvalOpt = Spec | HNF | Simplify Bool | AtREPL
+data EvalOpt = Spec
+ | HNF
+ | Simplify
+ | AtREPL
deriving (Show, Eq)
initEval = ES [] 0
@@ -44,15 +48,6 @@
-- | VLazy Env [Value] Term
| VTmp Int
-data HNF = HP NameType Name (TT Name)
- | HV Int
- | HBind Name (Binder HNF) (HNF -> Eval HNF)
- | HApp HNF [HNF] [TT Name]
- | HType UExp
- | HConstant Const
- | HTmp Int
- deriving Show
-
instance Show Value where
show x = show $ evalState (quote 100 x) initEval
@@ -94,14 +89,18 @@
-- | Like normalise, but we only reduce functions that are marked as okay to
-- inline (and probably shouldn't reduce lets?)
-simplify :: Context -> Bool -> Env -> TT Name -> TT Name
-simplify ctxt runtime env t
+-- 20130908: now only used to reduce for totality checking. Inlining should
+-- be done elsewhere.
+
+simplify :: Context -> Env -> TT Name -> TT Name
+simplify ctxt env t
= evalState (do val <- eval False ctxt [(UN "lazy", 0),
(UN "assert_smaller", 0),
(UN "par", 0),
+ (UN "prim__syntactic_eq", 0),
(UN "fork", 0)]
(map finalEntry env) (finalise t)
- [Simplify runtime]
+ [Simplify]
quote 0 val) initEval
-- | Reduce a term to head normal form
@@ -127,22 +126,21 @@
unbindEnv [] tm = tm
unbindEnv (_:bs) (Bind n b sc) = unbindEnv bs sc
-usable :: Bool -> Bool -> Name -> [(Name, Int)] -> Eval (Bool, [(Name, Int)])
-usable _ _ _ ns@((MN 0 "STOP", _) : _) = return (False, ns)
-usable True _ (UN "io_bind") ns = return (False, ns)
-usable simpl False n [] = return (True, [])
-usable simpl True n ns
+usable :: Bool -- specialising
+ -> Name -> [(Name, Int)] -> Eval (Bool, [(Name, Int)])
+-- usable _ _ ns@((MN 0 "STOP", _) : _) = return (False, ns)
+usable False n [] = return (True, [])
+usable True n ns
= do ES ls num <- get
case lookup n ls of
Just 0 -> return (False, ns)
Just i -> return (True, ns)
_ -> return (False, ns)
-usable simpl False n ns
+usable False n ns
= case lookup n ns of
Just 0 -> return (False, ns)
Just i -> return $ (True, (n, abs (i-1)) : filter (\ (n', _) -> n/=n') ns)
- _ -> if simpl then return $ (True, (n, 0) : filter (\ (n', _) -> n/=n') ns)
- else return $ (True, (n, 100) : filter (\ (n', _) -> n/=n') ns)
+ _ -> return $ (True, (n, 100) : filter (\ (n', _) -> n/=n') ns)
deduct :: Name -> Eval ()
@@ -163,20 +161,24 @@
[EvalOpt] -> Eval Value
eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
spec = Spec `elem` opts
- simpl = Simplify True `elem` opts
+ simpl = Simplify `elem` opts
atRepl = AtREPL `elem` opts
hnf = HNF `elem` opts
- canSimplify inl inr n stk
- = (Simplify False `elem` opts && (not inl || elem n stk))
- || (Simplify True `elem` opts && (not inr || elem n stk))
+ -- returns 'True' if the function should block
+ -- normal evaluation should return false
+ blockSimplify (CaseInfo inl dict) n stk
+ | Simplify `elem` opts
+ = (not (inl || dict) || elem n stk)
+ || (n == UN "prim__syntactic_eq")
+ | otherwise = False
ev ntimes stk top env (P _ n ty)
| Just (Let t v) <- lookup n genv = ev ntimes stk top env v
ev ntimes_in stk top env (P Ref n ty)
| not top && hnf = liftM (VP Ref n) (ev ntimes stk top env ty)
| otherwise
- = do (u, ntimes) <- usable simpl spec n ntimes_in
+ = do (u, ntimes) <- usable spec n ntimes_in
if u then
do let val = lookupDefAcc n atRepl ctxt
case val of
@@ -184,9 +186,12 @@
ev ntimes (n:stk) True env tm
[(TyDecl nt ty, _)] -> do vty <- ev ntimes stk True env ty
return $ VP nt n vty
- [(CaseOp inl inr _ _ _ [] tree _ _, acc)]
- | acc == Public || simpl -> -- unoptimised version
- if canSimplify inl inr n stk
+ [(CaseOp ci _ _ _ cd, acc)]
+ | acc == Public &&
+ null (fst (cases_totcheck cd)) -> -- unoptimised version
+ let (_, tree) = if simpl then cases_totcheck cd
+ else cases_compiletime cd in
+ if blockSimplify ci n stk
then liftM (VP Ref n) (ev ntimes stk top env ty)
else do c <- evCase ntimes n (n:stk) top env [] [] tree
case c of
@@ -200,20 +205,19 @@
| i < length env && i >= 0 = return $ env !! i
| otherwise = return $ VV i
ev ntimes stk top env (Bind n (Let t v) sc)
- | not simpl -- - || vinstances 0 sc < 2
= do v' <- ev ntimes stk top env v --(finalise v)
sc' <- ev ntimes stk top (v' : env) sc
wknV (-1) sc'
- | otherwise
- = do t' <- ev ntimes stk top env t
- v' <- ev ntimes stk top env v --(finalise v)
- -- use Tmp as a placeholder, then make it a variable reference
- -- again when evaluation finished
- hs <- get
- let vd = nexthole hs
- put (hs { nexthole = vd + 1 })
- sc' <- ev ntimes stk top (VP Bound (MN vd "vlet") VErased : env) sc
- return $ VBLet vd n t' v' sc'
+-- | otherwise
+-- = do t' <- ev ntimes stk top env t
+-- v' <- ev ntimes stk top env v --(finalise v)
+-- -- use Tmp as a placeholder, then make it a variable reference
+-- -- again when evaluation finished
+-- hs <- get
+-- let vd = nexthole hs
+-- put (hs { nexthole = vd + 1 })
+-- sc' <- ev ntimes stk top (VP Bound (MN vd "vlet") VErased : env) sc
+-- return $ VBLet vd n t' v' sc'
ev ntimes stk top env (Bind n (NLet t v) sc)
= do t' <- ev ntimes stk top env (finalise t)
v' <- ev ntimes stk top env (finalise v)
@@ -221,17 +225,14 @@
return $ VBind True n (Let t' v') (\x -> return sc')
ev ntimes stk top env (Bind n b sc)
= do b' <- vbind env b
- return $ VBind (not simpl || vinstances 0 sc < 2)
+ return $ VBind True -- (vinstances 0 sc < 2)
n b' (\x -> ev ntimes stk False (x:env) sc)
where vbind env t
- | simpl
- = fmapMB (\tm -> ev ((MN 0 "STOP", 0) : ntimes)
- stk top env (finalise tm)) t
- | otherwise
+-- | simpl
+-- = fmapMB (\tm -> ev ((MN 0 "STOP", 0) : ntimes)
+-- stk top env (finalise tm)) t
+-- | otherwise
= fmapMB (\tm -> ev ntimes stk top env (finalise tm)) t
--- ev ntimes stk top env (App (App (P _ laz _) _) a)
--- | laz == UN "lazy"
--- = trace (showEnvDbg genv a) $ ev ntimes stk top env a
ev ntimes stk top env (App f a)
= do f' <- ev ntimes stk False env f
a' <- ev ntimes stk False env a
@@ -240,28 +241,29 @@
ev ntimes stk top env Erased = return VErased
ev ntimes stk top env (TType i) = return $ VType i
- evApply ntimes stk top env args (VApp f a) =
- evApply ntimes stk top env (a:args) f
- evApply ntimes stk top env args f = apply ntimes stk top env f args
+ evApply ntimes stk top env args (VApp f a)
+ = evApply ntimes stk top env (a:args) f
+ evApply ntimes stk top env args f
+ = apply ntimes stk top env f args
apply ntimes stk top env (VBind True n (Lam t) sc) (a:as)
= do a' <- sc a
app <- apply ntimes stk top env a' as
wknV (-1) app
--- apply ntimes stk False env f args
--- | spec = specApply ntimes stk env f args
apply ntimes_in stk top env f@(VP Ref n ty) args
| not top && hnf = case args of
[] -> return f
_ -> return $ unload env f args
| otherwise
- = do (u, ntimes) <- usable simpl spec n ntimes_in
+ = do (u, ntimes) <- usable spec n ntimes_in
if u then
do let val = lookupDefAcc n atRepl ctxt
case val of
- [(CaseOp inl inr _ _ _ ns tree _ _, acc)]
+ [(CaseOp ci _ _ _ cd, acc)]
| acc == Public -> -- unoptimised version
- if canSimplify inl inr n stk
+ let (ns, tree) = if simpl then cases_totcheck cd
+ else cases_compiletime cd in
+ if blockSimplify ci n stk
then return $ unload env (VP Ref n ty) args
else do c <- evCase ntimes n (n:stk) top env ns args tree
case c of
@@ -291,6 +293,7 @@
-- _ -> return $ unload env f args
-- specApply stk env f args = return $ unload env f args
+ unload :: [Value] -> Value -> [Value] -> Value
unload env f [] = f
unload env f (a:as) = unload env (VApp f a) as
@@ -299,8 +302,8 @@
= do let args' = take (length ns) args
let rest = drop (length ns) args
when spec $ deduct n -- successful, so deduct usages
- t <- evTree ntimes stk top env
- (zipWith (\n t -> (n, t)) ns args') tree
+ t <- evTree ntimes stk top env (zip ns args') tree
+-- (zipWith (\n , t) -> (n, t)) ns args') tree
return (t, rest)
| otherwise = return (Nothing, args)
@@ -330,21 +333,40 @@
chooseAlt' ntimes stk env _ (f, args) alts amap
= do f' <- apply ntimes stk True env f args
- chooseAlt env f' (getValArgs f') alts amap
+ chooseAlt env f' (getValArgs f')
+ alts amap
- chooseAlt :: [Value] -> Value -> (Value, [Value]) -> [CaseAlt] -> [(Name, Value)] ->
+ chooseAlt :: [Value] -> Value -> (Value, [Value]) -> [CaseAlt] ->
+ [(Name, Value)] ->
Eval (Maybe ([(Name, Value)], SC))
chooseAlt env _ (VP (DCon i a) _ _, args) alts amap
| Just (ns, sc) <- findTag i alts = return $ Just (updateAmap (zip ns args) amap, sc)
| Just v <- findDefault alts = return $ Just (amap, v)
chooseAlt env _ (VP (TCon i a) _ _, args) alts amap
- | Just (ns, sc) <- findTag i alts = return $ Just (updateAmap (zip ns args) amap, sc)
+ | Just (ns, sc) <- findTag i alts
+ = return $ Just (updateAmap (zip ns args) amap, sc)
| Just v <- findDefault alts = return $ Just (amap, v)
chooseAlt env _ (VConstant c, []) alts amap
| Just v <- findConst c alts = return $ Just (amap, v)
+ | Just (n', sub, sc) <- findSuc c alts
+ = return $ Just (updateAmap [(n',sub)] amap, sc)
| Just v <- findDefault alts = return $ Just (amap, v)
- chooseAlt _ _ _ _ _ = return Nothing
+ chooseAlt env _ (VP _ n _, args) alts amap
+ | Just (ns, sc) <- findFn n alts = return $ Just (updateAmap (zip ns args) amap, sc)
+ chooseAlt env _ (VBind _ _ (Pi s) t, []) alts amap
+ | Just (ns, sc) <- findFn (UN "->") alts
+ = do t' <- t (VV 0) -- we know it's not in scope or it's not a pattern
+ return $ Just (updateAmap (zip ns [s, t']) amap, sc)
+ chooseAlt _ _ _ alts amap
+ | Just v <- findDefault alts
+ = if (any fnCase alts)
+ then return $ Just (amap, v)
+ else return Nothing
+ | otherwise = return Nothing
+ fnCase (FnCase _ _ _) = True
+ fnCase _ = False
+
-- Replace old variable names in the map with new matches
-- (This is possibly unnecessary since we make unique names and don't
-- allow repeated variables...?)
@@ -354,10 +376,19 @@
findTag i (ConCase n j ns sc : xs) | i == j = Just (ns, sc)
findTag i (_ : xs) = findTag i xs
+ findFn fn [] = Nothing
+ findFn fn (FnCase n ns sc : xs) | fn == n = Just (ns, sc)
+ findFn fn (_ : xs) = findFn fn xs
+
findDefault [] = Nothing
findDefault (DefaultCase sc : xs) = Just sc
findDefault (_ : xs) = findDefault xs
+ findSuc c [] = Nothing
+ findSuc (BI val) (SucCase n sc : _)
+ | val /= 0 = Just (n, VConstant (BI (val - 1)), sc)
+ findSuc c (_ : xs) = findSuc c xs
+
findConst c [] = Nothing
findConst c (ConstCase c' v : xs) | c == c' = Just v
findConst (AType (ATInt ITNative)) (ConCase n 1 [] v : xs) = Just v
@@ -385,6 +416,10 @@
-- tmpToV i vd (VApp f a) = liftM2 VApp (tmpToV i vd f) (tmpToV i vd a)
-- tmpToV i vd x = return x
+instance Eq Value where
+ (==) x y = getTT x == getTT y
+ where getTT v = evalState (quote 0 v) initEval
+
class Quote a where
quote :: Int -> a -> Eval (TT Name)
@@ -407,23 +442,6 @@
quote i (VConstant c) = return $ Constant c
quote i (VTmp x) = return $ V (i - x - 1)
-instance Quote HNF where
- quote i (HP nt n t) = return (P nt n t)
- quote i (HV x) = return $ V x
- quote i (HBind n b sc) = do sc' <- sc (HTmp i)
- b' <- quoteB b
- liftM (Bind n b') (quote (i+1) sc')
- where quoteB t = fmapMB (quote i) t
- quote i (HApp f env as) = do f' <- quote i f
- as' <- mapM (iEnv env) as
- return $ mkApp f' as'
- where iEnv [] a = return a
- iEnv (x:xs) a = do x' <- quote i x
- iEnv xs (weakenTm (-1) (instantiate x' a))
- quote i (HType u) = return $ TType u
- quote i (HConstant c) = return $ Constant c
- quote i (HTmp x) = return $ V (i - x - 1)
-
wknV :: Int -> Value -> Eval Value
wknV i (VV x) = return $ VV (x + i)
wknV i (VBind red n b sc) = do b' <- fmapMB (wknV i) b
@@ -432,142 +450,6 @@
wknV i (VApp f a) = liftM2 VApp (wknV i f) (wknV i a)
wknV i t = return t
-wknH :: Int -> HNF -> Eval HNF
-wknH i (HV x) = return $ HV (x + i)
-wknH i (HBind n b sc) = do b' <- fmapMB (wknH i) b
- return $ HBind n b' (\x -> do x' <- sc x
- wknH i x')
-wknH i (HApp f env as) = liftM3 HApp (wknH i f) (return env)
- (return as)
-wknH i t = return t
-
--- HEAD NORMAL FORM ---------------------------------------------------------
-
-eval_hnf :: Context -> Ctxt [Bool] -> Env -> TT Name -> Eval HNF
-eval_hnf ctxt statics genv tm = ev [] tm where
- ev :: [HNF] -> TT Name -> Eval HNF
- ev env (P _ n ty)
- | Just (Let t v) <- lookup n genv = ev env v
- ev env (P Ref n ty) = case lookupDef n ctxt of
- [Function _ t] -> ev env t
- [TyDecl nt ty] -> return $ HP nt n ty
- [CaseOp inl _ _ _ _ [] tree _ _] ->
- do c <- evCase env [] [] tree
- case c of
- (Nothing, _, _) -> return $ HP Ref n ty
- (Just v, _, _) -> return v
- _ -> return $ HP Ref n ty
- ev env (P nt n ty) = return $ HP nt n ty
- ev env (V i) | i < length env = return $ env !! i
- | otherwise = return $ HV i
- ev env (Bind n (Let t v) sc)
- = do v' <- ev env (finalise v)
- sc' <- ev (v' : env) sc
- wknH (-1) sc'
- ev env (Bind n b sc)
- = do b' <- hbind env b
- return $ HBind n b' (\x -> ev (x : env) sc)
- where hbind env t = fmapMB (\tm -> ev env (finalise tm)) t
- ev env (App f a) = evApply env [a] f
- ev env (Constant c) = return $ HConstant c
- ev env (TType i) = return $ HType i
-
- evApply env args (App f a) = evApply env (a : args) f
- evApply env args f = do f' <- ev env f
- apply env f' args
-
- apply env (HBind n (Lam t) sc) (a:as) = do a' <- ev env a
- sc' <- sc a'
- app <- apply env sc' as
- wknH (-1) app
- apply env (HP Ref n ty) args
- | [CaseOp _ _ _ _ _ ns tree _ _] <- lookupDef n ctxt
- = do c <- evCase env ns args tree
- case c of
- (Nothing, _, env') -> return $ unload env' (HP Ref n ty) args
- (Just v, rest, env') -> do v' <- quote 0 v
- apply env' v rest
--- | Just (Operator _ i op) <- lookupDef n ctxt
--- = if (i <= length args)
--- then case op (take i args) of
--- Nothing -> return $ unload env (HP Ref n ty) args
--- Just v -> evApply env (drop i args) v
--- else return $ unload env (HP Ref n ty) args
- apply env f (a:as) = return $ unload env f (a:as)
- apply env f [] = return f
-
- unload env f [] = f
- unload env f as = HApp f env as
-
- evCase env ns args tree
- | length ns <= length args
- = do let args' = take (length ns) args
- let rest = drop (length ns) args
- (t, env') <- evTree env (zipWith (\n t -> (n, t)) ns args') tree
- return (t, rest, env')
- | otherwise = return (Nothing, args, env)
-
- evTree :: [HNF] -> [(Name, TT Name)] -> SC -> Eval (Maybe HNF, [HNF])
- evTree env amap (UnmatchedCase str) = return (Nothing, env)
- evTree env amap (STerm tm)
- = do let etm = pToVs (map fst amap) tm
- amap' <- mapM (ev env) (map snd amap)
- envw <- mapM (wknH (length amap)) env
- let env' = amap' ++ envw
- etm' <- trace (show etm) $ ev env' etm
- etmq <- quote 0 etm'
- trace ("Ev: " ++ show (etm, etmq)) $ return $ (Just etm', env')
- evTree env amap (Case n alts)
- = case lookup n amap of
- Just v -> do v' <- ev env v
- case chooseAlt v' (getValArgs v') alts amap of
- Just (altmap, sc) -> evTree env altmap sc
- _ -> return (Nothing, env)
-
- chooseAlt :: HNF -> (HNF, [HNF], [TT Name]) ->
- [CaseAlt] -> [(Name, TT Name)] ->
- Maybe ([(Name, TT Name)], SC)
- chooseAlt _ (HP (DCon i a) _ _, env, args) alts amap
- | Just (ns, sc) <- findTag i alts = Just (updateAmap (zip ns args) amap, sc)
- | Just v <- findDefault alts = Just (amap, v)
- chooseAlt _ (HP (TCon i a) _ _, env, args) alts amap
- | Just (ns, sc) <- findTag i alts = Just (updateAmap (zip ns args) amap, sc)
- | Just v <- findDefault alts = Just (amap, v)
- chooseAlt _ (HConstant c, env, []) alts amap
- | Just v <- findConst c alts = Just (amap, v)
- | Just v <- findDefault alts = Just (amap, v)
- chooseAlt _ _ _ _ = Nothing
-
- -- Replace old variable names in the map with new matches
- -- (This is possibly unnecessary since we make unique names and don't
- -- allow repeated variables...?)
- updateAmap newm amap
- = newm ++ filter (\ (x, _) -> not (elem x (map fst newm))) amap
- findTag i [] = Nothing
- findTag i (ConCase n j ns sc : xs) | i == j = Just (ns, sc)
- findTag i (_ : xs) = findTag i xs
-
- findDefault [] = Nothing
- findDefault (DefaultCase sc : xs) = Just sc
- findDefault (_ : xs) = findDefault xs
-
- findConst c [] = Nothing
- findConst c (ConstCase c' v : xs) | c == c' = Just v
- findConst (AType (ATInt ITNative)) (ConCase n 1 [] v : xs) = Just v
- findConst (AType ATFloat) (ConCase n 2 [] v : xs) = Just v
- findConst (AType (ATInt ITChar)) (ConCase n 3 [] v : xs) = Just v
- findConst StrType (ConCase n 4 [] v : xs) = Just v
- findConst PtrType (ConCase n 5 [] v : xs) = Just v
- findConst (AType (ATInt ITBig)) (ConCase n 6 [] v : xs) = Just v
- findConst (AType (ATInt (ITFixed ity))) (ConCase n tag [] v : xs)
- | tag == 7 + fromEnum ity = Just v
- findConst (AType (ATInt (ITVec ity count))) (ConCase n tag [] v : xs)
- | tag == (fromEnum ity + 1) * 1000 + count = Just v
- findConst c (_ : xs) = findConst c xs
-
- getValArgs (HApp t env args) = (t, env, args)
- getValArgs t = (t, [], [])
-
convEq' ctxt x y = evalStateT (convEq ctxt x y) (0, [])
convEq :: Context -> TT Name -> TT Name -> StateT UCs TC Bool
@@ -619,9 +501,11 @@
sameDefs ps x y = case (lookupDef x ctxt, lookupDef y ctxt) of
([Function _ xdef], [Function _ ydef])
-> ceq ((x,y):ps) xdef ydef
- ([CaseOp _ _ _ _ _ _ xdef _ _],
- [CaseOp _ _ _ _ _ _ ydef _ _])
- -> caseeq ((x,y):ps) xdef ydef
+ ([CaseOp _ _ _ _ xd],
+ [CaseOp _ _ _ _ yd])
+ -> let (_, xdef) = cases_compiletime xd
+ (_, ydef) = cases_compiletime yd in
+ caseeq ((x,y):ps) xdef ydef
_ -> return False
-- SPECIALISATION -----------------------------------------------------------
@@ -642,24 +526,51 @@
data Def = Function Type Term
| TyDecl NameType Type
| Operator Type Int ([Value] -> Maybe Value)
- | CaseOp Bool Bool -- compile-time/run-time inlinable
+ | CaseOp CaseInfo
Type
[Either Term (Term, Term)] -- original definition
- [([Name], Term, Term)] -- simplified definition
- [Name] SC -- Compile time case definition
- [Name] SC -- Run time cae definitions
+ [([Name], Term, Term)] -- simplified for totality check definition
+ CaseDefs
+-- [Name] SC -- Compile time case definition
+-- [Name] SC -- Run time cae definitions
+
+data CaseDefs = CaseDefs {
+ cases_totcheck :: ([Name], SC),
+ cases_compiletime :: ([Name], SC),
+ cases_inlined :: ([Name], SC),
+ cases_runtime :: ([Name], SC)
+ }
+
+data CaseInfo = CaseInfo {
+ case_inlinable :: Bool,
+ tc_dictionary :: Bool
+ }
+
{-!
deriving instance Binary Def
!-}
+{-!
+deriving instance Binary CaseInfo
+!-}
+{-!
+deriving instance Binary CaseDefs
+!-}
instance Show Def where
show (Function ty tm) = "Function: " ++ show (ty, tm)
show (TyDecl nt ty) = "TyDecl: " ++ show nt ++ " " ++ show ty
show (Operator ty _ _) = "Operator: " ++ show ty
- show (CaseOp inlc inlr ty ps_in ps ns sc ns' sc')
- = "Case: " ++ show ty ++ " " ++ show ps ++ "\n" ++
- show ns ++ " " ++ show sc ++ "\n" ++
- show ns' ++ " " ++ show sc' ++ "\n" ++
+ show (CaseOp (CaseInfo inlc inlr) ty ps_in ps cd)
+ = let (ns, sc) = cases_compiletime cd
+ (ns_t, sc_t) = cases_totcheck cd
+ (ns', sc') = cases_runtime cd in
+ "Case: " ++ show ty ++ " " ++ show ps ++ "\n" ++
+ "TOTALITY CHECK TIME:\n\n" ++
+ show ns_t ++ " " ++ show sc_t ++ "\n\n" ++
+ "COMPILE TIME:\n\n" ++
+ show ns ++ " " ++ show sc ++ "\n\n" ++
+ "RUN TIME:\n\n" ++
+ show ns' ++ " " ++ show sc' ++ "\n\n" ++
if inlc then "Inlinable\n" else "Not inlinable\n"
-- We need this for serialising Def. Fortunately, it never gets used because
@@ -774,41 +685,57 @@
addCons (tag+1) cons (addDef n
(TyDecl (DCon tag (arity ty')) ty, Public, Unchecked) ctxt)
-addCasedef :: Name -> Bool -> Bool -> Bool -> Bool ->
+-- FIXME: Too many arguments! Refactor all these Bools.
+addCasedef :: Name -> CaseInfo -> Bool -> Bool -> Bool -> Bool ->
[Either Term (Term, Term)] ->
- [([Name], Term, Term)] ->
- [([Name], Term, Term)] ->
+ [([Name], Term, Term)] -> -- totality
+ [([Name], Term, Term)] -> -- compile time
+ [([Name], Term, Term)] -> -- inlined
+ [([Name], Term, Term)] -> -- run time
Type -> Context -> Context
-addCasedef n alwaysInline tcase covering asserted ps_in ps psrt ty uctxt
+addCasedef n ci@(CaseInfo alwaysInline tcdict)
+ tcase covering reflect asserted ps_in
+ ps_tot ps_inl ps_ct ps_rt ty uctxt
= let ctxt = definitions uctxt
access = case lookupDefAcc n False uctxt of
[(_, acc)] -> acc
_ -> Public
- ctxt' = case (simpleCase tcase covering CompileTime (FC "" 0) ps,
- simpleCase tcase covering RunTime (FC "" 0) psrt) of
- (OK (CaseDef args sc _), OK (CaseDef args' sc' _)) ->
- let inl = alwaysInline
- inlc = (inl || small n args sc') && (not asserted)
- inlr = inl || small n args sc' in
- addDef n (CaseOp inlc inlr
- ty ps_in ps args sc args' sc',
+ ctxt' = case (simpleCase tcase covering reflect CompileTime (FC "" 0) ps_tot,
+ simpleCase tcase covering reflect CompileTime (FC "" 0) ps_ct,
+ simpleCase tcase covering reflect CompileTime (FC "" 0) ps_inl,
+ simpleCase tcase covering reflect RunTime (FC "" 0) ps_rt) of
+ (OK (CaseDef args_tot sc_tot _),
+ OK (CaseDef args_ct sc_ct _),
+ OK (CaseDef args_inl sc_inl _),
+ OK (CaseDef args_rt sc_rt _)) ->
+ let inl = alwaysInline -- || tcdict
+ inlc = (inl || small n args_ct sc_ct) && (not asserted)
+ inlr = inl || small n args_rt sc_rt
+ cdef = CaseDefs (args_tot, sc_tot)
+ (args_ct, sc_ct)
+ (args_inl, sc_inl)
+ (args_rt, sc_rt) in
+ addDef n (CaseOp (ci { case_inlinable = inlc })
+ ty ps_in ps_tot cdef,
access, Unchecked) ctxt in
uctxt { definitions = ctxt' }
+-- simplify a definition for totality checking
simplifyCasedef :: Name -> Context -> Context
simplifyCasedef n uctxt
= let ctxt = definitions uctxt
ctxt' = case lookupCtxt n ctxt of
- [(CaseOp inl inr ty [] ps args sc args' sc', acc, tot)] ->
+ [(CaseOp ci ty [] ps _, acc, tot)] ->
ctxt -- nothing to simplify (or already done...)
- [(CaseOp inl inr ty ps_in ps args sc args' sc', acc, tot)] ->
+ [(CaseOp ci ty ps_in ps cd, acc, tot)] ->
let ps_in' = map simpl ps_in
pdef = map debind ps_in' in
- case simpleCase False True CompileTime (FC "" 0) pdef of
+ case simpleCase False True False CompileTime (FC "" 0) pdef of
OK (CaseDef args sc _) ->
- addDef n (CaseOp inl inr
- ty ps_in' ps args sc args' sc',
+ addDef n (CaseOp ci
+ ty ps_in' ps (cd { cases_totcheck = (args, sc) }),
acc, tot) ctxt
+ Error err -> error (show err)
_ -> ctxt in
uctxt { definitions = ctxt' }
where
@@ -820,7 +747,7 @@
(vs, x', y')
debind (Left x) = let (vs, x') = depat [] x in
(vs, x', Impossible)
- simpl (Right (x, y)) = Right (x, simplify uctxt False [] y)
+ simpl (Right (x, y)) = Right (x, simplify uctxt [] y)
simpl t = t
addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) ->
@@ -844,23 +771,32 @@
(Function ty _) -> return ty
(TyDecl _ ty) -> return ty
(Operator ty _ _) -> return ty
- (CaseOp _ _ ty _ _ _ _ _ _) -> return ty
+ (CaseOp _ ty _ _ _) -> return ty
isConName :: Name -> Context -> Bool
-isConName n ctxt
+isConName n ctxt = isTConName n ctxt || isDConName n ctxt
+
+isTConName :: Name -> Context -> Bool
+isTConName n ctxt
= or $ do def <- lookupCtxt n (definitions ctxt)
case tfst def of
- (TyDecl (DCon _ _) _) -> return True
(TyDecl (TCon _ _) _) -> return True
_ -> return False
+isDConName :: Name -> Context -> Bool
+isDConName n ctxt
+ = or $ do def <- lookupCtxt n (definitions ctxt)
+ case tfst def of
+ (TyDecl (DCon _ _) _) -> return True
+ _ -> return False
+
isFnName :: Name -> Context -> Bool
isFnName n ctxt
= or $ do def <- lookupCtxt n (definitions ctxt)
case tfst def of
(Function _ _) -> return True
(Operator _ _ _) -> return True
- (CaseOp _ _ _ _ _ _ _ _ _) -> return True
+ (CaseOp _ _ _ _ _) -> return True
_ -> return False
lookupP :: Name -> Context -> [Term]
@@ -869,7 +805,7 @@
p <- case def of
(Function ty tm, a, _) -> return (P Ref n ty, a)
(TyDecl nt ty, a, _) -> return (P nt n ty, a)
- (CaseOp _ _ ty _ _ _ _ _ _, a, _) -> return (P Ref n ty, a)
+ (CaseOp _ ty _ _ _, a, _) -> return (P Ref n ty, a)
(Operator ty _ _, a, _) -> return (P Ref n ty, a)
case snd p of
Hidden -> []
@@ -882,7 +818,9 @@
[(Def, Accessibility)]
lookupDefAcc n mkpublic ctxt
= map mkp $ lookupCtxt n (definitions ctxt)
- where mkp (d, a, _) = if mkpublic then (d, Public) else (d, a)
+ -- io_bind a special case for REPL prettiness
+ where mkp (d, a, _) = if mkpublic && (not (n == UN "io_bind" || n == UN "io_return"))
+ then (d, Public) else (d, a)
lookupTotal :: Name -> Context -> [Totality]
lookupTotal n ctxt = map mkt $ lookupCtxt n (definitions ctxt)
diff --git a/src/Core/Execute.hs b/src/Core/Execute.hs
--- a/src/Core/Execute.hs
+++ b/src/Core/Execute.hs
@@ -181,9 +181,9 @@
[Function _ tm] -> doExec env ctxt tm
[TyDecl _ _] -> return (EP Ref n EErased) -- abstract def
[Operator tp arity op] -> return (EP Ref n EErased) -- will be special-cased later
- [CaseOp _ _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun
+ [CaseOp _ _ _ _ (CaseDefs _ ([], STerm tm) _ _)] -> -- nullary fun
doExec env ctxt tm
- [CaseOp _ _ _ _ _ ns sc _ _] -> return (EP Ref n EErased)
+ [CaseOp _ _ _ _ (CaseDefs _ (ns, sc) _ _)] -> return (EP Ref n EErased)
[] -> execFail $ "Could not find " ++ show n ++ " in definitions."
thing -> trace (take 200 $ "got to " ++ show thing ++ " lookup up " ++ show n) $ undefined
doExec env ctxt p@(P Bound n ty) =
@@ -228,55 +228,69 @@
execApp' :: ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp' env ctxt v [] = return v -- no args is just a constant! can result from function calls
-execApp' env ctxt (EP _ (UN "unsafePerformIO") _) (ty:action:rest) | (prim__IO, [_, v]) <- unApplyV action =
+execApp' env ctxt (EP _ (UN "unsafePerformPrimIO") _) (ty:action:rest) | (prim__IO, [_, v]) <- unApplyV action =
execApp' env ctxt v rest
-execApp' env ctxt (EP _ (UN "io_bind") _) args@(_:_:v:k:rest) | (prim__IO, [_, v']) <- unApplyV v =
+execApp' env ctxt (EP _ (UN "prim_io_bind") _) args@(_:_:v:k:rest) | (prim__IO, [_, v']) <- unApplyV v =
do v'' <- tryForce v'
res <- execApp' env ctxt k [v''] >>= tryForce
execApp' env ctxt res rest
-execApp' env ctxt con@(EP _ (UN "io_return") _) args@(tp:v:rest) =
+execApp' env ctxt con@(EP _ (UN "prim_io_return") _) args@(tp:v:rest) =
do v' <- tryForce v
execApp' env ctxt (mkEApp con [tp, v']) rest
-- Special cases arising from not having access to the C RTS in the interpreter
-execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:EConstant (Str arg):rest)
- | Just (FFun "putStr" _ _) <- foreignFromTT fn = do execIO (putStr arg)
- execApp' env ctxt ioUnit rest
-execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:EConstant (Str f):EConstant (Str mode):rest)
- | Just (FFun "fileOpen" _ _) <- foreignFromTT fn = do m <- case mode of
- "r" -> return ReadMode
- "w" -> return WriteMode
- "a" -> return AppendMode
- "rw" -> return ReadWriteMode
- "wr" -> return ReadWriteMode
- "r+" -> return ReadWriteMode
- _ -> execFail ("Invalid mode for " ++ f ++ ": " ++ mode)
- h <- execIO $ openFile f m
- execApp' env ctxt (ioWrap (EHandle h)) rest
+execApp' env ctxt (EP _ (UN "mkForeignPrim") _) (_:fn:EConstant (Str arg):_:rest)
+ | Just (FFun "putStr" _ _) <- foreignFromTT fn
+ = do execIO (putStr arg)
+ execApp' env ctxt ioUnit rest
+execApp' env ctxt (EP _ (UN "mkForeignPrim") _) (_:fn:_:EHandle h:_:rest)
+ | Just (FFun "idris_readStr" _ _) <- foreignFromTT fn
+ = do contents <- execIO $ hGetLine h
+ execApp' env ctxt (EConstant (Str (contents ++ "\n"))) rest
+execApp' env ctxt (EP _ (UN "mkForeignPrim") _) (_:fn:EConstant (Str f):EConstant (Str mode):rest)
+ | Just (FFun "fileOpen" _ _) <- foreignFromTT fn
+ = do m <- case mode of
+ "r" -> return ReadMode
+ "w" -> return WriteMode
+ "a" -> return AppendMode
+ "rw" -> return ReadWriteMode
+ "wr" -> return ReadWriteMode
+ "r+" -> return ReadWriteMode
+ _ -> execFail ("Invalid mode for " ++ f ++ ": " ++ mode)
+ h <- execIO $ openFile f m
+ execApp' env ctxt (ioWrap (EHandle h)) (tail rest)
-execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:(EHandle h):rest)
- | Just (FFun "fileEOF" _ _) <- foreignFromTT fn = do eofp <- execIO $ hIsEOF h
- let res = ioWrap (EConstant (I $ if eofp then 1 else 0))
- execApp' env ctxt res rest
+execApp' env ctxt (EP _ (UN "mkForeignPrim") _) (_:fn:(EHandle h):rest)
+ | Just (FFun "fileEOF" _ _) <- foreignFromTT fn
+ = do eofp <- execIO $ hIsEOF h
+ let res = ioWrap (EConstant (I $ if eofp then 1 else 0))
+ execApp' env ctxt res (tail rest)
-execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:(EHandle h):rest)
- | Just (FFun "fileClose" _ _) <- foreignFromTT fn = do execIO $ hClose h
- execApp' env ctxt ioUnit rest
+execApp' env ctxt (EP _ (UN "mkForeignPrim") _) (_:fn:(EHandle h):rest)
+ | Just (FFun "fileClose" _ _) <- foreignFromTT fn
+ = do execIO $ hClose h
+ execApp' env ctxt ioUnit (tail rest)
-execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:(EPtr p):rest)
- | Just (FFun "isNull" _ _) <- foreignFromTT fn = let res = ioWrap . EConstant . I $
- if p == nullPtr then 1 else 0
- in execApp' env ctxt res rest
+execApp' env ctxt (EP _ (UN "mkForeignPrim") _) (_:fn:(EPtr p):rest)
+ | Just (FFun "isNull" _ _) <- foreignFromTT fn
+ = let res = ioWrap . EConstant . I $
+ if p == nullPtr then 1 else 0
+ in execApp' env ctxt res (tail rest)
-execApp' env ctxt f@(EP _ (UN "mkForeign") _) args@(ty:fn:xs) | Just (FFun f argTs retT) <- foreignFromTT fn
- , length xs >= length argTs =
- do res <- stepForeign (ty:fn:take (length argTs) xs)
+-- Throw away the 'World' argument to the foreign function
+
+execApp' env ctxt f@(EP _ (UN "mkForeignPrim") _) args@(ty:fn:xs)
+ | Just (FFun f argTs retT) <- foreignFromTT fn
+ , length xs >= length argTs =
+ do let (args', xs') = (take (length argTs) xs, -- foreign args
+ drop (length argTs + 1) xs) -- rest
+ res <- stepForeign (ty:fn:args')
case res of
Nothing -> fail $ "Could not call foreign function \"" ++ f ++
- "\" with args " ++ show (take (length argTs) xs)
- Just r -> return (mkEApp r (drop (length argTs) xs))
- | otherwise = return (mkEApp f args)
+ "\" with args " ++ show args
+ Just r -> return (mkEApp r xs')
+ | otherwise = return (mkEApp f args)
execApp' env ctxt c@(EP (DCon _ arity) n _) args =
do args' <- mapM tryForce (take arity args)
@@ -301,10 +315,10 @@
execApp' env ctxt r (drop arity args)
Nothing -> return (mkEApp f args)
else return (mkEApp f args)
- [CaseOp _ _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun
+ [CaseOp _ _ _ _ (CaseDefs _ ([], STerm tm) _ _)] -> -- nullary fun
do rhs <- doExec env ctxt tm
execApp' env ctxt rhs args
- [CaseOp _ _ _ _ _ ns sc _ _] ->
+ [CaseOp _ _ _ _ (CaseDefs _ (ns, sc) _ _)] ->
do res <- execCase env ctxt ns sc args
return $ fromMaybe (mkEApp f args) res
thing -> return $ mkEApp f args
@@ -502,7 +516,7 @@
Just f -> f args
Nothing -> return Nothing
return f'
-stepForeign _ = fail "Tried to call foreign function that wasn't mkForeign"
+stepForeign _ = fail "Tried to call foreign function that wasn't mkForeignPrim"
mapMaybeM :: Monad m => (a -> m (Maybe b)) -> [a] -> m [b]
mapMaybeM f [] = return []
diff --git a/src/Core/ProofState.hs b/src/Core/ProofState.hs
--- a/src/Core/ProofState.hs
+++ b/src/Core/ProofState.hs
@@ -58,6 +58,7 @@
| StartUnify Name
| EndUnify
| Compute
+ | ComputeLet Name
| Simplify
| HNF_Compute
| EvalIn Raw
@@ -175,13 +176,13 @@
unify' ctxt env topx topy =
do ps <- get
let dont = dontunify ps
- (u, fails) <- -- trace ("Trying " ++ show (topx, topy)) $
+ (u, fails) <- traceWhen (unifylog ps) ("Trying " ++ show (topx, topy)) $
lift $ unify ctxt env topx topy dont (holes ps)
traceWhen (unifylog ps)
("Unified " ++ show (topx, topy) ++ " without " ++ show dont ++
" in " ++ show env ++
- "\n" ++ show u ++ "\n" ++ qshow fails ++ "\nCurrent problems:\n"
- ++ qshow (problems ps) ++ "\n" ++ show (holes ps) ++ "\n"
+ "\nSolved: " ++ show u ++ "\nNew problems: " ++ qshow fails ++ "\nCurrent problems:\n"
+ ++ qshow (problems ps) ++ "\nHoles: " ++ show (holes ps) ++ "\n"
-- ++ show (pterm ps)
++ "\n----------") $
case fails of
@@ -265,6 +266,15 @@
atHb c env t = do ty' <- atH c env (binderTy t)
return $ t { binderTy = ty' }
+computeLet :: Context -> Name -> Term -> Term
+computeLet ctxt n tm = cl [] tm where
+ cl env (Bind n' (Let t v) sc)
+ | n' == n = let v' = normalise ctxt env v in
+ Bind n' (Let t v') sc
+ cl env (Bind n' b sc) = Bind n' (fmap (cl env) b) (cl ((n, b):env) sc)
+ cl env (App f a) = App (cl env f) (cl env a)
+ cl env t = t
+
attack :: RunTactic
attack ctxt env (Bind x (Hole t) sc)
= do h <- getName "hole"
@@ -698,6 +708,8 @@
processTactic (Reorder n) ps
= do ps' <- execStateT (tactic (Just n) reorder_claims) ps
return (ps' { previous = Just ps, plog = "" }, plog ps')
+processTactic (ComputeLet n) ps
+ = return (ps { pterm = computeLet (context ps) n (pterm ps) }, "")
processTactic t ps
= case holes ps of
[] -> fail "Nothing to fill in."
diff --git a/src/Core/TT.hs b/src/Core/TT.hs
--- a/src/Core/TT.hs
+++ b/src/Core/TT.hs
@@ -78,6 +78,7 @@
| ProofSearchFail Err
| NoRewriting Term
| At FC Err
+ | Elaborating String Name Err
| ProviderError String
deriving Eq
@@ -98,6 +99,7 @@
size UniverseError = 1
size ProgramLineComment = 1
size (At fc err) = size fc + size err
+ size (Elaborating _ n err) = size err
size (ProviderError msg) = length msg
size _ = 1
@@ -191,28 +193,64 @@
| NS Name [String] -- ^ Root, namespaces
| MN Int String -- ^ Machine chosen names
| NErased -- ^ Name of somethng which is never used in scope
+ | SN SpecialName -- ^ Decorated function names
deriving (Eq, Ord)
{-!
deriving instance Binary Name
!-}
+data SpecialName = WhereN Int Name Name
+ | InstanceN Name [String]
+ | ParentN Name String
+ | MethodN Name
+ | CaseN Name
+ deriving (Eq, Ord)
+{-!
+deriving instance Binary SpecialName
+!-}
+
instance Sized Name where
size (UN n) = 1
size (NS n els) = 1 + length els
size (MN i n) = 1
- size NErased = 1
+ size _ = 1
instance Pretty Name where
pretty (UN n) = text n
pretty (NS n s) = pretty n
pretty (MN i s) = lbrace <+> text s <+> (text . show $ i) <+> rbrace
+ pretty (SN s) = text (show s)
instance Show Name where
show (UN n) = n
show (NS n s) = showSep "." (reverse s) ++ "." ++ show n
+ show (MN _ "underscore") = "_"
show (MN i s) = "{" ++ s ++ show i ++ "}"
+ show (SN s) = show s
show NErased = "_"
+instance Show SpecialName where
+ show (WhereN i p c) = show p ++ ", " ++ show c
+ show (InstanceN cl inst) = showSep ", " inst ++ " instance of " ++ show cl
+ show (MethodN m) = "method " ++ show m
+ show (ParentN p c) = show p ++ "#" ++ c
+ show (CaseN n) = "case block in " ++ show n
+
+-- Show a name in a way decorated for code generation, not human reading
+showCG :: Name -> String
+showCG (UN n) = n
+showCG (NS n s) = showSep "." (reverse s) ++ "." ++ show n
+showCG (MN _ "underscore") = "_"
+showCG (MN i s) = "{" ++ s ++ show i ++ "}"
+showCG (SN s) = showCG' s
+ where showCG' (WhereN i p c) = show p ++ ":" ++ show c ++ ":" ++ show i
+ showCG' (InstanceN cl inst) = '@':show cl ++ '$':showSep ":" inst
+ showCG' (MethodN m) = '!':show m
+ showCG' (ParentN p c) = show p ++ "#" ++ show c
+ showCG' (CaseN c) = show c ++ "_case"
+showCG NErased = "_"
+
+
-- |Contexts allow us to map names to things. A root name maps to a collection
-- of things in different namespaces with that name.
type Ctxt a = Map.Map Name (Map.Map Name a)
@@ -220,6 +258,9 @@
tcname (UN ('@':_)) = True
tcname (NS n _) = tcname n
+tcname (SN (InstanceN _ _)) = True
+tcname (SN (MethodN _)) = True
+tcname (SN (ParentN _ _)) = True
tcname _ = False
implicitable (NS n _) = implicitable n
@@ -758,6 +799,11 @@
where
readN "" = 0
readN x = read x
+nextName (SN x) = SN (nextName' x)
+ where
+ nextName' (WhereN i f x) = WhereN i f (nextName x)
+ nextName' (CaseN n) = CaseN (nextName n)
+ nextName' (MethodN n) = MethodN (nextName n)
type Term = TT Name
type Type = Term
diff --git a/src/Core/Typecheck.hs b/src/Core/Typecheck.hs
--- a/src/Core/Typecheck.hs
+++ b/src/Core/Typecheck.hs
@@ -79,7 +79,7 @@
do convertsC ctxt env aty s
-- let apty = normalise initContext env
-- (Bind x (Let aty av) t)
- let apty = simplify initContext False env
+ let apty = simplify initContext env
(Bind x (Let aty av) t)
return (App fv av, apty)
t -> lift $ tfail $ NonFunctionType fv fty -- "Can't apply a non-function type"
@@ -203,28 +203,15 @@
discharge n (NLet t v) scv sct
= return (Bind n (NLet t v) scv, Bind n (Let t v) sct)
discharge n (Hole t) scv sct
- = do -- A hole can't appear in the type of its scope
- checkNotHoley 0 sct
- return (Bind n (Hole t) scv, sct)
+ = return (Bind n (Hole t) scv, sct)
discharge n (GHole t) scv sct
- = do -- A hole can't appear in the type of its scope
- checkNotHoley 0 sct
- return (Bind n (GHole t) scv, sct)
+ = return (Bind n (GHole t) scv, sct)
discharge n (Guess t v) scv sct
- = do -- A hole can't appear in the type of its scope
- checkNotHoley 0 sct
- return (Bind n (Guess t v) scv, sct)
+ = return (Bind n (Guess t v) scv, sct)
discharge n (PVar t) scv sct
= return (Bind n (PVar t) scv, Bind n (PVTy t) sct)
discharge n (PVTy t) scv sct
= return (Bind n (PVTy t) scv, sct)
-
- checkNotHoley i (V v)
- | v == i = fail "You can't put a hole where a hole don't belong"
- checkNotHoley i (App f a) = do checkNotHoley i f
- checkNotHoley i a
- checkNotHoley i (Bind n b sc) = checkNotHoley (i+1) sc
- checkNotHoley _ _ = return ()
checkProgram :: Context -> RProgram -> TC Context
diff --git a/src/Core/Unify.hs b/src/Core/Unify.hs
--- a/src/Core/Unify.hs
+++ b/src/Core/Unify.hs
@@ -154,6 +154,9 @@
sc i = do UI s f <- get
put (UI (s+i) f)
+ errors = do UI s f <- get
+ return (not (null f))
+
uplus u1 u2 = do UI s f <- get
r <- u1
UI s f' <- get
@@ -290,7 +293,9 @@
then
-- (notFn headx && notFn heady))) then
do uf <- un' True bnames headx heady
- unArgs uf argsx argsy
+ failed <- errors
+ if (not failed) then unArgs uf argsx argsy
+ else return []
else -- trace ("TMPFAIL " ++ show (appx, appy, injective appx, injective appy)) $
unifyTmpFail appx appy)
(unifyTmpFail appx appy) -- whole application fails
diff --git a/src/IRTS/CodegenC.hs b/src/IRTS/CodegenC.hs
--- a/src/IRTS/CodegenC.hs
+++ b/src/IRTS/CodegenC.hs
@@ -23,10 +23,11 @@
OutputType -> -- generate executable if True, only .o if False
[FilePath] -> -- include files
String -> -- extra object files
- String -> -- extra compiler flags
+ String -> -- extra compiler flags (libraries)
+ String -> -- extra compiler flags (anything)
DbgLevel ->
IO ()
-codegenC defs out exec incs objs libs dbg
+codegenC defs out exec incs objs libs flags dbg
= do -- print defs
let bc = map toBC defs
let h = concatMap toDecl (map fst bc)
@@ -47,13 +48,15 @@
libFlags <- getLibFlags
incFlags <- getIncFlags
let gcc = comp ++ " " ++
- gccDbg dbg ++
+ gccDbg dbg ++ " " ++
+ gccFlags ++
" -I. " ++ objs ++ " -x c " ++
(if (exec == Executable) then "" else " -c ") ++
" " ++ tmpn ++
" " ++ libFlags ++
" " ++ incFlags ++
" " ++ libs ++
+ " " ++ flags ++
" -o " ++ out
-- putStrLn gcc
exit <- system gcc
@@ -68,12 +71,16 @@
debug TRACE = "#define IDRIS_TRACE\n\n"
debug _ = ""
+-- We're using signed integers now. Make sure we get consistent semantics
+-- out of them from gcc. See e.g. http://thiemonagel.de/2010/01/signed-integer-overflow/
+gccFlags = " -fwrapv -fno-strict-overflow"
+
gccDbg DEBUG = "-g"
gccDbg TRACE = "-O2"
gccDbg _ = "-O2"
cname :: Name -> String
-cname n = "_idris_" ++ concatMap cchar (show n)
+cname n = "_idris_" ++ concatMap cchar (showCG n)
where cchar x | isAlpha x || isDigit x = [x]
| otherwise = "_" ++ show (fromEnum x) ++ "_"
@@ -272,10 +279,14 @@
doOp v (LASHR ITNative) [l, r] = v ++ "INTOP(>>," ++ creg l ++ ", " ++ creg r ++ ")"
doOp v (LCompl ITNative) [x] = v ++ "INTOP(~," ++ creg x ++ ")"
doOp v (LEq (ATInt ITNative)) [l, r] = v ++ "INTOP(==," ++ creg l ++ ", " ++ creg r ++ ")"
-doOp v (LLt (ATInt ITNative)) [l, r] = v ++ "INTOP(<," ++ creg l ++ ", " ++ creg r ++ ")"
-doOp v (LLe (ATInt ITNative)) [l, r] = v ++ "INTOP(<=," ++ creg l ++ ", " ++ creg r ++ ")"
-doOp v (LGt (ATInt ITNative)) [l, r] = v ++ "INTOP(>," ++ creg l ++ ", " ++ creg r ++ ")"
-doOp v (LGe (ATInt ITNative)) [l, r] = v ++ "INTOP(>=," ++ creg l ++ ", " ++ creg r ++ ")"
+doOp v (LSLt (ATInt ITNative)) [l, r] = v ++ "INTOP(<," ++ creg l ++ ", " ++ creg r ++ ")"
+doOp v (LSLe (ATInt ITNative)) [l, r] = v ++ "INTOP(<=," ++ creg l ++ ", " ++ creg r ++ ")"
+doOp v (LSGt (ATInt ITNative)) [l, r] = v ++ "INTOP(>," ++ creg l ++ ", " ++ creg r ++ ")"
+doOp v (LSGe (ATInt ITNative)) [l, r] = v ++ "INTOP(>=," ++ creg l ++ ", " ++ creg r ++ ")"
+doOp v (LLt ITNative) [l, r] = v ++ "UINTOP(<," ++ creg l ++ ", " ++ creg r ++ ")"
+doOp v (LLe ITNative) [l, r] = v ++ "UINTOP(<=," ++ creg l ++ ", " ++ creg r ++ ")"
+doOp v (LGt ITNative) [l, r] = v ++ "UINTOP(>," ++ creg l ++ ", " ++ creg r ++ ")"
+doOp v (LGe ITNative) [l, r] = v ++ "UINTOP(>=," ++ creg l ++ ", " ++ creg r ++ ")"
doOp v (LPlus (ATInt ITChar)) [l, r] = doOp v (LPlus (ATInt ITNative)) [l, r]
doOp v (LMinus (ATInt ITChar)) [l, r] = doOp v (LMinus (ATInt ITNative)) [l, r]
@@ -292,20 +303,24 @@
doOp v (LASHR ITChar) [l, r] = doOp v (LASHR ITNative) [l, r]
doOp v (LCompl ITChar) [x] = doOp v (LCompl ITNative) [x]
doOp v (LEq (ATInt ITChar)) [l, r] = doOp v (LEq (ATInt ITNative)) [l, r]
-doOp v (LLt (ATInt ITChar)) [l, r] = doOp v (LLt (ATInt ITNative)) [l, r]
-doOp v (LLe (ATInt ITChar)) [l, r] = doOp v (LLe (ATInt ITNative)) [l, r]
-doOp v (LGt (ATInt ITChar)) [l, r] = doOp v (LGt (ATInt ITNative)) [l, r]
-doOp v (LGe (ATInt ITChar)) [l, r] = doOp v (LGe (ATInt ITNative)) [l, r]
+doOp v (LSLt (ATInt ITChar)) [l, r] = doOp v (LSLt (ATInt ITNative)) [l, r]
+doOp v (LSLe (ATInt ITChar)) [l, r] = doOp v (LSLe (ATInt ITNative)) [l, r]
+doOp v (LSGt (ATInt ITChar)) [l, r] = doOp v (LSGt (ATInt ITNative)) [l, r]
+doOp v (LSGe (ATInt ITChar)) [l, r] = doOp v (LSGe (ATInt ITNative)) [l, r]
+doOp v (LLt ITChar) [l, r] = doOp v (LLt ITNative) [l, r]
+doOp v (LLe ITChar) [l, r] = doOp v (LLe ITNative) [l, r]
+doOp v (LGt ITChar) [l, r] = doOp v (LGt ITNative) [l, r]
+doOp v (LGe ITChar) [l, r] = doOp v (LGe ITNative) [l, r]
doOp v (LPlus ATFloat) [l, r] = v ++ "FLOATOP(+," ++ creg l ++ ", " ++ creg r ++ ")"
doOp v (LMinus ATFloat) [l, r] = v ++ "FLOATOP(-," ++ creg l ++ ", " ++ creg r ++ ")"
doOp v (LTimes ATFloat) [l, r] = v ++ "FLOATOP(*," ++ creg l ++ ", " ++ creg r ++ ")"
doOp v (LSDiv ATFloat) [l, r] = v ++ "FLOATOP(/," ++ creg l ++ ", " ++ creg r ++ ")"
doOp v (LEq ATFloat) [l, r] = v ++ "FLOATBOP(==," ++ creg l ++ ", " ++ creg r ++ ")"
-doOp v (LLt ATFloat) [l, r] = v ++ "FLOATBOP(<," ++ creg l ++ ", " ++ creg r ++ ")"
-doOp v (LLe ATFloat) [l, r] = v ++ "FLOATBOP(<=," ++ creg l ++ ", " ++ creg r ++ ")"
-doOp v (LGt ATFloat) [l, r] = v ++ "FLOATBOP(>," ++ creg l ++ ", " ++ creg r ++ ")"
-doOp v (LGe ATFloat) [l, r] = v ++ "FLOATBOP(>=," ++ creg l ++ ", " ++ creg r ++ ")"
+doOp v (LSLt ATFloat) [l, r] = v ++ "FLOATBOP(<," ++ creg l ++ ", " ++ creg r ++ ")"
+doOp v (LSLe ATFloat) [l, r] = v ++ "FLOATBOP(<=," ++ creg l ++ ", " ++ creg r ++ ")"
+doOp v (LSGt ATFloat) [l, r] = v ++ "FLOATBOP(>," ++ creg l ++ ", " ++ creg r ++ ")"
+doOp v (LSGe ATFloat) [l, r] = v ++ "FLOATBOP(>=," ++ creg l ++ ", " ++ creg r ++ ")"
doOp v (LIntFloat ITBig) [x] = v ++ "idris_castBigFloat(vm, " ++ creg x ++ ")"
doOp v (LFloatInt ITBig) [x] = v ++ "idris_castFloatBig(vm, " ++ creg x ++ ")"
@@ -315,10 +330,10 @@
doOp v (LSDiv (ATInt ITBig)) [l, r] = v ++ "idris_bigDivide(vm, " ++ creg l ++ ", " ++ creg r ++ ")"
doOp v (LSRem (ATInt ITBig)) [l, r] = v ++ "idris_bigMod(vm, " ++ creg l ++ ", " ++ creg r ++ ")"
doOp v (LEq (ATInt ITBig)) [l, r] = v ++ "idris_bigEq(vm, " ++ creg l ++ ", " ++ creg r ++ ")"
-doOp v (LLt (ATInt ITBig)) [l, r] = v ++ "idris_bigLt(vm, " ++ creg l ++ ", " ++ creg r ++ ")"
-doOp v (LLe (ATInt ITBig)) [l, r] = v ++ "idris_bigLe(vm, " ++ creg l ++ ", " ++ creg r ++ ")"
-doOp v (LGt (ATInt ITBig)) [l, r] = v ++ "idris_bigGt(vm, " ++ creg l ++ ", " ++ creg r ++ ")"
-doOp v (LGe (ATInt ITBig)) [l, r] = v ++ "idris_bigGe(vm, " ++ creg l ++ ", " ++ creg r ++ ")"
+doOp v (LSLt (ATInt ITBig)) [l, r] = v ++ "idris_bigLt(vm, " ++ creg l ++ ", " ++ creg r ++ ")"
+doOp v (LSLe (ATInt ITBig)) [l, r] = v ++ "idris_bigLe(vm, " ++ creg l ++ ", " ++ creg r ++ ")"
+doOp v (LSGt (ATInt ITBig)) [l, r] = v ++ "idris_bigGt(vm, " ++ creg l ++ ", " ++ creg r ++ ")"
+doOp v (LSGe (ATInt ITBig)) [l, r] = v ++ "idris_bigGe(vm, " ++ creg l ++ ", " ++ creg r ++ ")"
doOp v LStrConcat [l,r] = v ++ "idris_concat(vm, " ++ creg l ++ ", " ++ creg r ++ ")"
doOp v LStrLt [l,r] = v ++ "idris_strlt(vm, " ++ creg l ++ ", " ++ creg r ++ ")"
@@ -340,11 +355,15 @@
doOp _ LPrintNum [x] = "printf(\"%ld\\n\", GETINT(" ++ creg x ++ "))"
doOp _ LPrintStr [x] = "fputs(GETSTR(" ++ creg x ++ "), stdout)"
-doOp v (LLt (ATInt (ITFixed ty))) [x, y] = bitOp v "Lt" ty [x, y]
-doOp v (LLe (ATInt (ITFixed ty))) [x, y] = bitOp v "Lte" ty [x, y]
+doOp v (LSLt (ATInt (ITFixed ty))) [x, y] = bitOp v "SLt" ty [x, y]
+doOp v (LSLe (ATInt (ITFixed ty))) [x, y] = bitOp v "SLte" ty [x, y]
doOp v (LEq (ATInt (ITFixed ty))) [x, y] = bitOp v "Eq" ty [x, y]
-doOp v (LGe (ATInt (ITFixed ty))) [x, y] = bitOp v "Gte" ty [x, y]
-doOp v (LGt (ATInt (ITFixed ty))) [x, y] = bitOp v "Gt" ty [x, y]
+doOp v (LSGe (ATInt (ITFixed ty))) [x, y] = bitOp v "SGte" ty [x, y]
+doOp v (LSGt (ATInt (ITFixed ty))) [x, y] = bitOp v "SGt" ty [x, y]
+doOp v (LLt (ITFixed ty)) [x, y] = bitOp v "Lt" ty [x, y]
+doOp v (LLe (ITFixed ty)) [x, y] = bitOp v "Lte" ty [x, y]
+doOp v (LGe (ITFixed ty)) [x, y] = bitOp v "Gte" ty [x, y]
+doOp v (LGt (ITFixed ty)) [x, y] = bitOp v "Gt" ty [x, y]
doOp v (LSHL (ITFixed ty)) [x, y] = bitOp v "Shl" ty [x, y]
doOp v (LLSHR (ITFixed ty)) [x, y] = bitOp v "LShr" ty [x, y]
@@ -364,8 +383,6 @@
doOp v (LSExt (ITFixed from) ITBig) [x]
= v ++ "MKBIGSI(vm, (" ++ signedTy from ++ ")" ++ creg x ++ "->info.bits" ++ show (nativeTyWidth from) ++ ")"
-doOp v (LZExt ITNative ITBig) [x]
- = v ++ "MKBIGSI(vm, GETINT(" ++ creg x ++ "))"
doOp v (LSExt ITNative (ITFixed to)) [x]
= v ++ "idris_b" ++ show (nativeTyWidth to) ++ "const(vm, GETINT(" ++ creg x ++ "))"
doOp v (LSExt ITChar (ITFixed to)) [x]
@@ -386,8 +403,8 @@
= doOp v (LZExt (ITFixed from) ITNative) [x]
doOp v (LZExt (ITFixed from) ITBig) [x]
= v ++ "MKBIGUI(vm, " ++ creg x ++ "->info.bits" ++ show (nativeTyWidth from) ++ ")"
--- doOp v (LZExt ITNative ITBig) [x]
--- = v ++ "MKBIGUI(vm, (uintptr_t)GETINT(" ++ creg x ++ "))"
+doOp v (LZExt ITNative ITBig) [x]
+ = v ++ "MKBIGUI(vm, (uintptr_t)GETINT(" ++ creg x ++ "))"
doOp v (LZExt (ITFixed from) (ITFixed to)) [x]
| nativeTyWidth from < nativeTyWidth to = bitCoerce v "Z" from to x
doOp v (LTrunc ITNative (ITFixed to)) [x]
diff --git a/src/IRTS/CodegenJavaScript.hs b/src/IRTS/CodegenJavaScript.hs
--- a/src/IRTS/CodegenJavaScript.hs
+++ b/src/IRTS/CodegenJavaScript.hs
@@ -2,7 +2,7 @@
module IRTS.CodegenJavaScript (codegenJavaScript, JSTarget(..)) where
-import Idris.AbsSyntax
+import Idris.AbsSyntax hiding (TypeCase)
import IRTS.Bytecode
import IRTS.Lang
import IRTS.Simplified
@@ -14,16 +14,204 @@
import Control.Arrow
import Data.Char
import Data.List
-import qualified Data.Map as Map
+import Data.Maybe
import System.IO
import System.Directory
idrNamespace :: String
-idrNamespace = "__IDR__"
+idrNamespace = "__IDR__"
idrRTNamespace = "__IDRRT__"
+idrLTNamespace = "__IDRLT__"
data JSTarget = Node | JavaScript deriving Eq
+data JSType = JSIntTy
+ | JSStringTy
+ | JSIntegerTy
+ | JSFloatTy
+ | JSCharTy
+ | JSPtrTy
+ | JSForgotTy
+ deriving Eq
+
+data JSNum = JSInt Int
+ | JSFloat Double
+ | JSInteger Integer
+
+data JS = JSRaw String
+ | JSFunction [String] JS
+ | JSType JSType
+ | JSSeq [JS]
+ | JSReturn JS
+ | JSApp JS [JS]
+ | JSNew String [JS]
+ | JSError String
+ | JSOp String JS JS
+ | JSProj JS String
+ | JSVar LVar
+ | JSNull
+ | JSThis
+ | JSTrue
+ | JSArray [JS]
+ | JSObject [(String, JS)]
+ | JSString String
+ | JSNum JSNum
+ | JSAssign JS JS
+ | JSAlloc String (Maybe JS)
+ | JSIndex JS JS
+ | JSCond [(JS, JS)]
+ | JSTernary JS JS JS
+
+compileJS :: JS -> String
+compileJS (JSRaw code) =
+ code
+
+compileJS (JSFunction args body) =
+ "function("
+ ++ intercalate "," args
+ ++ "){\n"
+ ++ compileJS body
+ ++ "\n}"
+
+compileJS (JSType ty)
+ | JSIntTy <- ty = idrRTNamespace ++ "Int"
+ | JSStringTy <- ty = idrRTNamespace ++ "String"
+ | JSIntegerTy <- ty = idrRTNamespace ++ "Integer"
+ | JSFloatTy <- ty = idrRTNamespace ++ "Float"
+ | JSCharTy <- ty = idrRTNamespace ++ "Char"
+ | JSPtrTy <- ty = idrRTNamespace ++ "Ptr"
+ | JSForgotTy <- ty = idrRTNamespace ++ "Forgot"
+
+compileJS (JSSeq seq) =
+ intercalate ";\n" (map compileJS seq)
+
+compileJS (JSReturn val) =
+ "return " ++ compileJS val
+
+compileJS (JSApp lhs rhs)
+ | JSFunction {} <- lhs =
+ concat ["(", compileJS lhs, ")(", args, ")"]
+ | otherwise =
+ concat [compileJS lhs, "(", args, ")"]
+ where args :: String
+ args = intercalate "," $ map compileJS rhs
+
+compileJS (JSNew name args) =
+ "new " ++ name ++ "(" ++ intercalate "," (map compileJS args) ++ ")"
+
+compileJS (JSError exc) =
+ "(function(){throw '" ++ exc ++ "';})()"
+
+compileJS (JSOp op lhs rhs) =
+ compileJS lhs ++ " " ++ op ++ " " ++ compileJS rhs
+
+compileJS (JSProj obj field)
+ | JSFunction {} <- obj =
+ concat ["(", compileJS obj, ").", field]
+ | otherwise =
+ compileJS obj ++ '.' : field
+
+compileJS (JSVar var) =
+ translateVariableName var
+
+compileJS JSNull =
+ "null"
+
+compileJS JSThis =
+ "this"
+
+compileJS JSTrue =
+ "true"
+
+compileJS (JSArray elems) =
+ "[" ++ intercalate "," (map compileJS elems) ++ "]"
+
+compileJS (JSObject fields) =
+ "{" ++ intercalate ",\n" (map compileField fields) ++ "}"
+ where
+ compileField :: (String, JS) -> String
+ compileField (name, val) = '\'' : name ++ "' : " ++ compileJS val
+
+compileJS (JSString str) =
+ show str
+
+compileJS (JSNum num)
+ | JSInt i <- num = show i
+ | JSFloat f <- num = show f
+ | JSInteger i <- num = show i
+
+compileJS (JSAssign lhs rhs) =
+ compileJS lhs ++ "=" ++ compileJS rhs
+
+compileJS (JSAlloc name val) =
+ "var " ++ name ++ maybe "" ((" = " ++) . compileJS) val
+
+compileJS (JSIndex lhs rhs) =
+ compileJS lhs ++ "[" ++ compileJS rhs ++ "]"
+
+compileJS (JSCond branches) =
+ intercalate " else " $ map createIfBlock branches
+ where
+ createIfBlock (cond, e) =
+ "if (" ++ compileJS cond ++") {\n"
+ ++ "return " ++ compileJS e
+ ++ ";\n}"
+
+compileJS (JSTernary cond true false) =
+ let c = compileJS cond
+ t = compileJS true
+ f = compileJS false in
+ "(" ++ c ++ ")?(" ++ t ++ "):(" ++ f ++ ")"
+
+jsTailcall :: JS -> JS
+jsTailcall call =
+ jsCall (idrRTNamespace ++ "tailcall") [
+ JSFunction [] (JSReturn call)
+ ]
+
+jsCall :: String -> [JS] -> JS
+jsCall fun = JSApp (JSRaw fun)
+
+jsMeth :: JS -> String -> [JS] -> JS
+jsMeth obj meth =
+ JSApp (JSProj obj meth)
+
+jsInstanceOf :: JS -> JS -> JS
+jsInstanceOf = JSOp "instanceof"
+
+jsEq :: JS -> JS -> JS
+jsEq = JSOp "=="
+
+jsAnd :: JS -> JS -> JS
+jsAnd = JSOp "&&"
+
+jsType :: JS
+jsType = JSRaw $ idrRTNamespace ++ "Type"
+
+jsCon :: JS
+jsCon = JSRaw $ idrRTNamespace ++ "Con"
+
+jsTag :: JS -> JS
+jsTag obj = JSProj obj "tag"
+
+jsTypeTag :: JS -> JS
+jsTypeTag obj = JSProj obj "type"
+
+jsBigInt :: JS -> JS
+jsBigInt val =
+ JSApp (JSRaw $ idrRTNamespace ++ "bigInt") [val]
+
+jsVar :: Int -> String
+jsVar = ("__var_" ++) . show
+
+jsLet :: String -> JS -> JS -> JS
+jsLet name value body =
+ JSApp (
+ JSFunction [name] (
+ JSReturn body
+ )
+ ) [value]
+
codegenJavaScript
:: JSTarget
-> [(Name, SDecl)]
@@ -36,38 +224,44 @@
("#!/usr/bin/env node\n", "-node")
JavaScript ->
("", "-browser")
- path <- getDataDir
+ path <- getDataDir
idrRuntime <- readFile $ path ++ "/js/Runtime-common.js"
tgtRuntime <- readFile $ concat [path, "/js/Runtime", runtime, ".js"]
- writeFile filename ( header
- ++ idrRuntime
- ++ tgtRuntime
- ++ functions
- ++ mainLoop)
+ writeFile filename $ intercalate "\n" $ [ header
+ , idrRuntime
+ , tgtRuntime
+ ] ++ functions ++ [mainLoop]
setPermissions filename (emptyPermissions { readable = True
, executable = target == Node
, writable = True
})
where
+ def :: [(String, SDecl)]
def = map (first translateNamespace) definitions
-
- functions = concatMap translateDeclaration def
+ functions :: [String]
+ functions = map (compileJS . translateDeclaration) def
+
mainLoop :: String
- mainLoop = intercalate "\n" [ "\nfunction main() {"
- , createTailcall "__IDR__runMain0()"
- , "}\n\nmain();\n"
- ]
+ mainLoop = compileJS $
+ JSSeq [ JSAlloc "main" $ Just $ JSFunction [] (
+ jsTailcall $ jsCall mainFun []
+ )
+ , jsCall "main" []
+ ]
+ mainFun :: String
+ mainFun = idrNamespace ++ translateName (MN 0 "runMain")
+
translateIdentifier :: String -> String
translateIdentifier =
replaceReserved . concatMap replaceBadChars
where replaceBadChars :: Char -> String
replaceBadChars c
- | ' ' <- c = "_"
- | '_' <- c = "__"
- | isDigit c = "_" ++ [c] ++ "_"
+ | ' ' <- c = "_"
+ | '_' <- c = "__"
+ | isDigit c = '_' : show (ord c)
| not (isLetter c && isAscii c) = '_' : show (ord c)
| otherwise = [c]
replaceReserved s
@@ -99,14 +293,14 @@
, "void"
, "while"
, "with"
-
+
, "class"
, "enum"
, "export"
, "extends"
, "import"
, "super"
-
+
, "implements"
, "interface"
, "let"
@@ -122,131 +316,210 @@
translateNamespace (UN _) = idrNamespace
translateNamespace (NS _ ns) = idrNamespace ++ concatMap translateIdentifier ns
translateNamespace (MN _ _) = idrNamespace
+translateNamespace (SN name) = idrNamespace ++ translateSpecialName name
+translateNamespace NErased = idrNamespace
translateName :: Name -> String
-translateName (UN name) = translateIdentifier name
-translateName (NS name _) = translateName name
-translateName (MN i name) = translateIdentifier name ++ show i
+translateName (UN name) = 'u' : translateIdentifier name
+translateName (NS name _) = 'n' : translateName name
+translateName (MN i name) = 'm' : translateIdentifier name ++ show i
+translateName (SN name) = 's' : translateSpecialName name
+translateName NErased = "e"
-translateConstant :: Const -> String
-translateConstant (I i) = show i
-translateConstant (BI i) = idrRTNamespace ++ "bigInt('" ++ show i ++ "')"
-translateConstant (Fl f) = show f
-translateConstant (Ch c) = show c
-translateConstant (Str s) = show s
-translateConstant (AType (ATInt ITNative)) = idrRTNamespace ++ "Int"
-translateConstant StrType = idrRTNamespace ++ "String"
-translateConstant (AType (ATInt ITBig)) = idrRTNamespace ++ "Integer"
-translateConstant (AType ATFloat) = idrRTNamespace ++ "Float"
-translateConstant (AType (ATInt ITChar)) = idrRTNamespace ++ "Char"
-translateConstant PtrType = idrRTNamespace ++ "Ptr"
-translateConstant Forgot = idrRTNamespace ++ "Forgot"
-translateConstant c =
- "(function(){throw 'Unimplemented Const: " ++ show c ++ "';})()"
+translateSpecialName :: SpecialName -> String
+translateSpecialName name
+ | WhereN i m n <- name =
+ 'w' : translateName m ++ translateName n ++ show i
+ | InstanceN n s <- name =
+ 'i' : translateName n ++ concatMap translateIdentifier s
+ | ParentN n s <- name =
+ 'p' : translateName n ++ translateIdentifier s
+ | MethodN n <- name =
+ 'm' : translateName n
+ | CaseN n <- name =
+ 'c' : translateName n
-translateParameterlist =
- map translateParameter
- where translateParameter (MN i name) = translateIdentifier name ++ show i
- translateParameter (UN name) = translateIdentifier name
+translateConstant :: Const -> JS
+translateConstant (I i) = JSNum (JSInt i)
+translateConstant (Fl f) = JSNum (JSFloat f)
+translateConstant (Ch c) = JSString [c]
+translateConstant (Str s) = JSString s
+translateConstant (AType (ATInt ITNative)) = JSType JSIntTy
+translateConstant StrType = JSType JSStringTy
+translateConstant (AType (ATInt ITBig)) = JSType JSIntegerTy
+translateConstant (AType ATFloat) = JSType JSFloatTy
+translateConstant (AType (ATInt ITChar)) = JSType JSCharTy
+translateConstant PtrType = JSType JSPtrTy
+translateConstant Forgot = JSType JSForgotTy
+translateConstant (BI i) = jsBigInt $ JSNum (JSInteger i)
+translateConstant c =
+ JSError $ "Unimplemented Constant: " ++ show c
-translateDeclaration :: (String, SDecl) -> String
-translateDeclaration (path, SFun name params stackSize body) =
- "var " ++ path ++ translateName name
- ++ " = function("
- ++ intercalate "," p
- ++ "){\n"
- ++ concatMap assignVar (zip [0..] p)
- ++ concatMap allocVar [numP..(numP+stackSize-1)]
- ++ "return "
- ++ translateExpression body
- ++ ";\n};\n"
- where
- numP :: Int
- numP = length params
+translateDeclaration :: (String, SDecl) -> JS
+translateDeclaration (path, SFun name params stackSize body)
+ | (MN _ "APPLY") <- name
+ , (SLet var val next) <- body
+ , (SChkCase cvar cases) <- next =
+ let lvar = translateVariableName var
+ lookup = "[" ++ lvar ++ ".tag](fn0,arg0," ++ lvar ++ ")" in
+ JSSeq [ lookupTable [(var, "chk")] var cases
+ , jsDecl $ JSFunction ["fn0", "arg0"] (
+ JSSeq [ JSAlloc "__var_0" (Just $ JSRaw "fn0")
+ , JSReturn $ jsLet (translateVariableName var) (
+ translateExpression val
+ ) (JSTernary (
+ (JSVar var `jsInstanceOf` jsCon) `jsAnd`
+ (hasProp lookupTableName (translateVariableName var))
+ ) (JSRaw $
+ lookupTableName ++ lookup
+ ) JSNull
+ )
+ ]
+ )
+ ]
- allocVar :: Int -> String
- allocVar n = "var __var_" ++ show n ++ ";\n"
+ | (MN _ "EVAL") <- name
+ , (SChkCase var cases) <- body =
+ JSSeq [ lookupTable [] var cases
+ , jsDecl $ JSFunction ["arg0"] (JSReturn $
+ JSTernary (
+ (JSRaw "arg0" `jsInstanceOf` jsCon) `jsAnd`
+ (hasProp lookupTableName "arg0")
+ ) (JSRaw $ lookupTableName ++ "[arg0.tag](arg0)") (JSRaw "arg0")
+ )
+ ]
+ | otherwise =
+ let fun = translateExpression body in
+ jsDecl $ jsFun fun
- assignVar :: (Int, String) -> String
- assignVar (n, s) = "var __var_" ++ show n ++ " = " ++ s ++ ";\n"
+ where
+ hasProp :: String -> String -> JS
+ hasProp table var =
+ jsMeth (JSRaw table) "hasOwnProperty" [JSRaw $ var ++ ".tag"]
- p :: [String]
- p = translateParameterlist params
+ caseFun :: [(LVar, String)] -> LVar -> SAlt -> JS
+ caseFun aux var cse =
+ jsFunAux aux (translateCase (Just (translateVariableName var)) cse)
+ getTag :: SAlt -> Maybe String
+ getTag (SConCase _ tag _ _ _) = Just $ show tag
+ getTag _ = Nothing
+
+ lookupTableName :: String
+ lookupTableName = idrLTNamespace ++ translateName name
+
+ lookupTable :: [(LVar, String)] -> LVar -> [SAlt] -> JS
+ lookupTable aux var cases =
+ JSAlloc lookupTableName $ Just (
+ JSObject $ catMaybes $ map (lookupEntry aux var) cases
+ )
+ where
+ lookupEntry :: [(LVar, String)] -> LVar -> SAlt -> Maybe (String, JS)
+ lookupEntry aux var alt = do
+ tag <- getTag alt
+ return (tag, caseFun aux var alt)
+
+ jsDecl :: JS -> JS
+ jsDecl = JSAlloc (path ++ translateName name) . Just
+
+ jsFun body = jsFunAux [] body
+
+ jsFunAux :: [(LVar, String)] -> JS -> JS
+ jsFunAux aux body =
+ JSFunction (p ++ map snd aux) (
+ JSSeq $
+ zipWith assignVar [0..] p ++
+ map allocVar [numP .. (numP + stackSize - 1)] ++
+ map assignAux aux ++
+ [JSReturn body]
+ )
+ where
+ numP :: Int
+ numP = length params
+
+ allocVar :: Int -> JS
+ allocVar n = JSAlloc (jsVar n) Nothing
+
+ assignVar :: Int -> String -> JS
+ assignVar n s = JSAlloc (jsVar n) (Just $ JSRaw s)
+
+ assignAux :: (LVar, String) -> JS
+ assignAux (var, val) =
+ JSAssign (JSRaw $ translateVariableName var) (JSRaw val)
+
+ p :: [String]
+ p = map translateName params
+
translateVariableName :: LVar -> String
translateVariableName (Loc i) =
- "__var_" ++ show i
+ jsVar i
-translateExpression :: SExp -> String
+translateExpression :: SExp -> JS
translateExpression (SLet name value body) =
- "(function("
- ++ translateVariableName name
- ++ "){\nreturn "
- ++ translateExpression body
- ++ ";\n})("
- ++ translateExpression value
- ++ ")"
+ jsLet (translateVariableName name) (
+ translateExpression value
+ ) (translateExpression body)
translateExpression (SConst cst) =
translateConstant cst
translateExpression (SV var) =
- translateVariableName var
-
-translateExpression (SApp False name vars) =
- createTailcall $ translateFunctionCall name vars
+ JSVar var
-translateExpression (SApp True name vars) =
- "new " ++ idrRTNamespace ++ "Tailcall("
- ++ "function(){\n"
- ++ "return " ++ translateFunctionCall name vars
- ++ ";\n})"
+translateExpression (SApp tc name vars)
+ | False <- tc =
+ jsTailcall $ translateFunctionCall name vars
+ | True <- tc =
+ JSNew (idrRTNamespace ++ "Tailcall") [JSFunction [] (
+ JSReturn $ translateFunctionCall name vars
+ )]
+ where
+ translateFunctionCall name vars =
+ jsCall (translateNamespace name ++ translateName name) (map JSVar vars)
translateExpression (SOp op vars)
- | LNoOp <- op = translateVariableName (last vars)
-
- | (LZExt _ ITBig) <- op =
- idrRTNamespace ++ "bigInt(" ++ translateVariableName (last vars) ++ ")"
+ | LNoOp <- op = JSVar (last vars)
- | (LPlus (ATInt ITBig)) <- op
- , (lhs:rhs:_) <- vars = translateBinaryOp ".add(" lhs rhs ++ ")"
+ | (LZExt _ ITBig) <- op = jsBigInt $ JSVar (last vars)
+ | (LPlus (ATInt ITBig)) <- op
+ , (lhs:rhs:_) <- vars = invokeMeth lhs "add" [rhs]
| (LMinus (ATInt ITBig)) <- op
- , (lhs:rhs:_) <- vars = translateBinaryOp ".minus(" lhs rhs ++ ")"
+ , (lhs:rhs:_) <- vars = invokeMeth lhs "minus" [rhs]
| (LTimes (ATInt ITBig)) <- op
- , (lhs:rhs:_) <- vars = translateBinaryOp ".times(" lhs rhs ++ ")"
- | (LSDiv (ATInt ITBig)) <- op
- , (lhs:rhs:_) <- vars = translateBinaryOp ".divide(" lhs rhs ++ ")"
- | (LSRem (ATInt ITBig)) <- op
- , (lhs:rhs:_) <- vars = translateBinaryOp ".mod(" lhs rhs ++ ")"
- | (LEq (ATInt ITBig)) <- op
- , (lhs:rhs:_) <- vars = translateBinaryOp ".equals(" lhs rhs ++ ")"
- | (LLt (ATInt ITBig)) <- op
- , (lhs:rhs:_) <- vars = translateBinaryOp ".lesser(" lhs rhs ++ ")"
- | (LLe (ATInt ITBig)) <- op
- , (lhs:rhs:_) <- vars = translateBinaryOp ".lesserOrEquals(" lhs rhs ++ ")"
- | (LGt (ATInt ITBig)) <- op
- , (lhs:rhs:_) <- vars = translateBinaryOp ".greater(" lhs rhs ++ ")"
- | (LGe (ATInt ITBig)) <- op
- , (lhs:rhs:_) <- vars = translateBinaryOp ".greaterOrEquals(" lhs rhs ++ ")"
+ , (lhs:rhs:_) <- vars = invokeMeth lhs "times" [rhs]
+ | (LSDiv (ATInt ITBig)) <- op
+ , (lhs:rhs:_) <- vars = invokeMeth lhs "divide" [rhs]
+ | (LSRem (ATInt ITBig)) <- op
+ , (lhs:rhs:_) <- vars = invokeMeth lhs "mod" [rhs]
+ | (LEq (ATInt ITBig)) <- op
+ , (lhs:rhs:_) <- vars = invokeMeth lhs "equals" [rhs]
+ | (LSLt (ATInt ITBig)) <- op
+ , (lhs:rhs:_) <- vars = invokeMeth lhs "lesser" [rhs]
+ | (LSLe (ATInt ITBig)) <- op
+ , (lhs:rhs:_) <- vars = invokeMeth lhs "lesserOrEquals" [rhs]
+ | (LSGt (ATInt ITBig)) <- op
+ , (lhs:rhs:_) <- vars = invokeMeth lhs "greater" [rhs]
+ | (LSGe (ATInt ITBig)) <- op
+ , (lhs:rhs:_) <- vars = invokeMeth lhs "greaterOrEquals" [rhs]
| (LPlus ATFloat) <- op
- , (lhs:rhs:_) <- vars = translateBinaryOp "+" lhs rhs
+ , (lhs:rhs:_) <- vars = translateBinaryOp "+" lhs rhs
| (LMinus ATFloat) <- op
- , (lhs:rhs:_) <- vars = translateBinaryOp "-" lhs rhs
+ , (lhs:rhs:_) <- vars = translateBinaryOp "-" lhs rhs
| (LTimes ATFloat) <- op
- , (lhs:rhs:_) <- vars = translateBinaryOp "*" lhs rhs
+ , (lhs:rhs:_) <- vars = translateBinaryOp "*" lhs rhs
| (LSDiv ATFloat) <- op
- , (lhs:rhs:_) <- vars = translateBinaryOp "/" lhs rhs
- | (LEq ATFloat) <- op
- , (lhs:rhs:_) <- vars = translateBinaryOp "==" lhs rhs
- | (LLt ATFloat) <- op
- , (lhs:rhs:_) <- vars = translateBinaryOp "<" lhs rhs
- | (LLe ATFloat) <- op
- , (lhs:rhs:_) <- vars = translateBinaryOp "<=" lhs rhs
- | (LGt ATFloat) <- op
- , (lhs:rhs:_) <- vars = translateBinaryOp ">" lhs rhs
- | (LGe ATFloat) <- op
- , (lhs:rhs:_) <- vars = translateBinaryOp ">=" lhs rhs
+ , (lhs:rhs:_) <- vars = translateBinaryOp "/" lhs rhs
+ | (LEq ATFloat) <- op
+ , (lhs:rhs:_) <- vars = translateBinaryOp "==" lhs rhs
+ | (LSLt ATFloat) <- op
+ , (lhs:rhs:_) <- vars = translateBinaryOp "<" lhs rhs
+ | (LSLe ATFloat) <- op
+ , (lhs:rhs:_) <- vars = translateBinaryOp "<=" lhs rhs
+ | (LSGt ATFloat) <- op
+ , (lhs:rhs:_) <- vars = translateBinaryOp ">" lhs rhs
+ | (LSGe ATFloat) <- op
+ , (lhs:rhs:_) <- vars = translateBinaryOp ">=" lhs rhs
| (LPlus _) <- op
, (lhs:rhs:_) <- vars = translateBinaryOp "+" lhs rhs
@@ -260,13 +533,13 @@
, (lhs:rhs:_) <- vars = translateBinaryOp "%" lhs rhs
| (LEq _) <- op
, (lhs:rhs:_) <- vars = translateBinaryOp "==" lhs rhs
- | (LLt _) <- op
+ | (LSLt _) <- op
, (lhs:rhs:_) <- vars = translateBinaryOp "<" lhs rhs
- | (LLe _) <- op
+ | (LSLe _) <- op
, (lhs:rhs:_) <- vars = translateBinaryOp "<=" lhs rhs
- | (LGt _) <- op
+ | (LSGt _) <- op
, (lhs:rhs:_) <- vars = translateBinaryOp ">" lhs rhs
- | (LGe _) <- op
+ | (LSGe _) <- op
, (lhs:rhs:_) <- vars = translateBinaryOp ">=" lhs rhs
| (LAnd _) <- op
, (lhs:rhs:_) <- vars = translateBinaryOp "&" lhs rhs
@@ -279,7 +552,7 @@
| (LASHR _) <- op
, (lhs:rhs:_) <- vars = translateBinaryOp ">>" rhs lhs
| (LCompl _) <- op
- , (arg:_) <- vars = '~' : translateVariableName arg
+ , (arg:_) <- vars = JSRaw $ '~' : translateVariableName arg
| LStrConcat <- op
, (lhs:rhs:_) <- vars = translateBinaryOp "+" lhs rhs
@@ -288,233 +561,202 @@
| LStrLt <- op
, (lhs:rhs:_) <- vars = translateBinaryOp "<" lhs rhs
| LStrLen <- op
- , (arg:_) <- vars = translateVariableName arg ++ ".length"
+ , (arg:_) <- vars = JSProj (JSVar arg) "length"
- | (LStrInt ITNative) <- op
- , (arg:_) <- vars = "parseInt(" ++ translateVariableName arg ++ ")"
- | (LIntStr ITNative) <- op
- , (arg:_) <- vars = "String(" ++ translateVariableName arg ++ ")"
- | (LSExt ITNative ITBig) <- op
- , (arg:_) <- vars = idrRTNamespace ++ "bigInt(" ++ translateVariableName arg ++ ")"
+ | (LStrInt ITNative) <- op
+ , (arg:_) <- vars = jsCall "parseInt" [JSVar arg]
+ | (LIntStr ITNative) <- op
+ , (arg:_) <- vars = jsCall "String" [JSVar arg]
+ | (LSExt ITNative ITBig) <- op
+ , (arg:_) <- vars = jsBigInt $ JSVar arg
| (LTrunc ITBig ITNative) <- op
- , (arg:_) <- vars = translateVariableName arg ++ ".valueOf()"
- | (LIntStr ITBig) <- op
- , (arg:_) <- vars = translateVariableName arg ++ ".toString()"
- | (LStrInt ITBig) <- op
- , (arg:_) <- vars = idrRTNamespace ++ "bigInt(" ++ translateVariableName arg ++ ")"
- | LFloatStr <- op
- , (arg:_) <- vars = "String(" ++ translateVariableName arg ++ ")"
- | LStrFloat <- op
- , (arg:_) <- vars = "parseFloat(" ++ translateVariableName arg ++ ")"
- | (LIntFloat ITNative) <- op
- , (arg:_) <- vars = translateVariableName arg
- | (LFloatInt ITNative) <- op
- , (arg:_) <- vars = translateVariableName arg
- | (LChInt ITNative) <- op
- , (arg:_) <- vars = translateVariableName arg ++ ".charCodeAt(0)"
- | (LIntCh ITNative) <- op
- , (arg:_) <- vars =
- "String.fromCharCode(" ++ translateVariableName arg ++ ")"
+ , (arg:_) <- vars = jsMeth (JSVar arg) "valueOf" []
+ | (LIntStr ITBig) <- op
+ , (arg:_) <- vars = jsMeth (JSVar arg) "toString" []
+ | (LStrInt ITBig) <- op
+ , (arg:_) <- vars = jsBigInt $ JSVar arg
+ | LFloatStr <- op
+ , (arg:_) <- vars = jsCall "String" [JSVar arg]
+ | LStrFloat <- op
+ , (arg:_) <- vars = jsCall "parseFloat" [JSVar arg]
+ | (LIntFloat ITNative) <- op
+ , (arg:_) <- vars = JSVar arg
+ | (LFloatInt ITNative) <- op
+ , (arg:_) <- vars = JSVar arg
+ | (LChInt ITNative) <- op
+ , (arg:_) <- vars = JSProj (JSVar arg) "charCodeAt(0)"
+ | (LIntCh ITNative) <- op
+ , (arg:_) <- vars = jsCall "String.fromCharCode" [JSVar arg]
| LFExp <- op
- , (arg:_) <- vars = "Math.exp(" ++ translateVariableName arg ++ ")"
+ , (arg:_) <- vars = jsCall "Math.exp" [JSVar arg]
| LFLog <- op
- , (arg:_) <- vars = "Math.log(" ++ translateVariableName arg ++ ")"
+ , (arg:_) <- vars = jsCall "Math.log" [JSVar arg]
| LFSin <- op
- , (arg:_) <- vars = "Math.sin(" ++ translateVariableName arg ++ ")"
+ , (arg:_) <- vars = jsCall "Math.sin" [JSVar arg]
| LFCos <- op
- , (arg:_) <- vars = "Math.cos(" ++ translateVariableName arg ++ ")"
+ , (arg:_) <- vars = jsCall "Math.cos" [JSVar arg]
| LFTan <- op
- , (arg:_) <- vars = "Math.tan(" ++ translateVariableName arg ++ ")"
+ , (arg:_) <- vars = jsCall "Math.tan" [JSVar arg]
| LFASin <- op
- , (arg:_) <- vars = "Math.asin(" ++ translateVariableName arg ++ ")"
+ , (arg:_) <- vars = jsCall "Math.asin" [JSVar arg]
| LFACos <- op
- , (arg:_) <- vars = "Math.acos(" ++ translateVariableName arg ++ ")"
+ , (arg:_) <- vars = jsCall "Math.acos" [JSVar arg]
| LFATan <- op
- , (arg:_) <- vars = "Math.atan(" ++ translateVariableName arg ++ ")"
+ , (arg:_) <- vars = jsCall "Math.atan" [JSVar arg]
| LFSqrt <- op
- , (arg:_) <- vars = "Math.sqrt(" ++ translateVariableName arg ++ ")"
+ , (arg:_) <- vars = jsCall "Math.sqrt" [JSVar arg]
| LFFloor <- op
- , (arg:_) <- vars = "Math.floor(" ++ translateVariableName arg ++ ")"
+ , (arg:_) <- vars = jsCall "Math.floor" [JSVar arg]
| LFCeil <- op
- , (arg:_) <- vars = "Math.ceil(" ++ translateVariableName arg ++ ")"
+ , (arg:_) <- vars = jsCall "Math.ceil" [JSVar arg]
| LStrCons <- op
, (lhs:rhs:_) <- vars = translateBinaryOp "+" lhs rhs
| LStrHead <- op
- , (arg:_) <- vars = translateVariableName arg ++ "[0]"
+ , (arg:_) <- vars = JSIndex (JSVar arg) (JSRaw "0")
| LStrRev <- op
- , (arg:_) <- vars = let v = translateVariableName arg in
- v ++ ".split('').reverse().join('')"
+ , (arg:_) <- vars = JSProj (JSVar arg) "split('').reverse().join('')"
| LStrIndex <- op
- , (lhs:rhs:_) <- vars = let l = translateVariableName lhs
- r = translateVariableName rhs in
- l ++ "[" ++ r ++ "]"
+ , (lhs:rhs:_) <- vars = JSIndex (JSVar lhs) (JSVar rhs)
| LStrTail <- op
, (arg:_) <- vars = let v = translateVariableName arg in
- v ++ ".substr(1," ++ v ++ ".length-1)"
+ JSRaw $ v ++ ".substr(1," ++ v ++ ".length-1)"
where
- translateBinaryOp :: String -> LVar -> LVar -> String
- translateBinaryOp f lhs rhs =
- translateVariableName lhs
- ++ f
- ++ translateVariableName rhs
+ translateBinaryOp :: String -> LVar -> LVar -> JS
+ translateBinaryOp f lhs rhs = JSOp f (JSVar lhs) (JSVar rhs)
+ invokeMeth :: LVar -> String -> [LVar] -> JS
+ invokeMeth obj meth args = jsMeth (JSVar obj) meth (map JSVar args)
+
translateExpression (SError msg) =
- "(function(){throw \'" ++ msg ++ "\';})()"
+ JSError msg
translateExpression (SForeign _ _ "putStr" [(FString, var)]) =
- idrRTNamespace ++ "print(" ++ translateVariableName var ++ ")"
-
-translateExpression (SForeign _ _ fun args)
- | "[]=" `isSuffixOf` fun
- , (obj:idx:val:[]) <- args =
- concat [object obj, index idx, assign val]
-
- | "[]" `isSuffixOf` fun
- , (obj:idx:[]) <- args =
- object obj ++ index idx
-
- | "[" `isPrefixOf` fun && "]=" `isSuffixOf` fun
- , (obj:val:[]) <- args =
- concat [object obj, '[' : name ++ "]", assign val]
-
- | "[" `isPrefixOf` fun && "]" `isSuffixOf` fun
- , (obj:[]) <- args =
- object obj ++ '[' : name ++ "]"
-
- | "." `isPrefixOf` fun, "=" `isSuffixOf` fun
- , (obj:val:[]) <- args =
- concat [object obj, field, assign val]
-
- | "." `isPrefixOf` fun
- , (obj:[]) <- args =
- object obj ++ field
-
- | "." `isPrefixOf` fun
- , (obj:[(FUnit, _)]) <- args =
- concat [object obj, method, "()"]
-
- | "." `isPrefixOf` fun
- , (obj:as) <- args =
- concat [object obj, method, arguments as]
-
- | "[]=" `isSuffixOf` fun
- , (idx:val:[]) <- args =
- concat [array, index idx, assign val]
-
- | "[]" `isSuffixOf` fun
- , (idx:[]) <- args =
- array ++ index idx
+ jsCall (idrRTNamespace ++ "print") [JSVar var]
- | otherwise = fun ++ arguments args
+translateExpression (SForeign _ _ fun args) =
+ ffi fun (map generateWrapper args)
where
- name = filter (`notElem` "[]=") fun
- method = name
- field = name
- array = name
- object o = translateVariableName (snd o)
- index i = "[" ++ translateVariableName (snd i) ++ "]"
- assign v = '=' : generateWrapper v
- arguments as =
- '(' : intercalate "," (map generateWrapper as) ++ ")"
-
generateWrapper (ffunc, name)
- | FFunction <- ffunc = idrRTNamespace ++ "ffiWrap(" ++ translateVariableName name ++ ")"
- | FFunctionIO <- ffunc = idrRTNamespace ++ "ffiWrap(" ++ translateVariableName name ++ ")"
+ | FFunction <- ffunc =
+ idrRTNamespace ++ "ffiWrap(" ++ translateVariableName name ++ ")"
+ | FFunctionIO <- ffunc =
+ idrRTNamespace ++ "ffiWrap(" ++ translateVariableName name ++ ")"
generateWrapper (_, name) =
translateVariableName name
-translateExpression (SChkCase var cases) =
- "(function(e){\n"
- ++ intercalate " else " (map (translateCase "e") cases)
- ++ "\n})("
- ++ translateVariableName var
- ++ ")"
+translateExpression patterncase
+ | (SChkCase var cases) <- patterncase = caseHelper var cases "chk"
+ | (SCase var cases) <- patterncase = caseHelper var cases "cse"
+ where
+ caseHelper var cases param =
+ JSApp (JSFunction [param] (
+ JSCond $ map (expandCase param . translateCaseCond param) cases
+ )) [JSVar var]
-translateExpression (SCase var cases) =
- "(function(e){\n"
- ++ intercalate " else " (map (translateCase "e") cases)
- ++ "\n})("
- ++ translateVariableName var
- ++ ")"
+ expandCase :: String -> (Cond, JS) -> (JS, JS)
+ expandCase _ (RawCond cond, branch) = (cond, branch)
+ expandCase _ (CaseCond DefaultCase, branch) = (JSTrue , branch)
+ expandCase var (CaseCond caseTy, branch)
+ | ConCase tag <- caseTy =
+ let checkCon = JSRaw var `jsInstanceOf` jsCon
+ checkTag = (JSRaw $ show tag) `jsEq` jsTag (JSRaw var) in
+ (checkCon `jsAnd` checkTag, branch)
+ | TypeCase ty <- caseTy =
+ let checkTy = JSRaw var `jsInstanceOf` jsType
+ checkTag = jsTypeTag (JSRaw var) `jsEq` JSType ty in
+ (checkTy `jsAnd` checkTag, branch)
+
translateExpression (SCon i name vars) =
- concat [ "new " ++ idrRTNamespace ++ "Con("
- , show i
- , ",["
- , intercalate "," $ map translateVariableName vars
- , "])"
- ]
+ JSNew (idrRTNamespace ++ "Con") [ JSRaw $ show i
+ , JSArray $ map JSVar vars
+ ]
translateExpression (SUpdate var e) =
- translateVariableName var ++ " = " ++ translateExpression e
+ JSAssign (JSVar var) (translateExpression e)
translateExpression (SProj var i) =
- translateVariableName var ++ ".vars[" ++ show i ++"]"
+ JSIndex (JSProj (JSVar var) "vars") (JSRaw $ show i)
-translateExpression SNothing = "null"
+translateExpression SNothing = JSNull
translateExpression e =
- "(function(){throw 'Not yet implemented: "
- ++ filter (/= '\'') (show e)
- ++ "';})()"
+ JSError $ "Not yet implemented: " ++ filter (/= '\'') (show e)
-translateCase :: String -> SAlt -> String
-translateCase _ (SDefaultCase e) =
- createIfBlock "true" (translateExpression e)
+data FFI = FFICode Char | FFIArg Int | FFIError String
-translateCase var (SConstCase ty e)
- | StrType <- ty = matchHelper "String"
- | PtrType <- ty = matchHelper "Ptr"
- | Forgot <- ty = matchHelper "Forgot"
- | (AType ATFloat) <- ty = matchHelper "Float"
- | (AType (ATInt ITBig)) <- ty = matchHelper "Integer"
- | (AType (ATInt ITNative)) <- ty = matchHelper "Int"
- | (AType (ATInt ITChar)) <- ty = matchHelper "Char"
+ffi :: String -> [String] -> JS
+ffi code args = let parsed = ffiParse code in
+ case ffiError parsed of
+ Just err -> JSError err
+ Nothing -> JSRaw $ renderFFI parsed args
where
- matchHelper tyName = translateTypeMatch var tyName e
+ ffiParse :: String -> [FFI]
+ ffiParse "" = []
+ ffiParse ['%'] = [FFIError "Invalid positional argument"]
+ ffiParse ('%':'%':ss) = FFICode '%' : ffiParse ss
+ ffiParse ('%':s:ss)
+ | isDigit s =
+ FFIArg (read $ s : takeWhile isDigit ss) : ffiParse (dropWhile isDigit ss)
+ | otherwise =
+ [FFIError "Invalid positional argument"]
+ ffiParse (s:ss) = FFICode s : ffiParse ss
-translateCase var (SConstCase cst@(BI _) e) =
- let cond = idrRTNamespace ++ "bigInt(" ++ var ++ ").equals(" ++ translateConstant cst ++ ")" in
- createIfBlock cond (translateExpression e)
+ ffiError :: [FFI] -> Maybe String
+ ffiError [] = Nothing
+ ffiError ((FFIError s):xs) = Just s
+ ffiError (x:xs) = ffiError xs
-translateCase var (SConstCase cst e) =
- let cond = var ++ " == " ++ translateConstant cst in
- createIfBlock cond (translateExpression e)
+ renderFFI :: [FFI] -> [String] -> String
+ renderFFI [] _ = ""
+ renderFFI ((FFICode c) : fs) args = c : renderFFI fs args
+ renderFFI ((FFIArg i) : fs) args
+ | i < length args && i >= 0 = args !! i ++ renderFFI fs args
+ | otherwise = "Argument index out of bounds"
-translateCase var (SConCase a i name vars e) =
- let isCon = var ++ " instanceof " ++ idrRTNamespace ++ "Con"
- isI = show i ++ " == " ++ var ++ ".i"
- params = intercalate "," $ map (("__var_" ++) . show) [a..(a+length vars)]
- args = ".apply(this," ++ var ++ ".vars)"
- f b =
- "(function("
- ++ params
- ++ "){\nreturn " ++ b ++ "\n})" ++ args
- cond = intercalate " && " [isCon, isI] in
- createIfBlock cond $ f (translateExpression e)
+data CaseType = ConCase Int
+ | TypeCase JSType
+ | DefaultCase
+ deriving Eq
-translateTypeMatch :: String -> String -> SExp -> String
-translateTypeMatch var ty exp =
- let e = translateExpression exp in
- createIfBlock (var
- ++ " instanceof " ++ idrRTNamespace ++ "Type && "
- ++ var ++ ".type == '"++ ty ++"'") e
+data Cond = CaseCond CaseType
+ | RawCond JS
+translateCaseCond :: String -> SAlt -> (Cond, JS)
+translateCaseCond _ cse@(SDefaultCase _) =
+ (CaseCond DefaultCase, translateCase Nothing cse)
-createIfBlock cond e =
- "if (" ++ cond ++") {\n"
- ++ "return " ++ e
- ++ ";\n}"
+translateCaseCond var cse@(SConstCase ty _)
+ | StrType <- ty = matchHelper JSStringTy
+ | PtrType <- ty = matchHelper JSPtrTy
+ | Forgot <- ty = matchHelper JSForgotTy
+ | (AType ATFloat) <- ty = matchHelper JSFloatTy
+ | (AType (ATInt ITBig)) <- ty = matchHelper JSIntegerTy
+ | (AType (ATInt ITNative)) <- ty = matchHelper JSIntTy
+ | (AType (ATInt ITChar)) <- ty = matchHelper JSCharTy
+ where
+ matchHelper :: JSType -> (Cond, JS)
+ matchHelper ty = (CaseCond $ TypeCase ty, translateCase Nothing cse)
-createTailcall call =
- idrRTNamespace ++ "tailcall(function(){return " ++ call ++ "})"
+translateCaseCond var cse@(SConstCase cst@(BI _) _) =
+ let cond = jsMeth (JSRaw var) "equals" [translateConstant cst] in
+ (RawCond cond, translateCase Nothing cse)
-translateFunctionCall name vars =
- translateNamespace name
- ++ translateName name
- ++ "("
- ++ intercalate "," (map translateVariableName vars)
- ++ ")"
+translateCaseCond var cse@(SConstCase cst _) =
+ let cond = JSRaw var `jsEq` translateConstant cst in
+ (RawCond cond, translateCase Nothing cse)
+
+translateCaseCond var cse@(SConCase _ tag _ _ _) =
+ (CaseCond $ ConCase tag, translateCase (Just var) cse)
+
+translateCase :: Maybe String -> SAlt -> JS
+translateCase _ (SDefaultCase e) = translateExpression e
+translateCase _ (SConstCase _ e) = translateExpression e
+translateCase (Just var) (SConCase a _ _ vars e) =
+ let params = map jsVar [a .. (a + length vars)] in
+ jsMeth (JSFunction params (JSReturn $ translateExpression e)) "apply" [
+ JSThis, JSProj (JSRaw var) "vars"
+ ]
diff --git a/src/IRTS/CodegenLLVM.hs b/src/IRTS/CodegenLLVM.hs
--- a/src/IRTS/CodegenLLVM.hs
+++ b/src/IRTS/CodegenLLVM.hs
@@ -389,8 +389,8 @@
alloc' :: Operand -> Codegen Operand
alloc' size = inst $ simpleCall "GC_malloc" [size]
-allocAtomic :: Operand -> Codegen Operand
-allocAtomic size = inst $ simpleCall "GC_malloc_atomic" [size]
+allocAtomic' :: Operand -> Codegen Operand
+allocAtomic' size = inst $ simpleCall "GC_malloc_atomic" [size]
alloc :: Type -> Codegen Operand
alloc ty = do
@@ -398,6 +398,12 @@
mem <- alloc' size
inst $ BitCast mem (PointerType ty (AddrSpace 0)) []
+allocAtomic :: Type -> Codegen Operand
+allocAtomic ty = do
+ size <- sizeOf ty
+ mem <- allocAtomic' size
+ inst $ BitCast mem (PointerType ty (AddrSpace 0)) []
+
sizeOf :: Type -> Codegen Operand
sizeOf ty = ConstantOperand . C.PtrToInt
(C.GetElementPtr True (C.Null (PointerType ty (AddrSpace 0))) [C.Int 32 1])
@@ -701,11 +707,14 @@
nameAlt _ (SConCase _ _ name _ _) = getName (show name)
nameAlt _ (SConstCase const _) = getName (show const)
+isHeapFTy :: FType -> Bool
+isHeapFTy f = elem f [FString, FPtr, FAny, FArith (ATInt ITBig)]
+
box :: FType -> Operand -> Codegen Operand
box FUnit _ = return $ ConstantOperand nullValue
box fty fval = do
let ty = primTy (ftyToTy fty)
- val <- alloc ty
+ val <- if isHeapFTy fty then alloc ty else allocAtomic ty
tagptr <- inst $ GetElementPtr True val [ConstantOperand (C.Int 32 0), ConstantOperand (C.Int 32 0)] []
valptr <- inst $ GetElementPtr True val [ConstantOperand (C.Int 32 0), ConstantOperand (C.Int 32 1)] []
inst' $ Store False tagptr (ConstantOperand (C.Int 32 (-1))) Nothing 0 []
@@ -860,11 +869,11 @@
cgOp (LChInt ITNative) [x] = return x
cgOp (LIntCh ITNative) [x] = return x
-cgOp (LLt (ATInt ITBig)) [x,y] = mpzCmp IPred.SLT x y
-cgOp (LLe (ATInt ITBig)) [x,y] = mpzCmp IPred.SLE x y
+cgOp (LSLt (ATInt ITBig)) [x,y] = mpzCmp IPred.SLT x y
+cgOp (LSLe (ATInt ITBig)) [x,y] = mpzCmp IPred.SLE x y
cgOp (LEq (ATInt ITBig)) [x,y] = mpzCmp IPred.EQ x y
-cgOp (LGe (ATInt ITBig)) [x,y] = mpzCmp IPred.SGE x y
-cgOp (LGt (ATInt ITBig)) [x,y] = mpzCmp IPred.SGT x y
+cgOp (LSGe (ATInt ITBig)) [x,y] = mpzCmp IPred.SGE x y
+cgOp (LSGt (ATInt ITBig)) [x,y] = mpzCmp IPred.SGT x y
cgOp (LPlus (ATInt ITBig)) [x,y] = mpzBin "add" x y
cgOp (LMinus (ATInt ITBig)) [x,y] = mpzBin "sub" x y
cgOp (LTimes (ATInt ITBig)) [x,y] = mpzBin "mul" x y
@@ -898,11 +907,15 @@
cgOp (LSExt (ITFixed from) (ITFixed to)) [x]
| nativeTyWidth from < nativeTyWidth to = iCoerce SExt from to x
-cgOp (LLt (ATInt ity)) [x,y] = iCmp ity IPred.ULT x y
-cgOp (LLe (ATInt ity)) [x,y] = iCmp ity IPred.ULE x y
+cgOp (LSLt (ATInt ity)) [x,y] = iCmp ity IPred.SLT x y
+cgOp (LSLe (ATInt ity)) [x,y] = iCmp ity IPred.SLE x y
+cgOp (LLt ity) [x,y] = iCmp ity IPred.ULT x y
+cgOp (LLe ity) [x,y] = iCmp ity IPred.ULE x y
cgOp (LEq (ATInt ity)) [x,y] = iCmp ity IPred.EQ x y
-cgOp (LGe (ATInt ity)) [x,y] = iCmp ity IPred.UGE x y
-cgOp (LGt (ATInt ity)) [x,y] = iCmp ity IPred.UGT x y
+cgOp (LSGe (ATInt ity)) [x,y] = iCmp ity IPred.SGE x y
+cgOp (LSGt (ATInt ity)) [x,y] = iCmp ity IPred.SGT x y
+cgOp (LGe ity) [x,y] = iCmp ity IPred.UGE x y
+cgOp (LGt ity) [x,y] = iCmp ity IPred.UGT x y
cgOp (LPlus (ATInt ity)) [x,y] = ibin ity x y (Add False False)
cgOp (LMinus (ATInt ity)) [x,y] = ibin ity x y (Sub False False)
cgOp (LTimes (ATInt ity)) [x,y] = ibin ity x y (Mul False False)
@@ -1072,7 +1085,7 @@
zlen <- inst $ Add False True xlen ylen []
ws <- getWordSize
total <- inst $ Add False True zlen (ConstantOperand (C.Int ws 1)) []
- mem <- allocAtomic total
+ mem <- allocAtomic' total
inst $ simpleCall "memcpy" [mem, x', xlen]
i <- inst $ PtrToInt mem (IntegerType ws) []
offi <- inst $ Add False True i xlen []
diff --git a/src/IRTS/Compiler.hs b/src/IRTS/Compiler.hs
--- a/src/IRTS/Compiler.hs
+++ b/src/IRTS/Compiler.hs
@@ -45,7 +45,9 @@
maindef <- irMain tm
objs <- getObjectFiles codegen
libs <- getLibs codegen
+ flags <- getFlags codegen
hdrs <- getHdrs codegen
+ impdirs <- allImportDirs
let defs = defsIn ++ [(MN 0 "runMain", maindef)]
-- iputStrLn $ showSep "\n" (map show defs)
let (nexttag, tagged) = addTags 65536 (liftAll defs)
@@ -77,7 +79,9 @@
ViaC ->
codegenC c f outty hdrs
(concatMap mkObj objs)
- (concatMap mkLib libs) NONE
+ (concatMap mkLib libs)
+ (concatMap mkFlag flags ++
+ concatMap incdir impdirs) NONE
ViaJava ->
codegenJava [] c f hdrs libs outty
ViaJavaScript ->
@@ -97,7 +101,9 @@
if ex then return f else return h
mkObj f = f ++ " "
mkLib l = "-l" ++ l ++ " "
+ mkFlag l = l ++ " "
+ incdir i = "-I" ++ i ++ " "
irMain :: TT Name -> Idris LDecl
@@ -159,8 +165,10 @@
mkLDecl n (Function tm _) = do e <- ir tm
return (declArgs [] True n e)
-mkLDecl n (CaseOp _ inl _ _ pats _ _ args sc) = do e <- ir (args, sc)
- return (declArgs [] inl n e)
+mkLDecl n (CaseOp ci _ _ pats cd)
+ = let (args, sc) = cases_runtime cd in
+ do e <- ir (args, sc)
+ return (declArgs [] (case_inlinable ci) n e)
mkLDecl n (TyDecl (DCon t a) _) = return $ LConstructor n t a
mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a
mkLDecl n _ = return (LFun [] n [] (LError ("Impossible declaration " ++ show n)))
@@ -168,9 +176,9 @@
instance ToIR (TT Name) where
ir tm = ir' [] tm where
ir' env tm@(App f a)
- | (P _ (UN "mkForeign") _, args) <- unApply tm
+ | (P _ (UN "mkForeignPrim") _, args) <- unApply tm
= doForeign env args
- | (P _ (UN "unsafePerformIO") _, [_, arg]) <- unApply tm
+ | (P _ (UN "unsafePerformPrimIO") _, [_, arg]) <- unApply tm
= ir' env arg
-- TMP HACK - until we get inlining.
| (P _ (UN "replace") _, [_, _, _, _, _, arg]) <- unApply tm
@@ -183,20 +191,20 @@
| (P _ (UN "par") _, [_, arg]) <- unApply tm
= do arg' <- ir' env arg
return $ LOp LPar [LLazyExp arg']
- | (P _ (UN "fork") _, [arg]) <- unApply tm
+ | (P _ (UN "prim_fork") _, [arg]) <- unApply tm
= do arg' <- ir' env arg
return $ LOp LFork [LLazyExp arg']
- | (P _ (UN "prim__IO") _, [v]) <- unApply tm
- = do v' <- ir' env v
- return v'
- | (P _ (UN "io_bind") _, [_,_,v,Bind n (Lam _) sc]) <- unApply tm
- = do v' <- ir' env v
- sc' <- ir' (n:env) sc
- return (LLet n (LForce v') sc')
- | (P _ (UN "io_bind") _, [_,_,v,k]) <- unApply tm
- = do v' <- ir' env v
- k' <- ir' env k
- return (LApp False k' [LForce v'])
+-- | (P _ (UN "prim__IO") _, [v]) <- unApply tm
+-- = do v' <- ir' env v
+-- return v'
+-- | (P _ (UN "prim_io_bind") _, [_,_,v,Bind n (Lam _) sc]) <- unApply tm
+-- = do v' <- ir' env v
+-- sc' <- ir' (n:env) sc
+-- return (LLet n (LForce v') sc')
+-- | (P _ (UN "prim_io_bind") _, [_,_,v,k]) <- unApply tm
+-- = do v' <- ir' env v
+-- k' <- ir' env k
+-- return (LApp False k' [LForce v'])
| (P _ (UN "malloc") _, [_,size,t]) <- unApply tm
= do size' <- ir' env size
t' <- ir' env t
@@ -280,7 +288,7 @@
case maybeTys of
Nothing -> fail $ "Foreign type specification is not a constant list: " ++ show (fgn:args)
Just tys -> do
- args' <- mapM (ir' env) args
+ args' <- mapM (ir' env) (init args)
-- wrap it in a prim__IO
-- return $ con_ 0 @@ impossible @@
return $ -- LLazyExp $
@@ -344,10 +352,10 @@
ir' (STerm t) = ir t
ir' (UnmatchedCase str) = return $ LError str
- ir' (ProjCase tm alts) = do alts' <- mapM (mkIRAlt tm) alts
- tm' <- ir tm
+ ir' (ProjCase tm alts) = do tm' <- ir tm
+ alts' <- mapM (mkIRAlt tm') alts
return $ LCase tm' alts'
- ir' (Case n alts) = do alts' <- mapM (mkIRAlt (P Bound n Erased)) alts
+ ir' (Case n alts) = do alts' <- mapM (mkIRAlt (LV (Glob n))) alts
return $ LCase (LV (Glob n)) alts'
ir' ImpossibleCase = return LNothing
@@ -371,6 +379,12 @@
| matchableTy x
= do rhs' <- ir rhs
return $ LDefaultCase rhs'
+ mkIRAlt tm (SucCase n rhs)
+ = do rhs' <- ir rhs
+ return $ LDefaultCase (LLet n (LOp (LMinus (ATInt ITBig))
+ [tm,
+ LConst (BI 1)]) rhs')
+-- return $ LSucCase n rhs'
mkIRAlt _ (ConstCase c rhs)
= fail $ "Can't match on (" ++ show c ++ ")"
mkIRAlt _ (DefaultCase rhs)
diff --git a/src/IRTS/Defunctionalise.hs b/src/IRTS/Defunctionalise.hs
--- a/src/IRTS/Defunctionalise.hs
+++ b/src/IRTS/Defunctionalise.hs
@@ -286,13 +286,14 @@
tagOrd (DConCase t _ _ _) (DConCase t' _ _ _) = compare t t'
tagOrd (DConstCase c _) (DConstCase c' _) = compare c c'
tagOrd (DDefaultCase _) (DDefaultCase _) = EQ
+
tagOrd (DConCase _ _ _ _) (DDefaultCase _) = LT
tagOrd (DConCase _ _ _ _) (DConstCase _ _) = LT
tagOrd (DConstCase _ _) (DDefaultCase _) = LT
+
tagOrd (DDefaultCase _) (DConCase _ _ _ _) = GT
tagOrd (DConstCase _ _) (DConCase _ _ _ _) = GT
tagOrd (DDefaultCase _) (DConstCase _ _) = GT
-
groupsOf :: Int -> [DAlt] -> [[DAlt]]
groupsOf x [] = []
diff --git a/src/IRTS/Java/JTypes.hs b/src/IRTS/Java/JTypes.hs
--- a/src/IRTS/Java/JTypes.hs
+++ b/src/IRTS/Java/JTypes.hs
@@ -242,10 +242,14 @@
sourceTypes (LLSHR from) = [intTyToJType from, intTyToJType from]
sourceTypes (LASHR from) = [intTyToJType from, intTyToJType from]
sourceTypes (LEq from) = [arithTyToJType from, arithTyToJType from]
-sourceTypes (LLt from) = [arithTyToJType from, arithTyToJType from]
-sourceTypes (LLe from) = [arithTyToJType from, arithTyToJType from]
-sourceTypes (LGt from) = [arithTyToJType from, arithTyToJType from]
-sourceTypes (LGe from) = [arithTyToJType from, arithTyToJType from]
+sourceTypes (LSLt from) = [arithTyToJType from, arithTyToJType from]
+sourceTypes (LSLe from) = [arithTyToJType from, arithTyToJType from]
+sourceTypes (LSGt from) = [arithTyToJType from, arithTyToJType from]
+sourceTypes (LSGe from) = [arithTyToJType from, arithTyToJType from]
+sourceTypes (LLt from) = [intTyToJType from, intTyToJType from]
+sourceTypes (LLe from) = [intTyToJType from, intTyToJType from]
+sourceTypes (LGt from) = [intTyToJType from, intTyToJType from]
+sourceTypes (LGe from) = [intTyToJType from, intTyToJType from]
sourceTypes (LSExt from _) = [intTyToJType from]
sourceTypes (LZExt from _) = [intTyToJType from]
sourceTypes (LTrunc from _) = [intTyToJType from]
diff --git a/src/IRTS/Java/Mangling.hs b/src/IRTS/Java/Mangling.hs
--- a/src/IRTS/Java/Mangling.hs
+++ b/src/IRTS/Java/Mangling.hs
@@ -18,6 +18,7 @@
import qualified Language.Java.Syntax as J
import System.FilePath
+import Debug.Trace
prefixCallNamespaces :: Ident -> SDecl -> SDecl
prefixCallNamespaces name (SFun fname args i e) =
@@ -83,6 +84,9 @@
| x == ']' = "_RSBrace" ++ cleanNonLetter xs
| x == '(' = "_LBrace" ++ cleanNonLetter xs
| x == ')' = "_RBrace" ++ cleanNonLetter xs
+ | x == ':' = "_Colon" ++ cleanNonLetter xs
+ | x == ' ' = "_Space" ++ cleanNonLetter xs
+ | x == ',' = "_Comma" ++ cleanNonLetter xs
| x == '_' = "__" ++ cleanNonLetter xs
| not (isAlphaNum x) = "_" ++ (show $ ord x) ++ xs
| otherwise = x:cleanNonLetter xs
@@ -92,6 +96,7 @@
| capitalize = (toUpper x) : (cleanWs False xs)
| otherwise = x : (cleanWs False xs)
cleanWs _ [] = []
+mangleWithPrefix prefix s@(SN _) = mangleWithPrefix prefix (UN (showCG s))
mangle :: (Applicative m, MonadError String m) => Name -> m Ident
mangle = mangleWithPrefix "__IDRCG__"
diff --git a/src/IRTS/LParser.hs b/src/IRTS/LParser.hs
--- a/src/IRTS/LParser.hs
+++ b/src/IRTS/LParser.hs
@@ -60,7 +60,7 @@
-- print checked
case checked of
OK c -> case cgn of
- ViaC -> codegenC c "a.out" outty ["math.h"] "" "" TRACE
+ ViaC -> codegenC c "a.out" outty ["math.h"] "" "" "" TRACE
ViaJava -> codegenJava [] c "a.out" [] [] outty
Error e -> fail $ show e
@@ -115,26 +115,26 @@
[
binary "==" (\x y -> LOp (LEq (ATInt ITNative)) [x, y]) AssocNone,
binary "==." (\x y -> LOp (LEq ATFloat) [x, y]) AssocNone,
- binary "<" (\x y -> LOp (LLt (ATInt ITNative)) [x, y]) AssocNone,
- binary "<." (\x y -> LOp (LLt ATFloat) [x, y]) AssocNone,
- binary ">" (\x y -> LOp (LGt (ATInt ITNative)) [x, y]) AssocNone,
- binary ">." (\x y -> LOp (LGt ATFloat) [x, y]) AssocNone,
- binary "<=" (\x y -> LOp (LLe (ATInt ITNative)) [x, y]) AssocNone,
- binary "<=." (\x y -> LOp (LLe ATFloat) [x, y]) AssocNone,
- binary ">=" (\x y -> LOp (LGe (ATInt ITNative)) [x, y]) AssocNone,
- binary ">=." (\x y -> LOp (LGe ATFloat) [x, y]) AssocNone,
+ binary "<" (\x y -> LOp (LSLt (ATInt ITNative)) [x, y]) AssocNone,
+ binary "<." (\x y -> LOp (LSLt ATFloat) [x, y]) AssocNone,
+ binary ">" (\x y -> LOp (LSGt (ATInt ITNative)) [x, y]) AssocNone,
+ binary ">." (\x y -> LOp (LSGt ATFloat) [x, y]) AssocNone,
+ binary "<=" (\x y -> LOp (LSLe (ATInt ITNative)) [x, y]) AssocNone,
+ binary "<=." (\x y -> LOp (LSLe ATFloat) [x, y]) AssocNone,
+ binary ">=" (\x y -> LOp (LSGe (ATInt ITNative)) [x, y]) AssocNone,
+ binary ">=." (\x y -> LOp (LSGe ATFloat) [x, y]) AssocNone,
binary "==:" (\x y -> LOp (LEq (ATInt ITBig)) [x, y]) AssocNone,
- binary "<:" (\x y -> LOp (LLt (ATInt ITBig)) [x, y]) AssocNone,
- binary ">:" (\x y -> LOp (LGt (ATInt ITBig)) [x, y]) AssocNone,
- binary "<=:" (\x y -> LOp (LLe (ATInt ITBig)) [x, y]) AssocNone,
- binary ">=:" (\x y -> LOp (LGe (ATInt ITBig)) [x, y]) AssocNone,
+ binary "<:" (\x y -> LOp (LSLt (ATInt ITBig)) [x, y]) AssocNone,
+ binary ">:" (\x y -> LOp (LSGt (ATInt ITBig)) [x, y]) AssocNone,
+ binary "<=:" (\x y -> LOp (LSLe (ATInt ITBig)) [x, y]) AssocNone,
+ binary ">=:" (\x y -> LOp (LSGe (ATInt ITBig)) [x, y]) AssocNone,
binary "==," (\x y -> LOp (LEq (ATInt ITChar)) [x, y]) AssocNone,
- binary "<," (\x y -> LOp (LLt (ATInt ITChar)) [x, y]) AssocNone,
- binary ">," (\x y -> LOp (LGt (ATInt ITChar)) [x, y]) AssocNone,
- binary "<=," (\x y -> LOp (LLe (ATInt ITChar)) [x, y]) AssocNone,
- binary ">=," (\x y -> LOp (LGe (ATInt ITChar)) [x, y]) AssocNone
+ binary "<," (\x y -> LOp (LSLt (ATInt ITChar)) [x, y]) AssocNone,
+ binary ">," (\x y -> LOp (LSGt (ATInt ITChar)) [x, y]) AssocNone,
+ binary "<=," (\x y -> LOp (LSLe (ATInt ITChar)) [x, y]) AssocNone,
+ binary ">=," (\x y -> LOp (LSGe (ATInt ITChar)) [x, y]) AssocNone
]]
binary name f assoc = Infix (do reservedOp name; return f) assoc
diff --git a/src/IRTS/Lang.hs b/src/IRTS/Lang.hs
--- a/src/IRTS/Lang.hs
+++ b/src/IRTS/Lang.hs
@@ -32,7 +32,8 @@
| LUDiv IntTy | LSDiv ArithTy | LURem IntTy | LSRem ArithTy
| LAnd IntTy | LOr IntTy | LXOr IntTy | LCompl IntTy
| LSHL IntTy | LLSHR IntTy | LASHR IntTy
- | LEq ArithTy | LLt ArithTy | LLe ArithTy | LGt ArithTy | LGe ArithTy
+ | LEq ArithTy | LLt IntTy | LLe IntTy | LGt IntTy | LGe IntTy
+ | LSLt ArithTy | LSLe ArithTy | LSGt ArithTy | LSGe ArithTy
| LSExt IntTy IntTy | LZExt IntTy IntTy | LTrunc IntTy IntTy
| LStrConcat | LStrLt | LStrEq | LStrLen
| LIntFloat IntTy | LFloatInt IntTy | LIntStr IntTy | LStrInt IntTy
diff --git a/src/Idris/AbsSyntax.hs b/src/Idris/AbsSyntax.hs
--- a/src/Idris/AbsSyntax.hs
+++ b/src/Idris/AbsSyntax.hs
@@ -9,6 +9,7 @@
import Core.Typecheck
import Idris.AbsSyntaxTree
import Idris.IdeSlave
+import Idris.Colours
import IRTS.CodegenCommon
import Util.DynamicLinker
@@ -21,6 +22,7 @@
import Data.List
import Data.Char
import Data.Either
+import Data.Maybe
import Debug.Trace
@@ -37,26 +39,40 @@
getObjectFiles tgt = do i <- getIState; return (forCodegen tgt $ idris_objs i)
addObjectFile :: Codegen -> FilePath -> Idris ()
-addObjectFile tgt f = do i <- getIState; putIState $ i { idris_objs = (tgt, f) : idris_objs i }
+addObjectFile tgt f = do i <- getIState; putIState $ i { idris_objs = nub $ (tgt, f) : idris_objs i }
getLibs :: Codegen -> Idris [String]
getLibs tgt = do i <- getIState; return (forCodegen tgt $ idris_libs i)
addLib :: Codegen -> String -> Idris ()
-addLib tgt f = do i <- getIState; putIState $ i { idris_libs = (tgt, f) : idris_libs i }
+addLib tgt f = do i <- getIState; putIState $ i { idris_libs = nub $ (tgt, f) : idris_libs i }
+getFlags :: Codegen -> Idris [String]
+getFlags tgt = do i <- getIState; return (forCodegen tgt $ idris_cgflags i)
+
+addFlag :: Codegen -> String -> Idris ()
+addFlag tgt f = do i <- getIState; putIState $ i { idris_cgflags = nub $ (tgt, f) : idris_cgflags i }
+
addDyLib :: [String] -> Idris (Either DynamicLib String)
addDyLib libs = do i <- getIState
- handle <- lift $ mapM (\l -> catchIO (tryLoadLib l) (\_ -> return Nothing)) libs
- case msum handle of
- Nothing -> return (Right $ "Could not load dynamic alternatives \"" ++
- concat (intersperse "," libs) ++ "\"")
- Just x -> do let ls = idris_dynamic_libs i
- putIState $ i { idris_dynamic_libs = x:ls }
- return (Left x)
+ let ls = idris_dynamic_libs i
+ case mapMaybe (findDyLib ls) libs of
+ x:_ -> return (Left x)
+ [] -> do
+ handle <- lift $ mapM (\l -> catchIO (tryLoadLib l) (\_ -> return Nothing)) $ libs
+ case msum handle of
+ Nothing -> return (Right $ "Could not load dynamic alternatives \"" ++
+ concat (intersperse "," libs) ++ "\"")
+ Just x -> do putIState $ i { idris_dynamic_libs = x:ls }
+ return (Left x)
+ where findDyLib :: [DynamicLib] -> String -> Maybe DynamicLib
+ findDyLib [] l = Nothing
+ findDyLib (lib:libs) l | l == lib_name lib = Just lib
+ | otherwise = findDyLib libs l
+
addHdr :: Codegen -> String -> Idris ()
-addHdr tgt f = do i <- getIState; putIState $ i { idris_hdrs = (tgt, f) : idris_hdrs i }
+addHdr tgt f = do i <- getIState; putIState $ i { idris_hdrs = nub $ (tgt, f) : idris_hdrs i }
addLangExt :: LanguageExt -> Idris ()
addLangExt TypeProviders = do i <- getIState ; putIState $ i { idris_language_extensions = [TypeProviders] }
@@ -68,6 +84,9 @@
totcheck :: (FC, Name) -> Idris ()
totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }
+clear_totcheck :: Idris ()
+clear_totcheck = do i <- getIState; putIState $ i { idris_totcheck = [] }
+
setFlags :: Name -> [FnOpt] -> Idris ()
setFlags n fs = do i <- getIState; putIState $ i { idris_flags = addDef n fs (idris_flags i) }
@@ -112,7 +131,7 @@
addCoercion :: Name -> Idris ()
addCoercion n = do i <- getIState
- putIState $ i { idris_coercions = n : idris_coercions i }
+ putIState $ i { idris_coercions = nub $ n : idris_coercions i }
addDocStr :: Name -> String -> Idris ()
addDocStr n doc
@@ -318,6 +337,10 @@
let iopts = idris_options i
putIState $ i { idris_options = iopts { opt_cmdline = opts } }
+getCmdLine :: Idris [Opt]
+getCmdLine = do i <- getIState
+ return (opt_cmdline (idris_options i))
+
getDumpDefun :: Idris (Maybe FilePath)
getDumpDefun = do i <- getIState
return $ findC (opt_cmdline (idris_options i))
@@ -473,10 +496,19 @@
let opt' = opts { opt_importdirs = fps }
putIState $ i { idris_options = opt' }
-allImportDirs :: IState -> Idris [FilePath]
-allImportDirs i = do let optdirs = opt_importdirs (idris_options i)
- return ("." : reverse optdirs)
+allImportDirs :: Idris [FilePath]
+allImportDirs = do i <- getIState
+ let optdirs = opt_importdirs (idris_options i)
+ return ("." : reverse optdirs)
+colourise :: Idris Bool
+colourise = do i <- getIState
+ return $ idris_colourRepl i
+
+setColourise :: Bool -> Idris ()
+setColourise b = do i <- getIState
+ putIState $ i { idris_colourRepl = b }
+
impShow :: Idris Bool
impShow = do i <- getIState
return (opt_showimp (idris_options i))
@@ -487,6 +519,18 @@
let opt' = opts { opt_showimp = t }
putIState $ i { idris_options = opt' }
+setColour :: ColourType -> IdrisColour -> Idris ()
+setColour ct c = do i <- getIState
+ let newTheme = setColour' ct c (idris_colourTheme i)
+ putIState $ i { idris_colourTheme = newTheme }
+ where setColour' KeywordColour c t = t { keywordColour = c }
+ setColour' BoundVarColour c t = t { boundVarColour = c }
+ setColour' ImplicitColour c t = t { implicitColour = c }
+ setColour' FunctionColour c t = t { functionColour = c }
+ setColour' TypeColour c t = t { typeColour = c }
+ setColour' DataColour c t = t { dataColour = c }
+ setColour' PromptColour c t = t { promptColour = c }
+
logLvl :: Int -> String -> Idris ()
logLvl l str = do i <- getIState
let lvl = opt_logLevel (idris_options i)
@@ -605,20 +649,25 @@
mkShadow (NS x s) = NS (mkShadow x) s
en (PLam n t s)
- | n `elem` map fst ps
+ | n `elem` (map fst ps ++ ns)
= let n' = mkShadow n in
PLam n' (en t) (en (shadow n n' s))
| otherwise = PLam n (en t) (en s)
en (PPi p n t s)
- | n `elem` map fst ps
+ | n `elem` (map fst ps ++ ns)
= let n' = mkShadow n in
PPi p n' (en t) (en (shadow n n' s))
| otherwise = PPi p n (en t) (en s)
en (PLet n ty v s)
- | n `elem` map fst ps
+ | n `elem` (map fst ps ++ ns)
= let n' = mkShadow n in
PLet n' (en ty) (en v) (en (shadow n n' s))
| otherwise = PLet n (en ty) (en v) (en s)
+ -- FIXME: Should only do this in a type signature!
+ en (PDPair f (PRef f' n) t r)
+ | n `elem` (map fst ps ++ ns) && t /= Placeholder
+ = let n' = mkShadow n in
+ PDPair f (PRef f' n') (en t) (en (shadow n n' r))
en (PEq f l r) = PEq f (en l) (en r)
en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)
en (PTyped l r) = PTyped (en l) (en r)
@@ -683,24 +732,36 @@
= let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
- n' = if n `elem` ns then dec n else n in
+ n' = if n `elem` ns then dec n else n
+ -- names bound on the lhs should not be expanded on the rhs
+ ns' = removeBound lhs ns in
PClause fc n' lhs'
- (map (expandParams dec ps'' ns []) ws)
- (expandParams dec ps'' ns [] rhs)
- (map (expandParamsD True ist dec ps'' ns) ds)
+ (map (expandParams dec ps'' ns' []) ws)
+ (expandParams dec ps'' ns' [] rhs)
+ (map (expandParamsD True ist dec ps'' ns') ds)
expandParamsC (PWith fc n lhs ws wval ds)
= let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
- n' = if n `elem` ns then dec n else n in
+ n' = if n `elem` ns then dec n else n
+ ns' = removeBound lhs ns in
PWith fc n' lhs'
- (map (expandParams dec ps'' ns []) ws)
- (expandParams dec ps'' ns [] wval)
- (map (expandParamsD rhsonly ist dec ps'' ns) ds)
+ (map (expandParams dec ps'' ns' []) ws)
+ (expandParams dec ps'' ns' [] wval)
+ (map (expandParamsD rhsonly ist dec ps'' ns') ds)
updateps yn nm [] = []
updateps yn nm (((a, t), i):as)
| (a `elem` nm) == yn = (a, t) : updateps yn nm as
| otherwise = (MN i (show n ++ "_u"), t) : updateps yn nm as
+
+ removeBound lhs ns = ns \\ nub (bnames lhs)
+
+ bnames (PRef _ n) = [n]
+ bnames (PApp _ _ args) = concatMap bnames (map getTm args)
+ bnames (PPair _ l r) = bnames l ++ bnames r
+ bnames (PDPair _ l Placeholder r) = bnames l ++ bnames r
+ bnames _ = []
+
expandParamsD rhs ist dec ps ns (PData doc syn fc co pd)
= PData doc syn fc co (expandPData pd)
where
@@ -1023,9 +1084,13 @@
ai env (PPi p n ty sc) = let ty' = ai env ty
sc' = ai ((n, Just ty):env) sc in
PPi p n ty' sc'
+ ai env (PGoal fc r n sc) = let r' = ai env r
+ sc' = ai ((n, Nothing):env) sc in
+ PGoal fc r' n sc'
ai env (PHidden tm) = PHidden (ai env tm)
ai env (PProof ts) = PProof (map (fmap (ai env)) ts)
ai env (PTactics ts) = PTactics (map (fmap (ai env)) ts)
+ ai env (PRefl fc tm) = PRefl fc (ai env tm)
ai env (PUnifyLog tm) = PUnifyLog (ai env tm)
ai env tm = tm
@@ -1145,7 +1210,7 @@
-- FIXME: It's possible that this really has to happen after elaboration
findStatics :: IState -> PTerm -> (PTerm, [Bool])
-findStatics ist tm = trace (showImp True tm) $
+findStatics ist tm = trace (showImp Nothing True False tm) $
let (ns, ss) = fs tm in
runState (pos ns ss tm) []
where fs (PPi p n t sc)
@@ -1176,7 +1241,7 @@
dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
-dumpDecl (PTy _ _ _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
+dumpDecl (PTy _ _ _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp Nothing True False t
dumpDecl (PClauses _ _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)
dumpDecl (PData _ _ _ _ d) = showDImp True d
dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
diff --git a/src/Idris/AbsSyntaxTree.hs b/src/Idris/AbsSyntaxTree.hs
--- a/src/Idris/AbsSyntaxTree.hs
+++ b/src/Idris/AbsSyntaxTree.hs
@@ -12,10 +12,13 @@
import Util.Pretty
import Util.DynamicLinker
+import Idris.Colours
+
import Paths_idris
import System.Console.Haskeline
+
import Control.Monad.Trans.State.Strict
import Data.List
@@ -28,7 +31,7 @@
opt_typecase :: Bool,
opt_typeintype :: Bool,
opt_coverage :: Bool,
- opt_showimp :: Bool,
+ opt_showimp :: Bool, -- ^^ show implicits
opt_errContext :: Bool,
opt_repl :: Bool,
opt_verbose :: Bool,
@@ -104,6 +107,7 @@
idris_scprims :: [(Name, (Int, PrimFn))],
idris_objs :: [(Codegen, FilePath)],
idris_libs :: [(Codegen, String)],
+ idris_cgflags :: [(Codegen, String)],
idris_hdrs :: [(Codegen, String)],
proof_list :: [(Name, [String])],
errLine :: Maybe Int,
@@ -117,7 +121,9 @@
compiled_so :: Maybe String,
idris_dynamic_libs :: [DynamicLib],
idris_language_extensions :: [LanguageExt],
- idris_outputmode :: OutputMode
+ idris_outputmode :: OutputMode,
+ idris_colourRepl :: Bool,
+ idris_colourTheme :: ColourTheme
}
data SizeChange = Smaller | Same | Bigger | Unknown
@@ -138,7 +144,10 @@
deriving instance Binary CGInfo
!-}
-primDefs = [UN "unsafePerformIO", UN "mkLazyForeign", UN "mkForeign", UN "FalseElim"]
+primDefs = [UN "unsafePerformPrimIO",
+ UN "mkLazyForeignPrim",
+ UN "mkForeignPrim",
+ UN "FalseElim"]
-- information that needs writing for the current module's .ibc file
data IBCWrite = IBCFix FixDecl
@@ -154,6 +163,7 @@
| IBCImport FilePath
| IBCObj Codegen FilePath
| IBCLib Codegen String
+ | IBCCGFlag Codegen String
| IBCDyLib String
| IBCHeader Codegen String
| IBCAccess Name Accessibility
@@ -169,8 +179,9 @@
idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
emptyContext emptyContext emptyContext emptyContext
emptyContext emptyContext emptyContext emptyContext
- [] "" defaultOpts 6 [] [] [] [] [] [] [] [] [] []
+ [] "" defaultOpts 6 [] [] [] [] [] [] [] [] [] [] []
[] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput
+ True defaultTheme
-- | The monad for the main REPL - reading and processing files and updating
-- global state (hence the IO inner monad).
@@ -202,7 +213,6 @@
| Compile Codegen String
| Execute
| ExecVal PTerm
- | NewCompile String
| Metavars
| Prove Name
| AddProof (Maybe Name)
@@ -225,11 +235,15 @@
| SetOpt Opt
| UnsetOpt Opt
| NOP
+ | SetColour ColourType IdrisColour
+ | ColourOn
+ | ColourOff
data Opt = Filename String
| Ver
| Usage
| Quiet
+ | ColourREPL Bool
| Ideslave
| ShowLibs
| ShowLibdir
@@ -238,14 +252,13 @@
| NoREPL
| OLogging Int
| Output String
- | NewOutput String
| TypeCase
| TypeInType
| DefaultTotal
| DefaultPartial
| WarnPartial
- | NoCoverage
- | ErrContext
+ | NoCoverage
+ | ErrContext
| ShowImpl
| Verbose
| IBCSubDir String
@@ -330,10 +343,14 @@
constraint = Constraint False Dynamic ""
tacimpl t = TacImp False Dynamic t ""
-data FnOpt = Inlinable | TotalFn | PartialFn
- | Coinductive | AssertTotal | TCGen
+data FnOpt = Inlinable -- always evaluate when simplifying
+ | TotalFn | PartialFn
+ | Coinductive | AssertTotal
+ | Dictionary -- type class dictionary, eval only when
+ -- a function argument, and further evaluation resutls
| Implicit -- implicit coercion
| CExport String -- export, with a C name
+ | Reflection -- a reflecting function, compile-time only
| Specialise [(Name, Maybe Int)] -- specialise it, freeze these names
deriving (Show, Eq)
{-!
@@ -345,6 +362,9 @@
inlinable :: FnOpts -> Bool
inlinable = elem Inlinable
+dictionary :: FnOpts -> Bool
+dictionary = elem Dictionary
+
-- | Top-level declarations such as compiler directives, definitions,
-- datatypes and typeclasses.
data PDecl' t
@@ -379,9 +399,6 @@
| PProvider SyntaxInfo FC Name t t -- ^ Type provider. The first t is the type, the second is the term
| PTransform FC Bool t t -- ^ Source-to-source transformation rule. If
-- bool is True, lhs and rhs must be convertible
- | PReflection FC Name -- type to reflect to
- t -- type of variables
- [PClause' t] -- ^ Pattern clauses
deriving Functor
{-!
deriving instance Binary PDecl'
@@ -458,7 +475,9 @@
tldeclared (PParams _ _ ds) = []
tldeclared (PMutual _ ds) = concatMap tldeclared ds
tldeclared (PNamespace _ ds) = concatMap tldeclared ds
-
+tldeclared (PClass _ _ _ _ n _ ms) = concatMap tldeclared ms
+tldeclared (PInstance _ _ _ _ _ _ _ _) = []
+tldeclared _ = []
defined :: PDecl -> [Name]
defined (PFix _ _ _) = []
@@ -524,6 +543,7 @@
| PAlternative Bool [PTerm] -- True if only one may work
| PHidden PTerm -- ^ Irrelevant or hidden pattern
| PType
+ | PGoal FC PTerm Name PTerm
| PConstant Const
| Placeholder
| PDoBlock [PDo]
@@ -560,6 +580,7 @@
mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
+ mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
mpt x = x
@@ -679,6 +700,7 @@
!-}
data OptInfo = Optimise { collapsible :: Bool,
+ isnewtype :: Bool,
forceable :: [Int], -- argument positions
recursive :: [Int] }
deriving Show
@@ -779,7 +801,7 @@
--- Pretty printing declarations and terms
instance Show PTerm where
- show tm = showImp False tm
+ show tm = showImp Nothing False False tm
instance Pretty PTerm where
pretty = prettyImp False
@@ -794,8 +816,8 @@
show d = showDImp False d
showDeclImp _ (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
-showDeclImp t (PTy _ _ _ _ n ty) = show n ++ " : " ++ showImp t ty
-showDeclImp t (PPostulate _ _ _ _ n ty) = show n ++ " : " ++ showImp t ty
+showDeclImp t (PTy _ _ _ _ n ty) = show n ++ " : " ++ showImp Nothing t False ty
+showDeclImp t (PPostulate _ _ _ _ n ty) = show n ++ " : " ++ showImp Nothing t False ty
showDeclImp _ (PClauses _ _ n c) = showSep "\n" (map show c)
showDeclImp _ (PData _ _ _ _ d) = show d
showDeclImp _ (PParams f ns ps) = "parameters " ++ show ns ++ "\n" ++
@@ -804,24 +826,24 @@
showCImp :: Bool -> PClause -> String
showCImp impl (PClause _ n l ws r w)
- = showImp impl l ++ showWs ws ++ " = " ++ showImp impl r
+ = showImp Nothing impl False l ++ showWs ws ++ " = " ++ showImp Nothing impl False r
++ " where " ++ show w
where
showWs [] = ""
- showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
+ showWs (x : xs) = " | " ++ showImp Nothing impl False x ++ showWs xs
showCImp impl (PWith _ n l ws r w)
- = showImp impl l ++ showWs ws ++ " with " ++ showImp impl r
+ = showImp Nothing impl False l ++ showWs ws ++ " with " ++ showImp Nothing impl False r
++ " { " ++ show w ++ " } "
where
showWs [] = ""
- showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
+ showWs (x : xs) = " | " ++ showImp Nothing impl False x ++ showWs xs
showDImp :: Bool -> PData -> String
showDImp impl (PDatadecl n ty cons)
- = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"
+ = "data " ++ show n ++ " : " ++ showImp Nothing impl False ty ++ " where\n\t"
++ showSep "\n\t| "
- (map (\ (_, n, t, _) -> show n ++ " : " ++ showImp impl t) cons)
+ (map (\ (_, n, t, _) -> show n ++ " : " ++ showImp Nothing impl False t) cons)
getImps :: [PArg] -> [(Name, PTerm)]
getImps [] = []
@@ -841,7 +863,10 @@
getAll :: [PArg] -> [PTerm]
getAll = map getTm
-prettyImp :: Bool -> PTerm -> Doc
+-- | Pretty-print a high-level Idris term
+prettyImp :: Bool -- ^^ whether to show implicits
+ -> PTerm -- ^^ the term to pretty-print
+ -> Doc
prettyImp impl = prettySe 10
where
prettySe p (PQuote r) =
@@ -1027,106 +1052,150 @@
bracket outer inner doc
| inner > outer = lparen <> doc <> rparen
| otherwise = doc
-
-showImp :: Bool -> PTerm -> String
-showImp impl tm = se 10 tm where
- se p (PQuote r) = "![" ++ show r ++ "]"
- se p (PPatvar fc n) = if impl then show n ++ "[p]" else show n
- se p (PInferRef fc n) = "!" ++ show n -- ++ "[" ++ show fc ++ "]"
- se p (PRef fc n) = if impl then show n -- ++ "[" ++ show fc ++ "]"
- else showbasic n
- where showbasic n@(UN _) = show n
- showbasic (MN _ s) = s
- showbasic (NS n s) = showSep "." (reverse s) ++ "." ++ showbasic n
- se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++
- (if impl then " : " ++ se 10 ty else "") ++ " => "
- ++ se 10 sc
- se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v ++
- " in " ++ se 10 sc
- se p (PPi (Exp l s _) n ty sc)
+
+-- | Show Idris name
+showName :: Maybe IState -- ^^ the Idris state, for information about names and colours
+ -> [(Name, Bool)] -- ^^ the bound variables and whether they're implicit
+ -> Bool -- ^^ whether to show implicits
+ -> Bool -- ^^ whether to colourise
+ -> Name -- ^^ the term to show
+ -> String
+showName ist bnd impl colour n = case ist of
+ Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
+ Nothing -> showbasic n
+ where name = if impl then show n else showbasic n
+ showbasic n@(UN _) = show n
+ showbasic (MN _ s) = s
+ showbasic (NS n s) = showSep "." (reverse s) ++ "." ++ showbasic n
+ showbasic (SN s) = show s
+ fst3 (x, _, _) = x
+ colourise n t = let ctxt' = fmap tt_ctxt ist in
+ case ctxt' of
+ Nothing -> name
+ Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit t name
+ else colouriseBound t name
+ | isDConName n ctxt -> colouriseData t name
+ | isFnName n ctxt -> colouriseFun t name
+ | isTConName n ctxt -> colouriseType t name
+ -- The assumption is that if a name is not bound and does not exist in the
+ -- global context, then we're somewhere in which implicit info has been lost
+ -- (like error messages). Thus, unknown vars are colourised as implicits.
+ | otherwise -> colouriseImplicit t name
+
+-- | Show Idris term
+showImp :: Maybe IState -- ^^ the Idris state, for information about identifiers and colours
+ -> Bool -- ^^ whether to show implicits
+ -> Bool -- ^^ whether to colourise
+ -> PTerm -- ^^ the term to show
+ -> String
+showImp ist impl colour tm = se 10 [] tm where
+ perhapsColourise :: (ColourTheme -> String -> String) -> String -> String
+ perhapsColourise col str = case ist of
+ Just i -> if colour then col (idris_colourTheme i) str else str
+ Nothing -> str
+
+ se :: Int -> [(Name, Bool)] -> PTerm -> String
+ se p bnd (PQuote r) = "![" ++ show r ++ "]"
+ se p bnd (PPatvar fc n) = if impl then show n ++ "[p]" else show n
+ se p bnd (PInferRef fc n) = "!" ++ show n -- ++ "[" ++ show fc ++ "]"
+ se p bnd e
+ | Just str <- slist p bnd e = str
+ | Just num <- snat p e = perhapsColourise colouriseData (show num)
+ se p bnd (PRef fc n) = showName ist bnd impl colour n
+ se p bnd (PLam n ty sc) = bracket p 2 $ "\\ " ++ perhapsColourise colouriseBound (show n) ++
+ (if impl then " : " ++ se 10 bnd ty else "") ++ " => "
+ ++ se 10 ((n, False):bnd) sc
+ se p bnd (PLet n ty v sc) = bracket p 2 $ "let " ++ perhapsColourise colouriseBound (show n) ++
+ " = " ++ se 10 bnd v ++
+ " in " ++ se 10 ((n, False):bnd) sc
+ se p bnd (PPi (Exp l s _) n ty sc)
| n `elem` allNamesIn sc || impl
= bracket p 2 $
- (if l then "|(" else "(") ++
- show n ++ " : " ++ se 10 ty ++
+ (if l then "|(" else "(") ++
+ perhapsColourise colouriseBound (show n) ++ " : " ++ se 10 bnd ty ++
") " ++ st ++
- "-> " ++ se 10 sc
- | otherwise = bracket p 2 $ se 0 ty ++ " " ++ st ++ "-> " ++ se 10 sc
+ "-> " ++ se 10 ((n, False):bnd) sc
+ | otherwise = bracket p 2 $ se 0 bnd ty ++ " " ++ st ++ "-> " ++ se 10 bnd sc
where st = case s of
Static -> "[static] "
_ -> ""
- se p (PPi (Imp l s _) n ty sc)
- | impl = bracket p 2 $ (if l then "|{" else "{") ++
- show n ++ " : " ++ se 10 ty ++
- "} " ++ st ++ "-> " ++ se 10 sc
- | otherwise = se 10 sc
+ se p bnd (PPi (Imp l s _) n ty sc)
+ | impl = bracket p 2 $ (if l then "|{" else "{") ++
+ perhapsColourise colouriseBound (show n) ++ " : " ++ se 10 bnd ty ++
+ "} " ++ st ++ "-> " ++ se 10 ((n, True):bnd) sc
+ | otherwise = se 10 ((n, True):bnd) sc
where st = case s of
Static -> "[static] "
_ -> ""
- se p (PPi (Constraint _ _ _) n ty sc)
- = bracket p 2 $ se 10 ty ++ " => " ++ se 10 sc
- se p (PPi (TacImp _ _ s _) n ty sc)
- = bracket p 2 $ "{tacimp " ++ show n ++ " : " ++ se 10 ty ++ "} -> " ++ se 10 sc
- se p e
- | Just str <- slist p e = str
- | Just num <- snat p e = show num
- se p (PMatchApp _ f) = "match " ++ show f
- se p (PApp _ (PRef _ f) [])
- | not impl = show f
- se p (PApp _ (PRef _ op@(UN (f:_))) args)
+ se p bnd (PPi (Constraint _ _ _) n ty sc)
+ = bracket p 2 $ se 10 bnd ty ++ " => " ++ se 10 bnd sc
+ se p bnd (PPi (TacImp _ _ s _) n ty sc)
+ = bracket p 2 $
+ "{tacimp " ++ (perhapsColourise colouriseBound (show n)) ++ " : " ++ se 10 bnd ty ++ "} -> " ++
+ se 10 ((n, False):bnd) sc
+ se p bnd (PMatchApp _ f) = "match " ++ show f
+ se p bnd (PApp _ hd@(PRef _ f) [])
+ | not impl = se p bnd hd
+ se p bnd (PApp _ op@(PRef _ (UN (f:_))) args)
| length (getExps args) == 2 && not impl && not (isAlpha f)
= let [l, r] = getExps args in
- bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r
- se p (PApp _ f as)
+ bracket p 1 $ se 1 bnd l ++ " " ++ se p bnd op ++ " " ++ se 0 bnd r
+ se p bnd (PApp _ f as)
= let args = getExps as in
- bracket p 1 $ se 1 f ++ if impl then concatMap sArg as
- else concatMap seArg args
- se p (PCase _ scr opts) = "case " ++ se 10 scr ++ " of " ++ showSep " | " (map sc opts)
- where sc (l, r) = se 10 l ++ " => " ++ se 10 r
- se p (PHidden tm) = "." ++ se 0 tm
- se p (PRefl _ t)
- | not impl = "refl"
- | otherwise = "refl {" ++ se 10 t ++ "}"
- se p (PResolveTC _) = "resolvetc"
- se p (PTrue _) = "()"
- se p (PFalse _) = "_|_"
- se p (PEq _ l r) = bracket p 2 $ se 10 l ++ " = " ++ se 10 r
- se p (PRewrite _ l r _) = bracket p 2 $ "rewrite " ++ se 10 l ++ " in " ++ se 10 r
- se p (PTyped l r) = "(" ++ se 10 l ++ " : " ++ se 10 r ++ ")"
- se p (PPair _ l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"
- se p (PDPair _ l t r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"
- se p (PAlternative a as) = "(|" ++ showSep " , " (map (se 10) as) ++ "|)"
- se p PType = "Type"
- se p (PConstant c) = show c
- se p (PProof ts) = "proof { " ++ show ts ++ "}"
- se p (PTactics ts) = "tactics { " ++ show ts ++ "}"
- se p (PMetavar n) = "?" ++ show n
- se p (PReturn f) = "return"
- se p PImpossible = "impossible"
- se p Placeholder = "_"
- se p (PDoBlock _) = "do block show not implemented"
- se p (PElabError s) = show s
- se p (PCoerced t) = se p t
- se p (PUnifyLog t) = "%unifyLog " ++ se p t
--- se p x = "Not implemented"
+ bracket p 1 $ se 1 bnd f ++ if impl then concatMap (sArg bnd) as
+ else concatMap (seArg bnd) args
+ se p bnd (PCase _ scr opts) = "case " ++ se 10 bnd scr ++ " of " ++ showSep " | " (map sc opts)
+ where sc (l, r) = se 10 bnd l ++ " => " ++ se 10 bnd r
+ se p bnd (PHidden tm) = "." ++ se 0 bnd tm
+ se p bnd (PRefl _ t)
+ | not impl = perhapsColourise colouriseData "refl"
+ | otherwise = perhapsColourise colouriseData $ "refl {" ++ se 10 bnd t ++ "}"
+ se p bnd (PResolveTC _) = "resolvetc"
+ se p bnd (PTrue _) = perhapsColourise colouriseType "()"
+ se p bnd (PFalse _) = perhapsColourise colouriseType "_|_"
+ se p bnd (PEq _ l r) = bracket p 2 $ se 10 bnd l ++ perhapsColourise colouriseType " = " ++ se 10 bnd r
+ se p bnd (PRewrite _ l r _) = bracket p 2 $ "rewrite " ++ se 10 bnd l ++ " in " ++ se 10 bnd r
+ se p bnd (PTyped l r) = "(" ++ se 10 bnd l ++ " : " ++ se 10 bnd r ++ ")"
+ se p bnd (PPair _ l r) = "(" ++ se 10 bnd l ++ ", " ++ se 10 bnd r ++ ")"
+ se p bnd (PDPair _ l t r) = "(" ++ se 10 bnd l ++ " ** " ++ se 10 bnd r ++ ")"
+ se p bnd (PAlternative a as) = "(|" ++ showSep " , " (map (se 10 bnd) as) ++ "|)"
+ se p bnd PType = perhapsColourise colouriseType "Type"
+ se p bnd (PConstant c) = perhapsColourise (cfun c) (show c)
+ where cfun (AType _) = colouriseType
+ cfun StrType = colouriseType
+ cfun PtrType = colouriseType
+ cfun VoidType = colouriseType
+ cfun _ = colouriseData
+ se p bnd (PProof ts) = "proof { " ++ show ts ++ "}"
+ se p bnd (PTactics ts) = "tactics { " ++ show ts ++ "}"
+ se p bnd (PMetavar n) = "?" ++ show n
+ se p bnd (PReturn f) = "return"
+ se p bnd PImpossible = "impossible"
+ se p bnd Placeholder = "_"
+ se p bnd (PDoBlock _) = "do block show not implemented"
+ se p bnd (PElabError s) = show s
+ se p bnd (PCoerced t) = se p bnd t
+ se p bnd (PUnifyLog t) = "%unifyLog " ++ se p bnd t
+-- se p bnd x = "Not implemented"
- slist' p (PApp _ (PRef _ nil) _)
+ slist' p bnd (PApp _ (PRef _ nil) _)
| nsroot nil == UN "Nil" = Just []
- slist' p (PApp _ (PRef _ cons) args)
+ slist' p bnd (PApp _ (PRef _ cons) args)
| nsroot cons == UN "::",
(PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
all isImp imps,
- Just tl' <- slist' p tl
+ Just tl' <- slist' p bnd tl
= Just (hd:tl')
where
isImp (PImp {}) = True
isImp _ = False
- slist' _ _ = Nothing
+ slist' _ _ _ = Nothing
- slist p e | Just es <- slist' p e = Just $
+ slist p bnd e | Just es <- slist' p bnd e = Just $
case es of [] -> "[]"
- [x] -> "[" ++ se p x ++ "]"
- xs -> "[" ++ intercalate "," (map (se p) xs) ++ "]"
- slist _ _ = Nothing
+ [x] -> "[" ++ se p bnd x ++ "]"
+ xs -> "[" ++ intercalate "," (map (se p bnd ) xs) ++ "]"
+ slist _ _ _ = Nothing
-- since Prelude is always imported, S & Z are unqualified iff they're the
-- Nat ones.
@@ -1140,15 +1209,15 @@
natns = "Prelude.Nat."
- sArg (PImp _ _ n tm _) = siArg (n, tm)
- sArg (PExp _ _ tm _) = seArg tm
- sArg (PConstraint _ _ tm _) = scArg tm
- sArg (PTacImplicit _ _ n _ tm _) = stiArg (n, tm)
+ sArg bnd (PImp _ _ n tm _) = siArg bnd (n, tm)
+ sArg bnd (PExp _ _ tm _) = seArg bnd tm
+ sArg bnd (PConstraint _ _ tm _) = scArg bnd tm
+ sArg bnd (PTacImplicit _ _ n _ tm _) = stiArg bnd (n, tm)
- seArg arg = " " ++ se 0 arg
- siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"
- scArg val = " {{" ++ se 10 val ++ "}}"
- stiArg (n, val) = " {auto " ++ show n ++ " = " ++ se 10 val ++ "}"
+ seArg bnd arg = " " ++ se 0 bnd arg
+ siArg bnd (n, val) = " {" ++ show n ++ " = " ++ se 10 bnd val ++ "}"
+ scArg bnd val = " {{" ++ se 10 bnd val ++ "}}"
+ stiArg bnd (n, val) = " {auto " ++ show n ++ " = " ++ se 10 bnd val ++ "}"
bracket outer inner str | inner > outer = "(" ++ str ++ ")"
| otherwise = str
diff --git a/src/Idris/Chaser.hs b/src/Idris/Chaser.hs
new file mode 100644
--- /dev/null
+++ b/src/Idris/Chaser.hs
@@ -0,0 +1,135 @@
+module Idris.Chaser(buildTree, getModuleFiles, ModuleTree(..)) where
+
+import Idris.Parser
+import Idris.AbsSyntax
+import Idris.Imports
+import Idris.Unlit
+import Idris.Error
+import Idris.IBC
+
+import System.FilePath
+import System.Directory
+import Data.Time.Clock
+import Control.Monad.Trans
+import Control.Monad.State
+import Data.List
+
+import Debug.Trace
+
+data ModuleTree = MTree { mod_path :: IFileType,
+ mod_needsRecheck :: Bool,
+ mod_time :: UTCTime,
+ mod_deps :: [ModuleTree] }
+ deriving Show
+
+latest :: UTCTime -> [ModuleTree] -> UTCTime
+latest tm [] = tm
+latest tm (m : ms) = latest (max tm (mod_time m)) (ms ++ mod_deps m)
+
+-- Given a module tree, return the list of files to be loaded. If any
+-- module has a descendent which needs reloading, return its source, otherwise
+-- return the IBC
+
+getModuleFiles :: [ModuleTree] -> [IFileType]
+getModuleFiles ts = nub $ execState (modList ts) [] where
+ modList :: [ModuleTree] -> State [IFileType] ()
+ modList [] = return ()
+ modList (m : ms) = do modTree [] m; modList ms
+
+ modTree path (MTree p rechk tm deps)
+ = do let file = chkReload rechk p
+ -- Needs rechecking if 'rechk' is true, or if any of the
+ -- modification times in 'deps' are later than tm
+ let depMod = latest tm deps
+ let needsRechk = rechk || depMod > tm
+
+ st <- get
+ if needsRechk then put $ nub (getSrc file : updateToSrc path st)
+ else put $ nub (file : st)
+-- when (not (ibc p) || rechk) $
+ mapM_ (modTree (getSrc p : path)) deps
+
+ ibc (IBC _ _) = True
+ ibc _ = False
+
+ chkReload False p = p
+ chkReload True (IBC fn src) = chkReload True src
+ chkReload True p = p
+
+ getSrc (IBC fn src) = getSrc src
+ getSrc f = f
+
+ updateToSrc path [] = []
+ updateToSrc path (x : xs) = if getSrc x `elem` path
+ then getSrc x : updateToSrc path xs
+ else x : updateToSrc path xs
+
+getIModTime (IBC i _) = getModificationTime i
+getIModTime (IDR i) = getModificationTime i
+getIModTime (LIDR i) = getModificationTime i
+
+buildTree :: [FilePath] -> -- already guaranteed built
+ FilePath -> Idris [ModuleTree]
+buildTree built fp = idrisCatch (btree [] fp)
+ (\e -> do now <- liftIO $ getCurrentTime
+ return [MTree (IDR fp) True now []])
+ where
+ btree done f =
+ do i <- getIState
+ let file = takeWhile (/= ' ') f
+ iLOG $ "CHASING " ++ show file
+ ibcsd <- valIBCSubDir i
+ ids <- allImportDirs
+ fp <- liftIO $ findImport ids ibcsd file
+ mt <- liftIO $ getIModTime fp
+ if (file `elem` built)
+ then return [MTree fp False mt []]
+ else if file `elem` done
+ then return []
+ else mkChildren fp
+
+ where mkChildren (LIDR fn) = do ms <- children True fn (f:done)
+ mt <- liftIO $ getModificationTime fn
+ return [MTree (LIDR fn) True mt ms]
+ mkChildren (IDR fn) = do ms <- children False fn (f:done)
+ mt <- liftIO $ getModificationTime fn
+ return [MTree (IDR fn) True mt ms]
+ mkChildren (IBC fn src)
+ = do srcexist <- liftIO $ doesFileExist (getSrcFile src)
+ ms <- if srcexist then
+ do [MTree _ _ _ ms'] <- mkChildren src
+ return ms'
+ else return []
+ mt <- idrisCatch (liftIO $ getModificationTime fn)
+ (\c -> liftIO $ getIModTime src)
+ ok <- checkIBCUpToDate fn src
+ return [MTree (IBC fn src) ok mt ms]
+
+ getSrcFile (IBC _ src) = getSrcFile src
+ getSrcFile (LIDR src) = src
+ getSrcFile (IDR src) = src
+
+ -- FIXME: It's also not up to date if anything it imports has
+ -- been modified since its own ibc has.
+
+ checkIBCUpToDate fn (LIDR src) = older fn src
+ checkIBCUpToDate fn (IDR src) = older fn src
+
+ older ibc src = do exist <- liftIO $ doesFileExist src
+ if exist then do
+ ibct <- liftIO $ getModificationTime ibc
+ srct <- liftIO $ getModificationTime src
+ return (srct > ibct)
+ else return False
+
+ children :: Bool -> FilePath -> [FilePath] -> Idris [ModuleTree]
+ children lit f done = idrisCatch
+ (do exist <- liftIO $ doesFileExist f
+ if exist then do
+ file_in <- liftIO $ readFile f
+ file <- if lit then tclift $ unlit f file_in else return file_in
+ (_, modules, _, _) <- parseImports f file
+ ms <- mapM (btree done) modules
+ return (concat ms)
+ else return []) -- IBC with no source available
+ (\c -> return []) -- error, can't chase modules here
diff --git a/src/Idris/Colours.hs b/src/Idris/Colours.hs
new file mode 100644
--- /dev/null
+++ b/src/Idris/Colours.hs
@@ -0,0 +1,78 @@
+module Idris.Colours (
+ IdrisColour(..),
+ ColourTheme(..),
+ defaultTheme,
+ colouriseKwd, colouriseBound, colouriseImplicit,
+ colouriseType, colouriseFun, colouriseData,
+ colourisePrompt,
+ ColourType(..)) where
+
+import System.Console.ANSI
+
+data IdrisColour = IdrisColour { colour :: Color
+ , vivid :: Bool
+ , underline :: Bool
+ , bold :: Bool
+ }
+ deriving (Eq, Show)
+
+mkColour :: Color -> IdrisColour
+mkColour c = IdrisColour c True False False
+
+data ColourTheme = ColourTheme { keywordColour :: IdrisColour
+ , boundVarColour :: IdrisColour
+ , implicitColour :: IdrisColour
+ , functionColour :: IdrisColour
+ , typeColour :: IdrisColour
+ , dataColour :: IdrisColour
+ , promptColour :: IdrisColour
+ }
+ deriving (Eq, Show)
+
+defaultTheme :: ColourTheme
+defaultTheme = ColourTheme { keywordColour = IdrisColour Black True True True
+ , boundVarColour = mkColour Magenta
+ , implicitColour = IdrisColour Magenta True True False
+ , functionColour = mkColour Green
+ , typeColour = mkColour Blue
+ , dataColour = mkColour Red
+ , promptColour = IdrisColour Black True False True
+ }
+
+-- Set the colour of a string using POSIX escape codes
+colourise :: IdrisColour -> String -> String
+colourise (IdrisColour c v u b) str = setSGRCode sgr ++ str ++ setSGRCode [Reset]
+ where sgr = [SetColor Foreground (if v then Vivid else Dull) c] ++
+ (if u then [SetUnderlining SingleUnderline] else []) ++
+ (if b then [SetConsoleIntensity BoldIntensity] else [])
+
+colouriseKwd :: ColourTheme -> String -> String
+colouriseKwd t = colourise (keywordColour t)
+
+colouriseBound :: ColourTheme -> String -> String
+colouriseBound t = colourise (boundVarColour t)
+
+colouriseImplicit :: ColourTheme -> String -> String
+colouriseImplicit t = colourise (implicitColour t)
+
+colouriseFun :: ColourTheme -> String -> String
+colouriseFun t = colourise (functionColour t)
+
+colouriseType :: ColourTheme -> String -> String
+colouriseType t = colourise (typeColour t)
+
+colouriseData :: ColourTheme -> String -> String
+colouriseData t = colourise (dataColour t)
+
+colourisePrompt :: ColourTheme -> String -> String
+colourisePrompt t = colourise (promptColour t)
+
+
+data ColourType = KeywordColour
+ | BoundVarColour
+ | ImplicitColour
+ | FunctionColour
+ | TypeColour
+ | DataColour
+ | PromptColour
+ deriving (Eq, Show, Bounded, Enum)
diff --git a/src/Idris/Compiler.hs b/src/Idris/Compiler.hs
deleted file mode 100644
--- a/src/Idris/Compiler.hs
+++ /dev/null
@@ -1,239 +0,0 @@
-{-# LANGUAGE PatternGuards #-}
-
-module Idris.Compiler where
-
-import Idris.AbsSyntax
-import Core.TT
-
-{-
-import Idris.Transforms
-
-import Core.Evaluate
-import Core.CaseTree
-
-import Control.Monad.State
-import Data.List
-import System.Process
-import System.IO
-import System.Directory
-import System.Environment
-
-import Paths_idris
-
-import Epic.Epic hiding (Term, Type, Name, fn, compile)
-import qualified Epic.Epic as E
--}
-
-compileEpic :: FilePath -> Term -> Idris ()
-compileEpic f t = fail "Epic backend disabled"
-
-{-
-compile f tm
- = do checkMVs
- let tmnames = namesUsed (STerm tm)
- used <- mapM (allNames []) tmnames
- ds <- mkDecls tm (concat used)
- objs <- getObjectFiles
- libs <- getLibs
- hdrs <- getHdrs
- ddir <- liftIO $ getDataDir
- -- if any includes exist in the data directory, use that
- hdrs' <- liftIO $ mapM (inDir ddir) hdrs
- let incs = map Include hdrs'
- so <- getSO
--- let ilib = ddir ++ "/libidris.a"
- case so of
- Nothing ->
- do m <- epicMain tm
- let mainval = EpicFn (name "main") m
- liftIO $ compileObjWith []
- (mkProgram (incs ++ mainval : ds)) (f ++ ".o")
- liftIO $ link ((f ++ ".o") : objs ++ (map ("-l"++) libs)) f
- where checkMVs = do i <- get
- case idris_metavars i \\ primDefs of
- [] -> return ()
- ms -> fail $ "There are undefined metavariables: " ++ show ms
- inDir d h = do let f = d ++ "/" ++ h
- ex <- doesFileExist f
- if ex then return f else return h
-
-
-allNames :: [Name] -> Name -> Idris [Name]
-allNames ns n | n `elem` ns = return []
-allNames ns n = do i <- get
- case lookupCtxt Nothing n (idris_callgraph i) of
- [ns'] -> do more <- mapM (allNames (n:ns)) ns'
- return (nub (n : concat more))
- _ -> return [n]
-
-mkDecls :: Term -> [Name] -> Idris [EpicDecl]
-mkDecls t used
- = do i <- getIState
- let ds = filter (\ (n, d) -> n `elem` used) $ ctxtAlist (tt_ctxt i)
- decls <- mapM build ds
- return $ basic_defs ++ decls
-
--- EpicFn (name "main") epicMain : decls
-
-ename x = name ("idris_" ++ show x)
-aname x = name ("a_" ++ show x)
-
-epicMain tm = do e <- epic tm
- return $ effect_ e
-
--- epicMain = effect_ $ -- ref (ename (UN "run__IO")) @@
--- ref (ename (NS (UN "main") ["main"]))
-
-class ToEpic a where
- epic :: a -> Idris E.Term
-
-build :: (Name, Def) -> Idris EpicDecl
-build (n, d) = do i <- getIState
- case lookup n (idris_prims i) of
- Just opDef -> return $ EpicFn (ename n) opDef
- _ -> do def <- epic d
- logLvl 3 $ "Compiled " ++ show n ++ " =\n\t" ++ show def
- return $ EpicFn (ename n) def
-
-impossible = int 42424242
-
-instance ToEpic Def where
- epic (Function tm _) = epic tm
- epic (CaseOp _ _ pats _ _ args sc) = epic (args, sc) -- optimised version
- epic _ = return impossible
-
-instance ToEpic (TT Name) where
- epic tm = epic' [] tm where
- epic' env tm@(App f a)
- | (P _ (UN "mkForeign") _, args) <- unApply tm
- = doForeign False args
- | (P _ (UN "mkLazyForeign") _, args) <- unApply tm
- = doForeign True args
- | (P _ (UN "unsafePerformIO") _, [_, arg]) <- unApply tm
- = epic' env arg
- | (P _ (UN "lazy") _, [_,arg]) <- unApply tm
- = do arg' <- epic' env arg
- return $ lazy_ arg'
- | (P _ (UN "prim__IO") _, [v]) <- unApply tm
- = do v' <- epic' env v
- return (effect_ v')
- | (P _ (UN "io_bind") _, [_,_,v,k]) <- unApply tm
- = do v' <- epic' env v
- k' <- epic' env k
- return (effect_ (k' @@ (effect_ v')))
- | (P _ (UN "malloc") _, [_,size,t]) <- unApply tm
- = do size' <- epic' env size
- t' <- epic' env t
- return $ malloc_ size' t'
- | (P _ (UN "trace_malloc") _, [_,t]) <- unApply tm
- = do t' <- epic' env t
- return $ mallocTrace_ t'
- | (P (DCon t a) n _, args) <- unApply tm
- = epicCon env t a n args
- epic' env (P (DCon t a) n _) = return $ con_ t
- epic' env (P (TCon t a) n _) = return $ con_ t
- epic' env (P _ n _) = return $ ref (ename n)
- epic' env (V i) = return $ ref (env!!i)
- epic' env (Bind n (Lam _) sc)
- = do sc' <- epic' (aname n : env) sc
- return $ term ([aname n], sc')
- epic' env (Bind n (Let _ v) sc)
- = do sc' <- epic' (aname n : env) sc
- v' <- epic' env v
- return $ let_ v' (aname n, sc')
- epic' env (Bind _ _ _) = return impossible
- epic' env (App f a) = do f' <- epic' env f
- a' <- epic' env a
- return (f' @@ a')
- epic' env (Constant c) = epic c
- epic' env Erased = return impossible
- epic' env (TType _) = return impossible
-
- epicCon env t arity n args
- | length args == arity = buildApp env (con_ t) args
- | otherwise = let extra = satArgs (arity - length args) in
- do sc' <- epicCon env t arity n
- (args ++ map (\n -> P Bound n undefined) extra)
- return $ term (map ename extra, sc')
-
- satArgs n = map (\i -> MN i "sat") [1..n]
-
- buildApp env e [] = return e
- buildApp env e (x:xs) = do x' <- epic' env x
- buildApp env (e @@ x') xs
-
-
-doForeign :: Bool -> [TT Name] -> Idris E.Term
-doForeign lazy (_ : fgn : args)
- | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn
- = let tys = getFTypes fgnArgTys
- rty = mkEty' ret in
- do args' <- mapM epic args
- -- wrap it in a prim__IO
- -- return $ con_ 0 @@ impossible @@
- if lazy
- then return $ lazy_ $ foreignL_ rty fgnName (zip args' tys)
- else return $ lazy_ $ foreign_ rty fgnName (zip args' tys)
- | otherwise = fail "Badly formed foreign function call"
-
-getFTypes :: TT Name -> [E.Type]
-getFTypes tm = case unApply tm of
- (nil, []) -> []
- (cons, [ty, xs]) ->
- let rest = getFTypes xs in
- mkEty' ty : rest
-
-mkEty' (P _ (UN ty) _) = mkEty ty
-mkEty' _ = tyAny
-
-mkEty "FInt" = tyInt
-mkEty "FFloat" = tyFloat
-mkEty "FChar" = tyChar
-mkEty "FString" = tyString
-mkEty "FPtr" = tyPtr
-mkEty "FUnit" = tyUnit
-
-instance ToEpic Const where
- epic (I i) = return (int i)
- epic (BI i) = return (bigint i)
- epic (Fl f) = return (float f)
- epic (Str s) = return (str s)
- epic (Ch c) = return (char c)
- epic IType = return $ con_ 1
- epic FlType = return $ con_ 2
- epic ChType = return $ con_ 3
- epic StrType = return $ con_ 4
- epic PtrType = return $ con_ 5
- epic BIType = return $ con_ 6
-
-instance ToEpic ([Name], SC) where
- epic (args, tree) = do logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree
- tree' <- epic tree
- return $ term (map ename args, tree')
-
-instance ToEpic SC where
- epic (Case n [ConCase _ i ns sc])
- = epicLet n ns 0 sc
- where
- epicLet x [] _ sc = epic sc
- epicLet x (n:ns) i sc
- = do sc' <- epicLet x ns (i+1) sc
- return $ let_ (ref (ename x) !. i) (ename n, sc')
-
- epic (STerm t) = epic t
- epic (UnmatchedCase str) = return $ error_ str
- epic (Case n alts) = do alts' <- mapM mkEpicAlt alts
- return $ case_ (ref (ename n)) alts'
- where
- mkEpicAlt (ConCase n t args rhs) = do rhs' <- epic rhs
- return $ con t (map ename args, rhs')
- mkEpicAlt (ConstCase (I i) rhs) = do rhs' <- epic rhs
- return $ constcase i rhs'
- mkEpicAlt (ConstCase IType rhs) = do rhs' <- epic rhs
- return $ defaultcase rhs'
- mkEpicAlt (ConstCase c rhs)
- = fail $ "Can only pattern match on integer constants (" ++ show c ++ ")"
- mkEpicAlt (DefaultCase rhs) = do rhs' <- epic rhs
- return $ defaultcase rhs'
-
--}
diff --git a/src/Idris/Completion.hs b/src/Idris/Completion.hs
--- a/src/Idris/Completion.hs
+++ b/src/Idris/Completion.hs
@@ -7,13 +7,16 @@
import Idris.AbsSyntaxTree
import Idris.Help
+import Idris.Colours
import Control.Monad.State.Strict
import Data.List
import Data.Maybe
+import Data.Char(toLower)
import System.Console.Haskeline
+import System.Console.ANSI (Color)
fst3 :: (a, b, c) -> a
@@ -109,6 +112,32 @@
| otherwise = lookupInHelp' cmd xs
lookupInHelp' cmd [] = Nothing
+completeColour :: CompletionFunc Idris
+completeColour (prev, next) = case words (reverse prev) of
+ [c] | isCmd c -> do cmpls <- completeColourOpt next
+ return (reverse $ c ++ " ", cmpls)
+ [c, o] | o `elem` opts -> let correct = (c ++ " " ++ o) in
+ return (reverse correct, [simpleCompletion ""])
+ | o `elem` colourTypes -> completeColourFormat (prev, next)
+ | otherwise -> let cmpls = completeWith (opts ++ colourTypes) o in
+ let sofar = (c ++ " ") in
+ return (reverse sofar, cmpls)
+ cmd@(c:o:_) | isCmd c && o `elem` colourTypes ->
+ completeColourFormat (prev, next)
+ _ -> noCompletion (prev, next)
+ where completeColourOpt :: String -> Idris [Completion]
+ completeColourOpt = return . completeWith (opts ++ colourTypes)
+ opts = ["on", "off"]
+ colourTypes = map (map toLower . reverse . drop 6 . reverse . show) $
+ enumFromTo (minBound::ColourType) maxBound
+ isCmd ":colour" = True
+ isCmd ":color" = True
+ isCmd _ = False
+ colours = map (map toLower . show) $ enumFromTo (minBound::Color) maxBound
+ formats = ["vivid", "dull", "underline", "nounderline", "bold", "nobold"]
+ completeColourFormat = let getCmpl = completeWith (colours ++ formats) in
+ completeWord Nothing " \t" (return . getCmpl)
+
-- | Get the completion function for a particular command
completeCmd :: String -> CompletionFunc Idris
completeCmd cmd (prev, next) = fromMaybe completeCmdName $ fmap completeArg $ lookupInHelp cmd
@@ -118,6 +147,7 @@
completeArg ModuleArg = noCompletion (prev, next) -- FIXME do later
completeArg ExprArg = completeExpr [] (prev, next)
completeArg MetaVarArg = completeMetaVar (prev, next) -- FIXME only complete one name
+ completeArg ColourArg = completeColour (prev, next)
completeArg NoArg = noCompletion (prev, next)
completeCmdName = return $ ("", completeWith commands cmd)
diff --git a/src/Idris/Coverage.hs b/src/Idris/Coverage.hs
--- a/src/Idris/Coverage.hs
+++ b/src/Idris/Coverage.hs
@@ -50,7 +50,7 @@
logLvl 5 $ show (map length argss) ++ "\n" ++ show (map length all_args)
logLvl 10 $ show argss ++ "\n" ++ show all_args
logLvl 10 $ "Original: \n" ++
- showSep "\n" (map (\t -> showImp True (delab' i t True)) xs)
+ showSep "\n" (map (\t -> showImp Nothing True False (delab' i t True)) xs)
-- add an infinite supply of explicit arguments to update the possible
-- cases for (the return type may be variadic, or function type, sp
-- there may be more case splitting that the idris_implicits record
@@ -62,7 +62,7 @@
logLvl 2 $ show (length tryclauses) ++ " initially to check"
let new = filter (noMatch i) (mnub i tryclauses)
logLvl 1 $ show (length new) ++ " clauses to check for impossibility"
- logLvl 5 $ "New clauses: \n" ++ showSep "\n" (map (showImp True) new)
+ logLvl 5 $ "New clauses: \n" ++ showSep "\n" (map (showImp Nothing True False) new)
-- ++ " from:\n" ++ showSep "\n" (map (showImp True) tryclauses)
return new
-- return (map (\t -> PClause n t [] PImpossible []) new)
@@ -142,6 +142,14 @@
otherPats :: PTerm -> [PTerm]
otherPats o@(PRef fc n) = ops fc n [] o
otherPats o@(PApp _ (PRef fc n) xs) = ops fc n xs o
+ otherPats o@(PPair fc l r)
+ = ops fc pairCon
+ ([pimp (UN "A") Placeholder, pimp (UN "B") Placeholder] ++
+ [pexp l, pexp r]) o
+ otherPats o@(PDPair fc t _ v)
+ = ops fc (UN "Ex_intro")
+ ([pimp (UN "a") Placeholder, pimp (UN "P") Placeholder] ++
+ [pexp t,pexp v]) o
otherPats arg = return Placeholder
ops fc n xs_in o
@@ -149,15 +157,23 @@
= do let force = getForceable i n -- no need to generate forceable positions
let xs = dropForce force xs_in 0
xs' <- mapM otherPats (map getTm xs)
- let p = PApp fc (PRef fc n) (zipWith upd xs' xs)
+ let p = resugar (PApp fc (PRef fc n) (zipWith upd xs' xs))
let tyn = getTy n (tt_ctxt i)
case lookupCtxt tyn (idris_datatypes i) of
(TI ns _ _ : _) -> p : map (mkPat fc) (ns \\ [n])
_ -> [p]
ops fc n arg o = return Placeholder
+ -- put it back to its original form
+ resugar (PApp _ (PRef fc (UN "Ex_intro")) [_,_,t,v])
+ = PDPair fc (getTm t) Placeholder (getTm v)
+ resugar (PApp _ (PRef fc n) [_,_,l,r])
+ | n == pairCon
+ = PPair fc (getTm l) (getTm r)
+ resugar t = t
+
getForceable i n = case lookupCtxt n (idris_optimisation i) of
- [Optimise _ fs _] -> fs
+ [o] -> forceable o
_ -> []
dropForce force (x : xs) i | i `elem` force
@@ -287,7 +303,7 @@
t' <- case t of
Unchecked ->
case lookupDef n ctxt of
- [CaseOp _ _ _ _ pats _ _ _ _] ->
+ [CaseOp _ _ _ pats _] ->
do t' <- if AssertTotal `elem` opts
then return $ Total []
else calcTotality path fc n pats
@@ -297,11 +313,11 @@
-- typechecking decidable
case t' of
-- FIXME: Put this back when we can handle mutually recursive things
--- p@(Partial _) ->
--- do setAccessibility n Frozen
--- addIBC (IBCAccess n Frozen)
--- logLvl 5 $ "HIDDEN: "
--- ++ show n ++ show p
+ p@(Partial _) ->
+ do setAccessibility n Frozen
+ addIBC (IBCAccess n Frozen)
+ logLvl 5 $ "HIDDEN: "
+ ++ show n ++ show p
_ -> return ()
return t'
_ -> return $ Total []
@@ -351,7 +367,8 @@
ist <- getIState
case lookupCtxt n (idris_callgraph ist) of
[cg] -> case lookupDef n (tt_ctxt ist) of
- [CaseOp _ _ _ pats _ args sc _ _] ->
+ [CaseOp _ _ pats _ cd] ->
+ let (args, sc) = cases_totcheck cd in
do logLvl 2 $ "Building SCG for " ++ show n ++ " from\n"
++ show pats ++ "\n" ++ show sc
let newscg = buildSCG' ist (rights pats) args
diff --git a/src/Idris/DSL.hs b/src/Idris/DSL.hs
--- a/src/Idris/DSL.hs
+++ b/src/Idris/DSL.hs
@@ -40,6 +40,8 @@
expandDo dsl (PReturn fc) = dsl_return dsl
expandDo dsl (PRewrite fc r t ty)
= PRewrite fc r (expandDo dsl t) ty
+expandDo dsl (PGoal fc r n sc)
+ = PGoal fc (expandDo dsl r) n (expandDo dsl sc)
expandDo dsl (PDoBlock ds) = expandDo dsl $ block (dsl_bind dsl) ds
where
block b [DoExp fc tm] = tm
diff --git a/src/Idris/DataOpts.hs b/src/Idris/DataOpts.hs
--- a/src/Idris/DataOpts.hs
+++ b/src/Idris/DataOpts.hs
@@ -18,7 +18,7 @@
forceArgs n t = do i <- getIState
let fargs = force i 0 t
copt <- case lookupCtxt n (idris_optimisation i) of
- [] -> return $ Optimise False [] []
+ [] -> return $ Optimise False False [] []
(op:_) -> return op
let opts = addDef n (copt { forceable = fargs }) (idris_optimisation i)
putIState (i { idris_optimisation = opts })
@@ -62,8 +62,22 @@
let cons' = map (\ (n, t) -> (n, map snd (getArgTys t))) cons
allFR <- mapM (forceRec i) cons'
if and allFR then detaggable (map getRetTy (map snd cons))
- else return () -- not collapsible as not detaggable
+ else checkNewType cons'
where
+ -- one constructor; if one remaining argument, treat as newtype
+ checkNewType [(n, ts)] = do
+ i <- getIState
+ case lookupCtxt n (idris_optimisation i) of
+ (oi:_) -> do let remaining = length ts - length (forceable oi)
+ if remaining == 1 then
+ do let oi' = oi { isnewtype = True }
+ let opts = addDef n oi' (idris_optimisation i)
+ putIState (i { idris_optimisation = opts })
+ else return ()
+ _ -> return ()
+
+ checkNewType _ = return ()
+
setCollapsible :: Name -> Idris ()
setCollapsible n
= do i <- getIState
@@ -72,7 +86,7 @@
(oi:_) -> do let oi' = oi { collapsible = True }
let opts = addDef n oi' (idris_optimisation i)
putIState (i { idris_optimisation = opts })
- [] -> do let oi = Optimise True [] []
+ [] -> do let oi = Optimise True False [] []
let opts = addDef n oi (idris_optimisation i)
putIState (i { idris_optimisation = opts })
addIBC (IBCOpt n)
@@ -200,13 +214,23 @@
-- Run-time: do everything
instance Optimisable (TT Name) where
+ applyOpts (P _ (NS (UN "plus") ["Nat","Prelude"]) _)
+ = return (P Ref (UN "prim__addBigInt") Erased)
+ applyOpts (P _ (NS (UN "mult") ["Nat","Prelude"]) _)
+ = return (P Ref (UN "prim__mulBigInt") Erased)
+ applyOpts (App (P _ (NS (UN "fromIntegerNat") ["Nat","Prelude"]) _) x)
+ = applyOpts x
+ applyOpts (P _ (NS (UN "fromIntegerNat") ["Nat","Prelude"]) _)
+ = return (App (P Ref (NS (UN "id") ["Builtins"]) Erased) Erased)
+ applyOpts (P _ (NS (UN "toIntegerNat") ["Nat","Prelude"]) _)
+ = return (App (P Ref (NS (UN "id") ["Builtins"]) Erased) Erased)
applyOpts c@(P (DCon t arity) n _)
= do i <- getIState
case lookupCtxt n (idris_optimisation i) of
(oi:_) -> return $ applyDataOptRT oi n t arity []
_ -> return c
applyOpts t@(App f a)
- | (c@(P (DCon t arity) n _), args) <- unApply t -- MAGIC HERE
+ | (c@(P (DCon t arity) n _), args) <- unApply t
= do args' <- mapM applyOpts args
i <- getIState
case lookupCtxt n (idris_optimisation i) of
@@ -252,11 +276,23 @@
bind [] tm = tm
bind (n:ns) tm = Bind n (Lam Erased) (pToV n (bind ns tm))
+ -- Nat special cases
+ -- TODO: Would be nice if this was configurable in idris source!
+ doOpts (NS (UN "Z") ["Nat", "Prelude"]) [] _ _ = Constant (BI 0)
+ doOpts (NS (UN "S") ["Nat", "Prelude"]) [k] _ _
+ = App (App (P Ref (UN "prim__addBigInt") Erased) k) (Constant (BI 1))
+
doOpts n args True f = Erased
doOpts n args _ forced
= let args' = filter keep (zip (map (\x -> x `elem` forced) [0..])
args) in
- mkApp (P (DCon tag (arity - length forced)) n Erased) (map snd args')
+ if isnewtype oi
+ then case args' of
+ [(_, val)] -> val
+ _ -> error "Can't happen (not isnewtype)"
+ else
+ mkApp (P (DCon tag (arity - length forced)) n Erased)
+ (map snd args')
keep (forced, _) = not forced
diff --git a/src/Idris/Delaborate.hs b/src/Idris/Delaborate.hs
--- a/src/Idris/Delaborate.hs
+++ b/src/Idris/Delaborate.hs
@@ -93,40 +93,52 @@
imp (PConstraint p l _ d) arg = PConstraint p l arg d
imp (PTacImplicit p l n sc _ d) arg = PTacImplicit p l n sc arg d
+
+indented text = boxIt '\n' $ unlines $ map ('\t':) $ lines text where
+ boxIt c text = (c:text) ++ if last text == c
+ then ""
+ else [c]
+
pshow :: IState -> Err -> String
pshow i (Msg s) = s
pshow i (InternalMsg s) = "INTERNAL ERROR: " ++ show s ++
"\nThis is probably a bug, or a missing error message.\n" ++
"Please consider reporting at " ++ bugaddr
-pshow i (CantUnify _ x y e sc s)
+pshow i (CantUnify _ x y e sc s)
= let imps = opt_showimp (idris_options i) in
- "Can't unify " ++ showImp imps (delab i x)
- ++ " with " ++ showImp imps (delab i y) ++
+ let colour = idris_colourRepl i in
+ "Can't unify" ++ indented (showImp (Just i) imps colour (delab i x))
+ ++ "with" ++ indented (showImp (Just i) imps colour (delab i y)) ++
-- " (" ++ show x ++ " and " ++ show y ++ ") " ++
case e of
Msg "" -> ""
- _ -> "\n\nSpecifically:\n\t" ++ pshow i e ++
- if (opt_errContext (idris_options i)) then showSc i sc else ""
-pshow i (CantConvert x y env)
+ _ -> "\nSpecifically:" ++
+ indented (pshow i e) ++
+ if (opt_errContext (idris_options i)) then showSc i sc else ""
+pshow i (CantConvert x y env)
= let imps = opt_showimp (idris_options i) in
- "Can't convert " ++ showImp imps (delab i x) ++ " with "
- ++ showImp imps (delab i y) ++
+ let colour = idris_colourRepl i in
+ "Can't convert" ++ indented (showImp (Just i) imps colour (delab i x)) ++ "with"
+ ++ indented (showImp (Just i) imps colour (delab i y)) ++
if (opt_errContext (idris_options i)) then showSc i env else ""
-pshow i (UnifyScope n out tm env)
+pshow i (UnifyScope n out tm env)
= let imps = opt_showimp (idris_options i) in
- "Can't unify " ++ show n ++ " with "
- ++ showImp imps (delab i tm) ++ " as " ++ show out ++
- " is not in scope" ++
+ let colour = idris_colourRepl i in
+ "Can't unify" ++ indented (show n) ++ "with"
+ ++ indented (showImp (Just i) imps colour (delab i tm)) ++ "as" ++
+ indented (show out) ++ "is not in scope" ++
if (opt_errContext (idris_options i)) then showSc i env else ""
pshow i (CantInferType t)
= "Can't infer type for " ++ t
pshow i (NonFunctionType f ty)
= let imps = opt_showimp (idris_options i) in
- showImp imps (delab i f) ++ " does not have a function type ("
- ++ showImp imps (delab i ty) ++ ")"
+ let colour = idris_colourRepl i in
+ showImp (Just i) imps colour (delab i f) ++ " does not have a function type ("
+ ++ showImp (Just i) imps colour (delab i ty) ++ ")"
pshow i (CantIntroduce ty)
= let imps = opt_showimp (idris_options i) in
- "Can't use lambda here: type is " ++ showImp imps (delab i ty)
+ let colour = idris_colourRepl i in
+ "Can't use lambda here: type is " ++ showImp (Just i) imps colour (delab i ty)
pshow i (InfiniteUnify x tm env)
= "Unifying " ++ showbasic x ++ " and " ++ show (delab i tm) ++
" would lead to infinite value" ++
@@ -138,7 +150,7 @@
pshow i (CantResolveAlts as) = "Can't disambiguate name: " ++ showSep ", " as
pshow i (NoTypeDecl n) = "No type declaration for " ++ show n
pshow i (NoSuchVariable n) = "No such variable " ++ show n
-pshow i (IncompleteTerm t) = "Incomplete term " ++ showImp True (delab i t)
+pshow i (IncompleteTerm t) = "Incomplete term " ++ showImp Nothing True False (delab i t)
pshow i UniverseError = "Universe inconsistency"
pshow i ProgramLineComment = "Program line next to comment"
pshow i (Inaccessible n) = show n ++ " is not an accessible pattern variable"
@@ -148,12 +160,25 @@
pshow i (ProofSearchFail e) = pshow i e
pshow i (NoRewriting tm) = "rewrite did not change type " ++ show (delab i tm)
pshow i (At f e) = show f ++ ":" ++ pshow i e
+pshow i (Elaborating s n e) = "When elaborating " ++ s ++
+ showqual i n ++ ":\n" ++ pshow i e
pshow i (ProviderError msg) = "Type provider error: " ++ msg
showSc i [] = ""
showSc i xs = "\n\nIn context:\n" ++ showSep "\n" (map showVar (reverse xs))
where showVar (x, y) = "\t" ++ showbasic x ++ " : " ++ show (delab i y)
+showqual :: IState -> Name -> String
+showqual i n = showName (Just i) [] False False (dens n)
+ where
+ dens ns@(NS n _) = case lookupCtxt n (idris_implicits i) of
+ [_] -> n -- just one thing
+ _ -> ns
+ dens n = n
+
showbasic n@(UN _) = show n
showbasic (MN _ s) = s
showbasic (NS n s) = showSep "." (reverse s) ++ "." ++ showbasic n
+showbasic (SN s) = show s
+
+
diff --git a/src/Idris/ElabDecls.hs b/src/Idris/ElabDecls.hs
--- a/src/Idris/ElabDecls.hs
+++ b/src/Idris/ElabDecls.hs
@@ -13,6 +13,7 @@
import Idris.DataOpts
import Idris.Providers
import Idris.Primitives
+import Idris.Inliner
import Idris.PartialEval
import IRTS.Lang
import Paths_idris
@@ -51,13 +52,14 @@
do checkUndefined fc n
ctxt <- getContext
i <- getIState
- logLvl 3 $ show n ++ " pre-type " ++ showImp True ty'
+ logLvl 3 $ show n ++ " pre-type " ++ showImp Nothing True False ty'
ty' <- addUsingConstraints syn fc ty'
ty' <- implicit syn n ty'
let ty = addImpl i ty'
- logLvl 2 $ show n ++ " type " ++ showImp True ty
- ((tyT, defer, is), log) <- tclift $ elaborate ctxt n (TType (UVal 0)) []
- (erun fc (build i info False n ty))
+ logLvl 2 $ show n ++ " type " ++ showImp Nothing True False ty
+ ((tyT, defer, is), log) <-
+ tclift $ elaborate ctxt n (TType (UVal 0)) []
+ (errAt "type of " n (erun fc (build i info False n ty)))
ds <- checkDef fc defer
addDeferred ds
mapM_ (elabCaseBlock info) is
@@ -138,8 +140,9 @@
i <- getIState
t_in <- implicit syn n t_in
let t = addImpl i t_in
- ((t', defer, is), log) <- tclift $ elaborate ctxt n (TType (UVal 0)) []
- (erun fc (build i info False n t))
+ ((t', defer, is), log) <-
+ tclift $ elaborate ctxt n (TType (UVal 0)) []
+ (errAt "data declaration " n (erun fc (build i info False n t)))
def' <- checkDef fc defer
addDeferredTyCon def'
mapM_ (elabCaseBlock info) is
@@ -222,6 +225,8 @@
mapM_ elabPrim primitives
-- Special case prim__believe_me because it doesn't work on just constants
elabBelieveMe
+ -- Finally, syntactic equality
+ elabSynEq
where elabPrim :: Prim -> Idris ()
elabPrim (Prim n ty i def sc tot)
= do updateContext (addOperator n ty i (valuePrim def))
@@ -241,15 +246,43 @@
believeTy = Bind (UN "a") (Pi (TType (UVar (-2))))
(Bind (UN "b") (Pi (TType (UVar (-2))))
(Bind (UN "x") (Pi (V 1)) (V 1)))
- elabBelieveMe = do let prim__believe_me = (UN "prim__believe_me")
- updateContext (addOperator prim__believe_me believeTy 3 p_believeMe)
- setTotality prim__believe_me (Partial NotCovering)
- i <- getIState
- putIState i {
- idris_scprims = (prim__believe_me, (3, LNoOp)) : idris_scprims i
- }
+ elabBelieveMe
+ = do let prim__believe_me = (UN "prim__believe_me")
+ updateContext (addOperator prim__believe_me believeTy 3 p_believeMe)
+ setTotality prim__believe_me (Partial NotCovering)
+ i <- getIState
+ putIState i {
+ idris_scprims = (prim__believe_me, (3, LNoOp)) : idris_scprims i
+ }
+ p_synEq [t,_,x,y]
+ | x == y = Just (VApp (VApp vnJust VErased)
+ (VApp (VApp vnRefl t) x))
+ | otherwise = Just (VApp vnNothing VErased)
+ p_synEq args = Nothing
+ nMaybe = P (TCon 0 2) (NS (UN "Maybe") ["Maybe", "Prelude"]) Erased
+ vnJust = VP (DCon 1 2) (NS (UN "Just") ["Maybe", "Prelude"]) VErased
+ vnNothing = VP (DCon 0 1) (NS (UN "Nothing") ["Maybe", "Prelude"]) VErased
+ vnRefl = VP (DCon 0 2) eqCon VErased
+
+ synEqTy = Bind (UN "a") (Pi (TType (UVar (-3))))
+ (Bind (UN "b") (Pi (TType (UVar (-3))))
+ (Bind (UN "x") (Pi (V 1))
+ (Bind (UN "y") (Pi (V 1))
+ (mkApp nMaybe [mkApp (P (TCon 0 4) eqTy Erased)
+ [V 3, V 2, V 1, V 0]]))))
+ elabSynEq
+ = do let synEq = UN "prim__syntactic_eq"
+
+ updateContext (addOperator synEq synEqTy 4 p_synEq)
+ setTotality synEq (Total [])
+ i <- getIState
+ putIState i {
+ idris_scprims = (synEq, (4, LNoOp)) : idris_scprims i
+ }
+
+
-- | Elaborate a type provider
elabProvider :: ElabInfo -> SyntaxInfo -> FC -> Name -> PTerm -> PTerm -> Idris ()
elabProvider info syn fc n ty tm
@@ -276,7 +309,10 @@
elabType info syn "" fc [] n ty
-- Execute the type provider and normalise the result
- rhs <- execute e
+ -- use 'run__provider' to convert to a primitive IO action
+
+ rhs <- execute (mkApp (P Ref (UN "run__provider") Erased)
+ [Erased, e])
let rhs' = normalise ctxt [] rhs
logLvl 1 $ "Normalised " ++ show n ++ "'s RHS to " ++ show rhs
@@ -449,9 +485,10 @@
i <- getIState
t_in <- implicit syn n (if codata then mkLazy t_in else t_in)
let t = addImpl i t_in
- logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ showImp True t
- ((t', defer, is), log) <- tclift $ elaborate ctxt n (TType (UVal 0)) []
- (erun fc (build i info False n t))
+ logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ showImp Nothing True False t
+ ((t', defer, is), log) <-
+ tclift $ elaborate ctxt n (TType (UVal 0)) []
+ (errAt "constructor " n (erun fc (build i info False n t)))
logLvl 2 $ "Rechecking " ++ show t'
def' <- checkDef fc defer
addDeferred def'
@@ -483,6 +520,7 @@
do ctxt <- getContext
-- Check n actually exists, with no definition yet
let tys = lookupTy n ctxt
+ let reflect = Reflection `elem` opts
checkUndefined n ctxt
unless (length tys > 1) $ do
fty <- case tys of
@@ -490,8 +528,10 @@
-- question: CAFs in where blocks?
tclift $ tfail $ At fc (NoTypeDecl n)
[ty] -> return ty
- pats_in <- mapM (elabClause info (TCGen `elem` opts))
+ pats_in <- mapM (elabClause info (Dictionary `elem` opts))
(zip [0..] cs)
+ logLvl 3 $ "Elaborated patterns:\n" ++ show pats_in
+
-- if the return type of 'ty' is collapsible, the optimised version should
-- just do nothing
ist <- getIState
@@ -511,7 +551,7 @@
[oi] -> do let opts = addDef n (oi { collapsible = True })
(idris_optimisation ist)
putIState (ist { idris_optimisation = opts })
- _ -> do let opts = addDef n (Optimise True [] [])
+ _ -> do let opts = addDef n (Optimise True False [] [])
(idris_optimisation ist)
putIState (ist { idris_optimisation = opts })
addIBC (IBCOpt n)
@@ -522,24 +562,49 @@
-- show l ++ " = " ++
-- show r) pats))
let tcase = opt_typecase (idris_options ist)
- let pdef = map debind $ map (simpl (tt_ctxt ist)) pats
+
+ -- Summary of what's about to happen: Definitions go:
+
+ -- pats_in -> pats -> optpats
+ -- pdef comes from pats,
+ -- optpdef comes from optpats
+ -- Then pdef' is optpdef with forcing/collapsing applied everywhere
+
+ -- addCaseDef builds case trees from and
+
+ -- pdef is the compile-time pattern definition.
+ -- This will get further optimised for run-time, and, separately,
+ -- further inlined to help with totality checking.
+ let pdef = map debind $ map (simple_lhs (tt_ctxt ist)) pats
+ logLvl 5 $ "Initial typechecked patterns:\n" ++ show pdef
+
+ -- TODO: Inlining on initial definition happens here.
+
+ -- NOTE: Need to store original definition so that proofs which
+ -- rely on its structure aren't affected by any changes to the
+ -- inliner. Just use the inlined version to generate pdef' and to
+ -- help with later inlinings.
+
+ ist <- getIState
+ let pdef_inl = inlineDef ist pdef
+
numArgs <- tclift $ sameLength pdef
+ -- patterns after collapsing optimisation applied
+ -- (i.e. check if the function should do nothing at run time)
optpats <- if doNothing
then return $ [Right (mkApp (P Bound n Erased)
(take numArgs (repeat Erased)), Erased)]
else stripCollapsed pats
- logLvl 5 $ "Patterns:\n" ++ show pats_in
case specNames opts of
Just _ -> logLvl 5 $ "Partially evaluated:\n" ++ show pats
_ -> return ()
- logLvl 3 $ "SIMPLIFIED: \n" ++ show pdef
- let optpdef = map debind $ map (simpl (tt_ctxt ist)) optpats
+ let optpdef = map debind $ map (simple_lhs (tt_ctxt ist)) optpats
tree@(CaseDef scargs sc _) <- tclift $
- simpleCase tcase False CompileTime fc pdef
+ simpleCase tcase False reflect CompileTime fc pdef
cov <- coverage
pmissing <-
if cov
@@ -548,9 +613,9 @@
missing' <- filterM (checkPossible info fc True n) missing
let clhs = map getLHS pdef
logLvl 2 $ "Must be unreachable:\n" ++
- showSep "\n" (map (showImp True) missing') ++
+ showSep "\n" (map (showImp Nothing True False) missing') ++
"\nAgainst: " ++
- showSep "\n" (map (\t -> showImp True (delab ist t)) (map getLHS pdef))
+ showSep "\n" (map (\t -> showImp Nothing True False (delab ist t)) (map getLHS pdef))
-- filter out anything in missing' which is
-- matched by any of clhs. This might happen since
-- unification may force a variable to take a
@@ -559,11 +624,11 @@
return (filter (noMatch ist clhs) missing')
else return []
let pcover = null pmissing
- logLvl 2 $ "Optimising patterns"
- logLvl 5 $ show optpdef
+
+ -- pdef' is the version that gets compiled for run-time
pdef' <- applyOpts optpdef
- logLvl 2 $ "Optimised patterns"
- logLvl 5 $ show pdef'
+ logLvl 5 $ "After data structure transformations:\n" ++ show pdef'
+
ist <- getIState
-- let wf = wellFounded ist n sc
let tot = if pcover || AssertTotal `elem` opts
@@ -584,26 +649,31 @@
show (delab ist x)) xs
let knowncovering = (pcover && cov) || AssertTotal `elem` opts
- tree' <- tclift $ simpleCase tcase knowncovering RunTime fc pdef'
+ tree' <- tclift $ simpleCase tcase knowncovering reflect
+ RunTime fc pdef'
logLvl 3 (show tree)
logLvl 3 $ "Optimised: " ++ show tree'
ctxt <- getContext
ist <- getIState
putIState (ist { idris_patdefs = addDef n (pdef', pmissing)
(idris_patdefs ist) })
+ let caseInfo = CaseInfo (inlinable opts) (dictionary opts)
case lookupTy n ctxt of
- [ty] -> do updateContext (addCasedef n (inlinable opts)
+ [ty] -> do updateContext (addCasedef n caseInfo
tcase knowncovering
+ reflect
(AssertTotal `elem` opts)
pats
- pdef pdef' ty)
+ pdef pdef pdef_inl pdef' ty)
addIBC (IBCDef n)
setTotality n tot
- totcheck (fc, n)
+ when (not reflect) $ totcheck (fc, n)
when (tot /= Unchecked) $ addIBC (IBCTotal n tot)
i <- getIState
case lookupDef n (tt_ctxt i) of
- (CaseOp _ _ _ _ _ scargs sc scargs' sc' : _) ->
+ (CaseOp _ _ _ _ cd : _) ->
+ let (scargs, sc) = cases_compiletime cd
+ (scargs', sc') = cases_runtime cd in
do let calls = findCalls sc' scargs'
let used = findUsedArgs sc' scargs'
-- let scg = buildSCG i sc scargs
@@ -614,6 +684,7 @@
addToCalledG n (nub (map fst calls)) -- plus names in type!
addIBC (IBCCG n)
_ -> return ()
+ return ()
-- addIBC (IBCTotal n tot)
[] -> return ()
return ()
@@ -638,8 +709,8 @@
getLHS (_, l, _) = l
- simpl ctxt (Right (x, y)) = Right (normalise ctxt [] x, y)
- simpl ctxt t = t
+ simple_lhs ctxt (Right (x, y)) = Right (normalise ctxt [] x, y)
+ simple_lhs ctxt t = t
specNames [] = Nothing
specNames (Specialise ns : _) = Just ns
@@ -664,7 +735,7 @@
= do ctxt <- getContext
i <- getIState
let tm = addImpl i tm_in
- logLvl 10 (showImp True tm)
+ logLvl 10 (showImp Nothing True False tm)
-- try:
-- * ordinary elaboration
-- * elaboration as a Type
@@ -675,6 +746,10 @@
-- (build i info aspat (MN 0 "val") tm))
tclift (elaborate ctxt (MN 0 "val") infP []
(build i info aspat (MN 0 "val") (infTerm tm)))
+ def' <- checkDef (FC "(input)" 0) defer
+ addDeferred def'
+ mapM_ (elabCaseBlock info) is
+
logLvl 3 ("Value: " ++ show tm')
recheckC (FC "(input)" 0) [] tm'
let vtm = getInferTerm tm'
@@ -696,12 +771,12 @@
do let lhs_tm = orderPats (getInferTerm lhs')
case recheck ctxt [] (forget lhs_tm) lhs_tm of
OK _ -> return True
- _ -> return False
+ err -> return False
-- b <- inferredDiff fc (delab' i lhs_tm True) lhs
-- return (not b) -- then return (Just lhs_tm) else return Nothing
-- trace (show (delab' i lhs_tm True) ++ "\n" ++ show lhs) $ return (not b)
- Error _ -> return False
+ err@(Error _) -> return False
elabClause :: ElabInfo -> Bool -> (Int, PClause) ->
Idris (Either Term (Term, Term))
@@ -725,11 +800,12 @@
_ -> []
let params = getParamsInType i [] fn_is fn_ty
let lhs = addImplPat i (propagateParams params (stripLinear i lhs_in))
- logLvl 5 ("LHS: " ++ show fc ++ " " ++ showImp True lhs)
+ logLvl 5 ("LHS: " ++ show fc ++ " " ++ showImp Nothing True False lhs)
logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show (fn_ty, fn_is))
((lhs', dlhs, []), _) <-
tclift $ elaborate ctxt (MN 0 "patLHS") infP []
- (erun fc (buildTC i info True tcgen fname (infTerm lhs)))
+ (errAt "left hand side of " fname
+ (erun fc (buildTC i info True tcgen fname (infTerm lhs))))
let lhs_tm = orderPats (getInferTerm lhs')
let lhs_ty = getInferType lhs'
logLvl 3 ("Elaborated: " ++ show lhs_tm)
@@ -755,17 +831,19 @@
mapM_ (elabDecl' EAll info) wbefore
-- Now build the RHS, using the type of the LHS as the goal.
i <- getIState -- new implicits from where block
- logLvl 5 (showImp True (expandParams decorate newargs defs (defs \\ decls) rhs_in))
+ logLvl 5 (showImp Nothing True False (expandParams decorate newargs defs (defs \\ decls) rhs_in))
let rhs = addImplBoundInf i (map fst newargs) (defs \\ decls)
(expandParams decorate newargs defs (defs \\ decls) rhs_in)
- logLvl 2 $ "RHS: " ++ showImp True rhs
+ logLvl 2 $ "RHS: " ++ showImp Nothing True False rhs
ctxt <- getContext -- new context with where block added
logLvl 5 "STARTING CHECK"
((rhs', defer, is), _) <-
tclift $ elaborate ctxt (MN 0 "patRHS") clhsty []
(do pbinds lhs_tm
- (_, _, is) <- erun fc (build i info False fname rhs)
- erun fc $ psolve lhs_tm
+ (_, _, is) <- errAt "right hand side of " fname
+ (erun fc (build i info False fname rhs))
+ errAt "right hand side of " fname
+ (erun fc $ psolve lhs_tm)
tt <- get_term
let (tm, ds) = runState (collectDeferred tt) []
return (tm, ds, is))
@@ -792,8 +870,13 @@
checkInferred fc (delab' i crhs True) rhs
return $ Right (clhs, crhs)
where
- decorate (NS x ns) = NS (UN ('#':show x)) (ns ++ [show cnum, show fname])
- decorate x = NS (UN ('#':show x)) [show cnum, show fname]
+ decorate (NS x ns)
+ = NS (SN (WhereN cnum fname x)) ns -- ++ [show cnum])
+-- = NS (UN ('#':show x)) (ns ++ [show cnum, show fname])
+ decorate x
+ = SN (WhereN cnum fname x)
+-- = NS (SN (WhereN cnum fname x)) [show cnum]
+-- = NS (UN ('#':show x)) [show cnum, show fname]
sepBlocks bs = sepBlocks' [] bs where
sepBlocks' ns (d@(PTy _ _ _ _ n t) : bs)
@@ -860,10 +943,11 @@
-- pattern bindings
i <- getIState
let lhs = addImplPat i lhs_in
- logLvl 5 ("LHS: " ++ showImp True lhs)
+ logLvl 5 ("LHS: " ++ showImp Nothing True False lhs)
((lhs', dlhs, []), _) <-
tclift $ elaborate ctxt (MN 0 "patLHS") infP []
- (erun fc (buildTC i info True tcgen fname (infTerm lhs)))
+ (errAt "left hand side of with in " fname
+ (erun fc (buildTC i info True tcgen fname (infTerm lhs))) )
let lhs_tm = orderPats (getInferTerm lhs')
let lhs_ty = getInferType lhs'
let ret_ty = getRetTy lhs_ty
@@ -872,14 +956,15 @@
logLvl 5 ("Checked " ++ show clhs)
let bargs = getPBtys lhs_tm
let wval = addImplBound i (map fst bargs) wval_in
- logLvl 5 ("Checking " ++ showImp True wval)
+ logLvl 5 ("Checking " ++ showImp Nothing True False wval)
-- Elaborate wval in this context
((wval', defer, is), _) <-
tclift $ elaborate ctxt (MN 0 "withRHS")
(bindTyArgs PVTy bargs infP) []
(do pbinds lhs_tm
-- TODO: may want where here - see winfo abpve
- (_', d, is) <- erun fc (build i info False fname (infTerm wval))
+ (_', d, is) <- errAt "with value in " fname
+ (erun fc (build i info False fname (infTerm wval)))
erun fc $ psolve lhs_tm
tt <- get_term
return (tt, d, is))
@@ -929,7 +1014,7 @@
(map (pexp . (PRef fc) . fst) bargs_pre ++
pexp wval :
(map (pexp . (PRef fc) . fst) bargs_post))
- logLvl 5 ("New RHS " ++ showImp True rhs)
+ logLvl 5 ("New RHS " ++ showImp Nothing True False rhs)
ctxt <- getContext -- New context with block added
i <- getIState
((rhs', defer, is), _) <-
@@ -958,8 +1043,8 @@
mkAux wname toplhs ns ns' (PClause fc n tm_in (w:ws) rhs wheres)
= do i <- getIState
let tm = addImplPat i tm_in
- logLvl 2 ("Matching " ++ showImp True tm ++ " against " ++
- showImp True toplhs)
+ logLvl 2 ("Matching " ++ showImp Nothing True False tm ++ " against " ++
+ showImp Nothing True False toplhs)
case matchClause i toplhs tm of
Left f -> fail $ show fc ++ ":with clause does not match top level"
Right mvars ->
@@ -969,8 +1054,8 @@
mkAux wname toplhs ns ns' (PWith fc n tm_in (w:ws) wval withs)
= do i <- getIState
let tm = addImplPat i tm_in
- logLvl 2 ("Matching " ++ showImp True tm ++ " against " ++
- showImp True toplhs)
+ logLvl 2 ("Matching " ++ showImp Nothing True False tm ++ " against " ++
+ showImp Nothing True False toplhs)
withs' <- mapM (mkAuxC wname toplhs ns ns') withs
case matchClause i toplhs tm of
Left _ -> fail $ show fc ++ "with clause does not match top level"
@@ -1055,7 +1140,7 @@
pibind [] x = x
pibind ((n, ty): ns) x = PPi expl n ty (pibind ns x)
- mdec (UN n) = UN ('!':n)
+ mdec (UN n) = SN (MethodN (UN n))
mdec (NS x n) = NS (mdec x) n
mdec x = x
@@ -1067,7 +1152,7 @@
getMName (PTy _ _ _ _ n _) = nsroot n
tdecl allmeths (PTy doc syn _ o n t)
= do t' <- implicit' syn allmeths n t
- logLvl 5 $ "Method " ++ show n ++ " : " ++ showImp True t'
+ logLvl 5 $ "Method " ++ show n ++ " : " ++ showImp Nothing True False t'
return ( (n, (toExp (map fst ps) Exp t')),
(n, (doc, o, (toExp (map fst ps) Imp t'))),
(n, (syn, o, t) ) )
@@ -1079,7 +1164,7 @@
Just (syn, o, ty) -> do let ty' = insertConstraint c ty
let ds = map (decorateid defaultdec)
[PTy "" syn fc [] n ty',
- PClauses fc (Inlinable:TCGen:o ++ opts) n cs]
+ PClauses fc (o ++ opts) n cs]
iLOG (show ds)
return (n, ((defaultdec n, ds!!1), ds))
_ -> fail $ show n ++ " is not a method"
@@ -1093,15 +1178,17 @@
clause (PClauses _ _ _ _) = True
clause _ = False
+ -- Generate a function for chasing a dictionary constraint
cfun cn c syn all con
- = do let cfn = UN ('@':'@':show cn ++ "#" ++ show con)
+ = do let cfn = UN ('@':'@':show cn ++ "#" ++ show con)
+ -- SN (ParentN cn (show con))
let mnames = take (length all) $ map (\x -> MN x "meth") [0..]
let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)
let lhs = PApp fc (PRef fc cfn) [pconst capp]
let rhs = PResolveTC (FC "HACK" 0)
let ty = PPi constraint (MN 0 "pc") c con
- iLOG (showImp True ty)
- iLOG (showImp True lhs ++ " = " ++ showImp True rhs)
+ iLOG (showImp Nothing True False ty)
+ iLOG (showImp Nothing True False lhs ++ " = " ++ showImp Nothing True False rhs)
i <- getIState
let conn = case con of
PRef _ n -> n
@@ -1113,8 +1200,10 @@
addIBC (IBCInstance False conn' cfn)
-- iputStrLn ("Added " ++ show (conn, cfn, ty))
return [PTy "" syn fc [] cfn ty,
- PClauses fc [Inlinable,TCGen] cfn [PClause fc cfn lhs [] rhs []]]
+ PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]
+ -- Generate a top level function which looks up a method in a given
+ -- dictionary (this is inlinable, always)
tfun cn c syn all (m, (doc, o, ty))
= do let ty' = insertConstraint c ty
let mnames = take (length all) $ map (\x -> MN x "meth") [0..]
@@ -1123,11 +1212,11 @@
let anames = map (\x -> MN x "arg") [0..]
let lhs = PApp fc (PRef fc m) (pconst capp : lhsArgs margs anames)
let rhs = PApp fc (getMeth mnames all m) (rhsArgs margs anames)
- iLOG (showImp True ty)
+ iLOG (showImp Nothing True False ty)
iLOG (show (m, ty', capp, margs))
- iLOG (showImp True lhs ++ " = " ++ showImp True rhs)
+ iLOG (showImp Nothing True False lhs ++ " = " ++ showImp Nothing True False rhs)
return [PTy doc syn fc o m ty',
- PClauses fc [Inlinable,TCGen] m [PClause fc m lhs [] rhs []]]
+ PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []]]
getMArgs (PPi (Imp _ _ _) n ty sc) = IA : getMArgs sc
getMArgs (PPi (Exp _ _ _) n ty sc) = EA : getMArgs sc
@@ -1172,7 +1261,8 @@
_ -> fail $ show fc ++ ":" ++ show n ++ " is not a type class"
let constraint = PApp fc (PRef fc n) (map pexp ps)
let iname = case expn of
- Nothing -> UN ('@':show n ++ "$" ++ show ps)
+ Nothing -> SN (InstanceN n (map show ps))
+ -- UN ('@':show n ++ "$" ++ show ps)
Just nm -> nm
-- if the instance type matches any of the instances we have already,
-- and it's not a named instance, then it's overlapping, so report an error
@@ -1210,7 +1300,7 @@
let lhs = PRef fc iname
let rhs = PApp fc (PRef fc (instanceName ci))
(map (pexp . mkMethApp) mtys)
- let idecls = [PClauses fc [Inlinable, TCGen] iname
+ let idecls = [PClauses fc [Dictionary] iname
[PClause fc iname lhs [] rhs wb]]
iLOG (show idecls)
mapM (elabDecl EAll info) idecls
@@ -1269,8 +1359,8 @@
_ -> return ps'
getWParams (_ : ps) = getWParams ps
- decorate ns iname (UN n) = NS (UN ('!':n)) ns
- decorate ns iname (NS (UN n) s) = NS (UN ('!':n)) ns
+ decorate ns iname (UN n) = NS (SN (MethodN (UN n))) ns
+ decorate ns iname (NS (UN n) s) = NS (SN (MethodN (UN n))) ns
mkTyDecl (n, op, t, _) = PTy "" syn fc op n t
@@ -1332,7 +1422,7 @@
addIBC (IBCInstance False conn' cfn)
iputStrLn ("Added " ++ show (conn, cfn, ty) ++ "\n" ++ show (lhs, rhs))
return [PTy "" syn fc [] cfn ty,
- PClauses fc [Inlinable,TCGen] cfn [PClause fc cfn lhs [] rhs []]]
+ PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]
-}
decorateid decorate (PTy doc s f o n t) = PTy doc s f o (decorate n) t
@@ -1406,6 +1496,12 @@
elabDecl' what info (PMutual f ps)
= do mapM_ (elabDecl ETypes info) ps
mapM_ (elabDecl EDefns info) ps
+ -- Do totality checking after entire mutual block
+ i <- get
+ mapM_ buildSCG (idris_totcheck i)
+ mapM_ checkDeclTotality (idris_totcheck i)
+ clear_totcheck
+
elabDecl' what info (PParams f ns ps)
= do i <- getIState
iLOG $ "Expanding params block with " ++ show ns ++ " decls " ++
@@ -1430,7 +1526,7 @@
elabDecl' what info (PClass doc s f cs n ps ds)
| what /= EDefns
= do iLOG $ "Elaborating class " ++ show n
- elabClass info s doc f cs n ps ds
+ elabClass info (s { syn_params = [] }) doc f cs n ps ds
elabDecl' what info (PInstance s f cs n ps t expn ds)
| what /= ETypes
= do iLOG $ "Elaborating instance " ++ show n
@@ -1466,8 +1562,8 @@
checkInferred :: FC -> PTerm -> PTerm -> Idris ()
checkInferred fc inf user =
- do logLvl 6 $ "Checked to\n" ++ showImp True inf ++ "\n\nFROM\n\n" ++
- showImp True user
+ do logLvl 6 $ "Checked to\n" ++ showImp Nothing True False inf ++ "\n\nFROM\n\n" ++
+ showImp Nothing True False user
logLvl 10 $ "Checking match"
i <- getIState
tclift $ case matchClause' True i user inf of
@@ -1484,8 +1580,8 @@
inferredDiff :: FC -> PTerm -> PTerm -> Idris Bool
inferredDiff fc inf user =
do i <- getIState
- logLvl 6 $ "Checked to\n" ++ showImp True inf ++ "\n" ++
- showImp True user
+ logLvl 6 $ "Checked to\n" ++ showImp Nothing True False inf ++ "\n" ++
+ showImp Nothing True False user
tclift $ case matchClause' True i user inf of
Right vs -> return False
Left (x, y) -> return True
diff --git a/src/Idris/ElabTerm.hs b/src/Idris/ElabTerm.hs
--- a/src/Idris/ElabTerm.hs
+++ b/src/Idris/ElabTerm.hs
@@ -292,6 +292,22 @@
expandLet n (case lookup n env of
Just (Let t v) -> v)
solve
+ elab' ina@(_,a) (PGoal fc r n sc) = do
+ rty <- goal
+ attack
+ tyn <- unique_hole (MN 0 "letty")
+ claim tyn RType
+ valn <- unique_hole (MN 0 "letval")
+ claim valn (Var tyn)
+ letbind n (Var tyn) (Var valn)
+ focus valn
+ elabE (True, a) (PApp fc r [pexp (delab ist rty)])
+ env <- get_env
+ computeLet n
+ elabE (True, a) sc
+ solve
+-- elab' ina (PLet n Placeholder
+-- (PApp fc r [pexp (delab ist rty)]) sc)
elab' ina tm@(PApp fc (PInferRef _ f) args) = do
rty <- goal
ds <- get_deferred
@@ -333,6 +349,7 @@
elabIArg _ = return () -- already done, just a name
mkN n@(NS _ _) = n
+ mkN n@(SN _) = n
mkN n = case namespace info of
Just xs@(_:_) -> NS n xs
_ -> n
@@ -482,8 +499,10 @@
movelast tyn
solve
where mkCaseName (NS n ns) = NS (mkCaseName n) ns
- mkCaseName (UN x) = UN (x ++ "_case")
- mkCaseName (MN i x) = MN i (x ++ "_case")
+ mkCaseName n = SN (CaseN n)
+-- mkCaseName (UN x) = UN (x ++ "_case")
+-- mkCaseName (MN i x) = MN i (x ++ "_case")
+-- mkCaseName (SN s) =
mkN n@(NS _ _) = n
mkN n = case namespace info of
Just xs@(_:_) -> NS n xs
@@ -651,7 +670,7 @@
scopeOnly <- needsDefault t tc ttypes
let insts_in = findInstances ist t
let insts = if scopeOnly then filter chaser insts_in
- else insts_in
+ else insts_in
tm <- get_term
-- traceWhen (depth > 6) ("GOAL: " ++ show t ++ "\nTERM: " ++ show tm) $
-- (tryAll (map elabTC (map fst (ctxtAlist (tt_ctxt ist)))))
@@ -669,7 +688,8 @@
-- HACK! Rather than giving a special name, better to have some kind
-- of flag in ClassInfo structure
- chaser (UN ('@':'@':_)) = True
+ chaser (UN ('@':'@':_)) = True -- old way
+ chaser (SN (ParentN _ _)) = True
chaser (NS n _) = chaser n
chaser _ = False
@@ -761,11 +781,15 @@
runT (Exact tm) = do elab ist toplevel False False (MN 0 "tac") tm
when autoSolve solveAll
runT (MatchRefine fn)
- = do (fn', imps) <- case lookupCtxtName fn (idris_implicits ist) of
- [] -> do a <- envArgs fn
- return (fn, a)
- [(n, args)] -> return $ (n, map (const True) args)
- ns <- match_apply (Var fn') (map (\x -> (x, 0)) imps)
+ = do fnimps <-
+ case lookupCtxtName fn (idris_implicits ist) of
+ [] -> do a <- envArgs fn
+ return [(fn, a)]
+ ns -> return (map (\ (n, a) -> (n, map (const True) a)) ns)
+ let tacs = map (\ (fn', imps) ->
+ (match_apply (Var fn') (map (\x -> (x, 0)) imps),
+ show fn')) fnimps
+ tryAll tacs
when autoSolve solveAll
where envArgs n = do e <- get_env
case lookup n e of
@@ -773,12 +797,15 @@
(getArgTys (binderTy t))
_ -> return []
runT (Refine fn [])
- = do (fn', imps) <- case lookupCtxtName fn (idris_implicits ist) of
- [] -> do a <- envArgs fn
- return (fn, a)
- -- FIXME: resolve ambiguities
- [(n, args)] -> return $ (n, map isImp args)
- ns <- apply (Var fn') (map (\x -> (x, 0)) imps)
+ = do fnimps <-
+ case lookupCtxtName fn (idris_implicits ist) of
+ [] -> do a <- envArgs fn
+ return [(fn, a)]
+ ns -> return (map (\ (n, a) -> (n, map isImp a)) ns)
+ let tacs = map (\ (fn', imps) ->
+ (apply (Var fn') (map (\x -> (x, 0)) imps),
+ show fn')) fnimps
+ tryAll tacs
when autoSolve solveAll
where isImp (PImp _ _ _ _ _) = True
isImp _ = False
@@ -1185,6 +1212,7 @@
reflectName (MN i n)
= reflCall "MN" [RConstant (I i), RConstant (Str n)]
reflectName (NErased) = Var (reflm "NErased")
+reflectName n = Var (reflm "NErased") -- special name, not yet implemented
reflectBinder :: Binder Term -> Raw
reflectBinder (Lam t)
@@ -1270,9 +1298,9 @@
mkSpecialised i fc n args def
= do let tm' = def
case lookupCtxt n (idris_statics i) of
- [] -> return tm'
[as] -> if (not (or as)) then return tm' else
mkSpecDecl i n (zip args as) tm'
+ _ -> return tm'
mkSpecDecl :: IState -> Name -> [(PTerm, Bool)] -> PTerm -> ElabD PTerm
mkSpecDecl i n pargs tm'
diff --git a/src/Idris/Help.hs b/src/Idris/Help.hs
--- a/src/Idris/Help.hs
+++ b/src/Idris/Help.hs
@@ -6,17 +6,19 @@
| ModuleArg -- ^ The command takes a module name
| OptionArg -- ^ The command takes an option
| MetaVarArg -- ^ The command takes a metavariable
+ | ColourArg -- ^ The command is the colour-setting command
| NoArg -- ^ No completion (yet!?)
| SpecialHeaderArg -- ^ do not use
instance Show CmdArg where
- show ExprArg = ""
- show NameArg = ""
- show FileArg = ""
- show ModuleArg = ""
- show OptionArg = "