1.1 --- a/src/Tools/isac/Interpret/mstools.sml Wed May 29 14:22:31 2019 +0200
1.2 +++ b/src/Tools/isac/Interpret/mstools.sml Thu May 30 12:04:55 2019 +0200
1.3 @@ -33,8 +33,6 @@
1.4 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
1.5 val pblID_of_match : match -> Celem.pblID
1.6 val refined_IDitms : match list -> match option
1.7 - val prep_program : thm -> term
1.8 -(*val prep_program : theory -> string -> term *)
1.9 end
1.10
1.11 structure Stool(**) : SPECIFY_TOOL(**) =
1.12 @@ -135,17 +133,6 @@
1.13 val caller_ctxt = (scrval |> Model.dest_list' |> insert_assumptions) caller_ctxt
1.14 in transfer_asms_from_to sub_ctxt caller_ctxt end;
1.15
1.16 -(* prepare program for Lucas-Interpretation *)
1.17 -(* version introduced BEFORE switch to partial_function *)
1.18 -fun prep_program thy str = (TermC.inst_abs o Thm.term_of o the o (TermC.parse thy)) str
1.19 -(* version for later switch to partial_function *)
1.20 -fun prep_program thm = (thm
1.21 - |> Thm.prop_of
1.22 - |> HOLogic.dest_Trueprop
1.23 - |> Logic.unvarify_global
1.24 - |> TermC.inst_abs)
1.25 - handle TERM _ => raise TERM ("prep_program", [Thm.prop_of thm])
1.26 -
1.27 fun common_subthy (thy1, thy2) =
1.28 if Context.subthy (thy1, thy2) then thy2
1.29 else if Context.subthy (thy2, thy1) then thy1
2.1 --- a/src/Tools/isac/Interpret/ptyps.sml Wed May 29 14:22:31 2019 +0200
2.2 +++ b/src/Tools/isac/Interpret/ptyps.sml Thu May 30 12:04:55 2019 +0200
2.3 @@ -369,7 +369,7 @@
2.4 | ((_, wh') :: []) => (map (TermC.parse_patt thy) wh'
2.5 handle _ => error ("prep_pbt: syntax error in '#Where' of " ^ strs2str metID))
2.6 | _ => error ("prep_pbt: more than one '#Where' in " ^ strs2str metID));
2.7 - val sc = Stool.prep_program scr
2.8 + val sc = LTool.prep_program scr
2.9 val calc = if Thm.eq_thm (scr, @{thm refl}) then [] else LTool.get_calcs thy sc
2.10 in
2.11 ({guh = guh, mathauthors = maa, init = init, ppc = gi @ fi @ re, pre = wh, rew_ord' = ro,
3.1 --- a/src/Tools/isac/Interpret/script.sml Wed May 29 14:22:31 2019 +0200
3.2 +++ b/src/Tools/isac/Interpret/script.sml Thu May 30 12:04:55 2019 +0200
3.3 @@ -189,7 +189,7 @@
3.4 (* version to be replaced during switch to partial_function *)
3.5 fun formal_args scr = (fst o split_last o snd o strip_comb) scr;
3.6 (* version for later switch to partial_function *)
3.7 -fun formal_args tm = (tm
3.8 +fun formal_args tm = (tm (*TODO move to scrtools.sml*)
3.9 |> HOLogic.dest_eq
3.10 |> fst
3.11 |> strip_comb
4.1 --- a/src/Tools/isac/Knowledge/Test_Build_Thydata.thy Wed May 29 14:22:31 2019 +0200
4.2 +++ b/src/Tools/isac/Knowledge/Test_Build_Thydata.thy Thu May 30 12:04:55 2019 +0200
4.3 @@ -52,7 +52,7 @@
4.4 ("dummy_ord", _), rules = [], scr = EmptyScr, srls = Erls},
4.5 errpatts = [], id = "rls111", preconds = [], rew_ord = ("termlessI", _), rules =
4.6 [Thm ("thm111", _), Thm ("refl", _)], scr =
4.7 - Prog (Const ("Script.Stepwise", _) $ Free ("t_t", _) $ _),
4.8 + Prog (Const ("HOL.eq", _) $ (Const ("Atools.auto_generated", _) $ Free ("t_t", _)) $ _),
4.9 srls = Erls})) => ()
4.10 | _ => error "test/../thy-hierarchy CHANGED 4";
4.11 \<close> ML \<open>
4.12 @@ -65,7 +65,7 @@
4.13 errpatts = [], id = "rls222", preconds = [], rew_ord = ("termlessI", _), rules =
4.14 [Thm ("sym_thm111", _), Thm ("o_def", _)],
4.15 scr =
4.16 - Prog (Const ("Script.Stepwise", _) $ Free ("t_t", _) $ _),
4.17 + Prog (Const ("HOL.eq", _) $ (Const ("Atools.auto_generated", _) $ Free ("t_t", _)) $ _),
4.18 srls = Erls})) => ()
4.19 | _ => error "test/../thy-hierarchy CHANGED 5";
4.20 \<close>
5.1 --- a/src/Tools/isac/ProgLang/Atools.thy Wed May 29 14:22:31 2019 +0200
5.2 +++ b/src/Tools/isac/ProgLang/Atools.thy Thu May 30 12:04:55 2019 +0200
5.3 @@ -6,6 +6,10 @@
5.4 theory Atools imports Descript Script
5.5 begin
5.6
5.7 +partial_function (tailrec) auto_generated :: "'z \<Rightarrow> 'z"
5.8 + where "auto_generated t_t = t_t"
5.9 +partial_function (tailrec) auto_generated_inst :: "'z \<Rightarrow> real \<Rightarrow> 'z"
5.10 + where "auto_generated_inst t_t v = t_t"
5.11 ML_file "~~/src/Tools/isac/ProgLang/scrtools.sml"
5.12
5.13 consts
6.1 --- a/src/Tools/isac/ProgLang/scrtools.sml Wed May 29 14:22:31 2019 +0200
6.2 +++ b/src/Tools/isac/ProgLang/scrtools.sml Thu May 30 12:04:55 2019 +0200
6.3 @@ -27,12 +27,15 @@
6.4 val op_of_calc: term -> string
6.5 val get_calcs: theory -> term -> (Rule.prog_calcID * (Rule.calID * Rule.eval_fn)) list
6.6 val prep_rls: theory -> Rule.rls -> Rule.rls
6.7 + val prep_program : thm -> term
6.8 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
6.9 (* NONE *)
6.10 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
6.11 val rule2stac: theory -> Rule.rule -> term
6.12 val rule2stac_inst: theory -> Rule.rule -> term
6.13 val @@ : term list -> term
6.14 + val rules2scr_Rls : theory -> Rule.rule list -> term
6.15 + val rules2scr_Seq : theory -> Rule.rule list -> term
6.16 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
6.17 end
6.18
6.19 @@ -41,6 +44,17 @@
6.20 struct
6.21 (**)
6.22
6.23 +(* prepare program for Lucas-Interpretation *)
6.24 +(* version introduced BEFORE switch to partial_function *)
6.25 +fun prep_program thy str = (TermC.inst_abs o Thm.term_of o the o (TermC.parse thy)) str
6.26 +(* version for later switch to partial_function *)
6.27 +fun prep_program thm = (thm
6.28 + |> Thm.prop_of
6.29 + |> HOLogic.dest_Trueprop
6.30 + |> Logic.unvarify_global
6.31 + |> TermC.inst_abs)
6.32 + handle TERM _ => raise TERM ("prep_program", [Thm.prop_of thm])
6.33 +
6.34 (* distinguish input to Model (deep embedding of terms as Isac's object language) *)
6.35 fun is_reall_dsc (Const (_, Type("fun", [Type ("List.list", [Type ("Real.real", [])]), _]))) = true
6.36 | is_reall_dsc (Const (_, Type("fun", [Type ("List.list", [Type ("Real.real", [])]),_])) $ _) = true
6.37 @@ -89,11 +103,15 @@
6.38 fun_and_args |> strip_comb |> fst |> dest_Const
6.39 | get_fun_id t = raise TERM ("get_fun_id", [t])
6.40
6.41 +fun formal_args tm = (tm
6.42 + |> HOLogic.dest_eq
6.43 + |> fst
6.44 + |> strip_comb
6.45 + |> snd)
6.46 + handle TERM _ => raise TERM ("formal_args", [tm])
6.47 (* construct scr-env from scr(created automatically) and Rewrite_Set *)
6.48 -fun one_scr_arg (Const _ $ arg $ _) = arg
6.49 - | one_scr_arg t = error ("one_scr_arg: called by " ^ Rule.term2str t);
6.50 -fun two_scr_arg (Const _ $ a1 $ a2 $ _) = (a1, a2)
6.51 - | two_scr_arg t = error ("two_scr_arg: called by " ^ Rule.term2str t);
6.52 +fun one_scr_arg tm = nth 1 (formal_args tm);
6.53 +fun two_scr_arg tm = (nth 1 (formal_args tm), nth 2 (formal_args tm));
6.54
6.55
6.56 (** generate a "type calc" from a script **)
6.57 @@ -221,23 +239,9 @@
6.58 (** build up a program from rules **)
6.59
6.60 (* transform type rule to a term *)
6.61 -val ScrStep $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parse @{theory}))
6.62 - (*'z not affected by parse: 'a --> real*)
6.63 - "Script Stepwise (t_t::'z) =\
6.64 - \(Repeat\
6.65 - \ ((Try (Repeat (Rewrite ''real_diff_minus'' False))) @@ \
6.66 - \ (Try (Repeat (Rewrite ''add_commute'' False))) @@ \
6.67 - \ (Try (Repeat (Rewrite ''mult_commute'' False)))) \
6.68 - \ t_t)";
6.69 (*WN060605 script-arg (t_::'z) and "Free (t_, 'a)" at end of body are inconsistent !!!*)
6.70 -val ScrStep_inst $ Term $ Bdv $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parse @{theory}))
6.71 - (*'z not affected by parse: 'a --> real*)
6.72 - "Script Stepwise_inst (t_t::'z) (v::real) =\
6.73 - \(Repeat\
6.74 - \ ((Try (Repeat (Rewrite_Inst [(''bdv'',v)] ''real_diff_minus'' False))) @@ \
6.75 - \ (Try (Repeat (Rewrite_Inst [(''bdv'',v)] ''add_commute'' False))) @@\
6.76 - \ (Try (Repeat (Rewrite_Inst [(''bdv'',v)] ''mult_commute'' False)))) \
6.77 - \ t_t)";
6.78 +val (FunID_Term $ _) = prep_program @{thm auto_generated.simps}
6.79 +val (FunID_Term_Bdv $ _) = prep_program @{thm auto_generated_inst.simps}
6.80 val Repeat $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
6.81 "Repeat (Rewrite ''real_diff_minus'' False t)";
6.82 val Try $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
6.83 @@ -248,7 +252,7 @@
6.84 "Calculate1 ''PLUS''";
6.85 val Rew $ _ $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
6.86 "Rewrite ''real_diff_minus'' False t";
6.87 -(*this is specific to ScrStep_inst ...*)
6.88 +(*this is specific to FunHead_inst ...*)
6.89 val Rew_Inst $ Subs $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
6.90 "Rewrite_Inst [(''bdv'',v)] ''real_diff_minus'' False";
6.91 val Rew_Set $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
6.92 @@ -305,14 +309,12 @@
6.93
6.94 fun rules2scr_Rls thy rules = (*WN100816 t_ -> t_t like "Script Stepwise..*)
6.95 if contain_bdv rules
6.96 - then ScrStep_inst $ Term $ Bdv $ (Repeat $ (((@@ o (map (rule2stac_inst thy))) rules) $ Rule.e_term))
6.97 - else ScrStep $ Term $ (Repeat $ (((@@ o (map (rule2stac thy))) rules) $ Rule.e_term));
6.98 + then FunID_Term_Bdv $ (Repeat $ (((@@ o (map (rule2stac_inst thy))) rules) $ Rule.e_term))
6.99 + else FunID_Term $ (Repeat $ (((@@ o (map (rule2stac thy))) rules) $ Rule.e_term));
6.100 fun rules2scr_Seq thy rules = (*WN100816 t_ -> t_t like "Script Stepwise..*)
6.101 if contain_bdv rules
6.102 - then ScrStep_inst $ Term $ Bdv $
6.103 - (((@@ o (map (rule2stac_inst thy))) rules) $ Rule.e_term)
6.104 - else ScrStep $ Term $
6.105 - (((@@ o (map (rule2stac thy))) rules) $ Rule.e_term);
6.106 + then FunID_Term_Bdv $ (((@@ o (map (rule2stac_inst thy))) rules) $ Rule.e_term)
6.107 + else FunID_Term $ (((@@ o (map (rule2stac thy))) rules) $ Rule.e_term);
6.108
6.109 (* prepare the input for an rls for use:
6.110 # generate a script for stepwise execution of the rls
6.111 @@ -337,5 +339,6 @@
6.112 scr = Rule.Prog sc} end
6.113 | prep_rls _ (Rule.Rrls {id, ...}) =
6.114 error ("prep_rls: not required for Rrls \"" ^ id ^ "\"");
6.115 -
6.116 -end
6.117 \ No newline at end of file
6.118 +(**)
6.119 +end
6.120 +(**)
6.121 \ No newline at end of file
7.1 --- a/test/Tools/isac/ProgLang/scrtools.sml Wed May 29 14:22:31 2019 +0200
7.2 +++ b/test/Tools/isac/ProgLang/scrtools.sml Thu May 30 12:04:55 2019 +0200
7.3 @@ -10,7 +10,7 @@
7.4 "-------- test the same called by interSteps norm_Poly -----------";
7.5 "-------- test the same called by interSteps norm_Rational -------";
7.6 "-------- check auto-gen.script for Rewrite_Set_Inst -------------";
7.7 -"-------- how to stepwise construct Scripts ----------------------";
7.8 +"-------- how to stepwise construct Scripts -------";(*TODO remove -- partial_function is easier*)
7.9 "-------- distinguish input to Model -----------------------------------------";
7.10 "-------- fun subpbl, fun pblterm --------------------------------------------";
7.11 "-------- fun stacpbls, fun subst_stacexpr -----------------------------------";
7.12 @@ -21,6 +21,7 @@
7.13 "-------- Handle Var from parsing by partial_function ------------------------";
7.14 "-------- Compare program terms: from old parsing | from partial_function ----";
7.15 "-------- fun get_fun_id -----------------------------------------------------";
7.16 +"-------- fun rules2scr_Rls --------------------------------------------------";
7.17 "-----------------------------------------------------------------------------";
7.18 "-----------------------------------------------------------------------------";
7.19 "-----------------------------------------------------------------------------";
7.20 @@ -515,12 +516,12 @@
7.21 (*Output: val prog_'''' = ... $ (Const ("HOL.Let", "bool... )... $ Free ("e_e", "bool")) $ ...*)
7.22
7.23 (* (2) parsing by funpack: take the definition from test/../ProgLang/scrtools.thy *)
7.24 -val prog_part = (HOLogic.dest_Trueprop o Thm.prop_of) @{thm xxx.simps}
7.25 +val prog_part = (HOLogic.dest_Trueprop o Thm.prop_of) @{thm simplify.simps}
7.26 (*Output: val prog_part = ... $ (Const ("HOL.Let", "bool... )... $ Var (("e_e", 0), "bool")) $ ...*)
7.27 ;
7.28 Logic.unvarify_global: term -> term
7.29 ;
7.30 -val prog_part = (Logic.unvarify_global o HOLogic.dest_Trueprop o Thm.prop_of) @{thm xxx.simps};
7.31 +val prog_part = (Logic.unvarify_global o HOLogic.dest_Trueprop o Thm.prop_of) @{thm simplify.simps};
7.32 (*val prog_part = ... $ (Const ("HOL.Let", "bool... )... $ Var (("e_e", 0), "bool")) $ ...*)
7.33
7.34 (* (3) compare (1)..(2) *)
7.35 @@ -599,7 +600,6 @@
7.36 "-------- fun get_fun_id -----------------------------------------------------";
7.37 "-------- fun get_fun_id -----------------------------------------------------";
7.38 "-------- fun get_fun_id -----------------------------------------------------";
7.39 -(* version for later switch to partial_function *--------------------------------\\)
7.40 (* fun_id is nested into arguments, compare ... *)
7.41 val Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $
7.42 (((((Const (const_id, const_typ) $ _) $ _) $ _) $ _) $ _) $ _) =
7.43 @@ -633,4 +633,20 @@
7.44 case get_fun_id (Thm.prop_of @{thm simplify.simps}) of
7.45 ("PolyMinus.simplify", _) => ()
7.46 | _ => error "get_fun_id changed";
7.47 -( * version for later switch to partial_function *--------------------------------//*)
7.48 \ No newline at end of file
7.49 +
7.50 +"-------- fun rules2scr_Rls --------------------------------------------------";
7.51 +"-------- fun rules2scr_Rls --------------------------------------------------";
7.52 +"-------- fun rules2scr_Rls --------------------------------------------------";
7.53 +(*compare Atools.*)
7.54 +val prog = LTool.rules2scr_Rls @{theory} [Rule.Thm ("thm111", @{thm thm111}), Rule.Thm ("refl", @{thm refl})]
7.55 +;
7.56 +writeln (t2str @{theory} prog);
7.57 +(*auto_generated t_t =
7.58 +Repeat
7.59 + ((Try (Repeat (Rewrite ''thm111'' False)) @@
7.60 + Try (Repeat (Rewrite ''refl'' False)))
7.61 + ??.empty)*)
7.62 +;
7.63 +if t2str @{theory} prog =
7.64 +"auto_generated t_t =\nRepeat\n ((Try (Repeat (Rewrite ''thm111'' False)) @@\n Try (Repeat (Rewrite ''refl'' False)))\n ??.empty)"
7.65 +then () else error "rules2scr_Rls auto_generated changed"