# HG changeset patch # User haftmann # Date 1276583552 -7200 # Node ID 4202e11ae7dc1d3c315f59b4ef20ce7bbf4a0617 # Parent a2a89563bfcb52c2d9ed642c652d5c20386e484b formal introduction of case cong diff -r a2a89563bfcb -r 4202e11ae7dc src/Tools/Code/code_eval.ML --- a/src/Tools/Code/code_eval.ML Tue Jun 15 07:42:48 2010 +0200 +++ b/src/Tools/Code/code_eval.ML Tue Jun 15 08:32:32 2010 +0200 @@ -55,7 +55,7 @@ val value_name = "Value.VALUE.value" val program' = program |> Graph.new_node (value_name, - Code_Thingol.Fun (Term.dummy_patternN, (([], ty), [(([], t), (NONE, true))]))) + Code_Thingol.Fun (Term.dummy_patternN, ((([], ty), [(([], t), (NONE, true))]), NONE))) |> fold (curry Graph.add_edge value_name) deps; val (value_code, [SOME value_name']) = Code_ML.evaluation_code_of thy (the_default target some_target) "" naming program' [value_name]; diff -r a2a89563bfcb -r 4202e11ae7dc src/Tools/Code/code_haskell.ML --- a/src/Tools/Code/code_haskell.ML Tue Jun 15 07:42:48 2010 +0200 +++ b/src/Tools/Code/code_haskell.ML Tue Jun 15 08:32:32 2010 +0200 @@ -115,7 +115,7 @@ end | print_case tyvars some_thm vars fxy ((_, []), _) = (brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""]; - fun print_stmt (name, Code_Thingol.Fun (_, ((vs, ty), raw_eqs))) = + fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) = let val tyvars = intro_vars (map fst vs) reserved; fun print_err n = diff -r a2a89563bfcb -r 4202e11ae7dc src/Tools/Code/code_ml.ML --- a/src/Tools/Code/code_ml.ML Tue Jun 15 07:42:48 2010 +0200 +++ b/src/Tools/Code/code_ml.ML Tue Jun 15 08:32:32 2010 +0200 @@ -758,7 +758,7 @@ val base' = if upper then first_upper base else base; val ([base''], nsp') = Name.variants [base'] nsp; in (base'', nsp') end; - fun ml_binding_of_stmt (name, Code_Thingol.Fun (_, (tysm as (vs, ty), raw_eqs))) = + fun ml_binding_of_stmt (name, Code_Thingol.Fun (_, ((tysm as (vs, ty), raw_eqs), _))) = let val eqs = filter (snd o snd) raw_eqs; val (eqs', is_value) = if null (filter_out (null o snd) vs) then case eqs diff -r a2a89563bfcb -r 4202e11ae7dc src/Tools/Code/code_scala.ML --- a/src/Tools/Code/code_scala.ML Tue Jun 15 07:42:48 2010 +0200 +++ b/src/Tools/Code/code_scala.ML Tue Jun 15 08:32:32 2010 +0200 @@ -129,7 +129,7 @@ (map2 (fn param => fn ty => print_typed tyvars ((str o lookup_var vars) param) ty) params tys)) implicits) ty, str " ="] - fun print_stmt (name, Code_Thingol.Fun (_, ((vs, ty), raw_eqs))) = (case filter (snd o snd) raw_eqs + fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) = (case filter (snd o snd) raw_eqs of [] => let val (tys, ty') = Code_Thingol.unfold_fun ty; @@ -351,8 +351,8 @@ module_name reserved raw_module_alias program; val reserved = make_vars reserved; fun args_num c = case Graph.get_node program c - of Code_Thingol.Fun (_, ((_, ty), [])) => (length o fst o Code_Thingol.unfold_fun) ty - | Code_Thingol.Fun (_, (_, ((ts, _), _) :: _)) => length ts + of Code_Thingol.Fun (_, (((_, ty), []), _)) => (length o fst o Code_Thingol.unfold_fun) ty + | Code_Thingol.Fun (_, ((_, ((ts, _), _) :: _), _)) => length ts | Code_Thingol.Datatypecons (_, tyco) => let val Code_Thingol.Datatype (_, (_, constrs)) = Graph.get_node program tyco in (length o the o AList.lookup (op =) constrs) c end diff -r a2a89563bfcb -r 4202e11ae7dc src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Tue Jun 15 07:42:48 2010 +0200 +++ b/src/Tools/Code/code_thingol.ML Tue Jun 15 08:32:32 2010 +0200 @@ -66,7 +66,7 @@ datatype stmt = NoStmt - | Fun of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list) + | Fun of string * ((typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option) | Datatype of string * ((vname * sort) list * (string * itype list) list) | Datatypecons of string * string | Class of class * (vname * ((class * string) list * (string * itype) list)) @@ -402,7 +402,7 @@ type typscheme = (vname * sort) list * itype; datatype stmt = NoStmt - | Fun of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list) + | Fun of string * ((typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option) | Datatype of string * ((vname * sort) list * (string * itype list) list) | Datatypecons of string * string | Class of class * (vname * ((class * string) list * (string * itype) list)) @@ -416,7 +416,7 @@ type program = stmt Graph.T; fun empty_funs program = - Graph.fold (fn (name, (Fun (c, (_, [])), _)) => cons c + Graph.fold (fn (name, (Fun (c, ((_, []), _)), _)) => cons c | _ => I) program []; fun map_terms_bottom_up f (t as IConst _) = f t @@ -430,8 +430,8 @@ (map_terms_bottom_up f) ps), map_terms_bottom_up f t0)); fun map_terms_stmt f NoStmt = NoStmt - | map_terms_stmt f (Fun (c, (tysm, eqs))) = Fun (c, (tysm, (map o apfst) - (fn (ts, t) => (map f ts, f t)) eqs)) + | map_terms_stmt f (Fun (c, ((tysm, eqs), case_cong))) = Fun (c, ((tysm, (map o apfst) + (fn (ts, t) => (map f ts, f t)) eqs), case_cong)) | map_terms_stmt f (stmt as Datatype _) = stmt | map_terms_stmt f (stmt as Datatypecons _) = stmt | map_terms_stmt f (stmt as Class _) = stmt @@ -573,7 +573,7 @@ ##>> translate_typ thy algbr eqngr permissive ty ##>> (fold_map (translate_equation thy algbr eqngr permissive) eqns #>> map_filter I) - #>> (fn info => Fun (c, info)) + #>> (fn info => Fun (c, (info, NONE))) end; val stmt_const = case Code.get_type_of_constr_or_abstr thy c of SOME (tyco, _) => stmt_datatypecons tyco @@ -847,10 +847,10 @@ ##>> translate_typ thy algbr eqngr false ty ##>> translate_term thy algbr eqngr false NONE (Code.subst_signatures thy t, NONE) #>> (fn ((vs, ty), t) => Fun - (Term.dummy_patternN, ((vs, ty), [(([], t), (NONE, true))]))); + (Term.dummy_patternN, (((vs, ty), [(([], t), (NONE, true))]), NONE))); fun term_value (dep, (naming, program1)) = let - val Fun (_, (vs_ty, [(([], t), _)])) = + val Fun (_, ((vs_ty, [(([], t), _)]), _)) = Graph.get_node program1 Term.dummy_patternN; val deps = Graph.imm_succs program1 Term.dummy_patternN; val program2 = Graph.del_nodes [Term.dummy_patternN] program1; diff -r a2a89563bfcb -r 4202e11ae7dc src/Tools/nbe.ML --- a/src/Tools/nbe.ML Tue Jun 15 07:42:48 2010 +0200 +++ b/src/Tools/nbe.ML Tue Jun 15 08:32:32 2010 +0200 @@ -396,9 +396,9 @@ (* preparing function equations *) -fun eqns_of_stmt (_, Code_Thingol.Fun (_, (_, []))) = +fun eqns_of_stmt (_, Code_Thingol.Fun (_, ((_, []), _))) = [] - | eqns_of_stmt (const, Code_Thingol.Fun (_, ((vs, _), eqns))) = + | eqns_of_stmt (const, Code_Thingol.Fun (_, (((vs, _), eqns), _))) = [(const, (vs, map fst eqns))] | eqns_of_stmt (_, Code_Thingol.Datatypecons _) = []