From c0a733b932a64804f67ac93f9ab9f52bd0614fc6 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 9 Mar 2007 22:53:49 +0000 Subject: [PATCH] Procedural: 2 bug fix in eta expansion + 1 bug fix in pattern generation --- .../acic_procedural/acic2Procedural.ml | 19 ++++-- .../acic_procedural/proceduralConversion.ml | 15 +++-- .../acic_procedural/proceduralPreprocess.ml | 59 ++++++++++++++----- 3 files changed, 66 insertions(+), 27 deletions(-) diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml index 9a5662a1d..e3545f62a 100644 --- a/helm/software/components/acic_procedural/acic2Procedural.ml +++ b/helm/software/components/acic_procedural/acic2Procedural.ml @@ -154,6 +154,12 @@ try with Not_found -> `Type (CicUniv.fresh()) with Invalid_argument _ -> failwith "A2P.get_sort" +let get_type msg st bo = +try + let ty, _ = TC.type_of_aux' [] st.context (cic bo) Un.empty_ugraph in + ty +with e -> failwith (msg ^ ": " ^ Printexc.to_string e) + (* proof construction *******************************************************) let unused_premise = "UNUSED" @@ -178,7 +184,7 @@ let eta_expand n t = let ty = C.AImplicit ("", None) in let name i = Printf.sprintf "%s%u" expanded_premise i in let lambda i t = C.ALambda (id, C.Name (name i), ty, t) in - let arg i n = T.mk_arel (n - i) (name (n - i - 1)) in + let arg i n = T.mk_arel ((* n - *) succ i) (name (n - i - 1)) in let rec aux i f a = if i >= n then f, a else aux (succ i) (comp f (lambda i)) (arg i n :: a) in @@ -246,7 +252,7 @@ and mk_fwd_proof st dtext name = function | C.AAppl (_, hd :: tl) as v -> if is_fwd_rewrite_right hd tl then mk_fwd_rewrite st dtext name tl true else if is_fwd_rewrite_left hd tl then mk_fwd_rewrite st dtext name tl false else - let ty, _ = TC.type_of_aux' [] st.context (cic hd) Un.empty_ugraph in + let ty = get_type "TC1" st hd in begin match get_inner_types st v with | Some (ity, _) when M.bkd st.context ty -> let qs = [[T.Id ""]; mk_proof (next st) v] in @@ -299,11 +305,14 @@ and mk_proof st = function | C.AAppl (_, hd :: tl) as t -> let proceed, dtext = test_depth st in let script = if proceed then - let ty, _ = TC.type_of_aux' [] st.context (cic hd) Un.empty_ugraph in + let ty = get_type "TC2" st hd in let (classes, rc) as h = Cl.classify st.context ty in let premises, _ = P.split st.context ty in let decurry = List.length classes - List.length tl in - if decurry < 0 then mk_proof (clear st) (appl_expand decurry t) else + if decurry <> 0 then + Printf.eprintf "DECURRY: %u %s\n" decurry (CicPp.ppterm (cic t)); + assert (decurry = 0); + if decurry < 0 then mk_proof (clear st) (appl_expand decurry t) else if decurry > 0 then mk_proof (clear st) (eta_expand decurry t) else let synth = I.S.singleton 0 in let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in @@ -330,7 +339,7 @@ and mk_proof st = function [T.Apply (t, dtext)] in mk_intros st script - | C.AMutCase (id, uri, tyno, outty, arg, cases) -> + | C.AMutCase (id, uri, tyno, outty, arg, cases) as t -> begin match Cn.mk_ind st.context id uri tyno outty arg cases with | _ (* None *) -> let text = Printf.sprintf "%s" "UNEXPANDED: mutcase" in diff --git a/helm/software/components/acic_procedural/proceduralConversion.ml b/helm/software/components/acic_procedural/proceduralConversion.ml index 3df6802ff..d2d305ed4 100644 --- a/helm/software/components/acic_procedural/proceduralConversion.ml +++ b/helm/software/components/acic_procedural/proceduralConversion.ml @@ -29,6 +29,7 @@ module Un = CicUniv module TC = CicTypeChecker module D = Deannotate module UM = UriManager +module Rd = CicReduction module P = ProceduralPreprocess module T = ProceduralTypes @@ -63,7 +64,6 @@ let rec list_sub start length = function | hd :: tl when length > 0 -> hd :: list_sub start (pred length) tl | _ -> [] - (* proof construction *******************************************************) let lift k n = @@ -140,12 +140,15 @@ let fake_annotate c = let clear_absts m = let rec aux k n = function + | C.AImplicit (_, None) as t -> t | C.ALambda (id, s, v, t) when k > 0 -> C.ALambda (id, s, v, aux (pred k) n t) - | C.ALambda (_, _, _, t) when n > 0 -> + | C.ALambda (_, _, _, t) when n > 0 -> aux 0 (pred n) (lift 1 (-1) t) - | t when n > 0 -> assert false - | t -> t + | t when n > 0 -> + Printf.eprintf "CLEAR: %u %s\n" n (CicPp.ppterm (cic t)); + assert false + | t -> t in aux m @@ -158,7 +161,7 @@ try in let lpsno, (_, _, _, constructors) = get_ind_type uri tyno in let inty, _ = TC.type_of_aux' [] context (cic arg) Un.empty_ugraph in - let ps = match inty with + let ps = match Rd.whd ~delta:true context inty with | C.MutInd _ -> [] | C.Appl (C.MutInd _ :: args) -> List.map (fake_annotate context) args | _ -> assert false @@ -212,7 +215,7 @@ let generalize n = | C.AMutConstruct (id, _, _, _, _) | C.AMeta (id, _, _) -> meta id | C.ARel (id, _, m, _) -> - if m = succ (n - k) then hole id else meta id + if m = succ (k - n) then hole id else meta id | C.AAppl (id, ts) -> let ts = List.map (gen_term k) ts in if is_meta ts then meta id else C.AAppl (id, ts) diff --git a/helm/software/components/acic_procedural/proceduralPreprocess.ml b/helm/software/components/acic_procedural/proceduralPreprocess.ml index 8030c403b..6b2b2cc90 100644 --- a/helm/software/components/acic_procedural/proceduralPreprocess.ml +++ b/helm/software/components/acic_procedural/proceduralPreprocess.ml @@ -43,7 +43,8 @@ let get_type c t = let is_proof c t = match Rd.whd ~delta:true c (get_type c (get_type c t)) with | C.Sort C.Prop -> true - | _ -> false + | C.Sort _ -> false + | _ -> assert false let is_not_atomic = function | C.Sort _ @@ -78,25 +79,43 @@ let expanded_premise = "EXPANDED" let defined_premise = "DEFINED" -let eta_expand tys t = - let n = List.length tys in +let eta_expand g tys t = + assert (tys <> []); let name i = Printf.sprintf "%s%u" expanded_premise i in let lambda i ty t = C.Lambda (C.Name (name i), ty, t) in - let arg i n = C.Rel (n - i) in + let arg i = C.Rel (succ i) in let rec aux i f a = function | [] -> f, a - | ty :: tl -> aux (succ i) (comp f (lambda i ty)) (arg i n :: a) tl + | ty :: tl -> aux (succ i) (comp f (lambda i ty)) (arg i :: a) tl in + let n = List.length tys in let absts, args = aux 0 identity [] tys in - absts (C.Appl (S.lift n t :: args)) - -let get_tys c decurry t = - let tys, _ = split c (get_type c t) in - let tys, _ = HEL.split_nth decurry (List.tl tys) in - List.rev tys + let t = match S.lift n t with + | C.Appl ts -> C.Appl (ts @ args) + | t -> C.Appl (t :: args) + in + g (absts t) + +let get_tys c decurry = + let rec aux n = function +(* | C.Appl (hd :: tl) -> aux (n + List.length tl) hd *) + | t -> + let tys, _ = split c (get_type c t) in + let _, tys = HEL.split_nth n (List.rev tys) in + let tys, _ = HEL.split_nth decurry tys in + tys + in + aux 0 let eta_fix c t proof decurry = - if proof && decurry > 0 then eta_expand (get_tys c decurry t) t else t + let rec aux g c = function + | C.LetIn (name, v, t) -> + let g t = g (C.LetIn (name, v, t)) in + let entry = Some (name, C.Def (v, None)) in + aux g (entry :: c) t + | t -> eta_expand g (get_tys c decurry t) t + in + if proof && decurry > 0 then aux identity c t else t let rec pp_cast g ht es c t v = if true then pp_proof g ht es c t else find g ht t @@ -119,7 +138,6 @@ and pp_letin g ht es c name v t = pp_proof g ht false c x | v -> let v = eta_fix c v proof d in -(* let t = eta_fix (entry :: c) t true decurry in *) g (C.LetIn (name, v, t)) true decurry in if true then pp_term g ht es c v else find g ht v @@ -144,9 +162,8 @@ and pp_appl_one g ht es c t v = let x = C.LetIn (mame, t, C.Appl [C.Rel 1; S.lift 1 v]) in pp_proof g ht false c x | t, v -> - let _, premsno = split c (get_type c t) in let v = eta_fix c v proof d in - g (C.Appl [t; v]) true (pred premsno) + g (C.Appl [t; v]) true (pred decurry) in if true then pp_term g ht es c v else find g ht v in @@ -159,14 +176,23 @@ and pp_appl g ht es c t = function let x = C.Appl (C.Appl [t; v1] :: v2 :: vs) in pp_proof g ht es c x +and pp_atomic g ht es c t = + let _, premsno = split c (get_type c t) in + g t true premsno + and pp_proof g ht es c t = + Printf.eprintf "IN: |- %s\n" (*CicPp.ppcontext c*) (CicPp.ppterm t); + let g t proof decurry = + Printf.eprintf "OUT: %b %u |- %s\n" proof decurry (CicPp.ppterm t); + g t proof decurry + in (* let g t proof decurry = add g ht t proof decurry in *) match t with | C.Cast (t, v) -> pp_cast g ht es c t v | C.Lambda (name, v, t) -> pp_lambda g ht es c name v t | C.LetIn (name, v, t) -> pp_letin g ht es c name v t | C.Appl (t :: vs) -> pp_appl g ht es c t vs - | t -> g t true 0 + | t -> pp_atomic g ht es c t and pp_term g ht es c t = if is_proof c t then pp_proof g ht es c t else g t false 0 @@ -180,6 +206,7 @@ let pp_obj = function C.Constant (name, Some bo, ty, pars, attrs) in let ht = C.CicHash.create 1 in + Printf.eprintf "BEGIN: %s\n" name; begin try pp_term g ht true [] bo with e -> failwith ("PPP: " ^ Printexc.to_string e) end | obj -> obj -- 2.39.2