improved indexed syntax / implicit structures;
authorwenzelm
Sat May 01 22:10:37 2004 +0200 (2004-05-01)
changeset 146975ad13d05049b
parent 14696 e862cc138e9c
child 14698 7e4dec3fd515
improved indexed syntax / implicit structures;
src/Pure/Isar/proof_context.ML
src/Pure/Syntax/mixfix.ML
src/Pure/Syntax/syn_ext.ML
src/Pure/Syntax/syn_trans.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Sat May 01 22:09:45 2004 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Sat May 01 22:10:37 2004 +0200
     1.3 @@ -157,19 +157,18 @@
     1.4      data: Object.T Symtab.table,                              (*user data*)
     1.5      asms:
     1.6        ((cterm list * exporter) list *                         (*assumes: A ==> _*)
     1.7 -        (string * thm list) list) *
     1.8 +        (string * thm list) list) *                           (*prems: A |- A *)
     1.9        (string * string) list,                                 (*fixes: !!x. _*)
    1.10 -    (* CB: asms is of the form ((asms, prems), fixed) *)
    1.11      binds: (term * typ) option Vartab.table,                  (*term bindings*)
    1.12      thms: bool * NameSpace.T * thm list option Symtab.table
    1.13        * FactIndex.T,                                          (*local thms*)
    1.14 -    (* CB: thms is of the form (q, n, t, i) where
    1.15 +    (*thms is of the form (q, n, t, i) where
    1.16         q: indicates whether theorems with qualified names may be stored;
    1.17            this is initially forbidden (false); flag may be changed with
    1.18            qualified and restore_qualified;
    1.19         n: theorem namespace;
    1.20         t: table of theorems;
    1.21 -       i: index for theorem lookup (find theorem command) *) 
    1.22 +       i: index for theorem lookup (cf. thms_containing) *)
    1.23      cases: (string * RuleCases.T) list,                       (*local contexts*)
    1.24      defs:
    1.25        typ Vartab.table *                                      (*type constraints*)
    1.26 @@ -304,31 +303,11 @@
    1.27  val fixedN = "\\<^fixed>";
    1.28  val structN = "\\<^struct>";
    1.29  
    1.30 -fun the_struct structs i =
    1.31 -  if 1 <= i andalso i <= length structs then Library.nth_elem (i - 1, structs)
    1.32 -  else raise ERROR_MESSAGE ("Illegal reference to implicit structure #" ^ string_of_int i);
    1.33  
    1.34 -
    1.35 -(* parse translations *)
    1.36 +(* translation functions *)
    1.37  
    1.38  fun fixed_tr x = (fixedN ^ x, curry Term.list_comb (Syntax.free x));
    1.39  
    1.40 -fun index_tr struct_ (Const ("_noindex", _)) = Syntax.free (struct_ 1)
    1.41 -  | index_tr struct_ (t as (Const ("_index", _) $ Const (s, _))) =
    1.42 -      Syntax.free (struct_
    1.43 -        (case Syntax.read_nat s of Some n => n | None => raise TERM ("index_tr", [t])))
    1.44 -  | index_tr _ (Const ("_indexlogic", _) $ t) = t
    1.45 -  | index_tr _ t = raise TERM ("index_tr", [t]);
    1.46 -
    1.47 -fun struct_tr structs [idx] = index_tr (the_struct structs) idx
    1.48 -  | struct_tr _ ts = raise TERM ("struct_tr", ts);
    1.49 -
    1.50 -
    1.51 -(* print (ast) translations *)
    1.52 -
    1.53 -fun index_tr' 1 = Syntax.const "_noindex"
    1.54 -  | index_tr' i = Syntax.const "_index" $ Syntax.const (Library.string_of_int i);
    1.55 -
    1.56  fun context_tr' ctxt =
    1.57    let
    1.58      val (_, structs, mixfixed) = syntax_of ctxt;
    1.59 @@ -336,25 +315,14 @@
    1.60      fun tr' (t $ u) = tr' t $ tr' u
    1.61        | tr' (Abs (x, T, t)) = Abs (x, T, tr' t)
    1.62        | tr' (t as Free (x, T)) =
    1.63 -          let val i = Library.find_index (equal x) structs + 1 in
    1.64 -            if 1 <= i andalso i <= 9 then Syntax.const "_struct" $ index_tr' i
    1.65 -            else if x mem_string mixfixed then Const (fixedN ^ x, T)
    1.66 +          let val i = Library.find_index_eq x structs + 1 in
    1.67 +            if i = 0 andalso x mem_string mixfixed then Const (fixedN ^ x, T)
    1.68 +            else if i = 1 then Syntax.const "_struct" $ Syntax.const "_indexdefault"
    1.69              else t
    1.70            end
    1.71        | tr' a = a;
    1.72    in tr' end;
    1.73  
    1.74 -fun index_ast_tr' structs s =
    1.75 -  (case Syntax.read_nat s of
    1.76 -    Some i => Syntax.Variable (the_struct structs i handle ERROR_MESSAGE _ => raise Match)
    1.77 -  | None => raise Match);
    1.78 -
    1.79 -fun struct_ast_tr' structs [Syntax.Constant "_noindex"] =
    1.80 -      index_ast_tr' structs "1"
    1.81 -  | struct_ast_tr' structs [Syntax.Appl [Syntax.Constant "_index", Syntax.Constant s]] =
    1.82 -      index_ast_tr' structs s
    1.83 -  | struct_ast_tr' _ _ = raise Match;
    1.84 -
    1.85  
    1.86  (* add syntax *)
    1.87  
    1.88 @@ -391,8 +359,8 @@
    1.89      in (thy, (syn', structs', fixed @ mixfixed), data, asms, binds, thms, cases, defs) end)
    1.90  
    1.91  fun syn_of (Context {syntax = (syn, structs, _), ...}) =
    1.92 -  syn |> Syntax.extend_trfuns
    1.93 -    ([], [("_struct", struct_tr structs)], [], [("_struct", struct_ast_tr' structs)]);
    1.94 +  syn |> Syntax.extend_trfuns (Syntax.struct_trfuns structs);
    1.95 +
    1.96  
    1.97  end;
    1.98  
    1.99 @@ -459,8 +427,8 @@
   1.100            (case env (x, ~1) of
   1.101                Some _ => t
   1.102              | None => (case lookup_skolem ctxt (no_skolem false ctxt x) of
   1.103 -		  Some x' => Free (x', T)
   1.104 -		| None => t))
   1.105 +                  Some x' => Free (x', T)
   1.106 +                | None => t))
   1.107        | intern (t $ u) = intern t $ intern u
   1.108        | intern (Abs (x, T, t)) = Abs (x, T, intern t)
   1.109        | intern a = a;
   1.110 @@ -592,13 +560,13 @@
   1.111                    | Some (_, _, used'') => used @ used'';
   1.112    in
   1.113      (transform_error (read (syn_of ctxt)
   1.114 -	(sign_of ctxt) (types', sorts', used')) s
   1.115 +        (sign_of ctxt) (types', sorts', used')) s
   1.116        handle TERM (msg, _) => raise CONTEXT (msg, ctxt)
   1.117        | ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt))
   1.118      |> app (intern_skolem ctxt (case env_opt of None => K None | Some (env, _, _) => env))
   1.119      |> app (if is_pat then I else norm_term ctxt schematic allow_vars)
   1.120      |> app (if is_pat then prepare_dummies
   1.121 -	 else if dummies then I else reject_dummies ctxt)
   1.122 +         else if dummies then I else reject_dummies ctxt)
   1.123    end
   1.124  in
   1.125  
     2.1 --- a/src/Pure/Syntax/mixfix.ML	Sat May 01 22:09:45 2004 +0200
     2.2 +++ b/src/Pure/Syntax/mixfix.ML	Sat May 01 22:10:37 2004 +0200
     2.3 @@ -239,10 +239,10 @@
     2.4    ("",            "var => logic",              Delimfix "_"),
     2.5    ("_DDDOT",      "logic",                     Delimfix "..."),
     2.6    ("_constify",   "num => num_const",          Delimfix "_"),
     2.7 -  ("_index",      "num_const => index",        Delimfix "\\<^sub>_"),
     2.8 -  ("_indexlogic", "logic => index",            Delimfix "\\<^bsub>_\\<^esub>"),
     2.9 +  ("_indexnum",   "num_const => index",        Delimfix "\\<^sub>_"),
    2.10 +  ("_index",      "logic => index",            Delimfix "\\<^bsub>_\\<^esub>"),
    2.11 +  ("_indexdefault", "index",                   Delimfix ""),
    2.12    ("_indexvar",   "index",                     Delimfix "'\\<index>"),
    2.13 -  ("_noindex",    "index",                     Delimfix ""),
    2.14    ("_struct",     "index => logic",            Mixfix ("\\<struct>_", [1000], 1000))];
    2.15  
    2.16  val pure_syntax_output =
     3.1 --- a/src/Pure/Syntax/syn_ext.ML	Sat May 01 22:09:45 2004 +0200
     3.2 +++ b/src/Pure/Syntax/syn_ext.ML	Sat May 01 22:10:37 2004 +0200
     3.3 @@ -267,17 +267,18 @@
     3.4        if not (exists is_index args) then (const, typ, [])
     3.5        else
     3.6          let
     3.7 -          val c = if const <> "" then "_indexed_" ^ const
     3.8 +          val indexed_const = if const <> "" then "_indexed_" ^ const
     3.9              else err_in_mfix "Missing constant name for indexed syntax" mfix;
    3.10 -          val T = Term.range_type typ handle Match =>
    3.11 +          val rangeT = Term.range_type typ handle Match =>
    3.12              err_in_mfix "Missing structure argument for indexed syntax" mfix;
    3.13  
    3.14 -          val xs = map Ast.Variable (Term.invent_names [] "x" (length args - 1));
    3.15 +          val xs = map Ast.Variable (Term.invent_names [] "xa" (length args - 1));
    3.16 +          val (xs1, xs2) = Library.splitAt (Library.find_index is_index args, xs);
    3.17            val i = Ast.Variable "i";
    3.18 -          val n = Library.find_index is_index args;
    3.19 -          val lhs = Ast.mk_appl (Ast.Constant c) (take (n, xs) @ [i] @ drop (n, xs));
    3.20 -          val rhs = Ast.mk_appl (Ast.Constant const) (Ast.Appl [Ast.Constant "_struct", i] :: xs);
    3.21 -        in (c, T, [(lhs, rhs)]) end;
    3.22 +          val lhs = Ast.mk_appl (Ast.Constant indexed_const)
    3.23 +            (xs1 @ [Ast.mk_appl (Ast.Constant "_index") [i]] @ xs2);
    3.24 +          val rhs = Ast.mk_appl (Ast.Constant const) (i :: xs);
    3.25 +        in (indexed_const, rangeT, [(lhs, rhs)]) end;
    3.26  
    3.27      val (symbs, lhs) = add_args raw_symbs typ' pris;
    3.28  
     4.1 --- a/src/Pure/Syntax/syn_trans.ML	Sat May 01 22:09:45 2004 +0200
     4.2 +++ b/src/Pure/Syntax/syn_trans.ML	Sat May 01 22:10:37 2004 +0200
     4.3 @@ -36,6 +36,11 @@
     4.4        (string * (term list -> term)) list *
     4.5        (string * (Ast.ast list -> Ast.ast)) list
     4.6    val pure_trfunsT: (string * (bool -> typ -> term list -> term)) list
     4.7 +  val struct_trfuns: string list ->
     4.8 +      (string * (Ast.ast list -> Ast.ast)) list *
     4.9 +      (string * (term list -> term)) list *
    4.10 +      (string * (bool -> typ -> term list -> term)) list *
    4.11 +      (string * (Ast.ast list -> Ast.ast)) list
    4.12  end;
    4.13  
    4.14  signature SYN_TRANS =
    4.15 @@ -165,10 +170,43 @@
    4.16    in (quoteN, tr) end;
    4.17  
    4.18  
    4.19 -(* index variable *)
    4.20 +(* indexed syntax *)
    4.21 +
    4.22 +fun struct_ast_tr (*"_struct"*) [Ast.Appl [Ast.Constant "_index", ast]] = ast
    4.23 +  | struct_ast_tr (*"_struct"*) asts = Ast.mk_appl (Ast.Constant "_struct") asts;
    4.24 +
    4.25 +fun index_ast_tr ast =
    4.26 +  Ast.mk_appl (Ast.Constant "_index") [Ast.mk_appl (Ast.Constant "_struct") [ast]];
    4.27 +
    4.28 +fun indexdefault_ast_tr (*"_indexdefault"*) [] =
    4.29 +      index_ast_tr (Ast.Constant "_indexdefault")
    4.30 +  | indexdefault_ast_tr (*"_indexdefault"*) asts =
    4.31 +      raise Ast.AST ("indexdefault_ast_tr", asts);
    4.32 +
    4.33 +fun indexnum_ast_tr (*"_indexnum"*) [ast] =
    4.34 +      index_ast_tr (Ast.mk_appl (Ast.Constant "_indexnum") [ast])
    4.35 +  | indexnum_ast_tr (*"_indexnum"*) asts = raise Ast.AST ("indexnum_ast_tr", asts);
    4.36  
    4.37 -fun indexvar_ast_tr [] = Ast.Variable "some_index"
    4.38 -  | indexvar_ast_tr asts = raise Ast.AST ("indexvar_ast_tr", asts);
    4.39 +fun indexvar_ast_tr (*"_indexvar"*) [] =
    4.40 +      Ast.mk_appl (Ast.Constant "_index") [Ast.Variable "some_index"]
    4.41 +  | indexvar_ast_tr (*"_indexvar"*) asts = raise Ast.AST ("indexvar_ast_tr", asts);
    4.42 +
    4.43 +fun index_tr (*"_index"*) [t] = t
    4.44 +  | index_tr (*"_index"*) ts = raise TERM ("index_tr", ts);
    4.45 +
    4.46 +
    4.47 +(* implicit structures *)
    4.48 +
    4.49 +fun the_struct structs i =
    4.50 +  if 1 <= i andalso i <= length structs then Library.nth_elem (i - 1, structs)
    4.51 +  else raise ERROR_MESSAGE ("Illegal reference to implicit structure #" ^ string_of_int i);
    4.52 +
    4.53 +fun struct_tr structs (*"_struct"*) [Const ("_indexdefault", _)] =
    4.54 +      Lexicon.free (the_struct structs 1)
    4.55 +  | struct_tr structs (*"_struct"*) [t as (Const ("_indexnum", _) $ Const (s, _))] =
    4.56 +      Lexicon.free (the_struct structs
    4.57 +        (case Lexicon.read_nat s of Some n => n | None => raise TERM ("struct_tr", [t])))
    4.58 +  | struct_tr _ (*"_struct"*) ts = raise TERM ("struct_tr", ts);
    4.59  
    4.60  
    4.61  
    4.62 @@ -233,10 +271,9 @@
    4.63    foldr (fn (x, t) => Lexicon.const "_abs" $ x $ t)
    4.64      (strip_abss strip_abs_vars strip_abs_body (eta_contr tm));
    4.65  
    4.66 -
    4.67 -fun atomic_abs_tr' (x,T,t) = 
    4.68 -  let val [xT] = rename_wrt_term t [(x,T)];
    4.69 -  in  (mark_boundT xT, subst_bound (mark_bound(fst xT), t)) end;
    4.70 +fun atomic_abs_tr' (x, T, t) =
    4.71 +  let val [xT] = rename_wrt_term t [(x, T)]
    4.72 +  in (mark_boundT xT, subst_bound (mark_bound (fst xT), t)) end;
    4.73  
    4.74  fun abs_ast_tr' (*"_abs"*) asts =
    4.75    (case Ast.unfold_ast_p "_abs" (Ast.Appl (Ast.Constant "_abs" :: asts)) of
    4.76 @@ -370,22 +407,49 @@
    4.77    in (name, tr') end;
    4.78  
    4.79  
    4.80 +(* indexed syntax *)
    4.81  
    4.82 -(** pure_trfuns **)
    4.83 +fun index_ast_tr' (*"_index"*) [Ast.Appl [Ast.Constant "_struct", ast]] = ast
    4.84 +  | index_ast_tr' _ = raise Match;
    4.85 +
    4.86 +
    4.87 +(* implicit structures *)
    4.88 +
    4.89 +fun the_struct' structs s =
    4.90 +  [(case Lexicon.read_nat s of
    4.91 +    Some i => Ast.Variable (the_struct structs i handle ERROR_MESSAGE _ => raise Match)
    4.92 +  | None => raise Match)] |> Ast.mk_appl (Ast.Constant "_free");
    4.93 +;
    4.94 +
    4.95 +fun struct_ast_tr' structs (*"_struct"*) [Ast.Constant "_indexdefault"] =
    4.96 +      the_struct' structs "1"
    4.97 +  | struct_ast_tr' structs (*"_struct"*) [Ast.Appl [Ast.Constant "_indexnum", Ast.Constant s]] =
    4.98 +      the_struct' structs s
    4.99 +  | struct_ast_tr' _ _ = raise Match;
   4.100 +
   4.101 +
   4.102 +
   4.103 +(** Pure translations **)
   4.104  
   4.105  val pure_trfuns =
   4.106   ([("_constify", constify_ast_tr), ("_appl", appl_ast_tr), ("_applC", applC_ast_tr),
   4.107     ("_lambda", lambda_ast_tr), ("_idtyp", idtyp_ast_tr), ("_bigimpl", bigimpl_ast_tr),
   4.108 -   ("_indexvar", indexvar_ast_tr)],
   4.109 +   ("_indexdefault", indexdefault_ast_tr), ("_indexnum", indexnum_ast_tr),
   4.110 +   ("_indexvar", indexvar_ast_tr), ("_struct", struct_ast_tr)],
   4.111    [("_abs", abs_tr), ("_aprop", aprop_tr), ("_ofclass", ofclass_tr),
   4.112 -   ("_TYPE", type_tr), ("_DDDOT", dddot_tr), ("_K", k_tr)],
   4.113 +   ("_TYPE", type_tr), ("_DDDOT", dddot_tr), ("_K", k_tr),
   4.114 +   ("_index", index_tr)],
   4.115    [("all", meta_conjunction_tr')],
   4.116    [("_abs", abs_ast_tr'), ("_idts", idtyp_ast_tr' "_idts"),
   4.117 -   ("_pttrns", idtyp_ast_tr' "_pttrns"), ("==>", impl_ast_tr')]);
   4.118 +   ("_pttrns", idtyp_ast_tr' "_pttrns"), ("==>", impl_ast_tr'),
   4.119 +   ("_index", index_ast_tr')]);
   4.120  
   4.121  val pure_trfunsT =
   4.122    [("_mk_ofclass", mk_ofclass_tr'), ("TYPE", type_tr')];
   4.123  
   4.124 +fun struct_trfuns structs =
   4.125 +  ([], [("_struct", struct_tr structs)], [], [("_struct", struct_ast_tr' structs)]);
   4.126 +
   4.127  
   4.128  
   4.129  (** pt_to_ast **)