# HG changeset patch # User wenzelm # Date 908893827 -7200 # Node ID 4b056ee5435ca216c6b0aa377d1c9a452bd53ce5 # Parent ffecea5475013419da80339878fd488dc519b450 no open; diff -r ffecea547501 -r 4b056ee5435c src/Pure/Syntax/mixfix.ML --- a/src/Pure/Syntax/mixfix.ML Tue Oct 20 16:29:47 1998 +0200 +++ b/src/Pure/Syntax/mixfix.ML Tue Oct 20 16:30:27 1998 +0200 @@ -16,7 +16,6 @@ Infixl of int | Infixr of int | Binder of string * int * int - val max_pri: int end; signature MIXFIX1 = @@ -47,8 +46,6 @@ structure Mixfix : MIXFIX = struct -open Lexicon SynExt Ast SynTrans; - (** mixfix declarations **) @@ -94,8 +91,8 @@ (* mixfix_args *) fun mixfix_args NoSyn = 0 - | mixfix_args (Mixfix (sy, _, _)) = mfix_args sy - | mixfix_args (Delimfix sy) = mfix_args sy + | mixfix_args (Mixfix (sy, _, _)) = SynExt.mfix_args sy + | mixfix_args (Delimfix sy) = SynExt.mfix_args sy | mixfix_args (*infix or binder*) _ = 2; @@ -106,7 +103,8 @@ fun name_of (t, _, mx) = type_name t mx; fun mk_infix sy t p1 p2 p3 = - Mfix ("(_ " ^ sy ^ "/ _)", [typeT, typeT] ---> typeT, t, [p1, p2], p3); + SynExt.Mfix ("(_ " ^ sy ^ "/ _)", + [SynExt.typeT, SynExt.typeT] ---> SynExt.typeT, t, [p1, p2], p3); fun mfix_of decl = let val t = name_of decl in @@ -121,9 +119,7 @@ val mfix = mapfilter mfix_of type_decls; val xconsts = map name_of type_decls; - in - syn_ext logtypes mfix xconsts ([], [], [], []) [] ([], []) - end; + in SynExt.syn_ext logtypes mfix xconsts ([], [], [], []) [] ([], []) end; (* syn_ext_consts *) @@ -133,8 +129,8 @@ fun name_of (c, _, mx) = const_name c mx; fun mk_infix sy ty c p1 p2 p3 = - [Mfix ("op " ^ sy, ty, c, [], max_pri), - Mfix ("(_ " ^ sy ^ "/ _)", ty, c, [p1, p2], p3)]; + [SynExt.Mfix ("op " ^ sy, ty, c, [], SynExt.max_pri), + SynExt.Mfix ("(_ " ^ sy ^ "/ _)", ty, c, [p1, p2], p3)]; fun binder_typ _ (Type ("fun", [Type ("fun", [_, ty2]), ty3])) = [Type ("idts", []), ty2] ---> ty3 @@ -144,14 +140,14 @@ let val c = name_of decl in (case decl of (_, _, NoSyn) => [] - | (_, ty, Mixfix (sy, ps, p)) => [Mfix (sy, ty, c, ps, p)] - | (_, ty, Delimfix sy) => [Mfix (sy, ty, c, [], max_pri)] + | (_, ty, Mixfix (sy, ps, p)) => [SynExt.Mfix (sy, ty, c, ps, p)] + | (_, ty, Delimfix sy) => [SynExt.Mfix (sy, ty, c, [], SynExt.max_pri)] | (_, ty, InfixlName (sy, p)) => mk_infix sy ty c p (p + 1) p | (_, ty, InfixrName (sy, p)) => mk_infix sy ty c (p + 1) p p | (sy, ty, Infixl p) => mk_infix sy ty c p (p + 1) p | (sy, ty, Infixr p) => mk_infix sy ty c (p + 1) p p | (_, ty, Binder (sy, p, q)) => - [Mfix ("(3" ^ sy ^ "_./ _)", binder_typ c ty, sy, [0, p], q)]) + [SynExt.Mfix ("(3" ^ sy ^ "_./ _)", binder_typ c ty, sy, [0, p], q)]) end; fun binder (c, _, Binder (sy, _, _)) = Some (sy, c) @@ -160,25 +156,24 @@ val mfix = flat (map mfix_of const_decls); val xconsts = map name_of const_decls; val binders = mapfilter binder const_decls; - val binder_trs = map mk_binder_tr binders; - val binder_trs' = map (apsnd fix_tr' o mk_binder_tr' o swap) binders; - in - syn_ext logtypes mfix xconsts ([], binder_trs, binder_trs', []) [] ([], []) - end; + val binder_trs = map SynTrans.mk_binder_tr binders; + val binder_trs' = map (apsnd SynExt.fix_tr' o SynTrans.mk_binder_tr' o swap) binders; + in SynExt.syn_ext logtypes mfix xconsts ([], binder_trs, binder_trs', []) [] ([], []) end; (** Pure syntax **) val pure_nonterms = - (terminals @ [logic, "type", "types", "sort", "classes", args, cargs, - "pttrn", "pttrns", "idt", "idts", "aprop", "asms", any, sprop]); + (Lexicon.terminals @ [SynExt.logic, "type", "types", "sort", "classes", + SynExt.args, SynExt.cargs, "pttrn", "pttrns", "idt", "idts", "aprop", + "asms", SynExt.any, SynExt.sprop]); val pure_syntax = [("_lambda", "[pttrns, 'a] => logic", Mixfix ("(3%_./ _)", [0, 3], 3)), ("_abs", "'a", NoSyn), - ("", "'a => " ^ args, Delimfix "_"), - ("_args", "['a, " ^ args ^ "] => " ^ args, Delimfix "_,/ _"), + ("", "'a => " ^ SynExt.args, Delimfix "_"), + ("_args", "['a, " ^ SynExt.args ^ "] => " ^ SynExt.args, Delimfix "_,/ _"), ("", "id => idt", Delimfix "_"), ("_idtyp", "[id, type] => idt", Mixfix ("_::_", [], 0)), ("", "idt => idt", Delimfix "'(_')"), @@ -204,19 +199,19 @@ ("_BIND", "id => logic", Delimfix "??_")]; val pure_appl_syntax = - [("_appl", "[('b => 'a), args] => logic", Mixfix ("(1_/(1'(_')))", [max_pri, 0], max_pri)), - ("_appl", "[('b => 'a), args] => aprop", Mixfix ("(1_/(1'(_')))", [max_pri, 0], max_pri))]; + [("_appl", "[('b => 'a), args] => logic", Mixfix ("(1_/(1'(_')))", [SynExt.max_pri, 0], SynExt.max_pri)), + ("_appl", "[('b => 'a), args] => aprop", Mixfix ("(1_/(1'(_')))", [SynExt.max_pri, 0], SynExt.max_pri))]; val pure_applC_syntax = [("", "'a => cargs", Delimfix "_"), - ("_cargs", "['a, cargs] => cargs", Mixfix ("_/ _", [max_pri, max_pri], max_pri)), - ("_applC", "[('b => 'a), cargs] => logic", Mixfix ("(1_/ _)", [max_pri, max_pri], max_pri - 1)), - ("_applC", "[('b => 'a), cargs] => aprop", Mixfix ("(1_/ _)", [max_pri, max_pri], max_pri - 1))]; + ("_cargs", "['a, cargs] => cargs", Mixfix ("_/ _", [SynExt.max_pri, SynExt.max_pri], SynExt.max_pri)), + ("_applC", "[('b => 'a), cargs] => logic", Mixfix ("(1_/ _)", [SynExt.max_pri, SynExt.max_pri], SynExt.max_pri - 1)), + ("_applC", "[('b => 'a), cargs] => aprop", Mixfix ("(1_/ _)", [SynExt.max_pri, SynExt.max_pri], SynExt.max_pri - 1))]; val pure_sym_syntax = [("fun", "[type, type] => type", Mixfix ("(_/ \\ _)", [1, 0], 0)), ("_bracket", "[types, type] => type", Mixfix ("([_]/ \\ _)", [0, 0], 0)), - ("_ofsort", "[tid, sort] => type", Mixfix ("_\\_", [max_pri, 0], max_pri)), + ("_ofsort", "[tid, sort] => type", Mixfix ("_\\_", [SynExt.max_pri, 0], SynExt.max_pri)), ("_constrain", "['a, type] => 'a", Mixfix ("_\\_", [4, 0], 3)), ("_idtyp", "[id, type] => idt", Mixfix ("_\\_", [], 0)), ("_lambda", "[pttrns, 'a] => logic", Mixfix ("(3\\_./ _)", [0, 3], 3)), diff -r ffecea547501 -r 4b056ee5435c src/Pure/Syntax/syn_ext.ML --- a/src/Pure/Syntax/syn_ext.ML Tue Oct 20 16:29:47 1998 +0200 +++ b/src/Pure/Syntax/syn_ext.ML Tue Oct 20 16:30:27 1998 +0200 @@ -9,6 +9,7 @@ sig val typeT: typ val constrainC: string + val max_pri: int end; signature SYN_EXT = @@ -26,7 +27,6 @@ Space of string | Bg of int | Brk of int | En datatype xprod = XProd of string * xsymb list * string * int - val max_pri: int val chain_pri: int val delims_of: xprod list -> string list list datatype mfix = Mfix of string * typ * string * int list * int @@ -73,8 +73,6 @@ structure SynExt : SYN_EXT = struct -open Lexicon Ast; - (** misc definitions **) @@ -239,7 +237,7 @@ | is_arg _ = false; fun is_term (Delim _) = true - | is_term (Argument (s, _)) = is_terminal s + | is_term (Argument (s, _)) = Lexicon.is_terminal s | is_term _ = false; fun rem_pri (Argument (s, _)) = Argument (s, chain_pri) @@ -272,7 +270,7 @@ check_pri pri; check_blocks symbs'; - if is_terminal lhs' then err ("Illegal lhs: " ^ lhs') + if Lexicon.is_terminal lhs' then err ("Illegal lhs: " ^ lhs') else if const <> "" then xprod else if length (filter is_arg symbs') <> 1 then err "Copy production must have exactly one argument" @@ -313,7 +311,7 @@ SynExt { logtypes = logtypes', xprods = xprods, - consts = filter is_xid (consts union mfix_consts), + consts = filter Lexicon.is_xid (consts union mfix_consts), prmodes = distinct (map (fn (m, _, _) => m) tokentrfuns), parse_ast_translation = parse_ast_translation, parse_rules = parse_rules, diff -r ffecea547501 -r 4b056ee5435c src/Pure/Syntax/syn_trans.ML --- a/src/Pure/Syntax/syn_trans.ML Tue Oct 20 16:29:47 1998 +0200 +++ b/src/Pure/Syntax/syn_trans.ML Tue Oct 20 16:30:27 1998 +0200 @@ -44,42 +44,40 @@ structure SynTrans: SYN_TRANS = struct -open TypeExt Lexicon Ast SynExt Parser; - (** parse (ast) translations **) (* application *) -fun appl_ast_tr [f, args] = Appl (f :: unfold_ast "_args" args) - | appl_ast_tr asts = raise AST ("appl_ast_tr", asts); +fun appl_ast_tr [f, args] = Ast.Appl (f :: Ast.unfold_ast "_args" args) + | appl_ast_tr asts = raise Ast.AST ("appl_ast_tr", asts); -fun applC_ast_tr [f, args] = Appl (f :: unfold_ast "_cargs" args) - | applC_ast_tr asts = raise AST ("applC_ast_tr", asts); +fun applC_ast_tr [f, args] = Ast.Appl (f :: Ast.unfold_ast "_cargs" args) + | applC_ast_tr asts = raise Ast.AST ("applC_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 idtyp_ast_tr (*"_idtyp"*) [x, ty] = Ast.Appl [Ast.Constant SynExt.constrainC, x, ty] + | idtyp_ast_tr (*"_idtyp"*) asts = raise Ast.AST ("idtyp_ast_tr", asts); fun lambda_ast_tr (*"_lambda"*) [pats, body] = - fold_ast_p "_abs" (unfold_ast "_pttrns" pats, body) - | lambda_ast_tr (*"_lambda"*) asts = raise AST ("lambda_ast_tr", asts); + Ast.fold_ast_p "_abs" (Ast.unfold_ast "_pttrns" pats, body) + | lambda_ast_tr (*"_lambda"*) asts = raise Ast.AST ("lambda_ast_tr", asts); val constrainAbsC = "_constrainAbs"; -fun abs_tr (*"_abs"*) [Free (x, T), body] = absfree (x, T, body) +fun abs_tr (*"_abs"*) [Free (x, T), body] = Term.absfree (x, T, body) | abs_tr (*"_abs"*) (ts as [Const (c, _) $ Free (x, T) $ tT, body]) = - if c = constrainC - then const constrainAbsC $ absfree (x, T, body) $ tT + if c = SynExt.constrainC + then Lexicon.const constrainAbsC $ Term.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) +fun k_tr (*"_K"*) [t] = Abs ("uu", dummyT, Term.incr_boundvars 1 t) | k_tr (*"_K"*) ts = raise TERM ("k_tr", ts); @@ -87,11 +85,11 @@ fun mk_binder_tr (sy, name) = let - fun tr (Free (x, T), t) = const name $ absfree (x, T, t) + fun tr (Free (x, T), t) = Lexicon.const name $ Term.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 constrainAbsC $ absfree (x, T, t) $ tT) + if c = SynExt.constrainC then + Lexicon.const name $ (Lexicon.const constrainAbsC $ Term.absfree (x, T, t) $ tT) else raise TERM ("binder_tr", [t1, t]) | tr (t1, t2) = raise TERM ("binder_tr", [t1, t2]); @@ -104,32 +102,34 @@ (* meta propositions *) -fun aprop_tr (*"_aprop"*) [t] = const constrainC $ t $ const "prop" +fun aprop_tr (*"_aprop"*) [t] = Lexicon.const SynExt.constrainC $ t $ Lexicon.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)) + cls $ (Lexicon.const SynExt.constrainC $ Lexicon.const "TYPE" $ + (Lexicon.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); + Ast.fold_ast_p "==>" (Ast.unfold_ast "_asms" asms, concl) + | bigimpl_ast_tr (*"_bigimpl"*) asts = raise Ast.AST ("bigimpl_ast_tr", asts); (* type reflection *) fun type_tr (*"_TYPE"*) [ty] = - const constrainC $ const "TYPE" $ (const "itself" $ ty) + Lexicon.const SynExt.constrainC $ Lexicon.const "TYPE" $ (Lexicon.const "itself" $ ty) | type_tr (*"_TYPE"*) ts = raise TERM ("type_tr", ts); (* binds *) -fun bind_ast_tr (*"_BIND"*) [Variable x] = Variable (string_of_vname (binding x, 0)) - | bind_ast_tr (*"_BIND"*) asts = raise AST ("bind_ast_tr", asts); +fun bind_ast_tr (*"_BIND"*) [Ast.Variable x] = + Ast.Variable (Lexicon.string_of_vname (Lexicon.binding x, 0)) + | bind_ast_tr (*"_BIND"*) asts = raise Ast.AST ("bind_ast_tr", asts); (* quote / antiquote *) @@ -143,7 +143,8 @@ | antiquote_tr i (Abs (x, T, t)) = Abs (x, T, antiquote_tr (i + 1) t) | antiquote_tr _ a = a; - fun quote_tr [t] = const name $ Abs ("uu", dummyT, antiquote_tr 0 (incr_boundvars 1 t)) + fun quote_tr [t] = Lexicon.const name $ + Abs ("uu", dummyT, antiquote_tr 0 (Term.incr_boundvars 1 t)) | quote_tr ts = raise TERM ("quote_tr", ts); in (quoteN, quote_tr) end; @@ -153,17 +154,16 @@ (* 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]; +fun appl_ast_tr' (f, []) = raise Ast.AST ("appl_ast_tr'", [f]) + | appl_ast_tr' (f, args) = Ast.Appl [Ast.Constant "_appl", f, Ast.fold_ast "_args" args]; -fun applC_ast_tr' (f, []) = raise AST ("applC_ast_tr'", [f]) - | applC_ast_tr' (f, args) = - Appl [Constant "_applC", f, fold_ast "_cargs" args]; +fun applC_ast_tr' (f, []) = raise Ast.AST ("applC_ast_tr'", [f]) + | applC_ast_tr' (f, args) = Ast.Appl [Ast.Constant "_applC", f, Ast.fold_ast "_cargs" args]; (* abstraction *) -fun mark_boundT x_T = const "_bound" $ Free x_T; +fun mark_boundT x_T = Lexicon.const "_bound" $ Free x_T; fun mark_bound x = mark_boundT (x, dummyT); fun strip_abss vars_of body_of tm = @@ -202,14 +202,14 @@ fun abs_tr' tm = - foldr (fn (x, t) => const "_abs" $ x $ t) + foldr (fn (x, t) => Lexicon.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 "_pttrns" xs, body]); + (case Ast.unfold_ast_p "_abs" (Ast.Appl (Ast.Constant "_abs" :: asts)) of + ([], _) => raise Ast.AST ("abs_ast_tr'", asts) + | (xs, body) => Ast.Appl [Ast.Constant "_lambda", Ast.fold_ast "_pttrns" xs, body]); (* binder *) @@ -218,17 +218,14 @@ let fun mk_idts [] = raise Match (*abort translation*) | mk_idts [idt] = idt - | mk_idts (idt :: idts) = const "_idts" $ idt $ mk_idts idts; + | mk_idts (idt :: idts) = Lexicon.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; + in Lexicon.const sy $ mk_idts xs $ bd end; - fun binder_tr' (*name*) (t :: ts) = - list_comb (tr' (const name $ t), ts) + fun binder_tr' (*name*) (t :: ts) = Term.list_comb (tr' (Lexicon.const name $ t), ts) | binder_tr' (*name*) [] = raise Match; in (name, binder_tr') @@ -237,9 +234,9 @@ (* idtyp constraints *) -fun idtyp_ast_tr' a [Appl [Constant c, x, ty], xs] = - if c = constrainC then - Appl [Constant a, Appl [Constant "_idtyp", x, ty], xs] +fun idtyp_ast_tr' a [Ast.Appl [Ast.Constant c, x, ty], xs] = + if c = SynExt.constrainC then + Ast.Appl [ Ast.Constant a, Ast.Appl [Ast.Constant "_idtyp", x, ty], xs] else raise Match | idtyp_ast_tr' _ _ = raise Match; @@ -248,16 +245,16 @@ fun prop_tr' tm = let - fun aprop t = const "_aprop" $ t; + fun aprop t = Lexicon.const "_aprop" $ t; fun is_prop Ts t = fastype_of1 (Ts, t) = propT handle TERM _ => false; fun tr' _ (t as Const _) = t | tr' _ (t as Free (x, T)) = - if T = propT then aprop (free x) else t + if T = propT then aprop (Lexicon.free x) else t | tr' _ (t as Var (xi, T)) = - if T = propT then aprop (var xi) else t + if T = propT then aprop (Lexicon.var xi) else t | tr' Ts (t as Bound _) = if is_prop Ts t then aprop t else t | tr' Ts (Abs (x, T, t)) = Abs (x, T, tr' (T :: Ts) t) @@ -265,30 +262,30 @@ if is_prop Ts t then Const ("_mk_ofclass", T) $ tr' Ts t1 else tr' Ts t1 $ tr' Ts t2 | tr' Ts (t as t1 $ t2) = - (if is_Const (head_of t) orelse not (is_prop Ts t) + (if is_Const (Term.head_of t) orelse not (is_prop Ts t) then I else aprop) (tr' Ts t1 $ tr' Ts t2); in tr' [] tm end; fun mk_ofclass_tr' show_sorts (*"_mk_ofclass"*) T [t] = - const "_ofclass" $ term_of_typ show_sorts T $ t + Lexicon.const "_ofclass" $ TypeExt.term_of_typ show_sorts T $ t | mk_ofclass_tr' _ (*"_mk_ofclass"*) T ts = raise TYPE ("mk_ofclass_tr'", [T], ts); (* meta implication *) fun impl_ast_tr' (*"==>"*) asts = - (case unfold_ast_p "==>" (Appl (Constant "==>" :: asts)) of + (case Ast.unfold_ast_p "==>" (Ast.Appl (Ast.Constant "==>" :: asts)) of (asms as _ :: _ :: _, concl) - => Appl [Constant "_bigimpl", fold_ast "_asms" asms, concl] + => Ast.Appl [Ast.Constant "_bigimpl", Ast.fold_ast "_asms" asms, concl] | _ => raise Match); (* type reflection *) fun type_tr' show_sorts (*"TYPE"*) (Type ("itself", [T])) ts = - list_comb (const "_TYPE" $ term_of_typ show_sorts T, ts) + Term.list_comb (Lexicon.const "_TYPE" $ TypeExt.term_of_typ show_sorts T, ts) | type_tr' _ _ _ = raise Match; @@ -302,8 +299,8 @@ fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) = if Term.loose_bvar1 (B, 0) then let val (x', B') = variant_abs' (x, dummyT, B); - in list_comb (const q $ mark_boundT (x', T) $ A $ B', ts) end - else list_comb (const r $ A $ B, ts) + in Term.list_comb (Lexicon.const q $ mark_boundT (x', T) $ A $ B', ts) end + else Term.list_comb (Lexicon.const r $ A $ B, ts) | dependent_tr' _ _ = raise Match; @@ -315,13 +312,13 @@ fun quote_antiquote_tr' quoteN antiquoteN name = let fun antiquote_tr' i (t $ u) = - if u = Bound i then const antiquoteN $ no_loose_bvar i t + if u = Bound i then Lexicon.const antiquoteN $ no_loose_bvar i t else antiquote_tr' i t $ antiquote_tr' i u | antiquote_tr' i (Abs (x, T, t)) = Abs (x, T, antiquote_tr' (i + 1) t) | antiquote_tr' i a = no_loose_bvar i a; fun quote_tr' (Abs (x, T, t) :: ts) = - Term.list_comb (const quoteN $ incr_boundvars ~1 (antiquote_tr' 0 t), ts) + Term.list_comb ( Lexicon.const quoteN $ Term.incr_boundvars ~1 (antiquote_tr' 0 t), ts) | quote_tr' _ = raise Match; in (name, quote_tr') end; @@ -350,14 +347,14 @@ let fun trans a args = (case trf a of - None => mk_appl (Constant a) args + None => Ast.mk_appl (Ast.Constant a) args | Some f => f args handle exn => (writeln ("Error in parse ast translation for " ^ quote a); raise exn)); (*translate pt bottom-up*) - fun ast_of (Node (a, pts)) = trans a (map ast_of pts) - | ast_of (Tip tok) = Variable (str_of_token tok); + fun ast_of (Parser.Node (a, pts)) = trans a (map ast_of pts) + | ast_of (Parser.Tip tok) = Ast.Variable (Lexicon.str_of_token tok); in ast_of pt end; @@ -370,18 +367,18 @@ let fun trans a args = (case trf a of - None => list_comb (const a, args) + None => Term.list_comb (Lexicon.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) = read_var x - | term_of (Appl (Constant a :: (asts as _ :: _))) = + fun term_of (Ast.Constant a) = trans a [] + | term_of (Ast.Variable x) = Lexicon.read_var x + | term_of (Ast.Appl (Ast.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]); + | term_of (Ast.Appl (ast :: (asts as _ :: _))) = + Term.list_comb (term_of ast, map term_of asts) + | term_of (ast as Ast.Appl _) = raise Ast.AST ("ast_to_term: malformed ast", [ast]); in term_of ast end; diff -r ffecea547501 -r 4b056ee5435c src/Pure/Syntax/type_ext.ML --- a/src/Pure/Syntax/type_ext.ML Tue Oct 20 16:29:47 1998 +0200 +++ b/src/Pure/Syntax/type_ext.ML Tue Oct 20 16:30:27 1998 +0200 @@ -24,8 +24,6 @@ structure TypeExt : TYPE_EXT = struct -open Lexicon SynExt Ast; - (** input utils **) @@ -60,7 +58,7 @@ fun typ_of_term get_sort t = let fun typ_of (Free (x, _)) = - if is_tid x then TFree (x, get_sort (x, ~1)) + if Lexicon.is_tid x then TFree (x, get_sort (x, ~1)) else Type (x, []) | typ_of (Var (xi, _)) = TVar (xi, get_sort xi) | typ_of (Const ("_ofsort", _) $ Free (x, _) $ _) = @@ -90,16 +88,16 @@ fun term_of_sort S = let - fun class c = const "_class" $ free c; + fun class c = Lexicon.const "_class" $ Lexicon.free c; fun classes [] = sys_error "term_of_sort" | classes [c] = class c - | classes (c :: cs) = const "_classes" $ class c $ classes cs; + | classes (c :: cs) = Lexicon.const "_classes" $ class c $ classes cs; in (case S of - [] => const "_topsort" + [] => Lexicon.const "_topsort" | [c] => class c - | cs => const "_sort" $ classes cs) + | cs => Lexicon.const "_sort" $ classes cs) end; @@ -108,12 +106,12 @@ fun term_of_typ show_sorts ty = let fun of_sort t S = - if show_sorts then const "_ofsort" $ t $ term_of_sort S + if show_sorts then Lexicon.const "_ofsort" $ t $ term_of_sort S else t; - fun term_of (Type (a, Ts)) = list_comb (const a, map term_of Ts) - | term_of (TFree (x, S)) = of_sort (const "_tfree" $ free x) S - | term_of (TVar (xi, S)) = of_sort (const "_tvar" $ var xi) S; + fun term_of (Type (a, Ts)) = list_comb (Lexicon.const a, map term_of Ts) + | term_of (TFree (x, S)) = of_sort (Lexicon.const "_tfree" $ Lexicon.free x) S + | term_of (TVar (xi, S)) = of_sort (Lexicon.const "_tvar" $ Lexicon.var xi) S; in term_of ty end; @@ -124,29 +122,29 @@ (* parse ast translations *) -fun tapp_ast_tr (*"_tapp"*) [ty, f] = Appl [f, ty] - | tapp_ast_tr (*"_tapp"*) asts = raise AST ("tapp_ast_tr", asts); +fun tapp_ast_tr (*"_tapp"*) [ty, f] = Ast.Appl [f, ty] + | tapp_ast_tr (*"_tapp"*) asts = raise Ast.AST ("tapp_ast_tr", asts); fun tappl_ast_tr (*"_tappl"*) [ty, tys, f] = - Appl (f :: ty :: unfold_ast "_types" tys) - | tappl_ast_tr (*"_tappl"*) asts = raise AST ("tappl_ast_tr", asts); + Ast.Appl (f :: ty :: Ast.unfold_ast "_types" tys) + | tappl_ast_tr (*"_tappl"*) asts = raise Ast.AST ("tappl_ast_tr", asts); fun bracket_ast_tr (*"_bracket"*) [dom, cod] = - fold_ast_p "fun" (unfold_ast "_types" dom, cod) - | bracket_ast_tr (*"_bracket"*) asts = raise AST ("bracket_ast_tr", asts); + Ast.fold_ast_p "fun" (Ast.unfold_ast "_types" dom, cod) + | bracket_ast_tr (*"_bracket"*) asts = raise Ast.AST ("bracket_ast_tr", asts); (* print ast translations *) -fun tappl_ast_tr' (f, []) = raise AST ("tappl_ast_tr'", [f]) - | tappl_ast_tr' (f, [ty]) = Appl [Constant "_tapp", ty, f] +fun tappl_ast_tr' (f, []) = raise Ast.AST ("tappl_ast_tr'", [f]) + | tappl_ast_tr' (f, [ty]) = Ast.Appl [Ast.Constant "_tapp", ty, f] | tappl_ast_tr' (f, ty :: tys) = - Appl [Constant "_tappl", ty, fold_ast "_types" tys, f]; + Ast.Appl [Ast.Constant "_tappl", ty, Ast.fold_ast "_types" tys, f]; fun fun_ast_tr' (*"fun"*) asts = - (case unfold_ast_p "fun" (Appl (Constant "fun" :: asts)) of + (case Ast.unfold_ast_p "fun" (Ast.Appl (Ast.Constant "fun" :: asts)) of (dom as _ :: _ :: _, cod) - => Appl [Constant "_bracket", fold_ast "_types" dom, cod] + => Ast.Appl [Ast.Constant "_bracket", Ast.fold_ast "_types" dom, cod] | _ => raise Match); @@ -156,6 +154,8 @@ val classesT = Type ("classes", []); val typesT = Type ("types", []); +local open Lexicon SynExt in + val type_ext = mk_syn_ext false [] [Mfix ("_", tidT --> typeT, "", [], max_pri), Mfix ("_", tvarT --> typeT, "", [], max_pri), @@ -190,3 +190,6 @@ ([], []); end; + + +end;