From 9b9760f052c85202cd59e7132d2649d41e54424f Mon Sep 17 00:00:00 2001 From: Your Name Date: Tue, 5 Mar 2019 20:37:32 +0100 Subject: [PATCH] =?UTF-8?q?WIP=E2=80=A6?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- AST.ml | 167 +++++++++++++++++++++--- AST.mli | 122 ++++++++++++++++-- Parser.mly | 12 +- ParserMain.ml | 6 +- Print.ml | 145 ++++++++++----------- Print.mli | 2 +- Typecheck2.ml | 337 +++++++++++++++++++++++++++++++++++++++++++++++++ Typecheck2.mli | 1 + typecheck.ml | 5 - 9 files changed, 688 insertions(+), 109 deletions(-) create mode 100644 Typecheck2.ml create mode 100644 Typecheck2.mli diff --git a/AST.ml b/AST.ml index 940b562c4..6f62f6e98 100644 --- a/AST.ml +++ b/AST.ml @@ -142,9 +142,45 @@ type 'a braces = (lbrace * 'a * rbrace) reg (* The Abstract Syntax Tree *) -type t = < ty: unit > ast +type ttrue = TTrue +type tfalse = TFalse +type ('a, 'type_expr_typecheck) gadt_if = + Present : 'a -> ('a, ttrue) gadt_if -and 'x 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 = { types : 'x type_decl reg list; constants : 'x const_decl reg list; parameter : 'x parameter_decl reg; @@ -154,6 +190,7 @@ and 'x ast = { block : 'x block reg; eof : eof } +constraint 'x = 'x x_sig and 'x parameter_decl = { kwd_parameter : kwd_parameter; @@ -162,18 +199,21 @@ 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 *) @@ -184,32 +224,79 @@ 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 -| 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 + 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 + *) 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; @@ -224,6 +311,7 @@ and 'x fun_decl = { return : 'x expr; terminator : semi option } +constraint 'x = 'x x_sig and 'x proc_decl = { kwd_procedure : kwd_procedure; @@ -234,16 +322,21 @@ 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; @@ -251,11 +344,13 @@ 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; @@ -266,6 +361,7 @@ and 'x const_decl = { init : 'x expr; terminator : semi option } +constraint 'x = 'x x_sig and 'x var_decl = { kwd_var : kwd_var; @@ -276,12 +372,15 @@ 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 @@ -291,6 +390,7 @@ 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; @@ -300,6 +400,7 @@ and 'x conditional = { kwd_else : kwd_else; ifnot : 'x instruction } +constraint 'x = 'x x_sig and 'x match_instr = { kwd_match : kwd_match; @@ -309,22 +410,29 @@ 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; @@ -335,6 +443,7 @@ 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; @@ -344,6 +453,7 @@ and 'x for_collect = { expr : 'x expr; block : 'x block reg } +constraint 'x = 'x x_sig (* Expressions *) @@ -383,33 +493,43 @@ 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 @@ -424,22 +544,39 @@ 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 = 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 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 expr_to_region = function Or {region; _} diff --git a/AST.mli b/AST.mli index cb6fbcd2b..d89d92b25 100644 --- a/AST.mli +++ b/AST.mli @@ -126,9 +126,45 @@ type 'a braces = (lbrace * 'a * rbrace) reg (* The Abstract Syntax Tree *) -type t = < ty:unit > ast +type ttrue = TTrue +type tfalse = TFalse +type ('a, 'type_expr_typecheck) gadt_if = + Present : 'a -> ('a, ttrue) gadt_if -and 'x 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 = { types : 'x type_decl reg list; constants : 'x const_decl reg list; parameter : 'x parameter_decl reg; @@ -138,6 +174,7 @@ and 'x ast = { block : 'x block reg; eof : eof } +constraint 'x = 'x x_sig and 'x parameter_decl = { kwd_parameter : kwd_parameter; @@ -146,18 +183,21 @@ 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 *) @@ -168,32 +208,47 @@ 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 -| 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 + 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 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; @@ -208,6 +263,7 @@ and 'x fun_decl = { return : 'x expr; terminator : semi option } +constraint 'x = 'x x_sig and 'x proc_decl = { kwd_procedure : kwd_procedure; @@ -218,16 +274,21 @@ 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; @@ -235,11 +296,13 @@ 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; @@ -250,6 +313,7 @@ and 'x const_decl = { init : 'x expr; terminator : semi option } +constraint 'x = 'x x_sig and 'x var_decl = { kwd_var : kwd_var; @@ -260,12 +324,15 @@ 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 @@ -275,6 +342,7 @@ 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; @@ -284,6 +352,7 @@ and 'x conditional = { kwd_else : kwd_else; ifnot : 'x instruction } +constraint 'x = 'x x_sig and 'x match_instr = { kwd_match : kwd_match; @@ -293,22 +362,29 @@ 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; @@ -319,6 +395,7 @@ 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; @@ -328,6 +405,7 @@ and 'x for_collect = { expr : 'x expr; block : 'x block reg } +constraint 'x = 'x x_sig (* Expressions *) @@ -367,33 +445,43 @@ 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 @@ -408,14 +496,30 @@ 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 : 'x type_expr -> Region.t +val type_expr_to_region : parse_phase type_expr -> Region.t val expr_to_region : 'x expr -> Region.t diff --git a/Parser.mly b/Parser.mly index d3aca6dcc..547e20e68 100644 --- a/Parser.mly +++ b/Parser.mly @@ -171,9 +171,9 @@ type_decl: in {region; value}} type_expr: - cartesian { Prod $1 } -| sum_type { Sum $1 } -| record_type { Record $1 } + cartesian { Prod (Present $1) } +| sum_type { Sum (Present $1) } +| record_type { Record (Present $1) } cartesian: nsepseq(core_type,TIMES) { @@ -183,14 +183,14 @@ cartesian: core_type: type_name { - TAlias $1 + TAlias (Present $1) } | type_name type_tuple { let region = cover $1.region $2.region - in TypeApp {region; value = $1,$2} + in TypeApp (Present {region; value = $1,$2}) } | par(type_expr) { - ParType $1 + ParType (Present $1) } type_tuple: diff --git a/ParserMain.ml b/ParserMain.ml index 0c940bfb6..c23833c25 100644 --- a/ParserMain.ml +++ b/ParserMain.ml @@ -57,8 +57,10 @@ let tokeniser = read ~log let () = try let ast = Parser.program tokeniser buffer in - if Utils.String.Set.mem "parser" EvalOpt.verbose - then Print.print_tokens ast + let () = if Utils.String.Set.mem "parser" EvalOpt.verbose + then Print.print_tokens ast in + let _ = Typecheck2.tc_ast ast + in () with Lexer.Error err -> close_all (); diff --git a/Print.ml b/Print.ml index c41da7f0a..389a1f54d 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 (v: 'x visitor) ast = +and print_tokens : 'x visitor -> 'x ast -> unit = fun v ast -> List.iter v.type_decl ast.types; v.parameter_decl ast.parameter; v.storage_decl ast.storage; @@ -56,87 +56,90 @@ and print_tokens (v: 'x visitor) ast = v.block ast.block; v.token ast.eof "EOF" -and print_parameter_decl (v: 'x visitor) {value=node; _} = +and print_parameter_decl (v : 'xvisitor) {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: 'x visitor) {value=node; _} = +and print_storage_decl (v : 'xvisitor) {value=node; _} = v.token node.kwd_storage "storage"; v.type_expr node.store_type; v.terminator node.terminator -and print_operations_decl (v: 'x visitor) {value=node; _} = +and print_operations_decl (v : 'xvisitor) {value=node; _} = v.token node.kwd_operations "operations"; v.type_expr node.op_type; v.terminator node.terminator -and print_type_decl (v: 'x visitor) {value=node; _} = +and print_type_decl (v : 'xvisitor) {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: '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_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_cartesian (v: 'x visitor) {value=sequence; _} = +and print_cartesian (v : 'xvisitor) {value=sequence; _} = v.nsepseq "*" v.type_expr sequence -and print_variant (v: 'x visitor) {value=node; _} = +and print_variant (v : 'xvisitor) {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: 'x visitor) {value=sequence; _} = +and print_sum_type (v : 'xvisitor) {value=sequence; _} = v.nsepseq "|" v.variant sequence -and print_record_type (v: 'x visitor) {value=node; _} = +and print_record_type (v : 'xvisitor) {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: 'x visitor) {value=node; _} = +and print_type_app (v : 'xvisitor) {value=node; _} = let type_name, type_tuple = node in v.var type_name; v.type_tuple type_tuple -and print_par_type (v: 'x visitor) {value=node; _} = +and print_par_type (v : 'xvisitor) {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: 'x visitor) sequence = +and print_field_decls (v : 'xvisitor) sequence = v.nsepseq ";" v.field_decl sequence -and print_field_decl (v: 'x visitor) {value=node; _} = +and print_field_decl (v : 'xvisitor) {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: 'x visitor) {value=node; _} = +and print_type_tuple (v : 'xvisitor) {value=node; _} = let lpar, sequence, rpar = node in v.token lpar "("; v.nsepseq "," v.var sequence; v.token rpar ")" -and print_lambda_decl (v: 'x visitor) = function +and print_lambda_decl (v : 'xvisitor) = function FunDecl fun_decl -> v.fun_decl fun_decl | ProcDecl proc_decl -> v.proc_decl proc_decl -and print_fun_decl (v: 'x visitor) {value=node; _} = +and print_fun_decl (v : 'xvisitor) {value=node; _} = v.token node.kwd_function "function"; v.var node.name; v.parameters node.param; @@ -149,7 +152,7 @@ and print_fun_decl (v: 'x visitor) {value=node; _} = v.expr node.return; v.terminator node.terminator -and print_proc_decl (v: 'x visitor) {value=node; _} = +and print_proc_decl (v : 'xvisitor) {value=node; _} = v.token node.kwd_procedure "procedure"; v.var node.name; v.parameters node.param; @@ -158,45 +161,45 @@ and print_proc_decl (v: 'x visitor) {value=node; _} = v.block node.block; v.terminator node.terminator -and print_parameters (v: 'x visitor) {value=node; _} = +and print_parameters (v : 'xvisitor) {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: 'x visitor) = function +and print_param_decl (v : 'xvisitor) = function ParamConst param_const -> v.param_const param_const | ParamVar param_var -> v.param_var param_var -and print_param_const (v: 'x visitor) {value=node; _} = +and print_param_const (v : 'xvisitor) {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: 'x visitor) {value=node; _} = +and print_param_var (v : 'xvisitor) {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: 'x visitor) {value=node; _} = +and print_block (v : 'xvisitor) {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: 'x visitor) sequence = +and print_local_decls (v : 'xvisitor) sequence = List.iter v.local_decl sequence -and print_local_decl (v: 'x visitor) = function +and print_local_decl (v : 'xvisitor) = function LocalLam decl -> v.lambda_decl decl | LocalConst decl -> v.const_decl decl | LocalVar decl -> v.var_decl decl -and print_const_decl (v: 'x visitor) {value=node; _} = +and print_const_decl (v : 'xvisitor) {value=node; _} = v.token node.kwd_const "const"; v.var node.name; v.token node.colon ":"; @@ -205,7 +208,7 @@ and print_const_decl (v: 'x visitor) {value=node; _} = v.expr node.init; v.terminator node.terminator -and print_var_decl (v: 'x visitor) {value=node; _} = +and print_var_decl (v : 'xvisitor) {value=node; _} = v.token node.kwd_var "var"; v.var node.name; v.token node.colon ":"; @@ -214,14 +217,14 @@ and print_var_decl (v: 'x visitor) {value=node; _} = v.expr node.init; v.terminator node.terminator -and print_instructions (v: 'x visitor) {value=sequence; _} = +and print_instructions (v : 'xvisitor) {value=sequence; _} = v.nsepseq ";" v.instruction sequence -and print_instruction (v: 'x visitor) = function +and print_instruction (v : 'xvisitor) = function Single instr -> v.single_instr instr | Block block -> v.block block -and print_single_instr (v: 'x visitor) = function +and print_single_instr (v : 'xvisitor) = function Cond {value; _} -> v.conditional value | Match {value; _} -> v.match_instr value | Ass instr -> v.ass_instr instr @@ -230,11 +233,11 @@ and print_single_instr (v: 'x visitor) = function | Null kwd_null -> v.token kwd_null "null" | Fail {value; _} -> v.fail value -and print_fail (v: 'x visitor) (kwd_fail, expr) = +and print_fail (v : 'xvisitor) (kwd_fail, expr) = v.token kwd_fail "fail"; v.expr expr -and print_conditional (v: 'x visitor) node = +and print_conditional (v : 'xvisitor) node = v.token node.kwd_if "if"; v.expr node.test; v.token node.kwd_then "then"; @@ -242,43 +245,43 @@ and print_conditional (v: 'x visitor) node = v.token node.kwd_else "else"; v.instruction node.ifnot -and print_match_instr (v: 'x visitor) node = +and print_match_instr (v : 'xvisitor) 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: 'x visitor) {value=sequence; _} = +and print_cases (v : 'xvisitor) {value=sequence; _} = v.nsepseq "|" v.case sequence -and print_case (v: 'x visitor) {value=node; _} = +and print_case (v : 'xvisitor) {value=node; _} = let pattern, arrow, instruction = node in v.pattern pattern; v.token arrow "->"; v.instruction instruction -and print_ass_instr (v: 'x visitor) {value=node; _} = +and print_ass_instr (v : 'xvisitor) {value=node; _} = let variable, ass, expr = node in v.var variable; v.token ass ":="; v.expr expr -and print_loop (v: 'x visitor) = function +and print_loop (v : 'xvisitor) = function While while_loop -> v.while_loop while_loop | For for_loop -> v.for_loop for_loop -and print_while_loop (v: 'x visitor) {value=node; _} = +and print_while_loop (v : 'xvisitor) {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: 'x visitor) = function +and print_for_loop (v : 'xvisitor) = function ForInt for_int -> v.for_int for_int | ForCollect for_collect -> v.for_collect for_collect -and print_for_int (v: 'x visitor) ({value=node; _} : 'x for_int reg) = +and print_for_int (v : 'xvisitor) ({value=node; _} : 'x for_int reg) = v.token node.kwd_for "for"; v.ass_instr node.ass; v.down node.down; @@ -287,17 +290,17 @@ and print_for_int (v: 'x visitor) ({value=node; _} : 'x for_int reg) = v.step node.step; v.block node.block -and print_down (v: 'x visitor) = function +and print_down (v : 'xvisitor) = function Some kwd_down -> v.token kwd_down "down" | None -> () -and print_step (v: 'x visitor) = function +and print_step (v : 'xvisitor) = function Some (kwd_step, expr) -> v.token kwd_step "step"; v.expr expr | None -> () -and print_for_collect (v: 'x visitor) ({value=node; _} : 'x for_collect reg) = +and print_for_collect (v : 'xvisitor) ({value=node; _} : 'x for_collect reg) = v.token node.kwd_for "for"; v.var node.var; v.bind_to node.bind_to; @@ -305,13 +308,13 @@ and print_for_collect (v: 'x visitor) ({value=node; _} : 'x for_collect reg) = v.expr node.expr; v.block node.block -and print_bind_to (v: 'x visitor) = function +and print_bind_to (v : 'xvisitor) = function Some (arrow, variable) -> v.token arrow "->"; v.var variable | None -> () -and print_expr (v: 'x visitor) = function +and print_expr (v : 'xvisitor) = function Or {value = expr1, bool_or, expr2; _} -> v.expr expr1; v.token bool_or "||"; v.expr expr2 | And {value = expr1, bool_and, expr2; _} -> @@ -365,19 +368,19 @@ and print_expr (v: 'x visitor) = function | MapLookUp lookup -> v.map_lookup lookup | ParExpr pexpr -> v.par_expr pexpr -and print_tuple (v: 'x visitor) {value=node; _} = +and print_tuple (v : 'xvisitor) {value=node; _} = let lpar, sequence, rpar = node in v.token lpar "("; v.nsepseq "," v.expr sequence; v.token rpar ")" -and print_list (v: 'x visitor) {value=node; _} = +and print_list (v : 'xvisitor) {value=node; _} = let lbra, sequence, rbra = node in v.token lbra "["; v.nsepseq "," v.expr sequence; v.token rbra "]" -and print_empty_list (v: 'x visitor) {value=node; _} = +and print_empty_list (v : 'xvisitor) {value=node; _} = let lpar, (lbracket, rbracket, colon, type_expr), rpar = node in v.token lpar "("; v.token lbracket "["; @@ -386,13 +389,13 @@ and print_empty_list (v: 'x visitor) {value=node; _} = v.type_expr type_expr; v.token rpar ")" -and print_set (v: 'x visitor) {value=node; _} = +and print_set (v : 'xvisitor) {value=node; _} = let lbrace, sequence, rbrace = node in v.token lbrace "{"; v.nsepseq "," v.expr sequence; v.token rbrace "}" -and print_empty_set (v: 'x visitor) {value=node; _} = +and print_empty_set (v : 'xvisitor) {value=node; _} = let lpar, (lbrace, rbrace, colon, type_expr), rpar = node in v.token lpar "("; v.token lbrace "{"; @@ -401,7 +404,7 @@ and print_empty_set (v: 'x visitor) {value=node; _} = v.type_expr type_expr; v.token rpar ")" -and print_none_expr (v: 'x visitor) {value=node; _} = +and print_none_expr (v : 'xvisitor) {value=node; _} = let lpar, (c_None, colon, type_expr), rpar = node in v.token lpar "("; v.token c_None "None"; @@ -409,22 +412,22 @@ and print_none_expr (v: 'x visitor) {value=node; _} = v.type_expr type_expr; v.token rpar ")" -and print_fun_call (v: 'x visitor) {value=node; _} = +and print_fun_call (v : 'xvisitor) {value=node; _} = let fun_name, arguments = node in v.var fun_name; v.tuple arguments -and print_constr_app (v: 'x visitor) {value=node; _} = +and print_constr_app (v : 'xvisitor) {value=node; _} = let constr, arguments = node in v.constr constr; v.tuple arguments -and print_some_app (v: 'x visitor) {value=node; _} = +and print_some_app (v : 'xvisitor) {value=node; _} = let c_Some, arguments = node in v.token c_Some "Some"; v.tuple arguments -and print_map_lookup (v: 'x visitor) {value=node; _} = +and print_map_lookup (v : 'xvisitor) {value=node; _} = let {value = lbracket, expr, rbracket; _} = node.index in v.var node.map_name; v.token node.selector "."; @@ -432,16 +435,16 @@ and print_map_lookup (v: 'x visitor) {value=node; _} = v.expr expr; v.token rbracket "]" -and print_par_expr (v: 'x visitor) {value=node; _} = +and print_par_expr (v : 'xvisitor) {value=node; _} = let lpar, expr, rpar = node in v.token lpar "("; v.expr expr; v.token rpar ")" -and print_pattern (v: 'x visitor) {value=sequence; _} = +and print_pattern (v : 'xvisitor) {value=sequence; _} = v.nsepseq "<:" v.core_pattern sequence -and print_core_pattern (v: 'x visitor) = function +and print_core_pattern (v : 'xvisitor) = function PVar var -> v.var var | PWild wild -> v.token wild "_" | PInt i -> v.int i @@ -455,28 +458,28 @@ and print_core_pattern (v: 'x visitor) = function | PList pattern -> v.list_pattern pattern | PTuple ptuple -> v.ptuple ptuple -and print_psome (v: 'x visitor) {value=node; _} = +and print_psome (v : 'xvisitor) {value=node; _} = let c_Some, patterns = node in v.token c_Some "Some"; v.patterns patterns -and print_patterns (v: 'x visitor) {value=node; _} = +and print_patterns (v : 'xvisitor) {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: 'x visitor) = function +and print_list_pattern (v : 'xvisitor) = function Sugar sugar -> v.sugar sugar | Raw raw -> v.raw raw -and print_sugar (v: 'x visitor) {value=node; _} = +and print_sugar (v : 'xvisitor) {value=node; _} = let lbracket, sequence, rbracket = node in v.token lbracket "["; v.sepseq "," v.core_pattern sequence; v.token rbracket "]" -and print_raw (v: 'x visitor) {value=node; _} = +and print_raw (v : 'xvisitor) {value=node; _} = let lpar, (core_pattern, cons, pattern), rpar = node in v.token lpar "("; v.core_pattern core_pattern; @@ -484,13 +487,13 @@ and print_raw (v: 'x visitor) {value=node; _} = v.pattern pattern; v.token rpar ")" -and print_ptuple (v: 'x visitor) {value=node; _} = +and print_ptuple (v : 'xvisitor) {value=node; _} = let lpar, sequence, rpar = node in v.token lpar "("; v.nsepseq "," v.core_pattern sequence; v.token rpar ")" -and print_terminator (v: 'x visitor) = function +and print_terminator (v : 'xvisitor) = function Some semi -> v.token semi ";" | None -> () diff --git a/Print.mli b/Print.mli index 66fae6dfa..97621a8fc 100644 --- a/Print.mli +++ b/Print.mli @@ -2,4 +2,4 @@ open AST -val print_tokens : t -> unit +val print_tokens : parse_phase ast -> unit diff --git a/Typecheck2.ml b/Typecheck2.ml new file mode 100644 index 000000000..ae5d9bdb3 --- /dev/null +++ b/Typecheck2.ml @@ -0,0 +1,337 @@ +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 new file mode 100644 index 000000000..8f5bf59e1 --- /dev/null +++ b/Typecheck2.mli @@ -0,0 +1 @@ +val tc_ast : AST.parse_phase AST.ast -> AST.typecheck_phase AST.ast diff --git a/typecheck.ml b/typecheck.ml index b768a9949..dc2bc374a 100644 --- a/typecheck.ml +++ b/typecheck.ml @@ -1,8 +1,3 @@ - - - - - (* module I = AST (* In *)