Skip to content

Break out semantics to library #1619

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.

Sign up for GitHub

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

Open
wants to merge 2 commits into
base: projector-gadts
Choose a base branch
from
Open

Break out semantics to library #1619

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
543d234
break out semantics to library
disconcision Apr 17, 2025
30f562d
rm unused/redundant build libs
disconcision Apr 18, 2025
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
4 changes: 0 additions & 4 deletions src/haz3lcore/CodeString.re
View file
Open in desktop

This file was deleted.

13 changes: 5 additions & 8 deletions src/haz3lcore/zipper/Editor.re → src/haz3lcore/Editor.re
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -130,7 +130,7 @@
(module M);
};

let trailing_hole_ctx = (ed: t, info_map: Statics.Map.t) => {
let trailing_hole_ctx = (ed: t, info_map: Semantics.Statics.Map.t) => {

Check warning on line 133 in src/haz3lcore/Editor.re

View check run for this annotation

Codecov / codecov/patch

src/haz3lcore/Editor.re#L133 

Added line #L133 was not covered by tests
let segment = Zipper.unselect_and_zip(ed.state.zipper);
let convex_grout = Segment.convex_grout(segment);
// print_endline(String.concat("; ", List.map(Grout.show, convex_grout)));
Expand All @@ -139,9 +139,9 @@
| None => None
| Some(grout) =>
let id = grout.id;
let info = Id.Map.find_opt(id, info_map);
let info = Semantics.Statics.Map.lookup(id, info_map);
switch (info) {
| Some(info) => Some(Info.ctx_of(info))
| Some(info) => Some(Semantics.Info.ctx_of(info))

Check warning on line 144 in src/haz3lcore/Editor.re

View check run for this annotation

Codecov / codecov/patch

src/haz3lcore/Editor.re#L144 

Added line #L144 was not covered by tests
| _ => None
};
};
Expand All @@ -153,7 +153,7 @@

let update =
(
~settings: CoreSettings.t,
~settings: Semantics.CoreSettings.t,
a: Action.t,
old_statics,
{state, history, syntax}: Model.t,
Expand Down Expand Up @@ -222,9 +222,6 @@
state.zipper,
);

settings.flip_animations && Action.should_animate(a)
? Animation.request([Animation.Actions.move("caret")]) : ();
Comment on lines -225 to -226
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I know this is happening on perform now, but can I get some context.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

the animation system I created requires (a) capturing DOM state before an action is triggered, (b) storing that state so that it is persisted into the next MVU loop, and (c) capturing DOM state after the action has been formed, after the DOM is regenerated, but before draw occurs. (a) was done here; now i've moved it slightly so that Animation can live in Web. (b) happens in Main.re.

The reason why it was here to begin with (aside from the lazy fact that core has web dep due to projectors), is that in general we want to trigger animations based on the particular action taken, possibly with explicit dependence on both the before and after state of the model. I'm continually torn on whether effects like this should be handled as part of an entirely separate switch; i like the separation of concerns, but also think that it's not terrible to be forced to think about the effect when you change an action. I had started moving in the separation direction, but ended up punting, forgetting about it, and leaving it in an intermediate state. I think now that the effect should probably be abstracted to the Action.should_animate function, which should take the before and after models as well as the action, and produce an effect.


// Recombine
Model.{
state: {
Expand Down Expand Up @@ -266,7 +263,7 @@

let calculate =
(
~settings: CoreSettings.t,
~settings: Semantics.CoreSettings.t,
~is_edited,
new_statics,
dyn_map,
Expand Down
1 change: 1 addition & 0 deletions src/haz3lcore/Id.re
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
include Util.Id;
9 changes: 0 additions & 9 deletions src/haz3lcore/StructureShareSexp.rei
View file
Open in desktop

This file was deleted.

5 changes: 0 additions & 5 deletions src/haz3lcore/TermMap.re
View file
Open in desktop

This file was deleted.

21 changes: 11 additions & 10 deletions src/haz3lcore/assistant/TyDi.re → src/haz3lcore/TyDi/TyDi.re
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,8 +1,9 @@
open Util.OptUtil.Syntax;
open Suggestion;
open TyDiSuggestion;
open Semantics;

/* Suggest the token at the top of the backpack, if we can put it down */
let suggest_backpack = (z: Zipper.t): list(Suggestion.t) => {
let suggest_backpack = (z: Zipper.t): list(t) => {

Check warning on line 6 in src/haz3lcore/TyDi/TyDi.re

View check run for this annotation

Codecov / codecov/patch

src/haz3lcore/TyDi/TyDi.re#L6 

Added line #L6 was not covered by tests
/* Note: Sort check unnecessary here as wouldn't be able to put down */
switch (z.backpack) {
| [] => []
Expand All @@ -19,7 +20,7 @@
};
};

let suggest = (ci: Info.t, z: Zipper.t): list(Suggestion.t) => {
let suggest = (ci: Info.t, z: Zipper.t): list(t) => {

Check warning on line 23 in src/haz3lcore/TyDi/TyDi.re

View check run for this annotation

Codecov / codecov/patch

src/haz3lcore/TyDi/TyDi.re#L23 

Added line #L23 was not covered by tests
/* NOTE: Sorting ensures that if we have an exact match already,
* we won't suggest extending it, but straight-up lexical sorting
* may not be desirable in other ways, for example maybe we want
Expand All @@ -35,13 +36,13 @@
| _ =>
suggest_backpack(z)
@ (
AssistantForms.suggest_operand(ci)
@ AssistantForms.suggest_leading(ci)
@ AssistantCtx.suggest_variable(ci)
@ AssistantCtx.suggest_lookahead_variable(ci)
|> List.sort(Suggestion.compare)
TyDiForms.suggest_operand(ci)
@ TyDiForms.suggest_leading(ci)
@ TyDiCtx.suggest_variable(ci)
@ TyDiCtx.suggest_lookahead_variable(ci)
|> List.sort(TyDiSuggestion.compare)

Check warning on line 43 in src/haz3lcore/TyDi/TyDi.re

View check run for this annotation

Codecov / codecov/patch

src/haz3lcore/TyDi/TyDi.re#L39-L43 

Added lines #L39 - L43 were not covered by tests
)
@ (AssistantForms.suggest_operator(ci) |> List.sort(Suggestion.compare))
@ (TyDiForms.suggest_operator(ci) |> List.sort(TyDiSuggestion.compare))

Check warning on line 45 in src/haz3lcore/TyDi/TyDi.re

View check run for this annotation

Codecov / codecov/patch

src/haz3lcore/TyDi/TyDi.re#L45 

Added line #L45 was not covered by tests
};
};

Expand Down Expand Up @@ -106,7 +107,7 @@
let suggestions = suggest(ci, z);
let suggestions =
suggestions
|> List.filter(({content, _}: Suggestion.t) =>
|> List.filter(({content, _}: TyDiSuggestion.t) =>
String.starts_with(~prefix=tok_to_left, content)
);
let* top_suggestion = suggestions |> Util.ListUtil.hd_opt;
Expand Down
20 changes: 11 additions & 9 deletions src/haz3lcore/assistant/AssistantCtx.re → src/haz3lcore/TyDi/TyDiCtx.re
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,9 +1,10 @@
open Suggestion;
open TyDiSuggestion;
open Semantics;

/* For suggestions in patterns, suggest variables which
* occur free in that pattern's scope. */
let free_variables =
(expected_ty: Typ.t, ctx: Ctx.t, co_ctx: CoCtx.t): list(Suggestion.t) => {
(expected_ty: Typ.t, ctx: Ctx.t, co_ctx: CoCtx.t): list(TyDiSuggestion.t) => {

Check warning on line 7 in src/haz3lcore/TyDi/TyDiCtx.re

View check run for this annotation

Codecov / codecov/patch

src/haz3lcore/TyDi/TyDiCtx.re#L7 

Added line #L7 was not covered by tests
List.filter_map(
((name, entries)) =>
switch (Ctx.lookup_var(ctx, name)) {
Expand All @@ -24,7 +25,7 @@
};

/* For suggestsions in expressions, suggest variables from the ctx */
let bound_variables = (ty_expect: Typ.t, ctx: Ctx.t): list(Suggestion.t) =>
let bound_variables = (ty_expect: Typ.t, ctx: Ctx.t): list(TyDiSuggestion.t) =>
List.filter_map(
fun
| Ctx.VarEntry({typ, name, _})
Expand All @@ -39,7 +40,7 @@

let bound_constructors =
(wrap: strategy_common => strategy, ty: Typ.t, ctx: Ctx.t)
: list(Suggestion.t) =>
: list(TyDiSuggestion.t) =>
/* get names of all constructor entries consistent with ty */
List.filter_map(
fun
Expand All @@ -54,7 +55,7 @@
);

/* Suggest applying a function from the ctx which returns an appropriate type */
let bound_aps = (ty_expect: Typ.t, ctx: Ctx.t): list(Suggestion.t) =>
let bound_aps = (ty_expect: Typ.t, ctx: Ctx.t): list(TyDiSuggestion.t) =>
List.filter_map(
fun
| Ctx.VarEntry({typ: {term: Arrow(_, ty_out), _} as ty_arr, name, _})
Expand All @@ -70,7 +71,8 @@
ctx.entries,
);

let bound_constructor_aps = (wrap, ty: Typ.t, ctx: Ctx.t): list(Suggestion.t) =>
let bound_constructor_aps =
(wrap, ty: Typ.t, ctx: Ctx.t): list(TyDiSuggestion.t) =>
List.filter_map(
fun
| Ctx.ConstructorEntry({
Expand All @@ -90,7 +92,7 @@
);

/* Suggest bound type aliases in type annotations or definitions */
let typ_context_entries = (ctx: Ctx.t): list(Suggestion.t) =>
let typ_context_entries = (ctx: Ctx.t): list(TyDiSuggestion.t) =>
List.filter_map(
fun
| Ctx.TVarEntry({kind: Singleton(_), name, _}) =>
Expand All @@ -102,7 +104,7 @@
ctx.entries,
);

let suggest_variable = (ci: Info.t): list(Suggestion.t) => {
let suggest_variable = (ci: Info.t): list(TyDiSuggestion.t) => {

Check warning on line 107 in src/haz3lcore/TyDi/TyDiCtx.re

View check run for this annotation

Codecov / codecov/patch

src/haz3lcore/TyDi/TyDiCtx.re#L107 

Added line #L107 was not covered by tests
let ctx = Info.ctx_of(ci);
switch (ci) {
| InfoExp({ana, _}) =>
Expand Down Expand Up @@ -141,7 +143,7 @@
*
*/

let suggest_lookahead_variable = (ci: Info.t): list(Suggestion.t) => {
let suggest_lookahead_variable = (ci: Info.t): list(TyDiSuggestion.t) => {

Check warning on line 146 in src/haz3lcore/TyDi/TyDiCtx.re

View check run for this annotation

Codecov / codecov/patch

src/haz3lcore/TyDi/TyDiCtx.re#L146 

Added line #L146 was not covered by tests
let restrategize = (suffix, {content, strategy}) => {
content: content ++ suffix,
strategy,
Expand Down
16 changes: 9 additions & 7 deletions src/haz3lcore/assistant/AssistantForms.re → src/haz3lcore/TyDi/TyDiForms.re
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
open Util;
open OptUtil.Syntax;
open Semantics;

/* This module generates TyDi suggestions which depend
* neither on the typing context or the backpack */
Expand Down Expand Up @@ -172,7 +173,8 @@
};
};

let suggest_form = (ty_map, delims_of_sort, ci: Info.t): list(Suggestion.t) => {
let suggest_form =
(ty_map, delims_of_sort, ci: Info.t): list(TyDiSuggestion.t) => {

Check warning on line 177 in src/haz3lcore/TyDi/TyDiForms.re

View check run for this annotation

Codecov / codecov/patch

src/haz3lcore/TyDi/TyDiForms.re#L177 

Added line #L177 was not covered by tests
let sort = Info.sort_of(ci);
let delims = delims_of_sort(sort);
let filtered =
Expand All @@ -181,7 +183,7 @@
| Exp =>
List.map(
((content, ty)) =>
Suggestion.{
TyDiSuggestion.{

Check warning on line 186 in src/haz3lcore/TyDi/TyDiForms.re

View check run for this annotation

Codecov / codecov/patch

src/haz3lcore/TyDi/TyDiForms.re#L186 

Added line #L186 was not covered by tests
content,
strategy: Exp(Common(NewForm(ty))),
},
Expand All @@ -190,7 +192,7 @@
| Pat =>
List.map(
((content, ty)) =>
Suggestion.{
TyDiSuggestion.{

Check warning on line 195 in src/haz3lcore/TyDi/TyDiForms.re

View check run for this annotation

Codecov / codecov/patch

src/haz3lcore/TyDi/TyDiForms.re#L195 

Added line #L195 was not covered by tests
content,
strategy: Pat(Common(NewForm(ty))),
},
Expand All @@ -199,15 +201,15 @@
| _ =>
delims
|> List.map(content =>
Suggestion.{
TyDiSuggestion.{

Check warning on line 204 in src/haz3lcore/TyDi/TyDiForms.re

View check run for this annotation

Codecov / codecov/patch

src/haz3lcore/TyDi/TyDiForms.re#L204 

Added line #L204 was not covered by tests
content,
strategy: Typ(NewForm),
}
)
};
};

let suggest_operator: Info.t => list(Suggestion.t) =
let suggest_operator: Info.t => list(TyDiSuggestion.t) =
info => {
switch (info) {
| InfoExp({
Expand All @@ -225,8 +227,8 @@
};
};

let suggest_operand: Info.t => list(Suggestion.t) =
let suggest_operand: Info.t => list(TyDiSuggestion.t) =
suggest_form(Typ.of_const_mono_delim, Delims.const_mono);

let suggest_leading: Info.t => list(Suggestion.t) =
let suggest_leading: Info.t => list(TyDiSuggestion.t) =
suggest_form(Typ.of_leading_delim, Delims.delayed_leading);
8 changes: 4 additions & 4 deletions src/haz3lcore/assistant/Suggestion.re → src/haz3lcore/TyDi/TyDiSuggestion.re
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,9 +37,9 @@

[@deriving (show({with_path: false}), sexp, yojson)]
type strategy_common =
| NewForm(Typ.t)
| FromCtx(Typ.t)
| FromCtxAp(Typ.t);
| NewForm(Semantics.Typ.t)
| FromCtx(Semantics.Typ.t)
| FromCtxAp(Semantics.Typ.t);

Check warning on line 42 in src/haz3lcore/TyDi/TyDiSuggestion.re

View check run for this annotation

Codecov / codecov/patch

src/haz3lcore/TyDi/TyDiSuggestion.re#L40-L42 

Added lines #L40 - L42 were not covered by tests

[@deriving (show({with_path: false}), sexp, yojson)]
type strategy_exp =
Expand All @@ -48,7 +48,7 @@
[@deriving (show({with_path: false}), sexp, yojson)]
type strategy_pat =
| Common(strategy_common)
| FromCoCtx(Typ.t);
| FromCoCtx(Semantics.Typ.t);

Check warning on line 51 in src/haz3lcore/TyDi/TyDiSuggestion.re

View check run for this annotation

Codecov / codecov/patch

src/haz3lcore/TyDi/TyDiSuggestion.re#L51 

Added line #L51 was not covered by tests

[@deriving (show({with_path: false}), sexp, yojson)]
type strategy_typ =
Expand Down
16 changes: 0 additions & 16 deletions src/haz3lcore/assistant/AssistantExpander.re
View file
Open in desktop

This file was deleted.

1 change: 1 addition & 0 deletions src/haz3lcore/prog/CachedStatics.re → src/haz3lcore/derived/CachedStatics.re
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
open Util;
open Semantics;

[@deriving (show({with_path: false}), sexp, yojson)]
type t = {
Expand Down
0 src/haz3lcore/Measured.re → src/haz3lcore/derived/Measured.re
View file
Open in desktop
File renamed without changes.
5 changes: 5 additions & 0 deletions src/haz3lcore/derived/TermMap.re
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
include Id.Map;
type t = Id.Map.t(Semantics.Any.t);

let add_all = (ids: list(Id.t), tm: Semantics.Any.t, map: t) =>
ids |> List.fold_left((map, id) => add(id, tm, map), map);
0 src/haz3lcore/TermRanges.re → src/haz3lcore/derived/TermRanges.re
View file
Open in desktop
File renamed without changes.
0 src/haz3lcore/TileMap.re → src/haz3lcore/derived/TileMap.re
View file
Open in desktop
File renamed without changes.
2 changes: 1 addition & 1 deletion src/haz3lcore/dune
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@

(library
(name haz3lcore)
(libraries util sexplib unionFind uuidm virtual_dom yojson core)
(libraries semantics)
(js_of_ocaml)
(instrumentation
(backend bisect_ppx))
Expand Down
6 changes: 0 additions & 6 deletions src/haz3lcore/lang/Labels.re
View file
Open in desktop

This file was deleted.

12 changes: 6 additions & 6 deletions src/haz3lcore/statics/MakeTerm.re → src/haz3lcore/lang/MakeTerm.re
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@
*/

open Util;
open Any;
open Semantics;

/* Hack: Temporary construct internal to maketerm
* to handle probe parsing; see `tokens` below */
Expand All @@ -33,17 +33,17 @@
);

[@deriving (show({with_path: false}), sexp, yojson)]
type tile = (Id.t, Aba.t(Token.t, t));
type tile = (Id.t, Aba.t(Token.t, Any.t));

Check warning on line 36 in src/haz3lcore/lang/MakeTerm.re

View check run for this annotation

Codecov / codecov/patch

src/haz3lcore/lang/MakeTerm.re#L36 

Added line #L36 was not covered by tests
[@deriving (show({with_path: false}), sexp, yojson)]
type tiles = Aba.t(tile, t);
type tiles = Aba.t(tile, Any.t);

Check warning on line 38 in src/haz3lcore/lang/MakeTerm.re

View check run for this annotation

Codecov / codecov/patch

src/haz3lcore/lang/MakeTerm.re#L38 

Added line #L38 was not covered by tests
let single = (id, subst) => ([(id, subst)], []);

[@deriving (show({with_path: false}), sexp, yojson)]
type unsorted =
| Op(tiles)
| Pre(tiles, t)
| Post(t, tiles)
| Bin(t, tiles, t);
| Pre(tiles, Any.t)
| Post(Any.t, tiles)
| Bin(Any.t, tiles, Any.t);

Check warning on line 46 in src/haz3lcore/lang/MakeTerm.re

View check run for this annotation

Codecov / codecov/patch

src/haz3lcore/lang/MakeTerm.re#L44-L46 

Added lines #L44 - L46 were not covered by tests

type t = {
term: Exp.t,
Expand Down
2 changes: 1 addition & 1 deletion src/haz3lcore/lang/Precedence.re
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -108,7 +108,7 @@ let associativity_map: IntMap.t(Direction.t) =
let associativity = (p: t): option(Direction.t) =>
IntMap.find_opt(p, associativity_map);

let of_bin_op: Operators.op_bin => t =
let of_bin_op: Semantics.Operators.op_bin => t =
fun
| Nat(op)
| SInt(op)
Expand Down
Loading