--- a/src/Tools/code/code_thingol.ML Wed Mar 04 10:43:39 2009 +0100
+++ b/src/Tools/code/code_thingol.ML Wed Mar 04 10:45:52 2009 +0100
@@ -109,7 +109,7 @@
let val (xs', x') = unfoldr dest x2 in (x1::xs', x') end;
-(** language core - types, patterns, expressions **)
+(** language core - types, terms **)
type vname = string;
@@ -131,31 +131,6 @@
| ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
(*see also signature*)
-(*
- variable naming conventions
-
- bare names:
- variable names v
- class names class
- type constructor names tyco
- datatype names dtco
- const names (general) c (const)
- constructor names co
- class parameter names classparam
- arbitrary name s
-
- v, c, co, classparam also annotated with types etc.
-
- constructs:
- sort sort
- type parameters vs
- type ty
- type schemes tysm
- term t
- (term as pattern) p
- instance (class, tyco) inst
- *)
-
val op `$$ = Library.foldl (op `$);
val op `|--> = Library.foldr (op `|->);
@@ -478,7 +453,7 @@
let
val err_class = Sorts.class_error (Syntax.pp_global thy) e;
val err_thm = case thm
- of SOME thm => "\n(in defining equation " ^ Display.string_of_thm thm ^ ")" | NONE => "";
+ of SOME thm => "\n(in code equation " ^ Display.string_of_thm thm ^ ")" | NONE => "";
val err_typ = "Type " ^ Syntax.string_of_typ_global thy ty ^ " not of sort "
^ Syntax.string_of_sort_global thy sort;
in error ("Wellsortedness error" ^ err_thm ^ ":\n" ^ err_typ ^ "\n" ^ err_class) end;
@@ -486,12 +461,6 @@
(* translation *)
-(*FIXME move to code(_unit).ML*)
-fun get_case_scheme thy c = case Code.get_case_data thy c
- of SOME (proto_case_scheme as (_, case_pats)) =>
- SOME (1 + (if null case_pats then 1 else length case_pats), proto_case_scheme)
- | NONE => NONE
-
fun ensure_class thy (algbr as (_, algebra)) funcgr class =
let
val superclasses = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
@@ -526,9 +495,8 @@
and translate_tyvar_sort thy (algbr as (proj_sort, _)) funcgr (v, sort) =
fold_map (ensure_class thy algbr funcgr) (proj_sort sort)
#>> (fn sort => (unprefix "'" v, sort))
-and translate_typ thy algbr funcgr (TFree v_sort) =
- translate_tyvar_sort thy algbr funcgr v_sort
- #>> (fn (v, sort) => ITyVar v)
+and translate_typ thy algbr funcgr (TFree (v, _)) =
+ pair (ITyVar (unprefix "'" v))
| translate_typ thy algbr funcgr (Type (tyco, tys)) =
ensure_tyco thy algbr funcgr tyco
##>> fold_map (translate_typ thy algbr funcgr) tys
@@ -543,16 +511,8 @@
Global ((class, tyco), yss)
| class_relation (Local (classrels, v), subclass) superclass =
Local ((subclass, superclass) :: classrels, v);
- fun norm_typargs ys =
- let
- val raw_sort = map snd ys;
- val sort = Sorts.minimize_sort algebra raw_sort;
- in
- map_filter (fn (y, class) =>
- if member (op =) sort class then SOME y else NONE) ys
- end;
fun type_constructor tyco yss class =
- Global ((class, tyco), map norm_typargs yss);
+ Global ((class, tyco), (map o map) fst yss);
fun type_variable (TFree (v, sort)) =
let
val sort' = proj_sort sort;
@@ -622,9 +582,8 @@
fun stmt_classparam class =
ensure_class thy algbr funcgr class
#>> (fn class => Classparam (c, class));
- fun stmt_fun ((vs, raw_ty), raw_thms) =
+ fun stmt_fun ((vs, ty), raw_thms) =
let
- val ty = Logic.unvarifyT raw_ty;
val thms = if null (Term.add_tfreesT ty []) orelse (null o fst o strip_type) ty
then raw_thms
else (map o apfst) (Code_Unit.expand_eta thy 1) raw_thms;
@@ -638,7 +597,7 @@
of SOME tyco => stmt_datatypecons tyco
| NONE => (case AxClass.class_of_param thy c
of SOME class => stmt_classparam class
- | NONE => stmt_fun (Code_Funcgr.typ funcgr c, Code_Funcgr.eqns funcgr c))
+ | NONE => stmt_fun (Code_Wellsorted.typ funcgr c, Code_Wellsorted.eqns funcgr c))
in ensure_stmt lookup_const (declare_const thy) stmt_const c end
and translate_term thy algbr funcgr thm (Const (c, ty)) =
translate_app thy algbr funcgr thm ((c, ty), [])
@@ -663,7 +622,7 @@
and translate_const thy algbr funcgr thm (c, ty) =
let
val tys = Sign.const_typargs thy (c, ty);
- val sorts = (map snd o fst o Code_Funcgr.typ funcgr) c;
+ val sorts = (map snd o fst o Code_Wellsorted.typ funcgr) c;
val tys_args = (fst o Term.strip_type) ty;
in
ensure_const thy algbr funcgr c
@@ -671,7 +630,7 @@
##>> fold_map (translate_typ thy algbr funcgr) tys_args
#>> (fn ((c, iss), tys) => IConst (c, (iss, tys)))
end
-and translate_app_default thy algbr funcgr thm (c_ty, ts) =
+and translate_app_const thy algbr funcgr thm (c_ty, ts) =
translate_const thy algbr funcgr thm c_ty
##>> fold_map (translate_term thy algbr funcgr thm) ts
#>> (fn (t, ts) => t `$$ ts)
@@ -683,11 +642,6 @@
val ts_clause = nth_drop t_pos ts;
fun mk_clause (co, num_co_args) t =
let
- val _ = if (is_some o Code.get_datatype_of_constr thy) co then ()
- else error ("Non-constructor " ^ quote co
- ^ " encountered in case pattern"
- ^ (case thm of NONE => ""
- | SOME thm => ", in equation\n" ^ Display.string_of_thm thm))
val (vs, body) = Term.strip_abs_eta num_co_args t;
val not_undefined = case body
of (Const (c, _)) => not (Code.is_undefined thy c)
@@ -722,26 +676,28 @@
#>> pair b) clauses
#>> (fn (((const, t), ty), ds) => mk_icase const t ty ds)
end
-and translate_app thy algbr funcgr thm ((c, ty), ts) = case get_case_scheme thy c
- of SOME (case_scheme as (num_args, _)) =>
- if length ts < num_args then
- let
- val k = length ts;
- val tys = (curry Library.take (num_args - k) o curry Library.drop k o fst o strip_type) ty;
- val ctxt = (fold o fold_aterms) Term.declare_term_frees ts Name.context;
- val vs = Name.names ctxt "a" tys;
- in
- fold_map (translate_typ thy algbr funcgr) tys
- ##>> translate_case thy algbr funcgr thm case_scheme ((c, ty), ts @ map Free vs)
- #>> (fn (tys, t) => map2 (fn (v, _) => pair v) vs tys `|--> t)
- end
- else if length ts > num_args then
- translate_case thy algbr funcgr thm case_scheme ((c, ty), Library.take (num_args, ts))
- ##>> fold_map (translate_term thy algbr funcgr thm) (Library.drop (num_args, ts))
- #>> (fn (t, ts) => t `$$ ts)
- else
- translate_case thy algbr funcgr thm case_scheme ((c, ty), ts)
- | NONE => translate_app_default thy algbr funcgr thm ((c, ty), ts);
+and translate_app_case thy algbr funcgr thm (case_scheme as (num_args, _)) ((c, ty), ts) =
+ if length ts < num_args then
+ let
+ val k = length ts;
+ val tys = (curry Library.take (num_args - k) o curry Library.drop k o fst o strip_type) ty;
+ val ctxt = (fold o fold_aterms) Term.declare_term_frees ts Name.context;
+ val vs = Name.names ctxt "a" tys;
+ in
+ fold_map (translate_typ thy algbr funcgr) tys
+ ##>> translate_case thy algbr funcgr thm case_scheme ((c, ty), ts @ map Free vs)
+ #>> (fn (tys, t) => map2 (fn (v, _) => pair v) vs tys `|--> t)
+ end
+ else if length ts > num_args then
+ translate_case thy algbr funcgr thm case_scheme ((c, ty), Library.take (num_args, ts))
+ ##>> fold_map (translate_term thy algbr funcgr thm) (Library.drop (num_args, ts))
+ #>> (fn (t, ts) => t `$$ ts)
+ else
+ translate_case thy algbr funcgr thm case_scheme ((c, ty), ts)
+and translate_app thy algbr funcgr thm (c_ty_ts as ((c, _), _)) =
+ case Code.get_case_scheme thy c
+ of SOME case_scheme => translate_app_case thy algbr funcgr thm case_scheme c_ty_ts
+ | NONE => translate_app_const thy algbr funcgr thm c_ty_ts;
(* store *)
@@ -779,7 +735,7 @@
fun generate_consts thy algebra funcgr =
fold_map (ensure_const thy algebra funcgr);
in
- invoke_generation thy (Code_Funcgr.make thy cs) generate_consts cs
+ invoke_generation thy (Code_Wellsorted.make thy cs) generate_consts cs
|-> project_consts
end;
@@ -822,8 +778,8 @@
in evaluator'' naming program vs_ty_t deps end;
in (t', evaluator') end
-fun eval_conv thy = Code_Funcgr.eval_conv thy o eval thy;
-fun eval_term thy = Code_Funcgr.eval_term thy o eval thy;
+fun eval_conv thy = Code_Wellsorted.eval_conv thy o eval thy;
+fun eval_term thy = Code_Wellsorted.eval_term thy o eval thy;
end; (*struct*)