src/Tools/isac/calcelems.sml
changeset 55372 32b7d689e299
parent 55364 c531d9770184
child 55373 4f3f530f3cf6
     1.1 --- a/src/Tools/isac/calcelems.sml	Tue Jan 28 11:09:45 2014 +0100
     1.2 +++ b/src/Tools/isac/calcelems.sml	Fri Jan 31 17:50:50 2014 +0100
     1.3 @@ -845,7 +845,54 @@
     1.4        then Ptyp (k, y, merge_ptyps (ps, ps')) :: merge_ptyps (xs, ys)
     1.5        else x' :: merge_ptyps (xs, xs');
     1.6  
     1.7 -(* types for methods *)
     1.8 +
     1.9 +(* data for methods stored in 'methods'-database*)
    1.10 +type met = 
    1.11 +     {guh        : guh,        (*unique within this isac-knowledge           *)
    1.12 +      mathauthors: string list,(*copyright                                   *)
    1.13 +      init       : pblID,      (*WN060721 introduced mistakenly--TODO.REMOVE!*)
    1.14 +      rew_ord'   : rew_ord',   (*for rules in Detail
    1.15 +			                           TODO.WN0509 store fun itself, see 'type pbt'*)
    1.16 +      erls       : rls,        (*the eval_rls for cond. in rules FIXME "rls'
    1.17 +				                         instead erls in "fun prep_met"              *)
    1.18 +      srls       : rls,        (*for evaluating list expressions in scr      *)
    1.19 +      prls       : rls,        (*for evaluating predicates in modelpattern   *)
    1.20 +      crls       : rls,        (*for check_elementwise, ie. formulae in calc.*)
    1.21 +      nrls       : rls,        (*canonical simplifier specific for this met  *)
    1.22 +      errpats    : errpat list,(*error patterns expected in this method      *)
    1.23 +      calc       : calc list,  (*Theory_Data in fun prep_met                 *)
    1.24 +      (*branch   : TransitiveB set in append_problem at generation ob pblobj
    1.25 +          FIXXXME.0308: set branch from met in Apply_Method ?                *)
    1.26 +      ppc        : pat list,   (*.items in given, find, relate;
    1.27 +	      items (in "#Find") which need not occur in the arg-list of a SubProblem
    1.28 +        are 'copy-named' with an identifier "*'.'".
    1.29 +        copy-named items are 'generating' if they are NOT "*'''" ?WN120516??
    1.30 +        see ME/calchead.sml 'fun is_copy_named'.                              *)
    1.31 +      pre        : term list,  (*preconditions in where                       *)
    1.32 +      scr        : scr         (*prep_met gets progam or string "empty_script"*)
    1.33 +	   };
    1.34 +val e_met = {guh="met_empty",mathauthors=[],init=e_metID,
    1.35 +	     rew_ord' = "e_rew_ord'": rew_ord',
    1.36 +	      erls = e_rls, srls = e_rls, prls = e_rls,
    1.37 +	      calc = [], crls = e_rls, errpats = [], nrls= e_rls,
    1.38 +	      ppc = []: (string * (term * term)) list,
    1.39 +	      pre = []: term list,
    1.40 +	      scr = EmptyScr: scr}:met;
    1.41 +
    1.42 +
    1.43 +(** problem-types stored in format for usage in specify  **)
    1.44 +(*25.8.01 ----
    1.45 +val pbltypes = Unsynchronized.ref ([(e_pblID,[])]:(pblID * ((string * (* field "#Given",..*)
    1.46 +			     (term *   (* description      *)
    1.47 +			      term))    (* id | struct-var  *)
    1.48 +			     list)
    1.49 +		    ) list);*)
    1.50 +
    1.51 +val e_Mets = Ptyp ("e_metID",[e_met],[]);
    1.52 +
    1.53 +
    1.54 +type mets = (met ptyp) list;
    1.55 +val mets = Unsynchronized.ref ([e_Mets]:mets);
    1.56  
    1.57  
    1.58  (*