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 use import SumList 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 use import SumList use import module ref.Ref 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