Skip to content

New mode solver supporting multiple axes with morphisms #1760

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 85 commits into from
Feb 14, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
85 commits
Select commit Hold shift + click to select a range
28146f6
new solver
riaqn Oct 26, 2023
96dd0de
better printing
riaqn Oct 26, 2023
da7cd38
remove solver_mono from mode_intf
riaqn Nov 3, 2023
3327f19
document solver_polarized
riaqn Nov 3, 2023
2dc6c3b
address some comments
riaqn Nov 6, 2023
7e88ecf
address more comments
riaqn Nov 6, 2023
d8d5ab8
rename "constrain" to "zap"
riaqn Nov 6, 2023
d736c10
rename constrain_legacy
riaqn Nov 7, 2023
06aca32
make depend
riaqn Nov 7, 2023
1966bf9
make fmt
riaqn Nov 7, 2023
d3bcfe5
remove _intf.ml
riaqn Nov 7, 2023
eed31e5
use comonadic in env
riaqn Nov 9, 2023
d29be3a
Add Allow_Disallow, restricting types of Obj.magic
goldfirere Nov 22, 2023
710e48e
Fix type errors discovered in previous commit
goldfirere Nov 22, 2023
01edf27
Use Allow_disallow in more places
goldfirere Nov 22, 2023
cc21c15
show soundness of allow_disallow
riaqn Dec 4, 2023
ba477d8
Prevent chance of forgetting the "sound" version
goldfirere Dec 4, 2023
b137166
minor changes
riaqn Dec 4, 2023
f4c9021
Remove the Solver_polarized.morph type (#1)
goldfirere Dec 14, 2023
3715f1e
adjust comments
riaqn Dec 15, 2023
e697f2b
remove address_of
riaqn Dec 19, 2023
92d1ed0
more comments
riaqn Dec 19, 2023
a62c2f6
make [log] non-optional
riaqn Dec 19, 2023
b0348e1
better comments
riaqn Dec 19, 2023
eb4afb7
More fixes
riaqn Dec 19, 2023
38a6cc7
bind temp results
riaqn Dec 19, 2023
37ec828
add C.eq_morph
riaqn Dec 22, 2023
7e7fddf
set_append_changes
riaqn Dec 22, 2023
1bf1b09
compare Value with Alloc
riaqn Dec 22, 2023
a70a331
more comments
riaqn Dec 22, 2023
183c27b
warn about infinite lattices
riaqn Dec 22, 2023
9dfd9c0
Small simplification to set_obj
goldfirere Jan 9, 2024
943c2cb
example of variable cycle
riaqn Jan 26, 2024
830cd44
say "uniqueness_op" because monotonicity
riaqn Jan 26, 2024
6875b5c
rename set to lift
riaqn Jan 26, 2024
67336b5
exhaustive match
riaqn Jan 26, 2024
df9129a
inline unusual helper functions
riaqn Jan 26, 2024
010c56c
fix rebase issues
riaqn Jan 28, 2024
203395b
Small simplification
goldfirere Jan 29, 2024
d1318ad
some renaming and comments
riaqn Jan 29, 2024
e2a7fde
more comment
riaqn Jan 29, 2024
c3d80d1
remove un-needed assertions.
riaqn Jan 29, 2024
1913745
fix chamelon
riaqn Jan 30, 2024
c1b3674
make fmt
riaqn Jan 30, 2024
ad809f9
add file header comments
riaqn Jan 30, 2024
86d84bc
exhausive match
riaqn Jan 30, 2024
6541816
use ref for morph counting
riaqn Jan 30, 2024
5616931
Reorder in maybe_compose
goldfirere Jan 31, 2024
1689d4b
switch from lift to map
riaqn Jan 31, 2024
d7dda91
avoid caml_curry
riaqn Feb 1, 2024
7219e41
dedup in join and meet
riaqn Feb 1, 2024
aaaff40
better error message
riaqn Feb 1, 2024
8d12968
fix tests
riaqn Feb 1, 2024
98874a0
comments
riaqn Feb 1, 2024
cdc5c49
inlining newvar_above/blow, and more uncurrying
riaqn Feb 1, 2024
f2fff0f
remove ?logging
riaqn Feb 1, 2024
99b91ed
make sure arity is correct and avoid closure allocation
riaqn Feb 2, 2024
e781f42
remove morphism counting
riaqn Feb 2, 2024
6b471cf
force inline to avoid caml_applyX
riaqn Feb 2, 2024
acce132
address comments
riaqn Feb 2, 2024
c7f4503
rename and phy eq in eq_morphvar
riaqn Feb 2, 2024
9a23f74
Small improvement to [eq_morphvar]
goldfirere Feb 2, 2024
63528a4
better comments about lattices
riaqn Feb 6, 2024
d63f905
don't hint to use exclave when useless
riaqn Feb 6, 2024
8a02513
fix type_argument
riaqn Feb 6, 2024
1a7fed6
comments about inner_alloc_mode
riaqn Feb 6, 2024
7919454
magic for eq_obj and eq_morph
riaqn Feb 8, 2024
fee6159
allow/disallow for Value.List
riaqn Feb 9, 2024
dde47c9
Add comment about actual vs expected
goldfirere Feb 9, 2024
ff88178
comment mode_argument
riaqn Feb 11, 2024
e968487
eq_morph doesn't take dst
riaqn Feb 11, 2024
2ff988f
Magic_equal
riaqn Feb 11, 2024
f28aa46
better comment about adjunction
riaqn Feb 11, 2024
51a2bb0
abstraction in ctype
riaqn Feb 12, 2024
fea325e
comment close_over and partial_apply
riaqn Feb 12, 2024
6bafada
fix eta expansion bug
riaqn Feb 12, 2024
aeb463c
Alloc.Const.t is record, not tuple
riaqn Feb 12, 2024
f739fbf
Simplify interface to [close_over]
goldfirere Feb 12, 2024
8a74f92
Generalize the type of close_over
goldfirere Feb 12, 2024
56fa2a9
fixed definition of partial adjoint
riaqn Feb 14, 2024
8313502
better comment about partial adjoint
riaqn Feb 14, 2024
05f028c
even better comments
riaqn Feb 14, 2024
eb01326
Merge remote-tracking branch 'origin/main' into new-solver-flambda-ba…
goldfirere Feb 14, 2024
32bf63e
make fmt
riaqn Feb 14, 2024
6d6ca39
bootstrap
goldfirere Feb 14, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
39 changes: 21 additions & 18 deletions chamelon/compat.jst.ml
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ open Types
open Mode

let dummy_jkind = Jkind.value ~why:(Unknown "dummy_layout")
let dummy_value_mode = Value.legacy
let dummy_value_mode = Value.disallow_right Value.legacy
let mkTvar name = Tvar { name; jkind = dummy_jkind }

let mkTarrow (label, t1, t2, comm) =
Expand All @@ -16,30 +16,33 @@ let mkTexp_ident ?id:(ident_kind, uu = (Id_value, shared_many_use))
Texp_ident (path, longident, vd, ident_kind, uu)

type nonrec apply_arg = apply_arg
type texp_apply_identifier = apply_position * Locality.t
type texp_apply_identifier = apply_position * Locality.l

let mkTexp_apply ?id:(pos, mode = (Default, Locality.legacy)) (exp, args) =
let mkTexp_apply
?id:(pos, mode = (Default, Locality.disallow_right Locality.legacy))
(exp, args) =
Texp_apply (exp, args, pos, mode)

type texp_tuple_identifier = string option list * Alloc.t
type texp_tuple_identifier = string option list * Alloc.r

let mkTexp_tuple ?id exps =
let labels, alloc =
match id with
| None -> (List.map (fun _ -> None) exps, Alloc.legacy)
| None -> (List.map (fun _ -> None) exps, Alloc.disallow_left Alloc.legacy)
| Some id -> id
in
let exps = List.combine labels exps in
Texp_tuple (exps, alloc)

type texp_construct_identifier = Alloc.t option
type texp_construct_identifier = Alloc.r option

let mkTexp_construct ?id:(mode = Some Alloc.legacy) (name, desc, args) =
let mkTexp_construct ?id:(mode = Some (Alloc.disallow_left Alloc.legacy))
(name, desc, args) =
Texp_construct (name, desc, args, mode)

type texp_function_param_identifier = {
param_sort : Jkind.Sort.t;
param_mode : Alloc.t;
param_mode : Alloc.l;
param_curry : function_curry;
param_newtypes : (string Location.loc * Jkind.annotation option) list;
}
Expand All @@ -54,7 +57,7 @@ type texp_function_param = {
}

type texp_function_cases_identifier = {
last_arg_mode : Alloc.t;
last_arg_mode : Alloc.l;
last_arg_sort : Jkind.Sort.t;
last_arg_exp_extra : exp_extra option;
last_arg_attributes : attributes;
Expand All @@ -75,15 +78,15 @@ type texp_function = {
}

type texp_function_identifier = {
alloc_mode : Alloc.t;
alloc_mode : Alloc.r;
ret_sort : Jkind.sort;
region : bool;
ret_mode : Alloc.t;
ret_mode : Alloc.l;
}

let texp_function_cases_identifier_defaults =
{
last_arg_mode = Alloc.legacy;
last_arg_mode = Alloc.disallow_right Alloc.legacy;
last_arg_sort = Jkind.Sort.value;
last_arg_exp_extra = None;
last_arg_attributes = [];
Expand All @@ -92,16 +95,16 @@ let texp_function_cases_identifier_defaults =
let texp_function_param_identifier_defaults =
{
param_sort = Jkind.Sort.value;
param_mode = Alloc.legacy;
param_curry = More_args { partial_mode = Alloc.legacy };
param_mode = Alloc.disallow_right Alloc.legacy;
param_curry = More_args { partial_mode = Alloc.disallow_right Alloc.legacy };
param_newtypes = [];
}

let texp_function_defaults =
{
alloc_mode = Alloc.legacy;
alloc_mode = Alloc.disallow_left Alloc.legacy;
ret_sort = Jkind.Sort.value;
ret_mode = Alloc.legacy;
ret_mode = Alloc.disallow_right Alloc.legacy;
region = false;
}

Expand Down Expand Up @@ -249,12 +252,12 @@ let view_texp (e : expression_desc) =
| Texp_match (e, sort, cases, partial) -> Texp_match (e, cases, partial, sort)
| _ -> O e

type tpat_var_identifier = Value.t
type tpat_var_identifier = Value.l

let mkTpat_var ?id:(mode = dummy_value_mode) (ident, name) =
Tpat_var (ident, name, Uid.internal_not_actually_unique, mode)

type tpat_alias_identifier = Value.t
type tpat_alias_identifier = Value.l

let mkTpat_alias ?id:(mode = dummy_value_mode) (p, ident, name) =
Tpat_alias (p, ident, name, Uid.internal_not_actually_unique, mode)
Expand Down
2 changes: 1 addition & 1 deletion native_toplevel/opttoploop.ml
Original file line number Diff line number Diff line change
Expand Up @@ -348,7 +348,7 @@ let name_expression ~loc ~attrs sort exp =
in
let sg = [Sig_value(id, vd, Exported)] in
let pat =
{ pat_desc = Tpat_var(id, mknoloc name, vd.val_uid, Mode.Value.legacy);
{ pat_desc = Tpat_var(id, mknoloc name, vd.val_uid, Mode.Value.disallow_right Mode.Value.legacy);
pat_loc = loc;
pat_extra = [];
pat_type = exp.exp_type;
Expand Down
22 changes: 21 additions & 1 deletion ocaml/.depend
Original file line number Diff line number Diff line change
Expand Up @@ -1114,12 +1114,22 @@ typing/jkind.cmi : \
parsing/jane_asttypes.cmi \
typing/ident.cmi
typing/mode.cmo : \
typing/solver_intf.cmi \
typing/solver.cmi \
typing/mode_intf.cmi \
utils/misc.cmi \
typing/mode.cmi
typing/mode.cmx : \
typing/solver_intf.cmi \
typing/solver.cmx \
typing/mode_intf.cmi \
utils/misc.cmx \
typing/mode.cmi
typing/mode.cmi :
typing/mode.cmi : \
typing/mode_intf.cmi
typing/mode_intf.cmi : \
typing/solver_intf.cmi \
typing/solver.cmi
typing/mtype.cmo : \
typing/types.cmi \
typing/subst.cmi \
Expand Down Expand Up @@ -1507,6 +1517,16 @@ typing/signature_group.cmx : \
typing/signature_group.cmi
typing/signature_group.cmi : \
typing/types.cmi
typing/solver.cmo : \
typing/solver_intf.cmi \
typing/solver.cmi
typing/solver.cmx : \
typing/solver_intf.cmi \
typing/solver.cmi
typing/solver.cmi : \
typing/solver_intf.cmi
typing/solver_intf.cmi : \
utils/misc.cmi
typing/stypes.cmo : \
typing/typedtree.cmi \
typing/printtyp.cmi \
Expand Down
Binary file modified ocaml/boot/ocamlc
Binary file not shown.
1 change: 1 addition & 0 deletions ocaml/compilerlibs/Makefile.compilerlibs
Original file line number Diff line number Diff line change
Expand Up @@ -82,6 +82,7 @@ PARSING_CMI = \
parsing/parsetree.cmi

TYPING = \
typing/solver.cmo \
typing/path.cmo \
typing/jkind.cmo \
typing/primitive.cmo \
Expand Down
5 changes: 3 additions & 2 deletions ocaml/dune
Original file line number Diff line number Diff line change
Expand Up @@ -68,7 +68,7 @@
parser)))
(library_flags -linkall)
(modules_without_implementation
annot asttypes cmo_format outcometree parsetree debug_event)
annot asttypes cmo_format outcometree parsetree debug_event solver_intf mode_intf)
(modules
;; UTILS
config build_path_prefix_map misc identifiable numbers arg_helper clflags
Expand All @@ -91,7 +91,7 @@
tast_iterator tast_mapper signature_group cmt_format cms_format untypeast
includemod includemod_errorprinter
typetexp patterns printpat parmatch stypes typedecl typeopt rec_check
typecore mode uniqueness_analysis
typecore solver_intf solver mode_intf mode uniqueness_analysis
typeclass typemod typedecl_variance typedecl_properties
typedecl_separability cmt2annot
; manual update: mli only files
Expand Down Expand Up @@ -317,6 +317,7 @@
(typeopt.mli as compiler-libs/typeopt.mli)
(rec_check.mli as compiler-libs/rec_check.mli)
(typecore.mli as compiler-libs/typecore.mli)
(solver.mli as compiler-libs/solver.mli)
(mode.mli as compiler-libs/mode.mli)
(uniqueness_analysis.mli as compiler-libs/uniqueness_analysis.mli)
(typeclass.mli as compiler-libs/typeclass.mli)
Expand Down
Loading