1.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy Sun Jul 31 13:45:20 2022 +0200
1.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy Sun Jul 31 16:35:33 2022 +0200
1.3 @@ -45,11 +45,11 @@
1.4 signature PROG_EXPR =
1.5 sig
1.6 val eval_lhs: 'a -> string -> term -> 'b -> (string * term) option
1.7 - val eval_matches: string -> string -> term -> theory -> (string * term) option
1.8 + val eval_matches: string -> string -> term -> Proof.context -> (string * term) option
1.9 val matchsub: theory -> term -> term -> bool
1.10 - val eval_matchsub: string -> string -> term -> theory -> (string * term) option
1.11 + val eval_matchsub: string -> string -> term -> Proof.context -> (string * term) option
1.12 val eval_rhs: 'a -> string -> term -> 'b -> (string * term) option
1.13 - val eval_var: string -> string -> term -> theory -> (string * term) option
1.14 + val eval_var: string -> string -> term -> Proof.context -> (string * term) option
1.15
1.16 val or2list: term -> term
1.17
1.18 @@ -62,8 +62,8 @@
1.19 val even: int -> bool
1.20 val eval_is_even: string -> string -> term -> 'a -> (string * term) option
1.21 val eval_equ: string -> string -> term -> 'a -> (string * term) option
1.22 - val eval_ident: string -> string -> term -> theory -> (string * term) option
1.23 - val eval_equal: string -> string -> term -> theory -> (string * term) option
1.24 + val eval_ident: string -> string -> term -> Proof.context -> (string * term) option
1.25 + val eval_equal: string -> string -> term -> Proof.context -> (string * term) option
1.26 val eval_cancel: string -> string -> term -> 'a -> (string * term) option
1.27 val eval_argument_in: string -> string -> term -> 'a -> (string * term) option
1.28 val same_funid: term -> term -> bool
1.29 @@ -76,7 +76,7 @@
1.30 end
1.31
1.32 (**)
1.33 -structure Prog_Expr(**): PROG_EXPR =(**)
1.34 +structure Prog_Expr(**): PROG_EXPR(**) =
1.35 struct
1.36 (**)
1.37
1.38 @@ -98,16 +98,17 @@
1.39
1.40 (*. evaluate the predicate matches (match on whole term only) .*)
1.41 (*("matches",("Prog_Expr.matches", eval_matches "#matches_")):calc*)
1.42 -fun eval_matches (_:string) "Prog_Expr.matches" (t as Const (\<^const_name>\<open>Prog_Expr.matches\<close>, _) $ pat $ tst) thy =
1.43 - if TermC.matches thy tst pat
1.44 +fun eval_matches (_:string) "Prog_Expr.matches"
1.45 + (t as Const (\<^const_name>\<open>Prog_Expr.matches\<close>, _) $ pat $ tst) ctxt =
1.46 + if TermC.matches (Proof_Context.theory_of ctxt) tst pat
1.47 then
1.48 let
1.49 val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))
1.50 - in SOME (UnparseC.term_in_thy thy prop, prop) end
1.51 + in SOME (UnparseC.term_in_ctxt ctxt prop, prop) end
1.52 else
1.53 let
1.54 val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))
1.55 - in SOME (UnparseC.term_in_thy thy prop, prop) end
1.56 + in SOME (UnparseC.term_in_ctxt ctxt prop, prop) end
1.57 | eval_matches _ _ _ _ = NONE;
1.58
1.59 (*.does a pattern match some subterm ?.*)
1.60 @@ -126,22 +127,22 @@
1.61
1.62 (*("matchsub",("Prog_Expr.matchsub", eval_matchsub "#matchsub_")):calc*)
1.63 fun eval_matchsub (_:string) "Prog_Expr.matchsub"
1.64 - (t as Const (\<^const_name>\<open>Prog_Expr.matchsub\<close>, _) $ pat $ tst) thy =
1.65 - if matchsub thy tst pat
1.66 + (t as Const (\<^const_name>\<open>Prog_Expr.matchsub\<close>, _) $ pat $ tst) ctxt =
1.67 + if matchsub (Proof_Context.theory_of ctxt) tst pat
1.68 then
1.69 let val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))
1.70 - in SOME (UnparseC.term_in_thy thy prop, prop) end
1.71 + in SOME (UnparseC.term_in_ctxt ctxt prop, prop) end
1.72 else
1.73 let val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))
1.74 - in SOME (UnparseC.term_in_thy thy prop, prop) end
1.75 + in SOME (UnparseC.term_in_ctxt ctxt prop, prop) end
1.76 | eval_matchsub _ _ _ _ = NONE;
1.77
1.78 (*get the variables in an isabelle-term*)
1.79 (*("Vars" ,("Prog_Expr.Vars" , eval_var "#Vars_")):calc*)
1.80 -fun eval_var (thmid:string) "Prog_Expr.Vars" (t as (Const _ $ arg)) thy =
1.81 +fun eval_var (thmid:string) "Prog_Expr.Vars" (t as (Const _ $ arg)) ctxt =
1.82 let
1.83 val t' = ((TermC.list2isalist HOLogic.realT) o TermC.vars) t;
1.84 - val thmId = thmid ^ UnparseC.term_in_thy thy arg;
1.85 + val thmId = thmid ^ UnparseC.term_in_ctxt ctxt arg;
1.86 in SOME (thmId, HOLogic.Trueprop $ (TermC.mk_equality (t, t'))) end
1.87 | eval_var _ _ _ _ = NONE;
1.88
1.89 @@ -158,11 +159,9 @@
1.90 SOME (UnparseC.term t ^ " = " ^ UnparseC.term r,
1.91 HOLogic.Trueprop $ (TermC.mk_equality (t, r)))
1.92 | eval_rhs _ _ _ _ = NONE;
1.93 -(*\\------------------------- from Prog_Expr.thy-------------------------------------------------//*)
1.94
1.95 -(*//------------------------- from Atools.thy------------------------------------------------\\*)
1.96 +
1.97 fun occurs_in v t = member op = (((map strip_thy) o TermC.ids2str) t) (Term.term_name v);
1.98 -
1.99 (*("occurs_in", ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in ""))*)
1.100 fun eval_occurs_in _ "Prog_Expr.occurs_in" (p as (Const (\<^const_name>\<open>occurs_in\<close>, _) $ v $ t)) _ =
1.101 ((*tracing("#>@ eval_occurs_in: v= "^(UnparseC.term v));
1.102 @@ -287,15 +286,15 @@
1.103 the arguments: thus special handling by 'fun eval_binop'*)
1.104 (*("ident" ,("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_")):calc*)
1.105 fun eval_ident (thmid:string) "Prog_Expr.ident" (t as
1.106 - (Const _(*op0, t0*) $ t1 $ t2 )) thy =
1.107 + (Const _(*op0, t0*) $ t1 $ t2 )) ctxt =
1.108 if t1 = t2
1.109 then SOME (TermC.mk_thmid thmid
1.110 - ("(" ^ (UnparseC.term_in_thy thy t1) ^ ")")
1.111 - ("(" ^ (UnparseC.term_in_thy thy t2) ^ ")"),
1.112 + ("(" ^ (UnparseC.term_in_ctxt ctxt t1) ^ ")")
1.113 + ("(" ^ (UnparseC.term_in_ctxt ctxt t2) ^ ")"),
1.114 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
1.115 else SOME (TermC.mk_thmid thmid
1.116 - ("(" ^ (UnparseC.term_in_thy thy t1) ^ ")")
1.117 - ("(" ^ (UnparseC.term_in_thy thy t2) ^ ")"),
1.118 + ("(" ^ (UnparseC.term_in_ctxt ctxt t1) ^ ")")
1.119 + ("(" ^ (UnparseC.term_in_ctxt ctxt t2) ^ ")"),
1.120 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
1.121 | eval_ident _ _ _ _ = NONE;
1.122 (* TODO
1.123 @@ -320,11 +319,11 @@
1.124 (* evaluate identity of terms, which stay ready for further evaluation;
1.125 thus returns False only for atoms *)
1.126 (*("equal" ,(\<^const_name>\<open>HOL.eq\<close>, Prog_Expr.eval_equal "#equal_")):calc*)
1.127 -fun eval_equal (thmid : string) \<^const_name>\<open>HOL.eq\<close> (t as (Const _(*op0,t0*) $ t1 $ t2 )) thy =
1.128 +fun eval_equal (thmid : string) \<^const_name>\<open>HOL.eq\<close> (t as (Const _(*op0,t0*) $ t1 $ t2 )) ctxt =
1.129 if t1 = t2
1.130 then
1.131 SOME (TermC.mk_thmid thmid
1.132 - ("(" ^ UnparseC.term_in_thy thy t1 ^ ")") ("(" ^ UnparseC.term_in_thy thy t2 ^ ")"),
1.133 + ("(" ^ UnparseC.term_in_ctxt ctxt t1 ^ ")") ("(" ^ UnparseC.term_in_ctxt ctxt t2 ^ ")"),
1.134 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
1.135 else
1.136 (case (TermC.is_atom t1, TermC.is_atom t2) of
1.137 @@ -332,7 +331,7 @@
1.138 if TermC.variable_constant_pair (t1, t2)
1.139 then NONE
1.140 else SOME (TermC.mk_thmid thmid
1.141 - ("(" ^ UnparseC.term_in_thy thy t1 ^ ")") ("(" ^ UnparseC.term_in_thy thy t2 ^ ")"),
1.142 + ("(" ^ UnparseC.term_in_ctxt ctxt t1 ^ ")") ("(" ^ UnparseC.term_in_ctxt ctxt t2 ^ ")"),
1.143 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
1.144 | _ => NONE) (* NOT is_atom t1,t2 --> rew_sub *)
1.145 | eval_equal _ _ _ _ = NONE; (* error-exit *)