Mercurial > cpdt > repo

comparison src/Hoas.v @ 292:2c88fc1dbe33

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
A pass of double-quotes and LaTeX operator beautification
author Adam Chlipala <adam@chlipala.net>
date Wed, 10 Nov 2010 16:31:04 -0500
parents e3c3b7ef5901
children b441010125d4
comparison
equal deleted inserted replaced
291:da9ccc6bf572 292:2c88fc1dbe33
1 (* Copyright (c) 2008-2009, Adam Chlipala 1 (* Copyright (c) 2008-2010, Adam Chlipala
2 * 2 *
3 * This work is licensed under a 3 * This work is licensed under a
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
5 * Unported License. 5 * Unported License.
6 * The license text is available at: 6 * The license text is available at:
23 In this chapter, we will see that HOAS cannot be implemented directly in Coq. However, a few very similar encodings are possible and are in fact very effective in some important domains. *) 23 In this chapter, we will see that HOAS cannot be implemented directly in Coq. However, a few very similar encodings are possible and are in fact very effective in some important domains. *)
24 24
25 25
26 (** * Classic HOAS *) 26 (** * Classic HOAS *)
27 27
28 (** The motto of HOAS is simple: represent object language binders using meta language binders. Here, "object language" refers to the language being formalized, while the meta language is the language in which the formalization is done. Our usual meta language, Coq's Gallina, contains the standard binding facilities of functional programming, making it a promising base for higher-order encodings. 28 (** The motto of HOAS is simple: represent object language binders using meta language binders. Here, %``%#"#object language#"#%''% refers to the language being formalized, while the meta language is the language in which the formalization is done. Our usual meta language, Coq's Gallina, contains the standard binding facilities of functional programming, making it a promising base for higher-order encodings.
29 29
30 Recall the concrete encoding of basic untyped lambda calculus expressions. *) 30 Recall the concrete encoding of basic untyped lambda calculus expressions. *)
31 31
32 Inductive uexp : Set := 32 Inductive uexp : Set :=
33 | UVar : string -> uexp 33 | UVar : string -> uexp
498 498
499 Infix "@" := plug (no associativity, at level 60). 499 Infix "@" := plug (no associativity, at level 60).
500 500
501 (** Finally, we have the step relation itself, which combines our ingredients in the standard way. In the congruence rule, we introduce the extra variable [E1] and its associated equality to make the rule easier for [eauto] to apply. *) 501 (** Finally, we have the step relation itself, which combines our ingredients in the standard way. In the congruence rule, we introduce the extra variable [E1] and its associated equality to make the rule easier for [eauto] to apply. *)
502 502
503 (** printing ==> $\Rightarrow$ *)
503 Reserved Notation "E1 ==> E2" (no associativity, at level 90). 504 Reserved Notation "E1 ==> E2" (no associativity, at level 90).
504 505
505 Inductive Step : forall t, Exp t -> Exp t -> Prop := 506 Inductive Step : forall t, Exp t -> Exp t -> Prop :=
506 | Beta : forall dom ran (B : Exp1 dom ran) (X : Exp dom), 507 | Beta : forall dom ran (B : Exp1 dom ran) (X : Exp dom),
507 Val X 508 Val X
577 578
578 (** Another standard exercise in operational semantics is proving the equivalence of small-step and big-step semantics. We can carry out this exercise for our PHOAS lambda calculus. Most of the steps are just as pleasant as in the previous section, but things get complicated near to the end. 579 (** Another standard exercise in operational semantics is proving the equivalence of small-step and big-step semantics. We can carry out this exercise for our PHOAS lambda calculus. Most of the steps are just as pleasant as in the previous section, but things get complicated near to the end.
579 580
580 We must start by defining the big-step semantics itself. The definition is completely standard. *) 581 We must start by defining the big-step semantics itself. The definition is completely standard. *)
581 582
583 (** printing ===> $\Longrightarrow$ *)
582 Reserved Notation "E1 ===> E2" (no associativity, at level 90). 584 Reserved Notation "E1 ===> E2" (no associativity, at level 90).
583 585
584 Inductive BigStep : forall t, Exp t -> Exp t -> Prop := 586 Inductive BigStep : forall t, Exp t -> Exp t -> Prop :=
585 | SConst : forall n, 587 | SConst : forall n,
586 Const n ===> Const n 588 Const n ===> Const n
604 (* EX: Prove the equivalence of the small- and big-step semantics. *) 606 (* EX: Prove the equivalence of the small- and big-step semantics. *)
605 607
606 (** To prove a crucial intermediate lemma, we will want to name the transitive-reflexive closure of the small-step relation. *) 608 (** To prove a crucial intermediate lemma, we will want to name the transitive-reflexive closure of the small-step relation. *)
607 609
608 (* begin thide *) 610 (* begin thide *)
611 (** printing ==>* $\Rightarrow^*$ *)
609 Reserved Notation "E1 ==>* E2" (no associativity, at level 90). 612 Reserved Notation "E1 ==>* E2" (no associativity, at level 90).
610 613
611 Inductive MultiStep : forall t, Exp t -> Exp t -> Prop := 614 Inductive MultiStep : forall t, Exp t -> Exp t -> Prop :=
612 | Done : forall t (E : Exp t), E ==>* E 615 | Done : forall t (E : Exp t), E ==>* E
613 | OneStep : forall t (E E' E'' : Exp t), 616 | OneStep : forall t (E E' E'' : Exp t),