Stefan pushed to branch unification at Stefan / Typer
Commits: 5cd13387 by Pierre Delaunay at 2016-11-01T12:53:39-04:00 -
- - - - - b8dfa7da by Pierre Delaunay at 2016-11-07T13:21:31-05:00 * tests/eval_test.ml - added tests cases for argument reordering and implicit arguments
* src/lparse.ml - added argument reordering
- - - - - 8768911e by Pierre Delaunay at 2016-11-07T13:41:43-05:00 Merging
- - - - - 735256f3 by Stefan Monnier at 2016-11-07T15:04:27-05:00 Merge branch 'trunk' into unification
- - - - -
7 changed files:
- btl/types.typer - src/builtin.ml - src/eval.ml - src/lexp.ml - src/lparse.ml - tests/eval_test.ml - tests/macro_test.ml
Changes:
===================================== btl/types.typer ===================================== --- a/btl/types.typer +++ b/btl/types.typer @@ -176,7 +176,7 @@ read = Built-in "read" (FileHandle -> Int -> IO String); Attribute = Built-in "Attribute"; new-attribute = Built-in "new-attribute" (Macro);
-add-attribute = Built-in "add-attribute" (Macro); +add-attribute = Built-in "add-attribute" (List Sexp -> Sexp); attribute = Macro_ add-attribute;
get-attribute = Built-in "get-attribute" Macro;
===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -201,7 +201,8 @@ let declexpr_impl loc largs ctx ftype = let lxp = match env_lookup_expr ctx ((loc, vn), vi) with | Some lxp -> lxp | None -> error loc "no expr available" in - let ltp = env_lookup_type ctx ((loc, vn), vi) in (* FIXME: Unused? *) + (* ltp and ftype should be the same + let ltp = env_lookup_type ctx ((loc, vn), vi) in *) lxp, ftype
===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -92,9 +92,10 @@ let debug_messages error_type loc message messages = error_type loc (msg ^ "\n")
let root_string () = - match !_global_eval_trace with - | [], _ -> "" - | e::_, _ -> OL.pol_string e + let a, _ = !_global_eval_trace in + match List.rev a with + | [] -> "" + | e::_ -> OL.pol_string e
let debug_message error_type type_name type_string loc expr message = debug_messages error_type loc
===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -267,6 +267,7 @@ let lexp_name e = | Case _ -> "case" | Inductive _ -> "inductive_" | Builtin _ -> "Builtin" + | Susp _ -> "Susp" | _ -> "lexp_to_string: not implemented"
(*
===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -622,13 +622,15 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = | [] -> largs, ltp | (Node (Symbol (_, "_:=_"), [Symbol (_, aname); sarg])) :: sargs (* Explicit-implicit argument. *) + (* check if a = b in (a : Type) -> ... and (b := val) *) -> (match OL.lexp_whnf ltp (ectx_to_lctx ctx) meta_ctx with | Arrow (ak, Some (_, aname'), arg_type, _, ret_type) - when aname = aname' + when (aname = aname' || aname = "_") -> let parg = pexp_parse sarg in let larg = lexp_check parg arg_type ctx in handle_fun_args ((ak, larg) :: largs) sargs (L.mkSusp ret_type (S.substitute larg)) + | _ -> fatal (sexp_location sarg) ("Explicit-implicit arg `" ^ aname ^ "` to non-function " ^ "(type = " ^ (lexp_string ltp) ^ ")")) @@ -675,12 +677,82 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i =
| e -> (* Process Arguments *) - let largs, ret_type = try handle_fun_args [] sargs ltp - with Internal_error m -> print_string ( ( lexp_string e ) ^ "---\n" ); - List.iter (fun s -> Sexp.sexp_print s; print_newline () ) sargs; - print_endline (">>>" ^ lexp_string ltp); - raise (Internal_error m) - in + + (* Extract correct ordering *) + let rec extract_order ltp aargs eargs = + match nosusp ltp with + | Arrow (kind, Some (_, varname), ltp, _, ret) -> + extract_order ret ((kind, varname, ltp)::aargs) + (if kind = Aexplicit then (varname::eargs) else eargs) + + | _ -> (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 + + (* 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 + + 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 + (SMap.add aname (kind, Some sarg) map), + (if kind = Aexplicit then + (match eargs with + | _::tl -> tl + | _ -> []) else eargs) + + | _ -> (match eargs with + | name::tl -> (SMap.add name (Aexplicit, Some sexp) map), tl + | _ -> 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) -> + try match SMap.find name args_dict with + | Aimplicit, (Some sexp) -> Node (Symbol (dloc, "_:=_"), [Symbol (dloc, name); sexp]) + | Aerasable, Some sexp -> Node (Symbol (dloc, "_:=_"), [Symbol (dloc, name); sexp]) + | Aexplicit, (Some sexp) -> sexp + | Aexplicit, None -> fatal dloc "Explicit argument expected" + | Aimplicit, None -> ( + (* get variable info *) + let vidx, vname = match ltp with + | Var ((_, name), idx) -> idx, name + | _ -> lexp_fatal loc ltp "Unable to find default attribute" in + + (* get default property *) + let pidx, pname = (senv_lookup "default" ctx), "default" in + + (* get macro *) + let default_macro = try get_property ctx (vidx, vname) (pidx, pname) + with _ -> dump_properties ctx; dltype in + + lexp_print default_macro; + + print_string ((lexp_name ltp) ^ ": "); + lexp_print ltp; print_string "\n"; + fatal dloc "Default Arg lookup not implemented") + + + with Not_found -> fatal dloc (name ^ " not found") + ) order in + + (* + print_string "\nSarg2: "; List.iter (fun lxp -> sexp_print lxp; print_string ", ") sargs2; + print_string "\n"; *) + + (* check if we had enough information to reorder args *) + let sargs = if (List.length order >= List.length sargs) then sargs2 else sargs in + + let largs, ret_type = handle_fun_args [] sargs ltp in mkCall (body, List.rev largs), ret_type in
let handle_macro_call () =
===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -87,7 +87,8 @@ let _ = test_eval_eqv_named
"c = 3; e = 1; f = 2; d = 4;"
- "let TrueProp = inductive_ TrueProp I; I = inductive-cons TrueProp I; + "let TrueProp = inductive_ TrueProp I; + I = inductive-cons TrueProp I; x = let a = 1; b = 2 in I in (case x | I => c) : Int;" (* == *) "3"
@@ -96,8 +97,10 @@ let _ = test_eval_eqv_named
"c = 3; e = 1; f = 2; d = 4;"
- "let TrueProp : Type; I : TrueProp; - TrueProp = inductive_ TrueProp I; I = inductive-cons TrueProp I; + "let TrueProp : Type; + I : TrueProp; + TrueProp = inductive_ TrueProp I; + I = inductive-cons TrueProp I; x = let a = 1; b = 2 in I in (case x | I => c) : Int;" (* == *) "3"
@@ -317,6 +320,38 @@ let _ = (add_test "EVAL" "Monads" (fun () -> | _ -> failure () ))
+let _ = test_eval_eqv_named + "Argument Reordering" + + "fun = lambda (x : Int) => + lambda (y : Int) -> + lambda (z : Int) -> x * y + z;" + + "fun (x := 3) 2 1; + fun 2 1 (x := 3); + fun (z := 3) (y := 2) (x := 1); + fun (z := 1) (y := 2) (x := 3); + fun (x := 3) (y := 2) (z := 1);" + + "7; 7; 5; 7; 7" + + +let _ = test_eval_eqv_named + "Implicit Arguments" + + "default = new-attribute (List Sexp -> Sexp); + attribute Int default (lambda (lst : List Sexp) -> integer_ 1); + + fun = lambda (x : Int) => + lambda (y : Int) -> + lambda (z : Int) -> x * y + z;" + + "fun 2 1; + fun (z := 1) (y := 2)" + + "3; 3" + + (* run all tests *) let _ = run_all ()
===================================== tests/macro_test.ml ===================================== --- a/tests/macro_test.ml +++ b/tests/macro_test.ml @@ -47,8 +47,12 @@ let _ = (add_test "MACROS" "macros base" (fun () -> (* define 'lambda x -> x * x' using macros *) let dcode = " my_fun = lambda (x : List Sexp) -> - let hd = head(a := Sexp) x in - (node_ (symbol_ "_*_") (cons(a := Sexp) hd (cons(a := Sexp) hd (nil(a := Sexp))))); + let hd = case x + | cons hd tl => hd + | nil => symbol_ "x" in + (node_ (symbol_ "_*_") + (cons (a := Sexp) hd + (cons (a := Sexp) hd (nil (a := Sexp)))));
sqr = Macro_ my_fun; " in
View it on GitLab: https://gitlab.com/monnier/typer/compare/989e999bad50f35b7e2402064dbe6d5a34e...
Afficher les réponses par date