Isabelle2021-1

examples/ROOT

@@ -60,7 +60,7 @@ session "HOL-TestGen-MyKeOS" in "concurrency/MyKeOS" = "HOL-TestGen" +
      "main.tex"
      "titlepage.tex"
 
-session "HOL-TestGen-MyKeOS2" in "concurrency/MyKeOS" = "HOL-TestGen" +
+session "HOL-TestGen-MyKeOS2" in "concurrency/MyKeOS2" = "HOL-TestGen" +
   options [quick_and_dirty(*, document = pdf,document_variants="document:outline=/proof,/ML",document_output=output*)]
   theories 
     MyKeOS

src/ROOT

@@ -1,11 +1,16 @@
 
-session "HOL-TestGenLib" = HOL +
+session "HOL-TestGenLib" in "test" = "HOL-Library" +
   description {* HOL-TestGen Basic Libraries without Code-Generators and Testgenerator *}
+  (*directories "/cygdrive/c/Program Files (x86)/Isabelle HOL/Isabelle2021/hol-testgen-1.9.1/hol-testgen-1.9.1/src"*)
+
   theories
     "TestLib"
 
-session "HOL-TestGen" (main) = "HOL-TestGenLib" +
+session "HOL-TestGen" (main) in "main" = "HOL-TestGenLib" +
   description {* HOL-TestGen *}
+  (*directories "/cygdrive/c/Program Files (x86)/Isabelle HOL/Isabelle2021/hol-testgen-1.9.1/hol-testgen-1.9.1/src"*)
+  (*directories "../../../../Isabelle-linux/Isabelle2021-1/src/HOL"*)
+  directories "codegen_fsharp" "codegen_gdb"
   theories 
     "codegen_fsharp/Code_String_Fsharp"
     "codegen_fsharp/Code_Char_chr_Fsharp"

src/main/Old_SMT/old_smt_builtin.ML

@@ -0,0 +1,231 @@
+(*  Title:      HOL/Library/Old_SMT/old_smt_builtin.ML
+    Author:     Sascha Boehme, TU Muenchen
+
+Tables of types and terms directly supported by SMT solvers.
+*)
+
+signature OLD_SMT_BUILTIN =
+sig
+  (*for experiments*)
+  val filter_builtins: (typ -> bool) -> Proof.context -> Proof.context
+
+  (*built-in types*)
+  val add_builtin_typ: Old_SMT_Utils.class ->
+    typ * (typ -> string option) * (typ -> int -> string option) ->
+    Context.generic -> Context.generic
+  val add_builtin_typ_ext: typ * (typ -> bool) -> Context.generic ->
+    Context.generic
+  val dest_builtin_typ: Proof.context -> typ -> string option
+  val is_builtin_typ_ext: Proof.context -> typ -> bool
+
+  (*built-in numbers*)
+  val dest_builtin_num: Proof.context -> term -> (string * typ) option
+  val is_builtin_num: Proof.context -> term -> bool
+  val is_builtin_num_ext: Proof.context -> term -> bool
+
+  (*built-in functions*)
+  type 'a bfun = Proof.context -> typ -> term list -> 'a
+  type bfunr = string * int * term list * (term list -> term)
+  val add_builtin_fun: Old_SMT_Utils.class ->
+    (string * typ) * bfunr option bfun -> Context.generic -> Context.generic
+  val add_builtin_fun': Old_SMT_Utils.class -> term * string -> Context.generic ->
+    Context.generic
+  val add_builtin_fun_ext: (string * typ) * term list bfun ->
+    Context.generic -> Context.generic
+  val add_builtin_fun_ext': string * typ -> Context.generic -> Context.generic
+  val add_builtin_fun_ext'': string -> Context.generic -> Context.generic
+  val dest_builtin_fun: Proof.context -> string * typ -> term list ->
+    bfunr option
+  val dest_builtin_eq: Proof.context -> term -> term -> bfunr option
+  val dest_builtin_pred: Proof.context -> string * typ -> term list ->
+    bfunr option
+  val dest_builtin_conn: Proof.context -> string * typ -> term list ->
+    bfunr option
+  val dest_builtin: Proof.context -> string * typ -> term list -> bfunr option
+  val dest_builtin_ext: Proof.context -> string * typ -> term list ->
+    term list option
+  val is_builtin_fun: Proof.context -> string * typ -> term list -> bool
+  val is_builtin_fun_ext: Proof.context -> string * typ -> term list -> bool
+end
+
+structure Old_SMT_Builtin: OLD_SMT_BUILTIN =
+struct
+
+
+(* built-in tables *)
+
+datatype ('a, 'b) kind = Ext of 'a | Int of 'b
+
+type ('a, 'b) ttab = ((typ * ('a, 'b) kind) Ord_List.T) Old_SMT_Utils.dict 
+
+fun typ_ord ((T, _), (U, _)) =
+  let
+    fun tord (TVar _, Type _) = GREATER
+      | tord (Type _, TVar _) = LESS
+      | tord (Type (n, Ts), Type (m, Us)) =
+          if n = m then list_ord tord (Ts, Us)
+          else Term_Ord.typ_ord (T, U)
+      | tord TU = Term_Ord.typ_ord TU
+  in tord (T, U) end
+
+fun insert_ttab cs T f =
+  Old_SMT_Utils.dict_map_default (cs, [])
+    (Ord_List.insert typ_ord (perhaps (try Logic.varifyT_global) T, f))
+
+fun merge_ttab ttabp =
+  Old_SMT_Utils.dict_merge (Ord_List.merge typ_ord) ttabp
+
+fun lookup_ttab ctxt ttab T =
+  let fun match (U, _) = Sign.typ_instance (Proof_Context.theory_of ctxt) (T, U)
+  in
+    get_first (find_first match)
+      (Old_SMT_Utils.dict_lookup ttab (Old_SMT_Config.solver_class_of ctxt))
+  end
+
+type ('a, 'b) btab = ('a, 'b) ttab Symtab.table
+
+fun insert_btab cs n T f =
+  Symtab.map_default (n, []) (insert_ttab cs T f)
+
+fun merge_btab btabp = Symtab.join (K merge_ttab) btabp
+
+fun lookup_btab ctxt btab (n, T) =
+  (case Symtab.lookup btab n of
+    NONE => NONE
+  | SOME ttab => lookup_ttab ctxt ttab T)
+
+type 'a bfun = Proof.context -> typ -> term list -> 'a
+
+type bfunr = string * int * term list * (term list -> term)
+
+structure Builtins = Generic_Data
+(
+  type T =
+    (typ -> bool, (typ -> string option) * (typ -> int -> string option)) ttab *
+    (term list bfun, bfunr option bfun) btab
+  val empty = ([], Symtab.empty)
+  val extend = I
+  fun merge ((t1, b1), (t2, b2)) = (merge_ttab (t1, t2), merge_btab (b1, b2))
+)
+
+fun filter_ttab keep_T = map (apsnd (filter (keep_T o fst)))
+
+fun filter_builtins keep_T =
+  Context.proof_map (Builtins.map (fn (ttab, btab) =>
+    (filter_ttab keep_T ttab, Symtab.map (K (filter_ttab keep_T)) btab)))
+
+
+(* built-in types *)
+
+fun add_builtin_typ cs (T, f, g) =
+  Builtins.map (apfst (insert_ttab cs T (Int (f, g))))
+
+fun add_builtin_typ_ext (T, f) =
+  Builtins.map (apfst (insert_ttab Old_SMT_Utils.basicC T (Ext f)))
+
+fun lookup_builtin_typ ctxt =
+  lookup_ttab ctxt (fst (Builtins.get (Context.Proof ctxt)))
+
+fun dest_builtin_typ ctxt T =
+  (case lookup_builtin_typ ctxt T of
+    SOME (_, Int (f, _)) => f T
+  | _ => NONE) 
+
+fun is_builtin_typ_ext ctxt T =
+  (case lookup_builtin_typ ctxt T of
+    SOME (_, Int (f, _)) => is_some (f T)
+  | SOME (_, Ext f) => f T
+  | NONE => false)
+
+
+(* built-in numbers *)
+
+fun dest_builtin_num ctxt t =
+  (case try HOLogic.dest_number t of
+    NONE => NONE
+  | SOME (T, i) =>
+      if i < 0 then NONE else
+        (case lookup_builtin_typ ctxt T of
+          SOME (_, Int (_, g)) => g T i |> Option.map (rpair T)
+        | _ => NONE))
+
+val is_builtin_num = is_some oo dest_builtin_num
+
+fun is_builtin_num_ext ctxt t =
+  (case try HOLogic.dest_number t of
+    NONE => false
+  | SOME (T, _) => is_builtin_typ_ext ctxt T)
+
+
+(* built-in functions *)
+
+fun add_builtin_fun cs ((n, T), f) =
+  Builtins.map (apsnd (insert_btab cs n T (Int f)))
+
+fun add_builtin_fun' cs (t, n) =
+  let
+    val c as (m, T) = Term.dest_Const t
+    fun app U ts = Term.list_comb (Const (m, U), ts)
+    fun bfun _ U ts = SOME (n, length (Term.binder_types T), ts, app U)
+  in add_builtin_fun cs (c, bfun) end
+
+fun add_builtin_fun_ext ((n, T), f) =
+  Builtins.map (apsnd (insert_btab Old_SMT_Utils.basicC n T (Ext f)))
+
+fun add_builtin_fun_ext' c = add_builtin_fun_ext (c, fn _ => fn _ => I)
+
+fun add_builtin_fun_ext'' n context =
+  let val thy = Context.theory_of context
+  in add_builtin_fun_ext' (n, Sign.the_const_type thy n) context end
+
+fun lookup_builtin_fun ctxt =
+  lookup_btab ctxt (snd (Builtins.get (Context.Proof ctxt)))
+
+fun dest_builtin_fun ctxt (c as (_, T)) ts =
+  (case lookup_builtin_fun ctxt c of
+    SOME (_, Int f) => f ctxt T ts
+  | _ => NONE)
+
+fun dest_builtin_eq ctxt t u =
+  let
+    val aT = TFree (Name.aT, @{sort type})
+    val c = (@{const_name HOL.eq}, aT --> aT --> @{typ bool})
+    fun mk ts = Term.list_comb (HOLogic.eq_const (Term.fastype_of (hd ts)), ts)
+  in
+    dest_builtin_fun ctxt c []
+    |> Option.map (fn (n, i, _, _) => (n, i, [t, u], mk))
+  end
+
+fun special_builtin_fun pred ctxt (c as (_, T)) ts =
+  if pred (Term.body_type T, Term.binder_types T) then
+    dest_builtin_fun ctxt c ts
+  else NONE
+
+fun dest_builtin_pred ctxt = special_builtin_fun (equal @{typ bool} o fst) ctxt
+
+fun dest_builtin_conn ctxt =
+  special_builtin_fun (forall (equal @{typ bool}) o (op ::)) ctxt
+
+fun dest_builtin ctxt c ts =
+  let val t = Term.list_comb (Const c, ts)
+  in
+    (case dest_builtin_num ctxt t of
+      SOME (n, _) => SOME (n, 0, [], K t)
+    | NONE => dest_builtin_fun ctxt c ts)
+  end
+
+fun dest_builtin_fun_ext ctxt (c as (_, T)) ts =    
+  (case lookup_builtin_fun ctxt c of
+    SOME (_, Int f) => f ctxt T ts |> Option.map (fn (_, _, us, _) => us)
+  | SOME (_, Ext f) => SOME (f ctxt T ts)
+  | NONE => NONE)
+
+fun dest_builtin_ext ctxt c ts =
+  if is_builtin_num_ext ctxt (Term.list_comb (Const c, ts)) then SOME []
+  else dest_builtin_fun_ext ctxt c ts
+
+fun is_builtin_fun ctxt c ts = is_some (dest_builtin_fun ctxt c ts)
+
+fun is_builtin_fun_ext ctxt c ts = is_some (dest_builtin_fun_ext ctxt c ts)
+
+end