From 728734356fbb8f3d66fb022c8a97b464f8893be8 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 20 Sep 2004 15:51:19 +0000 Subject: [PATCH] added initial_status --- helm/ocaml/tactics/proofEngineTypes.ml | 15 +++++++++++++++ helm/ocaml/tactics/proofEngineTypes.mli | 5 +++++ 2 files changed, 20 insertions(+) diff --git a/helm/ocaml/tactics/proofEngineTypes.ml b/helm/ocaml/tactics/proofEngineTypes.ml index ac0713bd0..8d1def22e 100644 --- a/helm/ocaml/tactics/proofEngineTypes.ml +++ b/helm/ocaml/tactics/proofEngineTypes.ml @@ -31,6 +31,21 @@ type proof = UriManager.uri option * Cic.metasenv * Cic.term * Cic.term 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 diff --git a/helm/ocaml/tactics/proofEngineTypes.mli b/helm/ocaml/tactics/proofEngineTypes.mli index c58b729b5..af5daf5dc 100644 --- a/helm/ocaml/tactics/proofEngineTypes.mli +++ b/helm/ocaml/tactics/proofEngineTypes.mli @@ -31,6 +31,11 @@ type proof = UriManager.uri option * Cic.metasenv * Cic.term * Cic.term type goal = int type status = proof * goal + (** @param goal + * @param goal's metasenv + * @return initial proof status for the given goal *) +val initial_status: Cic.term -> Cic.metasenv -> status + (** a tactic: make a transition from one status to another one or, usually, raise a "Fail" (@see Fail) exception in case of failure -- 2.39.2