adam@297: (* Copyright (c) 2008-2011, Adam Chlipala
adamc@170:  * 
adamc@170:  * This work is licensed under a
adamc@170:  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@170:  * Unported License.
adamc@170:  * The license text is available at:
adamc@170:  *   http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@170:  *)
adamc@170: 
adamc@170: (* begin hide *)
adam@297: Require Import String List FunctionalExtensionality.
adamc@170: 
adam@314: Require Import CpdtTactics.
adamc@170: 
adamc@170: Set Implicit Arguments.
adamc@170: (* end hide *)
adamc@170: 
adamc@170: 
adamc@170: (** %\chapter{Type-Theoretic Interpreters}% *)
adamc@170: 
adamc@255: (** Throughout this book, we have given semantics for programming languages via executable interpreters written in Gallina.  PHOAS is quite compatible with that model, when we want to formalize many of the wide variety of interesting non-Turing-complete programming languages.  Most such languages have very straightforward elaborations into Gallina.  In this chapter, we show how to extend our past approach to higher-order languages encoded with PHOAS, and we show how simple program transformations may be proved correct with respect to these elaborative semantics. *)
adamc@170: 
adamc@170: 
adamc@170: (** * Simply-Typed Lambda Calculus *)
adamc@170: 
adamc@255: (** We begin with a copy of last chapter's encoding of the syntax of simply-typed lambda calculus with natural numbers and addition.  The primes at the ends of constructor names are gone, since here our primary subject is [exp]s instead of [Exp]s. *)
adamc@255: 
adamc@170: Module STLC.
adamc@170:   Inductive type : Type :=
adamc@170:   | Nat : type
adamc@170:   | Arrow : type -> type -> type.
adamc@170: 
adamc@170:   Infix "-->" := Arrow (right associativity, at level 60).
adamc@170: 
adamc@170:   Section vars.
adamc@170:     Variable var : type -> Type.
adamc@170: 
adamc@170:     Inductive exp : type -> Type :=
adamc@170:     | Var : forall t,
adamc@170:       var t
adamc@170:       -> exp t
adamc@170: 
adamc@170:     | Const : nat -> exp Nat
adamc@170:     | Plus : exp Nat -> exp Nat -> exp Nat
adamc@170: 
adamc@170:     | App : forall t1 t2,
adamc@170:       exp (t1 --> t2)
adamc@170:       -> exp t1
adamc@170:       -> exp t2
adamc@170:     | Abs : forall t1 t2,
adamc@170:       (var t1 -> exp t2)
adamc@170:       -> exp (t1 --> t2).
adamc@170:   End vars.
adamc@170: 
adamc@170:   Definition Exp t := forall var, exp var t.
adamc@170: 
adamc@170:   Implicit Arguments Var [var t].
adamc@170:   Implicit Arguments Const [var].
adamc@170:   Implicit Arguments Plus [var].
adamc@170:   Implicit Arguments App [var t1 t2].
adamc@170:   Implicit Arguments Abs [var t1 t2].
adamc@170: 
adamc@255:   (** The definitions that follow will be easier to read if we define some parsing notations for the constructors. *)
adamc@255: 
adamc@170:   Notation "# v" := (Var v) (at level 70).
adamc@170: 
adam@292:   (** printing ^ $\dag$ *)
adamc@170:   Notation "^ n" := (Const n) (at level 70).
adam@292:   (** printing +^ $\hat{+}$ *)
adamc@171:   Infix "+^" := Plus (left associativity, at level 79).
adamc@170: 
adamc@170:   Infix "@" := App (left associativity, at level 77).
adamc@170:   Notation "\ x , e" := (Abs (fun x => e)) (at level 78).
adamc@170:   Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78).
adamc@170: 
adamc@255:   (** A few examples will be useful for testing the functions we will write. *)
adamc@255: 
adamc@255:   Example zero : Exp Nat := fun _ => ^0.
adamc@255:   Example one : Exp Nat := fun _ => ^1.
adamc@255:   Example zpo : Exp Nat := fun _ => zero _ +^ one _.
adamc@255:   Example ident : Exp (Nat --> Nat) := fun _ => \x, #x.
adamc@255:   Example app_ident : Exp Nat := fun _ => ident _ @ zpo _.
adamc@255:   Example app : Exp ((Nat --> Nat) --> Nat --> Nat) := fun _ => \f, \x, #f @ #x.
adamc@255:   Example app_ident' : Exp Nat := fun _ => app _ @ ident _ @ zpo _.
adamc@172: 
adamc@174:   (* EX: Define an interpreter for [Exp]s. *)
adamc@174: 
adamc@174: (* begin thide *)
adamc@255:   (** To write our interpreter, we must first interpret object language types as meta language types. *)
adamc@255: 
adamc@170:   Fixpoint typeDenote (t : type) : Set :=
adamc@170:     match t with
adamc@170:       | Nat => nat
adamc@170:       | t1 --> t2 => typeDenote t1 -> typeDenote t2
adamc@170:     end.
adamc@170: 
adamc@255:   (** The crucial trick of the expression interpreter is to represent variables using the [typeDenote] function.  Due to limitations in Coq's syntax extension system, we cannot take advantage of some of our notations when they appear in patterns, so, to be consistent, in patterns we avoid notations altogether. *)
adamc@255: 
adamc@223:   Fixpoint expDenote t (e : exp typeDenote t) : typeDenote t :=
adamc@223:     match e with
adamc@170:       | Var _ v => v
adamc@170:         
adamc@170:       | Const n => n
adamc@170:       | Plus e1 e2 => expDenote e1 + expDenote e2
adamc@170:         
adamc@170:       | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
adamc@170:       | Abs _ _ e' => fun x => expDenote (e' x)
adamc@170:     end.
adamc@170: 
adamc@170:   Definition ExpDenote t (e : Exp t) := expDenote (e _).
adamc@174: (* end thide *)
adamc@170: 
adamc@255:   (** Some tests establish that [ExpDenote] produces Gallina terms like we might write manually. *)
adamc@255: 
adamc@172:   Eval compute in ExpDenote zero.
adamc@255:   (** %\vspace{-.15in}% [[
adamc@255:      = 0
adamc@255:      : typeDenote Nat
adam@302:      ]]
adam@302:      *)
adamc@255: 
adamc@172:   Eval compute in ExpDenote one.
adamc@255:   (** %\vspace{-.15in}% [[
adamc@255:      = 1
adamc@255:      : typeDenote Nat
adam@302:      ]]
adam@302:      *)
adamc@255: 
adamc@172:   Eval compute in ExpDenote zpo.
adamc@255:   (** %\vspace{-.15in}% [[
adamc@255:      = 1
adamc@255:      : typeDenote Nat
adam@302:      ]]
adam@302:      *)
adamc@255: 
adamc@172:   Eval compute in ExpDenote ident.
adamc@255:   (** %\vspace{-.15in}% [[
adamc@255:      = fun x : nat => x
adamc@255:      : typeDenote (Nat --> Nat)
adam@302:      ]]
adam@302:      *)
adamc@255: 
adamc@172:   Eval compute in ExpDenote app_ident.
adamc@255:   (** %\vspace{-.15in}% [[
adamc@255:      = 1
adamc@255:      : typeDenote Nat
adam@302:      ]]
adam@302:      *)
adamc@255: 
adamc@172:   Eval compute in ExpDenote app.
adamc@255:   (** %\vspace{-.15in}% [[
adamc@255:      = fun (x : nat -> nat) (x0 : nat) => x x0
adamc@255:      : typeDenote ((Nat --> Nat) --> Nat --> Nat)
adam@302:      ]]
adam@302:      *)
adamc@255: 
adamc@172:   Eval compute in ExpDenote app_ident'.
adamc@255:   (** %\vspace{-.15in}% [[
adamc@255:      = 1
adamc@255:      : typeDenote Nat
adam@302:      ]]
adam@302:      *)
adamc@255: 
adamc@172: 
adamc@174:   (* EX: Define a constant-folding function for [Exp]s. *)
adamc@174: 
adamc@255:   (** We can update to the higher-order case our common example of a constant folding function.  The workhorse function [cfold] is parameterized to apply to an [exp] that uses any [var] type.  An output of [cfold] uses the same [var] type as the input.  As in the definition of [expDenote], we cannot use most of our notations in patterns, but we use them freely to make the bodies of [match] cases easier to read. *)
adamc@255: 
adamc@174: (* begin thide *)
adamc@170:   Section cfold.
adamc@170:     Variable var : type -> Type.
adamc@170: 
adamc@223:     Fixpoint cfold t (e : exp var t) : exp var t :=
adamc@223:       match e with
adamc@170:         | Var _ v => #v
adamc@170: 
adamc@170:         | Const n => ^n
adamc@170:         | Plus e1 e2 =>
adamc@170:           let e1' := cfold e1 in
adamc@170:           let e2' := cfold e2 in
adamc@204:           match e1', e2' return _ with
adamc@170:             | Const n1, Const n2 => ^(n1 + n2)
adamc@171:             | _, _ => e1' +^ e2'
adamc@170:           end
adamc@170: 
adamc@170:         | App _ _ e1 e2 => cfold e1 @ cfold e2
adamc@255:         | Abs _ _ e' => \x, cfold (e' x)
adamc@170:       end.
adamc@170:   End cfold.
adamc@170: 
adamc@170:   Definition Cfold t (E : Exp t) : Exp t := fun _ => cfold (E _).
adamc@174: (* end thide *)
adamc@170: 
adamc@174:   (* EX: Prove the correctness of constant-folding. *)
adamc@174: 
adamc@255:   (** Now we would like to prove the correctness of [Cfold], which follows from a simple inductive lemma about [cfold]. *)
adamc@255: 
adamc@174: (* begin thide *)
adamc@170:   Lemma cfold_correct : forall t (e : exp _ t),
adamc@170:     expDenote (cfold e) = expDenote e.
adam@297:     induction e; crush; try (let x := fresh in extensionality x; crush);
adamc@170:       repeat (match goal with
adamc@170:                 | [ |- context[cfold ?E] ] => dep_destruct (cfold E)
adamc@170:               end; crush).
adamc@170:   Qed.
adamc@170: 
adamc@170:   Theorem Cfold_correct : forall t (E : Exp t),
adamc@170:     ExpDenote (Cfold E) = ExpDenote E.
adamc@170:     unfold ExpDenote, Cfold; intros; apply cfold_correct.
adamc@170:   Qed.
adamc@174: (* end thide *)
adamc@170: End STLC.
adamc@171: 
adamc@171: 
adamc@171: (** * Adding Products and Sums *)
adamc@171: 
adamc@255: (** The example is easily adapted to support products and sums, the basis of non-recursive datatypes in ML and Haskell. *)
adamc@255: 
adamc@171: Module PSLC.
adamc@174:   (* EX: Extend the development with products and sums. *)
adamc@174: 
adamc@174: (* begin thide *)
adamc@171:   Inductive type : Type :=
adamc@171:   | Nat : type
adamc@171:   | Arrow : type -> type -> type
adamc@171:   | Prod : type -> type -> type
adamc@171:   | Sum : type -> type -> type.
adamc@174: (* end thide *)
adamc@171: 
adamc@171:   Infix "-->" := Arrow (right associativity, at level 62).
adamc@171:   Infix "**" := Prod (right associativity, at level 61).
adamc@171:   Infix "++" := Sum (right associativity, at level 60).
adamc@171: 
adamc@174: (* begin thide *)
adamc@171:   Section vars.
adamc@171:     Variable var : type -> Type.
adamc@171: 
adamc@171:     Inductive exp : type -> Type :=
adamc@171:     | Var : forall t,
adamc@171:       var t
adamc@171:       -> exp t
adamc@171: 
adamc@171:     | Const : nat -> exp Nat
adamc@171:     | Plus : exp Nat -> exp Nat -> exp Nat
adamc@171: 
adamc@171:     | App : forall t1 t2,
adamc@171:       exp (t1 --> t2)
adamc@171:       -> exp t1
adamc@171:       -> exp t2
adamc@171:     | Abs : forall t1 t2,
adamc@171:       (var t1 -> exp t2)
adamc@171:       -> exp (t1 --> t2)
adamc@171: 
adamc@171:     | Pair : forall t1 t2,
adamc@171:       exp t1
adamc@171:       -> exp t2
adamc@171:       -> exp (t1 ** t2)
adamc@171:     | Fst : forall t1 t2,
adamc@171:       exp (t1 ** t2)
adamc@171:       -> exp t1
adamc@171:     | Snd : forall t1 t2,
adamc@171:       exp (t1 ** t2)
adamc@171:       -> exp t2
adamc@171: 
adamc@171:     | Inl : forall t1 t2,
adamc@171:       exp t1
adamc@171:       -> exp (t1 ++ t2)
adamc@171:     | Inr : forall t1 t2,
adamc@171:       exp t2
adamc@171:       -> exp (t1 ++ t2)
adamc@171:     | SumCase : forall t1 t2 t,
adamc@171:       exp (t1 ++ t2)
adamc@171:       -> (var t1 -> exp t)
adamc@171:       -> (var t2 -> exp t)
adamc@171:       -> exp t.
adamc@171:   End vars.
adamc@171: 
adamc@171:   Definition Exp t := forall var, exp var t.
adamc@174: (* end thide *)
adamc@171: 
adamc@171:   Implicit Arguments Var [var t].
adamc@171:   Implicit Arguments Const [var].
adamc@171:   Implicit Arguments Abs [var t1 t2].
adamc@171:   Implicit Arguments Inl [var t1 t2].
adamc@171:   Implicit Arguments Inr [var t1 t2].
adamc@171: 
adamc@171:   Notation "# v" := (Var v) (at level 70).
adamc@171: 
adamc@171:   Notation "^ n" := (Const n) (at level 70).
adamc@172:   Infix "+^" := Plus (left associativity, at level 78).
adamc@171: 
adamc@171:   Infix "@" := App (left associativity, at level 77).
adamc@171:   Notation "\ x , e" := (Abs (fun x => e)) (at level 78).
adamc@171:   Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78).
adamc@171: 
adamc@171:   Notation "[ e1 , e2 ]" := (Pair e1 e2).
adamc@171:   Notation "#1 e" := (Fst e) (at level 75).
adamc@171:   Notation "#2 e" := (Snd e) (at level 75).
adamc@171: 
adamc@171:   Notation "'case' e 'of' x => e1 | y => e2" := (SumCase e (fun x => e1) (fun y => e2))
adamc@171:     (at level 79).
adamc@171: 
adamc@255:   (** A few examples can be defined easily, using the notations above. *)
adamc@172: 
adamc@255:   Example swap : Exp (Nat ** Nat --> Nat ** Nat) := fun _ => \p, [#2 #p, #1 #p].
adamc@255:   Example zo : Exp (Nat ** Nat) := fun _ => [^0, ^1].
adamc@255:   Example swap_zo : Exp (Nat ** Nat) := fun _ => swap _ @ zo _.
adamc@255: 
adamc@255:   Example natOut : Exp (Nat ++ Nat --> Nat) := fun _ =>
adamc@172:     \s, case #s of x => #x | y => #y +^ #y.
adamc@255:   Example ns1 : Exp (Nat ++ Nat) := fun _ => Inl (^3).
adamc@255:   Example ns2 : Exp (Nat ++ Nat) := fun _ => Inr (^5).
adamc@255:   Example natOut_ns1 : Exp Nat := fun _ => natOut _ @ ns1 _.
adamc@255:   Example natOut_ns2 : Exp Nat := fun _ => natOut _ @ ns2 _.
adamc@255: 
adamc@255:   (** The semantics adapts without incident. *)
adamc@172: 
adamc@174: (* begin thide *)
adamc@171:   Fixpoint typeDenote (t : type) : Set :=
adamc@171:     match t with
adamc@171:       | Nat => nat
adamc@171:       | t1 --> t2 => typeDenote t1 -> typeDenote t2
adamc@171:       | t1 ** t2 => typeDenote t1 * typeDenote t2
adamc@171:       | t1 ++ t2 => typeDenote t1 + typeDenote t2
adamc@171:     end%type.
adamc@171: 
adamc@223:   Fixpoint expDenote t (e : exp typeDenote t) : typeDenote t :=
adamc@223:     match e with
adamc@171:       | Var _ v => v
adamc@171:         
adamc@171:       | Const n => n
adamc@171:       | Plus e1 e2 => expDenote e1 + expDenote e2
adamc@171:         
adamc@171:       | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
adamc@171:       | Abs _ _ e' => fun x => expDenote (e' x)
adamc@171: 
adamc@171:       | Pair _ _ e1 e2 => (expDenote e1, expDenote e2)
adamc@171:       | Fst _ _ e' => fst (expDenote e')
adamc@171:       | Snd _ _ e' => snd (expDenote e')
adamc@171: 
adamc@171:       | Inl _ _ e' => inl _ (expDenote e')
adamc@171:       | Inr _ _ e' => inr _ (expDenote e')
adamc@171:       | SumCase _ _ _ e' e1 e2 =>
adamc@171:         match expDenote e' with
adamc@171:           | inl v => expDenote (e1 v)
adamc@171:           | inr v => expDenote (e2 v)
adamc@171:         end
adamc@171:     end.
adamc@171: 
adamc@171:   Definition ExpDenote t (e : Exp t) := expDenote (e _).
adamc@174: (* end thide *)
adamc@171: 
adamc@172:   Eval compute in ExpDenote swap.
adamc@255:   (** %\vspace{-.15in}% [[
adamc@255:      = fun x : nat * nat => (let (_, y) := x in y, let (x0, _) := x in x0)
adamc@255:      : typeDenote (Nat ** Nat --> Nat ** Nat)
adam@302:      ]]
adam@302:      *)
adamc@255: 
adamc@172:   Eval compute in ExpDenote zo.
adamc@255:   (** %\vspace{-.15in}% [[
adamc@255:      = (0, 1)
adamc@255:      : typeDenote (Nat ** Nat)
adam@302:      ]]
adam@302:      *)
adamc@255: 
adamc@172:   Eval compute in ExpDenote swap_zo.
adamc@255:   (** %\vspace{-.15in}% [[
adamc@255:      = (1, 0)
adamc@255:      : typeDenote (Nat ** Nat)
adam@302:      ]]
adam@302:      *)
adamc@172: 
adamc@255:   Eval cbv beta iota delta -[plus] in ExpDenote natOut.
adamc@255:   (** %\vspace{-.15in}% [[
adamc@255:      = fun x : nat + nat => match x with
adamc@255:                             | inl v => v
adamc@255:                             | inr v => v + v
adamc@255:                             end
adamc@255:      : typeDenote (Nat ++ Nat --> Nat)
adam@302:      ]]
adam@302:      *)
adamc@255: 
adamc@172:   Eval compute in ExpDenote ns1.
adamc@255:   (** %\vspace{-.15in}% [[
adamc@255:      = inl nat 3
adamc@255:      : typeDenote (Nat ++ Nat)
adam@302:      ]]
adam@302:      *)
adamc@255: 
adamc@172:   Eval compute in ExpDenote ns2.
adamc@255:   (** %\vspace{-.15in}% [[
adamc@255:      = inr nat 5
adamc@255:      : typeDenote (Nat ++ Nat)
adam@302:      ]]
adam@302:      *)
adamc@255: 
adamc@172:   Eval compute in ExpDenote natOut_ns1.
adamc@255:   (** %\vspace{-.15in}% [[
adamc@255:      = 3
adamc@255:      : typeDenote Nat
adam@302:      ]]
adam@302:      *)
adamc@255: 
adamc@172:   Eval compute in ExpDenote natOut_ns2.
adamc@255:   (** %\vspace{-.15in}% [[
adamc@255:      = 10
adamc@255:      : typeDenote Nat
adam@302:      ]]
adam@302:      *)
adamc@255: 
adamc@255:   (** We adapt the [cfold] function using the same basic dependent-types trick that we applied in an earlier chapter to a very similar function for a language without variables. *)
adamc@172: 
adamc@174: (* begin thide *)
adamc@171:   Section cfold.
adamc@171:     Variable var : type -> Type.
adamc@171: 
adamc@172:     Definition pairOutType t :=
adamc@204:       match t return Type with
adamc@172:         | t1 ** t2 => option (exp var t1 * exp var t2)
adamc@172:         | _ => unit
adamc@172:       end.
adamc@172: 
adamc@172:     Definition pairOutDefault (t : type) : pairOutType t :=
adamc@255:       match t with
adamc@172:         | _ ** _ => None
adamc@172:         | _ => tt
adamc@172:       end.
adamc@172: 
adamc@223:     Definition pairOut t1 t2 (e : exp var (t1 ** t2))
adamc@223:       : option (exp var t1 * exp var t2) :=
adamc@172:       match e in exp _ t return pairOutType t with
adamc@172:         | Pair _ _ e1 e2 => Some (e1, e2)
adamc@172:         | _ => pairOutDefault _
adamc@172:       end.
adamc@172: 
adamc@223:     Fixpoint cfold t (e : exp var t) : exp var t :=
adamc@223:       match e with
adamc@171:         | Var _ v => #v
adamc@171: 
adamc@171:         | Const n => ^n
adamc@171:         | Plus e1 e2 =>
adamc@171:           let e1' := cfold e1 in
adamc@171:           let e2' := cfold e2 in
adamc@204:           match e1', e2' return _ with
adamc@171:             | Const n1, Const n2 => ^(n1 + n2)
adamc@171:             | _, _ => e1' +^ e2'
adamc@171:           end
adamc@171: 
adamc@171:         | App _ _ e1 e2 => cfold e1 @ cfold e2
adamc@255:         | Abs _ _ e' => \x, cfold (e' x)
adamc@171: 
adamc@171:         | Pair _ _ e1 e2 => [cfold e1, cfold e2]
adamc@172:         | Fst t1 _ e' =>
adamc@172:           let e'' := cfold e' in
adamc@172:             match pairOut e'' with
adamc@172:               | None => #1 e''
adamc@172:               | Some (e1, _) => e1
adamc@172:             end
adamc@172:         | Snd _ _ e' =>
adamc@172:           let e'' := cfold e' in
adamc@172:             match pairOut e'' with
adamc@172:               | None => #2 e''
adamc@172:               | Some (_, e2) => e2
adamc@172:             end
adamc@171: 
adamc@171:         | Inl _ _ e' => Inl (cfold e')
adamc@171:         | Inr _ _ e' => Inr (cfold e')
adamc@171:         | SumCase _ _ _ e' e1 e2 =>
adamc@171:           case cfold e' of
adamc@171:             x => cfold (e1 x)
adamc@171:           | y => cfold (e2 y)
adamc@171:       end.
adamc@171:   End cfold.
adamc@171: 
adamc@171:   Definition Cfold t (E : Exp t) : Exp t := fun _ => cfold (E _).
adamc@171: 
adamc@255:   (** The proofs are almost as straightforward as before.  We first establish two simple theorems about pairs and their projections. *)
adamc@255: 
adamc@172:   Section pairs.
adamc@172:     Variables A B : Type.
adamc@172: 
adamc@172:     Variable v1 : A.
adamc@172:     Variable v2 : B.
adamc@172:     Variable v : A * B.
adamc@172: 
adamc@172:     Theorem pair_eta1 : (v1, v2) = v -> v1 = fst v.
adamc@172:       destruct v; crush.
adamc@172:     Qed.
adamc@172: 
adamc@172:     Theorem pair_eta2 : (v1, v2) = v -> v2 = snd v.
adamc@172:       destruct v; crush.
adamc@172:     Qed.
adamc@172:   End pairs.
adamc@172: 
adamc@172:   Hint Resolve pair_eta1 pair_eta2.
adamc@172: 
adamc@255:   (** To the proof script for the main lemma, we add just one more [match] case, detecting when case analysis is appropriate on discriminees of matches over sum types. *)
adamc@255: 
adamc@171:   Lemma cfold_correct : forall t (e : exp _ t),
adamc@171:     expDenote (cfold e) = expDenote e.
adam@297:     induction e; crush; try (let x := fresh in extensionality x; crush);
adamc@171:       repeat (match goal with
adamc@171:                 | [ |- context[cfold ?E] ] => dep_destruct (cfold E)
adamc@171:                 | [ |- match ?E with inl _ => _ | inr _ => _ end = _ ] => destruct E
adamc@172:               end; crush); eauto.
adamc@171:   Qed.
adamc@171: 
adamc@171:   Theorem Cfold_correct : forall t (E : Exp t),
adamc@171:     ExpDenote (Cfold E) = ExpDenote E.
adamc@171:     unfold ExpDenote, Cfold; intros; apply cfold_correct.
adamc@171:   Qed.
adamc@174: (* end thide *)
adamc@171: End PSLC.