Commit aab7a47d authored by POTTIER Francois's avatar POTTIER Francois
Browse files

Add three new test files from zipperposition.1.5.

parent 6b50c3d0
Pipeline #125456 passed with stages
in 25 seconds
Grammar has 23 nonterminal symbols, among which 1 start symbols.
Grammar has 44 terminal symbols.
Grammar has 80 productions.
nullable(type_simple) = false
nullable(type_qid) = false
nullable(typ) = false
nullable(term_simple) = false
nullable(term) = false
nullable(separated_nonempty_list(COMMA,env_decl)) = false
nullable(qid) = false
nullable(proofheaders) = false
nullable(pre_typ) = false
nullable(nonempty_list(term_simple)) = false
nullable(nonempty_list(compact_arg)) = false
nullable(loption(separated_nonempty_list(COMMA,env_decl))) = true
nullable(list(type_simple)) = true
nullable(kind) = false
nullable(goal) = false
nullable(file) = false
nullable(env_decl) = false
nullable(env) = false
nullable(declared_or_defined_id) = false
nullable(complex_type) = false
nullable(compact_arg) = false
nullable(body) = false
nullable(arrow_type) = false
first(type_simple) = QID LPAREN ID
first(type_qid) = QID ID
first(typ) = TERM PROP
first(term_simple) = TRUE QID OR NUMBER NOT LPAREN IMP ID FALSE EX_TYPE EX EQV EQUAL CCARR AND ALL_TYPE ALL
first(term) = error TRUE QID OR NUMBER NOT LPAREN IMP ID FALSE EX_TYPE EX EQV EQUAL CCARR AND ALL_TYPE ALL
first(separated_nonempty_list(COMMA,env_decl)) = ID
first(qid) = QID ID
first(proofheaders) = error QID LBRACK ID DEFKW BEGIN_VAR BEGIN_TYPEALIAS BEGIN_TY BEGIN_HYP BEGINNAME BEGINHEADER
first(pre_typ) = QID LPAREN ID CCARR
first(nonempty_list(term_simple)) = TRUE QID OR NUMBER NOT LPAREN IMP ID FALSE EX_TYPE EX EQV EQUAL CCARR AND ALL_TYPE ALL
first(nonempty_list(compact_arg)) = LPAREN
first(loption(separated_nonempty_list(COMMA,env_decl))) = ID
first(list(type_simple)) = QID LPAREN ID
first(kind) = TYPE ID
first(goal) = ID
first(file) = error QID LBRACK ID DEFKW BEGINPROOF
first(env_decl) = ID
first(env) = LBRACK
first(declared_or_defined_id) = QID ID
first(complex_type) = TERM PROP LPAREN
first(compact_arg) = LPAREN
first(body) = QID LBRACK ID DEFKW
first(arrow_type) = TERM PROP LPAREN ID
minimal(type_simple) = (* 1 *) ID
minimal(type_qid) = (* 1 *) ID
minimal(typ) = (* 1 *) PROP
minimal(term_simple) = (* 1 *) QID
minimal(term) = (* 1 *) error
minimal(separated_nonempty_list(COMMA,env_decl)) = (* 1 *) ID
minimal(qid) = (* 1 *) QID
minimal(proofheaders) = (* 1 *) error
minimal(pre_typ) = (* 1 *) ID
minimal(nonempty_list(term_simple)) = (* 1 *) QID
minimal(nonempty_list(compact_arg)) = (* 5 *) LPAREN ID COLON PROP RPAREN
minimal(loption(separated_nonempty_list(COMMA,env_decl))) = (* 0 *)
minimal(list(type_simple)) = (* 0 *)
minimal(kind) = (* 1 *) TYPE
minimal(goal) = (* 5 *) ID COLON PROOF error DOT
minimal(file) = (* 1 *) error
minimal(env_decl) = (* 1 *) ID
minimal(env) = (* 2 *) LBRACK RBRACK
minimal(declared_or_defined_id) = (* 1 *) ID
minimal(complex_type) = (* 1 *) PROP
minimal(compact_arg) = (* 5 *) LPAREN ID COLON PROP RPAREN
minimal(body) = (* 5 *) ID COLON PROOF error DOT
minimal(arrow_type) = (* 1 *) PROP
follow(type_simple) = TRUE RPAREN REW RBRACK QID OR NUMBER NOT LPAREN IMP ID FALSE EX_TYPE EX EQV EQUAL END_VAR END_TYPEALIAS END_HYP DOUBLE_ARROW DOT DEF COMMA CCARR ARROW AND ALL_TYPE ALL
follow(type_qid) = TRUE RPAREN REW RBRACK QID OR NUMBER NOT LPAREN IMP ID FALSE EX_TYPE EX EQV EQUAL END_VAR END_TYPEALIAS END_HYP DOUBLE_ARROW DOT DEF COMMA CCARR ARROW AND ALL_TYPE ALL
follow(typ) = RPAREN RBRACK END_VAR DOUBLE_ARROW DOT DEF COMMA ARROW
follow(term_simple) = TRUE RPAREN REW QID OR NUMBER NOT LPAREN IMP ID FALSE EX_TYPE EX EQV EQUAL END_HYP DOUBLE_ARROW DOT CCARR AND ALL_TYPE ALL
follow(term) = RPAREN REW DOUBLE_ARROW DOT
follow(separated_nonempty_list(COMMA,env_decl)) = RBRACK
follow(qid) = TRUE RPAREN REW QID OR NUMBER NOT LPAREN IMP ID FALSE EX_TYPE EX EQV EQUAL END_HYP DOUBLE_ARROW DOT CCARR AND ALL_TYPE ALL
follow(proofheaders) = EOF
follow(pre_typ) = RPAREN
follow(nonempty_list(term_simple)) = RPAREN REW DOUBLE_ARROW DOT
follow(nonempty_list(compact_arg)) = COLON
follow(loption(separated_nonempty_list(COMMA,env_decl))) = RBRACK
follow(list(type_simple)) = RPAREN
follow(kind) = DOT
follow(goal) = EOF ENDPROOF
follow(file) = #
follow(env_decl) = RBRACK COMMA
follow(env) = error TRUE QID OR NUMBER NOT LPAREN IMP ID FALSE EX_TYPE EX EQV EQUAL CCARR AND ALL_TYPE ALL
follow(declared_or_defined_id) = LPAREN
follow(complex_type) = DOUBLE_ARROW ARROW
follow(compact_arg) = LPAREN COLON
follow(body) = EOF ENDPROOF
follow(arrow_type) = RPAREN RBRACK DOT COMMA
Built an LR(0) automaton with 227 states.
The grammar is SLR(1).
The construction mode is pager.
Built an LR(1) automaton with 227 states.
69 out of 227 states have a default reduction.
80 out of 227 states are represented.
5 out of 70 symbols keep track of their start position.
4 out of 70 symbols keep track of their end position.
34 out of 81 productions exploit shiftreduce optimization.
1 out of 227 states can peek at an error.
The generated parser cannot raise Error.
564 functions before inlining, 67 functions after inlining.
/* Copyright 2005 INRIA */
/* Copyright 2014 Ali Assaf */
/* Copyright 2014 Raphaël Cauderlier */
%{
open Logtk
module T = Ast_dk
module L = ParseLocation
%}
%token <string> ID QID NUMBER
%token COLON DOT DOUBLE_ARROW DEF ARROW
%token TYPE TERM PROOF CCARR PROP
%token LPAREN RPAREN EOF
%token LBRACK COMMA RBRACK REW DEFKW
%token TRUE FALSE NOT AND OR IMP EQV ALL EX ALL_TYPE EX_TYPE EQUAL
%token BEGINPROOF
%token BEGIN_TYPEALIAS
%token BEGIN_TY
%token BEGIN_VAR
%token BEGIN_HYP
%token END_TYPEALIAS
%token END_VAR
%token END_HYP
%token <string> BEGINNAME
%token BEGINHEADER
%token ENDPROOF
%start file
%type <Ast_dk.statement list> file
%type <Ast_dk.ty> typ
%type <Ast_dk.term> term
%type <Ast_dk.ty> term_simple
%%
file:
| b=body EOF { b }
| BEGINPROOF h=proofheaders EOF { h }
| error {
let loc = L.mk_pos $startpos $endpos in
UntypedAST.errorf loc "expected problem"
}
goal:
| name=ID COLON PROOF t=term DOT
{ let loc = L.mk_pos $startpos $endpos in
T.mk_goal ~loc ~name t }
proofheaders:
| BEGINNAME h=proofheaders { h }
| BEGINHEADER h=proofheaders { h }
| BEGIN_TY id=ID h=proofheaders { T.mk_ty_decl id T.tType :: h }
| BEGIN_TYPEALIAS f=ID DEF ty=type_simple END_TYPEALIAS h=proofheaders
{ (* Type aliases are substituted in the parser *)
(* This does not work because it does not substitute
the alias in already-parsed input.
TODO: give it to the typer. *)
T.add_alias f ty;
h
}
| BEGIN_VAR ID COLON typ END_VAR h=proofheaders { h }
| BEGIN_HYP ID COLON PROOF term_simple END_HYP h=proofheaders { h }
| b=body ENDPROOF { b }
| error {
let loc = L.mk_pos $startpos $endpos in
UntypedAST.errorf loc "expected proofheader"
}
qid:
| x=QID { T.find_alias x ~or_else:(T.var x) }
| x=ID { T.find_alias x ~or_else:(T.var x) }
term_simple:
| x=qid { x }
| x=NUMBER { T.mk_int x } (* TODO: use nat *)
| TRUE { T.true_ }
| FALSE { T.false_ }
| NOT t=term_simple { T.not_ t }
| AND t=term_simple u=term_simple { T.and_ [t;u] }
| OR t=term_simple u=term_simple { T.or_ [t;u] }
| IMP t=term_simple u=term_simple { T.imply t u }
| EQV t=term_simple u=term_simple { T.equiv t u }
| ALL ty=type_simple LPAREN x=ID COLON complex_type DOUBLE_ARROW body=term RPAREN
{ T.forall [ (T.v x, Some ty) ] body }
| EX ty=type_simple LPAREN x=ID COLON complex_type DOUBLE_ARROW body=term RPAREN
{ T.exists [ (T.v x, Some ty) ] body }
| ALL_TYPE LPAREN x=ID COLON TYPE DOUBLE_ARROW body=term RPAREN
{ T.forall [ (T.v x, Some T.tType) ] body }
| EX_TYPE LPAREN x=ID COLON TYPE DOUBLE_ARROW body=term RPAREN
{ T.exists [ (T.v x, Some T.tType) ] body }
| EQUAL ty=type_simple t=term_simple u=term_simple { T.eq t (T.cast u ty) }
| LPAREN t=term RPAREN { t }
| x=ID COLON ty=typ DOUBLE_ARROW body=term_simple
{ T.mk_fun [ (T.v x, Some ty) ] body }
| x=ID DEF t=term DOUBLE_ARROW u=term_simple
{ T.let_ [ (T.v x, t) ] u }
| CCARR a=type_simple b=type_simple
{ T.mk_arrow a b }
term:
| t=term_simple { t }
| f=term_simple l=term_simple+ { T.mk_app f l }
| error {
let loc = L.mk_pos $startpos $endpos in
UntypedAST.errorf loc "expected term"
}
type_qid:
| x=ID { T.find_alias x ~or_else:(T.mk_var_t x) }
| x=QID { T.find_alias x ~or_else:(T.mk_var_t x) }
type_simple:
| ty=type_qid { ty }
| LPAREN ty=pre_typ RPAREN { ty }
pre_typ:
| f=type_simple l=type_simple* { T.mk_app f l }
| CCARR a=type_simple b=type_simple { T.mk_arrow a b }
typ:
| TERM ty=type_simple { ty }
| PROP { T.ty_prop }
complex_type :
| ty=typ { ty }
| LPAREN ty=arrow_type RPAREN { ty }
arrow_type :
| ty=typ { ty }
| a=complex_type ARROW b=arrow_type { T.mk_arrow a b }
| x=ID COLON TYPE ARROW body=arrow_type
{ T.forall_ty [T.V x, None] body }
kind :
| TYPE { T.tType }
| ID COLON TYPE ARROW ty=kind { T.mk_arrow T.tType ty }
declared_or_defined_id:
| x=ID { x }
| x=QID { x }
body:
| id=ID COLON ty=kind DOT l=body { T.mk_ty_decl id ty :: l }
| id=QID COLON ty=kind DOT l=body { T.mk_ty_decl id ty :: l }
| name=ID COLON PROOF t=term DOT l=body { T.mk_assert ~name t :: l }
| name=QID COLON PROOF t=term DOT l=body { T.mk_assert ~name t :: l }
| id=ID COLON ty=arrow_type DOT l=body { T.mk_ty_decl id ty :: l }
| id=QID COLON ty=arrow_type DOT l=body { T.mk_ty_decl id ty :: l }
| DEFKW id=ID COLON ty=arrow_type DOT l=body { T.mk_ty_decl id ty :: l }
| DEFKW id=QID COLON ty=arrow_type DOT l=body { T.mk_ty_decl id ty :: l }
| DEFKW id=ID COLON ty=typ DEF body=term DOT l=body
{ let loc = L.mk_pos $startpos $endpos in
T.mk_def ~loc id ty body :: l }
| DEFKW id=QID COLON ty=typ DEF body=term DOT l=body
{ let loc = L.mk_pos $startpos $endpos in
T.mk_def ~loc id ty body :: l }
| DEFKW id=declared_or_defined_id args=compact_arg+ COLON ty_ret=typ DEF body=term DOT l=body
{ let loc = L.mk_pos $startpos $endpos in
let ty_args = List.map snd args in
let ty = T.mk_arrow_l ty_args ty_ret in
let args = List.map (fun (id,ty) -> T.V id, Some ty) args in
T.mk_def ~loc id ty (T.mk_fun args body) :: l
}
| env=env lhs=term REW rhs=term DOT l=body
{ let loc = L.mk_pos $startpos $endpos in
let t = T.mk_forall env (T.eq lhs rhs) in
T.mk_rewrite ~loc t :: l
}
| g=goal { [g] }
compact_arg:
| LPAREN id=ID COLON ty=arrow_type RPAREN { id, ty }
env_decl:
| id=ID COLON ty=arrow_type { T.v id, Some ty }
| id=ID COLON TYPE { T.v id, Some T.tType }
| id=ID { T.v id, None }
env:
| LBRACK l=separated_list(COMMA, env_decl) RBRACK { l }
%%
%{
open Logtk
module T = Ast_dk
module L = ParseLocation
%}
%start file
%token ALL
%token ALL_TYPE
%token AND
%token ARROW
%token BEGINHEADER
%token <string> BEGINNAME
%token BEGINPROOF
%token BEGIN_HYP
%token BEGIN_TY
%token BEGIN_TYPEALIAS
%token BEGIN_VAR
%token CCARR
%token COLON
%token COMMA
%token DEF
%token DEFKW
%token DOT
%token DOUBLE_ARROW
%token ENDPROOF
%token END_HYP
%token END_TYPEALIAS
%token END_VAR
%token EOF
%token EQUAL
%token EQV
%token EX
%token EX_TYPE
%token FALSE
%token <string> ID
%token IMP
%token LBRACK
%token LPAREN
%token NOT
%token <string> NUMBER
%token OR
%token PROOF
%token PROP
%token <string> QID
%token RBRACK
%token REW
%token RPAREN
%token TERM
%token TRUE
%token TYPE
%type <Ast_dk.statement list> file
%type <Ast_dk.term> term
%type <Ast_dk.ty> term_simple
%type <Ast_dk.ty> typ
%%
loption_separated_nonempty_list_COMMA_env_decl__:
{ ( [] )}
| x = separated_nonempty_list_COMMA_env_decl_
{ ( x )}
list_type_simple_:
{ ( [] )}
| x = type_simple xs = list_type_simple_
{ ( x :: xs )}
nonempty_list_compact_arg_:
x = compact_arg
{ ( [ x ] )}
| x = compact_arg xs = nonempty_list_compact_arg_
{ ( x :: xs )}
nonempty_list_term_simple_:
x = term_simple
{ ( [ x ] )}
| x = term_simple xs = nonempty_list_term_simple_
{ ( x :: xs )}
separated_nonempty_list_COMMA_env_decl_:
x = env_decl
{ ( [ x ] )}
| x = env_decl _2 = COMMA xs = separated_nonempty_list_COMMA_env_decl_
{ ( x :: xs )}
file:
b = body _2 = EOF
{ ( b )}
| _1 = BEGINPROOF h = proofheaders _3 = EOF
{ ( h )}
| _1 = error
{let _endpos = _endpos__1_ in
let _startpos = _startpos__1_ in
(
let loc = L.mk_pos _startpos _endpos in
UntypedAST.errorf loc "expected problem"
)}
goal:
name = ID _2 = COLON _3 = PROOF t = term _5 = DOT
{let _endpos = _endpos__5_ in
let _startpos = _startpos_name_ in
( let loc = L.mk_pos _startpos _endpos in
T.mk_goal ~loc ~name t )}
proofheaders:
_1 = BEGINNAME h = proofheaders
{ ( h )}
| _1 = BEGINHEADER h = proofheaders
{ ( h )}
| _1 = BEGIN_TY id = ID h = proofheaders
{ ( T.mk_ty_decl id T.tType :: h )}
| _1 = BEGIN_TYPEALIAS f = ID _3 = DEF ty = type_simple _5 = END_TYPEALIAS h = proofheaders
{ ( (* Type aliases are substituted in the parser *)
(* This does not work because it does not substitute
the alias in already-parsed input.
TODO: give it to the typer. *)
T.add_alias f ty;
h
)}
| _1 = BEGIN_VAR _2 = ID _3 = COLON _4 = typ _5 = END_VAR h = proofheaders
{ ( h )}
| _1 = BEGIN_HYP _2 = ID _3 = COLON _4 = PROOF _5 = term_simple _6 = END_HYP h = proofheaders
{ ( h )}
| b = body _2 = ENDPROOF
{ ( b )}
| _1 = error
{let _endpos = _endpos__1_ in
let _startpos = _startpos__1_ in
(
let loc = L.mk_pos _startpos _endpos in
UntypedAST.errorf loc "expected proofheader"
)}
qid:
x = QID
{ ( T.find_alias x ~or_else:(T.var x) )}
| x = ID
{ ( T.find_alias x ~or_else:(T.var x) )}
term_simple:
x = qid
{ ( x )}
| x = NUMBER
{ ( T.mk_int x )}
| _1 = TRUE
{ ( T.true_ )}
| _1 = FALSE
{ ( T.false_ )}
| _1 = NOT t = term_simple
{ ( T.not_ t )}
| _1 = AND t = term_simple u = term_simple
{ ( T.and_ [t;u] )}
| _1 = OR t = term_simple u = term_simple
{ ( T.or_ [t;u] )}
| _1 = IMP t = term_simple u = term_simple
{ ( T.imply t u )}
| _1 = EQV t = term_simple u = term_simple
{ ( T.equiv t u )}
| _1 = ALL ty = type_simple _3 = LPAREN x = ID _5 = COLON _6 = complex_type _7 = DOUBLE_ARROW body = term _9 = RPAREN
{ ( T.forall [ (T.v x, Some ty) ] body )}
| _1 = EX ty = type_simple _3 = LPAREN x = ID _5 = COLON _6 = complex_type _7 = DOUBLE_ARROW body = term _9 = RPAREN
{ ( T.exists [ (T.v x, Some ty) ] body )}
| _1 = ALL_TYPE _2 = LPAREN x = ID _4 = COLON _5 = TYPE _6 = DOUBLE_ARROW body = term _8 = RPAREN
{ ( T.forall [ (T.v x, Some T.tType) ] body )}
| _1 = EX_TYPE _2 = LPAREN x = ID _4 = COLON _5 = TYPE _6 = DOUBLE_ARROW body = term _8 = RPAREN
{ ( T.exists [ (T.v x, Some T.tType) ] body )}
| _1 = EQUAL ty = type_simple t = term_simple u = term_simple
{ ( T.eq t (T.cast u ty) )}
| _1 = LPAREN t = term _3 = RPAREN
{ ( t )}
| x = ID _2 = COLON ty = typ _4 = DOUBLE_ARROW body = term_simple
{ ( T.mk_fun [ (T.v x, Some ty) ] body )}
| x = ID _2 = DEF t = term _4 = DOUBLE_ARROW u = term_simple
{ ( T.let_ [ (T.v x, t) ] u )}
| _1 = CCARR a = type_simple b = type_simple
{ ( T.mk_arrow a b )}
term:
t = term_simple
{ ( t )}
| f = term_simple l = nonempty_list_term_simple_
{ ( T.mk_app f l )}
| _1 = error
{let _endpos = _endpos__1_ in
let _startpos = _startpos__1_ in
(
let loc = L.mk_pos _startpos _endpos in
UntypedAST.errorf loc "expected term"
)}
type_qid:
x = ID
{ ( T.find_alias x ~or_else:(T.mk_var_t x) )}
| x = QID
{ ( T.find_alias x ~or_else:(T.mk_var_t x) )}
type_simple:
ty = type_qid
{ ( ty )}
| _1 = LPAREN ty = pre_typ _3 = RPAREN
{ ( ty )}
pre_typ:
f = type_simple l = list_type_simple_
{ ( T.mk_app f l )}
| _1 = CCARR a = type_simple b = type_simple
{ ( T.mk_arrow a b )}
typ:
_1 = TERM ty = type_simple
{ ( ty )}
| _1 = PROP
{ ( T.ty_prop )}
complex_type:
ty = typ
{ ( ty )}
| _1 = LPAREN ty = arrow_type _3 = RPAREN
{ ( ty )}
arrow_type:
ty = typ
{ ( ty )}
| a = complex_type _2 = ARROW b = arrow_type
{ ( T.mk_arrow a b )}
| x = ID _2 = COLON _3 = TYPE _4 = ARROW body = arrow_type
{ ( T.forall_ty [T.V x, None] body )}
kind:
_1 = TYPE
{ ( T.tType )}
| _1 = ID _2 = COLON _3 = TYPE _4 = ARROW ty = kind
{ ( T.mk_arrow T.tType ty )}
declared_or_defined_id:
x = ID
{ ( x )}
| x = QID
{ ( x )}
body:
id = ID _2 = COLON ty = kind _4 = DOT l = body
{ ( T.mk_ty_decl id ty :: l )}
| id = QID _2 = COLON ty = kind _4 = DOT l = body
{ ( T.mk_ty_decl id ty :: l )}
| name = ID _2 = COLON _3 = PROOF t = term _5 = DOT l = body
{ ( T.mk_assert ~name t :: l )}
| name = QID _2 = COLON _3 = PROOF t = term _5 = DOT l = body
{ ( T.mk_assert ~name t :: l )}
| id = ID _2 = COLON ty = arrow_type _4 = DOT l = body
{ ( T.mk_ty_decl id ty :: l )}
| id = QID _2 = COLON ty = arrow_type _4 = DOT l = body
{ ( T.mk_ty_decl id ty :: l )}
| _1 = DEFKW id = ID _3 = COLON ty = arrow_type _5 = DOT l = body
{ ( T.mk_ty_decl id ty :: l )}
| _1 = DEFKW id = QID _3 = COLON ty = arrow_type _5 = DOT l = body
{ ( T.mk_ty_decl id ty :: l )}
| _1 = DEFKW id = ID _3 = COLON ty = typ _5 = DEF body = term _7 = DOT l = body
{let _endpos = _endpos_l_ in
let _startpos = _startpos__1_ in
( let loc = L.mk_pos _startpos _endpos in
T.mk_def ~loc id ty body :: l )}
| _1 = DEFKW id = QID _3 = COLON ty = typ _5 = DEF body = term _7 = DOT l = body
{let _endpos = _endpos_l_ in
let _startpos = _startpos__1_ in
( let loc = L.mk_pos _startpos _endpos in
T.mk_def ~loc id ty body :: l )}
| _1 = DEFKW id = declared_or_defined_id args = nonempty_list_compact_arg_ _4 = COLON ty_ret = typ _6 = DEF body = term _8 = DOT l = body
{let _endpos = _endpos_l_ in
let _startpos = _startpos__1_ in
( let loc = L.mk_pos _startpos _endpos in
let ty_args = List.map snd args in
let ty = T.mk_arrow_l ty_args ty_ret in
let args = List.map (fun (id,ty) -> T.V id, Some ty) args in
T.mk_def ~loc id ty (T.mk_fun args body) :: l
)}
| env = env lhs = term _3 = REW rhs = term _5 = DOT l = body
{let _endpos = _endpos_l_ in
let _startpos = _startpos_env_ in
( let loc = L.mk_pos _startpos _endpos in
let t = T.mk_forall env (T.eq lhs rhs) in
T.mk_rewrite ~loc t :: l
)}
| g = goal
{ ( [g] )}
compact_arg:
_1 = LPAREN id = ID _3 = COLON ty = arrow_type _5 = RPAREN
{ ( id, ty )}
env_decl:
id = ID _2 = COLON ty = arrow_type
{ ( T.v id, Some ty )}
| id = ID _2 = COLON _3 = TYPE
{ ( T.v id, Some T.tType )}
| id = ID
{ ( T.v id, None )}
env:
_1 = LBRACK xs = loption_separated_nonempty_list_COMMA_env_decl__ _3 = RBRACK
{let l = ( xs ) in
( l )}
%%
This diff is collapsed.