1.1 --- a/src/Tools/code/code_thingol.ML Thu Aug 28 22:08:11 2008 +0200
1.2 +++ b/src/Tools/code/code_thingol.ML Thu Aug 28 22:09:20 2008 +0200
1.3 @@ -89,7 +89,7 @@
1.4 -> term -> 'a;
1.5 end;
1.6
1.7 -structure CodeThingol: CODE_THINGOL =
1.8 +structure Code_Thingol: CODE_THINGOL =
1.9 struct
1.10
1.11 (** auxiliary **)
1.12 @@ -353,7 +353,7 @@
1.13 let
1.14 val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class;
1.15 val cs = #params (AxClass.get_info thy class);
1.16 - val class' = CodeName.class thy class;
1.17 + val class' = Code_Name.class thy class;
1.18 val stmt_class =
1.19 fold_map (fn superclass => ensure_class thy algbr funcgr superclass
1.20 ##>> ensure_classrel thy algbr funcgr (class, superclass)) superclasses
1.21 @@ -363,7 +363,7 @@
1.22 in ensure_stmt stmt_class class' end
1.23 and ensure_classrel thy algbr funcgr (subclass, superclass) =
1.24 let
1.25 - val classrel' = CodeName.classrel thy (subclass, superclass);
1.26 + val classrel' = Code_Name.classrel thy (subclass, superclass);
1.27 val stmt_classrel =
1.28 ensure_class thy algbr funcgr subclass
1.29 ##>> ensure_class thy algbr funcgr superclass
1.30 @@ -383,7 +383,7 @@
1.31 ##>> fold_map (exprgen_typ thy algbr funcgr) tys) cos
1.32 #>> Datatype
1.33 end;
1.34 - val tyco' = CodeName.tyco thy tyco;
1.35 + val tyco' = Code_Name.tyco thy tyco;
1.36 in ensure_stmt stmt_datatype tyco' end
1.37 and exprgen_tyvar_sort thy (algbr as (proj_sort, _)) funcgr (v, sort) =
1.38 fold_map (ensure_class thy algbr funcgr) (proj_sort sort)
1.39 @@ -467,11 +467,11 @@
1.40 ##>> fold_map exprgen_classparam_inst classparams
1.41 #>> (fn ((((class, tyco), arity), superarities), classparams) =>
1.42 Classinst ((class, (tyco, arity)), (superarities, classparams)));
1.43 - val inst = CodeName.instance thy (class, tyco);
1.44 + val inst = Code_Name.instance thy (class, tyco);
1.45 in ensure_stmt stmt_inst inst end
1.46 and ensure_const thy algbr funcgr c =
1.47 let
1.48 - val c' = CodeName.const thy c;
1.49 + val c' = Code_Name.const thy c;
1.50 fun stmt_datatypecons tyco =
1.51 ensure_tyco thy algbr funcgr tyco
1.52 #>> Datatypecons;
1.53 @@ -480,12 +480,12 @@
1.54 #>> Classparam;
1.55 fun stmt_fun trns =
1.56 let
1.57 - val raw_thms = CodeFuncgr.funcs funcgr c;
1.58 - val (vs, raw_ty) = CodeFuncgr.typ funcgr c;
1.59 + val raw_thms = Code_Funcgr.funcs funcgr c;
1.60 + val (vs, raw_ty) = Code_Funcgr.typ funcgr c;
1.61 val ty = Logic.unvarifyT raw_ty;
1.62 val thms = if (null o Term.typ_tfrees) ty orelse (null o fst o strip_type) ty
1.63 then raw_thms
1.64 - else map (CodeUnit.expand_eta 1) raw_thms;
1.65 + else map (Code_Unit.expand_eta 1) raw_thms;
1.66 in
1.67 trns
1.68 |> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
1.69 @@ -522,7 +522,7 @@
1.70 and exprgen_const thy algbr funcgr thm (c, ty) =
1.71 let
1.72 val tys = Sign.const_typargs thy (c, ty);
1.73 - val sorts = (map snd o fst o CodeFuncgr.typ funcgr) c;
1.74 + val sorts = (map snd o fst o Code_Funcgr.typ funcgr) c;
1.75 val tys_args = (fst o Term.strip_type) ty;
1.76 in
1.77 ensure_const thy algbr funcgr c
1.78 @@ -552,7 +552,7 @@
1.79 val ([v_ty], body) = Term.strip_abs_eta 1 (the_single (nth_drop n ts))
1.80 in [(Free v_ty, body)] end
1.81 | mk_ds cases = map_filter (uncurry mk_case)
1.82 - (AList.make (CodeUnit.no_args thy) cases ~~ nth_drop n ts);
1.83 + (AList.make (Code_Unit.no_args thy) cases ~~ nth_drop n ts);
1.84 in
1.85 exprgen_term thy algbr funcgr thm dt
1.86 ##>> exprgen_typ thy algbr funcgr dty
1.87 @@ -596,9 +596,9 @@
1.88 fun purge thy cs program =
1.89 let
1.90 val cs_exisiting =
1.91 - map_filter (CodeName.const_rev thy) (Graph.keys program);
1.92 + map_filter (Code_Name.const_rev thy) (Graph.keys program);
1.93 val dels = (Graph.all_preds program
1.94 - o map (CodeName.const thy)
1.95 + o map (Code_Name.const thy)
1.96 o filter (member (op =) cs_exisiting)
1.97 ) cs;
1.98 in Graph.del_nodes dels program end;
1.99 @@ -626,7 +626,7 @@
1.100 fun generate_consts thy algebra funcgr =
1.101 fold_map (ensure_const thy algebra funcgr);
1.102 in
1.103 - generate thy (CodeFuncgr.make thy cs) generate_consts cs
1.104 + generate thy (Code_Funcgr.make thy cs) generate_consts cs
1.105 |-> project_consts
1.106 end;
1.107
1.108 @@ -646,14 +646,14 @@
1.109 fun term_value (dep, program1) =
1.110 let
1.111 val Fun ((vs, ty), [(([], t), _)]) =
1.112 - Graph.get_node program1 CodeName.value_name;
1.113 - val deps = Graph.imm_succs program1 CodeName.value_name;
1.114 - val program2 = Graph.del_nodes [CodeName.value_name] program1;
1.115 + Graph.get_node program1 Code_Name.value_name;
1.116 + val deps = Graph.imm_succs program1 Code_Name.value_name;
1.117 + val program2 = Graph.del_nodes [Code_Name.value_name] program1;
1.118 val deps_all = Graph.all_succs program2 deps;
1.119 val program3 = Graph.subgraph (member (op =) deps_all) program2;
1.120 in ((program3, (((vs, ty), t), deps)), (dep, program2)) end;
1.121 in
1.122 - ensure_stmt stmt_value CodeName.value_name
1.123 + ensure_stmt stmt_value Code_Name.value_name
1.124 #> snd
1.125 #> term_value
1.126 end;
1.127 @@ -670,10 +670,10 @@
1.128 in (t', evaluator'' evaluator''') end;
1.129 in eval_kind thy evaluator' end
1.130
1.131 -fun eval_conv thy = eval CodeFuncgr.eval_conv thy;
1.132 -fun eval_term thy = eval CodeFuncgr.eval_term thy;
1.133 +fun eval_conv thy = eval Code_Funcgr.eval_conv thy;
1.134 +fun eval_term thy = eval Code_Funcgr.eval_term thy;
1.135
1.136 end; (*struct*)
1.137
1.138
1.139 -structure BasicCodeThingol: BASIC_CODE_THINGOL = CodeThingol;
1.140 +structure Basic_Code_Thingol: BASIC_CODE_THINGOL = Code_Thingol;