diff options
Diffstat (limited to 'plugins/subtac/subtac_obligations.ml')
| -rw-r--r-- | plugins/subtac/subtac_obligations.ml | 699 |
1 files changed, 0 insertions, 699 deletions
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml deleted file mode 100644 index 7a4916fa..00000000 --- a/plugins/subtac/subtac_obligations.ml +++ /dev/null @@ -1,699 +0,0 @@ -open Printf -open Pp -open Subtac_utils -open Command -open Environ - -open Term -open Names -open Libnames -open Summary -open Libobject -open Entries -open Decl_kinds -open Util -open Evd -open Declare -open Proof_type -open Compat - -let ppwarn cmd = Pp.warn (str"Program:" ++ cmd) -let pperror cmd = Util.errorlabstrm "Program" cmd -let error s = pperror (str s) - -let reduce c = - Reductionops.clos_norm_flags Closure.betaiota (Global.env ()) Evd.empty c - -exception NoObligations of identifier option - -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 * hole_kind located * - obligation_definition_status * Intset.t * tactic option) array - -type obligation = - { obl_name : identifier; - obl_type : types; - obl_location : hole_kind located; - obl_body : constr option; - obl_status : obligation_definition_status; - obl_deps : Intset.t; - obl_tac : tactic option; - } - -type obligations = (obligation array * int) - -type fixpoint_kind = - | IsFixpoint of (identifier located option * Topconstr.recursion_order_expr) list - | IsCoFixpoint - -type notations = (Vernacexpr.lstring * Topconstr.constr_expr * Topconstr.scope_name option) list - -type program_info = { - prg_name: identifier; - prg_body: constr; - prg_type: constr; - prg_obligations: obligations; - prg_deps : identifier list; - prg_fixkind : fixpoint_kind option ; - prg_implicits : (Topconstr.explicitation * (bool * bool * bool)) list; - prg_notations : notations ; - prg_kind : definition_kind; - prg_reduce : constr -> constr; - prg_hook : Tacexpr.declaration_hook; -} - -let assumption_message id = - Flags.if_verbose message ((string_of_id id) ^ " is assumed") - -let (set_default_tactic, get_default_tactic, print_default_tactic) = - Tactic_option.declare_tactic_option "Program tactic" - -(* true = All transparent, false = Opaque if possible *) -let proofs_transparency = ref true - -let set_proofs_transparency = (:=) proofs_transparency -let get_proofs_transparency () = !proofs_transparency - -open Goptions - -let _ = - declare_bool_option - { optsync = true; - optdepr = false; - optname = "transparency of Program obligations"; - optkey = ["Transparent";"Obligations"]; - optread = get_proofs_transparency; - optwrite = set_proofs_transparency; } - -(* true = hide obligations *) -let hide_obligations = ref false - -let set_hide_obligations = (:=) hide_obligations -let get_hide_obligations () = !hide_obligations - -open Goptions - -let _ = - declare_bool_option - { optsync = true; - optdepr = false; - optname = "Hidding of Program obligations"; - optkey = ["Hide";"Obligations"]; - optread = get_hide_obligations; - optwrite = set_hide_obligations; } - -let evar_of_obligation o = make_evar (Global.named_context_val ()) o.obl_type - -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 obl_substitution expand obls deps = - Intset.fold - (fun x acc -> - let xobl = obls.(x) in - let oblb = - try get_obligation_body expand xobl - with e when Errors.noncritical e -> assert(false) - in (xobl.obl_name, (xobl.obl_type, oblb)) :: acc) - deps [] - -let subst_deps expand obls deps t = - let subst = obl_substitution expand obls deps in - Term.replace_vars (List.map (fun (n, (_, b)) -> n, b) subst) t - -let rec prod_app t n = - match kind_of_term (strip_outer_cast t) with - | Prod (_,_,b) -> subst1 n b - | LetIn (_, b, t, b') -> prod_app (subst1 b b') n - | _ -> - errorlabstrm "prod_app" - (str"Needed a product, but didn't find one" ++ fnl ()) - - -(* prod_appvect T [| a1 ; ... ; an |] -> (T a1 ... an) *) -let prod_applist t nL = List.fold_left prod_app t nL - -let replace_appvars subst = - let rec aux c = - let f, l = decompose_app c in - if isVar f then - try - let c' = List.map (map_constr aux) l in - let (t, b) = List.assoc (destVar f) subst in - mkApp (delayed_force hide_obligation, - [| prod_applist t c'; applistc b c' |]) - with Not_found -> map_constr aux c - else map_constr aux c - in map_constr aux - -let subst_prog expand obls ints prg = - let subst = obl_substitution expand obls ints in - if get_hide_obligations () then - (replace_appvars subst prg.prg_body, - replace_appvars subst (Termops.refresh_universes prg.prg_type)) - else - let subst' = List.map (fun (n, (_, b)) -> n, b) subst in - (Term.replace_vars subst' prg.prg_body, - Term.replace_vars subst' (Termops.refresh_universes prg.prg_type)) - -let subst_deps_obl obls obl = - let t' = subst_deps true 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) - -let map_replace k v m = ProgMap.add k v (ProgMap.remove k m) - -let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m [] - -let map_cardinal m = - let i = ref 0 in - ProgMap.iter (fun _ _ -> incr i) m; - !i - -exception Found of program_info - -let map_first m = - try - ProgMap.iter (fun _ v -> raise (Found v)) m; - assert(false) - with Found x -> x - -let from_prg : program_info ProgMap.t ref = ref ProgMap.empty - -let freeze () = !from_prg -let unfreeze v = from_prg := v -let init () = from_prg := ProgMap.empty - -(** Beware: if this code is dynamically loaded via dynlink after the start - of Coq, then this [init] function will not be run by [Lib.init ()]. - Luckily, here we can launch [init] at load-time. *) - -let _ = init () - -let _ = - Summary.declare_summary "program-tcc-table" - { Summary.freeze_function = freeze; - Summary.unfreeze_function = unfreeze; - Summary.init_function = init } - -let progmap_union = ProgMap.fold ProgMap.add - -let close sec = - if not (ProgMap.is_empty !from_prg) then - let keys = map_keys !from_prg in - errorlabstrm "Program" (str "Unsolved obligations when closing " ++ str sec ++ str":" ++ spc () ++ - prlist_with_sep spc (fun x -> Nameops.pr_id x) keys ++ - (str (if List.length keys = 1 then " has " else "have ") ++ - str "unsolved obligations")) - -let input : program_info ProgMap.t -> obj = - declare_object - { (default_object "Program state") with - cache_function = (fun (na, pi) -> from_prg := pi); - load_function = (fun _ (_, pi) -> from_prg := pi); - discharge_function = (fun _ -> close "section"; None); - classify_function = (fun _ -> close "module"; Dispose) } - -open Evd - -let progmap_remove prg = - Lib.add_anonymous_leaf (input (ProgMap.remove prg.prg_name !from_prg)) - -let progmap_add n prg = - Lib.add_anonymous_leaf (input (ProgMap.add n prg !from_prg)) - -let progmap_replace prg' = - Lib.add_anonymous_leaf (input (map_replace prg'.prg_name prg' !from_prg)) - -let rec intset_to = function - -1 -> Intset.empty - | n -> Intset.add n (intset_to (pred n)) - -let subst_body expand prg = - let obls, _ = prg.prg_obligations in - let ints = intset_to (pred (Array.length obls)) in - subst_prog expand obls ints prg - -let declare_definition prg = - let body, typ = subst_body true prg in - let (local, kind) = prg.prg_kind in - let ce = - { const_entry_body = body; - const_entry_secctx = None; - const_entry_type = Some typ; - const_entry_opaque = false } - in - (Command.get_declare_definition_hook ()) ce; - match local with - | Local when Lib.sections_are_opened () -> - let c = - SectionLocalDef(ce.const_entry_body,ce.const_entry_type,false) in - let _ = declare_variable prg.prg_name (Lib.cwd(),c,IsDefinition kind) in - print_message (Subtac_utils.definition_message prg.prg_name); - if Pfedit.refining () then - Flags.if_verbose msg_warning - (str"Local definition " ++ Nameops.pr_id prg.prg_name ++ - str" is not visible from current goals"); - progmap_remove prg; - VarRef prg.prg_name - | (Global|Local) -> - let c = - Declare.declare_constant - prg.prg_name (DefinitionEntry ce,IsDefinition (snd prg.prg_kind)) - in - let gr = ConstRef c in - if Impargs.is_implicit_args () || prg.prg_implicits <> [] then - Impargs.declare_manual_implicits false gr [prg.prg_implicits]; - print_message (Subtac_utils.definition_message prg.prg_name); - progmap_remove prg; - prg.prg_hook local gr; - gr - -open Pp -open Ppconstr - -let rec lam_index n t acc = - match kind_of_term t with - | Lambda (na, _, b) -> - if na = Name n then acc - else lam_index n b (succ acc) - | _ -> raise Not_found - -let compute_possible_guardness_evidences (n,_) fixbody fixtype = - match n with - | Some (loc, n) -> [lam_index n fixbody 0] - | None -> - (* If recursive argument was not given by user, we try all args. - An earlier approach was to look only for inductive arguments, - but doing it properly involves delta-reduction, and it finally - doesn't seem to worth the effort (except for huge mutual - fixpoints ?) *) - let m = Term.nb_prod fixtype in - let ctx = fst (decompose_prod_n_assum m fixtype) in - list_map_i (fun i _ -> i) 0 ctx - -let declare_mutual_definition l = - let len = List.length l in - let first = List.hd l in - let fixdefs, fixtypes, fiximps = - list_split3 - (List.map (fun x -> - let subs, typ = (subst_body true x) in - let term = snd (Reductionops.splay_lam_n (Global.env ()) Evd.empty len subs) in - let typ = snd (Reductionops.splay_prod_n (Global.env ()) Evd.empty len typ) in - x.prg_reduce term, x.prg_reduce typ, x.prg_implicits) l) - in -(* let fixdefs = List.map reduce_fix fixdefs in *) - let fixkind = Option.get first.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 - let (local,kind) = first.prg_kind in - let fixnames = first.prg_deps in - let kind = if fixkind <> IsCoFixpoint then Fixpoint else CoFixpoint in - let indexes, fixdecls = - match fixkind with - | IsFixpoint wfl -> - let possible_indexes = - list_map3 compute_possible_guardness_evidences wfl fixdefs fixtypes in - let indexes = Pretyping.search_guard dummy_loc (Global.env ()) possible_indexes fixdecls in - Some indexes, list_map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 l - | IsCoFixpoint -> - None, list_map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 l - in - (* Declare the recursive definitions *) - let kns = list_map4 (declare_fix kind) fixnames fixdecls fixtypes fiximps in - (* Declare notations *) - List.iter Metasyntax.add_notation_interpretation first.prg_notations; - Declare.recursive_message (fixkind<>IsCoFixpoint) indexes fixnames; - let gr = List.hd kns in - let kn = match gr with ConstRef kn -> kn | _ -> assert false in - first.prg_hook local gr; - List.iter progmap_remove l; kn - -let declare_obligation prg obl body = - let body = prg.prg_reduce body in - let ty = prg.prg_reduce obl.obl_type in - match obl.obl_status with - | Expand -> { obl with obl_body = Some body } - | Define opaque -> - let opaque = if get_proofs_transparency () then false else opaque in - let ce = - { const_entry_body = body; - const_entry_secctx = None; - const_entry_type = Some ty; - const_entry_opaque = opaque } - in - let constant = Declare.declare_constant obl.obl_name - (DefinitionEntry ce,IsProof Property) - in - if not opaque then - Auto.add_hints false [string_of_id prg.prg_name] - (Auto.HintsUnfoldEntry [EvalConstRef constant]); - print_message (Subtac_utils.definition_message obl.obl_name); - { obl with obl_body = Some (mkConst constant) } - -let init_prog_info n b t deps fixkind notations obls impls kind reduce hook = - let obls', b = - match b with - | None -> - assert(obls = [||]); - let n = Nameops.add_suffix n "_obligation" in - [| { obl_name = n; obl_body = None; - obl_location = dummy_loc, InternalHole; obl_type = t; - obl_status = Expand; obl_deps = Intset.empty; obl_tac = None } |], - mkVar n - | Some b -> - Array.mapi - (fun i (n, t, l, o, d, tac) -> - { obl_name = n ; obl_body = None; - obl_location = l; obl_type = reduce t; obl_status = o; - obl_deps = d; obl_tac = tac }) - obls, b - in - { prg_name = n ; prg_body = b; prg_type = reduce t; prg_obligations = (obls', Array.length obls'); - prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ; - prg_implicits = impls; prg_kind = kind; prg_reduce = reduce; prg_hook = hook; } - -let get_prog name = - let prg_infos = !from_prg in - match name with - Some n -> - (try ProgMap.find n prg_infos - with Not_found -> raise (NoObligations (Some n))) - | None -> - (let n = map_cardinal prg_infos in - match n with - 0 -> raise (NoObligations None) - | 1 -> map_first prg_infos - | _ -> error "More than one program with unsolved obligations") - -let get_prog_err n = - try get_prog n with NoObligations id -> pperror (explain_no_obligations id) - -let obligations_solved prg = (snd prg.prg_obligations) = 0 - -let all_programs () = - ProgMap.fold (fun k p l -> p :: l) !from_prg [] - -type progress = - | Remain of int - | Dependent - | Defined of global_reference - -let obligations_message rem = - if rem > 0 then - if rem = 1 then - Flags.if_verbose msgnl (int rem ++ str " obligation remaining") - else - Flags.if_verbose msgnl (int rem ++ str " obligations remaining") - else - Flags.if_verbose msgnl (str "No more obligations remaining") - -let update_obls prg obls rem = - let prg' = { prg with prg_obligations = (obls, rem) } in - progmap_replace prg'; - obligations_message rem; - if rem > 0 then Remain rem - else ( - match prg'.prg_deps with - | [] -> - let kn = declare_definition prg' in - progmap_remove prg'; - Defined kn - | l -> - let progs = List.map (fun x -> ProgMap.find x !from_prg) prg'.prg_deps in - if List.for_all (fun x -> obligations_solved x) progs then - let kn = declare_mutual_definition progs in - Defined (ConstRef kn) - else Dependent) - -let is_defined obls x = obls.(x).obl_body <> None - -let deps_remaining obls deps = - Intset.fold - (fun x acc -> - if is_defined obls x then acc - else x :: acc) - deps [] - -let dependencies obls n = - let res = ref Intset.empty in - Array.iteri - (fun i obl -> - if i <> n && Intset.mem n obl.obl_deps then - res := Intset.add i !res) - obls; - !res - -let kind_of_opacity o = - 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 tac = - let user_num = succ num in - let obls, rem = prg.prg_obligations in - let obl = obls.(num) in - if obl.obl_body <> None then - 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 - Lemmas.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 - if transparent then - Auto.add_hints true [string_of_id prg.prg_name] - (Auto.HintsUnfoldEntry [EvalConstRef cst]); - { obl with obl_body = Some body } - in - let obls = Array.copy obls in - let _ = obls.(num) <- obl in - let res = try update_obls prg obls (pred rem) - with e when Errors.noncritical e -> - pperror (Errors.print (Cerrors.process_vernac_interp_error e)) - in - match res with - | Remain n when n > 0 -> - let deps = dependencies obls num in - if deps <> Intset.empty then - ignore(auto_solve_obligations (Some prg.prg_name) None ~oblset:deps) - | _ -> ()); - trace (str "Started obligation " ++ int user_num ++ str " proof: " ++ - Subtac_utils.my_print_constr (Global.env ()) obl.obl_type); - Pfedit.by (snd (get_default_tactic ())); - Option.iter (fun tac -> Pfedit.set_end_tac (Tacinterp.interp tac)) tac; - 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) tac = - let num = pred user_num in - let prg = get_prog_err name in - let obls, rem = prg.prg_obligations in - if num < Array.length obls then - let obl = obls.(num) in - match obl.obl_body with - None -> solve_obligation prg num tac - | Some r -> error "Obligation already solved" - else error (sprintf "Unknown obligation number %i" (succ num)) - - -and solve_obligation_by_tac prg obls i tac = - let obl = obls.(i) in - match obl.obl_body with - | Some _ -> false - | None -> - try - if deps_remaining obls obl.obl_deps = [] then - let obl = subst_deps_obl obls obl in - let tac = - match tac with - | Some t -> t - | None -> - match obl.obl_tac with - | Some t -> t - | None -> snd (get_default_tactic ()) - in - let t = Subtac_utils.solve_by_tac (evar_of_obligation obl) tac in - obls.(i) <- declare_obligation prg obl t; - true - else false - with - | Loc.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s))) - | Loc.Exc_located(_, Refiner.FailError (_, s)) - | Refiner.FailError (_, s) -> - user_err_loc (fst obl.obl_location, "solve_obligation", Lazy.force s) - | Util.Anomaly _ as e -> raise e - | e when Errors.noncritical e -> false - -and solve_prg_obligations prg ?oblset tac = - let obls, rem = prg.prg_obligations in - let rem = ref rem in - let obls' = Array.copy obls in - let set = ref Intset.empty in - let p = match oblset with - | None -> (fun _ -> true) - | Some s -> set := s; - (fun i -> Intset.mem i !set) - in - let _ = - Array.iteri (fun i x -> - if p i && solve_obligation_by_tac prg obls' i tac then - let deps = dependencies obls i in - (set := Intset.union !set deps; - decr rem)) - obls' - in - update_obls prg obls' !rem - -and solve_obligations n tac = - let prg = get_prog_err n in - solve_prg_obligations prg tac - -and solve_all_obligations tac = - ProgMap.iter (fun k v -> ignore(solve_prg_obligations v tac)) !from_prg - -and try_solve_obligation n prg tac = - let prg = get_prog prg in - let obls, rem = prg.prg_obligations in - let obls' = Array.copy obls in - if solve_obligation_by_tac prg obls' n tac then - ignore(update_obls prg obls' (pred rem)); - -and try_solve_obligations n tac = - try ignore (solve_obligations n tac) with NoObligations _ -> () - -and auto_solve_obligations n ?oblset tac : progress = - Flags.if_verbose msgnl (str "Solving obligations automatically..."); - try solve_prg_obligations (get_prog_err n) ?oblset tac with NoObligations _ -> Dependent - -open Pp -let show_obligations_of_prg ?(msg=true) prg = - 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 -> - 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_obligations ?(msg=true) n = - let progs = match n with - | None -> all_programs () - | Some n -> - try [ProgMap.find n !from_prg] - with Not_found -> raise (NoObligations (Some n)) - in List.iter (show_obligations_of_prg ~msg) progs - -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 ?term t ?(implicits=[]) ?(kind=Global,Definition) ?tactic - ?(reduce=reduce) ?(hook=fun _ _ -> ()) obls = - Flags.if_verbose pp (str (string_of_id n) ++ str " has type-checked"); - let prg = init_prog_info n term t [] None [] obls implicits kind reduce hook in - let obls,_ = prg.prg_obligations in - if Array.length obls = 0 then ( - Flags.if_verbose ppnl (str "."); - let cst = declare_definition prg in - Defined cst) - else ( - let len = Array.length obls in - let _ = Flags.if_verbose ppnl (str ", generating " ++ int len ++ str " obligation(s)") in - progmap_add n prg; - let res = auto_solve_obligations (Some n) tactic in - match res with - | Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res - | _ -> res) - -let add_mutual_definitions l ?tactic ?(kind=Global,Definition) ?(reduce=reduce) - ?(hook=fun _ _ -> ()) notations fixkind = - let deps = List.map (fun (n, b, t, imps, obls) -> n) l in - List.iter - (fun (n, b, t, imps, obls) -> - let prg = init_prog_info n (Some b) t deps (Some fixkind) - notations obls imps kind reduce hook - in progmap_add n prg) l; - let _defined = - List.fold_left (fun finished x -> - if finished then finished - else - let res = auto_solve_obligations (Some x) tactic in - match res with - | Defined _ -> (* If one definition is turned into a constant, the whole block is defined. *) true - | _ -> false) - false deps - in () - -let admit_obligations n = - let prg = get_prog_err n in - let obls, rem = prg.prg_obligations in - let obls = Array.copy obls in - Array.iteri - (fun i x -> - match x.obl_body with - | None -> - let x = subst_deps_obl obls x in - let kn = Declare.declare_constant x.obl_name - (ParameterEntry (None, x.obl_type,None), IsAssumption Conjectural) - in - assumption_message x.obl_name; - obls.(i) <- { x with obl_body = Some (mkConst kn) } - | Some _ -> ()) - obls; - ignore(update_obls prg obls 0) - -exception Found of int - -let array_find f arr = - try Array.iteri (fun i x -> if f x then raise (Found i)) arr; - raise Not_found - with Found i -> i - -let next_obligation n tac = - let prg = get_prog_err n in - let obls, rem = prg.prg_obligations in - let i = - try array_find (fun x -> x.obl_body = None && deps_remaining obls x.obl_deps = []) obls - with Not_found -> anomaly "Could not find a solvable obligation." - in solve_obligation prg i tac |