1.1 --- a/test/Tools/isac/Specify/o-model.sml Mon Jul 19 15:34:54 2021 +0200
1.2 +++ b/test/Tools/isac/Specify/o-model.sml Mon Jul 19 17:29:35 2021 +0200
1.3 @@ -50,29 +50,29 @@
1.4 |> add_variants;
1.5
1.6 (*+ decompose..*)
1.7 -(*+*)val aaa as Const ("Biegelinie.Traegerlaenge", _) $ Free ("L", _) = (nth 1 fmz) |> TermC.parseNEW'' thy;
1.8 -(*+*)val bbb as (Const ("Biegelinie.Traegerlaenge", _), [Free ("L", _)]) = aaa |> Input_Descript.split;
1.9 -(*+*)val ccc as ("#Given", Const ("Biegelinie.Traegerlaenge", _), [Free ("L", _)]) = bbb |> add_field thy pbt;
1.10 +(*+*)val aaa as Const (\<^const_name>\<open>Traegerlaenge\<close>, _) $ Free ("L", _) = (nth 1 fmz) |> TermC.parseNEW'' thy;
1.11 +(*+*)val bbb as (Const (\<^const_name>\<open>Traegerlaenge\<close>, _), [Free ("L", _)]) = aaa |> Input_Descript.split;
1.12 +(*+*)val ccc as ("#Given", Const (\<^const_name>\<open>Traegerlaenge\<close>, _), [Free ("L", _)]) = bbb |> add_field thy pbt;
1.13 (*+ WHY IS THE LIST IN "#Relate" NOT DECOMPOSED?...*)
1.14 -(*+*)val ddd as [("#Given", Const ("Biegelinie.Traegerlaenge", _), [Free ("L", _)]),
1.15 - ("#Given", Const ("Biegelinie.Streckenlast", _), [Free ("q_0", _)]),
1.16 - ("#Find", Const ("Biegelinie.Biegelinie", _), [Free ("y", _)]),
1.17 - ("#Relate", Const ("Biegelinie.Randbedingungen", _),
1.18 - [Const ("List.list.Cons", _) $ (Const ("HOL.eq", _) $ (Free ("y", _) $ _(*"0"*)) $ _(*"0"*)) $
1.19 - Const ("List.list.Nil", _),
1.20 - Const ("List.list.Cons", _) $ (Const ("HOL.eq", _) $ (Free ("y", _) $ _(**)) $ _(*"0"*)) $
1.21 - Const ("List.list.Nil", _),
1.22 - Const ("List.list.Cons", _) $ (Const ("HOL.eq", _) $ (Const ("Biegelinie.M_b", _) $ _(*"0"*)) $ _(*"0"*)) $
1.23 - Const ("List.list.Nil", _),
1.24 - Const ("List.list.Cons", _) $ (Const ("HOL.eq", _) $ (Const ("Biegelinie.M_b", _) $ Free ("L", _)) $ _(*"0"*)) $
1.25 - Const ("List.list.Nil", _)]),
1.26 - ("#undef", Const ("Biegelinie.FunktionsVariable", _), [Free ("x", _)]),
1.27 +(*+*)val ddd as [("#Given", Const (\<^const_name>\<open>Traegerlaenge\<close>, _), [Free ("L", _)]),
1.28 + ("#Given", Const (\<^const_name>\<open>Streckenlast\<close>, _), [Free ("q_0", _)]),
1.29 + ("#Find", Const (\<^const_name>\<open>Biegelinie\<close>, _), [Free ("y", _)]),
1.30 + ("#Relate", Const (\<^const_name>\<open>Randbedingungen\<close>, _),
1.31 + [Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Free ("y", _) $ _(*"0"*)) $ _(*"0"*)) $
1.32 + Const (\<^const_name>\<open>Nil\<close>, _),
1.33 + Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Free ("y", _) $ _(**)) $ _(*"0"*)) $
1.34 + Const (\<^const_name>\<open>Nil\<close>, _),
1.35 + Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Const (\<^const_name>\<open>Biegelinie.M_b\<close>, _) $ _(*"0"*)) $ _(*"0"*)) $
1.36 + Const (\<^const_name>\<open>Nil\<close>, _),
1.37 + Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Const (\<^const_name>\<open>Biegelinie.M_b\<close>, _) $ Free ("L", _)) $ _(*"0"*)) $
1.38 + Const (\<^const_name>\<open>Nil\<close>, _)]),
1.39 + ("#undef", Const (\<^const_name>\<open>FunktionsVariable\<close>, _), [Free ("x", _)]),
1.40 _, _] =
1.41 (map (fn str => str
1.42 |> TermC.parseNEW'' thy
1.43 |> Input_Descript.split
1.44 |> add_field thy pbt) fmz);
1.45 -(*+*)val eee as [(0, ("#Given", Const ("Biegelinie.Traegerlaenge", _), [Free ("L", _)])),
1.46 +(*+*)val eee as [(0, ("#Given", Const (\<^const_name>\<open>Traegerlaenge\<close>, _), [Free ("L", _)])),
1.47 _, _, _, _, _, _] = add_variants ddd;
1.48
1.49 val maxv = map fst ori |> max;
1.50 @@ -160,17 +160,17 @@
1.51
1.52 case o_model of
1.53 [
1.54 - (1, [1, 2, 3], "#Given", Const ("Input_Descript.fixedValues", _), [Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("r", _) $ Const ("Program.Arbfix", _)) $ _]),
1.55 - (2, [1, 2, 3], "#Find", Const ("Input_Descript.maximum", _), [Free ("A", _)]),
1.56 - (3, [1, 2, 3], "#Find", Const ("Input_Descript.valuesFor", _), [_ $ Free ("a", _) $ _, Const ("List.list.Cons", _) $ Free ("b", _) $ _]),
1.57 - (4, [1, 2], "#Relate", Const ("Input_Descript.relations", _), _),
1.58 - (5, [3], "#Relate", Const ("Input_Descript.relations", _), _),
1.59 - (6, [1], "#undef", Const ("Input_Descript.boundVariable", _), [Free ("a", _)]),
1.60 - (7, [2], "#undef", Const ("Input_Descript.boundVariable", _), [Free ("b", _)]),
1.61 - (8, [3], "#undef", Const ("Input_Descript.boundVariable", _), [Free ("alpha", _)]),
1.62 - (9, [1, 2], "#undef", Const ("Input_Descript.interval", _), [Const (\<^const_name>\<open>Collect\<close>, _) $ Abs ("x", _, Const (\<^const_name>\<open>conj\<close>, _) $ _ $ _)]),
1.63 - (10, [3], "#undef", Const ("Input_Descript.interval", _), _),
1.64 - (11, [1, 2, 3], "#undef", Const ("Input_Descript.errorBound", _), [Const ("HOL.eq", _) $ Free ("eps", _) $ _(*"0"*)])
1.65 + (1, [1, 2, 3], "#Given", Const (\<^const_name>\<open>Input_Descript.fixedValues\<close>, _), [Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("r", _) $ Const (\<^const_name>\<open>Program.Arbfix\<close>, _)) $ _]),
1.66 + (2, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.maximum\<close>, _), [Free ("A", _)]),
1.67 + (3, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.valuesFor\<close>, _), [_ $ Free ("a", _) $ _, Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("b", _) $ _]),
1.68 + (4, [1, 2], "#Relate", Const (\<^const_name>\<open>Input_Descript.relations\<close>, _), _),
1.69 + (5, [3], "#Relate", Const (\<^const_name>\<open>Input_Descript.relations\<close>, _), _),
1.70 + (6, [1], "#undef", Const (\<^const_name>\<open>Input_Descript.boundVariable\<close>, _), [Free ("a", _)]),
1.71 + (7, [2], "#undef", Const (\<^const_name>\<open>Input_Descript.boundVariable\<close>, _), [Free ("b", _)]),
1.72 + (8, [3], "#undef", Const (\<^const_name>\<open>Input_Descript.boundVariable\<close>, _), [Free ("alpha", _)]),
1.73 + (9, [1, 2], "#undef", Const (\<^const_name>\<open>Input_Descript.interval\<close>, _), [Const (\<^const_name>\<open>Collect\<close>, _) $ Abs ("x", _, Const (\<^const_name>\<open>conj\<close>, _) $ _ $ _)]),
1.74 + (10, [3], "#undef", Const (\<^const_name>\<open>Input_Descript.interval\<close>, _), _),
1.75 + (11, [1, 2, 3], "#undef", Const (\<^const_name>\<open>Input_Descript.errorBound\<close>, _), [Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("eps", _) $ _(*"0"*)])
1.76 ] => ()
1.77 | _ => error "fun O_Model.init CHANGED";
1.78
1.79 @@ -184,29 +184,29 @@
1.80
1.81 case filtered of
1.82 [[
1.83 - (1, [1, 2, 3], "#Given", Const ("Input_Descript.fixedValues", _), [Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("r", _) $ Const ("Program.Arbfix", _)) $ _]),
1.84 - (2, [1, 2, 3], "#Find", Const ("Input_Descript.maximum", _), [Free ("A", _)]),
1.85 - (3, [1, 2, 3], "#Find", Const ("Input_Descript.valuesFor", _), [_ $ Free ("a", _) $ _, Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("b", _) $ _]),
1.86 - (4, [1, 2], "#Relate", Const ("Input_Descript.relations", _), _),
1.87 - (6, [1], "#undef", Const ("Input_Descript.boundVariable", _), [Free ("a", _)]),
1.88 - (9, [1, 2], "#undef", Const ("Input_Descript.interval", _), [Const ("Set.Collect", _) $ Abs ("x", _, Const ("HOL.conj", _) $ _ $ _)]),
1.89 - (11, [1, 2, 3], "#undef", Const ("Input_Descript.errorBound", _), [Const ("HOL.eq", _) $ Free ("eps", _) $ _(*"0"*)])
1.90 + (1, [1, 2, 3], "#Given", Const (\<^const_name>\<open>Input_Descript.fixedValues\<close>, _), [Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("r", _) $ Const (\<^const_name>\<open>Program.Arbfix\<close>, _)) $ _]),
1.91 + (2, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.maximum\<close>, _), [Free ("A", _)]),
1.92 + (3, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.valuesFor\<close>, _), [_ $ Free ("a", _) $ _, Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("b", _) $ _]),
1.93 + (4, [1, 2], "#Relate", Const (\<^const_name>\<open>Input_Descript.relations\<close>, _), _),
1.94 + (6, [1], "#undef", Const (\<^const_name>\<open>Input_Descript.boundVariable\<close>, _), [Free ("a", _)]),
1.95 + (9, [1, 2], "#undef", Const (\<^const_name>\<open>Input_Descript.interval\<close>, _), [Const (\<^const_name>\<open>Collect\<close>, _) $ Abs ("x", _, Const (\<^const_name>\<open>conj\<close>, _) $ _ $ _)]),
1.96 + (11, [1, 2, 3], "#undef", Const (\<^const_name>\<open>Input_Descript.errorBound\<close>, _), [Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("eps", _) $ _(*"0"*)])
1.97 ], [
1.98 - (1, [1, 2, 3], "#Given", Const ("Input_Descript.fixedValues", _), [Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("r", _) $ Const ("Program.Arbfix", _)) $ _]),
1.99 - (2, [1, 2, 3], "#Find", Const ("Input_Descript.maximum", _), [Free ("A", _)]),
1.100 - (3, [1, 2, 3], "#Find", Const ("Input_Descript.valuesFor", _), [_ $ Free ("a", _) $ _, Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("b", _) $ _]),
1.101 - (4, [1, 2], "#Relate", Const ("Input_Descript.relations", _), _),
1.102 - (7, [2], "#undef", Const ("Input_Descript.boundVariable", _), [Free ("b", _)]),
1.103 - (9, [1, 2], "#undef", Const ("Input_Descript.interval", _), [Const ("Set.Collect", _) $ Abs ("x", _, Const ("HOL.conj", _) $ _ $ _)]),
1.104 - (11, [1, 2, 3], "#undef", Const ("Input_Descript.errorBound", _), [Const ("HOL.eq", _) $ Free ("eps", _) $ _(*"0"*)])
1.105 + (1, [1, 2, 3], "#Given", Const (\<^const_name>\<open>Input_Descript.fixedValues\<close>, _), [Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("r", _) $ Const (\<^const_name>\<open>Program.Arbfix\<close>, _)) $ _]),
1.106 + (2, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.maximum\<close>, _), [Free ("A", _)]),
1.107 + (3, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.valuesFor\<close>, _), [_ $ Free ("a", _) $ _, Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("b", _) $ _]),
1.108 + (4, [1, 2], "#Relate", Const (\<^const_name>\<open>Input_Descript.relations\<close>, _), _),
1.109 + (7, [2], "#undef", Const (\<^const_name>\<open>Input_Descript.boundVariable\<close>, _), [Free ("b", _)]),
1.110 + (9, [1, 2], "#undef", Const (\<^const_name>\<open>Input_Descript.interval\<close>, _), [Const (\<^const_name>\<open>Collect\<close>, _) $ Abs ("x", _, Const (\<^const_name>\<open>conj\<close>, _) $ _ $ _)]),
1.111 + (11, [1, 2, 3], "#undef", Const (\<^const_name>\<open>Input_Descript.errorBound\<close>, _), [Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("eps", _) $ _(*"0"*)])
1.112 ], [
1.113 - (1, [1, 2, 3], "#Given", Const ("Input_Descript.fixedValues", _), [Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("r", _) $ Const ("Program.Arbfix", _)) $ _]),
1.114 - (2, [1, 2, 3], "#Find", Const ("Input_Descript.maximum", _), [Free ("A", _)]),
1.115 - (3, [1, 2, 3], "#Find", Const ("Input_Descript.valuesFor", _), [_ $ Free ("a", _) $ _, Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("b", _) $ _]),
1.116 - (5, [3], "#Relate", Const ("Input_Descript.relations", _), _),
1.117 - (8, [3], "#undef", Const ("Input_Descript.boundVariable", _), [Free ("alpha", _)]),
1.118 - (10, [3], "#undef", Const ("Input_Descript.interval", _), _),
1.119 - (11, [1, 2, 3], "#undef", Const ("Input_Descript.errorBound", _), [Const ("HOL.eq", _) $ Free ("eps", _) $ _(*"0"*)])
1.120 + (1, [1, 2, 3], "#Given", Const (\<^const_name>\<open>Input_Descript.fixedValues\<close>, _), [Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("r", _) $ Const (\<^const_name>\<open>Program.Arbfix\<close>, _)) $ _]),
1.121 + (2, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.maximum\<close>, _), [Free ("A", _)]),
1.122 + (3, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.valuesFor\<close>, _), [_ $ Free ("a", _) $ _, Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("b", _) $ _]),
1.123 + (5, [3], "#Relate", Const (\<^const_name>\<open>Input_Descript.relations\<close>, _), _),
1.124 + (8, [3], "#undef", Const (\<^const_name>\<open>Input_Descript.boundVariable\<close>, _), [Free ("alpha", _)]),
1.125 + (10, [3], "#undef", Const (\<^const_name>\<open>Input_Descript.interval\<close>, _), _),
1.126 + (11, [1, 2, 3], "#undef", Const (\<^const_name>\<open>Input_Descript.errorBound\<close>, _), [Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("eps", _) $ _(*"0"*)])
1.127 ]] => ()
1.128 | _ => error "fun O_Model.filter_vat CHANGED";
1.129
1.130 @@ -242,7 +242,7 @@
1.131 (*...all must be true*)
1.132
1.133 case O_Model.cpy_nam pbt oris (hd cy) of
1.134 - ([1], "#Find", Const ("Input_Descript.solutions", _), [Free ("x_i", _)]) => ()
1.135 + ([1], "#Find", Const (\<^const_name>\<open>Input_Descript.solutions\<close>, _), [Free ("x_i", _)]) => ()
1.136 | _ => error "calchead.sml regr.test O_Model.cpy_nam-1-";
1.137
1.138 (*new data: O_Model.cpy_nam without changing the name*)
1.139 @@ -259,6 +259,6 @@
1.140 (*could be more than 1*)];
1.141
1.142 case O_Model.cpy_nam pbt oris (hd cy) of
1.143 - ([1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)]) => ()
1.144 + ([1], "#Find", Const (\<^const_name>\<open>EqSystem.solution\<close>, _), [Free ("ss'''", _)]) => ()
1.145 | _ => error "calchead.sml regr.test O_Model.cpy_nam-2-";
1.146