107 lines
3.3 KiB
Coq
107 lines
3.3 KiB
Coq
Require Import Extraction.
|
|
Extraction Language Haskell.
|
|
|
|
Require Import ExtrHaskellBasic.
|
|
Require Import ExtrHaskellNatInt.
|
|
|
|
|
|
Inductive state: Type :=
|
|
| Good | Bad
|
|
| Tolerating: nat -> state.
|
|
|
|
Definition gtb (a b: nat): bool := Nat.ltb b a.
|
|
|
|
(* Goal *)
|
|
(* forall (a b:nat), Nat.ltb a b = gtb a b. *)
|
|
(* Proof. *)
|
|
(* intros a b. *)
|
|
(* induction a. *)
|
|
(* - induction b. *)
|
|
(* + trivial. *)
|
|
(* + simpl. *)
|
|
|
|
(*
|
|
p = (a+b) <= high && low >= (a+b)
|
|
~p;~p;~p |-> o=False
|
|
|
|
~p; X ~p; X X ~p ??????
|
|
*)
|
|
Definition monTf (limit: nat) (bounds: nat * nat) (st: state) (ab: nat * nat): state * bool :=
|
|
let a := fst ab in
|
|
let b := snd ab in
|
|
let low := fst bounds in
|
|
let high := snd bounds in
|
|
let res := a + b in
|
|
let outsideLimits :=
|
|
orb (Nat.ltb res low) (gtb res high) in
|
|
match st with
|
|
| Good =>
|
|
if outsideLimits then (Tolerating 1, true)
|
|
else (Good, true)
|
|
| Bad => (Bad, false)
|
|
| Tolerating failCount =>
|
|
if outsideLimits then
|
|
(*if failCount > limit then -- Spec mismatch. Tolerance is inclusive*)
|
|
if Nat.eqb failCount limit then (Bad, false)
|
|
else (Tolerating (S failCount), true)
|
|
else (Good, true)
|
|
end.
|
|
|
|
Extract Inductive nat => "Int" [ "0" "succ" ]
|
|
"(\fO fS n -> if n == 0 then fO () else fS (n - 1))".
|
|
|
|
(** ExtrHaskBasic **)
|
|
|
|
Extract Inductive bool => "Bool" [ "True" "False" ].
|
|
Extract Inductive option => "Maybe" [ "Just" "Nothing" ].
|
|
Extract Inductive unit => "()" [ "()" ].
|
|
Extract Inductive list => "([])" [ "([])" "(:)" ].
|
|
Extract Inductive prod => "(,)" [ "(,)" ].
|
|
|
|
Extract Inductive sumbool => "Bool" [ "True" "False" ].
|
|
Extract Inductive sumor => "Maybe" [ "Just" "Nothing" ].
|
|
Extract Inductive sum => "Either" [ "Left" "Right" ].
|
|
|
|
Extract Inlined Constant andb => "(&&)".
|
|
Extract Inlined Constant orb => "(||)".
|
|
Extract Inlined Constant negb => "not".
|
|
|
|
(** ExtrHaskellNatNum *)
|
|
|
|
Extract Inlined Constant Nat.add => "(+)".
|
|
Extract Inlined Constant Nat.mul => "(*)".
|
|
Extract Inlined Constant Nat.max => "max".
|
|
Extract Inlined Constant Nat.min => "min".
|
|
Extract Inlined Constant Init.Nat.add => "(+)".
|
|
Extract Inlined Constant Init.Nat.mul => "(*)".
|
|
Extract Inlined Constant Init.Nat.max => "max".
|
|
Extract Inlined Constant Init.Nat.min => "min".
|
|
Extract Inlined Constant Compare_dec.lt_dec => "(<)".
|
|
Extract Inlined Constant Compare_dec.leb => "(<=)".
|
|
Extract Inlined Constant Compare_dec.le_lt_dec => "(<=)".
|
|
Extract Inlined Constant Nat.eqb => "(==)".
|
|
Extract Inlined Constant EqNat.eq_nat_decide => "(==)".
|
|
Extract Inlined Constant Peano_dec.eq_nat_dec => "(==)".
|
|
|
|
Extract Constant Nat.pred => "(\n -> max 0 (pred n))".
|
|
Extract Constant Nat.sub => "(\n m -> max 0 (n - m))".
|
|
Extract Constant Init.Nat.pred => "(\n -> max 0 (pred n))".
|
|
Extract Constant Init.Nat.sub => "(\n m -> max 0 (n - m))".
|
|
|
|
Extract Constant Nat.div => "(\n m -> if m == 0 then 0 else div n m)".
|
|
Extract Constant Nat.modulo => "(\n m -> if m == 0 then n else mod n m)".
|
|
Extract Constant Init.Nat.div => "(\n m -> if m == 0 then 0 else div n m)".
|
|
Extract Constant Init.Nat.modulo => "(\n m -> if m == 0 then n else mod n m)".
|
|
|
|
(** Own *)
|
|
|
|
Extract Inlined Constant Nat.eqb => "(==)".
|
|
Extract Inlined Constant Nat.leb => "(<=)".
|
|
Extract Inlined Constant Nat.ltb => "(<)".
|
|
Extract Inlined Constant gtb => "(>)".
|
|
Extract Inlined Constant fst => "fst".
|
|
Extract Inlined Constant snd => "snd".
|
|
|
|
Recursive Extraction monTf.
|
|
Extraction "out.hs" monTf.
|