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 *)
let rec search_name i = function
| [] -> T.id_tac
| Some (Cic.Name n, _) :: _ when n = name ->
- destruct ~first_time:false ~term:(Cic.Rel i)
+ destruct ~first_time:false (Cic.Rel i)
| _ :: tl -> search_name (succ i) tl
in
PET.apply_tactic (search_name 1 context) 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 =
+and destruct ?(simplified = false) ~first_time term =
let are_convertible hd1 hd2 metasenv context =
fst (CR.are_convertible ~metasenv context hd1 hd2 CU.empty_ugraph)
in
| _, 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 *) ->
+ | _ when first_time && simplified -> raise exn_nothingtodo
+ | _ when simplified (* && not first time *) -> T.id_tac
+ | _ (* when not simplified *) ->
T.then_ ~start:(simpl_in_term context term)
- ~continuation:(destruct ~first_time:false ~term)
+ ~continuation:(destruct ~simplified:true ~first_time term)
end
- | _ when not first_time -> T.id_tac
- | _ (* when first_time *) -> raise exn_nothingtodo
+ | _ when first_time && simplified -> raise exn_nothingtodo
+ | _ when simplified (* && not first time *) -> T.id_tac
+ | _ (* when not simplified *) ->
+ T.then_ ~start:(simpl_in_term context term)
+ ~continuation:(destruct ~simplified:true ~first_time term)
in
PET.apply_tactic tac status
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
+ if exists context term then destruct ~first_time term else T.id_tac
in
PET.apply_tactic tactic status
in
(* destruct performs either injection or discriminate *)
(* equivalent to Coq's "analyze equality" *)
let destruct_tac = function
- | Some term -> destruct ~first_time:true ~term
+ | Some term -> destruct ~first_time:true term
| None ->
let destruct_all status =
let (proof, goal) = status in