
(* This file contains exemples of what kind of types the new inference
 * algorithm can (successfully) deal with.
 *)

(* Some easy examples *)

(* Infered improved in abstractions and introduced in products *)
Check (x:?) x = O.
Check [x] x==True.
Check (x:?) x = [y](S (S y)).

(* Non-dependent type is preferred *)
Check [x](x O)=true.
(* [x:(n:nat) Cases n of O => bool | _ => nat end](x O)=true
 * would be correct as well, but less probable!
 *)


Require PolyList.

(* Inference cannot be done properly for really polymorphic terms *)
Check [A:Set; x:A; l](In x l).
(* [x,l](In x l) does not work since the type of the elements of the list
 * is not constrained. [A,x,l](In x l) is obviously no better.
 *)


(* In Realizers *)
Parameter A : Set; P : A->Prop; P_dec : (x:?) {(P x)} + {~(P x)}. 
Goal (l:?) { x:? | (In x l) & (P x) } + { (x:?)~(P x) }.
Realizer Fix srch{
  srch [l:?]: ? :=
    Cases l of
      nil => (inright ?)
    | (cons x m) => if (P_dec x) then (inleft ? x) else (srch m)
    end}.
Abort.


(* Inference of the inductive type from the patterns *)

Check [n]Cases n of O => true | _ => false end.

(* The warning is because the type of b might depend on a. It is only when
 * the constrained to lists of booleans that we are sure that it indeed
 * does not depend on a.
 *)
Check [a,b]Cases a b of
        O nil => true
      | _ (cons x _) => x
      | _ _ => false
      end.

(* Deep patterns *)
Check [l]Cases l of
   nil => true
 | (cons true l) => false
 | (cons false l) => true
 end.


(* Inductive type with parameters. Arguments cannot be infered *)
Check [p:(le ? (S (S O)))]Cases p of
           le_n => I
         | (le_S m q) => ([_]I (q::(le O m)))
         end.
