1.1 --- a/TODO.md Fri Feb 24 16:14:28 2023 +0100
1.2 +++ b/TODO.md Mon Feb 27 09:45:29 2023 +0100
1.3 @@ -44,6 +44,8 @@
1.4
1.5 ***** priority of WN items is top down, most urgent/simple on top
1.6
1.7 +* WN: replace take in LibraryC with take from Library
1.8 +* WN: Syntax.read_term @{context} --> Syntax.read_term\<^context> , see I_Model "UnIqE_tErM"
1.9 * WN: renaming in References
1.10 * WN: correct design flaw in fun eval_*, see aa8760e4d987
1.11 * WN: unify get_ctxt in Solve_Step, Ctree (*DEPRECATED*)
2.1 --- a/src/Tools/isac/BaseDefinitions/model-pattern.sml Fri Feb 24 16:14:28 2023 +0100
2.2 +++ b/src/Tools/isac/BaseDefinitions/model-pattern.sml Mon Feb 27 09:45:29 2023 +0100
2.3 @@ -14,26 +14,39 @@
2.4 val to_string: Proof.context -> single list -> string
2.5
2.6 type model_input_pos
2.7 + type empty_input
2.8 + val empty_input: empty_input list
2.9 type pre_model
2.10 + type pre_model_TEST
2.11 type pre_model_single
2.12
2.13 type m_field = string
2.14 type descriptor = term
2.15 val parse_pos: Proof.context -> (m_field * (string * Position.T) list) list ->
2.16 pre_model * (term * Position.T) list
2.17 + val parse_pos_TEST: Proof.context -> (m_field * (string * Position.T) list) list ->
2.18 + pre_model_TEST * (term * Position.T) list
2.19
2.20 val variables: T -> term list
2.21 val get_field: descriptor -> T -> m_field option
2.22 datatype for = Problem | Method | Undef
2.23
2.24 val adapt_to_type: Proof.context -> single -> single
2.25 +(*from isac_test for Minisubpbl*)
2.26 + val split_descriptor: Proof.context -> m_field * term * Position.T ->
2.27 + (m_field * (descriptor * term) * Position.T)
2.28 + val split_descriptor': string -> (*TermC.as_*)string * empty_input
2.29 + datatype pre_model_single_TEST =
2.30 + Empty of (m_field * (descriptor * empty_input) * Position.T)
2.31 + | Proper of (m_field * (descriptor * term) * Position.T)
2.32 + val parse_pattern: Proof.context -> 'a * (string * Position.T) -> 'a * term * Position.T
2.33 + val empty_for: typ -> string
2.34 + val parse_term: Proof.context -> m_field * ((*TermC.as_*)string * Position.T) ->
2.35 + m_field * term * Position.T
2.36 + val parse_term_TEST: Proof.context -> m_field * (string * Position.T) -> pre_model_single_TEST
2.37
2.38 \<^isac_test>\<open>
2.39 - val split_descriptor: Proof.context -> m_field * term * Position.T -> pre_model_single
2.40 - val parse_term: Proof.context -> m_field * ((*TermC.as_*)string * Position.T) ->
2.41 - m_field * term * Position.T
2.42 - val parse_pattern: Proof.context -> m_field * ((*TermC.as_*)string * Position.T) ->
2.43 - m_field * term * Position.T
2.44 + (**)
2.45 \<close>
2.46 end
2.47
2.48 @@ -52,12 +65,26 @@
2.49 (* does NOT contain pre-conditions, because these have no \<open>descriptor\<close> *)
2.50 type T = single list;
2.51
2.52 -type model_input_pos = (* for internal use *)
2.53 - (m_field * (* "#Given", "#Find", "#Where", "#Relate" *)
2.54 +type model_input_pos = (* for internal use *)
2.55 + (m_field * (* "#Given", "#Find", "#Where", "#Relate" *)
2.56 ((*TermC.as_*)string * Position.T) list) (* list of items belonging to m_field *)
2.57 - list; (* list of "#Given" .. "#Relate" *)
2.58 + list; (* list of "#Given" .. "#Relate" *)
2.59 +type empty_input = string
2.60 +val empty_bool_list_input = "[__=__, __=__]"
2.61 +val empty_reallist_input = "[__, __]"
2.62 +val empty_bool_input = "(__=__)"
2.63 +val empty_item_input = "__"
2.64 +val empty_input = [empty_bool_list_input, empty_reallist_input, empty_bool_input, empty_item_input]
2.65 +fun empty_for (Type ("fun", [Type ("List.list", [Type ("HOL.bool", [])]), _])) = empty_bool_list_input
2.66 + | empty_for (Type ("fun", [Type ("List.list", [Type ("Real.real", [])]), _])) = empty_reallist_input
2.67 + | empty_for (Type ("HOL.bool", [])) = empty_bool_input
2.68 + | empty_for _ = empty_item_input
2.69 type pre_model_single = (m_field * (descriptor * term) * Position.T)
2.70 -type pre_model = (m_field * (term * term) * Position.T) list
2.71 +datatype pre_model_single_TEST =
2.72 + Empty of (m_field * (descriptor * empty_input) * Position.T)
2.73 + | Proper of (m_field * (descriptor * term) * Position.T)
2.74 +type pre_model = pre_model_single list
2.75 +type pre_model_TEST = pre_model_single_TEST list
2.76
2.77 (*val split_descriptor: Proof.context -> m_field * term * Position.T ->
2.78 m_field * (descriptor * term)(* * Position.T*)*)
2.79 @@ -68,10 +95,30 @@
2.80 | _ => error ("Wrong descriptor " ^ quote (UnparseC.term ctxt dsc_tm) ^ Position.here pos)
2.81 in (m_field, (hd, arg), pos) end
2.82
2.83 +fun is_empty_input arg = member (op =) empty_input arg
2.84 +fun split_descriptor' str =
2.85 + let
2.86 + val chars = Symbol.explode str
2.87 + val end_descr = find_index (fn str => (if str = " " then true else false)) chars
2.88 + (*^^^ TODO find parser for identifier*)
2.89 + in
2.90 + (implode (take (end_descr, chars)), implode (drop (end_descr + 1, chars)))
2.91 + (* 1 blank inbetween descriptor and argument, I_Model.feedback_to_string_TEST *)
2.92 + end
2.93
2.94 (*val parse_term: Proof.context -> m_field * ((*TermC.as_*)string * Position.T) -> m_field * term*)
2.95 fun parse_term ctxt (m_field, (str, pos)) =
2.96 (m_field, ParseC.term_position ctxt (str, pos), pos)
2.97 +fun parse_term_TEST ctxt (m_field, (str, pos)) =
2.98 + let
2.99 + val (descr, arg) = split_descriptor' str
2.100 + in
2.101 + if is_empty_input arg
2.102 + then Empty (m_field, (ParseC.term_position ctxt (descr, pos), arg), pos)
2.103 + else Proper (m_field, (ParseC.term_position ctxt (descr, pos),
2.104 + ParseC.term_position ctxt (arg, pos)), pos)
2.105 + end
2.106 +
2.107 fun parse_pattern ctxt (m_field, (str, pos)) =
2.108 (m_field, ParseC.pattern_position ctxt (str, pos), pos)
2.109
2.110 @@ -87,6 +134,17 @@
2.111 |> map (parse_pattern ctxt)
2.112 |> map (fn (_, a, b) => (a, b))
2.113 in (model, where_) end
2.114 +fun parse_pos_TEST ctxt model_input =
2.115 + let
2.116 + val items = model_input |> map (fn (m_field, items) => map (pair m_field) items) |> flat;
2.117 + val model = items
2.118 + |> filter_out ((fn f => (fn (f', _) => f = f')) "#Where")
2.119 + |> map (parse_term_TEST ctxt)
2.120 + val where_ = items
2.121 + |> filter ((fn f => (fn (f', _) => f = f')) "#Where")
2.122 + |> map (parse_pattern ctxt)
2.123 + |> map (fn (_, a, b) => (a, b))
2.124 + in (model, where_) end
2.125
2.126 fun pat2str ctxt (field, (dsc, id)) =
2.127 pair2str (field, pair2str (UnparseC.term ctxt dsc, UnparseC.term ctxt id));
3.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy Fri Feb 24 16:14:28 2023 +0100
3.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy Mon Feb 27 09:45:29 2023 +0100
3.3 @@ -56,7 +56,7 @@
3.4 Ctree.EmptyPtree;
3.5 (*---vvvvvvvvvvvvvv------- this comes from input \<Otimes> \<Odot> to Example *)
3.6 val (switch_pbl_met, user_model_spec) = (Model_Pattern.Problem, User_Model.Model_Refs)
3.7 - in set_data store thy end)));
3.8 + in set_data store thy end) ) );
3.9 \<close> ML \<open>
3.10 (*/-------------------------------------------------------------------------------------------\*)
3.11 Parse.name -- Parse.!!! ( \<^keyword>\<open>Specification\<close> -- \<^keyword>\<open>:\<close> --
3.12 @@ -65,12 +65,23 @@
3.13 (*\-------------------------------------------------------------------------------------------/*)
3.14 (*/-------------------------------------------------------------------------------------------\*)
3.15 : Token.T list ->
3.16 - (string * (Model_Pattern.model_input_pos *
3.17 - ((string * Position.T) * ((string * Position.T) * (string * Position.T))))) * Token.T list
3.18 -(*\-------------------------------------------------------------------------------------------/*)
3.19 -(*/-------------------------------------------------------------------------------------------\* )
3.20 - the type above is the type of the argument of \<open>(fn (_(*name*),..\<close>
3.21 -( *\------------------------------------------------------------------------------------------/*)
3.22 + (string * (Model_Pattern.model_input_pos *
3.23 + ((string * Position.T) * ((string * Position.T) * (string * Position.T))))) * Token.T list;
3.24 +(* ---------- the type above is the type of the argument of \<open>(fn (example_id, ...\<close> ------------*)
3.25 +(*\-------------------------------------------------------------------------------------------/*)
3.26 +
3.27 +(*/---------------------------------------- mimic input from PIDE ----------------------------\*)
3.28 +val example_id = "Diff_App-No.123a"
3.29 +val model_input = [("#Given", [("Constants [r = 7]", Position.none)])]
3.30 +val (thy_id, probl_id, meth_id) =
3.31 + ("Diff_App", "univariate_calculus/Optimisation", "Optimisation/by_univariate_calculus");
3.32 +(* ---------- ^^^ values for arguments of the fn below in order to determine signature -------*)
3.33 + (fn thy =>
3.34 + let
3.35 + val store = Ctree.EmptyPtree;
3.36 + in set_data store thy end)
3.37 +: theory -> theory
3.38 +(*\---------------------------------------- mimic input from PIDE ----------------------------/*)
3.39 \<close> ML \<open>
3.40 \<close>
3.41
4.1 --- a/src/Tools/isac/MathEngBasic/problem.sml Fri Feb 24 16:14:28 2023 +0100
4.2 +++ b/src/Tools/isac/MathEngBasic/problem.sml Mon Feb 27 09:45:29 2023 +0100
4.3 @@ -103,7 +103,7 @@
4.4 parse_pos_tagged_terms \<^keyword>\<open>Relate\<close> "#Relate";
4.5
4.6 val parse_authors = parse_item_names \<^keyword>\<open>Author\<close>;
4.7 -(*val parse_pos_cas: Token.T list -> (string * Position.T) option * Token.T list*)
4.8 +(*l parse_pos_cas: Token.T list -> (string * Position.T) option * Token.T list*)
4.9 val parse_pos_cas = Scan.option (parse_item \<^keyword>\<open>CAS\<close> (Parse.position Parse.term));
4.10 val parse_methods = parse_item_names \<^keyword>\<open>Method_Ref\<close>;
4.11 val ml = ML_Lex.read;
5.1 --- a/src/Tools/isac/MathEngBasic/references.sml Fri Feb 24 16:14:28 2023 +0100
5.2 +++ b/src/Tools/isac/MathEngBasic/references.sml Mon Feb 27 09:45:29 2023 +0100
5.3 @@ -57,7 +57,7 @@
5.4 val id_empty_input = "__/__"
5.5
5.6 val explode_id = References_Def.explode_id
5.7 -(* unused *)
5.8 +(* unused, see Model_Pattern. parse_term_TEST *)
5.9 fun explode_id' pbl_met input_id =
5.10 if input_id = id_empty_input
5.11 then case pbl_met of
5.12 @@ -67,7 +67,7 @@
5.13 else space_explode "/" input_id
5.14
5.15 val implode_id = References_Def.implode_id
5.16 -(* unused *)
5.17 +(* unused, see Model_Pattern. parse_term_TEST *)
5.18 fun implode_id' _ id =
5.19 if id = Problem.id_empty orelse id = MethodC.id_empty then id_empty_input
5.20 else References_Def.implode_id id
5.21 @@ -99,7 +99,7 @@
5.22 As long as in_* is empty (then spec_* is empty, except rare cases with \<Odot>\<Otimes>),
5.23 o_* is taken.
5.24 o_* is (too often?) true while References.empty.
5.25 - ATTENTION with redesign: if "in_* <> id_empty_input" then take "id_empty_input' "
5.26 + ATTENTION with redesign: if "in_* <> id_empty_input" then take "id_empty_input'"
5.27 *)
5.28 fun for_eval_model (in_thy, in_pbl, in_met) (spec_thy, spec_pbl, spec_met) (o_thy, o_pbl, o_met) =
5.29 let
6.1 --- a/src/Tools/isac/Specify/i-model.sml Fri Feb 24 16:14:28 2023 +0100
6.2 +++ b/src/Tools/isac/Specify/i-model.sml Mon Feb 27 09:45:29 2023 +0100
6.3 @@ -31,7 +31,6 @@
6.4 val to_string_TEST: Proof.context -> T_TEST -> string
6.5
6.6 datatype add_single = Add of single | Err of string
6.7 -(*val init: Proof.context -> Model_Pattern.T -> T*)
6.8 val init: Model_Pattern.T -> T
6.9 val init_TEST: Model_Pattern.T -> T_TEST
6.10 val check_single: Proof.context -> m_field -> O_Model.T -> T -> Model_Pattern.T ->
6.11 @@ -60,7 +59,6 @@
6.12 val to_p_model: theory -> feedback -> string
6.13 val eq1: ''a -> 'b * (''a * 'c) -> bool
6.14 (*from isac_test for Minisubpbl*)
6.15 - val empty_for: typ -> string
6.16
6.17 \<^isac_test>\<open>
6.18 (**)
6.19 @@ -102,12 +100,9 @@
6.20 | feedback_to_string ctxt (Sup (d, ts)) =
6.21 "Sup " ^ UnparseC.term ctxt (Input_Descript.join (d, ts))
6.22 | feedback_to_string ctxt (Mis (d, pid)) =
6.23 - "Mis "^ UnparseC.term ctxt d ^ " " ^ UnparseC.term ctxt pid
6.24 + "Mis " ^ UnparseC.term ctxt d ^ " " ^ UnparseC.term ctxt pid
6.25 | feedback_to_string _ (Par s) = "Trm "^s;
6.26 -fun empty_for (Type ("fun", [Type ("List.list", [Type ("HOL.bool", [])]), _])) = "[__=__, __=__]"
6.27 - | empty_for (Type ("fun", [Type ("List.list", [Type ("Real.real", [])]), _])) = "[__, __]"
6.28 - | empty_for (Type ("HOL.bool", [])) = "(__=__)"
6.29 - | empty_for _ = "__"
6.30 +
6.31 fun feedback_to_string_TEST ctxt (Cor_TEST ((d, ts), penv)) =
6.32 "Cor_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " ," ^ pen2str ctxt penv
6.33 | feedback_to_string_TEST ctxt (Inp_TEST (descriptor, format)) =
6.34 @@ -154,7 +149,7 @@
6.35 let
6.36 fun pat_to_item (m_field, (descriptor, _)) =
6.37 (0, [], false, m_field, (Position.none,
6.38 - Inp_TEST (descriptor, empty_for (type_of descriptor))))
6.39 + Inp_TEST (descriptor, Model_Pattern.empty_for (type_of descriptor))))
6.40 in map pat_to_item model_patt end
6.41 (*########################* )
6.42 val init = init_TEST see Test_Theory.thy
7.1 --- a/test/Tools/isac/BridgeJEdit/Test_VSCode_Example.thy Fri Feb 24 16:14:28 2023 +0100
7.2 +++ b/test/Tools/isac/BridgeJEdit/Test_VSCode_Example.thy Mon Feb 27 09:45:29 2023 +0100
7.3 @@ -34,7 +34,7 @@
7.4 \<close> ML \<open>
7.5 \<close> ML \<open> (** preliminary handling of References **)
7.6 \<close> ML \<open> (* assumption: we read the Specfication as a whole *)
7.7 -(*/-------------------- state of src/../preliminary at that time -----------------------------\*)
7.8 +(*/-------------------- state of src/../preliminary.sml at that time -------------------------\*)
7.9 fun re_eval_all ((*dummyarg*)) = ("re_eval_all if new_thy"; ((*dummyarg*)))
7.10 fun re_eval_pbl ((*dummyarg*)) = ("re_eval_pbl"; ((*dummyarg*)))
7.11 fun re_eval_met ((*dummyarg*)) = ("re_eval_met"; ((*dummyarg*)))
7.12 @@ -61,7 +61,7 @@
7.13 \<close> ML \<open>
7.14 \<close> ML \<open>
7.15 \<close> ML \<open>
7.16 -(*\-------------------- state of src/../preliminary at that time -----------------------------/*)
7.17 +(*\-------------------- state of src/../preliminary.sml at that time -------------------------/*)
7.18 \<close> ML \<open> (*\<longrightarrow> test/../calculation.sml*)
7.19 "----------- build Outer_Syntax Example_TEST ---------------------------------------------------";
7.20 "----------- build Outer_Syntax Example_TEST ---------------------------------------------------";
7.21 @@ -94,18 +94,12 @@
7.22 | _ => the_data thy
7.23 \<close> ML \<open>
7.24 (*let*)
7.25 - val ctree = the_data thy
7.26 val {origin = (_, o_ref, _), spec = spec_ref, ctxt, ...} =
7.27 - Ctree.get_obj I ctree [(*Pos will become variable*)] |> Ctree.rep_specify_data
7.28 + Ctree.get_obj I state [(*Pos will become variable*)] |> Ctree.rep_specify_data
7.29 val thy_id' = References.for_parse thy_id (#1 spec_ref) (#1 o_ref)
7.30 - val (model, where_) = Model_Pattern.parse_pos ctxt model_input (*+check syntax*)
7.31 + val (model, where_) = Model_Pattern.parse_pos_TEST ctxt model_input (*+check syntax*)
7.32 \<close> ML \<open>
7.33 -\<close> ML \<open>
7.34 -(*Specify.check_input \<longrightarrow> specify.sml*)
7.35 -fun check_input _ = 123
7.36 -\<close> ML \<open>
7.37 -\<close> ML \<open>
7.38 -\<close> ML \<open>
7.39 +(model, where_) (*GOON*)
7.40 \<close> ML \<open>
7.41 (**)
7.42 val _ = re_eval References.empty References.empty;
7.43 @@ -115,6 +109,8 @@
7.44 (example_id, (model_input, (thy_id, probl_id, meth_id))) (the_data thy)
7.45 (*end*)
7.46 \<close> ML \<open>
7.47 +(*POSTPONED Specify.check_input \<longrightarrow> specify.sml*)
7.48 +fun check_input _ = 123
7.49 \<close> ML \<open>
7.50 \<close> ML \<open>
7.51 \<close> ML \<open>
7.52 @@ -142,15 +138,16 @@
7.53 | _ =>
7.54 let
7.55 val {origin = (_, o_ref, _), spec = spec_ref, ctxt, ...} =
7.56 - Ctree.get_obj I (the_data thy) [] |> Ctree.rep_specify_data
7.57 + Ctree.get_obj I state [] |> Ctree.rep_specify_data
7.58 val thy_id' = References.for_parse thy_id (#1 spec_ref) (#1 o_ref)
7.59 - val (model, where_) = Model_Pattern.parse_pos ctxt model_input
7.60 + val (model, where_) = Model_Pattern.parse_pos_TEST ctxt model_input
7.61 (**)
7.62 val _ = re_eval References.empty References.empty
7.63 (**)
7.64 - in Preliminary.update_state_TEST thy
7.65 + in
7.66 + Preliminary.update_state_TEST thy
7.67 (example_id, (model_input, (thy_id, probl_id, meth_id))) (the_data thy)
7.68 - end
7.69 + end
7.70 in set_data state thy end)));
7.71 \<close> ML \<open>
7.72 \<close> ML \<open> (*Example_TEST below*)
7.73 @@ -180,7 +177,13 @@
7.74 text \<open>
7.75 Check complete \<open>Model\<close>, infer empty \<open>References\<close> from data hidden in "Diff_App-No.123a"
7.76 \<close>
7.77 -Example_TEST "Diff_App-No.123a" (*complete Model, empty References*)
7.78 +(*
7.79 +Example: no syntax check of terms, OK.
7.80 +Example_TEST: proper syntax check of terms with Model_Pattern.parse_pos,
7.81 + but with parse_pos_TEST ERROR Malformed YXML: unbalanced element "input"
7.82 +*)
7.83 +(**)Example
7.84 +(** )Example_TEST( **) "Diff_App-No.123a" (*complete Model, empty References*)
7.85 Specification:
7.86 Model:
7.87 Given: \<open>Constants [r = 7]\<close>
8.1 --- a/test/Tools/isac/BridgeJEdit/calculation.sml Fri Feb 24 16:14:28 2023 +0100
8.2 +++ b/test/Tools/isac/BridgeJEdit/calculation.sml Mon Feb 27 09:45:29 2023 +0100
8.3 @@ -40,7 +40,7 @@
8.4 (*/---------------------------------------- mimic input from PIDE -----------------------------\*)
8.5 (* Example_TEST "Diff_App-No.123a" (*complete Model, empty References*) *)
8.6 val in_refs as (thy_id, probl_id, meth_id) = ("__", "__/__", "__/__")
8.7 -val thy = @{theory}
8.8 +val thy = @{theory Calculation}
8.9 val model_input = (*type Position.T is hidden, thus redefinition*)
8.10 [("#Given", [("Constants [r = 7]", Position.none)]),
8.11 ("#Where", [("0 < r", Position.none)]),
8.12 @@ -50,14 +50,14 @@
8.13 [("Extremum (A = 2 * u * v - u \<up> 2)", Position.none),
8.14 ("SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]", Position.none)])]
8.15 : (Model_Pattern.m_field * (string * Position.T) list) list
8.16 -val example_id = "Diff_App-No.123a"
8.17 +val example_id = "Diff_App-No.123a";
8.18 (*\---------------------------------------- mimic input from PIDE -----------------------------/*)
8.19 (*/---------------------------------------- adapt to Test_Isac/_Short.thy ---------------------\*)
8.20 -val ctree = Preliminary.init_ctree_TEST thy example_id;
8.21 -(* --- why does this not work?
8.22 +(**)val ctree = Preliminary.init_ctree_TEST thy example_id;
8.23 +(** ) --- why does this not work? ( **)
8.24 set_data ctree thy;
8.25 the_data thy;
8.26 ------- why does this not work? Note (**)ctree(** )(the_data thy)( **) below.*)
8.27 +(** )-- why does this not work? Note (**)ctree(** )(the_data thy)( **) below.*)
8.28 (*\---------------------------------------- adapt to Test_Isac/_Short.thy ---------------------/*)
8.29 val state =
8.30 case the_data thy of
9.1 --- a/test/Tools/isac/Test_Isac.thy Fri Feb 24 16:14:28 2023 +0100
9.2 +++ b/test/Tools/isac/Test_Isac.thy Mon Feb 27 09:45:29 2023 +0100
9.3 @@ -302,14 +302,14 @@
9.4 ML_file "BridgeLibisabelle/interface-xml.sml" (*TODO after 2009-2*)
9.5 ML_file "BridgeLibisabelle/interface.sml"
9.6
9.7 -(**) (* evaluated in Build_Isac.thy already *)
9.8 +(** ) (* evaluated in Build_Isac.thy already *)
9.9 ML_file "BridgeJEdit/e-collect.sml"
9.10 ML_file "BridgeJEdit/user-model.sml"
9.11 ML_file "BridgeJEdit/template.sml"
9.12 ML_file "BridgeJEdit/preliminary.sml"
9.13 ML_file "BridgeJEdit/calculation.sml"
9.14 ML_file "BridgeJEdit/vscode-example.sml"
9.15 -(**)
9.16 +( **)
9.17
9.18 ML_file "Knowledge/delete.sml"
9.19 ML_file "Knowledge/descript.sml"