X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FdestructTactic.ml;h=f6fb61ac1ddf0e4a5511cf4c639bcc0bb0d17423;hb=1b70a1f66be53f76e475383e86d63c2b5c1fbcaa;hp=8164fc5f68a2165029697fc74b4fbff6e31060c9;hpb=61d82f6f49845fe5111969156945accf21fb5a70;p=helm.git diff --git a/helm/software/components/tactics/destructTactic.ml b/helm/software/components/tactics/destructTactic.ml index 8164fc5f6..f6fb61ac1 100644 --- a/helm/software/components/tactics/destructTactic.ml +++ b/helm/software/components/tactics/destructTactic.ml @@ -92,7 +92,7 @@ let discriminate_tac ~term = 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 @@ -158,7 +158,7 @@ let discriminate_tac ~term = 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] @@ -226,7 +226,7 @@ let clear_term first_time lterm = 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 @@ -247,7 +247,7 @@ let exists context = function | 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 @@ -259,13 +259,12 @@ let rec recur_on_child_tac ~before = 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) @@ -278,9 +277,9 @@ and injection_tac ~lterm ~i ~continuation = * 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 *) @@ -302,9 +301,9 @@ and injection_tac ~lterm ~i ~continuation = 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 @@ -384,7 +383,7 @@ and injection_tac ~lterm ~i ~continuation = 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) @@ -429,7 +428,7 @@ and injection_tac ~lterm ~i ~continuation = 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 @@ -438,12 +437,12 @@ and injection_tac ~lterm ~i ~continuation = 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 -> @@ -455,26 +454,27 @@ and subst_tac ~lterm ~direction ~where ~continuation = 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 @@ -492,10 +492,10 @@ and destruct ~first_time lterm = 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 @@ -519,7 +519,7 @@ and destruct ~first_time lterm = 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, @@ -563,7 +563,7 @@ and destruct ~first_time lterm = 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 @@ -572,9 +572,11 @@ let destruct_tac xterm = 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 ->