It is now possible for commands processed by grafiteEngine to either return

uris for an old object or for a new one. This information is only used to
generate preferences.

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index ebba1988dab1a22ab3f9069d9321b807dcd0d526..6b341f77c314a581e130e7e9e7f55ad712821334 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -414,7 +414,7 @@ type eval_ast =
   GrafiteTypes.status ->
   (('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement)
   disambiguator_input ->
-  GrafiteTypes.status * UriManager.uri list
+  GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list]
  }
 
 type 'a eval_command =
@@ -424,7 +424,7 @@ type 'a eval_command =
     GrafiteTypes.status * (Cic.term,Cic.obj) GrafiteAst.command) -> 
   options -> GrafiteTypes.status -> 
     (('term,'obj) GrafiteAst.command) disambiguator_input ->
-   GrafiteTypes.status * UriManager.uri list
+   GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list]
  }
 
 type 'a eval_comment =
@@ -434,7 +434,7 @@ type 'a eval_comment =
     GrafiteTypes.status * (Cic.term,Cic.obj) GrafiteAst.command) -> 
   options -> GrafiteTypes.status -> 
     (('term,'lazy_term,'reduction_kind,'obj,'ident) GrafiteAst.comment) disambiguator_input ->
-   GrafiteTypes.status * UriManager.uri list
+   GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list]
  }
 
 type 'a eval_executable =
@@ -460,7 +460,7 @@ type 'a eval_executable =
   options ->
   GrafiteTypes.status ->
   (('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.code) disambiguator_input ->
-  GrafiteTypes.status * UriManager.uri list
+  GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list]
  }
 
 type 'a eval_from_moo =
@@ -473,7 +473,7 @@ let coercion_moo_statement_of (uri,arity, saturations,_) =
 let eval_unification_hint status t n = 
   (* XXX no undo *)        
   NCicUnifHint.add_user_provided_hint t n;
-  status,[]
+  status,`Old []
 ;;
 
 let add_coercions_of_lemmas lemmas status =
@@ -514,7 +514,7 @@ let eval_prefer_coercion status c =
  let status = GrafiteSync.prefer_coercion status uri in
  let moo_content = GrafiteAst.PreferCoercion (HExtlib.dummy_floc,c) in
  let status = GrafiteTypes.add_moo_content [moo_content] status in 
- status, []  
+ status, `Old []
 
 module MatitaStatus =
  struct
@@ -648,9 +648,9 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
      prerr_endline msg;
 *)
       let status = GrafiteTypes.add_moo_content [cmd] status in
-      status,[] 
+      status,`Old [] 
   | GrafiteAst.Select (_,uri) as cmd ->
-      if List.mem cmd status.GrafiteTypes.moo_content_rev then status, []
+      if List.mem cmd status.GrafiteTypes.moo_content_rev then status, `Old []
       else 
        let cache = 
          AutomationCache.add_term_to_active status.GrafiteTypes.automation_cache
@@ -658,31 +658,36 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
        in
        let status = { status with GrafiteTypes.automation_cache = cache } in
        let status = GrafiteTypes.add_moo_content [cmd] status in
-       status, []
+       status, `Old []
   | GrafiteAst.Pump (_,steps) ->
       let cache = 
         AutomationCache.pump status.GrafiteTypes.automation_cache steps
       in
       let status = { status with GrafiteTypes.automation_cache = cache } in
-      status, []
+      status, `Old []
   | GrafiteAst.PreferCoercion (loc, coercion) ->
      eval_prefer_coercion status coercion
   | GrafiteAst.Coercion (loc, uri, add_composites, arity, saturations) ->
-     eval_coercion status ~add_composites uri arity saturations 
+     let res,uris =
+      eval_coercion status ~add_composites uri arity saturations
+     in
+      res,`Old uris
   | GrafiteAst.Inverter (loc, name, indty, params) ->
      let buri = GrafiteTypes.get_baseuri status in 
      let uri = UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con") in
      let indty_uri = 
        try CicUtil.uri_of_term indty
        with Invalid_argument _ ->
-         raise (Invalid_argument "not an inductive type to invert")
+         raise (Invalid_argument "not an inductive type to invert") in
+     let res,uris =
+      Inversion_principle.build_inverter ~add_obj status uri indty_uri params
      in
-     Inversion_principle.build_inverter ~add_obj status uri indty_uri params
+      res,`Old uris
   | GrafiteAst.UnificationHint (loc, t, n) ->
      eval_unification_hint status t n
   | GrafiteAst.Default (loc, what, uris) as cmd ->
      LibraryObjects.set_default what uris;
-     GrafiteTypes.add_moo_content [cmd] status,[]
+     GrafiteTypes.add_moo_content [cmd] status,`Old []
   | GrafiteAst.Drop loc -> raise Drop
   | GrafiteAst.Include (loc, baseuri) ->
      let moopath_rw, moopath_r = 
@@ -711,12 +716,12 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
      in
      prerr_endline msg;
 *)
-     status,[]
+     status,`Old []
   | GrafiteAst.Print (_,"proofterm") ->
       let _,_,_,p,_, _ = GrafiteTypes.get_current_proof status in
       prerr_endline (Auto.pp_proofterm (Lazy.force p));
-      status,[]
-  | GrafiteAst.Print (_,_) -> status,[]
+      status,`Old []
+  | GrafiteAst.Print (_,_) -> status,`Old []
   | GrafiteAst.Qed loc ->
       let uri, metasenv, _subst, bo, ty, attrs =
         match status.GrafiteTypes.proof_status with
@@ -740,7 +745,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
        {status with 
          GrafiteTypes.proof_status = GrafiteTypes.No_proof},
         (*CSC: I throw away the arities *)
-        uri::lemmas
+        `Old (uri::lemmas)
   | GrafiteAst.NQed loc ->
       (match status.GrafiteTypes.ng_status with
        | GrafiteTypes.ProofMode
@@ -758,12 +763,12 @@ prerr_endline "CSC: here we should fix the height!!!";
                NCicLibrary.add_obj uri obj;
                {status with 
                  GrafiteTypes.ng_status = 
-                  GrafiteTypes.CommandMode lexicon_status },[]
+                  GrafiteTypes.CommandMode lexicon_status },`Old []
        | _ -> raise (GrafiteTypes.Command_error "Not in proof mode"))
   | 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) -> status, []
+     status, `Old [] (*CSC: TO BE FIXED *)
+  | GrafiteAst.Set (loc, name, value) -> status, `Old []
 (*       GrafiteTypes.set_option status name value,[] *)
   | GrafiteAst.NObj (loc,obj) ->
      let lexicon_status =
@@ -783,7 +788,8 @@ prerr_endline "CSC: here we should fix the height!!!";
           in
            NCicLibrary.add_obj uri obj;
            {status with 
-             GrafiteTypes.ng_status=GrafiteTypes.CommandMode lexicon_status },[]
+             GrafiteTypes.ng_status=GrafiteTypes.CommandMode lexicon_status },
+           `Old []
       | _ ->
         let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
         { status with
@@ -791,7 +797,7 @@ prerr_endline "CSC: here we should fix the height!!!";
             GrafiteTypes.ProofMode
              { NTacStatus.gstatus = ninitial_stack; 
                istatus = { NTacStatus.pstatus = obj; lstatus = lexicon_status}}
-             },[])
+             },`Old [])
   | GrafiteAst.Obj (loc,obj) ->
      let ext,name =
       match obj with
@@ -845,18 +851,16 @@ prerr_endline "CSC: here we should fix the height!!!";
             GrafiteTypes.Incomplete_proof
             { GrafiteTypes.proof = initial_proof; stack = initial_stack } ;
          },
-          []
+          `Old []
      | _ ->
          if metasenv <> [] then
           raise (GrafiteTypes.Command_error (
             "metasenv not empty while giving a definition with body: " ^
             CicMetaSubst.ppmetasenv [] metasenv));
          let status, lemmas = add_obj uri obj status in 
-         let status,new_lemmas =
-          add_coercions_of_lemmas lemmas status
-         in
+         let status,new_lemmas = add_coercions_of_lemmas lemmas status in
           {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},
-           uri::new_lemmas@lemmas
+           `Old (uri::new_lemmas@lemmas)
  in
   match status.GrafiteTypes.proof_status with
      GrafiteTypes.Intermediate _ ->
@@ -879,10 +883,10 @@ prerr_endline "CSC: here we should fix the height!!!";
        print_endline "GOOD"; () 
      with ProofEngineTypes.Fail _ -> print_endline "BAD" | _ -> ());*)
       eval_tactical status
-       (punctuation_tactical_of_ast (text,prefix_len,punct)),[]
+       (punctuation_tactical_of_ast (text,prefix_len,punct)),`Old []
   | GrafiteAst.Tactic (_, None, punct) ->
       eval_tactical status
-       (punctuation_tactical_of_ast (text,prefix_len,punct)),[]
+       (punctuation_tactical_of_ast (text,prefix_len,punct)),`Old []
   | GrafiteAst.NTactic (_(*loc*), tac, punct) ->
       (match  status.GrafiteTypes.ng_status with
       | GrafiteTypes.CommandMode _ -> assert false
@@ -890,14 +894,14 @@ prerr_endline "CSC: here we should fix the height!!!";
          let nstatus = eval_ng_tac (text,prefix_len,tac) nstatus in
          let nstatus = eval_ng_punct (text,prefix_len,punct) nstatus in
          NTacStatus.pp_tac_status nstatus;
-         { status with GrafiteTypes.ng_status = GrafiteTypes.ProofMode nstatus }, [])
+         { status with GrafiteTypes.ng_status = GrafiteTypes.ProofMode nstatus }, `Old [])
   | GrafiteAst.NonPunctuationTactical (_, tac, punct) ->
      let status = 
       eval_tactical status
        (non_punctuation_tactical_of_ast (text,prefix_len,tac))
      in
       eval_tactical status
-       (punctuation_tactical_of_ast (text,prefix_len,punct)),[]
+       (punctuation_tactical_of_ast (text,prefix_len,punct)),`Old []
   | GrafiteAst.Command (_, cmd) ->
       eval_command.ec_go ~disambiguate_command opts status (text,prefix_len,cmd)
   | GrafiteAst.Macro (loc, macro) ->
@@ -920,7 +924,7 @@ prerr_endline "CSC: here we should fix the height!!!";
          ~disambiguate_macro:(fun _ _ -> assert false)
          status ast
       in
-       assert (lemmas=[]);
+       assert (lemmas=`Old []);
        status)
     status moo
 } and eval_ast = {ea_go = fun ~disambiguate_tactic ~disambiguate_command
@@ -935,7 +939,7 @@ prerr_endline "CSC: here we should fix the height!!!";
   | GrafiteAst.Comment (_,c) -> 
       eval_comment.ecm_go ~disambiguate_command opts status (text,prefix_len,c) 
 } and eval_comment = { ecm_go = fun ~disambiguate_command opts status (text,prefix_len,c) -> 
-    status, []
+    status, `Old []
 }
 ;;
 

diff --git a/helm/software/components/grafite_engine/grafiteEngine.mli b/helm/software/components/grafite_engine/grafiteEngine.mli
index 993ccda71e756bae0fa7913dc9ff521e6d0c2596..de7fb27907fcb3367e7ba16bf122c7a8a06f1361 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.mli
+++ b/helm/software/components/grafite_engine/grafiteEngine.mli
@@ -55,5 +55,5 @@ val eval_ast :
   (('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement)
   disambiguator_input ->
    (* the new status and generated objects, if any *)
-   GrafiteTypes.status * UriManager.uri list
+   GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list]
 

diff --git a/helm/software/components/lexicon/lexiconSync.ml b/helm/software/components/lexicon/lexiconSync.ml
index a3a0d766e884924ce5ae9995123cb32f2a8629dc..f99535d19da9e5b7430eab6c043a7a015d8aed1a 100644 (file)
--- a/helm/software/components/lexicon/lexiconSync.ml
+++ b/helm/software/components/lexicon/lexiconSync.ml
@@ -85,11 +85,14 @@ let add_aliases_for_object status uri =
   | Cic.Variable _
   | Cic.CurrentProof _ -> assert false
   
-let add_aliases_for_objs =
- List.fold_left
-  (fun status uri ->
-    let obj,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
-     add_aliases_for_object status uri obj)
+let add_aliases_for_objs status =
+ function
+    `Old uris ->
+      List.fold_left
+       (fun status uri ->
+         let obj,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
+          add_aliases_for_object status uri obj) status uris
+  | `New nrefs -> assert false
  
 module OrderedId = 
 struct

diff --git a/helm/software/components/lexicon/lexiconSync.mli b/helm/software/components/lexicon/lexiconSync.mli
index fd38927476c13d353f3c1cb295685bfce5e5ddc9..c2ff15c420befc8f47d8537c643a7da0eb2b59b9 100644 (file)
--- a/helm/software/components/lexicon/lexiconSync.mli
+++ b/helm/software/components/lexicon/lexiconSync.mli
@@ -24,7 +24,8 @@
  *)
 
 val add_aliases_for_objs:
- LexiconEngine.status -> UriManager.uri list -> LexiconEngine.status
+ LexiconEngine.status -> [`Old of UriManager.uri list | `New of NUri.uri list]->
+  LexiconEngine.status
 
 val time_travel: 
   present:LexiconEngine.status -> past:LexiconEngine.status -> unit