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