diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/eConstr.ml | 3 | ||||
| -rw-r--r-- | engine/eConstr.mli | 2 | ||||
| -rw-r--r-- | engine/evd.ml | 12 | ||||
| -rw-r--r-- | engine/evd.mli | 15 | ||||
| -rw-r--r-- | engine/proofview.ml | 37 | ||||
| -rw-r--r-- | engine/proofview.mli | 2 | ||||
| -rw-r--r-- | engine/termops.ml | 3 |
7 files changed, 62 insertions, 12 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index b6b202cd9..f50a8b850 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -634,6 +634,9 @@ let closedn sigma n c = let closed0 sigma c = closedn sigma 0 c +let subst_of_rel_context_instance ctx subst = + List.map of_constr (Vars.subst_of_rel_context_instance (List.map unsafe_to_rel_decl ctx) (List.map to_constr subst)) + end let rec isArity sigma c = diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 3b479a64d..1ae71216f 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -195,6 +195,8 @@ val closedn : Evd.evar_map -> int -> t -> bool val closed0 : Evd.evar_map -> t -> bool val subst_univs_level_constr : Univ.universe_level_subst -> t -> t +val subst_of_rel_context_instance : rel_context -> t list -> t list + end diff --git a/engine/evd.ml b/engine/evd.ml index b8f4b126a..0ea15dd21 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -664,13 +664,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 (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 @@ -829,6 +832,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 diff --git a/engine/evd.mli b/engine/evd.mli index 2151000b6..9c6cd60bc 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -463,7 +463,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 @@ -510,7 +520,8 @@ val new_univ_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_ 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 diff --git a/engine/proofview.ml b/engine/proofview.ml index 71e9acc88..9c264439b 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -424,11 +424,11 @@ let tclFOCUSID id t = exception SizeMismatch of int*int let _ = CErrors.register_handler begin function - | SizeMismatch (i,_) -> + | 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 CErrors.user_err errmsg | _ -> raise CErrors.Unhandled @@ -454,6 +454,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 @@ -586,7 +605,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} *) @@ -1157,10 +1184,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 diff --git a/engine/proofview.mli b/engine/proofview.mli index 4f662b294..a3b0304b1 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -293,6 +293,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} *) @@ -374,7 +375,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 diff --git a/engine/termops.ml b/engine/termops.ml index d8e712abc..410fb75c5 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -185,6 +185,7 @@ let pr_decl (decl,ok) = 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 -> @@ -1368,7 +1369,7 @@ let smash_rel_context sign = let fold_named_context_both_sides f l ~init = List.fold_right_and_left f l init let mem_named_context_val id ctxt = - try Environ.lookup_named_val id ctxt; true with Not_found -> false + try ignore(Environ.lookup_named_val id ctxt); true with Not_found -> false let map_rel_decl f = function | RelDecl.LocalAssum (id, t) -> RelDecl.LocalAssum (id, f t) |