src/holyhammer/hhWriter.sml

149 fun os oc s = output (oc,s)
164     then os oc (dfind_err "tyvar" ty (!(#tyvar_names state)))
168       if null Args then os oc s else
170         then (os oc "("; oty state oc (hd Args); os oc " > ";
171               oty state oc (hd (tl Args)); os oc ")")
172         else (os oc ("(" ^ s ^ " ");
173               oiter oc " " (oty state oc) Args; os oc ")")
192   if is_var tm then os oc (dfind_err "var" tm (!(#var_names state)))
201       then os oc (dfind {Thy=Thy,Name=Name} (!(#const_names state)))
202       else (os oc "(";
203             os oc (dfind {Thy=Thy,Name=Name} (!(#const_names state)));
204             os oc " ";
206             os oc ")")
209     (os oc "("; otm state oc (lhs tm);   os oc " = ";  otm state oc (rhs tm);  os oc ")")
211     (os oc "("; otm state oc (lhand tm); os oc " & ";  otm state oc (rand tm); os oc ")")
213     (os oc "("; otm state oc (lhand tm); os oc " | ";  otm state oc (rand tm); os oc ")")
215     (os oc "("; otm state oc (lhand tm); os oc " => "; otm state oc (rand tm); os oc ")")
216   else if is_neg tm      then (os oc "(~ "; otm state oc (rand tm); os oc ")")
222       (os oc "("; otm state oc v; app (fn x => (os oc " "; otm state oc x)) l; os oc ")")
230       (os oc (dfind_err "var" x (!(#var_names state)));
231        os oc " : "; oty state oc (type_of x))
233     os oc ("(" ^ s ^ "[");
235     os oc "]: "; otm state oc tm; os oc ")";
248       os oc "tt("; os oc news; os oc ", ty, ";
250           0 => os oc "$t"
251         | n => (os oc "$t > "; tyd (n - 1))
253         (tyd arity; os oc ").\n")
259   else (os oc "!["; oiter oc ", " (fn x => (os oc x; os oc " : $t")) l; os oc "]: ")
281     os oc "tt("; os oc news; os oc ", ty, ";
283     oty state oc ty; os oc ").\n"; undeclare ()
296     then (os oc "tt("; os oc name;
297           os oc (", " ^ role ^ ", "); quant_tyvarl oc l2;
299           os oc ").\n")
373     fun f x = (os oc x; os oc " "; oiter oc " " (os oc) (parents x); os oc "\n")
376     os oc namespace_tag; os oc " ";
377     oiter oc " " (os oc) [current_theory ()];
378     os oc "\n";