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