idris 0.9.6 → 0.9.6.1
raw patch · 56 files changed
+3527/−778 lines, 56 files
Files
- idris.cabal +6/−2
- js/Runtime-browser.js +3/−0
- js/Runtime-common.js +386/−0
- js/Runtime-node.js +6/−0
- lib/Builtins.idr +8/−0
- lib/Control/Arrow.idr +5/−4
- lib/Data/Bits.idr +432/−18
- lib/Data/Mod2.idr +64/−0
- lib/Data/Word.idr +0/−19
- lib/Makefile +1/−1
- lib/Prelude.idr +5/−3
- lib/Prelude/Fin.idr +17/−5
- lib/Prelude/Heap.idr +1/−1
- lib/Prelude/Nat.idr +6/−0
- lib/Prelude/Strings.idr +2/−2
- lib/Prelude/Vect.idr +2/−2
- lib/base.ipkg +1/−1
- rts/Makefile +2/−2
- rts/idris_bitstring.c +666/−0
- rts/idris_bitstring.h +125/−0
- rts/idris_gc.c +13/−0
- rts/idris_rts.c +13/−0
- rts/idris_rts.h +6/−1
- rts/libidris_rts.a binary
- src/Core/CaseTree.hs +6/−4
- src/Core/Constraints.hs +4/−0
- src/Core/CoreParser.hs +1/−1
- src/Core/Elaborate.hs +45/−21
- src/Core/Evaluate.hs +6/−3
- src/Core/ProofShell.hs +21/−17
- src/Core/ProofState.hs +98/−45
- src/Core/TT.hs +21/−11
- src/Core/Typecheck.hs +9/−5
- src/Core/Unify.hs +109/−44
- src/IRTS/CodegenC.hs +140/−2
- src/IRTS/CodegenJavaScript.hs +181/−182
- src/IRTS/Compiler.hs +20/−12
- src/IRTS/Lang.hs +17/−4
- src/Idris/AbsSyntax.hs +92/−92
- src/Idris/AbsSyntaxTree.hs +10/−3
- src/Idris/Completion.hs +143/−0
- src/Idris/Coverage.hs +38/−21
- src/Idris/DataOpts.hs +2/−2
- src/Idris/ElabDecls.hs +157/−52
- src/Idris/ElabTerm.hs +145/−59
- src/Idris/Error.hs +3/−3
- src/Idris/IBC.hs +37/−22
- src/Idris/Parser.hs +19/−16
- src/Idris/Primitives.hs +337/−26
- src/Idris/Prover.hs +30/−13
- src/Idris/REPL.hs +55/−47
- src/Idris/REPLParser.hs +1/−1
- src/Idris/UnusedArgs.hs +2/−2
- src/Main.hs +2/−2
- tutorial/examples/binary.idr +3/−5
- tutorial/examples/interp.idr +3/−0
idris.cabal view
@@ -1,5 +1,5 @@ Name: idris-Version: 0.9.6+Version: 0.9.6.1 License: BSD3 License-file: LICENSE Author: Edwin Brady@@ -47,6 +47,9 @@ Data-files: rts/libidris_rts.a rts/idris_rts.h rts/idris_gc.h rts/idris_stdfgn.h rts/idris_main.c rts/idris_gmp.h rts/libtest.c+ js/Runtime-common.js+ js/Runtime-node.js+ js/Runtime-browser.js Extra-source-files: lib/Makefile lib/*.idr lib/Prelude/*.idr lib/Network/*.idr lib/Control/*.idr lib/Control/Monad/*.idr lib/Language/*.idr@@ -55,6 +58,7 @@ tutorial/examples/*.idr lib/base.ipkg config.mk rts/*.c rts/*.h rts/Makefile+ js/*.js source-repository head type: git@@ -76,7 +80,7 @@ Idris.Compiler, Idris.Prover, Idris.ElabTerm, Idris.Coverage, Idris.IBC, Idris.Unlit, Idris.DataOpts, Idris.Transforms, Idris.DSL, - Idris.UnusedArgs, Idris.Docs,+ Idris.UnusedArgs, Idris.Docs, Idris.Completion, Util.Pretty, Util.System, Pkg.Package, Pkg.PParser,
+ js/Runtime-browser.js view
@@ -0,0 +1,3 @@+__IDRRT__.print = function(s) {+ console.log(s);+};
+ js/Runtime-common.js view
@@ -0,0 +1,386 @@+var __IDRRT__ = {};++/** @constructor */+__IDRRT__.Type = function(type) {+ this.type = type;+};++__IDRRT__.Int = new __IDRRT__.Type('Int');+__IDRRT__.Char = new __IDRRT__.Type('Char');+__IDRRT__.String = new __IDRRT__.Type('String');+__IDRRT__.Integer = new __IDRRT__.Type('Integer');+__IDRRT__.Float = new __IDRRT__.Type('Float');+__IDRRT__.Forgot = new __IDRRT__.Type('Forgot');++/** @constructor */+__IDRRT__.Tailcall = function(f) { this.f = f };++/** @constructor */+__IDRRT__.Con = function(i,vars) {+ this.i = i;+ this.vars = vars;+};++__IDRRT__.tailcall = function(f) {+ var __f = f;+ var ret;+ while (__f) {+ f = __f;+ __f = null;+ ret = f();++ if (ret instanceof __IDRRT__.Tailcall) {+ __f = ret.f;+ } else {+ return ret;+ }+ }+};++/*+ BigInteger Javascript code taken from:+ https://github.com/peterolson+*/+__IDRRT__.bigInt = (function () {+ var base = 10000000, logBase = 7;+ var sign = {+ positive: false,+ negative: true+ };++ var normalize = function (first, second) {+ var a = first.value, b = second.value;+ var length = a.length > b.length ? a.length : b.length;+ for (var i = 0; i < length; i++) {+ a[i] = a[i] || 0;+ b[i] = b[i] || 0;+ }+ for (var i = length - 1; i >= 0; i--) {+ if (a[i] === 0 && b[i] === 0) {+ a.pop();+ b.pop();+ } else break;+ }+ if (!a.length) a = [0], b = [0];+ first.value = a;+ second.value = b;+ };++ var parse = function (text, first) {+ if (typeof text === "object") return text;+ text += "";+ var s = sign.positive, value = [];+ if (text[0] === "-") {+ s = sign.negative;+ text = text.slice(1);+ }+ var text = text.split("e");+ if (text.length > 2) throw new Error("Invalid integer");+ if (text[1]) {+ var exp = text[1];+ if (exp[0] === "+") exp = exp.slice(1);+ exp = parse(exp);+ if (exp.lesser(0)) throw new Error("Cannot include negative exponent part for integers");+ while (exp.notEquals(0)) {+ text[0] += "0";+ exp = exp.prev();+ }+ }+ text = text[0];+ if (text === "-0") text = "0";+ var isValid = /^([0-9][0-9]*)$/.test(text);+ if (!isValid) throw new Error("Invalid integer");+ while (text.length) {+ var divider = text.length > logBase ? text.length - logBase : 0;+ value.push(+text.slice(divider));+ text = text.slice(0, divider);+ }+ var val = bigInt(value, s);+ if (first) normalize(first, val);+ return val;+ };++ var goesInto = function (a, b) {+ var a = bigInt(a, sign.positive), b = bigInt(b, sign.positive);+ if (a.equals(0)) throw new Error("Cannot divide by 0");+ var n = 0;+ do {+ var inc = 1;+ var c = bigInt(a.value, sign.positive), t = c.times(10);+ while (t.lesser(b)) {+ c = t;+ inc *= 10;+ t = t.times(10);+ }+ while (c.lesserOrEquals(b)) {+ b = b.minus(c);+ n += inc;+ }+ } while (a.lesserOrEquals(b));++ return {+ remainder: b.value,+ result: n+ };+ };++ var bigInt = function (value, s) {+ var self = {+ value: value,+ sign: s+ };+ var o = {+ value: value,+ sign: s,+ negate: function (m) {+ var first = m || self;+ return bigInt(first.value, !first.sign);+ },+ abs: function (m) {+ var first = m || self;+ return bigInt(first.value, sign.positive);+ },+ add: function (n, m) {+ var s, first = self, second;+ if (m) (first = parse(n)) && (second = parse(m));+ else second = parse(n, first);+ s = first.sign;+ if (first.sign !== second.sign) {+ first = bigInt(first.value, sign.positive);+ second = bigInt(second.value, sign.positive);+ return s === sign.positive ?+ o.subtract(first, second) :+ o.subtract(second, first);+ }+ normalize(first, second);+ var a = first.value, b = second.value;+ var result = [],+ carry = 0;+ for (var i = 0; i < a.length || carry > 0; i++) {+ var sum = (a[i] || 0) + (b[i] || 0) + carry;+ carry = sum >= base ? 1 : 0;+ sum -= carry * base;+ result.push(sum);+ }+ return bigInt(result, s);+ },+ plus: function (n, m) {+ return o.add(n, m);+ },+ subtract: function (n, m) {+ var first = self, second;+ if (m) (first = parse(n)) && (second = parse(m));+ else second = parse(n, first);+ if (first.sign !== second.sign) return o.add(first, o.negate(second));+ if (first.sign === sign.negative) return o.subtract(o.negate(second), o.negate(first));+ if (o.compare(first, second) === -1) return o.negate(o.subtract(second, first));+ var a = first.value, b = second.value;+ var result = [],+ borrow = 0;+ for (var i = 0; i < a.length; i++) {+ a[i] -= borrow;+ borrow = a[i] < b[i] ? 1 : 0;+ var minuend = (borrow * base) + a[i] - b[i];+ result.push(minuend);+ }+ return bigInt(result, sign.positive);+ },+ minus: function (n, m) {+ return o.subtract(n, m);+ },+ multiply: function (n, m) {+ var s, first = self, second;+ if (m) (first = parse(n)) && (second = parse(m));+ else second = parse(n, first);+ s = first.sign !== second.sign;+ var a = first.value, b = second.value;+ var resultSum = [];+ for (var i = 0; i < a.length; i++) {+ resultSum[i] = [];+ var j = i;+ while (j--) {+ resultSum[i].push(0);+ }+ }+ var carry = 0;+ for (var i = 0; i < a.length; i++) {+ var x = a[i];+ for (var j = 0; j < b.length || carry > 0; j++) {+ var y = b[j];+ var product = y ? (x * y) + carry : carry;+ carry = product > base ? Math.floor(product / base) : 0;+ product -= carry * base;+ resultSum[i].push(product);+ }+ }+ var max = -1;+ for (var i = 0; i < resultSum.length; i++) {+ var len = resultSum[i].length;+ if (len > max) max = len;+ }+ var result = [], carry = 0;+ for (var i = 0; i < max || carry > 0; i++) {+ var sum = carry;+ for (var j = 0; j < resultSum.length; j++) {+ sum += resultSum[j][i] || 0;+ }+ carry = sum > base ? Math.floor(sum / base) : 0;+ sum -= carry * base;+ result.push(sum);+ }+ return bigInt(result, s);+ },+ times: function (n, m) {+ return o.multiply(n, m);+ },+ divmod: function (n, m) {+ var s, first = self, second;+ if (m) (first = parse(n)) && (second = parse(m));+ else second = parse(n, first);+ s = first.sign !== second.sign;+ if (bigInt(first.value, first.sign).equals(0)) return {+ quotient: bigInt([0], sign.positive),+ remainder: bigInt([0], sign.positive)+ };+ if (second.equals(0)) throw new Error("Cannot divide by zero");+ var a = first.value, b = second.value;+ var result = [], remainder = [];+ for (var i = a.length - 1; i >= 0; i--) {+ var n = [a[i]].concat(remainder);+ var quotient = goesInto(b, n);+ result.push(quotient.result);+ remainder = quotient.remainder;+ }+ result.reverse();+ return {+ quotient: bigInt(result, s),+ remainder: bigInt(remainder, first.sign)+ };+ },+ divide: function (n, m) {+ return o.divmod(n, m).quotient;+ },+ over: function (n, m) {+ return o.divide(n, m);+ },+ mod: function (n, m) {+ return o.divmod(n, m).remainder;+ },+ pow: function (n, m) {+ var first = self, second;+ if (m) (first = parse(n)) && (second = parse(m));+ else second = parse(n, first);+ var a = first, b = second;+ if (b.lesser(0)) return ZERO;+ if (b.equals(0)) return ONE;+ var result = bigInt(a.value, a.sign);++ if (b.mod(2).equals(0)) {+ var c = result.pow(b.over(2));+ return c.times(c);+ } else {+ return result.times(result.pow(b.minus(1)));+ }+ },+ next: function (m) {+ var first = m || self;+ return o.add(first, 1);+ },+ prev: function (m) {+ var first = m || self;+ return o.subtract(first, 1);+ },+ compare: function (n, m) {+ var first = self, second;+ if (m) (first = parse(n)) && (second = parse(m, first));+ else second = parse(n, first);+ normalize(first, second);+ if (first.value.length === 1 && second.value.length === 1 && first.value[0] === 0 && second.value[0] === 0) return 0;+ if (second.sign !== first.sign) return first.sign === sign.positive ? 1 : -1;+ var multiplier = first.sign === sign.positive ? 1 : -1;+ var a = first.value, b = second.value;+ for (var i = a.length - 1; i >= 0; i--) {+ if (a[i] > b[i]) return 1 * multiplier;+ if (b[i] > a[i]) return -1 * multiplier;+ }+ return 0;+ },+ compareAbs: function (n, m) {+ var first = self, second;+ if (m) (first = parse(n)) && (second = parse(m, first));+ else second = parse(n, first);+ first.sign = second.sign = sign.positive;+ return o.compare(first, second);+ },+ equals: function (n, m) {+ return o.compare(n, m) === 0;+ },+ notEquals: function (n, m) {+ return !o.equals(n, m);+ },+ lesser: function (n, m) {+ return o.compare(n, m) < 0;+ },+ greater: function (n, m) {+ return o.compare(n, m) > 0;+ },+ greaterOrEquals: function (n, m) {+ return o.compare(n, m) >= 0;+ },+ lesserOrEquals: function (n, m) {+ return o.compare(n, m) <= 0;+ },+ isPositive: function (m) {+ var first = m || self;+ return first.sign === sign.positive;+ },+ isNegative: function (m) {+ var first = m || self;+ return first.sign === sign.negative;+ },+ isEven: function (m) {+ var first = m || self;+ return first.value[0] % 2 === 0;+ },+ isOdd: function (m) {+ var first = m || self;+ return first.value[0] % 2 === 1;+ },+ toString: function (m) {+ var first = m || self;+ var str = "", len = first.value.length;+ while (len--) {+ str += (base.toString() + first.value[len]).slice(-logBase);+ }+ while (str[0] === "0") {+ str = str.slice(1);+ }+ if (!str.length) str = "0";+ var s = first.sign === sign.positive ? "" : "-";+ return s + str;+ },+ toJSNumber: function (m) {+ return +o.toString(m);+ },+ valueOf: function (m) {+ return o.toJSNumber(m);+ }+ };+ return o;+ };++ var ZERO = bigInt([0], sign.positive);+ var ONE = bigInt([1], sign.positive);+ var MINUS_ONE = bigInt([1], sign.negative);++ var fnReturn = function (a) {+ if (typeof a === "undefined") return ZERO;+ return parse(a);+ };+ fnReturn.zero = ZERO;+ fnReturn.one = ONE;+ fnReturn.minusOne = MINUS_ONE;+ return fnReturn;+})();++var __IDR__ = {};
+ js/Runtime-node.js view
@@ -0,0 +1,6 @@+__IDRRT__.print = (function() {+ var util = require('util');+ return function(s) {+ util.print(s);+ };+})();
lib/Builtins.idr view
@@ -38,6 +38,10 @@ 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!+really_believe_me : a -> b +really_believe_me x = prim__believe_me _ _ x+ namespace Builtins { id : a -> a@@ -78,6 +82,10 @@ boolElim False t e = e data so : Bool -> Type where oh : so True++data Equality : {A : Type} -> (x : A) -> (y : A) -> Type where+ Unequal : {A : Type} -> {x : A} -> {y : A} -> (x = y -> _|_) -> Equality x y+ Equal : {A : Type} -> {x : A} -> {y : A} -> (x = y) -> Equality x y syntax if [test] then [t] else [e] = boolElim test t e syntax [test] "?" [t] ":" [e] = if test then t else e
lib/Control/Arrow.idr view
@@ -24,16 +24,17 @@ instance Monad m => Arrow (Kleislimorphism m) where arrow f = Kleisli (return . f)- first (Kleisli f) = Kleisli $ \(a, b) => do x <- f a- return (x, b)+ first (Kleisli f) = Kleisli $ \(a, b) => do x <- f a+ return (x, b) second (Kleisli f) = Kleisli $ \(a, b) => do x <- f b return (a, x) - (Kleisli f) *** (Kleisli g) = Kleisli $ \(a, b) => do x <- f a+ (Kleisli f) *** (Kleisli g) = Kleisli $ \(a, b) => do x <- f a y <- g b return (x, y) - (Kleisli f) &&& (Kleisli g) = Kleisli $ \a => do x <- f a+ (Kleisli f) &&& (Kleisli g) = Kleisli $ \a => do x <- f a y <- g a return (x, y)+
lib/Data/Bits.idr view
@@ -1,25 +1,439 @@ module Data.Bits -%access public-%default partial+%default total -infixl 5 .|.-infixl 7 .&.+divCeil : Nat -> Nat -> Nat+divCeil x y = case x `mod` y of+ O => x `div` y+ S _ => S (x `div` y) -class Num a => Bits a where- (.|.) : a -> a -> a- (.&.) : a -> a -> a+nextPow2 : Nat -> Nat+nextPow2 O = O+nextPow2 x = if x == (2 `power` l2x)+ then l2x+ else S l2x+ where+ l2x = log2 x - xor : a -> a -> a- complement : a -> a- shiftL : a -> Int -> a- shiftR : a -> Int -> a+nextBytes : Nat -> Nat+nextBytes bits = (nextPow2 (bits `divCeil` 8)) -instance Bits Int where- (.|.) = prim__orInt- (.&.) = prim__andInt+machineTy : Nat -> Type+machineTy O = Bits8+machineTy (S O) = Bits16+machineTy (S (S O)) = Bits32+machineTy (S (S (S _))) = Bits64 - xor = prim__xorInt- complement = prim__complInt- shiftL = prim__shLInt- shiftR = prim__shRInt+bitsUsed : Nat -> Nat+bitsUsed n = 8 * (2 `power` n)++%assert_total+natToBits' : machineTy n -> Nat -> machineTy n+natToBits' a O = a+natToBits' {n=n} a x with n+ natToBits' a (S x') | O = natToBits' (prim__addB8 a (prim__intToB8 1)) x'+ natToBits' a (S x') | S O = natToBits' (prim__addB16 a (prim__intToB16 1)) x'+ natToBits' a (S x') | S (S O) = natToBits' (prim__addB32 a (prim__intToB32 1)) x'+ natToBits' a (S x') | S (S (S _)) = natToBits' (prim__addB64 a (prim__intToB64 1)) x'++natToBits : Nat -> machineTy n+natToBits {n=n} x with n+ | O = natToBits' (prim__intToB8 0) x+ | S O = natToBits' (prim__intToB16 0) x+ | S (S O) = natToBits' (prim__intToB32 0) x+ | S (S (S _)) = natToBits' (prim__intToB64 0) x++getPad : Nat -> machineTy n+getPad n = natToBits ((bitsUsed (nextBytes n)) - n)++public+data Bits : Nat -> Type where+ MkBits : machineTy (nextBytes n) -> Bits n++pad8 : Nat -> (Bits8 -> Bits8 -> Bits8) -> Bits8 -> Bits8 -> Bits8+pad8 n f x y = prim__lshrB8 (f (prim__shlB8 x pad) (prim__shlB8 y pad)) pad+ where+ pad = getPad {n=0} n++pad16 : Nat -> (Bits16 -> Bits16 -> Bits16) -> Bits16 -> Bits16 -> Bits16+pad16 n f x y = prim__lshrB16 (f (prim__shlB16 x pad) (prim__shlB16 y pad)) pad+ where+ pad = getPad {n=1} n++pad32 : Nat -> (Bits32 -> Bits32 -> Bits32) -> Bits32 -> Bits32 -> Bits32+pad32 n f x y = prim__lshrB32 (f (prim__shlB32 x pad) (prim__shlB32 y pad)) pad+ where+ pad = getPad {n=2} n++pad64 : Nat -> (Bits64 -> Bits64 -> Bits64) -> Bits64 -> Bits64 -> Bits64+pad64 n f x y = prim__lshrB64 (f (prim__shlB64 x pad) (prim__shlB64 y pad)) pad+ where+ pad = getPad {n=3} n++-- These versions only pad the first operand+pad8' : Nat -> (Bits8 -> Bits8 -> Bits8) -> Bits8 -> Bits8 -> Bits8+pad8' n f x y = prim__lshrB8 (f (prim__shlB8 x pad) y) pad+ where+ pad = getPad {n=0} n++pad16' : Nat -> (Bits16 -> Bits16 -> Bits16) -> Bits16 -> Bits16 -> Bits16+pad16' n f x y = prim__lshrB16 (f (prim__shlB16 x pad) y) pad+ where+ pad = getPad {n=1} n++pad32' : Nat -> (Bits32 -> Bits32 -> Bits32) -> Bits32 -> Bits32 -> Bits32+pad32' n f x y = prim__lshrB32 (f (prim__shlB32 x pad) y) pad+ where+ pad = getPad {n=2} n++pad64' : Nat -> (Bits64 -> Bits64 -> Bits64) -> Bits64 -> Bits64 -> Bits64+pad64' n f x y = prim__lshrB64 (f (prim__shlB64 x pad) y) pad+ where+ pad = getPad {n=3} n++shiftLeft' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)+shiftLeft' {n=n} x c with (nextBytes n)+ | O = pad8' n prim__shlB8 x c+ | S O = pad16' n prim__shlB16 x c+ | S (S O) = pad32' n prim__shlB32 x c+ | S (S (S _)) = pad64' n prim__shlB64 x c++public+shiftLeft : Bits n -> Bits n -> Bits n+shiftLeft (MkBits x) (MkBits y) = MkBits (shiftLeft' x y)++shiftRightLogical' : machineTy n -> machineTy n -> machineTy n+shiftRightLogical' {n=n} x c with n+ | O = prim__lshrB8 x c+ | S O = prim__lshrB16 x c+ | S (S O) = prim__lshrB32 x c+ | S (S (S _)) = prim__lshrB64 x c++public+shiftRightLogical : Bits n -> Bits n -> Bits n+shiftRightLogical (MkBits x) (MkBits y) = MkBits (shiftRightLogical' x y)++shiftRightArithmetic' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)+shiftRightArithmetic' {n=n} x c with (nextBytes n)+ | O = pad8' n prim__ashrB8 x c+ | S O = pad16' n prim__ashrB16 x c+ | S (S O) = pad32' n prim__ashrB32 x c+ | S (S (S _)) = pad64' n prim__ashrB64 x c++public+shiftRightArithmetic : Bits n -> Bits n -> Bits n+shiftRightArithmetic (MkBits x) (MkBits y) = MkBits (shiftRightArithmetic' x y)++and' : machineTy n -> machineTy n -> machineTy n+and' {n=n} x y with n+ | O = prim__andB8 x y+ | S O = prim__andB16 x y+ | S (S O) = prim__andB32 x y+ | S (S (S _)) = prim__andB64 x y++public+and : Bits n -> Bits n -> Bits n+and (MkBits x) (MkBits y) = MkBits (and' x y)++or' : machineTy n -> machineTy n -> machineTy n+or' {n=n} x y with n+ | O = prim__orB8 x y+ | S O = prim__orB16 x y+ | S (S O) = prim__orB32 x y+ | S (S (S _)) = prim__orB64 x y++public+or : Bits n -> Bits n -> Bits n+or (MkBits x) (MkBits y) = MkBits (or' x y)++xor' : machineTy n -> machineTy n -> machineTy n+xor' {n=n} x y with n+ | O = prim__xorB8 x y+ | S O = prim__xorB16 x y+ | S (S O) = prim__xorB32 x y+ | S (S (S _)) = prim__xorB64 x y++public+xor : Bits n -> Bits n -> Bits n+xor (MkBits x) (MkBits y) = MkBits (xor' x y)++plus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)+plus' {n=n} x y with (nextBytes n)+ | O = pad8 n prim__addB8 x y+ | S O = pad16 n prim__addB16 x y+ | S (S O) = pad32 n prim__addB32 x y+ | S (S (S _)) = pad64 n prim__addB64 x y++public+plus : Bits n -> Bits n -> Bits n+plus (MkBits x) (MkBits y) = MkBits (plus' x y)++minus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)+minus' {n=n} x y with (nextBytes n)+ | O = pad8 n prim__subB8 x y+ | S O = pad16 n prim__subB16 x y+ | S (S O) = pad32 n prim__subB32 x y+ | S (S (S _)) = pad64 n prim__subB64 x y++public+minus : Bits n -> Bits n -> Bits n+minus (MkBits x) (MkBits y) = MkBits (minus' x y)++times' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)+times' {n=n} x y with (nextBytes n)+ | O = pad8 n prim__mulB8 x y+ | S O = pad16 n prim__mulB16 x y+ | S (S O) = pad32 n prim__mulB32 x y+ | S (S (S _)) = pad64 n prim__mulB64 x y++public+times : Bits n -> Bits n -> Bits n+times (MkBits x) (MkBits y) = MkBits (times' x y)++partial+sdiv' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)+sdiv' {n=n} x y with (nextBytes n)+ | O = prim__sdivB8 x y+ | S O = prim__sdivB16 x y+ | S (S O) = prim__sdivB32 x y+ | S (S (S _)) = prim__sdivB64 x y++public partial+sdiv : Bits n -> Bits n -> Bits n+sdiv (MkBits x) (MkBits y) = MkBits (sdiv' x y)++partial+udiv' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)+udiv' {n=n} x y with (nextBytes n)+ | O = prim__udivB8 x y+ | S O = prim__udivB16 x y+ | S (S O) = prim__udivB32 x y+ | S (S (S _)) = prim__udivB64 x y++public partial+udiv : Bits n -> Bits n -> Bits n+udiv (MkBits x) (MkBits y) = MkBits (udiv' x y)++partial+srem' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)+srem' {n=n} x y with (nextBytes n)+ | O = prim__sremB8 x y+ | S O = prim__sremB16 x y+ | S (S O) = prim__sremB32 x y+ | S (S (S _)) = prim__sremB64 x y++public partial+srem : Bits n -> Bits n -> Bits n+srem (MkBits x) (MkBits y) = MkBits (srem' x y)++partial+urem' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)+urem' {n=n} x y with (nextBytes n)+ | O = prim__uremB8 x y+ | S O = prim__uremB16 x y+ | S (S O) = prim__uremB32 x y+ | S (S (S _)) = prim__uremB64 x y++public partial+urem : Bits n -> Bits n -> Bits n+urem (MkBits x) (MkBits y) = MkBits (urem' x y)++-- TODO: Proofy comparisons via postulates+lt : machineTy n -> machineTy n -> Int+lt {n=n} x y with n+ | O = prim__ltB8 x y+ | S O = prim__ltB16 x y+ | S (S O) = prim__ltB32 x y+ | S (S (S _)) = prim__ltB64 x y++lte : machineTy n -> machineTy n -> Int+lte {n=n} x y with n+ | O = prim__lteB8 x y+ | S O = prim__lteB16 x y+ | S (S O) = prim__lteB32 x y+ | S (S (S _)) = prim__lteB64 x y++eq : machineTy n -> machineTy n -> Int+eq {n=n} x y with n+ | O = prim__eqB8 x y+ | S O = prim__eqB16 x y+ | S (S O) = prim__eqB32 x y+ | S (S (S _)) = prim__eqB64 x y++gte : machineTy n -> machineTy n -> Int+gte {n=n} x y with n+ | O = prim__gteB8 x y+ | S O = prim__gteB16 x y+ | S (S O) = prim__gteB32 x y+ | S (S (S _)) = prim__gteB64 x y++gt : machineTy n -> machineTy n -> Int+gt {n=n} x y with n+ | O = prim__gtB8 x y+ | S O = prim__gtB16 x y+ | S (S O) = prim__gtB32 x y+ | S (S (S _)) = prim__gtB64 x y++instance Eq (Bits n) where+ (MkBits x) == (MkBits y) = boolOp eq x y++instance Ord (Bits n) where+ (MkBits x) < (MkBits y) = boolOp lt x y+ (MkBits x) <= (MkBits y) = boolOp lte x y+ (MkBits x) >= (MkBits y) = boolOp gte x y+ (MkBits x) > (MkBits y) = boolOp gt x y+ compare (MkBits x) (MkBits y) =+ if boolOp lt x y+ then LT+ else if boolOp eq x y+ then EQ+ else GT++complement' : machineTy (nextBytes n) -> machineTy (nextBytes n)+complement' {n=n} x with (nextBytes n)+ | O = let pad = getPad {n=0} n in+ prim__complB8 (x `prim__shlB8` pad) `prim__lshrB8` pad+ | S O = let pad = getPad {n=1} n in+ prim__complB16 (x `prim__shlB16` pad) `prim__lshrB16` pad+ | S (S O) = let pad = getPad {n=2} n in+ prim__complB32 (x `prim__shlB32` pad) `prim__lshrB32` pad+ | S (S (S _)) = let pad = getPad {n=3} n in+ prim__complB64 (x `prim__shlB64` pad) `prim__lshrB64` pad++public+complement : Bits n -> Bits n+complement (MkBits x) = MkBits (complement' x)++-- TODO: Prove+zext' : machineTy (nextBytes n) -> machineTy (nextBytes (n+m))+zext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))+ | (O, O) = believe_me x+ | (O, S O) = believe_me (prim__zextB8_16 (believe_me x))+ | (O, S (S O)) = believe_me (prim__zextB8_32 (believe_me x))+ | (O, S (S (S _))) = believe_me (prim__zextB8_64 (believe_me x))+ | (S O, S O) = believe_me x+ | (S O, S (S O)) = believe_me (prim__zextB16_32 (believe_me x))+ | (S O, S (S (S _))) = believe_me (prim__zextB16_64 (believe_me x))+ | (S (S O), S (S O)) = believe_me x+ | (S (S O), S (S (S _))) = believe_me (prim__zextB32_64 (believe_me x))+ | (S (S (S _)), S (S (S _))) = believe_me x++public+zeroExtend : Bits n -> Bits (n+m)+zeroExtend (MkBits x) = MkBits (zext' x)++%assert_total+intToBits' : Int -> machineTy (nextBytes n)+intToBits' {n=n} x with (nextBytes n)+ | O = let pad = getPad {n=0} n in+ prim__lshrB8 (prim__shlB8 (prim__intToB8 x) pad) pad+ | S O = let pad = getPad {n=1} n in+ prim__lshrB16 (prim__shlB16 (prim__intToB16 x) pad) pad+ | S (S O) = let pad = getPad {n=2} n in+ prim__lshrB32 (prim__shlB32 (prim__intToB32 x) pad) pad+ | S (S (S _)) = let pad = getPad {n=3} n in+ prim__lshrB64 (prim__shlB64 (prim__intToB64 x) pad) pad++public+intToBits : Int -> Bits n+intToBits n = MkBits (intToBits' n)++instance Cast Int (Bits n) where+ cast = intToBits++bitsToInt' : machineTy n -> Int+bitsToInt' {n=n} x with n+ | O = prim__B32ToInt (prim__zextB8_32 x)+ | S O = prim__B32ToInt (prim__zextB16_32 x)+ | S (S O) = prim__B32ToInt x+ | S (S (S _)) = prim__B32ToInt (prim__truncB64_32 x)++public+bitsToInt : Bits n -> Int+bitsToInt (MkBits x) = bitsToInt' x++-- Zero out the high bits of a truncated bitstring+zeroUnused : machineTy (nextBytes n) -> machineTy (nextBytes n)+zeroUnused x = x `and'` complement' (intToBits' 0)++instance Cast Nat (Bits n) where+ cast x = MkBits (zeroUnused (natToBits n))++-- TODO: Prove+sext' : machineTy (nextBytes n) -> machineTy (nextBytes (n+m))+sext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))+ | (O, O) = let pad = getPad {n=0} n in+ believe_me (prim__ashrB8 (prim__shlB8 (believe_me x) pad) pad)+ | (O, S O) = let pad = getPad {n=0} n in+ believe_me (prim__ashrB16 (prim__sextB8_16 (prim__shlB8 (believe_me x) pad))+ (prim__zextB8_16 pad))+ | (O, S (S O)) = let pad = getPad {n=0} n in+ believe_me (prim__ashrB32 (prim__sextB8_32 (prim__shlB8 (believe_me x) pad))+ (prim__zextB8_32 pad))+ | (O, S (S (S _))) = let pad = getPad {n=0} n in+ believe_me (prim__ashrB64 (prim__sextB8_64 (prim__shlB8 (believe_me x) pad))+ (prim__zextB8_64 pad))+ | (S O, S O) = let pad = getPad {n=1} n in+ believe_me (prim__ashrB16 (prim__shlB16 (believe_me x) pad) pad)+ | (S O, S (S O)) = let pad = getPad {n=1} n in+ believe_me (prim__ashrB32 (prim__sextB16_32 (prim__shlB16 (believe_me x) pad))+ (prim__zextB16_32 pad))+ | (S O, S (S (S _))) = let pad = getPad {n=1} n in+ believe_me (prim__ashrB64 (prim__sextB16_64 (prim__shlB16 (believe_me x) pad))+ (prim__zextB16_64 pad))+ | (S (S O), S (S O)) = let pad = getPad {n=2} n in+ believe_me (prim__ashrB32 (prim__shlB32 (believe_me x) pad) pad)+ | (S (S O), S (S (S _))) = let pad = getPad {n=2} n in+ believe_me (prim__ashrB64 (prim__sextB32_64 (prim__shlB32 (believe_me x) pad))+ (prim__zextB32_64 pad))+ | (S (S (S _)), S (S (S _))) = let pad = getPad {n=3} n in+ believe_me (prim__ashrB64 (prim__shlB64 (believe_me x) pad) pad)++public+signExtend : Bits n -> Bits (n+m)+signExtend {m=m} (MkBits x) = MkBits (zeroUnused (sext' x))++-- TODO: Prove+trunc' : machineTy (nextBytes (n+m)) -> machineTy (nextBytes n)+trunc' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))+ | (O, O) = believe_me x+ | (O, S O) = believe_me (prim__truncB16_8 (believe_me x))+ | (O, S (S O)) = believe_me (prim__truncB32_8 (believe_me x))+ | (O, S (S (S _))) = believe_me (prim__truncB64_8 (believe_me x))+ | (S O, S O) = believe_me x+ | (S O, S (S O)) = believe_me (prim__truncB32_16 (believe_me x))+ | (S O, S (S (S _))) = believe_me (prim__truncB64_16 (believe_me x))+ | (S (S O), S (S O)) = believe_me x+ | (S (S O), S (S (S _))) = believe_me (prim__truncB64_32 (believe_me x))+ | (S (S (S _)), S (S (S _))) = believe_me x++public+truncate : Bits (n+m) -> Bits n+truncate (MkBits x) = MkBits (zeroUnused (trunc' x))++public+bitAt : Fin n -> Bits n+bitAt n = intToBits 1 `shiftLeft` intToBits (cast n)++public+getBit : Fin n -> Bits n -> Bool+getBit n x = (x `and` (bitAt n)) /= intToBits 0++public+setBit : Fin n -> Bits n -> Bits n+setBit n x = x `or` (bitAt n)++public+unsetBit : Fin n -> Bits n -> Bits n+unsetBit n x = x `and` complement (bitAt n)++bitsToStr : Bits n -> String+bitsToStr x = pack (helper last x)+ where+ %assert_total+ helper : Fin (S n) -> Bits n -> List Char+ helper fO _ = []+ helper (fS x) b = (if getBit x b then '1' else '0') :: helper (weaken x) b++instance Show (Bits n) where+ show = bitsToStr
+ lib/Data/Mod2.idr view
@@ -0,0 +1,64 @@+module Data.Mod2++import Data.Bits++%default total++-- Integers modulo 2^n+public+data Mod2 : Nat -> Type where+ MkMod2 : {n : Nat} -> Bits n -> Mod2 n++modBin : (Bits n -> Bits n -> Bits n) -> Mod2 n -> Mod2 n -> Mod2 n+modBin f (MkMod2 x) (MkMod2 y) = MkMod2 (f x y)++modComp : (Bits n -> Bits n -> a) -> Mod2 n -> Mod2 n -> a+modComp f (MkMod2 x) (MkMod2 y) = f x y++public partial+div : Mod2 n -> Mod2 n -> Mod2 n+div = modBin udiv++public partial+rem : Mod2 n -> Mod2 n -> Mod2 n+rem = modBin urem++%assert_total+public+intToMod : {n : Nat} -> Int -> Mod2 n+intToMod {n=n} x = MkMod2 (intToBits x)++instance Eq (Mod2 n) where+ (==) = modComp (==)++instance Ord (Mod2 n) where+ (<) = modComp (<)+ (<=) = modComp (<=)+ (>=) = modComp (>=)+ (>) = modComp (>)+ compare = modComp compare++instance Num (Mod2 n) where+ (+) = modBin plus+ (-) = modBin minus+ (*) = modBin times+ abs = id+ fromInteger = intToMod++instance Cast (Mod2 n) (Bits n) where+ cast (MkMod2 x) = x++instance Cast (Bits n) (Mod2 n) where+ cast x = MkMod2 x++modToStr : Mod2 n -> String+modToStr x = pack (reverse (helper x))+ where+ %assert_total+ helper : Mod2 n -> List Char+ helper x = strIndex "0123456789" (bitsToInt (cast (x `rem` 10)))+ :: (if x < 10 then [] else helper (x `div` 10))+++instance Show (Mod2 n) where+ show = modToStr
− lib/Data/Word.idr
@@ -1,19 +0,0 @@-module Data.Word--%access public--instance Num Word8 where- (+) = prim__addW8- (-) = prim__subW8- (*) = prim__mulW8-- abs x = x- fromInteger = prim__intToWord8--instance Num Word16 where- (+) = prim__addW16- (-) = prim__subW16- (*) = prim__mulW16-- abs x = x- fromInteger = prim__intToWord16
lib/Makefile view
@@ -11,6 +11,6 @@ $(IDRIS) --clean base.ipkg linecount: .PHONY- wc -l *.idr Network/*.idr Language/*.idr Prelude/*.idr Control/Monad/*.idr+ wc -l *.idr Network/*.idr Language/*.idr Prelude/*.idr Data/*.idr Control/Monad/*.idr Control/*.idr .PHONY:
lib/Prelude.idr view
@@ -52,14 +52,13 @@ instance Show a => Show (List a) where show xs = "[" ++ show' "" xs ++ "]" where - show' : String -> List a -> String show' acc [] = acc show' acc [x] = acc ++ show x show' acc (x :: xs) = show' (acc ++ show x ++ ", ") xs instance Show a => Show (Vect a n) where show xs = "[" ++ show' xs ++ "]" where - show' : Vect a m -> String+ show' : Vect a n -> String show' [] = "" show' [x] = show x show' (x :: xs) = show x ++ ", " ++ show' xs@@ -248,6 +247,9 @@ abstract data File = FHandle Ptr +partial stdin : File+stdin = FHandle prim__stdin+ do_fopen : String -> String -> IO Ptr do_fopen f m = mkForeign (FFun "fileOpen" [FString, FString] FPtr) f m @@ -328,7 +330,7 @@ c <- readFile' h "" closeFile h return c- where + where partial readFile' : File -> String -> IO String readFile' h contents =
lib/Prelude/Fin.idr view
@@ -8,11 +8,23 @@ fS : Fin k -> Fin (S k) instance Eq (Fin n) where- (==) = eq where- eq : Fin m -> Fin m -> Bool- eq fO fO = True- eq (fS k) (fS k') = eq k k'- eq _ _ = False+ (==) fO fO = True+ (==) (fS k) (fS k') = k == k'+ (==) _ _ = False++finToNat : Fin n -> Nat -> Nat+finToNat fO a = a+finToNat (fS x) a = finToNat x (S a)++instance Cast (Fin n) Nat where+ cast x = finToNat x O++finToInt : Fin n -> Int -> Int+finToInt fO a = a+finToInt (fS x) a = finToInt x (a + 1)++instance Cast (Fin n) Int where+ cast x = finToInt x 0 weaken : Fin n -> Fin (S n) weaken fO = fO
lib/Prelude/Heap.idr view
@@ -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 :: (toList (deleteMinimum heap p)) fromList : Ord a => List a -> MaxiphobicHeap a fromList = foldr insert empty
lib/Prelude/Nat.idr view
@@ -233,6 +233,12 @@ else S (div' left (centre - (S right)) right) +%assert_total+log2 : Nat -> Nat+log2 O = O+log2 (S O) = O+log2 n = S (log2 (n `div` 2))+ -------------------------------------------------------------------------------- -- Properties --------------------------------------------------------------------------------
lib/Prelude/Strings.idr view
@@ -25,8 +25,8 @@ %assert_total strM : (x : String) -> StrM x strM x with (choose (not (x == "")))- strM x | (Left p) = believe_me $ StrCons (strHead' x p) (strTail' x p)- strM x | (Right p) = believe_me StrNil+ strM x | (Left p) = really_believe_me $ StrCons (strHead' x p) (strTail' x p)+ strM x | (Right p) = really_believe_me StrNil -- annoyingly, we need these assert_totals because StrCons doesn't have -- a recursive argument, therefore the termination checker doesn't believe
lib/Prelude/Vect.idr view
@@ -129,10 +129,10 @@ or = foldr (||) False total any : (a -> Bool) -> Vect a m -> Bool-any p = or . map p+any p = Vect.or . map p total all : (a -> Bool) -> Vect a m -> Bool-all p = and . map p+all p = Vect.and . map p -------------------------------------------------------------------------------- -- Transformations
lib/base.ipkg view
@@ -15,7 +15,7 @@ Language.Reflection, - Data.Morphisms, Data.Bits, Data.Word,+ Data.Morphisms, Data.Bits, Data.Mod2, Control.Monad.Identity, Control.Monad.State, Control.Category, Control.Arrow
rts/Makefile view
@@ -1,7 +1,7 @@ include ../config.mk -OBJS = idris_rts.o idris_gc.o idris_gmp.o idris_stdfgn.o-HDRS = idris_rts.h idris_gc.h idris_gmp.h idris_stdfgn.h+OBJS = idris_rts.o idris_gc.o idris_gmp.o idris_stdfgn.o idris_bitstring.o+HDRS = idris_rts.h idris_gc.h idris_gmp.h idris_stdfgn.h idris_bitstring.h CFLAGS = -O2 -Wall ifneq ($(GMP_INCLUDE_DIR),) CFLAGS += -isystem $(GMP_INCLUDE_DIR)
+ rts/idris_bitstring.c view
@@ -0,0 +1,666 @@+#include "idris_rts.h"++VAL idris_b8CopyForGC(VM *vm, VAL a) {+ VAL cl = allocate(vm, sizeof(Closure), 1);+ SETTY(cl, BITS8);+ cl->info.bits8 = a->info.bits8;+ return cl;+}++VAL idris_b16CopyForGC(VM *vm, VAL a) {+ VAL cl = allocate(vm, sizeof(Closure), 1);+ SETTY(cl, BITS16);+ cl->info.bits16 = a->info.bits16;+ return cl;+}++VAL idris_b32CopyForGC(VM *vm, VAL a) {+ VAL cl = allocate(vm, sizeof(Closure), 1);+ SETTY(cl, BITS32);+ cl->info.bits32 = a->info.bits32;+ return cl;+}++VAL idris_b64CopyForGC(VM *vm, VAL a) {+ VAL cl = allocate(vm, sizeof(Closure), 1);+ SETTY(cl, BITS64);+ cl->info.bits64 = a->info.bits64;+ return cl;+}++VAL idris_b8(VM *vm, VAL a) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS8);+ cl->info.bits8 = (uint8_t) GETINT(a);+ return cl;+}++VAL idris_b16(VM *vm, VAL a) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS16);+ cl->info.bits16 = (uint16_t) GETINT(a);+ return cl;+}++VAL idris_b32(VM *vm, VAL a) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS32);+ cl->info.bits32 = (uint32_t) GETINT(a);+ return cl;+}++VAL idris_b64(VM *vm, VAL a) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS64);+ cl->info.bits64 = (uint64_t) GETINT(a);+ return cl;+}++VAL idris_castB32Int(VM *vm, VAL a) {+ return MKINT((i_int)a->info.bits32);+}++VAL idris_b8Plus(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS8);+ cl->info.bits8 = a->info.bits8 + b->info.bits8;+ return cl;+}++VAL idris_b8Minus(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS8);+ cl->info.bits8 = a->info.bits8 - b->info.bits8;+ return cl;+}++VAL idris_b8Times(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS8);+ cl->info.bits8 = a->info.bits8 * b->info.bits8;+ return cl;+}++VAL idris_b8UDiv(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS8);+ cl->info.bits8 = a->info.bits8 / b->info.bits8;+ return cl;+}++VAL idris_b8SDiv(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS8);+ cl->info.bits8 = (uint8_t) (((int8_t) a->info.bits8) / ((int8_t) b->info.bits8));+ return cl;+}++VAL idris_b8URem(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS8);+ cl->info.bits8 = a->info.bits8 % b->info.bits8;+ return cl;+}++VAL idris_b8SRem(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS8);+ cl->info.bits8 = (uint8_t) (((int8_t) a->info.bits8) % ((int8_t) b->info.bits8));+ return cl;+}++VAL idris_b8Lt(VM *vm, VAL a, VAL b) {+ return MKINT((i_int) (a->info.bits8 < b->info.bits8));+}++VAL idris_b8Gt(VM *vm, VAL a, VAL b) {+ return MKINT((i_int) (a->info.bits8 > b->info.bits8));+}++VAL idris_b8Eq(VM *vm, VAL a, VAL b) {+ return MKINT((i_int) (a->info.bits8 == b->info.bits8));+}++VAL idris_b8Lte(VM *vm, VAL a, VAL b) {+ return MKINT((i_int) (a->info.bits8 <= b->info.bits8));+}++VAL idris_b8Gte(VM *vm, VAL a, VAL b) {+ return MKINT((i_int) (a->info.bits8 >= b->info.bits8));+}++VAL idris_b8Compl(VM *vm, VAL a) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS8);+ cl->info.bits8 = ~ a->info.bits8;+ return cl;+}++VAL idris_b8And(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS8);+ cl->info.bits8 = a->info.bits8 & b->info.bits8;+ return cl;+}++VAL idris_b8Or(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS8);+ cl->info.bits8 = a->info.bits8 | b->info.bits8;+ return cl;+}++VAL idris_b8Xor(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS8);+ cl->info.bits8 = a->info.bits8 ^ b->info.bits8;+ return cl;+}++VAL idris_b8Shl(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS8);+ cl->info.bits8 = a->info.bits8 << b->info.bits8;+ return cl;+}++VAL idris_b8LShr(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS8);+ cl->info.bits8 = a->info.bits8 >> b->info.bits8;+ return cl;+}++VAL idris_b8AShr(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS8);+ cl->info.bits8 = (uint8_t) (((int8_t)a->info.bits8) >> ((int8_t)b->info.bits8));+ return cl;+}++VAL idris_b16Plus(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS16);+ cl->info.bits16 = a->info.bits16 + b->info.bits16;+ return cl;+}++VAL idris_b16Minus(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS16);+ cl->info.bits16 = a->info.bits16 - b->info.bits16;+ return cl;+}++VAL idris_b16Times(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS16);+ cl->info.bits16 = a->info.bits16 * b->info.bits16;+ return cl;+}++VAL idris_b16UDiv(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS16);+ cl->info.bits16 = a->info.bits16 / b->info.bits16;+ return cl;+}++VAL idris_b16SDiv(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS16);+ cl->info.bits16 =+ (uint16_t) (((int16_t) a->info.bits16) / ((int16_t) b->info.bits16));+ return cl;+}++VAL idris_b16URem(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS16);+ cl->info.bits16 = a->info.bits16 % b->info.bits16;+ return cl;+}++VAL idris_b16SRem(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS16);+ cl->info.bits16 =+ (uint16_t) (((int16_t) a->info.bits16) % ((int16_t) b->info.bits16));+ return cl;+}++VAL idris_b16Lt(VM *vm, VAL a, VAL b) {+ return MKINT((i_int) (a->info.bits16 < b->info.bits16));+}++VAL idris_b16Gt(VM *vm, VAL a, VAL b) {+ return MKINT((i_int) (a->info.bits16 > b->info.bits16));+}++VAL idris_b16Eq(VM *vm, VAL a, VAL b) {+ return MKINT((i_int) (a->info.bits16 == b->info.bits16));+}++VAL idris_b16Lte(VM *vm, VAL a, VAL b) {+ return MKINT((i_int) (a->info.bits16 <= b->info.bits16));+}++VAL idris_b16Gte(VM *vm, VAL a, VAL b) {+ return MKINT((i_int) (a->info.bits16 >= b->info.bits16));+}++VAL idris_b16Compl(VM *vm, VAL a) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS16);+ cl->info.bits16 = ~ a->info.bits16;+ return cl;+}++VAL idris_b16And(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS16);+ cl->info.bits16 = a->info.bits16 & b->info.bits16;+ return cl;+}++VAL idris_b16Or(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS16);+ cl->info.bits16 = a->info.bits16 | b->info.bits16;+ return cl;+}++VAL idris_b16Xor(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS16);+ cl->info.bits16 = a->info.bits16 ^ b->info.bits16;+ return cl;+}++VAL idris_b16Shl(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS16);+ cl->info.bits16 = a->info.bits16 << b->info.bits16;+ return cl;+}++VAL idris_b16LShr(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS16);+ cl->info.bits16 = a->info.bits16 >> b->info.bits16;+ return cl;+}++VAL idris_b16AShr(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS16);+ cl->info.bits16 = (uint16_t) (((int16_t)a->info.bits16) >> ((int16_t)b->info.bits16));+ return cl;+}++VAL idris_b32Plus(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS32);+ cl->info.bits32 = a->info.bits32 + b->info.bits32;+ return cl;+}++VAL idris_b32Minus(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS32);+ cl->info.bits32 = a->info.bits32 - b->info.bits32;+ return cl;+}++VAL idris_b32Times(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS32);+ cl->info.bits32 = a->info.bits32 * b->info.bits32;+ return cl;+}++VAL idris_b32UDiv(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS32);+ cl->info.bits32 = a->info.bits32 / b->info.bits32;+ return cl;+}++VAL idris_b32SDiv(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS32);+ cl->info.bits32 =+ (uint32_t) (((int32_t) a->info.bits32) / ((int32_t) b->info.bits32));+ return cl;+}++VAL idris_b32URem(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS32);+ cl->info.bits32 = a->info.bits32 % b->info.bits32;+ return cl;+}++VAL idris_b32SRem(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS32);+ cl->info.bits32 =+ (uint32_t) (((int32_t) a->info.bits32) % ((int32_t) b->info.bits32));+ return cl;+}++VAL idris_b32Lt(VM *vm, VAL a, VAL b) {+ return MKINT((i_int) (a->info.bits32 < b->info.bits32));+}++VAL idris_b32Gt(VM *vm, VAL a, VAL b) {+ return MKINT((i_int) (a->info.bits32 > b->info.bits32));+}++VAL idris_b32Eq(VM *vm, VAL a, VAL b) {+ return MKINT((i_int) (a->info.bits32 == b->info.bits32));+}++VAL idris_b32Lte(VM *vm, VAL a, VAL b) {+ return MKINT((i_int) (a->info.bits32 <= b->info.bits32));+}++VAL idris_b32Gte(VM *vm, VAL a, VAL b) {+ return MKINT((i_int) (a->info.bits32 >= b->info.bits32));+}++VAL idris_b32Compl(VM *vm, VAL a) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS32);+ cl->info.bits32 = ~ a->info.bits32;+ return cl;+}++VAL idris_b32And(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS32);+ cl->info.bits32 = a->info.bits32 & b->info.bits32;+ return cl;+}++VAL idris_b32Or(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS32);+ cl->info.bits32 = a->info.bits32 | b->info.bits32;+ return cl;+}++VAL idris_b32Xor(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS32);+ cl->info.bits32 = a->info.bits32 ^ b->info.bits32;+ return cl;+}++VAL idris_b32Shl(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS32);+ cl->info.bits32 = a->info.bits32 << b->info.bits32;+ return cl;+}++VAL idris_b32LShr(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS32);+ cl->info.bits32 = a->info.bits32 >> b->info.bits32;+ return cl;+}++VAL idris_b32AShr(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS32);+ cl->info.bits32 = (uint32_t) (((int32_t)a->info.bits32) >> ((int32_t)b->info.bits32));+ return cl;+}++VAL idris_b64Plus(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS64);+ cl->info.bits64 = a->info.bits64 + b->info.bits64;+ return cl;+}++VAL idris_b64Minus(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS64);+ cl->info.bits64 = a->info.bits64 - b->info.bits64;+ return cl;+}++VAL idris_b64Times(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS64);+ cl->info.bits64 = a->info.bits64 * b->info.bits64;+ return cl;+}++VAL idris_b64UDiv(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS64);+ cl->info.bits64 = a->info.bits64 / b->info.bits64;+ return cl;+}++VAL idris_b64SDiv(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS64);+ cl->info.bits64 =+ (uint64_t) (((int64_t) a->info.bits64) / ((int64_t) b->info.bits64));+ return cl;+}++VAL idris_b64URem(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS64);+ cl->info.bits64 = a->info.bits64 % b->info.bits64;+ return cl;+}++VAL idris_b64SRem(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS64);+ cl->info.bits64 =+ (uint64_t) (((int64_t) a->info.bits64) % ((int64_t) b->info.bits64));+ return cl;+}++VAL idris_b64Lt(VM *vm, VAL a, VAL b) {+ return MKINT((i_int) (a->info.bits64 < b->info.bits64));+}++VAL idris_b64Gt(VM *vm, VAL a, VAL b) {+ return MKINT((i_int) (a->info.bits64 > b->info.bits64));+}++VAL idris_b64Eq(VM *vm, VAL a, VAL b) {+ return MKINT((i_int) (a->info.bits64 == b->info.bits64));+}++VAL idris_b64Lte(VM *vm, VAL a, VAL b) {+ return MKINT((i_int) (a->info.bits64 <= b->info.bits64));+}++VAL idris_b64Gte(VM *vm, VAL a, VAL b) {+ return MKINT((i_int) (a->info.bits64 >= b->info.bits64));+}++VAL idris_b64Compl(VM *vm, VAL a) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS64);+ cl->info.bits64 = ~ a->info.bits64;+ return cl;+}++VAL idris_b64And(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS64);+ cl->info.bits64 = a->info.bits64 & b->info.bits64;+ return cl;+}++VAL idris_b64Or(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS64);+ cl->info.bits64 = a->info.bits64 | b->info.bits64;+ return cl;+}++VAL idris_b64Xor(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS64);+ cl->info.bits64 = a->info.bits64 ^ b->info.bits64;+ return cl;+}++VAL idris_b64Shl(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS64);+ cl->info.bits64 = a->info.bits64 << b->info.bits64;+ return cl;+}++VAL idris_b64LShr(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS64);+ cl->info.bits64 = a->info.bits64 >> b->info.bits64;+ return cl;+}++VAL idris_b64AShr(VM *vm, VAL a, VAL b) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS64);+ cl->info.bits64 = (uint64_t) (((int64_t)a->info.bits64) >> ((int64_t)b->info.bits64));+ return cl;+}++VAL idris_b8Z16(VM *vm, VAL a) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS16);+ cl->info.bits16 = (uint16_t) a->info.bits8;+ return cl;+}++VAL idris_b8Z32(VM *vm, VAL a) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS32);+ cl->info.bits32 = (uint32_t) a->info.bits8;+ return cl;+}++VAL idris_b8Z64(VM *vm, VAL a) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS16);+ cl->info.bits64 = (uint64_t) a->info.bits8;+ return cl;+}++VAL idris_b8S16(VM *vm, VAL a) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS16);+ cl->info.bits16 = (uint16_t) (int16_t) (int8_t) a->info.bits8;+ return cl;+}++VAL idris_b8S32(VM *vm, VAL a) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS32);+ cl->info.bits32 = (uint32_t) (int32_t) (int8_t) a->info.bits8;+ return cl;+}++VAL idris_b8S64(VM *vm, VAL a) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS64);+ cl->info.bits64 = (uint64_t) (int64_t) (int8_t) a->info.bits8;+ return cl;+}++VAL idris_b16Z32(VM *vm, VAL a) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS32);+ cl->info.bits32 = (uint32_t) a->info.bits16;+ return cl;+}++VAL idris_b16Z64(VM *vm, VAL a) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS64);+ cl->info.bits64 = (uint64_t) a->info.bits16;+ return cl;+}++VAL idris_b16S32(VM *vm, VAL a) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS32);+ cl->info.bits32 = (uint32_t) (int32_t) (int16_t) a->info.bits16;+ return cl;+}++VAL idris_b16S64(VM *vm, VAL a) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS64);+ cl->info.bits64 = (uint64_t) (int64_t) (int16_t) a->info.bits16;+ return cl;+}++VAL idris_b16T8(VM *vm, VAL a) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS8);+ cl->info.bits8 = (uint8_t) a->info.bits16;+ return cl;+}++VAL idris_b32Z64(VM *vm, VAL a) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS64);+ cl->info.bits64 = (uint64_t) a->info.bits32;+ return cl;+}++VAL idris_b32S64(VM *vm, VAL a) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS64);+ cl->info.bits64 = (uint64_t) (int64_t) (int32_t) a->info.bits32;+ return cl;+}++VAL idris_b32T8(VM *vm, VAL a) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS8);+ cl->info.bits8 = (uint8_t) a->info.bits32;+ return cl;+}++VAL idris_b32T16(VM *vm, VAL a) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS16);+ cl->info.bits16 = (uint16_t) a->info.bits32;+ return cl;+}++VAL idris_b64T8(VM *vm, VAL a) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS8);+ cl->info.bits8 = (uint8_t) a->info.bits64;+ return cl;+}++VAL idris_b64T16(VM *vm, VAL a) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS16);+ cl->info.bits16 = (uint16_t) a->info.bits64;+ return cl;+}++VAL idris_b64T32(VM *vm, VAL a) {+ VAL cl = allocate(vm, sizeof(Closure), 0);+ SETTY(cl, BITS32);+ cl->info.bits32 = (uint32_t) a->info.bits64;+ return cl;+}+
+ rts/idris_bitstring.h view
@@ -0,0 +1,125 @@+#ifndef _IDRISBITSTRING_H+#define _IDRISBITSTRING_H++VAL idris_b8CopyForGC(VM *vm, VAL a);+VAL idris_b16CopyForGC(VM *vm, VAL a);+VAL idris_b32CopyForGC(VM *vm, VAL a);+VAL idris_b64CopyForGC(VM *vm, VAL a);++VAL idris_b8(VM *vm, VAL a);+VAL idris_b16(VM *vm, VAL a);+VAL idris_b32(VM *vm, VAL a);+VAL idris_b64(VM *vm, VAL a);+VAL idris_castB32Int(VM *vm, VAL a);++VAL idris_b8Plus(VM *vm, VAL a, VAL b);+VAL idris_b8Minus(VM *vm, VAL a, VAL b);+VAL idris_b8Times(VM *vm, VAL a, VAL b);+VAL idris_b8UDiv(VM *vm, VAL a, VAL b);+VAL idris_b8SDiv(VM *vm, VAL a, VAL b);+VAL idris_b8URem(VM *vm, VAL a, VAL b);+VAL idris_b8SRem(VM *vm, VAL a, VAL b);+VAL idris_b8Lt(VM *vm, VAL a, VAL b);+VAL idris_b8Gt(VM *vm, VAL a, VAL b);+VAL idris_b8Eq(VM *vm, VAL a, VAL b);+VAL idris_b8Lte(VM *vm, VAL a, VAL b);+VAL idris_b8Gte(VM *vm, VAL a, VAL b);+VAL idris_b8Compl(VM *vm, VAL a);+VAL idris_b8And(VM *vm, VAL a, VAL b);+VAL idris_b8Or(VM *vm, VAL a, VAL b);+VAL idris_b8Neg(VM *vm, VAL a);+VAL idris_b8XOr(VM *vm, VAL a, VAL b);+VAL idris_b8Shl(VM *vm, VAL a, VAL b);+VAL idris_b8LShr(VM *vm, VAL a, VAL b);+VAL idris_b8AShr(VM *vm, VAL a, VAL b);++VAL idris_b16Eq(VM *vm, VAL a, VAL b);+VAL idris_b32Eq(VM *vm, VAL a, VAL b);+VAL idris_b64Eq(VM *vm, VAL a, VAL b);++VAL idris_b8Z16(VM *vm, VAL a);+VAL idris_b8Z32(VM *vm, VAL a);+VAL idris_b8Z64(VM *vm, VAL a);+VAL idris_b8S16(VM *vm, VAL a);+VAL idris_b8S32(VM *vm, VAL a);+VAL idris_b8S64(VM *vm, VAL a);++VAL idris_b16Plus(VM *vm, VAL a, VAL b);+VAL idris_b16Minus(VM *vm, VAL a, VAL b);+VAL idris_b16Times(VM *vm, VAL a, VAL b);+VAL idris_b16UDiv(VM *vm, VAL a, VAL b);+VAL idris_b16SDiv(VM *vm, VAL a, VAL b);+VAL idris_b16URem(VM *vm, VAL a, VAL b);+VAL idris_b16SRem(VM *vm, VAL a, VAL b);+VAL idris_b16Lt(VM *vm, VAL a, VAL b);+VAL idris_b16Gt(VM *vm, VAL a, VAL b);+VAL idris_b16Eq(VM *vm, VAL a, VAL b);+VAL idris_b16Lte(VM *vm, VAL a, VAL b);+VAL idris_b16Gte(VM *vm, VAL a, VAL b);+VAL idris_b16Compl(VM *vm, VAL a);+VAL idris_b16And(VM *vm, VAL a, VAL b);+VAL idris_b16Or(VM *vm, VAL a, VAL b);+VAL idris_b16Neg(VM *vm, VAL a);+VAL idris_b16XOr(VM *vm, VAL a, VAL b);+VAL idris_b16Shl(VM *vm, VAL a, VAL b);+VAL idris_b16LShr(VM *vm, VAL a, VAL b);+VAL idris_b16AShr(VM *vm, VAL a, VAL b);++VAL idris_b16Z32(VM *vm, VAL a);+VAL idris_b16Z64(VM *vm, VAL a);+VAL idris_b16S32(VM *vm, VAL a);+VAL idris_b16S64(VM *vm, VAL a);+VAL idris_b16T8(VM *vm, VAL a);++VAL idris_b32Plus(VM *vm, VAL a, VAL b);+VAL idris_b32Minus(VM *vm, VAL a, VAL b);+VAL idris_b32Times(VM *vm, VAL a, VAL b);+VAL idris_b32UDiv(VM *vm, VAL a, VAL b);+VAL idris_b32SDiv(VM *vm, VAL a, VAL b);+VAL idris_b32URem(VM *vm, VAL a, VAL b);+VAL idris_b32SRem(VM *vm, VAL a, VAL b);+VAL idris_b32Lt(VM *vm, VAL a, VAL b);+VAL idris_b32Gt(VM *vm, VAL a, VAL b);+VAL idris_b32Eq(VM *vm, VAL a, VAL b);+VAL idris_b32Lte(VM *vm, VAL a, VAL b);+VAL idris_b32Gte(VM *vm, VAL a, VAL b);+VAL idris_b32Compl(VM *vm, VAL a);+VAL idris_b32And(VM *vm, VAL a, VAL b);+VAL idris_b32Or(VM *vm, VAL a, VAL b);+VAL idris_b32Neg(VM *vm, VAL a);+VAL idris_b32XOr(VM *vm, VAL a, VAL b);+VAL idris_b32Shl(VM *vm, VAL a, VAL b);+VAL idris_b32LShr(VM *vm, VAL a, VAL b);+VAL idris_b32AShr(VM *vm, VAL a, VAL b);++VAL idris_b32Z64(VM *vm, VAL a);+VAL idris_b32S64(VM *vm, VAL a);+VAL idris_b32T8(VM *vm, VAL a);+VAL idris_b32T16(VM *vm, VAL a);++VAL idris_b64Plus(VM *vm, VAL a, VAL b);+VAL idris_b64Minus(VM *vm, VAL a, VAL b);+VAL idris_b64Times(VM *vm, VAL a, VAL b);+VAL idris_b64UDiv(VM *vm, VAL a, VAL b);+VAL idris_b64SDiv(VM *vm, VAL a, VAL b);+VAL idris_b64URem(VM *vm, VAL a, VAL b);+VAL idris_b64SRem(VM *vm, VAL a, VAL b);+VAL idris_b64Lt(VM *vm, VAL a, VAL b);+VAL idris_b64Gt(VM *vm, VAL a, VAL b);+VAL idris_b64Eq(VM *vm, VAL a, VAL b);+VAL idris_b64Lte(VM *vm, VAL a, VAL b);+VAL idris_b64Gte(VM *vm, VAL a, VAL b);+VAL idris_b64Compl(VM *vm, VAL a);+VAL idris_b64And(VM *vm, VAL a, VAL b);+VAL idris_b64Or(VM *vm, VAL a, VAL b);+VAL idris_b64Neg(VM *vm, VAL a);+VAL idris_b64XOr(VM *vm, VAL a, VAL b);+VAL idris_b64Shl(VM *vm, VAL a, VAL b);+VAL idris_b64LShr(VM *vm, VAL a, VAL b);+VAL idris_b64AShr(VM *vm, VAL a, VAL b);++VAL idris_b64T8(VM *vm, VAL a);+VAL idris_b64T16(VM *vm, VAL a);+VAL idris_b64T32(VM *vm, VAL a);++#endif
rts/idris_gc.c view
@@ -1,5 +1,6 @@ #include "idris_rts.h" #include "idris_gc.h"+#include "idris_bitstring.h" #include <assert.h> VAL copy(VM* vm, VAL x) {@@ -28,6 +29,18 @@ break; case PTR: cl = MKPTRc(vm, x->info.ptr);+ break;+ case BITS8:+ cl = idris_b8CopyForGC(vm, x);+ break;+ case BITS16:+ cl = idris_b16CopyForGC(vm, x);+ break;+ case BITS32:+ cl = idris_b32CopyForGC(vm, x);+ break;+ case BITS64:+ cl = idris_b64CopyForGC(vm, x); break; case FWD: return x->info.ptr;
rts/idris_rts.c view
@@ -8,6 +8,7 @@ #include "idris_rts.h" #include "idris_gc.h"+#include "idris_bitstring.h" VM* init_vm(int stack_size, size_t heap_size, int max_threads, // not implemented yet@@ -443,6 +444,18 @@ break; case PTR: cl = MKPTRc(vm, x->info.ptr);+ break;+ case BITS8:+ cl = idris_b8CopyForGC(vm, x);+ break;+ case BITS16:+ cl = idris_b16CopyForGC(vm, x);+ break;+ case BITS32:+ cl = idris_b32CopyForGC(vm, x);+ break;+ case BITS64:+ cl = idris_b64CopyForGC(vm, x); break; default: assert(0); // We're in trouble if this happens...
rts/idris_rts.h view
@@ -7,11 +7,12 @@ #include <unistd.h> #include <stdarg.h> #include <pthread.h>+#include <stdint.h> // Closures typedef enum {- CON, INT, BIGINT, FLOAT, STRING, UNIT, PTR, FWD+ CON, INT, BIGINT, FLOAT, STRING, BITS8, BITS16, BITS32, BITS64, UNIT, PTR, FWD } ClosureType; typedef struct Closure *VAL;@@ -31,6 +32,10 @@ double f; char* str; void* ptr;+ uint8_t bits8;+ uint16_t bits16;+ uint32_t bits32;+ uint64_t bits64; } info; } Closure;
rts/libidris_rts.a view
binary file changed (27896 → 50408 bytes)
src/Core/CaseTree.hs view
@@ -79,7 +79,7 @@ small :: Name -> [Name] -> SC -> Bool small n args t = let as = findAllUsedArgs t args in length as == length (nub as) && - termsize n t < 20 + termsize n t < 5 namesUsed :: SC -> [Name] namesUsed sc = nub $ nu' [] sc where@@ -226,9 +226,11 @@ toPat' (Constant ChType) [] | tc = return $ PCon (UN "Char") 3 [] toPat' (Constant StrType) [] | tc = return $ PCon (UN "String") 4 [] toPat' (Constant PtrType) [] | tc = return $ PCon (UN "Ptr") 5 [] - toPat' (Constant BIType) [] | tc = return $ PCon (UN "Integer") 6 [] - toPat' (Constant W8Type) [] | tc = return $ PCon (UN "Word8") 7 []- toPat' (Constant W16Type) [] | tc = return $ PCon (UN "Word16") 8 []+ toPat' (Constant BIType) [] | tc = return $ PCon (UN "Integer") 6 []+ toPat' (Constant B8Type) [] | tc = return $ PCon (UN "Bits8") 7 []+ toPat' (Constant B16Type) [] | tc = return $ PCon (UN "Bits16") 8 []+ toPat' (Constant B32Type) [] | tc = return $ PCon (UN "Bits32") 9 []+ toPat' (Constant B64Type) [] | tc = return $ PCon (UN "Bits64") 10 [] toPat' (P Bound n _) [] = do ns <- get if n `elem` ns
src/Core/Constraints.hs view
@@ -52,6 +52,10 @@ = Error $ At fc UniverseError -- FIXME: Make informative -- e.g. (Msg ("Cycle: " ++ show cv ++ ", " ++ show path))+ -- if we reach a cycle but we're at the same universe level, it's+ -- fine, because they must all be equal, so stop.+ | inc == 0 && cv `elem` map fst path+ = return () | otherwise = case M.lookup cv r of Nothing -> return () Just cs -> mapM_ (next ((cv, fc):path) inc) cs
src/Core/CoreParser.hs view
@@ -36,7 +36,7 @@ "using", "namespace", "class", "instance", "public", "private", "abstract", "Int", "Integer", "Float", "Char", "String", "Ptr",- "Word8", "Word16"]+ "Bits8", "Bits16", "Bits32", "Bits64"] } iOpStart = oneOf ":!#$%&*+./<=>?@\\^|-~"
src/Core/Elaborate.hs view
@@ -15,6 +15,7 @@ import Core.TT import Core.Evaluate import Core.Typecheck+import Core.Unify import Control.Monad.State import Data.Char@@ -118,6 +119,10 @@ get_holes = do ES p _ _ <- get return (holes (fst p)) +get_probs :: Elab' aux Fails+get_probs = do ES p _ _ <- get+ return (problems (fst p))+ -- get the current goal type goal :: Elab' aux Type goal = do ES p _ _ <- get@@ -150,10 +155,6 @@ get_deferred = do ES p _ _ <- get return (deferred (fst p)) -get_inj :: Elab' aux [(Term, Term, Term)]-get_inj = do ES p _ _ <- get- return (injective (fst p))- checkInjective :: (Term, Term, Term) -> Elab' aux () checkInjective (tm, l, r) = do ctxt <- get_context if isInj ctxt tm then return ()@@ -296,6 +297,9 @@ instanceArg :: Name -> Elab' aux () instanceArg n = processTactic' (Instance n) +setinj :: Name -> Elab' aux ()+setinj n = processTactic' (SetInjective n)+ proofstate :: Elab' aux () proofstate = processTactic' ProofState @@ -375,12 +379,14 @@ if null imps then [] -- do all we can else map fst (filter (not.snd) (zip args (map fst imps)))- let (n, hs) = -- trace ("AVOID UNIFY: " ++ show (fn, dont) ++ "\n" ++ show ptm) $ + let (n, hunis) = -- trace ("AVOID UNIFY: " ++ show (fn, dont) ++ "\n" ++ show ptm) $ unified p let unify = -- trace ("Not done " ++ show hs) $ - dropGiven dont hs+ dropGiven dont hunis hs put (ES (p { dontunify = dont, unified = (n, unify) }, a) s prev) ptm <- get_term+ g <- goal+-- trace ("Goal " ++ show g ++ "\n" ++ show (fn, imps, unify) ++ "\n" ++ show ptm) $ end_unify ptm <- get_term return (map (updateUnify unify) args)@@ -461,15 +467,20 @@ claim a RType claim b RType claim f (RBind (MN 0 "aX") (Pi (Var a)) (Var b))+ tm <- get_term start_unify s claim s (Var a) prep_fill f [s] -- try elaborating in both orders, since we might learn something useful -- either way- try (do focus s; arg- focus f; fun)- (do focus f; fun- focus s; arg)+-- try (do focus s; arg+-- focus f; fun)+-- (do focus f; fun+-- focus s; arg)+ focus f; fun+ focus s; arg+ tm <- get_term+ ps <- get_probs complete_fill hs <- get_holes -- We don't need a and b in the hole queue any more since they were just for@@ -493,7 +504,8 @@ try' :: Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a try' t1 t2 proofSearch = do s <- get- case runStateT t1 s of+ ps <- get_probs+ case prunStateT ps t1 s of OK (v, s') -> do put s' return v Error e1 -> if proofSearch || recoverableErr e1 then@@ -525,18 +537,30 @@ tryAll' [res] _ [] = res tryAll' (_:_) _ [] = cantResolve tryAll' [] (f, _) [] = f- tryAll' cs f (x:xs) = do s <- get- case runStateT x s of- OK (v, s') -> tryAll' ((do put s'- return v):cs) f xs- Error err -> do put s- if (score err) < 100- then- tryAll' cs (better err f) xs- else- tryAll' [] (better err f) xs -- give up+ tryAll' cs f (x:xs) + = do s <- get+ ps <- get_probs+ case prunStateT ps x s of+ OK (v, s') -> tryAll' ((do put s'+ return v):cs) f xs+ Error err -> do put s+ if (score err) < 100+ then tryAll' cs (better err f) xs+ else tryAll' [] (better err f) xs -- give up + better err (f, i) = let s = score err in if (s >= i) then (lift (tfail err), s) else (f, i) +prunStateT ps x s + = case runStateT x s of+ OK (v, s'@(ES (p, _) _ _)) -> + if (length (problems p) > length ps)+ then case reverse (problems p) of+ ((_,_,_,e):_) -> Error e+ else OK (v, s')+ Error e -> Error e++dumpprobs [] = ""+dumpprobs ((_,_,_,e):es) = show e ++ "\n" ++ dumpprobs es
src/Core/Evaluate.hs view
@@ -224,7 +224,7 @@ do let val = lookupDefAcc Nothing n atRepl ctxt case val of [(CaseOp inl inr _ _ _ ns tree _ _, acc)]- | acc == Public || simpl -> -- unoptimised version+ | acc == Public -> -- unoptimised version if canSimplify inl inr n stk then return $ unload env (VP Ref n ty) args else do c <- evCase ntimes (n:stk) top env ns args tree@@ -507,8 +507,11 @@ findConst ChType (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 W8Type (ConCase n 6 [] v : xs) = Just v- findConst W16Type (ConCase n 7 [] v : xs) = Just v+ findConst BIType (ConCase n 6 [] v : xs) = Just v+ findConst B8Type (ConCase n 7 [] v : xs) = Just v+ findConst B16Type (ConCase n 8 [] v : xs) = Just v+ findConst B32Type (ConCase n 9 [] v : xs) = Just v+ findConst B64Type (ConCase n 10 [] v : xs) = Just v findConst c (_ : xs) = findConst c xs getValArgs (HApp t env args) = (t, env, args)
src/Core/ProofShell.hs view
@@ -11,6 +11,8 @@ import Control.Monad.State import System.Console.Haskeline +import Idris.AbsSyntaxTree (Idris)+ import Util.Pretty data ShellState = ShellState @@ -55,21 +57,23 @@ err -> (state, show err) | otherwise = (state, "No proof in progress") -runShell :: ShellState -> InputT IO ShellState-runShell st = do (prompt, parser) <- - maybe (return ("TT# ", parseCommand)) - (\st -> do outputStrLn . render . pretty $ st- return (show (thname st) ++ "# ", parseTactic)) - (prf st)- x <- getInputLine prompt- cmd <- case x of- Nothing -> return $ Right Quit- Just input -> return (parser input)- case cmd of- Left err -> do outputStrLn (show err)- runShell st- Right cmd -> do let (st', r) = processCommand cmd st- outputStrLn r- if (not (exitNow st')) then runShell st'- else return st'+runShell :: ShellState -> Idris ShellState+runShell st = runInputT defaultSettings $ runShell' st+ where+ runShell' st = do (prompt, parser) <- + maybe (return ("TT# ", parseCommand)) + (\st -> do outputStrLn . render . pretty $ st+ return (show (thname st) ++ "# ", parseTactic)) + (prf st)+ x <- getInputLine prompt+ cmd <- case x of+ Nothing -> return $ Right Quit+ Just input -> return (parser input)+ case cmd of+ Left err -> do outputStrLn (show err)+ runShell' st+ Right cmd -> do let (st', r) = processCommand cmd st+ outputStrLn r+ if (not (exitNow st')) then runShell' st'+ else return st'
src/Core/ProofState.hs view
@@ -29,7 +29,7 @@ unified :: (Name, [(Name, Term)]), solved :: Maybe (Name, Term), problems :: Fails,- injective :: [(Term, Term, Term)],+ injective :: [Name], deferred :: [Name], -- names we'll need to define instances :: [Name], -- instance arguments (for type classes) previous :: Maybe ProofState, -- for undo@@ -68,6 +68,7 @@ | Defer Name | DeferType Name Raw [Name] | Instance Name+ | SetInjective Name | MoveLast Name | ProofState | Undo@@ -148,15 +149,28 @@ holeName i = MN i "hole" +qshow :: Fails -> String+qshow fs = show (map (\ (x, y, _, _) -> (x, y)) fs) + unify' :: Context -> Env -> TT Name -> TT Name -> StateT TState TC [(Name, TT Name)]-unify' ctxt env topx topy = do (u, inj, fails) <- lift $ unify ctxt env topx topy- addInj inj- case fails of- [] -> return u- err -> - do ps <- get- put (ps { problems = err ++ problems ps })- return []+unify' ctxt env topx topy = + do ps <- get+ (u, fails) <- lift $ unify ctxt env topx topy (injective ps) (holes ps)+-- trace ("Unified " ++ show (topx, topy) ++ show (injective ps) ++ +-- " " ++ show u ++ "\n" ++ qshow fails ++ "\nCurrent problems:\n"+-- ++ qshow (problems ps) ++ "\n" ++ show (holes ps)) $+ case fails of+-- [] -> return u+ err -> + do ps <- get+ let (h, ns) = unified ps+ let (ns', probs') = updateProblems (context ps) (u ++ ns) + (err ++ problems ps)+ (injective ps)+ (holes ps)+ put (ps { problems = probs',+ unified = (h, ns') })+ return u getName :: Monad m => String -> StateT TState m Name getName tag = do ps <- get@@ -194,6 +208,7 @@ goalAtFocus ps | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps) return (goalType g)+ | otherwise = error $ "No goal in " ++ show (holes ps) ++ show (pterm ps) goal :: Hole -> Term -> TC Goal goal h tm = g [] tm where@@ -288,6 +303,12 @@ instances = x:is }) return (Bind x (Hole t) sc) +setinj :: Name -> RunTactic+setinj n ctxt env (Bind x (Hole t) sc)+ = do action (\ps -> let is = injective ps in+ ps { injective = n : is })+ return (Bind x (Hole t) sc)+ defer :: Name -> RunTactic defer n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' = do action (\ps -> let hs = holes ps in@@ -322,10 +343,6 @@ return sc regret ctxt env (Bind x (Hole t) _) = fail $ show x ++ " : " ++ show t ++ " is not solved" -addInj :: [(Term, Term, Term)] -> StateT TState TC ()-addInj inj = do ps <- get- put (ps { injective = inj ++ injective ps })- exact :: Raw -> RunTactic exact guess ctxt env (Bind x (Hole ty) sc) = do (val, valty) <- lift $ check ctxt env guess @@ -344,7 +361,7 @@ ns <- unify' ctxt env valty ty ps <- get let (uh, uns) = unified ps- put (ps { unified = (uh, uns ++ ns) })+-- put (ps { unified = (uh, uns ++ ns) }) -- addLog (show (uh, uns ++ ns)) return $ Bind x (Guess ty val) sc fill _ _ _ _ = fail "Can't fill here."@@ -362,22 +379,25 @@ ns <- unify' ctxt env valty ty ps <- get let (uh, uns) = unified ps- put (ps { unified = (uh, uns ++ ns) })+-- put (ps { unified = (uh, uns ++ ns) }) return $ Bind x (Guess ty val) sc complete_fill ctxt env t = fail $ "Can't complete fill at " ++ show t solve :: RunTactic solve ctxt env (Bind x (Guess ty val) sc)- | pureTerm val = do ps <- get+ | True = do ps <- get let (uh, uns) = unified ps action (\ps -> ps { holes = holes ps \\ [x], solved = Just (x, val),+-- problems = solveInProblems +-- x val (problems ps), -- dontunify = dontunify ps \\ [x], -- unified = (uh, uns ++ [(x, val)]), instances = instances ps \\ [x] }) return $ {- Bind x (Let ty val) sc -} instantiate val (pToV x sc)- | otherwise = lift $ tfail $ IncompleteTerm val+ | otherwise = do ps <- get+ lift $ tfail $ IncompleteTerm val solve _ _ h = do ps <- get fail $ "Not a guess " ++ show h ++ "\n" ++ show (holes ps, pterm ps) @@ -396,7 +416,7 @@ do ns <- unify' ctxt env s tyv ps <- get let (uh, uns) = unified ps- put (ps { unified = (uh, uns ++ ns) })+-- put (ps { unified = (uh, uns ++ ns) }) return $ Bind n (Lam tyv) (Bind x (Hole t') (P Bound x t')) _ -> fail "Nothing to introduce" introTy ty n ctxt env _ = fail "Can't introduce here."@@ -494,7 +514,8 @@ do let ty' = hnf ctxt env ty in -- trace ("HNF " ++ show (ty, ty')) $ return $ Bind x (Hole ty') sc- +hnf_compute ctxt env t = return t+ check_in :: Raw -> RunTactic check_in t ctxt env tm = do (val, valty) <- lift $ check ctxt env t@@ -515,7 +536,7 @@ return tm start_unify :: Name -> RunTactic-start_unify n ctxt env tm = do action (\ps -> ps { unified = (n, []) })+start_unify n ctxt env tm = do -- action (\ps -> ps { unified = (n, []) }) return tm tmap f (a, b, c) = (f a, b, c)@@ -524,22 +545,24 @@ solve_unified ctxt env tm = do ps <- get let (_, ns) = unified ps- let unify = dropGiven (dontunify ps) ns+ let unify = dropGiven (dontunify ps) ns (holes ps) action (\ps -> ps { holes = holes ps \\ map fst unify }) action (\ps -> ps { pterm = updateSolved unify (pterm ps) })- action (\ps -> ps { injective = map (tmap (updateSolved unify)) (injective ps) }) return (updateSolved unify tm) where -dropGiven du [] = []-dropGiven du ((n, P Bound t ty) : us) | n `elem` du && not (t `elem` du)- = (t, P Bound n ty) : dropGiven du us-dropGiven du (u@(n, _) : us) | n `elem` du = dropGiven du us+dropGiven du [] hs = []+dropGiven du ((n, P Bound t ty) : us) hs+ | n `elem` du && not (t `elem` du)+ && n `elem` hs && t `elem` hs+ = (t, P Bound n ty) : dropGiven du us hs+dropGiven du (u@(n, _) : us) hs + | n `elem` du = dropGiven du us hs -- dropGiven du (u@(_, P a n ty) : us) | n `elem` du = dropGiven du us-dropGiven du (u : us) = u : dropGiven du us+dropGiven du (u : us) hs = u : dropGiven du us hs updateSolved xs x = -- trace ("Updating " ++ show xs ++ " in " ++ show x) $ - updateSolved' xs x+ updateSolved' xs x updateSolved' xs (Bind n (Hole ty) t) | Just v <- lookup n xs = instantiate v (pToV n (updateSolved' xs t)) updateSolved' xs (Bind n b t) @@ -549,11 +572,30 @@ | Just v <- lookup n xs = v updateSolved' xs t = t -updateProblems ns [] = []-updateProblems ns ((x, y, env, err) : ps) =+updateEnv ns [] = []+updateEnv ns ((n, b) : env) = (n, fmap (updateSolved ns) b) : updateEnv ns env++updateError ns (CantUnify b l r e xs sc)+ = CantUnify b (updateSolved ns l) (updateSolved ns r) (updateError ns e) xs sc+updateError ns e = e++solveInProblems x val [] = []+solveInProblems x val ((l, r, env, err) : ps)+ = ((instantiate val (pToV x l), instantiate val (pToV x r),+ updateEnv [(x, val)] env, err) : solveInProblems x val ps)++updateProblems ctxt ns ps inj holes = up ns ps where+ up ns [] = (ns, [])+ up ns ((x, y, env, err) : ps) = let x' = updateSolved ns x- y' = updateSolved ns y in- (x',y',env,err) : updateProblems ns ps+ y' = updateSolved ns y + err' = updateError ns err+ env' = updateEnv ns env in+ case unify ctxt env' x' y' inj holes of+ OK (v, []) -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $ + up (ns ++ v) ps+ _ -> let (ns', ps') = up ns ps in+ (ns', (x',y',env',err') : ps') processTactic :: Tactic -> ProofState -> TC (ProofState, String) processTactic QED ps = case holes ps of@@ -568,18 +610,16 @@ Just pold -> return (pold, "") processTactic EndUnify ps = let (h, ns_in) = unified ps- ns = dropGiven (dontunify ps) ns_in+ ns = dropGiven (dontunify ps) ns_in (holes ps) ns' = map (\ (n, t) -> (n, updateSolved ns t)) ns - tm' = -- trace ("Updating " ++ show ns') $ -- ++ " in " ++ show (pterm ps)) $- updateSolved ns' (pterm ps) - probs' = updateProblems ns' (problems ps) in- case probs' of- [] -> return (ps { pterm = tm', - unified = (h, []),- injective = map (tmap (updateSolved ns')) - (injective ps),- holes = holes ps \\ map fst ns' }, "")- errs@((_,_,_,err):_) -> tfail err+ (ns'', probs') = updateProblems (context ps) ns' (problems ps)+ (injective ps) (holes ps)+ tm' = -- trace ("Updating " ++ show ns' ++ "\n" ++ show ns'') $ -- ++ " in " ++ show (pterm ps)) $+ updateSolved ns'' (pterm ps) in+ return (ps { pterm = tm', + unified = (h, []),+ problems = probs',+ holes = holes ps \\ map fst ns'' }, "") processTactic (Reorder n) ps = do ps' <- execStateT (tactic (Just n) reorder_claims) ps return (ps' { previous = Just ps, plog = "" }, plog ps')@@ -590,9 +630,21 @@ let pterm' = case solved ps' of Just s -> updateSolved [s] (pterm ps') _ -> pterm ps'- return (ps' { pterm = pterm',+ let (ns', probs') + = case solved ps' of+ Just s -> updateProblems (context ps')+ [s] (problems ps') + (injective ps')+ (holes ps')+ _ -> ([], problems ps')+ -- rechecking problems may find more solutions, so + -- apply them here+ let pterm'' = updateSolved ns' pterm'+ return (ps' { pterm = pterm'', solved = Nothing,- previous = Just ps, plog = "" }, plog ps')+ problems = probs',+ previous = Just ps, plog = "",+ holes = holes ps' \\ (map fst ns')}, plog ps') process :: Tactic -> Name -> StateT TState TC () process EndUnify _ @@ -624,5 +676,6 @@ mktac (Defer n) = defer n mktac (DeferType n t a) = deferType n t a mktac (Instance n) = instanceArg n+ mktac (SetInjective n) = setinj n mktac (MoveLast n) = movelast n
src/Core/TT.hs view
@@ -260,8 +260,8 @@ data Const = I Int | BI Integer | Fl Double | Ch Char | Str String | IType | BIType | FlType | ChType | StrType - | W8 Word8 | W16 Word16- | W8Type | W16Type + | B8 Word8 | B16 Word16 | B32 Word32 | B64 Word64+ | B8Type | B16Type | B32Type | B64Type | PtrType | VoidType | Forgot deriving (Eq, Ord)@@ -286,8 +286,10 @@ pretty PtrType = text "Ptr" pretty VoidType = text "Void" pretty Forgot = text "Forgot"- pretty W8Type = text "Word8"- pretty W16Type = text "Word16"+ pretty B8Type = text "Bits8"+ pretty B16Type = text "Bits16"+ pretty B32Type = text "Bits32"+ pretty B64Type = text "Bits64" data Raw = Var Name | RBind Name (Binder Raw) Raw@@ -480,7 +482,7 @@ deriving (Show, Functor, Eq) instance Eq n => Eq (TT n) where- (==) (P xt x _) (P yt y _) = xt == yt && x == y+ (==) (P xt x _) (P yt y _) = x == y (==) (V x) (V y) = x == y (==) (Bind _ xb xs) (Bind _ yb ys) = xb == yb && xs == ys (==) (App fx ax) (App fy ay) = fx == fy && ax == ay@@ -689,16 +691,20 @@ show (Fl f) = show f show (Ch c) = show c show (Str s) = show s- show (W8 x) = show x- show (W16 x) = show x+ show (B8 x) = show x+ show (B16 x) = show x+ show (B32 x) = show x+ show (B64 x) = show x show IType = "Int" show BIType = "Integer" show FlType = "Float" show ChType = "Char" show StrType = "String" show PtrType = "Ptr"- show W8Type = "Word8"- show W16Type = "Word16"+ show B8Type = "Bits8"+ show B16Type = "Bits16"+ show B32Type = "Bits32"+ show B64Type = "Bits64" show VoidType = "Void" showEnv env t = showEnv' env t False@@ -788,13 +794,17 @@ -- Check whether a term has any holes in it - impure if so -pureTerm :: TT n -> Bool+pureTerm :: TT Name -> Bool pureTerm (App f a) = pureTerm f && pureTerm a-pureTerm (Bind n b sc) = pureBinder b && pureTerm sc where+pureTerm (Bind n b sc) = notClassName n && pureBinder b && pureTerm sc where pureBinder (Hole _) = False pureBinder (Guess _ _) = False pureBinder (Let t v) = pureTerm t && pureTerm v pureBinder t = pureTerm (binderTy t)++ notClassName (MN _ "class") = False+ notClassName _ = True+ pureTerm _ = True -- weaken a term by adding i to each de Bruijn index (i.e. lift it over i bindings)
src/Core/Typecheck.hs view
@@ -29,10 +29,10 @@ converts :: Context -> Env -> Term -> Term -> TC () converts ctxt env x y = case convEq' ctxt x y of - OK _ -> return ()+ OK True -> return () _ -> case convEq' ctxt (finalise (normalise ctxt env x)) (finalise (normalise ctxt env y)) of- OK _ -> return ()+ OK True -> return () _ -> tfail (CantConvert (finalise (normalise ctxt env x)) (finalise (normalise ctxt env y)) (errEnv env))@@ -68,7 +68,9 @@ let fty' = case uniqueBinders (map fst env) (finalise fty) of ty@(Bind x (Pi s) t) -> ty _ -> uniqueBinders (map fst env) - $ hnf ctxt env fty+ $ case hnf ctxt env fty of+ ty@(Bind x (Pi s) t) -> ty+ _ -> normalise ctxt env fty case fty' of Bind x (Pi s) t -> -- trace ("Converting " ++ show aty ++ " and " ++ show s ++@@ -101,8 +103,10 @@ constType (Fl _) = Constant FlType constType (Ch _) = Constant ChType constType (Str _) = Constant StrType- constType (W8 _) = Constant W8Type- constType (W16 _) = Constant W16Type+ constType (B8 _) = Constant B8Type+ constType (B16 _) = Constant B16Type+ constType (B32 _) = Constant B32Type+ constType (B64 _) = Constant B64Type constType Forgot = Erased constType _ = TType (UVal 0) chk env (RForce t) = do (_, ty) <- chk env t
src/Core/Unify.hs view
@@ -20,25 +20,29 @@ type Injs = [(TT Name, TT Name, TT Name)] type Fails = [(TT Name, TT Name, Env, Err)] -data UInfo = UI Int Injs Fails+data UInfo = UI Int Fails deriving Show -unify :: Context -> Env -> TT Name -> TT Name -> TC ([(Name, TT Name)], - Injs, Fails)-unify ctxt env topx topy =--- trace ("Unifying " ++ show (topx, topy)) $+data UResult a = UOK a+ | UPartOK a+ | UFail Err++unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] ->+ TC ([(Name, TT Name)], Fails)+unify ctxt env topx topy injtc holes =+-- trace ("Unifying " ++ show (topx, topy)) $ -- don't bother if topx and topy are different at the head- case runStateT (un False [] topx topy) (UI 0 [] []) of- OK (v, UI _ inj []) -> return (filter notTrivial v, inj, [])--- Error e@(CantUnify False _ _ _ _ _) -> tfail e+ case runStateT (un False [] topx topy) (UI 0 []) of+ OK (v, UI _ []) -> return (filter notTrivial v, []) res -> let topxn = normalise ctxt env topx topyn = normalise ctxt env topy in -- trace ("Unifying " ++ show (topx, topy) ++ "\n\n==>\n" ++ show (topxn, topyn) ++ "\n\n" ++ show res ++ "\n\n") $ case runStateT (un False [] topxn topyn)- (UI 0 [] []) of- OK (v, UI _ inj fails) -> - return (filter notTrivial v, inj, reverse fails)+ (UI 0 []) of+ OK (v, UI _ fails) -> + return (filter notTrivial v, reverse fails)+-- Error e@(CantUnify False _ _ _ _ _) -> tfail e Error e -> tfail e where notTrivial (x, P _ x' _) = x /= x'@@ -50,21 +54,22 @@ injective (P (DCon _ _) _ _) = True injective (P (TCon _ _) _ _) = True+ injective (P _ n _) = n `elem` injtc injective (App f a) = injective f injective _ = False notP (P _ _ _) = False notP _ = True - sc i = do UI s x f <- get- put (UI (s+i) x f)+ sc i = do UI s f <- get+ put (UI (s+i) f) - uplus u1 u2 = do UI s i f <- get+ uplus u1 u2 = do UI s f <- get r <- u1- UI s _ f' <- get+ UI s f' <- get if (length f == length f') then return r- else do put (UI s i f); u2+ else do put (UI s f); u2 un :: Bool -> [(Name, Name)] -> TT Name -> TT Name -> StateT UInfo @@ -89,34 +94,53 @@ = unifyFail topx topy un' fn names topx@(P (TCon _ _) x _) topy@(P (DCon _ _) y _) = unifyFail topx topy- un' fn bnames (P Bound x _) (P Bound y _) - | (x,y) `elem` bnames = do sc 1; return []- un' fn bnames (P Bound x _) tm- | holeIn env x = do UI s i f <- get+ un' fn bnames tx@(P _ x _) ty@(P _ y _) + | (x,y) `elem` bnames || x == y = do sc 1; return []+ | injective tx && not (holeIn env y || y `elem` holes)+ = unifyFail tx ty+ | injective ty && not (holeIn env x || x `elem` holes)+ = unifyFail tx ty+ un' fn bnames xtm@(P _ x _) tm+ | holeIn env x || x `elem` holes+ = do UI s f <- get -- injectivity check- when (notP tm && fn) $ + if (notP tm && fn) -- trace (show (x, tm, normalise ctxt env tm)) $- put (UI s ((tm, topx, topy) : i) f)- sc 1- checkCycle (x, tm)- un' fn bnames tm (P Bound y _)- | holeIn env y = do UI s i f <- get+-- put (UI s ((tm, topx, topy) : i) f)+ then unifyTmpFail xtm tm + else do sc 1+ checkCycle (x, tm)+ | not (injective xtm) && injective tm = unifyFail xtm tm+ un' fn bnames tm ytm@(P _ y _)+ | holeIn env y || y `elem` holes+ = do UI s f <- get -- injectivity check- when (notP tm && fn) $ + if (notP tm && fn) -- trace (show (y, tm, normalise ctxt env tm)) $- put (UI s ((tm, topx, topy) : i) f)- sc 1- checkCycle (y, tm)- un' fn bnames (V i) (P Bound x _)+-- put (UI s ((tm, topx, topy) : i) f)+ then unifyTmpFail tm ytm+ else do sc 1+ checkCycle (y, tm)+ | not (injective ytm) && injective tm = unifyFail ytm tm+ un' fn bnames (V i) (P _ x _) | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []- un' fn bnames (P Bound x _) (V i)+ un' fn bnames (P _ x _) (V i) | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return [] - un' fn bnames appx@(App fx ax) appy@(App fy ay) - = do let (headx, _) = unApply fx- let (heady, _) = unApply fy- checkHeads headx heady- uplus -- do the second one if the first adds any errors + un' fn bnames appx@(App fx ax) appy@(App fy ay)+ | injective fx && metavarApp appy + || injective fy && metavarApp appx + || injective fx && injective fy + || fx == fy+ = do let (headx, _) = unApply fx+ let (heady, _) = unApply fy+ -- fail quickly if the heads are disjoint+ checkHeads headx heady+-- if True then -- (injective fx || injective fy || fx == fy) then+-- if (injective fx && metavarApp appy) || +-- (injective fy && metavarApp appx) ||+-- (injective fx && injective fy) || fx == fy+ uplus (do hf <- un' True bnames fx fy let ax' = hnormalise hf ctxt env (substNames hf ax) let ay' = hnormalise hf ctxt env (substNames hf ay)@@ -129,8 +153,17 @@ hf <- un' False bnames fx' fy' sc 1 combine bnames hf ha)+ | otherwise + = do let (headx, argsx) = unApply appx+ let (heady, argsy) = unApply appy+ if (length argsx == length argsy && + ((headx == heady) || (argsx == argsy) ||+ (notFn headx && notFn heady))) then+ do uf <- un' True bnames headx heady+ unArgs uf argsx argsy+ else unifyTmpFail appx appy where hnormalise [] _ _ t = t- hnormalise ns ctxt env t = normalise ctxt env t+ hnormalise ns ctxt env t = hnf ctxt env t checkHeads (P (DCon _ _) x _) (P (DCon _ _) y _) | x /= y = unifyFail appx appy checkHeads (P (TCon _ _) x _) (P (TCon _ _) y _)@@ -141,6 +174,25 @@ = unifyFail appx appy checkHeads _ _ = return [] + unArgs as [] [] = return as+ unArgs as (x : xs) (y : ys) + = do let x' = hnormalise as ctxt env (substNames as x)+ let y' = hnormalise as ctxt env (substNames as y) + as' <- un' False bnames x' y'+ vs <- combine bnames as as'+ unArgs vs xs ys++ metavarApp tm = let (f, args) = unApply tm in+ all (\x -> metavar x || notFn x) (f : args)+ metavar t = case t of+ P _ x _ -> x `elem` holes || holeIn env x+ _ -> False+ inenv t = case t of+ P _ x _ -> x `elem` (map fst env) + _ -> False++ notFn t = injective t || metavar t || inenv t + un' fn bnames x (Bind n (Lam t) (App y (P Bound n' _))) | n == n' = un' False bnames x y un' fn bnames (Bind n (Lam t) (App x (P Bound n' _))) y@@ -155,20 +207,28 @@ combine bnames h1 h2 un' fn bnames x y | OK True <- convEq' ctxt x y = do sc 1; return []- | otherwise = do UI s i f <- get+ | otherwise = do UI s f <- get let r = recoverable x y let err = CantUnify r topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s if (not r) then lift $ tfail err- else do put (UI s i ((x, y, env, err) : f))+ else do put (UI s ((x, y, env, err) : f)) return [] -- lift $ tfail err + unifyTmpFail x y + = do UI s f <- get+ let r = recoverable x y+ let err = CantUnify r+ topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s+ put (UI s ((x, y, env, err) : f))+ return []+ -- shortcut failure, if we *know* nothing can fix it- unifyFail x y = do UI s i f <- get+ unifyFail x y = do UI s f <- get let r = recoverable x y let err = CantUnify r topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s- put (UI s i ((x, y, env, err) : f))+ put (UI s ((x, y, env, err) : f)) lift $ tfail err @@ -186,18 +246,23 @@ uB bnames (Pi tx) (Pi ty) = do sc 1; un' False bnames tx ty uB bnames (Hole tx) (Hole ty) = un' False bnames tx ty uB bnames (PVar tx) (PVar ty) = un' False bnames tx ty- uB bnames x y = do UI s i f <- get+ uB bnames x y = do UI s f <- get let r = recoverable (binderTy x) (binderTy y) let err = CantUnify r topx topy (CantUnify r (binderTy x) (binderTy y) (Msg "") [] s) (errEnv env) s- put (UI s i ((binderTy x, binderTy y, env, err) : f))+ put (UI s ((binderTy x, binderTy y, env, err) : f)) return [] -- lift $ tfail err checkCycle p@(x, P _ _ _) = return [p] checkCycle (x, tm) | not (x `elem` freeNames tm) = return [(x, tm)] | otherwise = lift $ tfail (InfiniteUnify x tm (errEnv env)) ++ combineArgs bnames args = ca [] args where+ ca acc [] = return acc+ ca acc (x : xs) = do x' <- combine bnames acc x+ ca x' xs combine bnames as [] = return as combine bnames as ((n, t) : bs)
src/IRTS/CodegenC.hs view
@@ -62,7 +62,7 @@ headers xs = concatMap (\h -> "#include <" ++ h ++ ">\n")- (xs ++ ["idris_rts.h", "idris_stdfgn.h", "gmp.h", "assert.h"])+ (xs ++ ["idris_rts.h", "idris_bitstring.h", "idris_stdfgn.h", "gmp.h", "assert.h"]) debug TRACE = "#define IDRIS_TRACE\n\n" debug _ = ""@@ -297,6 +297,144 @@ doOp _ LPrintNum [x] = "printf(\"%ld\\n\", GETINT(" ++ creg x ++ "))" doOp _ LPrintStr [x] = "fputs(GETSTR(" ++ creg x ++ "), stdout)" +doOp v LIntB8 [x] = v ++ "idris_b8(vm, " ++ creg x ++ ")"+doOp v LIntB16 [x] = v ++ "idris_b16(vm, " ++ creg x ++ ")"+doOp v LIntB32 [x] = v ++ "idris_b32(vm, " ++ creg x ++ ")"+doOp v LIntB64 [x] = v ++ "idris_b64(vm, " ++ creg x ++ ")"++doOp v LB32Int [x] = v ++ "idris_castB32Int(vm, " ++ creg x ++ ")"++doOp v LB8Lt [x, y] = v ++ "idris_b8Lt(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB8Lte [x, y] = v ++ "idris_b8Lte(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB8Eq [x, y] = v ++ "idris_b8Eq(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB8Gte [x, y] = v ++ "idris_b8Gte(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB8Gt [x, y] = v ++ "idris_b8Gt(vm, " ++ creg x ++ "," ++ creg y ++ ")"++doOp v LB8Shl [x, y] = v ++ "idris_b8Shl(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB8LShr [x, y] = v ++ "idris_b8Shr(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB8AShr [x, y] = v ++ "idris_b8AShr(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB8And [x, y] = v ++ "idris_b8And(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB8Or [x, y] = v ++ "idris_b8Or(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB8Xor [x, y] = v ++ "idris_b8Xor(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB8Compl [x] = v ++ "idris_b8Compl(vm, " ++ creg x ++ ")"++doOp v LB8Plus [x, y] = v ++ "idris_b8Plus(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB8Minus [x, y] = v ++ "idris_b8Minus(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB8Times [x, y] = v ++ "idris_b8Times(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB8UDiv [x, y] = v ++ "idris_b8UDiv(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB8SDiv [x, y] = v ++ "idris_b8SDiv(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB8URem [x, y] = v ++ "idris_b8URem(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB8SRem [x, y] = v ++ "idris_b8SRem(vm, " ++ creg x ++ "," ++ creg y ++ ")"++doOp v LB8Z16 [x] = v ++ "idris_b8Z16(vm, " ++ creg x ++ ")"+doOp v LB8Z32 [x] = v ++ "idris_b8Z32(vm, " ++ creg x ++ ")"+doOp v LB8Z64 [x] = v ++ "idris_b8Z64(vm, " ++ creg x ++ ")"+doOp v LB8S16 [x] = v ++ "idris_b8S16(vm, " ++ creg x ++ ")"+doOp v LB8S32 [x] = v ++ "idris_b8S32(vm, " ++ creg x ++ ")"+doOp v LB8S64 [x] = v ++ "idris_b8S64(vm, " ++ creg x ++ ")"++doOp v LB16Lt [x, y] = v ++ "idris_b16Lt(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB16Lte [x, y] = v ++ "idris_b16Lte(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB16Eq [x, y] = v ++ "idris_b16Eq(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB16Gte [x, y] = v ++ "idris_b16Gte(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB16Gt [x, y] = v ++ "idris_b16Gt(vm, " ++ creg x ++ "," ++ creg y ++ ")"++doOp v LB16Shl [x, y] = v ++ "idris_b16Shl(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB16LShr [x, y] = v ++ "idris_b16Shr(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB16AShr [x, y] = v ++ "idris_b16AShr(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB16And [x, y] = v ++ "idris_b16And(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB16Or [x, y] = v ++ "idris_b16Or(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB16Xor [x, y] = v ++ "idris_b16Xor(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB16Compl [x] = v ++ "idris_b16Compl(vm, " ++ creg x ++ ")"++doOp v LB16Plus [x, y] =+ v ++ "idris_b16Plus(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB16Minus [x, y] =+ v ++ "idris_b16Minus(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB16Times [x, y] =+ v ++ "idris_b16Times(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB16UDiv [x, y] =+ v ++ "idris_b16UDiv(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB16SDiv [x, y] =+ v ++ "idris_b16SDiv(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB16URem [x, y] =+ v ++ "idris_b16URem(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB16SRem [x, y] =+ v ++ "idris_b16SRem(vm, " ++ creg x ++ "," ++ creg y ++ ")"++doOp v LB16Z32 [x] = v ++ "idris_b16Z32(vm, " ++ creg x ++ ")"+doOp v LB16Z64 [x] = v ++ "idris_b16Z64(vm, " ++ creg x ++ ")"+doOp v LB16S32 [x] = v ++ "idris_b16S32(vm, " ++ creg x ++ ")"+doOp v LB16S64 [x] = v ++ "idris_b16S64(vm, " ++ creg x ++ ")"+doOp v LB16T8 [x] = v ++ "idris_b16T8(vm, " ++ creg x ++ ")"++doOp v LB32Lt [x, y] = v ++ "idris_b32Lt(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB32Lte [x, y] = v ++ "idris_b32Lte(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB32Eq [x, y] = v ++ "idris_b32Eq(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB32Gte [x, y] = v ++ "idris_b32Gte(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB32Gt [x, y] = v ++ "idris_b32Gt(vm, " ++ creg x ++ "," ++ creg y ++ ")"++doOp v LB32Shl [x, y] = v ++ "idris_b32Shl(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB32LShr [x, y] = v ++ "idris_b32Shr(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB32AShr [x, y] = v ++ "idris_b32AShr(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB32And [x, y] = v ++ "idris_b32And(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB32Or [x, y] = v ++ "idris_b32Or(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB32Xor [x, y] = v ++ "idris_b32Xor(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB32Compl [x] = v ++ "idris_b32Compl(vm, " ++ creg x ++ ")"++doOp v LB32Plus [x, y] =+ v ++ "idris_b32Plus(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB32Minus [x, y] =+ v ++ "idris_b32Minus(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB32Times [x, y] =+ v ++ "idris_b32Times(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB32UDiv [x, y] =+ v ++ "idris_b32UDiv(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB32SDiv [x, y] =+ v ++ "idris_b32SDiv(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB32URem [x, y] =+ v ++ "idris_b32URem(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB32SRem [x, y] =+ v ++ "idris_b32SRem(vm, " ++ creg x ++ "," ++ creg y ++ ")"++doOp v LB32Z64 [x] = v ++ "idris_b32Z64(vm, " ++ creg x ++ ")"+doOp v LB32S64 [x] = v ++ "idris_b32S64(vm, " ++ creg x ++ ")"+doOp v LB32T8 [x] = v ++ "idris_b32T8(vm, " ++ creg x ++ ")"+doOp v LB32T16 [x] = v ++ "idris_b32T16(vm, " ++ creg x ++ ")"++doOp v LB64Lt [x, y] = v ++ "idris_b64Lt(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB64Lte [x, y] = v ++ "idris_b64Lte(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB64Eq [x, y] = v ++ "idris_b64Eq(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB64Gte [x, y] = v ++ "idris_b64Gte(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB64Gt [x, y] = v ++ "idris_b64Gt(vm, " ++ creg x ++ "," ++ creg y ++ ")"++doOp v LB64Shl [x, y] = v ++ "idris_b64Shl(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB64LShr [x, y] = v ++ "idris_b64Shr(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB64AShr [x, y] = v ++ "idris_b64AShr(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB64And [x, y] = v ++ "idris_b64And(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB64Or [x, y] = v ++ "idris_b64Or(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB64Xor [x, y] = v ++ "idris_b64Xor(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB64Compl [x] = v ++ "idris_b64Compl(vm, " ++ creg x ++ ")"++doOp v LB64Plus [x, y] =+ v ++ "idris_b64Plus(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB64Minus [x, y] =+ v ++ "idris_b64Minus(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB64Times [x, y] =+ v ++ "idris_b64Times(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB64UDiv [x, y] =+ v ++ "idris_b64UDiv(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB64SDiv [x, y] =+ v ++ "idris_b64SDiv(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB64URem [x, y] =+ v ++ "idris_b64URem(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LB64SRem [x, y] =+ v ++ "idris_b64SRem(vm, " ++ creg x ++ "," ++ creg y ++ ")"++doOp v LB64T8 [x] = v ++ "idris_b64T8(vm, " ++ creg x ++ ")"+doOp v LB64T16 [x] = v ++ "idris_b64T16(vm, " ++ creg x ++ ")"+doOp v LB64T32 [x] = v ++ "idris_b64T32(vm, " ++ creg x ++ ")"+ doOp v LFExp [x] = v ++ "MKFLOAT(exp(GETFLOAT(" ++ creg x ++ ")))" doOp v LFLog [x] = v ++ "MKFLOAT(log(GETFLOAT(" ++ creg x ++ ")))" doOp v LFSin [x] = v ++ "MKFLOAT(sin(GETFLOAT(" ++ creg x ++ ")))"@@ -325,4 +463,4 @@ doOp v LChInt args = v ++ creg (last args) doOp v LIntCh args = v ++ creg (last args) doOp v LNoOp args = v ++ creg (last args)-doOp _ _ _ = "FAIL"+doOp _ op _ = "FAIL /* " ++ show op ++ " */"
src/IRTS/CodegenJavaScript.hs view
@@ -1,11 +1,6 @@ {-# LANGUAGE PatternGuards #-} -{-- BigInteger Javascript code taken from:- https://github.com/peterolson/BigInteger.js--}--module IRTS.CodegenJavaScript (codegenJavaScript) where+module IRTS.CodegenJavaScript (codegenJavaScript, JSTarget(..)) where import Idris.AbsSyntax import IRTS.Bytecode@@ -19,22 +14,36 @@ import Control.Arrow import Data.Char import Data.List+import qualified Data.Map as Map import System.IO -type NamespaceName = String--idrNamespace :: NamespaceName+idrNamespace :: String idrNamespace = "__IDR__" +data JSTarget = Node | JavaScript+ codegenJavaScript- :: [(Name, SDecl)]+ :: JSTarget+ -> [(Name, SDecl)] -> FilePath -> OutputType -> IO ()-codegenJavaScript definitions filename outputType =- writeFile filename output+codegenJavaScript target definitions filename outputType = do+ let runtime = case target of+ Node -> "-node"+ JavaScript -> "-browser"+ path <- getDataDir+ idrRuntime <- readFile $ path ++ "/js/Runtime-common.js"+ tgtRuntime <- readFile $ concat [path, "/js/Runtime", runtime, ".js"]+ writeFile filename (idrRuntime+ ++ tgtRuntime+ ++ modules + ++ functions+ ++ mainLoop) where def = map (first translateNamespace) definitions+ + functions = concatMap translateDeclaration def mainLoop :: String mainLoop = intercalate "\n" [ "\nfunction main() {"@@ -42,115 +51,72 @@ , "}\n\nmain();\n" ] - output :: String- output = concat [ idrRuntime- , concatMap (translateModule Nothing) def- , mainLoop- ]--idrRuntime :: String-idrRuntime =- createModule Nothing idrNamespace $ concat- [ "__IDR__.Type = function(type) { this.type = type; };"- , "__IDR__.Int = new __IDR__.Type('Int');"- , "__IDR__.Char = new __IDR__.Type('Char');"- , "__IDR__.String = new __IDR__.Type('String');"- , "__IDR__.Integer = new __IDR__.Type('Integer');"- , "__IDR__.Float = new __IDR__.Type('Float');"- , "__IDR__.Forgot = new __IDR__.Type('Forgot');" -- , "__IDR__.bigInt=function(){var e=1e7,t=7,n={positive:!1,negative:!0},r=function(e,t){var n=e.value,r=t.value,i=n.length>r.length?n.length:r.length;for(var s=0;s<i;s++)n[s]=n[s]||0,r[s]=r[s]||0;for(var s=i-1;s>=0;s--){if(n[s]!==0||r[s]!==0)break;n.pop(),r.pop()}n.length||(n=[0],r=[0]),e.value=n,t.value=r},i=function(e,s){if(typeof e=='object')return e;e+='';var u=n.positive,a=[];e[0]==='-'&&(u=n.negative,e=e.slice(1));var e=e.split('e');if(e.length>2)throw new Error('Invalid integer');if(e[1]){var f=e[1];f[0]==='+'&&(f=f.slice(1)),f=i(f);if(f.lesser(0))throw new Error('Cannot include negative exponent part for integers');while(f.notEquals(0))e[0]+='0',f=f.prev()}e=e[0],e==='-0'&&(e='0');var l=/^([1-9][0-9]*)$|^0$/.test(e);if(!l)throw new Error('Invalid integer');while(e.length){var c=e.length>t?e.length-t:0;a.push(+e.slice(c)),e=e.slice(0,c)}var h=o(a,u);return s&&r(s,h),h},s=function(e,t){var e=o(e,n.positive),t=o(t,n.positive);if(e.equals(0))throw new Error('Cannot divide by 0');var r=0;do{var i=1,s=o(e.value,n.positive),u=s.times(10);while(u.lesser(t))s=u,i*=10,u=u.times(10);while(s.lesserOrEquals(t))t=t.minus(s),r+=i}while(e.lesserOrEquals(t));return{remainder:t.value,result:r}},o=function(f,l){var c={value:f,sign:l},h={value:f,sign:l,negate:function(e){var t=e||c;return o(t.value,!t.sign)},abs:function(e){var t=e||c;return o(t.value,n.positive)},add:function(t,s){var u,a=c,f;s?(a=i(t))&&(f=i(s)):f=i(t,a),u=a.sign;if(a.sign!==f.sign)return a=o(a.value,n.positive),f=o(f.value,n.positive),u===n.positive?h.subtract(a,f):h.subtract(f,a);r(a,f);var l=a.value,p=f.value,d=[],v=0;for(var m=0;m<l.length||v>0;m++){var g=l[m]+p[m]+v;v=g>e?1:0,g-=v*e,d.push(g)}return o(d,u)},plus:function(e,t){return h.add(e,t)},subtract:function(t,r){var s=c,u;r?(s=i(t))&&(u=i(r)):u=i(t,s);if(s.sign!==u.sign)return h.add(s,h.negate(u));if(s.sign===n.negative)return h.subtract(h.negate(u),h.negate(s));if(h.compare(s,u)===-1)return h.negate(h.subtract(u,s));var a=s.value,f=u.value,l=[],p=0;for(var d=0;d<a.length;d++){a[d]-=p,p=a[d]<f[d]?1:0;var v=p*e+a[d]-f[d];l.push(v)}return o(l,n.positive)},minus:function(e,t){return h.subtract(e,t)},multiply:function(t,n){var r,s=c,u;n?(s=i(t))&&(u=i(n)):u=i(t,s),r=s.sign!==u.sign;var a=s.value,f=u.value,l=[];for(var h=0;h<a.length;h++){l[h]=[];var p=h;while(p--)l[h].push(0)}var d=0;for(var h=0;h<a.length;h++){var v=a[h];for(var p=0;p<f.length||d>0;p++){var m=f[p],g=m?v*m+d:d;d=g>e?Math.floor(g/e):0,g-=d*e,l[h].push(g)}}var y=-1;for(var h=0;h<l.length;h++){var b=l[h].length;b>y&&(y=b)}var w=[],d=0;for(var h=0;h<y||d>0;h++){var E=d;for(var p=0;p<l.length;p++)E+=l[p][h]||0;d=E>e?Math.floor(E/e):0,E-=d*e,w.push(E)}return o(w,r)},times:function(e,t){return h.multiply(e,t)},divmod:function(e,t){var r,u=c,a;t?(u=i(e))&&(a=i(t)):a=i(e,u),r=u.sign!==a.sign;if(o(u.value,u.sign).equals(0))return{quotient:o([0],n.positive),remainder:o([0],n.positive)};if(a.equals(0))throw new Error('Cannot divide by zero');var f=u.value,l=a.value,h=[],p=[];for(var d=f.length-1;d>=0;d--){var e=[f[d]].concat(p),v=s(l,e);h.push(v.result),p=v.remainder}return h.reverse(),{quotient:o(h,r),remainder:o(p,u.sign)}},divide:function(e,t){return h.divmod(e,t).quotient},over:function(e,t){return h.divide(e,t)},mod:function(e,t){return h.divmod(e,t).remainder},pow:function(e,t){var n=c,r;t?(n=i(e))&&(r=i(t)):r=i(e,n);var s=n,f=r;if(f.lesser(0))return u;if(f.equals(0))return a;var l=o(s.value,s.sign);if(f.mod(2).equals(0)){var h=l.pow(f.over(2));return h.times(h)}return l.times(l.pow(f.minus(1)))},next:function(e){var t=e||c;return h.add(t,1)},prev:function(e){var t=e||c;return h.subtract(t,1)},compare:function(e,t){var s=c,o;t?(s=i(e))&&(o=i(t,s)):o=i(e,s),r(s,o);if(s.value.length===1&&o.value.length===1&&s.value[0]===0&&o.value[0]===0)return 0;if(o.sign!==s.sign)return s.sign===n.positive?1:-1;var u=s.sign===n.positive?1:-1,a=s.value,f=o.value;for(var l=a.length-1;l>=0;l--){if(a[l]>f[l])return 1*u;if(f[l]>a[l])return-1*u}return 0},compareAbs:function(e,t){var r=c,s;return t?(r=i(e))&&(s=i(t,r)):s=i(e,r),r.sign=s.sign=n.positive,h.compare(r,s)},equals:function(e,t){return h.compare(e,t)===0},notEquals:function(e,t){return!h.equals(e,t)},lesser:function(e,t){return h.compare(e,t)<0},greater:function(e,t){return h.compare(e,t)>0},greaterOrEquals:function(e,t){return h.compare(e,t)>=0},lesserOrEquals:function(e,t){return h.compare(e,t)<=0},isPositive:function(e){var t=e||c;return t.sign===n.positive},isNegative:function(e){var t=e||c;return t.sign===n.negative},isEven:function(e){var t=e||c;return t.value[0]%2===0},isOdd:function(e){var t=e||c;return t.value[0]%2===1},toString:function(r){var i=r||c,s='',o=i.value.length;while(o--)s+=(e.toString()+i.value[o]).slice(-t);while(s[0]==='0')s=s.slice(1);s.length||(s='0');var u=i.sign===n.positive?'':'-';return u+s},toJSNumber:function(e){return+h.toString(e)},valueOf:function(e){return h.toJSNumber(e)}};return h},u=o([0],n.positive),a=o([1],n.positive),f=o([1],n.negative),l=function(e){return typeof e=='undefined'?u:i(e)};return l.zero=u,l.one=a,l.minusOne=f,l}();typeof module!='undefined'&&(module.exports=__IDR__.bigInt);"-- , "__IDR__.Tailcall = function(f) { this.f = f };"-- , "__IDR__.Con = function(i,name,vars)"- , "{this.i = i;this.name = name;this.vars = vars;};\n"-- , "__IDR__.tailcall = function(f){\n"- ++ "var __f = f;\n"- ++ "while (__f) {\n"- ++ "var f = __f;\n"- ++ "__f = null;\n"- ++ "var ret = f();\n"- ++ "if (ret instanceof __IDR__.Tailcall) {\n"- ++ "__f = ret.f;"- ++ "\n} else {\n"- ++ "return ret;"- ++ "\n}"- ++ "\n}"- ++ "\n};\n"-- , "var newline_regex =/(.*)\\n$/;\n"-- , "__IDR__.print = function(s){\n"- ++ "var m = s.match(newline_regex);\n"- ++ "console.log(m ? m[1] : s);"- ++ "\n};\n"- ]--createModule :: Maybe String -> NamespaceName -> String -> String-createModule toplevel modname body =- concat [header modname, body, footer modname]- where- header :: NamespaceName -> String- header modname =- concatMap (++ "\n")- [ "\nvar " ++ modname ++ ";"- , "(function(" ++ modname ++ "){"- ]-- footer :: NamespaceName -> String- footer modname =- let m = maybe "" (++ ".") toplevel ++ modname in- "\n})("- ++ m- ++ " || ("- ++ m- ++ " = {})"- ++ ");\n"+ modules =+ concatMap allocMod mods+ where+ allocMod m = intercalate "." m ++ " = {};\n"+ sortMods a b = compare (length a) (length b) -translateModule :: Maybe String -> ([String], SDecl) -> String-translateModule toplevel ([modname], decl) =- let body = translateDeclaration modname decl in- createModule toplevel modname body-translateModule toplevel (n:ns, decl) =- createModule toplevel n $ translateModule (Just n) (ns, decl)+ mods =+ drop 1 $ sortBy sortMods $ nub $ concatMap (inits . fst) def translateIdentifier :: String -> String translateIdentifier =- concatMap replaceBadChars+ replaceReserved . concatMap replaceBadChars where replaceBadChars :: Char -> String- replaceBadChars ' ' = "_"- replaceBadChars '_' = "__"- replaceBadChars '@' = "_at"- replaceBadChars '[' = "_OSB"- replaceBadChars ']' = "_CSB"- replaceBadChars '(' = "_OP"- replaceBadChars ')' = "_CP"- replaceBadChars '{' = "_OB"- replaceBadChars '}' = "_CB"- replaceBadChars '!' = "_bang"- replaceBadChars '#' = "_hash"- replaceBadChars '.' = "_dot"- replaceBadChars ',' = "_comma"- replaceBadChars ':' = "_colon"- replaceBadChars '+' = "_plus"- replaceBadChars '-' = "_minus"- replaceBadChars '*' = "_times"- replaceBadChars '<' = "_lt"- replaceBadChars '>' = "_gt"- replaceBadChars '=' = "_eq"- replaceBadChars '|' = "_pipe"- replaceBadChars '&' = "_amp"- replaceBadChars '/' = "_SL"- replaceBadChars '\\' = "_BSL"- replaceBadChars '%' = "_per"- replaceBadChars '?' = "_que"- replaceBadChars '~' = "_til"- replaceBadChars '\'' = "_apo" replaceBadChars c+ | ' ' <- c = "_"+ | '_' <- c = "__" | isDigit c = "_" ++ [c] ++ "_"+ | not (isLetter c && isAscii c) = '_' : show (ord c) | otherwise = [c]+ replaceReserved s+ | s `elem` reserved = '_' : s+ | otherwise = s+ reserved = [ "break"+ , "case"+ , "catch"+ , "continue"+ , "debugger"+ , "default"+ , "delete"+ , "do"+ , "else"+ , "finally"+ , "for"+ , "function"+ , "if"+ , "in"+ , "instanceof"+ , "new"+ , "return"+ , "switch"+ , "this"+ , "throw"+ , "try"+ , "typeof"+ , "var"+ , "void"+ , "while"+ , "with"+ + , "class"+ , "enum"+ , "export"+ , "extends"+ , "import"+ , "super"+ + , "implements"+ , "interface"+ , "let"+ , "package"+ , "private"+ , "protected"+ , "public"+ , "static"+ , "yield"+ ] translateNamespace :: Name -> [String] translateNamespace (UN _) = [idrNamespace]@@ -162,42 +128,36 @@ translateName (NS name _) = translateName name translateName (MN i name) = translateIdentifier name ++ show i -translateQualifiedName :: Name -> String-translateQualifiedName name =- intercalate "." (translateNamespace name) ++ "." ++ translateName name- translateConstant :: Const -> String translateConstant (I i) = show i-translateConstant (BI i) = "__IDR__.bigInt('" ++ show i ++ "')"+translateConstant (BI i) = "__IDRRT__.bigInt('" ++ show i ++ "')" translateConstant (Fl f) = show f translateConstant (Ch c) = show c translateConstant (Str s) = show s-translateConstant IType = "__IDR__.Int"-translateConstant ChType = "__IDR__.Char"-translateConstant StrType = "__IDR__.String"-translateConstant BIType = "__IDR__.Integer"-translateConstant FlType = "__IDR__.Float"-translateConstant Forgot = "__IDR__.Forgot"+translateConstant IType = "__IDRRT__.Int"+translateConstant ChType = "__IDRRT__.Char"+translateConstant StrType = "__IDRRT__.String"+translateConstant BIType = "__IDRRT__.Integer"+translateConstant FlType = "__IDRRT__.Float"+translateConstant Forgot = "__IDRRT__.Forgot" translateConstant c = "(function(){throw 'Unimplemented Const: " ++ show c ++ "';})()" translateParameterlist = map translateParameter- where translateParameter (MN i name) = name ++ show i- translateParameter (UN name) = name+ where translateParameter (MN i name) = translateIdentifier name ++ show i+ translateParameter (UN name) = translateIdentifier name -translateDeclaration :: NamespaceName -> SDecl -> String-translateDeclaration modname (SFun name params stackSize body) =- modname- ++ "."- ++ translateName name+translateDeclaration :: ([String], SDecl) -> String+translateDeclaration (path, SFun name params stackSize body) =+ intercalate "." (path ++ [translateName name]) ++ " = function(" ++ intercalate "," p ++ "){\n" ++ concatMap assignVar (zip [0..] p) ++ concatMap allocVar [numP..(numP+stackSize-1)] ++ "return "- ++ translateExpression modname body+ ++ translateExpression body ++ ";\n};\n" where numP :: Int@@ -216,32 +176,32 @@ translateVariableName (Loc i) = "__var_" ++ show i -translateExpression :: NamespaceName -> SExp -> String-translateExpression modname (SLet name value body) =+translateExpression :: SExp -> String+translateExpression (SLet name value body) = "(function(" ++ translateVariableName name ++ "){\nreturn "- ++ translateExpression modname body+ ++ translateExpression body ++ ";\n})("- ++ translateExpression modname value+ ++ translateExpression value ++ ")" -translateExpression _ (SConst cst) =+translateExpression (SConst cst) = translateConstant cst -translateExpression _ (SV var) =+translateExpression (SV var) = translateVariableName var -translateExpression modname (SApp False name vars) =+translateExpression (SApp False name vars) = createTailcall $ translateFunctionCall name vars -translateExpression modname (SApp True name vars) =- "new __IDR__.Tailcall("+translateExpression (SApp True name vars) =+ "new __IDRRT__.Tailcall(" ++ "function(){\n" ++ "return " ++ translateFunctionCall name vars ++ ";\n});" -translateExpression _ (SOp op vars)+translateExpression (SOp op vars) | LPlus <- op , (lhs:rhs:_) <- vars = translateBinaryOp "+" lhs rhs | LMinus <- op@@ -329,13 +289,13 @@ | LIntStr <- op , (arg:_) <- vars = "String(" ++ translateVariableName arg ++ ")" | LIntBig <- op- , (arg:_) <- vars = "__IDR__.bigint(" ++ translateVariableName arg ++ ")"+ , (arg:_) <- vars = "__IDRRT__.bigInt(" ++ translateVariableName arg ++ ")" | LBigInt <- op , (arg:_) <- vars = translateVariableName arg ++ ".valueOf()" | LBigStr <- op , (arg:_) <- vars = translateVariableName arg ++ ".toString()" | LStrBig <- op- , (arg:_) <- vars = "__IDR__.bigint(" ++ translateVariableName arg ++ ")"+ , (arg:_) <- vars = "__IDRRT__.bigInt(" ++ translateVariableName arg ++ ")" | LFloatStr <- op , (arg:_) <- vars = "String(" ++ translateVariableName arg ++ ")" | LStrFloat <- op@@ -394,78 +354,117 @@ ++ f ++ translateVariableName rhs -translateExpression _ (SError msg) =+translateExpression (SError msg) = "(function(){throw \'" ++ msg ++ "\';})();" -translateExpression _ (SForeign _ _ "putStr" [(FString, var)]) =- "__IDR__.print(" ++ translateVariableName var ++ ");"+translateExpression (SForeign _ _ "putStr" [(FString, var)]) =+ "__IDRRT__.print(" ++ translateVariableName var ++ ");" -translateExpression _ (SForeign _ _ fun args) =- fun- ++ "("- ++ intercalate "," (map (translateVariableName . snd) args)- ++ ");"+translateExpression (SForeign _ _ fun args)+ | "." `isPrefixOf` fun, "[]=" `isSuffixOf` fun+ , (obj:idx:val:[]) <- args =+ concat [object obj, field, index idx, assign val] -translateExpression modname (SChkCase var cases) =+ | "." `isPrefixOf` fun, "[]" `isSuffixOf` fun+ , (obj:idx:[]) <- args =+ concat [object obj, field, index idx]++ | "." `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]++ | "[]=" == fun+ , (idx:val:[]) <- args =+ concat [array, index idx, assign val]++ | "[]" == fun+ , (idx:[]) <- args =+ array ++ index idx++ | otherwise = fun ++ arguments args+ where+ name = filter (`notElem` "[]=") fun+ method = name+ field = name+ array = name+ object o = translateVariableName (snd o)+ index i = "[" ++ translateVariableName (snd i) ++ "]"+ assign v = '=' : translateVariableName (snd v)+ arguments as =+ '(' : intercalate "," (map (translateVariableName . snd) as) ++ ")"++translateExpression (SChkCase var cases) = "(function(e){\n"- ++ intercalate " else " (map (translateCase modname "e") cases)+ ++ intercalate " else " (map (translateCase "e") cases) ++ "\n})(" ++ translateVariableName var ++ ")" -translateExpression modname (SCase var cases) = +translateExpression (SCase var cases) = "(function(e){\n"- ++ intercalate " else " (map (translateCase modname "e") cases)+ ++ intercalate " else " (map (translateCase "e") cases) ++ "\n})(" ++ translateVariableName var ++ ")" -translateExpression _ (SCon i name vars) =- concat [ "new __IDR__.Con("+translateExpression (SCon i name vars) =+ concat [ "new __IDRRT__.Con(" , show i- , ","- , '\'' : translateQualifiedName name ++ "\',["+ , ",[" , intercalate "," $ map translateVariableName vars , "])" ] -translateExpression modname (SUpdate var e) =- translateVariableName var ++ " = " ++ translateExpression modname e+translateExpression (SUpdate var e) =+ translateVariableName var ++ " = " ++ translateExpression e -translateExpression modname (SProj var i) =+translateExpression (SProj var i) = translateVariableName var ++ ".vars[" ++ show i ++"]" -translateExpression _ SNothing = "null"+translateExpression SNothing = "null" -translateExpression _ e =+translateExpression e = "(function(){throw 'Not yet implemented: " ++ filter (/= '\'') (show e) ++ "';})()" -translateCase :: String -> String -> SAlt -> String-translateCase modname _ (SDefaultCase e) =- createIfBlock "true" (translateExpression modname e)+translateCase :: String -> SAlt -> String+translateCase _ (SDefaultCase e) =+ createIfBlock "true" (translateExpression e) -translateCase modname var (SConstCase ty e)+translateCase var (SConstCase ty e) | ChType <- ty = matchHelper "Char" | StrType <- ty = matchHelper "String" | IType <- ty = matchHelper "Int" | BIType <- ty = matchHelper "Integer" | FlType <- ty = matchHelper "Float"+ | PtrType <- ty = matchHelper "Pointer" | Forgot <- ty = matchHelper "Forgot" where- matchHelper tyName = translateTypeMatch modname var tyName e+ matchHelper tyName = translateTypeMatch var tyName e -translateCase modname var (SConstCase cst@(BI _) e) =+translateCase var (SConstCase cst@(BI _) e) = let cond = var ++ ".equals(" ++ translateConstant cst ++ ")" in- createIfBlock cond (translateExpression modname e)+ createIfBlock cond (translateExpression e) -translateCase modname var (SConstCase cst e) =+translateCase var (SConstCase cst e) = let cond = var ++ " == " ++ translateConstant cst in- createIfBlock cond (translateExpression modname e)+ createIfBlock cond (translateExpression e) -translateCase modname var (SConCase a i name vars e) =- let isCon = var ++ " instanceof __IDR__.Con"+translateCase var (SConCase a i name vars e) =+ let isCon = var ++ " instanceof __IDRRT__.Con" isI = show i ++ " == " ++ var ++ ".i" params = intercalate "," $ map (("__var_" ++) . show) [a..(a+length vars)] args = ".apply(this," ++ var ++ ".vars)"@@ -474,13 +473,13 @@ ++ params ++ "){\nreturn " ++ b ++ "\n})" ++ args cond = intercalate " && " [isCon, isI] in- createIfBlock cond $ f (translateExpression modname e)+ createIfBlock cond $ f (translateExpression e) -translateTypeMatch :: String -> String -> String -> SExp -> String-translateTypeMatch modname var ty exp =- let e = translateExpression modname exp in+translateTypeMatch :: String -> String -> SExp -> String+translateTypeMatch var ty exp =+ let e = translateExpression exp in createIfBlock (var- ++ " instanceof __IDR__.Type && "+ ++ " instanceof __IDRRT__.Type && " ++ var ++ ".type == '"++ ty ++"'") e @@ -490,7 +489,7 @@ ++ ";\n}" createTailcall call =- "__IDR__.tailcall(function(){return " ++ call ++ "})"+ "__IDRRT__.tailcall(function(){return " ++ call ++ "})" translateFunctionCall name vars = concat (intersperse "." $ translateNamespace name)
src/IRTS/Compiler.hs view
@@ -65,15 +65,21 @@ Just f -> liftIO $ writeFile f (dumpDefuns defuns) iLOG "Building output" case checked of- OK c -> case target of- ViaC -> liftIO $ codegenC c f outty hdrs - (concatMap mkObj objs)- (concatMap mkLib libs) NONE- ViaJava -> liftIO $ codegenJava c f outty- Bytecode -> liftIO $ dumpBC c f- ToJavaScript -> liftIO $ codegenJavaScript c f outty+ OK c -> liftIO $ case target of+ ViaC ->+ codegenC c f outty hdrs+ (concatMap mkObj objs)+ (concatMap mkLib libs) NONE+ ViaJava ->+ codegenJava c f outty+ ViaJavaScript ->+ codegenJavaScript JavaScript c f outty+ ViaNode -> + codegenJavaScript Node c f outty++ Bytecode -> dumpBC c f Error e -> fail $ show e - where checkMVs = do i <- get+ where checkMVs = do i <- getIState case idris_metavars i \\ primDefs of [] -> return () ms -> fail $ "There are undefined metavariables: " ++ show ms@@ -91,7 +97,7 @@ allNames :: [Name] -> Name -> Idris [Name] allNames ns n | n `elem` ns = return []-allNames ns n = do i <- get+allNames ns n = do i <- getIState case lookupCtxt Nothing n (idris_callgraph i) of [ns'] -> do more <- mapM (allNames (n:ns)) (map fst (calls ns')) return (nub (n : concat more))@@ -193,7 +199,7 @@ | (P (DCon t a) n _, args) <- unApply tm = irCon env t a n args | (P _ n _, args) <- unApply tm- = do i <- get+ = do i <- getIState args' <- mapM (ir' env) args case getPrim i n args' of Just tm -> return tm@@ -341,8 +347,10 @@ matchableTy ChType = True matchableTy StrType = True - matchableTy W8Type = True- matchableTy W16Type = True+ matchableTy B8Type = True+ matchableTy B16Type = True+ matchableTy B32Type = True+ matchableTy B64Type = True matchableTy _ = False
src/IRTS/Lang.hs view
@@ -40,10 +40,23 @@ | LIntBig | LBigInt | LStrBig | LBigStr | LChInt | LIntCh | LPrintNum | LPrintStr | LReadStr - | LW8 | LW16- - | LW8Plus | LW8Minus | LW8Times- | LW16Plus | LW16Minus | LW16Times+ | LB8Lt | LB8Lte | LB8Eq | LB8Gt | LB8Gte+ | LB8Plus | LB8Minus | LB8Times | LB8UDiv | LB8SDiv | LB8URem | LB8SRem+ | LB8Shl | LB8LShr | LB8AShr | LB8And | LB8Or | LB8Xor | LB8Compl+ | LB8Z16 | LB8Z32 | LB8Z64 | LB8S16 | LB8S32 | LB8S64 -- Zero/Sign extension+ | LB16Lt | LB16Lte | LB16Eq | LB16Gt | LB16Gte+ | LB16Plus | LB16Minus | LB16Times | LB16UDiv | LB16SDiv | LB16URem | LB16SRem+ | LB16Shl | LB16LShr | LB16AShr | LB16And | LB16Or | LB16Xor | LB16Compl+ | LB16Z32 | LB16Z64 | LB16S32 | LB16S64 | LB16T8 -- and Truncation+ | LB32Lt | LB32Lte | LB32Eq | LB32Gt | LB32Gte+ | LB32Plus | LB32Minus | LB32Times | LB32UDiv | LB32SDiv | LB32URem | LB32SRem+ | LB32Shl | LB32LShr | LB32AShr | LB32And | LB32Or | LB32Xor | LB32Compl+ | LB32Z64 | LB32S64 | LB32T8 | LB32T16+ | LB64Lt | LB64Lte | LB64Eq | LB64Gt | LB64Gte+ | LB64Plus | LB64Minus | LB64Times | LB64UDiv | LB64SDiv | LB64URem | LB64SRem+ | LB64Shl | LB64LShr | LB64AShr | LB64And | LB64Or | LB64Xor | LB64Compl+ | LB64T8 | LB64T16 | LB64T32+ | LIntB8 | LIntB16 | LIntB32 | LIntB64 | LB32Int | LFExp | LFLog | LFSin | LFCos | LFTan | LFASin | LFACos | LFATan | LFSqrt | LFFloor | LFCeil
src/Idris/AbsSyntax.hs view
@@ -26,57 +26,57 @@ getContext :: Idris Context-getContext = do i <- get; return (tt_ctxt i)+getContext = do i <- getIState; return (tt_ctxt i) getObjectFiles :: Idris [FilePath]-getObjectFiles = do i <- get; return (idris_objs i)+getObjectFiles = do i <- getIState; return (idris_objs i) addObjectFile :: FilePath -> Idris ()-addObjectFile f = do i <- get; put (i { idris_objs = f : idris_objs i })+addObjectFile f = do i <- getIState; putIState $ i { idris_objs = f : idris_objs i } getLibs :: Idris [String]-getLibs = do i <- get; return (idris_libs i)+getLibs = do i <- getIState; return (idris_libs i) addLib :: String -> Idris ()-addLib f = do i <- get; put (i { idris_libs = f : idris_libs i })+addLib f = do i <- getIState; putIState $ i { idris_libs = f : idris_libs i } addHdr :: String -> Idris ()-addHdr f = do i <- get; put (i { idris_hdrs = f : idris_hdrs i })+addHdr f = do i <- getIState; putIState $ i { idris_hdrs = f : idris_hdrs i } totcheck :: (FC, Name) -> Idris ()-totcheck n = do i <- get; put (i { idris_totcheck = idris_totcheck i ++ [n] })+totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] } setFlags :: Name -> [FnOpt] -> Idris ()-setFlags n fs = do i <- get; put (i { idris_flags = addDef n fs (idris_flags i) }) +setFlags n fs = do i <- getIState; putIState $ i { idris_flags = addDef n fs (idris_flags i) } setAccessibility :: Name -> Accessibility -> Idris () setAccessibility n a - = do i <- get+ = do i <- getIState let ctxt = setAccess n a (tt_ctxt i)- put (i { tt_ctxt = ctxt })+ putIState $ i { tt_ctxt = ctxt } setTotality :: Name -> Totality -> Idris () setTotality n a - = do i <- get+ = do i <- getIState let ctxt = setTotal n a (tt_ctxt i)- put (i { tt_ctxt = ctxt })+ putIState $ i { tt_ctxt = ctxt } getTotality :: Name -> Idris Totality getTotality n - = do i <- get+ = do i <- getIState case lookupTotal n (tt_ctxt i) of [t] -> return t _ -> return (Total []) addToCG :: Name -> CGInfo -> Idris () addToCG n cg - = do i <- get- put (i { idris_callgraph = addDef n cg (idris_callgraph i) })+ = do i <- getIState+ putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) } addDocStr :: Name -> String -> Idris () addDocStr n doc - = do i <- get- put (i { idris_docstrings = addDef n doc (idris_docstrings i) })+ = do i <- getIState+ putIState $ i { idris_docstrings = addDef n doc (idris_docstrings i) } addToCalledG :: Name -> [Name] -> Idris () addToCalledG n ns = return () -- TODO@@ -87,13 +87,13 @@ addInstance :: Bool -> Name -> Name -> Idris () addInstance int n i - = do ist <- get+ = do ist <- getIState case lookupCtxt Nothing n (idris_classes ist) of [CI a b c d ins] -> do let cs = addDef n (CI a b c d (addI i ins)) (idris_classes ist)- put (ist { idris_classes = cs })+ putIState $ ist { idris_classes = cs } _ -> do let cs = addDef n (CI (MN 0 "none") [] [] [] [i]) (idris_classes ist)- put (ist { idris_classes = cs })+ putIState $ ist { idris_classes = cs } where addI i ins | int = i : ins | chaser n = ins ++ [i] | otherwise = insI i ins@@ -107,45 +107,45 @@ addClass :: Name -> ClassInfo -> Idris () addClass n i - = do ist <- get+ = do ist <- getIState let i' = case lookupCtxt Nothing n (idris_classes ist) of [c] -> c { class_instances = class_instances i } _ -> i- put (ist { idris_classes = addDef n i' (idris_classes ist) }) + putIState $ ist { idris_classes = addDef n i' (idris_classes ist) } addIBC :: IBCWrite -> Idris () addIBC ibc@(IBCDef n) - = do i <- get+ = do i <- getIState when (notDef (ibc_write i)) $- put (i { ibc_write = ibc : ibc_write i })+ putIState $ i { ibc_write = ibc : ibc_write i } where notDef [] = True notDef (IBCDef n': is) | n == n' = False notDef (_ : is) = notDef is-addIBC ibc = do i <- get; put (i { ibc_write = ibc : ibc_write i }) +addIBC ibc = do i <- getIState; putIState $ i { ibc_write = ibc : ibc_write i } clearIBC :: Idris ()-clearIBC = do i <- get; put (i { ibc_write = [] })+clearIBC = do i <- getIState; putIState $ i { ibc_write = [] } getHdrs :: Idris [String]-getHdrs = do i <- get; return (idris_hdrs i)+getHdrs = do i <- getIState; return (idris_hdrs i) setErrLine :: Int -> Idris ()-setErrLine x = do i <- get;+setErrLine x = do i <- getIState; case (errLine i) of- Nothing -> put (i { errLine = Just x })+ Nothing -> putIState $ i { errLine = Just x } Just _ -> return () clearErr :: Idris ()-clearErr = do i <- get- put (i { errLine = Nothing })+clearErr = do i <- getIState+ putIState $ i { errLine = Nothing } getSO :: Idris (Maybe String)-getSO = do i <- get+getSO = do i <- getIState return (compiled_so i) setSO :: Maybe String -> Idris ()-setSO s = do i <- get- put (i { compiled_so = s })+setSO s = do i <- getIState+ putIState $ (i { compiled_so = s }) getIState :: Idris IState getIState = get@@ -154,9 +154,9 @@ putIState = put getName :: Idris Int-getName = do i <- get;+getName = do i <- getIState; let idx = idris_name i;- put (i { idris_name = idx + 1 })+ putIState $ (i { idris_name = idx + 1 }) return idx checkUndefined :: FC -> Name -> Idris ()@@ -175,24 +175,24 @@ _ -> return True setContext :: Context -> Idris ()-setContext ctxt = do i <- get; put (i { tt_ctxt = ctxt } )+setContext ctxt = do i <- getIState; putIState $ (i { tt_ctxt = ctxt } ) updateContext :: (Context -> Context) -> Idris ()-updateContext f = do i <- get; put (i { tt_ctxt = f (tt_ctxt i) } )+updateContext f = do i <- getIState; putIState $ (i { tt_ctxt = f (tt_ctxt i) } ) addConstraints :: FC -> (Int, [UConstraint]) -> Idris () addConstraints fc (v, cs)- = do i <- get+ = do i <- getIState let ctxt = tt_ctxt i let ctxt' = ctxt { uconstraints = cs ++ uconstraints ctxt, next_tvar = v } let ics = zip cs (repeat fc) ++ idris_constraints i- put (i { tt_ctxt = ctxt', idris_constraints = ics })+ putIState $ i { tt_ctxt = ctxt', idris_constraints = ics } addDeferred :: [(Name, Type)] -> Idris () addDeferred ns = do mapM_ (\(n, t) -> updateContext (addTyDecl n (tidyNames [] t))) ns- i <- get- put (i { idris_metavars = map fst ns ++ idris_metavars i })+ i <- getIState+ putIState $ i { idris_metavars = map fst ns ++ idris_metavars i } where tidyNames used (Bind (MN i x) b sc) = let n' = uniqueName (UN x) used in Bind n' b $ tidyNames (n':used) sc@@ -202,8 +202,8 @@ tidyNames used b = b solveDeferred :: Name -> Idris ()-solveDeferred n = do i <- get- put (i { idris_metavars = idris_metavars i \\ [n] })+solveDeferred n = do i <- getIState+ putIState $ i { idris_metavars = idris_metavars i \\ [n] } iputStrLn :: String -> Idris () iputStrLn = liftIO . putStrLn@@ -212,164 +212,164 @@ iWarn fc err = liftIO $ putStrLn (show fc ++ ":" ++ err) setLogLevel :: Int -> Idris ()-setLogLevel l = do i <- get+setLogLevel l = do i <- getIState let opts = idris_options i let opt' = opts { opt_logLevel = l }- put (i { idris_options = opt' } )+ putIState $ i { idris_options = opt' } setCmdLine :: [Opt] -> Idris ()-setCmdLine opts = do i <- get+setCmdLine opts = do i <- getIState let iopts = idris_options i- put (i { idris_options = iopts { opt_cmdline = opts } })+ putIState $ i { idris_options = iopts { opt_cmdline = opts } } getDumpDefun :: Idris (Maybe FilePath)-getDumpDefun = do i <- get+getDumpDefun = do i <- getIState return $ findC (opt_cmdline (idris_options i)) where findC [] = Nothing findC (DumpDefun x : _) = Just x findC (_ : xs) = findC xs getDumpCases :: Idris (Maybe FilePath)-getDumpCases = do i <- get+getDumpCases = do i <- getIState return $ findC (opt_cmdline (idris_options i)) where findC [] = Nothing findC (DumpCases x : _) = Just x findC (_ : xs) = findC xs logLevel :: Idris Int-logLevel = do i <- get+logLevel = do i <- getIState return (opt_logLevel (idris_options i)) setErrContext :: Bool -> Idris ()-setErrContext t = do i <- get+setErrContext t = do i <- getIState let opts = idris_options i let opt' = opts { opt_errContext = t }- put (i { idris_options = opt' })+ putIState $ i { idris_options = opt' } errContext :: Idris Bool-errContext = do i <- get+errContext = do i <- getIState return (opt_errContext (idris_options i)) useREPL :: Idris Bool-useREPL = do i <- get+useREPL = do i <- getIState return (opt_repl (idris_options i)) setREPL :: Bool -> Idris ()-setREPL t = do i <- get+setREPL t = do i <- getIState let opts = idris_options i let opt' = opts { opt_repl = t }- put (i { idris_options = opt' })+ putIState $ i { idris_options = opt' } setTarget :: Target -> Idris ()-setTarget t = do i <- get+setTarget t = do i <- getIState let opts = idris_options i let opt' = opts { opt_target = t }- put (i { idris_options = opt' })+ putIState $ i { idris_options = opt' } target :: Idris Target-target = do i <- get+target = do i <- getIState return (opt_target (idris_options i)) setOutputTy :: OutputType -> Idris ()-setOutputTy t = do i <- get+setOutputTy t = do i <- getIState let opts = idris_options i let opt' = opts { opt_outputTy = t }- put (i { idris_options = opt' })+ putIState $ i { idris_options = opt' } outputTy :: Idris OutputType-outputTy = do i <- get+outputTy = do i <- getIState return $ opt_outputTy $ idris_options i verbose :: Idris Bool-verbose = do i <- get+verbose = do i <- getIState return (opt_verbose (idris_options i)) setVerbose :: Bool -> Idris ()-setVerbose t = do i <- get+setVerbose t = do i <- getIState let opts = idris_options i let opt' = opts { opt_verbose = t }- put (i { idris_options = opt' })+ putIState $ i { idris_options = opt' } typeInType :: Idris Bool-typeInType = do i <- get+typeInType = do i <- getIState return (opt_typeintype (idris_options i)) setTypeInType :: Bool -> Idris ()-setTypeInType t = do i <- get+setTypeInType t = do i <- getIState let opts = idris_options i let opt' = opts { opt_typeintype = t }- put (i { idris_options = opt' })+ putIState $ i { idris_options = opt' } coverage :: Idris Bool-coverage = do i <- get+coverage = do i <- getIState return (opt_coverage (idris_options i)) setCoverage :: Bool -> Idris ()-setCoverage t = do i <- get+setCoverage t = do i <- getIState let opts = idris_options i let opt' = opts { opt_coverage = t }- put (i { idris_options = opt' })+ putIState $ i { idris_options = opt' } setIBCSubDir :: FilePath -> Idris ()-setIBCSubDir fp = do i <- get+setIBCSubDir fp = do i <- getIState let opts = idris_options i let opt' = opts { opt_ibcsubdir = fp }- put (i { idris_options = opt' })+ putIState $ i { idris_options = opt' } valIBCSubDir :: IState -> Idris FilePath valIBCSubDir i = return (opt_ibcsubdir (idris_options i)) addImportDir :: FilePath -> Idris ()-addImportDir fp = do i <- get+addImportDir fp = do i <- getIState let opts = idris_options i let opt' = opts { opt_importdirs = fp : opt_importdirs opts }- put (i { idris_options = opt' })+ putIState $ i { idris_options = opt' } setImportDirs :: [FilePath] -> Idris ()-setImportDirs fps = do i <- get+setImportDirs fps = do i <- getIState let opts = idris_options i let opt' = opts { opt_importdirs = fps }- put (i { idris_options = opt' })+ putIState $ i { idris_options = opt' } allImportDirs :: IState -> Idris [FilePath] allImportDirs i = do let optdirs = opt_importdirs (idris_options i) return ("." : optdirs) impShow :: Idris Bool-impShow = do i <- get+impShow = do i <- getIState return (opt_showimp (idris_options i)) setImpShow :: Bool -> Idris ()-setImpShow t = do i <- get+setImpShow t = do i <- getIState let opts = idris_options i let opt' = opts { opt_showimp = t }- put (i { idris_options = opt' })+ putIState $ i { idris_options = opt' } logLvl :: Int -> String -> Idris ()-logLvl l str = do i <- get+logLvl l str = do i <- getIState let lvl = opt_logLevel (idris_options i) when (lvl >= l) $ do liftIO (putStrLn str)- put (i { idris_log = idris_log i ++ str ++ "\n" } )+ putIState $ i { idris_log = idris_log i ++ str ++ "\n" } cmdOptType :: Opt -> Idris Bool-cmdOptType x = do i <- get+cmdOptType x = do i <- getIState return $ x `elem` opt_cmdline (idris_options i) iLOG :: String -> Idris () iLOG = logLvl 1 noErrors :: Idris Bool-noErrors = do i <- get+noErrors = do i <- getIState case errLine i of Nothing -> return True _ -> return False setTypeCase :: Bool -> Idris ()-setTypeCase t = do i <- get+setTypeCase t = do i <- getIState let opts = idris_options i let opt' = opts { opt_typecase = t }- put (i { idris_options = opt' })+ putIState $ i { idris_options = opt' } -- For inferring types of things@@ -634,8 +634,8 @@ let statics' = nub $ map fst statics ++ filter (\x -> not (elem x dnames)) stnames let stpos = staticList statics' tm- i <- get- put (i { idris_statics = addDef n stpos (idris_statics i) })+ i <- getIState+ putIState $ i { idris_statics = addDef n stpos (idris_statics i) } addIBC (IBCStatic n) where initStatics (Bind n (Pi ty) sc) (PPi p _ _ s)@@ -659,14 +659,14 @@ implicit' :: SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm implicit' syn ignore n ptm - = do i <- get+ = do i <- getIState let (tm', impdata) = implicitise syn ignore i ptm -- let (tm'', spos) = findStatics i tm'- put (i { idris_implicits = addDef n impdata (idris_implicits i) })+ putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) } addIBC (IBCImp n) logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata) -- i <- get--- put (i { idris_statics = addDef n spos (idris_statics i) })+-- putIState $ i { idris_statics = addDef n spos (idris_statics i) } return tm' implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
src/Idris/AbsSyntaxTree.hs view
@@ -136,11 +136,15 @@ -- The monad for the main REPL - reading and processing files and updating -- global state (hence the IO inner monad).-type Idris = StateT IState (InputT IO)+type Idris = StateT IState IO -- Commands in the REPL -data Target = ViaC | ViaJava | Bytecode | ToJavaScript+data Target = ViaC+ | ViaJava+ | ViaNode+ | ViaJavaScript+ | Bytecode deriving (Show, Eq) data Command = Quit@@ -524,6 +528,7 @@ -- The priority gives a hint as to elaboration order. Best to elaborate -- things early which will help give a more concrete type to other -- variables, e.g. a before (interpTy a).+-- TODO: priority no longer serves any purpose, drop it! data PArg' t = PImp { priority :: Int, lazyarg :: Bool, pname :: Name, getTm :: t,@@ -579,7 +584,9 @@ !-} -data TypeInfo = TI { con_names :: [Name], codata :: Bool }+data TypeInfo = TI { con_names :: [Name], + codata :: Bool,+ param_pos :: [Int] } deriving Show {-! deriving instance Binary TypeInfo
+ src/Idris/Completion.hs view
@@ -0,0 +1,143 @@+module Idris.Completion (replCompletion, proverCompletion) where++import Core.Evaluate (ctxtAlist)+import Core.TT++import Idris.AbsSyntaxTree++import Control.Monad.State.Strict++import Data.List+import Data.Maybe++import System.Console.Haskeline++-- TODO: add specific classes of identifiers to complete, fx metavariables+-- | A specification of the arguments that REPL commands can take+data CmdArg = ExprArg -- ^ The command takes an expression+ | NameArg -- ^ The command takes a name+ | FileArg -- ^ The command takes a file+ | ModuleArg -- ^ The command takes a module name+ | OptionArg -- ^ The command takes an option++-- | Information about how to complete the various commands+cmdArgs :: [(String, CmdArg)]+cmdArgs = [ (":t", ExprArg)+ , (":miss", NameArg)+ , (":missing", NameArg)+ , (":i", NameArg)+ , (":info", NameArg)+ , (":total", NameArg)+ , (":l", FileArg)+ , (":load", FileArg)+ , (":m", ModuleArg) -- NOTE: Argumentless form is a different command+ , (":p", NameArg)+ , (":prove", NameArg)+ , (":a", NameArg)+ , (":addproof", NameArg)+ , (":rmproof", NameArg)+ , (":showproof", NameArg)+ , (":c", FileArg)+ , (":compile", FileArg)+ , (":js", FileArg)+ , (":javascript", FileArg)+ , (":set", OptionArg)+ , (":unset", OptionArg)+ ]+commands = map fst cmdArgs++-- | A specification of the arguments that tactics can take+data TacticArg = NameTArg -- ^ Names: n1, n2, n3, ... n+ | ExprTArg+ | AltsTArg++-- | A list of available tactics and their argument requirements+tacticArgs :: [(String, Maybe TacticArg)]+tacticArgs = [ ("intro", Nothing)+ , ("intros", Nothing)+ , ("refine", Just ExprTArg)+ , ("rewrite", Just ExprTArg)+ , ("let", Nothing) -- FIXME syntax for let+ , ("focus", Just ExprTArg)+ , ("exact", Just ExprTArg)+ , ("reflect", Just ExprTArg)+ , ("try", Just AltsTArg)+ ] ++ map (\x -> (x, Nothing)) [+ "intro", "intros", "compute", "trivial", "solve", "attack",+ "state", "term", "undo", "qed", "abandon", ":q"+ ]+tactics = map fst tacticArgs++-- | Convert a name into a string usable for completion. Filters out names+-- that users probably don't want to see.+nameString :: Name -> Maybe String+nameString (UN ('@':_)) = Nothing+nameString (UN ('#':_)) = Nothing+nameString (UN n) = Just n+nameString (NS n _) = nameString n+nameString _ = Nothing++-- FIXME: Respect module imports+-- | Get the user-visible names from the current interpreter state.+names :: Idris[String]+names = do i <- get+ let ctxt = tt_ctxt i+ return $ nub $ mapMaybe (nameString . fst) $ ctxtAlist ctxt+++modules :: Idris [String]+modules = do i <- get+ return $ map show $ imported i++++completeWith :: [String] -> String -> [Completion]+completeWith ns n = if uniqueExists+ then [simpleCompletion n]+ else map simpleCompletion prefixMatches+ where prefixMatches = filter (isPrefixOf n) ns+ uniqueExists = n `elem` prefixMatches++completeName :: [String] -> String -> Idris [Completion]+completeName extra n = do ns <- names+ return $ completeWith (extra ++ ns) n++completeExpr :: [String] -> CompletionFunc Idris+completeExpr extra = completeWord Nothing " \t" (completeName extra)++completeOption :: CompletionFunc Idris+completeOption = completeWord Nothing " \t" completeOpt+ where completeOpt = return . (completeWith ["errorcontext", "showimplicits"])++isWhitespace :: Char -> Bool+isWhitespace = (flip elem) " \t\n"++-- | Get the completion function for a particular command+completeCmd :: String -> CompletionFunc Idris+completeCmd cmd (prev, next) = fromMaybe completeCmdName $ fmap completeArg $ lookup cmd cmdArgs+ where completeArg FileArg = completeFilename (prev, next)+ completeArg NameArg = completeExpr [] (prev, next) -- FIXME only complete one name+ completeArg OptionArg = completeOption (prev, next)+ completeArg ModuleArg = noCompletion (prev, next) -- FIXME do later+ completeArg ExprArg = completeExpr [] (prev, next)+ completeCmdName = return $ ("", completeWith commands cmd)++replCompletion :: CompletionFunc Idris+replCompletion (prev, next) = case firstWord of+ ':':cmdName -> completeCmd (':':cmdName) (prev, next)+ _ -> completeExpr [] (prev, next)+ where firstWord = fst $ break isWhitespace $ dropWhile isWhitespace $ reverse prev+++completeTactic :: [String] -> String -> CompletionFunc Idris+completeTactic as tac (prev, next) = fromMaybe completeTacName $ fmap completeArg $ lookup tac tacticArgs+ where completeTacName = return $ ("", completeWith tactics tac)+ completeArg Nothing = noCompletion (prev, next)+ completeArg (Just NameTArg) = noCompletion (prev, next) -- this is for binding new names!+ completeArg (Just ExprTArg) = completeExpr as (prev, next)+ completeArg (Just AltsTArg) = noCompletion (prev, next) -- TODO+++proverCompletion :: [String] -> CompletionFunc Idris+proverCompletion assumptions (prev, next) = completeTactic assumptions firstWord (prev, next)+ where firstWord = fst $ break isWhitespace $ dropWhile isWhitespace $ reverse prev
src/Idris/Coverage.hs view
@@ -33,23 +33,23 @@ -- covering...) mkPatTm :: PTerm -> Idris Term-mkPatTm t = do i <- get+mkPatTm t = do i <- getIState let timp = addImpl' True [] [] i t evalStateT (toTT timp) 0 where- toTT (PRef _ n) = do i <- lift $ get+ toTT (PRef _ n) = do i <- lift getIState case lookupDef Nothing n (tt_ctxt i) of [TyDecl nt _] -> return $ P nt n Erased _ -> return $ P Ref n Erased toTT (PApp _ t args) = do t' <- toTT t args' <- mapM (toTT . getTm) args return $ mkApp t' args'- toTT _ = do v <- get + toTT _ = do v <- get put (v + 1) return (P Bound (MN v "imp") Erased) mkPTerm :: Name -> [TT Name] -> Idris PTerm-mkPTerm f args = do i <- get+mkPTerm f args = do i <- getIState let fapp = mkApp (P Bound f Erased) (map eraseName args) return $ delab i fapp where eraseName (App f a) = App (eraseName f) (eraseName a)@@ -90,7 +90,7 @@ dropDefault [] = [] expandTree :: SC -> Idris SC-expandTree (Case n alts) = do i <- get+expandTree (Case n alts) = do i <- getIState as <- expandAlts i (dropDefault alts) (getDefault alts) alts' <- mapM expandTreeA as@@ -110,8 +110,8 @@ | (TyDecl c@(DCon _ arity) ty : _) <- lookupDef Nothing n (tt_ctxt i) = do let tyn = getTy n (tt_ctxt i) case lookupCtxt Nothing tyn (idris_datatypes i) of- (TI ns _ : _) -> do let ps = map mkPat ns- return $ addAlts ps (altsFor all) all+ (TI ns _ _: _) -> do let ps = map mkPat ns+ return $ addAlts ps (altsFor all) all _ -> return all where altsFor [] = []@@ -164,7 +164,9 @@ (p : _) -> p _ -> repeat (pexp Placeholder) let tryclauses = mkClauses parg all_args- let new = mnub i $ filter (noMatch i) tryclauses + logLvl 2 $ show (length tryclauses) ++ " initially to check"+ let new = mnub i $ filter (noMatch i) tryclauses+ logLvl 1 $ show (length new) ++ " clauses to check for impossibility" logLvl 7 $ "New clauses: \n" ++ showSep "\n" (map (showImp True) new) -- ++ " from:\n" ++ showSep "\n" (map (showImp True) tryclauses) return new@@ -202,13 +204,18 @@ as' <- mkArg as return (a':as') +fnub xs = fnub' [] xs where+ fnub' acc (x : xs) | x `elem` acc = fnub' acc xs+ | otherwise = fnub' (x : acc) xs+ fnub' acc [] = acc+ -- FIXME: Just look for which one is the deepest, then generate all -- possibilities up to that depth. genAll :: IState -> [PTerm] -> [PTerm] genAll i args = case filter (/=Placeholder) $ concatMap otherPats (nub args) of [] -> [Placeholder]- xs -> xs+ xs -> nub xs where conForm (PApp _ (PRef fc n) _) = isConName Nothing n (tt_ctxt i) conForm (PRef fc n) = isConName Nothing n (tt_ctxt i)@@ -225,7 +232,7 @@ let p = PApp fc (PRef fc n) (zipWith upd xs' xs) let tyn = getTy n (tt_ctxt i) case lookupCtxt Nothing tyn (idris_datatypes i) of- (TI ns _ : _) -> p : map (mkPat fc) (ns \\ [n])+ (TI ns _ _ : _) -> p : map (mkPat fc) (ns \\ [n]) _ -> [p] ops fc n arg o = return Placeholder @@ -300,14 +307,14 @@ cotype ty | (P _ t _, _) <- unApply (getRetTy ty) = case lookupCtxt Nothing t (idris_datatypes i) of- [TI _ True] -> True+ [TI _ True _] -> True _ -> False | otherwise = False calcTotality :: [Name] -> FC -> Name -> [([Name], Term, Term)] -> Idris Totality calcTotality path fc n pats - = do i <- get+ = do i <- getIState let opts = case lookupCtxt Nothing n (idris_flags i) of [fs] -> fs _ -> []@@ -370,7 +377,7 @@ totalityError t = tclift $ tfail (At fc (Msg (show n ++ " is " ++ show t))) warnPartial n t- = do i <- get+ = do i <- getIState case lookupDef Nothing n (tt_ctxt i) of [x] -> do iputStrLn $ show fc ++ ":Warning - " ++ show n ++ " is " ++ show t @@ -399,11 +406,11 @@ buildSCG :: (FC, Name) -> Idris () buildSCG (_, n) = do- ist <- get+ ist <- getIState case lookupCtxt Nothing n (idris_callgraph ist) of [cg] -> case lookupDef Nothing n (tt_ctxt ist) of [CaseOp _ _ _ _ _ args sc _ _] -> - do logLvl 5 $ "Building SCG for " ++ show n ++ " from\n" + do logLvl 3 $ "Building SCG for " ++ show n ++ " from\n" ++ show sc let newscg = buildSCG' ist sc args logLvl 5 $ show newscg@@ -495,11 +502,12 @@ checkSizeChange :: Name -> Idris Totality checkSizeChange n = do- ist <- get+ ist <- getIState case lookupCtxt Nothing n (idris_callgraph ist) of [cg] -> do let ms = mkMultiPaths ist [] (scg cg)- logLvl 6 ("Multipath for " ++ show n ++ ":\n" +++ logLvl 5 ("Multipath for " ++ show n ++ ":\n" ++ "from " ++ show (scg cg) ++ "\n" +++ show (length ms) ++ "\n" ++ showSep "\n" (map show ms)) logLvl 6 (show cg) -- every multipath must have an infinitely descending @@ -507,7 +515,8 @@ -- also need to checks functions called are all total -- (Unchecked is okay as we'll spot problems here) let tot = map (checkMP ist (length (argsdef cg))) ms- logLvl 3 $ "Paths for " ++ show n ++ " yield " ++ (show tot)+ logLvl 4 $ "Generated " ++ show (length tot) ++ " paths"+ logLvl 6 $ "Paths for " ++ show n ++ " yield " ++ (show tot) return (noPartial tot) [] -> do logLvl 5 $ "No paths for " ++ show n return Unchecked@@ -520,10 +529,11 @@ = concat (map extend cg) where extend (nextf, args) | (nextf, args) `elem` path = [ reverse ((nextf, args) : path) ]- | otherwise + | [Unchecked] <- lookupTotal nextf (tt_ctxt ist) = case lookupCtxt Nothing nextf (idris_callgraph ist) of [ncg] -> mkMultiPaths ist ((nextf, args) : path) (scg ncg) _ -> [ reverse ((nextf, args) : path) ]+ | otherwise = [ reverse ((nextf, args) : path) ] -- do (nextf, args) <- cg -- if ((nextf, args) `elem` path)@@ -569,7 +579,7 @@ Total [] else Partial (Mutual (map (fst . fst) path ++ [f])) | [Unchecked] <- lookupTotal f (tt_ctxt ist) =- let argspos = zip nextargs [0..] in+ let argspos = collapseNothing (zip nextargs [0..]) in collapse' Unchecked $ do (a, pos) <- argspos case a of@@ -593,9 +603,16 @@ _ -> trace ("Shouldn't happen " ++ show e) $ return (Partial Itself) else return Unchecked- | [Total _] <- lookupTotal f (tt_ctxt ist) = Unchecked+ | [Total a] <- lookupTotal f (tt_ctxt ist) = Total a | [Partial _] <- lookupTotal f (tt_ctxt ist) = Partial (Other [f]) | otherwise = Unchecked++collapseNothing ((Nothing, _) : xs) + = filter (\ (x, _) -> case x of+ Nothing -> False+ _ -> True) xs+collapseNothing (x : xs) = x : collapseNothing xs+collapseNothing [] = [] noPartial (Partial p : xs) = Partial p noPartial (_ : xs) = noPartial xs
src/Idris/DataOpts.hs view
@@ -48,8 +48,8 @@ guarded :: Term -> [Int] guarded t@(App f a)- | (P (TCon _ _) _ _, args) <- unApply t- = mapMaybe isF args ++ concatMap guarded args+-- | (P (TCon _ _) _ _, args) <- unApply t+-- = mapMaybe isF args ++ concatMap guarded args | (P (DCon _ _) _ _, args) <- unApply t = mapMaybe isF args ++ concatMap guarded args guarded t = mapMaybe isF [t]
src/Idris/ElabDecls.hs view
@@ -44,7 +44,7 @@ n = liftname info n_in in -} do checkUndefined fc n ctxt <- getContext- i <- get+ i <- getIState logLvl 3 $ show n ++ " pre-type " ++ showImp True ty' ty' <- implicit syn n ty' let ty = addImpl i ty'@@ -67,7 +67,7 @@ let (t, _) = unApply (getRetTy nty') let corec = case t of P _ rcty _ -> case lookupCtxt Nothing rcty (idris_datatypes i) of- [TI _ True] -> True+ [TI _ True _] -> True _ -> False _ -> False let opts' = if corec then (Coinductive : opts) else opts@@ -91,8 +91,8 @@ fty <- case lookupTy Nothing n ctxt of [] -> tclift $ tfail $ (At fc (NoTypeDecl n)) -- can't happen! [ty] -> return ty- ist <- get- let (ap, _) = unApply (getRetTy fty)+ ist <- getIState+ let (ap, _) = unApply (getRetTy (normalise ctxt [] fty)) logLvl 5 $ "Checking collapsibility of " ++ show (ap, fty) let postOK = case ap of P _ tn _ -> case lookupCtxt Nothing tn@@ -110,7 +110,7 @@ = do iLOG (show (fc, doc)) checkUndefined fc n ctxt <- getContext- i <- get+ 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)) []@@ -126,7 +126,7 @@ = do iLOG (show fc) undef <- isUndefined fc n ctxt <- getContext- i <- get+ 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)) []@@ -140,8 +140,11 @@ when undef $ updateContext (addTyDecl n cty) cons <- mapM (elabCon info syn n codata) dcons ttag <- getName- i <- get- put (i { idris_datatypes = addDef n (TI (map fst cons) codata)+ i <- getIState+ let as = map (const Nothing) (getArgTys cty) + let params = findParams (zip as (repeat True)) (map snd cons)+ logLvl 2 $ "Parameters : " ++ show params+ putIState (i { idris_datatypes = addDef n (TI (map fst cons) codata params) (idris_datatypes i) }) addIBC (IBCDef n) addIBC (IBCData n)@@ -150,13 +153,42 @@ collapseCons n cons updateContext (addDatatype (Data n ttag cty cons)) mapM_ (checkPositive n) cons+ where + -- parameters are names which are unchanged across the structure,+ -- which appear exactly once in the return type of a constructor+ findParams :: [(Maybe Name, Bool)] -> [Type] -> [Int]+ findParams ps [] = mapMaybe (\ ((x, y), n) ->+ if y then Just n else Nothing)+ (zip ps [0..])+ findParams ps (t : ts) = findParams (updateParams ps t) ts + updateParams ps (Bind n (Pi t) sc) + = updateParams (updateParams ps (instantiate (P Bound n t) sc)) t+ updateParams ps tm@(App f a)+ | (P _ fn _, args) <- unApply tm+ = if fn == n+ then updateParamsA ps args (tail args)+ else updateParams (updateParams ps f) a+ | otherwise = updateParams (updateParams ps f) a+ updateParams ps _ = ps++ updateParamsA ((mn, _) : ns) (p@(P _ n' _) : args) all+ | n' `elem` concatMap freeNames all+ = (mn, False) : updateParamsA ns args (p : all)+ updateParamsA ((Nothing, b) : ns) (p@(P _ n' _) : args) all+ = (Just n', b) : updateParamsA ns args (p : all)+ updateParamsA ((Just p, b) : ns) (tm@(P _ n' _) : args) all+ = (Just n', b && p == n') : updateParamsA ns args (tm : all)+ updateParamsA ((mn, _) : ns) (p : args) all+ = (mn, False) : updateParamsA ns args (p : all)+ updateParamsA ps args all = ps+ elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name -> PTerm -> String -> Name -> PTerm -> Idris () elabRecord info syn doc fc tyn ty cdoc cn cty = do elabData info syn doc fc False (PDatadecl tyn ty [(cdoc, cn, cty, fc)]) cty' <- implicit syn cn cty- i <- get+ i <- getIState cty <- case lookupTy Nothing cn (tt_ctxt i) of [t] -> return (delab i t) _ -> fail "Something went inexplicably wrong"@@ -181,13 +213,13 @@ isNonImp _ = Nothing tryElabDecl info (fn, ty, val)- = do i <- get+ = do i <- getIState idrisCatch (do elabDecl' EAll info ty elabDecl' EAll info val) (\v -> do iputStrLn $ show fc ++ ":Warning - can't generate setter for " ++ show fn ++ " (" ++ show ty ++ ")"- put i)+ putIState i) getImplB k (PPi (Imp l s _) n Placeholder sc) = getImplB k sc@@ -265,7 +297,7 @@ elabCon info syn tn codata (doc, n, t_in, fc) = do checkUndefined fc n ctxt <- getContext- i <- get+ 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@@ -311,7 +343,7 @@ (zip [0..] cs) -- if the return type of 'ty' is collapsible, the optimised version should -- just do nothing- ist <- get+ ist <- getIState let (ap, _) = unApply (getRetTy fty) logLvl 5 $ "Checking collapsibility of " ++ show (ap, fty) -- FIXME: Really ought to only do this for total functions!@@ -322,17 +354,17 @@ _ -> False _ -> False solveDeferred n- ist <- get+ ist <- getIState when doNothing $ case lookupCtxt Nothing n (idris_optimisation ist) of [oi] -> do let opts = addDef n (oi { collapsible = True }) (idris_optimisation ist)- put (ist { idris_optimisation = opts })+ putIState (ist { idris_optimisation = opts }) _ -> do let opts = addDef n (Optimise True [] []) (idris_optimisation ist)- put (ist { idris_optimisation = opts })+ putIState (ist { idris_optimisation = opts }) addIBC (IBCOpt n)- ist <- get+ ist <- getIState let pats = pats_in -- logLvl 3 (showSep "\n" (map (\ (l,r) -> -- show l ++ " = " ++ @@ -369,7 +401,7 @@ pdef' <- applyOpts optpdef logLvl 2 $ "Optimised patterns" logLvl 5 $ show pdef'- ist <- get+ ist <- getIState -- let wf = wellFounded ist n sc let tot = if pcover || AssertTotal `elem` opts then Unchecked -- finish checking later@@ -393,8 +425,8 @@ logLvl 3 (show tree) logLvl 3 $ "Optimised: " ++ show tree' ctxt <- getContext- ist <- get- put (ist { idris_patdefs = addDef n pdef' (idris_patdefs ist) })+ ist <- getIState+ putIState (ist { idris_patdefs = addDef n pdef' (idris_patdefs ist) }) case lookupTy (namespace info) n ctxt of [ty] -> do updateContext (addCasedef n (inlinable opts) tcase knowncovering @@ -405,7 +437,7 @@ setTotality n tot totcheck (fc, n) when (tot /= Unchecked) $ addIBC (IBCTotal n tot)- i <- get+ i <- getIState case lookupDef Nothing n (tt_ctxt i) of (CaseOp _ _ _ _ _ scargs sc scargs' sc' : _) -> do let calls = findCalls sc' scargs'@@ -453,7 +485,7 @@ elabVal :: ElabInfo -> Bool -> PTerm -> Idris (Term, Type) elabVal info aspat tm_in = do ctxt <- getContext- i <- get+ i <- getIState let tm = addImpl i tm_in logLvl 10 (showImp True tm) -- try:@@ -478,7 +510,7 @@ checkPossible :: ElabInfo -> FC -> Bool -> Name -> PTerm -> Idris Bool checkPossible info fc tcgen fname lhs_in = do ctxt <- getContext- i <- get+ i <- getIState let lhs = addImpl i lhs_in -- if the LHS type checks, it is possible case elaborate ctxt (MN 0 "patLHS") infP []@@ -505,17 +537,27 @@ = do ctxt <- getContext -- Build the LHS as an "Infer", and pull out its type and -- pattern bindings- i <- get- let lhs = addImplPat i lhs_in+ i <- getIState+ -- get the parameters first, to pass through to any where block+ let fn_ty = case lookupTy Nothing fname (tt_ctxt i) of+ [t] -> t+ _ -> error "Can't happen (elabClause function type)"+ let fn_is = case lookupCtxt Nothing fname (idris_implicits i) of+ [t] -> t+ _ -> [] + let params = getParamsInType i [] fn_is fn_ty+ let lhs = addImplPat i (propagateParams params lhs_in) logLvl 5 ("LHS: " ++ show fc ++ " " ++ showImp True 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))) let lhs_tm = orderPats (getInferTerm lhs') let lhs_ty = getInferType lhs' logLvl 3 ("Elaborated: " ++ show lhs_tm)+ logLvl 3 ("Elaborated type: " ++ show lhs_ty) (clhs, clhsty) <- recheckC fc [] lhs_tm- logLvl 5 ("Checked " ++ show clhs)+ logLvl 5 ("Checked " ++ show clhs ++ "\n" ++ show clhsty) -- Elaborate where block ist <- getIState windex <- getName@@ -533,7 +575,7 @@ logLvl 5 $ "Where block:\n " ++ show wbefore ++ "\n" ++ show wafter mapM_ (elabDecl' EAll info) wbefore -- Now build the RHS, using the type of the LHS as the goal.- i <- get -- new implicits from where block+ i <- getIState -- new implicits from where block logLvl 5 (showImp True (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)@@ -567,7 +609,7 @@ case converts ctxt [] clhsty crhsty of OK _ -> return () Error e -> ierror (At fc (CantUnify False clhsty crhsty e [] 0))- i <- get+ i <- getIState checkInferred fc (delab' i crhs True) rhs return $ Right (clhs, crhs) where@@ -598,11 +640,45 @@ -- _ -> MN i (show n)) . l } + getParamsInType i env (PExp _ _ _ _ : is) (Bind n (Pi t) sc) + = getParamsInType i env is (instantiate (P Bound n t) sc)+ getParamsInType i env (_ : is) (Bind n (Pi t) sc) + = getParamsInType i (n : env) is (instantiate (P Bound n t) sc)+ getParamsInType i env is tm@(App f a)+ | (P _ tn _, args) <- unApply tm + = case lookupCtxt Nothing tn (idris_datatypes i) of+ [t] -> nub $ paramNames args env (param_pos t) +++ getParamsInType i env is f ++ + getParamsInType i env is a+ [] -> nub $ getParamsInType i env is f ++ + getParamsInType i env is a+ | otherwise = nub $ getParamsInType i env is f ++ + getParamsInType i env is a+ getParamsInType i _ _ _ = []++ paramNames args env [] = []+ paramNames args env (p : ps) + | length args > p = case args!!p of+ P _ n _ -> if n `elem` env+ then n : paramNames args env ps+ else paramNames args env ps+ _ -> paramNames args env ps+ | otherwise = paramNames args env ps++ propagateParams :: [Name] -> PTerm -> PTerm+ propagateParams ps (PApp _ (PRef fc n) args)+ = PApp fc (PRef fc n) (map addP args)+ where addP imp@(PImp _ _ _ Placeholder _)+ | pname imp `elem` ps = imp { getTm = PRef fc (pname imp) }+ addP t = t+ propagateParams ps (PRef fc n)+ = PApp fc (PRef fc n) (map (\x -> pimp x (PRef fc x)) ps)+ elabClause info tcgen (_, PWith fc fname lhs_in withs wval_in withblock) = do ctxt <- getContext -- Build the LHS as an "Infer", and pull out its type and -- pattern bindings- i <- get+ i <- getIState let lhs = addImpl i lhs_in logLvl 5 ("LHS: " ++ showImp True lhs) ((lhs', dlhs, []), _) <- @@ -655,7 +731,7 @@ logLvl 3 ("New function type " ++ show wtype) let wname = MN windex (show fname) let imps = getImps wtype -- add to implicits context- put (i { idris_implicits = addDef wname imps (idris_implicits i) })+ putIState (i { idris_implicits = addDef wname imps (idris_implicits i) }) addIBC (IBCDef wname) def' <- checkDef fc [(wname, wtype)] addDeferred def'@@ -673,9 +749,9 @@ (map (pexp . (PRef fc) . fst) bargs_pre ++ pexp wval : (map (pexp . (PRef fc) . fst) bargs_post))- logLvl 1 ("New RHS " ++ show rhs)+ logLvl 5 ("New RHS " ++ showImp True rhs) ctxt <- getContext -- New context with block added- i <- get+ i <- getIState ((rhs', defer, is), _) <- tclift $ elaborate ctxt (MN 0 "wpatRHS") clhsty [] (do pbinds lhs_tm@@ -686,6 +762,7 @@ def' <- checkDef fc defer addDeferred def' mapM_ (elabCaseBlock info) is+ logLvl 5 ("Checked RHS " ++ show rhs') (crhs, crhsty) <- recheckC fc [] rhs' return $ Right (clhs, crhs) where@@ -699,7 +776,7 @@ mkAuxC wname lhs ns ns' d = return $ d mkAux wname toplhs ns ns' (PClause fc n tm_in (w:ws) rhs wheres)- = do i <- get+ = do i <- getIState let tm = addImpl i tm_in logLvl 2 ("Matching " ++ showImp True tm ++ " against " ++ showImp True toplhs)@@ -710,7 +787,7 @@ lhs <- updateLHS n wname mvars ns ns' (fullApp tm) w return $ PClause fc wname lhs ws rhs wheres mkAux wname toplhs ns ns' (PWith fc n tm_in (w:ws) wval withs)- = do i <- get+ = do i <- getIState let tm = addImpl i tm_in logLvl 2 ("Matching " ++ showImp True tm ++ " against " ++ showImp True toplhs)@@ -765,6 +842,8 @@ (filter clause ds) let (methods, imethods) = unzip (map (\ ( x,y,z) -> (x, y)) ims)+ let defaults = map (\ (x, (y, z)) -> (x,y)) defs+ addClass tn (CI cn (map nodoc imethods) defaults (map fst ps) []) -- build instance constructor type -- decorate names of functions to ensure they can't be referred -- to elsewhere in the class declaration@@ -785,9 +864,7 @@ mapM_ (elabDecl EAll info) (concat fns) -- add the default definitions mapM_ (elabDecl EAll info) (concat (map (snd.snd) defs))- i <- get- let defaults = map (\ (x, (y, z)) -> (x,y)) defs- addClass tn (CI cn (map nodoc imethods) defaults (map fst ps) []) + i <- getIState addIBC (IBCClass tn) where nodoc (n, (_, o, t)) = (n, (o, t))@@ -800,7 +877,7 @@ impbind [] x = x impbind ((n, ty): ns) x = PPi impl n ty (impbind ns x) - conbind (ty : ns) x = PPi constraint (MN 0 "c") ty (conbind ns x)+ conbind (ty : ns) x = PPi constraint (MN 0 "class") ty (conbind ns x) conbind [] x = x getMName (PTy _ _ _ _ n _) = nsroot n@@ -818,7 +895,7 @@ Just (syn, o, ty) -> do let ty' = insertConstraint c ty let ds = map (decorateid defaultdec) [PTy "" syn fc [] n ty', - PClauses fc (TCGen:o ++ opts) n cs]+ PClauses fc (Inlinable:TCGen:o ++ opts) n cs] iLOG (show ds) return (n, ((defaultdec n, ds!!1), ds)) _ -> fail $ show n ++ " is not a method"@@ -841,7 +918,7 @@ let ty = PPi constraint (MN 0 "pc") c con iLOG (showImp True ty) iLOG (showImp True lhs ++ " = " ++ showImp True rhs)- i <- get+ i <- getIState let conn = case con of PRef _ n -> n PApp _ (PRef _ n) _ -> n@@ -888,7 +965,7 @@ insertConstraint c (PPi p@(Imp _ _ _) n ty sc) = PPi p n ty (insertConstraint c sc)- insertConstraint c sc = PPi constraint (MN 0 "c") c sc+ insertConstraint c sc = PPi constraint (MN 0 "class") c sc -- make arguments explicit and don't bind class parameters toExp ns e (PPi (Imp l s _) n ty sc)@@ -905,10 +982,11 @@ Maybe Name -> -- explicit name [PDecl] -> Idris () elabInstance info syn fc cs n ps t expn ds- = do i <- get + = do i <- getIState (n, ci) <- case lookupCtxtName (namespace info) n (idris_classes i) of [c] -> return c _ -> 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) Just nm -> nm@@ -945,9 +1023,7 @@ logLvl 3 $ "Method types " ++ showSep "\n" (map (showDeclImp True . mkTyDecl) mtys) logLvl 3 $ "Instance is " ++ show ps ++ " implicits " ++ show (concat (nub wparams))- let lhs = case concat (nub wparams) of- [] -> PRef fc iname- as -> PApp fc (PRef fc iname) as+ let lhs = PRef fc iname let rhs = PApp fc (PRef fc (instanceName ci)) (map (pexp . mkMethApp) mtys) let idecls = [PClauses fc [Inlinable, TCGen] iname @@ -955,6 +1031,10 @@ iLOG (show idecls) mapM (elabDecl EAll info) idecls addIBC (IBCInstance intInst n iname)+-- -- for each constraint, build a top level function to chase it+-- logLvl 5 $ "Building functions"+-- fns <- mapM (cfun (instanceName ci) constraint syn idecls) cs+-- mapM_ (elabDecl EAll info) (concat fns) where intInst = case ps of [PConstant IType] -> True@@ -1010,7 +1090,7 @@ mkTyDecl (n, op, t, _) = PTy "" syn fc op n t - conbind (ty : ns) x = PPi constraint (MN 0 "c") ty (conbind ns x)+ conbind (ty : ns) x = PPi constraint (MN 0 "class") ty (conbind ns x) conbind [] x = x coninsert cs (PPi p@(Imp _ _ _) n t sc) = PPi p n t (coninsert cs sc)@@ -1046,6 +1126,31 @@ = decorate ns iname m == decorate ns iname m' clauseFor m iname ns _ = False +{- This won't work yet. Can it ever, in this form?++ cfun cn c syn all con+ = do let cfn = UN ('@':'@':show 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)+ i <- getIState+ let conn = case con of+ PRef _ n -> n+ PApp _ (PRef _ n) _ -> n+ let conn' = case lookupCtxtName Nothing conn (idris_classes i) of+ [(n, _)] -> n+ _ -> conn+ addInstance False conn' cfn+ 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 []]]+-}+ decorateid decorate (PTy doc s f o n t) = PTy doc s f o (decorate n) t decorateid decorate (PClauses f o n cs) = PClauses f o (decorate n) (map dc cs)@@ -1109,7 +1214,7 @@ elabDecl' what info d@(PClauses f o n ps) | what /= ETypes = do iLOG $ "Elaborating clause " ++ show n- i <- get -- get the type options too+ i <- getIState -- get the type options too let o' = case lookupCtxt Nothing n (idris_flags i) of [fs] -> fs [] -> []@@ -1118,7 +1223,7 @@ = do mapM_ (elabDecl ETypes info) ps mapM_ (elabDecl EDefns info) ps elabDecl' what info (PParams f ns ps) - = do i <- get+ = do i <- getIState iLOG $ "Expanding params block with " ++ show ns ++ " decls " ++ show (concatMap tldeclared ps) let nblock = pblock i@@ -1151,8 +1256,8 @@ = do iLOG $ "Elaborating record " ++ show tyn elabRecord info s doc f tyn ty cdoc cn cty elabDecl' _ info (PDSL n dsl)- = do i <- get- put (i { idris_dsls = addDef n dsl (idris_dsls i) }) + = do i <- getIState+ putIState (i { idris_dsls = addDef n dsl (idris_dsls i) }) addIBC (IBCDSL n) elabDecl' what info (PDirective i) | what /= EDefns = i@@ -1174,7 +1279,7 @@ do logLvl 6 $ "Checked to\n" ++ showImp True inf ++ "\n\nFROM\n\n" ++ showImp True user logLvl 10 $ "Checking match"- i <- get+ i <- getIState tclift $ case matchClause' True i user inf of Right vs -> return () Left (x, y) -> tfail $ At fc @@ -1188,7 +1293,7 @@ inferredDiff :: FC -> PTerm -> PTerm -> Idris Bool inferredDiff fc inf user =- do i <- get+ do i <- getIState logLvl 6 $ "Checked to\n" ++ showImp True inf ++ "\n" ++ showImp True user tclift $ case matchClause' True i user inf of
src/Idris/ElabTerm.hs view
@@ -39,6 +39,27 @@ ElabD (Term, [(Name, Type)], [PDecl]) build ist info pattern fn tm = do elab ist info pattern False fn tm+ ivs <- get_instances+ hs <- get_holes+ ptm <- get_term+ -- Resolve remaining type classes. Two passes - first to get the+ -- default Num instances, second to clean up the rest+ when (not pattern) $+ mapM_ (\n -> when (n `elem` hs) $ + do focus n+ try (resolveTC 7 fn ist)+ (movelast n)) ivs+ ivs <- get_instances+ hs <- get_holes+ when (not pattern) $+ mapM_ (\n -> when (n `elem` hs) $ + do focus n+ resolveTC 7 fn ist) ivs+ probs <- get_probs+ tm <- get_term+ case probs of+ [] -> return ()+ ((_,_,_,e):es) -> lift (Error e) is <- getAux tt <- get_term let (tm, ds) = runState (collectDeferred tt) []@@ -54,6 +75,11 @@ ElabD (Term, [(Name, Type)], [PDecl]) buildTC ist info pattern tcgen fn tm = do elab ist info pattern tcgen fn tm+ probs <- get_probs+ tm <- get_term+ case probs of+ [] -> return ()+ ((_,_,_,e):es) -> lift (Error e) is <- getAux tt <- get_term let (tm, ds) = runState (collectDeferred tt) []@@ -72,8 +98,6 @@ (do update_term orderPats -- tm <- get_term mkPat)- inj <- get_inj- mapM_ checkInjective inj where isph arg = case getTm arg of Placeholder -> (True, priority arg)@@ -110,11 +134,11 @@ elab' ina (PResolveTC (FC "HACK" _)) -- for chasing parent classes = resolveTC 5 fn ist elab' ina (PResolveTC fc) - | pattern = do c <- unique_hole (MN 0 "c")- instanceArg c+ | True = do c <- unique_hole (MN 0 "class")+ instanceArg c | otherwise = do g <- goal try (resolveTC 2 fn ist)- (do c <- unique_hole (MN 0 "c")+ (do c <- unique_hole (MN 0 "class") instanceArg c) elab' ina (PRefl fc t) = elab' ina (PApp fc (PRef fc eqCon) [pimp (MN 0 "a") Placeholder, pimp (MN 0 "x") t])@@ -122,15 +146,23 @@ pimp (MN 0 "b") Placeholder, pexp l, pexp r]) elab' ina@(_, a) (PPair fc l r) - = try (elabE (True, a) (PApp fc (PRef fc pairTy)- [pexp l,pexp r]))- (elabE (True, a) (PApp fc (PRef fc pairCon)+ = do hnf_compute + g <- goal+ case g of+ TType _ -> elabE (True, a) (PApp fc (PRef fc pairTy)+ [pexp l,pexp r])+ _ -> elabE (True, a) (PApp fc (PRef fc pairCon) [pimp (MN 0 "A") Placeholder, pimp (MN 0 "B") Placeholder,- pexp l, pexp r]))+ pexp l, pexp r]) elab' ina (PDPair fc l@(PRef _ n) t r) = case t of - Placeholder -> try asType asValue+ Placeholder -> + do hnf_compute+ g <- goal+ case g of+ TType _ -> asType+ _ -> asValue _ -> asType where asType = elab' ina (PApp fc (PRef fc sigmaTy) [pexp t,@@ -144,10 +176,14 @@ pimp (MN 0 "P") Placeholder, pexp l, pexp r]) elab' ina (PAlternative True as) - = do ty <- goal+ = do hnf_compute+ ty <- goal ctxt <- get_context let (tc, _) = unApply ty let as' = pruneByType tc ctxt as+-- case as' of+-- [a] -> elab' ina a+-- as -> lift $ tfail $ CantResolveAlts (map showHd as) tryAll (zip (map (elab' ina) as') (map showHd as')) where showHd (PApp _ h _) = show h showHd x = show x@@ -181,6 +217,7 @@ = do -- n' <- unique_hole n -- let sc' = mapPT (repN n n') sc ptm <- get_term+ g <- goal attack; intro (Just n); -- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm) elabE (True, a) sc; solve@@ -231,6 +268,7 @@ focus valn elabE (True, a) val elabE (True, a) sc+ ptm <- get_term solve elab' ina tm@(PApp fc (PInferRef _ f) args) = do rty <- goal@@ -277,43 +315,58 @@ Just xs@(_:_) -> NS n xs _ -> n + -- if f is local, just do a simple_app elab' (ina, g) tm@(PApp fc (PRef _ f) args') = do let args = {- case lookupCtxt f (inblock info) of Just ps -> (map (pexp . (PRef fc)) ps ++ args') _ ->-} args' -- newtm <- mkSpecialised ist fc f (map getTm args') tm- ivs <- get_instances- -- HACK: we shouldn't resolve type classes if we're defining an instance- -- function or default definition.- let isinf = f == inferCon || tcname f- ctxt <- get_context- let guarded = isConName Nothing f ctxt--- when True- tryWhen True- (do ns <- apply (Var f) (map isph args)+ env <- get_env+ if (f `elem` map fst env && length args' == 1)+ then -- simple app, as below+ do simple_app (elabE (ina, g) (PRef fc f)) + (elabE (True, g) (getTm (head args')))+ solve+ else + do ivs <- get_instances+ ps <- get_probs+ -- HACK: we shouldn't resolve type classes if we're defining an instance+ -- function or default definition.+ let isinf = f == inferCon || tcname f+ -- if f is a type class, we need to know its arguments so that+ -- we can unify with them+ case lookupCtxt Nothing f (idris_classes ist) of+ [] -> return ()+ _ -> mapM_ setInjective (map getTm args')+ ctxt <- get_context+ let guarded = isConName Nothing f ctxt+ ns <- apply (Var f) (map isph args) ptm <- get_term+ g <- goal let (ns', eargs) = unzip $ sortBy (\(_,x) (_,y) -> compare (priority x) (priority y)) (zip ns args)- tryWhen True - (elabArgs (ina || not isinf, guarded)- [] False ns' (map (\x -> (lazyarg x, getTm x)) eargs))- (elabArgs (ina || not isinf, guarded)- [] False (reverse ns') - (map (\x -> (lazyarg x, getTm x)) (reverse eargs)))- mkSpecialised ist fc f (map getTm args') tm- solve)- (do apply_elab f (map (toElab (ina || not isinf, guarded)) args)+ elabArgs (ina || not isinf, guarded)+ [] False ns' (map (\x -> (lazyarg x, getTm x)) eargs) mkSpecialised ist fc f (map getTm args') tm- solve)--- ptm <- get_term--- elog (show ptm)- ivs' <- get_instances- when (not pattern || (ina && not tcgen)) $- mapM_ (\n -> do focus n- -- let insts = filter tcname $ map fst (ctxtAlist (tt_ctxt ist))- resolveTC 7 fn ist) (ivs' \\ ivs) + solve+ ptm <- get_term+ ivs' <- get_instances+ ps' <- get_probs+ -- Attempt to resolve any type classes which have 'complete' types,+ -- i.e. no holes in them+ when (not pattern || (ina && not tcgen && not guarded)) $+ mapM_ (\n -> do focus n+ g <- goal+ env <- get_env+ hs <- get_holes+ if all (\n -> not (n `elem` hs)) (freeNames g)+ -- let insts = filter tcname $ map fst (ctxtAlist (tt_ctxt ist))+ then try (resolveTC 7 fn ist)+ (movelast n)+ else movelast n) + (ivs' \\ ivs) where tcArg (n, PConstraint _ _ Placeholder _) = True tcArg _ = False @@ -321,10 +374,13 @@ tacTm (PProof _) = True tacTm _ = False + setInjective (PRef _ n) = setinj n+ setInjective (PApp _ (PRef _ n) _) = setinj n+ setInjective _ = return ()+ elab' ina@(_, a) (PApp fc f [arg]) = erun fc $ - do ptm <- get_term- simple_app (elabE ina f) (elabE (True, a) (getTm arg))+ do simple_app (elabE ina f) (elabE (True, a) (getTm arg)) solve elab' ina Placeholder = do (h : hs) <- get_holes movelast h@@ -436,22 +492,29 @@ -- Rule out alternatives that don't return the same type as the head of the goal -- (If there are none left as a result, do nothing)- pruneByType :: Term -> Context -> [PTerm] -> [PTerm] pruneByType (P _ n _) c as - = let as' = filter (headIs n) as in- case as' of- [] -> as- _ -> as'+-- if the goal type is polymorphic, keep e+ | [] <- lookupTy Nothing n c = as+ | otherwise + = let asV = filter (headIs True n) as + as' = filter (headIs False n) as in+ case as' of+ [] -> case asV of+ [] -> as+ _ -> asV+ _ -> as' where- headIs f (PApp _ (PRef _ f') _) = typeHead f f'- headIs f (PApp _ f' _) = headIs f f'- headIs f (PPi _ _ _ sc) = headIs f sc- headIs _ _ = True -- keep if it's not an application+ headIs var f (PApp _ (PRef _ f') _) = typeHead var f f'+ headIs var f (PApp _ f' _) = headIs var f f'+ headIs var f (PPi _ _ _ sc) = headIs var f sc+ headIs _ _ _ = True -- keep if it's not an application - typeHead f f' = case lookupTy Nothing f' c of+ typeHead var f f' + = case lookupTy Nothing f' c of [ty] -> case unApply (getRetTy ty) of (P _ ftyn _, _) -> ftyn == f+ (V _, _) -> var -- keep, variable _ -> False _ -> False @@ -462,13 +525,20 @@ (PRefl (FC "prf" 0) Placeholder) return ()) (do env <- get_env- tryAll (map fst env)+ g <- goal+ tryAll env return ()) True where tryAll [] = fail "No trivial solution"- tryAll (x:xs) = try' (elab ist toplevel False False+ tryAll ((x, b):xs) + = do -- if type of x has any holes in it, move on+ hs <- get_holes+ g <- goal+ if all (\n -> not (n `elem` hs)) (freeNames (binderTy b))+ then try' (elab ist toplevel False False (MN 0 "tac") (PRef (FC "prf" 0) x)) (tryAll xs) True+ else tryAll xs findInstances :: IState -> Term -> [Name] findInstances ist t @@ -483,7 +553,11 @@ resolveTC 1 fn ist = try' (trivial ist) (resolveTC 0 fn ist) True resolveTC depth fn ist = do hnf_compute- try' (trivial ist)+ g <- goal+ ptm <- get_term+ hs <- get_holes + if True -- all (\n -> not (n `elem` hs)) (freeNames g)+ then try' (trivial ist) (do t <- goal let insts = findInstances ist t let (tc, ttypes) = unApply t@@ -491,17 +565,23 @@ tm <- get_term -- traceWhen (depth > 6) ("GOAL: " ++ show t ++ "\nTERM: " ++ show tm) $ -- (tryAll (map elabTC (map fst (ctxtAlist (tt_ctxt ist)))))+-- if scopeOnly then fail "Can't resolve" else let depth' = if scopeOnly then 2 else depth blunderbuss t depth' insts) True+ else do try' (trivial ist)+ (do g <- goal+ fail $ "Can't resolve " ++ show g) True+-- tm <- get_term+-- fail $ "Can't resolve yet in " ++ show tm where elabTC n | n /= fn && tcname n = (resolve n depth, show n) | otherwise = (fail "Can't resolve", show n) --- needsDefault t num@(P _ (NS (UN "Num") ["builtins"]) _) [P Bound a _]--- = do focus a--- fill (RConstant IType) -- default Int--- solve--- return False+ needsDefault t num@(P _ (NS (UN "Num") ["Builtins"]) _) [P Bound a _]+ = do focus a+ fill (RConstant IType) -- default Int+ solve+ return False needsDefault t f as | all boundVar as = return True -- fail $ "Can't resolve " ++ show t needsDefault t f a = return False -- trace (show t) $ return ()@@ -509,7 +589,9 @@ boundVar (P Bound _ _) = True boundVar _ = False - blunderbuss t d [] = lift $ tfail $ CantResolve t+ blunderbuss t d [] = do -- c <- get_env+ -- ps <- get_probs+ lift $ tfail $ CantResolve t blunderbuss t d (n:ns) | n /= fn && tcname n = try' (resolve n d) (blunderbuss t d ns) True@@ -526,8 +608,11 @@ let imps = case lookupCtxtName Nothing n (idris_implicits ist) of [] -> [] [args] -> map isImp (snd args) -- won't be overloaded!+ ps <- get_probs args <- apply (Var n) imps- -- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $+ ps' <- get_probs+ when (length ps < length ps') $ fail "Can't apply type class"+-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $ mapM_ (\ (_,n) -> do focus n t' <- goal let (tc', ttype) = unApply t'@@ -535,6 +620,7 @@ resolveTC depth' fn ist) (filter (\ (x, y) -> not x) (zip (map fst imps) args)) -- if there's any arguments left, we've failed to resolve+ hs <- get_holes solve where isImp (PImp p _ _ _ _) = (True, p) isImp arg = (False, priority arg)
src/Idris/Error.hs view
@@ -20,7 +20,7 @@ iucheck :: Idris () iucheck = do tit <- typeInType when (not tit) $- do ist <- get+ do ist <- getIState idrisCatch (tclift $ ucheck (idris_constraints ist)) (\e -> do let msg = show e setErrLine (getErrLine msg)@@ -46,13 +46,13 @@ ifail str = throwIO (IErr str) ierror :: Err -> Idris ()-ierror err = do i <- get+ierror err = do i <- getIState throwIO (IErr $ pshow i err) tclift :: TC a -> Idris a tclift tc = case tc of OK v -> return v- Error err -> do i <- get+ Error err -> do i <- getIState case err of At (FC f l) e -> setErrLine l _ -> return ()
src/Idris/IBC.hs view
@@ -21,7 +21,7 @@ import Paths_idris ibcVersion :: Word8-ibcVersion = 24+ibcVersion = 26 data IBCFile = IBCFile { ver :: Word8, sourcefile :: FilePath,@@ -353,16 +353,22 @@ put x1 Str x1 -> do putWord8 4 put x1- IType -> putWord8 5- BIType -> putWord8 6- FlType -> putWord8 7- ChType -> putWord8 8- StrType -> putWord8 9- PtrType -> putWord8 10- Forgot -> putWord8 11+ B8 x1 -> putWord8 5 >> put x1+ B16 x1 -> putWord8 6 >> put x1+ B32 x1 -> putWord8 7 >> put x1+ B64 x1 -> putWord8 8 >> put x1 - W8Type -> putWord8 12- W16Type -> putWord8 13+ IType -> putWord8 9+ BIType -> putWord8 10+ FlType -> putWord8 11+ ChType -> putWord8 12+ StrType -> putWord8 13+ PtrType -> putWord8 14+ Forgot -> putWord8 15+ B8Type -> putWord8 16+ B16Type -> putWord8 17+ B32Type -> putWord8 18+ B64Type -> putWord8 19 get = do i <- getWord8 case i of@@ -376,17 +382,24 @@ return (Ch x1) 4 -> do x1 <- get return (Str x1)- 5 -> return IType- 6 -> return BIType- 7 -> return FlType- 8 -> return ChType- 9 -> return StrType- 10 -> return PtrType- 11 -> return Forgot+ 5 -> fmap B8 get+ 6 -> fmap B16 get+ 7 -> fmap B32 get+ 8 -> fmap B64 get - 12 -> return W8Type- 13 -> return W16Type+ 9 -> return IType+ 10 -> return BIType+ 11 -> return FlType+ 12 -> return ChType+ 13 -> return StrType+ 14 -> return PtrType+ 15 -> return Forgot + 16 -> return B8Type+ 17 -> return B16Type+ 18 -> return B32Type+ 19 -> return B64Type+ _ -> error "Corrupted binary data for Const" @@ -1522,11 +1535,13 @@ return (Optimise x1 x2 x3) instance Binary TypeInfo where- put (TI x1 x2) = do put x1- put x2+ put (TI x1 x2 x3) = do put x1+ put x2+ put x3 get = do x1 <- get x2 <- get- return (TI x1 x2)+ x3 <- get+ return (TI x1 x2 x3) instance Binary SynContext where put x
src/Idris/Parser.hs view
@@ -63,12 +63,13 @@ loadModule :: FilePath -> Idris String loadModule f = idrisCatch (do i <- getIState+ let file = takeWhile (/= ' ') f ibcsd <- valIBCSubDir i ids <- allImportDirs i- fp <- liftIO $ findImport ids ibcsd f- if f `elem` imported i- then iLOG $ "Already read " ++ f- else do putIState (i { imported = f : imported i })+ fp <- liftIO $ findImport ids ibcsd file+ if file `elem` imported i+ then iLOG $ "Already read " ++ file+ else do putIState (i { imported = file : imported i }) case fp of IDR fn -> loadSource False fn LIDR fn -> loadSource True fn@@ -78,7 +79,7 @@ case src of IDR sfn -> loadSource False sfn LIDR sfn -> loadSource True sfn)- let (dir, fh) = splitFileName f+ let (dir, fh) = splitFileName file return (dropExtension fh)) (\e -> do let msg = show e setErrLine (getErrLine msg)@@ -110,7 +111,7 @@ v <- verbose when v $ iputStrLn $ "Type checking " ++ f elabDecls toplevel ds- i <- get+ i <- getIState -- simplify every definition do give the totality checker -- a better chance mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n@@ -118,7 +119,7 @@ (map snd (idris_totcheck i)) -- build size change graph from simplified definitions iLOG "Totality checking"- i <- get+ i <- getIState mapM_ buildSCG (idris_totcheck i) mapM_ checkDeclTotality (idris_totcheck i) iLOG ("Finished " ++ f)@@ -162,7 +163,7 @@ parseImports :: FilePath -> String -> Idris ([String], [String], String, SourcePos) parseImports fname input - = do i <- get+ = do i <- getIState case runParser (do whiteSpace mname <- pHeader ps <- many pImport@@ -170,7 +171,7 @@ pos <- getPosition return ((mname, ps, rest, pos), i)) i fname input of Left err -> fail (show err)- Right (x, i) -> do put i+ Right (x, i) -> do putIState i return x pHeader :: IParser [String]@@ -275,7 +276,7 @@ parseProg :: SyntaxInfo -> FilePath -> String -> SourcePos -> Idris [PDecl] parseProg syn fname input pos- = do i <- get+ = do i <- getIState case runParser (do setPosition pos whiteSpace ps <- many (pDecl syn)@@ -284,7 +285,7 @@ return (concat ps, i')) i fname input of Left err -> do iputStrLn (show err) return []- Right (x, i) -> do put i+ Right (x, i) -> do putIState i return (collect x) -- Collect PClauses with the same function name@@ -431,8 +432,8 @@ opts' <- pFnOpts opts n_in <- pfName let n = expandNS syn n_in- ty <- pTSig (impOK syn) fc <- pfc+ ty <- pTSig (impOK syn) pTerminator -- ty' <- implicit syn n ty addAcc n acc@@ -1084,8 +1085,10 @@ <|> do reserved "Float"; return FlType <|> do reserved "String"; return StrType <|> do reserved "Ptr"; return PtrType- <|> do reserved "Word8"; return W8Type- <|> do reserved "Word16"; return W16Type+ <|> do reserved "Bits8"; return B8Type+ <|> do reserved "Bits16"; return B16Type+ <|> do reserved "Bits32"; return B32Type+ <|> do reserved "Bits64"; return B64Type <|> try (do f <- float; return $ Fl f) -- <|> try (do i <- natural; lchar 'L'; return $ BI i) <|> try (do i <- natural; return $ I (fromInteger i))@@ -1117,8 +1120,8 @@ assoc (Infixr _) = AssocRight assoc (InfixN _) = AssocNone -binary name f = Infix (do reservedOp name- fc <- pfc; +binary name f = Infix (do fc <- pfc+ reservedOp name doc <- option "" (pDocComment '^') return (f fc)) prefix name f = Prefix (do reservedOp name
src/Idris/Primitives.hs view
@@ -11,6 +11,8 @@ import Core.TT import Core.Evaluate import Data.Bits+import Data.Word+import Data.Int data Prim = Prim { p_name :: Name, p_type :: Type,@@ -75,25 +77,217 @@ Prim (UN "prim__gteChar") (ty [ChType, ChType] IType) 2 (bcBin (>=)) (2, LGe) total, - Prim (UN "prim__addW8") (ty [W8Type, W8Type] W8Type) 2 (w8Bin (+))- (2, LW8Plus) total,- Prim (UN "prim__subW8") (ty [W8Type, W8Type] W8Type) 2 (w8Bin (-))- (2, LW8Minus) total,- Prim (UN "prim__mulW8") (ty [W8Type, W8Type] W8Type) 2 (w8Bin (*))- (2, LW8Times) total,+ Prim (UN "prim__ltB8") (ty [B8Type, B8Type] IType) 2 (b8Cmp (<))+ (2, LB8Lt) total,+ Prim (UN "prim__lteB8") (ty [B8Type, B8Type] IType) 2 (b8Cmp (<=))+ (2, LB8Lte) total,+ Prim (UN "prim__eqB8") (ty [B8Type, B8Type] IType) 2 (b8Cmp (==))+ (2, LB8Eq) total,+ Prim (UN "prim__gteB8") (ty [B8Type, B8Type] IType) 2 (b8Cmp (>))+ (2, LB8Gte) total,+ Prim (UN "prim__gtB8") (ty [B8Type, B8Type] IType) 2 (b8Cmp (>=))+ (2, LB8Gt) total,+ Prim (UN "prim__addB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (+))+ (2, LB8Plus) total,+ Prim (UN "prim__subB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (-))+ (2, LB8Minus) total,+ Prim (UN "prim__mulB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (*))+ (2, LB8Times) total,+ Prim (UN "prim__udivB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin div)+ (2, LB8UDiv) partial,+ Prim (UN "prim__sdivB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin s8div)+ (2, LB8SDiv) partial,+ Prim (UN "prim__uremB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin rem)+ (2, LB8URem) partial,+ Prim (UN "prim__sremB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin s8rem)+ (2, LB8SRem) partial,+ Prim (UN "prim__shlB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (\x y -> shiftL x (fromIntegral y)))+ (2, LB8Shl) total,+ Prim (UN "prim__lshrB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (\x y -> shiftR x (fromIntegral y)))+ (2, LB8AShr) total,+ Prim (UN "prim__ashrB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (\x y -> fromIntegral $+ shiftR (fromIntegral x :: Int8)+ (fromIntegral y)))+ (2, LB8LShr) total,+ Prim (UN "prim__andB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (.&.))+ (2, LB8And) total,+ Prim (UN "prim__orB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (.|.))+ (2, LB8Or) total,+ Prim (UN "prim__xorB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin xor)+ (2, LB8Xor) total,+ Prim (UN "prim__complB8") (ty [B8Type] B8Type) 1 (b8Un complement)+ (1, LB8Compl) total,+ Prim (UN "prim__zextB8_16") (ty [B8Type] B16Type) 1 zext8_16+ (1, LB8Z16) total,+ Prim (UN "prim__zextB8_32") (ty [B8Type] B32Type) 1 zext8_32+ (1, LB8Z32) total,+ Prim (UN "prim__zextB8_64") (ty [B8Type] B64Type) 1 zext8_64+ (1, LB8Z64) total,+ Prim (UN "prim__sextB8_16") (ty [B8Type] B16Type) 1 sext8_16+ (1, LB8Z16) total,+ Prim (UN "prim__sextB8_32") (ty [B8Type] B32Type) 1 sext8_32+ (1, LB8Z32) total,+ Prim (UN "prim__sextB8_64") (ty [B8Type] B64Type) 1 sext8_64+ (1, LB8Z64) total, - Prim (UN "prim__addW16") (ty [W16Type, W16Type] W16Type) 2 (w16Bin (+))- (2, LW16Plus) total,- Prim (UN "prim__subW16") (ty [W16Type, W16Type] W16Type) 2 (w16Bin (-))- (2, LW16Minus) total,- Prim (UN "prim__mulW16") (ty [W16Type, W16Type] W16Type) 2 (w16Bin (*))- (2, LW16Times) total,+ Prim (UN "prim__ltB16") (ty [B16Type, B16Type] IType) 2 (b16Cmp (<))+ (2, LB16Lt) total,+ Prim (UN "prim__lteB16") (ty [B16Type, B16Type] IType) 2 (b16Cmp (<=))+ (2, LB16Lte) total,+ Prim (UN "prim__eqB16") (ty [B16Type, B16Type] IType) 2 (b16Cmp (==))+ (2, LB16Eq) total,+ Prim (UN "prim__gteB16") (ty [B16Type, B16Type] IType) 2 (b16Cmp (>))+ (2, LB16Gte) total,+ Prim (UN "prim__gtB16") (ty [B16Type, B16Type] IType) 2 (b16Cmp (>=))+ (2, LB16Gt) total,+ Prim (UN "prim__addB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin (+))+ (2, LB16Plus) total,+ Prim (UN "prim__subB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin (-))+ (2, LB16Minus) total,+ Prim (UN "prim__mulB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin (*))+ (2, LB16Times) total,+ Prim (UN "prim__udivB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin div)+ (2, LB16UDiv) partial,+ Prim (UN "prim__sdivB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin s16div)+ (2, LB16SDiv) partial,+ Prim (UN "prim__uremB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin rem)+ (2, LB16URem) partial,+ Prim (UN "prim__sremB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin s16rem)+ (2, LB16SRem) partial,+ Prim (UN "prim__shlB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin (\x y -> shiftL x (fromIntegral y)))+ (2, LB16Shl) total,+ Prim (UN "prim__lshrB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin (\x y -> shiftR x (fromIntegral y)))+ (2, LB16AShr) total,+ Prim (UN "prim__ashrB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin (\x y -> fromIntegral $+ shiftR (fromIntegral x :: Int16)+ (fromIntegral y)))+ (2, LB16LShr) total,+ Prim (UN "prim__andB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin (.&.))+ (2, LB16And) total,+ Prim (UN "prim__orB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin (.|.))+ (2, LB16Or) total,+ Prim (UN "prim__xorB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin xor)+ (2, LB16Xor) total,+ Prim (UN "prim__complB16") (ty [B16Type] B16Type) 1 (b16Un complement)+ (1, LB16Compl) total,+ Prim (UN "prim__zextB16_32") (ty [B16Type] B32Type) 1 zext16_32+ (1, LB16Z32) total,+ Prim (UN "prim__zextB16_64") (ty [B16Type] B64Type) 1 zext16_64+ (1, LB16Z64) total,+ Prim (UN "prim__sextB16_32") (ty [B16Type] B32Type) 1 sext16_32+ (1, LB16Z32) total,+ Prim (UN "prim__sextB16_64") (ty [B16Type] B64Type) 1 sext16_64+ (1, LB16Z64) total,+ Prim (UN "prim__truncB16_8") (ty [B16Type] B8Type) 1 trunc16_8+ (1, LB16T8) total, - Prim (UN "prim__intToWord8") (ty [IType] W8Type) 1 intToWord8- (1, LW8) total,- Prim (UN "prim__intToWord16") (ty [IType] W16Type) 1 intToWord16- (1, LW16) total,+ Prim (UN "prim__ltB32") (ty [B32Type, B32Type] IType) 2 (b32Cmp (<))+ (2, LB32Lt) total,+ Prim (UN "prim__lteB32") (ty [B32Type, B32Type] IType) 2 (b32Cmp (<=))+ (2, LB32Lte) total,+ Prim (UN "prim__eqB32") (ty [B32Type, B32Type] IType) 2 (b32Cmp (==))+ (2, LB32Eq) total,+ Prim (UN "prim__gteB32") (ty [B32Type, B32Type] IType) 2 (b32Cmp (>))+ (2, LB32Gte) total,+ Prim (UN "prim__gtB32") (ty [B32Type, B32Type] IType) 2 (b32Cmp (>=))+ (2, LB32Gt) total,+ Prim (UN "prim__addB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin (+))+ (2, LB32Plus) total,+ Prim (UN "prim__subB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin (-))+ (2, LB32Minus) total,+ Prim (UN "prim__mulB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin (*))+ (2, LB32Times) total,+ Prim (UN "prim__udivB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin div)+ (2, LB32UDiv) partial,+ Prim (UN "prim__sdivB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin s32div)+ (2, LB32SDiv) partial,+ Prim (UN "prim__uremB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin rem)+ (2, LB32URem) partial,+ Prim (UN "prim__sremB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin s32rem)+ (2, LB32SRem) partial,+ Prim (UN "prim__shlB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin (\x y -> shiftL x (fromIntegral y)))+ (2, LB32Shl) total,+ Prim (UN "prim__lshrB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin (\x y -> shiftR x (fromIntegral y)))+ (2, LB32AShr) total,+ Prim (UN "prim__ashrB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin (\x y -> fromIntegral $+ shiftR (fromIntegral x :: Int32)+ (fromIntegral y)))+ (2, LB32LShr) total,+ Prim (UN "prim__andB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin (.&.))+ (2, LB32And) total,+ Prim (UN "prim__orB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin (.|.))+ (2, LB32Or) total,+ Prim (UN "prim__xorB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin xor)+ (2, LB32Xor) total,+ Prim (UN "prim__complB32") (ty [B32Type] B32Type) 1 (b32Un complement)+ (1, LB32Compl) total,+ Prim (UN "prim__zextB32_64") (ty [B32Type] B64Type) 1 zext32_64+ (1, LB32Z64) total,+ Prim (UN "prim__sextB32_64") (ty [B32Type] B64Type) 1 sext32_64+ (1, LB32Z64) total,+ Prim (UN "prim__truncB32_8") (ty [B32Type] B8Type) 1 trunc32_8+ (1, LB32T8) total,+ Prim (UN "prim__truncB32_16") (ty [B32Type] B16Type) 1 trunc32_16+ (1, LB32T16) total, + Prim (UN "prim__ltB64") (ty [B64Type, B64Type] IType) 2 (b64Cmp (<))+ (2, LB64Lt) total,+ Prim (UN "prim__lteB64") (ty [B64Type, B64Type] IType) 2 (b64Cmp (<=))+ (2, LB64Lte) total,+ Prim (UN "prim__eqB64") (ty [B64Type, B64Type] IType) 2 (b64Cmp (==))+ (2, LB64Eq) total,+ Prim (UN "prim__gteB64") (ty [B64Type, B64Type] IType) 2 (b64Cmp (>))+ (2, LB64Gte) total,+ Prim (UN "prim__gtB64") (ty [B64Type, B64Type] IType) 2 (b64Cmp (>=))+ (2, LB64Gt) total,+ Prim (UN "prim__addB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin (+))+ (2, LB64Plus) total,+ Prim (UN "prim__subB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin (-))+ (2, LB64Minus) total,+ Prim (UN "prim__mulB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin (*))+ (2, LB64Times) total,+ Prim (UN "prim__udivB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin div)+ (2, LB64UDiv) partial,+ Prim (UN "prim__sdivB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin s64div)+ (2, LB64SDiv) partial,+ Prim (UN "prim__uremB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin rem)+ (2, LB64URem) partial,+ Prim (UN "prim__sremB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin s64rem)+ (2, LB64SRem) partial,+ Prim (UN "prim__shlB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin (\x y -> shiftL x (fromIntegral y)))+ (2, LB64Shl) total,+ Prim (UN "prim__lshrB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin (\x y -> shiftR x (fromIntegral y)))+ (2, LB64AShr) total,+ Prim (UN "prim__ashrB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin (\x y -> fromIntegral $+ shiftR (fromIntegral x :: Int64)+ (fromIntegral y)))+ (2, LB64LShr) total,+ Prim (UN "prim__andB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin (.&.))+ (2, LB64And) total,+ Prim (UN "prim__orB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin (.|.))+ (2, LB64Or) total,+ Prim (UN "prim__xorB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin xor)+ (2, LB64Xor) total,+ Prim (UN "prim__complB64") (ty [B64Type] B64Type) 1 (b64Un complement)+ (1, LB64Compl) total,+ Prim (UN "prim__truncB64_8") (ty [B64Type] B8Type) 1 trunc64_8+ (1, LB64T8) total,+ Prim (UN "prim__truncB64_16") (ty [B64Type] B16Type) 1 trunc64_16+ (1, LB64T16) total,+ Prim (UN "prim__truncB64_32") (ty [B64Type] B32Type) 1 trunc64_32+ (1, LB64T32) total,++ Prim (UN "prim__intToB8") (ty [IType] B8Type) 1 intToBits8+ (1, LIntB8) total,+ Prim (UN "prim__intToB16") (ty [IType] B16Type) 1 intToBits16+ (1, LIntB16) total,+ Prim (UN "prim__intToB32") (ty [IType] B32Type) 1 intToBits32+ (1, LIntB32) total,+ Prim (UN "prim__intToB64") (ty [IType] B64Type) 1 intToBits64+ (1, LIntB64) total,+ Prim (UN "prim__B32ToInt") (ty [B32Type] IType) 1 bits32ToInt+ (1, LB32Int) total,+ Prim (UN "prim__addBigInt") (ty [BIType, BIType] BIType) 2 (bBin (+)) (2, LBPlus) total, Prim (UN "prim__subBigInt") (ty [BIType, BIType] BIType) 2 (bBin (-))@@ -245,19 +439,136 @@ sBin op [VConstant (Str x), VConstant (Str y)] = Just $ VConstant (Str (op x y)) sBin _ _ = Nothing -w8Bin op [VConstant (W8 x), VConstant (W8 y)] = Just $ VConstant (W8 (op x y))-w8Bin _ _ = Nothing+s8div :: Word8 -> Word8 -> Word8+s8div x y = fromIntegral (fromIntegral x `div` fromIntegral y :: Int8) -w16Bin op [VConstant (W16 x), VConstant (W16 y)] = Just $ VConstant (W16 (op x y))-w16Bin _ _ = Nothing+s16div :: Word16 -> Word16 -> Word16+s16div x y = fromIntegral (fromIntegral x `div` fromIntegral y :: Int16) --- w32Bin op [VConstant (W32 x), VConstant (W32 y)] = Just $ VConstant (W32 (op x y))--- w32Bin _ _ = Nothing+s32div :: Word32 -> Word32 -> Word32+s32div x y = fromIntegral (fromIntegral x `div` fromIntegral y :: Int32) -intToWord8 [VConstant (I x)] = Just $ VConstant (W8 $ fromIntegral x)-intToWord8 _ = Nothing-intToWord16 [VConstant (I x)] = Just $ VConstant (W16 $ fromIntegral x)-intToWord16 _ = Nothing+s64div :: Word64 -> Word64 -> Word64+s64div x y = fromIntegral (fromIntegral x `div` fromIntegral y :: Int64)++s8rem :: Word8 -> Word8 -> Word8+s8rem x y = fromIntegral (fromIntegral x `rem` fromIntegral y :: Int8)++s16rem :: Word16 -> Word16 -> Word16+s16rem x y = fromIntegral (fromIntegral x `rem` fromIntegral y :: Int16)++s32rem :: Word32 -> Word32 -> Word32+s32rem x y = fromIntegral (fromIntegral x `rem` fromIntegral y :: Int32)++s64rem :: Word64 -> Word64 -> Word64+s64rem x y = fromIntegral (fromIntegral x `rem` fromIntegral y :: Int64)++b8Bin op [VConstant (B8 x), VConstant (B8 y)] = Just $ VConstant (B8 (op x y))+b8Bin _ _ = Nothing++b8Un op [VConstant (B8 x)] = Just $ VConstant (B8 (op x))+b8Un _ _ = Nothing++b16Bin op [VConstant (B16 x), VConstant (B16 y)] = Just $ VConstant (B16 (op x y))+b16Bin _ _ = Nothing++b16Un op [VConstant (B16 x)] = Just $ VConstant (B16 (op x))+b16Un _ _ = Nothing++b32Bin op [VConstant (B32 x), VConstant (B32 y)] = Just $ VConstant (B32 (op x y))+b32Bin _ _ = Nothing++b32Un op [VConstant (B32 x)] = Just $ VConstant (B32 (op x))+b32Un _ _ = Nothing++b64Bin op [VConstant (B64 x), VConstant (B64 y)] = Just $ VConstant (B64 (op x y))+b64Bin _ _ = Nothing++b64Un op [VConstant (B64 x)] = Just $ VConstant (B64 (op x))+b64Un _ _ = Nothing++b8Cmp op [VConstant (B8 x), VConstant (B8 y)] = Just $ VConstant (I (if (op x y) then 1 else 0))+b8Cmp _ _ = Nothing++b16Cmp op [VConstant (B16 x), VConstant (B16 y)] = Just $ VConstant (I (if (op x y) then 1 else 0))+b16Cmp _ _ = Nothing++b32Cmp op [VConstant (B32 x), VConstant (B32 y)] = Just $ VConstant (I (if (op x y) then 1 else 0))+b32Cmp _ _ = Nothing++b64Cmp op [VConstant (B64 x), VConstant (B64 y)] = Just $ VConstant (I (if (op x y) then 1 else 0))+b64Cmp _ _ = Nothing++toB8 x = VConstant (B8 (fromIntegral x))+toB16 x = VConstant (B16 (fromIntegral x))+toB32 x = VConstant (B32 (fromIntegral x))+toB64 x = VConstant (B64 (fromIntegral x))++zext8_16 [VConstant (B8 x)] = Just $ toB16 x+zext8_16 _ = Nothing++zext8_32 [VConstant (B8 x)] = Just $ toB32 x+zext8_32 _ = Nothing++zext8_64 [VConstant (B8 x)] = Just $ toB64 x+zext8_64 _ = Nothing++sext8_16 [VConstant (B8 x)] = Just $ toB16 (fromIntegral x :: Int8)+sext8_16 _ = Nothing++sext8_32 [VConstant (B8 x)] = Just $ toB32 (fromIntegral x :: Int8)+sext8_32 _ = Nothing++sext8_64 [VConstant (B8 x)] = Just $ toB64 (fromIntegral x :: Int8)+sext8_64 _ = Nothing++zext16_32 [VConstant (B16 x)] = Just $ toB32 x+zext16_32 _ = Nothing++zext16_64 [VConstant (B16 x)] = Just $ toB64 x+zext16_64 _ = Nothing++sext16_32 [VConstant (B16 x)] = Just $ toB32 (fromIntegral x :: Int16)+sext16_32 _ = Nothing++sext16_64 [VConstant (B16 x)] = Just $ toB64 (fromIntegral x :: Int16)+sext16_64 _ = Nothing++trunc16_8 [VConstant (B16 x)] = Just $ toB8 x+trunc16_8 _ = Nothing++zext32_64 [VConstant (B32 x)] = Just $ toB64 x+zext32_64 _ = Nothing++sext32_64 [VConstant (B32 x)] = Just $ toB64 (fromIntegral x :: Int32)+sext32_64 _ = Nothing++trunc32_8 [VConstant (B32 x)] = Just $ toB8 x+trunc32_8 _ = Nothing++trunc32_16 [VConstant (B32 x)] = Just $ toB16 x+trunc32_16 _ = Nothing++trunc64_8 [VConstant (B64 x)] = Just $ toB8 x+trunc64_8 _ = Nothing++trunc64_16 [VConstant (B64 x)] = Just $ toB16 x+trunc64_16 _ = Nothing++trunc64_32 [VConstant (B64 x)] = Just $ toB32 x+trunc64_32 _ = Nothing++intToBits8 [VConstant (I x)] = Just $ toB8 x+intToBits8 _ = Nothing+intToBits16 [VConstant (I x)] = Just $ toB16 x+intToBits16 _ = Nothing+intToBits32 [VConstant (I x)] = Just $ toB32 x+intToBits32 _ = Nothing+intToBits64 [VConstant (I x)] = Just $ toB64 x+intToBits64 _ = Nothing++bits32ToInt [VConstant (B32 x)] = Just $ VConstant (I (fromIntegral x))+bits32ToInt _ = Nothing c_intToStr [VConstant (I x)] = Just $ VConstant (Str (show x)) c_intToStr _ = Nothing
src/Idris/Prover.hs view
@@ -13,8 +13,10 @@ import Idris.Parser import Idris.Error import Idris.DataOpts+import Idris.Completion import System.Console.Haskeline+import System.Console.Haskeline.History import Control.Monad.State import Util.Pretty@@ -22,7 +24,7 @@ prover :: Bool -> Name -> Idris () prover lit x = do ctxt <- getContext- i <- get+ i <- getIState case lookupTy Nothing x ctxt of [t] -> if elem x (idris_metavars i) then prove ctxt lit x t@@ -37,15 +39,23 @@ where bird = if lit then "> " else "" break = "\n" ++ bird +proverSettings :: ElabState [PDecl] -> Settings Idris+proverSettings e = setComplete (proverCompletion assumptionNames) defaultSettings+ where assumptionNames = case envAtFocus (proof e) of+ OK env -> names env+ names [] = []+ names ((MN _ _, _) : bs) = names bs+ names ((n, _) : bs) = show n : names bs+ prove :: Context -> Bool -> Name -> Type -> Idris () prove ctxt lit n ty - = do let ps = initElaborator n ctxt ty - (tm, prf) <- ploop True ("-" ++ show n) [] (ES (ps, []) "" Nothing)+ = do let ps = initElaborator n ctxt ty+ (tm, prf) <- ploop True ("-" ++ show n) [] (ES (ps, []) "" Nothing) Nothing iLOG $ "Adding " ++ show tm iputStrLn $ showProof lit n prf- i <- get+ i <- getIState let proofs = proof_list i- put (i { proof_list = (n, prf) : proofs })+ putIState (i { proof_list = (n, prf) : proofs }) let tree = simpleCase False True CompileTime (FC "proof" 0) [([], P Ref n ty, tm)] logLvl 3 (show tree) (ptm, pty) <- recheckC (FC "proof" 0) [] tm@@ -58,7 +68,7 @@ elabStep :: ElabState [PDecl] -> ElabD a -> Idris (a, ElabState [PDecl]) elabStep st e = do case runStateT e st of OK (a, st') -> return (a, st')- Error a -> do i <- get+ Error a -> do i <- getIState fail (pshow i a) dumpState :: IState -> ProofState -> IO ()@@ -108,18 +118,25 @@ lifte st e = do (v, _) <- elabStep st e return v -ploop :: Bool -> String -> [String] -> ElabState [PDecl] -> Idris (Term, [String])-ploop d prompt prf e - = do i <- get+ploop :: Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])+ploop d prompt prf e h+ = do i <- getIState when d $ liftIO $ dumpState i (proof e)- x <- lift $ getInputLine (prompt ++ "> ")+ (x, h') <- runInputT (proverSettings e) $+ -- Manually track the history so that we can use the proof state+ do _ <- case h of+ Just history -> putHistory history+ Nothing -> return ()+ l <- getInputLine (prompt ++ "> ")+ h' <- getHistory+ return (l, Just h') (cmd, step) <- case x of Nothing -> fail "Abandoned" Just input -> do return (parseTac i input, input) case cmd of Right Abandon -> fail "Abandoned" _ -> return ()- (d, st, done, prf') <- idrisCatch + (d, st, done, prf') <- idrisCatch (case cmd of Left err -> do iputStrLn (show err) return (False, e, False, prf)@@ -140,7 +157,7 @@ return (True, st, False, prf ++ [step])) (\err -> do iputStrLn (show err) return (False, e, False, prf))- if done then do (tm, _) <- elabStep st get_term + if done then do (tm, _) <- elabStep st get_term return (tm, prf')- else ploop d prompt prf' st+ else ploop d prompt prf' st h'
src/Idris/REPL.hs view
@@ -16,6 +16,7 @@ import Idris.Coverage import Idris.UnusedArgs import Idris.Docs+import Idris.Completion import Paths_idris import Util.System@@ -49,23 +50,23 @@ import Data.Char import Data.Version -repl :: IState -> [FilePath] -> Idris ()+repl :: IState -> [FilePath] -> InputT Idris () repl orig mods = H.catch (do let prompt = mkPrompt mods- x <- lift $ getInputLine (prompt ++ "> ")+ x <- getInputLine (prompt ++ "> ") case x of- Nothing -> do iputStrLn "Bye bye"+ Nothing -> do lift $ iputStrLn "Bye bye" return () Just input -> H.catch - (do ms <- processInput input orig mods+ (do ms <- lift $ processInput input orig mods case ms of Just mods -> repl orig mods Nothing -> return ()) ctrlC) ctrlC- where ctrlC :: SomeException -> Idris ()- ctrlC e = do iputStrLn (show e)+ where ctrlC :: SomeException -> InputT Idris ()+ ctrlC e = do lift $ iputStrLn (show e) repl orig mods mkPrompt [] = "Idris"@@ -78,7 +79,7 @@ processInput :: String -> IState -> [FilePath] -> Idris (Maybe [FilePath]) processInput cmd orig inputs- = do i <- get+ = do i <- getIState let fn = case inputs of (f:_) -> f _ -> ""@@ -86,12 +87,12 @@ Left err -> do liftIO $ print err return (Just inputs) Right Reload -> - do put (orig { idris_options = idris_options i })+ do putIState (orig { idris_options = idris_options i }) clearErr mods <- mapM loadModule inputs return (Just inputs) Right (Load f) -> - do put (orig { idris_options = idris_options i })+ do putIState (orig { idris_options = idris_options i }) clearErr mod <- loadModule f return (Just [f])@@ -111,7 +112,7 @@ resolveProof :: Name -> Idris Name resolveProof n'- = do i <- get+ = do i <- getIState ctxt <- getContext n <- case lookupNames Nothing n' ctxt of [x] -> return x@@ -121,15 +122,15 @@ removeProof :: Name -> Idris () removeProof n =- do i <- get+ do i <- getIState let proofs = proof_list i let ps = filter ((/= n) . fst) proofs- put $ i { proof_list = ps }+ putIState $ i { proof_list = ps } edit :: FilePath -> IState -> Idris () edit "" orig = iputStrLn "Nothing to edit" edit f orig- = do i <- get+ = do i <- getIState env <- liftIO $ getEnvironment let editor = getEditor env let line = case errLine i of@@ -138,7 +139,7 @@ let cmd = editor ++ line ++ f liftIO $ system cmd clearErr- put (orig { idris_options = idris_options i })+ putIState (orig { idris_options = idris_options i }) loadModule f iucheck return ()@@ -149,7 +150,7 @@ proofs :: IState -> Idris () proofs orig- = do i <- get+ = do i <- getIState let ps = proof_list i case ps of [] -> iputStrLn "No proofs available"@@ -166,7 +167,7 @@ process fn (Eval t) = do (tm, ty) <- elabVal toplevel False t ctxt <- getContext- ist <- get + ist <- getIState let tm' = normaliseAll ctxt [] tm let ty' = normaliseAll ctxt [] ty logLvl 3 $ "Raw: " ++ show (tm', ty')@@ -186,7 +187,7 @@ where fc = FC "(input)" 0 process fn (Check (PRef _ n)) = do ctxt <- getContext- ist <- get+ ist <- getIState imp <- impShow case lookupTy Nothing n ctxt of ts@(_:_) -> mapM_ (\t -> iputStrLn $ show n ++ " : " ++@@ -194,20 +195,20 @@ [] -> iputStrLn $ "No such variable " ++ show n process fn (Check t) = do (tm, ty) <- elabVal toplevel False t ctxt <- getContext- ist <- get + ist <- getIState imp <- impShow let ty' = normaliseC ctxt [] ty iputStrLn (showImp imp (delab ist tm) ++ " : " ++ showImp imp (delab ist ty)) -process fn (DocStr n) = do i <- get+process fn (DocStr n) = do i <- getIState case lookupCtxtName Nothing n (idris_docstrings i) of [] -> iputStrLn $ "No documentation for " ++ show n ns -> mapM_ showDoc ns where showDoc (n, d) = do doc <- getDocs n iputStrLn $ show doc-process fn Universes = do i <- get+process fn Universes = do i <- getIState let cs = idris_constraints i -- iputStrLn $ showSep "\n" (map show cs) liftIO $ print (map fst cs)@@ -216,7 +217,7 @@ case ucheck cs of Error e -> iputStrLn $ pshow i e OK _ -> iputStrLn "Universes OK"-process fn (Defn n) = do i <- get+process fn (Defn n) = do i <- getIState iputStrLn "Compiled patterns:\n" liftIO $ print (lookupDef Nothing n (tt_ctxt i)) case lookupCtxt Nothing n (idris_patdefs i) of@@ -230,40 +231,42 @@ = do liftIO $ putStr $ showImp True (delab i lhs) liftIO $ putStr " = " liftIO $ putStrLn $ showImp True (delab i rhs)-process fn (TotCheck n) = do i <- get+process fn (TotCheck n) = do i <- getIState case lookupTotal n (tt_ctxt i) of [t] -> iputStrLn (showTotal t i) _ -> return () process fn (DebugInfo n) - = do i <- get+ = do i <- getIState let oi = lookupCtxtName Nothing n (idris_optimisation i) when (not (null oi)) $ iputStrLn (show oi) let si = lookupCtxt Nothing n (idris_statics i) when (not (null si)) $ iputStrLn (show si)+ let di = lookupCtxt Nothing n (idris_datatypes i)+ when (not (null di)) $ iputStrLn (show di) let d = lookupDef Nothing n (tt_ctxt i) when (not (null d)) $ liftIO $ do print (head d) let cg = lookupCtxtName Nothing n (idris_callgraph i) findUnusedArgs (map fst cg)- i <- get+ i <- getIState let cg' = lookupCtxtName Nothing n (idris_callgraph i) sc <- checkSizeChange n iputStrLn $ "Size change: " ++ show sc when (not (null cg')) $ do iputStrLn "Call graph:\n" iputStrLn (show cg')-process fn (Info n) = do i <- get+process fn (Info n) = do i <- getIState case lookupCtxt Nothing n (idris_classes i) of [c] -> classInfo c _ -> iputStrLn "Not a class" process fn (Search t) = iputStrLn "Not implemented" process fn (Spec t) = do (tm, ty) <- elabVal toplevel False t ctxt <- getContext- ist <- get+ ist <- getIState let tm' = simplify ctxt True [] {- (idris_statics ist) -} tm iputStrLn (show (delab ist tm')) process fn (RmProof n')- = do i <- get+ = do i <- getIState n <- resolveProof n' let proofs = proof_list i case lookup n proofs of@@ -274,15 +277,15 @@ where insertMetavar :: Name -> Idris () insertMetavar n =- do i <- get+ do i <- getIState let ms = idris_metavars i- put $ i { idris_metavars = n : ms }+ putIState $ i { idris_metavars = n : ms } process fn (AddProof prf) = do let fb = fn ++ "~" liftIO $ copyFile fn fb -- make a backup in case something goes wrong! prog <- liftIO $ readFile fb- i <- get+ i <- getIState let proofs = proof_list i n' <- case prf of Nothing -> case proofs of@@ -299,7 +302,7 @@ where ls = (lines prog) process fn (ShowProof n')- = do i <- get+ = do i <- getIState n <- resolveProof n' let proofs = proof_list i case lookup n proofs of@@ -308,26 +311,26 @@ process fn (Prove n') = do ctxt <- getContext- ist <- get+ ist <- getIState n <- case lookupNames Nothing n' ctxt of [x] -> return x [] -> return n' ns -> fail $ pshow ist (CantResolveAlts (map show ns)) prover (lit fn) n -- recheck totality- i <- get+ i <- getIState totcheck (FC "(input)" 0, n) mapM_ (\ (f,n) -> setTotality n Unchecked) (idris_totcheck i) mapM_ checkDeclTotality (idris_totcheck i) process fn (HNF t) = do (tm, ty) <- elabVal toplevel False t ctxt <- getContext- ist <- get+ ist <- getIState let tm' = hnf ctxt [] tm iputStrLn (show (delab ist tm'))-process fn TTShell = do ist <- get+process fn TTShell = do ist <- getIState let shst = initState (tt_ctxt ist)- shst' <- lift $ runShell shst+ runShell shst return () process fn Execute = do (m, _) <- elabVal toplevel False (PApp fc @@ -359,7 +362,7 @@ = do (tm, ty) <- elabVal toplevel True t iputStrLn $ show tm ++ "\n\n : " ++ show ty -process fn (Missing n) = do i <- get+process fn (Missing n) = do i <- getIState case lookupDef Nothing n (tt_ctxt i) of [CaseOp _ _ _ _ _ args t _ _] -> do tms <- genMissing n args t@@ -367,7 +370,7 @@ [] -> iputStrLn $ show n ++ " undefined" _ -> iputStrLn $ "Ambiguous name" process fn Metavars - = do ist <- get+ = do ist <- getIState let mvs = idris_metavars ist \\ primDefs case mvs of [] -> iputStrLn "No global metavariables to solve"@@ -394,7 +397,7 @@ dumpMethod (n, (_, t)) = iputStrLn $ show n ++ " : " ++ show t dumpInstance :: Name -> Idris ()-dumpInstance n = do i <- get+dumpInstance n = do i <- getIState ctxt <- getContext imp <- impShow case lookupTy Nothing n ctxt of@@ -420,7 +423,8 @@ parseTarget "C" = ViaC parseTarget "Java" = ViaJava parseTarget "bytecode" = Bytecode-parseTarget "javascript" = ToJavaScript+parseTarget "javascript" = ViaJavaScript+parseTarget "node" = ViaNode parseTarget _ = error "unknown target" -- FIXME: partial function parseArgs :: [String] -> [Opt]@@ -487,12 +491,16 @@ ([":q",":quit"], "", "Exit the Idris system") ] ++replSettings :: Settings Idris+replSettings = setComplete replCompletion defaultSettings+ -- invoke as if from command line idris :: [Opt] -> IO IState-idris opts = runInputT defaultSettings $ execStateT (idrisMain opts) idrisInit+idris opts = execStateT (idrisMain opts) idrisInit idrisMain :: [Opt] -> Idris ()-idrisMain opts = +idrisMain opts = do let inputs = opt getFile opts let runrepl = not (NoREPL `elem` opts) let output = opt getOutput opts@@ -508,8 +516,8 @@ let tgt = case opt getTarget opts of [] -> ViaC xs -> last xs- when (DefaultTotal `elem` opts) $ do i <- get- put (i { default_total = True })+ when (DefaultTotal `elem` opts) $ do i <- getIState+ putIState (i { default_total = True }) setREPL runrepl setVerbose runrepl setCmdLine opts@@ -534,8 +542,8 @@ elabPrims when (not (NoPrelude `elem` opts)) $ do x <- loadModule "Prelude" return ()- when runrepl $ iputStrLn banner - ist <- get+ when runrepl $ iputStrLn banner+ ist <- getIState mods <- mapM loadModule inputs ok <- noErrors when ok $ case output of@@ -544,7 +552,7 @@ when ok $ case newoutput of [] -> return () (o:_) -> process "" (NewCompile o) - when runrepl $ repl ist inputs+ when runrepl $ runInputT replSettings $ repl ist inputs ok <- noErrors when (not ok) $ liftIO (exitWith (ExitFailure 1)) where
src/Idris/REPLParser.hs view
@@ -33,7 +33,7 @@ <|> try (do cmd ["ttshell"]; eof; return TTShell) <|> try (do cmd ["c", "compile"]; f <- identifier; eof; return (Compile ViaC f)) <|> try (do cmd ["jc", "newcompile"]; f <- identifier; eof; return (Compile ViaJava f))- <|> try (do cmd ["js", "javascript"]; f <- identifier; eof; return (Compile ToJavaScript f))+ <|> try (do cmd ["js", "javascript"]; f <- identifier; eof; return (Compile ViaJavaScript f)) <|> try (do cmd ["nc", "newcompile"]; f <- identifier; eof; return (NewCompile f)) <|> try (do cmd ["m", "metavars"]; eof; return Metavars) <|> try (do cmd ["proofs"]; eof; return Proofs)
src/Idris/UnusedArgs.hs view
@@ -14,7 +14,7 @@ traceUnused :: Name -> Idris () traceUnused n - = do i <- get+ = do i <- getIState case lookupCtxt Nothing n (idris_callgraph i) of [CGInfo args calls scg usedns _] -> do let argpos = zip args [0..]@@ -38,7 +38,7 @@ | (g, j) `elem` path = return False -- cycle, never used on the way | otherwise = do logLvl 5 $ (show ((g, j) : path)) - i <- get+ i <- getIState case lookupCtxt Nothing g (idris_callgraph i) of [CGInfo args calls scg usedns unused] -> if (j >= length args)
src/Main.hs view
@@ -39,7 +39,7 @@ main = do xs <- getArgs let opts = parseArgs xs- runInputT defaultSettings $ execStateT (runIdris opts) idrisInit+ execStateT (runIdris opts) idrisInit runIdris :: [Opt] -> Idris () runIdris opts = do@@ -92,4 +92,4 @@ "\t--libdir Show library install directory and exit\n" ++ "\t--link Show C library directories and exit (for C linking)\n" ++ "\t--include Show C include directories and exit (for C linking)\n" ++- "\t--target [target] Type the target: C, Java, bytecode, javascript\n"+ "\t--target [target] Type the target: C, Java, bytecode, javascript, node\n"
tutorial/examples/binary.idr view
@@ -6,11 +6,9 @@ bI : Binary n -> Binary (S (n + n)) instance Show (Binary n) where- show = show' where- show' : Binary n' -> String- show' (bO x) = show x ++ "0"- show' (bI x) = show x ++ "1"- show' bEnd = ""+ show (bO x) = show x ++ "0"+ show (bI x) = show x ++ "1"+ show bEnd = "" data Parity : Nat -> Type where even : Parity (n + n)
tutorial/examples/interp.idr view
@@ -44,6 +44,9 @@ eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt)) eAdd = Lam (Lam (Op (+) (Var stop) (Var (pop stop))))++ eEq : Expr G (TyFun TyInt (TyFun TyInt TyBool))+ eEq = Lam (Lam (Op (==) (Var stop) (Var (pop stop)))) eDouble : Expr G (TyFun TyInt TyInt) eDouble = Lam (App (App eAdd (Var stop)) (Var stop))