Dynamic typing feedback into static marking

src/haz3lcore/derived/CachedStatics.re

@@ -7,6 +7,8 @@ type t = {
   elaborated: Exp.t,
   info_map: Statics.Map.t,
   error_ids: list(Id.t),
+  dynamic_info_map: Statics.Map.t,
+  dynamic_error_ids: list(Id.t),
 };
 
 let empty: t = {
@@ -24,6 +26,8 @@ let empty: t = {
   },
   info_map: Id.Map.empty,
   error_ids: [],
+  dynamic_info_map: Id.Map.empty,
+  dynamic_error_ids: [],
 };
 
 let elaborate =
@@ -49,7 +53,7 @@ let init_from_term = (~settings, ~is_dynamic_term, ~ctx=?, ~ana=?, term): t => {
     | _ when !settings.dynamics && !settings.elaborate =>
       dh_err("Dynamics & Elaboration disabled")
     | _ =>
-      switch (elaborate(false, info_map, term)) {
+      switch (elaborate(settings.dynamic_feedback, info_map, term)) {
       | DoesNotElaborate => dh_err("Elaboration returns None")
       | Elaborates(d, _) => d
       }
@@ -59,6 +63,8 @@ let init_from_term = (~settings, ~is_dynamic_term, ~ctx=?, ~ana=?, term): t => {
     elaborated,
     info_map,
     error_ids,
+    dynamic_info_map: Statics.Map.empty,
+    dynamic_error_ids: [],
   };
 };
 

src/haz3lcore/projectors/implementations/ProbeProj.re

@@ -121,7 +121,11 @@ let hide_env = (info: info): bool =>
 let cur_ap = (info: info) =>
   switch (info.statics) {
   | Some(InfoExp({term: {term: Ap(_), _} as ap, _}))
-  | Some(InfoExp({term: {term: Probe({term: Ap(_), _} as ap, _), _}, _})) =>
+  | Some(InfoExp({term: {term: Probe({term: Ap(_), _} as ap, _), _}, _}))
+  | Some(InfoExp({term: {term: TypAp(_), _} as ap, _}))
+  | Some(
+      InfoExp({term: {term: Probe({term: TypAp(_), _} as ap, _), _}, _}),
+    ) =>
     Some(Exp.rep_id(ap))
   | _ => None
   };
@@ -147,6 +151,8 @@ module DynCursor = {
     s.pinned_call = None;
   };
 
+  let get_pinned_call = () => s.pinned_call;
+
   let capture_cursor = (closure: closure): unit => {
     s.call_cursor = closure.call_stack;
   };

src/haz3lcore/zipper/action/Introduce.re

@@ -94,7 +94,7 @@ module IntroduceExp: Introducable with type t = Exp.t = {
         | Arrow(_, _) =>
           let cursor_pat = Pat.empty_hole();
           Some((
-            fn(cursor_pat, empty_hole(), None, None),
+            fn(cursor_pat, empty_hole()),
             List.hd(cursor_pat.annotation.ids),
             false,
           ));

src/language/CoreSettings.re

@@ -36,6 +36,7 @@ type t = {
   elaborate: bool,
   assist: bool,
   dynamics: bool,
+  dynamic_feedback: bool,
   flip_animations: bool,
   evaluation: Evaluation.t,
 };
@@ -45,6 +46,7 @@ let off: t = {
   elaborate: false,
   assist: false,
   dynamics: false,
+  dynamic_feedback: false,
   flip_animations: false,
   evaluation: Evaluation.init,
 };
@@ -54,6 +56,7 @@ let on: t = {
   elaborate: true,
   assist: true,
   dynamics: true,
+  dynamic_feedback: true,
   flip_animations: true,
   evaluation: Evaluation.init,
 };

src/language/builtins/BuiltinsADT.re

@@ -88,8 +88,7 @@ module Option = {
                     ),
                   ],
                 ),
-                None,
-                Some("option_map+"),
+                ~name="option_map+",
               ),
               None,
             )
@@ -122,8 +121,7 @@ module Option = {
                     ),
                   ],
                 ),
-                None,
-                Some("option_bind+"),
+                ~name="option_bind+",
               ),
               None,
             )
@@ -156,8 +154,7 @@ module Option = {
                     ),
                   ],
                 ),
-                None,
-                Some("option_to_list+"),
+                ~name="option_to_list+",
               ),
               None,
             )