Theory C_paper

(******************************************************************************
 * Isabelle/C
 *
 * Copyright (c) 2018-2019 Université Paris-Saclay, Univ. Paris-Sud, France
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 *     * Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *
 *     * Redistributions in binary form must reproduce the above
 *       copyright notice, this list of conditions and the following
 *       disclaimer in the documentation and/or other materials provided
 *       with the distribution.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 ******************************************************************************)

chapter ‹Examples from the F-IDE Paper›

theory C_paper
  imports "../main/C_Main"
begin

text ‹ This theory contains the examples presented in F-IDE 2019 paper~\<^cite>‹"Tuong-IsabelleC:2019"›. ›

section ‹Setup›

ML‹
― ‹Annotation Commands Mimicking the ⬚‹setup› command›
val _ = Theory.setup
          (C_Inner_Syntax.command C_Inner_Isar_Cmd.setup' C_Parse.ML_source ("≃setup", ⌂, ⌂))

val C = C_Module.C'

fun C_def dir name _ _ =
  Context.map_theory 
    (C_Inner_Syntax.command'
      (C_Inner_Syntax.drop1
        (C_Scan.Right ( (fn src => fn context =>
                          C_Module.C' (SOME (C_Stack.Data_Lang.get' context |> #2)) src context)
                      , dir)))
      C_Parse.C_source
      name)

― ‹Defining the ML Antiquotation ‹C_def› to define on the fly new C annotation commands›
local
in
val _ = Theory.setup
  (ML_Antiquotation.declaration
    @{binding "C_def"}
    (Scan.lift (Parse.sym_ident -- Parse.position Parse.name))
    (fn _ => fn (top_down, (name, pos)) =>
      tap (fn ctxt => Context_Position.reports ctxt [(pos, Markup.keyword1)]) #>
      C_Context.fun_decl
               "cmd" "x" ( "C_def "
                         ^ (case top_down of "⇑" => "C_Inner_Syntax.bottom_up"
                                           | "⇓" => "C_Env.Top_down"
                                           | _ => error "Illegal symbol")
                         ^ " (\"" ^ name ^ "\", " ^ ML_Syntax.print_position pos ^ ")")))
end
›

text ‹ The next command is predefined here, so that the example below can later refer to the
constant. ›
definition [simplified]: "UINT_MAX ≡ (2 :: nat) ^ 32 - 1"

section ‹Defining Annotation Commands›

ML ― ‹\<^theory>‹Isabelle_C.C_Command›› ‹
local
datatype antiq_hol = Invariant of string (* term *)
val scan_colon = C_Parse.$$$ ":" >> SOME
fun command cmd scan0 scan f =
  C_Annotation.command' cmd "" (K (scan0 -- (scan >> f)
                                      >> K C_Env.Never))
in
val _ = Theory.setup ((* 1 '@' *)
                         command ("INVARIANT", ⌂) scan_colon C_Parse.term Invariant
                      #> command ("INV", ⌂) scan_colon C_Parse.term Invariant)
end
›

text‹Demonstrating the Effect of Annotation Command Context Navigation ›


C ‹
int sum1(int a)
{
  while (a < 10)
    /*@ @ INV: ‹…›
        @ highlight */
    { a = a + 1; }
  return a;
}›



C ‹
int sum2(int a)
/*@ ++@ INV: ‹…›
    ++@ highlight */
{
  while (a < 10)
    { a = a + 1; }
  return a;
}›




C (*NONE*) ― ‹starting environment = empty› ‹
int a (int b) { return &a + b + c; }
/*@ ≃setup ‹fn stack_top => fn env =>
            C (SOME env) ‹int c = &a + b + c;››
    ≃setup ‹fn stack_top => fn env =>
            C  NONE      ‹int c = &a + b + c;››
    declare [[C⇩_e⇩_n⇩_v⇩₀ = last]]
    C        (*SOME*)    ‹int c = &a + b + c;›
*/›

section ‹Proofs inside C-Annotations›

― ‹See also: 🌐‹https://gitlab.lisn.upsaclay.fr/burkhart.wolff/Isabelle_C/-/blob/C/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_linear_CCT.thy››

C ‹
#define SQRT_UINT_MAX 65536
/*@ lemma uint_max_factor [simp]:
      "UINT_MAX = SQRT_UINT_MAX * SQRT_UINT_MAX - 1"
    by (clarsimp simp: UINT_MAX_def SQRT_UINT_MAX_def)
*/›

term SQRT_UINT_MAX

section ‹Scheduling the Effects on the Logical Context›

C ‹int _;
/*@ @ C ‹//@ C1 ‹int _; //@ @ ≃setup⇓ ‹@{C_def ⇑ C2}› \
                            @ C1  ‹//* C2 ‹int _;››   \
                            @ C1⇓ ‹//* C2 ‹int _;››    ››
    @ C ‹//* C2 ‹int _;›                                ›
      ≃setup ‹@{C_def ⇑ (* bottom-up *)  C1  }›
      ≃setup ‹@{C_def ⇓ (* top-down  *) "C1⇓"}›
*/›

section ‹As Summary: A Spaghetti Language --- Bon Appétit!›

text‹... with the Bonus of a local C-inside-ML-inside-C-inside-Isar ...›

ML‹
fun highlight (_, (_, pos1, pos2)) =
  tap (fn _ => Position.reports_text [((Position.range (pos1, pos2)
                                        |> Position.range_position, Markup.intensify), "")])
›

C (*NONE*) ― ‹ the command starts with a default empty environment ›
‹int f (int a)
  //@ ++& ≃setup ‹fn stack_top => fn env => highlight stack_top›
  { /*@ @ ≃setup ‹fn stack_top => fn env =>
                    C (SOME env) (* the command starts with some provided environment *)
                     ‹int b = a + b; //@ C1' ‹int c; //@ @ ≃setup⇓ ‹@{C_def ⇑ C2'}› \
                                                         @ C1'  ‹//* C2' ‹int d;››        \
                                                         @ C1'⇓ ‹//* C2' ‹int d;››        ›
                      int b = a + b + c + d;››
        @ ≃setup ‹fn stack_top => fn env => C NONE ‹#define int int
                                                    int b = a + b; //* C2' ‹int c = b;›››
          ≃setup ‹@{C_def ⇑ (* bottom-up *)  C1'  }›
          ≃setup ‹@{C_def ⇓ (* top-down  *) "C1'⇓"}›
     */
    return a + b + c + d; /* explicit highlighting */ }›

text ‹ Note that in the current design-implementation of Isabelle/C, C directives have a
propagation side-effect to any occurring subsequent C annotations, even if C directives are supposed
to be all evaluated before any C code. (Making such effect inexistent would be equally easier to
implement though, this is what was the default behavior of directives in previous versions of
Isabelle/C.)›

end