X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_cic_content%2FnTermCicContent.ml;h=a558d99cfe98200fad80997f097affca1eec43b4;hb=32d3f10c1904d450ce8ea3525230acc6980a5601;hp=3253e7908802446780ab1f6a180dea3ff0503489;hpb=21d58ec6efaf1969c42eb3929475b638cdd0ce2e;p=helm.git diff --git a/helm/software/components/ng_cic_content/nTermCicContent.ml b/helm/software/components/ng_cic_content/nTermCicContent.ml index 3253e7908..a558d99cf 100644 --- a/helm/software/components/ng_cic_content/nTermCicContent.ml +++ b/helm/software/components/ng_cic_content/nTermCicContent.ml @@ -35,8 +35,6 @@ let debug_print s = if debug then prerr_endline (Lazy.force s) else () (* 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; @@ -45,126 +43,107 @@ type term_info = let get_types uri = let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in match o with - | Cic.InductiveDefinition (l,_,lpsno,_) -> l, lpsno + | Cic.InductiveDefinition (l,_,leftno,_) -> l, leftno | _ -> assert false - -let name_of_inductive_type uri i = - let types, _ = get_types uri in - let (name, _, _, _) = try List.nth types i with Not_found -> assert false in - name - - (* returns pairs *) -let constructors_of_inductive_type uri i = - let types, _ = get_types uri in - let (_, _, _, constructors) = - try List.nth types i with Not_found -> assert false - in - constructors - - (* returns name only *) -let constructor_of_inductive_type uri i j = - (try - fst (List.nth (constructors_of_inductive_type uri i) (j-1)) - with Not_found -> assert false) - - (* returns the number of left parameters *) -let left_params_no_of_inductive_type uri = - snd (get_types uri) *) -(* CODICE c&p da NCicPp *) -let r2s pp_fix_name r = - try - match r with - | NReference.Ref (u,NReference.Ind (_,i,_)) -> - (match NCicLibrary.get_obj u with - | _,_,_,_, NCic.Inductive (_,_,itl,_) -> - let _,name,_,_ = List.nth itl i in name - | _ -> assert false) - | NReference.Ref (u,NReference.Con (i,j,_)) -> - (match NCicLibrary.get_obj u with - | _,_,_,_, NCic.Inductive (_,_,itl,_) -> - let _,_,_,cl = List.nth itl i in - let _,name,_ = List.nth cl (j-1) in name - | _ -> assert false) - | NReference.Ref (u,(NReference.Decl | NReference.Def _)) -> - (match NCicLibrary.get_obj u with - | _,_,_,_, NCic.Constant (_,name,_,_,_) -> name - | _ -> assert false) - | NReference.Ref (u,(NReference.Fix (i,_,_)|NReference.CoFix i)) -> - (match NCicLibrary.get_obj u with - | _,_,_,_, NCic.Fixpoint (_,fl,_) -> - if pp_fix_name then - let _,name,_,_,_ = List.nth fl i in name - else - NUri.name_of_uri u ^"("^ string_of_int i ^ ")" - | _ -> assert false) - with NCicLibrary.ObjectNotFound _ -> NReference.string_of_reference r +let idref () = + let id = ref 0 in + function t -> + incr id; + Ast.AttributedTerm (`IdRef ("i" ^ string_of_int !id), t) ;; -let nast_of_cic ~subst = - let rec k = function - | NCic.Rel n -> Ast.Ident ("-" ^ string_of_int n, None) - | NCic.Const r -> Ast.Ident (r2s true r, None) +(* CODICE c&p da NCicPp *) +let nast_of_cic ~idref ~output_type ~subst ~context = + let rec k ctx = function + | NCic.Rel n -> + (try + let name,_ = List.nth ctx (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 ctx),None))) + | NCic.Const r -> idref (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) - | NCic.Meta (n,l) -> Ast.Meta (n, [](*aux_context l*)) - | NCic.Sort NCic.Prop -> Ast.Sort `Prop - | NCic.Sort NCic.Type _ -> Ast.Sort `Set - | NCic.Implicit `Hole -> Ast.UserInput - | NCic.Implicit _ -> Ast.Implicit + k ctx (NCicSubstitution.subst_meta 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 ctx (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) + | C.Sort (C.Type l) -> + F.fprintf f "Max("; + aux ctx (C.Sort (C.Type [List.hd l])); + List.iter (fun x -> F.fprintf f ",";aux ctx (C.Sort (C.Type [x]))) + (List.tl l); + F.fprintf f ")"*) + (* CSC: qua siamo grezzi *) + | NCic.Implicit `Hole -> idref (Ast.UserInput) + | NCic.Implicit _ -> idref (Ast.Implicit) | NCic.Prod (n,s,t) -> let binder_kind = `Forall in - Ast.Binder (binder_kind, (Ast.Ident (n,None), Some (k s)), k t) + idref (Ast.Binder (binder_kind, (Ast.Ident (n,None), Some (k ctx s)), + k ((n,NCic.Decl s)::ctx) t)) | NCic.Lambda (n,s,t) -> - Ast.Binder (`Lambda,(Ast.Ident (n,None), Some (k s)), k t) + idref (Ast.Binder (`Lambda,(Ast.Ident (n,None), Some (k ctx s)), + k ((n,NCic.Decl s)::ctx) t)) | NCic.LetIn (n,s,ty,t) -> - Ast.LetIn ((Ast.Ident (n,None), Some (k ty)), k s, k t) + idref (Ast.LetIn ((Ast.Ident (n,None), Some (k ctx ty)), k ctx s, + k ((n,NCic.Decl s)::ctx) 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 ctx (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 args) - (*| NCic.AConst (id,uri,substs) -> - register_uri id uri; - idref id (Ast.Ident (UriManager.name_of_uri uri, aux_substs substs))*) - | NCic.Match (uri,ty,te,patterns) -> -(* - let name = NReference.name_of_reference uri in + | NCic.Appl args -> idref (Ast.Appl (List.map (k ctx) 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, Some (UriManager.uri_of_string puri_str) in - let constructors = constructors_of_inductive_type uri typeno in - let lpsno = left_params_no_of_inductive_type uri in - let rec eat_branch n ty pat = +*) + let case_indty = + name, None(*CSC Some (UriManager.uri_of_string puri_str)*) in + let constructors, leftno = + let _,leftno,tys,_,n = NCicEnvironment.get_checked_indtys r in + let _,_,_,cl = List.nth tys n in + cl,leftno + in + let rec eat_branch n ctx ty pat = match (ty, pat) with - | NCic.Prod (_, _, t), _ when n > 0 -> eat_branch (pred n) t pat - | NCic.Prod (_, _, t), NCic.ALambda (_, name, s, t') -> - let (cv, rhs) = eat_branch 0 t t' in - (CicNotationUtil.name_of_cic_name name, Some (k s)) :: cv, rhs - | _, _ -> [], k pat + | NCic.Prod (name, s, t), _ when n > 0 -> + 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 in let j = ref 0 in let patterns = try List.map2 - (fun (name, ty) pat -> + (fun (_, name, ty) pat -> incr j; let name,(capture_variables,rhs) = match output_type with - `Term -> name, eat_branch lpsno ty pat - | `Pattern -> "_", ([], k pat) + `Term -> name, eat_branch leftno ctx ty pat + | `Pattern -> "_", ([], k ctx pat) in - Ast.Pattern (name, 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 @@ -173,18 +152,19 @@ let nast_of_cic ~subst = `Pattern -> None | `Term -> Some case_indty in - idref id (Ast.Case (k te, indty, Some (k ty), patterns)) -*) Ast.Ident ("Un case",None) + idref (Ast.Case (k ctx te, indty, Some (k ctx outty), patterns)) in - k + k context ;; let nmap_sequent ~subst (i,(n,context,ty):int * NCic.conjecture) = let module K = Content in - let context' = - List.map - (function - | name,NCic.Decl t -> + let nast_of_cic = nast_of_cic ~idref:(idref ()) ~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 *) @@ -193,9 +173,9 @@ let nmap_sequent ~subst (i,(n,context,ty):int * NCic.conjecture) = K.dec_id = "-1"; K.dec_inductive = false; K.dec_aref = "-1"; - K.dec_type = t - }) - | name,NCic.Def (t,ty) -> + 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 *) @@ -203,12 +183,12 @@ let nmap_sequent ~subst (i,(n,context,ty):int * NCic.conjecture) = { K.def_name = (Some name); K.def_id = "-1"; K.def_aref = "-1"; - K.def_term = t; - K.def_type = ty - }) - ) context + K.def_term = nast_of_cic ~context t; + K.def_type = nast_of_cic ~context ty + })::res,item::context + ) context ([],[]) in - "-1",i,context',ty + "-1",i,context',nast_of_cic ~context ty ;; (*