blob: 79f620edbf8ac211a424036cf235e6bffcfff58b (
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
44
45
46
47
48
49
50
51
52
53
54
55
56
|
Require Import Crypto.Compilers.SmartMap.
Require Import Crypto.Compilers.Syntax.
Require Import Crypto.Compilers.Named.Context.
Require Import Crypto.Compilers.Named.Syntax.
Require Import Crypto.Util.PointedProp.
Module Export Named.
Section language.
Context {base_type_code Name : Type}
{op : flat_type base_type_code -> flat_type base_type_code -> Type}.
Section with_var.
Context {var}
(Context : @Context base_type_code Name var).
Section gen.
Context (quantify : forall tx, (interp_flat_type var tx -> option pointed_Prop) -> option pointed_Prop).
Fixpoint wff_gen (ctx : Context) {t} (e : @exprf base_type_code op Name t) : option pointed_Prop
:= match e with
| TT => Some trivial
| Var t n => match lookupb t ctx n return bool with
| Some _ => true
| None => false
end
| Op _ _ op args => @wff_gen ctx _ args
| LetIn _ n ex _ eC => @wff_gen ctx _ ex
/\ quantify _ (fun v => @wff_gen (extend ctx n v) _ eC)
| Pair _ ex _ ey => @wff_gen ctx _ ex /\ @wff_gen ctx _ ey
end%option_pointed_prop.
End gen.
Definition wff := wff_gen (fun tx f => inject (forall v, prop_of_option (f v))).
Definition wf (ctx : Context) {t} (e : @expr base_type_code op Name t) : Prop
:= forall v, prop_of_option (@wff (extend ctx (Abs_name e) v) _ (invert_Abs e)).
End with_var.
Section unit.
Context (Context : @Context base_type_code Name (fun _ => unit)).
Local Notation TT := (SmartValf _ (fun _ => tt) _).
Definition wff_unit := wff_gen Context (fun tx f => f TT).
Definition wf_unit ctx {t} (e : @expr base_type_code op Name t) : option pointed_Prop
:= @wff_unit (extend ctx (Abs_name e) TT) _ (invert_Abs e).
End unit.
Definition Wf (Context : forall var, @Context base_type_code Name var) {t} (e : @expr base_type_code op Name t)
:= forall var, wf (Context var) empty e.
End language.
End Named.
Global Arguments wff_gen {_ _ _ _ _} quantify ctx {t} _.
Global Arguments wff_unit {_ _ _ _} ctx {t} _.
Global Arguments wf_unit {_ _ _ _} ctx {t} _.
Global Arguments wff {_ _ _ _ _} ctx {t} _.
Global Arguments wf {_ _ _ _ _} ctx {t} _.
Global Arguments Wf {_ _ _} Context {t} _.
|
