author | berghofe |
Fri, 16 Jul 1999 14:06:13 +0200 | |
changeset 7020 | 75ff179df7b7 |
parent 473 | fdacecc688a1 |
permissions | -rw-r--r-- |
(* Title: Pure/Syntax/sextension.ML ID: $Id$ Author: Tobias Nipkow and Markus Wenzel, TU Muenchen Syntax extensions (external interface): mixfix declarations, infixes, binders, translation rules / functions and the Pure syntax. TODO: move ast_to_term, pt_to_ast (?) *) infix |-> <-| <->; signature SEXTENSION0 = sig structure Parser: PARSER local open Parser.SynExt.Ast in datatype mixfix = Mixfix of string * string * string * int list * int | Delimfix of string * string * string | Infixl of string * string * int | Infixr of string * string * int | Binder of string * string * string * int * int | TInfixl of string * string * int | TInfixr of string * string * int datatype xrule = op |-> of (string * string) * (string * string) | op <-| of (string * string) * (string * string) | op <-> of (string * string) * (string * string) datatype sext = Sext of { mixfix: mixfix list, parse_translation: (string * (term list -> term)) list, print_translation: (string * (term list -> term)) list} | NewSext of { mixfix: mixfix list, xrules: xrule list, parse_ast_translation: (string * (ast list -> ast)) list, parse_translation: (string * (term list -> term)) list, print_translation: (string * (term list -> term)) list, print_ast_translation: (string * (ast list -> ast)) list} val eta_contract: bool ref val mk_binder_tr: string * string -> string * (term list -> term) val mk_binder_tr': string * string -> string * (term list -> term) val dependent_tr': string * string -> term list -> term val max_pri: int end end; signature SEXTENSION1 = sig include SEXTENSION0 local open Parser.SynExt.Ast in val empty_sext: sext val simple_sext: mixfix list -> sext val constants: sext -> (string list * string) list val pure_sext: sext val syntax_types: string list val syntax_consts: (string list * string) list val constrainAbsC: string val pure_trfuns: (string * (ast list -> ast)) list * (string * (term list -> term)) list * (string * (term list -> term)) list * (string * (ast list -> ast)) list end end; signature SEXTENSION = sig include SEXTENSION1 local open Parser Parser.SynExt Parser.SynExt.Ast in val xrules_of: sext -> xrule list val abs_tr': term -> term val prop_tr': bool -> term -> term val appl_ast_tr': ast * ast list -> ast val syn_ext_of_sext: string list -> string list -> string list -> (string -> typ) -> sext -> syn_ext val pt_to_ast: (string -> (ast list -> ast) option) -> parsetree -> ast val ast_to_term: (string -> (term list -> term) option) -> ast -> term end end; functor SExtensionFun(structure TypeExt: TYPE_EXT and Parser: PARSER sharing TypeExt.SynExt = Parser.SynExt): SEXTENSION = struct structure Parser = Parser; open TypeExt Parser.Lexicon Parser.SynExt.Ast Parser.SynExt Parser; (** datatype sext **) (* FIXME remove *) datatype mixfix = Mixfix of string * string * string * int list * int | Delimfix of string * string * string | Infixl of string * string * int | Infixr of string * string * int | Binder of string * string * string * int * int | TInfixl of string * string * int | TInfixr of string * string * int; (* FIXME -> syntax.ML, BASIC_SYNTAX, SYNTAX *) datatype xrule = op |-> of (string * string) * (string * string) | op <-| of (string * string) * (string * string) | op <-> of (string * string) * (string * string); datatype sext = Sext of { mixfix: mixfix list, parse_translation: (string * (term list -> term)) list, print_translation: (string * (term list -> term)) list} | NewSext of { mixfix: mixfix list, xrules: xrule list, parse_ast_translation: (string * (ast list -> ast)) list, parse_translation: (string * (term list -> term)) list, print_translation: (string * (term list -> term)) list, print_ast_translation: (string * (ast list -> ast)) list}; (* simple_sext *) fun simple_sext mixfix = Sext {mixfix = mixfix, parse_translation = [], print_translation = []}; (* empty_sext *) val empty_sext = simple_sext []; (* sext_components *) fun sext_components (Sext {mixfix, parse_translation, print_translation}) = {mixfix = mixfix, xrules = [], parse_ast_translation = [], parse_translation = parse_translation, print_translation = print_translation, print_ast_translation = []} | sext_components (NewSext cmps) = cmps; (* mixfix_of *) fun mixfix_of (Sext {mixfix, ...}) = mixfix | mixfix_of (NewSext {mixfix, ...}) = mixfix; (* xrules_of *) fun xrules_of (Sext _) = [] | xrules_of (NewSext {xrules, ...}) = xrules; (*** translation functions ***) (* FIXME -> trans.ML *) fun const c = Const (c, dummyT); (** parse (ast) translations **) (* application *) fun appl_ast_tr (*"_appl"*) [f, args] = Appl (f :: unfold_ast "_args" args) | appl_ast_tr (*"_appl"*) asts = raise_ast "appl_ast_tr" asts; (* abstraction *) fun idtyp_ast_tr (*"_idtyp"*) [x, ty] = Appl [Constant constrainC, x, ty] | idtyp_ast_tr (*"_idtyp"*) asts = raise_ast "idtyp_ast_tr" asts; fun lambda_ast_tr (*"_lambda"*) [idts, body] = fold_ast_p "_abs" (unfold_ast "_idts" idts, body) | lambda_ast_tr (*"_lambda"*) asts = raise_ast "lambda_ast_tr" asts; fun abs_tr (*"_abs"*) [Free (x, T), body] = absfree (x, T, body) | abs_tr (*"_abs"*) (ts as [Const (c, _) $ Free (x, T) $ tT, body]) = if c = constrainC then const "_constrainAbs" $ absfree (x, T, body) $ tT else raise_term "abs_tr" ts | abs_tr (*"_abs"*) ts = raise_term "abs_tr" ts; (* nondependent abstraction *) fun k_tr (*"_K"*) [t] = Abs ("uu", dummyT, incr_boundvars 1 t) | k_tr (*"_K"*) ts = raise_term "k_tr" ts; (* binder *) fun mk_binder_tr (sy, name) = let fun tr (Free (x, T), t) = const name $ absfree (x, T, t) | tr (Const ("_idts", _) $ idt $ idts, t) = tr (idt, tr (idts, t)) | tr (t1 as Const (c, _) $ Free (x, T) $ tT, t) = if c = constrainC then const name $ (const "_constrainAbs" $ absfree (x, T, t) $ tT) else raise_term "binder_tr" [t1, t] | tr (t1, t2) = raise_term "binder_tr" [t1, t2]; fun binder_tr (*sy*) [idts, body] = tr (idts, body) | binder_tr (*sy*) ts = raise_term "binder_tr" ts; in (sy, binder_tr) end; (* meta propositions *) fun aprop_tr (*"_aprop"*) [t] = const constrainC $ t $ const "prop" | aprop_tr (*"_aprop"*) ts = raise_term "aprop_tr" ts; fun ofclass_tr (*"_ofclass"*) [ty, cls] = cls $ (const constrainC $ const "TYPE" $ (const "itself" $ ty)) | ofclass_tr (*"_ofclass"*) ts = raise_term "ofclass_tr" ts; (* meta implication *) fun bigimpl_ast_tr (*"_bigimpl"*) [asms, concl] = fold_ast_p "==>" (unfold_ast "_asms" asms, concl) | bigimpl_ast_tr (*"_bigimpl"*) asts = raise_ast "bigimpl_ast_tr" asts; (* explode atoms *) fun explode_tr (*"_explode"*) (ts as [consC, nilC, bit0, bit1, txt]) = let fun mk_list [] = nilC | mk_list (t :: ts) = consC $ t $ mk_list ts; fun encode_bit 0 = bit0 | encode_bit 1 = bit1 | encode_bit _ = sys_error "encode_bit"; fun encode_char c = (* FIXME leading 0s (?) *) mk_list (map encode_bit (radixpand (2, (ord c)))); val str = (case txt of Free (s, _) => s | Const (s, _) => s | _ => raise_term "explode_tr" ts); in mk_list (map encode_char (explode str)) end | explode_tr (*"_explode"*) ts = raise_term "explode_tr" ts; (** print (ast) translations **) (* application *) fun appl_ast_tr' (f, []) = raise_ast "appl_ast_tr'" [f] | appl_ast_tr' (f, args) = Appl [Constant "_appl", f, fold_ast "_args" args]; (* abstraction *) fun strip_abss vars_of body_of tm = let fun free (x, _) = Free (x, dummyT); val vars = vars_of tm; val body = body_of tm; val rev_new_vars = rename_wrt_term body vars; in (map Free (rev rev_new_vars), subst_bounds (map free rev_new_vars, body)) end; (*do (partial) eta-contraction before printing*) val eta_contract = ref false; fun eta_contr tm = let fun eta_abs (Abs (a, T, t)) = (case eta_abs t of t' as f $ u => (case eta_abs u of Bound 0 => if not (0 mem loose_bnos f) then incr_boundvars ~1 f else Abs (a, T, t') | _ => Abs (a, T, t')) | t' => Abs (a, T, t')) | eta_abs t = t; in if ! eta_contract then eta_abs tm else tm end; fun abs_tr' tm = foldr (fn (x, t) => const "_abs" $ x $ t) (strip_abss strip_abs_vars strip_abs_body (eta_contr tm)); fun abs_ast_tr' (*"_abs"*) asts = (case unfold_ast_p "_abs" (Appl (Constant "_abs" :: asts)) of ([], _) => raise_ast "abs_ast_tr'" asts | (xs, body) => Appl [Constant "_lambda", fold_ast "_idts" xs, body]); (* binder *) fun mk_binder_tr' (name, sy) = let fun mk_idts [] = raise Match (*abort translation*) | mk_idts [idt] = idt | mk_idts (idt :: idts) = const "_idts" $ idt $ mk_idts idts; fun tr' t = let val (xs, bd) = strip_abss (strip_qnt_vars name) (strip_qnt_body name) t; in const sy $ mk_idts xs $ bd end; fun binder_tr' (*name*) (t :: ts) = list_comb (tr' (const name $ t), ts) | binder_tr' (*name*) [] = raise Match; in (name, binder_tr') end; (* idts *) fun idts_ast_tr' (*"_idts"*) [Appl [Constant c, x, ty], xs] = if c = constrainC then Appl [Constant "_idts", Appl [Constant "_idtyp", x, ty], xs] else raise Match | idts_ast_tr' (*"_idts"*) _ = raise Match; (* meta propositions *) fun prop_tr' show_sorts tm = let fun aprop t = const "_aprop" $ t; fun is_prop tys t = fastype_of1 (tys, t) = propT handle TERM _ => false; fun tr' _ (t as Const _) = t | tr' _ (t as Free (x, ty)) = if ty = propT then aprop (Free (x, dummyT)) else t | tr' _ (t as Var (xi, ty)) = if ty = propT then aprop (Var (xi, dummyT)) else t | tr' tys (t as Bound _) = if is_prop tys t then aprop t else t | tr' tys (Abs (x, ty, t)) = Abs (x, ty, tr' (ty :: tys) t) | tr' tys (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [ty])))) = if is_prop tys t then const "_ofclass" $ term_of_typ show_sorts ty $ tr' tys t1 else tr' tys t1 $ tr' tys t2 | tr' tys (t as t1 $ t2) = (if is_Const (head_of t) orelse not (is_prop tys t) then I else aprop) (tr' tys t1 $ tr' tys t2); in tr' [] tm end; (* meta implication *) fun impl_ast_tr' (*"==>"*) asts = (case unfold_ast_p "==>" (Appl (Constant "==>" :: asts)) of (asms as _ :: _ :: _, concl) => Appl [Constant "_bigimpl", fold_ast "_asms" asms, concl] | _ => raise Match); (* dependent / nondependent quantifiers *) fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) = if 0 mem (loose_bnos B) then let val (x', B') = variant_abs (x, dummyT, B); in list_comb (const q $ Free (x', T) $ A $ B', ts) end else list_comb (const r $ A $ B, ts) | dependent_tr' _ _ = raise Match; (* implode atoms *) fun implode_ast_tr' (*"_implode"*) (asts as [Constant cons_name, nilC, bit0, bit1, bitss]) = let fun err () = raise_ast "implode_ast_tr'" asts; fun strip_list lst = let val (xs, y) = unfold_ast_p cons_name lst in if y = nilC then xs else err () end; fun decode_bit bit = if bit = bit0 then "0" else if bit = bit1 then "1" else err (); fun decode_char bits = chr (#1 (scan_radixint (2, map decode_bit (strip_list bits)))); in Variable (implode (map decode_char (strip_list bitss))) end | implode_ast_tr' (*"_implode"*) asts = raise_ast "implode_ast_tr'" asts; (** syn_ext_of_sext **) (* FIXME remove *) fun strip_esc str = let fun strip ("'" :: c :: cs) = c :: strip cs | strip ["'"] = [] | strip (c :: cs) = c :: strip cs | strip [] = []; in implode (strip (explode str)) end; fun infix_name sy = "op " ^ strip_esc sy; fun syn_ext_of_sext all_roots new_roots xconsts read_typ sext = let val {mixfix, parse_ast_translation, parse_translation, print_translation, print_ast_translation, ...} = sext_components sext; val tinfixT = [typeT, typeT] ---> typeT; fun binder (Binder (sy, _, name, _, _)) = Some (sy, name) | binder _ = None; fun binder_typ ty = (case read_typ ty of Type ("fun", [Type ("fun", [_, T2]), T3]) => [Type ("idts", []), T2] ---> T3 | _ => error ("Illegal binder type " ^ quote ty)); fun mk_infix sy ty c p1 p2 p3 = [Mfix ("(_ " ^ sy ^ "/ _)", ty, c, [p1, p2], p3), Mfix ("op " ^ sy, ty, c, [], max_pri)]; fun mfix_of (Mixfix (sy, ty, c, ps, p)) = [Mfix (sy, read_typ ty, c, ps, p)] | mfix_of (Delimfix (sy, ty, c)) = [Mfix (sy, read_typ ty, c, [], max_pri)] | mfix_of (Infixl (sy, ty, p)) = mk_infix sy (read_typ ty) (infix_name sy) p (p + 1) p | mfix_of (Infixr (sy, ty, p)) = mk_infix sy (read_typ ty) (infix_name sy) (p + 1) p p | mfix_of (Binder (sy, ty, _, p, q)) = [Mfix ("(3" ^ sy ^ "_./ _)", binder_typ ty, sy, [0, p], q)] | mfix_of (TInfixl (s, c, p)) = [Mfix ("(_ " ^ s ^ "/ _)", tinfixT, c, [p, p + 1], p)] | mfix_of (TInfixr (s, c, p)) = [Mfix ("(_ " ^ s ^ "/ _)", tinfixT, c, [p + 1, p], p)]; val mfix = flat (map mfix_of mixfix); val binders = mapfilter binder mixfix; val bparses = map mk_binder_tr binders; val bprints = map (mk_binder_tr' o swap) binders; in syn_ext all_roots new_roots mfix (distinct (filter is_xid xconsts)) (parse_ast_translation, bparses @ parse_translation, bprints @ print_translation, print_ast_translation) ([], []) end; (** constants **) (* FIXME remove *) fun constants sext = let fun consts (Delimfix (_, ty, c)) = ([c], ty) | consts (Mixfix (_, ty, c, _, _)) = ([c], ty) | consts (Infixl (c, ty, _)) = ([infix_name c], ty) | consts (Infixr (c, ty, _)) = ([infix_name c], ty) | consts (Binder (_, ty, c, _, _)) = ([c], ty) | consts _ = ([""], ""); (*is filtered out below*) in distinct (filter_out (fn (l, _) => l = [""]) (map consts (mixfix_of sext))) end; (** pt_to_ast **) fun pt_to_ast trf pt = let fun trans a args = (case trf a of None => mk_appl (Constant a) args | Some f => f args handle exn => (writeln ("Error in parse ast translation for " ^ quote a); raise exn)); fun ast_of (Node (a, pts)) = trans a (map ast_of pts) | ast_of (Tip tok) = Variable (str_of_token tok); in ast_of pt end; (** ast_to_term **) fun ast_to_term trf ast = let fun trans a args = (case trf a of None => list_comb (const a, args) | Some f => f args handle exn => (writeln ("Error in parse translation for " ^ quote a); raise exn)); fun term_of (Constant a) = trans a [] | term_of (Variable x) = scan_var x | term_of (Appl (Constant a :: (asts as _ :: _))) = trans a (map term_of asts) | term_of (Appl (ast :: (asts as _ :: _))) = list_comb (term_of ast, map term_of asts) | term_of (ast as Appl _) = raise_ast "ast_to_term: malformed ast" [ast]; in term_of ast end; (** pure_trfuns **) val pure_trfuns = ([(applC, appl_ast_tr), ("_lambda", lambda_ast_tr), ("_idtyp", idtyp_ast_tr), ("_bigimpl", bigimpl_ast_tr)], [("_abs", abs_tr), ("_aprop", aprop_tr), ("_ofclass", ofclass_tr), ("_K", k_tr), ("_explode", explode_tr)], [], [("_abs", abs_ast_tr'), ("_idts", idts_ast_tr'), ("==>", impl_ast_tr'), ("_implode", implode_ast_tr')]); val constrainAbsC = "_constrainAbs"; (** the Pure syntax **) (* FIXME remove *) val pure_sext = NewSext { mixfix = [ Mixfix ("(3%_./ _)", "[idts, 'a] => ('b => 'a)", "_lambda", [0], 0), Delimfix ("_", "'a => " ^ args, ""), Delimfix ("_,/ _", "['a, " ^ args ^ "] => " ^ args, "_args"), Delimfix ("_", "id => idt", ""), Mixfix ("_::_", "[id, type] => idt", "_idtyp", [0, 0], 0), Delimfix ("'(_')", "idt => idt", ""), Delimfix ("_", "idt => idts", ""), Mixfix ("_/ _", "[idt, idts] => idts", "_idts", [1, 0], 0), Delimfix ("_", "id => aprop", ""), Delimfix ("_", "var => aprop", ""), Mixfix ("(1_/(1'(_')))", "[('b => 'a), " ^ args ^ "] => aprop", applC, [max_pri, 0], max_pri), Delimfix ("PROP _", "aprop => prop", "_aprop"), Delimfix ("_", "prop => asms", ""), Delimfix ("_;/ _", "[prop, asms] => asms", "_asms"), Mixfix ("((3[| _ |]) ==>/ _)", "[asms, prop] => prop", "_bigimpl", [0, 1], 1), Mixfix ("(_ ==/ _)", "['a::{}, 'a] => prop", "==", [3, 2], 2), Mixfix ("(_ =?=/ _)", "['a::{}, 'a] => prop", "=?=", [3, 2], 2), Mixfix ("(_ ==>/ _)", "[prop, prop] => prop", "==>", [2, 1], 1), Binder ("!!", "('a::logic => prop) => prop", "all", 0, 0)], xrules = [], parse_ast_translation = [(applC, appl_ast_tr), ("_lambda", lambda_ast_tr), ("_idtyp", idtyp_ast_tr), ("_bigimpl", bigimpl_ast_tr)], parse_translation = [("_abs", abs_tr), ("_aprop", aprop_tr), ("_K", k_tr), ("_explode", explode_tr)], print_translation = [], print_ast_translation = [("_abs", abs_ast_tr'), ("_idts", idts_ast_tr'), ("==>", impl_ast_tr'), ("_implode", implode_ast_tr')]}; val syntax_types = terminals @ ["syntax", logic, "type", "types", "sort", "classes", args, "idt", "idts", "aprop", "asms"]; val syntax_consts = [(["_K", "_explode", "_implode"], "syntax")]; end;