src/Pure/Syntax/syntax.ML
changeset 24488 646e782ba8ff
parent 24372 743575ccfec8
child 24512 fc4959967b30
     1.1 --- a/src/Pure/Syntax/syntax.ML	Thu Aug 30 15:04:49 2007 +0200
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Thu Aug 30 15:04:50 2007 +0200
     1.3 @@ -99,18 +99,20 @@
     1.4    val global_parse_typ: theory -> string -> typ
     1.5    val global_parse_term: theory -> string -> term
     1.6    val global_parse_prop: theory -> string -> term
     1.7 -  val add_type_check: (term list -> Proof.context -> Term.term list * Proof.context) ->
     1.8 -    Context.generic -> Context.generic
     1.9 -  val type_check: term list -> Proof.context -> term list * Proof.context
    1.10 +  val check_sort: Proof.context -> sort -> sort
    1.11 +  val check_typs: Proof.context -> typ list -> typ list
    1.12    val check_terms: Proof.context -> term list -> term list
    1.13    val check_props: Proof.context -> term list -> term list
    1.14 -  val check_typs: Proof.context -> typ list -> typ list
    1.15 +  val add_typ_check: (typ list -> Proof.context -> typ list * Proof.context) ->
    1.16 +    Context.generic -> Context.generic
    1.17 +  val add_term_check: (term list -> Proof.context -> term list * Proof.context) ->
    1.18 +    Context.generic -> Context.generic
    1.19    val read_sort: Proof.context -> string -> sort
    1.20    val read_typ: Proof.context -> string -> typ
    1.21 +  val read_term: Proof.context -> string -> term
    1.22 +  val read_prop: Proof.context -> string -> term
    1.23    val read_terms: Proof.context -> string list -> term list
    1.24    val read_props: Proof.context -> string list -> term list
    1.25 -  val read_term: Proof.context -> string -> term
    1.26 -  val read_prop: Proof.context -> string -> term
    1.27    val global_read_sort: theory -> string -> sort
    1.28    val global_read_typ: theory -> string -> typ
    1.29    val global_read_term: theory -> string -> term
    1.30 @@ -635,40 +637,53 @@
    1.31  val global_parse_prop = parse_prop o ProofContext.init;
    1.32  
    1.33  
    1.34 -(* type-checking *)
    1.35 +(* checking types/terms *)
    1.36  
    1.37 -structure TypeCheck = GenericDataFun
    1.38 +local
    1.39 +
    1.40 +structure Checks = GenericDataFun
    1.41  (
    1.42 -  type T = ((term list -> Proof.context -> term list * Proof.context) * stamp) list;
    1.43 -  val empty = [];
    1.44 +  type T =
    1.45 +    ((typ list -> Proof.context -> typ list * Proof.context) * stamp) list *
    1.46 +    ((term list -> Proof.context -> term list * Proof.context) * stamp) list;
    1.47 +  val empty = ([], []);
    1.48    val extend = I;
    1.49 -  fun merge _ type_checks : T = Library.merge (eq_snd op =) type_checks;
    1.50 +  fun merge _ ((typ_checks1, term_checks1), (typ_checks2, term_checks2)) : T =
    1.51 +    (Library.merge (eq_snd op =) (typ_checks1, typ_checks2),
    1.52 +     Library.merge (eq_snd op =) (term_checks1, term_checks2));
    1.53  );
    1.54  
    1.55 -fun add_type_check f = TypeCheck.map (cons (f, stamp ()));
    1.56 -
    1.57 -fun type_check ts0 ctxt0 =
    1.58 +fun gen_check which eq ctxt0 xs0 =
    1.59    let
    1.60 -    val funs = map #1 (rev (TypeCheck.get (Context.Proof ctxt0)));
    1.61 -    fun check [] ts ctxt = (ts, ctxt)
    1.62 -      | check (f :: fs) ts ctxt = f ts ctxt |-> check fs;
    1.63 +    val funs = map fst (rev (which (Checks.get (Context.Proof ctxt0))));
    1.64 +
    1.65 +    fun check [] xs ctxt = (xs, ctxt)
    1.66 +      | check (f :: fs) xs ctxt = f xs ctxt |-> check fs;
    1.67  
    1.68 -    fun check_fixpoint ts ctxt =
    1.69 -      let val (ts', ctxt') = check funs ts ctxt in
    1.70 -        if eq_list (op aconv) (ts, ts') then (ts, ctxt)
    1.71 -        else check_fixpoint ts' ctxt'
    1.72 +    fun check_fixpoint xs ctxt =
    1.73 +      let val (xs', ctxt') = check funs xs ctxt in
    1.74 +        if eq_list eq (xs, xs') then (xs, ctxt)
    1.75 +        else check_fixpoint xs' ctxt'
    1.76        end;
    1.77 -  in (case funs of [f] => f ts0 ctxt0 | _ => check_fixpoint ts0 ctxt0) end;
    1.78 +  in #1 (case funs of [f] => f xs0 ctxt0 | _ => check_fixpoint xs0 ctxt0) end;
    1.79 +
    1.80 +in
    1.81  
    1.82 -fun check_terms ctxt ts = #1 (type_check ts ctxt);
    1.83 +val check_typs = gen_check fst (op =);
    1.84 +val check_terms = gen_check snd (op aconv);
    1.85 +
    1.86  fun check_props ctxt = map (fn t => TypeInfer.constrain t propT) #> check_terms ctxt;
    1.87 -fun check_typs ctxt = map Logic.mk_type #> check_terms ctxt #> map Logic.dest_type;
    1.88  
    1.89  fun check_sort ctxt S =
    1.90    (case singleton (check_typs ctxt) (TFree ("", S)) of   (* FIXME TypeInfer.invent_type (!?) *)
    1.91      TFree ("", S') => S'
    1.92    | T => raise TYPE ("check_sort", [T], []));
    1.93  
    1.94 +fun add_typ_check f = Checks.map (apfst (cons (f, stamp ())));
    1.95 +fun add_term_check f = Checks.map (apsnd (cons (f, stamp ())));
    1.96 +
    1.97 +end;
    1.98 +
    1.99  
   1.100  (* combined operations *)
   1.101