This commit was manufactured by cvs2svn to create tag

[helm.git] / helm / matita / matitaEngine.ml

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 2a73193f6af3cc539048887dc5c738736f2aceb3..cb420d267ecf41f866a96dcb2695d1a95a93c00f 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -57,7 +57,7 @@ let tactic_of_ast = function
       Tactics.fold ~reduction ~term ~pattern
   | TacticAst.Fourier _ -> Tactics.fourier
   | TacticAst.FwdSimpl (_, hyp, names) -> 
-     Tactics.fwd_simpl ~mk_fresh_name_callback:(namer_of names) ~hyp ~dbd:(MatitaDb.instance ())
+     Tactics.fwd_simpl ~mk_fresh_name_callback:(namer_of names) ~dbd:(MatitaDb.instance ()) hyp
   | TacticAst.Generalize (_,pattern,ident) ->
      let names = match ident with None -> [] | Some id -> [id] in
      Tactics.generalize ~mk_fresh_name_callback:(namer_of names) pattern 
@@ -218,9 +218,22 @@ let generate_projections uri fields status =
            ("Unable to create projection " ^ name ^ " because it requires " ^ depend);
          status
   ) status projections
+
+(* to avoid a long list of recursive functions *)
+let eval_from_stream_ref = ref (fun _ _ _ -> assert false);;
  
 let eval_command status cmd =
   match cmd with
+  | TacticAst.Default (loc, what, uris) as cmd ->
+     LibraryObjects.set_default what uris;
+     {status with moo_content_rev =
+        (TacticAstPp.pp_command cmd ^ "\n") :: status.moo_content_rev}
+  | TacticAst.Include (loc, path) ->
+     let path = MatitaMisc.obj_file_of_script path in
+     let stream = Stream.of_channel (open_in path) in
+     let status = ref status in
+      !eval_from_stream_ref status stream (fun _ _ -> ());
+      !status
   | TacticAst.Set (loc, name, value) -> 
       let value = 
         if name = "baseuri" then
@@ -248,26 +261,31 @@ let eval_command status cmd =
       let obj = Cic.Constant (name,Some bo,ty,[],[]) in
       MatitaSync.add_obj uri obj status
   | TacticAst.Coercion (loc, coercion) -> 
-      eval_coercion status coercion
+      let status = eval_coercion status coercion in
+      let moo_content_rev =
+       (TacticAstPp.pp_cic_command
+         (TacticAst.Coercion (CicAst.dummy_floc,coercion)) ^ ".\n") ::
+       status.moo_content_rev in
+      {status with moo_content_rev = moo_content_rev}
   | TacticAst.Alias (loc, spec) -> 
-     (match spec with
+     let aliases =
+      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 }
+         DisambiguateTypes.Environment.add 
+          (DisambiguateTypes.Id id) 
+          (uri,(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 }
+         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 })
+         DisambiguateTypes.Environment.add 
+          (DisambiguateTypes.Num instance) 
+          (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases
+     in
+      MatitaSync.set_proof_aliases status aliases
   | TacticAst.Obj (loc,obj) ->
      let ext,name =
       match obj with
@@ -343,11 +361,8 @@ let disambiguate_term status term =
     | Intermediate _ -> Intermediate metasenv 
     | Proof _ -> assert false
   in
-  let status =
-    { status with
-        aliases = aliases;
-        proof_status = proof_status }
-  in
+  let status = { status with proof_status = proof_status } in
+  let status = MatitaSync.set_proof_aliases status aliases in
   status, cic
   
 let disambiguate_obj status obj =
@@ -373,11 +388,8 @@ let disambiguate_obj status obj =
     | Intermediate _
     | Proof _ -> assert false
   in
-  let status =
-    { status with
-        aliases = aliases;
-        proof_status = proof_status }
-  in
+  let status = { status with proof_status = proof_status } in
+  let status = MatitaSync.set_proof_aliases status aliases in
   status, cic
   
 let disambiguate_pattern status (wanted, hyp_paths, goal_path) =
@@ -528,12 +540,14 @@ and disambiguate_tacticals status tacticals =
   status, tacticals
   
 let disambiguate_command status = function
+  | TacticAst.Default _
+  | TacticAst.Alias _
+  | TacticAst.Include _ as cmd  -> status,cmd
   | TacticAst.Coercion (loc, term) ->
       let status, term = disambiguate_term status term in
       status, TacticAst.Coercion (loc,term)
   | (TacticAst.Set _ | TacticAst.Qed _ | TacticAst.Drop _ ) 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)
@@ -573,8 +587,13 @@ let eval_ast status ast =
 
 let eval_from_stream status str cb =
   let stl = CicTextualParser2.parse_statements str in
-  List.iter (fun ast -> cb !status ast;status := eval_ast !status ast) stl
+  List.iter
+   (fun ast -> cb !status ast;status := eval_ast !status ast) stl
+;;
 
+(* to avoid a long list of recursive functions *)
+eval_from_stream_ref := eval_from_stream;;
+  
 let eval_from_stream_greedy status str cb =
   while true do
     print_string "matita> ";
@@ -583,7 +602,8 @@ let eval_from_stream_greedy status str cb =
     cb !status ast;
     status := eval_ast !status ast 
   done
-  
+;;
+
 let eval_string status str =
   eval_from_stream status (Stream.of_string str) (fun _ _ -> ())
 
@@ -606,6 +626,7 @@ let default_options () =
 let initial_status =
   lazy {
     aliases = DisambiguateTypes.empty_environment;
+    moo_content_rev = [];
     proof_status = No_proof;
     options = default_options ();
     objects = [];