src/Pure/Syntax/syntax_trans.ML
author wenzelm
Fri Mar 21 20:33:56 2014 +0100 (2014-03-21)
changeset 56245 84fc7dfa3cd4
parent 56243 2e10a36b8d46
child 56438 7f6b2634d853
permissions -rw-r--r--
more qualified names;
     1 (*  Title:      Pure/Syntax/syntax_trans.ML
     2     Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
     3 
     4 Syntax translation functions.
     5 *)
     6 
     7 signature BASIC_SYNTAX_TRANS =
     8 sig
     9   val eta_contract: bool Config.T
    10 end
    11 
    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 * (Proof.context -> 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 ->
    26     string * (Proof.context -> term list -> term)
    27   val non_typed_tr': (Proof.context -> term list -> term) ->
    28     Proof.context -> typ -> term list -> term
    29   val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
    30   val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
    31   val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
    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 * (Proof.context -> term list -> term)
    40   val preserve_binder_abs_tr': string -> string -> string * (Proof.context -> term list -> term)
    41   val preserve_binder_abs2_tr': string -> string -> string * (Proof.context -> term list -> term)
    42   val variant_abs: string * typ * term -> string * term
    43   val variant_abs': string * typ * term -> string * term
    44   val dependent_tr': string * string -> term list -> term
    45   val antiquote_tr': string -> term -> term
    46   val quote_tr': string -> term -> term
    47   val quote_antiquote_tr': string -> string -> string ->
    48     string * (Proof.context -> term list -> term)
    49   val update_name_tr': term -> term
    50   val pure_parse_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list
    51   val pure_parse_translation: (string * (Proof.context -> term list -> term)) list
    52   val pure_print_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list
    53   val struct_tr: string list -> string * (Proof.context -> term list -> term)
    54   val struct_ast_tr': string list -> string * (Proof.context -> Ast.ast list -> Ast.ast)
    55 end;
    56 
    57 structure Syntax_Trans: SYNTAX_TRANS =
    58 struct
    59 
    60 structure Syntax = Lexicon.Syntax;
    61 
    62 
    63 (* print mode *)
    64 
    65 val bracketsN = "brackets";
    66 val no_bracketsN = "no_brackets";
    67 
    68 fun no_brackets () =
    69   find_first (fn mode => mode = bracketsN orelse mode = no_bracketsN)
    70     (print_mode_value ()) = SOME no_bracketsN;
    71 
    72 val type_bracketsN = "type_brackets";
    73 val no_type_bracketsN = "no_type_brackets";
    74 
    75 fun no_type_brackets () =
    76   find_first (fn mode => mode = type_bracketsN orelse mode = no_type_bracketsN)
    77     (print_mode_value ()) <> SOME type_bracketsN;
    78 
    79 
    80 
    81 (** parse (ast) translations **)
    82 
    83 (* strip_positions *)
    84 
    85 fun strip_positions_ast_tr [ast] = Ast.strip_positions ast
    86   | strip_positions_ast_tr asts = raise Ast.AST ("strip_positions_ast_tr", asts);
    87 
    88 
    89 (* constify *)
    90 
    91 fun constify_ast_tr [Ast.Appl [c as Ast.Constant "_constrain", ast1, ast2]] =
    92       Ast.Appl [c, constify_ast_tr [ast1], ast2]
    93   | constify_ast_tr [Ast.Variable c] = Ast.Constant c
    94   | constify_ast_tr asts = raise Ast.AST ("constify_ast_tr", asts);
    95 
    96 
    97 (* type syntax *)
    98 
    99 fun tapp_ast_tr [ty, c] = Ast.Appl [c, ty]
   100   | tapp_ast_tr asts = raise Ast.AST ("tapp_ast_tr", asts);
   101 
   102 fun tappl_ast_tr [ty, tys, c] = Ast.mk_appl c (ty :: Ast.unfold_ast "_types" tys)
   103   | tappl_ast_tr asts = raise Ast.AST ("tappl_ast_tr", asts);
   104 
   105 fun bracket_ast_tr [dom, cod] = Ast.fold_ast_p "\\<^type>fun" (Ast.unfold_ast "_types" dom, cod)
   106   | bracket_ast_tr asts = raise Ast.AST ("bracket_ast_tr", asts);
   107 
   108 
   109 (* application *)
   110 
   111 fun appl_ast_tr [f, args] = Ast.Appl (f :: Ast.unfold_ast "_args" args)
   112   | appl_ast_tr asts = raise Ast.AST ("appl_ast_tr", asts);
   113 
   114 fun applC_ast_tr [f, args] = Ast.Appl (f :: Ast.unfold_ast "_cargs" args)
   115   | applC_ast_tr asts = raise Ast.AST ("applC_ast_tr", asts);
   116 
   117 
   118 (* abstraction *)
   119 
   120 fun idtyp_ast_tr [x, ty] = Ast.Appl [Ast.Constant "_constrain", x, ty]
   121   | idtyp_ast_tr asts = raise Ast.AST ("idtyp_ast_tr", asts);
   122 
   123 fun lambda_ast_tr [pats, body] = Ast.fold_ast_p "_abs" (Ast.unfold_ast "_pttrns" pats, body)
   124   | lambda_ast_tr asts = raise Ast.AST ("lambda_ast_tr", asts);
   125 
   126 fun absfree_proper (x, T) t =
   127   if Name.is_internal x
   128   then error ("Illegal internal variable in abstraction: " ^ quote x)
   129   else absfree (x, T) t;
   130 
   131 fun abs_tr [Free x, t] = absfree_proper x t
   132   | abs_tr [Const ("_idtdummy", T), t] = absdummy T t
   133   | abs_tr [Const ("_constrain", _) $ x $ tT, t] =
   134       Syntax.const "_constrainAbs" $ abs_tr [x, t] $ tT
   135   | abs_tr ts = raise TERM ("abs_tr", ts);
   136 
   137 
   138 (* binder *)
   139 
   140 fun mk_binder_tr (syn, name) =
   141   let
   142     fun err ts = raise TERM ("binder_tr: " ^ syn, ts)
   143     fun binder_tr [Const ("_idts", _) $ idt $ idts, t] = binder_tr [idt, binder_tr [idts, t]]
   144       | binder_tr [x, t] =
   145           let val abs = abs_tr [x, t] handle TERM _ => err [x, t]
   146           in Syntax.const name $ abs end
   147       | binder_tr ts = err ts;
   148   in (syn, fn _ => binder_tr) end;
   149 
   150 
   151 (* type propositions *)
   152 
   153 fun mk_type ty =
   154   Syntax.const "_constrain" $
   155     Syntax.const "\\<^const>Pure.type" $ (Syntax.const "\\<^type>itself" $ ty);
   156 
   157 fun ofclass_tr [ty, cls] = cls $ mk_type ty
   158   | ofclass_tr ts = raise TERM ("ofclass_tr", ts);
   159 
   160 fun sort_constraint_tr [ty] = Syntax.const "\\<^const>Pure.sort_constraint" $ mk_type ty
   161   | sort_constraint_tr ts = raise TERM ("sort_constraint_tr", ts);
   162 
   163 
   164 (* meta propositions *)
   165 
   166 fun aprop_tr [t] = Syntax.const "_constrain" $ t $ Syntax.const "\\<^type>prop"
   167   | aprop_tr ts = raise TERM ("aprop_tr", ts);
   168 
   169 
   170 (* meta implication *)
   171 
   172 fun bigimpl_ast_tr (asts as [asms, concl]) =
   173       let val prems =
   174         (case Ast.unfold_ast_p "_asms" asms of
   175           (asms', Ast.Appl [Ast.Constant "_asm", asm']) => asms' @ [asm']
   176         | _ => raise Ast.AST ("bigimpl_ast_tr", asts))
   177       in Ast.fold_ast_p "\\<^const>Pure.imp" (prems, concl) end
   178   | bigimpl_ast_tr asts = raise Ast.AST ("bigimpl_ast_tr", asts);
   179 
   180 
   181 (* type/term reflection *)
   182 
   183 fun type_tr [ty] = mk_type ty
   184   | type_tr ts = raise TERM ("type_tr", ts);
   185 
   186 
   187 (* dddot *)
   188 
   189 fun dddot_tr ts = Term.list_comb (Syntax.var Syntax_Ext.dddot_indexname, ts);
   190 
   191 
   192 (* quote / antiquote *)
   193 
   194 fun antiquote_tr name =
   195   let
   196     fun tr i ((t as Const (c, _)) $ u) =
   197           if c = name then tr i u $ Bound i
   198           else tr i t $ tr i u
   199       | tr i (t $ u) = tr i t $ tr i u
   200       | tr i (Abs (x, T, t)) = Abs (x, T, tr (i + 1) t)
   201       | tr _ a = a;
   202   in tr 0 end;
   203 
   204 fun quote_tr name t = Abs ("s", dummyT, antiquote_tr name (Term.incr_boundvars 1 t));
   205 
   206 fun quote_antiquote_tr quoteN antiquoteN name =
   207   let
   208     fun tr [t] = Syntax.const name $ quote_tr antiquoteN t
   209       | tr ts = raise TERM ("quote_tr", ts);
   210   in (quoteN, fn _ => tr) end;
   211 
   212 
   213 (* corresponding updates *)
   214 
   215 fun update_name_tr (Free (x, T) :: ts) = list_comb (Free (suffix "_update" x, T), ts)
   216   | update_name_tr (Const (x, T) :: ts) = list_comb (Const (suffix "_update" x, T), ts)
   217   | update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) =
   218       if Term_Position.is_position ty then list_comb (c $ update_name_tr [t] $ ty, ts)
   219       else
   220         list_comb (c $ update_name_tr [t] $
   221           (Lexicon.fun_type $
   222             (Lexicon.fun_type $ Lexicon.dummy_type $ ty) $ Lexicon.dummy_type), ts)
   223   | update_name_tr ts = raise TERM ("update_name_tr", ts);
   224 
   225 
   226 (* indexed syntax *)
   227 
   228 fun indexdefault_ast_tr [] =
   229       Ast.Appl [Ast.Constant "_index",
   230         Ast.Appl [Ast.Constant "_struct", Ast.Constant "_indexdefault"]]
   231   | indexdefault_ast_tr asts = raise Ast.AST ("indexdefault_ast_tr", asts);
   232 
   233 fun indexvar_ast_tr [] = Ast.Appl [Ast.Constant "_index", Ast.Variable "some_index"]
   234   | indexvar_ast_tr asts = raise Ast.AST ("indexvar_ast_tr", asts);
   235 
   236 fun struct_ast_tr [Ast.Appl [Ast.Constant "_index", ast]] = ast
   237   | struct_ast_tr asts = Ast.mk_appl (Ast.Constant "_struct") asts;
   238 
   239 fun index_tr [t] = t
   240   | index_tr ts = raise TERM ("index_tr", ts);
   241 
   242 fun struct_tr structs =
   243   ("_struct", fn _ =>
   244     (fn [Const ("_indexdefault", _)] =>
   245         (case structs of
   246           x :: _ => Syntax.const (Lexicon.mark_fixed x)
   247         | _ => error "Illegal reference to implicit structure")
   248       | ts => raise TERM ("struct_tr", ts)));
   249 
   250 
   251 
   252 (** print (ast) translations **)
   253 
   254 (* types *)
   255 
   256 fun non_typed_tr' f ctxt _ ts = f ctxt ts;
   257 
   258 
   259 (* type syntax *)
   260 
   261 fun tappl_ast_tr' (f, []) = raise Ast.AST ("tappl_ast_tr'", [f])
   262   | tappl_ast_tr' (f, [ty]) = Ast.Appl [Ast.Constant "_tapp", ty, f]
   263   | tappl_ast_tr' (f, ty :: tys) =
   264       Ast.Appl [Ast.Constant "_tappl", ty, Ast.fold_ast "_types" tys, f];
   265 
   266 fun fun_ast_tr' asts =
   267   if no_brackets () orelse no_type_brackets () then raise Match
   268   else
   269     (case Ast.unfold_ast_p "\\<^type>fun" (Ast.Appl (Ast.Constant "\\<^type>fun" :: asts)) of
   270       (dom as _ :: _ :: _, cod)
   271         => Ast.Appl [Ast.Constant "_bracket", Ast.fold_ast "_types" dom, cod]
   272     | _ => raise Match);
   273 
   274 
   275 (* application *)
   276 
   277 fun appl_ast_tr' (f, []) = raise Ast.AST ("appl_ast_tr'", [f])
   278   | appl_ast_tr' (f, args) = Ast.Appl [Ast.Constant "_appl", f, Ast.fold_ast "_args" args];
   279 
   280 fun applC_ast_tr' (f, []) = raise Ast.AST ("applC_ast_tr'", [f])
   281   | applC_ast_tr' (f, args) = Ast.Appl [Ast.Constant "_applC", f, Ast.fold_ast "_cargs" args];
   282 
   283 
   284 (* partial eta-contraction before printing *)
   285 
   286 fun eta_abs (Abs (a, T, t)) =
   287       (case eta_abs t of
   288         t' as Const ("_aprop", _) $ _ => Abs (a, T, t')
   289       | t' as f $ u =>
   290           (case eta_abs u of
   291             Bound 0 =>
   292               if Term.is_dependent f then Abs (a, T, t')
   293               else incr_boundvars ~1 f
   294           | _ => Abs (a, T, t'))
   295       | t' => Abs (a, T, t'))
   296   | eta_abs t = t;
   297 
   298 val eta_contract_raw = Config.declare_option "eta_contract";
   299 val eta_contract = Config.bool eta_contract_raw;
   300 
   301 fun eta_contr ctxt tm =
   302   if Config.get ctxt eta_contract then eta_abs tm else tm;
   303 
   304 
   305 (* abstraction *)
   306 
   307 fun mark_bound_abs (x, T) = Const ("_bound", T --> T) $ Free (x, T);
   308 fun mark_bound_body (x, T) = Const ("_bound", dummyT) $ Free (x, T);
   309 
   310 fun bound_vars vars body =
   311   subst_bounds (map mark_bound_abs (Term.rename_wrt_term body vars), body);
   312 
   313 fun strip_abss vars_of body_of tm =
   314   let
   315     val vars = vars_of tm;
   316     val body = body_of tm;
   317     val rev_new_vars = Term.rename_wrt_term body vars;
   318     fun subst (x, T) b =
   319       if Name.is_internal x andalso not (Term.is_dependent b)
   320       then (Const ("_idtdummy", T), incr_boundvars ~1 b)
   321       else (mark_bound_abs (x, T), Term.subst_bound (mark_bound_body (x, T), b));
   322     val (rev_vars', body') = fold_map subst rev_new_vars body;
   323   in (rev rev_vars', body') end;
   324 
   325 
   326 fun abs_tr' ctxt tm =
   327   uncurry (fold_rev (fn x => fn t => Syntax.const "_abs" $ x $ t))
   328     (strip_abss strip_abs_vars strip_abs_body (eta_contr ctxt tm));
   329 
   330 fun atomic_abs_tr' (x, T, t) =
   331   let val [xT] = Term.rename_wrt_term t [(x, T)]
   332   in (mark_bound_abs xT, subst_bound (mark_bound_body xT, t)) end;
   333 
   334 fun abs_ast_tr' asts =
   335   (case Ast.unfold_ast_p "_abs" (Ast.Appl (Ast.Constant "_abs" :: asts)) of
   336     ([], _) => raise Ast.AST ("abs_ast_tr'", asts)
   337   | (xs, body) => Ast.Appl [Ast.Constant "_lambda", Ast.fold_ast "_pttrns" xs, body]);
   338 
   339 fun const_abs_tr' t =
   340   (case eta_abs t of
   341     Abs (_, _, t') =>
   342       if Term.is_dependent t' then raise Match
   343       else incr_boundvars ~1 t'
   344   | _ => raise Match);
   345 
   346 
   347 (* binders *)
   348 
   349 fun mk_binder_tr' (name, syn) =
   350   let
   351     fun mk_idts [] = raise Match    (*abort translation*)
   352       | mk_idts [idt] = idt
   353       | mk_idts (idt :: idts) = Syntax.const "_idts" $ idt $ mk_idts idts;
   354 
   355     fun tr' t =
   356       let
   357         val (xs, bd) = strip_abss (strip_qnt_vars name) (strip_qnt_body name) t;
   358       in Syntax.const syn $ mk_idts xs $ bd end;
   359 
   360     fun binder_tr' (t :: ts) = Term.list_comb (tr' (Syntax.const name $ t), ts)
   361       | binder_tr' [] = raise Match;
   362   in (name, fn _ => binder_tr') end;
   363 
   364 fun preserve_binder_abs_tr' name syn = (name, fn _ => fn Abs abs :: ts =>
   365   let val (x, t) = atomic_abs_tr' abs
   366   in list_comb (Syntax.const syn $ x $ t, ts) end);
   367 
   368 fun preserve_binder_abs2_tr' name syn = (name, fn _ => fn A :: Abs abs :: ts =>
   369   let val (x, t) = atomic_abs_tr' abs
   370   in list_comb (Syntax.const syn $ x $ A $ t, ts) end);
   371 
   372 
   373 (* idtyp constraints *)
   374 
   375 fun idtyp_ast_tr' a [Ast.Appl [Ast.Constant "_constrain", x, ty], xs] =
   376       Ast.Appl [Ast.Constant a, Ast.Appl [Ast.Constant "_idtyp", x, ty], xs]
   377   | idtyp_ast_tr' _ _ = raise Match;
   378 
   379 
   380 (* meta implication *)
   381 
   382 fun impl_ast_tr' asts =
   383   if no_brackets () then raise Match
   384   else
   385     (case Ast.unfold_ast_p "\\<^const>Pure.imp"
   386         (Ast.Appl (Ast.Constant "\\<^const>Pure.imp" :: asts)) of
   387       (prems as _ :: _ :: _, concl) =>
   388         let
   389           val (asms, asm) = split_last prems;
   390           val asms' = Ast.fold_ast_p "_asms" (asms, Ast.Appl [Ast.Constant "_asm", asm]);
   391         in Ast.Appl [Ast.Constant "_bigimpl", asms', concl] end
   392     | _ => raise Match);
   393 
   394 
   395 (* dependent / nondependent quantifiers *)
   396 
   397 fun var_abs mark (x, T, b) =
   398   let val (x', _) = Name.variant x (Term.declare_term_names b Name.context)
   399   in (x', subst_bound (mark (x', T), b)) end;
   400 
   401 val variant_abs = var_abs Free;
   402 val variant_abs' = var_abs mark_bound_abs;
   403 
   404 fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) =
   405       if Term.is_dependent B then
   406         let val (x', B') = variant_abs' (x, dummyT, B);
   407         in Term.list_comb (Syntax.const q $ mark_bound_abs (x', T) $ A $ B', ts) end
   408       else Term.list_comb (Syntax.const r $ A $ incr_boundvars ~1 B, ts)
   409   | dependent_tr' _ _ = raise Match;
   410 
   411 
   412 (* quote / antiquote *)
   413 
   414 fun antiquote_tr' name =
   415   let
   416     fun tr' i (t $ u) =
   417           if u aconv Bound i then Syntax.const name $ tr' i t
   418           else tr' i t $ tr' i u
   419       | tr' i (Abs (x, T, t)) = Abs (x, T, tr' (i + 1) t)
   420       | tr' i a = if a aconv Bound i then raise Match else a;
   421   in tr' 0 end;
   422 
   423 fun quote_tr' name (Abs (_, _, t)) = Term.incr_boundvars ~1 (antiquote_tr' name t)
   424   | quote_tr' _ _ = raise Match;
   425 
   426 fun quote_antiquote_tr' quoteN antiquoteN name =
   427   let
   428     fun tr' (t :: ts) = Term.list_comb (Syntax.const quoteN $ quote_tr' antiquoteN t, ts)
   429       | tr' _ = raise Match;
   430   in (name, fn _ => tr') end;
   431 
   432 
   433 (* corresponding updates *)
   434 
   435 local
   436 
   437 fun upd_type (Type ("fun", [Type ("fun", [_, T]), _])) = T
   438   | upd_type _ = dummyT;
   439 
   440 fun upd_tr' (x_upd, T) =
   441   (case try (unsuffix "_update") x_upd of
   442     SOME x => (x, upd_type T)
   443   | NONE => raise Match);
   444 
   445 in
   446 
   447 fun update_name_tr' (Free x) = Free (upd_tr' x)
   448   | update_name_tr' ((c as Const ("_free", _)) $ Free x) = c $ Free (upd_tr' x)
   449   | update_name_tr' (Const x) = Const (upd_tr' x)
   450   | update_name_tr' _ = raise Match;
   451 
   452 end;
   453 
   454 
   455 (* indexed syntax *)
   456 
   457 fun index_ast_tr' [Ast.Appl [Ast.Constant "_struct", ast]] = ast
   458   | index_ast_tr' _ = raise Match;
   459 
   460 fun struct_ast_tr' structs =
   461   ("_struct", fn _ =>
   462     (fn [Ast.Constant "_indexdefault"] =>
   463         (case structs of
   464           x :: _ => Ast.Appl [Ast.Constant "_free", Ast.Variable x]
   465         | _ => raise Match)
   466       | _ => raise Match));
   467 
   468 
   469 
   470 (** Pure translations **)
   471 
   472 val pure_parse_ast_translation =
   473  [("_strip_positions", fn _ => strip_positions_ast_tr),
   474   ("_constify", fn _ => constify_ast_tr),
   475   ("_tapp", fn _ => tapp_ast_tr),
   476   ("_tappl", fn _ => tappl_ast_tr),
   477   ("_bracket", fn _ => bracket_ast_tr),
   478   ("_appl", fn _ => appl_ast_tr),
   479   ("_applC", fn _ => applC_ast_tr),
   480   ("_lambda", fn _ => lambda_ast_tr),
   481   ("_idtyp", fn _ => idtyp_ast_tr),
   482   ("_bigimpl", fn _ => bigimpl_ast_tr),
   483   ("_indexdefault", fn _ => indexdefault_ast_tr),
   484   ("_indexvar", fn _ => indexvar_ast_tr),
   485   ("_struct", fn _ => struct_ast_tr)];
   486 
   487 val pure_parse_translation =
   488  [("_abs", fn _ => abs_tr),
   489   ("_aprop", fn _ => aprop_tr),
   490   ("_ofclass", fn _ => ofclass_tr),
   491   ("_sort_constraint", fn _ => sort_constraint_tr),
   492   ("_TYPE", fn _ => type_tr),
   493   ("_DDDOT", fn _ => dddot_tr),
   494   ("_update_name", fn _ => update_name_tr),
   495   ("_index", fn _ => index_tr)];
   496 
   497 val pure_print_ast_translation =
   498  [("\\<^type>fun", fn _ => fun_ast_tr'),
   499   ("_abs", fn _ => abs_ast_tr'),
   500   ("_idts", fn _ => idtyp_ast_tr' "_idts"),
   501   ("_pttrns", fn _ => idtyp_ast_tr' "_pttrns"),
   502   ("\\<^const>Pure.imp", fn _ => impl_ast_tr'),
   503   ("_index", fn _ => index_ast_tr')];
   504 
   505 end;
   506 
   507 structure Basic_Syntax_Trans: BASIC_SYNTAX_TRANS = Syntax_Trans;
   508 open Basic_Syntax_Trans;