From d906171bfb30327a9b3bc3c73c3380908f8c6f57 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 7 Mar 2007 15:49:41 +0000 Subject: [PATCH] Procedural: bug fix --- components/acic_procedural/acic2Procedural.ml | 11 +++-- .../acic_procedural/proceduralPreprocess.ml | 41 +++++++++++-------- 2 files changed, 32 insertions(+), 20 deletions(-) diff --git a/components/acic_procedural/acic2Procedural.ml b/components/acic_procedural/acic2Procedural.ml index 28fa98947..e91c4bdfc 100644 --- a/components/acic_procedural/acic2Procedural.ml +++ b/components/acic_procedural/acic2Procedural.ml @@ -219,6 +219,7 @@ let rec mk_atomic st dtext what = script @ mk_fwd_proof st dtext name what, T.mk_arel 0 name and mk_fwd_rewrite st dtext name tl direction = +try let what, where = List.nth tl 5, List.nth tl 3 in let rps, predicate = [List.nth tl 4], List.nth tl 2 in let e = Cn.mk_pattern rps predicate in @@ -227,6 +228,7 @@ and mk_fwd_rewrite st dtext name tl direction = let script, what = mk_atomic st dtext what in T.Rewrite (direction, what, Some (premise, name), e, dtext) :: script | _ -> assert false +with e -> failwith ("mk_fwd_rewrite: " ^ Printexc.to_string e) and mk_fwd_proof st dtext name = function | C.ALetIn (_, n, v, t) -> @@ -248,12 +250,12 @@ and mk_fwd_proof st dtext name = function let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in [T.LetIn (name, v, dtext ^ text)] end - | C.AMutCase (id, uri, tyno, outty, arg, cases) as v -> +(* | C.AMutCase (id, uri, tyno, outty, arg, cases) as v -> begin match Cn.mk_ind st.context id uri tyno outty arg cases with | None -> [T.LetIn (name, v, dtext)] | Some v -> mk_fwd_proof st dtext name v end - | C.ACast (_, v, _) -> +*) | C.ACast (_, v, _) -> mk_fwd_proof st dtext name v | v -> match get_inner_types st v with @@ -263,7 +265,9 @@ and mk_fwd_proof st dtext name = function | _ -> [T.LetIn (name, v, dtext)] -and mk_proof st = function +and mk_proof st t = +try + match t with | C.ALambda (_, name, v, t) -> let entry = Some (name, C.Decl (cic v)) in let intro = get_intro name t in @@ -342,6 +346,7 @@ and mk_proof st = function let text = Printf.sprintf "%s: %s" "UNEXPANDED" (string_of_head t) in let script = [T.Note text] in mk_intros st script +with e -> failwith ("mk_proof: " ^ Printexc.to_string e) and mk_bkd_proofs st synth classes ts = try diff --git a/components/acic_procedural/proceduralPreprocess.ml b/components/acic_procedural/proceduralPreprocess.ml index d31d0113b..4862db759 100644 --- a/components/acic_procedural/proceduralPreprocess.ml +++ b/components/acic_procedural/proceduralPreprocess.ml @@ -26,7 +26,7 @@ module C = Cic module Un = CicUniv module S = CicSubstitution -module R = CicReduction +module Rd = CicReduction module TC = CicTypeChecker module DTI = DoubleTypeInference module HEL = HExtlib @@ -41,7 +41,7 @@ let get_type c t = let ty, _ = TC.type_of_aux' [] c t Un.empty_ugraph in ty let is_proof c t = - match (get_type c (get_type c t)) with + match Rd.whd ~delta:true c (get_type c (get_type c t)) with | C.Sort C.Prop -> true | _ -> false @@ -59,7 +59,7 @@ let split c t = let rec aux whd a n c = function | C.Prod (s, v, t) -> aux false (v :: a) (succ n) (add s v c) t | v when whd -> v :: a, n - | v -> aux true a n c (R.whd ~delta:true c v) + | v -> aux true a n c (Rd.whd ~delta:true c v) in aux false [] 0 c t @@ -78,19 +78,25 @@ let expanded_premise = "EXPANDED" let defined_premise = "DEFINED" -let eta_expand n t = - let ty = C.Implicit None in +let eta_expand tys t = + let n = List.length tys in let name i = Printf.sprintf "%s%u" expanded_premise i in - let lambda i t = C.Lambda (C.Name (name i), ty, t) 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 rec aux i f a = - if i >= n then f, a else aux (succ i) (comp f (lambda i)) (arg i n :: a) + let rec aux i f a = function + | [] -> f, a + | ty :: tl -> aux (succ i) (comp f (lambda i ty)) (arg i n :: a) tl in - let absts, args = aux 0 identity [] in + let absts, args = aux 0 identity [] tys in absts (C.Appl (S.lift n t :: args)) -let eta_fix t proof decurry = - if proof && decurry > 0 then eta_expand decurry t else t +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 eta_fix c t proof decurry = + if proof && decurry > 0 then eta_expand (get_tys c decurry t) t else t let rec pp_cast g ht es c t v = if es then pp_proof g ht es c t else find g ht t @@ -99,7 +105,7 @@ and pp_lambda g ht es c name v t = let name = if DTI.does_not_occur 1 t then C.Anonymous else name in let entry = Some (name, C.Decl v) in let g t _ decurry = - let t = eta_fix t true decurry in + let t = eta_fix (entry :: c) t true decurry in g (C.Lambda (name, v, t)) true 0 in if es then pp_proof g ht es (entry :: c) t else find g ht t @@ -112,7 +118,7 @@ and pp_letin g ht es c name v t = let x = C.LetIn (mame, w, C.LetIn (name, u, S.lift_from 2 1 t)) in pp_proof g ht false c x | v -> - let v = eta_fix v proof d in + let v = eta_fix c v proof d in g (C.LetIn (name, v, t)) true decurry in if es then pp_term g ht es c v else find g ht v @@ -130,7 +136,7 @@ and pp_appl_one g ht es c t v = let x = C.LetIn (mame, w, C.Appl [u; S.lift 1 v]) in pp_proof g ht false c x | C.Appl ts, v when decurry > 0 -> - let v = eta_fix v proof d in + let v = eta_fix c v proof d in g (C.Appl (List.append ts [v])) true (pred decurry) | t, v when is_not_atomic t -> let mame = C.Name defined_premise in @@ -138,7 +144,7 @@ and pp_appl_one g ht es c t v = pp_proof g ht false c x | t, v -> let _, premsno = split c (get_type c t) in - let v = eta_fix v proof d in + let v = eta_fix c v proof d in g (C.Appl [t; v]) true (pred premsno) in if es then pp_term g ht es c v else find g ht v @@ -169,9 +175,10 @@ and pp_term g ht es c t = let pp_obj = function | C.Constant (name, Some bo, ty, pars, attrs) -> let g bo proof decurry = - let bo = eta_fix bo proof decurry in + let bo = eta_fix [] bo proof decurry in C.Constant (name, Some bo, ty, pars, attrs) in let ht = C.CicHash.create 1 in - pp_term g ht true [] bo + begin try pp_term g ht true [] bo + with e -> failwith ("PPP: " ^ Printexc.to_string e) end | obj -> obj -- 2.39.2