type goal = int
type status = proof * goal
+let initial_status ty metasenv =
+ let rec aux max = function
+ | [] -> max + 1
+ | (idx, _, _) :: tl ->
+ if idx > max then
+ aux idx tl
+ else
+ aux max tl
+ in
+ let newmeta_idx = aux 0 metasenv in
+ let proof =
+ None, (newmeta_idx, [], ty) :: metasenv, Cic.Meta (newmeta_idx, []), ty
+ in
+ (proof, newmeta_idx)
+
(**
a tactic: make a transition from one status to another one or, usually,
raise a "Fail" (@see Fail) exception in case of failure
(** an unfinished proof with the optional current goal *)
type tactic = status -> proof * goal list
+ (** creates an opaque tactic from a status->proof*goal list function *)
+let mk_tactic t = t
+
(** tactic failure *)
exception Fail of string
+ (**
+ calls the opaque tactic on the status, restoring the original
+ universe graph if the tactic Fails
+ *)
+let apply_tactic t status =
+ let saved_univ = CicUniv.get_working() in
+ try
+ t status
+ with Fail s -> CicUniv.set_working saved_univ; raise (Fail s)
+
(** constraint: the returned value will always be constructed by Cic.Name **)
type mk_fresh_name_type =
Cic.metasenv -> Cic.context -> Cic.name -> typ:Cic.term -> Cic.name