From 442f3a15d7c6afc480da02602d4d4c8db4f44c10 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sat, 6 Jun 2009 16:43:35 +0000 Subject: [PATCH] This commit restores the ids_to_father_ids table. However, after the implementation, I sort of realized that maybe this table is useless, after all. Thus I am gonna do my commit and immediately revert it (just to keep the code in SVN in case of need). --- .../components/binaries/transcript/.depend | 5 + .../binaries/transcript/.depend.opt | 5 + .../ng_cic_content/nTermCicContent.ml | 176 ++++++++++-------- .../ng_cic_content/nTermCicContent.mli | 7 +- .../components/syntax_extensions/.depend | 3 + helm/software/matita/applyTransformation.ml | 8 +- helm/software/matita/applyTransformation.mli | 8 +- helm/software/matita/matitaMathView.ml | 16 +- 8 files changed, 141 insertions(+), 87 deletions(-) diff --git a/helm/software/components/binaries/transcript/.depend b/helm/software/components/binaries/transcript/.depend index bb6f22a64..87d1ed25c 100644 --- a/helm/software/components/binaries/transcript/.depend +++ b/helm/software/components/binaries/transcript/.depend @@ -1,6 +1,11 @@ gallina8Parser.cmi: types.cmo grafiteParser.cmi: types.cmo grafite.cmi: types.cmo +engine.cmi: +types.cmo: +types.cmx: +options.cmo: +options.cmx: gallina8Parser.cmo: types.cmo options.cmo gallina8Parser.cmi gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi gallina8Lexer.cmo: options.cmo gallina8Parser.cmi diff --git a/helm/software/components/binaries/transcript/.depend.opt b/helm/software/components/binaries/transcript/.depend.opt index efadc681e..f17459162 100644 --- a/helm/software/components/binaries/transcript/.depend.opt +++ b/helm/software/components/binaries/transcript/.depend.opt @@ -1,6 +1,11 @@ gallina8Parser.cmi: types.cmx grafiteParser.cmi: types.cmx grafite.cmi: types.cmx +engine.cmi: +types.cmo: +types.cmx: +options.cmo: +options.cmx: gallina8Parser.cmo: types.cmx options.cmx gallina8Parser.cmi gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi gallina8Lexer.cmo: options.cmx gallina8Parser.cmi diff --git a/helm/software/components/ng_cic_content/nTermCicContent.ml b/helm/software/components/ng_cic_content/nTermCicContent.ml index 62d69f5d1..b1b2efec8 100644 --- a/helm/software/components/ng_cic_content/nTermCicContent.ml +++ b/helm/software/components/ng_cic_content/nTermCicContent.ml @@ -49,39 +49,50 @@ let get_types uri = | _ -> assert false *) -let idref register_ref = +let freshid register_ref register_father_id = let id = ref 0 in - fun ?reference t -> + fun ?reference father_id -> incr id; let id = "i" ^ string_of_int !id in (match reference with None -> () | Some r -> register_ref id r); - Ast.AttributedTerm (`IdRef id, t) + register_father_id id father_id; + Some id, fun t -> Ast.AttributedTerm (`IdRef id, t) ;; (* CODICE c&p da NCicPp *) let nast_of_cic0 - ~(idref: - ?reference:NReference.reference -> CicNotationPt.term -> CicNotationPt.term) - ~output_type ~subst k ~context = + ~(freshid: + ?reference:NReference.reference -> id option -> + id option * (CicNotationPt.term -> CicNotationPt.term)) + ~output_type ~subst k ~context father_id = function | NCic.Rel n -> - (try - let name,_ = List.nth context (n-1) in - let name = if name = "_" then "__"^string_of_int n else name in - idref (Ast.Ident (name,None)) - with Failure "nth" | Invalid_argument "List.nth" -> - idref (Ast.Ident ("-" ^ string_of_int (n - List.length context),None))) - | NCic.Const r -> idref ~reference:r (Ast.Ident (NCicPp.r2s true r, None)) + let id, idref = freshid father_id in + (try + let name,_ = List.nth context (n-1) in + let name = if name = "_" then "__"^string_of_int n else name in + idref (Ast.Ident (name,None)) + with Failure "nth" | Invalid_argument "List.nth" -> + idref (Ast.Ident ("-"^ string_of_int (n - List.length context),None))) + | NCic.Const r -> + let id, idref = freshid ~reference:r father_id in + idref (Ast.Ident (NCicPp.r2s true r, None)) | NCic.Meta (n,lc) when List.mem_assoc n subst -> let _,_,t,_ = List.assoc n subst in - k ~context (NCicSubstitution.subst_meta lc t) + k ~context father_id (NCicSubstitution.subst_meta lc t) | NCic.Meta (n,(s,l)) -> + let id, idref = freshid father_id in (* CSC: qua non dovremmo espandere *) let l = NCicUtils.expand_local_context l in idref (Ast.Meta - (n, List.map (fun x -> Some (k ~context (NCicSubstitution.lift s x))) l)) - | NCic.Sort NCic.Prop -> idref (Ast.Sort `Prop) - | NCic.Sort NCic.Type _ -> idref (Ast.Sort `Set) + (n, + List.map (fun x->Some(k ~context id (NCicSubstitution.lift s x))) l)) + | NCic.Sort NCic.Prop -> + let id, idref = freshid father_id in + idref (Ast.Sort `Prop) + | NCic.Sort NCic.Type _ -> + let id, idref = freshid father_id in + idref (Ast.Sort `Set) (* CSC: | C.Sort (C.Type []) -> F.fprintf f "Type0" | C.Sort (C.Type [false, u]) -> F.fprintf f "%s" (NUri.name_of_uri u) | C.Sort (C.Type [true, u]) -> F.fprintf f "S(%s)" (NUri.name_of_uri u) @@ -92,29 +103,40 @@ let nast_of_cic0 (List.tl l); F.fprintf f ")"*) (* CSC: qua siamo grezzi *) - | NCic.Implicit `Hole -> idref (Ast.UserInput) - | NCic.Implicit _ -> idref (Ast.Implicit) + | NCic.Implicit `Hole -> + let id, idref = freshid father_id in + idref (Ast.UserInput) + | NCic.Implicit _ -> + let id, idref = freshid father_id in + idref (Ast.Implicit) | NCic.Prod (n,s,t) -> - let n = if n.[0] = '_' then "_" else n in - let binder_kind = `Forall in - idref (Ast.Binder (binder_kind, (Ast.Ident (n,None), Some (k ~context s)), - k ~context:((n,NCic.Decl s)::context) t)) + let id, idref = freshid father_id in + let n = if n.[0] = '_' then "_" else n in + let binder_kind = `Forall in + idref + (Ast.Binder (binder_kind, (Ast.Ident (n,None), Some (k ~context id s)), + k ~context:((n,NCic.Decl s)::context) id t)) | NCic.Lambda (n,s,t) -> - idref (Ast.Binder (`Lambda,(Ast.Ident (n,None), Some (k ~context s)), - k ~context:((n,NCic.Decl s)::context) t)) + let id, idref = freshid father_id in + idref (Ast.Binder (`Lambda,(Ast.Ident (n,None), Some (k ~context id s)), + k ~context:((n,NCic.Decl s)::context) id t)) | NCic.LetIn (n,s,ty,t) -> - idref (Ast.LetIn ((Ast.Ident (n,None), Some (k ~context ty)), k ~context s, - k ~context:((n,NCic.Decl s)::context) t)) + let id, idref = freshid father_id in + idref (Ast.LetIn ((Ast.Ident (n,None), Some (k ~context id ty)), + k ~context id s, k ~context:((n,NCic.Decl s)::context) id t)) | NCic.Appl (NCic.Meta (n,lc) :: args) when List.mem_assoc n subst -> let _,_,t,_ = List.assoc n subst in let hd = NCicSubstitution.subst_meta lc t in - k ~context + k ~context father_id (NCicReduction.head_beta_reduce ~upto:(List.length args) (match hd with | NCic.Appl l -> NCic.Appl (l@args) | _ -> NCic.Appl (hd :: args))) - | NCic.Appl args -> idref (Ast.Appl (List.map (k ~context) args)) + | NCic.Appl args -> + let id, idref = freshid father_id in + idref (Ast.Appl (List.map (k ~context id) args)) | NCic.Match (NReference.Ref (uri,_) as r,outty,te,patterns) -> + let id, idref = freshid father_id in let name = NUri.name_of_uri uri in (* CSC let uri_str = UriManager.string_of_uri uri in @@ -137,8 +159,8 @@ let nast_of_cic0 eat_branch (pred n) ((name,NCic.Decl s)::ctx) t pat | NCic.Prod (_, _, t), NCic.Lambda (name, s, t') -> let cv, rhs = eat_branch 0 ((name,NCic.Decl s)::ctx) t t' in - (Ast.Ident (name,None), Some (k ~context s)) :: cv, rhs - | _, _ -> [], k ~context pat + (Ast.Ident (name,None), Some (k ~context id s)) :: cv, rhs + | _, _ -> [], k ~context id pat in let j = ref 0 in let patterns = @@ -149,9 +171,10 @@ let nast_of_cic0 let name,(capture_variables,rhs) = match output_type with `Term -> name, eat_branch leftno context ty pat - | `Pattern -> "_", ([], k ~context pat) + | `Pattern -> "_", ([], k ~context id pat) in - Ast.Pattern (name, None(*CSC Some (ctor_puri !j)*), capture_variables), rhs + Ast.Pattern + (name, None(*CSC Some (ctor_puri !j)*), capture_variables),rhs ) constructors patterns with Invalid_argument _ -> assert false in @@ -160,7 +183,9 @@ let nast_of_cic0 `Pattern -> None | `Term -> Some case_indty in - idref (Ast.Case (k ~context te, indty, Some (k ~context outty), patterns)) + idref + (Ast.Case + (k ~context id te, indty, Some (k ~context id outty), patterns)) ;; (* persistent state *) @@ -242,39 +267,34 @@ let instantiate32 idrefs env symbol args = if args = [] then head else Ast.Appl (head :: List.map instantiate_arg args) -let rec nast_of_cic1 ~idref ~output_type ~subst ~context term = +let rec nast_of_cic1 ~freshid ~output_type ~subst ~context father_id term = match (get_compiled32 ()) term with | None -> - nast_of_cic0 ~idref ~output_type ~subst - (nast_of_cic1 ~idref ~output_type ~subst) ~context term - | Some (env, ctors, pid) -> - let idrefs = - List.map - (fun term -> - let attrterm = - idref - ~reference: - (match term with NCic.Const nref -> nref | _ -> assert false) - (CicNotationPt.Ident ("dummy",None)) - in - match attrterm with - Ast.AttributedTerm (`IdRef id, _) -> id - | _ -> assert false - ) ctors - in - let env = - List.map - (fun (name, term) -> - name, - nast_of_cic1 ~idref ~output_type ~subst ~context term - ) env - in - let _, symbol, args, _ = - try - TermAcicContent.find_level2_patterns32 pid - with Not_found -> assert false - in - let ast = instantiate32 idrefs env symbol args in + nast_of_cic0 ~freshid ~output_type ~subst + (nast_of_cic1 ~freshid ~output_type ~subst) ~context father_id term + | Some (env, ctors, pid) -> + let id, idref = freshid father_id in + let idrefs = + List.map + (fun term -> + let id, _ = + freshid + ~reference: + (match term with NCic.Const nref -> nref | _ -> assert false) + father_id + in + match id with Some id -> id | None -> assert false + ) ctors in + let env = + List.map + (fun (name, term) -> + name,nast_of_cic1 ~freshid ~output_type ~subst ~context id term + ) env in + let _, symbol, args, _ = + try + TermAcicContent.find_level2_patterns32 pid + with Not_found -> assert false in + let ast = instantiate32 idrefs env symbol args in idref ast (*Ast.AttributedTerm (`IdRef (idref term), ast)*) ;; @@ -387,9 +407,10 @@ let instantiate_appl_pattern aux appl_pattern *) -let nmap_sequent0 ~idref ~subst (i,(n,context,ty):int * NCic.conjecture) = +let nmap_sequent0 ~freshid ~subst (i,(n,context,ty):int * NCic.conjecture) = let module K = Content in - let nast_of_cic = nast_of_cic1 ~idref ~output_type:`Term ~subst in + let nast_of_cic ~context = + nast_of_cic1 ~freshid ~output_type:`Term ~subst ~context None in let context',_ = List.fold_right (fun item (res,context) -> @@ -423,9 +444,12 @@ let nmap_sequent0 ~idref ~subst (i,(n,context,ty):int * NCic.conjecture) = let nmap_sequent ~subst metasenv = let module K = Content in - let ids_to_refs = Hashtbl.create 211 in + let ids_to_refs = Hashtbl.create 503 in + let ids_to_father_ids = Hashtbl.create 503 in let register_ref = Hashtbl.add ids_to_refs in - nmap_sequent0 ~idref:(idref register_ref) ~subst metasenv, ids_to_refs + let register_father_id = Hashtbl.add ids_to_father_ids in + nmap_sequent0 ~freshid:(freshid register_ref register_father_id) ~subst + metasenv,ids_to_refs,ids_to_father_ids ;; let object_prefix = "obj:";; @@ -498,18 +522,20 @@ let build_decl_item seed id n s = let nmap_obj (uri,_,metasenv,subst,kind) = let module K = Content in - let ids_to_refs = Hashtbl.create 211 in + let ids_to_refs = Hashtbl.create 503 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 ids_to_father_ids = Hashtbl.create 503 in + let register_father_id = Hashtbl.add ids_to_father_ids in + let freshid = freshid register_ref register_father_id in + let nast_of_cic ~context = + nast_of_cic1 ~freshid ~output_type:`Term ~subst ~context None 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) + Some (List.map (nmap_sequent0 ~freshid ~subst) metasenv) in let res = match kind with @@ -559,5 +585,5 @@ and }) l *) in - res,ids_to_refs + res,ids_to_refs,ids_to_father_ids ;; diff --git a/helm/software/components/ng_cic_content/nTermCicContent.mli b/helm/software/components/ng_cic_content/nTermCicContent.mli index bae7daee2..e5a6f26c9 100644 --- a/helm/software/components/ng_cic_content/nTermCicContent.mli +++ b/helm/software/components/ng_cic_content/nTermCicContent.mli @@ -88,9 +88,12 @@ type id = string val nmap_sequent: subst:NCic.substitution -> int * NCic.conjecture -> CicNotationPt.term Content.conjecture * - (id, NReference.reference) Hashtbl.t (* id -> reference *) + (id, NReference.reference) Hashtbl.t * (* id -> reference *) + (string, id option) Hashtbl.t (* id -> father_id *) + val nmap_obj: NCic.obj -> CicNotationPt.term Content.cobj * - (id, NReference.reference) Hashtbl.t (* id -> reference *) + (id, NReference.reference) Hashtbl.t * (* id -> reference *) + (string, id option) Hashtbl.t (* id -> father_id *) diff --git a/helm/software/components/syntax_extensions/.depend b/helm/software/components/syntax_extensions/.depend index f3c6a8bd1..25e67131f 100644 --- a/helm/software/components/syntax_extensions/.depend +++ b/helm/software/components/syntax_extensions/.depend @@ -1,2 +1,5 @@ +utf8Macro.cmi: +utf8MacroTable.cmo: +utf8MacroTable.cmx: utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml index 4015293a4..e23400fb2 100644 --- a/helm/software/matita/applyTransformation.ml +++ b/helm/software/matita/applyTransformation.ml @@ -66,12 +66,12 @@ let mml_of_cic_sequent metasenv sequent = (ids_to_terms,ids_to_father_ids,ids_to_hypotheses,ids_to_inner_sorts))) let nmml_of_cic_sequent metasenv subst sequent = - let content_sequent,ids_to_refs = + let content_sequent,ids_to_refs,ids_to_father_ids = NTermCicContent.nmap_sequent ~subst sequent in let pres_sequent = Sequent2pres.nsequent2pres ids_to_refs subst content_sequent in let xmlpres = mpres_document pres_sequent in - Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres + Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres,ids_to_father_ids let mml_of_cic_object obj = let (annobj, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, @@ -90,10 +90,10 @@ let mml_of_cic_object obj = ids_to_inner_sorts,ids_to_inner_types))) let nmml_of_cic_object obj = - let cobj,ids_to_nrefs = NTermCicContent.nmap_obj obj in + let cobj,ids_to_nrefs,ids_to_father_ids = 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 + Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres,ids_to_father_ids ;; let txt_of_cic_sequent ~map_unicode_to_tex size metasenv sequent = diff --git a/helm/software/matita/applyTransformation.mli b/helm/software/matita/applyTransformation.mli index f41f0a7a1..9fe4130c3 100644 --- a/helm/software/matita/applyTransformation.mli +++ b/helm/software/matita/applyTransformation.mli @@ -47,7 +47,8 @@ val mml_of_cic_sequent: val nmml_of_cic_sequent: NCic.metasenv -> NCic.substitution -> (* metasenv, substitution *) int * NCic.conjecture -> (* sequent *) - Gdome.document (* Math ML *) + Gdome.document * (* Math ML *) + (string, NTermCicContent.id option) Hashtbl.t (* id -> father id *) val mml_of_cic_object: Cic.obj -> (* object *) @@ -60,7 +61,10 @@ val mml_of_cic_object: (Cic.id, Cic2acic.sort_kind) Hashtbl.t * (* ids_to_inner_sorts *) (Cic.id, Cic2acic.anntypes) Hashtbl.t)) (* ids_to_inner_types *) -val nmml_of_cic_object: NCic.obj -> Gdome.document +val nmml_of_cic_object: + NCic.obj -> Gdome.document * + (string, NTermCicContent.id option) Hashtbl.t (* id -> father id *) + val txt_of_cic_term: map_unicode_to_tex:bool -> int -> Cic.metasenv -> Cic.context -> Cic.term -> diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml index 277dbe8f1..a6aa89e81 100644 --- a/helm/software/matita/matitaMathView.ml +++ b/helm/software/matita/matitaMathView.ml @@ -186,8 +186,11 @@ object (self) method set_href_callback f = href_callback <- f val mutable _cic_info = None + val mutable _ncic_info = None method private set_cic_info info = _cic_info <- info method private cic_info = _cic_info + method private set_ncic_info info = _ncic_info <- info + method private ncic_info = _ncic_info val normal_cursor = Gdk.Cursor.create `LEFT_PTR val href_cursor = Gdk.Cursor.create `HAND2 @@ -511,6 +514,11 @@ object (self) info, (~-1, [], t) (* dummy sequent for obj *) | None -> assert false + method private get_ncic_info id = + match self#ncic_info with + | Some info -> info + | None -> assert false + method private sequent_of_id ~(paste_kind:paste_kind) id = let cic_info, unsh_sequent = self#get_cic_info id in let cic_sequent = @@ -595,9 +603,10 @@ object (self) method nload_sequent metasenv subst metano = let sequent = List.assoc metano metasenv in - let mathml = + let mathml,ids_to_father_ids = ApplyTransformation.nmml_of_cic_sequent metasenv subst (metano,sequent) in + self#set_ncic_info (Some ids_to_father_ids); if BuildTimeConf.debug then begin let name = "/tmp/sequent_viewer_" ^ string_of_int (Unix.getuid ()) ^ ".xml" in @@ -631,10 +640,9 @@ object (self) current_mathml <- Some mathml); method load_nobject obj = - let mathml = ApplyTransformation.nmml_of_cic_object obj in + let mathml,ids_to_father_ids = ApplyTransformation.nmml_of_cic_object obj in + self#set_ncic_info (Some ids_to_father_ids); (* - self#set_cic_info - (Some (None, ids_to_terms, ids_to_hypotheses, ids_to_father_ids, ids_to_inner_types, Some annobj)); (match current_mathml with | Some current_mathml when use_diff -> self#freeze; -- 2.39.2