X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fng_cic_content%2Finterpretations.ml;h=ed2b58a79235389ae0f335975aad982a454f9854;hb=cdb85e803cd6038352ec0a318285f96f42faf02d;hp=ee4bb9437ca5a5002f3f2587768b29a03ac2e239;hpb=cacbe3c6493ddce76c4c13379ade271d8dd172e8;p=helm.git diff --git a/matitaB/components/ng_cic_content/interpretations.ml b/matitaB/components/ng_cic_content/interpretations.ml index ee4bb9437..ed2b58a79 100644 --- a/matitaB/components/ng_cic_content/interpretations.ml +++ b/matitaB/components/ng_cic_content/interpretations.ml @@ -38,11 +38,6 @@ let hide_coercions = ref true;; type cic_id = string -type term_info = - { sort: (cic_id, Ast.sort_kind) Hashtbl.t; - uri: (cic_id, NReference.reference) Hashtbl.t; - } - module IntMap = Map.Make(struct type t = int let compare = compare end);; module StringMap = Map.Make(String);; @@ -72,9 +67,9 @@ class type g_status = method interp_db: db end -class virtual status = +class virtual status uid = object(self) - inherit NCicCoercion.status + inherit NCicCoercion.status uid val mutable interp_db = None (* mutable only to initialize it :-( *) method interp_db = match interp_db with None -> assert false | Some x -> x method set_interp_db v = {< interp_db = Some v >} @@ -85,15 +80,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 +89,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 dsc args = let rec instantiate_arg = function | Ast.IdentArg (n, name) -> let t = @@ -122,23 +105,20 @@ let instantiate32 idrefs env symbol args = let rec add_lambda t n = if n > 0 then let name = NotationUtil.fresh_name () in - Ast.Binder (`Lambda, (Ast.Ident (name, None), None), - Ast.Appl [add_lambda t (n - 1); Ast.Ident (name, None)]) + Ast.Binder (`Lambda, (Ast.Ident (name, `Ambiguous), None), + Ast.Appl [add_lambda t (n - 1); Ast.Ident (name, `Ambiguous)]) else t in add_lambda t (n - count_lambda t) in - let head = - let symbol = Ast.Symbol (symbol, 0) in - add_idrefs idrefs symbol - in + let head = Ast.Symbol (symbol, Some (None, dsc)) 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,52 +206,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,None)) + Ast.Ident (name,`Ambiguous) 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 status true r, None)) + 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,None), 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,None), 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,None), 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 @@ -282,7 +261,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, -1)) + | Some n -> Ast.Num (string_of_int n, None) | None -> let args = if not !hide_coercions then args @@ -302,20 +281,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 @@ -327,7 +298,7 @@ let nast_of_cic0 status eat_branch (pred n) 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:ctx s)) :: cv, rhs + (Ast.Ident (name,`Ambiguous), Some (k ~context:ctx s)) :: cv, rhs | _, _ -> [], k ~context:ctx pat in let j = ref 0 in @@ -350,86 +321,54 @@ 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",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 status ~idref ~output_type ~subst ~metasenv ~context + nast_of_cic1 status ~output_type ~subst ~metasenv ~context term ) env in - let _, symbol, args, _ = + let dsc, symbol, args, _ = try 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 dsc 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:";; @@ -438,6 +377,7 @@ let definition_prefix = "def:";; let inductive_prefix = "ind:";; let joint_prefix = "joint:";; +(* let get_id = function Ast.AttributedTerm (`IdRef id, _) -> id @@ -450,58 +390,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 = @@ -588,12 +476,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