Changes requested in MR review

This commit is contained in:
Suzanne Dupéron 2020-01-28 20:23:11 +00:00
parent 1734d31a41
commit a9a12ae244
11 changed files with 53 additions and 39 deletions

View File

@ -1,45 +1,42 @@
open Solver open Solver
open Format open Format
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_map"
| 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_constraint : _ -> type_constraint_simpl -> unit = fun ppf -> let type_constraint : _ -> type_constraint_simpl -> unit = fun ppf ->
function function
|SC_Constructor { tv; c_tag; tv_list=_ } -> |SC_Constructor { tv; c_tag; tv_list=_ } ->
let ct = c_tag_to_string c_tag in let ct = match c_tag with
| 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_map"
| 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"
in
fprintf ppf "CTOR %a %s()" Var.pp tv ct fprintf ppf "CTOR %a %s()" Var.pp tv ct
|SC_Alias (a, b) -> fprintf ppf "Alias %a %a" Var.pp a Var.pp b |SC_Alias (a, b) -> fprintf ppf "Alias %a %a" Var.pp a Var.pp b
|SC_Poly _ -> fprintf ppf "Poly" |SC_Poly _ -> fprintf ppf "Poly"
|SC_Typeclass _ -> fprintf ppf "TC" |SC_Typeclass _ -> fprintf ppf "TC"
let all_constraints ppf ac = let all_constraints ppf ac =
fprintf ppf "[" ; fprintf ppf "[%a]" (pp_print_list ~pp_sep:(fun ppf () -> fprintf ppf ";\n") type_constraint) ac
pp_print_list ~pp_sep:(fun ppf () -> fprintf ppf ";\n") type_constraint ppf ac ;
fprintf ppf "]"
let aliases ppf (al : unionfind) = let aliases ppf (al : unionfind) =
fprintf ppf "ALIASES %a" UF.print al fprintf ppf "ALIASES %a" UF.print al

View File

@ -489,7 +489,7 @@ module UnionFindWrapper = struct
let dbs = { dbs with aliases } in let dbs = { dbs with aliases } in
(* Replace the two entries in grouped_by_variable by a single one *) (* Replace the two entries in grouped_by_variable by a single one *)
begin (
let get_constraints ab = let get_constraints ab =
match TypeVariableMap.find_opt ab dbs.grouped_by_variable with match TypeVariableMap.find_opt ab dbs.grouped_by_variable with
| Some x -> x | Some x -> x
@ -508,7 +508,7 @@ module UnionFindWrapper = struct
TypeVariableMap.remove variable_repr_b dbs.grouped_by_variable in TypeVariableMap.remove variable_repr_b dbs.grouped_by_variable in
let dbs = { dbs with grouped_by_variable} in let dbs = { dbs with grouped_by_variable} in
dbs dbs
end )
end end
(* sub-sub component: constraint normalizer: remove dupes and give structure (* sub-sub component: constraint normalizer: remove dupes and give structure

View File

@ -1,6 +1,8 @@
open Trace open Trace
open Types open Types
include Stage_common.Misc
module Errors = struct module Errors = struct
let different_literals_because_different_types name a b () = let different_literals_because_different_types name a b () =
let title () = "literals have different types: " ^ name in let title () = "literals have different types: " ^ name in

View File

@ -1,5 +1,8 @@
open Trace open Trace
open Types open Types
include module type of Stage_common.Misc
(* (*
module Errors : sig module Errors : sig

View File

@ -254,7 +254,7 @@ let ez_e_record (lst : (label * ae) list) : expression =
let map = List.fold_left aux LMap.empty lst in let map = List.fold_left aux LMap.empty lst in
e_record map e_record map
let e_some s : expression = E_constant (C_SOME, [s]) let e_some s : expression = E_constant (C_SOME, [s])
let e_none : expression = E_constant (C_NONE, []) let e_none () : expression = E_constant (C_NONE, [])
let e_map lst : expression = E_map lst let e_map lst : expression = E_map lst
@ -290,7 +290,7 @@ let e_a_address s = make_a_e (e_address s) (t_address ())
let e_a_pair a b = make_a_e (e_pair a b) (t_pair a.type_annotation b.type_annotation ()) let e_a_pair a b = make_a_e (e_pair a b) (t_pair a.type_annotation b.type_annotation ())
let e_a_some s = make_a_e (e_some s) (t_option s.type_annotation ()) let e_a_some s = make_a_e (e_some s) (t_option s.type_annotation ())
let e_a_lambda l in_ty out_ty = make_a_e (e_lambda l) (t_function in_ty out_ty ()) let e_a_lambda l in_ty out_ty = make_a_e (e_lambda l) (t_function in_ty out_ty ())
let e_a_none t = make_a_e e_none (t_option t ()) let e_a_none t = make_a_e (e_none ()) (t_option t ())
let e_a_tuple lst = make_a_e (E_tuple lst) (t_tuple (List.map get_type_annotation lst) ()) let e_a_tuple lst = make_a_e (E_tuple lst) (t_tuple (List.map get_type_annotation lst) ())
let e_a_record r = make_a_e (e_record r) (t_record (LMap.map get_type_annotation r) ()) let e_a_record r = make_a_e (e_record r) (t_record (LMap.map get_type_annotation r) ())
let e_a_application a b = make_a_e (e_application a b) (get_type_annotation b) let e_a_application a b = make_a_e (e_application a b) (get_type_annotation b)

View File

@ -111,7 +111,7 @@ val ez_e_record : ( string * annotated_expression ) list -> expression
*) *)
val e_some : value -> expression val e_some : value -> expression
val e_none : expression val e_none : unit -> expression
val e_map : ( value * value ) list -> expression val e_map : ( value * value ) list -> expression
val e_unit : unit -> expression val e_unit : unit -> expression
val e_int : int -> expression val e_int : int -> expression

View File

@ -1,5 +1,6 @@
open Trace open Trace
open Types open Types
include Stage_common.Misc include Stage_common.Misc
module Errors = struct module Errors = struct

View File

@ -1,6 +1,8 @@
open Trace open Trace
open Types open Types
include module type of Stage_common.Misc
val assert_value_eq : ( value * value ) -> unit result val assert_value_eq : ( value * value ) -> unit result
val assert_type_value_eq : ( type_value * type_value ) -> unit result val assert_type_value_eq : ( type_value * type_value ) -> unit result

View File

@ -91,3 +91,4 @@ let string_of_type_expression' = function
| T_constant c -> string_of_type_constant c | T_constant c -> string_of_type_constant c
| T_sum _|T_record _|T_arrow (_, _)|T_variable _ -> | T_sum _|T_record _|T_arrow (_, _)|T_variable _ ->
failwith "not a type operator or constant" failwith "not a type operator or constant"

View File

@ -0,0 +1,9 @@
open Types
val map_type_operator : ('a -> 'b) -> 'a type_operator -> 'b type_operator
val bind_map_type_operator : ('a -> ('b * 'c list, 'd) Pervasives.result) -> 'a type_operator -> ('b type_operator * 'c list, 'd) Pervasives.result
val type_operator_name : 'a type_operator -> string
val type_expression'_of_string : string * 'a list -> ('a type_expression' * 'b list, 'c) Pervasives.result
val string_of_type_operator : 'a type_operator -> string * 'a list
val string_of_type_constant : type_constant -> string * 'a list
val string_of_type_expression' : 'a type_expression' -> string * 'a list

View File

@ -87,8 +87,7 @@ module Substitution = struct
| None -> ok @@ T.T_variable variable | None -> ok @@ T.T_variable variable
end end
| T.T_operator type_name_and_args -> | 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 = T.Misc.bind_map_type_operator (s_type_value ~substs) type_name_and_args in
let%bind type_name_and_args = bind_map_type_operator (s_type_value ~substs) type_name_and_args in
ok @@ T.T_operator type_name_and_args ok @@ T.T_operator type_name_and_args
| T.T_arrow _ -> | T.T_arrow _ ->
let _TODO = substs in let _TODO = substs in
@ -101,7 +100,7 @@ module Substitution = struct
| Ast_simplified.T_variable _ -> failwith "TODO: subst: unimplemented case s_type_expression variable" | Ast_simplified.T_variable _ -> failwith "TODO: subst: unimplemented case s_type_expression variable"
| Ast_simplified.T_operator op -> | Ast_simplified.T_operator op ->
let%bind op = let%bind op =
Stage_common.Misc.bind_map_type_operator (* TODO: write Ast_simplified.Misc.type_operator_name *) Ast_simplified.Misc.bind_map_type_operator
(s_type_expression ~substs) (s_type_expression ~substs)
op in op in
(* TODO: when we have generalized operators, we might need to subst the operator name itself? *) (* TODO: when we have generalized operators, we might need to subst the operator name itself? *)