src/Pure/Syntax/extension.ML
author paulson
Thu Sep 25 12:09:41 1997 +0200 (1997-09-25)
changeset 3706 e57b5902822f
parent 171 ab0f93a291b5
permissions -rw-r--r--
Generalized and exported biresolution_from_nets_tac to allow the declaration
of Clarify_tac
     1 (*  Title:      Pure/Syntax/extension.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
     4 
     5 External grammar definition (internal interface).
     6 *)
     7 
     8 signature EXTENSION0 =
     9 sig
    10   val typeT: typ
    11   val constrainC: string
    12 end;
    13 
    14 signature EXTENSION =
    15 sig
    16   include EXTENSION0
    17   structure XGram: XGRAM
    18   local open XGram XGram.Ast in
    19     datatype mfix = Mfix of string * typ * string * int list * int
    20     datatype ext =
    21       Ext of {
    22         roots: string list,
    23         mfix: mfix list,
    24         extra_consts: string list,
    25         parse_ast_translation: (string * (ast list -> ast)) list,
    26         parse_translation: (string * (term list -> term)) list,
    27         print_translation: (string * (term list -> term)) list,
    28         print_ast_translation: (string * (ast list -> ast)) list} |
    29       ExtRules of {
    30         parse_rules: (ast * ast) list,
    31         print_rules: (ast * ast) list} |
    32       ExtRoots of string list
    33     val logic: string
    34     val args: string
    35     val idT: typ
    36     val varT: typ
    37     val tfreeT: typ
    38     val tvarT: typ
    39     val typ_to_nonterm: typ -> string
    40     val applC: string
    41     val empty_xgram: xgram
    42     val extend_xgram: xgram -> ext -> xgram
    43     val mk_xgram: ext -> xgram
    44   end
    45 end;
    46 
    47 functor ExtensionFun(structure XGram: XGRAM and Lexicon: LEXICON): EXTENSION =
    48 struct
    49 
    50 structure XGram = XGram;
    51 open XGram XGram.Ast Lexicon;
    52 
    53 
    54 (** datatype ext **)
    55 
    56 (*Mfix (sy, ty, c, ps, p):
    57     sy: rhs of production as symbolic string
    58     ty: type description of production
    59     c: head of parse tree
    60     ps: priorities of arguments in sy
    61     p: priority of production*)
    62 
    63 datatype mfix = Mfix of string * typ * string * int list * int;
    64 
    65 datatype ext =
    66   Ext of {
    67     roots: string list,
    68     mfix: mfix list,
    69     extra_consts: string list,
    70     parse_ast_translation: (string * (ast list -> ast)) list,
    71     parse_translation: (string * (term list -> term)) list,
    72     print_translation: (string * (term list -> term)) list,
    73     print_ast_translation: (string * (ast list -> ast)) list} |
    74   ExtRules of {
    75     parse_rules: (ast * ast) list,
    76     print_rules: (ast * ast) list} |
    77   ExtRoots of string list;
    78 
    79 
    80 (* ext_components *)
    81 
    82 fun ext_components (Ext ext) = {
    83       roots = #roots ext,
    84       mfix = #mfix ext,
    85       extra_consts = #extra_consts ext,
    86       parse_ast_translation = #parse_ast_translation ext,
    87       parse_rules = [],
    88       parse_translation = #parse_translation ext,
    89       print_translation = #print_translation ext,
    90       print_rules = [],
    91       print_ast_translation = #print_ast_translation ext}
    92   | ext_components (ExtRules {parse_rules, print_rules}) = {
    93       roots = [],
    94       mfix = [],
    95       extra_consts = [],
    96       parse_ast_translation = [],
    97       parse_rules = parse_rules,
    98       parse_translation = [],
    99       print_translation = [],
   100       print_rules = print_rules,
   101       print_ast_translation = []}
   102   | ext_components (ExtRoots roots) = {
   103       roots = roots,
   104       mfix = [],
   105       extra_consts = [],
   106       parse_ast_translation = [],
   107       parse_rules = [],
   108       parse_translation = [],
   109       print_translation = [],
   110       print_rules = [],
   111       print_ast_translation = []};
   112 
   113 
   114 (* empty_xgram *)
   115 
   116 val empty_xgram =
   117   XGram {
   118     roots = [], prods = [], consts = [],
   119     parse_ast_translation = [],
   120     parse_rules = [],
   121     parse_translation = [],
   122     print_translation = [],
   123     print_rules = [],
   124     print_ast_translation = []};
   125 
   126 
   127 (* syntactic categories *)
   128 
   129 val logic = "logic";
   130 val logicT = Type (logic, []);
   131 
   132 val logic1 = "logic1";
   133 val logic1T = Type (logic1, []);
   134 
   135 val args = "args";
   136 val argsT = Type (args, []);
   137 
   138 val funT = Type ("fun", []);
   139 
   140 val typeT = Type ("type", []);
   141 
   142 
   143 (* terminals *)
   144 
   145 val idT = Type (id, []);
   146 val varT = Type (var, []);
   147 val tfreeT = Type (tfree, []);
   148 val tvarT = Type (tvar, []);
   149 
   150 
   151 (* constants *)
   152 
   153 val applC = "_appl";
   154 val constrainC = "_constrain";
   155 
   156 
   157 (* typ_to_nonterm *)
   158 
   159 fun typ_to_nonterm (Type (c, _)) = c
   160   | typ_to_nonterm _ = logic;
   161 
   162 fun typ_to_nonterm1 (Type (c, _)) = c
   163   | typ_to_nonterm1 _ = logic1;
   164 
   165 
   166 
   167 (** mfix_to_prod **)
   168 
   169 fun mfix_to_prod (Mfix (sy, typ, const, pris, pri)) =
   170   let
   171     fun err msg =
   172       (writeln ("Error in mixfix annotation " ^ quote sy ^ " for " ^ quote const);
   173         error msg);
   174 
   175     fun check_pri p =
   176       if p >= 0 andalso p <= max_pri then ()
   177       else err ("precedence out of range: " ^ string_of_int p);
   178 
   179     fun blocks_ok [] 0 = true
   180       | blocks_ok [] _ = false
   181       | blocks_ok (Bg _ :: syms) n = blocks_ok syms (n + 1)
   182       | blocks_ok (En :: _) 0 = false
   183       | blocks_ok (En :: syms) n = blocks_ok syms (n - 1)
   184       | blocks_ok (_ :: syms) n = blocks_ok syms n;
   185 
   186     fun check_blocks syms =
   187       if blocks_ok syms 0 then ()
   188       else err "unbalanced block parentheses";
   189 
   190 
   191     fun is_meta c = c mem ["(", ")", "/", "_"];
   192 
   193     fun scan_delim_char ("'" :: c :: cs) =
   194           if is_blank c then err "illegal spaces in delimiter" else (c, cs)
   195       | scan_delim_char ["'"] = err "trailing escape character"
   196       | scan_delim_char (chs as c :: cs) =
   197           if is_blank c orelse is_meta c then raise LEXICAL_ERROR else (c, cs)
   198       | scan_delim_char [] = raise LEXICAL_ERROR;
   199 
   200     val scan_symb =
   201       $$ "_" >> K (Nonterminal ("", 0)) ||
   202       $$ "(" -- scan_int >> (Bg o #2) ||
   203       $$ ")" >> K En ||
   204       $$ "/" -- $$ "/" >> K (Brk ~1) ||
   205       $$ "/" -- scan_any is_blank >> (Brk o length o #2) ||
   206       scan_any1 is_blank >> (Space o implode) ||
   207       repeat1 scan_delim_char >> (Terminal o implode);
   208 
   209 
   210     val cons_fst = apfst o cons;
   211 
   212     fun add_args [] ty [] = ([], typ_to_nonterm1 ty)
   213       | add_args [] _ _ = err "too many precedences"
   214       | add_args (Nonterminal _ :: syms) (Type ("fun", [ty, tys])) [] =
   215           cons_fst (Nonterminal (typ_to_nonterm ty, 0)) (add_args syms tys [])
   216       | add_args (Nonterminal _ :: syms) (Type ("fun", [ty, tys])) (p :: ps) =
   217           cons_fst (Nonterminal (typ_to_nonterm ty, p)) (add_args syms tys ps)
   218       | add_args (Nonterminal _ :: _) _ _ =
   219           err "more arguments than in corresponding type"
   220       | add_args (sym :: syms) ty ps = cons_fst sym (add_args syms ty ps);
   221 
   222 
   223     fun is_arg (Nonterminal _) = true
   224       | is_arg _ = false;
   225 
   226     fun is_term (Terminal _) = true
   227       | is_term (Nonterminal (s, _)) = is_terminal s
   228       | is_term _ = false;
   229 
   230     fun rem_pri (Nonterminal (s, _)) = Nonterminal (s, chain_pri)
   231       | rem_pri sym = sym;
   232 
   233 
   234     val (raw_symbs, _) = repeat scan_symb (explode sy);
   235     val (symbs, lhs) = add_args raw_symbs typ pris;
   236     val prod = Prod (lhs, symbs, const, pri);
   237   in
   238     seq check_pri pris;
   239     check_pri pri;
   240     check_blocks symbs;
   241 
   242     if is_terminal lhs then err ("illegal lhs: " ^ lhs)
   243     else if const <> "" then prod
   244     else if length (filter is_arg symbs) <> 1 then
   245       err "copy production must have exactly one argument"
   246     else if exists is_term symbs then prod
   247     else Prod (lhs, map rem_pri symbs, "", chain_pri)
   248   end;
   249 
   250 
   251 
   252 (** extend_xgram **)
   253 
   254 fun extend_xgram (XGram xgram) ext =
   255   let
   256     fun descend (from, to) = Mfix ("_", to --> from, "", [0], 0);
   257 
   258     fun parents T = Mfix ("'(_')", T --> T, "", [0], max_pri);
   259 
   260     fun mkappl T =
   261       Mfix ("(1_/(1'(_')))", [funT, argsT] ---> T, applC, [max_pri, 0], max_pri);
   262 
   263     fun mkid T = Mfix ("_", idT --> T, "", [], max_pri);
   264 
   265     fun mkvar T = Mfix ("_", varT --> T, "", [], max_pri);
   266 
   267     fun constrain T =
   268       Mfix ("_::_", [T, typeT] ---> T, constrainC, [max_pri, 0], max_pri - 1);
   269 
   270 
   271     val {roots = roots1, prods, consts,
   272       parse_ast_translation = parse_ast_translation1,
   273       parse_rules = parse_rules1,
   274       parse_translation = parse_translation1,
   275       print_translation = print_translation1,
   276       print_rules = print_rules1,
   277       print_ast_translation = print_ast_translation1} = xgram;
   278 
   279     val {roots = roots2, mfix, extra_consts,
   280       parse_ast_translation = parse_ast_translation2,
   281       parse_rules = parse_rules2,
   282       parse_translation = parse_translation2,
   283       print_translation = print_translation2,
   284       print_rules = print_rules2,
   285       print_ast_translation = print_ast_translation2} = ext_components ext;
   286 
   287     val Troots = map (apr (Type, [])) (roots2 \\ roots1);
   288     val Troots' = Troots \\ [typeT, propT, logicT];
   289     val mfix' = mfix @ map parents (Troots \ logicT) @ map mkappl Troots' @
   290       map mkid Troots' @ map mkvar Troots' @ map constrain Troots' @
   291       map (apl (logicT, descend)) (Troots \\ [typeT, logicT]) @
   292       map (apr (descend, logic1T)) Troots';
   293     val mfix_consts =
   294       distinct (filter is_xid (map (fn (Mfix (_, _, c, _, _)) => c) mfix'));
   295   in
   296     XGram {
   297       roots = distinct (roots1 @ roots2),
   298       prods = prods @ map mfix_to_prod mfix',
   299       consts = extra_consts union (mfix_consts union consts),
   300       parse_ast_translation = parse_ast_translation1 @ parse_ast_translation2,
   301       parse_rules = parse_rules1 @ parse_rules2,
   302       parse_translation = parse_translation1 @ parse_translation2,
   303       print_translation = print_translation1 @ print_translation2,
   304       print_rules = print_rules1 @ print_rules2,
   305       print_ast_translation = print_ast_translation1 @ print_ast_translation2}
   306   end;
   307 
   308 
   309 (* mk_xgram *)
   310 
   311 val mk_xgram = extend_xgram empty_xgram;
   312 
   313 
   314 end;
   315