Stefan pushed to branch master at Stefan / Typer

Commits: 86d4a83d by Stefan Monnier at 2020-03-21T18:02:02-04:00 * unification.ml: Return just a list rather than an list option

Additionally, keep track of the ctx and annotate whether there's a possibility unification could succeed at some other time.

* src/lexp.ml (constraints): Move to unification.ml

* src/unification.ml (constraint_kind): New type. (constraints): Rewrite. (unify_and): Remove, use `@` instead.

- - - - -

5 changed files:

- src/debruijn.ml - src/elab.ml - src/lexp.ml - src/unification.ml - tests/unify_test.ml

Changes:

===================================== src/debruijn.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2019 Free Software Foundation, Inc. + * Copyright (C) 2011-2020 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types.

===================================== src/elab.ml ===================================== @@ -550,7 +550,7 @@ and infer_type pexp ectx var = l))) s (ectx_to_lctx ectx) with - | (None | Some (_::_)) + | (_::_) -> (let lexp_string e = lexp_string (L.clean e) in let typestr = lexp_string t ^ " : " ^ lexp_string s in match var with @@ -560,7 +560,7 @@ and infer_type pexp ectx var = -> lexp_error l t ("Type of `" ^ name ^ "` is not a proper type: " ^ typestr)) - | Some [] -> ()); + | [] -> ()); t

and lexp_let_decls declss (body: lexp) ctx = @@ -576,18 +576,13 @@ and unify_with_arrow ctx tloc lxp kind var aty let (l, _) = var in let arrow = mkArrow (kind, var, arg, l, body) in match Unif.unify arrow lxp (ectx_to_lctx ctx) with - | None -> lexp_error tloc lxp ("Type " ^ lexp_string lxp - ^ " and " - ^ lexp_string arrow - ^ " does not match"); - (mkDummy_type ctx l, mkDummy_type nctx l) - | Some ((t1,t2)::_) + | ((_ck, _ctx, t1, t2)::_) -> lexp_error tloc lxp ("Types:\n " ^ lexp_string t1 ^ "\n and:\n " ^ lexp_string t2 ^ "\n do not match!"); (mkDummy_type ctx l, mkDummy_type nctx l) - | Some [] -> arg, body + | [] -> arg, body

and check (p : sexp) (t : ltype) (ctx : elab_context): lexp = let (e, ot) = elaborate ctx p (Some t) in @@ -607,17 +602,12 @@ and check_inferred ctx e inferred_t t = -> (e, inferred_t) | _ -> instantiate_implicit e inferred_t ctx in (match Unif.unify inferred_t t (ectx_to_lctx ctx) with - | None - -> lexp_error (lexp_location e) e - ("Type mismatch! Context expected `" - ^ lexp_string t ^ "` but expression has type `" - ^ lexp_string inferred_t ^ "`") - | Some ((t1,t2)::_) + | ((_ck, _ctx, t1, t2)::_) -> lexp_error (lexp_location e) e ("Type mismatch! Context expected `" ^ lexp_string t2 ^ "` but expression has type `" ^ lexp_string t1 ^ "`") - | Some [] -> ()); + | [] -> ()); e

(* Lexp.case can sometimes be inferred, but we prefer to always check. *) @@ -680,12 +670,12 @@ and check_case rtype (loc, target, ppatterns) ctx = match nosusp (inst_args ctx lctor) with | Cons (it', (_, cons_name)) -> let _ = match Unif.unify it' it (ectx_to_lctx ctx) with - | (None | Some (_::_)) + | (_::_) -> lexp_error loc lctor ("Expected pattern of type `" ^ lexp_string it ^ "` but got `" ^ lexp_string it' ^ "`") - | Some [] -> () in + | [] -> () in let _ = check_uniqueness pat cons_name lbranches in let cargs = try SMap.find cons_name constructors @@ -1073,12 +1063,12 @@ and lexp_decls_1 | _ -> Log.internal_error "Var not found at its index!" in (* Unify it with the new one. *) let _ = match Unif.unify ltp pt (ectx_to_lctx nctx) with - | (None | Some (_::_)) + | (_::_) -> lexp_error loc ltp ("New type annotation `" ^ lexp_string ltp ^ "` incompatible with previous `" ^ lexp_string pt ^ "`") - | Some [] -> () in + | [] -> () in lexp_decls_1 sdecls ectx nctx pending_decls pending_defs else if List.exists (fun ((_, vname'), _) -> vname = vname') pending_defs then

===================================== src/lexp.ml ===================================== @@ -155,7 +155,6 @@ type metavar_info = * so we just keep the length of the lexp_context. *) * ctx_length type meta_subst = metavar_info U.IMap.t -type constraints = (lexp * lexp) list

let dummy_scope_level = 0 let impossible = Imm Sexp.dummy_epsilon

===================================== src/unification.ml ===================================== @@ -40,7 +40,15 @@ let create_metavar (ctx : DB.lexp_context) (sl : scope_level) (t : ltype) idx

(* For convenience *) -type return_type = constraints option +type constraint_kind = + | CKimpossible (* Unification is simply impossible. *) + | CKresidual (* We failed to find a unifier. *) +(* FIXME: Each constraint should additionally come with a description of how + it relates to its "top-level" or some other info which might let us + fix the problem (e.g. by introducing coercions). *) +type constraints = (constraint_kind * DB.lexp_context * lexp * lexp) list + +type return_type = constraints

(** Alias for VMap.add*) let associate (id: meta_id) (lxp: lexp) (subst: meta_subst) : meta_subst @@ -103,21 +111,6 @@ let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with (metavar_table := old_mvt; true) else false

-(** - lexp is equivalent to _ in ocaml - (Let , lexp) == (lexp , Let) - UNIFY -> recursive call or dispatching - OK -> add a substituion to the list of substitution - CONSTRAINT -> returns a constraint -*) - -let unify_and res op = match res with - | None -> None - | Some constraints1 - -> match op with - | None -> None - | Some constraints2 -> Some (constraints2@constraints1) - (****************************** Top level unify *************************************)

(** Dispatch to the right unifier. @@ -134,17 +127,17 @@ let rec unify (e1: lexp) (e2: lexp) and unify' (e1: lexp) (e2: lexp) (ctx : DB.lexp_context) (vs : OL.set_plexp) : return_type = - if e1 == e2 then Some [] else + if e1 == e2 then [] else let e1' = OL.lexp_whnf e1 ctx in let e2' = OL.lexp_whnf e2 ctx in - if e1' == e2' then Some [] else + if e1' == e2' then [] else let changed = true (* not (e1 == e1' && e2 == e2') *) in - if changed && OL.set_member_p vs e1' e2' then Some [] else + if changed && OL.set_member_p vs e1' e2' then [] else let vs' = if changed then OL.set_add vs e1' e2' else vs in match (e1', e2') with | ((Imm _, Imm _) | (Cons _, Cons _) | (Builtin _, Builtin _) | (Var _, Var _)) - -> if OL.conv_p ctx e1' e2' then Some [] else None + -> if OL.conv_p ctx e1' e2' then [] else [(CKimpossible, ctx, e1, e2)] | (l, (Metavar (idx, s, _) as r)) -> unify_metavar ctx idx s r l | ((Metavar (idx, s, _) as l), r) -> unify_metavar ctx idx s l r | (l, (Call _ as r)) -> unify_call r l ctx vs' @@ -163,10 +156,10 @@ and unify' (e1: lexp) (e2: lexp) * ^ " and " * ^ snd label2 * ^ "\n"); *) - unify_inductive ctx vs' args1 args2 consts1 consts2 - | _ -> Some (if OL.conv_p ctx e1' e2' then [] - else ((* print_string "Unification failure on default\n"; *) - [(e1, e2)])) + unify_inductive ctx vs' args1 args2 consts1 consts2 e1 e2 + | _ -> (if OL.conv_p ctx e1' e2' then [] + else ((* print_string "Unification failure on default\n"; *) + [(CKresidual, ctx, e1, e2)]))

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

@@ -183,15 +176,15 @@ and unify_arrow (arrow: lexp) (lxp: lexp) ctx vs | (Arrow (var_kind1, v1, ltype1, _, lexp1), Arrow (var_kind2, _, ltype2, _, lexp2)) -> if var_kind1 = var_kind2 - then unify_and (unify' ltype1 ltype2 ctx vs) - (unify' lexp1 lexp2 - (DB.lexp_ctx_cons ctx v1 Variable ltype1) - (OL.set_shift vs)) - else None - | (Arrow _, Imm _) -> None - | (Arrow _, Var _) -> Some ([(arrow, lxp)]) + then (unify' ltype1 ltype2 ctx vs) + @(unify' lexp1 lexp2 + (DB.lexp_ctx_cons ctx v1 Variable ltype1) + (OL.set_shift vs)) + else [(CKimpossible, ctx, arrow, lxp)] + | (Arrow _, Imm _) -> [(CKimpossible, ctx, arrow, lxp)] + | (Arrow _, Var _) -> ([(CKresidual, ctx, arrow, lxp)]) | (Arrow _, _) -> unify' lxp arrow ctx vs - | (_, _) -> None + | (_, _) -> [(CKimpossible, ctx, arrow, lxp)]

(** Unify a Lambda and a lexp if possible - Lamda , Lambda -> if var_kind = var_kind @@ -206,18 +199,18 @@ and unify_lambda (lambda: lexp) (lxp: lexp) ctx vs : return_type = | (Lambda (var_kind1, v1, ltype1, lexp1), Lambda (var_kind2, _, ltype2, lexp2)) -> if var_kind1 = var_kind2 - then unify_and (unify' ltype1 ltype2 ctx vs) - (unify' lexp1 lexp2 - (DB.lexp_ctx_cons ctx v1 Variable ltype1) - (OL.set_shift vs)) - else None + then (unify' ltype1 ltype2 ctx vs) + @(unify' lexp1 lexp2 + (DB.lexp_ctx_cons ctx v1 Variable ltype1) + (OL.set_shift vs)) + else [(CKimpossible, ctx, lambda, lxp)] | ((Lambda _, Var _) | (Lambda _, Let _) - | (Lambda _, Call _)) -> Some [(lambda, lxp)] - | (Lambda _, Arrow _) -> None - | (Lambda _, Imm _) -> None + | (Lambda _, Call _)) -> [(CKresidual, ctx, lambda, lxp)] + | (Lambda _, Arrow _) + | (Lambda _, Imm _) -> [(CKimpossible, ctx, lambda, lxp)] | (Lambda _, _) -> unify' lxp lambda ctx vs - | (_, _) -> None + | (_, _) -> [(CKimpossible, ctx, lambda, lxp)]

(** Unify a Metavar and a lexp if possible - lexp , {metavar <-> none} -> UNIFY @@ -235,15 +228,15 @@ and unify_metavar ctx idx s (lxp1: lexp) (lxp2: lexp) match Inverse_subst.apply_inv_subst lxp s with | exception Inverse_subst.Not_invertible -> log_info ?loc:None ("Unification of metavar failed:\n " - ^ "?[" ^ subst_string s ^ "]" - ^ "\nAgainst:\n " - ^ lexp_string lxp ^ "\n"); - None - | lxp' when occurs_in idx lxp' -> None + ^ "?[" ^ subst_string s ^ "]" + ^ "\nAgainst:\n " + ^ lexp_string lxp ^ "\n"); + [(CKresidual, ctx, lxp1, lxp2)] + | lxp' when occurs_in idx lxp' -> [(CKimpossible, ctx, lxp1, lxp2)] | lxp' -> metavar_table := associate idx lxp' (!metavar_table); match unify t (OL.get_type ctx lxp) ctx with - | Some [] as r -> r + | [] as r -> r (* FIXME: Let's ignore the error for now. *) | _ -> log_info ?loc:None @@ -251,21 +244,18 @@ and unify_metavar ctx idx s (lxp1: lexp) (lxp2: lexp) ^ lexp_string (Lexp.clean t) ^ " != " ^ lexp_string (Lexp.clean (OL.get_type ctx lxp)) ^ "\n" ^ "for " ^ lexp_string lxp ^ "\n"); - Some [] in + [(CKresidual, ctx, lxp1, lxp2)] in match lxp2 with | Metavar (idx2, s2, _) -> if idx = idx2 then (* FIXME: handle the case where s1 != s2 !! *) - Some [] + [] else (* If one of the two subst can't be inverted, try the other. * FIXME: There's probably a more general solution. *) (match unif idx s lxp2 with - | Some s -> Some s - | None -> - match unif idx2 s2 lxp1 with - | Some s -> Some s - | None -> None) + | [] -> [] + | _ -> unif idx2 s2 lxp1) | _ -> unif idx s lxp2

(** Unify a Call (call) and a lexp (lxp) @@ -279,12 +269,11 @@ and unify_call (call: lexp) (lxp: lexp) ctx vs when OL.conv_p ctx lxp_left lxp_right -> List.fold_left (fun op ((ak1, e1), (ak2, e2)) -> if ak1 == ak2 then - unify_and (unify' e1 e2 ctx vs) op - else None) - (Some []) + (unify' e1 e2 ctx vs)@op + else [(CKimpossible, ctx, call, lxp)]) + [] (List.combine lxp_list1 lxp_list2) - | (Call _, _) -> Some [(call, lxp)] - | (_, _) -> None + | (_, _) -> [(CKresidual, ctx, call, lxp)]

(** Unify a Case with a lexp - Case, Case -> try to unify @@ -346,16 +335,14 @@ and unify_call (call: lexp) (lxp: lexp) ctx vs and unify_sortlvl (sortlvl: lexp) (lxp: lexp) ctx vs : return_type = match sortlvl, lxp with | (SortLevel s, SortLevel s2) -> (match s, s2 with - | SLz, SLz -> Some [] + | SLz, SLz -> [] | SLsucc l1, SLsucc l2 -> unify' l1 l2 ctx vs | SLlub (l11, l12), SLlub (l21, l22) -> (* FIXME: This SLlub representation needs to be * more "canonicalized" otherwise it's too restrictive! *) - (match (unify' l11 l21 ctx vs, unify' l12 l22 ctx vs) with - | (Some cs1, Some cs2) -> Some (cs1 @ cs2) - | _ -> None) - | _, _ -> None) - | _, _ -> None + (unify' l11 l21 ctx vs)@(unify' l12 l22 ctx vs) + | _, _ -> [(CKimpossible, ctx, sortlvl, lxp)]) + | _, _ -> [(CKresidual, ctx, sortlvl, lxp)]

(** Unify a Sort and a lexp - Sort, Sort -> if Sort ~= Sort then OK else ERROR @@ -366,11 +353,11 @@ and unify_sort (sort_: lexp) (lxp: lexp) ctx vs : return_type = match sort_, lxp with | (Sort (_, srt), Sort (_, srt2)) -> (match srt, srt2 with | Stype lxp1, Stype lxp2 -> unify' lxp1 lxp2 ctx vs - | StypeOmega, StypeOmega -> Some [] - | StypeLevel, StypeLevel -> Some [] - | _, _ -> None) - | Sort _, Var _ -> Some [(sort_, lxp)] - | _, _ -> None + | StypeOmega, StypeOmega -> [] + | StypeLevel, StypeLevel -> [] + | _, _ -> [(CKimpossible, ctx, sort_, lxp)]) + | Sort _, Var _ -> [(CKresidual, ctx, sort_, lxp)] + | _, _ -> [(CKimpossible, ctx, sort_, lxp)]

(************************ Helper function **************************************)

@@ -420,24 +407,28 @@ and is_same arglist arglist2 = * | None -> test e subst) * ) None lst *)

-and unify_inductive ctx vs args1 args2 consts1 consts2 = +and unify_inductive ctx vs args1 args2 consts1 consts2 e1 e2 = let unif_formals ctx vs args1 args2 - = if not (List.length args1 == List.length args2) then (ctx, vs, None) else + = if not (List.length args1 == List.length args2) then + (ctx, vs, [(CKimpossible, ctx, e1, e2)]) + else List.fold_left (fun (ctx, vs, residue) ((ak1, v1, t1), (ak2, v2, t2)) -> (DB.lexp_ctx_cons ctx v1 Variable t1, OL.set_shift vs, - if not (ak1 == ak2) then None - else unify_and (unify' t1 t2 ctx vs) residue)) - (ctx, vs, Some []) + if not (ak1 == ak2) then [(CKimpossible, ctx, e1, e2)] + else (unify' t1 t2 ctx vs) @ residue)) + (ctx, vs, []) (List.combine args1 args2) in let (ctx, vs, residue) = unif_formals ctx vs args1 args2 in - if not (SMap.cardinal consts1 == SMap.cardinal consts2) then None else + if not (SMap.cardinal consts1 == SMap.cardinal consts2) then + [(CKimpossible, ctx, e1, e2)] + else SMap.fold (fun cname args1 residue -> match SMap.find cname consts2 with | args2 -> let (_ctx, _vs, residue') = unif_formals ctx vs args1 args2 in - unify_and residue' residue - | exception Not_found -> None) + residue' @ residue + | exception Not_found -> [(CKimpossible, ctx, e1, e2)]) consts1 residue

(** unify the SMap of list in Inductive *)

===================================== tests/unify_test.ml ===================================== @@ -1,6 +1,6 @@ (* unify_test.ml --- Test the unification algorithm * - * Copyright (C) 2016-2019 Free Software Foundation, Inc. + * Copyright (C) 2016-2020 Free Software Foundation, Inc. * * Author: Vincent Bonnevalle tiv.crb@gmail.com * @@ -43,7 +43,7 @@ type result = | Equivalent | Nothing

-type unif_res = (result * (constraints) option * lexp * lexp) +type unif_res = (result * (constraints) * lexp * lexp)

type triplet = string * string * string

@@ -192,13 +192,13 @@ let test_input (lxp1: lexp) (lxp2: lexp): unif_res = let orig_subst = !metavar_table in let res = unify lxp1 lxp2 Myers.nil in match res with - | Some [] + | [] -> let new_subst = !metavar_table in if orig_subst == new_subst then (Equivalent, res, lxp1, lxp2) else (Unification, res, lxp1, lxp2) - | Some _ -> (Constraint, res, lxp1, lxp2) - | None -> (Nothing, res, lxp1, lxp2) + | (CKresidual, _, _, _)::_ -> (Constraint, res, lxp1, lxp2) + | (CKimpossible, _, _, _)::_ -> (Nothing, res, lxp1, lxp2)

let check (lxp1: lexp) (lxp2: lexp) (res: result): bool = let r, _, _, _ = test_input lxp1 lxp2

View it on GitLab: https://gitlab.com/monnier/typer/-/commit/86d4a83db13b23cac91152ae7bff6858d7...