procedural: bug fixes

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

diff --git a/components/acic_procedural/acic2Procedural.ml b/components/acic_procedural/acic2Procedural.ml
index bff721a3e7b5a247e9bca1e0f442b9202ee31a53..c9423268ccb9d144cb1c536ee5cd258307d780b4 100644 (file)
--- a/components/acic_procedural/acic2Procedural.ml
+++ b/components/acic_procedural/acic2Procedural.ml
@@ -35,8 +35,9 @@ module HObj = HelmLibraryObjects
 module A    = Cic2acic
 module Ut   = CicUtil
 module E    = CicEnvironment
-module PEH  = ProofEngineHelpers
 module Pp   = CicPp
+module PEH  = ProofEngineHelpers
+module HEL  = HExtlib
 
 module Cl   = ProceduralClassify
 module T    = ProceduralTypes
@@ -59,8 +60,8 @@ let cic = D.deannotate_term
 let split2_last l1 l2 =
 try
    let n = pred (List.length l1) in
-   let before1, after1 = T.list_split n l1 in
-   let before2, after2 = T.list_split n l2 in
+   let before1, after1 = HEL.split_nth n l1 in
+   let before2, after2 = HEL.split_nth n l2 in
    before1, before2, List.hd after1, List.hd after2
 with Invalid_argument _ -> failwith "A2P.split2_last"
 
@@ -167,16 +168,16 @@ let get_entry st id =
 
 let unused_premise = "UNUSED"
 
-let mk_exp_args hd tl classes =
+let mk_exp_args hd tl classes synth =
    let meta id = C.AImplicit (id, None) in
    let map v (cl, b) =
-      if I.S.mem 0 cl && b then v else meta ""
+      if I.overlaps synth 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 = T.list_rev_map2 map tl classes in
    let args = aux args in
    if args = [] then hd else C.AAppl ("", hd :: args)
 
@@ -247,7 +248,7 @@ and proc_letin st what name v t =
               | C.AAppl (_, hd :: tl) when is_fwd_rewrite_left hd tl  ->
                  mk_fwd_rewrite st dtext intro tl false
               | v                                                     ->
-                 let qs = [[T.Id ""]; proc_proof (next st) v] in
+                 let qs = [proc_proof (next st) v; [T.Id ""]] in
                  [T.Branch (qs, ""); T.Cut (intro, ity, dtext)]
            in
            C.Decl (cic ity), rqv
@@ -278,11 +279,19 @@ and proc_appl st what hd tl =
    let script = if proceed then
       let ty = get_type "TC2" st hd in
       let (classes, rc) as h = Cl.classify st.context ty in
+      let goal_arity = match get_inner_types st what with
+         | None          -> 0
+        | Some (ity, _) -> snd (PEH.split_with_whd (st.context, cic ity))
+      in
       let argsno = List.length classes in
-      let diff = argsno - List.length tl in
-      if diff <> 0 then failwith (Printf.sprintf "NOT TOTAL: %i %s |--- %s" diff (Pp.ppcontext st.context) (Pp.ppterm (cic hd)));
-      let synth = I.S.singleton 0 in
-      let text = Printf.sprintf "%u %s" argsno (Cl.to_string h) in
+      let decurry = argsno - List.length tl in
+      let diff = goal_arity - decurry in
+      if diff < 0 then failwith (Printf.sprintf "NOT TOTAL: %i %s |--- %s" diff (Pp.ppcontext st.context) (Pp.ppterm (cic hd)));
+      let rec mk_synth a n =
+         if n < 0 then a else mk_synth (I.S.add n a) (pred n)
+      in
+      let synth = mk_synth I.S.empty decurry in
+      let text = "" (* Printf.sprintf "%u %s" argsno (Cl.to_string h) *) in
       let script = List.rev (mk_arg st hd) @ convert st what in
       match rc with
          | Some (i, j) ->
@@ -302,7 +311,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
+           let hd = mk_exp_args hd tl classes synth in
            script @ [T.Apply (hd, dtext ^ text); T.Branch (qs, "")]
    else
       [T.Apply (what, dtext)]
@@ -314,7 +323,6 @@ and proc_other st what =
    let script = [T.Note text] in
    mk_intros st script
 
-
 and proc_proof st = function
    | C.ALambda (_, name, w, t)        -> proc_lambda st name w t
    | C.ALetIn (_, name, v, t) as what -> proc_letin st what name v t
@@ -330,9 +338,9 @@ try
       if I.overlaps synth inv then None else
       if I.S.is_empty inv then Some (proc_proof st v) else
       Some [T.Apply (v, dtext ^ "dependent")]
-   in
-   T.list_map2_filter aux classes ts
-with Invalid_argument _ -> failwith "A2P.proc_bkd_proofs"
+   in  
+   List.rev (T.list_map2_filter aux classes ts)
+with Invalid_argument s -> failwith ("A2P.proc_bkd_proofs: " ^ s)
 
 (* object costruction *******************************************************)