computations and partiality
authorhaftmann
Mon Feb 06 20:56:32 2017 +0100 (2017-02-06)
changeset 6498893aaff2b0ae0
parent 64987 1985502518ce
child 64989 40c36a4aee1f
computations and partiality
src/HOL/ex/Computations.thy
src/Tools/Code/code_runtime.ML
     1.1 --- a/src/HOL/ex/Computations.thy	Mon Feb 06 20:56:30 2017 +0100
     1.2 +++ b/src/HOL/ex/Computations.thy	Mon Feb 06 20:56:32 2017 +0100
     1.3 @@ -30,14 +30,14 @@
     1.4  
     1.5  val comp_nat = @{computation "0 :: nat" Suc
     1.6    "plus :: nat \<Rightarrow>_" "times :: nat \<Rightarrow> _" fib :: nat}
     1.7 -  (fn post => post o HOLogic.mk_nat o int_of_nat);
     1.8 +  (fn post => post o HOLogic.mk_nat o int_of_nat o the);
     1.9  
    1.10  val comp_numeral = @{computation "0 :: nat" "1 :: nat" "2 :: nat" "3 :: nat" :: nat}
    1.11 -  (fn post => post o HOLogic.mk_nat o int_of_nat);
    1.12 +  (fn post => post o HOLogic.mk_nat o int_of_nat o the);
    1.13  
    1.14  val comp_bool = @{computation True False HOL.conj HOL.disj HOL.implies
    1.15    HOL.iff even "less_eq :: nat \<Rightarrow> _" "less :: nat \<Rightarrow> _" "HOL.eq :: nat \<Rightarrow> _" :: bool }
    1.16 -  (K I);
    1.17 +  (K the);
    1.18  
    1.19  end
    1.20  \<close>
     2.1 --- a/src/Tools/Code/code_runtime.ML	Mon Feb 06 20:56:30 2017 +0100
     2.2 +++ b/src/Tools/Code/code_runtime.ML	Mon Feb 06 20:56:32 2017 +0100
     2.3 @@ -33,7 +33,7 @@
     2.4    datatype truth = Holds
     2.5    val put_truth: (unit -> truth) -> Proof.context -> Proof.context
     2.6    val mount_computation: Proof.context -> (string * typ) list -> typ
     2.7 -    -> (term -> 'ml) -> ((term -> term) -> 'ml -> 'a) -> Proof.context -> term -> 'a
     2.8 +    -> (term -> 'ml) -> ((term -> term) -> 'ml option -> 'a) -> Proof.context -> term -> 'a
     2.9    val polyml_as_definition: (binding * typ) list -> Path.T list -> theory -> theory
    2.10    val trace: bool Config.T
    2.11  end;
    2.12 @@ -354,7 +354,8 @@
    2.13    check_typ ctxt T
    2.14    #> reject_vars ctxt
    2.15    #> check_computation_input ctxt cTs
    2.16 -  #> raw_computation;
    2.17 +  #> Exn.capture raw_computation
    2.18 +  #> partiality_as_none;
    2.19  
    2.20  fun mount_computation ctxt cTs T raw_computation lift_postproc =
    2.21    Code_Preproc.static_value { ctxt = ctxt, lift_postproc = lift_postproc, consts = [] }