let id_tac =
let id_tac (proof,goal) =
- let _, metasenv, _subst, _, _, _ = proof in
+ let _, metasenv, _, _, _, _ = proof in
let _, _, _ = CicUtil.lookup_meta goal metasenv in
(proof,[goal])
in
let fail_tac =
let fail_tac (proof,goal) =
- let _, metasenv, _subst, _ , _, _ = proof in
+ let _, metasenv, _, _ , _, _ = proof in
let _, _, _ = CicUtil.lookup_meta goal metasenv in
raise (PET.Fail (lazy "fail tactical"))
in
(HExtlib.list_concat ~sep:[ C.Semicolon ]
(List.map (fun t -> [ C.Tactical (C.Tactic t) ]) tactics)))
+(* Tacticals that cannot be implemented on top of tynycals *)
+
+let const_tac res = PET.mk_tactic (fun _ -> res)
+
let if_ ~start ~continuation ~fail =
- S.mk_tactic
- (fun istatus ->
- let xostatus =
- try
- let res = C.eval (C.Tactical (C.Tactic start)) istatus in
+ let if_ status =
+ let xoutput =
+ try
+ let result = PET.apply_tactic start status in
info (lazy ("Tacticals.if_: succedeed!!!"));
- Some res
+ Some result
with PET.Fail _ -> None
in
- match xostatus with
- | Some ostatus ->
- let opened,closed = S.goals ostatus in
- begin match opened with
- | [] -> ostatus
- | _ ->
- fold_eval (S.focus ~-1 ostatus)
- [ C.Semicolon; C.Tactical (C.Tactic continuation) ]
- end
- | None -> C.eval (C.Tactical (C.Tactic fail)) istatus
- )
-
-(* Tacticals that cannot be implemented on top of tynycals *)
+ let tactic = match xoutput with
+ | Some res -> then_ ~start:(const_tac res) ~continuation
+ | None -> fail
+ in
+ PET.apply_tactic tactic status
+ in
+ PET.mk_tactic if_
+
+let ifs ~start ~continuations ~fail =
+ let ifs status =
+ let xoutput =
+ try
+ let result = PET.apply_tactic start status in
+ info (lazy ("Tacticals.ifs: succedeed!!!"));
+ Some result
+ with PET.Fail _ -> None
+ in
+ let tactic = match xoutput with
+ | Some res -> thens ~start:(const_tac res) ~continuations
+ | None -> fail
+ in
+ PET.apply_tactic tactic status
+ in
+ PET.mk_tactic ifs
let first ~tactics =
let rec first ~(tactics: tactic list) status =
in
PET.mk_tactic (first ~tactics)
-
let rec do_tactic ~n ~tactic =
PET.mk_tactic
(function status ->
let progress_tactic ~tactic =
let msg = lazy "Failed to progress" in
- let progress_tactic (((_,metasenv,_subst,_,_,_),_) as istatus) =
- let ((_,metasenv',_subst,_,_,_),_) as ostatus =
+ let progress_tactic (((_,metasenv,_,_,_,_),g) as istatus) =
+ let ((_,metasenv',_,_,_,_),opened) as ostatus =
PET.apply_tactic tactic istatus
in
- (*CSC: Warning
- If just the index of some metas changes the tactic is recognized
- as a progressing one. This is wrong. *)
- if metasenv' = metasenv then
- raise (PET.Fail msg)
- else
- ostatus
+ match opened with
+ | [g1] ->
+ let _,oc,oldty = CicUtil.lookup_meta g metasenv in
+ let _,nc,newty = CicUtil.lookup_meta g1 metasenv' in
+ if oldty = newty && oc = nc then
+ raise (PET.Fail msg)
+ else
+ ostatus
+ | _ -> ostatus
in
PET.mk_tactic progress_tactic