1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/ProgLang/Script.thy Wed Aug 25 16:20:07 2010 +0200
1.3 @@ -0,0 +1,194 @@
1.4 +(* Title: tactics, tacticals etc. for scripts
1.5 + Author: Walther Neuper 000224
1.6 + (c) due to copyright terms
1.7 +
1.8 +use_thy_only"ProgLang/Script";
1.9 +use_thy"../ProgLang/Script";
1.10 +use_thy"Script";
1.11 + *)
1.12 +
1.13 +theory Script imports Tools begin
1.14 +
1.15 +typedecl
1.16 + ID (* identifiers for thy, ruleset,... *)
1.17 +
1.18 +typedecl
1.19 + arg (* argument of subproblem *)
1.20 +
1.21 +consts
1.22 +
1.23 +(*types of subproblems' arguments*)
1.24 + real_' :: "real => arg"
1.25 + real_list_' :: "(real list) => arg"
1.26 + real_set_' :: "(real set) => arg"
1.27 + bool_' :: "bool => arg"
1.28 + bool_list_' :: "(bool list) => arg"
1.29 + real_real_' :: "(real => real) => arg"
1.30 +
1.31 +(*tactics*)
1.32 + Rewrite :: "[ID, bool, 'a] => 'a"
1.33 + Rewrite'_Inst:: "[(real * real) list, ID, bool, 'a] => 'a"
1.34 + ("(Rewrite'_Inst (_ _ _))" 11)
1.35 + (*without last argument ^^ for @@*)
1.36 + Rewrite'_Set :: "[ID, bool, 'a] => 'a" ("(Rewrite'_Set (_ _))" 11)
1.37 + Rewrite'_Set'_Inst
1.38 + :: "[(real * real) list, ID, bool, 'a] => 'a"
1.39 + ("(Rewrite'_Set'_Inst (_ _ _))" 11)
1.40 + (*without last argument ^^ for @@*)
1.41 + Calculate :: "[ID, 'a] => 'a" (*WN100816 PLUS, TIMES, POWER miss.in scr*)
1.42 + Calculate1 :: "[ID, 'a] => 'a" (*FIXXXME: unknown to script-interpreter*)
1.43 +
1.44 + (* WN0509 substitution now is rewriting by a list of terms (of type bool)
1.45 + Substitute :: "[(real * real) list, 'a] => 'a"*)
1.46 + Substitute :: "[bool list, 'a] => 'a"
1.47 +
1.48 + Map :: "['a => 'b, 'a list] => 'b list"
1.49 + Tac :: "ID => 'a" (*deprecated; only use in Test.ML*)
1.50 + Check'_elementwise ::
1.51 + "['a list, 'b set] => 'a list"
1.52 + ("Check'_elementwise (_ _)" 11)
1.53 + Take :: "'a => 'a" (*for non-var args as long as no 'o'*)
1.54 + SubProblem :: "[ID * ID list * ID list, arg list] => 'a"
1.55 +
1.56 + Or'_to'_List :: "bool => 'a list" ("Or'_to'_List (_)" 11)
1.57 + (*=========== record these ^^^ in 'tacs' in Script.ML =========*)
1.58 +
1.59 + Assumptions :: bool
1.60 + Problem :: "[ID * ID list] => 'a"
1.61 +
1.62 +(*special formulas for frontend 'CAS format'*)
1.63 + Subproblem :: "(ID * ID list) => 'a"
1.64 +
1.65 +(*script-expressions (tacticals)*)
1.66 + Seq :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "@@" 10) (*@ used*)
1.67 + Try :: "['a => 'a, 'a] => 'a"
1.68 + Repeat :: "['a => 'a, 'a] => 'a"
1.69 + Or :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "Or" 10)
1.70 + While :: "[bool, 'a => 'a, 'a] => 'a" ("((While (_) Do)//(_))" 9)
1.71 +(*WN100723 because of "Error in syntax translation" below...
1.72 + (*'b => bool doesn't work with "contains_root _"*)
1.73 + Letpar :: "['a, 'a => 'b] => 'b"
1.74 + (*--- defined in Isabelle/scr/HOL/HOL.thy:
1.75 + Let :: "['a, 'a => 'b] => 'b"
1.76 + "_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" 10)
1.77 + If :: "[bool, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10)
1.78 + %x. P x .. lambda is defined in Isabelles meta logic
1.79 + --- *)
1.80 +*)
1.81 + failtac :: 'a
1.82 + idletac :: 'a
1.83 + (*... + RECORD IN 'screxpr' in Script.ML *)
1.84 +
1.85 +(*for scripts generated automatically from rls*)
1.86 + Stepwise :: "['z, 'z] => 'z" ("((Script Stepwise (_ =))// (_))" 9)
1.87 + Stepwise'_inst:: "['z,real,'z] => 'z"
1.88 + ("((Script Stepwise'_inst (_ _ =))// (_))" 9)
1.89 +
1.90 +
1.91 +(*SHIFT -> resp.thys ----vvv---------------------------------------------*)
1.92 +(*script-names: initial capital letter,
1.93 + type of last arg (=script-body) == result-type !
1.94 + Xxxx :: script ids, duplicate result-type 'r in last argument:
1.95 + "['a, ... , \
1.96 + \ 'r] => 'r
1.97 +*)
1.98 +
1.99 +(*make'_solution'_set :: "bool => bool list"
1.100 + ("(make'_solution'_set (_))" 11)
1.101 +
1.102 + max'_on'_interval
1.103 + :: "[ID * (ID list) * ID, bool,real,real set] => real"
1.104 + ("(max'_on'_interval (_)/ (_ _ _))" 9)
1.105 + find'_vals
1.106 + :: "[ID * (ID list) * ID,
1.107 + real,real,real,real,bool list] => bool list"
1.108 + ("(find'_vals (_)/ (_ _ _ _ _))" 9)
1.109 +
1.110 + make'_fun :: "[ID * (ID list) * ID, real,real,bool list] => bool"
1.111 + ("(make'_fun (_)/ (_ _ _))" 9)
1.112 +
1.113 + solve'_univar
1.114 + :: "[ID * (ID list) * ID, bool,real] => bool list"
1.115 + ("(solve'_univar (_)/ (_ _ ))" 9)
1.116 + solve'_univar'_err
1.117 + :: "[ID * (ID list) * ID, bool,real,bool] => bool list"
1.118 + ("(solve'_univar (_)/ (_ _ _))" 9)
1.119 +----------*)
1.120 +
1.121 + Testeq :: "[bool, bool] => bool"
1.122 + ("((Script Testeq (_ =))//
1.123 + (_))" 9)
1.124 +
1.125 + Testeq2 :: "[bool, bool list] => bool list"
1.126 + ("((Script Testeq2 (_ =))//
1.127 + (_))" 9)
1.128 +
1.129 + Testterm :: "[real, real] => real"
1.130 + ("((Script Testterm (_ =))//
1.131 + (_))" 9)
1.132 +
1.133 + Testchk :: "[bool, real, real list] => real list"
1.134 + ("((Script Testchk (_ _ =))//
1.135 + (_))" 9)
1.136 + (*... + RECORD IN 'subpbls' in Script.ML *)
1.137 +(*SHIFT -> resp.thys ----^^^----------------------------*)
1.138 +
1.139 +(*Makarius 10.03
1.140 +syntax
1.141 +
1.142 + "_Letpar" :: "[letbinds, 'a] => 'a" ("(letpar (_)/ in (_))" 10)
1.143 +
1.144 +translations
1.145 +
1.146 + "_Letpar (_binds b bs) e" == "_Letpar b (_Letpar bs e)"
1.147 + "letpar x = a in e" == "Letpar a (%x. e)"
1.148 +*** Error in syntax translation rule: rhs contains extra variables
1.149 +*** ("_Letpar" ("_bind" x a) e) -> (Letpar a ("_abs" x e))
1.150 +*** At command "translations" (line 140 of "/usr/local/isabisac/src/Pure/isac/Scripts/Script.thy").
1.151 +*)
1.152 +
1.153 +ML {* (*the former Script.ML*)
1.154 +
1.155 +(*.record all theories defined for Scripts; in order to distinguish them
1.156 + from general IsacKnowledge defined later on.*)
1.157 +script_thys := !theory';
1.158 +
1.159 +(*--vvv----- SHIFT? or delete ?*)
1.160 +val IDTyp = Type("Script.ID",[]);
1.161 +
1.162 +
1.163 +val tacs = ref (distinct (remove op = ""
1.164 + ["Calculate",
1.165 + "Rewrite","Rewrite'_Inst","Rewrite'_Set","Rewrite'_Set'_Inst",
1.166 + "Substitute","Tac","Check'_elementswise",
1.167 + "Take","Subproblem","Or'_to'_List"]));
1.168 +
1.169 +val screxpr = ref (distinct (remove op = ""
1.170 + ["Let","If","Repeat","While","Try","Or"]));
1.171 +
1.172 +val listfuns = ref [(*_all_ functions in Isa99.List.thy *)
1.173 + "@","filter","concat","foldl","hd","last","set","list_all",
1.174 + "map","mem","nth","list_update","take","drop",
1.175 + "takeWhile","dropWhile","tl","butlast",
1.176 + "rev","zip","upt","remdups","nodups","replicate",
1.177 +
1.178 + "Cons","Nil"];
1.179 +
1.180 +val scrfuns = ref (distinct (remove op = ""
1.181 + ["Testvar"]));
1.182 +
1.183 +val listexpr = ref (union op = (!listfuns) (!scrfuns));
1.184 +
1.185 +val notsimp = ref
1.186 + (distinct (remove op = ""
1.187 + (!tacs @ !screxpr @ (*!subpbls @*) !scrfuns @ !listfuns)));
1.188 +
1.189 +val negotiable = ref ((!tacs (*@ !subpbls*)));
1.190 +
1.191 +val tacpbl = ref
1.192 + (distinct (remove op = "" (!tacs (*@ !subpbls*))));
1.193 +(*--^^^----- SHIFT? or delete ?*)
1.194 +
1.195 +*}
1.196 +
1.197 +end