abort execution of generated code with explicit exception message
authorAndreas Lochbihler
Thu Aug 08 16:10:05 2013 +0200 (2013-08-08)
changeset 529107bfe0df532a9
parent 52909 66cc4ed9a1f2
child 52914 7a1537b54f16
child 52916 5f3faf72b62a
abort execution of generated code with explicit exception message
src/HOL/String.thy
     1.1 --- a/src/HOL/String.thy	Thu Aug 08 14:55:01 2013 +0200
     1.2 +++ b/src/HOL/String.thy	Thu Aug 08 16:10:05 2013 +0200
     1.3 @@ -420,6 +420,19 @@
     1.4      and (Haskell) infix 4 "=="
     1.5      and (Scala) infixl 5 "=="
     1.6  
     1.7 +setup {* Sign.map_naming (Name_Space.mandatory_path "Code") *}
     1.8 +
     1.9 +definition abort :: "literal \<Rightarrow> (unit \<Rightarrow> 'a) \<Rightarrow> 'a"
    1.10 +where [simp, code del]: "abort _ f = f ()"
    1.11 +
    1.12 +setup {* Sign.map_naming Name_Space.parent_path *}
    1.13 +
    1.14 +code_printing constant Code.abort \<rightharpoonup>
    1.15 +    (SML) "!(raise/ Fail/ _)"
    1.16 +    and (OCaml) "failwith"
    1.17 +    and (Haskell) "error"
    1.18 +    and (Scala) "!{/ sys.error((_));/  ((_)).apply(())/ }"
    1.19 +
    1.20  hide_type (open) literal
    1.21  
    1.22  end