Quick&dirty implementation of neqd:

 a) nCicLibrary has a new function add_obj to add objects to the storage
    (that is, so far, an associative list)
 b) new command nqed
 c) GrafiteDisambiguate modified so that identifiers are resolved
    in the new storage, if possible, before going back to translating
    the old library
 d) implementation of apply_subst for terms and objects (used during nqed)
    Note: these functions are currently in nTacStatus but should be moved
    elsewhere

diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index 67d42c64454205a12c4dccd0a23823ea585926a9..f6555fa04c7dd5ed86bb8c4f6c6bbe8d7fee4feb 100644 (file)
--- a/helm/software/components/grafite/grafiteAst.ml
+++ b/helm/software/components/grafite/grafiteAst.ml
@@ -188,6 +188,7 @@ type ('term,'obj) command =
   | Print of loc * string
   | Qed of loc
   | NObj of loc * CicNotationPt.term CicNotationPt.obj
+  | NQed of loc
 
 type punctuation_tactical =
   | Dot of loc

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 2e8b49f7d5980910456ba1f72249690a601be0e7..26e3aab2d05d4066def1e1e64fcbe267746226d1 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -741,6 +741,26 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
          GrafiteTypes.proof_status = GrafiteTypes.No_proof},
         (*CSC: I throw away the arities *)
         uri::lemmas
+  | GrafiteAst.NQed loc ->
+      (match status.GrafiteTypes.ng_status with
+       | GrafiteTypes.ProofMode
+          { NTacStatus.istatus =
+             {NTacStatus.pstatus = pstatus; lstatus=lexicon_status} } ->
+            let uri,height,menv,subst,obj = pstatus in
+             if menv <> [] then
+              raise
+               (GrafiteTypes.Command_error"You can't Qed an incomplete theorem")
+             else
+              let obj =
+prerr_endline "CSC: here we should fix the height!!!";
+prerr_endline (NUri.string_of_uri uri);
+               uri,height,[],[],NTacStatus.apply_subst_obj subst obj
+              in
+               NCicLibrary.add_obj uri obj;
+               {status with 
+                 GrafiteTypes.ng_status = 
+                  GrafiteTypes.CommandMode lexicon_status },[]
+       | _ -> 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 *)
@@ -752,7 +772,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
        | CicNotationPt.Theorem (_,name,ty,_) -> ty, name
        | _ -> assert false
      in
-     let suri = "cic:/ng_matita/" ^ name ^ ".def" in
+     (* CSC: ".con"??? it is like that for now *)
+     let suri = "cic:/ng_matita/" ^ name ^ ".con" in
      let nlexicon_status =
        match status.GrafiteTypes.ng_status with
        | GrafiteTypes.ProofMode _ -> assert false

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index 835e6b41153fd46e54dbe54cc4e69b367b13b24d..4ea3a95b3889cb6784cb77522e809e773039f836 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -89,8 +89,15 @@ let ncic_mk_choice = function
   | LexiconAst.Ident_alias (name, uri) -> 
      uri, `Sym_interp 
       (fun l->assert(l = []);
-      let uri = UriManager.uri_of_string uri in
-       fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)))
+        if String.sub uri 5 9 = "ng_matita" then
+         let nuri =
+          NUri.uri_of_string (String.sub uri 0 (String.length uri -3) ^ "def")
+         in
+          NCic.Const
+           (NReference.reference_of_spec nuri (NReference.Def 0))
+        else
+         let uri = UriManager.uri_of_string uri in
+          fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)))
 ;;
 
 
@@ -664,7 +671,7 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
        (try
          (match 
           NCicDisambiguate.disambiguate_obj
-           ~lookup_in_library:lookup_in_library
+           ~lookup_in_library
            ~description_of_alias:LexiconAst.description_of_alias
            ~mk_choice:ncic_mk_choice
            ~mk_implicit
@@ -784,6 +791,7 @@ let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)=
    | GrafiteAst.Include _
    | GrafiteAst.Print _
    | GrafiteAst.Qed _
+   | GrafiteAst.NQed _
    | GrafiteAst.Set _ as cmd ->
        lexicon_status,metasenv,cmd
    | GrafiteAst.Obj (loc,obj) ->

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index ff1771b5af6858deb3cfe8b0c5a0957298810eac..be6dab1a61085b8b84c0ec9d77d490f779944c95 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -717,6 +717,7 @@ EXTEND
     | IDENT "drop" -> GrafiteAst.Drop loc
     | IDENT "print"; s = IDENT -> GrafiteAst.Print (loc,s)
     | IDENT "qed" -> GrafiteAst.Qed loc
+    | IDENT "nqed" -> GrafiteAst.NQed loc
     | IDENT "variant" ; name = IDENT; SYMBOL ":"; 
       typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
         GrafiteAst.Obj (loc, 

diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml
index 946535fe1fd8d5cb70775fcb38bc2dc5d7730a81..4e91334170555f6f5c75638e00ced633c4321e4a 100644 (file)
--- a/helm/software/components/ng_kernel/nCicLibrary.ml
+++ b/helm/software/components/ng_kernel/nCicLibrary.ml
@@ -13,9 +13,14 @@
 
 exception ObjectNotFound of string Lazy.t
 
+let storage = ref [];;
+let add_obj u obj = storage := (u,obj)::!storage;;
+
 let cache = NUri.UriHash.create 313;;
 
 let get_obj u =
+ try List.assq u !storage
+ with Not_found ->
   try NUri.UriHash.find cache u
   with Not_found ->
     (* in the final implementation should get it from disk *)

diff --git a/helm/software/components/ng_kernel/nCicLibrary.mli b/helm/software/components/ng_kernel/nCicLibrary.mli
index 1893e9659eb8394533728a397514d7a7c2715f34..fdcbbde5c595ae5667d1b635414c1d04fa71ee53 100644 (file)
--- a/helm/software/components/ng_kernel/nCicLibrary.mli
+++ b/helm/software/components/ng_kernel/nCicLibrary.mli
@@ -13,6 +13,7 @@
 
 exception ObjectNotFound of string Lazy.t
 
+val add_obj: NUri.uri -> NCic.obj -> unit
 val get_obj: NUri.uri -> NCic.obj
 
 val clear_cache : unit -> unit

diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml
index f8ee5f1e5e929ab197773adaf6c8be5a567c0f3e..f0b00e561dbc7d26c21ebc4d469becb5faa0349e 100644 (file)
--- a/helm/software/components/ng_tactics/nTacStatus.ml
+++ b/helm/software/components/ng_tactics/nTacStatus.ml
@@ -326,25 +326,37 @@ let analyse_indty status ty =
 
 let mk_cic_term c t = None,c,t ;;
 
+(* CSC: next two functions to be moved elsewhere *)
+let rec apply_subst subst ctx =
+ function
+    NCic.Meta (i,lc) ->
+     (try
+       let _,_,t,_ = NCicUtils.lookup_subst i subst in
+       let t = NCicSubstitution.subst_meta lc t in
+        apply_subst subst ctx t
+      with
+       Not_found ->
+        match lc with
+           _,NCic.Irl _ -> NCic.Meta (i,lc)
+         | n,NCic.Ctx l ->
+            NCic.Meta
+             (i,(0,NCic.Ctx
+                 (List.map (fun t ->
+                   apply_subst subst ctx (NCicSubstitution.lift n t)) l))))
+  | t -> NCicUtils.map (fun item ctx -> item::ctx) ctx (apply_subst subst) t
+;;
+
+let apply_subst_obj subst =
+ function
+    NCic.Constant (relev,name,bo,ty,attrs) ->
+     NCic.Constant
+      (relev,name,HExtlib.map_option (apply_subst subst []) bo,
+        apply_subst subst [] ty,attrs)
+  | _ -> assert false (* not implemented yet *)
+;;
+
 let apply_subst status ctx t =
  let status, (name,_,t) = relocate status ctx t in
  let _,_,_,subst,_ = status.pstatus in
- let rec aux ctx =
-  function
-     NCic.Meta (i,lc) ->
-      (try
-        let _,_,t,_ = NCicUtils.lookup_subst i subst in
-        let t = NCicSubstitution.subst_meta lc t in
-         aux ctx t
-       with
-        Not_found ->
-         match lc with
-            _,NCic.Irl _ -> NCic.Meta (i,lc)
-          | n,NCic.Ctx l ->
-             NCic.Meta
-              (i,(0,NCic.Ctx
-                  (List.map (fun t -> aux ctx (NCicSubstitution.lift n t)) l))))
-   | t -> NCicUtils.map (fun item ctx -> item::ctx) ctx aux t
- in
-  status, (name, ctx, aux ctx t)
+  status, (name, ctx, apply_subst subst ctx t)
 ;;

diff --git a/helm/software/components/ng_tactics/nTacStatus.mli b/helm/software/components/ng_tactics/nTacStatus.mli
index 74b5366db396b5dee570fc213415a35f1764cca8..59ef3559264563ae6c2e2393e687eeb949df0af7 100644 (file)
--- a/helm/software/components/ng_tactics/nTacStatus.mli
+++ b/helm/software/components/ng_tactics/nTacStatus.mli
@@ -60,6 +60,8 @@ val refine:
 val apply_subst:
   lowtac_status -> NCic.context -> cic_term -> lowtac_status * cic_term
 
+(* CSC: this function must be moved elsewhere *)
+val apply_subst_obj: NCic.substitution -> NCic.obj_kind -> NCic.obj_kind
 
 val get_goalty: lowtac_status -> int -> cic_term
 val mk_meta: