changed datatype ext;
authorwenzelm
Mon Nov 29 12:29:41 1993 +0100 (1993-11-29)
changeset 16679e61c182b22
parent 165 793be9f1e88e
child 167 128e122acc89
changed datatype ext;
src/Pure/Syntax/extension.ML
     1.1 --- a/src/Pure/Syntax/extension.ML	Mon Nov 29 12:28:09 1993 +0100
     1.2 +++ b/src/Pure/Syntax/extension.ML	Mon Nov 29 12:29:41 1993 +0100
     1.3 @@ -5,9 +5,8 @@
     1.4  External grammar definition (internal interface).
     1.5  
     1.6  TODO:
     1.7 -  Ext of {roots, mfix, extra_consts} * {.._translation} * {.._rules}
     1.8 -  remove synrules
     1.9 -  extend_xgram: move '.. \\ roots1' to Syntax.extend_tables
    1.10 +  ext = {roots, mfix, extra_consts} | {.._translation} | {.._rules} (?)
    1.11 +  extend_xgram: move '.. \\ roots1' to Syntax.extend_tables (no?)
    1.12  *)
    1.13  
    1.14  signature EXTENSION0 =
    1.15 @@ -30,11 +29,11 @@
    1.16          parse_ast_translation: (string * (ast list -> ast)) list,
    1.17          parse_translation: (string * (term list -> term)) list,
    1.18          print_translation: (string * (term list -> term)) list,
    1.19 -        print_ast_translation: (string * (ast list -> ast)) list}
    1.20 -    datatype synrules =
    1.21 -      SynRules of {
    1.22 +        print_ast_translation: (string * (ast list -> ast)) list} |
    1.23 +      ExtRules of {
    1.24          parse_rules: (ast * ast) list,
    1.25 -        print_rules: (ast * ast) list}
    1.26 +        print_rules: (ast * ast) list} |
    1.27 +      ExtRoots of string list
    1.28      val logic: string
    1.29      val args: string
    1.30      val idT: typ
    1.31 @@ -43,10 +42,9 @@
    1.32      val tvarT: typ
    1.33      val typ_to_nonterm: typ -> string
    1.34      val applC: string
    1.35 -    val empty_synrules: synrules
    1.36      val empty_xgram: xgram
    1.37 -    val extend_xgram: xgram -> (ext * synrules) -> xgram
    1.38 -    val mk_xgram: (ext * synrules) -> xgram
    1.39 +    val extend_xgram: xgram -> ext -> xgram
    1.40 +    val mk_xgram: ext -> xgram
    1.41    end
    1.42  end;
    1.43  
    1.44 @@ -76,17 +74,30 @@
    1.45      parse_ast_translation: (string * (ast list -> ast)) list,
    1.46      parse_translation: (string * (term list -> term)) list,
    1.47      print_translation: (string * (term list -> term)) list,
    1.48 -    print_ast_translation: (string * (ast list -> ast)) list};
    1.49 -
    1.50 -datatype synrules =
    1.51 -  SynRules of {
    1.52 +    print_ast_translation: (string * (ast list -> ast)) list} |
    1.53 +  ExtRules of {
    1.54      parse_rules: (ast * ast) list,
    1.55 -    print_rules: (ast * ast) list};
    1.56 +    print_rules: (ast * ast) list} |
    1.57 +  ExtRoots of string list;
    1.58  
    1.59  
    1.60 -(* empty_synrules *)
    1.61 +(* ext_components *)
    1.62  
    1.63 -val empty_synrules = SynRules {parse_rules = [], print_rules = []};
    1.64 +fun ext_components (Ext ext) =
    1.65 +      {roots = #roots ext, mfix = #mfix ext, extra_consts = #extra_consts ext,
    1.66 +      parse_ast_translation = #parse_ast_translation ext,
    1.67 +      parse_translation = #parse_translation ext,
    1.68 +      print_translation = #print_translation ext,
    1.69 +      print_ast_translation = #print_ast_translation ext,
    1.70 +      parse_rules = [], print_rules = []}
    1.71 +  | ext_components (ExtRules {parse_rules, print_rules}) =
    1.72 +      {parse_rules = parse_rules, print_rules = print_rules, roots = [], mfix = [],
    1.73 +      extra_consts = [], parse_ast_translation = [], parse_translation = [],
    1.74 +      print_translation = [], print_ast_translation = []}
    1.75 +  | ext_components (ExtRoots roots) =
    1.76 +      {roots = roots, mfix = [], extra_consts = [], parse_ast_translation = [],
    1.77 +      parse_rules = [], parse_translation = [], print_translation = [],
    1.78 +      print_rules = [], print_ast_translation = []};
    1.79  
    1.80  
    1.81  (* empty_xgram *)
    1.82 @@ -216,9 +227,9 @@
    1.83      seq check_pri pris;
    1.84      check_pri pri;
    1.85      check_blocks symbs;
    1.86 -    if is_terminal lhs then err ("illegal lhs: " ^ lhs) else ();
    1.87  
    1.88 -    if const <> "" then prod
    1.89 +    if is_terminal lhs then err ("illegal lhs: " ^ lhs)
    1.90 +    else if const <> "" then prod
    1.91      else if length (filter is_arg symbs) <> 1 then
    1.92        err "copy production must have exactly one argument"
    1.93      else if exists is_term symbs then prod
    1.94 @@ -229,7 +240,7 @@
    1.95  
    1.96  (** extend_xgram **)
    1.97  
    1.98 -fun extend_xgram (XGram xgram) (Ext ext, SynRules rules) =
    1.99 +fun extend_xgram (XGram xgram) ext =
   1.100    let
   1.101      fun descend (from, to) = Mfix ("_", to --> from, "", [0], 0);
   1.102  
   1.103 @@ -256,11 +267,11 @@
   1.104  
   1.105      val {roots = roots2, mfix, extra_consts,
   1.106        parse_ast_translation = parse_ast_translation2,
   1.107 +      parse_rules = parse_rules2,
   1.108        parse_translation = parse_translation2,
   1.109        print_translation = print_translation2,
   1.110 -      print_ast_translation = print_ast_translation2} = ext;
   1.111 -
   1.112 -    val {parse_rules = parse_rules2, print_rules = print_rules2} = rules;
   1.113 +      print_rules = print_rules2,
   1.114 +      print_ast_translation = print_ast_translation2} = ext_components ext;
   1.115  
   1.116      val Troots = map (apr (Type, [])) (roots2 \\ roots1);
   1.117      val Troots' = Troots \\ [typeT, propT, logicT];