Setepenre pushed to branch master at Stefan / Typer

Commits: 49dad956 by Pierre Delaunay at 2016-09-07T15:13:34-04:00 finished type_ macro

Changes to be committed: * samples/inductive.typer - finished the type_ macro * samples/int_index_inconsistency.typer - type index are inconsistent * src/builtin.ml - improved error message

- - - - - 3ef3619c by Pierre Delaunay at 2016-09-07T15:15:21-04:00 Merge branch 'master' of gitlab.com:monnier/typer

- - - - -

5 changed files:

- samples/inductive.typer - + samples/int_index_inconsistency.typer - src/builtin.ml - src/lparse.ml - tests/eval_test.ml

Changes:

===================================== samples/inductive.typer ===================================== --- a/samples/inductive.typer +++ b/samples/inductive.typer @@ -1,10 +1,36 @@ +% build a declaration +% var-name = value-expr; +make-decl : Sexp -> Sexp -> Sexp; +make-decl var-name value-expr = + node_ (symbol_ "_=_") + (cons (a := Sexp) var-name + (cons (a := Sexp) value-expr (nil (a := Sexp)))); + +% build inductive-cons +% ctor-name = inductive-cons type-name ctor-name; +make-cons : Sexp -> Sexp -> Sexp; +make-cons ctor-name type-name = + make-decl ctor-name + (node_ (symbol_ "inductive-cons") + (cons (a := Sexp) type-name + (cons (a := Sexp) ctor-name (nil (a := Sexp))))); + +% buil type annotation +% var-name : type-expr; +make-ann : Sexp -> Sexp -> Sexp; +make-ann var-name type-expr = + node_ (symbol_ "_:_") + (cons (a := Sexp) var-name + (cons (a := Sexp) type-expr (nil (a := Sexp)))); + + type-impl = lambda (x : List Sexp) -> % x follow the mask -> (_|_ Nat zero (succ Nat)) % Type name --^ ^------^ constructors

% Get expression let expr = head (a := Sexp) x in - let sexp_nil = nil (a := Sexp) in + let sexp_nil = (nil (a := Sexp)) in

% Expression is node_ (symbol_ "|") (list) % we only care about the list bit @@ -18,29 +44,54 @@ type-impl = lambda (x : List Sexp) -> (lambda (float : Float) -> sexp_nil) % Float (lambda (lst : List Sexp) -> sexp_nil)) in % List of Sexp

+ % Get a name from a sexp + % (name t) -> name + % name -> name + let get-name : Sexp -> Sexp; + get-name sxp = + sexp_dispatch_ (a := Sexp) sxp + (lambda (op : Sexp) -> (lambda (lst : List Sexp) -> get-name op)) % Nodes + (lambda (str : String) -> symbol_ str) % Symbol + (lambda (str : String) -> symbol_ str) % String + (lambda (int : Int) -> symbol_ "error") % Integer + (lambda (float : Float) -> symbol_ "error") % Float + (lambda (lst : List Sexp) -> symbol_ "error") in % List of Sexp + let lst = get-list expr in

let name = head (a := Sexp) lst in let ctor = tail (a := Sexp) lst in

- % Create a forward declaration in case the declaration is recursive - let fdecl = node_ (symbol_ "_:_") - (cons (a := Sexp) name - (cons (a := Sexp) (symbol_ "Type") sexp_nil)) in + let type-name = get-name name in

% Create the inductive type definition let inductive = node_ (symbol_ "inductive_") - (cons (a := Sexp) (symbol_ "dlabel") ctor) in + (cons (a := Sexp) type-name ctor) in + + % Create a forward declaration in case the declaration is recursive + let fdecl = make-ann type-name (symbol_ "Type") in + let decl = make-decl type-name inductive in + + % Add constructors + let ctors = + let for-each : List Sexp -> List Sexp -> List Sexp; + for-each ctor acc = case ctor + | cons hd tl => ( + let acc2 = cons (a := Sexp) (make-cons (get-name hd) type-name) acc in + for-each tl acc2) + | nil => acc + in for-each ctor (nil (a := Sexp)) in

- let decl = node_ (symbol_ "_=_") - (cons (a := Sexp) name - (cons (a := Sexp) inductive sexp_nil)) in + % return decls + cons (a := Sexp) fdecl % Forward declaration + (cons (a := Sexp) decl % inductive type declaration + ctors); % constructor declarations

- cons (a := Sexp) fdecl - (cons (a := Sexp) decl sexp_nil);

type_ = Macro_ type-impl;

-type Nat - | zero - | succ Nat; +% (type_ (_|_ (Nat t) zero (succ Nat))) +% (type_ (_|_ Nat zero (succ Nat))) +type Nat t + | succ Nat + | zero;

===================================== samples/int_index_inconsistency.typer ===================================== --- /dev/null +++ b/samples/int_index_inconsistency.typer @@ -0,0 +1,10 @@ +% +% Int index inconsistency +% ------------------------------ +sqr = lambda (x : Int) -> x * x; +v = sqr 2; + +sqr2 : Int -> Int; +sqr2 = lambda x -> x * x; + +v2 = sqr2 2;

===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -191,8 +191,9 @@ let make_node loc depth args_val ctx =

let op, tlist = match args_val with | [Vsexp(op); lst] -> op, lst - | _ -> builtin_error loc - "node_ expects one 'Sexp' and one 'List Sexp'" in + | op::_ -> + builtin_error loc + ("node_ expects one 'Sexp' got " ^ (value_name op)) in

(* value_print tlist; print_string "\n"; *)

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -654,8 +654,6 @@ and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * lexp_context) = (* get a list of declaration *) let decls = eval elexp rctx in

- value_print decls; print_string "\n"; - (* convert typer list to ocaml *) let decls = tlist2olist [] decls in

===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -375,6 +375,29 @@ let _ = (add_test "EVAL" "List" (fun () -> ))

+let _ = (add_test "EVAL" "Monads" (fun () -> + reset_eval_trace (); + + let dcode = " + c = bind (a := Type) (b := Type) (open "./_build/w_file.txt" "w") + (lambda (f : FileHandle) -> + write f "Hello2"); + + " in + + let rctx, lctx = eval_decl_str dcode lctx rctx in + + let rcode = "run-io (a := Type) (b := Unit) c Unit" in + + (* Eval defined lambda *) + let ret = eval_expr_str rcode lctx rctx in + (* Expect a 3 results *) + match ret with + | [v] -> success () + | _ -> failure () +)) + + (* run all tests *) let _ = run_all ()

View it on GitLab: https://gitlab.com/monnier/typer/compare/915ca70f0c8c394e2b7cf724129c34b1c2b...