1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml Sat Oct 08 19:17:24 2022 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml Sun Oct 09 06:53:03 2022 +0200
1.3 @@ -17,6 +17,7 @@
1.4 val sub_at: path -> term -> term
1.5 val go_up: path -> term -> term
1.6
1.7 + val perm: term -> term -> bool (*old original Isabelle code*)
1.8 val contains_Var: term -> bool
1.9 val dest_binop_typ: typ -> typ * typ * typ
1.10 val dest_equals: term -> term * term
1.11 @@ -71,19 +72,21 @@
1.12
1.13 val matches: theory -> term -> term -> bool
1.14
1.15 - val parseNEW: Proof.context -> string -> term option
1.16 - val parseNEW': Proof.context -> string -> term
1.17 - val parseNEW'': theory -> string -> term
1.18 - val parse_strict: theory -> string -> term (*still required for CAS_Cmd*)
1.19 - val parse_strict_PIDE: theory -> string -> term
1.20 -
1.21 - val parse_patt: theory -> string -> term (*still required why ??? *)
1.22 - val parse_patt_PIDE: theory -> string -> term
1.23 - val perm: term -> term -> bool
1.24 + val parseNEW: Proof.context -> string -> term option(*old version to be eliminated*)
1.25 + val parseNEW': Proof.context -> string -> term (*old version to be eliminated*)
1.26 + val parseNEW'': theory -> string -> term (*old version to be eliminated*)
1.27 + val parse_strict: theory -> string -> term (*to be replaced by parse, typ_a2real for CAS_Cmd*)
1.28 + val parse_strict_PIDE: theory -> string -> term (*to be 1.replaced by parse_patt*)
1.29 +(*goal*)val parse: Proof.context -> string -> term
1.30 + val parse_patt_PIDE: theory -> string -> term (*rename to parse_patt*)
1.31 +(*goal*)val parse_patt: theory -> string -> term (*with typ_a2real still for tests *)
1.32 + (*for test/* *)
1.33 +(*goal*)val parse_test: Proof.context -> string -> term
1.34 +(*goal*)val parse_patt_test: theory -> string -> term
1.35 + val str2term: string -> term (*to be replaced by parse/_patt in src*, by parse/_patt in test/**)
1.36
1.37 val str_of_free_opt: term -> string option
1.38 val str_of_int: int -> string
1.39 - val str2term: string -> term
1.40 val strip_imp_prems': term -> term option
1.41 val subst_atomic_all: LibraryC.subst -> term -> bool * term
1.42 val term_detail2str: term -> string
1.43 @@ -545,7 +548,10 @@
1.44 | typ_a2real (Abs(s,T,t)) = Abs(s, T, typ_a2real t)
1.45 | typ_a2real (t1 $ t2) = (typ_a2real t1) $ (typ_a2real t2);
1.46
1.47 -(*WN110317 parseNEW will replace parse after introduction of ctxt completed*)
1.48 +
1.49 +(*** parse ***)
1.50 +
1.51 +(*/----- old versions to be eliminated -------------------------------------------------------\*)
1.52 fun parseNEW ctxt str = \<^try>\<open>Syntax.read_term ctxt str\<close>;
1.53 fun parseNEW' ctxt str =
1.54 case parseNEW ctxt str of
1.55 @@ -555,22 +561,38 @@
1.56 case parseNEW (Proof_Context.init_global thy) str of
1.57 SOME t => t
1.58 | NONE => raise TERM ("NO parseNEW'' for " ^ str, [])
1.59 +(*\----- old versions to be eliminated -------------------------------------------------------/*)
1.60
1.61 -fun parse_strict thy str = typ_a2real (Syntax.read_term_global thy str); (*still required for CAS_Cmd*)
1.62 +(* to be replaced by parse-test..*)
1.63 +fun parse_strict thy str = typ_a2real (Syntax.read_term_global thy str); (*still for CAS_Cmd*)
1.64 +(* to be replaced by parse..*)
1.65 fun parse_strict_PIDE thy str = (*typ_a2real*) (Syntax.read_term_global thy str);
1.66 -
1.67 -(* parse term patterns; Var ("v",_), i.e. "?v", are required for instantiation
1.68 - WN130613 probably compare to
1.69 - http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg04249.html*)
1.70 +fun parse ctxt str = Syntax.read_term_global (Proof_Context.theory_of ctxt) str;
1.71 +(* parse term patterns; Var ("v",_), i.e. "?v", are required for instantiation *)
1.72 +(*rename to parse_patt..*)
1.73 +fun parse_patt_PIDE thy str = (thy, str)
1.74 + |>> Proof_Context.init_global
1.75 + |-> Proof_Context.read_term_pattern
1.76 fun parse_patt thy str = (thy, str)
1.77 |>> Proof_Context.init_global
1.78 |-> Proof_Context.read_term_pattern
1.79 - |> typ_a2real; (*TODO drop*)
1.80 -fun parse_patt_PIDE thy str = (thy, str)
1.81 +(**)|> typ_a2real; (** )TODO drop*)
1.82 +
1.83 +(** parse in test/* **)
1.84 +(*
1.85 + This bypasses building ctxt at the begin of a calculation
1.86 + and thus borrows adapt_to_type (used for pre-parsed terms from Know_Store).
1.87 +*)
1.88 +fun parse_test ctxt str = str
1.89 + |> Syntax.read_term_global (Proof_Context.theory_of ctxt)
1.90 + |> Model_Pattern.adapt_term_to_type ctxt
1.91 +fun parse_patt_test thy str = (thy, str)
1.92 |>> Proof_Context.init_global
1.93 |-> Proof_Context.read_term_pattern
1.94 +(**)|> typ_a2real; (** )TODO drop*)
1.95 fun str2term str = parse_patt (ThyC.get_theory "Isac_Knowledge") str
1.96
1.97 +
1.98 fun is_atom (Const _) = true
1.99 | is_atom (Free _) = true
1.100 | is_atom (Var _) = true