X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaEngine.ml;h=89481b287434a12284dedd67c24e76c08acee8e5;hb=33a02e0b639217093eb63f30169aaa6ac8c78907;hp=a9b46267f98c9ba1a032ce6a9315aac3d04cadfe;hpb=d1126c6b78a3333bbf415daf027004496b77c2f4;p=helm.git

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index a9b46267f..89481b287 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -24,6 +24,7 @@
  *)
 
 open Printf
+
 open MatitaTypes
 
 exception Drop;;
@@ -156,7 +157,7 @@ let tactic_of_ast ast =
   | GrafiteAst.Transitivity (_, term) -> Tactics.transitivity term
 
 let singleton = function
-  | [x] -> x
+  | [x], _ -> x
   | _ -> assert false
 
 let disambiguate_term status_ref term =
@@ -192,9 +193,7 @@ let disambiguate_lazy_term status_ref term =
     cic, metasenv, ugraph)
 
 let disambiguate_pattern status_ref (wanted, hyp_paths, goal_path) =
-  let interp path =
-    Disambiguate.interpretate_path [] !status_ref.aliases path
-  in
+  let interp path = Disambiguate.interpretate_path [] path in
   let goal_path = interp goal_path in
   let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
   let wanted =
@@ -355,7 +354,7 @@ module MatitaStatus =
   let set_goals (status,_) goals = status,goals
 
   let id_tac status =
-    apply_tactic (GrafiteAst.IdTac Disambiguate.dummy_floc) status
+    apply_tactic (GrafiteAst.IdTac DisambiguateTypes.dummy_floc) status
 
   let mk_tactic tac = tac
 
@@ -453,21 +452,18 @@ let eval_coercion status coercion =
    List.fold_left (fun s (uri,o,ugraph) -> MatitaSync.add_obj uri o status)
     status new_coercions in
   let statement_of name =
-    GrafiteAstPp.pp_statement 
-      (GrafiteAst.Executable (Disambiguate.dummy_floc,
-        (GrafiteAst.Command (Disambiguate.dummy_floc,
-          (GrafiteAst.Coercion (Disambiguate.dummy_floc, 
-            (CicNotationPt.Ident (name, None)))))))) ^ "\n"
+    GrafiteAst.Coercion (DisambiguateTypes.dummy_floc, 
+      (CicNotationPt.Ident (name, None)))
   in
-  let moo_content_rev =
-    [statement_of (UriManager.name_of_uri coer_uri)] @ 
+  let moo_content = 
+    statement_of (UriManager.name_of_uri coer_uri) ::
     (List.map 
       (fun (uri, _, _) -> 
         statement_of (UriManager.name_of_uri uri))
-    new_coercions) @ status.moo_content_rev 
+    new_coercions)
   in
-  let status =  {status with moo_content_rev = moo_content_rev} in
-  {status with proof_status = No_proof}
+  let status = add_moo_content moo_content status in
+  { status with proof_status = No_proof }
 
 let generate_elimination_principles uri status =
  let elim sort status =
@@ -513,12 +509,9 @@ let disambiguate_obj status obj =
     | GrafiteAst.Inductive _ -> assert false
     | GrafiteAst.Theorem _ -> None in
   let (aliases, metasenv, cic, _) =
-    match
-      MatitaDisambiguator.disambiguate_obj ~dbd:(MatitaDb.instance ())
-        ~aliases:(status.aliases) ~uri obj
-    with
-    | [x] -> x
-    | _ -> assert false
+    singleton
+      (MatitaDisambiguator.disambiguate_obj ~dbd:(MatitaDb.instance ())
+        ~aliases:(status.aliases) ~uri obj)
   in
   let proof_status =
     match status.proof_status with
@@ -576,8 +569,7 @@ let eval_command opts status cmd =
   match cmd with
   | GrafiteAst.Default (loc, what, uris) as cmd ->
      LibraryObjects.set_default what uris;
-     {status with moo_content_rev =
-        (GrafiteAstPp.pp_command cmd ^ "\n") :: status.moo_content_rev}
+     add_moo_content [cmd] status
   | GrafiteAst.Include (loc, path) ->
      let absolute_path = make_absolute opts.include_paths path in
      let moopath = MatitaMisc.obj_file_of_script absolute_path in
@@ -612,7 +604,7 @@ let eval_command opts status cmd =
       set_option status name value
   | GrafiteAst.Drop loc -> raise Drop
   | GrafiteAst.Qed loc ->
-      let uri, metasenv, bo, ty = 
+      let uri, metasenv, bo, ty =
         match status.proof_status with
         | Proof (Some uri, metasenv, body, ty) ->
             uri, metasenv, body, ty
@@ -636,27 +628,33 @@ let eval_command opts status cmd =
              code in DisambiguatePp *)
       match spec with
       | GrafiteAst.Ident_alias (id,uri) -> 
-         DisambiguateTypes.Environment.add 
+         DisambiguateTypes.Environment.cons
           (DisambiguateTypes.Id id) 
           (uri,(fun _ _ _-> CicUtil.term_of_uri (UriManager.uri_of_string uri)))
           status.aliases 
       | GrafiteAst.Symbol_alias (symb, instance, desc) ->
-         DisambiguateTypes.Environment.add
+         DisambiguateTypes.Environment.cons
           (DisambiguateTypes.Symbol (symb,instance))
           (DisambiguateChoices.lookup_symbol_by_dsc symb desc)
           status.aliases
       | GrafiteAst.Number_alias (instance,desc) ->
-         DisambiguateTypes.Environment.add
+         DisambiguateTypes.Environment.cons
           (DisambiguateTypes.Num instance)
           (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases
      in
       MatitaSync.set_proof_aliases status aliases
   | GrafiteAst.Render _ -> assert false (* ZACK: to be removed *)
   | GrafiteAst.Dump _ -> assert false   (* ZACK: to be removed *)
-  | GrafiteAst.Interpretation _
-  | GrafiteAst.Notation _ as stm ->
-      { status with moo_content_rev =
-        (GrafiteAstPp.pp_command stm ^ "\n") :: status.moo_content_rev }
+  | GrafiteAst.Interpretation (_, dsc, (symbol, _), _) as stm ->
+      let status' = add_moo_content [stm] status in
+      let aliases' =
+        DisambiguateTypes.Environment.cons
+          (DisambiguateTypes.Symbol (symbol, 0))
+          (DisambiguateChoices.lookup_symbol_by_dsc symbol dsc)
+          status.aliases
+      in
+      MatitaSync.set_proof_aliases status' aliases'
+  | GrafiteAst.Notation _ as stm -> add_moo_content [stm] status
   | GrafiteAst.Obj (loc,obj) ->
      let ext,name =
       match obj with