pisigma (empty) → 0.1.0.1
raw patch · 18 files changed
+1057/−0 lines, 18 filesdep +ansi-wl-pprintdep +arraydep +basesetup-changed
Dependencies added: ansi-wl-pprint, array, base, haskeline, mtl, parsec
Files
- LICENSE +27/−0
- Setup.hs +3/−0
- examples/Bool.pi +15/−0
- examples/Conat.pi +83/−0
- examples/Data.pi +107/−0
- examples/Empty.pi +2/−0
- examples/EqProb.pi +39/−0
- examples/Equal.pi +54/−0
- examples/Fin.pi +40/−0
- examples/Maybe.pi +10/−0
- examples/Nat.pi +94/−0
- examples/Streams.pi +91/−0
- examples/Unit.pi +2/−0
- examples/Universe.pi +47/−0
- examples/Vec.pi +23/−0
- examples/stl.pi +131/−0
- pisigma.cabal +24/−0
- src/PiSigma.hs +265/−0
+ LICENSE view
@@ -0,0 +1,27 @@+Copyright (c) 2008--2009 Thorsten Altenkirch, Andres Loeh++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions+are met:+1. Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.+2. Redistributions in binary form must reproduce the above copyright+ notice, this list of conditions and the following disclaimer in the+ documentation and/or other materials provided with the distribution.+3. Neither the name of the author nor the names of his contributors+ may be used to endorse or promote products derived from this software+ without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE+ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS+OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)+HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT+LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY+OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF+SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,3 @@+import Distribution.Simple++main = defaultMain
+ examples/Bool.pi view
@@ -0,0 +1,15 @@+:l Empty.pi+:l Unit.pi++Bool : Type;+Bool = { true false };++T : Bool -> Type;+T = \ b -> case b of {+ true -> Unit+ | false -> Empty };++andb : Bool -> Bool -> Bool;+andb = \ b c -> case b of {+ true -> c+ | false -> 'false };
+ examples/Conat.pi view
@@ -0,0 +1,83 @@+:l Empty.pi+:l Unit.pi++Nat' : Type;+Nat' = (l : { z s }) * case l of {+ z -> Unit+ | s -> [^ Nat'] };+++zero : Nat';+zero = ('z,'unit);++succ : ^Nat' -> Nat';+succ = \ n -> ('s,n);++one : Nat';+one = succ [zero];++two : Nat';+two = succ [one];++omega : Nat';+omega = succ [omega];+++add : Nat' -> Nat' -> Nat';+add = \ m n -> split m with (lm , m') ->+ case lm of {+ z -> n+ | s -> succ [add (!m') n] };++eq : Nat' -> Nat' -> Type;+eq = \ m n -> split m with (lm , m') ->+ split n with (ln , n') ->+ case lm of {+ z -> case ln of { + z -> Unit+ | s -> Empty }+ | s -> case ln of { + z -> Empty+ | s -> [^ (eq (! m') (! n'))]}};+++refl : (n:Nat') -> eq n n;+refl = \ n -> split n with (ln , n') ->+ case ln of {+ z -> 'unit+ | s -> [refl (!n')] };++sym : (m:Nat') -> (n:Nat') -> eq m n -> eq n m;+sym = \ 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 { + z -> case p of {}+ | s -> [sym (! m') (! n') (! p)] }};++{-+subst : (P : Nat' -> Type) + -> (m : Nat') -> (n : Nat')+ -> (eq m n)+ -> P m -> ^ (P n);+subst = \ P m n q x -> + split m with (lm , m') ->+ split n with (ln , n') ->+ case lm of {+ z -> case ln of {+ z -> case m' of {+ unit -> case n' of {+ unit -> [x] }}+ | s -> case q of {}}+ | s -> case ln of { + z -> case q of {}+ | s -> [subst (\ i -> P (succ i)) (! m') (! n') (! q) x]}};+-}++{- seems we need an eliminator for boxes, e.g. unbox+-}+
+ examples/Data.pi view
@@ -0,0 +1,107 @@+:l Maybe.pi+:l Bool.pi++data : Type;+El : data -> Type;++data = ( l : {empty maybe sigma box} ) * + case l of {+ empty -> Unit+ | maybe -> [data]+ | sigma -> [(a : data) * (El a -> data)]+ | box -> [^ data] }; ++El = \ a -> split a with (la,a') ->+ case la of {+ empty -> {}+ | maybe -> [Maybe (El a')]+ | sigma -> split a' with (b,c) ->+ [(x:El b)*(El (c x))]+ | box -> [El (! a')] };++unit : data;+unit = ('maybe,('empty,'unit));++un : El unit;+un = ('nothing,'unit);++bool : data;+bool = ('maybe, unit);++tt : El bool;+tt = ('nothing,'unit);++ff : El bool;+ff = ('just,('nothing,'unit));++nat : data;+nat = ('sigma,(bool,\ b -> split b with (lb,b') ->+ case lb of {+ nothing -> unit+ | just -> ('box, [nat]) }));+ +zero : El nat;+zero = (tt,un);++succ : El nat -> El nat;+succ = \ n -> (ff,n);++Eq : Type -> Type;+Eq = \ A -> A -> A -> Bool;++eqMaybe : (A:Type) -> Eq A -> Eq (Maybe A);+eqMaybe = \ A eqA a b ->+ split a with (la,a') ->+ split b with (lb,b') ->+ case la of {+ nothing -> case lb of {+ nothing -> 'true + | just -> 'false }+ | just -> case lb of {+ nothing -> 'false+ | just -> eqA a' b'}};+++eq : (a : data) -> Eq (El a);++subst : (a : data) + -> (x:El a) -> (y : El a) -> T (eq a x y)+ -> (P : El a -> Type) -> P x -> P y;++sigmab : (b : Bool) -> (T b -> Bool) -> Bool;+sigmab = \ b c -> case b of {+ true -> c 'unit+ | false -> 'false };++eq = \ a x y -> split a with (la,a') ->+ ! case la of {+ empty -> case x of {} + | maybe -> [eqMaybe (El a') (eq a') x y]+ | sigma -> split a' with (b,c) ->+ split x with (x0,x1) ->+ split y with (y0,y1) ->+ [sigmab (eq b x0 y0)+ (\ p -> eq (c y0) + (subst b x0 y0 p (\ x -> El (c x))+ x1) y1)]+ | box -> [eq (! a') x y]}; ++{-+subst = \ a x y p P px ->+ split a with (la,a') ->+ ! case la of {+ empty -> case x of {} + | maybe -> split x with (lx,x') ->+ split y with (ly,y') -> + case lx of {+ nothing -> (case ly of {+ nothing -> (case x' of {+ unit -> case y' of {+ unit -> [px] } })+ | just -> case p of {}})+ | just -> case ly of {+ nothing -> (case p of {})+ | just -> [subst a' x' y' p (\ z -> P ('just,z)) px]}}+ | sigma -> [subst a x y p P px]+ | box -> [subst (! a') x y p P px]}; +-}
+ examples/Empty.pi view
@@ -0,0 +1,2 @@+Empty : Type;+Empty = { };
+ examples/EqProb.pi view
@@ -0,0 +1,39 @@+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;++Stream : Type;+Stream = (tag : {Cons}) * case tag of {Cons -> [^Stream] };++ticks : Stream;+ticks = ('Cons, [ticks]);++l1 : Eq Stream ticks ('Cons, [ticks]);+l1 = refl Stream ticks;++l2 : (s : Stream) -> (t : Stream) -> (Eq Stream s t)+ -> Eq Stream ('Cons, [s]) ('Cons, [t]);+l2 = \ s t q P p -> q (\ x -> P ('Cons,[x])) p;++{- bad error message! -}++{- unbox x with [y] -> t ++ |- C : Type+ |- x : ^A+ y:A, x==[y] |- t : C+ -----------------------------+ |- unbox x with [y] -> t : C++ unbox [a] with [y] -> t ==> let y=a in t+++ ![a] = a++-}++{-+l3 : (A:Type) -> (a:A) -> (b:A) -> Eq A a b -> Eq (^A) [a] [b];+-}
+ examples/Equal.pi view
@@ -0,0 +1,54 @@+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;++A : Type;+a : A;++b : A;+b = a;++t0 : Eq A a b;+t0 = refl A a;++{-+c : A;+t1 : Eq A a c;+t1 = refl A a;+-}++d : ^A;+d = [a];++t2 : Eq (^A) d [a];+t2 = refl (^A) [a];++{-+t3 : Eq (^A) [a] [b];+t3 = refl (^A) [a];+-}++e : A;+e = a;++t4 : Eq (^A) [e] [b];+t4 = refl (^A) [e];++id : A -> A;+id = \ x -> x;++f : A;+f = id a;++t5 : Eq (^A) [f] [b];+t5 = refl (^A) [f];+{-+? f = b+? id a = a [f=b=b]+-}++t6 : Eq A (id a) a;+t6 = refl A a;+
+ examples/Fin.pi view
@@ -0,0 +1,40 @@+:l Nat.pi++Fin : Nat -> Type;+Fin = \ n -> split n with (ln , n') ->+ ! case ln of {+ z -> [Empty]+ | s -> [(l : { z s }) * case l of {+ z -> Unit+ | s -> Fin n'}]};++fz : (n:Nat) -> Fin (succ n);+fz = \ n -> ('z , 'unit );++fs : (n:Nat) -> Fin n -> Fin (succ n);+fs = \ n i -> ('s, i);++fmax : (n:Nat) -> Fin (succ n);+fmax = \ n -> split n with (ln , n') ->+ ! case ln of {+ z -> [fz zero]+ | s -> [fs n (fmax n')] };++femb : (n:Nat) -> Fin n -> Fin (succ n);+femb = \ n i -> split n with (ln , n') ->+ ! case ln of {+ z -> case i of {}+ | s -> split i with (li , i') ->+ case li of {+ z -> [fz n]+ | s -> [fs n (femb n' i')] }};++finv : (n:Nat) -> Fin n -> Fin n;+finv = \ n i -> split n with (ln , n') ->+ ! case ln of {+ z -> case i of {}+ | s -> split i with (li , i') ->+ case li of {+ z -> [fmax n']+ | s -> [fs n' (finv n' i')] }};+
+ examples/Maybe.pi view
@@ -0,0 +1,10 @@+:l Unit.pi++Maybe : Type -> Type;+Maybe = \ A -> (l : { nothing just }) *+ case l of {+ nothing -> Unit+ | just -> A };+++
+ examples/Nat.pi view
@@ -0,0 +1,94 @@+:l Bool.pi++Nat : Type;+Nat = (l : { z s }) * case l of {+ z -> Unit+ | s -> [Nat] };++zero : Nat;+zero = ('z,'unit);++succ : Nat -> Nat;+succ = \ n -> ('s,n);++one : Nat;+one = succ zero;++two : Nat;+two = succ one;++add : Nat -> Nat -> Nat;+add = \ m n -> split m with (lm , m') ->+ ! case lm of {+ z -> [n]+ | s -> [succ (add 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 -> ['true]+ | s -> ['false] }+ | s -> case ln of {+ z -> ['false]+ | s -> [eqbNat m' n'] } };++eqNat : Nat -> Nat -> Type;+eqNat = \ m n -> T (eqbNat m n);++reflNat : (n:Nat) -> eqNat n n;+reflNat = \ n -> split n with (ln , n') ->+ ! case ln of {+ z -> ['unit]+ | s -> [reflNat n'] };++substNat : (P : Nat -> Type) + -> (m : Nat) -> (n : Nat)+ -> (eqNat m n)+ -> P m -> P n;+substNat = \ P m n q x -> + split m with (lm , m') ->+ split n with (ln , n') ->+ ! case lm of {+ z -> case ln of {+ z -> case m' of {+ unit -> case n' of {+ unit -> [x]}}+ | s -> case q of {}}+ | s -> case ln of { + z -> case q of {}+ | s -> [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);++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;++addCom0 : (n:Nat) -> eqNat n (add n zero);+addCom0 = \ n -> split n with (ln , n') ->+ ! case ln of { + z -> case n' of {+ unit -> [reflNat zero]}+ | s -> [addCom0 n'] };++addComS : (m:Nat) -> (n:Nat) ->+ (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] };++addCom : (m:Nat) -> (n:Nat) ->+ (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'))+ (addCom m' n) (addComS n m')] };+
+ examples/Streams.pi view
@@ -0,0 +1,91 @@+Unit : Type;+Unit = { unit };++Empty : Type;+Empty = { };++Bool : Type;+Bool = { true false };++T : Bool -> Type;+T = \ b -> case b of {+ true -> Unit+ | false -> Empty };+++Nat : Type;+Nat = (l : { z s }) * case l of {+ z -> Unit+ | s -> [Nat] };++zero : Nat;+zero = ('z,'unit);++succ : Nat -> Nat;+succ = \ n -> ('s,n);++one : Nat;+one = succ zero;++two : Nat;+two = succ one;++add : Nat -> Nat -> Nat;+add = \ m n -> split m with (lm , m') ->+ ! case lm of {+ z -> [n]+ | s -> [succ (add 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 -> ['true]+ | s -> ['false] }+ | s -> case ln of {+ z -> ['false]+ | s -> [eqbNat m' n'] } };++eqNat : Nat -> Nat -> Type;+eqNat = \ m n -> T (eqbNat m n);++reflNat : (n:Nat) -> eqNat n n;+reflNat = \ n -> split n with (ln , n') ->+ ! case ln of {+ z -> ['unit]+ | s -> [reflNat n'] };+++Stream : Type -> Type;+Stream = \ a -> a * [^ (Stream a)];++put : (a : Type) -> a -> Stream a -> Stream a;+put = \ a x xs -> (x,[xs]);++from : Nat -> Stream Nat;+from = \ n -> (n, [from (succ n)]);++tail : (a:Type) -> Stream a -> Stream a;+tail = \ a xs -> split xs with (x , xs') -> ! 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')]);++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'))];++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')]);++lemma : (n : Nat) -> eqStream Nat eqNat (from (succ n)) + (map Nat Nat succ (from n));+lemma = \ n -> ((reflNat (succ n)),[lemma (succ n)]);
+ examples/Unit.pi view
@@ -0,0 +1,2 @@+Unit : Type;+Unit = { unit };
+ examples/Universe.pi view
@@ -0,0 +1,47 @@+:l Maybe.pi++data : Type;+El : data -> Type;++data = ( l : {empty maybe sigma box} ) * + case l of {+ empty -> Unit+ | maybe -> [data]+ | sigma -> [(a : data) * (El a -> data)]+ | box -> [^ data] }; ++El = \ a -> split a with (la,a') ->+ case la of {+ empty -> {}+ | maybe -> Maybe [El a']+ | sigma -> split a' with (b,c) ->+ [(x:El b)*(El (c x))]+ | box -> [El (! a')] };++unit : data;+unit = ('maybe,('empty,'unit));++un : El unit;+un = ('nothing,'unit);++bool : data;+bool = ('maybe, unit);++tt : El bool;+tt = ('nothing,'unit);++ff : El bool;+ff = ('just,('nothing,'unit));++nat : data;+nat = ('sigma,(bool,\ b -> split b with (lb,b') ->+ case lb of {+ nothing -> unit+ | just -> ('box, [nat]) }));+ +zero : El nat;+zero = (tt,un);++succ : El nat -> El nat;+succ = \ n -> (ff,n);+
+ examples/Vec.pi view
@@ -0,0 +1,23 @@+:l Fin.pi++Vec : Nat -> Type -> Type;+Vec = \ m a -> split m with (lm , m') ->+ ! case lm of {+ z -> [Unit]+ | s -> [a * Vec m' a] }; ++vnil : (a : Type) -> Vec zero a;+vnil = \ a -> 'unit;++vcons : (a : Type) -> (n : Nat) -> a -> Vec n a -> Vec (succ n) a;+vcons = \ a b x xs -> (x ,xs);++nth : (a : Type) -> (n : Nat) -> (xs : Vec n a) -> Fin n -> a;+nth = \ a n xs i -> split n with (ln , n') ->+ ! case ln of {+ z -> case i of {}+ | s -> split xs with (x, xs') ->+ split i with (li , i') ->+ case li of {+ z -> [x]+ | s -> [nth a n' xs' i']}}
+ examples/stl.pi view
@@ -0,0 +1,131 @@+:l Bool.pi++{- stl.pi++Encoding of the simply typed lambda calculus+-}++pair : (a:Bool) -> (b:Bool) -> ((T a) * (T b)) -> T (andb a b);+pair = \ a b xy ->+ split xy with (x,y) -> + case a of {+ true -> y+ | false -> case x of {}};++unpair : (a:Bool) -> (b:Bool) -> T (andb a b) -> ((T a) * (T b));+unpair = \ a b x ->+ case a of {+ true -> case b of {+ true -> ('unit,'unit)+ | false -> case x of {}}+ | false -> case x of {}};++Ty : Type;+Ty = (l : {base arr}) * + case l of {+ base -> Unit+ | arr -> [Ty * Ty] };++base : Ty;+base = ('base, 'unit);++arr : Ty -> Ty -> Ty;+arr = \ a b -> ('arr,(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 -> ['true]+ | arr -> ['false]}+ | arr -> case lb of {+ base -> ['false]+ | arr -> split a' with (a0, a1) ->+ split b' with (b0, b1) ->+ [andb (eqb a0 b0) (eqb a1 b1)]}};++eq : Ty -> Ty -> Type;+eq = \ a b -> T (eqb a b);++refl : (a:Ty) -> eq a a;+refl = \ a -> split a with (la, a') ->+ ! case la of {+ base -> ['unit]+ | arr -> split a' with (b,c) ->+ [pair (eqb b b) (eqb c c) ((refl b) , (refl c))] };++subst : (P : Ty -> Type) + -> (a : Ty) -> (b : Ty)+ -> (eq a b)+ -> P a -> P b;+subst = \ P a b p x -> + split a with (la, a') ->+ split b with (lb, b') ->+ ! case la of {+ base -> case lb of {+ base -> case a' of {+ unit -> case b' of {+ unit -> [x]}}+ | arr -> case p of {}}+ | arr -> case lb of {+ base -> case p of {}+ | arr -> 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! -}++Con : Type;+Con = ( l : {empty ext} ) * + case l of {+ empty -> Unit+ | ext -> [Con * Ty] };++empty : Con;+empty = ('empty,'unit);++ext : Con -> Ty -> Con;+ext = \ g a -> ('ext,(g,a));++Var : Con -> Ty -> Type;+Var = \ g a -> + split g with (lg, g') -> + case lg of {+ empty -> Empty+ | ext -> split g' with (d, a') ->+ (l : {vz vs}) *+ ! case l of {+ vz -> [eq a a']+ | vs -> [Var d a] }};++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 -> + (l : {var app lam}) *+ case l of {+ var -> Var g a+ | app -> [(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] }};+ +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)));++lam : (g:Con) -> (a:Ty) -> (b:Ty)+ -> Lam (ext g a) b -> Lam g (arr a b);+lam = \ g a b t -> ('lam,t);
+ pisigma.cabal view
@@ -0,0 +1,24 @@+cabal-version: >= 1.6+name: pisigma+version: 0.1.0.1+license: BSD3+license-file: LICENSE+data-files: examples/*.pi+author: Thorsten Altenkirch <txa@cs.nott.ac.uk>,+ Andres Loeh <kspisigma@andres-loeh.de>+maintainer: Thorsten Altenkirch <txa@cs.nott.ac.uk>,+ Andres Loeh <kspisigma@andres-loeh.de>+description: dependently typed core language+synopsis: dependently typed core language+category: Development, Language, Dependent Types+build-type: Simple++executable pisigma+ main-is: PiSigma.hs+ hs-source-dirs:src+ build-depends: base >= 4 && < 5,+ array >= 0.2 && < 0.3,+ mtl >= 1.1 && < 1.2,+ haskeline >= 0.6 && < 0.7,+ parsec >= 3 && < 4,+ ansi-wl-pprint >= 0.5 && <1
+ src/PiSigma.hs view
@@ -0,0 +1,265 @@+{-# LANGUAGE ScopedTypeVariables #-}++module Main where++import Prelude hiding (catch)+import System.IO+import System.Environment+import System.Console.Haskeline hiding (catch)+import Control.Monad+import Control.Monad.Trans+import Control.Monad.State+import Control.Exception+import Data.List+import Data.Char+ +import PiSigma.Syntax+import PiSigma.Evaluation+import PiSigma.Check+import PiSigma.Print+import PiSigma.Nf+import PiSigma.Equality+import PiSigma.Parser++main :: IO ()+main = + do+ args <- getArgs+ let ini = mapM_ (handleCommand . Load) args+ liftM fst $ runStateT (runInputT + (setComplete pisigmaCompletion defaultSettings)+ (ini >> repl))+ initialReplState++-- | Completion in PiSigma. For the moment, we use file name completion+-- while in a load command, and identifier completion everywhere else.+pisigmaCompletion :: CompletionFunc (StateT ReplState IO)+pisigmaCompletion (x1,x2)+ | ":l" `isPrefixOf` reverse x1 = completeFilename (x1,x2)+ | otherwise = completeWord Nothing " " identifier (x1,x2)+ where+ identifier x = do+ (Scope sc,env) <- gets replState+ let names = map fst sc+ xr = reverse x+ cands = filter (x `isPrefixOf`) names+ return $ map simpleCompletion (sort cands)++type Repl = InputT (StateT ReplState IO)+type Continue = Bool++data ReplState =+ ReplState+ { replState :: (Scope, EnvEntries)+ , replFiles :: [FilePath]+ }++data ReplCommand =+ Load String+ | Reload+ | Quit+ | EvalPhrase Phrase+ | Noop+ | Clear+ | Equal (Term,Term)+ | TypeOf Term+ | Help++-- TODO:+-- browse current identifiers++-- | Preliminary interpreter help message.+help :: String+help =+ unlines $+ [ "PiSigma currently supports the following commands:",+ "",+ " :l load a source file",+ " :r reload current source file",+ " :c clear the environment",+ " :t ask for the type of a term",+ " :e test two terms for beta equality",+ " :q quit",+ "",+ "Type a declaration or an expression to evaluate it." ]++initialReplState :: ReplState+initialReplState = + ReplState (emptyScope, emptyE) []++replStep :: Repl Continue+replStep =+ do+ f <- lift $ gets replFiles+ x <- getInputLine (unwords (reverse f) ++ "> ")+ c <- interpretInput x+ handleCommand c++-- | Preliminary input interpretation, based on the+-- current parser and no particular intelligence in+-- parsing commands correctly.+interpretInput :: Maybe String -> Repl ReplCommand+interpretInput Nothing = return Quit+interpretInput (Just x)+ | ":l" `isPrefixOf` x = case break (== ' ') x of+ (x1,x2) -> return (Load (norm (trim x2)))+ | ":r" `isPrefixOf` x = return Reload+ | ":q" `isPrefixOf` x = return Quit+ | ":c" `isPrefixOf` x = return Clear+ | ":e" `isPrefixOf` x = case break (== ' ') x of+ (x1,x2) -> parseInputInteractive s2Terms Equal x2+ | ":t" `isPrefixOf` x = case break (== ' ') x of+ (x1,x2) -> parseInputInteractive sTerm TypeOf x2+ | ":h" `isPrefixOf` x || ":?" `isPrefixOf` x+ = return Help+ | ":" `isPrefixOf` x = replMessage "unknown command" >> return Noop+ | otherwise = parseInputInteractive sPhrase EvalPhrase x++-- | Turn a string into a Repl command.+parseInput :: String -> SParser t -> (t -> ReplCommand) ->+ String -> Repl ReplCommand+parseInput f p cmd s =+ case parse p f s of+ Left s -> do+ liftIO $ putStrLn ("Parse error: " ++ show s ++ "\n")+ return Noop+ Right p -> return (cmd p)++parseInputInteractive = parseInput "<interactive>"++-- | Placeholder for a message function that can depend+-- on verbosity settings.+replMessage :: String -> Repl ()+replMessage = liftIO . putStrLn++-- | Command handler. Returns a flag indicating whether+-- the interpreter should continue.+handleCommand :: ReplCommand -> Repl Continue+handleCommand c =+ case c of+ Help ->+ do+ replMessage $ help+ return True+ Load f ->+ do+ fs <- lift $ gets replFiles+ if f `elem` fs then do+ replMessage $ "Skipping " ++ f ++ "."+ return True+ else do+ mx <- liftIO $ catch (liftM Just (readFile f))+ (\ (_ :: IOException) -> return Nothing)+ case mx of+ Nothing -> do+ replMessage $ "Could not find " ++ f ++ "."+ return True+ Just x -> do+ -- Allow source files to have interpreter commands at the top;+ -- we currently use this as a replacement for a module system+ let (cmds,rest) = span (":" `isPrefixOf`) (lines x)+ mapM_ (\ c -> interpretInput (Just c) >>= handleCommand) cmds+ -- We print the "Loaded" message after executing initial+ -- interpreter commands in order to reflect the dependency+ -- order of different source files.+ replMessage $ "Loaded " ++ f ++ "."+ p <- parseInput f sProg (EvalPhrase . Prog)+ (unlines (replicate (length cmds) "" ++ rest))+ lift $ modify (\ s -> s { replFiles =+ case replFiles s of+ (g : fs) | g == f -> g : fs+ xs -> f : xs })+ handleCommand p+ Reload ->+ do+ f <- lift $ gets replFiles+ handleCommand Clear+ mapM_ (handleCommand . Load) (reverse f)+ return True+ Quit ->+ return False+ EvalPhrase (Prog p) ->+ do+ execProg p+ return True+ EvalPhrase (Term t) ->+ do+ execTerm t+ return True+ Equal (t1,t2) ->+ do+ eqTerms t1 t2+ return True+ TypeOf t ->+ do+ inferTerm t+ return True+ Clear ->+ do+ lift $ put initialReplState+ return True+ Noop ->+ return True++execProg :: Prog -> Repl ()+execProg p =+ do+ s <- lift get+ let (con,env) = replState s+ case run env (checkProg (p,con)) of+ Right s' -> lift $ put (s { replState = s' })+ Left e -> liftIO $ putStrLn e++execTerm :: Term -> Repl ()+execTerm t =+ do+ s <- lift get+ let (con,env) = replState s+ p = do+ a <- infer (t,con)+ pa <- prt a+ t' <- nf [] (t,con)+ pt <- prt t'+ return (pt++"\n: "++pa)+ case run env p of+ Right (m,_) -> liftIO $ putStrLn m+ Left e -> liftIO $ putStrLn e++eqTerms :: Term -> Term -> Repl ()+eqTerms t1 t2 =+ do+ s <- lift get+ let (con,env) = replState s+ p = eq (t1,con) (t2,con)+ case run env p of+ Right _ -> liftIO $ putStrLn "yes"+ Left e -> liftIO $ putStrLn e+ ++inferTerm :: Term -> Repl ()+inferTerm t =+ do+ s <- lift get+ let (con,env) = replState s+ p = infer (t,con) >>= prt+ case run env p of+ Right (m,_) -> liftIO $ putStrLn m+ Left e -> liftIO $ putStrLn e++-- | Run the interpreter as long as desired.+repl :: Repl ()+repl =+ do+ continue <- replStep+ when continue repl++-- * Helper functions++trim :: String -> String+trim = reverse . dropWhile isSpace . reverse . dropWhile isSpace++norm :: String -> String+norm [] = []+norm ('\\':c:xs) = c : norm xs+norm (x:xs) = x : norm xs+