| C.Meta (i, l), t -> (
try
let _, _, ty = CicUtil.lookup_meta i menv in
- assert (not (Subst.is_in_subst i subst));
let subst = Subst.buildsubst i context t ty subst in
- let menv = menv in (* List.filter (fun (m, _, _) -> i <> m) menv in *)
subst, menv
with CicUtil.Meta_not_found m ->
let names = names_of_context context in
let profiler3 = HExtlib.profile "P/Inference.unif_simple[resolve_meta]"
let profiler4 = HExtlib.profile "P/Inference.unif_simple[filter]"
+let check_for_duplicates metas msg =
+ let rec aux = function
+ | [] -> true
+ | (m,_,_)::tl ->
+ not (List.exists (fun (i, _, _) -> i = m) tl) && aux tl in
+ let b = aux metas in
+ if not b then
+ begin
+ prerr_endline ("DUPLICATI ---- " ^ msg);
+ prerr_endline (CicMetaSubst.ppmetasenv [] metas);
+ assert false
+ end
+ else b
+;;
+
+let check_metasenv msg menv =
+ List.iter
+ (fun (i,ctx,ty) ->
+ try ignore(CicTypeChecker.type_of_aux' menv ctx ty
+ CicUniv.empty_ugraph)
+ with
+ | CicUtil.Meta_not_found _ ->
+ prerr_endline (msg ^ CicMetaSubst.ppmetasenv [] menv);
+ assert false
+ | _ -> ()
+ ) menv
+;;
+
let unification_aux b metasenv1 metasenv2 context t1 t2 ugraph =
- let metasenv =
- HExtlib.list_uniq (List.sort Pervasives.compare (metasenv1 @ metasenv2))
- (* metasenv1 @ metasenv2 *)
- in
+ let metasenv = metasenv1@metasenv2 in
+ if Utils.debug_metas then
+ begin
+ ignore(check_for_duplicates metasenv "unification_aux");
+ check_metasenv "unification_aux" metasenv;
+ end;
let subst, menv, ug =
if not (is_simple_term t1) || not (is_simple_term t2) then (
debug_print
in
let flatten subst = profiler.HExtlib.profile flatten subst in
let subst = flatten subst in *)
- subst, menv, ug
+ if Utils.debug_metas then
+ ignore(check_for_duplicates menv "unification_aux prima di apply_subst");
+ let menv = Subst.apply_subst_metasenv subst menv in
+ if Utils.debug_metas then
+ (let _ = check_for_duplicates menv "unif_aux after" in
+ check_metasenv "unification_aux after 1" menv);
+ subst, menv, ug
;;
exception MatchingFailure;;
;;
let unification m1 m2 c t1 t2 ug =
+ let m1 =
+ if (m1 = m2 && m1 <> []) then assert false
+ (* (prerr_endline "eccoci 2"; []) *) else m1 in
+ (*
+ prerr_endline (CicPp.ppterm t1);
+ prerr_endline (CicPp.ppterm t2);
+ prerr_endline "++++++++++"; *)
try
unification_aux true m1 m2 c t1 t2 ug
with exn ->