module S = CicSubstitution
module RT = ReductionTactics
module PEH = ProofEngineHelpers
+module ET = EqualityTactics
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 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 *)
~continuation:
(T.then_
~start:
- (EqualityTactics.rewrite_simpl_tac
+ (ET.rewrite_simpl_tac
~direction:`RightToLeft
~pattern:(PET.conclusion_pattern None)
term [])
let names = List.map (function Some (n,_) -> Some n | None -> None) ctx in
CicPp.pp t names
-let injection_tac ~term ~i ~continuation =
+let clear_term first_time context term =
+ let g () = if first_time then raise exn_nothingtodo else T.id_tac in
+ match term with
+ | C.Rel n ->
+ begin match List.nth context (pred n) with
+ | Some (C.Name id, _) -> PST.clear ~hyps:[id]
+ | _ -> assert false
+ end
+ | _ -> g ()
+
+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)
+ | _ -> raise exn_nonproj
+
+(* ~term vive nel contesto della tattica una volta ~mappato
+ * ~continuation riceve la mappa assoluta
+ *)
+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)
* 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
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
with
| CTC.TypeCheckerFailure _ -> false
in
- if not go_on then
- PET.apply_tactic T.id_tac status (* FG: ??????? *)
+ if not go_on then
+ PET.apply_tactic (continuation ~map) status
else
let tac term =
let tac status =
RT.change_tac
~pattern:(None, [], Some (PEH.pattern_of ~term:gty [new_t1']))
(fun _ m u -> changed,m,u);
- EqualityTactics.rewrite_simpl_tac
+ ET.rewrite_simpl_tac
~direction:`LeftToRight
~pattern:(PET.conclusion_pattern None)
term [];
- EqualityTactics.reflexivity_tac
+ ET.reflexivity_tac
] in
PET.apply_tactic tac status
in
PET.mk_tactic tac
in
- debug_print (lazy ("CUT: " ^ pp context cutted));
+ debug_print (lazy ("CUT: " ^ pp context cutted));
PET.apply_tactic
(T.thens ~start: (P.cut_tac cutted)
- ~continuations:[continuation ~map:succ; tac term]
+ ~continuations:[
+ (destruct ~first_time:false ~term:(C.Rel 1) ~map:id
+ ~continuation:(after2 continuation succ map)
+ );
+ tac term]
) status
| _ -> raise exn_noneq
in
PET.mk_tactic injection_tac
-let clear_term first_time context term =
- let g () = if first_time then raise exn_nothingtodo else T.id_tac in
- match term with
- | C.Rel n ->
- begin match List.nth context (pred n) with
- | Some (C.Name id, _) -> PST.clear ~hyps:[id]
- | _ -> assert false
- end
- | _ -> g ()
-
-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)
- | _ -> raise exn_nonproj
+(* ~term vive nel contesto della tattica una volta ~mappato
+ * ~continuation riceve la mappa assoluta
+ *)
+and subst_tac ~map ~term ~direction ~where ~continuation =
+ let fail_tactic = continuation ~map in
+ let subst_tac status =
+ let term = relocate_term map term in
+ let tactic = match where with
+ | None ->
+ let pattern = PET.conclusion_pattern None in
+ let tactic = ET.rewrite_tac ~direction ~pattern term [] in
+ T.then_ ~start:(T.try_tactic ~tactic)
+ ~continuation:fail_tactic
+ | Some name ->
+ let pattern = None, [name, PET.hole], None in
+ let start = ET.rewrite_tac ~direction ~pattern term [] in
+ let continuation =
+ destruct ~first_time:false ~term:(C.Rel 1) ~map:id
+ ~continuation:(after2 continuation succ map)
+ in
+ T.if_ ~start ~continuation ~fail:fail_tactic
+ in
+ PET.apply_tactic tactic status
+ in
+ PET.mk_tactic subst_tac
-let rec qnify_tac ~first_time ~map ~term ~continuation =
+(* ~term vive nel contesto della tattica una volta ~mappato
+ * ~continuation riceve la mappa assoluta
+ *)
+and destruct ~first_time ~map ~term ~continuation =
let are_convertible hd1 hd2 metasenv context =
fst (CR.are_convertible ~metasenv context hd1 hd2 CicUniv.empty_ugraph)
in
- let qnify_tac status =
+ let destruct status =
let (proof, goal) = status in
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
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),
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:(destruct ~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
in
PET.apply_tactic tac status
in
- PET.mk_tactic qnify_tac
+ PET.mk_tactic destruct
(* destruct performs either injection or discriminate *)
(* equivalent to Coq's "analyze equality" *)
let destruct_tac =
- qnify_tac
+ destruct
~first_time:true ~map:id ~continuation:(fun ~map -> T.id_tac)
projects / helm.git / blobdiff