From ba8d987dab88c8a834c4e23508f13a397070d537 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sat, 6 Jun 2009 16:45:12 +0000 Subject: [PATCH] Previous commit reverted, as explained in that log. --- .../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, 87 insertions(+), 141 deletions(-) diff --git a/helm/software/components/binaries/transcript/.depend b/helm/software/components/binaries/transcript/.depend index 87d1ed25c..bb6f22a64 100644 --- a/helm/software/components/binaries/transcript/.depend +++ b/helm/software/components/binaries/transcript/.depend @@ -1,11 +1,6 @@ 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 f17459162..efadc681e 100644 --- a/helm/software/components/binaries/transcript/.depend.opt +++ b/helm/software/components/binaries/transcript/.depend.opt @@ -1,11 +1,6 @@ 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 b1b2efec8..62d69f5d1 100644 --- a/helm/software/components/ng_cic_content/nTermCicContent.ml +++ b/helm/software/components/ng_cic_content/nTermCicContent.ml @@ -49,50 +49,39 @@ let get_types uri = | _ -> assert false *) -let freshid register_ref register_father_id = +let idref register_ref = let id = ref 0 in - fun ?reference father_id -> + fun ?reference t -> incr id; let id = "i" ^ string_of_int !id in (match reference with None -> () | Some r -> register_ref id r); - register_father_id id father_id; - Some id, fun t -> Ast.AttributedTerm (`IdRef id, t) + Ast.AttributedTerm (`IdRef id, t) ;; (* CODICE c&p da NCicPp *) let nast_of_cic0 - ~(freshid: - ?reference:NReference.reference -> id option -> - id option * (CicNotationPt.term -> CicNotationPt.term)) - ~output_type ~subst k ~context father_id = + ~(idref: + ?reference:NReference.reference -> CicNotationPt.term -> CicNotationPt.term) + ~output_type ~subst k ~context = function | NCic.Rel n -> - 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)) + (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)) | NCic.Meta (n,lc) when List.mem_assoc n subst -> let _,_,t,_ = List.assoc n subst in - k ~context father_id (NCicSubstitution.subst_meta lc t) + k ~context (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 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) + (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) (* 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) @@ -103,40 +92,29 @@ let nast_of_cic0 (List.tl l); F.fprintf f ")"*) (* CSC: qua siamo grezzi *) - | 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.Implicit `Hole -> idref (Ast.UserInput) + | NCic.Implicit _ -> idref (Ast.Implicit) | NCic.Prod (n,s,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)) + 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)) | NCic.Lambda (n,s,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)) + idref (Ast.Binder (`Lambda,(Ast.Ident (n,None), Some (k ~context s)), + k ~context:((n,NCic.Decl s)::context) t)) | NCic.LetIn (n,s,ty,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)) + idref (Ast.LetIn ((Ast.Ident (n,None), Some (k ~context ty)), k ~context s, + k ~context:((n,NCic.Decl s)::context) 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 father_id + k ~context (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 -> - let id, idref = freshid father_id in - idref (Ast.Appl (List.map (k ~context id) args)) + | NCic.Appl args -> idref (Ast.Appl (List.map (k ~context) 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 @@ -159,8 +137,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 id s)) :: cv, rhs - | _, _ -> [], k ~context id pat + (Ast.Ident (name,None), Some (k ~context s)) :: cv, rhs + | _, _ -> [], k ~context pat in let j = ref 0 in let patterns = @@ -171,10 +149,9 @@ let nast_of_cic0 let name,(capture_variables,rhs) = match output_type with `Term -> name, eat_branch leftno context ty pat - | `Pattern -> "_", ([], k ~context id pat) + | `Pattern -> "_", ([], k ~context 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 @@ -183,9 +160,7 @@ let nast_of_cic0 `Pattern -> None | `Term -> Some case_indty in - idref - (Ast.Case - (k ~context id te, indty, Some (k ~context id outty), patterns)) + idref (Ast.Case (k ~context te, indty, Some (k ~context outty), patterns)) ;; (* persistent state *) @@ -267,34 +242,39 @@ let instantiate32 idrefs env symbol args = if args = [] then head else Ast.Appl (head :: List.map instantiate_arg args) -let rec nast_of_cic1 ~freshid ~output_type ~subst ~context father_id term = +let rec nast_of_cic1 ~idref ~output_type ~subst ~context term = match (get_compiled32 ()) term with | None -> - 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 + 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 idref ast (*Ast.AttributedTerm (`IdRef (idref term), ast)*) ;; @@ -407,10 +387,9 @@ let instantiate_appl_pattern aux appl_pattern *) -let nmap_sequent0 ~freshid ~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 nast_of_cic ~context = - nast_of_cic1 ~freshid ~output_type:`Term ~subst ~context None in + let nast_of_cic = nast_of_cic1 ~idref ~output_type:`Term ~subst in let context',_ = List.fold_right (fun item (res,context) -> @@ -444,12 +423,9 @@ let nmap_sequent0 ~freshid ~subst (i,(n,context,ty):int * NCic.conjecture) = let nmap_sequent ~subst metasenv = let module K = Content in - let ids_to_refs = Hashtbl.create 503 in - let ids_to_father_ids = Hashtbl.create 503 in + let ids_to_refs = Hashtbl.create 211 in let register_ref = Hashtbl.add ids_to_refs in - 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 + nmap_sequent0 ~idref:(idref register_ref) ~subst metasenv, ids_to_refs ;; let object_prefix = "obj:";; @@ -522,20 +498,18 @@ 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 503 in + let ids_to_refs = Hashtbl.create 211 in let register_ref = Hashtbl.add ids_to_refs 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 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 ~freshid ~subst) metasenv) + Some (List.map (nmap_sequent0 ~idref ~subst) metasenv) in let res = match kind with @@ -585,5 +559,5 @@ and }) l *) in - res,ids_to_refs,ids_to_father_ids + 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 e5a6f26c9..bae7daee2 100644 --- a/helm/software/components/ng_cic_content/nTermCicContent.mli +++ b/helm/software/components/ng_cic_content/nTermCicContent.mli @@ -88,12 +88,9 @@ type id = string val nmap_sequent: subst:NCic.substitution -> int * NCic.conjecture -> CicNotationPt.term Content.conjecture * - (id, NReference.reference) Hashtbl.t * (* id -> reference *) - (string, id option) Hashtbl.t (* id -> father_id *) - + (id, NReference.reference) Hashtbl.t (* id -> reference *) val nmap_obj: NCic.obj -> CicNotationPt.term Content.cobj * - (id, NReference.reference) Hashtbl.t * (* id -> reference *) - (string, id option) Hashtbl.t (* id -> father_id *) + (id, NReference.reference) Hashtbl.t (* id -> reference *) diff --git a/helm/software/components/syntax_extensions/.depend b/helm/software/components/syntax_extensions/.depend index 25e67131f..f3c6a8bd1 100644 --- a/helm/software/components/syntax_extensions/.depend +++ b/helm/software/components/syntax_extensions/.depend @@ -1,5 +1,2 @@ -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 e23400fb2..4015293a4 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,ids_to_father_ids = + let content_sequent,ids_to_refs = 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,ids_to_father_ids + Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres 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,ids_to_father_ids = NTermCicContent.nmap_obj obj in + 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,ids_to_father_ids + 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/applyTransformation.mli b/helm/software/matita/applyTransformation.mli index 9fe4130c3..f41f0a7a1 100644 --- a/helm/software/matita/applyTransformation.mli +++ b/helm/software/matita/applyTransformation.mli @@ -47,8 +47,7 @@ val mml_of_cic_sequent: val nmml_of_cic_sequent: NCic.metasenv -> NCic.substitution -> (* metasenv, substitution *) int * NCic.conjecture -> (* sequent *) - Gdome.document * (* Math ML *) - (string, NTermCicContent.id option) Hashtbl.t (* id -> father id *) + Gdome.document (* Math ML *) val mml_of_cic_object: Cic.obj -> (* object *) @@ -61,10 +60,7 @@ 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 * - (string, NTermCicContent.id option) Hashtbl.t (* id -> father id *) - +val nmml_of_cic_object: NCic.obj -> Gdome.document 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 a6aa89e81..277dbe8f1 100644 --- a/helm/software/matita/matitaMathView.ml +++ b/helm/software/matita/matitaMathView.ml @@ -186,11 +186,8 @@ 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 @@ -514,11 +511,6 @@ 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 = @@ -603,10 +595,9 @@ object (self) method nload_sequent metasenv subst metano = let sequent = List.assoc metano metasenv in - let mathml,ids_to_father_ids = + let mathml = 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 @@ -640,9 +631,10 @@ object (self) current_mathml <- Some mathml); method load_nobject obj = - let mathml,ids_to_father_ids = ApplyTransformation.nmml_of_cic_object obj in - self#set_ncic_info (Some ids_to_father_ids); + let mathml = ApplyTransformation.nmml_of_cic_object obj in (* + 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