auto look for the type of vwit to reduce the nb of case (fixme #30)

lib/int_proofs.pml

@@ -1,49 +1,31 @@
 include lib.int
 
-// FIXME #30: auto fails because two cases are impossible by typing
-// because p is positive below.
 val suc_pre : ∀n∈int, suc (pre n) ≡ n = fun n {
-  case n {
-    Zero → {}
-    S[p] → ncase⟨p⟩
-    P[_] → {}
-  }
+  set auto 2 1; {}
 }
+
 val pre_suc : ∀n∈int, pre (suc n) ≡ n = fun n {
-  case n {
-    Zero → {}
-    S[_] → {}
-    P[p] → pcase⟨p⟩
-  }
+  set auto 2 1; {}
 }
 
 val rec add_zero_right : ∀n∈int, n + Zero ≡ n = fun n {
   case n {
     Zero → {}
     S[p] → eqns p + Zero ≡ p by add_zero_right p;
            showing suc(p+Zero) ≡ S[p];
-           case p { //FIXME #30 too
-             Zero → {}
-             S[_] → {}
-           }
+           set auto 1 0; {}
     P[s] → eqns s + Zero ≡ s by add_zero_right s;
            showing pre(s+Zero) ≡ P[s];
+           set auto 1 0; {}
            //showing suc(s+Zero) ≡ S[s]; // FIXME #24: wrong but loops,
               //probably a cyclic value in the pool!
-           case s { //FIXME #30 too
-             Zero → {}
-             P[_] → {}
-           }
   }
 }
 
 val rec add_S_right : ∀n∈ int, ∀m∈pos, n + S[m] ≡ suc(n + m) = fun n m {
   case n {
     Zero → showing S[m] ≡ suc(m);
-           case m { //FIXME #30 too
-             Zero → {}
-             S[_] → {}
-           }
+           set auto 1 0; {}
     S[p] → eqns p + S[m] ≡ suc(p + m) by add_S_right p m;
            showing p + S[m] ≡ suc(p + m);
            {}
@@ -56,10 +38,7 @@ val rec add_S_right : ∀n∈ int, ∀m∈pos, n + S[m] ≡ suc(n + m) = fun n m
 val rec add_P_right : ∀n∈ int, ∀m∈neg, n + P[m] ≡ pre(n + m) = fun n m {
   case n {
     Zero → showing P[m] ≡ pre(m);
-           case m { //FIXME #30 too
-             Zero → {}
-             P[_] → {}
-           }
+           set auto 1 0; {}
     S[p] → eqns p + P[m] ≡ pre(p + m) by add_P_right p m;
            showing suc(pre(p + m)) ≡ pre(suc(p + m));
            use pre_suc (p + m); use suc_pre(p + m)

src/kernel/equiv.ml

@@ -1962,6 +1962,38 @@ let test_value : Ptr.t -> pool -> bool = fun p po ->
     | Ptr.V_ptr(v) -> fst (is_nobox p po)
     | Ptr.T_ptr(_) -> false
 
+let log_aut = Log.register 'a' (Some "aut") "automatic proving informations"
+let log_aut = Log.(log_aut.p)
+
+(** Try to get the list of cases from the type in a VWit to limit
+    the cases in auto *)
+let get_cases : Ptr.v_ptr -> pool -> A.key list option = fun pv po ->
+  let is_vwit = function VN_VWit _ -> true | _ -> false in
+  log_aut "get cases %a" Ptr.print (Ptr.V_ptr pv);
+  let l = List.find_all (fun (v',nn) ->
+              eq_ptr po (Ptr.V_ptr v') (Ptr.V_ptr pv)
+              && is_vwit nn) po.vs in
+  let rec gn = function
+    | []                   -> None
+    | (_, VN_VWit(e)) :: l ->
+       let (_,a,_) = !(e.valu) in
+       log_aut "get cases foud vwit : %a" Print.ex a;
+       let rec fn a =
+         match (Norm.whnf a).elt with
+         | HDef(_,d) -> fn d.expr_def
+         | DSum(s)   -> Some(A.keys s)
+         | FixM(_,b) -> fn (bndr_subst b (Dumm P))
+         | FixN(_,b) -> fn (bndr_subst b (Dumm P))
+         | Memb(_,a) -> fn a
+         | Rest(a,_) -> fn a
+         | Impl(_,a) -> fn a
+         | Univ(s,b) -> fn (bndr_subst b (Dumm s))
+         | Exis(s,b) -> fn (bndr_subst b (Dumm s))
+         | _         -> gn l
+       in
+       fn a
+    | _ -> assert false
+  in gn l
 
 (** get one original term from the pool or their applications. *)
 let get_orig : Ptr.t -> pool -> term =
@@ -2046,6 +2078,10 @@ let get_blocked : pool -> blocked list = fun po ->
              end
           | TN_Case(v,b) ->
              let cases = List.map fst (A.bindings b) in
+             let cases = match get_cases v po with
+               | Some l -> List.filter (fun x -> List.mem x l) cases
+               | None   -> cases
+             in
              let e = get_orig (Ptr.V_ptr v) po in
              let b = BCas (e, cases) in
              if List.exists (eq_blocked b) acc then acc else

src/kernel/typing.ml

@@ -59,9 +59,6 @@ let log_sub = Log.(log_sub.p)
 let log_typ = Log.register 't' (Some "typ") "typing informations"
 let log_typ = Log.(log_typ.p)
 
-let log_aut = Log.register 'a' (Some "aut") "automatic proving informations"
-let log_aut = Log.(log_aut.p)
-
 type auto_ctxt =
   { level : int * int
   ; doing : bool

src/util/assoc.ml

@@ -15,6 +15,8 @@ module ListMap =
     let map  f l = List.map (fun (k, v) -> (k, f v)) l
     let mapi f l = List.map (fun (k, v) -> (k, f k v)) l
 
+    let keys l = List.map fst l
+
     let bindings l = l
 
     let sort f l = List.sort (fun (_, d1) (_, d2) -> f d1 d2) l

src/util/assoc.mli

@@ -20,6 +20,8 @@ val map : ('a -> 'b) -> 'a t -> 'b t
 
 val mapi : (string -> 'a -> 'b) -> 'a t -> 'b t
 
+val keys : 'a t -> key list
+
 val bindings : 'a t -> (string * 'a) list
 
 val sort : ('a -> 'a -> int) -> 'a t -> 'a t