diff options
Diffstat (limited to 'src/Compilers/Named/Context.v')
| -rw-r--r-- | src/Compilers/Named/Context.v | 32 |
1 files changed, 16 insertions, 16 deletions
diff --git a/src/Compilers/Named/Context.v b/src/Compilers/Named/Context.v index ba0ad6feb..f63172de4 100644 --- a/src/Compilers/Named/Context.v +++ b/src/Compilers/Named/Context.v @@ -5,14 +5,14 @@ Require Import Crypto.Util.Notations. Record Context {base_type_code} (Name : Type) (var : base_type_code -> Type) := { ContextT : Type; - lookupb : ContextT -> Name -> forall {t : base_type_code}, option (var t); - extendb : ContextT -> Name -> forall {t : base_type_code}, var t -> ContextT; - removeb : ContextT -> Name -> base_type_code -> ContextT; + lookupb : forall {t : base_type_code}, ContextT -> Name -> option (var t); + extendb : forall {t : base_type_code}, ContextT -> Name -> var t -> ContextT; + removeb : base_type_code -> ContextT -> Name -> ContextT; empty : ContextT }. Coercion ContextT : Context >-> Sortclass. Arguments ContextT {_ _ _ _}, {_ _ _} _. -Arguments lookupb {_ _ _ _} _ _ {_}, {_ _ _ _} _ _ _. -Arguments extendb {_ _ _ _} _ _ [_] _. +Arguments lookupb {_ _ _ _ _} _ _, {_ _ _ _} _ _ _. +Arguments extendb {_ _ _ _} [_] _ _ _. Arguments removeb {_ _ _ _} _ _ _. Arguments empty {_ _ _ _}. @@ -24,31 +24,31 @@ Section language. Local Notation flat_type := (flat_type base_type_code). - Fixpoint extend (ctx : Context) {t : flat_type} + Fixpoint extend {t : flat_type} (ctx : Context) (n : interp_flat_type (fun _ => Name) t) (v : interp_flat_type var t) : Context := match t return interp_flat_type (fun _ => Name) t -> interp_flat_type var t -> Context with | Tbase t => fun n v => extendb ctx n v | Unit => fun _ _ => ctx | Prod A B => fun n v - => let ctx := @extend ctx A (fst n) (fst v) in - let ctx := @extend ctx B (snd n) (snd v) in + => let ctx := @extend A ctx (fst n) (fst v) in + let ctx := @extend B ctx (snd n) (snd v) in ctx end n v. - Fixpoint remove (ctx : Context) {t : flat_type} + Fixpoint remove {t : flat_type} (ctx : Context) (n : interp_flat_type (fun _ => Name) t) : Context := match t return interp_flat_type (fun _ => Name) t -> Context with - | Tbase t => fun n => removeb ctx n t + | Tbase t => fun n => removeb t ctx n | Unit => fun _ => ctx | Prod A B => fun n - => let ctx := @remove ctx A (fst n) in - let ctx := @remove ctx B (snd n) in + => let ctx := @remove A ctx (fst n) in + let ctx := @remove B ctx (snd n) in ctx end n. - Definition lookup (ctx : Context) {t} + Definition lookup {t} (ctx : Context) : interp_flat_type (fun _ => Name) t -> option (interp_flat_type var t) := smart_interp_flat_map (g := fun t => option (interp_flat_type var t)) @@ -60,6 +60,6 @@ Section language. end). End language. -Global Arguments extend {_ _ _ _} ctx {_} _ _. -Global Arguments remove {_ _ _ _} ctx {_} _. -Global Arguments lookup {_ _ _ _} ctx {_} _, {_ _ _ _} ctx _ _. +Global Arguments extend {_ _ _ _} {_} ctx _ _. +Global Arguments remove {_ _ _ _} {_} ctx _. +Global Arguments lookup {_ _ _ _} {_} ctx _, {_ _ _ _} _ ctx _. |