diff --git a/grammar.ott b/grammar.ott index 4d4b3f4d49f46dfd66dc5c2441dc7f60023fbd1a..31c3cefa4582fe14e2e4ea020eb849ca2fcdeb80 100644 --- a/grammar.ott +++ b/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 diff --git a/haskell.mng b/haskell.mng index bc2708fc3faf051fbe56e3706af03475a1cbcc45..69a1401f5387470a730b0789b1313cbc3a226b4b 100644 --- a/haskell.mng +++ b/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} diff --git a/rules.ott b/rules.ott index 6ebda6b49948a0bbfd6d037b9ad98711a741535d..4a86f9461a8f6072a8ff7d2923061b5dc76d118b 100644 --- a/rules.ott +++ b/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