From c99ea831128b7bc7724a06c5e5f52830f5ffe4d2 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 23 Oct 2017 22:07:14 -0400 Subject: Factor out some code in src/Compilers/Named/MapType.v --- src/Compilers/Named/MapType.v | 33 ++++++++------------------------- 1 file changed, 8 insertions(+), 25 deletions(-) (limited to 'src') 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. -- cgit v1.2.3