X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FoCic2NCic.ml;h=5b4d9f9e1222378768044194fd159b99f2902547;hb=805758c883a9bd9320942b310af8786ddb7f01b8;hp=d67089146171479ee83dac24f8429ff738668d8a;hpb=561d3c64857fc572a0d7cb3933a5525916cb0677;p=helm.git diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml index d67089146..5b4d9f9e1 100644 --- a/helm/software/components/ng_kernel/oCic2NCic.ml +++ b/helm/software/components/ng_kernel/oCic2NCic.ml @@ -93,7 +93,8 @@ prerr_endline ("LEFTNO: " ^ string_of_int leftno ^ " " ^ CicPp.ppterm arity);*) match n, CicReduction.whd context outsort with 0, Cic.Prod _ -> raise Nothing_to_do | 0, _ -> - let ty = Cic.MutInd (curi,tyno,ens) in + let irl = List.rev irl in + let ty = CicSubstitution.lift rightno (Cic.MutInd (curi,tyno,ens)) in let ty = if args = [] && irl = [] then ty else @@ -120,6 +121,87 @@ prerr_endline ("LEFTNO: " ^ string_of_int leftno ^ " " ^ CicPp.ppterm arity);*) (*prerr_endline (CicPp.ppterm outty ^ " <==> " ^ CicPp.ppterm outty');*) ;; +let fix_outtype t = + let module C = Cic in + let rec aux context = + function + C.Rel _ as t -> t + | C.Var (uri,exp_named_subst) -> + let exp_named_subst' = + List.map (function i,t -> i, (aux context t)) exp_named_subst in + C.Var (uri,exp_named_subst') + | C.Implicit _ + | C.Meta _ -> assert false + | C.Sort _ as t -> t + | C.Cast (v,t) -> C.Cast (aux context v, aux context t) + | C.Prod (n,s,t) -> + C.Prod (n, aux context s, aux ((Some (n, C.Decl s))::context) t) + | C.Lambda (n,s,t) -> + C.Lambda (n, aux context s, aux ((Some (n, C.Decl s))::context) t) + | C.LetIn (n,s,ty,t) -> + C.LetIn + (n, aux context s, aux context ty, + aux ((Some (n, C.Def(s,ty)))::context) t) + | C.Appl l -> C.Appl (List.map (aux context) l) + | C.Const (uri,exp_named_subst) -> + let exp_named_subst' = + List.map (function i,t -> i, (aux context t)) exp_named_subst + in + C.Const (uri,exp_named_subst') + | C.MutInd (uri,tyno,exp_named_subst) -> + let exp_named_subst' = + List.map (function i,t -> i, (aux context t)) exp_named_subst + in + C.MutInd (uri, tyno, exp_named_subst') + | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> + let exp_named_subst' = + List.map (function i,t -> i, (aux context t)) exp_named_subst + in + C.MutConstruct (uri, tyno, consno, exp_named_subst') + | C.MutCase (uri, tyno, outty, term, patterns) -> + let outty = fix_outty uri tyno term context outty in + C.MutCase (uri, tyno, aux context outty, + aux context term, List.map (aux context) patterns) + | C.Fix (funno, funs) -> + let tys,_ = + List.fold_left + (fun (types,len) (n,_,ty,_) -> + ((Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))))::types, + len+1 + ) ([],0) funs + in + C.Fix (funno, + List.map + (fun (name, indidx, ty, bo) -> + (name, indidx, aux context ty, aux (tys@context) bo) + ) funs + ) + | C.CoFix (funno, funs) -> + let tys,_ = + List.fold_left + (fun (types,len) (n,ty,_) -> + ((Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))))::types, + len+1 + ) ([],0) funs + in + C.CoFix (funno, + List.map + (fun (name, ty, bo) -> + (name, aux context ty, aux (tys@context) bo) + ) funs + ) + in + aux [] t +;; + +let get_fresh,reset_seed = + let seed = ref 0 in + (function () -> + incr seed; + string_of_int !seed), + (function () -> seed := 0) +;; + (* we are lambda-lifting also variables that do not occur *) (* ctx does not distinguish successive blocks of cofix, since there may be no * lambda separating them *) @@ -129,14 +211,14 @@ let convert_term uri t = let buri = UriManager.uri_of_string (UriManager.buri_of_uri uri^"/"^ - UriManager.name_of_uri uri ^ string_of_int (List.length ctx)^".con") + UriManager.name_of_uri uri ^ "___" ^ get_fresh () ^ ".con") in let bctx, fixpoints_tys, tys, _ = List.fold_right - (fun (name,ty,_) (ctx, fixpoints, tys, idx) -> + (fun (name,ty,_) (bctx, fixpoints, tys, idx) -> let ty, fixpoints_ty = aux octx ctx n_fix uri ty in let r = Ref.reference_of_ouri buri(Ref.CoFix idx) in - Fix (r,name,ty) :: ctx, fixpoints_ty @ fixpoints,ty::tys,idx+1) + Fix (r,name,ty) :: bctx, fixpoints_ty @ fixpoints,ty::tys,idx+1) fl ([], [], [], 0) in let bctx = bctx @ ctx in @@ -167,7 +249,7 @@ let convert_term uri t = let buri = UriManager.uri_of_string (UriManager.buri_of_uri uri^"/"^ - UriManager.name_of_uri uri ^ string_of_int (List.length ctx)^".con") + UriManager.name_of_uri uri ^ "___" ^ get_fresh () ^ ".con") in let bad_bctx, fixpoints_tys, tys, _ = List.fold_right @@ -262,7 +344,7 @@ let convert_term uri t = | (NCic.Appl l1)::l2 -> NCic.Appl (l1@l2), fixpoints | _ -> NCic.Appl l, fixpoints) | Cic.Const (curi, ens) -> - aux_ens octx ctx n_fix uri ens + aux_ens curi octx ctx n_fix uri ens (match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with | Cic.Constant (_,Some _,_,_,_) -> NCic.Const (Ref.reference_of_ouri curi Ref.Def) @@ -270,13 +352,17 @@ let convert_term uri t = NCic.Const (Ref.reference_of_ouri curi Ref.Decl) | _ -> assert false) | Cic.MutInd (curi, tyno, ens) -> - aux_ens octx ctx n_fix uri ens + aux_ens curi octx ctx n_fix uri ens (NCic.Const (Ref.reference_of_ouri curi (Ref.Ind tyno))) | Cic.MutConstruct (curi, tyno, consno, ens) -> - aux_ens octx ctx n_fix uri ens + aux_ens curi octx ctx n_fix uri ens (NCic.Const (Ref.reference_of_ouri curi (Ref.Con (tyno,consno)))) + | Cic.Var (curi, ens) -> + (match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with + Cic.Variable (_,Some bo,_,_,_) -> + aux octx ctx n_fix uri (CicSubstitution.subst_vars ens bo) + | _ -> assert false) | Cic.MutCase (curi, tyno, outty, t, branches) -> - let outty = fix_outty curi tyno t octx outty in let r = Ref.reference_of_ouri curi (Ref.Ind tyno) in let outty, fixpoints_outty = aux octx ctx n_fix uri outty in let t, fixpoints_t = aux octx ctx n_fix uri t in @@ -288,17 +374,29 @@ let convert_term uri t = branches ([],[]) in NCic.Match (r,outty,t,branches), fixpoints_outty@fixpoints_t@fixpoints - | Cic.Implicit _ | Cic.Meta _ | Cic.Var _ -> assert false - and aux_ens octx ctx n_fix uri ens he = + | Cic.Implicit _ | Cic.Meta _ -> assert false + and aux_ens curi octx ctx n_fix uri ens he = match ens with [] -> he,[] | _::_ -> + let params = + match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with + Cic.Constant (_,_,_,params,_) + | Cic.InductiveDefinition (_,params,_,_) -> params + | Cic.Variable _ + | Cic.CurrentProof _ -> assert false + in let ens,objs = List.fold_right - (fun (_,t) (l,objs) -> - let t,o = aux octx ctx n_fix uri t in - t::l, o@objs - ) ens ([],[]) + (fun luri (l,objs) -> + match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph luri) with + Cic.Variable (_,Some _,_,_,_) -> l, objs + | Cic.Variable (_,None,_,_,_) -> + let t = List.assoc luri ens in + let t,o = aux octx ctx n_fix uri t in + t::l, o@objs + | _ -> assert false + ) params ([],[]) in NCic.Appl (he::ens),objs in @@ -306,23 +404,31 @@ let convert_term uri t = ;; let cook mode vars t = - let t = CicSubstitution.lift (List.length vars) t in - snd (List.fold_right - (fun uri (n,t) -> - let t = CicSubstitution.subst_vars [uri,Cic.Rel 1] t in + let t = fix_outtype t in + let varsno = List.length vars in + let t = CicSubstitution.lift varsno t in + let rec aux n acc l = + let subst = + snd(List.fold_left (fun (i,res) uri -> i+1,(uri,Cic.Rel i)::res) (1,[]) acc) + in + match l with + [] -> CicSubstitution.subst_vars subst t + | uri::uris -> let bo,ty = match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with - Cic.Variable (_,bo,ty,_,_) -> bo,ty + Cic.Variable (_,bo,ty,_,_) -> + HExtlib.map_option fix_outtype bo, fix_outtype ty | _ -> assert false in + let ty = CicSubstitution.subst_vars subst ty in + let bo = HExtlib.map_option (CicSubstitution.subst_vars subst) bo in let id = Cic.Name (UriManager.name_of_uri uri) in - let t = + let t = aux (n-1) (uri::acc) uris in match bo,ty,mode with None,ty,`Lambda -> Cic.Lambda (id,ty,t) | None,ty,`Pi -> Cic.Prod (id,ty,t) | Some bo,ty,_ -> Cic.LetIn (id,bo,ty,t) - in - n+1,t - ) vars (1,t)) + in + aux varsno [] vars ;; let convert_obj_aux uri = function @@ -365,6 +471,7 @@ let convert_obj_aux uri = function ;; let convert_obj uri obj = + reset_seed (); let o, fixpoints = convert_obj_aux uri obj in let obj = NUri.nuri_of_ouri uri,max_int, [], [], o in fixpoints @ [obj]