wneuper/isa: src/Pure/Syntax/syn_trans.ML@d87a8838afa4

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

     2     ID:         $Id$

     3     Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen

     5 Syntax translation functions.

     6 *)

     8 signature SYN_TRANS0 =

     9 sig

    10   val eta_contract: bool ref

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

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

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

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

    15   val antiquote_tr: string -> term -> term

    16   val quote_tr: string -> term -> term

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

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

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

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

    21   val mark_bound: string -> term

    22   val mark_boundT: string * typ -> term

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

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

    25 end;

    27 signature SYN_TRANS1 =

    28 sig

    29   include SYN_TRANS0

    30   val non_typed_tr': (term list -> term) -> bool -> typ -> term list -> term

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

    32   val constrainAbsC: string

    33   val pure_trfuns:

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

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

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

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

    38   val pure_trfunsT: (string * (bool -> typ -> term list -> term)) list

    39   val struct_trfuns: string list ->

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

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

    42       (string * (bool -> typ -> term list -> term)) list *

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

    44 end;

    46 signature SYN_TRANS =

    47 sig

    48   include SYN_TRANS1

    49   val abs_tr': term -> term

    50   val prop_tr': term -> term

    51   val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast

    52   val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast

    53   val pts_to_asts: Context.generic ->

    54     (string -> (Context.generic -> Ast.ast list -> Ast.ast) option) ->

    55     Parser.parsetree list -> Ast.ast list

    56   val asts_to_terms: Context.generic ->

    57     (string -> (Context.generic -> term list -> term) option) -> Ast.ast list -> term list

    58 end;

    60 structure SynTrans: SYN_TRANS =

    61 struct

    64 (** parse (ast) translations **)

    66 (* constify *)

    68 fun constify_ast_tr [Ast.Variable c] = Ast.Constant c

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

    72 (* application *)

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

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

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

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

    81 (* abstraction *)

    83 fun idtyp_ast_tr (*"_idtyp"*) [x, ty] = Ast.Appl [Ast.Constant "_constrain", x, ty]

    84   | idtyp_ast_tr (*"_idtyp"*) asts = raise Ast.AST ("idtyp_ast_tr", asts);

    86 fun idtypdummy_ast_tr (*"_idtypdummy"*) [ty] =

    87       Ast.Appl [Ast.Constant "_constrain", Ast.Constant "_idtdummy", ty]

    88   | idtypdummy_ast_tr (*"_idtypdummy"*) asts = raise Ast.AST ("idtyp_ast_tr", asts);

    90 fun lambda_ast_tr (*"_lambda"*) [pats, body] =

    91       Ast.fold_ast_p "_abs" (Ast.unfold_ast "_pttrns" pats, body)

    92   | lambda_ast_tr (*"_lambda"*) asts = raise Ast.AST ("lambda_ast_tr", asts);

    94 val constrainAbsC = "_constrainAbs";

    96 fun abs_tr (*"_abs"*) [Free (x, T), t] = Term.absfree (x, T, t)

    97   | abs_tr (*"_abs"*) [Const ("_idtdummy", T), t] = Term.absdummy (T, t)

    98   | abs_tr (*"_abs"*) [Const ("_constrain", _) $ Free (x, T) $ tT, t] =

    99       Lexicon.const constrainAbsC $ Term.absfree (x, T, t) $ tT

   100   | abs_tr (*"_abs"*) [Const ("_constrain", _) $ Const ("_idtdummy", T) $ tT, t] =

   101       Lexicon.const constrainAbsC $ Term.absdummy (T, t) $ tT

   102   | abs_tr (*"_abs"*) ts = raise TERM ("abs_tr", ts);

   105 (* binder *)

   107 fun mk_binder_tr (sy, name) =

   108   let

   109     fun tr (Free (x, T), t) = Lexicon.const name $ Term.absfree (x, T, t)

   110       | tr (Const ("_idtdummy", T), t) = Lexicon.const name $ Term.absdummy (T, t)

   111       | tr (Const ("_constrain", _) $ Free (x, T) $ tT, t) =

   112           Lexicon.const name $ (Lexicon.const constrainAbsC $ Term.absfree (x, T, t) $ tT)

   113       | tr (Const ("_constrain", _) $ Const ("_idtdummy", T) $ tT, t) =

   114           Lexicon.const name $ (Lexicon.const constrainAbsC $ Term.absdummy (T, t) $ tT)

   115       | tr (Const ("_idts", _) $ idt $ idts, t) = tr (idt, tr (idts, t))

   116       | tr (t1, t2) = raise TERM ("binder_tr", [t1, t2]);

   118     fun binder_tr (*sy*) [idts, body] = tr (idts, body)

   119       | binder_tr (*sy*) ts = raise TERM ("binder_tr", ts);

   120   in (sy, binder_tr) end;

   123 (* meta propositions *)

   125 fun aprop_tr (*"_aprop"*) [t] = Lexicon.const "_constrain" $ t $ Lexicon.const "prop"

   126   | aprop_tr (*"_aprop"*) ts = raise TERM ("aprop_tr", ts);

   128 fun ofclass_tr (*"_ofclass"*) [ty, cls] =

   129       cls $ (Lexicon.const "_constrain" $ Lexicon.const "TYPE" $

   130         (Lexicon.const "itself" $ ty))

   131   | ofclass_tr (*"_ofclass"*) ts = raise TERM ("ofclass_tr", ts);

   134 (* meta implication *)

   136 fun bigimpl_ast_tr (*"_bigimpl"*) (asts as [asms, concl]) =

   137       let val prems =

   138         (case Ast.unfold_ast_p "_asms" asms of

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

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

   141       in Ast.fold_ast_p "==>" (prems, concl) end

   142   | bigimpl_ast_tr (*"_bigimpl"*) asts = raise Ast.AST ("bigimpl_ast_tr", asts);

   145 (* type reflection *)

   147 fun type_tr (*"_TYPE"*) [ty] =

   148       Lexicon.const "_constrain" $ Lexicon.const "TYPE" $ (Lexicon.const "itself" $ ty)

   149   | type_tr (*"_TYPE"*) ts = raise TERM ("type_tr", ts);

   152 (* dddot *)

   154 fun dddot_tr (*"_DDDOT"*) ts = Term.list_comb (Lexicon.var SynExt.dddot_indexname, ts);

   157 (* quote / antiquote *)

   159 fun antiquote_tr name =

   160   let

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

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

   163           else tr i t $ tr i u

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

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

   166       | tr _ a = a;

   167   in tr 0 end;

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

   171 fun quote_antiquote_tr quoteN antiquoteN name =

   172   let

   173     fun tr [t] = Lexicon.const name $ quote_tr antiquoteN t

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

   175   in (quoteN, tr) end;

   178 (* indexed syntax *)

   180 fun struct_ast_tr (*"_struct"*) [Ast.Appl [Ast.Constant "_index", ast]] = ast

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

   183 fun index_ast_tr ast =

   184   Ast.mk_appl (Ast.Constant "_index") [Ast.mk_appl (Ast.Constant "_struct") [ast]];

   186 fun indexdefault_ast_tr (*"_indexdefault"*) [] =

   187       index_ast_tr (Ast.Constant "_indexdefault")

   188   | indexdefault_ast_tr (*"_indexdefault"*) asts =

   189       raise Ast.AST ("indexdefault_ast_tr", asts);

   191 fun indexnum_ast_tr (*"_indexnum"*) [ast] =

   192       index_ast_tr (Ast.mk_appl (Ast.Constant "_indexnum") [ast])

   193   | indexnum_ast_tr (*"_indexnum"*) asts = raise Ast.AST ("indexnum_ast_tr", asts);

   195 fun indexvar_ast_tr (*"_indexvar"*) [] =

   196       Ast.mk_appl (Ast.Constant "_index") [Ast.Variable "some_index"]

   197   | indexvar_ast_tr (*"_indexvar"*) asts = raise Ast.AST ("indexvar_ast_tr", asts);

   199 fun index_tr (*"_index"*) [t] = t

   200   | index_tr (*"_index"*) ts = raise TERM ("index_tr", ts);

   203 (* implicit structures *)

   205 fun the_struct structs i =

   206   if 1 <= i andalso i <= length structs then List.nth (structs, i - 1)

   207   else raise error ("Illegal reference to implicit structure #" ^ string_of_int i);

   209 fun struct_tr structs (*"_struct"*) [Const ("_indexdefault", _)] =

   210       Lexicon.free (the_struct structs 1)

   211   | struct_tr structs (*"_struct"*) [t as (Const ("_indexnum", _) $ Const (s, _))] =

   212       Lexicon.free (the_struct structs

   213         (case Lexicon.read_nat s of SOME n => n | NONE => raise TERM ("struct_tr", [t])))

   214   | struct_tr _ (*"_struct"*) ts = raise TERM ("struct_tr", ts);

   218 (** print (ast) translations **)

   220 (* types *)

   222 fun non_typed_tr' f _ _ ts = f ts;

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

   226 (* application *)

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

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

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

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

   235 (* abstraction *)

   237 fun mark_boundT (x, T) = Const ("_bound", T --> T) $ Free (x, T);

   238 fun mark_bound x = mark_boundT (x, dummyT);

   240 fun bound_vars vars body =

   241   subst_bounds (map mark_boundT (Term.rename_wrt_term body vars), body);

   243 fun strip_abss vars_of body_of tm =

   244   let

   245     val vars = vars_of tm;

   246     val body = body_of tm;

   247     val rev_new_vars = rename_wrt_term body vars;

   248   in

   249     (map mark_boundT (rev rev_new_vars),

   250       subst_bounds (map (mark_bound o #1) rev_new_vars, body))

   251   end;

   254 (*do (partial) eta-contraction before printing*)

   256 val eta_contract = ref true;

   258 fun eta_contr tm =

   259   let

   260     fun is_aprop (Const ("_aprop", _)) = true

   261       | is_aprop _ = false;

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

   264           (case eta_abs t of

   265             t' as f $ u =>

   266               (case eta_abs u of

   267                 Bound 0 =>

   268                   if Term.loose_bvar1 (f, 0) orelse is_aprop f then Abs (a, T, t')

   269                   else  incr_boundvars ~1 f

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

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

   272       | eta_abs t = t;

   273   in

   274     if ! eta_contract then eta_abs tm else tm

   275   end;

   278 fun abs_tr' tm =

   279   uncurry (fold_rev (fn x => fn t => Lexicon.const "_abs" $ x $ t))

   280     (strip_abss strip_abs_vars strip_abs_body (eta_contr tm));

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

   283   let val [xT] = rename_wrt_term t [(x, T)]

   284   in (mark_boundT xT, subst_bound (mark_bound (fst xT), t)) end;

   286 fun abs_ast_tr' (*"_abs"*) asts =

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

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

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

   292 (* binder *)

   294 fun mk_binder_tr' (name, sy) =

   295   let

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

   297       | mk_idts [idt] = idt

   298       | mk_idts (idt :: idts) = Lexicon.const "_idts" $ idt $ mk_idts idts;

   300     fun tr' t =

   301       let

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

   303       in Lexicon.const sy $ mk_idts xs $ bd end;

   305     fun binder_tr' (*name*) (t :: ts) = Term.list_comb (tr' (Lexicon.const name $ t), ts)

   306       | binder_tr' (*name*) [] = raise Match;

   307   in

   308     (name, binder_tr')

   309   end;

   312 (* idtyp constraints *)

   314 fun idtyp_ast_tr' a [Ast.Appl [Ast.Constant c, x, ty], xs] =

   315       if c = "_constrain" then

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

   317       else raise Match

   318   | idtyp_ast_tr' _ _ = raise Match;

   321 (* meta propositions *)

   323 fun prop_tr' tm =

   324   let

   325     fun aprop t = Lexicon.const "_aprop" $ t;

   327     fun is_prop Ts t =

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

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

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

   332           if is_prop Ts u then aprop t else t

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

   334           if T = propT then aprop (Lexicon.free x) else t

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

   336           if T = propT then aprop (Lexicon.var xi) else t

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

   338           if is_prop Ts t then aprop t else t

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

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

   341           if is_prop Ts t then Const ("_mk_ofclass", T) $ tr' Ts t1

   342           else tr' Ts t1 $ tr' Ts t2

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

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

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

   346   in tr' [] tm end;

   348 fun mk_ofclass_tr' show_sorts (*"_mk_ofclass"*) T [t] =

   349       Lexicon.const "_ofclass" $ TypeExt.term_of_typ show_sorts T $ t

   350   | mk_ofclass_tr' _ (*"_mk_ofclass"*) T ts = raise TYPE ("mk_ofclass_tr'", [T], ts);

   353 (* meta implication *)

   355 fun impl_ast_tr' (*"==>"*) asts =

   356   if TypeExt.no_brackets () then raise Match

   357   else

   358     (case Ast.unfold_ast_p "==>" (Ast.Appl (Ast.Constant "==>" :: asts)) of

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

   360         let

   361           val (asms, asm) = split_last prems;

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

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

   364     | _ => raise Match);

   367 (* type reflection *)

   369 fun type_tr' show_sorts (*"TYPE"*) (Type ("itself", [T])) ts =

   370       Term.list_comb (Lexicon.const "_TYPE" $ TypeExt.term_of_typ show_sorts T, ts)

   371   | type_tr' _ _ _ = raise Match;

   374 (* dependent / nondependent quantifiers *)

   376 fun variant_abs' (x, T, B) =

   377   let val x' = variant (add_term_names (B, [])) x in

   378     (x', subst_bound (mark_boundT (x', T), B))

   379   end;

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

   382       if Term.loose_bvar1 (B, 0) then

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

   384         in Term.list_comb (Lexicon.const q $ mark_boundT (x', T) $ A $ B', ts) end

   385       else Term.list_comb (Lexicon.const r $ A $ B, ts)

   386   | dependent_tr' _ _ = raise Match;

   389 (* quote / antiquote *)

   391 fun antiquote_tr' name =

   392   let

   393     fun tr' i (t $ u) =

   394       if u aconv Bound i then Lexicon.const name $ tr' i t

   395       else tr' i t $ tr' i u

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

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

   398   in tr' 0 end;

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

   401   | quote_tr' _ _ = raise Match;

   403 fun quote_antiquote_tr' quoteN antiquoteN name =

   404   let

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

   406       | tr' _ = raise Match;

   407   in (name, tr') end;

   410 (* indexed syntax *)

   412 fun index_ast_tr' (*"_index"*) [Ast.Appl [Ast.Constant "_struct", ast]] = ast

   413   | index_ast_tr' _ = raise Match;

   416 (* implicit structures *)

   418 fun the_struct' structs s =

   419   [(case Lexicon.read_nat s of

   420     SOME i => Ast.Variable (the_struct structs i handle ERROR _ => raise Match)

   421   | NONE => raise Match)] |> Ast.mk_appl (Ast.Constant "_free");

   423 fun struct_ast_tr' structs (*"_struct"*) [Ast.Constant "_indexdefault"] =

   424       the_struct' structs "1"

   425   | struct_ast_tr' structs (*"_struct"*) [Ast.Appl [Ast.Constant "_indexnum", Ast.Constant s]] =

   426       the_struct' structs s

   427   | struct_ast_tr' _ _ = raise Match;

   431 (** Pure translations **)

   433 val pure_trfuns =

   434  ([("_constify", constify_ast_tr), ("_appl", appl_ast_tr), ("_applC", applC_ast_tr),

   435    ("_lambda", lambda_ast_tr), ("_idtyp", idtyp_ast_tr), ("_idtypdummy", idtypdummy_ast_tr),

   436    ("_bigimpl", bigimpl_ast_tr), ("_indexdefault", indexdefault_ast_tr),

   437    ("_indexnum", indexnum_ast_tr), ("_indexvar", indexvar_ast_tr), ("_struct", struct_ast_tr)],

   438   [("_abs", abs_tr), ("_aprop", aprop_tr), ("_ofclass", ofclass_tr),

   439    ("_TYPE", type_tr), ("_DDDOT", dddot_tr),

   440    ("_index", index_tr)],

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

   442   [("_abs", abs_ast_tr'), ("_idts", idtyp_ast_tr' "_idts"),

   443    ("_pttrns", idtyp_ast_tr' "_pttrns"), ("==>", impl_ast_tr'),

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

   446 val pure_trfunsT =

   447   [("_mk_ofclass", mk_ofclass_tr'), ("TYPE", type_tr')];

   449 fun struct_trfuns structs =

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

   454 (** pts_to_asts **)

   456 fun pts_to_asts context trf pts =

   457   let

   458     fun trans a args =

   459       (case trf a of

   460         NONE => Ast.mk_appl (Ast.Constant a) args

   461       | SOME f => transform_failure (fn exn =>

   462             EXCEPTION (exn, "Error in parse ast translation for " ^ quote a))

   463           (fn () => f context args) ());

   465     (*translate pt bottom-up*)

   466     fun ast_of (Parser.Node (a, pts)) = trans a (map ast_of pts)

   467       | ast_of (Parser.Tip tok) = Ast.Variable (Lexicon.str_of_token tok);

   469     val exn_results = map (capture ast_of) pts;

   470     val exns = List.mapPartial get_exn exn_results;

   471     val results = List.mapPartial get_result exn_results

   472   in (case (results, exns) of ([], exn :: _) => raise exn | _ => results) end;

   476 (** asts_to_terms **)

   478 fun asts_to_terms context trf asts =

   479   let

   480     fun trans a args =

   481       (case trf a of

   482         NONE => Term.list_comb (Lexicon.const a, args)

   483       | SOME f => transform_failure (fn exn =>

   484             EXCEPTION (exn, "Error in parse translation for " ^ quote a))

   485           (fn () => f context args) ());

   487     fun term_of (Ast.Constant a) = trans a []

   488       | term_of (Ast.Variable x) = Lexicon.read_var x

   489       | term_of (Ast.Appl (Ast.Constant a :: (asts as _ :: _))) =

   490           trans a (map term_of asts)

   491       | term_of (Ast.Appl (ast :: (asts as _ :: _))) =

   492           Term.list_comb (term_of ast, map term_of asts)

   493       | term_of (ast as Ast.Appl _) = raise Ast.AST ("ast_to_term: malformed ast", [ast]);

   495     val free_fixed = Term.map_aterms

   496       (fn t as Const (c, T) =>

   497           (case try (unprefix Lexicon.fixedN) c of

   498             NONE => t

   499           | SOME x => Free (x, T))

   500         | t => t);

   502     val exn_results = map (capture (term_of #> free_fixed)) asts;

   503     val exns = List.mapPartial get_exn exn_results;

   504     val results = List.mapPartial get_result exn_results

   505   in (case (results, exns) of ([], exn :: _) => raise exn | _ => results) end;

   507 end;

author	wenzelm
	Wed, 26 Apr 2006 22:38:05 +0200
changeset 19473	d87a8838afa4
parent 19311	e3d48fa3908e
child 19482	9f11af8f7ef9
permissions	-rw-r--r--