X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgrafite_engine%2FgrafiteEngine.ml;h=65dd17b6a096c1e144daf7068e80cf49cba2ce2d;hb=0c8963a0f3aef05cf4866e8bcd3fdbebddac8b87;hp=26d7712d39fc1e104b75dc8d4ad49215e339fff7;hpb=e66e67d2f9f2772d63a7457e386f9616f62a2f39;p=helm.git

diff --git a/helm/ocaml/grafite_engine/grafiteEngine.ml b/helm/ocaml/grafite_engine/grafiteEngine.ml
index 26d7712d3..65dd17b6a 100644
--- a/helm/ocaml/grafite_engine/grafiteEngine.ml
+++ b/helm/ocaml/grafite_engine/grafiteEngine.ml
@@ -25,11 +25,14 @@
 
 (* $Id$ *)
 
+open Printf
+
 exception Drop
 exception IncludedFileNotCompiled of string (* file name *)
 exception Macro of
  GrafiteAst.loc *
   (Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro)
+exception ReadOnlyUri of string
 
 type options = { 
   do_heavy_checks: bool ; 
@@ -92,6 +95,8 @@ let tactic_of_ast ast =
   | GrafiteAst.Fold (_, reduction_kind, term, pattern) ->
       let reduction =
         match reduction_kind with
+        | `Demodulate -> 
+            GrafiteTypes.command_error "demodulation can't be folded"
         | `Normalize ->
             PET.const_lazy_reduction
               (CicReduction.normalize ~delta:false ~subst:[])
@@ -133,11 +138,12 @@ let tactic_of_ast ast =
       Tactics.letin term ~mk_fresh_name_callback:(namer_of [name])
   | 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)
+	 | `Demodulate -> Tactics.demodulate ~dbd:(LibraryDb.instance ()) ~pattern
+	 | `Normalize -> Tactics.normalize ~pattern
+	 | `Reduce -> Tactics.reduce ~pattern  
+	 | `Simpl -> Tactics.simpl ~pattern 
+	 | `Unfold what -> Tactics.unfold ~pattern what
+	 | `Whd -> Tactics.whd ~pattern)
   | GrafiteAst.Reflexivity _ -> Tactics.reflexivity
   | GrafiteAst.Replace (_, pattern, with_what) ->
      Tactics.replace ~pattern ~with_what
@@ -391,6 +397,7 @@ let coercion_moo_statement_of uri =
 let eval_coercion status ~add_composites uri =
  let basedir = Helm_registry.get "matita.basedir" in
  let status,compounds =
+   prerr_endline "evaluating a coercion command";
   GrafiteSync.add_coercion ~basedir ~add_composites status uri in
  let moo_content = coercion_moo_statement_of uri in
  let status = GrafiteTypes.add_moo_content [moo_content] status in
@@ -516,18 +523,14 @@ let add_coercions_of_record_to_moo obj lemmas status =
                 None) 
             lemmas)
       in
+      prerr_endline "actual coercions:";
       List.iter 
         (fun u -> prerr_endline (UriManager.string_of_uri u)) 
         coercions;
-      let status = GrafiteTypes.add_moo_content moo_content status in
-      let basedir = Helm_registry.get "matita.basedir" in
-      List.fold_left 
-        (fun (status,lemmas) uri ->
-          let status,new_lemmas =
-           GrafiteSync.add_coercion ~basedir ~add_composites:true status uri
-          in
-           status,new_lemmas@lemmas
-        ) (status,[]) coercions
+      let status = GrafiteTypes.add_moo_content moo_content status in 
+      {status with 
+        GrafiteTypes.coercions = coercions @ status.GrafiteTypes.coercions}, 
+      lemmas
 
 let add_obj uri obj status =
  let basedir = Helm_registry.get "matita.basedir" in
@@ -544,7 +547,6 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd ->
      GrafiteTypes.add_moo_content [cmd] status,[]
   | GrafiteAst.Include (loc, baseuri) ->
      let moopath = LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri in
-     let metadatapath= LibraryMisc.metadata_file_of_baseuri ~basedir ~baseuri in
      if not (Sys.file_exists moopath) then
        raise (IncludedFileNotCompiled moopath);
      let status = eval_from_moo.efm_go status moopath in
@@ -555,11 +557,15 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd ->
           let v = Http_getter_misc.strip_trailing_slash value in
           try
             ignore (String.index v ' ');
-            raise (GrafiteTypes.Command_error "baseuri can't contain spaces")
+            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 (sprintf "uri %s belongs to a read-only repository" value);
+          raise (ReadOnlyUri value)
+        end;
         if not (GrafiteMisc.is_empty value) && opts.clean_baseuri then begin
-          HLog.warn ("baseuri " ^ value ^ " is not empty");
+          HLog.message ("baseuri " ^ value ^ " is not empty");
           HLog.message ("cleaning baseuri " ^ value);
           LibraryClean.clean_baseuris ~basedir [value];
         end;
@@ -637,9 +643,6 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd ->
                   "\nPlease use a variant."));
            end;
          assert (metasenv = metasenv');
-         let goalno =
-           match metasenv' with (goalno,_,_)::_ -> goalno | _ -> assert false 
-         in
          let initial_proof = (Some uri, metasenv, bo, ty) in
          let initial_stack = Continuationals.Stack.of_metasenv metasenv in
          { status with GrafiteTypes.proof_status =