|
(* Title: Pure/term_xml.ML
Author: Makarius
XML data representation of lambda terms.
*)
signature TERM_XML_OPS =
sig
type 'a T
type 'a P
val indexname: indexname P
val sort: sort T
val typ: typ T
val term_raw: term T
val typ_body: typ T
val term: Consts.T -> term T
end
signature TERM_XML =
sig
structure Encode: TERM_XML_OPS
structure Decode: TERM_XML_OPS
end;
structure Term_XML: TERM_XML =
struct
structure Encode =
struct
open XML.Encode;
fun indexname (a, b) = if b = 0 then [a] else [a, int_atom b];
val sort = list string;
fun typ T = T |> variant
[fn Type (a, b) => ([a], list typ b),
fn TFree (a, b) => ([a], sort b),
fn TVar (a, b) => (indexname a, sort b)];
fun term_raw t = t |> variant
[fn Const (a, b) => ([a], typ b),
fn Free (a, b) => ([a], typ b),
fn Var (a, b) => (indexname a, typ b),
fn Bound a => ([], int a),
fn Abs (a, b, c) => ([a], pair typ term_raw (b, c)),
fn op $ a => ([], pair term_raw term_raw a)];
fun typ_body T = if T = dummyT then [] else typ T;
fun term consts t = t |> variant
[fn Const (a, b) => ([a], list typ (Consts.typargs consts (a, b))),
fn Free (a, b) => ([a], typ_body b),
fn Var (a, b) => (indexname a, typ_body b),
fn Bound a => ([], int a),
fn Abs (a, b, c) => ([a], pair typ (term consts) (b, c)),
fn op $ a => ([], pair (term consts) (term consts) a)];
end;
structure Decode =
struct
open XML.Decode;
fun indexname [a] = (a, 0)
| indexname [a, b] = (a, int_atom b);
val sort = list string;
fun typ body = body |> variant
[fn ([a], b) => Type (a, list typ b),
fn ([a], b) => TFree (a, sort b),
fn (a, b) => TVar (indexname a, sort b)];
fun term_raw body = body |> variant
[fn ([a], b) => Const (a, typ b),
fn ([a], b) => Free (a, typ b),
fn (a, b) => Var (indexname a, typ b),
fn ([], a) => Bound (int a),
fn ([a], b) => let val (c, d) = pair typ term_raw b in Abs (a, c, d) end,
fn ([], a) => op $ (pair term_raw term_raw a)];
fun typ_body [] = dummyT
| typ_body body = typ body;
fun term consts body = body |> variant
[fn ([a], b) => Const (a, Consts.instance consts (a, list typ b)),
fn ([a], b) => Free (a, typ_body b),
fn (a, b) => Var (indexname a, typ_body b),
fn ([], a) => Bound (int a),
fn ([a], b) => let val (c, d) = pair typ (term consts) b in Abs (a, c, d) end,
fn ([], a) => op $ (pair (term consts) (term consts) a)];
end;
end;
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
