src/Pure/sorts.ML
changeset 47005 421760a1efe7
parent 46614 165886a4fe64
child 48272 db75b4005d9a
     1.1 --- a/src/Pure/sorts.ML	Sun Mar 18 12:51:44 2012 +0100
     1.2 +++ b/src/Pure/sorts.ML	Sun Mar 18 13:04:22 2012 +0100
     1.3 @@ -38,15 +38,15 @@
     1.4    val minimize_sort: algebra -> sort -> sort
     1.5    val complete_sort: algebra -> sort -> sort
     1.6    val minimal_sorts: algebra -> sort list -> sort Ord_List.T
     1.7 -  val add_class: Proof.context -> class * class list -> algebra -> algebra
     1.8 -  val add_classrel: Proof.context -> class * class -> algebra -> algebra
     1.9 -  val add_arities: Proof.context -> string * (class * sort list) list -> algebra -> algebra
    1.10 +  val add_class: Context.pretty -> class * class list -> algebra -> algebra
    1.11 +  val add_classrel: Context.pretty -> class * class -> algebra -> algebra
    1.12 +  val add_arities: Context.pretty -> string * (class * sort list) list -> algebra -> algebra
    1.13    val empty_algebra: algebra
    1.14 -  val merge_algebra: Proof.context -> algebra * algebra -> algebra
    1.15 -  val subalgebra: Proof.context -> (class -> bool) -> (class * string -> sort list option)
    1.16 +  val merge_algebra: Context.pretty -> algebra * algebra -> algebra
    1.17 +  val subalgebra: Context.pretty -> (class -> bool) -> (class * string -> sort list option)
    1.18      -> algebra -> (sort -> sort) * algebra
    1.19    type class_error
    1.20 -  val class_error: Proof.context -> class_error -> string
    1.21 +  val class_error: Context.pretty -> class_error -> string
    1.22    exception CLASS_ERROR of class_error
    1.23    val mg_domain: algebra -> string -> sort -> sort list   (*exception CLASS_ERROR*)
    1.24    val meet_sort: algebra -> typ * sort
    1.25 @@ -187,16 +187,16 @@
    1.26  
    1.27  fun err_dup_class c = error ("Duplicate declaration of class: " ^ quote c);
    1.28  
    1.29 -fun err_cyclic_classes ctxt css =
    1.30 +fun err_cyclic_classes pp css =
    1.31    error (cat_lines (map (fn cs =>
    1.32 -    "Cycle in class relation: " ^ Syntax.string_of_classrel ctxt cs) css));
    1.33 +    "Cycle in class relation: " ^ Syntax.string_of_classrel (Syntax.init_pretty pp) cs) css));
    1.34  
    1.35 -fun add_class ctxt (c, cs) = map_classes (fn classes =>
    1.36 +fun add_class pp (c, cs) = map_classes (fn classes =>
    1.37    let
    1.38      val classes' = classes |> Graph.new_node (c, serial ())
    1.39        handle Graph.DUP dup => err_dup_class dup;
    1.40      val classes'' = classes' |> fold Graph.add_edge_trans_acyclic (map (pair c) cs)
    1.41 -      handle Graph.CYCLES css => err_cyclic_classes ctxt css;
    1.42 +      handle Graph.CYCLES css => err_cyclic_classes pp css;
    1.43    in classes'' end);
    1.44  
    1.45  
    1.46 @@ -207,12 +207,14 @@
    1.47  fun for_classes _ NONE = ""
    1.48    | for_classes ctxt (SOME (c1, c2)) = " for classes " ^ Syntax.string_of_classrel ctxt [c1, c2];
    1.49  
    1.50 -fun err_conflict ctxt t cc (c, Ss) (c', Ss') =
    1.51 -  error ("Conflict of type arities" ^ for_classes ctxt cc ^ ":\n  " ^
    1.52 -    Syntax.string_of_arity ctxt (t, Ss, [c]) ^ " and\n  " ^
    1.53 -    Syntax.string_of_arity ctxt (t, Ss', [c']));
    1.54 +fun err_conflict pp t cc (c, Ss) (c', Ss') =
    1.55 +  let val ctxt = Syntax.init_pretty pp in
    1.56 +    error ("Conflict of type arities" ^ for_classes ctxt cc ^ ":\n  " ^
    1.57 +      Syntax.string_of_arity ctxt (t, Ss, [c]) ^ " and\n  " ^
    1.58 +      Syntax.string_of_arity ctxt (t, Ss', [c']))
    1.59 +  end;
    1.60  
    1.61 -fun coregular ctxt algebra t (c, Ss) ars =
    1.62 +fun coregular pp algebra t (c, Ss) ars =
    1.63    let
    1.64      fun conflict (c', Ss') =
    1.65        if class_le algebra (c, c') andalso not (sorts_le algebra (Ss, Ss')) then
    1.66 @@ -222,62 +224,62 @@
    1.67        else NONE;
    1.68    in
    1.69      (case get_first conflict ars of
    1.70 -      SOME ((c1, c2), (c', Ss')) => err_conflict ctxt t (SOME (c1, c2)) (c, Ss) (c', Ss')
    1.71 +      SOME ((c1, c2), (c', Ss')) => err_conflict pp t (SOME (c1, c2)) (c, Ss) (c', Ss')
    1.72      | NONE => (c, Ss) :: ars)
    1.73    end;
    1.74  
    1.75  fun complete algebra (c, Ss) = map (rpair Ss) (c :: super_classes algebra c);
    1.76  
    1.77 -fun insert ctxt algebra t (c, Ss) ars =
    1.78 +fun insert pp algebra t (c, Ss) ars =
    1.79    (case AList.lookup (op =) ars c of
    1.80 -    NONE => coregular ctxt algebra t (c, Ss) ars
    1.81 +    NONE => coregular pp algebra t (c, Ss) ars
    1.82    | SOME Ss' =>
    1.83        if sorts_le algebra (Ss, Ss') then ars
    1.84        else if sorts_le algebra (Ss', Ss)
    1.85 -      then coregular ctxt algebra t (c, Ss) (remove (op =) (c, Ss') ars)
    1.86 -      else err_conflict ctxt t NONE (c, Ss) (c, Ss'));
    1.87 +      then coregular pp algebra t (c, Ss) (remove (op =) (c, Ss') ars)
    1.88 +      else err_conflict pp t NONE (c, Ss) (c, Ss'));
    1.89  
    1.90  in
    1.91  
    1.92 -fun insert_ars ctxt algebra t = fold_rev (insert ctxt algebra t);
    1.93 +fun insert_ars pp algebra t = fold_rev (insert pp algebra t);
    1.94  
    1.95 -fun insert_complete_ars ctxt algebra (t, ars) arities =
    1.96 +fun insert_complete_ars pp algebra (t, ars) arities =
    1.97    let val ars' =
    1.98      Symtab.lookup_list arities t
    1.99 -    |> fold_rev (insert_ars ctxt algebra t) (map (complete algebra) ars);
   1.100 +    |> fold_rev (insert_ars pp algebra t) (map (complete algebra) ars);
   1.101    in Symtab.update (t, ars') arities end;
   1.102  
   1.103 -fun add_arities ctxt arg algebra =
   1.104 -  algebra |> map_arities (insert_complete_ars ctxt algebra arg);
   1.105 +fun add_arities pp arg algebra =
   1.106 +  algebra |> map_arities (insert_complete_ars pp algebra arg);
   1.107  
   1.108 -fun add_arities_table ctxt algebra =
   1.109 -  Symtab.fold (fn (t, ars) => insert_complete_ars ctxt algebra (t, ars));
   1.110 +fun add_arities_table pp algebra =
   1.111 +  Symtab.fold (fn (t, ars) => insert_complete_ars pp algebra (t, ars));
   1.112  
   1.113  end;
   1.114  
   1.115  
   1.116  (* classrel *)
   1.117  
   1.118 -fun rebuild_arities ctxt algebra = algebra |> map_arities (fn arities =>
   1.119 +fun rebuild_arities pp algebra = algebra |> map_arities (fn arities =>
   1.120    Symtab.empty
   1.121 -  |> add_arities_table ctxt algebra arities);
   1.122 +  |> add_arities_table pp algebra arities);
   1.123  
   1.124 -fun add_classrel ctxt rel = rebuild_arities ctxt o map_classes (fn classes =>
   1.125 +fun add_classrel pp rel = rebuild_arities pp o map_classes (fn classes =>
   1.126    classes |> Graph.add_edge_trans_acyclic rel
   1.127 -    handle Graph.CYCLES css => err_cyclic_classes ctxt css);
   1.128 +    handle Graph.CYCLES css => err_cyclic_classes pp css);
   1.129  
   1.130  
   1.131  (* empty and merge *)
   1.132  
   1.133  val empty_algebra = make_algebra (Graph.empty, Symtab.empty);
   1.134  
   1.135 -fun merge_algebra ctxt
   1.136 +fun merge_algebra pp
   1.137     (Algebra {classes = classes1, arities = arities1},
   1.138      Algebra {classes = classes2, arities = arities2}) =
   1.139    let
   1.140      val classes' = Graph.merge_trans_acyclic (op =) (classes1, classes2)
   1.141        handle Graph.DUP c => err_dup_class c
   1.142 -        | Graph.CYCLES css => err_cyclic_classes ctxt css;
   1.143 +        | Graph.CYCLES css => err_cyclic_classes pp css;
   1.144      val algebra0 = make_algebra (classes', Symtab.empty);
   1.145      val arities' =
   1.146        (case (pointer_eq (classes1, classes2), pointer_eq (arities1, arities2)) of
   1.147 @@ -285,20 +287,20 @@
   1.148        | (true, false) =>  (*no completion*)
   1.149            (arities1, arities2) |> Symtab.join (fn t => fn (ars1, ars2) =>
   1.150              if pointer_eq (ars1, ars2) then raise Symtab.SAME
   1.151 -            else insert_ars ctxt algebra0 t ars2 ars1)
   1.152 +            else insert_ars pp algebra0 t ars2 ars1)
   1.153        | (false, true) =>  (*unary completion*)
   1.154            Symtab.empty
   1.155 -          |> add_arities_table ctxt algebra0 arities1
   1.156 +          |> add_arities_table pp algebra0 arities1
   1.157        | (false, false) => (*binary completion*)
   1.158            Symtab.empty
   1.159 -          |> add_arities_table ctxt algebra0 arities1
   1.160 -          |> add_arities_table ctxt algebra0 arities2);
   1.161 +          |> add_arities_table pp algebra0 arities1
   1.162 +          |> add_arities_table pp algebra0 arities2);
   1.163    in make_algebra (classes', arities') end;
   1.164  
   1.165  
   1.166  (* algebra projections *)  (* FIXME potentially violates abstract type integrity *)
   1.167  
   1.168 -fun subalgebra ctxt P sargs (algebra as Algebra {classes, arities}) =
   1.169 +fun subalgebra pp P sargs (algebra as Algebra {classes, arities}) =
   1.170    let
   1.171      val restrict_sort = minimize_sort algebra o filter P o Graph.all_succs classes;
   1.172      fun restrict_arity t (c, Ss) =
   1.173 @@ -310,7 +312,7 @@
   1.174        else NONE;
   1.175      val classes' = classes |> Graph.restrict P;
   1.176      val arities' = arities |> Symtab.map (map_filter o restrict_arity);
   1.177 -  in (restrict_sort, rebuild_arities ctxt (make_algebra (classes', arities'))) end;
   1.178 +  in (restrict_sort, rebuild_arities pp (make_algebra (classes', arities'))) end;
   1.179  
   1.180  
   1.181  
   1.182 @@ -323,13 +325,14 @@
   1.183    No_Arity of string * class |
   1.184    No_Subsort of sort * sort;
   1.185  
   1.186 -fun class_error ctxt (No_Classrel (c1, c2)) =
   1.187 -      "No class relation " ^ Syntax.string_of_classrel ctxt [c1, c2]
   1.188 -  | class_error ctxt (No_Arity (a, c)) =
   1.189 -      "No type arity " ^ Syntax.string_of_arity ctxt (a, [], [c])
   1.190 -  | class_error ctxt (No_Subsort (S1, S2)) =
   1.191 -      "Cannot derive subsort relation " ^
   1.192 -        Syntax.string_of_sort ctxt S1 ^ " < " ^ Syntax.string_of_sort ctxt S2;
   1.193 +fun class_error pp =
   1.194 +  let val ctxt = Syntax.init_pretty pp in
   1.195 +    fn No_Classrel (c1, c2) => "No class relation " ^ Syntax.string_of_classrel ctxt [c1, c2]
   1.196 +     | No_Arity (a, c) => "No type arity " ^ Syntax.string_of_arity ctxt (a, [], [c])
   1.197 +     | No_Subsort (S1, S2) =>
   1.198 +        "Cannot derive subsort relation " ^
   1.199 +          Syntax.string_of_sort ctxt S1 ^ " < " ^ Syntax.string_of_sort ctxt S2
   1.200 +  end;
   1.201  
   1.202  exception CLASS_ERROR of class_error;
   1.203