1.1 --- a/src/Tools/isac/Specify/calchead.sml Mon May 04 16:47:32 2020 +0200
1.2 +++ b/src/Tools/isac/Specify/calchead.sml Mon May 04 17:08:32 2020 +0200
1.3 @@ -69,16 +69,16 @@
1.4 type calcstate
1.5 type calcstate'
1.6
1.7 - val nxt_spec : Pos.pos_ -> bool -> Model.ori list -> Spec.T -> Model.itm list * Model.itm list ->
1.8 + val nxt_spec : Pos.pos_ -> bool -> O_Model.T -> Spec.T -> I_Model.T * I_Model.T ->
1.9 (string * (term * 'a)) list * (string * (term * 'b)) list -> Spec.T -> Pos.pos_ * Tactic.input
1.10
1.11 val reset_calchead : Calc.T -> Calc.T
1.12 val get_ocalhd : Calc.T -> Ctree.ocalhd
1.13 - val ocalhd_complete : Model.itm list -> (bool * term) list -> ThyC.id * Problem.id * Method.id -> bool
1.14 + val ocalhd_complete : I_Model.T -> (bool * term) list -> ThyC.id * Problem.id * Method.id -> bool
1.15 val all_modspec : Calc.T -> Calc.T
1.16
1.17 - val complete_metitms : Model.ori list -> Model.itm list -> Model.itm list -> Celem4.pat list -> Model.itm list
1.18 - val insert_ppc' : Model.itm -> Model.itm list -> Model.itm list
1.19 + val complete_metitms : O_Model.T -> I_Model.T -> I_Model.T -> Celem4.pat list -> I_Model.T
1.20 + val insert_ppc' : I_Model.single -> I_Model.T -> I_Model.T
1.21
1.22 val complete_mod : Calc.T -> Calc.T
1.23 val is_complete_mod : Calc.T -> bool
1.24 @@ -91,21 +91,21 @@
1.25 val pt_extract : Calc.T -> Ctree.ptform * Tactic.input option * term list
1.26 val get_interval : Pos.pos' -> Pos.pos' -> int -> Ctree.ctree -> (Pos.pos' * term * Tactic.input option) list
1.27
1.28 - val match_ags : theory -> Celem4.pat list -> term list -> Model.ori list
1.29 + val match_ags : theory -> Celem4.pat list -> term list -> O_Model.T
1.30 val match_ags_msg : Problem.id -> term -> term list -> unit
1.31 - val oris2fmz_vals : Model.ori list -> string list * term list
1.32 + val oris2fmz_vals : O_Model.T -> string list * term list
1.33 val vars_of_pbl_' : ('a * ('b * term)) list -> term list
1.34 - val is_known : Proof.context -> string -> Model.ori list -> term -> string * Model.ori * term list
1.35 - val is_notyet_input : Proof.context -> Model.itm list -> term list -> Model.ori -> ('a * (term * term)) list
1.36 - -> string * Model.itm
1.37 + val is_known : Proof.context -> string -> O_Model.T -> term -> string * O_Model.single * term list
1.38 + val is_notyet_input : Proof.context -> I_Model.T -> term list -> O_Model.single -> ('a * (term * term)) list
1.39 + -> string * I_Model.single
1.40 val ppc2list : 'a Model.ppc -> 'a list
1.41 val mk_delete: theory -> string -> Model.itm_ -> Tactic.input
1.42 val mk_additem: string -> TermC.as_string -> Tactic.input
1.43 - val nxt_add: theory -> Model.ori list -> (string * (term * 'a)) list -> (int * Model.vats * bool * string * Model.itm_) list -> (string * string) option
1.44 + val nxt_add: theory -> O_Model.T -> (string * (term * 'a)) list -> (int * Model.vats * bool * string * Model.itm_) list -> (string * string) option
1.45 val is_error: Model.itm_ -> bool
1.46 - val complete_mod_: (int * int list * string * term * term list) list * ('a * (term * term)) list * ('b * (term * term)) list * Model.itm list -> Model.itm list * Model.itm list
1.47 + val complete_mod_: (int * int list * string * term * term list) list * ('a * (term * term)) list * ('b * (term * term)) list * I_Model.T -> I_Model.T * I_Model.T
1.48 val nxt_specif_additem: string -> TermC.as_string -> Calc.T -> calcstate'
1.49 - val vals_of_oris : Model.ori list -> term list
1.50 + val vals_of_oris : O_Model.T -> term list
1.51 val specify_additem: string -> TermC.as_string -> Calc.T -> string * calcstate'
1.52 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
1.53 val e_calcstate : Calc.T * State_Steps.T
1.54 @@ -117,19 +117,19 @@
1.55 val is_copy_named_generating_idstr : string -> bool
1.56 val is_copy_named_generating : 'a * ('b * term) -> bool
1.57 val is_copy_named : 'a * ('b * term) -> bool
1.58 - val ori2Coritm : Celem4.pat list -> Model.ori -> Model.itm
1.59 + val ori2Coritm : Celem4.pat list -> O_Model.single -> I_Model.single
1.60 val matc : theory -> (string * (term * term)) list -> term list -> Model.preori list -> Model.preori list
1.61 val mtc : theory -> Celem4.pat -> term -> Model.preori option
1.62 val cpy_nam : Celem4.pat list -> Model.preori list -> Celem4.pat -> Model.preori
1.63 - datatype additm = Add of Model.itm | Err of string
1.64 - val appl_add: Proof.context -> string -> Model.ori list ->
1.65 - Model.itm list -> (string * (term * term)) list -> TermC.as_string -> additm
1.66 + datatype additm = Add of I_Model.single | Err of string
1.67 + val appl_add: Proof.context -> string -> O_Model.T ->
1.68 + I_Model.T -> (string * (term * term)) list -> TermC.as_string -> additm
1.69 val seek_oridts: Proof.context -> ''a -> term * term list -> (int * 'b list * ''a * term * term list) list -> string * (int * 'b list * ''a * term * term list) * term list
1.70 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.71
1.72 (*----- kept as hints to initial design ideas; NOT in src/, NOT in test ------------------------*)
1.73 val variants_in : term list -> int
1.74 - val is_untouched : Model.itm -> bool
1.75 + val is_untouched : I_Model.single -> bool
1.76 val is_list_type : typ -> bool
1.77 val parse_ok : Model.itm_ list -> bool
1.78 val all_dsc_in : Model.itm_ list -> term list
1.79 @@ -183,7 +183,7 @@
1.80
1.81 (* is the calchead complete ? *)
1.82 fun ocalhd_complete its pre (dI, pI, mI) =
1.83 - foldl and_ (true, map #3 (its: Model.itm list)) andalso
1.84 + foldl and_ (true, map #3 (its: I_Model.T)) andalso
1.85 foldl and_ (true, map #1 (pre: (bool * term) list)) andalso
1.86 dI <> ThyC.id_empty andalso pI <> Problem.id_empty andalso mI <> Method.id_empty
1.87
1.88 @@ -230,7 +230,7 @@
1.89
1.90 (* find_first item with #1 equal to id *)
1.91 fun seek_ppc _ [] = NONE
1.92 - | seek_ppc id (p :: ppc) = if id = #1 (p: Model.itm) then SOME p else seek_ppc id ppc
1.93 + | seek_ppc id (p :: ppc) = if id = #1 (p: I_Model.single) then SOME p else seek_ppc id ppc
1.94
1.95 fun ppc2list {Given = gis, Where = whs, Find = fis, With = wis, Relate = res} =
1.96 gis @ whs @ fis @ wis @ res
1.97 @@ -311,11 +311,11 @@
1.98 end
1.99 | nxt_add thy oris _ itms =
1.100 let
1.101 - fun testr_vt v ori = member op= (#2 (ori : Model.ori)) v andalso (#3 ori) <> "#undef"
1.102 - fun testi_vt v itm = member op= (#2 (itm : Model.itm)) v
1.103 - fun test_id ids r = member op= ids (#1 (r : Model.ori))
1.104 + fun testr_vt v ori = member op= (#2 (ori : O_Model.single)) v andalso (#3 ori) <> "#undef"
1.105 + fun testi_vt v itm = member op= (#2 (itm : I_Model.single)) v
1.106 + fun test_id ids r = member op= ids (#1 (r : O_Model.single))
1.107 fun test_subset itm (_, _, _, d, ts) =
1.108 - (Model.d_in (#5 (itm: Model.itm))) = d andalso subset op = (Model.ts_in (#5 itm), ts)
1.109 + (Model.d_in (#5 (itm: I_Model.single))) = d andalso subset op = (Model.ts_in (#5 itm), ts)
1.110 fun false_and_not_Sup (_, _, false, _, Model.Sup _) = false
1.111 | false_and_not_Sup (_, _, false, _, _) = true
1.112 | false_and_not_Sup _ = false
1.113 @@ -491,7 +491,7 @@
1.114
1.115
1.116 datatype additm =
1.117 - Add of Model.itm (* return-value of appl_add *)
1.118 + Add of I_Model.single (* return-value of appl_add *)
1.119 | Err of string (* error-message *)
1.120
1.121 (* add an item to the model; check wrt. oris and pbt.
1.122 @@ -878,7 +878,7 @@
1.123 if mI = Method.id_empty then omI else mI)
1.124
1.125 (* get the values from oris; handle the term list w.r.t. penv *)
1.126 -fun vals_of_oris (oris: Model.ori list) =
1.127 +fun vals_of_oris (oris: O_Model.T) =
1.128 ((map (Model.mkval' o (#5))) o
1.129 (filter ((member_swap op= 1) o (#2)))) oris
1.130