Procedural: some improvements

[helm.git] / components / acic_procedural / acic2Procedural.ml

diff --git a/components/acic_procedural/acic2Procedural.ml b/components/acic_procedural/acic2Procedural.ml
index 7fd8290ba224783c9856a4cb84a1e2576749c90e..08727be1cfde78d6c773dcc76177ff679351dbcd 100644 (file)
--- 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)]