Refactor Initial_check to remove some state

Previously we would had a variable incremental_ctx that we would be update for
each parsed file. This is one of the last pieces of global state in the Sail frontend
that needed to be removed.

Turns out that doing this is a bit tricky because the prover_regstate is a bit special,
so we need to thread the Initial_check context through the rewrites all the way to the
backends.

The targets were getting an unwieldy amount of arguments so now just use the
Interactive.State.istate type which is a struct containing everything we need.

Author: Alasdair

src/bin/repl.ml

@@ -81,10 +81,11 @@ type mode = Evaluation of frame | Normal
 type display_options = { clear : bool; registers : IdSet.t }
 
 type istate = {
+  ctx : Initial_check.ctx;
   ast : Type_check.typed_ast;
   effect_info : Effects.side_effect_info;
   env : Type_check.Env.t;
-  ref_state : Interactive.istate ref;
+  ref_state : Interactive.State.istate ref;
   vs_ids : IdSet.t ref;
   options : (Arg.key * Arg.spec * Arg.doc) list;
   mode : mode;
@@ -94,21 +95,23 @@ type istate = {
   config : Yojson.Basic.t option;
 }
 
-let shrink_istate istate : Interactive.istate =
+let shrink_istate istate : Interactive.State.istate =
   {
+    ctx = istate.ctx;
     ast = istate.ast;
     effect_info = istate.effect_info;
     env = istate.env;
     default_sail_dir = istate.default_sail_dir;
     config = istate.config;
   }
 
-let initial_istate config options env effect_info ast =
+let initial_istate config options ctx env effect_info ast =
   {
+    ctx;
     ast;
     effect_info;
     env;
-    ref_state = ref (Interactive.initial_istate config Locations.sail_dir);
+    ref_state = ref (Interactive.State.initial_istate config Locations.sail_dir);
     vs_ids = ref (val_spec_ids ast.defs);
     options;
     mode = Normal;
@@ -121,6 +124,7 @@ let initial_istate config options env effect_info ast =
 let setup_interpreter_state istate =
   istate.ref_state :=
     {
+      ctx = istate.ctx;
       ast = istate.ast;
       effect_info = istate.effect_info;
       env = istate.env;
@@ -632,19 +636,19 @@ let handle_input' istate input =
           | ":def" ->
               (* Add an extra blank line so we can handle directives that require a newline to be parsed. *)
               ignore (Sail_file.add_to_repl_contents ~command:"");
-              let ast =
-                Initial_check.ast_of_def_string_with ~inline:pos __POS__
+              let ast, ctx =
+                Initial_check.ast_of_def_string_with ~inline:pos __POS__ istate.ctx
                   (Preprocess.preprocess istate.default_sail_dir None istate.options)
                   (arg ^ "\n")
               in
               let ast, env = Type_check.check istate.env ast in
-              { istate with ast = append_ast istate.ast ast; env }
+              { istate with ast = append_ast istate.ast ast; env; ctx }
           | ":rewrite" ->
               let open Rewrites in
               let args = Str.split (Str.regexp " +") arg in
               let rec parse_args rw args =
                 match (rw, args) with
-                | Base_rewriter rw, [] -> rw
+                | Full_rewriter rw, [] -> rw
                 | Bool_rewriter rw, arg :: args -> parse_args (rw (bool_of_string arg)) args
                 | String_rewriter rw, arg :: args -> parse_args (rw arg) args
                 | Literal_rewriter rw, arg :: args -> begin
@@ -661,8 +665,8 @@ let handle_input' istate input =
                 | rw :: args ->
                     let rw = List.assoc rw Rewrites.all_rewriters in
                     let rw = parse_args rw args in
-                    let ast', effect_info', env' = rw istate.effect_info istate.env istate.ast in
-                    { istate with ast = ast'; effect_info = effect_info'; env = env' }
+                    let ctx', ast', effect_info', env' = rw istate.ctx istate.effect_info istate.env istate.ast in
+                    { istate with ctx = ctx'; ast = ast'; effect_info = effect_info'; env = env' }
                 | [] ->
                     failwith "Must provide the name of a rewrite, use :list_rewrites for a list of possible rewrites"
               end
@@ -764,16 +768,16 @@ let handle_input istate input =
       print_endline (Printexc.to_string exn);
       istate
 
-let start_repl ?(banner = true) ?commands:(script = []) ?auto_rewrites:(rewrites = true) ~config ~options env
+let start_repl ?(banner = true) ?commands:(script = []) ?auto_rewrites:(rewrites = true) ~config ~options ctx env
     effect_info ast =
   let istate =
     if rewrites then (
-      let ast, effect_info, env =
-        Rewrites.rewrite effect_info env (Rewrites.instantiate_rewrites Rewrites.rewrites_interpreter) ast
+      let ctx, ast, effect_info, env =
+        Rewrites.rewrite ctx effect_info env (Rewrites.instantiate_rewrites Rewrites.rewrites_interpreter) ast
       in
-      initial_istate config options env effect_info ast
+      initial_istate config options ctx env effect_info ast
     )
-    else initial_istate config options env effect_info ast
+    else initial_istate config options ctx env effect_info ast
   in
 
   LNoise.set_completion_callback (fun line_so_far ln_completions ->

src/bin/repl.mli

@@ -85,6 +85,7 @@ val start_repl :
   ?auto_rewrites:bool ->
   config:Yojson.Basic.t option ->
   options:(Arg.key * Arg.spec * Arg.doc) list ->
+  Initial_check.ctx ->
   Env.t ->
   Effects.side_effect_info ->
   typed_ast ->

src/bin/sail.ml

@@ -67,6 +67,8 @@
 
 open Libsail
 
+open Interactive.State
+
 type version = { major : int; minor : int; patch : int }
 
 (* Current version of Sail. Must be updated manually. CI checks this matches
@@ -415,7 +417,7 @@ let run_sail (config : Yojson.Basic.t option) tgt =
     List.partition (fun free -> Filename.check_suffix free ".sail_project") !opt_free_arguments
   in
 
-  let ast, env, effect_info =
+  let ctx, ast, env, effect_info =
     match (project_files, !opt_project_files) with
     | [], [] ->
         (* If there are no provided project files, we concatenate all
@@ -467,19 +469,19 @@ let run_sail (config : Yojson.Basic.t option) tgt =
           )
   in
   let ast, env = Frontend.initial_rewrite effect_info env ast in
-  let ast, env = match !opt_splice with [] -> (ast, env) | files -> Splice.splice_files ast (List.rev files) in
+  let ast, env = match !opt_splice with [] -> (ast, env) | files -> Splice.splice_files ctx ast (List.rev files) in
   let effect_info = Effects.infer_side_effects (Target.asserts_termination tgt) ast in
 
   (* Don't show warnings during re-writing for now *)
   Reporting.suppressed_warning_info ();
   Reporting.opt_warnings := false;
 
   Target.run_pre_rewrites_hook tgt ast effect_info env;
-  let ast, effect_info, env = Rewrites.rewrite effect_info env (Target.rewrites tgt) ast in
+  let ctx, ast, effect_info, env = Rewrites.rewrite ctx effect_info env (Target.rewrites tgt) ast in
 
-  Target.action tgt config Locations.sail_dir !opt_file_out ast effect_info env;
+  Target.action tgt !opt_file_out { ctx; ast; effect_info; env; default_sail_dir = Locations.sail_dir; config };
 
-  (ast, env, effect_info)
+  (ctx, ast, env, effect_info)
 
 let run_sail_format (config : Yojson.Basic.t option) =
   let is_format_file f = match !opt_format_only with [] -> true | files -> List.exists (fun f' -> f = f') files in
@@ -616,7 +618,7 @@ let main () =
 
   if !opt_memo_z3 then Constraint.load_digests ();
 
-  let ast, env, effect_info =
+  let ctx, ast, env, effect_info =
     match Target.get_the_target () with
     | Some target when not !opt_just_check -> run_sail config target
     | _ -> run_sail config default_target
@@ -640,7 +642,7 @@ let main () =
           with End_of_file -> List.rev !lines
         )
     in
-    Repl.start_repl ~commands:script ~auto_rewrites:!opt_auto_interpreter_rewrites ~config ~options:!options env
+    Repl.start_repl ~commands:script ~auto_rewrites:!opt_auto_interpreter_rewrites ~config ~options:!options ctx env
       effect_info ast
   )
 

src/lib/ast_util.ml

@@ -108,6 +108,8 @@ let attribute_data_bool = function AD_aux (AD_bool b, _) -> Some b | _ -> None
 
 let attribute_data_string = function AD_aux (AD_string s, _) -> Some s | _ -> None
 
+let attribute_data_string_with_loc = function AD_aux (AD_string s, l) -> Some (s, l) | _ -> None
+
 let json_of_attribute attr = function
   | None -> `String attr
   | Some data -> `List [`String attr; json_of_attribute_data data]
@@ -204,9 +206,9 @@ let rec is_gen_loc = function
 
 let mk_id ?loc:(l = Parse_ast.Unknown) str = Id_aux (Id str, l)
 
-let mk_nc nc_aux = NC_aux (nc_aux, Parse_ast.Unknown)
+let mk_nc ?loc:(l = Parse_ast.Unknown) nc_aux = NC_aux (nc_aux, l)
 
-let mk_nexp nexp_aux = Nexp_aux (nexp_aux, Parse_ast.Unknown)
+let mk_nexp ?loc:(l = Parse_ast.Unknown) nexp_aux = Nexp_aux (nexp_aux, l)
 
 let mk_exp ?loc:(l = Parse_ast.Unknown) exp_aux = E_aux (exp_aux, (l, empty_uannot))
 let unaux_exp (E_aux (exp_aux, _)) = exp_aux
@@ -221,36 +223,36 @@ let untyp_pat = function P_aux (P_typ (typ, pat), _) -> (pat, Some typ) | pat ->
 
 let mk_pexp ?loc:(l = Parse_ast.Unknown) pexp_aux = Pat_aux (pexp_aux, (l, empty_uannot))
 
-let mk_mpat mpat_aux = MP_aux (mpat_aux, no_annot)
-let mk_mpexp mpexp_aux = MPat_aux (mpexp_aux, no_annot)
+let mk_mpat ?loc:(l = Parse_ast.Unknown) mpat_aux = MP_aux (mpat_aux, (l, empty_uannot))
+let mk_mpexp ?loc:(l = Parse_ast.Unknown) mpexp_aux = MPat_aux (mpexp_aux, (l, empty_uannot))
 
-let mk_lexp lexp_aux = LE_aux (lexp_aux, no_annot)
+let mk_lexp ?loc:(l = Parse_ast.Unknown) lexp_aux = LE_aux (lexp_aux, (l, empty_uannot))
 
-let mk_typ_pat tpat_aux = TP_aux (tpat_aux, Parse_ast.Unknown)
+let mk_typ_pat ?loc:(l = Parse_ast.Unknown) tpat_aux = TP_aux (tpat_aux, l)
 
-let mk_lit lit_aux = L_aux (lit_aux, Parse_ast.Unknown)
+let mk_lit ?loc:(l = Parse_ast.Unknown) lit_aux = L_aux (lit_aux, Parse_ast.Unknown)
 
-let mk_lit_exp ?loc:(l = Parse_ast.Unknown) lit_aux = mk_exp ~loc:l (E_lit (mk_lit lit_aux))
+let mk_lit_exp ?loc:(l = Parse_ast.Unknown) lit_aux = mk_exp ~loc:l (E_lit (mk_lit ~loc:l lit_aux))
 
 let mk_funcl ?loc:(l = Parse_ast.Unknown) id pat body =
   FCL_aux (FCL_funcl (id, Pat_aux (Pat_exp (pat, body), (l, empty_uannot))), (mk_def_annot l (), empty_uannot))
 
-let mk_qi_nc nc = QI_aux (QI_constraint nc, Parse_ast.Unknown)
+let mk_qi_nc ?loc:(l = Parse_ast.Unknown) nc = QI_aux (QI_constraint nc, l)
 
-let mk_qi_id k kid =
-  let kopt = KOpt_aux (KOpt_kind (K_aux (k, Parse_ast.Unknown), kid), Parse_ast.Unknown) in
-  QI_aux (QI_id kopt, Parse_ast.Unknown)
+let mk_qi_id ?loc:(l = Parse_ast.Unknown) k kid =
+  let kopt = KOpt_aux (KOpt_kind (K_aux (k, l), kid), l) in
+  QI_aux (QI_id kopt, l)
 
-let mk_qi_kopt kopt = QI_aux (QI_id kopt, Parse_ast.Unknown)
+let mk_qi_kopt ?loc:(l = Parse_ast.Unknown) kopt = QI_aux (QI_id kopt, l)
 
-let mk_fundef funcls =
-  let tannot_opt = Typ_annot_opt_aux (Typ_annot_opt_none, Parse_ast.Unknown) in
-  let rec_opt = Rec_aux (Rec_nonrec, Parse_ast.Unknown) in
-  DEF_aux (DEF_fundef (FD_aux (FD_function (rec_opt, tannot_opt, funcls), no_annot)), mk_def_annot Parse_ast.Unknown ())
+let mk_fundef ?loc:(l = Parse_ast.Unknown) funcls =
+  let tannot_opt = Typ_annot_opt_aux (Typ_annot_opt_none, l) in
+  let rec_opt = Rec_aux (Rec_nonrec, l) in
+  DEF_aux (DEF_fundef (FD_aux (FD_function (rec_opt, tannot_opt, funcls), no_annot)), mk_def_annot l ())
 
 let mk_letbind ?loc:(l = Parse_ast.Unknown) pat exp = LB_aux (LB_val (pat, exp), (l, empty_uannot))
 
-let mk_val_spec vs_aux = DEF_aux (DEF_val (VS_aux (vs_aux, no_annot)), mk_def_annot Parse_ast.Unknown ())
+let mk_val_spec ?loc:(l = Parse_ast.Unknown) vs_aux = DEF_aux (DEF_val (VS_aux (vs_aux, no_annot)), mk_def_annot l ())
 
 let mk_def ?loc:(l = Parse_ast.Unknown) def env = DEF_aux (def, mk_def_annot l env)
 
@@ -642,11 +644,11 @@ let rec constraint_conj (NC_aux (nc_aux, _) as nc) =
 let rec constraint_disj (NC_aux (nc_aux, _) as nc) =
   match nc_aux with NC_or (nc1, nc2) -> constraint_disj nc1 @ constraint_disj nc2 | _ -> [nc]
 
-let mk_typ typ = Typ_aux (typ, Parse_ast.Unknown)
-let mk_typ_arg arg = A_aux (arg, Parse_ast.Unknown)
-let mk_kid str = Kid_aux (Var ("'" ^ str), Parse_ast.Unknown)
+let mk_typ ?loc:(l = Parse_ast.Unknown) typ = Typ_aux (typ, l)
+let mk_typ_arg ?loc:(l = Parse_ast.Unknown) arg = A_aux (arg, l)
+let mk_kid ?loc:(l = Parse_ast.Unknown) str = Kid_aux (Var ("'" ^ str), l)
 
-let mk_id_typ id = Typ_aux (Typ_id id, Parse_ast.Unknown)
+let mk_id_typ ?loc:(l = Parse_ast.Unknown) id = Typ_aux (Typ_id id, l)
 
 let mk_kopt ?loc:(l = Parse_ast.Unknown) kind_aux v =
   let l = match l with Parse_ast.Unknown -> kid_loc v | l -> l in
@@ -723,12 +725,12 @@ let arg_kopt (KOpt_aux (KOpt_kind (K_aux (k, _), v), _)) =
 
 let nc_not nc = mk_nc (NC_app (mk_id "not", [arg_bool nc]))
 
-let mk_typschm typq typ = TypSchm_aux (TypSchm_ts (typq, typ), Parse_ast.Unknown)
+let mk_typschm ?loc:(l = Parse_ast.Unknown) typq typ = TypSchm_aux (TypSchm_ts (typq, typ), l)
 
 let mk_empty_typquant ~loc:l = TypQ_aux (TypQ_no_forall, l)
-let mk_typquant qis = TypQ_aux (TypQ_tq qis, Parse_ast.Unknown)
+let mk_typquant ?loc:(l = Parse_ast.Unknown) qis = TypQ_aux (TypQ_tq qis, l)
 
-let mk_fexp id exp = FE_aux (FE_fexp (id, exp), no_annot)
+let mk_fexp ?loc:(l = Parse_ast.Unknown) id exp = FE_aux (FE_fexp (id, exp), (l, empty_uannot))
 
 type effect = bool
 
@@ -1980,6 +1982,18 @@ and locate_lexp : 'a. (l -> l) -> 'a lexp -> 'a lexp =
 and locate_fexp : 'a. (l -> l) -> 'a fexp -> 'a fexp =
  fun f (FE_aux (FE_fexp (id, exp), (l, annot))) -> FE_aux (FE_fexp (locate_id f id, locate f exp), (f l, annot))
 
+let unknown_to into_l l =
+  let open Parse_ast in
+  let rec go l =
+    match l with
+    | Unknown -> into_l
+    | Hint (msg, l1, l2) -> Hint (msg, go l1, go l2)
+    | Generated l -> Generated (go l)
+    | Unique (n, l) -> Unique (n, go l)
+    | Range _ -> l
+  in
+  go l
+
 let unique_ref = ref 0
 
 let unique l =

src/lib/ast_util.mli

@@ -102,6 +102,8 @@ val attribute_data_bool : attribute_data -> bool option
 
 val attribute_data_string : attribute_data -> string option
 
+val attribute_data_string_with_loc : attribute_data -> (string * Parse_ast.l) option
+
 (** Add an attribute to an annotation. Attributes are attached to expressions in Sail  via:
     {@sail[
     $[attribute argument] expression
@@ -177,28 +179,28 @@ val is_order_dec : order -> bool
 (** {2 Functions for building untyped AST elements} *)
 
 val mk_id : ?loc:l -> string -> id
-val mk_kid : string -> kid
-val mk_nc : n_constraint_aux -> n_constraint
-val mk_nexp : nexp_aux -> nexp
+val mk_kid : ?loc:l -> string -> kid
+val mk_nc : ?loc:l -> n_constraint_aux -> n_constraint
+val mk_nexp : ?loc:l -> nexp_aux -> nexp
 val mk_exp : ?loc:l -> uannot exp_aux -> uannot exp
 val mk_pat : ?loc:l -> uannot pat_aux -> uannot pat
-val mk_mpat : uannot mpat_aux -> uannot mpat
+val mk_mpat : ?loc:l -> uannot mpat_aux -> uannot mpat
 val mk_pexp : ?loc:l -> uannot pexp_aux -> uannot pexp
-val mk_mpexp : uannot mpexp_aux -> uannot mpexp
-val mk_lexp : uannot lexp_aux -> uannot lexp
-val mk_lit : lit_aux -> lit
+val mk_mpexp : ?loc:l -> uannot mpexp_aux -> uannot mpexp
+val mk_lexp : ?loc:l -> uannot lexp_aux -> uannot lexp
+val mk_lit : ?loc:l -> lit_aux -> lit
 val mk_lit_exp : ?loc:l -> lit_aux -> uannot exp
-val mk_typ_pat : typ_pat_aux -> typ_pat
+val mk_typ_pat : ?loc:l -> typ_pat_aux -> typ_pat
 val mk_funcl : ?loc:l -> id -> uannot pat -> uannot exp -> uannot funcl
-val mk_fundef : uannot funcl list -> untyped_def
-val mk_val_spec : val_spec_aux -> untyped_def
-val mk_typschm : typquant -> typ -> typschm
+val mk_fundef : ?loc:l -> uannot funcl list -> untyped_def
+val mk_val_spec : ?loc:l -> val_spec_aux -> untyped_def
+val mk_typschm : ?loc:l -> typquant -> typ -> typschm
 val mk_empty_typquant : loc:l -> typquant
-val mk_typquant : quant_item list -> typquant
-val mk_qi_id : kind_aux -> kid -> quant_item
-val mk_qi_nc : n_constraint -> quant_item
-val mk_qi_kopt : kinded_id -> quant_item
-val mk_fexp : id -> uannot exp -> uannot fexp
+val mk_typquant : ?loc:l -> quant_item list -> typquant
+val mk_qi_id : ?loc:l -> kind_aux -> kid -> quant_item
+val mk_qi_nc : ?loc:l -> n_constraint -> quant_item
+val mk_qi_kopt : ?loc:l -> kinded_id -> quant_item
+val mk_fexp : ?loc:l -> id -> uannot exp -> uannot fexp
 val mk_letbind : ?loc:l -> uannot pat -> uannot exp -> uannot letbind
 val mk_kopt : ?loc:l -> kind_aux -> kid -> kinded_id
 val mk_def : ?loc:l -> ('a, 'b) def_aux -> 'b -> ('a, 'b) def
@@ -235,9 +237,9 @@ val is_bool_kopt : kinded_id -> bool
 
 (** {2 Utility functions for constructing types} *)
 
-val mk_typ : typ_aux -> typ
-val mk_typ_arg : typ_arg_aux -> typ_arg
-val mk_id_typ : id -> typ
+val mk_typ : ?loc:l -> typ_aux -> typ
+val mk_typ_arg : ?loc:l -> typ_arg_aux -> typ_arg
+val mk_id_typ : ?loc:l -> id -> typ
 
 val is_typ_arg_nexp : typ_arg -> bool
 val is_typ_arg_typ : typ_arg -> bool
@@ -585,6 +587,8 @@ val hex_to_bin : string -> string
 
 val vector_string_to_bit_list : lit -> lit list
 
+val extern_assoc : string -> extern option -> string option
+
 (** {1 Manipulating locations} *)
 
 (** locate takes an expression and recursively sets the location in
@@ -605,7 +609,10 @@ val locate_typ : (l -> l) -> typ -> typ
    a generated number. *)
 val unique : l -> l
 
-val extern_assoc : string -> extern option -> string option
+(** Convert unknown locations into known ones by replacing any Unknown
+    subparts of the second argument with the first argument. Set up so
+    one can do: [locate (unknown_to l) exp] and similar. *)
+val unknown_to : l -> l -> l
 
 (** Try to find the annotation closest to the provided location (which
     can be in any format, as long as we can tell if it is smaller than