From 2145dd3b74a9039c35b67a30fec01eb9212900ca Mon Sep 17 00:00:00 2001
From: Brian Campbell <Brian.Campbell@ed.ac.uk>
Date: Wed, 30 Aug 2023 17:37:20 +0100
Subject: [PATCH] Support internal_assume with -dmagic_hash for debugging

---
 src/lib/chunk_ast.ml     | 5 +++++
 src/lib/initial_check.ml | 3 +++
 src/lib/lexer.mll        | 1 +
 src/lib/parse_ast.ml     | 1 +
 src/lib/parser.mly       | 4 +++-
 5 files changed, 13 insertions(+), 1 deletion(-)

diff --git a/src/lib/chunk_ast.ml b/src/lib/chunk_ast.ml
index 0ec4a4e8a..31bd24f39 100644
--- a/src/lib/chunk_ast.ml
+++ b/src/lib/chunk_ast.ml
@@ -976,6 +976,11 @@ let rec chunk_exp comments chunks (E_aux (aux, l)) =
               { repeat_until = true; termination_measure = measure_chunks_opt; cond = cond_chunks; body = body_chunks }
             |> add_chunk chunks
       end
+  | E_internal_assume (nc, exp) ->
+      let nc_chunks = Queue.create () in
+      chunk_atyp comments nc_chunks nc;
+      let exp_chunks = rec_chunk_exp exp in
+      Queue.add (App (Id_aux (Id "internal_assume", l), [nc_chunks; exp_chunks])) chunks
 
 and chunk_vector_update comments (E_aux (aux, l) as exp) =
   let rec_chunk_exp exp =
diff --git a/src/lib/initial_check.ml b/src/lib/initial_check.ml
index 4b7357fd8..294bc70e7 100644
--- a/src/lib/initial_check.ml
+++ b/src/lib/initial_check.ml
@@ -570,6 +570,9 @@ and to_ast_exp ctx (P.E_aux (exp, l) : P.exp) =
         | P.E_internal_return exp ->
             if !opt_magic_hash then E_internal_return (to_ast_exp ctx exp)
             else raise (Reporting.err_general l "Internal return construct found without -dmagic_hash")
+        | P.E_internal_assume (nc, exp) ->
+            if !opt_magic_hash then E_internal_assume (to_ast_constraint ctx nc, to_ast_exp ctx exp)
+            else raise (Reporting.err_general l "Internal assume construct found without -dmagic_hash")
         | P.E_deref exp -> E_app (Id_aux (Id "__deref", l), [to_ast_exp ctx exp])
       in
       E_aux (aux, (l, empty_uannot))
diff --git a/src/lib/lexer.mll b/src/lib/lexer.mll
index e3308f882..18ec186ba 100644
--- a/src/lib/lexer.mll
+++ b/src/lib/lexer.mll
@@ -207,6 +207,7 @@ let kw_table =
      ("backwards",               (fun _ -> Backwards));
      ("internal_plet",           (fun _ -> InternalPLet));
      ("internal_return",         (fun _ -> InternalReturn));
+     ("internal_assume",         (fun _ -> InternalAssume));
    ]
 
 type comment_type = Comment_block | Comment_line
diff --git a/src/lib/parse_ast.ml b/src/lib/parse_ast.ml
index 1b8288745..61832914e 100644
--- a/src/lib/parse_ast.ml
+++ b/src/lib/parse_ast.ml
@@ -263,6 +263,7 @@ and exp_aux =
   | E_attribute of string * string * exp
   | E_internal_plet of pat * exp * exp
   | E_internal_return of exp
+  | E_internal_assume of atyp * exp
 
 and exp = E_aux of exp_aux * l
 
diff --git a/src/lib/parser.mly b/src/lib/parser.mly
index a3c124894..ae73aa9dc 100644
--- a/src/lib/parser.mly
+++ b/src/lib/parser.mly
@@ -226,7 +226,7 @@ let warn_extern_effect l =
 %token Undefined Union Newtype With Val Outcome Constraint Throw Try Catch Exit Bitfield Constant
 %token Barr Depend Rreg Wreg Rmem Wmem Wmv Eamem Exmem Undef Unspec Nondet Escape
 %token Repeat Until While Do Mutual Var Ref Configuration TerminationMeasure Instantiation Impl
-%token InternalPLet InternalReturn
+%token InternalPLet InternalReturn InternalAssume
 %token Forwards Backwards
 
 %nonassoc Then
@@ -899,6 +899,8 @@ exp:
     { mk_exp (E_internal_plet ($2,$4,$6)) $startpos $endpos }
   | InternalReturn exp
     { mk_exp (E_internal_return($2)) $startpos $endpos }
+  | InternalAssume typ In exp
+    { mk_exp (E_internal_assume($2,$4)) $startpos $endpos }
 
 /* The following implements all nine levels of user-defined precedence for
 operators in expressions, with both left, right and non-associative operators */