wneuper@59595: (* Title:  collect all defitions for the Lucas-Interpreter
wneuper@59595:    Author: Walther Neuper 110226
wneuper@59595:    (c) due to copyright terms
walther@59950: 
Walther@60556: Descriptors for interactive input into a Specification of an Example.
Walther@60556: 
walther@59950: Since PblObj.ctxt records explicit type constraints in Formalise.model,
Walther@60556: and since we have Model_Pattern.adapt_to_type,
walther@59950: the types of the descriptors below can be more relaxed. 
walther@59950: *)
wneuper@59595: 
wenzelm@60192: theory Input_Descript imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
wneuper@59595: begin
wneuper@59595: 
walther@59951: subsection \<open>typedecl for descriptors of input in specify-phase\<close>
wneuper@59595: text \<open>
walther@59953:   The typedecl below MUST ALL be registered in "Input_Descript.is_a"
wneuper@59595: \<close>
wneuper@59595:   typedecl nam     (* named variables                                             *)
wneuper@59595:   typedecl una     (* unnamed variables                                           *)
wneuper@59595:   typedecl unl     (* unnamed variables of type list, elementwise input prohibited*)
wneuper@59595:   typedecl str     (* structured variables                                        *)
wneuper@59595:   typedecl toreal  (* var with undef real value: forces typing                    *)
wneuper@59595:   typedecl toreall (* var with undef real list value: forces typing               *)
wneuper@59595:   typedecl tobooll (* var with undef bool list value: forces typing               *)
wneuper@59595:   typedecl unknow  (* input without dsc in fmz=[]                                 *)
wneuper@59595:   typedecl cpy     (* copy-named variables identified by .._0, .._i .._' in pbt   *)
wneuper@59595: 
walther@59951: subsection \<open>consts for general descriptors of input in the specify-phase\<close>
wneuper@59595: 
wneuper@59595: consts
wneuper@59595: (*TODO.180331: review for localisation of model-patterns and of method's guards*)
wneuper@59595:   someList       :: "'a list => unl" (*not for elementwise input, eg. inssort*)
wneuper@59595: 
wneuper@59595:   additionalRels :: "bool list => una"
Walther@60460:   boundVariable    :: "real => una"
Walther@60460:   FunctionVariable :: "real => una"
wneuper@59595:   derivative     :: "real => una"
wneuper@59595:   equalities     :: "bool list => tobooll" (*WN071228 see fixedValues*)
wneuper@59595:   equality       :: "bool => una"
wneuper@59595:   errorBound     :: "bool => nam"
Walther@60460:   ErrorBound     :: "bool => nam"
wneuper@59595:   
wneuper@59595:   fixedValues    :: "bool list => nam"
Walther@60460:   Constants      :: "bool list => nam"
wneuper@59595:   functionEq     :: "bool => una"     (*6.5.03: functionTerm -> functionEq*)
wneuper@59595:   antiDerivative :: "bool => una"
wneuper@59595:   functionOf     :: "real => una"
wneuper@59595: (*functionTerm   :: 'a => toreal 28.11.00*)
wneuper@59595:   functionTerm   :: "real => una"     (*6.5.03: functionTerm -> functionEq*)
wneuper@59595:   functionName   :: "real => una"
wneuper@59595:   interval       :: "real set => una"
Walther@60460:   Domain         :: "real set => una"
wneuper@59595:   maxArgument    :: "bool => toreal"
wneuper@59595:   maximum        :: "real => toreal"
Walther@60460:   Maximum        :: "real => toreal"
Walther@60460:   Extremum       :: "bool => toreal"
wneuper@59595:   
wneuper@59595:   relations      :: "bool list => una"
Walther@60460:   SideConditions :: "bool list => una"
wneuper@59595:   solutions      :: "bool list => toreall"
wneuper@59595:   solveFor       :: "real => una"
wneuper@59595:   differentiateFor:: "real => una"
wneuper@59595:   unknown        :: "'a => unknow"
Walther@60460:   valuesFor        :: "real list => toreall"
Walther@60460:   AdditionalValues :: "real list => toreall"
wneuper@59595: 
wneuper@59595:   intTestGiven   :: "int => una"
wneuper@59595:   realTestGiven  :: "real => una"
wneuper@59595:   realTestFind   :: "real => una"
wneuper@59595:   boolTestGiven  :: "bool => una"
wneuper@59595:   boolTestFind   :: "bool => una"
wneuper@59595: 
wneuper@59595: subsection \<open>Functions decking for descriptions of input in specify-phase\<close>
wneuper@59595: ML \<open>
wneuper@59595: \<close> ML \<open>
wneuper@59595: signature INPUT_DESCRIPT =
wneuper@59595: sig
walther@60125: (*type T          ..TODO rename*)
Walther@60766:   type descriptor
walther@59953: 
wenzelm@60223:   val for_real_list: term -> bool
walther@59953:   val for_list: term -> bool
wenzelm@60223: \<^isac_test>\<open>
wenzelm@60223:   val for_bool_list: term -> bool
wenzelm@60223:   val for_fun: term -> bool
wenzelm@60223:   val is_a: term -> bool 
wenzelm@60223: \<close>
walther@59953:   val split: term -> descriptor * term list
walther@59953:   val split': term * term -> term list
walther@59953:   val join: descriptor * term list -> term
walther@59953:   val join': descriptor * term list -> term
walther@59953:   val join''': descriptor * term list -> string
walther@59953:   val join'''': descriptor * term list -> term
wneuper@59595: end
wneuper@59595: \<close> ML \<open>
walther@59954: 
walther@59954: 
wneuper@59595: (**)
wneuper@59595: structure Input_Descript(**): INPUT_DESCRIPT =(**)
wneuper@59595: struct
wneuper@59595: (**)
walther@59953: 
Walther@60766: type descriptor = term; (*see Model_Def.descriptor*)
walther@59953: 
wneuper@59595: (* distinguish input to Model (deep embedding of terms as Isac's object language) *)
walther@60373: fun for_real_list (Const (_, Type(\<^type_name>\<open>fun\<close>, [Type(\<^type_name>\<open>list\<close>, [Type (\<^type_name>\<open>real\<close>, [])]), _]))) = true
walther@60373:   | for_real_list (Const (_, Type(\<^type_name>\<open>fun\<close>, [Type(\<^type_name>\<open>list\<close>, [Type (\<^type_name>\<open>real\<close>, [])]),_])) $ _) = true
walther@59953:   | for_real_list _ = false;
walther@60373: fun for_bool_list (Const (_, Type(\<^type_name>\<open>fun\<close>, [Type(\<^type_name>\<open>list\<close>, [Type (\<^type_name>\<open>bool\<close>, [])]), _]))) = true
walther@60373:   | for_bool_list (Const (_, Type(\<^type_name>\<open>fun\<close>, [Type(\<^type_name>\<open>list\<close>, [Type (\<^type_name>\<open>bool\<close>, [])]),_])) $ _) = true
walther@59953:   | for_bool_list _ = false;
wenzelm@60309: fun for_list (Const (_, Type(\<^type_name>\<open>fun\<close>, [Type(\<^type_name>\<open>list\<close>, _), _]))) = true
wenzelm@60309:   | for_list (Const (_, Type(\<^type_name>\<open>fun\<close>, [Type(\<^type_name>\<open>list\<close>, _), _])) $ _) = true
wneuper@59595:   (*WN:8.5.03: ???   TODO test/../scrtools.sml                ~~~~ ???*)
walther@59953:   | for_list _ = false;
walther@60373: fun for_fun (Const (_, Type(\<^type_name>\<open>fun\<close>, [_, Type(\<^type_name>\<open>unl\<close>, _)]))) = true
walther@59953:   | for_fun _ = false;
walther@60373: fun is_a (Const(_, Type(\<^type_name>\<open>fun\<close>, [_, Type(\<^type_name>\<open>nam\<close>, _)]))) = true
walther@60373:   | is_a (Const(_, Type(\<^type_name>\<open>fun\<close>, [_, Type(\<^type_name>\<open>una\<close>, _)]))) = true
walther@60373:   | is_a (Const(_, Type(\<^type_name>\<open>fun\<close>, [_, Type(\<^type_name>\<open>unl\<close>, _)]))) = true
walther@60373:   | is_a (Const(_, Type(\<^type_name>\<open>fun\<close>, [_, Type(\<^type_name>\<open>str\<close>, _)]))) = true
walther@60373:   | is_a (Const(_, Type(\<^type_name>\<open>fun\<close>, [_, Type(\<^type_name>\<open>toreal\<close>, _)]))) = true
walther@60373:   | is_a (Const(_, Type(\<^type_name>\<open>fun\<close>, [_, Type(\<^type_name>\<open>toreall\<close>, _)])))= true
walther@60373:   | is_a (Const(_, Type(\<^type_name>\<open>fun\<close>, [_, Type(\<^type_name>\<open>tobooll\<close>, _)])))= true
walther@60373:   | is_a (Const(_, Type(\<^type_name>\<open>fun\<close>, [_, Type(\<^type_name>\<open>unknow\<close>, _)])))= true
walther@60373:   | is_a (Const(_, Type(\<^type_name>\<open>fun\<close>, [_, Type(\<^type_name>\<open>cpy\<close>, _)])))= true
walther@59953:   | is_a _ = false;
wneuper@59595: 
walther@59953: (* special handling for lists. ?WN:14.5.03 ??!? *)
walther@59953: fun dest_list (d, ts) = 
walther@59953:   let fun dest t = 
walther@59953:     if for_list d andalso not (for_fun d) andalso not (is_Free t) (*..for pbt*)
walther@59953:     then TermC.isalist2list t
walther@59953:     else [t]
walther@59953:   in (flat o (map dest)) ts end;
wneuper@59599: 
walther@59997: (* take list-term apart w.r.t. handling elementwise input: @{term "[a, b]"} \<rightarrow> ["[a]", "[b]"] *)
walther@59953: fun take_apart t =
walther@59953:   let val elems = TermC.isalist2list t
walther@59953:   in map ((TermC.list2isalist (type_of (hd elems))) o single) elems end;
walther@59953: 
walther@59953: (* decompose an input into description, terms (ev. elems of lists),
walther@59953:     and the value for the problem-environment; inv to join   *)
walther@59953: fun split (t as d $ arg) =
walther@59953:     if is_a d
walther@59953:     then if for_list d andalso TermC.is_list arg andalso for_fun d |> not
walther@59953:       then (d, take_apart arg)
walther@59953:       else (d, [arg])
walther@59953:     else (TermC.empty, TermC.dest_list' t)
walther@59953:   | split t =
walther@59953:     let val t' as (h, _) = strip_comb t;
walther@59953:     in
walther@59953:       if is_a h
walther@59953:       then (h, dest_list t')
walther@59953:       else (TermC.empty, TermC.dest_list' t)
walther@59953:     end;
walther@59953: 
walther@59953: (* version returning ts only *)
walther@59953: fun split' (d, arg) = 
walther@59953:     if is_a d
walther@59953:     then if for_list d
walther@59953:       then if TermC.is_list arg
walther@59953: 	      then if for_fun d
walther@59953: 	        then ([arg])           (* e.g. someList [1,3,2]                 *)
walther@59953: 		      else (take_apart arg)  (* [a,b] --> SML[ [a], [b] ]SML          *)
walther@59953: 	      else ([arg])             (* a variable or metavariable for a list *)
walther@59953: 	     else ([arg])
walther@59953:     else (TermC.dest_list' arg)
walther@59953: 
Walther@60710: (* 
Walther@60710:   take list-term apart w.r.t. handling elementwise input: @{term "[a, b]"} \<rightarrow> ["[a]", "[b]"]
Walther@60710:     take_apart_inv: term list -> term
Walther@60710: *)
walther@59953: fun take_apart_inv ts = (* t = (take_apart_inv o take_apart) t *)
walther@59953:   let val elems = (flat o (map TermC.isalist2list)) ts;
walther@59953:   in TermC.list2isalist (type_of (hd elems)) elems end;
walther@59953: 
Walther@60661: fun script_parse str =
Walther@60661:   let
Walther@60661:     val ctxt = @{theory BaseDefinitions} |> Proof_Context.init_global
Walther@60661:   in
Walther@60661:     ParseC.term_opt ctxt str |> the
Walther@60661:   end;
walther@59953: val e_listReal = script_parse "[]::(real list)";
walther@59953: val e_listBool = script_parse "[]::(bool list)";
walther@59953: 
Walther@60478: (* revert split only for ts *)
walther@59953: fun join'''' (d, ts) = 
walther@59953:   if for_list d
walther@59953:   then if TermC.is_list (hd ts)
walther@59953: 	  then if for_fun d
walther@59953: 	    then (hd ts)             (* e.g. someList [1,3,2] *)
Walther@60766: 	    else (take_apart_inv ts) (* [ [a], [b] ] -> [a,b], see "type values"*)
walther@59953: 	  else (hd ts)               (* a variable or metavariable for a list *)
walther@59953:   else (hd ts);
walther@59953: fun join (d, []) = 
walther@59953:   	if for_real_list d
walther@59953:   	then (d $ e_listReal)
walther@59953:   	else if for_bool_list d then (d $ e_listBool) else d
walther@60265:   | join (d, ts) = 
walther@60265:     case \<^try>\<open> d $ (join'''' (d, ts))\<close> of
walther@60265:       SOME x => x
Walther@60678:     | NONE => raise ERROR ("join: " ^ UnparseC.term (ContextC.for_ERROR ()) d ^ " $ " ^ UnparseC.term (ContextC.for_ERROR ()) (hd ts)); 
walther@59953: fun join' (d, []) = 
walther@59953:     if for_real_list d
walther@59953:     then (d $ e_listReal)
walther@59953:     else if for_bool_list d then (d $ e_listBool) else d
walther@60265:   | join' (d, ts) = 
walther@60265:     case \<^try>\<open> d $ (join'''' (d, ts))\<close> of
walther@60265:       SOME x => x
Walther@60678:     | NONE => raise ERROR ("join': " ^ UnparseC.term (ContextC.for_ERROR ()) d ^ " $ " ^ UnparseC.term (ContextC.for_ERROR ()) (hd ts)); 
walther@59953: fun join''' (d, []) = 
walther@59953:     if for_real_list d
Walther@60678:     then UnparseC.term (ContextC.for_ERROR ()) (d $ e_listReal)
walther@59953:     else if for_bool_list d
Walther@60678:       then UnparseC.term (ContextC.for_ERROR ()) (d $ e_listBool)
Walther@60678:       else UnparseC.term (ContextC.for_ERROR ()) d
walther@60265:   | join''' (d, ts) = 
Walther@60678:     case \<^try>\<open> UnparseC.term (ContextC.for_ERROR ()) (d $ (join'''' (d, ts)))\<close> of
walther@60265:       SOME x => x
Walther@60678:     | NONE => raise ERROR ("join''': " ^ UnparseC.term (ContextC.for_ERROR ()) d ^ " $ " ^ UnparseC.term (ContextC.for_ERROR ()) (hd ts)); 
wneuper@59599: 
wneuper@59595: (**)end(**)
wneuper@59595: \<close> ML \<open>
wneuper@59595: \<close> ML \<open>
wneuper@59595: \<close> 
wneuper@59595: 
wneuper@59599: end