revisiting type annotations for Haskell: necessary type annotations are not inferred on the provided theorems but using the arguments and right hand sides, as these might differ in the case of constants with abstract code types
1 (* Title: Tools/Code/code_thingol.ML
2 Author: Florian Haftmann, TU Muenchen
4 Intermediate language ("Thin-gol") representing executable code.
5 Representation and translation.
14 signature BASIC_CODE_THINGOL =
18 Dict of string list * plain_dict
20 Dict_Const of string * dict list list
21 | Dict_Var of vname * (int * int)
23 `%% of string * itype list
25 type const = string * (((itype list * dict list list) * (itype list * itype)) * bool)
26 (* f [T1..Tn] {dicts} (_::S1) .. (_..Sm) =^= (f, (([T1..Tn], dicts), [S1..Sm]) *)
29 | IVar of vname option
31 | `|=> of (vname option * itype) * iterm
32 | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
33 (*((term, type), [(selector pattern, body term )]), primitive term)*)
34 val `$$ : iterm * iterm list -> iterm;
35 val `|==> : (vname option * itype) list * iterm -> iterm;
36 type typscheme = (vname * sort) list * itype;
39 signature CODE_THINGOL =
41 include BASIC_CODE_THINGOL
43 val unfoldl: ('a -> ('a * 'b) option) -> 'a -> 'a * 'b list
44 val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a
45 val unfold_fun: itype -> itype list * itype
46 val unfold_fun_n: int -> itype -> itype list * itype
47 val unfold_app: iterm -> iterm * iterm list
48 val unfold_abs: iterm -> (vname option * itype) list * iterm
49 val split_let: iterm -> (((iterm * itype) * iterm) * iterm) option
50 val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm
51 val split_pat_abs: iterm -> ((iterm * itype) * iterm) option
52 val unfold_pat_abs: iterm -> (iterm * itype) list * iterm
53 val unfold_const_app: iterm -> (const * iterm list) option
54 val is_IVar: iterm -> bool
55 val is_IAbs: iterm -> bool
56 val eta_expand: int -> const * iterm list -> iterm
57 val contains_dict_var: iterm -> bool
58 val add_constnames: iterm -> string list -> string list
59 val add_tyconames: iterm -> string list -> string list
60 val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a
63 val empty_naming: naming
64 val lookup_class: naming -> class -> string option
65 val lookup_classrel: naming -> class * class -> string option
66 val lookup_tyco: naming -> string -> string option
67 val lookup_instance: naming -> class * string -> string option
68 val lookup_const: naming -> string -> string option
69 val ensure_declared_const: theory -> string -> naming -> string * naming
73 | Fun of string * ((typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option)
74 | Datatype of string * ((vname * sort) list *
75 ((string * vname list (*type argument wrt. canonical order*)) * itype list) list)
76 | Datatypecons of string * string
77 | Class of class * (vname * ((class * string) list * (string * itype) list))
78 | Classrel of class * class
79 | Classparam of string * class
80 | Classinst of (class * (string * (vname * sort) list) (*class and arity*))
81 * ((class * (string * (string * dict list list))) list (*super instances*)
82 * (((string * const) * (thm * bool)) list (*class parameter instances*)
83 * ((string * const) * (thm * bool)) list (*super class parameter instances*)))
84 type program = stmt Graph.T
85 val empty_funs: program -> string list
86 val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm
87 val map_terms_stmt: (iterm -> iterm) -> stmt -> stmt
88 val is_cons: program -> string -> bool
89 val is_case: stmt -> bool
90 val labelled_name: theory -> program -> string -> string
91 val group_stmts: theory -> program
92 -> ((string * stmt) list * (string * stmt) list
93 * ((string * stmt) list * (string * stmt) list)) list
95 val read_const_exprs: theory -> string list -> string list * string list
96 val consts_program: theory -> bool -> string list -> string list * (naming * program)
97 val dynamic_conv: theory -> (naming -> program
98 -> ((string * sort) list * typscheme) * iterm -> string list -> conv)
100 val dynamic_value: theory -> ((term -> term) -> 'a -> 'a) -> (naming -> program
101 -> ((string * sort) list * typscheme) * iterm -> string list -> 'a)
103 val static_conv: theory -> string list -> (naming -> program -> string list
104 -> ((string * sort) list * typscheme) * iterm -> string list -> conv)
106 val static_conv_simple: theory -> string list
107 -> (program -> (string * sort) list -> term -> conv) -> conv
108 val static_value: theory -> ((term -> term) -> 'a -> 'a) -> string list ->
109 (naming -> program -> string list
110 -> ((string * sort) list * typscheme) * iterm -> string list -> 'a)
114 structure Code_Thingol: CODE_THINGOL =
123 let val (x', xs') = unfoldl dest x1 in (x', xs' @ [x2]) end;
129 let val (xs', x') = unfoldr dest x2 in (x1::xs', x') end;
132 (** language core - types, terms **)
137 Dict of string list * plain_dict
139 Dict_Const of string * dict list list
140 | Dict_Var of vname * (int * int)
143 `%% of string * itype list
146 type const = string * (((itype list * dict list list) *
147 (itype list (*types of arguments*) * itype (*body type*))) * bool (*requires type annotation*))
151 | IVar of vname option
152 | `$ of iterm * iterm
153 | `|=> of (vname option * itype) * iterm
154 | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
155 (*see also signature*)
157 fun is_IVar (IVar _) = true
160 fun is_IAbs (_ `|=> _) = true
163 val op `$$ = Library.foldl (op `$);
164 val op `|==> = Library.foldr (op `|=>);
166 val unfold_app = unfoldl
167 (fn op `$ t => SOME t
170 val unfold_abs = unfoldr
171 (fn op `|=> t => SOME t
175 (fn ICase (((td, ty), [(p, t)]), _) => SOME (((p, ty), td), t)
178 val unfold_let = unfoldr split_let;
180 fun unfold_const_app t =
182 of (IConst c, ts) => SOME (c, ts)
185 fun fold_constexprs f =
187 fun fold' (IConst c) = f c
189 | fold' (t1 `$ t2) = fold' t1 #> fold' t2
190 | fold' (_ `|=> t) = fold' t
191 | fold' (ICase (((t, _), ds), _)) = fold' t
192 #> fold (fn (pat, body) => fold' pat #> fold' body) ds
195 val add_constnames = fold_constexprs (fn (c, _) => insert (op =) c);
197 fun add_tycos (tyco `%% tys) = insert (op =) tyco #> fold add_tycos tys
198 | add_tycos (ITyVar _) = I;
200 val add_tyconames = fold_constexprs (fn (_, (((tys, _), _), _)) => fold add_tycos tys);
202 fun fold_varnames f =
206 fun fold_term _ (IConst _) = I
207 | fold_term vs (IVar (SOME v)) = if member (op =) vs v then I else f v
208 | fold_term _ (IVar NONE) = I
209 | fold_term vs (t1 `$ t2) = fold_term vs t1 #> fold_term vs t2
210 | fold_term vs ((SOME v, _) `|=> t) = fold_term (insert (op =) v vs) t
211 | fold_term vs ((NONE, _) `|=> t) = fold_term vs t
212 | fold_term vs (ICase (((t, _), ds), _)) = fold_term vs t #> fold (fold_case vs) ds
213 and fold_case vs (p, t) = fold_term (add p vs) t;
215 fun add t = fold_aux add (insert (op =)) t;
216 in fold_aux add f end;
218 fun exists_var t v = fold_varnames (fn w => fn b => v = w orelse b) t false;
220 fun split_pat_abs ((NONE, ty) `|=> t) = SOME ((IVar NONE, ty), t)
221 | split_pat_abs ((SOME v, ty) `|=> t) = SOME (case t
222 of ICase (((IVar (SOME w), _), [(p, t')]), _) =>
223 if v = w andalso (exists_var p v orelse not (exists_var t' v))
225 else ((IVar (SOME v), ty), t)
226 | _ => ((IVar (SOME v), ty), t))
227 | split_pat_abs _ = NONE;
229 val unfold_pat_abs = unfoldr split_pat_abs;
231 fun unfold_abs_eta [] t = ([], t)
232 | unfold_abs_eta (_ :: tys) (v_ty `|=> t) =
234 val (vs_tys, t') = unfold_abs_eta tys t;
235 in (v_ty :: vs_tys, t') end
236 | unfold_abs_eta tys t =
238 val ctxt = fold_varnames Name.declare t Name.context;
239 val vs_tys = (map o apfst) SOME (Name.invent_names ctxt "a" tys);
240 in (vs_tys, t `$$ map (IVar o fst) vs_tys) end;
242 fun eta_expand k (c as (name, ((_, (tys, _)), _)), ts) =
246 val _ = if l > length tys
247 then error ("Impossible eta-expansion for constant " ^ quote name) else ();
248 val ctxt = (fold o fold_varnames) Name.declare ts Name.context;
249 val vs_tys = (map o apfst) SOME
250 (Name.invent_names ctxt "a" ((take l o drop j) tys));
251 in vs_tys `|==> IConst c `$$ ts @ map (IVar o fst) vs_tys end;
253 fun contains_dict_var t =
255 fun cont_dict (Dict (_, d)) = cont_plain_dict d
256 and cont_plain_dict (Dict_Const (_, dss)) = (exists o exists) cont_dict dss
257 | cont_plain_dict (Dict_Var _) = true;
258 fun cont_term (IConst (_, (((_, dss), _), _))) = (exists o exists) cont_dict dss
259 | cont_term (IVar _) = false
260 | cont_term (t1 `$ t2) = cont_term t1 orelse cont_term t2
261 | cont_term (_ `|=> t) = cont_term t
262 | cont_term (ICase (_, t)) = cont_term t;
271 fun thyname_of_class thy = #theory_name o Name_Space.the_entry (Sign.class_space thy);
272 fun thyname_of_instance thy inst = case AxClass.thynames_of_arity thy inst
273 of [] => error ("No such instance: " ^ quote (snd inst ^ " :: " ^ fst inst))
274 | thyname :: _ => thyname;
275 fun thyname_of_const thy c = case AxClass.class_of_param thy c
276 of SOME class => thyname_of_class thy class
277 | NONE => (case Code.get_type_of_constr_or_abstr thy c
278 of SOME (tyco, _) => Codegen.thyname_of_type thy tyco
279 | NONE => Codegen.thyname_of_const thy c);
280 fun purify_base "==>" = "follows"
281 | purify_base "==" = "meta_eq"
282 | purify_base s = Name.desymbolize false s;
283 fun namify thy get_basename get_thyname name =
285 val prefix = get_thyname thy name;
286 val base = (purify_base o get_basename) name;
287 in Long_Name.append prefix base end;
290 fun namify_class thy = namify thy Long_Name.base_name thyname_of_class;
291 fun namify_classrel thy = namify thy (fn (sub_class, super_class) =>
292 Long_Name.base_name super_class ^ "_" ^ Long_Name.base_name sub_class)
293 (fn thy => thyname_of_class thy o fst);
294 (*order fits nicely with composed projections*)
295 fun namify_tyco thy "fun" = "Pure.fun"
296 | namify_tyco thy tyco = namify thy Long_Name.base_name Codegen.thyname_of_type tyco;
297 fun namify_instance thy = namify thy (fn (class, tyco) =>
298 Long_Name.base_name class ^ "_" ^ Long_Name.base_name tyco) thyname_of_instance;
299 fun namify_const thy = namify thy Long_Name.base_name thyname_of_const;
306 datatype naming = Naming of {
307 class: class Symtab.table * Name.context,
308 classrel: string Symreltab.table * Name.context,
309 tyco: string Symtab.table * Name.context,
310 instance: string Symreltab.table * Name.context,
311 const: string Symtab.table * Name.context
314 fun dest_Naming (Naming naming) = naming;
316 val empty_naming = Naming {
317 class = (Symtab.empty, Name.context),
318 classrel = (Symreltab.empty, Name.context),
319 tyco = (Symtab.empty, Name.context),
320 instance = (Symreltab.empty, Name.context),
321 const = (Symtab.empty, Name.context)
325 fun mk_naming (class, classrel, tyco, instance, const) =
326 Naming { class = class, classrel = classrel,
327 tyco = tyco, instance = instance, const = const };
328 fun map_naming f (Naming { class, classrel, tyco, instance, const }) =
329 mk_naming (f (class, classrel, tyco, instance, const));
331 fun map_class f = map_naming
332 (fn (class, classrel, tyco, inst, const) =>
333 (f class, classrel, tyco, inst, const));
334 fun map_classrel f = map_naming
335 (fn (class, classrel, tyco, inst, const) =>
336 (class, f classrel, tyco, inst, const));
337 fun map_tyco f = map_naming
338 (fn (class, classrel, tyco, inst, const) =>
339 (class, classrel, f tyco, inst, const));
340 fun map_instance f = map_naming
341 (fn (class, classrel, tyco, inst, const) =>
342 (class, classrel, tyco, f inst, const));
343 fun map_const f = map_naming
344 (fn (class, classrel, tyco, inst, const) =>
345 (class, classrel, tyco, inst, f const));
348 fun add_variant update (thing, name) (tab, used) =
350 val (name', used') = Name.variant name used;
351 val tab' = update (thing, name') tab;
352 in (tab', used') end;
354 fun declare thy mapp lookup update namify thing =
355 mapp (add_variant update (thing, namify thy thing))
356 #> `(fn naming => the (lookup naming thing));
359 (* lookup and declare *)
363 val suffix_class = "class";
364 val suffix_classrel = "classrel"
365 val suffix_tyco = "tyco";
366 val suffix_instance = "inst";
367 val suffix_const = "const";
369 fun add_suffix nsp NONE = NONE
370 | add_suffix nsp (SOME name) = SOME (Long_Name.append name nsp);
374 val lookup_class = add_suffix suffix_class
375 oo Symtab.lookup o fst o #class o dest_Naming;
376 val lookup_classrel = add_suffix suffix_classrel
377 oo Symreltab.lookup o fst o #classrel o dest_Naming;
378 val lookup_tyco = add_suffix suffix_tyco
379 oo Symtab.lookup o fst o #tyco o dest_Naming;
380 val lookup_instance = add_suffix suffix_instance
381 oo Symreltab.lookup o fst o #instance o dest_Naming;
382 val lookup_const = add_suffix suffix_const
383 oo Symtab.lookup o fst o #const o dest_Naming;
385 fun declare_class thy = declare thy map_class
386 lookup_class Symtab.update_new namify_class;
387 fun declare_classrel thy = declare thy map_classrel
388 lookup_classrel Symreltab.update_new namify_classrel;
389 fun declare_tyco thy = declare thy map_tyco
390 lookup_tyco Symtab.update_new namify_tyco;
391 fun declare_instance thy = declare thy map_instance
392 lookup_instance Symreltab.update_new namify_instance;
393 fun declare_const thy = declare thy map_const
394 lookup_const Symtab.update_new namify_const;
396 fun ensure_declared_const thy const naming =
397 case lookup_const naming const
398 of SOME const' => (const', naming)
399 | NONE => declare_const thy const naming;
401 val fun_tyco = Long_Name.append (namify_tyco Pure.thy "fun") suffix_tyco
402 (*depends on add_suffix*);
404 val unfold_fun = unfoldr
405 (fn tyco `%% [ty1, ty2] => if tyco = fun_tyco then SOME (ty1, ty2) else NONE
408 fun unfold_fun_n n ty =
410 val (tys1, ty1) = unfold_fun ty;
411 val (tys3, tys2) = chop n tys1;
412 val ty3 = Library.foldr (fn (ty1, ty2) => fun_tyco `%% [ty1, ty2]) (tys2, ty1);
418 (** statements, abstract programs **)
420 type typscheme = (vname * sort) list * itype;
423 | Fun of string * ((typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option)
424 | Datatype of string * ((vname * sort) list * ((string * vname list) * itype list) list)
425 | Datatypecons of string * string
426 | Class of class * (vname * ((class * string) list * (string * itype) list))
427 | Classrel of class * class
428 | Classparam of string * class
429 | Classinst of (class * (string * (vname * sort) list))
430 * ((class * (string * (string * dict list list))) list
431 * (((string * const) * (thm * bool)) list
432 * ((string * const) * (thm * bool)) list))
433 (*see also signature*);
435 type program = stmt Graph.T;
437 fun empty_funs program =
438 Graph.fold (fn (name, (Fun (c, ((_, []), _)), _)) => cons c
439 | _ => I) program [];
441 fun map_terms_bottom_up f (t as IConst _) = f t
442 | map_terms_bottom_up f (t as IVar _) = f t
443 | map_terms_bottom_up f (t1 `$ t2) = f
444 (map_terms_bottom_up f t1 `$ map_terms_bottom_up f t2)
445 | map_terms_bottom_up f ((v, ty) `|=> t) = f
446 ((v, ty) `|=> map_terms_bottom_up f t)
447 | map_terms_bottom_up f (ICase (((t, ty), ps), t0)) = f
448 (ICase (((map_terms_bottom_up f t, ty), (map o pairself)
449 (map_terms_bottom_up f) ps), map_terms_bottom_up f t0));
451 fun map_classparam_instances_as_term f =
452 (map o apfst o apsnd) (fn const => case f (IConst const) of IConst const' => const')
454 fun map_terms_stmt f NoStmt = NoStmt
455 | map_terms_stmt f (Fun (c, ((tysm, eqs), case_cong))) = Fun (c, ((tysm, (map o apfst)
456 (fn (ts, t) => (map f ts, f t)) eqs), case_cong))
457 | map_terms_stmt f (stmt as Datatype _) = stmt
458 | map_terms_stmt f (stmt as Datatypecons _) = stmt
459 | map_terms_stmt f (stmt as Class _) = stmt
460 | map_terms_stmt f (stmt as Classrel _) = stmt
461 | map_terms_stmt f (stmt as Classparam _) = stmt
462 | map_terms_stmt f (Classinst (arity, (super_instances, classparam_instances))) =
463 Classinst (arity, (super_instances, (pairself o map_classparam_instances_as_term) f classparam_instances));
465 fun is_cons program name = case Graph.get_node program name
466 of Datatypecons _ => true
469 fun is_case (Fun (_, (_, SOME _))) = true
472 fun lookup_classparam_instance program name = program |> Graph.get_first
473 (fn (_, (Classinst ((class, _), (_, (param_insts, _))), _)) =>
474 Option.map (fn ((const, _), _) => (class, const))
475 (find_first (fn ((_, (inst_const, _)), _) => inst_const = name) param_insts) | _ => NONE)
477 fun labelled_name thy program name =
478 let val ctxt = Proof_Context.init_global thy in
479 case Graph.get_node program name of
480 Fun (c, _) => quote (Code.string_of_const thy c)
481 | Datatype (tyco, _) => "type " ^ quote (Proof_Context.extern_type ctxt tyco)
482 | Datatypecons (c, _) => quote (Code.string_of_const thy c)
483 | Class (class, _) => "class " ^ quote (Proof_Context.extern_class ctxt class)
484 | Classrel (sub, super) =>
486 val Class (sub, _) = Graph.get_node program sub;
487 val Class (super, _) = Graph.get_node program super;
489 quote (Proof_Context.extern_class ctxt sub ^ " < " ^ Proof_Context.extern_class ctxt super)
491 | Classparam (c, _) => quote (Code.string_of_const thy c)
492 | Classinst ((class, (tyco, _)), _) =>
494 val Class (class, _) = Graph.get_node program class;
495 val Datatype (tyco, _) = Graph.get_node program tyco;
497 quote (Proof_Context.extern_type ctxt tyco ^ " :: " ^ Proof_Context.extern_class ctxt class)
501 fun linear_stmts program =
502 rev (Graph.strong_conn program)
503 |> map (AList.make (Graph.get_node program));
505 fun group_stmts thy program =
507 fun is_fun (_, Fun _) = true | is_fun _ = false;
508 fun is_datatypecons (_, Datatypecons _) = true | is_datatypecons _ = false;
509 fun is_datatype (_, Datatype _) = true | is_datatype _ = false;
510 fun is_class (_, Class _) = true | is_class _ = false;
511 fun is_classrel (_, Classrel _) = true | is_classrel _ = false;
512 fun is_classparam (_, Classparam _) = true | is_classparam _ = false;
513 fun is_classinst (_, Classinst _) = true | is_classinst _ = false;
515 if forall (is_datatypecons orf is_datatype) stmts
516 then (filter is_datatype stmts, [], ([], []))
517 else if forall (is_class orf is_classrel orf is_classparam) stmts
518 then ([], filter is_class stmts, ([], []))
519 else if forall (is_fun orf is_classinst) stmts
520 then ([], [], List.partition is_fun stmts)
521 else error ("Illegal mutual dependencies: " ^
522 (commas o map (labelled_name thy program o fst)) stmts)
529 (** translation kernel **)
531 (* generic mechanisms *)
533 fun ensure_stmt lookup declare generate thing (dep, (naming, program)) =
535 fun add_dep name = case dep of NONE => I
536 | SOME dep => Graph.add_edge (dep, name);
537 val (name, naming') = case lookup naming thing
538 of SOME name => (name, naming)
539 | NONE => declare thing naming;
540 in case try (Graph.get_node program) name
541 of SOME stmt => program
547 |> Graph.default_node (name, NoStmt)
550 |> curry generate (SOME name)
552 |-> (fn stmt => (apsnd o Graph.map_node name) (K stmt))
557 exception PERMISSIVE of unit;
559 fun translation_error thy permissive some_thm msg sub_msg =
561 then raise PERMISSIVE ()
566 SOME thm => "\n(in code equation " ^ Display.string_of_thm_global thy thm ^ ")"
568 in error (msg ^ err_thm ^ ":\n" ^ sub_msg) end;
570 fun not_wellsorted thy permissive some_thm ty sort e =
572 val ctxt = Syntax.init_pretty_global thy;
573 val err_class = Sorts.class_error ctxt e;
575 "Type " ^ Syntax.string_of_typ ctxt ty ^ " not of sort " ^
576 Syntax.string_of_sort_global thy sort;
578 translation_error thy permissive some_thm "Wellsortedness error"
579 (err_typ ^ "\n" ^ err_class)
582 (* inference of type annotations for disambiguation with type classes *)
584 fun annotate_term (Const (c', T'), Const (c, T)) tvar_names =
586 val tvar_names' = Term.add_tvar_namesT T' tvar_names
588 (Const (c, if eq_set (op =) (tvar_names, tvar_names') then T else Type("", [T])), tvar_names')
590 | annotate_term (t1 $ u1, t $ u) tvar_names =
592 val (u', tvar_names') = annotate_term (u1, u) tvar_names
593 val (t', tvar_names'') = annotate_term (t1, t) tvar_names'
595 (t' $ u', tvar_names'')
597 | annotate_term (Abs (_, _, t1) , Abs (x, T, t)) tvar_names =
598 apfst (fn t => Abs (x, T, t)) (annotate_term (t1, t) tvar_names)
599 | annotate_term (_, t) tvar_names = (t, tvar_names)
601 fun annotate_eqns thy (c, ty) eqns =
603 val ctxt = ProofContext.init_global thy |> Config.put Type_Infer_Context.const_sorts false
604 val erase = map_types (fn _ => Type_Infer.anyT [])
605 val reinfer = singleton (Type_Infer_Context.infer_types ctxt)
606 fun add_annotations (args, (rhs, some_abs)) =
608 val lhs = list_comb (Const (c, ty), map (map_types Type.strip_sorts o fst) args)
609 val reinferred_rhs = snd (Logic.dest_equals (reinfer (Logic.mk_equals (lhs, erase rhs))))
610 val (rhs', _) = annotate_term (reinferred_rhs, rhs) []
612 (args, (rhs', some_abs))
615 map (apfst add_annotations) eqns
620 fun ensure_tyco thy algbr eqngr permissive tyco =
622 val ((vs, cos), _) = Code.get_type thy tyco;
624 fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs
625 ##>> fold_map (fn (c, (vs, tys)) =>
626 ensure_const thy algbr eqngr permissive c
627 ##>> pair (map (unprefix "'" o fst) vs)
628 ##>> fold_map (translate_typ thy algbr eqngr permissive) tys) cos
629 #>> (fn info => Datatype (tyco, info));
630 in ensure_stmt lookup_tyco (declare_tyco thy) stmt_datatype tyco end
631 and ensure_const thy algbr eqngr permissive c =
633 fun stmt_datatypecons tyco =
634 ensure_tyco thy algbr eqngr permissive tyco
635 #>> (fn tyco => Datatypecons (c, tyco));
636 fun stmt_classparam class =
637 ensure_class thy algbr eqngr permissive class
638 #>> (fn class => Classparam (c, class));
641 val ((vs, ty), eqns) = Code.equations_of_cert thy cert;
642 val eqns' = annotate_eqns thy (c, ty) eqns
643 val some_case_cong = Code.get_case_cong thy c;
645 fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs
646 ##>> translate_typ thy algbr eqngr permissive ty
647 ##>> translate_eqns thy algbr eqngr permissive eqns'
648 #>> (fn info => Fun (c, (info, some_case_cong)))
650 val stmt_const = case Code.get_type_of_constr_or_abstr thy c
651 of SOME (tyco, _) => stmt_datatypecons tyco
652 | NONE => (case AxClass.class_of_param thy c
653 of SOME class => stmt_classparam class
654 | NONE => stmt_fun (Code_Preproc.cert eqngr c))
655 in ensure_stmt lookup_const (declare_const thy) stmt_const c end
656 and ensure_class thy (algbr as (_, algebra)) eqngr permissive class =
658 val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
659 val cs = #params (AxClass.get_info thy class);
661 fold_map (fn super_class => ensure_class thy algbr eqngr permissive super_class
662 ##>> ensure_classrel thy algbr eqngr permissive (class, super_class)) super_classes
663 ##>> fold_map (fn (c, ty) => ensure_const thy algbr eqngr permissive c
664 ##>> translate_typ thy algbr eqngr permissive ty) cs
665 #>> (fn info => Class (class, (unprefix "'" Name.aT, info)))
666 in ensure_stmt lookup_class (declare_class thy) stmt_class class end
667 and ensure_classrel thy algbr eqngr permissive (sub_class, super_class) =
670 ensure_class thy algbr eqngr permissive sub_class
671 ##>> ensure_class thy algbr eqngr permissive super_class
673 in ensure_stmt lookup_classrel (declare_classrel thy) stmt_classrel (sub_class, super_class) end
674 and ensure_inst thy (algbr as (_, algebra)) eqngr permissive (class, tyco) =
676 val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
677 val these_classparams = these o try (#params o AxClass.get_info thy);
678 val classparams = these_classparams class;
679 val further_classparams = maps these_classparams
680 ((Sorts.complete_sort algebra o Sorts.super_classes algebra) class);
681 val vs = Name.invent_names Name.context "'a" (Sorts.mg_domain algebra tyco [class]);
682 val sorts' = Sorts.mg_domain (Sign.classes_of thy) tyco [class];
683 val vs' = map2 (fn (v, sort1) => fn sort2 => (v,
684 Sorts.inter_sort (Sign.classes_of thy) (sort1, sort2))) vs sorts';
685 val arity_typ = Type (tyco, map TFree vs);
686 val arity_typ' = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) vs');
687 fun translate_super_instance super_class =
688 ensure_class thy algbr eqngr permissive super_class
689 ##>> ensure_classrel thy algbr eqngr permissive (class, super_class)
690 ##>> translate_dicts thy algbr eqngr permissive NONE (arity_typ, [super_class])
691 #>> (fn ((super_class, classrel), [Dict ([], Dict_Const (inst, dss))]) =>
692 (super_class, (classrel, (inst, dss))));
693 fun translate_classparam_instance (c, ty) =
695 val raw_const = Const (c, map_type_tfree (K arity_typ') ty);
696 val thm = AxClass.unoverload_conv thy (Thm.cterm_of thy raw_const);
697 val const = (apsnd Logic.unvarifyT_global o dest_Const o snd
698 o Logic.dest_equals o Thm.prop_of) thm;
700 ensure_const thy algbr eqngr permissive c
701 ##>> translate_const thy algbr eqngr permissive (SOME thm) (const, NONE)
702 #>> (fn (c, IConst const') => ((c, const'), (thm, true)))
705 ensure_class thy algbr eqngr permissive class
706 ##>> ensure_tyco thy algbr eqngr permissive tyco
707 ##>> fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs
708 ##>> fold_map translate_super_instance super_classes
709 ##>> fold_map translate_classparam_instance classparams
710 ##>> fold_map translate_classparam_instance further_classparams
711 #>> (fn (((((class, tyco), arity_args), super_instances),
712 classparam_instances), further_classparam_instances) =>
713 Classinst ((class, (tyco, arity_args)), (super_instances,
714 (classparam_instances, further_classparam_instances))));
715 in ensure_stmt lookup_instance (declare_instance thy) stmt_inst (class, tyco) end
716 and translate_typ thy algbr eqngr permissive (TFree (v, _)) =
717 pair (ITyVar (unprefix "'" v))
718 | translate_typ thy algbr eqngr permissive (Type (tyco, tys)) =
719 ensure_tyco thy algbr eqngr permissive tyco
720 ##>> fold_map (translate_typ thy algbr eqngr permissive) tys
721 #>> (fn (tyco, tys) => tyco `%% tys)
722 and translate_term thy algbr eqngr permissive some_thm (Const (c, ty), some_abs) =
723 translate_app thy algbr eqngr permissive some_thm (((c, ty), []), some_abs)
724 | translate_term thy algbr eqngr permissive some_thm (Free (v, _), some_abs) =
726 | translate_term thy algbr eqngr permissive some_thm (Abs (v, ty, t), some_abs) =
728 val (v', t') = Syntax_Trans.variant_abs (Name.desymbolize false v, ty, t);
729 val v'' = if member (op =) (Term.add_free_names t' []) v'
730 then SOME v' else NONE
732 translate_typ thy algbr eqngr permissive ty
733 ##>> translate_term thy algbr eqngr permissive some_thm (t', some_abs)
734 #>> (fn (ty, t) => (v'', ty) `|=> t)
736 | translate_term thy algbr eqngr permissive some_thm (t as _ $ _, some_abs) =
738 of (Const (c, ty), ts) =>
739 translate_app thy algbr eqngr permissive some_thm (((c, ty), ts), some_abs)
741 translate_term thy algbr eqngr permissive some_thm (t', some_abs)
742 ##>> fold_map (translate_term thy algbr eqngr permissive some_thm o rpair NONE) ts
743 #>> (fn (t, ts) => t `$$ ts)
744 and translate_eqn thy algbr eqngr permissive ((args, (rhs, some_abs)), (some_thm, proper)) =
745 fold_map (translate_term thy algbr eqngr permissive some_thm) args
746 ##>> translate_term thy algbr eqngr permissive some_thm (rhs, some_abs)
747 #>> rpair (some_thm, proper)
748 and translate_eqns thy algbr eqngr permissive eqns prgrm =
749 prgrm |> fold_map (translate_eqn thy algbr eqngr permissive) eqns
750 handle PERMISSIVE () => ([], prgrm)
751 and translate_const thy algbr eqngr permissive some_thm ((c, ty), some_abs) =
753 val _ = if (case some_abs of NONE => true | SOME abs => not (c = abs))
754 andalso Code.is_abstr thy c
755 then translation_error thy permissive some_thm
756 "Abstraction violation" ("constant " ^ Code.string_of_const thy c)
758 val (annotate, ty') = (case ty of Type("", [ty']) => (true, ty') | ty' => (false, ty'))
759 val arg_typs = Sign.const_typargs thy (c, ty');
760 val sorts = Code_Preproc.sortargs eqngr c;
761 val (function_typs, body_typ) = Term.strip_type ty';
763 ensure_const thy algbr eqngr permissive c
764 ##>> fold_map (translate_typ thy algbr eqngr permissive) arg_typs
765 ##>> fold_map (translate_dicts thy algbr eqngr permissive some_thm) (arg_typs ~~ sorts)
766 ##>> fold_map (translate_typ thy algbr eqngr permissive) (body_typ :: function_typs)
767 #>> (fn (((c, arg_typs), dss), body_typ :: function_typs) =>
768 IConst (c, (((arg_typs, dss), (function_typs, body_typ)), annotate)))
770 and translate_app_const thy algbr eqngr permissive some_thm ((c_ty, ts), some_abs) =
771 translate_const thy algbr eqngr permissive some_thm (c_ty, some_abs)
772 ##>> fold_map (translate_term thy algbr eqngr permissive some_thm o rpair NONE) ts
773 #>> (fn (t, ts) => t `$$ ts)
774 and translate_case thy algbr eqngr permissive some_thm (num_args, (t_pos, case_pats)) (c_ty, ts) =
776 fun arg_types num_args ty = fst (chop num_args (binder_types ty));
777 val tys = arg_types num_args (snd c_ty);
778 val ty = nth tys t_pos;
779 fun mk_constr c t = let val n = Code.args_number thy c
780 in ((c, arg_types n (fastype_of t) ---> ty), n) end;
781 val constrs = if null case_pats then []
782 else map2 mk_constr case_pats (nth_drop t_pos ts);
783 fun casify naming constrs ty ts =
785 val undefineds = map_filter (lookup_const naming) (Code.undefineds thy);
786 fun collapse_clause vs_map ts body =
789 of IConst (c, _) => if member (op =) undefineds c
792 | ICase (((IVar (SOME v), _), subclauses), _) =>
793 if forall (fn (pat', body') => exists_var pat' v
794 orelse not (exists_var body' v)) subclauses
795 then case AList.lookup (op =) vs_map v
796 of SOME i => maps (fn (pat', body') =>
797 collapse_clause (AList.delete (op =) v vs_map)
798 (nth_map i (K pat') ts) body') subclauses
799 | NONE => [(ts, body)]
803 fun mk_clause mk tys t =
805 val (vs, body) = unfold_abs_eta tys t;
806 val vs_map = fold_index (fn (i, (SOME v, _)) => cons (v, i) | _ => I) vs [];
807 val ts = map (IVar o fst) vs;
808 in map mk (collapse_clause vs_map ts body) end;
809 val t = nth ts t_pos;
810 val ts_clause = nth_drop t_pos ts;
811 val clauses = if null case_pats
812 then mk_clause (fn ([t], body) => (t, body)) [ty] (the_single ts_clause)
813 else maps (fn ((constr as IConst (_, ((_, (tys, _)), _)), n), t) =>
814 mk_clause (fn (ts, body) => (constr `$$ ts, body)) (take n tys) t)
815 (constrs ~~ ts_clause);
816 in ((t, ty), clauses) end;
818 translate_const thy algbr eqngr permissive some_thm (c_ty, NONE)
819 ##>> fold_map (fn (constr, n) => translate_const thy algbr eqngr permissive some_thm (constr, NONE)
821 ##>> translate_typ thy algbr eqngr permissive ty
822 ##>> fold_map (translate_term thy algbr eqngr permissive some_thm o rpair NONE) ts
823 #-> (fn (((t, constrs), ty), ts) =>
824 `(fn (_, (naming, _)) => ICase (casify naming constrs ty ts, t `$$ ts)))
826 and translate_app_case thy algbr eqngr permissive some_thm (case_scheme as (num_args, _)) ((c, ty), ts) =
827 if length ts < num_args then
830 val tys = (take (num_args - k) o drop k o fst o strip_type) ty;
831 val ctxt = (fold o fold_aterms) Term.declare_term_frees ts Name.context;
832 val vs = Name.invent_names ctxt "a" tys;
834 fold_map (translate_typ thy algbr eqngr permissive) tys
835 ##>> translate_case thy algbr eqngr permissive some_thm case_scheme ((c, ty), ts @ map Free vs)
836 #>> (fn (tys, t) => map2 (fn (v, _) => pair (SOME v)) vs tys `|==> t)
838 else if length ts > num_args then
839 translate_case thy algbr eqngr permissive some_thm case_scheme ((c, ty), take num_args ts)
840 ##>> fold_map (translate_term thy algbr eqngr permissive some_thm o rpair NONE) (drop num_args ts)
841 #>> (fn (t, ts) => t `$$ ts)
843 translate_case thy algbr eqngr permissive some_thm case_scheme ((c, ty), ts)
844 and translate_app thy algbr eqngr permissive some_thm (c_ty_ts as ((c, _), _), some_abs) =
845 case Code.get_case_scheme thy c
846 of SOME case_scheme => translate_app_case thy algbr eqngr permissive some_thm case_scheme c_ty_ts
847 | NONE => translate_app_const thy algbr eqngr permissive some_thm (c_ty_ts, some_abs)
848 and translate_tyvar_sort thy (algbr as (proj_sort, _)) eqngr permissive (v, sort) =
849 fold_map (ensure_class thy algbr eqngr permissive) (proj_sort sort)
850 #>> (fn sort => (unprefix "'" v, sort))
851 and translate_dicts thy (algbr as (proj_sort, algebra)) eqngr permissive some_thm (ty, sort) =
853 datatype typarg_witness =
854 Weakening of (class * class) list * plain_typarg_witness
855 and plain_typarg_witness =
856 Global of (class * string) * typarg_witness list list
857 | Local of string * (int * sort);
858 fun class_relation ((Weakening (classrels, x)), sub_class) super_class =
859 Weakening ((sub_class, super_class) :: classrels, x);
860 fun type_constructor (tyco, _) dss class =
861 Weakening ([], Global ((class, tyco), (map o map) fst dss));
862 fun type_variable (TFree (v, sort)) =
864 val sort' = proj_sort sort;
865 in map_index (fn (n, class) => (Weakening ([], Local (v, (n, sort'))), class)) sort' end;
866 val typarg_witnesses = Sorts.of_sort_derivation algebra
867 {class_relation = K (Sorts.classrel_derivation algebra class_relation),
868 type_constructor = type_constructor,
869 type_variable = type_variable} (ty, proj_sort sort)
870 handle Sorts.CLASS_ERROR e => not_wellsorted thy permissive some_thm ty sort e;
871 fun mk_dict (Weakening (classrels, x)) =
872 fold_map (ensure_classrel thy algbr eqngr permissive) classrels
875 and mk_plain_dict (Global (inst, dss)) =
876 ensure_inst thy algbr eqngr permissive inst
877 ##>> (fold_map o fold_map) mk_dict dss
878 #>> (fn (inst, dss) => Dict_Const (inst, dss))
879 | mk_plain_dict (Local (v, (n, sort))) =
880 pair (Dict_Var (unprefix "'" v, (n, length sort)))
881 in fold_map mk_dict typarg_witnesses end;
886 structure Program = Code_Data
888 type T = naming * program;
889 val empty = (empty_naming, Graph.empty);
892 fun invoke_generation ignore_cache thy (algebra, eqngr) f name =
893 Program.change_yield (if ignore_cache then NONE else SOME thy)
894 (fn naming_program => (NONE, naming_program)
895 |> f thy algebra eqngr name
896 |-> (fn name => fn (_, naming_program) => (name, naming_program)));
899 (* program generation *)
901 fun consts_program thy permissive consts =
903 fun project_consts consts (naming, program) =
904 if permissive then (consts, (naming, program))
905 else (consts, (naming, Graph.subgraph
906 (member (op =) (Graph.all_succs program consts)) program));
907 fun generate_consts thy algebra eqngr =
908 fold_map (ensure_const thy algebra eqngr permissive);
910 invoke_generation permissive thy (Code_Preproc.obtain false thy consts [])
911 generate_consts consts
916 (* value evaluation *)
918 fun ensure_value thy algbr eqngr t =
920 val ty = fastype_of t;
921 val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
922 o dest_TFree))) t [];
924 fold_map (translate_tyvar_sort thy algbr eqngr false) vs
925 ##>> translate_typ thy algbr eqngr false ty
926 ##>> translate_term thy algbr eqngr false NONE (Code.subst_signatures thy t, NONE)
927 #>> (fn ((vs, ty), t) => Fun
928 (Term.dummy_patternN, (((vs, ty), [(([], t), (NONE, true))]), NONE)));
929 fun term_value (dep, (naming, program1)) =
931 val Fun (_, ((vs_ty, [(([], t), _)]), _)) =
932 Graph.get_node program1 Term.dummy_patternN;
933 val deps = Graph.immediate_succs program1 Term.dummy_patternN;
934 val program2 = Graph.del_nodes [Term.dummy_patternN] program1;
935 val deps_all = Graph.all_succs program2 deps;
936 val program3 = Graph.subgraph (member (op =) deps_all) program2;
937 in (((naming, program3), ((vs_ty, t), deps)), (dep, (naming, program2))) end;
939 ensure_stmt ((K o K) NONE) pair stmt_value Term.dummy_patternN
944 fun original_sorts vs =
945 map (fn (v, _) => (v, (the o AList.lookup (op =) vs o prefix "'") v));
947 fun dynamic_evaluator thy evaluator algebra eqngr vs t =
949 val (((naming, program), (((vs', ty'), t'), deps)), _) =
950 invoke_generation false thy (algebra, eqngr) ensure_value t;
951 in evaluator naming program ((original_sorts vs vs', (vs', ty')), t') deps end;
953 fun dynamic_conv thy evaluator =
954 Code_Preproc.dynamic_conv thy (dynamic_evaluator thy evaluator);
956 fun dynamic_value thy postproc evaluator =
957 Code_Preproc.dynamic_value thy postproc (dynamic_evaluator thy evaluator);
959 fun lift_evaluation thy evaluation' algebra eqngr naming program vs t =
961 val (((_, program'), (((vs', ty'), t'), deps)), _) =
962 ensure_value thy algebra eqngr t (NONE, (naming, program));
963 in evaluation' ((original_sorts vs vs', (vs', ty')), t') deps end;
965 fun lift_evaluator thy evaluator' consts algebra eqngr =
967 fun generate_consts thy algebra eqngr =
968 fold_map (ensure_const thy algebra eqngr false);
969 val (consts', (naming, program)) =
970 invoke_generation true thy (algebra, eqngr) generate_consts consts;
971 val evaluation' = evaluator' naming program consts';
972 in lift_evaluation thy evaluation' algebra eqngr naming program end;
974 fun lift_evaluator_simple thy evaluator' consts algebra eqngr =
976 fun generate_consts thy algebra eqngr =
977 fold_map (ensure_const thy algebra eqngr false);
978 val (consts', (naming, program)) =
979 invoke_generation true thy (algebra, eqngr) generate_consts consts;
980 in evaluator' program end;
982 fun static_conv thy consts conv =
983 Code_Preproc.static_conv thy consts (lift_evaluator thy conv consts);
985 fun static_conv_simple thy consts conv =
986 Code_Preproc.static_conv thy consts (lift_evaluator_simple thy conv consts);
988 fun static_value thy postproc consts evaluator =
989 Code_Preproc.static_value thy postproc consts (lift_evaluator thy evaluator consts);
992 (** diagnostic commands **)
994 fun read_const_exprs thy =
996 fun consts_of thy' = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
997 ((snd o #constants o Consts.dest o #consts o Sign.rep_sg) thy') [];
998 fun belongs_here thy' c = forall
999 (fn thy'' => not (Sign.declared_const thy'' c)) (Theory.parents_of thy');
1000 fun consts_of_select thy' = filter (belongs_here thy') (consts_of thy');
1001 fun read_const_expr "_" = ([], consts_of thy)
1002 | read_const_expr s = if String.isSuffix "._" s
1003 then ([], consts_of_select (Context.this_theory thy (unsuffix "._" s)))
1004 else ([Code.read_const thy s], []);
1005 in pairself flat o split_list o map read_const_expr end;
1007 fun code_depgr thy consts =
1009 val (_, eqngr) = Code_Preproc.obtain true thy consts [];
1010 val all_consts = Graph.all_succs eqngr consts;
1011 in Graph.subgraph (member (op =) all_consts) eqngr end;
1013 fun code_thms thy = Pretty.writeln o Code_Preproc.pretty thy o code_depgr thy;
1015 fun code_deps thy consts =
1017 val eqngr = code_depgr thy consts;
1018 val constss = Graph.strong_conn eqngr;
1019 val mapping = Symtab.empty |> fold (fn consts => fold (fn const =>
1020 Symtab.update (const, consts)) consts) constss;
1021 fun succs consts = consts
1022 |> maps (Graph.immediate_succs eqngr)
1023 |> subtract (op =) consts
1024 |> map (the o Symtab.lookup mapping)
1026 val conn = [] |> fold (fn consts => cons (consts, succs consts)) constss;
1027 fun namify consts = map (Code.string_of_const thy) consts
1029 val prgr = map (fn (consts, constss) =>
1030 { name = namify consts, ID = namify consts, dir = "", unfold = true,
1031 path = "", parents = map namify constss }) conn;
1032 in Present.display_graph prgr end;
1036 fun code_thms_cmd thy = code_thms thy o op @ o read_const_exprs thy;
1037 fun code_deps_cmd thy = code_deps thy o op @ o read_const_exprs thy;
1042 Outer_Syntax.improper_command "code_thms" "print system of code equations for code" Keyword.diag
1043 (Scan.repeat1 Parse.term_group
1044 >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
1045 o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of)));
1048 Outer_Syntax.improper_command "code_deps" "visualize dependencies of code equations for code"
1050 (Scan.repeat1 Parse.term_group
1051 >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
1052 o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));
1059 structure Basic_Code_Thingol: BASIC_CODE_THINGOL = Code_Thingol;