Added infrastructure for mapping SPARK field / constructor names
authorberghofe
Tue Feb 28 11:10:09 2012 +0100 (2012-02-28)
changeset 46725d34ec0512dfb
parent 46724 5759ecd5c905
child 46726 49cbc06af3e5
Added infrastructure for mapping SPARK field / constructor names
to Isabelle types
src/HOL/SPARK/Manual/Reference.thy
src/HOL/SPARK/Tools/spark_commands.ML
src/HOL/SPARK/Tools/spark_vcs.ML
     1.1 --- a/src/HOL/SPARK/Manual/Reference.thy	Mon Feb 27 10:32:39 2012 +0100
     1.2 +++ b/src/HOL/SPARK/Manual/Reference.thy	Tue Feb 28 11:10:09 2012 +0100
     1.3 @@ -43,11 +43,14 @@
     1.4  or packages, whereas the former allows the given term to refer to the types generated
     1.5  by \isa{\isacommand{spark\_open}} for record or enumeration types specified in the
     1.6  \texttt{*.fdl} file.
     1.7 -@{rail "@'spark_types' ((name '=' type)+)"}
     1.8 +@{rail "@'spark_types' ((name '=' type (mapping?))+);
     1.9 +mapping: '('((name '=' nameref)+',')')'"}
    1.10  Associates a \SPARK{} type with the given name with an Isabelle type. This command can
    1.11  only be used outside a verification environment. The given type must be either a record
    1.12 -or a datatype, where the field names and constructors must match those of the corresponding
    1.13 -\SPARK{} types (modulo casing). This command is useful when having to define
    1.14 +or a datatype, where the names of fields or constructors must either match those of the
    1.15 +corresponding \SPARK{} types (modulo casing), or a mapping from \SPARK{} to Isabelle
    1.16 +names has to be provided.
    1.17 +This command is useful when having to define
    1.18  proof functions referring to record or enumeration types that are shared by several
    1.19  procedures or packages. First, the types required by the proof functions can be introduced
    1.20  using Isabelle's commands for defining records or datatypes. Having introduced the
     2.1 --- a/src/HOL/SPARK/Tools/spark_commands.ML	Mon Feb 27 10:32:39 2012 +0100
     2.2 +++ b/src/HOL/SPARK/Tools/spark_commands.ML	Tue Feb 28 11:10:09 2012 +0100
     2.3 @@ -40,8 +40,8 @@
     2.4         Syntax.check_term ctxt) pf thy
     2.5    end;
     2.6  
     2.7 -fun add_spark_type_cmd (s, raw_typ) thy =
     2.8 -  SPARK_VCs.add_type (s, Syntax.read_typ_global thy raw_typ) thy;
     2.9 +fun add_spark_type_cmd (s, (raw_typ, cmap)) thy =
    2.10 +  SPARK_VCs.add_type (s, (Syntax.read_typ_global thy raw_typ, cmap)) thy;
    2.11  
    2.12  fun get_vc thy vc_name =
    2.13    (case SPARK_VCs.lookup_vc thy vc_name of
    2.14 @@ -124,7 +124,9 @@
    2.15    Outer_Syntax.command "spark_types"
    2.16      "associate SPARK types with types"
    2.17      Keyword.thy_decl
    2.18 -    (Scan.repeat1 (Parse.name --| Args.$$$ "=" -- Parse.typ) >>
    2.19 +    (Scan.repeat1 (Parse.name -- Parse.!!! (Args.$$$ "=" |-- Parse.typ --
    2.20 +       Scan.optional (Args.parens (Parse.list1
    2.21 +         (Parse.name -- Parse.!!! (Args.$$$ "=" |-- Parse.xname)))) [])) >>
    2.22         (Toplevel.theory o fold add_spark_type_cmd));
    2.23  
    2.24  val _ =
     3.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML	Mon Feb 27 10:32:39 2012 +0100
     3.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Tue Feb 28 11:10:09 2012 +0100
     3.3 @@ -12,7 +12,7 @@
     3.4    val add_proof_fun: (typ option -> 'a -> term) ->
     3.5      string * ((string list * string) option * 'a) ->
     3.6      theory -> theory
     3.7 -  val add_type: string * typ -> theory -> theory
     3.8 +  val add_type: string * (typ * (string * string) list) -> theory -> theory
     3.9    val lookup_vc: theory -> string -> (Element.context_i list *
    3.10      (string * thm list option * Element.context_i * Element.statement_i)) option
    3.11    val get_vcs: theory ->
    3.12 @@ -44,7 +44,7 @@
    3.13  (
    3.14    type T =
    3.15      {pfuns: ((string list * string) option * term) Symtab.table,
    3.16 -     type_map: typ Symtab.table,
    3.17 +     type_map: (typ * (string * string) list) Symtab.table,
    3.18       env:
    3.19         {ctxt: Element.context_i list,
    3.20          defs: (binding * thm) list,
    3.21 @@ -86,6 +86,11 @@
    3.22        | strip ys (x :: xs) = strip (x :: ys) xs
    3.23    in strip [] (rev (raw_explode s)) end;
    3.24  
    3.25 +fun unprefix_pfun "" s = s
    3.26 +  | unprefix_pfun prfx s =
    3.27 +      let val (prfx', s') = strip_prfx s
    3.28 +      in if prfx = prfx' then s' else s end;
    3.29 +
    3.30  fun mk_unop s t =
    3.31    let val T = fastype_of t
    3.32    in Const (s, T --> T) $ t end;
    3.33 @@ -104,14 +109,17 @@
    3.34    let val {type_map, ...} = VCs.get thy
    3.35    in lookup_prfx prfx type_map ty end;
    3.36  
    3.37 -fun mk_type _ _ "integer" = HOLogic.intT
    3.38 -  | mk_type _ _ "boolean" = HOLogic.boolT
    3.39 -  | mk_type thy prfx ty =
    3.40 +fun mk_type' _ _ "integer" = (HOLogic.intT, [])
    3.41 +  | mk_type' _ _ "boolean" = (HOLogic.boolT, [])
    3.42 +  | mk_type' thy prfx ty =
    3.43        (case get_type thy prfx ty of
    3.44           NONE =>
    3.45 -           Syntax.check_typ (Proof_Context.init_global thy)
    3.46 -             (Type (Sign.full_name thy (Binding.name ty), []))
    3.47 -       | SOME T => T);
    3.48 +           (Syntax.check_typ (Proof_Context.init_global thy)
    3.49 +              (Type (Sign.full_name thy (Binding.name ty), [])),
    3.50 +            [])
    3.51 +       | SOME p => p);
    3.52 +
    3.53 +fun mk_type thy prfx ty = fst (mk_type' thy prfx ty);
    3.54  
    3.55  val booleanN = "boolean";
    3.56  val integerN = "integer";
    3.57 @@ -146,7 +154,12 @@
    3.58        Record.get_info thy (Long_Name.qualifier tyname)
    3.59    | _ => NONE);
    3.60  
    3.61 -fun find_field fname = find_first (curry lcase_eq fname o fst);
    3.62 +fun find_field [] fname fields =
    3.63 +      find_first (curry lcase_eq fname o fst) fields
    3.64 +  | find_field cmap fname fields =
    3.65 +      (case AList.lookup (op =) cmap fname of
    3.66 +         NONE => NONE
    3.67 +       | SOME fname' => SOME (fname', the (AList.lookup (op =) fields fname')));
    3.68  
    3.69  fun find_field' fname = get_first (fn (flds, fldty) =>
    3.70    if member (op =) flds fname then SOME fldty else NONE);
    3.71 @@ -291,6 +304,10 @@
    3.72        else SOME ("either has no element " ^ el ^
    3.73          " or it is at the wrong position");
    3.74  
    3.75 +fun invert_map [] = I
    3.76 +  | invert_map cmap =
    3.77 +      map (apfst (the o AList.lookup (op =) (map swap cmap)));
    3.78 + 
    3.79  fun add_type_def prfx (s, Basic_Type ty) (ids, thy) =
    3.80        (check_no_assoc thy prfx s;
    3.81         (ids,
    3.82 @@ -307,26 +324,23 @@
    3.83                in
    3.84                  (thy |>
    3.85                   Datatype.add_datatype {strict = true, quiet = true}
    3.86 -                   [((tyb, [], NoSyn), map (fn s => (Binding.name s, [], NoSyn)) els)] |> snd |>
    3.87 +                   [((tyb, [], NoSyn),
    3.88 +                     map (fn s => (Binding.name s, [], NoSyn)) els)] |> snd |>
    3.89                   add_enum_type s tyname,
    3.90                   tyname)
    3.91                end
    3.92 -          | SOME (T as Type (tyname, [])) =>
    3.93 +          | SOME (T as Type (tyname, []), cmap) =>
    3.94                (case Datatype.get_constrs thy tyname of
    3.95                   NONE => assoc_ty_err thy T s "is not a datatype"
    3.96                 | SOME cs =>
    3.97 -                   let
    3.98 -                     val (prfx', _) = strip_prfx s;
    3.99 -                     val els' =
   3.100 -                       if prfx' = "" then els
   3.101 -                       else map (unprefix (prfx' ^ "__")) els
   3.102 -                         handle Fail _ => error ("Bad enumeration type " ^ s)
   3.103 +                   let val (prfx', _) = strip_prfx s
   3.104                     in
   3.105 -                     case check_enum els' cs of
   3.106 +                     case check_enum (map (unprefix_pfun prfx') els)
   3.107 +                         (invert_map cmap cs) of
   3.108                         NONE => (thy, tyname)
   3.109                       | SOME msg => assoc_ty_err thy T s msg
   3.110                     end)
   3.111 -          | SOME T => assoc_ty_err thy T s "is not a datatype");
   3.112 +          | SOME (T, _) => assoc_ty_err thy T s "is not a datatype");
   3.113          val cs = map Const (the (Datatype.get_constrs thy' tyname));
   3.114        in
   3.115          ((fold (Symtab.update_new o apsnd (rpair s)) (els ~~ cs) tab,
   3.116 @@ -349,24 +363,27 @@
   3.117             NONE =>
   3.118               Record.add_record ([], Binding.name s) NONE
   3.119                 (map (fn (fld, T) => (Binding.name fld, T, NoSyn)) fldTs) thy
   3.120 -         | SOME rT =>
   3.121 +         | SOME (rT, cmap) =>
   3.122               (case get_record_info thy rT of
   3.123                  NONE => assoc_ty_err thy rT s "is not a record type"
   3.124                | SOME {fields, ...} =>
   3.125 -                  (case subtract (lcase_eq o pairself fst) fldTs fields of
   3.126 -                     [] => ()
   3.127 -                   | flds => assoc_ty_err thy rT s ("has extra field(s) " ^
   3.128 -                       commas (map (Long_Name.base_name o fst) flds));
   3.129 -                   map (fn (fld, T) =>
   3.130 -                     case AList.lookup lcase_eq fields fld of
   3.131 -                       NONE => assoc_ty_err thy rT s ("has no field " ^ fld)
   3.132 -                     | SOME U => T = U orelse assoc_ty_err thy rT s
   3.133 -                         ("has field " ^
   3.134 -                          fld ^ " whose type\n" ^
   3.135 -                          Syntax.string_of_typ_global thy U ^
   3.136 -                          "\ndoes not match declared type\n" ^
   3.137 -                          Syntax.string_of_typ_global thy T)) fldTs;
   3.138 -                   thy))
   3.139 +                  let val fields' = invert_map cmap fields
   3.140 +                  in
   3.141 +                    (case subtract (lcase_eq o pairself fst) fldTs fields' of
   3.142 +                       [] => ()
   3.143 +                     | flds => assoc_ty_err thy rT s ("has extra field(s) " ^
   3.144 +                         commas (map (Long_Name.base_name o fst) flds));
   3.145 +                     map (fn (fld, T) =>
   3.146 +                       case AList.lookup lcase_eq fields' fld of
   3.147 +                         NONE => assoc_ty_err thy rT s ("has no field " ^ fld)
   3.148 +                       | SOME U => T = U orelse assoc_ty_err thy rT s
   3.149 +                           ("has field " ^
   3.150 +                            fld ^ " whose type\n" ^
   3.151 +                            Syntax.string_of_typ_global thy U ^
   3.152 +                            "\ndoes not match declared type\n" ^
   3.153 +                            Syntax.string_of_typ_global thy T)) fldTs;
   3.154 +                     thy)
   3.155 +                  end)
   3.156         end)
   3.157  
   3.158    | add_type_def prfx (s, Pending_Type) (ids, thy) =
   3.159 @@ -467,10 +484,10 @@
   3.160                 [e] =>
   3.161                   let
   3.162                     val (t, rcdty) = tm_of vs e;
   3.163 -                   val rT = mk_type thy prfx rcdty
   3.164 +                   val (rT, cmap) = mk_type' thy prfx rcdty
   3.165                   in case (get_record_info thy rT, lookup types rcdty) of
   3.166                       (SOME {fields, ...}, SOME (Record_Type fldtys)) =>
   3.167 -                       (case (find_field fname fields,
   3.168 +                       (case (find_field cmap fname fields,
   3.169                              find_field' fname fldtys) of
   3.170                            (SOME (fname', fT), SOME fldty) =>
   3.171                              (Const (fname', rT --> fT) $ t, fldty)
   3.172 @@ -487,12 +504,12 @@
   3.173                 [e, e'] =>
   3.174                   let
   3.175                     val (t, rcdty) = tm_of vs e;
   3.176 -                   val rT = mk_type thy prfx rcdty;
   3.177 +                   val (rT, cmap) = mk_type' thy prfx rcdty;
   3.178                     val (u, fldty) = tm_of vs e';
   3.179                     val fT = mk_type thy prfx fldty
   3.180                   in case get_record_info thy rT of
   3.181                       SOME {fields, ...} =>
   3.182 -                       (case find_field fname fields of
   3.183 +                       (case find_field cmap fname fields of
   3.184                            SOME (fname', fU) =>
   3.185                              if fT = fU then
   3.186                                (Const (fname' ^ "_update",
   3.187 @@ -576,13 +593,14 @@
   3.188  
   3.189        | tm_of vs (Record (s, flds)) =
   3.190            let
   3.191 -            val T = mk_type thy prfx s;
   3.192 +            val (T, cmap) = mk_type' thy prfx s;
   3.193              val {extension = (ext_name, _), fields, ...} =
   3.194                (case get_record_info thy T of
   3.195                   NONE => error (s ^ " is not a record type")
   3.196                 | SOME info => info);
   3.197              val flds' = map (apsnd (tm_of vs)) flds;
   3.198 -            val fnames = map (Long_Name.base_name o fst) fields;
   3.199 +            val fnames = fields |> invert_map cmap |>
   3.200 +              map (Long_Name.base_name o fst);
   3.201              val fnames' = map fst flds;
   3.202              val (fvals, ftys) = split_list (map (fn s' =>
   3.203                case AList.lookup lcase_eq flds' s' of
   3.204 @@ -727,11 +745,6 @@
   3.205  
   3.206  fun upd_option x y = if is_some x then x else y;
   3.207  
   3.208 -fun unprefix_pfun "" s = s
   3.209 -  | unprefix_pfun prfx s =
   3.210 -      let val (prfx', s') = strip_prfx s
   3.211 -      in if prfx = prfx' then s' else s end;
   3.212 -
   3.213  fun check_pfuns_types thy prfx funs =
   3.214    Symtab.map (fn s => fn (optty, t) =>
   3.215     let val optty' = lookup funs (unprefix_pfun prfx s)
   3.216 @@ -834,29 +847,54 @@
   3.217         else error ("Undeclared proof function " ^ s))
   3.218      end) thy;
   3.219  
   3.220 -fun add_type (s, T as Type (tyname, Ts)) thy =
   3.221 -      thy |>
   3.222 -      VCs.map (fn
   3.223 -          {env = SOME _, ...} => err_unfinished ()
   3.224 -        | {pfuns, type_map, env} =>
   3.225 -            {pfuns = pfuns,
   3.226 -             type_map = Symtab.update_new (s, T) type_map,
   3.227 -             env = env}
   3.228 -              handle Symtab.DUP _ => error ("SPARK type " ^ s ^
   3.229 -                " already associated with type")) |>
   3.230 -      (fn thy' =>
   3.231 -         case Datatype.get_constrs thy' tyname of
   3.232 -           NONE => thy'
   3.233 -         | SOME cs =>
   3.234 -             if null Ts then
   3.235 -               (map
   3.236 -                  (fn (_, Type (_, [])) => ()
   3.237 -                    | (cname, _) => assoc_ty_err thy T s
   3.238 -                        ("has illegal constructor " ^
   3.239 -                         Long_Name.base_name cname)) cs;
   3.240 -                add_enum_type s tyname thy')
   3.241 -             else assoc_ty_err thy T s "is illegal")
   3.242 -  | add_type (s, T) thy = assoc_ty_err thy T s "is illegal";
   3.243 +fun check_mapping _ _ [] _ = ()
   3.244 +  | check_mapping err s cmap cs =
   3.245 +      (case duplicates (op = o pairself fst) cmap of
   3.246 +         [] => (case duplicates (op = o pairself snd) cmap of
   3.247 +             [] => (case subtract (op = o apsnd snd) cs cmap of
   3.248 +                 [] => (case subtract (op = o apfst snd) cmap cs of
   3.249 +                     [] => ()
   3.250 +                   | zs => err ("has extra " ^ s ^ "(s) " ^ commas zs))
   3.251 +               | zs => err ("does not have " ^ s ^ "(s) " ^
   3.252 +                   commas (map snd zs)))
   3.253 +           | zs => error ("Several SPARK names are mapped to " ^
   3.254 +               commas (map snd zs)))
   3.255 +       | zs => error ("The SPARK names " ^ commas (map fst zs) ^
   3.256 +           " are mapped to more than one name"));
   3.257 +
   3.258 +fun add_type (s, (T as Type (tyname, Ts), cmap)) thy =
   3.259 +      let val cmap' = map (apsnd (Sign.intern_const thy)) cmap
   3.260 +      in
   3.261 +        thy |>
   3.262 +        VCs.map (fn
   3.263 +            {env = SOME _, ...} => err_unfinished ()
   3.264 +          | {pfuns, type_map, env} =>
   3.265 +              {pfuns = pfuns,
   3.266 +               type_map = Symtab.update_new (s, (T, cmap')) type_map,
   3.267 +               env = env}
   3.268 +                handle Symtab.DUP _ => error ("SPARK type " ^ s ^
   3.269 +                  " already associated with type")) |>
   3.270 +        (fn thy' =>
   3.271 +           case Datatype.get_constrs thy' tyname of
   3.272 +             NONE => (case get_record_info thy' T of
   3.273 +               NONE => thy'
   3.274 +             | SOME {fields, ...} =>
   3.275 +                 (check_mapping (assoc_ty_err thy' T s) "field"
   3.276 +                    cmap' (map fst fields);
   3.277 +                  thy'))
   3.278 +           | SOME cs =>
   3.279 +               if null Ts then
   3.280 +                 (map
   3.281 +                    (fn (_, Type (_, [])) => ()
   3.282 +                      | (cname, _) => assoc_ty_err thy' T s
   3.283 +                          ("has illegal constructor " ^
   3.284 +                           Long_Name.base_name cname)) cs;
   3.285 +                  check_mapping (assoc_ty_err thy' T s) "constructor"
   3.286 +                    cmap' (map fst cs);
   3.287 +                  add_enum_type s tyname thy')
   3.288 +               else assoc_ty_err thy' T s "is illegal")
   3.289 +      end
   3.290 +  | add_type (s, (T, _)) thy = assoc_ty_err thy T s "is illegal";
   3.291  
   3.292  val is_closed = is_none o #env o VCs.get;
   3.293