# HG changeset patch # User blanchet # Date 1402527649 -7200 # Node ID c22ad39c3b4bada99c6bb0595c84ed81a58b79a2 # Parent ff69e42ccf9237f195d4ae54303d3de9937bdee7 use 'ctr_sugar' abstraction in SMT(2) diff -r ff69e42ccf92 -r c22ad39c3b4b src/HOL/SMT.thy --- a/src/HOL/SMT.thy Thu Jun 12 01:00:49 2014 +0200 +++ b/src/HOL/SMT.thy Thu Jun 12 01:00:49 2014 +0200 @@ -5,7 +5,7 @@ header {* Bindings to Satisfiability Modulo Theories (SMT) solvers *} theory SMT -imports Record +imports List keywords "smt_status" :: diag begin diff -r ff69e42ccf92 -r c22ad39c3b4b src/HOL/SMT2.thy --- a/src/HOL/SMT2.thy Thu Jun 12 01:00:49 2014 +0200 +++ b/src/HOL/SMT2.thy Thu Jun 12 01:00:49 2014 +0200 @@ -5,7 +5,7 @@ header {* Bindings to Satisfiability Modulo Theories (SMT) solvers based on SMT-LIB 2 *} theory SMT2 -imports Record +imports List keywords "smt2_status" :: diag begin diff -r ff69e42ccf92 -r c22ad39c3b4b src/HOL/Tools/SMT/smt_datatypes.ML --- a/src/HOL/Tools/SMT/smt_datatypes.ML Thu Jun 12 01:00:49 2014 +0200 +++ b/src/HOL/Tools/SMT/smt_datatypes.ML Thu Jun 12 01:00:49 2014 +0200 @@ -17,56 +17,23 @@ val lhs_head_of = Term.head_of o fst o Logic.dest_equals o Thm.prop_of -fun mk_selectors T Ts ctxt = - let - val (sels, ctxt') = - Variable.variant_fixes (replicate (length Ts) "select") ctxt - in (map2 (fn n => fn U => Free (n, T --> U)) sels Ts, ctxt') end +fun mk_selectors T Ts = + Variable.variant_fixes (replicate (length Ts) "select") + #>> map2 (fn U => fn n => Free (n, T --> U)) Ts -(* datatype declarations *) - -fun get_datatype_decl ({descr, ...} : Datatype.info) n Ts ctxt = - let - fun get_vars (_, (m, vs, _)) = if m = n then SOME vs else NONE - val vars = the (get_first get_vars descr) ~~ Ts - val lookup_var = the o AList.lookup (op =) vars - - fun typ_of (dt as Datatype.DtTFree _) = lookup_var dt - | typ_of (Datatype.DtType (m, dts)) = Type (m, map typ_of dts) - | typ_of (Datatype.DtRec i) = - the (AList.lookup (op =) descr i) - |> (fn (m, dts, _) => Type (m, map typ_of dts)) - - fun mk_constr T (m, dts) ctxt = - let - val Ts = map typ_of dts - val constr = Const (m, Ts ---> T) - val (selects, ctxt') = mk_selectors T Ts ctxt - in ((constr, selects), ctxt') end +(* free constructor type declarations *) - fun mk_decl (i, (_, _, constrs)) ctxt = - let - val T = typ_of (Datatype.DtRec i) - val (css, ctxt') = fold_map (mk_constr T) constrs ctxt - in ((T, css), ctxt') end - - in fold_map mk_decl descr ctxt end - - -(* record declarations *) - -val record_name_of = Long_Name.implode o fst o split_last o Long_Name.explode - -fun get_record_decl ({ext_def, ...} : Record.info) T ctxt = +fun get_ctr_sugar_decl ({ctrs, ...} : Ctr_Sugar.ctr_sugar) T Ts ctxt = let - val (con, _) = Term.dest_Const (lhs_head_of ext_def) - val (fields, more) = Record.get_extT_fields (Proof_Context.theory_of ctxt) T - val fieldTs = map snd fields @ [snd more] - - val constr = Const (con, fieldTs ---> T) - val (selects, ctxt') = mk_selectors T fieldTs ctxt - in ((T, [(constr, selects)]), ctxt') end + fun mk_constr ctr0 = + let val ctr = Ctr_Sugar.mk_ctr Ts ctr0 in + mk_selectors T (binder_types (fastype_of ctr)) #>> pair ctr + end + in + fold_map mk_constr ctrs ctxt + |>> (pair T #> single) + end (* typedef declarations *) @@ -91,18 +58,12 @@ fun declared' dss T = exists (exists (equal T o fst) o snd) dss fun get_decls T n Ts ctxt = - let val thy = Proof_Context.theory_of ctxt - in - (case Datatype.get_info thy n of - SOME info => get_datatype_decl info n Ts ctxt - | NONE => - (case Record.get_info thy (record_name_of n) of - SOME info => get_record_decl info T ctxt |>> single - | NONE => - (case Typedef.get_info ctxt n of - [] => ([], ctxt) - | info :: _ => (get_typedef_decl info T Ts, ctxt)))) - end + (case Ctr_Sugar.ctr_sugar_of ctxt n of + SOME ctr_sugar => get_ctr_sugar_decl ctr_sugar T Ts ctxt + | NONE => + (case Typedef.get_info ctxt n of + [] => ([], ctxt) + | info :: _ => (get_typedef_decl info T Ts, ctxt))) fun add_decls T (declss, ctxt) = let @@ -132,5 +93,4 @@ in fold add Us (ins dss, ctxt2) end)) in add T ([], ctxt) |>> append declss o map snd end - end diff -r ff69e42ccf92 -r c22ad39c3b4b src/HOL/Tools/SMT2/smt2_datatypes.ML --- a/src/HOL/Tools/SMT2/smt2_datatypes.ML Thu Jun 12 01:00:49 2014 +0200 +++ b/src/HOL/Tools/SMT2/smt2_datatypes.ML Thu Jun 12 01:00:49 2014 +0200 @@ -15,57 +15,23 @@ structure SMT2_Datatypes: SMT2_DATATYPES = struct -val lhs_head_of = Term.head_of o fst o Logic.dest_equals o Thm.prop_of - -fun mk_selectors T Ts ctxt = - let - val (sels, ctxt') = Variable.variant_fixes (replicate (length Ts) "select") ctxt - in (map2 (fn n => fn U => Free (n, T --> U)) sels Ts, ctxt') end +fun mk_selectors T Ts = + Variable.variant_fixes (replicate (length Ts) "select") + #>> map2 (fn U => fn n => Free (n, T --> U)) Ts -(* datatype declarations *) - -fun get_datatype_decl ({descr, ...} : Datatype.info) n Ts ctxt = - let - fun get_vars (_, (m, vs, _)) = if m = n then SOME vs else NONE - val vars = the (get_first get_vars descr) ~~ Ts - val lookup_var = the o AList.lookup (op =) vars - - fun typ_of (dt as Datatype.DtTFree _) = lookup_var dt - | typ_of (Datatype.DtType (m, dts)) = Type (m, map typ_of dts) - | typ_of (Datatype.DtRec i) = - the (AList.lookup (op =) descr i) - |> (fn (m, dts, _) => Type (m, map typ_of dts)) - - fun mk_constr T (m, dts) ctxt = - let - val Ts = map typ_of dts - val constr = Const (m, Ts ---> T) - val (selects, ctxt') = mk_selectors T Ts ctxt - in ((constr, selects), ctxt') end +(* free constructor type declarations *) - fun mk_decl (i, (_, _, constrs)) ctxt = - let - val T = typ_of (Datatype.DtRec i) - val (css, ctxt') = fold_map (mk_constr T) constrs ctxt - in ((T, css), ctxt') end - - in fold_map mk_decl descr ctxt end - - -(* record declarations *) - -val record_name_of = Long_Name.implode o fst o split_last o Long_Name.explode - -fun get_record_decl ({ext_def, ...} : Record.info) T ctxt = +fun get_ctr_sugar_decl ({ctrs, ...} : Ctr_Sugar.ctr_sugar) T Ts ctxt = let - val (con, _) = Term.dest_Const (lhs_head_of ext_def) - val (fields, more) = Record.get_extT_fields (Proof_Context.theory_of ctxt) T - val fieldTs = map snd fields @ [snd more] - - val constr = Const (con, fieldTs ---> T) - val (selects, ctxt') = mk_selectors T fieldTs ctxt - in ((T, [(constr, selects)]), ctxt') end + fun mk_constr ctr0 = + let val ctr = Ctr_Sugar.mk_ctr Ts ctr0 in + mk_selectors T (binder_types (fastype_of ctr)) #>> pair ctr + end + in + fold_map mk_constr ctrs ctxt + |>> (pair T #> single) + end (* typedef declarations *) @@ -90,18 +56,12 @@ fun declared' dss T = exists (exists (equal T o fst) o snd) dss fun get_decls T n Ts ctxt = - let val thy = Proof_Context.theory_of ctxt - in - (case Datatype.get_info thy n of - SOME info => get_datatype_decl info n Ts ctxt - | NONE => - (case Record.get_info thy (record_name_of n) of - SOME info => get_record_decl info T ctxt |>> single - | NONE => - (case Typedef.get_info ctxt n of - [] => ([], ctxt) - | info :: _ => (get_typedef_decl info T Ts, ctxt)))) - end + (case Ctr_Sugar.ctr_sugar_of ctxt n of + SOME ctr_sugar => get_ctr_sugar_decl ctr_sugar T Ts ctxt + | NONE => + (case Typedef.get_info ctxt n of + [] => ([], ctxt) + | info :: _ => (get_typedef_decl info T Ts, ctxt))) fun add_decls T (declss, ctxt) = let @@ -120,8 +80,7 @@ ([], _) => (dss, ctxt1) | (ds, ctxt2) => let - val constrTs = - maps (map (snd o Term.dest_Const o fst) o snd) ds + val constrTs = maps (map (snd o Term.dest_Const o fst) o snd) ds val Us = fold (union (op =) o Term.binder_types) constrTs [] fun ins [] = [(Us, ds)]