Typeclasses API using EConstr.

13 files changed, 59 insertions, 44 deletions

diff --git a/engine/termops.ml b/engine/termops.ml
index f191e2dc1..e5db3c085 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -818,6 +818,15 @@ let is_section_variable id =
   try let _ = Global.lookup_named id in true
   with Not_found -> false
 
+let global_of_constr sigma c =
+  let open Globnames in
+  match EConstr.kind sigma c with
+  | Const (c, u) -> ConstRef c, u
+  | Ind (i, u) -> IndRef i, u
+  | Construct (c, u) -> ConstructRef c, u
+  | Var id -> VarRef id, Univ.Instance.empty
+  | _ -> raise Not_found
+
 let isGlobalRef sigma c =
   match EConstr.kind sigma c with
   | Const _ | Ind _ | Construct _ | Var _ -> true
diff --git a/engine/termops.mli b/engine/termops.mli
index 4becca907..c90fdf9c2 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -264,6 +264,8 @@ val dependency_closure : env -> Evd.evar_map -> Context.Named.t -> Id.Set.t -> I
 (** Test if an identifier is the basename of a global reference *)
 val is_section_variable : Id.t -> bool
 
+val global_of_constr : Evd.evar_map -> EConstr.constr -> Globnames.global_reference puniverses
+
 val isGlobalRef : Evd.evar_map -> EConstr.t -> bool
 
 val is_template_polymorphic : env -> Evd.evar_map -> EConstr.t -> bool
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index 5703687c4..0091d0d0a 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -127,7 +127,7 @@ let app_poly_sort b =
 let find_class_proof proof_type proof_method env evars carrier relation =
   try
     let evars, goal = app_poly_check env evars proof_type [| carrier ; relation |] in
-    let evars', c = Typeclasses.resolve_one_typeclass env (goalevars evars) goal in
+    let evars', c = Typeclasses.resolve_one_typeclass env (goalevars evars) (EConstr.of_constr goal) in
       if extends_undefined (goalevars evars) evars' then raise Not_found
       else app_poly_check env (evars',cstrevars evars) proof_method [| carrier; relation; c |]
   with e when Logic.catchable_exception e -> raise Not_found
@@ -367,7 +367,7 @@ end) = struct
 	   let evars, inst = 
 	     app_poly env (evars,Evar.Set.empty)
 	       rewrite_relation_class [| evar; mkApp (c, params) |] in
-	   let _ = Typeclasses.resolve_one_typeclass env' (goalevars evars) inst in
+	   let _ = Typeclasses.resolve_one_typeclass env' (goalevars evars) (EConstr.of_constr inst) in
 	     Some (it_mkProd_or_LetIn t rels)
 	   with e when CErrors.noncritical e -> None)
   | _ -> None
@@ -1937,7 +1937,7 @@ let default_morphism sign m =
     PropGlobal.build_signature (sigma, Evar.Set.empty) env t (fst sign) (snd sign)
   in
   let evars, morph = app_poly_check env evars PropGlobal.proper_type [| t; sign; m |] in
-  let evars, mor = resolve_one_typeclass env (goalevars evars) morph in
+  let evars, mor = resolve_one_typeclass env (goalevars evars) (EConstr.of_constr morph) in
     mor, proper_projection mor morph
 
 let add_setoid global binders a aeq t n =
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 9997976c4..b729f3b9b 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1314,7 +1314,7 @@ let reduce_to_ref_gen allow_product env sigma ref t =
             error_cannot_recognize ref
       | _ ->
 	  try
-	    if eq_gr (global_of_constr (EConstr.to_constr sigma c)) ref
+	    if eq_gr (fst (global_of_constr sigma c)) ref
 	    then it_mkProd_or_LetIn t l
 	    else raise Not_found
 	  with Not_found ->
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 11f71ee02..a970c434f 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -136,23 +136,24 @@ let typeclass_univ_instance (cl,u') =
 
 let class_info c =
   try Refmap.find c !classes
-  with Not_found -> not_a_class (Global.env()) (printable_constr_of_global c)
+  with Not_found -> not_a_class (Global.env()) (EConstr.of_constr (printable_constr_of_global c))
 
-let global_class_of_constr env c =
-  try let gr, u = Universes.global_of_constr c in
+let global_class_of_constr env sigma c =
+  try let gr, u = Termops.global_of_constr sigma c in
 	class_info gr, u
   with Not_found -> not_a_class env c
 
-let dest_class_app env c =
-  let cl, args = decompose_app c in
-    global_class_of_constr env cl, args
+let dest_class_app env sigma c =
+  let cl, args = EConstr.decompose_app sigma c in
+    global_class_of_constr env sigma cl, (List.map EConstr.Unsafe.to_constr args)
 
-let dest_class_arity env c =
-  let rels, c = decompose_prod_assum c in
-    rels, dest_class_app env c
+let dest_class_arity env sigma c =
+  let open EConstr in
+  let rels, c = decompose_prod_assum sigma c in
+    rels, dest_class_app env sigma c
 
-let class_of_constr c =
-  try Some (dest_class_arity (Global.env ()) c)
+let class_of_constr sigma c =
+  try Some (dest_class_arity (Global.env ()) sigma c)
   with e when CErrors.noncritical e -> None
 
 let is_class_constr c = 
@@ -161,15 +162,14 @@ let is_class_constr c =
   with Not_found -> false
 
 let rec is_class_type evd c =
-  let c, args = decompose_app c in
-    match kind_of_term c with
+  let c, _ = Termops.decompose_app_vect evd c in
+    match EConstr.kind evd (EConstr.of_constr c) with
     | Prod (_, _, t) -> is_class_type evd t
-    | Evar (e, _) when Evd.is_defined evd e ->
-      is_class_type evd (EConstr.Unsafe.to_constr (Evarutil.whd_head_evar evd (EConstr.of_constr c)))
+    | Cast (t, _, _) -> is_class_type evd t
     | _ -> is_class_constr c
       
 let is_class_evar evd evi =
-  is_class_type evd evi.Evd.evar_concl
+  is_class_type evd (EConstr.of_constr evi.Evd.evar_concl)
 
 (*
  * classes persistent object
@@ -222,7 +222,7 @@ let discharge_class (_,cl) =
   let discharge_context ctx' subst (grs, ctx) =
     let grs' =
       let newgrs = List.map (fun decl ->
-			     match decl |> RelDecl.get_type |> class_of_constr with
+			     match decl |> RelDecl.get_type |> EConstr.of_constr |> class_of_constr Evd.empty with
 			     | None -> None
 			     | Some (_, ((tc,_), _)) -> Some (tc.cl_impl, true))
 			    ctx'
@@ -270,7 +270,7 @@ let add_class cl =
 let check_instance env sigma c =
   try 
     let (evd, c) = resolve_one_typeclass env sigma
-      (Retyping.get_type_of env sigma c) in
+      (EConstr.of_constr (Retyping.get_type_of env sigma c)) in
       not (Evd.has_undefined evd)
   with e when CErrors.noncritical e -> false
 
@@ -282,10 +282,10 @@ let build_subclasses ~check env sigma glob pri =
         Nameops.add_suffix _id ("_subinstance_" ^ string_of_int !i))
   in
   let ty, ctx = Global.type_of_global_in_context env glob in
+  let ty = EConstr.of_constr ty in
   let sigma = Evd.merge_context_set Evd.univ_rigid sigma (Univ.ContextSet.of_context ctx) in
   let rec aux pri c ty path =
-    let ty = Evarutil.nf_evar sigma ty in
-      match class_of_constr ty with
+      match class_of_constr sigma ty with
       | None -> []
       | Some (rels, ((tc,u), args)) ->
 	let instapp = 
@@ -313,7 +313,7 @@ let build_subclasses ~check env sigma glob pri =
 	let declare_proj hints (cref, pri, body) =
 	  let path' = cref :: path in
 	  let ty = Retyping.get_type_of env sigma (EConstr.of_constr body) in
-	  let rest = aux pri body ty path' in
+	  let rest = aux pri body (EConstr.of_constr ty) path' in
 	    hints @ (path', pri, body) :: rest
 	in List.fold_left declare_proj [] projs 
   in
@@ -406,7 +406,7 @@ let remove_instance i =
 
 let declare_instance pri local glob =
   let ty = Global.type_of_global_unsafe glob in
-    match class_of_constr ty with
+    match class_of_constr Evd.empty (EConstr.of_constr ty) with
     | Some (rels, ((tc,_), args) as _cl) ->
       add_instance (new_instance tc pri (not local) (Flags.use_polymorphic_flag ()) glob)
 (*       let path, hints = build_subclasses (not local) (Global.env ()) Evd.empty glob in *)
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 2530f5dfa..ec36c57e0 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -61,13 +61,13 @@ val class_info : global_reference -> typeclass (** raises a UserError if not a c
 (** These raise a UserError if not a class.
     Caution: the typeclass structures is not instantiated w.r.t. the universe instance.
     This is done separately by typeclass_univ_instance. *)
-val dest_class_app : env -> constr -> typeclass puniverses * constr list
+val dest_class_app : env -> evar_map -> EConstr.constr -> typeclass puniverses * constr list
 
 (** Get the instantiated typeclass structure for a given universe instance. *)
 val typeclass_univ_instance : typeclass puniverses -> typeclass puniverses
 
 (** Just return None if not a class *)
-val class_of_constr : constr -> (Context.Rel.t * (typeclass puniverses * constr list)) option
+val class_of_constr : evar_map -> EConstr.constr -> (Context.Rel.t * (typeclass puniverses * constr list)) option
   
 val instance_impl : instance -> global_reference
 
@@ -99,11 +99,11 @@ val mark_unresolvables : ?filter:evar_filter -> evar_map -> evar_map
 val mark_resolvables   : ?filter:evar_filter -> evar_map -> evar_map
 val mark_resolvable : evar_info -> evar_info
 val is_class_evar : evar_map -> evar_info -> bool
-val is_class_type : evar_map -> types -> bool
+val is_class_type : evar_map -> EConstr.types -> bool
 
 val resolve_typeclasses : ?fast_path:bool -> ?filter:evar_filter -> ?unique:bool ->
   ?split:bool -> ?fail:bool -> env -> evar_map -> evar_map
-val resolve_one_typeclass : ?unique:bool -> env -> evar_map -> types -> open_constr
+val resolve_one_typeclass : ?unique:bool -> env -> evar_map -> EConstr.types -> open_constr
 
 val set_typeclass_transparency_hook : (evaluable_global_reference -> bool (*local?*) -> bool -> unit) Hook.t
 val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> unit
@@ -120,7 +120,7 @@ val add_instance_hint : global_reference_or_constr -> global_reference list ->
 val remove_instance_hint : global_reference -> unit
 
 val solve_all_instances_hook : (env -> evar_map -> evar_filter -> bool -> bool -> bool -> evar_map) Hook.t
-val solve_one_instance_hook : (env -> evar_map -> types -> bool -> open_constr) Hook.t
+val solve_one_instance_hook : (env -> evar_map -> EConstr.types -> bool -> open_constr) Hook.t
 
 val declare_instance : int option -> bool -> global_reference -> unit
 
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index b1dfb19a0..2db0e9e88 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -9,6 +9,7 @@
 (*i*)
 open Names
 open Term
+open EConstr
 open Environ
 open Constrexpr
 open Globnames
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index ee76f6383..9bd430e4d 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -9,6 +9,7 @@
 open Loc
 open Names
 open Term
+open EConstr
 open Environ
 open Constrexpr
 open Globnames
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index bef43d20b..ff7dbfa91 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -478,9 +478,9 @@ let is_Prop env sigma concl =
   | Sort (Prop Null) -> true
   | _ -> false
 
-let is_unique env concl =
+let is_unique env sigma concl =
   try
-    let (cl,u), args = dest_class_app env concl in
+    let (cl,u), args = dest_class_app env sigma concl in
     cl.cl_unique
   with e when CErrors.noncritical e -> false
 
@@ -675,7 +675,7 @@ module V85 = struct
     let tacgl = {it = gl; sigma = s;} in
     let secvars = secvars_of_hyps (Environ.named_context_of_val (Goal.V82.hyps s gl)) in
     let poss = e_possible_resolve hints info.hints secvars info.only_classes s concl in
-    let unique = is_unique env concl in
+    let unique = is_unique env s (EConstr.of_constr concl) in
     let rec aux i foundone = function
       | (tac, _, extern, name, pp) :: tl ->
          let derivs = path_derivate info.auto_cut name in
@@ -997,7 +997,7 @@ module Search = struct
     let concl = Goal.concl gl in
     let sigma = Goal.sigma gl in
     let s = Sigma.to_evar_map sigma in
-    let unique = not info.search_dep || is_unique env concl in
+    let unique = not info.search_dep || is_unique env s (EConstr.of_constr concl) in
     let backtrack = needs_backtrack env s unique concl in
     if !typeclasses_debug > 0 then
       Feedback.msg_debug
@@ -1071,7 +1071,7 @@ module Search = struct
             try
               let evi = Evd.find_undefined sigma ev in
               if info.search_only_classes then
-                Some (ev, is_class_type sigma (Evd.evar_concl evi))
+                Some (ev, is_class_evar sigma evi)
               else Some (ev, true)
             with Not_found -> None
           in
@@ -1351,7 +1351,7 @@ let error_unresolvable env comp evd =
   | Some s -> Evar.Set.mem ev s
   in
   let fold ev evi (found, accu) =
-    let ev_class = class_of_constr evi.evar_concl in
+    let ev_class = class_of_constr evd (EConstr.of_constr evi.evar_concl) in
     if not (Option.is_empty ev_class) && is_part ev then
       (* focus on one instance if only one was searched for *)
       if not found then (true, Some ev)
@@ -1481,7 +1481,7 @@ let resolve_one_typeclass env ?(sigma=Evd.empty) gl unique =
 
 let _ =
   Hook.set Typeclasses.solve_one_instance_hook
-    (fun x y z w -> resolve_one_typeclass x ~sigma:y z w)
+    (fun x y z w -> resolve_one_typeclass x ~sigma:y (EConstr.Unsafe.to_constr z) w)
 
 (** Take the head of the arity of a constr.
     Used in the partial application tactic. *)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e4503dab6..a6bc805bd 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1672,6 +1672,7 @@ let solve_remaining_apply_goals =
       let env = Proofview.Goal.env gl in
       let evd = Sigma.to_evar_map sigma in
       let concl = Proofview.Goal.concl gl in
+      let concl = EConstr.of_constr concl in
       if Typeclasses.is_class_type evd concl then
         let evd', c' = Typeclasses.resolve_one_typeclass env evd concl in
         let tac = Refine.refine ~unsafe:true { run = fun h -> Sigma.here c' h } in
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index ad4a13c21..26e29540c 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -65,7 +65,7 @@ let existing_instance glob g pri =
   let c = global g in
   let instance = Global.type_of_global_unsafe c in
   let _, r = decompose_prod_assum instance in
-    match class_of_constr r with
+    match class_of_constr Evd.empty (EConstr.of_constr r) with
       | Some (_, ((tc,u), _)) -> add_instance (new_instance tc pri glob 
   (*FIXME*) (Flags.use_polymorphic_flag ()) c)
       | None -> user_err ~loc:(loc_of_reference g)
@@ -155,7 +155,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
     let imps = imps @ Impargs.lift_implicits len imps' in
     let ctx', c = decompose_prod_assum c' in
     let ctx'' = ctx' @ ctx in
-    let k, args = Typeclasses.dest_class_app (push_rel_context ctx'' env) c in
+    let k, args = Typeclasses.dest_class_app (push_rel_context ctx'' env) !evars (EConstr.of_constr c) in
     let cl, u = Typeclasses.typeclass_univ_instance k in
     let _, args = 
       List.fold_right (fun decl (args, args') ->
@@ -378,7 +378,7 @@ let context poly l =
       let () = uctx := Univ.ContextSet.empty in
       let decl = (ParameterEntry (None,poly,(t,ctx),None), IsAssumption Logical) in
       let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in
-	match class_of_constr t with
+	match class_of_constr !evars (EConstr.of_constr t) with
 	| Some (rels, ((tc,_), args) as _cl) ->
 	    add_instance (Typeclasses.new_instance tc None false (*FIXME*)
 			    poly (ConstRef cst));
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 1d82d9ae1..df1f47e33 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -584,7 +584,7 @@ let rec explain_evar_kind env sigma evk ty = function
       (pr_lconstr_env env sigma ty') (snd evi.evar_source)
 
 let explain_typeclass_resolution env sigma evi k =
-  match Typeclasses.class_of_constr evi.evar_concl with
+  match Typeclasses.class_of_constr sigma (EConstr.of_constr evi.evar_concl) with
   | Some _ ->
     let env = Evd.evar_filtered_env evi in
       fnl () ++ str "Could not find an instance for " ++
@@ -597,7 +597,7 @@ let explain_placeholder_kind env sigma c e =
   | Some (SeveralInstancesFound n) ->
       strbrk " (several distinct possible type class instances found)"
   | None ->
-      match Typeclasses.class_of_constr c with
+      match Typeclasses.class_of_constr sigma (EConstr.of_constr c) with
       | Some _ -> strbrk " (no type class instance found)"
       | _ -> mt ()
 
@@ -1012,6 +1012,7 @@ let explain_module_internalization_error = function
 (* Typeclass errors *)
 
 let explain_not_a_class env c =
+  let c = EConstr.to_constr Evd.empty c in
   pr_constr_env env Evd.empty c ++ str" is not a declared type class."
 
 let explain_unbound_method env cid id =
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 5f2b99f90..dc49c5385 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -484,7 +484,7 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity
   in
   let ctx_context =
     List.map (fun decl ->
-      match Typeclasses.class_of_constr (RelDecl.get_type decl) with
+      match Typeclasses.class_of_constr Evd.empty (EConstr.of_constr (RelDecl.get_type decl)) with
       | Some (_, ((cl,_), _)) -> Some (cl.cl_impl, true)
       | None -> None)
       params, params