1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml Mon Jun 21 22:08:01 2021 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml Sun Jul 18 18:15:27 2021 +0200
1.3 @@ -26,17 +26,21 @@
1.4 val inst_abs: term -> term
1.5 val inst_bdv: (term * term) list -> term -> term
1.6
1.7 + val mk_frac: typ -> int * (int * int) -> term
1.8 + val numerals_to_Free: term -> term
1.9 val term_of_num: typ -> int -> term
1.10 val num_of_term: term -> int
1.11 + val to_string: term -> string
1.12 val int_of_str: string -> int
1.13 val isastr_of_int: int -> string
1.14 - val int_opt_of_string: string -> int option (* belongs to TermC *)
1.15 + val int_opt_of_string: string -> int option
1.16
1.17 val isalist2list: term -> term list
1.18 val list2isalist: typ -> term list -> term
1.19 val isapair2pair: term -> term * term (* rename to dest_pair, compare HOLogic.dest_string *)
1.20
1.21 val is_atom: term -> bool
1.22 + val string_of_atom: term -> string
1.23 val is_const: term -> bool
1.24 val is_variable: term -> bool
1.25 val is_bdv: string -> bool
1.26 @@ -50,6 +54,7 @@
1.27 val dest_listT: typ -> typ
1.28 val is_num: term -> bool
1.29 val is_num': string -> bool
1.30 + val string_of_num: term -> string
1.31 val variable_constant_pair: term * term -> bool
1.32
1.33 val mk_add: term -> term -> term
1.34 @@ -63,7 +68,6 @@
1.35 val mk_var_op_num: term -> string -> typ -> typ -> int -> term
1.36
1.37 val matches: theory -> term -> term -> bool
1.38 - val parse_strict: theory -> string -> term
1.39 val parse: theory -> string -> cterm option
1.40 val parseN: theory -> string -> cterm option
1.41 val parseNEW: Proof.context -> string -> term option
1.42 @@ -89,13 +93,14 @@
1.43 val uminus_to_string: term -> term
1.44
1.45 val var2free: term -> term
1.46 - val vars: term -> term list (* recognises numerals, should replace "fun vars_of" *)
1.47 + val vars: term -> term list (* recognises numerals, should replace "fun vars_of" TODOO*)
1.48 val vars': term list -> term list
1.49 - val vars_of: term -> term list (* deprecated *)
1.50 + val vars_of: term -> term list (* deprecated TODOO: see differences in test/../termC.sml*)
1.51 val dest_list': term -> term list
1.52 val negates: term -> term -> bool
1.53
1.54 \<^isac_test>\<open>
1.55 + val mk_negative: typ -> term -> term
1.56 val scala_of_term: term -> string
1.57 val atomtyp(*<-- atom_typ TODO*): typ -> unit
1.58 val atomty: term -> unit
1.59 @@ -246,13 +251,46 @@
1.60 val int_of_str = Value.parse_int;
1.61
1.62 val int_opt_of_string = ThmC_Def.int_opt_of_string
1.63 +fun is_num' str = case int_opt_of_string str of SOME _ => true | NONE => false;
1.64
1.65 -fun is_num' str = case int_opt_of_string str of SOME _ => true | NONE => false;
1.66 -fun is_num (Free (s, _)) = if is_num' s then true else false | is_num _ = false;
1.67 -fun term_of_num ntyp n = Free (str_of_int n, ntyp);
1.68 -fun num_of_term (t as (Free (istr, _))) =
1.69 - (case int_opt_of_string istr of SOME i => i | NONE => raise TERM ("num_of_term: NOT int ", [t]))
1.70 - | num_of_term t = raise TERM ("num_of_term: NOT Free ", [t])
1.71 +fun is_num (Const ("Num.numeral_class.numeral", _) $ _) = true
1.72 + | is_num (Const ("Groups.uminus_class.uminus", _) $
1.73 + (Const ("Num.numeral_class.numeral", _) $ _)) = true
1.74 + | is_num (Const ("Groups.one_class.one", _)) = true
1.75 + | is_num (Const ("Groups.uminus_class.uminus", _) $ Const ("Groups.one_class.one", _)) = true
1.76 + | is_num (Const ("Groups.zero_class.zero", _)) = true
1.77 + | is_num (Const ("Groups.uminus_class.uminus", _) $ Const ("Groups.zero_class.zero", _)) = true
1.78 + | is_num _ = false;
1.79 +
1.80 +fun string_of_num n = (n |> HOLogic.dest_number |> snd |> string_of_int)
1.81 +
1.82 +fun mk_negative T t = Const ("Groups.uminus_class.uminus", T --> T) $ t
1.83 +fun mk_frac T (sg, (i1, i2)) =
1.84 + if sg = 1 then
1.85 + if i2 = 1 then HOLogic.mk_number T i1
1.86 + else Const ("Rings.divide_class.divide", T --> T --> T) $
1.87 + HOLogic.mk_number T i1 $ HOLogic.mk_number T i2
1.88 + else (*take negative*)
1.89 + if i2 = 1 then mk_negative T (HOLogic.mk_number T i1)
1.90 + else Const ("Rings.divide_class.divide", T --> T --> T) $
1.91 + mk_negative T (HOLogic.mk_number T i1) $ HOLogic.mk_number T i2
1.92 +
1.93 +val numerals_to_Free = (* Makarius 100308 *)
1.94 + let
1.95 + fun dest_num t =
1.96 + (case try HOLogic.dest_number t of
1.97 + SOME (T, i) => SOME (Free (signed_string_of_int i, T))
1.98 + | NONE => NONE);
1.99 + fun to_str (Abs (x, T, b)) = Abs (x, T, to_str b)
1.100 + | to_str (t as (u1 $ u2)) =
1.101 + (case dest_num t of SOME t' => t' | NONE => to_str u1 $ to_str u2)
1.102 + | to_str t = perhaps dest_num t;
1.103 + in to_str end
1.104 +
1.105 +val term_of_num = HOLogic.mk_number;
1.106 +fun num_of_term t = t |> HOLogic.dest_number |> snd;
1.107 +(* accomodate string-representation for int to term-orders *)
1.108 +fun to_string t = t |> num_of_term |> LibraryC.string_of_int'
1.109
1.110 fun is_const (Const _) = true | is_const _ = false;
1.111 fun is_variable (t as Free _) = not (is_num t)
1.112 @@ -273,7 +311,7 @@
1.113 fun vars t =
1.114 let
1.115 fun scan vs (Const _) = vs
1.116 - | scan vs (t as Free (s, _)) = if is_num' s then vs else t :: vs
1.117 + | scan vs (t as Free _) = (*if is_num' s then vs else*) t :: vs
1.118 | scan vs (t as Var _) = t :: vs
1.119 | scan vs (Bound _) = vs
1.120 | scan vs (Abs (_, _, t)) = scan vs t
1.121 @@ -436,10 +474,10 @@
1.122 fun mk_factroot op_(*=thy.sqrt*) T fact root =
1.123 Const (\<^const_name>\<open>times\<close>, [T, T] ---> T) $ (term_of_num T fact) $
1.124 (Const (op_, T --> T) $ term_of_num T root);
1.125 -fun mk_var_op_num v op_ optype ntyp n = Const (op_, optype) $ v $ Free (str_of_int n, ntyp);
1.126 -fun mk_num_op_var v op_ optype ntyp n = Const (op_, optype) $ Free (str_of_int n, ntyp) $ v;
1.127 +fun mk_var_op_num v op_ optype ntyp n = Const (op_, optype) $ v $ HOLogic.mk_number ntyp n;
1.128 +fun mk_num_op_var v op_ optype ntyp n = Const (op_, optype) $ HOLogic.mk_number ntyp n $ v;
1.129 fun mk_num_op_num T1 T2 (op_, Top) n1 n2 =
1.130 - Const (op_, Top) $ Free (str_of_int n1, T1) $ Free (str_of_int n2, T2);
1.131 + Const (op_, Top) $ HOLogic.mk_number T1 n1 $ HOLogic.mk_number T2 n2;
1.132 fun mk_thmid thmid n1 n2 =
1.133 thmid ^ (strip_thy n1) ^ "_" ^ (strip_thy n2);
1.134 fun mk_add t1 t2 =
1.135 @@ -529,11 +567,13 @@
1.136 fun parse_patt thy str = (thy, str)
1.137 |>> ThyC.to_ctxt
1.138 |-> Proof_Context.read_term_pattern
1.139 - |> numbers_to_string (*TODO drop*)
1.140 +(*|> numbers_to_string TODO drop*)
1.141 |> typ_a2real; (*TODO drop*)
1.142 fun str2term str = parse_patt (ThyC.get_theory "Isac_Knowledge") str
1.143
1.144 -fun is_atom (Const ("Float.Float",_) $ _) = true
1.145 +fun is_atom (Const ("Num.numeral_class.numeral", _) $ _) = true
1.146 + | is_atom (Const ("Groups.one_class.one", _)) = true
1.147 + | is_atom (Const ("Groups.zero_class.zero", _)) = true
1.148 | is_atom (Const _) = true
1.149 | is_atom (Free _) = true
1.150 | is_atom (Var _) = true
1.151 @@ -574,7 +614,7 @@
1.152 val poly_consts = (* TODO: adopt syntax-const from Isabelle*)
1.153 [\<^const_name>\<open>plus\<close>, \<^const_name>\<open>minus\<close>,
1.154 \<^const_name>\<open>divide\<close>, \<^const_name>\<open>times\<close>,
1.155 - \<^const_name>\<open>powr\<close>];
1.156 + \<^const_name>\<open>powr\<close>],
1.157 (* treat Free, Const, Var as variables in polynomials *)
1.158 fun vars_of t =
1.159 let
1.160 @@ -617,4 +657,4 @@
1.161 in trm' end
1.162
1.163
1.164 -end
1.165 \ No newline at end of file
1.166 +end