(* 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 Rule.cterm' | False of Rule.cterm' | Incompl of Rule.cterm' | Missing of Rule.cterm' | Superfl of string

     | SyntaxE of string | TypeE of string

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

  | Syn of Rule.cterm' | Typ of Rule.cterm' | Inc of (term * (term list))	* (term * (term list))

  | Sup of (term * (term list)) | Mis of (term * term) | Par of Rule.cterm'

  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} |> Rule.thy2ctxt |> 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: " ^ Rule.term2str d ^ " $ " ^ Rule.term2str (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': " ^ Rule.term2str d ^ " $ " ^ Rule.term2str (hd ts)); 

fun comp_dts'' (d, []) = 

    if Input_Descript.is_reall_dsc d

    then Rule.term2str (d $ e_listReal)

    else if Input_Descript.is_booll_dsc d

      then Rule.term2str (d $ e_listBool)

      else Rule.term2str d

  | comp_dts'' (d, ts) = Rule.term2str (d $ (comp_ts (d, ts)))

    handle _ => error ("comp_dts'': " ^ Rule.term2str d ^ " $ " ^ Rule.term2str (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 (Rule.e_term, 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 (Rule.e_term, 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 (Rule.term_to_string' ctxt t, (strs2str' o map (Rule.term_to_string'  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 '" ^ Rule.term2str 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 Rule.e_term 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 Rule.cterm'

| Typ of Rule.cterm'

| 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 Rule.cterm';              (* 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, [], "", Rule.e_term, [Rule.e_term]) : ori;

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

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

  Rule.term2str t ^ ", " ^ (strs2str o (map Rule.term2str)) ts ^ ")";

val oris2str = strs2str' o (map (Celem.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 ^ ", " ^

  Rule.term2str t ^ ", " ^ (strs2str o (map Rule.term2str)) ts ^ ")";

val preoris2str = (strs2str' o (map (Celem.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 Rule.cterm' (* labels a correct formula (type cterm') *)

  | SyntaxE of string (**)

  | TypeE   of string (**)

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

  | Incompl of Rule.cterm' (**)

  | Superfl of string (**)

  | Missing of Rule.cterm';

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 " ^ Rule.term_to_string'  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 " ^ Rule.term_to_string'  ctxt (comp_dts (d, ts)) ^ " ," ^ pen2str ctxt penv

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

    "Sup " ^ Rule.term_to_string'  ctxt (comp_dts (d, ts))

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

    "Mis "^ Rule.term_to_string'  ctxt d ^ " " ^ Rule.term_to_string'  ctxt pid

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

fun itm_2str t = itm_2str_ (Rule.thy2ctxt' "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 (Celem.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 _ = error "d_in: uncovered case in fun.def.";

fun dts2str (d, ts) = pair2str (Rule.term2str d, Rule.terms2str 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(Rule.term2str d, Rule.term2str 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, Rule.term2str t);

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

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

end;