# HG changeset patch # User berghofe # Date 1302874437 -7200 # Node ID e8777e3ea6ef3ae5c47d9d34709910164fce0f2f # Parent ce00462fe8aade9033a296b8ffba45528aa94a7d Added command for associating user-defined types with SPARK types. diff -r ce00462fe8aa -r e8777e3ea6ef etc/isar-keywords.el --- a/etc/isar-keywords.el Thu Apr 14 15:04:42 2011 +0200 +++ b/etc/isar-keywords.el Fri Apr 15 15:33:57 2011 +0200 @@ -227,6 +227,7 @@ "spark_open" "spark_proof_functions" "spark_status" + "spark_types" "spark_vc" "specification" "statespace" @@ -520,6 +521,7 @@ "spark_end" "spark_open" "spark_proof_functions" + "spark_types" "statespace" "syntax" "syntax_declaration" diff -r ce00462fe8aa -r e8777e3ea6ef src/HOL/SPARK/Tools/spark_commands.ML --- a/src/HOL/SPARK/Tools/spark_commands.ML Thu Apr 14 15:04:42 2011 +0200 +++ b/src/HOL/SPARK/Tools/spark_commands.ML Fri Apr 15 15:33:57 2011 +0200 @@ -27,7 +27,7 @@ SPARK_VCs.set_vcs (snd (Fdl_Parser.parse_declarations (Path.position fdl_path) (File.read fdl_path))) (Fdl_Parser.parse_rules (Path.position rls_path) (File.read rls_path)) - (snd (snd (Fdl_Parser.parse_vcs header (Path.position vc_path) (File.read vc_path)))) + (snd (Fdl_Parser.parse_vcs header (Path.position vc_path) (File.read vc_path))) base thy end; @@ -39,6 +39,9 @@ Syntax.check_term ctxt) pf thy end; +fun add_spark_type_cmd (s, raw_typ) thy = + SPARK_VCs.add_type (s, Syntax.read_typ_global thy raw_typ) thy; + fun get_vc thy vc_name = (case SPARK_VCs.lookup_vc thy vc_name of SOME (ctxt, (_, proved, ctxt', stmt)) => @@ -117,6 +120,13 @@ (Toplevel.theory o fold add_proof_fun_cmd)); val _ = + Outer_Syntax.command "spark_types" + "associate SPARK types with types" + Keyword.thy_decl + (Scan.repeat1 (Parse.name --| Args.$$$ "=" -- Parse.typ) >> + (Toplevel.theory o fold add_spark_type_cmd)); + +val _ = Outer_Syntax.command "spark_vc" "enter into proof mode for a specific verification condition" Keyword.thy_goal diff -r ce00462fe8aa -r e8777e3ea6ef src/HOL/SPARK/Tools/spark_vcs.ML --- a/src/HOL/SPARK/Tools/spark_vcs.ML Thu Apr 14 15:04:42 2011 +0200 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML Fri Apr 15 15:33:57 2011 +0200 @@ -7,11 +7,12 @@ signature SPARK_VCS = sig - val set_vcs: Fdl_Parser.decls -> Fdl_Parser.rules -> Fdl_Parser.vcs -> - Path.T -> theory -> theory + val set_vcs: Fdl_Parser.decls -> Fdl_Parser.rules -> + (string * string) * Fdl_Parser.vcs -> Path.T -> theory -> theory val add_proof_fun: (typ option -> 'a -> term) -> string * ((string list * string) option * 'a) -> theory -> theory + val add_type: string * typ -> theory -> theory val lookup_vc: theory -> string -> (Element.context_i list * (string * thm list option * Element.context_i * Element.statement_i)) option val get_vcs: theory -> @@ -28,8 +29,49 @@ open Fdl_Parser; +(** theory data **) + +fun err_unfinished () = error "An unfinished SPARK environment is still open." + +val strip_number = pairself implode o take_suffix Fdl_Lexer.is_digit o raw_explode; + +val name_ord = prod_ord string_ord (option_ord int_ord) o + pairself (strip_number ##> Int.fromString); + +structure VCtab = Table(type key = string val ord = name_ord); + +structure VCs = Theory_Data +( + type T = + {pfuns: ((string list * string) option * term) Symtab.table, + type_map: typ Symtab.table, + env: + {ctxt: Element.context_i list, + defs: (binding * thm) list, + types: fdl_type tab, + funs: (string list * string) tab, + ids: (term * string) Symtab.table * Name.context, + proving: bool, + vcs: (string * thm list option * + (string * expr) list * (string * expr) list) VCtab.table, + path: Path.T} option} + val empty : T = {pfuns = Symtab.empty, type_map = Symtab.empty, env = NONE} + val extend = I + fun merge ({pfuns = pfuns1, type_map = type_map1, env = NONE}, + {pfuns = pfuns2, type_map = type_map2, env = NONE}) = + {pfuns = Symtab.merge (eq_pair (op =) (op aconv)) (pfuns1, pfuns2), + type_map = Symtab.merge (op =) (type_map1, type_map2), + env = NONE} + | merge _ = err_unfinished () +) + + (** utilities **) +val to_lower = raw_explode #> map Symbol.to_ascii_lower #> implode; + +val lcase_eq = (op =) o pairself (to_lower o Long_Name.base_name); + fun mk_unop s t = let val T = fastype_of t in Const (s, T --> T) $ t end; @@ -44,17 +86,22 @@ HOLogic.mk_setT (HOLogic.mk_prodT (T, U))) $ t $ Abs ("", T, u) end; +fun get_type thy ty = + let val {type_map, ...} = VCs.get thy + in Symtab.lookup type_map ty end; + fun mk_type _ "integer" = HOLogic.intT | mk_type _ "boolean" = HOLogic.boolT - | mk_type thy ty = Syntax.check_typ (ProofContext.init_global thy) - (Type (Sign.full_name thy (Binding.name ty), [])); + | mk_type thy ty = + (case get_type thy ty of + NONE => + Syntax.check_typ (ProofContext.init_global thy) + (Type (Sign.full_name thy (Binding.name ty), [])) + | SOME T => T); val booleanN = "boolean"; val integerN = "integer"; -fun mk_qual_name thy s s' = - Sign.full_name thy (Binding.qualify true s (Binding.name s')); - fun define_overloaded (def_name, eq) lthy = let val ((c, _), rhs) = eq |> Syntax.check_term lthy |> @@ -80,17 +127,29 @@ val zs = map (Free o rpair T) ys; in (zs, (fold (Symtab.update o apsnd (rpair ty)) (xs ~~ zs) tab, ctxt')) end; +fun get_record_info thy T = (case Record.dest_recTs T of + [(tyname, [@{typ unit}])] => + Record.get_info thy (Long_Name.qualifier tyname) + | _ => NONE); + +fun find_field fname = find_first (curry lcase_eq fname o fst); + +fun find_field' fname = get_first (fn (flds, fldty) => + if member (op =) flds fname then SOME fldty else NONE); + +fun assoc_ty_err thy T s msg = + error ("Type " ^ Syntax.string_of_typ_global thy T ^ + " associated with SPARK type " ^ s ^ "\n" ^ msg); + (** generate properties of enumeration types **) -fun add_enum_type tyname els (tab, ctxt) thy = +fun add_enum_type tyname tyname' thy = let - val tyb = Binding.name tyname; - val tyname' = Sign.full_name thy tyb; + val {case_name, ...} = the (Datatype_Data.get_info thy tyname'); + val cs = map Const (the (Datatype_Data.get_constrs thy tyname')); + val k = length cs; val T = Type (tyname', []); - val case_name = mk_qual_name thy tyname (tyname ^ "_case"); - val cs = map (fn s => Const (mk_qual_name thy tyname s, T)) els; - val k = length els; val p = Const (@{const_name pos}, T --> HOLogic.intT); val v = Const (@{const_name val}, HOLogic.intT --> T); val card = Const (@{const_name card}, @@ -103,9 +162,6 @@ (f $ Bound 1) $ (f $ Bound 0)))); val (((def1, def2), def3), lthy) = thy |> - Datatype.add_datatype {strict = true, quiet = true} [tyname] - [([], tyb, NoSyn, - map (fn s => (Binding.name s, [], NoSyn)) els)] |> snd |> Class.instantiation ([tyname'], [], @{sort enum}) |> @@ -195,46 +251,107 @@ val simp_att = [Attrib.internal (K Simplifier.simp_add)] in - ((fold (Symtab.update_new o apsnd (rpair tyname)) (els ~~ cs) tab, - fold Name.declare els ctxt), - lthy' |> - Local_Theory.note - ((Binding.name (tyname ^ "_card_UNIV"), simp_att), [card_UNIV]) ||>> - Local_Theory.note - ((Binding.name (tyname ^ "_pos"), simp_att), pos_eqs) ||>> - Local_Theory.note - ((Binding.name (tyname ^ "_val"), simp_att), val_eqs) ||>> - Local_Theory.note - ((Binding.name (tyname ^ "_first_el"), simp_att), [first_el]) ||>> - Local_Theory.note - ((Binding.name (tyname ^ "_last_el"), simp_att), [last_el]) |> snd |> - Local_Theory.exit_global) + lthy' |> + Local_Theory.note + ((Binding.name (tyname ^ "_card_UNIV"), simp_att), [card_UNIV]) ||>> + Local_Theory.note + ((Binding.name (tyname ^ "_pos"), simp_att), pos_eqs) ||>> + Local_Theory.note + ((Binding.name (tyname ^ "_val"), simp_att), val_eqs) ||>> + Local_Theory.note + ((Binding.name (tyname ^ "_first_el"), simp_att), [first_el]) ||>> + Local_Theory.note + ((Binding.name (tyname ^ "_last_el"), simp_att), [last_el]) |> snd |> + Local_Theory.exit_global end; +fun check_no_assoc thy s = case get_type thy s of + NONE => () + | SOME _ => error ("Cannot associate a type with " ^ s ^ + "\nsince it is no record or enumeration type"); + +fun check_enum [] [] = NONE + | check_enum els [] = SOME ("has no element(s) " ^ commas els) + | check_enum [] cs = SOME ("has extra element(s) " ^ + commas (map (Long_Name.base_name o fst) cs)) + | check_enum (el :: els) ((cname, _) :: cs) = + if lcase_eq (el, cname) then check_enum els cs + else SOME ("either has no element " ^ el ^ + " or it is at the wrong position"); + fun add_type_def (s, Basic_Type ty) (ids, thy) = - (ids, - Typedecl.abbrev_global (Binding.name s, [], NoSyn) - (mk_type thy ty) thy |> snd) + (check_no_assoc thy s; + (ids, + Typedecl.abbrev_global (Binding.name s, [], NoSyn) + (mk_type thy ty) thy |> snd)) - | add_type_def (s, Enum_Type els) (ids, thy) = add_enum_type s els ids thy + | add_type_def (s, Enum_Type els) ((tab, ctxt), thy) = + let + val (thy', tyname) = (case get_type thy s of + NONE => + let + val tyb = Binding.name s; + val tyname = Sign.full_name thy tyb + in + (thy |> + Datatype.add_datatype {strict = true, quiet = true} [s] + [([], tyb, NoSyn, + map (fn s => (Binding.name s, [], NoSyn)) els)] |> snd |> + add_enum_type s tyname, + tyname) + end + | SOME (T as Type (tyname, [])) => + (case Datatype_Data.get_constrs thy tyname of + NONE => assoc_ty_err thy T s "is not a datatype" + | SOME cs => (case check_enum els cs of + NONE => (thy, tyname) + | SOME msg => assoc_ty_err thy T s msg))); + val cs = map Const (the (Datatype_Data.get_constrs thy' tyname)) + in + ((fold (Symtab.update_new o apsnd (rpair s)) (els ~~ cs) tab, + fold Name.declare els ctxt), + thy') + end | add_type_def (s, Array_Type (argtys, resty)) (ids, thy) = - (ids, - Typedecl.abbrev_global (Binding.name s, [], NoSyn) - (foldr1 HOLogic.mk_prodT (map (mk_type thy) argtys) --> - mk_type thy resty) thy |> snd) + (check_no_assoc thy s; + (ids, + Typedecl.abbrev_global (Binding.name s, [], NoSyn) + (foldr1 HOLogic.mk_prodT (map (mk_type thy) argtys) --> + mk_type thy resty) thy |> snd)) | add_type_def (s, Record_Type fldtys) (ids, thy) = (ids, - Record.add_record true ([], Binding.name s) NONE - (maps (fn (flds, ty) => - let val T = mk_type thy ty - in map (fn fld => (Binding.name fld, T, NoSyn)) flds - end) fldtys) thy) + let val fldTs = maps (fn (flds, ty) => + map (rpair (mk_type thy ty)) flds) fldtys + in case get_type thy s of + NONE => + Record.add_record true ([], Binding.name s) NONE + (map (fn (fld, T) => (Binding.name fld, T, NoSyn)) fldTs) thy + | SOME rT => + (case get_record_info thy rT of + NONE => assoc_ty_err thy rT s "is not a record type" + | SOME {fields, ...} => + (case subtract (lcase_eq o pairself fst) fldTs fields of + [] => () + | flds => assoc_ty_err thy rT s ("has extra field(s) " ^ + commas (map (Long_Name.base_name o fst) flds)); + map (fn (fld, T) => + case AList.lookup lcase_eq fields fld of + NONE => assoc_ty_err thy rT s ("has no field " ^ fld) + | SOME U => T = U orelse assoc_ty_err thy rT s + ("has field " ^ + fld ^ " whose type\n" ^ + Syntax.string_of_typ_global thy U ^ + "\ndoes not match declared type\n" ^ + Syntax.string_of_typ_global thy T)) fldTs; + thy)) + end) | add_type_def (s, Pending_Type) (ids, thy) = - (ids, Typedecl.typedecl_global (Binding.name s, [], NoSyn) thy |> snd); + (check_no_assoc thy s; + (ids, Typedecl.typedecl_global (Binding.name s, [], NoSyn) thy |> snd)); fun term_of_expr thy types funs pfuns = @@ -323,17 +440,16 @@ (case try (unprefix "fld_") s of SOME fname => (case es of [e] => - let val (t, rcdty) = tm_of vs e - in case lookup types rcdty of - SOME (Record_Type fldtys) => - (case get_first (fn (flds, fldty) => - if member (op =) flds fname then SOME fldty - else NONE) fldtys of - SOME fldty => - (Const (mk_qual_name thy rcdty fname, - mk_type thy rcdty --> mk_type thy fldty) $ t, - fldty) - | NONE => error ("Record " ^ rcdty ^ + let + val (t, rcdty) = tm_of vs e; + val rT = mk_type thy rcdty + in case (get_record_info thy rT, lookup types rcdty) of + (SOME {fields, ...}, SOME (Record_Type fldtys)) => + (case (find_field fname fields, + find_field' fname fldtys) of + (SOME (fname', fT), SOME fldty) => + (Const (fname', rT --> fT) $ t, fldty) + | _ => error ("Record " ^ rcdty ^ " has no field named " ^ fname)) | _ => error (rcdty ^ " is not a record type") end @@ -349,20 +465,20 @@ val rT = mk_type thy rcdty; val (u, fldty) = tm_of vs e'; val fT = mk_type thy fldty - in case lookup types rcdty of - SOME (Record_Type fldtys) => - (case get_first (fn (flds, fldty) => - if member (op =) flds fname then SOME fldty - else NONE) fldtys of - SOME fldty' => - if fldty = fldty' then - (Const (mk_qual_name thy rcdty (fname ^ "_update"), + in case get_record_info thy rT of + SOME {fields, ...} => + (case find_field fname fields of + SOME (fname', fU) => + if fT = fU then + (Const (fname' ^ "_update", (fT --> fT) --> rT --> rT) $ Abs ("x", fT, u) $ t, rcdty) - else error ("Type " ^ fldty ^ - " does not match type " ^ fldty' ^ " of field " ^ - fname) + else error ("Type\n" ^ + Syntax.string_of_typ_global thy fT ^ + "\ndoes not match type\n" ^ + Syntax.string_of_typ_global thy fU ^ + "\nof field " ^ fname) | NONE => error ("Record " ^ rcdty ^ " has no field named " ^ fname)) | _ => error (rcdty ^ " is not a record type") @@ -431,34 +547,35 @@ end | tm_of vs (Record (s, flds)) = - (case lookup types s of - SOME (Record_Type fldtys) => - let - val flds' = map (apsnd (tm_of vs)) flds; - val fnames = maps fst fldtys; - val fnames' = map fst flds; - val (fvals, ftys) = split_list (map (fn s' => - case AList.lookup (op =) flds' s' of - SOME fval_ty => fval_ty - | NONE => error ("Field " ^ s' ^ " missing in record " ^ s)) - fnames); - val _ = (case subtract (op =) fnames fnames' of - [] => () - | xs => error ("Extra field(s) " ^ commas xs ^ - " in record " ^ s)); - val _ = (case duplicates (op =) fnames' of - [] => () - | xs => error ("Duplicate field(s) " ^ commas xs ^ - " in record " ^ s)) - in - (list_comb - (Const (mk_qual_name thy s (s ^ "_ext"), - map (mk_type thy) ftys @ [HOLogic.unitT] ---> - mk_type thy s), - fvals @ [HOLogic.unit]), - s) - end - | _ => error (s ^ " is not a record type")) + let + val T = mk_type thy s; + val {extension = (ext_name, _), fields, ...} = + (case get_record_info thy T of + NONE => error (s ^ " is not a record type") + | SOME info => info); + val flds' = map (apsnd (tm_of vs)) flds; + val fnames = map (Long_Name.base_name o fst) fields; + val fnames' = map fst flds; + val (fvals, ftys) = split_list (map (fn s' => + case AList.lookup lcase_eq flds' s' of + SOME fval_ty => fval_ty + | NONE => error ("Field " ^ s' ^ " missing in record " ^ s)) + fnames); + val _ = (case subtract lcase_eq fnames fnames' of + [] => () + | xs => error ("Extra field(s) " ^ commas xs ^ + " in record " ^ s)); + val _ = (case duplicates (op =) fnames' of + [] => () + | xs => error ("Duplicate field(s) " ^ commas xs ^ + " in record " ^ s)) + in + (list_comb + (Const (ext_name, + map (mk_type thy) ftys @ [HOLogic.unitT] ---> T), + fvals @ [HOLogic.unit]), + s) + end | tm_of vs (Array (s, default, assocs)) = (case lookup types s of @@ -592,44 +709,15 @@ (** the VC store **) -fun err_unfinished () = error "An unfinished SPARK environment is still open." - fun err_vcs names = error (Pretty.string_of (Pretty.big_list "The following verification conditions have not been proved:" (map Pretty.str names))) -val strip_number = pairself implode o take_suffix Fdl_Lexer.is_digit o raw_explode; - -val name_ord = prod_ord string_ord (option_ord int_ord) o - pairself (strip_number ##> Int.fromString); - -structure VCtab = Table(type key = string val ord = name_ord); - -structure VCs = Theory_Data -( - type T = - {pfuns: ((string list * string) option * term) Symtab.table, - env: - {ctxt: Element.context_i list, - defs: (binding * thm) list, - types: fdl_type tab, - funs: (string list * string) tab, - ids: (term * string) Symtab.table * Name.context, - proving: bool, - vcs: (string * thm list option * - (string * expr) list * (string * expr) list) VCtab.table, - path: Path.T} option} - val empty : T = {pfuns = Symtab.empty, env = NONE} - val extend = I - fun merge ({pfuns = pfuns1, env = NONE}, {pfuns = pfuns2, env = NONE}) = - {pfuns = Symtab.merge (eq_pair (op =) (op aconv)) (pfuns1, pfuns2), - env = NONE} - | merge _ = err_unfinished () -) - fun set_env (env as {funs, ...}) thy = VCs.map (fn - {pfuns, env = NONE} => - {pfuns = check_pfuns_types thy funs pfuns, env = SOME env} + {pfuns, type_map, env = NONE} => + {pfuns = check_pfuns_types thy funs pfuns, + type_map = type_map, + env = SOME env} | _ => err_unfinished ()) thy; fun mk_pat s = (case Int.fromString s of @@ -672,28 +760,60 @@ fun add_proof_fun prep (s, (optty, raw_t)) thy = VCs.map (fn {env = SOME {proving = true, ...}, ...} => err_unfinished () - | {pfuns, env} => + | {pfuns, type_map, env} => let val optty' = (case env of SOME {funs, ...} => lookup funs s | NONE => NONE); val optty'' = NONE |> upd_option optty |> upd_option optty'; - val t = prep (Option.map (pfun_type thy) optty'') raw_t + val t = prep (Option.map (pfun_type thy) optty'') raw_t; + val _ = (case fold_aterms (fn u => + if is_Var u orelse is_Free u then insert (op =) u else I) t [] of + [] => () + | ts => error ("Term\n" ^ Syntax.string_of_term_global thy t ^ + "\nto be associated with proof function " ^ s ^ + " contains free variable(s) " ^ + commas (map (Syntax.string_of_term_global thy) ts))); in (check_pfun_type thy s t optty optty'; if is_some optty'' orelse is_none env then {pfuns = Symtab.update_new (s, (optty'', t)) pfuns, + type_map = type_map, env = env} handle Symtab.DUP _ => error ("Proof function " ^ s ^ " already associated with function") else error ("Undeclared proof function " ^ s)) end) thy; +fun add_type (s, T as Type (tyname, Ts)) thy = + thy |> + VCs.map (fn + {env = SOME _, ...} => err_unfinished () + | {pfuns, type_map, env} => + {pfuns = pfuns, + type_map = Symtab.update_new (s, T) type_map, + env = env} + handle Symtab.DUP _ => error ("SPARK type " ^ s ^ + " already associated with type")) |> + (fn thy' => + case Datatype_Data.get_constrs thy' tyname of + NONE => thy' + | SOME cs => + if null Ts then + (map + (fn (_, Type (_, [])) => () + | (cname, _) => assoc_ty_err thy T s + ("has illegal constructor " ^ + Long_Name.base_name cname)) cs; + add_enum_type s tyname thy') + else assoc_ty_err thy T s "is illegal") + | add_type (s, T) thy = assoc_ty_err thy T s "is illegal"; + val is_closed = is_none o #env o VCs.get; fun lookup_vc thy name = (case VCs.get thy of - {env = SOME {vcs, types, funs, ids, ctxt, ...}, pfuns} => + {env = SOME {vcs, types, funs, ids, ctxt, ...}, pfuns, ...} => (case VCtab.lookup vcs name of SOME vc => let val (pfuns', ctxt', ids') = @@ -703,7 +823,7 @@ | _ => NONE); fun get_vcs thy = (case VCs.get thy of - {env = SOME {vcs, types, funs, ids, ctxt, defs, ...}, pfuns} => + {env = SOME {vcs, types, funs, ids, ctxt, defs, ...}, pfuns, ...} => let val (pfuns', ctxt', ids') = declare_missing_pfuns thy funs pfuns vcs ids in @@ -714,8 +834,10 @@ | _ => ([], [], [])); fun mark_proved name thms = VCs.map (fn - {pfuns, env = SOME {ctxt, defs, types, funs, ids, vcs, path, ...}} => + {pfuns, type_map, + env = SOME {ctxt, defs, types, funs, ids, vcs, path, ...}} => {pfuns = pfuns, + type_map = type_map, env = SOME {ctxt = ctxt, defs = defs, types = types, funs = funs, ids = ids, proving = true, @@ -724,18 +846,21 @@ path = path}} | x => x); -fun close thy = VCs.map (fn - {pfuns, env = SOME {vcs, path, ...}} => - (case VCtab.fold_rev (fn vc as (_, (_, p, _, _)) => - (if is_some p then apfst else apsnd) (cons vc)) vcs ([], []) of - (proved, []) => - (Thm.join_proofs (maps (the o #2 o snd) proved); - File.write (Path.ext "prv" path) - (concat (map (fn (s, _) => snd (strip_number s) ^ - " -- proved by " ^ Distribution.version ^ "\n") proved)); - {pfuns = pfuns, env = NONE}) - | (_, unproved) => err_vcs (map fst unproved)) - | x => x) thy; +fun close thy = + thy |> + VCs.map (fn + {pfuns, type_map, env = SOME {vcs, path, ...}} => + (case VCtab.fold_rev (fn vc as (_, (_, p, _, _)) => + (if is_some p then apfst else apsnd) (cons vc)) vcs ([], []) of + (proved, []) => + (Thm.join_proofs (maps (the o #2 o snd) proved); + File.write (Path.ext "prv" path) + (concat (map (fn (s, _) => snd (strip_number s) ^ + " -- proved by " ^ Distribution.version ^ "\n") proved)); + {pfuns = pfuns, type_map = type_map, env = NONE}) + | (_, unproved) => err_vcs (map fst unproved)) + | _ => error "No SPARK environment is currently open") |> + Sign.parent_path; (** set up verification conditions **) @@ -822,7 +947,8 @@ (remove (op =) d defs) (d :: sdefs) | NONE => error ("Bad definitions: " ^ rulenames defs)); -fun set_vcs ({types, vars, consts, funs} : decls) (rules, _) vcs path thy = +fun set_vcs ({types, vars, consts, funs} : decls) + (rules, _) ((_, ident), vcs) path thy = let val {pfuns, ...} = VCs.get thy; val (defs, rules') = partition_opt dest_def rules; @@ -847,7 +973,8 @@ ((Symtab.empty |> Symtab.update ("false", (HOLogic.false_const, booleanN)) |> Symtab.update ("true", (HOLogic.true_const, booleanN)), - Name.context), thy) |> + Name.context), + thy |> Sign.add_path (Long_Name.base_name ident)) |> fold add_type_def (items types) |> fold (snd oo add_const) consts' |> (fn ids_thy as ((tab, _), _) => ids_thy |>