diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/evarutil.ml | 188 | ||||
| -rw-r--r-- | engine/evarutil.mli | 20 | ||||
| -rw-r--r-- | engine/evd.ml | 30 | ||||
| -rw-r--r-- | engine/evd.mli | 16 | ||||
| -rw-r--r-- | engine/ftactic.ml | 23 | ||||
| -rw-r--r-- | engine/logic_monad.ml | 20 | ||||
| -rw-r--r-- | engine/namegen.ml | 10 | ||||
| -rw-r--r-- | engine/namegen.mli | 3 | ||||
| -rw-r--r-- | engine/proofview.ml | 148 | ||||
| -rw-r--r-- | engine/proofview.mli | 20 | ||||
| -rw-r--r-- | engine/sigma.ml | 12 | ||||
| -rw-r--r-- | engine/sigma.mli | 6 | ||||
| -rw-r--r-- | engine/termops.ml | 13 | ||||
| -rw-r--r-- | engine/termops.mli | 3 | ||||
| -rw-r--r-- | engine/uState.ml | 23 |
15 files changed, 342 insertions, 193 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml index df1424e1c6..df170c8ddc 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,10 @@ open Environ open Evd open Sigma.Notations +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 +70,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') @@ -290,78 +296,110 @@ 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 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 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 replace_var_named_declaration id0 id decl = let id' = 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 - 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 open Context.Rel.Declaration in + let (na, c, t) = to_tuple 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 + (** 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 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 = (fst subst, Int.Map.map (replace_vars [id0,mkVar id]) (snd 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 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 = match c with + | None -> LocalAssum (id, subst2 subst vsubst t) + | Some c -> LocalDef (id, subst2 subst vsubst c, subst2 subst vsubst t) + 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 * @@ -640,6 +678,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 diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 111d0f3e8c..7fdc7aac78 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -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..aa91fc5222 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Names open Nameops @@ -252,6 +252,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 @@ -640,6 +641,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} @@ -789,16 +791,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 = @@ -998,7 +1000,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 +1259,12 @@ 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 print_constr a = protect print_constr a + let pr_meta_map mmap = let pr_name = function Name id -> str"[" ++ pr_id id ++ str"]" @@ -1404,6 +1412,16 @@ 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 () ++ str (match pbty with diff --git a/engine/evd.mli b/engine/evd.mli index df491c27b4..b47b389d1b 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -98,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. *) } @@ -508,9 +509,10 @@ 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 make_flexible_variable : evar_map -> bool -> Univ.universe_level -> evar_map @@ -568,8 +570,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 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/logic_monad.ml b/engine/logic_monad.ml index 64be07b9c7..17ff898b0f 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.errorlabstrm "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/namegen.ml b/engine/namegen.ml index bc04e3e483..84eb986845 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -191,18 +191,26 @@ let visible_ids (nenv, c) = 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 (lookup_name_of_rel (p - n) nenv) - with Not_found -> None (* Unbound indice : may happen in debug *) + with Not_found -> + (* 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 diff --git a/engine/namegen.mli b/engine/namegen.mli index e5c156b4e5..97c7c34a56 100644 --- a/engine/namegen.mli +++ b/engine/namegen.mli @@ -64,9 +64,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 d876860652..c01879765b 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -152,33 +152,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 +285,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 +338,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.errorlabstrm "" + (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 @@ -443,15 +420,15 @@ let tclFOCUSID id t = (** {7 Dispatching on goals} *) exception SizeMismatch of int*int -let _ = Errors.register_handler begin function +let _ = CErrors.register_handler begin function | SizeMismatch (i,_) -> let open Pp in let errmsg = str"Incorrect number of goals" ++ spc() ++ str"(expected "++int i++str(String.plural i " tactic") ++ str")." in - Errors.errorlabstrm "" errmsg - | _ -> raise Errors.Unhandled + CErrors.errorlabstrm "" errmsg + | _ -> raise CErrors.Unhandled end (** A variant of [Monad.List.iter] where we iter over the focused list @@ -464,7 +441,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] >> @@ -488,7 +465,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] >> @@ -532,7 +509,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 @@ -684,6 +661,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 -> @@ -696,8 +688,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]].*) @@ -844,12 +839,12 @@ let tclPROGRESS t = if not test then tclUNIT res else - tclZERO (Errors.UserError ("Proofview.tclPROGRESS" , Pp.str"Failed to progress.")) + tclZERO (CErrors.UserError ("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.errorlabstrm "Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!") + | _ -> Pervasives.raise CErrors.Unhandled end let tclTIMEOUT n t = @@ -928,6 +923,8 @@ module Unsafe = struct { step with comb = step.comb @ gls } end + let tclSETENV = Env.set + let tclGETGOALS = Comb.get let tclSETGOALS = Comb.set @@ -942,19 +939,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 @@ -983,7 +973,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 @@ -1029,7 +1019,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 @@ -1052,11 +1042,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.errorlabstrm "" (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 } @@ -1071,7 +1081,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 @@ -1087,7 +1097,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 @@ -1096,7 +1106,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 = @@ -1108,6 +1118,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 @@ -1143,10 +1157,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 @@ -1175,7 +1185,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 @@ -1220,7 +1230,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 @@ -1230,7 +1240,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 901cf26e0e..90be2f90ab 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -326,8 +326,9 @@ val unshelve : Goal.goal list -> proofview -> proofview (** [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. *) +(** [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] @@ -372,7 +373,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 @@ -409,6 +409,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. *) @@ -431,6 +434,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) @@ -499,6 +505,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 } @@ -514,6 +524,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/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 aaf603efd8..7473a251b7 100644 --- a/engine/sigma.mli +++ b/engine/sigma.mli @@ -68,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 ac8461a3ab..697b9a5f15 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 @@ -599,6 +599,10 @@ 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] *) @@ -975,11 +979,8 @@ 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 l decl = diff --git a/engine/termops.mli b/engine/termops.mli index 5d85088f8d..fd8edafbcf 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -121,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 *) @@ -237,7 +238,7 @@ 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 mem_named_context_val : Id.t -> named_context_val -> bool val compact_named_context : Context.Named.t -> Context.NamedList.t val compact_named_context_reverse : Context.Named.t -> Context.NamedList.t diff --git a/engine/uState.ml b/engine/uState.ml index 8aa9a61ab9..c35f97b2e9 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 @@ -263,13 +263,17 @@ let universe_context ?names ctx = 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.")) + (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 } |