bench/check-ce/algebraic_types_poly.mlw

   1 module M
   2
   3   use int.Int
   4   use list.List
   5   use list.Length
   6
   7   goal g: forall l: list int. length l = 0
   8
   9   type int_type = Integer int
  10
  11   (*********************************
  12    ** Non-terminating projections **
  13    *********************************)
  14    (* Warning: if definition of the following projections are present,
  15       the proof of everything below will not terminate. *)
  16   function projfl [@model_trace:.projfl] (l : list int_type) : int
  17   =
  18   match l with
  19   | Nil -> 0
  20   | Cons (Integer n) _ -> n
  21   | _ -> 0
  22   end
  23   meta "inline:no" function projfl
  24   meta "model_projection" function projfl
  25
  26   (* list int_type will be projected using projfl to int,
  27      int will be projected using projfi, projf1, and projf2
  28      Warning: does not terminate. *)
  29   let proj_test ( l [@model_projected] : list int_type) : int
  30   ensures { result > 0  }
  31   =
  32   match l with
  33   | Nil -> 1
  34   | Cons (Integer n) _ -> n
  35   | _ -> 1
  36   end
  37
  38 end