Add explicit ML effect annotations for --MLish removal

With the removal of --MLish from F*, functions that call effectful
operations must now have explicit ML return type annotations. The
--MLish flag previously made ML the default effect for all unannotated
top-level let bindings; without it, the default is Tot.

Changes by file:

src/syntax_extension/PulseSyntaxExtension.Sugar.fst:
  - Added 'open FStarC.Effect' and 'open FStarC.Class.Deq'
  - eq_ident, eq_lident: added ': ML bool' (=? operator is ML)
  - forall2: changed parameter type to 'f:'a -> 'a -> ML bool'
  - eq_opt, eq_slprop, eq_while_invariant1: added ': ML bool'
  - Entire eq_decl mutual recursion block (eq_decl, eq_fn_decl,
    eq_fn_defn, eq_slprop_defn, eq_ascription, eq_computation_type,
    eq_annot, eq_body, eq_stmt, eq_stmt', eq_let_init, eq_array_init,
    eq_hint_type, eq_ensures_slprop, eq_lambda): added ': ML bool'
  - stmt_to_string, branch_to_string: added ': ML string'

src/syntax_extension/PulseSyntaxExtension.Err.fst:
  - err type: nat -> ML (...) instead of nat -> Tot (...)
  - bind_err, map_err_opt: added ML annotations

src/syntax_extension/PulseSyntaxExtension.Desugar.fst:
  - All desugar_* functions: added ': ML (err ...)' annotations
  - as_qual: added ML annotation
  - desugar_decl: moved out of mutual recursion group (it calls
    but is not called by the other mutually recursive functions)
  - Helper functions (close_st_term_bvs, close_comp_bvs,
    fold_right1, sugar_app, sugar_var, etc.): added ML annotations

src/syntax_extension/PulseSyntaxExtension.ASTBuilder.fst:
  - Functions calling mk/mk_term/show: added ML annotations

src/syntax_extension/PulseSyntaxExtension.Env.fst:
  - Functions using refs and show: added ML annotations

src/syntax_extension/PulseSyntaxExtension.Printing.fst:
  - Printing functions using show: added ML annotations

src/extraction/ExtractPulse.fst:
  - lookup_goto: added ': ML' (dereferences goto_env ref)

src/extraction/ExtractPulseC.fst:
  - char_of_typechar, string_of_typestring, go: added ML annotations
  - Functions calling FStarC.String operations: added ML annotations

src/extraction/ExtractPulseOCaml.fst:
  - hua, tr_typ: added ': ML' annotations

Build verified: clean build passes with no errors.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Author: nikswamy

src/extraction/ExtractPulse.fst

@@ -74,7 +74,7 @@ let with_goto_env_update #a (f: goto_env_t -> goto_env_t) (k: unit -> ML a) : ML
 let with_goto_env_elem #a (id: mlident) (e: goto_env_elem) (k: unit -> ML a) : ML a =
   with_goto_env_update (Cons (id, e)) k
 
-let lookup_goto (id: mlident) : option goto_env_elem =
+let lookup_goto (id: mlident) : ML (option goto_env_elem) =
   let rec go (env: goto_env_t) =
     match env with
     | [] -> None

src/extraction/ExtractPulseC.fst

@@ -14,10 +14,10 @@ open FStarC.Extraction.Krml
 module BU = FStarC.Util
 
 (* JL: TODO: in stdlib somewhere? *)
-let opt_bind (m: option 'a) (k: 'a -> option 'b): option 'b =
+let opt_bind (m: option 'a) (k: 'a -> ML (option 'b)): ML (option 'b) =
   match m with Some x -> k x | None -> None
 
-let char_of_typechar (t: mlty): option char =
+let char_of_typechar (t: mlty): ML (option char) =
   match t with
   | MLTY_Named ([], p) ->
     let p = Syntax.string_of_mlpath p in
@@ -30,8 +30,8 @@ let char_of_typechar (t: mlty): option char =
 
   | _ -> None
 
-let string_of_typestring (t: mlty): option string =
-  let rec go t: option (list string) =
+let string_of_typestring (t: mlty): ML (option string) =
+  let rec go t: ML (option (list string)) =
     match t with
     | MLTY_Named ([], p)
       when Syntax.string_of_mlpath p = "Pulse.C.Typestring.string_nil"
@@ -49,9 +49,9 @@ let string_of_typestring (t: mlty): option string =
   in
   opt_bind (go t) (fun ss -> Some (FStar.String.concat "" ss))
 
-let lident_of_string (s: string): option lident =
+let lident_of_string (s: string): ML (option lident) =
   let path = FStar.String.split ['.'] s in
-  let rec go p =
+  let rec go p : ML (option lident) =
     match p with
     | [] -> None
     | [s] -> Some ([], s)
@@ -60,11 +60,11 @@ let lident_of_string (s: string): option lident =
       Some (s :: names, name))
   in go path
 
-let lident_of_typestring (t: mlty): option lident =
+let lident_of_typestring (t: mlty): ML (option lident) =
   opt_bind (string_of_typestring t) lident_of_string
 
-let int_of_typenat (t: mlty): option int =
-  let rec go t =
+let int_of_typenat (t: mlty): ML (option int) =
+  let rec go t : ML (option int) =
     match t with
     | MLTY_Named ([], p)
       when Syntax.string_of_mlpath p = "Pulse.C.Typenat.z"
@@ -81,7 +81,7 @@ let int_of_typenat (t: mlty): option int =
   in
   go t
 
-let my_types_without_decay () = 
+let my_types_without_decay () : ML unit = 
   register_pre_translate_type_without_decay begin fun env t ->
   match t with
   
@@ -124,7 +124,7 @@ let my_types_without_decay () =
   | _ -> raise NotSupportedByKrmlExtension
 end
 
-let my_types () = register_pre_translate_type begin fun env t ->
+let my_types () : ML unit = register_pre_translate_type begin fun env t ->
   match t with
   | MLTY_Named ([t; _; _], p)
     when false
@@ -135,7 +135,7 @@ let my_types () = register_pre_translate_type begin fun env t ->
   | _ -> raise NotSupportedByKrmlExtension
 end
 
-let my_exprs () = register_pre_translate_expr begin fun env e ->
+let my_exprs () : ML unit = register_pre_translate_expr begin fun env e ->
   match e.expr with
   | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ _ (* typedef *) ])
     when (
@@ -302,8 +302,8 @@ let my_exprs () = register_pre_translate_expr begin fun env e ->
   | _ -> raise NotSupportedByKrmlExtension
 end
 
-let parse_steel_c_fields env (fields: mlty): option (list _) =
-      let rec go fields =
+let parse_steel_c_fields env (fields: mlty): ML (option (list _)) =
+      let rec go fields : ML _ =
         match fields with
         | MLTY_Named ([], p)
           when false
@@ -347,6 +347,7 @@ let parse_steel_c_fields env (fields: mlty): option (list _) =
 
 let define_struct_gen
   env p args fields
+: ML (option _)
 =
     let env = List.fold_left (fun env name -> extend_t env name) env args in
     let fields = Option.must (parse_steel_c_fields env fields) in
@@ -355,6 +356,7 @@ let define_struct_gen
 
 let define_struct
   env tag fields
+: ML (option _)
 =
   (* JL: TODO remove/improve these print commands *)
   print_endline "Parsing struct definition.";
@@ -368,13 +370,15 @@ let define_struct
 
 let define_union_gen
   env p args fields
+: ML (option _)
 =
     let env = List.fold_left (fun env name -> extend_t env name) env args in
     let fields = Option.must (parse_steel_c_fields env fields) in
     Some (DUntaggedUnion (p, [], List.length args, fields))
 
 let define_union
   env tag fields
+: ML (option _)
 =
   (* JL: TODO remove/improve these print commands *)
   print_endline "Parsing union definition.";
@@ -386,7 +390,7 @@ let define_union
   | Some p ->
     define_union_gen env p [] fields
 
-let my_type_decls () = register_pre_translate_type_decl begin fun env ty ->
+let my_type_decls () : ML unit = register_pre_translate_type_decl begin fun env ty ->
     match ty with
     | {tydecl_defn=Some (MLTD_Abbrev (MLTY_Named ([tag; fields; _; _], p)))}
       when Syntax.string_of_mlpath p = "Pulse.C.Types.Struct.define_struct0"

src/extraction/ExtractPulseOCaml.fst

@@ -32,7 +32,7 @@ module Ident = FStarC.Ident
 
 let dbg = Debug.get_toggle "extraction"
 
-let hua (t:term) : option (S.fv & list S.universe & S.args) =
+let hua (t:term) : ML (option (S.fv & list S.universe & S.args)) =
   let t = U.unmeta t in
   let hd, args = U.head_and_args_full t in
   let hd = U.unmeta hd in
@@ -41,7 +41,7 @@ let hua (t:term) : option (S.fv & list S.universe & S.args) =
   | Tm_uinst ({ n = Tm_fvar fv }, us) -> Some (fv, us, args)
   | _ -> None
 
-let tr_typ (g:uenv) (t:term) : mlty =
+let tr_typ (g:uenv) (t:term) : ML mlty =
   (* Only enabled with an extension flag *)
   if Options.Ext.get "pulse:extract_ocaml_bare" = "" then
     raise NotSupportedByExtension;
@@ -74,7 +74,7 @@ let tr_typ (g:uenv) (t:term) : mlty =
   | _ -> 
     raise NotSupportedByExtension
 
-let tr_expr (g:uenv) (t:term) : mlexpr & e_tag & mlty =
+let tr_expr (g:uenv) (t:term) : ML (mlexpr & e_tag & mlty) =
   (* Only enabled with an extension flag *)
   if Options.Ext.get "pulse:extract_ocaml_bare" = "" then
     raise NotSupportedByExtension;

src/syntax_extension/PulseSyntaxExtension.ASTBuilder.fst

@@ -38,7 +38,7 @@ let tm t r = { tm=t; range=r; level=Un}
 let parse_decl_name
   : contents:string ->
     FStarC.Range.range ->
-    either AU.error_message FStarC.Ident.ident
+    ML (either AU.error_message FStarC.Ident.ident)
   = fun contents r ->
     match Parser.parse_peek_id contents r with
     | Inl s -> Inr (Ident.id_of_text s)
@@ -49,12 +49,12 @@ let parse_decl_name
 
 let i s r = tm (Const (Const_int(string_of_int s, None))) r
 let str s r = tm (Const (Const_string (s, r))) r
-let lid_as_term ns r = str (Ident.string_of_lid ns) r
+let lid_as_term ns r : ML _ = str (Ident.string_of_lid ns) r
 
 let encode_open_namespaces_and_abbreviations
     (ctx:open_namespaces_and_abbreviations)
     (r:FStarC.Range.range)
-: term & term
+: ML (term & term)
 = let tm t = tm t r in
   let str s = str s r in
   let lid_as_term ns = lid_as_term ns r in
@@ -72,7 +72,7 @@ let encode_open_namespaces_and_abbreviations
   namespaces, abbrevs
 
 let encode_range (r:FStarC.Range.range)
-: term & term & term
+: ML (term & term & term)
 = let open FStarC.Range in
   let line = line_of_pos (start_of_range r) in
   let col = col_of_pos (start_of_range r) in
@@ -82,7 +82,7 @@ let parse_decl
   : open_namespaces_and_abbreviations ->
     contents:string ->
     FStarC.Range.range ->
-    either AU.error_message decl
+    ML (either AU.error_message decl)
   = fun ctx contents r ->
       let tm t = tm t r in
       let str s = str s r in
@@ -110,7 +110,7 @@ let parse_decl
         let d = { d; drange = r; quals = [ Irreducible ]; attrs = [str "uninterpreted_by_smt"]; interleaved = false  } in
         Inr d
 
-let maybe_report_error first_error decls =
+let maybe_report_error first_error decls : ML _ =
   match first_error with
   | None -> Inr decls
   | Some (raw_error, msg, r) ->
@@ -135,7 +135,7 @@ let maybe_report_error first_error decls =
     )
 open FStarC.Class.Show
 let parse_extension_lang (contents:string) (r:FStarC.Range.range)
-: either AU.error_message (list decl)
+: ML (either AU.error_message (list decl))
 = match Parser.parse_lang contents r with
   | Inr None ->
     Inl { message = [Errors.text "#lang-pulse: Parsing failed"]; range = r }
@@ -160,7 +160,7 @@ let parse_extension_lang (contents:string) (r:FStarC.Range.range)
       in
       let splice_decl
           (d:PulseSyntaxExtension.Sugar.decl)
-      : decl
+      : ML decl
       = let id, r = id_and_range_of_decl d in  
         let id_txt = Ident.string_of_id id in
         let decors =
@@ -218,7 +218,7 @@ let desugar_pulse (env:TcEnv.env)
                   (namespaces:list string)
                   (module_abbrevs:list (string & string))
                   (sugar:sugar_decl)
-: either PulseSyntaxExtension.SyntaxWrapper.decl (option (list Pprint.document & R.range))
+: ML (either PulseSyntaxExtension.SyntaxWrapper.decl (option (list Pprint.document & R.range)))
 = let namespaces = L.map Ident.path_of_text namespaces in
   let module_abbrevs = L.map (fun (x, l) -> x, Ident.path_of_text l) module_abbrevs in
   let env = D.reinitialize_env env.dsenv (TcEnv.current_module env) namespaces module_abbrevs in
@@ -230,7 +230,7 @@ let desugar_pulse_decl_callback
       (blob:FStarC.Dyn.dyn)
       (lids:list lident)
       (rng:R.range)
-: list FStarC.Syntax.Syntax.sigelt'
+: ML (list FStarC.Syntax.Syntax.sigelt')
 = let d = D.desugar_decl (D.mk_env env) (FStarC.Dyn.undyn blob) 0 in
   match fst d with
   | Inr None ->
@@ -259,7 +259,7 @@ let parse_pulse (env:TcEnv.env)
                 (content:string)
                 (file_name:string)
                 (line col:int)
-  : either PulseSyntaxExtension.SyntaxWrapper.decl (option (list Pprint.document & R.range))
+  : ML (either PulseSyntaxExtension.SyntaxWrapper.decl (option (list Pprint.document & R.range)))
   = let range = 
       let p = R.mk_pos line col in
       R.mk_range file_name p p