1structure term_pp_utils :> term_pp_utils = 2struct 3 4type term = Term.term 5open smpp term_pp_types term_pp_utils_dtype 6 7fun bv2term (Simple t) = t 8 | bv2term (Restricted {Bvar,...}) = Bvar 9 10fun PP_ERR fname str = Feedback.mk_HOL_ERR "term_pp_utils" fname str 11 12infix >> >- 13 14fun getbvs x = 15 (fupdate (fn x => x) >- 16 (fn (i:printing_info) => return (#current_bvars i))) 17 x 18 19val dflt_pinfo = {seen_frees = Term.empty_tmset, 20 current_bvars = Term.empty_tmset, 21 last_string = " ", in_gspec = false} 22 23fun setbvs bvs = let 24 fun set {seen_frees,current_bvars,last_string,in_gspec} = 25 {seen_frees=seen_frees, current_bvars=bvs,last_string=last_string, 26 in_gspec=in_gspec} 27in 28 fupdate set >> return () 29end 30 31fun addbvs bvlist = 32 getbvs >- (fn old => setbvs (HOLset.addList(old,bvlist))) 33 34fun getfvs x = 35 (fupdate (fn x => x) >- 36 (fn (i:printing_info) => return (#seen_frees i))) 37 x 38 39fun spotfv v = let 40 fun set {seen_frees,current_bvars,last_string,in_gspec} = 41 {seen_frees = HOLset.add(seen_frees, v), 42 current_bvars = current_bvars, last_string=last_string, 43 in_gspec = in_gspec} 44in 45 fupdate set >> return () 46end 47 48fun record_bvars newbvs p = 49 getbvs >- 50 (fn old => setbvs (HOLset.addList(old,newbvs)) >> 51 p >- (fn pres => setbvs old >> return pres)) 52 53fun get_gspec x = 54 (fupdate (fn x => x) >- 55 (fn (i : printing_info) => return (#in_gspec i))) x 56 57fun set_gspec p = let 58 fun set b {in_gspec,current_bvars,seen_frees,last_string} = 59 {in_gspec = b, current_bvars = current_bvars, seen_frees = seen_frees, 60 last_string = last_string} 61in 62 get_gspec >- 63 (fn old => fupdate (set true) >> p >- 64 (fn pval => fupdate (set old) >> return pval)) 65end 66 67fun decdepth n = if n < 0 then n else n - 1 68 69fun mk_pair (t1,t2) = let 70 open HolKernel 71 val fsty = Term.type_of t1 72 val sndty = Term.type_of t2 73 val commaty = fsty --> sndty --> 74 mk_thy_type{Tyop="prod",Thy="pair",Args=[fsty,sndty]} 75 val c = mk_thy_const{Name=",", Thy="pair", Ty = commaty} 76in 77 list_mk_comb(c,[t1,t2]) 78end; 79 80 (* This code will print paired abstractions "properly" only if 81 1. the term has a constant in the right place, and 82 2. that constant maps to the name "UNCURRY" in the overloading map. 83 These conditions are checked in the call to grammar_name. 84 85 We might vary this. In particular, in 2., we could check to see 86 name "UNCURRY" maps to a term (looking at the overload map in the 87 reverse direction). 88 89 Another option again might be to look to see if the term is a 90 constant whose real name is UNCURRY, and if this term also maps 91 to the name UNCURRY. This last used to be the actual 92 implementation, but it's hard to do this in the changed world 93 (since r6355) of "syntactic patterns" because of the way 94 overloading resolution can create fake constants (concealing true 95 names) before this code gets a chance to run. 96 97 The particular choice made above means that the printer does the 98 'right thing' 99 (prints `(\(x,y). x /\ y)` as `pair$UNCURRY (\x y. x /\ y)`) 100 if given a paired abstraction to print wrt an "earlier" grammar, 101 such boolTheory.bool_grammars. *) 102 103fun pp_dest_abs G tm = 104 let 105 open HolKernel 106 fun recurse tm = 107 case dest_term tm of 108 LAMB p => p 109 | COMB(Rator,Rand) => 110 let 111 val _ = 112 term_grammar.grammar_name G Rator = SOME "UNCURRY" orelse 113 raise PP_ERR "pp_dest_abs" "term not an abstraction" 114 val (v1, body0) = recurse Rand 115 val (v2, body) = recurse body0 116 in 117 (mk_pair(v1, v2), body) 118 end 119 | _ => raise PP_ERR "pp_dest_abs" "term not an abstraction" 120 in 121 recurse tm 122 end 123 124fun pp_is_abs G tm = Portable.can (pp_dest_abs G) tm 125 126 127fun has_name G s tm = (term_grammar.grammar_name G tm = SOME s) 128 129fun dest_vstruct G {binder=bnder,restrictor=res} t = 130 let 131 open HolKernel 132 val my_is_abs = pp_is_abs G 133 val my_dest_abs = pp_dest_abs G 134 in 135 case bnder of 136 NONE => 137 let 138 in 139 case (Lib.total (pp_dest_abs G) t, res) of 140 (SOME (bv, body), _) => (Simple bv, body) 141 | (NONE, NONE) => 142 raise PP_ERR "dest_vstruct" "term not an abstraction" 143 | (NONE, SOME s) => 144 let 145 in 146 case dest_term t of 147 COMB (Rator, Rand) => 148 let 149 in 150 case dest_term Rator of 151 COMB(rator1, rand1) => 152 if has_name G s rator1 andalso my_is_abs Rand then 153 let 154 val (bv, body) = my_dest_abs Rand 155 in 156 (Restricted{Bvar = bv, Restrictor = rand1}, body) 157 end 158 else 159 raise PP_ERR "dest_vstruct" "term not an abstraction" 160 | _ => raise PP_ERR "dest_vstruct" 161 "term not an abstraction" 162 end 163 | _ => raise PP_ERR "dest_vstruct" "term not an abstraction" 164 end 165 end 166 | SOME s => 167 let 168 in 169 case (dest_term t) of 170 COMB(Rator,Rand) => 171 let 172 in 173 if has_name G s Rator andalso my_is_abs Rand then 174 let 175 val (bv, body) = my_dest_abs Rand 176 in 177 (Simple bv, body) 178 end 179 else 180 case res of 181 NONE => raise PP_ERR "dest_vstruct" "term not an abstraction" 182 | SOME s => let 183 in 184 case (dest_term Rator) of 185 COMB(rator1, rand1) => 186 if has_name G s rator1 andalso my_is_abs Rand then let 187 val (bv, body) = my_dest_abs Rand 188 in 189 (Restricted{Bvar = bv, Restrictor = rand1}, body) 190 end 191 else 192 raise PP_ERR "dest_vstruct" "term not an abstraction" 193 | _ => 194 raise PP_ERR "dest_vstruct" "term not an abstraction" 195 end 196 end 197 | _ => raise PP_ERR "dest_vstruct" "term not an abstraction" 198 end 199 end 200 201fun strip_vstructs G bres tm = 202 let 203 fun strip acc t = let 204 val (bvar, body) = dest_vstruct G bres t 205 in 206 strip (bvar::acc) body 207 end handle Feedback.HOL_ERR _ => (List.rev acc, t) 208 in 209 strip [] tm 210 end 211 212end (* struct *) 213