Type aliasing ListInt = Lis Int; does not produce an (eval) error a…

…nymore

* tests/eval_test.ml: Added test for type aliasing
* src/env.ml: Added a `Vinductive` value to detect type aliasing calls
* src/eval.ml: type aliasing calls to constructor are recognized and not evaluated
* src/REPL.ml: file provided using the command line are read in the correct order
* samples/typer_proof.typer: Added a new example `samples/typer_proof.typer`
	which implements a Tree based interpreter and a Stack VM.

btl/builtins.typer

@@ -127,6 +127,7 @@ float_   = Built-in "float_"   (Float     -> Sexp);
 
 Macro  = typecons (Macro)
   (Macro_ (List Sexp -> Sexp));
+% (macro ((ctx : Context) ≡> (a : Type) ≡> (arg : List Sexp) -> Sexp));
 
 Macro_ = datacons Macro Macro_ ;
 
@@ -207,6 +208,18 @@ length = lambda a ≡>
       | nil => 0
       | cons hd tl => (1 + (length tl));
 
+reverse : (a : Type) ≡> List a -> List a -> List a;
+reverse = lambda a ≡> lambda l -> lambda t ->
+    case l
+        | nil => t
+        | cons hd tl => reverse tl (cons hd t);
+
+concat : (a : Type) ≡> List a -> List a -> List a;
+concat = lambda a ≡>
+    lambda l -> lambda t ->
+        let l' = reverse l nil in
+            reverse l' t;
+
 % ML's typical `head` function is not total, so can't be defined
 % as-is in Typer.  There are several workarounds:
 % - Provide a default value : (a : Type) ≡> List a -> a -> a;

samples/typer_proof.typer

@@ -0,0 +1,78 @@
+%   Example from `An Introduction to programming and proving with Dependent Types in Coq`
+%   http://adam.chlipala.net/cpdt/
+%
+%
+
+type OperatorType
+    | Plus
+    | Times;
+
+Exp : Type;
+type Exp
+    | Const Int
+    | BinaryNode OperatorType Exp Exp;
+
+% retrieve function from OperatorType
+binopDenote : OperatorType -> Int -> Int -> Int;
+binopDenote b =
+    case b
+        | Plus => _+_
+        | Times => _*_;
+
+
+% Tree based interpreter
+expDenote : Exp -> Int;
+expDenote e =
+    case e
+        | Const n => n
+        | BinaryNode op lhs rhs =>
+            (binopDenote op) (expDenote lhs) (expDenote rhs);
+
+% Create a Stack based VM
+% -----------------------
+
+% Instruction set
+type Instr
+    | IConst Int
+    | IBinop OperatorType;
+
+% Type alias
+Program = List Instr;
+Stack   = List Int;
+
+% eval instruction
+instrDenote : Instr -> Stack -> Option Stack;
+instrDenote i s =
+    case i
+        | IConst n => some (cons n s)
+        | IBinop b =>
+            (case s
+                | cons arg1 s' => (case s'
+                    | cons arg2 s'' => some
+                        (cons ((binopDenote b) arg1 arg2) s'')
+                    | _ => none)
+                | _ => none);
+
+% eval program
+progDenote : Program -> Stack -> Option Stack;
+progDenote p s =
+    case p
+        | nil => some s
+        | cons i p' => (case instrDenote i s
+            | none => none
+            | some s' => progDenote p' s');
+
+% Compile expression to Program
+compile : Exp -> Program;
+compile e =
+    case e
+        | Const n => cons (IConst n) nil
+        | BinaryNode b lhs rhs =>
+            concat (compile rhs) (concat (compile lhs) (cons (IBinop b) nil));
+
+% Make a proof that our VM is behaving like our interpreter
+% ---------------------------------------------------------
+
+%             Stack VM         ==       Interpreter
+%   progDenote (compile e) nil == some (expDenote (cons e nil))
+

src/REPL.ml

@@ -277,7 +277,7 @@ let main () =
     print_string (make_sep '-');
     flush stdout;
 
-    let (i, ectx, rctx) = readfiles (!arg_files) (1, ectx, rctx) true in
+    let (i, ectx, rctx) = readfiles (List.rev !arg_files) (1, ectx, rctx) true in
 
     flush stdout;
 

src/env.ml

@@ -57,6 +57,7 @@ type value_type =
     (* Unable to eval during macro expansion, only throw if the value is used *)
     | Vundefined
     | Vdummy
+    | Vinductive
     | Vin of in_channel
     | Vout of out_channel
     | Vcommand of (unit -> value_type)
@@ -76,6 +77,7 @@ let rec value_equal a b =
     | Vout (c1), Vout(c2)        -> c2 = c2
     | Vcommand (f1), Vcommand(f2)-> f1 = f2
     | Vdummy, Vdummy             -> warning dloc "Vdummy"; true
+    | Vinductive, Vinductive     -> warning dloc "Vinductive"; true
 
     | Closure(s1, b1, ctx1), Closure(s2, b2, ctx2) ->
       warning dloc "Closure";
@@ -116,12 +118,14 @@ let value_name v =
     | Closure  _ -> "Closure"
     | Vbuiltin _ -> "Vbuiltin"
     | Vcommand _ -> "Vcommand"
+    | Vinductive  -> "Vinductive"
 
 let rec value_string v =
   match v with
     | Vin   _ -> "in_channel"
     | Vout  _ -> "out_channe;"
     | Vdummy     -> "dummy"
+    | Vinductive -> "inductive"
     | Vundefined -> "<undefined!>"
     | Vcommand _ -> "command"
     | Vstring  s -> "\"" ^ s ^ "\""

src/eval.ml

@@ -267,7 +267,7 @@ let rec _eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type
         | Imm(Integer (_, i))       -> Vint(i)
         | Imm(String (_, s))        -> Vstring(s)
         | Imm(sxp)                  -> Vsexp(sxp)
-        | Inductive (_, _)          -> Vdummy
+        | Inductive (_, _)          -> Vinductive
         | Cons (label)              -> Vcons (label, [])
         | Lambda ((_, n), lxp)      -> Closure(n, lxp, ctx)
         | Builtin ((_, str))        -> Vbuiltin(str)
@@ -354,6 +354,8 @@ and eval_call loc unef i f args =
             error loc ("Requested Built-in `" ^ name ^ "` does not exist")
           | e -> error loc ("Exception thrown from primitive `" ^ name ^"`"))
 
+  (* Type Alias is not a fun call, we just ignore it*)
+  | Vinductive, _ -> Vundefined
   | _ -> value_fatal loc f "Trying to call a non-function!"
 
 and eval_case ctx i loc target pat dflt =

tests/eval_test.ml

@@ -393,6 +393,9 @@ let _ = test_eval_eqv_named
 
   "2;"
 
+let _ = test_eval_eqv_named
+  "Type Alias" "ListInt = List Int;" "" (* == *) ""
+
 (* run all tests *)
 let _ = run_all ()