diff --git a/AST.ml b/AST.ml index 2fb5d70ff..38a3d2cdc 100644 --- a/AST.ml +++ b/AST.ml @@ -1,3 +1,5 @@ +[@@@warning "-30"] + (* Abstract Syntax Tree (AST) for Ligo *) open Utils @@ -134,7 +136,7 @@ type 'a braces = (lbrace * 'a * rbrace) reg (* The Abstract Syntax Tree *) -type t = < +type t = { types : type_decl list; parameter : parameter_decl; storage : storage_decl; @@ -142,7 +144,7 @@ type t = < lambdas : lambda_decl list; block : block reg; eof : eof -> +} and ast = t @@ -182,7 +184,7 @@ and lambda_decl = FunDecl of fun_decl reg | ProcDecl of proc_decl reg -and fun_decl = < +and fun_decl = { kwd_function : kwd_function; var : variable; param : parameters; @@ -192,15 +194,15 @@ and fun_decl = < body : block reg; kwd_with : kwd_with; return : expr -> +} -and proc_decl = < +and proc_decl = { kwd_procedure : kwd_procedure; var : variable; param : parameters; kwd_is : kwd_is; body : block reg -> +} and parameters = (param_decl, semi) nsepseq par @@ -210,23 +212,23 @@ and var_kind = Mutable of kwd_var | Const of kwd_const -and block = < +and block = { decls : value_decls; opening : kwd_begin; instr : instructions; close : kwd_end -> +} and value_decls = (var_decl reg, semi) sepseq reg -and var_decl = < +and var_decl = { kind : var_kind; var : variable; colon : colon; vtype : type_expr; setter : Region.t; (* "=" or ":=" *) init : expr -> +} and instructions = (instruction, semi) nsepseq reg @@ -242,22 +244,22 @@ and single_instr = | ProcCall of fun_call | Null of kwd_null -and conditional = < +and conditional = { kwd_if : kwd_if; test : expr; kwd_then : kwd_then; ifso : instruction; kwd_else : kwd_else; ifnot : instruction -> +} -and match_instr = < +and match_instr = { kwd_match : kwd_match; expr : expr; kwd_with : kwd_with; cases : cases; kwd_end : kwd_end -> +} and cases = (case, vbar) nsepseq reg @@ -275,7 +277,7 @@ and for_loop = ForInt of for_int reg | ForCollect of for_collect reg -and for_int = < +and for_int = { kwd_for : kwd_for; asgnmnt : asgnmnt_instr; down : kwd_down option; @@ -283,16 +285,16 @@ and for_int = < bound : expr; step : (kwd_step * expr) option; block : block reg -> +} -and for_collect = < +and for_collect = { kwd_for : kwd_for; var : variable; bind_to : (arrow * variable) option; kwd_in : kwd_in; expr : expr; block : block reg -> +} (* Expressions *) @@ -350,11 +352,11 @@ and arguments = tuple and constr_app = (constr * arguments) reg -and map_lookup = < +and map_lookup = { map_name : variable; selector : dot; index : expr brackets -> +} (* Patterns *) @@ -459,8 +461,8 @@ let core_pattern_to_region = function (* Printing the tokens with their source regions *) -type xyz = - < asgnmnt_instr : asgnmnt_instr -> unit; +type xyz = { + asgnmnt_instr : asgnmnt_instr -> unit; bind_to : (region * variable) option -> unit; block : block reg -> unit; bytes : (string * MBytes.t) reg -> unit; @@ -528,7 +530,8 @@ type xyz = var_decl : var_decl reg -> unit; var_kind : var_kind -> unit; variant : variant -> unit; - while_loop : while_loop -> unit > + while_loop : while_loop -> unit +} let printf = Printf.printf @@ -571,490 +574,490 @@ and print_int (_visitor : xyz) {region; value = lexeme, abstract} = (* main print function *) and print_tokens (visitor : xyz) ast = - List.iter visitor#type_decl ast#types; - visitor#parameter_decl ast#parameter; - visitor#storage_decl ast#storage; - visitor#operations_decl ast#operations; - List.iter visitor#lambda_decl ast#lambdas; - visitor#block ast#block; - visitor#token ast#eof "EOF" + List.iter visitor.type_decl ast.types; + visitor.parameter_decl ast.parameter; + visitor.storage_decl ast.storage; + visitor.operations_decl ast.operations; + List.iter visitor.lambda_decl ast.lambdas; + visitor.block ast.block; + visitor.token ast.eof "EOF" and print_parameter_decl (visitor : xyz) {value=node; _} = let kwd_parameter, variable, colon, type_expr = node in - visitor#token kwd_parameter "parameter"; - visitor#var variable; - visitor#token colon ":"; - visitor#type_expr type_expr + visitor.token kwd_parameter "parameter"; + visitor.var variable; + visitor.token colon ":"; + visitor.type_expr type_expr and print_storage_decl (visitor : xyz) {value=node; _} = let kwd_storage, type_expr = node in - visitor#token kwd_storage "storage"; - visitor#type_expr type_expr + visitor.token kwd_storage "storage"; + visitor.type_expr type_expr and print_operations_decl (visitor : xyz) {value=node; _} = let kwd_operations, type_expr = node in - visitor#token kwd_operations "operations"; - visitor#type_expr type_expr + visitor.token kwd_operations "operations"; + visitor.type_expr type_expr and print_type_decl (visitor : xyz) {value=node; _} = let kwd_type, type_name, kwd_is, type_expr = node in - visitor#token kwd_type "type"; - visitor#var type_name; - visitor#token kwd_is "is"; - visitor#type_expr type_expr + visitor.token kwd_type "type"; + visitor.var type_name; + visitor.token kwd_is "is"; + visitor.type_expr type_expr and print_type_expr (visitor : xyz) = function - Prod cartesian -> visitor#cartesian cartesian -| Sum sum_type -> visitor#sum_type sum_type -| Record record_type -> visitor#record_type record_type -| TypeApp type_app -> visitor#type_app type_app -| ParType par_type -> visitor#par_type par_type -| TAlias type_alias -> visitor#var type_alias + Prod cartesian -> visitor.cartesian cartesian +| Sum sum_type -> visitor.sum_type sum_type +| Record record_type -> visitor.record_type record_type +| TypeApp type_app -> visitor.type_app type_app +| ParType par_type -> visitor.par_type par_type +| TAlias type_alias -> visitor.var type_alias and print_cartesian (visitor : xyz) {value=sequence; _} = - visitor#nsepseq "*" visitor#type_expr sequence + visitor.nsepseq "*" visitor.type_expr sequence and print_variant (visitor : xyz) {value=node; _} = let constr, kwd_of, cartesian = node in - visitor#constr constr; - visitor#token kwd_of "of"; - visitor#cartesian cartesian + visitor.constr constr; + visitor.token kwd_of "of"; + visitor.cartesian cartesian and print_sum_type (visitor : xyz) {value=sequence; _} = - visitor#nsepseq "|" visitor#variant sequence + visitor.nsepseq "|" visitor.variant sequence and print_record_type (visitor : xyz) {value=node; _} = let kwd_record, field_decls, kwd_end = node in - visitor#token kwd_record "record"; - visitor#field_decls field_decls; - visitor#token kwd_end "end" + visitor.token kwd_record "record"; + visitor.field_decls field_decls; + visitor.token kwd_end "end" and print_type_app (visitor : xyz) {value=node; _} = let type_name, type_tuple = node in - visitor#var type_name; - visitor#type_tuple type_tuple + visitor.var type_name; + visitor.type_tuple type_tuple and print_par_type (visitor : xyz) {value=node; _} = let lpar, type_expr, rpar = node in - visitor#token lpar "("; - visitor#type_expr type_expr; - visitor#token rpar ")" + visitor.token lpar "("; + visitor.type_expr type_expr; + visitor.token rpar ")" and print_field_decls (visitor : xyz) sequence = - visitor#nsepseq ";" visitor#field_decl sequence + visitor.nsepseq ";" visitor.field_decl sequence and print_field_decl (visitor : xyz) {value=node; _} = let var, colon, type_expr = node in - visitor#var var; - visitor#token colon ":"; - visitor#type_expr type_expr + visitor.var var; + visitor.token colon ":"; + visitor.type_expr type_expr and print_type_tuple (visitor : xyz) {value=node; _} = let lpar, sequence, rpar = node in - visitor#token lpar "("; - visitor#nsepseq "," visitor#var sequence; - visitor#token rpar ")" + visitor.token lpar "("; + visitor.nsepseq "," visitor.var sequence; + visitor.token rpar ")" and print_lambda_decl (visitor : xyz) = function - FunDecl fun_decl -> visitor#fun_decl fun_decl -| ProcDecl proc_decl -> visitor#proc_decl proc_decl + FunDecl fun_decl -> visitor.fun_decl fun_decl +| ProcDecl proc_decl -> visitor.proc_decl proc_decl and print_fun_decl (visitor : xyz) {value=node; _} = - visitor#token node#kwd_function "function"; - visitor#var node#var; - visitor#parameters node#param; - visitor#token node#colon ":"; - visitor#type_expr node#ret_type; - visitor#token node#kwd_is "is"; - visitor#block node#body; - visitor#token node#kwd_with "with"; - visitor#expr node#return + visitor.token node.kwd_function "function"; + visitor.var node.var; + visitor.parameters node.param; + visitor.token node.colon ":"; + visitor.type_expr node.ret_type; + visitor.token node.kwd_is "is"; + visitor.block node.body; + visitor.token node.kwd_with "with"; + visitor.expr node.return and print_proc_decl (visitor : xyz) {value=node; _} = - visitor#token node#kwd_procedure "procedure"; - visitor#var node#var; - visitor#parameters node#param; - visitor#token node#kwd_is "is"; - visitor#block node#body + visitor.token node.kwd_procedure "procedure"; + visitor.var node.var; + visitor.parameters node.param; + visitor.token node.kwd_is "is"; + visitor.block node.body and print_parameters (visitor : xyz) {value=node; _} = let lpar, sequence, rpar = node in - visitor#token lpar "("; - visitor#nsepseq ";" visitor#param_decl sequence; - visitor#token rpar ")" + visitor.token lpar "("; + visitor.nsepseq ";" visitor.param_decl sequence; + visitor.token rpar ")" and print_param_decl (visitor : xyz) {value=node; _} = let var_kind, variable, colon, type_expr = node in - visitor#var_kind var_kind; - visitor#var variable; - visitor#token colon ":"; - visitor#type_expr type_expr + visitor.var_kind var_kind; + visitor.var variable; + visitor.token colon ":"; + visitor.type_expr type_expr and print_var_kind (visitor : xyz) = function - Mutable kwd_var -> visitor#token kwd_var "var" -| Const kwd_const -> visitor#token kwd_const "const" + Mutable kwd_var -> visitor.token kwd_var "var" +| Const kwd_const -> visitor.token kwd_const "const" and print_block (visitor : xyz) {value=node; _} = - visitor#value_decls node#decls; - visitor#token node#opening "begin"; - visitor#instructions node#instr; - visitor#token node#close "end" + visitor.value_decls node.decls; + visitor.token node.opening "begin"; + visitor.instructions node.instr; + visitor.token node.close "end" and print_value_decls (visitor : xyz) {value=sequence; _} = - visitor#sepseq ";" visitor#var_decl sequence + visitor.sepseq ";" visitor.var_decl sequence and print_var_decl (visitor : xyz) {value=node; _} = let setter = - match node#kind with + match node.kind with Mutable _ -> ":=" | Const _ -> "=" in - visitor#var_kind node#kind; - visitor#var node#var; - visitor#token node#colon ":"; - visitor#type_expr node#vtype; - visitor#token node#setter setter; - visitor#expr node#init + visitor.var_kind node.kind; + visitor.var node.var; + visitor.token node.colon ":"; + visitor.type_expr node.vtype; + visitor.token node.setter setter; + visitor.expr node.init and print_instructions (visitor : xyz) {value=sequence; _} = - visitor#nsepseq ";" visitor#instruction sequence + visitor.nsepseq ";" visitor.instruction sequence and print_instruction (visitor : xyz) = function - Single instr -> visitor#single_instr instr -| Block block -> visitor#block block + Single instr -> visitor.single_instr instr +| Block block -> visitor.block block and print_single_instr (visitor : xyz) = function - Cond {value; _} -> visitor#conditional value -| Match {value; _} -> visitor#match_instr value -| Asgnmnt instr -> visitor#asgnmnt_instr instr -| Loop loop -> visitor#loop loop -| ProcCall fun_call -> visitor#fun_call fun_call -| Null kwd_null -> visitor#token kwd_null "null" + Cond {value; _} -> visitor.conditional value +| Match {value; _} -> visitor.match_instr value +| Asgnmnt instr -> visitor.asgnmnt_instr instr +| Loop loop -> visitor.loop loop +| ProcCall fun_call -> visitor.fun_call fun_call +| Null kwd_null -> visitor.token kwd_null "null" and print_conditional (visitor : xyz) node = - visitor#token node#kwd_if "if"; - visitor#expr node#test; - visitor#token node#kwd_then "then"; - visitor#instruction node#ifso; - visitor#token node#kwd_else "else"; - visitor#instruction node#ifnot + visitor.token node.kwd_if "if"; + visitor.expr node.test; + visitor.token node.kwd_then "then"; + visitor.instruction node.ifso; + visitor.token node.kwd_else "else"; + visitor.instruction node.ifnot and print_match_instr (visitor : xyz) node = - visitor#token node#kwd_match "match"; - visitor#expr node#expr; - visitor#token node#kwd_with "with"; - visitor#cases node#cases; - visitor#token node#kwd_end "end" + visitor.token node.kwd_match "match"; + visitor.expr node.expr; + visitor.token node.kwd_with "with"; + visitor.cases node.cases; + visitor.token node.kwd_end "end" and print_cases (visitor : xyz) {value=sequence; _} = - visitor#nsepseq "|" visitor#case sequence + visitor.nsepseq "|" visitor.case sequence and print_case (visitor : xyz) {value=node; _} = let pattern, arrow, instruction = node in - visitor#pattern pattern; - visitor#token arrow "->"; - visitor#instruction instruction + visitor.pattern pattern; + visitor.token arrow "->"; + visitor.instruction instruction and print_asgnmnt_instr (visitor : xyz) {value=node; _} = let variable, asgnmnt, expr = node in - visitor#var variable; - visitor#token asgnmnt ":="; - visitor#expr expr + visitor.var variable; + visitor.token asgnmnt ":="; + visitor.expr expr and print_loop (visitor : xyz) = function - While while_loop -> visitor#while_loop while_loop -| For for_loop -> visitor#for_loop for_loop + While while_loop -> visitor.while_loop while_loop +| For for_loop -> visitor.for_loop for_loop and print_while_loop (visitor : xyz) {value=node; _} = let kwd_while, expr, block = node in - visitor#token kwd_while "while"; - visitor#expr expr; - visitor#block block + visitor.token kwd_while "while"; + visitor.expr expr; + visitor.block block and print_for_loop (visitor : xyz) = function - ForInt for_int -> visitor#for_int for_int -| ForCollect for_collect -> visitor#for_collect for_collect + ForInt for_int -> visitor.for_int for_int +| ForCollect for_collect -> visitor.for_collect for_collect -and print_for_int (visitor : xyz) {value=node; _} = - visitor#token node#kwd_for "for"; - visitor#asgnmnt_instr node#asgnmnt; - visitor#down node#down; - visitor#token node#kwd_to "to"; - visitor#expr node#bound; - visitor#step node#step; - visitor#block node#block +and print_for_int (visitor : xyz) ({value=node; _} : for_int reg) = + visitor.token node.kwd_for "for"; + visitor.asgnmnt_instr node.asgnmnt; + visitor.down node.down; + visitor.token node.kwd_to "to"; + visitor.expr node.bound; + visitor.step node.step; + visitor.block node.block and print_down (visitor : xyz) = function - Some kwd_down -> visitor#token kwd_down "down" + Some kwd_down -> visitor.token kwd_down "down" | None -> () and print_step (visitor : xyz) = function Some (kwd_step, expr) -> - visitor#token kwd_step "step"; - visitor#expr expr + visitor.token kwd_step "step"; + visitor.expr expr | None -> () -and print_for_collect (visitor : xyz) {value=node; _} = - visitor#token node#kwd_for "for"; - visitor#var node#var; - visitor#bind_to node#bind_to; - visitor#token node#kwd_in "in"; - visitor#expr node#expr; - visitor#block node#block +and print_for_collect (visitor : xyz) ({value=node; _} : for_collect reg) = + visitor.token node.kwd_for "for"; + visitor.var node.var; + visitor.bind_to node.bind_to; + visitor.token node.kwd_in "in"; + visitor.expr node.expr; + visitor.block node.block and print_bind_to (visitor : xyz) = function Some (arrow, variable) -> - visitor#token arrow "->"; - visitor#var variable + visitor.token arrow "->"; + visitor.var variable | None -> () and print_expr (visitor : xyz) = function Or {value = expr1, bool_or, expr2; _} -> - visitor#expr expr1; visitor#token bool_or "||"; visitor#expr expr2 + visitor.expr expr1; visitor.token bool_or "||"; visitor.expr expr2 | And {value = expr1, bool_and, expr2; _} -> - visitor#expr expr1; visitor#token bool_and "&&"; visitor#expr expr2 + visitor.expr expr1; visitor.token bool_and "&&"; visitor.expr expr2 | Lt {value = expr1, lt, expr2; _} -> - visitor#expr expr1; visitor#token lt "<"; visitor#expr expr2 + visitor.expr expr1; visitor.token lt "<"; visitor.expr expr2 | Leq {value = expr1, leq, expr2; _} -> - visitor#expr expr1; visitor#token leq "<="; visitor#expr expr2 + visitor.expr expr1; visitor.token leq "<="; visitor.expr expr2 | Gt {value = expr1, gt, expr2; _} -> - visitor#expr expr1; visitor#token gt ">"; visitor#expr expr2 + visitor.expr expr1; visitor.token gt ">"; visitor.expr expr2 | Geq {value = expr1, geq, expr2; _} -> - visitor#expr expr1; visitor#token geq ">="; visitor#expr expr2 + visitor.expr expr1; visitor.token geq ">="; visitor.expr expr2 | Equal {value = expr1, equal, expr2; _} -> - visitor#expr expr1; visitor#token equal "="; visitor#expr expr2 + visitor.expr expr1; visitor.token equal "="; visitor.expr expr2 | Neq {value = expr1, neq, expr2; _} -> - visitor#expr expr1; visitor#token neq "=/="; visitor#expr expr2 + visitor.expr expr1; visitor.token neq "=/="; visitor.expr expr2 | Cat {value = expr1, cat, expr2; _} -> - visitor#expr expr1; visitor#token cat "^"; visitor#expr expr2 + visitor.expr expr1; visitor.token cat "^"; visitor.expr expr2 | Cons {value = expr1, cons, expr2; _} -> - visitor#expr expr1; visitor#token cons "<:"; visitor#expr expr2 + visitor.expr expr1; visitor.token cons "<:"; visitor.expr expr2 | Add {value = expr1, add, expr2; _} -> - visitor#expr expr1; visitor#token add "+"; visitor#expr expr2 + visitor.expr expr1; visitor.token add "+"; visitor.expr expr2 | Sub {value = expr1, sub, expr2; _} -> - visitor#expr expr1; visitor#token sub "-"; visitor#expr expr2 + visitor.expr expr1; visitor.token sub "-"; visitor.expr expr2 | Mult {value = expr1, mult, expr2; _} -> - visitor#expr expr1; visitor#token mult "*"; visitor#expr expr2 + visitor.expr expr1; visitor.token mult "*"; visitor.expr expr2 | Div {value = expr1, div, expr2; _} -> - visitor#expr expr1; visitor#token div "/"; visitor#expr expr2 + visitor.expr expr1; visitor.token div "/"; visitor.expr expr2 | Mod {value = expr1, kwd_mod, expr2; _} -> - visitor#expr expr1; visitor#token kwd_mod "mod"; visitor#expr expr2 + visitor.expr expr1; visitor.token kwd_mod "mod"; visitor.expr expr2 | Neg {value = minus, expr; _} -> - visitor#token minus "-"; visitor#expr expr + visitor.token minus "-"; visitor.expr expr | Not {value = kwd_not, expr; _} -> - visitor#token kwd_not "not"; visitor#expr expr -| Int i -> visitor#int i -| Var v -> visitor#var v -| String s -> visitor#string s -| Bytes b -> visitor#bytes b -| False region -> visitor#token region "False" -| True region -> visitor#token region "True" -| Unit region -> visitor#token region "Unit" -| Tuple tuple -> visitor#tuple tuple -| List list -> visitor#list list -| EmptyList elist -> visitor#empty_list elist -| Set set -> visitor#set set -| EmptySet eset -> visitor#empty_set eset -| NoneExpr nexpr -> visitor#none_expr nexpr -| FunCall fun_call -> visitor#fun_call fun_call -| ConstrApp capp -> visitor#constr_app capp -| SomeApp sapp -> visitor#some_app sapp -| MapLookUp lookup -> visitor#map_lookup lookup -| ParExpr pexpr -> visitor#par_expr pexpr + visitor.token kwd_not "not"; visitor.expr expr +| Int i -> visitor.int i +| Var v -> visitor.var v +| String s -> visitor.string s +| Bytes b -> visitor.bytes b +| False region -> visitor.token region "False" +| True region -> visitor.token region "True" +| Unit region -> visitor.token region "Unit" +| Tuple tuple -> visitor.tuple tuple +| List list -> visitor.list list +| EmptyList elist -> visitor.empty_list elist +| Set set -> visitor.set set +| EmptySet eset -> visitor.empty_set eset +| NoneExpr nexpr -> visitor.none_expr nexpr +| FunCall fun_call -> visitor.fun_call fun_call +| ConstrApp capp -> visitor.constr_app capp +| SomeApp sapp -> visitor.some_app sapp +| MapLookUp lookup -> visitor.map_lookup lookup +| ParExpr pexpr -> visitor.par_expr pexpr and print_tuple (visitor : xyz) {value=node; _} = let lpar, sequence, rpar = node in - visitor#token lpar "("; - visitor#nsepseq "," visitor#expr sequence; - visitor#token rpar ")" + visitor.token lpar "("; + visitor.nsepseq "," visitor.expr sequence; + visitor.token rpar ")" and print_list (visitor : xyz) {value=node; _} = let lbra, sequence, rbra = node in - visitor#token lbra "["; - visitor#nsepseq "," visitor#expr sequence; - visitor#token rbra "]" + visitor.token lbra "["; + visitor.nsepseq "," visitor.expr sequence; + visitor.token rbra "]" and print_empty_list (visitor : xyz) {value=node; _} = let lpar, (lbracket, rbracket, colon, type_expr), rpar = node in - visitor#token lpar "("; - visitor#token lbracket "["; - visitor#token rbracket "]"; - visitor#token colon ":"; - visitor#type_expr type_expr; - visitor#token rpar ")" + visitor.token lpar "("; + visitor.token lbracket "["; + visitor.token rbracket "]"; + visitor.token colon ":"; + visitor.type_expr type_expr; + visitor.token rpar ")" and print_set (visitor : xyz) {value=node; _} = let lbrace, sequence, rbrace = node in - visitor#token lbrace "{"; - visitor#nsepseq "," visitor#expr sequence; - visitor#token rbrace "}" + visitor.token lbrace "{"; + visitor.nsepseq "," visitor.expr sequence; + visitor.token rbrace "}" and print_empty_set (visitor : xyz) {value=node; _} = let lpar, (lbrace, rbrace, colon, type_expr), rpar = node in - visitor#token lpar "("; - visitor#token lbrace "{"; - visitor#token rbrace "}"; - visitor#token colon ":"; - visitor#type_expr type_expr; - visitor#token rpar ")" + visitor.token lpar "("; + visitor.token lbrace "{"; + visitor.token rbrace "}"; + visitor.token colon ":"; + visitor.type_expr type_expr; + visitor.token rpar ")" and print_none_expr (visitor : xyz) {value=node; _} = let lpar, (c_None, colon, type_expr), rpar = node in - visitor#token lpar "("; - visitor#token c_None "None"; - visitor#token colon ":"; - visitor#type_expr type_expr; - visitor#token rpar ")" + visitor.token lpar "("; + visitor.token c_None "None"; + visitor.token colon ":"; + visitor.type_expr type_expr; + visitor.token rpar ")" and print_fun_call (visitor : xyz) {value=node; _} = let fun_name, arguments = node in - visitor#var fun_name; - visitor#tuple arguments + visitor.var fun_name; + visitor.tuple arguments and print_constr_app (visitor : xyz) {value=node; _} = let constr, arguments = node in - visitor#constr constr; - visitor#tuple arguments + visitor.constr constr; + visitor.tuple arguments and print_some_app (visitor : xyz) {value=node; _} = let c_Some, arguments = node in - visitor#token c_Some "Some"; - visitor#tuple arguments + visitor.token c_Some "Some"; + visitor.tuple arguments and print_map_lookup (visitor : xyz) {value=node; _} = - let {value = lbracket, expr, rbracket; _} = node#index in - visitor#var node#map_name; - visitor#token node#selector "."; - visitor#token lbracket "["; - visitor#expr expr; - visitor#token rbracket "]" + let {value = lbracket, expr, rbracket; _} = node.index in + visitor.var node.map_name; + visitor.token node.selector "."; + visitor.token lbracket "["; + visitor.expr expr; + visitor.token rbracket "]" and print_par_expr (visitor : xyz) {value=node; _} = let lpar, expr, rpar = node in - visitor#token lpar "("; - visitor#expr expr; - visitor#token rpar ")" + visitor.token lpar "("; + visitor.expr expr; + visitor.token rpar ")" and print_pattern (visitor : xyz) {value=sequence; _} = - visitor#nsepseq "<:" visitor#core_pattern sequence + visitor.nsepseq "<:" visitor.core_pattern sequence and print_core_pattern (visitor : xyz) = function - PVar var -> visitor#var var -| PWild wild -> visitor#token wild "_" -| PInt i -> visitor#int i -| PBytes b -> visitor#bytes b -| PString s -> visitor#string s -| PUnit region -> visitor#token region "Unit" -| PFalse region -> visitor#token region "False" -| PTrue region -> visitor#token region "True" -| PNone region -> visitor#token region "None" -| PSome psome -> visitor#psome psome -| PList pattern -> visitor#list_pattern pattern -| PTuple ptuple -> visitor#ptuple ptuple + PVar var -> visitor.var var +| PWild wild -> visitor.token wild "_" +| PInt i -> visitor.int i +| PBytes b -> visitor.bytes b +| PString s -> visitor.string s +| PUnit region -> visitor.token region "Unit" +| PFalse region -> visitor.token region "False" +| PTrue region -> visitor.token region "True" +| PNone region -> visitor.token region "None" +| PSome psome -> visitor.psome psome +| PList pattern -> visitor.list_pattern pattern +| PTuple ptuple -> visitor.ptuple ptuple and print_psome (visitor : xyz) {value=node; _} = let c_Some, patterns = node in - visitor#token c_Some "Some"; - visitor#patterns patterns + visitor.token c_Some "Some"; + visitor.patterns patterns and print_patterns (visitor : xyz) {value=node; _} = let lpar, core_pattern, rpar = node in - visitor#token lpar "("; - visitor#core_pattern core_pattern; - visitor#token rpar ")" + visitor.token lpar "("; + visitor.core_pattern core_pattern; + visitor.token rpar ")" and print_list_pattern (visitor : xyz) = function - Sugar sugar -> visitor#sugar sugar -| Raw raw -> visitor#raw raw + Sugar sugar -> visitor.sugar sugar +| Raw raw -> visitor.raw raw and print_sugar (visitor : xyz) {value=node; _} = let lbracket, sequence, rbracket = node in - visitor#token lbracket "["; - visitor#sepseq "," visitor#core_pattern sequence; - visitor#token rbracket "]" + visitor.token lbracket "["; + visitor.sepseq "," visitor.core_pattern sequence; + visitor.token rbracket "]" and print_raw (visitor : xyz) {value=node; _} = let lpar, (core_pattern, cons, pattern), rpar = node in - visitor#token lpar "("; - visitor#core_pattern core_pattern; - visitor#token cons "<:"; - visitor#pattern pattern; - visitor#token rpar ")" + visitor.token lpar "("; + visitor.core_pattern core_pattern; + visitor.token cons "<:"; + visitor.pattern pattern; + visitor.token rpar ")" and print_ptuple (visitor : xyz) {value=node; _} = let lpar, sequence, rpar = node in - visitor#token lpar "("; - visitor#nsepseq "," visitor#core_pattern sequence; - visitor#token rpar ")" + visitor.token lpar "("; + visitor.nsepseq "," visitor.core_pattern sequence; + visitor.token rpar ")" -let rec visitor : unit -> xyz = fun () -> object - method nsepseq : 'a . string -> ('a -> unit) -> ('a * (Region.t * 'a) list) -> unit = print_nsepseq - method sepseq : 'a . string -> ('a -> unit) -> ('a * (Region.t * 'a) list) option -> unit = print_sepseq - method token = print_token (visitor ()) - method var = print_var (visitor ()) - method constr = print_constr (visitor ()) - method string = print_string (visitor ()) - method bytes = print_bytes (visitor ()) - method int = print_int (visitor ()) +let rec visitor () : xyz = { + nsepseq = print_nsepseq; (* : 'a . string -> ('a -> unit) -> ('a * (Region.t * 'a) list) -> unit *) + sepseq = print_sepseq; (* : 'a . string -> ('a -> unit) -> ('a * (Region.t * 'a) list) option -> unit *) + token = print_token (visitor ()); + var = print_var (visitor ()); + constr = print_constr (visitor ()); + string = print_string (visitor ()); + bytes = print_bytes (visitor ()); + int = print_int (visitor ()); - method parameter_decl = print_parameter_decl (visitor ()) - method storage_decl = print_storage_decl (visitor ()) - method operations_decl = print_operations_decl (visitor ()) - method type_decl = print_type_decl (visitor ()) - method type_expr = print_type_expr (visitor ()) - method cartesian = print_cartesian (visitor ()) - method variant = print_variant (visitor ()) - method sum_type = print_sum_type (visitor ()) - method record_type = print_record_type (visitor ()) - method type_app = print_type_app (visitor ()) - method par_type = print_par_type (visitor ()) - method field_decls = print_field_decls (visitor ()) - method field_decl = print_field_decl (visitor ()) - method type_tuple = print_type_tuple (visitor ()) - method lambda_decl = print_lambda_decl (visitor ()) - method fun_decl = print_fun_decl (visitor ()) - method proc_decl = print_proc_decl (visitor ()) - method parameters = print_parameters (visitor ()) - method param_decl = print_param_decl (visitor ()) - method var_kind = print_var_kind (visitor ()) - method block = print_block (visitor ()) - method value_decls = print_value_decls (visitor ()) - method var_decl = print_var_decl (visitor ()) - method instructions = print_instructions (visitor ()) - method instruction = print_instruction (visitor ()) - method single_instr = print_single_instr (visitor ()) - method conditional = print_conditional (visitor ()) - method match_instr = print_match_instr (visitor ()) - method cases = print_cases (visitor ()) - method case = print_case (visitor ()) - method asgnmnt_instr = print_asgnmnt_instr (visitor ()) - method loop = print_loop (visitor ()) - method while_loop = print_while_loop (visitor ()) - method for_loop = print_for_loop (visitor ()) - method for_int = print_for_int (visitor ()) - method down = print_down (visitor ()) - method step = print_step (visitor ()) - method for_collect = print_for_collect (visitor ()) - method bind_to = print_bind_to (visitor ()) - method expr = print_expr (visitor ()) - method tuple = print_tuple (visitor ()) - method list = print_list (visitor ()) - method empty_list = print_empty_list (visitor ()) - method set = print_set (visitor ()) - method empty_set = print_empty_set (visitor ()) - method none_expr = print_none_expr (visitor ()) - method fun_call = print_fun_call (visitor ()) - method constr_app = print_constr_app (visitor ()) - method some_app = print_some_app (visitor ()) - method map_lookup = print_map_lookup (visitor ()) - method par_expr = print_par_expr (visitor ()) - method pattern = print_pattern (visitor ()) - method core_pattern = print_core_pattern (visitor ()) - method psome = print_psome (visitor ()) - method patterns = print_patterns (visitor ()) - method list_pattern = print_list_pattern (visitor ()) - method sugar = print_sugar (visitor ()) - method raw = print_raw (visitor ()) - method ptuple = print_ptuple (visitor ()) - end + parameter_decl = print_parameter_decl (visitor ()); + storage_decl = print_storage_decl (visitor ()); + operations_decl = print_operations_decl (visitor ()); + type_decl = print_type_decl (visitor ()); + type_expr = print_type_expr (visitor ()); + cartesian = print_cartesian (visitor ()); + variant = print_variant (visitor ()); + sum_type = print_sum_type (visitor ()); + record_type = print_record_type (visitor ()); + type_app = print_type_app (visitor ()); + par_type = print_par_type (visitor ()); + field_decls = print_field_decls (visitor ()); + field_decl = print_field_decl (visitor ()); + type_tuple = print_type_tuple (visitor ()); + lambda_decl = print_lambda_decl (visitor ()); + fun_decl = print_fun_decl (visitor ()); + proc_decl = print_proc_decl (visitor ()); + parameters = print_parameters (visitor ()); + param_decl = print_param_decl (visitor ()); + var_kind = print_var_kind (visitor ()); + block = print_block (visitor ()); + value_decls = print_value_decls (visitor ()); + var_decl = print_var_decl (visitor ()); + instructions = print_instructions (visitor ()); + instruction = print_instruction (visitor ()); + single_instr = print_single_instr (visitor ()); + conditional = print_conditional (visitor ()); + match_instr = print_match_instr (visitor ()); + cases = print_cases (visitor ()); + case = print_case (visitor ()); + asgnmnt_instr = print_asgnmnt_instr (visitor ()); + loop = print_loop (visitor ()); + while_loop = print_while_loop (visitor ()); + for_loop = print_for_loop (visitor ()); + for_int = print_for_int (visitor ()); + down = print_down (visitor ()); + step = print_step (visitor ()); + for_collect = print_for_collect (visitor ()); + bind_to = print_bind_to (visitor ()); + expr = print_expr (visitor ()); + tuple = print_tuple (visitor ()); + list = print_list (visitor ()); + empty_list = print_empty_list (visitor ()); + set = print_set (visitor ()); + empty_set = print_empty_set (visitor ()); + none_expr = print_none_expr (visitor ()); + fun_call = print_fun_call (visitor ()); + constr_app = print_constr_app (visitor ()); + some_app = print_some_app (visitor ()); + map_lookup = print_map_lookup (visitor ()); + par_expr = print_par_expr (visitor ()); + pattern = print_pattern (visitor ()); + core_pattern = print_core_pattern (visitor ()); + psome = print_psome (visitor ()); + patterns = print_patterns (visitor ()); + list_pattern = print_list_pattern (visitor ()); + sugar = print_sugar (visitor ()); + raw = print_raw (visitor ()); + ptuple = print_ptuple (visitor ()) + } let print_tokens = print_tokens (visitor ()) diff --git a/AST.mli b/AST.mli index 3d6c2e361..fa998434a 100644 --- a/AST.mli +++ b/AST.mli @@ -1,5 +1,7 @@ (* Abstract Syntax Tree (AST) for Ligo *) +[@@@warning "-30"] + open Utils (* Regions @@ -123,7 +125,7 @@ type 'a braces = (lbrace * 'a * rbrace) reg (* The Abstract Syntax Tree *) -type t = < +type t = { types : type_decl list; parameter : parameter_decl; storage : storage_decl; @@ -131,7 +133,7 @@ type t = < lambdas : lambda_decl list; block : block reg; eof : eof -> +} and ast = t @@ -171,7 +173,7 @@ and lambda_decl = FunDecl of fun_decl reg | ProcDecl of proc_decl reg -and fun_decl = < +and fun_decl = { kwd_function : kwd_function; var : variable; param : parameters; @@ -181,15 +183,15 @@ and fun_decl = < body : block reg; kwd_with : kwd_with; return : expr -> +} -and proc_decl = < +and proc_decl = { kwd_procedure : kwd_procedure; var : variable; param : parameters; kwd_is : kwd_is; body : block reg -> +} and parameters = (param_decl, semi) nsepseq par @@ -199,23 +201,23 @@ and var_kind = Mutable of kwd_var | Const of kwd_const -and block = < +and block = { decls : value_decls; opening : kwd_begin; instr : instructions; close : kwd_end -> +} and value_decls = (var_decl reg, semi) sepseq reg -and var_decl = < +and var_decl = { kind : var_kind; var : variable; colon : colon; vtype : type_expr; setter : Region.t; (* "=" or ":=" *) init : expr -> +} and instructions = (instruction, semi) nsepseq reg @@ -231,22 +233,22 @@ and single_instr = | ProcCall of fun_call | Null of kwd_null -and conditional = < +and conditional = { kwd_if : kwd_if; test : expr; kwd_then : kwd_then; ifso : instruction; kwd_else : kwd_else; ifnot : instruction -> +} -and match_instr = < +and match_instr = { kwd_match : kwd_match; expr : expr; kwd_with : kwd_with; cases : cases; kwd_end : kwd_end -> +} and cases = (case, vbar) nsepseq reg @@ -264,7 +266,7 @@ and for_loop = ForInt of for_int reg | ForCollect of for_collect reg -and for_int = < +and for_int = { kwd_for : kwd_for; asgnmnt : asgnmnt_instr; down : kwd_down option; @@ -272,16 +274,16 @@ and for_int = < bound : expr; step : (kwd_step * expr) option; block : block reg -> +} -and for_collect = < +and for_collect = { kwd_for : kwd_for; var : variable; bind_to : (arrow * variable) option; kwd_in : kwd_in; expr : expr; block : block reg -> +} (* Expressions *) @@ -339,11 +341,11 @@ and arguments = tuple and constr_app = (constr * arguments) reg -and map_lookup = < +and map_lookup = { map_name : variable; selector : dot; index : expr brackets -> +} (* Patterns *) diff --git a/Parser.mly b/Parser.mly index f4b81b073..7a0478256 100644 --- a/Parser.mly +++ b/Parser.mly @@ -92,15 +92,15 @@ program: seq(lambda_decl) block EOF { - object - method types = $1 - method parameter = $2 - method storage = $3 - method operations = $4 - method lambdas = $5 - method block = $6 - method eof = $7 - end + { + types = $1; + parameter = $2; + storage = $3; + operations = $4; + lambdas = $5; + block = $6; + eof = $7; + } } parameter_decl: @@ -197,17 +197,17 @@ fun_decl: With expr { let region = cover $1 (expr_to_region $9) in let value = - object - method kwd_function = $1 - method var = $2 - method param = $3 - method colon = $4 - method ret_type = $5 - method kwd_is = $6 - method body = $7 - method kwd_with = $8 - method return = $9 - end + { + kwd_function = $1; + var = $2; + param = $3; + colon = $4; + ret_type = $5; + kwd_is = $6; + body = $7; + kwd_with = $8; + return = $9; + } in {region; value} } @@ -216,13 +216,13 @@ proc_decl: block { let region = cover $1 $5.region in let value = - object - method kwd_procedure = $1 - method var = $2 - method param = $3 - method kwd_is = $4 - method body = $5 - end + { + kwd_procedure = $1; + var = $2; + param = $3; + kwd_is = $4; + body = $5; + } in {region; value} } @@ -248,12 +248,12 @@ block: End { let region = cover $1.region $4 in let value = - object - method decls = $1 - method opening = $2 - method instr = $3 - method close = $4 - end + { + decls = $1; + opening = $2; + instr = $3; + close = $4; + } in {region; value} } @@ -267,27 +267,27 @@ var_decl: Var var COLON type_expr ASGNMNT expr { let region = cover $1 (expr_to_region $6) in let value = - object - method kind = Mutable $1 - method var = $2 - method colon = $3 - method vtype = $4 - method setter = $5 - method init = $6 - end + { + kind = Mutable $1; + var = $2; + colon = $3; + vtype = $4; + setter = $5; + init = $6; + } in {region; value} } | Const var COLON type_expr EQUAL expr { let region = cover $1 (expr_to_region $6) in let value = - object - method kind = Const $1 - method var = $2 - method colon = $3 - method vtype = $4 - method setter = $5 - method init = $6 - end + { + kind = Const $1; + var = $2; + colon = $3; + vtype = $4; + setter = $5; + init = $6; + } in {region; value} } @@ -316,14 +316,14 @@ conditional: If expr Then instruction Else instruction { let region = cover $1 (instr_to_region $6) in let value = - object - method kwd_if = $1 - method test = $2 - method kwd_then = $3 - method ifso = $4 - method kwd_else = $5 - method ifnot = $6 - end + { + kwd_if = $1; + test = $2; + kwd_then = $3; + ifso = $4; + kwd_else = $5; + ifnot = $6; + } in {region; value} } @@ -331,13 +331,13 @@ match_instr: Match expr With cases End { let region = cover $1 $5 in let value = - object - method kwd_match = $1 - method expr = $2 - method kwd_with = $3 - method cases = $4 - method kwd_end = $5 - end + { + kwd_match = $1; + expr = $2; + kwd_with = $3; + cases = $4; + kwd_end = $5; + } in {region; value} } @@ -373,29 +373,29 @@ for_loop: For asgnmnt Down? To expr option(step_clause) block { let region = cover $1 $7.region in let value = - object - method kwd_for = $1 - method asgnmnt = $2 - method down = $3 - method kwd_to = $4 - method bound = $5 - method step = $6 - method block = $7 - end + { + kwd_for = $1; + asgnmnt = $2; + down = $3; + kwd_to = $4; + bound = $5; + step = $6; + block = $7; + } in For (ForInt {region; value}) } | For var option(arrow_clause) In expr block { let region = cover $1 $6.region in let value = - object - method kwd_for = $1 - method var = $2 - method bind_to = $3 - method kwd_in = $4 - method expr = $5 - method block = $6 - end + { + kwd_for = $1; + var = $2; + bind_to = $3; + kwd_in = $4; + expr = $5; + block = $6; + } in For (ForCollect {region; value}) } @@ -557,11 +557,11 @@ core_expr: | map_name DOT brackets(expr) { let region = cover $1.region $3.region in let value = - object - method map_name = $1 - method selector = $2 - method index = $3 - end + { + map_name = $1; + selector = $2; + index = $3; + } in MapLookUp {region; value} } diff --git a/typecheck.ml b/typecheck.ml index 2d7565907..99037d0bb 100644 --- a/typecheck.ml +++ b/typecheck.ml @@ -1,32 +1,230 @@ -open AST -open Region +module I = AST (* In *) module SMap = Map.Make(String) +module O = struct + open AST (* TODO: for now, should disappear *) + + type t = ast + + and type_expr = + Prod of cartesian + | Sum of (variant, vbar) Utils.nsepseq + | Record of record_type + | TypeApp of (type_name * type_tuple) + | ParType of type_expr par + | TAlias of variable + | Function of (type_expr list) * type_expr + | Mutable of type_expr + | Unit + | TODO of string + + and te = type_expr list SMap.t + + and ve = type_expr list SMap.t + + and vte = ve * te + + and ast = { + lambdas : lambda_decl list; + block : block + } + + and lambda_decl = + FunDecl of fun_decl + | ProcDecl of proc_decl + + and fun_decl = { + kwd_function : kwd_function; + var : variable; + param : parameters; + colon : colon; + ret_type : type_expr; + kwd_is : kwd_is; + body : block; + kwd_with : kwd_with; + return : checked_expr + } + + and proc_decl = { + kwd_procedure : kwd_procedure; + var : variable; + param : parameters; + kwd_is : kwd_is; + body : block + } + + and block = { + decls : value_decls; + opening : kwd_begin; + instr : instructions; + close : kwd_end + } + + and value_decls = var_decl list + + and var_decl = { + kind : var_kind; + var : variable; + colon : colon; + vtype : type_expr; + setter : Region.t; (* "=" or ":=" *) + init : checked_expr + } + + and checked_expr = {ty:type_expr;expr:expr} +end [@warning "-30"] + +open O +open AST +open Region + +let mk_checked_expr ~ty ~expr = {ty;expr} +let mk_proc_decl ~kwd_procedure ~var ~param ~kwd_is ~body = + O.{kwd_procedure; var; param; kwd_is; body} +let mk_ast ~lambdas ~block = {lambdas;block} +let mk_fun_decl ~kwd_function ~var ~param ~colon ~ret_type ~kwd_is ~body ~kwd_with ~return = + O.{kwd_function; var; param; colon; ret_type; kwd_is; body; kwd_with; return} + (* open Sanity: *) -let (|>) v f = f v -let (@@) f v = f v +let (|>) v f = f v (* pipe f to v *) +let (@@) f v = f v (* apply f on v *) +let (@.) f g x = f (g x) (* compose *) let map f l = List.rev (List.rev_map f l) +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 type_decl_to_tenv td = - td - |> List.map (fun (_, name, _, type_expr) -> (name, type_expr)) - |> List.to_seq |> SMap.of_seq +let unreg : 'a reg -> 'a = fun {value; _} -> value +let unpar : 'a par -> 'a = (fun (_left_par, x, _right_par) -> x) @. unreg +let nsepseq_to_list : ('a,'sep) Utils.nsepseq -> 'a list = + fun (first, rest) -> first :: (map snd rest) +let sepseq_to_list : ('a,'sep) Utils.sepseq -> 'a list = + function + None -> [] + | Some nsepseq -> nsepseq_to_list nsepseq -let shadow name typ env = +let rec xty : I.type_expr -> O.type_expr = + function + I.Prod x -> O.Prod x + | I.Sum x -> O.Sum (unreg x) + | I.Record x -> O.Record x + | I.TypeApp x -> O.TypeApp (unreg x) + | I.ParType {region;value=(l,x,r)} -> O.ParType {region;value=(l, xty x, r)} + | I.TAlias x -> O.TAlias x + +let shadow (name : string) (typ : O.type_expr) (env : O.type_expr list SMap.t) + : O.type_expr list SMap.t = SMap.update name (function None -> Some [typ] | Some tl -> Some (typ :: tl)) env -let shadow_list name_typ_list env = +let shadow_list (name_typ_list : (string * O.type_expr) list) (env : O.type_expr list SMap.t) + : O.type_expr list SMap.t = List.fold_left (fun acc (name, typ) -> shadow name typ acc) env name_typ_list -let tc ast = +let type_decls_to_tenv (td : I.type_decl list) (te : te) : O.te = + td + |> List.map unreg + |> List.map (fun (_, name, _, type_expr) -> (unreg name, xty type_expr)) + |> fun up -> shadow_list up te + +let var_kind_to_ty : var_kind -> I.type_expr -> O.type_expr = + fun var_kind ty -> + match var_kind with + Mutable _ -> O.Mutable (xty ty) + | Const _ -> xty ty + +let params_to_xty params ret_type = + unpar params + |> nsepseq_to_list + |> map (fun {value=(var_kind, _variable, _colon, type_expr);_} -> var_kind_to_ty var_kind type_expr) + |> fun param_types -> O.Function (param_types, ret_type) + +let type_equal t1 t2 = match t1,t2 with + | O.Prod _x, O.Prod _y -> true (* TODO *) + | O.Sum _x, O.Sum _y -> true (* TODO *) + | _ -> false + +exception TypeError of string + +let check_type expr expected_type = + if type_equal expr.ty expected_type then expr + else raise (TypeError "oops") + +let tc_expr (_te,_ve) expr = mk_checked_expr ~ty:(TODO "all expressions") ~expr (* TODO *) + +let tc_var_decl : vte -> I.var_decl -> vte * O.var_decl = + fun (ve,te) var_decl -> + let vtype = (xty var_decl.vtype) in + let init = check_type (tc_expr (te,ve) var_decl.init) vtype in + let ve = shadow (unreg var_decl.var) vtype ve in + (ve,te), { + kind = var_decl.kind; + var = var_decl.var; + colon = var_decl.colon; + vtype; + setter = var_decl.setter; + init} + +let tc_var_decls (ve,te) var_decls = fold_map tc_var_decl (ve,te) var_decls + +let tc_block (te, ve : vte) (block : I.block) : vte * O.block = + let decls,opening,instr,close = block.decls, block.opening, block.instr, block.close in + let (ve,te), decls = tc_var_decls (ve,te) (decls |> unreg |> sepseq_to_list |> map unreg) in + (ve,te), O.{decls;opening;instr;close} (* TODO *) + +let tc_proc_decl : vte -> I.proc_decl -> O.proc_decl = + fun vte proc_decl -> + let _vte', block' = tc_block vte (unreg proc_decl.body) + in mk_proc_decl + ~kwd_procedure: proc_decl.kwd_procedure + ~kwd_is: proc_decl.kwd_is + ~var: proc_decl.var + ~param: proc_decl.param + ~body: block' + +let tc_fun_decl : vte -> I.fun_decl -> O.fun_decl = + fun vte fun_decl -> + let vte', block' = tc_block vte (unreg fun_decl.body) in + let return' = tc_expr vte' fun_decl.return in + let checked_return' = check_type return' (xty fun_decl.ret_type) + in mk_fun_decl + ~kwd_function: fun_decl.kwd_function + ~colon: fun_decl.colon + ~kwd_is: fun_decl.kwd_is + ~kwd_with: fun_decl.kwd_with + ~var: fun_decl.var + ~param: fun_decl.param + ~ret_type: (xty fun_decl.ret_type) + ~body: block' + ~return: checked_return' + +let ve_lambda_decl : vte -> I.lambda_decl -> ve = + fun (ve,_te) -> + function + FunDecl {value;_} -> shadow value.var.value (params_to_xty value.param (xty value.ret_type)) ve + | ProcDecl {value;_} -> shadow value.var.value (params_to_xty value.param Unit) ve + +let tc_lambda_decl (ve, te : vte) (whole : I.lambda_decl) : vte * O.lambda_decl = + match whole with + FunDecl {value;_} -> ((ve_lambda_decl (ve, te) whole), te), O.FunDecl (tc_fun_decl (ve, te) value) + | ProcDecl {value;_} -> ((ve_lambda_decl (ve, te) whole), te), O.ProcDecl (tc_proc_decl (ve, te) value) + +let tc_ast (ast : I.ast) : O.ast = (* te is the type environment, ve is the variable environment *) - let te = type_decl_to_tenv ast#types in + let te = + SMap.empty + |> type_decls_to_tenv ast.types in let ve = SMap.empty - |> (match ast#parameter.value with (_,name,_,ty) -> shadow name ty) - |> shadow "storage" (snd ast#storage.value) - |> shadow "operations" (snd ast#operations.value) - (* |> shadow_list @@ map (function FunDecl {value} -> value.var.value, ) lambdas *) + |> (match ast.parameter.value with (_,name,_,ty) -> shadow (unreg name) @@ xty ty) + |> shadow "storage" @@ xty (snd ast.storage.value) + |> shadow "operations" @@ xty (snd ast.operations.value) in - te, ve + let (ve',te'), lambdas = fold_map tc_lambda_decl (ve, te) ast.lambdas in + let (ve'', te''), block = tc_block (ve', te') (unreg ast.block) in + let _ve'' = ve'' in (* not needed anymore *) + let _te'' = te'' in (* not needed anymore *) + mk_ast ~lambdas ~block