X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_cic_content%2FnTermCicContent.ml;h=3c17823b6c9160e25f298839d67c41703a395aba;hb=07713b63c109a99c2b9dc7265571bcdd3dd6ed0d;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..3c17823b6 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 = +let nast_of_cic0 status + ~(idref: + ?reference:NReference.reference -> CicNotationPt.term -> CicNotationPt.term) + ~output_type ~metasenv ~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,51 @@ 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 `Vector -> idref (Ast.Implicit `Vector) + | NCic.Implicit _ -> idref (Ast.Implicit `JustOne) | 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,NCic.Rel 1) -> + idref (Ast.Cast (k ~context ty, k ~context s)) | 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 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 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 as t -> + let args = + if not !Acic2content.hide_coercions then args + else + match + NCicCoercion.match_coercion status ~metasenv ~context ~subst t + with + | None -> args + | Some (_,sats,cpos) -> +(* CSC: sats e' il numero di pi, ma non so cosa farmene! voglio il numero di + argomenti da saltare, come prima! *) + if cpos < List.length args - 1 then + List.nth args (cpos + 1) :: + try snd (HExtlib.split_nth (cpos+sats+2) args) with Failure _->[] + else + args + in + (match args with + [arg] -> idref (k ~context arg) + | _ -> 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 @@ -156,11 +156,11 @@ let nast_of_cic0 let rec eat_branch n ctx ty pat = match (ty, pat) with | NCic.Prod (name, s, t), _ when n > 0 -> - eat_branch (pred n) ((name,NCic.Decl s)::ctx) t pat + 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 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 +171,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 +182,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 +264,40 @@ 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 status ~idref ~output_type ~metasenv ~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 status ~idref ~output_type ~metasenv ~subst + (nast_of_cic1 status ~idref ~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) + (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 status ~idref ~output_type ~subst ~metasenv ~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 +410,10 @@ let instantiate_appl_pattern aux appl_pattern *) -let nmap_sequent0 ~freshid ~subst (i,(n,context,ty):int * NCic.conjecture) = +let nmap_sequent0 status ~idref ~metasenv ~subst (i,(n,context,ty)) = 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 status ~idref ~output_type:`Term ~metasenv ~subst in let context',_ = List.fold_right (fun item (res,context) -> @@ -442,19 +445,19 @@ let nmap_sequent0 ~freshid ~subst (i,(n,context,ty):int * NCic.conjecture) = ("-1",i,context',nast_of_cic ~context ty) ;; -let nmap_sequent ~subst metasenv = +let nmap_sequent status ~metasenv ~subst conjecture = 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 status ~idref:(idref register_ref) ~metasenv ~subst conjecture, + ids_to_refs ;; let object_prefix = "obj:";; let declaration_prefix = "decl:";; let definition_prefix = "def:";; +let inductive_prefix = "ind:";; +let joint_prefix = "joint:";; let get_id = function @@ -520,26 +523,76 @@ let build_decl_item seed id n s = } ;; -let nmap_obj (uri,_,metasenv,subst,kind) = +let nmap_obj status (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 status ~idref ~output_type:`Term ~metasenv ~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 status ~idref ~metasenv ~subst) metasenv) in +let build_constructors seed l = + List.map + (fun (_,n,ty) -> + let ty = nast_of_cic ~context:[] ty in + { K.dec_name = Some n; + K.dec_id = gen_id declaration_prefix seed; + K.dec_inductive = false; + K.dec_aref = ""; + K.dec_type = ty + }) l +in +let build_inductive b seed = + fun (_,n,ty,cl) -> + let ty = nast_of_cic ~context:[] ty in + `Inductive + { K.inductive_id = gen_id inductive_prefix seed; + K.inductive_name = n; + K.inductive_kind = b; + K.inductive_type = ty; + K.inductive_constructors = build_constructors seed cl + } +in +let build_fixpoint b seed = + fun (_,n,_,ty,t) -> + let t = nast_of_cic ~context:[] t in + let ty = nast_of_cic ~context:[] ty in + `Definition + { K.def_id = gen_id inductive_prefix seed; + K.def_name = Some n; + K.def_aref = ""; + K.def_type = ty; + K.def_term = t; + } +in let res = match kind with - NCic.Constant (_,_,Some bo,ty,_) -> + | NCic.Fixpoint (is_rec, ifl, _) -> + (gen_id object_prefix seed, [], conjectures, + `Joint + { K.joint_id = gen_id joint_prefix seed; + K.joint_kind = + if is_rec then + `Recursive (List.map (fun (_,_,i,_,_) -> i) ifl) + else `CoRecursive; + K.joint_defs = List.map (build_fixpoint is_rec seed) ifl + }) + | NCic.Inductive (is_ind, lno, itl, _) -> + (gen_id object_prefix seed, [], conjectures, + `Joint + { K.joint_id = gen_id joint_prefix seed; + K.joint_kind = + if is_ind then `Inductive lno else `CoInductive lno; + K.joint_defs = List.map (build_inductive is_ind seed) itl + }) + | NCic.Constant (_,_,Some bo,ty,_) -> let ty = nast_of_cic ~context:[] ty in let bo = nast_of_cic ~context:[] bo in (gen_id object_prefix seed, [], conjectures, @@ -551,39 +604,6 @@ let nmap_obj (uri,_,metasenv,subst,kind) = `Decl (K.Const, (*CSC: ??? get_id ty here used to be the id of the axiom! *) build_decl_item seed (get_id ty) (NUri.name_of_uri uri) ty)) -(* - | C.AInductiveDefinition (id,l,params,nparams,_) -> - (gen_id object_prefix seed, params, conjectures, - `Joint - { K.joint_id = gen_id joint_prefix seed; - K.joint_kind = `Inductive nparams; - K.joint_defs = List.map (build_inductive seed) l - }) - -and - build_inductive seed = - let module K = Content in - fun (_,n,b,ty,l) -> - `Inductive - { K.inductive_id = gen_id inductive_prefix seed; - K.inductive_name = n; - K.inductive_kind = b; - K.inductive_type = ty; - K.inductive_constructors = build_constructors seed l - } - -and - build_constructors seed l = - let module K = Content in - List.map - (fun (n,t) -> - { K.dec_name = Some n; - K.dec_id = gen_id declaration_prefix seed; - K.dec_inductive = false; - K.dec_aref = ""; - K.dec_type = t - }) l -*) in - res,ids_to_refs,ids_to_father_ids + res,ids_to_refs ;;