Stefan pushed to branch unification at Stefan / Typer
Commits: e0c03878 by Stefan Monnier at 2016-11-08T23:07:54-05:00 Make explicit args reordering work
* btl/types.typer (run-io): Make first operation of type Unit.
* src/lexp.ml (meta_subst): Rename from substitution. (empty_meta_subst): Rename from empty_meta_subst.
* src/lparse.ml (_lexp_p_infer): Un-comment out the Plambda case. (lexp_call): Improve handle_fun_args for re-ordering of explicit args.
- - - - -
6 changed files:
- btl/types.typer - src/lexp.ml - src/lparse.ml - src/unification.ml - tests/eval_test.ml - tests/unify_test.ml
Changes:
===================================== btl/types.typer ===================================== --- a/btl/types.typer +++ b/btl/types.typer @@ -155,24 +155,15 @@ bind = Built-in "bind" ( % define a dummy type that supposed to represent a file FileHandle = Built-in "FileHandle";
-% define operation on file handle -%% runIO should have type IO Unit -> b -> b +%% `runIO` should have type IO Unit -> b -> b %% or IO a -> b -> b, which means "run the IO, throw away the result, %% and then return the second argument unchanged". The "dummy" b argument %% is actually crucial to make sure the result of runIO is used, otherwise %% the whole call would look like a dead function call and could be %% optimized away! -run-io = Built-in "run-io" ( - %% FIXME: runIO should have type IO Unit -> b -> b - %% or IO a -> b -> b, which means "run the IO, throw away the result, - %% and then return the second argument unchanged". The "dummy" b argument - %% is actually crucial to make sure the result of runIO is used, otherwise - %% the whole call would look like a dead function call and could be - %% optimized away! - (a : Type) ≡> - (b : Type) ≡> - IO a -> b -> b); +run-io = Built-in "run-io" ((a : Type) ≡> IO Unit -> a -> a);
+% Define operations on file handle. open = Built-in "open" (String -> String -> IO FileHandle); write = Built-in "write" (FileHandle -> String -> IO Unit); read = Built-in "read" (FileHandle -> Int -> IO String);
===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -76,7 +76,7 @@ type ltype = lexp * ltype (* The type of the return value of all branches *) * (U.location * (arg_kind * vdef option) list * lexp) SMap.t * (vdef option * lexp) option (* Default. *) - (* The substitution `s` only applies to the lexp associated + (* The `subst` only applies to the lexp associated * with the metavar's index (i.e. its "value"), not to the ltype. *) | Metavar of int * subst * vdef * ltype (* (* For logical metavars, there's no substitution. *) @@ -118,9 +118,9 @@ type varbind = | LetDef of lexp
module VMap = Map.Make (struct type t = int let compare = compare end) -type substitution = lexp VMap.t +type meta_subst = lexp VMap.t type constraints = (lexp * lexp) list -let empty_subst = (VMap.empty) +let empty_meta_subst = VMap.empty
let builtin_size = ref 0
@@ -422,13 +422,13 @@ let rec lexp_unparse lxp = | Sort (l, Stype sl) -> Pcall (Pimm (Symbol (l, "<Type>")), [pexp_unparse (lexp_unparse sl)])
+(* FIXME: ¡Unify lexp_print and lexp_string! *) +let lexp_string lxp = sexp_string (pexp_unparse (lexp_unparse lxp)) + let rec subst_string s = match s with | S.Identity -> "Id" | S.Shift (s, n) -> "(" ^ subst_string s ^ "↑" ^ string_of_int n ^ ")" | S.Cons (l, s) -> lexp_string l ^ " · " ^ subst_string s - -(* FIXME: ¡Unify lexp_print and lexp_string! *) -and lexp_string lxp = sexp_string (pexp_unparse (lexp_unparse lxp)) (* * Printing * --------------------- *)
===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -93,7 +93,7 @@ let pexp_error = debug_message error pexp_name pexp_string let value_fatal = debug_message fatal value_name value_string
(* :-( *) -let global_substitution = ref (empty_subst, []) +let global_substitution = ref (empty_meta_subst, [])
let elab_check_sort (ctx : elab_context) lsort var ltp = let meta_ctx, _ = !global_substitution in @@ -289,19 +289,16 @@ let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype = let v = mkInductive(tloc, label, formal, map_ctor) in v, ltp
- (* This case can be inferred *) - (* | Plambda (kind, var, optype, body) - * -> let ltp, _ = match optype with - * | Some ptype -> lexp_infer ptype ctx - * (* This case must have been lexp_p_check *) - * | None -> pexp_error tloc p "Lambda require type annotation"; - * dltype, dltype in - * - * let nctx = env_extend ctx var Variable ltp in - * let lbody, lbtp = lexp_infer body nctx in - * - * let lambda_type = mkArrow(kind, Some var, ltp, tloc, lbtp) in - * mkLambda(kind, var, ltp, lbody), lambda_type *) + (* This case can be inferred. *) + | Plambda (kind, var, Some ptype, body) + -> let ltp, lasort = lexp_infer ptype ctx in + elab_check_sort ctx lasort (Some var) ltp; + + let nctx = env_extend ctx var Variable ltp in + let lbody, lbtp = lexp_infer body nctx 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
@@ -373,8 +370,7 @@ and lexp_let_decls declss (body: lexp) ctx i = and _lexp_p_check (p : pexp) (t : ltype) (ctx : elab_context) trace: lexp =
let trace = ((OL.Pexp p)::trace) in - let tloc = pexp_location p - in + let tloc = pexp_location p in let lexp_infer p ctx = _lexp_p_infer p ctx trace in let lexp_check p ltp ctx = _lexp_p_check p ltp ctx trace in
@@ -594,41 +590,65 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = let body, ltp = lexp_infer func ctx in let ltp = nosusp ltp in
- let rec handle_fun_args largs sargs ltp = - match sargs with - | [] -> largs, ltp - | (Node (Symbol (_, "_:=_"), [Symbol (_, aname); sarg])) :: sargs + let rec handle_fun_args largs sargs pending ltp = + let ltp' = OL.lexp_whnf ltp (ectx_to_lctx ctx) meta_ctx in + match sargs, ltp' with + | _, Arrow (ak, Some (_, aname'), arg_type, _, ret_type) + when SMap.mem aname' pending + -> let sarg = SMap.find aname' pending in + let parg = pexp_parse sarg in + let larg = lexp_check parg arg_type ctx in + handle_fun_args ((ak, larg) :: largs) sargs + (SMap.remove aname' pending) + (L.mkSusp ret_type (S.substitute larg)) + + | [], _ + -> (if not (SMap.is_empty pending) then + let pending = SMap.bindings pending in + let loc = match pending with (_, sarg)::_ -> sexp_location sarg in + pexp_error loc func + ("Explicit actual args `" + ^ String.concat ", " (List.map (fun (l, _) -> l) + pending) + ^ "` have no matching formal args")); + largs, ltp + + | (Node (Symbol (_, "_:=_"), [Symbol (_, aname); sarg])) :: sargs, + Arrow (ak, Some (_, aname'), arg_type, _, ret_type) + when (aname = aname' || aname = "_") (* 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' || 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) ^ ")")) - | sarg :: sargs - (* Process Argument *) - -> (match OL.lexp_whnf ltp (ectx_to_lctx ctx) meta_ctx with - | Arrow (Aexplicit, _, arg_type, _, ret_type) - -> let parg = pexp_parse sarg in - let larg = _lexp_p_check parg arg_type ctx i in - handle_fun_args ((Aexplicit, larg) :: largs) sargs - (L.mkSusp ret_type (S.substitute larg)) - | Arrow (kind, _, arg_type, _, ret_type) - -> let larg = newMetavar arg_type in - handle_fun_args ((kind, larg) :: largs) (sarg::sargs) - (L.mkSusp ret_type (S.substitute larg)) - - | t -> - print_lexp_ctx (ectx_to_lctx ctx); - lexp_fatal (sexp_location sarg) t - ("Explicit arg `" ^ sexp_string sarg ^ - "` to non-function (type = " ^ lexp_string ltp ^ ")")) in + -> let parg = pexp_parse sarg in + let larg = lexp_check parg arg_type ctx in + handle_fun_args ((ak, larg) :: largs) sargs pending + (L.mkSusp ret_type (S.substitute larg)) + + | (Node (Symbol (_, "_:=_"), [Symbol (l, aname); sarg])) :: sargs, + Arrow _ + -> if SMap.mem aname pending then + sexp_error l ("Duplicate explicit arg `" ^ aname ^ "`"); + handle_fun_args largs sargs (SMap.add aname sarg pending) ltp + + | (Node (Symbol (_, "_:=_"), Symbol (l, aname) :: _)) :: sargs, _ + -> sexp_error l + ("Explicit arg `" ^ aname ^ "` to non-function " + ^ "(type = " ^ (lexp_string ltp) ^ ")"); + handle_fun_args largs sargs pending ltp + + | sarg :: sargs, Arrow (Aexplicit, _, arg_type, _, ret_type) + -> let parg = pexp_parse sarg in + let larg = _lexp_p_check parg arg_type ctx i in + handle_fun_args ((Aexplicit, larg) :: largs) sargs pending + (L.mkSusp ret_type (S.substitute larg)) + | sarg :: sargs, Arrow (kind, _, arg_type, _, ret_type) + -> let larg = newMetavar arg_type in + handle_fun_args ((kind, larg) :: largs) (sarg::sargs) pending + (L.mkSusp ret_type (S.substitute larg)) + + | sarg :: sargs, t -> + print_lexp_ctx (ectx_to_lctx ctx); + lexp_fatal (sexp_location sarg) t + ("Explicit arg `" ^ sexp_string sarg ^ + "` to non-function (type = " ^ lexp_string ltp ^ ")") in
let handle_funcall () = (* Here we use lexp_whnf on actual code, but it's OK @@ -654,89 +674,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i =
| e -> (* Process Arguments. *) - - (* Extract correct ordering aargs: all args and eargs: explicit args. *) - let meta_ctx, _ = !global_substitution in - let rec extract_order ltp aargs eargs nctx = - match OL.lexp_whnf ltp nctx meta_ctx with - | Arrow (kind, Some (_, varname), ltp, _, ret) -> - extract_order ret ((kind, varname, ltp)::aargs) - (if kind = Aexplicit then (varname::eargs) else eargs) (lctx_extend nctx None (ForwardRef) ltp) - - | 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 [] [] (ectx_to_lctx ctx) 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 - - let args_dict, eargs = List.fold_left (fun (map, eargs) sexp -> - match sexp with - | Node (Symbol (_, "_:=_"), [Symbol (_, aname); sarg]) -> - 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 - | _::tl -> tl - | _ -> []) else eargs) - - | _ -> (match eargs with - | name::tl -> (SMap.add name (Aexplicit, Some sexp) map), tl - | _ -> map, [])) - (args_dict, eorder) sargs in - - - (* 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 | Aerasable), 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 + let largs, ret_type = handle_fun_args [] sargs SMap.empty ltp in mkCall (body, List.rev largs), ret_type in
let handle_macro_call () =
===================================== src/unification.ml ===================================== --- a/src/unification.ml +++ b/src/unification.ml @@ -40,17 +40,17 @@ let create_metavar () = global_last_metavar := !global_last_metavar + 1; !global_last_metavar
(* For convenience *) -type return_type = (substitution * constraints) option +type return_type = (meta_subst * constraints) option
(** Alias for VMap.add*) -let associate (meta: int) (lxp: lexp) (subst: substitution) - : substitution = +let associate (meta: int) (lxp: lexp) (subst: meta_subst) + : meta_subst = (VMap.add meta lxp subst)
(** If key is in map returns the value associated else returns <code>None</code> *) -let find_or_none (value: lexp) (map: substitution) : lexp option = +let find_or_none (value: lexp) (map: meta_subst) : lexp option = match value with | Metavar (idx, _, _, _) -> if VMap.mem idx map @@ -82,12 +82,12 @@ let unify_and res op = match res with The metavar unifyer is the end rule, it can't call unify with it's parameter (changing their order) *) let rec unify (e1: lexp) (e2: lexp) - (ctx : DB.lexp_context) (subst: substitution) + (ctx : DB.lexp_context) (subst: meta_subst) : return_type = unify' e1 e2 ctx OL.set_empty subst
and unify' (e1: lexp) (e2: lexp) - (ctx : DB.lexp_context) (vs : OL.set_lexp) (subst: substitution) + (ctx : DB.lexp_context) (vs : OL.set_lexp) (subst: meta_subst) : return_type = let e1' = OL.lexp_whnf e1 ctx subst in let e2' = OL.lexp_whnf e2 ctx subst in @@ -123,7 +123,7 @@ and unify' (e1: lexp) (e2: lexp) - (Arrow, Var) -> Constraint - (_, _) -> None *) -and _unify_arrow (arrow: lexp) (lxp: lexp) ctx vs (subst: substitution) +and _unify_arrow (arrow: lexp) (lxp: lexp) ctx vs (subst: meta_subst) : return_type = match (arrow, lxp) with | (Arrow (var_kind1, v1, ltype1, _, lexp1), @@ -147,7 +147,7 @@ and _unify_arrow (arrow: lexp) (lxp: lexp) ctx vs (subst: substitution) - Lambda , Let -> Constraint - Lambda , lexp -> unify lexp lambda subst *) -and _unify_lambda (lambda: lexp) (lxp: lexp) ctx vs (subst: substitution) : return_type = +and _unify_lambda (lambda: lexp) (lxp: lexp) ctx vs (subst: meta_subst) : return_type = match (lambda, lxp) with | (Lambda (var_kind1, v1, ltype1, lexp1), Lambda (var_kind2, _, ltype2, lexp2)) @@ -171,7 +171,7 @@ and _unify_lambda (lambda: lexp) (lxp: lexp) ctx vs (subst: substitution) : retu - metavar , metavar -> if Metavar = Metavar then OK else ERROR - metavar , lexp -> OK *) -and _unify_metavar (meta: lexp) (lxp: lexp) (subst: substitution) : return_type = +and _unify_metavar (meta: lexp) (lxp: lexp) (subst: meta_subst) : return_type = let find_or_unify metavar value lxp s = match find_or_none metavar s with | Some (lxp_) -> assert false @@ -192,7 +192,7 @@ and _unify_metavar (meta: lexp) (lxp: lexp) (subst: substitution) : return_type - Call , Call -> UNIFY - Call , lexp -> CONSTRAINT *) -and _unify_call (call: lexp) (lxp: lexp) ctx vs (subst: substitution) +and _unify_call (call: lexp) (lxp: lexp) ctx vs (subst: meta_subst) : return_type = match (call, lxp) with | (Call (lxp_left, lxp_list1), Call (lxp_right, lxp_list2)) @@ -211,7 +211,7 @@ and _unify_call (call: lexp) (lxp: lexp) ctx vs (subst: substitution) - Case, Case -> try to unify - Case, _ -> Constraint *) -(* and _unify_case (case: lexp) (lxp: lexp) (subst: substitution) : return_type = +(* and _unify_case (case: lexp) (lxp: lexp) (subst: meta_subst) : return_type = * let merge (_, const) subst_res = match subst_res with * | None -> None * | Some (s', c') -> Some (s', const@c') @@ -239,7 +239,7 @@ and _unify_call (call: lexp) (lxp: lexp) ctx vs (subst: substitution) - Inductive, Call/Metavar/Case/Let -> constraint - Inductive, _ -> None *) -(* and _unify_induct (induct: lexp) (lxp: lexp) (subst: substitution) : return_type = +(* and _unify_induct (induct: lexp) (lxp: lexp) (subst: meta_subst) : return_type = * let transform (a, b, c) (d, e, f) = ((a, Some b, c), (d, Some e, f)) * and merge map1 map2 (subst, const) : return_type = * match (_unify_induct_sub_list (SMap.bindings map1) (SMap.bindings map2) subst) with @@ -264,7 +264,7 @@ and _unify_call (call: lexp) (lxp: lexp) ctx vs (subst: substitution) - SortLevel, SortLevel -> if SortLevel ~= SortLevel then OK else ERROR - SortLevel, _ -> ERROR *) -and _unify_sortlvl (sortlvl: lexp) (lxp: lexp) ctx vs (subst: substitution) : return_type = +and _unify_sortlvl (sortlvl: lexp) (lxp: lexp) ctx vs (subst: meta_subst) : return_type = match sortlvl, lxp with | (SortLevel s, SortLevel s2) -> (match s, s2 with | SLz, SLz -> Some (subst, []) @@ -277,7 +277,7 @@ and _unify_sortlvl (sortlvl: lexp) (lxp: lexp) ctx vs (subst: substitution) : re - Sort, Var -> Constraint - Sort, lexp -> ERROR *) -and _unify_sort (sort_: lexp) (lxp: lexp) ctx vs (subst: substitution) : return_type = +and _unify_sort (sort_: lexp) (lxp: lexp) ctx vs (subst: meta_subst) : return_type = match sort_, lxp with | (Sort (_, srt), Sort (_, srt2)) -> (match srt, srt2 with | Stype lxp1, Stype lxp2 -> unify' lxp1 lxp2 ctx vs subst
===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -248,18 +248,16 @@ let _ = test_eval_eqv_named let _ = test_eval_eqv_named "Lists"
- (* FIXME: This doesn't signal an error, even we don't yet have the code - * to handle the `nil` below! *) "my_list = cons 1 (cons 2 (cons 3 - (cons 4 nil)))" + (cons 4 (nil (a := Int)))))"
"length my_list; head my_list; head (tail my_list)"
- "4; Some (a := Int) 1; Some (a := Int) 2" + "4; Some 1; Some 2"
(* * Special forms @@ -311,7 +309,7 @@ let _ = (add_test "EVAL" "Monads" (fun () ->
let rctx, lctx = eval_decl_str dcode lctx rctx in
- let rcode = "run-io (a := Unit) (b := Int) c 2" in + let rcode = "run-io c 2" in
(* Eval defined lambda *) let ret = eval_expr_str rcode lctx rctx in @@ -328,12 +326,11 @@ let _ = test_eval_eqv_named 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" + "7; 5; 7; 7"
let _ = test_eval_eqv_named
===================================== tests/unify_test.ml ===================================== --- a/tests/unify_test.ml +++ b/tests/unify_test.ml @@ -23,7 +23,7 @@ type result = | Equivalent | Nothing
-type unif_res = (result * (substitution * constraints) option * lexp * lexp) +type unif_res = (result * (meta_subst * constraints) option * lexp * lexp)
type triplet = string * string * string
@@ -168,29 +168,29 @@ let generate_testable (_: lexp list) : ((lexp * lexp * result) list) =
::[]
-let test_input (lxp1: lexp) (lxp2: lexp) (subst: substitution): unif_res = +let test_input (lxp1: lexp) (lxp2: lexp) (subst: meta_subst): unif_res = let res = unify lxp1 lxp2 Myers.nil subst in let tmp = match res with - | Some (s, []) when s = empty_subst -> (Equivalent, res, lxp1, lxp2) + | Some (s, []) when s = empty_meta_subst -> (Equivalent, res, lxp1, lxp2) | Some (_, []) -> (Unification, res, lxp1, lxp2) | Some _ -> (Constraint, res, lxp1, lxp2) | None -> (Nothing, res, lxp1, lxp2) in tmp
-let check (lxp1: lexp) (lxp2: lexp) (res: result) (subst: substitution): bool = +let check (lxp1: lexp) (lxp2: lexp) (res: result) (subst: meta_subst): bool = let r, _, _, _ = test_input lxp1 lxp2 subst in if r = res then true else false
let test_if (input: lexp list) sample_generator checker : bool = let rec test_if_ samples checker = match samples with - | (l1, l2, res)::t -> if checker l1 l2 res empty_subst then test_if_ t checker else false + | (l1, l2, res)::t -> if checker l1 l2 res empty_meta_subst then test_if_ t checker else false | [] -> true in test_if_ (sample_generator input) checker
let unifications = List.map (fun (l1, l2, res) -> - let r, _, _, _ = test_input l1 l2 empty_subst + let r, _, _, _ = test_input l1 l2 empty_meta_subst in (l1, l2, res, r)) (generate_testable [])
View it on GitLab: https://gitlab.com/monnier/typer/commit/e0c03878fe8afce8c23a23d7023d3c98c61c...
Afficher les réponses par date