From b7535cd20248c564e942cc4e9058d34fbb062c6f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 19 Feb 2008 15:38:00 +0000 Subject: [PATCH] transformation almost finisced, not tested --- helm/software/components/ng_kernel/nCic.ml | 3 +- .../components/ng_kernel/nCicEnvironment.ml | 2 +- .../components/ng_kernel/oCic2NCic.ml | 211 +++++++++++++++--- .../components/ng_kernel/oCic2NCic.mli | 2 +- .../components/ng_kernel/oCicTypeChecker.ml | 2 +- 5 files changed, 186 insertions(+), 34 deletions(-) diff --git a/helm/software/components/ng_kernel/nCic.ml b/helm/software/components/ng_kernel/nCic.ml index 08726422e..4fd950af0 100644 --- a/helm/software/components/ng_kernel/nCic.ml +++ b/helm/software/components/ng_kernel/nCic.ml @@ -108,8 +108,9 @@ type i_attr = generated * ind_pragma type obj_kind = | Constant of relevance * string * term option * term * c_attr | Fixpoint of bool * inductiveFun list * f_attr + (* true -> fix, funcs, arrts *) | Inductive of bool * int * inductiveType list * i_attr - (* (co)inductive, leftno, types *) + (* true -> inductive, leftno, types *) (* the int must be 0 if the object has no body *) type obj = NUri.uri * int * metasenv * substitution * obj_kind diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml index e10aba973..8d0ae1a4f 100644 --- a/helm/software/components/ng_kernel/nCicEnvironment.ml +++ b/helm/software/components/ng_kernel/nCicEnvironment.ml @@ -7,7 +7,7 @@ let get_checked_obj u = let o,_ = CicEnvironment.get_cooked_obj ~trust:false CicUniv.oblivion_ugraph ouri in - let no = OCic2NCic.convert_obj ouri o in + let no,_ = OCic2NCic.convert_obj ouri o in NUri.UriHash.add cache u no; no ;; diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml index b46345268..407f705e2 100644 --- a/helm/software/components/ng_kernel/oCic2NCic.ml +++ b/helm/software/components/ng_kernel/oCic2NCic.ml @@ -5,38 +5,185 @@ let cn_to_s = function | Cic.Name s -> s ;; -let rec convert_fix_definition acc = function - | Cic.Lambda (n,s,t) -> - convert_fix_definition ((n,s)::acc) t - | Cic.Fix (_, [name,rno,ty,bo]) -> - let acc = List.map (fun (n,s) -> cn_to_s n, convert_term s) acc in - let ty = convert_term ty in - let bo = convert_term bo in - Some (true,[[],name,rno, - List.fold_right (fun (n,s) acc -> NCic.Prod(n,s,acc)) acc ty, - List.fold_right (fun (n,s) acc -> NCic.Lambda(n,s,acc)) acc bo]) - | Cic.CoFix (_, [name,ty,bo]) -> - let acc = List.map (fun (n,s) -> cn_to_s n, convert_term s) acc in - let ty = convert_term ty in - let bo = convert_term bo in - Some (false,[[],name,0, - List.fold_right (fun (n,s) acc -> NCic.Prod(n,s,acc)) acc ty, - List.fold_right (fun (n,s) acc -> NCic.Lambda(n,s,acc)) acc bo]) - | _ -> None +type ctx = Ce of NCic.hypothesis | Fix of int * int + +let splat mk_pi ctx t = + List.fold_left + (fun t c -> + match c with + | Ce (name, NCic.Def (bo,ty)) -> NCic.LetIn (name, ty, bo, t) + | Ce (name, NCic.Decl ty) when mk_pi -> NCic.Prod (name, ty, t) + | Ce (name, NCic.Decl ty) -> NCic.Lambda (name, ty, t) + | Fix _ -> t) + t ctx +;; + +let splat_args ctx t = + let n_args = + List.length (List.filter (function Ce _ -> true | _ -> false) ctx) + in + if n_args = 0 then t + else + let rec aux = function + | 0 -> [] + | n -> aux (n-1) @ [NCic.Rel n] + in + NCic.Appl (t:: aux n_args) ;; -let convert_obj_aux = function +let convert_term uri t = + let rec aux octx (ctx : ctx list) n_fix uri = function + | Cic.CoFix (k, fl) -> + let idx = ref ~-1 in + let bctx = + List.map (fun (_,_,_) -> + incr idx; Fix (~-1,!idx)) fl @ ctx + in + let buri = + UriManager.uri_of_string + (UriManager.string_of_uri uri^string_of_int (List.length ctx)^".con") + in + let n_fl = List.length fl in + let boctx,_ = + List.fold_left + (fun (types,len) (n,ty,_) -> + (Some (Cic.Name n,(Cic.Decl (CicSubstitution.lift len ty)))::types, + len+1)) (octx,0) fl + in + let fl, fixpoints = + List.fold_right + (fun (name,ty,bo) (l,fixpoints) -> + let ty, fixpoints_ty = aux octx ctx n_fix uri ty in + let bo, fixpoints_bo = aux boctx bctx (n_fix + n_fl) buri bo in + (([],name,~-1,splat true ctx ty, splat false ctx bo)::l), + fixpoints_ty @ fixpoints_bo @ fixpoints) + fl ([],[]) + in + let obj = + NUri.nuri_of_ouri uri,0,[],[], + NCic.Fixpoint (false, fl, (`Generated, `Definition)) + in + NCic.Const (NReference.reference_of_ouri uri (NReference.CoFix (k))), + obj::fixpoints + | Cic.Fix (k, fl) -> + let idx = ref ~-1 in + let rno = ref 0 in + let bctx = + List.map (fun (_,recno,_,_) -> + incr idx; if !idx = k then rno := recno;Fix (recno,!idx)) fl @ ctx + in + let buri = + UriManager.uri_of_string + (UriManager.string_of_uri uri^string_of_int (List.length ctx)^".con") + in + let n_fl = List.length fl in + let boctx,_ = + List.fold_left + (fun (types,len) (n,_,ty,_) -> + (Some (Cic.Name n,(Cic.Decl (CicSubstitution.lift len ty)))::types, + len+1)) (octx,0) fl + in + let fl, fixpoints = + List.fold_right + (fun (name,rno,ty,bo) (l,fixpoints) -> + let ty, fixpoints_ty = aux octx ctx n_fix uri ty in + let bo, fixpoints_bo = aux boctx bctx (n_fix + n_fl) buri bo in + (([],name,rno,splat true ctx ty, splat false ctx bo)::l), + fixpoints_ty @ fixpoints_bo @ fixpoints) + fl ([],[]) + in + let obj = + NUri.nuri_of_ouri uri,0,[],[], + NCic.Fixpoint (true, fl, (`Generated, `Definition)) + in + NCic.Const (NReference.reference_of_ouri uri (NReference.Fix (k,!rno))), + obj::fixpoints + | Cic.Rel n -> + (match List.nth ctx n with + | Ce _ -> NCic.Rel (n-n_fix), [] + | Fix (recno, fixno) -> + splat_args ctx + (NCic.Const + (NReference.reference_of_ouri uri (NReference.Fix (fixno,recno)))), + []) + | Cic.Lambda (name, (s as old_s), t) -> + let s, fixpoints_s = aux octx ctx n_fix uri s in + let ctx = Ce (cn_to_s name, NCic.Decl s) :: ctx in + let octx = Some (name, Cic.Decl old_s) :: octx in + let t, fixpoints_t = aux octx ctx n_fix uri t in + NCic.Lambda (cn_to_s name, s, t), fixpoints_s @ fixpoints_t + | Cic.Prod (name, (s as old_s), t) -> + let s, fixpoints_s = aux octx ctx n_fix uri s in + let ctx = Ce (cn_to_s name, NCic.Decl s) :: ctx in + let octx = Some (name, Cic.Decl old_s) :: octx in + let t, fixpoints_t = aux octx ctx n_fix uri t in + NCic.Prod (cn_to_s name, s, t), fixpoints_s @ fixpoints_t + | Cic.LetIn (name, (s as old_s), t) -> + let s, fixpoints_s = aux octx ctx n_fix uri s in + let old_ty,_ = + CicTypeChecker.type_of_aux' [] octx old_s CicUniv.oblivion_ugraph + in + let ty, fixpoints_ty = aux octx ctx n_fix uri old_ty in + let ctx = Ce (cn_to_s name, NCic.Def (s, ty)) :: ctx in + let octx = Some (name, Cic.Def (old_s, Some old_ty)) :: octx in + let t, fixpoints_t = aux octx ctx n_fix uri t in + NCic.LetIn (cn_to_s name, ty, s, t), + fixpoints_s @ fixpoints_t @ fixpoints_ty + | Cic.Cast (t,ty) -> + let t, fixpoints_t = aux octx ctx n_fix uri t in + let ty, fixpoints_ty = aux octx ctx n_fix uri ty in + NCic.LetIn ("cast", ty, t, NCic.Rel 1), fixpoints_t @ fixpoints_ty + | Cic.Sort Cic.Prop -> NCic.Sort NCic.Prop,[] + | Cic.Sort Cic.Set -> NCic.Sort NCic.Set,[] + | Cic.Sort Cic.CProp -> NCic.Sort NCic.CProp,[] + | Cic.Sort (Cic.Type _) -> NCic.Sort (NCic.Type 0),[] + (* calculate depth in the univ_graph*) + | Cic.Appl l -> + let l, fixpoints = + List.fold_right + (fun t (l,acc) -> + let t, fixpoints = aux octx ctx n_fix uri t in + (t::l,fixpoints@acc)) + l ([],[]) + in + NCic.Appl l, fixpoints + | Cic.Const (curi, _) -> + NCic.Const (NReference.reference_of_ouri curi NReference.Def),[] + | Cic.MutInd (curi, tyno, _) -> + NCic.Const (NReference.reference_of_ouri curi (NReference.Ind tyno)),[] + | Cic.MutConstruct (curi, tyno, consno, _) -> + NCic.Const (NReference.reference_of_ouri curi + (NReference.Con (tyno,consno))),[] + | Cic.MutCase (curi, tyno, oty, t, branches) -> + let r = NReference.reference_of_ouri curi (NReference.Ind tyno) in + let oty, fixpoints_oty = aux octx ctx n_fix uri oty in + let t, fixpoints_t = aux octx ctx n_fix uri t in + let branches, fixpoints = + List.fold_right + (fun t (l,acc) -> + let t, fixpoints = aux octx ctx n_fix uri t in + (t::l,fixpoints@acc)) + branches ([],[]) + in + NCic.Match (r,oty,t,branches), fixpoints_oty @ fixpoints_t @ fixpoints + | Cic.Implicit _ | Cic.Meta _ | Cic.Var _ -> assert false + in + aux [] [] 0 uri t +;; + +let convert_obj_aux uri = function | Cic.Constant (name, None, ty, _, _) -> - NCic.Constant ([], name, None, convert_term ty, - (`Provided,`Theorem,`Regular)) + let nty, fixpoints = convert_term uri ty in + assert(fixpoints = []); + NCic.Constant ([], name, None, nty, (`Provided,`Theorem,`Regular)), + fixpoints | Cic.Constant (name, Some bo, ty, _, _) -> - (match convert_fix_definition [] bo with - | None -> - NCic.Constant ([], name, Some (convert_term bo), convert_term ty, - (`Provided,`Theorem,`Regular)) - | Some (recursive, ifl) -> - NCic.Fixpoint (recursive, ifl, (`Provided, `Definition))) - | Cic.InductiveDefinition (itl,_,leftno,_) -> + let nbo, fixpoints_bo = convert_term uri bo in + let nty, fixpoints_ty = convert_term uri ty in + assert(fixpoints_ty = []); + NCic.Constant ([], name, Some nbo, nty, (`Provided,`Theorem,`Regular)), + fixpoints_bo @ fixpoints_ty + | Cic.InductiveDefinition (_,_,_,_) -> assert false (* let ind = let _,x,_,_ = List.hd itl in x in let itl = List.map @@ -45,9 +192,13 @@ let convert_obj_aux = function List.map (fun name, ty -> [], name, convert_term ty) cl) itl in - NCic.Inductive (ind, leftno, itl, (`Provided, `Regular)) + NCic.Inductive (ind, leftno, itl, (`Provided, `Regular)) *) | Cic.Variable _ | Cic.CurrentProof _ -> assert false ;; -let convert_obj uri obj = NUri.nuri_of_ouri uri,0, [], [], convert_obj_aux obj;; +let convert_obj uri obj = + let o, fixpoints = convert_obj_aux uri obj in + let obj = NUri.nuri_of_ouri uri,0, [], [], o in + obj, fixpoints +;; diff --git a/helm/software/components/ng_kernel/oCic2NCic.mli b/helm/software/components/ng_kernel/oCic2NCic.mli index bc58762a7..3930caea2 100644 --- a/helm/software/components/ng_kernel/oCic2NCic.mli +++ b/helm/software/components/ng_kernel/oCic2NCic.mli @@ -1 +1 @@ -val convert_obj: UriManager.uri -> Cic.obj -> NCic.obj +val convert_obj: UriManager.uri -> Cic.obj -> NCic.obj * NCic.obj list diff --git a/helm/software/components/ng_kernel/oCicTypeChecker.ml b/helm/software/components/ng_kernel/oCicTypeChecker.ml index 2139654c7..878706b9e 100644 --- a/helm/software/components/ng_kernel/oCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/oCicTypeChecker.ml @@ -1,7 +1,7 @@ let typecheck_obj uri obj = try - NCicTypeChecker.typecheck_obj (OCic2NCic.convert_obj uri obj); true + NCicTypeChecker.typecheck_obj (fst (OCic2NCic.convert_obj uri obj)); true with | NCicTypeChecker.TypeCheckerFailure _ | NCicTypeChecker.AssertFailure _ -> false -- 2.39.2