diff options
author | Yann Herklotz <git@yannherklotz.com> | 2022-07-19 08:53:57 +0200 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2022-07-19 08:53:57 +0200 |
commit | 5321f82fb46a87ca372b10ba5729509871cc935a (patch) | |
tree | 599ab805c9a807e9883cbae2dac034162e95890f /src/common/Vericertlib.v | |
parent | aa753acd776638971abb5d9901cc99ef259cb314 (diff) | |
download | vericert-5321f82fb46a87ca372b10ba5729509871cc935a.tar.gz vericert-5321f82fb46a87ca372b10ba5729509871cc935a.zip |
Work on implementing abstract predicates
Diffstat (limited to 'src/common/Vericertlib.v')
-rw-r--r-- | src/common/Vericertlib.v | 40 |
1 files changed, 1 insertions, 39 deletions
diff --git a/src/common/Vericertlib.v b/src/common/Vericertlib.v index 5540f34..24abece 100644 --- a/src/common/Vericertlib.v +++ b/src/common/Vericertlib.v @@ -31,6 +31,7 @@ Require Import compcert.lib.Integers. Require Import compcert.lib.Maps. Require Import vericert.common.Show. +Require Export vericert.common.Optionmonad. (* Depend on CompCert for the basic library, as they declare and prove some useful theorems. *) @@ -198,45 +199,6 @@ Ltac crush := simplify; try discriminate; try congruence; try lia; liapp; Definition compose (A B C : Type) (f : B -> C) (g : A -> B) (x : A) : C := f (g x). *) -Module Option. - -Definition default {T : Type} (x : T) (u : option T) : T := - match u with - | Some y => y - | _ => x - end. - -Definition map {S : Type} {T : Type} (f : S -> T) (u : option S) : option T := - match u with - | Some y => Some (f y) - | _ => None - end. - -Definition liftA2 {T : Type} (f : T -> T -> T) (a : option T) (b : option T) : option T := - match a with - | Some x => map (f x) b - | _ => None - end. - -Definition bind {A B : Type} (f : option A) (g : A -> option B) : option B := - match f with - | Some a => g a - | _ => None - end. - -Definition join {A : Type} (a : option (option A)) : option A := - match a with - | None => None - | Some a' => a' - end. - -Module Notation. -Notation "'do' X <- A ; B" := (bind A (fun X => B)) - (at level 200, X name, A at level 100, B at level 200). -End Notation. - -End Option. - Parameter debug_print : string -> unit. Definition debug_show {A B : Type} `{Show A} (a : A) (b : B) : B := |