# HG changeset patch # User wenzelm # Date 1303291272 -7200 # Node ID 6a2837ddde4b3d6ad7c0f154de35773e448c43f0 # Parent 6bc725d6059315c7d25a2d0ceda0f7a08484241e# Parent ff997038e8eb3773070917c0753ee73240b4c286 merged diff -r 6bc725d60593 -r 6a2837ddde4b NEWS --- a/NEWS Wed Apr 20 10:14:24 2011 +0200 +++ b/NEWS Wed Apr 20 11:21:12 2011 +0200 @@ -115,6 +115,9 @@ * Refined PARALLEL_GOALS tactical: degrades gracefully for schematic goal states; body tactic needs to address all subgoals uniformly. +* Slightly more special eq_list/eq_set, with shortcut involving +pointer equality (assumes that eq relation is reflexive). + New in Isabelle2011 (January 2011) diff -r 6bc725d60593 -r 6a2837ddde4b doc-src/IsarImplementation/Thy/Logic.thy --- a/doc-src/IsarImplementation/Thy/Logic.thy Wed Apr 20 10:14:24 2011 +0200 +++ b/doc-src/IsarImplementation/Thy/Logic.thy Wed Apr 20 11:21:12 2011 +0200 @@ -127,8 +127,10 @@ \begin{mldecls} @{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\ @{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\ - @{index_ML Sign.add_types: "(binding * int * mixfix) list -> theory -> theory"} \\ - @{index_ML Sign.add_type_abbrev: "binding * string list * typ -> theory -> theory"} \\ + @{index_ML Sign.add_types: "Proof.context -> + (binding * int * mixfix) list -> theory -> theory"} \\ + @{index_ML Sign.add_type_abbrev: "Proof.context -> + binding * string list * typ -> theory -> theory"} \\ @{index_ML Sign.primitive_class: "binding * class list -> theory -> theory"} \\ @{index_ML Sign.primitive_classrel: "class * class -> theory -> theory"} \\ @{index_ML Sign.primitive_arity: "arity -> theory -> theory"} \\ @@ -164,13 +166,12 @@ \item @{ML Sign.of_sort}~@{text "thy (\, s)"} tests whether type @{text "\"} is of sort @{text "s"}. - \item @{ML Sign.add_types}~@{text "[(\, k, mx), \]"} declares a new - type constructors @{text "\"} with @{text "k"} arguments and + \item @{ML Sign.add_types}~@{text "ctxt [(\, k, mx), \]"} declares a + new type constructors @{text "\"} with @{text "k"} arguments and optional mixfix syntax. - \item @{ML Sign.add_type_abbrev}~@{text "(\, \<^vec>\, - \)"} defines a new type abbreviation @{text - "(\<^vec>\)\ = \"}. + \item @{ML Sign.add_type_abbrev}~@{text "ctxt (\, \<^vec>\, \)"} + defines a new type abbreviation @{text "(\<^vec>\)\ = \"}. \item @{ML Sign.primitive_class}~@{text "(c, [c\<^isub>1, \, c\<^isub>n])"} declares a new class @{text "c"}, together with class @@ -364,8 +365,8 @@ @{index_ML fastype_of: "term -> typ"} \\ @{index_ML lambda: "term -> term -> term"} \\ @{index_ML betapply: "term * term -> term"} \\ - @{index_ML Sign.declare_const: "(binding * typ) * mixfix -> - theory -> term * theory"} \\ + @{index_ML Sign.declare_const: "Proof.context -> + (binding * typ) * mixfix -> theory -> term * theory"} \\ @{index_ML Sign.add_abbrev: "string -> binding * term -> theory -> (term * term) * theory"} \\ @{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\ @@ -412,9 +413,8 @@ "t u"}, with topmost @{text "\"}-conversion if @{text "t"} is an abstraction. - \item @{ML Sign.declare_const}~@{text "((c, \), mx)"} - declares a new constant @{text "c :: \"} with optional mixfix - syntax. + \item @{ML Sign.declare_const}~@{text "ctxt ((c, \), mx)"} declares + a new constant @{text "c :: \"} with optional mixfix syntax. \item @{ML Sign.add_abbrev}~@{text "print_mode (c, t)"} introduces a new term abbreviation @{text "c \ t"}. @@ -640,15 +640,16 @@ @{index_ML Thm.implies_elim: "thm -> thm -> thm"} \\ @{index_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\ @{index_ML Thm.instantiate: "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"} \\ - @{index_ML Thm.add_axiom: "binding * term -> theory -> (string * thm) * theory"} \\ + @{index_ML Thm.add_axiom: "Proof.context -> + binding * term -> theory -> (string * thm) * theory"} \\ @{index_ML Thm.add_oracle: "binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory"} \\ - @{index_ML Thm.add_def: "bool -> bool -> binding * term -> theory -> - (string * thm) * theory"} \\ + @{index_ML Thm.add_def: "Proof.context -> bool -> bool -> + binding * term -> theory -> (string * thm) * theory"} \\ \end{mldecls} \begin{mldecls} - @{index_ML Theory.add_deps: "string -> string * typ -> (string * typ) list -> - theory -> theory"} \\ + @{index_ML Theory.add_deps: "Proof.context -> string -> + string * typ -> (string * typ) list -> theory -> theory"} \\ \end{mldecls} \begin{description} @@ -696,7 +697,7 @@ term variables. Note that the types in @{text "\<^vec>x\<^isub>\"} refer to the instantiated versions. - \item @{ML Thm.add_axiom}~@{text "(name, A) thy"} declares an + \item @{ML Thm.add_axiom}~@{text "ctxt (name, A)"} declares an arbitrary proposition as axiom, and retrieves it as a theorem from the resulting theory, cf.\ @{text "axiom"} in \figref{fig:prim-rules}. Note that the low-level representation in @@ -706,17 +707,17 @@ oracle rule, essentially generating arbitrary axioms on the fly, cf.\ @{text "axiom"} in \figref{fig:prim-rules}. - \item @{ML Thm.add_def}~@{text "unchecked overloaded (name, c + \item @{ML Thm.add_def}~@{text "ctxt unchecked overloaded (name, c \<^vec>x \ t)"} states a definitional axiom for an existing constant @{text "c"}. Dependencies are recorded via @{ML Theory.add_deps}, unless the @{text "unchecked"} option is set. Note that the low-level representation in the axiom table may differ slightly from the returned theorem. - \item @{ML Theory.add_deps}~@{text "name c\<^isub>\ - \<^vec>d\<^isub>\"} declares dependencies of a named specification - for constant @{text "c\<^isub>\"}, relative to existing - specifications for constants @{text "\<^vec>d\<^isub>\"}. + \item @{ML Theory.add_deps}~@{text "ctxt name c\<^isub>\ \<^vec>d\<^isub>\"} + declares dependencies of a named specification for constant @{text + "c\<^isub>\"}, relative to existing specifications for constants @{text + "\<^vec>d\<^isub>\"}. \end{description} *} diff -r 6bc725d60593 -r 6a2837ddde4b doc-src/IsarImplementation/Thy/Prelim.thy --- a/doc-src/IsarImplementation/Thy/Prelim.thy Wed Apr 20 10:14:24 2011 +0200 +++ b/doc-src/IsarImplementation/Thy/Prelim.thy Wed Apr 20 11:21:12 2011 +0200 @@ -1109,8 +1109,8 @@ @{index_ML_type Name_Space.T} \\ @{index_ML Name_Space.empty: "string -> Name_Space.T"} \\ @{index_ML Name_Space.merge: "Name_Space.T * Name_Space.T -> Name_Space.T"} \\ - @{index_ML Name_Space.declare: "bool -> Name_Space.naming -> binding -> Name_Space.T -> - string * Name_Space.T"} \\ + @{index_ML Name_Space.declare: "Proof.context -> bool -> + Name_Space.naming -> binding -> Name_Space.T -> string * Name_Space.T"} \\ @{index_ML Name_Space.intern: "Name_Space.T -> string -> string"} \\ @{index_ML Name_Space.extern: "Proof.context -> Name_Space.T -> string -> string"} \\ @{index_ML Name_Space.is_concealed: "Name_Space.T -> string -> bool"} @@ -1173,7 +1173,7 @@ (\secref{sec:context-data}); @{text "kind"} is a formal comment to characterize the purpose of a name space. - \item @{ML Name_Space.declare}~@{text "strict naming bindings + \item @{ML Name_Space.declare}~@{text "ctxt strict naming bindings space"} enters a name binding as fully qualified internal name into the name space, with external accesses determined by the naming policy. diff -r 6bc725d60593 -r 6a2837ddde4b doc-src/IsarImplementation/Thy/document/Logic.tex --- a/doc-src/IsarImplementation/Thy/document/Logic.tex Wed Apr 20 10:14:24 2011 +0200 +++ b/doc-src/IsarImplementation/Thy/document/Logic.tex Wed Apr 20 11:21:12 2011 +0200 @@ -138,8 +138,10 @@ \begin{mldecls} \indexdef{}{ML}{Sign.subsort}\verb|Sign.subsort: theory -> sort * sort -> bool| \\ \indexdef{}{ML}{Sign.of\_sort}\verb|Sign.of_sort: theory -> typ * sort -> bool| \\ - \indexdef{}{ML}{Sign.add\_types}\verb|Sign.add_types: (binding * int * mixfix) list -> theory -> theory| \\ - \indexdef{}{ML}{Sign.add\_type\_abbrev}\verb|Sign.add_type_abbrev: binding * string list * typ -> theory -> theory| \\ + \indexdef{}{ML}{Sign.add\_types}\verb|Sign.add_types: Proof.context ->|\isasep\isanewline% +\verb| (binding * int * mixfix) list -> theory -> theory| \\ + \indexdef{}{ML}{Sign.add\_type\_abbrev}\verb|Sign.add_type_abbrev: Proof.context ->|\isasep\isanewline% +\verb| binding * string list * typ -> theory -> theory| \\ \indexdef{}{ML}{Sign.primitive\_class}\verb|Sign.primitive_class: binding * class list -> theory -> theory| \\ \indexdef{}{ML}{Sign.primitive\_classrel}\verb|Sign.primitive_classrel: class * class -> theory -> theory| \\ \indexdef{}{ML}{Sign.primitive\_arity}\verb|Sign.primitive_arity: arity -> theory -> theory| \\ @@ -172,11 +174,12 @@ \item \verb|Sign.of_sort|~\isa{thy\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{2C}{\isacharcomma}}\ s{\isaliteral{29}{\isacharparenright}}} tests whether type \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} is of sort \isa{s}. - \item \verb|Sign.add_types|~\isa{{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}{\isaliteral{2C}{\isacharcomma}}\ k{\isaliteral{2C}{\isacharcomma}}\ mx{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{5D}{\isacharbrackright}}} declares a new - type constructors \isa{{\isaliteral{5C3C6B617070613E}{\isasymkappa}}} with \isa{k} arguments and + \item \verb|Sign.add_types|~\isa{ctxt\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}{\isaliteral{2C}{\isacharcomma}}\ k{\isaliteral{2C}{\isacharcomma}}\ mx{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{5D}{\isacharbrackright}}} declares a + new type constructors \isa{{\isaliteral{5C3C6B617070613E}{\isasymkappa}}} with \isa{k} arguments and optional mixfix syntax. - \item \verb|Sign.add_type_abbrev|~\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{29}{\isacharparenright}}} defines a new type abbreviation \isa{{\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}}. + \item \verb|Sign.add_type_abbrev|~\isa{ctxt\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{29}{\isacharparenright}}} + defines a new type abbreviation \isa{{\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}}. \item \verb|Sign.primitive_class|~\isa{{\isaliteral{28}{\isacharparenleft}}c{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ c\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}} declares a new class \isa{c}, together with class relations \isa{c\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ c\isaliteral{5C3C5E697375623E}{}\isactrlisub i}, for \isa{i\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ n}. @@ -386,8 +389,8 @@ \indexdef{}{ML}{fastype\_of}\verb|fastype_of: term -> typ| \\ \indexdef{}{ML}{lambda}\verb|lambda: term -> term -> term| \\ \indexdef{}{ML}{betapply}\verb|betapply: term * term -> term| \\ - \indexdef{}{ML}{Sign.declare\_const}\verb|Sign.declare_const: (binding * typ) * mixfix ->|\isasep\isanewline% -\verb| theory -> term * theory| \\ + \indexdef{}{ML}{Sign.declare\_const}\verb|Sign.declare_const: Proof.context ->|\isasep\isanewline% +\verb| (binding * typ) * mixfix -> theory -> term * theory| \\ \indexdef{}{ML}{Sign.add\_abbrev}\verb|Sign.add_abbrev: string -> binding * term ->|\isasep\isanewline% \verb| theory -> (term * term) * theory| \\ \indexdef{}{ML}{Sign.const\_typargs}\verb|Sign.const_typargs: theory -> string * typ -> typ list| \\ @@ -426,9 +429,8 @@ \item \verb|betapply|~\isa{{\isaliteral{28}{\isacharparenleft}}t{\isaliteral{2C}{\isacharcomma}}\ u{\isaliteral{29}{\isacharparenright}}} produces an application \isa{t\ u}, with topmost \isa{{\isaliteral{5C3C626574613E}{\isasymbeta}}}-conversion if \isa{t} is an abstraction. - \item \verb|Sign.declare_const|~\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}c{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ mx{\isaliteral{29}{\isacharparenright}}} - declares a new constant \isa{c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}} with optional mixfix - syntax. + \item \verb|Sign.declare_const|~\isa{ctxt\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}c{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ mx{\isaliteral{29}{\isacharparenright}}} declares + a new constant \isa{c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}} with optional mixfix syntax. \item \verb|Sign.add_abbrev|~\isa{print{\isaliteral{5F}{\isacharunderscore}}mode\ {\isaliteral{28}{\isacharparenleft}}c{\isaliteral{2C}{\isacharcomma}}\ t{\isaliteral{29}{\isacharparenright}}} introduces a new term abbreviation \isa{c\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t}. @@ -673,15 +675,16 @@ \indexdef{}{ML}{Thm.implies\_elim}\verb|Thm.implies_elim: thm -> thm -> thm| \\ \indexdef{}{ML}{Thm.generalize}\verb|Thm.generalize: string list * string list -> int -> thm -> thm| \\ \indexdef{}{ML}{Thm.instantiate}\verb|Thm.instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm| \\ - \indexdef{}{ML}{Thm.add\_axiom}\verb|Thm.add_axiom: binding * term -> theory -> (string * thm) * theory| \\ + \indexdef{}{ML}{Thm.add\_axiom}\verb|Thm.add_axiom: Proof.context ->|\isasep\isanewline% +\verb| binding * term -> theory -> (string * thm) * theory| \\ \indexdef{}{ML}{Thm.add\_oracle}\verb|Thm.add_oracle: binding * ('a -> cterm) -> theory ->|\isasep\isanewline% \verb| (string * ('a -> thm)) * theory| \\ - \indexdef{}{ML}{Thm.add\_def}\verb|Thm.add_def: bool -> bool -> binding * term -> theory ->|\isasep\isanewline% -\verb| (string * thm) * theory| \\ + \indexdef{}{ML}{Thm.add\_def}\verb|Thm.add_def: Proof.context -> bool -> bool ->|\isasep\isanewline% +\verb| binding * term -> theory -> (string * thm) * theory| \\ \end{mldecls} \begin{mldecls} - \indexdef{}{ML}{Theory.add\_deps}\verb|Theory.add_deps: string -> string * typ -> (string * typ) list ->|\isasep\isanewline% -\verb| theory -> theory| \\ + \indexdef{}{ML}{Theory.add\_deps}\verb|Theory.add_deps: Proof.context -> string ->|\isasep\isanewline% +\verb| string * typ -> (string * typ) list -> theory -> theory| \\ \end{mldecls} \begin{description} @@ -726,7 +729,7 @@ term variables. Note that the types in \isa{\isaliteral{5C3C5E7665633E}{}\isactrlvec x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}} refer to the instantiated versions. - \item \verb|Thm.add_axiom|~\isa{{\isaliteral{28}{\isacharparenleft}}name{\isaliteral{2C}{\isacharcomma}}\ A{\isaliteral{29}{\isacharparenright}}\ thy} declares an + \item \verb|Thm.add_axiom|~\isa{ctxt\ {\isaliteral{28}{\isacharparenleft}}name{\isaliteral{2C}{\isacharcomma}}\ A{\isaliteral{29}{\isacharparenright}}} declares an arbitrary proposition as axiom, and retrieves it as a theorem from the resulting theory, cf.\ \isa{axiom} in \figref{fig:prim-rules}. Note that the low-level representation in @@ -736,15 +739,14 @@ oracle rule, essentially generating arbitrary axioms on the fly, cf.\ \isa{axiom} in \figref{fig:prim-rules}. - \item \verb|Thm.add_def|~\isa{unchecked\ overloaded\ {\isaliteral{28}{\isacharparenleft}}name{\isaliteral{2C}{\isacharcomma}}\ c\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t{\isaliteral{29}{\isacharparenright}}} states a definitional axiom for an existing constant + \item \verb|Thm.add_def|~\isa{ctxt\ unchecked\ overloaded\ {\isaliteral{28}{\isacharparenleft}}name{\isaliteral{2C}{\isacharcomma}}\ c\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t{\isaliteral{29}{\isacharparenright}}} states a definitional axiom for an existing constant \isa{c}. Dependencies are recorded via \verb|Theory.add_deps|, unless the \isa{unchecked} option is set. Note that the low-level representation in the axiom table may differ slightly from the returned theorem. - \item \verb|Theory.add_deps|~\isa{name\ c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec d\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7369676D613E}{\isasymsigma}}} declares dependencies of a named specification - for constant \isa{c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}}, relative to existing - specifications for constants \isa{\isaliteral{5C3C5E7665633E}{}\isactrlvec d\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7369676D613E}{\isasymsigma}}}. + \item \verb|Theory.add_deps|~\isa{ctxt\ name\ c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec d\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7369676D613E}{\isasymsigma}}} + declares dependencies of a named specification for constant \isa{c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}}, relative to existing specifications for constants \isa{\isaliteral{5C3C5E7665633E}{}\isactrlvec d\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7369676D613E}{\isasymsigma}}}. \end{description}% \end{isamarkuptext}% diff -r 6bc725d60593 -r 6a2837ddde4b doc-src/IsarImplementation/Thy/document/Prelim.tex --- a/doc-src/IsarImplementation/Thy/document/Prelim.tex Wed Apr 20 10:14:24 2011 +0200 +++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex Wed Apr 20 11:21:12 2011 +0200 @@ -1607,8 +1607,8 @@ \indexdef{}{ML type}{Name\_Space.T}\verb|type Name_Space.T| \\ \indexdef{}{ML}{Name\_Space.empty}\verb|Name_Space.empty: string -> Name_Space.T| \\ \indexdef{}{ML}{Name\_Space.merge}\verb|Name_Space.merge: Name_Space.T * Name_Space.T -> Name_Space.T| \\ - \indexdef{}{ML}{Name\_Space.declare}\verb|Name_Space.declare: bool -> Name_Space.naming -> binding -> Name_Space.T ->|\isasep\isanewline% -\verb| string * Name_Space.T| \\ + \indexdef{}{ML}{Name\_Space.declare}\verb|Name_Space.declare: Proof.context -> bool ->|\isasep\isanewline% +\verb| Name_Space.naming -> binding -> Name_Space.T -> string * Name_Space.T| \\ \indexdef{}{ML}{Name\_Space.intern}\verb|Name_Space.intern: Name_Space.T -> string -> string| \\ \indexdef{}{ML}{Name\_Space.extern}\verb|Name_Space.extern: Proof.context -> Name_Space.T -> string -> string| \\ \indexdef{}{ML}{Name\_Space.is\_concealed}\verb|Name_Space.is_concealed: Name_Space.T -> string -> bool| @@ -1667,7 +1667,7 @@ (\secref{sec:context-data}); \isa{kind} is a formal comment to characterize the purpose of a name space. - \item \verb|Name_Space.declare|~\isa{strict\ naming\ bindings\ space} enters a name binding as fully qualified internal name into + \item \verb|Name_Space.declare|~\isa{ctxt\ strict\ naming\ bindings\ space} enters a name binding as fully qualified internal name into the name space, with external accesses determined by the naming policy. diff -r 6bc725d60593 -r 6a2837ddde4b src/HOL/HOL.thy --- a/src/HOL/HOL.thy Wed Apr 20 10:14:24 2011 +0200 +++ b/src/HOL/HOL.thy Wed Apr 20 11:21:12 2011 +0200 @@ -1746,20 +1746,21 @@ setup {* let -fun eq_codegen thy defs dep thyname b t gr = +fun eq_codegen thy mode defs dep thyname b t gr = (case strip_comb t of (Const (@{const_name HOL.eq}, Type (_, [Type ("fun", _), _])), _) => NONE | (Const (@{const_name HOL.eq}, _), [t, u]) => let - val (pt, gr') = Codegen.invoke_codegen thy defs dep thyname false t gr; - val (pu, gr'') = Codegen.invoke_codegen thy defs dep thyname false u gr'; - val (_, gr''') = Codegen.invoke_tycodegen thy defs dep thyname false HOLogic.boolT gr''; + val (pt, gr') = Codegen.invoke_codegen thy mode defs dep thyname false t gr; + val (pu, gr'') = Codegen.invoke_codegen thy mode defs dep thyname false u gr'; + val (_, gr''') = + Codegen.invoke_tycodegen thy mode defs dep thyname false HOLogic.boolT gr''; in SOME (Codegen.parens (Pretty.block [pt, Codegen.str " =", Pretty.brk 1, pu]), gr''') end | (t as Const (@{const_name HOL.eq}, _), ts) => SOME (Codegen.invoke_codegen - thy defs dep thyname b (Codegen.eta_expand t ts 2) gr) + thy mode defs dep thyname b (Codegen.eta_expand t ts 2) gr) | _ => NONE); in diff -r 6bc725d60593 -r 6a2837ddde4b src/HOL/Int.thy --- a/src/HOL/Int.thy Wed Apr 20 10:14:24 2011 +0200 +++ b/src/HOL/Int.thy Wed Apr 20 11:21:12 2011 +0200 @@ -2351,11 +2351,11 @@ fun strip_number_of (@{term "Int.number_of :: int => int"} $ t) = t | strip_number_of t = t; -fun numeral_codegen thy defs dep module b t gr = +fun numeral_codegen thy mode defs dep module b t gr = let val i = HOLogic.dest_numeral (strip_number_of t) in SOME (Codegen.str (string_of_int i), - snd (Codegen.invoke_tycodegen thy defs dep module false HOLogic.intT gr)) + snd (Codegen.invoke_tycodegen thy mode defs dep module false HOLogic.intT gr)) end handle TERM _ => NONE; in diff -r 6bc725d60593 -r 6a2837ddde4b src/HOL/List.thy --- a/src/HOL/List.thy Wed Apr 20 10:14:24 2011 +0200 +++ b/src/HOL/List.thy Wed Apr 20 11:21:12 2011 +0200 @@ -5207,13 +5207,13 @@ setup {* let - fun list_codegen thy defs dep thyname b t gr = + fun list_codegen thy mode defs dep thyname b t gr = let val ts = HOLogic.dest_list t; - val (_, gr') = Codegen.invoke_tycodegen thy defs dep thyname false + val (_, gr') = Codegen.invoke_tycodegen thy mode defs dep thyname false (fastype_of t) gr; val (ps, gr'') = fold_map - (Codegen.invoke_codegen thy defs dep thyname false) ts gr' + (Codegen.invoke_codegen thy mode defs dep thyname false) ts gr' in SOME (Pretty.list "[" "]" ps, gr'') end handle TERM _ => NONE; in fold (List_Code.add_literal_list) ["SML", "OCaml", "Haskell", "Scala"] diff -r 6bc725d60593 -r 6a2837ddde4b src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Wed Apr 20 10:14:24 2011 +0200 +++ b/src/HOL/Product_Type.thy Wed Apr 20 11:21:12 2011 +0200 @@ -336,7 +336,7 @@ | strip_abs_split i t = strip_abs_split i (Abs ("x", hd (binder_types (fastype_of t)), t $ Bound 0)); -fun let_codegen thy defs dep thyname brack t gr = +fun let_codegen thy mode defs dep thyname brack t gr = (case strip_comb t of (t1 as Const (@{const_name Let}, _), t2 :: t3 :: ts) => let @@ -347,17 +347,17 @@ | dest_let t = ([], t); fun mk_code (l, r) gr = let - val (pl, gr1) = Codegen.invoke_codegen thy defs dep thyname false l gr; - val (pr, gr2) = Codegen.invoke_codegen thy defs dep thyname false r gr1; + val (pl, gr1) = Codegen.invoke_codegen thy mode defs dep thyname false l gr; + val (pr, gr2) = Codegen.invoke_codegen thy mode defs dep thyname false r gr1; in ((pl, pr), gr2) end in case dest_let (t1 $ t2 $ t3) of ([], _) => NONE | (ps, u) => let val (qs, gr1) = fold_map mk_code ps gr; - val (pu, gr2) = Codegen.invoke_codegen thy defs dep thyname false u gr1; + val (pu, gr2) = Codegen.invoke_codegen thy mode defs dep thyname false u gr1; val (pargs, gr3) = fold_map - (Codegen.invoke_codegen thy defs dep thyname true) ts gr2 + (Codegen.invoke_codegen thy mode defs dep thyname true) ts gr2 in SOME (Codegen.mk_app brack (Pretty.blk (0, [Codegen.str "let ", Pretty.blk (0, flat @@ -370,14 +370,14 @@ end | _ => NONE); -fun split_codegen thy defs dep thyname brack t gr = (case strip_comb t of +fun split_codegen thy mode defs dep thyname brack t gr = (case strip_comb t of (t1 as Const (@{const_name prod_case}, _), t2 :: ts) => let val ([p], u) = strip_abs_split 1 (t1 $ t2); - val (q, gr1) = Codegen.invoke_codegen thy defs dep thyname false p gr; - val (pu, gr2) = Codegen.invoke_codegen thy defs dep thyname false u gr1; + val (q, gr1) = Codegen.invoke_codegen thy mode defs dep thyname false p gr; + val (pu, gr2) = Codegen.invoke_codegen thy mode defs dep thyname false u gr1; val (pargs, gr3) = fold_map - (Codegen.invoke_codegen thy defs dep thyname true) ts gr2 + (Codegen.invoke_codegen thy mode defs dep thyname true) ts gr2 in SOME (Codegen.mk_app brack (Pretty.block [Codegen.str "(fn ", q, Codegen.str " =>", diff -r 6bc725d60593 -r 6a2837ddde4b src/HOL/String.thy --- a/src/HOL/String.thy Wed Apr 20 10:14:24 2011 +0200 +++ b/src/HOL/String.thy Wed Apr 20 11:21:12 2011 +0200 @@ -227,10 +227,10 @@ setup {* let -fun char_codegen thy defs dep thyname b t gr = +fun char_codegen thy mode defs dep thyname b t gr = let val i = HOLogic.dest_char t; - val (_, gr') = Codegen.invoke_tycodegen thy defs dep thyname false + val (_, gr') = Codegen.invoke_tycodegen thy mode defs dep thyname false (fastype_of t) gr; in SOME (Codegen.str (ML_Syntax.print_string (chr i)), gr') end handle TERM _ => NONE; diff -r 6bc725d60593 -r 6a2837ddde4b src/HOL/Tools/Datatype/datatype_codegen.ML --- a/src/HOL/Tools/Datatype/datatype_codegen.ML Wed Apr 20 10:14:24 2011 +0200 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Wed Apr 20 11:21:12 2011 +0200 @@ -151,7 +151,7 @@ (* datatype definition *) -fun add_dt_defs thy defs dep module descr sorts gr = +fun add_dt_defs thy mode defs dep module descr sorts gr = let val descr' = filter (can (map Datatype_Aux.dest_DtTFree o #2 o snd)) descr; val rtnames = map (#1 o snd) (filter (fn (_, (_, _, cs)) => @@ -159,7 +159,7 @@ val (_, (tname, _, _)) :: _ = descr'; val node_id = tname ^ " (type)"; - val module' = Codegen.if_library (Codegen.thyname_of_type thy tname) module; + val module' = Codegen.if_library mode (Codegen.thyname_of_type thy tname) module; fun mk_dtdef prfx [] gr = ([], gr) | mk_dtdef prfx ((_, (tname, dts, cs))::xs) gr = @@ -169,7 +169,7 @@ val ((_, type_id), gr') = Codegen.mk_type_id module' tname gr; val (ps, gr'') = gr' |> fold_map (fn (cname, cargs) => - fold_map (Codegen.invoke_tycodegen thy defs node_id module' false) + fold_map (Codegen.invoke_tycodegen thy mode defs node_id module' false) cargs ##>> Codegen.mk_const_id module' cname) cs'; val (rest, gr''') = mk_dtdef "and " xs gr'' @@ -309,11 +309,11 @@ Codegen.map_node node_id (K (NONE, module', Codegen.string_of (Pretty.blk (0, separate Pretty.fbrk dtdef @ [Codegen.str ";"])) ^ "\n\n" ^ - (if member (op =) (! Codegen.mode) "term_of" then + (if member (op =) mode "term_of" then Codegen.string_of (Pretty.blk (0, separate Pretty.fbrk (mk_term_of_def gr2 "fun " descr') @ [Codegen.str ";"])) ^ "\n\n" else "") ^ - (if member (op =) (! Codegen.mode) "test" then + (if member (op =) mode "test" then Codegen.string_of (Pretty.blk (0, separate Pretty.fbrk (mk_gen_of_def gr2 "fun " descr') @ [Codegen.str ";"])) ^ "\n\n" else ""))) gr2 @@ -323,10 +323,10 @@ (* case expressions *) -fun pretty_case thy defs dep module brack constrs (c as Const (_, T)) ts gr = +fun pretty_case thy mode defs dep module brack constrs (c as Const (_, T)) ts gr = let val i = length constrs in if length ts <= i then - Codegen.invoke_codegen thy defs dep module brack (Codegen.eta_expand c ts (i+1)) gr + Codegen.invoke_codegen thy mode defs dep module brack (Codegen.eta_expand c ts (i+1)) gr else let val ts1 = take i ts; @@ -342,10 +342,10 @@ val xs = Name.variant_list names (replicate j "x"); val Us' = take j (binder_types U); val frees = map2 (curry Free) xs Us'; - val (cp, gr0) = Codegen.invoke_codegen thy defs dep module false + val (cp, gr0) = Codegen.invoke_codegen thy mode defs dep module false (list_comb (Const (cname, Us' ---> dT), frees)) gr; val t' = Envir.beta_norm (list_comb (t, frees)); - val (p, gr1) = Codegen.invoke_codegen thy defs dep module false t' gr0; + val (p, gr1) = Codegen.invoke_codegen thy mode defs dep module false t' gr0; val (ps, gr2) = pcase cs ts Us gr1; in ([Pretty.block [cp, Codegen.str " =>", Pretty.brk 1, p]] :: ps, gr2) @@ -353,8 +353,8 @@ val (ps1, gr1) = pcase constrs ts1 Ts gr ; val ps = flat (separate [Pretty.brk 1, Codegen.str "| "] ps1); - val (p, gr2) = Codegen.invoke_codegen thy defs dep module false t gr1; - val (ps2, gr3) = fold_map (Codegen.invoke_codegen thy defs dep module true) ts2 gr2; + val (p, gr2) = Codegen.invoke_codegen thy mode defs dep module false t gr1; + val (ps2, gr3) = fold_map (Codegen.invoke_codegen thy mode defs dep module true) ts2 gr2; in ((if not (null ts2) andalso brack then Codegen.parens else I) (Pretty.block (separate (Pretty.brk 1) (Pretty.block ([Codegen.str "(case ", p, Codegen.str " of", @@ -365,15 +365,15 @@ (* constructors *) -fun pretty_constr thy defs dep module brack args (c as Const (s, T)) ts gr = +fun pretty_constr thy mode defs dep module brack args (c as Const (s, T)) ts gr = let val i = length args in if i > 1 andalso length ts < i then - Codegen.invoke_codegen thy defs dep module brack (Codegen.eta_expand c ts i) gr + Codegen.invoke_codegen thy mode defs dep module brack (Codegen.eta_expand c ts i) gr else let val id = Codegen.mk_qual_id module (Codegen.get_const_id gr s); val (ps, gr') = fold_map - (Codegen.invoke_codegen thy defs dep module (i = 1)) ts gr; + (Codegen.invoke_codegen thy mode defs dep module (i = 1)) ts gr; in (case args of _ :: _ :: _ => (if brack then Codegen.parens else I) @@ -385,14 +385,14 @@ (* code generators for terms and types *) -fun datatype_codegen thy defs dep module brack t gr = +fun datatype_codegen thy mode defs dep module brack t gr = (case strip_comb t of (c as Const (s, T), ts) => (case Datatype_Data.info_of_case thy s of SOME {index, descr, ...} => if is_some (Codegen.get_assoc_code thy (s, T)) then NONE else - SOME (pretty_case thy defs dep module brack + SOME (pretty_case thy mode defs dep module brack (#3 (the (AList.lookup op = descr index))) c ts gr) | NONE => (case (Datatype_Data.info_of_constr thy (s, T), body_type T) of @@ -406,28 +406,28 @@ if tyname <> tyname' then NONE else SOME - (pretty_constr thy defs + (pretty_constr thy mode defs dep module brack args c ts - (snd (Codegen.invoke_tycodegen thy defs dep module false U gr))) + (snd (Codegen.invoke_tycodegen thy mode defs dep module false U gr))) end | _ => NONE)) | _ => NONE); -fun datatype_tycodegen thy defs dep module brack (Type (s, Ts)) gr = +fun datatype_tycodegen thy mode defs dep module brack (Type (s, Ts)) gr = (case Datatype_Data.get_info thy s of NONE => NONE | SOME {descr, sorts, ...} => if is_some (Codegen.get_assoc_type thy s) then NONE else let val (ps, gr') = fold_map - (Codegen.invoke_tycodegen thy defs dep module false) Ts gr; - val (module', gr'') = add_dt_defs thy defs dep module descr sorts gr' ; + (Codegen.invoke_tycodegen thy mode defs dep module false) Ts gr; + val (module', gr'') = add_dt_defs thy mode defs dep module descr sorts gr' ; val (tyid, gr''') = Codegen.mk_type_id module' s gr'' in SOME (Pretty.block ((if null Ts then [] else [Codegen.mk_tuple ps, Codegen.str " "]) @ [Codegen.str (Codegen.mk_qual_id module tyid)]), gr''') end) - | datatype_tycodegen _ _ _ _ _ _ _ = NONE; + | datatype_tycodegen _ _ _ _ _ _ _ _ = NONE; (** theory setup **) diff -r 6bc725d60593 -r 6a2837ddde4b src/HOL/Tools/code_evaluation.ML --- a/src/HOL/Tools/code_evaluation.ML Wed Apr 20 10:14:24 2011 +0200 +++ b/src/HOL/Tools/code_evaluation.ML Wed Apr 20 11:21:12 2011 +0200 @@ -150,8 +150,8 @@ | NONE => NONE) | subst_termify t = subst_termify_app (strip_comb t) -fun check_termify ts ctxt = map_default subst_termify ts - |> Option.map (rpair ctxt) +fun check_termify ctxt ts = + the_default ts (map_default subst_termify ts); (** evaluation **) diff -r 6bc725d60593 -r 6a2837ddde4b src/HOL/Tools/inductive_codegen.ML --- a/src/HOL/Tools/inductive_codegen.ML Wed Apr 20 10:14:24 2011 +0200 +++ b/src/HOL/Tools/inductive_codegen.ML Wed Apr 20 11:21:12 2011 +0200 @@ -239,9 +239,9 @@ end) ps)); -fun use_random () = member (op =) (!Codegen.mode) "random_ind"; +fun use_random codegen_mode = member (op =) codegen_mode "random_ind"; -fun check_mode_clause thy arg_vs modes ((iss, is), rnd) (ts, ps) = +fun check_mode_clause thy codegen_mode arg_vs modes ((iss, is), rnd) (ts, ps) = let val modes' = modes @ map_filter (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [(([], js), false)])) @@ -253,7 +253,7 @@ (rnd orelse needs_random m) (filter_out (equal x) ps) | (_, (_, vs') :: _) :: _ => - if use_random () then + if use_random codegen_mode then check_mode_prems (union (op =) vs (map (fst o fst) vs')) true ps else NONE | _ => NONE); @@ -268,17 +268,17 @@ let val missing_vs = missing_vars vs ts in if null missing_vs orelse - use_random () andalso monomorphic_vars missing_vs + use_random codegen_mode andalso monomorphic_vars missing_vs then SOME (rnd' orelse not (null missing_vs)) else NONE end) else NONE end; -fun check_modes_pred thy arg_vs preds modes (p, ms) = +fun check_modes_pred thy codegen_mode arg_vs preds modes (p, ms) = let val SOME rs = AList.lookup (op =) preds p in (p, List.mapPartial (fn m as (m', _) => - let val xs = map (check_mode_clause thy arg_vs modes m) rs + let val xs = map (check_mode_clause thy codegen_mode arg_vs modes m) rs in case find_index is_none xs of ~1 => SOME (m', exists (fn SOME b => b) xs) | i => (Codegen.message ("Clause " ^ string_of_int (i+1) ^ " of " ^ @@ -290,8 +290,8 @@ let val y = f x in if x = y then x else fixp f y end; -fun infer_modes thy extra_modes arities arg_vs preds = fixp (fn modes => - map (check_modes_pred thy arg_vs preds (modes @ extra_modes)) modes) +fun infer_modes thy codegen_mode extra_modes arities arg_vs preds = fixp (fn modes => + map (check_modes_pred thy codegen_mode arg_vs preds (modes @ extra_modes)) modes) (map (fn (s, (ks, k)) => (s, map (rpair false) (cprod (cprods (map (fn NONE => [NONE] | SOME k' => map SOME (subsets 1 k')) ks), @@ -358,34 +358,34 @@ separate (Pretty.brk 1) (Codegen.str s :: replicate k (Codegen.str "|> ???")) @ (if k = 0 then [] else [Codegen.str ")"])), Pretty.brk 1, p]); -fun compile_expr thy defs dep module brack modes (NONE, t) gr = - apfst single (Codegen.invoke_codegen thy defs dep module brack t gr) - | compile_expr _ _ _ _ _ _ (SOME _, Var ((name, _), _)) gr = +fun compile_expr thy codegen_mode defs dep module brack modes (NONE, t) gr = + apfst single (Codegen.invoke_codegen thy codegen_mode defs dep module brack t gr) + | compile_expr _ _ _ _ _ _ _ (SOME _, Var ((name, _), _)) gr = ([Codegen.str name], gr) - | compile_expr thy defs dep module brack modes (SOME (Mode ((mode, _), _, ms)), t) gr = + | compile_expr thy codegen_mode defs dep module brack modes (SOME (Mode ((mode, _), _, ms)), t) gr = (case strip_comb t of (Const (name, _), args) => if name = @{const_name HOL.eq} orelse AList.defined op = modes name then let val (args1, args2) = chop (length ms) args; val ((ps, mode_id), gr') = gr |> fold_map - (compile_expr thy defs dep module true modes) (ms ~~ args1) + (compile_expr thy codegen_mode defs dep module true modes) (ms ~~ args1) ||>> modename module name mode; val (ps', gr'') = (case mode of ([], []) => ([Codegen.str "()"], gr') | _ => fold_map - (Codegen.invoke_codegen thy defs dep module true) args2 gr') + (Codegen.invoke_codegen thy codegen_mode defs dep module true) args2 gr') in ((if brack andalso not (null ps andalso null ps') then single o Codegen.parens o Pretty.block else I) (flat (separate [Pretty.brk 1] ([Codegen.str mode_id] :: ps @ map single ps'))), gr') end else apfst (single o mk_funcomp brack "??" (length (binder_types (fastype_of t)))) - (Codegen.invoke_codegen thy defs dep module true t gr) + (Codegen.invoke_codegen thy codegen_mode defs dep module true t gr) | _ => apfst (single o mk_funcomp brack "??" (length (binder_types (fastype_of t)))) - (Codegen.invoke_codegen thy defs dep module true t gr)); + (Codegen.invoke_codegen thy codegen_mode defs dep module true t gr)); -fun compile_clause thy defs dep module all_vs arg_vs modes (iss, is) (ts, ps) inp gr = +fun compile_clause thy codegen_mode defs dep module all_vs arg_vs modes (iss, is) (ts, ps) inp gr = let val modes' = modes @ map_filter (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [(([], js), false)])) @@ -399,7 +399,7 @@ fun compile_eq (s, t) gr = apfst (Pretty.block o cons (Codegen.str (s ^ " = ")) o single) - (Codegen.invoke_codegen thy defs dep module false t gr); + (Codegen.invoke_codegen thy codegen_mode defs dep module false t gr); val (in_ts, out_ts) = get_args is 1 ts; val (in_ts', (all_vs', eqs)) = fold_map check_constrt in_ts (all_vs, []); @@ -407,13 +407,13 @@ fun compile_prems out_ts' vs names [] gr = let val (out_ps, gr2) = - fold_map (Codegen.invoke_codegen thy defs dep module false) out_ts gr; + fold_map (Codegen.invoke_codegen thy codegen_mode defs dep module false) out_ts gr; val (eq_ps, gr3) = fold_map compile_eq eqs gr2; val (out_ts'', (names', eqs')) = fold_map check_constrt out_ts' (names, []); val (out_ts''', nvs) = fold_map distinct_v out_ts'' (names', map (fn x => (x, [x])) vs); val (out_ps', gr4) = - fold_map (Codegen.invoke_codegen thy defs dep module false) out_ts''' gr3; + fold_map (Codegen.invoke_codegen thy codegen_mode defs dep module false) out_ts''' gr3; val (eq_ps', gr5) = fold_map compile_eq eqs' gr4; val vs' = distinct (op =) (flat (vs :: map term_vs out_ts')); val missing_vs = missing_vars vs' out_ts; @@ -425,7 +425,7 @@ final_p (exists (not o is_exhaustive) out_ts'''), gr5) else let - val (pat_p, gr6) = Codegen.invoke_codegen thy defs dep module true + val (pat_p, gr6) = Codegen.invoke_codegen thy codegen_mode defs dep module true (HOLogic.mk_tuple (map Var missing_vs)) gr5; val gen_p = Codegen.mk_gen gr6 module true [] "" @@ -445,7 +445,7 @@ val (out_ts', (names', eqs)) = fold_map check_constrt out_ts (names, []); val (out_ts'', nvs) = fold_map distinct_v out_ts' (names', map (fn x => (x, [x])) vs); val (out_ps, gr0) = - fold_map (Codegen.invoke_codegen thy defs dep module false) out_ts'' gr; + fold_map (Codegen.invoke_codegen thy codegen_mode defs dep module false) out_ts'' gr; val (eq_ps, gr1) = fold_map compile_eq eqs gr0; in (case hd (select_mode_prem thy modes' vs' ps) of @@ -454,13 +454,13 @@ val ps' = filter_out (equal p) ps; val (in_ts, out_ts''') = get_args js 1 us; val (in_ps, gr2) = - fold_map (Codegen.invoke_codegen thy defs dep module true) in_ts gr1; + fold_map (Codegen.invoke_codegen thy codegen_mode defs dep module true) in_ts gr1; val (ps, gr3) = if not is_set then apfst (fn ps => ps @ (if null in_ps then [] else [Pretty.brk 1]) @ separate (Pretty.brk 1) in_ps) - (compile_expr thy defs dep module false modes + (compile_expr thy codegen_mode defs dep module false modes (SOME mode, t) gr2) else apfst (fn p => @@ -468,7 +468,7 @@ Codegen.str "of", Codegen.str "Set", Codegen.str "xs", Codegen.str "=>", Codegen.str "xs)"]) (*this is a very strong assumption about the generated code!*) - (Codegen.invoke_codegen thy defs dep module true t gr2); + (Codegen.invoke_codegen thy codegen_mode defs dep module true t gr2); val (rest, gr4) = compile_prems out_ts''' vs' (fst nvs) ps' gr3; in (compile_match (snd nvs) eq_ps out_ps @@ -479,7 +479,8 @@ | (p as Sidecond t, [(_, [])]) => let val ps' = filter_out (equal p) ps; - val (side_p, gr2) = Codegen.invoke_codegen thy defs dep module true t gr1; + val (side_p, gr2) = + Codegen.invoke_codegen thy codegen_mode defs dep module true t gr1; val (rest, gr3) = compile_prems [] vs' (fst nvs) ps' gr2; in (compile_match (snd nvs) eq_ps out_ps @@ -490,7 +491,8 @@ | (_, (_, missing_vs) :: _) => let val T = HOLogic.mk_tupleT (map snd missing_vs); - val (_, gr2) = Codegen.invoke_tycodegen thy defs dep module false T gr1; + val (_, gr2) = + Codegen.invoke_tycodegen thy codegen_mode defs dep module false T gr1; val gen_p = Codegen.mk_gen gr2 module true [] "" T; val (rest, gr3) = compile_prems [HOLogic.mk_tuple (map Var missing_vs)] vs' (fst nvs) ps gr2 @@ -508,12 +510,12 @@ Codegen.str " :->", Pretty.brk 1, prem_p], gr') end; -fun compile_pred thy defs dep module prfx all_vs arg_vs modes s cls mode gr = +fun compile_pred thy codegen_mode defs dep module prfx all_vs arg_vs modes s cls mode gr = let val xs = map Codegen.str (Name.variant_list arg_vs (map (fn i => "x" ^ string_of_int i) (snd mode))); val ((cl_ps, mode_id), gr') = gr |> - fold_map (fn cl => compile_clause thy defs + fold_map (fn cl => compile_clause thy codegen_mode defs dep module all_vs arg_vs modes mode cl (mk_tuple xs)) cls ||>> modename module s mode in @@ -527,9 +529,9 @@ flat (separate [Codegen.str " ++", Pretty.brk 1] (map single cl_ps))), (gr', "and ")) end; -fun compile_preds thy defs dep module all_vs arg_vs modes preds gr = +fun compile_preds thy codegen_mode defs dep module all_vs arg_vs modes preds gr = let val (prs, (gr', _)) = fold_map (fn (s, cls) => - fold_map (fn (mode, _) => fn (gr', prfx') => compile_pred thy defs + fold_map (fn (mode, _) => fn (gr', prfx') => compile_pred thy codegen_mode defs dep module prfx' all_vs arg_vs modes s cls mode gr') (((the o AList.lookup (op =) modes) s))) preds (gr, "fun ") in @@ -562,18 +564,19 @@ NONE => xs | SOME xs' => inter (op = o apfst fst) xs' xs) :: constrain cs ys; -fun mk_extra_defs thy defs gr dep names module ts = +fun mk_extra_defs thy codegen_mode defs gr dep names module ts = fold (fn name => fn gr => if member (op =) names name then gr else (case get_clauses thy name of NONE => gr | SOME (names, thyname, nparms, intrs) => - mk_ind_def thy defs gr dep names (Codegen.if_library thyname module) + mk_ind_def thy codegen_mode defs gr dep names + (Codegen.if_library codegen_mode thyname module) [] (prep_intrs intrs) nparms)) (fold Term.add_const_names ts []) gr -and mk_ind_def thy defs gr dep names module modecs intrs nparms = +and mk_ind_def thy codegen_mode defs gr dep names module modecs intrs nparms = Codegen.add_edge_acyclic (hd names, dep) gr handle Graph.CYCLES (xs :: _) => error ("Inductive_Codegen: illegal cyclic dependencies:\n" ^ commas xs) @@ -617,16 +620,16 @@ length Us)) arities) end; - val gr' = mk_extra_defs thy defs + val gr' = mk_extra_defs thy codegen_mode defs (Codegen.add_edge (hd names, dep) (Codegen.new_node (hd names, (NONE, "", "")) gr)) (hd names) names module intrs; val (extra_modes, extra_arities) = lookup_modes gr' (hd names); val (clauses, arities) = fold add_clause intrs ([], []); val modes = constrain modecs - (infer_modes thy extra_modes arities arg_vs clauses); + (infer_modes thy codegen_mode extra_modes arities arg_vs clauses); val _ = print_arities arities; val _ = print_modes modes; - val (s, gr'') = compile_preds thy defs (hd names) module (terms_vs intrs) + val (s, gr'') = compile_preds thy codegen_mode defs (hd names) module (terms_vs intrs) arg_vs (modes @ extra_modes) clauses gr'; in (Codegen.map_node (hd names) @@ -639,7 +642,7 @@ ("No such mode for " ^ s ^ ": " ^ string_of_mode ([], is)) | mode => mode); -fun mk_ind_call thy defs dep module is_query s T ts names thyname k intrs gr = +fun mk_ind_call thy codegen_mode defs dep module is_query s T ts names thyname k intrs gr = let val (ts1, ts2) = chop k ts; val u = list_comb (Const (s, T), ts1); @@ -647,9 +650,9 @@ fun mk_mode (Const (@{const_name dummy_pattern}, _)) ((ts, mode), i) = ((ts, mode), i + 1) | mk_mode t ((ts, mode), i) = ((ts @ [t], mode @ [i]), i + 1); - val module' = Codegen.if_library thyname module; - val gr1 = mk_extra_defs thy defs - (mk_ind_def thy defs gr dep names module' + val module' = Codegen.if_library codegen_mode thyname module; + val gr1 = mk_extra_defs thy codegen_mode defs + (mk_ind_def thy codegen_mode defs gr dep names module' [] (prep_intrs intrs) k) dep names module' [u]; val (modes, _) = lookup_modes gr1 dep; val (ts', is) = @@ -658,8 +661,9 @@ val mode = find_mode gr1 dep s u modes is; val _ = if is_query orelse not (needs_random (the mode)) then () else warning ("Illegal use of random data generators in " ^ s); - val (in_ps, gr2) = fold_map (Codegen.invoke_codegen thy defs dep module true) ts' gr1; - val (ps, gr3) = compile_expr thy defs dep module false modes (mode, u) gr2; + val (in_ps, gr2) = + fold_map (Codegen.invoke_codegen thy codegen_mode defs dep module true) ts' gr1; + val (ps, gr3) = compile_expr thy codegen_mode defs dep module false modes (mode, u) gr2; in (Pretty.block (ps @ (if null in_ps then [] else [Pretty.brk 1]) @ separate (Pretty.brk 1) in_ps), gr3) @@ -675,7 +679,7 @@ (list_comb (Const (s ^ "_aux", Ts @ [U] ---> HOLogic.boolT), ts @ [u])))) end; -fun mk_fun thy defs name eqns dep module module' gr = +fun mk_fun thy codegen_mode defs name eqns dep module module' gr = case try (Codegen.get_node gr) name of NONE => let @@ -693,7 +697,7 @@ Pretty.brk 1, Codegen.str "DSeq.hd", Pretty.brk 1, Codegen.parens (Pretty.block (separate (Pretty.brk 1) (Codegen.str mode_id :: vars)))]) ^ ";\n\n"; - val gr'' = mk_ind_def thy defs (Codegen.add_edge (name, dep) + val gr'' = mk_ind_def thy codegen_mode defs (Codegen.add_edge (name, dep) (Codegen.new_node (name, (NONE, module', s)) gr')) name [pname] module' [(pname, [([], mode)])] clauses 0; val (modes, _) = lookup_modes gr'' dep; @@ -726,7 +730,7 @@ else p end; -fun inductive_codegen thy defs dep module brack t gr = (case strip_comb t of +fun inductive_codegen thy codegen_mode defs dep module brack t gr = (case strip_comb t of (Const (@{const_name Collect}, _), [u]) => let val (r, Ts, fs) = HOLogic.strip_psplits u in case strip_comb r of @@ -743,7 +747,7 @@ if null (duplicates op = ots) andalso closed ts1 andalso closed its then - let val (call_p, gr') = mk_ind_call thy defs dep module true + let val (call_p, gr') = mk_ind_call thy codegen_mode defs dep module true s T (ts1 @ ts2') names thyname k intrs gr in SOME ((if brack then Codegen.parens else I) (Pretty.block [Codegen.str "Set", Pretty.brk 1, Codegen.str "(DSeq.list_of", Pretty.brk 1, @@ -762,20 +766,21 @@ (case (get_clauses thy s, Codegen.get_assoc_code thy (s, T)) of (SOME (names, thyname, k, intrs), NONE) => if length ts < k then NONE else SOME - (let val (call_p, gr') = mk_ind_call thy defs dep module false + (let val (call_p, gr') = mk_ind_call thy codegen_mode defs dep module false s T (map Term.no_dummy_patterns ts) names thyname k intrs gr in (mk_funcomp brack "?!" (length (binder_types T) - length ts) (Codegen.parens call_p), gr') - end handle TERM _ => mk_ind_call thy defs dep module true + end handle TERM _ => mk_ind_call thy codegen_mode defs dep module true s T ts names thyname k intrs gr ) | _ => NONE) | SOME eqns => let val (_, thyname) :: _ = eqns; - val (id, gr') = mk_fun thy defs s (Codegen.preprocess thy (map fst (rev eqns))) - dep module (Codegen.if_library thyname module) gr; - val (ps, gr'') = fold_map - (Codegen.invoke_codegen thy defs dep module true) ts gr'; + val (id, gr') = + mk_fun thy codegen_mode defs s (Codegen.preprocess thy (map fst (rev eqns))) + dep module (Codegen.if_library codegen_mode thyname module) gr; + val (ps, gr'') = + fold_map (Codegen.invoke_codegen thy codegen_mode defs dep module true) ts gr'; in SOME (Codegen.mk_app brack (Codegen.str id) ps, gr'') end) | _ => NONE); @@ -830,8 +835,9 @@ val pred = HOLogic.mk_Trueprop (list_comb (Const (Sign.intern_const thy' "quickcheckp", T), map Term.dummy_pattern Ts)); - val (code, gr) = setmp_CRITICAL Codegen.mode ["term_of", "test", "random_ind"] - (Codegen.generate_code_i thy' [] "Generated") [("testf", pred)]; + val (code, gr) = + Codegen.generate_code_i thy' ["term_of", "test", "random_ind"] [] "Generated" + [("testf", pred)]; val s = "structure TestTerm =\nstruct\n\n" ^ cat_lines (map snd code) ^ "\nopen Generated;\n\n" ^ Codegen.string_of diff -r 6bc725d60593 -r 6a2837ddde4b src/HOL/Tools/recfun_codegen.ML --- a/src/HOL/Tools/recfun_codegen.ML Wed Apr 20 10:14:24 2011 +0200 +++ b/src/HOL/Tools/recfun_codegen.ML Wed Apr 20 11:21:12 2011 +0200 @@ -70,7 +70,7 @@ if member (op =) xs x then xs else fold (cycle g) (flat (Graph.all_paths (fst g) (x, x))) (x :: xs); -fun add_rec_funs thy defs dep module eqs gr = +fun add_rec_funs thy mode defs dep module eqs gr = let fun dest_eq t = (fst (const_of t) ^ mk_suffix thy defs (const_of t), Logic.dest_equals (Codegen.rename_term t)); @@ -81,10 +81,10 @@ fun mk_fundef module fname first [] gr = ([], gr) | mk_fundef module fname first ((fname' : string, (lhs, rhs)) :: xs) gr = let - val (pl, gr1) = Codegen.invoke_codegen thy defs dname module false lhs gr; - val (pr, gr2) = Codegen.invoke_codegen thy defs dname module false rhs gr1; + val (pl, gr1) = Codegen.invoke_codegen thy mode defs dname module false lhs gr; + val (pr, gr2) = Codegen.invoke_codegen thy mode defs dname module false rhs gr1; val (rest, gr3) = mk_fundef module fname' false xs gr2 ; - val (ty, gr4) = Codegen.invoke_tycodegen thy defs dname module false T gr3; + val (ty, gr4) = Codegen.invoke_tycodegen thy mode defs dname module false T gr3; val num_args = (length o snd o strip_comb) lhs; val prfx = if fname = fname' then " |" else if not first then "and" @@ -121,7 +121,7 @@ if not (member (op =) xs dep) then let val thmss as (_, thyname) :: _ = map (get_equations thy defs) cs; - val module' = Codegen.if_library thyname module; + val module' = Codegen.if_library mode thyname module; val eqs'' = map (dest_eq o prop_of) (maps fst thmss); val (fundef', gr3) = mk_fundef module' "" true eqs'' (Codegen.add_edge (dname, dep) @@ -137,7 +137,7 @@ else if s = dep then gr else Codegen.add_edge (s, dep) gr)) end; -fun recfun_codegen thy defs dep module brack t gr = +fun recfun_codegen thy mode defs dep module brack t gr = (case strip_comb t of (Const (p as (s, T)), ts) => (case (get_equations thy defs p, Codegen.get_assoc_code thy (s, T)) of @@ -145,12 +145,12 @@ | (_, SOME _) => NONE | ((eqns, thyname), NONE) => let - val module' = Codegen.if_library thyname module; + val module' = Codegen.if_library mode thyname module; val (ps, gr') = fold_map - (Codegen.invoke_codegen thy defs dep module true) ts gr; + (Codegen.invoke_codegen thy mode defs dep module true) ts gr; val suffix = mk_suffix thy defs p; val (module'', gr'') = - add_rec_funs thy defs dep module' (map prop_of eqns) gr'; + add_rec_funs thy mode defs dep module' (map prop_of eqns) gr'; val (fname, gr''') = Codegen.mk_const_id module'' (s ^ suffix) gr'' in SOME (Codegen.mk_app brack (Codegen.str (Codegen.mk_qual_id module fname)) ps, gr''') diff -r 6bc725d60593 -r 6a2837ddde4b src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Wed Apr 20 10:14:24 2011 +0200 +++ b/src/Pure/IsaMakefile Wed Apr 20 11:21:12 2011 +0200 @@ -253,6 +253,7 @@ thm.ML \ type.ML \ type_infer.ML \ + type_infer_context.ML \ unify.ML \ variable.ML @./mk diff -r 6bc725d60593 -r 6a2837ddde4b src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Wed Apr 20 10:14:24 2011 +0200 +++ b/src/Pure/Isar/class.ML Wed Apr 20 11:21:12 2011 +0200 @@ -462,7 +462,7 @@ handle Sorts.CLASS_ERROR e => error (Sorts.class_error ctxt e); val inst = map_type_tvar (fn (vi, sort) => TVar (vi, the_default sort (Vartab.lookup tvartab vi))); - in if Vartab.is_empty tvartab then NONE else SOME ((map o map_types) inst ts) end; + in if Vartab.is_empty tvartab then ts else (map o map_types) inst ts end; (* target *) @@ -535,10 +535,7 @@ val consts = Sign.consts_of thy; val improve_constraints = AList.lookup (op =) (map (fn (_, (class, (c, _))) => (c, [[class]])) class_params); - fun resort_check ts ctxt = - (case resort_terms ctxt algebra consts improve_constraints ts of - NONE => NONE - | SOME ts' => SOME (ts', ctxt)); + fun resort_check ctxt ts = resort_terms ctxt algebra consts improve_constraints ts; val lookup_inst_param = AxClass.lookup_inst_param consts params; fun improve (c, ty) = (case lookup_inst_param (c, ty) of diff -r 6bc725d60593 -r 6a2837ddde4b src/Pure/Isar/class_declaration.ML --- a/src/Pure/Isar/class_declaration.ML Wed Apr 20 10:14:24 2011 +0200 +++ b/src/Pure/Isar/class_declaration.ML Wed Apr 20 11:21:12 2011 +0200 @@ -139,19 +139,18 @@ (fn T as TFree _ => T | T as TVar (vi, _) => if Type_Infer.is_param vi then Type_Infer.param 0 (Name.aT, sort') else T) Ts end; - fun add_typ_check level name f = Context.proof_map - (Syntax.add_typ_check level name (fn Ts => fn ctxt => - let val Ts' = f Ts in if eq_list (op =) (Ts, Ts') then NONE else SOME (Ts', ctxt) end)); (* preprocessing elements, retrieving base sort from type-checked elements *) - val raw_supexpr = (map (fn sup => (sup, (("", false), - Expression.Positional []))) sups, []); - val init_class_body = fold (Proof_Context.add_const_constraint o apsnd SOME) base_constraints + val raw_supexpr = + (map (fn sup => (sup, (("", false), Expression.Positional []))) sups, []); + val init_class_body = + fold (Proof_Context.add_const_constraint o apsnd SOME) base_constraints #> Class.redeclare_operations thy sups - #> add_typ_check 10 "reject_bcd_etc" reject_bcd_etc - #> add_typ_check ~10 "singleton_fixate" singleton_fixate; - val ((raw_supparams, _, raw_inferred_elems), _) = Proof_Context.init_global thy - |> add_typ_check 5 "after_infer_fixate" after_infer_fixate + #> Context.proof_map (Syntax.add_typ_check 10 "reject_bcd_etc" (K reject_bcd_etc)) + #> Context.proof_map (Syntax.add_typ_check ~10 "singleton_fixate" (K singleton_fixate)); + val ((raw_supparams, _, raw_inferred_elems), _) = + Proof_Context.init_global thy + |> Context.proof_map (Syntax.add_typ_check 5 "after_infer_fixate" (K after_infer_fixate)) |> prep_decl raw_supexpr init_class_body raw_elems; fun filter_element (Element.Fixes []) = NONE | filter_element (e as Element.Fixes _) = SOME e @@ -165,7 +164,7 @@ fun fold_element_types f (Element.Fixes fxs) = fold (fn (_, SOME T, _) => f T) fxs | fold_element_types f (Element.Constrains cnstrs) = fold (f o snd) cnstrs | fold_element_types f (Element.Assumes assms) = fold (fold (fn (t, ts) => - fold_types f t #> (fold o fold_types) f ts) o snd) assms + fold_types f t #> (fold o fold_types) f ts) o snd) assms; val base_sort = if null inferred_elems then proto_base_sort else case (fold o fold_element_types) Term.add_tfreesT inferred_elems [] of [] => error "No type variable in class specification" diff -r 6bc725d60593 -r 6a2837ddde4b src/Pure/Isar/overloading.ML --- a/src/Pure/Isar/overloading.ML Wed Apr 20 10:14:24 2011 +0200 +++ b/src/Pure/Isar/overloading.ML Wed Apr 20 11:21:12 2011 +0200 @@ -19,13 +19,13 @@ structure Overloading: OVERLOADING = struct -(** generic check/uncheck combinators for improvable constants **) +(* generic check/uncheck combinators for improvable constants *) type improvable_syntax = ((((string * typ) list * (string * typ) list) * ((((string * typ -> (typ * typ) option) * (string * typ -> (typ * term) option)) * bool) * (term * term) list)) * bool); -structure ImprovableSyntax = Proof_Data +structure Improvable_Syntax = Proof_Data ( type T = { primary_constraints: (string * typ) list, @@ -47,16 +47,17 @@ }; ); -fun map_improvable_syntax f = ImprovableSyntax.map (fn { primary_constraints, - secondary_constraints, improve, subst, consider_abbrevs, unchecks, passed } => +fun map_improvable_syntax f = Improvable_Syntax.map (fn {primary_constraints, + secondary_constraints, improve, subst, consider_abbrevs, unchecks, passed} => let val (((primary_constraints', secondary_constraints'), (((improve', subst'), consider_abbrevs'), unchecks')), passed') = f (((primary_constraints, secondary_constraints), (((improve, subst), consider_abbrevs), unchecks)), passed) - in { primary_constraints = primary_constraints', secondary_constraints = secondary_constraints', + in + {primary_constraints = primary_constraints', secondary_constraints = secondary_constraints', improve = improve', subst = subst', consider_abbrevs = consider_abbrevs', - unchecks = unchecks', passed = passed' } + unchecks = unchecks', passed = passed'} end); val mark_passed = (map_improvable_syntax o apsnd) (K true); @@ -65,8 +66,8 @@ let val thy = Proof_Context.theory_of ctxt; - val { secondary_constraints, improve, subst, consider_abbrevs, passed, ... } = - ImprovableSyntax.get ctxt; + val {secondary_constraints, improve, subst, consider_abbrevs, passed, ...} = + Improvable_Syntax.get ctxt; val is_abbrev = consider_abbrevs andalso Proof_Context.abbrev_mode ctxt; val passed_or_abbrev = passed orelse is_abbrev; fun accumulate_improvements (Const (c, ty)) = @@ -87,38 +88,38 @@ | _ => NONE) t; val ts'' = if is_abbrev then ts' else map apply_subst ts'; in - if eq_list (op aconv) (ts, ts'') andalso passed_or_abbrev then NONE else - if passed_or_abbrev then SOME (ts'', ctxt) - else SOME (ts'', ctxt - |> fold (Proof_Context.add_const_constraint o apsnd SOME) secondary_constraints - |> mark_passed) + if eq_list (op aconv) (ts, ts'') andalso passed_or_abbrev then NONE + else if passed_or_abbrev then SOME (ts'', ctxt) + else + SOME (ts'', ctxt + |> fold (Proof_Context.add_const_constraint o apsnd SOME) secondary_constraints + |> mark_passed) end; fun rewrite_liberal thy unchecks t = - case try (Pattern.rewrite_term thy unchecks []) t - of NONE => NONE - | SOME t' => if t aconv t' then NONE else SOME t'; + (case try (Pattern.rewrite_term thy unchecks []) t of + NONE => NONE + | SOME t' => if t aconv t' then NONE else SOME t'); fun improve_term_uncheck ts ctxt = let val thy = Proof_Context.theory_of ctxt; - val unchecks = (#unchecks o ImprovableSyntax.get) ctxt; + val {unchecks, ...} = Improvable_Syntax.get ctxt; val ts' = map (rewrite_liberal thy unchecks) ts; in if exists is_some ts' then SOME (map2 the_default ts ts', ctxt) else NONE end; fun set_primary_constraints ctxt = - let - val { primary_constraints, ... } = ImprovableSyntax.get ctxt; + let val {primary_constraints, ...} = Improvable_Syntax.get ctxt; in fold (Proof_Context.add_const_constraint o apsnd SOME) primary_constraints ctxt end; val activate_improvable_syntax = Context.proof_map - (Syntax.add_term_check 0 "improvement" improve_term_check - #> Syntax.add_term_uncheck 0 "improvement" improve_term_uncheck) + (Syntax.context_term_check 0 "improvement" improve_term_check + #> Syntax.context_term_uncheck 0 "improvement" improve_term_uncheck) #> set_primary_constraints; -(** overloading target **) +(* overloading target *) structure Data = Proof_Data ( @@ -129,16 +130,18 @@ val get_overloading = Data.get o Local_Theory.target_of; val map_overloading = Local_Theory.target o Data.map; -fun operation lthy b = get_overloading lthy +fun operation lthy b = + get_overloading lthy |> get_first (fn ((c, _), (v, checked)) => if Binding.name_of b = v then SOME (c, (v, checked)) else NONE); fun synchronize_syntax ctxt = let val overloading = Data.get ctxt; - fun subst (c, ty) = case AList.lookup (op =) overloading (c, ty) - of SOME (v, _) => SOME (ty, Free (v, ty)) - | NONE => NONE; + fun subst (c, ty) = + (case AList.lookup (op =) overloading (c, ty) of + SOME (v, _) => SOME (ty, Free (v, ty)) + | NONE => NONE); val unchecks = map (fn (c_ty as (_, ty), (v, _)) => (Free (v, ty), Const c_ty)) overloading; in @@ -155,12 +158,13 @@ #-> (fn (_, def) => pair (Const (c, U), def)) fun foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy = - case operation lthy b - of SOME (c, (v, checked)) => if mx <> NoSyn - then error ("Illegal mixfix syntax for overloaded constant " ^ quote c) - else lthy |> define_overloaded (c, U) (v, checked) (b_def, rhs) - | NONE => lthy |> - Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params); + (case operation lthy b of + SOME (c, (v, checked)) => + if mx <> NoSyn + then error ("Illegal mixfix syntax for overloaded constant " ^ quote c) + else lthy |> define_overloaded (c, U) (v, checked) (b_def, rhs) + | NONE => lthy + |> Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params)); fun pretty lthy = let @@ -177,8 +181,8 @@ val _ = if null overloading then () else - error ("Missing definition(s) for parameter(s) " ^ commas (map (quote - o Syntax.string_of_term lthy o Const o fst) overloading)); + error ("Missing definition(s) for parameter(s) " ^ + commas_quote (map (Syntax.string_of_term lthy o Const o fst) overloading)); in lthy end; fun gen_overloading prep_const raw_overloading thy = diff -r 6bc725d60593 -r 6a2837ddde4b src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Wed Apr 20 10:14:24 2011 +0200 +++ b/src/Pure/Isar/proof_context.ML Wed Apr 20 11:21:12 2011 +0200 @@ -76,7 +76,6 @@ val get_sort: Proof.context -> (indexname * sort) list -> indexname -> sort val check_tvar: Proof.context -> indexname * sort -> indexname * sort val check_tfree: Proof.context -> string * sort -> string * sort - val standard_infer_types: Proof.context -> term list -> term list val intern_skolem: Proof.context -> string -> string option val read_term_pattern: Proof.context -> string -> term val read_term_schematic: Proof.context -> string -> term @@ -678,38 +677,27 @@ end; -(* type checking/inference *) +(* check/uncheck *) fun def_type ctxt = let val Mode {pattern, ...} = get_mode ctxt in Variable.def_type ctxt pattern end; -fun standard_infer_types ctxt = - Type_Infer.infer_types ctxt (try (Consts.the_constraint (consts_of ctxt))) (def_type ctxt); - local fun standard_typ_check ctxt = map (cert_typ_mode (Type.get_mode ctxt) ctxt) #> map (prepare_patternT ctxt); -fun standard_term_check ctxt = - standard_infer_types ctxt #> - map (expand_abbrevs ctxt); - fun standard_term_uncheck ctxt = map (contract_abbrevs ctxt); -fun add eq what f = Context.>> (what (fn xs => fn ctxt => - let val xs' = f ctxt xs in if eq_list eq (xs, xs') then NONE else SOME (xs', ctxt) end)); - in -val _ = add (op =) (Syntax.add_typ_check 0 "standard") standard_typ_check; -val _ = add (op aconv) (Syntax.add_term_check 0 "standard") standard_term_check; -val _ = add (op aconv) (Syntax.add_term_check 100 "fixate") prepare_patterns; - -val _ = add (op aconv) (Syntax.add_term_uncheck 0 "standard") standard_term_uncheck; +val _ = Context.>> + (Syntax.add_typ_check 0 "standard" standard_typ_check #> + Syntax.add_term_check 100 "fixate" prepare_patterns #> + Syntax.add_term_uncheck 0 "standard" standard_term_uncheck); end; diff -r 6bc725d60593 -r 6a2837ddde4b src/Pure/Isar/skip_proof.ML --- a/src/Pure/Isar/skip_proof.ML Wed Apr 20 10:14:24 2011 +0200 +++ b/src/Pure/Isar/skip_proof.ML Wed Apr 20 11:21:12 2011 +0200 @@ -7,6 +7,7 @@ signature SKIP_PROOF = sig + val make_thm_cterm: cterm -> thm val make_thm: theory -> term -> thm val cheat_tac: theory -> tactic val prove: Proof.context -> string list -> term list -> term -> @@ -20,14 +21,14 @@ (* oracle setup *) -val (_, skip_proof) = Context.>>> (Context.map_theory_result - (Thm.add_oracle (Binding.name "skip_proof", fn (thy, prop) => Thm.cterm_of thy prop))); +val (_, make_thm_cterm) = + Context.>>> (Context.map_theory_result (Thm.add_oracle (Binding.name "skip_proof", I))); + +fun make_thm thy prop = make_thm_cterm (Thm.cterm_of thy prop); (* basic cheating *) -fun make_thm thy prop = skip_proof (thy, prop); - fun cheat_tac thy st = ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st; diff -r 6bc725d60593 -r 6a2837ddde4b src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Wed Apr 20 10:14:24 2011 +0200 +++ b/src/Pure/Proof/extraction.ML Wed Apr 20 11:21:12 2011 +0200 @@ -32,16 +32,17 @@ (**** tools ****) -fun add_syntax thy = - thy - |> Theory.copy - |> Sign.root_path - |> Sign.add_types_global [(Binding.name "Type", 0, NoSyn), (Binding.name "Null", 0, NoSyn)] - |> Sign.add_consts - [(Binding.name "typeof", "'b::{} => Type", NoSyn), - (Binding.name "Type", "'a::{} itself => Type", NoSyn), - (Binding.name "Null", "Null", NoSyn), - (Binding.name "realizes", "'a::{} => 'b::{} => 'b", NoSyn)]; +val typ = Simple_Syntax.read_typ; + +val add_syntax = + Theory.copy + #> Sign.root_path + #> Sign.add_types_global [(Binding.name "Type", 0, NoSyn), (Binding.name "Null", 0, NoSyn)] + #> Sign.add_consts_i + [(Binding.name "typeof", typ "'b => Type", NoSyn), + (Binding.name "Type", typ "'a itself => Type", NoSyn), + (Binding.name "Null", typ "Null", NoSyn), + (Binding.name "realizes", typ "'a => 'b => 'b", NoSyn)]; val nullT = Type ("Null", []); val nullt = Const ("Null", nullT); @@ -150,11 +151,13 @@ let val vs = Term.add_vars t []; val fs = Term.add_frees t []; - in fn - Var (ixn, _) => (case AList.lookup (op =) vs ixn of + in + fn Var (ixn, _) => + (case AList.lookup (op =) vs ixn of NONE => error "get_var_type: no such variable in term" | SOME T => Var (ixn, T)) - | Free (s, _) => (case AList.lookup (op =) fs s of + | Free (s, _) => + (case AList.lookup (op =) fs s of NONE => error "get_var_type: no such variable in term" | SOME T => Free (s, T)) | _ => error "get_var_type: not a variable" @@ -163,7 +166,7 @@ fun read_term thy T s = let val ctxt = Proof_Context.init_global thy - |> Proof_Syntax.strip_sorts_consttypes + |> Config.put Type_Infer_Context.const_sorts false |> Proof_Context.set_defsort []; val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term; in parse ctxt s |> Type.constraint T |> Syntax.check_term ctxt end; @@ -528,7 +531,7 @@ | corr d defs vs ts Ts hs cs (AbsP (s, SOME prop, prf)) (AbsP (_, _, prf')) t = let val T = etype_of thy' vs Ts prop; - val u = if T = nullT then + val u = if T = nullT then (case t of SOME u => SOME (incr_boundvars 1 u) | NONE => NONE) else (case t of SOME (Abs (_, _, u)) => SOME u | _ => NONE); val (defs', corr_prf) = diff -r 6bc725d60593 -r 6a2837ddde4b src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Wed Apr 20 10:14:24 2011 +0200 +++ b/src/Pure/Proof/proof_syntax.ML Wed Apr 20 11:21:12 2011 +0200 @@ -11,7 +11,6 @@ val proof_of_term: theory -> bool -> term -> Proofterm.proof val term_of_proof: Proofterm.proof -> term val cterm_of_proof: theory -> Proofterm.proof -> cterm * (cterm -> Proofterm.proof) - val strip_sorts_consttypes: Proof.context -> Proof.context val read_term: theory -> bool -> typ -> string -> term val read_proof: theory -> bool -> bool -> string -> Proofterm.proof val proof_syntax: Proofterm.proof -> theory -> theory @@ -201,13 +200,6 @@ (cterm_of thy' (term_of_proof prf), proof_of_term thy true o Thm.term_of) end; -fun strip_sorts_consttypes ctxt = - let val {constants = (_, tab), ...} = Consts.dest (Proof_Context.consts_of ctxt) - in Symtab.fold (fn (s, (T, _)) => - Proof_Context.add_const_constraint (s, SOME (Type.strip_sorts T))) - tab ctxt - end; - fun read_term thy topsort = let val thm_names = filter_out (fn s => s = "") (map fst (Global_Theory.all_thms_of thy)); @@ -219,10 +211,7 @@ |> Proof_Context.init_global |> Proof_Context.allow_dummies |> Proof_Context.set_mode Proof_Context.mode_schematic - |> (if topsort then - strip_sorts_consttypes #> - Proof_Context.set_defsort [] - else I); + |> topsort ? (Config.put Type_Infer_Context.const_sorts false #> Proof_Context.set_defsort []); in fn ty => fn s => (if ty = propT then Syntax.parse_prop else Syntax.parse_term) ctxt s diff -r 6bc725d60593 -r 6a2837ddde4b src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Wed Apr 20 10:14:24 2011 +0200 +++ b/src/Pure/ROOT.ML Wed Apr 20 11:21:12 2011 +0200 @@ -173,6 +173,7 @@ use "type_infer.ML"; use "Syntax/local_syntax.ML"; use "Isar/proof_context.ML"; +use "type_infer_context.ML"; use "Syntax/syntax_phases.ML"; use "Isar/local_defs.ML"; diff -r 6bc725d60593 -r 6a2837ddde4b src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Wed Apr 20 10:14:24 2011 +0200 +++ b/src/Pure/Syntax/syntax.ML Wed Apr 20 11:21:12 2011 +0200 @@ -31,18 +31,26 @@ val unparse_typ: Proof.context -> typ -> Pretty.T val unparse_term: Proof.context -> term -> Pretty.T val print_checks: Proof.context -> unit - val add_typ_check: int -> string -> + val context_typ_check: int -> string -> (typ list -> Proof.context -> (typ list * Proof.context) option) -> Context.generic -> Context.generic - val add_term_check: int -> string -> + val context_term_check: int -> string -> (term list -> Proof.context -> (term list * Proof.context) option) -> Context.generic -> Context.generic - val add_typ_uncheck: int -> string -> + val context_typ_uncheck: int -> string -> (typ list -> Proof.context -> (typ list * Proof.context) option) -> Context.generic -> Context.generic - val add_term_uncheck: int -> string -> + val context_term_uncheck: int -> string -> (term list -> Proof.context -> (term list * Proof.context) option) -> Context.generic -> Context.generic + val add_typ_check: int -> string -> (Proof.context -> typ list -> typ list) -> + Context.generic -> Context.generic + val add_term_check: int -> string -> (Proof.context -> term list -> term list) -> + Context.generic -> Context.generic + val add_typ_uncheck: int -> string -> (Proof.context -> typ list -> typ list) -> + Context.generic -> Context.generic + val add_term_uncheck: int -> string -> (Proof.context -> term list -> term list) -> + Context.generic -> Context.generic val typ_check: Proof.context -> typ list -> typ list val term_check: Proof.context -> term list -> term list val typ_uncheck: Proof.context -> typ list -> typ list @@ -224,13 +232,11 @@ (* context-sensitive (un)checking *) -local - type key = int * bool; -type 'a check = 'a list -> Proof.context -> ('a list * Proof.context) option; structure Checks = Generic_Data ( + type 'a check = 'a list -> Proof.context -> ('a list * Proof.context) option; type T = ((key * ((string * typ check) * stamp) list) list * (key * ((string * term check) * stamp) list) list); @@ -241,27 +247,6 @@ AList.join (op =) (K (Library.merge (eq_snd (op =)))) (term_checks1, term_checks2)); ); -fun gen_add which (key: key) name f = - Checks.map (which (AList.map_default op = (key, []) (cons ((name, f), stamp ())))); - -fun check_stage fs = perhaps_loop (perhaps_apply (map uncurry fs)); - -fun gen_check which uncheck ctxt0 xs0 = - let - val funs = which (Checks.get (Context.Proof ctxt0)) - |> map_filter (fn ((i, u), fs) => if uncheck = u then SOME (i, map (snd o fst) fs) else NONE) - |> Library.sort (int_ord o pairself fst) |> map snd - |> not uncheck ? map rev; - val check_all = perhaps_apply (map check_stage funs); - in #1 (perhaps check_all (xs0, ctxt0)) end; - -fun map_sort f S = - (case f (TFree ("", S)) of - TFree ("", S') => S' - | _ => raise TYPE ("map_sort", [TFree ("", S)], [])); - -in - fun print_checks ctxt = let fun split_checks checks = @@ -283,15 +268,50 @@ pretty_checks "term_unchecks" term_unchecks end |> Pretty.chunks |> Pretty.writeln; -fun add_typ_check stage = gen_add apfst (stage, false); -fun add_term_check stage = gen_add apsnd (stage, false); -fun add_typ_uncheck stage = gen_add apfst (stage, true); -fun add_term_uncheck stage = gen_add apsnd (stage, true); + +local + +fun context_check which (key: key) name f = + Checks.map (which (AList.map_default op = (key, []) (cons ((name, f), stamp ())))); + +fun simple_check eq f xs ctxt = + let val xs' = f ctxt xs + in if eq_list eq (xs, xs') then NONE else SOME (xs', ctxt) end; + +in + +fun context_typ_check stage = context_check apfst (stage, false); +fun context_term_check stage = context_check apsnd (stage, false); +fun context_typ_uncheck stage = context_check apfst (stage, true); +fun context_term_uncheck stage = context_check apsnd (stage, true); + +fun add_typ_check key name f = context_typ_check key name (simple_check (op =) f); +fun add_term_check key name f = context_term_check key name (simple_check (op aconv) f); +fun add_typ_uncheck key name f = context_typ_uncheck key name (simple_check (op =) f); +fun add_term_uncheck key name f = context_term_uncheck key name (simple_check (op aconv) f); -val typ_check = gen_check fst false; -val term_check = gen_check snd false; -val typ_uncheck = gen_check fst true; -val term_uncheck = gen_check snd true; +end; + + +local + +fun check_stage fs = perhaps_loop (perhaps_apply (map uncurry fs)); +fun check_all fs = perhaps_apply (map check_stage fs); + +fun check which uncheck ctxt0 xs0 = + let + val funs = which (Checks.get (Context.Proof ctxt0)) + |> map_filter (fn ((i, u), fs) => if uncheck = u then SOME (i, map (snd o fst) fs) else NONE) + |> Library.sort (int_ord o pairself fst) |> map snd + |> not uncheck ? map rev; + in #1 (perhaps (check_all funs) (xs0, ctxt0)) end; + +in + +val typ_check = check fst false; +val term_check = check snd false; +val typ_uncheck = check fst true; +val term_uncheck = check snd true; val check_typs = operation #check_typs; val check_terms = operation #check_terms; @@ -300,17 +320,30 @@ val check_typ = singleton o check_typs; val check_term = singleton o check_terms; val check_prop = singleton o check_props; -val check_sort = map_sort o check_typ; val uncheck_typs = operation #uncheck_typs; val uncheck_terms = operation #uncheck_terms; + +end; + + +(* derived operations for algebra of sorts *) + +local + +fun map_sort f S = + (case f (TFree ("", S)) of + TFree ("", S') => S' + | _ => raise TYPE ("map_sort", [TFree ("", S)], [])); + +in + +val check_sort = map_sort o check_typ; val uncheck_sort = map_sort o singleton o uncheck_typs; end; -(* derived operations for classrel and arity *) - val uncheck_classrel = map o singleton o uncheck_sort; fun unparse_classrel ctxt cs = Pretty.block (flat @@ -590,7 +623,7 @@ (* basic syntax *) val token_markers = - ["_tfree", "_tvar", "_free", "_bound", "_var", "_numeral", "_inner_string"]; + ["_tfree", "_tvar", "_free", "_bound", "_loose", "_var", "_numeral", "_inner_string"]; val basic_nonterms = (Lexicon.terminals @ ["logic", "type", "types", "sort", "classes", diff -r 6bc725d60593 -r 6a2837ddde4b src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Wed Apr 20 10:14:24 2011 +0200 +++ b/src/Pure/Syntax/syntax_phases.ML Wed Apr 20 11:21:12 2011 +0200 @@ -146,7 +146,7 @@ val c = get_type (Lexicon.str_of_token tok); val _ = report (Lexicon.pos_of_token tok) (markup_type ctxt) c; in [Ast.Constant (Lexicon.mark_type c)] end - | asts_of (Parser.Node ("_constrain_position", [pt as Parser.Tip tok])) = + | asts_of (Parser.Node ("_position", [pt as Parser.Tip tok])) = if constrain_pos then [Ast.Appl [Ast.Constant "_constrain", ast_of pt, Ast.Variable (Term_Position.encode (Lexicon.pos_of_token tok))]] @@ -464,7 +464,7 @@ | ast_of (t as _ $ _) = let val (f, args) = strip_comb t in Ast.mk_appl (ast_of f) (map ast_of args) end - | ast_of (Bound i) = Ast.Variable ("B." ^ string_of_int i) + | ast_of (Bound i) = Ast.Appl [Ast.Constant "_loose", Ast.Variable ("B." ^ string_of_int i)] | ast_of (Abs _) = raise Fail "simple_ast_of: Abs"; in ast_of end; @@ -610,6 +610,7 @@ | token_trans "_tvar" x = SOME (Pretty.mark_str (Markup.tvar, x)) | token_trans "_free" x = SOME (Pretty.marks_str (free_or_skolem ctxt x)) | token_trans "_bound" x = SOME (Pretty.mark_str (Markup.bound, x)) + | token_trans "_loose" x = SOME (Pretty.mark_str (Markup.malformed, x)) | token_trans "_var" x = SOME (Pretty.mark_str (var_or_skolem x)) | token_trans "_numeral" x = SOME (Pretty.mark_str (Markup.numeral, x)) | token_trans "_inner_string" x = SOME (Pretty.mark_str (Markup.inner_string, x)) diff -r 6bc725d60593 -r 6a2837ddde4b src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Wed Apr 20 10:14:24 2011 +0200 +++ b/src/Pure/Thy/thy_output.ML Wed Apr 20 11:21:12 2011 +0200 @@ -498,7 +498,7 @@ fun pretty_abbrev ctxt s = let - val t = Syntax.parse_term ctxt s |> singleton (Proof_Context.standard_infer_types ctxt); + val t = Syntax.read_term (Proof_Context.set_mode Proof_Context.mode_abbrev ctxt) s; fun err () = error ("Abbreviated constant expected: " ^ Syntax.string_of_term ctxt t); val (head, args) = Term.strip_comb t; val (c, T) = Term.dest_Const head handle TERM _ => err (); diff -r 6bc725d60593 -r 6a2837ddde4b src/Pure/codegen.ML --- a/src/Pure/codegen.ML Wed Apr 20 10:14:24 2011 +0200 +++ b/src/Pure/codegen.ML Wed Apr 20 11:21:12 2011 +0200 @@ -8,7 +8,6 @@ sig val quiet_mode : bool Unsynchronized.ref val message : string -> unit - val mode : string list Unsynchronized.ref val margin : int Unsynchronized.ref val string_of : Pretty.T -> string val str : string -> Pretty.T @@ -31,9 +30,9 @@ val preprocess: theory -> thm list -> thm list val preprocess_term: theory -> term -> term val print_codegens: theory -> unit - val generate_code: theory -> string list -> string -> (string * string) list -> + val generate_code: theory -> string list -> string list -> string -> (string * string) list -> (string * string) list * codegr - val generate_code_i: theory -> string list -> string -> (string * term) list -> + val generate_code_i: theory -> string list -> string list -> string -> (string * term) list -> (string * string) list * codegr val assoc_const: string * (term mixfix list * (string * string) list) -> theory -> theory @@ -46,9 +45,9 @@ val get_assoc_type: theory -> string -> (typ mixfix list * (string * string) list) option val codegen_error: codegr -> string -> string -> 'a - val invoke_codegen: theory -> deftab -> string -> string -> bool -> + val invoke_codegen: theory -> string list -> deftab -> string -> string -> bool -> term -> codegr -> Pretty.T * codegr - val invoke_tycodegen: theory -> deftab -> string -> string -> bool -> + val invoke_tycodegen: theory -> string list -> deftab -> string -> string -> bool -> typ -> codegr -> Pretty.T * codegr val mk_id: string -> string val mk_qual_id: string -> string * string -> string @@ -62,7 +61,7 @@ val rename_term: term -> term val new_names: term -> string list -> string list val new_name: term -> string -> string - val if_library: 'a -> 'a -> 'a + val if_library: string list -> 'a -> 'a -> 'a val get_defn: theory -> deftab -> string -> typ -> ((typ * (string * thm)) * int option) option val is_instance: typ -> typ -> bool @@ -105,8 +104,6 @@ val quiet_mode = Unsynchronized.ref true; fun message s = if !quiet_mode then () else writeln s; -val mode = Unsynchronized.ref ([] : string list); (* FIXME proper functional argument *) - val margin = Unsynchronized.ref 80; fun string_of p = Print_Mode.setmp [] (Pretty.string_of_margin (!margin)) p; @@ -171,13 +168,14 @@ (* type of code generators *) type 'a codegen = - theory -> (* theory in which generate_code was called *) - deftab -> (* definition table (for efficiency) *) - string -> (* node name of caller (for recording dependencies) *) - string -> (* module name of caller (for modular code generation) *) - bool -> (* whether to parenthesize generated expression *) - 'a -> (* item to generate code from *) - codegr -> (* code dependency graph *) + theory -> (* theory in which generate_code was called *) + string list -> (* mode *) + deftab -> (* definition table (for efficiency) *) + string -> (* node name of caller (for recording dependencies) *) + string -> (* module name of caller (for modular code generation) *) + bool -> (* whether to parenthesize generated expression *) + 'a -> (* item to generate code from *) + codegr -> (* code dependency graph *) (Pretty.T * codegr) option; @@ -478,8 +476,8 @@ fun get_assoc_code thy (s, T) = Option.map snd (find_first (fn ((s', T'), _) => s = s' andalso is_instance T T') (#consts (CodegenData.get thy))); -fun get_aux_code xs = map_filter (fn (m, code) => - if m = "" orelse member (op =) (!mode) m then SOME code else NONE) xs; +fun get_aux_code mode xs = map_filter (fn (m, code) => + if m = "" orelse member (op =) mode m then SOME code else NONE) xs; fun dest_prim_def t = let @@ -525,14 +523,14 @@ fun codegen_error (gr, _) dep s = error (s ^ "\nrequired by:\n" ^ commas (Graph.all_succs gr [dep])); -fun invoke_codegen thy defs dep module brack t gr = (case get_first - (fn (_, f) => f thy defs dep module brack t gr) (#codegens (CodegenData.get thy)) of +fun invoke_codegen thy mode defs dep module brack t gr = (case get_first + (fn (_, f) => f thy mode defs dep module brack t gr) (#codegens (CodegenData.get thy)) of NONE => codegen_error gr dep ("Unable to generate code for term:\n" ^ Syntax.string_of_term_global thy t) | SOME x => x); -fun invoke_tycodegen thy defs dep module brack T gr = (case get_first - (fn (_, f) => f thy defs dep module brack T gr ) (#tycodegens (CodegenData.get thy)) of +fun invoke_tycodegen thy mode defs dep module brack T gr = (case get_first + (fn (_, f) => f thy mode defs dep module brack T gr ) (#tycodegens (CodegenData.get thy)) of NONE => codegen_error gr dep ("Unable to generate code for type:\n" ^ Syntax.string_of_typ_global thy T) | SOME x => x); @@ -597,17 +595,17 @@ fun new_name t x = hd (new_names t [x]); -fun if_library x y = if member (op =) (!mode) "library" then x else y; +fun if_library mode x y = if member (op =) mode "library" then x else y; -fun default_codegen thy defs dep module brack t gr = +fun default_codegen thy mode defs dep module brack t gr = let val (u, ts) = strip_comb t; - fun codegens brack = fold_map (invoke_codegen thy defs dep module brack) + fun codegens brack = fold_map (invoke_codegen thy mode defs dep module brack) in (case u of Var ((s, i), T) => let val (ps, gr') = codegens true ts gr; - val (_, gr'') = invoke_tycodegen thy defs dep module false T gr' + val (_, gr'') = invoke_tycodegen thy mode defs dep module false T gr' in SOME (mk_app brack (str (s ^ (if i=0 then "" else string_of_int i))) ps, gr'') end @@ -615,7 +613,7 @@ | Free (s, T) => let val (ps, gr') = codegens true ts gr; - val (_, gr'') = invoke_tycodegen thy defs dep module false T gr' + val (_, gr'') = invoke_tycodegen thy mode defs dep module false T gr' in SOME (mk_app brack (str s) ps, gr'') end | Const (s, T) => @@ -623,26 +621,26 @@ SOME (ms, aux) => let val i = num_args_of ms in if length ts < i then - default_codegen thy defs dep module brack (eta_expand u ts i) gr + default_codegen thy mode defs dep module brack (eta_expand u ts i) gr else let val (ts1, ts2) = args_of ms ts; val (ps1, gr1) = codegens false ts1 gr; val (ps2, gr2) = codegens true ts2 gr1; val (ps3, gr3) = codegens false (quotes_of ms) gr2; - val (_, gr4) = invoke_tycodegen thy defs dep module false + val (_, gr4) = invoke_tycodegen thy mode defs dep module false (funpow (length ts) (hd o tl o snd o dest_Type) T) gr3; val (module', suffix) = (case get_defn thy defs s T of - NONE => (if_library (thyname_of_const thy s) module, "") + NONE => (if_library mode (thyname_of_const thy s) module, "") | SOME ((U, (module', _)), NONE) => - (if_library module' module, "") + (if_library mode module' module, "") | SOME ((U, (module', _)), SOME i) => - (if_library module' module, " def" ^ string_of_int i)); + (if_library mode module' module, " def" ^ string_of_int i)); val node_id = s ^ suffix; fun p module' = mk_app brack (Pretty.block (pretty_mixfix module module' ms ps1 ps3)) ps2 in SOME (case try (get_node gr4) node_id of - NONE => (case get_aux_code aux of + NONE => (case get_aux_code mode aux of [] => (p module, gr4) | xs => (p module', add_edge (node_id, dep) (new_node (node_id, (NONE, module', cat_lines xs ^ "\n")) gr4))) @@ -654,7 +652,7 @@ NONE => NONE | SOME ((U, (thyname, thm)), k) => (case prep_prim_def thy thm of SOME (_, (_, (args, rhs))) => let - val module' = if_library thyname module; + val module' = if_library mode thyname module; val suffix = (case k of NONE => "" | SOME i => " def" ^ string_of_int i); val node_id = s ^ suffix; val ((ps, def_id), gr') = gr |> codegens true ts @@ -669,12 +667,12 @@ if not (null args) orelse null Ts then (args, rhs) else let val v = Free (new_name rhs "x", hd Ts) in ([v], betapply (rhs, v)) end; - val (p', gr1) = invoke_codegen thy defs node_id module' false + val (p', gr1) = invoke_codegen thy mode defs node_id module' false rhs' (add_edge (node_id, dep) (new_node (node_id, (NONE, "", "")) gr')); val (xs, gr2) = codegens false args' gr1; - val (_, gr3) = invoke_tycodegen thy defs dep module false T gr2; - val (ty, gr4) = invoke_tycodegen thy defs node_id module' false U gr3; + val (_, gr3) = invoke_tycodegen thy mode defs dep module false T gr2; + val (ty, gr4) = invoke_tycodegen thy mode defs node_id module' false U gr3; in (p, map_node node_id (K (NONE, module', string_of (Pretty.block (separate (Pretty.brk 1) (if null args' then @@ -692,7 +690,7 @@ val t = strip_abs_body u val bs' = new_names t bs; val (ps, gr1) = codegens true ts gr; - val (p, gr2) = invoke_codegen thy defs dep module false + val (p, gr2) = invoke_codegen thy mode defs dep module false (subst_bounds (map Free (rev (bs' ~~ Ts)), t)) gr1; in SOME (mk_app brack (Pretty.block (str "(" :: pretty_fn bs' p @ @@ -702,26 +700,26 @@ | _ => NONE) end; -fun default_tycodegen thy defs dep module brack (TVar ((s, i), _)) gr = +fun default_tycodegen thy mode defs dep module brack (TVar ((s, i), _)) gr = SOME (str (s ^ (if i = 0 then "" else string_of_int i)), gr) - | default_tycodegen thy defs dep module brack (TFree (s, _)) gr = + | default_tycodegen thy mode defs dep module brack (TFree (s, _)) gr = SOME (str s, gr) - | default_tycodegen thy defs dep module brack (Type (s, Ts)) gr = + | default_tycodegen thy mode defs dep module brack (Type (s, Ts)) gr = (case AList.lookup (op =) ((#types o CodegenData.get) thy) s of NONE => NONE | SOME (ms, aux) => let val (ps, gr') = fold_map - (invoke_tycodegen thy defs dep module false) + (invoke_tycodegen thy mode defs dep module false) (fst (args_of ms Ts)) gr; val (qs, gr'') = fold_map - (invoke_tycodegen thy defs dep module false) + (invoke_tycodegen thy mode defs dep module false) (quotes_of ms) gr'; - val module' = if_library (thyname_of_type thy s) module; + val module' = if_library mode (thyname_of_type thy s) module; val node_id = s ^ " (type)"; fun p module' = Pretty.block (pretty_mixfix module module' ms ps qs) in SOME (case try (get_node gr'') node_id of - NONE => (case get_aux_code aux of + NONE => (case get_aux_code mode aux of [] => (p module', gr'') | xs => (p module', snd (mk_type_id module' s (add_edge (node_id, dep) (new_node (node_id, @@ -780,10 +778,10 @@ else [(module, implode (map (#3 o snd) code))] end; -fun gen_generate_code prep_term thy modules module xs = +fun gen_generate_code prep_term thy mode modules module xs = let val _ = (module <> "" orelse - member (op =) (!mode) "library" andalso forall (fn (s, _) => s = "") xs) + member (op =) mode "library" andalso forall (fn (s, _) => s = "") xs) orelse error "missing module name"; val graphs = get_modules thy; val defs = mk_deftab thy; @@ -800,7 +798,7 @@ | expand t = (case fastype_of t of Type ("fun", [T, U]) => Abs ("x", T, t $ Bound 0) | _ => t); val (ps, gr') = fold_map (fn (s, t) => fn gr => apfst (pair s) - (invoke_codegen thy defs "" module false t gr)) + (invoke_codegen thy mode defs "" module false t gr)) (map (apsnd (expand o preprocess_term thy o prep_term thy)) xs) gr; val code = map_filter (fn ("", _) => NONE @@ -809,12 +807,12 @@ val code' = space_implode "\n\n" code ^ "\n\n"; val code'' = map_filter (fn (name, s) => - if member (op =) (!mode) "library" andalso name = module andalso null code + if member (op =) mode "library" andalso name = module andalso null code then NONE else SOME (name, mk_struct name s)) ((if null code then I else add_to_module module code') - (output_code (fst gr') (if_library "" module) [""])) + (output_code (fst gr') (if_library mode "" module) [""])) in (code'', del_nodes [""] gr') end; @@ -873,8 +871,7 @@ fun test_term ctxt t = let val thy = Proof_Context.theory_of ctxt; - val (code, gr) = setmp_CRITICAL mode ["term_of", "test"] - (generate_code_i thy [] "Generated") [("testf", t)]; + val (code, gr) = generate_code_i thy ["term_of", "test"] [] "Generated" [("testf", t)]; val Ts = map snd (fst (strip_abs t)); val args = map_index (fn (i, T) => ("arg" ^ string_of_int i, T)) Ts; val s = "structure TestTerm =\nstruct\n\n" ^ @@ -913,9 +910,9 @@ error "Term to be evaluated contains type variables"; val _ = (null (Term.add_vars t []) andalso null (Term.add_frees t [])) orelse error "Term to be evaluated contains variables"; - val (code, gr) = setmp_CRITICAL mode ["term_of"] - (generate_code_i thy [] "Generated") - [("result", Abs ("x", TFree ("'a", []), t))]; + val (code, gr) = + generate_code_i thy ["term_of"] [] "Generated" + [("result", Abs ("x", TFree ("'a", []), t))]; val s = "structure EvalTerm =\nstruct\n\n" ^ cat_lines (map snd code) ^ "\nopen Generated;\n\n" ^ string_of @@ -988,7 +985,7 @@ (const, (parse_mixfix (Syntax.read_term_global thy) mfx, aux)))) xs thy))); fun parse_code lib = - Scan.optional (Parse.$$$ "(" |-- Parse.enum "," Parse.xname --| Parse.$$$ ")") (!mode) -- + Scan.optional (Parse.$$$ "(" |-- Parse.enum "," Parse.xname --| Parse.$$$ ")") [] -- (if lib then Scan.optional Parse.name "" else Parse.name) -- Scan.option (Parse.$$$ "file" |-- Parse.name) -- (if lib then Scan.succeed [] @@ -996,10 +993,10 @@ Parse.$$$ "contains" -- ( Scan.repeat1 (Parse.name --| Parse.$$$ "=" -- Parse.term) || Scan.repeat1 (Parse.term >> pair "")) >> - (fn ((((mode', module), opt_fname), modules), xs) => Toplevel.theory (fn thy => + (fn ((((mode, module), opt_fname), modules), xs) => Toplevel.theory (fn thy => let - val mode'' = (if lib then insert (op =) "library" else I) (remove (op =) "library" mode'); - val (code, gr) = setmp_CRITICAL mode mode'' (generate_code thy modules module) xs; + val mode' = (if lib then insert (op =) "library" else I) (remove (op =) "library" mode); + val (code, gr) = generate_code thy mode' modules module xs; val thy' = thy |> Context.theory_map (ML_Context.exec (fn () => (case opt_fname of NONE => ML_Context.eval_text false Position.none (cat_lines (map snd code)) diff -r 6bc725d60593 -r 6a2837ddde4b src/Pure/library.ML --- a/src/Pure/library.ML Wed Apr 20 10:14:24 2011 +0200 +++ b/src/Pure/library.ML Wed Apr 20 11:21:12 2011 +0200 @@ -93,7 +93,7 @@ val find_first: ('a -> bool) -> 'a list -> 'a option val get_index: ('a -> 'b option) -> 'a list -> (int * 'b) option val get_first: ('a -> 'b option) -> 'a list -> 'b option - val eq_list: ('a * 'b -> bool) -> 'a list * 'b list -> bool + val eq_list: ('a * 'a -> bool) -> 'a list * 'a list -> bool val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c val fold_rev2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c @@ -168,7 +168,7 @@ val inter: ('a * 'b -> bool) -> 'b list -> 'a list -> 'a list val merge: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list val subset: ('a * 'b -> bool) -> 'a list * 'b list -> bool - val eq_set: ('a * 'b -> bool) -> 'a list * 'b list -> bool + val eq_set: ('a * 'a -> bool) -> 'a list * 'a list -> bool val distinct: ('a * 'a -> bool) -> 'a list -> 'a list val duplicates: ('a * 'a -> bool) -> 'a list -> 'a list val has_duplicates: ('a * 'a -> bool) -> 'a list -> bool @@ -396,10 +396,11 @@ (* basic list functions *) fun eq_list eq (list1, list2) = - let - fun eq_lst (x :: xs, y :: ys) = eq (x, y) andalso eq_lst (xs, ys) - | eq_lst _ = true; - in length list1 = length list2 andalso eq_lst (list1, list2) end; + pointer_eq (list1, list2) orelse + let + fun eq_lst (x :: xs, y :: ys) = eq (x, y) andalso eq_lst (xs, ys) + | eq_lst _ = true; + in length list1 = length list2 andalso eq_lst (list1, list2) end; fun maps f [] = [] | maps f (x :: xs) = f x @ maps f xs; diff -r 6bc725d60593 -r 6a2837ddde4b src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Wed Apr 20 10:14:24 2011 +0200 +++ b/src/Pure/pure_thy.ML Wed Apr 20 11:21:12 2011 +0200 @@ -134,8 +134,8 @@ ("_struct", typ "index => logic", Mixfix ("\\_", [1000], 1000)), ("_update_name", typ "idt", NoSyn), ("_constrainAbs", typ "'a", NoSyn), - ("_constrain_position", typ "id => id_position", Delimfix "_"), - ("_constrain_position", typ "longid => longid_position", Delimfix "_"), + ("_position", typ "id => id_position", Delimfix "_"), + ("_position", typ "longid => longid_position", Delimfix "_"), ("_type_constraint_", typ "'a", NoSyn), ("_context_const", typ "id_position => logic", Delimfix "CONST _"), ("_context_const", typ "id_position => aprop", Delimfix "CONST _"), diff -r 6bc725d60593 -r 6a2837ddde4b src/Pure/type_infer.ML --- a/src/Pure/type_infer.ML Wed Apr 20 10:14:24 2011 +0200 +++ b/src/Pure/type_infer.ML Wed Apr 20 11:21:12 2011 +0200 @@ -1,13 +1,15 @@ (* Title: Pure/type_infer.ML Author: Stefan Berghofer and Markus Wenzel, TU Muenchen -Representation of type-inference problems. Simple type inference. +Basic representation of type-inference problems. *) signature TYPE_INFER = sig val is_param: indexname -> bool val is_paramT: typ -> bool + val param_maxidx: term -> int -> int + val param_maxidx_of: term list -> int val param: int -> string * sort -> typ val mk_param: int -> sort -> typ val anyT: sort -> typ @@ -16,10 +18,6 @@ val deref: typ Vartab.table -> typ -> typ val finish: Proof.context -> typ Vartab.table -> typ list * term list -> typ list * term list val fixate: Proof.context -> term list -> term list - val prepare: Proof.context -> (string -> typ option) -> (string * int -> typ option) -> - term list -> int * term list - val infer_types: Proof.context -> (string -> typ option) -> (indexname -> typ option) -> - term list -> term list end; structure Type_Infer: TYPE_INFER = @@ -34,6 +32,12 @@ fun is_paramT (TVar (xi, _)) = is_param xi | is_paramT _ = false; +val param_maxidx = + (Term.fold_types o Term.fold_atyps) + (fn (TVar (xi as (_, i), _)) => if is_param xi then Integer.max i else I | _ => I); + +fun param_maxidx_of ts = fold param_maxidx ts ~1; + fun param i (x, S) = TVar (("?" ^ x, i), S); fun mk_param i S = TVar (("?'a", i), S); @@ -62,96 +66,6 @@ -(** prepare types/terms: create inference parameters **) - -(* prepare_typ *) - -fun prepare_typ typ params_idx = - let - val (params', idx) = fold_atyps - (fn TVar (xi as (x, _), S) => - (fn ps_idx as (ps, idx) => - if is_param xi andalso not (Vartab.defined ps xi) - then (Vartab.update (xi, mk_param idx S) ps, idx + 1) else ps_idx) - | _ => I) typ params_idx; - - fun prepare (T as Type (a, Ts)) idx = - if T = dummyT then (mk_param idx [], idx + 1) - else - let val (Ts', idx') = fold_map prepare Ts idx - in (Type (a, Ts'), idx') end - | prepare (T as TVar (xi, _)) idx = - (case Vartab.lookup params' xi of - NONE => T - | SOME p => p, idx) - | prepare (TFree ("'_dummy_", S)) idx = (mk_param idx S, idx + 1) - | prepare (T as TFree _) idx = (T, idx); - - val (typ', idx') = prepare typ idx; - in (typ', (params', idx')) end; - - -(* prepare_term *) - -fun prepare_term ctxt const_type tm (vparams, params, idx) = - let - fun add_vparm xi (ps_idx as (ps, idx)) = - if not (Vartab.defined ps xi) then - (Vartab.update (xi, mk_param idx []) ps, idx + 1) - else ps_idx; - - val (vparams', idx') = fold_aterms - (fn Var (_, Type ("_polymorphic_", _)) => I - | Var (xi, _) => add_vparm xi - | Free (x, _) => add_vparm (x, ~1) - | _ => I) - tm (vparams, idx); - fun var_param xi = the (Vartab.lookup vparams' xi); - - fun polyT_of T idx = apsnd snd (prepare_typ (paramify_vars T) (Vartab.empty, idx)); - - fun constraint T t ps = - if T = dummyT then (t, ps) - else - let val (T', ps') = prepare_typ T ps - in (Type.constraint T' t, ps') end; - - fun prepare (Const ("_type_constraint_", T) $ t) ps_idx = - let - fun err () = - error ("Malformed internal type constraint: " ^ Syntax.string_of_typ ctxt T); - val A = (case T of Type ("fun", [A, B]) => if A = B then A else err () | _ => err ()); - val (A', ps_idx') = prepare_typ A ps_idx; - val (t', ps_idx'') = prepare t ps_idx'; - in (Const ("_type_constraint_", A' --> A') $ t', ps_idx'') end - | prepare (Const (c, T)) (ps, idx) = - (case const_type c of - SOME U => - let val (U', idx') = polyT_of U idx - in constraint T (Const (c, U')) (ps, idx') end - | NONE => error ("Undeclared constant: " ^ quote c)) - | prepare (Var (xi, Type ("_polymorphic_", [T]))) (ps, idx) = - let val (T', idx') = polyT_of T idx - in (Var (xi, T'), (ps, idx')) end - | prepare (Var (xi, T)) ps_idx = constraint T (Var (xi, var_param xi)) ps_idx - | prepare (Free (x, T)) ps_idx = constraint T (Free (x, var_param (x, ~1))) ps_idx - | prepare (Bound i) ps_idx = (Bound i, ps_idx) - | prepare (Abs (x, T, t)) ps_idx = - let - val (T', ps_idx') = prepare_typ T ps_idx; - val (t', ps_idx'') = prepare t ps_idx'; - in (Abs (x, T', t'), ps_idx'') end - | prepare (t $ u) ps_idx = - let - val (t', ps_idx') = prepare t ps_idx; - val (u', ps_idx'') = prepare u ps_idx'; - in (t' $ u', ps_idx'') end; - - val (tm', (params', idx'')) = prepare tm (params, idx'); - in (tm', (vparams', params', idx'')) end; - - - (** results **) (* dereferenced views *) @@ -160,7 +74,7 @@ (case Vartab.lookup tye xi of NONE => T | SOME U => deref tye U) - | deref tye T = T; + | deref _ T = T; fun add_parms tye T = (case deref tye T of @@ -211,148 +125,4 @@ val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) ([], used); in (map o map_types) (Term_Subst.instantiateT inst) ts end; - - -(** order-sorted unification of types **) - -exception NO_UNIFIER of string * typ Vartab.table; - -fun unify ctxt = - let - val thy = Proof_Context.theory_of ctxt; - val arity_sorts = Type.arity_sorts (Context.pretty ctxt) (Sign.tsig_of thy); - - - (* adjust sorts of parameters *) - - fun not_of_sort x S' S = - "Variable " ^ x ^ "::" ^ Syntax.string_of_sort ctxt S' ^ " not of sort " ^ - Syntax.string_of_sort ctxt S; - - fun meet (_, []) tye_idx = tye_idx - | meet (Type (a, Ts), S) (tye_idx as (tye, _)) = - meets (Ts, arity_sorts a S handle ERROR msg => raise NO_UNIFIER (msg, tye)) tye_idx - | meet (TFree (x, S'), S) (tye_idx as (tye, _)) = - if Sign.subsort thy (S', S) then tye_idx - else raise NO_UNIFIER (not_of_sort x S' S, tye) - | meet (TVar (xi, S'), S) (tye_idx as (tye, idx)) = - if Sign.subsort thy (S', S) then tye_idx - else if is_param xi then - (Vartab.update_new (xi, mk_param idx (Sign.inter_sort thy (S', S))) tye, idx + 1) - else raise NO_UNIFIER (not_of_sort (Term.string_of_vname xi) S' S, tye) - and meets (T :: Ts, S :: Ss) (tye_idx as (tye, _)) = - meets (Ts, Ss) (meet (deref tye T, S) tye_idx) - | meets _ tye_idx = tye_idx; - - - (* occurs check and assignment *) - - fun occurs_check tye xi (TVar (xi', S)) = - if xi = xi' then raise NO_UNIFIER ("Occurs check!", tye) - else - (case Vartab.lookup tye xi' of - NONE => () - | SOME T => occurs_check tye xi T) - | occurs_check tye xi (Type (_, Ts)) = List.app (occurs_check tye xi) Ts - | occurs_check _ _ _ = (); - - fun assign xi (T as TVar (xi', _)) S env = - if xi = xi' then env - else env |> meet (T, S) |>> Vartab.update_new (xi, T) - | assign xi T S (env as (tye, _)) = - (occurs_check tye xi T; env |> meet (T, S) |>> Vartab.update_new (xi, T)); - - - (* unification *) - - fun show_tycon (a, Ts) = - quote (Syntax.string_of_typ ctxt (Type (a, replicate (length Ts) dummyT))); - - fun unif (T1, T2) (env as (tye, _)) = - (case pairself (`is_paramT o deref tye) (T1, T2) of - ((true, TVar (xi, S)), (_, T)) => assign xi T S env - | ((_, T), (true, TVar (xi, S))) => assign xi T S env - | ((_, Type (a, Ts)), (_, Type (b, Us))) => - if a <> b then - raise NO_UNIFIER - ("Clash of types " ^ show_tycon (a, Ts) ^ " and " ^ show_tycon (b, Us), tye) - else fold unif (Ts ~~ Us) env - | ((_, T), (_, U)) => if T = U then env else raise NO_UNIFIER ("", tye)); - - in unif end; - - - -(** simple type inference **) - -(* infer *) - -fun infer ctxt = - let - (* errors *) - - fun prep_output tye bs ts Ts = - let - val (Ts_bTs', ts') = finish ctxt tye (Ts @ map snd bs, ts); - val (Ts', Ts'') = chop (length Ts) Ts_bTs'; - fun prep t = - let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts''))) - in Term.subst_bounds (map Syntax_Trans.mark_boundT xs, t) end; - in (map prep ts', Ts') end; - - fun err_loose i = error ("Loose bound variable: B." ^ string_of_int i); - - fun unif_failed msg = - "Type unification failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n\n"; - - fun err_appl msg tye bs t T u U = - let val ([t', u'], [T', U']) = prep_output tye bs [t, u] [T, U] - in error (unif_failed msg ^ Type.appl_error ctxt t' T' u' U' ^ "\n") end; - - - (* main *) - - fun inf _ (Const (_, T)) tye_idx = (T, tye_idx) - | inf _ (Free (_, T)) tye_idx = (T, tye_idx) - | inf _ (Var (_, T)) tye_idx = (T, tye_idx) - | inf bs (Bound i) tye_idx = - (snd (nth bs i handle Subscript => err_loose i), tye_idx) - | inf bs (Abs (x, T, t)) tye_idx = - let val (U, tye_idx') = inf ((x, T) :: bs) t tye_idx - in (T --> U, tye_idx') end - | inf bs (t $ u) tye_idx = - let - val (T, tye_idx') = inf bs t tye_idx; - val (U, (tye, idx)) = inf bs u tye_idx'; - val V = mk_param idx []; - val tye_idx'' = unify ctxt (U --> V, T) (tye, idx + 1) - handle NO_UNIFIER (msg, tye') => err_appl msg tye' bs t T u U; - in (V, tye_idx'') end; - - in inf [] end; - - -(* main interfaces *) - -fun prepare ctxt const_type var_type raw_ts = - let - val get_type = the_default dummyT o var_type; - val constrain_vars = Term.map_aterms - (fn Free (x, T) => Type.constraint T (Free (x, get_type (x, ~1))) - | Var (xi, T) => Type.constraint T (Var (xi, get_type xi)) - | t => t); - - val ts = burrow_types (Syntax.check_typs ctxt) raw_ts; - val (ts', (_, _, idx)) = - fold_map (prepare_term ctxt const_type o constrain_vars) ts - (Vartab.empty, Vartab.empty, 0); - in (idx, ts') end; - -fun infer_types ctxt const_type var_type raw_ts = - let - val (idx, ts) = prepare ctxt const_type var_type raw_ts; - val (tye, _) = fold (snd oo infer ctxt) ts (Vartab.empty, idx); - val (_, ts') = finish ctxt tye ([], ts); - in ts' end; - end; diff -r 6bc725d60593 -r 6a2837ddde4b src/Pure/type_infer_context.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/type_infer_context.ML Wed Apr 20 11:21:12 2011 +0200 @@ -0,0 +1,267 @@ +(* Title: Pure/type_infer_context.ML + Author: Stefan Berghofer and Markus Wenzel, TU Muenchen + +Type-inference preparation and standard type inference. +*) + +signature TYPE_INFER_CONTEXT = +sig + val const_sorts: bool Config.T + val prepare: Proof.context -> term list -> int * term list + val infer_types: Proof.context -> term list -> term list +end; + +structure Type_Infer_Context: TYPE_INFER_CONTEXT = +struct + +(** prepare types/terms: create inference parameters **) + +(* constraints *) + +val const_sorts = Config.bool (Config.declare "const_sorts" (K (Config.Bool true))); + +fun const_type ctxt = + try ((not (Config.get ctxt const_sorts) ? Type.strip_sorts) o + Consts.the_constraint (Proof_Context.consts_of ctxt)); + +fun var_type ctxt = the_default dummyT o Proof_Context.def_type ctxt; + + +(* prepare_typ *) + +fun prepare_typ typ params_idx = + let + val (params', idx) = fold_atyps + (fn TVar (xi, S) => + (fn ps_idx as (ps, idx) => + if Type_Infer.is_param xi andalso not (Vartab.defined ps xi) + then (Vartab.update (xi, Type_Infer.mk_param idx S) ps, idx + 1) else ps_idx) + | _ => I) typ params_idx; + + fun prepare (T as Type (a, Ts)) idx = + if T = dummyT then (Type_Infer.mk_param idx [], idx + 1) + else + let val (Ts', idx') = fold_map prepare Ts idx + in (Type (a, Ts'), idx') end + | prepare (T as TVar (xi, _)) idx = + (case Vartab.lookup params' xi of + NONE => T + | SOME p => p, idx) + | prepare (TFree ("'_dummy_", S)) idx = (Type_Infer.mk_param idx S, idx + 1) + | prepare (T as TFree _) idx = (T, idx); + + val (typ', idx') = prepare typ idx; + in (typ', (params', idx')) end; + + +(* prepare_term *) + +fun prepare_term ctxt tm (vparams, params, idx) = + let + fun add_vparm xi (ps_idx as (ps, idx)) = + if not (Vartab.defined ps xi) then + (Vartab.update (xi, Type_Infer.mk_param idx []) ps, idx + 1) + else ps_idx; + + val (vparams', idx') = fold_aterms + (fn Var (_, Type ("_polymorphic_", _)) => I + | Var (xi, _) => add_vparm xi + | Free (x, _) => add_vparm (x, ~1) + | _ => I) + tm (vparams, idx); + fun var_param xi = the (Vartab.lookup vparams' xi); + + fun polyT_of T idx = + apsnd snd (prepare_typ (Type_Infer.paramify_vars T) (Vartab.empty, idx)); + + fun constraint T t ps = + if T = dummyT then (t, ps) + else + let val (T', ps') = prepare_typ T ps + in (Type.constraint T' t, ps') end; + + fun prepare (Const ("_type_constraint_", T) $ t) ps_idx = + let + fun err () = + error ("Malformed internal type constraint: " ^ Syntax.string_of_typ ctxt T); + val A = (case T of Type ("fun", [A, B]) => if A = B then A else err () | _ => err ()); + val (A', ps_idx') = prepare_typ A ps_idx; + val (t', ps_idx'') = prepare t ps_idx'; + in (Const ("_type_constraint_", A' --> A') $ t', ps_idx'') end + | prepare (Const (c, T)) (ps, idx) = + (case const_type ctxt c of + SOME U => + let val (U', idx') = polyT_of U idx + in constraint T (Const (c, U')) (ps, idx') end + | NONE => error ("Undeclared constant: " ^ quote c)) + | prepare (Var (xi, Type ("_polymorphic_", [T]))) (ps, idx) = + let val (T', idx') = polyT_of T idx + in (Var (xi, T'), (ps, idx')) end + | prepare (Var (xi, T)) ps_idx = constraint T (Var (xi, var_param xi)) ps_idx + | prepare (Free (x, T)) ps_idx = constraint T (Free (x, var_param (x, ~1))) ps_idx + | prepare (Bound i) ps_idx = (Bound i, ps_idx) + | prepare (Abs (x, T, t)) ps_idx = + let + val (T', ps_idx') = prepare_typ T ps_idx; + val (t', ps_idx'') = prepare t ps_idx'; + in (Abs (x, T', t'), ps_idx'') end + | prepare (t $ u) ps_idx = + let + val (t', ps_idx') = prepare t ps_idx; + val (u', ps_idx'') = prepare u ps_idx'; + in (t' $ u', ps_idx'') end; + + val (tm', (params', idx'')) = prepare tm (params, idx'); + in (tm', (vparams', params', idx'')) end; + + + +(** order-sorted unification of types **) + +exception NO_UNIFIER of string * typ Vartab.table; + +fun unify ctxt = + let + val thy = Proof_Context.theory_of ctxt; + val arity_sorts = Type.arity_sorts (Context.pretty ctxt) (Sign.tsig_of thy); + + + (* adjust sorts of parameters *) + + fun not_of_sort x S' S = + "Variable " ^ x ^ "::" ^ Syntax.string_of_sort ctxt S' ^ " not of sort " ^ + Syntax.string_of_sort ctxt S; + + fun meet (_, []) tye_idx = tye_idx + | meet (Type (a, Ts), S) (tye_idx as (tye, _)) = + meets (Ts, arity_sorts a S handle ERROR msg => raise NO_UNIFIER (msg, tye)) tye_idx + | meet (TFree (x, S'), S) (tye_idx as (tye, _)) = + if Sign.subsort thy (S', S) then tye_idx + else raise NO_UNIFIER (not_of_sort x S' S, tye) + | meet (TVar (xi, S'), S) (tye_idx as (tye, idx)) = + if Sign.subsort thy (S', S) then tye_idx + else if Type_Infer.is_param xi then + (Vartab.update_new + (xi, Type_Infer.mk_param idx (Sign.inter_sort thy (S', S))) tye, idx + 1) + else raise NO_UNIFIER (not_of_sort (Term.string_of_vname xi) S' S, tye) + and meets (T :: Ts, S :: Ss) (tye_idx as (tye, _)) = + meets (Ts, Ss) (meet (Type_Infer.deref tye T, S) tye_idx) + | meets _ tye_idx = tye_idx; + + + (* occurs check and assignment *) + + fun occurs_check tye xi (TVar (xi', _)) = + if xi = xi' then raise NO_UNIFIER ("Occurs check!", tye) + else + (case Vartab.lookup tye xi' of + NONE => () + | SOME T => occurs_check tye xi T) + | occurs_check tye xi (Type (_, Ts)) = List.app (occurs_check tye xi) Ts + | occurs_check _ _ _ = (); + + fun assign xi (T as TVar (xi', _)) S env = + if xi = xi' then env + else env |> meet (T, S) |>> Vartab.update_new (xi, T) + | assign xi T S (env as (tye, _)) = + (occurs_check tye xi T; env |> meet (T, S) |>> Vartab.update_new (xi, T)); + + + (* unification *) + + fun show_tycon (a, Ts) = + quote (Syntax.string_of_typ ctxt (Type (a, replicate (length Ts) dummyT))); + + fun unif (T1, T2) (env as (tye, _)) = + (case pairself (`Type_Infer.is_paramT o Type_Infer.deref tye) (T1, T2) of + ((true, TVar (xi, S)), (_, T)) => assign xi T S env + | ((_, T), (true, TVar (xi, S))) => assign xi T S env + | ((_, Type (a, Ts)), (_, Type (b, Us))) => + if a <> b then + raise NO_UNIFIER + ("Clash of types " ^ show_tycon (a, Ts) ^ " and " ^ show_tycon (b, Us), tye) + else fold unif (Ts ~~ Us) env + | ((_, T), (_, U)) => if T = U then env else raise NO_UNIFIER ("", tye)); + + in unif end; + + + +(** simple type inference **) + +(* infer *) + +fun infer ctxt = + let + (* errors *) + + fun prep_output tye bs ts Ts = + let + val (Ts_bTs', ts') = Type_Infer.finish ctxt tye (Ts @ map snd bs, ts); + val (Ts', Ts'') = chop (length Ts) Ts_bTs'; + fun prep t = + let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts''))) + in Term.subst_bounds (map Syntax_Trans.mark_boundT xs, t) end; + in (map prep ts', Ts') end; + + fun err_loose i = error ("Loose bound variable: B." ^ string_of_int i); + + fun unif_failed msg = + "Type unification failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n\n"; + + fun err_appl msg tye bs t T u U = + let val ([t', u'], [T', U']) = prep_output tye bs [t, u] [T, U] + in error (unif_failed msg ^ Type.appl_error ctxt t' T' u' U' ^ "\n") end; + + + (* main *) + + fun inf _ (Const (_, T)) tye_idx = (T, tye_idx) + | inf _ (Free (_, T)) tye_idx = (T, tye_idx) + | inf _ (Var (_, T)) tye_idx = (T, tye_idx) + | inf bs (Bound i) tye_idx = + (snd (nth bs i handle Subscript => err_loose i), tye_idx) + | inf bs (Abs (x, T, t)) tye_idx = + let val (U, tye_idx') = inf ((x, T) :: bs) t tye_idx + in (T --> U, tye_idx') end + | inf bs (t $ u) tye_idx = + let + val (T, tye_idx') = inf bs t tye_idx; + val (U, (tye, idx)) = inf bs u tye_idx'; + val V = Type_Infer.mk_param idx []; + val tye_idx'' = unify ctxt (U --> V, T) (tye, idx + 1) + handle NO_UNIFIER (msg, tye') => err_appl msg tye' bs t T u U; + in (V, tye_idx'') end; + + in inf [] end; + + +(* main interfaces *) + +fun prepare ctxt raw_ts = + let + val constrain_vars = Term.map_aterms + (fn Free (x, T) => Type.constraint T (Free (x, var_type ctxt (x, ~1))) + | Var (xi, T) => Type.constraint T (Var (xi, var_type ctxt xi)) + | t => t); + + val ts = burrow_types (Syntax.check_typs ctxt) raw_ts; + val idx = Type_Infer.param_maxidx_of ts + 1; + val (ts', (_, _, idx')) = + fold_map (prepare_term ctxt o constrain_vars) ts + (Vartab.empty, Vartab.empty, idx); + in (idx', ts') end; + +fun infer_types ctxt raw_ts = + let + val (idx, ts) = prepare ctxt raw_ts; + val (tye, _) = fold (snd oo infer ctxt) ts (Vartab.empty, idx); + val (_, ts') = Type_Infer.finish ctxt tye ([], ts); + in ts' end; + +val _ = + Context.>> + (Syntax.add_term_check 0 "standard" + (fn ctxt => infer_types ctxt #> map (Proof_Context.expand_abbrevs ctxt))); + +end; diff -r 6bc725d60593 -r 6a2837ddde4b src/Tools/adhoc_overloading.ML --- a/src/Tools/adhoc_overloading.ML Wed Apr 20 10:14:24 2011 +0200 +++ b/src/Tools/adhoc_overloading.ML Wed Apr 20 11:21:12 2011 +0200 @@ -134,8 +134,8 @@ (* setup *) val setup = Context.theory_map - (Syntax.add_term_check 0 "adhoc_overloading" check - #> Syntax.add_term_check 1 "adhoc_overloading_unresolved_check" reject_unresolved - #> Syntax.add_term_uncheck 0 "adhoc_overloading" uncheck); + (Syntax.context_term_check 0 "adhoc_overloading" check + #> Syntax.context_term_check 1 "adhoc_overloading_unresolved_check" reject_unresolved + #> Syntax.context_term_uncheck 0 "adhoc_overloading" uncheck); end diff -r 6bc725d60593 -r 6a2837ddde4b src/Tools/nbe.ML --- a/src/Tools/nbe.ML Wed Apr 20 10:14:24 2011 +0200 +++ b/src/Tools/nbe.ML Wed Apr 20 11:21:12 2011 +0200 @@ -545,9 +545,9 @@ val ctxt = Syntax.init_pretty_global thy; val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt); val ty' = typ_of_itype program vs0 ty; - fun type_infer t = singleton - (Type_Infer.infer_types ctxt (try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE)) - (Type.constraint ty' t); + fun type_infer t = + Syntax.check_term (Config.put Type_Infer_Context.const_sorts false ctxt) + (Type.constraint ty' t); fun check_tvars t = if null (Term.add_tvars t []) then t else error ("Illegal schematic type variables in normalized term: " ^ string_of_term t); diff -r 6bc725d60593 -r 6a2837ddde4b src/Tools/subtyping.ML --- a/src/Tools/subtyping.ML Wed Apr 20 10:14:24 2011 +0200 +++ b/src/Tools/subtyping.ML Wed Apr 20 11:21:12 2011 +0200 @@ -6,13 +6,9 @@ signature SUBTYPING = sig - datatype variance = COVARIANT | CONTRAVARIANT | INVARIANT | INVARIANT_TO of typ; val coercion_enabled: bool Config.T - val infer_types: Proof.context -> (string -> typ option) -> (indexname -> typ option) -> - term list -> term list val add_type_map: term -> Context.generic -> Context.generic val add_coercion: term -> Context.generic -> Context.generic - val gen_coercion: Proof.context -> typ Vartab.table -> (typ * typ) -> term val setup: theory -> theory end; @@ -520,8 +516,8 @@ | SOME S => SOME (map nameT - (filter_out Type_Infer.is_paramT (map (Type_Infer.deref tye) (get_bound G T))), - S)); + (filter_out Type_Infer.is_paramT + (map (Type_Infer.deref tye) (get_bound G T))), S)); val styps_and_sorts = distinct (op =) (map_filter to_fulfil raw_bound); val assignment = if null bound orelse null not_params then NONE @@ -651,7 +647,8 @@ end | insert bs (t $ u) = let - val (t', Type ("fun", [U, T])) = apsnd (Type_Infer.deref tye) (insert bs t); + val (t', Type ("fun", [U, T])) = + apsnd (Type_Infer.deref tye) (insert bs t); val (u', U') = insert bs u; in if can (fn TU => strong_unify ctxt TU (tye, 0)) (U, U') @@ -666,9 +663,9 @@ (** assembling the pipeline **) -fun infer_types ctxt const_type var_type raw_ts = +fun coercion_infer_types ctxt raw_ts = let - val (idx, ts) = Type_Infer.prepare ctxt const_type var_type raw_ts; + val (idx, ts) = Type_Infer_Context.prepare ctxt raw_ts; fun inf _ (t as (Const (_, T))) tye_idx = (t, T, tye_idx) | inf _ (t as (Free (_, T))) tye_idx = (t, T, tye_idx) @@ -714,20 +711,12 @@ (* term check *) -fun coercion_infer_types ctxt = - infer_types ctxt - (try (Consts.the_constraint (Proof_Context.consts_of ctxt))) - (Proof_Context.def_type ctxt); - -val (coercion_enabled, coercion_enabled_setup) = Attrib.config_bool "coercion_enabled" (K false); +val (coercion_enabled, coercion_enabled_setup) = + Attrib.config_bool "coercion_enabled" (K false); val add_term_check = Syntax.add_term_check ~100 "coercions" - (fn xs => fn ctxt => - if Config.get ctxt coercion_enabled then - let val xs' = coercion_infer_types ctxt xs - in if eq_list (op aconv) (xs, xs') then NONE else SOME (xs', ctxt) end - else NONE); + (fn ctxt => Config.get ctxt coercion_enabled ? coercion_infer_types ctxt); (* declarations *)