chap11: progress
This commit is contained in:
+298
-92
@@ -22,32 +22,86 @@ Module Chap11.
|
||||
*)
|
||||
|
||||
Definition varname := string.
|
||||
Definition record_label := string.
|
||||
|
||||
Inductive type : Type :=
|
||||
(** T1 -> T2 *)
|
||||
| type_Arrow : type -> type -> type
|
||||
(** ArbitraryType *)
|
||||
| type_Base : string -> type
|
||||
(** T1 x T2 *)
|
||||
| type_Product : type -> type -> type
|
||||
| type_Tuple : list type -> type.
|
||||
|
||||
(** {T1, T2, ..., Tn} *)
|
||||
| type_Tuple : list type -> type
|
||||
(** { k1 : T1, k2 : T2, ..., kn : Tn } *)
|
||||
| type_Record : list (record_label * type) -> type
|
||||
(** T1 + T2 *)
|
||||
| type_Sum : type -> type -> type
|
||||
(** <l1 : T1, l2 : T2, ..., ln : Tn> *)
|
||||
| type_Variant : list (record_label * type) -> type.
|
||||
|
||||
Definition type_Bool := type_Base "Bool".
|
||||
Definition type_Unit := type_Base "Unit".
|
||||
|
||||
Module M := FMapList.Make(String_as_OT).
|
||||
Module MFacts := FMapFacts.WFacts_fun String_as_OT M.
|
||||
Definition context := M.t type.
|
||||
Definition empty_ctx : context := @M.empty type.
|
||||
|
||||
Inductive term : Type :=
|
||||
(** x *)
|
||||
| term_var : varname -> term
|
||||
(** t1 t2 *)
|
||||
| term_app : term -> term -> term
|
||||
(** (λx:T. t) *)
|
||||
| term_abs : varname -> type -> term -> term
|
||||
(** true *)
|
||||
| term_true : term
|
||||
(** false *)
|
||||
| term_false : term
|
||||
(** if t1 then t2 else t3 *)
|
||||
| term_if : term -> term -> term -> term
|
||||
(** unit *)
|
||||
| term_unit : term
|
||||
(** t as T *)
|
||||
| term_ascribe : term -> type -> term
|
||||
(** let x = t1 in t2 *)
|
||||
| term_let : varname -> term -> term -> term
|
||||
|
||||
(** {1,2} *)
|
||||
| term_pair : term -> term -> term
|
||||
(** fst {1,2} *)
|
||||
| term_fst : term -> term
|
||||
(** snd {1,2} *)
|
||||
| term_snd : term -> term
|
||||
|
||||
(** {5, true} *)
|
||||
| term_tuple : list term -> term
|
||||
| term_tuple_proj : term -> nat -> term.
|
||||
(** {5, true}.1 *)
|
||||
| term_tuple_proj : term -> nat -> term
|
||||
|
||||
(** { k = 1, y = true } *)
|
||||
| term_record : list (record_label * term) -> term
|
||||
(** { k = 1, y = true }.k *)
|
||||
| term_record_proj : term -> record_label -> term
|
||||
(** let p = t1 in t2 *)
|
||||
| term_pattern_bind : term -> term -> term -> term
|
||||
|
||||
(** inl t as T *)
|
||||
| term_inl : term -> type -> term
|
||||
(** inr t as T*)
|
||||
| term_inr : term -> type -> term
|
||||
(** case (t as T) of inl x => t1 | inr y => t2 *)
|
||||
| term_case : term -> type -> varname -> term -> varname -> term -> term
|
||||
|
||||
(** <var=t> as T *)
|
||||
| term_variant : record_label -> term -> type -> term
|
||||
|
||||
(** case t of <l_i=x_i> => t_i *)
|
||||
| term_variant_case : term -> list (record_label * varname * term) -> term
|
||||
|
||||
(** fix t *)
|
||||
| term_fix : term -> term.
|
||||
|
||||
(* Although we don't have syntax sugar because we omit "Notation",
|
||||
we can simply define a function that looks like a "term_" constructor
|
||||
@@ -55,27 +109,44 @@ Module Chap11.
|
||||
Definition term_seq (t1 t2 : term) : term :=
|
||||
term_app (term_abs "_" type_Unit t2) t1.
|
||||
|
||||
Module M := FMapList.Make(String_as_OT).
|
||||
Module MFacts := FMapFacts.WFacts_fun String_as_OT M.
|
||||
Definition context := M.t type.
|
||||
Definition empty_ctx : context := @M.empty type.
|
||||
Definition term_letrec (x : string) (T1 : type) (t1 : term) (t2 : term) : term :=
|
||||
term_let x (term_fix (term_abs x T1 t1)) t2.
|
||||
|
||||
Inductive value : term -> Prop :=
|
||||
Inductive is_value : term -> Prop :=
|
||||
| v_abs : forall (x : string) (T2 : type) (t1 : term),
|
||||
value (term_abs x T2 t1)
|
||||
is_value (term_abs x T2 t1)
|
||||
| v_true :
|
||||
value term_true
|
||||
is_value term_true
|
||||
| v_false :
|
||||
value term_false
|
||||
is_value term_false
|
||||
| v_unit :
|
||||
value term_unit
|
||||
is_value term_unit
|
||||
| v_pair : forall (v1 v2 : term),
|
||||
value v1 ->
|
||||
value v2 ->
|
||||
value (term_pair v1 v2)
|
||||
is_value v1 ->
|
||||
is_value v2 ->
|
||||
is_value (term_pair v1 v2)
|
||||
| v_tuple : forall (vs : list term),
|
||||
(forall v, In v vs -> value v) ->
|
||||
value (term_tuple vs).
|
||||
(forall v, In v vs -> is_value v) ->
|
||||
is_value (term_tuple vs)
|
||||
| v_record : forall (m : list (record_label * term)),
|
||||
(forall k v, In (k, v) m -> is_value v) ->
|
||||
is_value (term_record m)
|
||||
| v_inl : forall (v : term) (T : type),
|
||||
is_value v ->
|
||||
is_value (term_inl v T)
|
||||
| v_inr : forall (v : term) (T : type),
|
||||
is_value v ->
|
||||
is_value (term_inr v T)
|
||||
| v_variant : forall (l : record_label) (v : term) (T : type),
|
||||
is_value v ->
|
||||
is_value (term_variant l v T).
|
||||
|
||||
Inductive is_pattern : term -> Prop :=
|
||||
| p_var : forall (x : string),
|
||||
is_pattern (term_var x)
|
||||
| p_pattern_bind : forall (t1 t2 t3 : term),
|
||||
is_pattern t1 ->
|
||||
is_pattern (term_pattern_bind t1 t2 t3).
|
||||
|
||||
(* Before we continue with evaluation and typing rules,
|
||||
we need substitution. After chapter 6, it seems like tapl
|
||||
@@ -139,7 +210,15 @@ Module Chap11.
|
||||
is_free_variable x (term_tuple ts)
|
||||
| FV_TupleProj : forall x t n,
|
||||
is_free_variable x t ->
|
||||
is_free_variable x (term_tuple_proj t n).
|
||||
is_free_variable x (term_tuple_proj t n)
|
||||
|
||||
| FV_Record : forall x m,
|
||||
(forall k v, In (k, v) m -> is_free_variable x v) ->
|
||||
is_free_variable x (term_record m)
|
||||
| FV_RecordProj : forall x t k,
|
||||
is_free_variable x t ->
|
||||
is_free_variable x (term_record_proj t k).
|
||||
(* TODO: expand me, and double check that the above is correct *)
|
||||
|
||||
|
||||
(* In order to generate fresh names, we need to define a function that
|
||||
@@ -205,6 +284,7 @@ Module Chap11.
|
||||
|
||||
|
||||
Fixpoint substitute (x : string) (s : term) (t : term) : term :=
|
||||
let f := fun t => substitute x s t in
|
||||
match t with
|
||||
| term_var y =>
|
||||
if String.eqb x y
|
||||
@@ -213,108 +293,192 @@ Module Chap11.
|
||||
| term_abs y T t1 =>
|
||||
if String.eqb x y
|
||||
then t
|
||||
else term_abs y T (substitute x s t1)
|
||||
| term_app t1 t2 =>
|
||||
term_app (substitute x s t1) (substitute x s t2)
|
||||
| term_true =>
|
||||
term_true
|
||||
| term_false =>
|
||||
term_false
|
||||
| term_unit =>
|
||||
term_unit
|
||||
| term_if t1 t2 t3 =>
|
||||
term_if (substitute x s t1) (substitute x s t2) (substitute x s t3)
|
||||
| term_ascribe t1 T =>
|
||||
term_ascribe (substitute x s t1) T
|
||||
else term_abs y T (f t1)
|
||||
| term_app t1 t2 => term_app (f t1) (f t2)
|
||||
| term_true => term_true
|
||||
| term_false => term_false
|
||||
| term_unit => term_unit
|
||||
| term_if t1 t2 t3 => term_if (f t1) (f t2) (f t3)
|
||||
| term_ascribe t1 T => term_ascribe (f t1) T
|
||||
| term_let y t1 t2 =>
|
||||
if String.eqb x y
|
||||
then term_let y (substitute x s t1) t2
|
||||
else term_let y (substitute x s t1) (substitute x s t2)
|
||||
| term_pair t1 t2 =>
|
||||
term_pair (substitute x s t1) (substitute x s t2)
|
||||
| term_fst t1 =>
|
||||
term_fst (substitute x s t1)
|
||||
| term_snd t1 =>
|
||||
term_snd (substitute x s t1)
|
||||
| term_tuple ts =>
|
||||
term_tuple (map (substitute x s) ts)
|
||||
| term_tuple_proj t n =>
|
||||
term_tuple_proj (substitute x s t) n
|
||||
then term_let y (f t1) t2
|
||||
else term_let y (f t1) (f t2)
|
||||
| term_pair t1 t2 => term_pair (f t1) (f t2)
|
||||
| term_fst t1 => term_fst (f t1)
|
||||
| term_snd t1 => term_snd (f t1)
|
||||
| term_tuple ts => term_tuple (map f ts)
|
||||
| term_tuple_proj t n => term_tuple_proj (f t) n
|
||||
| term_record m => term_record (map (fun '(k, v) => (k, f v)) m)
|
||||
| term_record_proj t k => term_record_proj (f t) k
|
||||
| term_pattern_bind p t1 t2 => term_pattern_bind p (f t1) (f t2)
|
||||
| term_inl t1 T => term_inl (f t1) T
|
||||
| term_inr t1 T => term_inr (f t1) T
|
||||
| term_case t0 T x t1 y t2 => term_case (f t0) T x (f t1) y (f t2)
|
||||
| term_variant l t1 T => term_variant l (f t1) T
|
||||
| term_variant_case t0 cases =>
|
||||
term_variant_case (f t0) (map (fun '(l, x, t) => (l, x, f t)) cases)
|
||||
| term_fix t1 => term_fix (f t1)
|
||||
end.
|
||||
|
||||
Inductive matching : term -> term -> term -> Prop :=
|
||||
(** match(x, 5) -> [x -> 5] *)
|
||||
| M_Var : forall (x : string) (v : term),
|
||||
is_pattern (term_var x) ->
|
||||
matching (term_var x) v (substitute x v (term_var x)).
|
||||
(** match({x, y}, {5, true}) -> [x -> 5, y -> true]
|
||||
match(x, {5, true}) -> [x -> {5, true}] *)
|
||||
(* | M_Rcd : forall (t : *)
|
||||
|
||||
Inductive step : term -> term -> Prop :=
|
||||
| E_App1 : forall t1 t1' t2,
|
||||
| E_App1 : forall (t1 t1' t2 : term),
|
||||
step t1 t1' ->
|
||||
step (term_app t1 t2) (term_app t1' t2)
|
||||
| E_App2 : forall v1 t2 t2',
|
||||
value v1 ->
|
||||
| E_App2 : forall (v1 t2 t2' : term),
|
||||
is_value v1 ->
|
||||
step t2 t2' ->
|
||||
step (term_app v1 t2) (term_app v1 t2')
|
||||
|
||||
| E_AppAbs : forall x T t v,
|
||||
value v ->
|
||||
| E_AppAbs : forall (x : string) (T : type) (t v : term),
|
||||
is_value v ->
|
||||
step (term_app (term_abs x T t) v) (substitute x v t)
|
||||
|
||||
| E_Wildcard : forall t1 t2,
|
||||
| E_Wildcard : forall (t1 t2 : term),
|
||||
step (term_app (term_abs "_" type_Unit t1) t2) t1
|
||||
|
||||
| E_IfTrue : forall t1 t2,
|
||||
| E_IfTrue : forall (t1 t2 : term),
|
||||
step (term_if term_true t1 t2) t1
|
||||
| E_IfFalse : forall t1 t2,
|
||||
| E_IfFalse : forall (t1 t2 : term),
|
||||
step (term_if term_false t1 t2) t2
|
||||
| E_If : forall t1 t1' t2 t3,
|
||||
| E_If : forall (t1 t1' t2 t3 : term),
|
||||
step t1 t1' ->
|
||||
step (term_if t1 t2 t3) (term_if t1' t2 t3)
|
||||
|
||||
| E_Ascribe : forall v T,
|
||||
value v ->
|
||||
| E_Ascribe : forall (v : term) (T : type),
|
||||
is_value v ->
|
||||
step (term_ascribe v T) v
|
||||
| E_Ascribe1 : forall t t' T,
|
||||
| E_Ascribe1 : forall (t t' : term) (T : type),
|
||||
step t t' ->
|
||||
step (term_ascribe t T) (term_ascribe t' T)
|
||||
|
||||
| E_LetV : forall x v t2,
|
||||
value v ->
|
||||
| E_LetV : forall (x : string) (v t2 : term),
|
||||
is_value v ->
|
||||
step (term_let x v t2) (substitute x v t2)
|
||||
| E_Let : forall x t1 t1' t2,
|
||||
| E_Let : forall (x : string) (t1 t1' t2 : term),
|
||||
step t1 t1' ->
|
||||
step (term_let x t1 t2) (term_let x t1' t2)
|
||||
|
||||
| E_PairBeta1 : forall v1 v2,
|
||||
value v1 ->
|
||||
value v2 ->
|
||||
| E_PairBeta1 : forall (v1 v2 : term),
|
||||
is_value v1 ->
|
||||
is_value v2 ->
|
||||
step (term_fst (term_pair v1 v2)) v1
|
||||
| E_PairBeta2 : forall v1 v2,
|
||||
value v1 ->
|
||||
value v2 ->
|
||||
| E_PairBeta2 : forall (v1 v2 : term),
|
||||
is_value v1 ->
|
||||
is_value v2 ->
|
||||
step (term_snd (term_pair v1 v2)) v2
|
||||
| E_Proj1 : forall t1 t1',
|
||||
| E_Proj1 : forall (t1 t1' : term),
|
||||
step t1 t1' ->
|
||||
step (term_fst t1) (term_fst t1')
|
||||
| E_Proj2 : forall t1 t1',
|
||||
| E_Proj2 : forall (t1 t1' : term),
|
||||
step t1 t1' ->
|
||||
step (term_snd t1) (term_snd t1')
|
||||
| E_Pair1 : forall t1 t1' t2,
|
||||
| E_Pair1 : forall (t1 t1' t2 : term),
|
||||
step t1 t1' ->
|
||||
step (term_pair t1 t2) (term_pair t1' t2)
|
||||
| E_Pair2 : forall v1 t2 t2',
|
||||
value v1 ->
|
||||
| E_Pair2 : forall (v1 t2 t2' : term),
|
||||
is_value v1 ->
|
||||
step t2 t2' ->
|
||||
step (term_pair v1 t2) (term_pair v1 t2')
|
||||
|
||||
| E_ProjTuple :
|
||||
forall vs n,
|
||||
(forall v, In v vs -> value v) ->
|
||||
forall (vs : list term) (n : nat),
|
||||
(forall v, In v vs -> is_value v) ->
|
||||
n < length vs ->
|
||||
step (term_tuple_proj (term_tuple vs) n) (nth n vs term_unit)
|
||||
| E_Proj : forall t1 t1' n,
|
||||
| E_Proj : forall (t1 t1' : term) (n : nat),
|
||||
step t1 t1' ->
|
||||
step (term_tuple_proj t1 n) (term_tuple_proj t1' n)
|
||||
| E_Tuple : forall ts ts' n,
|
||||
(forall i, i < n -> i < length ts -> value (nth i ts term_unit)) ->
|
||||
(step (nth n ts term_unit) (nth n ts' term_unit)) ->
|
||||
ts' = List.app (firstn n ts) ((nth n ts' term_unit) :: (skipn (S n) ts)) ->
|
||||
step (term_tuple ts) (term_tuple ts').
|
||||
| E_Tuple : forall (t : list term) (tj tj' : term) (j : nat),
|
||||
(* j is bounded by the length of the tuple *)
|
||||
0 <= j < length t ->
|
||||
(* All terms before j are values *)
|
||||
(forall i,
|
||||
1 <= i < j ->
|
||||
i < length t ->
|
||||
is_value (nth i t term_unit)) ->
|
||||
(* j-th element is an evaluatable term *)
|
||||
tj = nth j t term_unit ->
|
||||
step tj tj' ->
|
||||
(* t' is the tuple with the j-th element replaced by tj' *)
|
||||
let t' := List.app (firstn j t) (nth j t term_unit :: (skipn (S j) t)) in
|
||||
step (term_tuple t) (term_tuple t')
|
||||
|
||||
| E_ProjRcd : forall (k : record_label) (v : term) (m : list (record_label * term)),
|
||||
(forall k' v', In (k', v') m -> is_value v') ->
|
||||
In (k, v) m ->
|
||||
step (term_record_proj (term_record m) k) v
|
||||
| E_Proj' : forall (t1 t1' : term) (k : record_label),
|
||||
step t1 t1' ->
|
||||
step (term_record_proj t1 k) (term_record_proj t1' k)
|
||||
| E_Rcd : forall (r : list (string * term)) (tj tj' : term) (j : nat),
|
||||
(* j is bounded by the length of the record *)
|
||||
1 <= j <= length r ->
|
||||
(* All terms before j are values *)
|
||||
(forall i,
|
||||
1 <= i < j ->
|
||||
i < length r ->
|
||||
is_value (snd (nth i r ("", term_unit)))) ->
|
||||
(* j-th element is an evaluatable term *)
|
||||
tj = snd (nth j r ("", term_unit)) ->
|
||||
step tj tj' ->
|
||||
(* r' is the record with the j-th element replaced by tj' *)
|
||||
let r' := List.app (firstn j r) (nth j r ("", term_unit) :: (skipn (S j) r)) in
|
||||
step (term_record r) (term_record r')
|
||||
|
||||
(* TODO: this should possibly perform some sort of substitution *)
|
||||
| E_LetVPattern : forall (p v t2 : term),
|
||||
is_pattern p ->
|
||||
is_value v ->
|
||||
matching p v t2 ->
|
||||
step (term_pattern_bind p v t2) t2
|
||||
|
||||
| E_LetPattern : forall (p t1 t1' t2 : term),
|
||||
is_pattern p ->
|
||||
step t1 t1' ->
|
||||
step (term_pattern_bind p t1 t2) (term_pattern_bind p t1' t2)
|
||||
|
||||
| E_CaseInl : forall (v t1 t2 : term) (T : type) (x y : string),
|
||||
is_value v ->
|
||||
step (term_case (term_inl v T) T x t1 y t2) (substitute x v t1)
|
||||
| E_CaseInr : forall (v t1 t2 : term) (T : type) (x y : string),
|
||||
is_value v ->
|
||||
step (term_case (term_inr v T) T x t1 y t2) (substitute y v t2)
|
||||
| E_Case : forall (t t' t1 t2 : term) (T : type) (x y : string),
|
||||
step t t' ->
|
||||
step (term_case t T x t1 y t2) (term_case t' T x t1 y t2)
|
||||
| E_Inl : forall (t t' : term) (T : type),
|
||||
step t t' ->
|
||||
step (term_inl t T) (term_inl t' T)
|
||||
| E_Inr : forall (t t' : term) (T : type),
|
||||
step t t' ->
|
||||
step (term_inr t T) (term_inr t' T)
|
||||
|
||||
| E_CaseVariant : forall (Γ : context) (lj xj : record_label) (vj tj : term) (T : type) (c : list (record_label * varname * term)),
|
||||
is_value vj ->
|
||||
In (lj, xj, tj) c ->
|
||||
step (term_variant_case (term_variant lj vj T) c) (substitute xj vj tj)
|
||||
| E_Case' : forall (t0 t0' : term) (c : list (record_label * varname * term)),
|
||||
step t0 t0' ->
|
||||
step (term_variant_case t0 c) (term_variant_case t0' c)
|
||||
| E_Variant : forall (l : record_label) (t t' : term) (T : type),
|
||||
step t t' ->
|
||||
step (term_variant l t T) (term_variant l t' T)
|
||||
|
||||
| E_FixBeta : forall (x : string) (T1 : type) (t2 : term),
|
||||
step (term_fix (term_abs x T1 t2)) (substitute x (term_fix (term_abs x T1 t2)) t2)
|
||||
| E_Fix : forall (t t' : term),
|
||||
step t t' ->
|
||||
step (term_fix t) (term_fix t').
|
||||
|
||||
Inductive has_type : context -> term -> type -> Prop :=
|
||||
| T_Var : forall (Γ : context) (x : string) (T1 : type),
|
||||
@@ -330,59 +494,101 @@ Module Chap11.
|
||||
has_type Γ t2 T2 ->
|
||||
has_type Γ (term_app t1 t2) T1
|
||||
|
||||
| T_True : forall Γ,
|
||||
| T_True : forall (Γ : context),
|
||||
has_type Γ term_true type_Bool
|
||||
| T_False : forall Γ,
|
||||
| T_False : forall (Γ : context),
|
||||
has_type Γ term_false type_Bool
|
||||
|
||||
| T_If : forall t1 t2 t3 T1 Γ,
|
||||
| T_If : forall (Γ : context) (t1 t2 t3 : term) (T1 : type),
|
||||
has_type Γ t1 type_Bool ->
|
||||
has_type Γ t2 T1 ->
|
||||
has_type Γ t3 T1 ->
|
||||
has_type Γ (term_if t1 t2 t3) T1
|
||||
|
||||
| T_Unit : forall Γ,
|
||||
| T_Unit : forall (Γ : context),
|
||||
has_type Γ term_unit type_Unit
|
||||
|
||||
| T_Wildcard : forall Γ t T,
|
||||
| T_Wildcard : forall (Γ : context) (t : term) (T : type),
|
||||
has_type Γ t T ->
|
||||
has_type Γ (term_abs "_" T t) (type_Arrow T type_Unit)
|
||||
|
||||
| T_Ascribe : forall Γ t T,
|
||||
| T_Ascribe : forall (Γ : context) (t : term) (T : type),
|
||||
has_type Γ t T ->
|
||||
has_type Γ (term_ascribe t T) T
|
||||
|
||||
| T_Let : forall Γ x t1 t2 T1 T2,
|
||||
| T_Let : forall (Γ : context) (x : string) (t1 t2 : term) (T1 T2 : type),
|
||||
has_type Γ t1 T1 ->
|
||||
has_type (M.add x T1 Γ) t2 T2 ->
|
||||
has_type Γ (term_let x t1 t2) T2
|
||||
|
||||
| T_Pair : forall Γ t1 t2 T1 T2,
|
||||
| T_Pair : forall (Γ : context) (t1 t2 : term) (T1 T2 : type),
|
||||
has_type Γ t1 T1 ->
|
||||
has_type Γ t2 T2 ->
|
||||
has_type Γ (term_pair t1 t2) (type_Product T1 T2)
|
||||
|
||||
| T_Proj1 : forall Γ t T1 T2,
|
||||
| T_Proj1 : forall (Γ : context) (t : term) (T1 T2 : type),
|
||||
has_type Γ t (type_Product T1 T2) ->
|
||||
has_type Γ (term_fst t) T1
|
||||
| T_Proj2 : forall Γ t T1 T2,
|
||||
| T_Proj2 : forall (Γ : context) (t : term) (T1 T2 : type),
|
||||
has_type Γ t (type_Product T1 T2) ->
|
||||
has_type Γ (term_snd t) T2
|
||||
|
||||
| T_Tuple : forall Γ ts Ts,
|
||||
| T_Tuple : forall (Γ : context) (ts : list term) (Ts : list type),
|
||||
(forall t T, In (t, T) (combine ts Ts) -> has_type Γ t T) ->
|
||||
has_type Γ (term_tuple ts) (type_Tuple Ts)
|
||||
| T_Proj : forall Γ t Ts n T,
|
||||
| T_TupleProj : forall (Γ : context) (t : term) (Ts : list type) (n : nat) (T : type),
|
||||
has_type Γ t (type_Tuple Ts) ->
|
||||
n < length Ts ->
|
||||
nth_error Ts n = Some T ->
|
||||
has_type Γ (term_tuple_proj t n) T.
|
||||
has_type Γ (term_tuple_proj t n) T
|
||||
|
||||
| T_Rcd : forall (Γ : context) (m : list (record_label * term)) (Ts : list type),
|
||||
(forall (k : record_label) (v : term) (T : type),
|
||||
In (k, T) (combine (map fst m) Ts) ->
|
||||
has_type Γ v T) ->
|
||||
has_type Γ (term_record m) (type_Record (combine (map fst m) Ts))
|
||||
| T_RcdProj : forall (Γ : context) (t : term) (m : list (record_label * type)) (k : record_label) (T : type),
|
||||
has_type Γ t (type_Record m) ->
|
||||
In (k, T) m ->
|
||||
has_type Γ (term_record_proj t k) T
|
||||
|
||||
| T_Inl : forall (Γ : context) (t : term) (T1 T2 : type),
|
||||
has_type Γ t T1 ->
|
||||
has_type Γ (term_inl t (type_Sum T1 T2)) (type_Sum T1 T2)
|
||||
| T_Inr : forall (Γ : context) (t : term) (T1 T2 : type),
|
||||
has_type Γ t T2 ->
|
||||
has_type Γ (term_inr t (type_Sum T1 T2)) (type_Sum T1 T2)
|
||||
| T_Case : forall (Γ : context) (t0 t1 t2 : term) (x1 x2 : string) (T1 T2 T : type),
|
||||
has_type Γ t0 (type_Sum T1 T2) ->
|
||||
has_type (M.add x1 T1 Γ) t1 T ->
|
||||
has_type (M.add x2 T2 Γ) t2 T ->
|
||||
has_type Γ (term_case t0 T x1 t1 x2 t2) T
|
||||
|
||||
| T_Variant : forall (Γ : context) (tj : term) (l : record_label) (Tj : type) (c : list (record_label * type)),
|
||||
has_type Γ tj Tj ->
|
||||
In (l, Tj) c ->
|
||||
has_type Γ (term_variant l tj (type_Variant c)) (type_Variant c)
|
||||
| T_VariantCase : forall (Γ : context) (t0 : term) (cs : list (record_label * varname * term)) (Ts: list (record_label * type)) (T : type),
|
||||
(* All labels in the case must be in the type *)
|
||||
let case_labels := map (fun '(l, _, _) => l) cs in
|
||||
let type_labels := map (fun '(l, _) => l) Ts in
|
||||
(forall l, In l case_labels <-> In l type_labels) ->
|
||||
(* All types in the typemap must yield T for the entire variant *)
|
||||
(forall (l : record_label) (x : varname) (t : term) (T' : type),
|
||||
In (l, x, t) cs ->
|
||||
In (l, T') Ts ->
|
||||
has_type (M.add x T' Γ) t T) ->
|
||||
has_type Γ (term_variant_case t0 cs) T
|
||||
|
||||
| T_Fix : forall (Γ : context) (t1 : term) (T1 : type),
|
||||
has_type Γ t1 (type_Arrow T1 T1) ->
|
||||
has_type Γ (term_fix t1) T1.
|
||||
|
||||
(* 11.3.2 *)
|
||||
(* Give typing and evaluation rules for wildcard abstractions, and
|
||||
prove that they can be derived from the abbreviation stated above. *)
|
||||
|
||||
Lemma substitution_noop : forall (Γ : context) (x : string) (v t : term) (T : type),
|
||||
(* Lemma substitution_noop : forall (Γ : context) (x : string) (v t : term) (T : type),
|
||||
~ is_free_variable x t ->
|
||||
substitute x v t = t.
|
||||
Proof.
|
||||
@@ -437,7 +643,7 @@ Module Chap11.
|
||||
intros Γ x v t T1 T2 Ht Hv.
|
||||
generalize dependent Γ.
|
||||
generalize dependent T1.
|
||||
induction t; intros T1 Γ Ht; simpl in *; inversion Ht; subst; try (econstructor; eauto).
|
||||
induction t; intros T1 Γ Ht; simpl in *; inversion Ht; subst; try (econstructor; eauto). *)
|
||||
|
||||
Definition wildcard (t : term) (T : type) : term :=
|
||||
term_app (term_abs "_" T t) (term_unit).
|
||||
|
||||
Reference in New Issue
Block a user