~thon/thon

e1c37a8074e0966021671defe79956699db8ecd6 — Evan Bergeron 8 months ago fd82ecc
Lower Type.Plus precedence; parse `data eq` tyrec
3 files changed, 9 insertions(+), 4 deletions(-)

M parse/ast.sml
M parse/thon.grm
M parse/thon.lex
M parse/ast.sml => parse/ast.sml +2 -0
@@ 24,6 24,7 @@ sig
      | App of Exp * Exp
      | Rec of Exp (*i : Nat*) * Exp (*baseCase: t*) * string * Exp (*recCase - binds*)
      | Fix of string (*x*) * Typ (*: t*) * Exp (*x's scope*)
      | Data of string (*x*) * Typ (*= t*) * Exp (*x's scope*)
      | TypAbs of string * Exp (* binds type variable *)
      | Ifz of Exp * Exp * string * Exp
      | TypApp of Typ * Exp


@@ 75,6 76,7 @@ struct
      | App of Exp * Exp
      | Rec of Exp (*i : Nat*) * Exp (*baseCase: t*) * string * Exp (*recCase - binds*)
      | Fix of string (*x*) * Typ (*: t*) * Exp (*x's scope*)
      | Data of string (*x*) * Typ (*= t*) * Exp (*x's scope*)
      | TypAbs of string * Exp (* binds type variable *)
      | Ifz of Exp * Exp * string * Exp
      | TypApp of Typ * Exp

M parse/thon.grm => parse/thon.grm +6 -4
@@ 17,6 17,7 @@ structure A = Ast
 | NAT
 | REC
 | APP
 | TYPEOR
 | IDX of int
 | ID of string
 | GO


@@ 46,6 47,7 @@ structure A = Ast
 | IFZ
 | FIX
 | FUN
 | DATA

%nonterm
   exp of A.Exp


@@ 63,7 65,8 @@ structure A = Ast
(* If the rule has the higher precedence, the reduction is chosen. *)

(* The precedence grows down *)
%nonassoc EOF ZERO SUCC LPAREN RPAREN LAM COLON NAT IDX ID REC PIPE POLY COMMA STAR LEFT RIGHT FST SND ALL SOME TYPEREC DOT UNIT FOLD UNFOLD WITH AS USE IN CASE OF IMPL LET EQ IFZ FIX FUN
%nonassoc TYPEOR (* Deliberately first *)
%nonassoc EOF ZERO SUCC LPAREN RPAREN LAM COLON NAT IDX ID REC PIPE POLY COMMA STAR LEFT RIGHT FST SND ALL SOME TYPEREC DOT UNIT FOLD UNFOLD WITH AS USE IN CASE OF IMPL LET EQ IFZ FIX FUN DATA
%right SARROW
%nonassoc APP GO (* Deliberately last *)



@@ 94,8 97,6 @@ exp:
  | RIGHT exp COLON typ (A.PlusRight(typ, exp))
  | FOLD typ WITH exp (A.Fold(typ, exp))
  | UNFOLD exp (A.Unfold(exp))
  (* impl reprType in pkgImpl as pkgType *)
  (* Impl (reprType, pkgImpl, pkgType) *)
  | IMPL typ WITH typ AS exp (A.Impl(typ2, exp, typ1))
  | USE exp AS LPAREN ID COMMA ID RPAREN IN exp (A.Use(exp1, ID1, ID2, exp2))
  | CASE exp OF ID SARROW exp PIPE ID SARROW exp (A.Case(exp1, ID1, exp2, ID2, exp3))


@@ 111,5 112,6 @@ typ:
  | ALL ID DOT typ (A.All (ID, typ))
  | SOME ID DOT typ (A.Some (ID, typ))
  | TYPEREC ID DOT typ (A.TyRec (ID, typ))
  | DATA ID EQ typ (A.TyRec (ID, typ))
  (* TODO should this take precedence below star and arrow? *)
  | typ PIPE typ (A.Plus (typ1, typ2))
  | typ PIPE typ %prec TYPEOR (A.Plus (typ1, typ2))

M parse/thon.lex => parse/thon.lex +1 -0
@@ 69,6 69,7 @@ ws = [\ \t];
<INITIAL> "impl"   => (Tokens.IMPL(!pos,!pos));
<INITIAL> "use"    => (Tokens.USE(!pos,!pos));
<INITIAL> "case"   => (Tokens.CASE(!pos,!pos));
<INITIAL> "data"   => (Tokens.DATA(!pos,!pos));
<INITIAL> "as"     => (Tokens.AS(!pos,!pos));
<INITIAL> "in"     => (Tokens.IN(!pos,!pos));
<INITIAL> "of"     => (Tokens.OF(!pos,!pos));