wneuper/isa: test/Tools/isac/ProgLang/calculate.sml@460c24a6a6ba

     1 (* Title:  test calculation of values for function constants

     2    Author: Walther Neuper 2000

     3    (c) copyright due to lincense terms.

     5 12345678901234567890123456789012345678901234567890123456789012345678901234567890

     6         10        20        30        40        50        60        70        80

     7 *)

     9 "--------------------------------------------------------";

    10 "table of contents --------------------------------------";

    11 "--------------------------------------------------------";

    12 "----------- check return value of get_calculation_  ----";

    13 " ================= calculate.sml: calculate_ ======================== ";

    14 " ================= calculate.sml: aus script ======================== ";

    15 " ================= calculate.sml: 2.8.02 check test-root-equ ======== ";

    16 "--------------(4): check bottom up: ---------------------------";

    17 " ================= calculate.sml:10.8.02 2002:///->/ ======== ";

    18 " ================= calculate.sml: calculate_ 2002 =================== ";

    19 "----------- get_pair with 3 args --------------------------------";

    20 " ================= eval_binop Float  =================== ";

    21 "------------------ 3.6.03 (2 * x is_const) ---------------------------";

    22 "--------------------------------------------------------";

    23 "--------------------------------------------------------";

    24 "--------------------------------------------------------";

    27 "----------- check return value of get_calculation_  ----";

    28 "----------- check return value of get_calculation_  ----";

    29 "----------- check return value of get_calculation_  ----";

    30 val thy = theory "Poly";

    31 val cal = snd (assoc1 (! calclist', "is_polyexp"));

    32 val t = @{term "(x / x) is_polyexp"};

    33 val SOME (thmID, thm) = get_calculation_ thy cal t;

    34 (HOLogic.dest_Trueprop (prop_of thm); writeln "all thms wrapped by Trueprop")

    35 handle TERM _ =>

    36        error "calculate.sml: get_calculation_ must return Trueprop";

    40 (*===== inhibit exn ?===========================================================

    41 val thy' = "Isac.thy";

    43 " ================= calculate.sml: calculate_ ======================== ";

    44 " ================= calculate.sml: calculate_ ======================== ";

    45 " ================= calculate.sml: calculate_ ======================== ";

    48 val thy = Test.thy;

    49 val t = (term_of o the o (parse thy)) "1+2";

    50 val Some (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"plus"))) t;

    52 val t = (term_of o the o (parse thy)) "((1+2)*4/3)^^^2";

    53 val Some (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"plus"))) t;

    54 val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;

    55 Sign.string_of_term (sign_of thy) t;

    56 (*val it = "(#3 * #4 // #3) ^^^ #2" : string*)

    57 val Some (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"times"))) t;

    58 val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;

    59 Sign.string_of_term (sign_of thy) t;

    60 (*val it = "(#12 // #3) ^^^ #2" : string*)

    61 val Some (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"divide_")))t;

    62 val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;

    63 Sign.string_of_term (sign_of thy) t;

    64 (*it = "#4 ^^^ #2" : string*)

    65 val Some (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_")))t;

    66 val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;

    67 Sign.string_of_term (sign_of thy) t;

    68 (*val it = "#16" : string*)

    69 if it <> "16" then error "calculate.sml: new behaviour in calculate_"

    70 else ();

    72 " ================= calculate.sml: aus script ======================== ";

    73 " ================= calculate.sml: aus script ======================== ";

    74 " ================= calculate.sml: aus script ======================== ";

    76 store_pbt

    77  (prep_pbt Test.thy "pbl_ttest" [] e_pblID

    78  (["test"],

    79   [],

    80   e_rls, None, []));

    81 store_pbt

    82  (prep_pbt Test.thy "pbl_ttest_calc" [] e_pblID

    83  (["calculate","test"],

    84   [("#Given" ,["realTestGiven t_"]),

    85    ("#Find"  ,["realTestFind s_"])

    86    ],

    87   e_rls, None, [["Test","test_calculate"]]));

    89 store_met

    90  (prep_met Test.thy "met_testcal" [] e_metID

    91  (["Test","test_calculate"]:metID,

    92   [("#Given" ,["realTestGiven t_"]),

    93    ("#Find"  ,["realTestFind s_"])

    94    ],

    95   {rew_ord'="sqrt_right",rls'=tval_rls,srls=e_rls,prls=e_rls,

    96    calc=[("plus"    ,("op +"        ,eval_binop "#add_")),

    97 	 ("times"   ,("op *"        ,eval_binop "#mult_")),

    98 	 ("divide_" ,("HOL.divide"  ,eval_cancel "#divide_")),

    99 	 ("power_"  ,("Atools.pow"  ,eval_binop "#power_"))],

   100    crls=tval_rls, nrls=e_rls(*,

   101    asm_rls=[],asm_thm=[]*)},

   102   "Script STest_simplify (t_::real) =          \

   103   \(Repeat                                        \

   104   \ ((Try (Repeat (Calculate plus))) @@   \

   105   \  (Try (Repeat (Calculate times))) @@  \

   106   \  (Try (Repeat (Calculate divide_))) @@ \

   107   \  (Try (Repeat (Calculate power_))))) t_"

   108    ));

   110 val fmz = ["realTestGiven (((1+2)*4/3)^^^2)","realTestFind s"];

   111 val (dI',pI',mI') =

   112   ("Test.thy",["calculate","test"],["Test","test_calculate"]);

   113 (*val p = e_pos'; val c = [];

   114 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

   115 val (p,_,f,nxt,_,pt) = me (mI,m) p c  EmptyPtree;*)

   116 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

   117 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   118 (*nxt =("Add_Given",Add_Given "realTestGiven (((#1 + #2) * #4 // #3) ^^^#2)")*)

   119 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   120 (*nxt = ("Add_Find",Add_Find "realTestFind s") : string * tac*)

   121 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   122 (*nxt = ("Specify_Theory",Specify_Theory "Test.thy") : string * tac*)

   123 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   124 (*nxt = ("Specify_Problem",Specify_Problem ["calculate","test"])*)

   125 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   126 (*nxt = ("Specify_Method",Specify_Method ("Test.thy","test_calculate"))*)

   127 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   128 (*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_calculate"))*)

   130 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   131 (*nxt = ("Calculate",Calculate "plus")*)

   132 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   133 (*nxt = ("Calculate",Calculate "times")*)

   134 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   135 (*nxt = ("Calculate",Calculate "divide_")*)

   136 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   137 (*nxt = ("Calculate",Calculate "power_")*)

   138 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   139 (*nxt = ("Check_Postcond",Check_Postcond ["calculate","test"])*)

   140 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   141 (*nxt = ("End_Proof'",End_Proof')*)

   142 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"16")) then ()

   143 else error "calculate.sml: script test_calculate changed behaviour";

   148 " ================= calculate.sml: 2.8.02 check test-root-equ ======== ";

   149 " ================= calculate.sml: 2.8.02 check test-root-equ ======== ";

   150 " ================= calculate.sml: 2.8.02 check test-root-equ ======== ";

   151 (*(1): 2nd Test_simplify didn't work:

   152 val ct =

   153   "sqrt (x ^^^ 2 + -3 * x) = (-3 + 2 * x + -1 * (9 + 4 * x)) / (-1 * 2)"

   154 > val rls = ("Test_simplify");

   155 > val (ct,_) = the (rewrite_set thy' ("tval_rls") false rls ct);

   156 val ct = "sqrt (x ^^^ 2 + -3 * x) =

   157 (-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))";

   158 ie. cancel does not work properly

   159 *)

   160  val thy = "Test.thy";

   161  val op_ = "divide_";

   162  val ct = "sqrt (x ^^^ 2 + -3 * x) =\

   163  \(-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))";

   164  val Some (ct,_) = calculate thy (the(assoc(calclist,op_))) ct;

   165  writeln ct;

   166 (*

   167            sqrt (x ^^^ 2 + -3 * x) =\

   168  \(-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))

   169 ............... does not work *)

   171 (*--------------(2): does divide work in Test_simplify ?: ------*)

   172  val thy = Test.thy;

   173  val t = (term_of o the o (parse thy)) "6 / 2";

   174  val rls = Test_simplify;

   175  val (t,_) = the (rewrite_set_ thy false rls t);

   176 (*val t = Free ("3","RealDef.real") : term*)

   178  val thy = "Test.thy";

   179  val t = "6 / 2";

   180  val rls = "Test_simplify";

   181  val (t,_) = the (rewrite_set thy false rls t);

   182 (*val t = "3" : string

   183       ....... works, thus: which rule in SqRoot_simplify works differently ?*)

   186 (*--------------(3): is_const works ?: -------------------------------------*)

   187  val t = (term_of o the o (parse Test.thy)) "2 is_const";

   188  atomty t;

   189  rewrite_set_ Test.thy false tval_rls t;

   190 (*val it = Some (Const ("True","bool"),[]) ... works*)

   192  val t = str2term "2 * x is_const";

   193  val Some (str,t') = eval_const "" "" t Isac.thy;

   194  term2str t';

   199 "--------------(4): check bottom up: ---------------------------";

   200 (*-------------- eval_cancel works: *)

   201  trace_rewrite:=true;

   202  val thy = Test.thy;

   203  val t = (term_of o the o (parse thy)) "(-4) / 2";

   204  val Some (_,t) = eval_cancel "xxx" "HOL.divide" t thy;

   205  term2str t;

   206 "-4 / 2 = (-2)";

   207 (*-------------- but ... *)

   208  val ct = "x + (-4) / 2";

   209  val (ct,_) = the (rewrite_set thy' false rls ct);

   210 "(-2) + x";

   211 (*-------------- while ... *)

   212  val ct = "(-4) / 2";

   213  val (ct,_) = the (rewrite_set thy'  false rls ct);

   214 "-2";

   216 (*--------------(5): reproduce (1) with simpler term: ------------*)

   217  val thy = "Test.thy";

   218  val t = "(3+5)/2";

   219  val (t,_) = the (rewrite_set thy false rls t);

   220 (*val t = "4" ... works*)

   222  val t = "(3+1+2*x)/2";

   223  val (t,_) = the (rewrite_set thy false rls t);

   224 (*val t = "2 + x" ... works*)

   226  trace_rewrite:=true; (*3.6.03*)

   227  val thy = "Test.thy";

   228  val rls = "Test_simplify";

   229  val t = "(3+(1+2*x))/2";

   230  val (t,_) = the (rewrite_set thy false rls t);

   231 (*val t = "2 + x" ... works: give up----------------------------------------*)

   232  trace_rewrite:=false;

   234  trace_rewrite:=true; (*3.6.03*)

   235  val thy = Test.thy;

   236  val rls = Test_simplify;

   237  val t = str2term "(3+(1+2*x))/2";

   238  val Some (t',asm) = rewrite_set_ thy false rls t;

   239  term2str t';

   240 (*val t = "2 + x" ... works: give up----------------------------------------*)

   241  trace_rewrite:=false;

   246 (*--- trace_rewrite before correction of ... --------------------

   247  val ct = "(-3 + 2 * x + -1) / 2";

   248  val (ct,_) = the (rewrite_set thy'  false rls ct);

   249 :

   250 ### trying thm 'root_ge0_2'

   251 ### rewrite_set_: x + (-1 + -3) / 2

   252 ### trying thm 'radd_real_const_eq'

   253 ### trying thm 'radd_real_const'

   254 ### rewrite_set_: x + (-4) / 2

   255 ### trying thm 'rcollect_right'

   256 :

   257 "x + (-4) / 2"

   258 -------------------------------------while before Isabelle20002:

   259  val ct = "(#-3 + #2 * x + #-1) // #2";

   260  val (ct,_) = the (rewrite_set thy'  false rls ct);

   261 :

   262 ### trying thm 'root_ge0_2'

   263 ### rewrite_set_: x + (#-1 + #-3) // #2

   264 ### trying thm 'radd_real_const_eq'

   265 ### trying thm 'radd_real_const'

   266 ### rewrite_set_: x + #-4 // #2

   267 ### rewrite_set_: x + #-2

   268 ### trying thm 'rcollect_right'

   269 :

   270 "#-2 + x"

   271 -----------------------------------------------------------------*)

   274  toggle trace_rewrite;

   275 (*===================*)

   276  trace_rewrite:=true;

   277  val thy' = "Test.thy";

   278  val rls = "Test_simplify";

   279  val ct = "x + (-1 + -3) / 2";

   280  val (ct,_) = the (rewrite_set thy'  false rls ct);

   281 "x + (-4) / 2";

   282 (*

   283 ### trying calc. 'cancel'

   284 @@@ get_pair: binop, t = x + (-4) / 2

   285 @@@ get_pair: t else

   286 @@@ get_pair: t else -> None

   287 @@@ get_pair: binop, t = (-4) / 2

   288 @@@ get_pair: then 1

   289 @@@ get_pair: t -> None

   290 @@@ get_pair: t1 -> None

   291 @@@ get_calculation: None

   292 ### trying calc. 'pow'

   293 *)

   295  trace_rewrite:=true;

   296  val thy' = "Test.thy";

   297  val rls = "Test_simplify";

   298  val ct = "x + (-4) / 2";

   299  val (ct,_) = the (rewrite_set thy'  false rls ct);

   300 "(-2) + x";

   301 (*

   302 ### trying calc. 'cancel'

   303 @@@ get_pair: binop, t = x + -4 / 2

   304 @@@ get_pair: t else

   305 @@@ get_pair: t else -> None

   306 @@@ get_pair: binop, t = -4 / 2

   307 @@@ get_pair: then 1

   308 @@@ get_calculation: Some #cancel_-4_2

   309 ### calc. to: x + (-2)

   310 ### trying calc. 'cancel'

   311 *)

   312  trace_rewrite:=false;

   314 " ================= calculate.sml:10.8.02 2002:///->/ ======== ";

   315 " ================= calculate.sml:10.8.02 2002:///->/ ======== ";

   316 " ================= calculate.sml:10.8.02 2002:///->/ ======== ";

   317 " ----------------- rewriting works ? -----------------------";

   318  val thy = Isac.thy;

   319  val prop = (#prop o rep_thm) real_divide_1;

   320  atomty prop;

   321 (*** -------------

   322 *** Const ( Trueprop, bool => prop)

   323 *** . Const ( op =, [real, real] => bool)

   324 *** . . Const ( HOL.divide, [real, real] => real)

   325 *** . . . Var ((x, 0), real)

   326 *** . . . Const ( 1, real)

   327 *** . . Var ((x, 0), real) *)

   328  val prop' = (#prop o rep_thm o num_str) real_divide_1;

   329  atomty prop';

   330 (*** -------------

   331 *** Const ( Trueprop, bool => prop)

   332 *** . Const ( op =, [real, real] => bool)

   333 *** . . Const ( HOL.divide, [real, real] => real)

   334 *** . . . Var ((x, 0), real)

   335 *** . . . Free ( 1, real)   (*app_num_tr'*)

   336 *** . . Var ((x, 0), real)*)

   337  val t = (term_of o the o (parseold thy)) "aaa/1";

   338  atomty t;

   339 (*** -------------

   340 *** Const ( HOL.divide, ['a, 'a] => 'a)

   341 *** . Free ( aaa, 'a)

   342 *** . Free ( 1, 'a) *)

   343  val t = (term_of o the o (parse thy)) "aaa/1";

   344  atomty t;

   345 (*** -------------

   346 *** Const ( HOL.divide, [real, real] => real)

   347 *** . Free ( aaa, real)

   348 *** . Free ( 1, real)  *)

   349  val thm = num_str real_divide_1;

   350  val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;

   351 (*val t = Free ("aaa","RealDef.real") : term*)

   354  val prop = (#prop o rep_thm) realpow_eq_one;

   355  atomty prop;

   356 (*** -------------

   357 *** Const ( Trueprop, bool => prop)

   358 *** . Const ( op =, [real, real] => bool)

   359 *** . . Const ( Nat.power, [real, nat] => real)

   360 *** . . . Const ( 1, real)

   361 *** . . . Var ((n, 0), nat)

   362 *** . . Const ( 1, real) *)

   363  val prop' = (#prop o rep_thm o num_str) realpow_eq_one;

   364  atomty prop';

   365 (*** -------------

   366 *** Const ( Trueprop, bool => prop)

   367 *** . Const ( op =, [real, real] => bool)

   368 *** . . Const ( Nat.power, [real, nat] => real)

   369 *** . . . Free ( 1, real)

   370 *** . . . Var ((n, 0), nat)

   371 *** . . Free ( 1, real)*)

   372  val t = (term_of o the o (parseold thy)) "1 ^ aaa";

   373  atomty t;

   374 (*** -------------

   375 *** Const ( Nat.power, ['a, nat] => 'a)

   376 *** . Free ( 1, 'a)

   377 *** . Free ( aaa, nat) *)

   378  val t = (term_of o the o (parse thy)) "1 ^ aaa";

   379  atomty t;

   380 (*** -------------

   381 *** Const ( Nat.power, [real, nat] => real)

   382 *** . Free ( 1, real)

   383 *** . Free ( aaa, nat) .......................... nat !!! *)

   384  val thm = num_str realpow_eq_one;

   385  val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;

   386 (*val t = Free ("1","RealDef.real") : term*)

   388 " ================= calculate.sml: calculate_ 2002 =================== ";

   389 " ================= calculate.sml: calculate_ 2002 =================== ";

   390 " ================= calculate.sml: calculate_ 2002 =================== ";

   392 val thy = Test.thy;

   393 val t = (term_of o the o (parse thy)) "12 / 3";

   394 val Some (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"divide_")))t;

   395 val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;

   396 "12 / 3 = 4";

   397 val thy = Test.thy;

   398 val t = (term_of o the o (parse thy)) "4 ^^^ 2";

   399 val Some (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_"))) t;

   400 val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;

   401 "4 ^ 2 = 16";

   403  val t = (term_of o the o (parse thy)) "((1 + 2) * 4 / 3) ^^^ 2";

   404  val Some (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"plus"))) t;

   405 "1 + 2 = 3";

   406  val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;

   407  Sign.string_of_term (sign_of thy) t;

   408 "(3 * 4 / 3) ^^^ 2";

   409  val Some (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"times")))t;

   410 "3 * 4 = 12";

   411  val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;

   412  Sign.string_of_term (sign_of thy) t;

   413 "(12 / 3) ^^^ 2";

   414  val Some (thmID,thm) =get_calculation_ thy(the(assoc(calclist,"divide_")))t;

   415 "12 / 3 = 4";

   416  val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;

   417  Sign.string_of_term (sign_of thy) t;

   418 "4 ^^^ 2";

   419  val Some (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_")))t;

   420 "4 ^^^ 2 = 16";

   421  val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;

   422  Sign.string_of_term (sign_of thy) t;

   423 "16";

   424  if it <> "16" then error "calculate.sml: new behaviour in calculate_"

   425  else ();

   427 (*13.9.02 *** calc: operator = pow not defined*)

   428   val t = (term_of o the o (parse thy)) "3^^^2";

   429   val Some (thmID,thm) =

   430       get_calculation_ thy (the(assoc(calclist,"power_"))) t;

   431 (*** calc: operator = pow not defined*)

   433   val (op_, eval_fn) = the (assoc(calclist,"power_"));

   434   (*

   435 val op_ = "Atools.pow" : string

   436 val eval_fn = fn : string -> term -> theory -> (string * term) option*)

   438   val Some (thmid,t') = get_pair thy op_ eval_fn t;

   439 (*** calc: operator = pow not defined*)

   441   val Some (id,t') = eval_fn op_ t thy;

   442 (*** calc: operator = pow not defined*)

   444   val (thmid, (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) = (op_, t);

   445   val Some (id,t') = eval_binop thmid op_ t thy;

   446 (*** calc: operator = pow not defined*)

   449 "----------- get_pair with 3 args --------------------------------";

   450 "----------- get_pair with 3 args --------------------------------";

   451 "----------- get_pair with 3 args --------------------------------";

   452 val (thy, op_, ef, arg) =

   453     (thy, "EqSystem.occur'_exactly'_in",

   454      snd (the (assoc(!calclist',"occur_exactly_in"))),

   455      str2term

   456       "[] from_ [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) / 2"

   457       );

   458 val Some (str, simpl) = get_pair thy op_ ef arg;

   459 if str =

   460 "[] from_ [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) / 2 = True"

   461 then () else error "calculate.sml get_pair with 3 args:occur_exactly_in";

   465 " ================= eval_binop Float  =================== ";

   466 val t = str2term "Float ((1,2),(0,0))";

   467 atomty t;

   468 val Const ("Float.Float",_) $

   469 	  (Const ("Pair",_) $

   470 		 (Const ("Pair",_) $ Free (i1,_) $ Free (i2,_)) $ _) = t;

   472 val t = str2term "Float ((1,2),(0,0)) * Float ((3,4),(0,0))";

   473 atomty t;

   474 (*WN.10.4.03 eval_binop Float *)

   477 "------------------ 3.6.03 (2 * x is_const) ---------------------------";

   478 "------------------ 3.6.03 (2 * x is_const) ---------------------------";

   479 "------------------ 3.6.03 (2 * x is_const) ---------------------------";

   480 val t = str2term "2 * x is_const";

   481 val Some (str, t') = eval_const "" "" t Test.thy;

   482 term2str t';

   483 "(2 * x is_const) = False";

   485 val Some (t',_) = rewrite_set_ Test.thy false tval_rls t;

   486 term2str t';

   487 "False";

   488 ===== inhibit exn ?===========================================================*)

author	Walther Neuper <neuper@ist.tugraz.at>
	Tue, 28 Sep 2010 09:06:56 +0200
branch	isac-update-Isa09-2
changeset 38031	460c24a6a6ba
parent 38022	e6d356fc4d38
child 38032	121765ba0a34
permissions	-rw-r--r--