diff options
author | Jason Gross <jgross@mit.edu> | 2017-10-23 22:07:14 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-10-23 22:07:14 -0400 |
commit | c99ea831128b7bc7724a06c5e5f52830f5ffe4d2 (patch) | |
tree | 07d6bfd424f18a0cc7a1aaed52a4443c4b97e328 /src | |
parent | 8ba5b99185d3ae7725a37aea0c4594f9bceb3600 (diff) |
Factor out some code in src/Compilers/Named/MapType.v
Diffstat (limited to 'src')
-rw-r--r-- | src/Compilers/Named/MapType.v | 33 |
1 files changed, 8 insertions, 25 deletions
diff --git a/src/Compilers/Named/MapType.v b/src/Compilers/Named/MapType.v index 06d8063b8..15b40f7b7 100644 --- a/src/Compilers/Named/MapType.v +++ b/src/Compilers/Named/MapType.v @@ -9,32 +9,15 @@ Section language. {op1 : flat_type base_type_code1 -> flat_type base_type_code1 -> Type} {op2 : flat_type base_type_code2 -> flat_type base_type_code2 -> Type} {Name : Type} - (f_base_type_code : base_type_code1 -> base_type_code2). - Fixpoint lift_flat_type (t : flat_type base_type_code1) : flat_type base_type_code2 - := match t with - | Tbase T => Tbase (f_base_type_code T) - | Unit => Unit - | Prod A B => Prod (lift_flat_type A) (lift_flat_type B) - end. - Context (f_op : forall s d, + (f_base : base_type_code1 -> base_type_code2) + (f_op : forall s d, op1 s d - -> option (op2 (lift_flat_type s) (lift_flat_type d))). - - Fixpoint transfer_interp_flat_type {t} - : interp_flat_type (fun _ => Name) t - -> interp_flat_type (fun _ => Name) (lift_flat_type t) - := match t with - | Tbase T => fun v => v - | Unit => fun v => v - | Prod A B => fun ab : interp_flat_type _ A * interp_flat_type _ B - => (@transfer_interp_flat_type _ (fst ab), - @transfer_interp_flat_type _ (snd ab))%core - end. + -> option (op2 (lift_flat_type f_base s) (lift_flat_type f_base d))). Fixpoint mapf_type {t} (e : exprf base_type_code1 op1 Name t) - : option (exprf base_type_code2 op2 Name (lift_flat_type t)) - := match e in exprf _ _ _ t return option (exprf _ _ _ (lift_flat_type t)) with + : option (exprf base_type_code2 op2 Name (lift_flat_type f_base t)) + := match e in exprf _ _ _ t return option (exprf _ _ _ (lift_flat_type f_base t)) with | TT => Some TT | Var t x => Some (Var x) | Op t1 tR opc args @@ -45,7 +28,7 @@ Section language. | _, _ => None end | LetIn tx n ex tC eC - => let n := transfer_interp_flat_type n in + => let n := transfer_interp_flat_type f_base (fun _ (n : Name) => n) n in let ex := @mapf_type _ ex in let eC := @mapf_type _ eC in match ex, eC with @@ -65,11 +48,11 @@ Section language. Definition map_type {t} (e : expr base_type_code1 op1 Name t) - : option (expr base_type_code2 op2 Name (Arrow (lift_flat_type (domain t)) (lift_flat_type (codomain t)))) + : option (expr base_type_code2 op2 Name (Arrow (lift_flat_type f_base (domain t)) (lift_flat_type f_base (codomain t)))) := let f := invert_Abs e in let f := mapf_type f in let n := Abs_name e in - let n := transfer_interp_flat_type n in + let n := transfer_interp_flat_type f_base (fun _ (n : Name) => n) n in option_map (fun f => Abs n f) f. |