formal introduction of case cong
authorhaftmann
Tue Jun 15 08:32:32 2010 +0200 (2010-06-15)
changeset 374374202e11ae7dc
parent 37433 a2a89563bfcb
child 37438 4906ab970316
formal introduction of case cong
src/Tools/Code/code_eval.ML
src/Tools/Code/code_haskell.ML
src/Tools/Code/code_ml.ML
src/Tools/Code/code_scala.ML
src/Tools/Code/code_thingol.ML
src/Tools/nbe.ML
     1.1 --- a/src/Tools/Code/code_eval.ML	Tue Jun 15 07:42:48 2010 +0200
     1.2 +++ b/src/Tools/Code/code_eval.ML	Tue Jun 15 08:32:32 2010 +0200
     1.3 @@ -55,7 +55,7 @@
     1.4          val value_name = "Value.VALUE.value"
     1.5          val program' = program
     1.6            |> Graph.new_node (value_name,
     1.7 -              Code_Thingol.Fun (Term.dummy_patternN, (([], ty), [(([], t), (NONE, true))])))
     1.8 +              Code_Thingol.Fun (Term.dummy_patternN, ((([], ty), [(([], t), (NONE, true))]), NONE)))
     1.9            |> fold (curry Graph.add_edge value_name) deps;
    1.10          val (value_code, [SOME value_name']) = Code_ML.evaluation_code_of thy
    1.11            (the_default target some_target) "" naming program' [value_name];
     2.1 --- a/src/Tools/Code/code_haskell.ML	Tue Jun 15 07:42:48 2010 +0200
     2.2 +++ b/src/Tools/Code/code_haskell.ML	Tue Jun 15 08:32:32 2010 +0200
     2.3 @@ -115,7 +115,7 @@
     2.4            end
     2.5        | print_case tyvars some_thm vars fxy ((_, []), _) =
     2.6            (brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""];
     2.7 -    fun print_stmt (name, Code_Thingol.Fun (_, ((vs, ty), raw_eqs))) =
     2.8 +    fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) =
     2.9            let
    2.10              val tyvars = intro_vars (map fst vs) reserved;
    2.11              fun print_err n =
     3.1 --- a/src/Tools/Code/code_ml.ML	Tue Jun 15 07:42:48 2010 +0200
     3.2 +++ b/src/Tools/Code/code_ml.ML	Tue Jun 15 08:32:32 2010 +0200
     3.3 @@ -758,7 +758,7 @@
     3.4          val base' = if upper then first_upper base else base;
     3.5          val ([base''], nsp') = Name.variants [base'] nsp;
     3.6        in (base'', nsp') end;
     3.7 -    fun ml_binding_of_stmt (name, Code_Thingol.Fun (_, (tysm as (vs, ty), raw_eqs))) =
     3.8 +    fun ml_binding_of_stmt (name, Code_Thingol.Fun (_, ((tysm as (vs, ty), raw_eqs), _))) =
     3.9            let
    3.10              val eqs = filter (snd o snd) raw_eqs;
    3.11              val (eqs', is_value) = if null (filter_out (null o snd) vs) then case eqs
     4.1 --- a/src/Tools/Code/code_scala.ML	Tue Jun 15 07:42:48 2010 +0200
     4.2 +++ b/src/Tools/Code/code_scala.ML	Tue Jun 15 08:32:32 2010 +0200
     4.3 @@ -129,7 +129,7 @@
     4.4              (map2 (fn param => fn ty => print_typed tyvars
     4.5                  ((str o lookup_var vars) param) ty)
     4.6                params tys)) implicits) ty, str " ="]
     4.7 -    fun print_stmt (name, Code_Thingol.Fun (_, ((vs, ty), raw_eqs))) = (case filter (snd o snd) raw_eqs
     4.8 +    fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) = (case filter (snd o snd) raw_eqs
     4.9           of [] =>
    4.10                let
    4.11                  val (tys, ty') = Code_Thingol.unfold_fun ty;
    4.12 @@ -351,8 +351,8 @@
    4.13        module_name reserved raw_module_alias program;
    4.14      val reserved = make_vars reserved;
    4.15      fun args_num c = case Graph.get_node program c
    4.16 -     of Code_Thingol.Fun (_, ((_, ty), [])) => (length o fst o Code_Thingol.unfold_fun) ty
    4.17 -      | Code_Thingol.Fun (_, (_, ((ts, _), _) :: _)) => length ts
    4.18 +     of Code_Thingol.Fun (_, (((_, ty), []), _)) => (length o fst o Code_Thingol.unfold_fun) ty
    4.19 +      | Code_Thingol.Fun (_, ((_, ((ts, _), _) :: _), _)) => length ts
    4.20        | Code_Thingol.Datatypecons (_, tyco) =>
    4.21            let val Code_Thingol.Datatype (_, (_, constrs)) = Graph.get_node program tyco
    4.22            in (length o the o AList.lookup (op =) constrs) c end
     5.1 --- a/src/Tools/Code/code_thingol.ML	Tue Jun 15 07:42:48 2010 +0200
     5.2 +++ b/src/Tools/Code/code_thingol.ML	Tue Jun 15 08:32:32 2010 +0200
     5.3 @@ -66,7 +66,7 @@
     5.4  
     5.5    datatype stmt =
     5.6        NoStmt
     5.7 -    | Fun of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list)
     5.8 +    | Fun of string * ((typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option)
     5.9      | Datatype of string * ((vname * sort) list * (string * itype list) list)
    5.10      | Datatypecons of string * string
    5.11      | Class of class * (vname * ((class * string) list * (string * itype) list))
    5.12 @@ -402,7 +402,7 @@
    5.13  type typscheme = (vname * sort) list * itype;
    5.14  datatype stmt =
    5.15      NoStmt
    5.16 -  | Fun of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list)
    5.17 +  | Fun of string * ((typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option)
    5.18    | Datatype of string * ((vname * sort) list * (string * itype list) list)
    5.19    | Datatypecons of string * string
    5.20    | Class of class * (vname * ((class * string) list * (string * itype) list))
    5.21 @@ -416,7 +416,7 @@
    5.22  type program = stmt Graph.T;
    5.23  
    5.24  fun empty_funs program =
    5.25 -  Graph.fold (fn (name, (Fun (c, (_, [])), _)) => cons c
    5.26 +  Graph.fold (fn (name, (Fun (c, ((_, []), _)), _)) => cons c
    5.27                 | _ => I) program [];
    5.28  
    5.29  fun map_terms_bottom_up f (t as IConst _) = f t
    5.30 @@ -430,8 +430,8 @@
    5.31          (map_terms_bottom_up f) ps), map_terms_bottom_up f t0));
    5.32  
    5.33  fun map_terms_stmt f NoStmt = NoStmt
    5.34 -  | map_terms_stmt f (Fun (c, (tysm, eqs))) = Fun (c, (tysm, (map o apfst)
    5.35 -      (fn (ts, t) => (map f ts, f t)) eqs))
    5.36 +  | map_terms_stmt f (Fun (c, ((tysm, eqs), case_cong))) = Fun (c, ((tysm, (map o apfst)
    5.37 +      (fn (ts, t) => (map f ts, f t)) eqs), case_cong))
    5.38    | map_terms_stmt f (stmt as Datatype _) = stmt
    5.39    | map_terms_stmt f (stmt as Datatypecons _) = stmt
    5.40    | map_terms_stmt f (stmt as Class _) = stmt
    5.41 @@ -573,7 +573,7 @@
    5.42          ##>> translate_typ thy algbr eqngr permissive ty
    5.43          ##>> (fold_map (translate_equation thy algbr eqngr permissive) eqns
    5.44            #>> map_filter I)
    5.45 -        #>> (fn info => Fun (c, info))
    5.46 +        #>> (fn info => Fun (c, (info, NONE)))
    5.47        end;
    5.48      val stmt_const = case Code.get_type_of_constr_or_abstr thy c
    5.49       of SOME (tyco, _) => stmt_datatypecons tyco
    5.50 @@ -847,10 +847,10 @@
    5.51        ##>> translate_typ thy algbr eqngr false ty
    5.52        ##>> translate_term thy algbr eqngr false NONE (Code.subst_signatures thy t, NONE)
    5.53        #>> (fn ((vs, ty), t) => Fun
    5.54 -        (Term.dummy_patternN, ((vs, ty), [(([], t), (NONE, true))])));
    5.55 +        (Term.dummy_patternN, (((vs, ty), [(([], t), (NONE, true))]), NONE)));
    5.56      fun term_value (dep, (naming, program1)) =
    5.57        let
    5.58 -        val Fun (_, (vs_ty, [(([], t), _)])) =
    5.59 +        val Fun (_, ((vs_ty, [(([], t), _)]), _)) =
    5.60            Graph.get_node program1 Term.dummy_patternN;
    5.61          val deps = Graph.imm_succs program1 Term.dummy_patternN;
    5.62          val program2 = Graph.del_nodes [Term.dummy_patternN] program1;
     6.1 --- a/src/Tools/nbe.ML	Tue Jun 15 07:42:48 2010 +0200
     6.2 +++ b/src/Tools/nbe.ML	Tue Jun 15 08:32:32 2010 +0200
     6.3 @@ -396,9 +396,9 @@
     6.4  
     6.5  (* preparing function equations *)
     6.6  
     6.7 -fun eqns_of_stmt (_, Code_Thingol.Fun (_, (_, []))) =
     6.8 +fun eqns_of_stmt (_, Code_Thingol.Fun (_, ((_, []), _))) =
     6.9        []
    6.10 -  | eqns_of_stmt (const, Code_Thingol.Fun (_, ((vs, _), eqns))) =
    6.11 +  | eqns_of_stmt (const, Code_Thingol.Fun (_, (((vs, _), eqns), _))) =
    6.12        [(const, (vs, map fst eqns))]
    6.13    | eqns_of_stmt (_, Code_Thingol.Datatypecons _) =
    6.14        []