adamc@615: (* Copyright (c) 2009, Adam Chlipala
adamc@615:  * All rights reserved.
adamc@615:  *
adamc@615:  * Redistribution and use in source and binary forms, with or without
adamc@615:  * modification, are permitted provided that the following conditions are met:
adamc@615:  *
adamc@615:  * - Redistributions of source code must retain the above copyright notice,
adamc@615:  *   this list of conditions and the following disclaimer.
adamc@615:  * - Redistributions in binary form must reproduce the above copyright notice,
adamc@615:  *   this list of conditions and the following disclaimer in the documentation
adamc@615:  *   and/or other materials provided with the distribution.
adamc@615:  * - The names of contributors may not be used to endorse or promote products
adamc@615:  *   derived from this software without specific prior written permission.
adamc@615:  *
adamc@615:  * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@615:  * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@615:  * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@615:  * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@615:  * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
adamc@615:  * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@615:  * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@615:  * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@615:  * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@615:  * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@615:  * POSSIBILITY OF SUCH DAMAGE.
adamc@615:  *)
adamc@615: 
adamc@615: Require Import Arith List Omega TheoryList.
adamc@615: 
adamc@615: Require Import Syntax.
adamc@615: 
adamc@615: Set Implicit Arguments.
adamc@615: 
adamc@615: 
adamc@615: Section row'.
adamc@615:   Variable A : Type.
adamc@615: 
adamc@615:   Inductive row' : list name -> Type :=
adamc@615:   | Nil : row' nil
adamc@615:   | Cons : forall n ls, A -> AllS (lt n) ls -> row' ls -> row' (n :: ls).
adamc@615: End row'.
adamc@615: 
adamc@615: Implicit Arguments Nil [A].
adamc@615: 
adamc@615: Record row (A : Type) : Type := Row {
adamc@615:   keys : list name;
adamc@615:   data : row' A keys
adamc@615: }.
adamc@615: 
adamc@615: Inductive record' : forall ls, row' Set ls -> Set :=
adamc@615: | RNil : record' Nil
adamc@615: | RCons : forall n ls (T : Set) (pf : AllS (lt n) ls) r, T -> record' r -> record' (Cons T pf r).
adamc@615: 
adamc@615: Definition record (r : row Set) := record' (data r).
adamc@615: 
adamc@615: Fixpoint kDen (k : kind) : Type :=
adamc@615:   match k with
adamc@615:     | KType => Set
adamc@615:     | KName => name
adamc@615:     | KArrow k1 k2 => kDen k1 -> kDen k2
adamc@615:     | KRecord k1 => row (kDen k1)
adamc@615:   end.
adamc@615: 
adamc@615: Axiom cheat : forall T, T.
adamc@615: 
adamc@615: Fixpoint cinsert (n : name) (ls : list name) {struct ls} : list name :=
adamc@615:   match ls with
adamc@615:     | nil => n :: nil
adamc@615:     | n' :: ls' =>
adamc@615:       if eq_nat_dec n n'
adamc@615:         then ls
adamc@615:         else if le_lt_dec n n'
adamc@615:           then n :: ls
adamc@615:           else n' :: cinsert n ls'
adamc@615:   end.
adamc@615: 
adamc@615: Hint Constructors AllS.
adamc@615: Hint Extern 1 (_ < _) => omega.
adamc@615: 
adamc@615: Lemma insert_front' : forall n n',
adamc@615:   n <> n'
adamc@615:   -> n <= n'
adamc@615:   -> forall ls, AllS (lt n') ls
adamc@615:     -> AllS (lt n) ls.
adamc@615:   induction 3; auto.
adamc@615: Qed.
adamc@615: 
adamc@615: Lemma insert_front : forall n n',
adamc@615:   n <> n'
adamc@615:   -> n <= n'
adamc@615:   -> forall ls, AllS (lt n') ls
adamc@615:     -> AllS (lt n) (n' :: ls).
adamc@615:   Hint Resolve insert_front'.
adamc@615:   eauto.
adamc@615: Qed.
adamc@615: 
adamc@615: Lemma insert_continue : forall n n',
adamc@615:   n <> n'
adamc@615:   -> n' < n
adamc@615:   -> forall ls, AllS (lt n') ls
adamc@615:     -> AllS (lt n') (cinsert n ls).
adamc@615:   induction 3; simpl; auto;
adamc@615:     repeat (match goal with
adamc@615:               | [ |- context[if ?E then _ else _] ] => destruct E
adamc@615:             end; auto).
adamc@615: Qed.
adamc@615: 
adamc@615: Fixpoint insert T (n : name) (v : T) ls (r : row' T ls) {struct r} : row' T (cinsert n ls) :=
adamc@615:   match r in row' _ ls return row' T (cinsert n ls) with
adamc@615:     | Nil => Cons (n := n) v (allS_nil _) Nil
adamc@615:     | Cons n' ls' v' pf r' =>
adamc@615:       match eq_nat_dec n n' as END
adamc@615:         return row' _ (if END then _ else _) with
adamc@615:         | left _ => Cons (n := n') v' pf r'
adamc@615:         | right pfNe =>
adamc@615:           match le_lt_dec n n' as LLD
adamc@615:             return row' _ (if LLD then _ else _) with
adamc@615:             | left pfLe => Cons (n := n) v (insert_front pfNe pfLe pf) (Cons (n := n') v' pf r')
adamc@615:             | right pfLt => Cons (n := n') v' (insert_continue pfNe pfLt pf) (insert n v r')
adamc@615:           end
adamc@615:       end
adamc@615:   end.
adamc@615: 
adamc@615: Fixpoint cconcat (ls1 ls2 : list name) {struct ls1} : list name :=
adamc@615:   match ls1 with
adamc@615:     | nil => ls2
adamc@615:     | n :: ls1' => cinsert n (cconcat ls1' ls2)
adamc@615:   end.
adamc@615: 
adamc@615: Fixpoint concat T ls1 ls2 (r1 : row' T ls1) (r2 : row' T ls2) {struct r1} : row' T (cconcat ls1 ls2) :=
adamc@615:   match r1 in row' _ ls1 return row' _ (cconcat ls1 _) with
adamc@615:     | Nil => r2
adamc@615:     | Cons n _ v _ r1' => insert n v (concat r1' r2)
adamc@615:   end.
adamc@615: 
adamc@615: Fixpoint cfold T T' (f : name -> T -> T' -> T') (i : T') ls (r : row' T ls) {struct r} : T' :=
adamc@615:   match r with
adamc@615:     | Nil => i
adamc@615:     | Cons n _ v _ r' => f n v (cfold f i r')
adamc@615:   end.
adamc@615: 
adamc@615: Fixpoint cDen k (c : con kDen k) {struct c} : kDen k :=
adamc@615:   match c in con _ k return kDen k with
adamc@615:     | CVar _ x => x
adamc@615:     | Arrow c1 c2 => cDen c1 -> cDen c2
adamc@615:     | Poly _ c1 => forall x, cDen (c1 x)
adamc@615:     | CAbs _ _ c1 => fun x => cDen (c1 x)
adamc@615:     | CApp _ _ c1 c2 => (cDen c1) (cDen c2)
adamc@615:     | Name n => n
adamc@615:     | TRecord c1 => record (cDen c1)
adamc@615:     | CEmpty _ => Row Nil
adamc@615:     | CSingle _ c1 c2 => Row (Cons (n := cDen c1) (cDen c2) (allS_nil _) Nil)
adamc@615:     | CConcat _ c1 c2 => Row (concat (data (cDen c1)) (data (cDen c2)))
adamc@615:     | CFold k1 k2 => fun f i r => cfold f i (data r)
adamc@615:     | CGuarded _ _ _ _ c => cDen c
adamc@615:   end.