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