From: Ferruccio Guidi Date: Mon, 2 Apr 2007 17:57:03 +0000 (+0000) Subject: Procedural: some improvements X-Git-Tag: 0.4.95@7852~552 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1308643448fc685f58827de4c68fc98d0f701062;p=helm.git Procedural: some improvements --- diff --git a/components/acic_procedural/acic2Procedural.ml b/components/acic_procedural/acic2Procedural.ml index 7fd8290ba..08727be1c 100644 --- a/components/acic_procedural/acic2Procedural.ml +++ b/components/acic_procedural/acic2Procedural.ml @@ -159,6 +159,19 @@ with e -> failwith (msg ^ ": " ^ Printexc.to_string e) let unused_premise = "UNUSED" +let mk_exp_args hd tl classes = + let meta id = C.AImplicit (id, None) in + let map v (cl, b) = + if I.S.mem 0 cl && b then v else meta "" + in + let rec aux = function + | [] -> [] + | hd :: tl -> if hd = meta "" then aux tl else List.rev (hd :: tl) + in + let args = List.rev_map2 map tl classes in + let args = aux args in + if args = [] then hd else C.AAppl ("", hd :: args) + let convert st ?name v = match get_inner_types st v with | None -> [] @@ -180,7 +193,7 @@ let mk_intros st script = T.Intros (Some count, List.rev st.intros, "") :: script let mk_arg st = function - | C.ARel (_, _, _, name) as what -> convert st ~name what + | C.ARel (_, _, _, name) as what -> [] (* convert st ~name what *) | _ -> [] let mk_fwd_rewrite st dtext name tl direction = @@ -272,6 +285,7 @@ and proc_appl st what hd tl = [T.Elim (where, using, e, dtext ^ text); T.Branch (qs, "")] | None -> let qs = proc_bkd_proofs (next st) synth classes tl in + let hd = mk_exp_args hd tl classes in script @ [T.Apply (hd, dtext ^ text); T.Branch (qs, "")] else [T.Apply (what, dtext)] diff --git a/components/acic_procedural/proceduralHelpers.ml b/components/acic_procedural/proceduralHelpers.ml index 39607fefd..d08dca701 100644 --- a/components/acic_procedural/proceduralHelpers.ml +++ b/components/acic_procedural/proceduralHelpers.ml @@ -48,7 +48,7 @@ let split name = let join (s, i) = C.Name (if i < 0 then s else s ^ string_of_int i) -let mk_fresh_name context name = +let mk_fresh_name context (name, k) = let rec aux i = function | [] -> name, i | Some (C.Name s, _) :: entries -> @@ -56,11 +56,11 @@ let mk_fresh_name context name = if m = name && j >= i then aux (succ j) entries else aux i entries | _ :: entries -> aux i entries in - join (aux (-1) context) + join (aux k context) let mk_fresh_name context = function | C.Anonymous -> C.Anonymous - | C.Name s -> mk_fresh_name context s + | C.Name s -> mk_fresh_name context (split s) (* helper functions *********************************************************) diff --git a/components/acic_procedural/proceduralOptimizer.ml b/components/acic_procedural/proceduralOptimizer.ml index fe06207d3..67b3af940 100644 --- a/components/acic_procedural/proceduralOptimizer.ml +++ b/components/acic_procedural/proceduralOptimizer.ml @@ -126,11 +126,11 @@ and opt1_appl g es c t vs = | Some _, rv :: rvs when csno = vsno && H.is_not_atomic rv -> let x = C.Appl (t :: List.rev rvs @ [define rv]) in HLog.warn "Optimizer: anticipate 3"; opt1_proof g true c x - | Some _, _ -> + | _ (* Some _, _ *) -> g (C.Appl (t :: vs)) - | None, _ -> +(* | None, _ -> aux false [] (vs, classes) - in +*) in let rec aux h prev = function | C.LetIn (name, vv, tt) :: vs -> let t = S.lift 1 t in