From 1c4d219404055f521ecf48528d7b9853d7a03499 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 8 Mar 2007 15:31:02 +0000 Subject: [PATCH] some improvements --- components/acic_procedural/acic2Procedural.ml | 27 +++++++++---------- .../acic_procedural/proceduralPreprocess.ml | 15 ++++++----- 2 files changed, 20 insertions(+), 22 deletions(-) diff --git a/components/acic_procedural/acic2Procedural.ml b/components/acic_procedural/acic2Procedural.ml index e91c4bdfc..9a5662a1d 100644 --- a/components/acic_procedural/acic2Procedural.ml +++ b/components/acic_procedural/acic2Procedural.ml @@ -218,8 +218,8 @@ let rec mk_atomic st dtext what = let script = convert st ~name what in script @ mk_fwd_proof st dtext name what, T.mk_arel 0 name -and mk_fwd_rewrite st dtext name tl direction = -try +and mk_fwd_rewrite st dtext name tl direction = + assert (List.length tl = 6); 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 @@ -228,7 +228,13 @@ try 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_rewrite st dtext script t what qs tl direction = + assert (List.length tl = 5); + let rps, predicate = [List.nth tl 4], List.nth tl 2 in + let e = Cn.mk_pattern rps predicate in + List.rev script @ convert st t @ + [T.Rewrite (direction, what, None, e, dtext); T.Branch (qs, "")] and mk_fwd_proof st dtext name = function | C.ALetIn (_, n, v, t) -> @@ -265,9 +271,7 @@ and mk_fwd_proof st dtext name = function | _ -> [T.LetIn (name, v, dtext)] -and mk_proof st t = -try - match t with +and mk_proof st = function | C.ALambda (_, name, v, t) -> let entry = Some (name, C.Decl (cic v)) in let intro = get_intro name t in @@ -310,15 +314,9 @@ try let synth = I.S.add 1 synth in let qs = mk_bkd_proofs (next st) synth classes tl in if is_rewrite_right hd then - let rps, predicate = [List.nth tl 4], List.nth tl 2 in - let e = Cn.mk_pattern rps predicate in - List.rev script @ convert st t @ - [T.Rewrite (false, what, None, e, dtext); T.Branch (qs, "")] + mk_rewrite st dtext script t what qs tl false else if is_rewrite_left hd then - let rps, predicate = [List.nth tl 4], List.nth tl 2 in - let e = Cn.mk_pattern rps predicate in - List.rev script @ convert st t @ - [T.Rewrite (true, what, None, e, dtext); T.Branch (qs, "")] + mk_rewrite st dtext script t what qs tl true else let using = Some hd in List.rev script @ convert st t @ @@ -346,7 +344,6 @@ try 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 4862db759..8030c403b 100644 --- a/components/acic_procedural/proceduralPreprocess.ml +++ b/components/acic_procedural/proceduralPreprocess.ml @@ -99,7 +99,7 @@ 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 + if true then pp_proof g ht es c t else find g ht t 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 @@ -107,7 +107,7 @@ and pp_lambda g ht es c name v t = let g t _ decurry = 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 + if true then pp_proof g ht es (entry :: c) t else find g ht t and pp_letin g ht es c name v t = let entry = Some (name, C.Def (v, None)) in @@ -119,11 +119,12 @@ 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 es then pp_term g ht es c v else find g ht v + if true then pp_term g ht es c v else find g ht v in - if es then pp_proof g ht es (entry :: c) t else find g ht t + if true then pp_proof g ht es (entry :: c) t else find g ht t and pp_appl_one g ht es c t v = let g t _ decurry = @@ -147,9 +148,9 @@ and pp_appl_one g ht es c t v = 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 + if true then pp_term g ht es c v else find g ht v in - if es then pp_proof g ht es c t else find g ht t + if true then pp_proof g ht es c t else find g ht t and pp_appl g ht es c t = function | [] -> pp_proof g ht es c t @@ -159,7 +160,7 @@ and pp_appl g ht es c t = function pp_proof g ht es c x and pp_proof g ht es c t = - let g t proof decurry = add g ht 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 -- 2.39.2