diff --git a/src/stages/ast_typed/combinators.ml b/src/stages/ast_typed/combinators.ml index af742b334..5700cb0f5 100644 --- a/src/stages/ast_typed/combinators.ml +++ b/src/stages/ast_typed/combinators.ml @@ -5,7 +5,6 @@ let make_t type_value' simplified = { type_value' ; simplified } let make_a_e ?(location = Location.generated) expression type_annotation environment = { expression ; type_annotation ; - dummy_field = () ; environment ; location ; } diff --git a/src/stages/ast_typed/types.ml b/src/stages/ast_typed/types.ml index b60632a0d..3ecf979d5 100644 --- a/src/stages/ast_typed/types.ml +++ b/src/stages/ast_typed/types.ml @@ -38,7 +38,6 @@ and annotated_expression = { type_annotation : tv ; environment : full_environment ; location : Location.t ; - dummy_field : unit ; } and named_expression = { diff --git a/src/stages/typesystem/misc.ml b/src/stages/typesystem/misc.ml index 88b06e3fd..ee83bfd78 100644 --- a/src/stages/typesystem/misc.ml +++ b/src/stages/typesystem/misc.ml @@ -7,16 +7,137 @@ module Substitution = struct module Pattern = struct open Trace + module T = Ast_typed + module TSMap = Trace.TMap(String) - let rec declaration ~(d : Ast_typed.declaration Location.wrap) ~v ~expr : Ast_typed.declaration Location.wrap result = - Trace.bind_map_location (function - Ast_typed.Declaration_constant (e, (env1, env2)) -> - let _ = v, expr, failwith "TODO: subst" in - ok @@ Ast_typed.Declaration_constant (e, (env1, env2)) - ) d + type 'a w = 'a -> 'a result + + let todo = failwith "TODO" + + let rec rec_yes = true + and s_full_environment ~v ~expr : T.full_environment w = fun (a , b) -> + let%bind a = todo ~v ~expr a in + let%bind b = bind_map_list (todo ~v ~expr) b in + ok (a , b) + + and s_variable ~v ~expr : T.name w = fun var -> todo + + and s_type_variable ~v ~expr : T.name w = fun tvar -> todo + + and s_type_value ~v ~expr : T.type_value w = fun { type_value'; simplified } -> todo + + and s_expression ~v ~expr : T.expression w = function + | T.E_literal x -> + let%bind x = s_literal ~v ~expr x in + ok @@ T.E_literal x + | T.E_constant (var, vals) -> + let%bind var = s_variable ~v ~expr var in + let%bind vals = bind_map_list (s_annotated_expression ~v ~expr) vals in + ok @@ T.E_constant (var, vals) + | T.E_variable tv -> + let%bind tv = s_variable ~v ~expr tv in + ok @@ T.E_variable tv + | T.E_application (val1 , val2) -> + let%bind val1 = s_annotated_expression ~v ~expr val1 in + let%bind val2 = s_annotated_expression ~v ~expr val2 in + ok @@ T.E_application (val1 , val2) + | T.E_lambda { binder; body } -> + let%bind binder = s_variable ~v ~expr binder in + let%bind body = s_annotated_expression ~v ~expr body in + ok @@ T.E_lambda { binder; body } + | T.E_let_in { binder; rhs; result } -> + let%bind binder = s_variable ~v ~expr binder in + let%bind rhs = s_annotated_expression ~v ~expr rhs in + let%bind result = s_annotated_expression ~v ~expr result in + ok @@ T.E_let_in { binder; rhs; result } + | T.E_tuple vals -> + let%bind vals = bind_map_list (s_annotated_expression ~v ~expr) vals in + ok @@ T.E_tuple vals + | T.E_tuple_accessor (val_, i) -> + let%bind val_ = s_annotated_expression ~v ~expr val_ in + let i = i in + ok @@ T.E_tuple_accessor (val_, i) + | T.E_constructor (tvar, val_) -> + let%bind tvar = s_type_variable ~v ~expr tvar in + let%bind val_ = s_annotated_expression ~v ~expr val_ in + ok @@ T.E_constructor (tvar, val_) + | T.E_record aemap -> + let%bind aemap = TSMap.bind_map_Map (fun ~k:key ~v:val_ -> + let key = s_type_variable ~v ~expr key in + let val_ = s_annotated_expression ~v ~expr val_ in + ok @@ (key , val_)) aemap in + ok @@ T.E_record aemap + | T.E_record_accessor (val_, tvar) -> + let%bind val_ = s_annotated_expression ~v ~expr val_ in + let%bind tvar = s_type_variable ~v ~expr tvar in + ok @@ T.E_record_accessor (val_, tvar) + | T.E_map val_val_list -> + let%bind val_val_list = bind_map_list (fun (val1 , val2) -> + let%bind val1 = s_annotated_expression ~v ~expr val1 in + let%bind val2 = s_annotated_expression ~v ~expr val2 in + (val1 , val2) + ) val_val_list in + ok @@ T.E_map val_val_list + | T.E_big_map val_val_list -> + let%bind val_val_list = bind_map_list (fun (val1 , val2) -> + let%bind val1 = s_annotated_expression ~v ~expr val1 in + let%bind val2 = s_annotated_expression ~v ~expr val2 in + (val1 , val2) + ) val_val_list in + ok @@ T.E_big_map val_val_list + | T.E_list vals -> + let%bind vals = bind_map_list s_annotated_expression ~v ~expr vals in + ok @@ T.E_list vals + | T.E_set vals -> + let%bind vals = bind_map_list s_annotated_expression ~v ~expr vals in + ok @@ T.E_set vals + | T.E_look_up (val1, val2) -> + let%bind val1 = s_annotated_expression ~v ~expr val1 in + let%bind val2 = s_annotated_expression ~v ~expr val2 in + ok @@ T.E_look_up (val1 , val2) + | T.E_matching (val_ , matching) -> + let%bind val_ = s_annotated_expression ~v ~expr val_ in + let%bind matching = s_matching matching in + ok @@ T.E_matching (val_ , matching) + | T.E_sequence (val1, val2) -> + let%bind val1 = s_annotated_expression ~v ~expr val1 in + let%bind val2 = s_annotated_expression ~v ~expr val2 in + ok @@ T.E_sequence (val1 , val2) + | T.E_loop (val1, val2) -> + let%bind val1 = s_annotated_expression ~v ~expr val1 in + let%bind val2 = s_annotated_expression ~v ~expr val2 in + ok @@ T.E_loop (val1 , val2) + | T.E_assign (named_tval, access_path, val_) -> + let%bind named_tval = s_named_type_value ~v ~expr named_tval in + let%bind access_path = s_access_path ~v ~expr access_path in + let%bind val_ = s_annotated_expression ~v ~expr val_ in + ok @@ T.E_assign (named_tval, access_path, val_) + + and s_annotated_expression ~v ~expr : T.annotated_expression w = fun { expression; type_annotation; environment; location } -> + let%bind expression = s_expression ~v ~expr expression in + let%bind type_annotation = s_type_value ~v ~expr type_annotation in + let%bind environment = s_full_environment ~v ~expr environment in + let location = location in + ok T.{ expression; type_annotation; environment; location } + + and s_named_expression ~v ~expr : T.named_expression w = fun { name; annotated_expression } -> + let name = name in + let annotated_expression = s_annotated_expression annotated_expression in + ok T.{ name; annotated_expression } + + and s_declaration ~v ~expr : T.declaration w = + function + Ast_typed.Declaration_constant (e, (env1, env2)) -> + let e = s_named_expression ~v ~expr e in + let env1 = s_full_environment ~v ~expr env1 in + let env2 = s_full_environment ~v ~expr env2 in + ok @@ Ast_typed.Declaration_constant (e, (env1, env2)) + + and s_declaration_wrap ~v ~expr : T.declaration Location.wrap w = fun d -> + Trace.bind_map_location (s_declaration ~v ~expr) d and program ~(p : Ast_typed.program) ~v ~expr : Ast_typed.program Trace.result = - Trace.bind_map_list (fun d -> declaration ~d ~v ~expr) p + Trace.bind_map_list (s_declaration_wrap ~v ~expr) p (* Computes `P[v := expr]`. diff --git a/vendors/ligo-utils/simple-utils/trace.ml b/vendors/ligo-utils/simple-utils/trace.ml index e8f3b43eb..46981eae5 100644 --- a/vendors/ligo-utils/simple-utils/trace.ml +++ b/vendors/ligo-utils/simple-utils/trace.ml @@ -600,9 +600,20 @@ module TMap(X : Map.OrderedType) = struct f ~x ~k ~v in MX.fold aux map (ok init) + + let bind_map_Map f map = + let aux k v map' = + map' >>? fun map' -> + f ~k ~v >>? fun v' -> + ok @@ MX.update k (function + | None -> Some v' + | Some _ -> failwith "key collision, shouldn't happen in bind_map_Map") + map' + in + MX.fold aux map (ok MX.empty) end -let bind_fold_pair f init (a,b) = +let bind_fold_pair f init (a,b) = let aux x y = x >>? fun x -> f x y