From e64013e67dc485047940b77022078a2fcaad1813 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 2 Apr 2007 17:57:03 +0000
Subject: [PATCH] Procedural: some improvements

---
 .../acic_procedural/acic2Procedural.ml           | 16 +++++++++++++++-
 .../acic_procedural/proceduralHelpers.ml         |  6 +++---
 .../acic_procedural/proceduralOptimizer.ml       |  6 +++---
 3 files changed, 21 insertions(+), 7 deletions(-)

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index 7fd8290ba..08727be1c 100644
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/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/helm/software/components/acic_procedural/proceduralHelpers.ml b/helm/software/components/acic_procedural/proceduralHelpers.ml
index 39607fefd..d08dca701 100644
--- a/helm/software/components/acic_procedural/proceduralHelpers.ml
+++ b/helm/software/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/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml
index fe06207d3..67b3af940 100644
--- a/helm/software/components/acic_procedural/proceduralOptimizer.ml
+++ b/helm/software/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
-- 
2.39.2