inline old Record.read_typ/cert_typ;
authorwenzelm
Thu Apr 15 15:39:50 2010 +0200 (2010-04-15)
changeset 361495ca66e58dcfa
parent 36148 4ddcc2b07891
child 36150 123f721c9a37
inline old Record.read_typ/cert_typ;
spelling;
src/HOL/Statespace/state_space.ML
     1.1 --- a/src/HOL/Statespace/state_space.ML	Thu Apr 15 15:38:58 2010 +0200
     1.2 +++ b/src/HOL/Statespace/state_space.ML	Thu Apr 15 15:39:50 2010 +0200
     1.3 @@ -478,6 +478,21 @@
     1.4      Type (name, Ts) => (Ts, name)
     1.5    | T => error ("Bad parent statespace specification: " ^ Syntax.string_of_typ ctxt T));
     1.6  
     1.7 +fun read_typ ctxt raw_T env =
     1.8 +  let
     1.9 +    val ctxt' = fold (Variable.declare_typ o TFree) env ctxt;
    1.10 +    val T = Syntax.read_typ ctxt' raw_T;
    1.11 +    val env' = OldTerm.add_typ_tfrees (T, env);
    1.12 +  in (T, env') end;
    1.13 +
    1.14 +fun cert_typ ctxt raw_T env =
    1.15 +  let
    1.16 +    val thy = ProofContext.theory_of ctxt;
    1.17 +    val T = Type.no_tvars (Sign.certify_typ thy raw_T)
    1.18 +      handle TYPE (msg, _, _) => error msg;
    1.19 +    val env' = OldTerm.add_typ_tfrees (T, env);
    1.20 +  in (T, env') end;
    1.21 +
    1.22  fun gen_define_statespace prep_typ state_space args name parents comps thy =
    1.23    let (* - args distinct
    1.24           - only args may occur in comps and parent-instantiations
    1.25 @@ -500,7 +515,7 @@
    1.26  
    1.27          val (Ts',env') = fold_map (prep_typ ctxt) Ts env
    1.28              handle ERROR msg => cat_error msg
    1.29 -                    ("The error(s) above occured in parent statespace specification "
    1.30 +                    ("The error(s) above occurred in parent statespace specification "
    1.31                      ^ quote pname);
    1.32          val err_insts = if length args <> length Ts' then
    1.33              ["number of type instantiation(s) does not match arguments of parent statespace "
    1.34 @@ -539,7 +554,7 @@
    1.35  
    1.36      fun prep_comp (n,T) env =
    1.37        let val (T', env') = prep_typ ctxt T env handle ERROR msg =>
    1.38 -       cat_error msg ("The error(s) above occured in component " ^ quote n)
    1.39 +       cat_error msg ("The error(s) above occurred in component " ^ quote n)
    1.40        in ((n,T'), env') end;
    1.41  
    1.42      val (comps',env') = fold_map prep_comp comps env;
    1.43 @@ -579,8 +594,8 @@
    1.44    end
    1.45    handle ERROR msg => cat_error msg ("Failed to define statespace " ^ quote name);
    1.46  
    1.47 -val define_statespace = gen_define_statespace Record.read_typ NONE;
    1.48 -val define_statespace_i = gen_define_statespace Record.cert_typ;
    1.49 +val define_statespace = gen_define_statespace read_typ NONE;
    1.50 +val define_statespace_i = gen_define_statespace cert_typ;
    1.51  
    1.52  
    1.53  (*** parse/print - translations ***)