diff options
Diffstat (limited to 'contrib/subtac/subtac_utils.ml')
| -rw-r--r-- | contrib/subtac/subtac_utils.ml | 72 |
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 |