improving clash-free naming of variables and preds in code_prolog
authorbulwahn
Tue Aug 31 11:49:15 2010 +0200 (2010-08-31)
changeset 3895808eb0ffa2413
parent 38957 2eb265efa1b0
child 38959 706ab66e3464
improving clash-free naming of variables and preds in code_prolog
src/HOL/Predicate_Compile_Examples/Lambda_Example.thy
src/HOL/Tools/Predicate_Compile/code_prolog.ML
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy	Tue Aug 31 10:51:49 2010 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy	Tue Aug 31 11:49:15 2010 +0200
     1.3 @@ -84,9 +84,9 @@
     1.4  setup {* Code_Prolog.map_code_options (K 
     1.5    { ensure_groundness = true,
     1.6      limited_types = [(@{typ nat}, 1), (@{typ "type"}, 1), (@{typ dB}, 1), (@{typ "type list"}, 1)],
     1.7 -    limited_predicates = [("typing", 2), ("nth_el1", 2)],
     1.8 +    limited_predicates = [("typing", 2), ("nthel1", 2)],
     1.9      replacing = [(("typing", "limited_typing"), "quickcheck"),
    1.10 -                 (("nth_el1", "limited_nth_el1"), "lim_typing")],
    1.11 +                 (("nthel1", "limited_nthel1"), "lim_typing")],
    1.12      prolog_system = Code_Prolog.SWI_PROLOG}) *}
    1.13  
    1.14  lemma
     2.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Tue Aug 31 10:51:49 2010 +0200
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Tue Aug 31 11:49:15 2010 +0200
     2.3 @@ -156,14 +156,14 @@
     2.4  
     2.5  (* translation from introduction rules to internal representation *)
     2.6  
     2.7 -fun mk_conform empty avoid name =
     2.8 +fun mk_conform f empty avoid name =
     2.9    let
    2.10      fun dest_Char (Symbol.Char c) = c
    2.11      val name' = space_implode "" (map (dest_Char o Symbol.decode)
    2.12        (filter (fn s => Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s)
    2.13          (Symbol.explode name)))
    2.14 -    val name'' = if name' = "" then empty else name'
    2.15 -  in Name.variant avoid name'' end
    2.16 +    val name'' = f (if name' = "" then empty else name')
    2.17 +  in (if member (op =) avoid name'' then Name.variant avoid name'' else name'') end
    2.18  
    2.19  (** constant table **)
    2.20  
    2.21 @@ -175,7 +175,7 @@
    2.22      fun update' c table =
    2.23        if AList.defined (op =) table c then table else
    2.24          let
    2.25 -          val c' = first_lower (mk_conform "pred" (map snd table) (Long_Name.base_name c))
    2.26 +          val c' = mk_conform first_lower "pred" (map snd table) (Long_Name.base_name c)
    2.27          in
    2.28            AList.update (op =) (c, c') table
    2.29          end
    2.30 @@ -282,7 +282,8 @@
    2.31          val prems' = Conj (map (translate_prem ensure_groundness ctxt' constant_table') prems)
    2.32          val clause = (dest_Rel (translate_literal ctxt' constant_table' head), prems')
    2.33        in clause end
    2.34 -  in (map translate_intro intros', constant_table') end
    2.35 +    val res = (map translate_intro intros', constant_table')
    2.36 +  in res end
    2.37  
    2.38  fun depending_preds_of (key, intros) =
    2.39    fold Term.add_const_names (map Thm.prop_of intros) []
    2.40 @@ -458,7 +459,7 @@
    2.41    forall (fn s => Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s) (Symbol.explode v)
    2.42    
    2.43  fun mk_renaming v renaming =
    2.44 -  (v, first_upper (mk_conform "var" (map snd renaming) v)) :: renaming
    2.45 +  (v, mk_conform first_upper "Var" (map snd renaming) v) :: renaming
    2.46  
    2.47  fun rename_vars_clause ((rel, args), prem) =
    2.48    let