fix the handling of external_action to enable proper inference of loc…

…_index

src/3d/Target.fst

@@ -486,7 +486,7 @@ let rec print_action (mname:string) (a:action) : ML string =
       | Action_assignment lhs rhs ->
         Printf.sprintf "(action_assignment %s %s)" (print_ident lhs) (print_expr mname rhs)
       | Action_call f args ->
-        Printf.sprintf "(mk_external_action (%s %s))" (print_ident f) (String.concat " " (List.map (print_expr mname) args))
+        Printf.sprintf "(mk_extern_action (%s %s))" (print_ident f) (String.concat " " (List.map (print_expr mname) args))
   in
   match a with
   | Atomic_action a ->
@@ -1116,7 +1116,7 @@ let print_out_expr_set_fstar (tbl:set) (mname:string) (oe:output_expr) : ML stri
           (Some?.v oe.oe_bitwidth)
       end in
     Printf.sprintf
-        "\n\nval %s (_:%s) (_:%s) : external_action output_loc\n\n"
+        "\n\nval %s (_:%s) (_:%s) : extern_action (NonTrivial output_loc)\n\n"
         fn_name
         fn_arg1_t
         fn_arg2_t
@@ -1234,7 +1234,7 @@ let print_external_api_fstar_interpreter (modul:string) (ds:decls) : ML string =
     | Extern_type i ->
       Printf.sprintf "\n\nval %s : Type0\n\n" (print_ident i)
     | Extern_fn f ret params ->
-      Printf.sprintf "\n\nval %s %s : external_action output_loc\n"
+      Printf.sprintf "\n\nval %s %s : extern_action (NonTrivial output_loc)\n"
         (print_ident f)
         (String.concat " " (params |> List.map (fun (i, t) -> Printf.sprintf "(%s:%s)"
           (print_ident i)
@@ -1252,6 +1252,7 @@ let print_external_api_fstar_interpreter (modul:string) (ds:decls) : ML string =
     "module %s.ExternalAPI\n\n\
      open EverParse3d.Prelude\n\
      open EverParse3d.Actions.All\n\
+     open EverParse3d.Interpreter\n\
      %s\n\
      noextract val output_loc : eloc\n\n%s"
     modul

src/3d/prelude/EverParse3d.Interpreter.fst

@@ -475,7 +475,7 @@ let dtyp_as_leaf_reader #nz (#pk:P.parser_kind nz P.WeakKindStrongPrefix)
       let (| _, lr |) = get_leaf_reader b in
       lr
 
-(** Now we define the AST of 3D programs *)
+(** Actions *)
 
 let action_binding
       (inv:inv_index)
@@ -485,12 +485,19 @@ let action_binding
   : Type u#0
   = A.action (interp_inv inv) A.disjointness_trivial (interp_loc l) on_success a
 
+inline_for_extraction
+let extern_action (l:loc_index) = A.external_action (interp_loc l)
+
+inline_for_extraction
+let mk_extern_action (#l:loc_index) ($f:extern_action l)
+  = A.mk_external_action f
+
 [@@specialize]
 let mk_action_binding
     (#l:loc_index)
-    ($f:A.external_action (interp_loc l))
+    ($f:extern_action l)
   : action_binding inv_none l false unit
-  = A.mk_external_action f
+  = mk_extern_action f
 
 (* The type of atomic actions.
 
@@ -545,7 +552,7 @@ type atomic_action
       squash (EverParse3d.Actions.BackendFlag.backend_flag == A.BackendFlagExtern) ->
       sz: FStar.UInt64.t ->
       #out_loc:loc_index ->
-      write_to: (A.___PUINT8 -> Tot (A.external_action (interp_loc out_loc))) ->
+      write_to: (A.___PUINT8 -> Tot (extern_action out_loc)) ->
       atomic_action inv_none disj_none out_loc false bool
 
   | Action_deref: