From 5de98259dc00d3153886b2d51ed8d7367f0f45da Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Suzanne=20Dup=C3=A9ron?= Date: Wed, 9 Oct 2019 00:51:29 -0400 Subject: [PATCH] Trying to merge new typer and new dev --- src/passes/4-typer/solver.ml | 98 ++++++++++++++++--------- src/passes/4-typer/typer.ml | 20 ++--- src/passes/6-transpiler/transpiler.ml | 6 ++ src/passes/6-transpiler/untranspiler.ml | 1 + src/passes/operators/helpers.ml | 2 +- src/passes/operators/operators.ml | 24 +++--- src/stages/ast_typed/PP.ml | 1 + src/stages/ast_typed/combinators.ml | 11 ++- src/stages/ast_typed/misc.ml | 2 + src/stages/ast_typed/types.ml | 1 + 10 files changed, 104 insertions(+), 62 deletions(-) diff --git a/src/passes/4-typer/solver.ml b/src/passes/4-typer/solver.ml index 941104001..138671f6e 100644 --- a/src/passes/4-typer/solver.ml +++ b/src/passes/4-typer/solver.ml @@ -4,6 +4,7 @@ module Core = Typesystem.Core module Wrap = struct module I = Ast_simplified + module T = Ast_typed module O = Core type constraints = O.type_constraint list @@ -16,8 +17,8 @@ module Wrap = struct (* let%bind state' = add_type state t in *) (* return expr state' in *) - let rec type_expression_to_type_value : I.type_expression -> O.type_value = fun te -> - match te with + let rec type_expression_to_type_value : T.type_value -> O.type_value = fun te -> + match te.type_value' with | T_tuple types -> P_constant (C_tuple, List.map type_expression_to_type_value types) | T_sum kvmap -> @@ -42,16 +43,43 @@ module Wrap = struct in P_constant (csttag, List.map type_expression_to_type_value args) + + let rec type_expression_to_type_value_copypasted : I.type_expression -> O.type_value = fun te -> + match te with + | T_tuple types -> + P_constant (C_tuple, List.map type_expression_to_type_value_copypasted types) + | T_sum kvmap -> + P_constant (C_variant, Map.String.to_list @@ Map.String.map type_expression_to_type_value_copypasted kvmap) + | T_record kvmap -> + P_constant (C_record, Map.String.to_list @@ Map.String.map type_expression_to_type_value_copypasted kvmap) + | T_function (arg , ret) -> + P_constant (C_arrow, List.map type_expression_to_type_value_copypasted [ arg ; ret ]) + | T_variable type_name -> P_variable type_name + | T_constant (type_name , args) -> + let csttag = Core.(match type_name with + | "arrow" -> C_arrow + | "option" -> C_option + | "tuple" -> C_tuple + | "map" -> C_map + | "list" -> C_list + | "set" -> C_set + | "unit" -> C_unit + | "bool" -> C_bool + | "string" -> C_string + | _ -> failwith "unknown type constructor") + in + P_constant (csttag, List.map type_expression_to_type_value_copypasted args) + (** TODO *) let type_declaration : I.declaration -> constraints = fun td -> match td with | Declaration_type (name , te) -> - let pattern = type_expression_to_type_value te in + let pattern = type_expression_to_type_value_copypasted te in [C_equation (P_variable (name) , pattern)] (* TODO: this looks wrong. If this is a type declaration, it should not set any constraints. *) | Declaration_constant (name, te, _) ->( match te with | Some (exp) -> - let pattern = type_expression_to_type_value exp in + let pattern = type_expression_to_type_value_copypasted exp in [C_equation (P_variable (name) , pattern)] (* TODO: this looks wrong. If this is a type declaration, it should not set any constraints. *) | None -> (** TODO *) @@ -62,12 +90,12 @@ module Wrap = struct let type_name = Core.fresh_type_variable () in [] , type_name - let variable : I.name -> I.type_expression -> (constraints * O.type_variable) = fun _name expr -> + let variable : I.name -> T.type_value -> (constraints * O.type_variable) = fun _name expr -> let pattern = type_expression_to_type_value expr in let type_name = Core.fresh_type_variable () in [C_equation (P_variable (type_name) , pattern)] , type_name - let literal : I.type_expression -> (constraints * O.type_variable) = fun t -> + let literal : T.type_value -> (constraints * O.type_variable) = fun t -> let pattern = type_expression_to_type_value t in let type_name = Core.fresh_type_variable () in [C_equation (P_variable (type_name) , pattern)] , type_name @@ -85,7 +113,7 @@ module Wrap = struct *) let tuple : I.type_expression list -> (constraints * O.type_variable) = fun tys -> - let patterns = List.map type_expression_to_type_value tys in + let patterns = List.map type_expression_to_type_value_copypasted tys in let pattern = O.(P_constant (C_tuple , patterns)) in let type_name = Core.fresh_type_variable () in [C_equation (P_variable (type_name) , pattern)] , type_name @@ -129,8 +157,8 @@ module Wrap = struct fun ~base ~key -> let key_type = Core.fresh_type_variable () in let element_type = Core.fresh_type_variable () in - let base' = type_expression_to_type_value base in - let key' = type_expression_to_type_value key in + let base' = type_expression_to_type_value_copypasted base in + let key' = type_expression_to_type_value_copypasted key in let base_expected = mk_map_type key_type element_type in let expr_type = Core.fresh_type_variable () in O.[C_equation (base' , base_expected); @@ -140,9 +168,9 @@ module Wrap = struct let constructor : I.type_expression -> I.type_expression -> I.type_expression -> (constraints * O.type_variable) = fun t_arg c_arg sum -> - let t_arg = type_expression_to_type_value t_arg in - let c_arg = type_expression_to_type_value c_arg in - let sum = type_expression_to_type_value sum in + let t_arg = type_expression_to_type_value_copypasted t_arg in + let c_arg = type_expression_to_type_value_copypasted c_arg in + let sum = type_expression_to_type_value_copypasted sum in let whole_expr = Core.fresh_type_variable () in [ C_equation (P_variable (whole_expr) , sum) ; @@ -150,7 +178,7 @@ module Wrap = struct ] , whole_expr let record : I.type_expression I.type_name_map -> (constraints * O.type_variable) = fun fields -> - let record_type = type_expression_to_type_value (I.t_record fields) in + let record_type = type_expression_to_type_value_copypasted (I.t_record fields) in let whole_expr = Core.fresh_type_variable () in [C_equation (P_variable whole_expr , record_type)] , whole_expr @@ -158,7 +186,7 @@ module Wrap = struct fun ctor element_tys -> let elttype = O.P_variable (Core.fresh_type_variable ()) in let aux elt = - let elt' = type_expression_to_type_value elt + let elt' = type_expression_to_type_value_copypasted elt in O.C_equation (elttype , elt') in let equations = List.map aux element_tys in let whole_expr = Core.fresh_type_variable () in @@ -174,10 +202,10 @@ module Wrap = struct let k_type = O.P_variable (Core.fresh_type_variable ()) in let v_type = O.P_variable (Core.fresh_type_variable ()) in let aux_k (k , _v) = - let k' = type_expression_to_type_value k in + let k' = type_expression_to_type_value_copypasted k in O.C_equation (k_type , k') in let aux_v (_k , v) = - let v' = type_expression_to_type_value v in + let v' = type_expression_to_type_value_copypasted v in O.C_equation (v_type , v') in let equations_k = List.map aux_k kv_tys in let equations_v = List.map aux_v kv_tys in @@ -189,16 +217,16 @@ module Wrap = struct let application : I.type_expression -> I.type_expression -> (constraints * O.type_variable) = fun f arg -> let whole_expr = Core.fresh_type_variable () in - let f' = type_expression_to_type_value f in - let arg' = type_expression_to_type_value arg in + let f' = type_expression_to_type_value_copypasted f in + let arg' = type_expression_to_type_value_copypasted arg in O.[ C_equation (f' , P_constant (C_arrow , [arg' ; P_variable whole_expr])) ] , whole_expr let look_up : I.type_expression -> I.type_expression -> (constraints * O.type_variable) = fun ds ind -> - let ds' = type_expression_to_type_value ds in - let ind' = type_expression_to_type_value ind in + let ds' = type_expression_to_type_value_copypasted ds in + let ind' = type_expression_to_type_value_copypasted ind in let whole_expr = Core.fresh_type_variable () in let v = Core.fresh_type_variable () in O.[ @@ -208,8 +236,8 @@ module Wrap = struct let sequence : I.type_expression -> I.type_expression -> (constraints * O.type_variable) = fun a b -> - let a' = type_expression_to_type_value a in - let b' = type_expression_to_type_value b in + let a' = type_expression_to_type_value_copypasted a in + let b' = type_expression_to_type_value_copypasted b in let whole_expr = Core.fresh_type_variable () in O.[ C_equation (a' , P_constant (C_unit , [])) ; @@ -218,8 +246,8 @@ module Wrap = struct let loop : I.type_expression -> I.type_expression -> (constraints * O.type_variable) = fun expr body -> - let expr' = type_expression_to_type_value expr in - let body' = type_expression_to_type_value body in + let expr' = type_expression_to_type_value_copypasted expr in + let body' = type_expression_to_type_value_copypasted body in let whole_expr = Core.fresh_type_variable () in O.[ C_equation (expr' , P_constant (C_bool , [])) ; @@ -229,11 +257,11 @@ module Wrap = struct let let_in : I.type_expression -> I.type_expression option -> I.type_expression -> (constraints * O.type_variable) = fun rhs rhs_tv_opt result -> - let rhs' = type_expression_to_type_value rhs in - let result' = type_expression_to_type_value result in + let rhs' = type_expression_to_type_value_copypasted rhs in + let result' = type_expression_to_type_value_copypasted result in let rhs_tv_opt' = match rhs_tv_opt with None -> [] - | Some annot -> O.[C_equation (rhs' , type_expression_to_type_value annot)] in + | Some annot -> O.[C_equation (rhs' , type_expression_to_type_value_copypasted annot)] in let whole_expr = Core.fresh_type_variable () in O.[ C_equation (result' , P_variable whole_expr) @@ -241,8 +269,8 @@ module Wrap = struct let assign : I.type_expression -> I.type_expression -> (constraints * O.type_variable) = fun v e -> - let v' = type_expression_to_type_value v in - let e' = type_expression_to_type_value e in + let v' = type_expression_to_type_value_copypasted v in + let e' = type_expression_to_type_value_copypasted e in let whole_expr = Core.fresh_type_variable () in O.[ C_equation (v' , e') ; @@ -251,8 +279,8 @@ module Wrap = struct let annotation : I.type_expression -> I.type_expression -> (constraints * O.type_variable) = fun e annot -> - let e' = type_expression_to_type_value e in - let annot' = type_expression_to_type_value annot in + let e' = type_expression_to_type_value_copypasted e in + let annot' = type_expression_to_type_value_copypasted annot in let whole_expr = Core.fresh_type_variable () in O.[ C_equation (e' , annot') ; @@ -262,7 +290,7 @@ module Wrap = struct let matching : I.type_expression list -> (constraints * O.type_variable) = fun es -> let whole_expr = Core.fresh_type_variable () in - let type_values = (List.map type_expression_to_type_value es) in + let type_values = (List.map type_expression_to_type_value_copypasted es) in let cs = List.map (fun e -> O.C_equation (P_variable whole_expr , e)) type_values in cs, whole_expr @@ -280,12 +308,12 @@ module Wrap = struct let unification_body = Core.fresh_type_variable () in let arg' = match arg with None -> [] - | Some arg -> O.[C_equation (P_variable unification_arg , type_expression_to_type_value arg)] in + | Some arg -> O.[C_equation (P_variable unification_arg , type_expression_to_type_value_copypasted arg)] in let body' = match body with None -> [] - | Some body -> O.[C_equation (P_variable unification_body , type_expression_to_type_value body)] + | Some body -> O.[C_equation (P_variable unification_body , type_expression_to_type_value_copypasted body)] in O.[ - C_equation (type_expression_to_type_value fresh , P_variable unification_arg) ; + C_equation (type_expression_to_type_value_copypasted fresh , P_variable unification_arg) ; C_equation (P_variable whole_expr , P_constant (C_arrow , [P_variable unification_arg ; P_variable unification_body])) diff --git a/src/passes/4-typer/typer.ml b/src/passes/4-typer/typer.ml index d32263ba8..70ad57305 100644 --- a/src/passes/4-typer/typer.ml +++ b/src/passes/4-typer/typer.ml @@ -420,17 +420,17 @@ and type_expression : environment -> Solver.state -> I.expression -> (O.annotate to actually perform the recursive calls *) (* Basic *) - | E_failwith expr -> ( - let%bind (expr', state') = type_expression e state expr in - let (constraints , expr_type) = Wrap.failwith_ () in - let expr'' = e_failwith expr' in - return expr'' state' constraints expr_type - ) + (* | E_failwith expr -> ( + * let%bind (expr', state') = type_expression e state expr in + * let (constraints , expr_type) = Wrap.failwith_ () in + * let expr'' = e_failwith expr' in + * return expr'' state' constraints expr_type + * ) *) | E_variable name -> ( - let%bind tv' = + let%bind (tv' : Environment.element) = trace_option (unbound_variable e name ae.location) @@ Environment.get_opt name e in - let (constraints , expr_type) = Wrap.variable name tv'.type_expression in + let (constraints , expr_type) = Wrap.variable name tv'.type_value in let expr' = e_variable name in return expr' state constraints expr_type ) @@ -449,8 +449,8 @@ and type_expression : environment -> Solver.state -> I.expression -> (O.annotate | E_literal (Literal_nat n) -> ( return_wrapped (e_nat n) state @@ Wrap.literal (t_nat ()) ) - | E_literal (Literal_tez t) -> ( - return_wrapped (e_tez t) state @@ Wrap.literal (t_tez ()) + | E_literal (Literal_mutez t) -> ( + return_wrapped (e_mutez t) state @@ Wrap.literal (t_mutez ()) ) | E_literal (Literal_address a) -> ( return_wrapped (e_address a) state @@ Wrap.literal (t_address ()) diff --git a/src/passes/6-transpiler/transpiler.ml b/src/passes/6-transpiler/transpiler.ml index db7fe394a..a3eca7837 100644 --- a/src/passes/6-transpiler/transpiler.ml +++ b/src/passes/6-transpiler/transpiler.ml @@ -28,6 +28,11 @@ them. please report this to the developers." in let content () = name in error title content + let no_type_variable name = + let title () = "type variables can't be transpiled" in + let content () = name in + error title content + let row_loc l = ("location" , fun () -> Format.asprintf "%a" Location.pp l) let unsupported_pattern_matching kind location = @@ -102,6 +107,7 @@ open Errors let rec transpile_type (t:AST.type_value) : type_value result = match t.type_value' with + | T_variable name -> fail @@ no_type_variable name | T_constant ("bool", []) -> ok (T_base Base_bool) | T_constant ("int", []) -> ok (T_base Base_int) | T_constant ("nat", []) -> ok (T_base Base_nat) diff --git a/src/passes/6-transpiler/untranspiler.ml b/src/passes/6-transpiler/untranspiler.ml index 78c41cca8..fb5a7c97b 100644 --- a/src/passes/6-transpiler/untranspiler.ml +++ b/src/passes/6-transpiler/untranspiler.ml @@ -203,3 +203,4 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression let m' = map_of_kv_list lst in return (E_record m') | T_function _ -> fail @@ bad_untranspile "function" v + | T_variable v -> return (E_variable v) diff --git a/src/passes/operators/helpers.ml b/src/passes/operators/helpers.ml index b588605f2..46ffc302b 100644 --- a/src/passes/operators/helpers.ml +++ b/src/passes/operators/helpers.ml @@ -113,7 +113,7 @@ module Typer = struct List.exists (eq_2 (a , b)) [ t_int () ; t_nat () ; - t_tez () ; + t_mutez () ; t_string () ; t_bytes () ; t_address () ; diff --git a/src/passes/operators/operators.ml b/src/passes/operators/operators.ml index 5eb1dfb91..27584f065 100644 --- a/src/passes/operators/operators.ml +++ b/src/passes/operators/operators.ml @@ -297,8 +297,8 @@ module Typer = struct then ok @@ t_int () else if (eq_1 a (t_timestamp ()) && eq_1 b (t_int ())) then ok @@ t_timestamp () else - if (eq_2 (a , b) (t_tez ())) - then ok @@ t_tez () else + if (eq_2 (a , b) (t_mutez ())) + then ok @@ t_mutez () else fail (simple_error "Typing substraction, bad parameters.") let some = typer_1 "SOME" @@ fun a -> ok @@ t_option a () @@ -428,16 +428,16 @@ module Typer = struct let unit = constant "UNIT" @@ t_unit () - let amount = constant "AMOUNT" @@ t_tez () + let amount = constant "AMOUNT" @@ t_mutez () - let balance = constant "BALANCE" @@ t_tez () + let balance = constant "BALANCE" @@ t_mutez () let address = constant "ADDRESS" @@ t_address () let now = constant "NOW" @@ t_timestamp () let transaction = typer_3 "CALL" @@ fun param amount contract -> - let%bind () = assert_t_tez amount in + let%bind () = assert_t_mutez amount in let%bind contract_param = get_t_contract contract in let%bind () = assert_type_value_eq (param , contract_param) in ok @@ t_operation () @@ -447,7 +447,7 @@ module Typer = struct let%bind () = assert_eq_1 delegate_opt (t_option (t_key_hash ()) ()) in let%bind () = assert_eq_1 spendable (t_bool ()) in let%bind () = assert_eq_1 delegatable (t_bool ()) in - let%bind () = assert_t_tez init_balance in + let%bind () = assert_t_mutez init_balance in let%bind (arg , res) = get_t_function code in let%bind (_param , storage) = get_t_pair arg in let%bind (storage' , op_lst) = get_t_pair res in @@ -485,8 +485,8 @@ module Typer = struct then ok @@ t_nat () else if eq_2 (a , b) (t_int ()) then ok @@ t_int () else - if (eq_1 a (t_nat ()) && eq_1 b (t_tez ())) || (eq_1 b (t_nat ()) && eq_1 a (t_tez ())) - then ok @@ t_tez () else + if (eq_1 a (t_nat ()) && eq_1 b (t_mutez ())) || (eq_1 b (t_nat ()) && eq_1 a (t_mutez ())) + then ok @@ t_mutez () else simple_fail "Multiplying with wrong types" let div = typer_2 "DIV" @@ fun a b -> @@ -494,8 +494,8 @@ module Typer = struct then ok @@ t_nat () else if eq_2 (a , b) (t_int ()) then ok @@ t_int () else - if eq_1 a (t_tez ()) && eq_1 b (t_nat ()) - then ok @@ t_tez () else + if eq_1 a (t_mutez ()) && eq_1 b (t_nat ()) + then ok @@ t_mutez () else simple_fail "Dividing with wrong types" let mod_ = typer_2 "MOD" @@ fun a b -> @@ -508,8 +508,8 @@ module Typer = struct then ok @@ t_nat () else if eq_2 (a , b) (t_int ()) then ok @@ t_int () else - if eq_2 (a , b) (t_tez ()) - then ok @@ t_tez () else + if eq_2 (a , b) (t_mutez ()) + then ok @@ t_mutez () else if (eq_1 a (t_nat ()) && eq_1 b (t_int ())) || (eq_1 b (t_nat ()) && eq_1 a (t_int ())) then ok @@ t_int () else if (eq_1 a (t_timestamp ()) && eq_1 b (t_int ())) || (eq_1 b (t_timestamp ()) && eq_1 a (t_int ())) diff --git a/src/stages/ast_typed/PP.ml b/src/stages/ast_typed/PP.ml index fb8923ea9..d77334e87 100644 --- a/src/stages/ast_typed/PP.ml +++ b/src/stages/ast_typed/PP.ml @@ -14,6 +14,7 @@ let rec type_value' ppf (tv':type_value') : unit = | T_function (a, b) -> fprintf ppf "%a -> %a" type_value a type_value b | T_constant (c, []) -> fprintf ppf "%s" c | T_constant (c, n) -> fprintf ppf "%s(%a)" c (list_sep_d type_value) n + | T_variable name -> fprintf ppf "%s" name and type_value ppf (tv:type_value) : unit = type_value' ppf tv.type_value' diff --git a/src/stages/ast_typed/combinators.ml b/src/stages/ast_typed/combinators.ml index d9dcebb73..a4909851c 100644 --- a/src/stages/ast_typed/combinators.ml +++ b/src/stages/ast_typed/combinators.ml @@ -21,11 +21,12 @@ let t_int ?s () : type_value = make_t (T_constant ("int", [])) s let t_address ?s () : type_value = make_t (T_constant ("address", [])) s let t_operation ?s () : type_value = make_t (T_constant ("operation", [])) s let t_nat ?s () : type_value = make_t (T_constant ("nat", [])) s -let t_tez ?s () : type_value = make_t (T_constant ("tez", [])) s +let t_mutez ?s () : type_value = make_t (T_constant ("tez", [])) s let t_timestamp ?s () : type_value = make_t (T_constant ("timestamp", [])) s let t_unit ?s () : type_value = make_t (T_constant ("unit", [])) s let t_option o ?s () : type_value = make_t (T_constant ("option", [o])) s let t_tuple lst ?s () : type_value = make_t (T_tuple lst) s +let t_variable t ?s () : type_value = make_t (T_variable t) s let t_list t ?s () : type_value = make_t (T_constant ("list", [t])) s let t_set t ?s () : type_value = make_t (T_constant ("set", [t])) s let t_contract t ?s () : type_value = make_t (T_constant ("contract", [t])) s @@ -82,7 +83,7 @@ let get_t_unit (t:type_value) : unit result = match t.type_value' with | T_constant ("unit", []) -> ok () | _ -> simple_fail "not a unit" -let get_t_tez (t:type_value) : unit result = match t.type_value' with +let get_t_mutez (t:type_value) : unit result = match t.type_value' with | T_constant ("tez", []) -> ok () | _ -> simple_fail "not a tez" @@ -179,7 +180,7 @@ let assert_t_map = fun t -> let is_t_map = Function.compose to_bool get_t_map let is_t_big_map = Function.compose to_bool get_t_big_map -let assert_t_tez : type_value -> unit result = get_t_tez +let assert_t_mutez : type_value -> unit result = get_t_mutez let assert_t_key = get_t_key let assert_t_signature = get_t_signature let assert_t_key_hash = get_t_key_hash @@ -235,6 +236,8 @@ let e_nat n : expression = E_literal (Literal_nat n) let e_mutez n : expression = E_literal (Literal_mutez n) let e_bool b : expression = E_literal (Literal_bool b) let e_string s : expression = E_literal (Literal_string s) +let e_bytes s : expression = E_literal (Literal_bytes s) +let e_timestamp s : expression = E_literal (Literal_timestamp s) let e_address s : expression = E_literal (Literal_address s) let e_operation s : expression = E_literal (Literal_operation s) let e_lambda l : expression = E_lambda l @@ -247,7 +250,7 @@ let e_let_in binder rhs result = E_let_in { binder ; rhs ; result } let e_a_unit = make_a_e e_unit (t_unit ()) let e_a_int n = make_a_e (e_int n) (t_int ()) let e_a_nat n = make_a_e (e_nat n) (t_nat ()) -let e_a_mutez n = make_a_e (e_mutez n) (t_tez ()) +let e_a_mutez n = make_a_e (e_mutez n) (t_mutez ()) let e_a_bool b = make_a_e (e_bool b) (t_bool ()) let e_a_string s = make_a_e (e_string s) (t_string ()) let e_a_address s = make_a_e (e_address s) (t_address ()) diff --git a/src/stages/ast_typed/misc.ml b/src/stages/ast_typed/misc.ml index 5ba66b4ea..723ba3100 100644 --- a/src/stages/ast_typed/misc.ml +++ b/src/stages/ast_typed/misc.ml @@ -346,6 +346,8 @@ let rec assert_type_value_eq (a, b: (type_value * type_value)) : unit result = m let%bind _ = assert_type_value_eq (result, result') in ok () | T_function _, _ -> fail @@ different_kinds a b + | T_variable x, T_variable y -> let _ = x == y in failwith "TODO : we must check that the two types were bound at the same location (even if they have the same name), i.e. use something like De Bruijn indices or a propper graph encoding" + | T_variable _, _ -> fail @@ different_kinds a b (* No information about what made it fail *) let type_value_eq ab = Trace.to_bool @@ assert_type_value_eq ab diff --git a/src/stages/ast_typed/types.ml b/src/stages/ast_typed/types.ml index d0b8ee2bb..b60632a0d 100644 --- a/src/stages/ast_typed/types.ml +++ b/src/stages/ast_typed/types.ml @@ -56,6 +56,7 @@ and type_value' = | T_sum of tv_map | T_record of tv_map | T_constant of type_name * tv list + | T_variable of type_name | T_function of (tv * tv) and type_value = {