1(* Title: Tools/Argo/argo_term.ML 2 Author: Sascha Boehme 3 4Internal language of the Argo solver. 5 6Terms are fully-shared via hash-consing. Alpha-equivalent terms have the same identifier. 7*) 8 9signature ARGO_TERM = 10sig 11 (* data types *) 12 type meta 13 datatype term = T of meta * Argo_Expr.kind * term list 14 15 (* term operations *) 16 val id_of: term -> int 17 val expr_of: term -> Argo_Expr.expr 18 val type_of: term -> Argo_Expr.typ 19 val eq_term: term * term -> bool 20 val term_ord: term ord 21 22 (* context *) 23 type context 24 val context: context 25 26 (* identifying expressions *) 27 datatype item = Expr of Argo_Expr.expr | Term of term 28 datatype identified = New of term | Known of term 29 val identify_item: item -> context -> identified * context 30end 31 32structure Argo_Term: ARGO_TERM = 33struct 34 35(* data types *) 36 37(* 38 The type meta is intentionally hidden to prevent that functions outside of this structure 39 are able to build terms. Meta stores the identifier of the term as well as the complete 40 expression underlying the term. 41*) 42 43datatype meta = M of int * Argo_Expr.expr 44datatype term = T of meta * Argo_Expr.kind * term list 45 46 47(* term operations *) 48 49fun id_of (T (M (id, _), _, _)) = id 50fun expr_of (T (M (_, e), _, _)) = e 51fun type_of t = Argo_Expr.type_of (expr_of t) 52 53(* 54 Comparing terms is fast as only the identifiers are compared. No expressions need to 55 be taken into account. 56*) 57 58fun eq_term (t1, t2) = (id_of t1 = id_of t2) 59fun term_ord (t1, t2) = int_ord (id_of t1, id_of t2) 60 61 62(* sharing of terms *) 63 64(* 65 Kinds are short representation of expressions. Constants and numbers carry additional 66 information and have no arguments. Their kind is hence similar to them. All other expressions 67 are stored in a flat way with identifiers of shared terms as arguments instead of expression 68 as arguments. 69*) 70 71datatype kind = 72 Con of string * Argo_Expr.typ | 73 Num of Rat.rat | 74 Exp of int list 75 76fun kind_of (Argo_Expr.E (Argo_Expr.Con c, _)) _ = Con c 77 | kind_of (Argo_Expr.E (Argo_Expr.Num n, _)) _ = Num n 78 | kind_of (Argo_Expr.E (k, _)) is = Exp (Argo_Expr.int_of_kind k :: is) 79 80fun int_of_kind (Con _) = 1 81 | int_of_kind (Num _) = 2 82 | int_of_kind (Exp _) = 3 83 84fun kind_ord (Con c1, Con c2) = Argo_Expr.con_ord (c1, c2) 85 | kind_ord (Num n1, Num n2) = Rat.ord (n1, n2) 86 | kind_ord (Exp is1, Exp is2) = dict_ord int_ord (is1, is2) 87 | kind_ord (k1, k2) = int_ord (int_of_kind k1, int_of_kind k2) 88 89structure Kindtab = Table(type key = kind val ord = kind_ord) 90 91(* 92 The context keeps track of the next unused identifier as well as all shared terms, 93 which are indexed by their unique kind. For each term, a boolean marker flag is stored. 94 When set to true on an atom, the atom is already asserted to the solver core. When set to 95 true on an if-then-else term, the term has already been lifted. 96 97 Zero is intentionally avoided as identifier, since literals use term identifiers 98 with a sign as literal identifiers. 99*) 100 101type context = { 102 next_id: int, 103 terms: (term * bool) Kindtab.table} 104 105fun mk_context next_id terms: context = {next_id=next_id, terms=terms} 106 107val context = mk_context 1 Kindtab.empty 108 109fun note_atom true kind (t, false) ({next_id, terms}: context) = 110 mk_context next_id (Kindtab.update (kind, (t, true)) terms) 111 | note_atom _ _ _ cx = cx 112 113fun with_unique_id kind is_atom (e as Argo_Expr.E (k, _)) ts ({next_id, terms}: context) = 114 let val t = T (M (next_id, e), k, ts) 115 in ((t, false), mk_context (next_id + 1) (Kindtab.update (kind, (t, is_atom)) terms)) end 116 117fun unique kind is_atom e ts (cx as {terms, ...}: context) = 118 (case Kindtab.lookup terms kind of 119 SOME tp => (tp, note_atom is_atom kind tp cx) 120 | NONE => with_unique_id kind is_atom e ts cx) 121 122 123(* identifying expressions *) 124 125(* 126 Only atoms, i.e., boolean propositons, and if-then-else expressions need to be identified. 127 Other terms are identified implicitly. The identification process works bottom-up. 128 129 The solver core needs to know whether an atom has already been added. Likewise, the clausifier 130 needs to know whether an if-then-else expression has already been lifted. Therefore, 131 the identified term is marked as either "new" when identified for the first time or 132 "known" when it has already been identified before. 133*) 134 135datatype item = Expr of Argo_Expr.expr | Term of term 136datatype identified = New of term | Known of term 137 138fun identify_head is_atom e (ts, cx) = unique (kind_of e (map id_of ts)) is_atom e ts cx 139 140fun identify is_atom (e as Argo_Expr.E (_, es)) cx = 141 identify_head is_atom e (fold_map (apfst fst oo identify false) es cx) 142 143fun identified (t, true) = Known t 144 | identified (t, false) = New t 145 146fun identify_item (Expr e) cx = identify true e cx |>> identified 147 | identify_item (Term (t as T (_, _, ts))) cx = 148 identify_head true (expr_of t) (ts, cx) |>> identified 149 150end 151 152structure Argo_Termtab = Table(type key = Argo_Term.term val ord = Argo_Term.term_ord) 153