Library syntax
Require Export PosInf.
Require Export List.
Definition integer := nat.
Definition Var := Word.
Definition progCount := Word.
Definition Var_dec := eq_word_dec.
Definition ClassName := Word.
Definition FieldName := Word.
Definition Field_dec := eq_word_dec.
Definition MethodID := Word.
Definition MethodName := Word.
Definition MethodName_dec := eq_word_dec.
Inductive Operator : Set :=
| OpMult : Operator
| OpPlus : Operator.
Inductive Instruction : Set :=
| nop : Instruction
| push : integer -> Instruction
| pop : Instruction
| numop : Operator -> Instruction
| load : Var -> Instruction
| store : Var -> Instruction
| If : progCount -> Instruction
| new : ClassName -> Instruction
| putfield : FieldName -> Instruction
| getfield : FieldName -> Instruction
| goto : progCount -> Instruction.
Inductive typeOfField : Set :=
| fieldNum : typeOfField
| fieldRef : typeOfField.
Record Field : Set := Field_constr {
nameField : FieldName;
typeField : typeOfField
}.
Record Class : Set := Class_constr {
nameClass : ClassName;
instanceFields : (list Field)
}.
Record Program : Set := Program_constr {
classes : list Class;
instructions : list Instruction
}.
Definition nth_positive := fun (l:(list Instruction)) (pc:positive) =>
nth_error l (pred (nat_of_P pc)).
Definition instructionAt := fun (P:Program) (pc:progCount) =>
nth_positive (instructions P) (word2pos pc).
Definition nextAddress : Program -> progCount -> progCount :=
fun P pc => (succ_word pc).
Fixpoint searchField_rec (l:(list Field)) : FieldName->(option Field) :=
fun f => match l with
nil => None
| (cons fi q) => match (eq_word_dec f (nameField fi)) with
(left _) => (Some fi)
| (right _) => (searchField_rec q f)
end
end.
Definition searchField : Class->FieldName->(option Field) :=
fun c f => (searchField_rec (instanceFields c) f).
Fixpoint searchClass_rec (l:(list Class)) : ClassName->(option Class) :=
fun f => match l with
nil => None
| (cons fi q) => match (eq_word_dec f (nameClass fi)) with
(left _) => (Some fi)
| (right _) => (searchClass_rec q f)
end
end.
Lemma searchClass_rec_in_l : forall l cl c,
searchClass_rec l cl = Some c -> In c l.
induction l; simpl.
intros _ c H; inversion H.
intros cl c; case eq_word_dec; intros.
left; injection H; auto.
right; apply (IHl cl); auto.
Qed.
Lemma searchClass_rec_in_l_classname : forall l cl c,
searchClass_rec l cl = Some c -> eq_word cl (nameClass c).
induction l; simpl.
intros cl c H; inversion H.
intros cl c; case eq_word_dec; intros.
injection H; intros H1; rewrite <- H1; auto.
apply IHl; auto.
Qed.
Definition searchClass : Program->ClassName->(option Class) :=
fun P f => (searchClass_rec (classes P) f).
Lemma searchClass_in_class : forall P cl c,
searchClass P cl = Some c -> In c (classes P).
intros; apply searchClass_rec_in_l with cl; auto.
Qed.
Lemma searchClass_in_class_nameClass : forall P cl c,
searchClass P cl = Some c -> eq_word cl (nameClass c).
intros; apply searchClass_rec_in_l_classname with (classes P); auto.
Qed.
Lemma searchClass_eq_word : forall P cl1 cl2,
eq_word cl1 cl2 ->
searchClass P cl1 = searchClass P cl2.
unfold searchClass.
intros P cl1 cl2; generalize (classes P).
induction l; simpl; intros; auto.
case eq_word_dec; intros.
case eq_word_dec; intros.
auto.
elim n.
generalize dependent (nameClass a); intros.
destruct cl1; destruct cl2; destruct c; simpl in *; subst; auto.
case eq_word_dec; intros.
elim n.
generalize dependent (nameClass a); intros.
destruct cl1; destruct cl2; destruct c; simpl in *; subst; auto.
auto.
Qed.
Definition definedFields (P:Program) (cl:ClassName) : list FieldName :=
match (searchClass P cl) with
| Some c => map nameField (instanceFields c)
| None => nil
end.
Lemma definedFields_eq_word : forall P cl1 cl2,
eq_word cl1 cl2 ->
definedFields P cl1 = definedFields P cl2.
unfold definedFields; intros.
rewrite (searchClass_eq_word P cl1 cl2); auto.
Qed.
Lemma in_definedFields : forall P cl f,
In f (definedFields P cl) ->
exists c, searchClass P cl = Some c /\ ~ searchField c f = None /\
exists fi, In fi (instanceFields c) /\
f = nameField fi.
intros P cl f.
unfold definedFields.
CaseEq (searchClass P cl); intros.
exists c; split; auto.
split.
unfold searchField.
generalize dependent (instanceFields c).
induction l; simpl; intros.
elim H0.
elim H0; intros.
case eq_word_dec; intros.
discriminate.
elim n; rewrite H1.
destruct f; simpl; auto.
case eq_word_dec; intros.
discriminate.
auto.
generalize dependent (instanceFields c).
induction l; simpl; intros.
elim H0.
elim H0; intros.
eauto.
elim (IHl H1); intros.
exists x; intuition.
elim H0.
Qed.
Index
This page has been generated by coqdoc