# HG changeset patch # User haftmann # Date 1276594720 -7200 # Node ID a5d44161ba2abe1ae6f32a12cc1d1c9653bd752f # Parent c72a43a7d2c53316e79701390d064bfb75b7399d maintain cong rules for case combinators; more precise permissiveness diff -r c72a43a7d2c5 -r a5d44161ba2a src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Tue Jun 15 11:38:40 2010 +0200 +++ b/src/Tools/Code/code_thingol.ML Tue Jun 15 11:38:40 2010 +0200 @@ -81,6 +81,7 @@ val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm val map_terms_stmt: (iterm -> iterm) -> stmt -> stmt val is_cons: program -> string -> bool + val is_case: stmt -> bool val contr_classparam_typs: program -> string -> itype option list val labelled_name: theory -> program -> string -> string val group_stmts: theory -> program @@ -445,6 +446,9 @@ of Datatypecons _ => true | _ => false; +fun is_case (Fun (_, (_, SOME _))) = true + | is_case _ = false; + fun contr_classparam_typs program name = case Graph.get_node program name of Classparam (_, class) => let val Class (_, (_, (_, params))) = Graph.get_node program class; @@ -473,6 +477,10 @@ val Datatype (tyco, _) = Graph.get_node program tyco in quote (Sign.extern_type thy tyco ^ " :: " ^ Sign.extern_class thy class) end +fun linear_stmts program = + rev (Graph.strong_conn program) + |> map (AList.make (Graph.get_node program)); + fun group_stmts thy program = let fun is_fun (_, Fun _) = true | is_fun _ = false; @@ -492,8 +500,7 @@ else error ("Illegal mutual dependencies: " ^ (commas o map (labelled_name thy program o fst)) stmts) in - rev (Graph.strong_conn program) - |> map (AList.make (Graph.get_node program)) + linear_stmts program |> map group end; @@ -568,12 +575,12 @@ fun stmt_fun cert = let val ((vs, ty), eqns) = Code.equations_of_cert thy cert; + val some_case_cong = Code.get_case_cong thy c; in fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs ##>> translate_typ thy algbr eqngr permissive ty - ##>> (fold_map (translate_equation thy algbr eqngr permissive) eqns - #>> map_filter I) - #>> (fn info => Fun (c, (info, NONE))) + ##>> translate_eqns thy algbr eqngr permissive eqns + #>> (fn info => Fun (c, (info, some_case_cong))) end; val stmt_const = case Code.get_type_of_constr_or_abstr thy c of SOME (tyco, _) => stmt_datatypecons tyco @@ -667,9 +674,9 @@ fold_map (translate_term thy algbr eqngr permissive some_thm) args ##>> translate_term thy algbr eqngr permissive some_thm (rhs, some_abs) #>> rpair (some_thm, proper) -and translate_equation thy algbr eqngr permissive eqn prgrm = - prgrm |> translate_eqn thy algbr eqngr permissive eqn |>> SOME - handle PERMISSIVE () => (NONE, prgrm) +and translate_eqns thy algbr eqngr permissive eqns prgrm = + prgrm |> fold_map (translate_eqn thy algbr eqngr permissive) eqns + handle PERMISSIVE () => ([], prgrm) and translate_const thy algbr eqngr permissive some_thm ((c, ty), some_abs) = let val _ = if (case some_abs of NONE => true | SOME abs => not (c = abs))