--- a/src/Pure/Syntax/extension.ML Sat Apr 05 16:18:58 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,315 +0,0 @@
-(* Title: Pure/Syntax/extension.ML
- ID: $Id$
- Author: Tobias Nipkow and Markus Wenzel, TU Muenchen
-
-External grammar definition (internal interface).
-*)
-
-signature EXTENSION0 =
-sig
- val typeT: typ
- val constrainC: string
-end;
-
-signature EXTENSION =
-sig
- include EXTENSION0
- structure XGram: XGRAM
- local open XGram XGram.Ast in
- datatype mfix = Mfix of string * typ * string * int list * int
- datatype ext =
- Ext of {
- roots: string list,
- mfix: mfix list,
- extra_consts: string list,
- parse_ast_translation: (string * (ast list -> ast)) list,
- parse_translation: (string * (term list -> term)) list,
- print_translation: (string * (term list -> term)) list,
- print_ast_translation: (string * (ast list -> ast)) list} |
- ExtRules of {
- parse_rules: (ast * ast) list,
- print_rules: (ast * ast) list} |
- ExtRoots of string list
- val logic: string
- val args: string
- val idT: typ
- val varT: typ
- val tfreeT: typ
- val tvarT: typ
- val typ_to_nonterm: typ -> string
- val applC: string
- val empty_xgram: xgram
- val extend_xgram: xgram -> ext -> xgram
- val mk_xgram: ext -> xgram
- end
-end;
-
-functor ExtensionFun(structure XGram: XGRAM and Lexicon: LEXICON): EXTENSION =
-struct
-
-structure XGram = XGram;
-open XGram XGram.Ast Lexicon;
-
-
-(** datatype ext **)
-
-(*Mfix (sy, ty, c, ps, p):
- sy: rhs of production as symbolic string
- ty: type description 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;
-
-datatype ext =
- Ext of {
- roots: string list,
- mfix: mfix list,
- extra_consts: string list,
- parse_ast_translation: (string * (ast list -> ast)) list,
- parse_translation: (string * (term list -> term)) list,
- print_translation: (string * (term list -> term)) list,
- print_ast_translation: (string * (ast list -> ast)) list} |
- ExtRules of {
- parse_rules: (ast * ast) list,
- print_rules: (ast * ast) list} |
- ExtRoots of string list;
-
-
-(* ext_components *)
-
-fun ext_components (Ext ext) = {
- roots = #roots ext,
- mfix = #mfix ext,
- extra_consts = #extra_consts ext,
- parse_ast_translation = #parse_ast_translation ext,
- parse_rules = [],
- parse_translation = #parse_translation ext,
- print_translation = #print_translation ext,
- print_rules = [],
- print_ast_translation = #print_ast_translation ext}
- | ext_components (ExtRules {parse_rules, print_rules}) = {
- roots = [],
- mfix = [],
- extra_consts = [],
- parse_ast_translation = [],
- parse_rules = parse_rules,
- parse_translation = [],
- print_translation = [],
- print_rules = print_rules,
- print_ast_translation = []}
- | ext_components (ExtRoots roots) = {
- roots = roots,
- mfix = [],
- extra_consts = [],
- parse_ast_translation = [],
- parse_rules = [],
- parse_translation = [],
- print_translation = [],
- print_rules = [],
- print_ast_translation = []};
-
-
-(* empty_xgram *)
-
-val empty_xgram =
- XGram {
- roots = [], prods = [], consts = [],
- parse_ast_translation = [],
- parse_rules = [],
- parse_translation = [],
- print_translation = [],
- print_rules = [],
- print_ast_translation = []};
-
-
-(* syntactic categories *)
-
-val logic = "logic";
-val logicT = Type (logic, []);
-
-val logic1 = "logic1";
-val logic1T = Type (logic1, []);
-
-val args = "args";
-val argsT = Type (args, []);
-
-val funT = Type ("fun", []);
-
-val typeT = Type ("type", []);
-
-
-(* terminals *)
-
-val idT = Type (id, []);
-val varT = Type (var, []);
-val tfreeT = Type (tfree, []);
-val tvarT = Type (tvar, []);
-
-
-(* constants *)
-
-val applC = "_appl";
-val constrainC = "_constrain";
-
-
-(* 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;
-
-
-
-(** mfix_to_prod **)
-
-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 check_pri p =
- if p >= 0 andalso p <= max_pri then ()
- else err ("precedence out of range: " ^ string_of_int p);
-
- 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 check_blocks syms =
- if blocks_ok syms 0 then ()
- else err "unbalanced block parentheses";
-
-
- 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 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;
-
-
-
-(** extend_xgram **)
-
-fun extend_xgram (XGram xgram) ext =
- let
- fun descend (from, to) = Mfix ("_", to --> from, "", [0], 0);
-
- fun parents T = Mfix ("'(_')", T --> T, "", [0], max_pri);
-
- fun mkappl T =
- Mfix ("(1_/(1'(_')))", [funT, argsT] ---> T, applC, [max_pri, 0], max_pri);
-
- fun mkid T = Mfix ("_", idT --> T, "", [], max_pri);
-
- fun mkvar T = Mfix ("_", varT --> T, "", [], max_pri);
-
- fun constrain T =
- Mfix ("_::_", [T, typeT] ---> T, constrainC, [max_pri, 0], max_pri - 1);
-
-
- val {roots = roots1, prods, consts,
- parse_ast_translation = parse_ast_translation1,
- parse_rules = parse_rules1,
- parse_translation = parse_translation1,
- print_translation = print_translation1,
- print_rules = print_rules1,
- print_ast_translation = print_ast_translation1} = xgram;
-
- val {roots = roots2, mfix, extra_consts,
- parse_ast_translation = parse_ast_translation2,
- parse_rules = parse_rules2,
- parse_translation = parse_translation2,
- print_translation = print_translation2,
- print_rules = print_rules2,
- print_ast_translation = print_ast_translation2} = ext_components ext;
-
- val Troots = map (apr (Type, [])) (roots2 \\ roots1);
- val Troots' = Troots \\ [typeT, propT, logicT];
- val mfix' = mfix @ map parents (Troots \ logicT) @ map mkappl Troots' @
- 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),
- 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_rules = parse_rules1 @ parse_rules2,
- parse_translation = parse_translation1 @ parse_translation2,
- print_translation = print_translation1 @ print_translation2,
- print_rules = print_rules1 @ print_rules2,
- print_ast_translation = print_ast_translation1 @ print_ast_translation2}
- end;
-
-
-(* mk_xgram *)
-
-val mk_xgram = extend_xgram empty_xgram;
-
-
-end;
-