balsoft/ligo
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Merge branch 'bugfix/new-typer-7' into 'dev'

Browse Source 
bugfix/new typer 7

See merge request ligolang/ligo!366
This commit is contained in:
Suzanne Dupéron 2020-01-28 23:30:53 +00:00
commit 27df6df8bb
33 changed files with 478 additions and 330 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/bin/expect_tests/typer_error_tests.ml
View File

@ -41,7 +41,7 @@ let%expect_test _ =
run_ligo_bad [ "compile-contract" ; "../../test/contracts/negative/error_typer_3.mligo" ; "main" ] ;
[%expect {|
ligo: in file "error_typer_3.mligo", line 3, characters 34-53. tuples have different sizes: Expected these two types to be the same, but they're different (both are tuples, but with a different number of arguments) {"a":"tuple[int , string , bool]","b":"tuple[int , string]"}
ligo: in file "error_typer_3.mligo", line 3, characters 34-53. different number of arguments to type constructors: Expected these two n-ary type constructors to be the same, but they have different numbers of arguments (both use the TC_tuple type constructor, but they have 3 and 2 arguments, respectively) {"a":"(TO_tuple[int , string , bool])","b":"(TO_tuple[int , string])","op":"TC_tuple","len_a":"3","len_b":"2"}
If you're not sure how to fix this error, you can

6
src/main/compile/of_mini_c.ml
View File

@ -9,15 +9,13 @@ let compile_contract : expression -> Compiler.compiled_expression result = fun e
let%bind body = Compiler.Program.translate_function_body body [] input_ty in
let expr = Self_michelson.optimize body in
let%bind expr_ty = Compiler.Type.Ty.type_ e.type_value in
let open! Compiler.Program in
ok { expr_ty ; expr }
ok ({ expr_ty ; expr } : Compiler.Program.compiled_expression)
let compile_expression : expression -> Compiler.compiled_expression result = fun e ->
let%bind expr = Compiler.Program.translate_expression e Compiler.Environment.empty in
let expr = Self_michelson.optimize expr in
let%bind expr_ty = Compiler.Type.Ty.type_ e.type_value in
let open! Compiler.Program in
ok { expr_ty ; expr }
ok ({ expr_ty ; expr } : Compiler.Program.compiled_expression)
let aggregate_and_compile = fun program form ->
let%bind aggregated = aggregate_entry program form in

5
src/main/compile/of_simplified.ml
View File

@ -7,14 +7,15 @@ let compile (program : Ast_simplified.program) : (Ast_typed.program * Typer.Solv
let compile_expression ?(env = Ast_typed.Environment.full_empty) ~(state : Typer.Solver.state) (ae : Ast_simplified.expression)
: (Ast_typed.value * Typer.Solver.state) result =
Typer.type_expression env state ae
let () = Typer.Solver.discard_state state in
Typer.type_expression_subst env state ae
let apply (entry_point : string) (param : Ast_simplified.expression) : Ast_simplified.expression result =
let name = Var.of_name entry_point in
let entry_point_var : Ast_simplified.expression =
{ expression = Ast_simplified.E_variable name ;
location = Virtual "generated entry-point variable" } in
let applied : Ast_simplified.expression =
let applied : Ast_simplified.expression =
{ expression = Ast_simplified.E_application (entry_point_var, param) ;
location = Virtual "generated application" } in
ok applied

4
src/main/compile/of_typed.ml
View File

@ -14,7 +14,7 @@ let assert_equal_contract_type : check_type -> string -> Ast_typed.program -> As
match entry_point.type_annotation.type_value' with
| T_arrow (args,_) -> (
match args.type_value' with
| T_tuple [param_exp;storage_exp] -> (
| T_operator (TC_tuple [param_exp;storage_exp]) -> (
match c with
| Check_parameter -> assert_type_value_eq (param_exp, param.type_annotation)
| Check_storage -> assert_type_value_eq (storage_exp, param.type_annotation)
@ -24,4 +24,4 @@ let assert_equal_contract_type : check_type -> string -> Ast_typed.program -> As
| _ -> dummy_fail )
let pretty_print ppf program =
Ast_typed.PP.program ppf program
Ast_typed.PP.program ppf program

2
src/passes/2-simplify/cameligo.ml
View File

@ -246,7 +246,7 @@ and simpl_list_type_expression (lst:Raw.type_expr list) : type_expression result
| [hd] -> simpl_type_expression hd
| lst ->
let%bind lst = bind_map_list simpl_type_expression lst in
ok @@ make_t @@ T_tuple lst
ok @@ make_t @@ T_operator (TC_tuple lst)
let rec simpl_expression :
Raw.expr -> expr result = fun t ->

14
src/passes/2-simplify/pascaligo.ml
View File

@ -267,7 +267,7 @@ and simpl_list_type_expression (lst:Raw.type_expr list) : type_expression result
| [hd] -> simpl_type_expression hd
| lst ->
let%bind lst = bind_list @@ List.map simpl_type_expression lst in
ok @@ make_t @@ T_tuple lst
ok @@ make_t @@ T_operator (TC_tuple lst)
let simpl_projection : Raw.projection Region.reg -> _ = fun p ->
let (p' , loc) = r_split p in
@ -663,7 +663,7 @@ and simpl_fun_decl :
let arguments_name = Var.of_name "arguments" in
let%bind params = bind_map_list simpl_param lst in
let (binder , input_type) =
let type_expression = T_tuple (List.map snd params) in
let type_expression = t_tuple (List.map snd params) in
(arguments_name , type_expression) in
let%bind tpl_declarations =
let aux = fun i x ->
@ -682,8 +682,8 @@ and simpl_fun_decl :
let aux prec cur = cur (Some prec) in
bind_fold_right_list aux result body in
let expression =
e_lambda ~loc binder (Some (make_t @@ input_type)) (Some output_type) result in
let type_annotation = Some (make_t @@ T_arrow (make_t input_type, output_type)) in
e_lambda ~loc binder (Some input_type) (Some output_type) result in
let type_annotation = Some (make_t @@ T_arrow (input_type, output_type)) in
ok ((Var.of_name fun_name.value, type_annotation), expression)
)
)
@ -717,7 +717,7 @@ and simpl_fun_expression :
let arguments_name = Var.of_name "arguments" in
let%bind params = bind_map_list simpl_param lst in
let (binder , input_type) =
let type_expression = T_tuple (List.map snd params) in
let type_expression = t_tuple (List.map snd params) in
(arguments_name , type_expression) in
let%bind tpl_declarations =
let aux = fun i x ->
@ -736,8 +736,8 @@ and simpl_fun_expression :
let aux prec cur = cur (Some prec) in
bind_fold_right_list aux result body in
let expression =
e_lambda ~loc binder (Some (make_t @@ input_type)) (Some output_type) result in
let type_annotation = Some (make_t @@ T_arrow (make_t input_type, output_type)) in
e_lambda ~loc binder (Some (input_type)) (Some output_type) result in
let type_annotation = Some (make_t @@ T_arrow (input_type, output_type)) in
ok (type_annotation, expression)
)
)

54
src/passes/4-typer-new/PP.ml Normal file
View File

@ -0,0 +1,54 @@
open Solver
open Format
let type_constraint : _ -> type_constraint_simpl -> unit = fun ppf ->
function
|SC_Constructor { tv; c_tag; tv_list=_ } ->
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
|SC_Alias (a, b) -> fprintf ppf "Alias %a %a" Var.pp a Var.pp b
|SC_Poly _ -> fprintf ppf "Poly"
|SC_Typeclass _ -> fprintf ppf "TC"
let all_constraints ppf ac =
fprintf ppf "[%a]" (pp_print_list ~pp_sep:(fun ppf () -> fprintf ppf ";\n") type_constraint) ac
let aliases ppf (al : unionfind) =
fprintf ppf "ALIASES %a" UF.print al
let structured_dbs : _ -> structured_dbs -> unit = fun ppf structured_dbs ->
let { all_constraints = a ; aliases = b ; _ } = structured_dbs in
fprintf ppf "STRUCTURED_DBS\n %a\n %a" all_constraints a aliases b
let already_selected : _ -> already_selected -> unit = fun ppf already_selected ->
let _ = already_selected in
fprintf ppf "ALREADY_SELECTED"
let state : _ -> state -> unit = fun ppf state ->
let { structured_dbs=a ; already_selected=b } = state in
fprintf ppf "STATE %a %a" structured_dbs a already_selected b

125
src/passes/4-typer-new/solver.ml
View File

@ -34,8 +34,6 @@ module Wrap = struct
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 ->
P_constant (C_variant, T.CMap.to_list @@ T.CMap.map type_expression_to_type_value kvmap)
| T_record kvmap ->
@ -64,21 +62,20 @@ module Wrap = struct
P_constant (csttag, [])
| T_operator (type_operator) ->
let (csttag, args) = Core.(match type_operator with
| TC_option o -> (C_option, [o])
| TC_set s -> (C_set, [s])
| TC_map (k,v) -> (C_map, [k;v])
| TC_big_map (k,v) -> (C_big_map, [k;v])
| TC_list l -> (C_list, [l])
| TC_contract c -> (C_contract, [c])
| TC_option o -> (C_option, [o])
| TC_set s -> (C_set, [s])
| TC_map ( k , v ) -> (C_map, [k;v])
| TC_big_map ( k , v) -> (C_big_map, [k;v])
| TC_list l -> (C_list, [l])
| TC_contract c -> (C_contract, [c])
| TC_arrow ( arg , ret ) -> (C_arrow, [ arg ; ret ])
| TC_tuple lst -> (C_tuple, lst)
)
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.type_expression' with
| T_tuple types ->
P_constant (C_tuple, List.map type_expression_to_type_value_copypasted types)
| T_sum kvmap ->
P_constant (C_variant, I.CMap.to_list @@ I.CMap.map type_expression_to_type_value_copypasted kvmap)
| T_record kvmap ->
@ -96,12 +93,14 @@ module Wrap = struct
P_constant (csttag,[])
| T_operator (type_name) ->
let (csttag, args) = Core.(match type_name with
| TC_option o -> (C_option , [o])
| TC_list l -> (C_list , [l])
| TC_set s -> (C_set , [s])
| TC_map (k,v) -> (C_map , [k;v])
| TC_big_map (k,v) -> (C_big_map, [k;v])
| TC_contract c -> (C_contract, [c])
| TC_option o -> (C_option , [o])
| TC_list l -> (C_list , [l])
| TC_set s -> (C_set , [s])
| TC_map ( k , v ) -> (C_map , [k;v])
| TC_big_map ( k , v ) -> (C_big_map, [k;v])
| TC_contract c -> (C_contract, [c])
| TC_arrow ( arg , ret ) -> (C_arrow, [ arg ; ret ])
| TC_tuple lst -> (C_tuple, lst)
)
in
P_constant (csttag, List.map type_expression_to_type_value_copypasted args)
@ -350,7 +349,7 @@ end
module TypeVariable =
struct
type t = Core.type_variable
let compare a b= Var.compare a b
let compare a b = Var.compare a b
let to_string = (fun s -> Format.asprintf "%a" Var.pp s)
end
@ -475,44 +474,69 @@ module UnionFindWrapper = struct
in
let dbs = { dbs with grouped_by_variable } in
dbs
let merge_variables : type_variable -> type_variable -> structured_dbs -> structured_dbs =
let merge_constraints : type_variable -> type_variable -> structured_dbs -> structured_dbs =
fun variable_a variable_b dbs ->
(* get old representant for variable_a *)
let variable_repr_a , aliases = UF.get_or_set variable_a dbs.aliases in
let dbs = { dbs with aliases } in
(* get old representant for variable_b *)
let variable_repr_b , aliases = UF.get_or_set variable_b dbs.aliases in
let dbs = { dbs with aliases } in
let default d = function None -> d | Some y -> y in
let get_constraints ab =
TypeVariableMap.find_opt ab dbs.grouped_by_variable
|> default { constructor = [] ; poly = [] ; tc = [] } in
let constraints_a = get_constraints variable_repr_a in
let constraints_b = get_constraints variable_repr_b in
let all_constraints = {
constructor = constraints_a.constructor @ constraints_b.constructor ;
poly = constraints_a.poly @ constraints_b.poly ;
tc = constraints_a.tc @ constraints_b.tc ;
} in
let grouped_by_variable =
TypeVariableMap.add variable_repr_a all_constraints dbs.grouped_by_variable in
let dbs = { dbs with grouped_by_variable} in
let grouped_by_variable =
TypeVariableMap.remove variable_repr_b dbs.grouped_by_variable in
let dbs = { dbs with grouped_by_variable} in
dbs
(* alias variable_a and variable_b together *)
let aliases = UF.alias variable_a variable_b dbs.aliases in
let dbs = { dbs with aliases } in
(* Replace the two entries in grouped_by_variable by a single one *)
(
let get_constraints ab =
match TypeVariableMap.find_opt ab dbs.grouped_by_variable with
| Some x -> x
| None -> { constructor = [] ; poly = [] ; tc = [] } in
let constraints_a = get_constraints variable_repr_a in
let constraints_b = get_constraints variable_repr_b in
let all_constraints = {
constructor = constraints_a.constructor @ constraints_b.constructor ;
poly = constraints_a.poly @ constraints_b.poly ;
tc = constraints_a.tc @ constraints_b.tc ;
} in
let grouped_by_variable =
TypeVariableMap.add variable_repr_a all_constraints dbs.grouped_by_variable in
let dbs = { dbs with grouped_by_variable} in
let grouped_by_variable =
TypeVariableMap.remove variable_repr_b dbs.grouped_by_variable in
let dbs = { dbs with grouped_by_variable} in
dbs
)
end
(* sub-sub component: constraint normalizer: remove dupes and give structure
* right now: union-find of unification vars
* later: better database-like organisation of knowledge *)
(* Each normalizer returns a *)
(* If implemented in a language with decent sets, should be 'b set not 'b list. *)
(* Each normalizer returns an updated database (after storing the
incoming constraint) and a list of constraints, used when the
normalizer rewrites the constraints e.g. into simpler ones. *)
(* TODO: If implemented in a language with decent sets, should be 'b set not 'b list. *)
type ('a , 'b) normalizer = structured_dbs -> 'a -> (structured_dbs * 'b list)
(** Updates the dbs.all_constraints field when new constraints are
discovered.
This field contains a list of all the constraints, without any form of
grouping or sorting. *)
let normalizer_all_constraints : (type_constraint_simpl , type_constraint_simpl) normalizer =
fun dbs new_constraint ->
({ dbs with all_constraints = new_constraint :: dbs.all_constraints } , [new_constraint])
(** Updates the dbs.grouped_by_variable field when new constraints are
discovered.
This field contains a map from type variables to lists of
constraints that are related to that variable (in other words, the
key appears in the equation).
*)
let normalizer_grouped_by_variable : (type_constraint_simpl , type_constraint_simpl) normalizer =
fun dbs new_constraint ->
let store_constraint tvars constraints =
@ -520,16 +544,18 @@ let normalizer_grouped_by_variable : (type_constraint_simpl , type_constraint_si
UnionFindWrapper.add_constraints_related_to tvar constraints dbs
in List.fold_left aux dbs tvars
in
let merge_constraints a b =
UnionFindWrapper.merge_variables a b dbs in
let dbs = match new_constraint with
SC_Constructor ({tv ; c_tag = _ ; tv_list} as c) -> store_constraint (tv :: tv_list) {constructor = [c] ; poly = [] ; tc = []}
| SC_Typeclass ({tc = _ ; args} as c) -> store_constraint args {constructor = [] ; poly = [] ; tc = [c]}
| SC_Poly ({tv; forall = _} as c) -> store_constraint [tv] {constructor = [] ; poly = [c] ; tc = []}
| SC_Alias (a , b) -> merge_constraints a b
| SC_Alias (a , b) -> UnionFindWrapper.merge_constraints a b dbs
in (dbs , [new_constraint])
(* Stores the first assinment ('a = ctor('b, …)) seen *)
(** Stores the first assinment ('a = ctor('b, …)) that is encountered.
Subsequent ('a = ctor('b2, …)) with the same 'a are ignored.
TOOD: are we checking somewhere that 'b … = 'b2 … ? *)
let normalizer_assignments : (type_constraint_simpl , type_constraint_simpl) normalizer =
fun dbs new_constraint ->
match new_constraint with
@ -540,9 +566,14 @@ let normalizer_assignments : (type_constraint_simpl , type_constraint_simpl) nor
| _ ->
(dbs , [new_constraint])
(** Evaluates a type-leval application. For now, only supports
immediate beta-reduction at the root of the type. *)
let type_level_eval : type_value -> type_value * type_constraint list =
fun tv -> Typesystem.Misc.Substitution.Pattern.eval_beta_root ~tv
(** Checks that a type-level application has been fully reduced. For
now, only some simple cases like applications of `forall`
<polymorphic types are allowed. *)
let check_applied ((reduced, _new_constraints) as x) =
let () = match reduced with
P_apply _ -> failwith "internal error: shouldn't happen" (* failwith "could not reduce type-level application. Arbitrary type-level applications are not supported for now." *)
@ -552,6 +583,14 @@ let check_applied ((reduced, _new_constraints) as x) =
(* TODO: at some point there may be uses of named type aliases (type
foo = int; let x : foo = 42). These should be inlined. *)
(** This function converts constraints from type_constraint to
type_constraint_simpl. The former has more possible cases, and the
latter uses a more minimalistic constraint language.
It does not modify the dbs, and only rewrites the constraint
TODO: update the code to show that the dbs are always copied as-is
*)
let rec normalizer_simpl : (type_constraint , type_constraint_simpl) normalizer =
fun dbs new_constraint ->
let insert_fresh a b =

96
src/passes/4-typer-new/typer.ml
View File

@ -334,9 +334,6 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_value result =
let%bind a' = evaluate_type e a in
let%bind b' = evaluate_type e b in
return (T_arrow (a', b'))
| T_tuple lst ->
let%bind lst' = bind_list @@ List.map (evaluate_type e) lst in
return (T_tuple lst')
| T_sum m ->
let aux k v prev =
let%bind prev' = prev in
@ -382,6 +379,13 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_value result =
| TC_contract c ->
let%bind c = evaluate_type e c in
ok @@ O.TC_contract c
| TC_arrow ( arg , ret ) ->
let%bind arg' = evaluate_type e arg in
let%bind ret' = evaluate_type e ret in
ok @@ O.TC_arrow ( arg' , ret' )
| TC_tuple lst ->
let%bind lst' = bind_map_list (evaluate_type e) lst in
ok @@ O.TC_tuple lst'
in
return (T_operator (opt))
@ -469,10 +473,11 @@ and type_expression : environment -> Solver.state -> ?tv_opt:O.type_value -> I.e
return_wrapped (e_operation o) state @@ Wrap.literal (t_operation ())
)
| E_literal (Literal_unit) -> (
return_wrapped (e_unit) state @@ Wrap.literal (t_unit ())
return_wrapped (e_unit ()) state @@ Wrap.literal (t_unit ())
)
| E_skip -> (
failwith "TODO: missing implementation for E_skip"
(* E_skip just returns unit *)
return_wrapped (e_unit ()) state @@ Wrap.literal (t_unit ())
)
(* | E_literal (Literal_string s) -> (
* L.log (Format.asprintf "literal_string option type: %a" PP_helpers.(option O.PP.type_expression) tv_opt) ;
@ -516,7 +521,6 @@ and type_expression : environment -> Solver.state -> ?tv_opt:O.type_value -> I.e
trace_option error @@
Environment.get_constructor c e in
let%bind (expr' , state') = type_expression e state expr in
let%bind _assert = O.assert_type_value_eq (expr'.type_annotation, c_tv) in
let wrapped = Wrap.constructor expr'.type_annotation c_tv sum_tv in
return_wrapped (E_constructor (c , expr')) state' wrapped
@ -932,9 +936,7 @@ let untype_type_value (t:O.type_value) : (I.type_expression) result =
(*
Apply type_declaration on all the node of the AST_simplified from the root p
*)
let type_program_returns_state (p:I.program) : (environment * Solver.state * O.program) result =
let env = Ast_typed.Environment.full_empty in
let state = Solver.initial_state in
let type_program_returns_state ((env, state, p) : environment * Solver.state * I.program) : (environment * Solver.state * O.program) result =
let aux ((e : environment), (s : Solver.state) , (ds : O.declaration Location.wrap list)) (d:I.declaration Location.wrap) =
let%bind (e' , s' , d'_opt) = type_declaration e s (Location.unwrap d) in
let ds' = match d'_opt with
@ -949,51 +951,45 @@ let type_program_returns_state (p:I.program) : (environment * Solver.state * O.p
let () = ignore (env' , state') in
ok (env', state', declarations)
(* 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 type_and_subst_xyz (env_state_node : environment * Solver.state * 'a) (apply_substs : 'b Typesystem.Misc.Substitution.Pattern.w) (type_xyz_returns_state : (environment * Solver.state * 'a) -> (environment * Solver.state * 'b) Trace.result) : ('b * Solver.state) result =
let%bind (env, state, program) = type_xyz_returns_state env_state_node in
let subst_all =
let aliases = state.structured_dbs.aliases in
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 substs : variable: I.type_variable -> _ = fun ~variable ->
to_option @@
let%bind root =
trace_option (simple_error (Format.asprintf "can't find alias root of variable %a" Var.pp variable)) @@
(* TODO: after upgrading UnionFind, this will be an option, not an exception. *)
try Some (Solver.UF.repr variable aliases) with Not_found -> None in
let%bind assignment =
trace_option (simple_error (Format.asprintf "can't find assignment for root %a" Var.pp root)) @@
(Solver.TypeVariableMap.find_opt root assignments) in
let Solver.{ tv ; c_tag ; tv_list } = assignment 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
ok @@ expr
in
let p = apply_substs ~substs program in
p in
let%bind program = subst_all in
let () = ignore env in (* TODO: shouldn't we use the `env` somewhere? *)
ok (program, state)
let type_program (p : I.program) : (O.program * Solver.state) result =
let empty_env = Ast_typed.Environment.full_empty in
let empty_state = Solver.initial_state in
type_and_subst_xyz (empty_env , empty_state , p) Typesystem.Misc.Substitution.Pattern.s_program type_program_returns_state
let type_expression_returns_state : (environment * Solver.state * I.expression) -> (environment * Solver.state * O.annotated_expression) Trace.result =
fun (env, state, e) ->
let%bind (e , state) = type_expression env state e in
ok (env, state, e)
let type_expression_subst (env : environment) (state : Solver.state) ?(tv_opt : O.type_value option) (e : I.expression) : (O.annotated_expression * Solver.state) result =
let () = ignore tv_opt in (* For compatibility with the old typer's API, this argument can be removed once the new typer is used. *)
type_and_subst_xyz (env , state , e) Typesystem.Misc.Substitution.Pattern.s_annotated_expression type_expression_returns_state
(*
TODO: Similar to type_program but use a fold_map_list and List.fold_left and add element to the left or the list which gives a better complexity
*)
@ -1021,9 +1017,6 @@ let type_program' : I.program -> O.program result = fun p ->
let rec untype_type_expression (t:O.type_value) : (I.type_expression) result =
(* TODO: or should we use t.simplified if present? *)
let%bind t = match t.type_value' with
| O.T_tuple x ->
let%bind x' = bind_map_list untype_type_expression x in
ok @@ I.T_tuple x'
| O.T_sum x ->
let%bind x' = I.bind_map_cmap untype_type_expression x in
ok @@ I.T_sum x'
@ -1059,6 +1052,13 @@ let rec untype_type_expression (t:O.type_value) : (I.type_expression) result =
| O.TC_contract c->
let%bind c = untype_type_expression c in
ok @@ I.TC_contract c
| O.TC_arrow ( arg , ret ) ->
let%bind arg' = untype_type_expression arg in
let%bind ret' = untype_type_expression ret in
ok @@ I.TC_arrow ( arg' , ret' )
| O.TC_tuple lst ->
let%bind lst' = bind_map_list untype_type_expression lst in
ok @@ I.TC_tuple lst'
in
ok @@ I.T_operator (type_name)
in

1
src/passes/4-typer-new/typer.mli
View File

@ -44,6 +44,7 @@ val type_declaration : environment -> Solver.state -> I.declaration -> (environm
(* val type_match : (environment -> 'i -> 'o result) -> environment -> O.type_value -> 'i I.matching -> I.expression -> Location.t -> 'o O.matching result *)
val evaluate_type : environment -> I.type_expression -> O.type_value result
val type_expression : environment -> Solver.state -> ?tv_opt:O.type_value -> I.expression -> (O.annotated_expression * Solver.state) result
val type_expression_subst : environment -> Solver.state -> ?tv_opt:O.type_value -> I.expression -> (O.annotated_expression * Solver.state) result
val type_constant : I.constant -> O.type_value list -> O.type_value option -> (O.constant * O.type_value) result
(*
val untype_type_value : O.type_value -> (I.type_expression) result

10
src/passes/4-typer-old/typer.ml
View File

@ -327,9 +327,6 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_value result =
let%bind a' = evaluate_type e a in
let%bind b' = evaluate_type e b in
return (T_arrow (a', b'))
| T_tuple lst ->
let%bind lst' = bind_list @@ List.map (evaluate_type e) lst in
return (T_tuple lst')
| T_sum m ->
let aux k v prev =
let%bind prev' = prev in
@ -375,6 +372,13 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_value result =
| TC_contract c ->
let%bind c = evaluate_type e c in
ok @@ I.TC_contract c
| TC_arrow ( arg , ret ) ->
let%bind arg' = evaluate_type e arg in
let%bind ret' = evaluate_type e ret in
ok @@ I.TC_arrow ( arg' , ret' )
| TC_tuple lst ->
let%bind lst' = bind_map_list (evaluate_type e) lst in
ok @@ I.TC_tuple lst'
in
return (T_operator (opt))

2
src/passes/4-typer/typer.ml
View File

@ -10,5 +10,5 @@ module Solver = Typer_new.Solver (* Both the old typer and the new typer use the
type environment = Environment.t
let type_program = if use_new_typer then Typer_new.type_program else Typer_old.type_program
let type_expression = if use_new_typer then Typer_new.type_expression else Typer_old.type_expression
let type_expression_subst = if use_new_typer then Typer_new.type_expression_subst else Typer_old.type_expression (* the old typer does not have unification variables that would need substitution, so no need to "subst" anything. *)
let untype_expression = if use_new_typer then Typer_new.untype_expression else Typer_old.untype_expression

2
src/passes/4-typer/typer.mli
View File

@ -12,5 +12,5 @@ module Solver = Typer_new.Solver
type environment = Environment.t
val type_program : I.program -> (O.program * Solver.state) result
val type_expression : environment -> Solver.state -> ?tv_opt:O.type_value -> I.expression -> (O.annotated_expression * Solver.state) result
val type_expression_subst : environment -> Solver.state -> ?tv_opt:O.type_value -> I.expression -> (O.annotated_expression * Solver.state) result
val untype_expression : O.annotated_expression -> I.expression result

11
src/passes/6-transpiler/transpiler.ml
View File

@ -146,6 +146,11 @@ let rec transpile_type (t:AST.type_value) : type_value result =
| T_operator (TC_option o) ->
let%bind o' = transpile_type o in
ok (T_option o')
| T_operator (TC_arrow (param , result)) -> (
let%bind param' = transpile_type param in
let%bind result' = transpile_type result in
ok (T_function (param', result'))
)
(* TODO hmm *)
| T_sum m ->
let node = Append_tree.of_list @@ kv_list_of_cmap m in
@ -173,7 +178,7 @@ let rec transpile_type (t:AST.type_value) : type_value result =
ok (Some ann, a))
aux node in
ok @@ snd m'
| T_tuple lst ->
| T_operator (TC_tuple lst) ->
let node = Append_tree.of_list lst in
let aux a b : type_value result =
let%bind a = a in
@ -320,7 +325,7 @@ and transpile_annotated_expression (ae:AST.annotated_expression) : expression re
| E_tuple_accessor (tpl, ind) -> (
let%bind ty' = transpile_type tpl.type_annotation in
let%bind ty_lst =
trace_strong (corner_case ~loc:__LOC__ "not a tuple") @@
trace_strong (corner_case ~loc:__LOC__ "transpiler: E_tuple_accessor: not a tuple") @@
get_t_tuple tpl.type_annotation in
let%bind ty'_lst = bind_map_list transpile_type ty_lst in
let%bind path =
@ -505,7 +510,7 @@ and transpile_annotated_expression (ae:AST.annotated_expression) : expression re
match cur with
| Access_tuple ind -> (
let%bind ty_lst =
trace_strong (corner_case ~loc:__LOC__ "not a tuple") @@
trace_strong (corner_case ~loc:__LOC__ "transpiler: E_assign: Access_tuple: not a tuple") @@
AST.Combinators.get_t_tuple prev in
let%bind ty'_lst = bind_map_list transpile_type ty_lst in
let%bind path = tuple_access_to_lr ty' ty'_lst ind in

35
src/passes/6-transpiler/untranspiler.ml
View File

@ -36,15 +36,6 @@ them. please report this to the developers." in
] in
error ~data title content
let unknown_untranspile unknown_type value =
let title () = "untranspiling unknown value" in
let content () = Format.asprintf "can not untranspile %s" unknown_type in
let data = [
("unknown_type" , fun () -> unknown_type) ;
("value" , fun () -> Format.asprintf "%a" Mini_c.PP.value value) ;
] in
error ~data title content
end
open Errors
@ -196,6 +187,22 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression
)
| TC_contract _ ->
fail @@ bad_untranspile "contract" v
| TC_arrow _ -> (
let%bind n =
trace_strong (wrong_mini_c_value "lambda as string" v) @@
get_string v in
return (E_literal (Literal_string n))
)
| TC_tuple lst ->
let%bind node = match Append_tree.of_list lst with
| Empty -> fail @@ corner_case ~loc:__LOC__ "empty tuple"
| Full t -> ok t in
let%bind tpl =
trace_strong (corner_case ~loc:__LOC__ "tuple extract") @@
extract_tuple v node in
let%bind tpl' = bind_list
@@ List.map (fun (x, y) -> untranspile x y) tpl in
return (E_tuple tpl')
)
| T_sum m ->
let lst = kv_list_of_cmap m in
@ -208,16 +215,6 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression
extract_constructor v node in
let%bind sub = untranspile v tv in
return (E_constructor (Constructor name, sub))
| T_tuple lst ->
let%bind node = match Append_tree.of_list lst with
| Empty -> fail @@ corner_case ~loc:__LOC__ "empty tuple"
| Full t -> ok t in
let%bind tpl =
trace_strong (corner_case ~loc:__LOC__ "tuple extract") @@
extract_tuple v node in
let%bind tpl' = bind_list
@@ List.map (fun (x, y) -> untranspile x y) tpl in
return (E_tuple tpl')
| T_record m ->
let lst = kv_list_of_lmap m in
let%bind node = match Append_tree.of_list lst with

2
src/stages/ast_simplified/PP.ml
View File

@ -18,7 +18,7 @@ and type_expression ppf (te: type_expression) : unit =
te' ppf te.type_expression'
let rec expression ppf (e:expression) = match e.expression with
| E_literal l -> literal ppf l
| E_literal l -> fprintf ppf "%a" literal l
| E_variable n -> fprintf ppf "%a" name n
| E_application (f, arg) -> fprintf ppf "(%a)@(%a)" expression f expression arg
| E_constructor (c, ae) -> fprintf ppf "%a(%a)" constructor c expression ae

4
src/stages/ast_simplified/combinators.ml
View File

@ -36,7 +36,7 @@ let t_key_hash : type_expression = make_t @@ T_constant (TC_key_hash)
let t_option o : type_expression = make_t @@ T_operator (TC_option o)
let t_list t : type_expression = make_t @@ T_operator (TC_list t)
let t_variable n : type_expression = make_t @@ T_variable (Var.of_name n)
let t_tuple lst : type_expression = make_t @@ T_tuple lst
let t_tuple lst : type_expression = make_t @@ T_operator (TC_tuple lst)
let t_pair (a , b) : type_expression = t_tuple [a ; b]
let t_record_ez lst =
let lst = List.map (fun (k, v) -> (Label k, v)) lst in
@ -206,7 +206,7 @@ let get_e_list = fun t ->
let get_e_tuple = fun t ->
match t with
| E_tuple lst -> ok lst
| _ -> simple_fail "not a tuple"
| _ -> simple_fail "ast_simplified: get_e_tuple: not a tuple"
let extract_pair : expression -> (expression * expression) result = fun e ->
match e.expression with

2
src/stages/ast_simplified/combinators.mli
View File

@ -27,8 +27,8 @@ val t_option : type_expression -> type_expression
*)
val t_list : type_expression -> type_expression
val t_variable : string -> type_expression
(*
val t_tuple : type_expression list -> type_expression
(*
val t_record : te_map -> type_expression
*)
val t_pair : ( type_expression * type_expression ) -> type_expression

2
src/stages/ast_simplified/misc.ml
View File

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

5
src/stages/ast_simplified/misc.mli
View File

@ -1,5 +1,8 @@
open Trace
open Types
include module type of Stage_common.Misc
(*
module Errors : sig
@ -15,4 +18,4 @@ val assert_literal_eq : ( literal * literal ) -> unit result
val assert_value_eq : ( expression * expression ) -> unit result
val is_value_eq : ( expression * expression ) -> bool
val is_value_eq : ( expression * expression ) -> bool

15
src/stages/ast_typed/PP.ml
View File

@ -15,13 +15,12 @@ and type_value ppf (tv:type_value) : unit =
let rec annotated_expression ppf (ae:annotated_expression) : unit =
match ae.type_annotation.simplified with
| Some _ -> fprintf ppf "@[<v>%a:%a@]" expression ae.expression type_value ae.type_annotation
| _ -> fprintf ppf "@[<v>%a@]" expression ae.expression
| _ -> fprintf ppf "@[<v>%a:%a@]" expression ae.expression type_value ae.type_annotation
and lambda ppf l =
let ({ binder ; body } : lambda) = l in
fprintf ppf "lambda (%a) -> %a"
name binder
fprintf ppf "(lambda (%a) -> %a)"
name binder
annotated_expression body
and option_inline ppf inline =
@ -33,9 +32,9 @@ and option_inline ppf inline =
and expression ppf (e:expression) : unit =
match e with
| E_literal l -> Stage_common.PP.literal ppf l
| E_constant (b, lst) -> fprintf ppf "%a(%a)" constant b (list_sep_d annotated_expression) lst
| E_constructor (c, lst) -> fprintf ppf "%a(%a)" constructor c annotated_expression lst
| E_variable a -> fprintf ppf "%a" name a
| E_constant (b, lst) -> fprintf ppf "(e_constant %a(%a))" constant b (list_sep_d annotated_expression) lst
| E_constructor (c, lst) -> fprintf ppf "(e_constructor %a(%a))" constructor c annotated_expression lst
| E_variable a -> fprintf ppf "(e_var %a)" name a
| E_application (f, arg) -> fprintf ppf "(%a) (%a)" annotated_expression f annotated_expression arg
| E_lambda l -> fprintf ppf "%a" lambda l
| E_tuple_accessor (ae, i) -> fprintf ppf "%a.%d" annotated_expression ae i
@ -50,7 +49,7 @@ and expression ppf (e:expression) : unit =
| E_look_up (ds, i) -> fprintf ppf "(%a)[%a]" annotated_expression ds annotated_expression i
| E_matching (ae, m) ->
fprintf ppf "match %a with %a" annotated_expression ae (matching annotated_expression) m
| E_sequence (a , b) -> fprintf ppf "%a ; %a" annotated_expression a annotated_expression b
| E_sequence (a , b) -> fprintf ppf "(e_seq %a ; %a)" annotated_expression a annotated_expression b
| E_loop (expr , body) -> fprintf ppf "while %a { %a }" annotated_expression expr annotated_expression body
| E_assign (name , path , expr) ->
fprintf ppf "%a.%a := %a"

15
src/stages/ast_typed/combinators.ml
View File

@ -48,7 +48,7 @@ let t_mutez ?s () : type_value = make_t (T_constant TC_mutez) s
let t_timestamp ?s () : type_value = make_t (T_constant TC_timestamp) s
let t_unit ?s () : type_value = make_t (T_constant TC_unit) s
let t_option o ?s () : type_value = make_t (T_operator (TC_option o)) s
let t_tuple lst ?s () : type_value = make_t (T_tuple lst) s
let t_tuple lst ?s () : type_value = make_t (T_operator (TC_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_operator (TC_list t)) s
let t_set t ?s () : type_value = make_t (T_operator (TC_set t)) s
@ -147,11 +147,11 @@ let get_t_key_hash (t:type_value) : unit result = match t.type_value' with
| _ -> fail @@ Errors.not_a_x_type "key_hash" t ()
let get_t_tuple (t:type_value) : type_value list result = match t.type_value' with
| T_tuple lst -> ok lst
| T_operator (TC_tuple lst) -> ok lst
| _ -> fail @@ Errors.not_a_x_type "tuple" t ()
let get_t_pair (t:type_value) : (type_value * type_value) result = match t.type_value' with
| T_tuple lst ->
| T_operator (TC_tuple lst) ->
let%bind () =
trace_strong (Errors.not_a_x_type "pair (tuple with two elements)" t ()) @@
Assert.assert_list_size lst 2 in
@ -160,6 +160,7 @@ let get_t_pair (t:type_value) : (type_value * type_value) result = match t.type_
let get_t_function (t:type_value) : (type_value * type_value) result = match t.type_value' with
| T_arrow (a,r) -> ok (a,r)
| T_operator (TC_arrow (a , b)) -> ok (a , b)
| _ -> fail @@ Errors.not_a_x_type "function" t ()
let get_t_sum (t:type_value) : type_value constructor_map result = match t.type_value' with
@ -253,11 +254,11 @@ let ez_e_record (lst : (label * ae) list) : expression =
let map = List.fold_left aux LMap.empty lst in
e_record map
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_unit : expression = E_literal (Literal_unit)
let e_unit () : expression = E_literal (Literal_unit)
let e_int n : expression = E_literal (Literal_int n)
let e_nat n : expression = E_literal (Literal_nat n)
let e_mutez n : expression = E_literal (Literal_mutez n)
@ -279,7 +280,7 @@ let e_list lst : expression = E_list lst
let e_let_in binder inline rhs result = E_let_in { binder ; rhs ; result; inline }
let e_tuple lst : expression = E_tuple lst
let e_a_unit = make_a_e e_unit (t_unit ())
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_mutez ())
@ -289,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_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_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_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)

4
src/stages/ast_typed/combinators.mli
View File

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

37
src/stages/ast_typed/misc.ml
View File

@ -1,5 +1,6 @@
open Trace
open Types
include Stage_common.Misc
module Errors = struct
@ -29,6 +30,21 @@ module Errors = struct
] in
error ~data title message ()
let different_operator_number_of_arguments opa opb lena lenb () =
let title = (thunk "different number of arguments to type constructors") in
assert (String.equal (type_operator_name opa) (type_operator_name opb));
let message () = Format.asprintf
"Expected these two n-ary type constructors to be the same, but they have different numbers of arguments (both use the %s type constructor, but they have %d and %d arguments, respectively)"
(type_operator_name opa) lena lenb in
let data = [
("a" , fun () -> Format.asprintf "%a" (Stage_common.PP.type_operator PP.type_value) opa) ;
("b" , fun () -> Format.asprintf "%a" (Stage_common.PP.type_operator PP.type_value) opb) ;
("op" , fun () -> type_operator_name opa) ;
("len_a" , fun () -> Format.asprintf "%d" lena) ;
("len_b" , fun () -> Format.asprintf "%d" lenb) ;
] in
error ~data title message ()
let different_size_type name a b () =
let title () = name ^ " have different sizes" in
let message () = "Expected these two types to be the same, but they're different (both are " ^ name ^ ", but with a different number of arguments)" in
@ -49,8 +65,6 @@ module Errors = struct
let _different_size_constants = different_size_type "type constructors"
let different_size_tuples = different_size_type "tuples"
let different_size_sums = different_size_type "sums"
let different_size_records = different_size_type "records"
@ -301,13 +315,6 @@ open Errors
let rec assert_type_value_eq (a, b: (type_value * type_value)) : unit result = match (a.type_value', b.type_value') with
| T_tuple ta, T_tuple tb -> (
let%bind _ =
trace_strong (fun () -> (different_size_tuples a b ()))
@@ Assert.assert_true List.(length ta = length tb) in
bind_list_iter assert_type_value_eq (List.combine ta tb)
)
| T_tuple _, _ -> fail @@ different_kinds a b
| T_constant ca, T_constant cb -> (
trace_strong (different_constants ca cb)
@@ Assert.assert_true (ca = cb)
@ -321,10 +328,16 @@ let rec assert_type_value_eq (a, b: (type_value * type_value)) : unit result = m
| TC_set la, TC_set lb -> ok @@ ([la], [lb])
| TC_map (ka,va), TC_map (kb,vb)
| TC_big_map (ka,va), TC_big_map (kb,vb) -> ok @@ ([ka;va] ,[kb;vb])
| _,_ -> fail @@ different_operators opa opb
| TC_tuple lsta, TC_tuple lstb -> ok @@ (lsta , lstb)
| TC_arrow (froma , toa) , TC_arrow (fromb , tob) -> ok @@ ([froma;toa] , [fromb;tob])
| (TC_option _ | TC_list _ | TC_contract _ | TC_set _ | TC_map _ | TC_big_map _ | TC_tuple _ | TC_arrow _),
(TC_option _ | TC_list _ | TC_contract _ | TC_set _ | TC_map _ | TC_big_map _ | TC_tuple _ | TC_arrow _) -> fail @@ different_operators opa opb
in
trace (different_types "arguments to type operators" a b)
@@ bind_list_iter (fun (a,b) -> assert_type_value_eq (a,b) )(List.combine lsta lstb)
if List.length lsta <> List.length lstb then
fail @@ different_operator_number_of_arguments opa opb (List.length lsta) (List.length lstb)
else
trace (different_types "arguments to type operators" a b)
@@ bind_list_iter (fun (a,b) -> assert_type_value_eq (a,b) )(List.combine lsta lstb)
)
| T_operator _, _ -> fail @@ different_kinds a b
| T_sum sa, T_sum sb -> (

3
src/stages/ast_typed/misc.mli
View File

@ -1,6 +1,8 @@
open Trace
open Types
include module type of Stage_common.Misc
val assert_value_eq : ( value * value ) -> unit result
val assert_type_value_eq : ( type_value * type_value ) -> unit result
@ -43,7 +45,6 @@ module Errors : sig
val different_size_type : name -> type_value -> type_value -> unit -> error
val different_props_in_record : string -> string -> unit -> error
val different_size_constants : type_value -> type_value -> unit -> error
val different_size_tuples : type_value -> type_value -> unit -> error
val different_size_sums : type_value -> type_value -> unit -> error
val different_size_records : type_value -> type_value -> unit -> error
val different_types : name -> type_value -> type_value -> unit -> error

11
src/stages/ast_typed/types.ml
View File

@ -18,7 +18,7 @@ and environment_element_definition =
and free_variables = expression_variable list
and environment_element = {
type_value : type_value ;
type_value : type_value ;
source_environment : full_environment ;
definition : environment_element_definition ;
}
@ -34,6 +34,12 @@ and annotated_expression = {
location : Location.t ;
}
(* This seems to be used only for top-level declarations, and
represents the name of the top-level binding, and the expression
assigned to it. -- Suzanne.
TODO: if this is correct, then we should inline this in
"declaration" or at least move it close to it. *)
and named_expression = {
name: expression_variable ;
annotated_expression: ae ;
@ -41,6 +47,7 @@ and named_expression = {
and ae = annotated_expression
and type_value' = type_value type_expression'
and type_value = {
type_value' : type_value';
simplified : S.type_expression option ; (* If we have the simplified this AST fragment comes from, it is stored here, for easier untyping. *)
@ -77,7 +84,7 @@ and 'a expression' =
| E_application of (('a) * ('a))
| E_lambda of lambda
| E_let_in of let_in
(* Tuple *)
(* Tuple, TODO: remove tuples and use records with integer keys instead *)
| E_tuple of ('a) list
| E_tuple_accessor of (('a) * int) (* Access n'th tuple's element *)
(* Sum *)

3
src/stages/common/PP.ml
View File

@ -141,7 +141,6 @@ let lmap_sep_d x = lmap_sep x (const " , ")
let rec type_expression' : type a . (formatter -> a -> unit) -> formatter -> a type_expression' -> unit =
fun f ppf te ->
match te with
| T_tuple lst -> fprintf ppf "tuple[%a]" (list_sep_d f) lst
| T_sum m -> fprintf ppf "sum[%a]" (cmap_sep_d f) m
| T_record m -> fprintf ppf "record[%a]" (lmap_sep_d f ) m
| T_arrow (a, b) -> fprintf ppf "%a -> %a" f a f b
@ -178,6 +177,8 @@ and type_operator : type a . (formatter -> a -> unit) -> formatter -> a type_ope
| TC_map (k, v) -> Format.asprintf "Map (%a,%a)" f k f v
| TC_big_map (k, v) -> Format.asprintf "Big Map (%a,%a)" f k f v
| TC_contract (c) -> Format.asprintf "Contract (%a)" f c
| TC_arrow (a , b) -> Format.asprintf "TC_Arrow (%a,%a)" f a f b
| TC_tuple lst -> Format.asprintf "tuple[%a]" (list_sep_d f) lst
in
fprintf ppf "(TO_%s)" s

15
src/stages/common/misc.ml
View File

@ -7,7 +7,9 @@ let map_type_operator f = function
| 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)
| TC_big_map (x , y) -> TC_big_map (f x , f y)
| TC_arrow (x , y) -> TC_arrow (f x , f y)
| TC_tuple lst -> TC_tuple (List.map f lst)
let bind_map_type_operator f = function
TC_contract x -> let%bind x = f x in ok @@ TC_contract x
@ -15,7 +17,9 @@ let bind_map_type_operator f = function
| 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)
| TC_big_map (x , y) -> let%bind x = f x in let%bind y = f y in ok @@ TC_big_map (x , y)
| TC_arrow (x , y) -> let%bind x = f x in let%bind y = f y in ok @@ TC_arrow (x , y)
| TC_tuple lst -> let%bind lst = bind_map_list f lst in ok @@ TC_tuple lst
let type_operator_name = function
TC_contract _ -> "TC_contract"
@ -24,6 +28,8 @@ let type_operator_name = function
| TC_set _ -> "TC_set"
| TC_map _ -> "TC_map"
| TC_big_map _ -> "TC_big_map"
| TC_arrow _ -> "TC_arrow"
| TC_tuple _ -> "TC_tuple"
let type_expression'_of_string = function
| "TC_contract" , [x] -> ok @@ T_operator(TC_contract x)
@ -61,6 +67,8 @@ let string_of_type_operator = function
| TC_set x -> "TC_set" , [x]
| TC_map (x , y) -> "TC_map" , [x ; y]
| TC_big_map (x , y) -> "TC_big_map" , [x ; y]
| TC_arrow (x , y) -> "TC_arrow" , [x ; y]
| TC_tuple lst -> "TC_tuple" , lst
let string_of_type_constant = function
| TC_unit -> "TC_unit", []
@ -81,5 +89,6 @@ let string_of_type_constant = function
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 _ ->
| T_sum _|T_record _|T_arrow (_, _)|T_variable _ ->
failwith "not a type operator or constant"

9
src/stages/common/misc.mli Normal file
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

3
src/stages/common/types.ml
View File

@ -66,7 +66,6 @@ and literal =
(* The ast is a tree of node, 'a is the type of the node (type_variable or {type_variable, previous_type}) *)
type 'a type_expression' =
| T_tuple of 'a list
| T_sum of 'a constructor_map
| T_record of 'a label_map
| T_arrow of 'a * 'a
@ -96,6 +95,8 @@ and 'a type_operator =
| TC_set of 'a
| TC_map of 'a * 'a
| TC_big_map of 'a * 'a
| TC_arrow of 'a * 'a
| TC_tuple of 'a list
type type_base =
| Base_unit

291
src/stages/typesystem/misc.ml
View File

@ -3,120 +3,122 @@ open Core
let pair_map = fun f (x , y) -> (f x , f y)
module Substitution = struct
module Pattern = struct
open Trace
module T = Ast_typed
(* module TSMap = Trace.TMap(String) *)
type 'a w = 'a -> 'a result
type substs = variable:type_variable -> T.type_value' option (* this string is a type_name or type_variable I think *)
let mk_substs ~v ~expr = (v , expr)
type 'a w = substs:substs -> 'a -> 'a result
let rec rec_yes = true
and s_environment_element_definition ~v ~expr = function
and s_environment_element_definition ~substs = function
| T.ED_binder -> ok @@ T.ED_binder
| T.ED_declaration (val_, free_variables) ->
let%bind val_ = s_annotated_expression ~v ~expr val_ in
let%bind free_variables = bind_map_list (s_variable ~v ~expr) free_variables in
let%bind val_ = s_annotated_expression ~substs val_ in
let%bind free_variables = bind_map_list (s_variable ~substs) free_variables in
ok @@ T.ED_declaration (val_, free_variables)
and s_environment ~v ~expr : T.environment w = fun env ->
and s_environment : T.environment w = fun ~substs env ->
bind_map_list (fun (variable, T.{ type_value; source_environment; definition }) ->
let%bind variable = s_variable ~v ~expr variable in
let%bind type_value = s_type_value ~v ~expr type_value in
let%bind source_environment = s_full_environment ~v ~expr source_environment in
let%bind definition = s_environment_element_definition ~v ~expr definition in
let%bind variable = s_variable ~substs variable in
let%bind type_value = s_type_value ~substs type_value in
let%bind source_environment = s_full_environment ~substs source_environment in
let%bind definition = s_environment_element_definition ~substs definition in
ok @@ (variable, T.{ type_value; source_environment; definition })) env
and s_type_environment ~v ~expr : T.type_environment w = fun tenv ->
and s_type_environment : T.type_environment w = fun ~substs tenv ->
bind_map_list (fun (type_variable , type_value) ->
let%bind type_variable = s_type_variable ~v ~expr type_variable in
let%bind type_value = s_type_value ~v ~expr type_value in
let%bind type_variable = s_type_variable ~substs type_variable in
let%bind type_value = s_type_value ~substs type_value in
ok @@ (type_variable , type_value)) tenv
and s_small_environment ~v ~expr : T.small_environment w = fun (environment, type_environment) ->
let%bind environment = s_environment ~v ~expr environment in
let%bind type_environment = s_type_environment ~v ~expr type_environment in
and s_small_environment : T.small_environment w = fun ~substs (environment, type_environment) ->
let%bind environment = s_environment ~substs environment in
let%bind type_environment = s_type_environment ~substs type_environment in
ok @@ (environment, type_environment)
and s_full_environment ~v ~expr : T.full_environment w = fun (a , b) ->
let%bind a = s_small_environment ~v ~expr a in
let%bind b = bind_map_list (s_small_environment ~v ~expr) b in
and s_full_environment : T.full_environment w = fun ~substs (a , b) ->
let%bind a = s_small_environment ~substs a in
let%bind b = bind_map_list (s_small_environment ~substs) b in
ok (a , b)
and s_variable ~v ~expr : T.expression_variable w = fun var ->
let () = ignore (v, expr) in
and s_variable : T.expression_variable w = fun ~substs var ->
let () = ignore @@ substs in
ok var
and s_type_variable ~v ~expr : T.type_variable w = fun tvar ->
let _TODO = ignore (v, expr) in
and s_type_variable : T.type_variable w = fun ~substs tvar ->
let _TODO = ignore @@ substs in
Printf.printf "TODO: subst: unimplemented case s_type_variable";
ok @@ tvar
(* if String.equal tvar v then
* expr
* else
* ok tvar *)
and s_label ~v ~expr : T.label w = fun l ->
let () = ignore (v, expr) in
and s_label : T.label w = fun ~substs l ->
let () = ignore @@ substs in
ok l
and s_build_in ~v ~expr : T.constant w = fun b ->
let () = ignore (v, expr) in
and s_build_in : T.constant w = fun ~substs b ->
let () = ignore @@ substs in
ok b
and s_constructor ~v ~expr : T.constructor w = fun c ->
let () = ignore (v, expr) in
and s_constructor : T.constructor w = fun ~substs c ->
let () = ignore @@ substs in
ok c
and s_type_name_constant ~v ~expr : T.type_constant w = fun type_name ->
and s_type_name_constant : T.type_constant w = fun ~substs type_name ->
(* TODO: we don't need to subst anything, right? *)
let () = ignore (v , expr) in
let () = ignore @@ substs in
ok @@ type_name
and s_type_value' ~v ~expr : T.type_value' w = function
| T.T_tuple type_value_list ->
let%bind type_value_list = bind_map_list (s_type_value ~v ~expr) type_value_list in
ok @@ T.T_tuple type_value_list
and s_type_value' : T.type_value' w = fun ~substs -> function
| T.T_operator (TC_tuple type_value_list) ->
let%bind type_value_list = bind_map_list (s_type_value ~substs) type_value_list in
ok @@ T.T_operator (TC_tuple type_value_list)
| T.T_sum _ -> failwith "TODO: T_sum"
| T.T_record _ -> failwith "TODO: T_record"
| T.T_constant (type_name) ->
let%bind type_name = s_type_name_constant ~v ~expr type_name in
| T.T_constant type_name ->
let%bind type_name = s_type_name_constant ~substs type_name in
ok @@ T.T_constant (type_name)
| 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
begin
match substs ~variable with
| Some expr -> s_type_value' ~substs expr (* TODO: is it the right thing to recursively examine this? We mustn't go into an infinite loop. *)
| None -> ok @@ T.T_variable variable
end
| T.T_operator type_name_and_args ->
let%bind type_name_and_args = T.Misc.bind_map_type_operator (s_type_value ~substs) type_name_and_args in
ok @@ T.T_operator type_name_and_args
| T.T_arrow _ ->
let _TODO = (v, expr) in
let _TODO = substs in
failwith "TODO: T_function"
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 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' : _ Ast_simplified.type_expression' w = fun ~substs -> function
| 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 =
Ast_simplified.Misc.bind_map_type_operator
(s_type_expression ~substs)
op in
(* TODO: when we have generalized operators, we might need to subst the operator name itself? *)
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
and s_type_expression : Ast_simplified.type_expression w = fun ~substs {type_expression'} ->
let%bind type_expression' = s_type_expression' ~substs 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
let%bind simplified = bind_map_option (s_type_expression ~v ~expr) simplified in
and s_type_value : T.type_value w = fun ~substs { type_value'; simplified } ->
let%bind type_value' = s_type_value' ~substs type_value' in
let%bind simplified = bind_map_option (s_type_expression ~substs) simplified in
ok @@ T.{ type_value'; simplified }
and s_literal ~v ~expr : T.literal w = function
and s_literal : T.literal w = fun ~substs -> function
| T.Literal_unit ->
let () = ignore (v, expr) in
let () = ignore @@ substs in
ok @@ T.Literal_unit
| (T.Literal_bool _ as x)
| (T.Literal_int _ as x)
@ -132,144 +134,145 @@ module Substitution = struct
| (T.Literal_chain_id _ as x)
| (T.Literal_operation _ as x) ->
ok @@ x
and s_matching_expr ~v ~expr : T.matching_expr w = fun _ ->
let _TODO = v, expr in
and s_matching_expr : T.matching_expr w = fun ~substs _ ->
let _TODO = substs in
failwith "TODO: subst: unimplemented case s_matching"
and s_named_type_value ~v ~expr : T.named_type_value w = fun _ ->
let _TODO = v, expr in
and s_named_type_value : T.named_type_value w = fun ~substs _ ->
let _TODO = substs in
failwith "TODO: subst: unimplemented case s_named_type_value"
and s_access_path ~v ~expr : T.access_path w = fun _ ->
let _TODO = v, expr in
and s_access_path : T.access_path w = fun ~substs _ ->
let _TODO = substs in
failwith "TODO: subst: unimplemented case s_access_path"
and s_expression ~v ~expr : T.expression w = function
and s_expression : T.expression w = fun ~(substs : substs) -> function
| T.E_literal x ->
let%bind x = s_literal ~v ~expr x in
let%bind x = s_literal ~substs x in
ok @@ T.E_literal x
| T.E_constant (var, vals) ->
let%bind var = s_build_in ~v ~expr var in
let%bind vals = bind_map_list (s_annotated_expression ~v ~expr) vals in
let%bind var = s_build_in ~substs var in
let%bind vals = bind_map_list (s_annotated_expression ~substs) vals in
ok @@ T.E_constant (var, vals)
| T.E_variable tv ->
let%bind tv = s_variable ~v ~expr tv in
let%bind tv = s_variable ~substs 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
let%bind val1 = s_annotated_expression ~substs val1 in
let%bind val2 = s_annotated_expression ~substs 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
let%bind binder = s_variable ~substs binder in
let%bind body = s_annotated_expression ~substs body in
ok @@ T.E_lambda { binder; body }
| T.E_let_in { binder; rhs; result; inline } ->
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
let%bind binder = s_variable ~substs binder in
let%bind rhs = s_annotated_expression ~substs rhs in
let%bind result = s_annotated_expression ~substs result in
ok @@ T.E_let_in { binder; rhs; result; inline }
| T.E_tuple vals ->
let%bind vals = bind_map_list (s_annotated_expression ~v ~expr) vals in
let%bind vals = bind_map_list (s_annotated_expression ~substs) vals in
ok @@ T.E_tuple vals
| T.E_tuple_accessor (val_, i) ->
let%bind val_ = s_annotated_expression ~v ~expr val_ in
let%bind val_ = s_annotated_expression ~substs val_ in
let i = i in
ok @@ T.E_tuple_accessor (val_, i)
| T.E_constructor (tvar, val_) ->
let%bind tvar = s_constructor ~v ~expr tvar in
let%bind val_ = s_annotated_expression ~v ~expr val_ in
let%bind tvar = s_constructor ~substs tvar in
let%bind val_ = s_annotated_expression ~substs val_ in
ok @@ T.E_constructor (tvar, val_)
| T.E_record aemap ->
let _TODO = aemap in
failwith "TODO: subst in record"
(* 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
* let key = s_type_variable ~substs key in
* let val_ = s_annotated_expression ~substs val_ in
* ok @@ (key , val_)) aemap in
* ok @@ T.E_record aemap *)
| T.E_record_accessor (val_, l) ->
let%bind val_ = s_annotated_expression ~v ~expr val_ in
let%bind l = s_label ~v ~expr l in
let%bind val_ = s_annotated_expression ~substs val_ in
let l = l in (* Nothing to substitute, this is a label, not a type *)
ok @@ T.E_record_accessor (val_, l)
| T.E_record_update (r, (l,e)) ->
let%bind r = s_annotated_expression ~v ~expr r in
let%bind e = s_annotated_expression ~v ~expr e in
ok @@ T.E_record_update (r,(l,e))
| T.E_record_update (r, (l, e)) ->
let%bind r = s_annotated_expression ~substs r in
let%bind e = s_annotated_expression ~substs e in
ok @@ T.E_record_update (r, (l, e))
| 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
let%bind val1 = s_annotated_expression ~substs val1 in
let%bind val2 = s_annotated_expression ~substs val2 in
ok @@ (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
let%bind val1 = s_annotated_expression ~substs val1 in
let%bind val2 = s_annotated_expression ~substs val2 in
ok @@ (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
let%bind vals = bind_map_list (s_annotated_expression ~substs) vals in
ok @@ T.E_list vals
| T.E_set vals ->
let%bind vals = bind_map_list (s_annotated_expression ~v ~expr) vals in
let%bind vals = bind_map_list (s_annotated_expression ~substs) 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
let%bind val1 = s_annotated_expression ~substs val1 in
let%bind val2 = s_annotated_expression ~substs val2 in
ok @@ T.E_look_up (val1 , val2)
| T.E_matching (val_ , matching_expr) ->
let%bind val_ = s_annotated_expression ~v ~expr val_ in
let%bind matching = s_matching_expr ~v ~expr matching_expr in
let%bind val_ = s_annotated_expression ~substs val_ in
let%bind matching = s_matching_expr ~substs matching_expr 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
let%bind val1 = s_annotated_expression ~substs val1 in
let%bind val2 = s_annotated_expression ~substs 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
let%bind val1 = s_annotated_expression ~substs val1 in
let%bind val2 = s_annotated_expression ~substs 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
let%bind named_tval = s_named_type_value ~substs named_tval in
let%bind access_path = s_access_path ~substs access_path in
let%bind val_ = s_annotated_expression ~substs 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
and s_annotated_expression : T.annotated_expression w = fun ~substs { expression; type_annotation; environment; location } ->
let%bind expression = s_expression ~substs expression in
let%bind type_annotation = s_type_value ~substs type_annotation in
let%bind environment = s_full_environment ~substs 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%bind name = s_variable ~v ~expr name in
let%bind annotated_expression = s_annotated_expression ~v ~expr annotated_expression in
and s_named_expression : T.named_expression w = fun ~substs { name; annotated_expression } ->
let name = name in (* Nothing to substitute, this is a variable name *)
let%bind annotated_expression = s_annotated_expression ~substs annotated_expression in
ok T.{ name; annotated_expression }
and s_declaration ~v ~expr : T.declaration w =
and s_declaration : T.declaration w = fun ~substs ->
function
Ast_typed.Declaration_constant (e, i, (env1, env2)) ->
let%bind e = s_named_expression ~v ~expr e in
let%bind env1 = s_full_environment ~v ~expr env1 in
let%bind env2 = s_full_environment ~v ~expr env2 in
ok @@ Ast_typed.Declaration_constant (e, i, (env1, env2))
Ast_typed.Declaration_constant (e, inline, (env1, env2)) ->
let%bind e = s_named_expression ~substs e in
let%bind env1 = s_full_environment ~substs env1 in
let%bind env2 = s_full_environment ~substs env2 in
ok @@ Ast_typed.Declaration_constant (e, inline, (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 s_declaration_wrap : T.declaration Location.wrap w = fun ~substs d ->
Trace.bind_map_location (s_declaration ~substs) d
(* 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 =
Trace.bind_map_list (s_declaration_wrap ~v ~expr) p
and s_program : Ast_typed.program w = fun ~substs p ->
Trace.bind_map_list (s_declaration_wrap ~substs) p
(*
Computes `P[v := expr]`.
*)
and type_value ~tv ~v ~expr =
let self tv = type_value ~tv ~v ~expr in
and type_value ~tv ~substs =
let self tv = type_value ~tv ~substs in
let (v, expr) = substs in
match tv with
| P_variable v' when v' = v -> expr
| P_variable v' when Var.equal v' v -> expr
| P_variable _ -> tv
| P_constant (x , lst) -> (
let lst' = List.map self lst in
@ -280,7 +283,7 @@ module Substitution = struct
P_apply ab'
)
| P_forall p -> (
let aux c = constraint_ ~c ~v ~expr in
let aux c = constraint_ ~c ~substs in
let constraints = List.map aux p.constraints in
if (p.binder = v) then (
P_forall { p with constraints }
@ -290,31 +293,33 @@ module Substitution = struct
)
)
and constraint_ ~c ~v ~expr =
and constraint_ ~c ~substs =
match c with
| C_equation ab -> (
let ab' = pair_map (fun tv -> type_value ~tv ~v ~expr) ab in
let ab' = pair_map (fun tv -> type_value ~tv ~substs) ab in
C_equation ab'
)
| C_typeclass (tvs , tc) -> (
let tvs' = List.map (fun tv -> type_value ~tv ~v ~expr) tvs in
let tc' = typeclass ~tc ~v ~expr in
let tvs' = List.map (fun tv -> type_value ~tv ~substs) tvs in
let tc' = typeclass ~tc ~substs in
C_typeclass (tvs' , tc')
)
| C_access_label (tv , l , v') -> (
let tv' = type_value ~tv ~v ~expr in
let tv' = type_value ~tv ~substs in
C_access_label (tv' , l , v')
)
and typeclass ~tc ~v ~expr =
List.map (List.map (fun tv -> type_value ~tv ~v ~expr)) tc
and typeclass ~tc ~substs =
List.map (List.map (fun tv -> type_value ~tv ~substs)) tc
let program = s_program
(* Performs beta-reduction at the root of the type *)
let eval_beta_root ~(tv : type_value) =
match tv with
P_apply (P_forall { binder; constraints; body }, arg) ->
let constraints = List.map (fun c -> constraint_ ~c ~v:binder ~expr:arg) constraints in
(type_value ~tv:body ~v:binder ~expr:arg , constraints)
let constraints = List.map (fun c -> constraint_ ~c ~substs:(mk_substs ~v:binder ~expr:arg)) constraints in
(type_value ~tv:body ~substs:(mk_substs ~v:binder ~expr:arg) , constraints)
| _ -> (tv , [])
end

6
src/test/typer_tests.ml
View File

@ -12,7 +12,7 @@ let int () : unit result =
let open Typer in
let e = Environment.full_empty in
let state = Typer.Solver.initial_state in
let%bind (post , new_state) = type_expression e state pre in
let%bind (post , new_state) = type_expression_subst e state pre in
let () = Typer.Solver.discard_state new_state in
let open! Typed in
let open Combinators in
@ -27,7 +27,7 @@ module TestExpressions = struct
let pre = expr in
let open Typer in
let open! Typed in
let%bind (post , new_state) = type_expression env state pre in
let%bind (post , new_state) = type_expression_subst env state pre in
let () = Typer.Solver.discard_state new_state in
let%bind () = assert_type_value_eq (post.type_annotation, test_expected_ty) in
ok ()
@ -37,7 +37,7 @@ module TestExpressions = struct
module E = O
let unit () : unit result = test_expression I.(e_unit ()) O.(t_unit ())
let int () : unit result = test_expression I.(e_int 32) O.(t_int ())
let int () : unit result = test_expression I.(e_int 32) O.(t_int ())
let bool () : unit result = test_expression I.(e_bool true) O.(t_bool ())
let string () : unit result = test_expression I.(e_string "s") O.(t_string ())
let bytes () : unit result =

12
vendors/UnionFind/Partition0.ml vendored
View File

@ -38,12 +38,10 @@ module Make (Item: Partition.Item) =
(* Printing *)
let print (p: partition) =
let buffer = Buffer.create 80 in
let print ppf p =
let print src dst =
let link =
Printf.sprintf "%s -> %s\n"
(Item.to_string src) (Item.to_string dst)
in Buffer.add_string buffer link
in (ItemMap.iter print p; buffer)
Format.fprintf ppf "%s -> %s (%s)\n"
(Item.to_string src) (Item.to_string dst) (Item.to_string (repr src p))
in ItemMap.iter print p
end