From d95707e8c3e8fa8ae58eeec15448556ab7eeb0b3 Mon Sep 17 00:00:00 2001 From: Robert Sloan Date: Fri, 26 Aug 2016 16:50:48 -0700 Subject: Fix evalWordRangeOpt --- src/Assembly/Evaluables.v | 2 +- src/Experiments/SpecificCurve25519.v | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) (limited to 'src') diff --git a/src/Assembly/Evaluables.v b/src/Assembly/Evaluables.v index 823d05cfb..6a08a7d54 100644 --- a/src/Assembly/Evaluables.v +++ b/src/Assembly/Evaluables.v @@ -548,7 +548,7 @@ Section WordRange. | someRange low high _ _ => Some (range N low high) | applyBinOp rangeF wordF _ a b => omap (evalWordRangeOpt a) (fun a' => - omap (evalWordRangeOpt a) (fun b' => + omap (evalWordRangeOpt b) (fun b' => rangeF a' b')) end. diff --git a/src/Experiments/SpecificCurve25519.v b/src/Experiments/SpecificCurve25519.v index b5878825f..80f6ff3a6 100644 --- a/src/Experiments/SpecificCurve25519.v +++ b/src/Experiments/SpecificCurve25519.v @@ -118,6 +118,8 @@ Module Input. Definition ZInterp {t} E := @Interp Z ZEvaluable t E. + Definition WordInterp {n t} E := @Interp (word n) (@WordEvaluable n) t E. + Definition RangeInterp {n t} E: @interp_type (option (Range N)) t := typeMap evalWordRangeOpt (@Interp (@WordRangeOpt n) (@WordRangeOptEvaluable n) t E). -- cgit v1.2.3