matita/matita/contribs/lambdadelta/basic_2/etc_2A1/snta/snta.etc

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 : * break [ l ] break term 46 T2 )"
  16    non associative with precedence 45
  17    for @{ 'NativeTypeStar $h $l $L $T1 $T2 }.
  18
  19 notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 : break [ l ] break term 46 T2 )"
  20    non associative with precedence 45
  21    for @{ 'StratifiedNativeType $h $l $L $T1 $T2 }.
  22
  23 include "basic_2/static/sh.ma".
  24 include "basic_2/equivalence/cpcs.ma".
  25
  26 (* STRATIFIED NATIVE TYPE ASSIGNMENT ON TERMS *******************************)
  27
  28 inductive snta (h:sh): nat → lenv → relation term ≝
  29 | snta_sort: ∀L,k. snta h 0 L (⋆k) (⋆(next h k))
  30 | snta_ldef: ∀L,K,V,W,U,i,l. ⇩[0, i] L ≡ K. ⓓV → snta h l K V W →
  31              ⇧[0, i + 1] W ≡ U → snta h l L (#i) U
  32 | snta_ldec: ∀L,K,W,V,U,i,l. ⇩[0, i] L ≡ K. ⓛW → snta h l K W V →
  33              ⇧[0, i + 1] W ≡ U → snta h (l+1) L (#i) U
  34 | snta_bind: ∀I,L,V,W,T,U,l1,l2. snta h l1 L V W → snta h l2 (L. ⓑ{I} V) T U →
  35              snta h l2 L (ⓑ{I}V.T) (ⓑ{I}V.U)
  36 | snta_appl: ∀L,V,W1,W2,T,U,l1,l2. snta h (l1+1) L V W2 →
  37              snta h l2 L (ⓛW1.T) (ⓛW2.U) →
  38              snta h l2 L (ⓐV.ⓛW1.T) (ⓐV.ⓛW2.U)
  39 | snta_pure: ∀L,V,T,U,W,l. snta h (l+1) L T U → snta h l L (ⓐV.U) W →
  40              snta h (l+1) L (ⓐV.T) (ⓐV.U)
  41 | snta_cast: ∀L,T,U,W,l1,l2. snta h l2 L T U → snta h l1 L U W →
  42              snta h l2 L (ⓝU.T) U
  43 | snta_conv: ∀L,T,U1,U2,V2,l. snta h l L T U1 → L ⊢ U1 ⬌* U2 →
  44              snta h (l-1) L U2 V2 → snta h l L T U2
  45 .
  46
  47 interpretation "stratified native type assignment (term)"
  48    'StratifiedNativeType h l L T U = (snta h l L T U).