wneuper/isac: src/sml/Scripts/scrtools.sml@9acb256f8a40

     1 (* tools which depend on Script.thy and thus are not in term_G.sml

     2    (c) Walther Neuper 2000

     4 use"Scripts/scrtools.sml";

     5 use"scrtools.sml";

     6 *)

     9 fun is_reall_dsc

    10   (Const(_,Type("fun",[Type("List.list",

    11 			    [Type ("real",[])]),_]))) = true

    12   | is_reall_dsc

    13   (Const(_,Type("fun",[Type("List.list",

    14 			    [Type ("real",[])]),_])) $ t) = true

    15   | is_reall_dsc _ = false;

    16 fun is_booll_dsc

    17   (Const(_,Type("fun",[Type("List.list",

    18 			    [Type ("bool",[])]),_]))) = true

    19   | is_booll_dsc

    20   (Const(_,Type("fun",[Type("List.list",

    21 			    [Type ("bool",[])]),_])) $ t) = true

    22   | is_booll_dsc _ = false;

    23 (*

    24 > val t = (term_of o the o (parse thy)) "relations";

    25 > atomtyp (type_of t);

    26 *** Type (fun,[

    27 ***   Type (List.list,[

    28 ***     Type (bool,[])

    29 ***     ]

    30 ***   Type (Tools.una,[])

    31 ***   ]

    32 > is_booll_dsc t;

    33 val it = true : bool

    34 > is_reall_dsc t;

    35 val it = false : bool

    36 *)

    38 fun is_list_dsc (Const(_,Type("fun",[Type("List.list",_),_]))) = true

    39   | is_list_dsc (Const(_,Type("fun",[Type("List.list",_),_])) $ t) = true

    40   (*WN:8.5.03: ???                                           ~~~~ ???*)

    41   | is_list_dsc _ = false;

    42 (*

    43 > val t = str2term "someList";

    44 > is_list_dsc t;

    45 val it = true : bool

    47 > val t = (term_of o the o (parse thy))

    48           "additional_relations [a=b,c=(d::real)]";

    49 > is_list_dsc t;

    50 val it = true : bool

    51 > is_list_dsc (head_of t);

    52 val it = true : bool

    54 > val t = (term_of o the o (parse thy))"max_relation (A=#2*a*b-a^^^#2)";

    55 > is_list_dsc t;

    56 val it = false : bool

    57 > is_list_dsc (head_of t);

    58 val it = false : bool

    59 > val t = (term_of o the o (parse thy)) "testdscforlist";

    60 > is_list_dsc (head_of t);

    61 val it = true : bool

    62 *)

    65 fun is_unl (Const(_,Type("fun",[_,Type("Tools.unl",_)]))) = true

    66   | is_unl _ = false;

    67 (*

    68 > val t = str2term "someList"; is_unl t;

    69 val it = true : bool

    70 > val t = (term_of o the o (parse thy)) "maximum";

    71 > is_unl t;

    72 val it = false : bool

    73 *)

    75 fun is_dsc (Const(_,Type("fun",[_,Type("Tools.nam",_)]))) = true

    76   | is_dsc (Const(_,Type("fun",[_,Type("Tools.una",_)]))) = true

    77   | is_dsc (Const(_,Type("fun",[_,Type("Tools.unl",_)]))) = true

    78   | is_dsc (Const(_,Type("fun",[_,Type("Tools.str",_)]))) = true

    79   | is_dsc (Const(_,Type("fun",[_,Type("Tools.toreal",_)]))) = true

    80   | is_dsc (Const(_,Type("fun",[_,Type("Tools.toreall",_)])))= true

    81   | is_dsc (Const(_,Type("fun",[_,Type("Tools.tobooll",_)])))= true

    82   | is_dsc (Const(_,Type("fun",[_,Type("Tools.unknow",_)])))= true

    83   | is_dsc (Const(_,Type("fun",[_,Type("Tools.cpy",_)])))= true

    84   | is_dsc _ = false;

    85 fun is_dsc term =

    86     (case (range_type o type_of) term of

    87 	Type("Tools.nam",_) => true

    88       | Type("Tools.una",_) => true

    89       | Type("Tools.unl",_) => true

    90       | Type("Tools.str",_) => true

    91       | Type("Tools.toreal",_) => true

    92       | Type("Tools.toreall",_) => true

    93       | Type("Tools.tobooll",_) => true

    94       | Type("Tools.unknow",_) => true

    95       | Type("Tools.cpy",_) => true

    96       | _ => false)

    97     handle Match => false;

   100 (*

   101 val t as t1 $ t2 = str2term "antiDerivativeName M_b";

   102 val Const (_, Type ("fun", [Type ("fun", _), Type ("Tools.una",[])])) $ _ = t;

   103 is_dsc t1;

   105 > val t = (term_of o the o (parse thy)) "maximum";

   106 > is_dsc t;

   107 val it = true : bool

   108 > val t = (term_of o the o (parse thy)) "testdscforlist";

   109 > is_dsc t;

   110 val it = true : bool

   112 > val t = (head_of o term_of o the o (parse thy)) "maximum A";

   113 > is_dsc t;

   114 val it = true : bool

   115 > val t = (head_of o term_of o the o (parse thy))

   116   "fixedValues [R=(R::real)]";

   117 > is_dsc t;

   118 val it = true : bool

   119 *)

   122 (*make the term 'Subproblem (domID, pblID)' to a formula for frontend;

   123   needs to be here after def. Subproblem in Script.thy*)

   124 val t as (subpbl_t $ (pair_t $ Free (domID,_) $ pblID)) =

   125     (term_of o the o (parse Script.thy))

   126 	"Subproblem (Isac,[equation,univar])";

   127 val t as (pbl_t $ _) =

   128     (term_of o the o (parse Script.thy))

   129 	"Problem (Isac,[equation,univar])";

   130 val Free (_, ID_type) = (term_of o the o (parse Script.thy)) "x::ID";

   133 fun subpbl domID pblID =

   134     subpbl_t $ (pair_t $ Free (domID,ID_type) $

   135 	(((list2isalist ID_type) o (map (mk_free ID_type))) pblID));

   136 (*> subpbl "Isac" ["equation","univar"] = t;

   137 val it = true : bool *)

   140 fun pblterm (domID:domID) (pblID:pblID) =

   141     pbl_t $ (pair_t $ Free (domID,ID_type) $

   142 	(((list2isalist ID_type) o (map (mk_free ID_type))) pblID));

   145 (**.construct scr-env from scr(created automatically) and Rewrite_Set.**)

   147 fun one_scr_arg (Const _ $ arg $ _) = arg

   148   | one_scr_arg t = raise error ("one_scr_arg: called by "^(term2str t));

   149 fun two_scr_arg (Const _ $ a1 $ a2 $ _) = (a1, a2)

   150   | two_scr_arg t = raise error ("two_scr_arg: called by "^(term2str t));

   153 (**.generate calc from a script.**)

   155 (*.instantiate a stactic or scriptexpr, and ev. attach (curried) argument

   156 args:

   157    E       environment

   158    v       current value, is attached to curried stactics

   159    stac     stactic to be instantiated

   160 precond:

   161    not (a = None) /\ (v = e_term) /\ (stac curried, i.e. without last arg.)

   162    this ........................ is the initialization for assy with l=[],

   163    but the 1st stac is

   164    (a) curried:     then (a = Some _), or

   165    (b) not curried: then the values of the initialization are not used

   166 .*)

   167 datatype stacexpr = STac of term | Expr of term

   168 fun rep_stacexpr (STac t ) = t

   169   | rep_stacexpr (Expr t) =

   170     raise error ("rep_stacexpr called with t= "^(term2str t));

   172 type env = (term * term) list;

   174 (*update environment; t <> empty if coming from listexpr*)

   175 fun upd_env (env:env) (v,t) =

   176   let val env' = if t = e_term then env else overwrite (env,(v,t));

   177     (*val _= writeln("### upd_env: = "^(subst2str env'));*)

   178   in env' end;

   180 (*.substitute the scripts environment in a leaf of the scripts parse-tree

   181    and attach the curried argument of a tactic, if any.

   182    a leaf is either a tactic or an 'exp' in 'let v = expr'

   183    where 'exp' does not contain a tactic.

   184 CAUTION: (1) currying with @@ requires 2 patterns for each tactic

   185          (2) the non-curried version must return None for a

   186 	 (3) non-matching patterns become an Expr by fall-through.

   187 WN060906 quick and dirty fix: due to (2) a is returned, too.*)

   188 fun subst_stacexpr E a v (t as (Const ("Script.Rewrite",_) $ _ $ _ $ _ ))=

   189     (None, STac (subst_atomic E t))

   191   | subst_stacexpr E a v (t as (Const ("Script.Rewrite",_) $ _ $ _ ))=

   192     (a, (*in these cases we hope, that a = Some _*)

   193      STac (case a of Some a' => (subst_atomic E (t $ a'))

   194 		   | None => ((subst_atomic E t) $ v)))

   196   | subst_stacexpr E a v

   197 	      (t as (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ $ _ )) =

   198     (None, STac (subst_atomic E t))

   200   | subst_stacexpr E a v (t as (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _))=

   201     (a, STac (case a of Some a' => subst_atomic E (t $ a')

   202 	     | None => ((subst_atomic E t) $ v)))

   204   | subst_stacexpr E a v (t as (Const ("Script.Rewrite'_Set",_) $ _ $ _ $ _ ))=

   205     (None, STac (subst_atomic E t))

   207   | subst_stacexpr E a v (t as (Const ("Script.Rewrite'_Set",_) $ _ $ _ )) =

   208     (a, STac (case a of Some a' => subst_atomic E (t $ a')

   209 	     | None => ((subst_atomic E t) $ v)))

   211   | subst_stacexpr E a v

   212 	      (t as (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ $ _ )) =

   213     (None, STac (subst_atomic E t))

   215   | subst_stacexpr E a v

   216 	      (t as (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ )) =

   217     (a, STac (case a of Some a' => subst_atomic E (t $ a')

   218 	     | None => ((subst_atomic E t) $ v)))

   220   | subst_stacexpr E a v (t as (Const ("Script.Calculate",_) $ _ $ _ )) =

   221     (None, STac (subst_atomic E t))

   223   | subst_stacexpr E a v (t as (Const ("Script.Calculate",_) $ _ )) =

   224     (a, STac (case a of Some a' => subst_atomic E (t $ a')

   225 	     | None => ((subst_atomic E t) $ v)))

   227   | subst_stacexpr E a v

   228 	      (t as (Const("Script.Check'_elementwise",_) $ _ $ _ )) =

   229     (None, STac (subst_atomic E t))

   231   | subst_stacexpr E a v (t as (Const("Script.Check'_elementwise",_) $ _ )) =

   232     (a, STac (case a of Some a' => subst_atomic E (t $ a')

   233 		 | None => ((subst_atomic E t) $ v)))

   235   | subst_stacexpr E a v (t as (Const("Script.Or'_to'_List",_) $ _ )) =

   236     (None, STac (subst_atomic E t))

   238   | subst_stacexpr E a v (t as (Const("Script.Or'_to'_List",_))) = (*t $ v*)

   239     (a, STac (case a of Some a' => subst_atomic E (t $ a')

   240 		 | None => ((subst_atomic E t) $ v)))

   242   | subst_stacexpr E a v (t as (Const ("Script.SubProblem",_) $ _ $ _ )) =

   243     (None, STac (subst_atomic E t))

   245   | subst_stacexpr E a v (t as (Const ("Script.Take",_) $ _ )) =

   246     (None, STac (subst_atomic E t))

   248   | subst_stacexpr E a v (t as (Const ("Script.Substitute",_) $ _ $ _ )) =

   249     (None, STac (subst_atomic E t))

   251   | subst_stacexpr E a v (t as (Const ("Script.Substitute",_) $ _ )) =

   252     (a, STac (case a of Some a' => subst_atomic E (t $ a')

   253 		 | None => ((subst_atomic E t) $ v)))

   255   (*now all tactics are matched out and this leaf must be without a tactic*)

   256   | subst_stacexpr E a v t =

   257     (a, Expr (subst_atomic (case a of Some a => upd_env E (a,v)

   258 				| None => E) t));

   259 (*> val t = str2term "SubProblem(Test_, [linear, univariate, equation, test], [Test, solve_linear]) [bool_ e_, real_ v_]";

   260 > subst_stacexpr [] None e_term t;*)

   263 fun stacpbls (h $ body) =

   264   let

   265     fun scan ts (Const ("Let",_) $ e $ (Abs (v,T,b))) =

   266       (scan ts e) @ (scan ts b)

   267       | scan ts (Const ("If",_) $ c $ e1 $ e2) = (scan ts e1) @ (scan ts e2)

   268       | scan ts (Const ("Script.While",_) $ c $ e $ _) = scan ts e

   269       | scan ts (Const ("Script.While",_) $ c $ e) = scan ts e

   270       | scan ts (Const ("Script.Repeat",_) $ e $ _) = scan ts e

   271       | scan ts (Const ("Script.Repeat",_) $ e) = scan ts e

   272       | scan ts (Const ("Script.Try",_) $ e $ _) = scan ts e

   273       | scan ts (Const ("Script.Try",_) $ e) = scan ts e

   274       | scan ts (Const ("Script.Or",_) $e1 $ e2 $ _) =

   275 	(scan ts e1) @ (scan ts e2)

   276       | scan ts (Const ("Script.Or",_) $e1 $ e2) =

   277 	(scan ts e1) @ (scan ts e2)

   278       | scan ts (Const ("Script.Seq",_) $e1 $ e2 $ _) =

   279 	(scan ts e1) @ (scan ts e2)

   280       | scan ts (Const ("Script.Seq",_) $e1 $ e2) =

   281 	(scan ts e1) @ (scan ts e2)

   282       | scan ts t = case subst_stacexpr [] None e_term t of

   283 			(_, STac _) => [t] | (_, Expr _) => []

   284   in (distinct o (scan [])) body end;

   285     (*sc = Solve_root_equation ...

   286 > val ts = stacpbls sc;

   287 > writeln (terms2str thy ts);

   288 ["Rewrite square_equation_left True e_",

   289  "Rewrite_Set SqRoot_simplify False e_",

   290  "Rewrite_Set rearrange_assoc False e_",

   291  "Rewrite_Set isolate_root False e_",

   292  "Rewrite_Set norm_equation False e_",

   293  "Rewrite_Set_Inst [(bdv, v_)] isolate_bdv False e_"]

   294 *)

   298 fun is_calc (Const ("Script.Calculate",_) $ _) = true

   299   | is_calc (Const ("Script.Calculate",_) $ _ $ _) = true

   300   | is_calc _ = false;

   301 fun op_of_calc (Const ("Script.Calculate",_) $ Free (op_,_)) = op_

   302   | op_of_calc (Const ("Script.Calculate",_) $ Free (op_,_) $ _) = op_

   303   | op_of_calc t = raise error ("op_of_calc called with"^term2str t);

   305 (*######################################################################

   307  val Script sc = (#scr o rep_rls) Test_simplify;

   308  val stacs = stacpbls sc;

   310  val calcs = filter is_calc stacs;

   311  val ids = map op_of_calc calcs;

   312  map (curry assoc1 (!calclist')) ids;

   314  (((map (curry assoc1 (!calclist'))) o (map op_of_calc) o

   315   (filter is_calc) o stacpbls) sc):calc list;

   317 ######################################################################*)

   319 (**.for automatic creation of scripts from rls.**)

   321 val ScrStep $ _ $ _ =     (*'z not affected by parse: 'a --> real*)

   322     ((inst_abs thy) o term_of o the o (parse thy))

   323 	"Script Stepwise (t_::'z) =\

   324         \(Repeat\

   325 	\  ((Try (Repeat (Rewrite real_diff_minus False))) @@  \

   326 	\   (Try (Repeat (Rewrite real_add_commute False))) @@ \

   327 	\   (Try (Repeat (Rewrite real_mult_commute False))))  \

   328 	\  t_)";

   329 (*WN060605 script-arg (t_::'z) and "Free (t_, 'a)" at end of body

   330 are inconsistent !!!*)

   331 val ScrStep_inst $ Term $ Bdv $ _=(*'z not affected by parse: 'a --> real*)

   332     ((inst_abs thy) o term_of o the o (parse thy))

   333 	"Script Stepwise_inst (t_::'z) (v_::real) =\

   334         \(Repeat\

   335 	\  ((Try (Repeat (Rewrite_Inst [(bdv,v_)] real_diff_minus False))) @@ \

   336 	\   (Try (Repeat (Rewrite_Inst [(bdv,v_)] real_add_commute False))) @@\

   337 	\   (Try (Repeat (Rewrite_Inst [(bdv,v_)] real_mult_commute False)))) \

   338 	\  t_)";

   339 val Repeat $ _ =

   340     ((inst_abs thy) o term_of o the o (parseN thy))

   341 	"Repeat (Rewrite real_diff_minus False t_)";

   342 val Try $ _ =

   343     ((inst_abs thy) o term_of o the o (parseN thy))

   344 	"Try (Rewrite real_diff_minus False t_)";

   345 val Cal $ _ =

   346     ((inst_abs thy) o term_of o the o (parseN thy))

   347 	"Calculate plus";

   348 val Rew $ (Free (_,IDtype)) $ _ $ t_ =

   349     ((inst_abs thy) o term_of o the o (parseN thy))

   350 	"Rewrite real_diff_minus False t_";

   351 val Rew_Inst $ Subs $ _ $ _ =

   352     ((inst_abs thy) o term_of o the o (parseN thy))

   353 	"Rewrite_Inst [(bdv,v_)] real_diff_minus False";

   354 val Rew_Set $ _ $ _ =

   355     ((inst_abs thy) o term_of o the o (parseN thy))

   356 	"Rewrite_Set real_diff_minus False";

   357 val Rew_Set_Inst $ _ $ _ $ _ =

   358     ((inst_abs thy) o term_of o the o (parseN thy))

   359 	"Rewrite_Set_Inst [(bdv,v_)] real_diff_minus False";

   360 val SEq $ _ $ _ $ _ =

   361     ((inst_abs thy) o term_of o the o (parseN thy))

   362 	"  ((Try (Repeat (Rewrite real_diff_minus False))) @@  \

   363         \   (Try (Repeat (Rewrite real_add_commute False))) @@ \

   364         \   (Try (Repeat (Rewrite real_mult_commute False)))) t_";

   366 fun rule2stac _ (Thm (thmID, _)) =

   367     Try $ (Repeat $ (Rew $ Free (thmID, IDtype) $ HOLogic.false_const))

   368   | rule2stac calc (Calc (c, _)) =

   369     Try $ (Repeat $ (Cal $ Free (assoc_calc (calc ,c), IDtype)))

   370   | rule2stac _ (Rls_ rls) =

   371     Try $ (Rew_Set $ Free (id_rls rls, IDtype) $ HOLogic.false_const);

   372 (*val t = rule2stac [] (Thm ("real_diff_minus", num_str real_diff_minus));

   373 atomt t; term2str t;

   374 val t = rule2stac calclist (Calc ("op +", eval_binop "#add_"));

   375 atomt t; term2str t;

   376 val t = rule2stac [] (Rls_ rearrange_assoc);

   377 atomt t; term2str t;

   378 *)

   379 fun rule2stac_inst _ (Thm (thmID, _)) =

   380     Try $ (Repeat $ (Rew_Inst $ Subs $ Free (thmID, IDtype) $

   381 			      HOLogic.false_const))

   382   | rule2stac_inst calc (Calc (c, _)) =

   383     Try $ (Repeat $ (Cal $ Free (assoc_calc (calc ,c), IDtype)))

   384   | rule2stac_inst _ (Rls_ rls) =

   385     Try $ (Rew_Set_Inst $ Subs $ Free (id_rls rls, IDtype) $

   386 			HOLogic.false_const);

   387 (*val t = rule2stac_inst [] (Thm ("real_diff_minus", num_str real_diff_minus));

   388 atomt t; term2str t;

   389 val t = rule2stac_inst calclist (Calc ("op +", eval_binop "#add_"));

   390 atomt t; term2str t;

   391 val t = rule2stac_inst [] (Rls_ rearrange_assoc);

   392 atomt t; term2str t;

   393 *)

   395 (*for appropriate nesting take stacs in _reverse_ order*)

   396 fun @@@ sts [s] = SEq $ s $ sts

   397   | @@@ sts (s::ss) = @@@ (SEq $ s $ sts) ss;

   398 fun @@ [stac] = stac

   399   | @@ [s1, s2] = SEq $ s1 $ s2 (*---------vvv--*)

   400   | @@ stacs =

   401     let val s3::s2::ss = rev stacs

   402     in @@@ (SEq $ s2 $ s3) ss end;

   403 (*

   404  val rules = (#rules o rep_rls) isolate_root;

   405  val rs = map (rule2stac calclist) rules;

   406  val tt = @@ rs;

   407  atomt tt; writeln (term2str tt);

   408  *)

   410 val contains_bdv = (not o null o (filter is_bdv) o ids2str o #prop o rep_thm);

   412 (*.does a rule contain a 'bdv'; descend recursively into Rls_.*)

   413 fun contain_bdv [] = false

   414   | contain_bdv (Thm (_, thm)::rs) =

   415     if (not o contains_bdv) thm

   416     then contain_bdv rs

   417     else true

   418   | contain_bdv (Calc _ ::rs) = contain_bdv rs

   419   | contain_bdv (Rls_ rls ::rs) =

   420     contain_bdv (get_rules rls) orelse contain_bdv rs

   421   | contain_bdv (r::_) =

   422     raise error ("contain_bdv called with ["^(id_rule r)^",...]");

   425 fun rules2scr_Rls calc rules =

   426     if contain_bdv rules

   427     then ScrStep_inst $ Term $ Bdv $

   428 	 (Repeat $ (((@@ o (map (rule2stac_inst calc))) rules) $ t_))

   429     else ScrStep $ Term $

   430 	 (Repeat $ (((@@ o (map (rule2stac      calc))) rules) $ t_));

   431 fun rules2scr_Seq calc rules =

   432     if contain_bdv rules

   433     then ScrStep_inst $ Term $ Bdv $

   434 	 (((@@ o (map (rule2stac_inst calc))) rules) $ t_)

   435     else ScrStep $ Term $

   436 	 (((@@ o (map (rule2stac      calc))) rules) $ t_);

   438 (*.prepare the input for an rls for use:

   439    # generate a script for stepwise execution of the rls

   440    # filter the operators for Calc out of the script

   441    !!!use this function in ruleset' := !!! .*)

   442 fun prep_rls Erls = raise error "prep_rls not impl. for Erls"

   443   | prep_rls (Rls {id,preconds,rew_ord,erls,srls,calc,rules,...}) =

   444     let val sc = (rules2scr_Rls (!calclist') rules)

   445     in Rls {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,

   446 	    srls=srls,

   447 	    calc = (*FIXXXME.040207 use also for met*)

   448 	    ((map (curry assoc1 (!calclist'))) o (map op_of_calc) o

   449 	     (filter is_calc) o stacpbls) sc,

   450 	    rules=rules,

   451 	    scr = Script sc} end

   452   | prep_rls (Seq {id,preconds,rew_ord,erls,srls,calc,rules,...}) =

   453     let val sc = (rules2scr_Seq (!calclist') rules)

   454     in Seq {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,

   455 	 srls=srls,

   456 	    calc = ((map (curry assoc1 (!calclist'))) o (map op_of_calc) o

   457 		    (filter is_calc) o stacpbls) sc,

   458 	 rules=rules,

   459 	 scr = Script sc} end

   460   | prep_rls (Rrls {id,...}) =

   461     raise error ("prep_rls not required for Rrls \""^id^"\"");

   462 (*

   463  val Script sc = (#scr o rep_rls o prep_rls) isolate_root;

   464  (writeln o term2str) sc;

   465  val Script sc = (#scr o rep_rls o prep_rls) isolate_bdv;

   466  (writeln o term2str) sc;

   467   *)

author	wneuper
	Fri, 28 Dec 2007 14:57:38 +0100
branch	start-work-070517
changeset 266	9acb256f8a40
permissions	-rw-r--r--