From d7fd52648af0f0d0dc8ca53c5582281531973243 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 7 Apr 2008 23:16:36 +0000 Subject: [PATCH] Tentative (and bad!) fix of outtypes in non-dependent eliminations. The fix does not work since there is no guarantee in Coq that the outtype is made of a sequence of Lambdas (and indeed it is not for automatically generated elimiantion principles). Thus I need to perform recursion on the type of the outtype and I also need to perform some eta-expansion to insert the additional lambda in the right position :-( --- .../components/ng_kernel/oCic2NCic.ml | 54 +++++++++++++++++-- 1 file changed, 51 insertions(+), 3 deletions(-) diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml index d758c2ca6..af9642e3f 100644 --- a/helm/software/components/ng_kernel/oCic2NCic.ml +++ b/helm/software/components/ng_kernel/oCic2NCic.ml @@ -61,6 +61,53 @@ let splat_args ctx t n_fix = NCic.Appl (t:: aux (List.length ctx)) ;; +let fix_outty curi tyno t context outty = + let leftno,rightno = + match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with + Cic.InductiveDefinition (tyl,_,leftno,_) -> + let _,_,arity,_ = List.nth tyl tyno in + let rec count_prods leftno context arity = + match leftno, CicReduction.whd context arity with + 0, Cic.Sort _ -> 0 + | 0, Cic.Prod (name,so,ty) -> + 1 + count_prods 0 (Some (name, Cic.Decl so)::context) ty + | n, Cic.Prod (name,so,ty) -> + count_prods (leftno - 1) (Some (name, Cic.Decl so)::context) ty + | _,_ -> assert false + in +(*prerr_endline (UriManager.string_of_uri curi); +prerr_endline ("LEFTNO: " ^ string_of_int leftno ^ " " ^ CicPp.ppterm arity);*) + leftno, count_prods leftno [] arity + | _ -> assert false in + let ens,args = + match fst (CicTypeChecker.type_of_aux' [] context t CicUniv.oblivion_ugraph) + with + Cic.MutInd (_,_,ens) -> ens,[] + | Cic.Appl (Cic.MutInd (_,_,ens)::args) -> + ens,fst (HExtlib.split_nth leftno args) + | _ -> assert false + in + let rec aux n irl context outty = + match n, CicReduction.whd context outty with + 0, (Cic.Lambda _ as t) -> t + | 0, t -> + let ty = Cic.MutInd (curi,tyno,ens) in + let args = args @ irl in + let ty = if args = [] then ty else Cic.Appl (ty::args) in + Cic.Lambda (Cic.Anonymous, ty, CicSubstitution.lift 1 t) + | n, Cic.Lambda (name,so,ty) -> + let ty' = + aux (n - 1) (Cic.Rel n::irl) (Some (name, Cic.Decl so)::context) ty + in + Cic.Lambda (name,so,ty') + | _,_ -> assert false + in +(*prerr_endline ("RIGHTNO = " ^ string_of_int rightno ^ " OUTTY = " ^ CicPp.ppterm outty);*) + let outty' = aux rightno [] context outty in +(*prerr_endline (CicPp.ppterm outty ^ " <==> " ^ CicPp.ppterm outty');*) + if outty' = outty then outty else outty' +;; + (* 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 *) @@ -216,9 +263,10 @@ let convert_term uri t = | Cic.MutConstruct (curi, tyno, consno, ens) -> aux_ens octx ctx n_fix uri ens (NCic.Const (Ref.reference_of_ouri curi (Ref.Con (tyno,consno)))) - | Cic.MutCase (curi, tyno, oty, t, branches) -> + | 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 oty, fixpoints_oty = aux octx ctx n_fix uri oty 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 let branches, fixpoints = List.fold_right @@ -227,7 +275,7 @@ let convert_term uri t = (t::l,fixpoints@acc)) branches ([],[]) in - NCic.Match (r,oty,t,branches), fixpoints_oty @ fixpoints_t @ fixpoints + 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 = match ens with -- 2.39.2