diff options
Diffstat (limited to 'contrib/subtac/subtac_obligations.ml')
| -rw-r--r-- | contrib/subtac/subtac_obligations.ml | 249 |
1 files changed, 249 insertions, 0 deletions
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml new file mode 100644 index 00000000..7b13b402 --- /dev/null +++ b/contrib/subtac/subtac_obligations.ml @@ -0,0 +1,249 @@ +open Printf +open Pp +open Subtac_utils + +open Term +open Names +open Libnames +open Summary +open Libobject +open Entries +open Decl_kinds +open Util +open Evd + +type obligation = + { obl_name : identifier; + obl_type : types; + obl_body : constr option; + obl_deps : Intset.t; + } + +type obligations = (obligation array * int) + +type program_info = { + prg_name: identifier; + prg_body: constr; + prg_type: types; + prg_obligations: obligations; +} + +let evar_of_obligation o = { evar_hyps = Environ.empty_named_context_val ; + evar_concl = o.obl_type ; + evar_body = Evar_empty ; + evar_extra = None } + +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_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 _ = + Summary.declare_summary "program-tcc-table" + { Summary.freeze_function = (fun () -> !from_prg); + Summary.unfreeze_function = + (fun v -> from_prg := v); + Summary.init_function = + (fun () -> from_prg := ProgMap.empty); + Summary.survive_module = false; + Summary.survive_section = false } + +let declare_definition prg = +(* let obls_constrs = + Array.fold_right (fun x acc -> (out_some x.obl_evar.evar_body) :: acc) (fst prg.prg_obligations) [] + in*) + let ce = + { const_entry_body = prg.prg_body; + const_entry_type = Some prg.prg_type; + const_entry_opaque = false; + const_entry_boxed = false} + in + let _constant = Declare.declare_constant + prg.prg_name (DefinitionEntry ce,IsDefinition Definition) + in + Subtac_utils.definition_message prg.prg_name + +open Evd + +let terms_of_evar ev = + match ev.evar_body with + Evar_defined b -> + let nc = Environ.named_context_of_val ev.evar_hyps in + let body = Termops.it_mkNamedLambda_or_LetIn b nc in + let typ = Termops.it_mkNamedProd_or_LetIn ev.evar_concl nc in + body, typ + | _ -> assert(false) + +let declare_obligation obl body = + let ce = + { const_entry_body = body; + const_entry_type = Some obl.obl_type; + const_entry_opaque = true; + const_entry_boxed = false} + in + let constant = Declare.declare_constant obl.obl_name (DefinitionEntry ce,IsProof Property) + in + 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 + +let add_entry n b t obls = + Options.if_verbose pp (str (string_of_id n) ++ str " has type-checked"); + let init_obls e = + Array.map + (fun (n, t, d) -> + { obl_name = n ; obl_body = None; obl_type = t; obl_deps = d }) + e + in + if Array.length obls = 0 then ( + Options.if_verbose ppnl (str "."); + declare_definition { prg_name = n ; prg_body = b ; prg_type = t ; prg_obligations = ([||], 0) } ) + else ( + let len = Array.length obls in + let _ = Options.if_verbose ppnl (str ", generating " ++ int len ++ str " obligation(s)") in + let obls = init_obls obls in + let rem = Array.fold_left (fun acc obl -> if obl.obl_body = None then succ acc else acc) 0 obls in + let prg = { prg_name = n ; prg_body = b ; prg_type = t ; prg_obligations = (obls, rem) } in + if rem < len then + Options.if_verbose ppnl (int rem ++ str " obligation(s) remaining."); + if rem = 0 then + declare_definition prg + else + from_prg := ProgMap.add n prg !from_prg) + +let error s = Util.error s + +let get_prog name = + let prg_infos = !from_prg in + match name with + Some n -> ProgMap.find n prg_infos + | None -> + (let n = map_cardinal prg_infos in + match n with + 0 -> error "No obligations remaining" + | 1 -> map_first prg_infos + | _ -> error "More than one program with unsolved obligations") + +let update_obls prg obls rem = + let prg' = { prg with prg_obligations = (obls, rem) } in + if rem > 1 then ( + debug 2 (int rem ++ str " obligations remaining"); + from_prg := map_replace prg.prg_name prg' !from_prg) + else ( + declare_definition prg'; + from_prg := ProgMap.remove prg.prg_name !from_prg + ) + +let is_defined obls x = obls.(x).obl_body <> None + +let deps_remaining obls x = + let deps = obls.(x).obl_deps in + Intset.fold + (fun x acc -> + if is_defined obls x then acc + else x :: acc) + deps [] + +let subst_deps obls obl = + let t' = + Intset.fold + (fun x acc -> + let xobl = obls.(x) in + let oblb = out_some xobl.obl_body in + Term.subst1 oblb (Term.subst_var xobl.obl_name acc)) + obl.obl_deps obl.obl_type + in { obl with obl_type = t' } + +let subtac_obligation (user_num, name) = + let num = pred user_num in + let prg = get_prog 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 -> + (match deps_remaining obls num with + [] -> + let obl = subst_deps obls obl in + Command.start_proof obl.obl_name Subtac_utils.goal_proof_kind 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 + update_obls prg obls (pred rem)); + trace (str "Started obligation " ++ int user_num ++ str " proof") + | l -> msgnl (str "Obligation " ++ int user_num ++ str " depends on obligation(s) " + ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l))) + | Some r -> error "Obligation already solved" + else error (sprintf "Unknown obligation number %i" (succ num)) + + +let obligations_of_evars evars = + let arr = + Array.of_list + (List.map + (fun (n, t) -> + { obl_name = n; + obl_type = t; + obl_body = None; + obl_deps = Intset.empty; + }) evars) + in arr, Array.length arr + +let solve_obligations n tac = + let prg = get_prog n in + let obls, rem = prg.prg_obligations in + let rem = ref rem in + let obls' = + Array.map (fun x -> + match x.obl_body with + Some _ -> x + | None -> + try + let t = Subtac_utils.solve_by_tac (evar_of_obligation x) tac in + decr rem; + { x with obl_body = Some t } + with _ -> x) + obls + in + update_obls prg obls' !rem + +open Pp +let show_obligations n = + let prg = get_prog n in + let obls, rem = prg.prg_obligations in + msgnl (int rem ++ str " obligation(s) remaining: "); + Array.iteri (fun i x -> + match x.obl_body with + None -> msgnl (int (succ i) ++ str " : " ++ spc () ++ + my_print_constr (Global.env ()) x.obl_type) + | Some _ -> ()) + obls + |