testboard: src/Pure/Syntax/syntax

     1 (*  Title:      Pure/Syntax/syntax_trans.ML

     2     Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen

     4 Syntax translation functions.

     5 *)

     7 signature BASIC_SYNTAX_TRANS =

     8 sig

     9   val eta_contract: bool Config.T

    10 end

    12 signature SYNTAX_TRANS =

    13 sig

    14   include BASIC_SYNTAX_TRANS

    15   val bracketsN: string

    16   val no_bracketsN: string

    17   val no_brackets: unit -> bool

    18   val type_bracketsN: string

    19   val no_type_bracketsN: string

    20   val no_type_brackets: unit -> bool

    21   val abs_tr: term list -> term

    22   val mk_binder_tr: string * string -> string * (term list -> term)

    23   val antiquote_tr: string -> term -> term

    24   val quote_tr: string -> term -> term

    25   val quote_antiquote_tr: string -> string -> string -> string * (term list -> term)

    26   val non_typed_tr': (term list -> term) -> typ -> term list -> term

    27   val non_typed_tr'': ('a -> term list -> term) -> 'a -> typ -> term list -> term

    28   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 applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast

    31   val eta_contract_default: bool Unsynchronized.ref

    32   val eta_contract_raw: Config.raw

    33   val mark_bound_abs: string * typ -> term

    34   val mark_bound_body: string * typ -> term

    35   val bound_vars: (string * typ) list -> term -> term

    36   val abs_tr': Proof.context -> term -> term

    37   val atomic_abs_tr': string * typ * term -> term * term

    38   val const_abs_tr': term -> term

    39   val mk_binder_tr': string * string -> string * (term list -> term)

    40   val preserve_binder_abs_tr': string -> string -> string * (term list -> term)

    41   val preserve_binder_abs2_tr': string -> string -> string * (term list -> term)

    42   val prop_tr': term -> term

    43   val variant_abs: string * typ * term -> string * term

    44   val variant_abs': string * typ * term -> string * term

    45   val dependent_tr': string * string -> term list -> term

    46   val antiquote_tr': string -> term -> term

    47   val quote_tr': string -> term -> term

    48   val quote_antiquote_tr': string -> string -> string -> string * (term list -> term)

    49   val update_name_tr': term -> term

    50   val pure_trfuns:

    51     (string * (Ast.ast list -> Ast.ast)) list *

    52     (string * (term list -> term)) list *

    53     (string * (term list -> term)) list *

    54     (string * (Ast.ast list -> Ast.ast)) list

    55   val struct_trfuns: string list ->

    56     (string * (Ast.ast list -> Ast.ast)) list *

    57     (string * (term list -> term)) list *

    58     (string * (typ -> term list -> term)) list *

    59     (string * (Ast.ast list -> Ast.ast)) list

    60 end;

    62 structure Syntax_Trans: SYNTAX_TRANS =

    63 struct

    65 structure Syntax = Lexicon.Syntax;

    68 (* print mode *)

    70 val bracketsN = "brackets";

    71 val no_bracketsN = "no_brackets";

    73 fun no_brackets () =

    74   find_first (fn mode => mode = bracketsN orelse mode = no_bracketsN)

    75     (print_mode_value ()) = SOME no_bracketsN;

    77 val type_bracketsN = "type_brackets";

    78 val no_type_bracketsN = "no_type_brackets";

    80 fun no_type_brackets () =

    81   find_first (fn mode => mode = type_bracketsN orelse mode = no_type_bracketsN)

    82     (print_mode_value ()) <> SOME type_bracketsN;

    86 (** parse (ast) translations **)

    88 (* strip_positions *)

    90 fun strip_positions_ast_tr [ast] = Ast.strip_positions ast

    91   | strip_positions_ast_tr asts = raise Ast.AST ("strip_positions_ast_tr", asts);

    94 (* constify *)

    96 fun constify_ast_tr [Ast.Appl [c as Ast.Constant "_constrain", ast1, ast2]] =

    97       Ast.Appl [c, constify_ast_tr [ast1], ast2]

    98   | constify_ast_tr [Ast.Variable c] = Ast.Constant c

    99   | constify_ast_tr asts = raise Ast.AST ("constify_ast_tr", asts);

   102 (* type syntax *)

   104 fun tapp_ast_tr [ty, c] = Ast.Appl [c, ty]

   105   | tapp_ast_tr asts = raise Ast.AST ("tapp_ast_tr", asts);

   107 fun tappl_ast_tr [ty, tys, c] = Ast.mk_appl c (ty :: Ast.unfold_ast "_types" tys)

   108   | tappl_ast_tr asts = raise Ast.AST ("tappl_ast_tr", asts);

   110 fun bracket_ast_tr [dom, cod] = Ast.fold_ast_p "\\<^type>fun" (Ast.unfold_ast "_types" dom, cod)

   111   | bracket_ast_tr asts = raise Ast.AST ("bracket_ast_tr", asts);

   114 (* application *)

   116 fun appl_ast_tr [f, args] = Ast.Appl (f :: Ast.unfold_ast "_args" args)

   117   | appl_ast_tr asts = raise Ast.AST ("appl_ast_tr", asts);

   119 fun applC_ast_tr [f, args] = Ast.Appl (f :: Ast.unfold_ast "_cargs" args)

   120   | applC_ast_tr asts = raise Ast.AST ("applC_ast_tr", asts);

   123 (* abstraction *)

   125 fun idtyp_ast_tr [x, ty] = Ast.Appl [Ast.Constant "_constrain", x, ty]

   126   | idtyp_ast_tr asts = raise Ast.AST ("idtyp_ast_tr", asts);

   128 fun idtypdummy_ast_tr [ty] = Ast.Appl [Ast.Constant "_constrain", Ast.Constant "_idtdummy", ty]

   129   | idtypdummy_ast_tr asts = raise Ast.AST ("idtyp_ast_tr", asts);

   131 fun lambda_ast_tr [pats, body] = Ast.fold_ast_p "_abs" (Ast.unfold_ast "_pttrns" pats, body)

   132   | lambda_ast_tr asts = raise Ast.AST ("lambda_ast_tr", asts);

   134 fun absfree_proper (x, T) t =

   135   if can Name.dest_internal x

   136   then error ("Illegal internal variable in abstraction: " ^ quote x)

   137   else absfree (x, T) t;

   139 fun abs_tr [Free x, t] = absfree_proper x t

   140   | abs_tr [Const ("_idtdummy", T), t] = absdummy T t

   141   | abs_tr [Const ("_constrain", _) $ x $ tT, t] =

   142       Syntax.const "_constrainAbs" $ abs_tr [x, t] $ tT

   143   | abs_tr ts = raise TERM ("abs_tr", ts);

   146 (* binder *)

   148 fun mk_binder_tr (syn, name) =

   149   let

   150     fun err ts = raise TERM ("binder_tr: " ^ syn, ts)

   151     fun binder_tr [Const ("_idts", _) $ idt $ idts, t] = binder_tr [idt, binder_tr [idts, t]]

   152       | binder_tr [x, t] =

   153           let val abs = abs_tr [x, t] handle TERM _ => err [x, t]

   154           in Syntax.const name $ abs end

   155       | binder_tr ts = err ts;

   156   in (syn, binder_tr) end;

   159 (* type propositions *)

   161 fun mk_type ty =

   162   Syntax.const "_constrain" $

   163     Syntax.const "\\<^const>TYPE" $ (Syntax.const "\\<^type>itself" $ ty);

   165 fun ofclass_tr [ty, cls] = cls $ mk_type ty

   166   | ofclass_tr ts = raise TERM ("ofclass_tr", ts);

   168 fun sort_constraint_tr [ty] = Syntax.const "\\<^const>Pure.sort_constraint" $ mk_type ty

   169   | sort_constraint_tr ts = raise TERM ("sort_constraint_tr", ts);

   172 (* meta propositions *)

   174 fun aprop_tr [t] = Syntax.const "_constrain" $ t $ Syntax.const "\\<^type>prop"

   175   | aprop_tr ts = raise TERM ("aprop_tr", ts);

   178 (* meta implication *)

   180 fun bigimpl_ast_tr (asts as [asms, concl]) =

   181       let val prems =

   182         (case Ast.unfold_ast_p "_asms" asms of

   183           (asms', Ast.Appl [Ast.Constant "_asm", asm']) => asms' @ [asm']

   184         | _ => raise Ast.AST ("bigimpl_ast_tr", asts))

   185       in Ast.fold_ast_p "\\<^const>==>" (prems, concl) end

   186   | bigimpl_ast_tr asts = raise Ast.AST ("bigimpl_ast_tr", asts);

   189 (* type/term reflection *)

   191 fun type_tr [ty] = mk_type ty

   192   | type_tr ts = raise TERM ("type_tr", ts);

   195 (* dddot *)

   197 fun dddot_tr ts = Term.list_comb (Syntax.var Syntax_Ext.dddot_indexname, ts);

   200 (* quote / antiquote *)

   202 fun antiquote_tr name =

   203   let

   204     fun tr i ((t as Const (c, _)) $ u) =

   205           if c = name then tr i u $ Bound i

   206           else tr i t $ tr i u

   207       | tr i (t $ u) = tr i t $ tr i u

   208       | tr i (Abs (x, T, t)) = Abs (x, T, tr (i + 1) t)

   209       | tr _ a = a;

   210   in tr 0 end;

   212 fun quote_tr name t = Abs ("s", dummyT, antiquote_tr name (Term.incr_boundvars 1 t));

   214 fun quote_antiquote_tr quoteN antiquoteN name =

   215   let

   216     fun tr [t] = Syntax.const name $ quote_tr antiquoteN t

   217       | tr ts = raise TERM ("quote_tr", ts);

   218   in (quoteN, tr) end;

   221 (* corresponding updates *)

   223 fun update_name_tr (Free (x, T) :: ts) = list_comb (Free (suffix "_update" x, T), ts)

   224   | update_name_tr (Const (x, T) :: ts) = list_comb (Const (suffix "_update" x, T), ts)

   225   | update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) =

   226       if Term_Position.is_position ty then list_comb (c $ update_name_tr [t] $ ty, ts)

   227       else

   228         list_comb (c $ update_name_tr [t] $

   229           (Lexicon.fun_type $

   230             (Lexicon.fun_type $ Lexicon.dummy_type $ ty) $ Lexicon.dummy_type), ts)

   231   | update_name_tr ts = raise TERM ("update_name_tr", ts);

   234 (* indexed syntax *)

   236 fun indexdefault_ast_tr [] =

   237       Ast.Appl [Ast.Constant "_index",

   238         Ast.Appl [Ast.Constant "_struct", Ast.Constant "_indexdefault"]]

   239   | indexdefault_ast_tr asts = raise Ast.AST ("indexdefault_ast_tr", asts);

   241 fun indexvar_ast_tr [] = Ast.Appl [Ast.Constant "_index", Ast.Variable "some_index"]

   242   | indexvar_ast_tr asts = raise Ast.AST ("indexvar_ast_tr", asts);

   244 fun struct_ast_tr [Ast.Appl [Ast.Constant "_index", ast]] = ast

   245   | struct_ast_tr asts = Ast.mk_appl (Ast.Constant "_struct") asts;

   247 fun index_tr [t] = t

   248   | index_tr ts = raise TERM ("index_tr", ts);

   250 fun the_struct [] = error "Illegal reference to implicit structure"

   251   | the_struct (x :: _) = x;

   253 fun struct_tr structs [Const ("_indexdefault", _)] = Syntax.free (the_struct structs)

   254   | struct_tr _ ts = raise TERM ("struct_tr", ts);

   258 (** print (ast) translations **)

   260 (* types *)

   262 fun non_typed_tr' f _ ts = f ts;

   263 fun non_typed_tr'' f x _ ts = f x ts;

   266 (* type syntax *)

   268 fun tappl_ast_tr' (f, []) = raise Ast.AST ("tappl_ast_tr'", [f])

   269   | tappl_ast_tr' (f, [ty]) = Ast.Appl [Ast.Constant "_tapp", ty, f]

   270   | tappl_ast_tr' (f, ty :: tys) =

   271       Ast.Appl [Ast.Constant "_tappl", ty, Ast.fold_ast "_types" tys, f];

   273 fun fun_ast_tr' asts =

   274   if no_brackets () orelse no_type_brackets () then raise Match

   275   else

   276     (case Ast.unfold_ast_p "\\<^type>fun" (Ast.Appl (Ast.Constant "\\<^type>fun" :: asts)) of

   277       (dom as _ :: _ :: _, cod)

   278         => Ast.Appl [Ast.Constant "_bracket", Ast.fold_ast "_types" dom, cod]

   279     | _ => raise Match);

   282 (* application *)

   284 fun appl_ast_tr' (f, []) = raise Ast.AST ("appl_ast_tr'", [f])

   285   | appl_ast_tr' (f, args) = Ast.Appl [Ast.Constant "_appl", f, Ast.fold_ast "_args" args];

   287 fun applC_ast_tr' (f, []) = raise Ast.AST ("applC_ast_tr'", [f])

   288   | applC_ast_tr' (f, args) = Ast.Appl [Ast.Constant "_applC", f, Ast.fold_ast "_cargs" args];

   291 (* partial eta-contraction before printing *)

   293 fun eta_abs (Abs (a, T, t)) =

   294       (case eta_abs t of

   295         t' as Const ("_aprop", _) $ _ => Abs (a, T, t')

   296       | t' as f $ u =>

   297           (case eta_abs u of

   298             Bound 0 =>

   299               if Term.is_dependent f then Abs (a, T, t')

   300               else incr_boundvars ~1 f

   301           | _ => Abs (a, T, t'))

   302       | t' => Abs (a, T, t'))

   303   | eta_abs t = t;

   305 val eta_contract_default = Unsynchronized.ref true;

   306 val eta_contract_raw = Config.declare "eta_contract" (fn _ => Config.Bool (! eta_contract_default));

   307 val eta_contract = Config.bool eta_contract_raw;

   309 fun eta_contr ctxt tm =

   310   if Config.get ctxt eta_contract then eta_abs tm else tm;

   313 (* abstraction *)

   315 fun mark_bound_abs (x, T) = Const ("_bound", T --> T) $ Free (x, T);

   316 fun mark_bound_body (x, T) = Const ("_bound", dummyT) $ Free (x, T);

   318 fun bound_vars vars body =

   319   subst_bounds (map mark_bound_abs (Term.rename_wrt_term body vars), body);

   321 fun strip_abss vars_of body_of tm =

   322   let

   323     val vars = vars_of tm;

   324     val body = body_of tm;

   325     val rev_new_vars = Term.rename_wrt_term body vars;

   326     fun subst (x, T) b =

   327       if can Name.dest_internal x andalso not (Term.is_dependent b)

   328       then (Const ("_idtdummy", T), incr_boundvars ~1 b)

   329       else (mark_bound_abs (x, T), Term.subst_bound (mark_bound_body (x, T), b));

   330     val (rev_vars', body') = fold_map subst rev_new_vars body;

   331   in (rev rev_vars', body') end;

   334 fun abs_tr' ctxt tm =

   335   uncurry (fold_rev (fn x => fn t => Syntax.const "_abs" $ x $ t))

   336     (strip_abss strip_abs_vars strip_abs_body (eta_contr ctxt tm));

   338 fun atomic_abs_tr' (x, T, t) =

   339   let val [xT] = Term.rename_wrt_term t [(x, T)]

   340   in (mark_bound_abs xT, subst_bound (mark_bound_body xT, t)) end;

   342 fun abs_ast_tr' asts =

   343   (case Ast.unfold_ast_p "_abs" (Ast.Appl (Ast.Constant "_abs" :: asts)) of

   344     ([], _) => raise Ast.AST ("abs_ast_tr'", asts)

   345   | (xs, body) => Ast.Appl [Ast.Constant "_lambda", Ast.fold_ast "_pttrns" xs, body]);

   347 fun const_abs_tr' t =

   348   (case eta_abs t of

   349     Abs (_, _, t') =>

   350       if Term.is_dependent t' then raise Match

   351       else incr_boundvars ~1 t'

   352   | _ => raise Match);

   355 (* binders *)

   357 fun mk_binder_tr' (name, syn) =

   358   let

   359     fun mk_idts [] = raise Match    (*abort translation*)

   360       | mk_idts [idt] = idt

   361       | mk_idts (idt :: idts) = Syntax.const "_idts" $ idt $ mk_idts idts;

   363     fun tr' t =

   364       let

   365         val (xs, bd) = strip_abss (strip_qnt_vars name) (strip_qnt_body name) t;

   366       in Syntax.const syn $ mk_idts xs $ bd end;

   368     fun binder_tr' (t :: ts) = Term.list_comb (tr' (Syntax.const name $ t), ts)

   369       | binder_tr' [] = raise Match;

   370   in (name, binder_tr') end;

   372 fun preserve_binder_abs_tr' name syn = (name, fn Abs abs :: ts =>

   373   let val (x, t) = atomic_abs_tr' abs

   374   in list_comb (Syntax.const syn $ x $ t, ts) end);

   376 fun preserve_binder_abs2_tr' name syn = (name, fn A :: Abs abs :: ts =>

   377   let val (x, t) = atomic_abs_tr' abs

   378   in list_comb (Syntax.const syn $ x $ A $ t, ts) end);

   381 (* idtyp constraints *)

   383 fun idtyp_ast_tr' a [Ast.Appl [Ast.Constant "_constrain", x, ty], xs] =

   384       Ast.Appl [Ast.Constant a, Ast.Appl [Ast.Constant "_idtyp", x, ty], xs]

   385   | idtyp_ast_tr' _ _ = raise Match;

   388 (* meta propositions *)

   390 fun prop_tr' tm =

   391   let

   392     fun aprop t = Syntax.const "_aprop" $ t;

   394     fun is_prop Ts t =

   395       fastype_of1 (Ts, t) = propT handle TERM _ => false;

   397     fun is_term (Const ("Pure.term", _) $ _) = true

   398       | is_term _ = false;

   400     fun tr' _ (t as Const _) = t

   401       | tr' Ts (t as Const ("_bound", _) $ u) =

   402           if is_prop Ts u then aprop t else t

   403       | tr' _ (t as Free (x, T)) =

   404           if T = propT then aprop (Syntax.free x) else t

   405       | tr' _ (t as Var (xi, T)) =

   406           if T = propT then aprop (Syntax.var xi) else t

   407       | tr' Ts (t as Bound _) =

   408           if is_prop Ts t then aprop t else t

   409       | tr' Ts (Abs (x, T, t)) = Abs (x, T, tr' (T :: Ts) t)

   410       | tr' Ts (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [T])))) =

   411           if is_prop Ts t andalso not (is_term t) then Const ("_type_prop", T) $ tr' Ts t1

   412           else tr' Ts t1 $ tr' Ts t2

   413       | tr' Ts (t as t1 $ t2) =

   414           (if is_Const (Term.head_of t) orelse not (is_prop Ts t)

   415             then I else aprop) (tr' Ts t1 $ tr' Ts t2);

   416   in tr' [] tm end;

   419 (* meta implication *)

   421 fun impl_ast_tr' asts =

   422   if no_brackets () then raise Match

   423   else

   424     (case Ast.unfold_ast_p "\\<^const>==>" (Ast.Appl (Ast.Constant "\\<^const>==>" :: asts)) of

   425       (prems as _ :: _ :: _, concl) =>

   426         let

   427           val (asms, asm) = split_last prems;

   428           val asms' = Ast.fold_ast_p "_asms" (asms, Ast.Appl [Ast.Constant "_asm", asm]);

   429         in Ast.Appl [Ast.Constant "_bigimpl", asms', concl] end

   430     | _ => raise Match);

   433 (* dependent / nondependent quantifiers *)

   435 fun var_abs mark (x, T, b) =

   436   let val (x', _) = Name.variant x (Term.declare_term_names b Name.context)

   437   in (x', subst_bound (mark (x', T), b)) end;

   439 val variant_abs = var_abs Free;

   440 val variant_abs' = var_abs mark_bound_abs;

   442 fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) =

   443       if Term.is_dependent B then

   444         let val (x', B') = variant_abs' (x, dummyT, B);

   445         in Term.list_comb (Syntax.const q $ mark_bound_abs (x', T) $ A $ B', ts) end

   446       else Term.list_comb (Syntax.const r $ A $ incr_boundvars ~1 B, ts)

   447   | dependent_tr' _ _ = raise Match;

   450 (* quote / antiquote *)

   452 fun antiquote_tr' name =

   453   let

   454     fun tr' i (t $ u) =

   455           if u aconv Bound i then Syntax.const name $ tr' i t

   456           else tr' i t $ tr' i u

   457       | tr' i (Abs (x, T, t)) = Abs (x, T, tr' (i + 1) t)

   458       | tr' i a = if a aconv Bound i then raise Match else a;

   459   in tr' 0 end;

   461 fun quote_tr' name (Abs (_, _, t)) = Term.incr_boundvars ~1 (antiquote_tr' name t)

   462   | quote_tr' _ _ = raise Match;

   464 fun quote_antiquote_tr' quoteN antiquoteN name =

   465   let

   466     fun tr' (t :: ts) = Term.list_comb (Syntax.const quoteN $ quote_tr' antiquoteN t, ts)

   467       | tr' _ = raise Match;

   468   in (name, tr') end;

   471 (* corresponding updates *)

   473 local

   475 fun upd_type (Type ("fun", [Type ("fun", [_, T]), _])) = T

   476   | upd_type _ = dummyT;

   478 fun upd_tr' (x_upd, T) =

   479   (case try (unsuffix "_update") x_upd of

   480     SOME x => (x, upd_type T)

   481   | NONE => raise Match);

   483 in

   485 fun update_name_tr' (Free x) = Free (upd_tr' x)

   486   | update_name_tr' ((c as Const ("_free", _)) $ Free x) = c $ Free (upd_tr' x)

   487   | update_name_tr' (Const x) = Const (upd_tr' x)

   488   | update_name_tr' _ = raise Match;

   490 end;

   493 (* indexed syntax *)

   495 fun index_ast_tr' [Ast.Appl [Ast.Constant "_struct", ast]] = ast

   496   | index_ast_tr' _ = raise Match;

   498 fun struct_ast_tr' structs [Ast.Constant "_indexdefault"] =

   499       Ast.Appl [Ast.Constant "_free",

   500         Ast.Variable (the_struct structs handle ERROR _ => raise Match)]

   501   | struct_ast_tr' _ _ = raise Match;

   505 (** Pure translations **)

   507 val pure_trfuns =

   508   ([("_strip_positions", strip_positions_ast_tr),

   509     ("_constify", constify_ast_tr),

   510     ("_tapp", tapp_ast_tr),

   511     ("_tappl", tappl_ast_tr),

   512     ("_bracket", bracket_ast_tr),

   513     ("_appl", appl_ast_tr),

   514     ("_applC", applC_ast_tr),

   515     ("_lambda", lambda_ast_tr),

   516     ("_idtyp", idtyp_ast_tr),

   517     ("_idtypdummy", idtypdummy_ast_tr),

   518     ("_bigimpl", bigimpl_ast_tr),

   519     ("_indexdefault", indexdefault_ast_tr),

   520     ("_indexvar", indexvar_ast_tr),

   521     ("_struct", struct_ast_tr)],

   522    [("_abs", abs_tr),

   523     ("_aprop", aprop_tr),

   524     ("_ofclass", ofclass_tr),

   525     ("_sort_constraint", sort_constraint_tr),

   526     ("_TYPE", type_tr),

   527     ("_DDDOT", dddot_tr),

   528     ("_update_name", update_name_tr),

   529     ("_index", index_tr)],

   530    ([]: (string * (term list -> term)) list),

   531    [("\\<^type>fun", fun_ast_tr'),

   532     ("_abs", abs_ast_tr'),

   533     ("_idts", idtyp_ast_tr' "_idts"),

   534     ("_pttrns", idtyp_ast_tr' "_pttrns"),

   535     ("\\<^const>==>", impl_ast_tr'),

   536     ("_index", index_ast_tr')]);

   538 fun struct_trfuns structs =

   539   ([], [("_struct", struct_tr structs)], [], [("_struct", struct_ast_tr' structs)]);

   541 end;

   543 structure Basic_Syntax_Trans: BASIC_SYNTAX_TRANS = Syntax_Trans;

   544 open Basic_Syntax_Trans;

author	wenzelm
	Wed Dec 12 23:36:07 2012 +0100 (2012-12-12 ago)
changeset 50499	f496b2b7bafb
parent 49660	de49d9b4d7bc
child 51656	4ce2f7607d3d
permissions	-rw-r--r--