helm/software/components/grafite_engine/grafiteTypes.ml

   1 (* Copyright (C) 2004-2005, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://helm.cs.unibo.it/
  24  *)
  25
  26 (* $Id$ *)
  27
  28 exception Option_error of string * string
  29 exception Statement_error of string
  30 exception Command_error of string
  31
  32 let command_error msg = raise (Command_error msg)
  33
  34 type incomplete_proof = {
  35   proof: ProofEngineTypes.proof;
  36   stack: Continuationals.Stack.t;
  37 }
  38
  39 type proof_status =
  40   | No_proof
  41   | Incomplete_proof of incomplete_proof
  42   | Proof of ProofEngineTypes.proof
  43   | Intermediate of Cic.metasenv
  44       (* Status in which the proof could be while it is being processed by the
  45       * engine. No status entering/exiting the engine could be in it. *)
  46
  47 type ng_status =
  48   | ProofMode of NTacStatus.tac_status
  49   | CommandMode of NEstatus.status
  50
  51 class status =
  52  fun (mcr : GrafiteMarshal.moo) (ps : proof_status) (o : UriManager.uri list)
  53   (c : CoercDb.coerc_db) (ac : AutomationCache.cache) (b : string)
  54   (ns : ng_status)
  55  ->
  56   object
  57    val moo_content_rev = mcr
  58    val proof_status = ps
  59    val objects = o
  60    val coercions = c
  61    val automation_cache = ac
  62    val baseuri = b
  63    val ng_status = ns
  64    method moo_content_rev = moo_content_rev
  65    method set_moo_content_rev v = {< moo_content_rev = v >}
  66    method proof_status = proof_status
  67    method set_proof_status v = {< proof_status = v >}
  68    method objects = objects
  69    method set_objects v = {< objects = v >}
  70    method coercions = coercions
  71    method set_coercions v = {< coercions = v >}
  72    method automation_cache = automation_cache
  73    method set_automation_cache v = {< automation_cache = v >}
  74    method baseuri = baseuri
  75    method set_baseuri v = {< baseuri = v >}
  76    method ng_status = ng_status;
  77    method set_ng_status v = {< ng_status = v >}
  78  end
  79
  80 let get_estatus x =
  81   match x#ng_status with
  82   | ProofMode t -> (t :> NEstatus.status)
  83   | CommandMode e -> e
  84 ;;
  85
  86 let set_estatus e x =
  87  x#set_ng_status
  88   (match x#ng_status with
  89       ProofMode t -> ProofMode t#set_estatus e
  90     | CommandMode _ -> CommandMode e)
  91 ;;
  92
  93 let get_current_proof status =
  94   match status#proof_status with
  95   | Incomplete_proof { proof = p } -> p
  96   | Proof p -> p
  97   | _ -> raise (Statement_error "no ongoing proof")
  98
  99 let get_proof_metasenv status =
 100   match status#proof_status with
 101   | No_proof -> []
 102   | Proof (_, metasenv, _, _, _, _)
 103   | Incomplete_proof { proof = (_, metasenv, _, _, _, _) }
 104   | Intermediate metasenv ->
 105       metasenv
 106
 107 let get_stack status =
 108   match status#proof_status with
 109   | Incomplete_proof p -> p.stack
 110   | Proof _ -> Continuationals.Stack.empty
 111   | _ -> assert false
 112
 113 let set_stack stack status =
 114   match status#proof_status with
 115   | Incomplete_proof p ->
 116       status#set_proof_status (Incomplete_proof { p with stack = stack })
 117   | Proof _ ->
 118       assert (Continuationals.Stack.is_empty stack);
 119       status
 120   | _ -> assert false
 121
 122 let set_metasenv metasenv status =
 123   let proof_status =
 124     match status#proof_status with
 125     | No_proof -> Intermediate metasenv
 126     | Incomplete_proof ({ proof = (uri, _, subst, proof, ty, attrs) } as incomplete_proof) ->
 127         Incomplete_proof
 128           { incomplete_proof with proof = (uri, metasenv, subst, proof, ty, attrs) }
 129     | Intermediate _ -> Intermediate metasenv
 130     | Proof (_, metasenv', _, _, _, _) ->
 131        assert (metasenv = metasenv');
 132        status#proof_status
 133   in
 134    status#set_proof_status proof_status
 135
 136 let get_proof_context status goal =
 137   match status#proof_status with
 138   | Incomplete_proof { proof = (_, metasenv, _, _, _, _) } ->
 139       let (_, context, _) = CicUtil.lookup_meta goal metasenv in
 140       context
 141   | _ -> []
 142
 143 let get_proof_conclusion status goal =
 144   match status#proof_status with
 145   | Incomplete_proof { proof = (_, metasenv, _, _, _, _) } ->
 146       let (_, _, conclusion) = CicUtil.lookup_meta goal metasenv in
 147       conclusion
 148   | _ -> raise (Statement_error "no ongoing proof")
 149
 150 let add_moo_content cmds status =
 151   let content = status#moo_content_rev in
 152   let content' =
 153     List.fold_right
 154       (fun cmd acc ->
 155 (*         prerr_endline ("adding to moo command: " ^ GrafiteAstPp.pp_command cmd); *)
 156         match cmd with
 157         | GrafiteAst.Default _
 158         | GrafiteAst.Index _
 159         | GrafiteAst.Coercion _ ->
 160             if List.mem cmd content then acc
 161             else cmd :: acc
 162         | _ -> cmd :: acc)
 163       cmds content
 164   in
 165 (*   prerr_endline ("new moo content: " ^ String.concat " " (List.map
 166     GrafiteAstPp.pp_command content')); *)
 167    status#set_moo_content_rev content'
 168
 169 let get_baseuri status = status#baseuri;;
 170
 171 let dump_status status =
 172   HLog.message "status.aliases:\n";
 173   HLog.message "status.proof_status:";
 174   HLog.message
 175     (match status#proof_status with
 176     | No_proof -> "no proof\n"
 177     | Incomplete_proof _ -> "incomplete proof\n"
 178     | Proof _ -> "proof\n"
 179     | Intermediate _ -> "Intermediate\n");
 180   HLog.message "status.options\n";
 181   HLog.message "status.coercions\n";
 182   HLog.message "status.objects:\n";
 183   List.iter
 184     (fun u -> HLog.message (UriManager.string_of_uri u)) status#objects