wneuper/isa: src/Tools/isac/BridgeJEdit/parseC.sml@28e2088e7cf1

     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

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

    14   (*tools*)

    15   val tokenize: string -> Token.T list

    16   val string_of_toks: Token.T list -> string

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

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

    20   (*Problem headline*)

    21   type problem_headline

    22   val problem_headline: problem_headline parser

    24   (*Specification*)

    25   type specification

    26   val specification: specification parser

    28   (*Model*)

    29   type model

    30   val model: model parser

    32   (*References*)

    33   type refs

    34   val refs_dummy: refs

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

    37   (*compose Specification*)

    38   type model_refs_dummy

    39   val model_refs_dummy: model_refs_dummy

    41   (*Tactics *)

    42   val tactic: (string * string) parser

    44   val exec_check_postcond: string * string list -> string

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

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

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

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

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

    51   (*Problem*)

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

    53   (* TODO for mutual recursion Problem .. steps

    54   val subproblem_msg:

    55   val exec_subproblem *)

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

    58 end

    60 (**)

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

    62 struct

    63 (**)

    65 (*** tools ***)

    67 fun tokenize str =

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

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

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

    75 (*** Problem headline ***)

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

    79 val problem_headline = Parse.$$$ "Problem" --

    80   Parse.$$$ "(" --

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

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

    83   Parse.$$$ ")"

    86 (*** Specification ***)

    88 (** Model **)

    90 type model =

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

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

    93          string) * string) * string list);

    94 val model = (

    95   Parse.$$$ "Model" --

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

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

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

    99     Parse.$$$ ":" --

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

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

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

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

   104 )

   106 (** References **)

   108 type refs =

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

   110 val refs_dummy =

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

   113 val references = (

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

   115     (Scan.optional

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

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

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

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

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

   121       )

   122       refs_dummy

   123     ))

   125 (** compose Specification **)

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

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

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

   130        []),

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

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

   134 type specification = (string * string) * model_refs_dummy

   135 val specification = (

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

   137     (Scan.optional

   138       (model -- references)

   139     )

   140     model_refs_dummy

   141 )

   143 (*** Tactics ***)

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

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

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

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

   150 (* see test/../Test_Parsers.thy \<open>|| requires arguments of equal type *)

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

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

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

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

   155 fun exec_check_postcond (str, path) =

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

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

   159   Parse.$$$ "Tactic" --

   160     (substitute >> exec_substitute ||

   161      rewrite_set_inst >> exec_rewrite_set_inst ||

   162      check_postcond >> exec_check_postcond

   163     )

   164   )

   167 (*** Problem ***)

   169 type problem =

   170   (((( problem_headline *

   171       ((string * string) * (model *

   172       ((string * string) * refs)))) *

   173     string) * string) * string list)

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

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

   178 (** )

   179 fun subproblem_msg

   180   (((((((((s1, s2), s3), s4), strs0), s5),

   181          ((s6, s7),

   182           (((((((((((((((s11, ((s12, s13), s14)), s15), s16), s17), strs18), s19), s20), strs21), s22),

   183                 s23), s24), s25), s26), strs27),

   184            ((s31, s32), ((((((((s30, s33), s34), s35), s36), strs37), s38), s39), strs40)))))

   185        , s51), s61), strs71) = "EXEC IMMEDIATELY step_subproblem:\n" ^

   186 "  (((((((((" ^ s1 ^ ", " ^ s2 ^ "), " ^ s3 ^ "), " ^ s4 ^ "), " ^ LibraryC.strs2str strs0 ^ "), " ^ s5 ^ "),\n" ^

   187 "         ((" ^ s6 ^ ", " ^ s7 ^ "),\n" ^

   188 "          (((((((((((((((" ^ s11 ^ ", ((" ^ s12 ^ ", " ^ s13 ^ "), " ^ s14 ^ ")), " ^ s15 ^ "), " ^ s16 ^ "), " ^ s17 ^ "), " ^ LibraryC.strs2str strs18 ^ "), " ^ s19 ^ "), " ^ s20 ^ "), " ^ LibraryC.strs2str strs21 ^ "), " ^ s22 ^ "),\n" ^

   189                  s23 ^ "), " ^ s24 ^ "), " ^ s25 ^ "), " ^ s26 ^ "), " ^ LibraryC.strs2str strs27 ^ "),\n" ^

   190 "           ((" ^ s31 ^ ", " ^ s32 ^ "), ((((((((" ^ s30 ^ ", " ^ s33 ^ "), " ^ s34 ^ "), " ^ s35 ^ "), " ^ s36 ^ "), " ^ LibraryC.strs2str strs37 ^ "), " ^ s38 ^ "), " ^ s39 ^ "), " ^ LibraryC.strs2str strs40 ^ ")))))\n" ^

   191 "       , " ^ s51 ^ "), " ^ s61 ^ "), " ^ LibraryC.strs2str strs71 ^ ")";

   192 fun exec_subproblem

   193   (((((((((s1, s2), s3), s4), strs0), s5),

   194          ((s6, s7),

   195           (((((((((((((((s11, ((s12, s13), s14)), s15), s16), s17), strs18), s19), s20), strs21), s22),

   196                 s23), s24), s25), s26), strs27),

   197            ((s31, s32), ((((((((s30, s33), s34), s35), s36), strs37), s38), s39), strs40)))))

   198        , s51), s61), strs71) = subproblem_msg

   199   (((((((((s1, s2), s3), s4), strs0), s5),

   200          ((s6, s7),

   201           (((((((((((((((s11, ((s12, s13), s14)), s15), s16), s17), strs18), s19), s20), strs21), s22),

   202                 s23), s24), s25), s26), strs27),

   203            ((s31, s32), ((((((((s30, s33), s34), s35), s36), strs37), s38), s39), strs40)))))

   204        , s51), s61), strs71);

   205 ( **)

   207 val problem =

   208   problem_headline --

   209     specification --

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

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

   212       (Scan.repeat (

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

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

   215       ))

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

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

   220 (**)end(**)

author	Walther Neuper <walther.neuper@jku.at>
	Fri, 14 Aug 2020 12:36:33 +0200
changeset 60045	28e2088e7cf1
parent 60044	004bbb5d4417
child 60087	5e14a116524c
permissions	-rw-r--r--