diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/engine.mllib | 3 | ||||
| -rw-r--r-- | engine/evarutil.ml | 244 | ||||
| -rw-r--r-- | engine/evarutil.mli | 22 | ||||
| -rw-r--r-- | engine/evd.ml | 99 | ||||
| -rw-r--r-- | engine/evd.mli | 40 | ||||
| -rw-r--r-- | engine/ftactic.ml | 23 | ||||
| -rw-r--r-- | engine/ftactic.mli | 4 | ||||
| -rw-r--r-- | engine/geninterp.mli | 3 | ||||
| -rw-r--r-- | engine/logic_monad.ml | 20 | ||||
| -rw-r--r-- | engine/logic_monad.mli | 2 | ||||
| -rw-r--r-- | engine/namegen.ml | 116 | ||||
| -rw-r--r-- | engine/namegen.mli | 22 | ||||
| -rw-r--r-- | engine/proofview.ml | 220 | ||||
| -rw-r--r-- | engine/proofview.mli | 46 | ||||
| -rw-r--r-- | engine/proofview_monad.mli | 3 | ||||
| -rw-r--r-- | engine/sigma.ml | 12 | ||||
| -rw-r--r-- | engine/sigma.mli | 12 | ||||
| -rw-r--r-- | engine/termops.ml | 75 | ||||
| -rw-r--r-- | engine/termops.mli | 21 | ||||
| -rw-r--r-- | engine/uState.ml | 29 | ||||
| -rw-r--r-- | engine/uState.mli | 4 | ||||
| -rw-r--r-- | engine/universes.ml | 1131 | ||||
| -rw-r--r-- | engine/universes.mli | 231 |
23 files changed, 2047 insertions, 335 deletions
diff --git a/engine/engine.mllib b/engine/engine.mllib index 9ce5af8195..53cbbd73ef 100644 --- a/engine/engine.mllib +++ b/engine/engine.mllib @@ -1,9 +1,10 @@ Logic_monad -Termops Namegen +Universes UState Evd Sigma +Termops Proofview_monad Evarutil Proofview diff --git a/engine/evarutil.ml b/engine/evarutil.ml index c5dfe30332..13444cb379 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Names open Term @@ -18,6 +18,13 @@ open Environ open Evd open Sigma.Notations +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration + +let safe_evar_info sigma evk = + try Some (Evd.find sigma evk) + with Not_found -> None + let safe_evar_value sigma ev = try Some (Evd.existential_value sigma ev) with NotInstantiatedEvar | Not_found -> None @@ -66,12 +73,14 @@ let rec flush_and_check_evars sigma c = let rec whd_evar sigma c = match kind_of_term c with - | Evar ev -> - let (evk, args) = ev in + | Evar (evk, args) -> + begin match safe_evar_info sigma evk with + | Some ({ evar_body = Evar_defined c } as info) -> let args = Array.map (fun c -> whd_evar sigma c) args in - (match safe_evar_value sigma (evk, args) with - Some c -> whd_evar sigma c - | None -> c) + let c = instantiate_evar_array info c args in + whd_evar sigma c + | _ -> c + end | Sort (Type u) -> let u' = Evd.normalize_universe sigma u in if u' == u then c else mkSort (Sorts.sort_of_univ u') @@ -161,13 +170,11 @@ let is_ground_term evd t = not (has_undefined_evars evd t) let is_ground_env evd env = - let open Context.Rel.Declaration in let is_ground_rel_decl = function - | LocalDef (_,b,_) -> is_ground_term evd b + | RelDecl.LocalDef (_,b,_) -> is_ground_term evd b | _ -> true in - let open Context.Named.Declaration in let is_ground_named_decl = function - | LocalDef (_,b,_) -> is_ground_term evd b + | NamedDecl.LocalDef (_,b,_) -> is_ground_term evd b | _ -> true in List.for_all is_ground_rel_decl (rel_context env) && List.for_all is_ground_named_decl (named_context env) @@ -192,6 +199,7 @@ let head_evar = | Case (_,_,c,_) -> hrec c | App (c,_) -> hrec c | Cast (c,_,_) -> hrec c + | Proj (p, c) -> hrec c | _ -> raise NoHeadEvar in hrec @@ -248,11 +256,10 @@ let non_instantiated sigma = (************************) let make_pure_subst evi args = - let open Context.Named.Declaration in snd (List.fold_right (fun decl (args,l) -> match args with - | a::rest -> (rest, (get_id decl, a)::l) + | a::rest -> (rest, (NamedDecl.get_id decl, a)::l) | _ -> anomaly (Pp.str "Instance does not match its signature")) (evar_filtered_context evi) (Array.rev_to_list args,[])) @@ -289,78 +296,101 @@ let make_pure_subst evi args = * we have the property that u and phi(t) are convertible in env. *) +let csubst_subst (k, s) c = + let rec subst n c = match Constr.kind c with + | Rel m -> + if m <= n then c + else if m - n <= k then Int.Map.find (k - m + n) s + else mkRel (m - k) + | _ -> Constr.map_with_binders succ subst n c + in + if k = 0 then c else subst 0 c + let subst2 subst vsubst c = - substl subst (replace_vars vsubst c) + csubst_subst subst (replace_vars vsubst c) -let push_rel_context_to_named_context env typ = - (* compute the instances relative to the named context and rel_context *) - let open Context.Named.Declaration in - let ids = List.map get_id (named_context env) in - let inst_vars = List.map mkVar ids in - let inst_rels = List.rev (rel_list 0 (nb_rel env)) in +let next_ident_away id avoid = + let avoid id = Id.Set.mem id avoid in + next_ident_away_from id avoid + +let next_name_away na avoid = + let avoid id = Id.Set.mem id avoid in + let id = match na with Name id -> id | Anonymous -> default_non_dependent_ident in + next_ident_away_from id avoid + +type csubst = int * Constr.t Int.Map.t + +let empty_csubst = (0, Int.Map.empty) + +type ext_named_context = + csubst * (Id.t * Constr.constr) list * + Id.Set.t * Context.Named.t + +let push_var id (n, s) = + let s = Int.Map.add n (mkVar id) s in + (succ n, s) + +let push_rel_decl_to_named_context decl (subst, vsubst, avoid, nc) = let replace_var_named_declaration id0 id decl = - let id' = get_id decl in + let id' = NamedDecl.get_id decl in let id' = if Id.equal id0 id' then id else id' in let vsubst = [id0 , mkVar id] in - decl |> set_id id' |> map_constr (replace_vars vsubst) - in - let replace_var_named_context id0 id env = - let nc = Environ.named_context env in - let nc' = List.map (replace_var_named_declaration id0 id) nc in - Environ.reset_with_named_context (val_of_named_context nc') env + decl |> NamedDecl.set_id id' |> NamedDecl.map_constr (replace_vars vsubst) in let extract_if_neq id = function | Anonymous -> None | Name id' when id_ord id id' = 0 -> None | Name id' -> Some id' in - (* move the rel context to a named context and extend the named instance *) - (* with vars of the rel context *) - (* We do keep the instances corresponding to local definition (see above) *) - let (subst, vsubst, _, env) = - Context.Rel.fold_outside - (fun decl (subst, vsubst, avoid, env) -> - let open Context.Rel.Declaration in - let na = get_name decl in - let c = get_value decl in - let t = get_type decl in - let open Context.Named.Declaration in - let id = - (* ppedrot: we want to infer nicer names for the refine tactic, but - keeping at the same time backward compatibility in other code - using this function. For now, we only attempt to preserve the - old behaviour of Program, but ultimately, one should do something - about this whole name generation problem. *) - if Flags.is_program_mode () then next_name_away na avoid - else next_ident_away (id_of_name_using_hdchar env t na) avoid - in - match extract_if_neq id na with - | Some id0 when not (is_section_variable id0) -> - (* spiwack: if [id<>id0], rather than introducing a new - binding named [id], we will keep [id0] (the name given - by the user) and rename [id0] into [id] in the named - context. Unless [id] is a section variable. *) - let subst = List.map (replace_vars [id0,mkVar id]) subst in - let vsubst = (id0,mkVar id)::vsubst in - let d = match c with - | None -> LocalAssum (id0, subst2 subst vsubst t) - | Some c -> LocalDef (id0, subst2 subst vsubst c, subst2 subst vsubst t) - in - let env = replace_var_named_context id0 id env in - (mkVar id0 :: subst, vsubst, id::avoid, push_named d env) - | _ -> - (* spiwack: if [id0] is a section variable renaming it is - incorrect. We revert to a less robust behaviour where - the new binder has name [id]. Which amounts to the same - behaviour than when [id=id0]. *) - let d = match c with - | None -> LocalAssum (id, subst2 subst vsubst t) - | Some c -> LocalDef (id, subst2 subst vsubst c, subst2 subst vsubst t) - in - (mkVar id :: subst, vsubst, id::avoid, push_named d env) - ) - (rel_context env) ~init:([], [], ids, env) in - (named_context_val env, subst2 subst vsubst typ, inst_rels@inst_vars, subst, vsubst) + let na = RelDecl.get_name decl in + let id = + (* ppedrot: we want to infer nicer names for the refine tactic, but + keeping at the same time backward compatibility in other code + using this function. For now, we only attempt to preserve the + old behaviour of Program, but ultimately, one should do something + about this whole name generation problem. *) + if Flags.is_program_mode () then next_name_away na avoid + else + (** id_of_name_using_hdchar only depends on the rel context which is empty + here *) + next_ident_away (id_of_name_using_hdchar empty_env (RelDecl.get_type decl) na) avoid + in + match extract_if_neq id na with + | Some id0 when not (is_section_variable id0) -> + (* spiwack: if [id<>id0], rather than introducing a new + binding named [id], we will keep [id0] (the name given + by the user) and rename [id0] into [id] in the named + context. Unless [id] is a section variable. *) + let subst = (fst subst, Int.Map.map (replace_vars [id0,mkVar id]) (snd subst)) in + let vsubst = (id0,mkVar id)::vsubst in + let d = decl |> NamedDecl.of_rel_decl (fun _ -> id0) |> NamedDecl.map_constr (subst2 subst vsubst) in + let nc = List.map (replace_var_named_declaration id0 id) nc in + (push_var id0 subst, vsubst, Id.Set.add id avoid, d :: nc) + | _ -> + (* spiwack: if [id0] is a section variable renaming it is + incorrect. We revert to a less robust behaviour where + the new binder has name [id]. Which amounts to the same + behaviour than when [id=id0]. *) + let d = decl |> NamedDecl.of_rel_decl (fun _ -> id) |> NamedDecl.map_constr (subst2 subst vsubst) in + (push_var id subst, vsubst, Id.Set.add id avoid, d :: nc) + +let push_rel_context_to_named_context env typ = + (* compute the instances relative to the named context and rel_context *) + let open Context.Named.Declaration in + let ids = List.map get_id (named_context env) in + let inst_vars = List.map mkVar ids in + if List.is_empty (Environ.rel_context env) then + (named_context_val env, typ, inst_vars, empty_csubst, []) + else + let avoid = List.fold_right Id.Set.add ids Id.Set.empty in + let inst_rels = List.rev (rel_list 0 (nb_rel env)) in + (* move the rel context to a named context and extend the named instance *) + (* with vars of the rel context *) + (* We do keep the instances corresponding to local definition (see above) *) + let (subst, vsubst, _, env) = + Context.Rel.fold_outside push_rel_decl_to_named_context + (rel_context env) ~init:(empty_csubst, [], avoid, named_context env) in + (val_of_named_context env, subst2 subst vsubst typ, inst_rels@inst_vars, subst, vsubst) (*------------------------------------* * Entry points to define new evars * @@ -471,27 +501,30 @@ let cleared = Store.field () exception Depends of Id.t -let rec check_and_clear_in_constr env evdref err ids c = +let rec check_and_clear_in_constr env evdref err ids global c = (* returns a new constr where all the evars have been 'cleaned' (ie the hypotheses ids have been removed from the contexts of - evars) *) - let check id' = - if Id.Set.mem id' ids then - raise (ClearDependencyError (id',err)) - in + evars). [global] should be true iff there is some variable of [ids] which + is a section variable *) match kind_of_term c with | Var id' -> - check id'; c + if Id.Set.mem id' ids then raise (ClearDependencyError (id', err)) else c | ( Const _ | Ind _ | Construct _ ) -> - let vars = Environ.vars_of_global env c in - Id.Set.iter check vars; c + let () = if global then + let check id' = + if Id.Set.mem id' ids then + raise (ClearDependencyError (id',err)) + in + Id.Set.iter check (Environ.vars_of_global env c) + in + c | Evar (evk,l as ev) -> if Evd.is_defined !evdref evk then (* If evk is already defined we replace it by its definition *) let nc = whd_evar !evdref c in - (check_and_clear_in_constr env evdref err ids nc) + (check_and_clear_in_constr env evdref err ids global nc) else (* We check for dependencies to elements of ids in the evar_info corresponding to e and in the instance of @@ -518,15 +551,15 @@ let rec check_and_clear_in_constr env evdref err ids c = let () = Id.Map.iter check ri in (* No dependency at all, we can keep this ev's context hyp *) (ri, true::filter) - with Depends id -> let open Context.Named.Declaration in - (Id.Map.add (get_id h) id ri, false::filter)) + with Depends id -> (Id.Map.add (NamedDecl.get_id h) id ri, false::filter)) ctxt (Array.to_list l) (Id.Map.empty,[]) in (* Check if some rid to clear in the context of ev has dependencies in the type of ev and adjust the source of the dependency *) let _nconcl = try let nids = Id.Map.domain rids in - check_and_clear_in_constr env evdref (EvarTypingBreak ev) nids (evar_concl evi) + let global = Id.Set.exists is_section_variable nids in + check_and_clear_in_constr env evdref (EvarTypingBreak ev) nids global (evar_concl evi) with ClearDependencyError (rid,err) -> raise (ClearDependencyError (Id.Map.find rid rids,err)) in @@ -547,19 +580,19 @@ let rec check_and_clear_in_constr env evdref err ids c = (* spiwack: /hacking session *) whd_evar !evdref c - | _ -> map_constr (check_and_clear_in_constr env evdref err ids) c + | _ -> map_constr (check_and_clear_in_constr env evdref err ids global) c let clear_hyps_in_evi_main env evdref hyps terms ids = (* clear_hyps_in_evi erases hypotheses ids in hyps, checking if some hypothesis does not depend on a element of ids, and erases ids in the contexts of the evars occurring in evi *) + let global = Id.Set.exists is_section_variable ids in let terms = - List.map (check_and_clear_in_constr env evdref (OccurHypInSimpleClause None) ids) terms in + List.map (check_and_clear_in_constr env evdref (OccurHypInSimpleClause None) ids global) terms in let nhyps = - let open Context.Named.Declaration in let check_context decl = - let err = OccurHypInSimpleClause (Some (get_id decl)) in - map_constr (check_and_clear_in_constr env evdref err ids) decl + let err = OccurHypInSimpleClause (Some (NamedDecl.get_id decl)) in + NamedDecl.map_constr (check_and_clear_in_constr env evdref err ids global) decl in let check_value vk = match force_lazy_val vk with | None -> vk @@ -598,8 +631,8 @@ let process_dependent_evar q acc evm is_dependent e = hypotheses), they are all dependent. *) queue_term q true evi.evar_concl; List.iter begin fun decl -> - let open Context.Named.Declaration in - queue_term q true (get_type decl); + let open NamedDecl in + queue_term q true (NamedDecl.get_type decl); match decl with | LocalAssum _ -> () | LocalDef (_,b,_) -> queue_term q true b @@ -634,6 +667,28 @@ let gather_dependent_evars evm l = (* /spiwack *) +(** [advance sigma g] returns [Some g'] if [g'] is undefined and is + the current avatar of [g] (for instance [g] was changed by [clear] + into [g']). It returns [None] if [g] has been (partially) + solved. *) +(* spiwack: [advance] is probably performance critical, and the good + behaviour of its definition may depend sensitively to the actual + definition of [Evd.find]. Currently, [Evd.find] starts looking for + a value in the heap of undefined variable, which is small. Hence in + the most common case, where [advance] is applied to an unsolved + goal ([advance] is used to figure if a side effect has modified the + goal) it terminates quickly. *) +let rec advance sigma evk = + let evi = Evd.find sigma evk in + match evi.evar_body with + | Evar_empty -> Some evk + | Evar_defined v -> + if Option.default false (Store.get evi.evar_extra cleared) then + let (evk,_) = Term.destEvar v in + advance sigma evk + else + None + (** The following functions return the set of undefined evars contained in the object, the defined evars being traversed. This is roughly a combination of the previous functions and @@ -653,9 +708,8 @@ let undefined_evars_of_term evd t = evrec Evar.Set.empty t let undefined_evars_of_named_context evd nc = - let open Context.Named.Declaration in Context.Named.fold_outside - (fold (fun c s -> Evar.Set.union s (undefined_evars_of_term evd c))) + (NamedDecl.fold_constr (fun c s -> Evar.Set.union s (undefined_evars_of_term evd c))) nc ~init:Evar.Set.empty diff --git a/engine/evarutil.mli b/engine/evarutil.mli index ffff2c5dd9..7fdc7aac78 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -11,7 +11,7 @@ open Term open Evd open Environ -(** {5 This modules provides useful functions for unification modulo evars } *) +(** This module provides useful higher-level functions for evar manipulation. *) (** {6 Metas} *) @@ -110,6 +110,12 @@ val is_ground_env : evar_map -> env -> bool its (partial) definition. *) val gather_dependent_evars : evar_map -> evar list -> (Evar.Set.t option) Evar.Map.t +(** [advance sigma g] returns [Some g'] if [g'] is undefined and is + the current avatar of [g] (for instance [g] was changed by [clear] + into [g']). It returns [None] if [g] has been (partially) + solved. *) +val advance : evar_map -> evar -> evar option + (** The following functions return the set of undefined evars contained in the object, the defined evars being traversed. This is roughly a combination of the previous functions and @@ -199,8 +205,20 @@ val clear_hyps_in_evi : env -> evar_map ref -> named_context_val -> types -> val clear_hyps2_in_evi : env -> evar_map ref -> named_context_val -> types -> types -> Id.Set.t -> named_context_val * types * types +type csubst + +val empty_csubst : csubst +val csubst_subst : csubst -> Constr.t -> Constr.t + +type ext_named_context = + csubst * (Id.t * Constr.constr) list * + Id.Set.t * Context.Named.t + +val push_rel_decl_to_named_context : + Context.Rel.Declaration.t -> ext_named_context -> ext_named_context + val push_rel_context_to_named_context : Environ.env -> types -> - named_context_val * types * constr list * constr list * (identifier*constr) list + named_context_val * types * constr list * csubst * (identifier*constr) list val generalize_evar_over_rels : evar_map -> existential -> types * constr list diff --git a/engine/evd.ml b/engine/evd.ml index b883db615e..62d3963954 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -7,17 +7,19 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Names open Nameops open Term open Vars -open Termops open Environ open Globnames open Context.Named.Declaration +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration + (** Generic filters *) module Filter : sig @@ -226,7 +228,7 @@ let evar_instance_array test_id info args = if i < len then let c = Array.unsafe_get args i in if test_id d c then instrec filter ctxt (succ i) - else (get_id d, c) :: instrec filter ctxt (succ i) + else (NamedDecl.get_id d, c) :: instrec filter ctxt (succ i) else instance_mismatch () | _ -> instance_mismatch () in @@ -235,7 +237,7 @@ let evar_instance_array test_id info args = let map i d = if (i < len) then let c = Array.unsafe_get args i in - if test_id d c then None else Some (get_id d, c) + if test_id d c then None else Some (NamedDecl.get_id d, c) else instance_mismatch () in List.map_filter_i map (evar_context info) @@ -243,7 +245,7 @@ let evar_instance_array test_id info args = instrec filter (evar_context info) 0 let make_evar_instance_array info args = - evar_instance_array (isVarId % get_id) info args + evar_instance_array (NamedDecl.get_id %> isVarId) info args let instantiate_evar_array info c args = let inst = make_evar_instance_array info args in @@ -252,6 +254,7 @@ let instantiate_evar_array info c args = | _ -> 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 @@ -283,7 +286,7 @@ 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 + | _ -> Term.fold_constr collrec acc c in collrec Int.Set.empty c @@ -382,8 +385,7 @@ let add_name_newly_undefined naming evk evi (evtoid, idtoev as names) = | Misctypes.IntroAnonymous -> None | Misctypes.IntroIdentifier id -> if Idmap.mem id idtoev then - user_err_loc - (Loc.ghost,"",str "Already an existential evar of name " ++ pr_id id); + user_err (str "Already an existential evar of name " ++ pr_id id); Some id | Misctypes.IntroFresh id -> let id = Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev) in @@ -640,6 +642,7 @@ let set_universe_context evd uctx' = { evd with universes = uctx' } let add_conv_pb ?(tail=false) pb d = + (** MS: we have duplicates here, why? *) if tail then {d with conv_pbs = d.conv_pbs @ [pb]} else {d with conv_pbs = pb::d.conv_pbs} @@ -678,13 +681,16 @@ let restrict evk filter ?candidates evd = { evar_info with evar_filter = filter; evar_candidates = candidates; evar_extra = Store.empty } in + let last_mods = match evd.conv_pbs with + | [] -> evd.last_mods + | _ -> Evar.Set.add evk evd.last_mods in let evar_names = EvNames.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 (mkVar % get_id) ctxt in + let id_inst = Array.map_of_list (NamedDecl.get_id %> mkVar) ctxt in let body = mkEvar(evk',id_inst) in let (defn_evars, undf_evars) = define_aux 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' + defn_evars; last_mods; evar_names }, evk' let downcast evk ccl evd = let evar_info = EvMap.find evk evd.undf_evars in @@ -730,23 +736,22 @@ 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 + | _ -> Term.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 + | _ -> Term.fold_constr evrec acc c in evrec Evar.Set.empty c let evars_of_named_context nc = - List.fold_right (fun decl s -> - Option.fold_left (fun s t -> - Evar.Set.union s (evars_of_term t)) - (Evar.Set.union s (evars_of_term (get_type decl))) (get_value decl)) - nc Evar.Set.empty + Context.Named.fold_outside + (NamedDecl.fold_constr (fun constr s -> Evar.Set.union s (evars_of_term constr))) + nc + ~init:Evar.Set.empty let evars_of_filtered_evar_info evi = Evar.Set.union (evars_of_term evi.evar_concl) @@ -789,16 +794,16 @@ let merge_universe_subst evd subst = let with_context_set ?loc rigid d (a, ctx) = (merge_context_set ?loc rigid d ctx, a) -let new_univ_level_variable ?loc ?name ?(predicative=true) rigid evd = +let new_univ_level_variable ?loc ?name rigid evd = let uctx', u = UState.new_univ_variable ?loc rigid name evd.universes in ({evd with universes = uctx'}, u) -let new_univ_variable ?loc ?name ?(predicative=true) rigid evd = +let new_univ_variable ?loc ?name rigid evd = let uctx', u = UState.new_univ_variable ?loc rigid name evd.universes in ({evd with universes = uctx'}, Univ.Universe.make u) -let new_sort_variable ?loc ?name ?(predicative=true) rigid d = - let (d', u) = new_univ_variable ?loc rigid ?name ~predicative d in +let new_sort_variable ?loc ?name rigid d = + let (d', u) = new_univ_variable ?loc rigid ?name d in (d', Type u) let add_global_univ d u = @@ -852,6 +857,13 @@ let is_eq_sort s1 s2 = if Univ.Universe.equal u1 u2 then None else Some (u1, u2) +(* Precondition: l is not defined in the substitution *) +let universe_rigidity evd l = + let uctx = evd.universes in + if Univ.LSet.mem l (Univ.ContextSet.levels (UState.context_set uctx)) then + UnivFlexible (Univ.LSet.mem l (UState.algebraics uctx)) + else UnivRigid + let normalize_universe evd = let vars = ref (UState.subst evd.universes) in let normalize = Universes.normalize_universe_opt_subst vars in @@ -998,7 +1010,7 @@ let declare_principal_goal evk evd = | None -> { evd with future_goals = evk::evd.future_goals; principal_future_goal=Some evk; } - | Some _ -> Errors.error "Only one main subgoal per instantiation." + | Some _ -> CErrors.error "Only one main subgoal per instantiation." let future_goals evd = evd.future_goals @@ -1257,6 +1269,14 @@ let pr_instance_status (sc,typ) = | TypeProcessed -> str " [type is checked]" end +let protect f x = + try f x + with e -> str "EXCEPTION: " ++ str (Printexc.to_string e) + +let (f_print_constr, print_constr_hook) = Hook.make () + +let print_constr a = protect (fun c -> Hook.get f_print_constr (Global.env ()) c) a + let pr_meta_map mmap = let pr_name = function Name id -> str"[" ++ pr_id id ++ str"]" @@ -1276,13 +1296,13 @@ let pr_meta_map mmap = prlist pr_meta_binding (metamap_to_list mmap) let pr_decl (decl,ok) = - let id = get_id decl in - match get_value decl 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 "}") + match decl with + | LocalAssum (id,_) -> if ok then pr_id id else (str "{" ++ pr_id id ++ str "}") + | LocalDef (id,c,_) -> str (if ok then "(" else "{") ++ pr_id id ++ str ":=" ++ + print_constr c ++ str (if ok then ")" else "}") let pr_evar_source = function + | Evar_kinds.NamedHole id -> pr_id id | Evar_kinds.QuestionMark _ -> str "underscore" | Evar_kinds.CasesType false -> str "pattern-matching return predicate" | Evar_kinds.CasesType true -> @@ -1391,12 +1411,11 @@ let pr_evar_universe_context ctx = 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 decl = pr_body (Name (get_id decl)) (get_value decl) in - let pr_rel_decl decl = let open Context.Rel.Declaration in - pr_body (get_name decl) (get_value decl) in + let pr_rel_decl = function + | RelDecl.LocalAssum (n,_) -> pr_name n + | RelDecl.LocalDef (n,b,_) -> str "(" ++ pr_name n ++ str " := " ++ print_constr b ++ str ")" + in + let pr_named_decl = NamedDecl.to_rel_decl %> pr_rel_decl 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 () ++ @@ -1404,12 +1423,22 @@ let print_env_short env = let pr_evar_constraints pbs = let pr_evconstr (pbty, env, t1, t2) = + let env = + (** We currently allow evar instances to refer to anonymous de + Bruijn indices, so we protect the error printing code in this + case by giving names to every de Bruijn variable in the + rel_context of the conversion problem. MS: we should rather + stop depending on anonymous variables, they can be used to + indicate independency. Also, this depends on a strategy for + naming/renaming. *) + Namegen.make_all_name_different env + in print_env_short env ++ spc () ++ str "|-" ++ spc () ++ - print_constr_env env t1 ++ spc () ++ + Hook.get f_print_constr env t1 ++ spc () ++ str (match pbty with | Reduction.CONV -> "==" | Reduction.CUMUL -> "<=") ++ - spc () ++ print_constr_env env t2 + spc () ++ Hook.get f_print_constr env t2 in prlist_with_sep fnl pr_evconstr pbs diff --git a/engine/evd.mli b/engine/evd.mli index 3ae6e586c1..993ed300bc 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -12,7 +12,10 @@ open Names open Term open Environ -(** {5 Existential variables and unification states} +(** This file defines the pervasive unification state used everywhere in Coq + tactic engine. It is very low-level and most of the functions exported here + are irrelevant to the standard API user. Consider using {!Evarutil}, + {!Sigma} or {!Proofview} instead. A unification state (of type [evar_map]) is primarily a finite mapping from existential variables to records containing the type of the evar @@ -23,6 +26,8 @@ open Environ It also contains conversion constraints, debugging information and information about meta variables. *) +(** {5 Existential variables and unification states} *) + (** {6 Evars} *) type evar = existential_key @@ -93,11 +98,12 @@ type evar_info = { (** Optional content of the evar. *) evar_filter : Filter.t; (** Boolean mask over {!evar_hyps}. Should have the same length. - TODO: document me more. *) + When filtered out, the corresponding variable is not allowed to occur + in the solution *) evar_source : Evar_kinds.t located; (** Information about the evar. *) evar_candidates : constr list option; - (** TODO: document this *) + (** List of possible solutions when known that it is a finite list *) evar_extra : Store.t (** Extra store, used for clever hacks. *) } @@ -343,7 +349,6 @@ val on_sig : 'a sigma -> (evar_map -> evar_map * 'b) -> 'a sigma * 'b 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 @@ -462,7 +467,17 @@ val retract_coercible_metas : evar_map -> metabinding list * evar_map (********************************************************* Sort/universe variables *) -(** Rigid or flexible universe variables *) +(** Rigid or flexible universe variables. + + [UnivRigid] variables are user-provided or come from an explicit + [Type] in the source, we do not minimize them or unify them eagerly. + + [UnivFlexible alg] variables are fresh universe variables of + polymorphic constants or generated during refinement, sometimes in + algebraic position (i.e. not appearing in the term at the moment of + creation). They are the candidates for minimization (if alg, to an + algebraic universe) and unified eagerly in the first-order + unification heurstic. *) type rigid = UState.rigid = | UnivRigid @@ -504,11 +519,13 @@ val normalize_evar_universe_context_variables : evar_universe_context -> val normalize_evar_universe_context : evar_universe_context -> evar_universe_context -val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe_level -val new_univ_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe -val new_sort_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * sorts +val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * Univ.universe_level +val new_univ_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * Univ.universe +val new_sort_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * sorts + val add_global_univ : evar_map -> Univ.Level.t -> evar_map - + +val universe_rigidity : evar_map -> Univ.Level.t -> rigid 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 @@ -564,8 +581,8 @@ val fresh_constant_instance : ?loc:Loc.t -> env -> evar_map -> constant -> evar_ val fresh_inductive_instance : ?loc:Loc.t -> env -> evar_map -> inductive -> evar_map * pinductive val fresh_constructor_instance : ?loc:Loc.t -> env -> evar_map -> constructor -> evar_map * pconstructor -val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:Univ.Instance.t -> env -> evar_map -> - Globnames.global_reference -> evar_map * constr +val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:Univ.Instance.t -> env -> + evar_map -> Globnames.global_reference -> evar_map * constr (******************************************************************** Conversion w.r.t. an evar map, not unifying universes. See @@ -601,6 +618,7 @@ val pr_evar_suggested_name : existential_key -> evar_map -> Id.t (** {5 Debug pretty-printers} *) +val print_constr_hook : (Environ.env -> constr -> Pp.std_ppcmds) Hook.t 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 diff --git a/engine/ftactic.ml b/engine/ftactic.ml index 588709873e..aeaaea7e48 100644 --- a/engine/ftactic.ml +++ b/engine/ftactic.ml @@ -29,13 +29,28 @@ let bind (type a) (type b) (m : a t) (f : a -> b t) : b t = m >>= function | Uniform x -> (** We dispatch the uniform result on each goal under focus, as we know that the [m] argument was actually dependent. *) - Proofview.Goal.goals >>= fun l -> - let ans = List.map (fun _ -> x) l in + Proofview.Goal.goals >>= fun goals -> + let ans = List.map (fun g -> (g,x)) goals in Proofview.tclUNIT ans - | Depends l -> Proofview.tclUNIT l + | Depends l -> + Proofview.Goal.goals >>= fun goals -> + Proofview.tclUNIT (List.combine goals l) + in + (* After the tactic has run, some goals which were previously + produced may have been solved by side effects. The values + attached to such goals must be discarded, otherwise the list of + result would not have the same length as the list of focused + goals, which is an invariant of the [Ftactic] module. It is the + reason why a goal is attached to each result above. *) + let filter (g,x) = + g >>= fun g -> + Proofview.Goal.unsolved g >>= function + | true -> Proofview.tclUNIT (Some x) + | false -> Proofview.tclUNIT None in Proofview.tclDISPATCHL (List.map f l) >>= fun l -> - Proofview.tclUNIT (Depends (List.concat l)) + Proofview.Monad.List.map_filter filter (List.concat l) >>= fun filtered -> + Proofview.tclUNIT (Depends filtered) let goals = Proofview.Goal.goals >>= fun l -> Proofview.tclUNIT (Depends l) let set_sigma r = diff --git a/engine/ftactic.mli b/engine/ftactic.mli index 19041f1698..5db373199e 100644 --- a/engine/ftactic.mli +++ b/engine/ftactic.mli @@ -8,7 +8,9 @@ open Proofview.Notations -(** Potentially focussing tactics *) +(** This module defines potentially focussing tactics. They are used by Ltac to + emulate the historical behaviour of always-focussed tactics while still + allowing to remain global when the goal is not needed. *) type +'a focus diff --git a/engine/geninterp.mli b/engine/geninterp.mli index 42e1e3784c..b70671a2d9 100644 --- a/engine/geninterp.mli +++ b/engine/geninterp.mli @@ -6,7 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** Interpretation functions for generic arguments. *) +(** Interpretation functions for generic arguments and interpreted Ltac + values. *) open Names open Genarg diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml index 64be07b9c7..6e821ea5aa 100644 --- a/engine/logic_monad.ml +++ b/engine/logic_monad.ml @@ -33,11 +33,11 @@ exception Timeout 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 +let _ = CErrors.register_handler begin function + | Timeout -> CErrors.user_err ~hdr:"Some timeout function" (Pp.str"Timeout!") + | Exception e -> CErrors.print e + | TacticFailure e -> CErrors.print e + | _ -> Pervasives.raise CErrors.Unhandled end (** {6 Non-logical layer} *) @@ -86,11 +86,11 @@ struct let catch = fun s h -> (); fun () -> try s () with Exception e as src -> - let (src, info) = Errors.push src in + let (src, info) = CErrors.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 (e, info) = CErrors.push e in raise ~info e () let print_char = fun c -> (); fun () -> print_char c @@ -99,8 +99,8 @@ struct let make f = (); fun () -> try f () - with e when Errors.noncritical e -> - let (e, info) = Errors.push e in + with e when CErrors.noncritical e -> + let (e, info) = CErrors.push e in Util.iraise (Exception e, info) (** Use the current logger. The buffer is also flushed. *) @@ -112,7 +112,7 @@ struct let run = fun x -> try x () with Exception e as src -> - let (src, info) = Errors.push src in + let (src, info) = CErrors.push src in Util.iraise (e, info) end diff --git a/engine/logic_monad.mli b/engine/logic_monad.mli index c5160443b1..dd122cca0f 100644 --- a/engine/logic_monad.mli +++ b/engine/logic_monad.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** This file defines the low-level monadic operations used by the +(** This file implements 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) diff --git a/engine/namegen.ml b/engine/namegen.ml index 6b2b585316..e56ec2877c 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -21,9 +21,10 @@ open Nameops open Libnames open Globnames open Environ -open Termops open Context.Rel.Declaration +module RelDecl = Context.Rel.Declaration + (**********************************************************************) (* Conventional names *) @@ -76,6 +77,10 @@ let is_constructor id = with Not_found -> false +let is_section_variable id = + try let _ = Global.lookup_named id in true + with Not_found -> false + (**********************************************************************) (* Generating "intuitive" names from its type *) @@ -114,9 +119,9 @@ let hdchar env c = | Rel n -> (if n<=k then "p" (* the initial term is flexible product/function *) else - try match Environ.lookup_rel (n-k) env |> to_tuple with - | (Name id,_,_) -> lowercase_first_char id - | (Anonymous,_,t) -> hdrec 0 (lift (n-k) t) + try match Environ.lookup_rel (n-k) env with + | LocalAssum (Name id,_) | LocalDef (Name id,_,_) -> lowercase_first_char id + | LocalAssum (Anonymous,t) | LocalDef (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 @@ -168,7 +173,7 @@ let it_mkLambda_or_LetIn_name env b hyps = (* 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 + let rec name_rec id = if bad id then name_rec (increment_subscript id) else id in name_rec id (* Restart subscript from x0 if name starts with xN, or x00 if name @@ -180,32 +185,44 @@ let restart_subscript id = *** 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 +let visible_ids (nenv, c) = + let accu = ref (Refset_env.empty, Int.Set.empty, Id.Set.empty) in + let rec visible_ids n c = match kind_of_term c with + | Const _ | Ind _ | Construct _ | Var _ -> + let (gseen, vseen, ids) = !accu in + let g = global_of_constr c in + if not (Refset_env.mem g gseen) then + begin + try + let gseen = Refset_env.add g gseen in + let short = shortest_qualid_of_global Id.Set.empty g in + let dir, id = repr_qualid short in + let ids = if DirPath.is_empty dir then Id.Set.add id ids else ids in + accu := (gseen, vseen, ids) + with Not_found when !Flags.in_debugger || !Flags.in_toplevel -> () + end + | Rel p -> + let (gseen, vseen, ids) = !accu in + if p > n && not (Int.Set.mem p vseen) then + let vseen = Int.Set.add p vseen in + let name = + try Some (List.nth nenv (p - n - 1)) + with Invalid_argument _ | Failure _ -> + (* Unbound index: may happen in debug and actually also + while computing temporary implicit arguments of an + inductive type *) + None + in + let ids = match name with + | Some (Name id) -> Id.Set.add id ids + | _ -> ids + in + accu := (gseen, vseen, ids) + | _ -> Constr.iter_with_binders succ visible_ids n c in - try occur 1 c; false - with Occur -> true - | Not_found -> false (* Happens when a global is not in the env *) + let () = visible_ids 1 c in + let (_, _, ids) = !accu in + ids (* Now, there are different renaming strategies... *) @@ -213,8 +230,9 @@ let visibly_occur_id id (nenv,c) = 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 + let visible = visible_ids env_t in + let bad id = Id.List.mem id avoid || is_constructor id + || Id.Set.mem id visible in next_ident_away_from id bad (* 2- Looks for a fresh name for introduction in goal *) @@ -227,8 +245,8 @@ let next_name_away_in_cases_pattern env_t na avoid = 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 + let id = if Id.List.mem id avoid then restart_subscript id else id in + let bad id = Id.List.mem 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 = @@ -245,16 +263,16 @@ let next_name_away_in_goal na avoid = 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 + let id = if Id.List.mem id avoid then restart_subscript id else id in + let bad id = Id.List.mem 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) + if Id.List.mem id avoid then + next_ident_away_from (restart_subscript id) (fun id -> Id.List.mem id avoid) else id let next_name_away_with_default default na avoid = @@ -275,15 +293,18 @@ let next_name_away_with_default_using_types default na avoid t = 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 + (** FIXME: this is inefficient, but only used in printing *) + let avoid = ref (Id.Set.elements (Context.Named.to_vars (named_context env))) in + let sign = named_context_val env in + let rels = rel_context env in + let env0 = reset_with_named_context sign env in + Context.Rel.fold_outside (fun decl newenv -> - let (na,_,t) = to_tuple decl in - let na = named_hd newenv t na in + let na = named_hd newenv (RelDecl.get_type decl) (RelDecl.get_name decl) in let id = next_name_away na !avoid in avoid := id::!avoid; - push_rel (set_name (Name id) decl) newenv) - env + push_rel (RelDecl.set_name (Name id) decl) newenv) + rels ~init:env0 (* 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, @@ -291,7 +312,8 @@ let make_all_name_different env = 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 + let visible = visible_ids env_t in + let bad id = Id.List.mem id avoid || Id.Set.mem id visible in next_ident_away_from id bad let next_name_away_for_default_printing env_t na avoid = @@ -362,12 +384,12 @@ let rename_bound_vars_as_displayed avoid env c = let na',avoid' = compute_displayed_name_in (RenamingElsewhereFor (env,c2)) avoid na c2 in - mkProd (na', c1, rename avoid' (add_name na' env) c2) + mkProd (na', c1, rename avoid' (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) + mkLetIn (na',c1,t, rename avoid' (na' :: env) c2) | Cast (c,k,t) -> mkCast (rename avoid env c, k,t) | _ -> c in diff --git a/engine/namegen.mli b/engine/namegen.mli index a2923fee99..33ce9a34d0 100644 --- a/engine/namegen.mli +++ b/engine/namegen.mli @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** This file features facilities to generate fresh names. *) + open Names open Term open Environ @@ -52,7 +54,22 @@ val it_mkLambda_or_LetIn_name : env -> constr -> Context.Rel.t -> constr (** 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 *) +(** [next_ident_away original_id unwanted_ids] returns a new identifier as close as possible + to the [original_id] while avoiding all [unwanted_ids]. + + In particular: + {ul {- if [original_id] does not appear in the list of [unwanted_ids], then [original_id] is returned.} + {- if [original_id] appears in the list of [unwanted_ids], + then this function returns a new id that: + {ul {- has the same {i root} as the [original_id],} + {- does not occur in the list of [unwanted_ids],} + {- has the smallest possible {i subscript}.}}}} + + where by {i subscript} of some identifier we mean last part of it that is composed + only from (decimal) digits and by {i root} of some identifier we mean + the whole identifier except for the {i subscript}. + + E.g. if we take [foo42], then [42] is the {i subscript}, and [foo] is the root. *) val next_ident_away : Id.t -> Id.t list -> Id.t (** Avoid clashing with a name already used in current module *) @@ -62,9 +79,6 @@ val next_ident_away_in_goal : Id.t -> Id.t list -> Id.t 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 diff --git a/engine/proofview.ml b/engine/proofview.ml index bcdd4da115..721389af4f 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -22,6 +22,8 @@ open Context.Named.Declaration (** Main state of tactics *) type proofview = Proofview_monad.proofview +(* The first items in pairs below are proofs (under construction). + The second items in the pairs below are statements that are being proved. *) type entry = (Term.constr * Term.types) list (** Returns a stylised view of a proofview for use by, for instance, @@ -152,33 +154,9 @@ let focus i j sp = let (new_comb, context) = focus_sublist i j sp.comb in ( { sp with comb = new_comb } , context ) - -(** [advance sigma g] returns [Some g'] if [g'] is undefined and is - the current avatar of [g] (for instance [g] was changed by [clear] - into [g']). It returns [None] if [g] has been (partially) - solved. *) -(* spiwack: [advance] is probably performance critical, and the good - behaviour of its definition may depend sensitively to the actual - definition of [Evd.find]. Currently, [Evd.find] starts looking for - a value in the heap of undefined variable, which is small. Hence in - the most common case, where [advance] is applied to an unsolved - goal ([advance] is used to figure if a side effect has modified the - goal) it terminates quickly. *) -let rec advance sigma g = - let open Evd in - let evi = Evd.find sigma g in - match evi.evar_body with - | Evar_empty -> Some g - | Evar_defined v -> - if Option.default false (Store.get evi.evar_extra Evarutil.cleared) then - let (e,_) = Term.destEvar v in - advance sigma e - else - None - (** [undefined defs l] is the list of goals in [l] which are still unsolved (after advancing cleared goals). *) -let undefined defs l = CList.map_filter (advance defs) l +let undefined defs l = CList.map_filter (Evarutil.advance defs) l (** Unfocuses a proofview with respect to a context. *) let unfocus c sp = @@ -309,9 +287,9 @@ let tclIFCATCH a s f = let tclONCE = Proof.once exception MoreThanOneSuccess -let _ = Errors.register_handler begin function - | MoreThanOneSuccess -> Errors.error "This tactic has more than one success." - | _ -> raise Errors.Unhandled +let _ = CErrors.register_handler begin function + | MoreThanOneSuccess -> CErrors.error "This tactic has more than one success." + | _ -> raise CErrors.Unhandled end (** [tclEXACTLY_ONCE e t] succeeds as [t] if [t] has exactly one @@ -362,12 +340,13 @@ let set_nosuchgoals_hook f = nosuchgoals_hook := f (* This uses the hook above *) -let _ = Errors.register_handler begin function +let _ = CErrors.register_handler begin function | NoSuchGoals n -> let suffix = !nosuchgoals_hook n in - Errors.errorlabstrm "" - (str "No such " ++ str (String.plural n "goal") ++ str "." ++ suffix) - | _ -> raise Errors.Unhandled + CErrors.user_err + (str "No such " ++ str (String.plural n "goal") ++ str "." ++ + pr_non_empty_arg (fun x -> x) suffix) + | _ -> raise CErrors.Unhandled end (** [tclFOCUS_gen nosuchgoal i j t] applies [t] in a context where @@ -388,6 +367,36 @@ let tclFOCUS_gen nosuchgoal i j t = let tclFOCUS i j t = tclFOCUS_gen (tclZERO (NoSuchGoals (j+1-i))) i j t let tclTRYFOCUS i j t = tclFOCUS_gen (tclUNIT ()) i j t +let tclFOCUSLIST l t = + let open Proof in + Comb.get >>= fun comb -> + let n = CList.length comb in + (* First, remove empty intervals, and bound the intervals to the number + of goals. *) + let sanitize (i, j) = + if i > j then None + else if i > n then None + else if j < 1 then None + else Some ((max i 1), (min j n)) + in + let l = CList.map_filter sanitize l in + match l with + | [] -> tclZERO (NoSuchGoals 0) + | (mi, _) :: _ -> + (* Get the left-most goal to focus. This goal won't move, and we + will then place all the other goals to focus to the right. *) + let mi = CList.fold_left (fun m (i, _) -> min m i) mi l in + (* [CList.goto] returns a zipper, so that + [(rev left) @ sub_right = comb]. *) + let left, sub_right = CList.goto (mi-1) comb in + let p x _ = CList.exists (fun (i, j) -> i <= x + mi && x + mi <= j) l in + let sub, right = CList.partitioni p sub_right in + let mj = mi - 1 + CList.length sub in + Comb.set (CList.rev_append left (sub @ right)) >> + tclFOCUS mi mj t + + + (** Like {!tclFOCUS} but selects a single goal by name. *) let tclFOCUSID id t = let open Proof in @@ -413,15 +422,15 @@ let tclFOCUSID id t = (** {7 Dispatching on goals} *) exception SizeMismatch of int*int -let _ = Errors.register_handler begin function - | SizeMismatch (i,_) -> +let _ = CErrors.register_handler begin function + | SizeMismatch (i,j) -> let open Pp in let errmsg = str"Incorrect number of goals" ++ spc() ++ - str"(expected "++int i++str(String.plural i " tactic") ++ str")." + str"(expected "++int i++str(String.plural i " tactic") ++ str", was given "++ int j++str")." in - Errors.errorlabstrm "" errmsg - | _ -> raise Errors.Unhandled + CErrors.user_err errmsg + | _ -> raise CErrors.Unhandled end (** A variant of [Monad.List.iter] where we iter over the focused list @@ -434,7 +443,7 @@ let iter_goal i = Comb.get >>= fun initial -> Proof.List.fold_left begin fun (subgoals as cur) goal -> Solution.get >>= fun step -> - match advance step goal with + match Evarutil.advance step goal with | None -> return cur | Some goal -> Comb.set [goal] >> @@ -444,6 +453,25 @@ let iter_goal i = Solution.get >>= fun evd -> Comb.set CList.(undefined evd (flatten (rev subgoals))) +(** List iter but allocates a list of results *) +let map_goal i = + let rev = List.rev in (* hem... Proof masks List... *) + let open Proof in + Comb.get >>= fun initial -> + Proof.List.fold_left begin fun (acc, subgoals as cur) goal -> + Solution.get >>= fun step -> + match Evarutil.advance step goal with + | None -> return cur + | Some goal -> + Comb.set [goal] >> + i goal >>= fun res -> + Proof.map (fun comb -> comb :: subgoals) Comb.get >>= fun x -> + return (res :: acc, x) + end ([],[]) initial >>= fun (results_rev, subgoals) -> + Solution.get >>= fun evd -> + Comb.set CList.(undefined evd (flatten (rev subgoals))) >> + return (rev results_rev) + (** A variant of [Monad.List.fold_left2] where the first list is the list of focused goals. The argument tactic is executed in a focus comprising only of the current goal, a goal which has been solved @@ -458,7 +486,7 @@ let fold_left2_goal i s l = in Proof.List.fold_left2 err begin fun ((r,subgoals) as cur) goal a -> Solution.get >>= fun step -> - match advance step goal with + match Evarutil.advance step goal with | None -> return cur | Some goal -> Comb.set [goal] >> @@ -502,7 +530,7 @@ let tclDISPATCHGEN0 join tacs = let open Proof in Pv.get >>= function | { comb=[goal] ; solution } -> - begin match advance solution goal with + begin match Evarutil.advance solution goal with | None -> tclUNIT (join []) | Some _ -> Proof.map (fun res -> join [res]) tac end @@ -576,7 +604,15 @@ let tclINDEPENDENT tac = let tac = InfoL.tag (Info.DBranch) tac in InfoL.tag (Info.Dispatch) (iter_goal (fun _ -> tac)) - +let tclINDEPENDENTL tac = + let open Proof in + Pv.get >>= fun initial -> + match initial.comb with + | [] -> tclUNIT [] + | [_] -> tac >>= fun x -> return [x] + | _ -> + let tac = InfoL.tag (Info.DBranch) tac in + InfoL.tag (Info.Dispatch) (map_goal (fun _ -> tac)) (** {7 Goal manipulation} *) @@ -588,6 +624,13 @@ let shelve = InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve")) >> Shelf.modify (fun gls -> gls @ initial) +let shelve_goals l = + let open Proof in + Comb.get >>= fun initial -> + let comb = CList.filter (fun g -> not (CList.mem g l)) initial in + Comb.set comb >> + InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve_goals")) >> + Shelf.modify (fun gls -> gls @ l) (** [contained_in_info e evi] checks whether the evar [e] appears in the hypotheses, the conclusion or the body of the evar_info @@ -647,6 +690,21 @@ let unshelve l p = let l = undefined p.solution l in { p with comb = p.comb@l } +let mark_in_evm ~goal evd content = + let info = Evd.find evd content in + let info = + if goal then + { info with Evd.evar_source = match info.Evd.evar_source with + | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x + | loc,_ -> loc,Evar_kinds.GoalEvar } + else info + in + let info = match Evd.Store.get info.Evd.evar_extra typeclass_resolvable with + | None -> { info with Evd.evar_extra = Evd.Store.set info.Evd.evar_extra typeclass_resolvable () } + | Some () -> info + in + Evd.add evd content info + let with_shelf tac = let open Proof in Pv.get >>= fun pv -> @@ -659,8 +717,11 @@ let with_shelf tac = let fgoals = Evd.future_goals solution in let pgoal = Evd.principal_future_goal solution in let sigma = Evd.restore_future_goals sigma fgoals pgoal in - Pv.set { npv with shelf; solution = sigma } >> - tclUNIT (CList.rev_append gls' gls, ans) + (* Ensure we mark and return only unsolved goals *) + let gls' = undefined sigma (CList.rev_append gls' gls) in + let sigma = CList.fold_left (mark_in_evm ~goal:false) sigma gls' in + let npv = { npv with shelf; solution = sigma } in + Pv.set npv >> tclUNIT (gls', ans) (** [goodmod p m] computes the representative of [p] modulo [m] in the interval [[0,m-1]].*) @@ -807,12 +868,12 @@ let tclPROGRESS t = if not test then tclUNIT res else - tclZERO (Errors.UserError ("Proofview.tclPROGRESS" , Pp.str"Failed to progress.")) + tclZERO (CErrors.UserError (Some "Proofview.tclPROGRESS" , Pp.str"Failed to progress.")) exception Timeout -let _ = Errors.register_handler begin function - | Timeout -> Errors.errorlabstrm "Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!") - | _ -> Pervasives.raise Errors.Unhandled +let _ = CErrors.register_handler begin function + | Timeout -> CErrors.user_err ~hdr:"Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!") + | _ -> Pervasives.raise CErrors.Unhandled end let tclTIMEOUT n t = @@ -891,6 +952,8 @@ module Unsafe = struct { step with comb = step.comb @ gls } end + let tclSETENV = Env.set + let tclGETGOALS = Comb.get let tclSETGOALS = Comb.set @@ -905,19 +968,12 @@ module Unsafe = struct { p with solution = Evd.reset_future_goals p.solution } let mark_as_goal evd content = - let info = Evd.find evd content in - let info = - { info with Evd.evar_source = match info.Evd.evar_source with - | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x - | loc,_ -> loc,Evar_kinds.GoalEvar } - in - let info = match Evd.Store.get info.Evd.evar_extra typeclass_resolvable with - | None -> { info with Evd.evar_extra = Evd.Store.set info.Evd.evar_extra typeclass_resolvable () } - | Some () -> info - in - Evd.add evd content info + mark_in_evm ~goal:true evd content + + let advance = Evarutil.advance - let advance = advance + let mark_as_unresolvable p gl = + { p with solution = mark_in_evm ~goal:false p.solution gl } let typeclass_resolvable = typeclass_resolvable @@ -946,7 +1002,7 @@ let goal_extra evars gl = let catchable_exception = function | Logic_monad.Exception _ -> false - | e -> Errors.noncritical e + | e -> CErrors.noncritical e module Goal = struct @@ -992,7 +1048,7 @@ module Goal = struct let (gl, sigma) = nf_gmake env sigma goal in tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) (f.enter gl)) with e when catchable_exception e -> - let (e, info) = Errors.push e in + let (e, info) = CErrors.push e in tclZERO ~info e end end @@ -1015,11 +1071,31 @@ module Goal = struct tclEVARMAP >>= fun sigma -> try f (gmake env sigma goal) with e when catchable_exception e -> - let (e, info) = Errors.push e in + let (e, info) = CErrors.push e in tclZERO ~info e end end + exception NotExactlyOneSubgoal + let _ = CErrors.register_handler begin function + | NotExactlyOneSubgoal -> + CErrors.user_err (Pp.str"Not exactly one subgoal.") + | _ -> raise CErrors.Unhandled + end + + let enter_one f = + let open Proof in + Comb.get >>= function + | [goal] -> begin + Env.get >>= fun env -> + tclEVARMAP >>= fun sigma -> + try f.enter (gmake env sigma goal) + with e when catchable_exception e -> + let (e, info) = CErrors.push e in + tclZERO ~info e + end + | _ -> tclZERO NotExactlyOneSubgoal + type ('a, 'b) s_enter = { s_enter : 'r. ('a, 'r) t -> ('b, 'r) Sigma.sigma } @@ -1034,7 +1110,7 @@ module Goal = struct let sigma = Sigma.to_evar_map sigma in tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) tac) with e when catchable_exception e -> - let (e, info) = Errors.push e in + let (e, info) = CErrors.push e in tclZERO ~info e end end @@ -1050,7 +1126,7 @@ module Goal = struct let sigma = Sigma.to_evar_map sigma in tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) tac) with e when catchable_exception e -> - let (e, info) = Errors.push e in + let (e, info) = CErrors.push e in tclZERO ~info e end end @@ -1059,7 +1135,7 @@ module Goal = struct Pv.get >>= fun step -> let sigma = step.solution in let map goal = - match advance sigma goal with + match Evarutil.advance sigma goal with | None -> None (** ppedrot: Is this check really necessary? *) | Some goal -> let gl = @@ -1071,6 +1147,10 @@ module Goal = struct in tclUNIT (CList.map_filter map step.comb) + let unsolved { self=self } = + tclEVARMAP >>= fun sigma -> + tclUNIT (not (Option.is_empty (Evarutil.advance sigma self))) + (* compatibility *) let goal { self=self } = self @@ -1106,10 +1186,6 @@ let tclLIFT = Proof.lift let tclCHECKINTERRUPT = tclLIFT (NonLogical.make Control.check_for_interrupt) - - - - (*** Compatibility layer with <= 8.2 tactics ***) module V82 = struct type tac = Evar.t Evd.sigma -> Evar.t list Evd.sigma @@ -1138,7 +1214,7 @@ module V82 = struct InfoL.leaf (Info.Tactic (fun () -> Pp.str"<unknown>")) >> Pv.set { ps with solution = evd; comb = sgs; } with e when catchable_exception e -> - let (e, info) = Errors.push e in + let (e, info) = CErrors.push e in tclZERO ~info e @@ -1183,7 +1259,7 @@ module V82 = struct let (_,final,_,_) = apply (goal_env gls.Evd.sigma gls.Evd.it) t init in { Evd.sigma = final.solution ; it = final.comb } with Logic_monad.TacticFailure e as src -> - let (_, info) = Errors.push src in + let (_, info) = CErrors.push src in iraise (e, info) let put_status = Status.put @@ -1193,7 +1269,7 @@ module V82 = struct let wrap_exceptions f = try f () with e when catchable_exception e -> - let (e, info) = Errors.push e in tclZERO ~info e + let (e, info) = CErrors.push e in tclZERO ~info e end diff --git a/engine/proofview.mli b/engine/proofview.mli index 7996b7969c..294b03dca2 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -63,7 +63,7 @@ val dependent_init : telescope -> entry * proofview (** [finished pv] is [true] if and only if [pv] is complete. That is, if it has an empty list of focused goals. There could still be - unsolved subgoaled, but they would then be out of focus. *) + unsolved subgoals, but they would then be out of focus. *) val finished : proofview -> bool (** Returns the current [evar] state. *) @@ -239,6 +239,16 @@ val set_nosuchgoals_hook: (int -> Pp.std_ppcmds) -> unit val tclFOCUS : int -> int -> 'a tactic -> 'a tactic +(** [tclFOCUSLIST li t] applies [t] on the list of focused goals + described by [li]. Each element of [li] is a pair [(i, j)] denoting + the goals numbered from [i] to [j] (inclusive, starting from 1). + It will try to apply [t] to all the valid goals in any of these + intervals. If the set of such goals is not a single range, then it + will move goals such that it is a single range. (So, for + instance, [[1, 3-5]; idtac.] is not the identity.) + If the set of such goals is empty, it will fail. *) +val tclFOCUSLIST : (int * int) list -> 'a tactic -> 'a tactic + (** [tclFOCUSID x t] applies [t] on a (single) focused goal like {!tclFOCUS}. The goal is found by its name rather than its number.*) @@ -282,6 +292,7 @@ val tclEXTEND : unit tactic list -> unit tactic -> unit tactic list -> unit tact independent of backtracking in another. It is equivalent to [tclEXTEND [] tac []]. *) val tclINDEPENDENT : unit tactic -> unit tactic +val tclINDEPENDENTL: 'a tactic -> 'a list tactic (** {7 Goal manipulation} *) @@ -290,6 +301,16 @@ val tclINDEPENDENT : unit tactic -> unit tactic shelf for later use (or being solved by side-effects). *) val shelve : unit tactic +(** Shelves the given list of goals, which might include some that are + under focus and some that aren't. All the goals are placed on the + shelf for later use (or being solved by side-effects). *) +val shelve_goals : Goal.goal list -> unit tactic + +(** [unifiable sigma g l] checks whether [g] appears in another + subgoal of [l]. The list [l] may contain [g], but it does not + affect the result. Used by [shelve_unifiable]. *) +val unifiable : Evd.evar_map -> Goal.goal -> Goal.goal list -> bool + (** Shelves the unifiable goals under focus, i.e. the goals which appear in other goals under focus (the unfocused goals are not considered). *) @@ -303,8 +324,12 @@ val guard_no_unifiable : Names.Name.t list option tactic goals of p *) val unshelve : Goal.goal list -> proofview -> proofview -(** [with_shelf tac] executes [tac] and returns its result together with the set - of goals shelved by [tac]. The current shelf is unchanged. *) +(** [depends_on g1 g2 sigma] checks if g1 occurs in the type/ctx of g2 *) +val depends_on : Evd.evar_map -> Goal.goal -> Goal.goal -> bool + +(** [with_shelf tac] executes [tac] and returns its result together with + the set of goals shelved by [tac]. The current shelf is unchanged + and the returned list contains only unsolved goals. *) val with_shelf : 'a tactic -> (Goal.goal list * 'a) tactic (** If [n] is positive, [cycle n] puts the [n] first goal last. If [n] @@ -349,7 +374,6 @@ val mark_as_unsafe : unit tactic with given up goals cannot be closed. *) val give_up : unit tactic - (** {7 Control primitives} *) (** [tclPROGRESS t] checks the state of the proof after [t]. It it is @@ -386,6 +410,9 @@ module Unsafe : sig (** Like {!tclEVARS} but also checks whether goals have been solved. *) val tclEVARSADVANCE : Evd.evar_map -> unit tactic + (** Set the global environment of the tactic *) + val tclSETENV : Environ.env -> unit tactic + (** [tclNEWGOALS gls] adds the goals [gls] to the ones currently being proved, appending them to the list of focused goals. If a goal is already solved, it is not added. *) @@ -408,6 +435,9 @@ module Unsafe : sig and makes it unresolvable for type classes. *) val mark_as_goal : Evd.evar_map -> Evar.t -> Evd.evar_map + (** Make an evar unresolvable for type classes. *) + val mark_as_unresolvable : proofview -> Evar.t -> proofview + (** [advance sigma g] returns [Some g'] if [g'] is undefined and is the current avatar of [g] (for instance [g] was changed by [clear] into [g']). It returns [None] if [g] has been (partially) @@ -476,6 +506,10 @@ module Goal : sig (** Like {!nf_enter}, but does not normalize the goal beforehand. *) val enter : ([ `LZ ], unit tactic) enter -> unit tactic + (** Like {!enter}, but assumes exactly one goal under focus, raising *) + (** an error otherwise. *) + val enter_one : ([ `LZ ], 'a tactic) enter -> 'a tactic + type ('a, 'b) s_enter = { s_enter : 'r. ('a, 'r) t -> ('b, 'r) Sigma.sigma } @@ -491,6 +525,10 @@ module Goal : sig FIXME: encapsulate the level in an existential type. *) val goals : ([ `LZ ], 'r) t tactic list tactic + (** [unsolved g] is [true] if [g] is still unsolved in the current + proof state. *) + val unsolved : ('a, 'r) t -> bool tactic + (** Compatibility: avoid if possible *) val goal : ([ `NF ], 'r) t -> Evar.t diff --git a/engine/proofview_monad.mli b/engine/proofview_monad.mli index 0aff0a7207..637414cce7 100644 --- a/engine/proofview_monad.mli +++ b/engine/proofview_monad.mli @@ -7,7 +7,8 @@ (************************************************************************) (** This file defines the datatypes used as internal states by the - tactic monad, and specialises the [Logic_monad] to these type. *) + tactic monad, and specialises the [Logic_monad] to these types. It should + not be used directly. Consider using {!Proofview} instead. *) (** {6 Traces} *) diff --git a/engine/sigma.ml b/engine/sigma.ml index c7b0bb5a50..9381a33af1 100644 --- a/engine/sigma.ml +++ b/engine/sigma.ml @@ -36,16 +36,16 @@ let new_evar sigma ?naming info = let define evk c sigma = Sigma ((), Evd.define evk c sigma, ()) -let new_univ_level_variable ?loc ?name ?predicative rigid sigma = - let (sigma, u) = Evd.new_univ_level_variable ?loc ?name ?predicative rigid sigma in +let new_univ_level_variable ?loc ?name rigid sigma = + let (sigma, u) = Evd.new_univ_level_variable ?loc ?name rigid sigma in Sigma (u, sigma, ()) -let new_univ_variable ?loc ?name ?predicative rigid sigma = - let (sigma, u) = Evd.new_univ_variable ?loc ?name ?predicative rigid sigma in +let new_univ_variable ?loc ?name rigid sigma = + let (sigma, u) = Evd.new_univ_variable ?loc ?name rigid sigma in Sigma (u, sigma, ()) -let new_sort_variable ?loc ?name ?predicative rigid sigma = - let (sigma, u) = Evd.new_sort_variable ?loc ?name ?predicative rigid sigma in +let new_sort_variable ?loc ?name rigid sigma = + let (sigma, u) = Evd.new_sort_variable ?loc ?name rigid sigma in Sigma (u, sigma, ()) let fresh_sort_in_family ?loc ?rigid env sigma s = diff --git a/engine/sigma.mli b/engine/sigma.mli index 643bea4036..7473a251b7 100644 --- a/engine/sigma.mli +++ b/engine/sigma.mli @@ -12,7 +12,9 @@ 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. + and in particular statically suppress evar leaks and the like. To this + ends, it defines a type of indexed evarmaps whose phantom typing ensures + monotonous use. *) (** {5 Stages} *) @@ -32,7 +34,7 @@ val (+>) : ('a, 'b) le -> ('b, 'c) le -> ('a, 'c) le (** {5 Monotonous evarmaps} *) type 'r t -(** Stage-indexed evarmaps. *) +(** Stage-indexed evarmaps. This is just a plain evarmap with a phantom type. *) type ('a, 'r) sigma = Sigma : 'a * 's t * ('r, 's) le -> ('a, 'r) sigma (** Return values at a later stage *) @@ -66,11 +68,11 @@ val define : 'r evar -> Constr.t -> 'r t -> (unit, 'r) sigma (** Polymorphic universes *) -val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> +val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> Evd.rigid -> 'r t -> (Univ.universe_level, 'r) sigma -val new_univ_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> +val new_univ_variable : ?loc:Loc.t -> ?name:string -> Evd.rigid -> 'r t -> (Univ.universe, 'r) sigma -val new_sort_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> +val new_sort_variable : ?loc:Loc.t -> ?name:string -> Evd.rigid -> 'r t -> (Sorts.t, 'r) sigma val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:Evd.rigid -> Environ.env -> diff --git a/engine/termops.ml b/engine/termops.ml index f698f81513..2f4c5e2049 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Names open Nameops @@ -17,6 +17,7 @@ open Environ module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration +module CompactedDecl = Context.Compacted.Declaration (* Sorts and sort family *) @@ -100,6 +101,7 @@ 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 () = Hook.set Evd.print_constr_hook (fun env c -> !term_printer env c) let pr_var_decl env decl = let open NamedDecl in @@ -564,7 +566,14 @@ let occur_var_in_decl env hyp decl = occur_var env hyp typ || occur_var env hyp body -(* returns the list of free debruijn indices in a term *) +let local_occur_var id c = + let rec occur c = match kind_of_term c with + | Var id' -> if Id.equal id id' then raise Occur + | _ -> Constr.iter occur c + in + try occur c; false with Occur -> true + + (* 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 @@ -592,11 +601,18 @@ let collect_vars c = | _ -> fold_constr aux vars c in aux Id.Set.empty c +let vars_of_global_reference env gr = + let c, _ = Universes.unsafe_constr_of_global gr in + vars_of_global (Global.env ()) 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 eqc x y = + if univs then not (Option.is_empty (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 @@ -662,6 +678,21 @@ let rec subst_meta bl c = | Meta i -> (try Int.List.assoc i bl with Not_found -> c) | _ -> map_constr (subst_meta bl) c +let rec strip_outer_cast c = match kind_of_term c with + | Cast (c,_,_) -> strip_outer_cast c + | _ -> c + +(* flattens application lists throwing casts in-between *) +let collapse_appl c = match kind_of_term c with + | App (f,cl) -> + let rec collapse_rec f cl2 = + match kind_of_term (strip_outer_cast f) with + | App (g,cl1) -> collapse_rec g (Array.append cl1 cl2) + | _ -> mkApp (f,cl2) + in + collapse_rec f cl + | _ -> c + (* First utilities for avoiding telescope computation for subst_term *) let prefix_application eq_fun (k,c) (t : constr) = @@ -968,24 +999,30 @@ let smash_rel_context sign = let fold_named_context_both_sides f l ~init = List.fold_right_and_left f l init -let rec mem_named_context id ctxt = - match ctxt with - | decl :: _ when Id.equal id (NamedDecl.get_id decl) -> true - | _ :: sign -> mem_named_context id sign - | [] -> false +let mem_named_context_val id ctxt = + try ignore(Environ.lookup_named_val id ctxt); true with Not_found -> false -let compact_named_context_reverse sign = +let compact_named_context sign = let compact l decl = - let (i1,c1,t1) = NamedDecl.to_tuple decl in - 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.Named.fold_inside compact ~init:[] sign - -let compact_named_context sign = List.rev (compact_named_context_reverse sign) + match decl, l with + | NamedDecl.LocalAssum (i,t), [] -> + [CompactedDecl.LocalAssum ([i],t)] + | NamedDecl.LocalDef (i,c,t), [] -> + [CompactedDecl.LocalDef ([i],c,t)] + | NamedDecl.LocalAssum (i1,t1), CompactedDecl.LocalAssum (li,t2) :: q -> + if Constr.equal t1 t2 + then CompactedDecl.LocalAssum (i1::li, t2) :: q + else CompactedDecl.LocalAssum ([i1],t1) :: CompactedDecl.LocalAssum (li,t2) :: q + | NamedDecl.LocalDef (i1,c1,t1), CompactedDecl.LocalDef (li,c2,t2) :: q -> + if Constr.equal c1 c2 && Constr.equal t1 t2 + then CompactedDecl.LocalDef (i1::li, c2, t2) :: q + else CompactedDecl.LocalDef ([i1],c1,t1) :: CompactedDecl.LocalDef (li,c2,t2) :: q + | NamedDecl.LocalAssum (i,t), q -> + CompactedDecl.LocalAssum ([i],t) :: q + | NamedDecl.LocalDef (i,c,t), q -> + CompactedDecl.LocalDef ([i],c,t) :: q + in + sign |> Context.Named.fold_inside compact ~init:[] |> List.rev let clear_named_body id env = let open NamedDecl in diff --git a/engine/termops.mli b/engine/termops.mli index c2a4f33235..78826f79ae 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -6,6 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** This file defines various utilities for term manipulation that are not + needed in the kernel. *) + open Pp open Names open Term @@ -93,6 +96,7 @@ 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 @@ -102,6 +106,10 @@ val occur_var : env -> Id.t -> types -> bool val occur_var_in_decl : env -> Id.t -> Context.Named.Declaration.t -> bool + +(** As {!occur_var} but assume the identifier not to be a section variable *) +val local_occur_var : Id.t -> types -> bool + val free_rels : constr -> Int.Set.t (** [dependent m t] tests whether [m] is a subterm of [t] *) @@ -113,6 +121,7 @@ val dependent_in_decl : constr -> Context.Named.Declaration.t -> 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 vars_of_global_reference : env -> Globnames.global_reference -> Id.Set.t val occur_term : constr -> constr -> bool (** Synonymous of dependent Substitution of metavariables *) @@ -155,6 +164,13 @@ val eq_constr : constr -> constr -> bool (* FIXME rename: erases universes*) val eta_reduce_head : constr -> constr +(** Flattens application lists *) +val collapse_appl : constr -> constr + +(** Remove recursively the casts around a term i.e. + [strip_outer_cast (Cast (Cast ... (Cast c, t) ... ))] is [c]. *) +val strip_outer_cast : constr -> constr + exception CannotFilter (** Lightweight first-order filtering procedure. Unification @@ -229,9 +245,8 @@ val map_rel_context_with_binders : val fold_named_context_both_sides : ('a -> Context.Named.Declaration.t -> Context.Named.Declaration.t list -> 'a) -> Context.Named.t -> init:'a -> 'a -val mem_named_context : Id.t -> Context.Named.t -> bool -val compact_named_context : Context.Named.t -> Context.NamedList.t -val compact_named_context_reverse : Context.Named.t -> Context.NamedList.t +val mem_named_context_val : Id.t -> named_context_val -> bool +val compact_named_context : Context.Named.t -> Context.Compacted.t val clear_named_body : Id.t -> env -> env diff --git a/engine/uState.ml b/engine/uState.ml index 8aa9a61ab9..c66af02bb9 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Names @@ -49,7 +49,7 @@ let empty = uctx_univ_variables = Univ.LMap.empty; uctx_univ_algebraic = Univ.LSet.empty; uctx_universes = UGraph.initial_universes; - uctx_initial_universes = UGraph.initial_universes } + uctx_initial_universes = UGraph.initial_universes; } let make u = { empty with @@ -83,7 +83,7 @@ let union ctx ctx' = 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) } + UGraph.merge_constraints cstrsr (declarenew ctx.uctx_universes) } let context_set ctx = ctx.uctx_local @@ -255,21 +255,25 @@ let universe_context ?names ctx = 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.") + user_err ~loc ~hdr:"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 let loc = - let get_loc u = try (Univ.LMap.find u (snd ctx.uctx_names)).uloc with Not_found -> None in - try List.find_map get_loc (Univ.LSet.elements left) with Not_found -> Loc.ghost + try + let info = + Univ.LMap.find (Univ.LSet.choose left) (snd ctx.uctx_names) in + Option.default Loc.ghost info.uloc + with Not_found -> Loc.ghost in - user_err_loc (loc, "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.")) + user_err ~loc ~hdr:"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, @@ -329,7 +333,8 @@ let merge ?loc sideff rigid uctx ctx' = 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_names; uctx_local; uctx_universes; uctx_initial_universes = initial } + { uctx with uctx_names; 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 } diff --git a/engine/uState.mli b/engine/uState.mli index c5c454020c..0cdc6277a5 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -6,7 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** Universe unification states *) +(** This file defines universe unification states which are part of evarmaps. + Most of the API below is reexported in {!Evd}. Consider using higher-level + primitives when needed. *) open Names diff --git a/engine/universes.ml b/engine/universes.ml new file mode 100644 index 0000000000..6720fcef8f --- /dev/null +++ b/engine/universes.ml @@ -0,0 +1,1131 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Util +open Pp +open Names +open Term +open Environ +open Univ +open Globnames +open Decl_kinds + +let pr_with_global_universes l = + try Nameops.pr_id (LMap.find l (snd (Global.global_universe_names ()))) + with Not_found -> Level.pr l + +(** Local universe names of polymorphic references *) + +type universe_binders = (Id.t * Univ.universe_level) list + +let universe_binders_table = Summary.ref Refmap.empty ~name:"universe binders" + +let universe_binders_of_global ref = + try + let l = Refmap.find ref !universe_binders_table in l + with Not_found -> [] + +let register_universe_binders ref l = + universe_binders_table := Refmap.add ref l !universe_binders_table + +(* To disallow minimization to Set *) + +let set_minimization = ref true +let is_set_minimization () = !set_minimization + +type universe_constraint_type = ULe | UEq | ULub + +type universe_constraint = universe * universe_constraint_type * universe + +module Constraints = struct + module S = Set.Make( + struct + type t = universe_constraint + + let compare_type c c' = + match c, c' with + | ULe, ULe -> 0 + | ULe, _ -> -1 + | _, ULe -> 1 + | UEq, UEq -> 0 + | UEq, _ -> -1 + | ULub, ULub -> 0 + | ULub, _ -> 1 + + let compare (u,c,v) (u',c',v') = + let i = compare_type c c' in + if Int.equal i 0 then + let i' = Universe.compare u u' in + if Int.equal i' 0 then Universe.compare v v' + else + if c != ULe && Universe.compare u v' = 0 && Universe.compare v u' = 0 then 0 + else i' + else i + end) + + include S + + let add (l,d,r as cst) s = + if Universe.equal l r then s + else add cst s + + let tr_dir = function + | ULe -> Le + | UEq -> Eq + | ULub -> Eq + + let op_str = function ULe -> " <= " | UEq -> " = " | ULub -> " /\\ " + + let pr c = + fold (fun (u1,op,u2) pp_std -> + pp_std ++ Universe.pr u1 ++ str (op_str op) ++ + Universe.pr u2 ++ fnl ()) c (str "") + + let equal x y = + x == y || equal x y + +end + +type universe_constraints = Constraints.t +type 'a constraint_accumulator = universe_constraints -> 'a -> 'a option +type 'a universe_constrained = 'a * universe_constraints + +type 'a universe_constraint_function = 'a -> 'a -> universe_constraints -> universe_constraints + +let enforce_eq_instances_univs strict x y c = + let d = if strict then ULub else UEq in + let ax = Instance.to_array x and ay = Instance.to_array y in + if Array.length ax != Array.length ay then + CErrors.anomaly (Pp.str "Invalid argument: enforce_eq_instances_univs called with" ++ + Pp.str " instances of different lengths"); + CArray.fold_right2 + (fun x y -> Constraints.add (Universe.make x, d, Universe.make y)) + ax ay c + +let subst_univs_universe_constraint fn (u,d,v) = + let u' = subst_univs_universe fn u and v' = subst_univs_universe fn v in + if Universe.equal u' v' then None + else Some (u',d,v') + +let subst_univs_universe_constraints subst csts = + Constraints.fold + (fun c -> Option.fold_right Constraints.add (subst_univs_universe_constraint subst c)) + csts Constraints.empty + + +let to_constraints g s = + let tr (x,d,y) acc = + let add l d l' acc = Constraint.add (l,Constraints.tr_dir d,l') acc in + match Universe.level x, d, Universe.level y with + | Some l, (ULe | UEq | ULub), Some l' -> add l d l' acc + | _, ULe, Some l' -> enforce_leq x y acc + | _, ULub, _ -> acc + | _, d, _ -> + let f = if d == ULe then UGraph.check_leq else UGraph.check_eq in + if f g x y then acc else + raise (Invalid_argument + "to_constraints: non-trivial algebraic constraint between universes") + in Constraints.fold tr s Constraint.empty + +let test_constr_univs_infer leq univs fold m n accu = + if m == n then Some accu + else + let cstrs = ref accu in + let eq_universes strict l l' = UGraph.check_eq_instances univs l l' in + let eq_sorts s1 s2 = + if Sorts.equal s1 s2 then true + else + let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in + match fold (Constraints.singleton (u1, UEq, u2)) !cstrs with + | None -> false + | Some accu -> cstrs := accu; true + in + let leq_sorts s1 s2 = + if Sorts.equal s1 s2 then true + else + let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in + match fold (Constraints.singleton (u1, ULe, u2)) !cstrs with + | None -> false + | Some accu -> cstrs := accu; true + in + let rec eq_constr' m n = + m == n || Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n + in + let res = + if leq then + let rec compare_leq m n = + Constr.compare_head_gen_leq eq_universes leq_sorts + eq_constr' leq_constr' m n + and leq_constr' m n = m == n || compare_leq m n in + compare_leq m n + else Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n + in + if res then Some !cstrs else None + +let eq_constr_univs_infer univs fold m n accu = + test_constr_univs_infer false univs fold m n accu + +let leq_constr_univs_infer univs fold m n accu = + test_constr_univs_infer true univs fold m n accu + +(** Variant of [eq_constr_univs_infer] taking kind-of-term functions, + to expose subterms of [m] and [n], arguments. *) +let eq_constr_univs_infer_with kind1 kind2 univs fold m n accu = + (* spiwack: duplicates the code of [eq_constr_univs_infer] because I + haven't find a way to factor the code without destroying + pointer-equality optimisations in [eq_constr_univs_infer]. + Pointer equality is not sufficient to ensure equality up to + [kind1,kind2], because [kind1] and [kind2] may be different, + typically evaluating [m] and [n] in different evar maps. *) + let cstrs = ref accu in + let eq_universes strict = UGraph.check_eq_instances univs in + let eq_sorts s1 s2 = + if Sorts.equal s1 s2 then true + else + let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in + match fold (Constraints.singleton (u1, UEq, u2)) !cstrs with + | None -> false + | Some accu -> cstrs := accu; true + in + let rec eq_constr' m n = + Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' m n + in + let res = Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' m n in + if res then Some !cstrs else None + +let test_constr_universes leq m n = + if m == n then Some Constraints.empty + else + let cstrs = ref Constraints.empty in + let eq_universes strict l l' = + cstrs := enforce_eq_instances_univs strict l l' !cstrs; true in + let eq_sorts s1 s2 = + if Sorts.equal s1 s2 then true + else (cstrs := Constraints.add + (Sorts.univ_of_sort s1,UEq,Sorts.univ_of_sort s2) !cstrs; + true) + in + let leq_sorts s1 s2 = + if Sorts.equal s1 s2 then true + else + (cstrs := Constraints.add + (Sorts.univ_of_sort s1,ULe,Sorts.univ_of_sort s2) !cstrs; + true) + in + let rec eq_constr' m n = + m == n || Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n + in + let res = + if leq then + let rec compare_leq m n = + Constr.compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' m n + and leq_constr' m n = m == n || compare_leq m n in + compare_leq m n + else + Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n + in + if res then Some !cstrs else None + +let eq_constr_universes m n = test_constr_universes false m n +let leq_constr_universes m n = test_constr_universes true m n + +let compare_head_gen_proj env equ eqs eqc' m n = + match kind_of_term m, kind_of_term n with + | Proj (p, c), App (f, args) + | App (f, args), Proj (p, c) -> + (match kind_of_term f with + | Const (p', u) when eq_constant (Projection.constant p) p' -> + let pb = Environ.lookup_projection p env in + let npars = pb.Declarations.proj_npars in + if Array.length args == npars + 1 then + eqc' c args.(npars) + else false + | _ -> false) + | _ -> Constr.compare_head_gen equ eqs eqc' m n + +let eq_constr_universes_proj env m n = + if m == n then true, Constraints.empty + else + let cstrs = ref Constraints.empty in + let eq_universes strict l l' = + cstrs := enforce_eq_instances_univs strict l l' !cstrs; true in + let eq_sorts s1 s2 = + if Sorts.equal s1 s2 then true + else + (cstrs := Constraints.add + (Sorts.univ_of_sort s1, UEq, Sorts.univ_of_sort s2) !cstrs; + true) + in + let rec eq_constr' m n = + m == n || compare_head_gen_proj env eq_universes eq_sorts eq_constr' m n + in + let res = eq_constr' m n in + res, !cstrs + +(* Generator of levels *) +let new_univ_level, set_remote_new_univ_level = + RemoteCounter.new_counter ~name:"Universes" 0 ~incr:((+) 1) + ~build:(fun n -> Univ.Level.make (Global.current_dirpath ()) n) + +let new_univ_level _ = new_univ_level () + (* Univ.Level.make db (new_univ_level ()) *) + +let fresh_level () = new_univ_level (Global.current_dirpath ()) + +(* TODO: remove *) +let new_univ dp = Univ.Universe.make (new_univ_level dp) +let new_Type dp = mkType (new_univ dp) +let new_Type_sort dp = Type (new_univ dp) + +let fresh_universe_instance ctx = + Instance.subst_fn (fun _ -> new_univ_level (Global.current_dirpath ())) + (UContext.instance ctx) + +let fresh_instance_from_context ctx = + let inst = fresh_universe_instance ctx in + let constraints = instantiate_univ_constraints inst ctx in + inst, constraints + +let fresh_instance ctx = + let ctx' = ref LSet.empty in + let inst = + Instance.subst_fn (fun v -> + let u = new_univ_level (Global.current_dirpath ()) in + ctx' := LSet.add u !ctx'; u) + (UContext.instance ctx) + in !ctx', inst + +let existing_instance ctx inst = + let () = + let a1 = Instance.to_array inst + and a2 = Instance.to_array (UContext.instance ctx) in + let len1 = Array.length a1 and len2 = Array.length a2 in + if not (len1 == len2) then + CErrors.user_err ~hdr:"Universes" + (str "Polymorphic constant expected " ++ int len2 ++ + str" levels but was given " ++ int len1) + else () + in LSet.empty, inst + +let fresh_instance_from ctx inst = + let ctx', inst = + match inst with + | Some inst -> existing_instance ctx inst + | None -> fresh_instance ctx + in + let constraints = instantiate_univ_constraints inst ctx in + inst, (ctx', constraints) + +let unsafe_instance_from ctx = + (Univ.UContext.instance ctx, ctx) + +(** Fresh universe polymorphic construction *) + +let fresh_constant_instance env c inst = + let cb = lookup_constant c env in + if cb.Declarations.const_polymorphic then + let inst, ctx = + fresh_instance_from + (Declareops.universes_of_constant (Environ.opaque_tables env) cb) inst + in + ((c, inst), ctx) + else ((c,Instance.empty), ContextSet.empty) + +let fresh_inductive_instance env ind inst = + let mib, mip = Inductive.lookup_mind_specif env ind in + if mib.Declarations.mind_polymorphic then + let inst, ctx = fresh_instance_from mib.Declarations.mind_universes inst in + ((ind,inst), ctx) + else ((ind,Instance.empty), ContextSet.empty) + +let fresh_constructor_instance env (ind,i) inst = + let mib, mip = Inductive.lookup_mind_specif env ind in + if mib.Declarations.mind_polymorphic then + let inst, ctx = fresh_instance_from mib.Declarations.mind_universes inst in + (((ind,i),inst), ctx) + else (((ind,i),Instance.empty), ContextSet.empty) + +let unsafe_constant_instance env c = + let cb = lookup_constant c env in + if cb.Declarations.const_polymorphic then + let inst, ctx = unsafe_instance_from + (Declareops.universes_of_constant (Environ.opaque_tables env) cb) in + ((c, inst), ctx) + else ((c,Instance.empty), UContext.empty) + +let unsafe_inductive_instance env ind = + let mib, mip = Inductive.lookup_mind_specif env ind in + if mib.Declarations.mind_polymorphic then + let inst, ctx = unsafe_instance_from mib.Declarations.mind_universes in + ((ind,inst), ctx) + else ((ind,Instance.empty), UContext.empty) + +let unsafe_constructor_instance env (ind,i) = + let mib, mip = Inductive.lookup_mind_specif env ind in + if mib.Declarations.mind_polymorphic then + let inst, ctx = unsafe_instance_from mib.Declarations.mind_universes in + (((ind,i),inst), ctx) + else (((ind,i),Instance.empty), UContext.empty) + +open Globnames + +let fresh_global_instance ?names env gr = + match gr with + | VarRef id -> mkVar id, ContextSet.empty + | ConstRef sp -> + let c, ctx = fresh_constant_instance env sp names in + mkConstU c, ctx + | ConstructRef sp -> + let c, ctx = fresh_constructor_instance env sp names in + mkConstructU c, ctx + | IndRef sp -> + let c, ctx = fresh_inductive_instance env sp names in + mkIndU c, ctx + +let fresh_constant_instance env sp = + fresh_constant_instance env sp None + +let fresh_inductive_instance env sp = + fresh_inductive_instance env sp None + +let fresh_constructor_instance env sp = + fresh_constructor_instance env sp None + +let unsafe_global_instance env gr = + match gr with + | VarRef id -> mkVar id, UContext.empty + | ConstRef sp -> + let c, ctx = unsafe_constant_instance env sp in + mkConstU c, ctx + | ConstructRef sp -> + let c, ctx = unsafe_constructor_instance env sp in + mkConstructU c, ctx + | IndRef sp -> + let c, ctx = unsafe_inductive_instance env sp in + mkIndU c, ctx + +let constr_of_global gr = + let c, ctx = fresh_global_instance (Global.env ()) gr in + if not (Univ.ContextSet.is_empty ctx) then + if Univ.LSet.is_empty (Univ.ContextSet.levels ctx) then + (* Should be an error as we might forget constraints, allow for now + to make firstorder work with "using" clauses *) + c + else raise (Invalid_argument + ("constr_of_global: globalization of polymorphic reference " ^ + Pp.string_of_ppcmds (Nametab.pr_global_env Id.Set.empty gr) ^ + " would forget universes.")) + else c + +let constr_of_reference = constr_of_global + +let unsafe_constr_of_global gr = + unsafe_global_instance (Global.env ()) gr + +let constr_of_global_univ (gr,u) = + match gr with + | VarRef id -> mkVar id + | ConstRef sp -> mkConstU (sp,u) + | ConstructRef sp -> mkConstructU (sp,u) + | IndRef sp -> mkIndU (sp,u) + +let fresh_global_or_constr_instance env = function + | IsConstr c -> c, ContextSet.empty + | IsGlobal gr -> fresh_global_instance env gr + +let global_of_constr c = + match kind_of_term c with + | Const (c, u) -> ConstRef c, u + | Ind (i, u) -> IndRef i, u + | Construct (c, u) -> ConstructRef c, u + | Var id -> VarRef id, Instance.empty + | _ -> raise Not_found + +let global_app_of_constr c = + match kind_of_term c with + | Const (c, u) -> (ConstRef c, u), None + | Ind (i, u) -> (IndRef i, u), None + | Construct (c, u) -> (ConstructRef c, u), None + | Var id -> (VarRef id, Instance.empty), None + | Proj (p, c) -> (ConstRef (Projection.constant p), Instance.empty), Some c + | _ -> raise Not_found + +open Declarations + +let type_of_reference env r = + match r with + | VarRef id -> Environ.named_type id env, ContextSet.empty + | ConstRef c -> + let cb = Environ.lookup_constant c env in + let ty = Typeops.type_of_constant_type env cb.const_type in + if cb.const_polymorphic then + let inst, ctx = fresh_instance_from (Declareops.universes_of_constant (Environ.opaque_tables env) cb) None in + Vars.subst_instance_constr inst ty, ctx + else ty, ContextSet.empty + + | IndRef ind -> + let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in + if mib.mind_polymorphic then + let inst, ctx = fresh_instance_from mib.mind_universes None in + let ty = Inductive.type_of_inductive env (specif, inst) in + ty, ctx + else + let ty = Inductive.type_of_inductive env (specif, Univ.Instance.empty) in + ty, ContextSet.empty + | ConstructRef cstr -> + let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in + if mib.mind_polymorphic then + let inst, ctx = fresh_instance_from mib.mind_universes None in + Inductive.type_of_constructor (cstr,inst) specif, ctx + else Inductive.type_of_constructor (cstr,Instance.empty) specif, ContextSet.empty + +let type_of_global t = type_of_reference (Global.env ()) t + +let unsafe_type_of_reference env r = + match r with + | VarRef id -> Environ.named_type id env + | ConstRef c -> + let cb = Environ.lookup_constant c env in + Typeops.type_of_constant_type env cb.const_type + + | IndRef ind -> + let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in + let (_, inst), _ = unsafe_inductive_instance env ind in + Inductive.type_of_inductive env (specif, inst) + + | ConstructRef (ind, _ as cstr) -> + let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in + let (_, inst), _ = unsafe_inductive_instance env ind in + Inductive.type_of_constructor (cstr,inst) specif + +let unsafe_type_of_global t = unsafe_type_of_reference (Global.env ()) t + +let fresh_sort_in_family env = function + | InProp -> prop_sort, ContextSet.empty + | InSet -> set_sort, ContextSet.empty + | InType -> + let u = fresh_level () in + Type (Univ.Universe.make u), ContextSet.singleton u + +let new_sort_in_family sf = + fst (fresh_sort_in_family (Global.env ()) sf) + +let extend_context (a, ctx) (ctx') = + (a, ContextSet.union ctx ctx') + +let new_global_univ () = + let u = fresh_level () in + (Univ.Universe.make u, ContextSet.singleton u) + +(** Simplification *) + +module LevelUnionFind = Unionfind.Make (Univ.LSet) (Univ.LMap) + +let add_list_map u t map = + try + let l = LMap.find u map in + LMap.update u (t :: l) map + with Not_found -> + LMap.add u [t] map + +module UF = LevelUnionFind + +(** Precondition: flexible <= ctx *) +let choose_canonical ctx flexible algs s = + let global = LSet.diff s ctx in + let flexible, rigid = LSet.partition flexible (LSet.inter s ctx) in + (** If there is a global universe in the set, choose it *) + if not (LSet.is_empty global) then + let canon = LSet.choose global in + canon, (LSet.remove canon global, rigid, flexible) + else (** No global in the equivalence class, choose a rigid one *) + if not (LSet.is_empty rigid) then + let canon = LSet.choose rigid in + canon, (global, LSet.remove canon rigid, flexible) + else (** There are only flexible universes in the equivalence + class, choose a non-algebraic. *) + let algs, nonalgs = LSet.partition (fun x -> LSet.mem x algs) flexible in + if not (LSet.is_empty nonalgs) then + let canon = LSet.choose nonalgs in + canon, (global, rigid, LSet.remove canon flexible) + else + let canon = LSet.choose algs in + canon, (global, rigid, LSet.remove canon flexible) + +let subst_univs_fn_puniverses lsubst (c, u as cu) = + let u' = Instance.subst_fn lsubst u in + if u' == u then cu else (c, u') + +let nf_evars_and_universes_opt_subst f subst = + let subst = fun l -> match LMap.find l subst with None -> raise Not_found | Some l' -> l' in + let lsubst = Univ.level_subst_of subst in + let rec aux c = + match kind_of_term c with + | Evar (evk, args) -> + let args = Array.map aux args in + (match try f (evk, args) with Not_found -> None with + | None -> c + | Some c -> aux c) + | Const pu -> + let pu' = subst_univs_fn_puniverses lsubst pu in + if pu' == pu then c else mkConstU pu' + | Ind pu -> + let pu' = subst_univs_fn_puniverses lsubst pu in + if pu' == pu then c else mkIndU pu' + | Construct pu -> + let pu' = subst_univs_fn_puniverses lsubst pu in + if pu' == pu then c else mkConstructU pu' + | Sort (Type u) -> + let u' = Univ.subst_univs_universe subst u in + if u' == u then c else mkSort (sort_of_univ u') + | _ -> map_constr aux c + in aux + +let fresh_universe_context_set_instance ctx = + if ContextSet.is_empty ctx then LMap.empty, ctx + else + let (univs, cst) = ContextSet.levels ctx, ContextSet.constraints ctx in + let univs',subst = LSet.fold + (fun u (univs',subst) -> + let u' = fresh_level () in + (LSet.add u' univs', LMap.add u u' subst)) + univs (LSet.empty, LMap.empty) + in + let cst' = subst_univs_level_constraints subst cst in + subst, (univs', cst') + +let normalize_univ_variable ~find ~update = + let rec aux cur = + let b = find cur in + let b' = subst_univs_universe aux b in + if Universe.equal b' b then b + else update cur b' + in aux + +let normalize_univ_variable_opt_subst ectx = + let find l = + match Univ.LMap.find l !ectx with + | Some b -> b + | None -> raise Not_found + in + let update l b = + assert (match Universe.level b with Some l' -> not (Level.equal l l') | None -> true); + try ectx := Univ.LMap.add l (Some b) !ectx; b with Not_found -> assert false + in normalize_univ_variable ~find ~update + +let normalize_univ_variable_subst subst = + let find l = Univ.LMap.find l !subst in + let update l b = + assert (match Universe.level b with Some l' -> not (Level.equal l l') | None -> true); + try subst := Univ.LMap.update l b !subst; b with Not_found -> assert false in + normalize_univ_variable ~find ~update + +let normalize_universe_opt_subst subst = + let normlevel = normalize_univ_variable_opt_subst subst in + subst_univs_universe normlevel + +let normalize_universe_subst subst = + let normlevel = normalize_univ_variable_subst subst in + subst_univs_universe normlevel + +let normalize_opt_subst ctx = + let ectx = ref ctx in + let normalize = normalize_univ_variable_opt_subst ectx in + let () = + Univ.LMap.iter (fun u v -> + if Option.is_empty v then () + else try ignore(normalize u) with Not_found -> assert(false)) ctx + in !ectx + +type universe_opt_subst = universe option universe_map + +let make_opt_subst s = + fun x -> + (match Univ.LMap.find x s with + | Some u -> u + | None -> raise Not_found) + +let subst_opt_univs_constr s = + let f = make_opt_subst s in + Vars.subst_univs_fn_constr f + + +let normalize_univ_variables ctx = + let ctx = normalize_opt_subst ctx in + let undef, def, subst = + Univ.LMap.fold (fun u v (undef, def, subst) -> + match v with + | None -> (Univ.LSet.add u undef, def, subst) + | Some b -> (undef, Univ.LSet.add u def, Univ.LMap.add u b subst)) + ctx (Univ.LSet.empty, Univ.LSet.empty, Univ.LMap.empty) + in ctx, undef, def, subst + +let pr_universe_body = function + | None -> mt () + | Some v -> str" := " ++ Univ.Universe.pr v + +let pr_universe_opt_subst = Univ.LMap.pr pr_universe_body + +let compare_constraint_type d d' = + match d, d' with + | Eq, Eq -> 0 + | Eq, _ -> -1 + | _, Eq -> 1 + | Le, Le -> 0 + | Le, _ -> -1 + | _, Le -> 1 + | Lt, Lt -> 0 + +type lowermap = constraint_type LMap.t + +let lower_union = + let merge k a b = + match a, b with + | Some _, None -> a + | None, Some _ -> b + | None, None -> None + | Some l, Some r -> + if compare_constraint_type l r >= 0 then a + else b + in LMap.merge merge + +let lower_add l c m = + try let c' = LMap.find l m in + if compare_constraint_type c c' > 0 then + LMap.add l c m + else m + with Not_found -> LMap.add l c m + +let lower_of_list l = + List.fold_left (fun acc (d,l) -> LMap.add l d acc) LMap.empty l + +exception Found of Level.t * lowermap +let find_inst insts v = + try LMap.iter (fun k (enf,alg,v',lower) -> + if not alg && enf && Universe.equal v' v then raise (Found (k, lower))) + insts; raise Not_found + with Found (f,l) -> (f,l) + +let compute_lbound left = + (** The universe variable was not fixed yet. + Compute its level using its lower bound. *) + let sup l lbound = + match lbound with + | None -> Some l + | Some l' -> Some (Universe.sup l l') + in + List.fold_left (fun lbound (d, l) -> + if d == Le (* l <= ?u *) then sup l lbound + else (* l < ?u *) + (assert (d == Lt); + if not (Universe.level l == None) then + sup (Universe.super l) lbound + else None)) + None left + +let instantiate_with_lbound u lbound lower alg enforce (ctx, us, algs, insts, cstrs) = + if enforce then + let inst = Universe.make u in + let cstrs' = enforce_leq lbound inst cstrs in + (ctx, us, LSet.remove u algs, + LMap.add u (enforce,alg,lbound,lower) insts, cstrs'), + (enforce, alg, inst, lower) + else (* Actually instantiate *) + (Univ.LSet.remove u ctx, Univ.LMap.add u (Some lbound) us, algs, + LMap.add u (enforce,alg,lbound,lower) insts, cstrs), + (enforce, alg, lbound, lower) + +type constraints_map = (Univ.constraint_type * Univ.LMap.key) list Univ.LMap.t + +let pr_constraints_map cmap = + LMap.fold (fun l cstrs acc -> + Level.pr l ++ str " => " ++ + prlist_with_sep spc (fun (d,r) -> pr_constraint_type d ++ Level.pr r) cstrs ++ + fnl () ++ acc) + cmap (mt ()) + +let remove_alg l (ctx, us, algs, insts, cstrs) = + (ctx, us, LSet.remove l algs, insts, cstrs) + +let remove_lower u lower = + let levels = Universe.levels u in + LSet.fold (fun l acc -> LMap.remove l acc) levels lower + +let minimize_univ_variables ctx us algs left right cstrs = + let left, lbounds = + Univ.LMap.fold (fun r lower (left, lbounds as acc) -> + if Univ.LMap.mem r us || not (Univ.LSet.mem r ctx) then acc + else (* Fixed universe, just compute its glb for sharing *) + let lbounds' = + match compute_lbound (List.map (fun (d,l) -> d, Universe.make l) lower) with + | None -> lbounds + | Some lbound -> LMap.add r (true, false, lbound, lower_of_list lower) + lbounds + in (Univ.LMap.remove r left, lbounds')) + left (left, Univ.LMap.empty) + in + let rec instance (ctx', us, algs, insts, cstrs as acc) u = + let acc, left, lower = + try + let l = LMap.find u left in + let acc, left, newlow, lower = + List.fold_left + (fun (acc, left', newlow, lower') (d, l) -> + let acc', (enf,alg,l',lower) = aux acc l in + let l' = + if enf then Universe.make l + else l' + in acc', (d, l') :: left', + lower_add l d newlow, lower_union lower lower') + (acc, [], LMap.empty, LMap.empty) l + in + let not_lower (d,l) = + (* We're checking if (d,l) is already implied by the lower + constraints on some level u. If it represents l < u (d is Lt + or d is Le and i > 0, the i < 0 case is impossible due to + invariants of Univ), and the lower constraints only have l <= + u then it is not implied. *) + Univ.Universe.exists + (fun (l,i) -> + let d = + if i == 0 then d + else match d with + | Le -> Lt + | d -> d + in + try let d' = LMap.find l lower in + (* If d is stronger than the already implied lower + * constraints we must keep it. *) + compare_constraint_type d d' > 0 + with Not_found -> + (** No constraint existing on l *) true) l + in + let left = List.uniquize (List.filter not_lower left) in + (acc, left, LMap.union newlow lower) + with Not_found -> acc, [], LMap.empty + and right = + try Some (LMap.find u right) + with Not_found -> None + in + let instantiate_lbound lbound = + let alg = LSet.mem u algs in + if alg then + (* u is algebraic: we instantiate it with its lower bound, if any, + or enforce the constraints if it is bounded from the top. *) + let lower = remove_lower lbound lower in + instantiate_with_lbound u lbound lower true false acc + else (* u is non algebraic *) + match Universe.level lbound with + | Some l -> (* The lowerbound is directly a level *) + (* u is not algebraic but has no upper bounds, + we instantiate it with its lower bound if it is a + different level, otherwise we keep it. *) + let lower = LMap.remove l lower in + if not (Level.equal l u) then + (* Should check that u does not + have upper constraints that are not already in right *) + let acc' = remove_alg l acc in + instantiate_with_lbound u lbound lower false false acc' + else acc, (true, false, lbound, lower) + | None -> + try + (* Another universe represents the same lower bound, + we can share them with no harm. *) + let can, lower = find_inst insts lbound in + let lower = LMap.remove can lower in + instantiate_with_lbound u (Universe.make can) lower false false acc + with Not_found -> + (* We set u as the canonical universe representing lbound *) + instantiate_with_lbound u lbound lower false true acc + in + let acc' acc = + match right with + | None -> acc + | Some cstrs -> + let dangling = List.filter (fun (d, r) -> not (LMap.mem r us)) cstrs in + if List.is_empty dangling then acc + else + let ((ctx', us, algs, insts, cstrs), (enf,_,inst,lower as b)) = acc in + let cstrs' = List.fold_left (fun cstrs (d, r) -> + if d == Univ.Le then + enforce_leq inst (Universe.make r) cstrs + else + try let lev = Option.get (Universe.level inst) in + Constraint.add (lev, d, r) cstrs + with Option.IsNone -> failwith "") + cstrs dangling + in + (ctx', us, algs, insts, cstrs'), b + in + if not (LSet.mem u ctx) then acc' (acc, (true, false, Universe.make u, lower)) + else + let lbound = compute_lbound left in + match lbound with + | None -> (* Nothing to do *) + acc' (acc, (true, false, Universe.make u, lower)) + | Some lbound -> + try acc' (instantiate_lbound lbound) + with Failure _ -> acc' (acc, (true, false, Universe.make u, lower)) + and aux (ctx', us, algs, seen, cstrs as acc) u = + try acc, LMap.find u seen + with Not_found -> instance acc u + in + LMap.fold (fun u v (ctx', us, algs, seen, cstrs as acc) -> + if v == None then fst (aux acc u) + else LSet.remove u ctx', us, LSet.remove u algs, seen, cstrs) + us (ctx, us, algs, lbounds, cstrs) + +let normalize_context_set ctx us algs = + let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in + let uf = UF.create () in + (** Keep the Prop/Set <= i constraints separate for minimization *) + let smallles, csts = + Constraint.fold (fun (l,d,r as cstr) (smallles, noneqs) -> + if d == Le then + if Univ.Level.is_small l then + if is_set_minimization () && LSet.mem r ctx then + (Constraint.add cstr smallles, noneqs) + else (smallles, noneqs) + else if Level.is_small r then + if Level.is_prop r then + raise (Univ.UniverseInconsistency + (Le,Universe.make l,Universe.make r,None)) + else (smallles, Constraint.add (l,Eq,r) noneqs) + else (smallles, Constraint.add cstr noneqs) + else (smallles, Constraint.add cstr noneqs)) + csts (Constraint.empty, Constraint.empty) + in + let csts = + (* We first put constraints in a normal-form: all self-loops are collapsed + to equalities. *) + let g = Univ.LSet.fold (fun v g -> UGraph.add_universe v false g) + ctx UGraph.empty_universes + in + let g = + Univ.Constraint.fold + (fun (l, d, r) g -> + let g = + if not (Level.is_small l || LSet.mem l ctx) then + try UGraph.add_universe l false g + with UGraph.AlreadyDeclared -> g + else g + in + let g = + if not (Level.is_small r || LSet.mem r ctx) then + try UGraph.add_universe r false g + with UGraph.AlreadyDeclared -> g + else g + in g) csts g + in + let g = Univ.Constraint.fold UGraph.enforce_constraint csts g in + UGraph.constraints_of_universes g + in + let noneqs = + Constraint.fold (fun (l,d,r as cstr) noneqs -> + if d == Eq then (UF.union l r uf; noneqs) + else (* We ignore the trivial Prop/Set <= i constraints. *) + if d == Le && Univ.Level.is_small l then noneqs + else if Univ.Level.is_prop l && d == Lt && Univ.Level.is_set r + then noneqs + else Constraint.add cstr noneqs) + csts Constraint.empty + in + let noneqs = Constraint.union noneqs smallles in + let partition = UF.partition uf in + let flex x = LMap.mem x us in + let ctx, subst, us, eqs = List.fold_left (fun (ctx, subst, us, cstrs) s -> + let canon, (global, rigid, flexible) = choose_canonical ctx flex algs s in + (* Add equalities for globals which can't be merged anymore. *) + let cstrs = LSet.fold (fun g cst -> + Constraint.add (canon, Univ.Eq, g) cst) global + cstrs + in + (* Also add equalities for rigid variables *) + let cstrs = LSet.fold (fun g cst -> + Constraint.add (canon, Univ.Eq, g) cst) rigid + cstrs + in + let subst = LSet.fold (fun f -> LMap.add f canon) rigid subst in + let subst = LSet.fold (fun f -> LMap.add f canon) flexible subst in + let canonu = Some (Universe.make canon) in + let us = LSet.fold (fun f -> LMap.add f canonu) flexible us in + (LSet.diff ctx flexible, subst, us, cstrs)) + (ctx, LMap.empty, us, Constraint.empty) partition + in + (* Noneqs is now in canonical form w.r.t. equality constraints, + and contains only inequality constraints. *) + let noneqs = subst_univs_level_constraints subst noneqs in + (* Compute the left and right set of flexible variables, constraints + mentionning other variables remain in noneqs. *) + let noneqs, ucstrsl, ucstrsr = + Constraint.fold (fun (l,d,r as cstr) (noneq, ucstrsl, ucstrsr) -> + let lus = LMap.mem l us and rus = LMap.mem r us in + let ucstrsl' = + if lus then add_list_map l (d, r) ucstrsl + else ucstrsl + and ucstrsr' = + add_list_map r (d, l) ucstrsr + in + let noneqs = + if lus || rus then noneq + else Constraint.add cstr noneq + in (noneqs, ucstrsl', ucstrsr')) + noneqs (Constraint.empty, LMap.empty, LMap.empty) + in + (* Now we construct the instantiation of each variable. *) + let ctx', us, algs, inst, noneqs = + minimize_univ_variables ctx us algs ucstrsr ucstrsl noneqs + in + let us = normalize_opt_subst us in + (us, algs), (ctx', Constraint.union noneqs eqs) + +(* let normalize_conkey = Profile.declare_profile "normalize_context_set" *) +(* let normalize_context_set a b c = Profile.profile3 normalize_conkey normalize_context_set a b c *) + +let universes_of_constr c = + let rec aux s c = + match kind_of_term c with + | Const (_, u) | Ind (_, u) | Construct (_, u) -> + LSet.fold LSet.add (Instance.levels u) s + | Sort u when not (Sorts.is_small u) -> + let u = univ_of_sort u in + LSet.fold LSet.add (Universe.levels u) s + | _ -> fold_constr aux s c + in aux LSet.empty c + +let restrict_universe_context (univs,csts) s = + (* Universes that are not necessary to typecheck the term. + E.g. univs introduced by tactics and not used in the proof term. *) + let diff = LSet.diff univs s in + let rec aux diff candid univs ness = + let (diff', candid', univs', ness') = + Constraint.fold + (fun (l, d, r as c) (diff, candid, univs, csts) -> + if not (LSet.mem l diff) then + (LSet.remove r diff, candid, univs, Constraint.add c csts) + else if not (LSet.mem r diff) then + (LSet.remove l diff, candid, univs, Constraint.add c csts) + else (diff, Constraint.add c candid, univs, csts)) + candid (diff, Constraint.empty, univs, ness) + in + if ness' == ness then (LSet.diff univs diff', ness) + else aux diff' candid' univs' ness' + in aux diff csts univs Constraint.empty + +let simplify_universe_context (univs,csts) = + let uf = UF.create () in + let noneqs = + Constraint.fold (fun (l,d,r) noneqs -> + if d == Eq && (LSet.mem l univs || LSet.mem r univs) then + (UF.union l r uf; noneqs) + else Constraint.add (l,d,r) noneqs) + csts Constraint.empty + in + let partition = UF.partition uf in + let flex x = LSet.mem x univs in + let subst, univs', csts' = List.fold_left (fun (subst, univs, cstrs) s -> + let canon, (global, rigid, flexible) = choose_canonical univs flex LSet.empty s in + (* Add equalities for globals which can't be merged anymore. *) + let cstrs = LSet.fold (fun g cst -> + Constraint.add (canon, Univ.Eq, g) cst) (LSet.union global rigid) + cstrs + in + let subst = LSet.fold (fun f -> LMap.add f canon) + flexible subst + in (subst, LSet.diff univs flexible, cstrs)) + (LMap.empty, univs, noneqs) partition + in + (* Noneqs is now in canonical form w.r.t. equality constraints, + and contains only inequality constraints. *) + let csts' = subst_univs_level_constraints subst csts' in + (univs', csts'), subst + +let is_trivial_leq (l,d,r) = + Univ.Level.is_prop l && (d == Univ.Le || (d == Univ.Lt && Univ.Level.is_set r)) + +(* Prop < i <-> Set+1 <= i <-> Set < i *) +let translate_cstr (l,d,r as cstr) = + if Level.equal Level.prop l && d == Univ.Lt && not (Level.equal Level.set r) then + (Level.set, d, r) + else cstr + +let refresh_constraints univs (ctx, cstrs) = + let cstrs', univs' = + Univ.Constraint.fold (fun c (cstrs', univs as acc) -> + let c = translate_cstr c in + if is_trivial_leq c then acc + else (Univ.Constraint.add c cstrs', UGraph.enforce_constraint c univs)) + cstrs (Univ.Constraint.empty, univs) + in ((ctx, cstrs'), univs') + + +(**********************************************************************) +(* Tools for sort-polymorphic inductive types *) + +(* Miscellaneous functions to remove or test local univ assumed to + occur only in the le constraints *) + +(* + Solve a system of universe constraint of the form + + u_s11, ..., u_s1p1, w1 <= u1 + ... + u_sn1, ..., u_snpn, wn <= un + +where + + - the ui (1 <= i <= n) are universe variables, + - the sjk select subsets of the ui for each equations, + - the wi are arbitrary complex universes that do not mention the ui. +*) + +let is_direct_sort_constraint s v = match s with + | Some u -> univ_level_mem u v + | None -> false + +let solve_constraints_system levels level_bounds level_min = + let open Univ in + let levels = + Array.mapi (fun i o -> + match o with + | Some u -> + (match Universe.level u with + | Some u -> Some u + | _ -> level_bounds.(i) <- Universe.sup level_bounds.(i) u; None) + | None -> None) + levels in + let v = Array.copy level_bounds in + let nind = Array.length v in + let clos = Array.map (fun _ -> Int.Set.empty) levels in + (* First compute the transitive closure of the levels dependencies *) + for i=0 to nind-1 do + for j=0 to nind-1 do + if not (Int.equal i j) && is_direct_sort_constraint levels.(j) v.(i) then + clos.(i) <- Int.Set.add j clos.(i); + done; + done; + let rec closure () = + let continue = ref false in + Array.iteri (fun i deps -> + let deps' = + Int.Set.fold (fun j acc -> Int.Set.union acc clos.(j)) deps deps + in + if Int.Set.equal deps deps' then () + else (clos.(i) <- deps'; continue := true)) + clos; + if !continue then closure () + else () + in + closure (); + for i=0 to nind-1 do + for j=0 to nind-1 do + if not (Int.equal i j) && Int.Set.mem j clos.(i) then + (v.(i) <- Universe.sup v.(i) level_bounds.(j)); + done; + done; + v diff --git a/engine/universes.mli b/engine/universes.mli new file mode 100644 index 0000000000..725c21d296 --- /dev/null +++ b/engine/universes.mli @@ -0,0 +1,231 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Util +open Names +open Term +open Environ +open Univ + +val set_minimization : bool ref +val is_set_minimization : unit -> bool + +(** Universes *) + +val pr_with_global_universes : Level.t -> Pp.std_ppcmds + +(** Local universe name <-> level mapping *) + +type universe_binders = (Id.t * Univ.universe_level) list + +val register_universe_binders : Globnames.global_reference -> universe_binders -> unit +val universe_binders_of_global : Globnames.global_reference -> universe_binders + +(** The global universe counter *) +val set_remote_new_univ_level : universe_level RemoteCounter.installer + +(** Side-effecting functions creating new universe levels. *) + +val new_univ_level : Names.dir_path -> universe_level +val new_univ : Names.dir_path -> universe +val new_Type : Names.dir_path -> types +val new_Type_sort : Names.dir_path -> sorts + +val new_global_univ : unit -> universe in_universe_context_set +val new_sort_in_family : sorts_family -> sorts + +(** {6 Constraints for type inference} + + When doing conversion of universes, not only do we have =/<= constraints but + also Lub constraints which correspond to unification of two levels which might + not be necessary if unfolding is performed. +*) + +type universe_constraint_type = ULe | UEq | ULub + +type universe_constraint = universe * universe_constraint_type * universe +module Constraints : sig + include Set.S with type elt = universe_constraint + + val pr : t -> Pp.std_ppcmds +end + +type universe_constraints = Constraints.t +type 'a constraint_accumulator = universe_constraints -> 'a -> 'a option +type 'a universe_constrained = 'a * universe_constraints +type 'a universe_constraint_function = 'a -> 'a -> universe_constraints -> universe_constraints + +val subst_univs_universe_constraints : universe_subst_fn -> + universe_constraints -> universe_constraints + +val enforce_eq_instances_univs : bool -> universe_instance universe_constraint_function + +val to_constraints : UGraph.t -> universe_constraints -> constraints + +(** [eq_constr_univs_infer u a b] is [true, c] if [a] equals [b] modulo alpha, casts, + application grouping, the universe constraints in [u] and additional constraints [c]. *) +val eq_constr_univs_infer : UGraph.t -> 'a constraint_accumulator -> + constr -> constr -> 'a -> 'a option + +(** [eq_constr_univs_infer_With kind1 kind2 univs m n] is a variant of + {!eq_constr_univs_infer} taking kind-of-term functions, to expose + subterms of [m] and [n], arguments. *) +val eq_constr_univs_infer_with : + (constr -> (constr,types) kind_of_term) -> + (constr -> (constr,types) kind_of_term) -> + UGraph.t -> 'a constraint_accumulator -> constr -> constr -> 'a -> 'a option + +(** [leq_constr_univs u a b] is [true, c] if [a] is convertible to [b] + modulo alpha, casts, application grouping, the universe constraints + in [u] and additional constraints [c]. *) +val leq_constr_univs_infer : UGraph.t -> 'a constraint_accumulator -> + constr -> constr -> 'a -> 'a option + +(** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts, + application grouping and the universe constraints in [c]. *) +val eq_constr_universes : constr -> constr -> universe_constraints option + +(** [leq_constr_universes a b] [true, c] if [a] is convertible to [b] modulo + alpha, casts, application grouping and the universe constraints in [c]. *) +val leq_constr_universes : constr -> constr -> universe_constraints option + +(** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts, + application grouping and the universe constraints in [c]. *) +val eq_constr_universes_proj : env -> constr -> constr -> bool universe_constrained + +(** Build a fresh instance for a given context, its associated substitution and + the instantiated constraints. *) + +val fresh_instance_from_context : universe_context -> + universe_instance constrained + +val fresh_instance_from : universe_context -> universe_instance option -> + universe_instance in_universe_context_set + +val fresh_sort_in_family : env -> sorts_family -> + sorts in_universe_context_set +val fresh_constant_instance : env -> constant -> + pconstant in_universe_context_set +val fresh_inductive_instance : env -> inductive -> + pinductive in_universe_context_set +val fresh_constructor_instance : env -> constructor -> + pconstructor in_universe_context_set + +val fresh_global_instance : ?names:Univ.Instance.t -> env -> Globnames.global_reference -> + constr in_universe_context_set + +val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr -> + constr in_universe_context_set + +(** Get fresh variables for the universe context. + Useful to make tactics that manipulate constrs in universe contexts polymorphic. *) +val fresh_universe_context_set_instance : universe_context_set -> + universe_level_subst * universe_context_set + +(** Raises [Not_found] if not a global reference. *) +val global_of_constr : constr -> Globnames.global_reference puniverses + +val global_app_of_constr : constr -> Globnames.global_reference puniverses * constr option + +val constr_of_global_univ : Globnames.global_reference puniverses -> constr + +val extend_context : 'a in_universe_context_set -> universe_context_set -> + 'a in_universe_context_set + +(** Simplification and pruning of constraints: + [normalize_context_set ctx us] + + - Instantiate the variables in [us] with their most precise + universe levels respecting the constraints. + + - Normalizes the context [ctx] w.r.t. equality constraints, + choosing a canonical universe in each equivalence class + (a global one if there is one) and transitively saturate + the constraints w.r.t to the equalities. *) + +module UF : Unionfind.PartitionSig with type elt = universe_level + +type universe_opt_subst = universe option universe_map + +val make_opt_subst : universe_opt_subst -> universe_subst_fn + +val subst_opt_univs_constr : universe_opt_subst -> constr -> constr + +val normalize_context_set : universe_context_set -> + universe_opt_subst (* The defined and undefined variables *) -> + universe_set (* univ variables that can be substituted by algebraics *) -> + (universe_opt_subst * universe_set) in_universe_context_set + +val normalize_univ_variables : universe_opt_subst -> + universe_opt_subst * universe_set * universe_set * universe_subst + +val normalize_univ_variable : + find:(universe_level -> universe) -> + update:(universe_level -> universe -> universe) -> + universe_level -> universe + +val normalize_univ_variable_opt_subst : universe_opt_subst ref -> + (universe_level -> universe) + +val normalize_univ_variable_subst : universe_subst ref -> + (universe_level -> universe) + +val normalize_universe_opt_subst : universe_opt_subst ref -> + (universe -> universe) + +val normalize_universe_subst : universe_subst ref -> + (universe -> universe) + +(** Create a fresh global in the global environment, without side effects. + BEWARE: this raises an ANOMALY on polymorphic constants/inductives: + the constraints should be properly added to an evd. + See Evd.fresh_global, Evarutil.new_global, and pf_constr_of_global for + the proper way to get a fresh copy of a global reference. *) +val constr_of_global : Globnames.global_reference -> constr + +(** ** DEPRECATED ** synonym of [constr_of_global] *) +val constr_of_reference : Globnames.global_reference -> constr + +(** [unsafe_constr_of_global gr] turns [gr] into a constr, works on polymorphic + references by taking the original universe instance that is not recorded + anywhere. The constraints are forgotten as well. DO NOT USE in new code. *) +val unsafe_constr_of_global : Globnames.global_reference -> constr in_universe_context + +(** Returns the type of the global reference, by creating a fresh instance of polymorphic + references and computing their instantiated universe context. (side-effect on the + universe counter, use with care). *) +val type_of_global : Globnames.global_reference -> types in_universe_context_set + +(** [unsafe_type_of_global gr] returns [gr]'s type, works on polymorphic + references by taking the original universe instance that is not recorded + anywhere. The constraints are forgotten as well. + USE with care. *) +val unsafe_type_of_global : Globnames.global_reference -> types + +(** Full universes substitutions into terms *) + +val nf_evars_and_universes_opt_subst : (existential -> constr option) -> + universe_opt_subst -> constr -> constr + +(** Shrink a universe context to a restricted set of variables *) + +val universes_of_constr : constr -> universe_set +val restrict_universe_context : universe_context_set -> universe_set -> universe_context_set +val simplify_universe_context : universe_context_set -> + universe_context_set * universe_level_subst + +val refresh_constraints : UGraph.t -> universe_context_set -> universe_context_set * UGraph.t + +(** Pretty-printing *) + +val pr_universe_opt_subst : universe_opt_subst -> Pp.std_ppcmds + +(** {6 Support for old-style sort-polymorphism } *) + +val solve_constraints_system : universe option array -> universe array -> universe array -> + universe array |