From b06d11d9e12cae00475e8f9a5f69d42cf34ae729 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 11 Feb 2019 16:34:03 -0800 Subject: Add Option.{lift,map,combine}, List.Option.lift These will be useful for extending the AST with `option` types. --- src/AbstractInterpretationWf.v | 1 + src/Arithmetic.v | 2 +- src/CStringification.v | 2 +- src/Language.v | 2 +- src/LanguageWf.v | 2 +- src/Primitives/EdDSARepChange.v | 4 ++-- src/RewriterProofs.v | 2 +- src/RewriterRulesGood.v | 2 +- src/RewriterWf1.v | 2 +- src/RewriterWf2.v | 2 +- src/UnderLetsProofs.v | 2 +- src/Util/Option.v | 19 +++++++++++++++++++ src/Util/OptionList.v | 5 +++++ 13 files changed, 36 insertions(+), 11 deletions(-) (limited to 'src') diff --git a/src/AbstractInterpretationWf.v b/src/AbstractInterpretationWf.v index a6a2d8d6b..3d9f03f79 100644 --- a/src/AbstractInterpretationWf.v +++ b/src/AbstractInterpretationWf.v @@ -23,6 +23,7 @@ Require Import Crypto.LanguageInversion. Require Import Crypto.LanguageWf. Require Import Crypto.UnderLetsProofs. Require Import Crypto.AbstractInterpretation. +Import Coq.Lists.List. Module Compilers. Import Language.Compilers. diff --git a/src/Arithmetic.v b/src/Arithmetic.v index dc4c5031b..5f4b6de50 100644 --- a/src/Arithmetic.v +++ b/src/Arithmetic.v @@ -54,7 +54,7 @@ Require Import Crypto.Util.Prod. Require Import Crypto.Util.CPSNotations. Require Import Crypto.Util.Equality. Require Import Crypto.Util.Tactics.SetEvars. -Import ListNotations. Local Open Scope Z_scope. +Import Coq.Lists.List ListNotations. Local Open Scope Z_scope. Module Associational. Definition eval (p:list (Z*Z)) : Z := diff --git a/src/CStringification.v b/src/CStringification.v index b50957dcd..0cdf55c99 100644 --- a/src/CStringification.v +++ b/src/CStringification.v @@ -18,7 +18,7 @@ Require Import Crypto.Language. Require Import Crypto.AbstractInterpretation. Require Import Crypto.Util.Bool.Equality. Require Import Crypto.Util.Notations. -Import ListNotations. Local Open Scope zrange_scope. Local Open Scope Z_scope. +Import Coq.Lists.List ListNotations. Local Open Scope zrange_scope. Local Open Scope Z_scope. Module Compilers. Local Set Boolean Equality Schemes. diff --git a/src/Language.v b/src/Language.v index 6eac36949..efcc16b63 100644 --- a/src/Language.v +++ b/src/Language.v @@ -1237,7 +1237,7 @@ Module Compilers. | @repeat ?A => let rA := base.reify A in then_tac (@ident.List_repeat rA) - | @combine ?A ?B + | @List.combine ?A ?B => let rA := base.reify A in let rB := base.reify B in then_tac (@ident.List_combine rA rB) diff --git a/src/LanguageWf.v b/src/LanguageWf.v index 1aa0a775a..7f6bd5e18 100644 --- a/src/LanguageWf.v +++ b/src/LanguageWf.v @@ -31,7 +31,7 @@ Require Import Crypto.Util.Decidable. Require Import Crypto.Util.HProp. Require Import Crypto.Util.CPSNotations. Require Import Crypto.Util.Notations. -Import ListNotations. Local Open Scope list_scope. +Import Coq.Lists.List ListNotations. Local Open Scope list_scope. Import EqNotations. Module Compilers. diff --git a/src/Primitives/EdDSARepChange.v b/src/Primitives/EdDSARepChange.v index d867a62df..b7f4acd9b 100644 --- a/src/Primitives/EdDSARepChange.v +++ b/src/Primitives/EdDSARepChange.v @@ -56,7 +56,7 @@ Section EdDSA. Context {Edec:word b-> option E} {eq_enc_E_iff: forall P_ P, Eenc P = P_ <-> option_eq Eeq (Edec P_) (Some P)}. Context {Sdec:word b-> option (F l)} {eq_enc_S_iff: forall n_ n, Senc n = n_ <-> Sdec n_ = Some n}. - Local Infix "++" := combine. + Local Infix "++" := Word.combine. Definition verify'_sig : { verify | forall mlen (message:word mlen) (pk:word b) (sig:word (b+b)), verify mlen message pk sig = true <-> valid message pk sig }. Proof. @@ -231,7 +231,7 @@ Section EdDSA. dlet r := SRepDecModL (H _ (p ++ msg)) in dlet R := SRepERepMul r ErepB in dlet S := SRepAdd r (SRepMul (SRepDecModL (H _ (ERepEnc R ++ pk ++ msg))) s) in - ERepEnc R ++ SRepEnc S. + ERepEnc R ++ SRepEnc S. Lemma Z_l_nonzero : Z.pos l <> 0%Z. discriminate. Qed. diff --git a/src/RewriterProofs.v b/src/RewriterProofs.v index e4ac4afda..0587aec51 100644 --- a/src/RewriterProofs.v +++ b/src/RewriterProofs.v @@ -27,7 +27,7 @@ Require Import Crypto.Util.Option. Require Import Crypto.Util.CPSNotations. Require Import Crypto.Util.HProp. Require Import Crypto.Util.Decidable. -Import ListNotations. Local Open Scope list_scope. +Import Coq.Lists.List ListNotations. Local Open Scope list_scope. Local Open Scope Z_scope. Import EqNotations. diff --git a/src/RewriterRulesGood.v b/src/RewriterRulesGood.v index 9deb2ec6d..585ba2387 100644 --- a/src/RewriterRulesGood.v +++ b/src/RewriterRulesGood.v @@ -24,7 +24,7 @@ Require Import Crypto.Util.Option. Require Import Crypto.Util.CPSNotations. Require Import Crypto.Util.HProp. Require Import Crypto.Util.Decidable. -Import ListNotations. Local Open Scope list_scope. +Import Coq.Lists.List ListNotations. Local Open Scope list_scope. Local Open Scope Z_scope. Import EqNotations. diff --git a/src/RewriterWf1.v b/src/RewriterWf1.v index 2b18d01d0..f425a769b 100644 --- a/src/RewriterWf1.v +++ b/src/RewriterWf1.v @@ -34,7 +34,7 @@ Require Import Crypto.Util.CPSNotations. Require Import Crypto.Util.Notations. Require Import Crypto.Util.HProp. Require Import Crypto.Util.Decidable. -Import ListNotations. Local Open Scope list_scope. +Import Coq.Lists.List ListNotations. Local Open Scope list_scope. Local Open Scope Z_scope. Import EqNotations. diff --git a/src/RewriterWf2.v b/src/RewriterWf2.v index 13238361b..96911abe5 100644 --- a/src/RewriterWf2.v +++ b/src/RewriterWf2.v @@ -25,7 +25,7 @@ Require Import Crypto.Util.Option. Require Import Crypto.Util.CPSNotations. Require Import Crypto.Util.HProp. Require Import Crypto.Util.Decidable. -Import ListNotations. Local Open Scope list_scope. +Import Coq.Lists.List ListNotations. Local Open Scope list_scope. Local Open Scope Z_scope. Import EqNotations. diff --git a/src/UnderLetsProofs.v b/src/UnderLetsProofs.v index 787fdb7c4..884b6687a 100644 --- a/src/UnderLetsProofs.v +++ b/src/UnderLetsProofs.v @@ -12,7 +12,7 @@ Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Tactics.DestructHead. Require Import Crypto.Util.Tactics.SpecializeAllWays. Require Import Crypto.Util.Tactics.SpecializeBy. -Import ListNotations. Local Open Scope list_scope. +Import Coq.Lists.List ListNotations. Local Open Scope list_scope. Import EqNotations. Module Compilers. diff --git a/src/Util/Option.v b/src/Util/Option.v index 2c6549cb6..2eae8d0e5 100644 --- a/src/Util/Option.v +++ b/src/Util/Option.v @@ -16,6 +16,19 @@ Definition option_beq_hetero {A B} (AB_beq : A -> B -> bool) (x : option A) (y : => false end. +(** In general, [lift : M (option A) -> option (M A)]. This is a bit + confusing for [option] because [M = option]. We want to return + [None] if the thing contained in the [M (option A)] is [None], and + say [Some] otherwise. *) +Definition lift {A} (x : option (option A)) : option (option A) + := match x with + | Some None => None (* the contained thing is bad/not present *) + | Some (Some x) => Some (Some x) + | None => Some None + end. + +Notation map := option_map (only parsing). (* so we have [Option.map] *) + Definition bind {A B} (v : option A) (f : A -> option B) : option B := match v with | Some v => f v @@ -45,6 +58,12 @@ Module Export Notations. End Notations. Local Open Scope option_scope. +Definition combine {A B} (x : option A) (y : option B) : option (A * B) + := match x, y with + | Some x, Some y => Some (x, y) + | _, _ => None + end. + Section Relations. Definition option_eq {A B} eq (x : option A) (y : option B) := match x with diff --git a/src/Util/OptionList.v b/src/Util/OptionList.v index c2157346e..4b88dd9a3 100644 --- a/src/Util/OptionList.v +++ b/src/Util/OptionList.v @@ -25,6 +25,11 @@ Module Option. | x :: xs => (x <- x; @bind_list A B xs (fun xs => f (x :: xs))) end%option%list. + Definition lift {A} (ls : list (option A)) : option (list A) + := fold_right (fun x xs => x <- x; xs <- xs; Some (x :: xs))%option + (Some nil) + ls. + Module Export Notations. Notation "A <-- X ; B" := (bind_list X (fun A => B%option)) : option_scope. End Notations. -- cgit v1.2.3