BONNEVALLE Vincent pushed to branch unification at Stefan / Typer

Commits: 2f8bf17e by n3f4s at 2016-06-30T16:01:58+02:00 improved debug printing

- - - - - 156353fa by n3f4s at 2016-06-30T16:03:49+02:00 zip returns option for error handling & refactor

zip return an option for the case when the two list don't have the same size (-> error), and the empty list case (-> not an error)

extract some function for readability

- - - - - 817f5f19 by n3f4s at 2016-06-30T16:06:20+02:00 add debug printing, correct _unify_inner, add test

_unify_inner returns a substitution if it receive an empty list

change one of the case test to have more difference between the two case

- - - - -

3 changed files:

- src/debug_fun.ml - src/unification.ml - tests/unify_test.ml

Changes:

===================================== src/debug_fun.ml ===================================== --- a/src/debug_fun.ml +++ b/src/debug_fun.ml @@ -1,13 +1,16 @@

open Fmt_lexp

-let _debug = true +let _debug = false

let indent = ref 0

let do_debug func = if _debug then (func ()) else ()

+let debug_print str = + do_debug (fun () -> print_string str; print_newline (); ()) + let clear_indent () = do_debug (fun () -> indent := 0; ())

@@ -20,7 +23,6 @@ let debug_print_lexp lxp =

let debug_print_unify fn lhs rhs str = let debug_print_unify fn lhs rhs str = - print_newline (); print_string (padding_left fn 10 ' '); print_string " : "; print_string (String.make (!indent * 4) '-'); @@ -29,4 +31,5 @@ let debug_print_unify fn lhs rhs str = debug_print_lexp rhs; print_string str; indent := !indent + 1; + print_newline (); in do_debug (fun () -> debug_print_unify fn lhs rhs str; ())

===================================== src/unification.ml ===================================== --- a/src/unification.ml +++ b/src/unification.ml @@ -2,8 +2,6 @@ open Lexp open Sexp

-open Debug_fun - module VMap = Map.Make (struct type t = int let compare = compare end)

type substitution = lexp VMap.t @@ -11,15 +9,15 @@ type constraints = (lexp * lexp) list

(* IMPROVEMENT For error handling : can carry location and name of type error *) (*type 'a result =*) - (*| Some of 'a*) - (*| Error of Util.location * string (*location * type name*)*) - (*| Nil*) +(*| Some of 'a*) +(*| Error of Util.location * string (*location * type name*)*) +(*| Nil*)

(*let result_to_option (e: 'a result) : ('a option) =*) - (*match e with*) - (*| Some elt -> Some elt*) - (*| Error _ -> None*) - (*| Nil -> None*) +(*match e with*) +(*| Some elt -> Some elt*) +(*| Error _ -> None*) +(*| Nil -> None*)

let global_last_metavar = ref 0 let create_metavar = global_last_metavar := !global_last_metavar + 1; !global_last_metavar @@ -45,20 +43,15 @@ let find_or_none (value: lexp) (map: substitution) : lexp option = let empty_subst = (VMap.empty)

(* Zip while applying a function, returns empty list if l1 & l2 have different size*) -let zip_map (l1: 'a list ) (l2: 'b list ) (f: ('a -> 'b -> 'c)): 'c list= +let zip_map (l1: 'a list ) (l2: 'b list ) (f: ('a -> 'b -> 'c)): 'c list option = let rec zip_ ll1 ll2 f = match ll1, ll2 with - | (h1::t1, h2::t2) -> (match zip_ t1 t2 f with - | None -> None - | Some t -> Some ((f h1 h2)::t)) - | ([], []) -> Some [] - | ([], _) -> None - | (_, []) -> None - in match zip_ l1 l2 f with - | None -> [] - | Some l -> l + | (h1::t1, h2::t2) -> (f h1 h2)::(zip_ t1 t2 f) + | ([], []) -> [] + | _, _ -> [] + in if List.length l1 = List.length l2 then Some (zip_ l1 l2 f) else None

-let zip (l1: 'a list) (l2: 'b list): (('a * 'b) list) = zip_map l1 l2 (fun x z -> (x, z)) +let zip (l1: 'a list) (l2: 'b list): (('a * 'b) list option) = zip_map l1 l2 (fun x z -> (x, z))

let zip_fold list1 list2 f = let l1 = List.fold_right (f) list1 [] @@ -79,10 +72,8 @@ let zip_fold list1 list2 f = * If (_unify_X X Y) don't handle the case (X, Y), it call (unify Y X) * 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 = - debug_print_unify "unify" l r ""; - match (l, r) with + let tmp = match (l, r) with | (_, Metavar _) -> _unify_metavar r l subst | (_, Call _) -> _unify_call r l subst | (_, Case _) -> _unify_case r l subst @@ -103,6 +94,9 @@ let rec unify (l: lexp) (r: lexp) (subst: substitution) : return_type = | (Sort _, _) -> _unify_sort l r subst | (SortLevel _, _) -> _unify_sortlvl l r subst (* | (_, _) -> None*) + in match tmp with + | Some _ -> Debug_fun.debug_print_unify "unify" l r " -> unification success"; tmp + | None -> Debug_fun.debug_print_unify "unify" l r " -> unification failed"; tmp

(********************************* Type specific unify *******************************)

@@ -157,16 +151,15 @@ and _unify_builtin (bltin: lexp) (lxp: lexp) (subst: substitution) : return_type * Let , lexp -> constraint *) and _unify_let (let_: lexp) (lxp: lexp) (subst: substitution) : return_type = - debug_print_unify "_unify_let" let_ lxp ""; match (let_, lxp) with | (Let (_, m, lxp_), Let (_, m1, lxp2)) -> let f = (fun (_, lxp, lt) acc -> lxp::lt::acc) - in let tail = zip_fold m m1 f - in (match tail with - | [] -> debug_print_unify "_unify_let" let_ lxp " -> No unification"; None - | _ -> _unify_inner ((lxp_, lxp2)::(tail)) subst ) - | (Let _, _) -> debug_print_unify "_unify_let" let_ lxp " -> Constraint"; Some (subst, [(let_, lxp)]) - | _, _ -> debug_print_unify "_unify_let" let_ lxp " -> No unification"; None + in (match zip_fold m m1 f with + | Some [] -> Some (subst, []) (* ??? *) + | None -> None + | Some tail -> _unify_inner ((lxp_, lxp2)::(tail)) 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 FIXME : shift indexes @@ -252,8 +245,9 @@ and _unify_call (call: lexp) (lxp: lexp) (subst: substitution) : return_type = let f = (fun (_, x) acc -> x::acc) in let tail = zip_fold lxp_list1 lxp_list2 f in (match tail with - | [] -> None - | _ -> _unify_inner ((lxp1, lxp2)::(tail)) subst) + | Some [] -> Some (subst, []) + | None -> None + | Some tail -> _unify_inner ((lxp1, lxp2)::(tail)) subst) | (Call _, _) -> Some ((subst, [(call, lxp)])) | (_, _) -> None

@@ -269,7 +263,7 @@ and _unify_susp (susp_: lexp) (lxp: lexp) (subst: substitution) : return_type = * Case, _ -> Constraint *) and _unify_case (case: lexp) (lxp: lexp) (subst: substitution) : return_type = - match case, lxp with + let tmp = match case, lxp with | (Case (_, lxp, lt11, lt12, smap, lxpopt), Case (_, lxp2, lt21, lt22, smap2, lxopt2)) -> ( match lxpopt, lxopt2 with | Some l1, Some l2 -> (match _unify_inner ((lxp, lxp2)::(lt11, lt21)::(lt12, lt22)::(l1, l2)::[]) subst with @@ -280,6 +274,9 @@ and _unify_case (case: lexp) (lxp: lexp) (subst: substitution) : return_type = | _, _ -> None) | (Case _, _) -> Some (subst, [(case, lxp)]) | (_, _) -> None + in match tmp with + | Some _ -> Debug_fun.debug_print_unify "_unify_case" case lxp " -> unification success"; tmp + | None -> Debug_fun.debug_print_unify "_unify_case" case lxp " -> unification failed"; tmp

(** Unify a Inductive and a lexp * Inductive, Inductive -> try unify @@ -289,13 +286,20 @@ and _unify_case (case: lexp) (lxp: lexp) (subst: substitution) : return_type = *) 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)) - in match (induct, lxp) with + and merge m1 m2 (s, c) : return_type = match (_unify_induct_sub_list (SMap.bindings m1) (SMap.bindings m2) s) with + | Some (s', c') -> Some (s', c@c') + | None -> None + in + let zip_unify lst subst m1 m2 : return_type = match _unify_inner_induct lst subst with + | None -> None + | Some (s, c) -> merge m1 m2 (s, c) + in + match (induct, lxp) with | (Inductive (_, lbl1, farg1, m1), Inductive (_, lbl2, farg2, m2)) when lbl1 = lbl2 -> - (match _unify_inner_induct (zip_map farg1 farg2 transform) subst with - | None -> None - | Some (s, c) -> (match (_unify_induct_sub_list (SMap.bindings m1) (SMap.bindings m2) s) with - | Some (s', c') -> Some (s', c@c') - | None -> None)) + (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

@@ -333,8 +337,8 @@ and _unify_sort (sort_: lexp) (lxp: lexp) (subst: substitution) : return_type = and is_same arglist arglist2 = match arglist, arglist2 with | (akind, _)::t1, (akind2, _)::t2 when akind = akind2 -> is_same t1 t2 - | [], [] -> true - | _, _ -> false + | [], [] -> Debug_fun.debug_print "is_same -> unification success"; true + | _, _ -> Debug_fun.debug_print "is_same -> unification failed"; false

(** try to unify the SMap part of the case *) and _unify_inner_case l s = @@ -343,21 +347,22 @@ and _unify_inner_case l s = | ((key, (_, arglist, lxp)), (key2, (_, arglist2, lxp2)))::tail when key = key2 -> (if is_same arglist arglist2 then ( match unify lxp lxp2 s with | Some (s', c) -> (match _unify_inner_case tail s' with - | Some (s_, c_) -> Some (s_, c@c_) - | None -> None) - | None -> None) + | Some (s_, c_) -> Debug_fun.debug_print "_unify_inner_case -> unification success"; Some (s_, c@c_) + | None -> Debug_fun.debug_print "_unify_inner_case -> unification failed"; None) + | None -> Debug_fun.debug_print "_unify_inner_case -> unification failed"; None) else None) - | [] -> Some (s, []) - | _ -> None + | [] -> Debug_fun.debug_print "_unify_inner_lxp -> unification success"; Some (s, []) + | _ -> Debug_fun.debug_print "_unify_inner_case -> unification failed"; None in (match l with - | [] -> None - | _ -> _unify_inner_case l s) + | Some [] -> Some (s, []) + | None -> None + | Some l -> _unify_inner_case l s)

(***** 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 + 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 @@ -369,12 +374,21 @@ and _unify_inner_induct lst subst : return_type =

(** unify the SMap of list in Inductive *) and _unify_induct_sub_list l1 l2 subst = - let test l1 l2 subst = match l1, l2 with - | (k1, v1)::t1, (k2, v2)::t2 when k1 = k2 -> (match _unify_inner_induct (zip v1 v2) subst with - | Some (s, c) -> (match (_unify_induct_sub_list t1 t2 s) with - | Some (s1, c1) -> Some (s1, c1@c) - | None -> Some (s, c)) - | None -> (_unify_induct_sub_list t1 t2 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

@@ -389,12 +403,13 @@ 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) - | Some (s_,c_) -> Some (s_, c@c_) + (*| None -> Some (s, c)*) + | None -> Debug_fun.debug_print "_unify_inner.merge -> unification failed"; None + | Some (s_,c_) -> Debug_fun.debug_print "_unify_inner.merge -> unification success"; Some (s_, c@c_) in match lxp_l with | (lxp1, lxp2)::tail -> ( match unify lxp1 lxp2 subst with | Some (s, c) -> merge (s, c) tail - | None -> None) - | [] -> None + | None -> Debug_fun.debug_print "_unify_inner -> unification failed"; None) + | [] -> Debug_fun.debug_print "_unify_inner -> unification failed : list empty"; Some (subst, [])

===================================== tests/unify_test.ml ===================================== --- a/tests/unify_test.ml +++ b/tests/unify_test.ml @@ -68,7 +68,6 @@ let str_case = "i = case 0 | _ => 5" let str_case2 = "i = case 0 | 0 => 12 -| 1 => 12 | _ => 12" let str_let = "i = let a = 5 in a + 1"

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