Mercurial Mercurial > wneuper > isa / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/Pure/type.ML
changeset 47876 421760a1efe7
parent 47525 bb185c45037e
child 50007 0518bf89c777
equal deleted inserted replaced
47875:6f00d8a83eb7 47876:421760a1efe7 
    85   val could_unify: typ * typ -> bool
 
    85   val could_unify: typ * typ -> bool
 
    86   val could_unifys: typ list * typ list -> bool
 
    86   val could_unifys: typ list * typ list -> bool
 
    87   val eq_type: tyenv -> typ * typ -> bool
 
    87   val eq_type: tyenv -> typ * typ -> bool
 
    88 
    88 
    89   (*extend and merge type signatures*)
 
    89   (*extend and merge type signatures*)
 
    90   val add_class: Proof.context -> Name_Space.naming -> binding * class list -> tsig -> tsig
 
    90   val add_class: Context.generic -> binding * class list -> tsig -> tsig
 
    91   val hide_class: bool -> string -> tsig -> tsig
 
    91   val hide_class: bool -> string -> tsig -> tsig
 
    92   val set_defsort: sort -> tsig -> tsig
 
    92   val set_defsort: sort -> tsig -> tsig
 
    93   val add_type: Proof.context -> Name_Space.naming -> binding * int -> tsig -> tsig
 
    93   val add_type: Context.generic -> binding * int -> tsig -> tsig
 
    94   val add_abbrev: Proof.context -> Name_Space.naming -> binding * string list * typ -> tsig -> tsig
 
    94   val add_abbrev: Context.generic -> binding * string list * typ -> tsig -> tsig
 
    95   val add_nonterminal: Proof.context -> Name_Space.naming -> binding -> tsig -> tsig
 
    95   val add_nonterminal: Context.generic -> binding -> tsig -> tsig
 
    96   val hide_type: bool -> string -> tsig -> tsig
 
    96   val hide_type: bool -> string -> tsig -> tsig
 
    97   val add_arity: Proof.context -> arity -> tsig -> tsig
 
    97   val add_arity: Context.pretty -> arity -> tsig -> tsig
 
    98   val add_classrel: Proof.context -> class * class -> tsig -> tsig
 
    98   val add_classrel: Context.pretty -> class * class -> tsig -> tsig
 
    99   val merge_tsig: Proof.context -> tsig * tsig -> tsig
 
    99   val merge_tsig: Context.pretty -> tsig * tsig -> tsig
 
   100 end;
 
   100 end;
 
   101 
   101 
   102 structure Type: TYPE =
 
   102 structure Type: TYPE =
 
   103 struct
 
   103 struct
 
   104 
   104 
   316   (case lookup_type tsig a of
 
   316   (case lookup_type tsig a of
 
   317     SOME (LogicalType n) => n
 
   317     SOME (LogicalType n) => n
 
   318   | _ => error (undecl_type a));
 
   318   | _ => error (undecl_type a));
 
   319 
   319 
   320 fun arity_sorts _ tsig a [] = replicate (arity_number tsig a) []
 
   320 fun arity_sorts _ tsig a [] = replicate (arity_number tsig a) []
 
   321   | arity_sorts pp (TSig {classes, ...}) a S = Sorts.mg_domain (#2 classes) a S
 
   321   | arity_sorts pp (TSig {classes, ...}) a S =
 
   322       handle Sorts.CLASS_ERROR err => error (Sorts.class_error (Syntax.init_pretty pp) err);
 
   322       Sorts.mg_domain (#2 classes) a S
 
       
   323         handle Sorts.CLASS_ERROR err => error (Sorts.class_error pp err);
 
   323 
   324 
   324 
   325 
   325 
   326 
   326 (** special treatment of type vars **)
 
   327 (** special treatment of type vars **)
 
   327 
   328 
   582 
   583 
   583 (** extend and merge type signatures **)
 
   584 (** extend and merge type signatures **)
 
   584 
   585 
   585 (* classes *)
 
   586 (* classes *)
 
   586 
   587 
   587 fun add_class ctxt naming (c, cs) tsig =
 
   588 fun add_class context (c, cs) tsig =
 
   588   tsig |> map_tsig (fn ((space, classes), default, types) =>
 
   589   tsig |> map_tsig (fn ((space, classes), default, types) =>
 
   589     let
 
   590     let
 
   590       val cs' = map (cert_class tsig) cs
 
   591       val cs' = map (cert_class tsig) cs
 
   591         handle TYPE (msg, _, _) => error msg;
 
   592         handle TYPE (msg, _, _) => error msg;
 
   592       val _ = Binding.check c;
 
   593       val _ = Binding.check c;
 
   593       val (c', space') = space |> Name_Space.declare ctxt true naming c;
 
   594       val (c', space') = space |> Name_Space.declare context true c;
 
   594       val classes' = classes |> Sorts.add_class ctxt (c', cs');
 
   595       val classes' = classes |> Sorts.add_class (Context.pretty_generic context) (c', cs');
 
   595     in ((space', classes'), default, types) end);
 
   596     in ((space', classes'), default, types) end);
 
   596 
   597 
   597 fun hide_class fully c = map_tsig (fn ((space, classes), default, types) =>
 
   598 fun hide_class fully c = map_tsig (fn ((space, classes), default, types) =>
 
   598   ((Name_Space.hide fully c space, classes), default, types));
 
   599   ((Name_Space.hide fully c space, classes), default, types));
 
   599 
   600 
   600 
   601 
   601 (* arities *)
 
   602 (* arities *)
 
   602 
   603 
   603 fun add_arity ctxt (t, Ss, S) tsig = tsig |> map_tsig (fn ((space, classes), default, types) =>
 
   604 fun add_arity pp (t, Ss, S) tsig = tsig |> map_tsig (fn ((space, classes), default, types) =>
 
   604   let
 
   605   let
 
   605     val _ =
 
   606     val _ =
 
   606       (case lookup_type tsig t of
 
   607       (case lookup_type tsig t of
 
   607         SOME (LogicalType n) => if length Ss <> n then error (bad_nargs t) else ()
 
   608         SOME (LogicalType n) => if length Ss <> n then error (bad_nargs t) else ()
 
   608       | SOME _ => error ("Logical type constructor expected: " ^ quote t)
 
   609       | SOME _ => error ("Logical type constructor expected: " ^ quote t)
 
   609       | NONE => error (undecl_type t));
 
   610       | NONE => error (undecl_type t));
 
   610     val (Ss', S') = (map (cert_sort tsig) Ss, cert_sort tsig S)
 
   611     val (Ss', S') = (map (cert_sort tsig) Ss, cert_sort tsig S)
 
   611       handle TYPE (msg, _, _) => error msg;
 
   612       handle TYPE (msg, _, _) => error msg;
 
   612     val classes' = classes |> Sorts.add_arities ctxt ((t, map (fn c' => (c', Ss')) S'));
 
   613     val classes' = classes |> Sorts.add_arities pp ((t, map (fn c' => (c', Ss')) S'));
 
   613   in ((space, classes'), default, types) end);
 
   614   in ((space, classes'), default, types) end);
 
   614 
   615 
   615 
   616 
   616 (* classrel *)
 
   617 (* classrel *)
 
   617 
   618 
   618 fun add_classrel ctxt rel tsig =
 
   619 fun add_classrel pp rel tsig =
 
   619   tsig |> map_tsig (fn ((space, classes), default, types) =>
 
   620   tsig |> map_tsig (fn ((space, classes), default, types) =>
 
   620     let
 
   621     let
 
   621       val rel' = pairself (cert_class tsig) rel
 
   622       val rel' = pairself (cert_class tsig) rel
 
   622         handle TYPE (msg, _, _) => error msg;
 
   623         handle TYPE (msg, _, _) => error msg;
 
   623       val classes' = classes |> Sorts.add_classrel ctxt rel';
 
   624       val classes' = classes |> Sorts.add_classrel pp rel';
 
   624     in ((space, classes'), default, types) end);
 
   625     in ((space, classes'), default, types) end);
 
   625 
   626 
   626 
   627 
   627 (* default sort *)
 
   628 (* default sort *)
 
   628 
   629 
   632 
   633 
   633 (* types *)
 
   634 (* types *)
 
   634 
   635 
   635 local
 
   636 local
 
   636 
   637 
   637 fun new_decl ctxt naming (c, decl) types =
 
   638 fun new_decl context (c, decl) types =
 
   638   (Binding.check c; #2 (Name_Space.define ctxt true naming (c, decl) types));
 
   639   (Binding.check c; #2 (Name_Space.define context true (c, decl) types));
 
   639 
   640 
   640 fun map_types f = map_tsig (fn (classes, default, types) =>
 
   641 fun map_types f = map_tsig (fn (classes, default, types) =>
 
   641   let
 
   642   let
 
   642     val (space', tab') = f types;
 
   643     val (space', tab') = f types;
 
   643     val _ = Name_Space.intern space' "dummy" = "dummy" orelse
 
   644     val _ = Name_Space.intern space' "dummy" = "dummy" orelse
 
   649         orelse exists (syntactic types) Ts
 
   650         orelse exists (syntactic types) Ts
 
   650   | syntactic _ _ = false;
 
   651   | syntactic _ _ = false;
 
   651 
   652 
   652 in
 
   653 in
 
   653 
   654 
   654 fun add_type ctxt naming (c, n) =
 
   655 fun add_type context (c, n) =
 
   655   if n < 0 then error ("Bad type constructor declaration " ^ Binding.print c)
 
   656   if n < 0 then error ("Bad type constructor declaration " ^ Binding.print c)
 
   656   else map_types (new_decl ctxt naming (c, LogicalType n));
 
   657   else map_types (new_decl context (c, LogicalType n));
 
   657 
   658 
   658 fun add_abbrev ctxt naming (a, vs, rhs) tsig = tsig |> map_types (fn types =>
 
   659 fun add_abbrev context (a, vs, rhs) tsig = tsig |> map_types (fn types =>
 
   659   let
 
   660   let
 
   660     fun err msg =
 
   661     fun err msg =
 
   661       cat_error msg ("The error(s) above occurred in type abbreviation " ^ Binding.print a);
 
   662       cat_error msg ("The error(s) above occurred in type abbreviation " ^ Binding.print a);
 
   662     val rhs' = strip_sorts (no_tvars (cert_typ_mode mode_syntax tsig rhs))
 
   663     val rhs' = strip_sorts (no_tvars (cert_typ_mode mode_syntax tsig rhs))
 
   663       handle TYPE (msg, _, _) => err msg;
 
   664       handle TYPE (msg, _, _) => err msg;
 
   667       | dups => err ("Duplicate variables on lhs: " ^ commas_quote dups));
 
   668       | dups => err ("Duplicate variables on lhs: " ^ commas_quote dups));
 
   668     val _ =
 
   669     val _ =
 
   669       (case subtract (op =) vs (map #1 (Term.add_tfreesT rhs' [])) of
 
   670       (case subtract (op =) vs (map #1 (Term.add_tfreesT rhs' [])) of
 
   670         [] => []
 
   671         [] => []
 
   671       | extras => err ("Extra variables on rhs: " ^ commas_quote extras));
 
   672       | extras => err ("Extra variables on rhs: " ^ commas_quote extras));
 
   672   in types |> new_decl ctxt naming (a, Abbreviation (vs, rhs', syntactic (#2 types) rhs')) end);
 
   673   in types |> new_decl context (a, Abbreviation (vs, rhs', syntactic (#2 types) rhs')) end);
 
   673 
   674 
   674 fun add_nonterminal ctxt naming = map_types o new_decl ctxt naming o rpair Nonterminal;
 
   675 fun add_nonterminal context = map_types o new_decl context o rpair Nonterminal;
 
   675 
   676 
   676 end;
 
   677 end;
 
   677 
   678 
   678 fun hide_type fully c = map_tsig (fn (classes, default, (space, types)) =>
 
   679 fun hide_type fully c = map_tsig (fn (classes, default, (space, types)) =>
 
   679   (classes, default, (Name_Space.hide fully c space, types)));
 
   680   (classes, default, (Name_Space.hide fully c space, types)));
 
   680 
   681 
   681 
   682 
   682 (* merge type signatures *)
 
   683 (* merge type signatures *)
 
   683 
   684 
   684 fun merge_tsig ctxt (tsig1, tsig2) =
 
   685 fun merge_tsig pp (tsig1, tsig2) =
 
   685   let
 
   686   let
 
   686     val (TSig {classes = (space1, classes1), default = default1, types = types1,
 
   687     val (TSig {classes = (space1, classes1), default = default1, types = types1,
 
   687       log_types = _}) = tsig1;
 
   688       log_types = _}) = tsig1;
 
   688     val (TSig {classes = (space2, classes2), default = default2, types = types2,
 
   689     val (TSig {classes = (space2, classes2), default = default2, types = types2,
 
   689       log_types = _}) = tsig2;
 
   690       log_types = _}) = tsig2;
 
   690 
   691 
   691     val space' = Name_Space.merge (space1, space2);
 
   692     val space' = Name_Space.merge (space1, space2);
 
   692     val classes' = Sorts.merge_algebra ctxt (classes1, classes2);
 
   693     val classes' = Sorts.merge_algebra pp (classes1, classes2);
 
   693     val default' = Sorts.inter_sort classes' (default1, default2);
 
   694     val default' = Sorts.inter_sort classes' (default1, default2);
 
   694     val types' = Name_Space.merge_tables (types1, types2);
 
   695     val types' = Name_Space.merge_tables (types1, types2);
 
   695   in build_tsig ((space', classes'), default', types') end;
 
   696   in build_tsig ((space', classes'), default', types') end;
 
   696 
   697 
   697 end;
 
   698 end;
wneuper/isa