add_list.mlw 1.83 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30

theory SumList

use export int.Int
use export real.RealInfix
use export list.List

type or_integer_float = Integer int | Real real


(* sum integers in a list *)
function add_int (e: list or_integer_float) : int =
  match e with
  | Nil -> 0
  | Cons (Integer n) t -> n + add_int t
  | Cons _ t -> add_int t
  end

(* sum reals in a list *)
function add_real (e: list or_integer_float) : real =
  match e with
  | Nil -> 0.0
  | Cons (Real x) t -> x +. add_real t
  | Cons _ t -> add_real t
  end

end

module AddListRec

31
use SumList
32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59

let rec sum (l: list or_integer_float) : (int, real) =
  { true }
  match l with
  | Nil -> (0, 0.0)
  | Cons h t ->
      let (a,b) = sum t in
      match h with
      | Integer n -> (n + a,b)
      | Real x -> (a,x +. b)
      end
  end
  { let (si, sf) = result in si = add_int l /\ sf = add_real l }

let main () =
  let l =
    Cons (Integer 5) (Cons (Real 3.3) (Cons (Integer 8)
      (Cons (Real 1.4) (Cons (Integer 9) Nil))))
  in
  let (s,f) = sum l in
  assert { s = 22 };
  assert { f = 4.7 }

end


module AddListImp

60 61
use SumList
use module ref.Ref
62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99

exception Break

let sum (l: list or_integer_float) : (int, real) =
  { true }
  let si = ref 0 in
  let sf = ref 0.0 in
  let ll = ref l in
  try
    while True do
    invariant { !si + add_int !ll = add_int l /\
                !sf +. add_real !ll = add_real l
              }
     match !ll with
     | Nil -> raise Break
     | Cons (Integer n) t ->
         si := !si + n; ll := t
     | Cons (Real x) t ->
         sf := !sf +. x; ll := t
     end
   done;
   absurd
  with Break -> (!si, !sf)
  end
  { let (si, sf) = result in si = add_int l /\ sf = add_real l }


let main () =
  let l =
    Cons (Integer 5) (Cons (Real 3.3) (Cons (Integer 8)
      (Cons (Real 1.4) (Cons (Integer 9) Nil))))
  in
  let (s,f) = sum l in
  assert { s = 22 };
  assert { f = 4.7 }

end