src/Tools/Code/code_thingol.ML
changeset 37440 a5d44161ba2a
parent 37437 4202e11ae7dc
child 37445 e372fa3c7239
     1.1 --- a/src/Tools/Code/code_thingol.ML	Tue Jun 15 11:38:40 2010 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Tue Jun 15 11:38:40 2010 +0200
     1.3 @@ -81,6 +81,7 @@
     1.4    val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm
     1.5    val map_terms_stmt: (iterm -> iterm) -> stmt -> stmt
     1.6    val is_cons: program -> string -> bool
     1.7 +  val is_case: stmt -> bool
     1.8    val contr_classparam_typs: program -> string -> itype option list
     1.9    val labelled_name: theory -> program -> string -> string
    1.10    val group_stmts: theory -> program
    1.11 @@ -445,6 +446,9 @@
    1.12   of Datatypecons _ => true
    1.13    | _ => false;
    1.14  
    1.15 +fun is_case (Fun (_, (_, SOME _))) = true
    1.16 +  | is_case _ = false;
    1.17 +
    1.18  fun contr_classparam_typs program name = case Graph.get_node program name
    1.19   of Classparam (_, class) => let
    1.20          val Class (_, (_, (_, params))) = Graph.get_node program class;
    1.21 @@ -473,6 +477,10 @@
    1.22          val Datatype (tyco, _) = Graph.get_node program tyco
    1.23        in quote (Sign.extern_type thy tyco ^ " :: " ^ Sign.extern_class thy class) end
    1.24  
    1.25 +fun linear_stmts program =
    1.26 +  rev (Graph.strong_conn program)
    1.27 +  |> map (AList.make (Graph.get_node program));
    1.28 +
    1.29  fun group_stmts thy program =
    1.30    let
    1.31      fun is_fun (_, Fun _) = true | is_fun _ = false;
    1.32 @@ -492,8 +500,7 @@
    1.33        else error ("Illegal mutual dependencies: " ^
    1.34          (commas o map (labelled_name thy program o fst)) stmts)
    1.35    in
    1.36 -    rev (Graph.strong_conn program)
    1.37 -    |> map (AList.make (Graph.get_node program))
    1.38 +    linear_stmts program
    1.39      |> map group
    1.40    end;
    1.41  
    1.42 @@ -568,12 +575,12 @@
    1.43      fun stmt_fun cert =
    1.44        let
    1.45          val ((vs, ty), eqns) = Code.equations_of_cert thy cert;
    1.46 +        val some_case_cong = Code.get_case_cong thy c;
    1.47        in
    1.48          fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs
    1.49          ##>> translate_typ thy algbr eqngr permissive ty
    1.50 -        ##>> (fold_map (translate_equation thy algbr eqngr permissive) eqns
    1.51 -          #>> map_filter I)
    1.52 -        #>> (fn info => Fun (c, (info, NONE)))
    1.53 +        ##>> translate_eqns thy algbr eqngr permissive eqns
    1.54 +        #>> (fn info => Fun (c, (info, some_case_cong)))
    1.55        end;
    1.56      val stmt_const = case Code.get_type_of_constr_or_abstr thy c
    1.57       of SOME (tyco, _) => stmt_datatypecons tyco
    1.58 @@ -667,9 +674,9 @@
    1.59    fold_map (translate_term thy algbr eqngr permissive some_thm) args
    1.60    ##>> translate_term thy algbr eqngr permissive some_thm (rhs, some_abs)
    1.61    #>> rpair (some_thm, proper)
    1.62 -and translate_equation thy algbr eqngr permissive eqn prgrm =
    1.63 -  prgrm |> translate_eqn thy algbr eqngr permissive eqn |>> SOME
    1.64 -    handle PERMISSIVE () => (NONE, prgrm)
    1.65 +and translate_eqns thy algbr eqngr permissive eqns prgrm =
    1.66 +  prgrm |> fold_map (translate_eqn thy algbr eqngr permissive) eqns
    1.67 +    handle PERMISSIVE () => ([], prgrm)
    1.68  and translate_const thy algbr eqngr permissive some_thm ((c, ty), some_abs) =
    1.69    let
    1.70      val _ = if (case some_abs of NONE => true | SOME abs => not (c = abs))