* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
module C = Cic
module P = PrimitiveTactics
module T = Tacticals
module F = FreshNamesGenerator
module E = ProofEngineTypes
module H = ProofEngineHelpers
-module Q = MetadataQuery
(*
let induction_tac ~term status =
~continuation:(S.clear what)
in
E.apply_tactic tac status
- else raise (E.Fail "unexported elim_clear: not an eliminable type")
+ else raise (E.Fail (lazy "unexported elim_clear: not an eliminable type"))
in
E.mk_tactic elim_clear_tac
(* elim type ****************************************************************)
-let elim_type_tac ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[])
- ?depth ?using what =
- let elim what = P.elim_intros_simpl_tac ?using ?depth ~mk_fresh_name_callback what in
- let elim_type_tac status =
- let tac = T.thens ~start: (P.cut_tac what)
- ~continuations:[elim (C.Rel 1); T.id_tac]
- in
- E.apply_tactic tac status
- in
- E.mk_tactic elim_type_tac
+let elim_type_tac ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) ?depth
+ ?using what
+=
+ let elim what =
+ P.elim_intros_simpl_tac ?using ?depth ~mk_fresh_name_callback what
+ in
+ let elim_type_tac status =
+ let tac =
+ T.thens ~start: (P.cut_tac what) ~continuations:[elim (C.Rel 1); T.id_tac]
+ in
+ E.apply_tactic tac status
+ in
+ E.mk_tactic elim_type_tac
(* decompose ****************************************************************)
let debug_print = fun _ -> ()
(** debugging print *)
-let warn s =
- if debug then
- debug_print ("DECOMPOSE: " ^ s)
+let warn s = debug_print (lazy ("DECOMPOSE: " ^ (Lazy.force s)))
(* search in term the Inductive Types and return a list of uris as triples like this: (uri,typeno,exp_named_subst) *)
let search_inductive_types ty =
let (proof, goal) = status in
let _, metasenv,_,_ = proof in
let _, context, _ = CicUtil.lookup_meta goal metasenv in
- let types = List.rev_append user_types (Q.decomposables dbd) in
+ let types = List.rev_append user_types (FwdQueries.decomposables dbd) in
let tactic = elim_clear_tac ~mk_fresh_name_callback ~types in
let old_context_length = List.length context in
let tac = T.then_ ~start:(tactic ~what)
let rec elim_clear_tac ~term' ~nr_of_hyp_still_to_elim status =
let (proof, goal) = status in
- warn ("nr_of_hyp_still_to_elim=" ^ (string_of_int nr_of_hyp_still_to_elim));
+ warn (lazy ("nr_of_hyp_still_to_elim=" ^ (string_of_int nr_of_hyp_still_to_elim)));
if nr_of_hyp_still_to_elim <> 0 then
let _,metasenv,_,_ = proof in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
let termty,_ =
CicTypeChecker.type_of_aux' metasenv context term'
CicUniv.empty_ugraph in
- warn ("elim_clear termty= " ^ CicPp.ppterm termty);
+ warn (lazy ("elim_clear termty= " ^ CicPp.ppterm termty));
match termty with
C.MutInd (uri,typeno,exp_named_subst)
| C.Appl((C.MutInd (uri,typeno,exp_named_subst))::_)
when (List.mem (uri,typeno,exp_named_subst) urilist) ->
- warn ("elim " ^ CicPp.ppterm termty);
+ warn (lazy ("elim " ^ CicPp.ppterm termty));
ProofEngineTypes.apply_tactic
(T.then_
~start:(P.elim_intros_simpl_tac term')
let _,metasenv,_,_ = proof in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
let new_context_len = List.length context in
- warn ("newcon=" ^ (string_of_int new_context_len) ^ " & oldcon=" ^ (string_of_int old_context_len) ^ " & old_nr_of_hyp=" ^ (string_of_int nr_of_hyp_still_to_elim));
+ warn (lazy ("newcon=" ^ (string_of_int new_context_len) ^ " & oldcon=" ^ (string_of_int old_context_len) ^ " & old_nr_of_hyp=" ^ (string_of_int nr_of_hyp_still_to_elim)));
let new_nr_of_hyp_still_to_elim = nr_of_hyp_still_to_elim + (new_context_len - old_context_len) - 1 in
let hyp_name =
match List.nth context new_nr_of_hyp_still_to_elim with
(T.then_
~start:(
if (term'==term) (* if it's the first application of elim, there's no need to clear the hyp *)
- then begin debug_print ("%%%%%%% no clear"); T.id_tac end
- else begin debug_print ("%%%%%%% clear " ^ (string_of_int (new_nr_of_hyp_still_to_elim))); (S.clear ~hyp:hyp_name) end)
+ then begin debug_print (lazy ("%%%%%%% no clear")); T.id_tac end
+ else begin debug_print (lazy ("%%%%%%% clear " ^ (string_of_int (new_nr_of_hyp_still_to_elim)))); (S.clear ~hyp:hyp_name) end)
~continuation:(ProofEngineTypes.mk_tactic (elim_clear_tac ~term':(C.Rel new_nr_of_hyp_still_to_elim) ~nr_of_hyp_still_to_elim:new_nr_of_hyp_still_to_elim)))
status
)))
status
| _ ->
let new_nr_of_hyp_still_to_elim = nr_of_hyp_still_to_elim - 1 in
- warn ("fail; hyp=" ^ (string_of_int new_nr_of_hyp_still_to_elim));
+ warn (lazy ("fail; hyp=" ^ (string_of_int new_nr_of_hyp_still_to_elim)));
elim_clear_tac ~term':(C.Rel new_nr_of_hyp_still_to_elim) ~nr_of_hyp_still_to_elim:new_nr_of_hyp_still_to_elim status
else (* no hyp to elim left in this goal *)
ProofEngineTypes.apply_tactic T.id_tac status