1.1 --- a/src/Tools/isac/Build_Isac.thy	Wed Aug 25 16:49:56 2010 +0200
     1.2 +++ b/src/Tools/isac/Build_Isac.thy	Thu Aug 26 10:03:53 2010 +0200
     1.3 @@ -12,9 +12,7 @@
     1.4  header {* Loading the isac mathengine *}
     1.5  
     1.6  theory Build_Isac
     1.7 -(*imports Complex_Main*)
     1.8 -imports Complex_Main "ProgLang/Script" 
     1.9 -  (*ListC, Tools, Script*)
    1.10 +imports Complex_Main "ProgLang/Script" (*ListC, Tools, Script*)
    1.11  begin
    1.12  
    1.13  ML {* 

     2.1 --- a/src/Tools/isac/Knowledge/Atools.thy	Wed Aug 25 16:49:56 2010 +0200
     2.2 +++ b/src/Tools/isac/Knowledge/Atools.thy	Thu Aug 26 10:03:53 2010 +0200
     2.3 @@ -6,18 +6,707 @@
     2.4          10        20        30        40        50        60        70        80
     2.5  *)
     2.6  
     2.7 -theory Atools imports Descript Typefix begin
     2.8 -(*
     2.9 -*)
    2.10 -(*theory Atools imports "Knowledge/Descript" "Knowledge/Typefix" begin*)
    2.11 +(*theory Atools imports Descript Typefix begin  ...WOULD BE REQUIRED*)
    2.12 +theory Atools imports Complex_Main
    2.13  (*theory Atools imports "../Knowledge/Descript" "../Knowledge/Typefix" begin*)
    2.14 +uses ("../ProgLang/term.sml")
    2.15 +begin
    2.16 +use "../ProgLang/term.sml"
    2.17  
    2.18  consts
    2.19  
    2.20    Arbfix           :: "real"
    2.21 +  Undef            :: "real"
    2.22 +  dummy            :: "real"
    2.23 +
    2.24 +  some'_occur'_in  :: "[real list, 'a] => bool" ("some'_of _ occur'_in _")
    2.25 +  occurs'_in       :: "[real     , 'a] => bool" ("_ occurs'_in _")
    2.26 +
    2.27 +  pow              :: "[real, real] => real"    (infixr "^^^" 80)
    2.28 +(* ~~~ power doesn't allow Free("2",real) ^ Free("2",nat)
    2.29 +                           ~~~~     ~~~~    ~~~~     ~~~*)
    2.30 +(*WN0603 at FE-interface encoded strings to '^', 
    2.31 +	see 'fun encode', fun 'decode'*)
    2.32 +
    2.33 +  abs              :: "real => real"            ("(|| _ ||)")
    2.34 +(* ~~~ FIXXXME Isabelle2002 has abs already !!!*)
    2.35 +  absset           :: "real set => real"        ("(||| _ |||)")
    2.36 +  (*is numeral constant ?*)
    2.37 +  is'_const        :: "real => bool"            ("_ is'_const" 10)
    2.38 +  (*is_const rename to is_num FIXXXME.WN.16.5.03 *)
    2.39 +  is'_atom         :: "real => bool"            ("_ is'_atom" 10)
    2.40 +  is'_even         :: "real => bool"            ("_ is'_even" 10)
    2.41 +		
    2.42 +  (* identity on term level*)
    2.43 +  ident            :: "['a, 'a] => bool"        ("(_ =!=/ _)" [51, 51] 50)
    2.44 +
    2.45 +  argument'_in     :: "real => real"            ("argument'_in _" 10)
    2.46 +  sameFunId        :: "[real, bool] => bool"    (**"same'_funid _ _" 10
    2.47 +	WN0609 changed the id, because ".. _ _" inhibits currying**)
    2.48 +  filter'_sameFunId:: "[real, bool list] => bool list" 
    2.49 +					        ("filter'_sameFunId _ _" 10)
    2.50 +  boollist2sum     :: "bool list => real"
    2.51 +
    2.52 +axioms (*for evaluating the assumptions of conditional rules*)
    2.53 +
    2.54 +  last_thmI	      "lastI (x#xs) = (if xs =!= [] then x else lastI xs)"
    2.55 +  real_unari_minus    "- a = (-1) * a"           (*Isa!*)
    2.56 +
    2.57 +  rle_refl            "(n::real) <= n"
    2.58 +(*reflI               "(t = t) = True"*)
    2.59 +  radd_left_cancel_le "((k::real) + m <= k + n) = (m <= n)"
    2.60 +  not_true            "(~ True) = False"
    2.61 +  not_false           "(~ False) = True"
    2.62 +  and_true            "(a & True) = a"
    2.63 +  and_false           "(a & False) = False"
    2.64 +  or_true             "(a | True) = True"
    2.65 +  or_false            "(a | False) = a"
    2.66 +  and_commute         "(a & b) = (b & a)"
    2.67 +  or_commute          "(a | b) = (b | a)"
    2.68 +
    2.69 +  (*.should be in Rational.thy, but: 
    2.70 +   needed for asms in e.g. d2_pqformula1 in PolyEq.ML, RootEq.ML.*)
    2.71 +  rat_leq1	      "[| b ~= 0; d ~= 0 |] ==>
    2.72 +		       ((a / b) <= (c / d)) = ((a*d) <= (b*c))"(*Isa?*)
    2.73 +  rat_leq2	      "d ~= 0 ==>
    2.74 +		       ( a      <= (c / d)) = ((a*d) <=    c )"(*Isa?*)
    2.75 +  rat_leq3	      "b ~= 0 ==>
    2.76 +		       ((a / b) <=  c     ) = ( a    <= (b*c))"(*Isa?*)
    2.77 +
    2.78 +text {*copy from doc/math-eng.tex WN.28.3.03
    2.79 +WN071228 extended *}
    2.80 +
    2.81 +
    2.82 +section {*Coding standards*}
    2.83 +subsection {*Identifiers*}
    2.84 +text {*Naming is particularily crucial, because Isabelles name space is global, and isac does not yet use the novel locale features introduces by Isar. For instance, {\tt probe} sounds reasonable as (1) a description in the model of a problem-pattern, (2) as an element of the problem hierarchies key, (3) as a socalled CAS-command, (4) as the name of a related script etc. However, all the cases (1)..(4) require different typing for one and the same identifier {\tt probe} which is impossible, and actually leads to strange errors (for instance (1) is used as string, except in a script addressing a Subproblem).
    2.85 +
    2.86 +This are the preliminary rules for naming identifiers>
    2.87 +\begin{description}
    2.88 +\item [elements of a key] into the hierarchy of problems or methods must not contain capital letters and may contain underscrores, e.g. {\tt probe, for_polynomials}.
    2.89 +\item [descriptions in problem-patterns] must contain at least 1 capital letter and must not contain underscores, e.g. {\tt Probe, forPolynomials}.
    2.90 +\item [CAS-commands] follow the same rules as descriptions in problem-patterns above, thus beware of conflicts~!
    2.91 +\item [script identifiers] always end with {\tt Script}, e.g. {\tt ProbeScript}.
    2.92 +\item [???] ???
    2.93 +\item [???] ???
    2.94 +\end{description}
    2.95 +%WN071228 extended *}
    2.96 +
    2.97 +subsection {*Rule sets*}
    2.98 +text {*The actual version of the coding standards for rulesets is in {\tt /IsacKnowledge/Atools.ML where it can be viewed using the knowledge browsers.
    2.99 +
   2.100 +There are rulesets visible to the student, and there are rulesets visible (in general) only for math authors. There are also rulesets which {\em must} exist for {\em each} theory; these contain the identifier of the respective theory (including all capital letters) as indicated by {\it Thy} below.
   2.101 +\begin{description}
   2.102 +
   2.103 +\item [norm\_{\it Thy}] exists for each theory, and {\em efficiently} calculates a normalform for all terms which can be expressed by the definitions of the respective theory (and the respective parents).
   2.104 +
   2.105 +\item [simplify\_{\it Thy}] exists for each theory, and calculates a normalform for all terms which can be expressed by the definitions of the respective theory (and the respective parents) such, that the rewrites can be presented to the student.
   2.106 +
   2.107 +\item [calculate\_{\it Thy}] exists for each theory, and evaluates terms with numerical constants only (i.e. all terms which can be expressed by the definitions of the respective theory and the respective parent theories). In particular, this ruleset includes evaluating in/equalities with numerical constants only.
   2.108 +WN.3.7.03: may be dropped due to more generality: numericals and non-numericals are logically equivalent, where the latter often add to the assumptions (e.g. in Check_elementwise).
   2.109 +\end{description}
   2.110 +
   2.111 +The above rulesets are all visible to the user, and also may be input; thus they must be contained in the global associationlist {\tt ruleset':= }~! All these rulesets must undergo a preparation using the function {\tt prep_rls}, which generates a script for stepwise rewriting etc.
   2.112 +The following rulesets are used for internal purposes and usually invisible to the (naive) user:
   2.113 +\begin{description}
   2.114 +
   2.115 +\item [*\_erls] TODO
   2.116 +\item [*\_prls] 
   2.117 +\item [*\_srls] 
   2.118 +
   2.119 +\end{description}
   2.120 +{\tt append_rls, merge_rls, remove_rls} TODO
   2.121 +*}
   2.122  
   2.123  ML {*
   2.124 -111;
   2.125 +
   2.126 +(** evaluation of numerals and special predicates on the meta-level **)
   2.127 +(*-------------------------functions---------------------*)
   2.128 +local (* rlang 09.02 *)
   2.129 +    (*.a 'c is coefficient of v' if v does occur in c.*)
   2.130 +    fun coeff_in v c = member op = (vars c) v;
   2.131 +in
   2.132 +    fun occurs_in v t = coeff_in v t;
   2.133 +end;
   2.134 +
   2.135 +(*("occurs_in", ("Atools.occurs'_in", eval_occurs_in ""))*)
   2.136 +fun eval_occurs_in _ "Atools.occurs'_in"
   2.137 +	     (p as (Const ("Atools.occurs'_in",_) $ v $ t)) _ =
   2.138 +    ((*writeln("@@@ eval_occurs_in: v= "^(term2str v));
   2.139 +     writeln("@@@ eval_occurs_in: t= "^(term2str t));*)
   2.140 +     if occurs_in v t
   2.141 +    then SOME ((term2str p) ^ " = True",
   2.142 +	  Trueprop $ (mk_equality (p, HOLogic.true_const)))
   2.143 +    else SOME ((term2str p) ^ " = False",
   2.144 +	  Trueprop $ (mk_equality (p, HOLogic.false_const))))
   2.145 +  | eval_occurs_in _ _ _ _ = NONE;
   2.146 +
   2.147 +(*some of the (bound) variables (eg. in an eqsys) "vs" occur in term "t"*)   
   2.148 +fun some_occur_in vs t = 
   2.149 +    let fun occurs_in' a b = occurs_in b a
   2.150 +    in foldl or_ (false, map (occurs_in' t) vs) end;
   2.151 +
   2.152 +(*("some_occur_in", ("Atools.some'_occur'_in", 
   2.153 +			eval_some_occur_in "#eval_some_occur_in_"))*)
   2.154 +fun eval_some_occur_in _ "Atools.some'_occur'_in"
   2.155 +			  (p as (Const ("Atools.some'_occur'_in",_) 
   2.156 +				       $ vs $ t)) _ =
   2.157 +    if some_occur_in (isalist2list vs) t
   2.158 +    then SOME ((term2str p) ^ " = True",
   2.159 +	       Trueprop $ (mk_equality (p, HOLogic.true_const)))
   2.160 +    else SOME ((term2str p) ^ " = False",
   2.161 +	       Trueprop $ (mk_equality (p, HOLogic.false_const)))
   2.162 +  | eval_some_occur_in _ _ _ _ = NONE;
   2.163 +
   2.164 +
   2.165 +
   2.166 +
   2.167 +(*evaluate 'is_atom'*)
   2.168 +(*("is_atom",("Atools.is'_atom",eval_is_atom "#is_atom_"))*)
   2.169 +fun eval_is_atom (thmid:string) "Atools.is'_atom"
   2.170 +		 (t as (Const(op0,_) $ arg)) thy = 
   2.171 +    (case arg of 
   2.172 +	 Free (n,_) => SOME (mk_thmid thmid op0 n "", 
   2.173 +			      Trueprop $ (mk_equality (t, true_as_term)))
   2.174 +       | _ => SOME (mk_thmid thmid op0 "" "", 
   2.175 +		    Trueprop $ (mk_equality (t, false_as_term))))
   2.176 +  | eval_is_atom _ _ _ _ = NONE;
   2.177 +
   2.178 +(*evaluate 'is_even'*)
   2.179 +fun even i = (i div 2) * 2 = i;
   2.180 +(*("is_even",("Atools.is'_even",eval_is_even "#is_even_"))*)
   2.181 +fun eval_is_even (thmid:string) "Atools.is'_even"
   2.182 +		 (t as (Const(op0,_) $ arg)) thy = 
   2.183 +    (case arg of 
   2.184 +	Free (n,_) =>
   2.185 +	 (case int_of_str n of
   2.186 +	      SOME i =>
   2.187 +	      if even i then SOME (mk_thmid thmid op0 n "", 
   2.188 +				   Trueprop $ (mk_equality (t, true_as_term)))
   2.189 +	      else SOME (mk_thmid thmid op0 "" "", 
   2.190 +			 Trueprop $ (mk_equality (t, false_as_term)))
   2.191 +	    | _ => NONE)
   2.192 +       | _ => NONE)
   2.193 +  | eval_is_even _ _ _ _ = NONE; 
   2.194 +
   2.195 +(*evaluate 'is_const'*)
   2.196 +(*("is_const",("Atools.is'_const",eval_const "#is_const_"))*)
   2.197 +fun eval_const (thmid:string) _(*"Atools.is'_const" WN050820 diff.beh. rooteq*)
   2.198 +	       (t as (Const(op0,t0) $ arg)) (thy:theory) = 
   2.199 +    (*eval_const FIXXXXXME.WN.16.5.03 still forgets ComplexI*)
   2.200 +    (case arg of 
   2.201 +       Const (n1,_) =>
   2.202 +	 SOME (mk_thmid thmid op0 n1 "", 
   2.203 +	       Trueprop $ (mk_equality (t, false_as_term)))
   2.204 +     | Free (n1,_) =>
   2.205 +	 if is_numeral n1
   2.206 +	   then SOME (mk_thmid thmid op0 n1 "", 
   2.207 +		      Trueprop $ (mk_equality (t, true_as_term)))
   2.208 +	 else SOME (mk_thmid thmid op0 n1 "", 
   2.209 +		    Trueprop $ (mk_equality (t, false_as_term)))
   2.210 +     | Const ("Float.Float",_) =>
   2.211 +       SOME (mk_thmid thmid op0 (term2str arg) "", 
   2.212 +	     Trueprop $ (mk_equality (t, true_as_term)))
   2.213 +     | _ => (*NONE*)
   2.214 +       SOME (mk_thmid thmid op0 (term2str arg) "", 
   2.215 +		    Trueprop $ (mk_equality (t, false_as_term))))
   2.216 +  | eval_const _ _ _ _ = NONE; 
   2.217 +
   2.218 +(*. evaluate binary, associative, commutative operators: *,+,^ .*)
   2.219 +(*("PLUS"    ,("op +"        ,eval_binop "#add_")),
   2.220 +  ("TIMES"   ,("op *"        ,eval_binop "#mult_")),
   2.221 +  ("POWER"  ,("Atools.pow"  ,eval_binop "#power_"))*)
   2.222 +
   2.223 +(* val (thmid,op_,t as(Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2)),thy) =
   2.224 +       ("xxxxxx",op_,t,thy);
   2.225 +   *)
   2.226 +fun mk_thmid_f thmid ((v11, v12), (p11, p12)) ((v21, v22), (p21, p22))  = 
   2.227 +    thmid ^ "Float ((" ^ 
   2.228 +    (string_of_int v11)^","^(string_of_int v12)^"), ("^
   2.229 +    (string_of_int p11)^","^(string_of_int p12)^")) __ (("^
   2.230 +    (string_of_int v21)^","^(string_of_int v22)^"), ("^
   2.231 +    (string_of_int p21)^","^(string_of_int p22)^"))";
   2.232 +
   2.233 +(*.convert int and float to internal floatingpoint prepresentation.*)
   2.234 +fun numeral (Free (str, T)) = 
   2.235 +    (case int_of_str str of
   2.236 +	 SOME i => SOME ((i, 0), (0, 0))
   2.237 +       | NONE => NONE)
   2.238 +  | numeral (Const ("Float.Float", _) $
   2.239 +		   (Const ("Pair", _) $
   2.240 +			  (Const ("Pair", T) $ Free (v1, _) $ Free (v2,_)) $
   2.241 +			  (Const ("Pair", _) $ Free (p1, _) $ Free (p2,_))))=
   2.242 +    (case (int_of_str v1, int_of_str v2, int_of_str p1, int_of_str p2) of
   2.243 +	(SOME v1', SOME v2', SOME p1', SOME p2') =>
   2.244 +	SOME ((v1', v2'), (p1', p2'))
   2.245 +      | _ => NONE)
   2.246 +  | numeral _ = NONE;
   2.247 +
   2.248 +(*.evaluate binary associative operations.*)
   2.249 +fun eval_binop (thmid:string) (op_:string) 
   2.250 +	       (t as ( Const(op0,t0) $ 
   2.251 +			    (Const(op0',t0') $ v $ t1) $ t2)) 
   2.252 +	       thy =                                     (*binary . (v.n1).n2*)
   2.253 +    if op0 = op0' then
   2.254 +	case (numeral t1, numeral t2) of
   2.255 +	    (SOME n1, SOME n2) =>
   2.256 +	    let val (T1,T2,Trange) = dest_binop_typ t0
   2.257 +		val res = calc (if op0 = "op -" then "op +" else op0) n1 n2
   2.258 +		(*WN071229 "HOL.divide" never tried*)
   2.259 +		val rhs = var_op_float v op_ t0 T1 res
   2.260 +		val prop = Trueprop $ (mk_equality (t, rhs))
   2.261 +	    in SOME (mk_thmid_f thmid n1 n2, prop) end
   2.262 +	  | _ => NONE
   2.263 +    else NONE
   2.264 +  | eval_binop (thmid:string) (op_:string) 
   2.265 +	       (t as 
   2.266 +		  (Const (op0, t0) $ t1 $ 
   2.267 +			 (Const (op0', t0') $ t2 $ v))) 
   2.268 +	       thy =                                     (*binary . n1.(n2.v)*)
   2.269 +  if op0 = op0' then
   2.270 +	case (numeral t1, numeral t2) of
   2.271 +	    (SOME n1, SOME n2) =>
   2.272 +	    if op0 = "op -" then NONE else
   2.273 +	    let val (T1,T2,Trange) = dest_binop_typ t0
   2.274 +		val res = calc op0 n1 n2
   2.275 +		val rhs = float_op_var v op_ t0 T1 res
   2.276 +		val prop = Trueprop $ (mk_equality (t, rhs))
   2.277 +	    in SOME (mk_thmid_f thmid n1 n2, prop) end
   2.278 +	  | _ => NONE
   2.279 +  else NONE
   2.280 +    
   2.281 +  | eval_binop (thmid:string) (op_:string)
   2.282 +	       (t as (Const (op0,t0) $ t1 $ t2)) thy =       (*binary . n1.n2*)
   2.283 +    (case (numeral t1, numeral t2) of
   2.284 +	 (SOME n1, SOME n2) =>
   2.285 +	 let val (T1,T2,Trange) = dest_binop_typ t0;
   2.286 +	     val res = calc op0 n1 n2;
   2.287 +	     val rhs = term_of_float Trange res;
   2.288 +	     val prop = Trueprop $ (mk_equality (t, rhs));
   2.289 +	 in SOME (mk_thmid_f thmid n1 n2, prop) end
   2.290 +       | _ => NONE)
   2.291 +  | eval_binop _ _ _ _ = NONE; 
   2.292 +(*
   2.293 +> val SOME (thmid, t) = eval_binop "#add_" "op +" (str2term "-1 + 2") thy;
   2.294 +> term2str t;
   2.295 +val it = "-1 + 2 = 1"
   2.296 +> val t = str2term "-1 * (-1 * a)";
   2.297 +> val SOME (thmid, t) = eval_binop "#mult_" "op *" t thy;
   2.298 +> term2str t;
   2.299 +val it = "-1 * (-1 * a) = 1 * a"*)
   2.300 +
   2.301 +
   2.302 +
   2.303 +(*.evaluate < and <= for numerals.*)
   2.304 +(*("le"      ,("op <"        ,eval_equ "#less_")),
   2.305 +  ("leq"     ,("op <="       ,eval_equ "#less_equal_"))*)
   2.306 +fun eval_equ (thmid:string) (op_:string) (t as 
   2.307 +	       (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) thy = 
   2.308 +    (case (int_of_str n1, int_of_str n2) of
   2.309 +	 (SOME n1', SOME n2') =>
   2.310 +  if calc_equ (strip_thy op0) (n1', n2')
   2.311 +    then SOME (mk_thmid thmid op0 n1 n2, 
   2.312 +	  Trueprop $ (mk_equality (t, true_as_term)))
   2.313 +  else SOME (mk_thmid thmid op0 n1 n2,  
   2.314 +	  Trueprop $ (mk_equality (t, false_as_term)))
   2.315 +       | _ => NONE)
   2.316 +    
   2.317 +  | eval_equ _ _ _ _ = NONE;
   2.318 +
   2.319 +
   2.320 +(*evaluate identity
   2.321 +> reflI;
   2.322 +val it = "(?t = ?t) = True"
   2.323 +> val t = str2term "x = 0";
   2.324 +> val NONE = rewrite_ thy dummy_ord e_rls false reflI t;
   2.325 +
   2.326 +> val t = str2term "1 = 0";
   2.327 +> val NONE = rewrite_ thy dummy_ord e_rls false reflI t;
   2.328 +----------- thus needs Calc !
   2.329 +> val t = str2term "0 = 0";
   2.330 +> val SOME (t',_) = rewrite_ thy dummy_ord e_rls false reflI t;
   2.331 +> term2str t';
   2.332 +val it = "True"
   2.333 +
   2.334 +val t = str2term "Not (x = 0)";
   2.335 +atomt t; term2str t;
   2.336 +*** -------------
   2.337 +*** Const ( Not)
   2.338 +*** . Const ( op =)
   2.339 +*** . . Free ( x, )
   2.340 +*** . . Free ( 0, )
   2.341 +val it = "x ~= 0" : string*)
   2.342 +
   2.343 +(*.evaluate identity on the term-level, =!= ,i.e. without evaluation of 
   2.344 +  the arguments: thus special handling by 'fun eval_binop'*)
   2.345 +(*("ident"   ,("Atools.ident",eval_ident "#ident_")):calc*)
   2.346 +fun eval_ident (thmid:string) "Atools.ident" (t as 
   2.347 +	       (Const (op0,t0) $ t1 $ t2 )) thy = 
   2.348 +  if t1 = t2
   2.349 +    then SOME (mk_thmid thmid op0 
   2.350 +	       ("("^(Syntax.string_of_term (thy2ctxt thy) t1)^")")
   2.351 +	       ("("^(Syntax.string_of_term (thy2ctxt thy) t2)^")"), 
   2.352 +	  Trueprop $ (mk_equality (t, true_as_term)))
   2.353 +  else SOME (mk_thmid thmid op0  
   2.354 +	       ("("^(Syntax.string_of_term (thy2ctxt thy) t1)^")")
   2.355 +	       ("("^(Syntax.string_of_term (thy2ctxt thy) t2)^")"),  
   2.356 +	  Trueprop $ (mk_equality (t, false_as_term)))
   2.357 +  | eval_ident _ _ _ _ = NONE;
   2.358 +(* TODO
   2.359 +> val t = str2term "x =!= 0";
   2.360 +> val SOME (str, t') = eval_ident "ident_" "b" t thy;
   2.361 +> term2str t';
   2.362 +val str = "ident_(x)_(0)" : string
   2.363 +val it = "(x =!= 0) = False" : string                                
   2.364 +> val t = str2term "1 =!= 0";
   2.365 +> val SOME (str, t') = eval_ident "ident_" "b" t thy;
   2.366 +> term2str t';
   2.367 +val str = "ident_(1)_(0)" : string 
   2.368 +val it = "(1 =!= 0) = False" : string                                       
   2.369 +> val t = str2term "0 =!= 0";
   2.370 +> val SOME (str, t') = eval_ident "ident_" "b" t thy;
   2.371 +> term2str t';
   2.372 +val str = "ident_(0)_(0)" : string
   2.373 +val it = "(0 =!= 0) = True" : string
   2.374 +*)
   2.375 +
   2.376 +(*.evaluate identity of terms, which stay ready for evaluation in turn;
   2.377 +  thus returns False only for atoms.*)
   2.378 +(*("equal"   ,("op =",eval_equal "#equal_")):calc*)
   2.379 +fun eval_equal (thmid:string) "op =" (t as 
   2.380 +	       (Const (op0,t0) $ t1 $ t2 )) thy = 
   2.381 +  if t1 = t2
   2.382 +    then ((*writeln"... eval_equal: t1 = t2  --> True";*)
   2.383 +	  SOME (mk_thmid thmid op0 
   2.384 +	       ("("^(Syntax.string_of_term (thy2ctxt thy) t1)^")")
   2.385 +	       ("("^(Syntax.string_of_term (thy2ctxt thy) t2)^")"), 
   2.386 +	  Trueprop $ (mk_equality (t, true_as_term)))
   2.387 +	  )
   2.388 +  else (case (is_atom t1, is_atom t2) of
   2.389 +	    (true, true) => 
   2.390 +	    ((*writeln"... eval_equal: t1<>t2, is_atom t1,t2 --> False";*)
   2.391 +	     SOME (mk_thmid thmid op0  
   2.392 +			   ("("^(term2str t1)^")") ("("^(term2str t2)^")"),
   2.393 +		  Trueprop $ (mk_equality (t, false_as_term)))
   2.394 +	     )
   2.395 +	  | _ => ((*writeln"... eval_equal: t1<>t2, NOT is_atom t1,t2 --> go-on";*)
   2.396 +		  NONE))
   2.397 +  | eval_equal _ _ _ _ = (writeln"... eval_equal: error-exit";
   2.398 +			  NONE);
   2.399 +(*
   2.400 +val t = str2term "x ~= 0";
   2.401 +val NONE = eval_equal "equal_" "b" t thy;
   2.402 +
   2.403 +
   2.404 +> val t = str2term "(x + 1) = (x + 1)";
   2.405 +> val SOME (str, t') = eval_equal "equal_" "b" t thy;
   2.406 +> term2str t';
   2.407 +val str = "equal_(x + 1)_(x + 1)" : string
   2.408 +val it = "(x + 1 = x + 1) = True" : string
   2.409 +> val t = str2term "x = 0";
   2.410 +> val NONE = eval_equal "equal_" "b" t thy;
   2.411 +
   2.412 +> val t = str2term "1 = 0";
   2.413 +> val SOME (str, t') = eval_equal "equal_" "b" t thy;
   2.414 +> term2str t';
   2.415 +val str = "equal_(1)_(0)" : string 
   2.416 +val it = "(1 = 0) = False" : string
   2.417 +> val t = str2term "0 = 0";
   2.418 +> val SOME (str, t') = eval_equal "equal_" "b" t thy;
   2.419 +> term2str t';
   2.420 +val str = "equal_(0)_(0)" : string
   2.421 +val it = "(0 = 0) = True" : string
   2.422 +*)
   2.423 +
   2.424 +
   2.425 +(** evaluation on the metalevel **)
   2.426 +
   2.427 +(*. evaluate HOL.divide .*)
   2.428 +(*("DIVIDE" ,("HOL.divide"  ,eval_cancel "#divide_"))*)
   2.429 +fun eval_cancel (thmid:string) "HOL.divide" (t as 
   2.430 +	       (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) thy = 
   2.431 +    (case (int_of_str n1, int_of_str n2) of
   2.432 +	 (SOME n1', SOME n2') =>
   2.433 +  let 
   2.434 +    val sg = sign2 n1' n2';
   2.435 +    val (T1,T2,Trange) = dest_binop_typ t0;
   2.436 +    val gcd' = gcd (abs n1') (abs n2');
   2.437 +  in if gcd' = abs n2' 
   2.438 +     then let val rhs = term_of_num Trange (sg * (abs n1') div gcd')
   2.439 +	      val prop = Trueprop $ (mk_equality (t, rhs))
   2.440 +	  in SOME (mk_thmid thmid op0 n1 n2, prop) end     
   2.441 +     else if 0 < n2' andalso gcd' = 1 then NONE
   2.442 +     else let val rhs = num_op_num T1 T2 (op0,t0) (sg * (abs n1') div gcd')
   2.443 +				   ((abs n2') div gcd')
   2.444 +	      val prop = Trueprop $ (mk_equality (t, rhs))
   2.445 +	  in SOME (mk_thmid thmid op0 n1 n2, prop) end
   2.446 +  end
   2.447 +       | _ => ((*writeln"@@@ eval_cancel NONE";*)NONE))
   2.448 +
   2.449 +  | eval_cancel _ _ _ _ = NONE;
   2.450 +
   2.451 +(*. get the argument from a function-definition.*)
   2.452 +(*("argument_in" ,("Atools.argument'_in",
   2.453 +		   eval_argument_in "Atools.argument'_in"))*)
   2.454 +fun eval_argument_in _ "Atools.argument'_in" 
   2.455 +		     (t as (Const ("Atools.argument'_in", _) $ (f $ arg))) _ =
   2.456 +    if is_Free arg (*could be something to be simplified before*)
   2.457 +    then SOME (term2str t ^ " = " ^ term2str arg,
   2.458 +	       Trueprop $ (mk_equality (t, arg)))
   2.459 +    else NONE
   2.460 +  | eval_argument_in _ _ _ _ = NONE;
   2.461 +
   2.462 +(*.check if the function-identifier of the first argument matches 
   2.463 +   the function-identifier of the lhs of the second argument.*)
   2.464 +(*("sameFunId" ,("Atools.sameFunId",
   2.465 +		   eval_same_funid "Atools.sameFunId"))*)
   2.466 +fun eval_sameFunId _ "Atools.sameFunId" 
   2.467 +		     (p as Const ("Atools.sameFunId",_) $ 
   2.468 +			(f1 $ _) $ 
   2.469 +			(Const ("op =", _) $ (f2 $ _) $ _)) _ =
   2.470 +    if f1 = f2 
   2.471 +    then SOME ((term2str p) ^ " = True",
   2.472 +	       Trueprop $ (mk_equality (p, HOLogic.true_const)))
   2.473 +    else SOME ((term2str p) ^ " = False",
   2.474 +	       Trueprop $ (mk_equality (p, HOLogic.false_const)))
   2.475 +| eval_sameFunId _ _ _ _ = NONE;
   2.476 +
   2.477 +
   2.478 +(*.from a list of fun-definitions "f x = ..." as 2nd argument
   2.479 +   filter the elements with the same fun-identfier in "f y"
   2.480 +   as the fst argument;
   2.481 +   this is, because Isabelles filter takes more than 1 sec.*)
   2.482 +fun same_funid f1 (Const ("op =", _) $ (f2 $ _) $ _) = f1 = f2
   2.483 +  | same_funid f1 t = raise error ("same_funid called with t = ("
   2.484 +				   ^term2str f1^") ("^term2str t^")");
   2.485 +(*("filter_sameFunId" ,("Atools.filter'_sameFunId",
   2.486 +		   eval_filter_sameFunId "Atools.filter'_sameFunId"))*)
   2.487 +fun eval_filter_sameFunId _ "Atools.filter'_sameFunId" 
   2.488 +		     (p as Const ("Atools.filter'_sameFunId",_) $ 
   2.489 +			(fid $ _) $ fs) _ =
   2.490 +    let val fs' = ((list2isalist HOLogic.boolT) o 
   2.491 +		   (filter (same_funid fid))) (isalist2list fs)
   2.492 +    in SOME (term2str (mk_equality (p, fs')),
   2.493 +	       Trueprop $ (mk_equality (p, fs'))) end
   2.494 +| eval_filter_sameFunId _ _ _ _ = NONE;
   2.495 +
   2.496 +
   2.497 +(*make a list of terms to a sum*)
   2.498 +fun list2sum [] = error ("list2sum called with []")
   2.499 +  | list2sum [s] = s
   2.500 +  | list2sum (s::ss) = 
   2.501 +    let fun sum su [s'] = 
   2.502 +	    Const ("op +", [HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
   2.503 +		  $ su $ s'
   2.504 +	  | sum su (s'::ss') = 
   2.505 +	    sum (Const ("op +", [HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
   2.506 +		  $ su $ s') ss'
   2.507 +    in sum s ss end;
   2.508 +
   2.509 +(*make a list of equalities to the sum of the lhs*)
   2.510 +(*("boollist2sum"    ,("Atools.boollist2sum"    ,eval_boollist2sum "")):calc*)
   2.511 +fun eval_boollist2sum _ "Atools.boollist2sum" 
   2.512 +		      (p as Const ("Atools.boollist2sum", _) $ 
   2.513 +			 (l as Const ("List.list.Cons", _) $ _ $ _)) _ =
   2.514 +    let val isal = isalist2list l
   2.515 +	val lhss = map lhs isal
   2.516 +	val sum = list2sum lhss
   2.517 +    in SOME ((term2str p) ^ " = " ^ (term2str sum),
   2.518 +	  Trueprop $ (mk_equality (p, sum)))
   2.519 +    end
   2.520 +| eval_boollist2sum _ _ _ _ = NONE;
   2.521 +
   2.522 +
   2.523 +
   2.524 +local
   2.525 +
   2.526 +open Term;
   2.527 +
   2.528 +in
   2.529 +fun termlessI (_:subst) uv = termless uv;
   2.530 +fun term_ordI (_:subst) uv = term_ord uv;
   2.531 +end;
   2.532 +
   2.533 +
   2.534 +(** rule set, for evaluating list-expressions in scripts 8.01.02 **)
   2.535 +
   2.536 +
   2.537 +val list_rls = 
   2.538 +    append_rls "list_rls" list_rls
   2.539 +	       [Calc ("op *",eval_binop "#mult_"),
   2.540 +		Calc ("op +", eval_binop "#add_"), 
   2.541 +		Calc ("op <",eval_equ "#less_"),
   2.542 +		Calc ("op <=",eval_equ "#less_equal_"),
   2.543 +		Calc ("Atools.ident",eval_ident "#ident_"),
   2.544 +		Calc ("op =",eval_equal "#equal_"),(*atom <> atom -> False*)
   2.545 +       
   2.546 +		Calc ("Tools.Vars",eval_var "#Vars_"),
   2.547 +		
   2.548 +		Thm ("if_True",num_str if_True),
   2.549 +		Thm ("if_False",num_str if_False)
   2.550 +		];
   2.551 +
   2.552 +ruleset' := overwritelthy thy (!ruleset',
   2.553 +  [("list_rls",list_rls)
   2.554 +   ]);
   2.555 +
   2.556 +(*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = e_rew_ord = dummy_ord*)
   2.557 +val tless_true = dummy_ord;
   2.558 +rew_ord' := overwritel (!rew_ord',
   2.559 +			[("tless_true", tless_true),
   2.560 +			 ("e_rew_ord'", tless_true),
   2.561 +			 ("dummy_ord", dummy_ord)]);
   2.562 +
   2.563 +val calculate_Atools = 
   2.564 +    append_rls "calculate_Atools" e_rls
   2.565 +               [Calc ("op <",eval_equ "#less_"),
   2.566 +		Calc ("op <=",eval_equ "#less_equal_"),
   2.567 +		Calc ("op =",eval_equal "#equal_"),
   2.568 +
   2.569 +		Thm  ("real_unari_minus",num_str real_unari_minus),
   2.570 +		Calc ("op +",eval_binop "#add_"),
   2.571 +		Calc ("op -",eval_binop "#sub_"),
   2.572 +		Calc ("op *",eval_binop "#mult_")
   2.573 +		];
   2.574 +
   2.575 +val Atools_erls = 
   2.576 +    append_rls "Atools_erls" e_rls
   2.577 +               [Calc ("op =",eval_equal "#equal_"),
   2.578 +                Thm ("not_true",num_str not_true),
   2.579 +		(*"(~ True) = False"*)
   2.580 +		Thm ("not_false",num_str not_false),
   2.581 +		(*"(~ False) = True"*)
   2.582 +		Thm ("and_true",and_true),
   2.583 +		(*"(?a & True) = ?a"*)
   2.584 +		Thm ("and_false",and_false),
   2.585 +		(*"(?a & False) = False"*)
   2.586 +		Thm ("or_true",or_true),
   2.587 +		(*"(?a | True) = True"*)
   2.588 +		Thm ("or_false",or_false),
   2.589 +		(*"(?a | False) = ?a"*)
   2.590 +               
   2.591 +		Thm ("rat_leq1",rat_leq1),
   2.592 +		Thm ("rat_leq2",rat_leq2),
   2.593 +		Thm ("rat_leq3",rat_leq3),
   2.594 +                Thm ("refl",num_str refl),
   2.595 +		Thm ("le_refl",num_str le_refl),
   2.596 +		Thm ("radd_left_cancel_le",num_str radd_left_cancel_le),
   2.597 +		
   2.598 +		Calc ("op <",eval_equ "#less_"),
   2.599 +		Calc ("op <=",eval_equ "#less_equal_"),
   2.600 +		
   2.601 +		Calc ("Atools.ident",eval_ident "#ident_"),    
   2.602 +		Calc ("Atools.is'_const",eval_const "#is_const_"),
   2.603 +		Calc ("Atools.occurs'_in",eval_occurs_in ""),    
   2.604 +		Calc ("Tools.matches",eval_matches "")
   2.605 +		];
   2.606 +
   2.607 +val Atools_crls = 
   2.608 +    append_rls "Atools_crls" e_rls
   2.609 +               [Calc ("op =",eval_equal "#equal_"),
   2.610 +                Thm ("not_true",num_str not_true),
   2.611 +		Thm ("not_false",num_str not_false),
   2.612 +		Thm ("and_true",and_true),
   2.613 +		Thm ("and_false",and_false),
   2.614 +		Thm ("or_true",or_true),
   2.615 +		Thm ("or_false",or_false),
   2.616 +               
   2.617 +		Thm ("rat_leq1",rat_leq1),
   2.618 +		Thm ("rat_leq2",rat_leq2),
   2.619 +		Thm ("rat_leq3",rat_leq3),
   2.620 +                Thm ("refl",num_str refl),
   2.621 +		Thm ("le_refl",num_str le_refl),
   2.622 +		Thm ("radd_left_cancel_le",num_str radd_left_cancel_le),
   2.623 +		
   2.624 +		Calc ("op <",eval_equ "#less_"),
   2.625 +		Calc ("op <=",eval_equ "#less_equal_"),
   2.626 +		
   2.627 +		Calc ("Atools.ident",eval_ident "#ident_"),    
   2.628 +		Calc ("Atools.is'_const",eval_const "#is_const_"),
   2.629 +		Calc ("Atools.occurs'_in",eval_occurs_in ""),    
   2.630 +		Calc ("Tools.matches",eval_matches "")
   2.631 +		];
   2.632 +
   2.633 +(*val atools_erls = ... waere zu testen ...
   2.634 +    merge_rls calculate_Atools
   2.635 +	      (append_rls Atools_erls (*i.A. zu viele rules*)
   2.636 +			  [Calc ("Atools.ident",eval_ident "#ident_"),    
   2.637 +			   Calc ("Atools.is'_const",eval_const "#is_const_"),
   2.638 +			   Calc ("Atools.occurs'_in",
   2.639 +				 eval_occurs_in "#occurs_in"),    
   2.640 +			   Calc ("Tools.matches",eval_matches "#matches")
   2.641 +			   ] (*i.A. zu viele rules*)
   2.642 +			  );*)
   2.643 +(* val atools_erls = prep_rls(
   2.644 +  Rls {id="atools_erls",preconds = [], rew_ord = ("termlessI",termlessI), 
   2.645 +      erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*)
   2.646 +      rules = [Thm ("refl",num_str refl),
   2.647 +		Thm ("le_refl",num_str le_refl),
   2.648 +		Thm ("radd_left_cancel_le",num_str radd_left_cancel_le),
   2.649 +		Thm ("not_true",num_str not_true),
   2.650 +		Thm ("not_false",num_str not_false),
   2.651 +		Thm ("and_true",and_true),
   2.652 +		Thm ("and_false",and_false),
   2.653 +		Thm ("or_true",or_true),
   2.654 +		Thm ("or_false",or_false),
   2.655 +		Thm ("and_commute",num_str and_commute),
   2.656 +		Thm ("or_commute",num_str or_commute),
   2.657 +		
   2.658 +		Calc ("op <",eval_equ "#less_"),
   2.659 +		Calc ("op <=",eval_equ "#less_equal_"),
   2.660 +		
   2.661 +		Calc ("Atools.ident",eval_ident "#ident_"),    
   2.662 +		Calc ("Atools.is'_const",eval_const "#is_const_"),
   2.663 +		Calc ("Atools.occurs'_in",eval_occurs_in ""),    
   2.664 +		Calc ("Tools.matches",eval_matches "")
   2.665 +	       ],
   2.666 +      scr = Script ((term_of o the o (parse thy)) 
   2.667 +      "empty_script")
   2.668 +      }:rls);
   2.669 +ruleset' := overwritelth thy 
   2.670 +		(!ruleset',
   2.671 +		 [("atools_erls",atools_erls)(*FIXXXME:del with rls.rls'*)
   2.672 +		  ]);
   2.673 +*)
   2.674 +"******* Atools.ML end *******";
   2.675 +
   2.676 +calclist':= overwritel (!calclist', 
   2.677 +   [("occurs_in",("Atools.occurs'_in", eval_occurs_in "#occurs_in_")),
   2.678 +    ("some_occur_in",
   2.679 +     ("Atools.some'_occur'_in", eval_some_occur_in "#some_occur_in_")),
   2.680 +    ("is_atom"  ,("Atools.is'_atom",eval_is_atom "#is_atom_")),
   2.681 +    ("is_even"  ,("Atools.is'_even",eval_is_even "#is_even_")),
   2.682 +    ("is_const" ,("Atools.is'_const",eval_const "#is_const_")),
   2.683 +    ("le"       ,("op <"        ,eval_equ "#less_")),
   2.684 +    ("leq"      ,("op <="       ,eval_equ "#less_equal_")),
   2.685 +    ("ident"    ,("Atools.ident",eval_ident "#ident_")),
   2.686 +    ("equal"    ,("op =",eval_equal "#equal_")),
   2.687 +    ("PLUS"     ,("op +"        ,eval_binop "#add_")),
   2.688 +    ("minus"    ,("op -",eval_binop "#sub_")), (*040207 only for prep_rls
   2.689 +	        			      no script with "minus"*)
   2.690 +    ("TIMES"    ,("op *"        ,eval_binop "#mult_")),
   2.691 +    ("DIVIDE"  ,("HOL.divide"  ,eval_cancel "#divide_")),
   2.692 +    ("POWER"   ,("Atools.pow"  ,eval_binop "#power_")),
   2.693 +    ("boollist2sum",("Atools.boollist2sum",eval_boollist2sum ""))
   2.694 +    ]);
   2.695 +
   2.696 +val list_rls = prep_rls(
   2.697 +    merge_rls "list_erls"
   2.698 +	      (Rls {id="replaced",preconds = [], 
   2.699 +		    rew_ord = ("termlessI", termlessI),
   2.700 +		    erls = Rls {id="list_elrs", preconds = [], 
   2.701 +				rew_ord = ("termlessI",termlessI), 
   2.702 +				erls = e_rls, 
   2.703 +				srls = Erls, calc = [], (*asm_thm = [],*)
   2.704 +				rules = [Calc ("op +", eval_binop "#add_"),
   2.705 +					 Calc ("op <",eval_equ "#less_")
   2.706 +					 (*    ~~~~~~ for nth_Cons_*)
   2.707 +					 ],
   2.708 +				scr = EmptyScr},
   2.709 +		    srls = Erls, calc = [], (*asm_thm = [], *)
   2.710 +		    rules = [], scr = EmptyScr})
   2.711 +	      list_rls);
   2.712 +ruleset' := overwritelthy thy (!ruleset', [("list_rls", list_rls)]);
   2.713  *}
   2.714  
   2.715  end

     3.1 --- a/src/Tools/isac/Knowledge/Descript.thy	Wed Aug 25 16:49:56 2010 +0200
     3.2 +++ b/src/Tools/isac/Knowledge/Descript.thy	Thu Aug 26 10:03:53 2010 +0200
     3.3 @@ -5,8 +5,7 @@
     3.4     + see WN, Reactive User-Guidance ... Vers. Oct.2000 p.48 ff
     3.5  *)
     3.6  
     3.7 -theory Descript imports "ProgLang/Script" begin
     3.8 -(*theory Descript imports "../ProgLang/Script" begin*)
     3.9 +theory Descript imports "../ProgLang/Script" begin
    3.10  
    3.11  consts
    3.12  

     4.1 --- a/src/Tools/isac/Knowledge/Typefix.thy	Wed Aug 25 16:49:56 2010 +0200
     4.2 +++ b/src/Tools/isac/Knowledge/Typefix.thy	Thu Aug 26 10:03:53 2010 +0200
     4.3 @@ -4,8 +4,7 @@
     4.4     (c) due to copyright terms
     4.5   *)
     4.6  
     4.7 -theory Typefix imports "ProgLang/Script" begin
     4.8 -(*theory Typefix imports "../ProgLang/Script" begin*)
     4.9 +theory Typefix imports "../ProgLang/Script" begin
    4.10  
    4.11  syntax
    4.12         

     5.1 --- a/test/Tools/isac/ADDTESTS/file-depend/3knowledge/Foo_Know111.thy	Wed Aug 25 16:49:56 2010 +0200
     5.2 +++ b/test/Tools/isac/ADDTESTS/file-depend/3knowledge/Foo_Know111.thy	Thu Aug 26 10:03:53 2010 +0200
     5.3 @@ -4,4 +4,8 @@
     5.4         bar111 :: "'a"
     5.5  axioms code111 : "foo111 = bar111"
     5.6  
     5.7 +ML {*
     5.8 +(* there is an error when de-commenting *) 111
     5.9 +*}
    5.10 +
    5.11  end
    5.12 \ No newline at end of file

     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/test/Tools/isac/ADDTESTS/file-depend/3knowledge/Foo_KnowALL.thy	Thu Aug 26 10:03:53 2010 +0200
     6.3 @@ -0,0 +1,5 @@
     6.4 +theory Foo_KnowALL imports Foo_Know111 Foo_Know222 begin
     6.5 +
     6.6 +axioms codeALL : "foo111 = bar222"
     6.7 +
     6.8 +end
     6.9 \ No newline at end of file

     7.1 --- a/test/Tools/isac/ADDTESTS/file-depend/Build_Test.thy	Wed Aug 25 16:49:56 2010 +0200
     7.2 +++ b/test/Tools/isac/ADDTESTS/file-depend/Build_Test.thy	Thu Aug 26 10:03:53 2010 +0200
     7.3 @@ -4,24 +4,25 @@
     7.4  use_thy "1language/Foo_Language"
     7.5  use     "2interpreter/2foointerpreter.ML"
     7.6  
     7.7 +(*vvvvvvv can be bypassed with Foo_KnowALL
     7.8  use_thy "3knowledge/Foo_Know111"
     7.9  use_thy "3knowledge/Foo_Know222"
    7.10 +  ^^^^^^^ can be bypassed with Foo_KnowALL*)
    7.11 +use_thy "3knowledge/Foo_KnowALL"
    7.12  
    7.13 -
    7.14 -ML {* (* the different theories of knowledge are recognized, Const: *)
    7.15 -
    7.16 +text {* the different theories of knowledge are recognized, Const bar*: *}
    7.17 +ML {* 
    7.18  val trm = Syntax.read_term_global @{theory Foo_Know111} 
    7.19    "fooprog (foo111 = bar111)";
    7.20 -foointerpret trm;
    7.21 -(*Const ("Foo_Know111.bar111", "'a") : term*)
    7.22 +val Const ("Foo_Know111.bar111", _) = foointerpret trm;
    7.23  
    7.24  val trm = Syntax.read_term_global @{theory Foo_Know222} 
    7.25    "fooprog (foo222 = bar222)";
    7.26 -foointerpret trm;
    7.27 -(*val it = Const ("Foo_Know222.bar222", "'a") : term*)
    7.28 +val Const ("Foo_Know222.bar222", _) = foointerpret trm;
    7.29  *}
    7.30  
    7.31 -ML {* (* the different theories of knowledge are recognized, Free: *)
    7.32 +text {* the different theories of knowledge are recognized, Free bar*: *}
    7.33 +ML {*
    7.34  val trm = Syntax.read_term_global @{theory Foo_Know111} 
    7.35    "fooprog (foo222 = bar222)";
    7.36  (*Const ("Foo_Language.fooprog", "bool => Foo_Language.foosource") $