summaryrefslogtreecommitdiff
path: root/contrib/subtac/subtac_utils.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
commit208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch)
tree591e9e512063e34099782e2518573f15ffeac003 /contrib/subtac/subtac_utils.ml
parentde0085539583f59dc7c4bf4e272e18711d565466 (diff)
Imported Upstream version 8.1~gammaupstream/8.1.gamma
Diffstat (limited to 'contrib/subtac/subtac_utils.ml')
-rw-r--r--contrib/subtac/subtac_utils.ml72
1 files changed, 43 insertions, 29 deletions
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index d4db7c27..7b96758a 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -80,25 +80,34 @@ open Pp
let my_print_constr = Termops.print_constr_env
let my_print_constr_expr = Ppconstr.pr_constr_expr
let my_print_context = Termops.print_rel_context
+let my_print_named_context = Termops.print_named_context
let my_print_env = Termops.print_env
let my_print_rawconstr = Printer.pr_rawconstr_env
let my_print_evardefs = Evd.pr_evar_defs
let my_print_tycon_type = Evarutil.pr_tycon_type
-let debug_level = 2
+let debug_level = 1
+
+let debug_on = true
let debug n s =
- if !Options.debug && n >= debug_level then
- msgnl s
+ if debug_on then
+ if !Options.debug && n >= debug_level then
+ msgnl s
+ else ()
else ()
let debug_msg n s =
- if !Options.debug && n >= debug_level then s
+ if debug_on then
+ if !Options.debug && n >= debug_level then s
+ else mt ()
else mt ()
let trace s =
- if !Options.debug && debug_level > 0 then msgnl s
+ if debug_on then
+ if !Options.debug && debug_level > 0 then msgnl s
+ else ()
else ()
let wf_relations = Hashtbl.create 10
@@ -167,30 +176,6 @@ let goal_fix_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Fixp
open Tactics
open Tacticals
-let build_dependent_sum l =
- let rec aux (tac, typ) = function
- (n, t) :: tl ->
- let t' = mkLambda (Name n, t, typ) in
- trace (spc () ++ str ("treating evar " ^ string_of_id n));
- (try trace (str " assert: " ++ my_print_constr (Global.env ()) t)
- with _ -> ());
- let tac' =
- tclTHENS (assert_tac true (Name n) t)
- ([intros;
- (tclTHENSEQ
- [constructor_tac (Some 1) 1
- (Rawterm.ImplicitBindings [mkVar n]);
- tac]);
- ])
- in
- let newt = mkApp (Lazy.force ex_ind, [| t; t'; |]) in
- aux (tac', newt) tl
- | [] -> tac, typ
- in
- match l with
- (_, hd) :: tl -> aux (intros, hd) tl
- | [] -> raise (Invalid_argument "build_dependent_sum")
-
let id x = x
let build_dependent_sum l =
@@ -438,3 +423,32 @@ let rewrite_cases env c =
let c' = rewrite_cases c in
let _ = trace (str "Rewrote cases: " ++ spc () ++ my_print_rawconstr env c') in
c'
+
+let id_of_name = function
+ Name n -> n
+ | Anonymous -> raise (Invalid_argument "id_of_name")
+
+let definition_message id =
+ Options.if_verbose message ((string_of_id id) ^ " is defined")
+
+let recursive_message v =
+ match Array.length v with
+ | 0 -> error "no recursive definition"
+ | 1 -> (Printer.pr_global v.(0) ++ str " is recursively defined")
+ | _ -> hov 0 (prvect_with_sep pr_coma Printer.pr_global v ++
+ spc () ++ str "are recursively defined")
+
+(* Solve an obligation using tactics, return the corresponding proof term *)
+let solve_by_tac ev t =
+ debug 1 (str "Solving goal using tactics: " ++ Evd.pr_evar_info ev);
+ let goal = Proof_trees.mk_goal ev.evar_hyps ev.evar_concl None in
+ let ts = Tacmach.mk_pftreestate goal in
+ let solved_state = Tacmach.solve_pftreestate t ts in
+ 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