src/Tools/Code/code_runtime.ML
changeset 64991 d2c79b16e133
parent 64990 c6a7de505796
child 64992 41e2c3617582
     1.1 --- a/src/Tools/Code/code_runtime.ML	Mon Feb 06 20:56:34 2017 +0100
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Mon Feb 06 20:56:35 2017 +0100
     1.3 @@ -361,23 +361,32 @@
     1.4          ] |> rpair of_term_names
     1.5        end;
     1.6  
     1.7 -fun checked_computation cTs T raw_computation ctxt =
     1.8 +fun prechecked_computation T raw_computation ctxt =
     1.9    check_typ ctxt T
    1.10    #> reject_vars ctxt
    1.11 -  #> check_computation_input ctxt cTs
    1.12 +  #> raw_computation ctxt;
    1.13 +
    1.14 +fun prechecked_conv T raw_conv ctxt =
    1.15 +  tap (check_typ ctxt T o reject_vars ctxt o Thm.term_of)
    1.16 +  #> raw_conv ctxt;
    1.17 +
    1.18 +fun checked_computation cTs raw_computation ctxt =
    1.19 +  check_computation_input ctxt cTs
    1.20    #> Exn.capture raw_computation
    1.21    #> partiality_as_none;
    1.22  
    1.23  fun mount_computation ctxt cTs T raw_computation lift_postproc =
    1.24 -  Code_Preproc.static_value { ctxt = ctxt, lift_postproc = lift_postproc, consts = [] }
    1.25 -    (K (checked_computation cTs T raw_computation));
    1.26 +  prechecked_computation T (Code_Preproc.static_value
    1.27 +    { ctxt = ctxt, lift_postproc = lift_postproc, consts = [] }
    1.28 +    (K (checked_computation cTs raw_computation)));
    1.29  
    1.30  fun mount_computation_conv ctxt cTs T raw_computation conv =
    1.31 -  Code_Preproc.static_conv { ctxt = ctxt, consts = [] }
    1.32 +  prechecked_conv T (Code_Preproc.static_conv
    1.33 +    { ctxt = ctxt, consts = [] }
    1.34      (K (fn ctxt' => fn t =>
    1.35 -      case checked_computation cTs T raw_computation ctxt' t of
    1.36 +      case checked_computation cTs raw_computation ctxt' t of
    1.37          SOME x => conv x
    1.38 -      | NONE => Conv.all_conv));
    1.39 +      | NONE => Conv.all_conv)));
    1.40  
    1.41  local
    1.42