aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/engine.mllib7
-rw-r--r--engine/evd.ml1440
-rw-r--r--engine/evd.mli624
-rw-r--r--engine/logic_monad.ml384
-rw-r--r--engine/logic_monad.mli215
-rw-r--r--engine/namegen.ml395
-rw-r--r--engine/namegen.mli102
-rw-r--r--engine/proofview_monad.ml270
-rw-r--r--engine/proofview_monad.mli144
-rw-r--r--engine/sigma.ml105
-rw-r--r--engine/sigma.mli122
-rw-r--r--engine/termops.ml1026
-rw-r--r--engine/termops.mli248
-rw-r--r--engine/uState.ml475
-rw-r--r--engine/uState.mli117
15 files changed, 5674 insertions, 0 deletions
diff --git a/engine/engine.mllib b/engine/engine.mllib
new file mode 100644
index 000000000..7197a2583
--- /dev/null
+++ b/engine/engine.mllib
@@ -0,0 +1,7 @@
+Logic_monad
+Termops
+Namegen
+UState
+Evd
+Sigma
+Proofview_monad
diff --git a/engine/evd.ml b/engine/evd.ml
new file mode 100644
index 000000000..40409fe7f
--- /dev/null
+++ b/engine/evd.ml
@@ -0,0 +1,1440 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Pp
+open Errors
+open Util
+open Names
+open Nameops
+open Term
+open Vars
+open Termops
+open Environ
+open Globnames
+
+(** Generic filters *)
+module Filter :
+sig
+ type t
+ val equal : t -> t -> bool
+ val identity : t
+ val filter_list : t -> 'a list -> 'a list
+ val filter_array : t -> 'a array -> 'a array
+ val extend : int -> t -> t
+ val compose : t -> t -> t
+ val apply_subfilter : t -> bool list -> t
+ val restrict_upon : t -> int -> (int -> bool) -> t option
+ val map_along : (bool -> 'a -> bool) -> t -> 'a list -> t
+ val make : bool list -> t
+ val repr : t -> bool list option
+end =
+struct
+ type t = bool list option
+ (** We guarantee through the interface that if a filter is [Some _] then it
+ contains at least one [false] somewhere. *)
+
+ let identity = None
+
+ let rec equal l1 l2 = match l1, l2 with
+ | [], [] -> true
+ | h1 :: l1, h2 :: l2 ->
+ (if h1 then h2 else not h2) && equal l1 l2
+ | _ -> false
+
+ let equal l1 l2 = match l1, l2 with
+ | None, None -> true
+ | Some _, None | None, Some _ -> false
+ | Some l1, Some l2 -> equal l1 l2
+
+ let rec is_identity = function
+ | [] -> true
+ | true :: l -> is_identity l
+ | false :: _ -> false
+
+ let normalize f = if is_identity f then None else Some f
+
+ let filter_list f l = match f with
+ | None -> l
+ | Some f -> CList.filter_with f l
+
+ let filter_array f v = match f with
+ | None -> v
+ | Some f -> CArray.filter_with f v
+
+ let rec extend n l =
+ if n = 0 then l
+ else extend (pred n) (true :: l)
+
+ let extend n = function
+ | None -> None
+ | Some f -> Some (extend n f)
+
+ let compose f1 f2 = match f1 with
+ | None -> f2
+ | Some f1 ->
+ match f2 with
+ | None -> None
+ | Some f2 -> normalize (CList.filter_with f1 f2)
+
+ let apply_subfilter_array filter subfilter =
+ (** In both cases we statically know that the argument will contain at
+ least one [false] *)
+ match filter with
+ | None -> Some (Array.to_list subfilter)
+ | Some f ->
+ let len = Array.length subfilter in
+ let fold b (i, ans) =
+ if b then
+ let () = assert (0 <= i) in
+ (pred i, Array.unsafe_get subfilter i :: ans)
+ else
+ (i, false :: ans)
+ in
+ Some (snd (List.fold_right fold f (pred len, [])))
+
+ let apply_subfilter filter subfilter =
+ apply_subfilter_array filter (Array.of_list subfilter)
+
+ let restrict_upon f len p =
+ let newfilter = Array.init len p in
+ if Array.for_all (fun id -> id) newfilter then None
+ else
+ Some (apply_subfilter_array f newfilter)
+
+ let map_along f flt l =
+ let ans = match flt with
+ | None -> List.map (fun x -> f true x) l
+ | Some flt -> List.map2 f flt l
+ in
+ normalize ans
+
+ let make l = normalize l
+
+ let repr f = f
+
+end
+
+(* The kinds of existential variables are now defined in [Evar_kinds] *)
+
+(* The type of mappings for existential variables *)
+
+module Dummy = struct end
+module Store = Store.Make(Dummy)
+
+type evar = Term.existential_key
+
+let string_of_existential evk = "?X" ^ string_of_int (Evar.repr evk)
+
+type evar_body =
+ | Evar_empty
+ | Evar_defined of constr
+
+type evar_info = {
+ evar_concl : constr;
+ evar_hyps : named_context_val;
+ 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 }
+
+let make_evar hyps ccl = {
+ evar_concl = ccl;
+ evar_hyps = hyps;
+ evar_body = Evar_empty;
+ evar_filter = Filter.identity;
+ evar_source = (Loc.ghost,Evar_kinds.InternalHole);
+ evar_candidates = None;
+ evar_extra = Store.empty
+}
+
+let instance_mismatch () =
+ anomaly (Pp.str "Signature and its instance do not match")
+
+let evar_concl evi = evi.evar_concl
+
+let evar_filter evi = evi.evar_filter
+
+let evar_body evi = evi.evar_body
+
+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_hyps evi = evi.evar_hyps
+
+let evar_filtered_hyps evi = match Filter.repr (evar_filter evi) with
+| None -> evar_hyps evi
+| Some filter ->
+ let rec make_hyps filter ctxt = match filter, ctxt with
+ | [], [] -> empty_named_context_val
+ | false :: filter, _ :: ctxt -> make_hyps filter ctxt
+ | true :: filter, decl :: ctxt ->
+ let hyps = make_hyps filter ctxt in
+ push_named_context_val decl hyps
+ | _ -> instance_mismatch ()
+ in
+ make_hyps filter (evar_context evi)
+
+let evar_env evi = Global.env_of_context evi.evar_hyps
+
+let evar_filtered_env evi = match Filter.repr (evar_filter evi) with
+| None -> evar_env evi
+| Some filter ->
+ let rec make_env filter ctxt = match filter, ctxt with
+ | [], [] -> reset_context (Global.env ())
+ | false :: filter, _ :: ctxt -> make_env filter ctxt
+ | true :: filter, decl :: ctxt ->
+ let env = make_env filter ctxt in
+ push_named decl env
+ | _ -> instance_mismatch ()
+ in
+ make_env filter (evar_context evi)
+
+let map_evar_body f = function
+ | Evar_empty -> Evar_empty
+ | Evar_defined d -> Evar_defined (f d)
+
+let map_evar_info f evi =
+ {evi with
+ evar_body = map_evar_body f evi.evar_body;
+ evar_hyps = map_named_val f evi.evar_hyps;
+ evar_concl = f evi.evar_concl;
+ evar_candidates = Option.map (List.map f) evi.evar_candidates }
+
+let evar_ident_info evi =
+ match evi.evar_source with
+ | _,Evar_kinds.ImplicitArg (c,(n,Some id),b) -> id
+ | _,Evar_kinds.VarInstance id -> id
+ | _,Evar_kinds.GoalEvar -> Id.of_string "Goal"
+ | _ ->
+ let env = reset_with_named_context evi.evar_hyps (Global.env()) in
+ Namegen.id_of_name_using_hdchar env evi.evar_concl Anonymous
+
+(* This exception is raised by *.existential_value *)
+exception NotInstantiatedEvar
+
+(* Note: let-in contributes to the instance *)
+
+let evar_instance_array test_id info args =
+ let len = Array.length args in
+ let rec instrec filter ctxt i = match filter, ctxt with
+ | [], [] ->
+ if Int.equal i len then []
+ else instance_mismatch ()
+ | false :: filter, _ :: ctxt ->
+ instrec filter ctxt i
+ | true :: filter, (id,_,_ as d) :: ctxt ->
+ if i < len then
+ let c = Array.unsafe_get args i in
+ if test_id d c then instrec filter ctxt (succ i)
+ else (id, c) :: instrec filter ctxt (succ i)
+ else instance_mismatch ()
+ | _ -> instance_mismatch ()
+ in
+ match Filter.repr (evar_filter info) with
+ | None ->
+ let map i (id,_,_ as d) =
+ if (i < len) then
+ let c = Array.unsafe_get args i in
+ if test_id d c then None else Some (id,c)
+ else instance_mismatch ()
+ in
+ List.map_filter_i map (evar_context info)
+ | Some filter ->
+ instrec filter (evar_context info) 0
+
+let make_evar_instance_array info args =
+ evar_instance_array (fun (id,_,_) -> isVarId id) info args
+
+let instantiate_evar_array info c args =
+ let inst = make_evar_instance_array info args in
+ match inst with
+ | [] -> c
+ | _ -> replace_vars inst c
+
+type evar_universe_context = UState.t
+type 'a in_evar_universe_context = 'a * evar_universe_context
+
+let empty_evar_universe_context = UState.empty
+let is_empty_evar_universe_context = UState.is_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 add_universe_constraints_context = UState.add_universe_constraints
+let constrain_variables = UState.constrain_variables
+let evar_universe_context_of_binders = UState.of_binders
+
+(* let addunivconstrkey = Profile.declare_profile "add_universe_constraints_context";; *)
+(* let add_universe_constraints_context = *)
+(* Profile.profile2 addunivconstrkey add_universe_constraints_context;; *)
+(*******************************************************************)
+(* Metamaps *)
+
+(*******************************************************************)
+(* Constraints for existential variables *)
+(*******************************************************************)
+
+type 'a freelisted = {
+ rebus : 'a;
+ freemetas : Int.Set.t }
+
+(* Collects all metavars appearing in a constr *)
+let metavars_of c =
+ let rec collrec acc c =
+ match kind_of_term c with
+ | Meta mv -> Int.Set.add mv acc
+ | _ -> fold_constr collrec acc c
+ in
+ collrec Int.Set.empty c
+
+let mk_freelisted c =
+ { rebus = c; freemetas = metavars_of c }
+
+let map_fl f cfl = { cfl with rebus=f cfl.rebus }
+
+(* Status of an instance found by unification wrt to the meta it solves:
+ - a supertype of the meta (e.g. the solution to ?X <= T is a supertype of ?X)
+ - a subtype of the meta (e.g. the solution to T <= ?X is a supertype of ?X)
+ - a term that can be eta-expanded n times while still being a solution
+ (e.g. the solution [P] to [?X u v = P u v] can be eta-expanded twice)
+*)
+
+type instance_constraint = IsSuperType | IsSubType | Conv
+
+let eq_instance_constraint c1 c2 = c1 == c2
+
+(* Status of the unification of the type of an instance against the type of
+ the meta it instantiates:
+ - CoerceToType means that the unification of types has not been done
+ and that a coercion can still be inserted: the meta should not be
+ substituted freely (this happens for instance given via the
+ "with" binding clause).
+ - TypeProcessed means that the information obtainable from the
+ unification of types has been extracted.
+ - TypeNotProcessed means that the unification of types has not been
+ done but it is known that no coercion may be inserted: the meta
+ can be substituted freely.
+*)
+
+type instance_typing_status =
+ CoerceToType | TypeNotProcessed | TypeProcessed
+
+(* Status of an instance together with the status of its type unification *)
+
+type instance_status = instance_constraint * instance_typing_status
+
+(* Clausal environments *)
+
+type clbinding =
+ | Cltyp of Name.t * constr freelisted
+ | Clval of Name.t * (constr freelisted * instance_status) * constr freelisted
+
+let map_clb f = function
+ | Cltyp (na,cfl) -> Cltyp (na,map_fl f cfl)
+ | Clval (na,(cfl1,pb),cfl2) -> Clval (na,(map_fl f cfl1,pb),map_fl f cfl2)
+
+(* name of defined is erased (but it is pretty-printed) *)
+let clb_name = function
+ Cltyp(na,_) -> (na,false)
+ | Clval (na,_,_) -> (na,true)
+
+(***********************)
+
+module Metaset = Int.Set
+
+module Metamap = Int.Map
+
+let metamap_to_list m =
+ Metamap.fold (fun n v l -> (n,v)::l) m []
+
+(*************************)
+(* Unification state *)
+
+type conv_pb = Reduction.conv_pb
+type evar_constraint = conv_pb * Environ.env * constr * constr
+
+module EvMap = Evar.Map
+
+type evar_map = {
+ (** Existential variables *)
+ defn_evars : evar_info EvMap.t;
+ undf_evars : evar_info EvMap.t;
+ evar_names : Id.t EvMap.t * existential_key Idmap.t;
+ (** Universes *)
+ universes : evar_universe_context;
+ (** Conversion problems *)
+ conv_pbs : evar_constraint list;
+ last_mods : Evar.Set.t;
+ (** Metas *)
+ metas : clbinding Metamap.t;
+ (** Interactive proofs *)
+ effects : Safe_typing.private_constants;
+ future_goals : Evar.t list; (** list of newly created evars, to be
+ eventually turned into goals if not solved.*)
+ principal_future_goal : Evar.t option; (** if [Some e], [e] must be
+ contained
+ [future_goals]. The evar
+ [e] will inherit
+ properties (now: the
+ name) of the evar which
+ will be instantiated with
+ a term containing [e]. *)
+ extras : Store.t;
+}
+
+(*** Lifting primitive from Evar.Map. ***)
+
+let add_name_newly_undefined naming evk evi (evtoid,idtoev) =
+ let id = match naming with
+ | Misctypes.IntroAnonymous ->
+ let id = evar_ident_info evi in
+ Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev)
+ | Misctypes.IntroIdentifier id ->
+ let id' =
+ Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev) in
+ if not (Names.Id.equal id id') then
+ user_err_loc
+ (Loc.ghost,"",str "Already an existential evar of name " ++ pr_id id);
+ id'
+ | Misctypes.IntroFresh id ->
+ Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev) in
+ (EvMap.add evk id evtoid, Idmap.add id evk idtoev)
+
+let add_name_undefined naming evk evi (evtoid,idtoev as evar_names) =
+ if EvMap.mem evk evtoid then
+ evar_names
+ else
+ add_name_newly_undefined naming evk evi evar_names
+
+let remove_name_defined evk (evtoid,idtoev) =
+ let id = EvMap.find evk evtoid in
+ (EvMap.remove evk evtoid, Idmap.remove id idtoev)
+
+let remove_name_possibly_already_defined evk evar_names =
+ try remove_name_defined evk evar_names
+ with Not_found -> evar_names
+
+let rename evk id evd =
+ let (evtoid,idtoev) = evd.evar_names in
+ let id' = EvMap.find evk evtoid in
+ if Idmap.mem id idtoev then anomaly (str "Evar name already in use");
+ { evd with evar_names =
+ (EvMap.add evk id evtoid (* overwrite old name *),
+ Idmap.add id evk (Idmap.remove id' idtoev)) }
+
+let reassign_name_defined evk evk' (evtoid,idtoev) =
+ let id = EvMap.find evk evtoid in
+ (EvMap.add evk' id (EvMap.remove evk evtoid),
+ Idmap.add id evk' (Idmap.remove id idtoev))
+
+let add_with_name ?(naming = Misctypes.IntroAnonymous) d e i = match i.evar_body with
+| Evar_empty ->
+ let evar_names = add_name_undefined naming e i d.evar_names in
+ { d with undf_evars = EvMap.add e i d.undf_evars; evar_names }
+| Evar_defined _ ->
+ let evar_names = remove_name_possibly_already_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
+
+(** New evars *)
+
+let evar_counter_summary_name = "evar counter"
+
+(* Generator of existential names *)
+let new_untyped_evar =
+ let evar_ctr = Summary.ref 0 ~name:evar_counter_summary_name in
+ fun () -> incr evar_ctr; Evar.unsafe_of_int !evar_ctr
+
+let new_evar evd ?naming evi =
+ let evk = new_untyped_evar () in
+ let evd = add_with_name evd ?naming evk evi in
+ (evd, evk)
+
+let remove d e =
+ let undf_evars = EvMap.remove e d.undf_evars in
+ let defn_evars = EvMap.remove e d.defn_evars in
+ { d with undf_evars; defn_evars; }
+
+let find d e =
+ try EvMap.find e d.undf_evars
+ with Not_found -> EvMap.find e d.defn_evars
+
+let find_undefined d e = EvMap.find e d.undf_evars
+
+let mem d e = EvMap.mem e d.undf_evars || EvMap.mem e d.defn_evars
+
+(* spiwack: this function loses information from the original evar_map
+ it might be an idea not to export it. *)
+let to_list d =
+ (* Workaround for change in Map.fold behavior in ocaml 3.08.4 *)
+ let l = ref [] in
+ EvMap.iter (fun evk x -> l := (evk,x)::!l) d.defn_evars;
+ EvMap.iter (fun evk x -> l := (evk,x)::!l) d.undf_evars;
+ !l
+
+let undefined_map d = d.undf_evars
+
+let drop_all_defined d = { d with defn_evars = EvMap.empty }
+
+(* spiwack: not clear what folding over an evar_map, for now we shall
+ simply fold over the inner evar_map. *)
+let fold f d a =
+ EvMap.fold f d.defn_evars (EvMap.fold f d.undf_evars a)
+
+let fold_undefined f d a = EvMap.fold f d.undf_evars a
+
+let raw_map f d =
+ let f evk info =
+ let ans = f evk info in
+ let () = match info.evar_body, ans.evar_body with
+ | Evar_defined _, Evar_empty
+ | Evar_empty, Evar_defined _ ->
+ anomaly (str "Unrespectful mapping function.")
+ | _ -> ()
+ in
+ ans
+ in
+ let defn_evars = EvMap.smartmapi f d.defn_evars in
+ let undf_evars = EvMap.smartmapi f d.undf_evars in
+ { d with defn_evars; undf_evars; }
+
+let raw_map_undefined f d =
+ let f evk info =
+ let ans = f evk info in
+ let () = match ans.evar_body with
+ | Evar_defined _ ->
+ anomaly (str "Unrespectful mapping function.")
+ | _ -> ()
+ in
+ ans
+ in
+ { d with undf_evars = EvMap.smartmapi f d.undf_evars; }
+
+let is_evar = mem
+
+let is_defined d e = EvMap.mem e d.defn_evars
+
+let is_undefined d e = EvMap.mem e d.undf_evars
+
+let existential_value d (n, args) =
+ let info = find d n in
+ match evar_body info with
+ | Evar_defined c ->
+ instantiate_evar_array info c args
+ | Evar_empty ->
+ raise NotInstantiatedEvar
+
+let existential_opt_value d ev =
+ try Some (existential_value d ev)
+ with NotInstantiatedEvar -> None
+
+let existential_type d (n, args) =
+ let info =
+ try find d n
+ with Not_found ->
+ anomaly (str "Evar " ++ str (string_of_existential n) ++ str " was not declared") in
+ instantiate_evar_array info info.evar_concl args
+
+let add_constraints d c =
+ { d with universes = add_constraints_context d.universes c }
+
+let add_universe_constraints d c =
+ { d with universes = add_universe_constraints_context d.universes c }
+
+(*** /Lifting... ***)
+
+(* evar_map are considered empty disregarding histories *)
+let is_empty d =
+ EvMap.is_empty d.defn_evars &&
+ EvMap.is_empty d.undf_evars &&
+ List.is_empty d.conv_pbs &&
+ Metamap.is_empty d.metas
+
+let cmap f evd =
+ { evd with
+ metas = Metamap.map (map_clb f) evd.metas;
+ defn_evars = EvMap.map (map_evar_info f) evd.defn_evars;
+ undf_evars = EvMap.map (map_evar_info f) evd.undf_evars
+ }
+
+(* spiwack: deprecated *)
+let create_evar_defs sigma = { sigma with
+ conv_pbs=[]; last_mods=Evar.Set.empty; metas=Metamap.empty }
+
+let empty = {
+ defn_evars = EvMap.empty;
+ undf_evars = EvMap.empty;
+ universes = empty_evar_universe_context;
+ conv_pbs = [];
+ last_mods = Evar.Set.empty;
+ metas = Metamap.empty;
+ effects = Safe_typing.empty_private_constants;
+ evar_names = (EvMap.empty,Idmap.empty); (* id<->key for undefined evars *)
+ future_goals = [];
+ principal_future_goal = None;
+ extras = Store.empty;
+}
+
+let from_env e =
+ { empty with universes = UState.make (Environ.universes e) }
+
+let from_ctx ctx = { empty with universes = ctx }
+
+let has_undefined evd = not (EvMap.is_empty evd.undf_evars)
+
+let evars_reset_evd ?(with_conv_pbs=false) ?(with_univs=true) evd d =
+ let conv_pbs = if with_conv_pbs then evd.conv_pbs else d.conv_pbs in
+ let last_mods = if with_conv_pbs then evd.last_mods else d.last_mods in
+ let universes =
+ if not with_univs then evd.universes
+ else union_evar_universe_context evd.universes d.universes
+ in
+ { evd with
+ metas = d.metas;
+ last_mods; conv_pbs; universes }
+
+let merge_universe_context evd uctx' =
+ { evd with universes = union_evar_universe_context evd.universes uctx' }
+
+let set_universe_context evd uctx' =
+ { evd with universes = uctx' }
+
+let add_conv_pb ?(tail=false) pb d =
+ if tail then {d with conv_pbs = d.conv_pbs @ [pb]}
+ else {d with conv_pbs = pb::d.conv_pbs}
+
+let evar_source evk d = (find d evk).evar_source
+
+let evar_ident evk evd =
+ try EvMap.find evk (fst evd.evar_names)
+ with Not_found ->
+ (* Unnamed (non-dependent) evar *)
+ add_suffix (Id.of_string "X") (string_of_int (Evar.repr evk))
+
+let evar_key id evd =
+ Idmap.find id (snd evd.evar_names)
+
+let define_aux def undef evk body =
+ let oldinfo =
+ try EvMap.find evk undef
+ with Not_found ->
+ if EvMap.mem evk def then
+ anomaly ~label:"Evd.define" (Pp.str "cannot define an evar twice")
+ else
+ anomaly ~label:"Evd.define" (Pp.str "cannot define undeclared evar")
+ in
+ let () = assert (oldinfo.evar_body == Evar_empty) 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 (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 = remove_name_defined evk evd.evar_names in
+ { evd with defn_evars; undf_evars; last_mods; evar_names }
+
+let restrict evk filter ?candidates evd =
+ let evk' = new_untyped_evar () in
+ let evar_info = EvMap.find evk evd.undf_evars in
+ let evar_info' =
+ { evar_info with evar_filter = filter;
+ evar_candidates = candidates;
+ evar_extra = Store.empty } in
+ let evar_names = reassign_name_defined evk evk' evd.evar_names in
+ let ctxt = Filter.filter_list filter (evar_context evar_info) in
+ let id_inst = Array.map_of_list (fun (id,_,_) -> mkVar id) ctxt in
+ let body = mkEvar(evk',id_inst) in
+ let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
+ { evd with undf_evars = EvMap.add evk' evar_info' undf_evars;
+ defn_evars; evar_names }, evk'
+
+let downcast evk ccl evd =
+ let evar_info = EvMap.find evk evd.undf_evars in
+ let evar_info' = { evar_info with evar_concl = ccl } in
+ { evd with undf_evars = EvMap.add evk evar_info' evd.undf_evars }
+
+(* extracts conversion problems that satisfy predicate p *)
+(* Note: conv_pbs not satisying p are stored back in reverse order *)
+let extract_conv_pbs evd p =
+ let (pbs,pbs1) =
+ List.fold_left
+ (fun (pbs,pbs1) pb ->
+ if p pb then
+ (pb::pbs,pbs1)
+ else
+ (pbs,pb::pbs1))
+ ([],[])
+ evd.conv_pbs
+ in
+ {evd with conv_pbs = pbs1; last_mods = Evar.Set.empty},
+ pbs
+
+let extract_changed_conv_pbs evd p =
+ extract_conv_pbs evd (fun pb -> p evd.last_mods pb)
+
+let extract_all_conv_pbs evd =
+ extract_conv_pbs evd (fun _ -> true)
+
+let loc_of_conv_pb evd (pbty,env,t1,t2) =
+ match kind_of_term (fst (decompose_app t1)) with
+ | Evar (evk1,_) -> fst (evar_source evk1 evd)
+ | _ ->
+ match kind_of_term (fst (decompose_app t2)) with
+ | Evar (evk2,_) -> fst (evar_source evk2 evd)
+ | _ -> Loc.ghost
+
+(** The following functions return the set of evars immediately
+ contained in the object *)
+
+(* excluding defined evars *)
+
+let evar_list c =
+ let rec evrec acc c =
+ match kind_of_term c with
+ | Evar (evk, _ as ev) -> ev :: acc
+ | _ -> fold_constr evrec acc c in
+ evrec [] c
+
+let evars_of_term c =
+ let rec evrec acc c =
+ match kind_of_term c with
+ | Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l)
+ | _ -> fold_constr evrec acc c
+ in
+ evrec Evar.Set.empty c
+
+let evars_of_named_context nc =
+ List.fold_right (fun (_, b, t) s ->
+ Option.fold_left (fun s t ->
+ Evar.Set.union s (evars_of_term t))
+ (Evar.Set.union s (evars_of_term t)) b)
+ nc Evar.Set.empty
+
+let evars_of_filtered_evar_info evi =
+ Evar.Set.union (evars_of_term evi.evar_concl)
+ (Evar.Set.union
+ (match evi.evar_body with
+ | Evar_empty -> Evar.Set.empty
+ | Evar_defined b -> evars_of_term b)
+ (evars_of_named_context (evar_filtered_context evi)))
+
+(**********************************************************)
+(* Sort variables *)
+
+type rigid = UState.rigid =
+ | UnivRigid
+ | UnivFlexible of bool (** Is substitution by an algebraic ok? *)
+
+let univ_rigid = UnivRigid
+let univ_flexible = UnivFlexible false
+let univ_flexible_alg = UnivFlexible true
+
+let evar_universe_context d = d.universes
+
+let universe_context_set d = UState.context_set d.universes
+
+let pr_uctx_level = UState.pr_uctx_level
+let universe_context ?names evd = UState.universe_context ?names evd.universes
+
+let restrict_universe_context evd vars =
+ { evd with universes = UState.restrict evd.universes vars }
+
+let universe_subst evd =
+ UState.subst evd.universes
+
+let merge_context_set ?(sideff=false) rigid evd ctx' =
+ {evd with universes = UState.merge sideff rigid evd.universes ctx'}
+
+let merge_universe_subst evd subst =
+ {evd with universes = UState.merge_subst evd.universes subst }
+
+let with_context_set rigid d (a, ctx) =
+ (merge_context_set rigid d ctx, a)
+
+let new_univ_level_variable ?name ?(predicative=true) rigid evd =
+ let uctx', u = UState.new_univ_variable rigid name evd.universes in
+ ({evd with universes = uctx'}, u)
+
+let new_univ_variable ?name ?(predicative=true) rigid evd =
+ let uctx', u = UState.new_univ_variable rigid name evd.universes in
+ ({evd with universes = uctx'}, Univ.Universe.make u)
+
+let new_sort_variable ?name ?(predicative=true) rigid d =
+ let (d', u) = new_univ_variable rigid ?name ~predicative d in
+ (d', Type u)
+
+let add_global_univ d u =
+ { d with universes = UState.add_global_univ d.universes u }
+
+let make_flexible_variable evd b u =
+ { evd with universes = UState.make_flexible_variable evd.universes b u }
+
+let make_evar_universe_context e l =
+ let uctx = UState.make (Environ.universes e) in
+ match l with
+ | None -> uctx
+ | Some us ->
+ List.fold_left
+ (fun uctx (loc,id) ->
+ fst (UState.new_univ_variable univ_rigid (Some (Id.to_string id)) uctx))
+ uctx us
+
+(****************************************)
+(* Operations on constants *)
+(****************************************)
+
+let fresh_sort_in_family ?(rigid=univ_flexible) env evd s =
+ with_context_set rigid evd (Universes.fresh_sort_in_family env s)
+
+let fresh_constant_instance env evd c =
+ with_context_set univ_flexible evd (Universes.fresh_constant_instance env c)
+
+let fresh_inductive_instance env evd i =
+ with_context_set univ_flexible evd (Universes.fresh_inductive_instance env i)
+
+let fresh_constructor_instance env evd c =
+ with_context_set univ_flexible evd (Universes.fresh_constructor_instance env c)
+
+let fresh_global ?(rigid=univ_flexible) ?names env evd gr =
+ with_context_set rigid evd (Universes.fresh_global_instance ?names env gr)
+
+let whd_sort_variable evd t = t
+
+let is_sort_variable evd s = UState.is_sort_variable evd.universes s
+
+let is_flexible_level evd l =
+ let uctx = evd.universes in
+ Univ.LMap.mem l (UState.subst uctx)
+
+let is_eq_sort s1 s2 =
+ if Sorts.equal s1 s2 then None
+ else
+ let u1 = univ_of_sort s1
+ and u2 = univ_of_sort s2 in
+ if Univ.Universe.equal u1 u2 then None
+ else Some (u1, u2)
+
+let normalize_universe evd =
+ let vars = ref (UState.subst evd.universes) in
+ let normalize = Universes.normalize_universe_opt_subst vars in
+ normalize
+
+let normalize_universe_instance evd l =
+ let vars = ref (UState.subst evd.universes) in
+ let normalize = Univ.level_subst_of (Universes.normalize_univ_variable_opt_subst vars) in
+ Univ.Instance.subst_fn normalize l
+
+let normalize_sort evars s =
+ match s with
+ | Prop _ -> s
+ | Type u ->
+ let u' = normalize_universe evars u in
+ if u' == u then s else Type u'
+
+(* FIXME inefficient *)
+let set_eq_sort env d s1 s2 =
+ let s1 = normalize_sort d s1 and s2 = normalize_sort d s2 in
+ match is_eq_sort s1 s2 with
+ | None -> d
+ | Some (u1, u2) ->
+ if not (type_in_type env) then
+ add_universe_constraints d
+ (Universes.Constraints.singleton (u1,Universes.UEq,u2))
+ else
+ d
+
+let has_lub evd u1 u2 =
+ (* let normalize = Universes.normalize_universe_opt_subst (ref univs.uctx_univ_variables) in *)
+ (* (\* let dref, norm = memo_normalize_universe d in *\) *)
+ (* let u1 = normalize u1 and u2 = normalize u2 in *)
+ if Univ.Universe.equal u1 u2 then evd
+ else add_universe_constraints evd
+ (Universes.Constraints.singleton (u1,Universes.ULub,u2))
+
+let set_eq_level d u1 u2 =
+ add_constraints d (Univ.enforce_eq_level u1 u2 Univ.Constraint.empty)
+
+let set_leq_level d u1 u2 =
+ add_constraints d (Univ.enforce_leq_level u1 u2 Univ.Constraint.empty)
+
+let set_eq_instances ?(flex=false) d u1 u2 =
+ add_universe_constraints d
+ (Universes.enforce_eq_instances_univs flex u1 u2 Universes.Constraints.empty)
+
+let set_leq_sort env evd s1 s2 =
+ let s1 = normalize_sort evd s1
+ and s2 = normalize_sort evd s2 in
+ match is_eq_sort s1 s2 with
+ | None -> evd
+ | Some (u1, u2) ->
+ (* if Univ.is_type0_univ u2 then *)
+ (* if Univ.is_small_univ u1 then evd *)
+ (* else raise (Univ.UniverseInconsistency (Univ.Le, u1, u2, [])) *)
+ (* else if Univ.is_type0m_univ u2 then *)
+ (* raise (Univ.UniverseInconsistency (Univ.Le, u1, u2, [])) *)
+ (* else *)
+ if not (type_in_type env) then
+ add_universe_constraints evd (Universes.Constraints.singleton (u1,Universes.ULe,u2))
+ else evd
+
+let check_eq evd s s' =
+ UGraph.check_eq (UState.ugraph evd.universes) s s'
+
+let check_leq evd s s' =
+ UGraph.check_leq (UState.ugraph evd.universes) s s'
+
+let normalize_evar_universe_context_variables = UState.normalize_variables
+
+(* let normvarsconstrkey = Profile.declare_profile "normalize_evar_universe_context_variables";; *)
+(* let normalize_evar_universe_context_variables = *)
+(* Profile.profile1 normvarsconstrkey normalize_evar_universe_context_variables;; *)
+
+let abstract_undefined_variables = UState.abstract_undefined_variables
+
+let fix_undefined_variables evd =
+ { evd with universes = UState.fix_undefined_variables evd.universes }
+
+let refresh_undefined_universes evd =
+ let uctx', subst = UState.refresh_undefined_univ_variables evd.universes in
+ let evd' = cmap (subst_univs_level_constr subst) {evd with universes = uctx'} in
+ evd', subst
+
+let normalize_evar_universe_context = UState.normalize
+
+let nf_univ_variables evd =
+ let subst, uctx' = normalize_evar_universe_context_variables evd.universes in
+ let evd' = {evd with universes = uctx'} in
+ evd', subst
+
+let nf_constraints evd =
+ let subst, uctx' = normalize_evar_universe_context_variables evd.universes in
+ let uctx' = normalize_evar_universe_context uctx' in
+ {evd with universes = uctx'}
+
+let nf_constraints =
+ if Flags.profile then
+ let nfconstrkey = Profile.declare_profile "nf_constraints" in
+ Profile.profile1 nfconstrkey nf_constraints
+ else nf_constraints
+
+let universe_of_name evd s = UState.universe_of_name evd.universes s
+
+let add_universe_name evd s l =
+ { evd with universes = UState.add_universe_name evd.universes s l }
+
+let universes evd = UState.ugraph evd.universes
+
+let update_sigma_env evd env =
+ { evd with universes = UState.update_sigma_env evd.universes env }
+
+(* Conversion w.r.t. an evar map and its local universes. *)
+
+let conversion_gen env evd pb t u =
+ match pb with
+ | Reduction.CONV ->
+ Reduction.trans_conv_universes
+ full_transparent_state ~evars:(existential_opt_value evd) env
+ (UState.ugraph evd.universes) t u
+ | Reduction.CUMUL -> Reduction.trans_conv_leq_universes
+ full_transparent_state ~evars:(existential_opt_value evd) env
+ (UState.ugraph evd.universes) t u
+
+(* let conversion_gen_key = Profile.declare_profile "conversion_gen" *)
+(* let conversion_gen = Profile.profile5 conversion_gen_key conversion_gen *)
+
+let conversion env d pb t u =
+ conversion_gen env d pb t u; d
+
+let test_conversion env d pb t u =
+ try conversion_gen env d pb t u; true
+ with _ -> false
+
+exception UniversesDiffer = UState.UniversesDiffer
+
+let eq_constr_univs evd t u =
+ let b, c = Universes.eq_constr_univs_infer (UState.ugraph evd.universes) t u in
+ if b then
+ try let evd' = add_universe_constraints evd c in evd', b
+ with Univ.UniverseInconsistency _ | UniversesDiffer -> evd, false
+ else evd, b
+
+let e_eq_constr_univs evdref t u =
+ let evd, b = eq_constr_univs !evdref t u in
+ evdref := evd; b
+
+(**********************************************************)
+(* Side effects *)
+
+let emit_side_effects eff evd =
+ { evd with effects = Safe_typing.concat_private eff evd.effects;
+ universes = UState.emit_side_effects eff evd.universes }
+
+let drop_side_effects evd =
+ { evd with effects = Safe_typing.empty_private_constants; }
+
+let eval_side_effects evd = evd.effects
+
+(* Future goals *)
+let declare_future_goal evk evd =
+ { evd with future_goals = evk::evd.future_goals }
+
+let declare_principal_goal evk evd =
+ match evd.principal_future_goal with
+ | None -> { evd with
+ future_goals = evk::evd.future_goals;
+ principal_future_goal=Some evk; }
+ | Some _ -> Errors.error "Only one main subgoal per instantiation."
+
+let future_goals evd = evd.future_goals
+
+let principal_future_goal evd = evd.principal_future_goal
+
+let reset_future_goals evd =
+ { evd with future_goals = [] ; principal_future_goal=None }
+
+let restore_future_goals evd gls pgl =
+ { evd with future_goals = gls ; principal_future_goal = pgl }
+
+(**********************************************************)
+(* Accessing metas *)
+
+(** We use this function to overcome OCaml compiler limitations and to prevent
+ the use of costly in-place modifications. *)
+let set_metas evd metas = {
+ defn_evars = evd.defn_evars;
+ undf_evars = evd.undf_evars;
+ universes = evd.universes;
+ conv_pbs = evd.conv_pbs;
+ last_mods = evd.last_mods;
+ metas;
+ effects = evd.effects;
+ evar_names = evd.evar_names;
+ future_goals = evd.future_goals;
+ principal_future_goal = evd.principal_future_goal;
+ extras = evd.extras;
+}
+
+let meta_list evd = metamap_to_list evd.metas
+
+let undefined_metas evd =
+ let filter = function
+ | (n,Clval(_,_,typ)) -> None
+ | (n,Cltyp (_,typ)) -> Some n
+ in
+ let m = List.map_filter filter (meta_list evd) in
+ List.sort Int.compare m
+
+let map_metas_fvalue f evd =
+ let map = function
+ | 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)
+
+let meta_opt_fvalue evd mv =
+ match Metamap.find mv evd.metas with
+ | Clval(_,b,_) -> Some b
+ | Cltyp _ -> None
+
+let meta_defined evd mv =
+ match Metamap.find mv evd.metas with
+ | Clval _ -> true
+ | Cltyp _ -> false
+
+let try_meta_fvalue evd mv =
+ match Metamap.find mv evd.metas with
+ | Clval(_,b,_) -> b
+ | Cltyp _ -> raise Not_found
+
+let meta_fvalue evd mv =
+ try try_meta_fvalue evd mv
+ with Not_found -> anomaly ~label:"meta_fvalue" (Pp.str "meta has no value")
+
+let meta_value evd mv =
+ (fst (try_meta_fvalue evd mv)).rebus
+
+let meta_ftype evd mv =
+ match Metamap.find mv evd.metas with
+ | Cltyp (_,b) -> b
+ | Clval(_,_,b) -> b
+
+let meta_type evd mv = (meta_ftype evd mv).rebus
+
+let meta_declare mv v ?(name=Anonymous) evd =
+ let metas = Metamap.add mv (Cltyp(name,mk_freelisted v)) evd.metas in
+ set_metas evd metas
+
+let meta_assign mv (v, pb) evd =
+ let modify _ = function
+ | Cltyp (na, ty) -> Clval (na, (mk_freelisted v, pb), ty)
+ | _ -> anomaly ~label:"meta_assign" (Pp.str "already defined")
+ in
+ let metas = Metamap.modify mv modify evd.metas in
+ set_metas evd metas
+
+let meta_reassign mv (v, pb) evd =
+ let modify _ = function
+ | Clval(na, _, ty) -> Clval (na, (mk_freelisted v, pb), ty)
+ | _ -> anomaly ~label:"meta_reassign" (Pp.str "not yet defined")
+ in
+ let metas = Metamap.modify mv modify evd.metas in
+ set_metas evd metas
+
+(* If the meta is defined then forget its name *)
+let meta_name evd mv =
+ try fst (clb_name (Metamap.find mv evd.metas)) with Not_found -> Anonymous
+
+let clear_metas evd = {evd with metas = Metamap.empty}
+
+let meta_merge evd1 evd2 =
+ let metas = Metamap.fold Metamap.add evd1.metas evd2.metas in
+ let universes = union_evar_universe_context evd2.universes evd1.universes in
+ {evd2 with universes; metas; }
+
+type metabinding = metavariable * constr * instance_status
+
+let retract_coercible_metas evd =
+ let mc = ref [] in
+ let map n v = match v with
+ | Clval (na, (b, (Conv, CoerceToType as s)), typ) ->
+ let () = mc := (n, b.rebus, s) :: !mc in
+ Cltyp (na, typ)
+ | v -> v
+ in
+ let metas = Metamap.smartmapi map evd.metas in
+ !mc, set_metas evd metas
+
+let evar_source_of_meta mv evd =
+ match meta_name evd mv with
+ | Anonymous -> (Loc.ghost,Evar_kinds.GoalEvar)
+ | Name id -> (Loc.ghost,Evar_kinds.VarInstance id)
+
+let dependent_evar_ident ev evd =
+ let evi = find evd ev in
+ match evi.evar_source with
+ | (_,Evar_kinds.VarInstance id) -> id
+ | _ -> anomaly (str "Not an evar resulting of a dependent binding")
+
+(**********************************************************)
+(* Extra data *)
+
+let get_extra_data evd = evd.extras
+let set_extra_data extras evd = { evd with extras }
+
+(*******************************************************************)
+
+type pending = (* before: *) evar_map * (* after: *) evar_map
+
+type pending_constr = pending * constr
+
+type open_constr = evar_map * constr
+
+(*******************************************************************)
+(* The type constructor ['a sigma] adds an evar map to an object of
+ type ['a] *)
+type 'a sigma = {
+ it : 'a ;
+ sigma : evar_map
+}
+
+let sig_it x = x.it
+let sig_sig x = x.sigma
+let on_sig s f =
+ let sigma', v = f s.sigma in
+ { s with sigma = sigma' }, v
+
+(*******************************************************************)
+(* The state monad with state an evar map. *)
+
+module MonadR =
+ Monad.Make (struct
+
+ type +'a t = evar_map -> evar_map * 'a
+
+ let return a = fun s -> (s,a)
+
+ let (>>=) x f = fun s ->
+ let (s',a) = x s in
+ f a s'
+
+ let (>>) x y = fun s ->
+ let (s',()) = x s in
+ y s'
+
+ let map f x = fun s ->
+ on_snd f (x s)
+
+ end)
+
+module Monad =
+ Monad.Make (struct
+
+ type +'a t = evar_map -> 'a * evar_map
+
+ let return a = fun s -> (a,s)
+
+ let (>>=) x f = fun s ->
+ let (a,s') = x s in
+ f a s'
+
+ let (>>) x y = fun s ->
+ let ((),s') = x s in
+ y s'
+
+ let map f x = fun s ->
+ on_fst f (x s)
+
+ end)
+
+(**********************************************************)
+(* Failure explanation *)
+
+type unsolvability_explanation = SeveralInstancesFound of int
+
+(**********************************************************)
+(* Pretty-printing *)
+
+let pr_existential_key sigma evk = str "?" ++ pr_id (evar_ident evk sigma)
+
+let pr_instance_status (sc,typ) =
+ begin match sc with
+ | IsSubType -> str " [or a subtype of it]"
+ | IsSuperType -> str " [or a supertype of it]"
+ | Conv -> mt ()
+ end ++
+ begin match typ with
+ | CoerceToType -> str " [up to coercion]"
+ | TypeNotProcessed -> mt ()
+ | TypeProcessed -> str " [type is checked]"
+ end
+
+let pr_meta_map mmap =
+ let pr_name = function
+ Name id -> str"[" ++ pr_id id ++ str"]"
+ | _ -> mt() in
+ let pr_meta_binding = function
+ | (mv,Cltyp (na,b)) ->
+ hov 0
+ (pr_meta mv ++ pr_name na ++ str " : " ++
+ print_constr b.rebus ++ fnl ())
+ | (mv,Clval(na,(b,s),t)) ->
+ hov 0
+ (pr_meta mv ++ pr_name na ++ str " := " ++
+ print_constr b.rebus ++
+ str " : " ++ print_constr t.rebus ++
+ spc () ++ pr_instance_status s ++ fnl ())
+ in
+ prlist pr_meta_binding (metamap_to_list mmap)
+
+let pr_decl ((id,b,_),ok) =
+ match b with
+ | None -> if ok then pr_id id else (str "{" ++ pr_id id ++ str "}")
+ | Some c -> str (if ok then "(" else "{") ++ pr_id id ++ str ":=" ++
+ print_constr c ++ str (if ok then ")" else "}")
+
+let rec pr_evar_source = function
+ | Evar_kinds.QuestionMark _ -> str "underscore"
+ | Evar_kinds.CasesType false -> str "pattern-matching return predicate"
+ | Evar_kinds.CasesType true ->
+ str "subterm of pattern-matching return predicate"
+ | Evar_kinds.BinderType (Name id) -> str "type of " ++ Nameops.pr_id id
+ | Evar_kinds.BinderType Anonymous -> str "type of anonymous binder"
+ | Evar_kinds.ImplicitArg (c,(n,ido),b) ->
+ let id = Option.get ido in
+ str "parameter " ++ pr_id id ++ spc () ++ str "of" ++
+ spc () ++ print_constr (printable_constr_of_global c)
+ | Evar_kinds.InternalHole -> str "internal placeholder"
+ | Evar_kinds.TomatchTypeParameter (ind,n) ->
+ pr_nth n ++ str " argument of type " ++ print_constr (mkInd ind)
+ | Evar_kinds.GoalEvar -> str "goal evar"
+ | Evar_kinds.ImpossibleCase -> str "type of impossible pattern-matching clause"
+ | Evar_kinds.MatchingVar _ -> str "matching variable"
+ | Evar_kinds.VarInstance id -> str "instance of " ++ pr_id id
+ | Evar_kinds.SubEvar evk ->
+ str "subterm of " ++ str (string_of_existential evk)
+
+let pr_evar_info evi =
+ let phyps =
+ try
+ let decls = match Filter.repr (evar_filter evi) with
+ | None -> List.map (fun c -> (c, true)) (evar_context evi)
+ | Some filter -> List.combine (evar_context evi) filter
+ in
+ prlist_with_sep spc pr_decl (List.rev decls)
+ with Invalid_argument _ -> str "Ill-formed filtered context" in
+ let pty = print_constr evi.evar_concl in
+ let pb =
+ match evi.evar_body with
+ | Evar_empty -> mt ()
+ | Evar_defined c -> spc() ++ str"=> " ++ print_constr c
+ in
+ let candidates =
+ match evi.evar_body, evi.evar_candidates with
+ | Evar_empty, Some l ->
+ spc () ++ str "{" ++
+ prlist_with_sep (fun () -> str "|") print_constr l ++ str "}"
+ | _ ->
+ mt ()
+ in
+ let src = str "(" ++ pr_evar_source (snd evi.evar_source) ++ str ")" in
+ hov 2
+ (str"[" ++ phyps ++ spc () ++ str"|- " ++ pty ++ pb ++ str"]" ++
+ candidates ++ spc() ++ src)
+
+let compute_evar_dependency_graph (sigma : evar_map) =
+ (* Compute the map binding ev to the evars whose body depends on ev *)
+ let fold evk evi acc =
+ let fold_ev evk' acc =
+ let tab =
+ try EvMap.find evk' acc
+ with Not_found -> Evar.Set.empty
+ in
+ EvMap.add evk' (Evar.Set.add evk tab) acc
+ in
+ match evar_body evi with
+ | Evar_empty -> assert false
+ | Evar_defined c -> Evar.Set.fold fold_ev (evars_of_term c) acc
+ in
+ EvMap.fold fold sigma.defn_evars EvMap.empty
+
+let evar_dependency_closure n sigma =
+ (** Create the DAG of depth [n] representing the recursive dependencies of
+ undefined evars. *)
+ let graph = compute_evar_dependency_graph sigma in
+ let rec aux n curr accu =
+ if Int.equal n 0 then Evar.Set.union curr accu
+ else
+ let fold evk accu =
+ try
+ let deps = EvMap.find evk graph in
+ Evar.Set.union deps accu
+ with Not_found -> accu
+ in
+ (** Consider only the newly added evars *)
+ let ncurr = Evar.Set.fold fold curr Evar.Set.empty in
+ (** Merge the others *)
+ let accu = Evar.Set.union curr accu in
+ aux (n - 1) ncurr accu
+ in
+ let undef = EvMap.domain (undefined_map sigma) in
+ aux n undef Evar.Set.empty
+
+let evar_dependency_closure n sigma =
+ let deps = evar_dependency_closure n sigma in
+ let map = EvMap.bind (fun ev -> find sigma ev) deps in
+ EvMap.bindings map
+
+let has_no_evar sigma =
+ EvMap.is_empty sigma.defn_evars && EvMap.is_empty sigma.undf_evars
+
+let pr_evd_level evd = pr_uctx_level evd.universes
+
+let pr_evar_universe_context ctx =
+ let prl = pr_uctx_level ctx in
+ if is_empty_evar_universe_context ctx then mt ()
+ else
+ (str"UNIVERSES:"++brk(0,1)++
+ h 0 (Univ.pr_universe_context_set prl (evar_universe_context_set ctx)) ++ fnl () ++
+ str"ALGEBRAIC UNIVERSES:"++brk(0,1)++
+ h 0 (Univ.LSet.pr prl (UState.algebraics ctx)) ++ fnl() ++
+ str"UNDEFINED UNIVERSES:"++brk(0,1)++
+ h 0 (Universes.pr_universe_opt_subst (UState.subst ctx)) ++ fnl())
+
+let print_env_short env =
+ let pr_body n = function
+ | None -> pr_name n
+ | Some b -> str "(" ++ pr_name n ++ str " := " ++ print_constr b ++ str ")" in
+ let pr_named_decl (n, b, _) = pr_body (Name n) b in
+ let pr_rel_decl (n, b, _) = pr_body n b in
+ let nc = List.rev (named_context env) in
+ let rc = List.rev (rel_context env) in
+ str "[" ++ pr_sequence pr_named_decl nc ++ str "]" ++ spc () ++
+ str "[" ++ pr_sequence pr_rel_decl rc ++ str "]"
+
+let pr_evar_constraints pbs =
+ let pr_evconstr (pbty, env, t1, t2) =
+ print_env_short env ++ spc () ++ str "|-" ++ spc () ++
+ print_constr_env env t1 ++ spc () ++
+ str (match pbty with
+ | Reduction.CONV -> "=="
+ | Reduction.CUMUL -> "<=") ++
+ spc () ++ print_constr_env env t2
+ in
+ prlist_with_sep fnl pr_evconstr pbs
+
+let pr_evar_map_gen with_univs pr_evars sigma =
+ let { universes = uvs } = sigma in
+ let evs = if has_no_evar sigma then mt () else pr_evars sigma ++ fnl ()
+ and svs = if with_univs then pr_evar_universe_context uvs else mt ()
+ and cstrs =
+ if List.is_empty sigma.conv_pbs then mt ()
+ else
+ str "CONSTRAINTS:" ++ brk (0, 1) ++
+ pr_evar_constraints sigma.conv_pbs ++ fnl ()
+ and metas =
+ if Metamap.is_empty sigma.metas then mt ()
+ else
+ str "METAS:" ++ brk (0, 1) ++ pr_meta_map sigma.metas
+ in
+ evs ++ svs ++ cstrs ++ metas
+
+let pr_evar_list sigma l =
+ let pr (ev, evi) =
+ h 0 (str (string_of_existential ev) ++
+ str "==" ++ pr_evar_info evi ++
+ (if evi.evar_body == Evar_empty
+ then str " {" ++ pr_id (evar_ident ev sigma) ++ str "}"
+ else mt ()))
+ in
+ h 0 (prlist_with_sep fnl pr l)
+
+let pr_evar_by_depth depth sigma = match depth with
+| None ->
+ (* Print all evars *)
+ str"EVARS:"++brk(0,1)++pr_evar_list sigma (to_list sigma)++fnl()
+| Some n ->
+ (* Print all evars *)
+ str"UNDEFINED EVARS:"++
+ (if Int.equal n 0 then mt() else str" (+level "++int n++str" closure):")++
+ brk(0,1)++
+ pr_evar_list sigma (evar_dependency_closure n sigma)++fnl()
+
+let pr_evar_by_filter filter sigma =
+ let defined = Evar.Map.filter filter sigma.defn_evars in
+ let undefined = Evar.Map.filter filter sigma.undf_evars in
+ let prdef =
+ if Evar.Map.is_empty defined then mt ()
+ else str "DEFINED EVARS:" ++ brk (0, 1) ++
+ pr_evar_list sigma (Evar.Map.bindings defined)
+ in
+ let prundef =
+ if Evar.Map.is_empty undefined then mt ()
+ else str "UNDEFINED EVARS:" ++ brk (0, 1) ++
+ pr_evar_list sigma (Evar.Map.bindings undefined)
+ in
+ prdef ++ prundef
+
+let pr_evar_map ?(with_univs=true) depth sigma =
+ pr_evar_map_gen with_univs (fun sigma -> pr_evar_by_depth depth sigma) sigma
+
+let pr_evar_map_filter ?(with_univs=true) filter sigma =
+ pr_evar_map_gen with_univs (fun sigma -> pr_evar_by_filter filter sigma) sigma
+
+let pr_metaset metas =
+ str "[" ++ pr_sequence pr_meta (Metaset.elements metas) ++ str "]"
diff --git a/engine/evd.mli b/engine/evd.mli
new file mode 100644
index 000000000..3a95b77f0
--- /dev/null
+++ b/engine/evd.mli
@@ -0,0 +1,624 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Util
+open Loc
+open Names
+open Term
+open Context
+open Environ
+
+(** {5 Existential variables and unification states}
+
+ A unification state (of type [evar_map]) is primarily a finite mapping
+ from existential variables to records containing the type of the evar
+ ([evar_concl]), the context under which it was introduced ([evar_hyps])
+ and its definition ([evar_body]). [evar_extra] is used to add any other
+ kind of information.
+
+ It also contains conversion constraints, debugging information and
+ information about meta variables. *)
+
+(** {6 Evars} *)
+
+type evar = existential_key
+(** Existential variables. TODO: Should be made opaque one day. *)
+
+val string_of_existential : evar -> string
+
+(** {6 Evar filters} *)
+
+module Filter :
+sig
+ type t
+ (** Evar filters, seen as bitmasks. *)
+
+ val equal : t -> t -> bool
+ (** Equality over filters *)
+
+ val identity : t
+ (** The identity filter. *)
+
+ val filter_list : t -> 'a list -> 'a list
+ (** Filter a list. Sizes must coincide. *)
+
+ val filter_array : t -> 'a array -> 'a array
+ (** Filter an array. Sizes must coincide. *)
+
+ val extend : int -> t -> t
+ (** [extend n f] extends [f] on the left with [n]-th times [true]. *)
+
+ val compose : t -> t -> t
+ (** Horizontal composition : [compose f1 f2] only keeps parts of [f2] where
+ [f1] is set. In particular, [f1] and [f2] must have the same length. *)
+
+ val apply_subfilter : t -> bool list -> t
+ (** [apply_subfilter f1 f2] applies filter [f2] where [f1] is [true]. In
+ particular, the length of [f2] is the number of times [f1] is [true] *)
+
+ val restrict_upon : t -> int -> (int -> bool) -> t option
+ (** Ad-hoc primitive. *)
+
+ val map_along : (bool -> 'a -> bool) -> t -> 'a list -> t
+ (** Apply the function on the filter and the list. Sizes must coincide. *)
+
+ val make : bool list -> t
+ (** Create out of a list *)
+
+ val repr : t -> bool list option
+ (** Observe as a bool list. *)
+
+end
+
+(** {6 Evar infos} *)
+
+type evar_body =
+ | Evar_empty
+ | Evar_defined of constr
+
+
+module Store : Store.S
+(** Datatype used to store additional information in evar maps. *)
+
+type evar_info = {
+ evar_concl : constr;
+ (** Type of the evar. *)
+ evar_hyps : named_context_val;
+ (** Context of the evar. *)
+ evar_body : evar_body;
+ (** Optional content of the evar. *)
+ evar_filter : Filter.t;
+ (** Boolean mask over {!evar_hyps}. Should have the same length.
+ TODO: document me more. *)
+ evar_source : Evar_kinds.t located;
+ (** Information about the evar. *)
+ evar_candidates : constr list option;
+ (** TODO: document this *)
+ evar_extra : Store.t
+ (** Extra store, used for clever hacks. *)
+}
+
+val make_evar : named_context_val -> types -> evar_info
+val evar_concl : evar_info -> constr
+val evar_context : evar_info -> named_context
+val evar_filtered_context : evar_info -> named_context
+val evar_hyps : evar_info -> named_context_val
+val evar_filtered_hyps : evar_info -> named_context_val
+val evar_body : evar_info -> evar_body
+val evar_filter : evar_info -> Filter.t
+val evar_env : evar_info -> env
+val evar_filtered_env : evar_info -> env
+
+val map_evar_body : (constr -> constr) -> evar_body -> evar_body
+val map_evar_info : (constr -> constr) -> evar_info -> evar_info
+
+(** {6 Unification state} **)
+
+type evar_universe_context = UState.t
+(** The universe context associated to an evar map *)
+
+type evar_map
+(** Type of unification state. Essentially a bunch of state-passing data needed
+ to handle incremental term construction. *)
+
+val empty : evar_map
+(** The empty evar map. *)
+
+val from_env : env -> evar_map
+(** The empty evar map with given universe context, taking its initial
+ universes from env. *)
+
+val from_ctx : evar_universe_context -> evar_map
+(** The empty evar map with given universe context *)
+
+val is_empty : evar_map -> bool
+(** Whether an evarmap is empty. *)
+
+val has_undefined : evar_map -> bool
+(** [has_undefined sigma] is [true] if and only if
+ there are uninstantiated evars in [sigma]. *)
+
+val new_evar : evar_map ->
+ ?naming:Misctypes.intro_pattern_naming_expr -> evar_info -> evar_map * evar
+(** Creates a fresh evar mapping to the given information. *)
+
+val add : evar_map -> evar -> evar_info -> evar_map
+(** [add sigma ev info] adds [ev] with evar info [info] in sigma.
+ Precondition: ev must not preexist in [sigma]. *)
+
+val find : evar_map -> evar -> evar_info
+(** Recover the data associated to an evar. *)
+
+val find_undefined : evar_map -> evar -> evar_info
+(** Same as {!find} but restricted to undefined evars. For efficiency
+ reasons. *)
+
+val remove : evar_map -> evar -> evar_map
+(** Remove an evar from an evar map. Use with caution. *)
+
+val mem : evar_map -> evar -> bool
+(** Whether an evar is present in an evarmap. *)
+
+val fold : (evar -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a
+(** Apply a function to all evars and their associated info in an evarmap. *)
+
+val fold_undefined : (evar -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a
+(** Same as {!fold}, but restricted to undefined evars. For efficiency
+ reasons. *)
+
+val raw_map : (evar -> evar_info -> evar_info) -> evar_map -> evar_map
+(** Apply the given function to all evars in the map. Beware: this function
+ expects the argument function to preserve the kind of [evar_body], i.e. it
+ must send [Evar_empty] to [Evar_empty] and [Evar_defined c] to some
+ [Evar_defined c']. *)
+
+val raw_map_undefined : (evar -> evar_info -> evar_info) -> evar_map -> evar_map
+(** Same as {!raw_map}, but restricted to undefined evars. For efficiency
+ reasons. *)
+
+val define : evar -> constr -> evar_map -> evar_map
+(** Set the body of an evar to the given constr. It is expected that:
+ {ul
+ {- The evar is already present in the evarmap.}
+ {- The evar is not defined in the evarmap yet.}
+ {- All the evars present in the constr should be present in the evar map.}
+ } *)
+
+val cmap : (constr -> constr) -> evar_map -> evar_map
+(** Map the function on all terms in the evar map. *)
+
+val is_evar : evar_map -> evar -> bool
+(** Alias for {!mem}. *)
+
+val is_defined : evar_map -> evar -> bool
+(** Whether an evar is defined in an evarmap. *)
+
+val is_undefined : evar_map -> evar -> bool
+(** Whether an evar is not defined in an evarmap. *)
+
+val add_constraints : evar_map -> Univ.constraints -> evar_map
+(** Add universe constraints in an evar map. *)
+
+val undefined_map : evar_map -> evar_info Evar.Map.t
+(** Access the undefined evar mapping directly. *)
+
+val drop_all_defined : evar_map -> evar_map
+
+(** {6 Instantiating partial terms} *)
+
+exception NotInstantiatedEvar
+
+val existential_value : evar_map -> existential -> constr
+(** [existential_value sigma ev] raises [NotInstantiatedEvar] if [ev] has
+ no body and [Not_found] if it does not exist in [sigma] *)
+
+val existential_type : evar_map -> existential -> types
+
+val existential_opt_value : evar_map -> existential -> constr option
+(** Same as {!existential_value} but returns an option instead of raising an
+ exception. *)
+
+val evar_instance_array : (named_declaration -> 'a -> bool) -> evar_info ->
+ 'a array -> (Id.t * 'a) list
+
+val instantiate_evar_array : evar_info -> constr -> constr array -> constr
+
+val evars_reset_evd : ?with_conv_pbs:bool -> ?with_univs:bool ->
+ evar_map -> evar_map -> evar_map
+(** spiwack: this function seems to somewhat break the abstraction. *)
+
+(** {6 Misc} *)
+
+val restrict : evar -> Filter.t -> ?candidates:constr list ->
+ evar_map -> evar_map * evar
+(** Restrict an undefined evar into a new evar by filtering context and
+ possibly limiting the instances to a set of candidates *)
+
+val downcast : evar -> types -> evar_map -> evar_map
+(** Change the type of an undefined evar to a new type assumed to be a
+ subtype of its current type; subtyping must be ensured by caller *)
+
+val evar_source : existential_key -> evar_map -> Evar_kinds.t located
+(** Convenience function. Wrapper around {!find} to recover the source of an
+ evar in a given evar map. *)
+
+val evar_ident : existential_key -> evar_map -> Id.t
+
+val rename : existential_key -> Id.t -> evar_map -> evar_map
+
+val evar_key : Id.t -> evar_map -> existential_key
+
+val evar_source_of_meta : metavariable -> evar_map -> Evar_kinds.t located
+
+val dependent_evar_ident : existential_key -> evar_map -> Id.t
+
+(** {5 Side-effects} *)
+
+val emit_side_effects : Safe_typing.private_constants -> evar_map -> evar_map
+(** Push a side-effect into the evar map. *)
+
+val eval_side_effects : evar_map -> Safe_typing.private_constants
+(** Return the effects contained in the evar map. *)
+
+val drop_side_effects : evar_map -> evar_map
+(** This should not be used. For hacking purposes. *)
+
+(** {5 Future goals} *)
+
+val declare_future_goal : Evar.t -> evar_map -> evar_map
+(** Adds an existential variable to the list of future goals. For
+ internal uses only. *)
+
+val declare_principal_goal : Evar.t -> evar_map -> evar_map
+(** Adds an existential variable to the list of future goals and make
+ it principal. Only one existential variable can be made principal, an
+ error is raised otherwise. For internal uses only. *)
+
+val future_goals : evar_map -> Evar.t list
+(** Retrieves the list of future goals. Used by the [refine] primitive
+ of the tactic engine. *)
+
+val principal_future_goal : evar_map -> Evar.t option
+(** Retrieves the name of the principal existential variable if there
+ is one. Used by the [refine] primitive of the tactic engine. *)
+
+val reset_future_goals : evar_map -> evar_map
+(** Clears the list of future goals (as well as the principal future
+ goal). Used by the [refine] primitive of the tactic engine. *)
+
+val restore_future_goals : evar_map -> Evar.t list -> Evar.t option -> evar_map
+(** Sets the future goals (including the principal future goal) to a
+ previous value. Intended to be used after a local list of future
+ goals has been consumed. Used by the [refine] primitive of the
+ tactic engine. *)
+
+(** {5 Sort variables}
+
+ Evar maps also keep track of the universe constraints defined at a given
+ point. This section defines the relevant manipulation functions. *)
+
+val whd_sort_variable : evar_map -> constr -> constr
+
+exception UniversesDiffer
+
+val add_universe_constraints : evar_map -> Universes.universe_constraints -> evar_map
+(** Add the given universe unification constraints to the evar map.
+ @raises UniversesDiffer in case a first-order unification fails.
+ @raises UniverseInconsistency
+*)
+
+(** {5 Extra data}
+
+ Evar maps can contain arbitrary data, allowing to use an extensible state.
+ As evar maps are theoretically used in a strict state-passing style, such
+ additional data should be passed along transparently. Some old and bug-prone
+ code tends to drop them nonetheless, so you should keep cautious.
+
+*)
+
+val get_extra_data : evar_map -> Store.t
+val set_extra_data : Store.t -> evar_map -> evar_map
+
+(** {5 Enriching with evar maps} *)
+
+type 'a sigma = {
+ it : 'a ;
+ (** The base object. *)
+ sigma : evar_map
+ (** The added unification state. *)
+}
+(** The type constructor ['a sigma] adds an evar map to an object of type
+ ['a]. *)
+
+val sig_it : 'a sigma -> 'a
+val sig_sig : 'a sigma -> evar_map
+val on_sig : 'a sigma -> (evar_map -> evar_map * 'b) -> 'a sigma * 'b
+
+(** {5 The state monad with state an evar map} *)
+
+module MonadR : Monad.S with type +'a t = evar_map -> evar_map * 'a
+module Monad : Monad.S with type +'a t = evar_map -> 'a * evar_map
+
+
+(** {5 Meta machinery}
+
+ These functions are almost deprecated. They were used before the
+ introduction of the full-fledged evar calculus. In an ideal world, they
+ should be removed. Alas, some parts of the code still use them. Do not use
+ in newly-written code. *)
+
+module Metaset : Set.S with type elt = metavariable
+module Metamap : Map.ExtS with type key = metavariable and module Set := Metaset
+
+type 'a freelisted = {
+ rebus : 'a;
+ freemetas : Metaset.t }
+
+val metavars_of : constr -> Metaset.t
+val mk_freelisted : constr -> constr freelisted
+val map_fl : ('a -> 'b) -> 'a freelisted -> 'b freelisted
+
+(** Status of an instance found by unification wrt to the meta it solves:
+ - a supertype of the meta (e.g. the solution to ?X <= T is a supertype of ?X)
+ - a subtype of the meta (e.g. the solution to T <= ?X is a supertype of ?X)
+ - a term that can be eta-expanded n times while still being a solution
+ (e.g. the solution [P] to [?X u v = P u v] can be eta-expanded twice)
+*)
+
+type instance_constraint = IsSuperType | IsSubType | Conv
+
+val eq_instance_constraint :
+ instance_constraint -> instance_constraint -> bool
+
+(** Status of the unification of the type of an instance against the type of
+ the meta it instantiates:
+ - CoerceToType means that the unification of types has not been done
+ and that a coercion can still be inserted: the meta should not be
+ substituted freely (this happens for instance given via the
+ "with" binding clause).
+ - TypeProcessed means that the information obtainable from the
+ unification of types has been extracted.
+ - TypeNotProcessed means that the unification of types has not been
+ done but it is known that no coercion may be inserted: the meta
+ can be substituted freely.
+*)
+
+type instance_typing_status =
+ CoerceToType | TypeNotProcessed | TypeProcessed
+
+(** Status of an instance together with the status of its type unification *)
+
+type instance_status = instance_constraint * instance_typing_status
+
+(** Clausal environments *)
+
+type clbinding =
+ | Cltyp of Name.t * constr freelisted
+ | Clval of Name.t * (constr freelisted * instance_status) * constr freelisted
+
+(** Unification constraints *)
+type conv_pb = Reduction.conv_pb
+type evar_constraint = conv_pb * env * constr * constr
+val add_conv_pb : ?tail:bool -> evar_constraint -> evar_map -> evar_map
+
+val extract_changed_conv_pbs : evar_map ->
+ (Evar.Set.t -> evar_constraint -> bool) ->
+ evar_map * evar_constraint list
+val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list
+val loc_of_conv_pb : evar_map -> evar_constraint -> Loc.t
+
+(** The following functions return the set of evars immediately
+ contained in the object; need the term to be evar-normal otherwise
+ defined evars are returned too. *)
+
+val evar_list : constr -> existential list
+ (** excluding evars in instances of evars and collected with
+ redundancies from right to left (used by tactic "instantiate") *)
+
+val evars_of_term : constr -> Evar.Set.t
+ (** including evars in instances of evars *)
+
+val evars_of_named_context : named_context -> Evar.Set.t
+
+val evars_of_filtered_evar_info : evar_info -> Evar.Set.t
+
+(** Metas *)
+val meta_list : evar_map -> (metavariable * clbinding) list
+val meta_defined : evar_map -> metavariable -> bool
+
+val meta_value : evar_map -> metavariable -> constr
+(** [meta_fvalue] raises [Not_found] if meta not in map or [Anomaly] if
+ meta has no value *)
+
+val meta_fvalue : evar_map -> metavariable -> constr freelisted * instance_status
+val meta_opt_fvalue : evar_map -> metavariable -> (constr freelisted * instance_status) option
+val meta_type : evar_map -> metavariable -> types
+val meta_ftype : evar_map -> metavariable -> types freelisted
+val meta_name : evar_map -> metavariable -> Name.t
+val meta_declare :
+ metavariable -> types -> ?name:Name.t -> evar_map -> evar_map
+val meta_assign : metavariable -> constr * instance_status -> evar_map -> evar_map
+val meta_reassign : metavariable -> constr * instance_status -> evar_map -> evar_map
+
+val clear_metas : evar_map -> evar_map
+
+(** [meta_merge evd1 evd2] returns [evd2] extended with the metas of [evd1] *)
+val meta_merge : evar_map -> evar_map -> evar_map
+
+val undefined_metas : evar_map -> metavariable list
+val map_metas_fvalue : (constr -> constr) -> evar_map -> evar_map
+
+type metabinding = metavariable * constr * instance_status
+
+val retract_coercible_metas : evar_map -> metabinding list * evar_map
+
+(** {5 FIXME: Nothing to do here} *)
+
+(*********************************************************
+ Sort/universe variables *)
+
+(** Rigid or flexible universe variables *)
+
+type rigid = UState.rigid =
+ | UnivRigid
+ | UnivFlexible of bool (** Is substitution by an algebraic ok? *)
+
+val univ_rigid : rigid
+val univ_flexible : rigid
+val univ_flexible_alg : rigid
+
+type 'a in_evar_universe_context = 'a * evar_universe_context
+
+val evar_universe_context_set : evar_universe_context -> Univ.universe_context_set
+val evar_universe_context_constraints : evar_universe_context -> Univ.constraints
+val evar_context_universe_context : evar_universe_context -> Univ.universe_context
+val evar_universe_context_of : Univ.universe_context_set -> evar_universe_context
+val empty_evar_universe_context : evar_universe_context
+val union_evar_universe_context : evar_universe_context -> evar_universe_context ->
+ evar_universe_context
+val evar_universe_context_subst : evar_universe_context -> Universes.universe_opt_subst
+val constrain_variables : Univ.LSet.t -> evar_universe_context -> Univ.constraints
+
+
+val evar_universe_context_of_binders :
+ Universes.universe_binders -> evar_universe_context
+
+val make_evar_universe_context : env -> (Id.t located) list option -> evar_universe_context
+val restrict_universe_context : evar_map -> Univ.universe_set -> evar_map
+(** Raises Not_found if not a name for a universe in this map. *)
+val universe_of_name : evar_map -> string -> Univ.universe_level
+val add_universe_name : evar_map -> string -> Univ.universe_level -> evar_map
+
+val universes : evar_map -> UGraph.t
+
+val add_constraints_context : evar_universe_context ->
+ Univ.constraints -> evar_universe_context
+
+
+val normalize_evar_universe_context_variables : evar_universe_context ->
+ Univ.universe_subst in_evar_universe_context
+
+val normalize_evar_universe_context : evar_universe_context ->
+ evar_universe_context
+
+val new_univ_level_variable : ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe_level
+val new_univ_variable : ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe
+val new_sort_variable : ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * sorts
+val add_global_univ : evar_map -> Univ.Level.t -> evar_map
+
+val make_flexible_variable : evar_map -> bool -> Univ.universe_level -> evar_map
+val is_sort_variable : evar_map -> sorts -> Univ.universe_level option
+(** [is_sort_variable evm s] returns [Some u] or [None] if [s] is
+ not a local sort variable declared in [evm] *)
+val is_flexible_level : evar_map -> Univ.Level.t -> bool
+
+val whd_sort_variable : evar_map -> constr -> constr
+(* val normalize_universe_level : evar_map -> Univ.universe_level -> Univ.universe_level *)
+val normalize_universe : evar_map -> Univ.universe -> Univ.universe
+val normalize_universe_instance : evar_map -> Univ.universe_instance -> Univ.universe_instance
+
+val set_leq_sort : env -> evar_map -> sorts -> sorts -> evar_map
+val set_eq_sort : env -> evar_map -> sorts -> sorts -> evar_map
+val has_lub : evar_map -> Univ.universe -> Univ.universe -> evar_map
+val set_eq_level : evar_map -> Univ.universe_level -> Univ.universe_level -> evar_map
+val set_leq_level : evar_map -> Univ.universe_level -> Univ.universe_level -> evar_map
+val set_eq_instances : ?flex:bool ->
+ evar_map -> Univ.universe_instance -> Univ.universe_instance -> evar_map
+
+val check_eq : evar_map -> Univ.universe -> Univ.universe -> bool
+val check_leq : evar_map -> Univ.universe -> Univ.universe -> bool
+
+val evar_universe_context : evar_map -> evar_universe_context
+val universe_context_set : evar_map -> Univ.universe_context_set
+val universe_context : ?names:(Id.t located) list -> evar_map ->
+ (Id.t * Univ.Level.t) list * Univ.universe_context
+val universe_subst : evar_map -> Universes.universe_opt_subst
+val universes : evar_map -> UGraph.t
+
+
+val merge_universe_context : evar_map -> evar_universe_context -> evar_map
+val set_universe_context : evar_map -> evar_universe_context -> evar_map
+
+val merge_context_set : ?sideff:bool -> rigid -> evar_map -> Univ.universe_context_set -> evar_map
+val merge_universe_subst : evar_map -> Universes.universe_opt_subst -> evar_map
+
+val with_context_set : rigid -> evar_map -> 'a Univ.in_universe_context_set -> evar_map * 'a
+
+val nf_univ_variables : evar_map -> evar_map * Univ.universe_subst
+val abstract_undefined_variables : evar_universe_context -> evar_universe_context
+
+val fix_undefined_variables : evar_map -> evar_map
+
+val refresh_undefined_universes : evar_map -> evar_map * Univ.universe_level_subst
+
+val nf_constraints : evar_map -> evar_map
+
+val update_sigma_env : evar_map -> env -> evar_map
+
+(** Polymorphic universes *)
+
+val fresh_sort_in_family : ?rigid:rigid -> env -> evar_map -> sorts_family -> evar_map * sorts
+val fresh_constant_instance : env -> evar_map -> constant -> evar_map * pconstant
+val fresh_inductive_instance : env -> evar_map -> inductive -> evar_map * pinductive
+val fresh_constructor_instance : env -> evar_map -> constructor -> evar_map * pconstructor
+
+val fresh_global : ?rigid:rigid -> ?names:Univ.Instance.t -> env -> evar_map ->
+ Globnames.global_reference -> evar_map * constr
+
+(********************************************************************
+ Conversion w.r.t. an evar map: might generate universe unifications
+ that are kept in the evarmap.
+ Raises [NotConvertible]. *)
+
+val conversion : env -> evar_map -> conv_pb -> constr -> constr -> evar_map
+
+val test_conversion : env -> evar_map -> conv_pb -> constr -> constr -> bool
+(** This one forgets about the assignemts of universes. *)
+
+val eq_constr_univs : evar_map -> constr -> constr -> evar_map * bool
+(** Syntactic equality up to universes, recording the associated constraints *)
+
+val e_eq_constr_univs : evar_map ref -> constr -> constr -> bool
+(** Syntactic equality up to universes. *)
+
+(********************************************************************)
+(* constr with holes and pending resolution of classes, conversion *)
+(* problems, candidates, etc. *)
+
+type pending = (* before: *) evar_map * (* after: *) evar_map
+
+type pending_constr = pending * constr
+
+type open_constr = evar_map * constr (* Special case when before is empty *)
+
+(** Partially constructed constrs. *)
+
+type unsolvability_explanation = SeveralInstancesFound of int
+(** Failure explanation. *)
+
+val pr_existential_key : evar_map -> evar -> Pp.std_ppcmds
+
+(** {5 Debug pretty-printers} *)
+
+val pr_evar_info : evar_info -> Pp.std_ppcmds
+val pr_evar_constraints : evar_constraint list -> Pp.std_ppcmds
+val pr_evar_map : ?with_univs:bool -> int option -> evar_map -> Pp.std_ppcmds
+val pr_evar_map_filter : ?with_univs:bool -> (Evar.t -> evar_info -> bool) ->
+ evar_map -> Pp.std_ppcmds
+val pr_metaset : Metaset.t -> Pp.std_ppcmds
+val pr_evar_universe_context : evar_universe_context -> Pp.std_ppcmds
+val pr_evd_level : evar_map -> Univ.Level.t -> Pp.std_ppcmds
+
+(** {5 Deprecated functions} *)
+
+val create_evar_defs : evar_map -> evar_map
+(** Create an [evar_map] with empty meta map: *)
+
+(** {5 Summary names} *)
+
+val evar_counter_summary_name : string
diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml
new file mode 100644
index 000000000..75134e6f1
--- /dev/null
+++ b/engine/logic_monad.ml
@@ -0,0 +1,384 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(** This file defines the low-level monadic operations used by the
+ tactic monad. The monad is divided into two layers: a non-logical
+ layer which consists in operations which will not (or cannot) be
+ backtracked in case of failure (input/output or persistent state)
+ and a logical layer which handles backtracking, proof
+ manipulation, and any other effect which needs to backtrack. *)
+
+
+(** {6 Exceptions} *)
+
+
+(** To help distinguish between exceptions raised by the IO monad from
+ the one used natively by Coq, the former are wrapped in
+ [Exception]. It is only used internally so that [catch] blocks of
+ the IO monad would only catch exceptions raised by the [raise]
+ function of the IO monad, and not for instance, by system
+ interrupts. Also used in [Proofview] to avoid capturing exception
+ from the IO monad ([Proofview] catches errors in its compatibility
+ layer, and when lifting goal-level expressions). *)
+exception Exception of exn
+(** This exception is used to signal abortion in [timeout] functions. *)
+exception Timeout
+(** This exception is used by the tactics to signal failure by lack of
+ successes, rather than some other exceptions (like system
+ interrupts). *)
+exception TacticFailure of exn
+
+let _ = Errors.register_handler begin function
+ | Timeout -> Errors.errorlabstrm "Some timeout function" (Pp.str"Timeout!")
+ | Exception e -> Errors.print e
+ | TacticFailure e -> Errors.print e
+ | _ -> Pervasives.raise Errors.Unhandled
+end
+
+(** {6 Non-logical layer} *)
+
+(** The non-logical monad is a simple [unit -> 'a] (i/o) monad. The
+ operations are simple wrappers around corresponding usual
+ operations and require little documentation. *)
+module NonLogical =
+struct
+
+ (* The functions in this module follow the pattern that they are
+ defined with the form [(); fun ()->...]. This is an optimisation
+ which signals to the compiler that the function is usually partially
+ applied up to the [();]. Without this annotation, partial
+ applications can be significantly slower.
+
+ Documentation of this behaviour can be found at:
+ https://ocaml.janestreet.com/?q=node/30 *)
+
+ include Monad.Make(struct
+ type 'a t = unit -> 'a
+
+ let return a = (); fun () -> a
+ let (>>=) a k = (); fun () -> k (a ()) ()
+ let (>>) a k = (); fun () -> a (); k ()
+ let map f a = (); fun () -> f (a ())
+ end)
+
+ type 'a ref = 'a Pervasives.ref
+
+ let ignore a = (); fun () -> ignore (a ())
+
+ let ref a = (); fun () -> Pervasives.ref a
+
+ (** [Pervasives.(:=)] *)
+ let (:=) r a = (); fun () -> r := a
+
+ (** [Pervasives.(!)] *)
+ let (!) = fun r -> (); fun () -> ! r
+
+ (** [Pervasives.raise]. Except that exceptions are wrapped with
+ {!Exception}. *)
+ let raise ?info = fun e -> (); fun () -> Exninfo.raise ?info (Exception e)
+
+ (** [try ... with ...] but restricted to {!Exception}. *)
+ let catch = fun s h -> ();
+ fun () -> try s ()
+ with Exception e as src ->
+ let (src, info) = Errors.push src in
+ h (e, info) ()
+
+ let read_line = fun () -> try Pervasives.read_line () with e ->
+ let (e, info) = Errors.push e in raise ~info e ()
+
+ let print_char = fun c -> (); fun () -> print_char c
+
+ let timeout = fun n t -> (); fun () ->
+ Control.timeout n t (Exception Timeout)
+
+ let make f = (); fun () ->
+ try f ()
+ with e when Errors.noncritical e ->
+ let (e, info) = Errors.push e in
+ Util.iraise (Exception e, info)
+
+ (** Use the current logger. The buffer is also flushed. *)
+ let print_debug s = make (fun _ -> Pp.msg_info s;Pp.pp_flush ())
+ let print_info s = make (fun _ -> Pp.msg_info s;Pp.pp_flush ())
+ let print_warning s = make (fun _ -> Pp.msg_warning s;Pp.pp_flush ())
+ let print_error s = make (fun _ -> Pp.msg_error s;Pp.pp_flush ())
+ let print_notice s = make (fun _ -> Pp.msg_notice s;Pp.pp_flush ())
+
+ let run = fun x ->
+ try x () with Exception e as src ->
+ let (src, info) = Errors.push src in
+ Util.iraise (e, info)
+end
+
+(** {6 Logical layer} *)
+
+(** The logical monad is a backtracking monad on top of which is
+ layered a state monad (which is used to implement all of read/write,
+ read only, and write only effects). The state monad being layered on
+ top of the backtracking monad makes it so that the state is
+ backtracked on failure.
+
+ Backtracking differs from regular exception in that, writing (+)
+ for exception catching and (>>=) for bind, we require the
+ following extra distributivity laws:
+
+ x+(y+z) = (x+y)+z
+
+ zero+x = x
+
+ x+zero = x
+
+ (x+y)>>=k = (x>>=k)+(y>>=k) *)
+
+(** A view type for the logical monad, which is a form of list, hence
+ we can decompose it with as a list. *)
+type ('a, 'b, 'e) list_view =
+ | Nil of 'e
+ | Cons of 'a * ('e -> 'b)
+
+module BackState =
+struct
+
+ (** Double-continuation backtracking monads are reasonable folklore
+ for "search" implementations (including the Tac interactive
+ prover's tactics). Yet it's quite hard to wrap your head around
+ these. I recommand reading a few times the "Backtracking,
+ Interleaving, and Terminating Monad Transformers" paper by
+ O. Kiselyov, C. Shan, D. Friedman, and A. Sabry. The peculiar
+ shape of the monadic type is reminiscent of that of the
+ continuation monad transformer.
+
+ The paper also contains the rationale for the [split] abstraction.
+
+ An explanation of how to derive such a monad from mathematical
+ principles can be found in "Kan Extensions for Program
+ Optimisation" by Ralf Hinze.
+
+ A somewhat concrete view is that the type ['a iolist] is, in fact
+ the impredicative encoding of the following stream type:
+
+ [type 'a _iolist' = Nil of exn | Cons of 'a*'a iolist'
+ and 'a iolist = 'a _iolist NonLogical.t]
+
+ Using impredicative encoding avoids intermediate allocation and
+ is, empirically, very efficient in Ocaml. It also has the
+ practical benefit that the monadic operation are independent of
+ the underlying monad, which simplifies the code and side-steps
+ the limited inlining of Ocaml.
+
+ In that vision, [bind] is simply [concat_map] (though the cps
+ version is significantly simpler), [plus] is concatenation, and
+ [split] is pattern-matching. *)
+
+ type ('a, 'i, 'o, 'e) t =
+ { iolist : 'r. 'i -> ('e -> 'r NonLogical.t) ->
+ ('a -> 'o -> ('e -> 'r NonLogical.t) -> 'r NonLogical.t) ->
+ 'r NonLogical.t }
+
+ let return x =
+ { iolist = fun s nil cons -> cons x s nil }
+
+ let (>>=) m f =
+ { iolist = fun s nil cons ->
+ m.iolist s nil (fun x s next -> (f x).iolist s next cons) }
+
+ let (>>) m f =
+ { iolist = fun s nil cons ->
+ m.iolist s nil (fun () s next -> f.iolist s next cons) }
+
+ let map f m =
+ { iolist = fun s nil cons -> m.iolist s nil (fun x s next -> cons (f x) s next) }
+
+ let zero e =
+ { iolist = fun _ nil cons -> nil e }
+
+ let plus m1 m2 =
+ { iolist = fun s nil cons -> m1.iolist s (fun e -> (m2 e).iolist s nil cons) cons }
+
+ let ignore m =
+ { iolist = fun s nil cons -> m.iolist s nil (fun _ s next -> cons () s next) }
+
+ let lift m =
+ { iolist = fun s nil cons -> NonLogical.(m >>= fun x -> cons x s nil) }
+
+ (** State related *)
+
+ let get =
+ { iolist = fun s nil cons -> cons s s nil }
+
+ let set s =
+ { iolist = fun _ nil cons -> cons () s nil }
+
+ let modify f =
+ { iolist = fun s nil cons -> cons () (f s) nil }
+
+ (** Exception manipulation *)
+
+ let interleave src dst m =
+ { iolist = fun s nil cons ->
+ m.iolist s (fun e1 -> nil (src e1))
+ (fun x s next -> cons x s (fun e2 -> next (dst e2)))
+ }
+
+ (** List observation *)
+
+ let once m =
+ { iolist = fun s nil cons -> m.iolist s nil (fun x s _ -> cons x s nil) }
+
+ let break f m =
+ { iolist = fun s nil cons ->
+ m.iolist s nil (fun x s next -> cons x s (fun e -> match f e with None -> next e | Some e -> nil e))
+ }
+
+ (** For [reflect] and [split] see the "Backtracking, Interleaving,
+ and Terminating Monad Transformers" paper. *)
+ type ('a, 'e) reified = ('a, ('a, 'e) reified, 'e) list_view NonLogical.t
+
+ let rec reflect (m : ('a * 'o, 'e) reified) =
+ { iolist = fun s0 nil cons ->
+ let next = function
+ | Nil e -> nil e
+ | Cons ((x, s), l) -> cons x s (fun e -> (reflect (l e)).iolist s0 nil cons)
+ in
+ NonLogical.(m >>= next)
+ }
+
+ let split m : ((_, _, _) list_view, _, _, _) t =
+ let rnil e = NonLogical.return (Nil e) in
+ let rcons p s l = NonLogical.return (Cons ((p, s), l)) in
+ { iolist = fun s nil cons ->
+ let open NonLogical in
+ m.iolist s rnil rcons >>= begin function
+ | Nil e -> cons (Nil e) s nil
+ | Cons ((x, s), l) ->
+ let l e = reflect (l e) in
+ cons (Cons (x, l)) s nil
+ end }
+
+ let run m s =
+ let rnil e = NonLogical.return (Nil e) in
+ let rcons x s l =
+ let p = (x, s) in
+ NonLogical.return (Cons (p, l))
+ in
+ m.iolist s rnil rcons
+
+ let repr x = x
+end
+
+module type Param = sig
+
+ (** Read only *)
+ type e
+
+ (** Write only *)
+ type w
+
+ (** [w] must be a monoid *)
+ val wunit : w
+ val wprod : w -> w -> w
+
+ (** Read-write *)
+ type s
+
+ (** Update-only. Essentially a writer on [u->u]. *)
+ type u
+
+ (** [u] must be pointed. *)
+ val uunit : u
+
+end
+
+
+module Logical (P:Param) =
+struct
+
+ module Unsafe =
+ struct
+ (** All three of environment, writer and state are coded as a single
+ state-passing-style monad.*)
+ type state = {
+ rstate : P.e;
+ ustate : P.u;
+ wstate : P.w;
+ sstate : P.s;
+ }
+
+ let make m = m
+ let repr m = m
+ end
+
+ open Unsafe
+
+ type state = Unsafe.state
+
+ type iexn = Exninfo.iexn
+
+ type 'a reified = ('a, iexn) BackState.reified
+
+ (** Inherited from Backstate *)
+
+ open BackState
+
+ include Monad.Make(struct
+ type 'a t = ('a, state, state, iexn) BackState.t
+ let return = BackState.return
+ let (>>=) = BackState.(>>=)
+ let (>>) = BackState.(>>)
+ let map = BackState.map
+ end)
+
+ let zero = BackState.zero
+ let plus = BackState.plus
+ let ignore = BackState.ignore
+ let lift = BackState.lift
+ let once = BackState.once
+ let break = BackState.break
+ let reflect = BackState.reflect
+ let split = BackState.split
+ let repr = BackState.repr
+
+ (** State related. We specialize them here to ensure soundness (for reader and
+ writer) and efficiency. *)
+
+ let get =
+ { iolist = fun s nil cons -> cons s.sstate s nil }
+
+ let set (sstate : P.s) =
+ { iolist = fun s nil cons -> cons () { s with sstate } nil }
+
+ let modify (f : P.s -> P.s) =
+ { iolist = fun s nil cons -> cons () { s with sstate = f s.sstate } nil }
+
+ let current =
+ { iolist = fun s nil cons -> cons s.rstate s nil }
+
+ let local e m =
+ { iolist = fun s nil cons ->
+ m.iolist { s with rstate = e } nil
+ (fun x s' next -> cons x {s' with rstate = s.rstate} next) }
+
+ let put w =
+ { iolist = fun s nil cons -> cons () { s with wstate = P.wprod s.wstate w } nil }
+
+ let update (f : P.u -> P.u) =
+ { iolist = fun s nil cons -> cons () { s with ustate = f s.ustate } nil }
+
+ (** Monadic run is specialized to handle reader / writer *)
+
+ let run m r s =
+ let s = { wstate = P.wunit; ustate = P.uunit; rstate = r; sstate = s } in
+ let rnil e = NonLogical.return (Nil e) in
+ let rcons x s l =
+ let p = (x, s.sstate, s.wstate, s.ustate) in
+ NonLogical.return (Cons (p, l))
+ in
+ m.iolist s rnil rcons
+
+ end
diff --git a/engine/logic_monad.mli b/engine/logic_monad.mli
new file mode 100644
index 000000000..42a84f830
--- /dev/null
+++ b/engine/logic_monad.mli
@@ -0,0 +1,215 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(** This file defines the low-level monadic operations used by the
+ tactic monad. The monad is divided into two layers: a non-logical
+ layer which consists in operations which will not (or cannot) be
+ backtracked in case of failure (input/output or persistent state)
+ and a logical layer which handles backtracking, proof
+ manipulation, and any other effect which needs to backtrack. *)
+
+
+(** {6 Exceptions} *)
+
+
+(** To help distinguish between exceptions raised by the IO monad from
+ the one used natively by Coq, the former are wrapped in
+ [Exception]. It is only used internally so that [catch] blocks of
+ the IO monad would only catch exceptions raised by the [raise]
+ function of the IO monad, and not for instance, by system
+ interrupts. Also used in [Proofview] to avoid capturing exception
+ from the IO monad ([Proofview] catches errors in its compatibility
+ layer, and when lifting goal-level expressions). *)
+exception Exception of exn
+(** This exception is used to signal abortion in [timeout] functions. *)
+exception Timeout
+(** This exception is used by the tactics to signal failure by lack of
+ successes, rather than some other exceptions (like system
+ interrupts). *)
+exception TacticFailure of exn
+
+
+(** {6 Non-logical layer} *)
+
+(** The non-logical monad is a simple [unit -> 'a] (i/o) monad. The
+ operations are simple wrappers around corresponding usual
+ operations and require little documentation. *)
+module NonLogical : sig
+
+ include Monad.S
+
+ val ignore : 'a t -> unit t
+
+ type 'a ref
+
+ val ref : 'a -> 'a ref t
+ (** [Pervasives.(:=)] *)
+ val (:=) : 'a ref -> 'a -> unit t
+ (** [Pervasives.(!)] *)
+ val (!) : 'a ref -> 'a t
+
+ val read_line : string t
+ val print_char : char -> unit t
+
+ (** Loggers. The buffer is also flushed. *)
+ val print_debug : Pp.std_ppcmds -> unit t
+ val print_warning : Pp.std_ppcmds -> unit t
+ val print_notice : Pp.std_ppcmds -> unit t
+ val print_info : Pp.std_ppcmds -> unit t
+ val print_error : Pp.std_ppcmds -> unit t
+
+ (** [Pervasives.raise]. Except that exceptions are wrapped with
+ {!Exception}. *)
+ val raise : ?info:Exninfo.info -> exn -> 'a t
+ (** [try ... with ...] but restricted to {!Exception}. *)
+ val catch : 'a t -> (Exninfo.iexn -> 'a t) -> 'a t
+ val timeout : int -> 'a t -> 'a t
+
+ (** Construct a monadified side-effect. Exceptions raised by the argument are
+ wrapped with {!Exception}. *)
+ val make : (unit -> 'a) -> 'a t
+
+ (** [run] performs effects. *)
+ val run : 'a t -> 'a
+
+end
+
+
+(** {6 Logical layer} *)
+
+(** The logical monad is a backtracking monad on top of which is
+ layered a state monad (which is used to implement all of read/write,
+ read only, and write only effects). The state monad being layered on
+ top of the backtracking monad makes it so that the state is
+ backtracked on failure.
+
+ Backtracking differs from regular exception in that, writing (+)
+ for exception catching and (>>=) for bind, we require the
+ following extra distributivity laws:
+
+ x+(y+z) = (x+y)+z
+
+ zero+x = x
+
+ x+zero = x
+
+ (x+y)>>=k = (x>>=k)+(y>>=k) *)
+
+(** A view type for the logical monad, which is a form of list, hence
+ we can decompose it with as a list. *)
+type ('a, 'b, 'e) list_view =
+| Nil of 'e
+| Cons of 'a * ('e -> 'b)
+
+module BackState : sig
+
+ type (+'a, -'i, +'o, 'e) t
+ val return : 'a -> ('a, 's, 's, 'e) t
+ val (>>=) : ('a, 'i, 'm, 'e) t -> ('a -> ('b, 'm, 'o, 'e) t) -> ('b, 'i, 'o, 'e) t
+ val (>>) : (unit, 'i, 'm, 'e) t -> ('b, 'm, 'o, 'e) t -> ('b, 'i, 'o, 'e) t
+ val map : ('a -> 'b) -> ('a, 'i, 'o, 'e) t -> ('b, 'i, 'o, 'e) t
+
+ val ignore : ('a, 'i, 'o, 'e) t -> (unit, 'i, 'o, 'e) t
+
+ val set : 'o -> (unit, 'i, 'o, 'e) t
+ val get : ('s, 's, 's, 'e) t
+ val modify : ('i -> 'o) -> (unit, 'i, 'o, 'e) t
+
+ val interleave : ('e1 -> 'e2) -> ('e2 -> 'e1) -> ('a, 'i, 'o, 'e1) t ->
+ ('a, 'i, 'o, 'e2) t
+ (** [interleave src dst m] adapts the exceptional content of the monad
+ according to the functions [src] and [dst]. To ensure a meaningful result,
+ those functions must form a retraction, i.e. [dst (src e1) = e1] for all
+ [e1]. This is typically the case when the type ['e1] is [unit]. *)
+
+ val zero : 'e -> ('a, 'i, 'o, 'e) t
+ val plus : ('a, 'i, 'o, 'e) t -> ('e -> ('a, 'i, 'o, 'e) t) -> ('a, 'i, 'o, 'e) t
+
+ val split : ('a, 's, 's, 'e) t ->
+ (('a, ('a, 'i, 's, 'e) t, 'e) list_view, 's, 's, 'e) t
+
+ val once : ('a, 'i, 'o, 'e) t -> ('a, 'i, 'o, 'e) t
+ val break : ('e -> 'e option) -> ('a, 'i, 'o, 'e) t -> ('a, 'i, 'o, 'e) t
+ val lift : 'a NonLogical.t -> ('a, 's, 's, 'e) t
+
+ type ('a, 'e) reified
+
+ val repr : ('a, 'e) reified -> ('a, ('a, 'e) reified, 'e) list_view NonLogical.t
+
+ val run : ('a, 'i, 'o, 'e) t -> 'i -> ('a * 'o, 'e) reified
+
+end
+
+(** The monad is parametrised in the types of state, environment and
+ writer. *)
+module type Param = sig
+
+ (** Read only *)
+ type e
+
+ (** Write only *)
+ type w
+
+ (** [w] must be a monoid *)
+ val wunit : w
+ val wprod : w -> w -> w
+
+ (** Read-write *)
+ type s
+
+ (** Update-only. Essentially a writer on [u->u]. *)
+ type u
+
+ (** [u] must be pointed. *)
+ val uunit : u
+
+end
+
+module Logical (P:Param) : sig
+
+ include Monad.S
+
+ val ignore : 'a t -> unit t
+
+ val set : P.s -> unit t
+ val get : P.s t
+ val modify : (P.s -> P.s) -> unit t
+ val put : P.w -> unit t
+ val current : P.e t
+ val local : P.e -> 'a t -> 'a t
+ val update : (P.u -> P.u) -> unit t
+
+ val zero : Exninfo.iexn -> 'a t
+ val plus : 'a t -> (Exninfo.iexn -> 'a t) -> 'a t
+ val split : 'a t -> ('a, 'a t, Exninfo.iexn) list_view t
+ val once : 'a t -> 'a t
+ val break : (Exninfo.iexn -> Exninfo.iexn option) -> 'a t -> 'a t
+
+ val lift : 'a NonLogical.t -> 'a t
+
+ type 'a reified = ('a, Exninfo.iexn) BackState.reified
+
+ val repr : 'a reified -> ('a, 'a reified, Exninfo.iexn) list_view NonLogical.t
+
+ val run : 'a t -> P.e -> P.s -> ('a * P.s * P.w * P.u) reified
+
+ module Unsafe :
+ sig
+ type state = {
+ rstate : P.e;
+ ustate : P.u;
+ wstate : P.w;
+ sstate : P.s;
+ }
+
+ val make : ('a, state, state, Exninfo.iexn) BackState.t -> 'a t
+ val repr : 'a t -> ('a, state, state, Exninfo.iexn) BackState.t
+
+ end
+
+end
diff --git a/engine/namegen.ml b/engine/namegen.ml
new file mode 100644
index 000000000..a88c2e20e
--- /dev/null
+++ b/engine/namegen.ml
@@ -0,0 +1,395 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* Created from contents that was formerly in termops.ml and
+ nameops.ml, Nov 2009 *)
+
+(* This file is about generating new or fresh names and dealing with
+ alpha-renaming *)
+
+open Util
+open Names
+open Term
+open Vars
+open Nametab
+open Nameops
+open Libnames
+open Globnames
+open Environ
+open Termops
+
+(**********************************************************************)
+(* Conventional names *)
+
+let default_prop_string = "H"
+let default_prop_ident = Id.of_string default_prop_string
+
+let default_small_string = "H"
+let default_small_ident = Id.of_string default_small_string
+
+let default_type_string = "X"
+let default_type_ident = Id.of_string default_type_string
+
+let default_non_dependent_string = "H"
+let default_non_dependent_ident = Id.of_string default_non_dependent_string
+
+let default_dependent_ident = Id.of_string "x"
+
+(**********************************************************************)
+(* Globality of identifiers *)
+
+let is_imported_modpath = function
+ | MPfile dp ->
+ let rec find_prefix = function
+ |MPfile dp1 -> not (DirPath.equal dp1 dp)
+ |MPdot(mp,_) -> find_prefix mp
+ |MPbound(_) -> false
+ in find_prefix (Lib.current_mp ())
+ | _ -> false
+
+let is_imported_ref = function
+ | VarRef _ -> false
+ | IndRef (kn,_)
+ | ConstructRef ((kn,_),_) ->
+ let (mp,_,_) = repr_mind kn in is_imported_modpath mp
+ | ConstRef kn ->
+ let (mp,_,_) = repr_con kn in is_imported_modpath mp
+
+let is_global id =
+ try
+ let ref = locate (qualid_of_ident id) in
+ not (is_imported_ref ref)
+ with Not_found ->
+ false
+
+let is_constructor id =
+ try
+ match locate (qualid_of_ident id) with
+ | ConstructRef _ -> true
+ | _ -> false
+ with Not_found ->
+ false
+
+(**********************************************************************)
+(* Generating "intuitive" names from its type *)
+
+let head_name c = (* Find the head constant of a constr if any *)
+ let rec hdrec c =
+ match kind_of_term c with
+ | Prod (_,_,c) | Lambda (_,_,c) | LetIn (_,_,_,c)
+ | Cast (c,_,_) | App (c,_) -> hdrec c
+ | Proj (kn,_) -> Some (Label.to_id (con_label (Projection.constant kn)))
+ | Const _ | Ind _ | Construct _ | Var _ ->
+ Some (basename_of_global (global_of_constr c))
+ | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) ->
+ Some (match lna.(i) with Name id -> id | _ -> assert false)
+ | Sort _ | Rel _ | Meta _|Evar _|Case (_, _, _, _) -> None
+ in
+ hdrec c
+
+let lowercase_first_char id = (* First character of a constr *)
+ Unicode.lowercase_first_char (Id.to_string id)
+
+let sort_hdchar = function
+ | Prop(_) -> "P"
+ | Type(_) -> "T"
+
+let hdchar env c =
+ let rec hdrec k c =
+ match kind_of_term c with
+ | Prod (_,_,c) | Lambda (_,_,c) | LetIn (_,_,_,c) -> hdrec (k+1) c
+ | Cast (c,_,_) | App (c,_) -> hdrec k c
+ | Proj (kn,_) -> lowercase_first_char (Label.to_id (con_label (Projection.constant kn)))
+ | Const (kn,_) -> lowercase_first_char (Label.to_id (con_label kn))
+ | Ind (x,_) -> lowercase_first_char (basename_of_global (IndRef x))
+ | Construct (x,_) -> lowercase_first_char (basename_of_global (ConstructRef x))
+ | Var id -> lowercase_first_char id
+ | Sort s -> sort_hdchar s
+ | Rel n ->
+ (if n<=k then "p" (* the initial term is flexible product/function *)
+ else
+ try match Environ.lookup_rel (n-k) env with
+ | (Name id,_,_) -> lowercase_first_char id
+ | (Anonymous,_,t) -> hdrec 0 (lift (n-k) t)
+ with Not_found -> "y")
+ | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) ->
+ let id = match lna.(i) with Name id -> id | _ -> assert false in
+ lowercase_first_char id
+ | Evar _ (* We could do better... *)
+ | Meta _ | Case (_, _, _, _) -> "y"
+ in
+ hdrec 0 c
+
+let id_of_name_using_hdchar env a = function
+ | Anonymous -> Id.of_string (hdchar env a)
+ | Name id -> id
+
+let named_hd env a = function
+ | Anonymous -> Name (Id.of_string (hdchar env a))
+ | x -> x
+
+let mkProd_name env (n,a,b) = mkProd (named_hd env a n, a, b)
+let mkLambda_name env (n,a,b) = mkLambda (named_hd env a n, a, b)
+
+let lambda_name = mkLambda_name
+let prod_name = mkProd_name
+
+let prod_create env (a,b) = mkProd (named_hd env a Anonymous, a, b)
+let lambda_create env (a,b) = mkLambda (named_hd env a Anonymous, a, b)
+
+let name_assumption env (na,c,t) =
+ match c with
+ | None -> (named_hd env t na, None, t)
+ | Some body -> (named_hd env body na, c, t)
+
+let name_context env hyps =
+ snd
+ (List.fold_left
+ (fun (env,hyps) d ->
+ let d' = name_assumption env d in (push_rel d' env, d' :: hyps))
+ (env,[]) (List.rev hyps))
+
+let mkProd_or_LetIn_name env b d = mkProd_or_LetIn (name_assumption env d) b
+let mkLambda_or_LetIn_name env b d = mkLambda_or_LetIn (name_assumption env d)b
+
+let it_mkProd_or_LetIn_name env b hyps =
+ it_mkProd_or_LetIn b (name_context env hyps)
+let it_mkLambda_or_LetIn_name env b hyps =
+ it_mkLambda_or_LetIn b (name_context env hyps)
+
+(**********************************************************************)
+(* Fresh names *)
+
+(* Looks for next "good" name by lifting subscript *)
+
+let next_ident_away_from id bad =
+ let rec name_rec id = if bad id then name_rec (lift_subscript id) else id in
+ name_rec id
+
+(* Restart subscript from x0 if name starts with xN, or x00 if name
+ starts with x0N, etc *)
+
+let restart_subscript id =
+ if not (has_subscript id) then id else
+ (* It would probably be better with something in the spirit of
+ *** make_ident id (Some 0) *** but compatibility would be lost... *)
+ forget_subscript id
+
+let rec to_avoid id = function
+| [] -> false
+| id' :: avoid -> Id.equal id id' || to_avoid id avoid
+
+let occur_rel p env id =
+ try
+ let name = lookup_name_of_rel p env in
+ begin match name with
+ | Name id' -> Id.equal id' id
+ | Anonymous -> false
+ end
+ with Not_found -> false (* Unbound indice : may happen in debug *)
+
+let visibly_occur_id id (nenv,c) =
+ let rec occur n c = match kind_of_term c with
+ | Const _ | Ind _ | Construct _ | Var _
+ when
+ let short = shortest_qualid_of_global Id.Set.empty (global_of_constr c) in
+ qualid_eq short (qualid_of_ident id) ->
+ raise Occur
+ | Rel p when p>n && occur_rel (p-n) nenv id -> raise Occur
+ | _ -> iter_constr_with_binders succ occur n c
+ in
+ try occur 1 c; false
+ with Occur -> true
+ | Not_found -> false (* Happens when a global is not in the env *)
+
+(* Now, there are different renaming strategies... *)
+
+(* 1- Looks for a fresh name for printing in cases pattern *)
+
+let next_name_away_in_cases_pattern env_t na avoid =
+ let id = match na with Name id -> id | Anonymous -> default_dependent_ident in
+ let bad id = to_avoid id avoid || is_constructor id
+ || visibly_occur_id id env_t in
+ next_ident_away_from id bad
+
+(* 2- Looks for a fresh name for introduction in goal *)
+
+(* The legacy strategy for renaming introduction variables is not very uniform:
+ - if the name to use is fresh in the context but used as a global
+ name, then a fresh name is taken by finding a free subscript
+ starting from the current subscript;
+ - but if the name to use is not fresh in the current context, the fresh
+ name is taken by finding a free subscript starting from 0 *)
+
+let next_ident_away_in_goal id avoid =
+ let id = if to_avoid id avoid then restart_subscript id else id in
+ let bad id = to_avoid id avoid || (is_global id && not (is_section_variable id)) in
+ next_ident_away_from id bad
+
+let next_name_away_in_goal na avoid =
+ let id = match na with
+ | Name id -> id
+ | Anonymous -> default_non_dependent_ident in
+ next_ident_away_in_goal id avoid
+
+(* 3- Looks for next fresh name outside a list that is moreover valid
+ as a global identifier; the legacy algorithm is that if the name is
+ already used in the list, one looks for a name of same base with
+ lower available subscript; if the name is not in the list but is
+ used globally, one looks for a name of same base with lower subscript
+ beyond the current subscript *)
+
+let next_global_ident_away id avoid =
+ let id = if to_avoid id avoid then restart_subscript id else id in
+ let bad id = to_avoid id avoid || is_global id in
+ next_ident_away_from id bad
+
+(* 4- Looks for next fresh name outside a list; if name already used,
+ looks for same name with lower available subscript *)
+
+let next_ident_away id avoid =
+ if to_avoid id avoid then
+ next_ident_away_from (restart_subscript id) (fun id -> to_avoid id avoid)
+ else id
+
+let next_name_away_with_default default na avoid =
+ let id = match na with Name id -> id | Anonymous -> Id.of_string default in
+ next_ident_away id avoid
+
+let reserved_type_name = ref (fun t -> Anonymous)
+let set_reserved_typed_name f = reserved_type_name := f
+
+let next_name_away_with_default_using_types default na avoid t =
+ let id = match na with
+ | Name id -> id
+ | Anonymous -> match !reserved_type_name t with
+ | Name id -> id
+ | Anonymous -> Id.of_string default in
+ next_ident_away id avoid
+
+let next_name_away = next_name_away_with_default default_non_dependent_string
+
+let make_all_name_different env =
+ let avoid = ref (ids_of_named_context (named_context env)) in
+ process_rel_context
+ (fun (na,c,t) newenv ->
+ let na = named_hd newenv t na in
+ let id = next_name_away na !avoid in
+ avoid := id::!avoid;
+ push_rel (Name id,c,t) newenv)
+ env
+
+(* 5- Looks for next fresh name outside a list; avoids also to use names that
+ would clash with short name of global references; if name is already used,
+ looks for name of same base with lower available subscript beyond current
+ subscript *)
+
+let next_ident_away_for_default_printing env_t id avoid =
+ let bad id = to_avoid id avoid || visibly_occur_id id env_t in
+ next_ident_away_from id bad
+
+let next_name_away_for_default_printing env_t na avoid =
+ let id = match na with
+ | Name id -> id
+ | Anonymous ->
+ (* In principle, an anonymous name is not dependent and will not be *)
+ (* taken into account by the function compute_displayed_name_in; *)
+ (* just in case, invent a valid name *)
+ default_non_dependent_ident in
+ next_ident_away_for_default_printing env_t id avoid
+
+(**********************************************************************)
+(* Displaying terms avoiding bound variables clashes *)
+
+(* Renaming strategy introduced in December 1998:
+
+ - Rule number 1: all names, even if unbound and not displayed, contribute
+ to the list of names to avoid
+ - Rule number 2: only the dependency status is used for deciding if
+ a name is displayed or not
+
+ Example:
+ bool_ind: "forall (P:bool->Prop)(f:(P true))(f:(P false))(b:bool), P b" is
+ displayed "forall P:bool->Prop, P true -> P false -> forall b:bool, P b"
+ but f and f0 contribute to the list of variables to avoid (knowing
+ that f and f0 are how the f's would be named if introduced, assuming
+ no other f and f0 are already used).
+*)
+
+type renaming_flags =
+ | RenamingForCasesPattern of (Name.t list * constr)
+ | RenamingForGoal
+ | RenamingElsewhereFor of (Name.t list * constr)
+
+let next_name_for_display flags =
+ match flags with
+ | RenamingForCasesPattern env_t -> next_name_away_in_cases_pattern env_t
+ | RenamingForGoal -> next_name_away_in_goal
+ | RenamingElsewhereFor env_t -> next_name_away_for_default_printing env_t
+
+(* Remark: Anonymous var may be dependent in Evar's contexts *)
+let compute_displayed_name_in flags avoid na c =
+ match na with
+ | Anonymous when noccurn 1 c ->
+ (Anonymous,avoid)
+ | _ ->
+ let fresh_id = next_name_for_display flags na avoid in
+ let idopt = if noccurn 1 c then Anonymous else Name fresh_id in
+ (idopt, fresh_id::avoid)
+
+let compute_and_force_displayed_name_in flags avoid na c =
+ match na with
+ | Anonymous when noccurn 1 c ->
+ (Anonymous,avoid)
+ | _ ->
+ let fresh_id = next_name_for_display flags na avoid in
+ (Name fresh_id, fresh_id::avoid)
+
+let compute_displayed_let_name_in flags avoid na c =
+ let fresh_id = next_name_for_display flags na avoid in
+ (Name fresh_id, fresh_id::avoid)
+
+let rename_bound_vars_as_displayed avoid env c =
+ let rec rename avoid env c =
+ match kind_of_term c with
+ | Prod (na,c1,c2) ->
+ let na',avoid' =
+ compute_displayed_name_in
+ (RenamingElsewhereFor (env,c2)) avoid na c2 in
+ mkProd (na', c1, rename avoid' (add_name na' env) c2)
+ | LetIn (na,c1,t,c2) ->
+ let na',avoid' =
+ compute_displayed_let_name_in
+ (RenamingElsewhereFor (env,c2)) avoid na c2 in
+ mkLetIn (na',c1,t, rename avoid' (add_name na' env) c2)
+ | Cast (c,k,t) -> mkCast (rename avoid env c, k,t)
+ | _ -> c
+ in
+ rename avoid env c
+
+(**********************************************************************)
+(* "H"-based naming strategy introduced June 2014 for hypotheses in
+ Prop produced by case/elim/destruct/induction, in place of the
+ strategy that was using the first letter of the type, leading to
+ inelegant "n:~A", "e:t=u", etc. when eliminating sumbool or similar
+ types *)
+
+let h_based_elimination_names = ref false
+
+let use_h_based_elimination_names () =
+ !h_based_elimination_names && Flags.version_strictly_greater Flags.V8_4
+
+open Goptions
+
+let _ = declare_bool_option
+ { optsync = true;
+ optdepr = false;
+ optname = "use of \"H\"-based proposition names in elimination tactics";
+ optkey = ["Standard";"Proposition";"Elimination";"Names"];
+ optread = (fun () -> !h_based_elimination_names);
+ optwrite = (:=) h_based_elimination_names }
diff --git a/engine/namegen.mli b/engine/namegen.mli
new file mode 100644
index 000000000..f66bc6d88
--- /dev/null
+++ b/engine/namegen.mli
@@ -0,0 +1,102 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Names
+open Term
+open Context
+open Environ
+
+(*********************************************************************
+ Conventional default names *)
+
+val default_prop_ident : Id.t (* "H" *)
+val default_small_ident : Id.t (* "H" *)
+val default_type_ident : Id.t (* "X" *)
+val default_non_dependent_ident : Id.t (* "H" *)
+val default_dependent_ident : Id.t (* "x" *)
+
+(*********************************************************************
+ Generating "intuitive" names from their type *)
+
+val lowercase_first_char : Id.t -> string
+val sort_hdchar : sorts -> string
+val hdchar : env -> types -> string
+val id_of_name_using_hdchar : env -> types -> Name.t -> Id.t
+val named_hd : env -> types -> Name.t -> Name.t
+val head_name : types -> Id.t option
+
+val mkProd_name : env -> Name.t * types * types -> types
+val mkLambda_name : env -> Name.t * types * constr -> constr
+
+(** Deprecated synonyms of [mkProd_name] and [mkLambda_name] *)
+val prod_name : env -> Name.t * types * types -> types
+val lambda_name : env -> Name.t * types * constr -> constr
+
+val prod_create : env -> types * types -> constr
+val lambda_create : env -> types * constr -> constr
+val name_assumption : env -> rel_declaration -> rel_declaration
+val name_context : env -> rel_context -> rel_context
+
+val mkProd_or_LetIn_name : env -> types -> rel_declaration -> types
+val mkLambda_or_LetIn_name : env -> constr -> rel_declaration -> constr
+val it_mkProd_or_LetIn_name : env -> types -> rel_context -> types
+val it_mkLambda_or_LetIn_name : env -> constr -> rel_context -> constr
+
+(*********************************************************************
+ Fresh names *)
+
+(** Avoid clashing with a name satisfying some predicate *)
+val next_ident_away_from : Id.t -> (Id.t -> bool) -> Id.t
+
+(** Avoid clashing with a name of the given list *)
+val next_ident_away : Id.t -> Id.t list -> Id.t
+
+(** Avoid clashing with a name already used in current module *)
+val next_ident_away_in_goal : Id.t -> Id.t list -> Id.t
+
+(** Avoid clashing with a name already used in current module
+ but tolerate overwriting section variables, as in goals *)
+val next_global_ident_away : Id.t -> Id.t list -> Id.t
+
+(** Avoid clashing with a constructor name already used in current module *)
+val next_name_away_in_cases_pattern : (Termops.names_context * constr) -> Name.t -> Id.t list -> Id.t
+
+(** Default is [default_non_dependent_ident] *)
+val next_name_away : Name.t -> Id.t list -> Id.t
+
+val next_name_away_with_default : string -> Name.t -> Id.t list ->
+ Id.t
+
+val next_name_away_with_default_using_types : string -> Name.t ->
+ Id.t list -> types -> Id.t
+
+val set_reserved_typed_name : (types -> Name.t) -> unit
+
+(*********************************************************************
+ Making name distinct for displaying *)
+
+type renaming_flags =
+ | RenamingForCasesPattern of (Name.t list * constr) (** avoid only global constructors *)
+ | RenamingForGoal (** avoid all globals (as in intro) *)
+ | RenamingElsewhereFor of (Name.t list * constr)
+
+val make_all_name_different : env -> env
+
+val compute_displayed_name_in :
+ renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list
+val compute_and_force_displayed_name_in :
+ renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list
+val compute_displayed_let_name_in :
+ renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list
+val rename_bound_vars_as_displayed :
+ Id.t list -> Name.t list -> types -> types
+
+(**********************************************************************)
+(* Naming strategy for arguments in Prop when eliminating inductive types *)
+
+val use_h_based_elimination_names : unit -> bool
diff --git a/engine/proofview_monad.ml b/engine/proofview_monad.ml
new file mode 100644
index 000000000..6e68cd2e4
--- /dev/null
+++ b/engine/proofview_monad.ml
@@ -0,0 +1,270 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(** This file defines the datatypes used as internal states by the
+ tactic monad, and specialises the [Logic_monad] to these type. *)
+
+(** {6 Trees/forest for traces} *)
+
+module Trace = struct
+
+ (** The intent is that an ['a forest] is a list of messages of type
+ ['a]. But messages can stand for a list of more precise
+ messages, hence the structure is organised as a tree. *)
+ type 'a forest = 'a tree list
+ and 'a tree = Seq of 'a * 'a forest
+
+ (** To build a trace incrementally, we use an intermediary data
+ structure on which we can define an S-expression like language
+ (like a simplified xml except the closing tags do not carry a
+ name). Note that nodes are built from right to left in ['a
+ incr], the result is mirrored when returning so that in the
+ exposed interface, the forest is read from left to right.
+
+ Concretely, we want to add a new tree to a forest: and we are
+ building it by adding new trees to the left of its left-most
+ subtrees which is built the same way. *)
+ type 'a incr = { head:'a forest ; opened: 'a tree list }
+
+ (** S-expression like language as ['a incr] transformers. It is the
+ responsibility of the library builder not to use [close] when no
+ tag is open. *)
+ let empty_incr = { head=[] ; opened=[] }
+ let opn a { head ; opened } = { head ; opened = Seq(a,[])::opened }
+ let close { head ; opened } =
+ match opened with
+ | [a] -> { head = a::head ; opened=[] }
+ | a::Seq(b,f)::opened -> { head ; opened=Seq(b,a::f)::opened }
+ | [] -> assert false
+ let leaf a s = close (opn a s)
+
+ (** Returning a forest. It is the responsibility of the library
+ builder to close all the tags. *)
+ (* spiwack: I may want to close the tags instead, to deal with
+ interruptions. *)
+ let rec mirror f = List.rev_map mirror_tree f
+ and mirror_tree (Seq(a,f)) = Seq(a,mirror f)
+
+ let to_tree = function
+ | { head ; opened=[] } -> mirror head
+ | { head ; opened=_::_} -> assert false
+
+end
+
+
+
+(** {6 State types} *)
+
+(** We typically label nodes of [Trace.tree] with messages to
+ print. But we don't want to compute the result. *)
+type lazy_msg = unit -> Pp.std_ppcmds
+let pr_lazy_msg msg = msg ()
+
+(** Info trace. *)
+module Info = struct
+
+ (** The type of the tags for [info]. *)
+ type tag =
+ | Msg of lazy_msg (** A simple message *)
+ | Tactic of lazy_msg (** A tactic call *)
+ | Dispatch (** A call to [tclDISPATCH]/[tclEXTEND] *)
+ | DBranch (** A special marker to delimit individual branch of a dispatch. *)
+
+ type state = tag Trace.incr
+ type tree = tag Trace.forest
+
+
+
+ let pr_in_comments m = Pp.(str"(* "++pr_lazy_msg m++str" *)")
+
+ let unbranch = function
+ | Trace.Seq (DBranch,brs) -> brs
+ | _ -> assert false
+
+
+ let is_empty_branch = let open Trace in function
+ | Seq(DBranch,[]) -> true
+ | _ -> false
+
+ (** Dispatch with empty branches are (supposed to be) equivalent to
+ [idtac] which need not appear, so they are removed from the
+ trace. *)
+ let dispatch brs =
+ let open Trace in
+ if CList.for_all is_empty_branch brs then None
+ else Some (Seq(Dispatch,brs))
+
+ let constr = let open Trace in function
+ | Dispatch -> dispatch
+ | t -> fun br -> Some (Seq(t,br))
+
+ let rec compress_tree = let open Trace in function
+ | Seq(t,f) -> constr t (compress f)
+ and compress f =
+ CList.map_filter compress_tree f
+
+ let rec is_empty = let open Trace in function
+ | Seq(Dispatch,brs) -> List.for_all is_empty brs
+ | Seq(DBranch,br) -> List.for_all is_empty br
+ | _ -> false
+
+ (** [with_sep] is [true] when [Tactic m] must be printed with a
+ trailing semi-colon. *)
+ let rec pr_tree with_sep = let open Trace in function
+ | Seq (Msg m,[]) -> pr_in_comments m
+ | Seq (Tactic m,_) ->
+ let tail = if with_sep then Pp.str";" else Pp.mt () in
+ Pp.(pr_lazy_msg m ++ tail)
+ | Seq (Dispatch,brs) ->
+ let tail = if with_sep then Pp.str";" else Pp.mt () in
+ Pp.(pr_dispatch brs++tail)
+ | Seq (Msg _,_::_) | Seq (DBranch,_) -> assert false
+ and pr_dispatch brs =
+ let open Pp in
+ let brs = List.map unbranch brs in
+ match brs with
+ | [br] -> pr_forest br
+ | _ ->
+ let sep () = spc()++str"|"++spc() in
+ let branches = prlist_with_sep sep pr_forest brs in
+ str"[>"++spc()++branches++spc()++str"]"
+ and pr_forest = function
+ | [] -> Pp.mt ()
+ | [tr] -> pr_tree false tr
+ | tr::l -> Pp.(pr_tree true tr ++ pr_forest l)
+
+ let print f =
+ pr_forest (compress f)
+
+ let rec collapse_tree n t =
+ let open Trace in
+ match n , t with
+ | 0 , t -> [t]
+ | _ , (Seq(Tactic _,[]) as t) -> [t]
+ | n , Seq(Tactic _,f) -> collapse (pred n) f
+ | n , Seq(Dispatch,brs) -> [Seq(Dispatch, (collapse n brs))]
+ | n , Seq(DBranch,br) -> [Seq(DBranch, (collapse n br))]
+ | _ , (Seq(Msg _,_) as t) -> [t]
+ and collapse n f =
+ CList.map_append (collapse_tree n) f
+end
+
+
+(** Type of proof views: current [evar_map] together with the list of
+ focused goals. *)
+type proofview = { solution : Evd.evar_map; comb : Goal.goal list }
+
+
+(** {6 Instantiation of the logic monad} *)
+
+(** Parameters of the logic monads *)
+module P = struct
+
+ type s = proofview * Environ.env
+
+ (** Recording info trace (true) or not. *)
+ type e = bool
+
+ (** Status (safe/unsafe) * shelved goals * given up *)
+ type w = bool * Evar.t list * Evar.t list
+
+ let wunit = true , [] , []
+ let wprod (b1,s1,g1) (b2,s2,g2) = b1 && b2 , s1@s2 , g1@g2
+
+ type u = Info.state
+
+ let uunit = Trace.empty_incr
+
+end
+
+module Logical = Logic_monad.Logical(P)
+
+
+(** {6 Lenses to access to components of the states} *)
+
+module type State = sig
+ type t
+ val get : t Logical.t
+ val set : t -> unit Logical.t
+ val modify : (t->t) -> unit Logical.t
+end
+
+module type Writer = sig
+ type t
+ val put : t -> unit Logical.t
+end
+
+module Pv : State with type t := proofview = struct
+ let get = Logical.(map fst get)
+ let set p = Logical.modify (fun (_,e) -> (p,e))
+ let modify f= Logical.modify (fun (p,e) -> (f p,e))
+end
+
+module Solution : State with type t := Evd.evar_map = struct
+ let get = Logical.map (fun {solution} -> solution) Pv.get
+ let set s = Pv.modify (fun pv -> { pv with solution = s })
+ let modify f = Pv.modify (fun pv -> { pv with solution = f pv.solution })
+end
+
+module Comb : State with type t = Evar.t list = struct
+ (* spiwack: I don't know why I cannot substitute ([:=]) [t] with a type expression. *)
+ type t = Evar.t list
+ let get = Logical.map (fun {comb} -> comb) Pv.get
+ let set c = Pv.modify (fun pv -> { pv with comb = c })
+ let modify f = Pv.modify (fun pv -> { pv with comb = f pv.comb })
+end
+
+module Env : State with type t := Environ.env = struct
+ let get = Logical.(map snd get)
+ let set e = Logical.modify (fun (p,_) -> (p,e))
+ let modify f = Logical.modify (fun (p,e) -> (p,f e))
+end
+
+module Status : Writer with type t := bool = struct
+ let put s = Logical.put (s,[],[])
+end
+
+module Shelf : Writer with type t = Evar.t list = struct
+ (* spiwack: I don't know why I cannot substitute ([:=]) [t] with a type expression. *)
+ type t = Evar.t list
+ let put sh = Logical.put (true,sh,[])
+end
+
+module Giveup : Writer with type t = Evar.t list = struct
+ (* spiwack: I don't know why I cannot substitute ([:=]) [t] with a type expression. *)
+ type t = Evar.t list
+ let put gs = Logical.put (true,[],gs)
+end
+
+(** Lens and utilies pertaining to the info trace *)
+module InfoL = struct
+ let recording = Logical.current
+ let if_recording t =
+ let open Logical in
+ recording >>= fun r ->
+ if r then t else return ()
+
+ let record_trace t = Logical.local true t
+
+ let raw_update = Logical.update
+ let update f = if_recording (raw_update f)
+ let opn a = update (Trace.opn a)
+ let close = update Trace.close
+ let leaf a = update (Trace.leaf a)
+
+ let tag a t =
+ let open Logical in
+ recording >>= fun r ->
+ if r then begin
+ raw_update (Trace.opn a) >>
+ t >>= fun a ->
+ raw_update Trace.close >>
+ return a
+ end else
+ t
+end
diff --git a/engine/proofview_monad.mli b/engine/proofview_monad.mli
new file mode 100644
index 000000000..d2a2e55fb
--- /dev/null
+++ b/engine/proofview_monad.mli
@@ -0,0 +1,144 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(** This file defines the datatypes used as internal states by the
+ tactic monad, and specialises the [Logic_monad] to these type. *)
+
+(** {6 Traces} *)
+
+module Trace : sig
+
+ (** The intent is that an ['a forest] is a list of messages of type
+ ['a]. But messages can stand for a list of more precise
+ messages, hence the structure is organised as a tree. *)
+ type 'a forest = 'a tree list
+ and 'a tree = Seq of 'a * 'a forest
+
+ (** To build a trace incrementally, we use an intermediary data
+ structure on which we can define an S-expression like language
+ (like a simplified xml except the closing tags do not carry a
+ name). *)
+ type 'a incr
+ val to_tree : 'a incr -> 'a forest
+
+ (** [open a] opens a tag with name [a]. *)
+ val opn : 'a -> 'a incr -> 'a incr
+
+ (** [close] closes the last open tag. It is the responsibility of
+ the user to close all the tags. *)
+ val close : 'a incr -> 'a incr
+
+ (** [leaf] creates an empty tag with name [a]. *)
+ val leaf : 'a -> 'a incr -> 'a incr
+
+end
+
+(** {6 State types} *)
+
+(** We typically label nodes of [Trace.tree] with messages to
+ print. But we don't want to compute the result. *)
+type lazy_msg = unit -> Pp.std_ppcmds
+
+(** Info trace. *)
+module Info : sig
+
+ (** The type of the tags for [info]. *)
+ type tag =
+ | Msg of lazy_msg (** A simple message *)
+ | Tactic of lazy_msg (** A tactic call *)
+ | Dispatch (** A call to [tclDISPATCH]/[tclEXTEND] *)
+ | DBranch (** A special marker to delimit individual branch of a dispatch. *)
+
+ type state = tag Trace.incr
+ type tree = tag Trace.forest
+
+ val print : tree -> Pp.std_ppcmds
+
+ (** [collapse n t] flattens the first [n] levels of [Tactic] in an
+ info trace, effectively forgetting about the [n] top level of
+ names (if there are fewer, the last name is kept). *)
+ val collapse : int -> tree -> tree
+
+end
+
+(** Type of proof views: current [evar_map] together with the list of
+ focused goals. *)
+type proofview = { solution : Evd.evar_map; comb : Goal.goal list }
+
+(** {6 Instantiation of the logic monad} *)
+
+module P : sig
+ type s = proofview * Environ.env
+
+ (** Status (safe/unsafe) * shelved goals * given up *)
+ type w = bool * Evar.t list * Evar.t list
+
+ val wunit : w
+ val wprod : w -> w -> w
+
+ (** Recording info trace (true) or not. *)
+ type e = bool
+
+ type u = Info.state
+
+ val uunit : u
+end
+
+module Logical : module type of Logic_monad.Logical(P)
+
+
+(** {6 Lenses to access to components of the states} *)
+
+module type State = sig
+ type t
+ val get : t Logical.t
+ val set : t -> unit Logical.t
+ val modify : (t->t) -> unit Logical.t
+end
+
+module type Writer = sig
+ type t
+ val put : t -> unit Logical.t
+end
+
+(** Lens to the [proofview]. *)
+module Pv : State with type t := proofview
+
+(** Lens to the [evar_map] of the proofview. *)
+module Solution : State with type t := Evd.evar_map
+
+(** Lens to the list of focused goals. *)
+module Comb : State with type t = Evar.t list
+
+(** Lens to the global environment. *)
+module Env : State with type t := Environ.env
+
+(** Lens to the tactic status ([true] if safe, [false] if unsafe) *)
+module Status : Writer with type t := bool
+
+(** Lens to the list of goals which have been shelved during the
+ execution of the tactic. *)
+module Shelf : Writer with type t = Evar.t list
+
+(** Lens to the list of goals which were given up during the execution
+ of the tactic. *)
+module Giveup : Writer with type t = Evar.t list
+
+(** Lens and utilies pertaining to the info trace *)
+module InfoL : sig
+ (** [record_trace t] behaves like [t] and compute its [info] trace. *)
+ val record_trace : 'a Logical.t -> 'a Logical.t
+
+ val update : (Info.state -> Info.state) -> unit Logical.t
+ val opn : Info.tag -> unit Logical.t
+ val close : unit Logical.t
+ val leaf : Info.tag -> unit Logical.t
+
+ (** [tag a t] opens tag [a] runs [t] then closes the tag. *)
+ val tag : Info.tag -> 'a Logical.t -> 'a Logical.t
+end
diff --git a/engine/sigma.ml b/engine/sigma.ml
new file mode 100644
index 000000000..e886b0d1e
--- /dev/null
+++ b/engine/sigma.ml
@@ -0,0 +1,105 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+type 'a t = Evd.evar_map
+
+type ('a, 'b) le = unit
+
+let refl = ()
+let cons _ _ = ()
+let (+>) = fun _ _ -> ()
+
+type ('a, 'r) sigma = Sigma : 'a * 's t * ('r, 's) le -> ('a, 'r) sigma
+
+type 'a evar = Evar.t
+
+let lift_evar evk () = evk
+
+let to_evar_map evd = evd
+let to_evar evk = evk
+
+let here x s = Sigma (x, s, ())
+
+(** API *)
+
+type 'r fresh = Fresh : 's evar * 's t * ('r, 's) le -> 'r fresh
+
+let new_evar sigma ?naming info =
+ let (sigma, evk) = Evd.new_evar sigma ?naming info in
+ Fresh (evk, sigma, ())
+
+let define evk c sigma =
+ Sigma ((), Evd.define evk c sigma, ())
+
+let fresh_sort_in_family ?rigid env sigma s =
+ let (sigma, s) = Evd.fresh_sort_in_family ?rigid env sigma s in
+ Sigma (s, sigma, ())
+
+let fresh_constant_instance env sigma cst =
+ let (sigma, cst) = Evd.fresh_constant_instance env sigma cst in
+ Sigma (cst, sigma, ())
+
+let fresh_inductive_instance env sigma ind =
+ let (sigma, ind) = Evd.fresh_inductive_instance env sigma ind in
+ Sigma (ind, sigma, ())
+
+let fresh_constructor_instance env sigma pc =
+ let (sigma, c) = Evd.fresh_constructor_instance env sigma pc in
+ Sigma (c, sigma, ())
+
+let fresh_global ?rigid ?names env sigma r =
+ let (sigma, c) = Evd.fresh_global ?rigid ?names env sigma r in
+ Sigma (c, sigma, ())
+
+(** Run *)
+
+type 'a run = { run : 'r. 'r t -> ('a, 'r) sigma }
+
+let run sigma f : 'a * Evd.evar_map =
+ let Sigma (x, sigma, ()) = f.run sigma in
+ (x, sigma)
+
+(** Monotonic references *)
+
+type evdref = Evd.evar_map ref
+
+let apply evdref f =
+ let Sigma (x, sigma, ()) = f.run !evdref in
+ evdref := sigma;
+ x
+
+let purify f =
+ let f (sigma : Evd.evar_map) =
+ let evdref = ref sigma in
+ let ans = f evdref in
+ Sigma (ans, !evdref, ())
+ in
+ { run = f }
+
+(** Unsafe primitives *)
+
+module Unsafe =
+struct
+
+let le = ()
+let of_evar_map sigma = sigma
+let of_evar evk = evk
+let of_ref ref = ref
+let of_pair (x, sigma) = Sigma (x, sigma, ())
+
+end
+
+module Notations =
+struct
+ type ('a, 'r) sigma_ = ('a, 'r) sigma =
+ Sigma : 'a * 's t * ('r, 's) le -> ('a, 'r) sigma_
+
+ let (+>) = fun _ _ -> ()
+
+ type 'a run_ = 'a run = { run : 'r. 'r t -> ('a, 'r) sigma }
+end
diff --git a/engine/sigma.mli b/engine/sigma.mli
new file mode 100644
index 000000000..cb948dba5
--- /dev/null
+++ b/engine/sigma.mli
@@ -0,0 +1,122 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Names
+open Constr
+
+(** Monotonous state enforced by typing.
+
+ This module allows to constrain uses of evarmaps in a monotonous fashion,
+ and in particular statically suppress evar leaks and the like.
+*)
+
+(** {5 Stages} *)
+
+type ('a, 'b) le
+(** Relationship stating that stage ['a] is anterior to stage ['b] *)
+
+val refl : ('a, 'a) le
+(** Reflexivity of anteriority *)
+
+val cons : ('a, 'b) le -> ('b, 'c) le -> ('a, 'c) le
+(** Transitivity of anteriority *)
+
+val (+>) : ('a, 'b) le -> ('b, 'c) le -> ('a, 'c) le
+(** Alias for {!cons} *)
+
+(** {5 Monotonous evarmaps} *)
+
+type 'r t
+(** Stage-indexed evarmaps. *)
+
+type ('a, 'r) sigma = Sigma : 'a * 's t * ('r, 's) le -> ('a, 'r) sigma
+(** Return values at a later stage *)
+
+type 'r evar
+(** Stage-indexed evars *)
+
+(** {5 Constructors} *)
+
+val here : 'a -> 'r t -> ('a, 'r) sigma
+(** [here x s] is a shorthand for [Sigma (x, s, refl)] *)
+
+(** {5 Postponing} *)
+
+val lift_evar : 'r evar -> ('r, 's) le -> 's evar
+(** Any evar existing at stage ['r] is also valid at any later stage. *)
+
+(** {5 Downcasting} *)
+
+val to_evar_map : 'r t -> Evd.evar_map
+val to_evar : 'r evar -> Evar.t
+
+(** {5 Monotonous API} *)
+
+type 'r fresh = Fresh : 's evar * 's t * ('r, 's) le -> 'r fresh
+
+val new_evar : 'r t -> ?naming:Misctypes.intro_pattern_naming_expr ->
+ Evd.evar_info -> 'r fresh
+
+val define : 'r evar -> Constr.t -> 'r t -> (unit, 'r) sigma
+
+(** Polymorphic universes *)
+
+val fresh_sort_in_family : ?rigid:Evd.rigid -> Environ.env ->
+ 'r t -> Term.sorts_family -> (Term.sorts, 'r) sigma
+val fresh_constant_instance :
+ Environ.env -> 'r t -> constant -> (pconstant, 'r) sigma
+val fresh_inductive_instance :
+ Environ.env -> 'r t -> inductive -> (pinductive, 'r) sigma
+val fresh_constructor_instance : Environ.env -> 'r t -> constructor ->
+ (pconstructor, 'r) sigma
+
+val fresh_global : ?rigid:Evd.rigid -> ?names:Univ.Instance.t -> Environ.env ->
+ 'r t -> Globnames.global_reference -> (constr, 'r) sigma
+
+(** FILLME *)
+
+(** {5 Run} *)
+
+type 'a run = { run : 'r. 'r t -> ('a, 'r) sigma }
+
+val run : Evd.evar_map -> 'a run -> 'a * Evd.evar_map
+
+(** {5 Imperative monotonic functions} *)
+
+type evdref
+(** Monotonic references over evarmaps *)
+
+val apply : evdref -> 'a run -> 'a
+(** Apply a monotonic function on a reference. *)
+
+val purify : (evdref -> 'a) -> 'a run
+(** Converse of {!apply}. *)
+
+(** {5 Unsafe primitives} *)
+
+module Unsafe :
+sig
+ val le : ('a, 'b) le
+ val of_evar_map : Evd.evar_map -> 'r t
+ val of_evar : Evd.evar -> 'r evar
+ val of_ref : Evd.evar_map ref -> evdref
+ val of_pair : ('a * Evd.evar_map) -> ('a, 'r) sigma
+end
+
+(** {5 Notations} *)
+
+module Notations :
+sig
+ type ('a, 'r) sigma_ = ('a, 'r) sigma =
+ Sigma : 'a * 's t * ('r, 's) le -> ('a, 'r) sigma_
+
+ type 'a run_ = 'a run = { run : 'r. 'r t -> ('a, 'r) sigma }
+
+ val (+>) : ('a, 'b) le -> ('b, 'c) le -> ('a, 'c) le
+ (** Alias for {!cons} *)
+end
diff --git a/engine/termops.ml b/engine/termops.ml
new file mode 100644
index 000000000..5a55d47fd
--- /dev/null
+++ b/engine/termops.ml
@@ -0,0 +1,1026 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Pp
+open Errors
+open Util
+open Names
+open Nameops
+open Term
+open Vars
+open Context
+open Environ
+
+(* Sorts and sort family *)
+
+let print_sort = function
+ | Prop Pos -> (str "Set")
+ | Prop Null -> (str "Prop")
+ | Type u -> (str "Type(" ++ Univ.Universe.pr u ++ str ")")
+
+let pr_sort_family = function
+ | InSet -> (str "Set")
+ | InProp -> (str "Prop")
+ | InType -> (str "Type")
+
+let pr_name = function
+ | Name id -> pr_id id
+ | Anonymous -> str "_"
+
+let pr_con sp = str(string_of_con sp)
+
+let pr_fix pr_constr ((t,i),(lna,tl,bl)) =
+ let fixl = Array.mapi (fun i na -> (na,t.(i),tl.(i),bl.(i))) lna in
+ hov 1
+ (str"fix " ++ int i ++ spc() ++ str"{" ++
+ v 0 (prlist_with_sep spc (fun (na,i,ty,bd) ->
+ pr_name na ++ str"/" ++ int i ++ str":" ++ pr_constr ty ++
+ cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++
+ str"}")
+
+let pr_puniverses p u =
+ if Univ.Instance.is_empty u then p
+ else p ++ str"(*" ++ Univ.Instance.pr Universes.pr_with_global_universes u ++ str"*)"
+
+let rec pr_constr c = match kind_of_term c with
+ | Rel n -> str "#"++int n
+ | Meta n -> str "Meta(" ++ int n ++ str ")"
+ | Var id -> pr_id id
+ | Sort s -> print_sort s
+ | Cast (c,_, t) -> hov 1
+ (str"(" ++ pr_constr c ++ cut() ++
+ str":" ++ pr_constr t ++ str")")
+ | Prod (Name(id),t,c) -> hov 1
+ (str"forall " ++ pr_id id ++ str":" ++ pr_constr t ++ str"," ++
+ spc() ++ pr_constr c)
+ | Prod (Anonymous,t,c) -> hov 0
+ (str"(" ++ pr_constr t ++ str " ->" ++ spc() ++
+ pr_constr c ++ str")")
+ | Lambda (na,t,c) -> hov 1
+ (str"fun " ++ pr_name na ++ str":" ++
+ pr_constr t ++ str" =>" ++ spc() ++ pr_constr c)
+ | LetIn (na,b,t,c) -> hov 0
+ (str"let " ++ pr_name na ++ str":=" ++ pr_constr b ++
+ str":" ++ brk(1,2) ++ pr_constr t ++ cut() ++
+ pr_constr c)
+ | App (c,l) -> hov 1
+ (str"(" ++ pr_constr c ++ spc() ++
+ prlist_with_sep spc pr_constr (Array.to_list l) ++ str")")
+ | Evar (e,l) -> hov 1
+ (str"Evar#" ++ int (Evar.repr e) ++ str"{" ++
+ prlist_with_sep spc pr_constr (Array.to_list l) ++str"}")
+ | Const (c,u) -> str"Cst(" ++ pr_puniverses (pr_con c) u ++ str")"
+ | Ind ((sp,i),u) -> str"Ind(" ++ pr_puniverses (pr_mind sp ++ str"," ++ int i) u ++ str")"
+ | Construct (((sp,i),j),u) ->
+ str"Constr(" ++ pr_puniverses (pr_mind sp ++ str"," ++ int i ++ str"," ++ int j) u ++ str")"
+ | Proj (p,c) -> str"Proj(" ++ pr_con (Projection.constant p) ++ str"," ++ bool (Projection.unfolded p) ++ pr_constr c ++ str")"
+ | Case (ci,p,c,bl) -> v 0
+ (hv 0 (str"<"++pr_constr p++str">"++ cut() ++ str"Case " ++
+ pr_constr c ++ str"of") ++ cut() ++
+ prlist_with_sep (fun _ -> brk(1,2)) pr_constr (Array.to_list bl) ++
+ cut() ++ str"end")
+ | Fix f -> pr_fix pr_constr f
+ | CoFix(i,(lna,tl,bl)) ->
+ let fixl = Array.mapi (fun i na -> (na,tl.(i),bl.(i))) lna in
+ hov 1
+ (str"cofix " ++ int i ++ spc() ++ str"{" ++
+ v 0 (prlist_with_sep spc (fun (na,ty,bd) ->
+ pr_name na ++ str":" ++ pr_constr ty ++
+ cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++
+ str"}")
+
+let term_printer = ref (fun _ -> pr_constr)
+let print_constr_env t = !term_printer t
+let print_constr t = !term_printer (Global.env()) t
+let set_print_constr f = term_printer := f
+
+let pr_var_decl env (id,c,typ) =
+ let pbody = match c with
+ | None -> (mt ())
+ | Some c ->
+ (* Force evaluation *)
+ let pb = print_constr_env env c in
+ (str" := " ++ pb ++ cut () ) in
+ let pt = print_constr_env env typ in
+ let ptyp = (str" : " ++ pt) in
+ (pr_id id ++ hov 0 (pbody ++ ptyp))
+
+let pr_rel_decl env (na,c,typ) =
+ let pbody = match c with
+ | None -> mt ()
+ | Some c ->
+ (* Force evaluation *)
+ let pb = print_constr_env env c in
+ (str":=" ++ spc () ++ pb ++ spc ()) in
+ let ptyp = print_constr_env env typ in
+ match na with
+ | Anonymous -> hov 0 (str"<>" ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
+ | Name id -> hov 0 (pr_id id ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
+
+let print_named_context env =
+ hv 0 (fold_named_context
+ (fun env d pps ->
+ pps ++ ws 2 ++ pr_var_decl env d)
+ env ~init:(mt ()))
+
+let print_rel_context env =
+ hv 0 (fold_rel_context
+ (fun env d pps -> pps ++ ws 2 ++ pr_rel_decl env d)
+ env ~init:(mt ()))
+
+let print_env env =
+ let sign_env =
+ fold_named_context
+ (fun env d pps ->
+ let pidt = pr_var_decl env d in
+ (pps ++ fnl () ++ pidt))
+ env ~init:(mt ())
+ in
+ let db_env =
+ fold_rel_context
+ (fun env d pps ->
+ let pnat = pr_rel_decl env d in (pps ++ fnl () ++ pnat))
+ env ~init:(mt ())
+ in
+ (sign_env ++ db_env)
+
+(* [Rel (n+m);...;Rel(n+1)] *)
+let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i))
+
+let rel_list n m =
+ let rec reln l p =
+ if p>m then l else reln (mkRel(n+p)::l) (p+1)
+ in
+ reln [] 1
+
+(* Same as [rel_list] but takes a context as argument and skips let-ins *)
+let extended_rel_list n hyps =
+ let rec reln l p = function
+ | (_,None,_) :: hyps -> reln (mkRel (n+p) :: l) (p+1) hyps
+ | (_,Some _,_) :: hyps -> reln l (p+1) hyps
+ | [] -> l
+ in
+ reln [] 1 hyps
+
+let extended_rel_vect n hyps = Array.of_list (extended_rel_list n hyps)
+
+
+
+let push_rel_assum (x,t) env = push_rel (x,None,t) env
+
+let push_rels_assum assums =
+ push_rel_context (List.map (fun (x,t) -> (x,None,t)) assums)
+
+let push_named_rec_types (lna,typarray,_) env =
+ let ctxt =
+ Array.map2_i
+ (fun i na t ->
+ match na with
+ | Name id -> (id, None, lift i t)
+ | Anonymous -> anomaly (Pp.str "Fix declarations must be named"))
+ lna typarray in
+ Array.fold_left
+ (fun e assum -> push_named assum e) env ctxt
+
+let lookup_rel_id id sign =
+ let rec lookrec n = function
+ | [] -> raise Not_found
+ | (Anonymous, _, _) :: l -> lookrec (n + 1) l
+ | (Name id', b, t) :: l ->
+ if Names.Id.equal id' id then (n, b, t) else lookrec (n + 1) l
+ in
+ lookrec 1 sign
+
+(* Constructs either [forall x:t, c] or [let x:=b:t in c] *)
+let mkProd_or_LetIn (na,body,t) c =
+ match body with
+ | None -> mkProd (na, t, c)
+ | Some b -> mkLetIn (na, b, t, c)
+
+(* Constructs either [forall x:t, c] or [c] in which [x] is replaced by [b] *)
+let mkProd_wo_LetIn (na,body,t) c =
+ match body with
+ | None -> mkProd (na, t, c)
+ | Some b -> subst1 b c
+
+let it_mkProd init = List.fold_left (fun c (n,t) -> mkProd (n, t, c)) init
+let it_mkLambda init = List.fold_left (fun c (n,t) -> mkLambda (n, t, c)) init
+
+let it_named_context_quantifier f ~init =
+ List.fold_left (fun c d -> f d c) init
+
+let it_mkProd_or_LetIn init = it_named_context_quantifier mkProd_or_LetIn ~init
+let it_mkProd_wo_LetIn init = it_named_context_quantifier mkProd_wo_LetIn ~init
+let it_mkLambda_or_LetIn init = it_named_context_quantifier mkLambda_or_LetIn ~init
+let it_mkNamedProd_or_LetIn init = it_named_context_quantifier mkNamedProd_or_LetIn ~init
+let it_mkNamedProd_wo_LetIn init = it_named_context_quantifier mkNamedProd_wo_LetIn ~init
+let it_mkNamedLambda_or_LetIn init = it_named_context_quantifier mkNamedLambda_or_LetIn ~init
+
+let it_mkLambda_or_LetIn_from_no_LetIn c decls =
+ let rec aux k decls c = match decls with
+ | [] -> c
+ | (na,Some b,t)::decls -> mkLetIn (na,b,t,aux (k-1) decls (liftn 1 k c))
+ | (na,None,t)::decls -> mkLambda (na,t,aux (k-1) decls c)
+ in aux (List.length decls) (List.rev decls) c
+
+(* *)
+
+(* strips head casts and flattens head applications *)
+let rec strip_head_cast c = match kind_of_term c with
+ | App (f,cl) ->
+ let rec collapse_rec f cl2 = match kind_of_term f with
+ | App (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
+ | Cast (c,_,_) -> collapse_rec c cl2
+ | _ -> if Int.equal (Array.length cl2) 0 then f else mkApp (f,cl2)
+ in
+ collapse_rec f cl
+ | Cast (c,_,_) -> strip_head_cast c
+ | _ -> c
+
+let rec drop_extra_implicit_args c = match kind_of_term c with
+ (* Removed trailing extra implicit arguments, what improves compatibility
+ for constants with recently added maximal implicit arguments *)
+ | App (f,args) when isEvar (Array.last args) ->
+ drop_extra_implicit_args
+ (mkApp (f,fst (Array.chop (Array.length args - 1) args)))
+ | _ -> c
+
+(* Get the last arg of an application *)
+let last_arg c = match kind_of_term c with
+ | App (f,cl) -> Array.last cl
+ | _ -> anomaly (Pp.str "last_arg")
+
+(* Get the last arg of an application *)
+let decompose_app_vect c =
+ match kind_of_term c with
+ | App (f,cl) -> (f, cl)
+ | _ -> (c,[||])
+
+let adjust_app_list_size f1 l1 f2 l2 =
+ let len1 = List.length l1 and len2 = List.length l2 in
+ if Int.equal len1 len2 then (f1,l1,f2,l2)
+ else if len1 < len2 then
+ let extras,restl2 = List.chop (len2-len1) l2 in
+ (f1, l1, applist (f2,extras), restl2)
+ else
+ let extras,restl1 = List.chop (len1-len2) l1 in
+ (applist (f1,extras), restl1, f2, l2)
+
+let adjust_app_array_size f1 l1 f2 l2 =
+ let len1 = Array.length l1 and len2 = Array.length l2 in
+ if Int.equal len1 len2 then (f1,l1,f2,l2)
+ else if len1 < len2 then
+ let extras,restl2 = Array.chop (len2-len1) l2 in
+ (f1, l1, appvect (f2,extras), restl2)
+ else
+ let extras,restl1 = Array.chop (len1-len2) l1 in
+ (appvect (f1,extras), restl1, f2, l2)
+
+(* [map_constr_with_named_binders g f l c] maps [f l] on the immediate
+ subterms of [c]; it carries an extra data [l] (typically a name
+ list) which is processed by [g na] (which typically cons [na] to
+ [l]) at each binder traversal (with name [na]); it is not recursive
+ and the order with which subterms are processed is not specified *)
+
+let map_constr_with_named_binders g f l c = match kind_of_term c with
+ | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
+ | Construct _) -> c
+ | Cast (c,k,t) -> mkCast (f l c, k, f l t)
+ | Prod (na,t,c) -> mkProd (na, f l t, f (g na l) c)
+ | Lambda (na,t,c) -> mkLambda (na, f l t, f (g na l) c)
+ | LetIn (na,b,t,c) -> mkLetIn (na, f l b, f l t, f (g na l) c)
+ | App (c,al) -> mkApp (f l c, Array.map (f l) al)
+ | Proj (p,c) -> mkProj (p, f l c)
+ | Evar (e,al) -> mkEvar (e, Array.map (f l) al)
+ | Case (ci,p,c,bl) -> mkCase (ci, f l p, f l c, Array.map (f l) bl)
+ | Fix (ln,(lna,tl,bl)) ->
+ let l' = Array.fold_left (fun l na -> g na l) l lna in
+ mkFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl))
+ | CoFix(ln,(lna,tl,bl)) ->
+ let l' = Array.fold_left (fun l na -> g na l) l lna in
+ mkCoFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl))
+
+(* [map_constr_with_binders_left_to_right g f n c] maps [f n] on the
+ immediate subterms of [c]; it carries an extra data [n] (typically
+ a lift index) which is processed by [g] (which typically add 1 to
+ [n]) at each binder traversal; the subterms are processed from left
+ to right according to the usual representation of the constructions
+ (this may matter if [f] does a side-effect); it is not recursive;
+ in fact, the usual representation of the constructions is at the
+ time being almost those of the ML representation (except for
+ (co-)fixpoint) *)
+
+let fold_rec_types g (lna,typarray,_) e =
+ let ctxt = Array.map2_i (fun i na t -> (na, None, lift i t)) lna typarray in
+ Array.fold_left (fun e assum -> g assum e) e ctxt
+
+let map_left2 f a g b =
+ let l = Array.length a in
+ if Int.equal l 0 then [||], [||] else begin
+ let r = Array.make l (f a.(0)) in
+ let s = Array.make l (g b.(0)) in
+ for i = 1 to l - 1 do
+ r.(i) <- f a.(i);
+ s.(i) <- g b.(i)
+ done;
+ r, s
+ end
+
+let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with
+ | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
+ | Construct _) -> c
+ | Cast (b,k,t) ->
+ let b' = f l b in
+ let t' = f l t in
+ if b' == b && t' == t then c
+ else mkCast (b',k,t')
+ | Prod (na,t,b) ->
+ let t' = f l t in
+ let b' = f (g (na,None,t) l) b in
+ if t' == t && b' == b then c
+ else mkProd (na, t', b')
+ | Lambda (na,t,b) ->
+ let t' = f l t in
+ let b' = f (g (na,None,t) l) b in
+ if t' == t && b' == b then c
+ else mkLambda (na, t', b')
+ | LetIn (na,bo,t,b) ->
+ let bo' = f l bo in
+ let t' = f l t in
+ let b' = f (g (na,Some bo,t) l) b in
+ if bo' == bo && t' == t && b' == b then c
+ else mkLetIn (na, bo', t', b')
+ | App (c,[||]) -> assert false
+ | App (t,al) ->
+ (*Special treatment to be able to recognize partially applied subterms*)
+ let a = al.(Array.length al - 1) in
+ let app = (mkApp (t, Array.sub al 0 (Array.length al - 1))) in
+ let app' = f l app in
+ let a' = f l a in
+ if app' == app && a' == a then c
+ else mkApp (app', [| a' |])
+ | Proj (p,b) ->
+ let b' = f l b in
+ if b' == b then c
+ else mkProj (p, b')
+ | Evar (e,al) ->
+ let al' = Array.map_left (f l) al in
+ if Array.for_all2 (==) al' al then c
+ else mkEvar (e, al')
+ | Case (ci,p,b,bl) ->
+ (* In v8 concrete syntax, predicate is after the term to match! *)
+ let b' = f l b in
+ let p' = f l p in
+ let bl' = Array.map_left (f l) bl in
+ if b' == b && p' == p && bl' == bl then c
+ else mkCase (ci, p', b', bl')
+ | Fix (ln,(lna,tl,bl as fx)) ->
+ let l' = fold_rec_types g fx l in
+ let (tl', bl') = map_left2 (f l) tl (f l') bl in
+ if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl'
+ then c
+ else mkFix (ln,(lna,tl',bl'))
+ | CoFix(ln,(lna,tl,bl as fx)) ->
+ let l' = fold_rec_types g fx l in
+ let (tl', bl') = map_left2 (f l) tl (f l') bl in
+ if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl'
+ then c
+ else mkCoFix (ln,(lna,tl',bl'))
+
+(* strong *)
+let map_constr_with_full_binders g f l cstr = match kind_of_term cstr with
+ | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
+ | Construct _) -> cstr
+ | Cast (c,k, t) ->
+ let c' = f l c in
+ let t' = f l t in
+ if c==c' && t==t' then cstr else mkCast (c', k, t')
+ | Prod (na,t,c) ->
+ let t' = f l t in
+ let c' = f (g (na,None,t) l) c in
+ if t==t' && c==c' then cstr else mkProd (na, t', c')
+ | Lambda (na,t,c) ->
+ let t' = f l t in
+ let c' = f (g (na,None,t) l) c in
+ if t==t' && c==c' then cstr else mkLambda (na, t', c')
+ | LetIn (na,b,t,c) ->
+ let b' = f l b in
+ let t' = f l t in
+ let c' = f (g (na,Some b,t) l) c in
+ if b==b' && t==t' && c==c' then cstr else mkLetIn (na, b', t', c')
+ | App (c,al) ->
+ let c' = f l c in
+ let al' = Array.map (f l) al in
+ if c==c' && Array.for_all2 (==) al al' then cstr else mkApp (c', al')
+ | Proj (p,c) ->
+ let c' = f l c in
+ if c' == c then cstr else mkProj (p, c')
+ | Evar (e,al) ->
+ let al' = Array.map (f l) al in
+ if Array.for_all2 (==) al al' then cstr else mkEvar (e, al')
+ | Case (ci,p,c,bl) ->
+ let p' = f l p in
+ let c' = f l c in
+ let bl' = Array.map (f l) bl in
+ if p==p' && c==c' && Array.for_all2 (==) bl bl' then cstr else
+ mkCase (ci, p', c', bl')
+ | Fix (ln,(lna,tl,bl)) ->
+ let tl' = Array.map (f l) tl in
+ let l' =
+ Array.fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in
+ let bl' = Array.map (f l') bl in
+ if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl'
+ then cstr
+ else mkFix (ln,(lna,tl',bl'))
+ | CoFix(ln,(lna,tl,bl)) ->
+ let tl' = Array.map (f l) tl in
+ let l' =
+ Array.fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in
+ let bl' = Array.map (f l') bl in
+ if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl'
+ then cstr
+ else mkCoFix (ln,(lna,tl',bl'))
+
+(* [fold_constr_with_binders g f n acc c] folds [f n] on the immediate
+ subterms of [c] starting from [acc] and proceeding from left to
+ right according to the usual representation of the constructions as
+ [fold_constr] but it carries an extra data [n] (typically a lift
+ index) which is processed by [g] (which typically add 1 to [n]) at
+ each binder traversal; it is not recursive *)
+
+let fold_constr_with_full_binders g f n acc c = match kind_of_term c with
+ | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
+ | Construct _) -> acc
+ | Cast (c,_, t) -> f n (f n acc c) t
+ | Prod (na,t,c) -> f (g (na,None,t) n) (f n acc t) c
+ | Lambda (na,t,c) -> f (g (na,None,t) n) (f n acc t) c
+ | LetIn (na,b,t,c) -> f (g (na,Some b,t) n) (f n (f n acc b) t) c
+ | App (c,l) -> Array.fold_left (f n) (f n acc c) l
+ | Proj (p,c) -> f n acc c
+ | Evar (_,l) -> Array.fold_left (f n) acc l
+ | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
+ | Fix (_,(lna,tl,bl)) ->
+ let n' = CArray.fold_left2 (fun c n t -> g (n,None,t) c) n lna tl in
+ let fd = Array.map2 (fun t b -> (t,b)) tl bl in
+ Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
+ | CoFix (_,(lna,tl,bl)) ->
+ let n' = CArray.fold_left2 (fun c n t -> g (n,None,t) c) n lna tl in
+ let fd = Array.map2 (fun t b -> (t,b)) tl bl in
+ Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
+
+let fold_constr_with_binders g f n acc c =
+ fold_constr_with_full_binders (fun _ x -> g x) f n acc c
+
+(* [iter_constr_with_full_binders g f acc c] iters [f acc] on the immediate
+ subterms of [c]; it carries an extra data [acc] which is processed by [g] at
+ each binder traversal; it is not recursive and the order with which
+ subterms are processed is not specified *)
+
+let iter_constr_with_full_binders g f l c = match kind_of_term c with
+ | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
+ | Construct _) -> ()
+ | Cast (c,_, t) -> f l c; f l t
+ | Prod (na,t,c) -> f l t; f (g (na,None,t) l) c
+ | Lambda (na,t,c) -> f l t; f (g (na,None,t) l) c
+ | LetIn (na,b,t,c) -> f l b; f l t; f (g (na,Some b,t) l) c
+ | App (c,args) -> f l c; Array.iter (f l) args
+ | Proj (p,c) -> f l c
+ | Evar (_,args) -> Array.iter (f l) args
+ | Case (_,p,c,bl) -> f l p; f l c; Array.iter (f l) bl
+ | Fix (_,(lna,tl,bl)) ->
+ let l' = Array.fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in
+ Array.iter (f l) tl;
+ Array.iter (f l') bl
+ | CoFix (_,(lna,tl,bl)) ->
+ let l' = Array.fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in
+ Array.iter (f l) tl;
+ Array.iter (f l') bl
+
+(***************************)
+(* occurs check functions *)
+(***************************)
+
+exception Occur
+
+let occur_meta c =
+ let rec occrec c = match kind_of_term c with
+ | Meta _ -> raise Occur
+ | _ -> iter_constr occrec c
+ in try occrec c; false with Occur -> true
+
+let occur_existential c =
+ let rec occrec c = match kind_of_term c with
+ | Evar _ -> raise Occur
+ | _ -> iter_constr occrec c
+ in try occrec c; false with Occur -> true
+
+let occur_meta_or_existential c =
+ let rec occrec c = match kind_of_term c with
+ | Evar _ -> raise Occur
+ | Meta _ -> raise Occur
+ | _ -> iter_constr occrec c
+ in try occrec c; false with Occur -> true
+
+let occur_evar n c =
+ let rec occur_rec c = match kind_of_term c with
+ | Evar (sp,_) when Evar.equal sp n -> raise Occur
+ | _ -> iter_constr occur_rec c
+ in
+ try occur_rec c; false with Occur -> true
+
+let occur_in_global env id constr =
+ let vars = vars_of_global env constr in
+ if Id.Set.mem id vars then raise Occur
+
+let occur_var env id c =
+ let rec occur_rec c =
+ match kind_of_term c with
+ | Var _ | Const _ | Ind _ | Construct _ -> occur_in_global env id c
+ | _ -> iter_constr occur_rec c
+ in
+ try occur_rec c; false with Occur -> true
+
+let occur_var_in_decl env hyp (_,c,typ) =
+ match c with
+ | None -> occur_var env hyp typ
+ | Some body ->
+ occur_var env hyp typ ||
+ occur_var env hyp body
+
+(* returns the list of free debruijn indices in a term *)
+
+let free_rels m =
+ let rec frec depth acc c = match kind_of_term c with
+ | Rel n -> if n >= depth then Int.Set.add (n-depth+1) acc else acc
+ | _ -> fold_constr_with_binders succ frec depth acc c
+ in
+ frec 1 Int.Set.empty m
+
+(* collects all metavar occurrences, in left-to-right order, preserving
+ * repetitions and all. *)
+
+let collect_metas c =
+ let rec collrec acc c =
+ match kind_of_term c with
+ | Meta mv -> List.add_set Int.equal mv acc
+ | _ -> fold_constr collrec acc c
+ in
+ List.rev (collrec [] c)
+
+(* collects all vars; warning: this is only visible vars, not dependencies in
+ all section variables; for the latter, use global_vars_set *)
+let collect_vars c =
+ let rec aux vars c = match kind_of_term c with
+ | Var id -> Id.Set.add id vars
+ | _ -> fold_constr aux vars c in
+ aux Id.Set.empty c
+
+(* Tests whether [m] is a subterm of [t]:
+ [m] is appropriately lifted through abstractions of [t] *)
+
+let dependent_main noevar univs m t =
+ let eqc x y = if univs then fst (Universes.eq_constr_universes x y) else eq_constr_nounivs x y in
+ let rec deprec m t =
+ if eqc m t then
+ raise Occur
+ else
+ match kind_of_term m, kind_of_term t with
+ | App (fm,lm), App (ft,lt) when Array.length lm < Array.length lt ->
+ deprec m (mkApp (ft,Array.sub lt 0 (Array.length lm)));
+ CArray.Fun1.iter deprec m
+ (Array.sub lt
+ (Array.length lm) ((Array.length lt) - (Array.length lm)))
+ | _, Cast (c,_,_) when noevar && isMeta c -> ()
+ | _, Evar _ when noevar -> ()
+ | _ -> iter_constr_with_binders (fun c -> lift 1 c) deprec m t
+ in
+ try deprec m t; false with Occur -> true
+
+let dependent = dependent_main false false
+let dependent_no_evar = dependent_main true false
+
+let dependent_univs = dependent_main false true
+let dependent_univs_no_evar = dependent_main true true
+
+let dependent_in_decl a (_,c,t) =
+ match c with
+ | None -> dependent a t
+ | Some body -> dependent a body || dependent a t
+
+let count_occurrences m t =
+ let n = ref 0 in
+ let rec countrec m t =
+ if eq_constr m t then
+ incr n
+ else
+ match kind_of_term m, kind_of_term t with
+ | App (fm,lm), App (ft,lt) when Array.length lm < Array.length lt ->
+ countrec m (mkApp (ft,Array.sub lt 0 (Array.length lm)));
+ Array.iter (countrec m)
+ (Array.sub lt
+ (Array.length lm) ((Array.length lt) - (Array.length lm)))
+ | _, Cast (c,_,_) when isMeta c -> ()
+ | _, Evar _ -> ()
+ | _ -> iter_constr_with_binders (lift 1) countrec m t
+ in
+ countrec m t;
+ !n
+
+(* Synonymous *)
+let occur_term = dependent
+
+let pop t = lift (-1) t
+
+(***************************)
+(* bindings functions *)
+(***************************)
+
+type meta_type_map = (metavariable * types) list
+
+type meta_value_map = (metavariable * constr) list
+
+let rec subst_meta bl c =
+ match kind_of_term c with
+ | Meta i -> (try Int.List.assoc i bl with Not_found -> c)
+ | _ -> map_constr (subst_meta bl) c
+
+(* First utilities for avoiding telescope computation for subst_term *)
+
+let prefix_application eq_fun (k,c) (t : constr) =
+ let c' = collapse_appl c and t' = collapse_appl t in
+ match kind_of_term c', kind_of_term t' with
+ | App (f1,cl1), App (f2,cl2) ->
+ let l1 = Array.length cl1
+ and l2 = Array.length cl2 in
+ if l1 <= l2
+ && eq_fun c' (mkApp (f2, Array.sub cl2 0 l1)) then
+ Some (mkApp (mkRel k, Array.sub cl2 l1 (l2 - l1)))
+ else
+ None
+ | _ -> None
+
+let my_prefix_application eq_fun (k,c) (by_c : constr) (t : constr) =
+ let c' = collapse_appl c and t' = collapse_appl t in
+ match kind_of_term c', kind_of_term t' with
+ | App (f1,cl1), App (f2,cl2) ->
+ let l1 = Array.length cl1
+ and l2 = Array.length cl2 in
+ if l1 <= l2
+ && eq_fun c' (mkApp (f2, Array.sub cl2 0 l1)) then
+ Some (mkApp ((lift k by_c), Array.sub cl2 l1 (l2 - l1)))
+ else
+ None
+ | _ -> None
+
+(* Recognizing occurrences of a given subterm in a term: [subst_term c t]
+ substitutes [(Rel 1)] for all occurrences of term [c] in a term [t];
+ works if [c] has rels *)
+
+let subst_term_gen eq_fun c t =
+ let rec substrec (k,c as kc) t =
+ match prefix_application eq_fun kc t with
+ | Some x -> x
+ | None ->
+ if eq_fun c t then mkRel k
+ else
+ map_constr_with_binders (fun (k,c) -> (k+1,lift 1 c)) substrec kc t
+ in
+ substrec (1,c) t
+
+let subst_term = subst_term_gen eq_constr
+
+(* Recognizing occurrences of a given subterm in a term :
+ [replace_term c1 c2 t] substitutes [c2] for all occurrences of
+ term [c1] in a term [t]; works if [c1] and [c2] have rels *)
+
+let replace_term_gen eq_fun c by_c in_t =
+ let rec substrec (k,c as kc) t =
+ match my_prefix_application eq_fun kc by_c t with
+ | Some x -> x
+ | None ->
+ (if eq_fun c t then (lift k by_c) else
+ map_constr_with_binders (fun (k,c) -> (k+1,lift 1 c))
+ substrec kc t)
+ in
+ substrec (0,c) in_t
+
+let replace_term = replace_term_gen eq_constr
+
+let vars_of_env env =
+ let s =
+ Context.fold_named_context (fun (id,_,_) s -> Id.Set.add id s)
+ (named_context env) ~init:Id.Set.empty in
+ Context.fold_rel_context
+ (fun (na,_,_) s -> match na with Name id -> Id.Set.add id s | _ -> s)
+ (rel_context env) ~init:s
+
+let add_vname vars = function
+ Name id -> Id.Set.add id vars
+ | _ -> vars
+
+(*************************)
+(* Names environments *)
+(*************************)
+type names_context = Name.t list
+let add_name n nl = n::nl
+let lookup_name_of_rel p names =
+ try List.nth names (p-1)
+ with Invalid_argument _ | Failure _ -> raise Not_found
+let lookup_rel_of_name id names =
+ let rec lookrec n = function
+ | Anonymous :: l -> lookrec (n+1) l
+ | (Name id') :: l -> if Id.equal id' id then n else lookrec (n+1) l
+ | [] -> raise Not_found
+ in
+ lookrec 1 names
+let empty_names_context = []
+
+let ids_of_rel_context sign =
+ Context.fold_rel_context
+ (fun (na,_,_) l -> match na with Name id -> id::l | Anonymous -> l)
+ sign ~init:[]
+
+let ids_of_named_context sign =
+ Context.fold_named_context (fun (id,_,_) idl -> id::idl) sign ~init:[]
+
+let ids_of_context env =
+ (ids_of_rel_context (rel_context env))
+ @ (ids_of_named_context (named_context env))
+
+
+let names_of_rel_context env =
+ List.map (fun (na,_,_) -> na) (rel_context env)
+
+let is_section_variable id =
+ try let _ = Global.lookup_named id in true
+ with Not_found -> false
+
+let isGlobalRef c =
+ match kind_of_term c with
+ | Const _ | Ind _ | Construct _ | Var _ -> true
+ | _ -> false
+
+let is_template_polymorphic env f =
+ match kind_of_term f with
+ | Ind ind -> Environ.template_polymorphic_pind ind env
+ | Const c -> Environ.template_polymorphic_pconstant c env
+ | _ -> false
+
+let base_sort_cmp pb s0 s1 =
+ match (s0,s1) with
+ | (Prop c1, Prop c2) -> c1 == Null || c2 == Pos (* Prop <= Set *)
+ | (Prop c1, Type u) -> pb == Reduction.CUMUL
+ | (Type u1, Type u2) -> true
+ | _ -> false
+
+(* eq_constr extended with universe erasure *)
+let compare_constr_univ f cv_pb t1 t2 =
+ match kind_of_term t1, kind_of_term t2 with
+ Sort s1, Sort s2 -> base_sort_cmp cv_pb s1 s2
+ | Prod (_,t1,c1), Prod (_,t2,c2) ->
+ f Reduction.CONV t1 t2 && f cv_pb c1 c2
+ | _ -> compare_constr (fun t1 t2 -> f Reduction.CONV t1 t2) t1 t2
+
+let rec constr_cmp cv_pb t1 t2 = compare_constr_univ constr_cmp cv_pb t1 t2
+
+let eq_constr t1 t2 = constr_cmp Reduction.CONV t1 t2
+
+(* App(c,[t1,...tn]) -> ([c,t1,...,tn-1],tn)
+ App(c,[||]) -> ([],c) *)
+let split_app c = match kind_of_term c with
+ App(c,l) ->
+ let len = Array.length l in
+ if Int.equal len 0 then ([],c) else
+ let last = Array.get l (len-1) in
+ let prev = Array.sub l 0 (len-1) in
+ c::(Array.to_list prev), last
+ | _ -> assert false
+
+type subst = (rel_context*constr) Evar.Map.t
+
+exception CannotFilter
+
+let filtering env cv_pb c1 c2 =
+ let evm = ref Evar.Map.empty in
+ let define cv_pb e1 ev c1 =
+ try let (e2,c2) = Evar.Map.find ev !evm in
+ let shift = List.length e1 - List.length e2 in
+ if constr_cmp cv_pb c1 (lift shift c2) then () else raise CannotFilter
+ with Not_found ->
+ evm := Evar.Map.add ev (e1,c1) !evm
+ in
+ let rec aux env cv_pb c1 c2 =
+ match kind_of_term c1, kind_of_term c2 with
+ | App _, App _ ->
+ let ((p1,l1),(p2,l2)) = (split_app c1),(split_app c2) in
+ let () = aux env cv_pb l1 l2 in
+ begin match p1, p2 with
+ | [], [] -> ()
+ | (h1 :: p1), (h2 :: p2) ->
+ aux env cv_pb (applistc h1 p1) (applistc h2 p2)
+ | _ -> assert false
+ end
+ | Prod (n,t1,c1), Prod (_,t2,c2) ->
+ aux env cv_pb t1 t2;
+ aux ((n,None,t1)::env) cv_pb c1 c2
+ | _, Evar (ev,_) -> define cv_pb env ev c1
+ | Evar (ev,_), _ -> define cv_pb env ev c2
+ | _ ->
+ if compare_constr_univ
+ (fun pb c1 c2 -> aux env pb c1 c2; true) cv_pb c1 c2 then ()
+ else raise CannotFilter
+ (* TODO: le reste des binders *)
+ in
+ aux env cv_pb c1 c2; !evm
+
+let decompose_prod_letin : constr -> int * rel_context * constr =
+ let rec prodec_rec i l c = match kind_of_term c with
+ | Prod (n,t,c) -> prodec_rec (succ i) ((n,None,t)::l) c
+ | LetIn (n,d,t,c) -> prodec_rec (succ i) ((n,Some d,t)::l) c
+ | Cast (c,_,_) -> prodec_rec i l c
+ | _ -> i,l,c in
+ prodec_rec 0 []
+
+let align_prod_letin c a : rel_context * constr =
+ let (lc,_,_) = decompose_prod_letin c in
+ let (la,l,a) = decompose_prod_letin a in
+ if not (la >= lc) then invalid_arg "align_prod_letin";
+ let (l1,l2) = Util.List.chop lc l in
+ l2,it_mkProd_or_LetIn a l1
+
+(* We reduce a series of head eta-redex or nothing at all *)
+(* [x1:c1;...;xn:cn]@(f;a1...an;x1;...;xn) --> @(f;a1...an) *)
+(* Remplace 2 earlier buggish versions *)
+
+let rec eta_reduce_head c =
+ match kind_of_term c with
+ | Lambda (_,c1,c') ->
+ (match kind_of_term (eta_reduce_head c') with
+ | App (f,cl) ->
+ let lastn = (Array.length cl) - 1 in
+ if lastn < 0 then anomaly (Pp.str "application without arguments")
+ else
+ (match kind_of_term cl.(lastn) with
+ | Rel 1 ->
+ let c' =
+ if Int.equal lastn 0 then f
+ else mkApp (f, Array.sub cl 0 lastn)
+ in
+ if noccurn 1 c'
+ then lift (-1) c'
+ else c
+ | _ -> c)
+ | _ -> c)
+ | _ -> c
+
+
+(* iterator on rel context *)
+let process_rel_context f env =
+ let sign = named_context_val env in
+ let rels = rel_context env in
+ let env0 = reset_with_named_context sign env in
+ Context.fold_rel_context f rels ~init:env0
+
+let assums_of_rel_context sign =
+ Context.fold_rel_context
+ (fun (na,c,t) l ->
+ match c with
+ Some _ -> l
+ | None -> (na, t)::l)
+ sign ~init:[]
+
+let map_rel_context_in_env f env sign =
+ let rec aux env acc = function
+ | d::sign ->
+ aux (push_rel d env) (map_rel_declaration (f env) d :: acc) sign
+ | [] ->
+ acc
+ in
+ aux env [] (List.rev sign)
+
+let map_rel_context_with_binders f sign =
+ let rec aux k = function
+ | d::sign -> map_rel_declaration (f k) d :: aux (k-1) sign
+ | [] -> []
+ in
+ aux (rel_context_length sign) sign
+
+let substl_rel_context l =
+ map_rel_context_with_binders (fun k -> substnl l (k-1))
+
+let lift_rel_context n =
+ map_rel_context_with_binders (liftn n)
+
+let smash_rel_context sign =
+ let rec aux acc = function
+ | [] -> acc
+ | (_,None,_ as d) :: l -> aux (d::acc) l
+ | (_,Some b,_) :: l ->
+ (* Quadratic in the number of let but there are probably a few of them *)
+ aux (List.rev (substl_rel_context [b] (List.rev acc))) l
+ in List.rev (aux [] sign)
+
+let adjust_subst_to_rel_context sign l =
+ let rec aux subst sign l =
+ match sign, l with
+ | (_,None,_)::sign', a::args' -> aux (a::subst) sign' args'
+ | (_,Some c,_)::sign', args' ->
+ aux (substl (List.rev subst) c :: subst) sign' args'
+ | [], [] -> List.rev subst
+ | _ -> anomaly (Pp.str "Instance and signature do not match")
+ in aux [] (List.rev sign) l
+
+let fold_named_context_both_sides f l ~init = List.fold_right_and_left f l init
+
+let rec mem_named_context id = function
+ | (id',_,_) :: _ when Id.equal id id' -> true
+ | _ :: sign -> mem_named_context id sign
+ | [] -> false
+
+let compact_named_context_reverse sign =
+ let compact l (i1,c1,t1) =
+ match l with
+ | [] -> [[i1],c1,t1]
+ | (l2,c2,t2)::q ->
+ if Option.equal Constr.equal c1 c2 && Constr.equal t1 t2
+ then (i1::l2,c2,t2)::q
+ else ([i1],c1,t1)::l
+ in Context.fold_named_context_reverse compact ~init:[] sign
+
+let compact_named_context sign = List.rev (compact_named_context_reverse sign)
+
+let clear_named_body id env =
+ let aux _ = function
+ | (id',Some c,t) when Id.equal id id' -> push_named (id,None,t)
+ | d -> push_named d in
+ fold_named_context aux env ~init:(reset_context env)
+
+let global_vars env ids = Id.Set.elements (global_vars_set env ids)
+
+let global_vars_set_of_decl env = function
+ | (_,None,t) -> global_vars_set env t
+ | (_,Some c,t) ->
+ Id.Set.union (global_vars_set env t)
+ (global_vars_set env c)
+
+let dependency_closure env sign hyps =
+ if Id.Set.is_empty hyps then [] else
+ let (_,lh) =
+ Context.fold_named_context_reverse
+ (fun (hs,hl) (x,_,_ as d) ->
+ if Id.Set.mem x hs then
+ (Id.Set.union (global_vars_set_of_decl env d) (Id.Set.remove x hs),
+ x::hl)
+ else (hs,hl))
+ ~init:(hyps,[])
+ sign in
+ List.rev lh
+
+(* Combinators on judgments *)
+
+let on_judgment f j = { uj_val = f j.uj_val; uj_type = f j.uj_type }
+let on_judgment_value f j = { j with uj_val = f j.uj_val }
+let on_judgment_type f j = { j with uj_type = f j.uj_type }
+
+(* Cut a context ctx in 2 parts (ctx1,ctx2) with ctx1 containing k
+ variables; skips let-in's *)
+let context_chop k ctx =
+ let rec chop_aux acc = function
+ | (0, l2) -> (List.rev acc, l2)
+ | (n, ((_,Some _,_ as h)::t)) -> chop_aux (h::acc) (n, t)
+ | (n, (h::t)) -> chop_aux (h::acc) (pred n, t)
+ | (_, []) -> anomaly (Pp.str "context_chop")
+ in chop_aux [] (k,ctx)
+
+(* Do not skip let-in's *)
+let env_rel_context_chop k env =
+ let rels = rel_context env in
+ let ctx1,ctx2 = List.chop k rels in
+ push_rel_context ctx2 (reset_with_named_context (named_context_val env) env),
+ ctx1
+
+(*******************************************)
+(* Functions to deal with impossible cases *)
+(*******************************************)
+let impossible_default_case = ref None
+
+let set_impossible_default_clause c = impossible_default_case := Some c
+
+let coq_unit_judge =
+ let na1 = Name (Id.of_string "A") in
+ let na2 = Name (Id.of_string "H") in
+ fun () ->
+ match !impossible_default_case with
+ | Some fn ->
+ let (id,type_of_id), ctx = fn () in
+ make_judge id type_of_id, ctx
+ | None ->
+ (* In case the constants id/ID are not defined *)
+ make_judge (mkLambda (na1,mkProp,mkLambda(na2,mkRel 1,mkRel 1)))
+ (mkProd (na1,mkProp,mkArrow (mkRel 1) (mkRel 2))),
+ Univ.ContextSet.empty
diff --git a/engine/termops.mli b/engine/termops.mli
new file mode 100644
index 000000000..6c680005d
--- /dev/null
+++ b/engine/termops.mli
@@ -0,0 +1,248 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Pp
+open Names
+open Term
+open Context
+open Environ
+
+(** printers *)
+val print_sort : sorts -> std_ppcmds
+val pr_sort_family : sorts_family -> std_ppcmds
+val pr_fix : (constr -> std_ppcmds) -> fixpoint -> std_ppcmds
+
+(** debug printer: do not use to display terms to the casual user... *)
+val set_print_constr : (env -> constr -> std_ppcmds) -> unit
+val print_constr : constr -> std_ppcmds
+val print_constr_env : env -> constr -> std_ppcmds
+val print_named_context : env -> std_ppcmds
+val pr_rel_decl : env -> rel_declaration -> std_ppcmds
+val print_rel_context : env -> std_ppcmds
+val print_env : env -> std_ppcmds
+
+(** about contexts *)
+val push_rel_assum : Name.t * types -> env -> env
+val push_rels_assum : (Name.t * types) list -> env -> env
+val push_named_rec_types : Name.t array * types array * 'a -> env -> env
+
+val lookup_rel_id : Id.t -> rel_context -> int * constr option * types
+(** Associates the contents of an identifier in a [rel_context]. Raise
+ [Not_found] if there is no such identifier. *)
+
+(** Functions that build argument lists matching a block of binders or a context.
+ [rel_vect n m] builds [|Rel (n+m);...;Rel(n+1)|]
+ [extended_rel_vect n ctx] extends the [ctx] context of length [m]
+ with [n] elements.
+*)
+val rel_vect : int -> int -> constr array
+val rel_list : int -> int -> constr list
+val extended_rel_list : int -> rel_context -> constr list
+val extended_rel_vect : int -> rel_context -> constr array
+
+(** iterators/destructors on terms *)
+val mkProd_or_LetIn : rel_declaration -> types -> types
+val mkProd_wo_LetIn : rel_declaration -> types -> types
+val it_mkProd : types -> (Name.t * types) list -> types
+val it_mkLambda : constr -> (Name.t * types) list -> constr
+val it_mkProd_or_LetIn : types -> rel_context -> types
+val it_mkProd_wo_LetIn : types -> rel_context -> types
+val it_mkLambda_or_LetIn : constr -> rel_context -> constr
+val it_mkNamedProd_or_LetIn : types -> named_context -> types
+val it_mkNamedProd_wo_LetIn : types -> named_context -> types
+val it_mkNamedLambda_or_LetIn : constr -> named_context -> constr
+
+(* Ad hoc version reinserting letin, assuming the body is defined in
+ the context where the letins are expanded *)
+val it_mkLambda_or_LetIn_from_no_LetIn : constr -> rel_context -> constr
+
+(** {6 Generic iterators on constr} *)
+
+val map_constr_with_named_binders :
+ (Name.t -> 'a -> 'a) ->
+ ('a -> constr -> constr) -> 'a -> constr -> constr
+val map_constr_with_binders_left_to_right :
+ (rel_declaration -> 'a -> 'a) ->
+ ('a -> constr -> constr) ->
+ 'a -> constr -> constr
+val map_constr_with_full_binders :
+ (rel_declaration -> 'a -> 'a) ->
+ ('a -> constr -> constr) -> 'a -> constr -> constr
+
+(** [fold_constr_with_binders g f n acc c] folds [f n] on the immediate
+ subterms of [c] starting from [acc] and proceeding from left to
+ right according to the usual representation of the constructions as
+ [fold_constr] but it carries an extra data [n] (typically a lift
+ index) which is processed by [g] (which typically add 1 to [n]) at
+ each binder traversal; it is not recursive *)
+
+val fold_constr_with_binders :
+ ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b
+
+val fold_constr_with_full_binders :
+ (rel_declaration -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) ->
+ 'a -> 'b -> constr -> 'b
+
+val iter_constr_with_full_binders :
+ (rel_declaration -> 'a -> 'a) -> ('a -> constr -> unit) -> 'a ->
+ constr -> unit
+
+(**********************************************************************)
+
+val strip_head_cast : constr -> constr
+val drop_extra_implicit_args : constr -> constr
+
+(** occur checks *)
+exception Occur
+val occur_meta : types -> bool
+val occur_existential : types -> bool
+val occur_meta_or_existential : types -> bool
+val occur_evar : existential_key -> types -> bool
+val occur_var : env -> Id.t -> types -> bool
+val occur_var_in_decl :
+ env ->
+ Id.t -> 'a * types option * types -> bool
+val free_rels : constr -> Int.Set.t
+
+(** [dependent m t] tests whether [m] is a subterm of [t] *)
+val dependent : constr -> constr -> bool
+val dependent_no_evar : constr -> constr -> bool
+val dependent_univs : constr -> constr -> bool
+val dependent_univs_no_evar : constr -> constr -> bool
+val dependent_in_decl : constr -> named_declaration -> bool
+val count_occurrences : constr -> constr -> int
+val collect_metas : constr -> int list
+val collect_vars : constr -> Id.Set.t (** for visible vars only *)
+val occur_term : constr -> constr -> bool (** Synonymous
+ of dependent
+ Substitution of metavariables *)
+type meta_value_map = (metavariable * constr) list
+val subst_meta : meta_value_map -> constr -> constr
+
+(** Type assignment for metavariables *)
+type meta_type_map = (metavariable * types) list
+
+(** [pop c] lifts by -1 the positive indexes in [c] *)
+val pop : constr -> constr
+
+(** {6 ... } *)
+(** Substitution of an arbitrary large term. Uses equality modulo
+ reduction of let *)
+
+(** [subst_term_gen eq d c] replaces [d] by [Rel 1] in [c] using [eq]
+ as equality *)
+val subst_term_gen :
+ (constr -> constr -> bool) -> constr -> constr -> constr
+
+(** [replace_term_gen eq d e c] replaces [d] by [e] in [c] using [eq]
+ as equality *)
+val replace_term_gen :
+ (constr -> constr -> bool) ->
+ constr -> constr -> constr -> constr
+
+(** [subst_term d c] replaces [d] by [Rel 1] in [c] *)
+val subst_term : constr -> constr -> constr
+
+(** [replace_term d e c] replaces [d] by [e] in [c] *)
+val replace_term : constr -> constr -> constr -> constr
+
+(** Alternative term equalities *)
+val base_sort_cmp : Reduction.conv_pb -> sorts -> sorts -> bool
+val compare_constr_univ : (Reduction.conv_pb -> constr -> constr -> bool) ->
+ Reduction.conv_pb -> constr -> constr -> bool
+val constr_cmp : Reduction.conv_pb -> constr -> constr -> bool
+val eq_constr : constr -> constr -> bool (* FIXME rename: erases universes*)
+
+val eta_reduce_head : constr -> constr
+
+exception CannotFilter
+
+(** Lightweight first-order filtering procedure. Unification
+ variables ar represented by (untyped) Evars.
+ [filtering c1 c2] returns the substitution n'th evar ->
+ (context,term), or raises [CannotFilter].
+ Warning: Outer-kernel sort subtyping are taken into account: c1 has
+ to be smaller than c2 wrt. sorts. *)
+type subst = (rel_context*constr) Evar.Map.t
+val filtering : rel_context -> Reduction.conv_pb -> constr -> constr -> subst
+
+val decompose_prod_letin : constr -> int * rel_context * constr
+val align_prod_letin : constr -> constr -> rel_context * constr
+
+(** Get the last arg of a constr intended to be an application *)
+val last_arg : constr -> constr
+
+(** Force the decomposition of a term as an applicative one *)
+val decompose_app_vect : constr -> constr * constr array
+
+val adjust_app_list_size : constr -> constr list -> constr -> constr list ->
+ (constr * constr list * constr * constr list)
+val adjust_app_array_size : constr -> constr array -> constr -> constr array ->
+ (constr * constr array * constr * constr array)
+
+(** name contexts *)
+type names_context = Name.t list
+val add_name : Name.t -> names_context -> names_context
+val lookup_name_of_rel : int -> names_context -> Name.t
+val lookup_rel_of_name : Id.t -> names_context -> int
+val empty_names_context : names_context
+val ids_of_rel_context : rel_context -> Id.t list
+val ids_of_named_context : named_context -> Id.t list
+val ids_of_context : env -> Id.t list
+val names_of_rel_context : env -> names_context
+
+val context_chop : int -> rel_context -> rel_context * rel_context
+val env_rel_context_chop : int -> env -> env * rel_context
+
+(** Set of local names *)
+val vars_of_env: env -> Id.Set.t
+val add_vname : Id.Set.t -> Name.t -> Id.Set.t
+
+(** other signature iterators *)
+val process_rel_context : (rel_declaration -> env -> env) -> env -> env
+val assums_of_rel_context : rel_context -> (Name.t * constr) list
+val lift_rel_context : int -> rel_context -> rel_context
+val substl_rel_context : constr list -> rel_context -> rel_context
+val smash_rel_context : rel_context -> rel_context (** expand lets in context *)
+val adjust_subst_to_rel_context : rel_context -> constr list -> constr list
+val map_rel_context_in_env :
+ (env -> constr -> constr) -> env -> rel_context -> rel_context
+val map_rel_context_with_binders :
+ (int -> constr -> constr) -> rel_context -> rel_context
+val fold_named_context_both_sides :
+ ('a -> named_declaration -> named_declaration list -> 'a) ->
+ named_context -> init:'a -> 'a
+val mem_named_context : Id.t -> named_context -> bool
+val compact_named_context : named_context -> named_list_context
+val compact_named_context_reverse : named_context -> named_list_context
+
+val clear_named_body : Id.t -> env -> env
+
+val global_vars : env -> constr -> Id.t list
+val global_vars_set_of_decl : env -> named_declaration -> Id.Set.t
+
+(** Gives an ordered list of hypotheses, closed by dependencies,
+ containing a given set *)
+val dependency_closure : env -> named_context -> Id.Set.t -> Id.t list
+
+(** Test if an identifier is the basename of a global reference *)
+val is_section_variable : Id.t -> bool
+
+val isGlobalRef : constr -> bool
+
+val is_template_polymorphic : env -> constr -> bool
+
+(** Combinators on judgments *)
+
+val on_judgment : (types -> types) -> unsafe_judgment -> unsafe_judgment
+val on_judgment_value : (types -> types) -> unsafe_judgment -> unsafe_judgment
+val on_judgment_type : (types -> types) -> unsafe_judgment -> unsafe_judgment
+
+(** {6 Functions to deal with impossible cases } *)
+val set_impossible_default_clause : (unit -> (constr * types) Univ.in_universe_context_set) -> unit
+val coq_unit_judge : unit -> unsafe_judgment Univ.in_universe_context_set
diff --git a/engine/uState.ml b/engine/uState.ml
new file mode 100644
index 000000000..0901d81e9
--- /dev/null
+++ b/engine/uState.ml
@@ -0,0 +1,475 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Pp
+open Errors
+open Util
+open Names
+
+module StringOrd = struct type t = string let compare = String.compare end
+module UNameMap = struct
+
+ include Map.Make(StringOrd)
+
+ let union s t =
+ if s == t then s
+ else
+ merge (fun k l r ->
+ match l, r with
+ | Some _, _ -> l
+ | _, _ -> r) s t
+end
+
+(* 2nd part used to check consistency on the fly. *)
+type t =
+ { uctx_names : Univ.Level.t UNameMap.t * string Univ.LMap.t;
+ uctx_local : Univ.universe_context_set; (** The local context of variables *)
+ uctx_univ_variables : Universes.universe_opt_subst;
+ (** The local universes that are unification variables *)
+ uctx_univ_algebraic : Univ.universe_set;
+ (** The subset of unification variables that
+ can be instantiated with algebraic universes as they appear in types
+ and universe instances only. *)
+ uctx_universes : UGraph.t; (** The current graph extended with the local constraints *)
+ uctx_initial_universes : UGraph.t; (** The graph at the creation of the evar_map *)
+ }
+
+let empty =
+ { uctx_names = UNameMap.empty, Univ.LMap.empty;
+ uctx_local = Univ.ContextSet.empty;
+ uctx_univ_variables = Univ.LMap.empty;
+ uctx_univ_algebraic = Univ.LSet.empty;
+ uctx_universes = UGraph.initial_universes;
+ uctx_initial_universes = UGraph.initial_universes }
+
+let make u =
+ { empty with
+ uctx_universes = u; uctx_initial_universes = u}
+
+let is_empty ctx =
+ Univ.ContextSet.is_empty ctx.uctx_local &&
+ Univ.LMap.is_empty ctx.uctx_univ_variables
+
+let union ctx ctx' =
+ if ctx == ctx' then ctx
+ else if is_empty ctx' then ctx
+ else
+ let local = Univ.ContextSet.union ctx.uctx_local ctx'.uctx_local in
+ let names = UNameMap.union (fst ctx.uctx_names) (fst ctx'.uctx_names) in
+ let newus = Univ.LSet.diff (Univ.ContextSet.levels ctx'.uctx_local)
+ (Univ.ContextSet.levels ctx.uctx_local) in
+ let newus = Univ.LSet.diff newus (Univ.LMap.domain ctx.uctx_univ_variables) in
+ let declarenew g =
+ Univ.LSet.fold (fun u g -> UGraph.add_universe u false g) newus g
+ in
+ let names_rev = Univ.LMap.union (snd ctx.uctx_names) (snd ctx'.uctx_names) in
+ { uctx_names = (names, names_rev);
+ uctx_local = local;
+ uctx_univ_variables =
+ Univ.LMap.subst_union ctx.uctx_univ_variables ctx'.uctx_univ_variables;
+ uctx_univ_algebraic =
+ Univ.LSet.union ctx.uctx_univ_algebraic ctx'.uctx_univ_algebraic;
+ uctx_initial_universes = declarenew ctx.uctx_initial_universes;
+ uctx_universes =
+ if local == ctx.uctx_local then ctx.uctx_universes
+ else
+ let cstrsr = Univ.ContextSet.constraints ctx'.uctx_local in
+ UGraph.merge_constraints cstrsr (declarenew ctx.uctx_universes) }
+
+let context_set ctx = ctx.uctx_local
+
+let constraints ctx = snd ctx.uctx_local
+
+let context ctx = Univ.ContextSet.to_context ctx.uctx_local
+
+let of_context_set ctx = { empty with uctx_local = ctx }
+
+let subst ctx = ctx.uctx_univ_variables
+
+let ugraph ctx = ctx.uctx_universes
+
+let algebraics ctx = ctx.uctx_univ_algebraic
+
+let constrain_variables diff ctx =
+ Univ.LSet.fold
+ (fun l cstrs ->
+ try
+ match Univ.LMap.find l ctx.uctx_univ_variables with
+ | Some u -> Univ.Constraint.add (l, Univ.Eq, Option.get (Univ.Universe.level u)) cstrs
+ | None -> cstrs
+ with Not_found | Option.IsNone -> cstrs)
+ diff Univ.Constraint.empty
+
+let add_uctx_names s l (names, names_rev) =
+ (UNameMap.add s l names, Univ.LMap.add l s names_rev)
+
+let of_binders b =
+ let ctx = empty in
+ let names =
+ List.fold_left (fun acc (id, l) -> add_uctx_names (Id.to_string id) l acc)
+ ctx.uctx_names b
+ in { ctx with uctx_names = names }
+
+let instantiate_variable l b v =
+ v := Univ.LMap.add l (Some b) !v
+
+exception UniversesDiffer
+
+let process_universe_constraints univs vars alg cstrs =
+ let vars = ref vars in
+ let normalize = Universes.normalize_universe_opt_subst vars in
+ let rec unify_universes fo l d r local =
+ let l = normalize l and r = normalize r in
+ if Univ.Universe.equal l r then local
+ else
+ let varinfo x =
+ match Univ.Universe.level x with
+ | None -> Inl x
+ | Some l -> Inr (l, Univ.LMap.mem l !vars, Univ.LSet.mem l alg)
+ in
+ if d == Universes.ULe then
+ if UGraph.check_leq univs l r then
+ (** Keep Prop/Set <= var around if var might be instantiated by prop or set
+ later. *)
+ if Univ.Universe.is_level l then
+ match Univ.Universe.level r with
+ | Some r ->
+ Univ.Constraint.add (Option.get (Univ.Universe.level l),Univ.Le,r) local
+ | _ -> local
+ else local
+ else
+ match Univ.Universe.level r with
+ | None -> error ("Algebraic universe on the right")
+ | Some rl ->
+ if Univ.Level.is_small rl then
+ let levels = Univ.Universe.levels l in
+ Univ.LSet.fold (fun l local ->
+ if Univ.Level.is_small l || Univ.LMap.mem l !vars then
+ unify_universes fo (Univ.Universe.make l) Universes.UEq r local
+ else raise (Univ.UniverseInconsistency (Univ.Le, Univ.Universe.make l, r, None)))
+ levels local
+ else
+ Univ.enforce_leq l r local
+ else if d == Universes.ULub then
+ match varinfo l, varinfo r with
+ | (Inr (l, true, _), Inr (r, _, _))
+ | (Inr (r, _, _), Inr (l, true, _)) ->
+ instantiate_variable l (Univ.Universe.make r) vars;
+ Univ.enforce_eq_level l r local
+ | Inr (_, _, _), Inr (_, _, _) ->
+ unify_universes true l Universes.UEq r local
+ | _, _ -> assert false
+ else (* d = Universes.UEq *)
+ match varinfo l, varinfo r with
+ | Inr (l', lloc, _), Inr (r', rloc, _) ->
+ let () =
+ if lloc then
+ instantiate_variable l' r vars
+ else if rloc then
+ instantiate_variable r' l vars
+ else if not (UGraph.check_eq univs l r) then
+ (* Two rigid/global levels, none of them being local,
+ one of them being Prop/Set, disallow *)
+ if Univ.Level.is_small l' || Univ.Level.is_small r' then
+ raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None))
+ else
+ if fo then
+ raise UniversesDiffer
+ in
+ Univ.enforce_eq_level l' r' local
+ | Inr (l, loc, alg), Inl r
+ | Inl r, Inr (l, loc, alg) ->
+ let inst = Univ.univ_level_rem l r r in
+ if alg then (instantiate_variable l inst vars; local)
+ else
+ let lu = Univ.Universe.make l in
+ if Univ.univ_level_mem l r then
+ Univ.enforce_leq inst lu local
+ else raise (Univ.UniverseInconsistency (Univ.Eq, lu, r, None))
+ | _, _ (* One of the two is algebraic or global *) ->
+ if UGraph.check_eq univs l r then local
+ else raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None))
+ in
+ let local =
+ Universes.Constraints.fold (fun (l,d,r) local -> unify_universes false l d r local)
+ cstrs Univ.Constraint.empty
+ in
+ !vars, local
+
+let add_constraints ctx cstrs =
+ let univs, local = ctx.uctx_local in
+ let cstrs' = Univ.Constraint.fold (fun (l,d,r) acc ->
+ let l = Univ.Universe.make l and r = Univ.Universe.make r in
+ let cstr' =
+ if d == Univ.Lt then (Univ.Universe.super l, Universes.ULe, r)
+ else (l, (if d == Univ.Le then Universes.ULe else Universes.UEq), r)
+ in Universes.Constraints.add cstr' acc)
+ cstrs Universes.Constraints.empty
+ in
+ let vars, local' =
+ process_universe_constraints ctx.uctx_universes
+ ctx.uctx_univ_variables ctx.uctx_univ_algebraic
+ cstrs'
+ in
+ { ctx with uctx_local = (univs, Univ.Constraint.union local local');
+ uctx_univ_variables = vars;
+ uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes }
+
+(* let addconstrkey = Profile.declare_profile "add_constraints_context";; *)
+(* let add_constraints_context = Profile.profile2 addconstrkey add_constraints_context;; *)
+
+let add_universe_constraints ctx cstrs =
+ let univs, local = ctx.uctx_local in
+ let vars, local' =
+ process_universe_constraints ctx.uctx_universes
+ ctx.uctx_univ_variables ctx.uctx_univ_algebraic
+ cstrs
+ in
+ { ctx with uctx_local = (univs, Univ.Constraint.union local local');
+ uctx_univ_variables = vars;
+ uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes }
+
+let pr_uctx_level uctx =
+ let map, map_rev = uctx.uctx_names in
+ fun l ->
+ try str(Univ.LMap.find l map_rev)
+ with Not_found ->
+ Universes.pr_with_global_universes l
+
+let universe_context ?names ctx =
+ match names with
+ | None -> [], Univ.ContextSet.to_context ctx.uctx_local
+ | Some pl ->
+ let levels = Univ.ContextSet.levels ctx.uctx_local in
+ let newinst, map, left =
+ List.fold_right
+ (fun (loc,id) (newinst, map, acc) ->
+ let l =
+ try UNameMap.find (Id.to_string id) (fst ctx.uctx_names)
+ with Not_found ->
+ user_err_loc (loc, "universe_context",
+ str"Universe " ++ Nameops.pr_id id ++ str" is not bound anymore.")
+ in (l :: newinst, (id, l) :: map, Univ.LSet.remove l acc))
+ pl ([], [], levels)
+ in
+ if not (Univ.LSet.is_empty left) then
+ let n = Univ.LSet.cardinal left in
+ errorlabstrm "universe_context"
+ (str(CString.plural n "Universe") ++ spc () ++
+ Univ.LSet.pr (pr_uctx_level ctx) left ++
+ spc () ++ str (CString.conjugate_verb_to_be n) ++ str" unbound.")
+ else
+ let inst = Univ.Instance.of_array (Array.of_list newinst) in
+ let ctx = Univ.UContext.make (inst,
+ Univ.ContextSet.constraints ctx.uctx_local)
+ in map, ctx
+
+let restrict ctx vars =
+ let uctx' = Universes.restrict_universe_context ctx.uctx_local vars in
+ { ctx with uctx_local = uctx' }
+
+type rigid =
+ | UnivRigid
+ | UnivFlexible of bool (** Is substitution by an algebraic ok? *)
+
+let univ_rigid = UnivRigid
+let univ_flexible = UnivFlexible false
+let univ_flexible_alg = UnivFlexible true
+
+let merge sideff rigid uctx ctx' =
+ let open Univ in
+ let levels = ContextSet.levels ctx' in
+ let uctx = if sideff then uctx else
+ match rigid with
+ | UnivRigid -> uctx
+ | UnivFlexible b ->
+ let fold u accu =
+ if LMap.mem u accu then accu
+ else LMap.add u None accu
+ in
+ let uvars' = LSet.fold fold levels uctx.uctx_univ_variables in
+ if b then
+ { uctx with uctx_univ_variables = uvars';
+ uctx_univ_algebraic = LSet.union uctx.uctx_univ_algebraic levels }
+ else { uctx with uctx_univ_variables = uvars' }
+ in
+ let uctx_local =
+ if sideff then uctx.uctx_local
+ else ContextSet.append ctx' uctx.uctx_local
+ in
+ let declare g =
+ LSet.fold (fun u g ->
+ try UGraph.add_universe u false g
+ with UGraph.AlreadyDeclared when sideff -> g)
+ levels g
+ in
+ let initial = declare uctx.uctx_initial_universes in
+ let univs = declare uctx.uctx_universes in
+ let uctx_universes = UGraph.merge_constraints (ContextSet.constraints ctx') univs in
+ { uctx with uctx_local; uctx_universes; uctx_initial_universes = initial }
+
+let merge_subst uctx s =
+ { uctx with uctx_univ_variables = Univ.LMap.subst_union uctx.uctx_univ_variables s }
+
+let emit_side_effects eff u =
+ let uctxs = Safe_typing.universes_of_private eff in
+ List.fold_left (merge true univ_rigid) u uctxs
+
+let new_univ_variable rigid name
+ ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) =
+ let u = Universes.new_univ_level (Global.current_dirpath ()) in
+ let ctx' = Univ.ContextSet.add_universe u ctx in
+ let uctx', pred =
+ match rigid with
+ | UnivRigid -> uctx, true
+ | UnivFlexible b ->
+ let uvars' = Univ.LMap.add u None uvars in
+ if b then {uctx with uctx_univ_variables = uvars';
+ uctx_univ_algebraic = Univ.LSet.add u avars}, false
+ else {uctx with uctx_univ_variables = uvars'}, false
+ in
+ let names =
+ match name with
+ | Some n -> add_uctx_names n u uctx.uctx_names
+ | None -> uctx.uctx_names
+ in
+ let initial =
+ UGraph.add_universe u false uctx.uctx_initial_universes
+ in
+ let uctx' =
+ {uctx' with uctx_names = names; uctx_local = ctx';
+ uctx_universes = UGraph.add_universe u false uctx.uctx_universes;
+ uctx_initial_universes = initial}
+ in uctx', u
+
+let add_global_univ uctx u =
+ let initial =
+ UGraph.add_universe u true uctx.uctx_initial_universes
+ in
+ let univs =
+ UGraph.add_universe u true uctx.uctx_universes
+ in
+ { uctx with uctx_local = Univ.ContextSet.add_universe u uctx.uctx_local;
+ uctx_initial_universes = initial;
+ uctx_universes = univs }
+
+let make_flexible_variable ctx b u =
+ let {uctx_univ_variables = uvars; uctx_univ_algebraic = avars} = ctx in
+ let uvars' = Univ.LMap.add u None uvars in
+ let avars' =
+ if b then
+ let uu = Univ.Universe.make u in
+ let substu_not_alg u' v =
+ Option.cata (fun vu -> Univ.Universe.equal uu vu && not (Univ.LSet.mem u' avars)) false v
+ in
+ if not (Univ.LMap.exists substu_not_alg uvars)
+ then Univ.LSet.add u avars else avars
+ else avars
+ in
+ {ctx with uctx_univ_variables = uvars';
+ uctx_univ_algebraic = avars'}
+
+let is_sort_variable uctx s =
+ match s with
+ | Sorts.Type u ->
+ (match Univ.universe_level u with
+ | Some l as x ->
+ if Univ.LSet.mem l (Univ.ContextSet.levels uctx.uctx_local) then x
+ else None
+ | None -> None)
+ | _ -> None
+
+let subst_univs_context_with_def def usubst (ctx, cst) =
+ (Univ.LSet.diff ctx def, Univ.subst_univs_constraints usubst cst)
+
+let normalize_variables uctx =
+ let normalized_variables, undef, def, subst =
+ Universes.normalize_univ_variables uctx.uctx_univ_variables
+ in
+ let ctx_local = subst_univs_context_with_def def (Univ.make_subst subst) uctx.uctx_local in
+ let ctx_local', univs = Universes.refresh_constraints uctx.uctx_initial_universes ctx_local in
+ subst, { uctx with uctx_local = ctx_local';
+ uctx_univ_variables = normalized_variables;
+ uctx_universes = univs }
+
+let abstract_undefined_variables uctx =
+ let vars' =
+ Univ.LMap.fold (fun u v acc ->
+ if v == None then Univ.LSet.remove u acc
+ else acc)
+ uctx.uctx_univ_variables uctx.uctx_univ_algebraic
+ in { uctx with uctx_local = Univ.ContextSet.empty;
+ uctx_univ_algebraic = vars' }
+
+let fix_undefined_variables uctx =
+ let algs', vars' =
+ Univ.LMap.fold (fun u v (algs, vars as acc) ->
+ if v == None then (Univ.LSet.remove u algs, Univ.LMap.remove u vars)
+ else acc)
+ uctx.uctx_univ_variables
+ (uctx.uctx_univ_algebraic, uctx.uctx_univ_variables)
+ in
+ { uctx with uctx_univ_variables = vars';
+ uctx_univ_algebraic = algs' }
+
+let refresh_undefined_univ_variables uctx =
+ let subst, ctx' = Universes.fresh_universe_context_set_instance uctx.uctx_local in
+ let alg = Univ.LSet.fold (fun u acc -> Univ.LSet.add (Univ.subst_univs_level_level subst u) acc)
+ uctx.uctx_univ_algebraic Univ.LSet.empty
+ in
+ let vars =
+ Univ.LMap.fold
+ (fun u v acc ->
+ Univ.LMap.add (Univ.subst_univs_level_level subst u)
+ (Option.map (Univ.subst_univs_level_universe subst) v) acc)
+ uctx.uctx_univ_variables Univ.LMap.empty
+ in
+ let declare g = Univ.LSet.fold (fun u g -> UGraph.add_universe u false g)
+ (Univ.ContextSet.levels ctx') g in
+ let initial = declare uctx.uctx_initial_universes in
+ let univs = declare UGraph.initial_universes in
+ let uctx' = {uctx_names = uctx.uctx_names;
+ uctx_local = ctx';
+ uctx_univ_variables = vars; uctx_univ_algebraic = alg;
+ uctx_universes = univs;
+ uctx_initial_universes = initial } in
+ uctx', subst
+
+let normalize uctx =
+ let rec fixpoint uctx =
+ let ((vars',algs'), us') =
+ Universes.normalize_context_set uctx.uctx_local uctx.uctx_univ_variables
+ uctx.uctx_univ_algebraic
+ in
+ if Univ.ContextSet.equal us' uctx.uctx_local then uctx
+ else
+ let us', universes = Universes.refresh_constraints uctx.uctx_initial_universes us' in
+ let uctx' =
+ { uctx_names = uctx.uctx_names;
+ uctx_local = us';
+ uctx_univ_variables = vars';
+ uctx_univ_algebraic = algs';
+ uctx_universes = universes;
+ uctx_initial_universes = uctx.uctx_initial_universes }
+ in fixpoint uctx'
+ in fixpoint uctx
+
+let universe_of_name uctx s =
+ UNameMap.find s (fst uctx.uctx_names)
+
+let add_universe_name uctx s l =
+ let names' = add_uctx_names s l uctx.uctx_names in
+ { uctx with uctx_names = names' }
+
+let update_sigma_env uctx env =
+ let univs = Environ.universes env in
+ let eunivs =
+ { uctx with uctx_initial_universes = univs;
+ uctx_universes = univs }
+ in
+ merge true univ_rigid eunivs eunivs.uctx_local
diff --git a/engine/uState.mli b/engine/uState.mli
new file mode 100644
index 000000000..3a6f77e14
--- /dev/null
+++ b/engine/uState.mli
@@ -0,0 +1,117 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(** Universe unification states *)
+
+open Names
+
+exception UniversesDiffer
+
+type t
+(** Type of universe unification states. They allow the incremental building of
+ universe constraints during an interactive proof. *)
+
+(** {5 Constructors} *)
+
+val empty : t
+
+val make : UGraph.t -> t
+
+val is_empty : t -> bool
+
+val union : t -> t -> t
+
+val of_context_set : Univ.universe_context_set -> t
+
+val of_binders : Universes.universe_binders -> t
+
+(** {5 Projections} *)
+
+val context_set : t -> Univ.universe_context_set
+(** The local context of the state, i.e. a set of bound variables together
+ with their associated constraints. *)
+
+val subst : t -> Universes.universe_opt_subst
+(** The local universes that are unification variables *)
+
+val ugraph : t -> UGraph.t
+(** The current graph extended with the local constraints *)
+
+val algebraics : t -> Univ.LSet.t
+(** The subset of unification variables that can be instantiated with algebraic
+ universes as they appear in types and universe instances only. *)
+
+val constraints : t -> Univ.constraints
+(** Shorthand for {!context_set} composed with {!ContextSet.constraints}. *)
+
+val context : t -> Univ.universe_context
+(** Shorthand for {!context_set} with {!Context_set.to_context}. *)
+
+(** {5 Constraints handling} *)
+
+val add_constraints : t -> Univ.constraints -> t
+(**
+ @raise UniversesDiffer
+*)
+
+val add_universe_constraints : t -> Universes.universe_constraints -> t
+(**
+ @raise UniversesDiffer
+*)
+
+(** {5 Names} *)
+
+val add_universe_name : t -> string -> Univ.Level.t -> t
+(** Associate a human-readable name to a local variable. *)
+
+val universe_of_name : t -> string -> Univ.Level.t
+(** Retrieve the universe associated to the name. *)
+
+(** {5 Unification} *)
+
+val restrict : t -> Univ.universe_set -> t
+
+type rigid =
+ | UnivRigid
+ | UnivFlexible of bool (** Is substitution by an algebraic ok? *)
+
+val univ_rigid : rigid
+val univ_flexible : rigid
+val univ_flexible_alg : rigid
+
+val merge : bool -> rigid -> t -> Univ.universe_context_set -> t
+val merge_subst : t -> Universes.universe_opt_subst -> t
+val emit_side_effects : Safe_typing.private_constants -> t -> t
+
+val new_univ_variable : rigid -> string option -> t -> t * Univ.Level.t
+val add_global_univ : t -> Univ.Level.t -> t
+val make_flexible_variable : t -> bool -> Univ.Level.t -> t
+
+val is_sort_variable : t -> Sorts.t -> Univ.Level.t option
+
+val normalize_variables : t -> Univ.universe_subst * t
+
+val constrain_variables : Univ.LSet.t -> t -> Univ.constraints
+
+val abstract_undefined_variables : t -> t
+
+val fix_undefined_variables : t -> t
+
+val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst
+
+val normalize : t -> t
+
+(** {5 TODO: Document me} *)
+
+val universe_context : ?names:(Id.t Loc.located) list -> t -> (Id.t * Univ.Level.t) list * Univ.universe_context
+
+val update_sigma_env : t -> Environ.env -> t
+
+(** {5 Pretty-printing} *)
+
+val pr_uctx_level : t -> Univ.Level.t -> Pp.std_ppcmds
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 03:07:09 +0000