X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=aa056f3e2c35585c8d4c599bdbf055913918f1a9;hb=6beda5aa100b617b75d88a5a519b5022c99208a0;hp=e8e3171a08fa9290bd0d8405c63d0238843d7522;hpb=1ca749a387695a5a4abc138a06de496a63abac4a;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index e8e3171a0..aa056f3e2 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -33,13 +33,11 @@ exception IncludedFileNotCompiled of string * string
 exception Macro of
  GrafiteAst.loc *
   (Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro)
-exception ReadOnlyUri of string
 
 type 'a disambiguator_input = string * int * 'a
 
 type options = { 
   do_heavy_checks: bool ; 
-  clean_baseuri: bool
 }
 
 (** create a ProofEngineTypes.mk_fresh_name_type function which uses given
@@ -128,7 +126,6 @@ let rec tactic_of_ast status ast =
         | `Normalize ->
             PET.const_lazy_reduction
               (CicReduction.normalize ~delta:false ~subst:[])
-        | `Reduce -> PET.const_lazy_reduction ProofEngineReduction.reduce
         | `Simpl -> PET.const_lazy_reduction ProofEngineReduction.simpl
         | `Unfold None ->
             PET.const_lazy_reduction (ProofEngineReduction.unfold ?what:None)
@@ -163,7 +160,6 @@ let rec tactic_of_ast status ast =
   | GrafiteAst.Reduce (_, reduction_kind, pattern) ->
       (match reduction_kind with
 	 | `Normalize -> Tactics.normalize ~pattern
-	 | `Reduce -> Tactics.reduce ~pattern  
 	 | `Simpl -> Tactics.simpl ~pattern 
 	 | `Unfold what -> Tactics.unfold ~pattern what
 	 | `Whd -> Tactics.whd ~pattern)
@@ -410,7 +406,6 @@ type eval_ast =
     Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro) ->
 
   ?do_heavy_checks:bool ->
-  ?clean_baseuri:bool ->
   GrafiteTypes.status ->
   (('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement)
   disambiguator_input ->
@@ -482,10 +477,10 @@ let refinement_toolkit = {
   RefinementTool.pack_coercion_obj = CicRefine.pack_coercion_obj;
  }
   
-let eval_coercion status ~add_composites uri arity saturations baseuri =
+let eval_coercion status ~add_composites uri arity saturations =
  let status,compounds =
   GrafiteSync.add_coercion ~add_composites refinement_toolkit status uri arity
-   saturations baseuri
+   saturations (GrafiteTypes.get_baseuri status)
  in
  let moo_content = 
    List.map coercion_moo_statement_of ((uri,arity,saturations)::compounds)
@@ -570,6 +565,7 @@ let add_coercions_of_record_to_moo obj lemmas status =
           with Not_found -> false,0            
         with Not_found -> assert false
       in
+      let buri = GrafiteTypes.get_baseuri status in
       (* looking at the fields we can know the 'wanted' coercions, but not the 
        * actually generated ones. So, only the intersection between the wanted
        * and the actual should be in the moo as coercion, while everithing in
@@ -579,8 +575,7 @@ let add_coercions_of_record_to_moo obj lemmas status =
           (function 
             | (name,true,arity) -> 
                Some 
-                 (arity, UriManager.uri_of_string 
-                   (GrafiteTypes.qualify status name ^ ".con"))
+                 (arity, UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con" ))
             | _ -> None) 
           fields
       in
@@ -649,8 +644,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
       let status = GrafiteTypes.add_moo_content [cmd] status in
       status,[] 
   | GrafiteAst.Coercion (loc, uri, add_composites, arity, saturations) ->
-     eval_coercion status ~add_composites uri arity saturations
-      (GrafiteTypes.get_string_option status "baseuri")
+     eval_coercion status ~add_composites uri arity saturations 
   | GrafiteAst.Default (loc, what, uris) as cmd ->
      LibraryObjects.set_default what uris;
      GrafiteTypes.add_moo_content [cmd] status,[]
@@ -685,7 +679,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
      status,[]
   | GrafiteAst.Print (_,"proofterm") ->
       let _,_,_,p,_, _ = GrafiteTypes.get_current_proof status in
-      print_endline (Auto.pp_proofterm p);
+      prerr_endline (Auto.pp_proofterm p);
       status,[]
   | GrafiteAst.Print (_,_) -> status,[]
   | GrafiteAst.Qed loc ->
@@ -715,37 +709,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
   | GrafiteAst.Relation (loc, id, a, aeq, refl, sym, trans) -> 
      Setoids.add_relation id a aeq refl sym trans;
      status, [] (*CSC: TO BE FIXED *)
-  | GrafiteAst.Set (loc, name, value) -> 
-      if name = "baseuri" then begin
-        let value = 
-          let v = Http_getter_misc.strip_trailing_slash value in
-          try
-            ignore (String.index v ' ');
-            GrafiteTypes.command_error "baseuri can't contain spaces"
-          with Not_found -> v
-        in
-        if Http_getter_storage.is_read_only value then begin
-          HLog.error (Printf.sprintf "uri %s belongs to a read-only repository" value);
-          raise (ReadOnlyUri value)
-        end;
-        if (not (Http_getter_storage.is_empty ~local:true value) ||
-            LibraryClean.db_uris_of_baseuri value <> [])
-           && opts.clean_baseuri 
-          then begin
-          HLog.message ("baseuri " ^ value ^ " is not empty");
-          HLog.message ("cleaning baseuri " ^ value);
-          LibraryClean.clean_baseuris [value];
-          assert (Http_getter_storage.is_empty ~local:true value);
-        end;
-        if not (Helm_registry.get_opt_default Helm_registry.bool "matita.nodisk"
-                  ~default:false) 
-        then
-          HExtlib.mkdir 
-            (Filename.dirname 
-              (Http_getter.filename ~local:true ~writable:true (value ^
-              "/foo.con")));
-      end;
-      GrafiteTypes.set_option status name value,[]
+  | GrafiteAst.Set (loc, name, value) -> status, []
+(*       GrafiteTypes.set_option status name value,[] *)
   | GrafiteAst.Obj (loc,obj) ->
      let ext,name =
       match obj with
@@ -755,8 +720,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
           ".ind",
           (match types with (name,_,_,_)::_ -> name | _ -> assert false)
        | _ -> assert false in
-     let uri = 
-       UriManager.uri_of_string (GrafiteTypes.qualify status name ^ ext) in
+     let buri = GrafiteTypes.get_baseuri status in 
+     let uri = UriManager.uri_of_string (buri ^ "/" ^ name ^ ext) in
      let obj = CicRefine.pack_coercion_obj obj in
      let metasenv = GrafiteTypes.get_proof_metasenv status in
      match obj with
@@ -860,13 +825,10 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
        status)
     status moo
 } and eval_ast = {ea_go = fun ~disambiguate_tactic ~disambiguate_command
-~disambiguate_macro ?(do_heavy_checks=false) ?(clean_baseuri=true) status
+~disambiguate_macro ?(do_heavy_checks=false) status
 (text,prefix_len,st)
 ->
-  let opts = {
-    do_heavy_checks = do_heavy_checks ; 
-    clean_baseuri = clean_baseuri }
-  in
+  let opts = { do_heavy_checks = do_heavy_checks ; } in
   match st with
   | GrafiteAst.Executable (_,ex) ->
      eval_executable.ee_go ~disambiguate_tactic ~disambiguate_command