From 0e189432da864d7e31c9d6bb2355f349308a3d0a Mon Sep 17 00:00:00 2001 From: msozeau Date: Sun, 7 Sep 2008 00:05:39 +0000 Subject: Better handling of the opacity of proof obligations, add the possibility of overriding the default tactic when adding a definition. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11373 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/subtac/eterm.ml | 46 ++++++-- contrib/subtac/eterm.mli | 11 +- contrib/subtac/subtac.ml | 16 ++- contrib/subtac/subtac_cases.ml | 2 +- contrib/subtac/subtac_command.ml | 2 +- contrib/subtac/subtac_obligations.ml | 208 ++++++++++++++++++++-------------- contrib/subtac/subtac_obligations.mli | 7 +- contrib/subtac/subtac_utils.ml | 3 +- contrib/subtac/subtac_utils.mli | 3 +- interp/constrintern.ml | 2 +- parsing/q_constr.ml4 | 2 +- pretyping/evd.ml | 4 +- pretyping/evd.mli | 7 +- tactics/decl_interp.ml | 2 +- 14 files changed, 192 insertions(+), 123 deletions(-) diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml index 037911a19..c2d7a59f1 100644 --- a/contrib/subtac/eterm.ml +++ b/contrib/subtac/eterm.ml @@ -6,6 +6,7 @@ *) open Term +open Sign open Names open Evd open List @@ -20,15 +21,26 @@ let trace s = let succfix (depth, fixrels) = (succ depth, List.map succ fixrels) +type oblinfo = + { ev_name: int * identifier; + ev_hyps: named_context; + ev_status : obligation_definition_status; + ev_chop: int option; + ev_loc: Util.loc; + ev_typ: types; + ev_deps: Intset.t } + (** Substitute evar references in t using De Bruijn indices, where n binders were passed through. *) + let subst_evar_constr evs n t = let seen = ref Intset.empty in let transparent = ref Idset.empty in let evar_info id = List.assoc id evs in let rec substrec (depth, fixrels) c = match kind_of_term c with | Evar (k, args) -> - let (id, idstr), hyps, chop, _, _, _ = + let { ev_name = (id, idstr) ; + ev_hyps = hyps ; ev_chop = chop } = try evar_info k with Not_found -> anomaly ("eterm: existential variable " ^ string_of_int k ^ " not found") @@ -117,7 +129,7 @@ let rec chop_product n t = | Prod (_, _, b) -> if noccurn 1 b then chop_product (pred n) (Termops.pop b) else None | _ -> None -let eterm_obligations env name isevars evm fs t ty = +let eterm_obligations env name isevars evm fs ?status t ty = (* 'Serialize' the evars, we assume that the types of the existentials refer to previous existentials in the list only *) let nc = Environ.named_context env in @@ -139,14 +151,22 @@ let eterm_obligations env name isevars evm fs t ty = let evtyp, deps, transp = etype_of_evar l hyps ev.evar_concl in let evtyp, hyps, chop = match chop_product fs evtyp with - Some t -> t, trunc_named_context fs hyps, fs - | None -> evtyp, hyps, 0 + | Some t -> t, trunc_named_context fs hyps, fs + | None -> evtyp, hyps, 0 in let loc, k = evar_source id isevars in - let opacity = match k with QuestionMark o -> o | _ -> true in - let opaque = if not opacity || chop <> fs then None else Some chop in - let y' = (id, ((n, nstr), hyps, opaque, loc, evtyp, deps)) in - y' :: l) + let status = match k with QuestionMark o -> Some o | _ -> status in + let status, chop = match status with + | Some (Define true as stat) -> + if chop <> fs then Define false, None + else stat, Some chop + | Some s -> s, None + | None -> Define true, None + in + let info = { ev_name = (n, nstr); + ev_hyps = hyps; ev_status = status; ev_chop = chop; + ev_loc = loc; ev_typ = evtyp ; ev_deps = deps } + in (id, info) :: l) evn [] in let t', _, transparent = (* Substitute evar refs in the term by variables *) @@ -154,8 +174,14 @@ let eterm_obligations env name isevars evm fs t ty = in let ty, _, _ = subst_evar_constr evts 0 ty in let evars = - List.map (fun (_, ((_, name), _, opaque, loc, typ, deps)) -> - name, typ, loc, not (opaque = None) && not (Idset.mem name transparent), deps) evts + List.map (fun (_, info) -> + let { ev_name = (_, name); ev_status = status; + ev_loc = loc; ev_typ = typ; ev_deps = deps } = info + in + let status = match status with + | Define true when Idset.mem name transparent -> Define false + | _ -> status + in name, typ, loc, status, deps) evts in Array.of_list (List.rev evars), t', ty let mkMetas n = list_tabulate (fun _ -> Evarutil.mk_new_meta ()) n diff --git a/contrib/subtac/eterm.mli b/contrib/subtac/eterm.mli index bf854abb3..e197024ff 100644 --- a/contrib/subtac/eterm.mli +++ b/contrib/subtac/eterm.mli @@ -16,11 +16,12 @@ open Util val mkMetas : int -> constr list -(* env, id, evars, number of - function prototypes to try to clear from evars contexts, object and type *) -val eterm_obligations : env -> identifier -> evar_defs -> evar_map -> int -> constr -> types -> - (identifier * types * loc * bool * Intset.t) array * constr * types +(* env, id, evars, number of function prototypes to try to clear from + evars contexts, object and type *) +val eterm_obligations : env -> identifier -> evar_defs -> evar_map -> int -> + ?status:obligation_definition_status -> constr -> types -> + (identifier * types * loc * obligation_definition_status * Intset.t) array * constr * types (* Obl. name, type as product, location of the original evar, - opacity (true = opaque) and dependencies as indexes into the array *) + status and dependencies as indexes into the array *) val etermtac : open_constr -> tactic diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml index baf565ab1..acf1ae838 100644 --- a/contrib/subtac/subtac.ml +++ b/contrib/subtac/subtac.ml @@ -52,16 +52,14 @@ open Tacexpr let solve_tccs_in_type env id isevars evm c typ = if not (evm = Evd.empty) then let stmt_id = Nameops.add_suffix id "_stmt" in - let obls, c', t' = eterm_obligations env stmt_id !isevars evm 0 c typ in - (** Make all obligations transparent so that real dependencies can be sorted out by the user *) - let obls = Array.map (fun (id, t, l, op, d) -> (id, t, l, false, d)) obls in + let obls, c', t' = eterm_obligations env stmt_id !isevars evm 0 ~status:Expand c typ in match Subtac_obligations.add_definition stmt_id c' typ obls with - Subtac_obligations.Defined cst -> constant_value (Global.env()) - (match cst with ConstRef kn -> kn | _ -> assert false) - | _ -> - errorlabstrm "start_proof" - (str "The statement obligations could not be resolved automatically, " ++ spc () ++ - str "write a statement definition first.") + Subtac_obligations.Defined cst -> constant_value (Global.env()) + (match cst with ConstRef kn -> kn | _ -> assert false) + | _ -> + errorlabstrm "start_proof" + (str "The statement obligations could not be resolved automatically, " ++ spc () ++ + str "write a statement definition first.") else let _ = Typeops.infer_type env c in c diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml index 009b80606..f45efe50b 100644 --- a/contrib/subtac/subtac_cases.ml +++ b/contrib/subtac/subtac_cases.ml @@ -1572,7 +1572,7 @@ let mk_JMeq typ x typ' y = mkApp (Lazy.force Subtac_utils.jmeq_ind, [| typ; x ; typ'; y |]) let mk_JMeq_refl typ x = mkApp (Lazy.force Subtac_utils.jmeq_refl, [| typ; x |]) -let hole = RHole (dummy_loc, Evd.QuestionMark true) +let hole = RHole (dummy_loc, Evd.QuestionMark (Evd.Define true)) let context_of_arsign l = let (x, _) = List.fold_right diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml index a2f54b02d..503f34619 100644 --- a/contrib/subtac/subtac_command.ml +++ b/contrib/subtac/subtac_command.ml @@ -284,7 +284,7 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = mkApp (constr_of_global (Lazy.force fix_sub_ref), [| argtyp ; wf_rel ; - make_existential dummy_loc ~opaque:false env isevars wf_proof ; + make_existential dummy_loc ~opaque:(Define false) env isevars wf_proof ; lift lift_cst prop ; lift lift_cst intern_body_lam |]) | Some f -> diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml index 563b228d8..6d1ec5ede 100644 --- a/contrib/subtac/subtac_obligations.ml +++ b/contrib/subtac/subtac_obligations.ml @@ -1,7 +1,9 @@ +(* -*- compile-command: "make -C ../.. bin/coqtop.byte" -*- *) open Printf open Pp open Subtac_utils open Command +open Environ open Term open Names @@ -16,6 +18,7 @@ open Declare type definition_hook = global_reference -> unit +let ppwarn cmd = Pp.warn (str"Program:" ++ cmd) let pperror cmd = Util.errorlabstrm "Program" cmd let error s = pperror (str s) @@ -25,14 +28,14 @@ let explain_no_obligations = function Some ident -> str "No obligations for program " ++ str (string_of_id ident) | None -> str "No obligations remaining" -type obligation_info = (Names.identifier * Term.types * loc * bool * Intset.t) array +type obligation_info = (Names.identifier * Term.types * loc * obligation_definition_status * Intset.t) array type obligation = { obl_name : identifier; obl_type : types; obl_location : loc; obl_body : constr option; - obl_opaque : bool; + obl_status : obligation_definition_status; obl_deps : Intset.t; } @@ -79,22 +82,29 @@ let _ = let evar_of_obligation o = make_evar (Global.named_context_val ()) o.obl_type -let subst_deps obls deps t = - Intset.fold - (fun x acc -> - let xobl = obls.(x) in - debug 3 (str "Trying to get body of obligation " ++ int x); - let oblb = - try Option.get xobl.obl_body - with _ -> - debug 3 (str "Couldn't get body of obligation " ++ int x); - assert(false) - in - Term.subst1 oblb (Term.subst_var xobl.obl_name acc)) - deps t - +let get_obligation_body expand obl = + let c = Option.get obl.obl_body in + if expand && obl.obl_status = Expand then + match kind_of_term c with + | Const c -> constant_value (Global.env ()) c + | _ -> c + else c + +let subst_deps expand obls deps t = + let subst = + Intset.fold + (fun x acc -> + let xobl = obls.(x) in + let oblb = + try get_obligation_body expand xobl + with _ -> assert(false) + in (xobl.obl_name, oblb) :: acc) + deps [] + in(* Termops.it_mkNamedProd_or_LetIn t subst *) + Term.replace_vars subst t + let subst_deps_obl obls obl = - let t' = subst_deps obls obl.obl_deps obl.obl_type in + let t' = subst_deps false obls obl.obl_deps obl.obl_type in { obl with obl_type = t' } module ProgMap = Map.Make(struct type t = identifier let compare = compare end) @@ -150,14 +160,14 @@ let rec intset_to = function -1 -> Intset.empty | n -> Intset.add n (intset_to (pred n)) -let subst_body prg = +let subst_body expand prg = let obls, _ = prg.prg_obligations in let ints = intset_to (pred (Array.length obls)) in - subst_deps obls ints prg.prg_body, - subst_deps obls ints (Termops.refresh_universes prg.prg_type) + subst_deps expand obls ints prg.prg_body, + subst_deps expand obls ints (Termops.refresh_universes prg.prg_type) let declare_definition prg = - let body, typ = subst_body prg in + let body, typ = subst_body false prg in (try trace (str "Declaring: " ++ Ppconstr.pr_id prg.prg_name ++ spc () ++ my_print_constr (Global.env()) body ++ str " : " ++ my_print_constr (Global.env()) prg.prg_type); @@ -216,14 +226,18 @@ let compute_possible_guardness_evidences (n,_) fixbody fixtype = let ctx = fst (Sign.decompose_prod_n_assum m fixtype) in list_map_i (fun i _ -> i) 0 ctx +let reduce_fix = + Reductionops.clos_norm_flags Closure.betaiotazeta (Global.env ()) Evd.empty + let declare_mutual_definition l = let len = List.length l in let fixdefs, fixtypes, fiximps = list_split3 (List.map (fun x -> - let subs, typ = (subst_body x) in + let subs, typ = (subst_body false x) in snd (decompose_lam_n len subs), snd (decompose_prod_n len typ), x.prg_implicits) l) in +(* let fixdefs = List.map reduce_fix fixdefs in *) let fixkind = Option.get (List.hd l).prg_fixkind in let arrrec, recvec = Array.of_list fixtypes, Array.of_list fixdefs in let fixdecls = (Array.of_list (List.map (fun x -> Name x.prg_name) l), arrrec, recvec) in @@ -248,18 +262,23 @@ let declare_mutual_definition l = (match List.hd kns with ConstRef kn -> kn | _ -> assert false) let declare_obligation obl body = - let ce = - { const_entry_body = body; - const_entry_type = Some obl.obl_type; - const_entry_opaque = if get_proofs_transparency () then false else obl.obl_opaque; - const_entry_boxed = false} - in - let constant = Declare.declare_constant obl.obl_name - (DefinitionEntry ce,IsProof Property) - in - print_message (Subtac_utils.definition_message obl.obl_name); - { obl with obl_body = Some (mkConst constant) } - + match obl.obl_status with + | Expand -> { obl with obl_body = Some body } + | Define opaque -> + let ce = + { const_entry_body = body; + const_entry_type = Some obl.obl_type; + const_entry_opaque = + (if get_proofs_transparency () then false + else opaque) ; + const_entry_boxed = false} + in + let constant = Declare.declare_constant obl.obl_name + (DefinitionEntry ce,IsProof Property) + in + print_message (Subtac_utils.definition_message obl.obl_name); + { obl with obl_body = Some (mkConst constant) } + let red = Reductionops.nf_betaiota let init_prog_info n b t deps fixkind notations obls impls kind hook = @@ -268,7 +287,7 @@ let init_prog_info n b t deps fixkind notations obls impls kind hook = (fun i (n, t, l, o, d) -> debug 2 (str "Adding obligation " ++ int i ++ str " with deps : " ++ str (string_of_intset d)); { obl_name = n ; obl_body = None; - obl_location = l; obl_type = red t; obl_opaque = o; + obl_location = l; obl_type = red t; obl_status = o; obl_deps = d }) obls in @@ -356,22 +375,16 @@ let has_dependencies obls n = !res let kind_of_opacity o = - if o then Subtac_utils.goal_proof_kind - else Subtac_utils.goal_kind - -let obligations_of_evars evars = - let arr = - Array.of_list - (List.map - (fun (n, t) -> - { obl_name = n; - obl_type = t; - obl_location = dummy_loc; - obl_body = None; - obl_opaque = false; - obl_deps = Intset.empty; - }) evars) - in arr, Array.length arr + match o with + | Define false | Expand -> Subtac_utils.goal_kind + | _ -> Subtac_utils.goal_proof_kind + +let not_transp_msg = + str "Obligation should be transparent but was declared opaque." ++ spc () ++ + str"Use 'Defined' instead." + +let warn_not_transp () = ppwarn not_transp_msg +let error_not_transp () = pperror not_transp_msg let rec solve_obligation prg num = let user_num = succ num in @@ -381,26 +394,37 @@ let rec solve_obligation prg num = pperror (str "Obligation" ++ spc () ++ int user_num ++ str "already" ++ spc() ++ str "solved.") else match deps_remaining obls obl.obl_deps with - [] -> - let obl = subst_deps_obl obls obl in - Command.start_proof obl.obl_name (kind_of_opacity obl.obl_opaque) obl.obl_type - (fun strength gr -> - debug 2 (str "Proof of obligation " ++ int user_num ++ str " finished"); - let obl = { obl with obl_body = Some (Libnames.constr_of_global gr) } in - let obls = Array.copy obls in - let _ = obls.(num) <- obl in - match update_obls prg obls (pred rem) with - | Remain n when n > 0 -> - if has_dependencies obls num then - ignore(auto_solve_obligations (Some prg.prg_name)) - | _ -> ()); - trace (str "Started obligation " ++ int user_num ++ str " proof: " ++ - Subtac_utils.my_print_constr (Global.env ()) obl.obl_type); - Pfedit.by !default_tactic; - Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) () - | l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) " - ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l)) - + | [] -> + let obl = subst_deps_obl obls obl in + Command.start_proof obl.obl_name (kind_of_opacity obl.obl_status) obl.obl_type + (fun strength gr -> + let cst = match gr with ConstRef cst -> cst | _ -> assert false in + let obl = + let transparent = evaluable_constant cst (Global.env ()) in + let body = + match obl.obl_status with + | Expand -> + if not transparent then error_not_transp () + else constant_value (Global.env ()) cst + | Define opaque -> + if not opaque && not transparent then error_not_transp () + else Libnames.constr_of_global gr + in { obl with obl_body = Some body } + in + let obls = Array.copy obls in + let _ = obls.(num) <- obl in + match update_obls prg obls (pred rem) with + | Remain n when n > 0 -> + if has_dependencies obls num then + ignore(auto_solve_obligations (Some prg.prg_name)) + | _ -> ()); + trace (str "Started obligation " ++ int user_num ++ str " proof: " ++ + Subtac_utils.my_print_constr (Global.env ()) obl.obl_type); + Pfedit.by !default_tactic; + Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) () + | l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) " + ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l)) + and subtac_obligation (user_num, name, typ) = let num = pred user_num in let prg = get_prog_err name in @@ -422,11 +446,8 @@ and solve_obligation_by_tac prg obls i tac = if deps_remaining obls obl.obl_deps = [] then let obl = subst_deps_obl obls obl in let t = Subtac_utils.solve_by_tac (evar_of_obligation obl) tac in - if obl.obl_opaque then - obls.(i) <- declare_obligation obl t - else - obls.(i) <- { obl with obl_body = Some t }; - true + obls.(i) <- declare_obligation obl t; + true else false with | Stdpp.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s))) @@ -473,21 +494,25 @@ let show_obligations ?(msg=true) n = let prg = get_prog_err n in let n = prg.prg_name in let obls, rem = prg.prg_obligations in + let showed = ref 5 in if msg then msgnl (int rem ++ str " obligation(s) remaining: "); Array.iteri (fun i x -> match x.obl_body with - None -> msgnl (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++ str "of" ++ spc() ++ str (string_of_id n) ++ str ":" ++ spc () ++ - my_print_constr (Global.env ()) x.obl_type ++ str "." ++ fnl ()) - | Some _ -> ()) + | None -> + if !showed > 0 then ( + decr showed; + msgnl (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++ str "of" ++ spc() ++ str (string_of_id n) ++ str ":" ++ spc () ++ + hov 1 (my_print_constr (Global.env ()) x.obl_type ++ str "." ++ fnl ()))) + | Some _ -> ()) obls - + let show_term n = let prg = get_prog_err n in let n = prg.prg_name in msgnl (str (string_of_id n) ++ spc () ++ str":" ++ spc () ++ my_print_constr (Global.env ()) prg.prg_type ++ spc () ++ str ":=" ++ fnl () ++ my_print_constr (Global.env ()) prg.prg_body) -let add_definition n b t ?(implicits=[]) ?(kind=Global,false,Definition) ?(hook=fun x -> ()) obls = +let add_definition n b t ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic ?(hook=fun x -> ()) obls = Flags.if_verbose pp (str (string_of_id n) ++ str " has type-checked"); let prg = init_prog_info n b t [] None [] obls implicits kind hook in let obls,_ = prg.prg_obligations in @@ -500,12 +525,16 @@ let add_definition n b t ?(implicits=[]) ?(kind=Global,false,Definition) ?(hook= let len = Array.length obls in let _ = Flags.if_verbose ppnl (str ", generating " ++ int len ++ str " obligation(s)") in from_prg := ProgMap.add n prg !from_prg; - let res = auto_solve_obligations (Some n) in + let res = + match tactic with + | None -> auto_solve_obligations (Some n) + | Some tac -> solve_obligations (Some n) tac + in match res with - | Remain rem when rem < 5 -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res - | _ -> res) + | Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res + | _ -> res) -let add_mutual_definitions l ?(kind=Global,false,Definition) notations fixkind = +let add_mutual_definitions l ?tactic ?(kind=Global,false,Definition) notations fixkind = let deps = List.map (fun (n, b, t, imps, obls) -> n) l in let upd = List.fold_left (fun acc (n, b, t, imps, obls) -> @@ -518,8 +547,13 @@ let add_mutual_definitions l ?(kind=Global,false,Definition) notations fixkind = List.fold_left (fun finished x -> if finished then finished else - match auto_solve_obligations (Some x) with - Defined _ -> (* If one definition is turned into a constant, the whole block is defined. *) true + let res = + match tactic with + | None -> auto_solve_obligations (Some x) + | Some tac -> solve_obligations (Some x) tac + in + match res with + | Defined _ -> (* If one definition is turned into a constant, the whole block is defined. *) true | _ -> false) false deps in () diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli index 6d13e3bd3..355ca7cd7 100644 --- a/contrib/subtac/subtac_obligations.mli +++ b/contrib/subtac/subtac_obligations.mli @@ -1,9 +1,10 @@ open Names open Util open Libnames +open Evd -type obligation_info = (Names.identifier * Term.types * loc * bool * Intset.t) array - (* ident, type, location, opaque or transparent, dependencies *) +type obligation_info = (identifier * Term.types * loc * obligation_definition_status * Intset.t) array + (* ident, type, location, opaque or transparent, expand or define dependencies *) type progress = (* Resolution status of a program *) | Remain of int (* n obligations remaining *) @@ -21,6 +22,7 @@ type definition_hook = global_reference -> unit val add_definition : Names.identifier -> Term.constr -> Term.types -> ?implicits:(Topconstr.explicitation * (bool * bool)) list -> ?kind:Decl_kinds.definition_kind -> + ?tactic:Proof_type.tactic -> ?hook:definition_hook -> obligation_info -> progress type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option) list @@ -28,6 +30,7 @@ type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option) val add_mutual_definitions : (Names.identifier * Term.constr * Term.types * (Topconstr.explicitation * (bool * bool)) list * obligation_info) list -> + ?tactic:Proof_type.tactic -> ?kind:Decl_kinds.definition_kind -> notations -> Command.fixpoint_kind -> unit diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml index bae2731aa..920b33b7a 100644 --- a/contrib/subtac/subtac_utils.ml +++ b/contrib/subtac/subtac_utils.ml @@ -159,7 +159,7 @@ let app_opt c e = let print_args env args = Array.fold_right (fun a acc -> my_print_constr env a ++ spc () ++ acc) args (str "") -let make_existential loc ?(opaque = true) env isevars c = +let make_existential loc ?(opaque = Define true) env isevars c = let evar = Evarutil.e_new_evar isevars env ~src:(loc, QuestionMark opaque) c in let (key, args) = destEvar evar in (try trace (str "Constructed evar " ++ int key ++ str " applied to args: " ++ @@ -470,4 +470,3 @@ let tactics_tac s = let tactics_call tac args = TacArg(TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force (tactics_tac tac)),args)) - diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli index 493352114..964f668f2 100644 --- a/contrib/subtac/subtac_utils.mli +++ b/contrib/subtac/subtac_utils.mli @@ -83,7 +83,8 @@ val wf_relations : (constr, constr lazy_t) Hashtbl.t type binders = local_binder list val app_opt : ('a -> 'a) option -> 'a -> 'a val print_args : env -> constr array -> std_ppcmds -val make_existential : loc -> ?opaque:bool -> env -> evar_defs ref -> types -> constr +val make_existential : loc -> ?opaque:obligation_definition_status -> + env -> evar_defs ref -> types -> constr val make_existential_expr : loc -> 'a -> 'b -> constr_expr val string_of_hole_kind : hole_kind -> string val evars_of_term : evar_map -> evar_map -> constr -> evar_map diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 26ed02379..be7c75663 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -940,7 +940,7 @@ let internalise sigma globalenv env allow_patvar lvar c = let p' = Option.map (intern_type env'') po in RIf (loc, c', (na', p'), intern env b1, intern env b2) | CHole (loc, k) -> - RHole (loc, match k with Some k -> k | None -> Evd.QuestionMark true) + RHole (loc, match k with Some k -> k | None -> Evd.QuestionMark (Evd.Define true)) | CPatVar (loc, n) when allow_patvar -> RPatVar (loc, n) | CPatVar (loc, _) -> diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4 index 44ca8eb2c..a796cef82 100644 --- a/parsing/q_constr.ml4 +++ b/parsing/q_constr.ml4 @@ -75,7 +75,7 @@ EXTEND | "0" [ s = sort -> <:expr< Rawterm.RSort ($dloc$,s) >> | id = ident -> <:expr< Rawterm.RVar ($dloc$,$id$) >> - | "_" -> <:expr< Rawterm.RHole ($dloc$, QuestionMark False) >> + | "_" -> <:expr< Rawterm.RHole ($dloc$, QuestionMark (Define False)) >> | "?"; id = ident -> <:expr< Rawterm.RPatVar($dloc$,(False,$id$)) >> | "{"; c1 = constr; "}"; "+"; "{"; c2 = constr; "}" -> apply_ref <:expr< coq_sumbool_ref >> [c1;c2] diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 270dac01a..b29afc0cb 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -400,10 +400,12 @@ let metamap_to_list m = (*************************) (* Unification state *) +type obligation_definition_status = Define of bool | Expand + type hole_kind = | ImplicitArg of global_reference * (int * identifier option) | BinderType of name - | QuestionMark of bool + | QuestionMark of obligation_definition_status | CasesType | InternalHole | TomatchTypeParameter of inductive * int diff --git a/pretyping/evd.mli b/pretyping/evd.mli index cb7429002..38db90dad 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -166,11 +166,16 @@ val empty_evar_defs : evar_defs val evars_of : evar_defs -> evar_map val evars_reset_evd : evar_map -> evar_defs -> evar_defs +(* Should the obligation be defined (opaque or transparent (default)) or + defined transparent and expanded in the term? *) + +type obligation_definition_status = Define of bool | Expand + (* Evars *) type hole_kind = | ImplicitArg of global_reference * (int * identifier option) | BinderType of name - | QuestionMark of bool (* Can it be turned into an obligation ? *) + | QuestionMark of obligation_definition_status | CasesType | InternalHole | TomatchTypeParameter of inductive * int diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml index a25fcd923..2be95056e 100644 --- a/tactics/decl_interp.ml +++ b/tactics/decl_interp.ml @@ -342,7 +342,7 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps = (fun (loc,(id,_)) -> RVar (loc,id)) params in let dum_args= - list_tabulate (fun _ -> RHole (dummy_loc,Evd.QuestionMark false)) + list_tabulate (fun _ -> RHole (dummy_loc,Evd.QuestionMark (Evd.Define false))) oib.Declarations.mind_nrealargs in raw_app(dummy_loc,rind,rparams@rparams_rec@dum_args) in let pat_vars,aliases,patt = interp_pattern env pat in -- cgit v1.2.3