(* Title:  collect all defitions for the Lucas-Interpreter

   Author: Walther Neuper 110226

   (c) due to copyright terms

Descriptors for input into an I_Model.

Since PblObj.ctxt records explicit type constraints in Formalise.model,

the types of the descriptors below can be more relaxed. 

*)

theory Input_Descript imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"

begin

subsection \<open>typedecl for descriptors of input in specify-phase\<close>

text \<open>

  The typedecl below MUST ALL be registered in "Input_Descript.is_a"

\<close>

  typedecl nam     (* named variables                                             *)

  typedecl una     (* unnamed variables                                           *)

  typedecl unl     (* unnamed variables of type list, elementwise input prohibited*)

  typedecl str     (* structured variables                                        *)

  typedecl toreal  (* var with undef real value: forces typing                    *)

  typedecl toreall (* var with undef real list value: forces typing               *)

  typedecl tobooll (* var with undef bool list value: forces typing               *)

  typedecl unknow  (* input without dsc in fmz=[]                                 *)

  typedecl cpy     (* copy-named variables identified by .._0, .._i .._' in pbt   *)

subsection \<open>consts for general descriptors of input in the specify-phase\<close>

consts

(*TODO.180331: review for localisation of model-patterns and of method's guards*)

  someList       :: "'a list => unl" (*not for elementwise input, eg. inssort*)

  additionalRels :: "bool list => una"

  boundVariable    :: "real => una"

  FunctionVariable :: "real => una"

  derivative     :: "real => una"

  equalities     :: "bool list => tobooll" (*WN071228 see fixedValues*)

  equality       :: "bool => una"

  errorBound     :: "bool => nam"

  ErrorBound     :: "bool => nam"

  fixedValues    :: "bool list => nam"

  Constants      :: "bool list => nam"

  functionEq     :: "bool => una"     (*6.5.03: functionTerm -> functionEq*)

  antiDerivative :: "bool => una"

  functionOf     :: "real => una"

(*functionTerm   :: 'a => toreal 28.11.00*)

  functionTerm   :: "real => una"     (*6.5.03: functionTerm -> functionEq*)

  functionName   :: "real => una"

  interval       :: "real set => una"

  Domain         :: "real set => una"

  maxArgument    :: "bool => toreal"

  maximum        :: "real => toreal"

  Maximum        :: "real => toreal"

  Extremum       :: "bool => toreal"

  relations      :: "bool list => una"

  SideConditions :: "bool list => una"

  solutions      :: "bool list => toreall"

(*solution       :: bool => toreal  WN0509 bool list=> toreall --->EqSystem*)

  solveFor       :: "real => una"

  differentiateFor:: "real => una"

  unknown        :: "'a => unknow"

  valuesFor        :: "real list => toreall"

  AdditionalValues :: "real list => toreall"

  intTestGiven   :: "int => una"

  realTestGiven  :: "real => una"

  realTestFind   :: "real => una"

  boolTestGiven  :: "bool => una"

  boolTestFind   :: "bool => una"

subsection \<open>Functions decking for descriptions of input in specify-phase\<close>

ML \<open>

\<close> ML \<open>

signature INPUT_DESCRIPT =

sig

(*type T          ..TODO rename*)

  type descriptor = Model_Pattern.descriptor

  val for_real_list: term -> bool

  val for_list: term -> bool

\<^isac_test>\<open>

  val for_bool_list: term -> bool

  val for_fun: term -> bool

  val is_a: term -> bool 

\<close>

  val split: term -> descriptor * term list

  val split': term * term -> term list

  val join: descriptor * term list -> term

  val join': descriptor * term list -> term

  val join''': descriptor * term list -> string

  val join'''': descriptor * term list -> term

end

\<close> ML \<open>

(**)

structure Input_Descript(**): INPUT_DESCRIPT =(**)

struct

(**)

type descriptor = Model_Pattern.descriptor;

(* distinguish input to Model (deep embedding of terms as Isac's object language) *)

fun for_real_list (Const (_, Type(\<^type_name>\<open>fun\<close>, [Type(\<^type_name>\<open>list\<close>, [Type (\<^type_name>\<open>real\<close>, [])]), _]))) = true

  | for_real_list (Const (_, Type(\<^type_name>\<open>fun\<close>, [Type(\<^type_name>\<open>list\<close>, [Type (\<^type_name>\<open>real\<close>, [])]),_])) $ _) = true

  | for_real_list _ = false;

fun for_bool_list (Const (_, Type(\<^type_name>\<open>fun\<close>, [Type(\<^type_name>\<open>list\<close>, [Type (\<^type_name>\<open>bool\<close>, [])]), _]))) = true

  | for_bool_list (Const (_, Type(\<^type_name>\<open>fun\<close>, [Type(\<^type_name>\<open>list\<close>, [Type (\<^type_name>\<open>bool\<close>, [])]),_])) $ _) = true

  | for_bool_list _ = false;

fun for_list (Const (_, Type(\<^type_name>\<open>fun\<close>, [Type(\<^type_name>\<open>list\<close>, _), _]))) = true

  | for_list (Const (_, Type(\<^type_name>\<open>fun\<close>, [Type(\<^type_name>\<open>list\<close>, _), _])) $ _) = true

  (*WN:8.5.03: ???   TODO test/../scrtools.sml                ~~~~ ???*)

  | for_list _ = false;

fun for_fun (Const (_, Type(\<^type_name>\<open>fun\<close>, [_, Type(\<^type_name>\<open>unl\<close>, _)]))) = true

  | for_fun _ = false;

fun is_a (Const(_, Type(\<^type_name>\<open>fun\<close>, [_, Type(\<^type_name>\<open>nam\<close>, _)]))) = true

  | is_a (Const(_, Type(\<^type_name>\<open>fun\<close>, [_, Type(\<^type_name>\<open>una\<close>, _)]))) = true

  | is_a (Const(_, Type(\<^type_name>\<open>fun\<close>, [_, Type(\<^type_name>\<open>unl\<close>, _)]))) = true

  | is_a (Const(_, Type(\<^type_name>\<open>fun\<close>, [_, Type(\<^type_name>\<open>str\<close>, _)]))) = true

  | is_a (Const(_, Type(\<^type_name>\<open>fun\<close>, [_, Type(\<^type_name>\<open>toreal\<close>, _)]))) = true

  | is_a (Const(_, Type(\<^type_name>\<open>fun\<close>, [_, Type(\<^type_name>\<open>toreall\<close>, _)])))= true

  | is_a (Const(_, Type(\<^type_name>\<open>fun\<close>, [_, Type(\<^type_name>\<open>tobooll\<close>, _)])))= true

  | is_a (Const(_, Type(\<^type_name>\<open>fun\<close>, [_, Type(\<^type_name>\<open>unknow\<close>, _)])))= true

  | is_a (Const(_, Type(\<^type_name>\<open>fun\<close>, [_, Type(\<^type_name>\<open>cpy\<close>, _)])))= true

  | is_a _ = false;

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

fun dest_list (d, ts) = 

  let fun dest t = 

    if for_list d andalso not (for_fun d) andalso not (is_Free t) (*..for pbt*)

    then TermC.isalist2list t

    else [t]

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

(* 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;

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

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

fun split (t as d $ arg) =

    if is_a d

    then if for_list d andalso TermC.is_list arg andalso for_fun d |> not

      then (d, take_apart arg)

      else (d, [arg])

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

  | split t =

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

    in

      if is_a h

      then (h, dest_list t')

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

    end;

(* version returning ts only *)

fun split' (d, arg) = 

    if is_a d

    then if for_list d

      then if TermC.is_list arg

	      then if for_fun 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)

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

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;

val script_parse = the o (@{theory BaseDefinitions} |> Proof_Context.init_global |> TermC.parseNEW);

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

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

(* revert split only for ts; jcompare join *)

fun join'''' (d, ts) = 

  if for_list d

  then if TermC.is_list (hd ts)

	  then if for_fun 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 join (d, []) = 

  	if for_real_list d

  	then (d $ e_listReal)

  	else if for_bool_list d then (d $ e_listBool) else d

  | join (d, ts) = 

    case \<^try>\<open> d $ (join'''' (d, ts))\<close> of

      SOME x => x

    | NONE => raise ERROR ("join: " ^ UnparseC.term d ^ " $ " ^ UnparseC.term (hd ts)); 

fun join' (d, []) = 

    if for_real_list d

    then (d $ e_listReal)

    else if for_bool_list d then (d $ e_listBool) else d

  | join' (d, ts) = 

    case \<^try>\<open> d $ (join'''' (d, ts))\<close> of

      SOME x => x

    | NONE => raise ERROR ("join': " ^ UnparseC.term d ^ " $ " ^ UnparseC.term (hd ts)); 

fun join''' (d, []) = 

    if for_real_list d

    then UnparseC.term (d $ e_listReal)

    else if for_bool_list d

      then UnparseC.term (d $ e_listBool)

      else UnparseC.term d

  | join''' (d, ts) = 

    case \<^try>\<open> UnparseC.term (d $ (join'''' (d, ts)))\<close> of

      SOME x => x

    | NONE => raise ERROR ("join''': " ^ UnparseC.term d ^ " $ " ^ UnparseC.term (hd ts)); 

(**)end(**)

\<close> ML \<open>

\<close> ML \<open>

\<close> 

end