added class_error and exception CLASS_ERROR (supercedes DOMAIN);
authorwenzelm
Fri May 05 21:59:46 2006 +0200 (2006-05-05)
changeset 19578f93b7637a5e6
parent 19577 fdb3642feb49
child 19579 b802d1804b77
added class_error and exception CLASS_ERROR (supercedes DOMAIN);
clarified of_class_derivation;
tuned witness_sorts;
src/Pure/sorts.ML
     1.1 --- a/src/Pure/sorts.ML	Fri May 05 21:59:45 2006 +0200
     1.2 +++ b/src/Pure/sorts.ML	Fri May 05 21:59:46 2006 +0200
     1.3 @@ -40,14 +40,15 @@
     1.4    val add_class: Pretty.pp -> class * class list -> classes -> classes
     1.5    val add_classrel: Pretty.pp -> class * class -> classes -> classes
     1.6    val merge_classes: Pretty.pp -> classes * classes -> classes
     1.7 -  exception DOMAIN of string * class
     1.8 -  val domain_error: Pretty.pp -> string * class -> 'a
     1.9 -  val mg_domain: classes * arities -> string -> sort -> sort list  (*exception DOMAIN*)
    1.10 +  type class_error
    1.11 +  val class_error: Pretty.pp -> class_error -> 'a
    1.12 +  exception CLASS_ERROR of class_error
    1.13 +  val mg_domain: classes * arities -> string -> sort -> sort list   (*exception CLASS_ERROR*)
    1.14    val of_sort: classes * arities -> typ * sort -> bool
    1.15    val of_sort_derivation: Pretty.pp -> classes * arities ->
    1.16      {classrel: 'a * class -> class -> 'a,
    1.17       constructor: string -> ('a * class) list list -> class -> 'a,
    1.18 -     variable: typ -> ('a * class) list} -> typ * sort -> 'a list
    1.19 +     variable: typ -> ('a * class) list} -> typ * sort -> 'a list   (*exception CLASS_ERROR*)
    1.20    val witness_sorts: classes * arities -> string list ->
    1.21      sort list -> sort list -> (typ * sort) list
    1.22  end;
    1.23 @@ -245,18 +246,25 @@
    1.24  
    1.25  (** sorts of types **)
    1.26  
    1.27 -(* mg_domain *)
    1.28 +(* errors *)
    1.29 +
    1.30 +datatype class_error = NoClassrel of class * class | NoArity of string * class;
    1.31  
    1.32 -exception DOMAIN of string * class;
    1.33 +fun class_error pp (NoClassrel (c1, c2)) =
    1.34 +      error ("No class relation " ^ Pretty.string_of_classrel pp [c1, c2])
    1.35 +  | class_error pp (NoArity (a, c)) =
    1.36 +      error ("No type arity " ^ Pretty.string_of_arity pp (a, [], [c]));
    1.37  
    1.38 -fun domain_error pp (a, c) =
    1.39 -  error ("No way to get " ^ Pretty.string_of_arity pp (a, [], [c]));
    1.40 +exception CLASS_ERROR of class_error;
    1.41 +
    1.42 +
    1.43 +(* mg_domain *)
    1.44  
    1.45  fun mg_domain (classes, arities) a S =
    1.46    let
    1.47      fun dom c =
    1.48        (case AList.lookup (op =) (Symtab.lookup_list arities a) c of
    1.49 -        NONE => raise DOMAIN (a, c)
    1.50 +        NONE => raise CLASS_ERROR (NoArity (a, c))
    1.51        | SOME (_, Ss) => Ss);
    1.52      fun dom_inter c Ss = ListPair.map (inter_sort classes) (dom c, Ss);
    1.53    in
    1.54 @@ -276,7 +284,7 @@
    1.55        | ofS (Type (a, Ts), S) =
    1.56            let val Ss = mg_domain (classes, arities) a S in
    1.57              ListPair.all ofS (Ts, Ss)
    1.58 -          end handle DOMAIN _ => false;
    1.59 +          end handle CLASS_ERROR _ => false;
    1.60    in ofS end;
    1.61  
    1.62  
    1.63 @@ -284,7 +292,13 @@
    1.64  
    1.65  fun of_sort_derivation pp (classes, arities) {classrel, constructor, variable} =
    1.66    let
    1.67 -    fun weaken (x, c1) c2 = if c1 = c2 then x else classrel (x, c1) c2;
    1.68 +    fun weaken_path (x, c1 :: c2 :: cs) = weaken_path (classrel (x, c1) c2, c2 :: cs)
    1.69 +      | weaken_path (x, _) = x;
    1.70 +    fun weaken (x, c1) c2 =
    1.71 +      (case Graph.irreducible_paths classes (c1, c2) of
    1.72 +        [] => raise CLASS_ERROR (NoClassrel (c1, c2))
    1.73 +      | cs :: _ => weaken_path (x, cs));
    1.74 +
    1.75      fun weakens S1 S2 = S2 |> map (fn c2 =>
    1.76        (case S1 |> find_first (fn (_, c1) => class_le classes (c1, c2)) of
    1.77          SOME d1 => weaken d1 c2
    1.78 @@ -294,8 +308,7 @@
    1.79      fun derive _ [] = []
    1.80        | derive (Type (a, Ts)) S =
    1.81            let
    1.82 -            val Ss = mg_domain (classes, arities) a S
    1.83 -              handle DOMAIN d => domain_error pp d;
    1.84 +            val Ss = mg_domain (classes, arities) a S;
    1.85              val dom = map2 (fn T => fn S => derive T S ~~ S) Ts Ss;
    1.86            in
    1.87              S |> map (fn c =>
    1.88 @@ -310,60 +323,46 @@
    1.89  
    1.90  (* witness_sorts *)
    1.91  
    1.92 -local
    1.93 -
    1.94 -fun witness_aux (classes, arities) log_types hyps sorts =
    1.95 +fun witness_sorts (classes, arities) log_types hyps sorts =
    1.96    let
    1.97 -    val top_witn = (propT, []);
    1.98      fun le S1 S2 = sort_le classes (S1, S2);
    1.99      fun get_solved S2 (T, S1) = if le S1 S2 then SOME (T, S2) else NONE;
   1.100      fun get_hyp S2 S1 = if le S1 S2 then SOME (TFree ("'hyp", S1), S2) else NONE;
   1.101 -    fun mg_dom t S = SOME (mg_domain (classes, arities) t S) handle DOMAIN _ => NONE;
   1.102 +    fun mg_dom t S = SOME (mg_domain (classes, arities) t S) handle CLASS_ERROR _ => NONE;
   1.103  
   1.104 -    fun witn_sort _ (solved_failed, []) = (solved_failed, SOME top_witn)
   1.105 -      | witn_sort path ((solved, failed), S) =
   1.106 -          if exists (le S) failed then ((solved, failed), NONE)
   1.107 +    fun witn_sort _ [] solved_failed = (SOME (propT, []), solved_failed)
   1.108 +      | witn_sort path S (solved, failed) =
   1.109 +          if exists (le S) failed then (NONE, (solved, failed))
   1.110            else
   1.111              (case get_first (get_solved S) solved of
   1.112 -              SOME w => ((solved, failed), SOME w)
   1.113 +              SOME w => (SOME w, (solved, failed))
   1.114              | NONE =>
   1.115                  (case get_first (get_hyp S) hyps of
   1.116 -                  SOME w => ((w :: solved, failed), SOME w)
   1.117 -                | NONE => witn_types path log_types ((solved, failed), S)))
   1.118 +                  SOME w => (SOME w, (w :: solved, failed))
   1.119 +                | NONE => witn_types path log_types S (solved, failed)))
   1.120  
   1.121 -    and witn_sorts path x = foldl_map (witn_sort path) x
   1.122 +    and witn_sorts path x = fold_map (witn_sort path) x
   1.123  
   1.124 -    and witn_types _ [] ((solved, failed), S) = ((solved, S :: failed), NONE)
   1.125 -      | witn_types path (t :: ts) (solved_failed, S) =
   1.126 +    and witn_types _ [] S (solved, failed) = (NONE, (solved, S :: failed))
   1.127 +      | witn_types path (t :: ts) S solved_failed =
   1.128            (case mg_dom t S of
   1.129              SOME SS =>
   1.130                (*do not descend into stronger args (achieving termination)*)
   1.131                if exists (fn D => le D S orelse exists (le D) path) SS then
   1.132 -                witn_types path ts (solved_failed, S)
   1.133 +                witn_types path ts S solved_failed
   1.134                else
   1.135 -                let val ((solved', failed'), ws) = witn_sorts (S :: path) (solved_failed, SS) in
   1.136 +                let val (ws, (solved', failed')) = witn_sorts (S :: path) SS solved_failed in
   1.137                    if forall is_some ws then
   1.138                      let val w = (Type (t, map (#1 o the) ws), S)
   1.139 -                    in ((w :: solved', failed'), SOME w) end
   1.140 -                  else witn_types path ts ((solved', failed'), S)
   1.141 +                    in (SOME w, (w :: solved', failed')) end
   1.142 +                  else witn_types path ts S (solved', failed')
   1.143                  end
   1.144 -          | NONE => witn_types path ts (solved_failed, S));
   1.145 -
   1.146 -  in witn_sorts [] (([], []), sorts) end;
   1.147 -
   1.148 -fun str_of_sort [c] = c
   1.149 -  | str_of_sort cs = enclose "{" "}" (commas cs);
   1.150 +          | NONE => witn_types path ts S solved_failed);
   1.151  
   1.152 -in
   1.153 +    fun double_check TS =
   1.154 +      if of_sort (classes, arities) TS then TS
   1.155 +      else sys_error "FIXME Bad sort witness";
   1.156  
   1.157 -fun witness_sorts (classes, arities) log_types hyps sorts =
   1.158 -  let
   1.159 -    fun double_check_result NONE = NONE
   1.160 -      | double_check_result (SOME (T, S)) =
   1.161 -          if of_sort (classes, arities) (T, S) then SOME (T, S)
   1.162 -          else sys_error ("Sorts.witness_sorts: bad witness for sort " ^ str_of_sort S);
   1.163 -  in map_filter double_check_result (#2 (witness_aux (classes, arities) log_types hyps sorts)) end;
   1.164 +  in map_filter (Option.map double_check) (#1 (witn_sorts [] sorts ([], []))) end;
   1.165  
   1.166  end;
   1.167 -
   1.168 -end;