equal
deleted
inserted
replaced
23 val is_draft: sg -> bool |
23 val is_draft: sg -> bool |
24 val const_type: sg -> string -> typ option |
24 val const_type: sg -> string -> typ option |
25 val classes: sg -> class list |
25 val classes: sg -> class list |
26 val subsort: sg -> sort * sort -> bool |
26 val subsort: sg -> sort * sort -> bool |
27 val norm_sort: sg -> sort -> sort |
27 val norm_sort: sg -> sort -> sort |
|
28 val nonempty_sort: sg -> (string * sort) list -> sort -> bool |
28 val print_sg: sg -> unit |
29 val print_sg: sg -> unit |
29 val pretty_sg: sg -> Pretty.T |
30 val pretty_sg: sg -> Pretty.T |
30 val pprint_sg: sg -> pprint_args -> unit |
31 val pprint_sg: sg -> pprint_args -> unit |
31 val pretty_term: sg -> term -> Pretty.T |
32 val pretty_term: sg -> term -> Pretty.T |
32 val pretty_typ: sg -> typ -> Pretty.T |
33 val pretty_typ: sg -> typ -> Pretty.T |
60 val add_trrules: (string * string) trrule list -> sg -> sg |
61 val add_trrules: (string * string) trrule list -> sg -> sg |
61 val add_trrules_i: ast trrule list -> sg -> sg |
62 val add_trrules_i: ast trrule list -> sg -> sg |
62 val add_name: string -> sg -> sg |
63 val add_name: string -> sg -> sg |
63 val make_draft: sg -> sg |
64 val make_draft: sg -> sg |
64 val merge: sg * sg -> sg |
65 val merge: sg * sg -> sg |
65 val nonempty_sort: sg * sort list * sort -> bool |
|
66 val proto_pure: sg |
66 val proto_pure: sg |
67 val pure: sg |
67 val pure: sg |
68 val cpure: sg |
68 val cpure: sg |
69 val const_of_class: class -> string |
69 val const_of_class: class -> string |
70 val class_of_const: string -> class |
70 val class_of_const: string -> class |
118 |
118 |
119 val classes = #classes o Type.rep_tsig o tsig_of; |
119 val classes = #classes o Type.rep_tsig o tsig_of; |
120 |
120 |
121 val subsort = Type.subsort o tsig_of; |
121 val subsort = Type.subsort o tsig_of; |
122 val norm_sort = Type.norm_sort o tsig_of; |
122 val norm_sort = Type.norm_sort o tsig_of; |
|
123 val nonempty_sort = Type.nonempty_sort o tsig_of; |
123 |
124 |
124 fun pretty_sort [c] = Pretty.str c |
125 fun pretty_sort [c] = Pretty.str c |
125 | pretty_sort cs = Pretty.str_list "{" "}" cs; |
126 | pretty_sort cs = Pretty.str_list "{" "}" cs; |
126 |
127 |
127 |
128 |
133 fun print_sg sg = |
134 fun print_sg sg = |
134 let |
135 let |
135 fun prt_typ syn ty = Pretty.quote (Syntax.pretty_typ syn ty); |
136 fun prt_typ syn ty = Pretty.quote (Syntax.pretty_typ syn ty); |
136 |
137 |
137 fun pretty_subclass (cl, cls) = Pretty.block |
138 fun pretty_subclass (cl, cls) = Pretty.block |
138 [Pretty.str (cl ^ " <"), Pretty.brk 1, pretty_sort cls]; |
139 (Pretty.str (cl ^ " <") :: Pretty.brk 1 :: |
|
140 Pretty.commas (map Pretty.str cls)); |
139 |
141 |
140 fun pretty_default cls = Pretty.block |
142 fun pretty_default cls = Pretty.block |
141 [Pretty.str "default:", Pretty.brk 1, pretty_sort cls]; |
143 [Pretty.str "default:", Pretty.brk 1, pretty_sort cls]; |
142 |
144 |
143 fun pretty_ty (ty, n) = Pretty.str (ty ^ " " ^ string_of_int n); |
145 fun pretty_ty (ty, n) = Pretty.str (ty ^ " " ^ string_of_int n); |
550 |
552 |
551 val cpure = proto_pure |
553 val cpure = proto_pure |
552 |> add_syntax Syntax.pure_applC_syntax |
554 |> add_syntax Syntax.pure_applC_syntax |
553 |> add_name "CPure"; |
555 |> add_name "CPure"; |
554 |
556 |
555 (** |
|
556 Emptiness-test for sorts: does there exist a type of sort 'sort' whose |
|
557 vars have sorts contained in 'sorts'? |
|
558 Trivial approximation at the moment. |
|
559 **) |
|
560 fun nonempty_sort(_,sorts,sort) = exists (fn s => sort subset s) sorts; |
|
561 |
|
562 end; |
557 end; |