Revamped Proof General interface.
(* Title: Pure/ProofGeneral/pgip_types.ML
ID: $Id$
Author: David Aspinall
PGIP abstraction: types and conversions
*)
(* TODO: add objtypes and PGML *)
signature PGIPTYPES =
sig
(* Types and values (used for preferences and dialogs) *)
datatype pgiptype = Pgipnull | Pgipbool | Pgipint of int option * int option | Pgipnat
| Pgipstring | Pgipconst of string | Pgipchoice of pgipdtype list
and pgipdtype = Pgipdtype of string option * pgiptype (* type with opt. description *)
type pgipval (* typed value *)
(* URLs we can cope with *)
type pgipurl
(* Representation error in reading/writing PGIP *)
exception PGIP of string
(* Interface areas for message output *)
datatype displayarea = Status | Message | Display | Other of string
(* Kinds of message output (influence display behaviour) *)
datatype messagecategory = Normal | Information | Tracing | Internal
(* Error levels *)
datatype fatality = Nonfatal | Fatal | Panic | Log | Debug
(* File location *)
type location = { descr: string option,
url: pgipurl option,
line: int option,
column: int option,
char: int option }
(* Prover preference *)
type preference = { name: string,
descr: string option,
default: string option,
pgiptype: pgiptype }
end
signature PGIPTYPES_OPNS =
sig
include PGIPTYPES
(* Values as XML strings *)
val read_pgipint : (int option * int option) -> string -> int (* raises PGIP *)
val read_pgipnat : string -> int (* raises PGIP *)
val read_pgipbool : string -> bool (* raises PGIP *)
val read_pgipstring : string -> string (* raises PGIP *)
val int_to_pgstring : int -> string
val bool_to_pgstring : bool -> string
val string_to_pgstring : string -> string
(* PGIP datatypes *)
val pgiptype_to_xml : pgiptype -> XML.tree
val read_pgval : pgiptype -> string -> pgipval (* raises PGIP *)
val pgval_to_string : pgipval -> string
val attrs_of_displayarea : displayarea -> XML.attributes
val attrs_of_messagecategory : messagecategory -> XML.attributes
val attrs_of_fatality : fatality -> XML.attributes
val attrs_of_location : location -> XML.attributes
val location_of_attrs : XML.attributes -> location (* raises PGIP *)
val haspref : preference -> XML.tree
val pgipurl_of_url : Url.T -> pgipurl (* raises PGIP *)
val pgipurl_of_string : string -> pgipurl (* raises PGIP *)
val pgipurl_of_path : Path.T -> pgipurl
val attrs_of_pgipurl : pgipurl -> XML.attributes
val pgipurl_of_attrs : XML.attributes -> pgipurl (* raises PGIP *)
(* XML utils, only for PGIP code *)
val attr : string -> string -> XML.attributes
val opt_attr : string -> string option -> XML.attributes
val opt_attr_map : ('a -> string) -> string -> 'a option -> XML.attributes
val get_attr : string -> XML.attributes -> string (* raises PGIP *)
val get_attr_opt : string -> XML.attributes -> string option
val get_attr_dflt : string -> string -> XML.attributes -> string
end
structure PgipTypes : PGIPTYPES_OPNS =
struct
exception PGIP of string
(** Utils **)
fun get_attr_opt attr attrs = AList.lookup (op =) attrs attr
fun get_attr attr attrs =
(case get_attr_opt attr attrs of
SOME value => value
| NONE => raise PGIP ("Missing attribute: " ^ attr))
fun get_attr_dflt attr dflt attrs = the_default dflt (get_attr_opt attr attrs)
fun attr x y = [(x,y)] : XML.attributes
fun opt_attr_map f attr_name opt_val =
case opt_val of NONE => [] | SOME v => [(attr_name,f v)]
(* or, if you've got function-itis:
the_default [] (Option.map (single o (pair attr_name) o f) opt_val)
*)
val opt_attr = opt_attr_map I
(** Types and values **)
(* readers and writers for values represented in XML strings *)
fun read_pgipbool s =
(case s of
"false" => false
| "true" => true
| _ => raise PGIP ("Invalid boolean value: "^s))
local
fun int_in_range (NONE,NONE) _ = true
| int_in_range (SOME min,NONE) i = min<= i
| int_in_range (NONE,SOME max) i = i<=max
| int_in_range (SOME min,SOME max) i = min<= i andalso i<=max
in
fun read_pgipint range s =
(case Syntax.read_int s of
SOME i => if int_in_range range i then i
else raise PGIP ("Out of range integer value: "^s)
| NONE => raise PGIP ("Invalid integer value: "^s))
end;
fun read_pgipnat s =
(case Syntax.read_nat s of
SOME i => i
| NONE => raise PGIP ("Invalid natural number: "^s))
(* NB: we can maybe do without xml decode/encode here. *)
fun read_pgipstring s = (* non-empty strings, XML escapes decoded *)
(case XML.parse_string s of
SOME s => s
| NONE => raise PGIP ("Expected a non-empty string: "^s))
handle _ => raise PGIP ("Invalid XML string syntax: "^s)
fun int_to_pgstring i =
if i < 0 then "-" ^ string_of_int (~ i) else string_of_int i
fun string_to_pgstring s = XML.text s
fun bool_to_pgstring b = if b then "true" else "false"
(* PGIP datatypes.
This is a reflection of the type structure of PGIP configuration,
which is meant for setting up user dialogs and preference settings.
These are configured declaratively in XML, using a syntax for types
and values which is like a (vastly cut down) form of XML Schema
Datatypes.
The prover needs to interpret the strings representing the typed
values, at least for the types it expects from the dialogs it
configures. Here we go further and construct a type-safe
encapsulation of these values, which would be useful for more
advanced cases (e.g. generating and processing forms).
*)
datatype pgiptype =
Pgipnull (* unit type: unique element is empty string *)
| Pgipbool (* booleans: "true" or "false" *)
| Pgipint of int option * int option (* ranged integers, should be XSD canonical *)
| Pgipnat (* naturals: non-negative integers (convenience) *)
| Pgipstring (* non-empty strings *)
| Pgipconst of string (* singleton type *)
| Pgipchoice of pgipdtype list (* union type *)
(* Compared with the PGIP schema, we push descriptions of types inside choices. *)
and pgipdtype = Pgipdtype of string option * pgiptype
datatype pgipuval = Pgvalnull | Pgvalbool of bool | Pgvalint of int | Pgvalnat of int
| Pgvalstring of string | Pgvalconst of string
type pgipval = pgiptype * pgipuval (* type-safe values *)
fun pgipdtype_to_xml (desco,ty) =
let
val desc_attr = opt_attr "descr" desco
val elt = case ty of
Pgipnull => "pgipnull"
| Pgipbool => "pgipbool"
| Pgipint _ => "pgipint"
| Pgipnat => "pgipint"
| Pgipstring => "pgipstring"
| Pgipconst _ => "pgipconst"
| Pgipchoice _ => "pgipchoice"
fun range_attr r v = attr r (int_to_pgstring v)
val attrs = case ty of
Pgipint (SOME min,SOME max) => (range_attr "min" min)@(range_attr "max" max)
| Pgipint (SOME min,NONE) => (range_attr "min" min)
| Pgipint (NONE,SOME max) => (range_attr "max" max)
| Pgipnat => (range_attr "min" 0)
| Pgipconst nm => attr "name" nm
| _ => []
fun destpgipdtype (Pgipdtype x) = x
val typargs = case ty of
Pgipchoice ds => map destpgipdtype ds
| _ => []
in
XML.Elem (elt, (desc_attr @ attrs), (map pgipdtype_to_xml typargs))
end
val pgiptype_to_xml = pgipdtype_to_xml o (pair NONE)
fun read_pguval Pgipnull s =
if s="" then Pgvalnull
else raise PGIP ("Expecting empty string for null type, not: "^s)
| read_pguval Pgipbool s = Pgvalbool (read_pgipbool s)
| read_pguval (Pgipint range) s = Pgvalint (read_pgipint range s)
| read_pguval Pgipnat s = Pgvalnat (read_pgipnat s)
| read_pguval (Pgipconst c) s =
if c=s then Pgvalconst c
else raise PGIP ("Given string: "^s^" doesn't match expected string: "^c)
| read_pguval Pgipstring s =
if s<>"" then Pgvalstring s
else raise PGIP ("Expecting non-empty string, empty string illegal.")
| read_pguval (Pgipchoice tydescs) s =
let
(* Union type: match first in list *)
fun getty (Pgipdtype(_,ty)) = ty
val uval = get_first
(fn ty => SOME (read_pguval ty s) handle PGIP _ => NONE)
(map getty tydescs)
in
case uval of SOME pgv => pgv | NONE => raise PGIP ("Can't match string: "^s^
" against any allowed types.")
end
fun read_pgval ty s = (ty, read_pguval ty s)
fun pgval_to_string (_, Pgvalnull) = ""
| pgval_to_string (_,(Pgvalbool b)) = bool_to_pgstring b
| pgval_to_string (_,(Pgvalnat n)) = int_to_pgstring n
| pgval_to_string (_,(Pgvalint i)) = int_to_pgstring i
| pgval_to_string (_,(Pgvalconst c)) = string_to_pgstring c
| pgval_to_string (_,(Pgvalstring s)) = string_to_pgstring s
(** URLs: only local files **)
type pgipurl = Path.T
datatype displayarea = Status | Message | Display | Other of string
datatype messagecategory = Normal | Information | Tracing | Internal
datatype fatality = Nonfatal | Fatal | Panic | Log | Debug
type location = { descr: string option,
url: pgipurl option,
line: int option,
column: int option,
char: int option }
(** Url operations **)
fun pgipurl_of_string url = (* only handle file:/// or file://localhost/ *)
case Url.unpack url of
(Url.File path) => path
| _ => raise PGIP ("Cannot access non-local URL " ^ url)
fun pgipurl_of_path p = p
fun attrs_of_pgipurl purl =
[("url", "file:" ^ (XML.text (File.platform_path (File.full_path purl))))]
val pgipurl_of_attrs = pgipurl_of_string o (get_attr "url")
fun pgipurl_of_url (Url.File p) = p
| pgipurl_of_url url = raise PGIP ("Cannot access non-local/non-file URL " ^ (Url.pack url))
(** Messages and errors **)
local
fun string_of_area Status = "status"
| string_of_area Message = "message"
| string_of_area Display = "display"
| string_of_area (Other s) = s
fun string_of_msgcat Internal = "internal"
| string_of_msgcat Information = "information"
| string_of_msgcat Tracing = "tracing"
| string_of_msgcat Normal = "normal" (* omitted in PGIP *)
fun string_of_fatality Nonfatal = "nonfatal"
| string_of_fatality Fatal = "fatal"
| string_of_fatality Panic = "panic"
| string_of_fatality Log = "log"
| string_of_fatality Debug = "debug"
in
fun attrs_of_displayarea area = [("area", string_of_area area)]
fun attrs_of_messagecategory msgcat =
case msgcat of
Normal => []
| _ => [("messagecategory", string_of_msgcat msgcat)]
fun attrs_of_fatality fatality = [("fatality", string_of_fatality fatality)]
fun attrs_of_location ({ descr, url, line, column, char }:location) =
let
val descr = opt_attr "descr"descr
val url = the_default [] (Option.map attrs_of_pgipurl url)
val line = opt_attr_map int_to_pgstring "line" line
val column = opt_attr_map int_to_pgstring "column" column
val char = opt_attr_map int_to_pgstring "char" char
in
descr @ url @ line @ column @ char
end
fun pgipint_of_string err s =
case Syntax.read_int s of
SOME i => i
| NONE => raise PGIP ("Type error in " ^ err ^ ": expected integer.")
fun location_of_attrs attrs =
let
val descr = get_attr_opt "descr" attrs
val url = Option.map pgipurl_of_string (get_attr_opt "url" attrs)
val line = Option.map (pgipint_of_string "location element line attribute")
(get_attr_opt "line" attrs)
val column = Option.map (pgipint_of_string "location element column attribute")
(get_attr_opt "column" attrs)
val char = Option.map (pgipint_of_string "location element char attribute")
(get_attr_opt "char" attrs)
in
{descr=descr, url=url, line=line, column=column, char=char}
end
end
(** Preferences **)
type preference = { name: string,
descr: string option,
default: string option,
pgiptype: pgiptype }
fun haspref ({ name, descr, default, pgiptype}:preference) =
XML.Elem ("haspref",
attr "name" name @
opt_attr "descr" descr @
opt_attr "default" default,
[pgiptype_to_xml pgiptype])
end