Setepenre pushed to branch master at Stefan / Typer

Commits: d377f901 by Pierre Delaunay at 2016-12-08T10:01:37-05:00 * src/eval.ml: fixed sexp_dispatch implementation (was evaluating with the wrong context) * Merging

- - - - - 461aff50 by Pierre Delaunay at 2016-12-08T10:03:19-05:00 Merge

- - - - - 409f7728 by Pierre Delaunay at 2016-12-15T00:12:39-05:00 Merge branch 'master' of gitlab.com:monnier/typer

- - - - - a2986fcc by Pierre Delaunay at 2016-12-17T12:34:53-05:00 * btl/builtins.typer: removed `DMacro_` as DMacro now retruns a single Sexp. * src/lparse.ml: removed `expand_dmacro` * tests/macro_test.ml: updated test * samples/inductive.typer: updated example * src/debruijn.ml: removed variable shadowing warning

- - - - - ce0dfdc4 by Pierre Delaunay at 2016-12-17T12:42:50-05:00 Merging

- - - - -

9 changed files:

- btl/builtins.typer - samples/inductive.typer - samples/quote.typer - src/builtin.ml - src/debruijn.ml - src/eval.ml - src/lparse.ml - src/pexp.ml - tests/macro_test.ml

Changes:

===================================== btl/builtins.typer ===================================== --- a/btl/builtins.typer +++ b/btl/builtins.typer @@ -157,25 +157,14 @@ integer_ = Built-in "integer_" (Int -> Sexp); float_ = Built-in "float_" (Float -> Sexp);

Macro = typecons (Macro) - (Macro_ (List Sexp -> Sexp)) - (DMacro_ (List Sexp -> List Sexp)); + (Macro_ (List Sexp -> Sexp));

Macro_ = datacons Macro Macro_ ; -DMacro_ = datacons Macro DMacro_ ; +

expand_macro_ : Macro -> List Sexp -> Sexp; expand_macro_ m args = case m - | Macro_ f => (f args) - % return first sexp if a DMacro_ is used - | DMacro_ f => (case (f args) - | cons hd tl => hd - | nil => (symbol_ "error")); - -expand_dmacro_ : Macro -> List Sexp -> List Sexp; -expand_dmacro_ m args = case m - | DMacro_ f => (f args) - % Wrap a Macro in a list of Sexp if Macro_ is used - | Macro_ f => cons (f args) nil; + | Macro_ f => (f args);

sexp_dispatch_ = Built-in "sexp_dispatch_" ( (a : Type) ≡>

===================================== samples/inductive.typer ===================================== --- a/samples/inductive.typer +++ b/samples/inductive.typer @@ -6,6 +6,10 @@ make-decl var-name value-expr = (cons var-name (cons value-expr nil));

+chain-decl : Sexp -> Sexp -> Sexp; +chain-decl a b = + node_ (symbol_ "_;_") (cons a (cons b nil)); + % build datacons % ctor-name = datacons type-name ctor-name; make-cons : Sexp -> Sexp -> Sexp; @@ -23,7 +27,6 @@ make-ann var-name type-expr = (cons var-name (cons type-expr nil));

- type-impl = lambda (x : List Sexp) -> % x follow the mask -> (_|_ Nat zero (succ Nat)) % Type name --^ ^------^ constructors @@ -77,32 +80,34 @@ type-impl = lambda (x : List Sexp) ->

% Add constructors let ctors = - let for-each : List Sexp -> List Sexp -> List Sexp; + let for-each : List Sexp -> Sexp -> Sexp; for-each ctr acc = case ctr | cons hd tl => ( - let acc2 = cons (make-cons (get-name hd) type-name) acc in + let acc2 = chain-decl (make-cons (get-name hd) type-name) acc in for-each tl acc2) | nil => acc - in for-each ctor nil in + in for-each ctor (node_ (symbol_ "_;_") nil) in

% return decls - (cons decl % inductive type declaration - ctors); % constructor declarations + (chain-decl decl % inductive type declaration + ctors); % constructor declarations

-type_ = DMacro_ type-impl; +type_ = Macro_ type-impl;

% (type_ (_|_ (Either t1 t2) (either-first t1) (either-second t2))) %type Either t1 t2 % | either-first t1 % | either-second t2;

+type A + | a Int;

%type Pair t1 t2 % | pair t1 t2;

-type Point t - | point (x : t) (y : t); +%type Point t +% | point (x : t) (y : t);

%get-first : (a : Type) => (b : Type) => Pair a b -> a; %get-second : (a : Type) => (b : Type) => Pair a b -> b;

===================================== samples/quote.typer ===================================== --- a/samples/quote.typer +++ b/samples/quote.typer @@ -55,34 +55,30 @@ my_sqr = lambda (x : List Sexp) -> | nil => symbol_ "x") : Sexp in (node_ (symbol_ "_*_") (cons hd (cons hd nil)));

-my_add = lambda (x : List Sexp) -> - let hd = (case x - | cons hd tl => hd - | nil => symbol_ "x") : Sexp in - (node_ (symbol_ "_=_") (cons hd (cons hd nil))); +% Quote +qq_sqr' = lambda (args : List Sexp) -> + let hd : Sexp; + hd = case args + | cons hd tl => hd + | nil => symbol_ "sqr expects a single argument" in + + quote ((uquote hd) * (uquote hd));

sqr = Macro_ my_sqr; -add = Macro_ my_add; +qqsqr = Macro_ qq_sqr'; + +% fun = Macro_ my_fun; +% main = fun 2;

my_fun = lambda (arg : List Sexp) -> let x = sqr 2 in integer_ 2;

fun = Macro_ my_fun; -main = fun 2; +main = qqsqr 2;

- -% Quote -%my_fun = lambda (args : List Sexp) -> -% let hd : Sexp; -% hd = case args -% | cons hd tl => hd -% | nil => symbol_ "sqr expects a single argument" in -% -% quote ((uquote hd) * (uquote hd)); - -x = 2; -sqr = Macro_ my_fun; +% x = 2; +% sqr = Macro_ my_fun;

% main = sqr 2; % a = Macro_ (lambda x -> quote (2 + 2)); @@ -90,4 +86,4 @@ sqr = Macro_ my_fun; % main = a Unit; % main = let x = 2 in quote (x * x); % main = let x = 2 in quote ((uquote x) * (uquote x)); - +% add = Macro_ my_add;

===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -74,7 +74,6 @@ let predef_name = [ "false"; "Macro"; "expand_macro_"; - "expand_dmacro_"; ]

(* FIXME: Actually, we should map the predefs to *values* since that's

===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -155,9 +155,6 @@ let lctx_extend (ctx : lexp_context) (def: vdef option) (v: varbind) (t: lexp) = let env_extend_rec r (ctx: elab_context) (def: vdef) (v: varbind) (t: lexp) = let (loc, name) = def in let ((n, map), env) = ctx in - (try let _ = senv_lookup name ctx in - warning loc ("Variable Shadowing " ^ name); - with Not_found -> ()); let nmap = SMap.add name n map in ((n + 1, nmap), lexp_ctx_cons env r (Some def) v t)

===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -162,8 +162,8 @@ let make_node loc depth args_val = let s = List.map (fun g -> match g with | Vsexp(sxp) -> sxp (* eval transform sexp into those... *) - | Vint (i) -> Integer(dloc, i) - | Vstring (s) -> String(dloc, s) + | Vint (i) -> Integer(dloc, i) + | Vstring (s) -> String(dloc, s) | _ -> (* print_rte_ctx ctx; *) value_error loc g "node_ expects 'List Sexp' second as arguments") args in @@ -284,14 +284,9 @@ let rec _eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type

(* Function call *) | Call (f, args) -> - (* we need to keep the trace from f and args evaluation - * else the trace will be truncated. - * we use _global_eval_trace to keep in memory previous steps *) - let ef = _eval f ctx trace in - let eargs = (List.map (fun e -> _eval e ctx (get_trace ())) args) in - eval_call (elexp_location f) f (get_trace ()) - ef - eargs + eval_call (elexp_location f) f trace + (_eval f ctx trace) + (List.map (fun e -> _eval e ctx trace) args)

(* Case *) | Case (loc, target, pat, dflt)

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -356,7 +356,7 @@ and parse_special_form ctx f args ot = | None -> (e, inferred_t) | Some t -> let e = check_inferred ctx e inferred_t t in (e, t)) - + | _ -> lexp_error loc f ("Unknown special-form: " ^ lexp_string f); let t = newMetatype loc in (newMetavar loc "<dummy>" t, t) @@ -380,7 +380,7 @@ and get_implicit_arg ctx loc name t = * call a `default-arg-filler` function, implemented in Typer, * just like `expand_macro_` function. That one can then look * things up in a table and/or do anything else it wants. *) - let v = lexp_expand_macro attr [] ctx t in + let v = lexp_expand_macro attr [] ctx (Some t) in

(* get the sexp returned by the macro *) let lsarg = match v with @@ -706,7 +706,7 @@ and check_case rtype (loc, target, ppatterns) ctx = mkCase (loc, tlxp, rtype, lpattern, dflt)

and handle_macro_call ctx func args t = - let sxp = match lexp_expand_macro func args ctx t with + let sxp = match lexp_expand_macro func args ctx (Some t) with | Vsexp (sxp) -> sxp | v -> value_fatal (lexp_location func) v "Macros should return a Sexp" in @@ -820,14 +820,6 @@ and lexp_parse_inductive ctors ctx = SMap.add name (make_args args ctx) lctors) SMap.empty ctors

-(* Macro declaration handling, return a list of declarations - * to be processed *) -and lexp_expand_macro macro_funct sargs ctx t - = lexp_expand_macro_ macro_funct sargs ctx (Some t) "expand_macro_" - -and lexp_expand_dmacro macro_funct sargs ctx - = lexp_expand_macro_ macro_funct sargs ctx None "expand_dmacro_" - and track_fv meta_ctx rctx lctx e = let (fvs, mvs) = OL.fv e in let nc = EV.not_closed rctx fvs in @@ -854,10 +846,10 @@ and track_fv meta_ctx rctx lctx e = | _ -> name in String.concat " " (List.map tfv nc)

-and lexp_expand_macro_ macro_funct sargs ctx ot expand_fun : value_type = +and lexp_expand_macro macro_funct sargs ctx ot: value_type =

(* Build the function to be called *) - let macro_expand = BI.get_predef expand_fun ctx in + let macro_expand = BI.get_predef "expand_macro_" ctx in (* FIXME: provide `ot` (the optional expected type) for non-decl macros. *) let args = [(Aexplicit, macro_funct); (Aexplicit, (BI.o2l_list ctx sargs))] in @@ -885,19 +877,13 @@ and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * elab_context) = try let lxp, ltp = infer (Pvar (loc, mname)) ctx in

(* FIXME: Check that (conv_p ltp Macro)! *) - let ret = lexp_expand_dmacro lxp sargs ctx in - - (* convert typer list to ocaml *) - let decls = BI.v2o_list ret in - - (* extract sexp from result *) - let decls = List.map (fun g -> - match g with - | Vsexp(sxp) -> sxp - | _ -> value_fatal loc g "Macro expects sexp list") decls in + let ret = lexp_expand_macro lxp sargs ctx None in + let decls = match ret with + | Vsexp(sexp) -> sexp + | _ -> fatal loc ("Macro `" ^ mname ^ "` should return a sexp") in

(* read as pexp_declaraton *) - pexp_decls_all decls, ctx + pexp_decls_all [decls], ctx with e -> fatal loc ("Macro `" ^ mname ^ "`not found")

===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -78,6 +78,19 @@ let rec pexp_location e = | Pcall (f, _) -> pexp_location f | Pcase (l, _, _) -> l

+let pexp_name e = + match e with + | Pimm _ -> "Pimm" + | Pbuiltin _ -> "Pbuiltin" + | Pvar (_,_) -> "Pvar" + | Phastype (_,_,_) -> "Phastype" + | Pmetavar (_, _) -> "Pmetavar" + | Plet (_, _, _) -> "Plet" + | Parrow (_, _, _, _, _) -> "Parrow" + | Plambda (_,(_,_), _, _) -> "Plambda" + | Pcall (_, _) -> "Pcall" + | Pcase (_, _, _) -> "Pcase" + let rec pexp_pat_location e = match e with | Ppatany l -> l | Ppatsym (l,_) -> l @@ -271,6 +284,7 @@ and pexp_p_decls e: pdecl list = * once expanded the Pmcall macro will produce a list of pdecl *) | Node (Symbol (l, op), args) -> [Pmcall((l, op), args)] | _ -> + print_string ((sexp_name e) ^ ": ""); sexp_print e; print_string ""\n"; pexp_error (sexp_location e) ("Unknown declaration"); []

and pexp_unparse (e : pexp) : sexp = @@ -333,8 +347,8 @@ and pexp_u_decls (ds: pdecl list) = | _ -> Node (Symbol (dummy_location, "_;_"), List.map pexp_u_decl ds)

-let pexp_print e = sexp_print (pexp_unparse e) - +and pexp_string e = sexp_string (pexp_unparse e) +and pexp_print e = print_string (pexp_string e)

(* Parse All Pexp as a list *) let pexp_parse_all (nodes: sexp list) = @@ -371,19 +385,3 @@ let _pexp_decl_str (str: string) tenv grm limit = let pexp_decl_str str = _pexp_decl_str str default_stt default_grammar (Some ";")

- -let pexp_string e = sexp_string (pexp_unparse e) -let pexp_print e = print_string (pexp_string e) - -let pexp_name e = - match e with - | Pimm _ -> "Pimm" - | Pbuiltin _ -> "Pbuiltin" - | Pvar (_,_) -> "Pvar" - | Phastype (_,_,_) -> "Phastype" - | Pmetavar (_, _) -> "Pmetavar" - | Plet (_, _, _) -> "Plet" - | Parrow (_, _, _, _, _) -> "Parrow" - | Plambda (_,(_,_), _, _) -> "Plambda" - | Pcall (_, _) -> "Pcall" - | Pcase (_, _, _) -> "Pcase"

===================================== tests/macro_test.ml ===================================== --- a/tests/macro_test.ml +++ b/tests/macro_test.ml @@ -71,12 +71,18 @@ let _ = (add_test "MACROS" "macros base" (fun () -> let _ = (add_test "MACROS" "macros decls" (fun () -> let dcode = " decls-impl = lambda (x : List Sexp) -> - cons (node_ (symbol_ "_=_") - (cons (symbol_ "a") (cons (integer_ 1) nil))) - (cons (node_ (symbol_ "_=_") - (cons (symbol_ "b") (cons (integer_ 2) nil))) nil); + let chain-decl : Sexp -> Sexp -> Sexp; + chain-decl a b = node_ (symbol_ "_;_") (cons a (cons b nil)) in

- my-decls = DMacro_ decls-impl; + let make-decl : String -> Int -> Sexp; + make-decl name val = + (node_ (symbol_ "_=_") (cons (symbol_ name) (cons (integer_ val) nil))) in + + let d1 = make-decl "a" 1 in + let d2 = make-decl "b" 2 in + chain-decl d1 d2; + + my-decls = Macro_ decls-impl;

my-decls Nat;" in

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