- renamed ocaml/ to components/

[helm.git] / helm / ocaml / tactics / proofEngineTypes.ml

diff --git a/helm/ocaml/tactics/proofEngineTypes.ml b/helm/ocaml/tactics/proofEngineTypes.ml
deleted file mode 100644 (file)
index 68ea561..0000000
--- a/helm/ocaml/tactics/proofEngineTypes.ml
+++ /dev/null
@@ -1,101 +0,0 @@
-(* Copyright (C) 2002, HELM Team.
- * 
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- * 
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- * 
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA  02111-1307, USA.
- * 
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(* $Id$ *)
-
-  (**
-    current proof (proof uri * metas * (in)complete proof * term to be prooved)
-  *)
-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 -> 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
-
-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 ('term, 'lazy_term) pattern =
-  'lazy_term option * (string * 'term) list * 'term option
-
-type lazy_pattern = (Cic.term, Cic.lazy_term) pattern
-
-let conclusion_pattern t =
-  let t' = 
-    match t with
-    | None -> None
-    | Some t -> Some (fun _ m u -> t, m, u)
-  in
-  t',[],Some (Cic.Implicit (Some `Hole))
-
-  (** tactic failure *)
-exception Fail of string Lazy.t
-
-  (** 
-    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
-