From d4b7ac92a74485fdd50efbe97093845557d92bb6 Mon Sep 17 00:00:00 2001 From: Shubh Agrawal Date: Sun, 4 Dec 2022 23:43:29 -0500 Subject: [PATCH 1/8] begin outline of necessary changes --- src/haz3lcore/statics/Term.re | 23 +++++++++++ src/haz3lweb/view/CursorInspector.re | 58 +++++++++++++++++++++++++++- 2 files changed, 80 insertions(+), 1 deletion(-) diff --git a/src/haz3lcore/statics/Term.re b/src/haz3lcore/statics/Term.re index 90d9d785d1..3d5842bd46 100644 --- a/src/haz3lcore/statics/Term.re +++ b/src/haz3lcore/statics/Term.re @@ -319,6 +319,29 @@ module UPat = { } }; }; + + let rec get_all_bindings = (pat: t) => { + switch (pat.term) { + | Var(x) => [x] + | Parens(pat) + | TypeAnn(pat, _) => get_all_bindings(pat) + | Cons(pat1, pat2) + | Ap(pat1, pat2) => + List.append(get_all_bindings(pat1), get_all_bindings(pat2)) + | ListLit(pats) + | Tuple(pats) => List.flatten(List.map(get_all_bindings, pats)) + | Invalid(_) + | EmptyHole + | MultiHole(_) + | Wild + | Int(_) + | Float(_) + | Bool(_) + | String(_) + | Triv + | Tag(_) => [] + }; + }; }; module UExp = { diff --git a/src/haz3lweb/view/CursorInspector.re b/src/haz3lweb/view/CursorInspector.re index 2bcd1e4017..450dbc3f34 100644 --- a/src/haz3lweb/view/CursorInspector.re +++ b/src/haz3lweb/view/CursorInspector.re @@ -207,6 +207,51 @@ let toggle_context_and_print_ci = (~inject: Update.t => 'a, ci, _) => { inject(Set(ContextInspector)); }; +let binding_uses = + ( + ci: Haz3lcore.Statics.t, + zipper: Haz3lcore.Zipper.t, + _info_map: Haz3lcore.Statics.map, + ) + : Node.t => { + switch (ci) { + | InfoPat({term: _pat, _}) => + // extract the parent index + let parent_exp_gen = + List.find_opt( + gen => { + let anc: Haz3lcore.Ancestor.t = fst(gen); + switch (Haz3lcore.Ancestor.sort(anc)) { + | Exp => true + | _ => false + }; + }, + zipper.relatives.ancestors, + ); + switch (parent_exp_gen) { + | Some((anc, _)) => + div( + List.map( + x => text(string_of_int(x)), + [ + anc.id, + List.length(fst(anc.children)), + List.length(snd(anc.children)), + ], + ), + ) + | _ => div([]) + }; + // iterate over children of the parent exp + // get mold.out (sort) of Exp + // lookup in info_map to find items of cls Var + // for each var, check if the token matches + // if it does, determine if the id of this is in the Ctx + // then how do we get a id from that?? + | _ => div([]) + }; +}; + let inspector_view = ( ~inject, @@ -214,6 +259,8 @@ let inspector_view = ~show_lang_doc: bool, id: int, ci: Haz3lcore.Statics.t, + zipper: Haz3lcore.Zipper.t, + info_map: Haz3lcore.Statics.map, ) : Node.t => div( @@ -228,6 +275,7 @@ let inspector_view = [ extra_view(settings.context_inspector, id, ci), view_of_info(~inject, ~show_lang_doc, ci), + binding_uses(ci, zipper, info_map), CtxInspector.inspector_view(~inject, ~settings, id, ci), ], ); @@ -250,7 +298,15 @@ let view = | Some(index) => switch (Haz3lcore.Id.Map.find_opt(index, info_map)) { | Some(ci) => - inspector_view(~inject, ~settings, ~show_lang_doc, index, ci) + inspector_view( + ~inject, + ~settings, + ~show_lang_doc, + index, + ci, + zipper, + info_map, + ) | None => div( ~attr=clss(["cursor-inspector"]), From 7f1f4ec6267c9a340ddce408f66c35a61353e23b Mon Sep 17 00:00:00 2001 From: Shubh Agrawal Date: Fri, 13 Jan 2023 01:48:29 -0500 Subject: [PATCH 2/8] add binding expression ids to info_pat --- src/haz3lcore/statics/Statics.re | 49 ++++++++++++++------ src/haz3lweb/view/CursorInspector.re | 68 +++++++++++++++++----------- 2 files changed, 76 insertions(+), 41 deletions(-) diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index 86e4a8ca34..1fca27ff93 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -38,7 +38,8 @@ type info_pat = { term: Term.UPat.t, mode: Typ.mode, self: Typ.self, - ctx: Ctx.t // TODO: detect in-pattern shadowing + ctx: Ctx.t, // TODO: detect in-pattern shadowing + binding_exp: list(Id.t), }; /* (Syntactic) Types are assigned their corresponding semantic type. */ @@ -415,7 +416,8 @@ and uexp_to_info_map = ); | Fun(pat, body) => let (mode_pat, mode_body) = Typ.matched_arrow_mode(mode); - let (ty_pat, ctx_pat, m_pat) = upat_to_info_map(~mode=mode_pat, pat); + let (ty_pat, ctx_pat, m_pat) = + upat_to_info_map(~mode=mode_pat, ~binding_exp=ids, pat); let ctx_body = VarMap.concat(ctx, ctx_pat); let (ty_body, free_body, m_body) = uexp_to_info_map(~ctx=ctx_body, ~mode=mode_body, body); @@ -425,12 +427,14 @@ and uexp_to_info_map = union_m([m_pat, m_body]), ); | Let(pat, def, body) => - let (ty_pat, ctx_pat, _m_pat) = upat_to_info_map(~mode=Syn, pat); + let (ty_pat, ctx_pat, _m_pat) = + upat_to_info_map(~mode=Syn, ~binding_exp=ids, pat); let def_ctx = extend_let_def_ctx(ctx, pat, ctx_pat, def); let (ty_def, free_def, m_def) = uexp_to_info_map(~ctx=def_ctx, ~mode=Ana(ty_pat), def); /* Analyze pattern to incorporate def type into ctx */ - let (_, ctx_pat_ana, m_pat) = upat_to_info_map(~mode=Ana(ty_def), pat); + let (_, ctx_pat_ana, m_pat) = + upat_to_info_map(~mode=Ana(ty_def), ~binding_exp=ids, pat); let ctx_body = VarMap.concat(ctx, ctx_pat_ana); let (ty_body, free_body, m_body) = uexp_to_info_map(~ctx=ctx_body, ~mode, body); @@ -443,7 +447,10 @@ and uexp_to_info_map = let (ty_scrut, free_scrut, m_scrut) = go(~mode=Syn, scrut); let (pats, branches) = List.split(rules); let pat_infos = - List.map(upat_to_info_map(~mode=Typ.Ana(ty_scrut)), pats); + List.map( + upat_to_info_map(~mode=Typ.Ana(ty_scrut), ~binding_exp=ids), + pats, + ); let branch_infos = List.map2( (branch, (_, ctx_pat, _)) => @@ -469,6 +476,7 @@ and upat_to_info_map = ( ~ctx=Ctx.empty, ~mode: Typ.mode=Typ.Syn, + ~binding_exp: list(Id.t)=[Id.invalid], {ids, term} as upat: Term.UPat.t, ) : (Typ.t, Ctx.t, map) => { @@ -476,7 +484,11 @@ and upat_to_info_map = let add = (~self, ~ctx, m) => ( typ_after_fix(mode, self), ctx, - add_info(ids, InfoPat({cls, self, mode, ctx, term: upat}), m), + add_info( + ids, + InfoPat({cls, self, mode, ctx, binding_exp, term: upat}), + m, + ), ); let atomic = self => add(~self, ~ctx, Id.Map.empty); let unknown = Typ.Just(Unknown(SynSwitch)); @@ -503,7 +515,8 @@ and upat_to_info_map = let (ctx, infos) = List.fold_left2( ((ctx, infos), e, mode) => { - let (_, ctx, _) as info = upat_to_info_map(~mode, ~ctx, e); + let (_, ctx, _) as info = + upat_to_info_map(~mode, ~ctx, ~binding_exp, e); (ctx, infos @ [info]); }, (ctx, []), @@ -520,15 +533,17 @@ and upat_to_info_map = ) | Some(ty) => Just(List(ty)) }; - let info: t = InfoPat({cls, self, mode, ctx, term: upat}); + let info: t = InfoPat({cls, self, mode, binding_exp, ctx, term: upat}); let m = union_m(List.map(((_, _, m)) => m, infos)); /* Add an entry for the id of each comma tile */ let m = List.fold_left((m, id) => Id.Map.add(id, info, m), m, ids); (typ_after_fix(mode, self), ctx, m); | Cons(hd, tl) => let mode_elem = Typ.matched_list_mode(mode); - let (ty, ctx, m_hd) = upat_to_info_map(~ctx, ~mode=mode_elem, hd); - let (_, ctx, m_tl) = upat_to_info_map(~ctx, ~mode=Ana(List(ty)), tl); + let (ty, ctx, m_hd) = + upat_to_info_map(~ctx, ~mode=mode_elem, ~binding_exp, hd); + let (_, ctx, m_tl) = + upat_to_info_map(~ctx, ~mode=Ana(List(ty)), ~binding_exp, tl); add(~self=Just(List(ty)), ~ctx, union_m([m_hd, m_tl])); | Tag(name) => switch (BuiltinADTs.get_tag_typ(name)) { @@ -549,7 +564,8 @@ and upat_to_info_map = let (ctx, infos) = List.fold_left2( ((ctx, infos), e, mode) => { - let (_, ctx, _) as info = upat_to_info_map(~mode, ~ctx, e); + let (_, ctx, _) as info = + upat_to_info_map(~mode, ~ctx, ~binding_exp, e); (ctx, infos @ [info]); }, (ctx, []), @@ -560,18 +576,21 @@ and upat_to_info_map = let m = union_m(List.map(((_, _, m)) => m, infos)); add(~self, ~ctx, m); | Parens(p) => - let (ty, ctx, m) = upat_to_info_map(~ctx, ~mode, p); + let (ty, ctx, m) = upat_to_info_map(~ctx, ~mode, ~binding_exp, p); add(~self=Just(ty), ~ctx, m); | Ap(fn, arg) => /* Contructor application */ /* Function position mode Ana(Hole->Hole) instead of Syn */ - let (ty_fn, ctx, m_fn) = upat_to_info_map(~ctx, ~mode=Typ.ap_mode, fn); + let (ty_fn, ctx, m_fn) = + upat_to_info_map(~ctx, ~mode=Typ.ap_mode, ~binding_exp, fn); let (ty_in, ty_out) = Typ.matched_arrow(ty_fn); - let (_, ctx, m_arg) = upat_to_info_map(~ctx, ~mode=Ana(ty_in), arg); + let (_, ctx, m_arg) = + upat_to_info_map(~ctx, ~mode=Ana(ty_in), ~binding_exp, arg); add(~self=Just(ty_out), ~ctx, union_m([m_fn, m_arg])); | TypeAnn(p, ty) => let (ty_ann, m_typ) = utyp_to_info_map(ty); - let (_ty, ctx, m) = upat_to_info_map(~ctx, ~mode=Ana(ty_ann), p); + let (_ty, ctx, m) = + upat_to_info_map(~ctx, ~mode=Ana(ty_ann), ~binding_exp, p); add(~self=Just(ty_ann), ~ctx, union_m([m, m_typ])); }; } diff --git a/src/haz3lweb/view/CursorInspector.re b/src/haz3lweb/view/CursorInspector.re index 450dbc3f34..20df22a80b 100644 --- a/src/haz3lweb/view/CursorInspector.re +++ b/src/haz3lweb/view/CursorInspector.re @@ -210,39 +210,55 @@ let toggle_context_and_print_ci = (~inject: Update.t => 'a, ci, _) => { let binding_uses = ( ci: Haz3lcore.Statics.t, - zipper: Haz3lcore.Zipper.t, + _zipper: Haz3lcore.Zipper.t, _info_map: Haz3lcore.Statics.map, ) : Node.t => { switch (ci) { - | InfoPat({term: _pat, _}) => - // extract the parent index - let parent_exp_gen = - List.find_opt( - gen => { - let anc: Haz3lcore.Ancestor.t = fst(gen); - switch (Haz3lcore.Ancestor.sort(anc)) { - | Exp => true - | _ => false - }; + | InfoPat({term: _pat, binding_exp, _}) => + let _ = + List.map( + id => { + print_int(id); + print_string(", "); }, - zipper.relatives.ancestors, + binding_exp, ); - switch (parent_exp_gen) { - | Some((anc, _)) => - div( - List.map( - x => text(string_of_int(x)), - [ - anc.id, - List.length(fst(anc.children)), - List.length(snd(anc.children)), - ], - ), - ) - | _ => div([]) - }; + print_newline(); + div([]); + // extract the parent index + /* let parent_exp_gen = */ + /* List.find_opt( */ + /* gen => { */ + /* let anc: Haz3lcore.Ancestor.t = fst(gen); */ + /* switch (Haz3lcore.Ancestor.sort(anc)) { */ + /* | Exp => true */ + /* | Any => true */ + /* | _ => false */ + /* }; */ + /* }, */ + /* zipper.relatives.ancestors, */ + /* ); */ + /* switch (parent_exp_gen) { */ + /* | Some((anc, _)) => */ + /* switch (Haz3lcore.Id.Map.find_opt(anc.id, info_map)) { */ + /* | Some(InfoExp(info)) => */ + /* print_int(anc.id); */ + /* let _ = */ + /* List.map((_, co_entry) => print_endline(co_entry), info.free); */ + /* (); */ + /* | None => print_string("nothing in info_map") */ + /* | _ => () */ + /* }; */ + /* print_newline(); */ + /* div(List.map(x => text(string_of_int(x)), [anc.id])); */ + /* | _ => div([]) */ + /* }; */ // iterate over children of the parent exp + // co-context of binding expression will have the uids of variable uses + // in the info_map, store the binding uses + // make it a list of co-contexts for mutual recursion to work + // test recursive and mutually recursive bindings // get mold.out (sort) of Exp // lookup in info_map to find items of cls Var // for each var, check if the token matches From 01cc0bc1a4d59b67d1f02881ce0d9ae20800479e Mon Sep 17 00:00:00 2001 From: Shubh Agrawal Date: Tue, 17 Jan 2023 00:24:18 -0500 Subject: [PATCH 3/8] correctly find uses of binding in let and fun expressions --- src/haz3lcore/VarMap.re | 3 + src/haz3lweb/view/CursorInspector.re | 102 +++++++++++++++++++++++++-- 2 files changed, 99 insertions(+), 6 deletions(-) diff --git a/src/haz3lcore/VarMap.re b/src/haz3lcore/VarMap.re index 85bdd70980..394969139a 100644 --- a/src/haz3lcore/VarMap.re +++ b/src/haz3lcore/VarMap.re @@ -19,6 +19,9 @@ let concat = (ctx, new_ctx) => new_ctx @ ctx; let lookup = (ctx, x) => List.assoc_opt(x, ctx); +let lookup_all = (ctx, x) => + List.fold_left((vs, (tok, v)) => {tok == x ? [v, ...vs] : vs}, [], ctx); + let contains = (ctx, x) => List.mem_assoc(x, ctx); let map = (f, xs) => List.map(((x, _) as xa) => (x, f(xa)), xs); diff --git a/src/haz3lweb/view/CursorInspector.re b/src/haz3lweb/view/CursorInspector.re index 20df22a80b..57a8536e0d 100644 --- a/src/haz3lweb/view/CursorInspector.re +++ b/src/haz3lweb/view/CursorInspector.re @@ -207,24 +207,114 @@ let toggle_context_and_print_ci = (~inject: Update.t => 'a, ci, _) => { inject(Set(ContextInspector)); }; +type usage_info = (Haz3lcore.Token.t, list(Haz3lcore.Id.t)); let binding_uses = ( ci: Haz3lcore.Statics.t, _zipper: Haz3lcore.Zipper.t, - _info_map: Haz3lcore.Statics.map, + info_map: Haz3lcore.Statics.map, ) : Node.t => { switch (ci) { - | InfoPat({term: _pat, binding_exp, _}) => - let _ = + | InfoPat({term, binding_exp, _}) => + let bindings = + List.sort_uniq(compare, Haz3lcore.Term.UPat.get_all_bindings(term)); + let exps_to_search: list(list(Haz3lcore.Statics.info_exp)) = List.map( id => { - print_int(id); - print_string(", "); + switch (Haz3lcore.Id.Map.find_opt(id, info_map)) { + | Some(InfoExp(info_ancestor)) => + let body_infos: list(Haz3lcore.Statics.info_exp) = + switch (info_ancestor.term.term) { + | Let(_, _, body) + | Fun(_, body) => + List.fold_left( + (exps, id) => { + switch (Haz3lcore.Id.Map.find_opt(id, info_map)) { + | Some(InfoExp(info_body)) => [info_body, ...exps] + | _ => exps + } + }, + [], + body.ids, + ) + // | Match(_, rules) => { TODO: this is more complicated } + | _ => [] + }; + body_infos; + | _ => [] + } }, binding_exp, ); - print_newline(); + let empty_bindings_map: list(usage_info) = + List.map(var => (var, []), bindings); + let bindings_map = + List.fold_left( + (binding_map: list(usage_info), info_exp: Haz3lcore.Statics.info_exp) => { + let updated_map: list(usage_info) = + List.map( + (usage_pair: usage_info) => { + let (var, ids) = usage_pair; + let new_ids: list(Haz3lcore.Id.t) = + List.map( + (item: Haz3lcore.Ctx.co_item) => {item.id}, + List.flatten( + Haz3lcore.VarMap.lookup_all(info_exp.free, var), + ), + ); + print_string("co_ctx | "); + let _ = + List.map( + coctx_pair => { + let (var, co_items) = coctx_pair; + print_string(var); + print_string(":["); + let _ = + List.map( + (co_it: Haz3lcore.Ctx.co_item) => { + print_int(co_it.id); + print_string(","); + }, + co_items, + ); + print_string("]; "); + }, + info_exp.free, + ); + let all_ids: list(Haz3lcore.Id.t) = + List.sort_uniq(compare, new_ids @ ids); + let pair: (Haz3lcore.Token.t, list(Haz3lcore.Id.t)) = ( + var, + all_ids, + ); + pair; + }, + binding_map, + ); + updated_map; + }, + empty_bindings_map, + List.flatten(exps_to_search), + ); + let _ = + List.map( + (usage_pair: usage_info) => { + let (var, ids) = usage_pair; + print_string(var); + print_string(": "); + let _ = + List.map( + id => { + print_int(id); + print_string(", "); + }, + ids, + ); + print_newline(); + }, + bindings_map, + ); div([]); // extract the parent index /* let parent_exp_gen = */ From 52b4ef695779bba80ab95d4fc4a30561e2077ba8 Mon Sep 17 00:00:00 2001 From: Shubh Agrawal Date: Wed, 18 Jan 2023 22:56:20 -0500 Subject: [PATCH 4/8] add support for recursive let and match expressions --- src/haz3lcore/statics/Statics.re | 43 ++++++++++++++-------------- src/haz3lweb/view/CursorInspector.re | 35 ++++++---------------- 2 files changed, 31 insertions(+), 47 deletions(-) diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index 1fca27ff93..eb6b23981e 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -39,7 +39,7 @@ type info_pat = { mode: Typ.mode, self: Typ.self, ctx: Ctx.t, // TODO: detect in-pattern shadowing - binding_exp: list(Id.t), + body_ids: list(Id.t), }; /* (Syntactic) Types are assigned their corresponding semantic type. */ @@ -417,7 +417,7 @@ and uexp_to_info_map = | Fun(pat, body) => let (mode_pat, mode_body) = Typ.matched_arrow_mode(mode); let (ty_pat, ctx_pat, m_pat) = - upat_to_info_map(~mode=mode_pat, ~binding_exp=ids, pat); + upat_to_info_map(~mode=mode_pat, ~body_ids=body.ids, pat); let ctx_body = VarMap.concat(ctx, ctx_pat); let (ty_body, free_body, m_body) = uexp_to_info_map(~ctx=ctx_body, ~mode=mode_body, body); @@ -428,13 +428,13 @@ and uexp_to_info_map = ); | Let(pat, def, body) => let (ty_pat, ctx_pat, _m_pat) = - upat_to_info_map(~mode=Syn, ~binding_exp=ids, pat); + upat_to_info_map(~mode=Syn, ~body_ids=body.ids @ def.ids, pat); let def_ctx = extend_let_def_ctx(ctx, pat, ctx_pat, def); let (ty_def, free_def, m_def) = uexp_to_info_map(~ctx=def_ctx, ~mode=Ana(ty_pat), def); /* Analyze pattern to incorporate def type into ctx */ let (_, ctx_pat_ana, m_pat) = - upat_to_info_map(~mode=Ana(ty_def), ~binding_exp=ids, pat); + upat_to_info_map(~mode=Ana(ty_def), ~body_ids=body.ids @ def.ids, pat); let ctx_body = VarMap.concat(ctx, ctx_pat_ana); let (ty_body, free_body, m_body) = uexp_to_info_map(~ctx=ctx_body, ~mode, body); @@ -447,8 +447,13 @@ and uexp_to_info_map = let (ty_scrut, free_scrut, m_scrut) = go(~mode=Syn, scrut); let (pats, branches) = List.split(rules); let pat_infos = - List.map( - upat_to_info_map(~mode=Typ.Ana(ty_scrut), ~binding_exp=ids), + List.mapi( + (i, p) => + upat_to_info_map( + ~mode=Typ.Ana(ty_scrut), + ~body_ids=List.nth(branches, i).ids, + p, + ), pats, ); let branch_infos = @@ -476,7 +481,7 @@ and upat_to_info_map = ( ~ctx=Ctx.empty, ~mode: Typ.mode=Typ.Syn, - ~binding_exp: list(Id.t)=[Id.invalid], + ~body_ids: list(Id.t)=[Id.invalid], {ids, term} as upat: Term.UPat.t, ) : (Typ.t, Ctx.t, map) => { @@ -484,11 +489,7 @@ and upat_to_info_map = let add = (~self, ~ctx, m) => ( typ_after_fix(mode, self), ctx, - add_info( - ids, - InfoPat({cls, self, mode, ctx, binding_exp, term: upat}), - m, - ), + add_info(ids, InfoPat({cls, self, mode, ctx, body_ids, term: upat}), m), ); let atomic = self => add(~self, ~ctx, Id.Map.empty); let unknown = Typ.Just(Unknown(SynSwitch)); @@ -516,7 +517,7 @@ and upat_to_info_map = List.fold_left2( ((ctx, infos), e, mode) => { let (_, ctx, _) as info = - upat_to_info_map(~mode, ~ctx, ~binding_exp, e); + upat_to_info_map(~mode, ~ctx, ~body_ids, e); (ctx, infos @ [info]); }, (ctx, []), @@ -533,7 +534,7 @@ and upat_to_info_map = ) | Some(ty) => Just(List(ty)) }; - let info: t = InfoPat({cls, self, mode, binding_exp, ctx, term: upat}); + let info: t = InfoPat({cls, self, mode, body_ids, ctx, term: upat}); let m = union_m(List.map(((_, _, m)) => m, infos)); /* Add an entry for the id of each comma tile */ let m = List.fold_left((m, id) => Id.Map.add(id, info, m), m, ids); @@ -541,9 +542,9 @@ and upat_to_info_map = | Cons(hd, tl) => let mode_elem = Typ.matched_list_mode(mode); let (ty, ctx, m_hd) = - upat_to_info_map(~ctx, ~mode=mode_elem, ~binding_exp, hd); + upat_to_info_map(~ctx, ~mode=mode_elem, ~body_ids, hd); let (_, ctx, m_tl) = - upat_to_info_map(~ctx, ~mode=Ana(List(ty)), ~binding_exp, tl); + upat_to_info_map(~ctx, ~mode=Ana(List(ty)), ~body_ids, tl); add(~self=Just(List(ty)), ~ctx, union_m([m_hd, m_tl])); | Tag(name) => switch (BuiltinADTs.get_tag_typ(name)) { @@ -565,7 +566,7 @@ and upat_to_info_map = List.fold_left2( ((ctx, infos), e, mode) => { let (_, ctx, _) as info = - upat_to_info_map(~mode, ~ctx, ~binding_exp, e); + upat_to_info_map(~mode, ~ctx, ~body_ids, e); (ctx, infos @ [info]); }, (ctx, []), @@ -576,21 +577,21 @@ and upat_to_info_map = let m = union_m(List.map(((_, _, m)) => m, infos)); add(~self, ~ctx, m); | Parens(p) => - let (ty, ctx, m) = upat_to_info_map(~ctx, ~mode, ~binding_exp, p); + let (ty, ctx, m) = upat_to_info_map(~ctx, ~mode, ~body_ids, p); add(~self=Just(ty), ~ctx, m); | Ap(fn, arg) => /* Contructor application */ /* Function position mode Ana(Hole->Hole) instead of Syn */ let (ty_fn, ctx, m_fn) = - upat_to_info_map(~ctx, ~mode=Typ.ap_mode, ~binding_exp, fn); + upat_to_info_map(~ctx, ~mode=Typ.ap_mode, ~body_ids, fn); let (ty_in, ty_out) = Typ.matched_arrow(ty_fn); let (_, ctx, m_arg) = - upat_to_info_map(~ctx, ~mode=Ana(ty_in), ~binding_exp, arg); + upat_to_info_map(~ctx, ~mode=Ana(ty_in), ~body_ids, arg); add(~self=Just(ty_out), ~ctx, union_m([m_fn, m_arg])); | TypeAnn(p, ty) => let (ty_ann, m_typ) = utyp_to_info_map(ty); let (_ty, ctx, m) = - upat_to_info_map(~ctx, ~mode=Ana(ty_ann), ~binding_exp, p); + upat_to_info_map(~ctx, ~mode=Ana(ty_ann), ~body_ids, p); add(~self=Just(ty_ann), ~ctx, union_m([m, m_typ])); }; } diff --git a/src/haz3lweb/view/CursorInspector.re b/src/haz3lweb/view/CursorInspector.re index 57a8536e0d..9f5d7f4a26 100644 --- a/src/haz3lweb/view/CursorInspector.re +++ b/src/haz3lweb/view/CursorInspector.re @@ -216,36 +216,19 @@ let binding_uses = ) : Node.t => { switch (ci) { - | InfoPat({term, binding_exp, _}) => + | InfoPat({term, body_ids, _}) => let bindings = List.sort_uniq(compare, Haz3lcore.Term.UPat.get_all_bindings(term)); - let exps_to_search: list(list(Haz3lcore.Statics.info_exp)) = - List.map( - id => { + let exps_to_search: list(Haz3lcore.Statics.info_exp) = + List.fold_left( + (exps, id) => { switch (Haz3lcore.Id.Map.find_opt(id, info_map)) { - | Some(InfoExp(info_ancestor)) => - let body_infos: list(Haz3lcore.Statics.info_exp) = - switch (info_ancestor.term.term) { - | Let(_, _, body) - | Fun(_, body) => - List.fold_left( - (exps, id) => { - switch (Haz3lcore.Id.Map.find_opt(id, info_map)) { - | Some(InfoExp(info_body)) => [info_body, ...exps] - | _ => exps - } - }, - [], - body.ids, - ) - // | Match(_, rules) => { TODO: this is more complicated } - | _ => [] - }; - body_infos; - | _ => [] + | Some(InfoExp(info_body)) => [info_body, ...exps] + | _ => exps } }, - binding_exp, + [], + body_ids, ); let empty_bindings_map: list(usage_info) = List.map(var => (var, []), bindings); @@ -295,7 +278,7 @@ let binding_uses = updated_map; }, empty_bindings_map, - List.flatten(exps_to_search), + exps_to_search, ); let _ = List.map( From ba6596f2fbc669709e454fe7f184f2dc4ad3ba02 Mon Sep 17 00:00:00 2001 From: Shubh Agrawal Date: Sun, 22 Jan 2023 01:04:11 -0500 Subject: [PATCH 5/8] move new code into Statics --- src/haz3lcore/statics/Statics.re | 84 +++++++++++++++ src/haz3lweb/view/CursorInspector.re | 147 +-------------------------- 2 files changed, 85 insertions(+), 146 deletions(-) diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index eb6b23981e..29db9ac646 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -161,6 +161,90 @@ let is_error = (ci: t): bool => { }; }; +type usage_info = (Token.t, list(Id.t)); +let binding_uses = (ci: t, info_map: map): list(usage_info) => { + switch (ci) { + | InfoPat({term, body_ids, _}) => + let bindings = List.sort_uniq(compare, Term.UPat.get_all_bindings(term)); + let exps_to_search: list(info_exp) = + List.fold_left( + (exps, id) => { + switch (Id.Map.find_opt(id, info_map)) { + | Some(InfoExp(info_body)) => [info_body, ...exps] + | _ => exps + } + }, + [], + body_ids, + ); + let empty_bindings_map: list(usage_info) = + List.map(var => (var, []), bindings); + let bindings_map = + List.fold_left( + (binding_map: list(usage_info), info_exp: info_exp) => { + let updated_map: list(usage_info) = + List.map( + (usage_pair: usage_info) => { + let (var, ids) = usage_pair; + let new_ids: list(Id.t) = + List.map( + (item: Ctx.co_item) => {item.id}, + List.flatten(VarMap.lookup_all(info_exp.free, var)), + ); + print_string("co_ctx | "); + let _ = + List.map( + coctx_pair => { + let (var, co_items) = coctx_pair; + print_string(var); + print_string(":["); + let _ = + List.map( + (co_it: Ctx.co_item) => { + print_int(co_it.id); + print_string(","); + }, + co_items, + ); + print_string("]; "); + }, + info_exp.free, + ); + let all_ids: list(Id.t) = + List.sort_uniq(compare, new_ids @ ids); + let pair: (Token.t, list(Id.t)) = (var, all_ids); + pair; + }, + binding_map, + ); + updated_map; + }, + empty_bindings_map, + exps_to_search, + ); + let _ = + List.map( + (usage_pair: usage_info) => { + let (var, ids) = usage_pair; + print_string(var); + print_string(": "); + let _ = + List.map( + id => { + print_int(id); + print_string(", "); + }, + ids, + ); + print_newline(); + }, + bindings_map, + ); + bindings_map; + | _ => [] + }; +}; + /* Determined the type of an expression or pattern 'after hole wrapping'; that is, all ill-typed terms are considered to be 'wrapped in non-empty holes', i.e. assigned Unknown type. */ diff --git a/src/haz3lweb/view/CursorInspector.re b/src/haz3lweb/view/CursorInspector.re index 9f5d7f4a26..2bcd1e4017 100644 --- a/src/haz3lweb/view/CursorInspector.re +++ b/src/haz3lweb/view/CursorInspector.re @@ -207,140 +207,6 @@ let toggle_context_and_print_ci = (~inject: Update.t => 'a, ci, _) => { inject(Set(ContextInspector)); }; -type usage_info = (Haz3lcore.Token.t, list(Haz3lcore.Id.t)); -let binding_uses = - ( - ci: Haz3lcore.Statics.t, - _zipper: Haz3lcore.Zipper.t, - info_map: Haz3lcore.Statics.map, - ) - : Node.t => { - switch (ci) { - | InfoPat({term, body_ids, _}) => - let bindings = - List.sort_uniq(compare, Haz3lcore.Term.UPat.get_all_bindings(term)); - let exps_to_search: list(Haz3lcore.Statics.info_exp) = - List.fold_left( - (exps, id) => { - switch (Haz3lcore.Id.Map.find_opt(id, info_map)) { - | Some(InfoExp(info_body)) => [info_body, ...exps] - | _ => exps - } - }, - [], - body_ids, - ); - let empty_bindings_map: list(usage_info) = - List.map(var => (var, []), bindings); - let bindings_map = - List.fold_left( - (binding_map: list(usage_info), info_exp: Haz3lcore.Statics.info_exp) => { - let updated_map: list(usage_info) = - List.map( - (usage_pair: usage_info) => { - let (var, ids) = usage_pair; - let new_ids: list(Haz3lcore.Id.t) = - List.map( - (item: Haz3lcore.Ctx.co_item) => {item.id}, - List.flatten( - Haz3lcore.VarMap.lookup_all(info_exp.free, var), - ), - ); - print_string("co_ctx | "); - let _ = - List.map( - coctx_pair => { - let (var, co_items) = coctx_pair; - print_string(var); - print_string(":["); - let _ = - List.map( - (co_it: Haz3lcore.Ctx.co_item) => { - print_int(co_it.id); - print_string(","); - }, - co_items, - ); - print_string("]; "); - }, - info_exp.free, - ); - let all_ids: list(Haz3lcore.Id.t) = - List.sort_uniq(compare, new_ids @ ids); - let pair: (Haz3lcore.Token.t, list(Haz3lcore.Id.t)) = ( - var, - all_ids, - ); - pair; - }, - binding_map, - ); - updated_map; - }, - empty_bindings_map, - exps_to_search, - ); - let _ = - List.map( - (usage_pair: usage_info) => { - let (var, ids) = usage_pair; - print_string(var); - print_string(": "); - let _ = - List.map( - id => { - print_int(id); - print_string(", "); - }, - ids, - ); - print_newline(); - }, - bindings_map, - ); - div([]); - // extract the parent index - /* let parent_exp_gen = */ - /* List.find_opt( */ - /* gen => { */ - /* let anc: Haz3lcore.Ancestor.t = fst(gen); */ - /* switch (Haz3lcore.Ancestor.sort(anc)) { */ - /* | Exp => true */ - /* | Any => true */ - /* | _ => false */ - /* }; */ - /* }, */ - /* zipper.relatives.ancestors, */ - /* ); */ - /* switch (parent_exp_gen) { */ - /* | Some((anc, _)) => */ - /* switch (Haz3lcore.Id.Map.find_opt(anc.id, info_map)) { */ - /* | Some(InfoExp(info)) => */ - /* print_int(anc.id); */ - /* let _ = */ - /* List.map((_, co_entry) => print_endline(co_entry), info.free); */ - /* (); */ - /* | None => print_string("nothing in info_map") */ - /* | _ => () */ - /* }; */ - /* print_newline(); */ - /* div(List.map(x => text(string_of_int(x)), [anc.id])); */ - /* | _ => div([]) */ - /* }; */ - // iterate over children of the parent exp - // co-context of binding expression will have the uids of variable uses - // in the info_map, store the binding uses - // make it a list of co-contexts for mutual recursion to work - // test recursive and mutually recursive bindings - // get mold.out (sort) of Exp - // lookup in info_map to find items of cls Var - // for each var, check if the token matches - // if it does, determine if the id of this is in the Ctx - // then how do we get a id from that?? - | _ => div([]) - }; -}; - let inspector_view = ( ~inject, @@ -348,8 +214,6 @@ let inspector_view = ~show_lang_doc: bool, id: int, ci: Haz3lcore.Statics.t, - zipper: Haz3lcore.Zipper.t, - info_map: Haz3lcore.Statics.map, ) : Node.t => div( @@ -364,7 +228,6 @@ let inspector_view = [ extra_view(settings.context_inspector, id, ci), view_of_info(~inject, ~show_lang_doc, ci), - binding_uses(ci, zipper, info_map), CtxInspector.inspector_view(~inject, ~settings, id, ci), ], ); @@ -387,15 +250,7 @@ let view = | Some(index) => switch (Haz3lcore.Id.Map.find_opt(index, info_map)) { | Some(ci) => - inspector_view( - ~inject, - ~settings, - ~show_lang_doc, - index, - ci, - zipper, - info_map, - ) + inspector_view(~inject, ~settings, ~show_lang_doc, index, ci) | None => div( ~attr=clss(["cursor-inspector"]), From 709d076b4ade620507d201671c32ec77f319bdf2 Mon Sep 17 00:00:00 2001 From: Shubh Agrawal Date: Sat, 4 Feb 2023 23:39:00 -0500 Subject: [PATCH 6/8] fix bug with match co-ctx --- src/haz3lcore/statics/Statics.re | 13 +++++++++++-- src/haz3lweb/view/CursorInspector.re | 19 ++++++++++++++++++- 2 files changed, 29 insertions(+), 3 deletions(-) diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index 29db9ac646..33545dad5e 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -514,6 +514,7 @@ and uexp_to_info_map = let (ty_pat, ctx_pat, _m_pat) = upat_to_info_map(~mode=Syn, ~body_ids=body.ids @ def.ids, pat); let def_ctx = extend_let_def_ctx(ctx, pat, ctx_pat, def); + // use this ^^ to determine if recursive let or not let (ty_def, free_def, m_def) = uexp_to_info_map(~ctx=def_ctx, ~mode=Ana(ty_pat), def); /* Analyze pattern to incorporate def type into ctx */ @@ -555,9 +556,17 @@ and uexp_to_info_map = ); let pat_ms = List.map(((_, _, m)) => m, pat_infos); let branch_ms = List.map(((_, _, m)) => m, branch_infos); - let branch_frees = List.map(((_, free, _)) => free, branch_infos); + let branch_frees = + List.map2( + ((_, body_free, _), (_, ctx_pat, _)) => { + Ctx.subtract_typ(ctx_pat, body_free) + }, + branch_infos, + pat_infos, + ); let self = Typ.Joined(Fun.id, branch_sources); - let free = Ctx.union([free_scrut] @ branch_frees); + /* let free = Ctx.union([free_scrut] @ branch_frees); */ + let free = Ctx.union([free_scrut, ...branch_frees]); add(~self, ~free, union_m([m_scrut] @ pat_ms @ branch_ms)); }; } diff --git a/src/haz3lweb/view/CursorInspector.re b/src/haz3lweb/view/CursorInspector.re index 2bcd1e4017..d18ccd613e 100644 --- a/src/haz3lweb/view/CursorInspector.re +++ b/src/haz3lweb/view/CursorInspector.re @@ -250,7 +250,24 @@ let view = | Some(index) => switch (Haz3lcore.Id.Map.find_opt(index, info_map)) { | Some(ci) => - inspector_view(~inject, ~settings, ~show_lang_doc, index, ci) + let _ = + List.map( + usage => { + print_string(fst(usage)); + print_string(": "); + let _ = + List.map( + id => { + print_int(id); + print_string(", "); + }, + snd(usage), + ); + print_newline(); + }, + Haz3lcore.Statics.binding_uses(ci, info_map), + ); + inspector_view(~inject, ~settings, ~show_lang_doc, index, ci); | None => div( ~attr=clss(["cursor-inspector"]), From b1adad15a617968c4e645049bb40a644a4a9cf4f Mon Sep 17 00:00:00 2001 From: Shubh Agrawal Date: Sun, 5 Feb 2023 00:31:36 -0500 Subject: [PATCH 7/8] only use definition ids if let is recursive --- src/haz3lcore/statics/Statics.re | 26 ++++++++++++++++++++------ 1 file changed, 20 insertions(+), 6 deletions(-) diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index 33545dad5e..bd7aa246e4 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -311,12 +311,13 @@ let add_info = (ids, info: 'a, m: Ptmap.t('a)) => |> List.fold_left(Id.Map.disj_union, m); let extend_let_def_ctx = - (ctx: Ctx.t, pat: Term.UPat.t, pat_ctx: Ctx.t, def: Term.UExp.t) => + (ctx: Ctx.t, pat: Term.UPat.t, pat_ctx: Ctx.t, def: Term.UExp.t) + : (Ctx.t, bool) => if (Term.UPat.is_tuple_of_arrows(pat) && Term.UExp.is_tuple_of_functions(def)) { - VarMap.concat(ctx, pat_ctx); + (VarMap.concat(ctx, pat_ctx), true); } else { - ctx; + (ctx, false); }; let typ_exp_binop_bin_int: Term.UExp.op_bin_int => Typ.t = @@ -513,19 +514,32 @@ and uexp_to_info_map = | Let(pat, def, body) => let (ty_pat, ctx_pat, _m_pat) = upat_to_info_map(~mode=Syn, ~body_ids=body.ids @ def.ids, pat); - let def_ctx = extend_let_def_ctx(ctx, pat, ctx_pat, def); + let (def_ctx, is_rec) = extend_let_def_ctx(ctx, pat, ctx_pat, def); // use this ^^ to determine if recursive let or not let (ty_def, free_def, m_def) = uexp_to_info_map(~ctx=def_ctx, ~mode=Ana(ty_pat), def); /* Analyze pattern to incorporate def type into ctx */ + let pat_body_ids = + if (is_rec) { + body.ids @ def.ids; + } else { + body.ids; + }; let (_, ctx_pat_ana, m_pat) = - upat_to_info_map(~mode=Ana(ty_def), ~body_ids=body.ids @ def.ids, pat); + upat_to_info_map(~mode=Ana(ty_def), ~body_ids=pat_body_ids, pat); let ctx_body = VarMap.concat(ctx, ctx_pat_ana); let (ty_body, free_body, m_body) = uexp_to_info_map(~ctx=ctx_body, ~mode, body); add( ~self=Just(ty_body), - ~free=Ctx.union([free_def, Ctx.subtract_typ(ctx_pat_ana, free_body)]), + ~free= + Ctx.union([ + free_def, + Ctx.subtract_typ( + def_ctx, + Ctx.subtract_typ(ctx_pat_ana, free_body), + ), + ]), union_m([m_pat, m_def, m_body]), ); | Match(scrut, rules) => From f480427576e179d52cd18b14b2e4f87a444fffd6 Mon Sep 17 00:00:00 2001 From: Shubh Agrawal Date: Mon, 6 Feb 2023 00:02:43 -0500 Subject: [PATCH 8/8] add highlighting for uses --- src/haz3lweb/view/Cell.re | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/src/haz3lweb/view/Cell.re b/src/haz3lweb/view/Cell.re index 96f1de4183..7e33091e16 100644 --- a/src/haz3lweb/view/Cell.re +++ b/src/haz3lweb/view/Cell.re @@ -155,6 +155,18 @@ let test_result_layer = ); }; +let get_usage_ids = (zipper, info_map) => { + /* bad style, does reason have let*? */ + switch (Haz3lcore.Indicated.index(zipper)) { + | Some(index) => + switch (Haz3lcore.Id.Map.find_opt(index, info_map)) { + | Some(ci) => Haz3lcore.Statics.binding_uses(ci, info_map) + | None => [] + } + | None => [] + }; +}; + let deco = ( ~zipper, @@ -168,6 +180,16 @@ let deco = ~color_highlighting: option(ColorSteps.colorMap), ) => { let unselected = Zipper.unselect_and_zip(zipper); + let use_ids = get_usage_ids(zipper, info_map); + let use_highlights = + List.flatten( + List.map( + ((_tok, ids): Haz3lcore.Statics.usage_info) => { + List.map(id => (id, "orange"), ids) + }, + use_ids, + ), + ); module Deco = Deco.Deco({ let font_metrics = font_metrics; @@ -179,6 +201,7 @@ let deco = let tiles = TileMap.mk(unselected); }); let decos = selected ? Deco.all(zipper, segment) : Deco.err_holes(zipper); + let decos = decos @ Deco.color_highlights(use_highlights); let decos = switch (test_results) { | None => decos