File ‹termstypes-sig.ML›

(*
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 * Copyright (c) 2022 Apple Inc. All rights reserved.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

signature INT_INFO = sig
  val int : typ
  val long : typ
  val short : typ
  val char : typ
  val bool : typ
  val longlong : typ
  val int128 : typ
  val addr_ty : typ
  val ity_to_nat : term -> term
  val numeral2w : int Absyn.ctype -> int -> term
  val ptrdiff_ity : typ
  val INT_MAX : int
  val INT_MIN : int
  val UINT_MAX : int
  val gen_ity2wty: {bitint_padding:bool} -> int Absyn.ctype -> typ
  val ity2wty : int Absyn.ctype -> typ
  val nat_to_word : int Absyn.ctype -> term -> term
  val word_to_int : int Absyn.ctype -> term -> term
end

signature TERMS_TYPES =
sig
  include ISABELLE_TERMS_TYPES
  include HP_TERMS_TYPES

  (* Free variables which will be locale parameters *)
  val symbol_table : term

  (* types - words and arrays *)
  val word_ty : typ -> typ
  val word8 : typ
  val word16 : typ
  val word32 : typ
  val word64 : typ
  val word128 : typ

  val to_unsigned_word: typ -> typ option
  val to_signed_word: typ -> typ option
  val is_unsigned_word: typ -> bool
  val is_signed_word: typ -> bool
  val coerce_word: typ -> typ -> term -> term

  val mk_word_ty: int -> typ
  val mk_sword_ty: int -> typ
  val dest_array_type : typ -> typ * typ
  val dest_array_index : typ -> typ * int
  val mk_array_type : typ * int -> typ
  val is_array_type: typ -> bool
  val element_type : typ -> typ
  val innermost_element_type : typ -> typ
  val array_dimension: typ -> int
  val array_indexes: typ -> int list

  (* terms *)
  val mk_array_update_t : typ -> term (* element type *)
  val mk_array_nth : term * term -> term (* number second *)

  structure IntInfo : INT_INFO

  (* Basic machine terms/types - for calculate_state.ML *)
  val mk_ptr_ty : typ -> typ
  val is_ptr_ty : typ -> bool
  val addr_ty : typ
  val mk_okptr : term -> term
  val heap_ty : typ
  val mk_sizeof : term -> term

  (* More terms/types - for expression_translation.ML *)
  val NULLptr : term
  val mk_ptr : term * typ -> term
  val mk_fnptr : theory -> MString.t -> term
  val mk_cguard_ptr : term -> term
  val mk_global_addr_ptr : Proof.context -> string * typ -> term
  val mk_local_ptr_name : string -> string
  val dest_local_ptr_name : string -> string
  val mk_local_ptr : string * typ -> term

  val dest_ptr_ty : typ -> typ
  val mk_ptr_val : term -> term (* there is a HOL constant "ptr_val" *)
  val mk_ptr_coerce : term * typ -> term
  val mk_ptr_add : term * term -> term
  val mk_lift : term * term -> term


  val mk_lshift : term * term -> term
  val mk_rshift : term * term -> term
  val mk_arith_rshift : term * term -> term

  (* Given (addr,value) yield a primitive heap => heap transformer. *)
  val mk_heap_upd : term * term -> term

  val mk_field_lvalue_ptr : Proof.context -> term * term * typ * typ -> term

  val mk_qualified_field_name : string -> term
  val field_name_ty : typ
  val qualified_field_name_ty : typ

  val mk_asm_spec : typ list -> typ -> term -> bool -> string
    -> term -> term list -> term
  val mk_asm_ok_to_ignore : typ -> bool -> string -> term

  datatype 'varinfo termbuilder =
           TB of {var_updator : bool -> 'varinfo -> term -> term -> term,
                  var_accessor : 'varinfo -> term -> term,
                  rcd_updator : string*string -> term -> term -> term,
                  rcd_accessor : string*string -> term -> term}
                  (* in updator functions, first term is the new value,
                     second is composite value being updated *)

  (* for creation of uint w, and sint w terms *)
  val mk_w2ui : term -> term
  val mk_w2si : term -> term

end