# HG changeset patch
# User haftmann
# Date 1486410992 -3600
# Node ID 93aaff2b0ae0db91650cde515ad30e8949b1613c
# Parent  1985502518ce8b8eebf34142fb82181a20e6c58a
computations and partiality

diff -r 1985502518ce -r 93aaff2b0ae0 src/HOL/ex/Computations.thy
--- a/src/HOL/ex/Computations.thy	Mon Feb 06 20:56:30 2017 +0100
+++ b/src/HOL/ex/Computations.thy	Mon Feb 06 20:56:32 2017 +0100
@@ -30,14 +30,14 @@
 
 val comp_nat = @{computation "0 :: nat" Suc
   "plus :: nat \<Rightarrow>_" "times :: nat \<Rightarrow> _" fib :: nat}
-  (fn post => post o HOLogic.mk_nat o int_of_nat);
+  (fn post => post o HOLogic.mk_nat o int_of_nat o the);
 
 val comp_numeral = @{computation "0 :: nat" "1 :: nat" "2 :: nat" "3 :: nat" :: nat}
-  (fn post => post o HOLogic.mk_nat o int_of_nat);
+  (fn post => post o HOLogic.mk_nat o int_of_nat o the);
 
 val comp_bool = @{computation True False HOL.conj HOL.disj HOL.implies
   HOL.iff even "less_eq :: nat \<Rightarrow> _" "less :: nat \<Rightarrow> _" "HOL.eq :: nat \<Rightarrow> _" :: bool }
-  (K I);
+  (K the);
 
 end
 \<close>
diff -r 1985502518ce -r 93aaff2b0ae0 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Mon Feb 06 20:56:30 2017 +0100
+++ b/src/Tools/Code/code_runtime.ML	Mon Feb 06 20:56:32 2017 +0100
@@ -33,7 +33,7 @@
   datatype truth = Holds
   val put_truth: (unit -> truth) -> Proof.context -> Proof.context
   val mount_computation: Proof.context -> (string * typ) list -> typ
-    -> (term -> 'ml) -> ((term -> term) -> 'ml -> 'a) -> Proof.context -> term -> 'a
+    -> (term -> 'ml) -> ((term -> term) -> 'ml option -> 'a) -> Proof.context -> term -> 'a
   val polyml_as_definition: (binding * typ) list -> Path.T list -> theory -> theory
   val trace: bool Config.T
 end;
@@ -354,7 +354,8 @@
   check_typ ctxt T
   #> reject_vars ctxt
   #> check_computation_input ctxt cTs
-  #> raw_computation;
+  #> Exn.capture raw_computation
+  #> partiality_as_none;
 
 fun mount_computation ctxt cTs T raw_computation lift_postproc =
   Code_Preproc.static_value { ctxt = ctxt, lift_postproc = lift_postproc, consts = [] }