diff options
Diffstat (limited to 'contrib/subtac/subtac_obligations.ml')
| -rw-r--r-- | contrib/subtac/subtac_obligations.ml | 246 |
1 files changed, 136 insertions, 110 deletions
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml index a393e2c9..cc1e2dde 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 @@ -13,9 +15,11 @@ open Decl_kinds open Util open Evd open Declare +open Proof_type 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,15 +29,17 @@ 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 + * Tacexpr.raw_tactic_expr option) 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; + obl_tac : Tacexpr.raw_tactic_expr option; } type obligations = (obligation array * int) @@ -79,22 +85,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 +163,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); @@ -188,7 +201,7 @@ let declare_definition prg = in let gr = ConstRef c in if Impargs.is_implicit_args () || prg.prg_implicits <> [] then - Impargs.declare_manual_implicits false gr (Impargs.is_implicit_args ()) prg.prg_implicits; + Impargs.declare_manual_implicits false gr prg.prg_implicits; print_message (Subtac_utils.definition_message prg.prg_name); prg.prg_hook gr; gr @@ -216,14 +229,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,41 +265,33 @@ 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) } - -let try_tactics obls = - Array.map - (fun obl -> - match obl.obl_body with - None -> - (try - let ev = evar_of_obligation obl in - let c = Subtac_utils.solve_by_tac ev Auto.default_full_auto in - declare_obligation obl c - with _ -> obl) - | _ -> obl) - obls - + 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 = let obls' = Array.mapi - (fun i (n, t, l, o, d) -> + (fun i (n, t, l, o, d, tac) -> 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_deps = d }) + obl_location = l; obl_type = red t; obl_status = o; + obl_deps = d; obl_tac = tac }) obls in { prg_name = n ; prg_body = b; prg_type = red t; prg_obligations = (obls', Array.length obls'); @@ -369,22 +378,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 @@ -394,26 +397,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) None) + | _ -> ()); + 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 @@ -434,12 +448,17 @@ and solve_obligation_by_tac prg obls i tac = (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 -> Tacinterp.interp t + | None -> !default_tactic + 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,34 +492,40 @@ and try_solve_obligation n prg tac = 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 : progress = +and auto_solve_obligations n tac : progress = Flags.if_verbose msgnl (str "Solving obligations automatically..."); - try solve_obligations n !default_tactic with NoObligations _ -> Dependent + try solve_prg_obligations (get_prog_err n) tac with NoObligations _ -> Dependent open Pp 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 () + 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 @@ -513,12 +538,12 @@ 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 = auto_solve_obligations (Some n) tactic 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) -> @@ -531,8 +556,9 @@ 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 = 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 () @@ -562,8 +588,8 @@ let next_obligation n = let prg = get_prog_err n in let obls, rem = prg.prg_obligations in let i = - array_find (fun x -> x.obl_body = None && deps_remaining obls x.obl_deps = []) - obls + 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 let default_tactic () = !default_tactic |