clarified auxiliary structure Lexicon.Syntax;
authorwenzelm
Tue Apr 26 21:05:52 2011 +0200 (2011-04-26)
changeset 42476d0bc1268ef09
parent 42475 f830a72b27ed
child 42477 52fa26b6c524
clarified auxiliary structure Lexicon.Syntax;
src/Pure/Syntax/lexicon.ML
src/Pure/Syntax/syntax.ML
src/Pure/Syntax/syntax_phases.ML
src/Pure/Syntax/syntax_trans.ML
     1.1 --- a/src/Pure/Syntax/lexicon.ML	Tue Apr 26 17:23:21 2011 +0200
     1.2 +++ b/src/Pure/Syntax/lexicon.ML	Tue Apr 26 21:05:52 2011 +0200
     1.3 @@ -6,6 +6,12 @@
     1.4  
     1.5  signature LEXICON =
     1.6  sig
     1.7 +  structure Syntax:
     1.8 +  sig
     1.9 +    val const: string -> term
    1.10 +    val free: string -> term
    1.11 +    val var: indexname -> term
    1.12 +  end
    1.13    val is_identifier: string -> bool
    1.14    val is_ascii_identifier: string -> bool
    1.15    val is_xid: string -> bool
    1.16 @@ -47,9 +53,6 @@
    1.17    val explode_xstr: string -> string list
    1.18    val tokenize: Scan.lexicon -> bool -> Symbol_Pos.T list -> token list
    1.19    val read_indexname: string -> indexname
    1.20 -  val const: string -> term
    1.21 -  val free: string -> term
    1.22 -  val var: indexname -> term
    1.23    val read_var: string -> term
    1.24    val read_variable: string -> indexname option
    1.25    val read_nat: string -> int option
    1.26 @@ -74,6 +77,19 @@
    1.27  structure Lexicon: LEXICON =
    1.28  struct
    1.29  
    1.30 +(** syntaxtic terms **)
    1.31 +
    1.32 +structure Syntax =
    1.33 +struct
    1.34 +
    1.35 +fun const c = Const (c, dummyT);
    1.36 +fun free x = Free (x, dummyT);
    1.37 +fun var xi = Var (xi, dummyT);
    1.38 +
    1.39 +end;
    1.40 +
    1.41 +
    1.42 +
    1.43  (** is_identifier etc. **)
    1.44  
    1.45  val is_identifier = Symbol.is_ident o Symbol.explode;
    1.46 @@ -328,15 +344,13 @@
    1.47  
    1.48  (* read_var *)
    1.49  
    1.50 -fun const c = Const (c, dummyT);
    1.51 -fun free x = Free (x, dummyT);
    1.52 -fun var xi = Var (xi, dummyT);
    1.53 -
    1.54  fun read_var str =
    1.55    let
    1.56      val scan =
    1.57 -      $$$ "?" |-- scan_indexname --| Scan.ahead (Scan.one Symbol_Pos.is_eof) >> var ||
    1.58 -      Scan.many (Symbol.is_regular o Symbol_Pos.symbol) >> (free o implode o map Symbol_Pos.symbol);
    1.59 +      $$$ "?" |-- scan_indexname --| Scan.ahead (Scan.one Symbol_Pos.is_eof)
    1.60 +        >> Syntax.var ||
    1.61 +      Scan.many (Symbol.is_regular o Symbol_Pos.symbol)
    1.62 +        >> (Syntax.free o implode o map Symbol_Pos.symbol);
    1.63    in the (Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode (str, Position.none))) end;
    1.64  
    1.65  
    1.66 @@ -448,7 +462,7 @@
    1.67    unmark {case_class = K true, case_type = K true, case_const = K true,
    1.68      case_fixed = K true, case_default = K false};
    1.69  
    1.70 -val dummy_type = const (mark_type "dummy");
    1.71 -val fun_type = const (mark_type "fun");
    1.72 +val dummy_type = Syntax.const (mark_type "dummy");
    1.73 +val fun_type = Syntax.const (mark_type "fun");
    1.74  
    1.75  end;
     2.1 --- a/src/Pure/Syntax/syntax.ML	Tue Apr 26 17:23:21 2011 +0200
     2.2 +++ b/src/Pure/Syntax/syntax.ML	Tue Apr 26 21:05:52 2011 +0200
     2.3 @@ -7,9 +7,6 @@
     2.4  
     2.5  signature SYNTAX =
     2.6  sig
     2.7 -  val const: string -> term
     2.8 -  val free: string -> term
     2.9 -  val var: indexname -> term
    2.10    type operations
    2.11    val install_operations: operations -> unit
    2.12    val root: string Config.T
    2.13 @@ -143,16 +140,14 @@
    2.14      mode -> (string * typ * mixfix) list -> syntax -> syntax
    2.15    val update_trrules: Ast.ast trrule list -> syntax -> syntax
    2.16    val remove_trrules: Ast.ast trrule list -> syntax -> syntax
    2.17 +  val const: string -> term
    2.18 +  val free: string -> term
    2.19 +  val var: indexname -> term
    2.20  end;
    2.21  
    2.22  structure Syntax: SYNTAX =
    2.23  struct
    2.24  
    2.25 -val const = Lexicon.const;
    2.26 -val free = Lexicon.free;
    2.27 -val var = Lexicon.var;
    2.28 -
    2.29 -
    2.30  
    2.31  (** inner syntax operations **)
    2.32  
    2.33 @@ -750,5 +745,8 @@
    2.34  val update_trrules = ext_syntax Syntax_Ext.syn_ext_rules o check_rules;
    2.35  val remove_trrules = remove_syntax mode_default o Syntax_Ext.syn_ext_rules o check_rules;
    2.36  
    2.37 +
    2.38 +open Lexicon.Syntax;
    2.39 +
    2.40  end;
    2.41  
     3.1 --- a/src/Pure/Syntax/syntax_phases.ML	Tue Apr 26 17:23:21 2011 +0200
     3.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Tue Apr 26 21:05:52 2011 +0200
     3.3 @@ -180,7 +180,7 @@
     3.4    let
     3.5      fun trans a args =
     3.6        (case trf a of
     3.7 -        NONE => Term.list_comb (Lexicon.const a, args)
     3.8 +        NONE => Term.list_comb (Syntax.const a, args)
     3.9        | SOME f => f ctxt args);
    3.10  
    3.11      fun term_of (Ast.Constant a) = trans a []
    3.12 @@ -424,15 +424,15 @@
    3.13  
    3.14  fun term_of_sort S =
    3.15    let
    3.16 -    val class = Lexicon.const o Lexicon.mark_class;
    3.17 +    val class = Syntax.const o Lexicon.mark_class;
    3.18  
    3.19      fun classes [c] = class c
    3.20 -      | classes (c :: cs) = Lexicon.const "_classes" $ class c $ classes cs;
    3.21 +      | classes (c :: cs) = Syntax.const "_classes" $ class c $ classes cs;
    3.22    in
    3.23      (case S of
    3.24 -      [] => Lexicon.const "_topsort"
    3.25 +      [] => Syntax.const "_topsort"
    3.26      | [c] => class c
    3.27 -    | cs => Lexicon.const "_sort" $ classes cs)
    3.28 +    | cs => Syntax.const "_sort" $ classes cs)
    3.29    end;
    3.30  
    3.31  
    3.32 @@ -443,15 +443,15 @@
    3.33      val show_sorts = Config.get ctxt show_sorts;
    3.34  
    3.35      fun of_sort t S =
    3.36 -      if show_sorts then Lexicon.const "_ofsort" $ t $ term_of_sort S
    3.37 +      if show_sorts then Syntax.const "_ofsort" $ t $ term_of_sort S
    3.38        else t;
    3.39  
    3.40      fun term_of (Type (a, Ts)) =
    3.41 -          Term.list_comb (Lexicon.const (Lexicon.mark_type a), map term_of Ts)
    3.42 +          Term.list_comb (Syntax.const (Lexicon.mark_type a), map term_of Ts)
    3.43        | term_of (TFree (x, S)) =
    3.44            if is_some (Term_Position.decode x) then Syntax.free x
    3.45 -          else of_sort (Lexicon.const "_tfree" $ Syntax.free x) S
    3.46 -      | term_of (TVar (xi, S)) = of_sort (Lexicon.const "_tvar" $ Syntax.var xi) S;
    3.47 +          else of_sort (Syntax.const "_tfree" $ Syntax.free x) S
    3.48 +      | term_of (TVar (xi, S)) = of_sort (Syntax.const "_tvar" $ Syntax.var xi) S;
    3.49    in term_of ty end;
    3.50  
    3.51  
    3.52 @@ -518,12 +518,12 @@
    3.53              if i = 0 andalso member (op =) fixes x then
    3.54                Const (Lexicon.mark_fixed x, T)
    3.55              else if i = 1 andalso not show_structs then
    3.56 -              Lexicon.const "_struct" $ Lexicon.const "_indexdefault"
    3.57 -            else Lexicon.const "_free" $ t
    3.58 +              Syntax.const "_struct" $ Syntax.const "_indexdefault"
    3.59 +            else Syntax.const "_free" $ t
    3.60            end
    3.61        | mark_atoms (t as Var (xi, T)) =
    3.62            if xi = Syntax_Ext.dddot_indexname then Const ("_DDDOT", T)
    3.63 -          else Lexicon.const "_var" $ t
    3.64 +          else Syntax.const "_var" $ t
    3.65        | mark_atoms a = a;
    3.66  
    3.67      fun prune_typs (t_seen as (Const _, _)) = t_seen
    3.68 @@ -555,7 +555,7 @@
    3.69        | ((c as Const ("_bound", _)), Free (x, T) :: ts) =>
    3.70            Ast.mk_appl (constrain (c $ Syntax.free x) T) (map ast_of ts)
    3.71        | (Const ("_idtdummy", T), ts) =>
    3.72 -          Ast.mk_appl (constrain (Lexicon.const "_idtdummy") T) (map ast_of ts)
    3.73 +          Ast.mk_appl (constrain (Syntax.const "_idtdummy") T) (map ast_of ts)
    3.74        | (const as Const (c, T), ts) =>
    3.75            if show_all_types
    3.76            then Ast.mk_appl (constrain const T) (map ast_of ts)
    3.77 @@ -660,23 +660,23 @@
    3.78  (* type propositions *)
    3.79  
    3.80  fun type_prop_tr' ctxt T [Const ("\\<^const>Pure.sort_constraint", _)] =
    3.81 -      Lexicon.const "_sort_constraint" $ term_of_typ (Config.put show_sorts true ctxt) T
    3.82 +      Syntax.const "_sort_constraint" $ term_of_typ (Config.put show_sorts true ctxt) T
    3.83    | type_prop_tr' ctxt T [t] =
    3.84 -      Lexicon.const "_ofclass" $ term_of_typ ctxt T $ t
    3.85 +      Syntax.const "_ofclass" $ term_of_typ ctxt T $ t
    3.86    | type_prop_tr' _ T ts = raise TYPE ("type_prop_tr'", [T], ts);
    3.87  
    3.88  
    3.89  (* type reflection *)
    3.90  
    3.91  fun type_tr' ctxt (Type ("itself", [T])) ts =
    3.92 -      Term.list_comb (Lexicon.const "_TYPE" $ term_of_typ ctxt T, ts)
    3.93 +      Term.list_comb (Syntax.const "_TYPE" $ term_of_typ ctxt T, ts)
    3.94    | type_tr' _ _ _ = raise Match;
    3.95  
    3.96  
    3.97  (* type constraints *)
    3.98  
    3.99  fun type_constraint_tr' ctxt (Type ("fun", [T, _])) (t :: ts) =
   3.100 -      Term.list_comb (Lexicon.const "_constrain" $ t $ term_of_typ ctxt T, ts)
   3.101 +      Term.list_comb (Syntax.const "_constrain" $ t $ term_of_typ ctxt T, ts)
   3.102    | type_constraint_tr' _ _ _ = raise Match;
   3.103  
   3.104  
     4.1 --- a/src/Pure/Syntax/syntax_trans.ML	Tue Apr 26 17:23:21 2011 +0200
     4.2 +++ b/src/Pure/Syntax/syntax_trans.ML	Tue Apr 26 21:05:52 2011 +0200
     4.3 @@ -58,6 +58,9 @@
     4.4  structure Syntax_Trans: SYNTAX_TRANS =
     4.5  struct
     4.6  
     4.7 +structure Syntax = Lexicon.Syntax;
     4.8 +
     4.9 +
    4.10  (* print mode *)
    4.11  
    4.12  val bracketsN = "brackets";
    4.13 @@ -130,7 +133,7 @@
    4.14  fun abs_tr [Free (x, T), t] = absfree_proper (x, T, t)
    4.15    | abs_tr [Const ("_idtdummy", T), t] = Term.absdummy (T, t)
    4.16    | abs_tr [Const ("_constrain", _) $ x $ tT, t] =
    4.17 -      Lexicon.const "_constrainAbs" $ abs_tr [x, t] $ tT
    4.18 +      Syntax.const "_constrainAbs" $ abs_tr [x, t] $ tT
    4.19    | abs_tr ts = raise TERM ("abs_tr", ts);
    4.20  
    4.21  
    4.22 @@ -142,7 +145,7 @@
    4.23      fun binder_tr [Const ("_idts", _) $ idt $ idts, t] = binder_tr [idt, binder_tr [idts, t]]
    4.24        | binder_tr [x, t] =
    4.25            let val abs = abs_tr [x, t] handle TERM _ => err [x, t]
    4.26 -          in Lexicon.const name $ abs end
    4.27 +          in Syntax.const name $ abs end
    4.28        | binder_tr ts = err ts;
    4.29    in (syn, binder_tr) end;
    4.30  
    4.31 @@ -150,19 +153,19 @@
    4.32  (* type propositions *)
    4.33  
    4.34  fun mk_type ty =
    4.35 -  Lexicon.const "_constrain" $
    4.36 -    Lexicon.const "\\<^const>TYPE" $ (Lexicon.const "\\<^type>itself" $ ty);
    4.37 +  Syntax.const "_constrain" $
    4.38 +    Syntax.const "\\<^const>TYPE" $ (Syntax.const "\\<^type>itself" $ ty);
    4.39  
    4.40  fun ofclass_tr [ty, cls] = cls $ mk_type ty
    4.41    | ofclass_tr ts = raise TERM ("ofclass_tr", ts);
    4.42  
    4.43 -fun sort_constraint_tr [ty] = Lexicon.const "\\<^const>Pure.sort_constraint" $ mk_type ty
    4.44 +fun sort_constraint_tr [ty] = Syntax.const "\\<^const>Pure.sort_constraint" $ mk_type ty
    4.45    | sort_constraint_tr ts = raise TERM ("sort_constraint_tr", ts);
    4.46  
    4.47  
    4.48  (* meta propositions *)
    4.49  
    4.50 -fun aprop_tr [t] = Lexicon.const "_constrain" $ t $ Lexicon.const "\\<^type>prop"
    4.51 +fun aprop_tr [t] = Syntax.const "_constrain" $ t $ Syntax.const "\\<^type>prop"
    4.52    | aprop_tr ts = raise TERM ("aprop_tr", ts);
    4.53  
    4.54  
    4.55 @@ -185,7 +188,7 @@
    4.56  
    4.57  (* dddot *)
    4.58  
    4.59 -fun dddot_tr ts = Term.list_comb (Lexicon.var Syntax_Ext.dddot_indexname, ts);
    4.60 +fun dddot_tr ts = Term.list_comb (Syntax.var Syntax_Ext.dddot_indexname, ts);
    4.61  
    4.62  
    4.63  (* quote / antiquote *)
    4.64 @@ -204,7 +207,7 @@
    4.65  
    4.66  fun quote_antiquote_tr quoteN antiquoteN name =
    4.67    let
    4.68 -    fun tr [t] = Lexicon.const name $ quote_tr antiquoteN t
    4.69 +    fun tr [t] = Syntax.const name $ quote_tr antiquoteN t
    4.70        | tr ts = raise TERM ("quote_tr", ts);
    4.71    in (quoteN, tr) end;
    4.72  
    4.73 @@ -250,9 +253,9 @@
    4.74    else error ("Illegal reference to implicit structure #" ^ string_of_int i);
    4.75  
    4.76  fun struct_tr structs [Const ("_indexdefault", _)] =
    4.77 -      Lexicon.free (the_struct structs 1)
    4.78 +      Syntax.free (the_struct structs 1)
    4.79    | struct_tr structs [t as (Const ("_indexnum", _) $ Const (s, _))] =
    4.80 -      Lexicon.free (the_struct structs
    4.81 +      Syntax.free (the_struct structs
    4.82          (case Lexicon.read_nat s of SOME n => n | NONE => raise TERM ("struct_tr", [t])))
    4.83    | struct_tr _ ts = raise TERM ("struct_tr", ts);
    4.84  
    4.85 @@ -335,7 +338,7 @@
    4.86  
    4.87  
    4.88  fun abs_tr' ctxt tm =
    4.89 -  uncurry (fold_rev (fn x => fn t => Lexicon.const "_abs" $ x $ t))
    4.90 +  uncurry (fold_rev (fn x => fn t => Syntax.const "_abs" $ x $ t))
    4.91      (strip_abss strip_abs_vars strip_abs_body (eta_contr ctxt tm));
    4.92  
    4.93  fun atomic_abs_tr' (x, T, t) =
    4.94 @@ -361,24 +364,24 @@
    4.95    let
    4.96      fun mk_idts [] = raise Match    (*abort translation*)
    4.97        | mk_idts [idt] = idt
    4.98 -      | mk_idts (idt :: idts) = Lexicon.const "_idts" $ idt $ mk_idts idts;
    4.99 +      | mk_idts (idt :: idts) = Syntax.const "_idts" $ idt $ mk_idts idts;
   4.100  
   4.101      fun tr' t =
   4.102        let
   4.103          val (xs, bd) = strip_abss (strip_qnt_vars name) (strip_qnt_body name) t;
   4.104 -      in Lexicon.const syn $ mk_idts xs $ bd end;
   4.105 +      in Syntax.const syn $ mk_idts xs $ bd end;
   4.106  
   4.107 -    fun binder_tr' (t :: ts) = Term.list_comb (tr' (Lexicon.const name $ t), ts)
   4.108 +    fun binder_tr' (t :: ts) = Term.list_comb (tr' (Syntax.const name $ t), ts)
   4.109        | binder_tr' [] = raise Match;
   4.110    in (name, binder_tr') end;
   4.111  
   4.112  fun preserve_binder_abs_tr' name syn = (name, fn Abs abs :: ts =>
   4.113    let val (x, t) = atomic_abs_tr' abs
   4.114 -  in list_comb (Lexicon.const syn $ x $ t, ts) end);
   4.115 +  in list_comb (Syntax.const syn $ x $ t, ts) end);
   4.116  
   4.117  fun preserve_binder_abs2_tr' name syn = (name, fn A :: Abs abs :: ts =>
   4.118    let val (x, t) = atomic_abs_tr' abs
   4.119 -  in list_comb (Lexicon.const syn $ x $ A $ t, ts) end);
   4.120 +  in list_comb (Syntax.const syn $ x $ A $ t, ts) end);
   4.121  
   4.122  
   4.123  (* idtyp constraints *)
   4.124 @@ -392,7 +395,7 @@
   4.125  
   4.126  fun prop_tr' tm =
   4.127    let
   4.128 -    fun aprop t = Lexicon.const "_aprop" $ t;
   4.129 +    fun aprop t = Syntax.const "_aprop" $ t;
   4.130  
   4.131      fun is_prop Ts t =
   4.132        fastype_of1 (Ts, t) = propT handle TERM _ => false;
   4.133 @@ -404,9 +407,9 @@
   4.134        | tr' Ts (t as Const ("_bound", _) $ u) =
   4.135            if is_prop Ts u then aprop t else t
   4.136        | tr' _ (t as Free (x, T)) =
   4.137 -          if T = propT then aprop (Lexicon.free x) else t
   4.138 +          if T = propT then aprop (Syntax.free x) else t
   4.139        | tr' _ (t as Var (xi, T)) =
   4.140 -          if T = propT then aprop (Lexicon.var xi) else t
   4.141 +          if T = propT then aprop (Syntax.var xi) else t
   4.142        | tr' Ts (t as Bound _) =
   4.143            if is_prop Ts t then aprop t else t
   4.144        | tr' Ts (Abs (x, T, t)) = Abs (x, T, tr' (T :: Ts) t)
   4.145 @@ -445,8 +448,8 @@
   4.146  fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) =
   4.147        if Term.is_dependent B then
   4.148          let val (x', B') = variant_abs' (x, dummyT, B);
   4.149 -        in Term.list_comb (Lexicon.const q $ mark_boundT (x', T) $ A $ B', ts) end
   4.150 -      else Term.list_comb (Lexicon.const r $ A $ incr_boundvars ~1 B, ts)
   4.151 +        in Term.list_comb (Syntax.const q $ mark_boundT (x', T) $ A $ B', ts) end
   4.152 +      else Term.list_comb (Syntax.const r $ A $ incr_boundvars ~1 B, ts)
   4.153    | dependent_tr' _ _ = raise Match;
   4.154  
   4.155  
   4.156 @@ -455,7 +458,7 @@
   4.157  fun antiquote_tr' name =
   4.158    let
   4.159      fun tr' i (t $ u) =
   4.160 -          if u aconv Bound i then Lexicon.const name $ tr' i t
   4.161 +          if u aconv Bound i then Syntax.const name $ tr' i t
   4.162            else tr' i t $ tr' i u
   4.163        | tr' i (Abs (x, T, t)) = Abs (x, T, tr' (i + 1) t)
   4.164        | tr' i a = if a aconv Bound i then raise Match else a;
   4.165 @@ -466,7 +469,7 @@
   4.166  
   4.167  fun quote_antiquote_tr' quoteN antiquoteN name =
   4.168    let
   4.169 -    fun tr' (t :: ts) = Term.list_comb (Lexicon.const quoteN $ quote_tr' antiquoteN t, ts)
   4.170 +    fun tr' (t :: ts) = Term.list_comb (Syntax.const quoteN $ quote_tr' antiquoteN t, ts)
   4.171        | tr' _ = raise Match;
   4.172    in (name, tr') end;
   4.173