switched exception from arbitrary to undefined
authorhaftmann
Tue Mar 20 15:52:37 2007 +0100 (2007-03-20)
changeset 22480b20bc8029edb
parent 22479 de15ea8fb348
child 22481 79c2724c36b5
switched exception from arbitrary to undefined
src/HOL/Code_Generator.thy
src/HOL/Tools/datatype_codegen.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/primrec_package.ML
     1.1 --- a/src/HOL/Code_Generator.thy	Tue Mar 20 10:23:31 2007 +0100
     1.2 +++ b/src/HOL/Code_Generator.thy	Tue Mar 20 15:52:37 2007 +0100
     1.3 @@ -172,15 +172,12 @@
     1.4    by rule+
     1.5  
     1.6  
     1.7 -text {* code generation for arbitrary as exception *}
     1.8 +text {* code generation for undefined as exception *}
     1.9  
    1.10 -setup {*
    1.11 -  CodegenSerializer.add_undefined "SML" "arbitrary" "(raise Fail \"arbitrary\")"
    1.12 -  #> CodegenSerializer.add_undefined "OCaml" "arbitrary" "(failwith \"arbitrary\")"
    1.13 -*}
    1.14 -
    1.15 -code_const arbitrary
    1.16 -  (Haskell "error/ \"arbitrary\"")
    1.17 +code_const undefined
    1.18 +  (SML "(raise Fail \"undefined\")")
    1.19 +  (OCaml "(failwith \"undefined\")")
    1.20 +  (Haskell "error/ \"undefined\"")
    1.21  
    1.22  code_reserved SML Fail
    1.23  code_reserved OCaml failwith
     2.1 --- a/src/HOL/Tools/datatype_codegen.ML	Tue Mar 20 10:23:31 2007 +0100
     2.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Tue Mar 20 15:52:37 2007 +0100
     2.3 @@ -340,7 +340,7 @@
     2.4          val (vs, t') = Term.strip_abs_eta (length tys_decl) t;
     2.5          val c' = list_comb (Const (c, map snd vs ---> sty), map Free vs);
     2.6        in case t'
     2.7 -       of Const ("undefined", _) => NONE
     2.8 +       of Const ("HOL.undefined", _) => NONE
     2.9          | _ => SOME (c', t')
    2.10        end;
    2.11    in (abs, ((t, sty), map2 dest_case (cs ~~ tys') ts' |> map_filter I)) end;
    2.12 @@ -423,7 +423,7 @@
    2.13    let
    2.14      val {case_rewrites, ...} = DatatypePackage.the_datatype thy dtco
    2.15    in
    2.16 -    fold_rev CodegenData.add_func case_rewrites thy
    2.17 +    fold_rev (CodegenData.add_func true) case_rewrites thy
    2.18    end;
    2.19  
    2.20  
     3.1 --- a/src/HOL/Tools/datatype_package.ML	Tue Mar 20 10:23:31 2007 +0100
     3.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue Mar 20 15:52:37 2007 +0100
     3.3 @@ -433,7 +433,7 @@
     3.4                   (DatatypeProp.make_tnames (map (typ_of_dtyp descr sorts) dt)),
     3.5                   case default of
     3.6                     NONE => (warning ("No clause for constructor " ^ s ^
     3.7 -                     " in case expression"); Const ("undefined", dummyT))
     3.8 +                     " in case expression"); Const ("HOL.undefined", dummyT))
     3.9                   | SOME t => t), cases)
    3.10               | SOME (c as ((_, vs), t)) =>
    3.11                   if length dt <> length vs then
    3.12 @@ -486,7 +486,7 @@
    3.13        (fold_rev count_cases cases []);
    3.14      fun mk_case1 (cname, (vs, body), _) = Syntax.const "_case1" $
    3.15        list_comb (Syntax.const cname, vs) $ body;
    3.16 -    fun is_undefined (Const ("undefined", _)) = true
    3.17 +    fun is_undefined (Const ("HOL.undefined", _)) = true
    3.18        | is_undefined _ = false;
    3.19    in
    3.20      Syntax.const "_case_syntax" $ x $
     4.1 --- a/src/HOL/Tools/primrec_package.ML	Tue Mar 20 10:23:31 2007 +0100
     4.2 +++ b/src/HOL/Tools/primrec_package.ML	Tue Mar 20 15:52:37 2007 +0100
     4.3 @@ -142,7 +142,7 @@
     4.4        (case AList.lookup (op =) eqns cname of
     4.5            NONE => (warning ("No equation for constructor " ^ quote cname ^
     4.6              "\nin definition of function " ^ quote fname);
     4.7 -              (fnameTs', fnss', (Const ("arbitrary", dummyT))::fns))
     4.8 +              (fnameTs', fnss', (Const ("HOL.undefined", dummyT))::fns))
     4.9          | SOME (ls, cargs', rs, rhs, eq) =>
    4.10              let
    4.11                val recs = filter (is_rec_type o snd) (cargs' ~~ cargs);
    4.12 @@ -182,7 +182,7 @@
    4.13    case AList.lookup (op =) fns i of
    4.14       NONE =>
    4.15         let
    4.16 -         val dummy_fns = map (fn (_, cargs) => Const ("arbitrary",
    4.17 +         val dummy_fns = map (fn (_, cargs) => Const ("HOL.undefined",
    4.18             replicate ((length cargs) + (length (List.filter is_rec_type cargs)))
    4.19               dummyT ---> HOLogic.unitT)) constrs;
    4.20           val _ = warning ("No function definition for datatype " ^ quote tname)