From: Claudio Sacerdoti Coen Date: Fri, 5 Jun 2009 09:52:20 +0000 (+0000) Subject: 1) the home button of CicBrowser now works also for NG X-Git-Tag: make_still_working~3917 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9e7df95a820cb91d075f1a20d703175da874596c;p=helm.git 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. --- 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 *)