examples/add_list.mlw

   1 theory SumList
   2
   3 use export int.Int
   4 use export real.RealInfix
   5 use export list.List
   6
   7 type or_integer_float = Integer int | Real real
   8
   9
  10 (* sum integers in a list *)
  11 function add_int (e: list or_integer_float) : int =
  12   match e with
  13   | Nil -> 0
  14   | Cons (Integer n) t -> n + add_int t
  15   | Cons _ t -> add_int t
  16   end
  17
  18 (* sum reals in a list *)
  19 function add_real (e: list or_integer_float) : real =
  20   match e with
  21   | Nil -> 0.0
  22   | Cons (Real x) t -> x +. add_real t
  23   | Cons _ t -> add_real t
  24   end
  25
  26 end
  27
  28 module AddListRec
  29
  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       | Integer n -> n + a, b
  41       | Real x -> a, x +. b
  42       end
  43   end
  44
  45 let main () =
  46   let l =
  47     Cons (Integer 5) (Cons (Real 3.3) (Cons (Integer 8)
  48       (Cons (Real 1.4) (Cons (Integer 9) Nil))))
  49   in
  50   let s,f = sum l in
  51   assert { s = 22 };
  52   assert { f = 4.7 }
  53
  54 end
  55
  56
  57 module AddListImp
  58
  59 use SumList
  60 use ref.Ref
  61
  62 let sum (l: list or_integer_float) : (si: int, sf: real) =
  63     ensures { si = add_int l /\ sf = add_real l }
  64   let si = ref 0 in
  65   let sf = ref 0.0 in
  66   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      | Cons (Integer n) t ->
  74          si := !si + n; ll := t
  75      | Cons (Real x) t ->
  76          sf := !sf +. x; ll := t
  77      end
  78   done;
  79   absurd
  80
  81
  82 let main () =
  83   let l =
  84     Cons (Integer 5) (Cons (Real 3.3) (Cons (Integer 8)
  85       (Cons (Real 1.4) (Cons (Integer 9) Nil))))
  86   in
  87   let s,f = sum l in
  88   assert { s = 22 };
  89   assert { f = 4.7 }
  90
  91 end