Procedural: clear tactics added

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

diff --git a/components/acic_procedural/acic2Procedural.ml b/components/acic_procedural/acic2Procedural.ml
index 95c4c1a9a7825182daf0dcab6313c2eef0d707b9..18e1ecc5b3826b5a287bf3cd13f14c6fc443993a 100644 (file)
--- a/components/acic_procedural/acic2Procedural.ml
+++ b/components/acic_procedural/acic2Procedural.ml
@@ -43,6 +43,7 @@ module DTI  = DoubleTypeInference
 module Cl   = ProceduralClassify
 module T    = ProceduralTypes
 module Cn   = ProceduralConversion
+module H    = ProceduralHelpers
 
 type status = {
    sorts : (C.id, A.sort_kind) Hashtbl.t;
@@ -178,6 +179,8 @@ with Invalid_argument _ -> failwith "A2P.get_ind_names"
 
 (* proof construction *******************************************************)
 
+let used_premise = C.Name "USED"
+
 let mk_exp_args hd tl classes synth =
    let meta id = C.AImplicit (id, None) in
    let map v (cl, b) =
@@ -250,12 +253,16 @@ let mk_rewrite st dtext what qs tl direction =
 
 let rec proc_lambda st name v t =
    let dno = DTI.does_not_occur 1 (cic t) in
-   let dno = dno && match get_inner_types st v with
+   let dno = dno && match get_inner_types st t with
       | None          -> true
       | Some (it, et) -> 
          DTI.does_not_occur 1 (cic it) && DTI.does_not_occur 1 (cic et)
    in
-   let name = if dno then C.Anonymous else name in  
+   let name = match dno, name with
+      | true, _            -> C.Anonymous
+      | false, C.Anonymous -> H.mk_fresh_name st.context used_premise 
+      | false, name        -> name
+   in
    let entry = Some (name, C.Decl (cic v)) in
    let intro = get_intro name in
    proc_proof (add st entry intro) t
@@ -350,12 +357,14 @@ and proc_other st what =
 
 and proc_proof st t = 
    let f st =
-      let xet = match get_inner_types st t with
-         | Some (_, et) -> Some (cic et)
-         | None         -> None
+      let xtypes, note = match get_inner_types st t with
+         | Some (it, et) -> Some (cic it, cic et), 
+         (Printf.sprintf "\nInferred: %s\nExpected: %s"
+         (Pp.ppterm (cic it)) (Pp.ppterm (cic et))) 
+         | None          -> None, "\nNo types"
       in
-      let context, clears = Cn.get_clears st.context (cic t) xet in
-      let note = Pp.ppcontext st.context in
+      let context, clears = Cn.get_clears st.context (cic t) xtypes in
+      let note = Pp.ppcontext st.context ^ note in
       {st with context = context; clears = clears; clears_note = note}
    in
    match t with