tuned data structure
authorhaftmann
Thu Sep 18 18:48:04 2014 +0200 (2014-09-18)
changeset 583971c036d6216d3
parent 58396 7b60e4e74430
child 58398 f38717f175d9
tuned data structure
src/HOL/Imperative_HOL/Heap_Monad.thy
src/Tools/Code/code_haskell.ML
src/Tools/Code/code_thingol.ML
src/Tools/nbe.ML
     1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Sep 19 14:24:03 2014 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Sep 18 18:48:04 2014 +0200
     1.3 @@ -658,7 +658,7 @@
     1.4      val unitT = @{type_name unit} `%% [];
     1.5      val unitt =
     1.6        IConst { sym = Code_Symbol.Constant @{const_name Unity}, typargs = [], dicts = [], dom = [],
     1.7 -        range = unitT, annotate = false };
     1.8 +        annotation = NONE };
     1.9      fun dest_abs ((v, ty) `|=> t, _) = ((v, ty), t)
    1.10        | dest_abs (t, ty) =
    1.11            let
     2.1 --- a/src/Tools/Code/code_haskell.ML	Fri Sep 19 14:24:03 2014 +0200
     2.2 +++ b/src/Tools/Code/code_haskell.ML	Thu Sep 18 18:48:04 2014 +0200
     2.3 @@ -90,14 +90,12 @@
     2.4                  then print_case tyvars some_thm vars fxy case_expr
     2.5                  else print_app tyvars some_thm vars fxy app
     2.6              | NONE => print_case tyvars some_thm vars fxy case_expr)
     2.7 -    and print_app_expr tyvars some_thm vars ({ sym, dom, range, annotate, ... }, ts) =
     2.8 +    and print_app_expr tyvars some_thm vars ({ sym, annotation, ... }, ts) =
     2.9        let
    2.10 -        val ty = Library.foldr (op `->) (dom, range)
    2.11          val printed_const =
    2.12 -          if annotate then
    2.13 -            brackets [(str o deresolve) sym, str "::", print_typ tyvars NOBR ty]
    2.14 -          else
    2.15 -            (str o deresolve) sym
    2.16 +          case annotation of
    2.17 +            SOME ty => brackets [(str o deresolve) sym, str "::", print_typ tyvars NOBR ty]
    2.18 +          | NONE => (str o deresolve) sym
    2.19        in 
    2.20          printed_const :: map (print_term tyvars some_thm vars BR) ts
    2.21        end
    2.22 @@ -241,7 +239,7 @@
    2.23                    ]
    2.24                | SOME (k, Code_Printer.Complex_printer _) =>
    2.25                    let
    2.26 -                    val { sym = Constant c, dom, range, ... } = const;
    2.27 +                    val { sym = Constant c, dom, ... } = const;
    2.28                      val (vs, rhs) = (apfst o map) fst
    2.29                        (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
    2.30                      val s = if (is_some o const_syntax) c
    2.31 @@ -249,7 +247,7 @@
    2.32                      val vars = reserved
    2.33                        |> intro_vars (map_filter I (s :: vs));
    2.34                      val lhs = IConst { sym = Constant classparam, typargs = [],
    2.35 -                      dicts = [], dom = dom, range = range, annotate = false } `$$ map IVar vs;
    2.36 +                      dicts = [], dom = dom, annotation = NONE } `$$ map IVar vs;
    2.37                        (*dictionaries are not relevant at this late stage,
    2.38                          and these consts never need type annotations for disambiguation *)
    2.39                    in
     3.1 --- a/src/Tools/Code/code_thingol.ML	Fri Sep 19 14:24:03 2014 +0200
     3.2 +++ b/src/Tools/Code/code_thingol.ML	Thu Sep 18 18:48:04 2014 +0200
     3.3 @@ -24,7 +24,7 @@
     3.4        `%% of string * itype list
     3.5      | ITyVar of vname;
     3.6    type const = { sym: Code_Symbol.T, typargs: itype list, dicts: dict list list,
     3.7 -    dom: itype list, range: itype, annotate: bool };
     3.8 +    dom: itype list, annotation: itype option };
     3.9    datatype iterm =
    3.10        IConst of const
    3.11      | IVar of vname option
    3.12 @@ -152,7 +152,7 @@
    3.13    in (tys3, ty3) end;
    3.14  
    3.15  type const = { sym: Code_Symbol.T, typargs: itype list, dicts: dict list list,
    3.16 -  dom: itype list, range: itype, annotate: bool };
    3.17 +  dom: itype list, annotation: itype option };
    3.18  
    3.19  datatype iterm =
    3.20      IConst of const
    3.21 @@ -646,10 +646,11 @@
    3.22      ensure_const ctxt algbr eqngr permissive c
    3.23      ##>> fold_map (translate_typ ctxt algbr eqngr permissive) typargs
    3.24      ##>> fold_map (translate_dicts ctxt algbr eqngr permissive some_thm) (typargs ~~ sorts)
    3.25 -    ##>> fold_map (translate_typ ctxt algbr eqngr permissive) (range :: dom)
    3.26 -    #>> (fn (((c, typargs), dss), range :: dom) =>
    3.27 +    ##>> fold_map (translate_typ ctxt algbr eqngr permissive) (ty' :: dom)
    3.28 +    #>> (fn (((c, typargs), dss), annotation :: dom) =>
    3.29        IConst { sym = Constant c, typargs = typargs, dicts = dss,
    3.30 -        dom = dom, range = range, annotate = annotate })
    3.31 +        dom = dom, annotation =
    3.32 +          if annotate then SOME annotation else NONE })
    3.33    end
    3.34  and translate_app_const ctxt algbr eqngr permissive some_thm ((c_ty, ts), some_abs) =
    3.35    translate_const ctxt algbr eqngr permissive some_thm (c_ty, some_abs)
     4.1 --- a/src/Tools/nbe.ML	Fri Sep 19 14:24:03 2014 +0200
     4.2 +++ b/src/Tools/nbe.ML	Thu Sep 18 18:48:04 2014 +0200
     4.3 @@ -416,7 +416,7 @@
     4.4  
     4.5  fun dummy_const sym dss =
     4.6    IConst { sym = sym, typargs = [], dicts = dss,
     4.7 -    dom = [], range = ITyVar "", annotate = false };
     4.8 +    dom = [], annotation = NONE };
     4.9  
    4.10  fun eqns_of_stmt (_, Code_Thingol.NoStmt) =
    4.11        []