X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FdestructTactic.ml;h=f6fb61ac1ddf0e4a5511cf4c639bcc0bb0d17423;hb=1b70a1f66be53f76e475383e86d63c2b5c1fbcaa;hp=bbfee8041ac0f827f12ca84971d0010258286c79;hpb=2c80e9d9409119febcab9c08d6e6cad702384169;p=helm.git diff --git a/helm/software/components/tactics/destructTactic.ml b/helm/software/components/tactics/destructTactic.ml index bbfee8041..f6fb61ac1 100644 --- a/helm/software/components/tactics/destructTactic.ml +++ b/helm/software/components/tactics/destructTactic.ml @@ -39,60 +39,11 @@ module RT = ReductionTactics module PEH = ProofEngineHelpers module ET = EqualityTactics module DTI = DoubleTypeInference -module FNG = FreshNamesGenerator -let debug = true +let debug = false let debug_print = if debug then (fun x -> prerr_endline (Lazy.force x)) else (fun _ -> ()) -(* funzione generale di rilocazione dei riferimenti locali *) - -let relocate_term map t = - let rec map_xnss k xnss = - let imap (uri, t) = uri, map_term k t in - List.map imap xnss - and map_mss k mss = - let imap = function - | None -> None - | Some t -> Some (map_term k t) - in - List.map imap mss - and map_fs len k fs = - let imap (name, i, ty, bo) = name, i, map_term k ty, map_term (k + len) bo in - List.map imap fs - and map_cfs len k cfs = - let imap (name, ty, bo) = name, map_term k ty, map_term (k + len) bo in - List.map imap cfs - and map_term k = function - | C.Rel m -> if m < k then C.Rel m else C.Rel (map (m - k)) - | C.Sort _ as t -> t - | C.Implicit _ as t -> t - | C.Var (uri, xnss) -> C.Var (uri, map_xnss k xnss) - | C.Const (uri, xnss) -> C.Const (uri, map_xnss k xnss) - | C.MutInd (uri, tyno, xnss) -> C.MutInd (uri, tyno, map_xnss k xnss) - | C.MutConstruct (uri, tyno, consno, xnss) -> - C.MutConstruct (uri, tyno, consno, map_xnss k xnss) - | C.Meta (i, mss) -> C.Meta(i, map_mss k mss) - | C.Cast (te, ty) -> C.Cast (map_term k te, map_term k ty) - | C.Appl ts -> C.Appl (List.map (map_term k) ts) - | C.MutCase (sp, i, outty, t, pl) -> - C.MutCase (sp, i, map_term k outty, map_term k t, List.map (map_term k) pl) - | C.Prod (n, s, t) -> C.Prod (n, map_term k s, map_term (succ k) t) - | C.Lambda (n, s, t) -> C.Lambda (n, map_term k s, map_term (succ k) t) - | C.LetIn (n, s, t) -> C.LetIn (n, map_term k s, map_term (succ k) t) - | C.Fix (i, fs) -> C.Fix (i, map_fs (List.length fs) k fs) - | C.CoFix (i, cfs) -> C.CoFix (i, map_cfs (List.length cfs) k cfs) - in - map_term 0 t - -let id n = n - -let after continuation aftermap beforemap = - continuation ~map:(fun n -> aftermap (beforemap n)) - -let after2 continuation aftermap beforemap ~map = - continuation ~map:(fun n -> map (aftermap (beforemap n))) - (* term ha tipo t1=t2; funziona solo se t1 e t2 hanno in testa costruttori diversi *) @@ -141,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 @@ -207,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] @@ -275,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 @@ -292,44 +243,28 @@ let clear_term first_time lterm = in PET.mk_tactic clear_term -let simpl_in_term context = function - | Cic.Rel i -> - let name = match List.nth context (pred i) with - | Some (Cic.Name s, Cic.Def _) -> s - | Some (Cic.Name s, Cic.Decl _) -> s - | _ -> assert false - in - RT.simpl_tac ~pattern:(None,[name,Cic.Implicit (Some `Hole)],None) - | _ -> T.id_tac - -let mk_fresh_name metasenv context name typ = - let name = C.Name name in - match FNG.mk_fresh_name ~subst:[] metasenv context name ~typ with - | C.Name s -> s - | C.Anonymous -> assert false - let exists context = function | C.Rel i -> List.nth context (pred i) <> None | _ -> true -let rec recur_on_child_tac name = +let recur_on_child_tac ~before ~after = let recur_on_child status = let (proof, goal) = status in let _, metasenv, _subst, _, _, _ = proof in let _, context, _ = CicUtil.lookup_meta goal metasenv in - debug_print (lazy ("\nrecur_on_child su: " ^ name)); + debug_print (lazy ("\nrecur_on_child")); debug_print (lazy ("nel contesto:\n" ^ CicPp.ppcontext context)); - let rec search_name i = function - | [] -> T.id_tac - | Some (Cic.Name n, _) :: _ when n = name -> - destruct ~first_time:false ~term:(Cic.Rel i) - | _ :: tl -> search_name (succ i) tl + let mk_lterm term c m ug = + let distance = List.length c - List.length context in + S.lift distance term, m, ug in - PET.apply_tactic (search_name 1 context) status + let lterm = mk_lterm (Cic.Rel 1) 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) @@ -342,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 *) @@ -366,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 @@ -448,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) @@ -490,13 +425,10 @@ and injection_tac ~lterm ~i ~continuation = PET.mk_tactic fill_cut in debug_print (lazy ("CUT: " ^ pp context cutted)); - let name = mk_fresh_name metasenv context "Hcut" cutted in - let mk_fresh_name_callback = PEH.namer_of [Some name] in - debug_print (lazy ("figlio: " ^ name)); let tactic = - T.thens ~start: (P.cut_tac ~mk_fresh_name_callback cutted) + T.thens ~start: (P.cut_tac cutted) ~continuations:[ - T.seq ~tactics:[continuation; recur_on_child_tac name]; + recur_on_child_tac continuation recur; fill_cut_tac term ] in @@ -505,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 -> @@ -522,59 +454,54 @@ 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 = - T.seq ~tactics:[continuation; recur_on_child_tac name] - in - debug_print (lazy ("figlio: " ^ name)); + 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 -(* ~term vive nel contesto della tattica una volta ~mappato - * ~continuation riceve la mappa assoluta - *) -and destruct ~first_time ~term = +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 - 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 - debug_print (lazy ("\ndestruct su: " ^ pp context termty)); - let mk_lterm term c m ug = - let distance = List.length c - List.length context in - S.lift distance term, m, ug - in - let lterm = mk_lterm term in - let mk_subst_chain direction index with_what what = - let k = match term with C.Rel i -> i | _ -> -1 in - let rec traverse_context first_time j = function - | [] -> - let continuation = - T.seq ~tactics:[ - clear_term first_time lterm; - clear_term false (mk_lterm what); - clear_term false (mk_lterm with_what) - ] - in - subst_tac ~direction ~lterm ~where:None ~continuation - | 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) - ~continuation:(traverse_context false (succ j) tl) - | _ :: tl -> traverse_context first_time (succ j) tl + 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.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 + S.lift distance term, m, ug in - traverse_context first_time 1 context - in - let tac = match termty with + let lterm = mk_lterm term in + let mk_subst_chain direction index with_what what = + let k = match term with C.Rel i -> i | _ -> -1 in + let rec traverse_context first_time j = function + | [] -> + let continuation = + T.seq ~tactics:[ + clear_term first_time lterm; + clear_term false (mk_lterm what); + clear_term false (mk_lterm with_what) + ] + in + 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) ~recur + ~continuation:(traverse_context false (succ j) tl) + | _ :: tl -> traverse_context first_time (succ j) tl + in + traverse_context first_time 1 context + in + match termty with | C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2] when LibraryObjects.is_eq_URI equri -> begin match t1,t2 with @@ -592,7 +519,7 @@ and destruct ~first_time ~term = 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, @@ -625,53 +552,41 @@ and destruct ~first_time ~term = | _, C.Rel i2 when DTI.does_not_occur i2 t1 -> mk_subst_chain `RightToLeft i2 t1 t2 (* else part *) - | _ when not first_time -> T.id_tac - | _ (* when first_time *) -> - T.then_ ~start:(simpl_in_term context term) - ~continuation:(destruct ~first_time:false ~term) + | _ when first_time -> raise exn_nothingtodo + | _ (* when not first time *) -> T.id_tac end - | _ when not first_time -> T.id_tac - | _ (* when first_time *) -> raise exn_nothingtodo - in - PET.apply_tactic tac status + | _ when first_time -> raise exn_nothingtodo + | _ (* when not first time *) -> T.id_tac + end in + PET.apply_tactic tactic status in PET.mk_tactic destruct -let lazy_destruct_tac ~first_time ~lterm = - let lazy_destruct status = +(* destruct performs either injection or discriminate or subst *) +let destruct_tac xterms = + let destruct status = let (proof, goal) = status in let _,metasenv,_subst,_,_, _ = proof in let _,context,_ = CicUtil.lookup_meta goal metasenv in - let term, _, _ = lterm context metasenv CU.empty_ugraph in - let tactic = - if exists context term then destruct ~first_time ~term else T.id_tac + let mk_lterm term c m ug = + let distance = List.length c - List.length context in + S.lift distance term, m, ug in - PET.apply_tactic tactic status - in - PET.mk_tactic lazy_destruct - -(* destruct performs either injection or discriminate *) -(* equivalent to Coq's "analyze equality" *) -let destruct_tac = function - | Some term -> destruct ~first_time:true ~term - | None -> - let destruct_all status = - let (proof, goal) = status in - let _,metasenv,_subst,_,_, _ = proof in - let _,context,_ = CicUtil.lookup_meta goal metasenv in - let mk_lterm term c m ug = - let distance = List.length c - List.length context in - S.lift distance term, m, ug - in - let rec mk_tactics first_time i tacs = function - | [] -> List.rev tacs - | Some _ :: tl -> - let lterm = mk_lterm (C.Rel i) in - let tacs = lazy_destruct_tac ~first_time ~lterm :: tacs in - mk_tactics false (succ i) tacs tl - | _ :: tl -> mk_tactics first_time (succ i) tacs tl - in - let tactics = mk_tactics false 1 [] context in - PET.apply_tactic (T.seq ~tactics) status + 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 -> + let lterm = mk_lterm (C.Rel i) in + let tacs = destruct ~first_time lterm :: tacs in + mk_tactics false (succ i) tacs tl + | _ :: tl -> mk_tactics first_time (succ i) tacs tl + in + mk_tactics false 1 [] context in - PET.mk_tactic destruct_all + PET.apply_tactic (T.seq ~tactics) status + in + PET.mk_tactic destruct