Stefan pushed to branch unification at Stefan / Typer
Commits: 36b070f5 by Stefan Monnier at 2016-11-06T11:18:40-05:00 * src/lparse.ml (_lexp_p_check): Check inferred type with conv_p
* btl/types.typer (head): Make it total. (tail): Fix up minor type error.
* src/lexp.ml (lexp_unparse): Print `Sort` with more details.
* src/lparse.ml (_lexp_p_check): Check inferred type with conv_p.
* tests/eval_test.ml (Lists): Adjust to new `head` type. (Monads): Fix type arguments.
- - - - - 989e999b by Stefan Monnier at 2016-11-07T14:28:18-05:00 Merge branch 'trunk' into unification
- - - - -
7 changed files:
- btl/types.typer - src/inverse_subst.ml - 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 @@ -78,18 +78,23 @@ length = lambda a ≡> | nil => 0 | cons hd tl => (1 + (length (a := a) tl));
-head : (a : Type) ≡> List a -> a; +% ML's typical `head` function is not total, so can't be defined +% as-is in Typer. There are several workarounds: +% - Provide a default value : (a : Type) ≡> List a -> a -> a; +% - Disallow problem case : (a : Type) ≡> (l : List a) -> (l != nil) -> a; +% - Return an Option/Error. +head : (a : Type) ≡> List a -> Option a; head = lambda a ≡> lambda xs -> case xs - | nil => nil - | cons hd tl => hd; + | nil => None (a := a) + | cons hd tl => Some (a := a) hd;
tail : (a : Type) ≡> List a -> List a; tail = lambda a ≡> lambda xs -> case xs - | nil => nil + | nil => nil (a := a) | cons hd tl => tl;
===================================== src/inverse_subst.ml ===================================== --- a/src/inverse_subst.ml +++ b/src/inverse_subst.ml @@ -1,3 +1,23 @@ +(* inverse_subst.ml --- Computing the inverse of a substitution + +Copyright (C) 2016 Free Software Foundation, Inc. + +Author: Vincent Bonnevalle tiv.crb@gmail.com + +This file is part of Typer. + +Typer is free software; you can redistribute it and/or modify it under the +terms of the GNU General Public License as published by the Free Software +Foundation, either version 3 of the License, or (at your option) any +later version. + +Typer is distributed in the hope that it will be useful, but WITHOUT ANY +WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS +FOR A PARTICULAR PURPOSE. See the GNU General Public License for +more details. + +You should have received a copy of the GNU General Public License along with +this program. If not, see http://www.gnu.org/licenses/. *)
open Lexp open Util
===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -409,8 +409,6 @@ let rec lexp_unparse lxp = | None -> pbranch in Pcase (loc, lexp_unparse target, pbranch)
- (* | _ as e -> Pimm (Symbol(lexp_location e, "<")) *) - (* FIXME: The cases below are all broken! *) | Metavar (idx, subst, (loc, name), _) -> Pimm (Symbol (loc, "?<" ^ name ^ "-" ^ string_of_int idx ^ ">"))
===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -412,7 +412,7 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : elab_context) trace: lexp = elab_check_sort ctx lasort (Some var) laty; laty in let arrow = mkArrow (kind, None, arg, Util.dummy_location, body) in - match Unif.unify arrow lxp subst with + match Unif.unify arrow lxp (ectx_to_lctx ctx) subst with | Some subst -> global_substitution := subst; arg, body | None -> lexp_error tloc lxp ("Type " ^ lexp_string lxp ^ " and " @@ -453,24 +453,14 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : elab_context) trace: lexp =
and lexp_p_infer_and_check pexp ctx t i = let (e, inferred_t) = _lexp_p_infer pexp ctx i in - (match e with - (* Built-in is a dummy function with no type. We cannot check - * Built-in *) - | Builtin _ -> () - | _ -> - let subst, _ = !global_substitution in - match Unif.unify inferred_t t subst with - | Some subst -> global_substitution := subst - | None - -> debug_msg ( - Debug_fun.do_debug (fun () -> - prerr_endline ("0 pxp " ^ pexp_string pexp); - ()); - print_string "1 exp "; lexp_print e; print_string "\n"; - print_string "2 inf "; lexp_print inferred_t; print_string "\n"; - print_string "3 ann "; lexp_print t; print_string "\n"; - lexp_warning (pexp_location pexp) e - "Type Mismatch inferred != Annotation")); + let subst, _ = !global_substitution in + (match Unif.unify inferred_t t (ectx_to_lctx ctx) subst with + | Some subst -> global_substitution := subst + | None + -> lexp_error (pexp_location pexp) e + ("Type mismatch! Context expected `" + ^ lexp_string t ^ "` but expression has type `" + ^ lexp_string inferred_t ^ "`\n")); e
(* Lexp.case can sometimes be inferred, but we prefer to always check. *)
===================================== src/unification.ml ===================================== --- a/src/unification.ml +++ b/src/unification.ml @@ -1,8 +1,29 @@ +(* unification.ml --- Unification of Lexp terms
-open Lexp -open Sexp -open Inverse_subst +Copyright (C) 2016 Free Software Foundation, Inc. + +Author: Vincent Bonnevalle tiv.crb@gmail.com + +This file is part of Typer. + +Typer is free software; you can redistribute it and/or modify it under the +terms of the GNU General Public License as published by the Free Software +Foundation, either version 3 of the License, or (at your option) any +later version. + +Typer is distributed in the hope that it will be useful, but WITHOUT ANY +WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS +FOR A PARTICULAR PURPOSE. See the GNU General Public License for +more details.
+You should have received a copy of the GNU General Public License along with +this program. If not, see http://www.gnu.org/licenses/. *) + +open Lexp +(* open Sexp *) +(* open Inverse_subst *) +module OL = Opslexp +module DB = Debruijn
(** Provide unify function for unifying two Lambda-Expression *)
@@ -58,6 +79,13 @@ let zip_fold list1 list2 f = CONSTRAINT -> returns a constraint *)
+let unify_and res op = match res with + | None -> None + | Some (subst, constraints1) + -> match op subst with + | None -> None + | Some (subst, constraints2) -> Some (subst, constraints2@constraints1) + (****************************** Top level unify *************************************)
(** Dispatch to the right unifyer. @@ -66,104 +94,40 @@ let zip_fold list1 list2 f =
The metavar unifyer is the end rule, it can't call unify with it's parameter (changing their order) *) -let rec unify (l: lexp) (r: lexp) (subst: substitution) : return_type = - let l, r = (nosusp l, nosusp r) in - match (l, r) with - | (_, Metavar _) -> _unify_metavar r l subst - | (_, Call _) -> _unify_call r l subst - | (_, Case _) -> _unify_case r l subst - | (_, Susp _) -> assert false - | (_, Let _) -> _unify_let r l subst - | (Imm _, _) -> _unify_imm l r subst - | (Cons _, _) -> _unify_cons l r subst - | (Builtin _, _) -> _unify_builtin l r subst - | (Let _, _) -> _unify_let l r subst - | (Var _, _) -> _unify_var l r subst - | (Arrow _, _) -> _unify_arrow l r subst - | (Lambda _, _) -> _unify_lambda l r subst - | (Metavar _, _) -> _unify_metavar l r subst - | (Call _, _) -> _unify_call l r subst - | (Susp _, _) -> assert false - | (Case _, _) -> _unify_case l r subst - | (Inductive _, _) -> _unfiy_induct l r subst - | (Sort _, _) -> _unify_sort l r subst - | (SortLevel _, _) -> _unify_sortlvl l r subst +let rec unify (e1: lexp) (e2: lexp) + (ctx : DB.lexp_context) (subst: substitution) + : 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) + : return_type = + let e1' = OL.lexp_whnf e1 ctx subst in + let e2' = OL.lexp_whnf e2 ctx subst in + let stop1 = not (e1 == e1') && OL.set_member_p vs e1' in + let stop2 = not (e2 == e2') && OL.set_member_p vs e2' in + let vs' = if not (e1 == e1') && not stop1 then OL.set_add vs e1' + else if not (e2 == e2') && not stop2 then OL.set_add vs e2' + else vs in + match if stop1 || stop2 then (e1, e2) else (e1', e2') with + | ((Imm _, Imm _) | (Cons _, Cons _) | (Builtin _, Builtin _) + | (Var _, Var _) | (Inductive _, Inductive _)) + -> if OL.conv_p subst ctx e1' e2' then Some (subst, []) else None + | (l, (Metavar _ as r)) -> _unify_metavar r l subst + | (l, (Call _ as r)) -> _unify_call r l ctx vs subst + (* | (l, (Case _ as r)) -> _unify_case r l subst *) + | (Arrow _ as l, r) -> _unify_arrow l r ctx vs subst + | (Lambda _ as l, r) -> _unify_lambda l r ctx vs subst + | (Metavar _ as l, r) -> _unify_metavar l r subst + | (Call _ as l, r) -> _unify_call l r ctx vs subst + (* | (Case _ as l, r) -> _unify_case l r subst *) + (* | (Inductive _ as l, r) -> _unify_induct l r subst *) + | (Sort _ as l, r) -> _unify_sort l r ctx vs subst + | (SortLevel _ as l, r) -> _unify_sortlvl l r ctx vs subst + | _ -> Some (subst, [(e1, e2)])
(********************************* Type specific unify *******************************)
-(** Unify two Imm if they match <=> Same type and same value - - Add one of the Imm (the first arguement) to the substitution - - Imm, Imm -> if Imm =/= Imm then ERROR else OK - - Imm, lexp -> unify lexp Imm -*) -and _unify_imm (l: lexp) (r: lexp) (subst: substitution) : return_type = - match (l, r) with - | (Imm (String (_, v1)), Imm (String (_, v2))) - -> if v1 = v2 then Some ((subst, [])) - else None - | (Imm (Integer (_, v1)), Imm (Integer (_, v2))) - -> if v1 = v2 then Some ((subst, [])) - else None - | (Imm (Float (_, v1)), Imm (Float (_, v2))) - -> if v1 = v2 then Some ((subst, [])) - else None - | (Imm _, Imm _) -> None - | (Imm _, _) -> unify r l subst - -(** Unify a Cons and a lexp - - Cons, Cons -> if Cons ~= Cons then OK else ERROR - - Cons, _ -> ERROR -*) -and _unify_cons (cons: lexp) (lxp: lexp) (subst: substitution) : return_type = - match (cons, lxp) with - | (Cons (it1, (_, name)), - Cons (it2, (_, name2))) when name = name2 -> unify it1 it2 subst - | (_, _) -> None - -(** Unify a builtin (bltin) and a lexp (lxp) if it is possible - - If the two arguments are builtin, unify based on name - - If it's a Builtin and an other lexp, unify lexp part of Builtin with the lexp -*) -and _unify_builtin (bltin: lexp) (lxp: lexp) (subst: substitution) : return_type = - match (bltin, lxp) with - | (Builtin ((_, name1), _), Builtin ((_, name2),_)) - -> if name1 = name2 then Some ((subst, [])) - else None (* assuming that builtin have unique name *) - | (Builtin (_, lxp_bltin), _) -> unify lxp_bltin lxp subst - | (_, _) -> None - -(** Unify a Let (let_) and a lexp (lxp), if possible - - Let , Let -> check the 'inside' of the let - - Let , lexp -> constraint -*) -and _unify_let (let_: lexp) (lxp: lexp) (subst: substitution) : return_type = - let concat = (fun (_, lxp, lt) acc -> lxp::lt::acc) - in - let try_zip_fold body1 body2 func lxp_ lxp2 subst = - match zip_fold body1 body2 func with - | Some [] -> Some (subst, []) - | None -> None - | Some tail -> _unify_inner ((lxp_, lxp2)::(tail)) subst - in - match (let_, lxp) with - | (Let (_, m, lxp_), Let (_, m1, lxp2)) -> try_zip_fold m m1 concat lxp_ lxp2 subst - | (Let _, _) -> Some (subst, [(let_, lxp)]) - | _, _ -> None - -(** Unify a Var and a lexp, if possible - - (Var, Var) -> unify if they have the same debruijn index - - (Var, Metavar) -> unify_metavar Metavar var subst - - (Var _, _) -> unfiy lexp Var subst -*) -and _unify_var (var: lexp) (r: lexp) (subst: substitution) : return_type = - match (var, r) with - | (Var (_, idx1), Var (_, idx2)) - -> if idx1 = idx2 then Some ((subst, [])) - else None - | (Var _, Imm _) -> Some (subst, [(var, r)]) - | (Var _, _) -> unify r var subst (*returns to unify*) - | (_, _) -> None - (** Unify a Arrow and a lexp if possible - (Arrow, Arrow) -> if var_kind = var_kind then unify ltype & lexp (Arrow (var_kind, _, ltype, lexp)) @@ -171,16 +135,20 @@ and _unify_var (var: lexp) (r: lexp) (subst: substitution) : return_type = - (Arrow, Var) -> Constraint - (_, _) -> None *) -and _unify_arrow (arrow: lexp) (lxp: lexp) (subst: substitution) +and _unify_arrow (arrow: lexp) (lxp: lexp) ctx vs (subst: substitution) : return_type = match (arrow, lxp) with - | (Arrow (var_kind1, _, ltype1, _, lexp1), Arrow (var_kind2, _, ltype2, _, lexp2)) + | (Arrow (var_kind1, v1, ltype1, _, lexp1), + Arrow (var_kind2, _, ltype2, _, lexp2)) -> if var_kind1 = var_kind2 - then _unify_inner ((ltype1, ltype2)::(lexp1, lexp2)::[]) subst - else None + then unify_and (unify' ltype1 ltype2 ctx vs subst) + (unify' lexp1 lexp2 + (DB.lexp_ctx_cons ctx 0 v1 Variable ltype1) + (OL.set_shift vs)) + else None | (Arrow _, Imm _) -> None | (Arrow _, Var _) -> Some (subst, [(arrow, lxp)]) - | (Arrow _, _) -> unify lxp arrow subst + | (Arrow _, _) -> unify' lxp arrow ctx vs subst | (_, _) -> None
(** Unify a Lambda and a lexp if possible @@ -191,18 +159,22 @@ and _unify_arrow (arrow: lexp) (lxp: lexp) (subst: substitution) - Lambda , Let -> Constraint - Lambda , lexp -> unify lexp lambda subst *) -and _unify_lambda (lambda: lexp) (lxp: lexp) (subst: substitution) : return_type = +and _unify_lambda (lambda: lexp) (lxp: lexp) ctx vs (subst: substitution) : return_type = match (lambda, lxp) with - | (Lambda (var_kind1, _, ltype1, lexp1), Lambda (var_kind2, _, ltype2, lexp2)) + | (Lambda (var_kind1, v1, ltype1, lexp1), + Lambda (var_kind2, _, ltype2, lexp2)) -> if var_kind1 = var_kind2 - then _unify_inner ((ltype1, ltype2)::(lexp1, lexp2)::[]) subst - else None + then unify_and (unify' ltype1 ltype2 ctx vs subst) + (unify' lexp1 lexp2 + (DB.lexp_ctx_cons ctx 0 (Some v1) Variable ltype1) + (OL.set_shift vs)) + else None | (Lambda _, Var _) -> Some ((subst, [(lambda, lxp)])) | (Lambda _, Let _) -> Some ((subst, [(lambda, lxp)])) | (Lambda _, Arrow _) -> None | (Lambda _, Call _) -> Some ((subst, [(lambda, lxp)])) | (Lambda _, Imm _) -> None - | (Lambda _, _) -> unify lxp lambda subst + | (Lambda _, _) -> unify' lxp lambda ctx vs subst | (_, _) -> None
(** Unify a Metavar and a lexp if possible @@ -214,16 +186,17 @@ and _unify_lambda (lambda: lexp) (lxp: lexp) (subst: substitution) : return_type and _unify_metavar (meta: lexp) (lxp: lexp) (subst: substitution) : return_type = let find_or_unify metavar value lxp s = match find_or_none metavar s with - | Some (lxp_) -> unify lxp_ lxp s + | Some (lxp_) -> assert false | None -> (match metavar with - | Metavar (_, subst_, _, _) -> (match inverse subst_ with + | Metavar (_, subst_, _, _) -> (match Inverse_subst.inverse subst_ with | Some s' -> Some (associate value (mkSusp lxp s') s, []) | None -> None) | _ -> None) in match (meta, lxp) with - | (Metavar (val1, s1, _, _), Metavar (val2, s2, _, _)) when val1 = val2 -> - Some ((subst, [])) + | (Metavar (val1, s1, _, _), Metavar (val2, s2, _, _)) when val1 = val2 + (* FIXME: handle the case where s1 != s2 !! *) + -> Some ((subst, [])) | (Metavar (v, s1, _, _), _) -> find_or_unify meta v lxp subst | (_, _) -> None
@@ -231,15 +204,18 @@ and _unify_metavar (meta: lexp) (lxp: lexp) (subst: substitution) : return_type - Call , Call -> UNIFY - Call , lexp -> CONSTRAINT *) -and _unify_call (call: lexp) (lxp: lexp) (subst: substitution) : return_type = - let f = (fun (_, x) acc -> x::acc) - in let try_zip_fold lst1 lst2 lxp1 lxp2 subst = (match zip_fold lst1 lst2 f with - | Some [] -> Some (subst, []) - | None -> None - | Some tail -> _unify_inner ((lxp1, lxp2)::(tail)) subst) - in +and _unify_call (call: lexp) (lxp: lexp) ctx vs (subst: substitution) + : return_type = match (call, lxp) with - | (Call (lxp_left, lxp_list1), Call (lxp_right, lxp_list2)) -> try_zip_fold lxp_list1 lxp_list2 lxp_left lxp_right subst + | (Call (lxp_left, lxp_list1), Call (lxp_right, lxp_list2)) + when OL.conv_p subst ctx lxp_left lxp_right + -> List.fold_left (fun op ((ak1, e1), (ak2, e2)) subst + -> if ak1 == ak2 then + unify_and (unify' e1 e2 ctx vs subst) op + else None) + (fun subst -> Some (subst, [])) + (List.combine lxp_list1 lxp_list2) + subst | (Call _, _) -> Some ((subst, [(call, lxp)])) | (_, _) -> None
@@ -247,27 +223,27 @@ and _unify_call (call: lexp) (lxp: lexp) (subst: substitution) : return_type = - Case, Case -> try to unify - Case, _ -> Constraint *) -and _unify_case (case: lexp) (lxp: lexp) (subst: substitution) : return_type = - let merge (_, const) subst_res = match subst_res with - | None -> None - | Some (s', c') -> Some (s', const@c') - in - let match_unify_inner lst smap1 smap2 subst = - match _unify_inner lst subst with - | None -> None - | Some (s, c) -> merge (s, c) (_unify_inner_case (zip (SMap.bindings smap1) (SMap.bindings smap2)) s) - in - let match_lxp_opt lxp_opt1 lxp_opt2 tail smap1 smap2 subst = - match lxp_opt1, lxp_opt2 with - | Some (_, lxp1), Some (_, lxp2) - -> match_unify_inner ((lxp1, lxp2)::tail) smap1 smap2 subst - | _, _ -> None - in - match (case, lxp) with - | (Case (_, lxp, lt12, smap, lxpopt), Case (_, lxp2, lt22, smap2, lxopt2)) - -> match_lxp_opt lxpopt lxopt2 ((lt12, lt22)::[]) smap smap2 subst - | (Case _, _) -> Some (subst, [(case, lxp)]) - | (_, _) -> None +(* and _unify_case (case: lexp) (lxp: lexp) (subst: substitution) : return_type = + * let merge (_, const) subst_res = match subst_res with + * | None -> None + * | Some (s', c') -> Some (s', const@c') + * in + * let match_unify_inner lst smap1 smap2 subst = + * match _unify_inner lst subst with + * | None -> None + * | Some (s, c) -> merge (s, c) (_unify_inner_case (zip (SMap.bindings smap1) (SMap.bindings smap2)) s) + * in + * let match_lxp_opt lxp_opt1 lxp_opt2 tail smap1 smap2 subst = + * match lxp_opt1, lxp_opt2 with + * | Some (_, lxp1), Some (_, lxp2) + * -> match_unify_inner ((lxp1, lxp2)::tail) smap1 smap2 subst + * | _, _ -> None + * in + * match (case, lxp) with + * | (Case (_, lxp, lt12, smap, lxpopt), Case (_, lxp2, lt22, smap2, lxopt2)) + * -> match_lxp_opt lxpopt lxopt2 ((lt12, lt22)::[]) smap smap2 subst + * | (Case _, _) -> Some (subst, [(case, lxp)]) + * | (_, _) -> None *)
(** Unify a Inductive and a lexp - Inductive, Inductive -> try unify @@ -275,36 +251,36 @@ and _unify_case (case: lexp) (lxp: lexp) (subst: substitution) : return_type = - Inductive, Call/Metavar/Case/Let -> constraint - Inductive, _ -> None *) -and _unfiy_induct (induct: lexp) (lxp: lexp) (subst: substitution) : 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 - | Some (s', c') -> Some (s', const@c') - | None -> None - in - let zip_unify lst subst map1 map2 : return_type = - match _unify_inner_induct lst subst with - | None -> None - | Some (s, c) -> merge map1 map2 (s, c) - in - match (induct, lxp) with - | (Inductive (_, lbl1, farg1, m1), Inductive (_, lbl2, farg2, m2)) when lbl1 = lbl2 -> - (match zip_map farg1 farg2 transform with - | Some [] -> Some (subst, []) - | Some lst -> zip_unify lst subst m1 m2 - | None -> None) - | (Inductive _, Var _) -> Some (subst, [(induct, lxp)]) - | (_, _) -> None +(* and _unify_induct (induct: lexp) (lxp: lexp) (subst: substitution) : 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 + * | Some (s', c') -> Some (s', const@c') + * | None -> None + * in + * let zip_unify lst subst map1 map2 : return_type = + * match _unify_inner_induct lst subst with + * | None -> None + * | Some (s, c) -> merge map1 map2 (s, c) + * in + * match (induct, lxp) with + * | (Inductive (_, lbl1, farg1, m1), Inductive (_, lbl2, farg2, m2)) when lbl1 = lbl2 -> + * (match zip_map farg1 farg2 transform with + * | Some [] -> Some (subst, []) + * | Some lst -> zip_unify lst subst m1 m2 + * | None -> None) + * | (Inductive _, Var _) -> Some (subst, [(induct, lxp)]) + * | (_, _) -> None *)
(** Unify a SortLevel with a lexp - SortLevel, SortLevel -> if SortLevel ~= SortLevel then OK else ERROR - SortLevel, _ -> ERROR *) -and _unify_sortlvl (sortlvl: lexp) (lxp: lexp) (subst: substitution) : return_type = +and _unify_sortlvl (sortlvl: lexp) (lxp: lexp) ctx vs (subst: substitution) : return_type = match sortlvl, lxp with | (SortLevel s, SortLevel s2) -> (match s, s2 with | SLz, SLz -> Some (subst, []) - | SLsucc l1, SLsucc l2 -> unify l1 l2 subst + | SLsucc l1, SLsucc l2 -> unify' l1 l2 ctx vs subst | _, _ -> None) | _, _ -> None
@@ -313,10 +289,10 @@ and _unify_sortlvl (sortlvl: lexp) (lxp: lexp) (subst: substitution) : return_ty - Sort, Var -> Constraint - Sort, lexp -> ERROR *) -and _unify_sort (sort_: lexp) (lxp: lexp) (subst: substitution) : return_type = +and _unify_sort (sort_: lexp) (lxp: lexp) ctx vs (subst: substitution) : return_type = match sort_, lxp with | (Sort (_, srt), Sort (_, srt2)) -> (match srt, srt2 with - | Stype lxp1, Stype lxp2 -> unify lxp1 lxp2 subst + | Stype lxp1, Stype lxp2 -> unify' lxp1 lxp2 ctx vs subst | StypeOmega, StypeOmega -> Some (subst, []) | StypeLevel, StypeLevel -> Some (subst, []) | _, _ -> None) @@ -334,63 +310,63 @@ and is_same arglist arglist2 = | _, _ -> false
(** try to unify the SMap part of the case *) -and _unify_inner_case lst subst = - let merge (_, c) res = - match res with - | Some (s', c') -> Some (s', c@c') - | None -> None - in - let rec _unify_inner_case list_ subst = - match list_ with - | ((key, (_, arglist, lxp)), (key2, (_, arglist2, lxp2)))::tail when key = key2 -> - (if is_same arglist arglist2 - then ( match unify lxp lxp2 subst with - | Some (s', c) -> merge (s', c) (_unify_inner_case tail s') - | None -> None) - else None) - | [] -> Some (subst, []) - | _ -> None - in (match lst with - | Some [] -> Some (subst, []) - | None -> None - | Some l -> _unify_inner_case l subst) +(* and _unify_inner_case lst subst = + * let merge (_, c) res = + * match res with + * | Some (s', c') -> Some (s', c@c') + * | None -> None + * in + * let rec _unify_inner_case list_ subst = + * match list_ with + * | ((key, (_, arglist, lxp)), (key2, (_, arglist2, lxp2)))::tail when key = key2 -> + * (if is_same arglist arglist2 + * then ( match unify lxp lxp2 subst with + * | Some (s', c) -> merge (s', c) (_unify_inner_case tail s') + * | None -> None) + * else None) + * | [] -> Some (subst, []) + * | _ -> None + * in (match lst with + * | Some [] -> Some (subst, []) + * | None -> None + * | Some l -> _unify_inner_case l subst) *)
(***** for Inductive *****) (** for _unify_induct : unify the formal arg*) -and _unify_inner_induct lst subst : return_type = - let test ((a1, _, l1), (a2, _, l2)) subst : return_type = - if a1 = a2 then unify l1 l2 subst - else None - in - List.fold_left (fun a e -> - (match a with - | Some (s, c) -> - (match test e s with - | Some (s1, c1) -> Some (s1, c1@c) - | None -> Some (s, c)) - | None -> test e subst) - ) None lst +(* and _unify_inner_induct lst subst : return_type = + * let test ((a1, _, l1), (a2, _, l2)) subst : return_type = + * if a1 = a2 then unify l1 l2 subst + * else None + * in + * List.fold_left (fun a e -> + * (match a with + * | Some (s, c) -> + * (match test e s with + * | Some (s1, c1) -> Some (s1, c1@c) + * | None -> Some (s, c)) + * | None -> test e subst) + * ) None lst *)
(** unify the SMap of list in Inductive *) -and _unify_induct_sub_list l1 l2 subst = - let test l1 l2 subst = - let merge l1 l2 subst (s, c) = - match (_unify_induct_sub_list l1 l2 subst) with - | Some (s1, c1) -> Some (s1, c1@c) - | None -> Some (s, c) - in - let unify_zip lst t1 t2 = match _unify_inner_induct lst subst with - | Some (s, c) -> merge l1 l2 subst (s, c) - | None -> (_unify_induct_sub_list t1 t2 subst) - in - match l1, l2 with - | (k1, v1)::t1, (k2, v2)::t2 when k1 = k2 -> - (match zip v1 v2 with - | Some [] -> Some (subst, []) - | Some lst -> unify_zip lst t1 t2 - | None -> None) - | _, _ -> None - in test l1 l2 subst +(* and _unify_induct_sub_list l1 l2 subst = + * let test l1 l2 subst = + * let merge l1 l2 subst (s, c) = + * match (_unify_induct_sub_list l1 l2 subst) with + * | Some (s1, c1) -> Some (s1, c1@c) + * | None -> Some (s, c) + * in + * let unify_zip lst t1 t2 = match _unify_inner_induct lst subst with + * | Some (s, c) -> merge l1 l2 subst (s, c) + * | None -> (_unify_induct_sub_list t1 t2 subst) + * in + * match l1, l2 with + * | (k1, v1)::t1, (k2, v2)::t2 when k1 = k2 -> + * (match zip v1 v2 with + * | Some [] -> Some (subst, []) + * | Some lst -> unify_zip lst t1 t2 + * | None -> None) + * | _, _ -> None + * in test l1 l2 subst *)
(***** general *****)
@@ -399,24 +375,24 @@ and _unify_induct_sub_list l1 l2 subst = and zip them to [(ltype * ltype), (lexp * lexp), (ltype2 * ltype2), (lexp2 * lexp2), ...] *) -and _unify_inner (lxp_l: (lexp * lexp) list) (subst: substitution) : return_type = - let merge ((s, c): (substitution * constraints)) - (lxp_list: (lexp * lexp) list) : return_type = - match _unify_inner lxp_list s with - (*| None -> Some (s, c)*) - | None -> None - | Some (s_,c_) -> Some (s_, c@c_) - in - let tmp = match lxp_l with - | (lxp1, lxp2)::tail -> ( match unify lxp1 lxp2 subst with - | Some (s, c) -> merge (s, c) tail - | None -> None) - | [] -> Some (subst, []) - in match tmp with - | None -> ( match lxp_l with - | [] -> tmp - | (l1, l2)::_ -> tmp ) - | Some _ -> ( match lxp_l with - | [] -> tmp - | (l1, l2)::_ -> tmp ) +(* and _unify_inner (lxp_l: (lexp * lexp) list) ctx vs (subst: substitution) : return_type = + * let merge ((s, c): (substitution * constraints)) + * (lxp_list: (lexp * lexp) list) : return_type = + * match _unify_inner lxp_list ctx vs s with + * (*| None -> Some (s, c)*) + * | None -> None + * | Some (s_,c_) -> Some (s_, c@c_) + * in + * let tmp = match lxp_l with + * | (lxp1, lxp2)::tail -> ( match unify lxp1 lxp2 ctx vs subst with + * | Some (s, c) -> merge (s, c) tail + * | None -> None) + * | [] -> Some (subst, []) + * in match tmp with + * | None -> ( match lxp_l with + * | [] -> tmp + * | (l1, l2)::_ -> tmp ) + * | Some _ -> ( match lxp_l with + * | [] -> tmp + * | (l1, l2)::_ -> tmp ) *)
===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -256,7 +256,7 @@ let _ = test_eval_eqv_named head my_list; head (tail my_list)"
- "4; 1; 2" + "4; Some (a := Int) 1; Some (a := Int) 2"
(* * Special forms @@ -301,14 +301,14 @@ let _ = (add_test "EVAL" "Infinite Recursion failure" (fun () -> let _ = (add_test "EVAL" "Monads" (fun () ->
let dcode = " - c = bind (a := Type) (b := Type) (open "./_build/w_file.txt" "w") - (lambda (f : FileHandle) -> - write f "Hello2"); + c = bind (a := FileHandle) (b := Unit) + (open "./_build/w_file.txt" "w") + (lambda f -> 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 + let rcode = "run-io (a := Unit) (b := Int) c 2" in
(* Eval defined lambda *) let ret = eval_expr_str rcode lctx rctx in
===================================== tests/unify_test.ml ===================================== --- a/tests/unify_test.ml +++ b/tests/unify_test.ml @@ -171,7 +171,7 @@ let generate_testable (_: lexp list) : ((lexp * lexp * result) list) = ::[]
let test_input (lxp1: lexp) (lxp2: lexp) (subst: substitution): unif_res = - let res = unify lxp1 lxp2 subst in + 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 (_, []) -> (Unification, res, lxp1, lxp2)
View it on GitLab: https://gitlab.com/monnier/typer/compare/b6acb432f680c1d2a93e6447e0939affdc3...