1 files changed, 237 insertions, 71 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index f6e13e1f43..6345046431 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -21,6 +21,9 @@ open Environ
 (* module RelDecl = Context.Rel.Declaration *)
 module NamedDecl = Context.Named.Declaration
 
+type econstr = constr
+type etypes = types
+
 (** Generic filters *)
 module Filter :
 sig
@@ -129,8 +132,6 @@ end
 
 module Store = Store.Make ()
 
-type evar = Evar.t
-
 let string_of_existential evk = "?X" ^ string_of_int (Evar.repr evk)
 
 type evar_body =
@@ -143,8 +144,7 @@ type evar_info = {
   evar_body : evar_body;
   evar_filter : Filter.t;
   evar_source : Evar_kinds.t Loc.located;
-  evar_candidates : constr list option; (* if not None, list of allowed instances *)
-  evar_extra : Store.t }
+  evar_candidates : constr list option; (* if not None, list of allowed instances *)}
 
 let make_evar hyps ccl = {
   evar_concl = ccl;
@@ -152,9 +152,7 @@ let make_evar hyps ccl = {
   evar_body = Evar_empty;
   evar_filter = Filter.identity;
   evar_source = Loc.tag @@ Evar_kinds.InternalHole;
-  evar_candidates = None;
-  evar_extra = Store.empty
-}
+  evar_candidates = None; }
 
 let instance_mismatch () =
   anomaly (Pp.str "Signature and its instance do not match.")
@@ -170,6 +168,8 @@ let evar_context evi = named_context_of_val evi.evar_hyps
 let evar_filtered_context evi =
   Filter.filter_list (evar_filter evi) (evar_context evi)
 
+let evar_candidates evi = evi.evar_candidates
+
 let evar_hyps evi = evi.evar_hyps
 
 let evar_filtered_hyps evi = match Filter.repr (evar_filter evi) with
@@ -410,6 +410,11 @@ end
 
 type goal_kind = ToShelve | ToGiveUp
 
+type evar_flags =
+  { obligation_evars : Evar.Set.t;
+    restricted_evars : Evar.t Evar.Map.t;
+    typeclass_evars : Evar.Set.t }
+
 type evar_map = {
   (** Existential variables *)
   defn_evars : evar_info EvMap.t;
@@ -422,6 +427,7 @@ type evar_map = {
   last_mods  : Evar.Set.t;
   (** Metas *)
   metas      : clbinding Metamap.t;
+  evar_flags : evar_flags;
   (** Interactive proofs *)
   effects    : Safe_typing.private_constants;
   future_goals : Evar.t list; (** list of newly created evars, to be
@@ -438,20 +444,84 @@ type evar_map = {
   extras : Store.t;
 }
 
+let get_is_maybe_typeclass, (is_maybe_typeclass_hook : (evar_map -> constr -> bool) Hook.t) = Hook.make ~default:(fun evd c -> false) ()
+
+let is_maybe_typeclass sigma c = Hook.get get_is_maybe_typeclass sigma c
+
 (*** Lifting primitive from Evar.Map. ***)
 
 let rename evk id evd =
   { evd with evar_names = EvNames.rename evk id evd.evar_names }
 
-let add_with_name ?name d e i = match i.evar_body with
+let add_with_name ?name ?(typeclass_candidate = true) d e i = match i.evar_body with
 | Evar_empty ->
   let evar_names = EvNames.add_name_undefined name e i d.evar_names in
-  { d with undf_evars = EvMap.add e i d.undf_evars; evar_names }
+  let evar_flags =
+    if typeclass_candidate && is_maybe_typeclass d i.evar_concl then
+      let flags = d.evar_flags in
+      { flags with typeclass_evars = Evar.Set.add e flags.typeclass_evars }
+    else d.evar_flags
+  in
+  { d with undf_evars = EvMap.add e i d.undf_evars; evar_names; evar_flags }
 | Evar_defined _ ->
   let evar_names = EvNames.remove_name_defined e d.evar_names in
   { d with defn_evars = EvMap.add e i d.defn_evars; evar_names }
 
-let add d e i = add_with_name d e i
+(** Evd.add is a low-level function mainly used to update the evar_info
+    associated to an evar, so we prevent registering its typeclass status. *)
+let add d e i = add_with_name ~typeclass_candidate:false d e i
+
+(*** Evar flags: typeclasses, restricted or obligation flag *)
+
+let get_typeclass_evars evd = evd.evar_flags.typeclass_evars
+
+let set_typeclass_evars evd tcs =
+  let flags = evd.evar_flags in
+  { evd with evar_flags = { flags with typeclass_evars = tcs } }
+
+let is_typeclass_evar evd evk =
+  let flags = evd.evar_flags in
+  Evar.Set.mem evk flags.typeclass_evars
+
+let get_obligation_evars evd = evd.evar_flags.obligation_evars
+
+let set_obligation_evar evd evk =
+  let flags = evd.evar_flags in
+  let evar_flags = { flags with obligation_evars = Evar.Set.add evk flags.obligation_evars } in
+  { evd with evar_flags }
+
+let is_obligation_evar evd evk =
+  let flags = evd.evar_flags in
+  Evar.Set.mem evk flags.obligation_evars
+
+(** Inheritance of flags: for evar-evar and restriction cases *)
+
+let inherit_evar_flags evar_flags evk evk' =
+  let evk_typeclass = Evar.Set.mem evk evar_flags.typeclass_evars in
+  let evk_obligation = Evar.Set.mem evk evar_flags.obligation_evars in
+  if not (evk_obligation || evk_typeclass) then evar_flags
+  else
+    let typeclass_evars =
+      if evk_typeclass then
+        let typeclass_evars = Evar.Set.remove evk evar_flags.typeclass_evars in
+        Evar.Set.add evk' typeclass_evars
+      else evar_flags.typeclass_evars
+    in
+    let obligation_evars =
+      if evk_obligation then
+        let obligation_evars = Evar.Set.remove evk evar_flags.obligation_evars in
+        Evar.Set.add evk' obligation_evars
+      else evar_flags.obligation_evars
+    in
+    { evar_flags with obligation_evars; typeclass_evars }
+
+(** Removal: in all other cases of definition *)
+
+let remove_evar_flags evk evar_flags =
+  { typeclass_evars = Evar.Set.remove evk evar_flags.typeclass_evars;
+    obligation_evars = Evar.Set.remove evk evar_flags.obligation_evars;
+    (** Restriction information is kept. *)
+    restricted_evars = evar_flags.restricted_evars }
 
 (** New evars *)
 
@@ -461,9 +531,9 @@ let evar_counter_summary_name = "evar counter"
 let evar_ctr, evar_counter_summary_tag = Summary.ref_tag 0 ~name:evar_counter_summary_name
 let new_untyped_evar () = incr evar_ctr; Evar.unsafe_of_int !evar_ctr
 
-let new_evar evd ?name evi =
+let new_evar evd ?name ?typeclass_candidate evi =
   let evk = new_untyped_evar () in
-  let evd = add_with_name evd ?name evk evi in
+  let evd = add_with_name evd ?name ?typeclass_candidate evk evi in
   (evd, evk)
 
 let remove d e =
@@ -475,7 +545,9 @@ let remove d e =
   in
   let future_goals = List.filter (fun e' -> not (Evar.equal e e')) d.future_goals in
   let future_goals_status = EvMap.remove e d.future_goals_status in
-  { d with undf_evars; defn_evars; principal_future_goal; future_goals; future_goals_status }
+  let evar_flags = remove_evar_flags e d.evar_flags in
+  { d with undf_evars; defn_evars; principal_future_goal; future_goals; future_goals_status;
+           evar_flags }
 
 let find d e =
   try EvMap.find e d.undf_evars
@@ -507,8 +579,8 @@ let raw_map f d =
     in
     ans
   in
-  let defn_evars = EvMap.smartmapi f d.defn_evars in
-  let undf_evars = EvMap.smartmapi f d.undf_evars in
+  let defn_evars = EvMap.Smart.mapi f d.defn_evars in
+  let undf_evars = EvMap.Smart.mapi f d.undf_evars in
   { d with defn_evars; undf_evars; }
 
 let raw_map_undefined f d =
@@ -521,7 +593,7 @@ let raw_map_undefined f d =
     in
     ans
   in
-  { d with undf_evars = EvMap.smartmapi f d.undf_evars; }
+  { d with undf_evars = EvMap.Smart.mapi f d.undf_evars; }
 
 let is_evar = mem
 
@@ -537,10 +609,14 @@ let existential_value d (n, args) =
   | Evar_empty ->
     raise NotInstantiatedEvar
 
+let existential_value0 = existential_value
+
 let existential_opt_value d ev =
   try Some (existential_value d ev)
   with NotInstantiatedEvar -> None
 
+let existential_opt_value0 = existential_opt_value
+
 let existential_type d (n, args) =
   let info =
     try find d n
@@ -548,6 +624,8 @@ let existential_type d (n, args) =
       anomaly (str "Evar " ++ str (string_of_existential n) ++ str " was not declared.") in
   instantiate_evar_array info info.evar_concl args
 
+let existential_type0 = existential_type
+
 let add_constraints d c =
   { d with universes = UState.add_constraints d.universes c }
 
@@ -574,12 +652,18 @@ let cmap f evd =
 let create_evar_defs sigma = { sigma with
   conv_pbs=[]; last_mods=Evar.Set.empty; metas=Metamap.empty }
 
+let empty_evar_flags =
+  { obligation_evars = Evar.Set.empty;
+    restricted_evars = Evar.Map.empty;
+    typeclass_evars = Evar.Set.empty }
+
 let empty = {
   defn_evars = EvMap.empty;
   undf_evars = EvMap.empty;
   universes  = UState.empty;
   conv_pbs   = [];
   last_mods  = Evar.Set.empty;
+  evar_flags = empty_evar_flags;
   metas      = Metamap.empty;
   effects    = Safe_typing.empty_private_constants;
   evar_names = EvNames.empty; (* id<->key for undefined evars *)
@@ -613,19 +697,19 @@ let merge_universe_context evd uctx' =
 let set_universe_context evd uctx' =
   { evd with universes = uctx' }
 
+(* TODO: make unique *)
 let add_conv_pb ?(tail=false) pb d =
-  (** MS: we have duplicates here, why? *)
   if tail then {d with conv_pbs = d.conv_pbs @ [pb]}
   else {d with conv_pbs = pb::d.conv_pbs}
 
+let conv_pbs d = d.conv_pbs
+
 let evar_source evk d = (find d evk).evar_source
 
 let evar_ident evk evd = EvNames.ident evk evd.evar_names
 let evar_key id evd = EvNames.key id evd.evar_names
 
-let restricted = Store.field ()
-
-let define_aux ?dorestrict def undef evk body =
+let define_aux def undef evk body =
   let oldinfo =
     try EvMap.find evk undef
     with Not_found ->
@@ -635,24 +719,39 @@ let define_aux ?dorestrict def undef evk body =
         anomaly ~label:"Evd.define" (Pp.str "cannot define undeclared evar.")
   in
   let () = assert (oldinfo.evar_body == Evar_empty) in
-  let evar_extra = match dorestrict with
-    | Some evk' -> Store.set oldinfo.evar_extra restricted evk'
-    | None -> oldinfo.evar_extra in
-  let newinfo = { oldinfo with evar_body = Evar_defined body; evar_extra } in
+  let newinfo = { oldinfo with evar_body = Evar_defined body } in
   EvMap.add evk newinfo def, EvMap.remove evk undef
 
 (* define the existential of section path sp as the constr body *)
-let define evk body evd =
+let define_gen evk body evd evar_flags =
   let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
   let last_mods = match evd.conv_pbs with
   | [] ->  evd.last_mods
   | _ -> Evar.Set.add evk evd.last_mods
   in
   let evar_names = EvNames.remove_name_defined evk evd.evar_names in
-  { evd with defn_evars; undf_evars; last_mods; evar_names }
+  { evd with defn_evars; undf_evars; last_mods; evar_names; evar_flags }
+
+(** By default, the obligation and evar tag of the evar is removed *)
+let define evk body evd =
+  let evar_flags = remove_evar_flags evk evd.evar_flags in
+  define_gen evk body evd evar_flags
+
+(** In case of an evar-evar solution, the flags are inherited *)
+let define_with_evar evk body evd =
+  let evk' = fst (destEvar body) in
+  let evar_flags = inherit_evar_flags evd.evar_flags evk evk' in
+  define_gen evk body evd evar_flags
 
-let is_restricted_evar evi =
-  Store.get evi.evar_extra restricted
+let is_restricted_evar evd evk =
+  try Some (Evar.Map.find evk evd.evar_flags.restricted_evars)
+  with Not_found -> None
+
+let declare_restricted_evar evar_flags evk evk' =
+  { evar_flags with restricted_evars = Evar.Map.add evk evk' evar_flags.restricted_evars }
+
+(* In case of restriction, we declare the restriction and inherit the obligation
+   and typeclass flags. *)
 
 let restrict evk filter ?candidates ?src evd =
   let evk' = new_untyped_evar () in
@@ -668,9 +767,11 @@ let restrict evk filter ?candidates ?src evd =
   let ctxt = Filter.filter_list filter (evar_context evar_info) in
   let id_inst = Array.map_of_list (NamedDecl.get_id %> mkVar) ctxt in
   let body = mkEvar(evk',id_inst) in
-  let (defn_evars, undf_evars) = define_aux ~dorestrict:evk' evd.defn_evars evd.undf_evars evk body in
+  let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
+  let evar_flags = declare_restricted_evar evd.evar_flags evk evk' in
+  let evar_flags = inherit_evar_flags evar_flags evk evk' in
   { evd with undf_evars = EvMap.add evk' evar_info' undf_evars;
-    defn_evars; last_mods; evar_names }, evk'
+    defn_evars; last_mods; evar_names; evar_flags }, evk'
 
 let downcast evk ccl evd =
   let evar_info = EvMap.find evk evd.undf_evars in
@@ -763,7 +864,7 @@ let universe_subst evd =
   UState.subst evd.universes
 
 let merge_context_set ?loc ?(sideff=false) rigid evd ctx' =
-  {evd with universes = UState.merge ?loc sideff rigid evd.universes ctx'}
+  {evd with universes = UState.merge ?loc ~sideff ~extend:true rigid evd.universes ctx'}
 
 let merge_universe_subst evd subst = 
   {evd with universes = UState.merge_subst evd.universes subst }
@@ -790,26 +891,27 @@ let make_flexible_variable evd ~algebraic u =
   { evd with universes =
       UState.make_flexible_variable evd.universes ~algebraic u }
 
+let make_nonalgebraic_variable evd u =
+  { evd with universes = UState.make_nonalgebraic_variable evd.universes u }
+
 (****************************************)
 (* Operations on constants              *)
 (****************************************)
 
-let fresh_sort_in_family ?loc ?(rigid=univ_flexible) env evd s = 
-  with_context_set ?loc rigid evd (Universes.fresh_sort_in_family env s)
+let fresh_sort_in_family ?loc ?(rigid=univ_flexible) evd s =
+  with_context_set ?loc rigid evd (UnivGen.fresh_sort_in_family s)
 
 let fresh_constant_instance ?loc env evd c =
-  with_context_set ?loc univ_flexible evd (Universes.fresh_constant_instance env c)
+  with_context_set ?loc univ_flexible evd (UnivGen.fresh_constant_instance env c)
 
 let fresh_inductive_instance ?loc env evd i =
-  with_context_set ?loc univ_flexible evd (Universes.fresh_inductive_instance env i)
+  with_context_set ?loc univ_flexible evd (UnivGen.fresh_inductive_instance env i)
 
 let fresh_constructor_instance ?loc env evd c =
-  with_context_set ?loc univ_flexible evd (Universes.fresh_constructor_instance env c)
+  with_context_set ?loc univ_flexible evd (UnivGen.fresh_constructor_instance env c)
 
 let fresh_global ?loc ?(rigid=univ_flexible) ?names env evd gr =
-  with_context_set ?loc rigid evd (Universes.fresh_global_instance ?names env gr)
-
-let whd_sort_variable evd t = t
+  with_context_set ?loc rigid evd (UnivGen.fresh_global_instance ?loc ?names env gr)
 
 let is_sort_variable evd s = UState.is_sort_variable evd.universes s
 
@@ -833,18 +935,18 @@ let universe_rigidity evd l =
   else UnivRigid
 
 let normalize_universe evd =
-  let vars = ref (UState.subst evd.universes) in
-  let normalize = Universes.normalize_universe_opt_subst vars in
+  let vars = UState.subst evd.universes in
+  let normalize = UnivSubst.normalize_universe_opt_subst vars in
     normalize
 
 let normalize_universe_instance evd l =
-  let vars = ref (UState.subst evd.universes) in
-  let normalize = Universes.level_subst_of (Universes.normalize_univ_variable_opt_subst vars) in
+  let vars = UState.subst evd.universes in
+  let normalize = UnivSubst.level_subst_of (UnivSubst.normalize_univ_variable_opt_subst vars) in
     Univ.Instance.subst_fn normalize l
 
 let normalize_sort evars s =
   match s with
-  | Prop _ -> s
+  | Prop | Set -> s
   | Type u -> 
     let u' = normalize_universe evars u in
     if u' == u then s else Type u'
@@ -857,7 +959,7 @@ let set_eq_sort env d s1 s2 =
   | Some (u1, u2) ->
     if not (type_in_type env) then
       add_universe_constraints d
-        (Universes.Constraints.singleton (Universes.UEq (u1,u2)))
+        (UnivProblem.Set.singleton (UnivProblem.UEq (u1,u2)))
     else
       d
 
@@ -869,7 +971,7 @@ let set_leq_level d u1 u2 =
 
 let set_eq_instances ?(flex=false) d u1 u2 =
   add_universe_constraints d
-    (Universes.enforce_eq_instances_univs flex u1 u2 Universes.Constraints.empty)
+    (UnivProblem.enforce_eq_instances_univs flex u1 u2 UnivProblem.Set.empty)
 
 let set_leq_sort env evd s1 s2 =
   let s1 = normalize_sort evd s1 
@@ -878,7 +980,7 @@ let set_leq_sort env evd s1 s2 =
   | None -> evd
   | Some (u1, u2) ->
      if not (type_in_type env) then
-       add_universe_constraints evd (Universes.Constraints.singleton (Universes.ULe (u1,u2)))
+       add_universe_constraints evd (UnivProblem.Set.singleton (UnivProblem.ULe (u1,u2)))
      else evd
 	    
 let check_eq evd s s' =
@@ -887,6 +989,9 @@ let check_eq evd s s' =
 let check_leq evd s s' =
   UGraph.check_leq (UState.ugraph evd.universes) s s'
 
+let check_constraints evd csts =
+  UGraph.check_constraints csts (UState.ugraph evd.universes)
+
 let fix_undefined_variables evd =
   { evd with universes = UState.fix_undefined_variables evd.universes }
 
@@ -1007,6 +1112,7 @@ let set_metas evd metas = {
   universes  = evd.universes;
   conv_pbs = evd.conv_pbs;
   last_mods = evd.last_mods;
+  evar_flags = evd.evar_flags;
   metas;
   effects = evd.effects;
   evar_names = evd.evar_names;
@@ -1031,11 +1137,11 @@ let map_metas_fvalue f evd =
   | Clval(id,(c,s),typ) -> Clval(id,(mk_freelisted (f c.rebus),s),typ)
   | x -> x
   in
-  set_metas evd (Metamap.smartmap map evd.metas)
+  set_metas evd (Metamap.Smart.map map evd.metas)
 
 let map_metas f evd =
   let map cl = map_clb f cl in
-  set_metas evd (Metamap.smartmap map evd.metas)
+  set_metas evd (Metamap.Smart.map map evd.metas)
 
 let meta_opt_fvalue evd mv =
   match Metamap.find mv evd.metas with
@@ -1065,6 +1171,7 @@ let meta_ftype evd mv =
     | Clval(_,_,b) -> b
 
 let meta_type evd mv = (meta_ftype evd mv).rebus
+let meta_type0 = meta_type
 
 let meta_declare mv v ?(name=Anonymous) evd =
   let metas = Metamap.add mv (Cltyp(name,mk_freelisted v)) evd.metas in
@@ -1110,7 +1217,7 @@ let retract_coercible_metas evd =
     Cltyp (na, typ)
   | v -> v
   in
-  let metas = Metamap.smartmapi map evd.metas in
+  let metas = Metamap.Smart.mapi map evd.metas in
   !mc, set_metas evd metas
 
 let evar_source_of_meta mv evd =
@@ -1196,24 +1303,83 @@ module Monad =
 
 type unsolvability_explanation = SeveralInstancesFound of int
 
-(** Deprecated *)
-type evar_universe_context = UState.t
-let empty_evar_universe_context = UState.empty
-let union_evar_universe_context = UState.union
-let evar_universe_context_set = UState.context_set
-let evar_universe_context_constraints = UState.constraints
-let evar_context_universe_context = UState.context
-let evar_universe_context_of = UState.of_context_set
-let evar_universe_context_subst = UState.subst
-let add_constraints_context = UState.add_constraints
-let constrain_variables = UState.constrain_variables
-let evar_universe_context_of_binders = UState.of_binders
-let make_evar_universe_context e l =
-  let g = Environ.universes e in
-  match l with
-  | None -> UState.make g
-  | Some l -> UState.make_with_initial_binders g l
-let normalize_evar_universe_context_variables = UState.normalize_variables
-let abstract_undefined_variables = UState.abstract_undefined_variables
-let normalize_evar_universe_context = UState.minimize
-let nf_constraints = minimize_universes
+module MiniEConstr = struct
+
+  module ESorts =
+  struct
+    type t = Sorts.t
+    let make s = s
+    let kind sigma = function
+      | Sorts.Type u -> Sorts.sort_of_univ (normalize_universe sigma u)
+      | s -> s
+    let unsafe_to_sorts s = s
+  end
+
+  module EInstance =
+  struct
+    type t = Univ.Instance.t
+    let make i = i
+    let kind sigma i =
+      if Univ.Instance.is_empty i then i
+      else normalize_universe_instance sigma i
+    let empty = Univ.Instance.empty
+    let is_empty = Univ.Instance.is_empty
+    let unsafe_to_instance t = t
+  end
+
+  type t = econstr
+
+  let safe_evar_value sigma ev =
+    try Some (existential_value sigma ev)
+    with NotInstantiatedEvar | Not_found -> None
+
+  let rec whd_evar sigma c =
+    match Constr.kind c with
+    | Evar ev ->
+      begin match safe_evar_value sigma ev with
+        | Some c -> whd_evar sigma c
+        | None -> c
+      end
+    | App (f, args) when isEvar f ->
+      (** Enforce smart constructor invariant on applications *)
+      let ev = destEvar f in
+      begin match safe_evar_value sigma ev with
+        | None -> c
+        | Some f -> whd_evar sigma (mkApp (f, args))
+      end
+    | Cast (c0, k, t) when isEvar c0 ->
+      (** Enforce smart constructor invariant on casts. *)
+      let ev = destEvar c0 in
+      begin match safe_evar_value sigma ev with
+        | None -> c
+        | Some c -> whd_evar sigma (mkCast (c, k, t))
+      end
+    | _ -> c
+
+  let kind sigma c = Constr.kind (whd_evar sigma c)
+  let kind_upto = kind
+  let kind_of_type sigma c = Term.kind_of_type (whd_evar sigma c)
+  let of_kind = Constr.of_kind
+  let of_constr c = c
+  let of_constr_array v = v
+  let unsafe_to_constr c = c
+  let unsafe_to_constr_array v = v
+  let unsafe_eq = Refl
+
+  let to_constr ?(abort_on_undefined_evars=true) sigma c =
+    let evar_value =
+      if not abort_on_undefined_evars then fun ev -> safe_evar_value sigma ev
+      else fun ev ->
+        match safe_evar_value sigma ev with
+        | Some _ as v -> v
+        | None -> anomaly ~label:"econstr" Pp.(str "grounding a non evar-free term")
+    in
+    UnivSubst.nf_evars_and_universes_opt_subst evar_value (universe_subst sigma) c
+
+  let of_named_decl d = d
+  let unsafe_to_named_decl d = d
+  let of_rel_decl d = d
+  let unsafe_to_rel_decl d = d
+  let to_rel_decl sigma d = Context.Rel.Declaration.map_constr (to_constr sigma) d
+
+end