src/HOL/SPARK/Tools/spark_vcs.ML
changeset 48453 2421ff8c57a5
parent 48167 da1a1eae93fa
child 50126 3dec88149176
equal deleted inserted replaced
48431:6efff142bb54 48453:2421ff8c57a5
  1065          SOME d => sort_defs prfx funs pfuns consts
  1065          SOME d => sort_defs prfx funs pfuns consts
  1066            (remove (op =) d defs) (d :: sdefs)
  1066            (remove (op =) d defs) (d :: sdefs)
  1067        | NONE => error ("Bad definitions: " ^ rulenames defs));
  1067        | NONE => error ("Bad definitions: " ^ rulenames defs));
  1068 
  1068 
  1069 fun set_vcs ({types, vars, consts, funs} : decls)
  1069 fun set_vcs ({types, vars, consts, funs} : decls)
  1070       (rules, _) ((_, ident), vcs) path prfx thy =
  1070       (rules, _) ((_, ident), vcs) path opt_prfx thy =
  1071   let
  1071   let
       
  1072     val prfx' =
       
  1073       if opt_prfx = "" then
       
  1074         space_implode "__" (Long_Name.explode (Long_Name.qualifier ident))
       
  1075       else opt_prfx;
       
  1076     val prfx = to_lower prfx';
  1072     val {pfuns, ...} = VCs.get thy;
  1077     val {pfuns, ...} = VCs.get thy;
  1073     val (defs, rules') = partition_opt dest_def rules;
  1078     val (defs, rules') = partition_opt dest_def rules;
  1074     val consts' =
  1079     val consts' =
  1075       subtract (fn ((_, (s, _)), (s', _)) => s = s') defs (items consts);
  1080       subtract (fn ((_, (s, _)), (s', _)) => s = s') defs (items consts);
  1076     (* ignore all complex rules in rls files *)
  1081     (* ignore all complex rules in rls files *)
  1092       ((Symtab.empty |>
  1097       ((Symtab.empty |>
  1093         Symtab.update ("false", (@{term False}, booleanN)) |>
  1098         Symtab.update ("false", (@{term False}, booleanN)) |>
  1094         Symtab.update ("true", (@{term True}, booleanN)),
  1099         Symtab.update ("true", (@{term True}, booleanN)),
  1095         Name.context),
  1100         Name.context),
  1096        thy |> Sign.add_path
  1101        thy |> Sign.add_path
  1097          ((if prfx = "" then "" else prfx ^ "__") ^ Long_Name.base_name ident)) |>
  1102          ((if prfx' = "" then "" else prfx' ^ "__") ^ Long_Name.base_name ident)) |>
  1098       fold (add_type_def prfx) (items types) |>
  1103       fold (add_type_def prfx) (items types) |>
  1099       fold (snd oo add_const prfx) consts' |> (fn ids_thy as ((tab, _), _) =>
  1104       fold (snd oo add_const prfx) consts' |> (fn ids_thy as ((tab, _), _) =>
  1100         ids_thy |>
  1105         ids_thy |>
  1101         fold_map (add_def prfx types pfuns consts)
  1106         fold_map (add_def prfx types pfuns consts)
  1102           (sort_defs prfx funs pfuns (Symtab.defined tab) defs []) ||>>
  1107           (sort_defs prfx funs pfuns (Symtab.defined tab) defs []) ||>>