explizit dependencies
authorhaftmann
Mon Aug 20 18:07:31 2007 +0200 (2007-08-20)
changeset 24347245ff8661b8c
parent 24346 4f6b71b84ee7
child 24348 c708ea5b109a
explizit dependencies
src/Tools/nbe.ML
     1.1 --- a/src/Tools/nbe.ML	Mon Aug 20 18:07:30 2007 +0200
     1.2 +++ b/src/Tools/nbe.ML	Mon Aug 20 18:07:31 2007 +0200
     1.3 @@ -187,19 +187,19 @@
     1.4      fun of_iterm t =
     1.5        let
     1.6          val (t', ts) = CodeThingol.unfold_app t
     1.7 -      in of_itermapp t' (fold (cons o of_iterm) ts []) end
     1.8 -    and of_itermapp (IConst (c, (dss, _))) ts =
     1.9 -          (case num_args c
    1.10 -           of SOME n => if n <= length ts
    1.11 -                then let val (args2, args1) = chop (length ts - n) ts
    1.12 -                in nbe_apps (nbe_fun c `$` ml_list args1) args2
    1.13 -                end else nbe_const c ts
    1.14 -            | NONE => if is_fun c then nbe_apps (nbe_fun c) ts
    1.15 -                else nbe_const c ts)
    1.16 -      | of_itermapp (IVar v) ts = nbe_apps (nbe_bound v) ts
    1.17 -      | of_itermapp ((v, _) `|-> t) ts =
    1.18 +      in of_iapp t' (fold (cons o of_iterm) ts []) end
    1.19 +    and of_iconst c ts = case num_args c
    1.20 +     of SOME n => if n <= length ts
    1.21 +          then let val (args2, args1) = chop (length ts - n) ts
    1.22 +          in nbe_apps (nbe_fun c `$` ml_list args1) args2
    1.23 +          end else nbe_const c ts
    1.24 +      | NONE => if is_fun c then nbe_apps (nbe_fun c) ts
    1.25 +          else nbe_const c ts
    1.26 +    and of_iapp (IConst (c, (dss, _))) ts = of_iconst c ts
    1.27 +      | of_iapp (IVar v) ts = nbe_apps (nbe_bound v) ts
    1.28 +      | of_iapp ((v, _) `|-> t) ts =
    1.29            nbe_apps (nbe_abss 1 (ml_abs (ml_list [nbe_bound v]) (of_iterm t))) ts
    1.30 -      | of_itermapp (ICase (((t, _), cs), t0)) ts =
    1.31 +      | of_iapp (ICase (((t, _), cs), t0)) ts =
    1.32            nbe_apps (ml_cases (of_iterm t) (map (pairself of_iterm) cs
    1.33              @ [("_", of_iterm t0)])) ts
    1.34    in of_iterm end;
    1.35 @@ -215,8 +215,8 @@
    1.36      val default_eqn = ([ml_list default_params], nbe_const c default_params);
    1.37    in map assemble_eqn eqns @ [default_eqn] end;
    1.38  
    1.39 -fun assemble_eqnss thy is_fun [] = ([], "")
    1.40 -  | assemble_eqnss thy is_fun eqnss =
    1.41 +fun assemble_eqnss thy is_fun ([], deps) = ([], "")
    1.42 +  | assemble_eqnss thy is_fun (eqnss, deps) =
    1.43        let
    1.44          val cs = map fst eqnss;
    1.45          val num_args = cs ~~ map (fn (_, (args, rhs) :: _) => length args) eqnss;
    1.46 @@ -238,25 +238,26 @@
    1.47      val result = ml_list [nbe_value `$` ml_list (map nbe_free frees)];
    1.48    in ([nbe_value], ml_Let (bind_funs @ [bind_value]) result) end;
    1.49  
    1.50 -fun eqns_of_stmt (name, CodeThingol.Fun ([], _)) =
    1.51 +fun eqns_of_stmt ((_, CodeThingol.Fun ([], _)), _) =
    1.52        NONE
    1.53 -  | eqns_of_stmt (name, CodeThingol.Fun (eqns, _)) =
    1.54 -      SOME (name, eqns)
    1.55 -  | eqns_of_stmt (_, CodeThingol.Datatypecons _) =
    1.56 +  | eqns_of_stmt ((name, CodeThingol.Fun (eqns, _)), deps) =
    1.57 +      SOME ((name, eqns), deps)
    1.58 +  | eqns_of_stmt ((_, CodeThingol.Datatypecons _), _) =
    1.59        NONE
    1.60 -  | eqns_of_stmt (_, CodeThingol.Datatype _) =
    1.61 +  | eqns_of_stmt ((_, CodeThingol.Datatype _), _) =
    1.62        NONE
    1.63 -  | eqns_of_stmt (_, CodeThingol.Class _) =
    1.64 +  | eqns_of_stmt ((_, CodeThingol.Class _), _) =
    1.65        NONE
    1.66 -  | eqns_of_stmt (_, CodeThingol.Classrel _) =
    1.67 +  | eqns_of_stmt ((_, CodeThingol.Classrel _), _) =
    1.68        NONE
    1.69 -  | eqns_of_stmt (_, CodeThingol.Classop _) =
    1.70 +  | eqns_of_stmt ((_, CodeThingol.Classop _), _) =
    1.71        NONE
    1.72 -  | eqns_of_stmt (_, CodeThingol.Classinst _) =
    1.73 +  | eqns_of_stmt ((_, CodeThingol.Classinst _), _) =
    1.74        NONE;
    1.75  
    1.76  fun compile_stmts thy is_fun =
    1.77    map_filter eqns_of_stmt
    1.78 +  #> split_list
    1.79    #> assemble_eqnss thy is_fun
    1.80    #> compile_univs (Nbe_Functions.get thy);
    1.81  
    1.82 @@ -278,9 +279,11 @@
    1.83          val compiled = compile_stmts thy (Symtab.defined tab) stmts;
    1.84        in Nbe_Functions.change thy (fold Symtab.update compiled) end;
    1.85      val nbe_tab = Nbe_Functions.get thy;
    1.86 -    val stmtss =
    1.87 -      map (AList.make (Graph.get_node code)) (rev (Graph.strong_conn code))
    1.88 -      |> (map o filter_out) (Symtab.defined nbe_tab o fst)
    1.89 +    val stmtss = rev (Graph.strong_conn code)
    1.90 +      |> (map o map_filter) (fn name => if Symtab.defined nbe_tab name
    1.91 +           then NONE
    1.92 +           else SOME ((name, Graph.get_node code name), Graph.imm_succs code name))
    1.93 +      |> filter_out null
    1.94    in fold compile' stmtss nbe_tab end;
    1.95  
    1.96  (* re-conversion *)
    1.97 @@ -311,6 +314,7 @@
    1.98  
    1.99  fun eval thy code t t' deps =
   1.100    let
   1.101 +    val ty = type_of t;
   1.102      fun subst_Frees [] = I
   1.103        | subst_Frees inst =
   1.104            Term.map_aterms (fn (t as Term.Free (s, _)) => the_default t (AList.lookup (op =) inst s)
   1.105 @@ -318,12 +322,11 @@
   1.106      val anno_vars =
   1.107        subst_Frees (map (fn (s, T) => (s, Term.Free (s, T))) (Term.add_frees t []))
   1.108        #> subst_Vars (map (fn (ixn, T) => (ixn, Var (ixn, T))) (Term.add_vars t []))
   1.109 +    fun constrain t =
   1.110 +      singleton (ProofContext.infer_types_pats (ProofContext.init thy)) (TypeInfer.constrain t ty);
   1.111      fun check_tvars t = if null (Term.term_tvars t) then t else
   1.112        error ("Illegal schematic type variables in normalized term: "
   1.113          ^ setmp show_types true (Sign.string_of_term thy) t);
   1.114 -    val ty = type_of t;
   1.115 -    fun constrain t =
   1.116 -      singleton (ProofContext.infer_types_pats (ProofContext.init thy)) (TypeInfer.constrain t ty);
   1.117    in
   1.118      (t', deps)
   1.119      |> eval_term thy (Symtab.defined (ensure_funs thy code))