added same idiomatic handling of namings for Ctr_Sugar/BNF-related interpretation hooks as for typedef and (old-style) datatypes
authorblanchet
Thu Apr 03 10:51:24 2014 +0200 (2014-04-03)
changeset 563765a93b8f928a2
parent 56375 32e0da92c786
child 56377 a0c4a162bd13
child 56385 76acce58aeab
added same idiomatic handling of namings for Ctr_Sugar/BNF-related interpretation hooks as for typedef and (old-style) datatypes
src/HOL/Tools/BNF/bnf_def.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_def.ML	Thu Apr 03 10:51:22 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_def.ML	Thu Apr 03 10:51:24 2014 +0200
     1.3 @@ -1315,7 +1315,22 @@
     1.4    val eq: T * T -> bool = op = o pairself T_of_bnf;
     1.5  );
     1.6  
     1.7 -val bnf_interpretation = BNF_Interpretation.interpretation;
     1.8 +fun with_repaired_path f bnf thy =
     1.9 +  let
    1.10 +    val qualifiers =
    1.11 +      (case Binding.dest (name_of_bnf bnf) of
    1.12 +        (* arbitrarily use "Fun" as prefix for "fun"*)
    1.13 +        (_, [], @{type_name fun}) => [(Context.theory_name @{theory Fun}, false)]
    1.14 +      | (_, qs, _) => qs)
    1.15 +  in
    1.16 +    thy
    1.17 +    |> Sign.root_path
    1.18 +    |> fold (uncurry (fn true => Sign.mandatory_path | false => Sign.add_path) o swap) qualifiers
    1.19 +    |> f bnf
    1.20 +    |> Sign.restore_naming thy
    1.21 +  end;
    1.22 +
    1.23 +val bnf_interpretation = BNF_Interpretation.interpretation o with_repaired_path;
    1.24  
    1.25  fun register_bnf key bnf =
    1.26    Local_Theory.declaration {syntax = false, pervasive = true}
     2.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Apr 03 10:51:22 2014 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Apr 03 10:51:24 2014 +0200
     2.3 @@ -190,7 +190,14 @@
     2.4    val eq: T * T -> bool = op = o pairself #T;
     2.5  );
     2.6  
     2.7 -val fp_sugar_interpretation = FP_Sugar_Interpretation.interpretation;
     2.8 +fun with_repaired_path f (fp_sugar as {T, ...} : fp_sugar) thy =
     2.9 +  thy
    2.10 +  |> Sign.root_path
    2.11 +  |> Sign.add_path (Long_Name.qualifier (fst (dest_Type T)))
    2.12 +  |> f fp_sugar
    2.13 +  |> Sign.restore_naming thy;
    2.14 +
    2.15 +val fp_sugar_interpretation = FP_Sugar_Interpretation.interpretation o with_repaired_path;
    2.16  
    2.17  fun register_fp_sugar key fp_sugar =
    2.18    Local_Theory.declaration {syntax = false, pervasive = true}
     3.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Thu Apr 03 10:51:22 2014 +0200
     3.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Thu Apr 03 10:51:24 2014 +0200
     3.3 @@ -158,7 +158,14 @@
     3.4    val eq: T * T -> bool = op = o pairself #ctrs;
     3.5  );
     3.6  
     3.7 -val ctr_sugar_interpretation = Ctr_Sugar_Interpretation.interpretation;
     3.8 +fun with_repaired_path f (ctr_sugar as {ctrs = ctr1 :: _, ...} : ctr_sugar) thy =
     3.9 +  thy
    3.10 +  |> Sign.root_path
    3.11 +  |> Sign.add_path (Long_Name.qualifier (fst (dest_Type (body_type (fastype_of ctr1)))))
    3.12 +  |> f ctr_sugar
    3.13 +  |> Sign.restore_naming thy;
    3.14 +
    3.15 +val ctr_sugar_interpretation = Ctr_Sugar_Interpretation.interpretation o with_repaired_path;
    3.16  
    3.17  fun register_ctr_sugar key ctr_sugar =
    3.18    Local_Theory.declaration {syntax = false, pervasive = true}