1.1 --- a/src/Tools/isac/CalcElements/contextC.sml Tue Aug 27 15:32:38 2019 +0200
1.2 +++ b/src/Tools/isac/CalcElements/contextC.sml Tue Aug 27 18:03:33 2019 +0200
1.3 @@ -6,6 +6,7 @@
1.4 signature CONTEXT_C =
1.5 sig
1.6 val e_ctxt : Proof.context
1.7 + val isac_ctxt : 'a -> Proof.context
1.8 val initialise : string -> term list -> Proof.context
1.9 val initialise' : theory -> string list -> Proof.context
1.10 val get_assumptions : Proof.context -> term list
1.11 @@ -179,6 +180,7 @@
1.12 struct
1.13
1.14 val e_ctxt = Proof_Context.init_global @{theory "Pure"};
1.15 +fun isac_ctxt xxx = Proof_Context.init_global (Rule.Isac xxx)
1.16
1.17 (* in root-problem take respective formalisation *)
1.18 fun initialise' thy fmz =
2.1 --- a/src/Tools/isac/Interpret/Interpret.thy Tue Aug 27 15:32:38 2019 +0200
2.2 +++ b/src/Tools/isac/Interpret/Interpret.thy Tue Aug 27 18:03:33 2019 +0200
2.3 @@ -16,5 +16,6 @@
2.4 (* declare [[ML_print_depth = 999]] *)
2.5 ML \<open>
2.6 \<close> ML \<open>
2.7 +\<close> ML \<open>
2.8 \<close>
2.9 end
3.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Tue Aug 27 15:32:38 2019 +0200
3.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Tue Aug 27 18:03:33 2019 +0200
3.3 @@ -626,11 +626,11 @@
3.4 val itms =
3.5 if mI = ["Biegelinien", "ausBelastung"]
3.6 then itms @
3.7 - [(4, [1], true, "#Given", Model.Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])),
3.8 + [(4, [1], true, "#Given", Model.Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),
3.9 [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
3.10 (Free ("id_fun", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
3.11 [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] ))),
3.12 - (5, [1], true, "#Given", Model.Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])),
3.13 + (5, [1], true, "#Given", Model.Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),
3.14 [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
3.15 (Free ("id_abl", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
3.16 [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))]
4.1 --- a/src/Tools/isac/Interpret/script.sml Tue Aug 27 15:32:38 2019 +0200
4.2 +++ b/src/Tools/isac/Interpret/script.sml Tue Aug 27 18:03:33 2019 +0200
4.3 @@ -166,9 +166,9 @@
4.4 (*WN.5.5.03: ?: does this allow for different descriptions ???
4.5 ?: why not taken from formal args of script ???
4.6 !: FIXXXME penv: push it here in itms2args into script-evaluation*)
4.7 -(* val (thy, mI, itms) = (thy, metID, itms);
4.8 - *)
4.9 val errmsg = "ERROR: the guard is missing (#ppc in 'type met' added in prep_met)."
4.10 +fun errmsg2 d itms = ("itms2args: '" ^ Rule.term2str d ^ "' not in itms:\n" ^
4.11 +"itms:\n" ^ Model.itms2str_ @{context} itms)
4.12 fun itms2args _ mI itms =
4.13 let
4.14 val mvat = Model.max_vt itms
4.15 @@ -177,7 +177,7 @@
4.16 fun test_dsc d (_, _, _, _, itm_) = (d = Model.d_in itm_)
4.17 fun itm2arg itms (_,(d,_)) =
4.18 case find_first (test_dsc d) itms of
4.19 - NONE => error ("itms2args: '" ^ Rule.term2str d ^ "' not in itms")
4.20 + NONE => raise ERROR (errmsg2 d itms)
4.21 | SOME (_, _, _, _, itm_) => Model.penvval_in itm_
4.22 (*| SOME (_,_,_,_,itm_) => mk_arg thy (Model.d_in itm_) (ts_in itm_);
4.23 penv postponed; presently penv holds already LTool.env for script*)
4.24 @@ -576,11 +576,11 @@
4.25 val itms =
4.26 if metID = ["IntegrierenUndKonstanteBestimmen2"]
4.27 then itms @
4.28 - [(4, [1], true, "#Given", Model.Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])),
4.29 + [(4, [1], true, "#Given", Model.Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),
4.30 [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
4.31 (Free ("id_fun", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
4.32 [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] ))),
4.33 - (5, [1], true, "#Given", Model.Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])),
4.34 + (5, [1], true, "#Given", Model.Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),
4.35 [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
4.36 (Free ("id_abl", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
4.37 [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))]
5.1 --- a/src/Tools/isac/Specify/calchead.sml Tue Aug 27 15:32:38 2019 +0200
5.2 +++ b/src/Tools/isac/Specify/calchead.sml Tue Aug 27 18:03:33 2019 +0200
5.3 @@ -867,11 +867,11 @@
5.4 val itms =
5.5 if mI' = ["Biegelinien", "ausBelastung"]
5.6 then itms @
5.7 - [(4, [1], true, "#Given", Model.Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])),
5.8 + [(4, [1], true, "#Given", Model.Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),
5.9 [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
5.10 (Free ("id_fun", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
5.11 [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] ))),
5.12 - (5, [1], true, "#Given", Model.Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])),
5.13 + (5, [1], true, "#Given", Model.Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),
5.14 [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
5.15 (Free ("id_abl", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
5.16 [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))]
5.17 @@ -1140,11 +1140,11 @@
5.18 val itms =
5.19 if mID = ["Biegelinien", "ausBelastung"]
5.20 then itms @
5.21 - [(4, [1], true, "#Given", Model.Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])),
5.22 + [(4, [1], true, "#Given", Model.Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),
5.23 [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
5.24 (Free ("id_fun", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
5.25 [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] ))),
5.26 - (5, [1], true, "#Given", Model.Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])),
5.27 + (5, [1], true, "#Given", Model.Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),
5.28 [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
5.29 (Free ("id_abl", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
5.30 [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))]
6.1 --- a/src/Tools/isac/Specify/model.sml Tue Aug 27 15:32:38 2019 +0200
6.2 +++ b/src/Tools/isac/Specify/model.sml Tue Aug 27 18:03:33 2019 +0200
6.3 @@ -350,12 +350,12 @@
6.4 else
6.5 (case v of (*eg. eps=#0*) (Const ("HOL.eq", _) $ l $ r) => [r, l]
6.6 | _ => error ("pbl_ids Tools.nam: no equality " ^ Rule.term_to_string' ctxt v))
6.7 - | pbl_ids _ (Const (_, Type ("fun", [_,Type ("Tools.una", _)]))) v = [v]
6.8 - | pbl_ids _ (Const (_, Type ("fun", [_,Type ("Tools.unl", _)]))) v = [v]
6.9 - | pbl_ids _ (Const (_, Type ("fun", [_,Type ("Tools.str", _)]))) v = [v]
6.10 - | pbl_ids _ (Const (_, Type ("fun", [_,Type ("Tools.toreal", _)]))) v = [v]
6.11 - | pbl_ids _ (Const (_, Type ("fun", [_,Type ("Tools.toreall", _)])))v = [v]
6.12 - | pbl_ids _ (Const (_, Type ("fun", [_,Type ("Tools.unknown" ,_)])))v = [v]
6.13 + | pbl_ids _ (Const (_, Type ("fun", [_,Type ("Input_Descript.una", _)]))) v = [v]
6.14 + | pbl_ids _ (Const (_, Type ("fun", [_,Type ("Input_Descript.unl", _)]))) v = [v]
6.15 + | pbl_ids _ (Const (_, Type ("fun", [_,Type ("Input_Descript.str", _)]))) v = [v]
6.16 + | pbl_ids _ (Const (_, Type ("fun", [_,Type ("Input_Descript.toreal", _)]))) v = [v]
6.17 + | pbl_ids _ (Const (_, Type ("fun", [_,Type ("Input_Descript.toreall", _)])))v = [v]
6.18 + | pbl_ids _ (Const (_, Type ("fun", [_,Type ("Input_Descript.unknown" ,_)])))v = [v]
6.19 | pbl_ids _ _ v = error ("pbl_ids: not implemented for " ^ Rule.term2str v);
6.20
6.21 (* given an already input itm, ((14.9.01: no difference to pbl_ids jet!!))
6.22 @@ -369,12 +369,12 @@
6.23 (Const ("HOL.eq",_) $ l $ r) => [r,l]
6.24 | _ => error ("pbl_ids' Tools.nam: no equality " ^ term2str t))
6.25 | _ => vs (*14.9.01: ???TODO *))
6.26 - | pbl_ids' (Const (_, Type ("fun", [_, Type("Tools.una", _)]))) vs = vs
6.27 - | pbl_ids' (Const (_, Type ("fun", [_, Type("Tools.unl", _)]))) vs = vs
6.28 - | pbl_ids' (Const (_, Type ("fun", [_, Type("Tools.str", _)]))) vs = vs
6.29 - | pbl_ids' (Const (_, Type ("fun", [_, Type("Tools.toreal", _)]))) vs = vs
6.30 - | pbl_ids' (Const (_, Type ("fun", [_, Type("Tools.toreall", _)])))vs = vs
6.31 - | pbl_ids' (Const (_, Type ("fun", [_, Type("Tools.unknown", _)])))vs = vs
6.32 + | pbl_ids' (Const (_, Type ("fun", [_, Type("Input_Descript.una", _)]))) vs = vs
6.33 + | pbl_ids' (Const (_, Type ("fun", [_, Type("Input_Descript.unl", _)]))) vs = vs
6.34 + | pbl_ids' (Const (_, Type ("fun", [_, Type("Input_Descript.str", _)]))) vs = vs
6.35 + | pbl_ids' (Const (_, Type ("fun", [_, Type("Input_Descript.toreal", _)]))) vs = vs
6.36 + | pbl_ids' (Const (_, Type ("fun", [_, Type("Input_Descript.toreall", _)])))vs = vs
6.37 + | pbl_ids' (Const (_, Type ("fun", [_, Type("Input_Descript.unknown", _)])))vs = vs
6.38 | pbl_ids' _ vs = error ("pbl_ids': not implemented for " ^ terms2str vs);*)
6.39
6.40 (* 9.5.03 penv postponed: pbl_ids' *)
7.1 --- a/test/Tools/isac/Knowledge/biegelinie-3.sml Tue Aug 27 15:32:38 2019 +0200
7.2 +++ b/test/Tools/isac/Knowledge/biegelinie-3.sml Tue Aug 27 18:03:33 2019 +0200
7.3 @@ -254,11 +254,11 @@
7.4 val itms =
7.5 if mI' = ["Biegelinien", "ausBelastung"]
7.6 then itms @
7.7 - [(4, [1], true, "#Given", Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])),
7.8 + [(4, [1], true, "#Given", Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),
7.9 [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
7.10 (Free ("id_fun", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
7.11 [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] ))),
7.12 - (5, [1], true, "#Given", Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])),
7.13 + (5, [1], true, "#Given", Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),
7.14 [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
7.15 (Free ("id_abl", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
7.16 [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))]
7.17 @@ -275,11 +275,11 @@
7.18 (@{term "id_abl::real \<Rightarrow> real"},
7.19 [@{term "dy::real \<Rightarrow> real"}] )))]
7.20 val itms'' = itms @
7.21 - [(4, [1], true, "#Given", Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])),
7.22 + [(4, [1], true, "#Given", Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),
7.23 [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
7.24 (Free ("id_fun", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
7.25 [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] ))),
7.26 - (5, [1], true, "#Given", Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])),
7.27 + (5, [1], true, "#Given", Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),
7.28 [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
7.29 (Free ("id_abl", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
7.30 [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))]