Mercurial > urweb
view src/coq/Semantics.v @ 948:b03d48aac959
Find more opportunities for 'let' inlining with better purity information
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Thu, 17 Sep 2009 12:55:22 -0400 |
parents | 75c7a69354d6 |
children | 705cb41ac7d0 |
line wrap: on
line source
(* Copyright (c) 2009, Adam Chlipala * All rights reserved. * * Redistribution and use in source and binary forms, with or without * modification, are permitted provided that the following conditions are met: * * - Redistributions of source code must retain the above copyright notice, * this list of conditions and the following disclaimer. * - Redistributions in binary form must reproduce the above copyright notice, * this list of conditions and the following disclaimer in the documentation * and/or other materials provided with the distribution. * - The names of contributors may not be used to endorse or promote products * derived from this software without specific prior written permission. * * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE * POSSIBILITY OF SUCH DAMAGE. *) Require Import Eqdep. Require Import Axioms. Require Import Syntax. Set Implicit Arguments. Definition row (A : Type) : Type := name -> option A. Definition record (r : row Set) := forall n, match r n with | None => unit | Some T => T end. Fixpoint kDen (k : kind) : Type := match k with | KType => Set | KName => name | KArrow k1 k2 => kDen k1 -> kDen k2 | KRecord k1 => row (kDen k1) end. Definition disjoint T (r1 r2 : row T) := forall n, match r1 n, r2 n with | Some _, Some _ => False | _, _ => True end. Fixpoint cDen k (c : con kDen k) {struct c} : kDen k := match c in con _ k return kDen k with | CVar _ x => x | Arrow c1 c2 => cDen c1 -> cDen c2 | Poly _ c1 => forall x, cDen (c1 x) | CAbs _ _ c1 => fun x => cDen (c1 x) | CApp _ _ c1 c2 => (cDen c1) (cDen c2) | Name n => n | TRecord c1 => record (cDen c1) | CEmpty _ => fun _ => None | CSingle _ c1 c2 => fun n => if name_eq_dec n (cDen c1) then Some (cDen c2) else None | CConcat _ c1 c2 => fun n => match (cDen c1) n with | None => (cDen c2) n | v => v end | CMap k1 k2 => fun f r n => match r n with | None => None | Some T => Some (f T) end | TGuarded _ c1 c2 t => disjoint (cDen c1) (cDen c2) -> cDen t end. Theorem subs_correct : forall k1 (c1 : con kDen k1) k2 (c2 : _ -> con kDen k2) c2', subs c1 c2 c2' -> cDen (c2 (cDen c1)) = cDen c2'. induction 1; simpl; intuition; try (apply ext_eq_forallS || apply ext_eq); repeat match goal with | [ H : _ |- _ ] => rewrite H end; intuition. Qed. Definition dvar k (c1 c2 : con kDen (KRecord k)) := disjoint (cDen c1) (cDen c2). Scheme deq_mut := Minimality for deq Sort Prop with disj_mut := Minimality for disj Sort Prop. Ltac deq_disj_correct scm := let t := repeat progress (simpl; intuition; subst) in let rec use_disjoint' notDone E := match goal with | [ H : disjoint _ _ |- _ ] => notDone H; generalize (H E); use_disjoint' ltac:(fun H' => match H' with | H => fail 1 | _ => notDone H' end) E | _ => idtac end in let use_disjoint := use_disjoint' ltac:(fun _ => idtac) in apply (scm _ dvar (fun k (c1 c2 : con kDen k) => cDen c1 = cDen c2) (fun k (c1 c2 : con kDen (KRecord k)) => disjoint (cDen c1) (cDen c2))); t; repeat ((unfold row; apply ext_eq) || (match goal with | [ H : _ |- _ ] => rewrite H; [] | [ H : subs _ _ _ |- _ ] => rewrite <- (subs_correct H) end); t); unfold disjoint; t; repeat (match goal with | [ |- context[match cDen ?C ?E with Some _ => _ | None => _ end] ] => use_disjoint E; destruct (cDen C E) | [ |- context[if name_eq_dec ?N1 ?N2 then _ else _] ] => use_disjoint N1; use_disjoint N2; destruct (name_eq_dec N1 N2) | [ _ : context[match cDen ?C ?E with Some _ => _ | None => _ end] |- _ ] => use_disjoint E; destruct (cDen C E) | [ |- context[if ?E then _ else _] ] => destruct E end; t). Hint Unfold dvar. Theorem deq_correct : forall k (c1 c2 : con kDen k), deq dvar c1 c2 -> cDen c1 = cDen c2. deq_disj_correct deq_mut. Qed. Theorem disj_correct : forall k (c1 c2 : con kDen (KRecord k)), disj dvar c1 c2 -> disjoint (cDen c1) (cDen c2). deq_disj_correct disj_mut. Qed. Definition tDen (t : con kDen KType) : Set := cDen t. Theorem name_eq_dec_refl : forall n, name_eq_dec n n = left _ (refl_equal n). intros; destruct (name_eq_dec n n); intuition; [ match goal with | [ e : _ = _ |- _ ] => rewrite (UIP_refl _ _ e); reflexivity end | elimtype False; tauto ]. Qed. Theorem cut_disjoint : forall n1 v r, disjoint (fun n => if name_eq_dec n n1 then Some v else None) r -> unit = match r n1 with | Some T => T | None => unit end. intros; match goal with | [ H : disjoint _ _ |- _ ] => generalize (H n1) end; rewrite name_eq_dec_refl; destruct (r n1); intuition. Qed. Implicit Arguments cut_disjoint [v r]. Fixpoint eDen t (e : exp dvar tDen t) {struct e} : tDen t := match e in exp _ _ t return tDen t with | Var _ x => x | App _ _ e1 e2 => (eDen e1) (eDen e2) | Abs _ _ e1 => fun x => eDen (e1 x) | ECApp _ c _ _ e1 Hsub => match subs_correct Hsub in _ = T return T with | refl_equal => (eDen e1) (cDen c) end | ECAbs _ _ e1 => fun X => eDen (e1 X) | Cast _ _ Heq e1 => match deq_correct Heq in _ = T return T with | refl_equal => eDen e1 end | Empty => fun _ => tt | Single c _ e1 => fun n => if name_eq_dec n (cDen c) as B return (match (match (if B then _ else _) with Some _ => if B then _ else _ | None => _ end) with Some _ => _ | None => unit end) then eDen e1 else tt | Proj c _ _ e1 => match name_eq_dec_refl (cDen c) in _ = B return (match (match (if B then _ else _) with | Some _ => if B then _ else _ | None => _ end) return Set with Some _ => _ | None => _ end) with | refl_equal => (eDen e1) (cDen c) end | Cut c _ c' Hdisj e1 => fun n => match name_eq_dec n (cDen c) as B return (match (match (if B then Some _ else None) with Some _ => if B then _ else _ | None => (cDen c') n end) with Some T => T | None => unit end -> match (cDen c') n with | None => unit | Some T => T end) with | left Heq => fun _ => match sym_eq Heq in _ = n' return match cDen c' n' return Set with Some _ => _ | None => _ end with | refl_equal => match cut_disjoint _ (disj_correct Hdisj) in _ = T return T with | refl_equal => tt end end | right _ => fun x => x end ((eDen e1) n) | Concat c1 c2 e1 e2 => fun n => match (cDen c1) n as D return match D with | None => unit | Some T => T end -> match (match D with | None => (cDen c2) n | v => v end) with | None => unit | Some T => T end with | None => fun _ => (eDen e2) n | _ => fun x => x end ((eDen e1) n) | Guarded _ _ _ _ e1 => fun pf => eDen (e1 pf) | GuardedApp _ _ _ _ e1 Hdisj => (eDen e1) (disj_correct Hdisj) end.