(* Title: Model for (sub-)calculations.

           Various representations: item and ppc for frontend, itm_ and itm for internal functions.

           The former are related to structure Specify, the latter to structure Chead --

           -- apt to re-arrangement of structures

    Author: Walther Neuper 170207

    (c) due to copyright terms

 *)

 signature MODEL =

 sig

   type ori

   val oris2str : ori list -> string

   val e_ori : ori

   datatype item

   = Correct of TermC.as_string | False of TermC.as_string | Incompl of TermC.as_string | Missing of TermC.as_string | Superfl of string

      | SyntaxE of string | TypeE of string

   datatype itm_ = Cor of (term * (term list)) * (term * (term list))

   | Syn of TermC.as_string | Typ of TermC.as_string | Inc of (term * (term list))	* (term * (term list))

   | Sup of (term * (term list)) | Mis of (term * term) | Par of TermC.as_string

   val itm_2str : itm_ -> string

   val itm_2str_ : Proof.context -> itm_ -> string

   type itm

   val itm2str_ : Proof.context -> itm -> string

   val itms2str_ : Proof.context -> itm list -> string

   val e_itm : itm 

   type 'a ppc

   val empty_ppc : item ppc

   val ppc2str : {Find: string list, Given: string list, Relate: string list, Where: string list,

     With: string list} -> string

   val itemppc2str : item ppc -> string

   type vats

   val comp_dts : term * term list -> term

   val comp_dts' : term * term list -> term

   val comp_dts'' : term * term list -> string

   val comp_ts : term * term list -> term

   val split_dts : term -> term * term list

   val split_dts' : term * term -> term list

   val pbl_ids' : term -> term list -> term list

   val mkval' : term list -> term

   val d_in : itm_ -> term

   val ts_in : itm_ -> term list

   val penvval_in : itm_ -> term list

   val mk_env : itm list -> (term * term) list (* close to Chead.all_dsc_in, Chead.is_error, etc *)

   val vars_of : itm list -> term list

   val max_vt : itm list -> int

 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)

   type penv

   val penv2str_ : Proof.context -> penv -> string  (* NONE *)

   type preori

   val preoris2str : preori list -> string

 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )

   (* NONE *)

 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)

 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)

   val untouched : itm list -> bool

   type envv

   val upds_envv : Proof.context -> envv -> (vats * term * term * term) list -> envv

   val item_ppc : string ppc -> item ppc

   val all_ts_in : itm_ list -> term list

   val pres2str : (bool * term) list -> string

 end

 structure Model(**) : MODEL(**) =

 struct

 (*==========================================================================

 23.3.02 TODO: ideas on redesign of type itm_,type item,type ori,type item ppc

 (1) kinds of itms:

   (1.1) untouched: for modeling only dsc displayed(impossible after match_itms)

         =(presently) Mis (? should be Inc initially, and Mis after match_itms?)

   (1.2)  Syn,Typ,Sup: not related to oris

     Syn, Typ (presently) should be accepted in appl_add (instead Error')

     Sup      (presently) should be accepted in appl_add (instead Error')

          _could_ be w.r.t current vat (and then _is_ related to vat

     Mis should _not_ be  made Inc ((presently, by appl_add & match_itms)

 - dsc in itm_ is timeconsuming -- keep id for respective queries ?

 - order of items in ppc should be stable w.r.t order of itms

 - stepwise input of itms --- match_itms (in one go) ..not coordinated

   - unify code

   - match_itms / match_itms_oris ..2 versions ?!

     (fast, for refine / slow, for modeling)

 - clarify: efficiency <--> simplicity !!!

   ?: shift dsc itm_ -> itm | discard int in ori,itm | take int instead dsc 

     | take int for perserving order of item ppc in itms 

     | make all(!?) handling of itms stable against reordering(?)

     | field in ori ?? (not from fmz!) -- meant for efficiency (not doc!???)

       -"- "#undef" ?= not touched ?= (id,..)

 -----------------------------------------------------------------

 27.3.02:

 def: type pbt = (field, (dsc, pid)) *** design considerations ***

 (1) fmz + pbt -> oris

 (2) input + oris -> itm

 (3) match_itms      : schnell(?) f"ur refine

     match_itms_oris : r"uckmeldung f"ur item ppc

 (1.1) in oris fehlt daher pid: (i,v,f,d,ts,pid)

 ---------- ^^^^^ --- dh. pbt meist als argument zu viel !!!

 (3.1) abwarten, wie das matchen mehr unterschiedlicher pbt's sich macht;

       wenn Problem pbt v"ollig neue, dann w"are eigentlich n"otig ????:

       (a) (_,_,d1,ts,_):ori + pbt -> (i,vt,d2,ts,pid)  dh.vt neu  ????

       (b) 

 ==========================================================================*)

 val script_parse = the o (@{theory ProgLang} |> ThyC.to_ctxt |> TermC.parseNEW);

 val e_listReal = script_parse "[]::(real list)";

 val e_listBool = script_parse "[]::(bool list)";

 (* take list-term apart w.r.t. handling elementwise input: @{term "[a, b]"} \<rightarrow> ["[a]","[b]"] *)

 fun take_apart t =

   let val elems = TermC.isalist2list t

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

 fun take_apart_inv ts = (* t = (take_apart_inv o take_apart) t *)

   let val elems = (flat o (map TermC.isalist2list)) ts;

   in TermC.list2isalist (type_of (hd elems)) elems end;

 fun is_var (Free _) = true

   | is_var _ = false;

 (* special handling for lists. ?WN:14.5.03 ??!? *)

 fun dest_list (d, ts) = 

   let fun dest t = 

     if Input_Descript.is_list_dsc d andalso not (Input_Descript.is_unl d) andalso not (is_var t) (*..for pbt*)

     then TermC.isalist2list t

     else [t]

   in (flat o (map dest)) ts end;

 (* revert split_dts only for ts; compare comp_dts *)

 fun comp_ts (d, ts) = 

   if Input_Descript.is_list_dsc d

   then if TermC.is_list (hd ts)

 	  then if Input_Descript.is_unl d

 	    then (hd ts)             (* e.g. someList [1,3,2] *)

 	    else (take_apart_inv ts) (* [ [a], [b] ] -> [a,b] *)

 	  else (hd ts)               (* a variable or metavariable for a list *)

   else (hd ts);

 fun comp_dts (d, []) = 

   	if Input_Descript.is_reall_dsc d

   	then (d $ e_listReal)

   	else if Input_Descript.is_booll_dsc d then (d $ e_listBool) else d

   | comp_dts (d, ts) = (d $ (comp_ts (d, ts)))

     handle _ => error ("comp_dts: " ^ UnparseC.term d ^ " $ " ^ UnparseC.term (hd ts)); 

 fun comp_dts' (d, []) = 

     if Input_Descript.is_reall_dsc d

     then (d $ e_listReal)

     else if Input_Descript.is_booll_dsc d then (d $ e_listBool) else d

   | comp_dts' (d, ts) = (d $ (comp_ts (d, ts)))

     handle _ => error ("comp_dts': " ^ UnparseC.term d ^ " $ " ^ UnparseC.term (hd ts)); 

 fun comp_dts'' (d, []) = 

     if Input_Descript.is_reall_dsc d

     then UnparseC.term (d $ e_listReal)

     else if Input_Descript.is_booll_dsc d

       then UnparseC.term (d $ e_listBool)

       else UnparseC.term d

   | comp_dts'' (d, ts) = UnparseC.term (d $ (comp_ts (d, ts)))

     handle _ => error ("comp_dts'': " ^ UnparseC.term d ^ " $ " ^ UnparseC.term (hd ts)); 

 (* decompose an input into description, terms (ev. elems of lists),

     and the value for the problem-environment; inv to comp_dts   *)

 fun split_dts (t as d $ arg) =

     if Input_Descript.is_dsc d

     then if Input_Descript.is_list_dsc d andalso TermC.is_list arg andalso Input_Descript.is_unl d |> not

       then (d, take_apart arg)

       else (d, [arg])

     else (TermC.empty, TermC.dest_list' t)

   | split_dts t =

     let val t' as (h, _) = strip_comb t;

     in

       if Input_Descript.is_dsc h

       then (h, dest_list t')

       else (TermC.empty, TermC.dest_list' t)

     end;

 (* version returning ts only *)

 fun split_dts' (d, arg) = 

     if Input_Descript.is_dsc d

     then if Input_Descript.is_list_dsc d

       then if TermC.is_list arg

 	      then if Input_Descript.is_unl d

 	        then ([arg])           (* e.g. someList [1,3,2]                 *)

 		      else (take_apart arg)  (* [a,b] --> SML[ [a], [b] ]SML          *)

 	      else ([arg])             (* a variable or metavariable for a list *)

 	     else ([arg])

     else (TermC.dest_list' arg)

 (* WN170204: Warning "redundant"

   | split_dts' (d, t) =          (*either dsc or term; 14.5.03 only copied*)

     let val (h,argl) = strip_comb t

     in

       if (not o is_dsc) h

       then (dest_list' t)

       else (dest_list (h,argl))

     end;*)

 (* revert split_:

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

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

  solution: typecheck with (Thy_Info_get_theory "Isac_Knowledge"); i.e. arg 'thy' superfluous*)

 (*fun comp_dts thy (d,[]) = 

     Thm.global_cterm_of (*(sign_of o assoc_thy) "Isac_Knowledge"*)

 	     (Thy_Info_get_theory "Isac_Knowledge")

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

 	     (if is_reall_dsc d then (d $ e_listReal)

 	      else if is_booll_dsc d then (d $ e_listBool)

 	      else d)

   | comp_dts (d,ts) =

     (Thm.global_cterm_of (*(sign_of o assoc_thy) "Isac_Knowledge"*)

 	      (Thy_Info_get_theory "Isac_Knowledge")

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

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

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

 				" $ "^(term2str (hd ts))));*)

 (* 27.8.01: problem-environment

 WN.6.5.03: FIXXME reconsider if penv is worth the effort --

            -- just rerun a whole expl with num/var may show the same ?!

 WN.9.5.03: penv-concept stalled, immediately generate script env !

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

 type penv = (* problem-environment *)

   (term           (* err_                              *)

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

 	) list;

 fun pen2str ctxt (t, ts) =

   pair2str (UnparseC.term_in_ctxt ctxt t, (strs2str' o map (UnparseC.term_in_ctxt  ctxt)) ts);

 fun penv2str_ thy penv = (strs2str' o (map (pen2str thy))) penv;

 (* get the constant value from a penv *)

 fun getval (id, values) = 

   case values of

 	  [] => error ("penv_value: no values in '" ^ UnparseC.term id)

   | [v] => (id, v)

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

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

 	    | _ => (id, v1));

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

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

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

    make the result of split_* a value of problem-environment *)

 fun mkval _(*dsc*) [] = error "mkval called with []"

   | mkval _ [t] = t

   | mkval _ ts = TermC.list2isalist ((type_of o hd) ts) ts;

 fun mkval' x = mkval TermC.empty x;

 (* the internal representation of a models' item

   4.9.01: not consistent:

   after Init_Proof 'Inc', but after copy_probl 'Mis' - for same situation

   (involves 'is_error');

   bool in itm really necessary ???*)

 datatype itm_ = 

   Cor of (term *              (* description                                                     *)

     (term list)) *            (* for list: elem-wise input                                       *) 

    (term * (term list))       (* elem of penv ---- penv delayed to future                        *)

 | Syn of TermC.as_string

 | Typ of TermC.as_string

 | Inc of (term * (term list))	* (term * (term list)) (*lists,

 			+ init_pbl WN.11.03 FIXXME: empty penv .. bad; init_pbl should return Mis !!!              *)

 | Sup of (term * (term list)) (* user-input not found in pbt(+?oris?11.03)*)

 | Mis of (term * term)        (* after re-specification pbt-item not found in pbl: only dsc, pid_*)

 | Par of TermC.as_string;              (* internal state from fun parsitm                                 *)

 type vats = int list; (* variants in formalizations *)

 (* data-type for working on pbl/met-ppc:

   in pbl initially holds descriptions (only) for user guidance *)

 type itm = 

   int *        (* id  =0 .. untouched - descript (only) from init 

 		              seems to correspond to ori (fun insert_ppc) <> maintain order in item ppc?   *)

   vats *       (* variants - copy from ori                                                     *)

   bool *       (* input on this item is not/complete                                           *)

   string *     (* #Given | #Find | #Relate                                                     *)

   itm_;        (*                                                                              *)

 val e_itm = (0, [], false, "e_itm", Syn "e_itm");

 (* in CalcTree/Subproblem an 'untouched' model is created

   FIXME.WN.9.03 model should be filled to 'untouched' by Model/Refine_Problem*)

 fun untouched itms = foldl and_ (true , map ((curry op = 0) o (#1 : itm -> int)) itms);

 (* find most frequent variant v in itms *)

 fun vts_in itms = (distinct o flat o (map #2)) (itms:itm list);

 fun cnt itms v = (v, (length o (filter (curry op = v)) o flat o (map #2)) itms);

 fun vts_cnt vts itms = map (cnt itms) vts;

 fun max2 [] = error "max2 of []"

   | max2 (y :: ys) =

     let

       fun mx (a,x) [] = (a,x)

   	    | mx (a, x) ((b,y) :: ys) = if x < y then mx (b, y) ys else mx (a, x) ys;

     in mx y ys end;

 (* find the variant with most items already input *)

 fun max_vt itms = 

     let val vts = (vts_cnt (vts_in itms)) itms;

     in if vts = [] then 0 else (fst o max2) vts end;

 (* TODO ev. make more efficient by avoiding flat *)

 fun mk_e (Cor (_, iv)) = [getval iv]

   | mk_e (Syn _) = []

   | mk_e (Typ _) = [] 

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

   | mk_e (Sup _) = []

   | mk_e (Mis _) = []

   | mk_e  _ = error "mk_e: uncovered case in fun.def.";

 fun mk_en vt (_, vts, _, _, itm_) = if member op = vts vt then mk_e itm_ else [];

 (* extract the environment from an item list; takes the variant with most items *)

 fun mk_env itms = 

   let val vt = max_vt itms

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

 (* example as provided by an author, complete w.r.t. pbt specified 

    not touched by any user action                                 *)

 type ori =

   (int *     (* id: 10.3.00ff impl. only <>0 .. touched 

 			          21.3.02: insert_ppc needs it ! ?:purpose maintain order in item ppc ??? *)

 	vats *     (* variants 21.3.02: related to pbt..discard ?                             *)

 	string *   (* #Given | #Find | #Relate 21.3.02: discard ?                             *)

 	term *     (* description                                                             *)

 	term list  (* isalist2list t | [t]                                                    *)

 	);

 val e_ori = (0, [], "", TermC.empty, [TermC.empty]) : ori;

 fun ori2str (i, vs, fi, t, ts) = 

   "(" ^ string_of_int i ^ ", " ^ (strs2str o (map string_of_int)) vs ^ ", " ^ fi ^ "," ^

   UnparseC.term t ^ ", " ^ (strs2str o (map UnparseC.term)) ts ^ ")";

 val oris2str = strs2str' o (map (linefeed o ori2str));

 (* an or without leading integer *)

 type preori = (vats * string * term * term list);

 fun preori2str (vs, fi, t, ts) = 

   "(" ^ (strs2str o (map string_of_int)) vs ^ ", " ^ fi ^ ", " ^

   UnparseC.term t ^ ", " ^ (strs2str o (map UnparseC.term)) ts ^ ")";

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

 (* 9.5.03 penv postponed: pbl_ids' *)

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

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

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

 fun upd_penv ctxt penv dsc (id, vl) =

 ((*tracing"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";

  tracing"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";

  tracing"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";*)

   overwrite (penv, (id, Input_Descript.pbl_ids ctxt dsc vl))

 );

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

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

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

 		       SOME e => e

 		     | NONE => [];

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

     in (i, penv') end;

 (* 14.9.01: not used after putting pre-penv into itm_*)

 fun upd_envv thy envv vats dsc id vl  =

     let val vats = if length vats = 0 

 		   then (*unknown id to _all_ variants*)

 		       if length envv = 0 then [1]

 		       else (intsto o length) envv 

 		   else vats

 	fun isin vats (i, _) = member op = vats i;

 	val envs_notin_vat = filter_out (isin vats) envv;

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

 (* update envv by folding from a list of arguments *)

 fun upds_envv _ envv [] = envv

   | upds_envv thy envv ((vs, dsc, id, vl) :: ps) = 

     upds_envv thy (upd_envv thy envv vs dsc id vl) ps;

 (* for _output_ of the items of a Model *)

 datatype item = 

     Correct of TermC.as_string (* labels a correct formula (type cterm') *)

   | SyntaxE of string (**)

   | TypeE   of string (**)

   | False   of TermC.as_string (* WN050618 notexistent in itm_: only used in Where *)

   | Incompl of TermC.as_string (**)

   | Superfl of string (**)

   | Missing of TermC.as_string;

 fun item2str (Correct  s) ="Correct " ^ s

   | item2str (SyntaxE  s) ="SyntaxE " ^ s

   | item2str (TypeE    s) ="TypeE " ^ s

   | item2str (False    s) ="False " ^ s

   | item2str (Incompl  s) ="Incompl " ^ s

   | item2str (Superfl  s) ="Superfl " ^ s

   | item2str (Missing  s) ="Missing " ^ s;

 (*make string for error-msgs*)

 fun itm_2str_ ctxt (Cor ((d, ts), penv)) = 

     "Cor " ^ UnparseC.term_in_ctxt  ctxt (comp_dts (d, ts)) ^ " ," ^ pen2str ctxt penv

   | itm_2str_ _ (Syn c) = "Syn " ^ c

   | itm_2str_ _ (Typ c) = "Typ " ^ c

   | itm_2str_ ctxt (Inc ((d, ts), penv)) = 

     "Inc " ^ UnparseC.term_in_ctxt  ctxt (comp_dts (d, ts)) ^ " ," ^ pen2str ctxt penv

   | itm_2str_ ctxt (Sup (d, ts)) = 

     "Sup " ^ UnparseC.term_in_ctxt  ctxt (comp_dts (d, ts))

   | itm_2str_ ctxt (Mis (d, pid)) = 

     "Mis "^ UnparseC.term_in_ctxt  ctxt d ^ " " ^ UnparseC.term_in_ctxt  ctxt pid

   | itm_2str_ _ (Par s) = "Trm "^s;

 fun itm_2str t = itm_2str_ (ThyC.id_to_ctxt "Isac_Knowledge") t;

 fun itm2str_ ctxt ((i, is, b, s, itm_):itm) = 

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

   s ^ " ," ^ itm_2str_ ctxt itm_ ^ ")";

 fun itms2str_ ctxt itms = strs2str' (map (linefeed o (itm2str_ ctxt)) itms);

 fun init_item str = SyntaxE str;

 type 'a ppc = 

   {Given : 'a list, Where: 'a list, Find  : 'a list, With : 'a list, Relate: 'a list};

 fun ppc2str {Given = Given, Where = Where, Find = Find, With = With, Relate = Relate}=

   "{Given =" ^ strs2str Given ^ ",Where=" ^ strs2str Where ^ ",Find  =" ^ strs2str Find ^

   ",With =" ^ strs2str With ^ ",Relate=" ^ strs2str Relate ^ "}";

 fun item_ppc {Given = gi, Where= wh, Find = fi, With = wi, Relate= re} =

   {Given = map init_item gi, Where= map init_item wh, Find = map init_item fi,

     With = map init_item wi, Relate= map init_item re};

 fun itemppc2str ({Given=Given,Where=Where,

 		 Find=Find,With=With,Relate=Relate}:item ppc)=

     ("{Given =" ^ ((strs2str' o (map item2str))	 Given ) ^

      ",Where=" ^ ((strs2str' o (map item2str))	 Where) ^

      ",Find  =" ^ ((strs2str' o (map item2str))	 Find  ) ^

      ",With =" ^ ((strs2str' o (map item2str))	 With ) ^

      ",Relate=" ^ ((strs2str' o (map item2str))	 Relate) ^ "}");

 val empty_ppc = {Given = [], Where= [], Find  = [], With = [], Relate= []};

 fun ts_in (Cor ((_, ts), _)) = ts

   | ts_in (Syn _) = []

   | ts_in (Typ _) = []

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

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

   | ts_in (Mis _) = []

   | ts_in _ = error "ts_in: uncovered case in fun.def.";

 (*WN050629 unused*)

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

 val unique = (Thm.term_of o the o (TermC.parse @{theory "Real"} )) "UnIqE_tErM";

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

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

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

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

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

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

   | d_in _ = raise ERROR "d_in: uncovered case in fun.def.";

 fun dts2str (d, ts) = pair2str (UnparseC.term d, UnparseC.terms ts);

 fun penvval_in (Cor ((d, _), (_, ts))) = [comp_ts (d,ts)]

   | penvval_in (Syn  (c)) = ((*tracing("*** penvval_in: Syn ("^c^")");*) [])

   | penvval_in (Typ  (c)) = ((*tracing("*** penvval_in: Typ ("^c^")");*) [])

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

   | penvval_in (Sup dts) = ((*tracing ("*** penvval_in: Sup " ^ dts2str dts);*) [])

   | penvval_in (Mis (d, t)) = ((*tracing ("*** penvval_in: Mis " ^

 			pair2str(UnparseC.term d, UnparseC.term t));*) [])

 	| penvval_in _ = error "penvval_in: uncovered case in fun.def.";

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

   rls ->    (* for eval_true                                               *)

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

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

   term ->   (* the precondition                                            *)

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

   term      (* the precondition (for map)                                  *)

 *)

 fun pre2str (b, t) = pair2str(bool2str b, UnparseC.term t);

 fun pres2str pres = strs2str' (map (linefeed o pre2str) pres);

 fun vars_of itms = itms |> mk_env |> map snd

 end;