From 112daf37524662d6d2267d3f7e50ff3522683b8f Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Wed, 2 Mar 2011 14:25:04 -0800 Subject: [PATCH] Initial checkin of Coq-in-GHC code --- .gitignore | 2 + Makefile | 24 ++ src/Extraction-prefix.hs | 77 ++++++ src/Extraction.v | 51 ++++ src/General.v | 602 +++++++++++++++++++++++++++++++++++++++++ src/HaskCore.v | 76 ++++++ src/HaskCoreTypes.v | 58 ++++ src/HaskCoreVars.v | 18 ++ src/HaskGeneral.v | 70 +++++ src/HaskLiterals.v | 85 ++++++ src/HaskProof.v | 138 ++++++++++ src/HaskStrong.v | 62 +++++ src/HaskStrongTypes.v | 456 +++++++++++++++++++++++++++++++ src/HaskWeak.v | 169 ++++++++++++ src/Main.v | 19 ++ src/NaturalDeduction.v | 479 ++++++++++++++++++++++++++++++++ src/NaturalDeductionToLatex.v | 105 +++++++ src/Preamble.v | 142 ++++++++++ 18 files changed, 2633 insertions(+) create mode 100644 .gitignore create mode 100644 Makefile create mode 100644 src/Extraction-prefix.hs create mode 100644 src/Extraction.v create mode 100644 src/General.v create mode 100644 src/HaskCore.v create mode 100644 src/HaskCoreTypes.v create mode 100644 src/HaskCoreVars.v create mode 100644 src/HaskGeneral.v create mode 100644 src/HaskLiterals.v create mode 100644 src/HaskProof.v create mode 100644 src/HaskStrong.v create mode 100644 src/HaskStrongTypes.v create mode 100644 src/HaskWeak.v create mode 100644 src/Main.v create mode 100644 src/NaturalDeduction.v create mode 100644 src/NaturalDeductionToLatex.v create mode 100644 src/Preamble.v diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..50dd02a --- /dev/null +++ b/.gitignore @@ -0,0 +1,2 @@ +build/ +build/** diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..826866b --- /dev/null +++ b/Makefile @@ -0,0 +1,24 @@ +coqc := coqc -noglob +coqfiles := $(shell find src -name \*.v) +allfiles := $(coqfiles) $(shell find src -name \*.hs) + +default: build/CoqPass.hs + +build/CoqPass.hs: build/Makefile.coq $(allfiles) + + # first we build with -dont-load-proofs, since that runs very quickly + cd build; make -f Makefile.coq OPT="-dont-load-proofs" Main.vo + + # however the final extraction must be done without -dont-load-proofs + cd build; make -f Makefile.coq Extraction.vo + cat src/Extraction-prefix.hs build/Extraction.hs > build/CoqPass.hs + +build/Makefile.coq: $(coqfiles) + mkdir -p build + rm -f build/*.v + rm -f build/*.d + cd build; ln -s ../src/*.v . + cd build; coq_makefile *.v > Makefile.coq + +clean: + rm -rf build \ No newline at end of file diff --git a/src/Extraction-prefix.hs b/src/Extraction-prefix.hs new file mode 100644 index 0000000..68c40e5 --- /dev/null +++ b/src/Extraction-prefix.hs @@ -0,0 +1,77 @@ +{-# OPTIONS_GHC -fno-warn-unused-binds #-} +module Extraction ( coqCoreToStringPass ) +where +--import HsSyn +--import TcType +--import CoreFVs +--import CoreUtils +--import MkCore +--import Var +--import BasicTypes +--import Bag +--import VarSet +--import SrcLoc +--import Data.List + +import qualified TysWiredIn +import qualified TysPrim +import qualified Outputable +import qualified PrelNames +import qualified Name +import qualified Literal +import qualified Type +import qualified TypeRep +import qualified DataCon +import qualified TyCon +import qualified Coercion +import qualified Var +import qualified Id +import qualified FastString +import qualified BasicTypes +import qualified DataCon +import qualified CoreSyn +import qualified Class +import qualified Data.Char + +import Data.Bits ((.&.), shiftL, (.|.)) +import Prelude ( (++), (+), (==), Show, show, Char ) + +{- +nat2int :: Nat -> Prelude.Int +nat2int O = 0 +nat2int (S x) = 1 + (nat2int x) + +nat2string :: Nat -> Prelude.String +nat2string n = show (nat2int n) + +-- only needs to sanitize characters which might appear in Haskell identifiers +sanitizeForLatex :: Prelude.String -> Prelude.String +sanitizeForLatex [] = [] +sanitizeForLatex ('_':x) = "\\_"++(sanitizeForLatex x) +sanitizeForLatex ('$':x) = "\\$"++(sanitizeForLatex x) +sanitizeForLatex ('#':x) = "\\#"++(sanitizeForLatex x) +sanitizeForLatex (c:x) = c:(sanitizeForLatex x) + +coreKindToKind :: TypeRep.Kind -> Kind +coreKindToKind k = + case Coercion.splitKindFunTy_maybe k of + Prelude.Just (k1,k2) -> KindTypeFunction (coreKindToKind k1) (coreKindToKind k2) + Prelude.Nothing -> + if (Coercion.isLiftedTypeKind k) then KindType + else if (Coercion.isUnliftedTypeKind k) then KindUnliftedType + else if (Coercion.isOpenTypeKind k) then KindOpenType + else if (Coercion.isArgTypeKind k) then KindArgType + else if (Coercion.isUbxTupleKind k) then KindUnboxedTuple + else if (Coercion.isTySuperKind k) then Prelude.error "coreKindToKind got the kind-of-the-kind-of-types" + else if (Coercion.isCoSuperKind k) then Prelude.error "coreKindToKind got the kind-of-the-kind-of-coercions" + else Prelude.error ((Prelude.++) "coreKindToKind got an unknown kind: " + (Outputable.showSDoc (Outputable.ppr k))) +coreVarSort :: Var.Var -> CoreVarSort +coreVarSort v | Id.isId v = CoreExprVar (Var.varType{-AsType-} v) +coreVarSort v | Var.isTyVar v = CoreTypeVar (coreKindToKind (Var.varType v)) +coreVarSort v | Var.isCoVar v = CoreCoerVar (Coercion.coercionKind v) +coreVarSort v | otherwise = Prelude.error "Var.Var that is neither an expression variable, type variable, nor coercion variable!" + +outputableToString :: Outputable -> String +outputableToString = (\x -> Outputable.showSDoc (Outputable.ppr x)) +-} diff --git a/src/Extraction.v b/src/Extraction.v new file mode 100644 index 0000000..9e9622b --- /dev/null +++ b/src/Extraction.v @@ -0,0 +1,51 @@ +(* need this or the Haskell extraction fails *) +Set Printing Width 1300000. + +Require Import Coq.Lists.List. +Require Import Coq.Strings.Ascii. +Require Import Coq.Strings.String. +Require Import Main. +Require Import HaskCoreVars. +Require Import HaskCore. + +Open Scope string_scope. +Extraction Language Haskell. + +(* I try to reuse Haskell types mostly to get the "deriving Show" aspect *) +Extract Inductive option => "Prelude.Maybe" [ "Prelude.Just" "Prelude.Nothing" ]. +Extract Inductive list => "([])" [ "([])" "(:)" ]. +(*Extract Inductive vec => "([])" [ "([])" "(:)" ].*) +(*Extract Inductive Tree => "([])" [ "([])" "(:)" ].*) +Extract Inlined Constant map => "Prelude.map". +Extract Inductive string => "Prelude.String" [ "([])" "(:)" ]. +Extract Inductive prod => "(,)" [ "(,)" ]. +Extract Inductive sum => "Prelude.Either" [ "Prelude.Left" "Prelude.Right" ]. +Extract Inductive sumbool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ]. +Extract Inductive bool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ]. +Extract Inductive unit => "()" [ "()" ]. +Extract Inlined Constant string_dec => "(==)". +Extract Inlined Constant ascii_dec => "(==)". +Extract Inductive string => "Prelude.String" [ "[]" "(:)" ]. + +(* adapted from ExtrOcamlString.v *) +Extract Inductive ascii => "Prelude.Char" +[ +"{- If this appears, you're using Ascii internals. Please don't -} (\ b0 b1 b2 b3 b4 b5 b6 b7 -> let f b i = if b then 1 `shiftL` i else 0 in Data.Char.chr (f b0 0 .|. f b1 1 .|. f b2 2 .|. f b3 3 .|. f b4 4 .|. f b5 5 .|. f b6 6 .|. f b7 7))" +] +"{- If this appears, you're using Ascii internals. Please don't -} (\ f c -> let n = Char.code c in let h i = (n .&. (1 `shiftL` i)) /= 0 in f (h 0) (h 1) (h 2) (h 3) (h 4) (h 5) (h 6) (h 7))". +Extract Constant zero => "'\000'". +Extract Constant one => "'\001'". +Extract Constant shift => "\ b c -> Data.Char.chr (((Char.code c) `shiftL` 1) .&. 255 .|. if b then 1 else 0)". + +Unset Extraction Optimize. +Unset Extraction AutoInline. + +Definition coqCoreToStringPass (s:CoreExpr CoreVar) : string + := "FIXME". +(* +Definition coqCoreToCorePass (s:CoreExpr CoreVar) : CoreExpr CoreVar + := +*) + +Extraction "Extraction.hs" coqCoreToStringPass. + diff --git a/src/General.v b/src/General.v new file mode 100644 index 0000000..ad8e590 --- /dev/null +++ b/src/General.v @@ -0,0 +1,602 @@ +(*********************************************************************************************************************************) +(* General: general data structures *) +(*********************************************************************************************************************************) + +Require Import Coq.Unicode.Utf8. +Require Import Coq.Classes.RelationClasses. +Require Import Coq.Classes.Morphisms. +Require Import Coq.Setoids.Setoid. +Require Import Coq.Strings.String. +Require Setoid. +Require Import Coq.Lists.List. +Require Import Preamble. +Generalizable All Variables. +Require Import Omega. + + +Class EqDecidable (T:Type) := +{ eqd_type := T +; eqd_dec : forall v1 v2:T, sumbool (v1=v2) (not (v1=v2)) +; eqd_dec_reflexive : forall v, (eqd_dec v v) = (left _ (refl_equal _)) +}. +Coercion eqd_type : EqDecidable >-> Sortclass. + + +(*******************************************************************************) +(* Trees *) + +Inductive Tree (a:Type) : Type := + | T_Leaf : a -> Tree a + | T_Branch : Tree a -> Tree a -> Tree a. +Implicit Arguments T_Leaf [ a ]. +Implicit Arguments T_Branch [ a ]. + +Notation "a ,, b" := (@T_Branch _ a b) : tree_scope. + +(* tree-of-option-of-X comes up a lot, so we give it special notations *) +Notation "[ q ]" := (@T_Leaf (option _) (Some q)) : tree_scope. +Notation "[ ]" := (@T_Leaf (option _) None) : tree_scope. +Notation "[]" := (@T_Leaf (option _) None) : tree_scope. + +Open Scope tree_scope. + +Fixpoint mapTree {a b:Type}(f:a->b)(t:@Tree a) : @Tree b := + match t with + | T_Leaf x => T_Leaf (f x) + | T_Branch l r => T_Branch (mapTree f l) (mapTree f r) + end. +Fixpoint mapOptionTree {a b:Type}(f:a->b)(t:@Tree ??a) : @Tree ??b := + match t with + | T_Leaf None => T_Leaf None + | T_Leaf (Some x) => T_Leaf (Some (f x)) + | T_Branch l r => T_Branch (mapOptionTree f l) (mapOptionTree f r) + end. +Fixpoint mapTreeAndFlatten {a b:Type}(f:a->@Tree b)(t:@Tree a) : @Tree b := + match t with + | T_Leaf x => f x + | T_Branch l r => T_Branch (mapTreeAndFlatten f l) (mapTreeAndFlatten f r) + end. +Fixpoint mapOptionTreeAndFlatten {a b:Type}(f:a->@Tree ??b)(t:@Tree ??a) : @Tree ??b := + match t with + | T_Leaf None => [] + | T_Leaf (Some x) => f x + | T_Branch l r => T_Branch (mapOptionTreeAndFlatten f l) (mapOptionTreeAndFlatten f r) + end. +Fixpoint treeReduce {T:Type}{R:Type}(mapLeaf:T->R)(mergeBranches:R->R->R) (t:Tree T) := + match t with + | T_Leaf x => mapLeaf x + | T_Branch y z => mergeBranches (treeReduce mapLeaf mergeBranches y) (treeReduce mapLeaf mergeBranches z) + end. +Definition treeDecomposition {D T:Type} (mapLeaf:T->D) (mergeBranches:D->D->D) := + forall d:D, { tt:Tree T & d = treeReduce mapLeaf mergeBranches tt }. + +Lemma tree_dec_eq : + forall {Q}(t1 t2:Tree ??Q), + (forall q1 q2:Q, sumbool (q1=q2) (not (q1=q2))) -> + sumbool (t1=t2) (not (t1=t2)). + intro Q. + intro t1. + induction t1; intros. + + destruct a; destruct t2. + destruct o. + set (X q q0) as X'. + inversion X'; subst. + left; auto. + right; unfold not; intro; apply H. inversion H0; subst. auto. + right. unfold not; intro; inversion H. + right. unfold not; intro; inversion H. + destruct o. + right. unfold not; intro; inversion H. + left; auto. + right. unfold not; intro; inversion H. + + destruct t2. + right. unfold not; intro; inversion H. + set (IHt1_1 t2_1 X) as X1. + set (IHt1_2 t2_2 X) as X2. + destruct X1; destruct X2; subst. + left; auto. + + right. + unfold not; intro H. + apply n. + inversion H; auto. + + right. + unfold not; intro H. + apply n. + inversion H; auto. + + right. + unfold not; intro H. + apply n. + inversion H; auto. + Defined. + + + + +(*******************************************************************************) +(* Lists *) + +Notation "a :: b" := (cons a b) : list_scope. +Open Scope list_scope. +Fixpoint leaves {a:Type}(t:Tree (option a)) : list a := + match t with + | (T_Leaf l) => match l with + | None => nil + | Some x => x::nil + end + | (T_Branch l r) => app (leaves l) (leaves r) + end. +(* weak inverse of "leaves" *) +Fixpoint unleaves {A:Type}(l:list A) : Tree (option A) := + match l with + | nil => [] + | (a::b) => [a],,(unleaves b) + end. + +(* a map over a list and the conjunction of the results *) +Fixpoint mapProp {A:Type} (f:A->Prop) (l:list A) : Prop := + match l with + | nil => True + | (a::al) => f a /\ mapProp f al + end. + +Lemma map_id : forall A (l:list A), (map (fun x:A => x) l) = l. + induction l. + auto. + simpl. + rewrite IHl. + auto. + Defined. +Lemma map_app : forall `(f:A->B) l l', map f (app l l') = app (map f l) (map f l'). + intros. + induction l; auto. + simpl. + rewrite IHl. + auto. + Defined. +Lemma map_compose : forall A B C (f:A->B)(g:B->C)(l:list A), + (map (g ○ f) l) = (map g (map f l)). + intros. + induction l. + simpl; auto. + simpl. + rewrite IHl. + auto. + Defined. +Lemma list_cannot_be_longer_than_itself : forall `(a:A)(b:list A), b = (a::b) -> False. + intros. + induction b. + inversion H. + inversion H. apply IHb in H2. + auto. + Defined. +Lemma list_cannot_be_longer_than_itself' : forall A (b:list A) (a c:A), b = (a::c::b) -> False. + induction b. + intros; inversion H. + intros. + inversion H. + apply IHb in H2. + auto. + Defined. + +Lemma mapOptionTree_on_nil : forall `(f:A->B) h, [] = mapOptionTree f h -> h=[]. + intros. + destruct h. + destruct o. inversion H. + auto. + inversion H. + Defined. + +Lemma mapOptionTree_comp a b c (f:a->b) (g:b->c) q : (mapOptionTree g (mapOptionTree f q)) = mapOptionTree (g ○ f) q. + induction q. + destruct a0; simpl. + reflexivity. + reflexivity. + simpl. + rewrite IHq1. + rewrite IHq2. + reflexivity. + Qed. + +(* handy facts: map preserves the length of a list *) +Lemma map_on_nil : forall A B (s1:list A) (f:A->B), nil = map f s1 -> s1=nil. + intros. + induction s1. + auto. + assert False. + simpl in H. + inversion H. + inversion H0. + Defined. +Lemma map_on_singleton : forall A B (f:A->B) x (s1:list A), (cons x nil) = map f s1 -> { y : A & s1=(cons y nil) & (f y)=x }. + induction s1. + intros. + simpl in H; assert False. inversion H. inversion H0. + clear IHs1. + intros. + exists a. + simpl in H. + assert (s1=nil). + inversion H. apply map_on_nil in H2. auto. + subst. + auto. + assert (s1=nil). + inversion H. apply map_on_nil in H2. auto. + subst. + simpl in H. + inversion H. auto. + Defined. + +Lemma map_on_doubleton : forall A B (f:A->B) x y (s1:list A), ((x::y::nil) = map f s1) -> + { z : A*A & s1=((fst z)::(snd z)::nil) & (f (fst z))=x /\ (f (snd z))=y }. + intros. + destruct s1. + inversion H. + destruct s1. + inversion H. + destruct s1. + inversion H. + exists (a,a0); auto. + simpl in H. + inversion H. + Defined. + + +Lemma mapTree_compose : forall A B C (f:A->B)(g:B->C)(l:Tree A), + (mapTree (g ○ f) l) = (mapTree g (mapTree f l)). + induction l. + reflexivity. + simpl. + rewrite IHl1. + rewrite IHl2. + reflexivity. + Defined. + +Lemma lmap_compose : forall A B C (f:A->B)(g:B->C)(l:list A), + (map (g ○ f) l) = (map g (map f l)). + intros. + induction l. + simpl; auto. + simpl. + rewrite IHl. + auto. + Defined. + +(* sends a::b::c::nil to [[[[],,c],,b],,a] *) +Fixpoint unleaves' {A:Type}(l:list A) : Tree (option A) := + match l with + | nil => [] + | (a::b) => (unleaves' b),,[a] + end. + +(* sends a::b::c::nil to [[[[],,c],,b],,a] *) +Fixpoint unleaves'' {A:Type}(l:list ??A) : Tree ??A := + match l with + | nil => [] + | (a::b) => (unleaves'' b),,(T_Leaf a) + end. + +Fixpoint filter {T:Type}(l:list ??T) : list T := + match l with + | nil => nil + | (None::b) => filter b + | ((Some x)::b) => x::(filter b) + end. + +Inductive distinct {T:Type} : list T -> Prop := +| distinct_nil : distinct nil +| distinct_cons : forall a ax, (@In _ a ax -> False) -> distinct ax -> distinct (a::ax). + +Lemma map_preserves_length {A}{B}(f:A->B)(l:list A) : (length l) = (length (map f l)). + induction l; auto. + simpl. + omega. + Qed. + +(* decidable quality on a list of elements which have decidable equality *) +Definition list_eq_dec : forall {T:Type}(l1 l2:list T)(dec:forall t1 t2:T, sumbool (eq t1 t2) (not (eq t1 t2))), + sumbool (eq l1 l2) (not (eq l1 l2)). + intro T. + intro l1. + induction l1; intros. + destruct l2. + left; reflexivity. + right; intro H; inversion H. + destruct l2 as [| b l2]. + right; intro H; inversion H. + set (IHl1 l2 dec) as eqx. + destruct eqx. + subst. + set (dec a b) as eqy. + destruct eqy. + subst. + left; reflexivity. + right. intro. inversion H. subst. apply n. auto. + right. + intro. + inversion H. + apply n. + auto. + Defined. + + + + +(*******************************************************************************) +(* Length-Indexed Lists *) + +Inductive vec (A:Type) : nat -> Type := +| vec_nil : vec A 0 +| vec_cons : forall n, A -> vec A n -> vec A (S n). + +Fixpoint vec2list {n:nat}{t:Type}(v:vec t n) : list t := + match v with + | vec_nil => nil + | vec_cons n a va => a::(vec2list va) + end. + +Require Import Omega. +Definition vec_get : forall {T:Type}{l:nat}(v:vec T l)(n:nat)(pf:lt n l), T. + intro T. + intro len. + intro v. + induction v; intros. + assert False. + inversion pf. + inversion H. + rename n into len. + destruct n0 as [|n]. + exact a. + apply (IHv n). + omega. + Defined. + +Definition vec_zip {n:nat}{A B:Type}(va:vec A n)(vb:vec B n) : vec (A*B) n. + induction n. + apply vec_nil. + inversion va; subst. + inversion vb; subst. + apply vec_cons; auto. + Defined. + +Definition vec_map {n:nat}{A B:Type}(f:A->B)(v:vec A n) : vec B n. + induction n. + apply vec_nil. + inversion v; subst. + apply vec_cons; auto. + Defined. + +Fixpoint vec_In {A:Type} {n:nat} (a:A) (l:vec A n) : Prop := + match l with + | vec_nil => False + | vec_cons _ n m => (n = a) \/ vec_In a m + end. +Implicit Arguments vec_nil [ A ]. +Implicit Arguments vec_cons [ A n ]. + +Definition append_vec {n:nat}{T:Type}(v:vec T n)(t:T) : vec T (S n). + induction n. + apply (vec_cons t vec_nil). + apply vec_cons; auto. + Defined. + +Definition list2vec {T:Type}(l:list T) : vec T (length l). + induction l. + apply vec_nil. + apply vec_cons; auto. + Defined. + +Definition vec_head {n:nat}{T}(v:vec T (S n)) : T. + inversion v; auto. + Defined. +Definition vec_tail {n:nat}{T}(v:vec T (S n)) : vec T n. + inversion v; auto. + Defined. + +Lemma vec_chop {T}{l1 l2:list T}{Q}(v:vec Q (length (app l1 l2))) : vec Q (length l1). + induction l1. + apply vec_nil. + apply vec_cons. + simpl in *. + inversion v; subst; auto. + apply IHl1. + inversion v; subst; auto. + Defined. + +Lemma vec_chop' {T}{l1 l2:list T}{Q}(v:vec Q (length (app l1 l2))) : vec Q (length l2). + induction l1. + apply v. + simpl in *. + apply IHl1; clear IHl1. + inversion v; subst; auto. + Defined. + +Notation "a ::: b" := (@vec_cons _ _ a b) (at level 20). + + + +(*******************************************************************************) +(* Shaped Trees *) + +(* a ShapedTree is a tree indexed by the shape (but not the leaf values) of another tree; isomorphic to (ITree (fun _ => Q)) *) +Inductive ShapedTree {T:Type}(Q:Type) : Tree ??T -> Type := +| st_nil : @ShapedTree T Q [] +| st_leaf : forall {t}, Q -> @ShapedTree T Q [t] +| st_branch : forall {t1}{t2}, @ShapedTree T Q t1 -> @ShapedTree T Q t2 -> @ShapedTree T Q (t1,,t2). + +Fixpoint unshape {T:Type}{Q:Type}{idx:Tree ??T}(st:@ShapedTree T Q idx) : Tree ??Q := +match st with +| st_nil => [] +| st_leaf _ q => [q] +| st_branch _ _ b1 b2 => (unshape b1),,(unshape b2) +end. + +Definition mapShapedTree {T}{idx:Tree ??T}{V}{Q}(f:V->Q)(st:ShapedTree V idx) : ShapedTree Q idx. + induction st. + apply st_nil. + apply st_leaf. apply f. apply q. + apply st_branch; auto. + Defined. + +Definition zip_shapedTrees {T:Type}{Q1 Q2:Type}{idx:Tree ??T} + (st1:ShapedTree Q1 idx)(st2:ShapedTree Q2 idx) : ShapedTree (Q1*Q2) idx. + induction idx. + destruct a. + apply st_leaf; auto. + inversion st1. + inversion st2. + auto. + apply st_nil. + apply st_branch; auto. + inversion st1; subst; apply IHidx1; auto. + inversion st2; subst; auto. + inversion st2; subst; apply IHidx2; auto. + inversion st1; subst; auto. + Defined. + +Definition build_shapedTree {T:Type}(idx:Tree ??T){Q:Type}(f:T->Q) : ShapedTree Q idx. + induction idx. + destruct a. + apply st_leaf; auto. + apply st_nil. + apply st_branch; auto. + Defined. + +Lemma unshape_map : forall {Q}{b}(f:Q->b){T}{idx:Tree ??T}(t:ShapedTree Q idx), + mapOptionTree f (unshape t) = unshape (mapShapedTree f t). + intros. + induction t; auto. + simpl. + rewrite IHt1. + rewrite IHt2. + reflexivity. + Qed. + + + + +(*******************************************************************************) +(* Type-Indexed Lists *) + +(* an indexed list *) +Inductive IList (I:Type)(F:I->Type) : list I -> Type := +| INil : IList I F nil +| ICons : forall i is, F i -> IList I F is -> IList I F (i::is). +Implicit Arguments INil [ I F ]. +Implicit Arguments ICons [ I F ]. + +(* a tree indexed by a (Tree (option X)) *) +Inductive ITree (I:Type)(F:I->Type) : Tree ??I -> Type := +| INone : ITree I F [] +| ILeaf : forall i: I, F i -> ITree I F [i] +| IBranch : forall it1 it2:Tree ??I, ITree I F it1 -> ITree I F it2 -> ITree I F (it1,,it2). +Implicit Arguments INil [ I F ]. +Implicit Arguments ILeaf [ I F ]. +Implicit Arguments IBranch [ I F ]. + + + + +(*******************************************************************************) +(* Extensional equality on functions *) + +Definition extensionality := fun (t1 t2:Type) => (fun (f:t1->t2) g => forall x:t1, (f x)=(g x)). +Hint Transparent extensionality. +Instance extensionality_Equivalence : forall t1 t2, Equivalence (extensionality t1 t2). + intros; apply Build_Equivalence; + intros; compute; intros; auto. + rewrite H; rewrite H0; auto. + Defined. + Add Parametric Morphism (A B C:Type) : (fun f g => g ○ f) + with signature (extensionality A B ==> extensionality B C ==> extensionality A C) as parametric_morphism_extensionality. + unfold extensionality; intros; rewrite (H x1); rewrite (H0 (y x1)); auto. + Defined. +Lemma extensionality_composes : forall t1 t2 t3 (f f':t1->t2) (g g':t2->t3), + (extensionality _ _ f f') -> + (extensionality _ _ g g') -> + (extensionality _ _ (g ○ f) (g' ○ f')). + intros. + unfold extensionality. + unfold extensionality in H. + unfold extensionality in H0. + intros. + rewrite H. + rewrite H0. + auto. + Qed. + + + + + + +(* the Error monad *) +Inductive OrError (T:Type) := +| Error : forall error_message:string, OrError T +| OK : T -> OrError T. +Notation "??? T" := (OrError T) (at level 10). +Implicit Arguments Error [T]. +Implicit Arguments OK [T]. + +Definition orErrorBind {T:Type} (oe:OrError T) {Q:Type} (f:T -> OrError Q) := + match oe with + | Error s => Error s + | OK t => f t + end. +Notation "a >>= b" := (@orErrorBind _ a _ b) (at level 20). + +Fixpoint list2vecOrError {T}(l:list T)(n:nat) : ???(vec T n) := + match n as N return ???(vec _ N) with + | O => match l with + | nil => OK vec_nil + | _ => Error "list2vecOrError: list was too long" + end + | S n' => match l with + | nil => Error "list2vecOrError: list was too short" + | t::l' => list2vecOrError l' n' >>= fun l'' => OK (vec_cons t l'') + end + end. + +Inductive Indexed {T:Type}(f:T -> Type) : ???T -> Type := +| Indexed_Error : forall error_message:string, Indexed f (Error error_message) +| Indexed_OK : forall t, f t -> Indexed f (OK t) +. +Ltac xauto := try apply Indexed_Error; try apply Indexed_OK. + + + + + + +(* for a type with decidable equality, we can maintain lists of distinct elements *) +Section DistinctList. + Context `{V:EqDecidable}. + + Fixpoint addToDistinctList (cv:V)(cvl:list V) := + match cvl with + | nil => cv::nil + | cv'::cvl' => if eqd_dec cv cv' then cvl' else cv'::(addToDistinctList cv cvl') + end. + + Fixpoint removeFromDistinctList (cv:V)(cvl:list V) := + match cvl with + | nil => nil + | cv'::cvl' => if eqd_dec cv cv' then removeFromDistinctList cv cvl' else cv'::(removeFromDistinctList cv cvl') + end. + + Fixpoint removeFromDistinctList' (cvrem:list V)(cvl:list V) := + match cvrem with + | nil => cvl + | rem::cvrem' => removeFromDistinctList rem (removeFromDistinctList' cvrem' cvl) + end. + + Fixpoint mergeDistinctLists (cvl1:list V)(cvl2:list V) := + match cvl1 with + | nil => cvl2 + | cv'::cvl' => mergeDistinctLists cvl' (addToDistinctList cv' cvl2) + end. +End DistinctList. diff --git a/src/HaskCore.v b/src/HaskCore.v new file mode 100644 index 0000000..2242e48 --- /dev/null +++ b/src/HaskCore.v @@ -0,0 +1,76 @@ +(*********************************************************************************************************************************) +(* HaskCore: basically GHC's CoreSyn.Expr imported into Coqland *) +(*********************************************************************************************************************************) + +Generalizable All Variables. +Require Import Preamble. +Require Import General. +Require Import Coq.Strings.String. +Require Import HaskGeneral. +Require Import HaskLiterals. +Require Import HaskCoreTypes. +Require Import HaskCoreVars. + +(* this type must extract to EXACTLY match TypeRep.Type *) +Inductive CoreExpr (b:Type) := +| CoreEVar : CoreVar -> CoreExpr b +| CoreELit : HaskLiteral -> CoreExpr b +| CoreEApp : CoreExpr b -> CoreExpr b -> CoreExpr b +| CoreELam : b -> CoreExpr b -> CoreExpr b +| CoreELet : CoreBind b -> CoreExpr b -> CoreExpr b +| CoreECase : CoreExpr b -> b -> CoreType -> list (@triple AltCon (list b) (CoreExpr b)) -> CoreExpr b +| CoreECast : CoreExpr b -> CoreCoercion -> CoreExpr b +| CoreENote : Note -> CoreExpr b -> CoreExpr b +| CoreEType : CoreType -> CoreExpr b +with CoreBind (b:Type) := +| CoreNonRec : b -> CoreExpr b -> CoreBind b +| CoreRec : list (b * CoreExpr b) -> CoreBind b. +Extract Inductive CoreExpr => + "CoreSyn.Expr" [ + "CoreSyn.Var" + "CoreSyn.Lit" + "CoreSyn.App" + "CoreSyn.Lam" + "CoreSyn.Let" + "CoreSyn.Case" + "CoreSyn.Cast" + "CoreSyn.Note" + "CoreSyn.Type" ]. +Extract Inductive CoreBind => + "CoreSyn.Bind" [ "CoreSyn.NonRec" "CoreSyn.Rec" ]. + +(* extracts the Name from a CoreVar *) +Variable coreVarCoreName : CoreVar -> CoreName. Extract Inlined Constant coreVarCoreName => "Var.varName". + +Variable coretype_eq_dec : forall (c1 c2:CoreType), sumbool (eq c1 c2) (not (eq c1 c2)). + Extract Inlined Constant coretype_eq_dec => "Type.coreEqType". + +Extract Constant ArrowTyCon => "Type.funTyCon". (* Figure 7, (->) *) +Extract Constant CoFunConst => "TyCon.TyCon". Extraction Implicit CoFunConst [ 1 ]. +Extract Constant TyFunConst => "TyCon.TyCon". Extraction Implicit TyFunConst [ 1 ]. + +(*Extract Inlined Constant getDataCons => "TyCon.tyConDataCons".*) +Variable mkTyConApp : forall n, TyCon n -> list CoreType -> CoreType. + Extract Inlined Constant mkTyConApp => "Type.mkTyConApp". + +(* the magic wired-in name for the modal type introduction form *) +Variable hetmet_brak_name : CoreName. Extract Inlined Constant hetmet_brak_name => "PrelNames.hetmet_brak_name". + +(* the magic wired-in name for the modal type elimination form *) +Variable hetmet_esc_name : CoreName. Extract Inlined Constant hetmet_esc_name => "PrelNames.hetmet_esc_name". + +(* detects our crude Core-encoding of modal type introduction/elimination forms *) +Definition isBrak (ce:CoreExpr CoreVar) : ??CoreVar := +match ce with + | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody)) + => if coreName_eq hetmet_brak_name (coreVarCoreName v) then Some ec else None + | _ => None +end. +Definition isEsc (ce:CoreExpr CoreVar) : ??CoreVar := +match ce with + | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody)) + => if coreName_eq hetmet_esc_name (coreVarCoreName v) then Some ec else None + | _ => None +end. + + diff --git a/src/HaskCoreTypes.v b/src/HaskCoreTypes.v new file mode 100644 index 0000000..ec9ffcc --- /dev/null +++ b/src/HaskCoreTypes.v @@ -0,0 +1,58 @@ +(*********************************************************************************************************************************) +(* HaskCoreTypes: basically GHC's TypeRep.Type imported into Coqland *) +(*********************************************************************************************************************************) + +Generalizable All Variables. +Require Import Preamble. +Require Import General. +Require Import Coq.Strings.String. +Require Import HaskGeneral. +Require Import HaskLiterals. +Require Import HaskCoreVars. + +Variable CoreName : Type. Extract Inlined Constant CoreName => "Name.Name". +Variable coreName_eq : forall (a b:CoreName), sumbool (a=b) (not (a=b)). Extract Inlined Constant coreName_eq => "(==)". +Axiom coreName_eq_refl : ∀ v, (coreName_eq v v)=(left _ (refl_equal v)). +Instance CoreNameEqDecidable : EqDecidable CoreName := +{ eqd_dec := coreName_eq +; eqd_dec_reflexive := coreName_eq_refl +}. + +Inductive CoreIPName : Type -> Type := . Extract Inductive CoreIPName => "CoreSyn.IPName" [ ]. + +(* this exracts onto TypeRep.Type, on the nose *) +Inductive CoreType := +| TyVarTy : CoreVar -> CoreType +| AppTy : CoreType -> CoreType -> CoreType (* first arg must be AppTy or TyVarTy*) +| TyConApp : forall {n}, TyCon n -> list CoreType -> CoreType +| FunTy : CoreType -> CoreType -> CoreType (* technically redundant since we have FunTyCon *) +| ForAllTy : CoreVar -> CoreType -> CoreType +| PredTy : PredType -> CoreType +with PredType := +| ClassP : forall {n}, Class_ n -> list CoreType -> PredType +| IParam : CoreIPName CoreName -> CoreType -> PredType +| EqPred : CoreType -> CoreType -> PredType. +Extract Inductive CoreType => + "TypeRep.Type" [ "TypeRep.TyVarTy" "TypeRep.AppTy" "TypeRep.TyConApp" "TypeRep.FunTy" "TypeRep.ForAllTy" "TypeRep.PredTy" ]. +Extract Inductive PredType => + "TypeRep.PredType" [ "TypeRep.ClassP" "TypeRep.IParam" "TypeRep.EqPred" ]. + +Variable kindOfCoreType : CoreType -> Kind. Extract Inlined Constant kindOfCoreType => "(coreKindToKind . Coercion.typeKind)". + +Definition haskLiteralToCoreType lit : CoreType := + TyConApp (haskLiteralToTyCon lit) nil. + +Inductive CoreVarSort : Type := +| CoreExprVar : CoreType -> CoreVarSort +| CoreTypeVar : Kind -> CoreVarSort +| CoreCoerVar : CoreType * CoreType -> CoreVarSort. + +Variable coreVarSort : CoreVar -> CoreVarSort. Extract Inlined Constant coreVarSort => "coreVarSort". + +Variable coreTypeToString : CoreType -> string. Extract Inlined Constant coreTypeToString => "outputableToString". +Variable coreNameToString : CoreName -> string. Extract Inlined Constant coreNameToString => "outputableToString". + +Variable CoreCoercion : Type. Extract Inlined Constant CoreCoercion => "Coercion.Coercion". +Variable coreCoercionToString : CoreCoercion -> string. Extract Inlined Constant coreCoercionToString => "outputableToString". +Variable coreCoercionKind : CoreCoercion -> CoreType*CoreType. + Extract Inlined Constant coreCoercionKind => "Coercion.coercionKind". diff --git a/src/HaskCoreVars.v b/src/HaskCoreVars.v new file mode 100644 index 0000000..be64e5b --- /dev/null +++ b/src/HaskCoreVars.v @@ -0,0 +1,18 @@ +(*********************************************************************************************************************************) +(* HaskCoreVars: basically GHC's Var.Var imported into Coqland *) +(*********************************************************************************************************************************) + +Generalizable All Variables. +Require Import Preamble. +Require Import General. +Require Import HaskGeneral. + +(* GHC uses a single type for expression variables, type variables, and coercion variables; this is that type *) +Variable CoreVar : Type. Extract Inlined Constant CoreVar => "Var.Var". +Variable coreVar_eq : forall (a b:CoreVar), sumbool (a=b) (not (a=b)). Extract Inlined Constant coreVar_eq => "(==)". +Axiom coreVar_eq_refl : forall v, (coreVar_eq v v) = (left _ (refl_equal v)). +Instance CoreVarEqDecidable : EqDecidable CoreVar := +{ eqd_dec := coreVar_eq +; eqd_dec_reflexive := coreVar_eq_refl +}. + diff --git a/src/HaskGeneral.v b/src/HaskGeneral.v new file mode 100644 index 0000000..186ad1c --- /dev/null +++ b/src/HaskGeneral.v @@ -0,0 +1,70 @@ +(*********************************************************************************************************************************) +(* HaskGeneral: Definitions shared by all four representations (Core, Weak, Strong, Proof) *) +(*********************************************************************************************************************************) + +Generalizable All Variables. +Require Import Preamble. +Require Import General. +Require Import Coq.Strings.String. +Open Scope nat_scope. + +(* all Figure references are to the System FC1 paper *) + +(* Figure 1: production T; index is the number of type constructors *) +Variable TyCon : nat -> Type. Extract Inlined Constant TyCon => "TyCon.TyCon". + +(* Figure 1: production "K" *) +Variable DataCon : ∀n, TyCon n + -> nat (* number of existential tyvars associated with this datacon *) + -> nat (* number of coercion variables associated with this datacon *) + -> nat (* number of value variables (fields) associated with this datacon *) + -> Type. Extract Inlined Constant DataCon => "DataCon.DataCon". + +Variable CoFunConst : nat -> Type. (* production "C"; extracts to TyCon.TyCon *) +Variable TyFunConst : nat -> Type. (* production "Sn"; extracts to TyCon.TyCon *) + +(* magic TyCons *) +Variable ArrowTyCon : TyCon 2. (* the TyCon for (->), the regular old function-space type constructor *) +Variable CoercionTyCon : TyCon 2. (* the TyCon for (+>), the coercion type constructor *) +Variable hetMetCodeTypeTyCon : TyCon 2. Extract Inlined Constant hetMetCodeTypeTyCon => "TysWiredIn.hetMetCodeTypeTyCon". +Variable Class_ : nat -> Type. Extract Inlined Constant Class_ => "Class.Class". +Variable classTyCon : ∀ n, Class_ n -> TyCon n. Extract Inlined Constant classTyCon => "Class.classTyCon". +Variable Note : Type. Extract Inlined Constant Note => "CoreSyn.Note". +Implicit Arguments DataCon [ [n] ]. + +(* Figure 7: production κ, ι *) +Inductive Kind : Type := + | KindType : Kind (* ★ - the kind of boxed types*) + | KindTypeFunction : Kind -> Kind -> Kind (* ⇛ *) + | KindUnliftedType : Kind (* not in the paper - this is the kind of unboxed non-tuple types *) + | KindUnboxedTuple : Kind (* not in the paper - this is the kind of unboxed tuples *) + | KindArgType : Kind (* not in the paper - this is the lub of KindType and KindUnliftedType *) + | KindOpenType : Kind (* not in the paper - kind of all types (lifted, boxed, whatever) *). + +Notation "'★'" := KindType. +Notation "a ⇛ b" := (KindTypeFunction a b). + +Variable tyConToString : forall n, TyCon n -> string. Extract Inlined Constant tyConToString => "outputableToString". +Variable tyFunToString : ∀ n, TyFunConst n -> string. Extract Inlined Constant tyFunToString => "outputableToString". +Variable coFunToString : ∀ n, CoFunConst n -> string. Extract Inlined Constant coFunToString => "outputableToString". +Variable natTostring : nat->string. Extract Inlined Constant natTostring => "natTostring". + + +Axiom tycons_distinct : ~(ArrowTyCon=hetMetCodeTypeTyCon). +(* GHC provides decision procedures for equality on its primitive types; we tell Coq to blindly trust them *) +Variable tyCon_eq : forall {k}(n1 n2:TyCon k), sumbool (n1=n2) (not (n1=n2)). + Extract Inlined Constant tyCon_eq => "(==)". +Variable dataCon_eq : forall {n}{tc:TyCon n}{q}{r}{s}(n1 n2:DataCon tc q r s), sumbool (n1=n2) (not (n1=n2)). + Extract Inlined Constant dataCon_eq => "(==)". +Axiom tyCon_eq_reflexive : forall `(tc:TyCon n), (tyCon_eq tc tc) = (left _ (refl_equal tc)). +Axiom dataCon_eq_reflexive : forall `(tc:@DataCon y z q r p) , (dataCon_eq tc tc) = (left _ (refl_equal tc)). + +Instance TyConEqDecidable {n} : EqDecidable (TyCon n) := +{ eqd_dec := tyCon_eq +; eqd_dec_reflexive := tyCon_eq_reflexive +}. + +Instance DataConEqDecidable {n}{tc:TyCon n}{a}{b}{c} : EqDecidable (@DataCon _ tc a b c) := +{ eqd_dec := dataCon_eq +; eqd_dec_reflexive := dataCon_eq_reflexive +}. diff --git a/src/HaskLiterals.v b/src/HaskLiterals.v new file mode 100644 index 0000000..f41bcfb --- /dev/null +++ b/src/HaskLiterals.v @@ -0,0 +1,85 @@ +(*********************************************************************************************************************************) +(* HaskLiterals: representation of compile-time constants (literals) *) +(*********************************************************************************************************************************) + +Generalizable All Variables. +Require Import Preamble. +Require Import General. +Require Import Coq.Strings.String. +Require Import HaskGeneral. + +(* Since GHC is written in Haskell, compile-time Haskell constants are represented using Haskell (Prelude) types *) +Variable HaskInt : Type. Extract Inlined Constant HaskInt => "Prelude.Int". +Variable HaskChar : Type. Extract Inlined Constant HaskChar => "Prelude.Char". +Variable HaskFastString : Type. Extract Inlined Constant HaskFastString => "FastString.FastString". +Variable HaskInteger : Type. Extract Inlined Constant HaskInteger => "Prelude.Integer". +Variable HaskRational : Type. Extract Inlined Constant HaskRational => "Prelude.Rational". + +(* This type extracts exactly onto GHC's Literal.Literal type *) +Inductive HaskLiteral := +| HaskMachChar : HaskChar -> HaskLiteral +| HaskMachStr : HaskFastString -> HaskLiteral +| HaskMachNullAddr : HaskLiteral +| HaskMachInt : HaskInteger -> HaskLiteral +| HaskMachInt64 : HaskInteger -> HaskLiteral +| HaskMachWord : HaskInteger -> HaskLiteral +| HaskMachWord64 : HaskInteger -> HaskLiteral +| HaskMachFloat : HaskRational -> HaskLiteral +| HaskMachDouble : HaskRational -> HaskLiteral +| HaskMachLabel : HaskFastString -> option HaskInt -> HaskFunctionOrData -> HaskLiteral +with HaskFunctionOrData : Type := HaskIsFunction | HaskIsData. + +Extract Inductive HaskLiteral => "Literal.Literal" + [ "Literal.MachChar" + "Literal.MachStr" + "Literal.MachNullAddr" + "Literal.MachInt" + "Literal.MachInt64" + "Literal.MachWord" + "Literal.MachWord64" + "Literal.MachFloat" + "Literal.MachDouble" + "Literal.MachLabel" ]. +Extract Inductive HaskFunctionOrData => + "BasicTypes.FunctionOrData" [ "BasicTypes.IsFunction" "BasicTypes.IsData" ]. + +(* the TyCons for each of the literals above *) +Variable addrPrimTyCon : TyCon 0. Extract Inlined Constant addrPrimTyCon => "TysPrim.addrPrimTyCon". +Variable intPrimTyCon : TyCon 0. Extract Inlined Constant intPrimTyCon => "TysPrim.intPrimTyCon". +Variable wordPrimTyCon : TyCon 0. Extract Inlined Constant wordPrimTyCon => "TysPrim.wordPrimTyCon". +Variable int64PrimTyCon : TyCon 0. Extract Inlined Constant int64PrimTyCon => "TysPrim.int64PrimTyCon". +Variable word64PrimTyCon : TyCon 0. Extract Inlined Constant word64PrimTyCon => "TysPrim.word64PrimTyCon". +Variable floatPrimTyCon : TyCon 0. Extract Inlined Constant floatPrimTyCon => "TysPrim.floatPrimTyCon". +Variable doublePrimTyCon : TyCon 0. Extract Inlined Constant doublePrimTyCon => "TysPrim.doublePrimTyCon". +Variable charPrimTyCon : TyCon 0. Extract Inlined Constant charPrimTyCon => "TysPrim.charPrimTyCon". + +(* retrieves the TyCon for a given Literal *) +Definition haskLiteralToTyCon (lit:HaskLiteral) : TyCon 0 := +match lit with + | HaskMachNullAddr => addrPrimTyCon + | HaskMachChar _ => charPrimTyCon + | HaskMachStr _ => addrPrimTyCon + | HaskMachInt _ => intPrimTyCon + | HaskMachWord _ => wordPrimTyCon + | HaskMachInt64 _ => int64PrimTyCon + | HaskMachWord64 _ => word64PrimTyCon + | HaskMachFloat _ => floatPrimTyCon + | HaskMachDouble _ => doublePrimTyCon + | HaskMachLabel _ _ _ => addrPrimTyCon +end. + +Variable haskLiteralToString : HaskLiteral -> string. Extract Inlined Constant haskLiteralToString => "outputableToString". + +(* because Haskell's 3-tuples (triples) are distinct from both ((x,y),z) and (x,(y,z)), we need a new type: *) +Inductive triple {A B C:Type} := +| mkTriple : A -> B -> C -> triple. +Notation "a ** b ** c" := (mkTriple a b c) (at level 20). +Extract Inductive triple => "(,,)" [ "(,,)" ]. + +Inductive AltCon := +| DataAlt : forall {n:nat}(tc:TyCon n){m q r:nat}, @DataCon n tc m q r -> AltCon +| LitAlt : HaskLiteral -> AltCon +| DEFAULT : AltCon. +Extract Inductive AltCon => + "CoreSyn.AltCon" [ "CoreSyn.DataAlt" "CoreSyn.LitAlt" "CoreSyn.DEFAULT" ]. + diff --git a/src/HaskProof.v b/src/HaskProof.v new file mode 100644 index 0000000..87dfe2e --- /dev/null +++ b/src/HaskProof.v @@ -0,0 +1,138 @@ +(*********************************************************************************************************************************) +(* HaskProof: *) +(* *) +(* Natural Deduction proofs of the well-typedness of a Haskell term. Proofs use explicit structural rules (Gentzen-style) *) +(* and are in System FC extended with modal types indexed by Taha-Nielsen environment classifiers (λ^α) *) +(* *) +(*********************************************************************************************************************************) + +Generalizable All Variables. +Require Import Preamble. +Require Import General. +Require Import NaturalDeduction. +Require Import Coq.Strings.String. +Require Import Coq.Lists.List. +Require Import HaskGeneral. +Require Import HaskLiterals. +Require Import HaskStrongTypes. + +(* A judgment consists of an environment shape (Γ and Δ) and a pair of trees of leveled types (the antecedent and succedent) valid + * in any context of that shape. Notice that the succedent contains a tree of types rather than a single type; think + * of [ T1 |- T2 ] as asserting that a letrec with branches having types corresponding to the leaves of T2 is well-typed + * in environment T1. This subtle distinction starts to matter when we get into substructural (linear, affine, ordered, etc) + * types *) +Inductive Judg := + mkJudg : + forall Γ:TypeEnv, + forall Δ:CoercionEnv Γ, + Tree ??(LeveledHaskType Γ) -> + Tree ??(LeveledHaskType Γ) -> + Judg. + Notation "Γ > Δ > a '|-' s" := (mkJudg Γ Δ a s) (at level 52, Δ at level 50, a at level 52, s at level 50). + +(* A Uniform Judgment (UJudg) has its environment as a type index; we'll use these to distinguish proofs that have a single, + * uniform context throughout the whole proof. Such proofs are important because (1) we can do left and right context + * expansion on them (see rules RLeft and RRight) and (2) they will form the fiber categories of our fibration later on *) +Inductive UJudg (Γ:TypeEnv)(Δ:CoercionEnv Γ) := + mkUJudg : + Tree ??(LeveledHaskType Γ) -> + Tree ??(LeveledHaskType Γ) -> + UJudg Γ Δ. + Notation "Γ >> Δ > a '|-' s" := (mkUJudg Γ Δ a s) (at level 52, Δ at level 50, a at level 52, s at level 50). + Notation "'ext_tree_left'" := (fun ctx j => match j with mkUJudg t s => mkUJudg _ _ (ctx,,t) s end). + Notation "'ext_tree_right'" := (fun ctx j => match j with mkUJudg t s => mkUJudg _ _ (t,,ctx) s end). + +(* we can turn a UJudg into a Judg by simply internalizing the index *) +Definition UJudg2judg {Γ}{Δ}(ej:@UJudg Γ Δ) : Judg := + match ej with mkUJudg t s => Γ > Δ > t |- s end. + Coercion UJudg2judg : UJudg >-> Judg. + +(* information needed to define a case branch in a HaskProof *) +Record ProofCaseBranch {n}{tc:TyCon n}{Γ}{lev}{branchtype : HaskType Γ}{avars} := +{ cbi_cbi : @StrongAltConInContext n tc Γ avars +; cbri_freevars : Tree ??(LeveledHaskType Γ) +; cbri_judg := cbi_Γ cbi_cbi > cbi_Δ cbi_cbi + > (mapOptionTree weakLT' cbri_freevars),,(unleaves (vec2list (cbi_types cbi_cbi))) + |- [weakLT' (branchtype @@ lev)] +}. +Implicit Arguments ProofCaseBranch [ ]. + +(* Figure 3, production $\vdash_E$, Uniform rules *) +Inductive URule {Γ}{Δ} : Tree ??(UJudg Γ Δ) -> Tree ??(UJudg Γ Δ) -> Type := +| RCanL : ∀ t a , URule [Γ>>Δ> [],,a |- t ] [Γ>>Δ> a |- t ] +| RCanR : ∀ t a , URule [Γ>>Δ> a,,[] |- t ] [Γ>>Δ> a |- t ] +| RuCanL : ∀ t a , URule [Γ>>Δ> a |- t ] [Γ>>Δ> [],,a |- t ] +| RuCanR : ∀ t a , URule [Γ>>Δ> a |- t ] [Γ>>Δ> a,,[] |- t ] +| RAssoc : ∀ t a b c , URule [Γ>>Δ>a,,(b,,c) |- t ] [Γ>>Δ>(a,,b),,c |- t ] +| RCossa : ∀ t a b c , URule [Γ>>Δ>(a,,b),,c |- t ] [Γ>>Δ> a,,(b,,c) |- t ] +| RLeft : ∀ h c x , URule h c -> URule (mapOptionTree (ext_tree_left x) h) (mapOptionTree (ext_tree_left x) c) +| RRight : ∀ h c x , URule h c -> URule (mapOptionTree (ext_tree_right x) h) (mapOptionTree (ext_tree_right x) c) +| RExch : ∀ t a b , URule [Γ>>Δ> (b,,a) |- t ] [Γ>>Δ> (a,,b) |- t ] +| RWeak : ∀ t a , URule [Γ>>Δ> [] |- t ] [Γ>>Δ> a |- t ] +| RCont : ∀ t a , URule [Γ>>Δ> (a,,a) |- t ] [Γ>>Δ> a |- t ]. + + +(* Figure 3, production $\vdash_E$, all rules *) +Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type := + +| RURule : ∀ Γ Δ h c, @URule Γ Δ h c -> Rule (mapOptionTree UJudg2judg h) (mapOptionTree UJudg2judg c) + +(* λ^α rules *) +| RBrak : ∀ Γ Δ t v Σ l, Rule [Γ > Δ > Σ |- [t @@ (v::l) ]] [Γ > Δ > Σ |- [<[v|-t]> @@l]] +| REsc : ∀ Γ Δ t v Σ l, Rule [Γ > Δ > Σ |- [<[v|-t]> @@ l]] [Γ > Δ > Σ |- [t @@ (v::l) ]] + +(* Part of GHC, but not explicitly in System FC *) +| RNote : ∀ h c, Note -> Rule h [ c ] +| RLit : ∀ Γ Δ v l, Rule [ ] [Γ > Δ > []|- [literalType v @@ l]] + +(* SystemFC rules *) +| RVar : ∀ Γ Δ σ l, Rule [ ] [Γ>Δ> [σ@@l] |- [σ @@l]] +| RLam : ∀ Γ Δ Σ tx te l, Γ ⊢ᴛy tx : ★ -> Rule [Γ>Δ> Σ,,[tx@@l]|- [te@@l] ] [Γ>Δ> Σ |- [tx--->te @@l]] +| RCast : ∀ Γ Δ Σ σ τ γ l, Δ ⊢ᴄᴏ γ : σ ∼ τ -> Rule [Γ>Δ> Σ |- [σ@@l] ] [Γ>Δ> Σ |- [τ @@l]] +| RBindingGroup : ∀ Γ Δ Σ₁ Σ₂ τ₁ τ₂ , Rule ([Γ > Δ > Σ₁ |- τ₁ ],,[Γ > Δ > Σ₂ |- τ₂ ]) [Γ>Δ> Σ₁,,Σ₂ |- τ₁,,τ₂ ] +| RApp : ∀ Γ Δ Σ₁ Σ₂ tx te l, Rule ([Γ>Δ> Σ₁ |- [tx--->te @@l]],,[Γ>Δ> Σ₂ |- [tx@@l]]) [Γ>Δ> Σ₁,,Σ₂ |- [te @@l]] +| RLet : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l, Rule ([Γ>Δ> Σ₁,,[σ₂@@l] |- [σ₁@@l] ],,[Γ>Δ> Σ₂ |- [σ₂@@l]]) [Γ>Δ> Σ₁,,Σ₂ |- [σ₁ @@l]] +| REmptyGroup : ∀ Γ Δ , Rule [] [Γ > Δ > [] |- [] ] +| RAppT : ∀ Γ Δ Σ κ σ τ l, Γ ⊢ᴛy τ : κ -> Rule [Γ>Δ> Σ |- [HaskTAll κ σ @@l]] [Γ>Δ> Σ |- [substT σ τ @@l]] +| RAbsT : ∀ Γ Δ Σ κ σ l, + Rule [(κ::Γ)> (weakCE Δ) > mapOptionTree weakLT Σ |- [ HaskTApp (weakF σ) (FreshHaskTyVar _) @@ (weakL l)]] + [Γ>Δ > Σ |- [HaskTAll κ σ @@ l]] +| RAppCo : forall Γ Δ Σ κ σ₁ σ₂ σ γ l, Δ ⊢ᴄᴏ γ : σ₁∼σ₂ -> + Rule [Γ>Δ> Σ |- [σ₁∼∼σ₂:κ ⇒ σ@@l]] [Γ>Δ> Σ |- [σ @@l]] +| RAbsCo : ∀ Γ Δ Σ κ σ σ₁ σ₂ l, + Γ ⊢ᴛy σ₁:κ -> + Γ ⊢ᴛy σ₂:κ -> + Rule [Γ > ((σ₁∼∼∼σ₂)::Δ) > Σ |- [σ @@ l]] + [Γ > Δ > Σ |- [σ₁∼∼σ₂:κ⇒ σ @@l]] +| RLetRec : ∀ Γ Δ Σ₁ τ₁ τ₂, Rule [Γ > Δ > Σ₁,,τ₂ |- τ₁,,τ₂ ] [Γ > Δ > Σ₁ |- τ₁ ] +| RCase : forall Γ Δ lev n tc Σ avars tbranches + (alts:Tree ??(@ProofCaseBranch n tc Γ lev tbranches avars)), + Rule + ((mapOptionTree cbri_judg alts),, + [Γ > Δ > Σ |- [ caseType tc avars @@ lev ] ]) + [Γ > Δ > (mapOptionTreeAndFlatten cbri_freevars alts),,Σ |- [ tbranches @@ lev ] ] +. +Coercion RURule : URule >-> Rule. + + +(* A rule is considered "flat" if it is neither RBrak nor REsc *) +Inductive Rule_Flat : forall {h}{c}, Rule h c -> Prop := +| Flat_RURule : ∀ Γ Δ h c r , Rule_Flat (RURule Γ Δ h c r) +| Flat_RNote : ∀ x y z , Rule_Flat (RNote x y z) +| Flat_RVar : ∀ Γ Δ σ l, Rule_Flat (RVar Γ Δ σ l) +| Flat_RLam : ∀ Γ Δ Σ tx te q l, Rule_Flat (RLam Γ Δ Σ tx te q l) +| Flat_RCast : ∀ Γ Δ Σ σ τ γ q l, Rule_Flat (RCast Γ Δ Σ σ τ γ q l) +| Flat_RAbsT : ∀ Γ Σ κ σ a q , Rule_Flat (RAbsT Γ Σ κ σ a q ) +| Flat_RAppT : ∀ Γ Δ Σ κ σ τ q l, Rule_Flat (RAppT Γ Δ Σ κ σ τ q l) +| Flat_RAppCo : ∀ Γ Δ Σ κ σ₁ σ₂ σ γ q l, Rule_Flat (RAppCo Γ Δ Σ κ σ₁ σ₂ σ γ q l) +| Flat_RAbsCo : ∀ Γ Σ κ σ σ₁ σ₂ q1 q2 q3 x , Rule_Flat (RAbsCo Γ Σ κ σ σ₁ σ₂ q1 q2 q3 x ) +| Flat_RApp : ∀ Γ Δ Σ tx te p l, Rule_Flat (RApp Γ Δ Σ tx te p l) +| Flat_RLet : ∀ Γ Δ Σ σ₁ σ₂ p l, Rule_Flat (RLet Γ Δ Σ σ₁ σ₂ p l) +| Flat_RBindingGroup : ∀ q a b c d e , Rule_Flat (RBindingGroup q a b c d e) +| Flat_RCase : ∀ Σ Γ T κlen κ θ l x q, Rule_Flat (RCase Σ Γ T κlen κ θ l x q). + +(* given a proof that uses only uniform rules, we can produce a general proof *) +Definition UND_to_ND Γ Δ h c : ND (@URule Γ Δ) h c -> ND Rule (mapOptionTree UJudg2judg h) (mapOptionTree UJudg2judg c) + := @nd_map' _ (@URule Γ Δ ) _ Rule (@UJudg2judg Γ Δ ) (fun h c r => nd_rule (RURule _ _ h c r)) h c. + + diff --git a/src/HaskStrong.v b/src/HaskStrong.v new file mode 100644 index 0000000..6f0efa0 --- /dev/null +++ b/src/HaskStrong.v @@ -0,0 +1,62 @@ +(*********************************************************************************************************************************) +(* HaskStrong: a dependently-typed version of CoreSyn *) +(*********************************************************************************************************************************) + +Generalizable All Variables. +Require Import Preamble. +Require Import General. +Require Import Coq.Strings.String. +Require Import Coq.Lists.List. +Require Import HaskGeneral. +Require Import HaskLiterals. +Require Import HaskStrongTypes. + +Section HaskStrong. + + (* any type with decidable equality may be used to represent value variables *) + Context `{EQD_VV:EqDecidable VV}. + + (* a ExprCaseBranch contains all the data found in a case branch except the expression itself *) + Record ExprCaseBranch {n}{tc:TyCon n}{Γ}{atypes:vec (HaskType Γ) n} := + { cbi_sacic : @StrongAltConInContext n tc Γ atypes + ; cbi_vars : vec VV (tagNumValVars (cbi_tag cbi_sacic)) + ; cbi_varstypes := vec2list (vec_zip cbi_vars (cbi_types cbi_sacic)) + }. + Implicit Arguments ExprCaseBranch [[n][Γ]]. + Coercion cbi_sacic : ExprCaseBranch >-> StrongAltConInContext. + + Inductive Expr : forall Γ (Δ:CoercionEnv Γ), (VV -> LeveledHaskType Γ) -> LeveledHaskType Γ -> Type := + | EVar : ∀ Γ Δ ξ ev, Expr Γ Δ ξ (ξ ev) + | ELit : ∀ Γ Δ ξ lit l, Expr Γ Δ ξ (literalType lit@@l) + | EApp : ∀ Γ Δ ξ t1 t2 l, Expr Γ Δ ξ (t2--->t1 @@ l) -> Expr Γ Δ ξ (t2 @@ l) -> Expr Γ Δ ξ (t1 @@ l) + | ELam : ∀ Γ Δ ξ t1 t2 l ev, Γ ⊢ᴛy t1:★ ->Expr Γ Δ (update_ξ ξ ((ev,t1@@l)::nil)) (t2@@l) -> Expr Γ Δ ξ (t1--->t2@@l) + | ELet : ∀ Γ Δ ξ tv t l ev,Expr Γ Δ ξ (tv@@l)->Expr Γ Δ (update_ξ ξ ((ev,tv@@l)::nil))(t@@l) -> Expr Γ Δ ξ (t@@l) + | EEsc : ∀ Γ Δ ξ ec t l, Expr Γ Δ ξ (<[ ec |- t ]> @@ l) -> Expr Γ Δ ξ (t @@ (ec::l)) + | EBrak : ∀ Γ Δ ξ ec t l, Expr Γ Δ ξ (t @@ (ec::l)) -> Expr Γ Δ ξ (<[ ec |- t ]> @@ l) + | ECast : ∀ Γ Δ ξ γ t1 t2 l, Δ ⊢ᴄᴏ γ : t1 ∼ t2 -> Expr Γ Δ ξ (t1 @@ l) -> Expr Γ Δ ξ (t2 @@ l) + | ENote : ∀ Γ Δ ξ t, Note -> Expr Γ Δ ξ t -> Expr Γ Δ ξ t + | ETyApp : ∀ Γ Δ κ σ τ ξ l, Γ ⊢ᴛy τ : κ -> Expr Γ Δ ξ (HaskTAll κ σ @@ l) -> Expr Γ Δ ξ (substT σ τ @@ l) + | ECoLam : ∀ Γ Δ κ σ σ₁ σ₂ ξ l, Γ ⊢ᴛy σ₁:κ -> Γ ⊢ᴛy σ₂:κ -> Expr Γ (σ₁∼∼∼σ₂::Δ) ξ (σ @@ l) -> Expr Γ Δ ξ (σ₁∼∼σ₂ :κ ⇒ σ @@ l) + | ECoApp : ∀ Γ Δ κ γ σ₁ σ₂ σ ξ l, Δ ⊢ᴄᴏ γ : σ₁∼σ₂ -> Expr Γ Δ ξ (σ₁ ∼∼ σ₂ : κ ⇒ σ @@ l) -> Expr Γ Δ ξ (σ @@l) + | ETyLam : ∀ Γ Δ ξ κ σ l, + Expr (κ::Γ) (weakCE Δ) (weakLT○ξ) (HaskTApp (weakF σ) (FreshHaskTyVar _)@@(weakL l))-> Expr Γ Δ ξ (HaskTAll κ σ @@ l) + + | ECase : forall Γ Δ ξ l n (tc:TyCon n) atypes tbranches, + Expr Γ Δ ξ (caseType tc atypes @@ l) -> + Tree ??{ scb : ExprCaseBranch tc atypes + & Expr (cbi_Γ scb) (cbi_Δ scb) (update_ξ (weakLT'○ξ) (cbi_varstypes scb)) (weakLT' (tbranches@@l)) } -> + Expr Γ Δ ξ (tbranches @@ l) + + | ELetRec : ∀ Γ Δ ξ l τ vars, let ξ' := update_ξ ξ (map (fun x => ((fst x),(snd x @@ l))) (leaves vars)) in + ELetRecBindings Γ Δ ξ' l (mapOptionTree (@snd _ _) vars) -> + Expr Γ Δ ξ' (τ@@l) -> + Expr Γ Δ ξ (τ@@l) + + (* can't avoid having an additional inductive: it is a tree of Expr's, each of whose ξ depends on the type of the entire tree *) + with ELetRecBindings : forall Γ (Δ:CoercionEnv Γ), (VV -> LeveledHaskType Γ) -> HaskLevel Γ -> Tree ??(HaskType Γ) -> Type := + | ELR_nil : ∀ Γ Δ ξ l , ELetRecBindings Γ Δ ξ l [] + | ELR_leaf : ∀ Γ Δ ξ t l, Expr Γ Δ ξ (t @@ l) -> ELetRecBindings Γ Δ ξ l [t] + | ELR_branch : ∀ Γ Δ ξ l t1 t2, ELetRecBindings Γ Δ ξ l t1 -> ELetRecBindings Γ Δ ξ l t2 -> ELetRecBindings Γ Δ ξ l (t1,,t2) + . + +End HaskStrong. diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v new file mode 100644 index 0000000..d6c5ecc --- /dev/null +++ b/src/HaskStrongTypes.v @@ -0,0 +1,456 @@ +(*********************************************************************************************************************************) +(* HaskStrongTypes: representation of types and coercions for HaskStrong *) +(*********************************************************************************************************************************) + +Generalizable All Variables. +Require Import Preamble. +Require Import General. +Require Import Coq.Strings.String. +Require Import Coq.Lists.List. +Require Import HaskGeneral. +Require Import HaskLiterals. + +(* types prefixed with "Raw" are NOT binder-polymorphic; they have had their PHOAS parameter instantiated already *) +Section Raw. + + (* TV is the PHOAS type which stands for type variables of System FC *) + Context {TV:Type}. + + (* Figure 7: ρ, σ, τ, ν *) + Inductive RawHaskType : Type := + | TVar : TV -> RawHaskType (* a *) + | TCon : ∀n, TyCon n -> RawHaskType (* T *) + | TCoerc : Kind -> RawHaskType (* (+>) *) + | TApp : RawHaskType -> RawHaskType -> RawHaskType (* φ φ *) + | TFCApp : ∀n, TyFunConst n -> vec RawHaskType n -> RawHaskType (* S_n *) + | TAll : Kind -> (TV -> RawHaskType) -> RawHaskType (* ∀a:κ.φ *) + | TCode : RawHaskType -> RawHaskType -> RawHaskType (* from λ^α *). + + (* the "kind" of a coercion is a pair of types *) + Inductive RawCoercionKind : Type := mkRawCoercionKind : RawHaskType -> RawHaskType -> RawCoercionKind. + + Section CV. + + (* the PHOAS type which stands for coercion variables of System FC *) + Context {CV:Type}. + + (* Figure 7: γ, δ *) + Inductive RawHaskCoer : Prop := + | CoVar : CV -> RawHaskCoer (* g *) + | CoType : RawHaskType -> RawHaskCoer (* τ *) + | CoApp : RawHaskCoer -> RawHaskCoer -> RawHaskCoer (* γ γ *) + | CoAppT : RawHaskCoer -> RawHaskType -> RawHaskCoer (* γ@v *) + | CoCFApp : ∀n, CoFunConst n -> vec RawHaskCoer n -> RawHaskCoer (* C γⁿ *) + | CoTFApp : ∀n, TyFunConst n -> vec RawHaskCoer n -> RawHaskCoer (* S_n γⁿ *) + | CoAll : Kind -> (TV -> RawHaskCoer) -> RawHaskCoer (* ∀a:κ.γ *) + | CoSym : RawHaskCoer -> RawHaskCoer (* sym *) + | CoComp : RawHaskCoer -> RawHaskCoer -> RawHaskCoer (* ◯ *) + | CoLeft : RawHaskCoer -> RawHaskCoer (* left *) + | CoRight : RawHaskCoer -> RawHaskCoer (* right *). + + End CV. +End Raw. + +Implicit Arguments TCon [ [TV] [n]]. +Implicit Arguments TFCApp [ [TV] [n]]. +Implicit Arguments RawHaskType [ ]. +Implicit Arguments RawHaskCoer [ ]. +Implicit Arguments RawCoercionKind [ ]. + +Notation "t1 ---> t2" := (fun TV env => (@TApp _ (@TApp _ (@TCon TV _ ArrowTyCon) (t1 TV env)) (t2 TV env))). +Notation "φ₁ ∼∼ φ₂ : κ ⇒ φ₃" := + (fun TV env => @TApp _ (@TApp _ (@TCon _ _ ArrowTyCon) (@TApp _ (@TApp _ (@TCoerc _ κ) (φ₁ TV env)) (φ₂ TV env))) (φ₃ TV env)). + + + +(* Kind and Coercion Environments *) +(* + * In System FC, the environment consists of three components, each of + * whose well-formedness depends on all of those prior to it: + * + * 1. (TypeEnv) The list of free type variables and their kinds + * 2. (CoercionEnv) The list of free coercion variables and the pair of types between which it witnesses coercibility + * 3. (Tree ??CoreVar) The list of free value variables and the type of each one + *) + +Definition TypeEnv := list Kind. +Definition InstantiatedTypeEnv (TV:Type) (Γ:TypeEnv) := vec TV (length Γ). +Definition HaskCoercionKind (Γ:TypeEnv) := ∀ TV, InstantiatedTypeEnv TV Γ -> @RawCoercionKind TV. +Definition CoercionEnv (Γ:TypeEnv) := list (HaskCoercionKind Γ). +Definition InstantiatedCoercionEnv (TV CV:Type)(Γ:TypeEnv)(Δ:CoercionEnv Γ):= vec CV (length Δ). + + +(* A (HaskXX Γ) is an XX which is valid in environments of shape Γ; they are always PHOAS-uninstantiated *) +Definition HaskTyVar (Γ:TypeEnv) := forall TV (env:@InstantiatedTypeEnv TV Γ), TV. +Definition HaskCoVar Γ Δ := forall TV CV (env:@InstantiatedTypeEnv TV Γ)(cenv:@InstantiatedCoercionEnv TV CV Γ Δ), CV. +Definition HaskLevel (Γ:TypeEnv) := list (HaskTyVar Γ). +Definition HaskType (Γ:TypeEnv) := ∀ TV, @InstantiatedTypeEnv TV Γ -> RawHaskType TV. +Definition HaskCoercion Γ Δ := ∀ TV CV, + @InstantiatedTypeEnv TV Γ -> @InstantiatedCoercionEnv TV CV Γ Δ -> RawHaskCoer TV CV. +Inductive LeveledHaskType (Γ:TypeEnv) := mkLeveledHaskType : HaskType Γ -> HaskLevel Γ -> LeveledHaskType Γ. +Definition FreshHaskTyVar {Γ}(κ:Kind) : HaskTyVar (κ::Γ) := fun TV env => vec_head env. +Definition HaskTAll {Γ}(κ:Kind)(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV -> RawHaskType TV) : HaskType Γ + := fun TV env => TAll κ (σ TV env). +Definition HaskTApp {Γ}(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV -> RawHaskType TV)(cv:HaskTyVar Γ) : HaskType Γ + := fun TV env => σ TV env (cv TV env). +Definition HaskBrak {Γ}(v:HaskTyVar Γ)(t:HaskType Γ) : HaskType Γ := fun TV env => @TCode TV (TVar (v TV env)) (t TV env). +Definition HaskTCon {Γ}{n}(tc:TyCon n) : HaskType Γ := fun TV ite => TCon tc. +Definition HaskAppT {Γ}(t1 t2:HaskType Γ) : HaskType Γ := fun TV ite => TApp (t1 TV ite) (t2 TV ite). +Definition mkHaskCoercionKind {Γ}(t1 t2:HaskType Γ) : HaskCoercionKind Γ := + fun TV ite => mkRawCoercionKind (t1 TV ite) (t2 TV ite). + + +(* PHOAS substitution on types *) +Definition substT {Γ}(exp:forall TV (env:@InstantiatedTypeEnv TV Γ), TV -> RawHaskType TV)(v:@HaskType Γ) : @HaskType Γ + := fun TV env => + (fix flattenT (exp: RawHaskType (RawHaskType TV)) : RawHaskType TV := + match exp with + | TVar x => x + | TAll k y => TAll k (fun v => flattenT (y (TVar v))) + | TApp x y => TApp (flattenT x) (flattenT y) + | TCon n tc => TCon tc + | TCoerc k => TCoerc k + | TCode v e => TCode (flattenT v) (flattenT e) + | TFCApp n tfc lt => TFCApp tfc + ((fix flatten_vec n (expv:vec (RawHaskType (RawHaskType TV)) n) : vec (RawHaskType TV) n := + match expv in vec _ N return vec (RawHaskType TV) N with + | vec_nil => vec_nil + | x:::y => (flattenT x):::(flatten_vec _ y) + end) n lt) + end) + (exp (RawHaskType TV) (vec_map (fun tv => TVar tv) env) (v TV env)). +Notation "t @@ l" := (@mkLeveledHaskType _ t l) (at level 20). +Notation "t @@@ l" := (mapOptionTree (fun t' => t' @@ l) t) (at level 20). +Notation "'<[' a '|-' t ']>'" := (@HaskBrak _ a t). + + + + +(* A "tag" is something that distinguishes one case branch from another; it's a lot like Core's AltCon *) +Inductive Tag {n:nat}(tc:TyCon n) : Type := +| TagDefault : Tag tc +| TagLiteral : forall lit:HaskLiteral , Tag tc (* FIXME: solution is a new StrongLiteral indexed by a tycon *) +| TagDataCon : forall m q z, DataCon tc m q z -> Tag tc. + +(* the number of value variables bound in branches with the given tag *) +Definition tagNumValVars {n}{tc:TyCon n}(tag:Tag tc) : nat := + match tag with + | TagDefault => 0 + | TagLiteral lit => 0 + | TagDataCon m q z dc => z + end. + +(* the number of existential type variables bound in branches with the given tag *) +Definition tagNumExVars {n}{tc:TyCon n}(tag:Tag tc) : nat := + match tag with + | TagDefault => 0 + | TagLiteral lit => 0 + | TagDataCon m q z dc => m + end. + +(* the number of coercion variables bound in branches with the given tag *) +Definition tagNumCoVars {n}{tc:TyCon n}(tag:Tag tc) : nat := + match tag with + | TagDefault => 0 + | TagLiteral lit => 0 + | TagDataCon m q z dc => q + end. + +Definition caseType {Γ:TypeEnv}{n}(tc:TyCon n)(atypes:vec (HaskType Γ) n) := + fold_left HaskAppT (vec2list atypes) (HaskTCon(Γ:=Γ) tc). + +Record StrongAltCon {n}{tc:TyCon n}{alt:Tag tc} := +{ cb_akinds : vec Kind n +; cb_ekinds : vec Kind (tagNumExVars alt) +; cb_kinds := app (vec2list cb_akinds) (vec2list cb_ekinds) +; cb_coercions : vec (HaskType cb_kinds * HaskType cb_kinds) (tagNumCoVars alt) +; cb_types : vec (HaskType cb_kinds) (tagNumValVars alt) +}. +Implicit Arguments StrongAltCon [[n][tc]]. + + + + + + + + + + +(* FIXME: it's a mess below this point *) + + +Definition unAddKindFromInstantiatedTypeEnv {Γ:TypeEnv}{κ:Kind}{TV:Type}(ite:InstantiatedTypeEnv TV (κ::Γ)) := vec_tail ite. +Definition addKindToCoercionEnv (Γ:TypeEnv)(Δ:CoercionEnv Γ)(κ:Kind) : CoercionEnv (κ::Γ) := + map (fun f => (fun TV ite => f TV (unAddKindFromInstantiatedTypeEnv ite))) Δ. +Definition addKindToInstantiatedTypeEnv {Γ:TypeEnv}{TV:Type}(env:InstantiatedTypeEnv TV Γ)(tv:TV)(κ:Kind) + : InstantiatedTypeEnv TV (κ::Γ) := tv:::env. +Definition addKindToInstantiatedCoercionEnv {Γ:TypeEnv}{Δ}{TV CV:Type}(env:InstantiatedCoercionEnv TV CV Γ Δ)(tv:TV)(κ:Kind) + : InstantiatedCoercionEnv TV CV (κ::Γ) (addKindToCoercionEnv Γ Δ κ). + simpl. + unfold InstantiatedCoercionEnv. + unfold addKindToCoercionEnv. + simpl. + rewrite <- map_preserves_length. + apply env. + Defined. +Definition typeEnvContainsType {Γ}{TV:Type}(env:InstantiatedTypeEnv TV Γ)(tv:TV)(κ:Kind) : Prop + := @vec_In _ _ (tv,κ) (vec_zip env (list2vec Γ)). +Definition coercionEnvContainsCoercion {Γ}{Δ}{TV CV:Type}(ite:InstantiatedTypeEnv TV Γ) + (ice:InstantiatedCoercionEnv TV CV Γ Δ)(cv:CV)(ck:RawCoercionKind TV) + := @vec_In _ _ (cv,ck) (vec_zip ice (vec_map (fun f => f TV ite) (list2vec Δ))). +Definition addCoercionToCoercionEnv {Γ}(Δ:CoercionEnv Γ)(κ:HaskCoercionKind Γ) : CoercionEnv Γ := + κ::Δ. +Definition addCoercionToInstantiatedCoercionEnv {Γ}{Δ}{κ}{TV CV}(ice:InstantiatedCoercionEnv TV CV Γ Δ)(cv:CV) + : InstantiatedCoercionEnv TV CV Γ (addCoercionToCoercionEnv Δ κ). + simpl. + unfold addCoercionToCoercionEnv; simpl. + unfold InstantiatedCoercionEnv; simpl. + apply vec_cons; auto. + Defined. +Notation "env ∋ tv : κ" := (@typeEnvContainsType _ _ env tv κ). +Notation "env '+' tv : κ" := (@addKindToInstantiatedTypeEnv _ _ env tv κ). + +(* the various "weak" functions turn a HaskXX-in-Γ into a HaskXX-in-(κ::Γ) *) +Definition weakITE {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (κ::Γ)) : InstantiatedTypeEnv TV Γ := vec_tail ite. +Definition weakITE' {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (app κ Γ)) : InstantiatedTypeEnv TV Γ. + induction κ; auto. apply IHκ. inversion ite; subst. apply X0. Defined. +Definition weakCE {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (κ::Γ) := map (fun x => (fun tv ite => x tv (weakITE ite))) Δ. +Definition weakV {Γ:TypeEnv}{κ}(cv':HaskTyVar Γ) : HaskTyVar (κ::Γ) := fun TV ite => (cv' TV (weakITE ite)). +Definition weakV' {Γ:TypeEnv}{κ}(cv':HaskTyVar Γ) : HaskTyVar (app κ Γ). + induction κ; auto. apply weakV; auto. Defined. +Definition weakT {Γ:TypeEnv}{κ:Kind}(lt:HaskType Γ) : HaskType (κ::Γ) := fun TV ite => lt TV (weakITE ite). +Definition weakL {Γ}{κ}(lt:HaskLevel Γ) : HaskLevel (κ::Γ) := map weakV lt. +Definition weakT' {Γ}{κ}(lt:HaskType Γ) : HaskType (app κ Γ). + induction κ; auto. apply weakT; auto. Defined. +Definition weakT'' {Γ}{κ}(lt:HaskType Γ) : HaskType (app Γ κ). +unfold HaskType in *. +unfold InstantiatedTypeEnv in *. +intros. +apply vec_chop in X. +apply lt. +apply X. +Defined. +Definition lamer {a}{b}{c}(lt:HaskType (app (app a b) c)) : HaskType (app a (app b c)). +rewrite <- ass_app in lt. +exact lt. +Defined. +Definition weakL' {Γ}{κ}(lev:HaskLevel Γ) : HaskLevel (app κ Γ). + induction κ; auto. apply weakL; auto. Defined. +Definition weakLT {Γ}{κ}(lt:LeveledHaskType Γ) : LeveledHaskType (κ::Γ) := match lt with t @@ l => weakT t @@ weakL l end. +Definition weakLT' {Γ}{κ}(lt:LeveledHaskType Γ) : LeveledHaskType (app κ Γ) + := match lt with t @@ l => weakT' t @@ weakL' l end. +Definition weakCE' {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (app κ Γ). + induction κ; auto. apply weakCE; auto. Defined. +Definition weakICE {Γ:TypeEnv}{κ}{Δ:CoercionEnv Γ}{TV}{CV}(ice:InstantiatedCoercionEnv TV CV (κ::Γ) (weakCE Δ)) + : InstantiatedCoercionEnv TV CV Γ Δ. + intros. + unfold InstantiatedCoercionEnv; intros. + unfold InstantiatedCoercionEnv in ice. + unfold weakCE in ice. + simpl in ice. + rewrite <- map_preserves_length in ice. + apply ice. + Defined. +Definition weakICE' {Γ:TypeEnv}{κ}{Δ:CoercionEnv Γ}{TV}{CV}(ice:InstantiatedCoercionEnv TV CV (app κ Γ) (weakCE' Δ)) + : InstantiatedCoercionEnv TV CV Γ Δ. + induction κ; auto. apply IHκ. eapply weakICE. apply ice. Defined. +Definition weakCV {Γ}{Δ}{κ}(cv':HaskCoVar Γ Δ) : HaskCoVar (κ::Γ) (weakCE Δ) := + fun TV CV ite ice => (cv' TV CV (weakITE ite) (weakICE ice)). +Definition weakC {Γ}{κ}{Δ}(c:HaskCoercion Γ Δ) : HaskCoercion (κ::Γ) (weakCE Δ) := + fun TV CV ite ice => c TV CV (weakITE ite) (weakICE ice). +Definition weakF {Γ:TypeEnv}{κ:Kind}(f:forall TV (env:@InstantiatedTypeEnv TV Γ), TV -> RawHaskType TV) : + forall TV (env:@InstantiatedTypeEnv TV (κ::Γ)), TV -> RawHaskType TV + := fun TV ite tv => (f TV (weakITE ite) tv). + +(***************************************************************************************************) +(* Well-Formedness of Types and Coercions *) +(* also represents production "S_n:κ" of Γ because these can only wind up in Γ via rule (Type) *) +Inductive TypeFunctionDecl (n:nat)(tfc:TyFunConst n)(vk:vec Kind n) : Type := + mkTFD : Kind -> TypeFunctionDecl n tfc vk. + + +(* Figure 8, upper half *) +Inductive WellKinded_RawHaskType (TV:Type) + : forall Γ:TypeEnv, InstantiatedTypeEnv TV Γ -> RawHaskType TV -> Kind -> Prop := + | WFTyVar : forall Γ env κ d, + env∋d:κ -> + WellKinded_RawHaskType TV Γ env (TVar d) κ + | WFTyApp : forall Γ env κ₁ κ₂ σ₁ σ₂, + WellKinded_RawHaskType TV Γ env σ₁ (κ₁ ⇛ κ₂) -> + WellKinded_RawHaskType TV Γ env σ₂ κ₂ -> + WellKinded_RawHaskType TV Γ env (TApp σ₁ σ₂) κ₂ + | WFTyAll : forall Γ (env:InstantiatedTypeEnv TV Γ) κ σ , + (∀ a, WellKinded_RawHaskType TV _ (@addKindToInstantiatedTypeEnv _ TV env a κ) (σ a) ★ ) -> + WellKinded_RawHaskType TV _ env (TAll κ σ) ★ + | TySCon : forall Γ env n tfc lt vk ι , + @TypeFunctionDecl n tfc vk -> + ListWellKinded_RawHaskType TV Γ _ env lt vk -> + WellKinded_RawHaskType TV Γ env (TFCApp tfc lt) ι +with ListWellKinded_RawHaskType (TV:Type) + : forall (Γ:TypeEnv) n, InstantiatedTypeEnv TV Γ -> vec (RawHaskType TV) n -> vec Kind n -> Prop := + | ListWFRawHaskTypenil : forall Γ env, + ListWellKinded_RawHaskType TV Γ 0 env vec_nil vec_nil + | ListWFRawHaskTypecons : forall Γ env n t k lt lk, + WellKinded_RawHaskType TV Γ env t k -> + ListWellKinded_RawHaskType TV Γ n env lt lk -> + ListWellKinded_RawHaskType TV Γ (S n) env (t:::lt) (k:::lk). + +(* +Fixpoint kindOfRawHaskType {TV}(rht:RawHaskType Kind) : Kind := +match rht with + | TVar k => k + | TCon n tc => ̱★ (* FIXME: use the StrongAltCon *) + | TCoerc k => k ⇛ (k ⇛ (★ ⇛ ★ )) + | TApp ht1 ht2 : RawHaskType -> RawHaskType -> RawHaskType (* φ φ *) + | TFCApp : ∀n, TyFunConst n -> vec RawHaskType n -> RawHaskType (* S_n *) + | TAll : Kind -> (TV -> RawHaskType) -> RawHaskType (* ∀a:κ.φ *) + | TCode : RawHaskType -> RawHaskType -> RawHaskType (* from λ^α *). +*) +Definition WellKindedHaskType Γ (ht:HaskType Γ) κ := + forall TV env, WellKinded_RawHaskType TV Γ env (ht TV env) κ. + Notation "Γ '⊢ᴛy' σ : κ" := (WellKindedHaskType Γ σ κ). + + + +(* "decl", production for "axiom" *) +Structure AxiomDecl (n:nat)(ccon:CoFunConst n)(vk:vec Kind n){TV:Type} : Type := +{ axd_τ : vec TV n -> RawHaskType TV +; axd_σ : vec TV n -> RawHaskType TV +}. + + + + +Section WFCo. + Context {TV:Type}. + Context {CV:Type}. + + (* local notations *) + Notation "ienv '⊢ᴛy' σ : κ" := (@WellKinded_RawHaskType TV _ ienv σ κ). + Notation "env ∋ cv : t1 ∼ t2 : Γ : t" := (@coercionEnvContainsCoercion Γ _ TV CV t env cv (@mkRawCoercionKind _ t1 t2)) + (at level 20, t1 at level 99, t2 at level 99, t at level 99). + Reserved Notation "ice '⊢ᴄᴏ' γ : a '∼' b : Δ : Γ : ite" + (at level 20, γ at level 99, b at level 99, Δ at level 99, ite at level 99, Γ at level 99). + + (* Figure 8, lower half *) + Inductive WFCoercion:forall Γ (Δ:CoercionEnv Γ), + @InstantiatedTypeEnv TV Γ -> + @InstantiatedCoercionEnv TV CV Γ Δ -> + @RawHaskCoer TV CV -> @RawCoercionKind TV -> Prop :=. +(* + | CoTVar':∀ Γ Δ t e c σ τ, + (@coercionEnvContainsCoercion Γ _ TV CV t e c (@mkRawCoercionKind _ σ τ)) -> e⊢ᴄᴏ CoVar c : σ ∼ τ : Δ : Γ : t + | CoRefl :∀ Γ Δ t e τ κ, t ⊢ᴛy τ :κ -> e⊢ᴄᴏ CoType τ : τ ∼ τ : Δ :Γ: t + | Sym :∀ Γ Δ t e γ σ τ, (e⊢ᴄᴏ γ : σ ∼ τ : Δ : Γ:t) -> e⊢ᴄᴏ CoSym γ : τ ∼ σ : Δ :Γ: t + | Trans :∀ Γ Δ t e γ₁ γ₂ σ₁ σ₂ σ₃,(e⊢ᴄᴏ γ₁:σ₁∼σ₂:Δ:Γ:t) -> (e⊢ᴄᴏ γ₂:σ₂∼σ₃:Δ:Γ:t) -> e⊢ᴄᴏ CoComp γ₁ γ₂: σ₁ ∼ σ₃ : Δ :Γ: t + | Left :∀ Γ Δ t e γ σ₁ σ₂ τ₁ τ₂,(e⊢ᴄᴏ γ : TApp σ₁ σ₂ ∼ TApp τ₁ τ₂ :Δ:Γ:t ) -> e⊢ᴄᴏ CoLeft γ : σ₁ ∼ τ₁ : Δ :Γ: t + | Right :∀ Γ Δ t e γ σ₁ σ₂ τ₁ τ₂,(e⊢ᴄᴏ γ : TApp σ₁ σ₂ ∼ TApp τ₁ τ₂ :Δ:Γ:t ) -> e⊢ᴄᴏ CoRight γ : σ₂ ∼ τ₂ : Δ :Γ: t + | SComp :∀ Γ Δ t e γ n S σ τ κ, + ListWFCo Γ Δ t e γ σ τ -> t ⊢ᴛy TFCApp(n:=n) S σ : κ -> e⊢ᴄᴏ CoTFApp S γ : TFCApp S σ∼TFCApp S τ : Δ : Γ : t + | CoAx :∀ Γ Δ t e n C κ γ, forall (σ₁:vec TV n) (σ₂:vec TV n), forall (ax:@AxiomDecl n C κ TV), + ListWFCo Γ Δ t e γ (map TVar (vec2list σ₁)) (map TVar (vec2list σ₂)) -> + ListWellKinded_RawHaskType TV Γ t (map TVar (vec2list σ₁)) (vec2list κ) -> + ListWellKinded_RawHaskType TV Γ t (map TVar (vec2list σ₂)) (vec2list κ) -> + e⊢ᴄᴏ CoCFApp C γ : axd_σ _ _ _ ax σ₁ ∼ axd_τ _ _ _ ax σ₂ : Δ : Γ : t + + | WFCoAll : forall Γ Δ κ (t:InstantiatedTypeEnv TV Γ) (e:InstantiatedCoercionEnv TV CV (κ::Γ) (weakCE Δ)) γ σ τ , + (∀ a, e ⊢ᴄᴏ ( γ a) : ( σ a) ∼ ( τ a) : _ : _ : (t + a : κ)) + -> weakICE e ⊢ᴄᴏ (CoAll κ γ ) : (TAll κ σ ) ∼ (TAll κ τ ) : Δ : Γ : t + + | Comp :forall Γ Δ t e γ₁ γ₂ σ₁ σ₂ τ₁ τ₂ κ, + (t ⊢ᴛy TApp σ₁ σ₂:κ)-> + (e⊢ᴄᴏ γ₁:σ₁∼τ₁:Δ:Γ:t)-> + (e⊢ᴄᴏ γ₂:σ₂∼τ₂:Δ:Γ:t) -> + e⊢ᴄᴏ (CoApp γ₁ γ₂) : (TApp σ₁ σ₂) ∼ (TApp τ₁ τ₂) : Δ:Γ:t + + | CoInst :forall Γ Δ t e σ τ κ γ (v:∀ TV, InstantiatedTypeEnv TV Γ -> RawHaskType TV), + t ⊢ᴛy v TV t : κ -> + (e⊢ᴄᴏ γ:HaskTAll κ σ _ t ∼ HaskTAll κ τ _ t:Δ:Γ:t) -> + e⊢ᴄᴏ CoAppT γ (v TV t) : substT σ v TV t ∼substT τ v TV t : Δ : Γ : t + with ListWFCo : forall Γ (Δ:CoercionEnv Γ), + @InstantiatedTypeEnv TV Γ -> + InstantiatedCoercionEnv TV CV Γ Δ -> + list (RawHaskCoer TV CV) -> list (RawHaskType TV) -> list (RawHaskType TV) -> Prop := + | LWFCo_nil : ∀ Γ Δ t e , ListWFCo Γ Δ t e nil nil nil + | LWFCo_cons : ∀ Γ Δ t e a b c la lb lc, (e⊢ᴄᴏ a : b∼c : Δ : Γ : t )-> + ListWFCo Γ Δ t e la lb lc -> ListWFCo Γ Δ t e (a::la) (b::lb) (c::lc) + where "ice '⊢ᴄᴏ' γ : a '∼' b : Δ : Γ : ite" := (@WFCoercion Γ Δ ite ice γ (@mkRawCoercionKind _ a b)). +*) +End WFCo. + +Definition WFCCo (Γ:TypeEnv)(Δ:CoercionEnv Γ)(γ:HaskCoercion Γ Δ)(a b:HaskType Γ) := + forall {TV CV:Type}(env:@InstantiatedTypeEnv TV Γ)(cenv:InstantiatedCoercionEnv TV CV Γ Δ), + @WFCoercion _ _ Γ Δ env cenv (γ TV CV env cenv) (@mkRawCoercionKind _ (a TV env) (b TV env)). + Notation "Δ '⊢ᴄᴏ' γ : a '∼' b" := (@WFCCo _ Δ γ a b). + + Definition literalType (lit:HaskLiteral){Γ} : HaskType Γ := fun TV ite => (TCon (haskLiteralToTyCon lit)). + Notation "a ∼∼∼ b" := (mkHaskCoercionKind a b) (at level 18). + + +Fixpoint update_ξ + `{EQD_VV:EqDecidable VV}{Γ}(ξ:VV -> LeveledHaskType Γ)(vt:list (VV * LeveledHaskType Γ)) : VV -> LeveledHaskType Γ := + match vt with + | nil => ξ + | (v,τ)::tl => fun v' => if eqd_dec v v' then τ else (update_ξ ξ tl) v' + end. + + + + + + + + + + + +(* +Definition literalType (lit:Literal) : ∀ Γ, HaskType Γ := fun Γ TV ite => (TCon (literalTyCon lit)). +Definition unlev {Γ:TypeEnv}(lht:LeveledHaskType Γ) : HaskType Γ := match lht with t @@ l => t end. +Definition getlev {Γ:TypeEnv}(lht:LeveledHaskType Γ) : HaskLevel Γ := match lht with t @@ l => l end. +(* the type of the scrutinee in a case branch *) +Require Import Coq.Arith.EqNat. +Definition bump (n:nat) : {z:nat & lt z n} -> {z:nat & lt z (S n)}. + intros. + destruct H. + exists x; omega. + Defined. +Definition vecOfNats (n:nat) : vec {z:nat & lt z n} n. + induction n. + apply vec_nil. + apply vec_cons. + exists n; omega. + apply (vec_map (bump _)); auto. + Defined. +Definition var_eq_dec {Γ:TypeEnv}(hv1 hv2:HaskTyVar Γ) : sumbool (eq hv1 hv2) (not (eq hv1 hv2)). + set (hv1 _ (vecOfNats _)) as hv1'. + set (hv2 _ (vecOfNats _)) as hv2'. + destruct hv1' as [hv1_n hv1_pf]. + destruct hv2' as [hv2_n hv2_pf]. + clear hv1_pf. + clear hv2_pf. + set (eq_nat_decide hv1_n hv2_n) as dec. + destruct dec. + left. admit. + right. intro. apply n. assert (hv1_n=hv2_n). admit. rewrite H0. apply eq_nat_refl. + Defined. +(* equality on levels is decidable *) +Definition lev_eq_dec {Γ:TypeEnv}(l1 l2:HaskLevel Γ) : sumbool (eq l1 l2) (not (eq l1 l2)) + := @list_eq_dec (HaskTyVar Γ) (@var_eq_dec Γ) l1 l2. +*) + + + + + +(* just like GHC's AltCon, but using PHOAS types and coercions *) +Record StrongAltConInContext {n}{tc:TyCon n}{Γ}{atypes:vec (HaskType Γ) n} := +{ cbi_tag : Tag tc +; cbi_cb : StrongAltCon cbi_tag +; cbi_Γ : TypeEnv := app (vec2list (cb_ekinds cbi_cb)) Γ +; cbi_Δ : CoercionEnv cbi_Γ +; cbi_types : vec (LeveledHaskType (app (vec2list (cb_ekinds cbi_cb)) Γ)) (tagNumValVars cbi_tag) +}. +Implicit Arguments StrongAltConInContext [[n][Γ]]. + diff --git a/src/HaskWeak.v b/src/HaskWeak.v new file mode 100644 index 0000000..b450330 --- /dev/null +++ b/src/HaskWeak.v @@ -0,0 +1,169 @@ +(*********************************************************************************************************************************) +(* HaskWeak: a non-dependently-typed but Coq-friendly version of HaskCore *) +(*********************************************************************************************************************************) + +Generalizable All Variables. +Require Import Preamble. +Require Import General. +Require Import HaskGeneral. +Require Import HaskLiterals. +Require Import HaskCoreVars. +Require Import HaskCoreTypes. + +Inductive WeakExpr := +| WEVar : CoreVar -> WeakExpr +| WELit : HaskLiteral -> WeakExpr +| WELet : CoreVar -> WeakExpr -> WeakExpr -> WeakExpr +| WELetRec : Tree ??(CoreVar * WeakExpr) -> WeakExpr -> WeakExpr +| WECast : WeakExpr -> CoreCoercion -> WeakExpr +| WENote : Note -> WeakExpr -> WeakExpr +| WEApp : WeakExpr -> WeakExpr -> WeakExpr +| WETyApp : WeakExpr -> CoreType -> WeakExpr +| WECoApp : WeakExpr -> CoreCoercion -> WeakExpr +| WELam : CoreVar -> WeakExpr -> WeakExpr +| WETyLam : CoreVar -> WeakExpr -> WeakExpr +| WECoLam : CoreVar -> WeakExpr -> WeakExpr +| WEBrak : CoreVar -> WeakExpr -> WeakExpr +| WEEsc : CoreVar -> WeakExpr -> WeakExpr +| WECase : forall (scrutinee:WeakExpr) + (tbranches:CoreType) + {n:nat}(tc:TyCon n) + (type_params:vec CoreType n) + (alts : Tree ??(AltCon*list CoreVar*WeakExpr)), + WeakExpr. + +(* calculate the free CoreVar's in a WeakExpr *) +Fixpoint getWeakExprFreeVars (me:WeakExpr) : list CoreVar := + match me with + | WELit _ => nil + | WEVar cv => cv::nil + | WECast e co => getWeakExprFreeVars e + | WENote n e => getWeakExprFreeVars e + | WETyApp e t => getWeakExprFreeVars e + | WECoApp e co => getWeakExprFreeVars e + | WEBrak ec e => getWeakExprFreeVars e + | WEEsc ec e => getWeakExprFreeVars e + | WELet cv e1 e2 => mergeDistinctLists (getWeakExprFreeVars e1) (removeFromDistinctList cv (getWeakExprFreeVars e2)) + | WEApp e1 e2 => mergeDistinctLists (getWeakExprFreeVars e1) (getWeakExprFreeVars e2) + | WELam cv e => removeFromDistinctList cv (getWeakExprFreeVars e) + | WETyLam cv e => removeFromDistinctList cv (getWeakExprFreeVars e) + | WECoLam cv e => removeFromDistinctList cv (getWeakExprFreeVars e) + + (* the messy fixpoints below are required by Coq's termination conditions *) + | WECase scrutinee tbranches n tc type_params alts => + mergeDistinctLists (getWeakExprFreeVars scrutinee) ( + ((fix getWeakExprFreeVarsAlts (alts:Tree ??(AltCon*list CoreVar*WeakExpr)) {struct alts} : list CoreVar := + match alts with + | T_Leaf None => nil + | T_Leaf (Some (DEFAULT,_,e)) => getWeakExprFreeVars e + | T_Leaf (Some (LitAlt lit,_,e)) => getWeakExprFreeVars e + | T_Leaf (Some (DataAlt _ _ _ _ _ dc, vars,e)) => removeFromDistinctList' vars (getWeakExprFreeVars e) + | T_Branch b1 b2 => mergeDistinctLists (getWeakExprFreeVarsAlts b1) (getWeakExprFreeVarsAlts b2) + end) alts)) + | WELetRec mlr e => (fix removeVarsLetRec (mlr:Tree ??(CoreVar * WeakExpr))(cvl:list CoreVar) := + match mlr with + | T_Leaf None => cvl + | T_Leaf (Some (cv,e)) => removeFromDistinctList cv cvl + | T_Branch b1 b2 => removeVarsLetRec b1 (removeVarsLetRec b2 cvl) + end) mlr (mergeDistinctLists (getWeakExprFreeVars e) + ((fix getWeakExprFreeVarsLetRec (mlr:Tree ??(CoreVar * WeakExpr)) := + match mlr with + | T_Leaf None => nil + | T_Leaf (Some (cv,e)) => getWeakExprFreeVars e + | T_Branch b1 b2 => mergeDistinctLists (getWeakExprFreeVarsLetRec b1) (getWeakExprFreeVarsLetRec b2) + end) mlr)) + end. + +(* wrap lambdas around an expression until it has no free variables *) +Definition makeClosedExpression : WeakExpr -> WeakExpr := + fun me => (fix closeExpression (me:WeakExpr)(cvl:list CoreVar) := + match cvl with + | nil => me + | cv::cvl' => WELam cv (closeExpression me cvl') + end) me (getWeakExprFreeVars me). + +(* messy first-order capture-avoiding substitution on CoreType's *) +Fixpoint replaceCoreVar (te:CoreType)(tv:CoreVar)(tsubst:CoreType) := + match te with + | TyVarTy tv' => if eqd_dec tv tv' then tsubst else te + | AppTy t1 t2 => AppTy (replaceCoreVar t1 tv tsubst) (replaceCoreVar t2 tv tsubst) + | FunTy t1 t2 => FunTy (replaceCoreVar t1 tv tsubst) (replaceCoreVar t2 tv tsubst) + | ForAllTy tv' t => if eqd_dec tv tv' then te else ForAllTy tv' (replaceCoreVar t tv tsubst) + | PredTy (EqPred t1 t2) => PredTy (EqPred (replaceCoreVar t1 tv tsubst) (replaceCoreVar t2 tv tsubst)) + | PredTy (IParam ip ty) => PredTy (IParam ip (replaceCoreVar ty tv tsubst)) + | PredTy (ClassP _ c lt) => PredTy (ClassP c ((fix replaceCoreDistinctList (lt:list CoreType) := + match lt with + | nil => nil + | h::t => (replaceCoreVar h tv tsubst)::(replaceCoreDistinctList t) + end) lt)) + | TyConApp _ tc lt => TyConApp tc ((fix replaceCoreDistinctList (lt:list CoreType) := + match lt with + | nil => nil + | h::t => (replaceCoreVar h tv tsubst)::(replaceCoreDistinctList t) + end) lt) + end. + +(* calculate the CoreType of a WeakExpr *) +Fixpoint coreTypeOfWeakExpr (ce:WeakExpr) : ???CoreType := + match ce with + | WEVar v => match coreVarSort v with + | CoreExprVar t => OK t + | CoreTypeVar _ => Error "found tyvar in expression" + | CoreCoerVar _ => Error "found coercion variable in expression" + end + | WELit lit => OK (haskLiteralToCoreType lit) + | WEApp e1 e2 => coreTypeOfWeakExpr e1 >>= fun t' => + match t' with + | FunTy t1 t2 => OK t2 + | (TyConApp 2 tc (t1::t2::nil)) => + if (tyCon_eq tc ArrowTyCon) + then OK t2 + else Error ("found non-function type "+++(coreTypeToString t')+++" in EApp") + | _ => Error ("found non-function type "+++(coreTypeToString t')+++" in EApp") + end + | WETyApp e t => coreTypeOfWeakExpr e >>= fun te => + match te with + | ForAllTy v ct => match coreVarSort v with + | CoreExprVar _ => Error "found an expression variable inside an forall-type!" + | CoreTypeVar _ => OK (replaceCoreVar ct v t) + | CoreCoerVar _ => Error "found a coercion variable inside an forall-type!" + end + | _ => Error ("found non-forall type "+++(coreTypeToString te)+++" in ETyApp") + end + | WECoApp e co => coreTypeOfWeakExpr e >>= fun te => + match te with + | FunTy (PredTy (EqPred t1 t2)) t3 => OK t3 + | TyConApp 2 tc ((PredTy (EqPred t1 t2))::t3::nil) => + if (tyCon_eq tc ArrowTyCon) + then OK t3 + else Error ("found non-coercion type "+++(coreTypeToString te)+++" in ETyApp") + | _ => Error ("found non-coercion type "+++(coreTypeToString te)+++" in ETyApp") + end + | WELam ev e => coreTypeOfWeakExpr e >>= fun t' => match coreVarSort ev with + | CoreExprVar vt => OK (FunTy vt t') + | CoreTypeVar _ => Error "found a type variable in a WELam!" + | CoreCoerVar _ => Error "found a coercion variable in a WELam!" + end + | WETyLam tv e => coreTypeOfWeakExpr e >>= fun t' => OK (ForAllTy tv t') + | WECoLam cv e => coreTypeOfWeakExpr e >>= fun t' => match coreVarSort cv with + | CoreExprVar vt => Error "found an expression variable in a WECoLam!" + | CoreTypeVar _ => Error "found a type variable in a WECoLam!" + | CoreCoerVar (φ₁,φ₂) => OK (FunTy (PredTy (EqPred φ₁ φ₂)) t') + end + | WELet ev ve e => coreTypeOfWeakExpr e + | WELetRec rb e => coreTypeOfWeakExpr e + | WENote n e => coreTypeOfWeakExpr e + | WECast e co => OK (snd (coreCoercionKind co)) + | WECase scrutinee tbranches n tc type_params alts => OK tbranches + | WEBrak ec e => coreTypeOfWeakExpr e >>= fun t' => OK (TyConApp hetMetCodeTypeTyCon ((TyVarTy ec)::t'::nil)) + | WEEsc ec e => coreTypeOfWeakExpr e >>= fun t' => + match t' with + | (TyConApp 2 tc ((TyVarTy ec')::t''::nil)) => + if (tyCon_eq tc hetMetCodeTypeTyCon) + then if eqd_dec ec ec' then OK t'' + else Error "level mismatch in escapification" + else Error "ill-typed escapification" + | _ => Error "ill-typed escapification" + end + end. + diff --git a/src/Main.v b/src/Main.v new file mode 100644 index 0000000..99c6734 --- /dev/null +++ b/src/Main.v @@ -0,0 +1,19 @@ +Require Import Preamble. +Require Import General. + +Require Import NaturalDeduction. +Require Import NaturalDeductionToLatex. + +Require Import HaskGeneral. +Require Import HaskLiterals. +Require Import HaskCoreVars. +Require Import HaskCoreTypes. +Require Import HaskCore. +Require Import HaskWeak. +(*Require Import HaskCoreToWeak.*) +Require Import HaskStrongTypes. +Require Import HaskStrong. +(*Require Import HaskStrongToProof.*) +Require Import HaskProof. +(*Require Import HaskWeakToStrong.*) +(*Require Import HaskProofToLatex.*) diff --git a/src/NaturalDeduction.v b/src/NaturalDeduction.v new file mode 100644 index 0000000..047ab87 --- /dev/null +++ b/src/NaturalDeduction.v @@ -0,0 +1,479 @@ +(*********************************************************************************************************************************) +(* NaturalDeduction: structurally explicit proofs in Coq *) +(*********************************************************************************************************************************) + +Generalizable All Variables. +Require Import Preamble. +Require Import General. +Require Import Coq.Strings.Ascii. +Require Import Coq.Strings.String. + +(* + * IMPORTANT!!! + * + * Unlike most formalizations, this library offers TWO different ways + * to represent a natural deduction proof. To demonstrate this, + * consider the signature of the propositional calculus: + * + * Variable PropositionalVariable : Type. + * + * Inductive Formula : Prop := + * | formula_var : PropositionalVariable -> Formula (* every propositional variable is a formula *) + * | formula_and : Formula -> Formula -> Formula (* the conjunction of any two formulae is a formula *) + * | formula_or : Formula -> Formula -> Formula (* the disjunction of any two formulae is a formula *) + * + * And couple this with the theory of conjunction and disjunction: + * φ\/ψ is true if either φ is true or ψ is true, and φ/\ψ is true + * if both φ and ψ are true. + * + * 1) Structurally implicit proofs + * + * This is what you would call the "usual" representation –- it's + * what most people learn when they first start programming in Coq: + * + * Inductive IsTrue : Formula -> Prop := + * | IsTrue_or1 : forall f1 f2, IsTrue f1 -> IsTrue (formula_or f1 f2) + * | IsTrue_or2 : forall f1 f2, IsTrue f2 -> IsTrue (formula_or f1 f2) + * | IsTrue_and : forall f1 f2, IsTrue f2 -> IsTrue f2 -> IsTrue (formula_and f1 f2) + * + * Here each judgment (such as "φ is true") is represented by a Coq + * type; furthermore: + * + * 1. A proof of a judgment is any inhabitant of that Coq type. + * + * 2. A proof of a judgment "J2" from hypothesis judgment "J1" + * is any Coq function from the Coq type for J1 to the Coq + * type for J2; Composition of (hypothetical) proofs is + * represented by composition of Coq functions. + * + * 3. A pair of judgments is represented by their product (Coq + * type [prod]) in Coq; a pair of proofs is represented by + * their pair (Coq function [pair]) in Coq. + * + * 4. Duplication of hypotheses is represented by the Coq + * function (fun x => (x,x)). Dereliction of hypotheses is + * represented by the coq function (fun (x,y) => x) or (fun + * (x,y) => y). Exchange of the order of hypotheses is + * represented by the Coq function (fun (x,y) => (y,x)). + * + * The above can be done using lists instead of tuples. + * + * The advantage of this approach is that it requires a minimum + * amount of syntax, and takes maximum advantage of Coq's + * automation facilities. + * + * The disadvantage is that one cannot reason about proof-theoretic + * properties *generically* across different signatures and + * theories. Each signature has its own type of judgments, and + * each theory has its own type of proofs. In the present + * development we will want to prove –– in this generic manner -- + * that various classes of natural deduction calculi form various + * kinds of categories. So we will need this ability to reason + * about proofs independently of the type used to represent + * judgments and (more importantly) of the set of basic inference + * rules. + * + * 2) Structurally explicit proofs + * + * Structurally explicit proofs are formalized in this file + * (NaturalDeduction.v) and are designed specifically in order to + * circumvent the problem in the previous paragraph. + * + *) + +(* + * REGARDING LISTS versus TREES: + * + * You'll notice that this formalization uses (Tree (option A)) in a + * lot of places where you might find (list A) more natural. If this + * bothers you, see the end of the file for the technical reasons why. + * In short, it lets us avoid having to mess about with JMEq or EqDep, + * which are not as well-supported by the Coq core as the theory of + * CiC proper. + *) + +Section Natural_Deduction. + + (* any Coq Type may be used as the set of judgments *) + Context {Judgment : Type}. + + (* any Coq Type –- indexed by the hypothesis and conclusion judgments -- may be used as the set of basic inference rules *) + Context {Rule : forall (hypotheses:Tree ??Judgment)(conclusion:Tree ??Judgment), Type}. + + (* + * This type represents a valid Natural Deduction proof from a list + * (tree) of hypotheses; the notation H/⋯⋯/C is meant to look like + * a proof tree with the middle missing if you tilt your head to + * the left (yeah, I know it's a stretch). Note also that this + * type is capable of representing proofs with multiple + * conclusions, whereas a Rule may have only one conclusion. + *) + Inductive ND : + forall hypotheses:Tree ??Judgment, + forall conclusions:Tree ??Judgment, + Type := + + (* natural deduction: you may infer anything from itself -- "identity proof" *) + | nd_id0 : [ ] /⋯⋯/ [ ] + | nd_id1 : forall h, [ h ] /⋯⋯/ [ h ] + + (* natural deduction: you may discard conclusions *) + | nd_weak : forall h, [ h ] /⋯⋯/ [ ] + + (* natural deduction: you may duplicate conclusions *) + | nd_copy : forall h, h /⋯⋯/ (h,,h) + + (* natural deduction: you may write two proof trees side by side on a piece of paper -- "proof product" *) + | nd_prod : forall {h1 h2 c1 c2} + (pf1: h1 /⋯⋯/ c1 ) + (pf2: h2 /⋯⋯/ c2), + ( h1 ,, h2 /⋯⋯/ c1 ,, c2) + + (* natural deduction: given a proof of every hypothesis, you may discharge them -- "proof composition" *) + | nd_comp : + forall {h x c} + `(pf1: h /⋯⋯/ x) + `(pf2: x /⋯⋯/ c), + ( h /⋯⋯/ c) + + (* structural rules on lists of judgments *) + | nd_cancell : forall {a}, [] ,, a /⋯⋯/ a + | nd_cancelr : forall {a}, a ,, [] /⋯⋯/ a + | nd_llecnac : forall {a}, a /⋯⋯/ [] ,, a + | nd_rlecnac : forall {a}, a /⋯⋯/ a ,, [] + | nd_assoc : forall {a b c}, (a,,b),,c /⋯⋯/ a,,(b,,c) + | nd_cossa : forall {a b c}, a,,(b,,c) /⋯⋯/ (a,,b),,c + + (* any Rule by itself counts as a proof *) + | nd_rule : forall {h c} (r:Rule h c), h /⋯⋯/ c + + where "H /⋯⋯/ C" := (ND H C). + + Notation "H /⋯⋯/ C" := (ND H C) : pf_scope. + Notation "a ;; b" := (nd_comp a b) : nd_scope. + Notation "a ** b" := (nd_prod a b) : nd_scope. + Open Scope nd_scope. + Open Scope pf_scope. + + (* a proof is "structural" iff it does not contain any invocations of nd_rule *) + Inductive Structural : forall {h c}, h /⋯⋯/ c -> Prop := + | nd_structural_id0 : Structural nd_id0 + | nd_structural_id1 : forall h, Structural (nd_id1 h) + | nd_structural_weak : forall h, Structural (nd_weak h) + | nd_structural_copy : forall h, Structural (nd_copy h) + | nd_structural_prod : forall `(pf1:h1/⋯⋯/c1)`(pf2:h2/⋯⋯/c2), Structural pf1 -> Structural pf2 -> Structural (pf1**pf2) + | nd_structural_comp : forall `(pf1:h1/⋯⋯/x) `(pf2: x/⋯⋯/c2), Structural pf1 -> Structural pf2 -> Structural (pf1;;pf2) + | nd_structural_cancell : forall {a}, Structural (@nd_cancell a) + | nd_structural_cancelr : forall {a}, Structural (@nd_cancelr a) + | nd_structural_llecnac : forall {a}, Structural (@nd_llecnac a) + | nd_structural_rlecnac : forall {a}, Structural (@nd_rlecnac a) + | nd_structural_assoc : forall {a b c}, Structural (@nd_assoc a b c) + | nd_structural_cossa : forall {a b c}, Structural (@nd_cossa a b c) + . + + (* multi-judgment generalization of nd_id0 and nd_id1; making nd_id0/nd_id1 primitive and deriving all other *) + Fixpoint nd_id (sl:Tree ??Judgment) : sl /⋯⋯/ sl := + match sl with + | T_Leaf None => nd_id0 + | T_Leaf (Some x) => nd_id1 x + | T_Branch a b => nd_prod (nd_id a) (nd_id b) + end. + + Hint Constructors Structural. + Lemma nd_id_structural : forall sl, Structural (nd_id sl). + intros. + induction sl; simpl; auto. + destruct a; auto. + Defined. + + (* An equivalence relation on proofs which is sensitive only to the logical content of the proof -- insensitive to + * structural variations *) + Class ND_Relation := + { ndr_eqv : forall {h c }, h /⋯⋯/ c -> h /⋯⋯/ c -> Prop where "pf1 === pf2" := (@ndr_eqv _ _ pf1 pf2) + ; ndr_eqv_equivalence : forall h c, Equivalence (@ndr_eqv h c) + + (* the relation must respect composition, be associative wrt composition, and be left and right neutral wrt the identity proof *) + ; ndr_comp_respects : forall {a b c}(f f':a/⋯⋯/b)(g g':b/⋯⋯/c), f === f' -> g === g' -> f;;g === f';;g' + ; ndr_comp_associativity : forall `(f:a/⋯⋯/b)`(g:b/⋯⋯/c)`(h:c/⋯⋯/d), (f;;g);;h === f;;(g;;h) + ; ndr_comp_left_identity : forall `(f:a/⋯⋯/c), nd_id _ ;; f === f + ; ndr_comp_right_identity : forall `(f:a/⋯⋯/c), f ;; nd_id _ === f + + (* the relation must respect products, be associative wrt products, and be left and right neutral wrt the identity proof *) + ; ndr_prod_respects : forall {a b c d}(f f':a/⋯⋯/b)(g g':c/⋯⋯/d), f===f' -> g===g' -> f**g === f'**g' + ; ndr_prod_associativity : forall `(f:a/⋯⋯/a')`(g:b/⋯⋯/b')`(h:c/⋯⋯/c'), (f**g)**h === nd_assoc ;; f**(g**h) ;; nd_cossa + ; ndr_prod_left_identity : forall `(f:a/⋯⋯/b), (nd_id0 ** f ) === nd_cancell ;; f ;; nd_llecnac + ; ndr_prod_right_identity : forall `(f:a/⋯⋯/b), (f ** nd_id0) === nd_cancelr ;; f ;; nd_rlecnac + + (* products and composition must distribute over each other *) + ; ndr_prod_preserves_comp : forall `(f:a/⋯⋯/b)`(f':a'/⋯⋯/b')`(g:b/⋯⋯/c)`(g':b'/⋯⋯/c'), (f;;g)**(f';;g') === (f**f');;(g**g') + + (* any two _structural_ proofs with the same hypotheses/conclusions must be considered equal *) + ; ndr_structural_indistinguishable : forall `(f:a/⋯⋯/b)(g:a/⋯⋯/b), Structural f -> Structural g -> f===g + }. + + (* + * Single-conclusion proofs; this is an alternate representation + * where each inference has only a single conclusion. These have + * worse compositionality properties than ND's, but are easier to + * emit as LaTeX code. + *) + Inductive SCND : Tree ??Judgment -> Tree ??Judgment -> Type := + | scnd_axiom : forall c , SCND [] [c] + | scnd_comp : forall ht ct c , SCND ht ct -> Rule ct [c] -> SCND ht [c] + | scnd_weak : forall c , SCND c [] + | scnd_leaf : forall ht c , SCND ht [c] -> SCND ht [c] + | scnd_branch : forall ht c1 c2, SCND ht c1 -> SCND ht c2 -> SCND ht (c1,,c2) + . + Hint Constructors SCND. + + Definition mkSCNDAxioms (h:Tree ??Judgment) : SCND [] h. + induction h. + destruct a. + apply scnd_leaf. apply scnd_axiom. + apply scnd_weak. + apply scnd_branch; auto. + Defined. + + (* Any ND whose primitive Rules have at most one conclusion (note that nd_prod is allowed!) can be turned into an SCND. *) + Definition mkSCND (all_rules_one_conclusion : forall h c1 c2, Rule h (c1,,c2) -> False) + : forall h x c, ND x c -> SCND h x -> SCND h c. + intros h x c nd. + induction nd; intro k. + apply k. + apply k. + apply scnd_weak. + eapply scnd_branch; apply k. + inversion k; subst. + apply (scnd_branch _ _ _ (IHnd1 X) (IHnd2 X0)). + apply IHnd2. + apply IHnd1. + apply k. + inversion k; subst; auto. + inversion k; subst; auto. + apply scnd_branch; auto. + apply scnd_branch; auto. + inversion k; subst; inversion X; subst; auto. + inversion k; subst; inversion X0; subst; auto. + destruct c. + destruct o. + apply scnd_leaf. eapply scnd_comp. apply k. apply r. + apply scnd_weak. + set (all_rules_one_conclusion _ _ _ r) as bogus. + inversion bogus. + Defined. + + (* a "ClosedND" is a proof with no open hypotheses and no multi-conclusion rules *) + Inductive ClosedND : Tree ??Judgment -> Type := + | cnd_weak : ClosedND [] + | cnd_rule : forall h c , ClosedND h -> Rule h c -> ClosedND c + | cnd_branch : forall c1 c2, ClosedND c1 -> ClosedND c2 -> ClosedND (c1,,c2) + . + + (* + (* we can turn an SCND without hypotheses into a ClosedND *) + Definition closedFromSCND h c (pn2:SCND h c)(cnd:ClosedND h) : ClosedND c. + refine ((fix closedFromPnodes h c (pn2:SCND h c)(cnd:ClosedND h) {struct pn2} := + (match pn2 in SCND H C return H=h -> C=c -> _ with + | scnd_weak c => let case_weak := tt in _ + | scnd_leaf ht z pn' => let case_leaf := tt in let qq := closedFromPnodes _ _ pn' in _ + | scnd_axiom c => let case_axiom := tt in _ + | scnd_comp ht ct c pn' rule => let case_comp := tt in let qq := closedFromPnodes _ _ pn' in _ + | scnd_branch ht c1 c2 pn' pn'' => let case_branch := tt in + let q1 := closedFromPnodes _ _ pn' in + let q2 := closedFromPnodes _ _ pn'' in _ + + end (refl_equal _) (refl_equal _))) h c pn2 cnd). + + destruct case_axiom. + intros; subst. + (* FIXME *) + + destruct case_comp. + intros. + clear pn2. + apply (cnd_rule ct). + apply qq. + subst. + apply cnd0. + apply rule. + + destruct case_weak. + intros; subst. + apply cnd_weak. + + destruct case_leaf. + intros. + apply qq. + subst. + apply cnd0. + + destruct case_branch. + intros. + apply cnd_branch. + apply q1. subst. apply cnd0. + apply q2. subst. apply cnd0. + Defined. + *) + + Close Scope nd_scope. + Open Scope pf_scope. + +End Natural_Deduction. + +Implicit Arguments ND [ Judgment ]. +Hint Constructors Structural. +Hint Extern 1 => apply nd_id_structural. +Hint Extern 1 => apply ndr_structural_indistinguishable. + +(* This first notation gets its own scope because it can be confusing when we're working with multiple different kinds + * of proofs. When only one kind of proof is in use, it's quite helpful though. *) +Notation "H /⋯⋯/ C" := (@ND _ _ H C) : pf_scope. +Notation "a ;; b" := (nd_comp a b) : nd_scope. +Notation "a ** b" := (nd_prod a b) : nd_scope. +Notation "[# a #]" := (nd_rule a) : nd_scope. +Notation "a === b" := (@ndr_eqv _ _ _ _ _ a b) : nd_scope. + +(* enable setoid rewriting *) +Open Scope nd_scope. +Open Scope pf_scope. + +Add Parametric Relation {jt rt ndr h c} : (h/⋯⋯/c) (@ndr_eqv jt rt ndr h c) + reflexivity proved by (@Equivalence_Reflexive _ _ (ndr_eqv_equivalence h c)) + symmetry proved by (@Equivalence_Symmetric _ _ (ndr_eqv_equivalence h c)) + transitivity proved by (@Equivalence_Transitive _ _ (ndr_eqv_equivalence h c)) + as parametric_relation_ndr_eqv. + Add Parametric Morphism {jt rt ndr h x c} : (@nd_comp jt rt h x c) + with signature ((ndr_eqv(ND_Relation:=ndr)) ==> (ndr_eqv(ND_Relation:=ndr)) ==> (ndr_eqv(ND_Relation:=ndr))) + as parametric_morphism_nd_comp. + intros; apply ndr_comp_respects; auto. + Defined. + Add Parametric Morphism {jt rt ndr a b c d} : (@nd_prod jt rt a b c d) + with signature ((ndr_eqv(ND_Relation:=ndr)) ==> (ndr_eqv(ND_Relation:=ndr)) ==> (ndr_eqv(ND_Relation:=ndr))) + as parametric_morphism_nd_prod. + intros; apply ndr_prod_respects; auto. + Defined. + +(* a generalization of the procedure used to build (nd_id n) from nd_id0 and nd_id1 *) +Definition nd_replicate + : forall + {Judgment}{Rule}{Ob} + (h:Ob->Judgment) + (c:Ob->Judgment) + (j:Tree ??Ob), + (forall (o:Ob), @ND Judgment Rule [h o] [c o]) -> + @ND Judgment Rule (mapOptionTree h j) (mapOptionTree c j). + intros. + induction j; simpl. + destruct a; simpl. + apply X. + apply nd_id0. + apply nd_prod; auto. + Defined. + +(* "map" over natural deduction proofs, where the result proof has the same judgments (but different rules) *) +Definition nd_map + : forall + {Judgment}{Rule0}{Rule1} + (r:forall h c, Rule0 h c -> @ND Judgment Rule1 h c) + {h}{c} + (pf:@ND Judgment Rule0 h c) + , + @ND Judgment Rule1 h c. + intros Judgment Rule0 Rule1 r. + + refine ((fix nd_map h c pf {struct pf} := + ((match pf + in @ND _ _ H C + return + @ND Judgment Rule1 H C + with + | nd_id0 => let case_nd_id0 := tt in _ + | nd_id1 h => let case_nd_id1 := tt in _ + | nd_weak h => let case_nd_weak := tt in _ + | nd_copy h => let case_nd_copy := tt in _ + | nd_prod _ _ _ _ lpf rpf => let case_nd_prod := tt in _ + | nd_comp _ _ _ top bot => let case_nd_comp := tt in _ + | nd_rule _ _ rule => let case_nd_rule := tt in _ + | nd_cancell _ => let case_nd_cancell := tt in _ + | nd_cancelr _ => let case_nd_cancelr := tt in _ + | nd_llecnac _ => let case_nd_llecnac := tt in _ + | nd_rlecnac _ => let case_nd_rlecnac := tt in _ + | nd_assoc _ _ _ => let case_nd_assoc := tt in _ + | nd_cossa _ _ _ => let case_nd_cossa := tt in _ + end))) ); simpl in *. + + destruct case_nd_id0. apply nd_id0. + destruct case_nd_id1. apply nd_id1. + destruct case_nd_weak. apply nd_weak. + destruct case_nd_copy. apply nd_copy. + destruct case_nd_prod. apply (nd_prod (nd_map _ _ lpf) (nd_map _ _ rpf)). + destruct case_nd_comp. apply (nd_comp (nd_map _ _ top) (nd_map _ _ bot)). + destruct case_nd_cancell. apply nd_cancell. + destruct case_nd_cancelr. apply nd_cancelr. + destruct case_nd_llecnac. apply nd_llecnac. + destruct case_nd_rlecnac. apply nd_rlecnac. + destruct case_nd_assoc. apply nd_assoc. + destruct case_nd_cossa. apply nd_cossa. + apply r. apply rule. + Defined. + +(* "map" over natural deduction proofs, where the result proof has different judgments *) +Definition nd_map' + : forall + {Judgment0}{Rule0}{Judgment1}{Rule1} + (f:Judgment0->Judgment1) + (r:forall h c, Rule0 h c -> @ND Judgment1 Rule1 (mapOptionTree f h) (mapOptionTree f c)) + {h}{c} + (pf:@ND Judgment0 Rule0 h c) + , + @ND Judgment1 Rule1 (mapOptionTree f h) (mapOptionTree f c). + intros Judgment0 Rule0 Judgment1 Rule1 f r. + + refine ((fix nd_map' h c pf {struct pf} := + ((match pf + in @ND _ _ H C + return + @ND Judgment1 Rule1 (mapOptionTree f H) (mapOptionTree f C) + with + | nd_id0 => let case_nd_id0 := tt in _ + | nd_id1 h => let case_nd_id1 := tt in _ + | nd_weak h => let case_nd_weak := tt in _ + | nd_copy h => let case_nd_copy := tt in _ + | nd_prod _ _ _ _ lpf rpf => let case_nd_prod := tt in _ + | nd_comp _ _ _ top bot => let case_nd_comp := tt in _ + | nd_rule _ _ rule => let case_nd_rule := tt in _ + | nd_cancell _ => let case_nd_cancell := tt in _ + | nd_cancelr _ => let case_nd_cancelr := tt in _ + | nd_llecnac _ => let case_nd_llecnac := tt in _ + | nd_rlecnac _ => let case_nd_rlecnac := tt in _ + | nd_assoc _ _ _ => let case_nd_assoc := tt in _ + | nd_cossa _ _ _ => let case_nd_cossa := tt in _ + end))) ); simpl in *. + + destruct case_nd_id0. apply nd_id0. + destruct case_nd_id1. apply nd_id1. + destruct case_nd_weak. apply nd_weak. + destruct case_nd_copy. apply nd_copy. + destruct case_nd_prod. apply (nd_prod (nd_map' _ _ lpf) (nd_map' _ _ rpf)). + destruct case_nd_comp. apply (nd_comp (nd_map' _ _ top) (nd_map' _ _ bot)). + destruct case_nd_cancell. apply nd_cancell. + destruct case_nd_cancelr. apply nd_cancelr. + destruct case_nd_llecnac. apply nd_llecnac. + destruct case_nd_rlecnac. apply nd_rlecnac. + destruct case_nd_assoc. apply nd_assoc. + destruct case_nd_cossa. apply nd_cossa. + apply r. apply rule. + Defined. + +(* witnesses the fact that every Rule in a particular proof satisfies the given predicate *) +Inductive nd_property {Judgment}{Rule}(P:forall h c, @Rule h c -> Prop) : forall {h}{c}, @ND Judgment Rule h c -> Prop := + | nd_property_structural : forall h c pf, Structural pf -> @nd_property _ _ P h c pf + | nd_property_prod : forall h0 c0 pf0 h1 c1 pf1, + @nd_property _ _ P h0 c0 pf0 -> @nd_property _ _ P h1 c1 pf1 -> @nd_property _ _ P _ _ (nd_prod pf0 pf1) + | nd_property_comp : forall h0 c0 pf0 c1 pf1, + @nd_property _ _ P h0 c0 pf0 -> @nd_property _ _ P c0 c1 pf1 -> @nd_property _ _ P _ _ (nd_comp pf0 pf1) + | nd_property_rule : forall h c r, P h c r -> @nd_property _ _ P h c (nd_rule r). + Hint Constructors nd_property. + +Close Scope pf_scope. +Close Scope nd_scope. diff --git a/src/NaturalDeductionToLatex.v b/src/NaturalDeductionToLatex.v new file mode 100644 index 0000000..66c1a5c --- /dev/null +++ b/src/NaturalDeductionToLatex.v @@ -0,0 +1,105 @@ +(*********************************************************************************************************************************) +(* NaturalDeductionToLatex: rendering natural deduction proofs as LaTeX code *) +(*********************************************************************************************************************************) + +Generalizable All Variables. +Require Import Preamble. +Require Import General. +Require Import Coq.Strings.Ascii. +Require Import Coq.Strings.String. +Require Import NaturalDeduction. + +(* string stuff *) +Variable eol : string. +Extract Constant eol => "'\n':[]". + +Section ToLatex. + + Context {Judgment : Type}. + Context {Rule : forall (hypotheses:Tree ??Judgment)(conclusion:Tree ??Judgment), Type}. + + (* the "user" must supply functions for latexifying judgments and rules *) + Context (judgment2latex : Judgment -> string). + Context (rule2latex : forall h c, Rule h c -> string). + + Open Scope string_scope. + Notation "a +++ b" := (append a b) (at level 100). + Section TreeToLatex. + Context (emptyleaf:string). + Context {T:Type}. + Context (leaf:T -> string). + Fixpoint tree2latex' (j:Tree ??T) : string := + match j with + | T_Leaf None => emptyleaf + | T_Leaf (Some j') => leaf j' + | T_Branch b1 b2 => "\left["+++tree2latex' b1+++ + "\text{\tt{,}}"+++ + tree2latex' b2+++"\right]" + end. + Definition tree2latex (j:Tree ??T) : string := + match j with + | T_Leaf None => emptyleaf + | T_Leaf (Some j') => leaf j' + | T_Branch b1 b2 => tree2latex' b1+++ + "\text{\tt{,}}"+++ + tree2latex' b2 + end. + Fixpoint list2latex (sep:string)(l:list T) : string := + match l with + | nil => emptyleaf + | (a::nil) => leaf a + | (a::b) => (leaf a)+++sep+++(list2latex sep b) + end. + End TreeToLatex. + + Definition judgments2latex (j:Tree ??Judgment) := + list2latex " " judgment2latex " \\ " (leaves j). + + (* invariant: each proof shall emit its hypotheses visibly, except nd_id0 *) + Section SCND_toLatex. + Context (hideRule : forall h c (r:Rule h c), bool). + + Fixpoint SCND_toLatex {h}{c}(pns:SCND h c) : string := + match pns with + | scnd_leaf ht c pn => SCND_toLatex pn + | scnd_branch ht c1 c2 pns1 pns2 => SCND_toLatex pns1 +++ " \hspace{1cm} " +++ SCND_toLatex pns2 + | scnd_weak c => "" + | scnd_axiom c => judgment2latex c +++ eol + | scnd_comp ht ct c pns rule => if hideRule _ _ rule + then SCND_toLatex pns + else "\trfrac["+++rule2latex _ _ rule +++ "]{" +++ eol +++ + SCND_toLatex pns +++ "}{" +++ eol +++ + judgment2latex c +++ "}" +++ eol + end. + End SCND_toLatex. + + (* FIXME: this doesn't actually work properly (but SCND_toLatex does!) *) + Fixpoint nd_toLatex {h}{c}(nd:@ND _ Rule h c)(indent:string) := + match nd with + | nd_id0 => indent +++ "% nd_id0 " +++ eol + | nd_id1 h' => indent +++ "% nd_id1 "+++ judgments2latex h +++ eol + | nd_weak h' => indent +++ "\inferrule*[Left=ndWeak]{" +++ judgment2latex h' +++ "}{ }" +++ eol + | nd_copy h' => indent +++ "\inferrule*[Left=ndCopy]{"+++judgments2latex h+++ + "}{"+++judgments2latex c+++"}" +++ eol + | nd_prod h1 h2 c1 c2 pf1 pf2 => indent +++ "% prod " +++ eol +++ + indent +++ "\begin{array}{c c}" +++ eol +++ + (nd_toLatex pf1 (" "+++indent)) +++ + indent +++ " & " +++ eol +++ + (nd_toLatex pf2 (" "+++indent)) +++ + indent +++ "\end{array}" + | nd_comp h m c pf1 pf2 => indent +++ "% comp " +++ eol +++ + indent +++ "\begin{array}{c}" +++ eol +++ + (nd_toLatex pf1 (" "+++indent)) +++ + indent +++ " \\ " +++ eol +++ + (nd_toLatex pf2 (" "+++indent)) +++ + indent +++ "\end{array}" + | nd_cancell a => indent +++ "% nd-cancell " +++ (judgments2latex a) +++ eol + | nd_cancelr a => indent +++ "% nd-cancelr " +++ (judgments2latex a) +++ eol + | nd_llecnac a => indent +++ "% nd-llecnac " +++ (judgments2latex a) +++ eol + | nd_rlecnac a => indent +++ "% nd-rlecnac " +++ (judgments2latex a) +++ eol + | nd_assoc a b c => "" + | nd_cossa a b c => "" + | nd_rule h c r => rule2latex h c r + end. + +End ToLatex. diff --git a/src/Preamble.v b/src/Preamble.v new file mode 100644 index 0000000..026d6d1 --- /dev/null +++ b/src/Preamble.v @@ -0,0 +1,142 @@ +(*********************************************************************************************************************************) +(* Preamble: miscellaneous notations *) +(*********************************************************************************************************************************) + +Require Import Coq.Unicode.Utf8. +Require Import Coq.Classes.RelationClasses. +Require Import Coq.Classes.Morphisms. +Require Import Coq.Setoids.Setoid. +Require Setoid. +Require Import Coq.Strings.String. +Export Coq.Unicode.Utf8. +Export Coq.Classes.RelationClasses. +Export Coq.Classes.Morphisms. +Export Coq.Setoids.Setoid. + +Set Printing Width 130. (* Proof General seems to add an extra two columns of overhead *) +Generalizable All Variables. + +Reserved Notation "a -~- b" (at level 10). +Reserved Notation "a ** b" (at level 10). +Reserved Notation "?? x" (at level 1). +Reserved Notation "a ,, b" (at level 50). +Reserved Notation "!! f" (at level 3). +Reserved Notation "!` x" (at level 2). +Reserved Notation "`! x" (at level 2). +Reserved Notation "a ~=> b" (at level 70, right associativity). +Reserved Notation "H ===> C" (at level 100). +Reserved Notation "f >>=>> g" (at level 45). +Reserved Notation "a ~~{ C }~~> b" (at level 100). +Reserved Notation "f <--> g" (at level 20). +Reserved Notation "! f" (at level 2). +Reserved Notation "? f" (at level 2). +Reserved Notation "# f" (at level 2). +Reserved Notation "f '⁻¹'" (at level 1). +Reserved Notation "a ≅ b" (at level 70, right associativity). +Reserved Notation "C 'ᵒᴾ'" (at level 1). +Reserved Notation "F \ a" (at level 20). +Reserved Notation "f >>> g" (at level 45). +Reserved Notation "a ~~ b" (at level 54). +Reserved Notation "a ~> b" (at level 70, right associativity). +Reserved Notation "a ≃ b" (at level 70, right associativity). +Reserved Notation "a ≃≃ b" (at level 70, right associativity). +Reserved Notation "a ~~> b" (at level 70, right associativity). +Reserved Notation "F ~~~> G" (at level 70, right associativity). +Reserved Notation "F <~~~> G" (at level 70, right associativity). +Reserved Notation "a ⊗ b" (at level 40). +Reserved Notation "a ⊗⊗ b" (at level 40). +Reserved Notation "a ⊕ b" (at level 40). +Reserved Notation "a ⊕⊕ b" (at level 40). +Reserved Notation "f ⋉ A" (at level 40). +Reserved Notation "A ⋊ f" (at level 40). +Reserved Notation "- ⋉ A" (at level 40). +Reserved Notation "A ⋊ -" (at level 40). +Reserved Notation "a *** b" (at level 40). +Reserved Notation "a ;; b" (at level 45). +Reserved Notation "[# f #]" (at level 2). +Reserved Notation "a ---> b" (at level 11, right associativity). +Reserved Notation "a <- b" (at level 100, only parsing). +Reserved Notation "G |= S" (at level 75). +Reserved Notation "F -| G" (at level 75). +Reserved Notation "a :: b" (at level 60, right associativity). +Reserved Notation "a ++ b" (at level 60, right associativity). +Reserved Notation "<[ t @]>" (at level 30). +Reserved Notation "<[ t @ n ]>" (at level 30). +Reserved Notation "<[ e ]>" (at level 30). +Reserved Notation "'Λ' x : t :-> e" (at level 9, right associativity, x ident). +Reserved Notation "R ==> R' " (at level 55, right associativity). +Reserved Notation "f ○ g" (at level 100). +Reserved Notation "a ==[ n ]==> b" (at level 20). +Reserved Notation "a ==[ h | c ]==> b" (at level 20). +Reserved Notation "H /⋯⋯/ C" (at level 70). +Reserved Notation "pf1 === pf2" (at level 80). +Reserved Notation "a |== b @@ c" (at level 100). +Reserved Notation "f >>>> g" (at level 45). +Reserved Notation "a >>[ n ]<< b" (at level 100). +Reserved Notation "f **** g" (at level 40). +Reserved Notation "C × D" (at level 40). +Reserved Notation "C ×× D" (at level 45). +Reserved Notation "C ⁽ºᑭ⁾" (at level 1). + +Reserved Notation "'<[' a '|-' t ']>'" (at level 35). + +Reserved Notation "Γ '∌' x" (at level 10). +Reserved Notation "Γ '∌∌' x" (at level 10). +Reserved Notation "Γ '∋∋' x : a ∼ b" (at level 10, x at level 99). +Reserved Notation "Γ '∋' x : c" (at level 10, x at level 99). + +Reserved Notation "a ⇛ b" (at level 40). +Reserved Notation "φ₁ →→ φ₂" (at level 11, right associativity). +Reserved Notation "a '⊢ᴛy' b : c" (at level 20, b at level 99, c at level 80). +Reserved Notation "a '⊢ᴄᴏ' b : c ∼ d" (at level 20, b at level 99). +Reserved Notation "Γ '+' x : c" (at level 50, x at level 99). +Reserved Notation "Γ '++' x : a ∼ b" (at level 50, x at level 99). +Reserved Notation "φ₁ ∼∼ φ₂ : κ ⇒ φ₃" (at level 11, φ₂ at level 99, right associativity). + +Reserved Notation "Γ > past : present '⊢ᴇ' succedent" + (at level 52, past at level 99, present at level 50, succedent at level 50). + +Reserved Notation "'η'". +Reserved Notation "'ε'". +Reserved Notation "'★'". + +Notation "a +++ b" := (append a b) (at level 100). +Close Scope nat_scope. (* so I can redefine '1' *) + +Delimit Scope arrow_scope with arrow. +Delimit Scope biarrow_scope with biarrow. +Delimit Scope garrow_scope with garrow. + +Notation "f ○ g" := (fun x => f(g(x))). +Notation "?? T" := (option T). + +(* these are handy since Coq's pattern matching syntax isn't integrated with its abstraction binders (like Haskell and ML) *) +Notation "'⟨' x ',' y '⟩'" := ((x,y)) (at level 100). +Notation "'Λ' '⟨' x ',' y '⟩' e" := (fun xy => match xy with (a,b) => (fun x y => e) a b end) (at level 100). +Notation "'Λ' '⟨' x ',' '⟨' y ',' z '⟩' '⟩' e" := + (fun xyz => match xyz with (a,bc) => match bc with (b,c) => (fun x y z => e) a b c end end) (at level 100). +Notation "'Λ' '⟨' '⟨' x ',' y '⟩' ',' z '⟩' e" := + (fun xyz => match xyz with (ab,c) => match ab with (a,b) => (fun x y z => e) a b c end end) (at level 100). + +Notation "∀ x y z u q , P" := (forall x y z u q , P) + (at level 200, q ident, x ident, y ident, z ident, u ident, right associativity) + : type_scope. +Notation "∀ x y z u q v , P" := (forall x y z u q v , P) + (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, right associativity) + : type_scope. +Notation "∀ x y z u q v a , P" := (forall x y z u q v a , P) + (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, right associativity) + : type_scope. +Notation "∀ x y z u q v a b , P" := (forall x y z u q v a b , P) + (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, b ident, right associativity) + : type_scope. +Notation "∀ x y z u q v a b r , P" := (forall x y z u q v a b r , P) + (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, b ident, r ident, right associativity) + : type_scope. +Notation "∀ x y z u q v a b r s , P" := (forall x y z u q v a b r s , P) + (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, b ident, r ident, s ident, right associativity) + : type_scope. +Notation "∀ x y z u q v a b r s t , P" := (forall x y z u q v a b r s t , P) + (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, b ident, r ident, s ident, t ident, + right associativity) + : type_scope. -- 1.7.10.4