more precise code
authorhaftmann
Thu Jun 17 15:59:47 2010 +0200 (2010-06-17)
changeset 37449034ebe92f090
parent 37448 3bd4b3809bee
child 37450 45073611170a
more precise code
src/Tools/Code/code_haskell.ML
src/Tools/Code/code_ml.ML
src/Tools/Code/code_printer.ML
src/Tools/Code/code_simp.ML
src/Tools/nbe.ML
     1.1 --- a/src/Tools/Code/code_haskell.ML	Thu Jun 17 15:59:46 2010 +0200
     1.2 +++ b/src/Tools/Code/code_haskell.ML	Thu Jun 17 15:59:47 2010 +0200
     1.3 @@ -75,7 +75,7 @@
     1.4                  then print_case tyvars some_thm vars fxy cases
     1.5                  else print_app tyvars some_thm vars fxy c_ts
     1.6              | NONE => print_case tyvars some_thm vars fxy cases)
     1.7 -    and print_app_expr tyvars some_thm vars ((c, (_, tys)), ts) = case contr_classparam_typs c
     1.8 +    and print_app_expr tyvars some_thm vars ((c, (_, function_typs)), ts) = case contr_classparam_typs c
     1.9       of [] => (str o deresolve) c :: map (print_term tyvars some_thm vars BR) ts
    1.10        | fingerprint => let
    1.11            val ts_fingerprint = ts ~~ take (length ts) fingerprint;
    1.12 @@ -86,7 +86,7 @@
    1.13                  brackets [print_term tyvars some_thm vars NOBR t, str "::", print_typ tyvars NOBR ty];
    1.14          in
    1.15            if needs_annotation then
    1.16 -            (str o deresolve) c :: map2 print_term_anno ts_fingerprint (take (length ts) tys)
    1.17 +            (str o deresolve) c :: map2 print_term_anno ts_fingerprint (take (length ts) function_typs)
    1.18            else (str o deresolve) c :: map (print_term tyvars some_thm vars BR) ts
    1.19          end
    1.20      and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) syntax_const
    1.21 @@ -163,7 +163,7 @@
    1.22                print_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs))
    1.23              ]
    1.24            end
    1.25 -      | print_stmt (name, Code_Thingol.Datatype (_, (vs, [(co, [ty])]))) =
    1.26 +      | print_stmt (name, Code_Thingol.Datatype (_, (vs, [((co, _), [ty])]))) =
    1.27            let
    1.28              val tyvars = intro_vars (map fst vs) reserved;
    1.29            in
    1.30 @@ -179,7 +179,7 @@
    1.31        | print_stmt (name, Code_Thingol.Datatype (_, (vs, co :: cos))) =
    1.32            let
    1.33              val tyvars = intro_vars (map fst vs) reserved;
    1.34 -            fun print_co (co, tys) =
    1.35 +            fun print_co ((co, _), tys) =
    1.36                concat (
    1.37                  (str o deresolve_base) co
    1.38                  :: map (print_typ tyvars BR) tys
    1.39 @@ -214,7 +214,7 @@
    1.40                str "};"
    1.41              ) (map print_classparam classparams)
    1.42            end
    1.43 -      | print_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, classparam_instances))) =
    1.44 +      | print_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, (classparam_instances, _)))) =
    1.45            let
    1.46              val tyvars = intro_vars (map fst vs) reserved;
    1.47              fun print_classparam_instance ((classparam, const), (thm, _)) = case syntax_const classparam
     2.1 --- a/src/Tools/Code/code_ml.ML	Thu Jun 17 15:59:46 2010 +0200
     2.2 +++ b/src/Tools/Code/code_ml.ML	Thu Jun 17 15:59:47 2010 +0200
     2.3 @@ -33,13 +33,13 @@
     2.4      ML_Function of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list)
     2.5    | ML_Instance of string * ((class * (string * (vname * sort) list))
     2.6          * ((class * (string * (string * dict list list))) list
     2.7 -      * ((string * const) * (thm * bool)) list));
     2.8 +      * (((string * const) * (thm * bool)) list * ((string * const) * (thm * bool)) list)));
     2.9  
    2.10  datatype ml_stmt =
    2.11      ML_Exc of string * (typscheme * int)
    2.12    | ML_Val of ml_binding
    2.13    | ML_Funs of ml_binding list * string list
    2.14 -  | ML_Datas of (string * ((vname * sort) list * (string * itype list) list)) list
    2.15 +  | ML_Datas of (string * ((vname * sort) list * ((string * vname list) * itype list) list)) list
    2.16    | ML_Class of string * (vname * ((class * string) list * (string * itype) list));
    2.17  
    2.18  fun stmt_name_of_binding (ML_Function (name, _)) = name
    2.19 @@ -121,9 +121,9 @@
    2.20                  then print_case is_pseudo_fun some_thm vars fxy cases
    2.21                  else print_app is_pseudo_fun some_thm vars fxy c_ts
    2.22              | NONE => print_case is_pseudo_fun some_thm vars fxy cases)
    2.23 -    and print_app_expr is_pseudo_fun some_thm vars (app as ((c, ((_, iss), tys)), ts)) =
    2.24 +    and print_app_expr is_pseudo_fun some_thm vars (app as ((c, ((_, iss), function_typs)), ts)) =
    2.25        if is_cons c then
    2.26 -        let val k = length tys in
    2.27 +        let val k = length function_typs in
    2.28            if k < 2 orelse length ts = k
    2.29            then (str o deresolve) c
    2.30              :: the_list (print_tuple (print_term is_pseudo_fun some_thm vars) BR ts)
    2.31 @@ -174,8 +174,8 @@
    2.32        [str "val", str (deresolve name), str ":", print_typscheme typscheme];
    2.33      fun print_datatype_decl definer (tyco, (vs, cos)) =
    2.34        let
    2.35 -        fun print_co (co, []) = str (deresolve co)
    2.36 -          | print_co (co, tys) = concat [str (deresolve co), str "of",
    2.37 +        fun print_co ((co, _), []) = str (deresolve co)
    2.38 +          | print_co ((co, _), tys) = concat [str (deresolve co), str "of",
    2.39                enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];
    2.40        in
    2.41          concat (
    2.42 @@ -219,7 +219,7 @@
    2.43              ))
    2.44            end
    2.45        | print_def is_pseudo_fun _ definer
    2.46 -          (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, classparam_instances)))) =
    2.47 +          (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, (classparam_instances, _))))) =
    2.48            let
    2.49              fun print_super_instance (_, (classrel, dss)) =
    2.50                concat [
    2.51 @@ -466,8 +466,8 @@
    2.52        [str "val", str (deresolve name), str ":", print_typscheme typscheme];
    2.53      fun print_datatype_decl definer (tyco, (vs, cos)) =
    2.54        let
    2.55 -        fun print_co (co, []) = str (deresolve co)
    2.56 -          | print_co (co, tys) = concat [str (deresolve co), str "of",
    2.57 +        fun print_co ((co, _), []) = str (deresolve co)
    2.58 +          | print_co ((co, _), tys) = concat [str (deresolve co), str "of",
    2.59                enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];
    2.60        in
    2.61          concat (
    2.62 @@ -554,7 +554,7 @@
    2.63              ))
    2.64            end
    2.65        | print_def is_pseudo_fun _ definer
    2.66 -            (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, classparam_instances)))) =
    2.67 +            (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, (classparam_instances, _))))) =
    2.68            let
    2.69              fun print_super_instance (_, (classrel, dss)) =
    2.70                concat [
     3.1 --- a/src/Tools/Code/code_printer.ML	Thu Jun 17 15:59:46 2010 +0200
     3.2 +++ b/src/Tools/Code/code_printer.ML	Thu Jun 17 15:59:47 2010 +0200
     3.3 @@ -256,12 +256,12 @@
     3.4    fold_map (Code_Thingol.ensure_declared_const thy) cs naming
     3.5    |-> (fn cs' => pair (n, f literals cs'));
     3.6  
     3.7 -fun gen_print_app print_app_expr print_term syntax_const thm vars fxy (app as ((c, (_, tys)), ts)) =
     3.8 +fun gen_print_app print_app_expr print_term syntax_const thm vars fxy (app as ((c, (_, function_typs)), ts)) =
     3.9    case syntax_const c
    3.10     of NONE => brackify fxy (print_app_expr thm vars app)
    3.11      | SOME (k, print) =>
    3.12          let
    3.13 -          fun print' fxy ts = print (print_term thm) thm vars fxy (ts ~~ take k tys);
    3.14 +          fun print' fxy ts = print (print_term thm) thm vars fxy (ts ~~ take k function_typs);
    3.15          in if k = length ts
    3.16            then print' fxy ts
    3.17          else if k < length ts
     4.1 --- a/src/Tools/Code/code_simp.ML	Thu Jun 17 15:59:46 2010 +0200
     4.2 +++ b/src/Tools/Code/code_simp.ML	Thu Jun 17 15:59:47 2010 +0200
     4.3 @@ -51,8 +51,8 @@
     4.4  
     4.5  fun add_stmt (Code_Thingol.Fun (_, ((_, eqs), some_cong))) ss =
     4.6        ss addsimps (map_filter (fst o snd)) eqs addcongs (the_list some_cong)
     4.7 -  | add_stmt (Code_Thingol.Classinst (_, (_, classparam_insts))) ss =
     4.8 -      ss addsimps (map (fst o snd) classparam_insts)
     4.9 +  | add_stmt (Code_Thingol.Classinst (_, (_, (classparam_instances, _)))) ss =
    4.10 +      ss addsimps (map (fst o snd) classparam_instances)
    4.11    | add_stmt _ ss = ss;
    4.12  
    4.13  val add_program = Graph.fold (add_stmt o fst o snd)
     5.1 --- a/src/Tools/nbe.ML	Thu Jun 17 15:59:46 2010 +0200
     5.2 +++ b/src/Tools/nbe.ML	Thu Jun 17 15:59:47 2010 +0200
     5.3 @@ -417,7 +417,7 @@
     5.4        []
     5.5    | eqns_of_stmt (_, Code_Thingol.Classparam _) =
     5.6        []
     5.7 -  | eqns_of_stmt (inst, Code_Thingol.Classinst ((class, (_, arity_args)), (super_instances, classparam_instances))) =
     5.8 +  | eqns_of_stmt (inst, Code_Thingol.Classinst ((class, (_, arity_args)), (super_instances, (classparam_instances, _)))) =
     5.9        [(inst, (arity_args, [([], IConst (class, (([], []), [])) `$$
    5.10          map (fn (_, (_, (inst, dss))) => IConst (inst, (([], dss), []))) super_instances
    5.11          @ map (IConst o snd o fst) classparam_instances)]))];