1 (* Title: Tools/code/code_thingol.ML
3 Author: Florian Haftmann, TU Muenchen
5 Intermediate language ("Thin-gol") representing executable code.
6 Representation and translation.
17 signature BASIC_CODE_THINGOL =
21 DictConst of string * dict list list
22 | DictVar of string list * (vname * (int * int));
24 `%% of string * itype list
26 type const = string * (dict list list * itype list (*types of arguments*))
31 | `|-> of (vname * itype) * iterm
32 | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
33 (*((term, type), [(selector pattern, body term )]), primitive term)*)
34 val `-> : itype * itype -> itype;
35 val `--> : itype list * itype -> itype;
36 val `$$ : iterm * iterm list -> iterm;
37 val `|--> : (vname * itype) list * iterm -> iterm;
38 type typscheme = (vname * sort) list * itype;
41 signature CODE_THINGOL =
43 include BASIC_CODE_THINGOL;
44 val unfoldl: ('a -> ('a * 'b) option) -> 'a -> 'a * 'b list;
45 val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a;
46 val unfold_fun: itype -> itype list * itype;
47 val unfold_app: iterm -> iterm * iterm list;
48 val split_abs: iterm -> (((vname * iterm option) * itype) * iterm) option;
49 val unfold_abs: iterm -> ((vname * iterm option) * itype) list * iterm;
50 val split_let: iterm -> (((iterm * itype) * iterm) * iterm) option;
51 val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm;
52 val unfold_const_app: iterm ->
53 ((string * (dict list list * itype list)) * iterm list) option;
54 val collapse_let: ((vname * itype) * iterm) * iterm
55 -> (iterm * itype) * (iterm * iterm) list;
56 val eta_expand: (string * (dict list list * itype list)) * iterm list -> int -> iterm;
57 val contains_dictvar: iterm -> bool;
58 val fold_constnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
59 val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
60 val fold_unbound_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
64 | Fun of typscheme * ((iterm list * iterm) * thm) list
65 | Datatype of (vname * sort) list * (string * itype list) list
66 | Datatypecons of string
67 | Class of vname * ((class * string) list * (string * itype) list)
68 | Classrel of class * class
70 | Classinst of (class * (string * (vname * sort) list))
71 * ((class * (string * (string * dict list list))) list
72 * ((string * const) * thm) list);
73 type code = stmt Graph.T;
75 val merge_code: code * code -> code;
76 val project_code: bool (*delete empty funs*)
77 -> string list (*hidden*) -> string list option (*selected*)
79 val empty_funs: code -> string list;
80 val is_cons: code -> string -> bool;
83 val ensure_const: theory -> ((sort -> sort) * Sorts.algebra) * Consts.T
84 -> CodeFuncgr.T -> string -> transact -> string * transact;
85 val ensure_value: theory -> ((sort -> sort) * Sorts.algebra) * Consts.T
86 -> CodeFuncgr.T -> term -> transact -> string * transact;
87 val add_value_stmt: iterm * itype -> code -> code;
88 val transact: (transact -> 'a * transact) -> code -> 'a * code;
91 structure CodeThingol: CODE_THINGOL =
100 let val (x', xs') = unfoldl dest x1 in (x', xs' @ [x2]) end;
106 let val (xs', x') = unfoldr dest x2 in (x1::xs', x') end;
109 (** language core - types, pattern, expressions **)
111 (* language representation *)
116 DictConst of string * dict list list
117 | DictVar of string list * (vname * (int * int));
120 `%% of string * itype list
123 type const = string * (dict list list * itype list (*types of arguments*))
128 | `$ of iterm * iterm
129 | `|-> of (vname * itype) * iterm
130 | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
131 (*see also signature*)
134 variable naming conventions
139 type constructor names tyco
141 const names (general) c (const)
143 class parameter names classparam
146 v, c, co, classparam also annotated with types etc.
155 instance (class, tyco) inst
158 fun ty1 `-> ty2 = "fun" `%% [ty1, ty2];
159 val op `--> = Library.foldr (op `->);
160 val op `$$ = Library.foldl (op `$);
161 val op `|--> = Library.foldr (op `|->);
163 val unfold_fun = unfoldr
164 (fn "fun" `%% [ty1, ty2] => SOME (ty1, ty2)
167 val unfold_app = unfoldl
168 (fn op `$ t => SOME t
172 (fn (v, ty) `|-> (t as ICase (((IVar w, _), [(p, t')]), _)) =>
173 if v = w then SOME (((v, SOME p), ty), t') else SOME (((v, NONE), ty), t)
174 | (v, ty) `|-> t => SOME (((v, NONE), ty), t)
177 val unfold_abs = unfoldr split_abs;
180 (fn ICase (((td, ty), [(p, t)]), _) => SOME (((p, ty), td), t)
183 val unfold_let = unfoldr split_let;
185 fun unfold_const_app t =
187 of (IConst c, ts) => SOME (c, ts)
190 fun fold_aiterms f (t as IConst _) = f t
191 | fold_aiterms f (t as IVar _) = f t
192 | fold_aiterms f (t1 `$ t2) = fold_aiterms f t1 #> fold_aiterms f t2
193 | fold_aiterms f (t as _ `|-> t') = f t #> fold_aiterms f t'
194 | fold_aiterms f (ICase (_, t)) = fold_aiterms f t;
196 fun fold_constnames f =
198 fun add (IConst (c, _)) = f c
200 in fold_aiterms add end;
202 fun fold_varnames f =
204 fun add (IVar v) = f v
205 | add ((v, _) `|-> _) = f v
207 in fold_aiterms add end;
209 fun fold_unbound_varnames f =
211 fun add _ (IConst _) = I
212 | add vs (IVar v) = if not (member (op =) vs v) then f v else I
213 | add vs (t1 `$ t2) = add vs t1 #> add vs t2
214 | add vs ((v, _) `|-> t) = add (insert (op =) v vs) t
215 | add vs (ICase (_, t)) = add vs t;
218 fun collapse_let (((v, ty), se), be as ICase (((IVar w, _), ds), _)) =
220 fun exists_v t = fold_unbound_varnames (fn w => fn b =>
221 b orelse v = w) t false;
222 in if v = w andalso forall (fn (t1, t2) =>
223 exists_v t1 orelse not (exists_v t2)) ds
225 else ((se, ty), [(IVar v, be)])
227 | collapse_let (((v, ty), se), be) =
228 ((se, ty), [(IVar v, be)])
230 fun eta_expand (c as (_, (_, tys)), ts) k =
234 val ctxt = (fold o fold_varnames) Name.declare ts Name.context;
235 val vs_tys = Name.names ctxt "a" ((curry Library.take l o curry Library.drop j) tys);
236 in vs_tys `|--> IConst c `$$ ts @ map (fn (v, _) => IVar v) vs_tys end;
238 fun contains_dictvar t =
240 fun contains (DictConst (_, dss)) = (fold o fold) contains dss
241 | contains (DictVar _) = K true;
244 (fn IConst (_, (dss, _)) => (fold o fold) contains dss | _ => I) t false
248 (** definitions, transactions **)
250 type typscheme = (vname * sort) list * itype;
253 | Fun of typscheme * ((iterm list * iterm) * thm) list
254 | Datatype of (vname * sort) list * (string * itype list) list
255 | Datatypecons of string
256 | Class of vname * ((class * string) list * (string * itype) list)
257 | Classrel of class * class
258 | Classparam of class
259 | Classinst of (class * (string * (vname * sort) list))
260 * ((class * (string * (string * dict list list))) list
261 * ((string * const) * thm) list);
263 type code = stmt Graph.T;
268 val empty_code = Graph.empty : code; (*read: "depends on"*)
270 fun ensure_bot name = Graph.default_node (name, Bot);
272 fun add_def_incr (name, Bot) code =
273 (case the_default Bot (try (Graph.get_node code) name)
274 of Bot => error "Attempted to add Bot to code"
276 | add_def_incr (name, def) code =
277 (case try (Graph.get_node code) name
278 of NONE => Graph.new_node (name, def) code
279 | SOME Bot => Graph.map_node name (K def) code
280 | SOME _ => error ("Tried to overwrite definition " ^ quote name));
282 fun add_dep (NONE, _) = I
283 | add_dep (SOME name1, name2) =
284 if name1 = name2 then I else Graph.add_edge (name1, name2);
286 val merge_code : code * code -> code = Graph.merge (K true);
288 fun project_code delete_empty_funs hidden raw_selected code =
290 fun is_empty_fun name = case Graph.get_node code name
291 of Fun (_, []) => true
293 val names = subtract (op =) hidden (Graph.keys code);
294 val deleted = Graph.all_preds code (filter is_empty_fun names);
295 val selected = case raw_selected
296 of NONE => names |> subtract (op =) deleted
298 |> delete_empty_funs ? subtract (op =) deleted
299 |> subtract (op =) hidden
300 |> Graph.all_succs code
301 |> delete_empty_funs ? subtract (op =) deleted
302 |> subtract (op =) hidden;
305 |> Graph.subgraph (member (op =) selected)
308 fun empty_funs code =
309 Graph.fold (fn (name, (Fun (_, []), _)) => cons name
312 fun is_cons code name = case Graph.get_node code name
313 of Datatypecons _ => true
317 (* transaction protocol *)
319 type transact = Graph.key option * code;
321 fun ensure_stmt stmtgen name (dep, code) =
325 #> add_dep (dep, name)
326 #> curry stmtgen (SOME name)
328 #-> (fn def => add_def_incr (name, def))
333 |> add_def (can (Graph.get_node code) name)
338 fun transact f code =
341 |-> (fn x => fn (_, code) => (x, code));
344 (* translation kernel *)
346 fun ensure_class thy (algbr as ((_, algebra), _)) funcgr class =
348 val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class;
349 val cs = #params (AxClass.get_info thy class);
350 val class' = CodeName.class thy class;
352 fold_map (fn superclass => ensure_class thy algbr funcgr superclass
353 ##>> ensure_classrel thy algbr funcgr (class, superclass)) superclasses
354 ##>> fold_map (fn (c, ty) => ensure_const thy algbr funcgr c
355 ##>> exprgen_typ thy algbr funcgr ty) cs
356 #>> (fn info => Class (unprefix "'" Name.aT, info))
358 ensure_stmt stmt_class class'
360 and ensure_classrel thy algbr funcgr (subclass, superclass) =
362 val classrel' = CodeName.classrel thy (subclass, superclass);
364 ensure_class thy algbr funcgr subclass
365 ##>> ensure_class thy algbr funcgr superclass
368 ensure_stmt stmt_classrel classrel'
370 and ensure_tyco thy algbr funcgr "fun" =
372 | ensure_tyco thy algbr funcgr tyco =
376 val (vs, cos) = Code.get_datatype thy tyco;
378 fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
379 ##>> fold_map (fn (c, tys) =>
380 ensure_const thy algbr funcgr c
381 ##>> fold_map (exprgen_typ thy algbr funcgr) tys) cos
384 val tyco' = CodeName.tyco thy tyco;
386 ensure_stmt stmt_datatype tyco'
388 and exprgen_tyvar_sort thy (algbr as ((proj_sort, _), _)) funcgr (v, sort) =
389 fold_map (ensure_class thy algbr funcgr) (proj_sort sort)
390 #>> (fn sort => (unprefix "'" v, sort))
391 and exprgen_typ thy algbr funcgr (TFree vs) =
392 exprgen_tyvar_sort thy algbr funcgr vs
393 #>> (fn (v, sort) => ITyVar v)
394 | exprgen_typ thy algbr funcgr (Type (tyco, tys)) =
395 ensure_tyco thy algbr funcgr tyco
396 ##>> fold_map (exprgen_typ thy algbr funcgr) tys
397 #>> (fn (tyco, tys) => tyco `%% tys)
398 and exprgen_dicts thy (algbr as ((proj_sort, algebra), consts)) funcgr (ty_ctxt, sort_decl) =
400 val pp = Sign.pp thy;
402 Global of (class * string) * typarg list list
403 | Local of (class * class) list * (string * (int * sort));
404 fun class_relation (Global ((_, tyco), yss), _) class =
405 Global ((class, tyco), yss)
406 | class_relation (Local (classrels, v), subclass) superclass =
407 Local ((subclass, superclass) :: classrels, v);
408 fun type_constructor tyco yss class =
409 Global ((class, tyco), (map o map) fst yss);
410 fun type_variable (TFree (v, sort)) =
412 val sort' = proj_sort sort;
413 in map_index (fn (n, class) => (Local ([], (v, (n, sort'))), class)) sort' end;
414 val typargs = Sorts.of_sort_derivation pp algebra
415 {class_relation = class_relation, type_constructor = type_constructor,
416 type_variable = type_variable}
417 (ty_ctxt, proj_sort sort_decl);
418 fun mk_dict (Global (inst, yss)) =
419 ensure_inst thy algbr funcgr inst
420 ##>> (fold_map o fold_map) mk_dict yss
421 #>> (fn (inst, dss) => DictConst (inst, dss))
422 | mk_dict (Local (classrels, (v, (k, sort)))) =
423 fold_map (ensure_classrel thy algbr funcgr) classrels
424 #>> (fn classrels => DictVar (classrels, (unprefix "'" v, (k, length sort))))
426 fold_map mk_dict typargs
428 and exprgen_dict_parms thy (algbr as (_, consts)) funcgr (c, ty_ctxt) =
430 val ty_decl = Consts.the_declaration consts c;
431 val (tys, tys_decl) = pairself (curry (Consts.typargs consts) c) (ty_ctxt, ty_decl);
432 val sorts = map (snd o dest_TVar) tys_decl;
434 fold_map (exprgen_dicts thy algbr funcgr) (tys ~~ sorts)
436 and exprgen_eq thy algbr funcgr thm =
438 val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals
439 o Logic.unvarify o prop_of) thm;
441 fold_map (exprgen_term thy algbr funcgr) args
442 ##>> exprgen_term thy algbr funcgr rhs
445 and ensure_inst thy (algbr as ((_, algebra), _)) funcgr (class, tyco) =
447 val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class;
448 val classparams = these (try (#params o AxClass.get_info thy) class);
449 val vs = Name.names Name.context "'a" (Sorts.mg_domain algebra tyco [class]);
450 val sorts' = Sorts.mg_domain (Sign.classes_of thy) tyco [class];
451 val vs' = map2 (fn (v, sort1) => fn sort2 => (v,
452 Sorts.inter_sort (Sign.classes_of thy) (sort1, sort2))) vs sorts';
453 val arity_typ = Type (tyco, map TFree vs);
454 val arity_typ' = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) vs');
455 fun exprgen_superarity superclass =
456 ensure_class thy algbr funcgr superclass
457 ##>> ensure_classrel thy algbr funcgr (class, superclass)
458 ##>> exprgen_dicts thy algbr funcgr (arity_typ, [superclass])
459 #>> (fn ((superclass, classrel), [DictConst (inst, dss)]) =>
460 (superclass, (classrel, (inst, dss))));
461 fun exprgen_classparam_inst (c, ty) =
463 val c_inst = Const (c, map_type_tfree (K arity_typ') ty);
464 val thm = Class.unoverload thy (Thm.cterm_of thy c_inst);
465 val c_ty = (apsnd Logic.unvarifyT o dest_Const o snd
466 o Logic.dest_equals o Thm.prop_of) thm;
468 ensure_const thy algbr funcgr c
469 ##>> exprgen_const thy algbr funcgr c_ty
470 #>> (fn (c, IConst c_inst) => ((c, c_inst), thm))
473 ensure_class thy algbr funcgr class
474 ##>> ensure_tyco thy algbr funcgr tyco
475 ##>> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
476 ##>> fold_map exprgen_superarity superclasses
477 ##>> fold_map exprgen_classparam_inst classparams
478 #>> (fn ((((class, tyco), arity), superarities), classparams) =>
479 Classinst ((class, (tyco, arity)), (superarities, classparams)));
480 val inst = CodeName.instance thy (class, tyco);
482 ensure_stmt stmt_inst inst
484 and ensure_const thy (algbr as (_, consts)) funcgr c =
486 val c' = CodeName.const thy c;
487 fun stmt_datatypecons tyco =
488 ensure_tyco thy algbr funcgr tyco
489 #>> K (Datatypecons c');
490 fun stmt_classparam class =
491 ensure_class thy algbr funcgr class
492 #>> K (Classparam c');
495 val raw_thms = CodeFuncgr.funcs funcgr c;
496 val ty = (Logic.unvarifyT o CodeFuncgr.typ funcgr) c;
497 val vs = (map dest_TFree o Consts.typargs consts) (c, ty);
498 val thms = if (null o Term.typ_tfrees) ty orelse (null o fst o strip_type) ty
500 else map (CodeUnit.expand_eta 1) raw_thms;
503 |> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
504 ||>> exprgen_typ thy algbr funcgr ty
505 ||>> fold_map (exprgen_eq thy algbr funcgr) thms
506 |>> (fn ((vs, ty), eqs) => Fun ((vs, ty), eqs))
508 val stmtgen = case Code.get_datatype_of_constr thy c
509 of SOME tyco => stmt_datatypecons tyco
510 | NONE => (case AxClass.class_of_param thy c
511 of SOME class => stmt_classparam class
514 ensure_stmt stmtgen c'
516 and exprgen_term thy algbr funcgr (Const (c, ty)) =
517 exprgen_app thy algbr funcgr ((c, ty), [])
518 | exprgen_term thy algbr funcgr (Free (v, _)) =
520 | exprgen_term thy algbr funcgr (Abs (abs as (_, ty, _))) =
522 val (v, t) = Syntax.variant_abs abs;
524 exprgen_typ thy algbr funcgr ty
525 ##>> exprgen_term thy algbr funcgr t
526 #>> (fn (ty, t) => (v, ty) `|-> t)
528 | exprgen_term thy algbr funcgr (t as _ $ _) =
530 of (Const (c, ty), ts) =>
531 exprgen_app thy algbr funcgr ((c, ty), ts)
533 exprgen_term thy algbr funcgr t'
534 ##>> fold_map (exprgen_term thy algbr funcgr) ts
535 #>> (fn (t, ts) => t `$$ ts)
536 and exprgen_const thy algbr funcgr (c, ty) =
537 ensure_const thy algbr funcgr c
538 ##>> exprgen_dict_parms thy algbr funcgr (c, ty)
539 ##>> fold_map (exprgen_typ thy algbr funcgr) ((fst o Term.strip_type) ty)
540 #>> (fn ((c, iss), tys) => IConst (c, (iss, tys)))
541 and exprgen_app_default thy algbr funcgr (c_ty, ts) =
542 exprgen_const thy algbr funcgr c_ty
543 ##>> fold_map (exprgen_term thy algbr funcgr) ts
544 #>> (fn (t, ts) => t `$$ ts)
545 and exprgen_case thy algbr funcgr n cases (app as ((c, ty), ts)) =
548 (chop (1 + (if null cases then 1 else length cases)) o fst o strip_type) ty;
551 fun is_undefined (Const (c, _)) = Code.is_undefined thy c
552 | is_undefined _ = false;
553 fun mk_case (co, n) t =
555 val (vs, body) = Term.strip_abs_eta n t;
556 val selector = list_comb (Const (co, map snd vs ---> dty), map Free vs);
557 in if is_undefined body then NONE else SOME (selector, body) end;
560 val ([v_ty], body) = Term.strip_abs_eta 1 (the_single (nth_drop n ts))
561 in [(Free v_ty, body)] end
562 | mk_ds cases = map_filter (uncurry mk_case)
563 (AList.make (CodeUnit.no_args thy) cases ~~ nth_drop n ts);
565 exprgen_term thy algbr funcgr dt
566 ##>> exprgen_typ thy algbr funcgr dty
567 ##>> fold_map (fn (pat, body) => exprgen_term thy algbr funcgr pat
568 ##>> exprgen_term thy algbr funcgr body) (mk_ds cases)
569 ##>> exprgen_app_default thy algbr funcgr app
570 #>> (fn (((dt, dty), ds), t0) => ICase (((dt, dty), ds), t0))
572 and exprgen_app thy algbr funcgr ((c, ty), ts) = case Code.get_case_data thy c
573 of SOME (n, cases) => let val i = 1 + (if null cases then 1 else length cases) in
574 if length ts < i then
577 val tys = (curry Library.take (i - k) o curry Library.drop k o fst o strip_type) ty;
578 val ctxt = (fold o fold_aterms)
579 (fn Free (v, _) => Name.declare v | _ => I) ts Name.context;
580 val vs = Name.names ctxt "a" tys;
582 fold_map (exprgen_typ thy algbr funcgr) tys
583 ##>> exprgen_case thy algbr funcgr n cases ((c, ty), ts @ map Free vs)
584 #>> (fn (tys, t) => map2 (fn (v, _) => pair v) vs tys `|--> t)
586 else if length ts > i then
587 exprgen_case thy algbr funcgr n cases ((c, ty), Library.take (i, ts))
588 ##>> fold_map (exprgen_term thy algbr funcgr) (Library.drop (i, ts))
589 #>> (fn (t, ts) => t `$$ ts)
591 exprgen_case thy algbr funcgr n cases ((c, ty), ts)
593 | NONE => exprgen_app_default thy algbr funcgr ((c, ty), ts);
595 fun ensure_value thy algbr funcgr t =
597 val ty = fastype_of t;
598 val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
599 o dest_TFree))) t [];
601 fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
602 ##>> exprgen_typ thy algbr funcgr ty
603 ##>> exprgen_term thy algbr funcgr t
604 #>> (fn ((vs, ty), t) => Fun ((vs, ty), [(([], t), Drule.dummy_thm)]));
606 ensure_stmt stmt_value CodeName.value_name
609 fun add_value_stmt (t, ty) code =
611 |> Graph.new_node (CodeName.value_name, Fun (([], ty), [(([], t), Drule.dummy_thm)]))
612 |> fold (curry Graph.add_edge CodeName.value_name) (Graph.keys code);
617 structure BasicCodeThingol: BASIC_CODE_THINGOL = CodeThingol;