(**
current proof (proof uri * metas * (in)complete proof * term to be prooved)
*)
-type proof = UriManager.uri * Cic.metasenv * Cic.term * Cic.term
+type proof = UriManager.uri option * Cic.metasenv * Cic.term * Cic.term
(** current goal, integer index *)
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:status -> proof * goal list
+type tactic = status -> proof * goal list
+
+ (** creates an opaque tactic from a status->proof*goal list function *)
+let mk_tactic t = t
+
+type reduction = Cic.context -> Cic.term -> Cic.term
+
+type lazy_term =
+ Cic.context -> Cic.metasenv -> CicUniv.universe_graph ->
+ Cic.term * Cic.metasenv * CicUniv.universe_graph
+
+let const_lazy_term t =
+ (fun _ metasenv ugraph -> t, metasenv, ugraph)
+
+type lazy_reduction =
+ Cic.context -> Cic.metasenv -> CicUniv.universe_graph ->
+ reduction * Cic.metasenv * CicUniv.universe_graph
+
+let const_lazy_reduction red =
+ (fun _ metasenv ugraph -> red, metasenv, ugraph)
+
+type pattern = lazy_term option * (string * Cic.term) list * Cic.term
+
+let conclusion_pattern t =
+ let t' =
+ match t with
+ | None -> None
+ | Some t -> Some (fun _ m u -> t, m, u)
+ in
+ t',[],Cic.Implicit (Some `Hole)
(** 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 =
+ t status
+
(** 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
+
+let goals_of_proof (_,metasenv,_,_) = List.map (fun (g,_,_) -> g) metasenv
+