# HG changeset patch # User wenzelm # Date 749745049 -3600 # Node ID c9ec452ff08f5afc6215db388288bceb4be2d5f8 # Parent b35851cafd3e323b6dfd6861a15db6320f21cb46 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; diff -r b35851cafd3e -r c9ec452ff08f src/Pure/Syntax/README --- 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. diff -r b35851cafd3e -r c9ec452ff08f src/Pure/Syntax/ROOT.ML --- 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; diff -r b35851cafd3e -r c9ec452ff08f src/Pure/Syntax/ast.ML --- 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; diff -r b35851cafd3e -r c9ec452ff08f src/Pure/Syntax/earley0A.ML --- 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 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; + diff -r b35851cafd3e -r c9ec452ff08f src/Pure/Syntax/extension.ML --- 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; diff -r b35851cafd3e -r c9ec452ff08f src/Pure/Syntax/lexicon.ML --- 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 cd 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 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; diff -r b35851cafd3e -r c9ec452ff08f src/Pure/Syntax/parse_tree.ML --- 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; diff -r b35851cafd3e -r c9ec452ff08f src/Pure/Syntax/parser.ML --- /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; + diff -r b35851cafd3e -r c9ec452ff08f src/Pure/Syntax/pretty.ML --- 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 diff -r b35851cafd3e -r c9ec452ff08f src/Pure/Syntax/printer.ML --- 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; diff -r b35851cafd3e -r c9ec452ff08f src/Pure/Syntax/sextension.ML --- 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"; diff -r b35851cafd3e -r c9ec452ff08f src/Pure/Syntax/syntax.ML --- 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; diff -r b35851cafd3e -r c9ec452ff08f src/Pure/Syntax/type_ext.ML --- 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')]}; diff -r b35851cafd3e -r c9ec452ff08f src/Pure/Syntax/xgram.ML --- 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;