added first version of datatype antiquotation
authorhaftmann
Fri Feb 22 12:01:54 2008 +0100 (2008-02-22)
changeset 2611191e0999b075f
parent 26110 06eacfd8dd9f
child 26112 ac2ce7242eae
added first version of datatype antiquotation
src/HOL/Tools/datatype_package.ML
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Fri Feb 22 12:01:52 2008 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Fri Feb 22 12:01:54 2008 +0100
     1.3 @@ -886,6 +886,52 @@
     1.4  val add_datatype = gen_add_datatype read_typ true;
     1.5  
     1.6  
     1.7 +(** a datatype antiquotation **)
     1.8 +
     1.9 +local
    1.10 +
    1.11 +val sym_datatype = Pretty.str "\\isacommand{datatype}";
    1.12 +val sym_binder = Pretty.str "{\\isacharequal}";
    1.13 +val sym_of = Pretty.str "of";
    1.14 +val sym_sep = Pretty.str "{\\isacharbar}";
    1.15 +
    1.16 +in
    1.17 +
    1.18 +fun args_datatype (ctxt, args) =
    1.19 +  let
    1.20 +    val (tyco, (ctxt', args')) = Args.tyname (ctxt, args);
    1.21 +    val thy = Context.theory_of ctxt';
    1.22 +    val spec = the_datatype_spec thy tyco;
    1.23 +  in ((tyco, spec), (ctxt', args')) end;
    1.24 +
    1.25 +fun pretty_datatype ctxt (dtco, (vs, cos)) =
    1.26 +  let
    1.27 +    val ty = Type (dtco, map TFree vs);
    1.28 +    fun pretty_typ_br ty =
    1.29 +      let
    1.30 +        val p = Syntax.pretty_typ ctxt ty;
    1.31 +        val s = explode (Pretty.str_of p);
    1.32 +      in if member (op =) s " " then Pretty.enclose "(" ")" [p]
    1.33 +        else p
    1.34 +      end;
    1.35 +    fun pretty_constr (co, []) =
    1.36 +          Syntax.pretty_term ctxt (Const (co, ty))
    1.37 +      | pretty_constr (co, [ty']) =
    1.38 +          (Pretty.block o Pretty.breaks)
    1.39 +            [Syntax.pretty_term ctxt (Const (co, ty' --> ty)),
    1.40 +              sym_of, Syntax.pretty_typ ctxt ty']
    1.41 +      | pretty_constr (co, tys) =
    1.42 +          (Pretty.block o Pretty.breaks)
    1.43 +            (Syntax.pretty_term ctxt (Const (co, tys ---> ty)) ::
    1.44 +              sym_of :: map pretty_typ_br tys);
    1.45 +  in (Pretty.block o Pretty.breaks) (
    1.46 +    sym_datatype
    1.47 +    :: Syntax.pretty_typ ctxt ty
    1.48 +    :: sym_binder
    1.49 +    :: separate sym_sep (map pretty_constr cos)
    1.50 +  ) end
    1.51 +
    1.52 +end;
    1.53  
    1.54  (** package setup **)
    1.55  
    1.56 @@ -933,6 +979,10 @@
    1.57    OuterSyntax.command "rep_datatype" "represent existing types inductively" K.thy_decl
    1.58      (rep_datatype_decl >> (Toplevel.theory o mk_rep_datatype));
    1.59  
    1.60 +val _ =
    1.61 +  ThyOutput.add_commands [("datatype",
    1.62 +    ThyOutput.args args_datatype (ThyOutput.output pretty_datatype))];
    1.63 +
    1.64  end;
    1.65  
    1.66