1.1 --- a/src/Tools/isac/BaseDefinitions/contextC.sml Thu Nov 26 12:24:37 2020 +0100
1.2 +++ b/src/Tools/isac/BaseDefinitions/contextC.sml Fri Nov 27 16:53:08 2020 +0100
1.3 @@ -31,6 +31,7 @@
1.4
1.5 val empty = Proof_Context.init_global @{theory "Pure"};
1.6 (* ATTENTION: does _not_ recognise Variable.declare_constraints, etc...*)
1.7 +
1.8 fun is_empty ctxt = Context.eq_thy (Proof_Context.theory_of ctxt, @{theory "Pure"});
1.9 fun isac_ctxt xxx = Proof_Context.init_global (ThyC.Isac xxx)
1.10
2.1 --- a/src/Tools/isac/BaseDefinitions/references.sml Thu Nov 26 12:24:37 2020 +0100
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,51 +0,0 @@
2.4 -(* Title: BaseDefinitions/specification.sml
2.5 - Author: Walther Neuper
2.6 - (c) due to copyright terms
2.7 -
2.8 -References into Know_Store.
2.9 -*)
2.10 -signature REFERENCES =
2.11 -sig
2.12 - type id (* will be specialised to Problem.id, Method.id *)
2.13 - val id_to_string: id -> string
2.14 - val empty_probl_id: id
2.15 - val empty_meth_id: id
2.16 -
2.17 - type T
2.18 - val empty: T
2.19 - val to_string: string * string list * string list -> string
2.20 -
2.21 - val select : T -> T -> T
2.22 -
2.23 -(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
2.24 - (*NONE*)
2.25 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
2.26 - (*NONE*)
2.27 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
2.28 -end
2.29 -
2.30 -(**)
2.31 -structure References(**): REFERENCES(**) =
2.32 -struct
2.33 -(**)
2.34 -
2.35 -type id = string list;
2.36 -val id_to_string = strs2str;
2.37 -val empty_probl_id = ["empty_probl_id"];
2.38 -val empty_meth_id = ["empty_meth_id"];
2.39 -
2.40 -type T = (* 3-dimensional universe of math knowledge: *)
2.41 - ThyC.id * (* reference to a theory comprising definitions *)
2.42 - id * (* will become Problem.id; a reference into a tree *)
2.43 - id; (* will become Method.id; a reference into a tree *)
2.44 -fun to_string (dom, pbl, met) =
2.45 - "(" ^ quote dom ^ ", " ^ strs2str pbl ^ ", " ^ strs2str met ^ ")";
2.46 -val empty = (ThyC.id_empty, empty_probl_id, empty_meth_id);
2.47 -
2.48 -(* select a Specification; if still unspecified take it from PblObj.origin *)
2.49 -fun select (odI, opI, omI) (dI, pI, mI) =
2.50 - (if dI = ThyC.id_empty then odI else dI,
2.51 - if pI = empty_probl_id then opI else pI,
2.52 - if mI = empty_meth_id then omI else mI)
2.53 -
2.54 -(**)end(**)
3.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy Thu Nov 26 12:24:37 2020 +0100
3.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy Fri Nov 27 16:53:08 2020 +0100
3.3 @@ -45,7 +45,83 @@
3.4 (c) due to copyright terms
3.5
3.6 Preliminary code for developing Outer_Syntax.command..Example from spark_open as a model.
3.7 +The original signatures from this subsection are:
3.8 *)
3.9 +signature SPARK_VCS_PARTIALLY =
3.10 +sig
3.11 + val err_unfinished: unit -> 'a
3.12 + val strip_number: string -> string * string
3.13 + val name_ord: string * string -> order
3.14 + structure VCtab: TABLE
3.15 + structure VCs: THEORY_DATA
3.16 + val to_lower: string -> string
3.17 + val partition_opt: ('a -> 'b option) -> 'a list -> 'b list * 'a list
3.18 + val dest_def: 'a * Fdl_Parser.fdl_rule -> ('a * (string * Fdl_Parser.expr)) option
3.19 + val builtin: unit Symtab.table
3.20 + val complex_expr: Fdl_Parser.expr -> bool
3.21 + val complex_rule: Fdl_Parser.fdl_rule -> bool
3.22 + val is_trivial_vc: 'a list * ('b * Fdl_Parser.expr) list -> bool
3.23 + val rulenames: ((string * int) * 'a) list -> string
3.24 + val is_pfun: Symtab.key -> bool
3.25 + val fold_opt: ('a -> 'b -> 'b) -> 'a option -> 'b -> 'b
3.26 + val fold_pair: ('a -> 'b -> 'c) -> ('d -> 'c -> 'e) -> 'a * 'd -> 'b -> 'e
3.27 + val fold_expr: (string -> 'a -> 'a) -> (string -> 'a -> 'a) -> Fdl_Parser.expr -> 'a -> 'a
3.28 + val add_expr_pfuns: 'a Fdl_Parser.tab -> Fdl_Parser.expr -> Symtab.key list -> Symtab.key list
3.29 + val lookup_prfx: string -> 'a Symtab.table -> Symtab.key -> 'a option
3.30 + val fold_vcs: ('a -> 'b -> 'b) -> ('c * 'd * 'a list * 'a list) VCtab.table -> 'b -> 'b
3.31 + val pfuns_of_vcs: string -> 'a Fdl_Parser.tab -> 'b Symtab.table -> ('c * 'd * ('e * Fdl_Parser.expr) list * ('e * Fdl_Parser.expr) list) VCtab.table -> Symtab.key list
3.32 + val booleanN: string
3.33 + val integerN: string
3.34 + val get_type: theory -> string -> Symtab.key -> (typ * (string * string) list) option
3.35 + val mk_type': theory -> string -> string -> typ * (string * string) list
3.36 + val mk_type: theory -> string -> string -> typ
3.37 + val check_no_assoc: theory -> string -> string -> unit
3.38 + val define_overloaded: bstring * term -> Proof.context -> thm * local_theory
3.39 + val add_enum_type: string -> string -> theory -> theory
3.40 + val lcase_eq: string * string -> bool
3.41 + val check_enum: string list -> (string * 'a) list -> string option
3.42 + val strip_prfx: string -> string * string
3.43 + val assoc_ty_err: theory -> typ -> string -> string -> 'a
3.44 + val unprefix_pfun: string -> string -> string
3.45 + val invert_map: (''a * ''a) list -> (''a * 'b) list -> (''a * 'b) list
3.46 + val get_record_info: theory -> typ -> Record.info option
3.47 + val add_type_def: string -> string * Fdl_Parser.fdl_type -> ((term * bstring) Symtab.table * Name.context) * theory -> ((term * bstring) Symtab.table * Name.context) * theory
3.48 + val add_const: string -> bstring * string -> ((term * string) Symtab.table * Name.context) * theory -> term * (((term * string) Symtab.table * Name.context) * theory)
3.49 + val mk_unop: string -> term -> term
3.50 + val strip_underscores: string -> string
3.51 + val strip_tilde: string -> string
3.52 + val mangle_name: string -> string
3.53 + val mk_variables: theory -> string -> string list -> string -> (term * string) Symtab.table * Name.context -> term list * ((term * string) Symtab.table * Name.context)
3.54 + val find_field: (string * string) list -> string -> (string * 'a) list -> (string * 'a) option
3.55 + val find_field': ''a -> (''a list * 'b) list -> 'b option
3.56 + val mk_times: term * term -> term
3.57 + val term_of_expr: theory -> string -> Fdl_Parser.fdl_type Fdl_Parser.tab -> (('a list * string) option * term) Symtab.table -> (term * string) Symtab.table * Name.context -> Fdl_Parser.expr -> term * string
3.58 + val mk_rulename: string * int -> binding
3.59 + val add_def:
3.60 + string ->
3.61 + Fdl_Parser.fdl_type Fdl_Parser.tab ->
3.62 + (('a list * string) option * term) Symtab.table ->
3.63 + string Fdl_Parser.tab -> (string * int) * (string * Fdl_Parser.expr) -> ((term * string) Symtab.table * Name.context) * theory -> (binding * thm) * (((term * string) Symtab.table * Name.context) * theory)
3.64 + val add_expr_idents: Fdl_Parser.expr -> string list -> string list
3.65 + val sort_defs:
3.66 + string ->
3.67 + 'a Fdl_Parser.tab ->
3.68 + 'b Symtab.table -> (string -> bool) -> ((string * int) * (string * Fdl_Parser.expr)) list -> ((string * int) * (string * Fdl_Parser.expr)) list -> ((string * int) * (string * Fdl_Parser.expr)) list
3.69 + val add_var: string -> string * string -> ((term * string) Symtab.table * Name.context) * theory -> (string * typ) * (((term * string) Symtab.table * Name.context) * theory)
3.70 + val add_init_vars:
3.71 + string ->
3.72 + ('a * 'b * ('c * Fdl_Parser.expr) list * ('c * Fdl_Parser.expr) list) VCtab.table ->
3.73 + ((term * string) Symtab.table * Name.context) * theory -> (string * typ) list * (((term * string) Symtab.table * Name.context) * theory)
3.74 + val term_of_rule: theory -> string -> Fdl_Parser.fdl_type Fdl_Parser.tab -> (('a list * string) option * term) Symtab.table -> (term * string) Symtab.table * Name.context -> Fdl_Parser.fdl_rule -> term
3.75 + val pfun_type: theory -> string -> string list * string -> typ
3.76 + val check_pfun_type: theory -> string -> string -> term -> (string list * string) option -> (string list * string) option -> unit
3.77 + val upd_option: 'a option -> 'a option -> 'a option
3.78 + val check_pfuns_types: theory -> string -> (string list * string) Fdl_Parser.tab -> ((string list * string) option * term) Symtab.table -> ((string list * string) option * term) Symtab.table
3.79 + val pp_vcs: string -> (string * 'a) list -> Pretty.T
3.80 + val pp_open_vcs: (string * 'a) list -> Pretty.T
3.81 + val partition_vcs: ('a * 'b option * 'c * 'd) VCtab.table -> (VCtab.key * ('a * 'b * 'c * 'd)) list * (VCtab.key * ('a * 'c * 'd)) list
3.82 + val print_open_vcs: (Pretty.T -> Pretty.T) -> ('a * 'b option * 'c * 'd) VCtab.table -> ('a * 'b option * 'c * 'd) VCtab.table
3.83 +end
3.84
3.85 (** theory data **)
3.86
3.87 @@ -987,7 +1063,8 @@
3.88 (* set_env: Element.context_i list -> (binding * thm) list -> fdl_type tab ->
3.89 (string list * string) tab -> term * string) Symtab.table * Name.context ->
3.90 (string * thm list option * (string * expr) list * (string * expr) list) VCtab.table ->
3.91 - Path.T -> string -> theory -> theory *)
3.92 + Path.T -> string -> theory -> theory
3.93 + Context --vvvv is made Theory_Data by -------------------vvvvvvv, see.def. above *)
3.94 fun set_env ctxt defs types funs ids vcs path prefix thy = VCs.map (fn
3.95 {pfuns, type_map, env = NONE} =>
3.96 {pfuns = pfuns,
3.97 @@ -1008,8 +1085,41 @@
3.98 val map: (T -> T) -> theory -> theory (*..(VCs.T -> VCs.T)*)
3.99 end;
3.100 *)
3.101 -\<close> text \<open>
3.102 -val hdl =
3.103 +\<close> ML \<open>
3.104 +structure Refs_Data = Theory_Data
3.105 +(
3.106 + type T = References.T
3.107 + val empty : T = References.empty
3.108 + val extend = I
3.109 + fun merge (_, refs) = refs
3.110 +);
3.111 +(*
3.112 +Refs_Data.empty; (*in Refs_Data defined workers are hidden*)
3.113 +Refs_Data.extend; (*in Refs_Data defined workers are hidden*)
3.114 +Refs_Data.merge; (*in Refs_Data defined workers are hidden*)
3.115 +ML error\<^here>:
3.116 +Value or constructor (empty) has not been declared in structure Refs *)
3.117 +
3.118 +Refs_Data.get: theory -> Refs_Data.T; (*from signature THEORY_DATA*)
3.119 +Refs_Data.put: Refs_Data.T -> theory -> theory; (*from signature THEORY_DATA*)
3.120 +Refs_Data.map: (Refs_Data.T -> Refs_Data.T) -> theory -> theory; (*from signature THEORY_DATA*)
3.121 +\<close> ML \<open>
3.122 +structure OMod_Data = Theory_Data
3.123 +(
3.124 + type T = O_Model.T
3.125 + val empty : T = []
3.126 + val extend = I
3.127 + fun merge (_, o_model) = o_model
3.128 +)
3.129 +\<close> ML \<open>
3.130 +structure Ctxt_Data = Theory_Data
3.131 +(
3.132 + type T = Proof.context
3.133 + val empty : T = ContextC.empty
3.134 + val extend = I
3.135 + fun merge (_, ctxt) = ctxt
3.136 +)
3.137 +\<close> ML \<open>
3.138 \<close> ML \<open>
3.139 fun set_vcs _(*{types, vars, consts, funs} : Fdl_Parser.decls*)
3.140 _(*rules, _*) _(*(_, ident), vcs*) header path opt_prfx thy =
3.141 @@ -1021,13 +1131,13 @@
3.142 val ((_, ident), vcs) =
3.143 snd (Fdl_Parser.parse_vcs Fdl_Lexer.siv_header Position.start g_c_d_siv_content)
3.144 (*------ new argument: ParseC.vcs = ParseC.formalise ----------------------*)
3.145 - val formalise :: _ = case header of xxx as
3.146 + val formalise = case header of xxx as
3.147 [(["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y", "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]", "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]", "AbleitungBiegelinie dy"],
3.148 - ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))] => xxx
3.149 + ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))] => hd xxx
3.150 | _ => error "magic failed: handling file exp_Statics_Biegel_Timischl_7-70.str failed"
3.151 (*\----- keep running from spark_open \<open>greatest_common_divisor/g_c_d\<close> -----/*)
3.152 - val (hdlPIDE, _, (dI, pI, mI), pors, frees, _) = Step_Specify.initialisePIDE formalise
3.153 -
3.154 + val (hdlPIDE, _, refs, o_model, var_type_ctxt) = Step_Specify.initialisePIDE formalise
3.155 + (* ^^^^^^^ goes to PIDE as "Problem hdlPIDE" *)
3.156
3.157 val prfx' =
3.158 if opt_prfx = "" then
3.159 @@ -1053,11 +1163,11 @@
3.160 [] => ()
3.161 | fs => error ("Undeclared proof function(s) " ^ commas fs));
3.162
3.163 - val (((defs', vars''), ivars), (ids, thy')) = (*..thy'*)
3.164 + val (((defs', vars''), ivars)(*->*),(*<-*) (ids, thy')) = (*..thy'*)
3.165 ((Symtab.empty |>
3.166 Symtab.update ("false", (\<^term>\<open>False\<close>, booleanN)) |>
3.167 Symtab.update ("true", (\<^term>\<open>True\<close>, booleanN)), (*..(defs', vars'')*)
3.168 - Name.context), (*..ivars*)
3.169 + Name.context)(*->*),(*<-*) (*..ivars*)
3.170 thy |> Sign.add_path (*..thy*)
3.171 ((if prfx' = "" then "" else prfx' ^ "__") ^ Long_Name.base_name ident)) |>
3.172 fold (add_type_def prfx) (Fdl_Parser.items types) |>
3.173 @@ -1066,7 +1176,7 @@
3.174 fold_map (add_def prfx types pfuns consts)
3.175 (sort_defs prfx funs pfuns (Symtab.defined tab) defs []) ||>>
3.176 fold_map (add_var prfx) (Fdl_Parser.items vars) ||>>
3.177 - add_init_vars prfx vcs'); (*..(ids, thy')*)
3.178 + add_init_vars prfx vcs'); (*..(ids, thy')*)
3.179
3.180 val ctxt =
3.181 [Element.Fixes (map (fn (s, T) =>
3.182 @@ -1079,6 +1189,9 @@
3.183
3.184 in
3.185 set_env ctxt defs' types funs ids vcs' path prfx thy'
3.186 + |> Refs_Data.put refs
3.187 + |> OMod_Data.put o_model
3.188 + |> Ctxt_Data.put var_type_ctxt
3.189 end;
3.190 \<close> ML \<open>
3.191 \<close>
4.1 --- a/src/Tools/isac/Specify/step-specify.sml Thu Nov 26 12:24:37 2020 +0100
4.2 +++ b/src/Tools/isac/Specify/step-specify.sml Fri Nov 27 16:53:08 2020 +0100
4.3 @@ -10,7 +10,7 @@
4.4 val by_tactic: Tactic.T -> Calc.T -> string * Calc.state_post
4.5
4.6 val initialisePIDE: Formalise.T ->
4.7 - term * term * References.T * O_Model.T * term list * Proof.context
4.8 + term * term * References.T * O_Model.T * Proof.context
4.9 val nxt_specify_init_calc: Formalise.T -> Calc.T * State_Steps.T
4.10 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
4.11 (*NONE*)
4.12 @@ -240,10 +240,8 @@
4.13 val hdlPIDE = case cas of
4.14 NONE => Auto_Prog.pbltermPIDE dI pI
4.15 | SOME t => subst_atomic ((Model_Pattern.variables ppc) ~~~ O_Model.values pors) t
4.16 - val frees = map (TermC.parseNEW' (Proof_Context.init_global thy)) fmz |> TermC.vars'
4.17 - (*^^^^^^^^^ DUPLICATE ermC.parseNEW'*)
4.18 in
4.19 - (hdlPIDE, hdl, (dI, pI, mI), pors, frees, pctxt)
4.20 + (hdlPIDE, hdl, (dI, pI, mI), pors, pctxt)
4.21 end;
4.22 (* nxt_specify_init_calc \<rightarrow> initialise *)
4.23 fun nxt_specify_init_calc ([], (dI, pI, mI)) = (*this will probably be dropped with PIDE*)
4.24 @@ -279,7 +277,7 @@
4.25 in ((pt, ([], Pbl)), []) end
4.26 | nxt_specify_init_calc (fmz, (dI, pI, mI)) =
4.27 let (* both ^^^ ^^^^^^^^^^^^ are either empty or complete *)
4.28 - val (_, hdl, (dI, pI, mI), pors, _, pctxt) = initialisePIDE (fmz, (dI, pI, mI))
4.29 + val (_, hdl, (dI, pI, mI), pors, pctxt) = initialisePIDE (fmz, (dI, pI, mI))
4.30 val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, pctxt)
4.31 (fmz, (dI, pI, mI)) (pors, (dI, pI, mI), hdl, pctxt)
4.32 in
5.1 --- a/test/Pure/General/Basics.thy Thu Nov 26 12:24:37 2020 +0100
5.2 +++ b/test/Pure/General/Basics.thy Fri Nov 27 16:53:08 2020 +0100
5.3 @@ -7,34 +7,49 @@
5.4 begin
5.5
5.6 subsection \<open>Pure/General/basics.ML line by line\<close>
5.7 +text \<open>
5.8 + Combinators are best understood by looking at their fun definition
5.9 + in relation to their signature.
5.10 +\<close>
5.11 +subsubsection \<open>application and structured results\<close>
5.12 +(*fun x |> f = f x;
5.13 + val |> : 'a * ('a -> 'b) -> 'b*)
5.14 ML \<open>op |> ;
5.15 1 |> (fn x => x + 10)
5.16 |> (fn x => 2 * x);
5.17 (*val it = 22 : int*)
5.18 \<close>
5.19 -
5.20 +(*fun (x , y) |-> f = f x y;
5.21 + val |-> : ('c * 'a) * ('c -> 'a -> 'b) -> 'b*)
5.22 ML \<open>op |-> ;
5.23 fun ff c a = a + c;
5.24 (10, 1) |-> ff
5.25 (*val it = 11 : int*)
5.26 \<close>
5.27 -
5.28 +(*fun (x , y) |>> f = (f x, y);
5.29 + val |>> : ('a * 'c) * ('a -> 'b) -> 'b * 'c*)
5.30 ML \<open>op |>> ;
5.31 (1, "a") |>> (fn x => x + 10)
5.32 (*val it = (11, "a") : int * string*)
5.33 \<close>
5.34 -
5.35 +(*fun (x , y) ||> f = (x, f y);
5.36 + val ||> : ('c * 'a) * ('a -> 'b) -> 'c * 'b*)
5.37 ML \<open>op ||> ;
5.38 ("a", 1) ||> (fn x => x + 10)
5.39 (*val it = ("a", 11) : string * int*)
5.40 \<close>
5.41 -
5.42 -ML \<open>
5.43 - op ||>>;
5.44 +(*fun (x , y) ||>> f = let val (z, y') = f y in ((x, z), y') end;
5.45 + val ||>> : ('c * 'a) * ('a -> 'd * 'b) -> ('c * 'd) * 'b
5.46 + applied to ^^ and re-arranged ^^^ ^^^^^^^*)
5.47 +ML \<open> op ||>>;
5.48 (444, 2) ||>> (fn e => (e * 3, e + 5));
5.49 - (*val it = ((444, 6), 7): (int * int) * int*)
5.50 +(*val it = ((444, 6), 7): (int * int) * int*)
5.51 \<close>
5.52
5.53 +subsubsection \<open>composition and structured results\<close>
5.54 +text \<open>
5.55 + Note the analogies between |* above and #* below.
5.56 +\<close>
5.57 ML \<open>
5.58 op #>;
5.59 ((fn a => a + 10) #> (fn a => a + 5)) 3;