src/HolSmt/Yices.sml

170      defs: list of auxiliary Yices definitions *)
173       fun uninterpreted_type (acc as (ty_dict, fresh, defs), ty) =
178                       val defs' = "(define-type " ^ name ^ ")" :: defs
191                     ((ty_dict', fresh + 1, defs'), name)
194       fun data_type tyinfo (acc as (ty_dict, fresh, defs), ty) =
199                       val acc = (ty_dict', fresh + 1, defs)
230                       val (ty_dict, fresh, defs) = acc
231                       val defs' = "(define-type " ^ name ^ " " ^ datatype_def ^
232                         ")" :: defs
234                     ((ty_dict, fresh, defs'), name)
252             let val ((ty_dict, fresh, defs), yices_Args) = Lib.foldl_map
254                 val defs' = if def = "" orelse Lib.mem def defs then defs else
255                   def :: defs
258               ((ty_dict, fresh, defs'),
277      defs: list of auxiliary Yices definitions *)
458               val (dict, fresh, ty_dict, ty_fresh, defs) = acc
462                 ((ty_dict, ty_fresh, defs), typs)
463               val (ty_dict, ty_fresh, defs) = ty_acc
474               val acc = (union dict bound_dict, fresh, ty_dict, ty_fresh, defs)
476               val (body_dict, fresh, ty_dict, ty_fresh, defs) = acc
486               SOME ((dict, fresh, ty_dict, ty_fresh, defs),
499               val (dict, fresh, ty_dict, ty_fresh, defs) = acc'
500               val defs' = if def = "" orelse Lib.mem def defs then defs else
501                 def :: defs
504             ((dict, fresh, ty_dict, ty_fresh, defs'),
519                     val (dict, fresh, ty_dict, ty_fresh, defs) = acc
520                     val ((ty_dict, ty_fresh, defs), _) = translate_type
521                       ((ty_dict, ty_fresh, defs), ty)
526                       ((dict, fresh, ty_dict, ty_fresh, defs), rands)
681             let val (dict, fresh, ty_dict, ty_fresh, defs) = acc
689                     val ((ty_dict, ty_fresh, defs), ty_name) = translate_type
690                       ((ty_dict, ty_fresh, defs), Term.type_of tm)
691                     val defs = "(define " ^ name ^ "::" ^ ty_name ^ ")" :: defs
704                   ((dict, fresh + 1, ty_dict, ty_fresh, defs), name)
757     val ((_, _, _, _, defs), yices_asl_g) = Lib.foldl_map translate_term
759     val defs = List.map (fn s => s ^ "\n") (List.rev defs)
762     defs @ yices_asl_g @ ["(check)\n"]