src/HOL/Tools/SMT/smt_translate.ML
changeset 58429 0b94858325a5
parent 58361 7f2b3b6f6ad1
child 61782 7d754aca6a75
     1.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Wed Sep 24 15:46:24 2014 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Wed Sep 24 15:46:25 2014 +0200
     1.3 @@ -19,8 +19,7 @@
     1.4    type sign = {
     1.5      logic: string,
     1.6      sorts: string list,
     1.7 -    lfp_dtyps: (string * (string * (string * string) list) list) list list,
     1.8 -    gfp_dtyps: (string * (string * (string * string) list) list) list list,
     1.9 +    dtyps: (BNF_Util.fp_kind * (string * (string * (string * string) list) list)) list,
    1.10      funcs: (string * (string list * string)) list }
    1.11    type config = {
    1.12      logic: term list -> string,
    1.13 @@ -62,8 +61,7 @@
    1.14  type sign = {
    1.15    logic: string,
    1.16    sorts: string list,
    1.17 -  lfp_dtyps: (string * (string * (string * string) list) list) list list,
    1.18 -  gfp_dtyps: (string * (string * (string * string) list) list) list list,
    1.19 +  dtyps: (BNF_Util.fp_kind * (string * (string * (string * string) list) list)) list,
    1.20    funcs: (string * (string list * string)) list }
    1.21  
    1.22  type config = {
    1.23 @@ -116,11 +114,10 @@
    1.24          val terms' = Termtab.update (t, (name, sort)) terms
    1.25        in (name, (names', typs, terms')) end)
    1.26  
    1.27 -fun sign_of logic lfp_dtyps gfp_dtyps (_, typs, terms) = {
    1.28 +fun sign_of logic dtyps (_, typs, terms) = {
    1.29    logic = logic,
    1.30    sorts = Typtab.fold (fn (_, (n, true)) => cons n | _ => I) typs [],
    1.31 -  lfp_dtyps = lfp_dtyps,
    1.32 -  gfp_dtyps = gfp_dtyps,
    1.33 +  dtyps = dtyps,
    1.34    funcs = Termtab.fold (fn (_, (n, SOME ss)) => cons (n,ss) | _ => I) terms []}
    1.35  
    1.36  fun replay_data_of ctxt ll_defs rules assms (_, typs, terms) =
    1.37 @@ -142,21 +139,15 @@
    1.38  
    1.39  fun collect_co_datatypes fp_kinds (tr_context, ctxt) ts =
    1.40    let
    1.41 -    val (lfp_declss, ctxt') =
    1.42 +    val (fp_decls, ctxt') =
    1.43        ([], ctxt)
    1.44 -      |> member (op =) fp_kinds BNF_Util.Least_FP
    1.45 -        ? fold (Term.fold_types (SMT_Datatypes.add_decls BNF_Util.Least_FP)) ts
    1.46 -    val (gfp_declss, ctxt'') =
    1.47 -      ([], ctxt')
    1.48 -      |> member (op =) fp_kinds BNF_Util.Greatest_FP
    1.49 -        ? fold (Term.fold_types (SMT_Datatypes.add_decls BNF_Util.Greatest_FP)) ts
    1.50 +      |> fold (Term.fold_types (SMT_Datatypes.add_decls fp_kinds)) ts
    1.51 +      |>> flat
    1.52  
    1.53 -    val fp_declsss = [lfp_declss, gfp_declss]
    1.54 -
    1.55 -    fun is_decl_typ T = exists (exists (exists (equal T o fst))) fp_declsss
    1.56 +    fun is_decl_typ T = exists (equal T o fst o snd) fp_decls
    1.57  
    1.58      fun add_typ' T proper =
    1.59 -      (case SMT_Builtin.dest_builtin_typ ctxt'' T of
    1.60 +      (case SMT_Builtin.dest_builtin_typ ctxt' T of
    1.61          SOME n => pair n
    1.62        | NONE => add_typ T proper)
    1.63  
    1.64 @@ -165,17 +156,18 @@
    1.65        in add_fun sel NONE ##>> add_typ' T (not (is_decl_typ T)) end
    1.66      fun tr_constr (constr, selects) =
    1.67        add_fun constr NONE ##>> fold_map tr_select selects
    1.68 -    fun tr_typ (T, cases) = add_typ' T false ##>> fold_map tr_constr cases
    1.69 +    fun tr_typ (fp, (T, cases)) =
    1.70 +      add_typ' T false ##>> fold_map tr_constr cases #>> pair fp
    1.71  
    1.72 -    val (lfp_declss', tr_context') = fold_map (fold_map tr_typ) lfp_declss tr_context
    1.73 -    val (gfp_declss', tr_context'') = fold_map (fold_map tr_typ) gfp_declss tr_context'
    1.74 +    val (fp_decls', tr_context') = fold_map tr_typ fp_decls tr_context
    1.75  
    1.76      fun add (constr, selects) =
    1.77        Termtab.update (constr, length selects) #>
    1.78        fold (Termtab.update o rpair 1) selects
    1.79  
    1.80 -    val funcs = fold (fold (fold (fold add o snd))) fp_declsss Termtab.empty
    1.81 -  in ((funcs, lfp_declss', gfp_declss', tr_context'', ctxt''), ts) end
    1.82 +    val funcs = fold (fold add o snd o snd) fp_decls Termtab.empty
    1.83 +
    1.84 +  in ((funcs, fp_decls', tr_context', ctxt'), ts) end
    1.85      (* FIXME: also return necessary (co)datatype theorems *)
    1.86  
    1.87  
    1.88 @@ -430,7 +422,7 @@
    1.89  
    1.90  (** translation from Isabelle terms into SMT intermediate terms **)
    1.91  
    1.92 -fun intermediate logic lfp_dtyps gfp_dtyps builtin ctxt ts trx =
    1.93 +fun intermediate logic dtyps builtin ctxt ts trx =
    1.94    let
    1.95      fun transT (T as TFree _) = add_typ T true
    1.96        | transT (T as TVar _) = (fn _ => raise TYPE ("bad SMT type", [T], []))
    1.97 @@ -467,7 +459,7 @@
    1.98        end
    1.99  
   1.100      val (us, trx') = fold_map trans ts trx
   1.101 -  in ((sign_of (logic ts) lfp_dtyps gfp_dtyps trx', us), trx') end
   1.102 +  in ((sign_of (logic ts) dtyps trx', us), trx') end
   1.103  
   1.104  
   1.105  (* translation *)
   1.106 @@ -496,11 +488,11 @@
   1.107      val {logic, fp_kinds, serialize} = get_config ctxt
   1.108  
   1.109      fun no_dtyps (tr_context, ctxt) ts =
   1.110 -      ((Termtab.empty, [], [], tr_context, ctxt), ts)
   1.111 +      ((Termtab.empty, [], tr_context, ctxt), ts)
   1.112  
   1.113      val ts1 = map (Envir.beta_eta_contract o SMT_Util.prop_of o snd) ithms
   1.114  
   1.115 -    val ((funcs, lfp_dtyps, gfp_dtyps, tr_context, ctxt1), ts2) =
   1.116 +    val ((funcs, dtyps, tr_context, ctxt1), ts2) =
   1.117        ((empty_tr_context, ctxt), ts1)
   1.118        |-> (if null fp_kinds then no_dtyps else collect_co_datatypes fp_kinds)
   1.119  
   1.120 @@ -527,9 +519,10 @@
   1.121  
   1.122      val ((rewrite_rules, builtin), ts4) = folify ctxt2 ts3
   1.123        |>> apfst (cons fun_app_eq)
   1.124 +val _ = dtyps : (BNF_Util.fp_kind * (string * (string * (string * string) list) list)) list (*###*)
   1.125    in
   1.126      (ts4, tr_context)
   1.127 -    |-> intermediate logic lfp_dtyps gfp_dtyps (builtin SMT_Builtin.dest_builtin) ctxt2
   1.128 +    |-> intermediate logic dtyps (builtin SMT_Builtin.dest_builtin) ctxt2
   1.129      |>> uncurry (serialize smt_options comments)
   1.130      ||> replay_data_of ctxt2 ll_defs rewrite_rules ithms
   1.131    end