Skip to content
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

Implement Labeled Tuples #1235

Draft
wants to merge 120 commits into
base: dev
Choose a base branch
from
Draft
Changes from 1 commit
Commits
Show all changes
120 commits
Select commit Hold shift + click to select a range
3d2a351
labeled tuple rewrite
WondAli Feb 23, 2024
6889f4f
Merge branch 'dev' into labeled-tuple-rewrite
WondAli Feb 23, 2024
c137ded
working dot operator + bug fixes to precedence
WondAli Mar 23, 2024
5af500f
may need to revert some tuplabel code since no longer consistent with…
WondAli Mar 31, 2024
9927605
allow for unmatched labels in one direction
WondAli Apr 13, 2024
55500e6
updated casting for labels
WondAli Apr 22, 2024
f08c114
left-associativity for dot operator
WondAli Apr 25, 2024
7ab1470
dot now treats labels as tuples of size 1
WondAli Apr 25, 2024
1cdeb3a
multiple bug fixes and implemented labels as function arguments. TODO…
WondAli Apr 28, 2024
0598c9c
code cleanup, quality improvement. Also fixes to casting (mostly)
WondAli Jun 7, 2024
b3e7c84
casting bug fix
WondAli Jun 7, 2024
dfdf051
merged with dev
WondAli Jun 7, 2024
07275db
minor changes to dot in statics and matching
WondAli Jun 25, 2024
44841b8
standalone labels as singleton tuples + shifting error handling for u…
WondAli Jun 28, 2024
56d9a50
fixed bug concerning rearranging function arguments
WondAli Jul 3, 2024
3d294dd
documentation in progress
WondAli Jul 30, 2024
cbe3125
merge complete
WondAli Jul 31, 2024
e0952df
renamed some variables to be more accurate
WondAli Aug 8, 2024
bf1137c
dot operator update
WondAli Aug 12, 2024
9ab0f49
dot operator static fixes
WondAli Aug 16, 2024
db194f8
Creation of Label term, bug fixes, documentation updates
WondAli Aug 23, 2024
c20706a
fixes to labeled expressions as singleton tuples
WondAli Aug 24, 2024
fe24986
minor test_elaboration update
WondAli Aug 24, 2024
773fa9b
singleton tuple fixes
WondAli Aug 27, 2024
e76f5e2
fix statics to check for mismatched labels
WondAli Aug 27, 2024
a802eb7
fix to let elaboration so that dot operators operate on annotated typ…
WondAli Aug 28, 2024
65eec8e
merge (not working)
WondAli Sep 12, 2024
4753f3f
fix to precedence and cast ground_caes_of
WondAli Sep 13, 2024
cae4bb5
elaborator fixes
WondAli Sep 13, 2024
bc22754
updated parser for dot operator
WondAli Sep 13, 2024
e810400
debug
7h3kk1d Sep 20, 2024
840f06f
Temp commit
7h3kk1d Sep 21, 2024
58fc12c
Add rearrange2
7h3kk1d Sep 21, 2024
2b1eda8
I got some version of elaboration working
7h3kk1d Sep 21, 2024
2be5a46
Fix formatting
7h3kk1d Sep 21, 2024
f7a2666
Cleanup
7h3kk1d Sep 23, 2024
a2c34df
Revert makefile changes
7h3kk1d Sep 23, 2024
50536fe
Cleanup debugging code
7h3kk1d Sep 23, 2024
4226bb4
More cleanup
7h3kk1d Sep 23, 2024
8eef13c
Got a version of evaluation to work
7h3kk1d Sep 23, 2024
998caeb
Stop elaborating labels in Dot
7h3kk1d Sep 27, 2024
000b853
updates to elaboration, label extraction, ap in progress
WondAli Sep 27, 2024
76247f0
merged with labeled-tuple-rewrite
WondAli Sep 27, 2024
8379dec
Missing labeled tuple labels elboration (#1399)
WondAli Sep 27, 2024
d5dfa8f
cleaned LabeledTuple util file
WondAli Sep 27, 2024
7d707c9
Rearranging does not occur past elaboration. Functions reworked to al…
WondAli Sep 29, 2024
20c51f9
Add support for fast_equal on TupLabel expressions
7h3kk1d Oct 2, 2024
49c11d9
Add test for elaboration adding labels to labeled tuples
7h3kk1d Oct 2, 2024
38b10c1
Inline expectation
7h3kk1d Oct 2, 2024
c315caa
Fix typos
7h3kk1d Oct 2, 2024
5707718
Add test for rearranging labels during elaboration
7h3kk1d Oct 2, 2024
e4fb061
Merge remote-tracking branch 'origin/dev' into labeled-tuple-rewrite
7h3kk1d Oct 2, 2024
8d6528e
Add test for labeled tuple projection evaluation
7h3kk1d Oct 2, 2024
a5c83bc
Add statics test for labeled parameter in function
7h3kk1d Oct 2, 2024
f4d778e
Added tests to assure that types are inconsistent when unlabeled vari…
7h3kk1d Oct 4, 2024
32173ea
removed function implicit labelling and rearranging in type consisten…
WondAli Oct 4, 2024
318cfb3
Add basic elaboration tests for singleton tuples
7h3kk1d Oct 11, 2024
c8ef191
Modify singleton labeled tuple elaboration
7h3kk1d Oct 11, 2024
22cd8d6
Add parser tests for singleton tuples
7h3kk1d Oct 11, 2024
f04c976
Wrap all tuplabels in tuples in parser
7h3kk1d Oct 11, 2024
78e817c
Remove is_contained logic
7h3kk1d Oct 11, 2024
7008809
More tests
7h3kk1d Oct 13, 2024
59ff548
Add assertions that there's no static errors in static tests
7h3kk1d Oct 13, 2024
158a62d
Merge branch 'dev' into labeled-tuple-rewrite
7h3kk1d Oct 13, 2024
0669d9c
Ensure more tests are fully consistent
7h3kk1d Oct 13, 2024
c27642b
Stop recalculating statics in tests
7h3kk1d Oct 13, 2024
bcd9fe2
Add support for displaying TupLabel with label and type in view_ty fu…
7h3kk1d Oct 13, 2024
926c5c7
Add labeled tuples doc page
7h3kk1d Oct 14, 2024
5f790cb
revert scratch file
7h3kk1d Oct 14, 2024
39cbba1
Revert init.ml
7h3kk1d Oct 14, 2024
b242321
Add sdocumentation page for labeled tuples
7h3kk1d Oct 14, 2024
de85c69
Tests for multiple labels
7h3kk1d Oct 14, 2024
3c36566
Update Makefile to include dev profile in watch-test
7h3kk1d Oct 14, 2024
72b4cac
Add test case for singleton labeled tuple adding label
7h3kk1d Oct 14, 2024
828da51
Make labeled tuple not need parens in display
7h3kk1d Oct 14, 2024
7688a2b
Add test case for let statement that adds labels during elaboration
7h3kk1d Oct 14, 2024
c86e5f0
Add support for lifting single values into a singleton labeled tuple …
7h3kk1d Oct 14, 2024
dac5119
Refmt
7h3kk1d Oct 14, 2024
3420d2c
Additional test for singleton labels
7h3kk1d Oct 14, 2024
1fa320c
SIngleton labels kind of work
7h3kk1d Oct 14, 2024
c87048d
Remove singleton product from type view
7h3kk1d Oct 14, 2024
01f84c5
Fix the duplicate singleton label statics
7h3kk1d Oct 15, 2024
e018126
Fix stack overflow
7h3kk1d Oct 15, 2024
11804a2
Fix warning in test statics
7h3kk1d Oct 15, 2024
523177e
First attempt singleton labeled tuple elaboration
7h3kk1d Oct 15, 2024
c4db0d0
Remove debug comment
7h3kk1d Oct 16, 2024
03208ff
Fix test
7h3kk1d Oct 16, 2024
0f8521a
More singleton label elaborator fixes
7h3kk1d Oct 16, 2024
1bee9bb
Update init
7h3kk1d Oct 18, 2024
e66dd80
Add tests for singleton labeled argument function application
7h3kk1d Oct 18, 2024
b42c613
Progress on elaborating singleton tuples with mismatched labels
7h3kk1d Oct 21, 2024
9a918ef
Fix warnings
7h3kk1d Oct 21, 2024
a603ae7
Merge remote-tracking branch 'origin/dev' into labeled-tuple-rewrite
7h3kk1d Oct 30, 2024
61937e7
Merge remote-tracking branch 'origin/dev' into labeled-tuple-rewrite
7h3kk1d Oct 31, 2024
d88395e
Closer to getting singleton labeled tuples to work
7h3kk1d Oct 31, 2024
7c5abb5
Fix unused warnings
7h3kk1d Nov 1, 2024
d163367
Errored statuses showed up right
7h3kk1d Nov 1, 2024
0343f51
Extract functions to be slightly more legible
7h3kk1d Nov 1, 2024
8d3d3e6
Merge branch 'dev' into labeled-tuple-rewrite
7h3kk1d Nov 1, 2024
12eef70
Fixed singleton labeled tuple in function application
7h3kk1d Nov 4, 2024
868ed9b
Fix statics test
7h3kk1d Nov 4, 2024
effab75
Merge remote-tracking branch 'origin/dev' into labeled-tuple-rewrite
7h3kk1d Nov 7, 2024
d1cd408
Add some information on the lifted type to the cursor inspector
7h3kk1d Nov 8, 2024
ece70b4
label uniqueness checking
WondAli Nov 10, 2024
3624020
Start elaborating singleton labeled tuple patterns
7h3kk1d Nov 8, 2024
ecbd7ce
Singleton labeled tuple pattern elaboration disabled under ascription
7h3kk1d Nov 15, 2024
24de2fa
Fix assertions
7h3kk1d Nov 15, 2024
58029ad
Stop debugging
7h3kk1d Nov 15, 2024
69fb726
Remove unnecessary module name
7h3kk1d Nov 15, 2024
4a78f89
Fix tests and strip casts out of some of the tests
7h3kk1d Nov 15, 2024
30e3b9c
Bugfix: statics now check that the first argument in a TupLabel is a …
WondAli Nov 18, 2024
5529383
Progress on improving cursor inspector for automatic labelling
7h3kk1d Nov 18, 2024
4a8776c
Fix unused module open
7h3kk1d Nov 18, 2024
7166f28
Add sugar to info
7h3kk1d Nov 18, 2024
6e71d52
Add more labeling information to cursor inspector
7h3kk1d Nov 21, 2024
ddaaaa9
Add pattern labels to cursor inspector
7h3kk1d Nov 26, 2024
88931f4
Remove lifted_ty from Info types
7h3kk1d Nov 26, 2024
3a96a5a
Cursor inspector changes
7h3kk1d Dec 5, 2024
68f85ab
updated dot operator to use labels
WondAli Dec 6, 2024
bd36673
Fix cursor inspector message
7h3kk1d Dec 10, 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
Prev Previous commit
Next Next commit
updates to elaboration, label extraction, ap in progress
WondAli committed Sep 27, 2024
commit 000b853e6f9c49ecbd79483d763e9d3634a24bf5
3 changes: 2 additions & 1 deletion src/haz3lcore/dynamics/DHPat.re
Original file line number Diff line number Diff line change
@@ -57,9 +57,10 @@ let rec bound_vars = (dp: t): list(Var.t) =>
| Ap(_, dp1) => bound_vars(dp1)
};

let get_label: t => option((LabeledTuple.t, t)) =
let rec get_label: t => option((LabeledTuple.t, t)) =
dp =>
switch (dp |> term_of) {
| Parens(dp) => get_label(dp)
| TupLabel({term: Label(name), _}, t') => Some((name, t'))
| _ => None
};
49 changes: 37 additions & 12 deletions src/haz3lcore/dynamics/Elaborator.re
Original file line number Diff line number Diff line change
@@ -234,8 +234,6 @@ let rec elaborate =
(m: Statics.Map.t, uexp: UExp.t, in_container: bool)
: (DHExp.t, Typ.t) => {
let (elaborated_type, ctx, co_ctx) = elaborated_type(m, uexp);
print_endline("exp: " ++ UExp.show(uexp));
print_endline("typ: " ++ Typ.show(elaborated_type));
let elaborate = (~in_container=false, m, uexp) =>
elaborate(m, uexp, in_container);
let cast_from = (ty, exp) => fresh_cast(exp, ty, elaborated_type);
@@ -323,28 +321,36 @@ let rec elaborate =
| Tuple(es) =>
let (ds, tys) =
List.map(elaborate(m, ~in_container=true), es) |> ListUtil.unzip;
let elab_typ_list =
switch (Typ.weak_head_normalize(ctx, elaborated_type).term) {
| Prod(tys) => tys
| _ => tys
};
let ds =
LabeledTuple.rearrange(
Typ.get_label, Exp.get_label, tys, ds, (name, p) =>
Typ.get_label, Exp.get_label, elab_typ_list, ds, (name, p) =>
TupLabel(Label(name) |> Exp.fresh, p) |> Exp.fresh
);
Exp.Tuple(ds) |> rewrap |> cast_from(Prod(tys) |> Typ.temp);
| Dot(e1, e2) =>
let (e1, ty1) = elaborate(m, e1);
let (e2, ty2) = elaborate(m, e2);
let ty =
switch (ty1.term, ty2.term) {
let (e2, _) = elaborate(m, e2);
let (e1, ty) =
switch (Typ.weak_head_normalize(ctx, ty1).term, e2.term) {
| (Prod(tys), Var(name)) =>
let element = LabeledTuple.find_label(Typ.get_label, tys, name);
switch (element) {
| Some({term: TupLabel(_, ty), _}) => ty
| _ => Unknown(Internal) |> Typ.temp
| Some({term: TupLabel(_, ty), _}) => (e1, ty)
| _ => (e1, Unknown(Internal) |> Typ.temp)
};
| (TupLabel(_, ty), Var(name))
when LabeledTuple.equal(Typ.get_label(ty1), Some((name, ty2))) => ty
| _ => Unknown(Internal) |> Typ.temp
when LabeledTuple.equal(Typ.get_label(ty1), Some((name, e2))) => (
e1,
ty,
)
| _ => (e1, Unknown(Internal) |> Typ.temp)
};
// How to freshcast this?
// Freshcast this, if necessary?
Exp.Dot(e1, e2) |> rewrap |> cast_from(ty);
| Var(v) =>
uexp
@@ -414,13 +420,32 @@ let rec elaborate =
let (a', tya) = elaborate(m, a);
let (tyf1, tyf2) = Typ.matched_arrow(ctx, tyf);
let f'' = fresh_cast(f', tyf, Arrow(tyf1, tyf2) |> Typ.temp);
// In case of singleton tuple for fun ty_in, implicitly convert arg if necessary
// TODO: Is needed for other Aps?
let rec get_args = (a, tya, tyf1) =>
switch (
Typ.weak_head_normalize(ctx, tya).term,
Typ.weak_head_normalize(ctx, tyf1).term,
) {
| (Parens(tya), _) => get_args(a, tya, tyf1)
| (Prod(_), Prod(_)) => (a, tya)
| (_, Prod([{term: TupLabel(_), _}])) => (
Tuple([a']) |> Exp.fresh,
Prod([tya]) |> Typ.temp,
)
| (_, _) => (a, tya)
};
let (a', tya) = get_args(a', tya, tyf1);
let a'' = fresh_cast(a', tya, tyf1);
Exp.Ap(dir, f'', a'') |> rewrap |> cast_from(tyf2);
| DeferredAp(f, args) =>
let (f', tyf) = elaborate(m, f);
let (args', tys) = List.map(elaborate(m), args) |> ListUtil.unzip;
let (tyf1, tyf2) = Typ.matched_arrow(ctx, tyf);
let ty_fargs = Typ.matched_prod(ctx, args, Exp.get_label, tyf1);
let (args, ty_fargs) =
Typ.matched_prod(ctx, args, Exp.get_label, tyf1, (name, b) =>
TupLabel(Label(name) |> Exp.fresh, b) |> Exp.fresh
);
let f'' =
fresh_cast(
f',
4 changes: 2 additions & 2 deletions src/haz3lcore/dynamics/PatternMatch.re
Original file line number Diff line number Diff line change
@@ -33,8 +33,8 @@ let rec matches = (dp: Pat.t, d: DHExp.t): match_result =>
| Label(name) =>
let* name' = Unboxing.unbox(Label, d);
name == name' ? Matches(Environment.empty) : DoesNotMatch;
| TupLabel(label, x) =>
let* x' = Unboxing.unbox(TupLabel(label), d);
| TupLabel(_, x) =>
let* x' = Unboxing.unbox(TupLabel(dp), d);
matches(x, x');
| ListLit(xs) =>
let* s' = Unboxing.unbox(List, d);
64 changes: 41 additions & 23 deletions src/haz3lcore/dynamics/Transition.re
Original file line number Diff line number Diff line change
@@ -162,6 +162,7 @@ module Transition = (EV: EV_MODE) => {
// Split DHExp into term and id information
let (term, rewrap) = DHExp.unwrap(d);
let wrap_ctx = (term): EvalCtx.t => Term({term, ids: [rep_id(d)]});
// print_endline(Exp.show(d));

// Transition rules
switch (term) {
@@ -363,18 +364,35 @@ module Transition = (EV: EV_MODE) => {
args,
);
Tuple(labeled_args) |> DHPat.fresh;
// | TupLabel(_, _) => Tuple([dp]) |> DHPat.fresh
// | Var(name) =>
// Tuple([
// TupLabel(DHPat.Label(name) |> DHPat.fresh, dp) |> DHPat.fresh,
// ])
// |> DHPat.fresh
| _ => dp
};
// TODO: Probably not the right way to deal with casts
// let d2' =
// switch (DHPat.term_of(d2'), DHPat.term_of(dp)) {
// switch (d2'.term, DHPat.term_of(dp)) {
// | (Tuple(_), Tuple(_)) => d2'
// | (Cast(Tuple(_), _, Prod(_)), Tuple(_)) => d2'
// | (Cast(d, Prod(t1), Prod(t2)), Tuple(_)) =>
// Cast(Tuple([d]), Prod(t1), Prod(t2))
// | (Cast(d, t1, Prod(t2)), Tuple(_)) =>
// Cast(Tuple([d]), Prod([t1]), Prod(t2))
// | (_, Tuple([TupLabel(_)])) => Tuple([d2'])
// | (Cast({term: Tuple(_), _}, _, {term: Prod(_), _}), Tuple(_)) => d2'
// | (Cast(d, {term: Prod(t1), _}, {term: Prod(t2), _}), Tuple(_)) =>
// Cast(
// Tuple([d]) |> DHExp.fresh,
// Prod(t1) |> Typ.temp,
// Prod(t2) |> Typ.temp,
// )
// |> DHExp.fresh
// | (Cast(d, t1, {term: Prod(t2), _}), Tuple(_)) =>
// Cast(
// Tuple([d]) |> DHExp.fresh,
// Prod([t1]) |> Typ.temp,
// Prod(t2) |> Typ.temp,
// )
// |> DHExp.fresh
// | (_, Tuple([{term: TupLabel(_), _}])) =>
// Tuple([d2']) |> DHExp.fresh
// | (_, _) => d2'
// };
let.match env'' = (env', matches(dp, d2'));
@@ -676,34 +694,40 @@ module Transition = (EV: EV_MODE) => {
is_value: true,
});
| Dot(d1, d2) =>
let. _ = otherwise(env, (d1, d2) => Dot(d1, d2) |> rewrap)
let. _ = otherwise(env, d2 => Dot(d1, d2) |> rewrap)
and. d1' =
req_value(req(state, env), d1 => Dot1(d1, d2) |> wrap_ctx, d1)
and. d2' =
req_value(req(state, env), d2 => Dot2(d1, d2) |> wrap_ctx, d2);
req_final(req(state, env), d1 => Dot1(d1, d2) |> wrap_ctx, d1);
// TODO: Holes and other cases handled?
switch (DHExp.term_of(d1'), DHExp.term_of(d2')) {
switch (DHExp.term_of(d1'), DHExp.term_of(d2)) {
| (Tuple(ds), Var(name)) =>
Step({
expr:
// let element = LabeledTuple.find_label(DHExp.get_label, ds, name);
switch (LabeledTuple.find_label(DHExp.get_label, ds, name)) {
| Some({term: TupLabel(_, exp), _}) => exp
// TODO (Anthony): operate on casts instead of the original tuple, like static checking.
| _ => raise(EvaluatorError.Exception(BadPatternMatch))
| _ => Undefined |> DHExp.fresh
},
state_update,
kind: Dot,
is_value: false,
})
| (_, Cast(d2', ty, ty')) =>
// TODO: Probably not right
Step({
expr: Cast(Dot(d1, d2') |> fresh, ty, ty') |> fresh,
state_update,
kind: CastAp,
is_value: false,
})
| (Cast(d3', {term: Prod(ts), _}, {term: Prod(ts'), _}), Var(name)) =>
| (Cast(d3', t2, t3), Var(name)) =>
// TODO: doen't work because you get to a cast(1, Unknown, Int) which is Indet
let rec get_typs = (t2, t3) =>
switch (Typ.term_of(t2), Typ.term_of(t3)) {
| (Prod(ts), Prod(ts')) => (ts, ts')
| (Parens(t2), _) => get_typs(t2, t3)
| (_, Parens(t3)) => get_typs(t2, t3)
| (_, _) => ([], [])
};
let (ts, ts') = get_typs(t2, t3);
let ty =
switch (LabeledTuple.find_label(Typ.get_label, ts, name)) {
| Some({term: TupLabel(_, ty), _}) => ty
@@ -720,13 +744,7 @@ module Transition = (EV: EV_MODE) => {
kind: CastAp,
is_value: false,
});
| _ =>
Step({
expr: Dot(d1', d2') |> fresh,
state_update,
kind: Dot,
is_value: false,
})
| _ => Indet
};
| TupLabel(label, d1) =>
// TODO (Anthony): Fix this if needed
5 changes: 4 additions & 1 deletion src/haz3lcore/dynamics/TypeAssignment.re
Original file line number Diff line number Diff line change
@@ -54,7 +54,10 @@ let dhpat_extend_ctx = (dhpat: DHPat.t, ty: Typ.t, ctx: Ctx.t): option(Ctx.t) =>
let entry = Ctx.VarEntry({name, id: Id.invalid, typ: ty});
Some([entry]);
| Tuple(l1) =>
let* ts = Typ.matched_prod_strict(ctx, l1, Pat.get_label, ty);
let (l1, ts) =
Typ.matched_prod(ctx, l1, Pat.get_label, ty, (name, b) =>
TupLabel(Label(name) |> Pat.fresh, b) |> Pat.fresh
);
let* l =
List.map2((dhp, typ) => {dhpat_var_entry(dhp, typ)}, l1, ts)
|> OptUtil.sequence;
46 changes: 29 additions & 17 deletions src/haz3lcore/lang/term/Typ.re
Original file line number Diff line number Diff line change
@@ -159,8 +159,9 @@ let join_type_provenance =
| (SynSwitch, SynSwitch) => SynSwitch
};

let get_label = ty =>
let rec get_label = ty =>
switch (term_of(ty)) {
| Parens(ty) => get_label(ty)
| TupLabel(label, t') =>
switch (term_of(label)) {
| Label(name) => Some((name, t'))
@@ -350,6 +351,10 @@ let rec match_synswitch = (t1: t, t2: t) => {
| (Arrow(_), _) => t1
| (Prod(tys1), Prod(tys2)) when List.length(tys1) == List.length(tys2) =>
// TODO: Rearrange this prod?
let tys1 =
LabeledTuple.rearrange(get_label, get_label, tys1, tys2, (t, x) =>
TupLabel(Label(t) |> temp, x) |> temp
);
let tys = List.map2(match_synswitch, tys1, tys2);
Prod(tys) |> rewrap1;
| (Prod(_), _) => t1
@@ -463,29 +468,36 @@ let matched_label = (ctx, ty) =>
| _ => (Unknown(Internal) |> temp, ty)
};

let rec matched_prod_strict = (ctx, ts, get_label_ts, ty) =>
let rec matched_prod_strict = (ctx, es, get_label_es, ty, constructor) =>
switch (term_of(weak_head_normalize(ctx, ty))) {
| Parens(ty) => matched_prod_strict(ctx, ts, get_label_ts, ty)
| Parens(ty) => matched_prod_strict(ctx, es, get_label_es, ty, constructor)
| Prod(tys) =>
if (List.length(ts) != List.length(tys)) {
None;
if (List.length(es) != List.length(tys)) {
(es, None);
} else {
Some(
LabeledTuple.rearrange(get_label_ts, get_label, ts, tys, (name, b) =>
TupLabel(Label(name) |> temp, b) |> temp
),
(
LabeledTuple.rearrange(get_label, get_label_es, tys, es, constructor),
Some(tys),
);
}
| Unknown(SynSwitch) =>
Some(List.init(List.length(ts), _ => Unknown(SynSwitch) |> temp))
| _ => None
| Unknown(SynSwitch) => (
es,
Some(List.init(List.length(es), _ => Unknown(SynSwitch) |> temp)),
)
| _ => (es, None)
};

let matched_prod = (ctx, ts, get_label_ts, ty) =>
matched_prod_strict(ctx, ts, get_label_ts, ty)
|> Option.value(
~default=List.init(List.length(ts), _ => Unknown(Internal) |> temp),
);
let matched_prod = (ctx, es, get_label_es, ty, constructor) => {
let (es, tys_opt) =
matched_prod_strict(ctx, es, get_label_es, ty, constructor);
(
es,
tys_opt
|> Option.value(
~default=List.init(List.length(es), _ => Unknown(Internal) |> temp),
),
);
};

let rec matched_list_strict = (ctx, ty) =>
switch (term_of(weak_head_normalize(ctx, ty))) {
10 changes: 7 additions & 3 deletions src/haz3lcore/statics/Mode.re
Original file line number Diff line number Diff line change
@@ -70,12 +70,16 @@ let of_label = (ctx: Ctx.t, mode: t): (t, t) =>
(ana(ty1), ana(ty2));
};

let of_prod = (ctx: Ctx.t, mode: t, ts: list('a), filt): list(t) =>
let of_prod =
(ctx: Ctx.t, mode: t, es: list('a), filt, constructor)
: (list('a), list(t)) =>
switch (mode) {
| Syn
| SynFun
| SynTypFun => List.init(List.length(ts), _ => Syn)
| Ana(ty) => ty |> Typ.matched_prod(ctx, ts, filt) |> List.map(ana)
| SynTypFun => (es, List.init(List.length(es), _ => Syn))
| Ana(ty) =>
let (es, tys) = Typ.matched_prod(ctx, es, filt, ty, constructor);
(es, tys |> List.map(ana));
};

let of_cons_hd = (ctx: Ctx.t, mode: t): t =>
Loading