src/Pure/Syntax/syntax.ML
changeset 5692 2e873c5f0e2c
parent 4887 bbc13af86c16
child 5702 77ad51744aee
     1.1 --- a/src/Pure/Syntax/syntax.ML	Tue Oct 20 16:32:20 1998 +0200
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Tue Oct 20 16:33:13 1998 +0200
     1.3 @@ -47,7 +47,6 @@
     1.4    val print_gram: syntax -> unit
     1.5    val print_trans: syntax -> unit
     1.6    val print_syntax: syntax -> unit
     1.7 -  val trfun_names: syntax -> string list * string list * string list * string list
     1.8    val test_read: syntax -> string -> string -> unit
     1.9    val read: syntax -> typ -> string -> term list
    1.10    val read_typ: syntax -> ((indexname * sort) list -> indexname -> sort) -> string -> typ
    1.11 @@ -64,29 +63,22 @@
    1.12  structure Syntax : SYNTAX =
    1.13  struct
    1.14  
    1.15 -open Lexicon SynExt Ast Parser TypeExt SynTrans Mixfix Printer;
    1.16 -
    1.17  
    1.18  (** tables of translation functions **)
    1.19  
    1.20 -(*does not subsume typed print translations*)
    1.21 -type 'a trtab = (('a list -> 'a) * stamp) Symtab.table;
    1.22 -
    1.23 -fun dest_trtab tab = map fst (Symtab.dest tab);
    1.24 -
    1.25 -fun lookup_trtab tab c =
    1.26 -  apsome fst (Symtab.lookup (tab, c));
    1.27 +fun mk_trfun (c, f) = (c, (f, stamp ()));
    1.28 +fun eq_trfuns ((c1:string, (_, s1:stamp)), (c2, (_, s2))) = c1 = c2 andalso s1 = s2;
    1.29  
    1.30  
    1.31 -(* empty, extend, merge trtabs *)
    1.32 +(* parse (ast) translations *)
    1.33 +
    1.34 +fun lookup_tr tab c = apsome fst (Symtab.lookup (tab, c));
    1.35  
    1.36  fun err_dup_trfuns name cs =
    1.37    error ("More than one " ^ name ^ " for " ^ commas_quote cs);
    1.38  
    1.39 -val empty_trtab = Symtab.empty;
    1.40 -
    1.41  fun extend_trtab tab trfuns name =
    1.42 -  Symtab.extend (tab, map (fn (c, f) => (c, (f, stamp ()))) trfuns)
    1.43 +  Symtab.extend (tab, map mk_trfun trfuns)
    1.44      handle Symtab.DUPS cs => err_dup_trfuns name cs;
    1.45  
    1.46  fun merge_trtabs tab1 tab2 name =
    1.47 @@ -94,6 +86,16 @@
    1.48      handle Symtab.DUPS cs => err_dup_trfuns name cs;
    1.49  
    1.50  
    1.51 +(* print (ast) translations *)
    1.52 +
    1.53 +fun lookup_tr' tab c = map fst (Symtab.lookup_multi (tab, c));
    1.54 +
    1.55 +fun extend_tr'tab tab trfuns =
    1.56 +  generic_extend eq_trfuns Symtab.dest_multi Symtab.make_multi tab (map mk_trfun trfuns);
    1.57 +
    1.58 +val merge_tr'tabs = generic_merge eq_trfuns Symtab.dest_multi Symtab.make_multi;
    1.59 +
    1.60 +
    1.61  
    1.62  (** tables of token translation functions **)
    1.63  
    1.64 @@ -134,7 +136,7 @@
    1.65  
    1.66  (** tables of translation rules **)
    1.67  
    1.68 -type ruletab = (ast * ast) list Symtab.table;
    1.69 +type ruletab = (Ast.ast * Ast.ast) list Symtab.table;
    1.70  
    1.71  fun dest_ruletab tab = flat (map snd (Symtab.dest tab));
    1.72  
    1.73 @@ -148,11 +150,9 @@
    1.74  
    1.75  (* empty, extend, merge ruletabs *)
    1.76  
    1.77 -val empty_ruletab = Symtab.empty;
    1.78 -
    1.79  fun extend_ruletab tab rules =
    1.80    generic_extend (op =) Symtab.dest_multi Symtab.make_multi tab
    1.81 -    (map (fn r => (head_of_rule r, r)) (distinct rules));
    1.82 +    (map (fn r => (Ast.head_of_rule r, r)) (distinct rules));
    1.83  
    1.84  fun merge_ruletabs tab1 tab2 =
    1.85    generic_merge (op =) Symtab.dest_multi Symtab.make_multi tab1 tab2;
    1.86 @@ -165,17 +165,17 @@
    1.87    Syntax of {
    1.88      lexicon: Scan.lexicon,
    1.89      logtypes: string list,
    1.90 -    gram: gram,
    1.91 +    gram: Parser.gram,
    1.92      consts: string list,
    1.93      prmodes: string list,
    1.94 -    parse_ast_trtab: ast trtab,
    1.95 +    parse_ast_trtab: ((Ast.ast list -> Ast.ast) * stamp) Symtab.table,
    1.96      parse_ruletab: ruletab,
    1.97 -    parse_trtab: term trtab,
    1.98 -    print_trtab: ((bool -> typ -> term list -> term) * stamp) Symtab.table,
    1.99 +    parse_trtab: ((term list -> term) * stamp) Symtab.table,
   1.100 +    print_trtab: ((bool -> typ -> term list -> term) * stamp) list Symtab.table,
   1.101      print_ruletab: ruletab,
   1.102 -    print_ast_trtab: ast trtab,
   1.103 +    print_ast_trtab: ((Ast.ast list -> Ast.ast) * stamp) list Symtab.table,
   1.104      tokentrtab: (string * (string * ((string -> string * int) * stamp)) list) list,
   1.105 -    prtabs: prtabs}
   1.106 +    prtabs: Printer.prtabs}
   1.107  
   1.108  
   1.109  (* empty_syntax *)
   1.110 @@ -184,17 +184,17 @@
   1.111    Syntax {
   1.112      lexicon = Scan.empty_lexicon,
   1.113      logtypes = [],
   1.114 -    gram = empty_gram,
   1.115 +    gram = Parser.empty_gram,
   1.116      consts = [],
   1.117      prmodes = [],
   1.118 -    parse_ast_trtab = empty_trtab,
   1.119 -    parse_ruletab = empty_ruletab,
   1.120 -    parse_trtab = empty_trtab,
   1.121 -    print_trtab = empty_trtab,
   1.122 -    print_ruletab = empty_ruletab,
   1.123 -    print_ast_trtab = empty_trtab,
   1.124 +    parse_ast_trtab = Symtab.empty,
   1.125 +    parse_ruletab = Symtab.empty,
   1.126 +    parse_trtab = Symtab.empty,
   1.127 +    print_trtab = Symtab.empty,
   1.128 +    print_ruletab = Symtab.empty,
   1.129 +    print_ast_trtab = Symtab.empty,
   1.130      tokentrtab = [],
   1.131 -    prtabs = empty_prtabs}
   1.132 +    prtabs = Printer.empty_prtabs}
   1.133  
   1.134  
   1.135  (* extend_syntax *)
   1.136 @@ -204,26 +204,25 @@
   1.137      val {lexicon, logtypes = logtypes1, gram, consts = consts1, prmodes = prmodes1,
   1.138        parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab, print_ruletab,
   1.139        print_ast_trtab, tokentrtab, prtabs} = tabs;
   1.140 -    val SynExt {logtypes = logtypes2, xprods, consts = consts2, prmodes = prmodes2,
   1.141 +    val SynExt.SynExt {logtypes = logtypes2, xprods, consts = consts2, prmodes = prmodes2,
   1.142        parse_ast_translation, parse_rules, parse_translation, print_translation, print_rules,
   1.143        print_ast_translation, token_translation} = syn_ext;
   1.144    in
   1.145      Syntax {
   1.146 -      lexicon = if inout then Scan.extend_lexicon lexicon (delims_of xprods) else lexicon,
   1.147 +      lexicon = if inout then Scan.extend_lexicon lexicon (SynExt.delims_of xprods) else lexicon,
   1.148        logtypes = extend_list logtypes1 logtypes2,
   1.149 -      gram = if inout then extend_gram gram xprods else gram,
   1.150 +      gram = if inout then Parser.extend_gram gram xprods else gram,
   1.151        consts = consts2 union consts1,
   1.152        prmodes = (mode ins prmodes2) union prmodes1,
   1.153        parse_ast_trtab =
   1.154          extend_trtab parse_ast_trtab parse_ast_translation "parse ast translation",
   1.155        parse_ruletab = extend_ruletab parse_ruletab parse_rules,
   1.156        parse_trtab = extend_trtab parse_trtab parse_translation "parse translation",
   1.157 -      print_trtab = extend_trtab print_trtab print_translation "print translation",
   1.158 +      print_trtab = extend_tr'tab print_trtab print_translation,
   1.159        print_ruletab = extend_ruletab print_ruletab print_rules,
   1.160 -      print_ast_trtab =
   1.161 -        extend_trtab print_ast_trtab print_ast_translation "print ast translation",
   1.162 +      print_ast_trtab = extend_tr'tab print_ast_trtab print_ast_translation,
   1.163        tokentrtab = extend_tokentrtab tokentrtab token_translation,
   1.164 -      prtabs = extend_prtabs prtabs mode xprods}
   1.165 +      prtabs = Printer.extend_prtabs prtabs mode xprods}
   1.166    end;
   1.167  
   1.168  
   1.169 @@ -246,28 +245,25 @@
   1.170      Syntax {
   1.171        lexicon = Scan.merge_lexicons lexicon1 lexicon2,
   1.172        logtypes = merge_lists logtypes1 logtypes2,
   1.173 -      gram = merge_grams gram1 gram2,
   1.174 +      gram = Parser.merge_grams gram1 gram2,
   1.175        consts = merge_lists consts1 consts2,
   1.176        prmodes = merge_lists prmodes1 prmodes2,
   1.177        parse_ast_trtab =
   1.178          merge_trtabs parse_ast_trtab1 parse_ast_trtab2 "parse ast translation",
   1.179        parse_ruletab = merge_ruletabs parse_ruletab1 parse_ruletab2,
   1.180        parse_trtab = merge_trtabs parse_trtab1 parse_trtab2 "parse translation",
   1.181 -      print_trtab = merge_trtabs print_trtab1 print_trtab2 "print translation",
   1.182 +      print_trtab = merge_tr'tabs print_trtab1 print_trtab2,
   1.183        print_ruletab = merge_ruletabs print_ruletab1 print_ruletab2,
   1.184 -      print_ast_trtab =
   1.185 -        merge_trtabs print_ast_trtab1 print_ast_trtab2 "print ast translation",
   1.186 +      print_ast_trtab = merge_tr'tabs print_ast_trtab1 print_ast_trtab2,
   1.187        tokentrtab = merge_tokentrtabs tokentrtab1 tokentrtab2,
   1.188 -      prtabs = merge_prtabs prtabs1 prtabs2}
   1.189 +      prtabs = Printer.merge_prtabs prtabs1 prtabs2}
   1.190    end;
   1.191  
   1.192  
   1.193  (* type_syn *)
   1.194  
   1.195 -val type_syn =
   1.196 -  extend_syntax ("", true) empty_syntax type_ext;
   1.197 -
   1.198 -val pure_syn = extend_syntax ("", true) type_syn pure_ext;
   1.199 +val type_syn = extend_syntax ("", true) empty_syntax TypeExt.type_ext;
   1.200 +val pure_syn = extend_syntax ("", true) type_syn SynExt.pure_ext;
   1.201  
   1.202  
   1.203  
   1.204 @@ -286,7 +282,7 @@
   1.205    in
   1.206      Pretty.writeln (pretty_strs_qs "lexicon:" (map implode (Scan.dest_lexicon lexicon)));
   1.207      Pretty.writeln (Pretty.strs ("logtypes:" :: logtypes));
   1.208 -    Pretty.writeln (Pretty.big_list "prods:" (pretty_gram gram));
   1.209 +    Pretty.writeln (Pretty.big_list "prods:" (Parser.pretty_gram gram));
   1.210      Pretty.writeln (pretty_strs_qs "print modes:" prmodes')
   1.211    end;
   1.212  
   1.213 @@ -296,10 +292,10 @@
   1.214  fun print_trans (Syntax tabs) =
   1.215    let
   1.216      fun pretty_trtab name tab =
   1.217 -      pretty_strs_qs name (dest_trtab tab);
   1.218 +      pretty_strs_qs name (Symtab.keys tab);
   1.219  
   1.220      fun pretty_ruletab name tab =
   1.221 -      Pretty.big_list name (map pretty_rule (dest_ruletab tab));
   1.222 +      Pretty.big_list name (map Ast.pretty_rule (dest_ruletab tab));
   1.223  
   1.224      fun pretty_tokentr (mode, trs) = Pretty.strs (quote mode ^ ":" :: map fst trs);
   1.225  
   1.226 @@ -322,13 +318,6 @@
   1.227  fun print_syntax syn = (print_gram syn; print_trans syn);
   1.228  
   1.229  
   1.230 -(* trfun_names *)
   1.231 -
   1.232 -fun trfun_names (Syntax {parse_ast_trtab, parse_trtab, print_trtab, print_ruletab, ...}) =
   1.233 -  (dest_trtab parse_ast_trtab, dest_trtab parse_trtab,
   1.234 -    dest_trtab print_trtab, dest_trtab print_ruletab);
   1.235 -
   1.236 -
   1.237  
   1.238  (** read **)
   1.239  
   1.240 @@ -339,19 +328,17 @@
   1.241      val {lexicon, gram, parse_ast_trtab, parse_ruletab, ...} = tabs;
   1.242  
   1.243      val chars = Symbol.explode str;
   1.244 -    val toks = tokenize lexicon false chars;
   1.245 -    val _ = writeln ("tokens: " ^ space_implode " " (map display_token toks));
   1.246 +    val toks = Lexicon.tokenize lexicon false chars;
   1.247 +    val _ = writeln ("tokens: " ^ space_implode " " (map Lexicon.display_token toks));
   1.248  
   1.249      fun show_pt pt =
   1.250        let
   1.251 -        val raw_ast = pt_to_ast (K None) pt;
   1.252 -        val _ = writeln ("raw: " ^ str_of_ast raw_ast);
   1.253 -        val pre_ast = pt_to_ast (lookup_trtab parse_ast_trtab) pt;
   1.254 -        val _ = normalize true true (lookup_ruletab parse_ruletab) pre_ast;
   1.255 +        val raw_ast = SynTrans.pt_to_ast (K None) pt;
   1.256 +        val _ = writeln ("raw: " ^ Ast.str_of_ast raw_ast);
   1.257 +        val pre_ast = SynTrans.pt_to_ast (lookup_tr parse_ast_trtab) pt;
   1.258 +        val _ = Ast.normalize true true (lookup_ruletab parse_ruletab) pre_ast;
   1.259        in () end;
   1.260 -  in
   1.261 -    seq show_pt (parse gram root toks)
   1.262 -  end;
   1.263 +  in seq show_pt (Parser.parse gram root toks) end;
   1.264  
   1.265  
   1.266  (* read_ast *)
   1.267 @@ -361,19 +348,19 @@
   1.268  fun read_asts (Syntax tabs) xids root str =
   1.269    let
   1.270      val {lexicon, gram, parse_ast_trtab, logtypes, ...} = tabs;
   1.271 -    val root' = if root mem logtypes then logic else root;
   1.272 +    val root' = if root mem logtypes then SynExt.logic else root;
   1.273      val chars = Symbol.explode str;
   1.274 -    val pts = parse gram root' (tokenize lexicon xids chars);
   1.275 +    val pts = Parser.parse gram root' (Lexicon.tokenize lexicon xids chars);
   1.276  
   1.277      fun show_pt pt =
   1.278 -      warning (Pretty.string_of (pretty_ast (pt_to_ast (K None) pt)));
   1.279 +      warning (Pretty.string_of (Ast.pretty_ast (SynTrans.pt_to_ast (K None) pt)));
   1.280    in
   1.281      if length pts > ! ambiguity_level then
   1.282        (warning ("Ambiguous input " ^ quote str);
   1.283         warning "produces the following parse trees:";
   1.284         seq show_pt pts)
   1.285      else ();
   1.286 -    map (pt_to_ast (lookup_trtab parse_ast_trtab)) pts
   1.287 +    map (SynTrans.pt_to_ast (lookup_tr parse_ast_trtab)) pts
   1.288    end;
   1.289  
   1.290  
   1.291 @@ -382,18 +369,18 @@
   1.292  fun read (syn as Syntax tabs) ty str =
   1.293    let
   1.294      val {parse_ruletab, parse_trtab, ...} = tabs;
   1.295 -    val asts = read_asts syn false (typ_to_nonterm ty) str;
   1.296 +    val asts = read_asts syn false (SynExt.typ_to_nonterm ty) str;
   1.297    in
   1.298 -    map (ast_to_term (lookup_trtab parse_trtab))
   1.299 -      (map (normalize_ast (lookup_ruletab parse_ruletab)) asts)
   1.300 +    map (SynTrans.ast_to_term (lookup_tr parse_trtab))
   1.301 +      (map (Ast.normalize_ast (lookup_ruletab parse_ruletab)) asts)
   1.302    end;
   1.303  
   1.304  
   1.305  (* read types *)
   1.306  
   1.307  fun read_typ syn get_sort str =
   1.308 -  (case read syn typeT str of
   1.309 -    [t] => typ_of_term (get_sort (raw_term_sorts t)) t
   1.310 +  (case read syn SynExt.typeT str of
   1.311 +    [t] => TypeExt.typ_of_term (get_sort (TypeExt.raw_term_sorts t)) t
   1.312    | _ => error "read_typ: ambiguous type syntax");
   1.313  
   1.314  fun simple_read_typ str =
   1.315 @@ -424,10 +411,10 @@
   1.316  
   1.317  
   1.318  fun check_rule (rule as (lhs, rhs)) =
   1.319 -  (case rule_error rule of
   1.320 +  (case Ast.rule_error rule of
   1.321      Some msg =>
   1.322        error ("Error in syntax translation rule: " ^ msg ^ "\n" ^
   1.323 -        str_of_ast lhs ^ "  ->  " ^ str_of_ast rhs)
   1.324 +        Ast.str_of_ast lhs ^ "  ->  " ^ Ast.str_of_ast rhs)
   1.325    | None => rule);
   1.326  
   1.327  
   1.328 @@ -435,11 +422,11 @@
   1.329    let
   1.330      val Syntax {consts, ...} = syn;
   1.331  
   1.332 -    fun constify (ast as Constant _) = ast
   1.333 -      | constify (ast as Variable x) =
   1.334 -          if x mem consts orelse NameSpace.qualified x then Constant x
   1.335 +    fun constify (ast as Ast.Constant _) = ast
   1.336 +      | constify (ast as Ast.Variable x) =
   1.337 +          if x mem consts orelse NameSpace.qualified x then Ast.Constant x
   1.338            else ast
   1.339 -      | constify (Appl asts) = Appl (map constify asts);
   1.340 +      | constify (Ast.Appl asts) = Ast.Appl (map constify asts);
   1.341    in
   1.342      (case read_asts syn true root str of
   1.343        [ast] => constify ast
   1.344 @@ -462,16 +449,16 @@
   1.345  fun pretty_t t_to_ast prt_t (syn as Syntax tabs) curried t =
   1.346    let
   1.347      val {print_trtab, print_ruletab, print_ast_trtab, tokentrtab, prtabs, ...} = tabs;
   1.348 -    val ast = t_to_ast (lookup_trtab print_trtab) t;
   1.349 +    val ast = t_to_ast (lookup_tr' print_trtab) t;
   1.350    in
   1.351 -    prt_t curried prtabs (lookup_trtab print_ast_trtab)
   1.352 -      (lookup_tokentr tokentrtab (! print_mode))
   1.353 -      (normalize_ast (lookup_ruletab print_ruletab) ast)
   1.354 +    prt_t curried prtabs (lookup_tr' print_ast_trtab)
   1.355 +      (lookup_tokentr tokentrtab (! Printer.print_mode))
   1.356 +      (Ast.normalize_ast (lookup_ruletab print_ruletab) ast)
   1.357    end;
   1.358  
   1.359 -val pretty_term = pretty_t term_to_ast pretty_term_ast;
   1.360 -fun pretty_typ syn = pretty_t typ_to_ast pretty_typ_ast syn false;
   1.361 -fun pretty_sort syn = pretty_t sort_to_ast pretty_typ_ast syn false;
   1.362 +val pretty_term = pretty_t Printer.term_to_ast Printer.pretty_term_ast;
   1.363 +fun pretty_typ syn = pretty_t Printer.typ_to_ast Printer.pretty_typ_ast syn false;
   1.364 +fun pretty_sort syn = pretty_t Printer.sort_to_ast Printer.pretty_typ_ast syn false;
   1.365  
   1.366  val simple_str_of_sort = Pretty.str_of o pretty_sort type_syn;
   1.367  val simple_string_of_typ = Pretty.string_of o (pretty_typ type_syn);
   1.368 @@ -486,25 +473,35 @@
   1.369  
   1.370  
   1.371  fun extend_log_types syn logtypes =
   1.372 -  extend_syntax ("", true) syn (syn_ext_logtypes logtypes);
   1.373 +  extend_syntax ("", true) syn (SynExt.syn_ext_logtypes logtypes);
   1.374  
   1.375 -val extend_type_gram = ext_syntax syn_ext_types ("", true);
   1.376 +val extend_type_gram = ext_syntax Mixfix.syn_ext_types ("", true);
   1.377  
   1.378 -fun extend_const_gram syn prmode = ext_syntax syn_ext_consts prmode syn;
   1.379 +fun extend_const_gram syn prmode = ext_syntax Mixfix.syn_ext_consts prmode syn;
   1.380  
   1.381 -val extend_consts = ext_syntax syn_ext_const_names ("", true);
   1.382 +val extend_consts = ext_syntax SynExt.syn_ext_const_names ("", true);
   1.383  
   1.384 -val extend_trfuns = ext_syntax syn_ext_trfuns ("", true);
   1.385 +val extend_trfuns = ext_syntax SynExt.syn_ext_trfuns ("", true);
   1.386  
   1.387 -val extend_trfunsT = ext_syntax syn_ext_trfunsT ("", true);
   1.388 +val extend_trfunsT = ext_syntax SynExt.syn_ext_trfunsT ("", true);
   1.389  
   1.390 -val extend_tokentrfuns = ext_syntax syn_ext_tokentrfuns ("", true);
   1.391 +val extend_tokentrfuns = ext_syntax SynExt.syn_ext_tokentrfuns ("", true);
   1.392  
   1.393  fun extend_trrules syn rules =
   1.394 -  ext_syntax syn_ext_rules ("", true) syn (prep_rules (read_pattern syn) rules);
   1.395 +  ext_syntax SynExt.syn_ext_rules ("", true) syn (prep_rules (read_pattern syn) rules);
   1.396  
   1.397  fun extend_trrules_i syn rules =
   1.398 -  ext_syntax syn_ext_rules ("", true) syn (prep_rules I rules);
   1.399 +  ext_syntax SynExt.syn_ext_rules ("", true) syn (prep_rules I rules);
   1.400 +
   1.401 +
   1.402 +
   1.403 +(** export parts of internal Syntax structures **)
   1.404 +
   1.405 +open Lexicon SynExt Ast Parser TypeExt SynTrans Mixfix Printer;
   1.406  
   1.407  
   1.408  end;
   1.409 +
   1.410 +
   1.411 +structure BasicSyntax: BASIC_SYNTAX = Syntax;
   1.412 +open BasicSyntax;