src/Pure/Syntax/syn_trans.ML
author wenzelm
Wed Oct 31 21:59:07 2001 +0100 (2001-10-31)
changeset 12004 1703de633aaf
parent 11491 085a0d2857e8
child 12122 7f8d88ed4f21
permissions -rw-r--r--
IsarThy.theorem_i: no locale;
     1 (*  Title:      Pure/Syntax/syn_trans.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
     4 
     5 Syntax translation functions.
     6 *)
     7 
     8 signature SYN_TRANS0 =
     9 sig
    10   val eta_contract: bool ref
    11   val mk_binder_tr: string * string -> string * (term list -> term)
    12   val mk_binder_tr': string * string -> string * (term list -> term)
    13   val dependent_tr': string * string -> term list -> term
    14   val antiquote_tr: string -> term -> term
    15   val quote_tr: string -> term -> term
    16   val quote_antiquote_tr: string -> string -> string -> string * (term list -> term)
    17   val antiquote_tr': string -> term -> term
    18   val quote_tr': string -> term -> term
    19   val quote_antiquote_tr': string -> string -> string -> string * (term list -> term)
    20   val mark_bound: string -> term
    21   val mark_boundT: string * typ -> term
    22   val variant_abs': string * typ * term -> string * term
    23 end;
    24 
    25 signature SYN_TRANS1 =
    26 sig
    27   include SYN_TRANS0
    28   val constrainAbsC: string
    29   val pure_trfuns:
    30       (string * (Ast.ast list -> Ast.ast)) list *
    31       (string * (term list -> term)) list *
    32       (string * (term list -> term)) list *
    33       (string * (Ast.ast list -> Ast.ast)) list
    34   val pure_trfunsT: (string * (bool -> typ -> term list -> term)) list
    35 end;
    36 
    37 signature SYN_TRANS =
    38 sig
    39   include SYN_TRANS1
    40   val abs_tr': term -> term
    41   val prop_tr': term -> term
    42   val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
    43   val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
    44   val pt_to_ast: (string -> (Ast.ast list -> Ast.ast) option) -> Parser.parsetree -> Ast.ast
    45   val ast_to_term: (string -> (term list -> term) option) -> Ast.ast -> term
    46 end;
    47 
    48 structure SynTrans: SYN_TRANS =
    49 struct
    50 
    51 
    52 (** parse (ast) translations **)
    53 
    54 (* constify *)
    55 
    56 fun constify_ast_tr [Ast.Variable c] = Ast.Constant c
    57   | constify_ast_tr asts = raise Ast.AST ("constify_ast_tr", asts);
    58 
    59 
    60 (* application *)
    61 
    62 fun appl_ast_tr [f, args] = Ast.Appl (f :: Ast.unfold_ast "_args" args)
    63   | appl_ast_tr asts = raise Ast.AST ("appl_ast_tr", asts);
    64 
    65 fun applC_ast_tr [f, args] = Ast.Appl (f :: Ast.unfold_ast "_cargs" args)
    66   | applC_ast_tr asts = raise Ast.AST ("applC_ast_tr", asts);
    67 
    68 
    69 (* abstraction *)
    70 
    71 fun idtyp_ast_tr (*"_idtyp"*) [x, ty] = Ast.Appl [Ast.Constant SynExt.constrainC, x, ty]
    72   | idtyp_ast_tr (*"_idtyp"*) asts = raise Ast.AST ("idtyp_ast_tr", asts);
    73 
    74 fun lambda_ast_tr (*"_lambda"*) [pats, body] =
    75       Ast.fold_ast_p "_abs" (Ast.unfold_ast "_pttrns" pats, body)
    76   | lambda_ast_tr (*"_lambda"*) asts = raise Ast.AST ("lambda_ast_tr", asts);
    77 
    78 val constrainAbsC = "_constrainAbs";
    79 
    80 fun abs_tr (*"_abs"*) [Free (x, T), body] = Term.absfree (x, T, body)
    81   | abs_tr (*"_abs"*) (ts as [Const (c, _) $ Free (x, T) $ tT, body]) =
    82       if c = SynExt.constrainC
    83         then Lexicon.const constrainAbsC $ Term.absfree (x, T, body) $ tT
    84       else raise TERM ("abs_tr", ts)
    85   | abs_tr (*"_abs"*) ts = raise TERM ("abs_tr", ts);
    86 
    87 
    88 (* nondependent abstraction *)
    89 
    90 fun k_tr (*"_K"*) [t] = Abs ("uu", dummyT, Term.incr_boundvars 1 t)
    91   | k_tr (*"_K"*) ts = raise TERM ("k_tr", ts);
    92 
    93 
    94 (* binder *)
    95 
    96 fun mk_binder_tr (sy, name) =
    97   let
    98     fun tr (Free (x, T), t) = Lexicon.const name $ Term.absfree (x, T, t)
    99       | tr (Const ("_idts", _) $ idt $ idts, t) = tr (idt, tr (idts, t))
   100       | tr (t1 as Const (c, _) $ Free (x, T) $ tT, t) =
   101           if c = SynExt.constrainC then
   102             Lexicon.const name $ (Lexicon.const constrainAbsC $ Term.absfree (x, T, t) $ tT)
   103           else raise TERM ("binder_tr", [t1, t])
   104       | tr (t1, t2) = raise TERM ("binder_tr", [t1, t2]);
   105 
   106     fun binder_tr (*sy*) [idts, body] = tr (idts, body)
   107       | binder_tr (*sy*) ts = raise TERM ("binder_tr", ts);
   108   in
   109     (sy, binder_tr)
   110   end;
   111 
   112 
   113 (* meta propositions *)
   114 
   115 fun aprop_tr (*"_aprop"*) [t] = Lexicon.const SynExt.constrainC $ t $ Lexicon.const "prop"
   116   | aprop_tr (*"_aprop"*) ts = raise TERM ("aprop_tr", ts);
   117 
   118 fun ofclass_tr (*"_ofclass"*) [ty, cls] =
   119       cls $ (Lexicon.const SynExt.constrainC $ Lexicon.const "TYPE" $
   120         (Lexicon.const "itself" $ ty))
   121   | ofclass_tr (*"_ofclass"*) ts = raise TERM ("ofclass_tr", ts);
   122 
   123 
   124 (* meta implication *)
   125 
   126 fun bigimpl_ast_tr (*"_bigimpl"*) [asms, concl] =
   127       Ast.fold_ast_p "==>" (Ast.unfold_ast "_asms" asms, concl)
   128   | bigimpl_ast_tr (*"_bigimpl"*) asts = raise Ast.AST ("bigimpl_ast_tr", asts);
   129 
   130 
   131 (* type reflection *)
   132 
   133 fun type_tr (*"_TYPE"*) [ty] =
   134       Lexicon.const SynExt.constrainC $ Lexicon.const "TYPE" $ (Lexicon.const "itself" $ ty)
   135   | type_tr (*"_TYPE"*) ts = raise TERM ("type_tr", ts);
   136 
   137 
   138 (* dddot *)
   139 
   140 fun dddot_tr (*"_DDDOT"*) ts = Term.list_comb (Lexicon.var SynExt.dddot_indexname, ts);
   141 
   142 
   143 (* quote / antiquote *)
   144 
   145 fun antiquote_tr name =
   146   let
   147     fun tr i ((t as Const (c, _)) $ u) =
   148           if c = name then tr i u $ Bound i
   149           else tr i t $ tr i u
   150       | tr i (t $ u) = tr i t $ tr i u
   151       | tr i (Abs (x, T, t)) = Abs (x, T, tr (i + 1) t)
   152       | tr _ a = a;
   153   in tr 0 end;
   154 
   155 fun quote_tr name t = Abs ("s", dummyT, antiquote_tr name (Term.incr_boundvars 1 t));
   156 
   157 fun quote_antiquote_tr quoteN antiquoteN name =
   158   let
   159     fun tr [t] = Lexicon.const name $ quote_tr antiquoteN t
   160       | tr ts = raise TERM ("quote_tr", ts);
   161   in (quoteN, tr) end;
   162 
   163 
   164 
   165 (** print (ast) translations **)
   166 
   167 (* application *)
   168 
   169 fun appl_ast_tr' (f, []) = raise Ast.AST ("appl_ast_tr'", [f])
   170   | appl_ast_tr' (f, args) = Ast.Appl [Ast.Constant "_appl", f, Ast.fold_ast "_args" args];
   171 
   172 fun applC_ast_tr' (f, []) = raise Ast.AST ("applC_ast_tr'", [f])
   173   | applC_ast_tr' (f, args) = Ast.Appl [Ast.Constant "_applC", f, Ast.fold_ast "_cargs" args];
   174 
   175 
   176 (* abstraction *)
   177 
   178 fun mark_boundT x_T = Lexicon.const "_bound" $ Free x_T;
   179 fun mark_bound x = mark_boundT (x, dummyT);
   180 
   181 fun strip_abss vars_of body_of tm =
   182   let
   183     val vars = vars_of tm;
   184     val body = body_of tm;
   185     val rev_new_vars = rename_wrt_term body vars;
   186   in
   187     (map mark_boundT (rev rev_new_vars),
   188       subst_bounds (map (mark_bound o #1) rev_new_vars, body))
   189   end;
   190 
   191 
   192 (*do (partial) eta-contraction before printing*)
   193 
   194 val eta_contract = ref true;
   195 
   196 fun eta_contr tm =
   197   let
   198     fun is_aprop (Const ("_aprop", _)) = true
   199       | is_aprop _ = false;
   200 
   201     fun eta_abs (Abs (a, T, t)) =
   202           (case eta_abs t of
   203             t' as f $ u =>
   204               (case eta_abs u of
   205                 Bound 0 =>
   206                   if Term.loose_bvar1 (f, 0) orelse is_aprop f then Abs (a, T, t')
   207                   else  incr_boundvars ~1 f
   208               | _ => Abs (a, T, t'))
   209           | t' => Abs (a, T, t'))
   210       | eta_abs t = t;
   211   in
   212     if ! eta_contract then eta_abs tm else tm
   213   end;
   214 
   215 
   216 fun abs_tr' tm =
   217   foldr (fn (x, t) => Lexicon.const "_abs" $ x $ t)
   218     (strip_abss strip_abs_vars strip_abs_body (eta_contr tm));
   219 
   220 
   221 fun abs_ast_tr' (*"_abs"*) asts =
   222   (case Ast.unfold_ast_p "_abs" (Ast.Appl (Ast.Constant "_abs" :: asts)) of
   223     ([], _) => raise Ast.AST ("abs_ast_tr'", asts)
   224   | (xs, body) => Ast.Appl [Ast.Constant "_lambda", Ast.fold_ast "_pttrns" xs, body]);
   225 
   226 
   227 (* binder *)
   228 
   229 fun mk_binder_tr' (name, sy) =
   230   let
   231     fun mk_idts [] = raise Match    (*abort translation*)
   232       | mk_idts [idt] = idt
   233       | mk_idts (idt :: idts) = Lexicon.const "_idts" $ idt $ mk_idts idts;
   234 
   235     fun tr' t =
   236       let
   237         val (xs, bd) = strip_abss (strip_qnt_vars name) (strip_qnt_body name) t;
   238       in Lexicon.const sy $ mk_idts xs $ bd end;
   239 
   240     fun binder_tr' (*name*) (t :: ts) = Term.list_comb (tr' (Lexicon.const name $ t), ts)
   241       | binder_tr' (*name*) [] = raise Match;
   242   in
   243     (name, binder_tr')
   244   end;
   245 
   246 
   247 (* idtyp constraints *)
   248 
   249 fun idtyp_ast_tr' a [Ast.Appl [Ast.Constant c, x, ty], xs] =
   250       if c = SynExt.constrainC then
   251         Ast.Appl [ Ast.Constant a,  Ast.Appl [Ast.Constant "_idtyp", x, ty], xs]
   252       else raise Match
   253   | idtyp_ast_tr' _ _ = raise Match;
   254 
   255 
   256 (* meta propositions *)
   257 
   258 fun prop_tr' tm =
   259   let
   260     fun aprop t = Lexicon.const "_aprop" $ t;
   261 
   262     fun is_prop Ts t =
   263       fastype_of1 (Ts, t) = propT handle TERM _ => false;
   264 
   265     fun tr' _ (t as Const _) = t
   266       | tr' _ (t as Free (x, T)) =
   267           if T = propT then aprop (Lexicon.free x) else t
   268       | tr' _ (t as Var (xi, T)) =
   269           if T = propT then aprop (Lexicon.var xi) else t
   270       | tr' Ts (t as Bound _) =
   271           if is_prop Ts t then aprop t else t
   272       | tr' Ts (Abs (x, T, t)) = Abs (x, T, tr' (T :: Ts) t)
   273       | tr' Ts (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [T])))) =
   274           if is_prop Ts t then Const ("_mk_ofclass", T) $ tr' Ts t1
   275           else tr' Ts t1 $ tr' Ts t2
   276       | tr' Ts (t as t1 $ t2) =
   277           (if is_Const (Term.head_of t) orelse not (is_prop Ts t)
   278             then I else aprop) (tr' Ts t1 $ tr' Ts t2);
   279   in
   280     tr' [] tm
   281   end;
   282 
   283 fun mk_ofclass_tr' show_sorts (*"_mk_ofclass"*) T [t] =
   284       Lexicon.const "_ofclass" $ TypeExt.term_of_typ show_sorts T $ t
   285   | mk_ofclass_tr' _ (*"_mk_ofclass"*) T ts = raise TYPE ("mk_ofclass_tr'", [T], ts);
   286 
   287 
   288 (* meta implication *)
   289 
   290 fun impl_ast_tr' (*"==>"*) asts =
   291   if TypeExt.no_brackets () then raise Match
   292   else
   293     (case Ast.unfold_ast_p "==>" (Ast.Appl (Ast.Constant "==>" :: asts)) of
   294       (asms as _ :: _ :: _, concl)
   295         => Ast.Appl [Ast.Constant "_bigimpl", Ast.fold_ast "_asms" asms, concl]
   296     | _ => raise Match);
   297 
   298 
   299 (* type reflection *)
   300 
   301 fun type_tr' show_sorts (*"TYPE"*) (Type ("itself", [T])) ts =
   302       Term.list_comb (Lexicon.const "_TYPE" $ TypeExt.term_of_typ show_sorts T, ts)
   303   | type_tr' _ _ _ = raise Match;
   304 
   305 
   306 (* dependent / nondependent quantifiers *)
   307 
   308 fun variant_abs' (x, T, B) =
   309   let val x' = variant (add_term_names (B, [])) x in
   310     (x', subst_bound (mark_boundT (x', T), B))
   311   end;
   312 
   313 fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) =
   314       if Term.loose_bvar1 (B, 0) then
   315         let val (x', B') = variant_abs' (x, dummyT, B);
   316         in Term.list_comb (Lexicon.const q $ mark_boundT (x', T) $ A $ B', ts) end
   317       else Term.list_comb (Lexicon.const r $ A $ B, ts)
   318   | dependent_tr' _ _ = raise Match;
   319 
   320 
   321 (* quote / antiquote *)
   322 
   323 fun antiquote_tr' name =
   324   let
   325     fun tr' i (t $ u) =
   326       if u = Bound i then Lexicon.const name $ tr' i t
   327       else tr' i t $ tr' i u
   328       | tr' i (Abs (x, T, t)) = Abs (x, T, tr' (i + 1) t)
   329       | tr' i a = if a = Bound i then raise Match else a;
   330   in tr' 0 end;
   331 
   332 fun quote_tr' name (Abs (_, _, t)) = Term.incr_boundvars ~1 (antiquote_tr' name t)
   333   | quote_tr' _ _ = raise Match;
   334 
   335 fun quote_antiquote_tr' quoteN antiquoteN name =
   336   let
   337     fun tr' (t :: ts) = Term.list_comb (Lexicon.const quoteN $ quote_tr' antiquoteN t, ts)
   338       | tr' _ = raise Match;
   339   in (name, tr') end;
   340 
   341 
   342 
   343 (** pure_trfuns **)
   344 
   345 val pure_trfuns =
   346  ([("_constify", constify_ast_tr), ("_appl", appl_ast_tr), ("_applC", applC_ast_tr),
   347    ("_lambda", lambda_ast_tr), ("_idtyp", idtyp_ast_tr), ("_bigimpl", bigimpl_ast_tr)],
   348   [("_abs", abs_tr), ("_aprop", aprop_tr), ("_ofclass", ofclass_tr),
   349    ("_TYPE", type_tr), ("_DDDOT", dddot_tr), ("_K", k_tr)],
   350   []: (string * (term list -> term)) list,
   351   [("_abs", abs_ast_tr'), ("_idts", idtyp_ast_tr' "_idts"),
   352    ("_pttrns", idtyp_ast_tr' "_pttrns"), ("==>", impl_ast_tr')]);
   353 
   354 val pure_trfunsT =
   355   [("_mk_ofclass", mk_ofclass_tr'), ("TYPE", type_tr')];
   356 
   357 
   358 
   359 (** pt_to_ast **)
   360 
   361 fun pt_to_ast trf pt =
   362   let
   363     fun trans a args =
   364       (case trf a of
   365         None => Ast.mk_appl (Ast.Constant a) args
   366       | Some f => f args handle exn
   367           => (writeln ("Error in parse ast translation for " ^ quote a);
   368               raise exn));
   369 
   370     (*translate pt bottom-up*)
   371     fun ast_of (Parser.Node (a, pts)) = trans a (map ast_of pts)
   372       | ast_of (Parser.Tip tok) = Ast.Variable (Lexicon.str_of_token tok);
   373   in
   374     ast_of pt
   375   end;
   376 
   377 
   378 
   379 (** ast_to_term **)
   380 
   381 fun ast_to_term trf ast =
   382   let
   383     fun trans a args =
   384       (case trf a of
   385         None => Term.list_comb (Lexicon.const a, args)
   386       | Some f => f args handle exn
   387           => (writeln ("Error in parse translation for " ^ quote a);
   388               raise exn));
   389 
   390     fun term_of (Ast.Constant a) = trans a []
   391       | term_of (Ast.Variable x) = Lexicon.read_var x
   392       | term_of (Ast.Appl (Ast.Constant a :: (asts as _ :: _))) =
   393           trans a (map term_of asts)
   394       | term_of (Ast.Appl (ast :: (asts as _ :: _))) =
   395           Term.list_comb (term_of ast, map term_of asts)
   396       | term_of (ast as Ast.Appl _) = raise Ast.AST ("ast_to_term: malformed ast", [ast]);
   397   in
   398     term_of ast
   399   end;
   400 
   401 end;