src/Pure/sorts.ML
changeset 61264 95ede7916178
parent 61262 7bd1eb4b056e
child 62538 85ebb645b1a3
     1.1 --- a/src/Pure/sorts.ML	Fri Sep 25 19:20:24 2015 +0200
     1.2 +++ b/src/Pure/sorts.ML	Fri Sep 25 19:23:17 2015 +0200
     1.3 @@ -188,16 +188,16 @@
     1.4  
     1.5  fun err_dup_class c = error ("Duplicate declaration of class: " ^ quote c);
     1.6  
     1.7 -fun err_cyclic_classes pp css =
     1.8 +fun err_cyclic_classes context css =
     1.9    error (cat_lines (map (fn cs =>
    1.10 -    "Cycle in class relation: " ^ Syntax.string_of_classrel (Syntax.init_pretty pp) cs) css));
    1.11 +    "Cycle in class relation: " ^ Syntax.string_of_classrel (Syntax.init_pretty context) cs) css));
    1.12  
    1.13 -fun add_class pp (c, cs) = map_classes (fn classes =>
    1.14 +fun add_class context (c, cs) = map_classes (fn classes =>
    1.15    let
    1.16      val classes' = classes |> Graph.new_node (c, serial ())
    1.17        handle Graph.DUP dup => err_dup_class dup;
    1.18      val classes'' = classes' |> fold Graph.add_edge_trans_acyclic (map (pair c) cs)
    1.19 -      handle Graph.CYCLES css => err_cyclic_classes pp css;
    1.20 +      handle Graph.CYCLES css => err_cyclic_classes context css;
    1.21    in classes'' end);
    1.22  
    1.23  
    1.24 @@ -208,14 +208,14 @@
    1.25  fun for_classes _ NONE = ""
    1.26    | for_classes ctxt (SOME (c1, c2)) = " for classes " ^ Syntax.string_of_classrel ctxt [c1, c2];
    1.27  
    1.28 -fun err_conflict pp t cc (c, Ss) (c', Ss') =
    1.29 -  let val ctxt = Syntax.init_pretty pp in
    1.30 +fun err_conflict context t cc (c, Ss) (c', Ss') =
    1.31 +  let val ctxt = Syntax.init_pretty context in
    1.32      error ("Conflict of type arities" ^ for_classes ctxt cc ^ ":\n  " ^
    1.33        Syntax.string_of_arity ctxt (t, Ss, [c]) ^ " and\n  " ^
    1.34        Syntax.string_of_arity ctxt (t, Ss', [c']))
    1.35    end;
    1.36  
    1.37 -fun coregular pp algebra t (c, Ss) ars =
    1.38 +fun coregular context algebra t (c, Ss) ars =
    1.39    let
    1.40      fun conflict (c', Ss') =
    1.41        if class_le algebra (c, c') andalso not (sorts_le algebra (Ss, Ss')) then
    1.42 @@ -225,62 +225,62 @@
    1.43        else NONE;
    1.44    in
    1.45      (case get_first conflict ars of
    1.46 -      SOME ((c1, c2), (c', Ss')) => err_conflict pp t (SOME (c1, c2)) (c, Ss) (c', Ss')
    1.47 +      SOME ((c1, c2), (c', Ss')) => err_conflict context t (SOME (c1, c2)) (c, Ss) (c', Ss')
    1.48      | NONE => (c, Ss) :: ars)
    1.49    end;
    1.50  
    1.51  fun complete algebra (c, Ss) = map (rpair Ss) (c :: super_classes algebra c);
    1.52  
    1.53 -fun insert pp algebra t (c, Ss) ars =
    1.54 +fun insert context algebra t (c, Ss) ars =
    1.55    (case AList.lookup (op =) ars c of
    1.56 -    NONE => coregular pp algebra t (c, Ss) ars
    1.57 +    NONE => coregular context algebra t (c, Ss) ars
    1.58    | SOME Ss' =>
    1.59        if sorts_le algebra (Ss, Ss') then ars
    1.60        else if sorts_le algebra (Ss', Ss)
    1.61 -      then coregular pp algebra t (c, Ss) (remove (op =) (c, Ss') ars)
    1.62 -      else err_conflict pp t NONE (c, Ss) (c, Ss'));
    1.63 +      then coregular context algebra t (c, Ss) (remove (op =) (c, Ss') ars)
    1.64 +      else err_conflict context t NONE (c, Ss) (c, Ss'));
    1.65  
    1.66  in
    1.67  
    1.68 -fun insert_ars pp algebra t = fold_rev (insert pp algebra t);
    1.69 +fun insert_ars context algebra t = fold_rev (insert context algebra t);
    1.70  
    1.71 -fun insert_complete_ars pp algebra (t, ars) arities =
    1.72 +fun insert_complete_ars context algebra (t, ars) arities =
    1.73    let val ars' =
    1.74      Symtab.lookup_list arities t
    1.75 -    |> fold_rev (insert_ars pp algebra t) (map (complete algebra) ars);
    1.76 +    |> fold_rev (insert_ars context algebra t) (map (complete algebra) ars);
    1.77    in Symtab.update (t, ars') arities end;
    1.78  
    1.79 -fun add_arities pp arg algebra =
    1.80 -  algebra |> map_arities (insert_complete_ars pp algebra arg);
    1.81 +fun add_arities context arg algebra =
    1.82 +  algebra |> map_arities (insert_complete_ars context algebra arg);
    1.83  
    1.84 -fun add_arities_table pp algebra =
    1.85 -  Symtab.fold (fn (t, ars) => insert_complete_ars pp algebra (t, ars));
    1.86 +fun add_arities_table context algebra =
    1.87 +  Symtab.fold (fn (t, ars) => insert_complete_ars context algebra (t, ars));
    1.88  
    1.89  end;
    1.90  
    1.91  
    1.92  (* classrel *)
    1.93  
    1.94 -fun rebuild_arities pp algebra = algebra |> map_arities (fn arities =>
    1.95 +fun rebuild_arities context algebra = algebra |> map_arities (fn arities =>
    1.96    Symtab.empty
    1.97 -  |> add_arities_table pp algebra arities);
    1.98 +  |> add_arities_table context algebra arities);
    1.99  
   1.100 -fun add_classrel pp rel = rebuild_arities pp o map_classes (fn classes =>
   1.101 +fun add_classrel context rel = rebuild_arities context o map_classes (fn classes =>
   1.102    classes |> Graph.add_edge_trans_acyclic rel
   1.103 -    handle Graph.CYCLES css => err_cyclic_classes pp css);
   1.104 +    handle Graph.CYCLES css => err_cyclic_classes context css);
   1.105  
   1.106  
   1.107  (* empty and merge *)
   1.108  
   1.109  val empty_algebra = make_algebra (Graph.empty, Symtab.empty);
   1.110  
   1.111 -fun merge_algebra pp
   1.112 +fun merge_algebra context
   1.113     (Algebra {classes = classes1, arities = arities1},
   1.114      Algebra {classes = classes2, arities = arities2}) =
   1.115    let
   1.116      val classes' = Graph.merge_trans_acyclic (op =) (classes1, classes2)
   1.117        handle Graph.DUP c => err_dup_class c
   1.118 -        | Graph.CYCLES css => err_cyclic_classes pp css;
   1.119 +        | Graph.CYCLES css => err_cyclic_classes context css;
   1.120      val algebra0 = make_algebra (classes', Symtab.empty);
   1.121      val arities' =
   1.122        (case (pointer_eq (classes1, classes2), pointer_eq (arities1, arities2)) of
   1.123 @@ -288,20 +288,20 @@
   1.124        | (true, false) =>  (*no completion*)
   1.125            (arities1, arities2) |> Symtab.join (fn t => fn (ars1, ars2) =>
   1.126              if pointer_eq (ars1, ars2) then raise Symtab.SAME
   1.127 -            else insert_ars pp algebra0 t ars2 ars1)
   1.128 +            else insert_ars context algebra0 t ars2 ars1)
   1.129        | (false, true) =>  (*unary completion*)
   1.130            Symtab.empty
   1.131 -          |> add_arities_table pp algebra0 arities1
   1.132 +          |> add_arities_table context algebra0 arities1
   1.133        | (false, false) => (*binary completion*)
   1.134            Symtab.empty
   1.135 -          |> add_arities_table pp algebra0 arities1
   1.136 -          |> add_arities_table pp algebra0 arities2);
   1.137 +          |> add_arities_table context algebra0 arities1
   1.138 +          |> add_arities_table context algebra0 arities2);
   1.139    in make_algebra (classes', arities') end;
   1.140  
   1.141  
   1.142  (* algebra projections *)  (* FIXME potentially violates abstract type integrity *)
   1.143  
   1.144 -fun subalgebra pp P sargs (algebra as Algebra {classes, arities}) =
   1.145 +fun subalgebra context P sargs (algebra as Algebra {classes, arities}) =
   1.146    let
   1.147      val restrict_sort = minimize_sort algebra o filter P o Graph.all_succs classes;
   1.148      fun restrict_arity t (c, Ss) =
   1.149 @@ -313,7 +313,7 @@
   1.150        else NONE;
   1.151      val classes' = classes |> Graph.restrict P;
   1.152      val arities' = arities |> Symtab.map (map_filter o restrict_arity);
   1.153 -  in (restrict_sort, rebuild_arities pp (make_algebra (classes', arities'))) end;
   1.154 +  in (restrict_sort, rebuild_arities context (make_algebra (classes', arities'))) end;
   1.155  
   1.156  
   1.157  
   1.158 @@ -326,8 +326,8 @@
   1.159    No_Arity of string * class |
   1.160    No_Subsort of sort * sort;
   1.161  
   1.162 -fun class_error pp =
   1.163 -  let val ctxt = Syntax.init_pretty pp in
   1.164 +fun class_error context =
   1.165 +  let val ctxt = Syntax.init_pretty context in
   1.166      fn No_Classrel (c1, c2) => "No class relation " ^ Syntax.string_of_classrel ctxt [c1, c2]
   1.167       | No_Arity (a, c) => "No type arity " ^ Syntax.string_of_arity ctxt (a, [], [c])
   1.168       | No_Subsort (S1, S2) =>