src/Pure/Syntax/syntax.ML
changeset 24923 9e095546cdac
parent 24768 123e219b66c2
child 24970 050afeec89a7
     1.1 --- a/src/Pure/Syntax/syntax.ML	Tue Oct 09 00:20:22 2007 +0200
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Tue Oct 09 00:20:23 2007 +0200
     1.3 @@ -81,9 +81,9 @@
     1.4    val standard_parse_typ: Proof.context -> syntax -> ((indexname * sort) list -> indexname -> sort) ->
     1.5      (sort -> sort) -> string -> typ
     1.6    val standard_parse_sort: Proof.context -> syntax -> (sort -> sort) -> string -> sort
     1.7 -  val pretty_term: (string -> xstring) -> Proof.context -> syntax -> bool -> term -> Pretty.T
     1.8 -  val pretty_typ: Proof.context -> syntax -> typ -> Pretty.T
     1.9 -  val pretty_sort: Proof.context -> syntax -> sort -> Pretty.T
    1.10 +  val standard_unparse_term: (string -> xstring) -> Proof.context -> syntax -> bool -> term -> Pretty.T
    1.11 +  val standard_unparse_typ: Proof.context -> syntax -> typ -> Pretty.T
    1.12 +  val standard_unparse_sort: Proof.context -> syntax -> sort -> Pretty.T
    1.13    val ambiguity_level: int ref
    1.14    val ambiguity_is_error: bool ref
    1.15    val parse_sort: Proof.context -> string -> sort
    1.16 @@ -91,6 +91,8 @@
    1.17    val parse_term: Proof.context -> string -> term
    1.18    val parse_prop: Proof.context -> string -> term
    1.19    val unparse_sort: Proof.context -> sort -> Pretty.T
    1.20 +  val unparse_classrel: Proof.context -> class list -> Pretty.T
    1.21 +  val unparse_arity: Proof.context -> arity -> Pretty.T
    1.22    val unparse_typ: Proof.context -> typ -> Pretty.T
    1.23    val unparse_term: Proof.context -> term -> Pretty.T
    1.24    val install_operations:
    1.25 @@ -121,6 +123,9 @@
    1.26    val check_typs: Proof.context -> typ list -> typ list
    1.27    val check_terms: Proof.context -> term list -> term list
    1.28    val check_props: Proof.context -> term list -> term list
    1.29 +  val uncheck_sort: Proof.context -> sort -> sort
    1.30 +  val uncheck_arity: Proof.context -> arity -> arity
    1.31 +  val uncheck_classrel: Proof.context -> class list -> class list
    1.32    val uncheck_typs: Proof.context -> typ list -> typ list
    1.33    val uncheck_terms: Proof.context -> term list -> term list
    1.34    val read_sort: Proof.context -> string -> sort
    1.35 @@ -133,6 +138,16 @@
    1.36    val read_typ_global: theory -> string -> typ
    1.37    val read_term_global: theory -> string -> term
    1.38    val read_prop_global: theory -> string -> term
    1.39 +  val pretty_term: Proof.context -> term -> Pretty.T
    1.40 +  val pretty_typ: Proof.context -> typ -> Pretty.T
    1.41 +  val pretty_sort: Proof.context -> sort -> Pretty.T
    1.42 +  val pretty_classrel: Proof.context -> class list -> Pretty.T
    1.43 +  val pretty_arity: Proof.context -> arity -> Pretty.T
    1.44 +  val string_of_term: Proof.context -> term -> string
    1.45 +  val string_of_typ: Proof.context -> typ -> string
    1.46 +  val string_of_sort: Proof.context -> sort -> string
    1.47 +  val string_of_classrel: Proof.context -> class list -> string
    1.48 +  val string_of_arity: Proof.context -> arity -> string
    1.49  end;
    1.50  
    1.51  structure Syntax: SYNTAX =
    1.52 @@ -537,7 +552,6 @@
    1.53          Ast.str_of_ast lhs ^ "  ->  " ^ Ast.str_of_ast rhs)
    1.54    | NONE => rule);
    1.55  
    1.56 -
    1.57  fun read_pattern ctxt is_logtype syn (root, str) =
    1.58    let
    1.59      val Syntax ({consts, ...}, _) = syn;
    1.60 @@ -572,9 +586,11 @@
    1.61  
    1.62  
    1.63  
    1.64 -(** pretty terms, typs, sorts **)
    1.65 +(** unparse terms, typs, sorts **)
    1.66  
    1.67 -fun pretty_t t_to_ast prt_t markup ctxt (syn as Syntax (tabs, _)) curried t =
    1.68 +local
    1.69 +
    1.70 +fun unparse_t t_to_ast prt_t markup ctxt (syn as Syntax (tabs, _)) curried t =
    1.71    let
    1.72      val {print_trtab, print_ruletab, print_ast_trtab, tokentrtab, prtabs, ...} = tabs;
    1.73      val ast = t_to_ast ctxt (lookup_tr' print_trtab) t;
    1.74 @@ -584,12 +600,18 @@
    1.75        (Ast.normalize_ast (Symtab.lookup_list print_ruletab) ast))
    1.76    end;
    1.77  
    1.78 -fun pretty_term extern =
    1.79 -  pretty_t Printer.term_to_ast (Printer.pretty_term_ast extern) Markup.term;
    1.80 -fun pretty_typ ctxt syn =
    1.81 -  pretty_t Printer.typ_to_ast Printer.pretty_typ_ast Markup.typ ctxt syn false;
    1.82 -fun pretty_sort ctxt syn =
    1.83 -  pretty_t Printer.sort_to_ast Printer.pretty_typ_ast Markup.sort ctxt syn false;
    1.84 +in
    1.85 +
    1.86 +fun standard_unparse_term extern =
    1.87 +  unparse_t Printer.term_to_ast (Printer.pretty_term_ast extern) Markup.term;
    1.88 +
    1.89 +fun standard_unparse_typ ctxt syn =
    1.90 +  unparse_t Printer.typ_to_ast Printer.pretty_typ_ast Markup.typ ctxt syn false;
    1.91 +
    1.92 +fun standard_unparse_sort ctxt syn =
    1.93 +  unparse_t Printer.sort_to_ast Printer.pretty_typ_ast Markup.sort ctxt syn false;
    1.94 +
    1.95 +end;
    1.96  
    1.97  
    1.98  
    1.99 @@ -695,7 +717,7 @@
   1.100  fun map_sort f S =
   1.101    (case f (TFree ("", S)) of
   1.102      TFree ("", S') => S'
   1.103 -  | T => raise TYPE ("map_sort", [TFree ("", S), T], []));
   1.104 +  | _ => raise TYPE ("map_sort", [TFree ("", S)], []));
   1.105  
   1.106  in
   1.107  
   1.108 @@ -741,7 +763,33 @@
   1.109  end;
   1.110  
   1.111  
   1.112 -(* combined operations *)
   1.113 +(* derived operations for classrel and arity *)
   1.114 +
   1.115 +val uncheck_classrel = map o singleton o uncheck_sort;
   1.116 +
   1.117 +fun unparse_classrel ctxt cs = Pretty.block (flat
   1.118 +  (separate [Pretty.str " <", Pretty.brk 1] (map (single o unparse_sort ctxt o single) cs)));
   1.119 +
   1.120 +fun uncheck_arity ctxt (a, Ss, S) =
   1.121 +  let
   1.122 +    val T = Type (a, replicate (length Ss) dummyT);
   1.123 +    val a' =
   1.124 +      (case singleton (uncheck_typs ctxt) T of
   1.125 +        Type (a', _) => a'
   1.126 +      | T => raise TYPE ("uncheck_arity", [T], []));
   1.127 +    val Ss' = map (uncheck_sort ctxt) Ss;
   1.128 +    val S' = uncheck_sort ctxt S;
   1.129 +  in (a', Ss', S') end;
   1.130 +
   1.131 +fun unparse_arity ctxt (a, Ss, S) =
   1.132 +  let
   1.133 +    val dom =
   1.134 +      if null Ss then []
   1.135 +      else [Pretty.list "(" ")" (map (unparse_sort ctxt) Ss), Pretty.brk 1];
   1.136 +  in Pretty.block ([Pretty.str (a ^ " ::"), Pretty.brk 1] @ dom @ [unparse_sort ctxt S]) end;
   1.137 +
   1.138 +
   1.139 +(* read = parse + check *)
   1.140  
   1.141  fun read_sort ctxt = parse_sort ctxt #> check_sort ctxt;
   1.142  fun read_typ ctxt = parse_typ ctxt #> singleton (check_typs ctxt);
   1.143 @@ -758,6 +806,21 @@
   1.144  val read_prop_global = read_prop o ProofContext.init;
   1.145  
   1.146  
   1.147 +(* pretty = uncheck + unparse *)
   1.148 +
   1.149 +fun pretty_sort ctxt = uncheck_sort ctxt #> unparse_sort ctxt;
   1.150 +fun pretty_classrel ctxt = uncheck_classrel ctxt #> unparse_classrel ctxt;
   1.151 +fun pretty_arity ctxt = uncheck_arity ctxt #> unparse_arity ctxt;
   1.152 +fun pretty_typ ctxt = singleton (uncheck_typs ctxt) #> unparse_typ ctxt;
   1.153 +fun pretty_term ctxt = singleton (uncheck_terms ctxt) #> unparse_term ctxt;
   1.154 +
   1.155 +val string_of_sort = Pretty.string_of oo pretty_sort;
   1.156 +val string_of_classrel = Pretty.string_of oo pretty_classrel;
   1.157 +val string_of_arity = Pretty.string_of oo pretty_arity;
   1.158 +val string_of_typ = Pretty.string_of oo pretty_typ;
   1.159 +val string_of_term = Pretty.string_of oo pretty_term;
   1.160 +
   1.161 +
   1.162  (*export parts of internal Syntax structures*)
   1.163  open Lexicon SynExt Ast Parser TypeExt SynTrans Mixfix Printer;
   1.164