65 mk_bot : typ -> term, |
65 mk_bot : typ -> term, |
66 mk_single : term -> term, |
66 mk_single : term -> term, |
67 mk_bind : term * term -> term, |
67 mk_bind : term * term -> term, |
68 mk_sup : term * term -> term, |
68 mk_sup : term * term -> term, |
69 mk_if : term -> term, |
69 mk_if : term -> term, |
|
70 mk_iterate_upto : typ -> term * term * term -> term, |
70 mk_not : term -> term, |
71 mk_not : term -> term, |
71 mk_map : typ -> typ -> term -> term -> term |
72 mk_map : typ -> typ -> term -> term -> term |
72 }; |
73 }; |
73 val mk_predT : compilation_funs -> typ -> typ |
74 val mk_predT : compilation_funs -> typ -> typ |
74 val dest_predT : compilation_funs -> typ -> typ |
75 val dest_predT : compilation_funs -> typ -> typ |
75 val mk_bot : compilation_funs -> typ -> term |
76 val mk_bot : compilation_funs -> typ -> term |
76 val mk_single : compilation_funs -> term -> term |
77 val mk_single : compilation_funs -> term -> term |
77 val mk_bind : compilation_funs -> term * term -> term |
78 val mk_bind : compilation_funs -> term * term -> term |
78 val mk_sup : compilation_funs -> term * term -> term |
79 val mk_sup : compilation_funs -> term * term -> term |
79 val mk_if : compilation_funs -> term -> term |
80 val mk_if : compilation_funs -> term -> term |
|
81 val mk_iterate_upto : compilation_funs -> typ -> term * term * term -> term |
80 val mk_not : compilation_funs -> term -> term |
82 val mk_not : compilation_funs -> term -> term |
81 val mk_map : compilation_funs -> typ -> typ -> term -> term -> term |
83 val mk_map : compilation_funs -> typ -> typ -> term -> term -> term |
82 val funT_of : compilation_funs -> mode -> typ -> typ |
84 val funT_of : compilation_funs -> mode -> typ -> typ |
83 (* Different compilations *) |
85 (* Different compilations *) |
84 datatype compilation = Pred | Depth_Limited | Random | Depth_Limited_Random | DSeq | Annotated |
86 datatype compilation = Pred | Depth_Limited | Random | Depth_Limited_Random | DSeq | Annotated |
603 mk_bot : typ -> term, |
605 mk_bot : typ -> term, |
604 mk_single : term -> term, |
606 mk_single : term -> term, |
605 mk_bind : term * term -> term, |
607 mk_bind : term * term -> term, |
606 mk_sup : term * term -> term, |
608 mk_sup : term * term -> term, |
607 mk_if : term -> term, |
609 mk_if : term -> term, |
|
610 mk_iterate_upto : typ -> term * term * term -> term, |
608 mk_not : term -> term, |
611 mk_not : term -> term, |
609 mk_map : typ -> typ -> term -> term -> term |
612 mk_map : typ -> typ -> term -> term -> term |
610 }; |
613 }; |
611 |
614 |
612 fun mk_predT (CompilationFuns funs) = #mk_predT funs |
615 fun mk_predT (CompilationFuns funs) = #mk_predT funs |
614 fun mk_bot (CompilationFuns funs) = #mk_bot funs |
617 fun mk_bot (CompilationFuns funs) = #mk_bot funs |
615 fun mk_single (CompilationFuns funs) = #mk_single funs |
618 fun mk_single (CompilationFuns funs) = #mk_single funs |
616 fun mk_bind (CompilationFuns funs) = #mk_bind funs |
619 fun mk_bind (CompilationFuns funs) = #mk_bind funs |
617 fun mk_sup (CompilationFuns funs) = #mk_sup funs |
620 fun mk_sup (CompilationFuns funs) = #mk_sup funs |
618 fun mk_if (CompilationFuns funs) = #mk_if funs |
621 fun mk_if (CompilationFuns funs) = #mk_if funs |
|
622 fun mk_iterate_upto (CompilationFuns funs) = #mk_iterate_upto funs |
619 fun mk_not (CompilationFuns funs) = #mk_not funs |
623 fun mk_not (CompilationFuns funs) = #mk_not funs |
620 fun mk_map (CompilationFuns funs) = #mk_map funs |
624 fun mk_map (CompilationFuns funs) = #mk_map funs |
621 |
625 |
622 (** function types and names of different compilations **) |
626 (** function types and names of different compilations **) |
623 |
627 |