60 val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a; |
60 val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a; |
61 val fold_unbound_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a; |
61 val fold_unbound_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a; |
62 |
62 |
63 datatype stmt = |
63 datatype stmt = |
64 NoStmt |
64 NoStmt |
65 | Fun of typscheme * ((iterm list * iterm) * thm) list |
65 | Fun of typscheme * ((iterm list * iterm) * (thm * bool)) list |
66 | Datatype of (vname * sort) list * (string * itype list) list |
66 | Datatype of (vname * sort) list * (string * itype list) list |
67 | Datatypecons of string |
67 | Datatypecons of string |
68 | Class of vname * ((class * string) list * (string * itype) list) |
68 | Class of vname * ((class * string) list * (string * itype) list) |
69 | Classrel of class * class |
69 | Classrel of class * class |
70 | Classparam of class |
70 | Classparam of class |
71 | Classinst of (class * (string * (vname * sort) list)) |
71 | Classinst of (class * (string * (vname * sort) list)) |
72 * ((class * (string * (string * dict list list))) list |
72 * ((class * (string * (string * dict list list))) list |
73 * ((string * const) * thm) list); |
73 * ((string * const) * (thm * bool)) list); |
74 type program = stmt Graph.T; |
74 type program = stmt Graph.T; |
75 val empty_funs: program -> string list; |
75 val empty_funs: program -> string list; |
76 val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm; |
76 val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm; |
77 val map_terms_stmt: (iterm -> iterm) -> stmt -> stmt; |
77 val map_terms_stmt: (iterm -> iterm) -> stmt -> stmt; |
78 val transitivly_non_empty_funs: program -> string list -> string list; |
78 val transitivly_non_empty_funs: program -> string list -> string list; |
256 (** statements, abstract programs **) |
256 (** statements, abstract programs **) |
257 |
257 |
258 type typscheme = (vname * sort) list * itype; |
258 type typscheme = (vname * sort) list * itype; |
259 datatype stmt = |
259 datatype stmt = |
260 NoStmt |
260 NoStmt |
261 | Fun of typscheme * ((iterm list * iterm) * thm) list |
261 | Fun of typscheme * ((iterm list * iterm) * (thm * bool)) list |
262 | Datatype of (vname * sort) list * (string * itype list) list |
262 | Datatype of (vname * sort) list * (string * itype list) list |
263 | Datatypecons of string |
263 | Datatypecons of string |
264 | Class of vname * ((class * string) list * (string * itype) list) |
264 | Class of vname * ((class * string) list * (string * itype) list) |
265 | Classrel of class * class |
265 | Classrel of class * class |
266 | Classparam of class |
266 | Classparam of class |
267 | Classinst of (class * (string * (vname * sort) list)) |
267 | Classinst of (class * (string * (vname * sort) list)) |
268 * ((class * (string * (string * dict list list))) list |
268 * ((class * (string * (string * dict list list))) list |
269 * ((string * const) * thm) list); |
269 * ((string * const) * (thm * bool)) list); |
270 |
270 |
271 type program = stmt Graph.T; |
271 type program = stmt Graph.T; |
272 |
272 |
273 fun empty_funs program = |
273 fun empty_funs program = |
274 Graph.fold (fn (name, (Fun (_, []), _)) => cons name |
274 Graph.fold (fn (name, (Fun (_, []), _)) => cons name |
421 #>> (fn (inst, dss) => DictConst (inst, dss)) |
421 #>> (fn (inst, dss) => DictConst (inst, dss)) |
422 | mk_dict (Local (classrels, (v, (k, sort)))) = |
422 | mk_dict (Local (classrels, (v, (k, sort)))) = |
423 fold_map (ensure_classrel thy algbr funcgr) classrels |
423 fold_map (ensure_classrel thy algbr funcgr) classrels |
424 #>> (fn classrels => DictVar (classrels, (unprefix "'" v, (k, length sort)))) |
424 #>> (fn classrels => DictVar (classrels, (unprefix "'" v, (k, length sort)))) |
425 in fold_map mk_dict typargs end |
425 in fold_map mk_dict typargs end |
426 and exprgen_eq thy algbr funcgr thm = |
426 and exprgen_eq thy algbr funcgr (thm, linear) = |
427 let |
427 let |
428 val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals |
428 val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals |
429 o Logic.unvarify o prop_of) thm; |
429 o Logic.unvarify o prop_of) thm; |
430 in |
430 in |
431 fold_map (exprgen_term thy algbr funcgr (SOME thm)) args |
431 fold_map (exprgen_term thy algbr funcgr (SOME thm)) args |
432 ##>> exprgen_term thy algbr funcgr (SOME thm) rhs |
432 ##>> exprgen_term thy algbr funcgr (SOME thm) rhs |
433 #>> rpair thm |
433 #>> rpair (thm, linear) |
434 end |
434 end |
435 and ensure_inst thy (algbr as (_, algebra)) funcgr (class, tyco) = |
435 and ensure_inst thy (algbr as (_, algebra)) funcgr (class, tyco) = |
436 let |
436 let |
437 val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class; |
437 val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class; |
438 val classparams = these (try (#params o AxClass.get_info thy) class); |
438 val classparams = these (try (#params o AxClass.get_info thy) class); |
455 val c_ty = (apsnd Logic.unvarifyT o dest_Const o snd |
455 val c_ty = (apsnd Logic.unvarifyT o dest_Const o snd |
456 o Logic.dest_equals o Thm.prop_of) thm; |
456 o Logic.dest_equals o Thm.prop_of) thm; |
457 in |
457 in |
458 ensure_const thy algbr funcgr c |
458 ensure_const thy algbr funcgr c |
459 ##>> exprgen_const thy algbr funcgr (SOME thm) c_ty |
459 ##>> exprgen_const thy algbr funcgr (SOME thm) c_ty |
460 #>> (fn (c, IConst c_inst) => ((c, c_inst), thm)) |
460 #>> (fn (c, IConst c_inst) => ((c, c_inst), (thm, true))) |
461 end; |
461 end; |
462 val stmt_inst = |
462 val stmt_inst = |
463 ensure_class thy algbr funcgr class |
463 ensure_class thy algbr funcgr class |
464 ##>> ensure_tyco thy algbr funcgr tyco |
464 ##>> ensure_tyco thy algbr funcgr tyco |
465 ##>> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs |
465 ##>> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs |
483 val raw_thms = Code_Funcgr.funcs funcgr c; |
483 val raw_thms = Code_Funcgr.funcs funcgr c; |
484 val (vs, raw_ty) = Code_Funcgr.typ funcgr c; |
484 val (vs, raw_ty) = Code_Funcgr.typ funcgr c; |
485 val ty = Logic.unvarifyT raw_ty; |
485 val ty = Logic.unvarifyT raw_ty; |
486 val thms = if (null o Term.typ_tfrees) ty orelse (null o fst o strip_type) ty |
486 val thms = if (null o Term.typ_tfrees) ty orelse (null o fst o strip_type) ty |
487 then raw_thms |
487 then raw_thms |
488 else map (Code_Unit.expand_eta 1) raw_thms; |
488 else (map o apfst) (Code_Unit.expand_eta 1) raw_thms; |
489 in |
489 in |
490 trns |
490 trns |
491 |> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs |
491 |> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs |
492 ||>> exprgen_typ thy algbr funcgr ty |
492 ||>> exprgen_typ thy algbr funcgr ty |
493 ||>> fold_map (exprgen_eq thy algbr funcgr) thms |
493 ||>> fold_map (exprgen_eq thy algbr funcgr) thms |
640 o dest_TFree))) t []; |
640 o dest_TFree))) t []; |
641 val stmt_value = |
641 val stmt_value = |
642 fold_map (exprgen_tyvar_sort thy algbr funcgr) vs |
642 fold_map (exprgen_tyvar_sort thy algbr funcgr) vs |
643 ##>> exprgen_typ thy algbr funcgr ty |
643 ##>> exprgen_typ thy algbr funcgr ty |
644 ##>> exprgen_term thy algbr funcgr NONE t |
644 ##>> exprgen_term thy algbr funcgr NONE t |
645 #>> (fn ((vs, ty), t) => Fun ((vs, ty), [(([], t), Drule.dummy_thm)])); |
645 #>> (fn ((vs, ty), t) => Fun ((vs, ty), [(([], t), (Drule.dummy_thm, true))])); |
646 fun term_value (dep, program1) = |
646 fun term_value (dep, program1) = |
647 let |
647 let |
648 val Fun ((vs, ty), [(([], t), _)]) = |
648 val Fun ((vs, ty), [(([], t), _)]) = |
649 Graph.get_node program1 Code_Name.value_name; |
649 Graph.get_node program1 Code_Name.value_name; |
650 val deps = Graph.imm_succs program1 Code_Name.value_name; |
650 val deps = Graph.imm_succs program1 Code_Name.value_name; |