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

Add a reason string explaining why constraints are added by the typer

Browse Source
This commit is contained in:
Suzanne Dupéron 2020-04-29 17:54:52 +01:00
parent 4587862da7
commit 057bd19ca7
8 changed files with 80 additions and 61 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
src/passes/8-typer-new/PP.ml
View File

@ -2,7 +2,7 @@ open Ast_typed
open Format open Format
module UF = UnionFind.Poly2 module UF = UnionFind.Poly2
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 = match c_tag with let ct = match c_tag with
@ -34,6 +34,9 @@ let type_constraint : _ -> type_constraint_simpl -> unit = fun ppf ->
|SC_Poly _ -> fprintf ppf "Poly" |SC_Poly _ -> fprintf ppf "Poly"
|SC_Typeclass _ -> fprintf ppf "TC" |SC_Typeclass _ -> fprintf ppf "TC"
let type_constraint : _ -> type_constraint_simpl -> unit = fun ppf { reason_simpl ; c_simpl } ->
fprintf ppf "%a (reason: %s)" type_constraint_ c_simpl reason_simpl
let all_constraints ppf ac = let all_constraints ppf ac =
fprintf ppf "[%a]" (pp_print_list ~pp_sep:(fun ppf () -> fprintf ppf ";\n") type_constraint) ac fprintf ppf "[%a]" (pp_print_list ~pp_sep:(fun ppf () -> fprintf ppf ";\n") type_constraint) ac

41
src/passes/8-typer-new/solver.ml
View File

@ -159,7 +159,7 @@ let normalizer_grouped_by_variable : (type_constraint_simpl , type_constraint_si
UnionFindWrapper.add_constraints_related_to tvar constraints dbs UnionFindWrapper.add_constraints_related_to tvar constraints dbs
in List.fold_left aux dbs tvars in List.fold_left aux dbs tvars
in in
let dbs = match new_constraint with let dbs = match new_constraint.c_simpl with
SC_Constructor ({tv ; c_tag = _ ; tv_list} as c) -> store_constraint (tv :: tv_list) {constructor = [c] ; poly = [] ; tc = []} 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_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_Poly ({tv; forall = _} as c) -> store_constraint [tv] {constructor = [] ; poly = [c] ; tc = []}
@ -173,7 +173,7 @@ let normalizer_grouped_by_variable : (type_constraint_simpl , type_constraint_si
TOOD: are we checking somewhere that 'b … = 'b2 … ? *) TOOD: are we checking somewhere that 'b … = 'b2 … ? *)
let normalizer_assignments : (type_constraint_simpl , type_constraint_simpl) normalizer = let normalizer_assignments : (type_constraint_simpl , type_constraint_simpl) normalizer =
fun dbs new_constraint -> fun dbs new_constraint ->
match new_constraint with match new_constraint.c_simpl with
| SC_Constructor ({tv ; c_tag = _ ; tv_list = _} as c) -> | SC_Constructor ({tv ; c_tag = _ ; tv_list = _} as c) ->
let assignments = Map.update tv (function None -> Some c | e -> e) dbs.assignments in let assignments = Map.update tv (function None -> Some c | e -> e) dbs.assignments in
let dbs = {dbs with assignments} in let dbs = {dbs with assignments} in
@ -210,28 +210,28 @@ let rec normalizer_simpl : (type_constraint , type_constraint_simpl) normalizer
fun dbs new_constraint -> fun dbs new_constraint ->
let insert_fresh a b = let insert_fresh a b =
let fresh = Core.fresh_type_variable () in let fresh = Core.fresh_type_variable () in
let (dbs , cs1) = normalizer_simpl dbs (c_equation (P_variable fresh) a) in let (dbs , cs1) = normalizer_simpl dbs (c_equation (P_variable fresh) a "normalizer: simpl") in
let (dbs , cs2) = normalizer_simpl dbs (c_equation (P_variable fresh) b) in let (dbs , cs2) = normalizer_simpl dbs (c_equation (P_variable fresh) b "normalizer: simpl") in
(dbs , cs1 @ cs2) in (dbs , cs1 @ cs2) in
let split_constant a c_tag args = let split_constant a c_tag args =
let fresh_vars = List.map (fun _ -> Core.fresh_type_variable ()) args in let fresh_vars = List.map (fun _ -> Core.fresh_type_variable ()) args in
let fresh_eqns = List.map (fun (v,t) -> c_equation (P_variable v) t) (List.combine fresh_vars args) in let fresh_eqns = List.map (fun (v,t) -> c_equation (P_variable v) t "normalizer: split_constant") (List.combine fresh_vars args) in
let (dbs , recur) = List.fold_map_acc normalizer_simpl dbs fresh_eqns in let (dbs , recur) = List.fold_map_acc normalizer_simpl dbs fresh_eqns in
(dbs , [SC_Constructor {tv=a;c_tag;tv_list=fresh_vars}] @ List.flatten recur) in (dbs , [{c_simpl=SC_Constructor {tv=a;c_tag;tv_list=fresh_vars};reason_simpl="normalizer: split constant"}] @ List.flatten recur) in
let gather_forall a forall = (dbs , [SC_Poly { tv=a; forall }]) in let gather_forall a forall = (dbs , [{c_simpl=SC_Poly { tv=a; forall };reason_simpl="normalizer: gather_forall"}]) in
let gather_alias a b = (dbs , [SC_Alias { a ; b }]) in let gather_alias a b = (dbs , [{c_simpl=SC_Alias { a ; b };reason_simpl="normalizer: gather_alias"}]) in
let reduce_type_app a b = let reduce_type_app a b =
let (reduced, new_constraints) = check_applied @@ type_level_eval b in let (reduced, new_constraints) = check_applied @@ type_level_eval b in
let (dbs , recur) = List.fold_map_acc normalizer_simpl dbs new_constraints in let (dbs , recur) = List.fold_map_acc normalizer_simpl dbs new_constraints in
let (dbs , resimpl) = normalizer_simpl dbs (c_equation a reduced) in (* Note: this calls recursively but cant't fall in the same case. *) let (dbs , resimpl) = normalizer_simpl dbs (c_equation a reduced "normalizer: reduce_type_app") in (* Note: this calls recursively but cant't fall in the same case. *)
(dbs , resimpl @ List.flatten recur) in (dbs , resimpl @ List.flatten recur) in
let split_typeclass args tc = let split_typeclass args tc =
let fresh_vars = List.map (fun _ -> Core.fresh_type_variable ()) args in let fresh_vars = List.map (fun _ -> Core.fresh_type_variable ()) args in
let fresh_eqns = List.map (fun (v,t) -> c_equation (P_variable v) t) (List.combine fresh_vars args) in let fresh_eqns = List.map (fun (v,t) -> c_equation (P_variable v) t "normalizer: split_typeclass") (List.combine fresh_vars args) in
let (dbs , recur) = List.fold_map_acc normalizer_simpl dbs fresh_eqns in let (dbs , recur) = List.fold_map_acc normalizer_simpl dbs fresh_eqns in
(dbs, [SC_Typeclass { tc ; args = fresh_vars }] @ List.flatten recur) in (dbs, [{c_simpl=SC_Typeclass { tc ; args = fresh_vars };reason_simpl="normalizer: split_typeclass"}] @ List.flatten recur) in
match new_constraint with match new_constraint.c with
(* break down (forall 'b, body = forall 'c, body') into ('a = forall 'b, body and 'a = forall 'c, body')) *) (* break down (forall 'b, body = forall 'c, body') into ('a = forall 'b, body and 'a = forall 'c, body')) *)
| C_equation {aval=(P_forall _ as a); bval=(P_forall _ as b)} -> insert_fresh a b | C_equation {aval=(P_forall _ as a); bval=(P_forall _ as b)} -> insert_fresh a b
(* break down (forall 'b, body = c(args)) into ('a = forall 'b, body and 'a = c(args)) *) (* break down (forall 'b, body = c(args)) into ('a = forall 'b, body and 'a = c(args)) *)
@ -325,7 +325,7 @@ type 'selector_output propagator = 'selector_output -> structured_dbs -> new_con
let selector_break_ctor : (type_constraint_simpl, output_break_ctor) selector = let selector_break_ctor : (type_constraint_simpl, output_break_ctor) selector =
(* find two rules with the shape a = k(var …) and a = k'(var' …) *) (* find two rules with the shape a = k(var …) and a = k'(var' …) *)
fun type_constraint_simpl dbs -> fun type_constraint_simpl dbs ->
match type_constraint_simpl with match type_constraint_simpl.c_simpl with
SC_Constructor c -> SC_Constructor c ->
(* finding other constraints related to the same type variable and (* finding other constraints related to the same type variable and
with the same sort of constraint (constructor vs. constructor) with the same sort of constraint (constructor vs. constructor)
@ -473,7 +473,7 @@ let propagator_break_ctor : output_break_ctor propagator =
(* produce constraints: *) (* produce constraints: *)
(* a.tv = b.tv *) (* a.tv = b.tv *)
let eq1 = c_equation (P_variable a.tv) (P_variable b.tv) in let eq1 = c_equation (P_variable a.tv) (P_variable b.tv) "propagator: break_ctor" in
(* a.c_tag = b.c_tag *) (* a.c_tag = b.c_tag *)
if (compare_simple_c_constant a.c_tag b.c_tag) <> 0 then if (compare_simple_c_constant a.c_tag b.c_tag) <> 0 then
failwith (Format.asprintf "type error: incompatible types, not same ctor %a vs. %a (compare returns %d)" debug_pp_c_constructor_simpl a debug_pp_c_constructor_simpl b (compare_simple_c_constant a.c_tag b.c_tag)) failwith (Format.asprintf "type error: incompatible types, not same ctor %a vs. %a (compare returns %d)" debug_pp_c_constructor_simpl a debug_pp_c_constructor_simpl b (compare_simple_c_constant a.c_tag b.c_tag))
@ -482,7 +482,7 @@ let propagator_break_ctor : output_break_ctor propagator =
if List.length a.tv_list <> List.length b.tv_list then if List.length a.tv_list <> List.length b.tv_list then
failwith "type error: incompatible types, not same length" failwith "type error: incompatible types, not same length"
else else
let eqs3 = List.map2 (fun aa bb -> c_equation (P_variable aa) (P_variable bb)) a.tv_list b.tv_list in let eqs3 = List.map2 (fun aa bb -> c_equation (P_variable aa) (P_variable bb) "propagator: break_ctor") a.tv_list b.tv_list in
let eqs = eq1 :: eqs3 in let eqs = eq1 :: eqs3 in
(eqs , []) (* no new assignments *) (eqs , []) (* no new assignments *)
@ -531,7 +531,12 @@ and compare_type_expression = function
| P_variable _ -> 1 | P_variable _ -> 1
| P_constant _ -> 1 | P_constant _ -> 1
| P_apply { tf=b1; targ=b2 } -> compare_type_expression a1 b1 <? fun () -> compare_type_expression a2 b2) | P_apply { tf=b1; targ=b2 } -> compare_type_expression a1 b1 <? fun () -> compare_type_expression a2 b2)
and compare_type_constraint = function and compare_type_constraint = fun { c = ca ; reason = ra } { c = cb ; reason = rb } ->
let c = compare_type_constraint_ ca cb in
if c < 0 then -1
else if c = 0 then String.compare ra rb
else 1
and compare_type_constraint_ = function
| C_equation { aval=a1; bval=a2 } -> (function | C_equation { aval=a1; bval=a2 } -> (function
| C_equation { aval=b1; bval=b2 } -> compare_type_expression a1 b1 <? fun () -> compare_type_expression a2 b2 | C_equation { aval=b1; bval=b2 } -> compare_type_expression a1 b1 <? fun () -> compare_type_expression a2 b2
| C_typeclass _ -> -1 | C_typeclass _ -> -1
@ -569,7 +574,7 @@ let selector_specialize1 : (type_constraint_simpl, output_specialize1) selector
(* TODO: do the same for two rules with the shape (a = forall b, d) and tc(a…) *) (* TODO: do the same for two rules with the shape (a = forall b, d) and tc(a…) *)
(* TODO: do the appropriate thing for two rules with the shape (a = forall b, d) and (a = forall b', d') *) (* TODO: do the appropriate thing for two rules with the shape (a = forall b, d) and (a = forall b', d') *)
fun type_constraint_simpl dbs -> fun type_constraint_simpl dbs ->
match type_constraint_simpl with match type_constraint_simpl.c_simpl with
SC_Constructor c -> SC_Constructor c ->
(* vice versa *) (* vice versa *)
let other_cs = (UnionFindWrapper.get_constraints_related_to c.tv dbs).poly in let other_cs = (UnionFindWrapper.get_constraints_related_to c.tv dbs).poly in
@ -599,7 +604,7 @@ let propagator_specialize1 : output_specialize1 propagator =
The substitution is obtained by immediately applying the forall. *) The substitution is obtained by immediately applying the forall. *)
let apply = (P_apply {tf = (P_forall a.forall); targ = P_variable fresh_existential}) in let apply = (P_apply {tf = (P_forall a.forall); targ = P_variable fresh_existential}) in
let (reduced, new_constraints) = check_applied @@ type_level_eval apply in let (reduced, new_constraints) = check_applied @@ type_level_eval apply in
let eq1 = c_equation (P_variable b.tv) reduced in let eq1 = c_equation (P_variable b.tv) reduced "propagator: specialize1" in
let eqs = eq1 :: new_constraints in let eqs = eq1 :: new_constraints in
(eqs, []) (* no new assignments *) (eqs, []) (* no new assignments *)

71
src/passes/8-typer-new/wrap.ml
View File

@ -117,12 +117,12 @@ let failwith_ : unit -> (constraints * O.type_variable) = fun () ->
let variable : I.expression_variable -> T.type_expression -> (constraints * T.type_variable) = fun _name expr -> let variable : I.expression_variable -> T.type_expression -> (constraints * T.type_variable) = fun _name expr ->
let pattern = type_expression_to_type_value expr in let pattern = type_expression_to_type_value expr in
let type_name = Core.fresh_type_variable () in let type_name = Core.fresh_type_variable () in
[C_equation { aval = P_variable type_name ; bval = pattern }] , type_name [{ c = C_equation { aval = P_variable type_name ; bval = pattern } ; reason = "wrap: variable" }] , type_name
let literal : T.type_expression -> (constraints * T.type_variable) = fun t -> let literal : T.type_expression -> (constraints * T.type_variable) = fun t ->
let pattern = type_expression_to_type_value t in let pattern = type_expression_to_type_value t in
let type_name = Core.fresh_type_variable () in let type_name = Core.fresh_type_variable () in
[C_equation { aval = P_variable type_name ; bval = pattern }] , type_name [{ c = C_equation { aval = P_variable type_name ; bval = pattern } ; reason = "wrap: literal" }] , type_name
(* (*
let literal_bool : unit -> (constraints * O.type_variable) = fun () -> let literal_bool : unit -> (constraints * O.type_variable) = fun () ->
@ -140,7 +140,7 @@ let tuple : T.type_expression list -> (constraints * T.type_variable) = fun tys
let patterns = List.map type_expression_to_type_value tys in let patterns = List.map type_expression_to_type_value tys in
let pattern = p_constant C_record patterns in let pattern = p_constant C_record patterns in
let type_name = Core.fresh_type_variable () in let type_name = Core.fresh_type_variable () in
[C_equation { aval = P_variable type_name ; bval = pattern}] , type_name [{ c = C_equation { aval = P_variable type_name ; bval = pattern} ; reason = "wrap: tuple" }] , type_name
(* let t_tuple = ('label:int, 'v) … -> record ('label : 'v) … *) (* let t_tuple = ('label:int, 'v) … -> record ('label : 'v) … *)
(* let t_constructor = ('label:string, 'v) -> variant ('label : 'v) *) (* let t_constructor = ('label:string, 'v) -> variant ('label : 'v) *)
@ -169,7 +169,7 @@ end
let access_label ~(base : T.type_expression) ~(label : O.accessor) : (constraints * T.type_variable) = let access_label ~(base : T.type_expression) ~(label : O.accessor) : (constraints * T.type_variable) =
let base' = type_expression_to_type_value base in let base' = type_expression_to_type_value base in
let expr_type = Core.fresh_type_variable () in let expr_type = Core.fresh_type_variable () in
[T.C_access_label { c_access_label_tval = base' ; accessor = label ; c_access_label_tvar = expr_type }] , expr_type [{ c = C_access_label { c_access_label_tval = base' ; accessor = label ; c_access_label_tvar = expr_type } ; reason = "wrap: access_label" }] , expr_type
open Ast_typed.Misc open Ast_typed.Misc
let constructor let constructor
@ -180,25 +180,25 @@ let constructor
let sum = type_expression_to_type_value sum in let sum = type_expression_to_type_value sum in
let whole_expr = Core.fresh_type_variable () in let whole_expr = Core.fresh_type_variable () in
[ [
c_equation (P_variable whole_expr) sum ; c_equation (P_variable whole_expr) sum "wrap: constructor: whole" ;
c_equation t_arg c_arg ; c_equation t_arg c_arg "wrap: construcotr: arg" ;
] , whole_expr ] , whole_expr
let record : T.field_content T.label_map -> (constraints * T.type_variable) = fun fields -> let record : T.field_content T.label_map -> (constraints * T.type_variable) = fun fields ->
let record_type = type_expression_to_type_value (T.t_record fields ()) in let record_type = type_expression_to_type_value (T.t_record fields ()) in
let whole_expr = Core.fresh_type_variable () 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 "wrap: record: whole"] , whole_expr
let collection : O.constant_tag -> T.type_expression list -> (constraints * T.type_variable) = let collection : O.constant_tag -> T.type_expression list -> (constraints * T.type_variable) =
fun ctor element_tys -> fun ctor element_tys ->
let elttype = T.P_variable (Core.fresh_type_variable ()) in let elttype = T.P_variable (Core.fresh_type_variable ()) in
let aux elt = let aux elt =
let elt' = type_expression_to_type_value elt let elt' = type_expression_to_type_value elt
in c_equation elttype elt' in in c_equation elttype elt' "wrap: collection: elt" in
let equations = List.map aux element_tys in let equations = List.map aux element_tys in
let whole_expr = Core.fresh_type_variable () in let whole_expr = Core.fresh_type_variable () in
[ [
c_equation (P_variable whole_expr) (p_constant ctor [elttype]) ; c_equation (P_variable whole_expr) (p_constant ctor [elttype]) "wrap: collection: whole" ;
] @ equations , whole_expr ] @ equations , whole_expr
let list = collection T.C_list let list = collection T.C_list
@ -210,15 +210,15 @@ let map : (T.type_expression * T.type_expression) list -> (constraints * T.type_
let v_type = T.P_variable (Core.fresh_type_variable ()) in let v_type = T.P_variable (Core.fresh_type_variable ()) in
let aux_k (k , _v) = let aux_k (k , _v) =
let k' = type_expression_to_type_value k in let k' = type_expression_to_type_value k in
c_equation k_type k' in c_equation k_type k' "wrap: map: key" in
let aux_v (_k , v) = let aux_v (_k , v) =
let v' = type_expression_to_type_value v in let v' = type_expression_to_type_value v in
c_equation v_type v' in c_equation v_type v' "wrap: map: value" in
let equations_k = List.map aux_k kv_tys in let equations_k = List.map aux_k kv_tys in
let equations_v = List.map aux_v kv_tys in let equations_v = List.map aux_v kv_tys in
let whole_expr = Core.fresh_type_variable () in let whole_expr = Core.fresh_type_variable () in
[ [
c_equation (P_variable whole_expr) (p_constant C_map [k_type ; v_type]) ; c_equation (P_variable whole_expr) (p_constant C_map [k_type ; v_type]) "wrap: map: whole" ;
] @ equations_k @ equations_v , whole_expr ] @ equations_k @ equations_v , whole_expr
let big_map : (T.type_expression * T.type_expression) list -> (constraints * T.type_variable) = let big_map : (T.type_expression * T.type_expression) list -> (constraints * T.type_variable) =
@ -227,17 +227,17 @@ let big_map : (T.type_expression * T.type_expression) list -> (constraints * T.t
let v_type = T.P_variable (Core.fresh_type_variable ()) in let v_type = T.P_variable (Core.fresh_type_variable ()) in
let aux_k (k , _v) = let aux_k (k , _v) =
let k' = type_expression_to_type_value k in let k' = type_expression_to_type_value k in
c_equation k_type k' in c_equation k_type k' "wrap: big_map: key" in
let aux_v (_k , v) = let aux_v (_k , v) =
let v' = type_expression_to_type_value v in let v' = type_expression_to_type_value v in
c_equation v_type v' in c_equation v_type v' "wrap: big_map: value" in
let equations_k = List.map aux_k kv_tys in let equations_k = List.map aux_k kv_tys in
let equations_v = List.map aux_v kv_tys in let equations_v = List.map aux_v kv_tys in
let whole_expr = Core.fresh_type_variable () in let whole_expr = Core.fresh_type_variable () in
[ [
(* TODO: this doesn't tag big_maps uniquely (i.e. if two (* TODO: this doesn't tag big_maps uniquely (i.e. if two
big_map have the same type, they can be swapped. *) big_map have the same type, they can be swapped. *)
c_equation (P_variable whole_expr) (p_constant C_big_map [k_type ; v_type]) ; c_equation (P_variable whole_expr) (p_constant C_big_map [k_type ; v_type]) "wrap: big_map: whole" ;
] @ equations_k @ equations_v , whole_expr ] @ equations_k @ equations_v , whole_expr
let application : T.type_expression -> T.type_expression -> (constraints * T.type_variable) = let application : T.type_expression -> T.type_expression -> (constraints * T.type_variable) =
@ -246,7 +246,7 @@ let application : T.type_expression -> T.type_expression -> (constraints * T.typ
let f' = type_expression_to_type_value f in let f' = type_expression_to_type_value f in
let arg' = type_expression_to_type_value arg in let arg' = type_expression_to_type_value arg in
[ [
c_equation f' (p_constant C_arrow [arg' ; P_variable whole_expr]) ; c_equation f' (p_constant C_arrow [arg' ; P_variable whole_expr]) "wrap: application: f" ;
] , whole_expr ] , whole_expr
let look_up : T.type_expression -> T.type_expression -> (constraints * T.type_variable) = let look_up : T.type_expression -> T.type_expression -> (constraints * T.type_variable) =
@ -256,8 +256,8 @@ let look_up : T.type_expression -> T.type_expression -> (constraints * T.type_va
let whole_expr = Core.fresh_type_variable () in let whole_expr = Core.fresh_type_variable () in
let v = Core.fresh_type_variable () in let v = Core.fresh_type_variable () in
[ [
c_equation ds' (p_constant C_map [ind' ; P_variable v]) ; c_equation ds' (p_constant C_map [ind' ; P_variable v]) "wrap: look_up: map" ;
c_equation (P_variable whole_expr) (p_constant C_option [P_variable v]) ; c_equation (P_variable whole_expr) (p_constant C_option [P_variable v]) "wrap: look_up: whole" ;
] , whole_expr ] , whole_expr
let sequence : T.type_expression -> T.type_expression -> (constraints * T.type_variable) = let sequence : T.type_expression -> T.type_expression -> (constraints * T.type_variable) =
@ -266,8 +266,8 @@ let sequence : T.type_expression -> T.type_expression -> (constraints * T.type_v
let b' = type_expression_to_type_value b in let b' = type_expression_to_type_value b in
let whole_expr = Core.fresh_type_variable () in let whole_expr = Core.fresh_type_variable () in
[ [
c_equation a' (p_constant C_unit []) ; c_equation a' (p_constant C_unit []) "wrap: sequence: first" ;
c_equation b' (P_variable whole_expr) ; c_equation b' (P_variable whole_expr) "wrap: sequence: second (whole)" ;
] , whole_expr ] , whole_expr
let loop : T.type_expression -> T.type_expression -> (constraints * T.type_variable) = let loop : T.type_expression -> T.type_expression -> (constraints * T.type_variable) =
@ -276,9 +276,9 @@ let loop : T.type_expression -> T.type_expression -> (constraints * T.type_varia
let body' = type_expression_to_type_value body in let body' = type_expression_to_type_value body in
let whole_expr = Core.fresh_type_variable () in let whole_expr = Core.fresh_type_variable () in
[ [
c_equation expr' (P_variable (Stage_common.Constant.t_bool)) ; c_equation expr' (P_variable Stage_common.Constant.t_bool) "wrap: loop: expr" ;
c_equation body' (p_constant C_unit []) ; c_equation body' (p_constant C_unit []) "wrap: loop: body" ;
c_equation (P_variable whole_expr) (p_constant C_unit []) c_equation (P_variable whole_expr) (p_constant C_unit []) "wrap: loop: whole (unit)" ;
] , whole_expr ] , whole_expr
let let_in : T.type_expression -> T.type_expression option -> T.type_expression -> (constraints * T.type_variable) = let let_in : T.type_expression -> T.type_expression option -> T.type_expression -> (constraints * T.type_variable) =
@ -287,10 +287,10 @@ let let_in : T.type_expression -> T.type_expression option -> T.type_expression
let result' = type_expression_to_type_value result in let result' = type_expression_to_type_value result in
let rhs_tv_opt' = match rhs_tv_opt with let rhs_tv_opt' = match rhs_tv_opt with
None -> [] None -> []
| Some annot -> [c_equation rhs' (type_expression_to_type_value annot)] in | Some annot -> [c_equation rhs' (type_expression_to_type_value annot) "wrap: let_in: rhs"] in
let whole_expr = Core.fresh_type_variable () in let whole_expr = Core.fresh_type_variable () in
[ [
c_equation result' (P_variable whole_expr) ; c_equation result' (P_variable whole_expr) "wrap: let_in: result (whole)" ;
] @ rhs_tv_opt', whole_expr ] @ rhs_tv_opt', whole_expr
let recursive : T.type_expression -> (constraints * T.type_variable) = let recursive : T.type_expression -> (constraints * T.type_variable) =
@ -298,7 +298,7 @@ let recursive : T.type_expression -> (constraints * T.type_variable) =
let fun_type = type_expression_to_type_value fun_type in let fun_type = type_expression_to_type_value fun_type in
let whole_expr = Core.fresh_type_variable () in let whole_expr = Core.fresh_type_variable () in
[ [
c_equation fun_type (P_variable whole_expr) ; c_equation fun_type (P_variable whole_expr) "wrap: recursive: fun_type (whole)" ;
], whole_expr ], whole_expr
let assign : T.type_expression -> T.type_expression -> (constraints * T.type_variable) = let assign : T.type_expression -> T.type_expression -> (constraints * T.type_variable) =
@ -307,8 +307,8 @@ let assign : T.type_expression -> T.type_expression -> (constraints * T.type_var
let e' = type_expression_to_type_value e in let e' = type_expression_to_type_value e in
let whole_expr = Core.fresh_type_variable () in let whole_expr = Core.fresh_type_variable () in
[ [
c_equation v' e' ; c_equation v' e' "wrap: assign: var type must eq rhs type" ;
c_equation (P_variable whole_expr) (p_constant C_unit []) ; c_equation (P_variable whole_expr) (p_constant C_unit []) "wrap: assign: unit (whole)" ;
] , whole_expr ] , whole_expr
let annotation : T.type_expression -> T.type_expression -> (constraints * T.type_variable) = let annotation : T.type_expression -> T.type_expression -> (constraints * T.type_variable) =
@ -317,15 +317,15 @@ let annotation : T.type_expression -> T.type_expression -> (constraints * T.type
let annot' = type_expression_to_type_value annot in let annot' = type_expression_to_type_value annot in
let whole_expr = Core.fresh_type_variable () in let whole_expr = Core.fresh_type_variable () in
[ [
c_equation e' annot' ; c_equation e' annot' "wrap: annotation: expr type must eq annot" ;
c_equation e' (P_variable whole_expr) ; c_equation e' (P_variable whole_expr) "wrap: annotation: whole" ;
] , whole_expr ] , whole_expr
let matching : T.type_expression list -> (constraints * T.type_variable) = let matching : T.type_expression list -> (constraints * T.type_variable) =
fun es -> fun es ->
let whole_expr = Core.fresh_type_variable () in let whole_expr = Core.fresh_type_variable () in
let type_expressions = (List.map type_expression_to_type_value es) in let type_expressions = (List.map type_expression_to_type_value es) in
let cs = List.map (fun e -> c_equation (P_variable whole_expr) e) type_expressions let cs = List.map (fun e -> c_equation (P_variable whole_expr) e "wrap: matching: case (whole)") type_expressions
in cs, whole_expr in cs, whole_expr
let fresh_binder () = let fresh_binder () =
@ -342,15 +342,16 @@ let lambda
let unification_body = Core.fresh_type_variable () in let unification_body = Core.fresh_type_variable () in
let arg' = match arg with let arg' = match arg with
None -> [] None -> []
| Some arg -> [c_equation (P_variable unification_arg) (type_expression_to_type_value arg)] in | Some arg -> [c_equation (P_variable unification_arg) (type_expression_to_type_value arg) "wrap: lambda: arg annot"] in
let body' = match body with let body' = match body with
None -> [] None -> []
| Some body -> [c_equation (P_variable unification_body) (type_expression_to_type_value body)] | Some body -> [c_equation (P_variable unification_body) (type_expression_to_type_value body) "wrap: lambda: body annot"]
in [ in [
c_equation (type_expression_to_type_value fresh) (P_variable unification_arg) ; c_equation (type_expression_to_type_value fresh) (P_variable unification_arg) "wrap: lambda: arg" ;
c_equation (P_variable whole_expr) c_equation (P_variable whole_expr)
(p_constant C_arrow ([P_variable unification_arg ; (p_constant C_arrow ([P_variable unification_arg ;
P_variable unification_body])) P_variable unification_body]))
"wrap: lambda: arrow (whole)"
] @ arg' @ body' , whole_expr ] @ arg' @ body' , whole_expr
(* This is pretty much a wrapper for an n-ary function. *) (* This is pretty much a wrapper for an n-ary function. *)
@ -360,5 +361,5 @@ let constant : O.type_value -> T.type_expression list -> (constraints * T.type_v
let args' = List.map type_expression_to_type_value args in let args' = List.map type_expression_to_type_value args in
let args_tuple = p_constant C_record args' in let args_tuple = p_constant C_record args' in
[ [
c_equation f (p_constant C_arrow ([args_tuple ; P_variable whole_expr])) c_equation f (p_constant C_arrow ([args_tuple ; P_variable whole_expr])) "wrap: constant: as declared for built-in"
] , whole_expr ] , whole_expr

2
src/stages/4-ast_typed/misc.ml
View File

@ -536,4 +536,4 @@ let p_constant (p_ctor_tag : constant_tag) (p_ctor_args : p_ctor_args) =
p_ctor_args : p_ctor_args ; p_ctor_args : p_ctor_args ;
} }
let c_equation aval bval = C_equation { aval ; bval } let c_equation aval bval reason = { c = C_equation { aval ; bval }; reason }

2
src/stages/4-ast_typed/misc.mli
View File

@ -73,4 +73,4 @@ val get_entry : program -> string -> expression result
val program_environment : program -> full_environment val program_environment : program -> full_environment
val p_constant : constant_tag -> p_ctor_args -> type_value val p_constant : constant_tag -> p_ctor_args -> type_value
val c_equation : type_value -> type_value -> type_constraint val c_equation : type_value -> type_value -> string -> type_constraint

13
src/stages/4-ast_typed/types.ml
View File

@ -509,8 +509,11 @@ and c_access_label = {
c_access_label_tvar : type_variable ; c_access_label_tvar : type_variable ;
} }
(*What i was saying just before *) and type_constraint = {
and type_constraint = reason : string ;
c : type_constraint_ ;
}
and type_constraint_ =
(* | C_assignment of (type_variable * type_pattern) *) (* | C_assignment of (type_variable * type_pattern) *)
| C_equation of c_equation (* TVA = TVB *) | C_equation of c_equation (* TVA = TVB *)
| C_typeclass of c_typeclass (* TVL ∈ TVLs, for now in extension, later add intensional (rule-based system for inclusion in the typeclass) *) | C_typeclass of c_typeclass (* TVL ∈ TVLs, for now in extension, later add intensional (rule-based system for inclusion in the typeclass) *)
@ -569,7 +572,11 @@ and c_poly_simpl = {
tv : type_variable ; tv : type_variable ;
forall : p_forall ; forall : p_forall ;
} }
and type_constraint_simpl = and type_constraint_simpl = {
reason_simpl : string ;
c_simpl : type_constraint_simpl_ ;
}
and type_constraint_simpl_ =
| SC_Constructor of c_constructor_simpl (* α = ctor(β, …) *) | SC_Constructor of c_constructor_simpl (* α = ctor(β, …) *)
| SC_Alias of c_alias (* α = β *) | SC_Alias of c_alias (* α = β *)
| SC_Poly of c_poly_simpl (* α = forall β, δ where δ can be a more complex type *) | SC_Poly of c_poly_simpl (* α = forall β, δ where δ can be a more complex type *)

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

@ -245,7 +245,10 @@ module Substitution = struct
) )
) )
and constraint_ ~c ~substs = and constraint_ ~c:{c;reason} ~substs =
{c = constraint__ ~c ~substs;reason}
and constraint__ ~c ~substs =
match c with match c with
| C_equation { aval; bval } -> ( | C_equation { aval; bval } -> (
let aux tv = type_value ~tv ~substs in let aux tv = type_value ~tv ~substs in

2
src/stages/typesystem/shorthands.ml
View File

@ -3,7 +3,7 @@ open Core
open Ast_typed.Misc open Ast_typed.Misc
let tc type_vars allowed_list : type_constraint = let tc type_vars allowed_list : type_constraint =
C_typeclass {tc_args = type_vars ; typeclass = allowed_list} { c = C_typeclass {tc_args = type_vars ; typeclass = allowed_list} ; reason = "shorthands: typeclass" }
let forall binder f = let forall binder f =
let () = ignore binder in let () = ignore binder in