diff -r 000000000000 -r a5a9c433f639 src/Pure/Syntax/sextension.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Syntax/sextension.ML Thu Sep 16 12:20:38 1993 +0200 @@ -0,0 +1,511 @@ +(* Title: Pure/Syntax/sextension + ID: $Id$ + Author: Tobias Nipkow and Markus Wenzel, TU Muenchen + +Syntax extensions: mixfix declarations, syntax rules, infixes, binders and +the Pure syntax. + +Changes: + SEXTENSION: added Ast, xrule + changed sext + added ast_to_term + ext_of_sext: added xconsts + SEXTENSION1: added empty_sext, appl_ast_tr' + SEXTENSION1: removed appl_tr' +TODO: +*) + + +infix |-> <-| <->; + +signature SEXTENSION0 = +sig + structure Ast: AST + local open 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_preproc: (ast -> ast) option, + parse_postproc: (ast -> ast) option, + parse_translation: (string * (term list -> term)) list, + print_translation: (string * (term list -> term)) list, + print_preproc: (ast -> ast) option, + print_postproc: (ast -> ast) option, + 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 ndependent_tr: string -> term list -> term + val dependent_tr': string * string -> term list -> term + val max_pri: int + end +end; + +signature SEXTENSION1 = +sig + include SEXTENSION0 + 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 constrainAbsC: string +end; + +signature SEXTENSION = +sig + include SEXTENSION1 + structure Extension: EXTENSION + sharing Extension.XGram.Ast = Ast + local open Extension Ast in + val xrules_of: sext -> xrule list + val abs_tr': term -> term + val appl_ast_tr': ast * ast list -> ast + val ext_of_sext: string list -> string list -> (string -> typ) -> sext -> ext + val ast_to_term: (string -> (term list -> term) option) -> ast -> term + val constrainIdtC: string + val apropC: string + end +end; + +functor SExtensionFun(structure TypeExt: TYPE_EXT and Lexicon: LEXICON)(*: SEXTENSION *) = (* FIXME *) +struct + +structure Extension = TypeExt.Extension; +structure Ast = Extension.XGram.Ast; +open Extension Ast; + + +(** datatype sext **) + +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_preproc: (ast -> ast) option, + parse_postproc: (ast -> ast) option, + parse_translation: (string * (term list -> term)) list, + print_translation: (string * (term list -> term)) list, + print_preproc: (ast -> ast) option, + print_postproc: (ast -> ast) option, + 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_preproc = None, + parse_postproc = None, + parse_translation = parse_translation, + print_translation = print_translation, + print_preproc = None, + print_postproc = None, + 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; + + + +(** parse 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 "_%" (unfold_ast "_idts" idts, body) + | lambda_ast_tr (*"_lambda"*) asts = raise_ast "lambda_ast_tr" asts; + +fun abs_tr (*"_%"*) [Free (x, T), body] = absfree (x, T, body) + | abs_tr (*"_%"*) (ts as [Const (c, _) $ Free (x, T) $ tT, body]) = + if c = constrainC then + Const ("_constrainAbs", dummyT) $ absfree (x, T, body) $ tT + else raise (TERM ("abs_tr", ts)) + | abs_tr (*"_%"*) ts = raise (TERM ("abs_tr", ts)); + + +(* binder *) (* FIXME check *) (* FIXME check *) + +fun mk_binder_tr (sy, name) = + let + val const = Const (name, dummyT); + + fun tr (Free (x, T), t) = const $ 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) = (* FIXME *) + if c = constrainC then + const $ (Const ("_constrainAbs", dummyT) $ 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; + + +(* atomic props *) + +fun aprop_ast_tr (*"_aprop"*) [ast] = ast + | aprop_ast_tr (*"_aprop"*) asts = raise_ast "aprop_ast_tr" asts; + + +(* 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; + + +(* 'dependent' type operators *) + +fun ndependent_tr q [A, B] = + Const (q, dummyT) $ A $ Abs ("x", dummyT, incr_boundvars 1 B) + | ndependent_tr _ _ = raise Match; + + + +(** print 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 *) (* FIXME check *) + +fun strip_abss vars_of body_of tm = + let + 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 (fn (x, _) => Free (x, dummyT)) 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 ("_%", dummyT) $ x $ t) + (strip_abss strip_abs_vars strip_abs_body (eta_contr tm)); + + +fun lambda_ast_tr' (*"_%"*) asts = + (case unfold_ast_p "_%" (Appl (Constant "_%" :: asts)) of + ([], _) => raise_ast "lambda_ast_tr'" asts + | (xs, body) => Appl [Constant "_lambda", fold_ast "_idts" xs, body]); + + +(* binder *) (* FIXME check *) + +fun mk_binder_tr' (name, sy) = + let + fun mk_idts [] = raise Match (*abort translation*) + | mk_idts [idt] = idt + | mk_idts (idt :: idts) = Const ("_idts", dummyT) $ 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, dummyT) $ mk_idts xs $ bd + end; + + fun binder_tr' (*name*) (t :: ts) = + list_comb (tr' (Const (name, dummyT) $ 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 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' type operators *) + +fun dependent_tr' (q, r) [A, Abs (x, T, B)] = + if 0 mem (loose_bnos B) then + let val (x', B') = variant_abs (x, dummyT, B); + in Const (q, dummyT) $ Free (x', T) $ A $ B' end + else Const (r, dummyT) $ A $ B + | dependent_tr' _ _ = raise Match; + + + +(** constants **) + +(* FIXME opn, clean: move *) +val clean = + let + fun q ("'" :: c :: cs) = c ^ q cs + | q (c :: cs) = c ^ q cs + | q ([]) = "" + in q o explode end; + +val opn = "op "; + + +fun constants sext = + let + fun consts (Delimfix (_, ty, c)) = ([c], ty) + | consts (Mixfix (_, ty, c, _, _)) = ([c], ty) + | consts (Infixl (c, ty, _)) = ([opn ^ clean c], ty) + | consts (Infixr (c, ty, _)) = ([opn ^ clean 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; + + + +(** ext_of_sext **) (* FIXME check, clean *) + +fun ext_of_sext roots xconsts read_typ sext = + let + val + {mixfix, parse_ast_translation, parse_preproc, parse_postproc, + parse_translation, print_translation, print_preproc, print_postproc, + print_ast_translation, ...} = sext_components sext; + + val infixT = [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 (quote ty ^ " is not a valid binder type.")); + + fun mfix_of (Mixfix (sy, ty, c, pl, p)) = [Mfix (sy, read_typ ty, c, pl, p)] + | mfix_of (Delimfix (sy, ty, c)) = [Mfix (sy, read_typ ty, c, [], max_pri)] + | mfix_of (Infixl (sy, ty, p)) = + let val T = read_typ ty and c = opn ^ sy and c' = opn ^ clean sy + in + [Mfix (c, T, c', [], max_pri), + Mfix("(_ " ^ sy ^ "/ _)", T, c', [p, p + 1], p)] + end + | mfix_of (Infixr (sy, ty, p)) = + let val T = read_typ ty and c = opn ^ sy and c' = opn ^ clean sy + in + [Mfix(c, T, c', [], max_pri), + Mfix("(_ " ^ sy ^ "/ _)", T, c', [p + 1, p], p)] + end + | 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 ^ "/ _)", infixT, c, [p, p + 1], p)] + | mfix_of (TInfixr (s, c, p)) = + [Mfix ("(_ " ^ s ^ "/ _)", infixT, c, [p + 1, p], p)]; + + val mfix = flat (map mfix_of mixfix); + val mfix_consts = map (fn (Mfix (_, _, c, _, _)) => c) mfix; + val bs = mapfilter binder mixfix; + val bparses = map mk_binder_tr bs; + val bprints = map (mk_binder_tr' o (fn (x, y) => (y, x))) bs; + in + Ext { + roots = roots, mfix = mfix, + extra_consts = distinct (filter Lexicon.is_identifier (xconsts @ mfix_consts)), + parse_ast_translation = parse_ast_translation, + parse_preproc = parse_preproc, + parse_postproc = parse_postproc, + parse_translation = bparses @ parse_translation, + print_translation = bprints @ print_translation, + print_preproc = print_preproc, + print_postproc = print_postproc, + print_ast_translation = print_ast_translation} + end; + + + +(** ast_to_term **) + +fun ast_to_term trf ast = + let + fun scan_vname prfx cs = + (case Lexicon.scan_varname cs of + ((x, i), []) => Var ((prfx ^ x, i), dummyT) + | _ => error ("ast_to_term: bad variable name " ^ quote (implode cs))); + + fun vname_to_var v = + (case explode v of + "?" :: "'" :: cs => scan_vname "'" cs + | "?" :: cs => scan_vname "" cs + | _ => Free (v, dummyT)); + + fun trans a args = + (case trf a of + None => list_comb (Const (a, dummyT), args) + | Some f => ((f args) + handle _ => error ("ast_to_term: error in translation for " ^ quote a))); + + fun trav (Constant a) = trans a [] + | trav (Appl (Constant a :: (asts as _ :: _))) = trans a (map trav asts) + | trav (Appl (ast :: (asts as _ :: _))) = + list_comb (trav ast, map trav asts) + | trav (ast as (Appl _)) = raise_ast "ast_to_term: malformed ast" [ast] + | trav (Variable x) = vname_to_var x; + in + trav ast + end; + + + +(** the Pure syntax **) + +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 ("_'(_')", "[('b => 'a), " ^ args ^ "] => aprop", applC, [max_pri, 0], 0), + 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), + ("_aprop", aprop_ast_tr), ("_bigimpl", bigimpl_ast_tr)], + parse_preproc = None, + parse_postproc = None, + parse_translation = [("_%", abs_tr)], + print_translation = [], + print_preproc = None, + print_postproc = None, + print_ast_translation = [("_%", lambda_ast_tr'), ("_idts", idts_ast_tr'), + ("==>", impl_ast_tr')]}; + +val syntax_types = (* FIXME clean, check *) + [logic, "aprop", args, "asms", id, "idt", "idts", tfree, tvar, "type", "types", + var, "sort", "classes"] + +val constrainIdtC = "_idtyp"; +val constrainAbsC = "_constrainAbs"; +val apropC = "_aprop"; + + +end; +