patch evarconv

Author: Tragicus

apps/cs/src/evarconv_hacked.ml

@@ -488,7 +488,10 @@ let rec ise_stack2 no_app env evd f sk1 sk2 =
     |_, _ -> fail (UnifFailure (i,(* Maybe improve: *) NotSameHead))
   in ise_rev_stack2 false evd (List.rev sk1) (List.rev sk2)
 
-type hook = Environ.env -> Evd.evar_map -> EConstr.t -> EConstr.t -> Evd.evar_map option
+type hook = Environ.env -> Evd.evar_map -> (EConstr.t * Reductionops.Stack.t) -> (EConstr.t * Reductionops.Stack.t) -> (Evd.evar_map * (EConstr.t * EConstr.t) * EConstr.t * EConstr.t list *
+(EConstr.t list * EConstr.t list) * (EConstr.t list * EConstr.t list) *
+(Reductionops.Stack.t * Reductionops.Stack.t) * EConstr.constr *
+(int option * EConstr.constr)) option
 
 let all_hooks = ref (CString.Map.empty : hook CString.Map.t)
 
@@ -591,6 +594,38 @@ let infer_conv_noticing_evars ~pb ~ts env sigma t1 t2 =
     if !has_evar then None
     else Some (UnifFailure (sigma, UnifUnivInconsistency e))
 
+let pr_econstr = ref (fun _ _ _ -> Pp.str "unable to print econstr")
+
+(* TODO: move to a proper place *)
+let rec split_at n acc l =
+   if n = 0 then (List.rev acc, l)
+   else match l with
+   | [] -> (List.rev acc, l)
+   | h :: t -> split_at (n-1) (h :: acc) t
+let split_at n l = split_at n [] l
+
+let try_simplify_proj_construct flags env evd v k sk =
+   match k with (* try unfolding an applied projection on the rhs *)
+   | Proj (p, _, c) -> begin
+      let c = whd_all env evd c in (* reduce argument *)
+      try let (hd, args) = destApp evd c in
+         if isConstruct evd hd then Some (whd_nored_state env evd (args.(Projection.npars p + Projection.arg p), sk))
+         else None
+      with _ -> None
+      end
+   | Const (cn, _) when Structures.Structure.is_projection cn -> begin
+      match split_at (Structures.Structure.projection_nparams cn) (Option.default [] (Stack.list_of_app_stack sk)) with
+      | (_, []) -> None
+      | (_, c :: _) -> begin
+         let c = whd_all env evd c in
+         try let (hd, _) = destApp evd c in
+            if isConstruct evd hd then
+              Some (whd_betaiota_deltazeta_for_iota_state flags.open_ts env evd (v,sk))
+            else None
+         with _ -> None
+      end end
+   | _ -> None
+
 let rec evar_conv_x flags env evd pbty term1 term2 =
   let term1 = whd_head_evar evd term1 in
   let term2 = whd_head_evar evd term2 in
@@ -923,7 +958,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
       flex_maybeflex false ev2 appr2 appr1 v1
 
     | MaybeFlexible v1, MaybeFlexible v2 -> begin
-        match EConstr.kind evd term1, EConstr.kind evd term2 with
+       let k1 = EConstr.kind evd term1 in
+       let k2 = EConstr.kind evd term2 in
+        begin
+        match k1, k2 with
         | LetIn (na1,b1,t1,c'1), LetIn (na2,b2,t2,c'2) ->
         let f1 i = (* FO *)
           ise_and i
@@ -996,16 +1034,22 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
           | None ->
             UnifFailure (i,NotSameHead)
         and f2 i =
-          (try
+          (match try_simplify_proj_construct flags env evd v1 k1 sk1, try_simplify_proj_construct flags env evd v2 k2 sk2 with
+          | Some x1, Some x2 -> UnifFailure (i,NoCanonicalStructure)
+          | Some x1, None -> UnifFailure (i,NoCanonicalStructure)
+          | None, Some x2 -> UnifFailure (i,NoCanonicalStructure)
+          | _, _ -> (try
              if not flags.with_cs then raise Not_found
              else conv_record flags env
                (try check_conv_record env i appr1 appr2
-                with Not_found -> check_conv_record env i appr2 appr1)
-          with Not_found ->
-             let sigma = i in
-             match apply_hooks env sigma (Stack.zip sigma appr1) (Stack.zip sigma appr2) with
-             | Some sigma -> Success sigma
-             | None -> UnifFailure (i,NoCanonicalStructure))
+                with Not_found -> begin match (apply_hooks env i appr1 appr2) with
+                  | Some r -> r
+                  | None -> begin try check_conv_record env i appr2 appr1
+                    with Not_found -> begin match (apply_hooks env i appr2 appr1) with
+                      | Some r -> r
+                      | None -> raise Not_found
+                end end end)
+            with Not_found -> UnifFailure (i,NoCanonicalStructure)))
         and f3 i =
           (* heuristic: unfold second argument first, exception made
              if the first argument is a beta-redex (expand a constant
@@ -1044,7 +1088,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
                  flags.open_ts env i (v2,sk2))
         in
         ise_try evd [f1; f2; f3]
-    end
+    end end
 
     | Rigid, Rigid when EConstr.isLambda evd term1 && EConstr.isLambda evd term2 ->
         let (na1,c1,c'1) = EConstr.destLambda evd term1 in
@@ -1062,14 +1106,21 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
     | Rigid, Flexible ev2 -> flex_rigid false ev2 appr2 appr1
 
     | MaybeFlexible v1, Rigid ->
+       let k1 = EConstr.kind evd term1 in begin
+      let () = debug_unification (fun () -> Pp.(v 0 (str "v1 maybeflexible against rigid" ++ !pr_econstr env evd v1 ++ cut ()))) in
+       match try_simplify_proj_construct flags env evd v1 k1 sk1 with
+       | Some x1 -> evar_eqappr_x flags env evd pbty x1 appr2
+       | None ->
         let f3 i =
           (try
              if not flags.with_cs then raise Not_found
-             else conv_record flags env (check_conv_record env i appr1 appr2)
-           with Not_found -> let sigma = i in
-             match apply_hooks env sigma (Stack.zip sigma appr1) (Stack.zip sigma appr2) with
-             | Some sigma -> Success sigma
-             | None -> UnifFailure (i,NoCanonicalStructure))
+             else conv_record flags env (
+               try check_conv_record env i appr1 appr2 with
+               | Not_found -> begin match apply_hooks env i appr1 appr2 with
+                 | Some r -> r
+                 | None -> raise Not_found
+               end)
+           with Not_found -> UnifFailure (i,NoCanonicalStructure))
 
         and f4 i =
           evar_eqappr_x flags env i pbty
@@ -1078,22 +1129,32 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
             appr2
         in
           ise_try evd [f3; f4]
+        end
 
     | Rigid, MaybeFlexible v2 ->
+       let k2 = EConstr.kind evd term2 in begin
+      let () = debug_unification (fun () -> Pp.(v 0 (str "rigid against v2 maybeflexible" ++ !pr_econstr env evd v2 ++ cut ()))) in
+       match try_simplify_proj_construct flags env evd v2 k2 sk2 with
+       | Some x2 -> let () = debug_unification (fun () -> Pp.(v 0 (str "reduced to" ++ !pr_econstr env evd (let (x, _) = x2 in x)))) in evar_eqappr_x flags env evd pbty appr1 x2
+       | None ->
         let f3 i =
           (try
              if not flags.with_cs then raise Not_found
-             else conv_record flags env (check_conv_record env i appr2 appr1)
-           with Not_found -> let sigma = i in
-             match apply_hooks env sigma (Stack.zip sigma appr1) (Stack.zip sigma appr2) with
-             | Some sigma -> Success sigma
-             | None -> UnifFailure (i,NoCanonicalStructure))
+             else conv_record flags env (
+               try check_conv_record env i appr2 appr1 with
+               | Not_found -> begin let () = debug_unification (fun () -> Pp.(v 0 (str "ask cs hook"))) in match apply_hooks env i appr2 appr1 with
+                 | Some r -> r
+                 | None -> raise Not_found
+               end
+                 | e -> let () = Feedback.msg_info Pp.(str "cs hook crashed") in failwith "argh")
+           with Not_found -> UnifFailure (i,NoCanonicalStructure))
         and f4 i =
           evar_eqappr_x flags env i pbty appr1
             (whd_betaiota_deltazeta_for_iota_state
                flags.open_ts env i (v2,sk2))
         in
           ise_try evd [f3; f4]
+        end
 
     (* Eta-expansion *)
     | Rigid, _ when isLambda evd term1 && (* if ever ill-typed: *) List.is_empty sk1 ->
@@ -1277,8 +1338,7 @@ and conv_record flags env (evd,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2),c
        (fun i -> evar_conv_x flags env i CONV c1 app);
        (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk1 sk2);
        test;
-       (fun i -> evar_conv_x flags env i CONV h2
-         (fst (decompose_app i (substl ks h))))]
+       (fun i -> evar_conv_x flags env i CONV h2 (fst (decompose_app i (substl ks h))))]
   else UnifFailure(evd,(*dummy*)NotSameHead)
 
 and eta_constructor flags env evd ((ind, i), u) sk1 (term2,sk2) =