From: Ferruccio Guidi Date: Thu, 25 Oct 2007 21:36:13 +0000 (+0000) Subject: bug fix in injection e relocate term X-Git-Tag: make_still_working~5944 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6a0ba36a34474850464f568139fdda5e9d85f315;p=helm.git bug fix in injection e relocate term --- diff --git a/helm/software/components/tactics/discriminationTactics.ml b/helm/software/components/tactics/discriminationTactics.ml index f12e4b3f5..f31b52a2e 100644 --- a/helm/software/components/tactics/discriminationTactics.ml +++ b/helm/software/components/tactics/discriminationTactics.ml @@ -41,7 +41,6 @@ module PEH = ProofEngineHelpers 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 *) @@ -81,11 +80,15 @@ let relocate_term map 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 1 t + map_term 0 t let id n = n -let comp f g n = f (g 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 *) @@ -286,10 +289,10 @@ let simpl_in_term context = function RT.simpl_tac ~pattern:(None,[name,Cic.Implicit (Some `Hole)],None) | _ -> raise exn_nonproj -(* ~term vive nel contesto della tattica - * ~continuation riceve la mappa relativa +(* ~term vive nel contesto della tattica una volta ~mappato + * ~continuation riceve la mappa assoluta *) -let rec injection_tac ~term ~i ~continuation = +let rec injection_tac ~map ~term ~i ~continuation = let give_name seed = function | C.Name _ as name -> name | C.Anonymous -> C.Name (incr seed; "y" ^ string_of_int !seed) @@ -302,6 +305,7 @@ let rec injection_tac ~term ~i ~continuation = * del costruttore *) let _,metasenv,_subst,_,_, _ = proof in let _,context,_ = CicUtil.lookup_meta goal metasenv in + let term = relocate_term map term in let termty,_ = CTC.type_of_aux' metasenv context term CicUniv.empty_ugraph in @@ -322,7 +326,7 @@ let rec injection_tac ~term ~i ~continuation = when (uri1 = uri2) && (typeno1 = typeno2) && (consno1 = consno2) && (ens1 = ens2) -> (* controllo ridondante *) - List.nth applist1 (i-1),List.nth applist2 (i-1),consno2 + 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 @@ -447,13 +451,13 @@ let rec injection_tac ~term ~i ~continuation = in PET.mk_tactic tac in - debug_print (lazy ("CUT: " ^ pp context cutted)); - let continuation ~map = continuation ~map:(comp succ map) in + debug_print (lazy ("CUT: " ^ pp context cutted)); PET.apply_tactic (T.thens ~start: (P.cut_tac cutted) ~continuations:[ (qnify_tac ~first_time:false ~term:(C.Rel 1) ~map:id - ~continuation); + ~continuation:(after2 continuation succ map) + ); tac term] ) status | _ -> raise exn_noneq @@ -461,7 +465,7 @@ let rec injection_tac ~term ~i ~continuation = PET.mk_tactic injection_tac (* ~term vive nel contesto della tattica una volta ~mappato - * ~continuation riceve la mappa relativa + * ~continuation riceve la mappa assoluta *) and qnify_tac ~first_time ~map ~term ~continuation = let are_convertible hd1 hd2 metasenv context = @@ -472,6 +476,8 @@ and qnify_tac ~first_time ~map ~term ~continuation = let _,metasenv,_subst, _,_, _ = proof in let _,context,_ = CicUtil.lookup_meta goal metasenv in let term = relocate_term map term in + debug_print (lazy ("\nqnify di: " ^ pp context term)); + debug_print (lazy ("nel contesto:\n" ^ CicPp.ppcontext context)); let termty,_ = CTC.type_of_aux' metasenv context term CicUniv.empty_ugraph in @@ -487,25 +493,27 @@ and qnify_tac ~first_time ~map ~term ~continuation = C.MutConstruct _ when t1 = t2 -> T.then_ ~start:(clear_term first_time context term) - ~continuation:(continuation ~map:id) + ~continuation:(continuation ~map) | C.Appl (C.MutConstruct _ as mc1 :: applist1), C.Appl (C.MutConstruct _ as mc2 :: applist2) when mc1 = mc2 -> - let rec traverse_list i l1 l2 = match l1, l2 with - | [], [] -> - T.then_ ~start:(clear_term first_time context term) - ~continuation:(continuation ~map:id) - | hd1 :: tl1, hd2 :: tl2 -> - if are_convertible hd1 hd2 metasenv context then - traverse_list (succ i) tl1 tl2 - else - injection_tac ~i ~term ~continuation: - (qnify_tac ~first_time:false ~term ~continuation) - | _ -> assert false + let rec traverse_list first_time i l1 l2 = + match l1, l2 with + | [], [] -> + fun ~map:aftermap -> + T.then_ ~start:(clear_term first_time context term) + ~continuation:(after continuation aftermap map) + | hd1 :: tl1, hd2 :: tl2 -> + if are_convertible hd1 hd2 metasenv context then + traverse_list first_time (succ i) tl1 tl2 + else + injection_tac ~i ~term ~continuation: + (traverse_list false (succ i) tl1 tl2) + | _ -> assert false (* i 2 termini hanno in testa lo stesso costruttore, * ma applicato a un numero diverso di termini *) in - traverse_list 1 applist1 applist2 + traverse_list first_time 1 applist1 applist2 ~map:id | C.MutConstruct (_,_,consno1,ens1), C.MutConstruct (_,_,consno2,ens2) | C.MutConstruct (_,_,consno1,ens1), @@ -516,12 +524,12 @@ and qnify_tac ~first_time ~map ~term ~continuation = C.Appl ((C.MutConstruct (_,_,consno2,ens2))::_) when (consno1 <> consno2) || (ens1 <> ens2) -> discriminate_tac ~term - | _ when not first_time -> continuation ~map:id + | _ when not first_time -> continuation ~map | _ (* when first_time *) -> T.then_ ~start:(simpl_in_term context term) - ~continuation:(qnify_tac ~first_time:false ~term ~map:id ~continuation) + ~continuation:(qnify_tac ~first_time:false ~term ~map ~continuation) end - | _ when not first_time -> continuation ~map:id + | _ when not first_time -> continuation ~map | _ (* when first_time *) -> raise exn_nonproj end | _ -> raise exn_nonproj