Setepenre pushed to branch master at Stefan / Typer
Commits: 791587e6 by Pierre Delaunay at 2016-11-07T15:47:53-05:00 Changes to be committed: * btl/types.typer - added a new DMacro_ constructor to build declaration macro (DMacro_ : List Sexp -> List Sexp) (Macro_ : List Sexp -> Sexp)
* src/lparse.ml - Lambda Arrow type keep var name when possible (needed for arg re ordering)
* tests/macro_test.ml - Force case to use lexp_check instead of lexp_infer using hastype
- - - - -
6 changed files:
- btl/types.typer - src/builtin.ml - src/lparse.ml - tests/eval_test.ml - tests/lexp_test.ml - tests/macro_test.ml
Changes:
===================================== btl/types.typer ===================================== --- a/btl/types.typer +++ b/btl/types.typer @@ -109,13 +109,21 @@ node_ = Built-in "node_" (Sexp -> List Sexp -> Sexp); integer_ = Built-in "integer_" (Int -> Sexp); float_ = Built-in "float_" (Float -> Sexp);
-Macro = inductive_ (Macro) (Macro_ (List Sexp -> Sexp)); +Macro = inductive_ (Macro) + (Macro_ (List Sexp -> Sexp)) + (DMacro_ (List Sexp -> List Sexp)); + Macro_ = inductive-cons Macro Macro_ ; +DMacro_ = inductive-cons Macro DMacro_ ;
expand_macro_ : Macro -> List Sexp -> Sexp; expand_macro_ m args = case m | Macro_ f => (f args);
+expand_dmacro_ : Macro -> List Sexp -> List Sexp; +expand_dmacro_ m args = case m + | DMacro_ f => (f args); + sexp_dispatch_ = Built-in "sexp_dispatch_" ( (a : Type) ≡> Sexp @@ -168,14 +176,13 @@ read = Built-in "read" (FileHandle -> Int -> IO String); % -----------------------------------------------------
Attribute = Built-in "Attribute"; -new-attribute = Built-in "new-attribute" (Macro); +new-attribute = Built-in "new-attribute" Macro; +get-attribute = Built-in "get-attribute" Macro; +has-attribute = Built-in "has-attribute" Macro;
add-attribute = Built-in "add-attribute" (List Sexp -> Sexp); attribute = Macro_ add-attribute;
-get-attribute = Built-in "get-attribute" Macro; -has-attribute = Built-in "has-attribute" (Macro); - % ----------------------------------------------------- % Context Accessors % ----------------------------------------------------- @@ -187,5 +194,3 @@ declexpr = Built-in "declexpr" Macro;
- -
===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -53,6 +53,7 @@ let predef_name = [ "Bool"; "Macro"; "expand_macro_"; + "expand_dmacro_"; ]
let default_predef_map : predef_table =
===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -280,7 +280,7 @@ let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype = let nctx = env_extend ctx var Variable ltp in let lbody, lbtp = lexp_infer body nctx in
- let lambda_type = mkArrow (kind, None, ltp, tloc, lbtp) in + let lambda_type = mkArrow (kind, Some var, ltp, tloc, lbtp) in mkLambda(kind, var, ltp, lbody), lambda_type
| Pcall (fname, _args) -> lexp_call fname _args ctx trace @@ -594,11 +594,19 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = extract_order ret ((kind, varname, ltp)::aargs) (if kind = Aexplicit then (varname::eargs) else eargs)
- | _ -> (List.rev aargs), List.rev eargs in + | e -> (List.rev aargs), List.rev eargs in
(* first list has all the arguments, second only holds explicit arguments *) let order, eorder = extract_order ltp [] [] in
+ (*) + print_string "Type :"; lexp_print ltp; print_string "\n"; + print_string "Order:"; List.iter (fun (_, b, _) -> print_string (b ^ " ")) (order); print_string "\n"; + print_string "Sarg1: "; + List.iter (fun lxp -> sexp_print lxp; print_string ", ") sargs; + print_string "\n";*) + + (* from arg order build a dictionnary that will hold the defined args *) let args_dict = List.fold_left (fun map (kind, key, _) -> SMap.add key (kind, None) map) SMap.empty order in @@ -606,7 +614,10 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = let args_dict, eargs = List.fold_left (fun (map, eargs) sexp -> match sexp with | Node (Symbol (_, "_:=_"), [Symbol (_, aname); sarg]) -> - let kind, _ = SMap.find aname map in + let kind, _ = try SMap.find aname map + with Not_found -> + print_string (aname ^ " was not found" ^ "\n"); + Aerasable, None in (SMap.add aname (kind, Some sarg) map), (if kind = Aexplicit then (match eargs with @@ -618,11 +629,6 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = | _ -> map, [])) (args_dict, eorder) sargs in
- (* - print_string "Type :"; lexp_print ltp; print_string "\n"; - print_string "Order:"; List.iter (fun (a, b) -> print_string (b ^ " ")) (order); print_string "\n"; - print_string "Sarg1: "; - List.iter (fun lxp -> sexp_print lxp; print_string ", ") sargs; *)
(* Generate an argument list with the correct order *) let sargs2 = List.map (fun (_, name, ltp) -> @@ -724,10 +730,16 @@ and lexp_parse_inductive ctors ctx i =
(* Macro declaration handling, return a list of declarations * to be processed *) -and lexp_expand_macro macro_funct sargs ctx trace = +and lexp_expand_macro macro_funct sargs ctx trace + = lexp_expand_macro_ macro_funct sargs ctx trace "expand_macro_" + +and lexp_expand_dmacro macro_funct sargs ctx trace + = lexp_expand_macro_ macro_funct sargs ctx trace "expand_dmacro_" + +and lexp_expand_macro_ macro_funct sargs ctx trace expand_fun =
(* Build the function to be called *) - let macro_expand = get_predef "expand_macro_" ctx in + let macro_expand = get_predef expand_fun ctx in let args = [(Aexplicit, macro_funct); (Aexplicit, (olist2tlist_lexp sargs ctx))] in
let macro = mkCall (macro_expand, args) in @@ -773,7 +785,7 @@ and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * elab_context) = [], ctx)
| _ ->( - let ret = lexp_expand_macro body sargs ctx [] in + let ret = lexp_expand_dmacro body sargs ctx [] in
(* convert typer list to ocaml *) let decls = tlist2olist [] ret in @@ -786,7 +798,7 @@ and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * elab_context) =
(* read as pexp_declaraton *) pexp_decls_all decls, ctx) - with _ -> + with e -> fatal loc ("Macro `" ^ mname ^ "`not found")
(* Parse let declaration *)
===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -337,7 +337,7 @@ let _ = test_eval_eqv_named let _ = test_eval_eqv_named "Implicit Arguments"
- "default = new-attribute (List Sexp -> Sexp); + "default = new-attribute (Int -> Bool); attribute Int default (lambda (lst : List Sexp) -> integer_ 1);
fun = lambda (x : Int) =>
===================================== tests/lexp_test.ml ===================================== --- a/tests/lexp_test.ml +++ b/tests/lexp_test.ml @@ -33,7 +33,7 @@ open Lparse (* add_def *)
open Builtin
-(* default environment *) +(* default environment * ) let lctx = default_lctx
@@ -67,7 +67,7 @@ let _ = (add_test "LEXP" "lexp_print" (fun () -> let str2 = to_str ret2 in
if str1 = str2 then success () else failure () -)) +)) *)
(* let set_to_list s =
===================================== tests/macro_test.ml ===================================== --- a/tests/macro_test.ml +++ b/tests/macro_test.ml @@ -47,9 +47,9 @@ let _ = (add_test "MACROS" "macros base" (fun () -> (* define 'lambda x -> x * x' using macros *) let dcode = " my_fun = lambda (x : List Sexp) -> - let hd = case x + let hd = (case x | cons hd tl => hd - | nil => symbol_ "x" in + | nil => symbol_ "x") : Sexp in (node_ (symbol_ "_*_") (cons (a := Sexp) hd (cons (a := Sexp) hd (nil (a := Sexp))))); @@ -77,7 +77,7 @@ let _ = (add_test "MACROS" "macros decls" (fun () -> (cons(a := Sexp) (node_ (symbol_ "_=_") (cons(a := Sexp) (symbol_ "b") (cons(a := Sexp) (integer_ 2) (nil(a := Sexp))))) (nil(a := Sexp)));
- my-decls = Macro_ decls-impl; + my-decls = DMacro_ decls-impl;
my-decls Nat;" in
View it on GitLab: https://gitlab.com/monnier/typer/commit/791587e6246d2f293a15bad5e7181ca96692...
Afficher les réponses par date
expand_macro_ : Macro -> List Sexp -> Sexp; expand_macro_ m args = case m | Macro_ f => (f args);
While we currently don't check it, our functions need to be *total*, meaning they must always handle (and terminate on) all cases.
So expand_macro_ should also handle the DMacro case.
- "default = new-attribute (List Sexp -> Sexp);
- "default = new-attribute (Int -> Bool); attribute Int default (lambda (lst : List Sexp) -> integer_ 1);
Hmm... I don't understand this change. The value you provide for the `default` arg of `Int` seems to have type (List Sexp -> Sexp) rather than (Int -> Bool).
let hd = case x
let hd = (case x | cons hd tl => hd
| nil => symbol_ \"x\" in
| nil => symbol_ \"x\") : Sexp in
Good catch, thanks. We could have done "hd : Sexp", of course.
Stefan