balsoft/ligo
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Revert "WIP…"

Browse Source 
This reverts commit 9b9760f052.
This commit is contained in:
Your Name 2019-03-05 21:00:47 +01:00
parent a6585b6e91
commit 78629b6652
9 changed files with 109 additions and 688 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

167
AST.ml
View File

@ -142,45 +142,9 @@ type 'a braces = (lbrace * 'a * rbrace) reg
(* The Abstract Syntax Tree *) (* The Abstract Syntax Tree *)
type ttrue = TTrue type t = < ty: unit > ast
type tfalse = TFalse
type ('a, 'type_expr_typecheck) gadt_if =
Present : 'a -> ('a, ttrue) gadt_if
(* It is possible to further ensure well-typedness at the meta level and 'x ast = {
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; types : 'x type_decl reg list;
constants : 'x const_decl reg list; constants : 'x const_decl reg list;
parameter : 'x parameter_decl reg; parameter : 'x parameter_decl reg;
@ -190,7 +154,6 @@ type 'x ast = {
block : 'x block reg; block : 'x block reg;
eof : eof eof : eof
} }
constraint 'x = 'x x_sig
and 'x parameter_decl = { and 'x parameter_decl = {
kwd_parameter : kwd_parameter; kwd_parameter : kwd_parameter;
@ -199,21 +162,18 @@ and 'x parameter_decl = {
param_type : 'x type_expr; param_type : 'x type_expr;
terminator : semi option terminator : semi option
} }
constraint 'x = 'x x_sig
and 'x storage_decl = { and 'x storage_decl = {
kwd_storage : kwd_storage; kwd_storage : kwd_storage;
store_type : 'x type_expr; store_type : 'x type_expr;
terminator : semi option terminator : semi option
} }
constraint 'x = 'x x_sig
and 'x operations_decl = { and 'x operations_decl = {
kwd_operations : kwd_operations; kwd_operations : kwd_operations;
op_type : 'x type_expr; op_type : 'x type_expr;
terminator : semi option terminator : semi option
} }
constraint 'x = 'x x_sig
(* Type declarations *) (* Type declarations *)
@ -224,79 +184,32 @@ and 'x type_decl = {
type_expr : 'x type_expr; type_expr : 'x type_expr;
terminator : semi option terminator : semi option
} }
constraint 'x = 'x x_sig
and 'x type_expr = and 'x type_expr =
Prod of ('x cartesian, ttrue) gadt_if Prod of 'x cartesian
| Sum of (('x variant, vbar) nsepseq reg, ttrue) gadt_if | Sum of ('x variant, vbar) nsepseq reg
| Record of ('x record_type, ttrue) gadt_if | Record of 'x record_type
| TypeApp of (('x type_name * 'x type_tuple) reg, ttrue) gadt_if | TypeApp of ('x type_name * 'x type_tuple) reg
| ParType of ('x type_expr par, ttrue) gadt_if | ParType of 'x type_expr par
| TAlias of ('x variable, ttrue) gadt_if | TAlias of 'x variable
| 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 and 'x cartesian = ('x type_expr, times) nsepseq reg
constraint 'x = 'x x_sig
and 'x variant = ('x constr * kwd_of * 'x cartesian) reg 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 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 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 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 and 'x type_tuple = ('x type_name, comma) nsepseq par
constraint 'x = 'x x_sig
(* Function and procedure declarations *) (* Function and procedure declarations *)
and 'x lambda_decl = and 'x lambda_decl =
FunDecl of 'x fun_decl reg FunDecl of 'x fun_decl reg
| ProcDecl of 'x proc_decl reg | ProcDecl of 'x proc_decl reg
constraint 'x = 'x x_sig
and 'x fun_decl = { and 'x fun_decl = {
kwd_function : kwd_function; kwd_function : kwd_function;
@ -311,7 +224,6 @@ and 'x fun_decl = {
return : 'x expr; return : 'x expr;
terminator : semi option terminator : semi option
} }
constraint 'x = 'x x_sig
and 'x proc_decl = { and 'x proc_decl = {
kwd_procedure : kwd_procedure; kwd_procedure : kwd_procedure;
@ -322,21 +234,16 @@ and 'x proc_decl = {
block : 'x block reg; block : 'x block reg;
terminator : semi option terminator : semi option
} }
constraint 'x = 'x x_sig
and 'x parameters = ('x param_decl, semi) nsepseq par and 'x parameters = ('x param_decl, semi) nsepseq par
constraint 'x = 'x x_sig
and 'x param_decl = and 'x param_decl =
ParamConst of 'x param_const ParamConst of 'x param_const
| ParamVar of 'x param_var | ParamVar of 'x param_var
constraint 'x = 'x x_sig
and 'x param_const = (kwd_const * 'x variable * colon * 'x type_expr) reg 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 and 'x param_var = (kwd_var * 'x variable * colon * 'x type_expr) reg
constraint 'x = 'x x_sig
and 'x block = { and 'x block = {
opening : kwd_begin; opening : kwd_begin;
@ -344,13 +251,11 @@ and 'x block = {
terminator : semi option; terminator : semi option;
close : kwd_end close : kwd_end
} }
constraint 'x = 'x x_sig
and 'x local_decl = and 'x local_decl =
LocalLam of 'x lambda_decl LocalLam of 'x lambda_decl
| LocalConst of 'x const_decl reg | LocalConst of 'x const_decl reg
| LocalVar of 'x var_decl reg | LocalVar of 'x var_decl reg
constraint 'x = 'x x_sig
and 'x const_decl = { and 'x const_decl = {
kwd_const : kwd_const; kwd_const : kwd_const;
@ -361,7 +266,6 @@ and 'x const_decl = {
init : 'x expr; init : 'x expr;
terminator : semi option terminator : semi option
} }
constraint 'x = 'x x_sig
and 'x var_decl = { and 'x var_decl = {
kwd_var : kwd_var; kwd_var : kwd_var;
@ -372,15 +276,12 @@ and 'x var_decl = {
init : 'x expr; init : 'x expr;
terminator : semi option terminator : semi option
} }
constraint 'x = 'x x_sig
and 'x instructions = ('x instruction, semi) nsepseq reg and 'x instructions = ('x instruction, semi) nsepseq reg
constraint 'x = 'x x_sig
and 'x instruction = and 'x instruction =
Single of 'x single_instr Single of 'x single_instr
| Block of 'x block reg | Block of 'x block reg
constraint 'x = 'x x_sig
and 'x single_instr = and 'x single_instr =
Cond of 'x conditional reg Cond of 'x conditional reg
@ -390,7 +291,6 @@ and 'x single_instr =
| ProcCall of 'x fun_call | ProcCall of 'x fun_call
| Null of kwd_null | Null of kwd_null
| Fail of (kwd_fail * 'x expr) reg | Fail of (kwd_fail * 'x expr) reg
constraint 'x = 'x x_sig
and 'x conditional = { and 'x conditional = {
kwd_if : kwd_if; kwd_if : kwd_if;
@ -400,7 +300,6 @@ and 'x conditional = {
kwd_else : kwd_else; kwd_else : kwd_else;
ifnot : 'x instruction ifnot : 'x instruction
} }
constraint 'x = 'x x_sig
and 'x match_instr = { and 'x match_instr = {
kwd_match : kwd_match; kwd_match : kwd_match;
@ -410,29 +309,22 @@ and 'x match_instr = {
cases : 'x cases; cases : 'x cases;
kwd_end : kwd_end kwd_end : kwd_end
} }
constraint 'x = 'x x_sig
and 'x cases = ('x case, vbar) nsepseq reg and 'x cases = ('x case, vbar) nsepseq reg
constraint 'x = 'x x_sig
and 'x case = ('x pattern * arrow * 'x instruction) reg and 'x case = ('x pattern * arrow * 'x instruction) reg
constraint 'x = 'x x_sig
and 'x ass_instr = ('x variable * ass * 'x expr) reg and 'x ass_instr = ('x variable * ass * 'x expr) reg
constraint 'x = 'x x_sig
and 'x loop = and 'x loop =
While of 'x while_loop While of 'x while_loop
| For of 'x for_loop | For of 'x for_loop
constraint 'x = 'x x_sig
and 'x while_loop = (kwd_while * 'x expr * 'x block reg) reg and 'x while_loop = (kwd_while * 'x expr * 'x block reg) reg
constraint 'x = 'x x_sig
and 'x for_loop = and 'x for_loop =
ForInt of 'x for_int reg ForInt of 'x for_int reg
| ForCollect of 'x for_collect reg | ForCollect of 'x for_collect reg
constraint 'x = 'x x_sig
and 'x for_int = { and 'x for_int = {
kwd_for : kwd_for; kwd_for : kwd_for;
@ -443,7 +335,6 @@ and 'x for_int = {
step : (kwd_step * 'x expr) option; step : (kwd_step * 'x expr) option;
block : 'x block reg block : 'x block reg
} }
constraint 'x = 'x x_sig
and 'x for_collect = { and 'x for_collect = {
kwd_for : kwd_for; kwd_for : kwd_for;
@ -453,7 +344,6 @@ and 'x for_collect = {
expr : 'x expr; expr : 'x expr;
block : 'x block reg block : 'x block reg
} }
constraint 'x = 'x x_sig
(* Expressions *) (* Expressions *)
@ -493,43 +383,33 @@ and 'x expr =
| SomeApp of (c_Some * 'x arguments) reg | SomeApp of (c_Some * 'x arguments) reg
| MapLookUp of 'x map_lookup reg | MapLookUp of 'x map_lookup reg
| ParExpr of 'x expr par | ParExpr of 'x expr par
constraint 'x = 'x x_sig
and 'x tuple = ('x expr, comma) nsepseq par and 'x tuple = ('x expr, comma) nsepseq par
constraint 'x = 'x x_sig
and 'x empty_list = and 'x empty_list =
(lbracket * rbracket * colon * 'x type_expr) par (lbracket * rbracket * colon * 'x type_expr) par
constraint 'x = 'x x_sig
and 'x empty_set = and 'x empty_set =
(lbrace * rbrace * colon * 'x type_expr) par (lbrace * rbrace * colon * 'x type_expr) par
constraint 'x = 'x x_sig
and 'x none_expr = and 'x none_expr =
(c_None * colon * 'x type_expr) par (c_None * colon * 'x type_expr) par
constraint 'x = 'x x_sig
and 'x fun_call = ('x fun_name * 'x arguments) reg and 'x fun_call = ('x fun_name * 'x arguments) reg
constraint 'x = 'x x_sig
and 'x arguments = 'x tuple and 'x arguments = 'x tuple
constraint 'x = 'x x_sig
and 'x constr_app = ('x constr * 'x arguments) reg and 'x constr_app = ('x constr * 'x arguments) reg
constraint 'x = 'x x_sig
and 'x map_lookup = { and 'x map_lookup = {
map_name : 'x variable; map_name : 'x variable;
selector : dot; selector : dot;
index : 'x expr brackets index : 'x expr brackets
} }
constraint 'x = 'x x_sig
(* Patterns *) (* Patterns *)
and 'x pattern = ('x core_pattern, cons) nsepseq reg and 'x pattern = ('x core_pattern, cons) nsepseq reg
constraint 'x = 'x x_sig
and 'x core_pattern = and 'x core_pattern =
PVar of Lexer.lexeme reg PVar of Lexer.lexeme reg
@ -544,39 +424,22 @@ and 'x core_pattern =
| PSome of (c_Some * 'x core_pattern par) reg | PSome of (c_Some * 'x core_pattern par) reg
| PList of 'x list_pattern | PList of 'x list_pattern
| PTuple of ('x core_pattern, comma) nsepseq par | PTuple of ('x core_pattern, comma) nsepseq par
constraint 'x = 'x x_sig
and 'x list_pattern = and 'x list_pattern =
Sugar of ('x core_pattern, comma) sepseq brackets Sugar of ('x core_pattern, comma) sepseq brackets
| Raw of ('x core_pattern * cons * 'x pattern) par | 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 *) (* Projecting regions *)
open! Region open! Region
let type_expr_to_region : parse_phase type_expr -> region = function let type_expr_to_region = function
Prod (Present node) -> node.region Prod node -> node.region
| Sum (Present node) -> node.region | Sum node -> node.region
| Record (Present node) -> node.region | Record node -> node.region
| TypeApp (Present node) -> node.region | TypeApp node -> node.region
| ParType (Present node) -> node.region | ParType node -> node.region
| TAlias (Present node) -> node.region | TAlias node -> node.region
| _ -> .
let expr_to_region = function let expr_to_region = function
Or {region; _} Or {region; _}

122
AST.mli
View File

@ -126,45 +126,9 @@ type 'a braces = (lbrace * 'a * rbrace) reg
(* The Abstract Syntax Tree *) (* The Abstract Syntax Tree *)
type ttrue = TTrue type t = < ty:unit > ast
type tfalse = TFalse
type ('a, 'type_expr_typecheck) gadt_if =
Present : 'a -> ('a, ttrue) gadt_if
(* It is possible to further ensure well-typedness at the meta level and 'x ast = {
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; types : 'x type_decl reg list;
constants : 'x const_decl reg list; constants : 'x const_decl reg list;
parameter : 'x parameter_decl reg; parameter : 'x parameter_decl reg;
@ -174,7 +138,6 @@ type 'x ast = {
block : 'x block reg; block : 'x block reg;
eof : eof eof : eof
} }
constraint 'x = 'x x_sig
and 'x parameter_decl = { and 'x parameter_decl = {
kwd_parameter : kwd_parameter; kwd_parameter : kwd_parameter;
@ -183,21 +146,18 @@ and 'x parameter_decl = {
param_type : 'x type_expr; param_type : 'x type_expr;
terminator : semi option terminator : semi option
} }
constraint 'x = 'x x_sig
and 'x storage_decl = { and 'x storage_decl = {
kwd_storage : kwd_storage; kwd_storage : kwd_storage;
store_type : 'x type_expr; store_type : 'x type_expr;
terminator : semi option terminator : semi option
} }
constraint 'x = 'x x_sig
and 'x operations_decl = { and 'x operations_decl = {
kwd_operations : kwd_operations; kwd_operations : kwd_operations;
op_type : 'x type_expr; op_type : 'x type_expr;
terminator : semi option terminator : semi option
} }
constraint 'x = 'x x_sig
(* Type declarations *) (* Type declarations *)
@ -208,47 +168,32 @@ and 'x type_decl = {
type_expr : 'x type_expr; type_expr : 'x type_expr;
terminator : semi option terminator : semi option
} }
constraint 'x = 'x x_sig
and 'x type_expr = and 'x type_expr =
Prod of ('x cartesian, ttrue) gadt_if Prod of 'x cartesian
| Sum of (('x variant, vbar) nsepseq reg, ttrue) gadt_if | Sum of ('x variant, vbar) nsepseq reg
| Record of ('x record_type, ttrue) gadt_if | Record of 'x record_type
| TypeApp of (('x type_name * 'x type_tuple) reg, ttrue) gadt_if | TypeApp of ('x type_name * 'x type_tuple) reg
| ParType of ('x type_expr par, ttrue) gadt_if | ParType of 'x type_expr par
| TAlias of ('x variable, ttrue) gadt_if | TAlias of 'x variable
| 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 and 'x cartesian = ('x type_expr, times) nsepseq reg
constraint 'x = 'x x_sig
and 'x variant = ('x constr * kwd_of * 'x cartesian) reg 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 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 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 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 and 'x type_tuple = ('x type_name, comma) nsepseq par
constraint 'x = 'x x_sig
(* Function and procedure declarations *) (* Function and procedure declarations *)
and 'x lambda_decl = and 'x lambda_decl =
FunDecl of 'x fun_decl reg FunDecl of 'x fun_decl reg
| ProcDecl of 'x proc_decl reg | ProcDecl of 'x proc_decl reg
constraint 'x = 'x x_sig
and 'x fun_decl = { and 'x fun_decl = {
kwd_function : kwd_function; kwd_function : kwd_function;
@ -263,7 +208,6 @@ and 'x fun_decl = {
return : 'x expr; return : 'x expr;
terminator : semi option terminator : semi option
} }
constraint 'x = 'x x_sig
and 'x proc_decl = { and 'x proc_decl = {
kwd_procedure : kwd_procedure; kwd_procedure : kwd_procedure;
@ -274,21 +218,16 @@ and 'x proc_decl = {
block : 'x block reg; block : 'x block reg;
terminator : semi option terminator : semi option
} }
constraint 'x = 'x x_sig
and 'x parameters = ('x param_decl, semi) nsepseq par and 'x parameters = ('x param_decl, semi) nsepseq par
constraint 'x = 'x x_sig
and 'x param_decl = and 'x param_decl =
ParamConst of 'x param_const ParamConst of 'x param_const
| ParamVar of 'x param_var | ParamVar of 'x param_var
constraint 'x = 'x x_sig
and 'x param_const = (kwd_const * 'x variable * colon * 'x type_expr) reg 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 and 'x param_var = (kwd_var * 'x variable * colon * 'x type_expr) reg
constraint 'x = 'x x_sig
and 'x block = { and 'x block = {
opening : kwd_begin; opening : kwd_begin;
@ -296,13 +235,11 @@ and 'x block = {
terminator : semi option; terminator : semi option;
close : kwd_end close : kwd_end
} }
constraint 'x = 'x x_sig
and 'x local_decl = and 'x local_decl =
LocalLam of 'x lambda_decl LocalLam of 'x lambda_decl
| LocalConst of 'x const_decl reg | LocalConst of 'x const_decl reg
| LocalVar of 'x var_decl reg | LocalVar of 'x var_decl reg
constraint 'x = 'x x_sig
and 'x const_decl = { and 'x const_decl = {
kwd_const : kwd_const; kwd_const : kwd_const;
@ -313,7 +250,6 @@ and 'x const_decl = {
init : 'x expr; init : 'x expr;
terminator : semi option terminator : semi option
} }
constraint 'x = 'x x_sig
and 'x var_decl = { and 'x var_decl = {
kwd_var : kwd_var; kwd_var : kwd_var;
@ -324,15 +260,12 @@ and 'x var_decl = {
init : 'x expr; init : 'x expr;
terminator : semi option terminator : semi option
} }
constraint 'x = 'x x_sig
and 'x instructions = ('x instruction, semi) nsepseq reg and 'x instructions = ('x instruction, semi) nsepseq reg
constraint 'x = 'x x_sig
and 'x instruction = and 'x instruction =
Single of 'x single_instr Single of 'x single_instr
| Block of 'x block reg | Block of 'x block reg
constraint 'x = 'x x_sig
and 'x single_instr = and 'x single_instr =
Cond of 'x conditional reg Cond of 'x conditional reg
@ -342,7 +275,6 @@ and 'x single_instr =
| ProcCall of 'x fun_call | ProcCall of 'x fun_call
| Null of kwd_null | Null of kwd_null
| Fail of (kwd_fail * 'x expr) reg | Fail of (kwd_fail * 'x expr) reg
constraint 'x = 'x x_sig
and 'x conditional = { and 'x conditional = {
kwd_if : kwd_if; kwd_if : kwd_if;
@ -352,7 +284,6 @@ and 'x conditional = {
kwd_else : kwd_else; kwd_else : kwd_else;
ifnot : 'x instruction ifnot : 'x instruction
} }
constraint 'x = 'x x_sig
and 'x match_instr = { and 'x match_instr = {
kwd_match : kwd_match; kwd_match : kwd_match;
@ -362,29 +293,22 @@ and 'x match_instr = {
cases : 'x cases; cases : 'x cases;
kwd_end : kwd_end kwd_end : kwd_end
} }
constraint 'x = 'x x_sig
and 'x cases = ('x case, vbar) nsepseq reg and 'x cases = ('x case, vbar) nsepseq reg
constraint 'x = 'x x_sig
and 'x case = ('x pattern * arrow * 'x instruction) reg and 'x case = ('x pattern * arrow * 'x instruction) reg
constraint 'x = 'x x_sig
and 'x ass_instr = ('x variable * ass * 'x expr) reg and 'x ass_instr = ('x variable * ass * 'x expr) reg
constraint 'x = 'x x_sig
and 'x loop = and 'x loop =
While of 'x while_loop While of 'x while_loop
| For of 'x for_loop | For of 'x for_loop
constraint 'x = 'x x_sig
and 'x while_loop = (kwd_while * 'x expr * 'x block reg) reg and 'x while_loop = (kwd_while * 'x expr * 'x block reg) reg
constraint 'x = 'x x_sig
and 'x for_loop = and 'x for_loop =
ForInt of 'x for_int reg ForInt of 'x for_int reg
| ForCollect of 'x for_collect reg | ForCollect of 'x for_collect reg
constraint 'x = 'x x_sig
and 'x for_int = { and 'x for_int = {
kwd_for : kwd_for; kwd_for : kwd_for;
@ -395,7 +319,6 @@ and 'x for_int = {
step : (kwd_step * 'x expr) option; step : (kwd_step * 'x expr) option;
block : 'x block reg block : 'x block reg
} }
constraint 'x = 'x x_sig
and 'x for_collect = { and 'x for_collect = {
kwd_for : kwd_for; kwd_for : kwd_for;
@ -405,7 +328,6 @@ and 'x for_collect = {
expr : 'x expr; expr : 'x expr;
block : 'x block reg block : 'x block reg
} }
constraint 'x = 'x x_sig
(* Expressions *) (* Expressions *)
@ -445,43 +367,33 @@ and 'x expr =
| SomeApp of (c_Some * 'x arguments) reg | SomeApp of (c_Some * 'x arguments) reg
| MapLookUp of 'x map_lookup reg | MapLookUp of 'x map_lookup reg
| ParExpr of 'x expr par | ParExpr of 'x expr par
constraint 'x = 'x x_sig
and 'x tuple = ('x expr, comma) nsepseq par and 'x tuple = ('x expr, comma) nsepseq par
constraint 'x = 'x x_sig
and 'x empty_list = and 'x empty_list =
(lbracket * rbracket * colon * 'x type_expr) par (lbracket * rbracket * colon * 'x type_expr) par
constraint 'x = 'x x_sig
and 'x empty_set = and 'x empty_set =
(lbrace * rbrace * colon * 'x type_expr) par (lbrace * rbrace * colon * 'x type_expr) par
constraint 'x = 'x x_sig
and 'x none_expr = and 'x none_expr =
(c_None * colon * 'x type_expr) par (c_None * colon * 'x type_expr) par
constraint 'x = 'x x_sig
and 'x fun_call = ('x fun_name * 'x arguments) reg and 'x fun_call = ('x fun_name * 'x arguments) reg
constraint 'x = 'x x_sig
and 'x arguments = 'x tuple and 'x arguments = 'x tuple
constraint 'x = 'x x_sig
and 'x constr_app = ('x constr * 'x arguments) reg and 'x constr_app = ('x constr * 'x arguments) reg
constraint 'x = 'x x_sig
and 'x map_lookup = { and 'x map_lookup = {
map_name : 'x variable; map_name : 'x variable;
selector : dot; selector : dot;
index : 'x expr brackets index : 'x expr brackets
} }
constraint 'x = 'x x_sig
(* Patterns *) (* Patterns *)
and 'x pattern = ('x core_pattern, cons) nsepseq reg and 'x pattern = ('x core_pattern, cons) nsepseq reg
constraint 'x = 'x x_sig
and 'x core_pattern = and 'x core_pattern =
PVar of Lexer.lexeme reg PVar of Lexer.lexeme reg
@ -496,30 +408,14 @@ and 'x core_pattern =
| PSome of (c_Some * 'x core_pattern par) reg | PSome of (c_Some * 'x core_pattern par) reg
| PList of 'x list_pattern | PList of 'x list_pattern
| PTuple of ('x core_pattern, comma) nsepseq par | PTuple of ('x core_pattern, comma) nsepseq par
constraint 'x = 'x x_sig
and 'x list_pattern = and 'x list_pattern =
Sugar of ('x core_pattern, comma) sepseq brackets Sugar of ('x core_pattern, comma) sepseq brackets
| Raw of ('x core_pattern * cons * 'x pattern) par | 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 *) (* 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 val expr_to_region : 'x expr -> Region.t

12
Parser.mly
View File

@ -171,9 +171,9 @@ type_decl:
in {region; value}} in {region; value}}
type_expr: type_expr:
cartesian { Prod (Present $1) } cartesian { Prod $1 }
| sum_type { Sum (Present $1) } | sum_type { Sum $1 }
| record_type { Record (Present $1) } | record_type { Record $1 }
cartesian: cartesian:
nsepseq(core_type,TIMES) { nsepseq(core_type,TIMES) {
@ -183,14 +183,14 @@ cartesian:
core_type: core_type:
type_name { type_name {
TAlias (Present $1) TAlias $1
} }
| type_name type_tuple { | type_name type_tuple {
let region = cover $1.region $2.region let region = cover $1.region $2.region
in TypeApp (Present {region; value = $1,$2}) in TypeApp {region; value = $1,$2}
} }
| par(type_expr) { | par(type_expr) {
ParType (Present $1) ParType $1
} }
type_tuple: type_tuple:

6
ParserMain.ml
View File

@ -57,10 +57,8 @@ let tokeniser = read ~log
let () = let () =
try try
let ast = Parser.program tokeniser buffer in let ast = Parser.program tokeniser buffer in
let () = if Utils.String.Set.mem "parser" EvalOpt.verbose if Utils.String.Set.mem "parser" EvalOpt.verbose
then Print.print_tokens ast in then Print.print_tokens ast
let _ = Typecheck2.tc_ast ast
in ()
with with
Lexer.Error err -> Lexer.Error err ->
close_all (); close_all ();

17
Print.ml
View File

@ -47,7 +47,7 @@ and print_int _visitor {region; value = lexeme, abstract} =
(* Main printing function *) (* 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; List.iter v.type_decl ast.types;
v.parameter_decl ast.parameter; v.parameter_decl ast.parameter;
v.storage_decl ast.storage; v.storage_decl ast.storage;
@ -81,15 +81,12 @@ and print_type_decl (v : 'xvisitor) {value=node; _} =
v.terminator node.terminator v.terminator node.terminator
and print_type_expr (v: 'x visitor) = function and print_type_expr (v: 'x visitor) = function
Prod (Present cartesian) -> v.cartesian cartesian Prod cartesian -> v.cartesian cartesian
| Sum (Present sum_type) -> v.sum_type sum_type | Sum sum_type -> v.sum_type sum_type
| Record (Present record_type) -> v.record_type record_type | Record record_type -> v.record_type record_type
| TypeApp (Present type_app) -> v.type_app type_app | TypeApp type_app -> v.type_app type_app
| ParType (Present par_type) -> v.par_type par_type | ParType par_type -> v.par_type par_type
| TAlias (Present type_alias) -> v.var type_alias | TAlias 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: 'x visitor) {value=sequence; _} =
v.nsepseq "*" v.type_expr sequence v.nsepseq "*" v.type_expr sequence

2
Print.mli
View File

@ -2,4 +2,4 @@
open AST open AST
val print_tokens : parse_phase ast -> unit val print_tokens : t -> unit

337
Typecheck2.ml
View File

@ -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
*)

1
Typecheck2.mli
View File

@ -1 +0,0 @@
val tc_ast : AST.parse_phase AST.ast -> AST.typecheck_phase AST.ast

5
typecheck.ml
View File

@ -1,3 +1,8 @@
(* (*
module I = AST (* In *) module I = AST (* In *)