Wrap type names with a constructor Type_name, so that merlin does not think that all strings are type names

This commit is contained in:
Suzanne Dupéron 2019-10-30 12:50:19 -04:00
parent 3f0b9346a5
commit c0397f68a0
10 changed files with 125 additions and 125 deletions

View File

@ -42,8 +42,8 @@ module Wrap = struct
P_constant (C_record, Map.String.to_list @@ Map.String.map type_expression_to_type_value kvmap)
| T_function (arg , ret) ->
P_constant (C_arrow, List.map type_expression_to_type_value [ arg ; ret ])
| T_variable type_name -> P_variable type_name
| T_constant (type_name , args) ->
| T_variable (Type_name type_name) -> P_variable type_name
| T_constant (Type_name type_name , args) ->
let csttag = Core.(match type_name with
| "arrow" -> C_arrow
| "option" -> C_option
@ -105,15 +105,15 @@ module Wrap = struct
let type_name = Core.fresh_type_variable () in
[] , type_name
let variable : I.name -> T.type_value -> (constraints * O.type_variable) = fun _name expr ->
let variable : I.name -> T.type_value -> (constraints * T.type_name) = 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
[C_equation (P_variable (type_name) , pattern)] , Type_name type_name
let literal : T.type_value -> (constraints * O.type_variable) = fun t ->
let literal : T.type_value -> (constraints * T.type_name) = 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
[C_equation (P_variable (type_name) , pattern)] , Type_name type_name
(*
let literal_bool : unit -> (constraints * O.type_variable) = fun () ->
@ -127,11 +127,11 @@ module Wrap = struct
[C_equation (P_variable (type_name) , pattern)] , type_name
*)
let tuple : T.type_value list -> (constraints * O.type_variable) = fun tys ->
let tuple : T.type_value list -> (constraints * T.type_name) = fun tys ->
let patterns = List.map type_expression_to_type_value 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
[C_equation (P_variable (type_name) , pattern)] , Type_name type_name
(* let t_tuple = ('label:int, 'v) … -> record ('label : 'v)*)
(* let t_constructor = ('label:string, 'v) -> variant ('label : 'v) *)
@ -158,15 +158,15 @@ module Wrap = struct
end
(* TODO: I think we should take an I.expression for the base+label *)
let access_label ~(base : T.type_value) ~(label : O.label) : (constraints * O.type_variable) =
let access_label ~(base : T.type_value) ~(label : O.label) : (constraints * T.type_name) =
let base' = type_expression_to_type_value base in
let expr_type = Core.fresh_type_variable () in
[O.C_access_label (base' , label , expr_type)] , expr_type
[O.C_access_label (base' , label , expr_type)] , Type_name expr_type
let access_int ~base ~index = access_label ~base ~label:(L_int index)
let access_string ~base ~property = access_label ~base ~label:(L_string property)
let access_map : base:T.type_value -> key:T.type_value -> (constraints * O.type_variable) =
let access_map : base:T.type_value -> key:T.type_value -> (constraints * T.type_name) =
let mk_map_type key_type element_type =
O.P_constant O.(C_map , [P_variable element_type; P_variable key_type]) in
fun ~base ~key ->
@ -178,10 +178,10 @@ module Wrap = struct
let expr_type = Core.fresh_type_variable () in
O.[C_equation (base' , base_expected);
C_equation (key' , P_variable key_type);
C_equation (P_variable expr_type , P_variable element_type)] , expr_type
C_equation (P_variable expr_type , P_variable element_type)] , Type_name expr_type
let constructor
: T.type_value -> T.type_value -> T.type_value -> (constraints * O.type_variable)
: T.type_value -> T.type_value -> T.type_value -> (constraints * T.type_name)
= 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
@ -190,14 +190,14 @@ module Wrap = struct
[
C_equation (P_variable (whole_expr) , sum) ;
C_equation (t_arg , c_arg)
] , whole_expr
] , Type_name whole_expr
let record : T.type_value I.type_name_map -> (constraints * O.type_variable) = fun fields ->
let record : T.type_value I.type_name_map -> (constraints * T.type_name) = fun fields ->
let record_type = type_expression_to_type_value (T.t_record fields ()) in
let whole_expr = Core.fresh_type_variable () in
[C_equation (P_variable whole_expr , record_type)] , whole_expr
[C_equation (P_variable whole_expr , record_type)] , Type_name whole_expr
let collection : O.constant_tag -> T.type_value list -> (constraints * O.type_variable) =
let collection : O.constant_tag -> T.type_value list -> (constraints * T.type_name) =
fun ctor element_tys ->
let elttype = O.P_variable (Core.fresh_type_variable ()) in
let aux elt =
@ -207,12 +207,12 @@ module Wrap = struct
let whole_expr = Core.fresh_type_variable () in
O.[
C_equation (P_variable whole_expr , O.P_constant (ctor , [elttype]))
] @ equations , whole_expr
] @ equations , Type_name whole_expr
let list = collection O.C_list
let set = collection O.C_set
let map : (T.type_value * T.type_value) list -> (constraints * O.type_variable) =
let map : (T.type_value * T.type_value) list -> (constraints * T.type_name) =
fun kv_tys ->
let k_type = O.P_variable (Core.fresh_type_variable ()) in
let v_type = O.P_variable (Core.fresh_type_variable ()) in
@ -227,9 +227,9 @@ module Wrap = struct
let whole_expr = Core.fresh_type_variable () in
O.[
C_equation (P_variable whole_expr , O.P_constant (C_map , [k_type ; v_type]))
] @ equations_k @ equations_v , whole_expr
] @ equations_k @ equations_v , Type_name whole_expr
let big_map : (T.type_value * T.type_value) list -> (constraints * O.type_variable) =
let big_map : (T.type_value * T.type_value) list -> (constraints * T.type_name) =
fun kv_tys ->
let k_type = O.P_variable (Core.fresh_type_variable ()) in
let v_type = O.P_variable (Core.fresh_type_variable ()) in
@ -246,18 +246,18 @@ module Wrap = struct
(* TODO: this doesn't tag big_maps uniquely (i.e. if two
big_map have the same type, they can be swapped. *)
C_equation (P_variable whole_expr , O.P_constant (C_big_map , [k_type ; v_type]))
] @ equations_k @ equations_v , whole_expr
] @ equations_k @ equations_v , Type_name whole_expr
let application : T.type_value -> T.type_value -> (constraints * O.type_variable) =
let application : T.type_value -> T.type_value -> (constraints * T.type_name) =
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
O.[
C_equation (f' , P_constant (C_arrow , [arg' ; P_variable whole_expr]))
] , whole_expr
] , Type_name whole_expr
let look_up : T.type_value -> T.type_value -> (constraints * O.type_variable) =
let look_up : T.type_value -> T.type_value -> (constraints * T.type_name) =
fun ds ind ->
let ds' = type_expression_to_type_value ds in
let ind' = type_expression_to_type_value ind in
@ -266,9 +266,9 @@ module Wrap = struct
O.[
C_equation (ds' , P_constant (C_map, [ind' ; P_variable v])) ;
C_equation (P_variable whole_expr , P_constant (C_option , [P_variable v]))
] , whole_expr
] , Type_name whole_expr
let sequence : T.type_value -> T.type_value -> (constraints * O.type_variable) =
let sequence : T.type_value -> T.type_value -> (constraints * T.type_name) =
fun a b ->
let a' = type_expression_to_type_value a in
let b' = type_expression_to_type_value b in
@ -276,9 +276,9 @@ module Wrap = struct
O.[
C_equation (a' , P_constant (C_unit , [])) ;
C_equation (b' , P_variable whole_expr)
] , whole_expr
] , Type_name whole_expr
let loop : T.type_value -> T.type_value -> (constraints * O.type_variable) =
let loop : T.type_value -> T.type_value -> (constraints * T.type_name) =
fun expr body ->
let expr' = type_expression_to_type_value expr in
let body' = type_expression_to_type_value body in
@ -287,9 +287,9 @@ module Wrap = struct
C_equation (expr' , P_constant (C_bool , [])) ;
C_equation (body' , P_constant (C_unit , [])) ;
C_equation (P_variable whole_expr , P_constant (C_unit , []))
] , whole_expr
] , Type_name whole_expr
let let_in : T.type_value -> T.type_value option -> T.type_value -> (constraints * O.type_variable) =
let let_in : T.type_value -> T.type_value option -> T.type_value -> (constraints * T.type_name) =
fun rhs rhs_tv_opt result ->
let rhs' = type_expression_to_type_value rhs in
let result' = type_expression_to_type_value result in
@ -299,9 +299,9 @@ module Wrap = struct
let whole_expr = Core.fresh_type_variable () in
O.[
C_equation (result' , P_variable whole_expr)
] @ rhs_tv_opt', whole_expr
] @ rhs_tv_opt', Type_name whole_expr
let assign : T.type_value -> T.type_value -> (constraints * O.type_variable) =
let assign : T.type_value -> T.type_value -> (constraints * T.type_name) =
fun v e ->
let v' = type_expression_to_type_value v in
let e' = type_expression_to_type_value e in
@ -309,9 +309,9 @@ module Wrap = struct
O.[
C_equation (v' , e') ;
C_equation (P_variable whole_expr , P_constant (C_unit , []))
] , whole_expr
] , Type_name whole_expr
let annotation : T.type_value -> T.type_value -> (constraints * O.type_variable) =
let annotation : T.type_value -> T.type_value -> (constraints * T.type_name) =
fun e annot ->
let e' = type_expression_to_type_value e in
let annot' = type_expression_to_type_value annot in
@ -319,14 +319,14 @@ module Wrap = struct
O.[
C_equation (e' , annot') ;
C_equation (e' , P_variable whole_expr)
] , whole_expr
] , Type_name whole_expr
let matching : T.type_value list -> (constraints * O.type_variable) =
let matching : T.type_value list -> (constraints * T.type_name) =
fun es ->
let whole_expr = Core.fresh_type_variable () in
let type_values = (List.map type_expression_to_type_value es) in
let cs = List.map (fun e -> O.C_equation (P_variable whole_expr , e)) type_values
in cs, whole_expr
in cs, Type_name whole_expr
let fresh_binder () =
Core.fresh_type_variable ()
@ -335,7 +335,7 @@ module Wrap = struct
: T.type_value ->
T.type_value option ->
T.type_value option ->
(constraints * O.type_variable) =
(constraints * T.type_name) =
fun fresh arg body ->
let whole_expr = Core.fresh_type_variable () in
let unification_arg = Core.fresh_type_variable () in
@ -351,7 +351,7 @@ module Wrap = struct
C_equation (P_variable whole_expr ,
P_constant (C_arrow , [P_variable unification_arg ;
P_variable unification_body]))
] @ arg' @ body' , whole_expr
] @ arg' @ body' , Type_name whole_expr
end

View File

@ -389,7 +389,7 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_value result =
ok tv
| T_constant (cst, lst) ->
let%bind lst' = bind_list @@ List.map (evaluate_type e) lst in
return (T_constant(cst, lst'))
return (T_constant(Type_name cst, lst'))
and type_expression : environment -> Solver.state -> I.expression -> (O.annotated_expression * Solver.state) result = fun e state ae ->
let open Solver in
@ -867,7 +867,7 @@ and type_expression : environment -> Solver.state -> I.expression -> (O.annotate
let%bind input_type' = bind_map_option (evaluate_type e) input_type in
let%bind output_type' = bind_map_option (evaluate_type e) output_type in
let fresh : O.type_value = t_variable (Wrap.fresh_binder ()) () in
let fresh : O.type_value = t_variable (Type_name (Wrap.fresh_binder ())) () in
let e' = Environment.add_ez_binder (fst binder) fresh e in
let%bind (result , state') = type_expression e' state result in
@ -945,7 +945,7 @@ 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 : O.type_name) (expr : Solver.c_constructor_simpl) (p:O.program result) =
let aux (v : string (* this string is a type_name or type_variable I think *)) (expr : Solver.c_constructor_simpl) (p:O.program result) =
let%bind p = p 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 *)
@ -991,10 +991,10 @@ let rec untype_type_expression (t:O.type_value) : (I.type_expression) result =
| O.T_record x ->
let%bind x' = bind_map_smap untype_type_expression x in
ok @@ I.T_record x'
| O.T_constant (tag, args) ->
| O.T_constant (Type_name tag, args) ->
let%bind args' = bind_map_list untype_type_expression args in
ok @@ I.T_constant (tag, args')
| O.T_variable name -> ok @@ I.T_variable name (* TODO: is this the right conversion? *)
| O.T_variable (Type_name name) -> ok @@ I.T_variable name (* TODO: is this the right conversion? *)
| O.T_function (a , b) ->
let%bind a' = untype_type_expression a in
let%bind b' = untype_type_expression b in

View File

@ -114,36 +114,36 @@ 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)
| T_constant ("tez", []) -> ok (T_base Base_tez)
| T_constant ("string", []) -> ok (T_base Base_string)
| T_constant ("bytes", []) -> ok (T_base Base_bytes)
| T_constant ("address", []) -> ok (T_base Base_address)
| T_constant ("timestamp", []) -> ok (T_base Base_timestamp)
| T_constant ("unit", []) -> ok (T_base Base_unit)
| T_constant ("operation", []) -> ok (T_base Base_operation)
| T_constant ("contract", [x]) ->
| T_variable (Type_name name) -> fail @@ no_type_variable name
| T_constant (Type_name "bool", []) -> ok (T_base Base_bool)
| T_constant (Type_name "int", []) -> ok (T_base Base_int)
| T_constant (Type_name "nat", []) -> ok (T_base Base_nat)
| T_constant (Type_name "tez", []) -> ok (T_base Base_tez)
| T_constant (Type_name "string", []) -> ok (T_base Base_string)
| T_constant (Type_name "bytes", []) -> ok (T_base Base_bytes)
| T_constant (Type_name "address", []) -> ok (T_base Base_address)
| T_constant (Type_name "timestamp", []) -> ok (T_base Base_timestamp)
| T_constant (Type_name "unit", []) -> ok (T_base Base_unit)
| T_constant (Type_name "operation", []) -> ok (T_base Base_operation)
| T_constant (Type_name "contract", [x]) ->
let%bind x' = transpile_type x in
ok (T_contract x')
| T_constant ("map", [key;value]) ->
| T_constant (Type_name "map", [key;value]) ->
let%bind kv' = bind_map_pair transpile_type (key, value) in
ok (T_map kv')
| T_constant ("big_map", [key;value] ) ->
| T_constant (Type_name "big_map", [key;value] ) ->
let%bind kv' = bind_map_pair transpile_type (key, value) in
ok (T_big_map kv')
| T_constant ("list", [t]) ->
| T_constant (Type_name "list", [t]) ->
let%bind t' = transpile_type t in
ok (T_list t')
| T_constant ("set", [t]) ->
| T_constant (Type_name "set", [t]) ->
let%bind t' = transpile_type t in
ok (T_set t')
| T_constant ("option", [o]) ->
| T_constant (Type_name "option", [o]) ->
let%bind o' = transpile_type o in
ok (T_option o')
| T_constant (name , _lst) -> fail @@ unrecognized_type_constant name
| T_constant (Type_name name , _lst) -> fail @@ unrecognized_type_constant name
(* TODO hmm *)
| T_sum m ->
let node = Append_tree.of_list @@ kv_list_of_map m in

View File

@ -53,61 +53,61 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression
let open! AST in
let return e = ok (make_a_e_empty e t) in
match t.type_value' with
| T_constant ("unit", []) -> (
| T_constant (Type_name "unit", []) -> (
let%bind () =
trace_strong (wrong_mini_c_value "unit" v) @@
get_unit v in
return (E_literal Literal_unit)
)
| T_constant ("bool", []) -> (
| T_constant (Type_name "bool", []) -> (
let%bind b =
trace_strong (wrong_mini_c_value "bool" v) @@
get_bool v in
return (E_literal (Literal_bool b))
)
| T_constant ("int", []) -> (
| T_constant (Type_name "int", []) -> (
let%bind n =
trace_strong (wrong_mini_c_value "int" v) @@
get_int v in
return (E_literal (Literal_int n))
)
| T_constant ("nat", []) -> (
| T_constant (Type_name "nat", []) -> (
let%bind n =
trace_strong (wrong_mini_c_value "nat" v) @@
get_nat v in
return (E_literal (Literal_nat n))
)
| T_constant ("timestamp", []) -> (
| T_constant (Type_name "timestamp", []) -> (
let%bind n =
trace_strong (wrong_mini_c_value "timestamp" v) @@
get_timestamp v in
return (E_literal (Literal_timestamp n))
)
| T_constant ("tez", []) -> (
| T_constant (Type_name "tez", []) -> (
let%bind n =
trace_strong (wrong_mini_c_value "tez" v) @@
get_mutez v in
return (E_literal (Literal_mutez n))
)
| T_constant ("string", []) -> (
| T_constant (Type_name "string", []) -> (
let%bind n =
trace_strong (wrong_mini_c_value "string" v) @@
get_string v in
return (E_literal (Literal_string n))
)
| T_constant ("bytes", []) -> (
| T_constant (Type_name "bytes", []) -> (
let%bind n =
trace_strong (wrong_mini_c_value "bytes" v) @@
get_bytes v in
return (E_literal (Literal_bytes n))
)
| T_constant ("address", []) -> (
| T_constant (Type_name "address", []) -> (
let%bind n =
trace_strong (wrong_mini_c_value "address" v) @@
get_string v in
return (E_literal (Literal_address n))
)
| T_constant ("option", [o]) -> (
| T_constant (Type_name "option", [o]) -> (
let%bind opt =
trace_strong (wrong_mini_c_value "option" v) @@
get_option v in
@ -117,7 +117,7 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression
let%bind s' = untranspile s o in
ok (e_a_empty_some s')
)
| T_constant ("map", [k_ty;v_ty]) -> (
| T_constant (Type_name "map", [k_ty;v_ty]) -> (
let%bind lst =
trace_strong (wrong_mini_c_value "map" v) @@
get_map v in
@ -129,7 +129,7 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression
bind_map_list aux lst in
return (E_map lst')
)
| T_constant ("big_map", [k_ty;v_ty]) -> (
| T_constant (Type_name "big_map", [k_ty;v_ty]) -> (
let%bind lst =
trace_strong (wrong_mini_c_value "big_map" v) @@
get_big_map v in
@ -141,7 +141,7 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression
bind_map_list aux lst in
return (E_big_map lst')
)
| T_constant ("list", [ty]) -> (
| T_constant (Type_name "list", [ty]) -> (
let%bind lst =
trace_strong (wrong_mini_c_value "list" v) @@
get_list v in
@ -150,7 +150,7 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression
bind_map_list aux lst in
return (E_list lst')
)
| T_constant ("set", [ty]) -> (
| T_constant (Type_name "set", [ty]) -> (
let%bind lst =
trace_strong (wrong_mini_c_value "set" v) @@
get_set v in
@ -159,15 +159,15 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression
bind_map_list aux lst in
return (E_set lst')
)
| T_constant ("contract" , [_ty]) ->
| T_constant (Type_name "contract" , [_ty]) ->
fail @@ bad_untranspile "contract" v
| T_constant ("operation" , []) -> (
| T_constant (Type_name "operation" , []) -> (
let%bind op =
trace_strong (wrong_mini_c_value "operation" v) @@
get_operation v in
return (E_literal (Literal_operation op))
)
| T_constant (name , _lst) ->
| T_constant (Type_name name , _lst) ->
fail @@ unknown_untranspile name v
| T_sum m ->
let lst = kv_list_of_map m in
@ -203,4 +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)
| T_variable (Type_name v) -> return (E_variable v)

View File

@ -12,9 +12,9 @@ let rec type_value' ppf (tv':type_value') : unit =
| T_sum m -> fprintf ppf "sum[%a]" (smap_sep_d type_value) m
| T_record m -> fprintf ppf "record[%a]" (smap_sep_d type_value) m
| 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
| T_constant (Type_name c, []) -> fprintf ppf "%s" c
| T_constant (Type_name c, n) -> fprintf ppf "%s(%a)" c (list_sep_d type_value) n
| T_variable (Type_name name) -> fprintf ppf "%s" name
and type_value ppf (tv:type_value) : unit =
type_value' ppf tv.type_value'

View File

@ -11,24 +11,24 @@ let make_a_e ?(location = Location.generated) expression type_annotation environ
let make_n_e name a_e = { name ; annotated_expression = a_e }
let make_n_t type_name type_value = { type_name ; type_value }
let t_bool ?s () : type_value = make_t (T_constant ("bool", [])) s
let t_string ?s () : type_value = make_t (T_constant ("string", [])) s
let t_bytes ?s () : type_value = make_t (T_constant ("bytes", [])) s
let t_key ?s () : type_value = make_t (T_constant ("key", [])) s
let t_key_hash ?s () : type_value = make_t (T_constant ("key_hash", [])) s
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_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_bool ?s () : type_value = make_t (T_constant (Type_name "bool", [])) s
let t_string ?s () : type_value = make_t (T_constant (Type_name "string", [])) s
let t_bytes ?s () : type_value = make_t (T_constant (Type_name "bytes", [])) s
let t_key ?s () : type_value = make_t (T_constant (Type_name "key", [])) s
let t_key_hash ?s () : type_value = make_t (T_constant (Type_name "key_hash", [])) s
let t_int ?s () : type_value = make_t (T_constant (Type_name "int", [])) s
let t_address ?s () : type_value = make_t (T_constant (Type_name "address", [])) s
let t_operation ?s () : type_value = make_t (T_constant (Type_name "operation", [])) s
let t_nat ?s () : type_value = make_t (T_constant (Type_name "nat", [])) s
let t_mutez ?s () : type_value = make_t (T_constant (Type_name "tez", [])) s
let t_timestamp ?s () : type_value = make_t (T_constant (Type_name "timestamp", [])) s
let t_unit ?s () : type_value = make_t (T_constant (Type_name "unit", [])) s
let t_option o ?s () : type_value = make_t (T_constant (Type_name "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
let t_list t ?s () : type_value = make_t (T_constant (Type_name "list", [t])) s
let t_set t ?s () : type_value = make_t (T_constant (Type_name "set", [t])) s
let t_contract t ?s () : type_value = make_t (T_constant (Type_name "contract", [t])) s
let t_pair a b ?s () = t_tuple [a ; b] ?s ()
let t_record m ?s () : type_value = make_t (T_record m) s
@ -40,8 +40,8 @@ let ez_t_record lst ?s () : type_value =
let m = SMap.of_list lst in
t_record m ?s ()
let t_map key value ?s () = make_t (T_constant ("map", [key ; value])) s
let t_big_map key value ?s () = make_t (T_constant ("big_map", [key ; value])) s
let t_map key value ?s () = make_t (T_constant (Type_name "map", [key ; value])) s
let t_big_map key value ?s () = make_t (T_constant (Type_name "big_map", [key ; value])) s
let t_sum m ?s () : type_value = make_t (T_sum m) s
let make_t_ez_sum (lst:(string * type_value) list) : type_value =
@ -67,59 +67,59 @@ let get_lambda_with_type e =
| _ -> simple_fail "not a lambda with functional type"
let get_t_bool (t:type_value) : unit result = match t.type_value' with
| T_constant ("bool", []) -> ok ()
| T_constant (Type_name "bool", []) -> ok ()
| _ -> simple_fail "not a bool"
let get_t_int (t:type_value) : unit result = match t.type_value' with
| T_constant ("int", []) -> ok ()
| T_constant (Type_name "int", []) -> ok ()
| _ -> simple_fail "not a int"
let get_t_nat (t:type_value) : unit result = match t.type_value' with
| T_constant ("nat", []) -> ok ()
| T_constant (Type_name "nat", []) -> ok ()
| _ -> simple_fail "not a nat"
let get_t_unit (t:type_value) : unit result = match t.type_value' with
| T_constant ("unit", []) -> ok ()
| T_constant (Type_name "unit", []) -> ok ()
| _ -> simple_fail "not a unit"
let get_t_mutez (t:type_value) : unit result = match t.type_value' with
| T_constant ("tez", []) -> ok ()
| T_constant (Type_name "tez", []) -> ok ()
| _ -> simple_fail "not a tez"
let get_t_bytes (t:type_value) : unit result = match t.type_value' with
| T_constant ("bytes", []) -> ok ()
| T_constant (Type_name "bytes", []) -> ok ()
| _ -> simple_fail "not a bytes"
let get_t_string (t:type_value) : unit result = match t.type_value' with
| T_constant ("string", []) -> ok ()
| T_constant (Type_name "string", []) -> ok ()
| _ -> simple_fail "not a string"
let get_t_contract (t:type_value) : type_value result = match t.type_value' with
| T_constant ("contract", [x]) -> ok x
| T_constant (Type_name "contract", [x]) -> ok x
| _ -> simple_fail "not a contract"
let get_t_option (t:type_value) : type_value result = match t.type_value' with
| T_constant ("option", [o]) -> ok o
| T_constant (Type_name "option", [o]) -> ok o
| _ -> simple_fail "not a option"
let get_t_list (t:type_value) : type_value result = match t.type_value' with
| T_constant ("list", [o]) -> ok o
| T_constant (Type_name "list", [o]) -> ok o
| _ -> simple_fail "not a list"
let get_t_set (t:type_value) : type_value result = match t.type_value' with
| T_constant ("set", [o]) -> ok o
| T_constant (Type_name "set", [o]) -> ok o
| _ -> simple_fail "not a set"
let get_t_key (t:type_value) : unit result = match t.type_value' with
| T_constant ("key", []) -> ok ()
| T_constant (Type_name "key", []) -> ok ()
| _ -> simple_fail "not a key"
let get_t_signature (t:type_value) : unit result = match t.type_value' with
| T_constant ("signature", []) -> ok ()
| T_constant (Type_name "signature", []) -> ok ()
| _ -> simple_fail "not a signature"
let get_t_key_hash (t:type_value) : unit result = match t.type_value' with
| T_constant ("key_hash", []) -> ok ()
| T_constant (Type_name "key_hash", []) -> ok ()
| _ -> simple_fail "not a key_hash"
let get_t_tuple (t:type_value) : type_value list result = match t.type_value' with
@ -148,12 +148,12 @@ let get_t_record (t:type_value) : type_value SMap.t result = match t.type_value'
let get_t_map (t:type_value) : (type_value * type_value) result =
match t.type_value' with
| T_constant ("map", [k;v]) -> ok (k, v)
| T_constant (Type_name "map", [k;v]) -> ok (k, v)
| _ -> simple_fail "get: not a map"
let get_t_big_map (t:type_value) : (type_value * type_value) result =
match t.type_value' with
| T_constant ("big_map", [k;v]) -> ok (k, v)
| T_constant (Type_name "big_map", [k;v]) -> ok (k, v)
| _ -> simple_fail "get: not a big_map"
let get_t_map_key : type_value -> type_value result = fun t ->
@ -201,7 +201,7 @@ let assert_t_bytes = fun t ->
let assert_t_operation (t:type_value) : unit result =
match t.type_value' with
| T_constant ("operation" , []) -> ok ()
| T_constant (Type_name "operation" , []) -> ok ()
| _ -> simple_fail "assert: not an operation"
let assert_t_list_operation (t : type_value) : unit result =
@ -209,11 +209,11 @@ let assert_t_list_operation (t : type_value) : unit result =
assert_t_operation t'
let assert_t_int : type_value -> unit result = fun t -> match t.type_value' with
| T_constant ("int", []) -> ok ()
| T_constant (Type_name "int", []) -> ok ()
| _ -> simple_fail "not an int"
let assert_t_nat : type_value -> unit result = fun t -> match t.type_value' with
| T_constant ("nat", []) -> ok ()
| T_constant (Type_name "nat", []) -> ok ()
| _ -> simple_fail "not an nat"
let assert_t_bool : type_value -> unit result = fun v -> get_t_bool v

View File

@ -24,7 +24,7 @@ val t_option : type_value -> ?s:S.type_expression -> unit -> type_value
val t_pair : type_value -> type_value -> ?s:S.type_expression -> unit -> type_value
val t_list : type_value -> ?s:S.type_expression -> unit -> type_value
val t_tuple : type_value list -> ?s:S.type_expression -> unit -> type_value
val t_variable : name -> ?s:S.type_expression -> unit -> type_value
val t_variable : type_name -> ?s:S.type_expression -> unit -> type_value
val t_record : tv_map -> ?s:S.type_expression -> unit -> type_value
val make_t_ez_record : (string * type_value) list -> type_value
(*

View File

@ -296,7 +296,7 @@ let rec assert_type_value_eq (a, b: (type_value * type_value)) : unit result = m
bind_list_iter assert_type_value_eq (List.combine ta tb)
)
| T_tuple _, _ -> fail @@ different_kinds a b
| T_constant (ca, lsta), T_constant (cb, lstb) -> (
| T_constant (Type_name ca, lsta), T_constant (Type_name cb, lstb) -> (
let%bind _ =
trace_strong (different_size_constants a b)
@@ Assert.assert_true List.(length lsta = length lstb) in

View File

@ -5,7 +5,7 @@ module S = Ast_simplified
module SMap = Map.String
type name = string
type type_name = string
type type_name = Type_name of string
type constructor_name = string
type 'a name_map = 'a SMap.t

View File

@ -190,7 +190,7 @@ module Substitution = struct
(* Replace the type variable ~v with ~expr everywhere within the
program ~p. TODO: issues with scoping/shadowing. *)
and program ~(p : Ast_typed.program) ~(v:type_variable) ~expr : Ast_typed.program Trace.result =
and program ~(p : Ast_typed.program) ~(v:string (* this string is a type_name or type_variable I think *)) ~expr : Ast_typed.program Trace.result =
Trace.bind_map_list (s_declaration_wrap ~v ~expr) p
(*