(*  Title:      Tools/isac/BridgeJEdit/parseC.sml

    Author:     Walther Neuper, JKU Linz

    (c) due to copyright terms

Outer token syntax for Isabelle/Isac.

*)

signature PARSE_C =

sig

  type problem

  val problem: problem parser

  type problem_headline

  val problem_headline: problem_headline parser

(* exclude "Problem" from parsing * )

  val read_out_headline: headline_string * Token.T list -> ThyC.id * Problem.id

( * exclude "Problem" from parsing *)

  val read_out_headline: problem_headline -> ThyC.id * Problem.id

(* exclude "Problem" from parsing *)

  val read_out_problem: problem -> P_Spec.record

  val tokenize_formalise: Position.T -> string -> Fdl_Lexer.T list * Fdl_Lexer.chars

  type form_model = TermC.as_string list;

  type form_refs = (((((string * ThyC.id) * string) * Problem.id) * string) * MethodC.id) * string

  type form_model_refs = 

    (((((string * string) * form_model) * string) * form_refs) * string) * string

  val read_out_formalise: form_model_refs -> Formalise.T list

  (*RENAME TO parse_formalise..*)

  val formalisation: Fdl_Lexer.T list -> form_model_refs * Fdl_Lexer.T list;

(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)

  val tokenize: string -> Token.T list

  val string_of_toks: Token.T list -> string

  val parse: (Token.T list -> 'a * Token.T list) -> Token.T list -> 'a * Token.T list

(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )

  (*Model*)

  type model

  val model: model parser

  (*References*)

  type refs

  type model_refs_dummy = model * ((string * string) * refs)

  val model_refs_dummy: model_refs_dummy

  val references: ((string * string) * refs) parser

  val refs_dummy: refs

  (*Specification*)

  type specification = (string * string) * model_refs_dummy

  val specification: specification parser

  (*Tactics *)

  val check_postcond: (string * string list) parser

  val rewrite_set_inst: ((string * string) * string) parser

  val substitute: ((string * string) * string) parser

  val exec_check_postcond: string * string list -> string

  val exec_rewrite_set_inst: (string * string) * string -> string

  val exec_substitute: (string * string) * string -> string

  val tactic: Token.T list -> (string * string) * Token.T list

  (*Steps*)

  val steps: (string * (string * string)) list parser

  val exec_step_term: string * (string * string) -> string

  val steps_subpbl: string list parser

  (*Problem*)

  type body

  val body: body parser

  val body_dummy: body

  val tokenize_string: Fdl_Lexer.chars -> Fdl_Lexer.T * Fdl_Lexer.chars

  val scan: Fdl_Lexer.chars -> Fdl_Lexer.T list * Fdl_Lexer.chars

  val parse_form_refs: Fdl_Lexer.T list -> form_refs * Fdl_Lexer.T list;

  val parse_form_model: Fdl_Lexer.T list -> string list * Fdl_Lexer.T list;

  val parse_string         : Fdl_Lexer.T list -> string * Fdl_Lexer.T list;

( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)

end

(**)

structure ParseC(**): PARSE_C(**) =

struct

(**)

(**** Tools ****)

fun tokenize str =

  filter Token.is_proper (Token.explode (Thy_Header.get_keywords' @{context}) Position.none str)

fun parse parser toks = Scan.finite Token.stopper (Scan.error parser) toks

fun string_of_toks toks = fold (curry op ^) (map Token.unparse toks |> rev |> separate ", ") "";

(**** parse Calculation ****)

(*** Problem headline ***)

(* exclude "Problem" from parsing * )

type problem_headline = (((((string * string) * string) * string) * string list) * string)

( * exclude "Problem" from parsing *)

type problem_headline = (((string * ThyC.id) * string) * Problem.id) * string

(* exclude "Problem" from parsing *)

val problem_headline = (*Parse.$$$ "Problem" --*)

  Parse.$$$ "(" --

    Parse.string -- Parse.$$$ "," --

      (Parse.$$$ "[" |-- Parse.list1 Parse.string --| Parse.$$$ "]") --

  Parse.$$$ ")"

(* exclude "Problem" from parsing * )

fun string_of_headline ((((left, thy_id: ThyC.id), comm), pbl_id), right) =

      left ^ thy_id ^ comm ^ Problem.id_to_string pbl_id ^ right

fun read_out_headline ((((("(", thy_id), ","), pbl_id), ")"), []) = (thy_id, pbl_id)

  | read_out_headline (hdl, toks) =

      raise ERROR ("read_out_headline NOT for: (" ^ string_of_headline hdl ^ ", " ^

        string_of_toks toks ^ ")")

( * exclude "Problem" from parsing *)

fun read_out_headline ((((("(", thy_id), ","), pbl_id), ")")) = (thy_id, pbl_id)

  | read_out_headline arg =

      (@{print} {a = "read_out_headline with", arg = arg}; raise ERROR "read_out_headline")

(**)

(* used if at least "Problem (thy_id, pbl_id)" has been input *)

fun read_out_problem ((((((

    "(", thy_id), ","), pbl_id), ")"), (((((

      _(*"Specification"*), _(*":"*)), (((((((((((((((

        _(*"Model"*), (("", ""), "")), _(*":"*)),

          _(*"Given"*)), _(*":"*)), givens),

          _(*"Where"*)), _(*":"*)), wheres),

          _(*"Find"*)), _(*":"*)), find),

          _(*"Relate"*)), _(*":"*)), relates), ((

        _(*"References"*), _(*":"*)), ((((((((

          _(*"RTheory"*), _(*":"*)), rthy_id),

          _(*"RProblem"*)), _(*":"*)), rpbl_id),

          _(*"RMethod"*)), _(*":"*)), rmet_id)))),

        _(*"Solution"*)), _(*":"*)),

          _(*[]*))),

       _(*""*)) =

    {thy_id = thy_id, pbl_id = pbl_id,

      givens = givens, wheres = wheres, find = find, relates = relates,

      rthy_id = rthy_id, rpbl_id = rpbl_id, rmet_id = rmet_id}

  | read_out_problem arg =

    (@{print} {a = "read_out_problem called with", arg = arg};

      raise ERROR "read_out_problem called with")

(*** Specification ***)

(** Model **)

type model =

  ((((((((((((((string * ((string * string) * string)) * string) * string) * string) *

      string list) * string) * string) * string list) * string) * string) * string) *

         string) * string) * string list);

val model = (

  Parse.keyword_improper "Model" --

    (Scan.optional (*.. show, whether the Model refers to RProblem or to RMethod *)

      (Parse.$$$ "(" -- (Parse.$$$ "RProblem" || Parse.$$$ "RMethod") -- Parse.$$$ ")")

      (("", ""), "") ) --

    Parse.$$$ ":" --

    Parse.command_name "Given" -- Parse.$$$ ":" -- Parse.list1 Parse.term --

    Parse.keyword_improper "Where" -- Parse.$$$ ":" -- Parse.list Parse.term --

    Parse.command_name "Find" -- Parse.$$$ ":" -- Parse.term --

    Parse.command_name "Relate" -- Parse.$$$ ":" -- Parse.list Parse.term

)

(** References **)

type refs =

  ((((((((string * string) * string) * string) * string) * string list) * string) * string) * string list)

val refs_dummy =

  (((((((("", ""), ""), ""), ""), []), ""), ""), [])

val references = (

  Parse.$$$ "References" -- Parse.$$$ ":" (**) --

    (Scan.optional 

      (Parse.$$$ "RTheory" -- Parse.$$$ ":" -- Parse.string (**) --

      Parse.$$$ "RProblem" -- Parse.$$$ ":" (**) --

        (Parse.$$$ "[" |-- Parse.list1 Parse.string --| Parse.$$$ "]") (**) --

      Parse.$$$ "RMethod" -- Parse.$$$ ":" (**) --

        (Parse.$$$ "[" |-- Parse.list1 Parse.string --| Parse.$$$ "]")

      )

      refs_dummy

    ))

(** compose Specification **)

type model_refs_dummy = (model * ((string * string) * refs))

val model_refs_dummy = ((((((((((((((("", (("", ""), "")), ""), ""), ""),

    []), ""), ""), []), ""), ""), ""), ""), ""),

       []),

      (("", ""), (((((((("", ""), ""), ""), ""), []),

        ""), ""), [])))

type specification = (string * string) * model_refs_dummy

val specification = (

  (Parse.keyword_improper "Specification" -- Parse.$$$ ":") --

    (Scan.optional

      (model -- references)

    )

    model_refs_dummy

    );

(*** Solution ***)

(** Tactics **)

val substitute = Parse.reserved "Substitute" -- Parse.term -- Parse.term;

val rewrite_set_inst = Parse.reserved "Rewrite_Set_Inst" -- Parse.term -- Parse.name;

val check_postcond = Parse.reserved "Check_Postcond" --

  (Parse.$$$ "[" |-- Parse.list1 Parse.name --| Parse.$$$ "]");

(* see test/../Test_Parsers.thy || requires arguments of equal type *)

fun exec_substitute ((str, tm), bdv) =

  "EXEC IMMEDIATELY: " ^ str ^ " " ^ (*UnparseC.term*) tm ^ " " ^ (*UnparseC.term*) bdv;

fun exec_rewrite_set_inst ((str, tm), id) =

  "EXEC IMMEDIATELY: " ^ str ^ " " ^ (*UnparseC.term*) tm ^ " " ^ (*Problem.id_to_string*) id;

fun exec_check_postcond (str, path) =

  "EXEC IMMEDIATELY: " ^ str ^ " " ^ (*Problem.id_to_string*)fold (curry op ^) path "";

val tactic = ( (* incomplete list of tactics *)

  Parse.$$$ "Tactic" --

    (substitute >> exec_substitute ||

     rewrite_set_inst >> exec_rewrite_set_inst ||

     check_postcond >> exec_check_postcond

    )

  )

(** Step of term + tactic**)

val steps = (Scan.repeat (Parse.term -- (Scan.optional tactic ("", ""))))

fun exec_step_term (tm, (tac1, tac2)) =

  "EXEC IMMEDIATELY step_term: " ^ (*UnparseC.term*) tm ^ " (" ^ tac1 ^ ", " ^ tac2 ^ ")";

val steps_subpbl =

  Scan.repeat (

    ((Parse.term -- (Scan.optional tactic ("", ""))) >> exec_step_term) (** ) ||

    (problem >> exec_subproblem) ( **)

  )

(** Body **)

type body = (((((string * string) *

  (((((((((((((((string * ((string * string) * string)) * string) * string) * string) * string list) * string) * string) * string list) * string) * string) * string) * string) * string) * string list) *

    ((string * string) * ((((((((string * string) * string) * string) * string) * string list) * string) * string) * string list)))) *

        string) * string) * string list)

val body_dummy = ((((("", ""),

  ((((((((((((((("", (("", ""), "")), ""), ""), ""), []), ""), ""), []), ""), ""), ""), ""), ""), []),

    (("", ""), (((((((("", ""), ""), ""), ""), []), ""), ""), [])))),

      ""), ""), [])

val body =

  specification --

  Parse.$$$ "Solution" -- Parse.$$$ ":" --

  (*/----- this will become "and steps".. *)

    (Scan.repeat (

      ((Parse.term -- (Scan.optional tactic ("", ""))) >> exec_step_term)  (** ) ||

       (problem >> exec_subproblem)  ( *exec_* make types equal for both args of ||*)

    ))

  (*\----- ..this will become "and steps"

    see Test_Parse_Isac subsubsection \<open>trials on recursion stopped\<close> *)

(*** Problem ***)

(* exclude "Problem" from parsing * )

type problem =

  (((((((string * string) * string) * string) * string list) * string) *

    (((((string * string) *

      (((((((((((((((string * ((string * string) * string)) * string) * string) * string) *

        string list) * string) * string) * string list) * string) *

        string) * string) * string) * string) * string list) *

        ((string * string) *

          ((((((((string * string) * string) * string) * string) * string list) * string) *

            string) * string list)))) *

      string) * string) * string list)) *

    string)

( * exclude "Problem" from parsing *)

type problem =

  (((((string * string) * string) * string list) * string) *

    (((((string * string) *

      (((((((((((((((string * ((string * string) * string)) * string) * string) * string) *

        string list) * string) * string) * string list) * string) *

        string) * string) * string) * string) * string list) *

        ((string * string) *

          ((((((((string * string) * string) * string) * string) * string list) * string)

            * string) * string list)))) *

      string) * string) * string list)) *

    string

(* exclude "Problem" from parsing *)

val problem =

  problem_headline --

    (Scan.optional body) body_dummy --

  (Scan.optional Parse.term) ""

(**** parse Formalise ****)

(*** Tokenizer, from HOL/SPARK/Tools/fdl_lexer.ML ***)

val tokenize_string = Fdl_Lexer.$$$ "\"" |-- Fdl_Lexer.!!! "unclosed string" (*2*)

  (Scan.repeat (Scan.unless (Fdl_Lexer.$$$ "\"") Fdl_Lexer.any) --| Fdl_Lexer.$$$ "\"") >>

    Fdl_Lexer.make_token Fdl_Lexer.Comment(*!!!*);

val scan =

  Scan.repeat (Scan.unless (Scan.one Fdl_Lexer.is_char_eof)

    (Fdl_Lexer.!!! "bad input"

       (   tokenize_string           (*.. this must be first *)

        ||Scan.max Fdl_Lexer.leq_token

             (Scan.literal Fdl_Lexer.lexicon >> Fdl_Lexer.make_token Fdl_Lexer.Keyword)

             (   Fdl_Lexer.long_identifier >> Fdl_Lexer.make_token Fdl_Lexer.Long_Ident

              || Fdl_Lexer.identifier >> Fdl_Lexer.make_token Fdl_Lexer.Ident)

       ) --|

     Fdl_Lexer.whitespace) );

fun tokenize_formalise pos str =

  (Scan.finite Fdl_Lexer.char_stopper

    (Scan.error scan) (Fdl_Lexer.explode_pos str pos));

(*** the parser from HOL/SPARK/Tools/fdl_parser.ML ***)

type form_model = TermC.as_string list;

type form_refs = (((((string * string) * string) * string list) * string) * string list) * string

type form_model_refs = ((((((string * string) * form_model) * string) *

  ((((((string * ThyC.id) * string) * Problem.id) * string) * MethodC.id) * string)) * 

    string) * string)

type formalise = (((((string * string) * form_model) * string) *

  ((((((string * ThyC.id) * string) * Problem.id) * string) * MethodC.id) * string)) *

    string) * string;

val parse_string = Fdl_Parser.group "string"

  (Scan.one (fn t => Fdl_Lexer.kind_of t = Fdl_Lexer.Comment) >>

     Fdl_Lexer.content_of);

val parse_form_model =

  (Fdl_Parser.$$$ "[" |-- Fdl_Parser.!!! (

    Fdl_Parser.list1 parse_string --| 

  Fdl_Parser.$$$ "]"));

val parse_form_refs = 

  Fdl_Parser.$$$ "(" --

    parse_string --                     (* "Biegelinie" *)

  Fdl_Parser.$$$ "," --

    (Fdl_Parser.$$$ "[" |-- Fdl_Parser.!!! (

      Fdl_Parser.list1 parse_string --| (* ["Biegelinien"] *)

    Fdl_Parser.$$$ "]")) --

  Fdl_Parser.$$$ "," --

    (Fdl_Parser.$$$ "[" |-- Fdl_Parser.!!! (

      Fdl_Parser.list1 parse_string --| (* ["IntegrierenUndKonstanteBestimmen2"] *)

    Fdl_Parser.$$$ "]")) --

  Fdl_Parser.$$$ ")";

(*val parse_formalise =   KEEP IDENTIFIERS CLOSE TO SPARK..*)

val formalisation =

  Fdl_Parser.!!! (

    Fdl_Parser.$$$ "[" --

      Fdl_Parser.$$$ "(" --

        parse_form_model --

      Fdl_Parser.$$$ "," --

        parse_form_refs --

      Fdl_Parser.$$$ ")" --

    Fdl_Parser.$$$ "]");

fun read_out_formalise ((((( (

  "[", 

    "("),

      form_model: TermC.as_string list),

    ","), ((((((

      "(", 

        thy_id: ThyC.id), 

      ","), 

        probl_id: Problem.id), 

      ","), 

        meth_id: MethodC.id), 

      ")")),

    ")"),

  "]") = [(form_model, (thy_id, probl_id, meth_id))]

| read_out_formalise _ =

  raise ERROR "read_out_formalise: WRONGLY parsed";

(**)end(*struct*)