wneuper/isa: src/Tools/isac/Specify/p-spec.sml@0d22a6bf1fc6

     1 (* Title:  Specify/input-calchead.sml

     2    Author: Walther Neuper

     3    (c) due to copyright terms

     5 This will be dropped at switch to Isabelle/PIDE .

     6 *)

     8 signature PRESENTATION_SPECIFICATION =

     9 sig

    10   type record

    11 (*/------- rename -------\*)

    12   datatype iitem =

    13       Find of TermC.as_string list

    14     | Given of TermC.as_string list

    15     | Relate of TermC.as_string list

    16   type imodel = iitem list

    17   type icalhd = Pos.pos' * TermC.as_string * imodel * Pos.pos_ * References.T

    18   val empty: icalhd

    19   val input_icalhd : Ctree.ctree -> icalhd -> Ctree.ctree * SpecificationC.T

    20 \<^isac_test>\<open>

    21   val appl_add': ThyC.id -> O_Model.T -> I_Model.T -> Model_Pattern.T ->

    22     string * TermC.as_string -> I_Model.single

    23   val appl_adds: ThyC.id -> O_Model.T -> I_Model.T -> Model_Pattern.T ->

    24     (string * TermC.as_string) list -> I_Model.T

    25   val eq7: ''a * ''b -> ''a * (''b * 'c) -> bool

    26   val filter_sep: ('a -> bool) -> 'a list -> 'a list * 'a list

    27   val fstr2itm_: theory -> (''a * (term * term)) list -> ''a * string ->

    28     int list * bool * ''a * I_Model.feedback (*I_Model.single'*)

    29   val imodel2fstr: iitem list -> (string * TermC.as_string) list

    30   val is_Par: 'a * 'b * 'c * 'd * I_Model.feedback -> bool (*I_Model.T?*)

    31   val is_e_ts: term list -> bool

    32   val itms2fstr: I_Model.single -> string * string

    33   val par2fstr: I_Model.single -> string * TermC.as_string

    34   val parsitm: theory -> I_Model.single -> I_Model.single

    35   val unknown_expl: ThyC.id -> (''a * (term * term)) list -> (*Model_Pattern.T?*)

    36     (''a * string) list ->

    37       (int * int list * bool * ''a * Model_Def.i_model_feedback) list (*I_Model.T?*)

    38 \<close>

    39 (*\------- rename -------/*)

    40 end

    42 (**)

    43 structure P_Spec(**): PRESENTATION_SPECIFICATION(**) =

    44 struct

    45 (**)

    47   type record = {thy_id: ThyC.id, pbl_id: Problem.id,           (* headline of Problem *)

    48     givens: TermC.as_string list, wheres: TermC.as_string list, (* Model.T             *)

    49       find: TermC.as_string, relates: TermC.as_string list,

    50     rthy_id: ThyC.id, rpbl_id: Problem.id, rmet_id: MethodC.id}  (* References.T        *)

    52 fun flattup2 (a, (b ,c, d, e)) = (a, b, c, d, e)

    54 (** handle an input P_Specific'action **)

    56 datatype iitem =

    57   Given of TermC.as_string list

    58 (*Where is still not input*)

    59 | Find  of TermC.as_string list

    60 | Relate  of TermC.as_string list

    62 type imodel = iitem list

    64 type icalhd =

    65   Pos.pos' *         (* the position in Ctree              *)

    66   TermC.as_string *  (* the headline shown on Calc.T       *)

    67   imodel *           (* the model                          *)

    68   Pos.pos_ *         (* model belongs to Problem or MethodC *)

    69   References.T;      (* into Know_Store                    *)

    70 val empty = (Pos.e_pos', "", [Given [""]], Pos.Pbl, References.empty)

    72 (* re-parse itms with a new thy and prepare for checking with ori list *)

    73 fun parsitm dI (itm as (i, v, _, f, I_Model.Cor ((d, ts), _))) =

    74     (case \<^try>\<open>

    75         let val t = Input_Descript.join (d, ts)

    76           val _ = (UnparseC.term_in_thy dI t)

    77           (*t his ^^^^^^^^^^^^ should raise the exn on unability of re-parsing dts *)

    78         in itm end\<close> of

    79       SOME x => x

    80     | NONE => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t  ..(t) has not been declared*))))

    81   | parsitm dI (i, v, b, f, I_Model.Syn str) =

    82     (case \<^try>\<open>

    83         let val _ = TermC.parseNEW'' dI str

    84         in (i, v, b ,f, I_Model.Par str) end\<close> of

    85       SOME x => x

    86     | NONE => (i, v, b, f, I_Model.Syn str))

    87   | parsitm dI (i, v, b, f, I_Model.Typ str) =

    88     (case \<^try>\<open>

    89         let val _ = TermC.parseNEW'' dI str

    90          in (i, v, b, f, I_Model.Par str) end\<close> of

    91       SOME x => x

    92     | NONE => (i, v, b, f, I_Model.Syn str))

    93   | parsitm dI (itm as (i, v, _, f, I_Model.Inc ((d, ts), _))) =

    94     (case \<^try>\<open>

    95         let val t = Input_Descript.join (d,ts);

    96 	        val _ = UnparseC.term_in_thy dI t;

    97         (*this    ^ should raise the exn on unability of re-parsing dts*)

    98         in itm end\<close> of

    99       SOME x => x

   100     | NONE => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t  ..(t) has not been declared*))))

   101   | parsitm dI (itm as (i, v, _, f, I_Model.Sup (d, ts))) =

   102     (case \<^try>\<open>

   103         let val t = Input_Descript.join (d,ts);

   104 	        val _ = UnparseC.term_in_thy dI t;

   105         (*this    ^ should raise the exn on unability of re-parsing dts*)

   106         in itm end\<close> of

   107       SOME x => x

   108     | NONE => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t  ..(t) has not been declared*))))

   109   | parsitm dI (itm as (i, v, _, f, I_Model.Mis (d, t'))) =

   110     (case \<^try>\<open>

   111         let val t = d $ t';

   112 	        val _ = UnparseC.term_in_thy dI t;

   113         (*this    ^ should raise the exn on unability of re-parsing dts*)

   114         in itm end\<close> of

   115       SOME x => x

   116     | NONE => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t  ..(t) has not been declared*))))

   117   | parsitm dI (itm as (_, _, _, _, I_Model.Par _)) =

   118     raise ERROR ("parsitm (" ^ I_Model.single_to_string (ThyC.to_ctxt dI) itm ^ "): Par should be internal");

   120 (*separate a list to a pair of elements that do NOT satisfy the predicate,

   121  and of elements that satisfy the predicate, i.e. (false, true)*)

   122 fun filter_sep pred xs =

   123   let

   124     fun filt ab [] = ab

   125       | filt (a, b) (x :: xs) =

   126         if pred x

   127 			  then filt (a, b @ [x]) xs

   128 			  else filt (a @ [x], b) xs

   129   in filt ([], []) xs end;

   130 fun is_Par (_, _, _, _, I_Model.Par _) = true

   131   | is_Par _ = false;

   133 fun is_e_ts [] = true

   134   | is_e_ts [Const (\<^const_name>\<open>Nil\<close>, _)] = true

   135   | is_e_ts _ = false;

   137 (* WN.9.11.03 copied from fun appl_add *)

   138 fun appl_add' dI oris ppc pbt (sel, ct) =

   139   let

   140      val ctxt = ThyC.get_theory dI |> ThyC.to_ctxt;

   141   in

   142     case TermC.parseNEW ctxt ct of

   143 	    NONE => (0, [], false, sel, I_Model.Syn ct)

   144 	  | SOME t =>

   145 	    (case O_Model.is_known ctxt sel oris t of

   146         ("", ori', all) =>

   147           (case I_Model.is_notyet_input ctxt ppc all ori' pbt of

   148             ("",itm)  => itm

   149           | (msg,_) => raise ERROR ("appl_add': " ^ msg))

   150       | (_, (i, v, _, d, ts), _) =>

   151         if is_e_ts ts

   152         then (i, v, false, sel, I_Model.Inc ((d, ts), (TermC.empty, [])))

   153         else (i, v, false, sel, I_Model.Sup (d, ts)))

   154    end

   156 (* generate preliminary itm_ from a strin (with field "#Given" etc.) *)

   157 fun eq7 (f, d) (f', (d', _)) = f = f' andalso d = d';

   158 fun fstr2itm_ thy pbt (f, str) =

   159   let

   160     val topt = TermC.parseNEW (ThyC.to_ctxt thy) str

   161   in

   162     case topt of

   163       NONE => ([], false, f, I_Model.Syn str)

   164     | SOME ct =>

   165 	    let

   166 	      val (d, ts) = (Input_Descript.split) ct

   167 	      val popt = find_first (eq7 (f, d)) pbt

   168 	    in

   169 	      case popt of

   170 	        NONE => ([1](*??*), true(*??*), f, I_Model.Sup (d, ts))

   171 	      | SOME (f, (d, id)) => ([1], true, f, I_Model.Cor ((d, ts), (id, ts)))

   172 	    end

   173   end

   175 (*.input into empty PblObj, i.e. empty fmz+origin (unknown example).*)

   176 fun unknown_expl dI pbt selcts =

   177   let

   178     val thy = ThyC.get_theory dI

   179     val its_ = map (fstr2itm_ thy pbt) selcts (*([1],true,"#Given",Cor (...))*)

   180     val its = O_Model.add_id its_

   181   in map flattup2 its end

   183 (* WN.11.03 for input_icalhd, ~ specify_additem for Add_Given/_Find/_Relation

   184    appl_add': generate 1 item

   185    appl_add' . is_known: parse, get data from oris (vats, all (elems if list)..)

   186    appl_add' . is_notyet_input: compare with items in model already input

   187    insert_ppc': insert this 1 item*)

   188 fun appl_adds dI [] _ pbt selcts = unknown_expl dI pbt selcts

   189     (*already present itms in model are being overwritten*)

   190   | appl_adds _ _ ppc _ [] = ppc

   191   | appl_adds dI oris ppc pbt (selct :: ss) =

   192     let val itm = appl_add' dI oris ppc pbt selct;

   193     in appl_adds dI oris (I_Model.add itm ppc) pbt ss end

   195 fun par2fstr (_, _, _, f, I_Model.Par s) = (f, s)

   196   | par2fstr itm = raise ERROR ("par2fstr: called with " ^ I_Model.single_to_string (ThyC.id_to_ctxt "Isac_Knowledge") itm)

   197 fun itms2fstr (_, _, _, f, I_Model.Cor ((d, ts), _)) = (f, Input_Descript.join''' (d, ts))

   198   | itms2fstr (_, _, _, f, I_Model.Syn str) = (f, str)

   199   | itms2fstr (_, _, _, f, I_Model.Typ str) = (f, str)

   200   | itms2fstr (_, _, _, f, I_Model.Inc ((d, ts), _)) = (f, Input_Descript.join''' (d,ts))

   201   | itms2fstr (_, _, _, f, I_Model.Sup (d, ts)) = (f, Input_Descript.join''' (d, ts))

   202   | itms2fstr (_, _, _, f, I_Model.Mis (d, t)) = (f, UnparseC.term (d $ t))

   203   | itms2fstr (itm as (_, _, _, _, I_Model.Par _)) =

   204     raise ERROR ("parsitm (" ^ I_Model.single_to_string (ThyC.id_to_ctxt "Isac_Knowledge") itm ^ "): Par should be internal");

   206 fun imodel2fstr iitems =

   207   let

   208     fun xxx is [] = is

   209 	    | xxx is ((Given strs)::iis) = xxx (is @ (map (pair "#Given") strs)) iis

   210 	    | xxx is ((Find strs)::iis) = xxx (is @ (map (pair "#Find") strs)) iis

   211 	    | xxx is ((Relate strs)::iis) = xxx (is @ (map (pair "#Relate") strs)) iis

   212   in xxx [] iitems end;

   214 (* input a calchead, WN110505 "prep_oris -> (_, ctxt)" not handled properly *)

   215 fun input_icalhd pt (((p, _), hdf, imodel, Pos.Pbl, spec as (dI, pI, mI)) : icalhd) =

   216     let

   217 		  val (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth) = case Ctree.get_obj I pt p of

   218 		    Ctree.PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'),

   219 		      spec = sspec as (sdI, spI, smI), probl, meth, ...}

   220         => (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth)

   221       | _ => raise ERROR "input_icalhd: uncovered case of get_obj I pt p"

   222     in if CAS_Cmd.is_from hdf fmz then the (CAS_Cmd.input (TermC.str2term hdf))

   223        else        (*hacked WN0602 ~~~            ~~~~~~~~~,   ..dropped !*)

   224          let val (pos_, pits, mits) =

   225 	         if dI <> sdI

   226 	         then let val its = map (parsitm (ThyC.get_theory dI)) probl;

   227 			            val (its, trms) = filter_sep is_Par its;

   228 			            val pbt = (#ppc o Problem.from_store) (#2 (References.select ospec sspec))

   229 		            in (Pos.Pbl, appl_adds dI oris its pbt  (map par2fstr trms), meth) end

   230            else

   231              if pI <> spI

   232 	           then if pI = snd3 ospec then (Pos.Pbl, probl, meth)

   233                   else

   234 		                let val pbt = (#ppc o Problem.from_store) pI

   235 			                val dI' = #1 (References.select ospec spec)

   236 			                val oris = if pI = #2 ospec then oris

   237 				                         else O_Model.init fmz_(ThyC.get_theory"Isac_Knowledge") pbt(* |> #1*);

   238 		                in (Pos.Pbl, appl_adds dI' oris probl pbt

   239 				              (map itms2fstr probl), meth) end

   240              else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)

   241 	                then let val met = (#ppc o MethodC.from_store) mI

   242 		                     val mits = I_Model.complete oris probl meth met

   243 		                   in if foldl and_ (true, map #3 mits)

   244 		                      then (Pos.Pbl, probl, mits) else (Pos.Met, probl, mits)

   245 		                   end

   246                   else (Pos.Pbl, appl_adds (#1 (References.select ospec spec)) oris [(*!!!*)]

   247 			                  ((#ppc o Problem.from_store) (#2 (References.select ospec spec)))

   248 			                  (imodel2fstr imodel), meth)

   249 	         val pt = Ctree.update_spec pt p spec;

   250          in if pos_ = Pos.Pbl

   251 	          then let val {prls,where_,...} = Problem.from_store (#2 (References.select ospec spec))

   252 		               val (_, pre) = Pre_Conds.check prls where_ pits 0

   253 	               in (Ctree.update_pbl pt p pits,

   254 		                 (SpecificationC.complete pits pre spec, Pos.Pbl, hdf', pits, pre, spec): SpecificationC.T)

   255                  end

   256 	           else let val {prls,pre,...} = MethodC.from_store (#3 (References.select ospec spec))

   257 		                val (_, pre) = Pre_Conds.check prls pre mits 0

   258 	                in (Ctree.update_met pt p mits,

   259 		                  (SpecificationC.complete mits pre spec, Pos.Met, hdf', mits, pre, spec) : SpecificationC.T)

   260                   end

   261          end

   262     end

   263   | input_icalhd _ (_, _, _, _(*Met*), _) = raise ERROR "input_icalhd Met not impl."

   265 (**)end (**)

author	wneuper <walther.neuper@jku.at>
	Tue, 20 Jul 2021 14:37:56 +0200
changeset 60339	0d22a6bf1fc6
parent 60309	70a1d102660d
child 60340	0ee698b0a703
permissions	-rw-r--r--