src/HOL/Tools/SMT/smt_translate.ML
changeset 66551 4df6b0ae900d
parent 66136 dd006934a719
child 66738 793e7a9c30c5
     1.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Tue Aug 29 16:24:14 2017 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Tue Aug 29 18:30:23 2017 +0200
     1.3 @@ -10,8 +10,8 @@
     1.4    datatype squant = SForall | SExists
     1.5    datatype 'a spattern = SPat of 'a list | SNoPat of 'a list
     1.6    datatype sterm =
     1.7 -    SVar of int |
     1.8 -    SApp of string * sterm list |
     1.9 +    SVar of int * sterm list |
    1.10 +    SConst of string * sterm list |
    1.11      SQua of squant * string list * sterm spattern list * sterm
    1.12  
    1.13    (*translation configuration*)
    1.14 @@ -21,6 +21,7 @@
    1.15      dtyps: (BNF_Util.fp_kind * (string * (string * (string * string) list) list)) list,
    1.16      funcs: (string * (string list * string)) list }
    1.17    type config = {
    1.18 +    order: SMT_Util.order,
    1.19      logic: term list -> string,
    1.20      fp_kinds: BNF_Util.fp_kind list,
    1.21      serialize: (string * string) list -> string list -> sign -> sterm list -> string }
    1.22 @@ -50,8 +51,8 @@
    1.23    SPat of 'a list | SNoPat of 'a list
    1.24  
    1.25  datatype sterm =
    1.26 -  SVar of int |
    1.27 -  SApp of string * sterm list |
    1.28 +  SVar of int * sterm list |
    1.29 +  SConst of string * sterm list |
    1.30    SQua of squant * string list * sterm spattern list * sterm
    1.31  
    1.32  
    1.33 @@ -64,6 +65,7 @@
    1.34    funcs: (string * (string list * string)) list }
    1.35  
    1.36  type config = {
    1.37 +  order: SMT_Util.order,
    1.38    logic: term list -> string,
    1.39    fp_kinds: BNF_Util.fp_kind list,
    1.40    serialize: (string * string) list -> string list -> sign -> sterm list -> string }
    1.41 @@ -147,7 +149,7 @@
    1.42  
    1.43      fun add_typ' T proper =
    1.44        (case SMT_Builtin.dest_builtin_typ ctxt' T of
    1.45 -        SOME n => pair n
    1.46 +        SOME (n, Ts) => pair n (* FIXME HO: Consider Ts *)
    1.47        | NONE => add_typ T proper)
    1.48  
    1.49      fun tr_select sel =
    1.50 @@ -425,11 +427,12 @@
    1.51        | transT (T as TVar _) = (fn _ => raise TYPE ("bad SMT type", [T], []))
    1.52        | transT (T as Type _) =
    1.53            (case SMT_Builtin.dest_builtin_typ ctxt T of
    1.54 -            SOME n => pair n
    1.55 +            SOME (n, []) => pair n
    1.56 +          | SOME (n, Ts) =>
    1.57 +            fold_map transT Ts
    1.58 +            #>> (fn ns => enclose "(" ")" (space_implode " " (n :: ns)))
    1.59            | NONE => add_typ T true)
    1.60  
    1.61 -    fun app n ts = SApp (n, ts)
    1.62 -
    1.63      fun trans t =
    1.64        (case Term.strip_comb t of
    1.65          (Const (qn, _), [Abs (_, T, t1)]) =>
    1.66 @@ -440,17 +443,17 @@
    1.67            | NONE => raise TERM ("unsupported quantifier", [t]))
    1.68        | (u as Const (c as (_, T)), ts) =>
    1.69            (case builtin ctxt c ts of
    1.70 -            SOME (n, _, us, _) => fold_map trans us #>> app n
    1.71 -          | NONE => transs u T ts)
    1.72 -      | (u as Free (_, T), ts) => transs u T ts
    1.73 -      | (Bound i, []) => pair (SVar i)
    1.74 +            SOME (n, _, us, _) => fold_map trans us #>> curry SConst n
    1.75 +          | NONE => trans_applied_fun u T ts)
    1.76 +      | (u as Free (_, T), ts) => trans_applied_fun u T ts
    1.77 +      | (Bound i, ts) => pair i ##>> fold_map trans ts #>> SVar
    1.78        | _ => raise TERM ("bad SMT term", [t]))
    1.79  
    1.80 -    and transs t T ts =
    1.81 +    and trans_applied_fun t T ts =
    1.82        let val (Us, U) = SMT_Util.dest_funT (length ts) T
    1.83        in
    1.84          fold_map transT Us ##>> transT U #-> (fn Up =>
    1.85 -          add_fun t (SOME Up) ##>> fold_map trans ts #>> SApp)
    1.86 +          add_fun t (SOME Up) ##>> fold_map trans ts #>> SConst)
    1.87        end
    1.88  
    1.89      val (us, trx') = fold_map trans ts trx
    1.90 @@ -480,7 +483,7 @@
    1.91  
    1.92  fun translate ctxt smt_options comments ithms =
    1.93    let
    1.94 -    val {logic, fp_kinds, serialize} = get_config ctxt
    1.95 +    val {order, logic, fp_kinds, serialize} = get_config ctxt
    1.96  
    1.97      fun no_dtyps (tr_context, ctxt) ts =
    1.98        ((Termtab.empty, [], tr_context, ctxt), ts)
    1.99 @@ -510,10 +513,14 @@
   1.100        |> rpair ctxt1
   1.101        |-> Lambda_Lifting.lift_lambdas NONE is_binder
   1.102        |-> (fn (ts', ll_defs) => fn ctxt' =>
   1.103 -          (ctxt', (intro_explicit_application ctxt' funcs (map mk_trigger ll_defs @ ts'), ll_defs)))
   1.104 -
   1.105 +        let
   1.106 +          val ts'' = map mk_trigger ll_defs @ ts'
   1.107 +            |> order = SMT_Util.First_Order ? intro_explicit_application ctxt' funcs
   1.108 +        in
   1.109 +          (ctxt', (ts'', ll_defs))
   1.110 +        end)
   1.111      val ((rewrite_rules, builtin), ts4) = folify ctxt2 ts3
   1.112 -      |>> apfst (cons fun_app_eq)
   1.113 +      |>> order = SMT_Util.First_Order ? apfst (cons fun_app_eq)
   1.114    in
   1.115      (ts4, tr_context)
   1.116      |-> intermediate logic dtyps (builtin SMT_Builtin.dest_builtin) ctxt2