let mk_branches_and_outtype turi typeno consno context args =
(* a list of "True" except for the element in position consno which
* is "False" *)
- match fst (CicEnvironment.get_obj CU.empty_ugraph turi) with
+ match fst (CicEnvironment.get_obj CU.oblivion_ugraph turi) with
| C.InductiveDefinition (ind_type_list,_,paramsno,_) ->
let _,_,rty,constructor_list = List.nth ind_type_list typeno in
let false_constr_id,_ = List.nth constructor_list (consno - 1) in
let _,metasenv,_subst,_,_, _ = proof in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
let termty,_ =
- CTC.type_of_aux' metasenv context term CU.empty_ugraph
+ CTC.type_of_aux' metasenv context term CU.oblivion_ugraph
in
match termty with
| C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]
let (proof, goal) = status in
let _,metasenv,_subst,_,_, _ = proof in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
- let term, metasenv, _ugraph = lterm context metasenv CU.empty_ugraph in
+ let term, metasenv, _ugraph = lterm context metasenv CU.oblivion_ugraph in
debug_print (lazy ("\nclear di: " ^ pp context term));
debug_print (lazy ("nel contesto:\n" ^ CicPp.ppcontext context));
let g () = if first_time then raise exn_nothingtodo else T.id_tac in
| C.Rel i -> List.nth context (pred i) <> None
| _ -> true
-let rec recur_on_child_tac ~before =
+let recur_on_child_tac ~before ~after =
let recur_on_child status =
let (proof, goal) = status in
let _, metasenv, _subst, _, _, _ = proof in
S.lift distance term, m, ug
in
let lterm = mk_lterm (Cic.Rel 1) in
- let continuation = destruct ~first_time:false lterm in
- let tactic = T.then_ ~start:before ~continuation in
+ let tactic = T.then_ ~start:before ~continuation:(after lterm) in
PET.apply_tactic tactic status
in
PET.mk_tactic recur_on_child
-and injection_tac ~lterm ~i ~continuation =
+let injection_tac ~lterm ~i ~continuation ~recur =
let give_name seed = function
| C.Name _ as name -> name
| C.Anonymous -> C.Name (incr seed; "y" ^ string_of_int !seed)
* del costruttore *)
let _,metasenv,_subst,_,_, _ = proof in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
- let term, metasenv, _ugraph = lterm context metasenv CU.empty_ugraph in
+ let term, metasenv, _ugraph = lterm context metasenv CU.oblivion_ugraph in
let termty,_ =
- CTC.type_of_aux' metasenv context term CU.empty_ugraph
+ CTC.type_of_aux' metasenv context term CU.oblivion_ugraph
in
debug_print (lazy ("\ninjection su : " ^ pp context termty));
match termty with (* an equality *)
List.nth applist1 (pred i),List.nth applist2 (pred i),consno2
| _ -> assert false
in
- let tty',_ = CTC.type_of_aux' metasenv context t1' CU.empty_ugraph in
+ let tty',_ = CTC.type_of_aux' metasenv context t1' CU.oblivion_ugraph in
let patterns,outtype =
- match fst (CicEnvironment.get_obj CU.empty_ugraph turi) with
+ match fst (CicEnvironment.get_obj CU.oblivion_ugraph turi) with
| C.InductiveDefinition (ind_type_list,_,paramsno,_)->
let left_params, right_params = HExtlib.split_nth paramsno params in
let _,_,_,constructor_list = List.nth ind_type_list typeno in
let go_on =
try
let _,g = CTC.type_of_aux' metasenv context cutted
- CU.empty_ugraph
+ CU.oblivion_ugraph
in
let _,g = CTC.type_of_aux' metasenv context changed g in
fst (CR.are_convertible ~metasenv context t1' changed g)
let tactic =
T.thens ~start: (P.cut_tac cutted)
~continuations:[
- recur_on_child_tac continuation;
+ recur_on_child_tac continuation recur;
fill_cut_tac term
]
in
in
PET.mk_tactic injection_tac
-and subst_tac ~lterm ~direction ~where ~continuation =
+let subst_tac ~lterm ~direction ~where ~continuation ~recur =
let subst_tac status =
let (proof, goal) = status in
let _,metasenv,_subst,_,_, _ = proof in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
- let term, metasenv, _ugraph = lterm context metasenv CU.empty_ugraph in
+ let term, metasenv, _ugraph = lterm context metasenv CU.oblivion_ugraph in
debug_print (lazy ("\nsubst " ^ (match direction with `LeftToRight -> "->" | `RightToLeft -> "<-") ^ " di: " ^ pp context term));
let tactic = match where with
| None ->
debug_print (lazy ("nella premessa: " ^ name));
let pattern = None, [name, PET.hole], None in
let start = ET.rewrite_tac ~direction ~pattern term [] in
- let ok_tactic = recur_on_child_tac continuation in
+ let ok_tactic = recur_on_child_tac continuation recur in
T.if_ ~start ~continuation:ok_tactic ~fail:continuation
in
PET.apply_tactic tactic status
in
PET.mk_tactic subst_tac
-and destruct ~first_time lterm =
+let rec destruct ~first_time lterm =
let are_convertible hd1 hd2 metasenv context =
- fst (CR.are_convertible ~metasenv context hd1 hd2 CU.empty_ugraph)
+ fst (CR.are_convertible ~metasenv context hd1 hd2 CU.oblivion_ugraph)
in
+ let recur = destruct ~first_time:false in
let destruct status =
let (proof, goal) = status in
let _,metasenv,_subst, _,_, _ = proof in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
- let term, metasenv, _ugraph = lterm context metasenv CU.empty_ugraph in
+ let term, metasenv, _ugraph = lterm context metasenv CU.oblivion_ugraph in
let tactic = if not (first_time || exists context term) then T.id_tac else begin
debug_print (lazy ("\ndestruct di: " ^ pp context term));
debug_print (lazy ("nel contesto:\n" ^ CicPp.ppcontext context));
- let termty,_ = CTC.type_of_aux' metasenv context term CU.empty_ugraph in
+ let termty,_ = CTC.type_of_aux' metasenv context term CU.oblivion_ugraph in
debug_print (lazy ("\ndestruct su: " ^ pp context termty));
let mk_lterm term c m ug =
let distance = List.length c - List.length context in
clear_term false (mk_lterm with_what)
]
in
- subst_tac ~direction ~lterm ~where:None ~continuation
+ subst_tac ~direction ~lterm ~where:None ~continuation ~recur
| Some (C.Name name, _) :: tl when j < index && j <> k ->
debug_print (lazy ("\nsubst programmata: cosa: " ^ string_of_int index ^ ", dove: " ^ string_of_int j));
- subst_tac ~direction ~lterm ~where:(Some name)
+ subst_tac ~direction ~lterm ~where:(Some name) ~recur
~continuation:(traverse_context false (succ j) tl)
| _ :: tl -> traverse_context first_time (succ j) tl
in
if are_convertible hd1 hd2 metasenv context then
traverse_list first_time (succ i) tl1 tl2
else
- injection_tac ~i ~lterm ~continuation:
+ injection_tac ~i ~lterm ~recur ~continuation:
(traverse_list false (succ i) tl1 tl2)
| _ -> assert false
(* i 2 termini hanno in testa lo stesso costruttore,
PET.mk_tactic destruct
(* destruct performs either injection or discriminate or subst *)
-let destruct_tac xterm =
+let destruct_tac xterms =
let destruct status =
let (proof, goal) = status in
let _,metasenv,_subst,_,_, _ = proof in
let distance = List.length c - List.length context in
S.lift distance term, m, ug
in
- let tactics = match xterm with
- | Some term -> [destruct ~first_time:true (mk_lterm term)]
- | None ->
+ let tactics = match xterms with
+ | Some terms ->
+ let map term = destruct ~first_time:false (mk_lterm term) in
+ List.map map terms
+ | None ->
let rec mk_tactics first_time i tacs = function
| [] -> List.rev tacs
| Some _ :: tl ->
projects / helm.git / blobdiff