author: Walther Neuper

    author: Walther Neuper

    (c) due to copyright terms

    (c) due to copyright terms

 use"ME/mstools.sml" (*re-evaluate sml/ from scratch!*);

 use"ME/mstools.sml" (*re-evaluate sml/ from scratch!*);

 use"mstools.sml";

 use"mstools.sml";

 *)

 *)

 signature SPECIFY_TOOLS =

 signature SPECIFY_TOOLS =

   sig

   sig

     type envv

     type envv

         | Superfl of string

         | Superfl of string

         | SyntaxE of string

         | SyntaxE of string

         | TypeE of string

         | TypeE of string

     val item2str : item -> string

     val item2str : item -> string

     type itm

     type itm

     datatype

     datatype

       itm_ =

       itm_ =

         | Par of cterm'

         | Par of cterm'

         | Syn of cterm'

         | Syn of cterm'

         | Typ of cterm'

         | Typ of cterm'

     val itm_2str : itm_ -> string

     val itm_2str : itm_ -> string

     type 'a ppc

     type 'a ppc

     val ppc2str :

     val ppc2str :

        {Find: string list, With: string list, Given: string list,

        {Find: string list, With: string list, Given: string list,

          Where: string list, Relate: string list} -> string

          Where: string list, Relate: string list} -> string

     datatype

     datatype

           Matches of pblID * item ppc

           Matches of pblID * item ppc

         | NoMatch of pblID * item ppc

         | NoMatch of pblID * item ppc

     val match2str : match -> string

     val match2str : match -> string

     datatype

     datatype

       match_ =

       match_ =

         | NoMatch_

         | NoMatch_

     val matchs2str : match list -> string

     val matchs2str : match list -> string

     type ori

     type ori

     val ori2str : ori -> string

     val ori2str : ori -> string

     val oris2str : ori list -> string

     val oris2str : ori list -> string

     type preori

     type preori

     val preori2str : preori -> string

     val preori2str : preori -> string

     val preoris2str : preori list -> string

     val preoris2str : preori list -> string

     type penv

     type penv

     type vats

     type vats

     (*----------------------------------------------------------------------*)

     (*----------------------------------------------------------------------*)

     val check_preconds :

     val check_preconds :

        'a ->

        'a ->

        rls ->

        rls ->

     val check_preconds' :

     val check_preconds' :

        rls ->

        rls ->

    (* val cnt : itm list -> int -> int * int *)

    (* val cnt : itm list -> int -> int * int *)

     val de_item : item -> cterm'

     val de_item : item -> cterm'

     val e_itm : itm

     val e_itm : itm

     val e_ori : ori

     val e_ori : ori

     val e_ori_ : ori

     val e_ori_ : ori

     val empty_ppc : item ppc

     val empty_ppc : item ppc

    (* val empty_ppc_ct' : cterm' ppc *)

    (* val empty_ppc_ct' : cterm' ppc *)

    (*val head_precond :

    (*val head_precond :

        domID * pblID * 'a ->

        domID * pblID * 'a ->

        rls ->

        rls ->

    (* val init_item : string -> item *)

    (* val init_item : string -> item *)

    (* val is_matches : match -> bool *)

    (* val is_matches : match -> bool *)

    (* val is_matches_ : match_ -> bool *)

    (* val is_matches_ : match_ -> bool *)

    (* val item_ppc :

    (* val item_ppc :

        string ppc -> item ppc  *)

        string ppc -> item ppc  *)

     val itemppc2str : item ppc -> string

     val itemppc2str : item ppc -> string

    (* val matches_pblID : match -> pblID *)

    (* val matches_pblID : match -> pblID *)

     val max2 : ('a * int) list -> 'a * int

     val max2 : ('a * int) list -> 'a * int

     val max_vt : itm list -> int

     val max_vt : itm list -> int

    (* val pblID_of_match : match -> pblID *)

    (* val pblID_of_match : match -> pblID *)

     val refined : match list -> pblID

     val refined : match list -> pblID

     val refined_ :

     val refined_ :

   (*  val refined_IDitms :

   (*  val refined_IDitms :

     val untouched : itm list -> bool

     val untouched : itm list -> bool

     val upd :

     val upd :

     val upd_envv :

     val upd_envv :

        envv ->

        envv ->

        vats ->

        vats ->

     val upd_penv :

     val upd_penv :

    (* val upds_envv :

    (* val upds_envv :

        envv ->

        envv ->

        envv                         *)

        envv                         *)

     val vts_cnt : int list -> itm list -> (int * int) list

     val vts_cnt : int list -> itm list -> (int * int) list

     val vts_in : itm list -> int list

     val vts_in : itm list -> int list

   end

   end

 (*----------------------------------------------------------*)

 (*----------------------------------------------------------*)

 structure SpecifyTools : SPECIFY_TOOLS =

 structure SpecifyTools : SPECIFY_TOOLS =

 struct

 struct

 (*----------------------------------------------------------*)

 (*----------------------------------------------------------*)

 (*.take list-term apart w.r.t. handling elementwise input.*)

 (*.take list-term apart w.r.t. handling elementwise input.*)

 fun take_apart t =

 fun take_apart t =

     let val elems = isalist2list t

     let val elems = isalist2list t

     in map ((list2isalist (type_of (hd elems))) o single) elems end;

     in map ((list2isalist (type_of (hd elems))) o single) elems end;

     else (hd ts);

     else (hd ts);

 (*.revert split_.

 (*.revert split_.

  WN050903 we do NOT know which is from subtheory, description or term;

  WN050903 we do NOT know which is from subtheory, description or term;

  typecheck thus may lead to TYPE-error 'unknown constant';

  typecheck thus may lead to TYPE-error 'unknown constant';

  solution: typecheck with Isac.thy; i.e. arg 'thy' superfluous*)

  solution: typecheck with Isac.thy; i.e. arg 'thy' superfluous*)

 	     (*comp_dts:FIXXME stay with term for efficiency !!!*)

 	     (*comp_dts:FIXXME stay with term for efficiency !!!*)

 	     (if is_reall_dsc d then (d $ e_listReal)

 	     (if is_reall_dsc d then (d $ e_listReal)

 	      else if is_booll_dsc d then (d $ e_listBool)

 	      else if is_booll_dsc d then (d $ e_listBool)

 	      else d)

 	      else d)

   | comp_dts thy (d,ts) =

   | comp_dts thy (d,ts) =

 	      (*comp_dts:FIXXME stay with term for efficiency !!*)

 	      (*comp_dts:FIXXME stay with term for efficiency !!*)

 	      (d $ (comp_ts (d, ts)))

 	      (d $ (comp_ts (d, ts)))

        handle _ => raise error ("comp_dts: "^(term2str d)^

        handle _ => raise error ("comp_dts: "^(term2str d)^

 (*25.8.03*)

 (*25.8.03*)

 fun comp_dts' (d,[]) = 

 fun comp_dts' (d,[]) = 

     if is_reall_dsc d then (d $ e_listReal)

     if is_reall_dsc d then (d $ e_listReal)

     else if is_booll_dsc d then (d $ e_listBool)

     else if is_booll_dsc d then (d $ e_listBool)

     else d

     else d

            but [#0, epsilon] only outcommented for eventual reconsideration  

            but [#0, epsilon] only outcommented for eventual reconsideration  

 *)

 *)

 type penv = (term          (*err_*)

 type penv = (term          (*err_*)

 	     * (term list) (*[#0, epsilon] 9.5.03 outcommented*)

 	     * (term list) (*[#0, epsilon] 9.5.03 outcommented*)

 	     ) list;

 	     ) list;

 (*

 (*

   9.5.03: still unused, but left for eventual future development*)

   9.5.03: still unused, but left for eventual future development*)

 type envv = (int * penv) list; (*over variants*)

 type envv = (int * penv) list; (*over variants*)

 (*. get the constant value from a penv .*)

 (*. get the constant value from a penv .*)

 fun getval (id, values) = 

 fun getval (id, values) = 

     case values of

     case values of

 	[] => raise error ("penv_value: no values in '"^

 	[] => raise error ("penv_value: no values in '"^

       | [v] => (id, v)

       | [v] => (id, v)

       | (v1::v2::_) => (case v1 of 

       | (v1::v2::_) => (case v1 of 

 			     Const ("Script.Arbfix",_) => (id, v2)

 			     Const ("Script.Arbfix",_) => (id, v2)

 			   | _ => (id, v1));

 			   | _ => (id, v1));

 (*

 (*

   | mk_e (Typ _) = [] 

   | mk_e (Typ _) = [] 

   | mk_e (Inc (_, iv)) = [getval iv]

   | mk_e (Inc (_, iv)) = [getval iv]

   | mk_e (Sup _) = []

   | mk_e (Sup _) = []

   | mk_e (Mis _) = [];

   | mk_e (Mis _) = [];

 fun mk_en vt ((i,vts,b,f,itm_):itm) =

 fun mk_en vt ((i,vts,b,f,itm_):itm) =

 (*. extract the environment from an item list; 

 (*. extract the environment from an item list; 

     takes the variant with most items .*)

     takes the variant with most items .*)

 fun mk_env itms = 

 fun mk_env itms = 

     let val vt = max_vt itms

     let val vt = max_vt itms

     in (flat o (map (mk_en vt))) itms end;

     in (flat o (map (mk_en vt))) itms end;

 val preoris2str = (strs2str' o (map (linefeed o preori2str)));

 val preoris2str = (strs2str' o (map (linefeed o preori2str)));

 (*. given the input value (from split_dts)

 (*. given the input value (from split_dts)

     make the value in a problem-env according to description-type .*)

     make the value in a problem-env according to description-type .*)

 (*28.8.01: .nam and .una impl. properly, others copied .. TODO*)

 (*28.8.01: .nam and .una impl. properly, others copied .. TODO*)

     if is_list v 

     if is_list v 

     then [v]         (*eg. [r=Arbfix]*)

     then [v]         (*eg. [r=Arbfix]*)

     else (case v of  (*eg. eps=#0*)

     else (case v of  (*eg. eps=#0*)

 	      (Const ("op =",_) $ l $ r) => [r,l]

 	      (Const ("op =",_) $ l $ r) => [r,l]

 	    | _ => raise error ("pbl_ids Tools.nam: no equality "

 	    | _ => raise error ("pbl_ids Tools.nam: no equality "

 (*

 (*

 val t as t1 $ t2 = str2term "antiDerivativeName M_b";

 val t as t1 $ t2 = str2term "antiDerivativeName M_b";

   val t = (term_of o the o (parse thy)) "fixedValues [r=Arbfix]";

   val t = (term_of o the o (parse thy)) "fixedValues [r=Arbfix]";

   val (d,argl) = strip_comb t;

   val (d,argl) = strip_comb t;

   is_dsc d;                      (*see split_dts*)

   is_dsc d;                      (*see split_dts*)

   dest_list (d,argl);

   dest_list (d,argl);

   val (_ $ v) = t;

   val (_ $ v) = t;

   is_list v;

   is_list v;

 [Const ("List.list.Cons","[bool, bool List.list] => bool List.list") $

 [Const ("List.list.Cons","[bool, bool List.list] => bool List.list") $

        (Const # $ Free # $ Const (#,#)) $ Const ("List.list.Nil","bool List..

        (Const # $ Free # $ Const (#,#)) $ Const ("List.list.Nil","bool List..

   val (dsc,vl) = (split_dts o term_of o the o (parse thy)) "solveFor x";

   val (dsc,vl) = (split_dts o term_of o the o (parse thy)) "solveFor x";

 val dsc = Const ("Descript.solveFor","RealDef.real => Tools.una") : term

 val dsc = Const ("Descript.solveFor","RealDef.real => Tools.una") : term

 val vl = Free ("x","RealDef.real") : term 

 val vl = Free ("x","RealDef.real") : term 

   val (dsc,id) = (split_did o term_of o the o (parse thy)) "solveFor v_";

   val (dsc,id) = (split_did o term_of o the o (parse thy)) "solveFor v_";

 val it = [Free ("x","RealDef.real")] : term list

 val it = [Free ("x","RealDef.real")] : term list

   val (dsc,vl) = (split_dts o term_of o the o(parse thy))

   val (dsc,vl) = (split_dts o term_of o the o(parse thy))

 		       "errorBound (eps=#0)";

 		       "errorBound (eps=#0)";

   val (dsc,id) = (split_did o term_of o the o(parse thy)) "errorBound err_";

   val (dsc,id) = (split_did o term_of o the o(parse thy)) "errorBound err_";

 val it = [Free ("#0","RealDef.real"),Free ("eps","RealDef.real")] : term list     *)

 val it = [Free ("#0","RealDef.real"),Free ("eps","RealDef.real")] : term list     *)

 (*. given an already input itm, ((14.9.01: no difference to pbl_ids jet!!))

 (*. given an already input itm, ((14.9.01: no difference to pbl_ids jet!!))

     make the value in a problem-env according to description-type .*)

     make the value in a problem-env according to description-type .*)

 (*28.8.01: .nam and .una impl. properly, others copied .. TODO*)

 (*28.8.01: .nam and .una impl. properly, others copied .. TODO*)

     (case vs of 

     (case vs of 

 	 [] => raise error ("pbl_ids' Tools.nam called with []")

 	 [] => raise error ("pbl_ids' Tools.nam called with []")

        | [t] => (case t of  (*eg. eps=#0*)

        | [t] => (case t of  (*eg. eps=#0*)

 		     (Const ("op =",_) $ l $ r) => [r,l]

 		     (Const ("op =",_) $ l $ r) => [r,l]

 		   | _ => raise error ("pbl_ids' Tools.nam: no equality "

 		   | _ => raise error ("pbl_ids' Tools.nam: no equality "

        | vs' => vs (*14.9.01: ???TODO *))

        | vs' => vs (*14.9.01: ???TODO *))

   | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.una",_)]))) vs = vs

   | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.una",_)]))) vs = vs

   | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.unl",_)]))) vs = vs

   | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.unl",_)]))) vs = vs

   | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.str",_)]))) vs = vs

   | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.str",_)]))) vs = vs

   | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.toreal",_)]))) vs = vs 

   | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.toreal",_)]))) vs = vs 

 fun pbl_ids' thy d vs = [comp_ts (d, vs)];

 fun pbl_ids' thy d vs = [comp_ts (d, vs)];

 (*14.9.01: not used after putting values for penv into itm_

 (*14.9.01: not used after putting values for penv into itm_

   WN.5.5.03: used in upd .. upd_envv*)

   WN.5.5.03: used in upd .. upd_envv*)

 (writeln"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";

 (writeln"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";

  writeln"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";

  writeln"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";

  writeln"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";

  writeln"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";

 );

 );

 (* 

 (* 

   val penv = [];

   val penv = [];

   val (dsc,vl) = (split_did o term_of o the o (parse thy)) "solveFor x";

   val (dsc,vl) = (split_did o term_of o the o (parse thy)) "solveFor x";

   val (dsc,id) = (split_did o term_of o the o (parse thy)) "solveFor v_";

   val (dsc,id) = (split_did o term_of o the o (parse thy)) "solveFor v_";

 *)

 *)

 (*WN.9.5.03: not reconsidered; looks strange !!!*)

 (*WN.9.5.03: not reconsidered; looks strange !!!*)

 fun upd thy envv dsc (id, vl) i =

 fun upd thy envv dsc (id, vl) i =

     let val penv = case assoc (envv, i) of

     let val penv = case assoc (envv, i) of

         val penv' = upd_penv thy penv dsc (id, vl);

         val penv' = upd_penv thy penv dsc (id, vl);

     in (i, penv') end;

     in (i, penv') end;

 (*

 (*

   val i = 2;

   val i = 2;

   val envv = [(1,[]:penv),(2,[]:penv),(3,[]:penv)]:envv;

   val envv = [(1,[]:penv),(2,[]:penv),(3,[]:penv)]:envv;

     let val vats = if length vats = 0 

     let val vats = if length vats = 0 

 		   then (*unknown id to _all_ variants*)

 		   then (*unknown id to _all_ variants*)

 		       if length envv = 0 then [1]

 		       if length envv = 0 then [1]

 		       else (intsto o length) envv 

 		       else (intsto o length) envv 

 		   else vats

 		   else vats

 	val envs_notin_vat = filter_out (isin vats) envv;

 	val envs_notin_vat = filter_out (isin vats) envv;

     in ((map (upd thy envv dsc (id, vl)) vats) @ envs_notin_vat):envv end;

     in ((map (upd thy envv dsc (id, vl)) vats) @ envs_notin_vat):envv end;

 (*

 (*

   val envv = [(1,[]:penv),(2,[]:penv),(3,[]:penv)]:envv;

   val envv = [(1,[]:penv),(2,[]:penv),(3,[]:penv)]:envv;

   | TypeE   of string (**)

   | TypeE   of string (**)

   | False   of cterm' (*WN050618 notexistent in itm_: only used in Where*)

   | False   of cterm' (*WN050618 notexistent in itm_: only used in Where*)

   | Incompl of cterm' (**)

   | Incompl of cterm' (**)

   | Superfl of string (**)

   | Superfl of string (**)

   | Missing of cterm';

   | Missing of cterm';

 (*make string for error-msgs*)

 (*make string for error-msgs*)

     "("^(string_of_int i)^" ,"^(ints2str' is)^" ,"^(bool2str b)^" ,"^

     "("^(string_of_int i)^" ,"^(ints2str' is)^" ,"^(bool2str b)^" ,"^

 fun init_item str = SyntaxE str;

 fun init_item str = SyntaxE str;

   | ts_in (Inc ((_,ts),_)) = ts

   | ts_in (Inc ((_,ts),_)) = ts

   | ts_in (Sup (_,ts)) = ts

   | ts_in (Sup (_,ts)) = ts

   | ts_in (Mis _) = [];

   | ts_in (Mis _) = [];

 (*WN050629 unused*)

 (*WN050629 unused*)

 fun all_ts_in itm_s = (flat o (map ts_in)) itm_s;

 fun all_ts_in itm_s = (flat o (map ts_in)) itm_s;

 fun d_in (Cor ((d,_),_)) = d

 fun d_in (Cor ((d,_),_)) = d

   | d_in (Syn  (c)) = (writeln("*** d_in: Syn ("^c^")"); unique)

   | d_in (Syn  (c)) = (writeln("*** d_in: Syn ("^c^")"); unique)

   | d_in (Typ  (c)) = (writeln("*** d_in: Typ ("^c^")"); unique)

   | d_in (Typ  (c)) = (writeln("*** d_in: Typ ("^c^")"); unique)

   | d_in (Inc ((d,_),_)) = d

   | d_in (Inc ((d,_),_)) = d

   | d_in (Sup (d,_)) = d

   | d_in (Sup (d,_)) = d

 (*. check a predicate labelled with indication of incomplete substitution;

 (*. check a predicate labelled with indication of incomplete substitution;

 rls ->    (*for eval_true*)

 rls ->    (*for eval_true*)

 bool * 	  (*have _all_ variables(Free) from the model-pattern 

 bool * 	  (*have _all_ variables(Free) from the model-pattern 

             been substituted by a value from the pattern's environment ?*)

             been substituted by a value from the pattern's environment ?*)

 ->

 ->

 bool * 	  (*has the precondition evaluated to true*)

 bool * 	  (*has the precondition evaluated to true*)

 .*)

 .*)

 fun evalprecond prls (false, pre) = 

 fun evalprecond prls (false, pre) = 

   (*NOT ALL Free's have been substituted, eg. because of incomplete model*)

   (*NOT ALL Free's have been substituted, eg. because of incomplete model*)

     (false, pre)

     (false, pre)

   | evalprecond prls (true, pre) =

   | evalprecond prls (true, pre) =

       fun vt_and_dsc d' ((i,v,f,d,ts):ori) =

       fun vt_and_dsc d' ((i,v,f,d,ts):ori) =

 	  vt mem v andalso d'= d

 	  vt mem v andalso d'= d

       fun cpy its [] (f, (d, id)) = 

       fun cpy its [] (f, (d, id)) = 

 	  if length its = 0        (*no dsc found in pbl*)

 	  if length its = 0        (*no dsc found in pbl*)

 	  then case find_first (vt_and_dsc d) oris

 	  then case find_first (vt_and_dsc d) oris

 		   [(i,v,true,f, Cor ((d,ts), (id,pbl_ids' thy d ts)))]

 		   [(i,v,true,f, Cor ((d,ts), (id,pbl_ids' thy d ts)))]

 	  else its	       

 	  else its	       

 	| cpy its ((it as (i, vs, b, f, itm_))::itms) (pb as (x, (d, id))) =

 	| cpy its ((it as (i, vs, b, f, itm_))::itms) (pb as (x, (d, id))) =

 	  if d = d_in itm_ andalso i<>0 (*already touched by user*)

 	  if d = d_in itm_ andalso i<>0 (*already touched by user*)

 	  then cpy (its @ [it]) itms pb else cpy its itms pb;	  

 	  then cpy (its @ [it]) itms pb else cpy its itms pb;	  

   in ((flat o (map (cpy [] pbl))) met):itm list end;

   in ((flat o (map (cpy [] pbl))) met):itm list end;

 (* val (pbl, met) = (itms, pbt);

 (* val (pbl, met) = (itms, pbt);

    *)

    *)

 fun copy_pbl (pbl:itm list) met oris =

 fun copy_pbl (pbl:itm list) met oris =

   let fun eqdsc_pbt_itm ((_,(d,_))) ((_,_,_,_,itm_):itm) = d = d_in itm_;

   let fun eqdsc_pbt_itm ((_,(d,_))) ((_,_,_,_,itm_):itm) = d = d_in itm_;

       fun notmem pbl pbt1 = case find_first (eqdsc_pbt_itm pbt1) pbl of

       fun notmem pbl pbt1 = case find_first (eqdsc_pbt_itm pbt1) pbl of

  (*1*)val mis = ((map (cons2 (fst, fst o snd))) o (filter (notmem pbl))) met;

  (*1*)val mis = ((map (cons2 (fst, fst o snd))) o (filter (notmem pbl))) met;

       fun eqdsc_ori d ((_,_,_,d',_):ori) = d = d';

       fun eqdsc_ori d ((_,_,_,d',_):ori) = d = d';

       fun ori2itmMis f ((i,v,_,d,ts):ori) = (i,v,false,f,Mis (d,ts)):itm;

       fun ori2itmMis f ((i,v,_,d,ts):ori) = (i,v,false,f,Mis (d,ts)):itm;

       fun oris2itms oris mis1 = ((map (ori2itmMis (fst mis1)))

       fun oris2itms oris mis1 = ((map (ori2itmMis (fst mis1)))