src/Pure/Syntax/syntax.ML
changeset 24768 123e219b66c2
parent 24709 ecfb9dcb6c4c
child 24923 9e095546cdac
     1.1 --- a/src/Pure/Syntax/syntax.ML	Sat Sep 29 21:39:52 2007 +0200
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Sat Sep 29 21:39:53 2007 +0200
     1.3 @@ -86,15 +86,34 @@
     1.4    val pretty_sort: Proof.context -> syntax -> sort -> Pretty.T
     1.5    val ambiguity_level: int ref
     1.6    val ambiguity_is_error: bool ref
     1.7 -  val install_parsers:
     1.8 -   {sort: Proof.context -> string -> sort,
     1.9 -    typ: Proof.context -> string -> typ,
    1.10 -    term: Proof.context -> string -> term,
    1.11 -    prop: Proof.context -> string -> term} -> unit
    1.12    val parse_sort: Proof.context -> string -> sort
    1.13    val parse_typ: Proof.context -> string -> typ
    1.14    val parse_term: Proof.context -> string -> term
    1.15    val parse_prop: Proof.context -> string -> term
    1.16 +  val unparse_sort: Proof.context -> sort -> Pretty.T
    1.17 +  val unparse_typ: Proof.context -> typ -> Pretty.T
    1.18 +  val unparse_term: Proof.context -> term -> Pretty.T
    1.19 +  val install_operations:
    1.20 +   {parse_sort: Proof.context -> string -> sort,
    1.21 +    parse_typ: Proof.context -> string -> typ,
    1.22 +    parse_term: Proof.context -> string -> term,
    1.23 +    parse_prop: Proof.context -> string -> term,
    1.24 +    unparse_sort: Proof.context -> sort -> Pretty.T,
    1.25 +    unparse_typ: Proof.context -> typ -> Pretty.T,
    1.26 +    unparse_term: Proof.context -> term -> Pretty.T} -> unit
    1.27 +  val print_checks: Proof.context -> unit
    1.28 +  val add_typ_check: int -> string ->
    1.29 +    (typ list -> Proof.context -> typ list * Proof.context) ->
    1.30 +    Context.generic -> Context.generic
    1.31 +  val add_term_check: int -> string ->
    1.32 +    (term list -> Proof.context -> term list * Proof.context) ->
    1.33 +    Context.generic -> Context.generic
    1.34 +  val add_typ_uncheck: int -> string ->
    1.35 +    (typ list -> Proof.context -> typ list * Proof.context) ->
    1.36 +    Context.generic -> Context.generic
    1.37 +  val add_term_uncheck: int -> string ->
    1.38 +    (term list -> Proof.context -> term list * Proof.context) ->
    1.39 +    Context.generic -> Context.generic
    1.40    val check_sort: Proof.context -> sort -> sort
    1.41    val check_typ: Proof.context -> typ -> typ
    1.42    val check_term: Proof.context -> term -> term
    1.43 @@ -102,10 +121,8 @@
    1.44    val check_typs: Proof.context -> typ list -> typ list
    1.45    val check_terms: Proof.context -> term list -> term list
    1.46    val check_props: Proof.context -> term list -> term list
    1.47 -  val add_typ_check: (typ list -> Proof.context -> typ list * Proof.context) ->
    1.48 -    Context.generic -> Context.generic
    1.49 -  val add_term_check: (term list -> Proof.context -> term list * Proof.context) ->
    1.50 -    Context.generic -> Context.generic
    1.51 +  val uncheck_typs: Proof.context -> typ list -> typ list
    1.52 +  val uncheck_terms: Proof.context -> term list -> term list
    1.53    val read_sort: Proof.context -> string -> sort
    1.54    val read_typ: Proof.context -> string -> typ
    1.55    val read_term: Proof.context -> string -> term
    1.56 @@ -602,82 +619,124 @@
    1.57  
    1.58  
    1.59  
    1.60 -(** generic parsing and type-checking **)
    1.61 -
    1.62 -(* parsing *)
    1.63 +(** inner syntax operations **)
    1.64  
    1.65 -type parsers =
    1.66 - {sort: Proof.context -> string -> sort,
    1.67 -  typ: Proof.context -> string -> typ,
    1.68 -  term: Proof.context -> string -> term,
    1.69 -  prop: Proof.context -> string -> term};
    1.70 +(* (un)parsing *)
    1.71  
    1.72  local
    1.73 -  val parsers = ref (NONE: parsers option);
    1.74 +  type operations =
    1.75 +   {parse_sort: Proof.context -> string -> sort,
    1.76 +    parse_typ: Proof.context -> string -> typ,
    1.77 +    parse_term: Proof.context -> string -> term,
    1.78 +    parse_prop: Proof.context -> string -> term,
    1.79 +    unparse_sort: Proof.context -> sort -> Pretty.T,
    1.80 +    unparse_typ: Proof.context -> typ -> Pretty.T,
    1.81 +    unparse_term: Proof.context -> term -> Pretty.T};
    1.82 +
    1.83 +  val operations = ref (NONE: operations option);
    1.84 +
    1.85 +  fun operation which ctxt x =
    1.86 +    (case ! operations of
    1.87 +      NONE => error "Inner syntax operations not yet installed"
    1.88 +    | SOME ops => which ops ctxt x);
    1.89  in
    1.90 -  fun install_parsers ps = CRITICAL (fn () =>
    1.91 -    if is_some (! parsers) then error "Inner syntax parsers already installed"
    1.92 -    else parsers := SOME ps);
    1.93  
    1.94 -  fun parse which ctxt s =
    1.95 -    (case ! parsers of
    1.96 -      NONE => error "Inner syntax parsers not yet installed"
    1.97 -    | SOME ps => which ps ctxt s);
    1.98 +val parse_sort = operation #parse_sort;
    1.99 +val parse_typ = operation #parse_typ;
   1.100 +val parse_term = operation #parse_term;
   1.101 +val parse_prop = operation #parse_prop;
   1.102 +val unparse_sort = operation #unparse_sort;
   1.103 +val unparse_typ = operation #unparse_typ;
   1.104 +val unparse_term = operation #unparse_term;
   1.105 +
   1.106 +fun install_operations ops = CRITICAL (fn () =>
   1.107 +  if is_some (! operations) then error "Inner syntax operations already installed"
   1.108 +  else operations := SOME ops);
   1.109 +
   1.110  end;
   1.111  
   1.112 -val parse_sort = parse #sort;
   1.113 -val parse_typ = parse #typ;
   1.114 -val parse_term = parse #term;
   1.115 -val parse_prop = parse #prop;
   1.116  
   1.117 -
   1.118 -(* checking types/terms *)
   1.119 +(* context-sensitive (un)checking *)
   1.120  
   1.121  local
   1.122  
   1.123 +type key = int * bool;
   1.124 +type 'a check = 'a list -> Proof.context -> 'a list * Proof.context;
   1.125 +
   1.126  structure Checks = GenericDataFun
   1.127  (
   1.128    type T =
   1.129 -    ((typ list -> Proof.context -> typ list * Proof.context) * stamp) list *
   1.130 -    ((term list -> Proof.context -> term list * Proof.context) * stamp) list;
   1.131 +    ((key * ((string * typ check) * stamp) list) list *
   1.132 +     (key * ((string * term check) * stamp) list) list);
   1.133    val empty = ([], []);
   1.134    val extend = I;
   1.135    fun merge _ ((typ_checks1, term_checks1), (typ_checks2, term_checks2)) : T =
   1.136 -    (Library.merge (eq_snd op =) (typ_checks1, typ_checks2),
   1.137 -     Library.merge (eq_snd op =) (term_checks1, term_checks2));
   1.138 +    (AList.join (op =) (K (Library.merge (eq_snd (op =)))) (typ_checks1, typ_checks2),
   1.139 +     AList.join (op =) (K (Library.merge (eq_snd (op =)))) (term_checks1, term_checks2));
   1.140  );
   1.141  
   1.142 -fun gen_check which eq ctxt0 xs0 =
   1.143 +fun gen_add which (key: key) name f =
   1.144 +  Checks.map (which (AList.map_default op = (key, []) (cons ((name, f), stamp ()))));
   1.145 +
   1.146 +fun gen_check which uncheck eq ctxt0 xs0 =
   1.147    let
   1.148 -    val funs = map fst (rev (which (Checks.get (Context.Proof ctxt0))));
   1.149 -
   1.150 -    fun check [] xs ctxt = (xs, ctxt)
   1.151 -      | check (f :: fs) xs ctxt = f xs ctxt |-> check fs;
   1.152 +    val funs = which (Checks.get (Context.Proof ctxt0))
   1.153 +      |> map_filter (fn ((i, u), fs) => if uncheck = u then SOME (i, map (snd o fst) fs) else NONE)
   1.154 +      |> Library.sort (int_ord o pairself fst)
   1.155 +      |> not uncheck ? map (apsnd rev);
   1.156  
   1.157 -    fun check_fixpoint xs ctxt =
   1.158 -      let val (xs', ctxt') = check funs xs ctxt in
   1.159 +    fun check_fixpoint fs (xs, ctxt) =
   1.160 +      let val (xs', ctxt') = fold uncurry fs (xs, ctxt) in
   1.161          if eq_list eq (xs, xs') then (xs, ctxt)
   1.162 -        else check_fixpoint xs' ctxt'
   1.163 +        else check_fixpoint fs (xs', ctxt')
   1.164        end;
   1.165 -  in #1 (case funs of [f] => f xs0 ctxt0 | _ => check_fixpoint xs0 ctxt0) end;
   1.166 +  in #1 (fold (check_fixpoint o snd) funs (xs0, ctxt0)) end;
   1.167 +
   1.168 +fun map_sort f S =
   1.169 +  (case f (TFree ("", S)) of
   1.170 +    TFree ("", S') => S'
   1.171 +  | T => raise TYPE ("map_sort", [TFree ("", S), T], []));
   1.172  
   1.173  in
   1.174  
   1.175 -val check_typs = gen_check fst (op =);
   1.176 -val check_terms = gen_check snd (op aconv);
   1.177 +fun print_checks ctxt =
   1.178 +  let
   1.179 +    fun split_checks checks =
   1.180 +      List.partition (fn ((_, un), _) => not un) checks
   1.181 +      |> pairself (map (fn ((i, _), fs) => (i, map (fst o fst) fs))
   1.182 +          #> sort (int_ord o pairself fst));
   1.183 +    fun pretty_checks kind checks =
   1.184 +      checks |> map (fn (i, names) => Pretty.block
   1.185 +        [Pretty.str (kind ^ " (stage " ^ signed_string_of_int i ^ "):"),
   1.186 +          Pretty.brk 1, Pretty.strs names]);
   1.187 +
   1.188 +    val (typs, terms) = Checks.get (Context.Proof ctxt);
   1.189 +    val (typ_checks, typ_unchecks) = split_checks typs;
   1.190 +    val (term_checks, term_unchecks) = split_checks terms;
   1.191 +  in
   1.192 +    pretty_checks "typ_checks" typ_checks @
   1.193 +    pretty_checks "term_checks" term_checks @
   1.194 +    pretty_checks "typ_unchecks" typ_unchecks @
   1.195 +    pretty_checks "term_unchecks" term_unchecks
   1.196 +  end |> Pretty.chunks |> Pretty.writeln;
   1.197 +
   1.198 +fun add_typ_check stage = gen_add apfst (stage, false);
   1.199 +fun add_term_check stage = gen_add apsnd (stage, false);
   1.200 +fun add_typ_uncheck stage = gen_add apfst (stage, true);
   1.201 +fun add_term_uncheck stage = gen_add apsnd (stage, true);
   1.202 +
   1.203 +val check_typs = gen_check fst false (op =);
   1.204 +val check_terms = gen_check snd false (op aconv);
   1.205  fun check_props ctxt = map (TypeInfer.constrain propT) #> check_terms ctxt;
   1.206  
   1.207  val check_typ = singleton o check_typs;
   1.208  val check_term = singleton o check_terms;
   1.209  val check_prop = singleton o check_props;
   1.210 +val check_sort = map_sort o check_typ;
   1.211  
   1.212 -fun check_sort ctxt S =
   1.213 -  (case singleton (check_typs ctxt) (TFree ("", S)) of   (* FIXME TypeInfer.invent_type (!?) *)
   1.214 -    TFree ("", S') => S'
   1.215 -  | T => raise TYPE ("check_sort", [T], []));
   1.216 -
   1.217 -fun add_typ_check f = Checks.map (apfst (cons (f, stamp ())));
   1.218 -fun add_term_check f = Checks.map (apsnd (cons (f, stamp ())));
   1.219 +val uncheck_typs = gen_check fst true (op =);
   1.220 +val uncheck_terms = gen_check snd true (op aconv);
   1.221 +val uncheck_sort = map_sort o singleton o uncheck_typs;
   1.222  
   1.223  end;
   1.224