wneuper/isa: src/Tools/isac/BridgeJEdit/parseC.sml@74965ce81297

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

     2     Author:     Walther Neuper, JKU Linz

     3     (c) due to copyright terms

     5 Outer token syntax for Isabelle/Isac.

     6 *)

     8 signature PARSE_C =

     9 sig

    10   type problem

    11   val problem: problem parser

    12   type problem_headline

    13   val problem_headline: problem_headline parser

    15 (* exclude "Problem" from parsing * )

    16   val read_out_headline: headline_string * Token.src -> ThyC.id * Problem.id

    17 ( * exclude "Problem" from parsing *)

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

    19 (* exclude "Problem" from parsing *)

    20   val read_out_problem: problem -> P_Spec.record

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

    24   type form_model = TermC.as_string list;

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

    26   type form_model_refs =

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

    29   val read_out_formalise: form_model_refs -> Formalise.T list

    30   (*RENAME TO parse_formalise..*)

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

    33 \<^isac_test>\<open>

    34   val tokenize: string -> Token.src

    35   val string_of_toks: Token.src -> string

    36   val parse: (Token.src -> 'a * Token.src) -> Token.src -> 'a * Token.src

    38   (*Model*)

    39   type model

    40   val model: model parser

    42   (*References*)

    43   type refs

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

    45   val model_refs_dummy: model_refs_dummy

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

    47   val refs_dummy: refs

    49   (*Specification*)

    50   type specification = (string * string) * model_refs_dummy

    51   val specification: specification parser

    53   (*Tactics *)

    54   val check_postcond: (string * string list) parser

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

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

    57   val exec_check_postcond: string * string list -> string

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

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

    61   val tactic: Token.src -> (string * string) * Token.src

    63   (*Steps*)

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

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

    66   val steps_subpbl: string list parser

    68   (*Problem*)

    69   type body

    70   val body: body parser

    71   val body_dummy: body

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

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

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

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

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

    78 \<close>

    79 end

    81 (**)

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

    83 struct

    84 (**)

    86 (**** Tools ****)

    88 \<^isac_test>\<open>

    89 fun tokenize str =

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

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

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

    95 \<close>

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

    99 (*** Problem headline ***)

   101 (* exclude "Problem" from parsing * )

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

   103 ( * exclude "Problem" from parsing *)

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

   105 (* exclude "Problem" from parsing *)

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

   107   Parse.$$$ "(" --

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

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

   110   Parse.$$$ ")"

   112 (* exclude "Problem" from parsing * )

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

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

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

   116   | read_out_headline (hdl, toks) =

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

   118         string_of_toks toks ^ ")")

   119 ( * exclude "Problem" from parsing *)

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

   121   | read_out_headline arg =

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

   123 (**)

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

   126 fun read_out_problem ((((((

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

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

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

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

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

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

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

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

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

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

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

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

   139           _(*[]*))),

   140        _(*""*)) =

   141     {thy_id = thy_id, pbl_id = pbl_id,

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

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

   144   | read_out_problem arg =

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

   146       raise ERROR "read_out_problem called with")

   149 (*** Specification ***)

   151 (** Model **)

   153 type model =

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

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

   156          string) * string) * string list);

   157 val model = (

   158   Parse.command_name "Model" --

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

   160       (Parse.$$$ "(" --

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

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

   163     Parse.$$$ ":" --

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

   165     Parse.command_name "Where" -- Parse.$$$ ":" -- Parse.list Parse.term --

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

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

   168 )

   170 (** References **)

   172 type refs =

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

   174 val refs_dummy =

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

   177 val references = (

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

   179     (Scan.optional

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

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

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

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

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

   185       )

   186       refs_dummy

   187     ))

   189 (** compose Specification **)

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

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

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

   194        []),

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

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

   198 type specification = (string * string) * model_refs_dummy

   199 val specification = (

   200   (Parse.command_name "Specification" -- Parse.$$$ ":") --

   201     (Scan.optional

   202       (model -- references)

   203     )

   204     model_refs_dummy

   205     );

   208 (*** Solution ***)

   209 (** Tactics **)

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

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

   213 val check_postcond = Parse.reserved "Check_Postcond" --

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

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

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

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

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

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

   221 fun exec_check_postcond (str, path) =

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

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

   225   Parse.$$$ "Tactic" --

   226     (substitute >> exec_substitute ||

   227      rewrite_set_inst >> exec_rewrite_set_inst ||

   228      check_postcond >> exec_check_postcond

   229     )

   230   )

   232 (** Step of term + tactic**)

   234 \<^isac_test>\<open>

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

   236 \<close>

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

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

   240 \<^isac_test>\<open>

   241 val steps_subpbl =

   242   Scan.repeat (

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

   244     (problem >> exec_subproblem) ( **)

   245   )

   246 \<close>

   248 (** Body **)

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

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

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

   253         string) * string) * string list)

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

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

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

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

   258 val body =

   259   specification --

   260   Parse.command_name "Solution" -- Parse.$$$ ":" --

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

   262     (Scan.repeat (

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

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

   265     ))

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

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

   270 (*** Problem ***)

   271 (* exclude "Problem" from parsing * )

   272 type problem =

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

   274     (((((string * string) *

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

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

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

   278         ((string * string) *

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

   280             string) * string list)))) *

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

   282     string)

   283 ( * exclude "Problem" from parsing *)

   284 type problem =

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

   286     (((((string * string) *

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

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

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

   290         ((string * string) *

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

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

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

   294     string

   295 (* exclude "Problem" from parsing *)

   296 val problem =

   297   problem_headline --

   298     (Scan.optional body) body_dummy --

   299   (Scan.optional Parse.term) ""

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

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

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

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

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

   310 val scan =

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

   312     (Fdl_Lexer.!!! "bad input"

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

   314         ||Scan.max Fdl_Lexer.leq_token

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

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

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

   318        ) --|

   319      Fdl_Lexer.whitespace) );

   321 fun tokenize_formalise pos str =

   322   (Scan.finite Fdl_Lexer.char_stopper

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

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

   328 type form_model = TermC.as_string list;

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

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

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

   332     string) * string)

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

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

   335     string) * string;

   337 val parse_string = Fdl_Parser.group "string"

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

   339      Fdl_Lexer.content_of);

   341 val parse_form_model =

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

   343     Fdl_Parser.list1 parse_string --|

   344   Fdl_Parser.$$$ "]"));

   346 val parse_form_refs =

   347   Fdl_Parser.$$$ "(" --

   348     parse_string --                     (* "Biegelinie" *)

   349   Fdl_Parser.$$$ "," --

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

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

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

   353   Fdl_Parser.$$$ "," --

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

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

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

   357   Fdl_Parser.$$$ ")";

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

   360 val formalisation =

   361   Fdl_Parser.!!! (

   362     Fdl_Parser.$$$ "[" --

   363       Fdl_Parser.$$$ "(" --

   364         parse_form_model --

   365       Fdl_Parser.$$$ "," --

   366         parse_form_refs --

   367       Fdl_Parser.$$$ ")" --

   368     Fdl_Parser.$$$ "]");

   370 fun read_out_formalise ((((( (

   371   "[",

   372     "("),

   373       form_model: TermC.as_string list),

   374     ","), ((((((

   375       "(",

   376         thy_id: ThyC.id),

   377       ","),

   378         probl_id: Problem.id),

   379       ","),

   380         meth_id: MethodC.id),

   381       ")")),

   382     ")"),

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

   384 | read_out_formalise _ =

   385   raise ERROR "read_out_formalise: WRONGLY parsed";

   387 (**)end(*struct*)

author	wneuper <walther.neuper@jku.at>
	Thu, 29 Apr 2021 14:13:11 +0200
changeset 60269	74965ce81297
parent 60223	740ebee5948b
child 60431	5d1d51d29ad6
permissions	-rw-r--r--