X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_cic_content%2FnTermCicContent.ml;h=da8061fde197d56c3d482c071d75276ffa74cae1;hb=11b2157bacf59cfc561c2ef6f92ee41ee2c1a006;hp=826238d1c0b7b85b79a8e72dd53a55124dd6049a;hpb=7deb0d8f534f779adb1b5813a7f159609b9cba3c;p=helm.git diff --git a/helm/software/components/ng_cic_content/nTermCicContent.ml b/helm/software/components/ng_cic_content/nTermCicContent.ml index 826238d1c..da8061fde 100644 --- a/helm/software/components/ng_cic_content/nTermCicContent.ml +++ b/helm/software/components/ng_cic_content/nTermCicContent.ml @@ -32,11 +32,11 @@ module Ast = CicNotationPt let debug = false let debug_print s = if debug then prerr_endline (Lazy.force s) else () +type id = string + (* type interpretation_id = int -let idref id t = Ast.AttributedTerm (`IdRef id, t) - type term_info = { sort: (Cic.id, Ast.sort_kind) Hashtbl.t; uri: (Cic.id, UriManager.uri) Hashtbl.t; @@ -49,27 +49,39 @@ let get_types uri = | _ -> assert false *) +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) +;; + (* CODICE c&p da NCicPp *) -let nast_of_cic ~output_type ~subst ~context = - let rec k ctx = function +let nast_of_cic0 + ~(idref: + ?reference:NReference.reference -> CicNotationPt.term -> CicNotationPt.term) + ~output_type ~subst k ~context = + function | NCic.Rel n -> (try - let name,_ = List.nth ctx (n-1) in + let name,_ = List.nth context (n-1) in let name = if name = "_" then "__"^string_of_int n else name in - Ast.Ident (name,None) + idref (Ast.Ident (name,None)) with Failure "nth" | Invalid_argument "List.nth" -> - Ast.Ident ("-" ^ string_of_int (n - List.length ctx),None)) - | NCic.Const r -> Ast.Ident (NCicPp.r2s false r, None) + 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 ctx (NCicSubstitution.subst_meta lc t) + k ~context (NCicSubstitution.subst_meta lc t) | NCic.Meta (n,(s,l)) -> (* CSC: qua non dovremmo espandere *) let l = NCicUtils.expand_local_context l in - Ast.Meta - (n, List.map (fun x -> Some (k ctx (NCicSubstitution.lift s x))) l) - | NCic.Sort NCic.Prop -> Ast.Sort `Prop - | NCic.Sort NCic.Type _ -> Ast.Sort `Set + 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) (* 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) @@ -80,27 +92,28 @@ let nast_of_cic ~output_type ~subst ~context = (List.tl l); F.fprintf f ")"*) (* CSC: qua siamo grezzi *) - | NCic.Implicit `Hole -> Ast.UserInput - | NCic.Implicit _ -> Ast.Implicit + | NCic.Implicit `Hole -> idref (Ast.UserInput) + | NCic.Implicit _ -> idref (Ast.Implicit) | NCic.Prod (n,s,t) -> + let n = if n.[0] = '_' then "_" else n in let binder_kind = `Forall in - Ast.Binder (binder_kind, (Ast.Ident (n,None), Some (k ctx s)), - k ((n,NCic.Decl s)::ctx) t) + 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) -> - Ast.Binder (`Lambda,(Ast.Ident (n,None), Some (k ctx s)), - k ((n,NCic.Decl s)::ctx) 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) -> - Ast.LetIn ((Ast.Ident (n,None), Some (k ctx ty)), k ctx s, - k ((n,NCic.Decl s)::ctx) 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 ctx + 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 -> Ast.Appl (List.map (k ctx) args) + | NCic.Appl args -> idref (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 @@ -124,8 +137,8 @@ let nast_of_cic ~output_type ~subst ~context = 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 ctx s)) :: cv, rhs - | _, _ -> [], k ctx pat + (Ast.Ident (name,None), Some (k ~context s)) :: cv, rhs + | _, _ -> [], k ~context pat in let j = ref 0 in let patterns = @@ -135,8 +148,8 @@ let nast_of_cic ~output_type ~subst ~context = incr j; let name,(capture_variables,rhs) = match output_type with - `Term -> name, eat_branch leftno ctx ty pat - | `Pattern -> "_", ([], k ctx pat) + `Term -> name, eat_branch leftno context ty pat + | `Pattern -> "_", ([], k ~context pat) in Ast.Pattern (name, None(*CSC Some (ctor_puri !j)*), capture_variables), rhs ) constructors patterns @@ -147,54 +160,21 @@ let nast_of_cic ~output_type ~subst ~context = `Pattern -> None | `Term -> Some case_indty in - Ast.Case (k ctx te, indty, Some (k ctx outty), patterns) - in - k context -;; - -let nmap_sequent ~subst (i,(n,context,ty):int * NCic.conjecture) = - let module K = Content in - let context',_ = - 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 ~output_type:`Term ~subst ~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 ~output_type:`Term ~subst ~context t; - K.def_type = nast_of_cic ~output_type:`Term ~subst ~context ty - })::res,item::context - ) context ([],[]) - in - "-1",i,context',nast_of_cic ~output_type:`Term ~subst ~context ty + idref (Ast.Case (k ~context te, indty, Some (k ~context outty), patterns)) ;; -(* (* persistent state *) +(* let initial_level2_patterns32 () = Hashtbl.create 211 let initial_interpretations () = Hashtbl.create 211 let level2_patterns32 = ref (initial_level2_patterns32 ()) (* symb -> id list ref *) let interpretations = ref (initial_interpretations ()) +*) let compiled32 = ref None +(* let pattern32_matrix = ref [] let counter = ref ~-1 @@ -220,6 +200,7 @@ let pop () = compiled32 := ocompiled32; pattern32_matrix := opattern32_matrix ;; +*) let get_compiled32 () = match !compiled32 with @@ -231,7 +212,7 @@ let set_compiled32 f = compiled32 := Some f let add_idrefs = List.fold_right (fun idref t -> Ast.AttributedTerm (`IdRef idref, t)) -let instantiate32 term_info idrefs env symbol args = +let instantiate32 idrefs env symbol args = let rec instantiate_arg = function | Ast.IdentArg (n, name) -> let t = @@ -261,42 +242,53 @@ let instantiate32 term_info idrefs env symbol args = if args = [] then head else Ast.Appl (head :: List.map instantiate_arg args) -let rec ast_of_acic1 ~output_type term_info annterm = - let id_to_uris = term_info.uri in - let register_uri id uri = Hashtbl.add id_to_uris id uri in - match (get_compiled32 ()) annterm with +let rec nast_of_cic1 ~idref ~output_type ~subst ~context term = + match (get_compiled32 ()) term with | None -> - ast_of_acic0 ~output_type term_info annterm (ast_of_acic1 ~output_type) + 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 annterm -> - let idref = CicUtil.id_of_annterm annterm in - (try - register_uri idref - (CicUtil.uri_of_term (Deannotate.deannotate_term annterm)) - with Invalid_argument _ -> ()); - idref) - ctors + 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' = + let env = List.map - (fun (name, term) -> name, ast_of_acic1 ~output_type term_info term) env + (fun (name, term) -> + name, + nast_of_cic1 ~idref ~output_type ~subst ~context term + ) env in let _, symbol, args, _ = try - Hashtbl.find !level2_patterns32 pid + TermAcicContent.find_level2_patterns32 pid with Not_found -> assert false in - let ast = instantiate32 term_info idrefs env' symbol args in - Ast.AttributedTerm (`IdRef (CicUtil.id_of_annterm annterm), ast) + let ast = instantiate32 idrefs env symbol args in + idref ast (*Ast.AttributedTerm (`IdRef (idref term), ast)*) +;; let load_patterns32 t = - let t = - HExtlib.filter_map (function (true, ap, id) -> Some (ap, id) | _ -> None) t - in - set_compiled32 (lazy (Acic2astMatcher.Matcher32.compiler t)) + let t = + HExtlib.filter_map (function (true, ap, id) -> Some (ap, id) | _ -> None) t + in + set_compiled32 (lazy (Ncic2astMatcher.Matcher32.compiler t)) +in + TermAcicContent.add_load_patterns32 load_patterns32; + TermAcicContent.init () +;; +(* let ast_of_acic ~output_type id_to_sort annterm = debug_print (lazy ("ast_of_acic <- " ^ CicPp.ppterm (Deannotate.deannotate_term annterm))); @@ -394,3 +386,42 @@ let instantiate_appl_pattern in aux appl_pattern *) + +let nmap_sequent ~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 context',_ = + 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,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 + ) context ([],[]) + in + ("-1",i,context',nast_of_cic ~context ty), ids_to_refs +;; +