tuned (extend datatype to inline option)
authortraytel
Mon Mar 04 09:57:54 2013 +0100 (2013-03-04)
changeset 5132762c033d7f3d8
parent 51326 a75040aaf369
child 51328 d63ec23c9125
tuned (extend datatype to inline option)
src/Tools/subtyping.ML
     1.1 --- a/src/Tools/subtyping.ML	Sun Mar 03 18:50:46 2013 +0100
     1.2 +++ b/src/Tools/subtyping.ML	Mon Mar 04 09:57:54 2013 +0100
     1.3 @@ -20,7 +20,7 @@
     1.4  (** coercions data **)
     1.5  
     1.6  datatype variance = COVARIANT | CONTRAVARIANT | INVARIANT | INVARIANT_TO of typ;
     1.7 -datatype coerce_arg = PERMIT | FORBID
     1.8 +datatype coerce_arg = PERMIT | FORBID | LEAVE
     1.9  
    1.10  datatype data = Data of
    1.11    {coes: (term * ((typ list * typ list) * term list)) Symreltab.table,  (*coercions table*)
    1.12 @@ -29,7 +29,7 @@
    1.13     (*coercions graph restricted to base types - for efficiency reasons strored in the context*)
    1.14     coes_graph: int Graph.T,
    1.15     tmaps: (term * variance list) Symtab.table,  (*map functions*)
    1.16 -   coerce_args: coerce_arg option list Symtab.table  (*special constants with non-coercible arguments*)};
    1.17 +   coerce_args: coerce_arg list Symtab.table  (*special constants with non-coercible arguments*)};
    1.18  
    1.19  fun make_data (coes, full_graph, coes_graph, tmaps, coerce_args) =
    1.20    Data {coes = coes, full_graph = full_graph, coes_graph = coes_graph,
    1.21 @@ -297,8 +297,7 @@
    1.22    let
    1.23      val mk_coerce_args = the_default [] o Symtab.lookup (coerce_args_of ctxt);
    1.24      fun update _ [] = old
    1.25 -      | update 0 (coerce :: _) =
    1.26 -        (case coerce of NONE => old | SOME PERMIT => true | SOME FORBID => false)
    1.27 +      | update 0 (coerce :: _) = (case coerce of LEAVE => old | PERMIT => true | FORBID => false)
    1.28        | update n (_ :: cs) = update (n - 1) cs;
    1.29      val (f, n) = Term.strip_comb (Type.strip_constraints t) ||> length;
    1.30    in
    1.31 @@ -1054,9 +1053,7 @@
    1.32  (* theory setup *)
    1.33  
    1.34  val parse_coerce_args =
    1.35 -  Args.$$$ "+" >> K (SOME PERMIT) ||
    1.36 -  Args.$$$ "-" >> K (SOME FORBID) ||
    1.37 -  Args.$$$ "0" >> K NONE
    1.38 +  Args.$$$ "+" >> K PERMIT || Args.$$$ "-" >> K FORBID || Args.$$$ "0" >> K LEAVE
    1.39  
    1.40  val setup =
    1.41    Context.theory_map add_term_check #>