wip

Author: gares

plugins/ssrmatching/ssrmatching.ml

@@ -214,37 +214,58 @@ let flags_FO env =
     Unification.resolve_evars =
       (Unification.default_no_delta_unify_flags ts).Unification.resolve_evars
   }
-
 let unif_FO env ise metas p c = Unification.w_unify ~metas env ise Conversion.CONV ~flags:(flags_FO env) p c
 
+type hd_comparison = CompareArgs of Impargs.implicit_status list | CanonicalInfRequired | Different
+
 let same_hd ise p c =
   match EConstr.kind ise p, EConstr.kind ise c with
   | Const(c1,_), Const(c2,_) when Constant.CanOrd.equal c1 c2 ->
-      Some (Impargs.implicits_of_global (GlobRef.ConstRef c1) |> List.hd |> snd)
-  | _ -> None
+    CompareArgs (Impargs.implicits_of_global (GlobRef.ConstRef c1) |> List.hd |> snd)
+  | Ind(c1,_), Ind(c2,_) when Ind.CanOrd.equal c1 c2 ->
+    CompareArgs (Impargs.implicits_of_global (GlobRef.IndRef c1) |> List.hd |> snd)
+  | Construct(c1,_), Construct(c2,_) when Construct.CanOrd.equal c1 c2 ->
+    CompareArgs (Impargs.implicits_of_global (GlobRef.ConstructRef c1) |> List.hd |> snd)
+  | Const(c1,_), _ when Structures.Structure.is_projection c1 -> CanonicalInfRequired
+  | _ -> Different
 
 let rec unif_FO_skip_impl env ise metas p c =
   match EConstr.kind ise p, EConstr.kind ise c with
+  | Meta _, _ -> metas, ise
+  | App(hd,_), _ when EConstr.isMeta ise hd -> metas, ise
   | App(hd1,args1), App(hd2,args2) ->
     begin match same_hd ise hd1 hd2 with
-    | None -> unif_FO env ise metas p c
-    | Some imp -> unif_FO_skip_impl3 env ise metas (Array.to_list args1) (Array.to_list args2) imp
+    | CanonicalInfRequired -> raise (CErrors.user_err Pp.(mt ()))
+      (* pp(lazy(str"ho "));
+      metas, unif_HO env ise p c *)
+    | Different -> raise (CErrors.user_err Pp.(mt ()))
+    | CompareArgs imp -> unif_FO_skip_impl3 env ise metas (Array.to_list args1) (Array.to_list args2) imp
     end
   | _ -> unif_FO env ise metas p c
 and unif_FO_skip_impl3 env ise metas args1 args2 imp =
   match args1, args2, imp with
-  | _::args1, _::args2, Some _ :: imp -> unif_FO_skip_impl3 env ise metas args1 args2 imp
+  | a1::args1, a2::args2, Some _ :: imp ->
+    pp(lazy(str"skip " ++ pr_econstr_env env ise a1 ++ str " = " ++ pr_econstr_env env ise a2));
+    unif_FO_skip_impl3 env ise metas args1 args2 imp
   | a1::args1, a2::args2, None :: imp ->
+  pp(lazy(str"do " ++ pr_econstr_env env ise a1 ++ str " = " ++ pr_econstr_env env ise a2));
+
       let metas, ise = unif_FO_skip_impl env ise metas a1 a2 in
       unif_FO_skip_impl3 env ise metas args1 args2 imp
   | a1::args1, a2::args2, [] ->
-    let metas, ise = unif_FO_skip_impl env ise metas a1 a2 in
+  pp(lazy(str"do " ++ pr_econstr_env env ise a1 ++ str " = " ++ pr_econstr_env env ise a2));
+  let metas, ise = unif_FO_skip_impl env ise metas a1 a2 in
     unif_FO_skip_impl3 env ise metas args1 args2 []
-  | [], [], _ -> metas, ise
-  | _ -> raise (CErrors.user_err Pp.(mt ()))
+  | [], [], _ ->
+    pp(lazy(str"good"));
+        metas, ise
+  | _ ->
+    pp(lazy(str"bad"));
+        raise (CErrors.user_err Pp.(mt ()))
 
 let unif_FO env ise metas p c =
   let metas = Unification.Metamap.fold (fun mv t accu -> Unification.Meta.meta_declare mv t accu) metas Unification.Meta.empty in
+  pp(lazy(str"FO " ++ pr_econstr_env env ise p ++ str " = " ++ pr_econstr_env env ise c));
   let _ : _ * Evd.evar_map = unif_FO_skip_impl env ise metas p c in
   ()
 
@@ -594,7 +615,11 @@ let match_upats_FO upats env sigma0 ise orig_c =
            raise (FoundUnif (ungen_upat lhs pt' u))
        with FoundUnif (_, s,_,_) as sig_u when dont_impact_evars s -> raise sig_u
        | Not_found -> CErrors.anomaly (str"incomplete ise in match_upats_FO.")
-       | e when CErrors.noncritical e -> () in
+       | e when CErrors.noncritical e ->
+    pp(lazy(str"FO fail: " ++ CErrors.print e));
+
+
+        () in
     List.iter one_match fpats
   done;
   iter_constr_LR ise loop f; Array.iter loop a in