From 614970d2d759d763a492246e97ab455fd0b058ca Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Suzanne=20Dup=C3=A9ron?= Date: Sat, 9 Nov 2019 02:45:43 +0100 Subject: [PATCH] Implemented some missing cases of the subst. First kinda actual typer test passes! --- src/passes/4-typer-new/solver.ml | 48 +++++++++--------- src/passes/4-typer-new/typer.ml | 29 +++++++++++ src/stages/ast_typed/misc.ml | 1 + src/stages/common/ast_common.ml | 1 + src/stages/common/misc.ml | 85 ++++++++++++++++++++++++++++++++ src/stages/typesystem/core.ml | 32 ++++++++++++ src/stages/typesystem/misc.ml | 38 +++++++++----- 7 files changed, 200 insertions(+), 34 deletions(-) create mode 100644 src/stages/common/misc.ml diff --git a/src/passes/4-typer-new/solver.ml b/src/passes/4-typer-new/solver.ml index e5f12b144..2adac9659 100644 --- a/src/passes/4-typer-new/solver.ml +++ b/src/passes/4-typer-new/solver.ml @@ -729,94 +729,98 @@ let compare_simple_c_constant = function | C_arrow -> (function (* N/A -> 1 *) | C_arrow -> 0 - | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) + | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_option -> (function | C_arrow -> 1 | C_option -> 0 - | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) + | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_tuple -> (function | C_arrow | C_option -> 1 | C_tuple -> 0 - | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) + | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_record -> (function | C_arrow | C_option | C_tuple -> 1 | C_record -> 0 - | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) + | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_variant -> (function | C_arrow | C_option | C_tuple | C_record -> 1 | C_variant -> 0 - | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) + | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_map -> (function | C_arrow | C_option | C_tuple | C_record | C_variant -> 1 | C_map -> 0 - | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) + | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_big_map -> (function | C_arrow | C_option | C_tuple | C_record | C_variant | C_map -> 1 | C_big_map -> 0 - | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) + | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_list -> (function | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map -> 1 | C_list -> 0 - | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) + | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_set -> (function | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list -> 1 | C_set -> 0 - | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) + | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_unit -> (function | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set -> 1 | C_unit -> 0 - | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) + | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_bool -> (function | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit -> 1 | C_bool -> 0 - | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) + | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_string -> (function | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool -> 1 | C_string -> 0 - | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) + | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_nat -> (function | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string -> 1 | C_nat -> 0 - | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) + | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_mutez -> (function | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat -> 1 | C_mutez -> 0 - | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) + | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_timestamp -> (function | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez -> 1 | C_timestamp -> 0 - | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) + | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_int -> (function | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp -> 1 | C_int -> 0 - | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) + | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_address -> (function | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int -> 1 | C_address -> 0 - | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) + | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_bytes -> (function | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address -> 1 | C_bytes -> 0 - | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) + | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_key_hash -> (function | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes -> 1 | C_key_hash -> 0 - | C_key | C_signature | C_operation | C_contract -> -1) + | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_key -> (function | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash -> 1 | C_key -> 0 - | C_signature | C_operation | C_contract -> -1) + | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_signature -> (function | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key -> 1 | C_signature -> 0 - | C_operation | C_contract -> -1) + | C_operation | C_contract | C_chain_id -> -1) | C_operation -> (function | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature -> 1 | C_operation -> 0 - | C_contract -> -1) + | C_contract | C_chain_id -> -1) | C_contract -> (function | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation -> 1 | C_contract -> 0 + | C_chain_id -> -1) + | C_chain_id -> (function + | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> 1 + | C_chain_id -> 0 (* N/A -> -1 *) ) let rec compare_typeclass a b = compare_list (compare_list compare_type_value) a b diff --git a/src/passes/4-typer-new/typer.ml b/src/passes/4-typer-new/typer.ml index 5d1d68465..537a4c485 100644 --- a/src/passes/4-typer-new/typer.ml +++ b/src/passes/4-typer-new/typer.ml @@ -956,12 +956,41 @@ let type_program_returns_state (p:I.program) : (environment * Solver.state * O.p (* module TSMap = TMap(Solver.TypeVariable) *) +(* let c_tag_to_string : Solver.Core.constant_tag -> string = function + * | Solver.Core.C_arrow -> "arrow" + * | Solver.Core.C_option -> "option" + * | Solver.Core.C_tuple -> "tuple" + * | Solver.Core.C_record -> failwith "record" + * | Solver.Core.C_variant -> failwith "variant" + * | Solver.Core.C_map -> "map" + * | Solver.Core.C_big_map -> "big" + * | Solver.Core.C_list -> "list" + * | Solver.Core.C_set -> "set" + * | Solver.Core.C_unit -> "unit" + * | Solver.Core.C_bool -> "bool" + * | Solver.Core.C_string -> "string" + * | Solver.Core.C_nat -> "nat" + * | Solver.Core.C_mutez -> "mutez" + * | Solver.Core.C_timestamp -> "timestamp" + * | Solver.Core.C_int -> "int" + * | Solver.Core.C_address -> "address" + * | Solver.Core.C_bytes -> "bytes" + * | Solver.Core.C_key_hash -> "key_hash" + * | Solver.Core.C_key -> "key" + * | Solver.Core.C_signature -> "signature" + * | Solver.Core.C_operation -> "operation" + * | Solver.Core.C_contract -> "contract" + * | Solver.Core.C_chain_id -> "chain_id" *) + let type_program (p : I.program) : (O.program * Solver.state) result = let%bind (env, state, program) = type_program_returns_state p in let subst_all = let assignments = state.structured_dbs.assignments in let aux (v : I.type_variable) (expr : Solver.c_constructor_simpl) (p:O.program result) = let%bind p = p in + let Solver.{ tv ; c_tag ; tv_list } = expr in + let () = ignore tv (* I think there is an issue where the tv is stored twice (as a key and in the element itself) *) in + let%bind (expr : O.type_value') = Typesystem.Core.type_expression'_of_simple_c_constant (c_tag , (List.map (fun s -> O.{ type_value' = T_variable s ; simplified = None }) tv_list)) in Typesystem.Misc.Substitution.Pattern.program ~p ~v ~expr in (* let p = TSMap.bind_fold_Map aux program assignments in *) (* TODO: Module magic: this does not work *) let p = Solver.TypeVariableMap.fold aux assignments (ok program) in diff --git a/src/stages/ast_typed/misc.ml b/src/stages/ast_typed/misc.ml index 6ece0d8ab..43d0c8792 100644 --- a/src/stages/ast_typed/misc.ml +++ b/src/stages/ast_typed/misc.ml @@ -1,5 +1,6 @@ open Trace open Types +include Stage_common.Misc module Errors = struct let different_kinds a b () = diff --git a/src/stages/common/ast_common.ml b/src/stages/common/ast_common.ml index 302205f4b..b570d3941 100644 --- a/src/stages/common/ast_common.ml +++ b/src/stages/common/ast_common.ml @@ -1,2 +1,3 @@ module Types = Types module PP = PP +module Misc = Misc diff --git a/src/stages/common/misc.ml b/src/stages/common/misc.ml new file mode 100644 index 000000000..7f38acf62 --- /dev/null +++ b/src/stages/common/misc.ml @@ -0,0 +1,85 @@ +open Types +open Trace + +let map_type_operator f = function + TC_contract x -> TC_contract (f x) + | TC_option x -> TC_option (f x) + | TC_list x -> TC_list (f x) + | TC_set x -> TC_set (f x) + | TC_map (x , y) -> TC_map (f x , f y) + | TC_big_map (x , y)-> TC_big_map (f x , f y) + +let bind_map_type_operator f = function + TC_contract x -> let%bind x = f x in ok @@ TC_contract x + | TC_option x -> let%bind x = f x in ok @@ TC_option x + | TC_list x -> let%bind x = f x in ok @@ TC_list x + | TC_set x -> let%bind x = f x in ok @@ TC_set x + | TC_map (x , y) -> let%bind x = f x in let%bind y = f y in ok @@ TC_map (x , y) + | TC_big_map (x , y)-> let%bind x = f x in let%bind y = f y in ok @@ TC_big_map (x , y) + +let type_operator_name = function + TC_contract _ -> "TC_contract" + | TC_option _ -> "TC_option" + | TC_list _ -> "TC_list" + | TC_set _ -> "TC_set" + | TC_map _ -> "TC_map" + | TC_big_map _ -> "TC_big_map" + +let type_expression'_of_string = function + | "TC_contract" , [x] -> ok @@ T_operator(TC_contract x) + | "TC_option" , [x] -> ok @@ T_operator(TC_option x) + | "TC_list" , [x] -> ok @@ T_operator(TC_list x) + | "TC_set" , [x] -> ok @@ T_operator(TC_set x) + | "TC_map" , [x ; y] -> ok @@ T_operator(TC_map (x , y)) + | "TC_big_map" , [x ; y] -> ok @@ T_operator(TC_big_map (x, y)) + | ("TC_contract" | "TC_option" | "TC_list" | "TC_set" | "TC_map" | "TC_big_map"), _ -> + failwith "internal error: wrong number of arguments for type operator" + + | "TC_unit" , [] -> ok @@ T_constant(TC_unit) + | "TC_string" , [] -> ok @@ T_constant(TC_string) + | "TC_bytes" , [] -> ok @@ T_constant(TC_bytes) + | "TC_nat" , [] -> ok @@ T_constant(TC_nat) + | "TC_int" , [] -> ok @@ T_constant(TC_int) + | "TC_mutez" , [] -> ok @@ T_constant(TC_mutez) + | "TC_bool" , [] -> ok @@ T_constant(TC_bool) + | "TC_operation" , [] -> ok @@ T_constant(TC_operation) + | "TC_address" , [] -> ok @@ T_constant(TC_address) + | "TC_key" , [] -> ok @@ T_constant(TC_key) + | "TC_key_hash" , [] -> ok @@ T_constant(TC_key_hash) + | "TC_chain_id" , [] -> ok @@ T_constant(TC_chain_id) + | "TC_signature" , [] -> ok @@ T_constant(TC_signature) + | "TC_timestamp" , [] -> ok @@ T_constant(TC_timestamp) + | _, [] -> + failwith "internal error: wrong number of arguments for type constant" + | _ -> + failwith "internal error: unknown type operator" + +let string_of_type_operator = function + | TC_contract x -> "TC_contract" , [x] + | TC_option x -> "TC_option" , [x] + | TC_list x -> "TC_list" , [x] + | TC_set x -> "TC_set" , [x] + | TC_map (x , y) -> "TC_map" , [x ; y] + | TC_big_map (x , y) -> "TC_big_map" , [x ; y] + +let string_of_type_constant = function + | TC_unit -> "TC_unit", [] + | TC_string -> "TC_string", [] + | TC_bytes -> "TC_bytes", [] + | TC_nat -> "TC_nat", [] + | TC_int -> "TC_int", [] + | TC_mutez -> "TC_mutez", [] + | TC_bool -> "TC_bool", [] + | TC_operation -> "TC_operation", [] + | TC_address -> "TC_address", [] + | TC_key -> "TC_key", [] + | TC_key_hash -> "TC_key_hash", [] + | TC_chain_id -> "TC_chain_id", [] + | TC_signature -> "TC_signature", [] + | TC_timestamp -> "TC_timestamp", [] + +let string_of_type_expression' = function + | T_operator o -> string_of_type_operator o + | T_constant c -> string_of_type_constant c + | T_tuple _|T_sum _|T_record _|T_arrow (_, _)|T_variable _ -> + failwith "not a type operator or constant" diff --git a/src/stages/typesystem/core.ml b/src/stages/typesystem/core.ml index 30a3a5fa5..c21888908 100644 --- a/src/stages/typesystem/core.ml +++ b/src/stages/typesystem/core.ml @@ -31,6 +31,7 @@ type constant_tag = | C_signature (* * *) | C_operation (* * *) | C_contract (* * -> * *) + | C_chain_id (* * *) type accessor = | L_int of int @@ -67,3 +68,34 @@ and type_constraint = (* is the first list in case on of the type of the type class as a kind *->*->* ? *) and typeclass = type_value list list + +open Trace +let type_expression'_of_simple_c_constant = function + | C_contract , [x] -> ok @@ T_operator(TC_contract x) + | C_option , [x] -> ok @@ T_operator(TC_option x) + | C_list , [x] -> ok @@ T_operator(TC_list x) + | C_set , [x] -> ok @@ T_operator(TC_set x) + | C_map , [x ; y] -> ok @@ T_operator(TC_map (x , y)) + | C_big_map , [x ; y] -> ok @@ T_operator(TC_big_map (x, y)) + | (C_contract | C_option | C_list | C_set | C_map | C_big_map), _ -> + failwith "internal error: wrong number of arguments for type operator" + + | C_unit , [] -> ok @@ T_constant(TC_unit) + | C_string , [] -> ok @@ T_constant(TC_string) + | C_bytes , [] -> ok @@ T_constant(TC_bytes) + | C_nat , [] -> ok @@ T_constant(TC_nat) + | C_int , [] -> ok @@ T_constant(TC_int) + | C_mutez , [] -> ok @@ T_constant(TC_mutez) + | C_bool , [] -> ok @@ T_constant(TC_bool) + | C_operation , [] -> ok @@ T_constant(TC_operation) + | C_address , [] -> ok @@ T_constant(TC_address) + | C_key , [] -> ok @@ T_constant(TC_key) + | C_key_hash , [] -> ok @@ T_constant(TC_key_hash) + | C_chain_id , [] -> ok @@ T_constant(TC_chain_id) + | C_signature , [] -> ok @@ T_constant(TC_signature) + | C_timestamp , [] -> ok @@ T_constant(TC_timestamp) + | _ , [] -> + failwith "internal error: wrong number of arguments for type constant" + | _ , _ -> + failwith "internal error: unknown type operator" + diff --git a/src/stages/typesystem/misc.ml b/src/stages/typesystem/misc.ml index fdcaae910..b95c603fc 100644 --- a/src/stages/typesystem/misc.ml +++ b/src/stages/typesystem/misc.ml @@ -78,23 +78,37 @@ module Substitution = struct | T.T_constant (type_name) -> let%bind type_name = s_type_name_constant ~v ~expr type_name in ok @@ T.T_constant (type_name) - | T.T_variable _ -> failwith "TODO: T_variable" - | T.T_operator _ -> failwith "TODO: T_operator" + | T.T_variable variable -> + if Var.equal variable v + then ok @@ expr + else ok @@ T.T_variable variable + | T.T_operator (type_name_and_args) -> + let bind_map_type_operator = Stage_common.Misc.bind_map_type_operator in (* TODO: write T.Misc.bind_map_type_operator, but it doesn't work *) + let%bind type_name_and_args = bind_map_type_operator (s_type_value ~v ~expr) type_name_and_args in + ok @@ T.T_operator type_name_and_args | T.T_arrow _ -> let _TODO = (v, expr) in failwith "TODO: T_function" - and s_type_expression ~v ~expr : Ast_simplified.type_expression w = fun {type_expression'} -> + and s_type_expression' ~v ~expr : _ Ast_simplified.type_expression' w = fun type_expression' -> match type_expression' with - | Ast_simplified.T_tuple _ -> failwith "TODO: subst: unimplemented case s_type_expression" - | Ast_simplified.T_sum _ -> failwith "TODO: subst: unimplemented case s_type_expression" - | Ast_simplified.T_record _ -> failwith "TODO: subst: unimplemented case s_type_expression" - | Ast_simplified.T_arrow (_, _) -> failwith "TODO: subst: unimplemented case s_type_expression" - | Ast_simplified.T_variable _ -> failwith "TODO: subst: unimplemented case s_type_expression" - | Ast_simplified.T_operator _ -> failwith "TODO: subst: unimplemented case s_type_expression" - | Ast_simplified.T_constant _ -> - let _TODO = (v, expr) in - failwith "TODO: subst: unimplemented case s_type_expression" + | Ast_simplified.T_tuple _ -> failwith "TODO: subst: unimplemented case s_type_expression tuple" + | Ast_simplified.T_sum _ -> failwith "TODO: subst: unimplemented case s_type_expression sum" + | Ast_simplified.T_record _ -> failwith "TODO: subst: unimplemented case s_type_expression record" + | Ast_simplified.T_arrow (_, _) -> failwith "TODO: subst: unimplemented case s_type_expression arrow" + | Ast_simplified.T_variable _ -> failwith "TODO: subst: unimplemented case s_type_expression variable" + | Ast_simplified.T_operator op -> + let%bind op = + Stage_common.Misc.bind_map_type_operator (* TODO: write Ast_simplified.Misc.type_operator_name *) + (s_type_expression ~v ~expr) + op in + ok @@ Ast_simplified.T_operator op + | Ast_simplified.T_constant constant -> + ok @@ Ast_simplified.T_constant constant + + and s_type_expression ~v ~expr : Ast_simplified.type_expression w = fun {type_expression'} -> + let%bind type_expression' = s_type_expression' ~v ~expr type_expression' in + ok @@ Ast_simplified.{type_expression'} and s_type_value ~v ~expr : T.type_value w = fun { type_value'; simplified } -> let%bind type_value' = s_type_value' ~v ~expr type_value' in