aboutsummaryrefslogtreecommitdiff
path: root/src/Compilers/Named/Context.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Compilers/Named/Context.v')
-rw-r--r--src/Compilers/Named/Context.v32
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 _.