1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml Wed Jan 11 06:06:12 2023 +0100
1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml Wed Jan 11 09:23:18 2023 +0100
1.3 @@ -99,21 +99,24 @@
1.4 val dest_list': term -> term list
1.5 val negates: term -> term -> bool
1.6
1.7 -\<^isac_test>\<open>
1.8 + val contains_one_of: thm * (string * typ) list -> bool
1.9 + val contains_Const_typeless: term list -> term -> bool
1.10 + val sym_trm : term -> term (* unused code, kept as hints to design ideas *)
1.11 +
1.12 +(*isac_test*)
1.13 val mk_negative: typ -> term -> term
1.14 + val free2var: term -> term
1.15 val scala_of_term: term -> string
1.16 - val atomtyp(*<-- atom_typ TODO*): typ -> unit
1.17 +
1.18 +(*val atom_typ: typ -> unit RENAME*)
1.19 + val atomtyp: typ -> unit
1.20 val atomty: term -> unit
1.21 val atomw: term -> unit
1.22 val atomt: term -> unit
1.23 val atomwy: term -> unit
1.24 - val atomty_thy: ThyC.id -> term -> unit
1.25 - val free2var: term -> term
1.26 +
1.27 +\<^isac_test>\<open>
1.28 \<close>
1.29 - val contains_one_of: thm * (string * typ) list -> bool
1.30 - val contains_Const_typeless: term list -> term -> bool
1.31 -(*----- unused code, kept as hints to design ideas ---------------------------------------------*)
1.32 - val sym_trm : term -> term
1.33 end
1.34
1.35 (**)
1.36 @@ -148,8 +151,7 @@
1.37 handle Pattern.MATCH => false
1.38
1.39 (** transform typ / term to a String to be parsed by Scala after transport via libisabelle **)
1.40 -
1.41 -\<^isac_test>\<open>
1.42 +(*isac_test*)
1.43 fun scala_of_typ (Type (s, typs)) =
1.44 enclose "Type(" ")" (quote s ^ ", " ^
1.45 (typs |> map scala_of_typ |> commas |> enclose "List(" ")"))
1.46 @@ -202,40 +204,28 @@
1.47 fun atomw t = writeln ("\n*** -------------" ^ ato t 0 ^ "\n***");
1.48 fun atomt t = tracing ("\n*** -------------" ^ ato t 0 ^ "\n***");
1.49 end;
1.50 +
1.51 +\<^isac_test>\<open>
1.52 \<close>
1.53
1.54 fun term_detail2str t =
1.55 - let
1.56 - fun ato (Const (a, T)) n = "\n*** " ^ indent n ^ "Const (" ^ a ^ ", " ^ UnparseC.typ T ^ ")"
1.57 - | ato (Free (a, T)) n = "\n*** " ^ indent n ^ "Free (" ^ a ^ ", " ^ UnparseC.typ T ^ ")"
1.58 + let
1.59 + val ctxt = "Isac_Knowledge" |> Know_Store.get_via_last_thy |> Proof_Context.init_global
1.60 + fun ato (Const (a, T)) n = "\n*** " ^ indent n ^ "Const (" ^ a ^ ", " ^ UnparseC.typ_in_ctxt ctxt T ^ ")"
1.61 + | ato (Free (a, T)) n = "\n*** " ^ indent n ^ "Free (" ^ a ^ ", " ^ UnparseC.typ_in_ctxt ctxt T ^ ")"
1.62 | ato (Var ((a, i), T)) n =
1.63 - "\n*** " ^ indent n ^ "Var ((" ^ a ^ ", " ^ string_of_int i ^ "), " ^ UnparseC.typ T ^ ")"
1.64 + "\n*** " ^ indent n ^ "Var ((" ^ a ^ ", " ^ string_of_int i ^ "), " ^ UnparseC.typ_in_ctxt ctxt T ^ ")"
1.65 | ato (Bound i) n = "\n*** " ^ indent n ^ "Bound " ^ string_of_int i
1.66 | ato (Abs(a, T, body)) n =
1.67 - "\n*** " ^ indent n ^ "Abs (" ^ a ^ ", " ^ UnparseC.typ T ^ ",.." ^ ato body (n + 1)
1.68 + "\n*** " ^ indent n ^ "Abs (" ^ a ^ ", " ^ UnparseC.typ_in_ctxt ctxt T ^ ",.." ^ ato body (n + 1)
1.69 | ato (f $ t) n = ato f n ^ ato t (n + 1)
1.70 in "\n*** " ^ ato t 0 ^ "\n***" end;
1.71
1.72 -\<^isac_test>\<open>
1.73 -fun term_detail2str_thy thy t =
1.74 - let
1.75 - fun ato (Const (a, T)) n =
1.76 - "\n*** " ^ indent n ^ "Const (" ^ a ^ ", " ^ UnparseC.typ_by_thyID thy T ^ ")"
1.77 - | ato (Free (a, T)) n =
1.78 - "\n*** " ^ indent n ^ "Free (" ^ a ^ ", " ^ UnparseC.typ_by_thyID thy T ^ ")"
1.79 - | ato (Var ((a, i), T)) n =
1.80 - "\n*** " ^ indent n ^ "Var ((" ^ a ^ ", " ^ string_of_int i ^ "), " ^
1.81 - UnparseC.typ_by_thyID thy T ^ ")"
1.82 - | ato (Bound i) n =
1.83 - "\n*** " ^ indent n ^ "Bound " ^ string_of_int i
1.84 - | ato (Abs(a, T, body)) n =
1.85 - "\n*** " ^ indent n ^ "Abs (" ^ a ^ ", " ^ UnparseC.typ_by_thyID thy T ^ ",.." ^
1.86 - ato body (n + 1)
1.87 - | ato (f $ t) n = ato f n ^ ato t (n + 1)
1.88 - in "\n*** " ^ ato t 0 ^ "\n***" end;
1.89 +(*isac_test*)
1.90 fun atomwy t = (writeln o term_detail2str) t;
1.91 fun atomty t = (tracing o term_detail2str) t;
1.92 -fun atomty_thy thy t = (tracing o (term_detail2str_thy thy)) t;
1.93 +
1.94 +\<^isac_test>\<open>
1.95 \<close>
1.96
1.97 (* contains the term a VAR(("*",_),_) ? *)
1.98 @@ -375,7 +365,7 @@
1.99 | var2free (Abs(s, T, t)) = Abs(s, T, var2free t)
1.100 | var2free (t1 $ t2) = (var2free t1) $ (var2free t2);
1.101
1.102 -\<^isac_test>\<open>
1.103 +(*isac_test*)
1.104 (* Logic.varify does NOT take care of 'Free ("1", _)'*)
1.105 fun free2var (t as Const _) = t
1.106 | free2var (t as Free (s, T)) = if is_num' s then t else Var ((s, 0), T)
1.107 @@ -383,6 +373,8 @@
1.108 | free2var (t as Bound _) = t
1.109 | free2var (Abs (s, T, t)) = Abs (s, T, free2var t)
1.110 | free2var (t1 $ t2) = (free2var t1) $ (free2var t2);
1.111 +
1.112 +\<^isac_test>\<open>
1.113 \<close>
1.114
1.115 fun mk_listT T = Type (\<^type_name>\<open>list\<close>, [T]);