tests/add_list.mlw

   1
   2 theory SumList
   3
   4 use export int.Int
   5 use export real.RealInfix
   6 use export list.List
   7
   8 type or_integer_float = Integer int | Real real
   9
  10
  11 (* sum integers in a list *)
  12 function add_int (e: list or_integer_float) : int =
  13   match e with
  14   | Nil -> 0
  15   | Cons (Integer n) t -> n + add_int t
  16   | Cons _ t -> add_int t
  17   end
  18
  19 (* sum reals in a list *)
  20 function add_real (e: list or_integer_float) : real =
  21   match e with
  22   | Nil -> 0.0
  23   | Cons (Real x) t -> x +. add_real t
  24   | Cons _ t -> add_real t
  25   end
  26
  27 end
  28
  29 module AddListRec
  30
  31 use SumList
  32
  33 let rec sum (l: list or_integer_float) : (int, real) =
  34   { true }
  35   match l with
  36   | Nil -> (0, 0.0)
  37   | Cons h t ->
  38       let (a,b) = sum t in
  39       match h with
  40       | Integer n -> (n + a,b)
  41       | Real x -> (a,x +. b)
  42       end
  43   end
  44   { let (si, sf) = result in si = add_int l /\ sf = add_real l }
  45
  46 let main () =
  47   let l =
  48     Cons (Integer 5) (Cons (Real 3.3) (Cons (Integer 8)
  49       (Cons (Real 1.4) (Cons (Integer 9) Nil))))
  50   in
  51   let (s,f) = sum l in
  52   assert { s = 22 };
  53   assert { f = 4.7 }
  54
  55 end
  56
  57
  58 module AddListImp
  59
  60 use SumList
  61 use module ref.Ref
  62
  63 exception Break
  64
  65 let sum (l: list or_integer_float) : (int, real) =
  66   { true }
  67   let si = ref 0 in
  68   let sf = ref 0.0 in
  69   let ll = ref l in
  70   try
  71     while True do
  72     invariant { !si + add_int !ll = add_int l /\
  73                 !sf +. add_real !ll = add_real l
  74               }
  75      match !ll with
  76      | Nil -> raise Break
  77      | Cons (Integer n) t ->
  78          si := !si + n; ll := t
  79      | Cons (Real x) t ->
  80          sf := !sf +. x; ll := t
  81      end
  82    done;
  83    absurd
  84   with Break -> (!si, !sf)
  85   end
  86   { let (si, sf) = result in si = add_int l /\ sf = add_real l }
  87
  88
  89 let main () =
  90   let l =
  91     Cons (Integer 5) (Cons (Real 3.3) (Cons (Integer 8)
  92       (Cons (Real 1.4) (Cons (Integer 9) Nil))))
  93   in
  94   let (s,f) = sum l in
  95   assert { s = 22 };
  96   assert { f = 4.7 }
  97
  98 end
  99