From 53d4524b2dbe23f5b48f00099d8ff39efb00941d Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 20 May 2011 08:49:10 +0000 Subject: [PATCH] Simplified rendering --- .../ng_cic_content/interpretations.ml | 216 +++++------------- .../ng_cic_content/interpretations.mli | 10 +- 2 files changed, 57 insertions(+), 169 deletions(-) diff --git a/matitaB/components/ng_cic_content/interpretations.ml b/matitaB/components/ng_cic_content/interpretations.ml index 5f41a1fe5..598c93af7 100644 --- a/matitaB/components/ng_cic_content/interpretations.ml +++ b/matitaB/components/ng_cic_content/interpretations.ml @@ -85,15 +85,6 @@ class virtual status = interp_db <- Some (initial_db self) end -let idref register_ref = - let id = ref 0 in - fun ?reference t -> - 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) -;; - let level_of_uri u = let name = NUri.name_of_uri u in assert(String.length name > String.length "Type"); @@ -103,10 +94,7 @@ let level_of_uri u = let find_level2_patterns32 status pid = IntMap.find pid status#interp_db.level2_patterns32 -let add_idrefs = - List.fold_right (fun idref t -> Ast.AttributedTerm (`IdRef idref, t)) - -let instantiate32 idrefs env symbol args = +let instantiate32 env symbol args = let rec instantiate_arg = function | Ast.IdentArg (n, name) -> let t = @@ -129,16 +117,13 @@ let instantiate32 idrefs env symbol args = in add_lambda t (n - count_lambda t) in - let head = - let symbol = Ast.Symbol (symbol, None) in - add_idrefs idrefs symbol - in + let head = Ast.Symbol (symbol, None) in if args = [] then head else Ast.Appl (head :: List.map instantiate_arg args) let fresh_id status = - let counter = status#interp_db.counter+1 in - status#set_interp_db ({ status#interp_db with counter = counter }), counter + let counter = status#interp_db.counter + 1 in + status#set_interp_db {status#interp_db with counter = counter},counter let load_patterns32 status t = let t = @@ -226,53 +211,51 @@ let destroy_nat = in aux 0 -(* CODICE c&p da NCicPp *) let nast_of_cic0 status - ~(idref: - ?reference:NReference.reference -> NotationPt.term -> NotationPt.term) ~output_type ~metasenv ~subst k ~context = 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,`Ambiguous)) + Ast.Ident (name,`Ambiguous) with Failure "nth" | Invalid_argument "List.nth" -> - idref (Ast.Ident ("-" ^ string_of_int (n - List.length - context),`Ambiguous))) - | NCic.Const r -> idref ~reference:r (Ast.Ident (NCicPp.r2s status true r, `Ambiguous)) + Ast.Ident ("-" ^ string_of_int (n - List.length context),`Ambiguous)) + | NCic.Const r -> + let uri = `Uri (NReference.string_of_reference r) in + Ast.Ident (NCicPp.r2s status true r, uri) | NCic.Meta (n,lc) when List.mem_assoc n subst -> let _,_,t,_ = List.assoc n subst in k ~context (NCicSubstitution.subst_meta status lc t) | NCic.Meta (n,(s,l)) -> (* 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 status s x))) l)) - | NCic.Sort NCic.Prop -> idref (Ast.Sort `Prop) - | NCic.Sort NCic.Type [] -> idref (Ast.Sort `Set) + Ast.Meta + (n, List.map (fun x -> Some (k ~context (NCicSubstitution.lift status s x))) l) + | NCic.Sort NCic.Prop -> Ast.Sort `Prop + | NCic.Sort NCic.Type [] -> Ast.Sort `Set | NCic.Sort NCic.Type ((`Type,u)::_) -> - idref(Ast.Sort (`NType (level_of_uri u))) + Ast.Sort (`NType (level_of_uri u)) | NCic.Sort NCic.Type ((`CProp,u)::_) -> - idref(Ast.Sort (`NCProp (level_of_uri u))) + Ast.Sort (`NCProp (level_of_uri u)) | NCic.Sort NCic.Type ((`Succ,u)::_) -> - idref(Ast.Sort (`NType (level_of_uri u ^ "+1"))) - | NCic.Implicit `Hole -> idref (Ast.UserInput) - | NCic.Implicit `Vector -> idref (Ast.Implicit `Vector) - | NCic.Implicit _ -> idref (Ast.Implicit `JustOne) + Ast.Sort (`NType (level_of_uri u ^ "+1")) + | NCic.Implicit `Hole -> Ast.UserInput + | NCic.Implicit `Vector -> Ast.Implicit `Vector + | NCic.Implicit _ -> Ast.Implicit `JustOne | 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,`Ambiguous), Some (k ~context s)), - k ~context:((n,NCic.Decl s)::context) t)) + Ast.Binder (binder_kind, (Ast.Ident (n,`Ambiguous), Some (k ~context s)), + k ~context:((n,NCic.Decl s)::context) t) | NCic.Lambda (n,s,t) -> - idref (Ast.Binder (`Lambda,(Ast.Ident (n,`Ambiguous), Some (k ~context s)), - k ~context:((n,NCic.Decl s)::context) t)) + Ast.Binder (`Lambda,(Ast.Ident (n,`Ambiguous), Some (k ~context s)), + k ~context:((n,NCic.Decl s)::context) t) | NCic.LetIn (n,s,ty,NCic.Rel 1) -> - idref (Ast.Cast (k ~context ty, k ~context s)) + Ast.Cast (k ~context ty, k ~context s) | NCic.LetIn (n,s,ty,t) -> - idref (Ast.LetIn ((Ast.Ident (n,`Ambiguous), Some (k ~context s)), k ~context - ty, k ~context:((n,NCic.Decl s)::context) t)) + Ast.LetIn ((Ast.Ident (n,`Ambiguous), Some (k ~context s)), k ~context + ty, 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 status lc t in @@ -283,7 +266,7 @@ let nast_of_cic0 status | _ -> NCic.Appl (hd :: args))) | NCic.Appl args as t -> (match destroy_nat t with - | Some n -> idref (Ast.Num (string_of_int n, None)) + | Some n -> Ast.Num (string_of_int n, None) | None -> let args = if not !hide_coercions then args @@ -303,20 +286,12 @@ let nast_of_cic0 status args in (match args with - [arg] -> idref (k ~context arg) - | _ -> idref (Ast.Appl (List.map (k ~context) args)))) + [arg] -> k ~context arg + | _ -> Ast.Appl (List.map (k ~context) args))) | NCic.Match (NReference.Ref (uri,_) as r,outty,te,patterns) -> let name = NUri.name_of_uri uri in -(* CSC - let uri_str = UriManager.string_of_uri uri in - let puri_str = sprintf "%s#xpointer(1/%d)" uri_str (typeno+1) in - let ctor_puri j = - UriManager.uri_of_string - (sprintf "%s#xpointer(1/%d/%d)" uri_str (typeno+1) j) - in -*) let case_indty = - name, None(*CSC Some (UriManager.uri_of_string puri_str)*) in + name, Some r in let constructors, leftno = let _,leftno,tys,_,n = NCicEnvironment.get_checked_indtys status r in let _,_,_,cl = List.nth tys n in @@ -351,34 +326,20 @@ let nast_of_cic0 status `Pattern -> None | `Term -> Some case_indty in - idref (Ast.Case (k ~context te, indty, Some (k ~context outty), patterns)) + Ast.Case (k ~context te, indty, Some (k ~context outty), patterns) ;; -let rec nast_of_cic1 status ~idref ~output_type ~metasenv ~subst ~context term = +let rec nast_of_cic1 status ~output_type ~metasenv ~subst ~context term = match Lazy.force status#interp_db.compiled32 term with | None -> - nast_of_cic0 status ~idref ~output_type ~metasenv ~subst - (nast_of_cic1 status ~idref ~output_type ~metasenv ~subst) ~context term + nast_of_cic0 status ~output_type ~metasenv ~subst + (nast_of_cic1 status ~output_type ~metasenv ~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) - (NotationPt.Ident ("dummy",`Ambiguous)) - in - match attrterm with - Ast.AttributedTerm (`IdRef id, _) -> id - | _ -> assert false - ) ctors - in let env = List.map (fun (name, term) -> name, - nast_of_cic1 status ~idref ~output_type ~subst ~metasenv ~context + nast_of_cic1 status ~output_type ~subst ~metasenv ~context term ) env in @@ -387,50 +348,32 @@ let rec nast_of_cic1 status ~idref ~output_type ~metasenv ~subst ~context term = find_level2_patterns32 status pid with Not_found -> assert false in - let ast = instantiate32 idrefs env symbol args in - idref ast (*Ast.AttributedTerm (`IdRef (idref term), ast)*) + instantiate32 env symbol args ;; -let nmap_context0 status ~idref ~metasenv ~subst context = - let module K = Content in +let nmap_context0 status ~metasenv ~subst context = let nast_of_cic = - nast_of_cic1 status ~idref ~output_type:`Term ~metasenv ~subst + nast_of_cic1 status ~output_type:`Term ~metasenv ~subst in fst ( List.fold_right (fun item (res,context) -> match item with | name,NCic.Decl t -> - Some - (* We should call build_decl_item, but we have not computed *) - (* the inner-types ==> we always produce a declaration *) - (`Declaration - { K.dec_name = (Some name); - K.dec_id = "-1"; - K.dec_inductive = false; - K.dec_aref = "-1"; - K.dec_type = nast_of_cic ~context t - })::res,item::context + (name, Ast.Decl (nast_of_cic ~context t))::res, + item::context | name,NCic.Def (t,ty) -> - Some - (* We should call build_def_item, but we have not computed *) - (* the inner-types ==> we always produce a declaration *) - (`Definition - { K.def_name = (Some name); - K.def_id = "-1"; - K.def_aref = "-1"; - K.def_term = nast_of_cic ~context t; - K.def_type = nast_of_cic ~context ty - })::res,item::context + (name, Ast.Def (nast_of_cic ~context t, + nast_of_cic ~context ty))::res, + item::context ) context ([],[])) ;; -let nmap_sequent0 status ~idref ~metasenv ~subst (i,(n,context,ty)) = - let module K = Content in +let nmap_sequent0 status ~metasenv ~subst (i,(n,context,ty)) = let nast_of_cic = - nast_of_cic1 status ~idref ~output_type:`Term ~metasenv ~subst in - let context' = nmap_context0 status ~idref ~metasenv ~subst context in - ("-1",i,context',nast_of_cic ~context ty) + nast_of_cic1 status ~output_type:`Term ~metasenv ~subst in + let context' = nmap_context0 status ~metasenv ~subst context in + (i,context',nast_of_cic ~context ty) ;; let object_prefix = "obj:";; @@ -439,6 +382,7 @@ let definition_prefix = "def:";; let inductive_prefix = "ind:";; let joint_prefix = "joint:";; +(* let get_id = function Ast.AttributedTerm (`IdRef id, _) -> id @@ -451,58 +395,6 @@ let gen_id prefix 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_obj0 status ~idref (uri,_,metasenv,subst,kind) = let module K = Content in let nast_of_cic = @@ -589,12 +481,12 @@ let with_idrefs foo status obj = ;; let nmap_obj status = with_idrefs nmap_obj0 status +*) + +let nmap_obj = assert false -let nmap_sequent status ~metasenv ~subst = - with_idrefs (nmap_sequent0 ~metasenv ~subst) status +let nmap_sequent = nmap_sequent0 -let nmap_term status ~metasenv ~subst ~context = - with_idrefs (nast_of_cic1 ~output_type:`Term ~metasenv ~subst ~context) status +let nmap_term = nast_of_cic1 ~output_type:`Term -let nmap_context status ~metasenv ~subst = - with_idrefs (nmap_context0 ~metasenv ~subst) status +let nmap_context = nmap_context0 diff --git a/matitaB/components/ng_cic_content/interpretations.mli b/matitaB/components/ng_cic_content/interpretations.mli index 71732cc7d..b2c59b9c9 100644 --- a/matitaB/components/ng_cic_content/interpretations.mli +++ b/matitaB/components/ng_cic_content/interpretations.mli @@ -79,21 +79,17 @@ val nmap_term: #status -> metasenv:NCic.metasenv -> subst:NCic.substitution -> context:NCic.context -> NCic.term -> - NotationPt.term * - (Content.id, NReference.reference) Hashtbl.t (* id -> reference *) + NotationPt.term val nmap_context: #status -> metasenv:NCic.metasenv -> subst:NCic.substitution -> - NCic.context -> - NotationPt.term Content.context * - (Content.id, NReference.reference) Hashtbl.t (* id -> reference *) + NCic.context -> NotationPt.context val nmap_sequent: #status -> metasenv:NCic.metasenv -> subst:NCic.substitution -> int * NCic.conjecture -> - NotationPt.term Content.conjecture * - (Content.id, NReference.reference) Hashtbl.t (* id -> reference *) + NotationPt.sequent val nmap_obj: #status -> NCic.obj -> -- 2.39.2