add_list.mlw 1.75 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
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

30
use SumList
31

32
let rec sum (l: list or_integer_float) : (si: int, sf: real) =
33
    variant { l }
34
    ensures { si = add_int l /\ sf = add_real l }
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 41
      | Integer n -> n + a, b
      | Real x -> a, x +. b
42 43 44 45 46 47 48 49
      end
  end

let main () =
  let l =
    Cons (Integer 5) (Cons (Real 3.3) (Cons (Integer 8)
      (Cons (Real 1.4) (Cons (Integer 9) Nil))))
  in
50
  let s,f = sum l in
51 52 53 54 55 56 57 58
  assert { s = 22 };
  assert { f = 4.7 }

end


module AddListImp

59 60
use SumList
use ref.Ref
61

62 63
let sum (l: list or_integer_float) : (si: int, sf: real) =
    ensures { si = add_int l /\ sf = add_real l }
64 65 66
  let si = ref 0 in
  let sf = ref 0.0 in
  let ll = ref l in
67
  while True do
68
    invariant { !si + add_int !ll = add_int l /\
69
                !sf +. add_real !ll = add_real l }
70
    variant { !ll }
71
     match !ll with
72
     | Nil -> return !si, !sf
73 74 75 76 77
     | Cons (Integer n) t ->
         si := !si + n; ll := t
     | Cons (Real x) t ->
         sf := !sf +. x; ll := t
     end
78 79
  done;
  absurd
80 81 82 83 84 85 86


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

end