Setepenre pushed to branch master at Stefan / Typer

Commits: 129d4b0e by Pierre Delaunay at 2017-02-19T10:49:29-05:00 Type aliasing `ListInt = Lis Int;` does not produce an (eval) error anymore

* 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.

- - - - - a6aff881 by Pierre Delaunay at 2017-02-19T10:55:07-05:00 Merge branch 'master' of gitlab.com:monnier/typer

- - - - -

7 changed files:

- btl/builtins.typer - − samples/macro_decls.typer - + samples/typer_proof.typer - src/REPL.ml - src/env.ml - src/eval.ml - tests/eval_test.ml

Changes:

===================================== btl/builtins.typer ===================================== --- a/btl/builtins.typer +++ b/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/macro_decls.typer deleted ===================================== --- a/samples/macro_decls.typer +++ /dev/null @@ -1,6 +0,0 @@ -type_ = Macro_ (lambda (x : List Sexp) -> head Sexp x); - - -type Nat - | zero - | succ Nat;

===================================== samples/typer_proof.typer ===================================== --- /dev/null +++ b/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 ===================================== --- a/src/REPL.ml +++ b/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 ===================================== --- a/src/env.ml +++ b/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 ===================================== --- a/src/eval.ml +++ b/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 ===================================== --- a/tests/eval_test.ml +++ b/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 ()

View it on GitLab: https://gitlab.com/monnier/typer/compare/0bd0dac5c3e9a74fb52a8a4667118eca511...