Samir Jindel
77736e83f2
Previously, we inferred the return type of statements in a way that made it impossible to prove the statement typing consistency. Now, we use just the stated return type for checking statements. The proofs of statement typing are complete, except for one result generalizing the expression typing consistency result to multiple variables changing; this result is obvious to see directly from the provided lemmas but very tedious to prove in Coq. Bug: Change-Id: I0bbcfb613df7510015f278fa85021ba0b3e57503 Reviewed-on: https://dart-review.googlesource.com/9020 Reviewed-by: Dmitry Stefantsov <dmitryas@google.com>
62 lines
2.6 KiB
V
62 lines
2.6 KiB
V
Require Export SyntaxRaw.
|
|
Require Import Common.
|
|
|
|
Scheme dart_type_ind_mutual := Induction for dart_type Sort Prop
|
|
with interface_type_ind_mutual := Induction for interface_type Sort Prop
|
|
with function_type_ind_mutual := Induction for function_type Sort Prop.
|
|
|
|
Scheme expression_ind_mutual := Induction for expression Sort Prop
|
|
with variable_get_ind_mutual := Induction for variable_get Sort Prop
|
|
with property_get_ind_mutual := Induction for property_get Sort Prop
|
|
with invocation_expression_ind_mutual := Induction for invocation_expression Sort Prop
|
|
with method_invocation_ind_mutual := Induction for method_invocation Sort Prop
|
|
with constructor_invocation_ind_mutual := Induction for constructor_invocation Sort Prop
|
|
with arguments_ind_mutual := Induction for arguments Sort Prop.
|
|
|
|
Scheme statement_ind_mutual := Induction for statement Sort Prop
|
|
with expression_statement_ind_mutual := Induction for expression_statement Sort Prop
|
|
with block_ind_mutual := Induction for block Sort Prop
|
|
with return_ind_mutual := Induction for return_statement Sort Prop
|
|
with variable_declaration_ind_mutual := Induction for variable_declaration Sort Prop
|
|
.
|
|
|
|
Definition dart_type_induction prop :=
|
|
dart_type_ind_mutual
|
|
prop
|
|
(fun i => prop (DT_Interface_Type i))
|
|
(fun f => prop (DT_Function_Type f)).
|
|
|
|
Definition expr_induction prop :=
|
|
expression_ind_mutual
|
|
(fun e => prop e)
|
|
(fun v => prop (E_Variable_Get v))
|
|
(fun p => prop (E_Property_Get p))
|
|
(fun ie => prop (E_Invocation_Expression ie))
|
|
(fun mi => prop (E_Invocation_Expression (IE_Method_Invocation mi)))
|
|
(fun ci => prop (E_Invocation_Expression (IE_Constructor_Invocation ci)))
|
|
(fun args => let (param) := args in prop param).
|
|
|
|
(* Since blocks contain lists of statements, we can't just use Scheme to
|
|
generate a good induction prinicple. *)
|
|
Section Statement_Mutual_Induction.
|
|
Variable P : statement -> Prop.
|
|
Hypothesis Return : forall r, P (S_Return_Statement r).
|
|
Hypothesis VarDecl : forall vd, P (S_Variable_Declaration vd).
|
|
Hypothesis Expr : forall e, P (S_Expression_Statement e).
|
|
Hypothesis Blk : forall ss, Forall P ss -> P (S_Block (Block ss)).
|
|
|
|
Fixpoint statement_induction s : P s :=
|
|
match s with
|
|
| S_Return_Statement r => Return r
|
|
| S_Expression_Statement e => Expr e
|
|
| S_Variable_Declaration vd => VarDecl vd
|
|
| S_Block (Block ss) =>
|
|
let ss_all := (fix rec (ss : list statement) : Forall P ss :=
|
|
match ss with
|
|
| nil => Forall_nil _
|
|
| (s::ss) => Forall_cons _ (statement_induction s) (rec ss)
|
|
end) ss in
|
|
Blk ss ss_all
|
|
end.
|
|
End Statement_Mutual_Induction.
|