adapted pure_trfunsT;
authorwenzelm
Wed Nov 05 11:43:37 1997 +0100 (1997-11-05)
changeset 4148e0e5a2820ac1
parent 4147 e57d03a5fc73
child 4149 a6ccec4fd0c3
adapted pure_trfunsT;
added type_tr/tr';
eliminated mk_ofclassS_tr';
src/Pure/Syntax/syn_trans.ML
     1.1 --- a/src/Pure/Syntax/syn_trans.ML	Wed Nov 05 11:42:19 1997 +0100
     1.2 +++ b/src/Pure/Syntax/syn_trans.ML	Wed Nov 05 11:43:37 1997 +0100
     1.3 @@ -25,14 +25,14 @@
     1.4        (string * (term list -> term)) list *
     1.5        (string * (term list -> term)) list *
     1.6        (string * (Ast.ast list -> Ast.ast)) list
     1.7 -  val pure_trfunsT: (string * (typ -> term list -> term)) list
     1.8 +  val pure_trfunsT: (string * (bool -> typ -> term list -> term)) list
     1.9  end;
    1.10  
    1.11  signature SYN_TRANS =
    1.12  sig
    1.13    include SYN_TRANS1
    1.14    val abs_tr': term -> term
    1.15 -  val prop_tr': bool -> term -> term
    1.16 +  val prop_tr': term -> term
    1.17    val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
    1.18    val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
    1.19    val pt_to_ast: (string -> (Ast.ast list -> Ast.ast) option) -> Parser.parsetree -> Ast.ast
    1.20 @@ -117,6 +117,12 @@
    1.21    | bigimpl_ast_tr (*"_bigimpl"*) asts = raise AST ("bigimpl_ast_tr", asts);
    1.22  
    1.23  
    1.24 +(* type reflection *)
    1.25 +
    1.26 +fun type_tr (*"_TYPE"*) [ty] =
    1.27 +      const constrainC $ const "TYPE" $ (const "itself" $ ty)
    1.28 +  | type_tr (*"_TYPE"*) ts = raise TERM ("type_tr", ts);
    1.29 +
    1.30  
    1.31  (** print (ast) translations **)
    1.32  
    1.33 @@ -215,10 +221,9 @@
    1.34  
    1.35  (* meta propositions *)
    1.36  
    1.37 -fun prop_tr' show_sorts tm =
    1.38 +fun prop_tr' tm =
    1.39    let
    1.40      fun aprop t = const "_aprop" $ t;
    1.41 -    val mk_ofclass = if show_sorts then "_mk_ofclassS" else "_mk_ofclass";
    1.42  
    1.43      fun is_prop Ts t =
    1.44        fastype_of1 (Ts, t) = propT handle TERM _ => false;
    1.45 @@ -232,7 +237,7 @@
    1.46            if is_prop Ts t then aprop t else t
    1.47        | tr' Ts (Abs (x, T, t)) = Abs (x, T, tr' (T :: Ts) t)
    1.48        | tr' Ts (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [T])))) =
    1.49 -          if is_prop Ts t then Const (mk_ofclass, T) $ tr' Ts t1
    1.50 +          if is_prop Ts t then Const ("_mk_ofclass", T) $ tr' Ts t1
    1.51            else tr' Ts t1 $ tr' Ts t2
    1.52        | tr' Ts (t as t1 $ t2) =
    1.53            (if is_Const (head_of t) orelse not (is_prop Ts t)
    1.54 @@ -241,14 +246,9 @@
    1.55      tr' [] tm
    1.56    end;
    1.57  
    1.58 -
    1.59 -fun mk_ofclass_tr' (*"_mk_ofclass"*) T [t] =
    1.60 -      const "_ofclass" $ term_of_typ false T $ t
    1.61 -  | mk_ofclass_tr' (*"_mk_ofclass"*) T ts = raise TYPE ("mk_ofclass_tr'", [T], ts);
    1.62 -
    1.63 -fun mk_ofclassS_tr' (*"_mk_ofclassS"*) T [t] =
    1.64 -      const "_ofclass" $ term_of_typ true T $ t
    1.65 -  | mk_ofclassS_tr' (*"_mk_ofclassS"*) T ts = raise TYPE ("mk_ofclassS_tr'", [T], ts);
    1.66 +fun mk_ofclass_tr' show_sorts (*"_mk_ofclass"*) T [t] =
    1.67 +      const "_ofclass" $ term_of_typ show_sorts T $ t
    1.68 +  | mk_ofclass_tr' _ (*"_mk_ofclass"*) T ts = raise TYPE ("mk_ofclass_tr'", [T], ts);
    1.69  
    1.70  
    1.71  (* meta implication *)
    1.72 @@ -260,6 +260,13 @@
    1.73    | _ => raise Match);
    1.74  
    1.75  
    1.76 +(* type reflection *)
    1.77 +
    1.78 +fun type_tr' show_sorts (*"TYPE"*) (Type ("itself", [T])) ts =
    1.79 +      list_comb (const "_TYPE" $ term_of_typ show_sorts T, ts)
    1.80 +  | type_tr' _ _ _ = raise Match;
    1.81 +
    1.82 +
    1.83  (* dependent / nondependent quantifiers *)
    1.84  
    1.85  fun variant_abs' (x, T, B) =
    1.86 @@ -283,13 +290,13 @@
    1.87     ("_lambda", lambda_ast_tr), ("_idtyp", idtyp_ast_tr),
    1.88     ("_bigimpl", bigimpl_ast_tr)],
    1.89    [("_abs", abs_tr), ("_aprop", aprop_tr), ("_ofclass", ofclass_tr),
    1.90 -   ("_K", k_tr)],
    1.91 +   ("_TYPE", type_tr), ("_K", k_tr)],
    1.92    []: (string * (term list -> term)) list,
    1.93    [("_abs", abs_ast_tr'), ("_idts", idtyp_ast_tr' "_idts"),
    1.94     ("_pttrns", idtyp_ast_tr' "_pttrns"), ("==>", impl_ast_tr')]);
    1.95  
    1.96  val pure_trfunsT =
    1.97 -  [("_mk_ofclass", mk_ofclass_tr'), ("_mk_ofclassS", mk_ofclassS_tr')];
    1.98 +  [("_mk_ofclass", mk_ofclass_tr'), ("TYPE", type_tr')];
    1.99  
   1.100  
   1.101