X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaEngine.ml;h=f0d8ee46c7820b34feff186135edcd418b9b4fd4;hb=771ee8b9d122fa963881c876e86f90531bb7434f;hp=7302e3bde0ff6d5e2b5b012192e87f78fa56ad14;hpb=e32693f30563379989b75b53c3be088396b732da;p=helm.git

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 7302e3bde..f0d8ee46c 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -1,575 +1,142 @@
+(* Copyright (C) 2005, 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://helm.cs.unibo.it/
+ *)
+
+(* $Id$ *)
 
 open Printf
-open MatitaTypes
 
 let debug = false ;;
 let debug_print = if debug then prerr_endline else ignore ;;
 
-(** create a ProofEngineTypes.mk_fresh_name_type function which uses given
-  * names as long as they are available, then it fallbacks to name generation
-  * using FreshNamesGenerator module *)
-let namer_of names =
-  let len = List.length names in
-  let count = ref 0 in
-  fun metasenv context name ~typ ->
-    if !count < len then begin
-      let name = Cic.Name (List.nth names !count) in
-      incr count;
-      name
-    end else
-      FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ
-
-let tactic_of_ast = function
-  | TacticAst.Intros (_, None, names) ->
-      (* TODO Zack implement intros length *)
-      PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) ()
-  | TacticAst.Intros (_, Some num, names) ->
-      (* TODO Zack implement intros length *)
-      PrimitiveTactics.intros_tac ~howmany:num
-        ~mk_fresh_name_callback:(namer_of names) ()
-  | TacticAst.Reflexivity _ -> Tactics.reflexivity
-  | TacticAst.Assumption _ -> Tactics.assumption
-  | TacticAst.Contradiction _ -> Tactics.contradiction
-(*
-  | TacticAst.Discriminate (_,id) -> Tactics.discriminate id
-*)
-  | TacticAst.Exists _ -> Tactics.exists
-  | TacticAst.Fourier _ -> Tactics.fourier
-  | TacticAst.Generalize (_,term,pat) -> Tactics.generalize term pat
-  | TacticAst.Goal (_, n) -> Tactics.set_goal n
-  | TacticAst.Left _ -> Tactics.left
-  | TacticAst.Right _ -> Tactics.right
-  | TacticAst.Ring _ -> Tactics.ring
-  | TacticAst.Split _ -> Tactics.split
-  | TacticAst.Symmetry _ -> Tactics.symmetry
-  | TacticAst.Transitivity (_, term) -> Tactics.transitivity term
-  | TacticAst.Apply (_, term) -> Tactics.apply term
-  | TacticAst.Absurd (_, term) -> Tactics.absurd term
-  | TacticAst.Exact (_, term) -> Tactics.exact term
-  | TacticAst.Cut (_, term) -> Tactics.cut term
-  | TacticAst.Elim (_, term, _) ->
-      (* TODO Zack implement "using" argument *)
-      (* old: Tactics.elim_intros_simpl term *)
-      Tactics.elim_intros term
-  | TacticAst.ElimType (_, term) -> Tactics.elim_type term
-  | TacticAst.Replace (_, what, with_what) -> Tactics.replace ~what ~with_what
-  | TacticAst.Auto (_,depth) -> 
-(*       AutoTactic.auto_tac ~num (MatitaDb.instance ()) *)
-      AutoTactic.auto_tac_new ?depth ~dbd:(MatitaDb.instance ()) ()
-  | TacticAst.Change (_, what, with_what, _) -> Tactics.change ~what ~with_what
-(*
-  (* TODO Zack a lot more of tactics to be implemented here ... *)
-  | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
-  | TacticAst.Change of 'term * 'term * 'ident option
-  | TacticAst.Decompose of 'ident * 'ident list
-  | TacticAst.Fold of reduction_kind * 'term
-  | TacticAst.Injection of 'ident
-  | TacticAst.Replace_pattern of 'term pattern * 'term
-*)
-  | TacticAst.LetIn (loc,term,name) ->
-      Tactics.letin term ~mk_fresh_name_callback:(namer_of [name])
-  | TacticAst.Reduce (_, reduction_kind, pattern) ->
-      (match reduction_kind with
-      | `Normalize -> Tactics.normalize ~pattern
-      | `Reduce -> Tactics.reduce ~pattern  
-      | `Simpl -> Tactics.simpl ~pattern 
-      | `Whd -> Tactics.whd ~pattern)
-  | TacticAst.Rewrite (_, dir, t, pattern) ->
-      if dir = `Left then
-        EqualityTactics.rewrite_tac ~where:pattern ~term:t ()
-      else
-        EqualityTactics.rewrite_back_tac ~where:pattern ~term:t ()
-  | TacticAst.FwdSimpl (_, name) -> 
-     Tactics.fwd_simpl ~hyp:(Cic.Name name) ~dbd:(MatitaDb.instance ())
-  | TacticAst.LApply (_, term, substs) ->
-     let f (name, term) = Cic.Name name, term in
-     Tactics.lapply ~substs:(List.map f substs) term
-
-let eval_tactical status tac =
-  let apply_tactic tactic =
-    let (proof, goals) =
-      ProofEngineTypes.apply_tactic tactic (MatitaMisc.get_proof_status status)
-    in
-    let new_status =
-      match goals with
-      | [] -> 
-          let (_,metasenv,_,_) = proof in
-          (match metasenv with
-          | [] -> Proof proof
-          | (ng,_,_)::_ -> Incomplete_proof (proof,ng))
-      | ng::_ -> Incomplete_proof (proof, ng)
-    in
-    { status with proof_status = new_status }
-  in
-  let rec tactical_of_ast = function
-    | TacticAst.Tactic (loc, tactic) -> tactic_of_ast tactic
-    | TacticAst.Fail loc -> Tacticals.fail
-    | TacticAst.Do (loc, num, tactical) ->
-        Tacticals.do_tactic num (tactical_of_ast tactical)
-    | TacticAst.IdTac loc -> Tacticals.id_tac
-    | TacticAst.Repeat (loc, tactical) ->
-        Tacticals.repeat_tactic (tactical_of_ast tactical)
-    | TacticAst.Seq (loc, tacticals) ->  (* tac1; tac2; ... *)
-        Tacticals.seq (List.map tactical_of_ast tacticals)
-    | TacticAst.Then (loc, tactical, tacticals) ->  (* tac; [ tac1 | ... ] *)
-        Tacticals.thens (tactical_of_ast tactical)
-          (List.map tactical_of_ast tacticals)
-    | TacticAst.Tries (loc, tacticals) ->
-        Tacticals.try_tactics
-          (List.map (fun t -> "", tactical_of_ast t) tacticals)
-    | TacticAst.Try (loc, tactical) ->
-        Tacticals.try_tactic (tactical_of_ast tactical)
-  in
-  apply_tactic (tactical_of_ast tac)
-
-let eval_coercion status coercion = 
-  let coer_uri,coer_ty =
-    match coercion with 
-    | Cic.Const (uri,_)
-    | Cic.Var (uri,_) ->
-        let o,_ = 
-          CicEnvironment.get_obj CicUniv.empty_ugraph uri 
-        in
-        (match o with
-        | Cic.Constant (_,_,ty,_,_)
-        | Cic.Variable (_,_,ty,_,_) ->
-            uri,ty
-        | _ -> assert false)
-    | Cic.MutConstruct (uri,t,c,_) ->
-        let o,_ = 
-          CicEnvironment.get_obj CicUniv.empty_ugraph uri 
-        in
-        (match o with
-        | Cic.InductiveDefinition (l,_,_,_) ->
-            let (_,_,_,cl) = List.nth l t in
-            let (_,cty) = List.nth cl c in
-              uri,cty
-        | _ -> assert false)
-    | _ -> assert false 
-  in
-  (* we have to get the source and the tgt type uri 
-   * in Coq syntax we have already their names, but 
-   * since we don't support Funclass and similar I think
-   * all the coercion should be of the form
-   * (A:?)(B:?)T1->T2
-   * So we should be able to extract them from the coercion type
-   *)
-  let extract_last_two_p ty =
-    let rec aux = function
-      | Cic.Prod( _, src, Cic.Prod (n,t1,t2)) -> aux (Cic.Prod(n,t1,t2))   
-      | Cic.Prod( _, src, tgt) -> src, tgt
-      | _ -> assert false
-    in  
-    aux ty
-  in
-  let ty_src,ty_tgt = extract_last_two_p coer_ty in
-  let context = [] in 
-  let src_uri = 
-    let ty_src = CicReduction.whd context ty_src in
-     CicUtil.uri_of_term ty_src
-  in
-  let tgt_uri = 
-    let ty_tgt = CicReduction.whd context ty_tgt in
-     CicUtil.uri_of_term ty_tgt
-  in
-  let new_coercions =
-    (* also adds them to the Db *)
-    CoercGraph.close_coercion_graph src_uri tgt_uri coer_uri in
-  let status =
-   List.fold_left (fun s (uri,o,ugraph) -> MatitaSync.add_obj uri o status)
-    status new_coercions in
-  {status with proof_status = No_proof}
-
-let generate_elimination_principles uri status =
- let elim sort status =
-   try
-    let uri,obj = CicElim.elim_of ~sort uri 0 in
-     MatitaSync.add_obj uri obj status
-   with CicElim.Can_t_eliminate -> status
+let disambiguate_tactic lexicon_status_ref grafite_status goal tac =
+ let metasenv,tac =
+  GrafiteDisambiguate.disambiguate_tactic
+   lexicon_status_ref
+   (GrafiteTypes.get_proof_context grafite_status goal)
+   (GrafiteTypes.get_proof_metasenv grafite_status)
+   tac
  in
- List.fold_left (fun status sort -> elim sort status) status
-  [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ]
-
-let generate_projections uri fields status =
- let projections = CicRecord.projections_of uri fields in
-  List.fold_left
-   (fun status (uri, name, bo) -> 
-     try 
-      let ty, ugraph = 
-        CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in
-      let bo = Unshare.unshare bo in
-      let ty = Unshare.unshare ty in
-      let attrs = [`Class `Projection; `Generated] in
-      let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
-       MatitaSync.add_obj uri obj status
+  GrafiteTypes.set_metasenv metasenv grafite_status,tac
+
+let disambiguate_command lexicon_status_ref grafite_status cmd =
+ let lexicon_status,metasenv,cmd =
+  GrafiteDisambiguate.disambiguate_command
+   ~baseuri:(
+     try
+      Some (GrafiteTypes.get_string_option grafite_status "baseuri")
      with
-        CicTypeChecker.TypeCheckerFailure s ->
-         MatitaLog.message 
-          ("Unable to create projection " ^ name ^ " cause: " ^ s);
-         status
-      | CicEnvironment.Object_not_found uri ->
-         let depend = UriManager.name_of_uri uri in
-          MatitaLog.message 
-           ("Unable to create projection " ^ name ^ " because it requires " ^ depend);
-         status
-  ) status projections
- 
-let eval_command status cmd =
-  match cmd with
-  | TacticAst.Set (loc, name, value) -> set_option status name value
-  | TacticAst.Qed loc ->
-      let uri, metasenv, bo, ty = 
-        match status.proof_status with
-        | Proof (Some uri, metasenv, body, ty) ->
-            uri, metasenv, body, ty
-        | Proof (None, metasenv, body, ty) -> 
-            command_error 
-              ("Someone allows to start a thm without giving the "^
-               "name/uri. This should be fixed!")
-        | _-> command_error "You can't qed an uncomplete theorem"
-      in
-      let suri = UriManager.string_of_uri uri in
-      if metasenv <> [] then 
-        command_error "Proof not completed! metasenv is not empty!";
-      let name = UriManager.name_of_uri uri in
-      let obj = Cic.Constant (name,Some bo,ty,[],[]) in
-      MatitaSync.add_obj uri obj status
-  | TacticAst.Coercion (loc, coercion) -> 
-      eval_coercion status coercion
-  | TacticAst.Alias (loc, spec) -> 
-     (match spec with
-      | TacticAst.Ident_alias (id,uri) -> 
-          {status with aliases = 
-            DisambiguateTypes.Environment.add 
-              (DisambiguateTypes.Id id) 
-              ("boh?",(fun _ _ _ -> CicUtil.term_of_uri (UriManager.uri_of_string uri)))
-              status.aliases }
-      | TacticAst.Symbol_alias (symb, instance, desc) ->
-          {status with aliases = 
-            DisambiguateTypes.Environment.add 
-              (DisambiguateTypes.Symbol (symb,instance))
-              (DisambiguateChoices.lookup_symbol_by_dsc symb desc) 
-              status.aliases }
-      | TacticAst.Number_alias (instance,desc) ->
-          {status with aliases = 
-            DisambiguateTypes.Environment.add 
-              (DisambiguateTypes.Num instance) 
-              (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases })
-  | TacticAst.Obj (loc,obj) ->
-     let ext,name =
-      match obj with
-         Cic.Constant (name,_,_,_,_)
-       | Cic.CurrentProof (name,_,_,_,_,_) -> ".con",name
-       | Cic.InductiveDefinition (types,_,_,_) ->
-          ".ind",
-          (match types with (name,_,_,_)::_ -> name | _ -> assert false)
-       | _ -> assert false in
-     let uri = 
-       UriManager.uri_of_string (MatitaMisc.qualify status name ^ ext) 
-     in
-     let metasenv = MatitaMisc.get_proof_metasenv status in
-     match obj with
-        Cic.CurrentProof (_,metasenv',bo,ty,_,_) ->
-         assert (metasenv = metasenv');
-         let goalno =
-          match metasenv' with (goalno,_,_)::_ -> goalno | _ -> assert false in
-         let initial_proof = (Some uri, metasenv, bo, ty) in
-          { status with proof_status = Incomplete_proof (initial_proof,goalno)}
-      | _ ->
-        if metasenv <> [] then
-         command_error (
-           "metasenv not empty while giving a definition with body: " ^
-           CicMetaSubst.ppmetasenv metasenv []);
-        let status = MatitaSync.add_obj uri obj status in
-         match obj with
-            Cic.Constant _ -> status
-          | Cic.InductiveDefinition (_,_,_,attrs) ->
-             let status = generate_elimination_principles uri status in
-             let rec get_record_attrs =
-              function
-                 [] -> None
-               | (`Class (`Record fields))::_ -> Some fields
-               | _::tl -> get_record_attrs tl
-             in
-              (match get_record_attrs attrs with
-                  None -> status (* not a record *)
-                | Some fields -> generate_projections uri fields status)
-          | Cic.CurrentProof _
-          | Cic.Variable _ -> assert false
-
-let eval_executable status ex =
-  match ex with
-  | TacticAst.Tactical (_, tac) -> eval_tactical status tac
-  | TacticAst.Command (_, cmd) -> eval_command status cmd
-  | TacticAst.Macro (_, mac) -> 
-      command_error (sprintf "The macro %s can't be in a script" 
-        (TacticAstPp.pp_macro_cic mac))
-
-let eval_comment status c = status
-            
-let eval status st =
-  match st with
-  | TacticAst.Executable (_,ex) -> eval_executable status ex
-  | TacticAst.Comment (_,c) -> eval_comment status c
-
-let disambiguate_term status term =
-  let (aliases, metasenv, cic, _) =
-    match
-      MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
-        ~aliases:(status.aliases) ~context:(MatitaMisc.get_proof_context status)
-        ~metasenv:(MatitaMisc.get_proof_metasenv status) term
-    with
-    | [x] -> x
-    | _ -> assert false
-  in
-  let proof_status =
-    match status.proof_status with
-    | No_proof -> Intermediate metasenv
-    | Incomplete_proof ((uri, _, proof, ty), goal) ->
-        Incomplete_proof ((uri, metasenv, proof, ty), goal)
-    | Intermediate _ -> Intermediate metasenv 
-    | Proof _ -> assert false
-  in
-  let status =
-    { status with
-        aliases = aliases;
-        proof_status = proof_status }
-  in
-  status, cic
-  
-let disambiguate_obj status obj =
-  let uri =
-   match obj with
-      TacticAst.Inductive (_,(name,_,_,_)::_)
-    | TacticAst.Record (_,name,_,_) ->
-       Some (UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".ind"))
-    | TacticAst.Inductive _ -> assert false
-    | _ -> None in
-  let (aliases, metasenv, cic, _) =
-    match
-      MatitaDisambiguator.disambiguate_obj ~dbd:(MatitaDb.instance ())
-        ~aliases:(status.aliases) ~uri obj
-    with
-    | [x] -> x
-    | _ -> assert false
-  in
-  let proof_status =
-    match status.proof_status with
-    | No_proof -> Intermediate metasenv
-    | Incomplete_proof _
-    | Intermediate _
-    | Proof _ -> assert false
-  in
-  let status =
-    { status with
-        aliases = aliases;
-        proof_status = proof_status }
-  in
-  status, cic
-  
-let disambiguate_pattern aliases (hyp_paths ,goal_path) =
-  let interp path = Disambiguate.interpretate_path [] aliases path in
-  let goal_path = 
-    match goal_path with 
-    | None -> None
-    | Some path -> Some (interp path) in
-  let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
-  (hyp_paths ,goal_path)
-  
-let disambiguate_tactic status = function
-  | TacticAst.Transitivity (loc, term) -> 
-      let status, cic = disambiguate_term status term in
-      status, TacticAst.Transitivity (loc, cic)
-  | TacticAst.Apply (loc, term) ->
-      let status, cic = disambiguate_term status term in
-      status, TacticAst.Apply (loc, cic)
-  | TacticAst.Absurd (loc, term) -> 
-      let status, cic = disambiguate_term status term in
-      status, TacticAst.Absurd (loc, cic)
-  | TacticAst.Exact (loc, term) -> 
-      let status, cic = disambiguate_term status term in
-      status, TacticAst.Exact (loc, cic)
-  | TacticAst.Cut (loc, term) -> 
-      let status, cic = disambiguate_term status term in
-      status, TacticAst.Cut (loc, cic)
-  | TacticAst.Elim (loc, term, Some term') ->
-      let status, cic1 = disambiguate_term status term in
-      let status, cic2 = disambiguate_term status term' in
-      status, TacticAst.Elim (loc, cic1, Some cic2)
-  | TacticAst.Elim (loc, term, None) ->
-      let status, cic = disambiguate_term status term in
-      status, TacticAst.Elim (loc, cic, None)
-  | TacticAst.ElimType (loc, term) -> 
-      let status, cic = disambiguate_term status term in
-      status, TacticAst.ElimType (loc, cic)
-  | TacticAst.Replace (loc, what, with_what) -> 
-      let status, cic1 = disambiguate_term status what in
-      let status, cic2 = disambiguate_term status with_what in
-      status, TacticAst.Replace (loc, cic1, cic2)
-  | TacticAst.Change (loc, what, with_what, ident) -> 
-      let status, cic1 = disambiguate_term status what in
-      let status, cic2 = disambiguate_term status with_what in
-      status, TacticAst.Change (loc, cic1, cic2, ident)
-  | TacticAst.Generalize (loc,term,pattern) ->
-      let status,term = disambiguate_term status term in
-      let pattern = disambiguate_pattern status.aliases pattern in
-      status, TacticAst.Generalize(loc,term,pattern)
-(*
-  (* TODO Zack a lot more of tactics to be implemented here ... *)
-  | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
-  | TacticAst.Change of 'term * 'term * 'ident option
-  | TacticAst.Decompose of 'ident * 'ident list
-  | TacticAst.Discriminate of 'ident
-  | TacticAst.Fold of reduction_kind * 'term
-  | TacticAst.Injection of 'ident
-  | TacticAst.Replace_pattern of 'term pattern * 'term
-*)
-  | TacticAst.LetIn (loc, term, name) ->
-      let status, term = disambiguate_term status term in
-      status, TacticAst.LetIn (loc,term,name)
-  | TacticAst.Reduce (loc, reduction_kind, pattern) ->
-      let pattern = disambiguate_pattern status.aliases pattern in
-      status, TacticAst.Reduce(loc, reduction_kind, pattern)
-  | TacticAst.Rewrite (loc, dir, t, pattern) ->
-      let status, term = disambiguate_term status t in
-      let pattern = disambiguate_pattern status.aliases pattern in
-      status, TacticAst.Rewrite (loc, dir, term, pattern)
-  | TacticAst.Intros (loc, num, names) ->
-      status, TacticAst.Intros (loc, num, names)
-  | TacticAst.Auto (loc,num) -> status, TacticAst.Auto (loc,num)
-  | TacticAst.Reflexivity loc -> status, TacticAst.Reflexivity loc
-  | TacticAst.Assumption loc -> status, TacticAst.Assumption loc
-  | TacticAst.Contradiction loc -> status, TacticAst.Contradiction loc
-  | TacticAst.Exists loc -> status, TacticAst.Exists loc 
-  | TacticAst.Fourier loc -> status, TacticAst.Fourier loc
-  | TacticAst.Left loc -> status, TacticAst.Left loc
-  | TacticAst.Right loc -> status, TacticAst.Right loc
-  | TacticAst.Ring loc -> status, TacticAst.Ring loc
-  | TacticAst.Split loc -> status, TacticAst.Split loc
-  | TacticAst.Symmetry loc -> status, TacticAst.Symmetry loc
-  | TacticAst.Goal (loc, g) -> status, TacticAst.Goal (loc, g)
-  | TacticAst.FwdSimpl (loc, name) -> status, TacticAst.FwdSimpl (loc, name)  
-  | TacticAst.LApply (loc, term, substs) ->
-     let f (status, substs) (name, term) =
-        let status, term = disambiguate_term status term in
-	status, (name, term) :: substs
+      GrafiteTypes.Option_error _ -> None)
+   !lexicon_status_ref (GrafiteTypes.get_proof_metasenv grafite_status) cmd
+ in
+  lexicon_status_ref := lexicon_status;
+  GrafiteTypes.set_metasenv metasenv grafite_status,cmd
+
+let disambiguate_macro lexicon_status_ref grafite_status macro context =
+ let metasenv,macro =
+  GrafiteDisambiguate.disambiguate_macro
+   lexicon_status_ref
+   (GrafiteTypes.get_proof_metasenv grafite_status)
+   context macro
+ in
+  GrafiteTypes.set_metasenv metasenv grafite_status,macro
+
+let eval_ast ?do_heavy_checks ?clean_baseuri lexicon_status
+ grafite_status ast
+=
+ let lexicon_status_ref = ref lexicon_status in
+ let new_grafite_status,new_objs =
+  GrafiteEngine.eval_ast
+   ~disambiguate_tactic:(disambiguate_tactic lexicon_status_ref)
+   ~disambiguate_command:(disambiguate_command lexicon_status_ref)
+   ~disambiguate_macro:(disambiguate_macro lexicon_status_ref)
+   ?do_heavy_checks ?clean_baseuri grafite_status ast in
+ let new_lexicon_status =
+  LexiconSync.add_aliases_for_objs !lexicon_status_ref new_objs in
+ let new_aliases =
+  LexiconSync.alias_diff ~from:lexicon_status new_lexicon_status in
+ let _,intermediate_states = 
+  let baseuri = GrafiteTypes.get_string_option new_grafite_status "baseuri" in
+  List.fold_left
+   (fun (lexicon_status,acc) (k,((v,_) as value)) -> 
+     let b =
+      try
+       UriManager.buri_of_uri (UriManager.uri_of_string v) = baseuri
+      with
+       UriManager.IllFormedUri _ -> false (* v is a description, not a URI *)
      in
-     let status, term = disambiguate_term status term in
-     let status, substs = List.fold_left f (status, []) substs in 
-     status, TacticAst.LApply (loc, term, substs)
-
-let rec disambiguate_tactical status = function 
-  | TacticAst.Tactic (loc, tactic) -> 
-      let status, tac = disambiguate_tactic status tactic in
-      status, TacticAst.Tactic (loc, tac)
-  | TacticAst.Do (loc, num, tactical) ->
-      let status, tac = disambiguate_tactical status tactical in
-      status, TacticAst.Do (loc, num, tac)
-  | TacticAst.Repeat (loc, tactical) -> 
-      let status, tac = disambiguate_tactical status tactical in
-      status, TacticAst.Repeat (loc, tac)
-  | TacticAst.Seq (loc, tacticals) ->  (* tac1; tac2; ... *)
-      let status, tacticals = disambiguate_tacticals status tacticals in
-      let tacticals = List.rev tacticals in
-      status, TacticAst.Seq (loc, tacticals)
-  | TacticAst.Then (loc, tactical, tacticals) ->  (* tac; [ tac1 | ... ] *)
-      let status, tactical = disambiguate_tactical status tactical in
-      let status, tacticals = disambiguate_tacticals status tacticals in
-      status, TacticAst.Then (loc, tactical, tacticals)
-  | TacticAst.Tries (loc, tacticals) ->
-      let status, tacticals = disambiguate_tacticals status tacticals in
-      status, TacticAst.Tries (loc, tacticals)
-  | TacticAst.Try (loc, tactical) ->
-      let status, tactical = disambiguate_tactical status tactical in
-      status, TacticAst.Try (loc, tactical)
-  | (TacticAst.IdTac _ | TacticAst.Fail _) as tac ->
-      status, tac
-
-and disambiguate_tacticals status tacticals =
-  let status, tacticals =
-    List.fold_left
-      (fun (status, tacticals) tactical ->
-        let status, tac = disambiguate_tactical status tactical in
-        status, tac :: tacticals)
-      (status, [])
-      tacticals
-  in
-  let tacticals = List.rev tacticals in
-  status, tacticals
-  
-let disambiguate_command status = function
-  | TacticAst.Coercion (loc, term) ->
-      let status, term = disambiguate_term status term in
-      status, TacticAst.Coercion (loc,term)
-  | (TacticAst.Set _ | TacticAst.Qed _) as cmd ->
-      status, cmd
-  | TacticAst.Alias _ as x -> status, x
-  | TacticAst.Obj (loc,obj) ->
-      let status,obj = disambiguate_obj status obj in
-       status, TacticAst.Obj (loc,obj)
-
-let disambiguate_executable status ex =
-  match ex with
-  | TacticAst.Tactical (loc, tac) ->
-      let status, tac = disambiguate_tactical status tac in
-      status, (TacticAst.Tactical (loc, tac))
-  | TacticAst.Command (loc, cmd) ->
-      let status, cmd = disambiguate_command status cmd in
-      status, (TacticAst.Command (loc, cmd))
-  | TacticAst.Macro (_, mac) -> 
-      command_error (sprintf "The macro %s can't be in a script" 
-        (TacticAstPp.pp_macro_ast mac))
-
-let disambiguate_comment status c = 
-  match c with
-  | TacticAst.Note (loc,n) -> status, TacticAst.Note (loc,n)
-  | TacticAst.Code (loc,ex) -> 
-        let status, ex = disambiguate_executable status ex in
-        status, TacticAst.Code (loc,ex)
-        
-let disambiguate_statement status statement =
-  match statement with
-  | TacticAst.Comment (loc,c) -> 
-        let status, c = disambiguate_comment status c in
-        status, TacticAst.Comment (loc,c)
-  | TacticAst.Executable (loc,ex) -> 
-        let status, ex = disambiguate_executable status ex in
-        status, TacticAst.Executable (loc,ex)
-  
-let eval_ast status ast =
-  let status,st = disambiguate_statement status ast in
-  (* this disambiguation step should be deferred to support tacticals *)
-  eval status st
-
-let eval_from_stream status str cb =
-  let stl = CicTextualParser2.parse_statements str in
-  List.fold_left 
-    (fun status ast -> cb status ast;eval_ast status ast) status 
-  stl
-  
-let eval_string status str =
-  eval_from_stream status (Stream.of_string str) (fun _ _ -> ())
-
-let default_options () =
-  let options =
-    StringMap.add "baseuri"
-      (String
-        (Helm_registry.get "matita.baseuri" ^ Helm_registry.get "matita.owner"))
-      no_options
-  in
-  let options =
-    StringMap.add "basedir"
-      (String (Helm_registry.get "matita.basedir" ))
-      options
+      if b then 
+       lexicon_status,acc
+      else
+       let new_lexicon_status =
+        LexiconEngine.set_proof_aliases lexicon_status [k,value]
+       in
+        new_lexicon_status,
+         ((new_grafite_status,new_lexicon_status),Some (k,value))::acc
+   ) (lexicon_status,[]) new_aliases
+ in
+  ((new_grafite_status,new_lexicon_status),None)::intermediate_states
+
+let eval_from_stream ~first_statement_only ~include_paths ?(prompt=false)
+ ?do_heavy_checks ?clean_baseuri lexicon_status grafite_status str cb 
+=
+ let rec loop lexicon_status grafite_status statuses =
+  let loop =
+   if first_statement_only then
+    fun _ _ _ -> raise End_of_file
+   else
+    loop
   in
-  options
-
-let initial_status =
-  lazy {
-    aliases = DisambiguateTypes.empty_environment;
-    proof_status = No_proof;
-    options = default_options ();
-    objects = [];
-  }
-
-
+   if prompt then (print_string "matita> "; flush stdout);
+   try
+    let lexicon_status,ast =
+     GrafiteParser.parse_statement ~include_paths str lexicon_status
+    in
+     (match ast with
+         GrafiteParser.LNone _ ->
+          loop lexicon_status grafite_status
+           (((grafite_status,lexicon_status),None)::statuses)
+       | GrafiteParser.LSome ast ->
+          cb grafite_status ast;
+          let new_statuses =
+           eval_ast ?do_heavy_checks ?clean_baseuri lexicon_status
+            grafite_status ast in
+          let grafite_status,lexicon_status =
+           match new_statuses with
+              [] -> assert false
+            | (s,_)::_ -> s
+          in
+           loop lexicon_status grafite_status (new_statuses @ statuses))
+   with
+    End_of_file -> statuses
+ in
+  loop lexicon_status grafite_status []
+;;
+
+let eval_string ~first_statement_only ~include_paths ?do_heavy_checks
+ ?clean_baseuri lexicon_status status str
+=
+ eval_from_stream ~first_statement_only ~include_paths ?do_heavy_checks
+  ?clean_baseuri lexicon_status status (Ulexing.from_utf8_string str)
+  (fun _ _ -> ())