src/Pure/Syntax/syntax_trans.ML
changeset 52143 36ffe23b25f8
parent 52043 286629271d65
child 52144 9065615d0360
equal deleted inserted replaced
52142:348aed032cda 52143:36ffe23b25f8
    17   val no_brackets: unit -> bool
    17   val no_brackets: unit -> bool
    18   val type_bracketsN: string
    18   val type_bracketsN: string
    19   val no_type_bracketsN: string
    19   val no_type_bracketsN: string
    20   val no_type_brackets: unit -> bool
    20   val no_type_brackets: unit -> bool
    21   val abs_tr: term list -> term
    21   val abs_tr: term list -> term
    22   val mk_binder_tr: string * string -> string * (term list -> term)
    22   val mk_binder_tr: string * string -> string * (Proof.context -> term list -> term)
    23   val antiquote_tr: string -> term -> term
    23   val antiquote_tr: string -> term -> term
    24   val quote_tr: string -> term -> term
    24   val quote_tr: string -> term -> term
    25   val quote_antiquote_tr: string -> string -> string -> string * (term list -> term)
    25   val quote_antiquote_tr: string -> string -> string ->
    26   val non_typed_tr': (term list -> term) -> typ -> term list -> term
    26     string * (Proof.context -> term list -> term)
    27   val non_typed_tr'': ('a -> term list -> term) -> 'a -> typ -> term list -> term
    27   val non_typed_tr': (Proof.context -> term list -> term) ->
       
    28     Proof.context -> typ -> term list -> term
    28   val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
    29   val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
    29   val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
    30   val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
    30   val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
    31   val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
    31   val eta_contract_raw: Config.raw
    32   val eta_contract_raw: Config.raw
    32   val mark_bound_abs: string * typ -> term
    33   val mark_bound_abs: string * typ -> term
    33   val mark_bound_body: string * typ -> term
    34   val mark_bound_body: string * typ -> term
    34   val bound_vars: (string * typ) list -> term -> term
    35   val bound_vars: (string * typ) list -> term -> term
    35   val abs_tr': Proof.context -> term -> term
    36   val abs_tr': Proof.context -> term -> term
    36   val atomic_abs_tr': string * typ * term -> term * term
    37   val atomic_abs_tr': string * typ * term -> term * term
    37   val const_abs_tr': term -> term
    38   val const_abs_tr': term -> term
    38   val mk_binder_tr': string * string -> string * (term list -> term)
    39   val mk_binder_tr': string * string -> string * (Proof.context -> term list -> term)
    39   val preserve_binder_abs_tr': string -> string -> string * (term list -> term)
    40   val preserve_binder_abs_tr': string -> string -> string * (Proof.context -> term list -> term)
    40   val preserve_binder_abs2_tr': string -> string -> string * (term list -> term)
    41   val preserve_binder_abs2_tr': string -> string -> string * (Proof.context -> term list -> term)
    41   val prop_tr': term -> term
    42   val prop_tr': term -> term
    42   val variant_abs: string * typ * term -> string * term
    43   val variant_abs: string * typ * term -> string * term
    43   val variant_abs': string * typ * term -> string * term
    44   val variant_abs': string * typ * term -> string * term
    44   val dependent_tr': string * string -> term list -> term
    45   val dependent_tr': string * string -> term list -> term
    45   val antiquote_tr': string -> term -> term
    46   val antiquote_tr': string -> term -> term
    46   val quote_tr': string -> term -> term
    47   val quote_tr': string -> term -> term
    47   val quote_antiquote_tr': string -> string -> string -> string * (term list -> term)
    48   val quote_antiquote_tr': string -> string -> string ->
       
    49     string * (Proof.context -> term list -> term)
    48   val update_name_tr': term -> term
    50   val update_name_tr': term -> term
    49   val pure_trfuns:
    51   val pure_parse_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list
    50     (string * (Ast.ast list -> Ast.ast)) list *
    52   val pure_parse_translation: (string * (Proof.context -> term list -> term)) list
    51     (string * (term list -> term)) list *
    53   val pure_print_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list
    52     (string * (term list -> term)) list *
    54   val struct_parse_translation: string list ->
    53     (string * (Ast.ast list -> Ast.ast)) list
    55     (string * (Proof.context -> term list -> term)) list
    54   val struct_trfuns: string list ->
    56   val struct_print_ast_translation: string list ->
    55     (string * (Ast.ast list -> Ast.ast)) list *
    57     (string * (Proof.context -> Ast.ast list -> Ast.ast)) list
    56     (string * (term list -> term)) list *
       
    57     (string * (typ -> term list -> term)) list *
       
    58     (string * (Ast.ast list -> Ast.ast)) list
       
    59 end;
    58 end;
    60 
    59 
    61 structure Syntax_Trans: SYNTAX_TRANS =
    60 structure Syntax_Trans: SYNTAX_TRANS =
    62 struct
    61 struct
    63 
    62 
   150     fun binder_tr [Const ("_idts", _) $ idt $ idts, t] = binder_tr [idt, binder_tr [idts, t]]
   149     fun binder_tr [Const ("_idts", _) $ idt $ idts, t] = binder_tr [idt, binder_tr [idts, t]]
   151       | binder_tr [x, t] =
   150       | binder_tr [x, t] =
   152           let val abs = abs_tr [x, t] handle TERM _ => err [x, t]
   151           let val abs = abs_tr [x, t] handle TERM _ => err [x, t]
   153           in Syntax.const name $ abs end
   152           in Syntax.const name $ abs end
   154       | binder_tr ts = err ts;
   153       | binder_tr ts = err ts;
   155   in (syn, binder_tr) end;
   154   in (syn, fn _ => binder_tr) end;
   156 
   155 
   157 
   156 
   158 (* type propositions *)
   157 (* type propositions *)
   159 
   158 
   160 fun mk_type ty =
   159 fun mk_type ty =
   212 
   211 
   213 fun quote_antiquote_tr quoteN antiquoteN name =
   212 fun quote_antiquote_tr quoteN antiquoteN name =
   214   let
   213   let
   215     fun tr [t] = Syntax.const name $ quote_tr antiquoteN t
   214     fun tr [t] = Syntax.const name $ quote_tr antiquoteN t
   216       | tr ts = raise TERM ("quote_tr", ts);
   215       | tr ts = raise TERM ("quote_tr", ts);
   217   in (quoteN, tr) end;
   216   in (quoteN, fn _ => tr) end;
   218 
   217 
   219 
   218 
   220 (* corresponding updates *)
   219 (* corresponding updates *)
   221 
   220 
   222 fun update_name_tr (Free (x, T) :: ts) = list_comb (Free (suffix "_update" x, T), ts)
   221 fun update_name_tr (Free (x, T) :: ts) = list_comb (Free (suffix "_update" x, T), ts)
   257 
   256 
   258 (** print (ast) translations **)
   257 (** print (ast) translations **)
   259 
   258 
   260 (* types *)
   259 (* types *)
   261 
   260 
   262 fun non_typed_tr' f _ ts = f ts;
   261 fun non_typed_tr' f ctxt _ ts = f ctxt ts;
   263 fun non_typed_tr'' f x _ ts = f x ts;
       
   264 
   262 
   265 
   263 
   266 (* type syntax *)
   264 (* type syntax *)
   267 
   265 
   268 fun tappl_ast_tr' (f, []) = raise Ast.AST ("tappl_ast_tr'", [f])
   266 fun tappl_ast_tr' (f, []) = raise Ast.AST ("tappl_ast_tr'", [f])
   364         val (xs, bd) = strip_abss (strip_qnt_vars name) (strip_qnt_body name) t;
   362         val (xs, bd) = strip_abss (strip_qnt_vars name) (strip_qnt_body name) t;
   365       in Syntax.const syn $ mk_idts xs $ bd end;
   363       in Syntax.const syn $ mk_idts xs $ bd end;
   366 
   364 
   367     fun binder_tr' (t :: ts) = Term.list_comb (tr' (Syntax.const name $ t), ts)
   365     fun binder_tr' (t :: ts) = Term.list_comb (tr' (Syntax.const name $ t), ts)
   368       | binder_tr' [] = raise Match;
   366       | binder_tr' [] = raise Match;
   369   in (name, binder_tr') end;
   367   in (name, fn _ => binder_tr') end;
   370 
   368 
   371 fun preserve_binder_abs_tr' name syn = (name, fn Abs abs :: ts =>
   369 fun preserve_binder_abs_tr' name syn = (name, fn _ => fn Abs abs :: ts =>
   372   let val (x, t) = atomic_abs_tr' abs
   370   let val (x, t) = atomic_abs_tr' abs
   373   in list_comb (Syntax.const syn $ x $ t, ts) end);
   371   in list_comb (Syntax.const syn $ x $ t, ts) end);
   374 
   372 
   375 fun preserve_binder_abs2_tr' name syn = (name, fn A :: Abs abs :: ts =>
   373 fun preserve_binder_abs2_tr' name syn = (name, fn _ => fn A :: Abs abs :: ts =>
   376   let val (x, t) = atomic_abs_tr' abs
   374   let val (x, t) = atomic_abs_tr' abs
   377   in list_comb (Syntax.const syn $ x $ A $ t, ts) end);
   375   in list_comb (Syntax.const syn $ x $ A $ t, ts) end);
   378 
   376 
   379 
   377 
   380 (* idtyp constraints *)
   378 (* idtyp constraints *)
   462 
   460 
   463 fun quote_antiquote_tr' quoteN antiquoteN name =
   461 fun quote_antiquote_tr' quoteN antiquoteN name =
   464   let
   462   let
   465     fun tr' (t :: ts) = Term.list_comb (Syntax.const quoteN $ quote_tr' antiquoteN t, ts)
   463     fun tr' (t :: ts) = Term.list_comb (Syntax.const quoteN $ quote_tr' antiquoteN t, ts)
   466       | tr' _ = raise Match;
   464       | tr' _ = raise Match;
   467   in (name, tr') end;
   465   in (name, fn _ => tr') end;
   468 
   466 
   469 
   467 
   470 (* corresponding updates *)
   468 (* corresponding updates *)
   471 
   469 
   472 local
   470 local
   501 
   499 
   502 
   500 
   503 
   501 
   504 (** Pure translations **)
   502 (** Pure translations **)
   505 
   503 
   506 val pure_trfuns =
   504 val pure_parse_ast_translation =
   507   ([("_strip_positions", strip_positions_ast_tr),
   505  [("_strip_positions", fn _ => strip_positions_ast_tr),
   508     ("_constify", constify_ast_tr),
   506   ("_constify", fn _ => constify_ast_tr),
   509     ("_tapp", tapp_ast_tr),
   507   ("_tapp", fn _ => tapp_ast_tr),
   510     ("_tappl", tappl_ast_tr),
   508   ("_tappl", fn _ => tappl_ast_tr),
   511     ("_bracket", bracket_ast_tr),
   509   ("_bracket", fn _ => bracket_ast_tr),
   512     ("_appl", appl_ast_tr),
   510   ("_appl", fn _ => appl_ast_tr),
   513     ("_applC", applC_ast_tr),
   511   ("_applC", fn _ => applC_ast_tr),
   514     ("_lambda", lambda_ast_tr),
   512   ("_lambda", fn _ => lambda_ast_tr),
   515     ("_idtyp", idtyp_ast_tr),
   513   ("_idtyp", fn _ => idtyp_ast_tr),
   516     ("_idtypdummy", idtypdummy_ast_tr),
   514   ("_idtypdummy", fn _ => idtypdummy_ast_tr),
   517     ("_bigimpl", bigimpl_ast_tr),
   515   ("_bigimpl", fn _ => bigimpl_ast_tr),
   518     ("_indexdefault", indexdefault_ast_tr),
   516   ("_indexdefault", fn _ => indexdefault_ast_tr),
   519     ("_indexvar", indexvar_ast_tr),
   517   ("_indexvar", fn _ => indexvar_ast_tr),
   520     ("_struct", struct_ast_tr)],
   518   ("_struct", fn _ => struct_ast_tr)];
   521    [("_abs", abs_tr),
   519 
   522     ("_aprop", aprop_tr),
   520 val pure_parse_translation =
   523     ("_ofclass", ofclass_tr),
   521  [("_abs", fn _ => abs_tr),
   524     ("_sort_constraint", sort_constraint_tr),
   522   ("_aprop", fn _ => aprop_tr),
   525     ("_TYPE", type_tr),
   523   ("_ofclass", fn _ => ofclass_tr),
   526     ("_DDDOT", dddot_tr),
   524   ("_sort_constraint", fn _ => sort_constraint_tr),
   527     ("_update_name", update_name_tr),
   525   ("_TYPE", fn _ => type_tr),
   528     ("_index", index_tr)],
   526   ("_DDDOT", fn _ => dddot_tr),
   529    ([]: (string * (term list -> term)) list),
   527   ("_update_name", fn _ => update_name_tr),
   530    [("\\<^type>fun", fun_ast_tr'),
   528   ("_index", fn _ => index_tr)];
   531     ("_abs", abs_ast_tr'),
   529 
   532     ("_idts", idtyp_ast_tr' "_idts"),
   530 val pure_print_ast_translation =
   533     ("_pttrns", idtyp_ast_tr' "_pttrns"),
   531  [("\\<^type>fun", fn _ => fun_ast_tr'),
   534     ("\\<^const>==>", impl_ast_tr'),
   532   ("_abs", fn _ => abs_ast_tr'),
   535     ("_index", index_ast_tr')]);
   533   ("_idts", fn _ => idtyp_ast_tr' "_idts"),
   536 
   534   ("_pttrns", fn _ => idtyp_ast_tr' "_pttrns"),
   537 fun struct_trfuns structs =
   535   ("\\<^const>==>", fn _ => impl_ast_tr'),
   538   ([], [("_struct", struct_tr structs)], [], [("_struct", struct_ast_tr' structs)]);
   536   ("_index", fn _ => index_ast_tr')];
       
   537 
       
   538 fun struct_parse_translation structs = [("_struct", fn _ => struct_tr structs)];
       
   539 fun struct_print_ast_translation structs = [("_struct", fn _ => struct_ast_tr' structs)];
   539 
   540 
   540 end;
   541 end;
   541 
   542 
   542 structure Basic_Syntax_Trans: BASIC_SYNTAX_TRANS = Syntax_Trans;
   543 structure Basic_Syntax_Trans: BASIC_SYNTAX_TRANS = Syntax_Trans;
   543 open Basic_Syntax_Trans;
   544 open Basic_Syntax_Trans;