src/HOL/Tools/SMT/smt_translate.ML
changeset 39483 9f0e5684f04b
parent 39435 5d18f4c00c07
child 39535 cd1bb7125d8a
     1.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Fri Sep 17 08:41:07 2010 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Fri Sep 17 10:52:35 2010 +0200
     1.3 @@ -291,28 +291,31 @@
     1.4      SOME (f, _) => (f, cx)
     1.5    | NONE => new_fun func_prefix t ss cx)
     1.6  
     1.7 -fun inst_const f Ts t =
     1.8 -  let
     1.9 -    val (n, T) = Term.dest_Const (snd (Type.varify_global [] t))
    1.10 -    val inst = map Term.dest_TVar (snd (Term.dest_Type (f T))) ~~ Ts
    1.11 -  in Const (n, Term_Subst.instantiateT inst T) end
    1.12 +fun mk_type (_, Tfs) (d as Datatype.DtTFree _) = the (AList.lookup (op =) Tfs d)
    1.13 +  | mk_type Ts (Datatype.DtType (n, ds)) = Type (n, map (mk_type Ts) ds)
    1.14 +  | mk_type (Tds, _) (Datatype.DtRec i) = nth Tds i
    1.15  
    1.16 -fun inst_constructor Ts = inst_const Term.body_type Ts
    1.17 -fun inst_selector Ts = inst_const Term.domain_type Ts
    1.18 +fun mk_selector ctxt Ts T n (i, d) =
    1.19 +  (case Datatype_Selectors.lookup_selector ctxt (n, i+1) of
    1.20 +    NONE => raise Fail ("missing selector for datatype constructor " ^ quote n)
    1.21 +  | SOME m => mk_type Ts d |> (fn U => (Const (m, T --> U), U)))
    1.22 +
    1.23 +fun mk_constructor ctxt Ts T (n, args) =
    1.24 +  let val (sels, Us) = split_list (map_index (mk_selector ctxt Ts T n) args)
    1.25 +  in (Const (n, Us ---> T), sels) end
    1.26  
    1.27 -fun lookup_datatype ctxt n Ts = (* FIXME: use Datatype/Record.get_info *)
    1.28 -  if n = @{type_name prod}
    1.29 -  then SOME [
    1.30 -    (Type (n, Ts), [
    1.31 -      (inst_constructor Ts @{term Pair},
    1.32 -        map (inst_selector Ts) [@{term fst}, @{term snd}])])]
    1.33 -  else if n = @{type_name list}
    1.34 -  then SOME [
    1.35 -    (Type (n, Ts), [
    1.36 -      (inst_constructor Ts @{term Nil}, []),
    1.37 -      (inst_constructor Ts @{term Cons},
    1.38 -        map (inst_selector Ts) [@{term hd}, @{term tl}])])]
    1.39 -  else NONE
    1.40 +fun lookup_datatype ctxt n Ts = if n = @{type_name bool} then NONE else
    1.41 +  (case Datatype.get_info (ProofContext.theory_of ctxt) n of
    1.42 +    NONE => NONE  (* FIXME: also use Record.get_info *)
    1.43 +  | SOME {descr, ...} =>
    1.44 +      let
    1.45 +        val Tds = map (fn (_, (tn, _, _)) => Type (tn, Ts))
    1.46 +          (sort (int_ord o pairself fst) descr)
    1.47 +        val Tfs = (case hd descr of (_, (_, tfs, _)) => tfs ~~ Ts)
    1.48 +      in
    1.49 +        SOME (descr |> map (fn (i, (_, _, cs)) =>
    1.50 +          (nth Tds i, map (mk_constructor ctxt (Tds, Tfs) (nth Tds i)) cs)))
    1.51 +      end)
    1.52  
    1.53  fun relaxed thms = (([], thms), map prop_of thms)
    1.54