diff --git a/AST.ml b/AST.ml index 6f62f6e98..940b562c4 100644 --- a/AST.ml +++ b/AST.ml @@ -142,45 +142,9 @@ type 'a braces = (lbrace * 'a * rbrace) reg (* The Abstract Syntax Tree *) -type ttrue = TTrue -type tfalse = TFalse -type ('a, 'type_expr_typecheck) gadt_if = - Present : 'a -> ('a, ttrue) gadt_if +type t = < ty: unit > ast -(* It is possible to further ensure well-typedness at the meta level - by using the following constraint: - - type ttrue = [`True] - type tfalse = [`False] - - type 'x x_sig = 'x - constraint 'x = < ty: 'ty; - type_expr_typecheck: [< `True | `False] > - - we could also use a single selector for type_expr, as long as - the fields are monotonic: - - type z = [`Z] - type 'i s = [`S of 'i] - type 'is type_level_int = [< `S of 'i | `Z] - constraint 'i = 'prev type_level_int - - type parse_phase = z - type typecheck_phase = z s - type further_phase = z s s - - type 'x x_sig = 'x - constraint 'x = < ty: 'ty; - type_expr: 'type_expr > - - These schemes provide more guidance but the simple one below is - sufficient. - *) -type 'x x_sig = 'x -constraint 'x = < annot: 'type_annotation; - type_expr_typecheck: 'bool1 > - -type 'x ast = { +and 'x ast = { types : 'x type_decl reg list; constants : 'x const_decl reg list; parameter : 'x parameter_decl reg; @@ -190,7 +154,6 @@ type 'x ast = { block : 'x block reg; eof : eof } -constraint 'x = 'x x_sig and 'x parameter_decl = { kwd_parameter : kwd_parameter; @@ -199,21 +162,18 @@ and 'x parameter_decl = { param_type : 'x type_expr; terminator : semi option } -constraint 'x = 'x x_sig and 'x storage_decl = { kwd_storage : kwd_storage; store_type : 'x type_expr; terminator : semi option } -constraint 'x = 'x x_sig and 'x operations_decl = { kwd_operations : kwd_operations; op_type : 'x type_expr; terminator : semi option } -constraint 'x = 'x x_sig (* Type declarations *) @@ -224,79 +184,32 @@ and 'x type_decl = { type_expr : 'x type_expr; terminator : semi option } -constraint 'x = 'x x_sig and 'x type_expr = - Prod of ('x cartesian, ttrue) gadt_if -| Sum of (('x variant, vbar) nsepseq reg, ttrue) gadt_if -| Record of ('x record_type, ttrue) gadt_if -| TypeApp of (('x type_name * 'x type_tuple) reg, ttrue) gadt_if -| ParType of ('x type_expr par, ttrue) gadt_if -| TAlias of ('x variable, ttrue) gadt_if - -| Function of (('x type_expr list) * 'x type_expr, 'type_expr_typecheck) gadt_if -| Mutable of ('x type_expr, 'type_expr_typecheck) gadt_if -| Unit of (unit, 'type_expr_typecheck) gadt_if -constraint 'x = < type_expr_typecheck: 'type_expr_typecheck; - .. > -constraint 'x = 'x x_sig - -(* -and 'x type_expr = ('x cartesian, - ('x variant, vbar) nsepseq reg, - 'x record_type, - ('x type_name * 'x type_tuple) reg, - 'x type_expr par, - 'x variable, - - ('x type_expr list) * 'x type_expr, - 'x type_expr, - unit, - - 'type_expr_parse, - 'type_expr_typecheck) type_expr_gadt -constraint 'x = < type_expr_parse: 'type_expr_parse; - type_expr_typecheck: 'type_expr_typecheck; - .. > -constraint 'x = 'x x_sig - -and ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'type_expr_parse, 'type_expr_typecheck) type_expr_gadt = - Prod : 'a -> ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, ttrue, ttrue) type_expr_gadt -| Sum : 'b -> ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, ttrue, ttrue) type_expr_gadt -| Record : 'c -> ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, ttrue, ttrue) type_expr_gadt -| TypeApp : 'd -> ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, ttrue, ttrue) type_expr_gadt -| ParType : 'e -> ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, ttrue, ttrue) type_expr_gadt -| TAlias : 'f -> ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, ttrue, ttrue) type_expr_gadt - -| Function : 'g -> ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, tfalse, ttrue) type_expr_gadt -| Mutable : 'h -> ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, tfalse, ttrue) type_expr_gadt -| Unit : 'i -> ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, tfalse, ttrue) type_expr_gadt - *) + Prod of 'x cartesian +| Sum of ('x variant, vbar) nsepseq reg +| Record of 'x record_type +| TypeApp of ('x type_name * 'x type_tuple) reg +| ParType of 'x type_expr par +| TAlias of 'x variable and 'x cartesian = ('x type_expr, times) nsepseq reg -constraint 'x = 'x x_sig and 'x variant = ('x constr * kwd_of * 'x cartesian) reg -constraint 'x = 'x x_sig and 'x record_type = (kwd_record * 'x field_decls * kwd_end) reg -constraint 'x = 'x x_sig and 'x field_decls = ('x field_decl, semi) nsepseq -constraint 'x = 'x x_sig and 'x field_decl = ('x variable * colon * 'x type_expr) reg -constraint 'x = 'x x_sig and 'x type_tuple = ('x type_name, comma) nsepseq par -constraint 'x = 'x x_sig (* Function and procedure declarations *) and 'x lambda_decl = FunDecl of 'x fun_decl reg | ProcDecl of 'x proc_decl reg -constraint 'x = 'x x_sig and 'x fun_decl = { kwd_function : kwd_function; @@ -311,7 +224,6 @@ and 'x fun_decl = { return : 'x expr; terminator : semi option } -constraint 'x = 'x x_sig and 'x proc_decl = { kwd_procedure : kwd_procedure; @@ -322,21 +234,16 @@ and 'x proc_decl = { block : 'x block reg; terminator : semi option } -constraint 'x = 'x x_sig and 'x parameters = ('x param_decl, semi) nsepseq par -constraint 'x = 'x x_sig and 'x param_decl = ParamConst of 'x param_const | ParamVar of 'x param_var -constraint 'x = 'x x_sig and 'x param_const = (kwd_const * 'x variable * colon * 'x type_expr) reg -constraint 'x = 'x x_sig and 'x param_var = (kwd_var * 'x variable * colon * 'x type_expr) reg -constraint 'x = 'x x_sig and 'x block = { opening : kwd_begin; @@ -344,13 +251,11 @@ and 'x block = { terminator : semi option; close : kwd_end } -constraint 'x = 'x x_sig and 'x local_decl = LocalLam of 'x lambda_decl | LocalConst of 'x const_decl reg | LocalVar of 'x var_decl reg -constraint 'x = 'x x_sig and 'x const_decl = { kwd_const : kwd_const; @@ -361,7 +266,6 @@ and 'x const_decl = { init : 'x expr; terminator : semi option } -constraint 'x = 'x x_sig and 'x var_decl = { kwd_var : kwd_var; @@ -372,15 +276,12 @@ and 'x var_decl = { init : 'x expr; terminator : semi option } -constraint 'x = 'x x_sig and 'x instructions = ('x instruction, semi) nsepseq reg -constraint 'x = 'x x_sig and 'x instruction = Single of 'x single_instr | Block of 'x block reg -constraint 'x = 'x x_sig and 'x single_instr = Cond of 'x conditional reg @@ -390,7 +291,6 @@ and 'x single_instr = | ProcCall of 'x fun_call | Null of kwd_null | Fail of (kwd_fail * 'x expr) reg -constraint 'x = 'x x_sig and 'x conditional = { kwd_if : kwd_if; @@ -400,7 +300,6 @@ and 'x conditional = { kwd_else : kwd_else; ifnot : 'x instruction } -constraint 'x = 'x x_sig and 'x match_instr = { kwd_match : kwd_match; @@ -410,29 +309,22 @@ and 'x match_instr = { cases : 'x cases; kwd_end : kwd_end } -constraint 'x = 'x x_sig and 'x cases = ('x case, vbar) nsepseq reg -constraint 'x = 'x x_sig and 'x case = ('x pattern * arrow * 'x instruction) reg -constraint 'x = 'x x_sig and 'x ass_instr = ('x variable * ass * 'x expr) reg -constraint 'x = 'x x_sig and 'x loop = While of 'x while_loop | For of 'x for_loop -constraint 'x = 'x x_sig and 'x while_loop = (kwd_while * 'x expr * 'x block reg) reg -constraint 'x = 'x x_sig and 'x for_loop = ForInt of 'x for_int reg | ForCollect of 'x for_collect reg -constraint 'x = 'x x_sig and 'x for_int = { kwd_for : kwd_for; @@ -443,7 +335,6 @@ and 'x for_int = { step : (kwd_step * 'x expr) option; block : 'x block reg } -constraint 'x = 'x x_sig and 'x for_collect = { kwd_for : kwd_for; @@ -453,7 +344,6 @@ and 'x for_collect = { expr : 'x expr; block : 'x block reg } -constraint 'x = 'x x_sig (* Expressions *) @@ -493,43 +383,33 @@ and 'x expr = | SomeApp of (c_Some * 'x arguments) reg | MapLookUp of 'x map_lookup reg | ParExpr of 'x expr par -constraint 'x = 'x x_sig and 'x tuple = ('x expr, comma) nsepseq par -constraint 'x = 'x x_sig and 'x empty_list = (lbracket * rbracket * colon * 'x type_expr) par -constraint 'x = 'x x_sig and 'x empty_set = (lbrace * rbrace * colon * 'x type_expr) par -constraint 'x = 'x x_sig and 'x none_expr = (c_None * colon * 'x type_expr) par -constraint 'x = 'x x_sig and 'x fun_call = ('x fun_name * 'x arguments) reg -constraint 'x = 'x x_sig and 'x arguments = 'x tuple -constraint 'x = 'x x_sig and 'x constr_app = ('x constr * 'x arguments) reg -constraint 'x = 'x x_sig and 'x map_lookup = { map_name : 'x variable; selector : dot; index : 'x expr brackets } -constraint 'x = 'x x_sig (* Patterns *) and 'x pattern = ('x core_pattern, cons) nsepseq reg -constraint 'x = 'x x_sig and 'x core_pattern = PVar of Lexer.lexeme reg @@ -544,39 +424,22 @@ and 'x core_pattern = | PSome of (c_Some * 'x core_pattern par) reg | PList of 'x list_pattern | PTuple of ('x core_pattern, comma) nsepseq par -constraint 'x = 'x x_sig and 'x list_pattern = Sugar of ('x core_pattern, comma) sepseq brackets | Raw of ('x core_pattern * cons * 'x pattern) par -constraint 'x = 'x x_sig - -(* Variations on the AST *) - -type parse_phase = < - annot: unit; - type_expr_typecheck: tfalse; -> - -type typecheck_phase = < - annot: typecheck_phase type_expr; - type_expr_typecheck: ttrue; -> - -type t = parse_phase ast (* Projecting regions *) open! Region -let type_expr_to_region : parse_phase type_expr -> region = function - Prod (Present node) -> node.region -| Sum (Present node) -> node.region -| Record (Present node) -> node.region -| TypeApp (Present node) -> node.region -| ParType (Present node) -> node.region -| TAlias (Present node) -> node.region -| _ -> . +let type_expr_to_region = function + Prod node -> node.region +| Sum node -> node.region +| Record node -> node.region +| TypeApp node -> node.region +| ParType node -> node.region +| TAlias node -> node.region let expr_to_region = function Or {region; _} diff --git a/AST.mli b/AST.mli index d89d92b25..cb6fbcd2b 100644 --- a/AST.mli +++ b/AST.mli @@ -126,45 +126,9 @@ type 'a braces = (lbrace * 'a * rbrace) reg (* The Abstract Syntax Tree *) -type ttrue = TTrue -type tfalse = TFalse -type ('a, 'type_expr_typecheck) gadt_if = - Present : 'a -> ('a, ttrue) gadt_if +type t = < ty:unit > ast -(* It is possible to further ensure well-typedness at the meta level - by using the following constraint: - - type ttrue = [`True] - type tfalse = [`False] - - type 'x x_sig = 'x - constraint 'x = < annot: 'ty; - type_expr_typecheck: [< `True | `False] > - - we could also use a single selector for type_expr, as long as - the fields are monotonic: - - type z = [`Z] - type 'i s = [`S of 'i] - type 'is type_level_int = [< `S of 'i | `Z] - constraint 'i = 'prev type_level_int - - type parse_phase = z - type typecheck_phase = z s - type further_phase = z s s - - type 'x x_sig = 'x - constraint 'x = < annot: 'ty; - type_expr: 'type_expr > - - These schemes provide more guidance but the simple one below is - sufficient. - *) -type 'x x_sig = 'x -constraint 'x = < annot: 'type_annotation; - type_expr_typecheck: 'bool1 > - -type 'x ast = { +and 'x ast = { types : 'x type_decl reg list; constants : 'x const_decl reg list; parameter : 'x parameter_decl reg; @@ -174,7 +138,6 @@ type 'x ast = { block : 'x block reg; eof : eof } -constraint 'x = 'x x_sig and 'x parameter_decl = { kwd_parameter : kwd_parameter; @@ -183,21 +146,18 @@ and 'x parameter_decl = { param_type : 'x type_expr; terminator : semi option } -constraint 'x = 'x x_sig and 'x storage_decl = { kwd_storage : kwd_storage; store_type : 'x type_expr; terminator : semi option } -constraint 'x = 'x x_sig and 'x operations_decl = { kwd_operations : kwd_operations; op_type : 'x type_expr; terminator : semi option } -constraint 'x = 'x x_sig (* Type declarations *) @@ -208,47 +168,32 @@ and 'x type_decl = { type_expr : 'x type_expr; terminator : semi option } -constraint 'x = 'x x_sig and 'x type_expr = - Prod of ('x cartesian, ttrue) gadt_if -| Sum of (('x variant, vbar) nsepseq reg, ttrue) gadt_if -| Record of ('x record_type, ttrue) gadt_if -| TypeApp of (('x type_name * 'x type_tuple) reg, ttrue) gadt_if -| ParType of ('x type_expr par, ttrue) gadt_if -| TAlias of ('x variable, ttrue) gadt_if - -| Function of (('x type_expr list) * 'x type_expr, 'type_expr_typecheck) gadt_if -| Mutable of ('x type_expr, 'type_expr_typecheck) gadt_if -| Unit of (unit, 'type_expr_typecheck) gadt_if -constraint 'x = < type_expr_typecheck: 'type_expr_typecheck; - .. > -constraint 'x = 'x x_sig + Prod of 'x cartesian +| Sum of ('x variant, vbar) nsepseq reg +| Record of 'x record_type +| TypeApp of ('x type_name * 'x type_tuple) reg +| ParType of 'x type_expr par +| TAlias of 'x variable and 'x cartesian = ('x type_expr, times) nsepseq reg -constraint 'x = 'x x_sig and 'x variant = ('x constr * kwd_of * 'x cartesian) reg -constraint 'x = 'x x_sig and 'x record_type = (kwd_record * 'x field_decls * kwd_end) reg -constraint 'x = 'x x_sig and 'x field_decls = ('x field_decl, semi) nsepseq -constraint 'x = 'x x_sig and 'x field_decl = ('x variable * colon * 'x type_expr) reg -constraint 'x = 'x x_sig and 'x type_tuple = ('x type_name, comma) nsepseq par -constraint 'x = 'x x_sig (* Function and procedure declarations *) and 'x lambda_decl = FunDecl of 'x fun_decl reg | ProcDecl of 'x proc_decl reg -constraint 'x = 'x x_sig and 'x fun_decl = { kwd_function : kwd_function; @@ -263,7 +208,6 @@ and 'x fun_decl = { return : 'x expr; terminator : semi option } -constraint 'x = 'x x_sig and 'x proc_decl = { kwd_procedure : kwd_procedure; @@ -274,21 +218,16 @@ and 'x proc_decl = { block : 'x block reg; terminator : semi option } -constraint 'x = 'x x_sig and 'x parameters = ('x param_decl, semi) nsepseq par -constraint 'x = 'x x_sig and 'x param_decl = ParamConst of 'x param_const | ParamVar of 'x param_var -constraint 'x = 'x x_sig and 'x param_const = (kwd_const * 'x variable * colon * 'x type_expr) reg -constraint 'x = 'x x_sig and 'x param_var = (kwd_var * 'x variable * colon * 'x type_expr) reg -constraint 'x = 'x x_sig and 'x block = { opening : kwd_begin; @@ -296,13 +235,11 @@ and 'x block = { terminator : semi option; close : kwd_end } -constraint 'x = 'x x_sig and 'x local_decl = LocalLam of 'x lambda_decl | LocalConst of 'x const_decl reg | LocalVar of 'x var_decl reg -constraint 'x = 'x x_sig and 'x const_decl = { kwd_const : kwd_const; @@ -313,7 +250,6 @@ and 'x const_decl = { init : 'x expr; terminator : semi option } -constraint 'x = 'x x_sig and 'x var_decl = { kwd_var : kwd_var; @@ -324,15 +260,12 @@ and 'x var_decl = { init : 'x expr; terminator : semi option } -constraint 'x = 'x x_sig and 'x instructions = ('x instruction, semi) nsepseq reg -constraint 'x = 'x x_sig and 'x instruction = Single of 'x single_instr | Block of 'x block reg -constraint 'x = 'x x_sig and 'x single_instr = Cond of 'x conditional reg @@ -342,7 +275,6 @@ and 'x single_instr = | ProcCall of 'x fun_call | Null of kwd_null | Fail of (kwd_fail * 'x expr) reg -constraint 'x = 'x x_sig and 'x conditional = { kwd_if : kwd_if; @@ -352,7 +284,6 @@ and 'x conditional = { kwd_else : kwd_else; ifnot : 'x instruction } -constraint 'x = 'x x_sig and 'x match_instr = { kwd_match : kwd_match; @@ -362,29 +293,22 @@ and 'x match_instr = { cases : 'x cases; kwd_end : kwd_end } -constraint 'x = 'x x_sig and 'x cases = ('x case, vbar) nsepseq reg -constraint 'x = 'x x_sig and 'x case = ('x pattern * arrow * 'x instruction) reg -constraint 'x = 'x x_sig and 'x ass_instr = ('x variable * ass * 'x expr) reg -constraint 'x = 'x x_sig and 'x loop = While of 'x while_loop | For of 'x for_loop -constraint 'x = 'x x_sig and 'x while_loop = (kwd_while * 'x expr * 'x block reg) reg -constraint 'x = 'x x_sig and 'x for_loop = ForInt of 'x for_int reg | ForCollect of 'x for_collect reg -constraint 'x = 'x x_sig and 'x for_int = { kwd_for : kwd_for; @@ -395,7 +319,6 @@ and 'x for_int = { step : (kwd_step * 'x expr) option; block : 'x block reg } -constraint 'x = 'x x_sig and 'x for_collect = { kwd_for : kwd_for; @@ -405,7 +328,6 @@ and 'x for_collect = { expr : 'x expr; block : 'x block reg } -constraint 'x = 'x x_sig (* Expressions *) @@ -445,43 +367,33 @@ and 'x expr = | SomeApp of (c_Some * 'x arguments) reg | MapLookUp of 'x map_lookup reg | ParExpr of 'x expr par -constraint 'x = 'x x_sig and 'x tuple = ('x expr, comma) nsepseq par -constraint 'x = 'x x_sig and 'x empty_list = (lbracket * rbracket * colon * 'x type_expr) par -constraint 'x = 'x x_sig and 'x empty_set = (lbrace * rbrace * colon * 'x type_expr) par -constraint 'x = 'x x_sig and 'x none_expr = (c_None * colon * 'x type_expr) par -constraint 'x = 'x x_sig and 'x fun_call = ('x fun_name * 'x arguments) reg -constraint 'x = 'x x_sig and 'x arguments = 'x tuple -constraint 'x = 'x x_sig and 'x constr_app = ('x constr * 'x arguments) reg -constraint 'x = 'x x_sig and 'x map_lookup = { map_name : 'x variable; selector : dot; index : 'x expr brackets } -constraint 'x = 'x x_sig (* Patterns *) and 'x pattern = ('x core_pattern, cons) nsepseq reg -constraint 'x = 'x x_sig and 'x core_pattern = PVar of Lexer.lexeme reg @@ -496,30 +408,14 @@ and 'x core_pattern = | PSome of (c_Some * 'x core_pattern par) reg | PList of 'x list_pattern | PTuple of ('x core_pattern, comma) nsepseq par -constraint 'x = 'x x_sig and 'x list_pattern = Sugar of ('x core_pattern, comma) sepseq brackets | Raw of ('x core_pattern * cons * 'x pattern) par -constraint 'x = 'x x_sig - -(* Variations on the AST *) - -type parse_phase = < - annot: unit; - type_expr_typecheck: tfalse; -> - -type typecheck_phase = < - annot: typecheck_phase type_expr; - type_expr_typecheck: ttrue; -> - -type t = parse_phase ast (* Projecting regions *) -val type_expr_to_region : parse_phase type_expr -> Region.t +val type_expr_to_region : 'x type_expr -> Region.t val expr_to_region : 'x expr -> Region.t diff --git a/Parser.mly b/Parser.mly index 547e20e68..d3aca6dcc 100644 --- a/Parser.mly +++ b/Parser.mly @@ -171,9 +171,9 @@ type_decl: in {region; value}} type_expr: - cartesian { Prod (Present $1) } -| sum_type { Sum (Present $1) } -| record_type { Record (Present $1) } + cartesian { Prod $1 } +| sum_type { Sum $1 } +| record_type { Record $1 } cartesian: nsepseq(core_type,TIMES) { @@ -183,14 +183,14 @@ cartesian: core_type: type_name { - TAlias (Present $1) + TAlias $1 } | type_name type_tuple { let region = cover $1.region $2.region - in TypeApp (Present {region; value = $1,$2}) + in TypeApp {region; value = $1,$2} } | par(type_expr) { - ParType (Present $1) + ParType $1 } type_tuple: diff --git a/ParserMain.ml b/ParserMain.ml index c23833c25..0c940bfb6 100644 --- a/ParserMain.ml +++ b/ParserMain.ml @@ -57,10 +57,8 @@ let tokeniser = read ~log let () = try let ast = Parser.program tokeniser buffer in - let () = if Utils.String.Set.mem "parser" EvalOpt.verbose - then Print.print_tokens ast in - let _ = Typecheck2.tc_ast ast - in () + if Utils.String.Set.mem "parser" EvalOpt.verbose + then Print.print_tokens ast with Lexer.Error err -> close_all (); diff --git a/Print.ml b/Print.ml index 389a1f54d..c41da7f0a 100644 --- a/Print.ml +++ b/Print.ml @@ -47,7 +47,7 @@ and print_int _visitor {region; value = lexeme, abstract} = (* Main printing function *) -and print_tokens : 'x visitor -> 'x ast -> unit = fun v ast -> +and print_tokens (v: 'x visitor) ast = List.iter v.type_decl ast.types; v.parameter_decl ast.parameter; v.storage_decl ast.storage; @@ -56,90 +56,87 @@ and print_tokens : 'x visitor -> 'x ast -> unit = fun v ast -> v.block ast.block; v.token ast.eof "EOF" -and print_parameter_decl (v : 'xvisitor) {value=node; _} = +and print_parameter_decl (v: 'x visitor) {value=node; _} = v.token node.kwd_parameter "parameter"; v.var node.name; v.token node.colon ":"; v.type_expr node.param_type; v.terminator node.terminator -and print_storage_decl (v : 'xvisitor) {value=node; _} = +and print_storage_decl (v: 'x visitor) {value=node; _} = v.token node.kwd_storage "storage"; v.type_expr node.store_type; v.terminator node.terminator -and print_operations_decl (v : 'xvisitor) {value=node; _} = +and print_operations_decl (v: 'x visitor) {value=node; _} = v.token node.kwd_operations "operations"; v.type_expr node.op_type; v.terminator node.terminator -and print_type_decl (v : 'xvisitor) {value=node; _} = +and print_type_decl (v: 'x visitor) {value=node; _} = v.token node.kwd_type "type"; v.var node.name; v.token node.kwd_is "is"; v.type_expr node.type_expr; v.terminator node.terminator -and print_type_expr (v : 'xvisitor) = function - Prod (Present cartesian) -> v.cartesian cartesian -| Sum (Present sum_type) -> v.sum_type sum_type -| Record (Present record_type) -> v.record_type record_type -| TypeApp (Present type_app) -> v.type_app type_app -| ParType (Present par_type) -> v.par_type par_type -| TAlias (Present type_alias) -> v.var type_alias -| Function _function' -> printf "TODO" -| Mutable _mutable' -> printf "TODO" -| Unit _unit' -> printf "TODO" +and print_type_expr (v: 'x visitor) = function + Prod cartesian -> v.cartesian cartesian +| Sum sum_type -> v.sum_type sum_type +| Record record_type -> v.record_type record_type +| TypeApp type_app -> v.type_app type_app +| ParType par_type -> v.par_type par_type +| TAlias type_alias -> v.var type_alias -and print_cartesian (v : 'xvisitor) {value=sequence; _} = +and print_cartesian (v: 'x visitor) {value=sequence; _} = v.nsepseq "*" v.type_expr sequence -and print_variant (v : 'xvisitor) {value=node; _} = +and print_variant (v: 'x visitor) {value=node; _} = let constr, kwd_of, cartesian = node in v.constr constr; v.token kwd_of "of"; v.cartesian cartesian -and print_sum_type (v : 'xvisitor) {value=sequence; _} = +and print_sum_type (v: 'x visitor) {value=sequence; _} = v.nsepseq "|" v.variant sequence -and print_record_type (v : 'xvisitor) {value=node; _} = +and print_record_type (v: 'x visitor) {value=node; _} = let kwd_record, field_decls, kwd_end = node in v.token kwd_record "record"; v.field_decls field_decls; v.token kwd_end "end" -and print_type_app (v : 'xvisitor) {value=node; _} = +and print_type_app (v: 'x visitor) {value=node; _} = let type_name, type_tuple = node in v.var type_name; v.type_tuple type_tuple -and print_par_type (v : 'xvisitor) {value=node; _} = +and print_par_type (v: 'x visitor) {value=node; _} = let lpar, type_expr, rpar = node in v.token lpar "("; v.type_expr type_expr; v.token rpar ")" -and print_field_decls (v : 'xvisitor) sequence = +and print_field_decls (v: 'x visitor) sequence = v.nsepseq ";" v.field_decl sequence -and print_field_decl (v : 'xvisitor) {value=node; _} = +and print_field_decl (v: 'x visitor) {value=node; _} = let var, colon, type_expr = node in v.var var; v.token colon ":"; v.type_expr type_expr -and print_type_tuple (v : 'xvisitor) {value=node; _} = +and print_type_tuple (v: 'x visitor) {value=node; _} = let lpar, sequence, rpar = node in v.token lpar "("; v.nsepseq "," v.var sequence; v.token rpar ")" -and print_lambda_decl (v : 'xvisitor) = function +and print_lambda_decl (v: 'x visitor) = function FunDecl fun_decl -> v.fun_decl fun_decl | ProcDecl proc_decl -> v.proc_decl proc_decl -and print_fun_decl (v : 'xvisitor) {value=node; _} = +and print_fun_decl (v: 'x visitor) {value=node; _} = v.token node.kwd_function "function"; v.var node.name; v.parameters node.param; @@ -152,7 +149,7 @@ and print_fun_decl (v : 'xvisitor) {value=node; _} = v.expr node.return; v.terminator node.terminator -and print_proc_decl (v : 'xvisitor) {value=node; _} = +and print_proc_decl (v: 'x visitor) {value=node; _} = v.token node.kwd_procedure "procedure"; v.var node.name; v.parameters node.param; @@ -161,45 +158,45 @@ and print_proc_decl (v : 'xvisitor) {value=node; _} = v.block node.block; v.terminator node.terminator -and print_parameters (v : 'xvisitor) {value=node; _} = +and print_parameters (v: 'x visitor) {value=node; _} = let lpar, sequence, rpar = node in v.token lpar "("; v.nsepseq ";" v.param_decl sequence; v.token rpar ")" -and print_param_decl (v : 'xvisitor) = function +and print_param_decl (v: 'x visitor) = function ParamConst param_const -> v.param_const param_const | ParamVar param_var -> v.param_var param_var -and print_param_const (v : 'xvisitor) {value=node; _} = +and print_param_const (v: 'x visitor) {value=node; _} = let kwd_const, variable, colon, type_expr = node in v.token kwd_const "const"; v.var variable; v.token colon ":"; v.type_expr type_expr -and print_param_var (v : 'xvisitor) {value=node; _} = +and print_param_var (v: 'x visitor) {value=node; _} = let kwd_var, variable, colon, type_expr = node in v.token kwd_var "var"; v.var variable; v.token colon ":"; v.type_expr type_expr -and print_block (v : 'xvisitor) {value=node; _} = +and print_block (v: 'x visitor) {value=node; _} = v.token node.opening "begin"; v.instructions node.instr; v.terminator node.terminator; v.token node.close "end" -and print_local_decls (v : 'xvisitor) sequence = +and print_local_decls (v: 'x visitor) sequence = List.iter v.local_decl sequence -and print_local_decl (v : 'xvisitor) = function +and print_local_decl (v: 'x visitor) = function LocalLam decl -> v.lambda_decl decl | LocalConst decl -> v.const_decl decl | LocalVar decl -> v.var_decl decl -and print_const_decl (v : 'xvisitor) {value=node; _} = +and print_const_decl (v: 'x visitor) {value=node; _} = v.token node.kwd_const "const"; v.var node.name; v.token node.colon ":"; @@ -208,7 +205,7 @@ and print_const_decl (v : 'xvisitor) {value=node; _} = v.expr node.init; v.terminator node.terminator -and print_var_decl (v : 'xvisitor) {value=node; _} = +and print_var_decl (v: 'x visitor) {value=node; _} = v.token node.kwd_var "var"; v.var node.name; v.token node.colon ":"; @@ -217,14 +214,14 @@ and print_var_decl (v : 'xvisitor) {value=node; _} = v.expr node.init; v.terminator node.terminator -and print_instructions (v : 'xvisitor) {value=sequence; _} = +and print_instructions (v: 'x visitor) {value=sequence; _} = v.nsepseq ";" v.instruction sequence -and print_instruction (v : 'xvisitor) = function +and print_instruction (v: 'x visitor) = function Single instr -> v.single_instr instr | Block block -> v.block block -and print_single_instr (v : 'xvisitor) = function +and print_single_instr (v: 'x visitor) = function Cond {value; _} -> v.conditional value | Match {value; _} -> v.match_instr value | Ass instr -> v.ass_instr instr @@ -233,11 +230,11 @@ and print_single_instr (v : 'xvisitor) = function | Null kwd_null -> v.token kwd_null "null" | Fail {value; _} -> v.fail value -and print_fail (v : 'xvisitor) (kwd_fail, expr) = +and print_fail (v: 'x visitor) (kwd_fail, expr) = v.token kwd_fail "fail"; v.expr expr -and print_conditional (v : 'xvisitor) node = +and print_conditional (v: 'x visitor) node = v.token node.kwd_if "if"; v.expr node.test; v.token node.kwd_then "then"; @@ -245,43 +242,43 @@ and print_conditional (v : 'xvisitor) node = v.token node.kwd_else "else"; v.instruction node.ifnot -and print_match_instr (v : 'xvisitor) node = +and print_match_instr (v: 'x visitor) node = v.token node.kwd_match "match"; v.expr node.expr; v.token node.kwd_with "with"; v.cases node.cases; v.token node.kwd_end "end" -and print_cases (v : 'xvisitor) {value=sequence; _} = +and print_cases (v: 'x visitor) {value=sequence; _} = v.nsepseq "|" v.case sequence -and print_case (v : 'xvisitor) {value=node; _} = +and print_case (v: 'x visitor) {value=node; _} = let pattern, arrow, instruction = node in v.pattern pattern; v.token arrow "->"; v.instruction instruction -and print_ass_instr (v : 'xvisitor) {value=node; _} = +and print_ass_instr (v: 'x visitor) {value=node; _} = let variable, ass, expr = node in v.var variable; v.token ass ":="; v.expr expr -and print_loop (v : 'xvisitor) = function +and print_loop (v: 'x visitor) = function While while_loop -> v.while_loop while_loop | For for_loop -> v.for_loop for_loop -and print_while_loop (v : 'xvisitor) {value=node; _} = +and print_while_loop (v: 'x visitor) {value=node; _} = let kwd_while, expr, block = node in v.token kwd_while "while"; v.expr expr; v.block block -and print_for_loop (v : 'xvisitor) = function +and print_for_loop (v: 'x visitor) = function ForInt for_int -> v.for_int for_int | ForCollect for_collect -> v.for_collect for_collect -and print_for_int (v : 'xvisitor) ({value=node; _} : 'x for_int reg) = +and print_for_int (v: 'x visitor) ({value=node; _} : 'x for_int reg) = v.token node.kwd_for "for"; v.ass_instr node.ass; v.down node.down; @@ -290,17 +287,17 @@ and print_for_int (v : 'xvisitor) ({value=node; _} : 'x for_int reg) = v.step node.step; v.block node.block -and print_down (v : 'xvisitor) = function +and print_down (v: 'x visitor) = function Some kwd_down -> v.token kwd_down "down" | None -> () -and print_step (v : 'xvisitor) = function +and print_step (v: 'x visitor) = function Some (kwd_step, expr) -> v.token kwd_step "step"; v.expr expr | None -> () -and print_for_collect (v : 'xvisitor) ({value=node; _} : 'x for_collect reg) = +and print_for_collect (v: 'x visitor) ({value=node; _} : 'x for_collect reg) = v.token node.kwd_for "for"; v.var node.var; v.bind_to node.bind_to; @@ -308,13 +305,13 @@ and print_for_collect (v : 'xvisitor) ({value=node; _} : 'x for_collect reg) = v.expr node.expr; v.block node.block -and print_bind_to (v : 'xvisitor) = function +and print_bind_to (v: 'x visitor) = function Some (arrow, variable) -> v.token arrow "->"; v.var variable | None -> () -and print_expr (v : 'xvisitor) = function +and print_expr (v: 'x visitor) = function Or {value = expr1, bool_or, expr2; _} -> v.expr expr1; v.token bool_or "||"; v.expr expr2 | And {value = expr1, bool_and, expr2; _} -> @@ -368,19 +365,19 @@ and print_expr (v : 'xvisitor) = function | MapLookUp lookup -> v.map_lookup lookup | ParExpr pexpr -> v.par_expr pexpr -and print_tuple (v : 'xvisitor) {value=node; _} = +and print_tuple (v: 'x visitor) {value=node; _} = let lpar, sequence, rpar = node in v.token lpar "("; v.nsepseq "," v.expr sequence; v.token rpar ")" -and print_list (v : 'xvisitor) {value=node; _} = +and print_list (v: 'x visitor) {value=node; _} = let lbra, sequence, rbra = node in v.token lbra "["; v.nsepseq "," v.expr sequence; v.token rbra "]" -and print_empty_list (v : 'xvisitor) {value=node; _} = +and print_empty_list (v: 'x visitor) {value=node; _} = let lpar, (lbracket, rbracket, colon, type_expr), rpar = node in v.token lpar "("; v.token lbracket "["; @@ -389,13 +386,13 @@ and print_empty_list (v : 'xvisitor) {value=node; _} = v.type_expr type_expr; v.token rpar ")" -and print_set (v : 'xvisitor) {value=node; _} = +and print_set (v: 'x visitor) {value=node; _} = let lbrace, sequence, rbrace = node in v.token lbrace "{"; v.nsepseq "," v.expr sequence; v.token rbrace "}" -and print_empty_set (v : 'xvisitor) {value=node; _} = +and print_empty_set (v: 'x visitor) {value=node; _} = let lpar, (lbrace, rbrace, colon, type_expr), rpar = node in v.token lpar "("; v.token lbrace "{"; @@ -404,7 +401,7 @@ and print_empty_set (v : 'xvisitor) {value=node; _} = v.type_expr type_expr; v.token rpar ")" -and print_none_expr (v : 'xvisitor) {value=node; _} = +and print_none_expr (v: 'x visitor) {value=node; _} = let lpar, (c_None, colon, type_expr), rpar = node in v.token lpar "("; v.token c_None "None"; @@ -412,22 +409,22 @@ and print_none_expr (v : 'xvisitor) {value=node; _} = v.type_expr type_expr; v.token rpar ")" -and print_fun_call (v : 'xvisitor) {value=node; _} = +and print_fun_call (v: 'x visitor) {value=node; _} = let fun_name, arguments = node in v.var fun_name; v.tuple arguments -and print_constr_app (v : 'xvisitor) {value=node; _} = +and print_constr_app (v: 'x visitor) {value=node; _} = let constr, arguments = node in v.constr constr; v.tuple arguments -and print_some_app (v : 'xvisitor) {value=node; _} = +and print_some_app (v: 'x visitor) {value=node; _} = let c_Some, arguments = node in v.token c_Some "Some"; v.tuple arguments -and print_map_lookup (v : 'xvisitor) {value=node; _} = +and print_map_lookup (v: 'x visitor) {value=node; _} = let {value = lbracket, expr, rbracket; _} = node.index in v.var node.map_name; v.token node.selector "."; @@ -435,16 +432,16 @@ and print_map_lookup (v : 'xvisitor) {value=node; _} = v.expr expr; v.token rbracket "]" -and print_par_expr (v : 'xvisitor) {value=node; _} = +and print_par_expr (v: 'x visitor) {value=node; _} = let lpar, expr, rpar = node in v.token lpar "("; v.expr expr; v.token rpar ")" -and print_pattern (v : 'xvisitor) {value=sequence; _} = +and print_pattern (v: 'x visitor) {value=sequence; _} = v.nsepseq "<:" v.core_pattern sequence -and print_core_pattern (v : 'xvisitor) = function +and print_core_pattern (v: 'x visitor) = function PVar var -> v.var var | PWild wild -> v.token wild "_" | PInt i -> v.int i @@ -458,28 +455,28 @@ and print_core_pattern (v : 'xvisitor) = function | PList pattern -> v.list_pattern pattern | PTuple ptuple -> v.ptuple ptuple -and print_psome (v : 'xvisitor) {value=node; _} = +and print_psome (v: 'x visitor) {value=node; _} = let c_Some, patterns = node in v.token c_Some "Some"; v.patterns patterns -and print_patterns (v : 'xvisitor) {value=node; _} = +and print_patterns (v: 'x visitor) {value=node; _} = let lpar, core_pattern, rpar = node in v.token lpar "("; v.core_pattern core_pattern; v.token rpar ")" -and print_list_pattern (v : 'xvisitor) = function +and print_list_pattern (v: 'x visitor) = function Sugar sugar -> v.sugar sugar | Raw raw -> v.raw raw -and print_sugar (v : 'xvisitor) {value=node; _} = +and print_sugar (v: 'x visitor) {value=node; _} = let lbracket, sequence, rbracket = node in v.token lbracket "["; v.sepseq "," v.core_pattern sequence; v.token rbracket "]" -and print_raw (v : 'xvisitor) {value=node; _} = +and print_raw (v: 'x visitor) {value=node; _} = let lpar, (core_pattern, cons, pattern), rpar = node in v.token lpar "("; v.core_pattern core_pattern; @@ -487,13 +484,13 @@ and print_raw (v : 'xvisitor) {value=node; _} = v.pattern pattern; v.token rpar ")" -and print_ptuple (v : 'xvisitor) {value=node; _} = +and print_ptuple (v: 'x visitor) {value=node; _} = let lpar, sequence, rpar = node in v.token lpar "("; v.nsepseq "," v.core_pattern sequence; v.token rpar ")" -and print_terminator (v : 'xvisitor) = function +and print_terminator (v: 'x visitor) = function Some semi -> v.token semi ";" | None -> () diff --git a/Print.mli b/Print.mli index 97621a8fc..66fae6dfa 100644 --- a/Print.mli +++ b/Print.mli @@ -2,4 +2,4 @@ open AST -val print_tokens : parse_phase ast -> unit +val print_tokens : t -> unit diff --git a/Typecheck2.ml b/Typecheck2.ml deleted file mode 100644 index ae5d9bdb3..000000000 --- a/Typecheck2.ml +++ /dev/null @@ -1,337 +0,0 @@ -module SMap = Map.Make(String) - -open AST - -type i = parse_phase -type typecheck_phase = < - annot: typecheck_phase type_expr; - type_expr_typecheck: tfalse; -> -type o = typecheck_phase - -type te = o type_expr list SMap.t (* Type environment *) -type ve = o type_expr list SMap.t (* Value environment *) -type tve = te * ve - -let id (ast : i ast) : o ast = {ast with eof = ast.eof} - -(* Utilities *) - -let fold_map f a l = - let f (acc, l) elem = - let acc', elem' = f acc elem - in acc', (elem' :: l) in - let last_acc, last_l = List.fold_left f (a, []) l - in last_acc, List.rev last_l - -let reg ({value;region} : 'a reg) (f : 'a -> 'b) : 'b reg = {value = f value; region} -let unreg ({value;_} : 'a reg) : 'a = value - -(* Typecheck *) - -let tc_type_decl (te, ve : tve) (td : i type_decl reg) : tve * o type_decl reg = - (te, ve), (unreg td) - -let tc_types (tve : tve) (types : i type_decl reg list) = - fold_map tc_type_decl tve types - -let tc_ast (tve : tve) (ast : i ast) = - let {types;constants;parameter;storage;operations;lambdas;block;eof} = ast in - let tve, types = tc_types tve types in - let ast = {types;constants;parameter;storage;operations;lambdas;block;eof} in - tve, ast - -let tc_ast ast = - let tve, ast = tc_ast (SMap.empty, SMap.empty) ast in - let _ = tve in (* Drop the final type and value environment *) - ast - -(* -open Region -open Utils -type new_t = < ty: int > ast -and 'a ast = { - types : 'a type_decl reg list; - constants : 'a const_decl reg list; - parameter : 'a parameter_decl reg; - storage : 'a storage_decl reg; - operations : 'a operations_decl reg; - lambdas : 'a lambda_decl list; - block : 'a block reg; - eof : eof -} - -and 'a parameter_decl = { - kwd_parameter : kwd_parameter; - name : 'a variable; - colon : colon; - param_type : 'a type_expr; - terminator : semi option -} - -and 'a storage_decl = { - kwd_storage : kwd_storage; - store_type : 'a type_expr; - terminator : semi option -} - -and 'a operations_decl = { - kwd_operations : kwd_operations; - op_type : 'a type_expr; - terminator : semi option -} - -(* Type declarations *) - -and 'a type_decl = { - kwd_type : kwd_type; - name : 'a type_name; - kwd_is : kwd_is; - type_expr : 'a type_expr; - terminator : semi option -} - -and 'a type_expr = - Prod of 'a cartesian -| Sum of ('a variant, vbar) nsepseq reg -| Record of 'a record_type -| TypeApp of ('a type_name * 'a type_tuple) reg -| ParType of 'a type_expr par -| TAlias of 'a variable - -and 'a cartesian = ('a type_expr, times) nsepseq reg - -and 'a variant = ('a constr * kwd_of * 'a cartesian) reg - -and 'a record_type = (kwd_record * 'a field_decls * kwd_end) reg - -and 'a field_decls = ('a field_decl, semi) nsepseq - -and 'a field_decl = ('a variable * colon * 'a type_expr) reg - -and 'a type_tuple = ('a type_name, comma) nsepseq par - -(* Function and procedure declarations *) - -and 'a lambda_decl = - FunDecl of 'a fun_decl reg -| ProcDecl of 'a proc_decl reg - -and 'a fun_decl = { - kwd_function : kwd_function; - name : 'a variable; - param : 'a parameters; - colon : colon; - ret_type : 'a type_expr; - kwd_is : kwd_is; - local_decls : 'a local_decl list; - block : 'a block reg; - kwd_with : kwd_with; - return : 'a expr; - terminator : semi option -} - -and 'a proc_decl = { - kwd_procedure : kwd_procedure; - name : 'a variable; - param : 'a parameters; - kwd_is : kwd_is; - local_decls : 'a local_decl list; - block : 'a block reg; - terminator : semi option -} - -and 'a parameters = ('a param_decl, semi) nsepseq par - -and 'a param_decl = - ParamConst of 'a param_const -| ParamVar of 'a param_var - -and 'a param_const = (kwd_const * 'a variable * colon * 'a type_expr) reg - -and 'a param_var = (kwd_var * 'a variable * colon * 'a type_expr) reg - -and 'a block = { - opening : kwd_begin; - instr : 'a instructions; - terminator : semi option; - close : kwd_end -} - -and 'a local_decl = - LocalLam of 'a lambda_decl -| LocalConst of 'a const_decl reg -| LocalVar of 'a var_decl reg - -and 'a const_decl = { - kwd_const : kwd_const; - name : 'a variable; - colon : colon; - vtype : 'a type_expr; - equal : equal; - init : 'a expr; - terminator : semi option -} - -and 'a var_decl = { - kwd_var : kwd_var; - name : 'a variable; - colon : colon; - vtype : 'a type_expr; - ass : ass; - init : 'a expr; - terminator : semi option -} - -and 'a instructions = ('a instruction, semi) nsepseq reg - -and 'a instruction = - Single of 'a single_instr -| Block of 'a block reg - -and 'a single_instr = - Cond of 'a conditional reg -| Match of 'a match_instr reg -| Ass of 'a ass_instr -| Loop of 'a loop -| ProcCall of 'a fun_call -| Null of kwd_null -| Fail of (kwd_fail * 'a expr) reg - -and 'a conditional = { - kwd_if : kwd_if; - test : 'a expr; - kwd_then : kwd_then; - ifso : 'a instruction; - kwd_else : kwd_else; - ifnot : 'a instruction -} - -and 'a match_instr = { - kwd_match : kwd_match; - expr : 'a expr; - kwd_with : kwd_with; - lead_vbar : vbar option; - cases : 'a cases; - kwd_end : kwd_end -} - -and 'a cases = ('a case, vbar) nsepseq reg - -and 'a case = ('a pattern * arrow * 'a instruction) reg - -and 'a ass_instr = ('a variable * ass * 'a expr) reg - -and 'a loop = - While of 'a while_loop -| For of 'a for_loop - -and 'a while_loop = (kwd_while * 'a expr * 'a block reg) reg - -and 'a for_loop = - ForInt of 'a for_int reg -| ForCollect of 'a for_collect reg - -and 'a for_int = { - kwd_for : kwd_for; - ass : 'a ass_instr; - down : kwd_down option; - kwd_to : kwd_to; - bound : 'a expr; - step : (kwd_step * 'a expr) option; - block : 'a block reg -} - -and 'a for_collect = { - kwd_for : kwd_for; - var : 'a variable; - bind_to : (arrow * 'a variable) option; - kwd_in : kwd_in; - expr : 'a expr; - block : 'a block reg -} - -(* Expressions *) - -and 'a expr = - Or of ('a expr * bool_or * 'a expr) reg -| And of ('a expr * bool_and * 'a expr) reg -| Lt of ('a expr * lt * 'a expr) reg -| Leq of ('a expr * leq * 'a expr) reg -| Gt of ('a expr * gt * 'a expr) reg -| Geq of ('a expr * geq * 'a expr) reg -| Equal of ('a expr * equal * 'a expr) reg -| Neq of ('a expr * neq * 'a expr) reg -| Cat of ('a expr * cat * 'a expr) reg -| Cons of ('a expr * cons * 'a expr) reg -| Add of ('a expr * plus * 'a expr) reg -| Sub of ('a expr * minus * 'a expr) reg -| Mult of ('a expr * times * 'a expr) reg -| Div of ('a expr * slash * 'a expr) reg -| Mod of ('a expr * kwd_mod * 'a expr) reg -| Neg of (minus * 'a expr) reg -| Not of (kwd_not * 'a expr) reg -| Int of (Lexer.lexeme * Z.t) reg -| Var of Lexer.lexeme reg -| String of Lexer.lexeme reg -| Bytes of (Lexer.lexeme * MBytes.t) reg -| False of c_False -| True of c_True -| Unit of c_Unit -| Tuple of 'a tuple -| List of ('a expr, comma) nsepseq brackets -| EmptyList of 'a empty_list -| Set of ('a expr, comma) nsepseq braces -| EmptySet of 'a empty_set -| NoneExpr of 'a none_expr -| FunCall of 'a fun_call -| ConstrApp of 'a constr_app -| SomeApp of (c_Some * 'a arguments) reg -| MapLookUp of 'a map_lookup reg -| ParExpr of 'a expr par - -and 'a tuple = ('a expr, comma) nsepseq par - -and 'a empty_list = - (lbracket * rbracket * colon * 'a type_expr) par - -and 'a empty_set = - (lbrace * rbrace * colon * 'a type_expr) par - -and 'a none_expr = - (c_None * colon * 'a type_expr) par - -and 'a fun_call = ('a fun_name * 'a arguments) reg - -and 'a arguments = 'a tuple - -and 'a constr_app = ('a constr * 'a arguments) reg - -and 'a map_lookup = { - map_name : 'a variable; - selector : dot; - index : 'a expr brackets -} - -(* Patterns *) - -and 'a pattern = ('a core_pattern, cons) nsepseq reg - -and 'a core_pattern = - PVar of Lexer.lexeme reg -| PWild of wild -| PInt of (Lexer.lexeme * Z.t) reg -| PBytes of (Lexer.lexeme * MBytes.t) reg -| PString of Lexer.lexeme reg -| PUnit of c_Unit -| PFalse of c_False -| PTrue of c_True -| PNone of c_None -| PSome of (c_Some * 'a core_pattern par) reg -| PList of 'a list_pattern -| PTuple of ('a core_pattern, comma) nsepseq par - -and 'a list_pattern = - Sugar of ('a core_pattern, comma) sepseq brackets -| Raw of ('a core_pattern * cons * 'a pattern) par - *) diff --git a/Typecheck2.mli b/Typecheck2.mli deleted file mode 100644 index 8f5bf59e1..000000000 --- a/Typecheck2.mli +++ /dev/null @@ -1 +0,0 @@ -val tc_ast : AST.parse_phase AST.ast -> AST.typecheck_phase AST.ast diff --git a/typecheck.ml b/typecheck.ml index dc2bc374a..b768a9949 100644 --- a/typecheck.ml +++ b/typecheck.ml @@ -1,3 +1,8 @@ + + + + + (* module I = AST (* In *)