From 585469505faa97c21687128490828a1aabee94ee Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 24 Apr 2009 15:11:34 +0000 Subject: [PATCH] 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 --- .../software/components/grafite/grafiteAst.ml | 1 + .../grafite_engine/grafiteEngine.ml | 23 ++++++++- .../grafite_parser/grafiteDisambiguate.ml | 14 ++++-- .../grafite_parser/grafiteParser.ml | 1 + .../components/ng_kernel/nCicLibrary.ml | 5 ++ .../components/ng_kernel/nCicLibrary.mli | 1 + .../components/ng_tactics/nTacStatus.ml | 48 ++++++++++++------- .../components/ng_tactics/nTacStatus.mli | 2 + 8 files changed, 73 insertions(+), 22 deletions(-) diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 67d42c644..f6555fa04 100644 --- 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 2e8b49f7d..26e3aab2d 100644 --- 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 835e6b411..4ea3a95b3 100644 --- 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 ff1771b5a..be6dab1a6 100644 --- 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> ; newname = IDENT -> GrafiteAst.Obj (loc, diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml index 946535fe1..4e9133417 100644 --- 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 1893e9659..fdcbbde5c 100644 --- 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 f8ee5f1e5..f0b00e561 100644 --- 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 74b5366db..59ef35592 100644 --- 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: -- 2.39.2