blob: bdb7c8a25fca2e4d5f0c8168862fa92017f428f9 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
|
(** * Changing the interp function on PHOAS Representation of Gallina *)
Require Import Coq.Strings.String Coq.Classes.RelationClasses.
Require Import Crypto.Reflection.Syntax.
Require Import Crypto.Util.Tuple.
Require Import Crypto.Util.Tactics.
Require Import Crypto.Util.Notations.
Local Open Scope ctype_scope.
Local Open Scope expr_scope.
Section language.
Context {base_type_code : Type}
{interp_base_type1 interp_base_type2 : base_type_code -> Type}
{op : flat_type base_type_code -> flat_type base_type_code -> Type}
(f : forall t, interp_base_type1 t -> interp_base_type2 t).
Section with_var.
Context {var : base_type_code -> Type}.
Fixpoint mapf_interp {t} (e : @exprf base_type_code interp_base_type1 op var t)
: @exprf base_type_code interp_base_type2 op var t
:= match e in exprf _ _ _ t return exprf _ _ _ t with
| Const tx x => Const (mapf_interp_flat_type f x)
| Var _ x => Var x
| Op _ _ op args => Op op (@mapf_interp _ args)
| LetIn _ ex _ eC => LetIn (@mapf_interp _ ex) (fun x => @mapf_interp _ (eC x))
| Pair _ ex _ ey => Pair (@mapf_interp _ ex) (@mapf_interp _ ey)
end.
Fixpoint map_interp {t} (e : @expr base_type_code interp_base_type1 op var t)
: @expr base_type_code interp_base_type2 op var t
:= match e in expr _ _ _ t return expr _ _ _ t with
| Return _ x => Return (mapf_interp x)
| Abs _ _ f => Abs (fun x => @map_interp _ (f x))
end.
End with_var.
Definition MapInterp {t} (e : @Expr base_type_code interp_base_type1 op t)
: @Expr base_type_code interp_base_type2 op t
:= fun var => map_interp (e _).
End language.
Global Arguments mapf_interp {_ _ _ _} f {_ t} e.
Global Arguments map_interp {_ _ _ _} f {_ t} e.
Global Arguments MapInterp {_ _ _ _} f {t} e _.
|
