lots of internal cleaning and tuning;
removed {parse,print}_{pre,post}_proc;
new lexer: now human readable due to scanner combinators;
new parser installed, but still inactive (due to grammar ambiguities);
added Syntax.test_read;
typ_of_term: sorts now made distinct and sorted;
mixfix: added forced line breaks (//);
PROP now printed before subterm of type prop with non-const head;
--- a/src/Pure/Syntax/README Fri Oct 01 13:26:22 1993 +0100
+++ b/src/Pure/Syntax/README Mon Oct 04 15:30:49 1993 +0100
@@ -1,7 +1,8 @@
- Pure/Syntax
+ Pure/Syntax/
-This directory contains the source files for Isabelle's syntax module. Which
-includes a lexer, parser, pretty printer and macro system.
+This directory contains the source files for Isabelle's syntax module, which
+includes a lexer, parser, pretty printer and macro system. Note that only
+structures Pretty, Syntax and BasicSyntax are supposed to be exported.
There is no Makefile to compile these files separately; they are compiled as
part of Pure Isabelle.
--- a/src/Pure/Syntax/ROOT.ML Fri Oct 01 13:26:22 1993 +0100
+++ b/src/Pure/Syntax/ROOT.ML Mon Oct 04 15:30:49 1993 +0100
@@ -1,40 +1,48 @@
-(* Title: Pure/Syntax/ROOT
+(* Title: Pure/Syntax/ROOT.ML
ID: $Id$
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen
-This file builds the syntax module. It assumes the standard Isabelle
-environment.
+This file builds the syntax module.
*)
+use "lib.ML"; (* FIXME *)
+
+use "pretty.ML";
+
use "ast.ML";
use "xgram.ML";
+use "lexicon.ML";
use "extension.ML";
-use "lexicon.ML";
use "parse_tree.ML";
-use "earley0A.ML";
+use "parser.ML";
+use "earley0A.ML"; (* FIXME *)
use "type_ext.ML";
use "sextension.ML";
-use "pretty.ML";
use "printer.ML";
use "syntax.ML";
-structure Ast = AstFun();
+structure Pretty = PrettyFun();
+
+structure Ast = AstFun(Pretty);
structure XGram = XGramFun(Ast);
-structure Extension = ExtensionFun(XGram);
-structure Lexicon = LexiconFun(Extension);
-structure ParseTree = ParseTreeFun(structure Lexicon = Lexicon and Ast = Ast);
-structure Earley = EarleyFun(structure XGram = XGram and ParseTree = ParseTree);
+structure Lexicon = LexiconFun();
+structure Extension = ExtensionFun(structure XGram = XGram and Lexicon = Lexicon);
+structure ParseTree = ParseTreeFun(structure Ast = Ast and Lexicon = Lexicon);
+structure Parser = ParserFun(structure Symtab = Symtab and XGram = XGram
+ and ParseTree = ParseTree);
+structure Earley = EarleyFun(structure Symtab = Symtab and XGram = XGram
+ and ParseTree = ParseTree); (* FIXME *)
structure TypeExt = TypeExtFun(structure Extension = Extension
and Lexicon = Lexicon);
structure SExtension = SExtensionFun(structure TypeExt = TypeExt
and Lexicon = Lexicon);
-structure Pretty = PrettyFun();
structure Printer = PrinterFun(structure Symtab = Symtab and Lexicon = Lexicon
and TypeExt = TypeExt and SExtension = SExtension and Pretty = Pretty);
structure Syntax = SyntaxFun(structure Symtab = Symtab and TypeExt = TypeExt
and Parser = Earley and SExtension = SExtension and Printer = Printer);
+ (* FIXME ^^^^^^ *)
-(*Basic_Syntax has the most important primitives, which are made pervasive*)
+(*BasicSyntax has the most important primitives, which are made pervasive*)
signature BASIC_SYNTAX = sig include SEXTENSION0 include PRINTER0 end;
-structure Basic_Syntax: BASIC_SYNTAX = Syntax;
+structure BasicSyntax: BASIC_SYNTAX = Syntax;
--- a/src/Pure/Syntax/ast.ML Fri Oct 01 13:26:22 1993 +0100
+++ b/src/Pure/Syntax/ast.ML Mon Oct 04 15:30:49 1993 +0100
@@ -1,71 +1,105 @@
-(* Title: Pure/Syntax/ast
+(* Title: Pure/Syntax/ast.ML
ID: $Id$
Author: Markus Wenzel, TU Muenchen
-Abstract Syntax Trees, Syntax Rules and translation, matching, normalization
-of asts.
+Abstract syntax trees, translation rules, matching and normalization of asts.
*)
-signature AST =
+signature AST0 =
sig
+ structure Pretty: PRETTY
datatype ast =
Constant of string |
Variable of string |
Appl of ast list
val mk_appl: ast -> ast list -> ast
exception AST of string * ast list
+ val str_of_ast: ast -> string
+ val pretty_ast: ast -> Pretty.T
+ val pretty_rule: (ast * ast) -> Pretty.T
+ val pprint_ast: ast -> pprint_args -> unit
+ val trace_norm_ast: bool ref
+ val stat_norm_ast: bool ref
+end
+
+signature AST =
+sig
+ include AST0
val raise_ast: string -> ast list -> 'a
- val str_of_ast: ast -> string
val head_of_rule: ast * ast -> string
val rule_error: ast * ast -> string option
val fold_ast: string -> ast list -> ast
val fold_ast_p: string -> ast list * ast -> ast
val unfold_ast: string -> ast -> ast list
val unfold_ast_p: string -> ast -> ast list * ast
- val trace_norm: bool ref
- val stat_norm: bool ref
- val normalize: (string -> (ast * ast) list) option -> ast -> ast
+ val normalize: bool -> bool -> (string -> (ast * ast) list) option -> ast -> ast
+ val normalize_ast: (string -> (ast * ast) list) option -> ast -> ast
end;
-functor AstFun()(*: AST *) = (* FIXME *)
+functor AstFun(Pretty: PRETTY): AST =
struct
+structure Pretty = Pretty;
+
-(** Abstract Syntax Trees **)
+(** abstract syntax trees **)
(*asts come in two flavours:
- - proper asts representing terms and types: Variables are treated like
- Constants;
+ - ordinary asts representing terms and typs: Variables are (often) treated
+ like Constants;
- patterns used as lhs and rhs in rules: Variables are placeholders for
proper asts*)
datatype ast =
- Constant of string | (* "not", "_%", "fun" *)
- Variable of string | (* x, ?x, 'a, ?'a *)
- Appl of ast list; (* (f x y z), ("fun" 'a 'b) *)
+ Constant of string | (*"not", "_abs", "fun"*)
+ Variable of string | (*x, ?x, 'a, ?'a*)
+ Appl of ast list; (*(f x y z), ("fun" 'a 'b), ("_abs" x t)*)
(*the list of subasts of an Appl node has to contain at least 2 elements, i.e.
there are no empty asts or nullary applications; use mk_appl for convenience*)
-fun mk_appl ast [] = ast
- | mk_appl ast asts = Appl (ast :: asts);
+fun mk_appl f [] = f
+ | mk_appl f args = Appl (f :: args);
(*exception for system errors involving asts*)
exception AST of string * ast list;
-fun raise_ast msg asts = raise (AST (msg, asts));
+fun raise_ast msg asts = raise AST (msg, asts);
-(* print asts in a LISP-like style *)
+(** print asts in a LISP-like style **)
+
+(* str_of_ast *)
fun str_of_ast (Constant a) = quote a
| str_of_ast (Variable x) = x
| str_of_ast (Appl asts) = "(" ^ (space_implode " " (map str_of_ast asts)) ^ ")";
+(* pretty_ast *)
+
+fun pretty_ast (Constant a) = Pretty.str (quote a)
+ | pretty_ast (Variable x) = Pretty.str x
+ | pretty_ast (Appl asts) =
+ Pretty.blk (2, (Pretty.str "(") ::
+ (separate (Pretty.brk 1) (map pretty_ast asts)) @ [Pretty.str ")"]);
+
+
+(* pprint_ast *)
+
+val pprint_ast = Pretty.pprint o pretty_ast;
+
+
+(* pretty_rule *)
+
+fun pretty_rule (lhs, rhs) =
+ Pretty.blk
+ (2, [pretty_ast lhs, Pretty.str " ->", Pretty.brk 2, pretty_ast rhs]);
+
+
(* head_of_ast, head_of_rule *)
fun head_of_ast (Constant a) = Some a
@@ -76,9 +110,9 @@
-(** check Syntax Rules **)
+(** check translation rules **)
-(*a wellformed rule (lhs, rhs): (ast * ast) has the following properties:
+(*a wellformed rule (lhs, rhs): (ast * ast) obeys the following conditions:
- the head of lhs is a constant,
- the lhs has unique vars,
- vars of rhs is subset of vars of lhs*)
@@ -103,7 +137,7 @@
-(** translation utilities **)
+(** ast translation utilities **)
(* fold asts *)
@@ -120,10 +154,8 @@
if c = c' then x :: (unfold_ast c xs) else [y]
| unfold_ast _ y = [y];
-fun cons_fst x (xs, y) = (x :: xs, y);
-
fun unfold_ast_p c (y as Appl [Constant c', x, xs]) =
- if c = c' then cons_fst x (unfold_ast_p c xs)
+ if c = c' then apfst (cons x) (unfold_ast_p c xs)
else ([], y)
| unfold_ast_p _ y = ([], y);
@@ -131,6 +163,12 @@
(** normalization of asts **)
+(* tracing options *)
+
+val trace_norm_ast = ref false;
+val stat_norm_ast = ref false;
+
+
(* simple env *)
structure Env =
@@ -163,25 +201,20 @@
end;
-(* normalize *) (* FIXME clean *)
-
-val trace_norm = ref false;
-val stat_norm = ref false;
+(* normalize *)
(*the normalizer works yoyo-like: top-down, bottom-up, top-down, ...*)
-fun normalize get_rules pre_ast =
+fun normalize trace stat get_rules pre_ast =
let
val passes = ref 0;
val lookups = ref 0;
val failed_matches = ref 0;
val changes = ref 0;
- val trace = ! trace_norm;
-
fun inc i = i := ! i + 1;
- fun subst _ (ast as (Constant _)) = ast
+ fun subst _ (ast as Constant _) = ast
| subst env (Variable x) = Env.get (env, x)
| subst env (Appl asts) = Appl (map (subst env) asts);
@@ -189,7 +222,7 @@
(case match ast lhs of
Some env => (inc changes; Some (subst env rhs))
| None => (inc failed_matches; try_rules ast pats))
- | try_rules ast [] = None;
+ | try_rules _ [] = None;
fun try ast a = (inc lookups; try_rules ast (the get_rules a));
@@ -230,11 +263,11 @@
end;
- val () = if trace then writeln ("pre: " ^ str_of_ast pre_ast) else ();
+ val _ = if trace then writeln ("pre: " ^ str_of_ast pre_ast) else ();
val post_ast = if is_some get_rules then normal pre_ast else pre_ast;
in
- if trace orelse ! stat_norm then
+ if trace orelse stat then
writeln ("post: " ^ str_of_ast post_ast ^ "\nnormalize: " ^
string_of_int (! passes) ^ " passes, " ^
string_of_int (! lookups) ^ " lookups, " ^
@@ -245,5 +278,11 @@
end;
+(* normalize_ast *)
+
+fun normalize_ast get_rules ast =
+ normalize (! trace_norm_ast) (! stat_norm_ast) get_rules ast;
+
+
end;
--- a/src/Pure/Syntax/earley0A.ML Fri Oct 01 13:26:22 1993 +0100
+++ b/src/Pure/Syntax/earley0A.ML Mon Oct 04 15:30:49 1993 +0100
@@ -1,10 +1,8 @@
-(* Title: Pure/Syntax/earley0A
+(* Title: Pure/Syntax/earley0A.ML
ID: $Id$
Author: Tobias Nipkow
-Changes:
- PARSER: renamed Prod to prod
- renamed mk_early_gram to mk_earley_gram
+WARNING: This file is about to disappear.
*)
signature PARSER =
@@ -12,20 +10,67 @@
structure XGram: XGRAM
structure ParseTree: PARSE_TREE
local open XGram ParseTree ParseTree.Lexicon in
- type Gram
- val compile_xgram: string list * Token prod list -> Gram
- val parse: Gram * string * Token list -> ParseTree
- val parsable: Gram * string -> bool
- exception SYNTAX_ERR of Token list
- val print_gram: Gram * Lexicon -> unit
+ type gram
+ val mk_gram: string list -> string prod list -> gram
+ val parse: gram -> string -> token list -> parsetree
end
+
+(* exception SYNTAX_ERROR of token list *)
+(* val compile_xgram: string list * token prod list -> Gram *)
+(* val parsable: Gram * string -> bool *)
+(* val print_gram: Gram * lexicon -> unit *)
end;
-functor EarleyFun(structure XGram:XGRAM and ParseTree:PARSE_TREE): PARSER =
+functor EarleyFun(structure Symtab: SYMTAB and XGram: XGRAM
+ and ParseTree: PARSE_TREE): PARSER =
struct
+structure ParseTree = ParseTree;
+structure Lexicon = ParseTree.Lexicon;
structure XGram = XGram;
-structure ParseTree = ParseTree;
+open ParseTree Lexicon;
+
+
+(** mk_pt (from parse_tree.ML) **)
+
+fun mk_pt ("", [pt]) = pt
+ | mk_pt ("", _) = error "mk_pt: funny copy op in parse tree"
+ | mk_pt (s, ptl) = Node (s, ptl);
+
+
+
+(** token maps (from lexicon.ML) **)
+
+type 'b TokenMap = (token * 'b list) list * 'b list;
+val first_token = 0;
+
+fun int_of_token(Token(tk)) = first_token |
+ int_of_token(IdentSy _) = first_token - 1 |
+ int_of_token(VarSy _) = first_token - 2 |
+ int_of_token(TFreeSy _) = first_token - 3 |
+ int_of_token(TVarSy _) = first_token - 4 |
+ int_of_token(EndToken) = first_token - 5;
+
+fun lesstk(s, t) = int_of_token(s) < int_of_token(t) orelse
+ (case (s, t) of (Token(a), Token(b)) => a<b | _ => false);
+
+fun mkTokenMap(atll) =
+ let val aill = atll;
+ val dom = sort lesstk (distinct(flat(map snd aill)));
+ val mt = map fst (filter (null o snd) atll);
+ fun mktm(i) =
+ let fun add(l, (a, il)) = if i mem il then a::l else l
+ in (i, foldl add ([], aill)) end;
+ in (map mktm dom, mt) end;
+
+fun find_al (i) =
+ let fun find((j, al)::l) = if lesstk(i, j) then [] else
+ if matching_tokens(i, j) then al else find l |
+ find [] = [];
+ in find end;
+fun applyTokenMap((l, mt), tk:token) = mt@(find_al tk l);
+
+
(* Linked lists: *)
infix 5 &;
@@ -57,28 +102,28 @@
in acc(a0,0) end;
(*
-Gram: name of nt -> number, nt number -> productions array,
+gram: name of nt -> number, nt number -> productions array,
nt number -> list of nt's reachable via copy ops
*)
-datatype Symbol = T of Token | NT of int * int
+datatype Symbol = T of token | NT of int * int
and Op = Op of OpSyn * string * int
withtype OpSyn = Symbol array
and OpListA = Op array * int TokenMap
and FastAcc = int TokenMap;
-type Gram = int Symtab.table * OpListA array * int list array;
+type gram = int Symtab.table * OpListA array * int list array;
-fun non_term(Nonterminal(s,_)) = if predef_term(s)=end_token then [s] else []
+fun non_term(Nonterminal(s,_)) = if predef_term(s)=EndToken then [s] else []
| non_term(_) = [];
fun non_terms(Prod(_,symbs,_,_)) = flat(map non_term symbs);
(* mk_pre_grammar converts a list of productions in external format into an
-internal Gram object. *)
+internal gram object. *)
val dummyTM:FastAcc = mkTokenMap[];
-fun mk_pre_grammar(prods): Gram =
+fun mk_pre_grammar(prods): gram =
let fun same_res(Prod(t1,_,_,_), Prod(t2,_,_,_)) = t1=t2;
val partitioned0 = partition_eq same_res prods;
val nts0 = map (fn Prod(ty,_,_,_)::_ => ty) partitioned0;
@@ -90,7 +135,7 @@
fun nt_or_vt(s,p) =
(case predef_term(s) of
- end_token => let val Some(i) = Symtab.lookup(tab,s) in NT(i,p) end
+ EndToken => let val Some(i) = Symtab.lookup(tab,s) in NT(i,p) end
| tk => T(tk));
fun mksyn(Terminal(t)) = [T(t)]
@@ -106,7 +151,7 @@
val subs = array(length opLA,[]) : int list array;
fun newcp v (a,Op(syA,_,p)) =
- if p=copy_pri
+ if p=chain_pri
then let val NT(k,_) = sub(syA,0)
in if k mem v then a else k ins a end
else a;
@@ -123,7 +168,7 @@
(* Lookahead tables for speeding up parsing. Lkhd is a mapping from
nonterminals (in the form of OpList) to sets (lists) of token strings *)
-type Lkhd = Token list list list;
+type Lkhd = token list list list;
(* subst_syn(s,k) syn = [ pref k ts | ts is a token string derivable from sy
under substitution s ] *)
@@ -136,7 +181,7 @@
| pref k (e::l) = e::(pref (k-1) l);
fun subst_syn(s:Lkhd,k) =
- let fun subst(ref(symb & syn)):Token list list =
+ let fun subst(ref(symb & syn)):token list list =
let val l1 = case symb of T t => [[t]] |
NT(oplr,_) => let val Some l = assoc(s,!oplr) in l end
in distinct(map (pref k) (cross l1 (subst syn))) end |
@@ -168,7 +213,7 @@
iterate (replicate (length opLA) []) end;
(* create look ahead tables *)
-fun mk_earley_gram(g as (tab,opLA,_):Gram):Gram =
+fun mk_earley_gram(g as (tab,opLA,_):gram):gram =
let val lkhd = mk_lkhd(opLA,1);
fun mk_fa(i):FastAcc =
let val opA = #1(sub(opLA,i));
@@ -182,16 +227,40 @@
fun compile_xgram(roots,prods) =
let fun mk_root nt = Prod(RootPref^nt,
- [Nonterminal(nt,0),Terminal(end_token)],"",0);
+ [Nonterminal(nt,0),Terminal(EndToken)],"",0);
val prods' = (map mk_root roots) @ prods
in mk_earley_gram(mk_pre_grammar(prods')) end;
+
+(* translate (from xgram.ML) *)
+
+fun translate trfn =
+ map
+ (fn Terminal t => Terminal (trfn t)
+ | Nonterminal s => Nonterminal s
+ | Space s => Space s
+ | Bg i => Bg i
+ | Brk i => Brk i
+ | En => En);
+
+
+(* mk_gram (from syntax.ML) *)
+
+fun str_to_tok (opl: string prod list): token prod list =
+ map
+ (fn Prod (t, syn, s, pa) => Prod (t, translate Token syn, s, pa))
+ opl;
+
+fun mk_gram roots prods = compile_xgram (roots, str_to_tok prods);
+
+
+
(* State: nonterminal#, production#, index in production,
index of originating state set,
parse trees generated so far,
*)
-datatype State = St of int * int * int * int * ParseTree list
+datatype State = St of int * int * int * int * parsetree list
withtype StateSet = State LListR * (State -> unit) LListR;
type Compl = State -> unit;
type StateSetList = StateSet array;
@@ -255,22 +324,27 @@
in seq add (applyTokenMap(tm,tk)) end;
-fun parsable((tab,_,_):Gram, root:string) =
+(*(* FIXME *)
+fun parsable((tab,_,_):gram, root:string) =
not(Symtab.lookup(tab,RootPref^root) = None);
+*)
-exception SYNTAX_ERR of Token list;
+(* exception SYNTAX_ERROR of token list; *) (* FIXME *)
-fun unknown c = error("System Error - Trying to parse unknown category "^c);
+fun unknown c = error ("Unparsable category: " ^ c);
-fun parse((tab,opLA,rchA):Gram, root:string, tl: Token list): ParseTree =
- let val tl' = tl@[end_token];
+fun syn_err toks = error ("Syntax error at: " ^ space_implode " " (map str_of_token toks));
+
+fun parse ((tab,opLA,rchA):gram) (root:string) (tl: token list): parsetree =
+ let val tl' = tl; (* FIXME was ..@[EndToken] *)
val state_sets = mt_states(len tl' +1);
val s0 = mt_stateS();
val rooti = case Symtab.lookup(tab,RootPref^root) of
Some(ri) => ri | None => unknown root;
fun lr (tl,isi,si,t) =
- if ismt_stateS(si) then raise SYNTAX_ERR(t::tl) else
+(* if ismt_stateS(si) then raise SYNTAX_ERROR(t::tl) else *) (* FIXME *)
+ if ismt_stateS(si) then syn_err (t::tl) else
case tl of
[] => () |
t::tl =>
@@ -298,17 +372,19 @@
in update(state_sets,0,s0);
add_state(rooti,0,0,0,[],s0);
- lr(tl',0,s0,end_token(*dummy*));
+ lr(tl',0,s0,EndToken(*dummy*));
(*print_stat state_sets;*)
let val St(_,_,_,_,[pt]) = fst_state(sub(state_sets,len tl'))
in pt end
end;
-fun print_gram ((st,opAA,rchA):Gram,lex) =
+
+(*(* FIXME *)
+fun print_gram ((st,opAA,rchA):gram,lex) =
let val tts = Lexicon.name_of_token;
val al = map (fn (x,y)=>(y,x)) (Symtab.alist_of st);
fun nt i = let val Some(s) = assoc(al,i) in s end;
- fun print_sy(T(end_token)) = prs". " |
+ fun print_sy(T(EndToken)) = prs". " |
print_sy(T(tk)) = (prs(tts tk); prs" ") |
print_sy(NT(i,p)) = (prs((nt i)^"[");print_int p;prs"] ");
fun print_opA(i) =
@@ -324,7 +400,9 @@
fun print_rch(i) = (print_int i; prs" -> ";
print_list("[","]\n",print_int) (sub(rchA,i)))
in forA(print_opA,opAA) (*; forA(print_rch,rchA) *) end;
+*)
end;
end;
+
--- a/src/Pure/Syntax/extension.ML Fri Oct 01 13:26:22 1993 +0100
+++ b/src/Pure/Syntax/extension.ML Mon Oct 04 15:30:49 1993 +0100
@@ -1,8 +1,13 @@
-(* Title: Pure/Syntax/extension
+(* Title: Pure/Syntax/extension.ML
ID: $Id$
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen
-Syntax definition (internal interface)
+External grammar definition (internal interface).
+
+TODO:
+ Ext of {roots, mfix, extra_consts} * {.._translation} * {.._rules}
+ remove synrules
+ extend_xgram: move '.. \\ roots1' to Syntax.extend_tables
*)
signature EXTENSION0 =
@@ -23,52 +28,43 @@
mfix: mfix list,
extra_consts: string list,
parse_ast_translation: (string * (ast list -> ast)) list,
- parse_preproc: (ast -> ast) option,
- parse_postproc: (ast -> ast) option,
parse_translation: (string * (term list -> term)) list,
print_translation: (string * (term list -> term)) list,
- print_preproc: (ast -> ast) option,
- print_postproc: (ast -> ast) option,
print_ast_translation: (string * (ast list -> ast)) list}
datatype synrules =
SynRules of {
parse_rules: (ast * ast) list,
print_rules: (ast * ast) list}
- val max_pri: int
val logic: string
- val id: string
+ val args: string
val idT: typ
- val var: string
val varT: typ
- val tfree: string
val tfreeT: typ
- val tvar: string
val tvarT: typ
- val typ_to_nt: typ -> string
+ val typ_to_nonterm: typ -> string
val applC: string
- val args: string
val empty_synrules: synrules
- val empty: string xgram
- val extend: string xgram -> (ext * synrules) -> string xgram
+ val empty_xgram: xgram
+ val extend_xgram: xgram -> (ext * synrules) -> xgram
+ val mk_xgram: (ext * synrules) -> xgram
end
end;
-functor ExtensionFun(XGram: XGRAM): EXTENSION =
+functor ExtensionFun(structure XGram: XGRAM and Lexicon: LEXICON): EXTENSION =
struct
structure XGram = XGram;
-open XGram XGram.Ast;
+open XGram XGram.Ast Lexicon;
(** datatype ext **)
-(* Mfix (sy, ty, c, pl, p):
- sy: production as symbolic string
+(*Mfix (sy, ty, c, ps, p):
+ sy: rhs of production as symbolic string
ty: type description of production
- c: corresponding Isabelle Const
- pl: priorities of nonterminals in sy
- p: priority of production
-*)
+ c: head of parse tree
+ ps: priorities of arguments in sy
+ p: priority of production*)
datatype mfix = Mfix of string * typ * string * int list * int;
@@ -78,12 +74,8 @@
mfix: mfix list,
extra_consts: string list,
parse_ast_translation: (string * (ast list -> ast)) list,
- parse_preproc: (ast -> ast) option,
- parse_postproc: (ast -> ast) option,
parse_translation: (string * (term list -> term)) list,
print_translation: (string * (term list -> term)) list,
- print_preproc: (ast -> ast) option,
- print_postproc: (ast -> ast) option,
print_ast_translation: (string * (ast list -> ast)) list};
datatype synrules =
@@ -97,27 +89,20 @@
val empty_synrules = SynRules {parse_rules = [], print_rules = []};
-(* empty xgram *)
+(* empty_xgram *)
-val empty =
+val empty_xgram =
XGram {
roots = [], prods = [], consts = [],
parse_ast_translation = [],
- parse_preproc = None,
parse_rules = [],
- parse_postproc = None,
parse_translation = [],
print_translation = [],
- print_preproc = None,
print_rules = [],
- print_postproc = None,
print_ast_translation = []};
-
-(** syntactic constants etc. **)
-
-val max_pri = 1000; (*maximum legal priority*)
+(* syntactic categories *)
val logic = "logic";
val logicT = Type (logic, []);
@@ -125,114 +110,127 @@
val logic1 = "logic1";
val logic1T = Type (logic1, []);
+val args = "args";
+val argsT = Type (args, []);
+
val funT = Type ("fun", []);
+val typeT = Type ("type", []);
+
(* terminals *)
-val id = "id";
val idT = Type (id, []);
-
-val var = "var";
val varT = Type (var, []);
-
-val tfree = "tfree";
val tfreeT = Type (tfree, []);
-
-val tvar = "tvar";
val tvarT = Type (tvar, []);
-val terminalTs = [idT, varT, tfreeT, tvarT];
-
-val args = "args";
-val argsT = Type (args, []);
-
-val typeT = Type ("type", []);
+(* constants *)
val applC = "_appl";
val constrainC = "_constrain";
-fun typ_to_nt (Type (c, _)) = c
- | typ_to_nt _ = logic;
+(* typ_to_nonterm *)
+
+fun typ_to_nonterm (Type (c, _)) = c
+ | typ_to_nonterm _ = logic;
+
+fun typ_to_nonterm1 (Type (c, _)) = c
+ | typ_to_nonterm1 _ = logic1;
-(** extend xgram **) (* FIXME clean *)
-
-fun nonts syn = foldl (fn (i, "_") => i + 1 | (i, _) => i) (0, explode syn);
-
-val meta_chs = ["(", ")", "/", "_"];
+(** mfix_to_prod **)
-fun mk_term(pref, []) = (pref, [])
- | mk_term(pref, "'"::c::cl) = mk_term(pref^c, cl)
- | mk_term(pref, l as c::cl) = if is_blank(c) orelse c mem meta_chs
- then (pref, l) else mk_term(pref^c, cl);
-
-fun mk_space(sp, []) = (sp, []) |
- mk_space(sp, cl as c::cl') =
- if is_blank(c) then mk_space(sp^c, cl') else (sp, cl);
-
-exception ARG_EXN;
-exception BLOCK_EXN;
+fun mfix_to_prod (Mfix (sy, typ, const, pris, pri)) =
+ let
+ fun err msg =
+ (writeln ("Error in mixfix annotation " ^ quote sy ^ " for " ^ quote const);
+ error msg);
-fun mk_syntax([], ar, _, b, sy) = if b=0 then (sy, ar) else raise BLOCK_EXN
- | mk_syntax("_"::cs, Type("fun", [ar, ar']), [], b, sy) =
- mk_syntax(cs, ar', [], b, sy@[Nonterminal(typ_to_nt ar, 0)])
- | mk_syntax("_"::cs, Type("fun", [ar, ar']), p::pl, b, sy) =
- mk_syntax(cs, ar', pl, b, sy@[Nonterminal(typ_to_nt ar, p)])
- | mk_syntax("_"::cs, _, _, _, _) = raise ARG_EXN
- | mk_syntax("("::cs, ar, pl, b, sy) = let val (i, cs') = scan_int cs
- in mk_syntax(cs', ar, pl, b+1, sy@[Bg(i)]) end
- | mk_syntax(")"::cs, ar, pl, b, sy) =
- if b>0 then mk_syntax(cs, ar, pl, b-1, sy@[En]) else raise BLOCK_EXN
- | mk_syntax("/"::cs, ar, pl, b, sy) = let val (sp, cs') = take_prefix is_blank cs
- in mk_syntax(cs', ar, pl, b, sy@[Brk(length sp)]) end
- | mk_syntax(c::cs, ar, pl, b, sy) =
- let val (term, rest) =
- if is_blank(c)
- then let val (sp, cs') = mk_space(c, cs) in (Space(sp), cs') end
- else let val (tk, cs') = mk_term("", c::cs) in(Terminal(tk), cs') end
- in mk_syntax(rest, ar, pl, b, sy@[term]) end;
+ fun check_pri p =
+ if p >= 0 andalso p <= max_pri then ()
+ else err ("precedence out of range: " ^ string_of_int p);
-fun pri_test1 p = if 0 <= p andalso p <= max_pri then ()
- else error("Priority out of range: " ^ string_of_int p)
-fun pri_test(pl, p) = (pri_test1 p; seq pri_test1 pl);
+ fun blocks_ok [] 0 = true
+ | blocks_ok [] _ = false
+ | blocks_ok (Bg _ :: syms) n = blocks_ok syms (n + 1)
+ | blocks_ok (En :: _) 0 = false
+ | blocks_ok (En :: syms) n = blocks_ok syms (n - 1)
+ | blocks_ok (_ :: syms) n = blocks_ok syms n;
-fun mk_prod2(sy, T, opn, pl, p) =
-let val (syn, T') = mk_syntax(explode sy, T, pl, 0, []) handle
- ARG_EXN =>
- error("More arguments in "^sy^" than in corresponding type") |
- BLOCK_EXN => error("Unbalanced block parantheses in "^sy);
- val nt = case T' of Type(c, _) => c | _ => logic1;
-in Prod(nt, syn, opn, p) end;
-
-fun mk_prod1(sy, T, opn, pl, p) = (pri_test(pl, p); mk_prod2(sy, T, opn, pl, p));
+ fun check_blocks syms =
+ if blocks_ok syms 0 then ()
+ else err "unbalanced block parentheses";
-fun terminal1(T as Type("fun", _)) = hd(binder_types T) mem terminalTs
- | terminal1 _ = false;
+ fun is_meta c = c mem ["(", ")", "/", "_"];
+
+ fun scan_delim_char ("'" :: c :: cs) =
+ if is_blank c then err "illegal spaces in delimiter" else (c, cs)
+ | scan_delim_char ["'"] = err "trailing escape character"
+ | scan_delim_char (chs as c :: cs) =
+ if is_blank c orelse is_meta c then raise LEXICAL_ERROR else (c, cs)
+ | scan_delim_char [] = raise LEXICAL_ERROR;
+
+ val scan_symb =
+ $$ "_" >> K (Nonterminal ("", 0)) ||
+ $$ "(" -- scan_int >> (Bg o #2) ||
+ $$ ")" >> K En ||
+ $$ "/" -- $$ "/" >> K (Brk ~1) ||
+ $$ "/" -- scan_any is_blank >> (Brk o length o #2) ||
+ scan_any1 is_blank >> (Space o implode) ||
+ repeat1 scan_delim_char >> (Terminal o implode);
+
+
+ val cons_fst = apfst o cons;
-fun mk_prod(Mfix(sy, T, "", pl, p)) = if nonts sy <> 1
- then error"Copy op must have exactly one argument" else
- if filter_out is_blank (explode sy) = ["_"] andalso
- not(terminal1 T)
- then mk_prod2(sy, T, "", [copy_pri], copy_pri)
- else mk_prod1(sy, T, "", pl, p)
- | mk_prod(Mfix(sy, T, const, pl, p)) = mk_prod1(sy, T, const, pl, p)
+ fun add_args [] ty [] = ([], typ_to_nonterm1 ty)
+ | add_args [] _ _ = err "too many precedences"
+ | add_args (Nonterminal _ :: syms) (Type ("fun", [ty, tys])) [] =
+ cons_fst (Nonterminal (typ_to_nonterm ty, 0)) (add_args syms tys [])
+ | add_args (Nonterminal _ :: syms) (Type ("fun", [ty, tys])) (p :: ps) =
+ cons_fst (Nonterminal (typ_to_nonterm ty, p)) (add_args syms tys ps)
+ | add_args (Nonterminal _ :: _) _ _ =
+ err "more arguments than in corresponding type"
+ | add_args (sym :: syms) ty ps = cons_fst sym (add_args syms ty ps);
+
+
+ fun is_arg (Nonterminal _) = true
+ | is_arg _ = false;
+
+ fun is_term (Terminal _) = true
+ | is_term (Nonterminal (s, _)) = is_terminal s
+ | is_term _ = false;
+
+ fun rem_pri (Nonterminal (s, _)) = Nonterminal (s, chain_pri)
+ | rem_pri sym = sym;
+
+
+ val (raw_symbs, _) = repeat scan_symb (explode sy);
+ val (symbs, lhs) = add_args raw_symbs typ pris;
+ val prod = Prod (lhs, symbs, const, pri);
+ in
+ seq check_pri pris;
+ check_pri pri;
+ check_blocks symbs;
+ if is_terminal lhs then err ("illegal lhs: " ^ lhs) else ();
+
+ if const <> "" then prod
+ else if length (filter is_arg symbs) <> 1 then
+ err "copy production must have exactly one argument"
+ else if exists is_term symbs then prod
+ else Prod (lhs, map rem_pri symbs, "", chain_pri)
+ end;
-fun extend (XGram xgram) (Ext ext, SynRules rules) =
- let
- infix oo;
+(** extend_xgram **)
- fun None oo None = None
- | (Some f) oo None = Some f
- | None oo (Some g) = Some g
- | (Some f) oo (Some g) = Some (f o g);
-
+fun extend_xgram (XGram xgram) (Ext ext, SynRules rules) =
+ let
fun descend (from, to) = Mfix ("_", to --> from, "", [0], 0);
fun parents T = Mfix ("(1'(_'))", T --> T, "", [0], max_pri);
@@ -245,29 +243,21 @@
fun mkvar T = Mfix ("_", varT --> T, "", [], max_pri);
fun constrain T =
- Mfix ("_::_", [T, typeT]--->T, constrainC, [max_pri, 0], max_pri - 1);
+ Mfix ("_::_", [T, typeT] ---> T, constrainC, [max_pri, 0], max_pri - 1);
val {roots = roots1, prods, consts,
parse_ast_translation = parse_ast_translation1,
- parse_preproc = parse_preproc1,
parse_rules = parse_rules1,
- parse_postproc = parse_postproc1,
parse_translation = parse_translation1,
print_translation = print_translation1,
- print_preproc = print_preproc1,
print_rules = print_rules1,
- print_postproc = print_postproc1,
print_ast_translation = print_ast_translation1} = xgram;
val {roots = roots2, mfix, extra_consts,
parse_ast_translation = parse_ast_translation2,
- parse_preproc = parse_preproc2,
- parse_postproc = parse_postproc2,
parse_translation = parse_translation2,
print_translation = print_translation2,
- print_preproc = print_preproc2,
- print_postproc = print_postproc2,
print_ast_translation = print_ast_translation2} = ext;
val {parse_rules = parse_rules2, print_rules = print_rules2} = rules;
@@ -278,24 +268,26 @@
map mkid Troots' @ map mkvar Troots' @ map constrain Troots' @
map (apl (logicT, descend)) (Troots \\ [typeT, logicT]) @
map (apr (descend, logic1T)) Troots';
+ val mfix_consts =
+ distinct (filter is_xid (map (fn (Mfix (_, _, c, _, _)) => c) mfix'));
in
XGram {
roots = distinct (roots1 @ roots2),
-(* roots = roots1 union roots2, *) (* FIXME remove *)
- prods = prods @ map mk_prod mfix',
- consts = consts union extra_consts,
+ prods = prods @ map mfix_to_prod mfix',
+ consts = extra_consts union (mfix_consts union consts),
parse_ast_translation = parse_ast_translation1 @ parse_ast_translation2,
- parse_preproc = parse_preproc1 oo parse_preproc2,
parse_rules = parse_rules1 @ parse_rules2,
- parse_postproc = parse_postproc2 oo parse_postproc1,
parse_translation = parse_translation1 @ parse_translation2,
print_translation = print_translation1 @ print_translation2,
- print_preproc = print_preproc1 oo print_preproc2,
print_rules = print_rules1 @ print_rules2,
- print_postproc = print_postproc2 oo print_postproc1,
print_ast_translation = print_ast_translation1 @ print_ast_translation2}
end;
+(* mk_xgram *)
+
+val mk_xgram = extend_xgram empty_xgram;
+
+
end;
--- a/src/Pure/Syntax/lexicon.ML Fri Oct 01 13:26:22 1993 +0100
+++ b/src/Pure/Syntax/lexicon.ML Mon Oct 04 15:30:49 1993 +0100
@@ -1,251 +1,388 @@
-(* Title: Lexicon
+(* Title: Pure/Syntax/lexicon.ML
ID: $Id$
- Author: Tobias Nipkow, TU Muenchen
- Copyright 1993 TU Muenchen
+ Author: Tobias Nipkow and Markus Wenzel, TU Muenchen
-The Isabelle Lexer
+Scanner combinators and Isabelle's main lexer (used for terms and typs).
+*)
-Changes:
-TODO:
- Lexicon -> lexicon, Token -> token
- end_token -> EndToken ?
-*)
+infix 5 -- ^^;
+infix 3 >>;
+infix 0 ||;
signature LEXICON0 =
sig
val is_identifier: string -> bool
+ val string_of_vname: indexname -> string
val scan_varname: string list -> indexname * string list
- val string_of_vname: indexname -> string
+ val scan_var: string -> term
end;
signature LEXICON =
sig
- type Lexicon
- datatype Token = Token of string
- | IdentSy of string
- | VarSy of string * int
- | TFreeSy of string
- | TVarSy of string * int
- | end_token;
- val empty: Lexicon
- val extend: Lexicon * string list -> Lexicon
- val matching_tokens: Token * Token -> bool
- val mk_lexicon: string list -> Lexicon
- val name_of_token: Token -> string
- val predef_term: string -> Token
+ include LEXICON0
+ val is_xid: string -> bool
+ val is_tfree: string -> bool
+ type lexicon
+ datatype token =
+ Token of string |
+ IdentSy of string |
+ VarSy of string |
+ TFreeSy of string |
+ TVarSy of string |
+ EndToken;
+ val id: string
+ val var: string
+ val tfree: string
+ val tvar: string
+ val str_of_token: token -> string
+ val display_token: token -> string
+ val matching_tokens: token * token -> bool
+ val valued_token: token -> bool
+ val predef_term: string -> token
val is_terminal: string -> bool
- val tokenize: Lexicon -> string -> Token list
- val token_to_string: Token -> string
- val valued_token: Token -> bool
- type 'b TokenMap
- val mkTokenMap: ('b * Token list) list -> 'b TokenMap
- val applyTokenMap: 'b TokenMap * Token -> 'b list
- include LEXICON0
+ val empty_lexicon: lexicon
+ val extend_lexicon: lexicon -> string list -> lexicon
+ val mk_lexicon: string list -> lexicon
+ val tokenize: lexicon -> bool -> string -> token list
+
+ exception LEXICAL_ERROR
+ val >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c
+ val || : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b
+ val -- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e
+ val ^^ : ('a -> string * 'b) * ('b -> string * 'c) -> 'a -> string * 'c
+ val $$ : ''a -> ''a list -> ''a * ''a list
+ val scan_empty: 'a list -> 'b list * 'a list
+ val scan_one: ('a -> bool) -> 'a list -> 'a * 'a list
+ val scan_any: ('a -> bool) -> 'a list -> 'a list * 'a list
+ val scan_any1: ('a -> bool) -> 'a list -> 'a list * 'a list
+ val scan_end: 'a list -> 'b list * 'a list
+ val optional: ('a -> 'b * 'a) -> 'a -> 'b option * 'a
+ val repeat: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
+ val repeat1: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
end;
-functor LexiconFun(Extension: EXTENSION): LEXICON =
+functor LexiconFun(): LEXICON =
struct
-open Extension;
+
+(** is_identifier etc. **)
+
+fun is_ident [] = false
+ | is_ident (c :: cs) = is_letter c andalso forall is_letdig cs;
+
+val is_identifier = is_ident o explode;
+
+fun is_xid s =
+ (case explode s of
+ "_" :: cs => is_ident cs
+ | cs => is_ident cs);
+
+fun is_tfree s =
+ (case explode s of
+ "'" :: cs => is_ident cs
+ | _ => false);
+
-datatype Token = Token of string
- | IdentSy of string
- | VarSy of string * int
- | TFreeSy of string
- | TVarSy of string * int
- | end_token;
-val no_token = "";
-
-datatype dfa = Tip | Branch of string * string * dfa * dfa * dfa;
-
-type Lexicon = dfa;
-
-fun is_id(c::cs) = is_letter(c) andalso forall is_letdig cs
- | is_id([]) = false;
-
-fun is_identifier s = is_id(explode s);
+(** string_of_vname **)
-val empty = Tip;
+fun string_of_vname (x, i) =
+ let
+ val si = string_of_int i;
+ in
+ if is_digit (last_elem (explode x)) then "?" ^ x ^ "." ^ si
+ else if i = 0 then "?" ^ x
+ else "?" ^ x ^ si
+ end;
-fun extend1(dfa, s) =
- let fun add(Branch(c, a, less, eq, gr), cs as (d::ds)) =
- if c>d then Branch(c, a, add(less, cs), eq, gr) else
- if c<d then Branch(c, a, less, eq, add(gr, cs)) else
- Branch(c, if null ds then s else a, less, add(eq, ds), gr)
- | add(Tip, c::cs) =
- Branch(c, if null cs then s else no_token, Tip, add(Tip, cs), Tip)
- | add(dfa, []) = dfa
+
- in add(dfa, explode s) end;
-
-val extend = foldl extend1;
-
-fun mk_lexicon ss = extend(empty, ss);
+(** datatype token **)
-fun next_dfa (Tip, _) = None
- | next_dfa (Branch(d, a, less, eq, gr), c) =
- if c<d then next_dfa(less, c) else
- if c>d then next_dfa(gr, c) else Some(a, eq);
-
-exception ID of string * string list;
-
-val eof_id = "End of input - identifier expected.\n";
+datatype token =
+ Token of string |
+ IdentSy of string |
+ VarSy of string |
+ TFreeSy of string |
+ TVarSy of string |
+ EndToken;
-(*A string of letters, digits, or ' _ *)
-fun xscan_ident exn =
-let fun scan [] = raise exn(eof_id, [])
- | scan(c::cs) =
- if is_letter c
- then let val (ds, tail) = take_prefix is_letdig cs
- in (implode(c::ds), tail) end
- else raise exn("Identifier expected: ", c::cs)
-in scan end;
-(*Scan the offset of a Var, if present; otherwise ~1 *)
-fun scan_offset cs = case cs of
- ("."::[]) => (~1, cs)
- | ("."::(ds as c::cs')) => if is_digit c then scan_int ds else (~1, cs)
- | _ => (~1, cs);
-
-fun split_varname s =
- let val (rpost, rpref) = take_prefix is_digit (rev(explode s))
- val (i, _) = scan_int(rev rpost)
- in (implode(rev rpref), i) end;
+(* names of valued tokens *)
-fun xscan_varname exn cs : (string*int) * string list =
-let val (a, ds) = xscan_ident exn cs;
- val (i, es) = scan_offset ds
-in if i = ~1 then (split_varname a, es) else ((a, i), es) end;
+val id = "id";
+val var = "var";
+val tfree = "tfree";
+val tvar = "tvar";
-fun scan_varname s = xscan_varname ID s
- handle ID(err, cs) => error(err^(implode cs));
-fun tokenize (dfa) (s:string) : Token list =
-let exception LEX_ERR;
- exception FAIL of string * string list;
- val lexerr = "Lexical error: ";
+(* str_of_token *)
- fun tokenize1 (_:dfa, []:string list) : Token * string list =
- raise LEX_ERR
- | tokenize1(dfa, c::cs) =
- case next_dfa(dfa, c) of
- None => raise LEX_ERR
- | Some(a, dfa') =>
- if a=no_token then tokenize1(dfa', cs)
- else (tokenize1(dfa', cs) handle LEX_ERR =>
- if is_identifier a andalso not(null cs) andalso
- is_letdig(hd cs)
- then raise LEX_ERR else (Token(a), cs));
+fun str_of_token (Token s) = s
+ | str_of_token (IdentSy s) = s
+ | str_of_token (VarSy s) = s
+ | str_of_token (TFreeSy s) = s
+ | str_of_token (TVarSy s) = s
+ | str_of_token EndToken = "";
- fun token(cs) = tokenize1(dfa, cs) handle LEX_ERR => raise FAIL(lexerr, cs);
+
+(* display_token *)
- fun id([]) = raise FAIL(eof_id, [])
- | id(cs as c::cs') =
- if is_letter(c)
- then let val (id, cs'') = xscan_ident FAIL cs
- in (IdentSy(id), cs'') end
- else
- if c = "?"
- then case cs' of
- "'"::xs => let val ((a, i), ys) = xscan_varname FAIL xs
- in (TVarSy("'"^a, i), ys) end
- | _ => let val ((a, i), ys) = xscan_varname FAIL cs'
- in (VarSy(a, i), ys) end
- else
- if c = "'"
- then let val (a, cs'') = xscan_ident FAIL cs'
- in (TFreeSy("'" ^ a), cs'') end
- else raise FAIL(lexerr, cs);
+fun display_token (Token s) = quote s
+ | display_token (IdentSy s) = "id(" ^ s ^ ")"
+ | display_token (VarSy s) = "var(" ^ s ^ ")"
+ | display_token (TFreeSy s) = "tfree(" ^ s ^ ")"
+ | display_token (TVarSy s) = "tvar(" ^ s ^ ")"
+ | display_token EndToken = "";
- fun tknize([], ts) = rev(ts)
- | tknize(cs as c::cs', ts) =
- if is_blank(c) then tknize(cs', ts) else
- let val (t, cs'') =
- if c="?" then id(cs) handle FAIL _ => token(cs)
- else (token(cs) handle FAIL _ => id(cs))
- in tknize(cs'', t::ts) end
+
+(* matching_tokens *)
-in tknize(explode s, []) handle FAIL(s, cs) => error(s^(implode cs)) end;
+fun matching_tokens (Token x, Token y) = (x = y)
+ | matching_tokens (IdentSy _, IdentSy _) = true
+ | matching_tokens (VarSy _, VarSy _) = true
+ | matching_tokens (TFreeSy _, TFreeSy _) = true
+ | matching_tokens (TVarSy _, TVarSy _) = true
+ | matching_tokens (EndToken, EndToken) = true
+ | matching_tokens _ = false;
-(*Variables have the form ?nameidx, or ?name.idx if "name" ends with a digit*)
-fun string_of_vname (a, idx) = case rev(explode a) of
- [] => "?NULL_VARIABLE_NAME"
- | c::_ => "?" ^
- (if is_digit c then a ^ "." ^ string_of_int idx
- else if idx = 0 then a
- else a ^ string_of_int idx);
-fun token_to_string (Token(s)) = s
- | token_to_string (IdentSy(s)) = s
- | token_to_string (VarSy v) = string_of_vname v
- | token_to_string (TFreeSy a) = a
- | token_to_string (TVarSy v) = string_of_vname v
- | token_to_string end_token = "\n";
+(* valued_token *)
-(* MMW *)
-fun name_of_token (Token s) = quote s
- | name_of_token (IdentSy _) = id
- | name_of_token (VarSy _) = var
- | name_of_token (TFreeSy _) = tfree
- | name_of_token (TVarSy _) = tvar;
+fun valued_token (Token _) = false
+ | valued_token (IdentSy _) = true
+ | valued_token (VarSy _) = true
+ | valued_token (TFreeSy _) = true
+ | valued_token (TVarSy _) = true
+ | valued_token EndToken = false;
-fun matching_tokens(Token(i), Token(j)) = (i=j) |
- matching_tokens(IdentSy(_), IdentSy(_)) = true |
- matching_tokens(VarSy _, VarSy _) = true |
- matching_tokens(TFreeSy _, TFreeSy _) = true |
- matching_tokens(TVarSy _, TVarSy _) = true |
- matching_tokens(end_token, end_token) = true |
- matching_tokens(_, _) = false;
-fun valued_token(end_token) = false
- | valued_token(Token _) = false
- | valued_token(IdentSy _) = true
- | valued_token(VarSy _) = true
- | valued_token(TFreeSy _) = true
- | valued_token(TVarSy _) = true;
+(* predef_term *)
-(* MMW *)
fun predef_term name =
if name = id then IdentSy name
- else if name = var then VarSy (name, 0)
+ else if name = var then VarSy name
else if name = tfree then TFreeSy name
- else if name = tvar then TVarSy (name, 0)
- else end_token;
+ else if name = tvar then TVarSy name
+ else EndToken;
-(* MMW *)
+
+(* is_terminal **)
+
fun is_terminal s = s mem [id, var, tfree, tvar];
-type 'b TokenMap = (Token * 'b list) list * 'b list;
-val first_token = 0;
+(** datatype lexicon **)
+
+datatype lexicon =
+ Empty |
+ Branch of string * string * lexicon * lexicon * lexicon;
+
+val no_token = "";
+
+
+(* empty_lexicon *)
+
+val empty_lexicon = Empty;
+
+
+(* extend_lexicon *)
+
+fun extend_lexicon lexicon strs =
+ let
+ fun ext (lex, s) =
+ let
+ fun add (Branch (d, a, lt, eq, gt)) (chs as c :: cs) =
+ if c < d then Branch (d, a, add lt chs, eq, gt)
+ else if c > d then Branch (d, a, lt, eq, add gt chs)
+ else Branch (d, if null cs then s else a, lt, add eq cs, gt)
+ | add Empty [c] =
+ Branch (c, s, Empty, Empty, Empty)
+ | add Empty (c :: cs) =
+ Branch (c, no_token, Empty, add Empty cs, Empty)
+ | add lex [] = lex;
+
+ val cs = explode s;
+ in
+ if exists is_blank cs then
+ error ("extend_lexicon: blank in literal " ^ quote s)
+ else add lex cs
+ end;
+ in
+ foldl ext (lexicon, strs)
+ end;
+
+
+(* mk_lexicon *)
+
+val mk_lexicon = extend_lexicon empty_lexicon;
+
+
+
+(** scanners **)
+
+exception LEXICAL_ERROR;
+
-fun int_of_token(Token(tk)) = first_token |
- int_of_token(IdentSy _) = first_token - 1 |
- int_of_token(VarSy _) = first_token - 2 |
- int_of_token(TFreeSy _) = first_token - 3 |
- int_of_token(TVarSy _) = first_token - 4 |
- int_of_token(end_token) = first_token - 5;
+(* scanner combinators *)
+
+fun (scan >> f) cs = apfst f (scan cs);
+
+fun (scan1 || scan2) cs = scan1 cs handle LEXICAL_ERROR => scan2 cs;
+
+fun (scan1 -- scan2) cs =
+ let
+ val (x, cs') = scan1 cs;
+ val (y, cs'') = scan2 cs';
+ in
+ ((x, y), cs'')
+ end;
+
+fun (scan1 ^^ scan2) = scan1 -- scan2 >> op ^;
+
+
+(* generic scanners *)
+
+fun $$ _ [] = raise LEXICAL_ERROR
+ | $$ a (c :: cs) =
+ if a = c then (c, cs) else raise LEXICAL_ERROR;
+
+fun scan_empty cs = ([], cs);
-fun lesstk(s, t) = int_of_token(s) < int_of_token(t) orelse
- (case (s, t) of (Token(a), Token(b)) => a<b | _ => false);
+fun scan_one _ [] = raise LEXICAL_ERROR
+ | scan_one pred (c :: cs) =
+ if pred c then (c, cs) else raise LEXICAL_ERROR;
+
+val scan_any = take_prefix;
+
+fun scan_any1 pred = scan_one pred -- scan_any pred >> op ::;
+
+fun scan_rest cs = (cs, []);
+
+fun scan_end [] = ([], [])
+ | scan_end _ = raise LEXICAL_ERROR;
+
+fun optional scan = scan >> Some || scan_empty >> K None;
+
+fun repeat scan cs = (scan -- repeat scan >> op :: || scan_empty) cs;
+
+fun repeat1 scan = scan -- repeat scan >> op ::;
+
+
+(* other scanners *)
+
+val scan_letter_letdigs = scan_one is_letter -- scan_any is_letdig >> op ::;
+
+val scan_digits1 = scan_any1 is_digit;
+
+val scan_id = scan_letter_letdigs >> implode;
-fun mkTokenMap(atll) =
- let val aill = atll;
- val dom = sort lesstk (distinct(flat(map snd aill)));
- val mt = map fst (filter (null o snd) atll);
- fun mktm(i) =
- let fun add(l, (a, il)) = if i mem il then a::l else l
- in (i, foldl add ([], aill)) end;
- in (map mktm dom, mt) end;
+val scan_id_nat =
+ scan_id ^^ ($$ "." ^^ (scan_digits1 >> implode) || scan_empty >> K "");
+
+
+(* scan_literal *)
+
+fun scan_literal lex chrs =
+ let
+ fun scan_lit _ s_cs [] = s_cs
+ | scan_lit Empty s_cs _ = s_cs
+ | scan_lit (Branch (d, a, lt, eq, gt)) s_cs (chs as c :: cs) =
+ if c < d then scan_lit lt s_cs chs
+ else if c > d then scan_lit gt s_cs chs
+ else scan_lit eq (if a = no_token then s_cs else Some (a, cs)) cs;
+ in
+ (case scan_lit lex None chrs of
+ None => raise LEXICAL_ERROR
+ | Some s_cs => s_cs)
+ end;
+
+
+
+(** tokenize **)
+
+fun tokenize lex xids str =
+ let
+ val scan_xid =
+ if xids then $$ "_" ^^ scan_id || scan_id
+ else scan_id;
+
+ val scan_lit = scan_literal lex >> pair Token;
+
+ val scan_ident =
+ $$ "?" ^^ $$ "'" ^^ scan_id_nat >> pair TVarSy ||
+ $$ "?" ^^ scan_id_nat >> pair VarSy ||
+ $$ "'" ^^ scan_id >> pair TFreeSy ||
+ scan_xid >> pair IdentSy;
+
+ fun scan_max_token cs =
+ (case (optional scan_lit cs, optional scan_ident cs) of
+ (tok1, (None, _)) => tok1
+ | ((None, _), tok2) => tok2
+ | (tok1 as (Some (_, s1), _), tok2 as (Some (_, s2), _)) =>
+ if size s1 >= size s2 then tok1 else tok2);
-fun find_al (i) =
- let fun find((j, al)::l) = if lesstk(i, j) then [] else
- if matching_tokens(i, j) then al else find l |
- find [] = [];
- in find end;
-fun applyTokenMap((l, mt), tk:Token) = mt@(find_al tk l);
+ fun scan_tokens [] rev_toks = rev (EndToken :: rev_toks)
+ | scan_tokens (chs as c :: cs) rev_toks =
+ if is_blank c then scan_tokens cs rev_toks
+ else
+ (case scan_max_token chs of
+ (None, _) => error ("Lexical error at: " ^ quote (implode chs))
+ | (Some (tk, s), chs') => scan_tokens chs' (tk s :: rev_toks));
+ in
+ scan_tokens (explode str) []
+ end;
+
+
+
+(** scan variables **)
+
+(* scan_vname *)
+
+fun scan_vname chrs =
+ let
+ fun nat_of_chs n [] = n
+ | nat_of_chs n (c :: cs) = nat_of_chs (n * 10 + (ord c - ord "0")) cs;
+
+ val nat_of = nat_of_chs 0;
+
+ fun split_vname chs =
+ let val (cs, ds) = take_suffix is_digit chs
+ in (implode cs, nat_of ds) end
+
+ val scan =
+ scan_letter_letdigs --
+ ($$ "." -- scan_digits1 >> (nat_of o #2) || scan_empty >> K ~1);
+ in
+ (case scan chrs of
+ ((cs, ~1), cs') => (split_vname cs, cs')
+ | ((cs, i), cs') => ((implode cs, i), cs'))
+ end;
+
+
+(* scan_varname *)
+
+fun scan_varname chs =
+ scan_vname chs handle LEXICAL_ERROR
+ => error ("scan_varname: bad varname " ^ quote (implode chs));
+
+
+(* scan_var *)
+
+fun scan_var str =
+ let
+ fun tvar (x, i) = Var (("'" ^ x, i), dummyT);
+ fun var x_i = Var (x_i, dummyT);
+ fun free x = Free (x, dummyT);
+
+ val scan =
+ $$ "?" -- $$ "'" -- scan_vname -- scan_end >> (tvar o #2 o #1) ||
+ $$ "?" -- scan_vname -- scan_end >> (var o #2 o #1) ||
+ scan_rest >> (free o implode);
+ in
+ #1 (scan (explode str))
+ end;
end;
--- a/src/Pure/Syntax/parse_tree.ML Fri Oct 01 13:26:22 1993 +0100
+++ b/src/Pure/Syntax/parse_tree.ML Mon Oct 04 15:30:49 1993 +0100
@@ -1,41 +1,38 @@
-(* Title: Pure/Syntax/parse_tree
+(* Title: Pure/Syntax/parse_tree.ML
ID: $Id$
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen
+
+TODO:
+ move parsetree to parser.ML
+ move pt_to_ast before ast_to_term (sextension.ML (?))
+ delete this file
*)
signature PARSE_TREE =
sig
+ structure Ast: AST
structure Lexicon: LEXICON
- structure Ast: AST
- local open Lexicon Ast in
- datatype ParseTree =
- Node of string * ParseTree list |
- Tip of Token
- val mk_pt: string * ParseTree list -> ParseTree
- val pt_to_ast: (string -> (ast list -> ast) option) -> ParseTree -> ast
+ local open Ast Lexicon in
+ datatype parsetree =
+ Node of string * parsetree list |
+ Tip of token
+ val pt_to_ast: (string -> (ast list -> ast) option) -> parsetree -> ast
end
end;
-functor ParseTreeFun(structure Lexicon: LEXICON and Ast: AST): PARSE_TREE =
+functor ParseTreeFun(structure Ast: AST and Lexicon: LEXICON): PARSE_TREE =
struct
+structure Ast = Ast;
structure Lexicon = Lexicon;
-structure Ast = Ast;
-open Lexicon Ast;
+open Ast Lexicon;
-(* datatype ParseTree *) (* FIXME rename *)
-
-datatype ParseTree =
- Node of string * ParseTree list |
- Tip of Token;
+(* datatype parsetree *)
-
-(* mk_pt *)
-
-fun mk_pt("", [pt]) = pt
- | mk_pt("", _) = error "mk_pt: funny copy op in parse tree"
- | mk_pt(s, ptl) = Node (s, ptl);
+datatype parsetree =
+ Node of string * parsetree list |
+ Tip of token;
(* pt_to_ast *)
@@ -45,17 +42,13 @@
fun trans a args =
(case trf a of
None => mk_appl (Constant a) args
- | Some f =>
- (f args) handle _ => error ("pt_to_ast: error in translation for " ^ a));
+ | Some f => f args handle exn
+ => (writeln ("Error in parse ast translation for " ^ quote a); raise exn));
- fun trav (Node (a, pts)) = trans a (map trav pts)
- | trav (Tip (IdentSy x)) = Variable x
- | trav (Tip (VarSy xi)) = Variable (string_of_vname xi)
- | trav (Tip (TFreeSy x)) = Variable x
- | trav (Tip (TVarSy xi)) = Variable (string_of_vname xi)
- | trav (Tip _) = error "pt_to_ast: unexpected token in parse tree";
+ fun ast_of (Node (a, pts)) = trans a (map ast_of pts)
+ | ast_of (Tip tok) = Variable (str_of_token tok);
in
- trav pt
+ ast_of pt
end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Syntax/parser.ML Mon Oct 04 15:30:49 1993 +0100
@@ -0,0 +1,347 @@
+(* Title: Pure/Syntax/parser.ML
+ Author: Sonia Mahjoub and Markus Wenzel, TU Muenchen
+
+Isabelle's main parser (used for terms and typs).
+
+TODO:
+ ~1 --> chain_pri
+ rename T, NT
+ improve syntax error
+ fix ambiguous grammar problem
+*)
+
+signature PARSER =
+sig
+ structure XGram: XGRAM
+ structure ParseTree: PARSE_TREE
+ local open XGram ParseTree ParseTree.Lexicon in
+ type gram
+ val empty_gram: gram
+ val extend_gram: gram -> string list -> string prod list -> gram
+ val mk_gram: string list -> string prod list -> gram
+ val parse: gram -> string -> token list -> parsetree
+ end
+end;
+
+functor ParserFun(structure Symtab: SYMTAB and XGram: XGRAM
+ and ParseTree: PARSE_TREE)(*: PARSER *) = (* FIXME *)
+struct
+
+structure XGram = XGram;
+structure ParseTree = ParseTree;
+structure Lexicon = ParseTree.Lexicon;
+open XGram ParseTree Lexicon;
+
+
+(** datatype gram **)
+
+datatype symb = T of token | NT of string * int;
+
+datatype gram =
+ Gram of string list * (symb list * string * int) list Symtab.table;
+
+
+(* empty_gram *)
+
+val empty_gram = Gram ([], Symtab.null);
+
+
+(* extend_gram *)
+
+(*prods are stored in reverse order*)
+
+fun extend_gram (Gram (roots, tab)) new_roots xprods =
+ let
+ fun symb_of (Terminal s) = Some (T (Token s))
+ | symb_of (Nonterminal (s, p)) =
+ (case predef_term s of
+ EndToken => Some (NT (s, p))
+ | tk => Some (T tk))
+ | symb_of _ = None;
+
+ fun prod_of (Prod (s, xsyms, c, p)) = (s, mapfilter symb_of xsyms, c, p);
+
+ fun add_prod (tab, (s, syms, c, p)) =
+ (case Symtab.lookup (tab, s) of
+ None => Symtab.update ((s, [(syms, c, p)]), tab)
+ | Some prods => Symtab.update ((s, (syms, c, p) :: prods), tab));
+ in
+ Gram (new_roots union roots,
+ Symtab.balance (foldl add_prod (tab, map prod_of xprods)))
+ end;
+
+
+(* mk_gram *)
+
+val mk_gram = extend_gram empty_gram;
+
+
+(* get_prods *)
+
+fun get_prods tab s pred =
+ let
+ fun rfilter [] ys = ys
+ | rfilter (x :: xs) ys = rfilter xs (if pred x then x :: ys else ys);
+ in
+ (case Symtab.lookup (tab, s) of
+ Some prods => rfilter prods []
+ | None => [])
+ end;
+
+
+
+(** parse **)
+
+type state =
+ string * int
+ * parsetree list (*before point*)
+ * symb list (*after point*)
+ * string * int;
+
+type earleystate = state list Array.array;
+
+
+
+fun getProductions tab A i =
+ get_prods tab A (fn (_, _, j) => j >= i orelse j = ~1);
+
+fun getProductions' tab A i k =
+ get_prods tab A (fn (_, _, j) => (j >= i andalso j < k) orelse j = ~1);
+
+
+
+fun mkState i jj A ([NT(B,~1)],id,~1) =
+ (A,max_pri,[],[NT (B,jj)],id,i)
+ | mkState i jj A (ss,id,j) = (A,j,[],ss,id,i) ;
+
+
+
+fun conc (t,(k:int)) [] = (None, [(t,k)])
+ | conc (t,k) ((t',k')::ts) =
+ if (t = t')
+ then (Some k', ( if k' >= k
+ then (t',k')::ts
+ else (t,k)::ts )
+ )
+ else let val (n, ts') = conc (t,k) ts
+ in (n, (t',k')::ts')
+ end;
+
+
+fun update_tree ((B,(i,ts))::used) (A,t) =
+ if (A = B)
+ then
+ let val (n,ts') = conc t ts
+ in ((A,(i,ts'))::used, n)
+ end
+ else
+ let val (used', n) = update_tree used (A,t)
+ in ((B,(i,ts)) :: used', n)
+ end;
+
+
+
+fun update_index ((B,(i,ts))::used) (A,j) =
+ if (A = B)
+ then (A,(j,ts)) :: used
+ else (B,(i,ts)) :: (update_index used (A,j));
+
+
+
+fun getS A i Si =
+ filter (fn (_,_,_,(NT(B,j))::_,_,_)
+ => (A=B andalso j<=i)
+ | _ => false
+ ) Si;
+
+
+
+fun getS' A k n Si =
+ filter (fn (_,_,_,(NT(B,j))::_,_,_) => (A=B andalso
+ j<=k andalso
+ j>n )
+ | _ => false
+ ) Si;
+
+
+
+fun getStates Estate i ii A k =
+ filter (fn (_,_,_,(NT(B,j))::_,_,_)
+ => (A=B andalso j<=k)
+ | _ => false
+ )
+ (Array.sub (Estate, ii))
+;
+
+
+
+(* MMW *)(* FIXME *)
+fun movedot_term (A,j,ts,T a::sa,id,i) c =
+ if (valued_token c)
+ then (A,j,(ts@[Tip c]),sa,id,i)
+ else (A,j,ts,sa,id,i) ;
+
+
+
+fun movedot_nonterm ts (A,j,tss,NT(B,k) ::sa,id,i) =
+ (A,j,tss@ts,sa,id,i) ;
+
+
+
+fun movedot_lambda _ [] = []
+ | movedot_lambda (B,j,tss,(NT(A,k))::sa,id,i) ((t,ki)::ts) =
+ if k <= ki
+ then (B,j,tss@t,sa,id,i) ::
+ (movedot_lambda (B,j,tss,(NT(A,k))::sa,id,i) ts)
+ else movedot_lambda (B,j,tss,(NT(A,k))::sa,id,i) ts
+ ;
+
+
+
+
+fun PROCESSS Estate grammar i c states =
+
+let
+fun processS used [] (Si,Sii) = (Si,Sii)
+ | processS used (S::States) (Si,Sii) =
+ ( case S of
+
+ (_,_,_,(NT (A,j))::_,_,_) =>
+ let
+ val (used_neu, States_neu) =
+ ( case assoc (used, A) of
+ Some (k,l) => (* A gehoert zu used *)
+
+ if (k <= j) (* Prioritaet wurde
+ behandelt *)
+ then
+ (used, movedot_lambda S l)
+
+ else (* Prioritaet wurde noch nicht
+ behandelt *)
+ let val L =
+ getProductions' grammar A j k
+ val States' = map (mkState i j A) L
+ in
+ (update_index used (A,j),
+ States'@ movedot_lambda S l
+ )
+ end
+
+ | None => (* A gehoert nicht zu used *)
+ let val L = getProductions grammar A j
+ val States' = map (mkState i j A) L
+ in
+ ((A,(j,[]))::used, States')
+ end
+ )
+ in
+ processS used_neu (States @ States_neu) (S::Si,Sii)
+ end
+
+ | (_,_,_,(T a)::_,_,_) =>
+ processS used States
+ (S::Si, if (matching_tokens (a, c))
+ then (movedot_term S c)::Sii (* MMW *)(* FIXME *)
+ else Sii
+ )
+
+
+ | (A,k,ts,[],id,j) =>
+ let val tt = if id = ""
+ then ts
+ else [Node(id,ts)]
+ in
+ if (j = i)
+ then
+ let val (used',O) = update_tree used (A,(tt,k))
+ in ( case O of
+ None =>
+ let val Slist = getS A k Si
+ val States' =
+ map (movedot_nonterm tt ) Slist
+ in processS used'
+ (States @ States') (S::Si,Sii)
+ end
+ | Some n =>
+ if (n >= k)
+ then
+ processS used' States (S::Si,Sii)
+ else
+ let val Slist = getS' A k n Si
+ val States' =
+ map (movedot_nonterm tt ) Slist
+ in
+ processS used'
+ (States @ States') (S::Si,Sii)
+ end
+ )
+ end
+
+ else
+ processS used (States @
+ map (movedot_nonterm tt)
+ (getStates Estate i j A k))
+ (S::Si,Sii)
+ end
+ )
+in
+ processS [] states ([],[])
+end;
+
+
+
+fun syntax_error toks =
+ error ("Syntax error at: " ^ space_implode " " (map str_of_token toks));
+
+fun Produce grammar stateset i indata =
+ case (Array.sub (stateset,i)) of
+ [] => syntax_error indata (* MMW *)(* FIXME *)
+ | s =>
+ (case indata of
+ [] => Array.sub (stateset,i)
+ | (c::cs) =>
+ let val (si,sii) =
+ PROCESSS stateset grammar i c s
+ in
+ Array.update (stateset,i,si);
+ Array.update (stateset,i+1,sii);
+ Produce grammar stateset (i+1) cs
+ end
+ );
+
+
+fun get_trees [] = []
+ | get_trees ((_,_,pt_lst,_,_,_) :: stateset) =
+ let val l = get_trees stateset
+ in case pt_lst of
+ [ptree] => ptree :: l
+ | _ => l
+ end;
+
+
+
+fun earley grammar startsymbol indata =
+ let val S0 =
+ [("S'",0,[],[NT (startsymbol,0), T EndToken],"",0)]
+ val s = length indata + 1 (* MMW *)(* FIXME was .. + 2 *)
+ val Estate = Array.array (s, [])
+ in Array.update (Estate,0,S0);
+ let val l = Produce grammar Estate 0 indata (* MMW *)(* FIXME was .. @ [EndToken] *)
+ val p_trees = get_trees l
+ in p_trees
+ end
+ end;
+
+
+(* FIXME demo *)
+fun parse (Gram (roots, prod_tab)) root toks =
+ if root mem roots then
+ (case earley prod_tab root toks of
+ [] => error "parse: no parse trees"
+ | pt :: _ => pt)
+ else error ("Unparsable category: " ^ root);
+
+
+end;
+
--- a/src/Pure/Syntax/pretty.ML Fri Oct 01 13:26:22 1993 +0100
+++ b/src/Pure/Syntax/pretty.ML Mon Oct 04 15:30:49 1993 +0100
@@ -1,9 +1,9 @@
-(* Title: Pure/Syntax/pretty
+(* Title: Pure/Syntax/pretty.ML
ID: $Id$
Author: Lawrence C Paulson
Copyright 1991 University of Cambridge
-Pretty printing module
+Generic pretty printing module.
Loosely based on
D. C. Oppen, "Pretty Printing",
@@ -20,24 +20,24 @@
a unit for breaking).
*)
-(* FIXME improve? *)
-type pprint_args = (string -> unit) * (int -> unit) * (int -> unit) * (unit -> unit);
+type pprint_args = (string -> unit) * (int -> unit) * (int -> unit) *
+ (unit -> unit) * (unit -> unit);
signature PRETTY =
- sig
+sig
type T
- val blk : int * T list -> T
- val brk : int -> T
- val fbrk : T
- val str : string -> T
- val lst : string * string -> T list -> T
- val quote : T -> T
- val string_of : T -> string
- val str_of : T -> string
- val pprint : T -> pprint_args -> unit
+ val blk: int * T list -> T
+ val brk: int -> T
+ val fbrk: T
+ val str: string -> T
+ val lst: string * string -> T list -> T
+ val quote: T -> T
+ val string_of: T -> string
+ val str_of: T -> string
+ val pprint: T -> pprint_args -> unit
val setdepth: int -> unit
val setmargin: int -> unit
- end;
+end;
functor PrettyFun () : PRETTY =
struct
@@ -159,23 +159,23 @@
fun string_of e = #tx (format ([prune (!depth) e],0,0) emptytext);
-fun brk_width (force, wd) = if force andalso wd = 0 then 1 else wd;
-
fun str_of prt =
let
fun s_of (Block (prts, _, _)) = implode (map s_of prts)
| s_of (String s) = s
- | s_of (Break f_w) = repstring " " (brk_width f_w);
+ | s_of (Break (false, wd)) = repstring " " wd
+ | s_of (Break (true, _)) = " ";
in
s_of (prune (! depth) prt)
end;
-fun pprint prt (put_str, begin_blk, put_brk, end_blk) =
+fun pprint prt (put_str, begin_blk, put_brk, put_fbrk, end_blk) =
let
fun pp (Block (prts, ind, _)) = (begin_blk ind; pp_lst prts; end_blk ())
| pp (String s) = put_str s
- | pp (Break f_w) = put_brk (brk_width f_w)
+ | pp (Break (false, wd)) = put_brk wd
+ | pp (Break (true, _)) = put_fbrk ()
and pp_lst [] = ()
| pp_lst (prt :: prts) = (pp prt; pp_lst prts);
in
--- a/src/Pure/Syntax/printer.ML Fri Oct 01 13:26:22 1993 +0100
+++ b/src/Pure/Syntax/printer.ML Mon Oct 04 15:30:49 1993 +0100
@@ -1,6 +1,8 @@
-(* Title: Pure/Syntax/printer
+(* Title: Pure/Syntax/printer.ML
ID: $Id$
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen
+
+Pretty printing of asts, terms, types and print (ast) translation.
*)
signature PRINTER0 =
@@ -16,14 +18,15 @@
structure XGram: XGRAM
structure Pretty: PRETTY
local open XGram XGram.Ast in
- val pretty_ast: ast -> Pretty.T
- val pretty_rule: (ast * ast) -> Pretty.T
val term_to_ast: (string -> (term list -> term) option) -> term -> ast
val typ_to_ast: (string -> (term list -> term) option) -> typ -> ast
- type tab
- val mk_print_tab: (string prod list) -> (ast list -> ast) Symtab.table -> tab
- val pretty_term_ast: tab -> ast -> Pretty.T
- val pretty_typ_ast: tab -> ast -> Pretty.T
+ type prtab
+ val empty_prtab: prtab
+ val extend_prtab: prtab -> (string prod list) -> (string * (ast list -> ast)) list
+ -> prtab
+ val mk_prtab: (string prod list) -> (string * (ast list -> ast)) list -> prtab
+ val pretty_term_ast: prtab -> ast -> Pretty.T
+ val pretty_typ_ast: prtab -> ast -> Pretty.T
end
end;
@@ -46,36 +49,27 @@
-(** simple prettying **)
-
-(* pretty_ast *)
-
-fun pretty_ast (Constant a) = Pretty.str (quote a)
- | pretty_ast (Variable x) = Pretty.str x
- | pretty_ast (Appl asts) =
- Pretty.blk
- (2, (Pretty.str "(") ::
- (separate (Pretty.brk 1) (map pretty_ast asts)) @ [Pretty.str ")"]);
-
+(** convert term or typ to ast **)
-(* pretty_rule *)
-
-fun pretty_rule (lhs, rhs) =
- Pretty.blk
- (2, [pretty_ast lhs, Pretty.str " ->", Pretty.brk 2, pretty_ast rhs]);
-
-
-
-(** convert term/typ to ast **) (* FIXME check *)
-
-fun apply_trans a f args =
- ((f args) handle
+fun apply_trans name a f args =
+ (f args handle
Match => raise Match
- | exn => (writeln ("Error in translation for " ^ quote a); raise exn));
+ | exn => (writeln ("Error in " ^ name ^ " for " ^ quote a); raise exn));
fun ast_of_term trf show_types show_sorts tm =
let
+(*(* FIXME old - remove *)
+ fun fix_aprop tys (Abs (x, ty, t)) = Abs (x, ty, fix_aprop (ty :: tys) t)
+ | fix_aprop tys t =
+ let
+ val (f, args) = strip_comb t;
+ val t' = list_comb (f, map (fix_aprop tys) args);
+ in
+ if not (is_Const f) andalso fastype_of (tys, t) = propT
+ then Const (apropC, dummyT) $ t' else t'
+ end;
+
val aprop_const = Const (apropC, dummyT);
fun fix_aprop (tm as Const _) = tm
@@ -87,6 +81,28 @@
| fix_aprop (Abs (x, ty, t)) = Abs (x, ty, fix_aprop t)
| fix_aprop (t1 $ t2) = fix_aprop t1 $ fix_aprop t2;
+ val fix_aprop = fn _ => fn tm => fix_aprop tm;
+*)
+
+ (* FIXME check *)
+
+ fun aprop t = Const (apropC, dummyT) $ t;
+
+ fun is_prop tys tm =
+ fastype_of (tys, tm) = propT handle TERM _ => false;
+
+ fun fix_aprop _ (tm as Const _) = tm
+ | fix_aprop _ (tm as Free (x, ty)) =
+ if ty = propT then aprop (Free (x, dummyT)) else tm
+ | fix_aprop _ (tm as Var (xi, ty)) =
+ if ty = propT then aprop (Var (xi, dummyT)) else tm
+ | fix_aprop tys (tm as Bound _) =
+ if is_prop tys tm then aprop tm else tm
+ | fix_aprop tys (Abs (x, ty, t)) = Abs (x, ty, fix_aprop (ty :: tys) t)
+ | fix_aprop tys (tm as t1 $ t2) =
+ (if is_Const (head_of tm) orelse not (is_prop tys tm)
+ then I else aprop) (fix_aprop tys t1 $ fix_aprop tys t2);
+
fun prune_typs (t_seen as (Const _, _)) = t_seen
| prune_typs (t as Free (x, ty), seen) =
@@ -122,7 +138,7 @@
and trans a args =
(case trf a of
- Some f => ast_of (apply_trans a f args)
+ Some f => ast_of (apply_trans "print translation" a f args)
| None => raise Match)
handle Match => mk_appl (Constant a) (map ast_of args)
@@ -131,8 +147,8 @@
ast_of (Const (constrainC, dummyT) $ t $ term_of_typ show_sorts ty)
else Variable x;
in
- if show_types then ast_of (fst (prune_typs (fix_aprop tm, [])))
- else ast_of (fix_aprop tm)
+ if show_types then ast_of (#1 (prune_typs (fix_aprop [] tm, [])))
+ else ast_of (fix_aprop [] tm)
end;
@@ -149,7 +165,7 @@
-(** type tab **)
+(** type prtab **)
datatype symb =
Arg of int |
@@ -163,13 +179,18 @@
Trns of ast list -> ast |
TorP of (ast list -> ast) * (symb list * int * int);
-type tab = format Symtab.table;
+type prtab = format Symtab.table;
+
+
+(* empty_prtab *)
+
+val empty_prtab = Symtab.null;
-(** mk_print_tab **)
+(** extend_prtab **)
-fun mk_print_tab prods ast_trans =
+fun extend_prtab prtab prods trfuns =
let
fun nargs (Arg _ :: symbs) = nargs symbs + 1
| nargs (TypArg _ :: symbs) = nargs symbs + 1
@@ -181,15 +202,15 @@
fun merge (s, String s' :: l) = String (s ^ s') :: l
| merge (s, l) = String s :: l;
- fun mk_prnp sy opn p =
+ fun mk_prnp sy c p =
let
- val constr = (opn = constrainC orelse opn = constrainIdtC);
+ val constr = (c = constrainC orelse c = constrainIdtC);
fun syn2pr (Terminal s :: sy) =
- let val (symbs, sy') = syn2pr sy
+ let val (symbs, sy') = syn2pr sy;
in (merge (s, symbs), sy') end
| syn2pr (Space s :: sy) =
- let val (symbs, sy') = syn2pr sy
+ let val (symbs, sy') = syn2pr sy;
in (merge (s, symbs), sy') end
| syn2pr (Nonterminal (s, p) :: sy) =
let
@@ -204,7 +225,7 @@
val (symbs, sy'') = syn2pr sy';
in (Block (i, bsymbs) :: symbs, sy'') end
| syn2pr (Brk i :: sy) =
- let val (symbs, sy') = syn2pr sy
+ let val (symbs, sy') = syn2pr sy;
in (Break i :: symbs, sy') end
| syn2pr (En :: sy) = ([], sy)
| syn2pr [] = ([], []);
@@ -214,38 +235,54 @@
(pr, nargs pr, p)
end;
- fun add_prod (Prod (_, _, "", _), tab) = tab
- | add_prod (Prod (_, sy, opn, p), tab) =
- (case Symtab.lookup (tab, opn) of
- None => Symtab.update ((opn, Prnt (mk_prnp sy opn p)), tab)
- | Some (Prnt _) => tab
- | Some (Trns f) => Symtab.update ((opn, TorP (f, mk_prnp sy opn p)), tab)
- | Some (TorP _) => tab);
+ fun trns_err c = error ("More than one parse ast translation for " ^ quote c);
+
+ fun add_fmt tab c fmt x = Symtab.update ((c, fmt x), tab);
- fun add_tr (tab, (opn, f)) = Symtab.update_new ((opn, Trns f), tab);
+ fun add_prod (tab, Prod (_, _, "", _)) = tab
+ | add_prod (tab, Prod (_, sy, c, p)) =
+ (case Symtab.lookup (tab, c) of
+ None => add_fmt tab c Prnt (mk_prnp sy c p)
+ | Some (Prnt _) => add_fmt tab c Prnt (mk_prnp sy c p)
+ | Some (Trns f) => add_fmt tab c TorP (f, mk_prnp sy c p)
+ | Some (TorP (f, _)) => add_fmt tab c TorP (f, mk_prnp sy c p));
+
+ fun add_tr (tab, (c, f)) =
+ (case Symtab.lookup (tab, c) of
+ None => add_fmt tab c Trns f
+ | Some (Prnt pr) => add_fmt tab c TorP (f, pr)
+ | Some (Trns _) => trns_err c
+ | Some (TorP _) => trns_err c);
in
- Symtab.balance
- (foldr add_prod
- (prods, foldl add_tr (Symtab.null, Symtab.alist_of ast_trans)))
+ Symtab.balance (foldl add_prod (foldl add_tr (prtab, trfuns), prods))
end;
+(* mk_prtab *)
-(** pretty term/typ asts **) (* FIXME check *)
+val mk_prtab = extend_prtab empty_prtab;
+
+
+
+(** pretty term/typ asts **)
-(*assumes a syntax derived from Pure*)
+(*pretty assumes a syntax derived from Pure, otherwise it may loop forever*)
-fun pretty tab appT ast0 p0 =
+fun pretty tab type_mode ast0 p0 =
let
+ val trans = apply_trans "print ast translation";
+
+ val appT = if type_mode then tappl_ast_tr' else appl_ast_tr';
+
fun synT ([], args) = ([], args)
| synT (Arg p :: symbs, t :: args) =
- let val (Ts, args') = synT (symbs, args)
+ let val (Ts, args') = synT (symbs, args);
in (astT (t, p) @ Ts, args') end
| synT (TypArg p :: symbs, t :: args) =
- let val (Ts, args') = synT (symbs, args)
- in (pretty tab tappl_ast_tr' t p @ Ts, args') end
+ let val (Ts, args') = synT (symbs, args);
+ in (pretty tab true t p @ Ts, args') end
| synT (String s :: symbs, args) =
- let val (Ts, args') = synT (symbs, args)
+ let val (Ts, args') = synT (symbs, args);
in (Pretty.str s :: Ts, args') end
| synT (Block (i, bsymbs) :: symbs, args) =
let
@@ -253,39 +290,47 @@
val (Ts, args'') = synT (symbs, args');
in (Pretty.blk (i, bTs) :: Ts, args'') end
| synT (Break i :: symbs, args) =
- let val (Ts, args') = synT (symbs, args)
- in (Pretty.brk i :: Ts, args') end
+ let val (Ts, args') = synT (symbs, args);
+ in ((if i < 0 then Pretty.fbrk else Pretty.brk i) :: Ts, args') end
| synT (_ :: _, []) = error "synT"
and parT (pr, args, p, p': int) =
- if p > p' then fst (synT ([Block(1, String"(" :: pr @ [String")"])], args))
- else fst (synT (pr, args))
+ if p > p' then
+ #1 (synT ([Block (1, String "(" :: pr @ [String ")"])], args))
+ else #1 (synT (pr, args))
and prefixT (_, a, [], _) = [Pretty.str a]
| prefixT (c, _, args, p) = astT (appT (c, args), p)
+ and splitT 0 ([x], ys) = (x, ys)
+ | splitT 0 (rev_xs, ys) = (Appl (rev rev_xs), ys)
+ | splitT n (rev_xs, y :: ys) = splitT (n - 1) (y :: rev_xs, ys)
+ | splitT _ _ = error "splitT"
+
and combT (tup as (c, a, args, p)) =
let
val nargs = length args;
+
fun prnt (pr, n, p') =
- if n = nargs then parT (pr, args, p, p')
- else if n > nargs then prefixT tup
- else astT (appT (c, args), p); (* FIXME ??? *)
+ if nargs = n then parT (pr, args, p, p')
+ else if nargs < n orelse type_mode then prefixT tup
+ else astT (appT (splitT n ([c], args)), p);
in
- case Symtab.lookup (tab, a) of
+ (case Symtab.lookup (tab, a) of
None => prefixT tup
| Some (Prnt prnp) => prnt prnp
| Some (Trns f) =>
- (astT (apply_trans a f args, p) handle Match => prefixT tup)
+ (astT (trans a f args, p) handle Match => prefixT tup)
| Some (TorP (f, prnp)) =>
- (astT (apply_trans a f args, p) handle Match => prnt prnp)
+ (astT (trans a f args, p) handle Match => prnt prnp))
end
and astT (c as Constant a, p) = combT (c, a, [], p)
| astT (Variable x, _) = [Pretty.str x]
- | astT (Appl ((c as Constant a) :: args), p) = combT (c, a, args, p)
+ | astT (Appl ((c as Constant a) :: (args as _ :: _)), p) =
+ combT (c, a, args, p)
| astT (Appl (f :: (args as _ :: _)), p) = astT (appT (f, args), p)
- | astT (ast as (Appl _), _) = raise_ast "pretty: malformed ast" [ast];
+ | astT (ast as Appl _, _) = raise_ast "pretty: malformed ast" [ast];
in
astT (ast0, p0)
end;
@@ -294,13 +339,13 @@
(* pretty_term_ast *)
fun pretty_term_ast tab ast =
- Pretty.blk (0, pretty tab appl_ast_tr' ast 0);
+ Pretty.blk (0, pretty tab false ast 0);
(* pretty_typ_ast *)
fun pretty_typ_ast tab ast =
- Pretty.blk (0, pretty tab tappl_ast_tr' ast 0);
+ Pretty.blk (0, pretty tab true ast 0);
end;
--- a/src/Pure/Syntax/sextension.ML Fri Oct 01 13:26:22 1993 +0100
+++ b/src/Pure/Syntax/sextension.ML Mon Oct 04 15:30:49 1993 +0100
@@ -1,21 +1,14 @@
-(* Title: Pure/Syntax/sextension
+(* Title: Pure/Syntax/sextension.ML
ID: $Id$
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen
-Syntax extensions: mixfix declarations, syntax rules, infixes, binders and
-the Pure syntax.
+Syntax extensions (external interface): mixfix declarations, syntax rules,
+infixes, binders and the Pure syntax.
-Changes:
- SEXTENSION: added Ast, xrule
- changed sext
- added ast_to_term
- ext_of_sext: added xconsts
- SEXTENSION1: added empty_sext, appl_ast_tr'
- SEXTENSION1: removed appl_tr'
TODO:
+ move ast_to_term (?)
*)
-
infix |-> <-| <->;
signature SEXTENSION0 =
@@ -43,17 +36,13 @@
mixfix: mixfix list,
xrules: xrule list,
parse_ast_translation: (string * (ast list -> ast)) list,
- parse_preproc: (ast -> ast) option,
- parse_postproc: (ast -> ast) option,
parse_translation: (string * (term list -> term)) list,
print_translation: (string * (term list -> term)) list,
- print_preproc: (ast -> ast) option,
- print_postproc: (ast -> ast) option,
print_ast_translation: (string * (ast list -> ast)) list}
val eta_contract: bool ref
val mk_binder_tr: string * string -> string * (term list -> term)
val mk_binder_tr': string * string -> string * (term list -> term)
- val ndependent_tr: string -> term list -> term
+ val ndependent_tr: string -> term list -> term (* FIXME remove *)
val dependent_tr': string * string -> term list -> term
val max_pri: int
end
@@ -86,12 +75,12 @@
end
end;
-functor SExtensionFun(structure TypeExt: TYPE_EXT and Lexicon: LEXICON)(*: SEXTENSION *) = (* FIXME *)
+functor SExtensionFun(structure TypeExt: TYPE_EXT and Lexicon: LEXICON): SEXTENSION =
struct
structure Extension = TypeExt.Extension;
structure Ast = Extension.XGram.Ast;
-open Extension Ast;
+open Lexicon Extension Extension.XGram Ast;
(** datatype sext **)
@@ -119,12 +108,8 @@
mixfix: mixfix list,
xrules: xrule list,
parse_ast_translation: (string * (ast list -> ast)) list,
- parse_preproc: (ast -> ast) option,
- parse_postproc: (ast -> ast) option,
parse_translation: (string * (term list -> term)) list,
print_translation: (string * (term list -> term)) list,
- print_preproc: (ast -> ast) option,
- print_postproc: (ast -> ast) option,
print_ast_translation: (string * (ast list -> ast)) list};
@@ -145,12 +130,8 @@
{mixfix = mixfix,
xrules = [],
parse_ast_translation = [],
- parse_preproc = None,
- parse_postproc = None,
parse_translation = parse_translation,
print_translation = print_translation,
- print_preproc = None,
- print_postproc = None,
print_ast_translation = []}
| sext_components (NewSext cmps) = cmps;
@@ -168,7 +149,7 @@
-(** parse translations **)
+(** parse (ast) translations **)
(* application *)
@@ -182,18 +163,24 @@
| idtyp_ast_tr (*"_idtyp"*) asts = raise_ast "idtyp_ast_tr" asts;
fun lambda_ast_tr (*"_lambda"*) [idts, body] =
- fold_ast_p "_%" (unfold_ast "_idts" idts, body)
+ fold_ast_p "_abs" (unfold_ast "_idts" idts, body)
| lambda_ast_tr (*"_lambda"*) asts = raise_ast "lambda_ast_tr" asts;
-fun abs_tr (*"_%"*) [Free (x, T), body] = absfree (x, T, body)
- | abs_tr (*"_%"*) (ts as [Const (c, _) $ Free (x, T) $ tT, body]) =
+fun abs_tr (*"_abs"*) [Free (x, T), body] = absfree (x, T, body)
+ | abs_tr (*"_abs"*) (ts as [Const (c, _) $ Free (x, T) $ tT, body]) =
if c = constrainC then
Const ("_constrainAbs", dummyT) $ absfree (x, T, body) $ tT
- else raise (TERM ("abs_tr", ts))
- | abs_tr (*"_%"*) ts = raise (TERM ("abs_tr", ts));
+ else raise_term "abs_tr" ts
+ | abs_tr (*"_abs"*) ts = raise_term "abs_tr" ts;
-(* binder *) (* FIXME check *) (* FIXME check *)
+(* nondependent abstraction *)
+
+fun k_tr (*"_K"*) [t] = Abs ("x", dummyT, incr_boundvars 1 t)
+ | k_tr (*"_K"*) ts = raise_term "k_tr" ts;
+
+
+(* binder *)
fun mk_binder_tr (sy, name) =
let
@@ -201,14 +188,14 @@
fun tr (Free (x, T), t) = const $ absfree (x, T, t)
| tr (Const ("_idts", _) $ idt $ idts, t) = tr (idt, tr (idts, t))
- | tr (t1 as (Const (c, _) $ Free (x, T) $ tT), t) = (* FIXME *)
+ | tr (t1 as Const (c, _) $ Free (x, T) $ tT, t) =
if c = constrainC then
const $ (Const ("_constrainAbs", dummyT) $ absfree (x, T, t) $ tT)
- else raise (TERM ("binder_tr", [t1, t]))
- | tr (t1, t2) = raise (TERM ("binder_tr", [t1, t2]));
+ else raise_term "binder_tr" [t1, t]
+ | tr (t1, t2) = raise_term "binder_tr" [t1, t2];
fun binder_tr (*sy*) [idts, body] = tr (idts, body)
- | binder_tr (*sy*) ts = raise (TERM ("binder_tr", ts));
+ | binder_tr (*sy*) ts = raise_term "binder_tr" ts;
in
(sy, binder_tr)
end;
@@ -216,8 +203,9 @@
(* atomic props *)
-fun aprop_ast_tr (*"_aprop"*) [ast] = ast
- | aprop_ast_tr (*"_aprop"*) asts = raise_ast "aprop_ast_tr" asts;
+fun aprop_tr (*"_aprop"*) [t] =
+ Const (constrainC, dummyT) $ t $ Free ("prop", dummyT)
+ | aprop_tr (*"_aprop"*) ts = raise_term "aprop_tr" ts;
(* meta implication *)
@@ -227,15 +215,15 @@
| bigimpl_ast_tr (*"_bigimpl"*) asts = raise_ast "bigimpl_ast_tr" asts;
-(* 'dependent' type operators *)
+(* 'dependent' type operators *) (* FIXME remove *)
fun ndependent_tr q [A, B] =
Const (q, dummyT) $ A $ Abs ("x", dummyT, incr_boundvars 1 B)
- | ndependent_tr _ _ = raise Match;
+ | ndependent_tr _ ts = raise_term "ndependent_tr" ts;
-(** print translations **)
+(** print (ast) translations **)
(* application *)
@@ -243,16 +231,17 @@
| appl_ast_tr' (f, args) = Appl [Constant "_appl", f, fold_ast "_args" args];
-(* abstraction *) (* FIXME check *)
+(* abstraction *)
fun strip_abss vars_of body_of tm =
let
+ fun free (x, _) = Free (x, dummyT);
+
val vars = vars_of tm;
val body = body_of tm;
val rev_new_vars = rename_wrt_term body vars;
in
- (map Free (rev rev_new_vars),
- subst_bounds (map (fn (x, _) => Free (x, dummyT)) rev_new_vars, body))
+ (map Free (rev rev_new_vars), subst_bounds (map free rev_new_vars, body))
end;
(*do (partial) eta-contraction before printing*)
@@ -263,7 +252,7 @@
let
fun eta_abs (Abs (a, T, t)) =
(case eta_abs t of
- t' as (f $ u) =>
+ t' as f $ u =>
(case eta_abs u of
Bound 0 =>
if not (0 mem loose_bnos f) then incr_boundvars ~1 f
@@ -277,17 +266,17 @@
fun abs_tr' tm =
- foldr (fn (x, t) => Const ("_%", dummyT) $ x $ t)
+ foldr (fn (x, t) => Const ("_abs", dummyT) $ x $ t)
(strip_abss strip_abs_vars strip_abs_body (eta_contr tm));
-fun lambda_ast_tr' (*"_%"*) asts =
- (case unfold_ast_p "_%" (Appl (Constant "_%" :: asts)) of
- ([], _) => raise_ast "lambda_ast_tr'" asts
+fun abs_ast_tr' (*"_abs"*) asts =
+ (case unfold_ast_p "_abs" (Appl (Constant "_abs" :: asts)) of
+ ([], _) => raise_ast "abs_ast_tr'" asts
| (xs, body) => Appl [Constant "_lambda", fold_ast "_idts" xs, body]);
-(* binder *) (* FIXME check *)
+(* binder *)
fun mk_binder_tr' (name, sy) =
let
@@ -323,59 +312,43 @@
fun impl_ast_tr' (*"==>"*) asts =
(case unfold_ast_p "==>" (Appl (Constant "==>" :: asts)) of
- (asms as (_ :: _ :: _), concl)
+ (asms as _ :: _ :: _, concl)
=> Appl [Constant "_bigimpl", fold_ast "_asms" asms, concl]
| _ => raise Match);
-(* 'dependent' type operators *)
+(* dependent / nondependent quantifiers *)
-fun dependent_tr' (q, r) [A, Abs (x, T, B)] =
+fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) =
if 0 mem (loose_bnos B) then
let val (x', B') = variant_abs (x, dummyT, B);
- in Const (q, dummyT) $ Free (x', T) $ A $ B' end
- else Const (r, dummyT) $ A $ B
+ in list_comb (Const (q, dummyT) $ Free (x', T) $ A $ B', ts) end
+ else list_comb (Const (r, dummyT) $ A $ B, ts)
| dependent_tr' _ _ = raise Match;
-(** constants **)
-
-(* FIXME opn, clean: move *)
-val clean =
- let
- fun q ("'" :: c :: cs) = c ^ q cs
- | q (c :: cs) = c ^ q cs
- | q ([]) = ""
- in q o explode end;
-
-val opn = "op ";
+(** ext_of_sext **)
-
-fun constants sext =
+fun strip_esc str =
let
- fun consts (Delimfix (_, ty, c)) = ([c], ty)
- | consts (Mixfix (_, ty, c, _, _)) = ([c], ty)
- | consts (Infixl (c, ty, _)) = ([opn ^ clean c], ty)
- | consts (Infixr (c, ty, _)) = ([opn ^ clean c], ty)
- | consts (Binder (_, ty, c, _, _)) = ([c], ty)
- | consts _ = ([""], ""); (*is filtered out below*)
+ fun strip ("'" :: c :: cs) = c :: strip cs
+ | strip ["'"] = []
+ | strip (c :: cs) = c :: strip cs
+ | strip [] = [];
in
- distinct (filter_out (fn (l, _) => l = [""]) (map consts (mixfix_of sext)))
+ implode (strip (explode str))
end;
-
+fun infix_name sy = "op " ^ strip_esc sy;
-(** ext_of_sext **) (* FIXME check, clean *)
fun ext_of_sext roots xconsts read_typ sext =
let
- val
- {mixfix, parse_ast_translation, parse_preproc, parse_postproc,
- parse_translation, print_translation, print_preproc, print_postproc,
- print_ast_translation, ...} = sext_components sext;
+ val {mixfix, parse_ast_translation, parse_translation, print_translation,
+ print_ast_translation, ...} = sext_components sext;
- val infixT = [typeT, typeT] ---> typeT;
+ val tinfixT = [typeT, typeT] ---> typeT;
fun binder (Binder (sy, _, name, _, _)) = Some (sy, name)
| binder _ = None;
@@ -384,79 +357,76 @@
(case read_typ ty of
Type ("fun", [Type ("fun", [_, T2]), T3]) =>
[Type ("idts", []), T2] ---> T3
- | _ => error (quote ty ^ " is not a valid binder type."));
+ | _ => error ("Illegal binder type " ^ quote ty));
- fun mfix_of (Mixfix (sy, ty, c, pl, p)) = [Mfix (sy, read_typ ty, c, pl, p)]
+ fun mk_infix sy T c p1 p2 p3 =
+ [Mfix ("op " ^ sy, T, c, [], max_pri),
+ Mfix ("(_ " ^ sy ^ "/ _)", T, c, [p1, p2], p3)];
+
+ fun mfix_of (Mixfix (sy, ty, c, ps, p)) = [Mfix (sy, read_typ ty, c, ps, p)]
| mfix_of (Delimfix (sy, ty, c)) = [Mfix (sy, read_typ ty, c, [], max_pri)]
| mfix_of (Infixl (sy, ty, p)) =
- let val T = read_typ ty and c = opn ^ sy and c' = opn ^ clean sy
- in
- [Mfix (c, T, c', [], max_pri),
- Mfix("(_ " ^ sy ^ "/ _)", T, c', [p, p + 1], p)]
- end
+ mk_infix sy (read_typ ty) (infix_name sy) p (p + 1) p
| mfix_of (Infixr (sy, ty, p)) =
- let val T = read_typ ty and c = opn ^ sy and c' = opn ^ clean sy
- in
- [Mfix(c, T, c', [], max_pri),
- Mfix("(_ " ^ sy ^ "/ _)", T, c', [p + 1, p], p)]
- end
+ mk_infix sy (read_typ ty) (infix_name sy) (p + 1) p p
| mfix_of (Binder (sy, ty, _, p, q)) =
[Mfix ("(3" ^ sy ^ "_./ _)", binder_typ ty, sy, [0, p], q)]
| mfix_of (TInfixl (s, c, p)) =
- [Mfix ("(_ " ^ s ^ "/ _)", infixT, c, [p, p + 1], p)]
+ [Mfix ("(_ " ^ s ^ "/ _)", tinfixT, c, [p, p + 1], p)]
| mfix_of (TInfixr (s, c, p)) =
- [Mfix ("(_ " ^ s ^ "/ _)", infixT, c, [p + 1, p], p)];
+ [Mfix ("(_ " ^ s ^ "/ _)", tinfixT, c, [p + 1, p], p)];
val mfix = flat (map mfix_of mixfix);
- val mfix_consts = map (fn (Mfix (_, _, c, _, _)) => c) mfix;
- val bs = mapfilter binder mixfix;
- val bparses = map mk_binder_tr bs;
- val bprints = map (mk_binder_tr' o (fn (x, y) => (y, x))) bs;
+ val binders = mapfilter binder mixfix;
+ val bparses = map mk_binder_tr binders;
+ val bprints = map (mk_binder_tr' o (fn (x, y) => (y, x))) binders;
in
Ext {
roots = roots, mfix = mfix,
- extra_consts = distinct (filter Lexicon.is_identifier (xconsts @ mfix_consts)),
+ extra_consts = distinct (filter is_xid xconsts),
parse_ast_translation = parse_ast_translation,
- parse_preproc = parse_preproc,
- parse_postproc = parse_postproc,
parse_translation = bparses @ parse_translation,
print_translation = bprints @ print_translation,
- print_preproc = print_preproc,
- print_postproc = print_postproc,
print_ast_translation = print_ast_translation}
end;
+(** constants **)
+
+fun constants sext =
+ let
+ fun consts (Delimfix (_, ty, c)) = ([c], ty)
+ | consts (Mixfix (_, ty, c, _, _)) = ([c], ty)
+ | consts (Infixl (c, ty, _)) = ([infix_name c], ty)
+ | consts (Infixr (c, ty, _)) = ([infix_name c], ty)
+ | consts (Binder (_, ty, c, _, _)) = ([c], ty)
+ | consts _ = ([""], ""); (*is filtered out below*)
+ in
+ distinct (filter_out (fn (l, _) => l = [""]) (map consts (mixfix_of sext)))
+ end;
+
+
+
(** ast_to_term **)
fun ast_to_term trf ast =
let
- fun scan_vname prfx cs =
- (case Lexicon.scan_varname cs of
- ((x, i), []) => Var ((prfx ^ x, i), dummyT)
- | _ => error ("ast_to_term: bad variable name " ^ quote (implode cs)));
-
- fun vname_to_var v =
- (case explode v of
- "?" :: "'" :: cs => scan_vname "'" cs
- | "?" :: cs => scan_vname "" cs
- | _ => Free (v, dummyT));
-
fun trans a args =
(case trf a of
None => list_comb (Const (a, dummyT), args)
- | Some f => ((f args)
- handle _ => error ("ast_to_term: error in translation for " ^ quote a)));
+ | Some f => f args handle exn
+ => (writeln ("Error in parse translation for " ^ quote a); raise exn));
- fun trav (Constant a) = trans a []
- | trav (Appl (Constant a :: (asts as _ :: _))) = trans a (map trav asts)
- | trav (Appl (ast :: (asts as _ :: _))) =
- list_comb (trav ast, map trav asts)
- | trav (ast as (Appl _)) = raise_ast "ast_to_term: malformed ast" [ast]
- | trav (Variable x) = vname_to_var x;
+ fun term_of (Constant a) = trans a []
+ | term_of (Variable x) = scan_var x
+ | term_of (Appl (Constant a :: (asts as _ :: _))) =
+ trans a (map term_of asts)
+ | term_of (Appl (ast :: (asts as _ :: _))) =
+ list_comb (term_of ast, map term_of asts)
+ | term_of (ast as Appl _) = raise_ast "ast_to_term: malformed ast" [ast];
in
- trav ast
+ term_of ast
end;
@@ -488,19 +458,14 @@
xrules = [],
parse_ast_translation =
[(applC, appl_ast_tr), ("_lambda", lambda_ast_tr), ("_idtyp", idtyp_ast_tr),
- ("_aprop", aprop_ast_tr), ("_bigimpl", bigimpl_ast_tr)],
- parse_preproc = None,
- parse_postproc = None,
- parse_translation = [("_%", abs_tr)],
+ ("_bigimpl", bigimpl_ast_tr)],
+ parse_translation = [("_abs", abs_tr), ("_K", k_tr), ("_aprop", aprop_tr)],
print_translation = [],
- print_preproc = None,
- print_postproc = None,
- print_ast_translation = [("_%", lambda_ast_tr'), ("_idts", idts_ast_tr'),
+ print_ast_translation = [("_abs", abs_ast_tr'), ("_idts", idts_ast_tr'),
("==>", impl_ast_tr')]};
-val syntax_types = (* FIXME clean, check *)
- [logic, "aprop", args, "asms", id, "idt", "idts", tfree, tvar, "type", "types",
- var, "sort", "classes"]
+val syntax_types = [id, var, tfree, tvar, logic, "type", "types", "sort",
+ "classes", args, "idt", "idts", "aprop", "asms"];
val constrainIdtC = "_idtyp";
val constrainAbsC = "_constrainAbs";
--- a/src/Pure/Syntax/syntax.ML Fri Oct 01 13:26:22 1993 +0100
+++ b/src/Pure/Syntax/syntax.ML Mon Oct 04 15:30:49 1993 +0100
@@ -1,47 +1,53 @@
-(* Title: Pure/Syntax/syntax
+(* Title: Pure/Syntax/syntax.ML
ID: $Id$
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen
+
+Root of Isabelle's syntax module.
+
+TODO:
+ extend_tables (requires extend_gram) (roots!)
+ replace add_synrules by extend_tables
+ extend, merge: make roots handling more robust
+ extend: read_typ (incl check) as arg, remove def_sort
+ extend: use extend_tables
*)
signature SYNTAX =
sig
- (* FIXME include AST0 (?) *)
+ include AST0
include LEXICON0
include EXTENSION0
include TYPE_EXT0
include SEXTENSION1
include PRINTER0
- structure Extension: EXTENSION
- structure Pretty: PRETTY
- local open Extension.XGram Extension.XGram.Ast in
- type syntax
- val print_gram: syntax -> unit
- val print_trans: syntax -> unit
- val print_syntax: syntax -> unit
- val read_ast: syntax -> string * string -> ast
- val read: syntax -> typ -> string -> term
- val pretty_term: syntax -> term -> Pretty.T
- val pretty_typ: syntax -> typ -> Pretty.T
- val string_of_term: syntax -> term -> string
- val string_of_typ: syntax -> typ -> string
- val type_syn: syntax
- val extend: syntax * (indexname -> sort) -> string list * string list * sext
- -> syntax
- val merge: syntax * syntax -> syntax
- end
+ type syntax
+ val type_syn: syntax
+ val extend: syntax * (indexname -> sort) -> string list * string list * sext
+ -> syntax
+ val merge: syntax * syntax -> syntax
+ val print_gram: syntax -> unit
+ val print_trans: syntax -> unit
+ val print_syntax: syntax -> unit
+ val test_read: syntax -> string -> string -> unit
+ val read: syntax -> typ -> string -> term
+ val pretty_term: syntax -> term -> Pretty.T
+ val pretty_typ: syntax -> typ -> Pretty.T
+ val string_of_term: syntax -> term -> string
+ val string_of_typ: syntax -> typ -> string
end;
functor SyntaxFun(structure Symtab: SYMTAB and TypeExt: TYPE_EXT
and Parser: PARSER and SExtension: SEXTENSION and Printer: PRINTER
- sharing TypeExt.Extension.XGram = Parser.XGram = Printer.XGram
- and TypeExt.Extension = SExtension.Extension
- and Parser.ParseTree.Ast = Parser.XGram.Ast)(*: SYNTAX *) = (* FIXME *)
+ sharing TypeExt.Extension = SExtension.Extension
+ and Parser.XGram = TypeExt.Extension.XGram = Printer.XGram
+ and Parser.XGram.Ast = Parser.ParseTree.Ast)(*: SYNTAX *) = (* FIXME *)
struct
structure Extension = TypeExt.Extension;
structure XGram = Extension.XGram;
structure Lexicon = Parser.ParseTree.Lexicon;
-open Lexicon Extension TypeExt SExtension Printer XGram XGram.Ast;
+open Lexicon Parser Parser.ParseTree Extension TypeExt SExtension Printer
+ XGram XGram.Ast;
fun lookup tab a = Symtab.lookup (tab, a);
@@ -51,20 +57,17 @@
(** datatype syntax **)
datatype tables =
- Tab of {
- gram: Parser.Gram,
- lexicon: Lexicon,
- const_tab: unit Symtab.table,
+ Tabs of {
+ lexicon: lexicon,
+ roots: string list,
+ gram: gram,
+ consts: string list,
parse_ast_trtab: (ast list -> ast) Symtab.table,
- parse_preproc: ast -> ast,
parse_ruletab: (ast * ast) list Symtab.table,
- parse_postproc: ast -> ast,
parse_trtab: (term list -> term) Symtab.table,
print_trtab: (term list -> term) Symtab.table,
- print_preproc: ast -> ast,
print_ruletab: (ast * ast) list Symtab.table,
- print_postproc: ast -> ast,
- print_tab: Printer.tab};
+ prtab: prtab};
datatype gramgraph =
EmptyGG |
@@ -77,6 +80,75 @@
(*** compile syntax ***)
+(* translation funs *)
+
+fun extend_trtab tab trfuns name =
+ Symtab.balance (Symtab.st_of_alist (trfuns, tab)) handle Symtab.DUPLICATE s
+ => error ("More than one " ^ name ^ " for " ^ quote s);
+
+val mk_trtab = extend_trtab Symtab.null;
+
+
+(* translation rules *)
+
+fun mk_ruletab rules =
+ let
+ fun add_rule (r, tab) =
+ let val a = head_of_rule r;
+ in
+ (case lookup tab a of
+ None => Symtab.update ((a, [r]), tab)
+ | Some rs => Symtab.update ((a, r :: rs), tab))
+ end;
+ in
+ Symtab.balance (foldr add_rule (rules, Symtab.null))
+ end;
+
+fun extend_ruletab tab rules =
+ mk_ruletab (flat (map #2 (Symtab.alist_of tab)) @ rules);
+
+
+(* mk_tables *)
+
+fun mk_tables (XGram xgram) =
+ let
+ val {roots, prods, consts, parse_ast_translation, parse_rules,
+ parse_translation, print_translation, print_rules,
+ print_ast_translation} = xgram;
+ in
+ Tabs {
+ lexicon = mk_lexicon (literals_of prods),
+ roots = roots,
+ gram = mk_gram roots prods,
+ consts = consts,
+ parse_ast_trtab = mk_trtab parse_ast_translation "parse ast translation",
+ parse_ruletab = mk_ruletab parse_rules,
+ parse_trtab = mk_trtab parse_translation "parse translation",
+ print_trtab = mk_trtab print_translation "print translation",
+ print_ruletab = mk_ruletab print_rules,
+ prtab = mk_prtab prods print_ast_translation}
+ end;
+
+
+(* add_synrules *)
+
+fun add_synrules (Tabs tabs) (SynRules rules) =
+ let
+ val {lexicon, roots, gram, consts, parse_ast_trtab, parse_ruletab,
+ parse_trtab, print_trtab, print_ruletab, prtab} = tabs;
+ val {parse_rules, print_rules} = rules;
+ in
+ Tabs {
+ lexicon = lexicon, roots = roots, gram = gram, consts = consts,
+ parse_ast_trtab = parse_ast_trtab,
+ parse_ruletab = extend_ruletab parse_ruletab parse_rules,
+ parse_trtab = parse_trtab,
+ print_trtab = print_trtab,
+ print_ruletab = extend_ruletab print_ruletab print_rules,
+ prtab = prtab}
+ end;
+
+
(* ggr_to_xgram *)
fun ggr_to_xgram ggr =
@@ -86,130 +158,38 @@
and flatGG' (ref EmptyGG) xgv = xgv
| flatGG' (ref (ExtGG (ggr, ext))) xgv =
let
- val (xg', v') = flatGG ggr xgv
+ val (xg', v') = flatGG ggr xgv;
in
- (Extension.extend xg' ext, v')
+ (extend_xgram xg' ext, v')
end
| flatGG' (ref (MergeGG (ggr1, ggr2))) xgv =
flatGG ggr1 (flatGG ggr2 xgv);
in
- fst (flatGG ggr (Extension.empty, []))
- end;
-
-
-(* mk_ruletab *)
-
-fun mk_ruletab rules =
- let
- fun add_rule (r, tab) =
- let
- val a = head_of_rule r
- in
- case lookup tab a of
- None => Symtab.update ((a, [r]), tab)
- | Some rs => Symtab.update ((a, r :: rs), tab)
- end;
- in
- Symtab.balance (foldr add_rule (rules, Symtab.null))
+ #1 (flatGG ggr (empty_xgram, []))
end;
(* make_syntax *)
-fun make_syntax ggr =
- let
- fun mk_const_tab cs =
- Symtab.balance
- (Symtab.st_of_alist ((map (fn c => (c, ())) cs), Symtab.null));
-
- fun mk_trtab alst name =
- Symtab.balance (Symtab.st_of_alist (alst, Symtab.null))
- handle Symtab.DUPLICATE s => error ("More than one " ^ name ^ " for " ^ quote s);
-
- fun mk_proc (Some f) = f
- | mk_proc None = I;
-
- fun all_strings (opl: string prod list): string list =
- flat (map (fn Prod (_, syn, _, _) => terminals syn) opl);
-
- fun str_to_tok (opl: string prod list, lex: Lexicon): Token prod list =
- map
- (fn Prod (t, syn, s, pa) =>
- Prod (t, translate (hd o tokenize lex) syn, s, pa))
- opl;
-
- fun xgram_to_tables (XGram xgram) =
- let
- val {roots, prods, consts, parse_ast_translation, parse_preproc, parse_rules,
- parse_postproc, parse_translation, print_translation, print_preproc,
- print_rules, print_postproc, print_ast_translation} = xgram;
- val lexicon = mk_lexicon (all_strings prods);
- in
- Tab {
- gram = Parser.compile_xgram (roots, str_to_tok (prods, lexicon)),
- lexicon = lexicon,
- const_tab = mk_const_tab consts,
- parse_ast_trtab = mk_trtab parse_ast_translation "parse ast translation",
- parse_preproc = mk_proc parse_preproc,
- parse_ruletab = mk_ruletab parse_rules,
- parse_postproc = mk_proc parse_postproc,
- parse_trtab = mk_trtab parse_translation "parse translation",
- print_trtab = mk_trtab print_translation "print translation",
- print_preproc = mk_proc print_preproc,
- print_ruletab = mk_ruletab print_rules,
- print_postproc = mk_proc print_postproc,
- print_tab = mk_print_tab prods
- (mk_trtab print_ast_translation "print ast translation")}
- end;
- in
- Syntax (ggr, xgram_to_tables (ggr_to_xgram ggr))
- end;
-
-
-(* add_synrules *)
-
-fun add_synrules (Tab tabs) (SynRules rules) =
- let
- val {gram, lexicon, const_tab, parse_ast_trtab, parse_preproc, parse_ruletab,
- parse_postproc, parse_trtab, print_trtab, print_preproc, print_ruletab,
- print_postproc, print_tab} = tabs;
- val {parse_rules, print_rules} = rules;
- val parse_rs = flat (map snd (Symtab.alist_of parse_ruletab)) @ parse_rules;
- val print_rs = flat (map snd (Symtab.alist_of print_ruletab)) @ print_rules;
- in
- Tab {
- gram = gram, lexicon = lexicon, const_tab = const_tab,
- parse_ast_trtab = parse_ast_trtab,
- parse_preproc = parse_preproc,
- parse_ruletab = mk_ruletab parse_rs,
- parse_postproc = parse_postproc,
- parse_trtab = parse_trtab,
- print_trtab = print_trtab,
- print_preproc = print_preproc,
- print_ruletab = mk_ruletab print_rs,
- print_postproc = print_postproc,
- print_tab = print_tab}
- end;
+fun make_syntax ggr = Syntax (ggr, mk_tables (ggr_to_xgram ggr));
(*** inspect syntax ***)
-(* print_syntax_old *) (* FIXME remove *)
-
-fun print_syntax_old (Syntax (_, Tab {gram, lexicon, ...})) =
- Parser.print_gram (gram, lexicon);
-
-
-
fun xgram_of (Syntax (ggr, _)) = ggr_to_xgram ggr;
fun string_of_big_list name prts =
Pretty.string_of (Pretty.blk (2,
separate Pretty.fbrk (Pretty.str name :: prts)));
+fun string_of_strings name strs =
+ Pretty.string_of (Pretty.blk (2,
+ separate (Pretty.brk 1)
+ (map Pretty.str (name :: map quote (sort_strings strs)))));
-(* print_gram *) (* FIXME check *)
+
+(* print_gram *)
fun prt_gram (XGram {roots, prods, ...}) =
let
@@ -233,51 +213,36 @@
Pretty.blk (2, pretty_name name @ pretty_xsymbs xsymbs @
pretty_const const @ pretty_pri pri);
in
+ writeln (string_of_strings "lexicon:" (literals_of prods));
writeln (Pretty.string_of (Pretty.blk (2,
separate (Pretty.brk 1) (map Pretty.str ("roots:" :: roots)))));
writeln (string_of_big_list "prods:" (map pretty_prod prods))
end;
-
val print_gram = prt_gram o xgram_of;
-(* print_trans *) (* FIXME check *)
+(* print_trans *)
fun prt_trans (XGram xgram) =
let
- fun string_of_strings name strs =
- Pretty.string_of (Pretty.blk (2,
- separate (Pretty.brk 1) (map Pretty.str (name :: map quote strs))));
-
fun string_of_trs name trs = string_of_strings name (map fst trs);
- fun string_of_proc name proc =
- Pretty.string_of (Pretty.blk (2, [Pretty.str name, Pretty.brk 1,
- Pretty.str (if is_none proc then "None" else "Some fn")]));
-
fun string_of_rules name rules =
string_of_big_list name (map pretty_rule rules);
-
- val {consts, parse_ast_translation, parse_preproc, parse_rules,
- parse_postproc, parse_translation, print_translation, print_preproc,
- print_rules, print_postproc, print_ast_translation, ...} = xgram;
+ val {consts, parse_ast_translation, parse_rules, parse_translation,
+ print_translation, print_rules, print_ast_translation, ...} = xgram;
in
writeln (string_of_strings "consts:" consts);
writeln (string_of_trs "parse_ast_translation:" parse_ast_translation);
- writeln (string_of_proc "parse_preproc:" parse_preproc);
writeln (string_of_rules "parse_rules:" parse_rules);
- writeln (string_of_proc "parse_postproc:" parse_postproc);
writeln (string_of_trs "parse_translation:" parse_translation);
writeln (string_of_trs "print_translation:" print_translation);
- writeln (string_of_proc "print_preproc:" print_preproc);
writeln (string_of_rules "print_rules:" print_rules);
- writeln (string_of_proc "print_postproc:" print_postproc);
writeln (string_of_trs "print_ast_translation:" print_ast_translation)
end;
-
val print_trans = prt_trans o xgram_of;
@@ -294,63 +259,116 @@
(*** parsing and printing ***)
-(* read_ast *)
+(* mk_get_rules *)
-fun read_ast syn (root, s) =
- let
- val Syntax (_, Tab {gram, lexicon, parse_ast_trtab, ...}) = syn;
- val root = if Parser.parsable (gram, root) then root else error ("Unparsable root " ^ root) (* Extension.logic *); (* FIXME *)
- fun syn_err toks =
- error ("Syntax error at\n" ^ space_implode " " (map token_to_string toks));
- in
- Parser.ParseTree.pt_to_ast (lookup parse_ast_trtab)
- (Parser.parse (gram, root, tokenize lexicon s))
- handle Parser.SYNTAX_ERR toks => syn_err toks
- end;
-
-
-(* norm_ast *)
-
-fun norm_ast ruletab ast =
+fun mk_get_rules ruletab =
let
fun get_rules a =
(case lookup ruletab a of
Some rules => rules
| None => []);
in
- normalize (if Symtab.is_null ruletab then None else Some get_rules) ast
+ if Symtab.is_null ruletab then None else Some get_rules
+ end;
+
+
+(* read_ast *)
+
+fun read_ast (Syntax (_, tabs)) xids root str =
+ let
+ val Tabs {lexicon, gram, parse_ast_trtab, ...} = tabs;
+ in
+ pt_to_ast (lookup parse_ast_trtab)
+ (parse gram root (tokenize lexicon xids str))
end;
+(** test_read **)
+
+fun test_read (Syntax (_, tabs)) root str =
+ let
+ val Tabs {lexicon, gram, parse_ast_trtab, parse_ruletab, ...} = tabs;
+
+ val toks = tokenize lexicon false str;
+ val _ = writeln ("tokens: " ^ space_implode " " (map display_token toks));
+
+ val pt = parse gram root toks;
+ val raw_ast = pt_to_ast (K None) pt;
+ val _ = writeln ("raw: " ^ str_of_ast raw_ast);
+
+ val pre_ast = pt_to_ast (lookup parse_ast_trtab) pt;
+ val _ = normalize true true (mk_get_rules parse_ruletab) pre_ast;
+ in () end;
+
+
+
(** read **)
-fun read (syn as Syntax (_, Tab tabs)) ty s =
+fun read (syn as Syntax (_, tabs)) ty str =
let
- val {parse_preproc, parse_ruletab, parse_postproc, parse_trtab, ...} = tabs;
- val ast = read_ast syn (typ_to_nt ty, s);
+ val Tabs {parse_ruletab, parse_trtab, ...} = tabs;
+ val ast = read_ast syn false (typ_to_nonterm ty) str;
in
ast_to_term (lookup parse_trtab)
- (parse_postproc (norm_ast parse_ruletab (parse_preproc ast)))
+ (normalize_ast (mk_get_rules parse_ruletab) ast)
end;
-(** pprint_ast **)
+(** read_rule **)
+
+fun read_rule syn (xrule as ((_, lhs_src), (_, rhs_src))) =
+ let
+ val Syntax (_, Tabs {consts, ...}) = syn;
+
+ fun constantify (ast as Constant _) = ast
+ | constantify (ast as Variable x) =
+ if x mem consts then Constant x else ast
+ | constantify (Appl asts) = Appl (map constantify asts);
-val pprint_ast = Pretty.pprint o pretty_ast;
+ fun read_pat (root, str) =
+ constantify (read_ast syn true root str)
+ handle ERROR => error ("The error above occurred in " ^ quote str);
+
+ val rule as (lhs, rhs) = (pairself read_pat) xrule;
+ in
+ (case rule_error rule of
+ Some msg =>
+ error ("Error in syntax translation rule: " ^ msg ^
+ "\nexternal: " ^ quote lhs_src ^ " -> " ^ quote rhs_src ^
+ "\ninternal: " ^ str_of_ast lhs ^ " -> " ^ str_of_ast rhs)
+ | None => rule)
+ end;
-(** pretty term, typ **)
+(** read_xrules **)
+
+fun read_xrules syn xrules =
+ let
+ fun right_rule (xpat1 |-> xpat2) = Some (xpat1, xpat2)
+ | right_rule (xpat1 <-| xpat2) = None
+ | right_rule (xpat1 <-> xpat2) = Some (xpat1, xpat2);
-fun pretty_t t_to_ast pretty_t (syn as Syntax (_, Tab tabs)) t =
+ fun left_rule (xpat1 |-> xpat2) = None
+ | left_rule (xpat1 <-| xpat2) = Some (xpat2, xpat1)
+ | left_rule (xpat1 <-> xpat2) = Some (xpat2, xpat1);
+ in
+ (map (read_rule syn) (mapfilter right_rule xrules),
+ map (read_rule syn) (mapfilter left_rule xrules))
+ end;
+
+
+
+(** pretty terms or typs **)
+
+fun pretty_t t_to_ast pretty_t (syn as Syntax (_, tabs)) t =
let
- val {print_trtab, print_preproc, print_ruletab, print_postproc, print_tab, ...} = tabs;
+ val Tabs {print_trtab, print_ruletab, prtab, ...} = tabs;
val ast = t_to_ast (lookup print_trtab) t;
in
- pretty_t print_tab
- (print_postproc (norm_ast print_ruletab (print_preproc ast)))
+ pretty_t prtab (normalize_ast (mk_get_rules print_ruletab) ast)
end;
val pretty_term = pretty_t term_to_ast pretty_term_ast;
@@ -370,53 +388,23 @@
val type_syn = make_syntax (ref (ExtGG (ref EmptyGG, (type_ext, empty_synrules))));
-(* extend *) (* FIXME check *)
+(** extend **)
fun extend (old_syn as Syntax (ggr, _), def_sort) (roots, xconsts, sext) =
let
fun read_typ s = typ_of_term def_sort (read old_syn typeT s);
val ext = ext_of_sext roots xconsts read_typ sext;
- fun right_rule (xpat1 |-> xpat2) = Some (xpat1, xpat2)
- | right_rule (xpat1 <-| xpat2) = None
- | right_rule (xpat1 <-> xpat2) = Some (xpat1, xpat2);
-
- fun left_rule (xpat1 |-> xpat2) = None
- | left_rule (xpat1 <-| xpat2) = Some (xpat2, xpat1)
- | left_rule (xpat1 <-> xpat2) = Some (xpat2, xpat1);
-
val (tmp_syn as Syntax (_, tmp_tabs)) =
make_syntax (ref (ExtGG (ggr, (ext, empty_synrules))));
- val Syntax (_, Tab {const_tab, ...}) = tmp_syn;
- fun constantify (ast as (Constant _)) = ast
- | constantify (ast as (Variable x)) =
- if is_some (lookup const_tab x) then Constant x else ast
- | constantify (Appl asts) = Appl (map constantify asts);
-
- fun read_pat (r_s as (root, s)) =
- constantify ((read_ast tmp_syn r_s)
- handle ERROR => error ("The error above occurred in " ^ quote s));
-
- fun read_rule (xrule as ((_, lhs_src), (_, rhs_src))) =
- let
- val rule as (lhs, rhs) = (pairself read_pat) xrule;
- in
- case rule_error rule of
- Some msg =>
- error ("Error in syntax translation rule: " ^ msg ^
- "\nexternal: " ^ quote lhs_src ^ " -> " ^ quote rhs_src ^
- "\ninternal: " ^ str_of_ast lhs ^ " -> " ^ str_of_ast rhs)
- | None => rule
- end;
-
- val xrules = xrules_of sext;
- val new_rules =
+ val (parse_rules, print_rules) = read_xrules tmp_syn (xrules_of sext);
+ val rules =
SynRules {
- parse_rules = map read_rule (mapfilter right_rule xrules),
- print_rules = map read_rule (mapfilter left_rule xrules)};
+ parse_rules = parse_rules,
+ print_rules = print_rules};
in
- Syntax (ref (ExtGG (ggr, (ext, new_rules))), add_synrules tmp_tabs new_rules)
+ Syntax (ref (ExtGG (ggr, (ext, rules))), add_synrules tmp_tabs rules)
end;
--- a/src/Pure/Syntax/type_ext.ML Fri Oct 01 13:26:22 1993 +0100
+++ b/src/Pure/Syntax/type_ext.ML Mon Oct 04 15:30:49 1993 +0100
@@ -1,8 +1,12 @@
-(* Title: Pure/Syntax/type_ext
+(* Title: Pure/Syntax/type_ext.ML
ID: $Id$
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen
-The concrete syntax of types (used to bootstrap Pure)
+The concrete syntax of types (used to bootstrap Pure).
+
+TODO:
+ term_of_typ: prune sorts
+ move "_K" (?)
*)
signature TYPE_EXT0 =
@@ -25,39 +29,41 @@
struct
structure Extension = Extension;
-open Extension Extension.XGram.Ast;
+open Extension Extension.XGram Extension.XGram.Ast Lexicon;
-(** typ_of_term **) (* FIXME check *)
+(** typ_of_term **)
fun typ_of_term def_sort t =
let
fun sort_err (xi as (x, i)) =
- error ("typ_of_term: inconsistent sort constraints for type variable " ^
- (if i < 0 then x else Lexicon.string_of_vname xi));
-
- fun is_tfree name =
- (case explode name of
- "'" :: _ :: _ => true
- | _ :: _ => false
- | _ => error ("typ_of_term: bad var name " ^ quote name));
+ error ("Inconsistent sort constraints for type variable " ^
+ quote (if i < 0 then x else string_of_vname xi));
fun put_sort scs xi s =
(case assoc (scs, xi) of
None => (xi, s) :: scs
| Some s' => if s = s' then scs else sort_err xi);
- fun classes (Const (s, _)) = [s]
- | classes (Free (s, _)) = [s]
- | classes (Const ("_sortcons", _) $ Const (s, _) $ cls) = s :: classes cls
- | classes (Const ("_sortcons", _) $ Free (s, _) $ cls) = s :: classes cls
- | classes tm = raise (TERM ("typ_of_term: bad encoding of classes", [tm]));
+ fun insert x [] = [x: string]
+ | insert x (lst as y :: ys) =
+ if x > y then y :: insert x ys
+ else if x = y then lst
+ else x :: lst;
+
+ fun classes (Const (c, _)) = [c]
+ | classes (Free (c, _)) = [c]
+ | classes (Const ("_classes", _) $ Const (c, _) $ cls) =
+ insert c (classes cls)
+ | classes (Const ("_classes", _) $ Free (c, _) $ cls) =
+ insert c (classes cls)
+ | classes tm = raise_term "typ_of_term: bad encoding of classes" [tm];
fun sort (Const ("_emptysort", _)) = []
| sort (Const (s, _)) = [s]
| sort (Free (s, _)) = [s]
- | sort (Const ("_classes", _) $ cls) = classes cls
- | sort tm = raise (TERM ("typ_of_term: bad encoding of sort", [tm]));
+ | sort (Const ("_sort", _) $ cls) = classes cls
+ | sort tm = raise_term "typ_of_term: bad encoding of sort" [tm];
fun typ (Free (x, _), scs) =
(if is_tfree x then TFree (x, []) else Type (x, []), scs)
@@ -67,19 +73,19 @@
| typ (Const ("_ofsort", _) $ Var (xi, _) $ st, scs) =
(TVar (xi, []), put_sort scs xi (sort st))
| typ (Const (a, _), scs) = (Type (a, []), scs)
- | typ (tm as (_ $ _), scs) =
+ | typ (tm as _ $ _, scs) =
let
val (t, ts) = strip_comb tm;
val a =
- case t of
+ (case t of
Const (x, _) => x
| Free (x, _) => x
- | _ => raise (TERM ("typ_of_term: bad type application", [tm]));
+ | _ => raise_term "typ_of_term: bad type application" [tm]);
val (tys, scs') = typs (ts, scs);
in
(Type (a, tys), scs')
end
- | typ (tm, _) = raise (TERM ("typ_of_term: bad encoding of typ", [tm]))
+ | typ (tm, _) = raise_term "typ_of_term: bad encoding of typ" [tm]
and typs (t :: ts, scs) =
let
val (ty, scs') = typ (t, scs);
@@ -109,40 +115,43 @@
fun term_of_typ show_sorts ty =
let
fun const x = Const (x, dummyT);
+ fun free x = Free (x, dummyT);
+ fun var xi = Var (xi, dummyT);
fun classes [] = raise Match
- | classes [s] = const s
- | classes (s :: ss) = const "_sortcons" $ const s $ classes ss;
+ | classes [c] = free c
+ | classes (c :: cs) = const "_classes" $ free c $ classes cs;
fun sort [] = const "_emptysort"
- | sort [s] = const s
- | sort ss = const "_classes" $ classes ss;
+ | sort [s] = free s
+ | sort ss = const "_sort" $ classes ss;
fun of_sort t ss =
if show_sorts then const "_ofsort" $ t $ sort ss else t;
- fun typ (Type (a, tys)) = list_comb (const a, map typ tys)
- | typ (TFree (x, ss)) = of_sort (Free (x, dummyT)) ss
- | typ (TVar (xi, ss)) = of_sort (Var (xi, dummyT)) ss;
+ fun term_of (Type (a, tys)) = list_comb (const a, map term_of tys)
+ | term_of (TFree (x, ss)) = of_sort (free x) ss
+ | term_of (TVar (xi, ss)) = of_sort (var xi) ss;
in
- typ ty
+ term_of ty
end;
(** the type syntax **)
-(* parse translations *)
+(* parse ast translations *)
-fun tappl_ast_tr (*"_tappl"*) [types, f] = Appl (f :: unfold_ast "_types" types)
- | tappl_ast_tr (*"_tappl"*) asts = raise_ast "tappl_ast_tr" asts;
+fun tappl_ast_tr (*"_tapp(l)"*) [types, f] =
+ Appl (f :: unfold_ast "_types" types)
+ | tappl_ast_tr (*"_tapp(l)"*) asts = raise_ast "tappl_ast_tr" asts;
fun bracket_ast_tr (*"_bracket"*) [dom, cod] =
fold_ast_p "fun" (unfold_ast "_types" dom, cod)
| bracket_ast_tr (*"_bracket"*) asts = raise_ast "bracket_ast_tr" asts;
-(* print translations *)
+(* print ast translations *)
fun tappl_ast_tr' (f, []) = raise_ast "tappl_ast_tr'" [f]
| tappl_ast_tr' (f, [ty]) = Appl [Constant "_tapp", ty, f]
@@ -150,7 +159,7 @@
fun fun_ast_tr' (*"fun"*) asts =
(case unfold_ast_p "fun" (Appl (Constant "fun" :: asts)) of
- (dom as (_ :: _ :: _), cod)
+ (dom as _ :: _ :: _, cod)
=> Appl [Constant "_bracket", fold_ast "_types" dom, cod]
| _ => raise Match);
@@ -165,31 +174,27 @@
Ext {
roots = [logic, "type"],
mfix = [
- Mfix ("_", idT --> sortT, "", [], max_pri),
- Mfix ("{}", sortT, "_emptysort", [], max_pri),
- Mfix ("{_}", classesT --> sortT, "_classes", [], max_pri),
- Mfix ("_", idT --> classesT, "", [], max_pri),
- Mfix ("_,_", [idT, classesT] ---> classesT, "_sortcons", [], max_pri),
Mfix ("_", tfreeT --> typeT, "", [], max_pri),
Mfix ("_", tvarT --> typeT, "", [], max_pri),
Mfix ("_", idT --> typeT, "", [], max_pri),
Mfix ("_::_", [tfreeT, sortT] ---> typeT, "_ofsort", [max_pri, 0], max_pri),
Mfix ("_::_", [tvarT, sortT] ---> typeT, "_ofsort", [max_pri, 0], max_pri),
- Mfix ("_ _", [typeT, idT] ---> typeT, "_tapp", [max_pri, 0], max_pri),
- Mfix ("((1'(_'))_)", [typesT, idT] ---> typeT, "_tappl", [], max_pri),
+ Mfix ("_", idT --> sortT, "", [], max_pri),
+ Mfix ("{}", sortT, "_emptysort", [], max_pri),
+ Mfix ("{_}", classesT --> sortT, "_sort", [], max_pri),
+ Mfix ("_", idT --> classesT, "", [], max_pri),
+ Mfix ("_,_", [idT, classesT] ---> classesT, "_classes", [], max_pri),
+ Mfix ("_ _", [typeT, idT] ---> typeT, "_tapp", [max_pri, 0], max_pri), (* FIXME ambiguous *)
+ Mfix ("((1'(_'))_)", [typesT, idT] ---> typeT, "_tappl", [], max_pri), (* FIXME ambiguous *)
Mfix ("_", typeT --> typesT, "", [], max_pri),
Mfix ("_,/ _", [typeT, typesT] ---> typesT, "_types", [], max_pri),
Mfix ("(_/ => _)", [typeT, typeT] ---> typeT, "fun", [1, 0], 0),
Mfix ("([_]/ => _)", [typesT, typeT] ---> typeT, "_bracket", [0, 0], 0)],
- extra_consts = ["fun"],
+ extra_consts = ["_K"],
parse_ast_translation = [("_tapp", tappl_ast_tr), ("_tappl", tappl_ast_tr),
("_bracket", bracket_ast_tr)],
- parse_preproc = None,
- parse_postproc = None,
parse_translation = [],
print_translation = [],
- print_preproc = None,
- print_postproc = None,
print_ast_translation = [("fun", fun_ast_tr')]};
--- a/src/Pure/Syntax/xgram.ML Fri Oct 01 13:26:22 1993 +0100
+++ b/src/Pure/Syntax/xgram.ML Mon Oct 04 15:30:49 1993 +0100
@@ -1,61 +1,54 @@
-(* Title: Pure/Syntax/xgram
+(* Title: Pure/Syntax/xgram.ML
ID: $Id$
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen
-External Grammar Representation
+External grammar representation (internal interface).
-Changes:
- XGRAM: added Ast, changed XGram,
- renamed (XSymb, Prod, XGram) to (xsymb, prod, xgram)
- removed Symtab
TODO:
- prod, xsymb, xgram: 'a -> string (?)
+ prod, xsymb: 'a --> string
+ Terminal --> Literal, Nonterminal --> Argument (?)
*)
signature XGRAM =
sig
structure Ast: AST
- datatype 'a xsymb =
- Terminal of 'a |
- Nonterminal of string * int |
- Space of string |
- Bg of int | Brk of int | En
- datatype 'a prod = Prod of string * ('a xsymb list) * string * int
local open Ast in
- datatype 'a xgram =
+ datatype 'a xsymb =
+ Terminal of 'a |
+ Nonterminal of string * int |
+ Space of string |
+ Bg of int | Brk of int | En
+ datatype 'a prod = Prod of string * ('a xsymb list) * string * int
+ val max_pri: int
+ val chain_pri: int
+ val literals_of: string prod list -> string list
+ datatype xgram =
XGram of {
roots: string list,
- prods: 'a prod list,
+ prods: string prod list,
consts: string list,
parse_ast_translation: (string * (ast list -> ast)) list,
- parse_preproc: (ast -> ast) option,
parse_rules: (ast * ast) list,
- parse_postproc: (ast -> ast) option,
parse_translation: (string * (term list -> term)) list,
print_translation: (string * (term list -> term)) list,
- print_preproc: (ast -> ast) option,
print_rules: (ast * ast) list,
- print_postproc: (ast -> ast) option,
print_ast_translation: (string * (ast list -> ast)) list}
end
- val copy_pri: int
- val terminals: 'a xsymb list -> 'a list
- val nonterminals: 'a xsymb list -> string list
- val translate: ('a -> 'b) -> 'a xsymb list -> 'b xsymb list
end;
-functor XGramFun(Ast: AST)(*: XGRAM*) = (* FIXME *)
+functor XGramFun(Ast: AST): XGRAM =
struct
structure Ast = Ast;
open Ast;
-(** datatype 'a xgram **)
+
+(** datatype prod **)
-(* Terminal a: terminal a
- Nonterminal (s, p): nonterminal named s, require priority >= p
- Space s: some white space for printing
- Bg, Brk, En: see resp. routines in Pretty *)
+(*Terminal s: literal token s
+ Nonterminal (s, p): nonterminal s requiring priority >= p, or valued token
+ Space s: some white space for printing
+ Bg, Brk, En: blocks and breaks for pretty printing*)
datatype 'a xsymb =
Terminal of 'a |
@@ -64,53 +57,43 @@
Bg of int | Brk of int | En;
-(* Prod (lhs, rhs, opn, p):
+(*Prod (lhs, syms, c, p):
lhs: name of nonterminal on the lhs of the production
- rhs: list of symbols on the rhs of the production
- opn: name of the corresponding Isabelle Const
- p: priority of this production, 0 <= p <= max_pri *)
+ syms: list of symbols on the rhs of the production
+ c: head of parse tree
+ p: priority of this production*)
datatype 'a prod = Prod of string * ('a xsymb list) * string * int;
+val max_pri = 1000; (*maximum legal priority*)
+val chain_pri = ~1; (*dummy for chain productions*)
-datatype 'a xgram =
- XGram of {
- roots: string list,
- prods: 'a prod list,
- consts: string list,
- parse_ast_translation: (string * (ast list -> ast)) list,
- parse_preproc: (ast -> ast) option,
- parse_rules: (ast * ast) list,
- parse_postproc: (ast -> ast) option,
- parse_translation: (string * (term list -> term)) list,
- print_translation: (string * (term list -> term)) list,
- print_preproc: (ast -> ast) option,
- print_rules: (ast * ast) list,
- print_postproc: (ast -> ast) option,
- print_ast_translation: (string * (ast list -> ast)) list};
+
+(* literals_of *)
+
+fun literals_of prods =
+ let
+ fun lits_of (Prod (_, syn, _, _)) =
+ mapfilter (fn Terminal s => Some s | _ => None) syn;
+ in
+ distinct (flat (map lits_of prods))
+ end;
-(** misc stuff **)
-
-val copy_pri = ~1; (* must be < all legal priorities, i.e. 0 *)
-
-fun terminals [] = []
- | terminals (Terminal s :: sl) = s :: terminals sl
- | terminals (_ :: sl) = terminals sl;
+(** datatype xgram **)
-fun nonterminals [] = []
- | nonterminals (Nonterminal (s, _) :: sl) = s :: nonterminals sl
- | nonterminals (_ :: sl) = nonterminals sl;
-
-fun translate trfn =
- map
- (fn Terminal t => Terminal (trfn t)
- | Nonterminal s => Nonterminal s
- | Space s => Space s
- | Bg i => Bg i
- | Brk i => Brk i
- | En => En);
+datatype xgram =
+ XGram of {
+ roots: string list,
+ prods: string prod list,
+ consts: string list,
+ parse_ast_translation: (string * (ast list -> ast)) list,
+ parse_rules: (ast * ast) list,
+ parse_translation: (string * (term list -> term)) list,
+ print_translation: (string * (term list -> term)) list,
+ print_rules: (ast * ast) list,
+ print_ast_translation: (string * (ast list -> ast)) list};
end;