From 9e7df95a820cb91d075f1a20d703175da874596c Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 5 Jun 2009 09:52:20 +0000 Subject: [PATCH] 1) the home button of CicBrowser now works also for NG 2) implemented simple (i.e. no natural language) rendering of NG constants. Inductive types and (co)recursive definitions are still missing. --- .../components/content_pres/content2pres.ml | 16 +- .../components/content_pres/content2pres.mli | 6 + .../ng_cic_content/nTermCicContent.ml | 150 +++++++++++++++++- .../ng_cic_content/nTermCicContent.mli | 5 + helm/software/matita/applyTransformation.ml | 6 +- helm/software/matita/matitaMathView.ml | 19 ++- 6 files changed, 186 insertions(+), 16 deletions(-) diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml index 46f53d886..282cfe26e 100644 --- a/helm/software/components/content_pres/content2pres.ml +++ b/helm/software/components/content_pres/content2pres.ml @@ -929,7 +929,7 @@ let joint_def2pres term2pres def = | `Inductive ind -> inductive2pres term2pres ind | _ -> assert false (* ZACK or raise ToDo? *) -let content2pres +let content2pres0 ?skip_initial_lambdas ?(skip_thm_and_qed=false) term2pres (id,params,metasenv,obj) = @@ -976,7 +976,7 @@ let content2pres let content2pres ?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_inner_sorts = - content2pres ?skip_initial_lambdas ?skip_thm_and_qed + content2pres0 ?skip_initial_lambdas ?skip_thm_and_qed (fun ?(prec=90) annterm -> let ast, ids_to_uris = TermAcicContent.ast_of_acic ~output_type:`Term ids_to_inner_sorts annterm @@ -985,3 +985,15 @@ let content2pres (CicNotationPres.render ~lookup_uri:(CicNotationPres.lookup_uri ids_to_uris) ~prec (TermContentPres.pp_ast ast))) + +let ncontent2pres ?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_nrefs = + let lookup_uri id = + try + let nref = Hashtbl.find ids_to_nrefs id in + Some (NReference.string_of_reference nref) + with Not_found -> None + in + content2pres0 ?skip_initial_lambdas ?skip_thm_and_qed + (fun ?(prec=90) ast -> + CicNotationPres.box_of_mpres + (CicNotationPres.render ~lookup_uri ~prec (TermContentPres.pp_ast ast))) diff --git a/helm/software/components/content_pres/content2pres.mli b/helm/software/components/content_pres/content2pres.mli index c5d32e9fd..db2223a7a 100644 --- a/helm/software/components/content_pres/content2pres.mli +++ b/helm/software/components/content_pres/content2pres.mli @@ -38,3 +38,9 @@ val content2pres: Cic.annterm Content.cobj -> CicNotationPres.boxml_markup +val ncontent2pres: + ?skip_initial_lambdas:int -> ?skip_thm_and_qed:bool -> + ids_to_nrefs:(NTermCicContent.id, NReference.reference) Hashtbl.t -> + CicNotationPt.term Content.cobj -> + CicNotationPres.boxml_markup + diff --git a/helm/software/components/ng_cic_content/nTermCicContent.ml b/helm/software/components/ng_cic_content/nTermCicContent.ml index da8061fde..62d69f5d1 100644 --- a/helm/software/components/ng_cic_content/nTermCicContent.ml +++ b/helm/software/components/ng_cic_content/nTermCicContent.ml @@ -387,13 +387,9 @@ let instantiate_appl_pattern aux appl_pattern *) -let nmap_sequent ~subst (i,(n,context,ty):int * NCic.conjecture) = +let nmap_sequent0 ~idref ~subst (i,(n,context,ty):int * NCic.conjecture) = let module K = Content in - let ids_to_refs = Hashtbl.create 211 in - let register_ref = Hashtbl.add ids_to_refs in - let nast_of_cic = - nast_of_cic1 ~idref:(idref register_ref) ~output_type:`Term - ~subst in + let nast_of_cic = nast_of_cic1 ~idref ~output_type:`Term ~subst in let context',_ = List.fold_right (fun item (res,context) -> @@ -422,6 +418,146 @@ let nmap_sequent ~subst (i,(n,context,ty):int * NCic.conjecture) = })::res,item::context ) context ([],[]) in - ("-1",i,context',nast_of_cic ~context ty), ids_to_refs + ("-1",i,context',nast_of_cic ~context ty) +;; + +let nmap_sequent ~subst metasenv = + let module K = Content in + let ids_to_refs = Hashtbl.create 211 in + let register_ref = Hashtbl.add ids_to_refs in + nmap_sequent0 ~idref:(idref register_ref) ~subst metasenv, ids_to_refs +;; + +let object_prefix = "obj:";; +let declaration_prefix = "decl:";; +let definition_prefix = "def:";; + +let get_id = + function + Ast.AttributedTerm (`IdRef id, _) -> id + | _ -> assert false +;; + +let gen_id prefix seed = + let res = prefix ^ string_of_int !seed in + incr seed ; + res +;; + +let build_def_item seed context metasenv id n t ty = + let module K = Content in +(* + try + let sort = Hashtbl.find ids_to_inner_sorts id in + if sort = `Prop then + (let p = + (acic2content seed context metasenv ?name:(name_of n) ~ids_to_inner_sorts ~ids_to_inner_types t) + in + `Proof p;) + else +*) + `Definition + { K.def_name = Some n; + K.def_id = gen_id definition_prefix seed; + K.def_aref = id; + K.def_term = t; + K.def_type = ty + } +(* + with + Not_found -> assert false +*) + +let build_decl_item seed id n s = + let module K = Content in +(* + let sort = + try + Some (Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id)) + with Not_found -> None + in + match sort with + | Some `Prop -> + `Hypothesis + { K.dec_name = name_of n; + K.dec_id = gen_id declaration_prefix seed; + K.dec_inductive = false; + K.dec_aref = id; + K.dec_type = s + } + | _ -> +*) + `Declaration + { K.dec_name = Some n; + K.dec_id = gen_id declaration_prefix seed; + K.dec_inductive = false; + K.dec_aref = id; + K.dec_type = s + } ;; +let nmap_obj (uri,_,metasenv,subst,kind) = + let module K = Content in + let ids_to_refs = Hashtbl.create 211 in + let register_ref = Hashtbl.add ids_to_refs in + let idref = idref register_ref in + let nast_of_cic = + nast_of_cic1 ~idref ~output_type:`Term ~subst in + let seed = ref 0 in + let conjectures = + match metasenv with + [] -> None + | _ -> (*Some (List.map (map_conjectures seed) metasenv)*) + (*CSC: used to be the previous line, that uses seed *) + Some (List.map (nmap_sequent0 ~idref ~subst) metasenv) + in + let res = + match kind with + NCic.Constant (_,_,Some bo,ty,_) -> + let ty = nast_of_cic ~context:[] ty in + let bo = nast_of_cic ~context:[] bo in + (gen_id object_prefix seed, [], conjectures, + `Def (K.Const,ty, + build_def_item seed [] [] (get_id bo) (NUri.name_of_uri uri) bo ty)) + | NCic.Constant (_,_,None,ty,_) -> + let ty = nast_of_cic ~context:[] ty in + (gen_id object_prefix seed, [], conjectures, + `Decl (K.Const, + (*CSC: ??? get_id ty here used to be the id of the axiom! *) + build_decl_item seed (get_id ty) (NUri.name_of_uri uri) ty)) +(* + | C.AInductiveDefinition (id,l,params,nparams,_) -> + (gen_id object_prefix seed, params, conjectures, + `Joint + { K.joint_id = gen_id joint_prefix seed; + K.joint_kind = `Inductive nparams; + K.joint_defs = List.map (build_inductive seed) l + }) + +and + build_inductive seed = + let module K = Content in + fun (_,n,b,ty,l) -> + `Inductive + { K.inductive_id = gen_id inductive_prefix seed; + K.inductive_name = n; + K.inductive_kind = b; + K.inductive_type = ty; + K.inductive_constructors = build_constructors seed l + } + +and + build_constructors seed l = + let module K = Content in + List.map + (fun (n,t) -> + { K.dec_name = Some n; + K.dec_id = gen_id declaration_prefix seed; + K.dec_inductive = false; + K.dec_aref = ""; + K.dec_type = t + }) l +*) + in + res,ids_to_refs +;; diff --git a/helm/software/components/ng_cic_content/nTermCicContent.mli b/helm/software/components/ng_cic_content/nTermCicContent.mli index 5f1388bb2..bae7daee2 100644 --- a/helm/software/components/ng_cic_content/nTermCicContent.mli +++ b/helm/software/components/ng_cic_content/nTermCicContent.mli @@ -89,3 +89,8 @@ val nmap_sequent: subst:NCic.substitution -> int * NCic.conjecture -> CicNotationPt.term Content.conjecture * (id, NReference.reference) Hashtbl.t (* id -> reference *) + +val nmap_obj: + NCic.obj -> + CicNotationPt.term Content.cobj * + (id, NReference.reference) Hashtbl.t (* id -> reference *) diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml index da4bccba0..91fe7bcd0 100644 --- a/helm/software/matita/applyTransformation.ml +++ b/helm/software/matita/applyTransformation.ml @@ -90,8 +90,10 @@ let mml_of_cic_object obj = ids_to_inner_sorts,ids_to_inner_types))) let nmml_of_cic_object obj = - prerr_endline (NCicPp.ppobj obj); - assert false + let cobj,ids_to_nrefs = NTermCicContent.nmap_obj obj in + let pres_sequent = Content2pres.ncontent2pres ~ids_to_nrefs cobj in + let xmlpres = mpres_document pres_sequent in + Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres ;; let txt_of_cic_sequent ~map_unicode_to_tex size metasenv sequent = diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml index ade02fb80..277dbe8f1 100644 --- a/helm/software/matita/matitaMathView.ml +++ b/helm/software/matita/matitaMathView.ml @@ -1337,14 +1337,23 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) self#_showMath; match self#script#grafite_status.proof_status with | Proof (uri, metasenv, _subst, bo, ty, attrs) -> - let name = UriManager.name_of_uri (HExtlib.unopt uri) in - let obj = Cic.CurrentProof (name, metasenv, Lazy.force bo, ty, [], attrs) in + let name = UriManager.name_of_uri (HExtlib.unopt uri) in + let obj = + Cic.CurrentProof (name, metasenv, Lazy.force bo, ty, [], attrs) + in self#_loadObj obj | Incomplete_proof { proof = (uri, metasenv, _subst, bo, ty, attrs) } -> - let name = UriManager.name_of_uri (HExtlib.unopt uri) in - let obj = Cic.CurrentProof (name, metasenv, Lazy.force bo, ty, [], attrs) in + let name = UriManager.name_of_uri (HExtlib.unopt uri) in + let obj = + Cic.CurrentProof (name, metasenv, Lazy.force bo, ty, [], attrs) + in self#_loadObj obj - | _ -> self#blank () + | _ -> + match self#script#grafite_status.ng_status with + ProofMode tstatus -> + let nobj = tstatus.NTacStatus.istatus.NTacStatus.pstatus in + self#_loadNObj nobj + | _ -> self#blank () (** loads a cic uri from the environment * @param uri UriManager.uri *) -- 2.39.2