X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaTypes.ml;h=8bd32bb23eac45b32f53f8f88f818bc391222f02;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=95618d142624e932493666da151773b8d9f412c5;hpb=4cb4d286a1fdcb150c2848a9d21ac3486906c317;p=helm.git

diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml
index 95618d142..8bd32bb23 100644
--- a/helm/matita/matitaTypes.ml
+++ b/helm/matita/matitaTypes.ml
@@ -1,4 +1,4 @@
-(* Copyright (C) 2004, HELM Team.
+(* Copyright (C) 2004-2005, HELM Team.
  * 
  * This file is part of HELM, an Hypertextual, Electronic
  * Library of Mathematics, developed at the Computer Science
@@ -25,171 +25,267 @@
 
 open Printf
 
-exception Not_implemented of string
-let not_implemented feature = raise (Not_implemented feature)
-
-exception Failure of string
-let error s = raise (Failure s)
-let warning s = prerr_endline ("MATITA WARNING:\t" ^ s)
-let debug_print s =
-  if BuildTimeConf.debug then prerr_endline ("MATITA DEBUG:\t" ^ s)
-
-let explain = function
-  | StatefulProofEngine.Tactic_failure exn ->
-      sprintf "Tactic failed: %s"(Printexc.to_string exn)
-  | StatefulProofEngine.Observer_failures exns ->
-      String.concat "\n"
-        (List.map (fun (_, exn) -> Printexc.to_string exn) exns)
-  | CicTextualParser2.Parse_error (floc, msg) ->
-      let (x, y) = CicAst.loc_of_floc floc in
-      sprintf "parse error at character %d-%d: %s" x y msg
-  | CicEnvironment.Object_not_found uri ->
-      sprintf "object not found: %s" (UriManager.string_of_uri uri)
-  | exn -> sprintf "Uncaught exception: %s" (Printexc.to_string exn)
-
-exception No_proof
-
+  (** user hit the cancel button *)
 exception Cancel
+
+  (** statement invoked in the wrong context (e.g. tactic with no ongoing proof)
+   *)
+exception Statement_error of string
+let statement_error msg = raise (Statement_error msg)
+
+exception Command_error of string
+let command_error msg = raise (Command_error msg)
+
+  (** parameters are: option name, error message *)
+exception Option_error of string * string
+
 exception Unbound_identifier of string
 
-(*
-let untitled_con_uri = UriManager.uri_of_string "cic:/untitled.con"
-let untitled_def_uri = UriManager.uri_of_string "cic:/untitled.ind"
+type incomplete_proof = {
+  proof: ProofEngineTypes.proof;
+  stack: Continuationals.Stack.t;
+}
 
-let unopt_uri ?(kind = `Con) = function
-  | Some uri -> uri
-  | None ->
-      (match kind with `Con -> untitled_con_uri | `Def -> untitled_def_uri)
-*)
-let unopt_uri = function Some uri -> uri | None -> assert false
+type proof_status =
+  | No_proof
+  | Incomplete_proof of incomplete_proof
+  | Proof of ProofEngineTypes.proof
+  | Intermediate of Cic.metasenv
+      (* Status in which the proof could be while it is being processed by the
+      * engine. No status entering/exiting the engine could be in it. *)
 
-class type parserr =  (* "parser" is a keyword :-( *)
-  object
-    method parseTerm:     char Stream.t -> DisambiguateTypes.term
-    method parseTactical: char Stream.t -> DisambiguateTypes.tactical
-  end
+module StringMap = Map.Make (String)
 
-class type console =
-  object
-    method echo_message   : string -> unit
-    method echo_error     : string -> unit
-    method clear          : unit -> unit
-    method wrap_exn       : 'a. (unit -> 'a) -> 'a option
-    method choose_uri     : string list -> string
-    method show : ?msg:string -> unit -> unit
-  end
+type option_value =
+  | String of string
+  | Int of int
+type options = option_value StringMap.t
+let no_options = StringMap.empty
 
-type choose_uris_callback =
-  selection_mode:[`MULTIPLE|`SINGLE] ->
-  ?title:string -> ?msg:string -> ?nonvars_button:bool ->
-  string list ->
-    string list
-type choose_interp_callback = (string * string) list list -> int list
+type ast_command = (CicNotationPt.term, GrafiteAst.obj) GrafiteAst.command
+type moo = ast_command list * GrafiteAst.metadata list
 
-class type disambiguator =
-  object
-    method env: DisambiguateTypes.environment
-    method setEnv: DisambiguateTypes.environment -> unit
-
-    method chooseUris: choose_uris_callback
-    method setChooseUris: choose_uris_callback -> unit
-
-    method chooseInterp: choose_interp_callback
-    method setChooseInterp: choose_interp_callback -> unit
-
-    method parserr: parserr
-
-    method disambiguateTerm:
-      ?context:Cic.context -> ?metasenv:Cic.metasenv ->
-      ?env:DisambiguateTypes.environment ->
-        char Stream.t ->
-          (DisambiguateTypes.environment * Cic.metasenv * Cic.term *
-           CicUniv.universe_graph)
-    method disambiguateTermAst:
-      ?context:Cic.context -> ?metasenv:Cic.metasenv ->
-      ?env:DisambiguateTypes.environment ->
-        DisambiguateTypes.term ->
-          (DisambiguateTypes.environment * Cic.metasenv * Cic.term *
-           CicUniv.universe_graph) 
-
-    method disambiguateTermAsts:
-      ?metasenv:Cic.metasenv ->
-      ?env:DisambiguateTypes.environment ->
-      DisambiguateTypes.term list ->
-          (DisambiguateTypes.environment * Cic.metasenv * Cic.term list *
-          CicUniv.universe_graph)
-  end
+type status = {
+  aliases: DisambiguateTypes.environment;
+  multi_aliases: DisambiguateTypes.multiple_environment;
+  moo_content_rev: moo;
+  proof_status: proof_status;
+  options: options;
+  objects: (UriManager.uri * string) list;
+  coercions: UriManager.uri list;
+  notation_ids: CicNotation.notation_id list;
+}
 
-class type proof =
-  object
-    inherit [unit] StatefulProofEngine.status
+let set_metasenv metasenv status =
+  let proof_status =
+    match status.proof_status with
+    | No_proof -> Intermediate metasenv
+    | Incomplete_proof ({ proof = (uri, _, proof, ty) } as incomplete_proof) ->
+        Incomplete_proof
+          { incomplete_proof with proof = (uri, metasenv, proof, ty) }
+    | Intermediate _ -> Intermediate metasenv 
+    | Proof _ -> assert false
+  in
+  { status with proof_status = proof_status }
 
-    method toXml: Xml.token Stream.t * Xml.token Stream.t
-    method toString: string
-  end
+let dump_status status = 
+  MatitaLog.message "status.aliases:\n";
+  MatitaLog.message "status.proof_status:"; 
+  MatitaLog.message
+    (match status.proof_status with
+    | No_proof -> "no proof\n"
+    | Incomplete_proof _ -> "incomplete proof\n"
+    | Proof _ -> "proof\n"
+    | Intermediate _ -> "Intermediate\n");
+  MatitaLog.message "status.options\n";
+  StringMap.iter (fun k v -> 
+    let v = 
+      match v with
+      | String s -> s
+      | Int i -> string_of_int i
+    in
+    MatitaLog.message (k ^ "::=" ^ v)) status.options;
+  MatitaLog.message "status.coercions\n";
+  MatitaLog.message "status.objects:\n";
+  List.iter 
+    (fun (u,_) -> 
+      MatitaLog.message (UriManager.string_of_uri u)) status.objects 
+  
+let get_option status name =
+  try
+    StringMap.find name status.options
+  with Not_found -> raise (Option_error (name, "not found"))
 
-class type currentProof =
-  object
-    method onGoing: unit -> bool
-    method proof: proof
-    method start: proof -> unit
-    method abort: unit -> unit
-    method quit: unit -> unit
-  end
+let get_string_option status name =
+  match get_option status name with
+  | String s -> s
+  | _ -> raise (Option_error (name, "not a string value"))
 
-type command_outcome = bool * bool
+let set_option status name value =
+  let mangle_dir s =
+    let s = Str.global_replace (Str.regexp "//+") "/" s in
+    let s = Str.global_replace (Str.regexp "/$") "" s in
+    s
+  in
+  let types =
+    [ "baseuri", (`String, mangle_dir);
+      "basedir", (`String, mangle_dir);
+    ]
+  in
+  let ty_and_mangler =
+    try
+      List.assoc name types
+    with Not_found -> command_error (sprintf "Unknown option \"%s\"" name)
+  in
+  let value =
+    match ty_and_mangler with
+    | `String, f -> String (f value)
+    | `Int, f ->
+        (try
+          Int (int_of_string (f value))
+        with Failure _ ->
+          command_error (sprintf "Not an integer value \"%s\"" value))
+  in
+  if StringMap.mem name status.options && name = "baseuri" then
+    command_error "Redefinition of 'baseuri' is forbidden."
+  else
+    { status with options = StringMap.add name value status.options }
 
-type script_item =
-  [ `Tactic
-  | `Theorem
-  | `Qed of UriManager.uri
-  | `Def of UriManager.uri
-  | `Inductive of UriManager.uri
-  ]
+let add_moo_content cmds status =
+  let content, metadata = status.moo_content_rev in
+  let content' =
+    List.fold_right
+      (fun cmd acc ->
+(*         prerr_endline ("adding to moo command: " ^ GrafiteAstPp.pp_command cmd); *)
+        match cmd with
+        | GrafiteAst.Interpretation _
+        | GrafiteAst.Default _ ->
+            if List.mem cmd content then acc
+            else cmd :: acc
+        | GrafiteAst.Alias _ -> (* move Alias as the last inserted one *)
+            cmd :: (List.filter ((<>) cmd) acc)
+        | _ -> cmd :: acc)
+      cmds content
+  in
+(*   prerr_endline ("new moo content: " ^ String.concat " " (List.map
+    GrafiteAstPp.pp_command content')); *)
+  { status with moo_content_rev = content', metadata }
 
-class type interpreter =
+let add_moo_metadata new_metadata status =
+  let content, metadata = status.moo_content_rev in
+  let metadata' =
+    List.fold_left
+      (fun acc m ->
+        match m with
+        | GrafiteAst.Dependency buri ->
+            let is_self = (* self dependency *)
+              try
+                get_string_option status "baseuri" = buri
+              with Option_error _ -> false  (* baseuri not yet set *)
+            in
+            if is_self
+              || List.exists (GrafiteAst.eq_metadata m) metadata (* duplicate *)
+            then acc
+            else m :: acc
+        | _ -> m :: acc)
+      metadata new_metadata
+  in
+  { status with moo_content_rev = content, metadata' }
+
+  (* subset of MatitaConsole.console methods needed by MatitaInterpreter *)
+class type console =
   object
-    method evalAst : DisambiguateTypes.tactical -> command_outcome
-    method evalPhrase : string -> command_outcome
-(*     method evalStream: char Stream.t -> command_outcome *)
-    method endOffset : int
-    method lastItem: script_item option
-    method setState: [`Proof | `Command] -> unit
-    method setEvalAstCallback: (DisambiguateTypes.tactical -> unit) -> unit
+    method clear : unit -> unit
+    method echo_error : string -> unit
+    method echo_message : string -> unit
+    method wrap_exn : 'a. (unit -> 'a) -> 'a option
+    method choose_uri : string list -> string
+    method show : ?msg:string -> unit -> unit
   end
 
-type term_source =
-  [ `Ast of DisambiguateTypes.term
+type abouts =
+  [ `Blank
+  | `Current_proof
+  | `Us
+  ]
+  
+type mathViewer_entry =
+  [ `About of abouts  (* current proof *)
+  | `Check of string (* term *)
   | `Cic of Cic.term * Cic.metasenv
-  | `String of string
+  | `Dir of string (* "directory" in cic uris namespace *)
+  | `Uri of UriManager.uri (* cic object uri *)
+  | `Whelp of string * UriManager.uri list (* query and results *)
   ]
 
-class type mathViewer =
-  object
-    method checkTerm: term_source -> unit
-  end
+let string_of_entry = function
+  | `About `Blank -> "about:blank"
+  | `About `Current_proof -> "about:proof"
+  | `About `Us -> "about:us"
+  | `Check _ -> "check:"
+  | `Cic (_, _) -> "term:"
+  | `Dir uri -> uri
+  | `Uri uri -> UriManager.string_of_uri uri
+  | `Whelp (query, _) -> query
+
+let entry_of_string = function
+  | "about:blank" -> `About `Blank
+  | "about:proof" -> `About `Current_proof
+  | "about:us"    -> `About `Us
+  | _ ->  (* only about entries supported ATM *)
+      raise (Invalid_argument "entry_of_string")
 
-class type cicBrowser =
+class type mathViewer =
   object
-    method loadUri: string -> unit
-    method loadTerm: term_source -> unit
+    (** @param reuse if set reused last opened cic browser otherwise 
+     *  opens a new one. default is false
+     *)
+    method show_entry: ?reuse:bool -> mathViewer_entry -> unit
+    method show_uri_list:
+      ?reuse:bool -> entry:mathViewer_entry -> UriManager.uri list -> unit
   end
+  
+let qualify status name = get_string_option status "baseuri" ^ "/" ^ name
 
-type mml_of_cic_sequent =
-  Cic.metasenv -> Cic.conjecture ->
-    Gdome.document *
-    ((Cic.id, Cic.term) Hashtbl.t *
-    (Cic.id, Cic.id option) Hashtbl.t *
-    (string, Cic.hypothesis) Hashtbl.t)
+let get_current_proof status =
+  match status.proof_status with
+  | Incomplete_proof { proof = p } -> p
+  | _ -> statement_error "no ongoing proof"
 
-type mml_of_cic_object =
-  explode_all:bool -> UriManager.uri -> Cic.annobj ->
-  (string, string) Hashtbl.t -> (string, Cic2acic.anntypes) Hashtbl.t ->
-    Gdome.document
+let get_proof_metasenv status =
+  match status.proof_status with
+  | No_proof -> []
+  | Proof (_, metasenv, _, _)
+  | Incomplete_proof { proof = (_, metasenv, _, _) }
+  | Intermediate metasenv ->
+      metasenv
 
-type namer = ProofEngineTypes.mk_fresh_name_type
+let get_proof_context status goal =
+  match status.proof_status with
+  | Incomplete_proof { proof = (_, metasenv, _, _) } ->
+      let (_, context, _) = CicUtil.lookup_meta goal metasenv in
+      context
+  | _ -> []
+ 
+let get_proof_conclusion status goal =
+  match status.proof_status with
+  | Incomplete_proof { proof = (_, metasenv, _, _) } ->
+      let (_, _, conclusion) = CicUtil.lookup_meta goal metasenv in
+      conclusion
+  | _ -> statement_error "no ongoing proof"
 
-let mono_uris_callback ~selection_mode ?title ?msg ?nonvars_button _ =
-  raise (Failure "ambiguous input")
-let mono_interp_callback _ = raise (Failure "ambiguous input")
+let get_stack status =
+  match status.proof_status with
+  | Incomplete_proof p -> p.stack
+  | Proof _ -> Continuationals.Stack.empty
+  | _ -> assert false
 
+let set_stack stack status =
+  match status.proof_status with
+  | Incomplete_proof p ->
+      { status with proof_status = Incomplete_proof { p with stack = stack } }
+  | Proof _ ->
+      assert (Continuationals.Stack.is_empty stack);
+      status
+  | _ -> assert false
+