src/Tools/isac/Specify/p-spec.sml
author wneuper <Walther.Neuper@jku.at>
Sat, 29 Apr 2023 15:53:37 +0200
changeset 60708 9e987411cfda
parent 60676 8c37f1009457
child 60709 cb44eefd3c7b
permissions -rw-r--r--
add missing I_Model.OLD_to_TEST to sig
walther@59822
     1
(* Title:  Specify/input-calchead.sml
walther@59822
     2
   Author: Walther Neuper
walther@59822
     3
   (c) due to copyright terms
walther@59960
     4
walther@60111
     5
This will be dropped at switch to Isabelle/PIDE .
walther@59960
     6
*)
walther@59822
     7
walther@59984
     8
signature PRESENTATION_SPECIFICATION =
walther@59822
     9
sig
walther@60132
    10
  type record
walther@59995
    11
(*/------- rename -------\*)
walther@59960
    12
  datatype iitem =
walther@59960
    13
      Find of TermC.as_string list
walther@59960
    14
    | Given of TermC.as_string list
walther@59960
    15
    | Relate of TermC.as_string list
walther@59822
    16
  type imodel = iitem list
walther@59976
    17
  type icalhd = Pos.pos' * TermC.as_string * imodel * Pos.pos_ * References.T
walther@59995
    18
  val empty: icalhd
walther@60097
    19
  val input_icalhd : Ctree.ctree -> icalhd -> Ctree.ctree * SpecificationC.T
wenzelm@60223
    20
\<^isac_test>\<open>
walther@59977
    21
  val appl_add': ThyC.id -> O_Model.T -> I_Model.T -> Model_Pattern.T ->
walther@59977
    22
    string * TermC.as_string -> I_Model.single
walther@59977
    23
  val appl_adds: ThyC.id -> O_Model.T -> I_Model.T -> Model_Pattern.T ->
walther@59977
    24
    (string * TermC.as_string) list -> I_Model.T
walther@59977
    25
  val eq7: ''a * ''b -> ''a * (''b * 'c) -> bool
walther@59977
    26
  val filter_sep: ('a -> bool) -> 'a list -> 'a list * 'a list
walther@59977
    27
  val fstr2itm_: theory -> (''a * (term * term)) list -> ''a * string ->
walther@59977
    28
    int list * bool * ''a * I_Model.feedback (*I_Model.single'*)
walther@59977
    29
  val imodel2fstr: iitem list -> (string * TermC.as_string) list
walther@59977
    30
  val is_Par: 'a * 'b * 'c * 'd * I_Model.feedback -> bool (*I_Model.T?*)
walther@59977
    31
  val is_e_ts: term list -> bool
Walther@60673
    32
  val itms2fstr: Proof.context -> I_Model.single -> string * string
walther@59977
    33
  val par2fstr: I_Model.single -> string * TermC.as_string
walther@59977
    34
  val parsitm: theory -> I_Model.single -> I_Model.single
walther@59977
    35
  val unknown_expl: ThyC.id -> (''a * (term * term)) list -> (*Model_Pattern.T?*)
walther@59977
    36
    (''a * string) list ->
walther@59977
    37
      (int * int list * bool * ''a * Model_Def.i_model_feedback) list (*I_Model.T?*)
wenzelm@60223
    38
\<close>
walther@59995
    39
(*\------- rename -------/*)
walther@59822
    40
end
walther@59822
    41
walther@59977
    42
(**)
walther@59984
    43
structure P_Spec(**): PRESENTATION_SPECIFICATION(**) =
walther@59822
    44
struct
walther@59977
    45
(**)
walther@59822
    46
walther@60132
    47
  type record = {thy_id: ThyC.id, pbl_id: Problem.id,           (* headline of Problem *)
walther@60132
    48
    givens: TermC.as_string list, wheres: TermC.as_string list, (* Model.T             *)
walther@60132
    49
      find: TermC.as_string, relates: TermC.as_string list,
walther@60154
    50
    rthy_id: ThyC.id, rpbl_id: Problem.id, rmet_id: MethodC.id}  (* References.T        *)
walther@60132
    51
walther@59822
    52
fun flattup2 (a, (b ,c, d, e)) = (a, b, c, d, e)
walther@59822
    53
walther@59982
    54
(** handle an input P_Specific'action **)
walther@59822
    55
walther@59822
    56
datatype iitem = 
walther@59865
    57
  Given of TermC.as_string list
walther@59977
    58
(*Where is still not input*) 
walther@59865
    59
| Find  of TermC.as_string list
walther@59865
    60
| Relate  of TermC.as_string list
walther@59822
    61
walther@59822
    62
type imodel = iitem list
walther@59822
    63
walther@59822
    64
type icalhd =
walther@59977
    65
  Pos.pos' *         (* the position in Ctree              *) 
walther@59977
    66
  TermC.as_string *  (* the headline shown on Calc.T       *)
walther@59977
    67
  imodel *           (* the model                          *)
walther@60154
    68
  Pos.pos_ *         (* model belongs to Problem or MethodC *)
walther@59977
    69
  References.T;      (* into Know_Store                    *)
walther@59995
    70
val empty = (Pos.e_pos', "", [Given [""]], Pos.Pbl, References.empty)
walther@59822
    71
walther@59822
    72
(* re-parse itms with a new thy and prepare for checking with ori list *)
Walther@60673
    73
fun parsitm thy (itm as (i, v, _, f, I_Model.Cor ((d, ts), _))) =
walther@60265
    74
    (case \<^try>\<open>
walther@60265
    75
        let val t = Input_Descript.join (d, ts)
Walther@60673
    76
          val _ = (UnparseC.term_in_thy thy t)
walther@60265
    77
          (*t his ^^^^^^^^^^^^ should raise the exn on unability of re-parsing dts *)
walther@60265
    78
        in itm end\<close> of
walther@60265
    79
      SOME x => x
Walther@60674
    80
    | NONE =>
Walther@60674
    81
      (i, v, false, f, I_Model.Syn (UnparseC.term_in_thy thy TermC.empty (*t  ..(t) has not been declared*))))
Walther@60673
    82
  | parsitm _ (i, v, b, f, I_Model.Syn str) =
walther@60265
    83
    (case \<^try>\<open>
Walther@60664
    84
        let val _ = Syntax.read_term\<^context> str
walther@60265
    85
        in (i, v, b ,f, I_Model.Par str) end\<close> of
walther@60265
    86
      SOME x => x
walther@60265
    87
    | NONE => (i, v, b, f, I_Model.Syn str))
Walther@60673
    88
  | parsitm _ (i, v, b, f, I_Model.Typ str) =
walther@60265
    89
    (case \<^try>\<open>
Walther@60664
    90
        let val _ = Syntax.read_term\<^context> str
walther@60265
    91
         in (i, v, b, f, I_Model.Par str) end\<close> of
walther@60265
    92
      SOME x => x
walther@60265
    93
    | NONE => (i, v, b, f, I_Model.Syn str))
Walther@60673
    94
  | parsitm thy (itm as (i, v, _, f, I_Model.Inc ((d, ts), _))) =
walther@60265
    95
    (case \<^try>\<open>
walther@60265
    96
        let val t = Input_Descript.join (d,ts);
Walther@60673
    97
	        val _ = UnparseC.term_in_thy thy t;
walther@60265
    98
        (*this    ^ should raise the exn on unability of re-parsing dts*)
walther@60265
    99
        in itm end\<close> of
walther@60265
   100
      SOME x => x
Walther@60674
   101
    | NONE => (i, v, false, f, I_Model.Syn (UnparseC.term_in_thy thy TermC.empty (*t  ..(t) has not been declared*))))
Walther@60673
   102
  | parsitm thy (itm as (i, v, _, f, I_Model.Sup (d, ts))) =
walther@60265
   103
    (case \<^try>\<open>
walther@60265
   104
        let val t = Input_Descript.join (d,ts);
Walther@60673
   105
	        val _ = UnparseC.term_in_thy thy t;
walther@60265
   106
        (*this    ^ should raise the exn on unability of re-parsing dts*)
walther@60265
   107
        in itm end\<close> of
walther@60265
   108
      SOME x => x
Walther@60674
   109
    | NONE => (i, v, false, f, I_Model.Syn (UnparseC.term_in_thy thy TermC.empty (*t  ..(t) has not been declared*))))
Walther@60673
   110
  | parsitm thy (itm as (i, v, _, f, I_Model.Mis (d, t'))) =
walther@60265
   111
    (case \<^try>\<open>
walther@60265
   112
        let val t = d $ t';
Walther@60673
   113
	        val _ = UnparseC.term_in_thy thy t;
walther@60265
   114
        (*this    ^ should raise the exn on unability of re-parsing dts*)
walther@60265
   115
        in itm end\<close> of
walther@60265
   116
      SOME x => x
Walther@60674
   117
    | NONE => (i, v, false, f, I_Model.Syn (UnparseC.term_in_thy thy TermC.empty (*t  ..(t) has not been declared*))))
Walther@60673
   118
  | parsitm thy (itm as (_, _, _, _, I_Model.Par _)) = 
Walther@60673
   119
    raise ERROR ("parsitm (" ^ I_Model.single_to_string (Proof_Context.init_global thy) itm ^
walther@60360
   120
      "): Par should be internal");
walther@59822
   121
walther@59822
   122
(*separate a list to a pair of elements that do NOT satisfy the predicate,
walther@59822
   123
 and of elements that satisfy the predicate, i.e. (false, true)*)
walther@59822
   124
fun filter_sep pred xs =
walther@59822
   125
  let
walther@59822
   126
    fun filt ab [] = ab
walther@59822
   127
      | filt (a, b) (x :: xs) =
walther@59822
   128
        if pred x 
walther@59822
   129
			  then filt (a, b @ [x]) xs 
walther@59822
   130
			  else filt (a @ [x], b) xs
walther@59822
   131
  in filt ([], []) xs end;
walther@59943
   132
fun is_Par (_, _, _, _, I_Model.Par _) = true
walther@59822
   133
  | is_Par _ = false;
walther@59822
   134
walther@59822
   135
fun is_e_ts [] = true
wenzelm@60309
   136
  | is_e_ts [Const (\<^const_name>\<open>Nil\<close>, _)] = true
walther@59822
   137
  | is_e_ts _ = false;
walther@59822
   138
walther@59822
   139
(* WN.9.11.03 copied from fun appl_add *)
Walther@60586
   140
fun appl_add' dI oris model pbt (sel, ct) = 
walther@59822
   141
  let 
Walther@60676
   142
     val ctxt = Know_Store.get_via_last_thy dI |> Proof_Context.init_global;
walther@59822
   143
  in
Walther@60663
   144
    (*/------------ replace by ParseC.term_position ------------------\*)
Walther@60663
   145
    case ParseC.term_opt ctxt ct of
Walther@60663
   146
    (*\------------ replace by ParseC.term_position ------------------/*)
walther@59943
   147
	    NONE => (0, [], false, sel, I_Model.Syn ct)
walther@59822
   148
	  | SOME t =>
Walther@60471
   149
	    (case O_Model.contains ctxt sel oris t of
walther@59822
   150
        ("", ori', all) =>
Walther@60586
   151
          (case I_Model.is_notyet_input ctxt model all ori' pbt of
walther@59822
   152
            ("",itm)  => itm
walther@59962
   153
          | (msg,_) => raise ERROR ("appl_add': " ^ msg))
walther@59822
   154
      | (_, (i, v, _, d, ts), _) =>
walther@59822
   155
        if is_e_ts ts
walther@59943
   156
        then (i, v, false, sel, I_Model.Inc ((d, ts), (TermC.empty, [])))
walther@59943
   157
        else (i, v, false, sel, I_Model.Sup (d, ts)))
walther@59822
   158
   end
walther@59822
   159
Walther@60422
   160
(* generate preliminary itm_ from a string (with field "#Given" etc.) *)
walther@59822
   161
fun eq7 (f, d) (f', (d', _)) = f = f' andalso d = d';
walther@59822
   162
fun fstr2itm_ thy pbt (f, str) =
walther@59822
   163
  let
Walther@60663
   164
    (*/------------ replace by ParseC.term_position ? ------------\*)
Walther@60663
   165
    val topt = ParseC.term_opt (Proof_Context.init_global thy) str
Walther@60663
   166
    (*\------------ replace by ParseC.term_position ? ------------/*)
walther@59822
   167
  in
walther@59822
   168
    case topt of
walther@59943
   169
      NONE => ([], false, f, I_Model.Syn str)
walther@59822
   170
    | SOME ct => 
walther@59822
   171
	    let
Walther@60422
   172
	      val (d, ts) = Input_Descript.split ct
walther@59822
   173
	      val popt = find_first (eq7 (f, d)) pbt
walther@59822
   174
	    in
walther@59822
   175
	      case popt of
walther@59943
   176
	        NONE => ([1](*??*), true(*??*), f, I_Model.Sup (d, ts))
walther@59943
   177
	      | SOME (f, (d, id)) => ([1], true, f, I_Model.Cor ((d, ts), (id, ts))) 
walther@59822
   178
	    end
walther@59822
   179
  end
walther@59822
   180
walther@59822
   181
(*.input into empty PblObj, i.e. empty fmz+origin (unknown example).*)
walther@59822
   182
fun unknown_expl dI pbt selcts =
walther@59822
   183
  let
Walther@60649
   184
    val thy = Know_Store.get_via_last_thy dI
walther@59822
   185
    val its_ = map (fstr2itm_ thy pbt) selcts (*([1],true,"#Given",Cor (...))*)
Walther@60472
   186
    val its = O_Model.add_enumerate its_ 
walther@59822
   187
  in map flattup2 its end
walther@59822
   188
walther@59822
   189
(* WN.11.03 for input_icalhd, ~ specify_additem for Add_Given/_Find/_Relation
walther@59822
   190
   appl_add': generate 1 item 
Walther@60471
   191
   appl_add' . contains: parse, get data from oris (vats, all (elems if list)..)
walther@59822
   192
   appl_add' . is_notyet_input: compare with items in model already input
walther@59822
   193
   insert_ppc': insert this 1 item*)
walther@59822
   194
fun appl_adds dI [] _ pbt selcts = unknown_expl dI pbt selcts
walther@59822
   195
    (*already present itms in model are being overwritten*)
Walther@60586
   196
  | appl_adds _ _ model _ [] = model
Walther@60586
   197
  | appl_adds dI oris model pbt (selct :: ss) =
Walther@60586
   198
    let val itm = appl_add' dI oris model pbt selct;
Walther@60586
   199
    in appl_adds dI oris (I_Model.add itm model) pbt ss end
walther@59822
   200
walther@59943
   201
fun par2fstr (_, _, _, f, I_Model.Par s) = (f, s)
Walther@60676
   202
  | par2fstr itm = raise ERROR ("par2fstr: called with " ^
Walther@60676
   203
    I_Model.single_to_string (ContextC.for_ERROR ()) itm)
Walther@60673
   204
fun itms2fstr _ (_, _, _, f, I_Model.Cor ((d, ts), _)) = (f, Input_Descript.join''' (d, ts))
Walther@60673
   205
  | itms2fstr _ (_, _, _, f, I_Model.Syn str) = (f, str)
Walther@60673
   206
  | itms2fstr _ (_, _, _, f, I_Model.Typ str) = (f, str)
Walther@60673
   207
  | itms2fstr _ (_, _, _, f, I_Model.Inc ((d, ts), _)) = (f, Input_Descript.join''' (d,ts))
Walther@60673
   208
  | itms2fstr _ (_, _, _, f, I_Model.Sup (d, ts)) = (f, Input_Descript.join''' (d, ts))
Walther@60675
   209
  | itms2fstr ctxt (_, _, _, f, I_Model.Mis (d, t)) = (f, UnparseC.term ctxt (d $ t))
Walther@60673
   210
  | itms2fstr ctxt (itm as (_, _, _, _, I_Model.Par _)) = 
Walther@60708
   211
    raise ERROR ("itms2fstr (" ^ I_Model.single_to_string ctxt itm ^ "): Par should be internal");
walther@59822
   212
walther@59822
   213
fun imodel2fstr iitems = 
walther@59822
   214
  let 
walther@59822
   215
    fun xxx is [] = is
walther@59822
   216
	    | xxx is ((Given strs)::iis) = xxx (is @ (map (pair "#Given") strs)) iis
walther@59822
   217
	    | xxx is ((Find strs)::iis) = xxx (is @ (map (pair "#Find") strs)) iis
walther@59822
   218
	    | xxx is ((Relate strs)::iis) = xxx (is @ (map (pair "#Relate") strs)) iis
walther@59822
   219
  in xxx [] iitems end;
walther@59822
   220
walther@59822
   221
(* input a calchead, WN110505 "prep_oris -> (_, ctxt)" not handled properly *)
walther@59822
   222
fun input_icalhd pt (((p, _), hdf, imodel, Pos.Pbl, spec as (dI, pI, mI)) : icalhd) =
walther@59822
   223
    let
walther@59822
   224
		  val (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth) = case Ctree.get_obj I pt p of
walther@59822
   225
		    Ctree.PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'), 
Walther@60676
   226
		      spec = sspec as (sdI, spI, smI), probl, meth, ...}
walther@59822
   227
        => (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth)
walther@59962
   228
      | _ => raise ERROR "input_icalhd: uncovered case of get_obj I pt p"
Walther@60653
   229
      val thy = Know_Store.get_via_last_thy dI
Walther@60673
   230
      val ctxt = Proof_Context.init_global thy
Walther@60653
   231
    in if CAS_Cmd.is_from hdf fmz
Walther@60673
   232
       then the (CAS_Cmd.input (ParseC.term_opt ctxt hdf |> the)) 
Walther@60653
   233
       else
walther@59822
   234
         let val (pos_, pits, mits) = 
walther@59822
   235
	         if dI <> sdI
Walther@60676
   236
	         then let val its = map (parsitm thy) probl;
walther@59822
   237
			            val (its, trms) = filter_sep is_Par its;
Walther@60673
   238
			            val pbt = (#model o Problem.from_store ctxt)
Walther@60653
   239
			              (#2 (References.select_input ospec sspec))
walther@59822
   240
		            in (Pos.Pbl, appl_adds dI oris its pbt  (map par2fstr trms), meth) end 
walther@59822
   241
           else
walther@59822
   242
             if pI <> spI 
walther@59822
   243
	           then if pI = snd3 ospec then (Pos.Pbl, probl, meth) 
walther@59822
   244
                  else
Walther@60673
   245
		                let val pbt = (#model o Problem.from_store ctxt) pI
Walther@60494
   246
			                val dI' = #1 (References.select_input ospec spec)
Walther@60470
   247
			                val oris =
Walther@60470
   248
			                  if pI = #2 ospec then oris 
Walther@60653
   249
				                else O_Model.init thy fmz_ pbt |> #1;
walther@59822
   250
		                in (Pos.Pbl, appl_adds dI' oris probl pbt 
Walther@60673
   251
				              (map (itms2fstr ctxt) probl), meth) end 
walther@59822
   252
             else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)
Walther@60673
   253
	                then let val met = (#model o MethodC.from_store ctxt) mI
walther@59988
   254
		                     val mits = I_Model.complete oris probl meth met
walther@59822
   255
		                   in if foldl and_ (true, map #3 mits)
walther@59822
   256
		                      then (Pos.Pbl, probl, mits) else (Pos.Met, probl, mits) 
walther@59822
   257
		                   end 
Walther@60494
   258
                  else (Pos.Pbl, appl_adds (#1 (References.select_input ospec spec)) oris [(*!!!*)]
Walther@60673
   259
			                  ((#model o Problem.from_store ctxt)
Walther@60557
   260
			                    (#2 (References.select_input ospec spec)))
Walther@60557
   261
			                      (imodel2fstr imodel), meth)
walther@59822
   262
	         val pt = Ctree.update_spec pt p spec;
walther@59822
   263
         in if pos_ = Pos.Pbl
Walther@60557
   264
	          then 
Walther@60557
   265
	            let 
Walther@60673
   266
	              val {where_rls, where_,...} = Problem.from_store ctxt
Walther@60557
   267
	                (#2 (References.select_input ospec spec))
Walther@60673
   268
		            val (_, where_) = Pre_Conds.check ctxt where_rls where_ pits 0
Walther@60557
   269
	            in (Ctree.update_pbl pt p pits,
Walther@60586
   270
		                 (SpecificationC.is_complete' pits where_ spec, Pos.Pbl, hdf', pits, where_, spec)) 
Walther@60557
   271
              end
Walther@60557
   272
	          else 
Walther@60557
   273
	            let 
Walther@60673
   274
	              val {where_rls,where_,...} = MethodC.from_store ctxt 
Walther@60557
   275
	                (#3 (References.select_input ospec spec))
Walther@60673
   276
		            val (_, where_) = Pre_Conds.check ctxt where_rls where_ mits 0
Walther@60557
   277
	            in (Ctree.update_met pt p mits,
Walther@60586
   278
		                  (SpecificationC.is_complete' mits where_ spec, Pos.Met, hdf', mits, where_, spec))
Walther@60557
   279
              end
walther@59822
   280
         end 
walther@59822
   281
    end
walther@59962
   282
  | input_icalhd _ (_, _, _, _(*Met*), _) = raise ERROR "input_icalhd Met not impl."
walther@59822
   283
walther@60132
   284
(**)end (**)