src/Pure/Syntax/syn_trans.ML
author paulson
Fri Feb 16 17:24:51 1996 +0100 (1996-02-16)
changeset 1511 09354d37a5ab
parent 1326 1fbf9407757c
child 2698 8bccb3ab4ca4
permissions -rw-r--r--
Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.
     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   end;
    15 
    16 signature SYN_TRANS1 =
    17   sig
    18   include SYN_TRANS0
    19   val constrainAbsC: string
    20   val pure_trfuns:
    21       (string * (Ast.ast list -> Ast.ast)) list *
    22       (string * (term list -> term)) list *
    23       (string * (term list -> term)) list *
    24       (string * (Ast.ast list -> Ast.ast)) list
    25   end;
    26 
    27 signature SYN_TRANS =
    28   sig
    29   include SYN_TRANS1
    30   val abs_tr': term -> term
    31   val prop_tr': bool -> term -> term
    32   val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
    33   val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
    34   val pt_to_ast: (string -> (Ast.ast list -> Ast.ast) option) -> Parser.parsetree -> Ast.ast
    35   val ast_to_term: (string -> (term list -> term) option) -> Ast.ast -> term
    36   end;
    37 
    38 structure SynTrans : SYN_TRANS =
    39 struct
    40 open TypeExt Lexicon Ast SynExt Parser;
    41 
    42 (** parse (ast) translations **)
    43 
    44 (* application *)
    45 
    46 fun appl_ast_tr [f, args] = Appl (f :: unfold_ast "_args" args)
    47   | appl_ast_tr asts = raise_ast "appl_ast_tr" asts;
    48 
    49 fun applC_ast_tr [f, args] = Appl (f :: unfold_ast "_cargs" args)
    50   | applC_ast_tr asts = raise_ast "applC_ast_tr" asts;
    51 
    52 
    53 (* abstraction *)
    54 
    55 fun idtyp_ast_tr (*"_idtyp"*) [x, ty] = Appl [Constant constrainC, x, ty]
    56   | idtyp_ast_tr (*"_idtyp"*) asts = raise_ast "idtyp_ast_tr" asts;
    57 
    58 fun lambda_ast_tr (*"_lambda"*) [idts, body] =
    59       fold_ast_p "_abs" (unfold_ast "_idts" idts, body)
    60   | lambda_ast_tr (*"_lambda"*) asts = raise_ast "lambda_ast_tr" asts;
    61 
    62 val constrainAbsC = "_constrainAbs";
    63 
    64 fun abs_tr (*"_abs"*) [Free (x, T), body] = absfree (x, T, body)
    65   | abs_tr (*"_abs"*) (ts as [Const (c, _) $ Free (x, T) $ tT, body]) =
    66       if c = constrainC
    67         then const constrainAbsC $ absfree (x, T, body) $ tT
    68       else raise_term "abs_tr" ts
    69   | abs_tr (*"_abs"*) ts = raise_term "abs_tr" ts;
    70 
    71 
    72 (* nondependent abstraction *)
    73 
    74 fun k_tr (*"_K"*) [t] = Abs ("uu", dummyT, incr_boundvars 1 t)
    75   | k_tr (*"_K"*) ts = raise_term "k_tr" ts;
    76 
    77 
    78 (* binder *)
    79 
    80 fun mk_binder_tr (sy, name) =
    81   let
    82     fun tr (Free (x, T), t) = const name $ absfree (x, T, t)
    83       | tr (Const ("_idts", _) $ idt $ idts, t) = tr (idt, tr (idts, t))
    84       | tr (t1 as Const (c, _) $ Free (x, T) $ tT, t) =
    85           if c = constrainC then
    86             const name $ (const constrainAbsC $ absfree (x, T, t) $ tT)
    87           else raise_term "binder_tr" [t1, t]
    88       | tr (t1, t2) = raise_term "binder_tr" [t1, t2];
    89 
    90     fun binder_tr (*sy*) [idts, body] = tr (idts, body)
    91       | binder_tr (*sy*) ts = raise_term "binder_tr" ts;
    92   in
    93     (sy, binder_tr)
    94   end;
    95 
    96 
    97 (* meta propositions *)
    98 
    99 fun aprop_tr (*"_aprop"*) [t] = const constrainC $ t $ const "prop"
   100   | aprop_tr (*"_aprop"*) ts = raise_term "aprop_tr" ts;
   101 
   102 fun ofclass_tr (*"_ofclass"*) [ty, cls] =
   103       cls $ (const constrainC $ const "TYPE" $ (const "itself" $ ty))
   104   | ofclass_tr (*"_ofclass"*) ts = raise_term "ofclass_tr" ts;
   105 
   106 
   107 (* meta implication *)
   108 
   109 fun bigimpl_ast_tr (*"_bigimpl"*) [asms, concl] =
   110       fold_ast_p "==>" (unfold_ast "_asms" asms, concl)
   111   | bigimpl_ast_tr (*"_bigimpl"*) asts = raise_ast "bigimpl_ast_tr" asts;
   112 
   113 
   114 
   115 (** print (ast) translations **)
   116 
   117 (* application *)
   118 
   119 fun appl_ast_tr' (f, []) = raise_ast "appl_ast_tr'" [f]
   120   | appl_ast_tr' (f, args) = Appl [Constant "_appl", f, fold_ast "_args" args];
   121 
   122 fun applC_ast_tr' (f, []) = raise_ast "applC_ast_tr'" [f]
   123   | applC_ast_tr' (f, args) =
   124       Appl [Constant "_applC", f, fold_ast "_cargs" args];
   125 
   126 
   127 (* abstraction *)
   128 
   129 fun strip_abss vars_of body_of tm =
   130   let
   131     val vars = vars_of tm;
   132     val body = body_of tm;
   133     val rev_new_vars = rename_wrt_term body vars;
   134   in
   135     (map Free (rev rev_new_vars),
   136       subst_bounds (map (free o #1) rev_new_vars, body))
   137   end;
   138 
   139 (*do (partial) eta-contraction before printing*)
   140 
   141 val eta_contract = ref true;
   142 
   143 fun eta_contr tm =
   144   let
   145     fun eta_abs (Abs (a, T, t)) =
   146           (case eta_abs t of
   147             t' as f $ u =>
   148               (case eta_abs u of
   149                 Bound 0 =>
   150                   if not (0 mem loose_bnos f) then incr_boundvars ~1 f
   151                   else Abs (a, T, t')
   152               | _ => Abs (a, T, t'))
   153           | t' => Abs (a, T, t'))
   154       | eta_abs t = t;
   155   in
   156     if ! eta_contract then eta_abs tm else tm
   157   end;
   158 
   159 
   160 fun abs_tr' tm =
   161   foldr (fn (x, t) => const "_abs" $ x $ t)
   162     (strip_abss strip_abs_vars strip_abs_body (eta_contr tm));
   163 
   164 
   165 fun abs_ast_tr' (*"_abs"*) asts =
   166   (case unfold_ast_p "_abs" (Appl (Constant "_abs" :: asts)) of
   167     ([], _) => raise_ast "abs_ast_tr'" asts
   168   | (xs, body) => Appl [Constant "_lambda", fold_ast "_idts" xs, body]);
   169 
   170 
   171 (* binder *)
   172 
   173 fun mk_binder_tr' (name, sy) =
   174   let
   175     fun mk_idts [] = raise Match    (*abort translation*)
   176       | mk_idts [idt] = idt
   177       | mk_idts (idt :: idts) = const "_idts" $ idt $ mk_idts idts;
   178 
   179     fun tr' t =
   180       let
   181         val (xs, bd) = strip_abss (strip_qnt_vars name) (strip_qnt_body name) t;
   182       in
   183         const sy $ mk_idts xs $ bd
   184       end;
   185 
   186     fun binder_tr' (*name*) (t :: ts) =
   187           list_comb (tr' (const name $ t), ts)
   188       | binder_tr' (*name*) [] = raise Match;
   189   in
   190     (name, binder_tr')
   191   end;
   192 
   193 
   194 (* idts *)
   195 
   196 fun idts_ast_tr' (*"_idts"*) [Appl [Constant c, x, ty], xs] =
   197       if c = constrainC then
   198         Appl [Constant "_idts", Appl [Constant "_idtyp", x, ty], xs]
   199       else raise Match
   200   | idts_ast_tr' (*"_idts"*) _ = raise Match;
   201 
   202 
   203 (* meta propositions *)
   204 
   205 fun prop_tr' show_sorts tm =
   206   let
   207     fun aprop t = const "_aprop" $ t;
   208 
   209     fun is_prop tys t =
   210       fastype_of1 (tys, t) = propT handle TERM _ => false;
   211 
   212     fun tr' _ (t as Const _) = t
   213       | tr' _ (t as Free (x, ty)) =
   214           if ty = propT then aprop (free x) else t
   215       | tr' _ (t as Var (xi, ty)) =
   216           if ty = propT then aprop (var xi) else t
   217       | tr' tys (t as Bound _) =
   218           if is_prop tys t then aprop t else t
   219       | tr' tys (Abs (x, ty, t)) = Abs (x, ty, tr' (ty :: tys) t)
   220       | tr' tys (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [ty])))) =
   221           if is_prop tys t then
   222             const "_ofclass" $ term_of_typ show_sorts ty $ tr' tys t1
   223           else tr' tys t1 $ tr' tys t2
   224       | tr' tys (t as t1 $ t2) =
   225           (if is_Const (head_of t) orelse not (is_prop tys t)
   226             then I else aprop) (tr' tys t1 $ tr' tys t2);
   227   in
   228     tr' [] tm
   229   end;
   230 
   231 
   232 (* meta implication *)
   233 
   234 fun impl_ast_tr' (*"==>"*) asts =
   235   (case unfold_ast_p "==>" (Appl (Constant "==>" :: asts)) of
   236     (asms as _ :: _ :: _, concl)
   237       => Appl [Constant "_bigimpl", fold_ast "_asms" asms, concl]
   238   | _ => raise Match);
   239 
   240 
   241 (* dependent / nondependent quantifiers *)
   242 
   243 fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) =
   244       if 0 mem (loose_bnos B) then
   245         let val (x', B') = variant_abs (x, dummyT, B);
   246         in list_comb (const q $ Free (x', T) $ A $ B', ts) end
   247       else list_comb (const r $ A $ B, ts)
   248   | dependent_tr' _ _ = raise Match;
   249 
   250 
   251 
   252 (** pure_trfuns **)
   253 
   254 val pure_trfuns =
   255  ([("_appl", appl_ast_tr), ("_applC", applC_ast_tr),
   256    ("_lambda", lambda_ast_tr), ("_idtyp", idtyp_ast_tr),
   257    ("_bigimpl", bigimpl_ast_tr)],
   258   [("_abs", abs_tr), ("_aprop", aprop_tr), ("_ofclass", ofclass_tr),
   259    ("_K", k_tr)],
   260   [],
   261   [("_abs", abs_ast_tr'), ("_idts", idts_ast_tr'), ("==>", impl_ast_tr')]);
   262 
   263 
   264 
   265 (** pt_to_ast **)
   266 
   267 fun pt_to_ast trf pt =
   268   let
   269     fun trans a args =
   270       (case trf a of
   271         None => mk_appl (Constant a) args
   272       | Some f => f args handle exn
   273           => (writeln ("Error in parse ast translation for " ^ quote a);
   274               raise exn));
   275 
   276     (*translate pt bottom-up*)
   277     fun ast_of (Node (a, pts)) = trans a (map ast_of pts)
   278       | ast_of (Tip tok) = Variable (str_of_token tok);
   279   in
   280     ast_of pt
   281   end;
   282 
   283 
   284 
   285 (** ast_to_term **)
   286 
   287 fun ast_to_term trf ast =
   288   let
   289     fun trans a args =
   290       (case trf a of
   291         None => list_comb (const a, args)
   292       | Some f => f args handle exn
   293           => (writeln ("Error in parse translation for " ^ quote a);
   294               raise exn));
   295 
   296     fun term_of (Constant a) = trans a []
   297       | term_of (Variable x) = scan_var x
   298       | term_of (Appl (Constant a :: (asts as _ :: _))) =
   299           trans a (map term_of asts)
   300       | term_of (Appl (ast :: (asts as _ :: _))) =
   301           list_comb (term_of ast, map term_of asts)
   302       | term_of (ast as Appl _) = raise_ast "ast_to_term: malformed ast" [ast];
   303   in
   304     term_of ast
   305   end;
   306 
   307 end;