1.1 --- a/src/Tools/isac/Specify/cas-command.sml Mon Jun 20 17:22:26 2022 +0200
1.2 +++ b/src/Tools/isac/Specify/cas-command.sml Mon Jun 20 17:36:25 2022 +0200
1.3 @@ -44,7 +44,7 @@
1.4 val thy = ThyC.get_theory dI
1.5 val {ppc, ...} = Problem.from_store pI
1.6 val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
1.7 - val its = O_Model.add_id its_
1.8 + val its = O_Model.add_enumerate its_
1.9 val pits = map flattup2 its
1.10 val (pI, mI) =
1.11 if mI <> ["no_met"]
1.12 @@ -55,7 +55,7 @@
1.13 | NONE => (pI, (hd o #met o Problem.from_store) pI)
1.14 val {ppc, pre, prls, ...} = MethodC.from_store mI
1.15 val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
1.16 - val its = O_Model.add_id its_
1.17 + val its = O_Model.add_enumerate its_
1.18 val mits = map flattup2 its
1.19 val (_, pre) = Pre_Conds.check prls pre mits 0
1.20 val ctxt = Proof_Context.init_global thy
2.1 --- a/src/Tools/isac/Specify/m-match.sml Mon Jun 20 17:22:26 2022 +0200
2.2 +++ b/src/Tools/isac/Specify/m-match.sml Mon Jun 20 17:36:25 2022 +0200
2.3 @@ -199,7 +199,7 @@
2.4 val cy = filter O_Model.is_copy_named pbt (* cy is NOT a (formal) argument, but the fun's result *)
2.5 val oris' = matc thy pbt' ags []
2.6 val cy' = map (O_Model.cpy_nam pbt' oris') cy
2.7 - val ors = O_Model.add_id (oris' @ cy') (*...appended in order to get into the Model-items *)
2.8 + val ors = O_Model.add_enumerate (oris' @ cy') (*...appended in order to get into the Model-items *)
2.9 in (map flattup ors) end
2.10
2.11 (* report part of the error-msg which is not available in match_args *)
3.1 --- a/src/Tools/isac/Specify/o-model.sml Mon Jun 20 17:22:26 2022 +0200
3.2 +++ b/src/Tools/isac/Specify/o-model.sml Mon Jun 20 17:36:25 2022 +0200
3.3 @@ -38,14 +38,11 @@
3.4 (*/------- rename -------\*)
3.5 val associate_input: Proof.context -> m_field(*del?*) -> descriptor * values -> T -> message * single * values
3.6 val associate_input': Proof.context -> m_field -> values -> T -> message * single * values
3.7 -(*val contains: Proof.context -> m_field -> T -> term -> message * single * values*)
3.8 val contains: Proof.context -> m_field -> T -> term -> message * single * values
3.9 -(*val typeless: term -> term*)
3.10 val make_typeless: term -> term
3.11 val test_types: Proof.context -> descriptor * values -> string
3.12
3.13 -(*put add_id into a new auxiliary fun, see ONLY call..*)
3.14 - val add_id: 'a list -> (int * 'a) list
3.15 + val add_enumerate: 'a list -> (int * 'a) list
3.16 type preori
3.17 (*val cpy_nam: Model_Pattern.T -> preori list -> Model_Pattern.single -> preori*)
3.18 val cpy_nam: Model_Pattern.T -> preori list -> Model_Pattern.single -> preori
3.19 @@ -165,8 +162,8 @@
3.20 fun replace_0 vm [0] = intsto vm
3.21 | replace_0 _ vs = vs;
3.22
3.23 -fun add_id [] = raise ERROR "O_Model.add_id []"
3.24 - | add_id xs =
3.25 +fun add_enumerate [] = raise ERROR "O_Model.add_enumerate []"
3.26 + | add_enumerate xs =
3.27 let
3.28 fun add _ [] = []
3.29 | add n (x :: xs) = (n, x) :: add (n + 1) xs;
3.30 @@ -188,7 +185,7 @@
3.31 val model' = model
3.32 |> coll_variants
3.33 |> map (replace_0 maxv |> apfst)
3.34 - |> add_id
3.35 + |> add_enumerate
3.36 |> map flattup;
3.37 in model' end;
3.38
3.39 @@ -233,7 +230,7 @@
3.40 SOME m_field => (a, b, m_field, descr, e)
3.41 | NONE => (a, b, "#undef", descr, e))
3.42 |> map (fn (_, b, c, d, e) => (b, c, d, e)) (* for correct enumeration *)
3.43 - |> add_id (* for correct enumeration *)
3.44 + |> add_enumerate (* for correct enumeration *)
3.45 |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)), (* for correct enumeration *)
3.46 ctxt |> ContextC.add_constraints (add |> values |> TermC.vars'))
3.47 end
4.1 --- a/src/Tools/isac/Specify/p-spec.sml Mon Jun 20 17:22:26 2022 +0200
4.2 +++ b/src/Tools/isac/Specify/p-spec.sml Mon Jun 20 17:36:25 2022 +0200
4.3 @@ -178,7 +178,7 @@
4.4 let
4.5 val thy = ThyC.get_theory dI
4.6 val its_ = map (fstr2itm_ thy pbt) selcts (*([1],true,"#Given",Cor (...))*)
4.7 - val its = O_Model.add_id its_
4.8 + val its = O_Model.add_enumerate its_
4.9 in map flattup2 its end
4.10
4.11 (* WN.11.03 for input_icalhd, ~ specify_additem for Add_Given/_Find/_Relation
5.1 --- a/test/Tools/isac/Specify/o-model.sml Mon Jun 20 17:22:26 2022 +0200
5.2 +++ b/test/Tools/isac/Specify/o-model.sml Mon Jun 20 17:36:25 2022 +0200
5.3 @@ -9,7 +9,7 @@
5.4 "----------- initialise O_Model.T --------------------------------------------------------------";
5.5 "----------- fun mark --------------------------------------------------------------------------";
5.6 "----------- fun coll_variants -----------------------------------------------------------------";
5.7 -"----------- fun add_id ------------------------------------------------------------------------";
5.8 +"----------- fun add_enumerate ------------------------------------------------------------------------";
5.9 "----------- fun filter_vat --------------------------------------------------------------------";
5.10 "----------- regression test fun O_Model.is_copy_named -----------------------------------------";
5.11 "----------- .. CONTINUED regr.test fun O_Model.cpy_nam ----------------------------------------";
5.12 @@ -80,13 +80,13 @@
5.13 val oris = ori
5.14 |> coll_variants
5.15 |> map (replace_0 maxv |> apfst)
5.16 - |> add_id
5.17 + |> add_enumerate
5.18 |> map flattup;
5.19
5.20 (*+ decompose..*)
5.21 (*+*)val fff as [([0], ("#Given", _, _)), _, _, _, _, _, _] = ori |> coll_variants;
5.22 (*+*)val ggg as [([1], ("#Given", _, _)), _, _, _, _, _, _] = fff |> map (replace_0 maxv |> apfst);
5.23 -(*+*)val hhh as [(1, ([1], ("#Given", _, _))), (2, ([1], ("#Given", _, _))), _, _, _, _, _] = ggg |> add_id;
5.24 +(*+*)val hhh as [(1, ([1], ("#Given", _, _))), (2, ([1], ("#Given", _, _))), _, _, _, _, _] = ggg |> add_enumerate;
5.25 (*+*)val iii = hhh |> map flattup;
5.26 (*+*)val iii as [(1, [1], "#Given", _, _), (2, [1], "#Given", _, _), _, _, _, _, _] = hhh |> map flattup;
5.27
5.28 @@ -129,14 +129,14 @@
5.29 if coll_variants xs = [([1, 2, 3], 1), ([0], 2), ([1, 2], 4), ([0], 5)]
5.30 then () else error "fun coll_variants CHANGED";
5.31
5.32 -"----------- fun add_id ------------------------------------------------------------------------";
5.33 -"----------- fun add_id ------------------------------------------------------------------------";
5.34 -"----------- fun add_id ------------------------------------------------------------------------";
5.35 +"----------- fun add_enumerate ------------------------------------------------------------------------";
5.36 +"----------- fun add_enumerate ------------------------------------------------------------------------";
5.37 +"----------- fun add_enumerate ------------------------------------------------------------------------";
5.38 val xs = [([1,2,3],1),([0],2),([1,2],4),([0],5)];
5.39 -val xxx = add_id xs;
5.40 +val xxx = add_enumerate xs;
5.41
5.42 -if add_id xs = [(1, ([1, 2, 3], 1)), (2, ([0], 2)), (3, ([1, 2], 4)), (4, ([0], 5))]
5.43 -then () else error "fun add_id CHANGED";
5.44 +if add_enumerate xs = [(1, ([1, 2, 3], 1)), (2, ([0], 2)), (3, ([1, 2], 4)), (4, ([0], 5))]
5.45 +then () else error "fun add_enumerate CHANGED";
5.46
5.47
5.48 "----------- fun filter_vat --------------------------------------------------------------------";
6.1 --- a/test/Tools/isac/Specify/specify.sml Mon Jun 20 17:22:26 2022 +0200
6.2 +++ b/test/Tools/isac/Specify/specify.sml Mon Jun 20 17:36:25 2022 +0200
6.3 @@ -285,14 +285,14 @@
6.4 ((o_model @ add)
6.5 |> map (fn (a, b, _, descr, e) => (a, b, the (Model_Pattern.get_field descr m_patt), descr, e))
6.6 |> map (fn (_, b, c, d, e) => (b, c, d, e)) (* for correct enumeration *)
6.7 - |> add_id (* for correct enumeration *)
6.8 + |> add_enumerate (* for correct enumeration *)
6.9 |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)), (* for correct enumeration *)
6.10 ctxt |> ContextC.add_constraints (add |> values |> TermC.vars')) (*return from O_Model.complete_for*);
6.11 "~~~~~ fun complete_for \<longrightarrow>fun Specify_Step.complete_for , return:"; val (o_model', ctxt') =
6.12 ((o_model @ add)
6.13 |> map (fn (a, b, _, descr, e) => (a, b, the (Model_Pattern.get_field descr m_patt), descr, e))
6.14 |> map (fn (_, b, c, d, e) => (b, c, d, e)) (* for correct enumeration *)
6.15 - |> add_id (* for correct enumeration *)
6.16 + |> add_enumerate (* for correct enumeration *)
6.17 |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)), (* for correct enumeration *)
6.18 ctxt |> ContextC.add_constraints (add |> values |> TermC.vars'));
6.19
6.20 @@ -666,7 +666,7 @@
6.21 (*NEW*)|> map (fn (a, b, _, descr, e) => (a, b, the (Model_Pattern.get_field descr m_patt), descr, e))
6.22 (*NEW*)
6.23 |> map (fn (_, b, c, d, e) => (b, c, d, e))
6.24 - |> add_id
6.25 + |> add_enumerate
6.26 |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)),
6.27 ctxt |> ContextC.add_constraints (add |> O_Model.values |> TermC.vars')) (*return from O_Model.complete_for*);
6.28 "~~~~ from fun O_Model.complete_for \<longrightarrow>Step_Specify.by_tactic , return:"; val (o_model', ctxt') =
6.29 @@ -674,7 +674,7 @@
6.30 (*NEW*)|> map (fn (a, b, _, descr, e) => (a, b, the (Model_Pattern.get_field descr m_patt), descr, e))
6.31 (*NEW*)
6.32 |> map (fn (_, b, c, d, e) => (b, c, d, e))
6.33 - |> add_id
6.34 + |> add_enumerate
6.35 |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)),
6.36 ctxt |> ContextC.add_constraints (add |> O_Model.values |> TermC.vars'));
6.37
7.1 --- a/test/Tools/isac/Test_Some.thy Mon Jun 20 17:22:26 2022 +0200
7.2 +++ b/test/Tools/isac/Test_Some.thy Mon Jun 20 17:36:25 2022 +0200
7.3 @@ -247,14 +247,14 @@
7.4 ((o_model @ add)
7.5 |> map (fn (a, b, _, descr, e) => (a, b, the (Model_Pattern.get_field descr m_patt), descr, e))
7.6 |> map (fn (_, b, c, d, e) => (b, c, d, e)) (* for correct enumeration *)
7.7 - |> add_id (* for correct enumeration *)
7.8 + |> add_enumerate (* for correct enumeration *)
7.9 |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)), (* for correct enumeration *)
7.10 ctxt |> ContextC.add_constraints (add |> values |> TermC.vars')) (*return from O_Model.complete_for*);
7.11 "~~~~~ fun complete_for \<longrightarrow>fun Specify_Step.complete_for , return:"; val (o_model', ctxt') =
7.12 ((o_model @ add)
7.13 |> map (fn (a, b, _, descr, e) => (a, b, the (Model_Pattern.get_field descr m_patt), descr, e))
7.14 |> map (fn (_, b, c, d, e) => (b, c, d, e)) (* for correct enumeration *)
7.15 - |> add_id (* for correct enumeration *)
7.16 + |> add_enumerate (* for correct enumeration *)
7.17 |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)), (* for correct enumeration *)
7.18 ctxt |> ContextC.add_constraints (add |> values |> TermC.vars'));
7.19
7.20 @@ -641,7 +641,7 @@
7.21 (*NEW*)|> map (fn (a, b, _, descr, e) => (a, b, the (Model_Pattern.get_field descr m_patt), descr, e))
7.22 (*NEW*)
7.23 |> map (fn (_, b, c, d, e) => (b, c, d, e))
7.24 - |> add_id
7.25 + |> add_enumerate
7.26 |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)),
7.27 ctxt |> ContextC.add_constraints (add |> O_Model.values |> TermC.vars')) (*return from O_Model.complete_for*);
7.28 "~~~~ from fun O_Model.complete_for \<longrightarrow>Step_Specify.by_tactic , return:"; val (o_model', ctxt') =
7.29 @@ -649,7 +649,7 @@
7.30 (*NEW*)|> map (fn (a, b, _, descr, e) => (a, b, the (Model_Pattern.get_field descr m_patt), descr, e))
7.31 (*NEW*)
7.32 |> map (fn (_, b, c, d, e) => (b, c, d, e))
7.33 - |> add_id
7.34 + |> add_enumerate
7.35 |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)),
7.36 ctxt |> ContextC.add_constraints (add |> O_Model.values |> TermC.vars'));
7.37