diff options
Diffstat (limited to 'contrib/subtac/subtac_obligations.ml')
| -rw-r--r-- | contrib/subtac/subtac_obligations.ml | 76 |
1 files changed, 44 insertions, 32 deletions
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml index 76f79443e1..941a7576e8 100644 --- a/contrib/subtac/subtac_obligations.ml +++ b/contrib/subtac/subtac_obligations.ml @@ -1,4 +1,3 @@ -(* -*- default-directory: "~/research/coq/trunk/" -*- *) open Printf open Pp open Subtac_utils @@ -140,10 +139,11 @@ let declare_definition prg = const_entry_opaque = false; const_entry_boxed = false} in - let _constant = Declare.declare_constant + let c = Declare.declare_constant prg.prg_name (DefinitionEntry ce,IsDefinition Definition) in - Subtac_utils.definition_message prg.prg_name + print_message (definition_message c); + c open Pp open Ppconstr @@ -171,12 +171,11 @@ let declare_mutual_definition l = const_entry_type = Some arrec.(i); const_entry_opaque = false; const_entry_boxed = true} in - let kn = Declare.declare_constant fi (DefinitionEntry ce,IsDefinition Fixpoint) - in - ConstRef kn + Declare.declare_constant fi (DefinitionEntry ce,IsDefinition Fixpoint) in let lrefrec = Array.mapi declare namerec in - Options.if_verbose ppnl (recursive_message lrefrec) + print_message (recursive_message lrefrec); + lrefrec.(0) let declare_obligation obl body = let ce = @@ -188,7 +187,7 @@ let declare_obligation obl body = let constant = Declare.declare_constant obl.obl_name (DefinitionEntry ce,IsProof Property) in - Subtac_utils.definition_message obl.obl_name; + print_message (definition_message constant); { obl with obl_body = Some (mkConst constant) } let try_tactics obls = @@ -241,7 +240,12 @@ let update_state s = (* msgnl (str "Updating obligations info"); *) Lib.add_anonymous_leaf (input s) -let obligations_message rem = +type progress = + | Remain of int + | Dependent + | Defined of constant + +let obligations_message rem = if rem > 0 then if rem = 1 then Options.if_verbose msgnl (int rem ++ str " obligation remaining") @@ -249,26 +253,31 @@ let obligations_message rem = Options.if_verbose msgnl (int rem ++ str " obligations remaining") else Options.if_verbose msgnl (str "No more obligations remaining") - + let update_obls prg obls rem = let prg' = { prg with prg_obligations = (obls, rem) } in from_prg := map_replace prg.prg_name prg' !from_prg; obligations_message rem; - if rem > 0 then () - else ( - match prg'.prg_deps with - [] -> - declare_definition prg'; - from_prg := ProgMap.remove prg.prg_name !from_prg - | 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 - (declare_mutual_definition progs; - from_prg := List.fold_left - (fun acc x -> - ProgMap.remove x.prg_name acc) !from_prg progs)); - update_state (!from_prg, !default_tactic_expr); - rem + let res = + if rem > 0 then Remain rem + else ( + match prg'.prg_deps with + [] -> + let kn = declare_definition prg' in + from_prg := ProgMap.remove prg.prg_name !from_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 + from_prg := List.fold_left + (fun acc x -> + ProgMap.remove x.prg_name acc) !from_prg progs; + Defined kn) + else Dependent); + in + update_state (!from_prg, !default_tactic_expr); + res let is_defined obls x = obls.(x).obl_body <> None @@ -312,8 +321,10 @@ let rec solve_obligation prg num = let obl = { obl with obl_body = Some (Libnames.constr_of_global gr) } in let obls = Array.copy obls in let _ = obls.(num) <- obl in - if update_obls prg obls (pred rem) <> 0 then - auto_solve_obligations (Some prg.prg_name)); + match update_obls prg obls (pred rem) with + Remain n when n > 0 -> + 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 @@ -378,9 +389,9 @@ and try_solve_obligation n prg tac = and try_solve_obligations n tac = try ignore (solve_obligations n tac) with NoObligations _ -> () -and auto_solve_obligations n : unit = +and auto_solve_obligations n : progress = Options.if_verbose msgnl (str "Solving obligations automatically..."); - try_solve_obligations n !default_tactic + try solve_obligations n !default_tactic with NoObligations _ -> Dependent let add_definition n b t obls = Options.if_verbose pp (str (string_of_id n) ++ str " has type-checked"); @@ -388,8 +399,9 @@ let add_definition n b t obls = let obls,_ = prg.prg_obligations in if Array.length obls = 0 then ( Options.if_verbose ppnl (str "."); - declare_definition prg; - from_prg := ProgMap.remove prg.prg_name !from_prg) + let cst = declare_definition prg in + from_prg := ProgMap.remove prg.prg_name !from_prg; + Defined cst) else ( let len = Array.length obls in let _ = Options.if_verbose ppnl (str ", generating " ++ int len ++ str " obligation(s)") in @@ -405,7 +417,7 @@ let add_mutual_definitions l nvrec = !from_prg l in from_prg := upd; - List.iter (fun x -> auto_solve_obligations (Some x)) deps + List.iter (fun x -> ignore(auto_solve_obligations (Some x))) deps let admit_obligations n = let prg = get_prog_err n in |