pisigma 0.1.0.3 → 0.2
raw patch · 28 files changed
+674/−1167 lines, 28 filesdep +containersdep ~array
Dependencies added: containers
Dependency ranges changed: array
Files
- examples/Bool.pi +32/−0
- examples/Broken.pi +0/−9
- examples/Conat.pi +35/−29
- examples/Curry.pi +3/−3
- examples/Equal.pi +9/−9
- examples/Fin.pi +6/−5
- examples/Foo.pi +0/−1
- examples/Id.pi +12/−0
- examples/Nat.pi +30/−27
- examples/Parser.pi +41/−89
- examples/Parser2.pi +0/−331
- examples/Parser3.pi +0/−331
- examples/Streams.pi +20/−19
- examples/SubjectReduction.pi +0/−58
- examples/Universe.pi +34/−0
- examples/Vec.pi +2/−2
- examples/stl.pi +34/−27
- pisigma.cabal +26/−7
- src/Language/PiSigma/Check.hs +104/−75
- src/Language/PiSigma/Equality.hs +22/−14
- src/Language/PiSigma/Evaluate.hs +17/−25
- src/Language/PiSigma/Lexer.hs +6/−2
- src/Language/PiSigma/Normalise.hs +27/−19
- src/Language/PiSigma/Parser.hs +135/−51
- src/Language/PiSigma/Pretty.hs +43/−20
- src/Language/PiSigma/Syntax.hs +33/−11
- src/Tools/Interpreter/Main.hs +1/−1
- src/Tools/Interpreter/REPL.hs +2/−2
examples/Bool.pi view
@@ -13,3 +13,35 @@ andb = \ b c -> case b of { true -> c | false -> 'false };++orb : Bool -> Bool -> Bool;+orb = \ b c -> case b of {+ true -> 'true+ | false -> c };++eqBool : Bool -> Bool -> Bool;+eqBool = \ b1 b2 -> + case b1 of+ { true -> case b2 of { true -> 'true | false -> 'false} + | false -> case b2 of { true -> 'false | false -> 'true}}; ++EqBool : Bool -> Bool -> Type;+EqBool = \b1 b2 -> T(eqBool b1 b2);++reflBool : (b : Bool) -> EqBool b b;+reflBool = \ b -> case b of+ { true -> 'unit+ | false -> 'unit}; ++substBool : (P : Bool -> Type) -> + (b1 b2 : Bool)+ -> (EqBool b1 b2)+ -> P b1 -> P b2;+substBool = \ P b1 b2 m m1 ->+ case b1 of+ {true -> case b2 of+ { true -> m1+ | false -> case m of {}}+ | false -> case b2 of+ { true -> case m of {}+ | false -> m1}};
− examples/Broken.pi
@@ -1,9 +0,0 @@-Bool : Type;-Bool = { true false };--broken : Bool -> Bool;-broken = \ b -> case b of {- true -> 'true- | true -> 'true- | false -> 'true };-
examples/Conat.pi view
@@ -1,70 +1,74 @@ :l Empty.pi :l Unit.pi -Nat' : Type;-Nat' = (l : { z s }) * case l of {+CoNat : Type;+CoNat = (l : { z s }) * case l of { z -> Unit- | s -> [^ Nat'] };+ | s -> Rec [^ CoNat] }; -zero : Nat';+zero : CoNat; zero = ('z,'unit); -succ : ^Nat' -> Nat';-succ = \ n -> ('s,n);+succ : ^CoNat -> CoNat;+succ = \ n -> ('s,fold n); -one : Nat';+one : CoNat; one = succ [zero]; -two : Nat';+two : CoNat; two = succ [one]; -omega : Nat';+omega : CoNat; omega = succ [omega]; -add : Nat' -> Nat' -> Nat';+add : CoNat -> CoNat -> CoNat; add = \ m n -> split m with (lm , m') -> case lm of { z -> n- | s -> succ [add (!m') n] };+ | s -> succ [add (! (unfold m')) n] }; -eq : Nat' -> Nat' -> Type;-eq = \ m n -> split m with (lm , m') ->+EqCoNat : CoNat -> CoNat -> Type;+EqCoNat = \ m n -> split m with (lm , m') -> split n with (ln , n') -> case lm of {- z -> case ln of { + z -> case ln of { z -> Unit | s -> Empty }- | s -> case ln of { + | s -> case ln of { z -> Empty- | s -> [^ (eq (! m') (! n'))]}};+ | s -> Rec [^ (EqCoNat (! (unfold m')) (! (unfold n')))]}}; -refl : (n:Nat') -> eq n n;-refl = \ n -> split n with (ln , n') ->+reflCoNat : (n:CoNat) -> EqCoNat n n;+reflCoNat = \ n -> split n with (ln , n') -> case ln of { z -> 'unit- | s -> [refl (!n')] };+ | s -> fold [reflCoNat (! (unfold n'))] }; -sym : (m:Nat') -> (n:Nat') -> eq m n -> eq n m;-sym = \ m n p -> +symCoNat : (m n:CoNat) -> EqCoNat m n -> EqCoNat n m;+symCoNat = \ m n p -> split m with (lm , m') -> split n with (ln , n') -> case lm of { z -> case ln of { z -> 'unit | s -> case p of {}}- | s -> case ln of { + | s -> case ln of { z -> case p of {}- | s -> [sym (! m') (! n') (! p)] }};+ | s -> fold [symCoNat (! (unfold m')) (! (unfold n')) (! (unfold p))] }}; +transCoNat : (l m n:CoNat) -> EqCoNat l m -> EqCoNat m n -> EqCoNat l n;+--transCoNat = \ l m n p q ->+ + {--subst : (P : Nat' -> Type) - -> (m : Nat') -> (n : Nat')- -> (eq m n)+subst : (P : CoNat -> Type)+ -> (m : CoNat) -> (n : CoNat)+ -> (EqCoNat m n) -> P m -> ^ (P n);-subst = \ P m n q x -> +subst = \ P m n q x -> split m with (lm , m') -> split n with (ln , n') -> case lm of {@@ -73,9 +77,11 @@ unit -> case n' of { unit -> [x] }} | s -> case q of {}}- | s -> case ln of { + | s -> case ln of { z -> case q of {}- | s -> [subst (\ i -> P (succ i)) (! m') (! n') (! q) x]}};+ | s -> [unfold m' as m' ->+ unfold n' as n' ->+ subst (\ i -> P (succ [i])) (! m') (! n') (! q) x]}}; -} {- seems we need an eliminator for boxes, e.g. unbox
examples/Curry.pi view
@@ -4,10 +4,10 @@ -- Curry's paradox (usually ruled out by positivity check). A : Type;-A = [A] → ⊥;+A = Rec [A] → ⊥; ¬A : A → ⊥;-¬A = λ x → x x;+¬A = λ x → x (fold x); contradiction : ⊥;-contradiction = ¬A (λ x → ¬A x);+contradiction = ¬A (λ x → ¬A (unfold x));
examples/Equal.pi view
@@ -81,7 +81,7 @@ {- works, uses bet equality in contexts. -} t11a : Eq (^(^A)) [let x:A=a in [x]] [let y:A=a in [y]]- = refl (^(^A)) [let x:A=a in [x]]; + = refl (^(^A)) [let x:A=a in [x]]; {- works now -} t12 : Eq (^A) (let y:A=y in [y]) (let z:A=z in [z])@@ -94,21 +94,21 @@ -} Stream : Type;-Stream = A * [∞ Stream];+Stream = A * Rec [∞ Stream]; -as : Stream;-as = (a, [as]);+as' : Stream;+as' = (a, fold [as']); repeat : (x : A) → Stream;-repeat = λ x → (x, [repeat x]);+repeat = λ x → (x, fold [repeat x]); --- as is equal to its unfolding.+-- as' is equal to its unfolding. -unfolds : Eq Stream as (a, [as]);-unfolds = refl Stream as;+unfolds : Eq Stream as' (a, fold [as']);+unfolds = refl Stream as'; -- repeat a is not equal to its unfolding. {--doesNotUnfold : Eq Stream (repeat a) (a, [repeat a]);+doesNotUnfold : Eq Stream (repeat a) (a, fold [repeat a]); doesNotUnfold = refl Stream (repeat a); -}
examples/Fin.pi view
@@ -6,7 +6,7 @@ z -> [Empty] | s -> [(l : { z s }) * case l of { z -> Unit- | s -> Fin n'}]};+ | s -> Fin (unfold n')}]}; fz : (n:Nat) -> Fin (succ n); fz = \ n -> ('z , 'unit );@@ -18,7 +18,7 @@ fmax = \ n -> split n with (ln , n') -> ! case ln of { z -> [fz zero]- | s -> [fs n (fmax n')] };+ | s -> [fs n (fmax (unfold n'))] }; femb : (n:Nat) -> Fin n -> Fin (succ n); femb = \ n i -> split n with (ln , n') ->@@ -27,7 +27,7 @@ | s -> split i with (li , i') -> case li of { z -> [fz n]- | s -> [fs n (femb n' i')] }};+ | s -> [fs n (femb (unfold n') i')] }}; finv : (n:Nat) -> Fin n -> Fin n; finv = \ n i -> split n with (ln , n') ->@@ -35,6 +35,7 @@ z -> case i of {} | s -> split i with (li , i') -> case li of {- z -> [fmax n']- | s -> [fs n' (finv n' i')] }};+ z -> [fmax (unfold n')]+ | s -> [unfold n' as n' ->+ fs n' (finv n' i')] }};
− examples/Foo.pi
@@ -1,1 +0,0 @@-Nat
+ examples/Id.pi view
@@ -0,0 +1,12 @@+Id : (A:Type) -> A -> A -> Type;+refl : (A:Type) -> (a:A) -> Id A a a;++J : (A:Type) -> (P:(a:A) -> (b:A) -> Id A a b -> Type) + -> ((a:A) -> P a a (refl A a))+ -> (a:A) -> (b:A) -> (p : Id A a b) -> P a b p;++forceEq : (A:Type) -> (a : ^A) -> Id (^A) a [!a];+{-+forceEq = \ A a -> unbox a with [x] -> refl (^A) [x]+should not typecheck!+-}
examples/Nat.pi view
@@ -3,13 +3,13 @@ Nat : Type; Nat = (l : { z s }) * case l of { z -> Unit- | s -> [Nat] };+ | s -> Rec [Nat] }; zero : Nat; zero = ('z,'unit); succ : Nat -> Nat;-succ = \ n -> ('s,n);+succ = \ n -> ('s,fold n); one : Nat; one = succ zero;@@ -21,34 +21,34 @@ add = \ m n -> split m with (lm , m') -> ! case lm of { z -> [n]- | s -> [succ (add m' n)] };+ | s -> [succ (add (unfold m') n)] }; -eqbNat : Nat -> Nat -> Bool;-eqbNat = \ m n -> split m with (lm , m') ->+eqNat : Nat -> Nat -> Bool;+eqNat = \ m n -> split m with (lm , m') -> split n with (ln , n') -> ! case lm of {- z -> case ln of { + z -> case ln of { z -> ['true] | s -> ['false] } | s -> case ln of { z -> ['false]- | s -> [eqbNat m' n'] } };+ | s -> [eqNat (unfold m') (unfold n')] } }; -eqNat : Nat -> Nat -> Type;-eqNat = \ m n -> T (eqbNat m n);+EqNat : Nat -> Nat -> Type;+EqNat = \ m n -> T (eqNat m n); -reflNat : (n:Nat) -> eqNat n n;+reflNat : (n:Nat) -> EqNat n n; reflNat = \ n -> split n with (ln , n') -> ! case ln of { z -> ['unit]- | s -> [reflNat n'] };+ | s -> [reflNat (unfold n')] }; -substNat : (P : Nat -> Type) +substNat : (P : Nat -> Type) -> (m : Nat) -> (n : Nat)- -> (eqNat m n)+ -> (EqNat m n) -> P m -> P n;-substNat = \ P m n q x -> +substNat = \ P m n q x -> split m with (lm , m') -> split n with (ln , n') -> ! case lm of {@@ -57,38 +57,41 @@ unit -> case n' of { unit -> [x]}} | s -> case q of {}}- | s -> case ln of { + | s -> case ln of { z -> case q of {}- | s -> [substNat (\ i -> P (succ i)) m' n' q x]}};+ | s -> [unfold m' as m' ->+ unfold n' as n' ->+ substNat (\ i -> P (succ i)) m' n' q x]}}; -symNat : (m:Nat) -> (n:Nat) -> eqNat m n -> eqNat n m;-symNat = \ m n p -> substNat (\ i -> eqNat i m) m n p (reflNat m);+symNat : (m:Nat) -> (n:Nat) -> EqNat m n -> EqNat n m;+symNat = \ m n p -> substNat (\ i -> EqNat i m) m n p (reflNat m); transNat : (i:Nat) -> (j:Nat) -> (k:Nat) ->- eqNat i j -> eqNat j k -> eqNat i k;-transNat = \ i j k p q -> substNat (\ x -> eqNat i x) j k q p;+ EqNat i j -> EqNat j k -> EqNat i k;+transNat = \ i j k p q -> substNat (\ x -> EqNat i x) j k q p; -addCom0 : (n:Nat) -> eqNat n (add n zero);+addCom0 : (n:Nat) -> EqNat n (add n zero); addCom0 = \ n -> split n with (ln , n') ->- ! case ln of { + ! case ln of { z -> case n' of { unit -> [reflNat zero]}- | s -> [addCom0 n'] };+ | s -> [addCom0 (unfold n')] }; addComS : (m:Nat) -> (n:Nat) ->- (eqNat (add (succ m) n) (add m (succ n)));+ (EqNat (add (succ m) n) (add m (succ n))); addComS = \ m n -> split m with (lm , m') -> ! case lm of { z -> [reflNat (succ n)]- | s -> [addComS m' n] };+ | s -> [addComS (unfold m') n] }; addCom : (m:Nat) -> (n:Nat) ->- (eqNat (add m n) (add n m));+ (EqNat (add m n) (add n m)); addCom = \ m n -> split m with (lm , m') -> ! case lm of { z -> case m' of { unit -> [addCom0 n] }- | s -> [transNat (add (succ m') n) (add (succ n) m') (add n (succ m'))+ | s -> [unfold m' as m' ->+ transNat (add (succ m') n) (add (succ n) m') (add n (succ m')) (addCom m' n) (addComS n m')] };
examples/Parser.pi view
@@ -1,89 +1,41 @@-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;-Nat : type;+:l Bool.pi++andb' : Bool -> Bool -> Bool;+andb' = \ b c -> case c of {+ true -> b+ | false -> 'false };++inftyOpt : Type -> Bool -> Type+ = \ A b -> case b of {+ true -> A+ | false -> ^ A };++boxOpt : (b:Bool) -> (A:Type) -> A -> inftyOpt A b+ = \ b A a -> case b of { true -> a+ | false -> [a] };++forceOpt : (b:Bool) -> (A:Type) -> inftyOpt A b -> A + = \ b A a -> case b of { true -> a+ | false -> !a };++Tok : Type;++P : Bool -> Type+ = \ b -> (l : { fail empty sat alt seq } ) *+ case l of {+ fail -> EqBool 'false b+ | empty -> EqBool 'true b+ | sat -> (Tok -> Bool) * (EqBool 'false b)+ | alt -> (n1 n2 : Bool) * Rec [P n1] * Rec [P n2] * (EqBool (orb n1 n2) b)+ | seq -> (n1 n2 : Bool) * inftyOpt (Rec [P n1]) n2 *+ inftyOpt (Rec [P n2]) n1 * (EqBool (andb' n1 n2) b) };+++star : P 'false -> P 'true;+plus : P 'false -> P 'false;++star = \ p -> ('alt , ('true, ('false, (fold ('empty, reflBool 'true),+ (fold (plus p),+ reflBool 'false)))));++plus = \ p -> ('seq, ('false, ('true, (fold p, ([fold (star p)], reflBool 'false)) )) );
− examples/Parser2.pi
@@ -1,331 +0,0 @@-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;-Nat;
− examples/Parser3.pi
@@ -1,331 +0,0 @@-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat-Nat
examples/Streams.pi view
@@ -16,13 +16,13 @@ Nat : Type; Nat = (l : { z s }) * case l of { z -> Unit- | s -> [Nat] };+ | s -> Rec [Nat] }; zero : Nat; zero = ('z,'unit); succ : Nat -> Nat;-succ = \ n -> ('s,n);+succ = \ n -> ('s, fold n); one : Nat; one = succ zero;@@ -34,18 +34,18 @@ add = \ m n -> split m with (lm , m') -> ! case lm of { z -> [n]- | s -> [succ (add m' n)] };+ | s -> [succ (add (unfold m') n)] }; eqbNat : Nat -> Nat -> Bool; eqbNat = \ m n -> split m with (lm , m') -> split n with (ln , n') -> ! case lm of {- z -> case ln of { + z -> case ln of { z -> ['true] | s -> ['false] } | s -> case ln of { z -> ['false]- | s -> [eqbNat m' n'] } };+ | s -> [eqbNat (unfold m') (unfold n')] } }; eqNat : Nat -> Nat -> Type; eqNat = \ m n -> T (eqbNat m n);@@ -54,38 +54,39 @@ reflNat = \ n -> split n with (ln , n') -> ! case ln of { z -> ['unit]- | s -> [reflNat n'] };+ | s -> [reflNat (unfold n')] }; Stream : Type -> Type;-Stream = \ a -> a * [^ (Stream a)];+Stream = \ a -> a * Rec [^ (Stream a)]; put : (a : Type) -> a -> Stream a -> Stream a;-put = \ a x xs -> (x,[xs]);+put = \ a x xs -> (x, fold [xs]); from : Nat -> Stream Nat;-from = \ n -> (n, [from (succ n)]);+from = \ n -> (n, fold [from (succ n)]); tail : (a:Type) -> Stream a -> Stream a;-tail = \ a xs -> split xs with (x , xs') -> ! xs';+tail = \ a xs -> split xs with (x , xs') -> ! (unfold xs'); head : (a:Type) -> Stream a -> a; head = \ a xs -> split xs with (x , xs') -> x; map : (a : Type) -> (b : Type) -> (a -> b) -> Stream a -> Stream b;-map = \ a b f xs -> split xs with (x , xs') -> (f x, [map a b f (! xs')]);+map = \ a b f xs -> split xs with (x , xs') -> (f x, fold [map a b f (! (unfold xs'))]); eqStream : (a : Type) -> (a -> a -> Type) -> Stream a -> Stream a -> Type;-eqStream = \ a eq xs ys -> split xs with (x , xs') ->- split ys with (y , ys') ->- (eq x y) * [^ (eqStream a eq (! xs') (! ys'))];+eqStream = \ a eq xs ys ->+ split xs with (x , xs') ->+ split ys with (y , ys') ->+ eq x y * Rec [^ (eqStream a eq (! (unfold xs')) (! (unfold ys')))]; -reflStream : (a : Type) -> (eq : a -> a -> Type) +reflStream : (a : Type) -> (eq : a -> a -> Type) -> ((x : a) -> eq x x) -> (xs : Stream a) -> eqStream a eq xs xs;-reflStream = \ a eq refl xs -> split xs with (x , xs') -> - ((refl x), [reflStream a eq refl (! xs')]);+reflStream = \ a eq refl xs -> split xs with (x , xs') ->+ (refl x, fold [reflStream a eq refl (! (unfold xs'))]); -lemma : (n : Nat) -> eqStream Nat eqNat (from (succ n)) +lemma : (n : Nat) -> eqStream Nat eqNat (from (succ n)) (map Nat Nat succ (from n));-lemma = \ n -> ((reflNat (succ n)),[lemma (succ n)]); +lemma = \ n -> ((reflNat (succ n)), fold [lemma (succ n)]);
− examples/SubjectReduction.pi
@@ -1,58 +0,0 @@--- Context:--- Recursion with boxes--- Thorsten Altenkirch--- http://sneezy.cs.nott.ac.uk/fplunch/weblog/?p=104--Stream : Type;-Stream = [∞ Stream];--ticks : Stream;-ticks = [ticks];--Eq : (A : Type) → A → A → Type;-Eq = λ A x y → (P : A → Type) → P x → P y;--refl : (A : Type) → (x : A) → Eq A x x;-refl = λ A x P px → px;--unfold : Eq Stream ticks [ticks];-unfold = refl Stream ticks;---- We can prove this variant of congruence for boxes:--cong : (xs ys : Stream) → Eq Stream xs ys →- Eq Stream [let zs : Stream = xs in zs]- [let zs : Stream = ys in zs];-cong = λ xs ys eq P p → eq (λ zs → P [let us : Stream = zs in us]) p;---- This does not (obviously) break subject reduction, because the--- following property can be proved using refl:--unfoldInContext : Eq Stream [let xs : Stream = ticks in xs]- [let xs : Stream = [ticks] in xs];-unfoldInContext = cong ticks [ticks] unfold;-unfoldInContext = refl Stream [let xs : Stream = ticks in xs];---- Note also that unlimited unfolding is not possible (using refl):---- unfoldTwiceInContext : Eq Stream [let xs : Stream = ticks in xs]--- [let xs : Stream = [[ticks]] in xs];--- unfoldTwiceInContext = refl Stream [let xs : Stream = ticks in xs];---- However, we can move lets through boxes, so the idea from--- Thorsten's blog post needs to be qualified.--letThroughBox : (xs : Stream) →- Eq Stream [let ys : Stream = xs in ys]- (let ys : Stream = xs in [ys]);-letThroughBox = λ xs → refl Stream [let ys : Stream = xs in ys];--letThrough2Boxes : (xs : Stream) →- Eq Stream [[let ys : Stream = xs in ys]]- (let ys : Stream = xs in [[ys]]);-letThrough2Boxes = λ xs → refl Stream [[let ys : Stream = xs in ys]];--anotherExample : (A : Type) → (x : A) →- Eq (∞ (∞ A)) [let y : A = x in [y]]- (let y : A = x in [[let z : A = y in z]]);-anotherExample = λ A x → refl (∞ (∞ A)) (let y : A = x in [[y]]);
+ examples/Universe.pi view
@@ -0,0 +1,34 @@+:l Nat.pi+:l Fin.pi+:l Bool.pi++U : Type; +El : U -> Type;++U = (l : {enum sigma rec}) * + case l of { enum -> Nat+ | sigma -> Rec [(a : U) * (El a -> U)]+ | rec -> ^ (Rec [U]) };++El = \ a -> split a with (a_l,a_r) -> + ! case a_l of+ { enum -> [Fin a_r]+ | sigma -> [unfold a_r as a_r' -> + split a_r' with (b,c) -> + (x : El b) * (El (c x))]+ | rec -> [unfold (! a_r) as a_r' -> + Rec [El a_r']]};++nat : U = ('sigma, fold (('enum, succ (succ zero)),+ (\ i -> split i with (i_l,i_r) -> + ! case i_l of + { z -> [('enum, succ zero)]+ | s -> [('rec, [fold nat])]})));++eq : (a : U) -> El a -> El a -> Bool;++refl : (a : U) → (x : El a) → T (eq a x x);++subst : (a : U) → (x y : El a) → T (eq a x y) + → (P : El a → Type) → P x → P y;+
examples/Vec.pi view
@@ -4,7 +4,7 @@ Vec = \ m a -> split m with (lm , m') -> ! case lm of { z -> [Unit]- | s -> [a * Vec m' a] }; + | s -> [a * Vec (unfold m') a] }; vnil : (a : Type) -> Vec zero a; vnil = \ a -> 'unit;@@ -20,4 +20,4 @@ split i with (li , i') -> case li of { z -> [x]- | s -> [nth a n' xs' i']}}+ | s -> [nth a (unfold n') xs' i']}}
examples/stl.pi view
@@ -7,7 +7,7 @@ pair : (a:Bool) -> (b:Bool) -> ((T a) * (T b)) -> T (andb a b); pair = \ a b xy ->- split xy with (x,y) -> + split xy with (x,y) -> case a of { true -> y | false -> case x of {}};@@ -21,27 +21,29 @@ | false -> case x of {}}; Ty : Type;-Ty = (l : {base arr}) * +Ty = (l : {base arr}) * case l of { base -> Unit- | arr -> [Ty * Ty] };+ | arr -> Rec [Ty * Ty] }; base : Ty; base = ('base, 'unit); arr : Ty -> Ty -> Ty;-arr = \ a b -> ('arr,(a,b));+arr = \ a b -> ('arr,fold (a,b)); eqb : Ty -> Ty -> Bool; eqb = \ a b -> split a with (la, a') -> split b with (lb, b') -> ! case la of {- base -> case lb of { + base -> case lb of { base -> ['true] | arr -> ['false]} | arr -> case lb of { base -> ['false]- | arr -> split a' with (a0, a1) ->+ | arr -> unfold a' as a' ->+ unfold b' as b' ->+ split a' with (a0, a1) -> split b' with (b0, b1) -> [andb (eqb a0 b0) (eqb a1 b1)]}}; @@ -52,14 +54,15 @@ refl = \ a -> split a with (la, a') -> ! case la of { base -> ['unit]- | arr -> split a' with (b,c) ->+ | arr -> unfold a' as a' ->+ split a' with (b,c) -> [pair (eqb b b) (eqb c c) ((refl b) , (refl c))] }; -subst : (P : Ty -> Type) +subst : (P : Ty -> Type) -> (a : Ty) -> (b : Ty) -> (eq a b) -> P a -> P b;-subst = \ P a b p x -> +subst = \ P a b p x -> split a with (la, a') -> split b with (lb, b') -> ! case la of {@@ -70,32 +73,35 @@ | arr -> case p of {}} | arr -> case lb of { base -> case p of {}- | arr -> split a' with (a0 , a1) ->+ | arr -> unfold a' as a' ->+ unfold b' as b' ->+ split a' with (a0 , a1) -> split b' with (b0 , b1) -> split (unpair (eqb a0 b0) (eqb a1 b1) p) with (p0, p1) -> [subst (\ z -> P (arr b0 z)) a1 b1 p1 (subst (\ y -> P (arr y a1)) a0 b0 p0 x)]}};- -{- subst succesfully uses split on a non-variable! -} +{- subst successfully uses split on a non-variable! -}+ Con : Type;-Con = ( l : {empty ext} ) * +Con = ( l : {empty ext} ) * case l of { empty -> Unit- | ext -> [Con * Ty] };+ | ext -> Rec [Con * Ty] }; empty : Con; empty = ('empty,'unit); ext : Con -> Ty -> Con;-ext = \ g a -> ('ext,(g,a));+ext = \ g a -> ('ext, fold (g,a)); Var : Con -> Ty -> Type;-Var = \ g a -> - split g with (lg, g') -> +Var = \ g a ->+ split g with (lg, g') -> case lg of { empty -> Empty- | ext -> split g' with (d, a') ->+ | ext -> unfold g' as g' ->+ split g' with (d, a') -> (l : {vz vs}) * ! case l of { vz -> [eq a a']@@ -103,34 +109,35 @@ vz : (g:Con) -> (a:Ty) -> Var (ext g a) a; vz = \ g a -> ('vz, (refl a));- + vs : (g:Con) -> (a:Ty) -> (b:Ty) -> Var g a -> Var (ext g b) a; vs = \ g a b x -> ('vs,x); Lam : Con -> Ty -> Type;-Lam = \ g a -> +Lam = \ g a -> (l : {var app lam}) * case l of { var -> Var g a- | app -> [(b : Ty) * ((Lam g (arr b a)) * (Lam g b))]+ | app -> Rec [(b : Ty) * (Lam g (arr b a) * Lam g b)] | lam -> split a with (la, a') -> case la of { base -> Empty- | arr -> split a' with (b, c) ->- [Lam (ext g b) c] }};- + | arr -> unfold a' as a' ->+ split a' with (b, c) ->+ Rec [Lam (ext g b) c] }};+ var : (g:Con) -> (a:Ty) -> Var g a -> Lam g a; var = \ g a x -> ('var,x); app : (g:Con) -> (a:Ty) -> (b:Ty) -> Lam g (arr a b) -> Lam g a -> Lam g b;-app = \ g a b t u -> ('app,(a,(t,u)));+app = \ g a b t u -> ('app, fold (a,(t,u))); lam : (g:Con) -> (a:Ty) -> (b:Ty) -> Lam (ext g a) b -> Lam g (arr a b);-lam = \ g a b t -> ('lam,t);+lam = \ g a b t -> ('lam, fold t); -{- +{- Ren : Con -> Con -> Type Subst : Con -> Con -> Type
pisigma.cabal view
@@ -1,6 +1,6 @@ cabal-version: >= 1.6 name: pisigma-version: 0.1.0.3+version: 0.2 license: BSD3 license-file: LICENSE data-files: examples/*.pi@@ -12,13 +12,24 @@ Darin Morrison <dwm@cs.nott.ac.uk> maintainer: Thorsten Altenkirch <txa@cs.nott.ac.uk>, Andres Loeh <kspisigma@andres-loeh.de>-description: dependently typed core language-synopsis: dependently typed core language+synopsis: A dependently typed core language+description: + PiSigma is a small dependently typed language with only very few+ constructs: Type:Type, Pi-types, Sigma-types, enumerations and a+ general meachanism for mutual recursion for types and values+ controlled by lifted types. It is intended as a core language for+ dependently typed languages like Agda. It has been described in the+ paper <em>PiSigma: Dependent Types Without the Sugar</em> which has+ appeared in the proceedings of FLOPS 2010. category: Development, Language, Dependent Types build-type: Simple +flag debug+ description: Enable debug support+ default: False+ library- build-depends: array >= 0.2 && < 0.3,+ build-depends: array >= 0.2 && < 0.4, base >= 4.0 && < 5.0, bytestring >= 0.9 && < 1.0, haskeline >= 0.6 && < 0.7,@@ -27,7 +38,8 @@ mtl >= 1.1 && < 1.2, parsec >= 3.0 && < 4.0, text >= 0.5 && < 0.6,- utf8-string >= 0.3.5 && < 0.4+ utf8-string >= 0.3.5 && < 0.4,+ containers >= 0.2 && < 0.4 exposed-modules: Language.PiSigma.Check Language.PiSigma.Equality@@ -40,14 +52,21 @@ Language.PiSigma.Util.String.Internal Language.PiSigma.Util.String.Parser - ghc-options: -funbox-strict-fields+ if flag(debug)+ ghc-options: -Wall --enable-library-profiling -auto -funbox-strict-fields+ else+ ghc-options: -funbox-strict-fields hs-source-dirs: src executable pisigma- ghc-options: -funbox-strict-fields++ if flag(debug)+ ghc-options: -Wall --enable-library-profiling -auto -funbox-strict-fields+ else+ ghc-options: -funbox-strict-fields hs-source-dirs: src
src/Language/PiSigma/Check.hs view
@@ -8,26 +8,22 @@ import Control.Arrow ( first ) import Control.Monad.Error-import qualified Data.List- as List+import qualified Data.List as List import Language.PiSigma.Equality import Language.PiSigma.Evaluate import Language.PiSigma.Pretty import Language.PiSigma.Syntax-import qualified Language.PiSigma.Util.String.Internal- as Internal+import qualified Language.PiSigma.Util.String.Internal as Internal+import qualified Data.Set as Set ---import Debug.Trace---trace "check\n" $+-- import Debug.Trace+-- trace "check\n" $ -- closures are the other way around -- should be fixed by changing closures. -{--fog :: CTerm -> Closure-fog (g,t) = (con2scope g,t)--}+-- * Error handling throwErrorc :: (Print b, GetLoc b, Env e) => b -> Pretty -> Eval e a throwErrorc t m =@@ -60,12 +56,49 @@ duplicateLabels :: (GetLoc a, Print a, Env e) => a -> Eval e d duplicateLabels t =- throwErrorc t $ "Duplicate labels in enum type"+ throwErrorc t "Duplicate labels in enum type" nonLinearSplit :: (GetLoc a, Print a, Env e) => a -> Eval e d nonLinearSplit t =- throwErrorc t $ "Repeated variables in a split"+ throwErrorc t "Repeated variables in a split" +declaredButNotDefined :: Set.Set Name -> Eval e Scope+declaredButNotDefined xs = throwError "Variables declared but not defined"++declaredTwice :: Name -> Eval e Scope+declaredTwice x = throwError "Variable declared twice in the same block."++notDeclHere :: Name -> Eval e Scope+notDeclHere x = throwError "Name not declared in the same context"++-- * Checking++checkProg :: Env e => Clos Prog -> Eval e Scope+checkProg st = checkProg' Set.empty Set.empty st++-- to be finished+checkProg' :: Env e => Set.Set Name -> Set.Set Name -> Clos Prog -> Eval e Scope+checkProg' decls defns ([],g) = return g+-- do+-- let declndef = decls `Set.difference` defns+-- if not (Set.null declndef)+-- then declaredButNotDefined declndef+-- else return g+checkProg' decls defns ((Decl _ x a):tel,g) =+ do check (a,g) ty+ (_,g') <- decl x PrtInfo{ name = x, expand = False } g (Just (a,g))+ if x `Set.member` decls+ then declaredTwice x+ else checkProg' (Set.insert x decls) defns (tel,g')+checkProg' decls defns ((Defn l x t):tel,g) =+ do a <- inferVar l (x,g)+ check (t,g) a+ i <- getId l x g+ defn' i (t,g)+ if not (x `Set.member` decls) + then notDeclHere x+ else checkProg' decls (Set.insert x defns) (tel,g)+ -- | Takes a term and an (unevaluated) type. We first -- handle the cases that may potentially change the -- environment. If none of those cases match, we can@@ -73,7 +106,7 @@ check :: Env e => Clos Term -> Clos Type -> Eval e () --check (g,t) c | trace ("check\ng ="++(show g)++"\n t="++(show t)++"\nc="++(show c)++"\n") False = undefined -check (Let _ p t,g) c = +check (Let _ p t,g) c = do g' <- checkProg (p,g) check (t,g') c @@ -81,9 +114,9 @@ check (Split _ t (x,(y,u)),g) c | otherwise = do sigab <- infer' (t,g) case sigab of- (VQ Sigma ((a,(z,b)),s)) -> + (VQ Sigma ((a,(z,b)),s)) -> do t' <- eval (t,g)- (_,g') <- tdecl x g (a,s) + (_,g') <- tdecl x g (a,s) b' <- subst (z,(b,s)) (Var Unknown x, g') (_,g'') <- tdecl y g' b' case t' of@@ -98,10 +131,26 @@ msg1 = "sigma type" :: Internal.String msg2 = "split" :: Internal.String -check gt @ (Case _ t lus,g) c = +check (Unfold _ t (x,u),g) c =+ do rec <- infer' (t,g)+ case rec of+ VRec (a,s) ->+ do t' <- eval (t,g)+ (_,g') <- tdecl x g (Force Unknown a,s)+ case t' of+ (Ne (NVar i)) ->+ letn' i (Fold Unknown (Var Unknown x), g')+ (check (u,g') c)+ _ -> check (u,g') c+ _ -> expectedButFound (t,g) msg1 rec msg2+ where+ msg1 = "rec type" :: Internal.String+ msg2 = "unfold" :: Internal.String++check gt @ (Case _ t lus,g) c = do enum <- infer' (t,g) case enum of- VEnum ls -> + VEnum ls -> let ls' = map fst lus in if ls /= ls' then -- pt' <- evalPrint t'@@ -117,7 +166,7 @@ -- if the scrutinee is a variable, we add a constraint -- while checking each of the branches (Ne (NVar i)) ->- mapM_ (\ (l,u) -> + mapM_ (\ (l,u) -> letn' i (label l) (check (u,g) c)) lus -- if the scrutinee is not a variable, we do not add@@ -127,20 +176,17 @@ where msg1 = "enum type" :: Internal.String msg2 = "case" :: Internal.String- - {- Problem: here and other places: we try to print the term t which isn't yet ++ {- Problem: here and other places: we try to print the term t which isn't yet typechecked and may contain undefined variables which may crash the printer... see undef-bug.pi -}-check (Force _ t,g) (a , s) =- check (t,g) (Lift Unknown a , s)+check (Force _ t,g) c = check (t,g) (tlift c) -check t a = check' t =<< feval a+check t a = check' t =<< eval a check' :: Env e => Clos Term -> Val -> Eval e ()--- we ignore boxes in types, this is the other part of the lifting story.-check' gt (VBox (Boxed a)) = check gt a check' (Lam _ (x,t),g) (VQ Pi ((a,(y,b)),s)) = do (i,g') <- tdecl x g (a,s) let s' = extendScope s y (i,Nothing)@@ -158,51 +204,39 @@ check' (Label _ l,_) (VEnum ls) | l `elem` ls = return () check' gt @ (Label _ _,_) a = expected gt a "Label"--- To check that [sigma] is a type, it's sufficient to know--- that sigma is a type. The alternative would seem to be to--- assume that ^Type == Type, but that does not work.-check' (Box _ a,g) VType = - check (a,g) ty check' (Box _ t,g) (VLift a) = check (t,g) a-check' gt @ (Box _ _,_) a =- expected gt a "Box"+check' (Fold _ t,g) (VRec a) =+ check' (t,g) =<< eval (tforce a)+ check' t a = do b <- infer' t- catchE (eq a b) $ const $ expectedButFound t a b "check"+ catchE (eq a b) $ \ s -> expectedButFound t a b "Check"+-- line below leads to a runtime error +-- catchE (eq a b) $ \ s -> expectedButFound t a b (Internal.append "Check" s) -inferVar :: Env e => Loc -> Clos Name -> Eval e (Clos Type)-inferVar l (x,g) =- case lookupCon g x of- Just a -> return a- Nothing -> throwError msg- where- msg = Internal.concat [ Internal.fromString $ locMessage l- , "\nUndefined variable: "- , x- , "\n(inferVar)\n"- ]+-- * Inference infer :: Env e => Clos Term -> Eval e (Clos Type) --infer (g,t) | trace ("infer\ng ="++(show g)++"\n t="++(show t)++"\n") False = undefined infer (Var l x,g) = inferVar l (x,g) -infer (Let _ tel t,g) = +infer (Let _ tel t,g) = do g' <- checkProg (tel,g)- infer (t,g') + infer (t,g') infer (Type _,_) = return ty -infer (Q _ _ (a,(x,b)),g) = +infer (Q _ _ (a,(x,b)),g) = do check (a,g) ty (_,g') <- tdecl x g (a,g) check (b,g') ty return ty -infer (App t u,g) = +infer (App t u,g) = do piab <- infer' (t,g)- case piab of + case piab of (VQ Pi ((a,(x,b)),s)) -> do check (u,g) (a,s) subst (x,(b,s)) (u,g) _ -> expectedButFound (t,g) msg1 piab msg2@@ -217,14 +251,14 @@ infer (Box _ t,g) = liftM (first $ Lift Unknown) (infer (t,g)) --- TODO: either use infer', or explain why forced eval--- cannot be used here.+infer (Fold _ t,g) =+ liftM (first $ Rec Unknown . Box Unknown) (infer (t,g))+ infer (Force _ t,g) =- do a <- infer (t,g)- a' <- eval a- case a' of+ do a <- infer' (t,g)+ case a of VLift b -> return b- _ -> expectedButFound (t,g) msg1 a' msg2+ _ -> expectedButFound (t,g) msg1 a msg2 where msg1 = "lifted type" :: Internal.String msg2 = "Force" :: Internal.String@@ -233,29 +267,24 @@ do check (a,g) ty return ty --- infer (LType _ a,g) =--- do check (a,g) lty--- return ty-+infer (Rec _ a,g) =+ do check (a,g) lty+ return ty infer gt = throwErrorc gt $ "Not inferable" <$> "(infer)" - -- | Infers a type and evaluates it. infer' :: Env e => Clos Term -> Eval e Val-infer' gt = feval =<< infer gt+infer' gt = eval =<< infer gt -checkProg :: Env e => Clos Prog -> Eval e Scope-checkProg ([],g) = return g-checkProg ((Decl _ x a):tel,g) = - do check (a,g) ty - (_,g') <- decl x PrtInfo{ name = x, expand = False } g (Just (a,g))- checkProg (tel,g')-checkProg ((Defn l x t):tel,g) =- do a <- inferVar l (x,g)- check (t,g) a- i <- getId l x g- defn' i (t,g)- checkProg (tel,g)- - +inferVar :: Env e => Loc -> Clos Name -> Eval e (Clos Type)+inferVar l (x,g) =+ case lookupCon g x of+ Just a -> return a+ Nothing -> throwError msg+ where+ msg = Internal.concat [ Internal.fromString $ locMessage l+ , "\nUndefined variable: "+ , x+ , "\n(inferVar)\n"+ ]
src/Language/PiSigma/Equality.hs view
@@ -40,32 +40,33 @@ instance Equal Val where eq (Ne t0) (Ne t1) = eq t0 t1 eq (VQ ps0 ((a0,(x0,b0)),s0)) (VQ ps1 ((a1,(x1,b1)),s1))- | ps0 == ps1 = + | ps0 == ps1 = do eq (a0,s0) (a1,s1) eq (x0,(b0,s0)) (x1,(b1,s1)) eq (VLam xt0) (VLam xt1) = eq xt0 xt1- eq (VPair ((t0,u0),s0)) (VPair ((t1,u1),s1)) = + eq (VPair ((t0,u0),s0)) (VPair ((t1,u1),s1)) = do eq (t0,s0) (t1,s1) eq (u0,s0) (u1,s1)- eq (VBox b) (VBox b') = eq b b' + eq (VBox b) (VBox b') = eq b b' eq (VLift a) (VLift a') = eq a a'--- eq (VLType a) (VLType a') = eq a a'+ eq (VRec a) (VRec a') = eq a a'+ eq (VFold a) (VFold a') = eq a a' eq v0 v1 | v0 == v1 = return () -- Type, Label, Enum | otherwise = fail "Different values" {- eqBox implements alpha equality -} eqBox :: Env e => Clos Term -> Clos Term -> Eval e () --eqBox c c' | c == c' = return ()-eqBox (Var l x,s) (Var l' y,s') = +eqBox (Var l x,s) (Var l' y,s') = do x' <- getId l x s y' <- getId l' y s' eq x' y'-eqBox (Let _ p t,s) c = +eqBox (Let _ p t,s) c = do s' <- evalProg (p,s) eqBox (t,s') c-eqBox c c'@(Let _ _ _,_) = eqBox c' c +eqBox c c'@(Let _ _ _,_) = eqBox c' c eqBox (Q _ ps (a,(x,b)),s) (Q _ ps' (a',(x',b')),s')- | ps == ps' = + | ps == ps' = do eqBox (a,s) (a',s') eq (x,Boxed (b,s)) (x',Boxed (b',s')) eqBox (Lam _ (x,t),s) (Lam _ (x',t'),s') =@@ -81,21 +82,25 @@ eq (x,(y,Boxed (u,s))) (x',(y',Boxed (u',s'))) eqBox (Case _ t bs,s) (Case _ t' bs',s') = do eqBox (t,s) (t',s')- zipWithM_ (\ (l,t'') (l',t''') -> + zipWithM_ (\ (l,t'') (l',t''') -> if l==l' then eqBox (t'',s) (t''',s') else fail "eqBox case") bs bs' eqBox (Lift _ t,s) (Lift _ t',s') = eqBox (t,s) (t',s')--- eqBox (LType _ t,s) (LType _ t',s') = eqBox (t,s) (t',s') eqBox (Box _ t,s) (Box _ t',s') = eqBox (t,s) (t',s')-eqBox (Force _ t,s) (Force _ t',s') = eqBox (t,s) (t',s') +eqBox (Force _ t,s) (Force _ t',s') = eqBox (t,s) (t',s')+eqBox (Rec _ t,s) (Rec _ t',s') = eqBox (t,s) (t',s')+eqBox (Fold _ t,s) (Fold _ t',s') = eqBox (t,s) (t',s')+eqBox (Unfold _ t (x, u), s) (Unfold _ t' (x', u'), s') =+ do eqBox (t,s) (t',s')+ eq (x,Boxed (u,s)) (x',Boxed (u',s')) eqBox (t,_) (t',_) | t == t' = return () -- Type, Label, Enum | otherwise = fail "Different terms"- + instance Equal Boxed where eq (Boxed c) (Boxed c') = eqBox c c' instance Equal Id where- eq i0 i1 + eq i0 i1 | i0 == i1 = return () | otherwise = do ei0 <- lookupId i0 ei1 <- lookupId i1@@ -110,7 +115,7 @@ instance Equal Ne where eq (NVar i0) (NVar i1) = eq i0 i1- eq (t0 :.. u0) (t1 :.. u1) = + eq (t0 :.. u0) (t1 :.. u1) = do eq t0 t1 eq u0 u1 eq (NSplit t0 xyu0) (NSplit t1 xyu1) =@@ -126,4 +131,7 @@ eqBranches _ _ = fail "Case: branches differ" eqBranches lus0 lus1 eq (NForce t) (NForce t') = eq t t'+ eq (NUnfold t xu) (NUnfold t' xu') = do+ eq t t'+ eq xu xu' eq t u = fail ("Different neutrals:\n"++ show t ++"\n/=\n"++ show u ++"\n")
src/Language/PiSigma/Evaluate.hs view
@@ -8,9 +8,9 @@ , decl , decl' , defn'+ , force , eval , evalProg- , feval , getEnv , getId , letn@@ -42,7 +42,7 @@ , MonadState e ) run :: e -> Eval e a -> Either EvalErr (a, e)-run e (Eval p) = runIdentity $ runErrorT $ runStateT p e +run e (Eval p) = runIdentity $ runErrorT $ runStateT p e catchE :: Eval e a -> (EvalErr -> Eval e a) -> Eval e a catchE = catchError@@ -54,7 +54,7 @@ setEnv = put getId :: Loc -> Name -> Scope -> Eval e Id-getId l x s = case lookupScope s x of +getId l x s = case lookupScope s x of Just i -> return i Nothing -> throwError msg where@@ -108,7 +108,7 @@ subst :: Env e => Bind (Clos Term) -> (Clos Term) -> Eval e (Clos Term) subst (x,(t,s)) u = do (i,s') <- decl' x s- defn' i u + defn' i u return (t,s') evalApp :: Env e => Val -> (Clos Term) -> Eval e Val@@ -126,23 +126,18 @@ Closure t -> eval t Id j -> return (Ne (NVar j)) --- use subst! evalSplit :: Env e => Val -> Bind (Bind (Clos Term)) -> Eval e Val-evalSplit (VPair ((l,r),s)) (x,(y,(t,s'))) = - do (x',s2) <- decl' x s'- (y',s3) <- decl' y s2- defn' x' (l,s)- defn' y' (r,s)- eval (t,s3)--evalSplit (Ne n) (xy,t) = return (Ne (NSplit n (xy,t)))+evalSplit (VPair ((l,r),s)) (x,(y,(t,s'))) =+ do ts2 <- subst (x, (t, s')) (l, s)+ eval =<< subst (y, ts2) (r, s)+evalSplit (Ne n) b = return (Ne (NSplit n b)) evalSplit _ _ = throwError "Pair expected" evalCase :: Env e => Val -> Clos [(Label,Term)] -> Eval e Val-evalCase (VLabel l) (lts,s) = +evalCase (VLabel l) (lts,s) = case lookup l lts of Nothing -> throwError "case not matched" Just t -> eval (t,s)@@ -154,13 +149,17 @@ force (Ne n) = return (Ne (NForce n)) force _ = throwError "Box expected" +unfold :: Env e => Val -> Bind (Clos Term) -> Eval e Val+unfold (VFold c) b = eval =<< subst b c+unfold (Ne n) b = return (Ne (NUnfold n b))+unfold _ _ = throwError "Fold expected"+ eval :: Env e => (Clos Term) -> Eval e Val eval (Var l x, s) = evalId =<< getId l x s eval (Let _ g t, s) = curry eval t =<< evalProg (g,s) eval (Type _, _) = return VType eval (Q _ ps axb, s) = return (VQ ps (axb,s)) eval (Lift _ t, s) = return (VLift (t,s))---eval (LType _ t, s) = return (VLType (t,s)) eval (Lam _ (x,t), s) = return (VLam (x,(t,s))) eval (App t u, s) = flip evalApp (u,s) =<< eval (t,s) eval (Pair _ t u, s) = return (VPair ((t,u),s))@@ -170,16 +169,9 @@ eval (Case _ t lts, s) = flip evalCase (lts,s) =<< eval (t,s) eval (Box _ t, s) = return (VBox (Boxed (t,s))) eval (Force _ t, s) = force =<< eval (t,s)----- forced eval (should be integrated into eval?)-feval :: Env e => (Clos Term) -> Eval e Val-feval t = do t' <- eval t- case t' of - VBox (Boxed u) -> feval u- v -> return v-- +eval (Rec _ t, s) = return (VRec (t,s))+eval (Fold _ t, s) = return (VFold (t,s))+eval (Unfold _ t (x, u), s) = flip unfold (x, (u, s)) =<< eval (t,s) evalProg :: Env e => Clos Prog -> Eval e Scope evalProg ([],s) = return s
src/Language/PiSigma/Lexer.hs view
@@ -124,14 +124,18 @@ , "let" , "of" , "split"- , "with" ]+ , "with"+ , "Rec"+ , "fold"+ , "unfold"+ , "as"] , Token.reservedOpNames = [ "!" , "*" , "," , "->" , ":" , ";"- , "=" + , "=" , "\\" , "^" , "|"
src/Language/PiSigma/Normalise.hs view
@@ -44,27 +44,31 @@ nf' b xs i = do e <- getEnv let (PrtInfo x shouldExpand) = prtE e i case getE e i of- (Id _) -> return (Var Unknown x) - (Closure t) -> if shouldExpand then nf' b xs t- -- this is bad, we should not- -- expand inside a box!- else return (Var Unknown x) + (Id _) -> return (Var Unknown x)+ (Closure t) -> if shouldExpand then + do t' <- nf' b xs t+ return (Let Unknown + [Defn Unknown x t'] (Var Unknown x))+ -- we should also declare x, but we don't know its type!+ -- the let cannot be expanded if inside a box!+ else return (Var Unknown x) qq :: Env e => Vars -> Clos Term -> Eval e Term qq xs (Var l x , s) = quote xs =<< getId l x s-qq _ (Let _ _ _, _) = return (Label Unknown "*quote-let-not-implemented*")---qq xs (Let l g t, s) = fail "quote let: not implemented!"-{-do s' <- evalProg (g,s)- qq xs (t,s') - -- this seems wrong! we should return a Let- -- and we should extend xs!--}-qq xs (Q l ps (a,(x,b)),s) = +--qq _ (Let _ _ _, _) = return (Label Unknown "*quote-let-not-implemented*")+qq xs (Let l g t, s) = + do s' <- evalProg (g,s)+ qq (xs ++ decls g) (t,s')+qq xs (Q l ps (a,(x,b)),s) = do a' <- qq xs (a,s) xb' <- quote xs (x,(b,s)) return (Q l ps (a',xb')) qq xs (Lift l t,s) = liftM (Lift l) (qq xs (t,s))--- qq xs (LType l t,s) = liftM (LType l) (qq xs (t,s))+qq xs (Rec l t,s) = liftM (Rec l) (qq xs (t,s))+qq xs (Fold l t,s) = liftM (Fold l) (qq xs (t,s))+qq xs (Unfold l t (x, u), s) = do t' <- qq xs (t, s)+ xu' <- quote xs (x, (u, s))+ return (Unfold l t' xu') qq xs (Lam l (x,t), s) = liftM (Lam l) (quote xs (x,(t,s))) qq xs (App t u ,s) = do t' <- qq xs (t,s) u' <- qq xs (u,s)@@ -76,10 +80,10 @@ xyu' <- quote xs (x,(y,(u,s))) return (Split l t' xyu') qq xs (Case l t lts,s) = do t' <- qq xs (t,s)- lts' <- mapM (\ (l',t'') -> + lts' <- mapM (\ (l',t'') -> do t''' <- qq xs (t'',s) return (l',t''')) lts- return (Case l t' lts') + return (Case l t' lts') qq xs (Box l t,s) = liftM (Box l) (qq xs (t,s)) qq xs (Force l t,s) = liftM (Force l) (qq xs (t,s)) qq _ (t,_) = return t -- Type, Enum, Label@@ -93,11 +97,12 @@ instance Nf Val Term where nf' b xs (Ne n) = nf' b xs n nf' _ _ VType = return (Type Unknown)- nf' b xs (VQ ps ((a,(x,c)),s)) = do a' <- nf' b xs (a,s) + nf' b xs (VQ ps ((a,(x,c)),s)) = do a' <- nf' b xs (a,s) xc' <- nf' b xs (x,(c,s)) return (Q Unknown ps (a',xc')) nf' b xs (VLift c) = liftM (Lift Unknown) (nf' b xs c)--- nf' b xs (VLType c) = liftM (LType Unknown) (nf' b xs c)+ nf' b xs (VRec c) = liftM (Rec Unknown) (nf' b xs c)+ nf' b xs (VFold c) = liftM (Fold Unknown) (nf' b xs c) nf' b xs (VLam xt) = liftM (Lam Unknown) (nf' b xs xt) nf' b xs (VPair ((t,u),s)) = do t' <- nf' b xs (t,s) u' <- nf' b xs (u,s)@@ -116,8 +121,11 @@ xyu' <- nf' b xs xyu return (Split Unknown t' xyu') nf' b xs (NCase t (lus,s)) = do t' <- nf xs t- lus' <- mapM (\ (l,u) -> + lus' <- mapM (\ (l,u) -> do u' <- nf' b xs (u,s) return (l,u')) lus return (Case Unknown t' lus') nf' _ xs (NForce t) = liftM (Force Unknown) (nf xs t)+ nf' b xs (NUnfold t xu) = do t' <- nf' b xs t+ xu' <- nf' b xs xu+ return (Unfold Unknown t' xu')
src/Language/PiSigma/Parser.hs view
@@ -1,3 +1,72 @@+{-++The following grammar is (supposed to be) implemented below:++variable ∷= …++label ∷= …++arrow ∷= "→" | "->"++lambda ∷= "λ" | "\\"++branch ∷= label arrow term++branch⋆+ ∷= branch "|" branch⋆+ |++label⋆+ ∷= label label⋆+ |++variable⁺+ ∷= variable variable⁺+ | variable++prefix-operator+ ∷= "Rec" | "fold" | "unfold" | "^" | "∞" | "!" | "♭" | "♯"++infix-operator ∷= arrow | "*"++entry+ ∷= variable ":" term ( | "=" term)+ | variable "=" term++entry⁺+ ∷= entry ";" entry⁺+ | entry++program+ ∷= entry⁺ ";"+ | entry⁺+ |++atom+ ∷= "(" term ")"+ | variable+ | "Type"+ | "(" term "," term ")"+ | "{" label⋆ "}"+ | "′" label+ | "case" term "of" "{" branch⋆ "}"+ | "[" term "]"++atom-or-application+ ∷= atom+ | prefix-operator atom+ | atom-or-application atom++term+ ∷= atom-or-application ( | infix-operator term)+ | "let" program "in" term+ | "(" variable⁺ ":" term ")" infix-operator term+ | lambda variable⁺ arrow term+ | "split" term "with" "(" variable "," variable ")" arrow term+ | "unfold" term "as" variable arrow term++-}+ module Language.PiSigma.Parser ( parse , sPhrase@@ -41,70 +110,71 @@ -- * Terms -sTerm5 :: Parser Term-sTerm5 = choice- [ Type <$> locReserved "Type"+prefixOperator :: Parser (Term -> Term)+prefixOperator = choice+ [ Rec <$> locReserved "Rec"+ , Fold <$> locReserved "fold"+ , Lift <$> tokLift+ , Force <$> tokForce+ , Box <$> locReservedOp "♯"+ , unfold <$> locReserved "unfold"+ ]+ where+ unfold l t = Unfold l t id+ id = ( Internal.fromString " x"+ , Var Unknown (Internal.fromString " x")+ ) +infixOperator :: Parser (Term -> Term -> Term)+infixOperator = choice+ [ (->-) <$ tokArr+ , (-*-) <$ locReservedOp "*"+ ]++atom :: Parser Term+atom = choice+ [ try $ parens sTerm++ , Type <$> locReserved "Type"++ , pair <$> location+ <*> parens ((,) <$> sTerm <* comma <*> sTerm)+ <?> "pair"+ , Enum <$> location <*> braces (many sName) <?> "enumeration" + , Label <$> location+ <*> sLabel+ <?> "label"+ , Case <$> locReserved "case" <*> sTerm <* reserved "of" <*> braces (sBranch `sepBy` locReservedOp "|") - , Label <$> location- <*> sLabel- <?> "label"- , Box <$> location- <*> boxed sTerm+ <*> brackets sTerm <?> "box" - , Lift <$> tokLift- <*> sTerm5- <?> "'^'"- , Var <$> location <*> sName- , parens sTerm ]- where- boxed p = choice [ brackets p- , reservedOp "♯" *> p- ]--sTerm4 :: Parser Term-sTerm4 = choice- [ try $ (uncurry . Pair) <$> location- <*> parens ((,) <$> sTerm <* comma <*> sTerm)- , sTerm5- ]--sTerm3 :: Parser Term-sTerm3 = choice- [ try (parens (sigmas <$> many1 ((,) <$> location <*> sName) <* reservedOp ":" <*> sTerm) <* reservedOp "*") <*> sTerm2- , Force <$> tokForce <*> sTerm4- , foldl1 App <$> many1 sTerm4- ]--sTerm2 :: Parser Term-sTerm2 = foldr1 (-*-) <$> sTerm3 `sepBy1` reservedOp "*"+ where pair = uncurry . Pair --- TODO: make more beautiful or renumber-sTerm1b :: Parser Term-sTerm1b = choice- [ try (parens (pis <$> many1 ((,) <$> location <*> sName) <* reservedOp ":" <*> sTerm) <* tokArr) <*> sTerm- , sTerm2- ]- -sTerm1 :: Parser Term-sTerm1 = foldr1 (->-) <$> sTerm1b `sepBy1` tokArr+atomOrApplication :: Parser Term+atomOrApplication =+ foldl App <$> (atom <|> prefixOperator <*> atom) <*> many atom sTerm :: Parser Term sTerm = choice- [ lam <$ tokLam- <*> many ((,) <$> location <*> sName)+ [ Let <$> locReserved "let"+ <*> sProg+ <* reserved "in"+ <*> sTerm++ , lam <$ tokLam+ <*> many1 ((,) <$> location <*> sName) <* tokArr <*> sTerm @@ -117,11 +187,25 @@ <* tokArr <*> sTerm - , Let <$> locReserved "let"- <*> sProg- <* reserved "in"- <*> sTerm- , sTerm1+ , try (Unfold <$> locReserved "unfold"+ <*> sTerm+ <* reserved "as")+ <*> ((,) <$> sName+ <* tokArr+ <*> sTerm)++ , try (do (ns, t) <- parens $+ (,) <$> many1 ((,) <$> location <*> sName)+ <* reservedOp ":"+ <*> sTerm+ op <- choice [ pis <$ tokArr+ , sigmas <$ reservedOp "*"+ ]+ return $ op ns t) <*> sTerm++ , (\a -> maybe a ($ a)) <$>+ atomOrApplication <*>+ optionMaybe (flip <$> infixOperator <*> sTerm) ] sProg :: Parser Prog@@ -154,7 +238,7 @@ ] s2Terms :: Parser (Term, Term)-s2Terms = (,) <$> sTerm5 <*> sTerm5+s2Terms = (,) <$> atom <*> atom parse :: Parser a -> SourceName -> Parser.String -> Either ParseError a parse p = Parsec.parse (whiteSpace *> p <* eof)
src/Language/PiSigma/Pretty.hs view
@@ -77,25 +77,28 @@ prettyTerm _ (Var _ x) = text $ Seq x -prettyTerm _ (Let _ p t) =- list (map prettyEntry p)- <> prettyTerm 0 t+prettyTerm c (Let _ p t) =+ contextParens c 0+ $ text "let"+ <+> sep (map prettyEntry p)+ <+> text "in"+ <+> prettyTerm 0 t prettyTerm _ (Type _) = text "Type" prettyTerm c (Q _ Pi (t1, (n, t2))) =- contextParens c 1+ contextParens c 0 $ group- $ binding 2 n t1+ $ binding 1 n t1 <$> text "->"- <+> prettyTerm 1 t2+ <+> prettyTerm 0 t2 prettyTerm c (Q _ Sigma (t1, (n, t2))) =- contextParens c 2- $ binding 3 n t1+ contextParens c 0+ $ binding 1 n t1 <+> text "*"- <+> prettyTerm 2 t2+ <+> prettyTerm 0 t2 prettyTerm c (Lam _ (n, t)) = contextParens c 0@@ -107,9 +110,9 @@ prettyTerm c (App t1 t2) = group $ hang 2- $ contextParens c 3- $ prettyTerm 3 t1- <$> prettyTerm 4 t2+ $ contextParens c 1+ $ prettyTerm 1 t1+ <$> prettyTerm 2 t2 prettyTerm _ (Pair _ t1 t2) = tupled $ map (prettyTerm 0) [t1, t2]@@ -142,33 +145,53 @@ <$> branches bs prettyTerm c (Lift _ t) =- contextParens c 5- $ text "^"- <> prettyTerm 5 t+ contextParens c 1+ $ text "^"+ <+> prettyTerm 2 t prettyTerm _ (Box _ t) = brackets $ prettyTerm 0 t prettyTerm c (Force _ t) =- contextParens c 3- $ text "!"- <> prettyTerm 4 t+ contextParens c 1+ $ text "!"+ <+> prettyTerm 2 t +prettyTerm c (Rec _ t) =+ contextParens c 1+ $ text "Rec"+ <+> prettyTerm 2 t +prettyTerm c (Fold _ t) =+ contextParens c 1+ $ text "fold"+ <+> prettyTerm 2 t++prettyTerm c (Unfold _ t1 (n, t2)) =+ contextParens c 0+ $ hang 2+ $ text "unfold"+ <+> prettyTerm 0 t1+ <+> text "as"+ <+> text (Seq n)+ <+> text "->"+ <$> prettyTerm 0 t2++ prettyEntry :: Entry -> Pretty prettyEntry (Defn _ n t) = hang 2 $ text (Seq n) <+> text "="- <$> prettyTerm 0 t+ <+> prettyTerm 0 t <> text ";" prettyEntry (Decl _ n t) = hang 2 $ text (Seq n) <+> text ":"- <$> prettyTerm 0 t+ <> prettyTerm 0 t <> text ";"
src/Language/PiSigma/Syntax.hs view
@@ -35,6 +35,7 @@ , label , lam , locMessage+ , decls , lookupCon , lookupScope , pis@@ -42,7 +43,10 @@ , setE , sigmas , split- , ty )+ , ty+ , lty+ , tforce+ , tlift ) where import Prelude@@ -105,6 +109,12 @@ type Prog = [Entry] +decls :: Prog -> [Name]+decls [] = []+decls (Decl _ x _ : p) = x:decls p+decls (Defn _ _ _ : p) = decls p++ {- Maybe better data Prog = Decl Type (Bind Prog) | Defn Name Term Prog@@ -137,7 +147,9 @@ | Lift Loc Term | Box Loc Term | Force Loc Term--- | LType Loc Term -- lazy type ($ sigma)+ | Rec Loc Term+ | Fold Loc Term+ | Unfold Loc Term (Bind Term) -- unfold t as x -> u deriving (Show,Eq) instance GetLoc Term where@@ -155,7 +167,9 @@ getLoc (Lift l _ ) = l getLoc (Box l _ ) = l getLoc (Force l _ ) = l--- getLoc (LType l _) = l+ getLoc (Rec l _ ) = l+ getLoc (Fold l _ ) = l+ getLoc (Unfold l _ _) = l -- * Smart constructors @@ -230,7 +244,7 @@ We then need a forgetful mapping: fog :: Ctx -> Scope-fog c = map (\ (x,(i,a)) -> (x,(i,()))) c +fog c = map (\ (x,(i,a)) -> (x,(i,()))) c Alternatively, we can try to make Scopes existential, essentially:@@ -267,7 +281,7 @@ -- fix order, name of C... -class Closure a where +class Closure a where getScope :: a -> Scope putScope :: a -> Scope -> a @@ -288,9 +302,15 @@ ty :: Clos Type ty = (Type Unknown, emptyScope) ---lty :: Clos Type---lty = (Lift Unknown (Type Unknown), emptyScope)+lty :: Clos Type+lty = (Lift Unknown (Type Unknown), emptyScope) +tforce :: Clos Type -> Clos Type+tforce (a,s) = (Force Unknown a, s)++tlift :: Clos Type -> Clos Type+tlift (a,s) = (Lift Unknown a, s)+ label :: Label -> Clos Term label s = (Label Unknown s, emptyScope) @@ -303,15 +323,16 @@ data Val = Ne Ne- | VType + | VType | VQ PiSigma (Clos (Type, Bind Type)) | VLift (Clos Type) | VLam (Bind (Clos Term)) | VPair (Clos (Term, Term)) | VEnum [Label]- | VLabel Label + | VLabel Label | VBox Boxed--- | VLType (Clos Type)+ | VRec (Clos Type)+ | VFold (Clos Term) deriving (Show, Eq) -- | Neutral terms.@@ -321,6 +342,7 @@ | NSplit Ne (Bind (Bind (Clos Term))) | NCase Ne (Clos [(Label, Term)]) | NForce Ne+ | NUnfold Ne (Bind (Clos Term)) deriving (Show, Eq) -- ** Environments@@ -334,7 +356,7 @@ = PrtInfo { name :: Name , expand :: Bool } -class Env e where +class Env e where emptyE :: e extE :: e -> PrtInfo -> (Id,e) setE :: e -> Id -> EnvEntry -> e
src/Tools/Interpreter/Main.hs view
@@ -5,7 +5,7 @@ import Tools.Interpreter.REPL main :: IO ()-main = +main = do args <- getArgs let ini = mapM_ (handleCommand . Load) args
src/Tools/Interpreter/REPL.hs view
@@ -105,7 +105,7 @@ -- * REPL monad initialREPLState :: REPLState-initialREPLState = +initialREPLState = REPLState (emptyScope, emptyE) [] runREPL :: REPL () -> IO ()@@ -334,7 +334,7 @@ Left e -> do liftIO $ Internal.putStrLn e throwError Error- + inferTerm :: Term -> REPL () inferTerm t =