From fa68418f83c513562debf8b25eec7ea3bb28996d Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 27 Feb 2007 19:20:48 +0000 Subject: [PATCH] some improvements --- components/acic_procedural/acic2Procedural.ml | 61 +++++-------------- .../acic_procedural/proceduralConversion.ml | 6 -- .../acic_procedural/proceduralConversion.mli | 2 - components/acic_procedural/proceduralTypes.ml | 7 --- .../acic_procedural/proceduralTypes.mli | 1 - 5 files changed, 15 insertions(+), 62 deletions(-) diff --git a/components/acic_procedural/acic2Procedural.ml b/components/acic_procedural/acic2Procedural.ml index cf8159b0c..8dd8e02aa 100644 --- a/components/acic_procedural/acic2Procedural.ml +++ b/components/acic_procedural/acic2Procedural.ml @@ -49,8 +49,7 @@ type status = { max_depth: int option; depth: int; context: C.context; - intros: string list; - ety: C.annterm option + intros: string list } (* helpers ******************************************************************) @@ -87,15 +86,11 @@ let string_of_head = function | C.AMeta _ -> "meta" | C.AImplicit _ -> "implict" -let clear st = {st with intros = []; ety = None} +let clear st = {st with intros = []} let next st = {(clear st) with depth = succ st.depth} -let set_ety st ety = - if st.ety = None then {st with ety = ety} else st - -let add st entry intro ety = - let st = set_ety st ety in +let add st entry intro = {st with context = entry :: st.context; intros = intro :: st.intros} let test_depth st = @@ -164,8 +159,6 @@ let unused_premise = "UNUSED" let defined_premise = "DEFINED" -let assumed_premise = "ASSUMED" - let expanded_premise = "EXPANDED" let convert st ?name v = @@ -183,7 +176,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 i) in + let arg i n = T.mk_arel (n - 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 @@ -210,11 +203,7 @@ let mk_intros st script = try if st.intros = [] then script else let count = List.length st.intros in - let p0 = T.Whd (count, "") in - let p1 = T.Intros (Some count, List.rev st.intros, "") in - match st.ety with - | Some ety when Cn.need_whd count ety -> p0 :: p1 :: script - | _ -> p1 :: script + T.Intros (Some count, List.rev st.intros, "") :: script with Invalid_argument _ -> failwith "A2P.mk_intros" let rec mk_atomic st dtext what = @@ -229,27 +218,12 @@ let rec mk_atomic st dtext what = and mk_fwd_rewrite st dtext name tl direction = let what, where = List.nth tl 5, List.nth tl 3 in - let rewrite premise = - let script, what = mk_atomic st dtext what in - T.Rewrite (direction, what, Some (premise, name), dtext) :: script - in match where with - | C.ARel (_, _, _, binder) -> rewrite binder - | _ -> assert false - -(* - assert (get_inner_sort st where = `Prop); - let pred, old = List.nth tl 2, List.nth tl 1 in - let pred_name = defined_premise in - let pred_text = "extracted" in - let p1 = T.LetIn (pred_name, pred, pred_text) in - let cut_name = assumed_premise in - let cut_type = C.AAppl ("", [T.mk_arel 0 pred_name; old]) in - let cut_text = "" in - let p2 = T.Cut (cut_name, cut_type, cut_text) in - let qs = [rewrite cut_name; mk_proof (next st) where] in - [T.Branch (qs, ""); p2; p1] -*) + | C.ARel (_, _, _, premise) -> + let script, what = mk_atomic st dtext what in + T.Rewrite (direction, what, Some (premise, name), dtext) :: script + | _ -> assert false + 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 @@ -273,20 +247,16 @@ and mk_fwd_proof st dtext name = function [T.LetIn (name, v, dtext)] and mk_proof st = function - | C.ALambda (_, name, v, t) as what -> + | C.ALambda (_, name, v, t) -> let entry = Some (name, C.Decl (cic v)) in let intro = get_intro name t in - let ety = match get_inner_types st what with - | Some (_, ety) -> Some ety - | None -> None - in - mk_proof (add st entry intro ety) t + mk_proof (add st entry intro) t | C.ALetIn (_, name, v, t) as what -> let proceed, dtext = test_depth st in let script = if proceed then let entry = Some (name, C.Def (cic v, None)) in let intro = get_intro name t in - let q = mk_proof (next (add st entry intro None)) t in + let q = mk_proof (next (add st entry intro)) t in List.rev_append (mk_fwd_proof st dtext intro v) q else [T.Apply (what, dtext)] @@ -369,7 +339,7 @@ let is_theorem pars = let mk_obj st = function | C.AConstant (_, _, s, Some v, t, [], pars) when is_theorem pars -> - let ast = mk_proof (set_ety st (Some t)) v in + let ast = mk_proof st v in let count = T.count_steps 0 ast in let text = Printf.sprintf "tactics: %u" count in T.Theorem (s, t, text) :: ast @ [T.Qed ""] @@ -386,8 +356,7 @@ let acic2procedural ~ids_to_inner_sorts ~ids_to_inner_types ?depth prefix aobj = max_depth = depth; depth = 0; context = []; - intros = []; - ety = None + intros = [] } in HLog.debug "Level 2 transformation"; let steps = mk_obj st aobj in diff --git a/components/acic_procedural/proceduralConversion.ml b/components/acic_procedural/proceduralConversion.ml index 4e43164cb..b3ce56070 100644 --- a/components/acic_procedural/proceduralConversion.ml +++ b/components/acic_procedural/proceduralConversion.ml @@ -65,12 +65,6 @@ let rec list_sub start length = function (* proof construction *******************************************************) -let rec need_whd i = function - | C.ACast (_, t, _) -> need_whd i t - | C.AProd (_, _, _, t) when i > 0 -> need_whd (pred i) t - | _ when i > 0 -> true - | _ -> false - let lift k n = let rec lift_xns k (uri, t) = uri, lift_term k t and lift_ms k = function diff --git a/components/acic_procedural/proceduralConversion.mli b/components/acic_procedural/proceduralConversion.mli index fef3ad07b..f27d73aab 100644 --- a/components/acic_procedural/proceduralConversion.mli +++ b/components/acic_procedural/proceduralConversion.mli @@ -23,8 +23,6 @@ * http://cs.unibo.it/helm/. *) -val need_whd: int -> Cic.annterm -> bool - val lift: int -> int -> Cic.annterm -> Cic.annterm val mk_ind: diff --git a/components/acic_procedural/proceduralTypes.ml b/components/acic_procedural/proceduralTypes.ml index b81a7c3de..6aa769b03 100644 --- a/components/acic_procedural/proceduralTypes.ml +++ b/components/acic_procedural/proceduralTypes.ml @@ -87,7 +87,6 @@ type step = Note of note | Rewrite of how * what * where * note | Elim of what * using option * note | Apply of what * note - | Whd of count * note | Change of inferred * what * where * note | ClearBody of name * note | Branch of step list list * note @@ -147,11 +146,6 @@ let mk_apply t = let tactic = G.Apply (floc, t) in mk_tactic tactic -let mk_whd i = - let pattern = None, [], Some hole in - let tactic = G.Reduce (floc, `Whd, pattern) in - mk_tactic tactic - let mk_change t where = let pattern = match where with | None -> None, [], Some hole @@ -187,7 +181,6 @@ let rec render_step sep a = function | Rewrite (b, t, w, s) -> mk_note s :: cont sep (mk_rewrite b t w :: a) | Elim (t, xu, s) -> mk_note s :: cont sep (mk_elim t xu :: a) | Apply (t, s) -> mk_note s :: cont sep (mk_apply t :: a) - | Whd (c, s) -> mk_note s :: cont sep (mk_whd c :: a) | Change (t, _, w, s) -> mk_note s :: cont sep (mk_change t w :: a) | ClearBody (n, s) -> mk_note s :: cont sep (mk_clearbody n :: a) | Branch ([], s) -> a diff --git a/components/acic_procedural/proceduralTypes.mli b/components/acic_procedural/proceduralTypes.mli index f26c19d87..980bc1bc1 100644 --- a/components/acic_procedural/proceduralTypes.mli +++ b/components/acic_procedural/proceduralTypes.mli @@ -54,7 +54,6 @@ type step = Note of note | Rewrite of how * what * where * note | Elim of what * using option * note | Apply of what * note - | Whd of count * note | Change of inferred * what * where * note | ClearBody of name * note | Branch of step list list * note -- 2.39.2