explicit a-priori detection of unsuitable terms for computations
authorhaftmann
Tue Jan 24 22:29:36 2017 +0100 (2017-01-24)
changeset 64943c5618df67c2a
parent 64942 bae35a568b1b
child 64944 27b1ba3ef778
explicit a-priori detection of unsuitable terms for computations
src/Tools/Code/code_runtime.ML
     1.1 --- a/src/Tools/Code/code_runtime.ML	Tue Jan 24 09:39:21 2017 +0100
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Tue Jan 24 22:29:36 2017 +0100
     1.3 @@ -28,7 +28,7 @@
     1.4      -> Proof.context -> term -> 'a Exn.result
     1.5    val dynamic_holds_conv: Proof.context -> conv
     1.6    val static_holds_conv: { ctxt: Proof.context, consts: string list } -> Proof.context -> conv
     1.7 -  val experimental_computation: (Proof.context -> term -> 'a) cookie
     1.8 +  val experimental_computation: (term -> 'a) cookie
     1.9      -> { ctxt: Proof.context, lift_postproc: (term -> term) -> 'a -> 'a,
    1.10             terms: term list, T: typ }
    1.11      -> Proof.context -> term -> 'a (*EXPERIMENTAL!*)
    1.12 @@ -196,6 +196,8 @@
    1.13  
    1.14  (** computations -- experimental! **)
    1.15  
    1.16 +fun monomorphic T = fold_atyps ((K o K) false) T true;
    1.17 +
    1.18  fun typ_signatures_for T =
    1.19    let
    1.20      val (Ts, T') = strip_type T;
    1.21 @@ -217,23 +219,20 @@
    1.22      val var_names = map_range (fn n => "t" ^ string_of_int (n + 1));
    1.23      fun print_lhs c xs = "Const (" ^ quote c ^ ", _)"
    1.24        |> fold (fn x => fn s => s ^ " $ " ^ x) xs
    1.25 -      |> enclose "(" ")"
    1.26 -      |> prefix "ctxt ";
    1.27 +      |> enclose "(" ")";
    1.28      fun print_rhs c Ts T xs = eval_for_const (c, Ts ---> T)
    1.29        |> fold2 (fn T' => fn x => fn s =>
    1.30 -         s ^ (" (" ^ of_term_for_typ T' ^ " ctxt " ^ x ^ ")")) Ts xs
    1.31 +         s ^ (" (" ^ of_term_for_typ T' ^ " " ^ x ^ ")")) Ts xs
    1.32      fun print_eq T (c, Ts) =
    1.33        let
    1.34          val xs = var_names (length Ts);
    1.35        in print_lhs c xs ^ " = " ^ print_rhs c Ts T xs end;
    1.36 -    val err_eq =
    1.37 -      "ctxt t = error (" ^ quote "Bad term: " ^ " ^ Syntax.string_of_term ctxt t)";
    1.38      fun print_eqs T =
    1.39        let
    1.40          val typ_signs = typ_sign_for T;
    1.41          val name = of_term_for_typ T;
    1.42        in
    1.43 -        (map (print_eq T) typ_signs @ [err_eq])
    1.44 +        map (print_eq T) typ_signs
    1.45          |> map (prefix (name ^ " "))
    1.46          |> space_implode "\n  | "
    1.47        end;
    1.48 @@ -306,6 +305,27 @@
    1.49      ], map (prefix (generated_computationN ^ ".")) of_terms)
    1.50    end;
    1.51  
    1.52 +fun check_typ ctxt T t =
    1.53 +  Syntax.check_term ctxt (Type.constraint T t);
    1.54 +
    1.55 +fun check_computation_input ctxt cTs t =
    1.56 +  let
    1.57 +    fun check t = check_comb (strip_comb t)
    1.58 +    and check_comb (t as Abs _, _) =
    1.59 +          error ("Bad term, contains abstraction: " ^ Syntax.string_of_term ctxt t)
    1.60 +      | check_comb (t as Const (cT as (c, T)), ts) =
    1.61 +          let
    1.62 +            val _ = if not (member (op =) cTs cT)
    1.63 +              then error ("Bad term, computation cannot proceed on constant " ^ Syntax.string_of_term ctxt t)
    1.64 +              else ();
    1.65 +            val _ = if not (monomorphic T)
    1.66 +              then error ("Bad term, contains polymorphic constant " ^ Syntax.string_of_term ctxt t)
    1.67 +              else ();
    1.68 +            val _ = map check ts;
    1.69 +          in () end;
    1.70 +    val _ = check t;
    1.71 +  in t end;
    1.72 +
    1.73  fun compile_computation cookie ctxt T program evals vs_ty_evals deps =
    1.74    let
    1.75      val raw_cTs = case evals of
    1.76 @@ -325,12 +345,18 @@
    1.77      val compiled_computation =
    1.78        Exn.release (run_computation_text cookie ctxt comp' vs_ty_evals []);
    1.79    in fn ctxt' =>
    1.80 -    compiled_computation ctxt' o reject_vars ctxt' o Syntax.check_term ctxt' o Type.constraint T
    1.81 +    check_typ ctxt' T
    1.82 +    #> reject_vars ctxt'
    1.83 +    #> check_computation_input ctxt cTs
    1.84 +    #> compiled_computation
    1.85    end;
    1.86  
    1.87  fun experimental_computation cookie { ctxt, lift_postproc, terms = ts, T } =
    1.88    let
    1.89 -    val cTs = (fold o fold_aterms) (fn Const cT => insert (op =) cT | _ => I) ts [];
    1.90 +    val cTs = (fold o fold_aterms)
    1.91 +      (fn (t as Const (cT as (_, T))) =>
    1.92 +        if not (monomorphic T) then error ("Polymorphic constant:" ^ Syntax.string_of_term ctxt t)
    1.93 +        else insert (op =) cT | _ => I) ts [];
    1.94      val vT = TFree (singleton (Name.variant_list
    1.95        (fold (fn (_, T) => fold_atyps (fn TFree (v, _) => insert (op =) v | _ => I)
    1.96          T) cTs [])) Name.aT, []);