restored incremental code generation
authorhaftmann
Tue Oct 28 16:59:02 2008 +0100 (2008-10-28)
changeset 287063fef773ae6b1
parent 28705 c77a9f5672f8
child 28707 548703affff5
restored incremental code generation
src/Tools/code/code_thingol.ML
src/Tools/nbe.ML
     1.1 --- a/src/Tools/code/code_thingol.ML	Tue Oct 28 16:59:01 2008 +0100
     1.2 +++ b/src/Tools/code/code_thingol.ML	Tue Oct 28 16:59:02 2008 +0100
     1.3 @@ -57,6 +57,7 @@
     1.4    val fold_unbound_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a
     1.5  
     1.6    type naming
     1.7 +  val empty_naming: naming
     1.8    val lookup_class: naming -> class -> string option
     1.9    val lookup_classrel: naming -> class * class -> string option
    1.10    val lookup_tyco: naming -> string -> string option
    1.11 @@ -259,14 +260,11 @@
    1.12    fun thyname_of_instance thy inst = case AxClass.arity_property thy inst Markup.theory_nameN
    1.13     of [] => error ("no such instance: " ^ quote (snd inst ^ " :: " ^ fst inst))
    1.14      | thyname :: _ => thyname;
    1.15 -  fun thyname_of_const thy c = case Code.get_datatype_of_constr thy c
    1.16 -     of SOME dtco => thyname_of_tyco thy dtco
    1.17 -      | NONE => (case AxClass.class_of_param thy c
    1.18 -         of SOME class => thyname_of_class thy class
    1.19 -          | NONE => (case AxClass.inst_of_param thy c
    1.20 -             of SOME (c, tyco) => thyname_of_instance thy
    1.21 -                  ((the o AxClass.class_of_param thy) c, tyco)
    1.22 -              | NONE => thyname_of thy (Consts.the_tags (Sign.consts_of thy)) c));
    1.23 +  fun thyname_of_const thy c = case AxClass.class_of_param thy c
    1.24 +   of SOME class => thyname_of_class thy class
    1.25 +    | NONE => (case Code.get_datatype_of_constr thy c
    1.26 +       of SOME dtco => thyname_of_tyco thy dtco
    1.27 +        | NONE => thyname_of thy (Consts.the_tags (Sign.consts_of thy)) c);
    1.28    fun namify thy get_basename get_thyname name =
    1.29      let
    1.30        val prefix = get_thyname thy name;
    1.31 @@ -453,27 +451,26 @@
    1.32  
    1.33  fun ensure_stmt lookup declare generate thing (dep, (naming, program)) =
    1.34    let
    1.35 -    fun add_dep name = case dep
    1.36 -     of NONE => I | SOME dep => Graph.add_edge (dep, name);
    1.37 -  in case lookup naming thing
    1.38 -   of SOME name => program
    1.39 +    fun add_dep name = case dep of NONE => I
    1.40 +      | SOME dep => Graph.add_edge (dep, name);
    1.41 +    val (name, naming') = case lookup naming thing
    1.42 +     of SOME name => (name, naming)
    1.43 +      | NONE => declare thing naming;
    1.44 +  in case try (Graph.get_node program) name
    1.45 +   of SOME stmt => program
    1.46          |> add_dep name
    1.47 -        |> pair naming
    1.48 +        |> pair naming'
    1.49          |> pair dep
    1.50          |> pair name
    1.51 -    | NONE => let
    1.52 -          val (name, naming') = declare thing naming;
    1.53 -        in
    1.54 -          program
    1.55 -          |> Graph.default_node (name, NoStmt)
    1.56 -          |> add_dep name
    1.57 -          |> pair naming'
    1.58 -          |> curry generate (SOME name)
    1.59 -          ||> snd
    1.60 -          |-> (fn stmt => (apsnd o Graph.map_node name) (K stmt))
    1.61 -          |> pair dep
    1.62 -          |> pair name
    1.63 -        end
    1.64 +    | NONE => program
    1.65 +        |> Graph.default_node (name, NoStmt)
    1.66 +        |> add_dep name
    1.67 +        |> pair naming'
    1.68 +        |> curry generate (SOME name)
    1.69 +        ||> snd
    1.70 +        |-> (fn stmt => (apsnd o Graph.map_node name) (K stmt))
    1.71 +        |> pair dep
    1.72 +        |> pair name
    1.73    end;
    1.74  
    1.75  fun not_wellsorted thy thm ty sort e =
    1.76 @@ -719,15 +716,14 @@
    1.77  (
    1.78    type T = naming * program;
    1.79    val empty = (empty_naming, Graph.empty);
    1.80 -  fun purge thy cs (naming, program) = empty (*FIXME: problem: un-declaration of names
    1.81 +  fun purge thy cs (naming, program) =
    1.82      let
    1.83 -      val cs_exisiting =
    1.84 -        map_filter (Code_Name.const_rev thy) (Graph.keys program);
    1.85 -      val dels = (Graph.all_preds program
    1.86 -          o map (Code_Name.const thy)
    1.87 -          o filter (member (op =) cs_exisiting)
    1.88 -        ) cs;
    1.89 -    in Graph.del_nodes dels program end;*)
    1.90 +      val names_delete = cs
    1.91 +        |> map_filter (lookup_const naming)
    1.92 +        |> filter (can (Graph.get_node program))
    1.93 +        |> Graph.all_preds program;
    1.94 +      val program' = Graph.del_nodes names_delete program;
    1.95 +    in (naming, program') end;
    1.96  );
    1.97  
    1.98  val cached_program = Program.get;
     2.1 --- a/src/Tools/nbe.ML	Tue Oct 28 16:59:01 2008 +0100
     2.2 +++ b/src/Tools/nbe.ML	Tue Oct 28 16:59:02 2008 +0100
     2.3 @@ -336,14 +336,17 @@
     2.4        #-> fold (fn (name, univ) => (Graph.map_node name o apfst) (K (SOME univ))))
     2.5    end;
     2.6  
     2.7 -fun ensure_stmts ctxt program =
     2.8 +fun ensure_stmts ctxt naming program =
     2.9    let
    2.10      fun add_stmts names (gr, (maxidx, idx_tab)) = if exists ((can o Graph.get_node) gr) names
    2.11        then (gr, (maxidx, idx_tab))
    2.12        else (gr, (maxidx, idx_tab))
    2.13          |> compile_stmts ctxt (map (fn name => ((name, Graph.get_node program name),
    2.14            Graph.imm_succs program name)) names);
    2.15 -  in fold_rev add_stmts (Graph.strong_conn program) end;
    2.16 +  in
    2.17 +    fold_rev add_stmts (Graph.strong_conn program)
    2.18 +    #> pair naming
    2.19 +  end;
    2.20  
    2.21  
    2.22  (** evaluation **)
    2.23 @@ -404,25 +407,25 @@
    2.24  
    2.25  structure Nbe_Functions = CodeDataFun
    2.26  (
    2.27 -  type T = (Univ option * int) Graph.T * (int * string Inttab.table);
    2.28 -  val empty = (Graph.empty, (0, Inttab.empty));
    2.29 -  fun purge thy cs (gr, (maxidx, idx_tab)) = empty (*FIXME
    2.30 +  type T = Code_Thingol.naming * ((Univ option * int) Graph.T * (int * string Inttab.table));
    2.31 +  val empty = (Code_Thingol.empty_naming, (Graph.empty, (0, Inttab.empty)));
    2.32 +  fun purge thy cs (naming, (gr, (maxidx, idx_tab))) =
    2.33      let
    2.34 -      val cs_exisiting =
    2.35 -        map_filter (Code_Name.const_rev thy) (Graph.keys gr);
    2.36 -      val dels = (Graph.all_preds gr
    2.37 -          o map (Code_Name.const thy)
    2.38 -          o filter (member (op =) cs_exisiting)
    2.39 -        ) cs;
    2.40 -    in (Graph.del_nodes dels gr, (maxidx, idx_tab)) end*);
    2.41 +      val names_delete = cs
    2.42 +        |> map_filter (Code_Thingol.lookup_const naming)
    2.43 +        |> filter (can (Graph.get_node gr))
    2.44 +        |> Graph.all_preds gr;
    2.45 +      val gr' = Graph.del_nodes names_delete gr;
    2.46 +    in (naming, (gr', (maxidx, idx_tab))) end;
    2.47  );
    2.48  
    2.49  (* compilation, evaluation and reification *)
    2.50  
    2.51 -fun compile_eval thy program vs_ty_t deps =
    2.52 +fun compile_eval thy naming program vs_ty_t deps =
    2.53    let
    2.54      val ctxt = ProofContext.init thy;
    2.55 -    val (gr, (_, idx_tab)) = Nbe_Functions.change thy (ensure_stmts ctxt program);
    2.56 +    val (_, (gr, (_, idx_tab))) =
    2.57 +      Nbe_Functions.change thy (ensure_stmts ctxt naming program o snd);
    2.58    in
    2.59      vs_ty_t
    2.60      |> eval_term ctxt gr deps
    2.61 @@ -431,7 +434,7 @@
    2.62  
    2.63  (* evaluation with type reconstruction *)
    2.64  
    2.65 -fun eval thy t program vs_ty_t deps =
    2.66 +fun eval thy t naming program vs_ty_t deps =
    2.67    let
    2.68      fun subst_const f = map_aterms (fn t as Term.Const (c, ty) => Term.Const (f c, ty)
    2.69        | t => t);
    2.70 @@ -450,7 +453,7 @@
    2.71          ^ setmp show_types true (Syntax.string_of_term_global thy) t);
    2.72      val string_of_term = setmp show_types true (Syntax.string_of_term_global thy);
    2.73    in
    2.74 -    compile_eval thy program vs_ty_t deps
    2.75 +    compile_eval thy naming program vs_ty_t deps
    2.76      |> tracing (fn t => "Normalized:\n" ^ string_of_term t)
    2.77      |> subst_triv_consts
    2.78      |> type_frees
    2.79 @@ -464,8 +467,8 @@
    2.80  (* evaluation oracle *)
    2.81  
    2.82  val (_, norm_oracle) = Context.>>> (Context.map_theory_result
    2.83 -  (Thm.add_oracle ("norm", fn (thy, t, program, vs_ty_t, deps) =>
    2.84 -    Thm.cterm_of thy (Logic.mk_equals (t, eval thy t program vs_ty_t deps)))));
    2.85 +  (Thm.add_oracle ("norm", fn (thy, t, naming, program, vs_ty_t, deps) =>
    2.86 +    Thm.cterm_of thy (Logic.mk_equals (t, eval thy t naming program vs_ty_t deps)))));
    2.87  
    2.88  fun add_triv_classes thy =
    2.89    let
    2.90 @@ -479,13 +482,14 @@
    2.91  fun norm_conv ct =
    2.92    let
    2.93      val thy = Thm.theory_of_cterm ct;
    2.94 -    fun evaluator' t naming program vs_ty_t deps = norm_oracle (thy, t, program, vs_ty_t, deps);
    2.95 +    fun evaluator' t naming program vs_ty_t deps =
    2.96 +      norm_oracle (thy, t, naming, program, vs_ty_t, deps);
    2.97      fun evaluator t = (add_triv_classes thy t, evaluator' t);
    2.98    in Code_Thingol.eval_conv thy evaluator ct end;
    2.99  
   2.100  fun norm_term thy t =
   2.101    let
   2.102 -    fun evaluator' t naming program vs_ty_t deps = eval thy t program vs_ty_t deps;
   2.103 +    fun evaluator' t naming program vs_ty_t deps = eval thy t naming program vs_ty_t deps;
   2.104      fun evaluator t = (add_triv_classes thy t, evaluator' t);
   2.105    in (Code.postprocess_term thy o Code_Thingol.eval_term thy evaluator) t end;
   2.106