blob: 66b18f6f5852acf398eae83dc3028f884d9440b1 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
Require Import Coq.ZArith.BinIntDef.
Require Import Crypto.Compilers.SmartMap.
Require Import Crypto.Compilers.Syntax.
Require Import Crypto.Compilers.Z.Syntax.
Require Import Crypto.Compilers.Z.Syntax.Util.
Require Import Crypto.Compilers.ZExtended.Syntax.
Require Import Crypto.Compilers.ZExtended.Syntax.Util.
Require Import Crypto.Compilers.MapBaseType.
Definition MapBaseType' {t} (e : Expr t)
: Z.Syntax.Expr (Arrow (lift_flat_type unextend_base_type (domain t))
(lift_flat_type unextend_base_type (codomain t)))
:= @MapBaseType' _ _ _ _ unextend_base_type (fun _ s d opc _ => unextend_op opc)
(fun _ t => Op (make_const t (ZToInterp 0)) TT)
t e.
Definition MapBaseType {t} (e : Expr t)
: option (Z.Syntax.Expr (Arrow (lift_flat_type unextend_base_type (domain t))
(lift_flat_type unextend_base_type (codomain t))))
:= @MapBaseType _ _ _ _ unextend_base_type (fun _ s d opc _ => unextend_op opc)
(fun _ t => Op (make_const t (ZToInterp 0)) TT)
t e.
|
