# HG changeset patch
# User wenzelm
# Date 1303844752 -7200
# Node ID d0bc1268ef09113f42560f657a9bc2dfa4200ad5
# Parent  f830a72b27ed42258b49dacf7a2149002c4889b8
clarified auxiliary structure Lexicon.Syntax;

diff -r f830a72b27ed -r d0bc1268ef09 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Tue Apr 26 17:23:21 2011 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Tue Apr 26 21:05:52 2011 +0200
@@ -6,6 +6,12 @@
 
 signature LEXICON =
 sig
+  structure Syntax:
+  sig
+    val const: string -> term
+    val free: string -> term
+    val var: indexname -> term
+  end
   val is_identifier: string -> bool
   val is_ascii_identifier: string -> bool
   val is_xid: string -> bool
@@ -47,9 +53,6 @@
   val explode_xstr: string -> string list
   val tokenize: Scan.lexicon -> bool -> Symbol_Pos.T list -> token list
   val read_indexname: string -> indexname
-  val const: string -> term
-  val free: string -> term
-  val var: indexname -> term
   val read_var: string -> term
   val read_variable: string -> indexname option
   val read_nat: string -> int option
@@ -74,6 +77,19 @@
 structure Lexicon: LEXICON =
 struct
 
+(** syntaxtic terms **)
+
+structure Syntax =
+struct
+
+fun const c = Const (c, dummyT);
+fun free x = Free (x, dummyT);
+fun var xi = Var (xi, dummyT);
+
+end;
+
+
+
 (** is_identifier etc. **)
 
 val is_identifier = Symbol.is_ident o Symbol.explode;
@@ -328,15 +344,13 @@
 
 (* read_var *)
 
-fun const c = Const (c, dummyT);
-fun free x = Free (x, dummyT);
-fun var xi = Var (xi, dummyT);
-
 fun read_var str =
   let
     val scan =
-      $$$ "?" |-- scan_indexname --| Scan.ahead (Scan.one Symbol_Pos.is_eof) >> var ||
-      Scan.many (Symbol.is_regular o Symbol_Pos.symbol) >> (free o implode o map Symbol_Pos.symbol);
+      $$$ "?" |-- scan_indexname --| Scan.ahead (Scan.one Symbol_Pos.is_eof)
+        >> Syntax.var ||
+      Scan.many (Symbol.is_regular o Symbol_Pos.symbol)
+        >> (Syntax.free o implode o map Symbol_Pos.symbol);
   in the (Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode (str, Position.none))) end;
 
 
@@ -448,7 +462,7 @@
   unmark {case_class = K true, case_type = K true, case_const = K true,
     case_fixed = K true, case_default = K false};
 
-val dummy_type = const (mark_type "dummy");
-val fun_type = const (mark_type "fun");
+val dummy_type = Syntax.const (mark_type "dummy");
+val fun_type = Syntax.const (mark_type "fun");
 
 end;
diff -r f830a72b27ed -r d0bc1268ef09 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Tue Apr 26 17:23:21 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML	Tue Apr 26 21:05:52 2011 +0200
@@ -7,9 +7,6 @@
 
 signature SYNTAX =
 sig
-  val const: string -> term
-  val free: string -> term
-  val var: indexname -> term
   type operations
   val install_operations: operations -> unit
   val root: string Config.T
@@ -143,16 +140,14 @@
     mode -> (string * typ * mixfix) list -> syntax -> syntax
   val update_trrules: Ast.ast trrule list -> syntax -> syntax
   val remove_trrules: Ast.ast trrule list -> syntax -> syntax
+  val const: string -> term
+  val free: string -> term
+  val var: indexname -> term
 end;
 
 structure Syntax: SYNTAX =
 struct
 
-val const = Lexicon.const;
-val free = Lexicon.free;
-val var = Lexicon.var;
-
-
 
 (** inner syntax operations **)
 
@@ -750,5 +745,8 @@
 val update_trrules = ext_syntax Syntax_Ext.syn_ext_rules o check_rules;
 val remove_trrules = remove_syntax mode_default o Syntax_Ext.syn_ext_rules o check_rules;
 
+
+open Lexicon.Syntax;
+
 end;
 
diff -r f830a72b27ed -r d0bc1268ef09 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Tue Apr 26 17:23:21 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Tue Apr 26 21:05:52 2011 +0200
@@ -180,7 +180,7 @@
   let
     fun trans a args =
       (case trf a of
-        NONE => Term.list_comb (Lexicon.const a, args)
+        NONE => Term.list_comb (Syntax.const a, args)
       | SOME f => f ctxt args);
 
     fun term_of (Ast.Constant a) = trans a []
@@ -424,15 +424,15 @@
 
 fun term_of_sort S =
   let
-    val class = Lexicon.const o Lexicon.mark_class;
+    val class = Syntax.const o Lexicon.mark_class;
 
     fun classes [c] = class c
-      | classes (c :: cs) = Lexicon.const "_classes" $ class c $ classes cs;
+      | classes (c :: cs) = Syntax.const "_classes" $ class c $ classes cs;
   in
     (case S of
-      [] => Lexicon.const "_topsort"
+      [] => Syntax.const "_topsort"
     | [c] => class c
-    | cs => Lexicon.const "_sort" $ classes cs)
+    | cs => Syntax.const "_sort" $ classes cs)
   end;
 
 
@@ -443,15 +443,15 @@
     val show_sorts = Config.get ctxt show_sorts;
 
     fun of_sort t S =
-      if show_sorts then Lexicon.const "_ofsort" $ t $ term_of_sort S
+      if show_sorts then Syntax.const "_ofsort" $ t $ term_of_sort S
       else t;
 
     fun term_of (Type (a, Ts)) =
-          Term.list_comb (Lexicon.const (Lexicon.mark_type a), map term_of Ts)
+          Term.list_comb (Syntax.const (Lexicon.mark_type a), map term_of Ts)
       | term_of (TFree (x, S)) =
           if is_some (Term_Position.decode x) then Syntax.free x
-          else of_sort (Lexicon.const "_tfree" $ Syntax.free x) S
-      | term_of (TVar (xi, S)) = of_sort (Lexicon.const "_tvar" $ Syntax.var xi) S;
+          else of_sort (Syntax.const "_tfree" $ Syntax.free x) S
+      | term_of (TVar (xi, S)) = of_sort (Syntax.const "_tvar" $ Syntax.var xi) S;
   in term_of ty end;
 
 
@@ -518,12 +518,12 @@
             if i = 0 andalso member (op =) fixes x then
               Const (Lexicon.mark_fixed x, T)
             else if i = 1 andalso not show_structs then
-              Lexicon.const "_struct" $ Lexicon.const "_indexdefault"
-            else Lexicon.const "_free" $ t
+              Syntax.const "_struct" $ Syntax.const "_indexdefault"
+            else Syntax.const "_free" $ t
           end
       | mark_atoms (t as Var (xi, T)) =
           if xi = Syntax_Ext.dddot_indexname then Const ("_DDDOT", T)
-          else Lexicon.const "_var" $ t
+          else Syntax.const "_var" $ t
       | mark_atoms a = a;
 
     fun prune_typs (t_seen as (Const _, _)) = t_seen
@@ -555,7 +555,7 @@
       | ((c as Const ("_bound", _)), Free (x, T) :: ts) =>
           Ast.mk_appl (constrain (c $ Syntax.free x) T) (map ast_of ts)
       | (Const ("_idtdummy", T), ts) =>
-          Ast.mk_appl (constrain (Lexicon.const "_idtdummy") T) (map ast_of ts)
+          Ast.mk_appl (constrain (Syntax.const "_idtdummy") T) (map ast_of ts)
       | (const as Const (c, T), ts) =>
           if show_all_types
           then Ast.mk_appl (constrain const T) (map ast_of ts)
@@ -660,23 +660,23 @@
 (* type propositions *)
 
 fun type_prop_tr' ctxt T [Const ("\\<^const>Pure.sort_constraint", _)] =
-      Lexicon.const "_sort_constraint" $ term_of_typ (Config.put show_sorts true ctxt) T
+      Syntax.const "_sort_constraint" $ term_of_typ (Config.put show_sorts true ctxt) T
   | type_prop_tr' ctxt T [t] =
-      Lexicon.const "_ofclass" $ term_of_typ ctxt T $ t
+      Syntax.const "_ofclass" $ term_of_typ ctxt T $ t
   | type_prop_tr' _ T ts = raise TYPE ("type_prop_tr'", [T], ts);
 
 
 (* type reflection *)
 
 fun type_tr' ctxt (Type ("itself", [T])) ts =
-      Term.list_comb (Lexicon.const "_TYPE" $ term_of_typ ctxt T, ts)
+      Term.list_comb (Syntax.const "_TYPE" $ term_of_typ ctxt T, ts)
   | type_tr' _ _ _ = raise Match;
 
 
 (* type constraints *)
 
 fun type_constraint_tr' ctxt (Type ("fun", [T, _])) (t :: ts) =
-      Term.list_comb (Lexicon.const "_constrain" $ t $ term_of_typ ctxt T, ts)
+      Term.list_comb (Syntax.const "_constrain" $ t $ term_of_typ ctxt T, ts)
   | type_constraint_tr' _ _ _ = raise Match;
 
 
diff -r f830a72b27ed -r d0bc1268ef09 src/Pure/Syntax/syntax_trans.ML
--- a/src/Pure/Syntax/syntax_trans.ML	Tue Apr 26 17:23:21 2011 +0200
+++ b/src/Pure/Syntax/syntax_trans.ML	Tue Apr 26 21:05:52 2011 +0200
@@ -58,6 +58,9 @@
 structure Syntax_Trans: SYNTAX_TRANS =
 struct
 
+structure Syntax = Lexicon.Syntax;
+
+
 (* print mode *)
 
 val bracketsN = "brackets";
@@ -130,7 +133,7 @@
 fun abs_tr [Free (x, T), t] = absfree_proper (x, T, t)
   | abs_tr [Const ("_idtdummy", T), t] = Term.absdummy (T, t)
   | abs_tr [Const ("_constrain", _) $ x $ tT, t] =
-      Lexicon.const "_constrainAbs" $ abs_tr [x, t] $ tT
+      Syntax.const "_constrainAbs" $ abs_tr [x, t] $ tT
   | abs_tr ts = raise TERM ("abs_tr", ts);
 
 
@@ -142,7 +145,7 @@
     fun binder_tr [Const ("_idts", _) $ idt $ idts, t] = binder_tr [idt, binder_tr [idts, t]]
       | binder_tr [x, t] =
           let val abs = abs_tr [x, t] handle TERM _ => err [x, t]
-          in Lexicon.const name $ abs end
+          in Syntax.const name $ abs end
       | binder_tr ts = err ts;
   in (syn, binder_tr) end;
 
@@ -150,19 +153,19 @@
 (* type propositions *)
 
 fun mk_type ty =
-  Lexicon.const "_constrain" $
-    Lexicon.const "\\<^const>TYPE" $ (Lexicon.const "\\<^type>itself" $ ty);
+  Syntax.const "_constrain" $
+    Syntax.const "\\<^const>TYPE" $ (Syntax.const "\\<^type>itself" $ ty);
 
 fun ofclass_tr [ty, cls] = cls $ mk_type ty
   | ofclass_tr ts = raise TERM ("ofclass_tr", ts);
 
-fun sort_constraint_tr [ty] = Lexicon.const "\\<^const>Pure.sort_constraint" $ mk_type ty
+fun sort_constraint_tr [ty] = Syntax.const "\\<^const>Pure.sort_constraint" $ mk_type ty
   | sort_constraint_tr ts = raise TERM ("sort_constraint_tr", ts);
 
 
 (* meta propositions *)
 
-fun aprop_tr [t] = Lexicon.const "_constrain" $ t $ Lexicon.const "\\<^type>prop"
+fun aprop_tr [t] = Syntax.const "_constrain" $ t $ Syntax.const "\\<^type>prop"
   | aprop_tr ts = raise TERM ("aprop_tr", ts);
 
 
@@ -185,7 +188,7 @@
 
 (* dddot *)
 
-fun dddot_tr ts = Term.list_comb (Lexicon.var Syntax_Ext.dddot_indexname, ts);
+fun dddot_tr ts = Term.list_comb (Syntax.var Syntax_Ext.dddot_indexname, ts);
 
 
 (* quote / antiquote *)
@@ -204,7 +207,7 @@
 
 fun quote_antiquote_tr quoteN antiquoteN name =
   let
-    fun tr [t] = Lexicon.const name $ quote_tr antiquoteN t
+    fun tr [t] = Syntax.const name $ quote_tr antiquoteN t
       | tr ts = raise TERM ("quote_tr", ts);
   in (quoteN, tr) end;
 
@@ -250,9 +253,9 @@
   else error ("Illegal reference to implicit structure #" ^ string_of_int i);
 
 fun struct_tr structs [Const ("_indexdefault", _)] =
-      Lexicon.free (the_struct structs 1)
+      Syntax.free (the_struct structs 1)
   | struct_tr structs [t as (Const ("_indexnum", _) $ Const (s, _))] =
-      Lexicon.free (the_struct structs
+      Syntax.free (the_struct structs
         (case Lexicon.read_nat s of SOME n => n | NONE => raise TERM ("struct_tr", [t])))
   | struct_tr _ ts = raise TERM ("struct_tr", ts);
 
@@ -335,7 +338,7 @@
 
 
 fun abs_tr' ctxt tm =
-  uncurry (fold_rev (fn x => fn t => Lexicon.const "_abs" $ x $ t))
+  uncurry (fold_rev (fn x => fn t => Syntax.const "_abs" $ x $ t))
     (strip_abss strip_abs_vars strip_abs_body (eta_contr ctxt tm));
 
 fun atomic_abs_tr' (x, T, t) =
@@ -361,24 +364,24 @@
   let
     fun mk_idts [] = raise Match    (*abort translation*)
       | mk_idts [idt] = idt
-      | mk_idts (idt :: idts) = Lexicon.const "_idts" $ idt $ mk_idts idts;
+      | mk_idts (idt :: idts) = Syntax.const "_idts" $ idt $ mk_idts idts;
 
     fun tr' t =
       let
         val (xs, bd) = strip_abss (strip_qnt_vars name) (strip_qnt_body name) t;
-      in Lexicon.const syn $ mk_idts xs $ bd end;
+      in Syntax.const syn $ mk_idts xs $ bd end;
 
-    fun binder_tr' (t :: ts) = Term.list_comb (tr' (Lexicon.const name $ t), ts)
+    fun binder_tr' (t :: ts) = Term.list_comb (tr' (Syntax.const name $ t), ts)
       | binder_tr' [] = raise Match;
   in (name, binder_tr') end;
 
 fun preserve_binder_abs_tr' name syn = (name, fn Abs abs :: ts =>
   let val (x, t) = atomic_abs_tr' abs
-  in list_comb (Lexicon.const syn $ x $ t, ts) end);
+  in list_comb (Syntax.const syn $ x $ t, ts) end);
 
 fun preserve_binder_abs2_tr' name syn = (name, fn A :: Abs abs :: ts =>
   let val (x, t) = atomic_abs_tr' abs
-  in list_comb (Lexicon.const syn $ x $ A $ t, ts) end);
+  in list_comb (Syntax.const syn $ x $ A $ t, ts) end);
 
 
 (* idtyp constraints *)
@@ -392,7 +395,7 @@
 
 fun prop_tr' tm =
   let
-    fun aprop t = Lexicon.const "_aprop" $ t;
+    fun aprop t = Syntax.const "_aprop" $ t;
 
     fun is_prop Ts t =
       fastype_of1 (Ts, t) = propT handle TERM _ => false;
@@ -404,9 +407,9 @@
       | tr' Ts (t as Const ("_bound", _) $ u) =
           if is_prop Ts u then aprop t else t
       | tr' _ (t as Free (x, T)) =
-          if T = propT then aprop (Lexicon.free x) else t
+          if T = propT then aprop (Syntax.free x) else t
       | tr' _ (t as Var (xi, T)) =
-          if T = propT then aprop (Lexicon.var xi) else t
+          if T = propT then aprop (Syntax.var xi) else t
       | tr' Ts (t as Bound _) =
           if is_prop Ts t then aprop t else t
       | tr' Ts (Abs (x, T, t)) = Abs (x, T, tr' (T :: Ts) t)
@@ -445,8 +448,8 @@
 fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) =
       if Term.is_dependent B then
         let val (x', B') = variant_abs' (x, dummyT, B);
-        in Term.list_comb (Lexicon.const q $ mark_boundT (x', T) $ A $ B', ts) end
-      else Term.list_comb (Lexicon.const r $ A $ incr_boundvars ~1 B, ts)
+        in Term.list_comb (Syntax.const q $ mark_boundT (x', T) $ A $ B', ts) end
+      else Term.list_comb (Syntax.const r $ A $ incr_boundvars ~1 B, ts)
   | dependent_tr' _ _ = raise Match;
 
 
@@ -455,7 +458,7 @@
 fun antiquote_tr' name =
   let
     fun tr' i (t $ u) =
-          if u aconv Bound i then Lexicon.const name $ tr' i t
+          if u aconv Bound i then Syntax.const name $ tr' i t
           else tr' i t $ tr' i u
       | tr' i (Abs (x, T, t)) = Abs (x, T, tr' (i + 1) t)
       | tr' i a = if a aconv Bound i then raise Match else a;
@@ -466,7 +469,7 @@
 
 fun quote_antiquote_tr' quoteN antiquoteN name =
   let
-    fun tr' (t :: ts) = Term.list_comb (Lexicon.const quoteN $ quote_tr' antiquoteN t, ts)
+    fun tr' (t :: ts) = Term.list_comb (Syntax.const quoteN $ quote_tr' antiquoteN t, ts)
       | tr' _ = raise Match;
   in (name, tr') end;