Procedural: some improvements

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index 7fd8290ba224783c9856a4cb84a1e2576749c90e..08727be1cfde78d6c773dcc76177ff679351dbcd 100644 (file)
--- 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 39607fefd7186fa04552131f59fda270d84f408e..d08dca7013501224c797916efc26ccbfdef3f1ea 100644 (file)
--- 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 fe06207d38b9c99dfdb3e2a7424c63b79e2dae35..67b3af94091650d924b0269fe2af8d1f04c077c7 100644 (file)
--- 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