src/Tools/nbe.ML
changeset 24219 e558fe311376
parent 24166 7b28dc69bdbb
child 24283 8ca96f4e49cd
     1.1 --- a/src/Tools/nbe.ML	Fri Aug 10 17:04:24 2007 +0200
     1.2 +++ b/src/Tools/nbe.ML	Fri Aug 10 17:04:34 2007 +0200
     1.3 @@ -25,7 +25,7 @@
     1.4    val app: Univ -> Univ -> Univ              (*explicit application*)
     1.5  
     1.6    val univs_ref: Univ list ref 
     1.7 -  val lookup_fun: CodegenNames.const -> Univ
     1.8 +  val lookup_fun: CodeName.const -> Univ
     1.9  
    1.10    val normalization_conv: cterm -> thm
    1.11  
    1.12 @@ -183,7 +183,7 @@
    1.13  
    1.14  end;
    1.15  
    1.16 -open BasicCodegenThingol;
    1.17 +open BasicCodeThingol;
    1.18  
    1.19  (* greetings to Tarski *)
    1.20  
    1.21 @@ -191,7 +191,7 @@
    1.22    let
    1.23      fun of_iterm t =
    1.24        let
    1.25 -        val (t', ts) = CodegenThingol.unfold_app t
    1.26 +        val (t', ts) = CodeThingol.unfold_app t
    1.27        in of_itermapp t' (fold (cons o of_iterm) ts []) end
    1.28      and of_itermapp (IConst (c, (dss, _))) ts =
    1.29            (case num_args c
    1.30 @@ -225,7 +225,7 @@
    1.31        let
    1.32          val cs = map fst eqnss;
    1.33          val num_args = cs ~~ map (fn (_, (args, rhs) :: _) => length args) eqnss;
    1.34 -        val funs = fold (fold (CodegenThingol.fold_constnames
    1.35 +        val funs = fold (fold (CodeThingol.fold_constnames
    1.36            (insert (op =))) o map snd o snd) eqnss [];
    1.37          val bind_funs = map nbe_lookup (filter is_fun funs);
    1.38          val bind_locals = ml_fundefs (map nbe_fun cs ~~ map
    1.39 @@ -235,29 +235,29 @@
    1.40  
    1.41  fun assemble_eval thy is_fun t =
    1.42    let
    1.43 -    val funs = CodegenThingol.fold_constnames (insert (op =)) t [];
    1.44 -    val frees = CodegenThingol.fold_unbound_varnames (insert (op =)) t [];
    1.45 +    val funs = CodeThingol.fold_constnames (insert (op =)) t [];
    1.46 +    val frees = CodeThingol.fold_unbound_varnames (insert (op =)) t [];
    1.47      val bind_funs = map nbe_lookup (filter is_fun funs);
    1.48      val bind_value = ml_fundefs [(nbe_value, [([ml_list (map nbe_bound frees)],
    1.49        assemble_iterm thy is_fun (K NONE) t)])];
    1.50      val result = ml_list [nbe_value `$` ml_list (map nbe_free frees)];
    1.51    in ([nbe_value], ml_Let (bind_funs @ [bind_value]) result) end;
    1.52  
    1.53 -fun eqns_of_stmt (name, CodegenThingol.Fun ([], _)) =
    1.54 +fun eqns_of_stmt (name, CodeThingol.Fun ([], _)) =
    1.55        NONE
    1.56 -  | eqns_of_stmt (name, CodegenThingol.Fun (eqns, _)) =
    1.57 +  | eqns_of_stmt (name, CodeThingol.Fun (eqns, _)) =
    1.58        SOME (name, eqns)
    1.59 -  | eqns_of_stmt (_, CodegenThingol.Datatypecons _) =
    1.60 +  | eqns_of_stmt (_, CodeThingol.Datatypecons _) =
    1.61        NONE
    1.62 -  | eqns_of_stmt (_, CodegenThingol.Datatype _) =
    1.63 +  | eqns_of_stmt (_, CodeThingol.Datatype _) =
    1.64        NONE
    1.65 -  | eqns_of_stmt (_, CodegenThingol.Class _) =
    1.66 +  | eqns_of_stmt (_, CodeThingol.Class _) =
    1.67        NONE
    1.68 -  | eqns_of_stmt (_, CodegenThingol.Classrel _) =
    1.69 +  | eqns_of_stmt (_, CodeThingol.Classrel _) =
    1.70        NONE
    1.71 -  | eqns_of_stmt (_, CodegenThingol.Classop _) =
    1.72 +  | eqns_of_stmt (_, CodeThingol.Classop _) =
    1.73        NONE
    1.74 -  | eqns_of_stmt (_, CodegenThingol.Classinst _) =
    1.75 +  | eqns_of_stmt (_, CodeThingol.Classinst _) =
    1.76        NONE;
    1.77  
    1.78  fun compile_stmts thy is_fun =
    1.79 @@ -297,8 +297,8 @@
    1.80        #>> (fn ts' => list_comb (t, rev ts'))
    1.81      and of_univ bounds (Const (name, ts)) typidx =
    1.82            let
    1.83 -            val SOME (const as (c, _)) = CodegenNames.const_rev thy name;
    1.84 -            val T = CodegenData.default_typ thy const;
    1.85 +            val SOME (const as (c, _)) = CodeName.const_rev thy name;
    1.86 +            val T = Code.default_typ thy const;
    1.87              val T' = map_type_tvar (fn ((v, i), S) => TypeInfer.param (typidx + i) (v, S)) T;
    1.88              val typidx' = typidx + maxidx_of_typ T' + 1;
    1.89            in of_apps bounds (Term.Const (c, T'), ts) typidx' end
    1.90 @@ -345,7 +345,7 @@
    1.91  
    1.92  (* evaluation oracle *)
    1.93  
    1.94 -exception Normalization of CodegenThingol.code * term * CodegenThingol.iterm;
    1.95 +exception Normalization of CodeThingol.code * term * CodeThingol.iterm;
    1.96  
    1.97  fun normalization_oracle (thy, Normalization (code, t, t')) =
    1.98    Logic.mk_equals (t, eval thy code t t');
    1.99 @@ -361,7 +361,7 @@
   1.100        let
   1.101          val t = Thm.term_of ct;
   1.102        in normalization_invoke thy code t t' end;
   1.103 -  in CodegenPackage.eval_conv thy conv ct end;
   1.104 +  in CodePackage.eval_conv thy conv ct end;
   1.105  
   1.106  (* evaluation command *)
   1.107