X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_cic_content%2FnTermCicContent.ml;h=01e6fd48255fc97039a06407a5d03d6088951664;hb=72cd94b68037956a70b98cfa54f316fd54e52bae;hp=b1b2efec81e3b9ebe275d9a7a0e0c79cbf66981c;hpb=442f3a15d7c6afc480da02602d4d4c8db4f44c10;p=helm.git diff --git a/helm/software/components/ng_cic_content/nTermCicContent.ml b/helm/software/components/ng_cic_content/nTermCicContent.ml index b1b2efec8..01e6fd482 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:ctx s)) :: cv, rhs + | _, _ -> [], k ~context:ctx 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 ;;