diff options
author | 2006-10-31 16:45:46 +0000 | |
---|---|---|
committer | 2006-10-31 16:45:46 +0000 | |
commit | cec87055e59a80091416a57d0687ae4199860756 (patch) | |
tree | 871bbb6fec918def59864d3860f2a276ce442a87 | |
parent | 69c2964cf2a7eb49a83f70947d9ead1ef61f7557 (diff) |
Debug obligation handling code
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9329 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | contrib/subtac/eterm.ml | 8 | ||||
-rw-r--r-- | contrib/subtac/subtac_obligations.ml | 112 | ||||
-rw-r--r-- | contrib/subtac/subtac_utils.ml | 5 | ||||
-rw-r--r-- | contrib/subtac/subtac_utils.mli | 2 |
4 files changed, 92 insertions, 35 deletions
diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml index b95f643a5..790e61a0a 100644 --- a/contrib/subtac/eterm.ml +++ b/contrib/subtac/eterm.ml @@ -125,12 +125,12 @@ let trunc_named_context n ctx = let eterm_obligations name nclen evm t tycon = (* 'Serialize' the evars, we assume that the types of the existentials refer to previous existentials in the list only *) - let evl = to_list evm in + let evl = List.rev (to_list evm) in trace (str "Eterm, transformed to list"); let evn = let i = ref (-1) in - List.map (fun (id, ev) -> incr i; - (id, (!i, id_of_string (string_of_id name ^ "_obligation_" ^ string_of_int !i)), ev)) evl + List.rev_map (fun (id, ev) -> incr i; + (id, (!i, id_of_string (string_of_id name ^ "_obligation_" ^ string_of_int (succ !i))), ev)) evl in let evts = (* Remove existential variables in types and build the corresponding products *) @@ -163,7 +163,7 @@ let eterm_obligations name nclen evm t tycon = Termops.print_constr_env (Global.env ()) typ)) evars); with _ -> ()); - Array.of_list evars, t' + Array.of_list (List.rev evars), t' let mkMetas n = let rec aux i acc = diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml index 26a195e3d..7b13b4023 100644 --- a/contrib/subtac/subtac_obligations.ml +++ b/contrib/subtac/subtac_obligations.ml @@ -10,10 +10,11 @@ open Libobject open Entries open Decl_kinds open Util +open Evd type obligation = { obl_name : identifier; - obl_type : types; + obl_type : types; obl_body : constr option; obl_deps : Intset.t; } @@ -27,6 +28,11 @@ type program_info = { 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) @@ -57,9 +63,9 @@ let _ = Summary.survive_section = false } let declare_definition prg = - let obls_constrs = - Array.fold_right (fun x acc -> (out_some x.obl_body) :: acc) (fst prg.prg_obligations) [] - in +(* 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; @@ -72,21 +78,47 @@ let declare_definition prg = 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 try_tactics e = + let init_obls e = Array.map (fun (n, t, d) -> - let ev = { evar_concl = t ; evar_body = Evar_empty ; - evar_hyps = Environ.empty_named_context_val ; evar_extra = None } - in - let cstr = - try - let c = Subtac_utils.solve_by_tac ev Auto.default_full_auto in - Some c - with _ -> None - in { obl_name = n ; obl_type = t; obl_body = cstr; obl_deps = d }) + { obl_name = n ; obl_body = None; obl_type = t; obl_deps = d }) e in if Array.length obls = 0 then ( @@ -95,7 +127,7 @@ let add_entry n b t obls = else ( let len = Array.length obls in let _ = Options.if_verbose ppnl (str ", generating " ++ int len ++ str " obligation(s)") in - let obls = try_tactics obls 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 @@ -128,6 +160,26 @@ let update_obls prg obls rem = 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 @@ -136,14 +188,19 @@ let subtac_obligation (user_num, name) = let obl = obls.(num) in match obl.obl_body with None -> - 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") + (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)) @@ -160,13 +217,6 @@ let obligations_of_evars evars = }) evars) in arr, Array.length arr -let evar_of_obligation o = { evar_hyps = Environ.empty_named_context_val ; - evar_concl = o.obl_type ; - evar_body = Evar_empty ; - evar_extra = None } - - - let solve_obligations n tac = let prg = get_prog n in let obls, rem = prg.prg_obligations in @@ -192,7 +242,7 @@ let show_obligations n = msgnl (int rem ++ str " obligation(s) remaining: "); Array.iteri (fun i x -> match x.obl_body with - None -> msgnl (int i ++ str " : " ++ spc () ++ + None -> msgnl (int (succ i) ++ str " : " ++ spc () ++ my_print_constr (Global.env ()) x.obl_type) | Some _ -> ()) obls diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml index 3248ed30d..7b96758ad 100644 --- a/contrib/subtac/subtac_utils.ml +++ b/contrib/subtac/subtac_utils.ml @@ -447,3 +447,8 @@ let solve_by_tac ev t = let c = Tacmach.extract_pftreestate solved_state in debug 1 (str "Term constructed in solve by tac: " ++ my_print_constr (Global.env ()) c); c + +let rec string_of_list sep f = function + [] -> "" + | x :: [] -> f x + | x :: ((y :: _) as tl) -> f x ^ sep ^ string_of_list sep f tl diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli index c8afd9f8b..ebfc51232 100644 --- a/contrib/subtac/subtac_utils.mli +++ b/contrib/subtac/subtac_utils.mli @@ -96,3 +96,5 @@ val definition_message : identifier -> unit val recursive_message : global_reference array -> std_ppcmds val solve_by_tac : evar_info -> Tacmach.tactic -> constr + +val string_of_list : string -> ('a -> string) -> 'a list -> string |