1.1 --- a/src/Tools/isac/calcelems.sml Sat Mar 24 14:34:47 2018 +0100
1.2 +++ b/src/Tools/isac/calcelems.sml Sat Mar 24 14:41:32 2018 +0100
1.3 @@ -9,10 +9,10 @@
1.4
1.5 signature CALC_ELEMENT =
1.6 sig
1.7 - type eval_fn (*= string -> term -> theory -> (string * term) option*)
1.8 - type rew_ord (*= rew_ord' * rew_ord_*)
1.9 + type eval_fn
1.10 + type rew_ord
1.11 eqtype errpatID
1.12 - type calc (*= prog_calcID * cal*)
1.13 + type calc
1.14 datatype rule = Cal1 of string * eval_fn | Calc of string * eval_fn | Erule | Rls_ of rls
1.15 | Thm of string * thm
1.16 and scr
1.17 @@ -37,37 +37,34 @@
1.18 eqtype theory'
1.19 eqtype prog_calcID
1.20 eqtype calID
1.21 - type cas_elem (*= term * (spec * generate_fn)*)
1.22 - type pbt (*= {cas: term option, guh: guh, init: pblID, mathauthors: string list,
1.23 - met: metID list, ppc: pat list, prls: rls, thy: theory, where_: term list}*)
1.24 - type ptyps (*= pbt ptyp list*)
1.25 - type metID (*= string list*)
1.26 - type pblID (*= string list*)
1.27 - type mets (*= met ptyp list*)
1.28 - type met (*= {calc: calc list,
1.29 - crls: rls, erls: rls, errpats: errpat list, guh: guh, init: pblID, mathauthors: string list,
1.30 - nrls: rls, ppc: pat list, pre: term list, prls: rls, rew_ord': rew_ord', scr: scr, srls: rls}*)
1.31 + type cas_elem
1.32 + type pbt
1.33 + type ptyps
1.34 + type metID
1.35 + type pblID
1.36 + type mets
1.37 + type met
1.38 datatype 'a ptyp = Ptyp of string * 'a list * 'a ptyp list
1.39
1.40 type cal = calID * eval_fn
1.41 - type authors (*= string list*)
1.42 + type authors
1.43 type guh
1.44 - type subst (*= (term * term) list*)
1.45 + type subst
1.46 eqtype thyID
1.47 - type fillpat (*= fillpatID * term * errpatID*)
1.48 + type fillpat
1.49 datatype thydata
1.50 = Hcal of {calc: calc, coursedesign: authors, guh: guh, mathauthors: authors}
1.51 | Hord of {coursedesign: authors, guh: guh, mathauthors: authors, ord: subst -> term * term -> bool}
1.52 | Hrls of {coursedesign: authors, guh: guh, mathauthors: authors, thy_rls: thyID * rls}
1.53 | Hthm of {coursedesign: authors, fillpats: fillpat list, guh: guh, mathauthors: authors, thm: thm}
1.54 | Html of {coursedesign: authors, guh: guh, html: string, mathauthors: authors}
1.55 - type theID (*= string list*)
1.56 - type rlss_elem (*= rls' * (theory' * rls)*)
1.57 + type theID
1.58 + type rlss_elem
1.59 val merge_rlss: rlss_elem list * rlss_elem list -> rlss_elem list
1.60 val rls_eq: (''a * ('b * 'c)) * (''a * ('d * 'e)) -> bool
1.61 - type calc_elem (*= prog_calcID * (calID * eval_fn)*)
1.62 + type calc_elem
1.63 val calc_eq: calc_elem * calc_elem -> bool
1.64 - type spec (*= domID * pblID * metID*)
1.65 + type spec
1.66 val cas_eq: cas_elem * cas_elem -> bool
1.67 val e_Ptyp: pbt ptyp
1.68 val merge_ptyps: 'a ptyp list * 'a ptyp list -> 'a ptyp list
1.69 @@ -97,7 +94,7 @@
1.70 val thy2ctxt: theory -> Proof.context
1.71 val trace_calc: bool Unsynchronized.ref
1.72 eqtype thmID
1.73 - type thm' (*= thmID * cterm'*)
1.74 + type thm'
1.75 datatype lrd = D | L | R
1.76 val trace_rewrite: bool Unsynchronized.ref
1.77 val depth: int Unsynchronized.ref
1.78 @@ -121,28 +118,28 @@
1.79 val term_to_string': Proof.context -> term -> string
1.80 val thy2ctxt': string -> Proof.context
1.81 type rrlsstate = term * term * rule list list * (rule * (term * term list)) list
1.82 - type loc_ (*= lrd list*)
1.83 + type loc_
1.84 val loc_2str: loc_ -> string
1.85 val e_spec: spec
1.86 val env2str: subst -> string
1.87 val subst2str: subst -> string
1.88 val termopt2str: term option -> string
1.89 eqtype rew_ord'
1.90 - type thm'' (*= thmID * thm*)
1.91 - type rew_ord_ (*= subst -> term * term -> bool*)
1.92 + type thm''
1.93 + type rew_ord_
1.94 val metID2str: string list -> string
1.95 val e_domID: domID
1.96 val e_pblID: pblID
1.97 val e_metID: metID
1.98 val empty_spec: spec
1.99 datatype ketype = Exp_ | Met_ | Pbl_ | Thy_
1.100 - type kestoreID (*= string list*)
1.101 - type errpat (*= errpatID * term list * thm list*)
1.102 + type kestoreID
1.103 + type errpat
1.104 val app_py: 'a ptyp list -> ('a ptyp -> 'b) -> pblID -> string list -> 'b
1.105 val ketype2str: ketype -> string
1.106 val coll_pblguhs: pbt ptyp list -> guh list
1.107 val coll_metguhs: met ptyp list -> guh list
1.108 - type pat (*= string * (term * term)*)
1.109 + type pat
1.110 val e_type: typ
1.111 val theory2str: theory -> theory'
1.112 val pats2str: pat list -> string
1.113 @@ -194,65 +191,6 @@
1.114 val e_rrlsstate: rrlsstate
1.115 val thm_of_thm: rule -> thm
1.116 val remove_rls: string -> rls -> rule list -> rls
1.117 -
1.118 -(*---------------------- vvv^ make public for Test_Isac ------------------------------------
1.119 - val Html_default: theID -> thydata
1.120 - val a_term: term
1.121 - val a_type: typ
1.122 - val assoc': (string * 'a) list * string -> 'a option
1.123 - type generate_fn = term list -> (term * term list) list
1.124 - val e_guh: guh
1.125 - val e_kestoreID: string list
1.126 - val e_met: met
1.127 - val e_pbt_: pbt_
1.128 - val e_rew_ord': rew_ord'
1.129 - val e_rew_ord_: subst -> term * term -> bool
1.130 - val e_rfuns: scr
1.131 - val e_scr: scr
1.132 - val e_subst: (term * term) list
1.133 - val e_theID: string list
1.134 - val e_thydata: thydata
1.135 - val empty_cterm': string
1.136 - val eq_thmI: (thmID * thm) * (thmID * 'a) -> bool
1.137 - val eq_thmI': (string * 'a) * (string * 'b) -> bool
1.138 - val eqrule: rule * rule -> bool
1.139 - val fill_parents: string list * string list -> thydata -> thydata ptyp
1.140 - val insert_fillpats: thydata ptyp list -> (pblID * fillpat list) list -> thydata ptyp list -> thydata ptyp list
1.141 - val insert_merge_rls: rlss_elem -> rlss_elem list -> rlss_elem list
1.142 - val insthy: 'a -> 'b * 'c -> 'b * ('a * 'c)
1.143 - val kestoreID2str: string list -> string
1.144 - val ldr2str: lrd -> string
1.145 - val lim_rewrite: int Unsynchronized.ref
1.146 - val memrls: rule -> rls -> bool
1.147 - val merge_ids: rls -> rls -> string
1.148 - val merge_ptyps': 'a ptyp list -> 'a ptyp list -> 'a ptyp list
1.149 - val overwritelthy: theory -> (rls' * (string * rls)) list * (rls' * rls) list -> (rls' * (string * rls)) list
1.150 - val partID: theory -> string
1.151 - val pat2str: pat -> string
1.152 - val pblID2str: string list -> string
1.153 - val pbt2str: pbt -> string
1.154 - val progthys: unit -> theory list
1.155 - val rep_rrls:
1.156 - rls -> {attach_form: rule list list -> term -> term -> (rule * (term * term list)) list,
1.157 - calc: calc list,
1.158 - erls: rls,
1.159 - errpatts: errpatID list,
1.160 - id: string,
1.161 - init_state: term -> term * term * rule list list * (rule * (term * term list)) list,
1.162 - locate_rule: rule list list -> term -> rule -> (rule * (term * term list)) list,
1.163 - 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.164 - val rep_thm_G': rule -> string * thm
1.165 - val str2ketype: string -> ketype
1.166 - val string_to_bool: string -> bool
1.167 - type subs' = (cterm' * cterm') list
1.168 - type thehier = thydata ptyp list
1.169 - val theory2str': theory -> string
1.170 - eqtype thmDeriv
1.171 - val thy2ctxt: theory -> Proof.context
1.172 - val type_to_string': Proof.context -> typ -> string
1.173 - val type_to_string'': thyID -> typ -> string
1.174 - val type_to_string''': theory -> typ -> string
1.175 - ---------------------- vvv^ make public for Test_Isac ------------------------------------*)
1.176 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
1.177 (* NONE *)
1.178 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )