diff -r 179ff9cb160b -r 5b25fee0362c src/Tools/code/code_thingol.ML --- 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*)