src/Pure/ProofGeneral/pgip_tests.ML
author wenzelm
Fri, 18 Jan 2013 16:20:09 +0100
changeset 50974 55f8bd61b029
parent 29606 fedb8be05f24
permissions -rw-r--r--
added "tasks_proof" statistics, via slighly odd global reference Future.forked_proofs (NB: Future.report_status is intertwined with scheduler thread);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     1
(*  Title:      Pure/ProofGeneral/pgip_tests.ML
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     2
    Author:     David Aspinall
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     3
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     4
A test suite for the PGIP abstraction code (in progress).
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21867
diff changeset
     5
Run to provide some mild insurance against breakage in Isabelle here.
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     6
*)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     7
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     8
(** pgip_types.ML **)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     9
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    10
local
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    11
fun asseq_p toS a b =
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    12
    if a=b then ()
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    13
    else error("PGIP test: expected these two values to be equal:\n" ^
28020
1ff5167592ba get rid of tabs;
wenzelm
parents: 26541
diff changeset
    14
               (toS a) ^"\n and: \n" ^ (toS b))
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    15
26541
14b268974c4b XML.string_of, XML.parse;
wenzelm
parents: 25275
diff changeset
    16
val asseqx = asseq_p XML.string_of
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    17
val asseqs = asseq_p I
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    18
val asseqb = asseq_p (fn b=>if b then "true" else "false")
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    19
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    20
open PgipTypes;
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    21
in
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    22
26541
14b268974c4b XML.string_of, XML.parse;
wenzelm
parents: 25275
diff changeset
    23
val _ = asseqx (pgiptype_to_xml Pgipnull) (XML.parse "<pgipnull/>");
14b268974c4b XML.string_of, XML.parse;
wenzelm
parents: 25275
diff changeset
    24
val _ = asseqx (pgiptype_to_xml Pgipbool) (XML.parse "<pgipbool/>");
14b268974c4b XML.string_of, XML.parse;
wenzelm
parents: 25275
diff changeset
    25
val _ = asseqx (pgiptype_to_xml (Pgipint (NONE,NONE))) (XML.parse "<pgipint/>");
14b268974c4b XML.string_of, XML.parse;
wenzelm
parents: 25275
diff changeset
    26
val _ = asseqx (pgiptype_to_xml (Pgipint (SOME 5,SOME 7))) (XML.parse "<pgipint min='5' max='7'/>");
14b268974c4b XML.string_of, XML.parse;
wenzelm
parents: 25275
diff changeset
    27
val _ = asseqx (pgiptype_to_xml (Pgipint (NONE,SOME 7))) (XML.parse "<pgipint max='7'/>");
14b268974c4b XML.string_of, XML.parse;
wenzelm
parents: 25275
diff changeset
    28
val _ = asseqx (pgiptype_to_xml (Pgipint (SOME ~5,NONE))) (XML.parse "<pgipint min='-5'/>");
14b268974c4b XML.string_of, XML.parse;
wenzelm
parents: 25275
diff changeset
    29
val _ = asseqx (pgiptype_to_xml Pgipstring) (XML.parse "<pgipstring/>");
14b268974c4b XML.string_of, XML.parse;
wenzelm
parents: 25275
diff changeset
    30
val _ = asseqx (pgiptype_to_xml (Pgipconst "radio1"))  (XML.parse "<pgipconst name='radio1'/>");
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    31
val _ = asseqx (pgiptype_to_xml (Pgipchoice [Pgipdtype (SOME "the best choice",Pgipbool)]))
26541
14b268974c4b XML.string_of, XML.parse;
wenzelm
parents: 25275
diff changeset
    32
       (XML.parse "<pgipchoice><pgipbool descr='the best choice'/></pgipchoice>");
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    33
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    34
val _ = asseqs (pgval_to_string (read_pgval Pgipbool "true")) "true";
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    35
val _ = asseqs (pgval_to_string (read_pgval Pgipbool "false")) "false";
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    36
val _ = asseqs (pgval_to_string (read_pgval (Pgipint(NONE,NONE)) "-37")) "-37";
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    37
val _ = asseqs (pgval_to_string (read_pgval Pgipnat "45")) "45";
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    38
val _ = asseqs (pgval_to_string (read_pgval Pgipstring "stringvalue")) "stringvalue";
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    39
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    40
local
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    41
    val choices = Pgipchoice [Pgipdtype (NONE,Pgipbool), Pgipdtype (NONE,Pgipnat), 
28020
1ff5167592ba get rid of tabs;
wenzelm
parents: 26541
diff changeset
    42
                              Pgipdtype (NONE,Pgipnull), Pgipdtype (NONE,Pgipconst "foo")]
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    43
in
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    44
val _ = asseqs (pgval_to_string (read_pgval choices "45")) "45";
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    45
val _ = asseqs (pgval_to_string (read_pgval choices "foo")) "foo";
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    46
val _ = asseqs (pgval_to_string (read_pgval choices "true")) "true";
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    47
val _ = asseqs (pgval_to_string (read_pgval choices "")) "";
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    48
val _ = (asseqs (pgval_to_string (read_pgval choices "-37")) "-37"; 
28020
1ff5167592ba get rid of tabs;
wenzelm
parents: 26541
diff changeset
    49
         error "pgip_tests: should fail") handle PGIP _ => ()
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    50
end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    51
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    52
val _ = asseqx (haspref {name="provewithgusto",descr=SOME "use energetic proofs",
28020
1ff5167592ba get rid of tabs;
wenzelm
parents: 26541
diff changeset
    53
                 default=SOME "true", pgiptype=Pgipbool})
26541
14b268974c4b XML.string_of, XML.parse;
wenzelm
parents: 25275
diff changeset
    54
       (XML.parse "<haspref name='provewithgusto' descr='use energetic proofs' default='true'><pgipbool/></haspref>");
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    55
end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    56
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    57
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    58
(** pgip_input.ML **)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    59
local
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    60
26541
14b268974c4b XML.string_of, XML.parse;
wenzelm
parents: 25275
diff changeset
    61
fun e str = case XML.parse str of 
28020
1ff5167592ba get rid of tabs;
wenzelm
parents: 26541
diff changeset
    62
                (XML.Elem args) => args
1ff5167592ba get rid of tabs;
wenzelm
parents: 26541
diff changeset
    63
              | _ => error("Expected to get an XML Element")
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    64
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    65
open PgipInput;
22164
ac1bae165ad8 Test askref
aspinall
parents: 22083
diff changeset
    66
open PgipTypes;
22407
6e52564bcb53 Update test for new parse result
aspinall
parents: 22164
diff changeset
    67
open PgipIsabelle;
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    68
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    69
fun asseqi a b =
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21867
diff changeset
    70
    if input (e a) = b then ()
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    71
    else error("PGIP test: expected two inputs to be equal, for input:\n" ^ a)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    72
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    73
in
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    74
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    75
val _ = asseqi "<askpgip/>" (SOME (Askpgip()));
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    76
val _ = asseqi "<askpgml/>" (SOME (Askpgml()));
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    77
val _ = asseqi "<askconfig/>" (SOME (Askconfig()));
23436
343e84195e2c Remove dedicated flag setting elements in favour of setproverflag.
aspinall
parents: 22407
diff changeset
    78
(* FIXME: new tests:
22083
4bfd987b005c Fix pgmlsymbolsoff
aspinall
parents: 21940
diff changeset
    79
val _ = asseqi "<pgmlsymbolson/>" (SOME (Pgmlsymbolson()));
4bfd987b005c Fix pgmlsymbolsoff
aspinall
parents: 21940
diff changeset
    80
val _ = asseqi "<pgmlsymbolsoff/>" (SOME (Pgmlsymbolsoff()));
4bfd987b005c Fix pgmlsymbolsoff
aspinall
parents: 21940
diff changeset
    81
val _ = asseqi "<startquiet/>" (SOME (Startquiet()));
4bfd987b005c Fix pgmlsymbolsoff
aspinall
parents: 21940
diff changeset
    82
val _ = asseqi "<stopquiet/>" (SOME (Stopquiet()));
23436
343e84195e2c Remove dedicated flag setting elements in favour of setproverflag.
aspinall
parents: 22407
diff changeset
    83
*)
22164
ac1bae165ad8 Test askref
aspinall
parents: 22083
diff changeset
    84
val _ = asseqi "<askrefs thyname='foo' objtype='theory'/>" (SOME (Askrefs {url=NONE, thyname=SOME "foo",
28020
1ff5167592ba get rid of tabs;
wenzelm
parents: 26541
diff changeset
    85
                                                                          objtype=SOME ObjTheory,name=NONE}));
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    86
val _ = asseqi "<otherelt/>" NONE;
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    87
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    88
end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    89
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21637
diff changeset
    90
(** pgip_markup.ML **)
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21637
diff changeset
    91
local
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21637
diff changeset
    92
open PgipMarkup
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21637
diff changeset
    93
in
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21637
diff changeset
    94
val _ = ()
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21637
diff changeset
    95
end
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21637
diff changeset
    96
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21637
diff changeset
    97
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    98
(** pgip_output.ML **)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    99
local
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   100
open PgipOutput
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   101
in
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   102
val _ = ()
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   103
end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   104
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21637
diff changeset
   105
25275
76d7f3fd4fb3 removed obsolete ProofGeneral/parsing.ML;
wenzelm
parents: 24192
diff changeset
   106
(** pgip_parser.ML **)
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21637
diff changeset
   107
local
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21637
diff changeset
   108
open PgipMarkup
25275
76d7f3fd4fb3 removed obsolete ProofGeneral/parsing.ML;
wenzelm
parents: 24192
diff changeset
   109
open PgipParser
22407
6e52564bcb53 Update test for new parse result
aspinall
parents: 22164
diff changeset
   110
open PgipIsabelle
6e52564bcb53 Update test for new parse result
aspinall
parents: 22164
diff changeset
   111
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21637
diff changeset
   112
fun asseqp a b =
25275
76d7f3fd4fb3 removed obsolete ProofGeneral/parsing.ML;
wenzelm
parents: 24192
diff changeset
   113
    if pgip_parser Position.none a = b then ()
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21637
diff changeset
   114
    else error("PGIP test: expected two parses to be equal, for input:\n" ^ a)
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21637
diff changeset
   115
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21637
diff changeset
   116
in
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21637
diff changeset
   117
val _ = 
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21637
diff changeset
   118
    asseqp "theory A imports Bthy Cthy Dthy begin"
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21637
diff changeset
   119
    [Opentheory
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21637
diff changeset
   120
         {text = "theory A imports Bthy Cthy Dthy begin",
24192
4eccd4bb8b64 PGIP change: thyname is optional in opentheory, markup even in case of header parse failure
aspinall
parents: 23798
diff changeset
   121
          thyname = SOME "A",
22407
6e52564bcb53 Update test for new parse result
aspinall
parents: 22164
diff changeset
   122
          parentnames = ["Bthy", "Cthy", "Dthy"]},
6e52564bcb53 Update test for new parse result
aspinall
parents: 22164
diff changeset
   123
     Openblock {metavarid=NONE,name=NONE,objtype=SOME ObjTheoryBody}];
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21637
diff changeset
   124
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21637
diff changeset
   125
val _ = 
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21637
diff changeset
   126
    asseqp "end" 
22407
6e52564bcb53 Update test for new parse result
aspinall
parents: 22164
diff changeset
   127
   [Closeblock {}, Closetheory {text = "end"}];
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21637
diff changeset
   128
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21637
diff changeset
   129
end