Change polytypes from sg to s

grammar.ott

@@ -22,7 +22,7 @@ grammar
 prog :: 'Prog_' ::= {{ com Programs }}
 | empty                   ::  :: Empty         {{ com Empty }}
 | f = e , prog            ::  :: Bind          {{ com Inferred binding }}
-| f '::' sg '=' e , prog  ::  :: TypedBind     {{ com Ascribed binding }}
+| f '::' s '=' e , prog  ::  :: TypedBind     {{ com Ascribed binding }}
 
 CL :: 'ConLike_' ::= {{ com ConLikes }}
 | K       ::   :: RealDataCon              {{ com Data constructor }}
@@ -40,8 +40,8 @@ e :: 'Expr_' ::= {{ com Expressions }}
 | e1 e2                       ::   :: App       {{ com Application }}
 | case e of { alts }          ::   :: Case      {{ com Pattern-match }}
 | ( e )                       ::   :: Parens    {{ com Grouping }}
-| let  x '::' sg  = e1 in e2  ::   :: Let       {{ com Ascribed let }}
-  {{ tex \keyword{let}\ [[x]] [[::]] [[sg]] = [[e1]]\ \keyword{in}\ [[e2]] }}
+| let  x '::' s  = e1 in e2  ::   :: Let       {{ com Ascribed let }}
+  {{ tex \keyword{let}\ [[x]] [[::]] [[s]] = [[e1]]\ \keyword{in}\ [[e2]] }}
 
 alts {{ tex \overline{\ottnt{p} \to \ottnt{e} } }} :: 'Alts_' ::= {{ com Case alternatives }}
 | </ pi -> ei // i /> :: :: Patterns
@@ -49,7 +49,7 @@ alts {{ tex \overline{\ottnt{p} \to \ottnt{e} } }} :: 'Alts_' ::= {{ com Case al
 p :: 'Pat_' ::= {{ com Patterns }}
 | _               :: :: Underscore              {{ com Wildcard }}
 | x               :: :: Var                     {{ com Variable }}
-| p '::' sg       :: :: Sig                     {{ com Pattern signature }}
+| p '::' s       :: :: Sig                     {{ com Pattern signature }}
 | CL ps           :: :: Con                     {{ com Constructor }}
 | CL atts ps      :: :: ConTys                  {{ com Constructor with type arguments }}
 | ( p )           :: :: Parens                  {{ com Grouping }}
@@ -60,14 +60,14 @@ ps {{ tex \overline{\ottnt{p} } }} :: 'Pats_' ::= {{ com Lists of patterns }}
 atts {{ tex \overline{\at \tau} }} :: 'AtTypes_' ::= {{ com Lists of visible type patterns }}
 | @ t1 ... @ ti   ::  :: List
 
-sg {{ tex \sigma }} :: 'SigTy_' ::= {{ com Type schemes }}
-| Q => sg ::   :: ForallQTy                     {{ com Qualified type }}
-  {{ tex [[Q]] [[=>]] [[sg]] }}
-| forall as . sg      ::   :: ForallTy          {{ com Quantified type }}
-  {{ tex [[forall]] [[as]].\,[[sg]] }}
+s {{ tex \sigma }} :: 'SigTy_' ::= {{ com Type schemes }}
+| Q => s ::   :: ForallQTy                     {{ com Qualified type }}
+  {{ tex [[Q]] [[=>]] [[s]] }}
+| forall as . s      ::   :: ForallTy          {{ com Quantified type }}
+  {{ tex [[forall]] [[as]].\,[[s]] }}
 | t                             ::   :: MonoTy  {{ com Monotype }}
-| [ </ ai |-> ti // i /> ] sg   :: M :: Subst
-| theta ( sg )                  :: M :: SubstVar
+| [ </ ai |-> ti // i /> ] s   :: M :: Subst
+| theta ( s )                  :: M :: SubstVar
 
 tvs {{ tex \overline{\ottnt{tv} } }}, as {{ tex \overline{\ottmv{a} } }}, bs {{ tex \overline{\ottmv{b} } }}, cs {{ tex \overline{\ottmv{c} } }} :: 'Vars_' ::= {{ com Lists of variables }}
 | </ ai // i />   :: :: List
@@ -98,8 +98,8 @@ theta {{ tex \theta }} :: 'Subst_' ::= {{ com Type substitutions }}
 t {{ tex \tau }}, u {{ tex \upsilon }} :: 'Ty_' ::= {{ com Monotypes }}
 | a                              ::   :: IVar       {{ com Internal variable }}
 | c                              ::   :: UVar       {{ com External variable }}
-| sg -> t                        ::   :: Fun        {{ com Function }}
-| sgs -> t                       :: M :: Funs
+| s -> t                        ::   :: Fun        {{ com Function }}
+| ss -> t                       :: M :: Funs
 | T ts                           ::   :: ConApp     {{ com Constructor application }}
 | theta t                        :: M :: Subst
   {{ tex [[theta]] [[t]] }}
@@ -111,14 +111,14 @@ ts {{ tex \overline{\tau} }} :: 'Tys_' ::= {{ com Lists of monotypes }}
 | </ ti // i />               :: :: List
 | as                          :: :: Vars
 
-sgs {{ tex \overline{\sigma} }} :: 'Sigmas_' ::= {{ com Lists of polytypes }}
-| </ sgi // , // i />              ::  :: List
+ss {{ tex \overline{\sigma} }} :: 'Sigmas_' ::= {{ com Lists of polytypes }}
+| </ si // , // i />              ::  :: List
 
 G {{ tex \Gamma }}, Gt {{ tex \Gamma_t }} :: 'TyEnv_' ::= {{ com Type environments }}
 | empty                        :: :: Empty      {{ com Empty }}
 | G1 , ... , Gn                :: :: List       {{ com Concatentation }}
-| v : sg                       :: :: Var        {{ com Variable binding }}
-| CL : sg                       :: :: PatSyn    {{ com ConLike binding }}
+| v : s                       :: :: Var        {{ com Variable binding }}
+| CL : s                       :: :: PatSyn    {{ com ConLike binding }}
 | Q                            :: :: Constraint {{ com Given constraint }}
 | tv : type                    :: :: TyVar      {{ com Type variable binding }}
 | < tv : type >                :: M :: TyVars
@@ -128,7 +128,7 @@ G {{ tex \Gamma }}, Gt {{ tex \Gamma_t }} :: 'TyEnv_' ::= {{ com Type environmen
 | Giminus_one                  :: M  :: GIHack
 
 obj :: 'SynObj' ::= {{ com Syntactic object }}
-| sgs :: :: TypeScheme
+| ss :: :: TypeScheme
 | Q  :: :: Constraint
 | G  :: :: Context
 
@@ -186,8 +186,8 @@ terminals :: 'terminals_' ::=
 formula :: formula_ ::=
 |  judgement                       ::   :: judgement
 |  formula1 '//' .. '//' formulan            ::   :: dots
-|  ( v : sg ) in G                   ::   :: ctxtlookup
-|  ( P : sg ) in G                   ::   :: patsynlookup
+|  ( v : s ) in G                   ::   :: ctxtlookup
+|  ( P : s ) in G                   ::   :: patsynlookup
 |  theta1 = theta2                   ::   :: substdef
 |  G = G'                           ::   :: ctxtdef
 |  tvrel                             ::   :: tvrel

haskell.mng

@@ -30,16 +30,16 @@
 
 \section{Grammar}
 
-\nonterms{prog,CL,v,e,p,sg,Q,tv,theta,t,G}
+\nonterms{prog,CL,v,e,p,s,Q,tv,theta,t,G}
 
 \section{Typing rules}
 
 \drules[E]{$[[G |- e : t]]$}{Expressions}{VarCon,Eq,App,Abs,Case,Let}
 
-Abstract judgments $[[G ||- Q]]$ denotes entailment and $[[G ||- sg1 <= sg2]]$ denotes
-subtyping ($[[sg1]]$ is more general than $[[sg2]]$).
+Abstract judgments $[[G ||- Q]]$ denotes entailment and $[[G ||- s1 <= s2]]$ denotes
+subtyping ($[[s1]]$ is more general than $[[s2]]$).
 
-\drules[P]{$[[G |-p p : sg => G']]$}{Patterns}{Var,Con,Syn,Sig}
-\drules[Ps]{$[[G |-p* </ pi : sgi // i /> => G']]$}{Pattern sequences}{PatSeq}
+\drules[P]{$[[G |-p p : s => G']]$}{Patterns}{Var,Con,Syn,Sig}
+\drules[Ps]{$[[G |-p* </ pi : si // i /> => G']]$}{Pattern sequences}{PatSeq}
 
 \end{document}

rules.ott

@@ -43,30 +43,30 @@ ftv(t) (= dom(G)
 --------------------------------- :: Case
 G |- case e of {</ pi -> ei // i />} : t
 
-sg = forall cs. Q => u
-ftv(sg) (= dom(G)
+s = forall cs. Q => u
+ftv(s) (= dom(G)
 G, <c : type>, Q  |- e : u
-G, x : sg |- e2 : t
+G, x : s |- e2 : t
 ----------------------------- :: Let
-G |- let x :: sg = e in e2 : t
+G |- let x :: s = e in e2 : t
 
 defn
 G ||- Q'         :: :: ConImpl :: 'ConImpl_' {{ com Constraint implication }}
 by
 
 defn
-G ||- sg <= sg'  :: :: Subtype :: 'SubType_' {{ com Subtyping relation}}
+G ||- s <= s'  :: :: Subtype :: 'SubType_' {{ com Subtyping relation}}
 by
 
 
 defn
-G |-p p : sg => G' :: :: Pat :: 'P_' {{ com Pattern typing }}
+G |-p p : s => G' :: :: Pat :: 'P_' {{ com Pattern typing }}
 by
 
 -------------------------------- :: Var
-G |-p x : sg => G, (x : sg)
+G |-p x : s => G, (x : s)
 
-(P : forall </ ai // i />. Qr => forall </ bj // j />. Qp => </ sgk // k /> -> u) in G
+(P : forall </ ai // i />. Qr => forall </ bj // j />. Qp => </ sk // k /> -> u) in G
 G' = G, (</ ai : type // i />), (</ ai ~ u'i // i />)
 </ ai // i /> # dom(G)
 G' ||- (u ~ t) /\ Qr
@@ -75,45 +75,45 @@ G' ||- (u ~ t) /\ Qr
 G'' = G',(</ bj : type // j />),(</ cl : type // l />),(</ cl ~ b'l // l />),Qp
 </ G'' ||- t'i ~ ai // i />
 </ G'' ||- t''j ~ bj // j />
-G'' |-p* </ pk : theta(sgk) // k /> => G'''
+G'' |-p* </ pk : theta(sk) // k /> => G'''
 -------------------------------- :: Syn
 G |-p P </ @ t'i // i /> </ @ t''j // j /> </ pk // k /> : t => G'''
 
 
 
-(K : forall </ aj // j /> . Q  => </ sgk // k /> -> T </ ui // i />) in G
+(K : forall </ aj // j /> . Q  => </ sk // k /> -> T </ ui // i />) in G
 </ cl // l /> = ftv(</ t'j // j />) \ dom(G)
 </ aj // j /> # dom(G)
 G' = G,(</ aj : type // j />),(</ cl : type // l />),(</ cl ~ t''l // l />),(</ ui ~ ti // i />),Q
 </ G' ||- t'j ~ aj // j />
-G' |-p* </ pk : sgk // k /> => G''
+G' |-p* </ pk : sk // k /> => G''
 -------------------------------- :: Con
 G |-p K </ @ t'j // j /> </ pk // k /> : T </ ti // i /> => G''
 
-cs = ftv(sg') \ dom(G)
+cs = ftv(s') \ dom(G)
 G' = G, <c : type>, < c ~ t >
-G' ||- sg <= sg'
-G' |-p p : sg' => G''
+G' ||- s <= s'
+G' |-p p : s' => G''
 -------------------------------- :: Sig
-G |-p (p :: sg') : sg => G''
+G |-p (p :: s') : s => G''
 
 
 
 defn
-G |-p* </ pi : sgi // i />  => G' :: :: PatSeq :: 'Ps_' {{ com Pattern squence typing }}
+G |-p* </ pi : si // i />  => G' :: :: PatSeq :: 'Ps_' {{ com Pattern squence typing }}
 by
 
 % help, how do I typeset that with G_{i-1}
-</ Giminus_one |-p  pi : sgi => Gi  // i IN 1 .. n />
+</ Giminus_one |-p  pi : si => Gi  // i IN 1 .. n />
 ----------------------------- :: PatSeq
-G0 |-p*  </ pi : sgi // i IN 1 .. n />  => Gn
+G0 |-p*  </ pi : si // i IN 1 .. n />  => Gn
 
 
 % defn
-% G |-sb* e <= sg :: :: Check :: '' {{ com Checking against specified polytypes }}
-%   {{ tex [[G]] [[|-sb*]] [[e]] \Leftarrow [[sg]] }}
+% G |-sb* e <= s :: :: Check :: '' {{ com Checking against specified polytypes }}
+%   {{ tex [[G]] [[|-sb*]] [[e]] \Leftarrow [[s]] }}
 % by
 
-% G, c : type |-sb* e <= [a |-> c]sg
+% G, c : type |-sb* e <= [a |-> c]s
 % --------------------------------- :: SB_DTyAbs
-% G |-sb* \ @c . e <= forall a. sg
+% G |-sb* \ @c . e <= forall a. s