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 class status = fun (b : string) ->
  48  let fake_obj =
  49   NUri.uri_of_string "cic:/matita/dummy.decl",0,[],[],
  50    NCic.Constant([],"",None,NCic.Implicit `Closed,(`Provided,`Theorem,`Regular))
  51  in
  52   object
  53    val moo_content_rev = ([] : GrafiteMarshal.moo)
  54    val proof_status = No_proof
  55    val objects = ([] : UriManager.uri list)
  56    val coercions = CoercDb.empty_coerc_db
  57    val automation_cache = AutomationCache.empty ()
  58    val baseuri = b
  59    val ng_mode = (`CommandMode : [`CommandMode | `ProofMode])
  60    method moo_content_rev = moo_content_rev
  61    method set_moo_content_rev v = {< moo_content_rev = v >}
  62    method proof_status = proof_status
  63    method set_proof_status v = {< proof_status = v >}
  64    method objects = objects
  65    method set_objects v = {< objects = v >}
  66    method coercions = coercions
  67    method set_coercions v = {< coercions = v >}
  68    method automation_cache = automation_cache
  69    method set_automation_cache v = {< automation_cache = v >}
  70    method baseuri = baseuri
  71    method set_baseuri v = {< baseuri = v >}
  72    method ng_mode = ng_mode;
  73    method set_ng_mode v = {< ng_mode = v >}
  74    (* Warning: #stack and #obj are meaningful iff #ng_mode is `ProofMode *)
  75    inherit ([Continuationals.Stack.t] NTacStatus.status fake_obj (Continuationals.Stack.empty))
  76  end
  77
  78 let get_current_proof status =
  79   match status#proof_status with
  80   | Incomplete_proof { proof = p } -> p
  81   | Proof p -> p
  82   | _ -> raise (Statement_error "no ongoing proof")
  83
  84 let get_proof_metasenv status =
  85   match status#proof_status with
  86   | No_proof -> []
  87   | Proof (_, metasenv, _, _, _, _)
  88   | Incomplete_proof { proof = (_, metasenv, _, _, _, _) }
  89   | Intermediate metasenv ->
  90       metasenv
  91
  92 let get_stack status =
  93   match status#proof_status with
  94   | Incomplete_proof p -> p.stack
  95   | Proof _ -> Continuationals.Stack.empty
  96   | _ -> assert false
  97
  98 let set_stack stack status =
  99   match status#proof_status with
 100   | Incomplete_proof p ->
 101       status#set_proof_status (Incomplete_proof { p with stack = stack })
 102   | Proof _ ->
 103       assert (Continuationals.Stack.is_empty stack);
 104       status
 105   | _ -> assert false
 106
 107 let set_metasenv metasenv status =
 108   let proof_status =
 109     match status#proof_status with
 110     | No_proof -> Intermediate metasenv
 111     | Incomplete_proof ({ proof = (uri, _, subst, proof, ty, attrs) } as incomplete_proof) ->
 112         Incomplete_proof
 113           { incomplete_proof with proof = (uri, metasenv, subst, proof, ty, attrs) }
 114     | Intermediate _ -> Intermediate metasenv
 115     | Proof (_, metasenv', _, _, _, _) ->
 116        assert (metasenv = metasenv');
 117        status#proof_status
 118   in
 119    status#set_proof_status proof_status
 120
 121 let get_proof_context status goal =
 122   match status#proof_status with
 123   | Incomplete_proof { proof = (_, metasenv, _, _, _, _) } ->
 124       let (_, context, _) = CicUtil.lookup_meta goal metasenv in
 125       context
 126   | _ -> []
 127
 128 let get_proof_conclusion status goal =
 129   match status#proof_status with
 130   | Incomplete_proof { proof = (_, metasenv, _, _, _, _) } ->
 131       let (_, _, conclusion) = CicUtil.lookup_meta goal metasenv in
 132       conclusion
 133   | _ -> raise (Statement_error "no ongoing proof")
 134
 135 let add_moo_content cmds status =
 136   let content = status#moo_content_rev in
 137   let content' =
 138     List.fold_right
 139       (fun cmd acc ->
 140 (*         prerr_endline ("adding to moo command: " ^ GrafiteAstPp.pp_command cmd); *)
 141         match cmd with
 142         | GrafiteAst.Default _
 143         | GrafiteAst.Index _
 144         | GrafiteAst.Coercion _ ->
 145             if List.mem cmd content then acc
 146             else cmd :: acc
 147         | _ -> cmd :: acc)
 148       cmds content
 149   in
 150 (*   prerr_endline ("new moo content: " ^ String.concat " " (List.map
 151     GrafiteAstPp.pp_command content')); *)
 152    status#set_moo_content_rev content'
 153
 154 let dump_status status =
 155   HLog.message "status.aliases:\n";
 156   HLog.message "status.proof_status:";
 157   HLog.message
 158     (match status#proof_status with
 159     | No_proof -> "no proof\n"
 160     | Incomplete_proof _ -> "incomplete proof\n"
 161     | Proof _ -> "proof\n"
 162     | Intermediate _ -> "Intermediate\n");
 163   HLog.message "status.options\n";
 164   HLog.message "status.coercions\n";
 165   HLog.message "status.objects:\n";
 166   List.iter
 167     (fun u -> HLog.message (UriManager.string_of_uri u)) status#objects