(* Title:  BaseDefinitions/parseC..sml

   Author: Walther Neuper

   (c) due to copyright terms

*)

signature PARSE_ISAC =

sig

  val term_position: Proof.context -> string * Position.T -> term

  val pattern_position: Proof.context -> string * Position.T -> term

  val term_opt: Proof.context -> string -> term option

  val patt_opt: theory -> string -> term option

  val parse_test: Proof.context -> string -> term

  val parse_patt_test: theory -> string -> term

  val adapt_term_to_type: Proof.context -> term -> term

  val adapt_to_type_real: term -> term

  val adapt_to_type_int: term -> term

end

(**)

structure ParseC(**): PARSE_ISAC(**) =

struct

(**)

(** parse term with feedback by PIDE **)

fun term_position ctxt (str, pos) =

  Syntax.read_term ctxt str

    handle ERROR msg => error (msg ^ Position.here pos)

    (*this exception is caught by PIDE to show "msg" at the proper location on screen*)

fun pattern_position ctxt (str, pos) =

  Proof_Context.read_term_pattern ctxt str

    handle ERROR msg => error (msg ^ Position.here pos)

    (*this exception is caught by PIDE to show "msg" at the proper location on screen*)

(** parse term internally **)

fun term_opt ctxt str = \<^try>\<open>Syntax.read_term ctxt str\<close>;

fun patt_opt thy str = \<^try>\<open>Proof_Context.read_term_pattern (Proof_Context.init_global thy) str\<close>;

(** adapt type of pre-typed terms to current context **)

(* 

  adapt type of terms with most general type to a more specific one.

  TODO: clarify how to decide by use of data from the current context.

*)

fun T_a2real (Type (s, [])) = 

    if s = "'a" orelse s = "'b" orelse s = "'c" then HOLogic.realT else Type (s, [])

  | T_a2real (Type (s, Ts)) = Type (s, map T_a2real Ts)

  | T_a2real (TFree (s, srt)) = 

    if s = "'a" orelse s = "'b" orelse s = "'c" then HOLogic.realT else TFree (s, srt)

  | T_a2real (TVar (("DUMMY", _), _)) = HOLogic.realT

  | T_a2real (TVar ((s, i), srt)) = 

    if s = "'a" orelse s = "'b" orelse s = "'c" then HOLogic.realT else TVar ((s, i), srt)

(*val adapt_to_type_real: term -> term*)

fun adapt_to_type_real (Const( s, T)) = (Const( s, T_a2real T)) 

  | adapt_to_type_real (Free( s, T)) = (Free( s, T_a2real T))

  | adapt_to_type_real (Var( n, T)) = (Var( n, T_a2real T))

  | adapt_to_type_real (Bound i) = (Bound i)

  | adapt_to_type_real (Abs(s,T,t)) = Abs(s, T, adapt_to_type_real t)

  | adapt_to_type_real (t1 $ t2) = (adapt_to_type_real t1) $ (adapt_to_type_real t2);

(*val adapt_to_type_int: term -> term*)

fun adapt_to_type_int _ = raise ERROR "Model_Pattern.adapt_to_type NOT implemented for HOLogic.intT"

fun adapt_term_to_type ctxt t =

  let

    val choice = ctxt |> K HOLogic.realT (*clarify how ctxt can be used here*)

  in

    if choice = HOLogic.realT then adapt_to_type_real t

    else if choice = HOLogic.intT then adapt_to_type_int t

    else raise ERROR "TermC.adapt_to_type only implemented for HOLogic.realT"

  end

(** parse term in test/ **)

(*

  This bypasses building ctxt at the begin of a calculation

  and thus borrows adapt_to_type (used for adapting pre-parsed terms from Know_Store).

  These identifiers have been crudely query\replaced and

  shall eventually be brought in accordance with src/.

*)

fun parse_test ctxt str = str 

  |> Syntax.read_term_global (Proof_Context.theory_of ctxt)

  |> adapt_term_to_type ctxt

fun parse_patt_test thy str = (thy, str)

  |>> Proof_Context.init_global

  |-> Proof_Context.read_term_pattern

  |> adapt_term_to_type (Proof_Context.init_global thy)

(**)end(*struct*)