MARCHE Claude committed Jun 04, 2012 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 `````` Andrei Paskevich committed Jun 15, 2018 30 ``````use SumList `````` MARCHE Claude committed Jun 04, 2012 31 `````` `````` Andrei Paskevich committed Jun 07, 2018 32 ``````let rec sum (l: list or_integer_float) : (si: int, sf: real) = `````` MARCHE Claude committed Jan 26, 2014 33 `````` variant { l } `````` Andrei Paskevich committed Jun 07, 2018 34 `````` ensures { si = add_int l /\ sf = add_real l } `````` MARCHE Claude committed Jun 04, 2012 35 `````` match l with `````` Andrei Paskevich committed Jun 11, 2017 36 `````` | Nil -> 0, 0.0 `````` MARCHE Claude committed Jun 04, 2012 37 `````` | Cons h t -> `````` Andrei Paskevich committed Jun 11, 2017 38 `````` let a,b = sum t in `````` MARCHE Claude committed Jun 04, 2012 39 `````` match h with `````` Andrei Paskevich committed Jun 11, 2017 40 41 `````` | Integer n -> n + a, b | Real x -> a, x +. b `````` MARCHE Claude committed Jun 04, 2012 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 `````` Andrei Paskevich committed Jun 11, 2017 50 `````` let s,f = sum l in `````` MARCHE Claude committed Jun 04, 2012 51 52 53 54 55 56 57 58 `````` assert { s = 22 }; assert { f = 4.7 } end module AddListImp `````` Andrei Paskevich committed Jun 15, 2018 59 60 ``````use SumList use ref.Ref `````` MARCHE Claude committed Jun 04, 2012 61 `````` `````` Andrei Paskevich committed Jun 07, 2018 62 63 ``````let sum (l: list or_integer_float) : (si: int, sf: real) = ensures { si = add_int l /\ sf = add_real l } `````` MARCHE Claude committed Jun 04, 2012 64 65 66 `````` let si = ref 0 in let sf = ref 0.0 in let ll = ref l in `````` Andrei Paskevich committed Jun 06, 2017 67 `````` while True do `````` MARCHE Claude committed Jun 04, 2012 68 `````` invariant { !si + add_int !ll = add_int l /\ `````` Andrei Paskevich committed Jun 06, 2017 69 `````` !sf +. add_real !ll = add_real l } `````` MARCHE Claude committed Jan 26, 2014 70 `````` variant { !ll } `````` MARCHE Claude committed Jun 04, 2012 71 `````` match !ll with `````` Andrei Paskevich committed Jun 11, 2017 72 `````` | Nil -> return !si, !sf `````` MARCHE Claude committed Jun 04, 2012 73 74 75 76 77 `````` | Cons (Integer n) t -> si := !si + n; ll := t | Cons (Real x) t -> sf := !sf +. x; ll := t end `````` Andrei Paskevich committed Jun 06, 2017 78 79 `````` done; absurd `````` MARCHE Claude committed Jun 04, 2012 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 `````` Andrei Paskevich committed Jun 11, 2017 87 `````` let s,f = sum l in `````` MARCHE Claude committed Jun 04, 2012 88 89 90 91 `````` assert { s = 22 }; assert { f = 4.7 } end``````