src/Pure/ProofGeneral/pgip_tests.ML
author wenzelm
Fri Jun 13 21:04:42 2008 +0200 (2008-06-13)
changeset 27195 bbf4cbc69243
parent 26541 14b268974c4b
child 28020 1ff5167592ba
permissions -rw-r--r--
map_const: soft version, no failure here;
aspinall@21637
     1
(*  Title:      Pure/ProofGeneral/pgip_tests.ML
aspinall@21637
     2
    ID:         $Id$
aspinall@21637
     3
    Author:     David Aspinall
aspinall@21637
     4
aspinall@21637
     5
A test suite for the PGIP abstraction code (in progress).
wenzelm@21940
     6
Run to provide some mild insurance against breakage in Isabelle here.
aspinall@21637
     7
*)
aspinall@21637
     8
aspinall@21637
     9
(** pgip_types.ML **)
aspinall@21637
    10
aspinall@21637
    11
local
aspinall@21637
    12
fun asseq_p toS a b =
aspinall@21637
    13
    if a=b then ()
aspinall@21637
    14
    else error("PGIP test: expected these two values to be equal:\n" ^
aspinall@21637
    15
	       (toS a) ^"\n and: \n" ^ (toS b))
aspinall@21637
    16
wenzelm@26541
    17
val asseqx = asseq_p XML.string_of
aspinall@21637
    18
val asseqs = asseq_p I
aspinall@21637
    19
val asseqb = asseq_p (fn b=>if b then "true" else "false")
aspinall@21637
    20
aspinall@21637
    21
open PgipTypes;
aspinall@21637
    22
in
aspinall@21637
    23
wenzelm@26541
    24
val _ = asseqx (pgiptype_to_xml Pgipnull) (XML.parse "<pgipnull/>");
wenzelm@26541
    25
val _ = asseqx (pgiptype_to_xml Pgipbool) (XML.parse "<pgipbool/>");
wenzelm@26541
    26
val _ = asseqx (pgiptype_to_xml (Pgipint (NONE,NONE))) (XML.parse "<pgipint/>");
wenzelm@26541
    27
val _ = asseqx (pgiptype_to_xml (Pgipint (SOME 5,SOME 7))) (XML.parse "<pgipint min='5' max='7'/>");
wenzelm@26541
    28
val _ = asseqx (pgiptype_to_xml (Pgipint (NONE,SOME 7))) (XML.parse "<pgipint max='7'/>");
wenzelm@26541
    29
val _ = asseqx (pgiptype_to_xml (Pgipint (SOME ~5,NONE))) (XML.parse "<pgipint min='-5'/>");
wenzelm@26541
    30
val _ = asseqx (pgiptype_to_xml Pgipstring) (XML.parse "<pgipstring/>");
wenzelm@26541
    31
val _ = asseqx (pgiptype_to_xml (Pgipconst "radio1"))  (XML.parse "<pgipconst name='radio1'/>");
aspinall@21637
    32
val _ = asseqx (pgiptype_to_xml (Pgipchoice [Pgipdtype (SOME "the best choice",Pgipbool)]))
wenzelm@26541
    33
       (XML.parse "<pgipchoice><pgipbool descr='the best choice'/></pgipchoice>");
aspinall@21637
    34
aspinall@21637
    35
val _ = asseqs (pgval_to_string (read_pgval Pgipbool "true")) "true";
aspinall@21637
    36
val _ = asseqs (pgval_to_string (read_pgval Pgipbool "false")) "false";
aspinall@21637
    37
val _ = asseqs (pgval_to_string (read_pgval (Pgipint(NONE,NONE)) "-37")) "-37";
aspinall@21637
    38
val _ = asseqs (pgval_to_string (read_pgval Pgipnat "45")) "45";
aspinall@21637
    39
val _ = asseqs (pgval_to_string (read_pgval Pgipstring "stringvalue")) "stringvalue";
aspinall@21637
    40
aspinall@21637
    41
local
aspinall@21637
    42
    val choices = Pgipchoice [Pgipdtype (NONE,Pgipbool), Pgipdtype (NONE,Pgipnat), 
aspinall@21637
    43
			      Pgipdtype (NONE,Pgipnull), Pgipdtype (NONE,Pgipconst "foo")]
aspinall@21637
    44
in
aspinall@21637
    45
val _ = asseqs (pgval_to_string (read_pgval choices "45")) "45";
aspinall@21637
    46
val _ = asseqs (pgval_to_string (read_pgval choices "foo")) "foo";
aspinall@21637
    47
val _ = asseqs (pgval_to_string (read_pgval choices "true")) "true";
aspinall@21637
    48
val _ = asseqs (pgval_to_string (read_pgval choices "")) "";
aspinall@21637
    49
val _ = (asseqs (pgval_to_string (read_pgval choices "-37")) "-37"; 
aspinall@21637
    50
	 error "pgip_tests: should fail") handle PGIP _ => ()
aspinall@21637
    51
end
aspinall@21637
    52
aspinall@21637
    53
val _ = asseqx (haspref {name="provewithgusto",descr=SOME "use energetic proofs",
aspinall@21637
    54
		 default=SOME "true", pgiptype=Pgipbool})
wenzelm@26541
    55
       (XML.parse "<haspref name='provewithgusto' descr='use energetic proofs' default='true'><pgipbool/></haspref>");
aspinall@21637
    56
end
aspinall@21637
    57
aspinall@21637
    58
aspinall@21637
    59
(** pgip_input.ML **)
aspinall@21637
    60
local
aspinall@21637
    61
wenzelm@26541
    62
fun e str = case XML.parse str of 
aspinall@21637
    63
		(XML.Elem args) => args
aspinall@21637
    64
	      | _ => error("Expected to get an XML Element")
aspinall@21637
    65
aspinall@21637
    66
open PgipInput;
aspinall@22164
    67
open PgipTypes;
aspinall@22407
    68
open PgipIsabelle;
aspinall@21637
    69
aspinall@21637
    70
fun asseqi a b =
wenzelm@21940
    71
    if input (e a) = b then ()
aspinall@21637
    72
    else error("PGIP test: expected two inputs to be equal, for input:\n" ^ a)
aspinall@21637
    73
aspinall@21637
    74
in
aspinall@21637
    75
aspinall@21637
    76
val _ = asseqi "<askpgip/>" (SOME (Askpgip()));
aspinall@21637
    77
val _ = asseqi "<askpgml/>" (SOME (Askpgml()));
aspinall@21637
    78
val _ = asseqi "<askconfig/>" (SOME (Askconfig()));
aspinall@23436
    79
(* FIXME: new tests:
aspinall@22083
    80
val _ = asseqi "<pgmlsymbolson/>" (SOME (Pgmlsymbolson()));
aspinall@22083
    81
val _ = asseqi "<pgmlsymbolsoff/>" (SOME (Pgmlsymbolsoff()));
aspinall@22083
    82
val _ = asseqi "<startquiet/>" (SOME (Startquiet()));
aspinall@22083
    83
val _ = asseqi "<stopquiet/>" (SOME (Stopquiet()));
aspinall@23436
    84
*)
aspinall@22164
    85
val _ = asseqi "<askrefs thyname='foo' objtype='theory'/>" (SOME (Askrefs {url=NONE, thyname=SOME "foo",
aspinall@22164
    86
									  objtype=SOME ObjTheory,name=NONE}));
aspinall@21637
    87
val _ = asseqi "<otherelt/>" NONE;
aspinall@21637
    88
aspinall@21637
    89
end
aspinall@21637
    90
aspinall@21867
    91
(** pgip_markup.ML **)
aspinall@21867
    92
local
aspinall@21867
    93
open PgipMarkup
aspinall@21867
    94
in
aspinall@21867
    95
val _ = ()
aspinall@21867
    96
end
aspinall@21867
    97
aspinall@21867
    98
aspinall@21637
    99
(** pgip_output.ML **)
aspinall@21637
   100
local
aspinall@21637
   101
open PgipOutput
aspinall@21637
   102
in
aspinall@21637
   103
val _ = ()
aspinall@21637
   104
end
aspinall@21637
   105
aspinall@21867
   106
wenzelm@25275
   107
(** pgip_parser.ML **)
aspinall@21867
   108
local
aspinall@21867
   109
open PgipMarkup
wenzelm@25275
   110
open PgipParser
aspinall@22407
   111
open PgipIsabelle
aspinall@22407
   112
aspinall@21867
   113
fun asseqp a b =
wenzelm@25275
   114
    if pgip_parser Position.none a = b then ()
aspinall@21867
   115
    else error("PGIP test: expected two parses to be equal, for input:\n" ^ a)
aspinall@21867
   116
aspinall@21867
   117
in
aspinall@21867
   118
val _ = 
aspinall@21867
   119
    asseqp "theory A imports Bthy Cthy Dthy begin"
aspinall@21867
   120
    [Opentheory
aspinall@21867
   121
         {text = "theory A imports Bthy Cthy Dthy begin",
aspinall@24192
   122
          thyname = SOME "A",
aspinall@22407
   123
          parentnames = ["Bthy", "Cthy", "Dthy"]},
aspinall@22407
   124
     Openblock {metavarid=NONE,name=NONE,objtype=SOME ObjTheoryBody}];
aspinall@21867
   125
aspinall@21867
   126
val _ = 
aspinall@21867
   127
    asseqp "end" 
aspinall@22407
   128
   [Closeblock {}, Closetheory {text = "end"}];
aspinall@21867
   129
aspinall@21867
   130
end