wip

Author: qvermande

pretyping/evarconv.ml

@@ -892,12 +892,16 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
       | _ -> UnifFailure (evd,NotSameHead)
     in
     let tc evd =
-      let ty = Retyping.get_type_of env evd termF in
-      match Typeclasses.resolve_one_typeclass env evd ty with
-      | exception Not_found -> UnifFailure (evd, NotSameHead)
-      | evd, c -> ise_and evd [
-        (fun i -> evar_conv_x flags env i CONV termF c);
-        (fun i -> switch (evar_eqappr_x flags env i pbty keys lastUnfolded) apprF apprR)] in
+      let (e, _) = EConstr.destEvar evd termF in
+      if not (Evd.is_typeclass_evar evd e) then UnifFailure (evd, NotSameHead) else
+      let tc_evars = Evd.get_typeclass_evars evd in
+      let evd = Evd.set_typeclass_evars evd (Evar.Set.singleton e) in
+      let evd = Typeclasses.resolve_typeclasses env evd in
+      if not (Evd.is_defined evd e) then UnifFailure (evd, NotSameHead) else
+      let tc_evars = Evar.Set.union tc_evars (Evd.get_typeclass_evars evd) in
+      let tc_evars = Evar.Set.filter (fun e -> not (Evd.is_defined evd e)) tc_evars in
+      let evd = Evd.set_typeclass_evars evd tc_evars in
+      evar_eqappr_x flags env evd pbty keys lastUnfolded (whd_nored_state env evd apprF) apprR in
     match Stack.list_of_app_stack skF with
     | None ->
         ise_try evd [consume_stack l2r apprF apprR; eta; tc]

pretyping/keys.ml

@@ -15,6 +15,8 @@ open Constr
 open Libobject
 open Globnames
 
+let debug_keys = CDebug.create ~name:"keys" ()
+
 type key =
   | KGlob of GlobRef.t
   | KLam
@@ -64,6 +66,23 @@ module KeyOrdered = struct
     | k, k' -> k == k'
 end
 
+let pr_key pr_global k =
+  let open Pp in
+  match k with
+  | KGlob gr -> pr_global gr
+  | KLam -> str"Lambda"
+  | KLet -> str"Let"
+  | KProd -> str"Product"
+  | KSort -> str"Sort"
+  | KCase -> str"Case"
+  | KFix -> str"Fix"
+  | KCoFix -> str"CoFix"
+  | KRel -> str"Rel"
+  | KInt -> str"Int"
+  | KFloat -> str"Float"
+  | KString -> str"String"
+  | KArray -> str"Array"
+
 module Keymap = HMap.Make(KeyOrdered)
 
 (* Mapping structure for references to be considered equivalent *)
@@ -79,8 +98,12 @@ let add_keys k ki v vi =
 
 let equiv_keys k k' =
   if k == k' || KeyOrdered.equal k k' then Some ((0, 0)) else
-  try Some (Keymap.find k' (Keymap.find k !keys))
-  with Not_found -> None
+  try let r = Some (Keymap.find k' (Keymap.find k !keys)) in
+    let () = debug_keys (fun () -> Pp.(v 0 (pr_key Names.GlobRef.print k ++ str " = " ++ pr_key Names.GlobRef.print k' ++ cut ()))) in
+    r
+  with Not_found ->
+    let () = debug_keys (fun () -> Pp.(v 0 (pr_key Names.GlobRef.print k ++ str " != " ++ pr_key Names.GlobRef.print k' ++ cut ()))) in
+    None
 
 let mkKGlob env gr = KGlob (Environ.QGlobRef.canonize env gr)
 
@@ -150,21 +173,6 @@ let constr_key env kind c =
 
 open Pp
 
-let pr_key pr_global = function
-  | KGlob gr -> pr_global gr
-  | KLam -> str"Lambda"
-  | KLet -> str"Let"
-  | KProd -> str"Product"
-  | KSort -> str"Sort"
-  | KCase -> str"Case"
-  | KFix -> str"Fix"
-  | KCoFix -> str"CoFix"
-  | KRel -> str"Rel"
-  | KInt -> str"Int"
-  | KFloat -> str"Float"
-  | KString -> str"String"
-  | KArray -> str"Array"
-
 let pr_keyset pr_global v =
   prlist_with_sep spc (fun (k, (i, i')) -> pr_key pr_global k ++ str "(" ++ int i ++ str ", " ++ int i' ++ str ")") (Keymap.bindings v)
 

pretyping/reductionops.mli

@@ -302,6 +302,7 @@ type state_reduction_function =
 
 val pr_state : env -> evar_map -> state -> Pp.t
 
+(** Removes cast and puts into applicative form *)
 val whd_nored_state : ?metas:meta_handler -> state_reduction_function
 
 val whd_betaiota_deltazeta_for_iota_state :