Procedural: clear tactics added

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

diff --git a/components/acic_procedural/proceduralConversion.ml b/components/acic_procedural/proceduralConversion.ml
index 68b47341c05caff79f8972eb645c16c8fef30d73..b8cdc08ea1b3af2a0288ef6239f3718ad4aed5ea 100644 (file)
--- a/components/acic_procedural/proceduralConversion.ml
+++ b/components/acic_procedural/proceduralConversion.ml
@@ -145,44 +145,48 @@ let mk_pattern psno predicate =
    let body = generalize psno predicate in
    clear_absts 0 psno body
 
-let get_clears c p xet = 
+let get_clears c p xtypes = 
    let meta = C.Implicit None in
-   let rec aux c names p et = function
+   let rec aux c names p it et = function
       | []                                                -> 
          List.rev c, List.rev names         
       | Some (C.Name name as n, C.Decl v) as hd :: tl     ->
          let hd, names, v = 
-           if DTI.does_not_occur 1 p && DTI.does_not_occur 1 et then 
+           if DTI.does_not_occur 1 p && DTI.does_not_occur 1 it && DTI.does_not_occur 1 et then 
               Some (C.Anonymous, C.Decl v), name :: names, meta 
            else 
               hd, names, v
         in
         let p = C.Lambda (n, v, p) in
+        let it = C.Prod (n, v, it) in
         let et = C.Prod (n, v, et) in
-        aux (hd :: c) names p et tl
+        aux (hd :: c) names p it et tl
       | Some (C.Name name as n, C.Def (v, x)) as hd :: tl ->
          let hd, names, v = 
-           if DTI.does_not_occur 1 p && DTI.does_not_occur 1 et then 
+           if DTI.does_not_occur 1 p && DTI.does_not_occur 1 it && DTI.does_not_occur 1 et then 
               Some (C.Anonymous, C.Def (v, x)), name :: names, meta
            else 
               hd, names, v
         in
         let p = C.LetIn (n, v, p) in
+        let it = C.LetIn (n, v, it) in
         let et = C.LetIn (n, v, et) in
-        aux (hd :: c) names p et tl
+        aux (hd :: c) names p it et tl
       | Some (C.Anonymous as n, C.Decl v) as hd :: tl     ->
         let p = C.Lambda (n, meta, p) in
+        let it = C.Lambda (n, meta, it) in
         let et = C.Lambda (n, meta, et) in
-        aux (hd :: c) names p et tl
+        aux (hd :: c) names p it et tl
       | Some (C.Anonymous as n, C.Def (v, _)) as hd :: tl ->
         let p = C.LetIn (n, meta, p) in
+        let it = C.LetIn (n, meta, it) in
         let et = C.LetIn (n, meta, et) in
-        aux (hd :: c) names p et tl
+        aux (hd :: c) names p it et tl
       | None :: tl                                        -> assert false
    in
-   match xet with 
-      | Some et -> aux [] [] p et c
-      | None    -> c, []
+   match xtypes with 
+      | Some (it, et) -> aux [] [] p it et c
+      | None          -> c, []
 
 let clear c hyp =
    let rec aux c = function

diff --git a/components/acic_procedural/proceduralConversion.mli b/components/acic_procedural/proceduralConversion.mli
index f41f8e56c3f2d425d1e93b313de237d5cb9818c0..e5b2dcdcf9859e7f0ad2f23473053cce786fb205 100644 (file)
--- a/components/acic_procedural/proceduralConversion.mli
+++ b/components/acic_procedural/proceduralConversion.mli
@@ -32,6 +32,7 @@ val lift: int -> int -> Cic.annterm -> Cic.annterm
 val mk_pattern: int -> Cic.annterm -> Cic.annterm
 
 val get_clears: 
-   Cic.context -> Cic.term -> Cic.term option -> Cic.context * string list
+   Cic.context -> Cic.term -> (Cic.term * Cic.term) option -> 
+   Cic.context * string list
 
 val clear: Cic.context -> string -> Cic.context