From 543d234862024c14dc50e1ae2e924818b4c83a1a Mon Sep 17 00:00:00 2001 From: disconcision Date: Thu, 17 Apr 2025 19:37:03 -0400 Subject: [PATCH 1/2] break out semantics to library --- src/haz3lcore/CodeString.re | 4 - src/haz3lcore/{zipper => }/Editor.re | 13 +- src/haz3lcore/Id.re | 1 + src/haz3lcore/StructureShareSexp.rei | 9 -- src/haz3lcore/TermMap.re | 5 - src/haz3lcore/{assistant => TyDi}/TyDi.re | 21 ++-- .../AssistantCtx.re => TyDi/TyDiCtx.re} | 20 +-- .../AssistantForms.re => TyDi/TyDiForms.re} | 16 +-- .../Suggestion.re => TyDi/TyDiSuggestion.re} | 8 +- src/haz3lcore/assistant/AssistantExpander.re | 16 --- .../{prog => derived}/CachedStatics.re | 1 + src/haz3lcore/{ => derived}/Measured.re | 0 src/haz3lcore/derived/TermMap.re | 5 + src/haz3lcore/{ => derived}/TermRanges.re | 0 src/haz3lcore/{ => derived}/TileMap.re | 0 src/haz3lcore/dune | 2 +- src/haz3lcore/lang/Labels.re | 6 - src/haz3lcore/{statics => lang}/MakeTerm.re | 12 +- src/haz3lcore/lang/Precedence.re | 2 +- src/haz3lcore/lang/Sort.re | 36 +----- src/haz3lcore/pretty/ExpToSegment.re | 4 + src/haz3lcore/projectors/ProjectorBase.re | 9 +- src/haz3lcore/projectors/ProjectorInfo.re | 2 + src/haz3lcore/projectors/ProjectorInit.re | 4 +- .../projectors/implementations/CardProj.re | 1 + .../implementations/CheckboxProj.re | 4 +- .../projectors/implementations/ProbeProj.re | 1 + .../projectors/implementations/SliderFProj.re | 4 +- .../projectors/implementations/SliderProj.re | 4 +- .../implementations/TextAreaProj.re | 4 +- .../projectors/implementations/TypeProj.re | 4 +- src/haz3lcore/tiles/Secondary.re | 4 +- src/haz3lcore/tiles/Skel.re | 5 +- src/haz3lcore/zipper/EditorUtil.re | 102 --------------- src/haz3lcore/zipper/action/Indicated.re | 9 +- src/haz3lcore/zipper/action/Introduce.re | 2 + src/haz3lcore/zipper/action/Perform.re | 6 +- src/haz3lcore/zipper/action/Select.re | 22 ++-- src/haz3lmenhir/AST.re | 7 +- src/haz3lmenhir/Conversion.re | 24 ++-- src/haz3lmenhir/dune | 2 +- src/{haz3lcore => haz3lweb}/Animation.re | 0 src/{haz3lcore => haz3lweb}/ClipboardCache.re | 2 + src/haz3lweb/Main.re | 2 +- src/haz3lweb/Settings.re | 4 +- src/haz3lweb/app/Cursor.re | 2 +- src/haz3lweb/app/common/ProjectorView.re | 9 +- src/haz3lweb/app/editors/SettingsModal.re | 5 +- src/haz3lweb/app/editors/cell/CellEditor.re | 2 +- src/haz3lweb/app/editors/code/CodeEditable.re | 5 +- src/haz3lweb/app/editors/code/CodeViewable.re | 4 +- .../app/editors/code/CodeWithStatics.re | 13 +- src/haz3lweb/app/editors/decoration/Deco.re | 8 +- src/haz3lweb/app/editors/result/EvalResult.re | 69 ++++------ .../app/editors/result/StepperEditor.re | 2 +- src/haz3lweb/app/explainthis/ExplainThis.re | 1 + .../app/explainthis/ExplainThisForm.re | 8 +- src/haz3lweb/app/explainthis/data/DotExp.re | 1 + src/haz3lweb/app/globals/Globals.re | 2 +- src/haz3lweb/app/inspector/CursorInspector.re | 8 +- src/haz3lweb/app/inspector/ProjectorPanel.re | 2 +- src/haz3lweb/debug/DebugConsole.re | 12 +- src/haz3lweb/exercises/Exercise.re | 118 +++++++++++++++--- src/haz3lweb/exercises/Grading.re | 14 +-- src/haz3lweb/exercises/SyntaxTest.re | 2 +- src/haz3lweb/util/Unicode.re | 35 ------ src/haz3lweb/util/WorkerServer.re | 16 +-- src/haz3lweb/view/ContextInspector.re | 20 +-- src/haz3lweb/view/ExerciseMode.re | 6 +- src/haz3lweb/view/Kind.re | 2 +- src/haz3lweb/view/NutMenu.re | 8 +- src/haz3lweb/view/Page.re | 6 +- src/haz3lweb/view/ScratchMode.re | 4 +- src/haz3lweb/view/StepperView.re | 5 +- src/haz3lweb/view/TestView.re | 6 +- src/{haz3lcore/lang => semantics}/Builtins.re | 0 .../prog => semantics}/CoreSettings.re | 0 src/semantics/Id.re | 1 + src/semantics/dune | 25 ++++ .../dynamics/DHExp.re | 0 .../dynamics/DHPat.re | 0 .../prog => semantics/dynamics}/Dynamics.re | 0 .../dynamics/Evaluator.re | 0 .../dynamics/Evaluator.rei | 0 .../dynamics}/ProgramResult.re | 0 .../dynamics/Substitution.re | 0 .../dynamics/TypeAssignment.re | 0 .../dynamics/ValueChecker.re | 0 .../dynamics/state/EvaluatorState.re | 0 .../dynamics/state/EvaluatorState.rei | 0 .../dynamics/state/TestMap.re | 0 .../dynamics/state/TestResults.re | 0 .../dynamics/state/TestStatus.re | 0 .../dynamics/stepper/EvalCtx.re | 0 .../dynamics/stepper/EvaluatorStep.re | 0 .../dynamics/stepper/EvaluatorStep.rei | 0 .../dynamics/stepper/FilterMatcher.re | 0 .../dynamics/transition/Casts.re | 0 .../dynamics/transition/EvaluatorError.re | 0 .../dynamics/transition/PatternMatch.re | 0 .../dynamics/transition/Transition.re | 0 .../dynamics/transition/Unboxing.re | 0 .../statics/Binding.re | 0 src/{haz3lcore => semantics}/statics/CoCtx.re | 0 .../statics/Constructor.re | 0 .../statics/ConstructorMap.re | 0 .../statics/Coverage.re | 0 src/{haz3lcore => semantics}/statics/Ctx.re | 11 +- .../statics/Elaborator.re | 0 src/{haz3lcore => semantics}/statics/Info.re | 6 +- src/{haz3lcore => semantics}/statics/Self.re | 2 +- .../statics/Statics.re | 2 +- .../pretty => semantics/term}/Abbreviate.re | 0 src/{haz3lcore/lang => semantics}/term/Any.re | 0 .../lang => semantics/term}/Atom.re | 0 .../term/ClosureEnvironment.re | 0 src/{haz3lcore/lang => semantics}/term/Cls.re | 0 .../lang => semantics}/term/Environment.re | 0 src/{haz3lcore/lang => semantics}/term/Exp.re | 0 .../lang => semantics}/term/FilterAction.re | 0 .../term/FilterEnvironment.re | 0 .../lang => semantics}/term/Grammar.re | 0 .../lang => semantics}/term/IdTagged.re | 0 .../term/InvalidOperationError.re | 0 .../term}/LabeledTuple.re | 0 .../lang => semantics/term}/Operators.re | 0 src/{haz3lcore/lang => semantics}/term/Pat.re | 0 .../lang => semantics}/term/Probe.re | 0 src/{haz3lcore/lang => semantics}/term/Rul.re | 0 src/semantics/term/Secondary.re | 5 + src/semantics/term/Sort.re | 35 ++++++ .../lang => semantics}/term/TPat.re | 0 .../lang => semantics}/term/Term.re | 0 .../lang => semantics}/term/TermBase.re | 6 +- src/{haz3lcore/lang => semantics}/term/Typ.re | 0 src/{haz3lcore/lang => semantics}/term/Var.re | 0 .../lang => semantics}/term/VarBstMap.re | 0 .../lang => semantics}/term/VarBstMap.rei | 0 src/{haz3lcore/tiles => util}/Id.re | 10 +- src/{haz3lcore => util}/StructureShareSexp.re | 0 src/{haz3lcore => util}/Unicode.re | 0 src/util/Util.re | 4 + src/{haz3lcore => util}/VarMap.re | 5 +- src/util/dune | 13 +- test/Test_Coverage.re | 2 +- test/Test_Elaboration.re | 4 +- test/Test_Evaluator.re | 4 +- test/Test_ExpToSegment.re | 1 + test/Test_Grammar.re | 2 +- test/Test_Introduce.re | 6 +- test/Test_LabeledTuple.re | 2 +- test/Test_MakeTerm.re | 8 +- test/Test_Menhir.re | 32 ++--- test/Test_Statics.re | 4 +- test/Test_Typ.re | 2 +- test/Test_Unboxing.re | 2 +- 156 files changed, 502 insertions(+), 496 deletions(-) delete mode 100644 src/haz3lcore/CodeString.re rename src/haz3lcore/{zipper => }/Editor.re (95%) create mode 100644 src/haz3lcore/Id.re delete mode 100644 src/haz3lcore/StructureShareSexp.rei delete mode 100644 src/haz3lcore/TermMap.re rename src/haz3lcore/{assistant => TyDi}/TyDi.re (87%) rename src/haz3lcore/{assistant/AssistantCtx.re => TyDi/TyDiCtx.re} (90%) rename src/haz3lcore/{assistant/AssistantForms.re => TyDi/TyDiForms.re} (94%) rename src/haz3lcore/{assistant/Suggestion.re => TyDi/TyDiSuggestion.re} (94%) delete mode 100644 src/haz3lcore/assistant/AssistantExpander.re rename src/haz3lcore/{prog => derived}/CachedStatics.re (99%) rename src/haz3lcore/{ => derived}/Measured.re (100%) create mode 100644 src/haz3lcore/derived/TermMap.re rename src/haz3lcore/{ => derived}/TermRanges.re (100%) rename src/haz3lcore/{ => derived}/TileMap.re (100%) delete mode 100644 src/haz3lcore/lang/Labels.re rename src/haz3lcore/{statics => lang}/MakeTerm.re (99%) delete mode 100644 src/haz3lcore/zipper/EditorUtil.re rename src/{haz3lcore => haz3lweb}/Animation.re (100%) rename src/{haz3lcore => haz3lweb}/ClipboardCache.re (98%) delete mode 100644 src/haz3lweb/util/Unicode.re rename src/{haz3lcore/lang => semantics}/Builtins.re (100%) rename src/{haz3lcore/prog => semantics}/CoreSettings.re (100%) create mode 100644 src/semantics/Id.re create mode 100644 src/semantics/dune rename src/{haz3lcore => semantics}/dynamics/DHExp.re (100%) rename src/{haz3lcore => semantics}/dynamics/DHPat.re (100%) rename src/{haz3lcore/prog => semantics/dynamics}/Dynamics.re (100%) rename src/{haz3lcore => semantics}/dynamics/Evaluator.re (100%) rename src/{haz3lcore => semantics}/dynamics/Evaluator.rei (100%) rename src/{haz3lcore/prog => semantics/dynamics}/ProgramResult.re (100%) rename src/{haz3lcore => semantics}/dynamics/Substitution.re (100%) rename src/{haz3lcore => semantics}/dynamics/TypeAssignment.re (100%) rename src/{haz3lcore => semantics}/dynamics/ValueChecker.re (100%) rename src/{haz3lcore => semantics}/dynamics/state/EvaluatorState.re (100%) rename src/{haz3lcore => semantics}/dynamics/state/EvaluatorState.rei (100%) rename src/{haz3lcore => semantics}/dynamics/state/TestMap.re (100%) rename src/{haz3lcore => semantics}/dynamics/state/TestResults.re (100%) rename src/{haz3lcore => semantics}/dynamics/state/TestStatus.re (100%) rename src/{haz3lcore => semantics}/dynamics/stepper/EvalCtx.re (100%) rename src/{haz3lcore => semantics}/dynamics/stepper/EvaluatorStep.re (100%) rename src/{haz3lcore => semantics}/dynamics/stepper/EvaluatorStep.rei (100%) rename src/{haz3lcore => semantics}/dynamics/stepper/FilterMatcher.re (100%) rename src/{haz3lcore => semantics}/dynamics/transition/Casts.re (100%) rename src/{haz3lcore => semantics}/dynamics/transition/EvaluatorError.re (100%) rename src/{haz3lcore => semantics}/dynamics/transition/PatternMatch.re (100%) rename src/{haz3lcore => semantics}/dynamics/transition/Transition.re (100%) rename src/{haz3lcore => semantics}/dynamics/transition/Unboxing.re (100%) rename src/{haz3lcore => semantics}/statics/Binding.re (100%) rename src/{haz3lcore => semantics}/statics/CoCtx.re (100%) rename src/{haz3lcore => semantics}/statics/Constructor.re (100%) rename src/{haz3lcore => semantics}/statics/ConstructorMap.re (100%) rename src/{haz3lcore => semantics}/statics/Coverage.re (100%) rename src/{haz3lcore => semantics}/statics/Ctx.re (96%) rename src/{haz3lcore => semantics}/statics/Elaborator.re (100%) rename src/{haz3lcore => semantics}/statics/Info.re (99%) rename src/{haz3lcore => semantics}/statics/Self.re (98%) rename src/{haz3lcore => semantics}/statics/Statics.re (99%) rename src/{haz3lcore/pretty => semantics/term}/Abbreviate.re (100%) rename src/{haz3lcore/lang => semantics}/term/Any.re (100%) rename src/{haz3lcore/lang => semantics/term}/Atom.re (100%) rename src/{haz3lcore/lang => semantics}/term/ClosureEnvironment.re (100%) rename src/{haz3lcore/lang => semantics}/term/Cls.re (100%) rename src/{haz3lcore/lang => semantics}/term/Environment.re (100%) rename src/{haz3lcore/lang => semantics}/term/Exp.re (100%) rename src/{haz3lcore/lang => semantics}/term/FilterAction.re (100%) rename src/{haz3lcore/lang => semantics}/term/FilterEnvironment.re (100%) rename src/{haz3lcore/lang => semantics}/term/Grammar.re (100%) rename src/{haz3lcore/lang => semantics}/term/IdTagged.re (100%) rename src/{haz3lcore/lang => semantics}/term/InvalidOperationError.re (100%) rename src/{haz3lcore => semantics/term}/LabeledTuple.re (100%) rename src/{haz3lcore/lang => semantics/term}/Operators.re (100%) rename src/{haz3lcore/lang => semantics}/term/Pat.re (100%) rename src/{haz3lcore/lang => semantics}/term/Probe.re (100%) rename src/{haz3lcore/lang => semantics}/term/Rul.re (100%) create mode 100644 src/semantics/term/Secondary.re create mode 100644 src/semantics/term/Sort.re rename src/{haz3lcore/lang => semantics}/term/TPat.re (100%) rename src/{haz3lcore/lang => semantics}/term/Term.re (100%) rename src/{haz3lcore/lang => semantics}/term/TermBase.re (99%) rename src/{haz3lcore/lang => semantics}/term/Typ.re (100%) rename src/{haz3lcore/lang => semantics}/term/Var.re (100%) rename src/{haz3lcore/lang => semantics}/term/VarBstMap.re (100%) rename src/{haz3lcore/lang => semantics}/term/VarBstMap.rei (100%) rename src/{haz3lcore/tiles => util}/Id.re (95%) rename src/{haz3lcore => util}/StructureShareSexp.re (100%) rename src/{haz3lcore => util}/Unicode.re (100%) rename src/{haz3lcore => util}/VarMap.re (89%) diff --git a/src/haz3lcore/CodeString.re b/src/haz3lcore/CodeString.re deleted file mode 100644 index a6ddd14875..0000000000 --- a/src/haz3lcore/CodeString.re +++ /dev/null @@ -1,4 +0,0 @@ -open Util; - -[@deriving (show({with_path: false}), sexp, yojson)] -type t = string; diff --git a/src/haz3lcore/zipper/Editor.re b/src/haz3lcore/Editor.re similarity index 95% rename from src/haz3lcore/zipper/Editor.re rename to src/haz3lcore/Editor.re index f69dabdb1b..4a0af60fb7 100644 --- a/src/haz3lcore/zipper/Editor.re +++ b/src/haz3lcore/Editor.re @@ -130,7 +130,7 @@ module Model = { (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) => { 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))); @@ -139,9 +139,9 @@ module Model = { | 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)) | _ => None }; }; @@ -153,7 +153,7 @@ module Update = { let update = ( - ~settings: CoreSettings.t, + ~settings: Semantics.CoreSettings.t, a: Action.t, old_statics, {state, history, syntax}: Model.t, @@ -222,9 +222,6 @@ module Update = { state.zipper, ); - settings.flip_animations && Action.should_animate(a) - ? Animation.request([Animation.Actions.move("caret")]) : (); - // Recombine Model.{ state: { @@ -266,7 +263,7 @@ module Update = { let calculate = ( - ~settings: CoreSettings.t, + ~settings: Semantics.CoreSettings.t, ~is_edited, new_statics, dyn_map, diff --git a/src/haz3lcore/Id.re b/src/haz3lcore/Id.re new file mode 100644 index 0000000000..cdcf515e83 --- /dev/null +++ b/src/haz3lcore/Id.re @@ -0,0 +1 @@ +include Util.Id; diff --git a/src/haz3lcore/StructureShareSexp.rei b/src/haz3lcore/StructureShareSexp.rei deleted file mode 100644 index 5f5857ba15..0000000000 --- a/src/haz3lcore/StructureShareSexp.rei +++ /dev/null @@ -1,9 +0,0 @@ -// To be used on the data structure where the structure sharing takes place -let structure_share_here: - ('a => Id.t, 'a => Sexplib.Sexp.t, Sexplib.Sexp.t => 'a) => - ('a => Sexplib.Sexp.t, Sexplib.Sexp.t => 'a); - -// To be used only on the root of the data structure currently being serialized -let structure_share_in: - ('a => Sexplib.Sexp.t, Sexplib.Sexp.t => 'a) => - ('a => Sexplib.Sexp.t, Sexplib.Sexp.t => 'a); diff --git a/src/haz3lcore/TermMap.re b/src/haz3lcore/TermMap.re deleted file mode 100644 index df0f6341de..0000000000 --- a/src/haz3lcore/TermMap.re +++ /dev/null @@ -1,5 +0,0 @@ -include Id.Map; -type t = Id.Map.t(Any.t); - -let add_all = (ids: list(Id.t), tm: Any.t, map: t) => - ids |> List.fold_left((map, id) => add(id, tm, map), map); diff --git a/src/haz3lcore/assistant/TyDi.re b/src/haz3lcore/TyDi/TyDi.re similarity index 87% rename from src/haz3lcore/assistant/TyDi.re rename to src/haz3lcore/TyDi/TyDi.re index 1f6284db97..aa73b07f10 100644 --- a/src/haz3lcore/assistant/TyDi.re +++ b/src/haz3lcore/TyDi/TyDi.re @@ -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) => { /* Note: Sort check unnecessary here as wouldn't be able to put down */ switch (z.backpack) { | [] => [] @@ -19,7 +20,7 @@ let suggest_backpack = (z: Zipper.t): list(Suggestion.t) => { }; }; -let suggest = (ci: Info.t, z: Zipper.t): list(Suggestion.t) => { +let suggest = (ci: Info.t, z: Zipper.t): list(t) => { /* 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 @@ -35,13 +36,13 @@ let suggest = (ci: Info.t, z: Zipper.t): list(Suggestion.t) => { | _ => 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) ) - @ (AssistantForms.suggest_operator(ci) |> List.sort(Suggestion.compare)) + @ (TyDiForms.suggest_operator(ci) |> List.sort(TyDiSuggestion.compare)) }; }; @@ -106,7 +107,7 @@ let set_buffer = (~info_map: Statics.Map.t, z: Zipper.t): option(Zipper.t) => { 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; diff --git a/src/haz3lcore/assistant/AssistantCtx.re b/src/haz3lcore/TyDi/TyDiCtx.re similarity index 90% rename from src/haz3lcore/assistant/AssistantCtx.re rename to src/haz3lcore/TyDi/TyDiCtx.re index a3844911f0..9d502066fe 100644 --- a/src/haz3lcore/assistant/AssistantCtx.re +++ b/src/haz3lcore/TyDi/TyDiCtx.re @@ -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) => { List.filter_map( ((name, entries)) => switch (Ctx.lookup_var(ctx, name)) { @@ -24,7 +25,7 @@ let free_variables = }; /* 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, _}) @@ -39,7 +40,7 @@ let bound_variables = (ty_expect: Typ.t, ctx: Ctx.t): list(Suggestion.t) => 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 @@ -54,7 +55,7 @@ let bound_constructors = ); /* 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, _}) @@ -70,7 +71,8 @@ let bound_aps = (ty_expect: Typ.t, ctx: Ctx.t): list(Suggestion.t) => 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({ @@ -90,7 +92,7 @@ let bound_constructor_aps = (wrap, ty: Typ.t, ctx: Ctx.t): list(Suggestion.t) => ); /* 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, _}) => @@ -102,7 +104,7 @@ let typ_context_entries = (ctx: Ctx.t): list(Suggestion.t) => ctx.entries, ); -let suggest_variable = (ci: Info.t): list(Suggestion.t) => { +let suggest_variable = (ci: Info.t): list(TyDiSuggestion.t) => { let ctx = Info.ctx_of(ci); switch (ci) { | InfoExp({ana, _}) => @@ -141,7 +143,7 @@ let suggest_variable = (ci: Info.t): list(Suggestion.t) => { * */ -let suggest_lookahead_variable = (ci: Info.t): list(Suggestion.t) => { +let suggest_lookahead_variable = (ci: Info.t): list(TyDiSuggestion.t) => { let restrategize = (suffix, {content, strategy}) => { content: content ++ suffix, strategy, diff --git a/src/haz3lcore/assistant/AssistantForms.re b/src/haz3lcore/TyDi/TyDiForms.re similarity index 94% rename from src/haz3lcore/assistant/AssistantForms.re rename to src/haz3lcore/TyDi/TyDiForms.re index 03f6529495..ce27d7e10b 100644 --- a/src/haz3lcore/assistant/AssistantForms.re +++ b/src/haz3lcore/TyDi/TyDiForms.re @@ -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 */ @@ -172,7 +173,8 @@ module Delims = { }; }; -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) => { let sort = Info.sort_of(ci); let delims = delims_of_sort(sort); let filtered = @@ -181,7 +183,7 @@ let suggest_form = (ty_map, delims_of_sort, ci: Info.t): list(Suggestion.t) => { | Exp => List.map( ((content, ty)) => - Suggestion.{ + TyDiSuggestion.{ content, strategy: Exp(Common(NewForm(ty))), }, @@ -190,7 +192,7 @@ let suggest_form = (ty_map, delims_of_sort, ci: Info.t): list(Suggestion.t) => { | Pat => List.map( ((content, ty)) => - Suggestion.{ + TyDiSuggestion.{ content, strategy: Pat(Common(NewForm(ty))), }, @@ -199,7 +201,7 @@ let suggest_form = (ty_map, delims_of_sort, ci: Info.t): list(Suggestion.t) => { | _ => delims |> List.map(content => - Suggestion.{ + TyDiSuggestion.{ content, strategy: Typ(NewForm), } @@ -207,7 +209,7 @@ let suggest_form = (ty_map, delims_of_sort, ci: Info.t): list(Suggestion.t) => { }; }; -let suggest_operator: Info.t => list(Suggestion.t) = +let suggest_operator: Info.t => list(TyDiSuggestion.t) = info => { switch (info) { | InfoExp({ @@ -225,8 +227,8 @@ let suggest_operator: Info.t => list(Suggestion.t) = }; }; -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); diff --git a/src/haz3lcore/assistant/Suggestion.re b/src/haz3lcore/TyDi/TyDiSuggestion.re similarity index 94% rename from src/haz3lcore/assistant/Suggestion.re rename to src/haz3lcore/TyDi/TyDiSuggestion.re index 2f416a80f4..842d380bbd 100644 --- a/src/haz3lcore/assistant/Suggestion.re +++ b/src/haz3lcore/TyDi/TyDiSuggestion.re @@ -37,9 +37,9 @@ type strategy_all = [@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); [@deriving (show({with_path: false}), sexp, yojson)] type strategy_exp = @@ -48,7 +48,7 @@ type strategy_exp = [@deriving (show({with_path: false}), sexp, yojson)] type strategy_pat = | Common(strategy_common) - | FromCoCtx(Typ.t); + | FromCoCtx(Semantics.Typ.t); [@deriving (show({with_path: false}), sexp, yojson)] type strategy_typ = diff --git a/src/haz3lcore/assistant/AssistantExpander.re b/src/haz3lcore/assistant/AssistantExpander.re deleted file mode 100644 index f24be63756..0000000000 --- a/src/haz3lcore/assistant/AssistantExpander.re +++ /dev/null @@ -1,16 +0,0 @@ -/* We decorate buffers whose content will result in an - * expansion with a trailing "...". Note that this ... - * (at least in the current implementation) is not literally - * inserted into the syntax so will not be reflected - * in the decoration metrics */ - -let last = t => String.sub(t, String.length(t) - 1, 1); - -let is_expander = (label: Label.t) => - switch (label) { - | [t] => last(t) == " " || last(t) == "(" - | _ => false - }; - -let mark = (label: Label.t): Label.t => - is_expander(label) ? List.map(t => t ++ "…", label) : label; diff --git a/src/haz3lcore/prog/CachedStatics.re b/src/haz3lcore/derived/CachedStatics.re similarity index 99% rename from src/haz3lcore/prog/CachedStatics.re rename to src/haz3lcore/derived/CachedStatics.re index a82f89bdd8..2a3848e184 100644 --- a/src/haz3lcore/prog/CachedStatics.re +++ b/src/haz3lcore/derived/CachedStatics.re @@ -1,4 +1,5 @@ open Util; +open Semantics; [@deriving (show({with_path: false}), sexp, yojson)] type t = { diff --git a/src/haz3lcore/Measured.re b/src/haz3lcore/derived/Measured.re similarity index 100% rename from src/haz3lcore/Measured.re rename to src/haz3lcore/derived/Measured.re diff --git a/src/haz3lcore/derived/TermMap.re b/src/haz3lcore/derived/TermMap.re new file mode 100644 index 0000000000..0c8047f8c9 --- /dev/null +++ b/src/haz3lcore/derived/TermMap.re @@ -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); diff --git a/src/haz3lcore/TermRanges.re b/src/haz3lcore/derived/TermRanges.re similarity index 100% rename from src/haz3lcore/TermRanges.re rename to src/haz3lcore/derived/TermRanges.re diff --git a/src/haz3lcore/TileMap.re b/src/haz3lcore/derived/TileMap.re similarity index 100% rename from src/haz3lcore/TileMap.re rename to src/haz3lcore/derived/TileMap.re diff --git a/src/haz3lcore/dune b/src/haz3lcore/dune index 48eb441281..7cdea56366 100644 --- a/src/haz3lcore/dune +++ b/src/haz3lcore/dune @@ -2,7 +2,7 @@ (library (name haz3lcore) - (libraries util sexplib unionFind uuidm virtual_dom yojson core) + (libraries semantics util sexplib unionFind uuidm virtual_dom yojson core) (js_of_ocaml) (instrumentation (backend bisect_ppx)) diff --git a/src/haz3lcore/lang/Labels.re b/src/haz3lcore/lang/Labels.re deleted file mode 100644 index 822a1c0701..0000000000 --- a/src/haz3lcore/lang/Labels.re +++ /dev/null @@ -1,6 +0,0 @@ -let comma = [","]; - -let let_ = ["let", "=", "in"]; - -let case = ["case"]; -let rule = ["|", "=>"]; diff --git a/src/haz3lcore/statics/MakeTerm.re b/src/haz3lcore/lang/MakeTerm.re similarity index 99% rename from src/haz3lcore/statics/MakeTerm.re rename to src/haz3lcore/lang/MakeTerm.re index bc649d634a..7dcb3d7e6a 100644 --- a/src/haz3lcore/statics/MakeTerm.re +++ b/src/haz3lcore/lang/MakeTerm.re @@ -11,7 +11,7 @@ */ open Util; -open Any; +open Semantics; /* Hack: Temporary construct internal to maketerm * to handle probe parsing; see `tokens` below */ @@ -33,17 +33,17 @@ let tokens = ); [@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)); [@deriving (show({with_path: false}), sexp, yojson)] -type tiles = Aba.t(tile, t); +type tiles = Aba.t(tile, Any.t); 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); type t = { term: Exp.t, diff --git a/src/haz3lcore/lang/Precedence.re b/src/haz3lcore/lang/Precedence.re index 61c2d22e60..ce16bc28bc 100644 --- a/src/haz3lcore/lang/Precedence.re +++ b/src/haz3lcore/lang/Precedence.re @@ -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) diff --git a/src/haz3lcore/lang/Sort.re b/src/haz3lcore/lang/Sort.re index 91aeabc4b6..92162730ac 100644 --- a/src/haz3lcore/lang/Sort.re +++ b/src/haz3lcore/lang/Sort.re @@ -1,35 +1 @@ -[@deriving (show({with_path: false}), sexp, yojson)] -type t = - | Any - | Pat - | Typ - | TPat - | Rul - | Exp; - -let root = Exp; - -let consistent = (s, s') => - switch (s, s') { - | (Any, _) - | (_, Any) => true - | _ => s == s' - }; - -let to_string = - fun - | Any => "Any" - | Pat => "Pat" - | TPat => "TPat" - | Typ => "Typ" - | Rul => "Rul" - | Exp => "Exp"; - -let to_string_verbose = - fun - | Any => "any" - | Pat => "pattern" - | TPat => "type pattern" - | Typ => "type" - | Rul => "rule" - | Exp => "expression"; +include Semantics.Sort; diff --git a/src/haz3lcore/pretty/ExpToSegment.re b/src/haz3lcore/pretty/ExpToSegment.re index 628af85947..8a6c3e0925 100644 --- a/src/haz3lcore/pretty/ExpToSegment.re +++ b/src/haz3lcore/pretty/ExpToSegment.re @@ -1,6 +1,10 @@ open Util; open PrettySegment; open Base; +//TODO(andrew): ... +module Secondary2 = Secondary; +open Semantics; +module Secondary = Secondary2; module Settings = { type t = { diff --git a/src/haz3lcore/projectors/ProjectorBase.re b/src/haz3lcore/projectors/ProjectorBase.re index 10199a18a6..ac7718794e 100644 --- a/src/haz3lcore/projectors/ProjectorBase.re +++ b/src/haz3lcore/projectors/ProjectorBase.re @@ -1,5 +1,6 @@ open Util; open Virtual_dom.Vdom; +open Semantics; /* This descibes the API for projectors: GUIs which * can replace part of the program syntax and perform @@ -26,7 +27,7 @@ type external_action = [@deriving (show({with_path: false}), sexp, yojson)] type utility = { /* Convert a segment to a term */ - seg_to_term: Base.segment => option(Term.Any.t), + seg_to_term: Base.segment => option(Any.t), /* Convert a term to a segment */ term_to_seg: Any.t => Base.segment, /* Lifts term->term functions to syntax->syntax. This will @@ -78,12 +79,12 @@ type info = { /* Static information about the syntax including type * information. Statics may be disabled by the user; * this case (None) must be handled by projector authors */ - statics: option(Statics.Info.t), + statics: option(Semantics.Statics.Info.t), /* Dynamic information about the syntax including * live values of the syntax. Dynamics may be * disabled by the user; this case (None) must be * handled by projector authors */ - dynamics: option(Dynamics.Info.t), + dynamics: option(Semantics.Dynamics.Info.t), /* Syntax utility functions/values for projector use, * provided here to resolve cyclic dependency issues */ utility, @@ -140,7 +141,7 @@ module type Projector = { /* Init should return None if the projector doesn't want * to handle the provided term. Otherwise, it should * return the desired initial state of the model. */ - let init: Term.Any.t => option(model); + let init: Any.t => option(model); /* Does this projector have some notion of internal * positions, whose handling should override the editor * caret & keyboard handlers? If so, provide handlers diff --git a/src/haz3lcore/projectors/ProjectorInfo.re b/src/haz3lcore/projectors/ProjectorInfo.re index a6cca7f37a..164c015640 100644 --- a/src/haz3lcore/projectors/ProjectorInfo.re +++ b/src/haz3lcore/projectors/ProjectorInfo.re @@ -1,3 +1,5 @@ +open Semantics; + /* Projector data which is dependent on semantics, * separated out for dependency reasons */ diff --git a/src/haz3lcore/projectors/ProjectorInit.re b/src/haz3lcore/projectors/ProjectorInit.re index 7a7d620663..96aca9d000 100644 --- a/src/haz3lcore/projectors/ProjectorInit.re +++ b/src/haz3lcore/projectors/ProjectorInit.re @@ -19,7 +19,7 @@ let to_module = }; let init = - (kind: ProjectorCore.Kind.t, syntax: syntax, any: Term.Any.t) + (kind: ProjectorCore.Kind.t, syntax: syntax, any: Semantics.Any.t) : option(syntax) => { open ProjectorCore.Kind; let.gadt W(kind_gadt) = kind; @@ -34,7 +34,7 @@ let init = }; let init_or_noop = - (kind: ProjectorCore.Kind.t, syntax: syntax, any: Term.Any.t): syntax => + (kind: ProjectorCore.Kind.t, syntax: syntax, any: Semantics.Any.t): syntax => switch (init(kind, syntax, any)) { | Some(pr) => pr | None => syntax diff --git a/src/haz3lcore/projectors/implementations/CardProj.re b/src/haz3lcore/projectors/implementations/CardProj.re index 93169f27a1..9e3fd53220 100644 --- a/src/haz3lcore/projectors/implementations/CardProj.re +++ b/src/haz3lcore/projectors/implementations/CardProj.re @@ -1,6 +1,7 @@ open Util; open Virtual_dom.Vdom; open ProjectorBase; +open Semantics; [@deriving (show({with_path: false}), sexp, yojson)] type mode = ProjectorCore.Kind.card_mode; diff --git a/src/haz3lcore/projectors/implementations/CheckboxProj.re b/src/haz3lcore/projectors/implementations/CheckboxProj.re index ddd5838594..733f8abcb5 100644 --- a/src/haz3lcore/projectors/implementations/CheckboxProj.re +++ b/src/haz3lcore/projectors/implementations/CheckboxProj.re @@ -9,13 +9,13 @@ module M: Projector with type model = unit = { [@deriving (show({with_path: false}), sexp, yojson)] type action = unit; - let bool_of = (any: Any.t): option(bool) => + let bool_of = (any: Semantics.Any.t): option(bool) => switch (any) { | Exp({term: Atom(Bool(b)), _}) => Some(b) | _ => None }; - let init = (any: Term.Any.t) => + let init = (any: Semantics.Any.t) => switch (bool_of(any)) { | Some(_) => Some() | None => None diff --git a/src/haz3lcore/projectors/implementations/ProbeProj.re b/src/haz3lcore/projectors/implementations/ProbeProj.re index 490dccc803..197c3e9792 100644 --- a/src/haz3lcore/projectors/implementations/ProbeProj.re +++ b/src/haz3lcore/projectors/implementations/ProbeProj.re @@ -3,6 +3,7 @@ open ProjectorBase; open Virtual_dom.Vdom; open Node; open Js_of_ocaml; +open Semantics; [@deriving (show({with_path: false}), sexp, yojson)] type closure = Dynamics.Probe.Closure.t; diff --git a/src/haz3lcore/projectors/implementations/SliderFProj.re b/src/haz3lcore/projectors/implementations/SliderFProj.re index e3d6e5ef43..8c248bdb58 100644 --- a/src/haz3lcore/projectors/implementations/SliderFProj.re +++ b/src/haz3lcore/projectors/implementations/SliderFProj.re @@ -9,13 +9,13 @@ module M: Projector with type model = unit = { [@deriving (show({with_path: false}), sexp, yojson)] type action = unit; - let float_of = (any: Any.t): option(float) => + let float_of = (any: Semantics.Any.t): option(float) => switch (any) { | Exp({term: Atom(Float(f)), _}) => Some(f) | _ => None }; - let init = (any: Term.Any.t) => + let init = (any: Semantics.Any.t) => switch (float_of(any)) { | Some(_) => Some() | None => None diff --git a/src/haz3lcore/projectors/implementations/SliderProj.re b/src/haz3lcore/projectors/implementations/SliderProj.re index ae7b48e5bc..148d914007 100644 --- a/src/haz3lcore/projectors/implementations/SliderProj.re +++ b/src/haz3lcore/projectors/implementations/SliderProj.re @@ -9,13 +9,13 @@ module M: Projector with type model = unit = { [@deriving (show({with_path: false}), sexp, yojson)] type action = unit; - let int_of = (any: Any.t): option(Bigint.t) => + let int_of = (any: Semantics.Any.t): option(Bigint.t) => switch (any) { | Exp({term: Atom(Int(i)), _}) => Some(i) | _ => None }; - let init = (any: Term.Any.t) => + let init = (any: Semantics.Any.t) => switch (int_of(any)) { | Some(_) => Some() | None => None diff --git a/src/haz3lcore/projectors/implementations/TextAreaProj.re b/src/haz3lcore/projectors/implementations/TextAreaProj.re index 102eba96e3..ef4946f90e 100644 --- a/src/haz3lcore/projectors/implementations/TextAreaProj.re +++ b/src/haz3lcore/projectors/implementations/TextAreaProj.re @@ -2,7 +2,7 @@ open Util; open Virtual_dom.Vdom; open ProjectorBase; -let string_of = (any: Any.t): option(string) => +let string_of = (any: Semantics.Any.t): option(string) => switch (any) { | Exp({term: Atom(String(s)), _}) => Some(StringUtil.unescape_linebreaks(s)) @@ -87,7 +87,7 @@ module M: Projector with type model = unit = { [@deriving (show({with_path: false}), sexp, yojson)] type action = unit; - let init = (any: Term.Any.t) => + let init = (any: Semantics.Any.t) => switch (string_of(any)) { | Some(_) => Some() | None => None diff --git a/src/haz3lcore/projectors/implementations/TypeProj.re b/src/haz3lcore/projectors/implementations/TypeProj.re index 55c3c4f217..0c6ee70212 100644 --- a/src/haz3lcore/projectors/implementations/TypeProj.re +++ b/src/haz3lcore/projectors/implementations/TypeProj.re @@ -1,6 +1,7 @@ open Virtual_dom.Vdom; open Node; open ProjectorBase; +open Semantics; let expected_ty = (info: option(Info.t)): option(Typ.t) => switch (info) { @@ -54,7 +55,8 @@ module M: Projector with type model = ProjectorCore.Kind.type_model = { | Expected => statics |> expected_ty }; - let display_mode = (model: model, statics: option(Info.t)): string => + let display_mode = + (model: model, statics: option(Semantics.Info.t)): string => switch (model) { | _ when self_ty(statics) == expected_ty(statics) => "⇔" | _ when expected_ty(statics) |> totalize_ty |> Typ.is_syn => "⇒" diff --git a/src/haz3lcore/tiles/Secondary.re b/src/haz3lcore/tiles/Secondary.re index 13af22fddc..8982003624 100644 --- a/src/haz3lcore/tiles/Secondary.re +++ b/src/haz3lcore/tiles/Secondary.re @@ -1,9 +1,7 @@ open Util; [@deriving (show({with_path: false}), sexp, yojson, enumerate)] -type cls = - | Whitespace - | Comment; +type cls = Semantics.Secondary.cls; [@deriving (show({with_path: false}), sexp, yojson)] type secondary_content = diff --git a/src/haz3lcore/tiles/Skel.re b/src/haz3lcore/tiles/Skel.re index c2ed218cbb..7a07d49b9b 100644 --- a/src/haz3lcore/tiles/Skel.re +++ b/src/haz3lcore/tiles/Skel.re @@ -44,9 +44,12 @@ let rel = (p1: Piece.t, p2: Piece.t): option(rel) => | (Projector(_), _) => None | (_, Projector(_)) => None | (Tile(t1), Tile(t2)) => - open Labels; let lbl1 = (==)(t1.label); let lbl2 = (==)(t2.label); + //TODO: unhardcode + let comma = [","]; + let case = ["case"]; + let rule = ["|", "=>"]; let eq = [ lbl1(case) && lbl2(rule), diff --git a/src/haz3lcore/zipper/EditorUtil.re b/src/haz3lcore/zipper/EditorUtil.re deleted file mode 100644 index 0a6c213589..0000000000 --- a/src/haz3lcore/zipper/EditorUtil.re +++ /dev/null @@ -1,102 +0,0 @@ -let rec append_exp = (e1: Exp.t, e2: Exp.t): Exp.t => { - switch (e1.term) { - | EmptyHole - | Invalid(_) - | MultiHole(_) - | DynamicErrorHole(_) - | FailedCast(_) - | Undefined - | Deferral(_) - | Atom(_) - | ListLit(_) - | Constructor(_) - | Closure(_) - | Fun(_) - | TypFun(_) - | FixF(_) - | Tuple(_) - | TupLabel(_) - | Label(_) - | Dot(_) - | Var(_) - | Ap(_) - | TypAp(_) - | DeferredAp(_) - | If(_) - | Test(_) - | Parens(_) - | Probe(_) - | Cons(_) - | ListConcat(_) - | UnOp(_) - | BinOp(_) - | BuiltinFun(_) - | Cast(_) - | Match(_) => { - term: Seq(e1, e2), - annotation: { - ids: [Id.mk()], - }, - } - | Seq(e11, e12) => - let e12' = append_exp(e12, e2); - { - term: Seq(e11, e12'), - annotation: { - ids: IdTagged.ids(e1), - }, - }; - | Filter(kind, ebody) => - let ebody' = append_exp(ebody, e2); - { - term: Filter(kind, ebody'), - annotation: { - ids: IdTagged.ids(e1), - }, - }; - | Let(p, edef, ebody) => - let ebody' = append_exp(ebody, e2); - { - term: Let(p, edef, ebody'), - annotation: { - ids: IdTagged.ids(e1), - }, - }; - | TyAlias(tp, tdef, ebody) => - let ebody' = append_exp(ebody, e2); - { - term: TyAlias(tp, tdef, ebody'), - annotation: { - ids: IdTagged.ids(e1), - }, - }; - | Use(t, ebody) => - let ebody' = append_exp(ebody, e2); - { - term: Use(t, ebody'), - annotation: { - ids: IdTagged.ids(e1), - }, - }; - }; -}; - -let wrap_filter = (act: FilterAction.action, term: Exp.t): Exp.t => { - term: - Filter( - Filter({ - act: FilterAction.(act, One), - pat: { - term: - Constructor("$e", Some(Some(Unknown(Internal) |> Typ.fresh))), - annotation: { - ids: [Id.mk()], - }, - }, - }), - term, - ), - annotation: { - ids: [Id.mk()], - }, -}; diff --git a/src/haz3lcore/zipper/action/Indicated.re b/src/haz3lcore/zipper/action/Indicated.re index 2086695fc3..a911c2a3fa 100644 --- a/src/haz3lcore/zipper/action/Indicated.re +++ b/src/haz3lcore/zipper/action/Indicated.re @@ -102,7 +102,8 @@ let index = (z: ZipperBase.t): option(Id.t) => let piece'' = piece'(~no_ws=true, ~ign=Piece.is_secondary); let ci_of = - (z: ZipperBase.t, info_map: Statics.Map.t): option(Statics.Info.t) => + (z: ZipperBase.t, info_map: Semantics.Statics.Map.t) + : option(Semantics.Statics.Info.t) => /* This version takes into accounts Secondary, while accounting for the * fact that Secondary is not currently added to the info_map. First we * try the basic indication function, specifying that we do not want @@ -133,10 +134,10 @@ let ci_of = | _ => None }; let+ ci = Id.Map.find_opt(proxy_id, info_map); - Info.Secondary({ + Semantics.Statics.Info.Secondary({ id: proxy_id, cls: Secondary(cls), - sort: Info.sort_of(ci), - ctx: Info.ctx_of(ci), + sort: Semantics.Statics.Info.sort_of(ci), + ctx: Semantics.Statics.Info.ctx_of(ci), }); }; diff --git a/src/haz3lcore/zipper/action/Introduce.re b/src/haz3lcore/zipper/action/Introduce.re index d395de5f89..0909333910 100644 --- a/src/haz3lcore/zipper/action/Introduce.re +++ b/src/haz3lcore/zipper/action/Introduce.re @@ -1,3 +1,5 @@ +open Semantics; + module type Introducable = { type t; let parse: Segment.t => t; diff --git a/src/haz3lcore/zipper/action/Perform.re b/src/haz3lcore/zipper/action/Perform.re index f2a27dbf16..48ef222c4d 100644 --- a/src/haz3lcore/zipper/action/Perform.re +++ b/src/haz3lcore/zipper/action/Perform.re @@ -10,7 +10,7 @@ let buffer_clear = (z: t): t => | _ => z }; -let set_buffer = (info_map: Statics.Map.t, z: t): t => +let set_buffer = (info_map: Semantics.Statics.Map.t, z: t): t => switch (TyDi.set_buffer(~info_map, z)) { | None => z | Some(z) => z @@ -18,7 +18,7 @@ let set_buffer = (info_map: Statics.Map.t, z: t): t => let go_z = ( - ~settings as _: CoreSettings.t, + ~settings as _: Semantics.CoreSettings.t, statics: CachedStatics.t, a: Action.t, module M: Move.S, @@ -142,7 +142,7 @@ let go_z = open OptUtil.Syntax; let* idx = Indicated.index(z); let* ci = Id.Map.find_opt(idx, statics.info_map); - let* binding_id = Info.get_binding_site(ci); + let* binding_id = Semantics.Info.get_binding_site(ci); Move.jump_to_id(z, binding_id); | TileId(id) => Move.jump_to_id(z, id) } diff --git a/src/haz3lcore/zipper/action/Select.re b/src/haz3lcore/zipper/action/Select.re index 5900f64330..c2ae5d9645 100644 --- a/src/haz3lcore/zipper/action/Select.re +++ b/src/haz3lcore/zipper/action/Select.re @@ -167,10 +167,11 @@ module Make = (M: Move.S) => { let parent_cls = (z: Zipper.t, info_map) => { let* id = Indicated.index(z); - let* statics = Statics.Map.lookup(id, info_map); - let* parent_id = statics |> Info.ancestors_of |> ListUtil.hd_opt; - let+ parent_statics = Statics.Map.lookup(parent_id, info_map); - Info.cls_of(parent_statics); + let* statics = Semantics.Statics.Map.lookup(id, info_map); + let* parent_id = + statics |> Semantics.Statics.Info.ancestors_of |> ListUtil.hd_opt; + let+ parent_statics = Semantics.Statics.Map.lookup(parent_id, info_map); + Semantics.Statics.Info.cls_of(parent_statics); }; let parent_is_rule = (z: Zipper.t, info_map): option(Id.t) => { @@ -183,14 +184,15 @@ module Make = (M: Move.S) => { /* If the indicated term is the body of a definition * (let or type), return the id of the body, otherwise None */ let def_body_indicated = - (z: Zipper.t, info_map: Statics.Map.t): option(Id.t) => { + (z: Zipper.t, info_map: Semantics.Statics.Map.t): option(Id.t) => { let* id = Indicated.index(z); - let* statics = Statics.Map.lookup(id, info_map); - let* parent_id = statics |> Info.ancestors_of |> ListUtil.hd_opt; - let* ci_parent = Statics.Map.lookup(parent_id, info_map); + let* statics = Semantics.Statics.Map.lookup(id, info_map); + let* parent_id = + statics |> Semantics.Statics.Info.ancestors_of |> ListUtil.hd_opt; + let* ci_parent = Semantics.Statics.Map.lookup(parent_id, info_map); switch (ci_parent) { | InfoExp({term: {term: Let(_, _, body) | TyAlias(_, _, body), _}, _}) => - let body_id = IdTagged.rep_id(body); + let body_id = Semantics.IdTagged.rep_id(body); id == body_id ? Some(body_id) : None; | _ => None }; @@ -204,7 +206,7 @@ module Make = (M: Move.S) => { | Some(id) => Some(id) | _ => let* statics = Id.Map.find_opt(base_id, info_map); - statics |> Info.ancestors_of |> ListUtil.hd_opt; + statics |> Semantics.Info.ancestors_of |> ListUtil.hd_opt; }; }; diff --git a/src/haz3lmenhir/AST.re b/src/haz3lmenhir/AST.re index 421f4ac8c3..181f2546db 100644 --- a/src/haz3lmenhir/AST.re +++ b/src/haz3lmenhir/AST.re @@ -111,7 +111,7 @@ type pat = | CastPat(pat, typ, typ) | EmptyHolePat | WildPat - | AtomPat(Haz3lcore.Atom.t) + | AtomPat(Semantics.Atom.t) | VarPat(string) | ConstructorPat(string, option(option(typ))) | TuplePat(list(pat)) @@ -135,7 +135,7 @@ type deferral_pos = [@deriving (show({with_path: false}), sexp, eq)] type exp = - | Atom(Haz3lcore.Atom.t) + | Atom(Semantics.Atom.t) | Var(string) | Constructor(string, option(option(typ))) | ListExp(list(exp)) @@ -183,7 +183,8 @@ let gen_constructor_ident: QCheck.Gen.t(string) = let* leading = char_range('A', 'Z'); let+ tail = string_size(~gen=char_range('a', 'z'), int_range(1, 4)); let ident = String.make(1, leading) ++ tail; - if (List.exists(a => a == ident, Haz3lcore.Form.base_typs)) { + //TODO(andrew): copied list of base types below to remove Form dep... + if (List.exists(a => a == ident, ["String", "Int", "Float", "Bool"])) { "Keyword"; } else { ident; diff --git a/src/haz3lmenhir/Conversion.re b/src/haz3lmenhir/Conversion.re index c1e3136bb5..c1da1e771c 100644 --- a/src/haz3lmenhir/Conversion.re +++ b/src/haz3lmenhir/Conversion.re @@ -1,12 +1,12 @@ include Sexplib.Std; module IndicatedG = - Haz3lcore.Grammar.Factory({ + Semantics.Grammar.Factory({ type t = bool; let default_value = () => false; }); module FilterAction = { - open Haz3lcore.FilterAction; + open Semantics.FilterAction; let of_menhir_ast = (a: AST.filter_action): t => { switch (a) { | Eval => (Eval, All) @@ -27,7 +27,7 @@ module FilterAction = { }; module Operators = { - open Haz3lcore.Operators; + open Semantics.Operators; let op_un_meta_of_menhir_ast = (op: AST.op_un_meta) => { switch (op) { @@ -199,7 +199,7 @@ module rec Exp: { let of_menhir_ast: AST.exp => IndicatedG.exp; let of_core: IndicatedG.exp => AST.exp; let get_indicated_ids: - IndicatedG.exp => (Haz3lcore.Exp.t, list(Haz3lcore.Id.t)); + IndicatedG.exp => (Semantics.Exp.t, list(Semantics.Id.t)); } = { open IndicatedG.Exp; let rec of_menhir_ast = (exp: AST.exp): IndicatedG.exp => { @@ -245,7 +245,7 @@ module rec Exp: { List.mem(AST.Deferral, l) ? deferred_ap(of_menhir_ast(e1), List.map(of_menhir_ast, l)) : ap( - Haz3lcore.Operators.Forward, + Semantics.Operators.Forward, of_menhir_ast(e1), of_menhir_ast(args), ) @@ -253,7 +253,7 @@ module rec Exp: { | _ => ap( - Haz3lcore.Operators.Forward, + Semantics.Operators.Forward, of_menhir_ast(e1), of_menhir_ast(args), ) @@ -306,7 +306,7 @@ module rec Exp: { | DynamicErrorHole(e, s) => dynamic_error_hole( of_menhir_ast(e), - Haz3lcore.InvalidOperationError.t_of_sexp(sexp_of_string(s)), + Semantics.InvalidOperationError.t_of_sexp(sexp_of_string(s)), ) | IndicationExp(e) => { annotation: true, @@ -356,7 +356,7 @@ module rec Exp: { | DynamicErrorHole(e, s) => DynamicErrorHole( of_core(e), - Sexplib.Sexp.to_string(Haz3lcore.InvalidOperationError.sexp_of_t(s)), + Sexplib.Sexp.to_string(Semantics.InvalidOperationError.sexp_of_t(s)), ) | Deferral(_) => Deferral | Filter(Residue(_), _) => raise(Failure("Residue not supported")) @@ -378,8 +378,8 @@ module rec Exp: { let get_indicated_ids = (indicated_exp: IndicatedG.exp) - : (Haz3lcore.Exp.t, list(Haz3lcore.Id.t)) => { - open Haz3lcore; + : (Semantics.Exp.t, list(Semantics.Id.t)) => { + open Semantics; // mutable array to gather indicated IDs when generating expressions let indicated_ids = Dynarray.create(); let e = @@ -425,7 +425,7 @@ and Typ: { | ArrayType(t) => list(of_menhir_ast(t)) | ArrowType(t1, t2) => arrow(of_menhir_ast(t1), of_menhir_ast(t2)) | SumTyp(sumterms) => - open Haz3lcore; + open Semantics; let converted_terms: list(ConstructorMap.variant(IndicatedG.typ)) = List.map( (sumterm: AST.sumterm): ConstructorMap.variant(IndicatedG.typ) => @@ -478,7 +478,7 @@ and Typ: { | Sum(constructors) => let sumterms = List.map( - (variant: Haz3lcore.ConstructorMap.variant(IndicatedG.typ)): AST.sumterm => { + (variant: Semantics.ConstructorMap.variant(IndicatedG.typ)): AST.sumterm => { switch (variant) { | Variant(name, _, None) => Variant(name, None) | Variant(name, _, Some(t)) => Variant(name, Some(of_core(t))) diff --git a/src/haz3lmenhir/dune b/src/haz3lmenhir/dune index d86a64d07e..97f7436887 100644 --- a/src/haz3lmenhir/dune +++ b/src/haz3lmenhir/dune @@ -1,6 +1,6 @@ (library (name haz3lmenhir) - (libraries util re sexplib unionFind haz3lcore qcheck-alcotest) + (libraries util re sexplib unionFind semantics qcheck-alcotest) (modules AST Conversion Interface Lexer Parser) (instrumentation (backend bisect_ppx)) diff --git a/src/haz3lcore/Animation.re b/src/haz3lweb/Animation.re similarity index 100% rename from src/haz3lcore/Animation.re rename to src/haz3lweb/Animation.re diff --git a/src/haz3lcore/ClipboardCache.re b/src/haz3lweb/ClipboardCache.re similarity index 98% rename from src/haz3lcore/ClipboardCache.re rename to src/haz3lweb/ClipboardCache.re index 0ad854d813..3a175ed9b4 100644 --- a/src/haz3lcore/ClipboardCache.re +++ b/src/haz3lweb/ClipboardCache.re @@ -1,3 +1,5 @@ +open Haz3lcore; + /* In order to retain projectors on cut/copy/paste, and to speed * up pasting after in-editor copy/cut, we maintain a cached of * the last copied selection segment and do segment insertion diff --git a/src/haz3lweb/Main.re b/src/haz3lweb/Main.re index 53214d83fe..d6fca3f972 100644 --- a/src/haz3lweb/Main.re +++ b/src/haz3lweb/Main.re @@ -173,7 +173,7 @@ let start = { } else { (); }; - model.globals.settings.core.statics ? Haz3lcore.Animation.go() : (); + model.globals.settings.core.statics ? Animation.go() : (); }, (), ); diff --git a/src/haz3lweb/Settings.re b/src/haz3lweb/Settings.re index 1e478acd24..c8311b5727 100644 --- a/src/haz3lweb/Settings.re +++ b/src/haz3lweb/Settings.re @@ -5,7 +5,7 @@ module Model = { type t = { captions: bool, secondary_icons: bool, - core: Haz3lcore.CoreSettings.t, + core: Semantics.CoreSettings.t, async_evaluation: bool, context_inspector: bool, instructor_mode: bool, @@ -143,7 +143,7 @@ module Update = { } | Evaluation(u) => let evaluation = settings.core.evaluation; - let evaluation: Haz3lcore.CoreSettings.Evaluation.t = + let evaluation: Semantics.CoreSettings.Evaluation.t = switch (u) { | ShowRecord => { ...evaluation, diff --git a/src/haz3lweb/app/Cursor.re b/src/haz3lweb/app/Cursor.re index 827ac27c78..1a6c6c7b8e 100644 --- a/src/haz3lweb/app/Cursor.re +++ b/src/haz3lweb/app/Cursor.re @@ -1,5 +1,5 @@ type cursor('update) = { - info: option(Haz3lcore.Info.t), + info: option(Semantics.Info.t), selected_text: option(unit => string), selection: option(Haz3lcore.Segment.t), indicated_piece: option(Haz3lcore.Piece.t), diff --git a/src/haz3lweb/app/common/ProjectorView.re b/src/haz3lweb/app/common/ProjectorView.re index e56d5f3a8b..6ff793e57c 100644 --- a/src/haz3lweb/app/common/ProjectorView.re +++ b/src/haz3lweb/app/common/ProjectorView.re @@ -50,10 +50,11 @@ module Model = { ~id: Id.t, ) => { sort: - Option.map(Info.sort_of, info.statics) + Option.map(Semantics.Info.sort_of, info.statics) |> Option.value(~default=Sort.Exp), error: - Option.map(Info.is_error, info.statics) |> Option.value(~default=false), + Option.map(Semantics.Info.is_error, info.statics) + |> Option.value(~default=false), kind: p.kind, indication: editor_active ? indication(indicated, id) : None, selected: editor_active ? List.mem(id, selection_ids) : false, @@ -65,8 +66,8 @@ module Model = { measured: Measured.t, selection_ids: list(Id.t), indicated: option(Indicated.piece), - statics: Statics.Map.t, - dynamics: Dynamics.Map.t, + statics: Semantics.Statics.Map.t, + dynamics: Semantics.Dynamics.Map.t, editor_active: bool, ) => { List.filter_map( diff --git a/src/haz3lweb/app/editors/SettingsModal.re b/src/haz3lweb/app/editors/SettingsModal.re index f840948d7f..eb8ed6f1ab 100644 --- a/src/haz3lweb/app/editors/SettingsModal.re +++ b/src/haz3lweb/app/editors/SettingsModal.re @@ -1,11 +1,10 @@ open Virtual_dom.Vdom; open Node; -open Haz3lcore; let view = ( ~inject: Settings.Update.t => Ui_effect.t(unit), - settings: CoreSettings.Evaluation.t, + settings: Semantics.CoreSettings.Evaluation.t, ) => { let modal = div(~attrs=[Attr.class_("settings-modal")]); let setting = (icon, name, current, action: Settings.Update.t) => @@ -49,7 +48,7 @@ let view = Evaluation(ShowFixpoints), ), setting( - Unicode.castArrowSym, + Util.Unicode.castArrowSym, "show casts", settings.show_casts, Evaluation(ShowCasts), diff --git a/src/haz3lweb/app/editors/cell/CellEditor.re b/src/haz3lweb/app/editors/cell/CellEditor.re index e029cfb38a..dbfa9bf124 100644 --- a/src/haz3lweb/app/editors/cell/CellEditor.re +++ b/src/haz3lweb/app/editors/cell/CellEditor.re @@ -16,7 +16,7 @@ module Model = { editor: { editor, statics: CachedStatics.empty, - dynamics: Dynamics.Map.empty, + dynamics: Semantics.Dynamics.Map.empty, }, result: EvalResult.Model.init, }; diff --git a/src/haz3lweb/app/editors/code/CodeEditable.re b/src/haz3lweb/app/editors/code/CodeEditable.re index e3240d2e86..8d4aa472f4 100644 --- a/src/haz3lweb/app/editors/code/CodeEditable.re +++ b/src/haz3lweb/app/editors/code/CodeEditable.re @@ -66,7 +66,10 @@ module Update = { }, ); switch (action) { - | Perform(action) => perform(action, model) + | Perform(action) => + settings.core.flip_animations && Action.should_animate(action) + ? Animation.request([Animation.Actions.move("caret")]) : (); + perform(action, model); | Undo => switch (Editor.Update.undo(model.editor)) { | Some(editor) => diff --git a/src/haz3lweb/app/editors/code/CodeViewable.re b/src/haz3lweb/app/editors/code/CodeViewable.re index 2e333095ef..6aa252ad0d 100644 --- a/src/haz3lweb/app/editors/code/CodeViewable.re +++ b/src/haz3lweb/app/editors/code/CodeViewable.re @@ -37,14 +37,14 @@ let view_segment = view(~globals, ~sort, ~measured, ~buffer_ids, ~segment, ~shape_map); }; -let view_typ = (~globals: Globals.t, ~settings, typ: Typ.t) => { +let view_typ = (~globals: Globals.t, ~settings, typ: Semantics.Typ.t) => { let shape_map = ProjectorCore.Shape.Map.empty; // assume no projectors typ |> ExpToSegment.typ_to_segment(~settings) |> view_segment(~shape_map, ~globals, ~sort=Typ); }; -let view_any = (~globals: Globals.t, ~settings, any: Any.t) => { +let view_any = (~globals: Globals.t, ~settings, any: Semantics.Any.t) => { any |> ExpToSegment.any_to_segment(~settings) |> view_segment(~globals, ~sort=Any); diff --git a/src/haz3lweb/app/editors/code/CodeWithStatics.re b/src/haz3lweb/app/editors/code/CodeWithStatics.re index 0da315083a..4d20b9fa0b 100644 --- a/src/haz3lweb/app/editors/code/CodeWithStatics.re +++ b/src/haz3lweb/app/editors/code/CodeWithStatics.re @@ -13,16 +13,21 @@ module Model = { // Updated: editor: Editor.t, statics: CachedStatics.t, - dynamics: Dynamics.Map.t, + dynamics: Semantics.Dynamics.Map.t, }; let mk = editor => { editor, statics: CachedStatics.empty, - dynamics: Dynamics.Map.empty, + dynamics: Semantics.Dynamics.Map.empty, }; - let mk_from_exp = (~settings: CoreSettings.t, ~inline=false, term: Exp.t) => { + let mk_from_exp = + ( + ~settings: Semantics.CoreSettings.t, + ~inline=false, + term: Semantics.Exp.t, + ) => { ExpToSegment.exp_to_segment( term, ~settings=ExpToSegment.Settings.of_core(~inline, settings), @@ -71,7 +76,7 @@ module Update = { ~settings, ~is_edited, ~stitch, - ~dynamics: Dynamics.Map.t, + ~dynamics: Semantics.Dynamics.Map.t, ~is_dynamic_term, {editor, statics, dynamics: _}: Model.t, ) diff --git a/src/haz3lweb/app/editors/decoration/Deco.re b/src/haz3lweb/app/editors/decoration/Deco.re index 7afd859a9e..15eebcc45d 100644 --- a/src/haz3lweb/app/editors/decoration/Deco.re +++ b/src/haz3lweb/app/editors/decoration/Deco.re @@ -277,7 +277,7 @@ module Deco = ); let term_range = (p): option((Point.t, Point.t)) => { - let id = Any.rep_id(Id.Map.find(Piece.id(p), terms)); + let id = Semantics.Any.rep_id(Id.Map.find(Piece.id(p), terms)); switch (TermRanges.find_opt(id, term_ranges)) { | None => None | Some((p_l, p_r)) => @@ -289,7 +289,7 @@ module Deco = let all_tiles = (p: Piece.t): list((Uuidm.t, Mold.t, Measured.Shards.t)) => Id.Map.find(Piece.id(p), terms) - |> Any.ids + |> Semantics.Any.ids |> List.map(id => { let t = tile(id); let shards = Measured.find_shards(~msg="all_tiles", t, measured); @@ -548,7 +548,7 @@ module Deco = let shards = Measured.find_shards(t, map); let range: option((Measured.Point.t, Measured.Point.t)) = { // if (Piece.has_ends(p)) { - let id = Id.Map.find(id, terms) |> Any.rep_id; + let id = Id.Map.find(id, terms) |> Semantics.Any.rep_id; switch (TermRanges.find_opt(id, term_ranges)) { | None => None | Some((p_l, p_r)) => @@ -598,7 +598,7 @@ module Deco = let shards = Measured.find_shards(t, map); let range: option((Measured.Point.t, Measured.Point.t)) = { // if (Piece.has_ends(p)) { - let id = Id.Map.find(id, terms) |> Any.rep_id; + let id = Id.Map.find(id, terms) |> Semantics.Any.rep_id; switch (TermRanges.find_opt(id, term_ranges)) { | None => None | Some((p_l, p_r)) => diff --git a/src/haz3lweb/app/editors/result/EvalResult.re b/src/haz3lweb/app/editors/result/EvalResult.re index 7b2f763de0..3871b8ba0e 100644 --- a/src/haz3lweb/app/editors/result/EvalResult.re +++ b/src/haz3lweb/app/editors/result/EvalResult.re @@ -1,5 +1,5 @@ open Util; -open Haz3lcore; +open Semantics; /* The result box at the bottom of a cell. This is either the TestResutls kind where only a summary of test results is shown, or the EvalResults kind @@ -17,15 +17,10 @@ module Model = { type result = | NoElab | Evaluation({ - elab: Haz3lcore.Exp.t, - result: - Calc.t( - Haz3lcore.ProgramResult.t( - (Haz3lcore.Exp.t, Haz3lcore.EvaluatorState.t), - ), - ), - cached_settings: Calc.saved(Haz3lcore.CoreSettings.t), - editor: Calc.saved((Haz3lcore.Exp.t, CodeSelectable.Model.t)), + elab: Exp.t, + result: Calc.t(ProgramResult.t((Exp.t, EvaluatorState.t))), + cached_settings: Calc.saved(CoreSettings.t), + editor: Calc.saved((Exp.t, CodeSelectable.Model.t)), }) | Stepper(StepperView.Model.t); @@ -86,7 +81,7 @@ module Model = { | None => Dynamics.Map.mk(Dynamics.Probe.Map.empty) }; - let get_elaboration = (model: t): option(Haz3lcore.Exp.t) => + let get_elaboration = (model: t): option(Exp.t) => switch (model.result) { | Evaluation({elab, _}) => Some(elab) | Stepper(s) => StepperView.Model.get_elaboration(s) @@ -102,7 +97,7 @@ module Update = { | ToggleStepper | StepperAction(StepperView.Update.t) | EvalEditorAction(CodeSelectable.Update.t) - | UpdateResult(Haz3lcore.ProgramResult.t(Haz3lcore.ProgramResult.inner)); + | UpdateResult(ProgramResult.t(ProgramResult.inner)); // Update is meant to make minimal changes to the model, and calculate will do the rest. let update = (~settings, action, model: Model.t): Updated.t(Model.t) => @@ -162,8 +157,8 @@ module Update = { elab, result: NewValue( - Haz3lcore.ProgramResult.map( - ({result: exp, state: s}: Haz3lcore.ProgramResult.inner) => { + ProgramResult.map( + ({result: exp, state: s}: ProgramResult.inner) => { (exp, s) }, update, @@ -186,8 +181,8 @@ module Update = { let calculate = ( - ~settings: Haz3lcore.CoreSettings.t, - ~queue_worker: option(Haz3lcore.Exp.t => unit), + ~settings: CoreSettings.t, + ~queue_worker: option(Exp.t => unit), ~is_edited: bool, statics: Haz3lcore.CachedStatics.t, model: Model.t, @@ -200,7 +195,7 @@ module Update = { Evaluation, Evaluation({elab: elab', result, cached_settings, editor}), ) - when Haz3lcore.Exp.fast_equal(elab, elab') => { + when Exp.fast_equal(elab, elab') => { ...model, result: Evaluation({ @@ -221,9 +216,8 @@ module Update = { result: { switch (WorkerServer.work(elab)) { | Ok((exp, state)) => - NewValue(Haz3lcore.ProgramResult.ResultOk((exp, state))) - | Error(e) => - NewValue(Haz3lcore.ProgramResult.ResultFail(e)) + NewValue(ProgramResult.ResultOk((exp, state))) + | Error(e) => NewValue(ProgramResult.ResultFail(e)) }; }, cached_settings: Pending, @@ -238,7 +232,7 @@ module Update = { result: Evaluation({ elab, - result: NewValue(Haz3lcore.ProgramResult.ResultPending), + result: NewValue(ProgramResult.ResultPending), cached_settings: Pending, editor: Pending, }), @@ -278,10 +272,7 @@ module Update = { switch (result) { | ResultOk((exp, _state)) => exp - |> ( - settings.evaluation.show_casts - ? (x => x) : Haz3lcore.DHExp.strip_casts - ) + |> (settings.evaluation.show_casts ? (x => x) : DHExp.strip_casts) |> CodeSelectable.Model.mk_from_exp(~settings) |> (x => Calc.Calculated((exp, x))) | ResultFail(_) => Pending @@ -365,16 +356,16 @@ module View = { type event = | MakeActive(Selection.t) - | JumpTo(Haz3lcore.Id.t); + | JumpTo(Id.t); - let error_msg = (err: Haz3lcore.ProgramResult.error) => + let error_msg = (err: ProgramResult.error) => switch (err) { - | EvaulatorError(err) => Haz3lcore.EvaluatorError.show(err) + | EvaulatorError(err) => EvaluatorError.show(err) | UnknownException(str) => str | Timeout => "Evaluation timed out" }; - let status_of: Haz3lcore.ProgramResult.t('a) => string = + let status_of: ProgramResult.t('a) => string = fun | ResultPending => "pending" | ResultOk(_) => "ok" @@ -388,11 +379,8 @@ module View = { ~inject: Update.t => Ui_effect.t(unit), ~selected, ~locked, - elab: Haz3lcore.Exp.t, - result: - Haz3lcore.ProgramResult.t( - (Haz3lcore.Exp.t, Haz3lcore.EvaluatorState.t), - ), + elab: Exp.t, + result: ProgramResult.t((Exp.t, EvaluatorState.t)), editor: Calc.saved(('a, CodeSelectable.Model.t)), ) => { let editor = @@ -410,7 +398,7 @@ module View = { ~inject=a => inject(EvalEditorAction(a)), ~globals, ~selected, - ~sort=Haz3lcore.Sort.root, + ~sort=Sort.root, editor, ); let exn_view = @@ -500,10 +488,7 @@ module View = { (~font_metrics, insts, ms: Haz3lcore.Measured.Shards.t): option(Node.t) => switch (ms) { | [(_, {origin: _, last}), ..._] => - let status = - insts - |> Haz3lcore.TestMap.joint_status - |> Haz3lcore.TestStatus.to_string; + let status = insts |> TestMap.joint_status |> TestStatus.to_string; let pos = DecUtil.abs_position(~font_metrics, last); Some( Node.div(~attrs=[Attr.classes(["test-result", status]), pos], []), @@ -515,14 +500,14 @@ module View = { ( ~font_metrics, ~measured: Haz3lcore.Measured.t, - test_results: Haz3lcore.TestResults.t, + test_results: TestResults.t, ) : Web.Node.t => Web.div_c( "test-decos", List.filter_map( ((id, insts)) => - switch (Haz3lcore.Id.Map.find_opt(id, measured.tiles)) { + switch (Id.Map.find_opt(id, measured.tiles)) { | Some(ms) => test_status_icon_view(~font_metrics, insts, ms) | None => None }, @@ -570,7 +555,7 @@ module View = { text("Evaluation disabled, showing elaboration:"), switch (Model.get_elaboration(model)) { | Some(elab) => - let shape_map = ProjectorCore.Shape.Map.empty; // assume no projectors + let shape_map = Haz3lcore.ProjectorCore.Shape.Map.empty; // assume no projectors elab |> Haz3lcore.ExpToSegment.( exp_to_segment( diff --git a/src/haz3lweb/app/editors/result/StepperEditor.re b/src/haz3lweb/app/editors/result/StepperEditor.re index 080dacec6e..dd434648fb 100644 --- a/src/haz3lweb/app/editors/result/StepperEditor.re +++ b/src/haz3lweb/app/editors/result/StepperEditor.re @@ -35,7 +35,7 @@ module Update = { ~settings, ~is_edited, ~stitch, - ~dynamics: Dynamics.Map.t, + ~dynamics: Semantics.Dynamics.Map.t, {editor, taken_steps, next_steps}: Model.t, ) : Model.t => { diff --git a/src/haz3lweb/app/explainthis/ExplainThis.re b/src/haz3lweb/app/explainthis/ExplainThis.re index 77b3624bc1..39c7eafaa9 100644 --- a/src/haz3lweb/app/explainthis/ExplainThis.re +++ b/src/haz3lweb/app/explainthis/ExplainThis.re @@ -2,6 +2,7 @@ open Virtual_dom.Vdom; open Node; open Util.Web; open Haz3lcore; +open Semantics; /* If you are adding docs here for new syntax, see PipelineExp.re * which documents the simplest way to add a new form. */ diff --git a/src/haz3lweb/app/explainthis/ExplainThisForm.re b/src/haz3lweb/app/explainthis/ExplainThisForm.re index 418bb0a319..6e7d0771ef 100644 --- a/src/haz3lweb/app/explainthis/ExplainThisForm.re +++ b/src/haz3lweb/app/explainthis/ExplainThisForm.re @@ -198,8 +198,8 @@ type form_id = | SeqExp | UseExp | TestExp - | UnOpExp(Operators.op_un) - | BinOpExp(Operators.op_bin) + | UnOpExp(Semantics.Operators.op_un) + | BinOpExp(Semantics.Operators.op_bin) | CaseExp | TyAliasExp | EmptyHolePat @@ -301,8 +301,8 @@ type group_id = | IfExp | SeqExp | TestExp - | UnOpExp(Operators.op_un) - | BinOpExp(Operators.op_bin) + | UnOpExp(Semantics.Operators.op_un) + | BinOpExp(Semantics.Operators.op_bin) | CaseExp | TyAliasExp | PipelineExp diff --git a/src/haz3lweb/app/explainthis/data/DotExp.re b/src/haz3lweb/app/explainthis/data/DotExp.re index 726b1f3de4..e7c3c61d0f 100644 --- a/src/haz3lweb/app/explainthis/data/DotExp.re +++ b/src/haz3lweb/app/explainthis/data/DotExp.re @@ -1,4 +1,5 @@ open Haz3lcore; +open Semantics; open ExplainThisForm; open Example; diff --git a/src/haz3lweb/app/globals/Globals.re b/src/haz3lweb/app/globals/Globals.re index a1608dad4c..4a54186d0c 100644 --- a/src/haz3lweb/app/globals/Globals.re +++ b/src/haz3lweb/app/globals/Globals.re @@ -39,7 +39,7 @@ module Model = { get_log_and: (string => unit) => unit, export_all: ( - ~settings: Haz3lcore.CoreSettings.t, + ~settings: Semantics.CoreSettings.t, ~instructor_mode: bool, ~log: string ) => diff --git a/src/haz3lweb/app/inspector/CursorInspector.re b/src/haz3lweb/app/inspector/CursorInspector.re index 719d36977b..56fabddbfe 100644 --- a/src/haz3lweb/app/inspector/CursorInspector.re +++ b/src/haz3lweb/app/inspector/CursorInspector.re @@ -2,7 +2,7 @@ open Virtual_dom.Vdom; open Node; open Util.Web; open Util; -open Haz3lcore; +open Semantics; let errc = "error"; let okc = "ok"; @@ -88,7 +88,7 @@ let elements_noun: Cls.t => string = | Exp(ListConcat) => "Operands" | _ => failwith("elements_noun: Cls doesn't have elements"); -let code_view_settings: ExpToSegment.Settings.t = { +let code_view_settings: Haz3lcore.ExpToSegment.Settings.t = { inline: true, fold_case_clauses: false, fold_fn_bodies: false, @@ -103,7 +103,7 @@ let view_any = (~globals, any: Term.Any.t) => |> CodeViewable.view_any( ~globals, ~settings=code_view_settings, - ~shape_map=ProjectorCore.Shape.Map.empty // assume no projectors + ~shape_map=Haz3lcore.ProjectorCore.Shape.Map.empty // assume no projectors ) |> code_box_container; @@ -126,7 +126,7 @@ let common_err_view = ( switch (err) { | NoType(BadToken(token)) => - switch (Form.bad_token_cls(token)) { + switch (Haz3lcore.Form.bad_token_cls(token)) { | BadInt => [text("Integer is too large or too small")] | Other => [text(Printf.sprintf("\"%s\" isn't a valid token", token))] } diff --git a/src/haz3lweb/app/inspector/ProjectorPanel.re b/src/haz3lweb/app/inspector/ProjectorPanel.re index b3919550d5..92c40d8f6c 100644 --- a/src/haz3lweb/app/inspector/ProjectorPanel.re +++ b/src/haz3lweb/app/inspector/ProjectorPanel.re @@ -25,7 +25,7 @@ module Applicable = { MakeTerm.for_projection(Piece.unparenthesize(syntax)) | _ => let* info = cursor.info; - Info.any_of(info); + Semantics.Info.any_of(info); } | Some([Projector({syntax, _})]) => MakeTerm.for_projection(Piece.unparenthesize(syntax)) diff --git a/src/haz3lweb/debug/DebugConsole.re b/src/haz3lweb/debug/DebugConsole.re index fc6aa90a9b..8bd7954364 100644 --- a/src/haz3lweb/debug/DebugConsole.re +++ b/src/haz3lweb/debug/DebugConsole.re @@ -14,14 +14,14 @@ let print = switch (key) { | "F1" => zipper |> Zipper.show |> print | "F2" => zipper |> Zipper.unselect_and_zip |> Segment.show |> print - | "F3" => term |> Exp.show |> print - | "F4" => map |> Statics.Map.show |> print + | "F3" => term |> Semantics.Exp.show |> print + | "F4" => map |> Semantics.Statics.Map.show |> print | "F5" when settings.core.dynamics => - let env_init = Builtins.env_init; + let env_init = Semantics.Builtins.env_init; statics.elaborated - |> Evaluator.evaluate(~env=env_init) + |> Semantics.Evaluator.evaluate(~env=env_init) |> fst - |> DHExp.show + |> Semantics.DHExp.show |> print; | "F5" => print("Dynamics disabled, cannot show evaluation.") | "F6" => @@ -30,7 +30,7 @@ let print = | Some(index) => print("id:" ++ Id.to_string(index)); switch (Id.Map.find_opt(index, map)) { - | Some(ci) => print(Info.show(ci)) + | Some(ci) => print(Semantics.Info.show(ci)) | None => print("DEBUG: No CI found for index") }; | None => print("DEBUG: No indicated index") diff --git a/src/haz3lweb/exercises/Exercise.re b/src/haz3lweb/exercises/Exercise.re index 061828b495..5fe7cec4d4 100644 --- a/src/haz3lweb/exercises/Exercise.re +++ b/src/haz3lweb/exercises/Exercise.re @@ -87,7 +87,7 @@ type pos = type spec = p(Zipper.t); [@deriving (show({with_path: false}), sexp, yojson)] -type transitionary_spec = p(CodeString.t); +type transitionary_spec = p(string); let map = (p: p('a), f: 'a => 'b, f_hidden: 'a => 'b): p('b) => { { @@ -329,7 +329,7 @@ let eds_of_spec = hidden_tests, syntax_tests, }, - ~settings as _: CoreSettings.t, + ~settings as _: Semantics.CoreSettings.t, ) => { let editor_of_serialization = Editor.Model.mk; let prelude = editor_of_serialization(prelude); @@ -397,7 +397,7 @@ let visible_in = (pos, ~instructor_mode) => { module TermItem = { type t = { - term: Exp.t, + term: Semantics.Exp.t, editor: Editor.t, }; }; @@ -475,14 +475,19 @@ let put_stitched = (pos, s: stitched('a), x: 'a): stitched('a) => } }; -let wrap_filter = (act: FilterAction.action, term: Exp.t): Exp.t => { +let wrap_filter = + (act: Semantics.FilterAction.action, term: Semantics.Exp.t) + : Semantics.Exp.t => { term: Filter( Filter({ - act: FilterAction.(act, One), + act: Semantics.FilterAction.(act, One), pat: { term: - Constructor("$e", Some(Some(Unknown(Internal) |> Typ.fresh))), + Constructor( + "$e", + Some(Some(Unknown(Internal) |> Semantics.Typ.fresh)), + ), annotation: { ids: [Id.mk()], }, @@ -500,31 +505,112 @@ let wrap = (term, editor: Editor.t): TermItem.t => { editor, }; -let term_of = (editor: Editor.t): Exp.t => +let term_of = (editor: Editor.t): Semantics.Exp.t => MakeTerm.from_zip_for_sem(editor.state.zipper).term; +let rec append_exp = + (e1: Semantics.Exp.t, e2: Semantics.Exp.t): Semantics.Exp.t => { + switch (e1.term) { + | EmptyHole + | Invalid(_) + | MultiHole(_) + | DynamicErrorHole(_) + | FailedCast(_) + | Undefined + | Deferral(_) + | Atom(_) + | ListLit(_) + | Constructor(_) + | Closure(_) + | Fun(_) + | TypFun(_) + | FixF(_) + | Tuple(_) + | TupLabel(_) + | Label(_) + | Dot(_) + | Var(_) + | Ap(_) + | TypAp(_) + | DeferredAp(_) + | If(_) + | Test(_) + | Parens(_) + | Probe(_) + | Cons(_) + | ListConcat(_) + | UnOp(_) + | BinOp(_) + | BuiltinFun(_) + | Cast(_) + | Match(_) => { + term: Seq(e1, e2), + annotation: { + ids: [Id.mk()], + }, + } + | Seq(e11, e12) => + let e12' = append_exp(e12, e2); + { + term: Seq(e11, e12'), + annotation: { + ids: Semantics.IdTagged.ids(e1), + }, + }; + | Filter(kind, ebody) => + let ebody' = append_exp(ebody, e2); + { + term: Filter(kind, ebody'), + annotation: { + ids: Semantics.IdTagged.ids(e1), + }, + }; + | Let(p, edef, ebody) => + let ebody' = append_exp(ebody, e2); + { + term: Let(p, edef, ebody'), + annotation: { + ids: Semantics.IdTagged.ids(e1), + }, + }; + | TyAlias(tp, tdef, ebody) => + let ebody' = append_exp(ebody, e2); + { + term: TyAlias(tp, tdef, ebody'), + annotation: { + ids: Semantics.IdTagged.ids(e1), + }, + }; + | Use(t, ebody) => + let ebody' = append_exp(ebody, e2); + { + term: Use(t, ebody'), + annotation: { + ids: Semantics.IdTagged.ids(e1), + }, + }; + }; +}; + let stitch3 = (ed1: Editor.t, ed2: Editor.t, ed3: Editor.t) => - EditorUtil.append_exp( - EditorUtil.append_exp(term_of(ed1), term_of(ed2)), - term_of(ed3), - ); + append_exp(append_exp(term_of(ed1), term_of(ed2)), term_of(ed3)); let stitch_term = (eds: p('a)): stitched(TermItem.t) => { let instructor = stitch3(eds.prelude, eds.correct_impl, eds.hidden_tests.tests); let user_impl_term = { let your_impl_term = - eds.your_impl |> term_of |> wrap_filter(FilterAction.Step); + eds.your_impl |> term_of |> wrap_filter(Semantics.FilterAction.Step); let prelude_term = - eds.prelude |> term_of |> wrap_filter(FilterAction.Eval); - EditorUtil.append_exp(prelude_term, your_impl_term); + eds.prelude |> term_of |> wrap_filter(Semantics.FilterAction.Eval); + append_exp(prelude_term, your_impl_term); }; let test_validation_term = stitch3(eds.prelude, eds.correct_impl, eds.your_tests.tests); let user_tests_term = - EditorUtil.append_exp(user_impl_term, term_of(eds.your_tests.tests)); + append_exp(user_impl_term, term_of(eds.your_tests.tests)); let hidden_tests_term = - EditorUtil.append_exp(user_impl_term, term_of(eds.hidden_tests.tests)); + append_exp(user_impl_term, term_of(eds.hidden_tests.tests)); { test_validation: wrap(test_validation_term, eds.your_tests.tests), /* Passing tests term to user_impl so probes in impl reflect tests: */ diff --git a/src/haz3lweb/exercises/Grading.re b/src/haz3lweb/exercises/Grading.re index cb2e789aad..4dc860d4b4 100644 --- a/src/haz3lweb/exercises/Grading.re +++ b/src/haz3lweb/exercises/Grading.re @@ -1,4 +1,4 @@ -open Haz3lcore; +open Semantics; open Util; open Virtual_dom.Vdom; open Node; @@ -187,14 +187,14 @@ module MutationTestingReport = { let mk = ( ~test_validation, - ~hidden_bugs_state: list(wrong_impl(Editor.t)), + ~hidden_bugs_state: list(wrong_impl(Haz3lcore.Editor.t)), ~hidden_bugs, ) : t => { let results = List.map(hidden_bug_status(test_validation), hidden_bugs); let hints = List.map( - (wrong_impl: wrong_impl(Editor.t)) => wrong_impl.hint, + (wrong_impl: wrong_impl(Haz3lcore.Editor.t)) => wrong_impl.hint, hidden_bugs_state, ); let results = List.combine(results, hints); @@ -401,9 +401,9 @@ module SyntaxReport = { percentage, }; - let mk = (~your_impl: Editor.t, ~tests: syntax_tests): t => { + let mk = (~your_impl: Haz3lcore.Editor.t, ~tests: syntax_tests): t => { let user_impl_term = - MakeTerm.from_zip_for_sem(your_impl.state.zipper).term; + Haz3lcore.MakeTerm.from_zip_for_sem(your_impl.state.zipper).term; let predicates = List.map(((_, p)) => SyntaxTest.predicate_fn(p), tests); let hints = List.map(((h, _)) => h, tests); @@ -496,7 +496,7 @@ module ImplGradingReport = { Util.ListUtil.zip_defaults( statuses, hints, - Haz3lcore.TestStatus.Indet, + Semantics.TestStatus.Indet, "No hint available.", ); @@ -504,7 +504,7 @@ module ImplGradingReport = { Util.ListUtil.zip_defaults( [], hints, - Haz3lcore.TestStatus.Indet, + Semantics.TestStatus.Indet, "Exercise configuration error: Hint without a test.", ) }; diff --git a/src/haz3lweb/exercises/SyntaxTest.re b/src/haz3lweb/exercises/SyntaxTest.re index 63f56ec905..7bb7caf314 100644 --- a/src/haz3lweb/exercises/SyntaxTest.re +++ b/src/haz3lweb/exercises/SyntaxTest.re @@ -1,4 +1,4 @@ -open Haz3lcore; +open Semantics; open Util; /* diff --git a/src/haz3lweb/util/Unicode.re b/src/haz3lweb/util/Unicode.re deleted file mode 100644 index 8f02baeb5a..0000000000 --- a/src/haz3lweb/util/Unicode.re +++ /dev/null @@ -1,35 +0,0 @@ -let lam = "λ"; -let up_arrow = "↑"; -let down_arrow = "↓"; -let left_arrow = "←"; -let right_arrow = "→"; -let nbsp = "\xC2\xA0"; -let zwsp = "​"; - -let typeArrowSym = "→"; // U+2192 "Rightwards Arrow" -let castArrowSym = "⇨"; - -let ellipsis = "\xE2\x80\xA6"; - -// copied from hazel -// NOTE: 30% faster than Camomile -let length = (s: string): int => { - let stop = String.length(s); - let rec distance_aux = (start: int, count: int) => - if (start + count >= stop) { - stop - count; - } else { - let n = Char.code(String.unsafe_get(s, start + count)); - if (n < 0x80) { - distance_aux(start + 1, count); - } else if (n < 0xe0) { - distance_aux(start + 1, count + 1); - } else if (n < 0xf0) { - distance_aux(start + 1, count + 2); - } else { - distance_aux(start + 1, count + 3); - }; - }; - - distance_aux(0, 0); -}; diff --git a/src/haz3lweb/util/WorkerServer.re b/src/haz3lweb/util/WorkerServer.re index c03ffaeec4..f2b9982332 100644 --- a/src/haz3lweb/util/WorkerServer.re +++ b/src/haz3lweb/util/WorkerServer.re @@ -5,7 +5,7 @@ type key = string; module Request = { [@deriving (show, sexp, yojson)] - type value = Haz3lcore.Exp.t; + type value = Semantics.Exp.t; [@deriving (show, sexp, yojson)] type t = list((string, value)); @@ -17,8 +17,8 @@ module Response = { [@deriving (show, sexp, yojson)] type value = Result.t( - (Haz3lcore.Exp.t, Haz3lcore.EvaluatorState.t), - Haz3lcore.ProgramResult.error, + (Semantics.Exp.t, Semantics.EvaluatorState.t), + Semantics.ProgramResult.error, ); [@deriving (show, sexp, yojson)] type t = list((string, value)); @@ -28,16 +28,16 @@ module Response = { }; let work = (res: Request.value): Response.value => - switch (Haz3lcore.Evaluator.evaluate(~env=Haz3lcore.Builtins.env_init, res)) { - | exception (Haz3lcore.EvaluatorError.Exception(reason)) => + switch (Semantics.Evaluator.evaluate(~env=Semantics.Builtins.env_init, res)) { + | exception (Semantics.EvaluatorError.Exception(reason)) => print_endline( - "EvaluatorError:" ++ Haz3lcore.EvaluatorError.show(reason), + "EvaluatorError:" ++ Semantics.EvaluatorError.show(reason), ); - Error(Haz3lcore.ProgramResult.EvaulatorError(reason)); + Error(Semantics.ProgramResult.EvaulatorError(reason)); | exception exn => print_endline("EXN:" ++ Printexc.to_string(exn)); Error( - Haz3lcore.ProgramResult.UnknownException(Printexc.to_string(exn)), + Semantics.ProgramResult.UnknownException(Printexc.to_string(exn)), ); | (result, state) => Ok((result, state)) }; diff --git a/src/haz3lweb/view/ContextInspector.re b/src/haz3lweb/view/ContextInspector.re index 24df4919a2..998add155b 100644 --- a/src/haz3lweb/view/ContextInspector.re +++ b/src/haz3lweb/view/ContextInspector.re @@ -6,9 +6,9 @@ let alias_view = (s: string): Node.t => div(~attrs=[clss(["typ-alias-view"])], [text(s)]); let jump_to = entry => - Globals.Update.JumpToTile(Haz3lcore.Ctx.get_id(entry)); + Globals.Update.JumpToTile(Semantics.Ctx.get_id(entry)); -let context_entry_view = (~globals, entry: Haz3lcore.Ctx.entry): Node.t => { +let context_entry_view = (~globals, entry: Semantics.Ctx.entry): Node.t => { let view_type = CodeViewable.view_typ( ~globals, @@ -52,29 +52,29 @@ let context_entry_view = (~globals, entry: Haz3lcore.Ctx.entry): Node.t => { }; }; -let ctx_view = (~globals, ctx: Haz3lcore.Ctx.t): Node.t => +let ctx_view = (~globals, ctx: Semantics.Ctx.t): Node.t => div( ~attrs=[clss(["context-inspector"])], List.map( context_entry_view(~globals), ctx - |> Haz3lcore.Ctx.filter_duplicates - |> Haz3lcore.Ctx.filter_stepper_filter_variables + |> Semantics.Ctx.filter_duplicates + |> Semantics.Ctx.filter_stepper_filter_variables |> (x => x.entries) |> List.rev, ), ); -let ctx_sorts_view = (~globals, ci: Haz3lcore.Statics.Info.t) => - Haz3lcore.Info.ctx_of(ci) - |> Haz3lcore.Ctx.filter_duplicates - |> Haz3lcore.Ctx.filter_stepper_filter_variables +let ctx_sorts_view = (~globals, ci: Semantics.Statics.Info.t) => + Semantics.Info.ctx_of(ci) + |> Semantics.Ctx.filter_duplicates + |> Semantics.Ctx.filter_stepper_filter_variables |> (x => x.entries) |> List.rev |> List.map(context_entry_view(~globals)); let view = - (~globals: Globals.t, ci: option(Haz3lcore.Statics.Info.t)): Node.t => { + (~globals: Globals.t, ci: option(Semantics.Statics.Info.t)): Node.t => { let clss = clss( ["context-inspector"] diff --git a/src/haz3lweb/view/ExerciseMode.re b/src/haz3lweb/view/ExerciseMode.re index 592b31b1b7..6f50cb0199 100644 --- a/src/haz3lweb/view/ExerciseMode.re +++ b/src/haz3lweb/view/ExerciseMode.re @@ -176,7 +176,7 @@ module Update = { List.iter(((pos, result)) => { let pos' = Exercise.pos_of_key(pos); let result': - Haz3lcore.ProgramResult.t(Haz3lcore.ProgramResult.inner) = + Semantics.ProgramResult.t(Semantics.ProgramResult.inner) = switch (result) { | Ok((r, s)) => ResultOk({ @@ -444,7 +444,7 @@ module View = { Some(prelude_trailing_hole_ctx), ) => let specific_ctx = - Haz3lcore.Ctx.subtract_prefix( + Semantics.Ctx.subtract_prefix( correct_impl_trailing_hole_ctx, prelude_trailing_hole_ctx, ); @@ -471,7 +471,7 @@ module View = { editor: { editor: editor.editor.editor, statics: editor.editor.statics, - dynamics: Dynamics.Map.empty, + dynamics: Semantics.Dynamics.Map.empty, }, result: editor.result, }; diff --git a/src/haz3lweb/view/Kind.re b/src/haz3lweb/view/Kind.re index 683dbe8b46..8a600d27ca 100644 --- a/src/haz3lweb/view/Kind.re +++ b/src/haz3lweb/view/Kind.re @@ -2,7 +2,7 @@ open Virtual_dom.Vdom; open Node; open Util.Web; -let view = (~globals, kind: Haz3lcore.Ctx.kind): Node.t => +let view = (~globals, kind: Semantics.Ctx.kind): Node.t => switch (kind) { | Singleton(ty) => div_c( diff --git a/src/haz3lweb/view/NutMenu.re b/src/haz3lweb/view/NutMenu.re index f14e13b040..24cffb0c5a 100644 --- a/src/haz3lweb/view/NutMenu.re +++ b/src/haz3lweb/view/NutMenu.re @@ -2,7 +2,6 @@ open Virtual_dom.Vdom; open Node; open Util.Web; open Widgets; -open Haz3lcore; // COMPONENTS @@ -71,7 +70,12 @@ let values_group = (~globals: Globals.t) => { ("λ", "Functions", s.show_fn_bodies, Evaluation(ShowFnBodies)), ("|", "Cases", s.show_case_clauses, Evaluation(ShowCaseClauses)), ("f", "Fixpoints", s.show_fixpoints, Evaluation(ShowFixpoints)), - (Unicode.castArrowSym, "Casts", s.show_casts, Evaluation(ShowCasts)), + ( + Util.Unicode.castArrowSym, + "Casts", + s.show_casts, + Evaluation(ShowCasts), + ), ], ); }; diff --git a/src/haz3lweb/view/Page.re b/src/haz3lweb/view/Page.re index ae0c7c5671..8db6eba727 100644 --- a/src/haz3lweb/view/Page.re +++ b/src/haz3lweb/view/Page.re @@ -366,13 +366,13 @@ module View = { let str = (cursor.selected_text |> Option.value(~default=() => ""))(); /* Note that we cannot use the ClipboardCache system here unless * we refine it further to replace unique ids on paste */ - Haz3lcore.ClipboardCache.set(cursor.selection, str); + ClipboardCache.set(cursor.selection, str); JsUtil.copy(str); Effect.Ignore; }), Attr.on_cut(_ => { let str = (cursor.selected_text |> Option.value(~default=() => ""))(); - Haz3lcore.ClipboardCache.set(cursor.selection, str); + ClipboardCache.set(cursor.selection, str); JsUtil.copy(str); Option.map( inject, @@ -398,7 +398,7 @@ module View = { Dom.preventDefault(evt); let action = Js.to_string(evt##.clipboardData##getData(Js.string("text"))) - |> Haz3lcore.ClipboardCache.get + |> ClipboardCache.get |> cursor.editor_action; switch (action) { | None => Effect.Ignore diff --git a/src/haz3lweb/view/ScratchMode.re b/src/haz3lweb/view/ScratchMode.re index 6c3074e5fa..e3139778c0 100644 --- a/src/haz3lweb/view/ScratchMode.re +++ b/src/haz3lweb/view/ScratchMode.re @@ -204,11 +204,11 @@ module Update = { UpdateResult( switch (r |> List.hd |> snd) { | Ok((r, s)) => - Haz3lcore.ProgramResult.ResultOk({ + Semantics.ProgramResult.ResultOk({ result: r, state: s, }) - | Error(e) => Haz3lcore.ProgramResult.ResultFail(e) + | Error(e) => Semantics.ProgramResult.ResultFail(e) }, ), ), diff --git a/src/haz3lweb/view/StepperView.re b/src/haz3lweb/view/StepperView.re index caec3b453f..cbf344bfa6 100644 --- a/src/haz3lweb/view/StepperView.re +++ b/src/haz3lweb/view/StepperView.re @@ -1,5 +1,5 @@ open Util; -open Haz3lcore; +open Semantics; open Sexplib.Std; open OptUtil.Syntax; @@ -300,8 +300,7 @@ module Update = { let elab = elab |> ( - settings.evaluation.show_casts - ? x => x : Haz3lcore.DHExp.strip_casts + settings.evaluation.show_casts ? x => x : DHExp.strip_casts ) |> Typ.replace_temp_exp; let editor = CodeWithStatics.Model.mk_from_exp(~settings, elab); diff --git a/src/haz3lweb/view/TestView.re b/src/haz3lweb/view/TestView.re index ecfddcea56..50a5ef16a9 100644 --- a/src/haz3lweb/view/TestView.re +++ b/src/haz3lweb/view/TestView.re @@ -2,9 +2,9 @@ open Virtual_dom.Vdom; open Node; open Util.Web; -module TestStatus = Haz3lcore.TestStatus; -module TestMap = Haz3lcore.TestMap; -module TestResults = Haz3lcore.TestResults; +module TestStatus = Semantics.TestStatus; +module TestMap = Semantics.TestMap; +module TestResults = Semantics.TestResults; let test_bar_segment = (~inject_jump, (id, reports)) => { let status = reports |> TestMap.joint_status |> TestStatus.to_string; diff --git a/src/haz3lcore/lang/Builtins.re b/src/semantics/Builtins.re similarity index 100% rename from src/haz3lcore/lang/Builtins.re rename to src/semantics/Builtins.re diff --git a/src/haz3lcore/prog/CoreSettings.re b/src/semantics/CoreSettings.re similarity index 100% rename from src/haz3lcore/prog/CoreSettings.re rename to src/semantics/CoreSettings.re diff --git a/src/semantics/Id.re b/src/semantics/Id.re new file mode 100644 index 0000000000..cdcf515e83 --- /dev/null +++ b/src/semantics/Id.re @@ -0,0 +1 @@ +include Util.Id; diff --git a/src/semantics/dune b/src/semantics/dune new file mode 100644 index 0000000000..5772eec621 --- /dev/null +++ b/src/semantics/dune @@ -0,0 +1,25 @@ +(include_subdirs unqualified) + +(library + (name semantics) + (libraries util sexplib unionFind uuidm virtual_dom yojson core) + (js_of_ocaml) + (instrumentation + (backend bisect_ppx)) + (preprocess + (pps + ppx_yojson_conv + js_of_ocaml-ppx + ppx_let + ppx_sexp_conv + ppx_enumerate + ppx_deriving.show + ppx_deriving.eq))) + +(env + (dev + (js_of_ocaml + (flags :standard --debuginfo --noinline --dynlink --linkall --sourcemap))) + (release + (js_of_ocaml + (flags :standard)))) diff --git a/src/haz3lcore/dynamics/DHExp.re b/src/semantics/dynamics/DHExp.re similarity index 100% rename from src/haz3lcore/dynamics/DHExp.re rename to src/semantics/dynamics/DHExp.re diff --git a/src/haz3lcore/dynamics/DHPat.re b/src/semantics/dynamics/DHPat.re similarity index 100% rename from src/haz3lcore/dynamics/DHPat.re rename to src/semantics/dynamics/DHPat.re diff --git a/src/haz3lcore/prog/Dynamics.re b/src/semantics/dynamics/Dynamics.re similarity index 100% rename from src/haz3lcore/prog/Dynamics.re rename to src/semantics/dynamics/Dynamics.re diff --git a/src/haz3lcore/dynamics/Evaluator.re b/src/semantics/dynamics/Evaluator.re similarity index 100% rename from src/haz3lcore/dynamics/Evaluator.re rename to src/semantics/dynamics/Evaluator.re diff --git a/src/haz3lcore/dynamics/Evaluator.rei b/src/semantics/dynamics/Evaluator.rei similarity index 100% rename from src/haz3lcore/dynamics/Evaluator.rei rename to src/semantics/dynamics/Evaluator.rei diff --git a/src/haz3lcore/prog/ProgramResult.re b/src/semantics/dynamics/ProgramResult.re similarity index 100% rename from src/haz3lcore/prog/ProgramResult.re rename to src/semantics/dynamics/ProgramResult.re diff --git a/src/haz3lcore/dynamics/Substitution.re b/src/semantics/dynamics/Substitution.re similarity index 100% rename from src/haz3lcore/dynamics/Substitution.re rename to src/semantics/dynamics/Substitution.re diff --git a/src/haz3lcore/dynamics/TypeAssignment.re b/src/semantics/dynamics/TypeAssignment.re similarity index 100% rename from src/haz3lcore/dynamics/TypeAssignment.re rename to src/semantics/dynamics/TypeAssignment.re diff --git a/src/haz3lcore/dynamics/ValueChecker.re b/src/semantics/dynamics/ValueChecker.re similarity index 100% rename from src/haz3lcore/dynamics/ValueChecker.re rename to src/semantics/dynamics/ValueChecker.re diff --git a/src/haz3lcore/dynamics/state/EvaluatorState.re b/src/semantics/dynamics/state/EvaluatorState.re similarity index 100% rename from src/haz3lcore/dynamics/state/EvaluatorState.re rename to src/semantics/dynamics/state/EvaluatorState.re diff --git a/src/haz3lcore/dynamics/state/EvaluatorState.rei b/src/semantics/dynamics/state/EvaluatorState.rei similarity index 100% rename from src/haz3lcore/dynamics/state/EvaluatorState.rei rename to src/semantics/dynamics/state/EvaluatorState.rei diff --git a/src/haz3lcore/dynamics/state/TestMap.re b/src/semantics/dynamics/state/TestMap.re similarity index 100% rename from src/haz3lcore/dynamics/state/TestMap.re rename to src/semantics/dynamics/state/TestMap.re diff --git a/src/haz3lcore/dynamics/state/TestResults.re b/src/semantics/dynamics/state/TestResults.re similarity index 100% rename from src/haz3lcore/dynamics/state/TestResults.re rename to src/semantics/dynamics/state/TestResults.re diff --git a/src/haz3lcore/dynamics/state/TestStatus.re b/src/semantics/dynamics/state/TestStatus.re similarity index 100% rename from src/haz3lcore/dynamics/state/TestStatus.re rename to src/semantics/dynamics/state/TestStatus.re diff --git a/src/haz3lcore/dynamics/stepper/EvalCtx.re b/src/semantics/dynamics/stepper/EvalCtx.re similarity index 100% rename from src/haz3lcore/dynamics/stepper/EvalCtx.re rename to src/semantics/dynamics/stepper/EvalCtx.re diff --git a/src/haz3lcore/dynamics/stepper/EvaluatorStep.re b/src/semantics/dynamics/stepper/EvaluatorStep.re similarity index 100% rename from src/haz3lcore/dynamics/stepper/EvaluatorStep.re rename to src/semantics/dynamics/stepper/EvaluatorStep.re diff --git a/src/haz3lcore/dynamics/stepper/EvaluatorStep.rei b/src/semantics/dynamics/stepper/EvaluatorStep.rei similarity index 100% rename from src/haz3lcore/dynamics/stepper/EvaluatorStep.rei rename to src/semantics/dynamics/stepper/EvaluatorStep.rei diff --git a/src/haz3lcore/dynamics/stepper/FilterMatcher.re b/src/semantics/dynamics/stepper/FilterMatcher.re similarity index 100% rename from src/haz3lcore/dynamics/stepper/FilterMatcher.re rename to src/semantics/dynamics/stepper/FilterMatcher.re diff --git a/src/haz3lcore/dynamics/transition/Casts.re b/src/semantics/dynamics/transition/Casts.re similarity index 100% rename from src/haz3lcore/dynamics/transition/Casts.re rename to src/semantics/dynamics/transition/Casts.re diff --git a/src/haz3lcore/dynamics/transition/EvaluatorError.re b/src/semantics/dynamics/transition/EvaluatorError.re similarity index 100% rename from src/haz3lcore/dynamics/transition/EvaluatorError.re rename to src/semantics/dynamics/transition/EvaluatorError.re diff --git a/src/haz3lcore/dynamics/transition/PatternMatch.re b/src/semantics/dynamics/transition/PatternMatch.re similarity index 100% rename from src/haz3lcore/dynamics/transition/PatternMatch.re rename to src/semantics/dynamics/transition/PatternMatch.re diff --git a/src/haz3lcore/dynamics/transition/Transition.re b/src/semantics/dynamics/transition/Transition.re similarity index 100% rename from src/haz3lcore/dynamics/transition/Transition.re rename to src/semantics/dynamics/transition/Transition.re diff --git a/src/haz3lcore/dynamics/transition/Unboxing.re b/src/semantics/dynamics/transition/Unboxing.re similarity index 100% rename from src/haz3lcore/dynamics/transition/Unboxing.re rename to src/semantics/dynamics/transition/Unboxing.re diff --git a/src/haz3lcore/statics/Binding.re b/src/semantics/statics/Binding.re similarity index 100% rename from src/haz3lcore/statics/Binding.re rename to src/semantics/statics/Binding.re diff --git a/src/haz3lcore/statics/CoCtx.re b/src/semantics/statics/CoCtx.re similarity index 100% rename from src/haz3lcore/statics/CoCtx.re rename to src/semantics/statics/CoCtx.re diff --git a/src/haz3lcore/statics/Constructor.re b/src/semantics/statics/Constructor.re similarity index 100% rename from src/haz3lcore/statics/Constructor.re rename to src/semantics/statics/Constructor.re diff --git a/src/haz3lcore/statics/ConstructorMap.re b/src/semantics/statics/ConstructorMap.re similarity index 100% rename from src/haz3lcore/statics/ConstructorMap.re rename to src/semantics/statics/ConstructorMap.re diff --git a/src/haz3lcore/statics/Coverage.re b/src/semantics/statics/Coverage.re similarity index 100% rename from src/haz3lcore/statics/Coverage.re rename to src/semantics/statics/Coverage.re diff --git a/src/haz3lcore/statics/Ctx.re b/src/semantics/statics/Ctx.re similarity index 96% rename from src/haz3lcore/statics/Ctx.re rename to src/semantics/statics/Ctx.re index 04aaf3023e..a5f07150d3 100644 --- a/src/haz3lcore/statics/Ctx.re +++ b/src/semantics/statics/Ctx.re @@ -241,8 +241,17 @@ let filter_stepper_filter_variables = (ctx: t): t => { |> List.rev, }; +//TODO(andrew): betterize this garbagio +let is_base_typ = (name: string): bool => + name == "Int" + || name == "SInt" + || name == "Float" + || name == "Bool" + || name == "String" + || name == "Nat"; + let shadows_typ = (ctx: t, name: string): bool => - Form.is_base_typ(name) || lookup_tvar(ctx, name) != None; + is_base_typ(name) || lookup_tvar(ctx, name) != None; let empty_pre_elaboration = { use_mode: Some(Operators.default_mode), diff --git a/src/haz3lcore/statics/Elaborator.re b/src/semantics/statics/Elaborator.re similarity index 100% rename from src/haz3lcore/statics/Elaborator.re rename to src/semantics/statics/Elaborator.re diff --git a/src/haz3lcore/statics/Info.re b/src/semantics/statics/Info.re similarity index 99% rename from src/haz3lcore/statics/Info.re rename to src/semantics/statics/Info.re index 8066e4ffd4..b26dd788d5 100644 --- a/src/haz3lcore/statics/Info.re +++ b/src/semantics/statics/Info.re @@ -47,7 +47,7 @@ type error_inconsistent = [@deriving (show({with_path: false}), sexp, yojson, eq)] type error_no_type = /* Invalid expression token, treated as hole */ - | BadToken(Token.t) + | BadToken(string) /* Invalid operator for current use mode, treated as hole */ | BadOperator(string) /* Empty application of function with inconsistent type */ @@ -166,7 +166,7 @@ type typ_expects = possible be reimplemeted via a seperate sort */ [@deriving (show({with_path: false}), sexp, yojson, eq)] type error_typ = - | BadToken(Token.t) /* Invalid token, treated as type hole */ + | BadToken(string) /* Invalid token, treated as type hole */ | FreeTypeVariable(string) /* Free type variable */ | DuplicateConstructor(Constructor.t) /* Duplicate ctr in same sum */ | DuplicateLabels(list(LabeledTuple.label), Typ.t) @@ -658,7 +658,7 @@ let status_tpat = (ctx: Ctx.t, utpat: TPat.t): status_tpat => | EmptyHole => NotInHole(Empty) | Var(name) when Ctx.shadows_typ(ctx, name) => let f = src => InHole(ShadowsType(name, src)); - if (Form.is_base_typ(name)) { + if (Ctx.is_base_typ(name)) { f(BaseTyp); } else if (Ctx.is_alias(ctx, name)) { f(TyAlias); diff --git a/src/haz3lcore/statics/Self.re b/src/semantics/statics/Self.re similarity index 98% rename from src/haz3lcore/statics/Self.re rename to src/semantics/statics/Self.re index 5f17cbdc55..f9eb35c79a 100644 --- a/src/haz3lcore/statics/Self.re +++ b/src/semantics/statics/Self.re @@ -30,7 +30,7 @@ type t = | Just(Typ.t) /* Just a regular type */ | NoJoin(join_type, list(Typ.source)) /* Inconsistent types for e.g match, listlits */ | Duplicate(LabeledTuple.label, t) /* Duplicate label, marked as duplicate */ - | BadToken(Token.t) /* Invalid expression token, continues with undefined behavior */ + | BadToken(string) /* Invalid expression token, continues with undefined behavior */ | BadOperator(string) /* Invalid operator, continues with undefined behavior */ | BadTrivAp(Typ.t) /* Trivial (nullary) ap on function that doesn't take triv */ | BadLabel(Any.t) /* TupLabel label component is not a valid Label*/ diff --git a/src/haz3lcore/statics/Statics.re b/src/semantics/statics/Statics.re similarity index 99% rename from src/haz3lcore/statics/Statics.re rename to src/semantics/statics/Statics.re index d1b6076327..49443c52a8 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/semantics/statics/Statics.re @@ -70,7 +70,7 @@ module Map = { switch (lookup(id, m)) { | Some(InfoExp({co_ctx, ctx, _})) => co_ctx - |> VarMap.to_list + |> Util.VarMap.to_list |> List.map(((n, _)) => Ctx.binding_of(ctx, n)) | _ => [] }; diff --git a/src/haz3lcore/pretty/Abbreviate.re b/src/semantics/term/Abbreviate.re similarity index 100% rename from src/haz3lcore/pretty/Abbreviate.re rename to src/semantics/term/Abbreviate.re diff --git a/src/haz3lcore/lang/term/Any.re b/src/semantics/term/Any.re similarity index 100% rename from src/haz3lcore/lang/term/Any.re rename to src/semantics/term/Any.re diff --git a/src/haz3lcore/lang/Atom.re b/src/semantics/term/Atom.re similarity index 100% rename from src/haz3lcore/lang/Atom.re rename to src/semantics/term/Atom.re diff --git a/src/haz3lcore/lang/term/ClosureEnvironment.re b/src/semantics/term/ClosureEnvironment.re similarity index 100% rename from src/haz3lcore/lang/term/ClosureEnvironment.re rename to src/semantics/term/ClosureEnvironment.re diff --git a/src/haz3lcore/lang/term/Cls.re b/src/semantics/term/Cls.re similarity index 100% rename from src/haz3lcore/lang/term/Cls.re rename to src/semantics/term/Cls.re diff --git a/src/haz3lcore/lang/term/Environment.re b/src/semantics/term/Environment.re similarity index 100% rename from src/haz3lcore/lang/term/Environment.re rename to src/semantics/term/Environment.re diff --git a/src/haz3lcore/lang/term/Exp.re b/src/semantics/term/Exp.re similarity index 100% rename from src/haz3lcore/lang/term/Exp.re rename to src/semantics/term/Exp.re diff --git a/src/haz3lcore/lang/term/FilterAction.re b/src/semantics/term/FilterAction.re similarity index 100% rename from src/haz3lcore/lang/term/FilterAction.re rename to src/semantics/term/FilterAction.re diff --git a/src/haz3lcore/lang/term/FilterEnvironment.re b/src/semantics/term/FilterEnvironment.re similarity index 100% rename from src/haz3lcore/lang/term/FilterEnvironment.re rename to src/semantics/term/FilterEnvironment.re diff --git a/src/haz3lcore/lang/term/Grammar.re b/src/semantics/term/Grammar.re similarity index 100% rename from src/haz3lcore/lang/term/Grammar.re rename to src/semantics/term/Grammar.re diff --git a/src/haz3lcore/lang/term/IdTagged.re b/src/semantics/term/IdTagged.re similarity index 100% rename from src/haz3lcore/lang/term/IdTagged.re rename to src/semantics/term/IdTagged.re diff --git a/src/haz3lcore/lang/term/InvalidOperationError.re b/src/semantics/term/InvalidOperationError.re similarity index 100% rename from src/haz3lcore/lang/term/InvalidOperationError.re rename to src/semantics/term/InvalidOperationError.re diff --git a/src/haz3lcore/LabeledTuple.re b/src/semantics/term/LabeledTuple.re similarity index 100% rename from src/haz3lcore/LabeledTuple.re rename to src/semantics/term/LabeledTuple.re diff --git a/src/haz3lcore/lang/Operators.re b/src/semantics/term/Operators.re similarity index 100% rename from src/haz3lcore/lang/Operators.re rename to src/semantics/term/Operators.re diff --git a/src/haz3lcore/lang/term/Pat.re b/src/semantics/term/Pat.re similarity index 100% rename from src/haz3lcore/lang/term/Pat.re rename to src/semantics/term/Pat.re diff --git a/src/haz3lcore/lang/term/Probe.re b/src/semantics/term/Probe.re similarity index 100% rename from src/haz3lcore/lang/term/Probe.re rename to src/semantics/term/Probe.re diff --git a/src/haz3lcore/lang/term/Rul.re b/src/semantics/term/Rul.re similarity index 100% rename from src/haz3lcore/lang/term/Rul.re rename to src/semantics/term/Rul.re diff --git a/src/semantics/term/Secondary.re b/src/semantics/term/Secondary.re new file mode 100644 index 0000000000..b07085953a --- /dev/null +++ b/src/semantics/term/Secondary.re @@ -0,0 +1,5 @@ +[@deriving (show({with_path: false}), sexp, yojson, enumerate)] +type cls = + | Whitespace + | Comment; +/*TODO(andrew): clarify whether this needs to exist*/ diff --git a/src/semantics/term/Sort.re b/src/semantics/term/Sort.re new file mode 100644 index 0000000000..91aeabc4b6 --- /dev/null +++ b/src/semantics/term/Sort.re @@ -0,0 +1,35 @@ +[@deriving (show({with_path: false}), sexp, yojson)] +type t = + | Any + | Pat + | Typ + | TPat + | Rul + | Exp; + +let root = Exp; + +let consistent = (s, s') => + switch (s, s') { + | (Any, _) + | (_, Any) => true + | _ => s == s' + }; + +let to_string = + fun + | Any => "Any" + | Pat => "Pat" + | TPat => "TPat" + | Typ => "Typ" + | Rul => "Rul" + | Exp => "Exp"; + +let to_string_verbose = + fun + | Any => "any" + | Pat => "pattern" + | TPat => "type pattern" + | Typ => "type" + | Rul => "rule" + | Exp => "expression"; diff --git a/src/haz3lcore/lang/term/TPat.re b/src/semantics/term/TPat.re similarity index 100% rename from src/haz3lcore/lang/term/TPat.re rename to src/semantics/term/TPat.re diff --git a/src/haz3lcore/lang/term/Term.re b/src/semantics/term/Term.re similarity index 100% rename from src/haz3lcore/lang/term/Term.re rename to src/semantics/term/Term.re diff --git a/src/haz3lcore/lang/term/TermBase.re b/src/semantics/term/TermBase.re similarity index 99% rename from src/haz3lcore/lang/term/TermBase.re rename to src/semantics/term/TermBase.re index 272bcf3f1e..1cdcd5bd19 100644 --- a/src/haz3lcore/lang/term/TermBase.re +++ b/src/semantics/term/TermBase.re @@ -929,7 +929,11 @@ and ClosureEnvironment: { let call_stack_of = (t: t) => t.call_stack; let (sexp_of_t, t_of_sexp) = - StructureShareSexp.structure_share_here(id_of, sexp_of_t, t_of_sexp); + Util.StructureShareSexp.structure_share_here( + id_of, + sexp_of_t, + t_of_sexp, + ); }; include Inner; diff --git a/src/haz3lcore/lang/term/Typ.re b/src/semantics/term/Typ.re similarity index 100% rename from src/haz3lcore/lang/term/Typ.re rename to src/semantics/term/Typ.re diff --git a/src/haz3lcore/lang/term/Var.re b/src/semantics/term/Var.re similarity index 100% rename from src/haz3lcore/lang/term/Var.re rename to src/semantics/term/Var.re diff --git a/src/haz3lcore/lang/term/VarBstMap.re b/src/semantics/term/VarBstMap.re similarity index 100% rename from src/haz3lcore/lang/term/VarBstMap.re rename to src/semantics/term/VarBstMap.re diff --git a/src/haz3lcore/lang/term/VarBstMap.rei b/src/semantics/term/VarBstMap.rei similarity index 100% rename from src/haz3lcore/lang/term/VarBstMap.rei rename to src/semantics/term/VarBstMap.rei diff --git a/src/haz3lcore/tiles/Id.re b/src/util/Id.re similarity index 95% rename from src/haz3lcore/tiles/Id.re rename to src/util/Id.re index e2bad89353..2f38eea1c6 100644 --- a/src/haz3lcore/tiles/Id.re +++ b/src/util/Id.re @@ -1,4 +1,4 @@ -open Util; +open Ppx_yojson_conv_lib.Yojson_conv; /* ID FAQ @@ -42,7 +42,7 @@ let t_of_sexp: Sexplib.Sexp.t => Uuidm.t = fun | Sexplib.Sexp.Atom(s) => Uuidm.of_string(s) - |> Util.OptUtil.get(_ => failwith("Uuidm.t_of_sexp: not valid UUID (1)")) + |> OptUtil.get(_ => failwith("Uuidm.t_of_sexp: not valid UUID (1)")) | _ => failwith("Uuidm.t_of_sexp: not valid UUID (2)"); let yojson_of_t: Uuidm.t => Yojson.Safe.t = t => `String(Uuidm.to_string(t)); @@ -51,9 +51,7 @@ let t_of_yojson: Yojson.Safe.t => Uuidm.t = fun | `String(s) => Uuidm.of_string(s) - |> Util.OptUtil.get(_ => - failwith("Uuidm.t_of_yojson: not valid UUID (1)") - ) + |> OptUtil.get(_ => failwith("Uuidm.t_of_yojson: not valid UUID (1)")) | _ => failwith("Uuidm.t_of_yojson: not valid UUID (2)"); [@deriving eq] @@ -62,7 +60,7 @@ type t = Uuidm.t; let mk: unit => t = Uuidm.v4_gen(Random.State.make_self_init()); let namespace_uuid = Uuidm.of_string("6ba7b810-9dad-11d1-80b4-00c04fd430c8") - |> Util.OptUtil.get(_ => failwith("Invalid namespace UUID")); + |> OptUtil.get(_ => failwith("Invalid namespace UUID")); let next: t => t = x => Uuidm.v5(namespace_uuid, Uuidm.to_string(x)); let compare: (t, t) => int = Uuidm.compare; diff --git a/src/haz3lcore/StructureShareSexp.re b/src/util/StructureShareSexp.re similarity index 100% rename from src/haz3lcore/StructureShareSexp.re rename to src/util/StructureShareSexp.re diff --git a/src/haz3lcore/Unicode.re b/src/util/Unicode.re similarity index 100% rename from src/haz3lcore/Unicode.re rename to src/util/Unicode.re diff --git a/src/util/Util.re b/src/util/Util.re index dd9df4972d..437ee039db 100644 --- a/src/util/Util.re +++ b/src/util/Util.re @@ -24,6 +24,10 @@ module Point = Point; module Calc = Calc; module Sets = Sets; module Maps = Maps; +module Id = Id; +module Unicode = Unicode; +module StructureShareSexp = StructureShareSexp; +module VarMap = VarMap; // Used by [@deriving sexp, yojson)] include Sexplib.Std; diff --git a/src/haz3lcore/VarMap.re b/src/util/VarMap.re similarity index 89% rename from src/haz3lcore/VarMap.re rename to src/util/VarMap.re index dbee5045bb..3d8a8ed114 100644 --- a/src/haz3lcore/VarMap.re +++ b/src/util/VarMap.re @@ -1,7 +1,8 @@ -open Util; +open Sexplib.Std; +open Ppx_yojson_conv_lib.Yojson_conv; [@deriving (show({with_path: false}), sexp, yojson)] -type t_('a) = list((Token.t, 'a)); +type t_('a) = list((string, 'a)); let empty = []; diff --git a/src/util/dune b/src/util/dune index b8d31ccf2a..ad3cb81672 100644 --- a/src/util/dune +++ b/src/util/dune @@ -1,6 +1,16 @@ (library (name util) - (libraries re base ptmap bonsai bonsai.web virtual_dom yojson bignum) + (libraries + re + base + ptmap + bonsai + bonsai.web + virtual_dom + yojson + bignum + uuidm + unionFind) (js_of_ocaml) (instrumentation (backend bisect_ppx)) @@ -11,6 +21,7 @@ ppx_let ppx_sexp_conv ppx_deriving.show + ppx_deriving.eq bonsai.ppx_bonsai))) (env diff --git a/test/Test_Coverage.re b/test/Test_Coverage.re index a8c904a44a..b8d72e9e0e 100644 --- a/test/Test_Coverage.re +++ b/test/Test_Coverage.re @@ -1,5 +1,5 @@ open Alcotest; -open Haz3lcore; +open Semantics; let testable_error_map = testable( diff --git a/test/Test_Elaboration.re b/test/Test_Elaboration.re index 8a7cb71219..af0b724c07 100644 --- a/test/Test_Elaboration.re +++ b/test/Test_Elaboration.re @@ -1,5 +1,5 @@ open Alcotest; -open Haz3lcore; +open Semantics; /*Create a testable type for dhexp which requires an equal function (dhexp_eq) and a print function (dhexp_print) */ @@ -12,7 +12,7 @@ let mk_map = Statics.mk(CoreSettings.on, Builtins.ctx_init(Some(Int))); let dhexp_of_uexp = u => Elaborator.elaborate(mk_map(u), u) |> fst; let alco_check = dhexp_typ |> Alcotest.check; let parse_exp = (s: string) => { - switch (MakeTerm.parse_exp(s)) { + switch (Haz3lcore.MakeTerm.parse_exp(s)) { | Some(e) => e | None => Alcotest.fail("Failed to parse expression: " ++ s) }; diff --git a/test/Test_Evaluator.re b/test/Test_Evaluator.re index b75758a33f..d1877c2918 100644 --- a/test/Test_Evaluator.re +++ b/test/Test_Evaluator.re @@ -1,5 +1,5 @@ open Alcotest; -open Haz3lcore; +open Semantics; let dhexp_typ = testable(Fmt.using(Exp.show, Fmt.string), DHExp.fast_equal); let evaluation_test = (msg, expected, unevaluated) => @@ -17,7 +17,7 @@ let evaluate_probes = unevaluated => |> EvaluatorState.get_probes; let parse_exp = (s: string) => { - switch (MakeTerm.parse_exp(s)) { + switch (Haz3lcore.MakeTerm.parse_exp(s)) { | Some(e) => e | None => Alcotest.fail("Failed to parse expression: " ++ s) }; diff --git a/test/Test_ExpToSegment.re b/test/Test_ExpToSegment.re index 1565def3ad..8d4797a499 100644 --- a/test/Test_ExpToSegment.re +++ b/test/Test_ExpToSegment.re @@ -1,5 +1,6 @@ open Alcotest; open Haz3lcore; +open Semantics; open Base; // Id ignoring equality for tiles diff --git a/test/Test_Grammar.re b/test/Test_Grammar.re index 43a5cb418a..25e91c2e9a 100644 --- a/test/Test_Grammar.re +++ b/test/Test_Grammar.re @@ -1,4 +1,4 @@ -open Haz3lcore; +open Semantics; open Alcotest; let qcheck_map_annotation_test = QCheck.Test.make( diff --git a/test/Test_Introduce.re b/test/Test_Introduce.re index 66901f9300..6627970995 100644 --- a/test/Test_Introduce.re +++ b/test/Test_Introduce.re @@ -1,4 +1,4 @@ -open Haz3lcore; +open Semantics; open Alcotest; let exp = testable(Fmt.using(DHExp.show, Fmt.string), DHExp.fast_equal); @@ -31,6 +31,7 @@ let introduction_test = (before: string, expected: string) => { open Util.OptUtil.Syntax; let serialized = { + open Haz3lcore; let* zip = Printer.zipper_of_string(before); let exp = MakeTerm.from_zip_for_sem(zip).term; let* hole_id = find_hole_id(exp); @@ -55,7 +56,8 @@ let introduction_test = (before: string, expected: string) => { }; let introduce_expression = (x: Typ.t): option(Exp.t) => - Introduce.IntroduceExp.introduce(x) |> Option.map(((a, _b, _c)) => a); + Haz3lcore.Introduce.IntroduceExp.introduce(x) + |> Option.map(((a, _b, _c)) => a); let tests = IdTagged.FreshGrammar.[ diff --git a/test/Test_LabeledTuple.re b/test/Test_LabeledTuple.re index 8b6a0de5cc..6e6c2a6f90 100644 --- a/test/Test_LabeledTuple.re +++ b/test/Test_LabeledTuple.re @@ -1,5 +1,5 @@ open Alcotest; -open Haz3lcore; +open Semantics; let test_rearrange = (name, analyzed_types, actual_values, expected_values) => test_case( diff --git a/test/Test_MakeTerm.re b/test/Test_MakeTerm.re index f32510180f..291fdaa4d3 100644 --- a/test/Test_MakeTerm.re +++ b/test/Test_MakeTerm.re @@ -4,8 +4,12 @@ */ open Alcotest; open Haz3lcore; -module Fresh = IdTagged.FreshGrammar; -let exp_typ = testable(Fmt.using(Exp.show, Fmt.string), Exp.fast_equal); +module Fresh = Semantics.IdTagged.FreshGrammar; +let exp_typ = + testable( + Fmt.using(Semantics.Exp.show, Fmt.string), + Semantics.Exp.fast_equal, + ); let parse_exp = (s: string) => { switch (MakeTerm.parse_exp(s)) { diff --git a/test/Test_Menhir.re b/test/Test_Menhir.re index a388ea926d..4e01ebaff5 100644 --- a/test/Test_Menhir.re +++ b/test/Test_Menhir.re @@ -1,12 +1,9 @@ open Haz3lmenhir; open Alcotest; -open Haz3lcore; +open Semantics; module Fresh = IdTagged.FreshGrammar; let alco_check = - testable( - Fmt.using(Haz3lcore.Exp.show, Fmt.string), - Haz3lcore.DHExp.fast_equal, - ) + (testable(Fmt.using(Exp.show, Fmt.string)))(DHExp.fast_equal) |> Alcotest.check; let strip_Wrap_and_add_builtins = @@ -17,8 +14,7 @@ let strip_Wrap_and_add_builtins = | Parens(e) | Probe(e, _) => cont(e) | Var(x) => - let builtin = - VarMap.lookup(Haz3lcore.Builtins.Pervasives.builtins, x); + let builtin = Util.VarMap.lookup(Builtins.Pervasives.builtins, x); cont( switch (builtin) { | Some(Fn(_, _, _)) => cont(Fresh.Exp.builtin_fun(x)) @@ -47,7 +43,10 @@ let strip_Wrap_and_add_builtins = // Existing recovering parser let make_term_parse = (s: string) => strip_Wrap_and_add_builtins( - MakeTerm.from_zip_for_sem(Option.get(Printer.zipper_of_string(s))).term, + Haz3lcore.MakeTerm.from_zip_for_sem( + Option.get(Haz3lcore.Printer.zipper_of_string(s)), + ). + term, ); let menhir_matches = (exp: Term.Exp.t, actual: string) => @@ -118,20 +117,24 @@ let qcheck_menhir_maketerm_equivalent_test = Grammar.map_exp_annotation(_ => IdTagged.IdTag.fresh(), unit_exp); let segment = - ExpToSegment.exp_to_segment( + Haz3lcore.ExpToSegment.exp_to_segment( ~settings= - ExpToSegment.Settings.of_core(~inline=true, CoreSettings.off), + Haz3lcore.ExpToSegment.Settings.of_core( + ~inline=true, + Semantics.CoreSettings.off, + ), core_exp, ); - let serialized = Printer.of_segment(~holes=Some("?"), segment); + let serialized = + Haz3lcore.Printer.of_segment(~holes=Some("?"), segment); let make_term_parsed = make_term_parse(serialized); let menhir_parsed = Haz3lmenhir.Interface.parse_program(serialized); let menhir_parsed_converted = Haz3lmenhir.Conversion.Exp.of_menhir_ast(menhir_parsed); switch ( - Haz3lcore.DHExp.fast_equal( + DHExp.fast_equal( make_term_parsed, Grammar.map_exp_annotation( _ => IdTagged.IdTag.fresh(), @@ -175,7 +178,7 @@ let qcheck_menhir_serialized_equivalent_test = let core_exp = Grammar.map_exp_annotation(_ => IdTagged.IdTag.fresh(), unit_exp); let segment = - ExpToSegment.exp_to_segment( + Haz3lcore.ExpToSegment.exp_to_segment( ~settings={ inline: true, fold_case_clauses: false, @@ -187,7 +190,8 @@ let qcheck_menhir_serialized_equivalent_test = }, core_exp, ); - let serialized = Printer.of_segment(~holes=Some("?"), segment); + let serialized = + Haz3lcore.Printer.of_segment(~holes=Some("?"), segment); let menhir_parsed = Haz3lmenhir.Interface.parse_program(serialized); AST.equal_exp(menhir_parsed, exp); }, diff --git a/test/Test_Statics.re b/test/Test_Statics.re index 175c6b57d7..069c7b4b02 100644 --- a/test/Test_Statics.re +++ b/test/Test_Statics.re @@ -1,5 +1,5 @@ open Alcotest; -open Haz3lcore; +open Semantics; let testable_typ = testable(Fmt.using(Typ.show, Fmt.string), Typ.fast_equal); @@ -52,7 +52,7 @@ let testable_error: testable(Info.error) = let statics = Statics.mk(CoreSettings.on, Builtins.ctx_init(Some(Int))); let parse_exp = (s: string) => { - switch (MakeTerm.parse_exp(s)) { + switch (Haz3lcore.MakeTerm.parse_exp(s)) { | Some(e) => e | None => Alcotest.fail("Failed to parse expression: " ++ s) }; diff --git a/test/Test_Typ.re b/test/Test_Typ.re index 18eab74eb2..dec9c2270c 100644 --- a/test/Test_Typ.re +++ b/test/Test_Typ.re @@ -1,5 +1,5 @@ open Alcotest; -open Haz3lcore; +open Semantics; let tests = ( "Typ", diff --git a/test/Test_Unboxing.re b/test/Test_Unboxing.re index bedc8c52a3..37eb90abce 100644 --- a/test/Test_Unboxing.re +++ b/test/Test_Unboxing.re @@ -1,5 +1,5 @@ open Alcotest; -open Haz3lcore; +open Semantics; let unboxed_testable = (inner_testable: testable('a)) => testable( From 30f562d1c7eb7fae9e8c8f8ffdc30b9101d7a6fb Mon Sep 17 00:00:00 2001 From: disconcision Date: Thu, 17 Apr 2025 23:06:38 -0400 Subject: [PATCH 2/2] rm unused/redundant build libs --- src/haz3lcore/dune | 2 +- src/haz3lmenhir/dune | 10 ++-------- src/haz3lweb/dune | 18 ++---------------- src/pretty/Box.re | 2 -- src/pretty/Doc.re | 2 -- src/pretty/Layout.re | 2 -- src/pretty/MeasuredLayout.re | 2 -- src/pretty/MeasuredPosition.re | 2 -- src/pretty/dune | 5 +---- src/semantics/dune | 4 +--- src/util/dune | 12 +----------- test/dune | 20 ++------------------ 12 files changed, 10 insertions(+), 71 deletions(-) diff --git a/src/haz3lcore/dune b/src/haz3lcore/dune index 7cdea56366..6af608c283 100644 --- a/src/haz3lcore/dune +++ b/src/haz3lcore/dune @@ -2,7 +2,7 @@ (library (name haz3lcore) - (libraries semantics util sexplib unionFind uuidm virtual_dom yojson core) + (libraries semantics) (js_of_ocaml) (instrumentation (backend bisect_ppx)) diff --git a/src/haz3lmenhir/dune b/src/haz3lmenhir/dune index 97f7436887..d6e0fd9656 100644 --- a/src/haz3lmenhir/dune +++ b/src/haz3lmenhir/dune @@ -1,17 +1,11 @@ (library (name haz3lmenhir) - (libraries util re sexplib unionFind semantics qcheck-alcotest) + (libraries semantics qcheck-alcotest) (modules AST Conversion Interface Lexer Parser) (instrumentation (backend bisect_ppx)) (preprocess - (pps - ppx_let - ppx_sexp_conv - ppx_deriving.show - ppx_deriving.eq - ppx_yojson_conv - ppx_deriving_qcheck))) + (pps ppx_sexp_conv ppx_deriving.show ppx_deriving.eq ppx_deriving_qcheck))) (ocamllex Lexer) diff --git a/src/haz3lweb/dune b/src/haz3lweb/dune index 616712dd3c..2336f90689 100644 --- a/src/haz3lweb/dune +++ b/src/haz3lweb/dune @@ -10,24 +10,10 @@ (modules WorkerServer) (instrumentation (backend bisect_ppx)) - (libraries - str - bonsai - bonsai.web - virtual_dom.input_widgets - util - ppx_yojson_conv.expander - haz3lcore - pretty - omd) + (libraries semantics) (js_of_ocaml) (preprocess - (pps - ppx_yojson_conv - js_of_ocaml-ppx - ppx_let - ppx_sexp_conv - ppx_deriving.show))) + (pps ppx_yojson_conv ppx_sexp_conv ppx_deriving.show))) (library (name haz3lweb) diff --git a/src/pretty/Box.re b/src/pretty/Box.re index 2ac8129bd0..88b1ce0473 100644 --- a/src/pretty/Box.re +++ b/src/pretty/Box.re @@ -1,5 +1,3 @@ -open Util; - [@deriving sexp] type t('annot) = | Text(string) diff --git a/src/pretty/Doc.re b/src/pretty/Doc.re index ede6ffd420..724461bb2c 100644 --- a/src/pretty/Doc.re +++ b/src/pretty/Doc.re @@ -1,5 +1,3 @@ -open Util; - module WidthPosKey = { type t = (int, int); let hash = ((width, pos)) => 256 * 256 * width + pos; diff --git a/src/pretty/Layout.re b/src/pretty/Layout.re index f362db84c9..acc9d3fb85 100644 --- a/src/pretty/Layout.re +++ b/src/pretty/Layout.re @@ -1,5 +1,3 @@ -open Util; - // TODO: rename Annot to Ann? [@deriving sexp] type t('annot) = diff --git a/src/pretty/MeasuredLayout.re b/src/pretty/MeasuredLayout.re index cf1db89e51..c919087a28 100644 --- a/src/pretty/MeasuredLayout.re +++ b/src/pretty/MeasuredLayout.re @@ -1,5 +1,3 @@ -open Util; - [@deriving sexp] type box = { height: int, diff --git a/src/pretty/MeasuredPosition.re b/src/pretty/MeasuredPosition.re index 221e7da9d8..af6ddc5ff6 100644 --- a/src/pretty/MeasuredPosition.re +++ b/src/pretty/MeasuredPosition.re @@ -1,5 +1,3 @@ -open Util; - [@deriving sexp] type t = { row: int, diff --git a/src/pretty/dune b/src/pretty/dune index c131965aff..d9b2f0b3aa 100644 --- a/src/pretty/dune +++ b/src/pretty/dune @@ -2,11 +2,8 @@ (library (name pretty) - (libraries util sexplib) (instrumentation - (backend bisect_ppx)) - (preprocess - (pps ppx_let ppx_sexp_conv))) + (backend bisect_ppx))) (env (dev diff --git a/src/semantics/dune b/src/semantics/dune index 5772eec621..af7d74f3d3 100644 --- a/src/semantics/dune +++ b/src/semantics/dune @@ -2,15 +2,13 @@ (library (name semantics) - (libraries util sexplib unionFind uuidm virtual_dom yojson core) + (libraries util) (js_of_ocaml) (instrumentation (backend bisect_ppx)) (preprocess (pps ppx_yojson_conv - js_of_ocaml-ppx - ppx_let ppx_sexp_conv ppx_enumerate ppx_deriving.show diff --git a/src/util/dune b/src/util/dune index ad3cb81672..9492b67169 100644 --- a/src/util/dune +++ b/src/util/dune @@ -1,16 +1,6 @@ (library (name util) - (libraries - re - base - ptmap - bonsai - bonsai.web - virtual_dom - yojson - bignum - uuidm - unionFind) + (libraries ptmap bonsai.web bignum uuidm unionFind) (js_of_ocaml) (instrumentation (backend bisect_ppx)) diff --git a/test/dune b/test/dune index e16add0dc2..98c0ea0abe 100644 --- a/test/dune +++ b/test/dune @@ -2,23 +2,7 @@ (test (name haz3ltest) - (libraries - haz3lcore - haz3lweb - alcotest - sexplib - base - ptmap - incr_dom - haz3lmenhir - junit - junit_alcotest - bisect_ppx.runtime) + (libraries haz3lweb haz3lmenhir junit_alcotest bisect_ppx.runtime) (modes js) (preprocess - (pps - js_of_ocaml-ppx - ppx_let - ppx_sexp_conv - ppx_deriving.show - ppx_yojson_conv))) + (pps ppx_deriving.show)))