Theory try

(*
 * Copyright (c) 2023 Apple Inc. All rights reserved.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

(*
 * Tests for handling "try" construct introduced by Autocorres.
 *)
theory "try"
imports "AutoCorres2_Main.AutoCorres_Main"
begin

install_C_file "try.c"

autocorres []"try.c"

context ts_definition_w begin

thm w'_def
print_synthesize_rules exit
lemma "w' x ≡
  do { whileLoop (λx s. 0 < x)
               (λx. condition (λs. x = 0x2A)
                       (throw 1)
                       (return (x - 1)))
              x;
             skip
         }"
  ― ‹we do not want a const‹try› to show up in the definition of const‹w'›!›
  by (rule w'_def)

end

context ts_definition_f begin

thm f'_def

lemma "f' x ≡
  (do { assert_0' (sint x);
       when (x = 1) (throw ((- 1)));
       return (x + 1)
   })"
  ― ‹we do not want a const‹try› to show up in the definition of const‹f'›!›
  by (rule f'_def)

end

context ts_definition_g begin

thm g'_def

lemma "g' x ≡
  (do { assert_0' (sint x);
       condition (λs. x = 1)
         (throw (- 1))
         (return (x + 1))
   })"
  ― ‹we do not want a const‹try› to show up in the definition of const‹g'›!›
  by (rule g'_def)

end

context ts_definition_h begin

thm h'_def

lemma "h' x ≡
  do { assert_0' 1;
    (a, b) <- return (if x = 0 then (2, 3) else (6, 7));
    ret <- return (do_cmp' a b);
    unless (ret = 0) (assert_0' 2)
  }"
  ― ‹we do not want a const‹try› to show up in the definition of const‹h'›!›
  by (rule h'_def)

end

context wa_definition_i1 begin
thm wa_def
end
context ts_definition_i1 begin

thm i1'_def

lemma "i1' x ≡
  do { assert_0' (sint x);
    condition (λs. x = 0)
      (do { assert_0' 0;
           return 1
       })
      (return (x + 1))
  }"
  ― ‹we do not want a const‹try› to show up in the definition of const‹i1'›!›
  by (rule i1'_def)

end

context ts_definition_i2 begin

thm i2'_def
term i2'

lemma "i2' x ≡ do { assert_0' (sint x);
              condition (λs. x = 0)
                (liftE (do { x <- return 1;
                           return (x + 1)
                        }))
                (do{ assert_0' (sint x);
                     return 1
                 })
          }"
  ― ‹we do not want a const‹try› to show up in the definition of const‹i2'›!›
  
  by (rule i2'_def)

end

context ts_definition_i3 begin

thm i3'_def [no_vars]

lemma "i3' x ≡ do {
  _ ← assert_0' (sint x);
  condition (λs. 0 < x) 
    (condition (λs. x = 1) 
      (do {v ← assert_0' 1; return 1})
      (return 2))
    (return (x + 1))
}"
  ― ‹we do not want a const‹try› to show up in the definition of const‹i3'›!›
  by (rule i3'_def)

end

context ts_definition_i4 begin

thm i4'_def
term i4'
lemma "i4' x ≡
  do { assert_0' (sint x);
        condition (λs. x = 0)
          (do { assert_0' 0;
               modify (a_''_update (λold. 0));
               return 0
           })
          (return (x + 1))
    }"
  ― ‹we do not want a const‹try› to show up in the definition of const‹i4'›!›
  by (rule i4'_def)

end

context ts_definition_finally_elimination2 begin

thm finally_elimination2'_def
term finally_elimination2'
lemma "finally_elimination2' x ≡
heap_w32.assume_with_fresh_stack_ptr 1 (λa. {[x]})
 (λxp. do {condition (λs. 2 < heap_w32 s xp)
             (do {x <- gets (λs. heap_w32 s xp);
                 ret <- return (inc_value' x);
                 modify (heap_w32_update (λh. h(xp := ret)))
              })
             (inc' xp)
        })"
  ― ‹we do not want a const‹finally› to show up in the definition of
    const‹finally_elimination2'›!›
  by (rule finally_elimination2'_def)

end

end