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