1.1 --- a/src/Tools/isac/calcelems.sml Tue Mar 13 15:04:27 2018 +0100
1.2 +++ b/src/Tools/isac/calcelems.sml Thu Mar 15 10:17:44 2018 +0100
1.3 @@ -1,16 +1,272 @@
1.4 (* elements of calculations.
1.5 they are partially held in association lists as ref's for
1.6 - switching language levels (meta-string, object-values).
1.7 - in order to keep these ref's during re-evaluation of code,
1.8 + switching language levels (meta-string, object-values).
1.9 + in order to keep these ref's during re-evaluation of code,
1.10 they are defined here at the beginning of the code.
1.11 Author: Walther Neuper 2003
1.12 (c) copyright due to lincense terms
1.13 *)
1.14
1.15 -(*
1.16 -structure CalcElems =
1.17 +signature CALC_ELEMENT =
1.18 + sig
1.19 + type eval_fn (*= string -> term -> theory -> (string * term) option*)
1.20 + type rew_ord (*= rew_ord' * rew_ord_*)
1.21 + eqtype errpatID
1.22 + type calc (*= prog_calcID * cal*)
1.23 + datatype rule = Cal1 of string * eval_fn | Calc of string * eval_fn | Erule | Rls_ of rls
1.24 + | Thm of string * thm
1.25 + and scr
1.26 + = EmptyScr
1.27 + | Prog of term
1.28 + | Rfuns of
1.29 + {attach_form: rule list list -> term -> term -> (rule * (term * term list)) list,
1.30 + init_state: term -> term * term * rule list list * (rule * (term * term list)) list,
1.31 + locate_rule: rule list list -> term -> rule -> (rule * (term * term list)) list,
1.32 + next_rule: rule list list -> term -> rule option,
1.33 + normal_form: term -> (term * term list) option}
1.34 + and rls =
1.35 + Erls
1.36 + | Rls of {calc: calc list, erls: rls, errpatts: errpatID list, id: string, preconds: term list,
1.37 + rew_ord: rew_ord, rules: rule list, scr: scr, srls: rls}
1.38 + | Rrls of {calc: calc list, erls: rls, errpatts: errpatID list,
1.39 + id: string, prepat: (term list * term) list, rew_ord: rew_ord, scr: scr}
1.40 + | Seq of {calc: calc list, erls: rls, errpatts: errpatID list, id: string, preconds: term list,
1.41 + rew_ord: rew_ord, rules: rule list, scr: scr, srls: rls}
1.42 +
1.43 + eqtype rls'
1.44 + eqtype theory'
1.45 + eqtype prog_calcID
1.46 + eqtype calID
1.47 + type cas_elem (*= term * (spec * generate_fn)*)
1.48 + type pbt (*= {cas: term option, guh: guh, init: pblID, mathauthors: string list,
1.49 + met: metID list, ppc: pat list, prls: rls, thy: theory, where_: term list}*)
1.50 + type ptyps (*= pbt ptyp list*)
1.51 + type metID (*= string list*)
1.52 + type pblID (*= string list*)
1.53 + type mets (*= met ptyp list*)
1.54 + type met (*= {calc: calc list,
1.55 + crls: rls, erls: rls, errpats: errpat list, guh: guh, init: pblID, mathauthors: string list,
1.56 + nrls: rls, ppc: pat list, pre: term list, prls: rls, rew_ord': rew_ord', scr: scr, srls: rls}*)
1.57 + datatype 'a ptyp = Ptyp of string * 'a list * 'a ptyp list
1.58 +
1.59 + type cal = calID * eval_fn
1.60 + type authors (*= string list*)
1.61 + type guh
1.62 + type subst (*= (term * term) list*)
1.63 + eqtype thyID
1.64 + type fillpat (*= fillpatID * term * errpatID*)
1.65 + datatype thydata
1.66 + = Hcal of {calc: calc, coursedesign: authors, guh: guh, mathauthors: authors}
1.67 + | Hord of {coursedesign: authors, guh: guh, mathauthors: authors, ord: subst -> term * term -> bool}
1.68 + | Hrls of {coursedesign: authors, guh: guh, mathauthors: authors, thy_rls: thyID * rls}
1.69 + | Hthm of {coursedesign: authors, fillpats: fillpat list, guh: guh, mathauthors: authors, thm: thm}
1.70 + | Html of {coursedesign: authors, guh: guh, html: string, mathauthors: authors}
1.71 + type theID (*= string list*)
1.72 + type rlss_elem (*= rls' * (theory' * rls)*)
1.73 + val merge_rlss: rlss_elem list * rlss_elem list -> rlss_elem list
1.74 + val rls_eq: (''a * ('b * 'c)) * (''a * ('d * 'e)) -> bool
1.75 + type calc_elem (*= prog_calcID * (calID * eval_fn)*)
1.76 + val calc_eq: calc_elem * calc_elem -> bool
1.77 + type spec (*= domID * pblID * metID*)
1.78 + val cas_eq: cas_elem * cas_elem -> bool
1.79 + val e_Ptyp: pbt ptyp
1.80 + val merge_ptyps: 'a ptyp list * 'a ptyp list -> 'a ptyp list
1.81 + val check_guhs_unique: bool Unsynchronized.ref
1.82 + val check_pblguh_unique: guh -> pbt ptyp list -> unit
1.83 + val insrt: pblID -> 'a -> string list -> 'a ptyp list -> 'a ptyp list
1.84 + val e_Mets: met ptyp
1.85 + val check_metguh_unique: guh -> met ptyp list -> unit
1.86 + val add_thydata: string list * string list -> thydata -> thydata ptyp list -> thydata ptyp list
1.87 + val get_py: 'a ptyp list -> pblID -> string list -> 'a
1.88 + val update_hthm: thydata -> fillpat list -> thydata
1.89 + val update_ptyps: string list -> string list -> 'a -> 'a ptyp list -> 'a ptyp list
1.90 + val e_rls: rls
1.91 + val e_rrls: rls
1.92 + val part2guh: theID -> guh
1.93 + val spec2str: string * string list * string list -> string
1.94 + val term_to_string''': theory -> term -> string
1.95 + val linefeed: string -> string
1.96 + val pbts2str: pbt list -> string
1.97 + val thes2str: thydata list -> string
1.98 + val theID2str: string list -> string
1.99 + val the2str: thydata -> string
1.100 + val Thy_Info_get_theory: string -> theory
1.101 + val string_of_typ: typ -> string
1.102 + val string_of_typ_thy: thyID -> typ -> string
1.103 + val term2str: term -> string
1.104 + val thy2ctxt: theory -> Proof.context
1.105 + val trace_calc: bool Unsynchronized.ref
1.106 + eqtype thmID
1.107 + type thm' (*= thmID * cterm'*)
1.108 + datatype lrd = D | L | R
1.109 + val trace_rewrite: bool Unsynchronized.ref
1.110 + val depth: int Unsynchronized.ref
1.111 + val t2str: theory -> term -> string
1.112 + val ts2str: theory -> term list -> string
1.113 + val terms2str: term list -> string
1.114 + val id_rls: rls -> string
1.115 + val rls2str: rls -> string
1.116 + val rep_rls: rls -> {calc: calc list, erls: rls, id: string, preconds: term list, rew_ord: rew_ord, rules: rule list, scr: scr, srls: rls}
1.117 + val string_of_thmI: thm -> string
1.118 + val rule2str: rule -> string
1.119 + val e_term: term
1.120 + val dummy_ord: subst -> term * term -> bool
1.121 + val theory2domID: theory -> theory'
1.122 + val assoc_thy: theory' -> theory
1.123 + val append_rls: string -> rls -> rule list -> rls
1.124 + eqtype domID
1.125 + val get_rules: rls -> rule list
1.126 + val id_rule: rule -> string
1.127 + eqtype cterm'
1.128 + val term_to_string': Proof.context -> term -> string
1.129 + val thy2ctxt': string -> Proof.context
1.130 + type rrlsstate = term * term * rule list list * (rule * (term * term list)) list
1.131 + type loc_ = lrd list
1.132 + val loc_2str: loc_ -> string
1.133 + val e_spec: spec
1.134 + val env2str: subst -> string
1.135 + val subst2str: subst -> string
1.136 + val termopt2str: term option -> string
1.137 + eqtype rew_ord'
1.138 + type thm'' (*= thmID * thm*)
1.139 + type rew_ord_ (*= subst -> term * term -> bool*)
1.140 + val metID2str: string list -> string
1.141 + val e_domID: domID
1.142 + val e_pblID: pblID
1.143 + val e_metID: metID
1.144 + val empty_spec: spec
1.145 + datatype ketype = Exp_ | Met_ | Pbl_ | Thy_
1.146 + type kestoreID (*= string list*)
1.147 + type errpat (*= errpatID * term list * thm list*)
1.148 + val app_py: 'a ptyp list -> ('a ptyp -> 'b) -> pblID -> string list -> 'b
1.149 + val ketype2str: ketype -> string
1.150 + val coll_pblguhs: pbt ptyp list -> guh list
1.151 + val coll_metguhs: met ptyp list -> guh list
1.152 + type pat (*= string * (term * term)*)
1.153 + val e_type: typ
1.154 + val theory2str: theory -> theory'
1.155 + val pats2str: pat list -> string
1.156 + val string_of_thy: theory -> theory'
1.157 + val theory2theory': theory -> theory'
1.158 + val maxthy: theory -> theory -> theory
1.159 + val e_evalfn: 'a -> term -> theory -> (string * term) option
1.160 + val assoc_rew_ord: string -> subst -> term * term -> bool
1.161 + eqtype filename
1.162 + val rule2str': rule -> string
1.163 + val lim_deriv: int Unsynchronized.ref
1.164 + val id_of_thm: rule -> string
1.165 + val isabthys: unit -> theory list
1.166 + val thyID_of_derivation_name: string -> string
1.167 + val partID': theory' -> string
1.168 + val Isac: 'a -> theory
1.169 + val theory'2thyID: theory' -> theory'
1.170 + val thm2guh: string * thyID -> thmID -> guh
1.171 + val thmID_of_derivation_name: string -> string
1.172 + val rls2guh: string * thyID -> rls' -> guh
1.173 + val eq_rule: rule * rule -> bool
1.174 + val e_rew_ordX: rew_ord
1.175 + val theID2guh: theID -> guh
1.176 + val thyID2theory': thyID -> thyID
1.177 + val e_rule: rule
1.178 + val scr2str: scr -> string
1.179 + val type2str: typ -> string
1.180 + eqtype fillpatID
1.181 + type pbt_ = string * (term * term)
1.182 + val e_rew_ord: subst -> term * term -> bool
1.183 + eqtype xml
1.184 + val cal2guh: string * thyID -> string -> guh
1.185 + val ketype2str': ketype -> string
1.186 + val str2ketype': string -> ketype
1.187 + val thmID_of_derivation_name': thm -> string
1.188 + val subst2str': subst -> string
1.189 + eqtype path
1.190 + val theID2thyID: theID -> thyID
1.191 + val thy2guh: theID -> guh
1.192 + val theory2thyID: theory -> thyID
1.193 + val thypart2guh: theID -> guh
1.194 + val ord2guh: string * thyID -> rew_ord' -> guh
1.195 + val update_hrls: thydata -> errpatID list -> thydata
1.196 + eqtype iterID
1.197 + eqtype calcID
1.198 + val thm''_of_thm: thm -> thm''
1.199 + val rew_ord': (rew_ord' * (subst -> term * term -> bool)) list Unsynchronized.ref
1.200 +
1.201 +(*---------------------- ^^^ make public on a minimalist way down to Build?Isac -----------------
1.202 + val Html_default: theID -> thydata
1.203 + val a_term: term
1.204 + val a_type: typ
1.205 + val assoc': (string * 'a) list * string -> 'a option
1.206 + type generate_fn = term list -> (term * term list) list
1.207 + val e_guh: guh
1.208 + val e_kestoreID: string list
1.209 + val e_met: met
1.210 + val e_pbt: pbt
1.211 + val e_pbt_: pbt_
1.212 + val e_rew_ord': rew_ord'
1.213 + val e_rew_ord_: subst -> term * term -> bool
1.214 + val e_rfuns: scr
1.215 + val e_rrlsstate: rrlsstate
1.216 + val e_scr: scr
1.217 + val e_subst: (term * term) list
1.218 + val e_theID: string list
1.219 + val e_thydata: thydata
1.220 + val empty_cterm': string
1.221 + val eq_thmI: (thmID * thm) * (thmID * 'a) -> bool
1.222 + val eq_thmI': (string * 'a) * (string * 'b) -> bool
1.223 + val eqrule: rule * rule -> bool
1.224 + val fill_parents: string list * string list -> thydata -> thydata ptyp
1.225 + val insert_fillpats: thydata ptyp list -> (pblID * fillpat list) list -> thydata ptyp list -> thydata ptyp list
1.226 + val insert_merge_rls: rlss_elem -> rlss_elem list -> rlss_elem list
1.227 + val insthy: 'a -> 'b * 'c -> 'b * ('a * 'c)
1.228 + val kestoreID2str: string list -> string
1.229 + val knowthys: unit -> theory list
1.230 + val ldr2str: lrd -> string
1.231 + val lim_rewrite: int Unsynchronized.ref
1.232 + val memrls: rule -> rls -> bool
1.233 + val merge_ids: rls -> rls -> string
1.234 + val merge_ptyps': 'a ptyp list -> 'a ptyp list -> 'a ptyp list
1.235 + val merge_rls: string -> rls -> rls -> rls
1.236 + val overwritelthy: theory -> (rls' * (string * rls)) list * (rls' * rls) list -> (rls' * (string * rls)) list
1.237 + val partID: theory -> string
1.238 + val pat2str: pat -> string
1.239 + val pblID2str: string list -> string
1.240 + val pbt2str: pbt -> string
1.241 + val progthys: unit -> theory list
1.242 + val remove_rls: string -> rls -> rule list -> rls
1.243 + val rep_rrls:
1.244 + rls -> {attach_form: rule list list -> term -> term -> (rule * (term * term list)) list,
1.245 + calc: calc list,
1.246 + erls: rls,
1.247 + errpatts: errpatID list,
1.248 + id: string,
1.249 + init_state: term -> term * term * rule list list * (rule * (term * term list)) list,
1.250 + locate_rule: rule list list -> term -> rule -> (rule * (term * term list)) list,
1.251 + next_rule: rule list list -> term -> rule option, normal_form: term -> (term * term list) option, prepat: (term list * term) list, rew_ord: rew_ord}
1.252 + val rep_thm_G': rule -> string * thm
1.253 + val str2ketype: string -> ketype
1.254 + val string_of_thm: thm -> string
1.255 + val string_of_thm': theory -> thm -> string
1.256 + val string_to_bool: string -> bool
1.257 + type subs' = (cterm' * cterm') list
1.258 + val term_to_string'': thyID -> term -> string
1.259 + val terms2str': term list -> string
1.260 + val terms2strs: term list -> string list
1.261 + type thehier = thydata ptyp list
1.262 + val theory2str': theory -> string
1.263 + val thm2str: thm -> string
1.264 + eqtype thmDeriv
1.265 + val thm_of_thm: rule -> thm
1.266 + val thy2ctxt: theory -> Proof.context
1.267 + val type_to_string': Proof.context -> typ -> string
1.268 + val type_to_string'': thyID -> typ -> string
1.269 + val type_to_string''': theory -> typ -> string
1.270 + ----------------------------------------- ^^^ make public -----------------------------------*)
1.271 + end
1.272 +(**)
1.273 +structure Celem(**): CALC_ELEMENT(**) =
1.274 struct
1.275 -*)
1.276 +(**)
1.277 +
1.278 val linefeed = (curry op^) "\n";
1.279 type authors = string list;
1.280
1.281 @@ -528,9 +784,10 @@
1.282 -> bool)) (*if t1 <= t2 then true else false *)
1.283 list); (*association list *)
1.284
1.285 +(* NOT ACCEPTED BY struct
1.286 rew_ord' := overwritel (!rew_ord', [("e_rew_ord", e_rew_ord),
1.287 ("dummy_ord", dummy_ord)]);
1.288 -
1.289 +*)
1.290
1.291 (* A tree for storing data defined in different theories
1.292 for access from the Interpreter and from dialogue authoring
1.293 @@ -1149,6 +1406,6 @@
1.294 else if member Context.eq_thy (isabthys ()) thy then "Isabelle"
1.295 else error ("closure of thys in Isac is broken by " ^ string_of_thy thy)
1.296 fun partID' (thy' : theory') = partID (Thy_Info_get_theory thy')
1.297 -(*
1.298 +
1.299 end (*struct*)
1.300 -*)
1.301 +