--- 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)
--- 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 (\<tau>, s)"} tests whether type
@{text "\<tau>"} is of sort @{text "s"}.
- \item @{ML Sign.add_types}~@{text "[(\<kappa>, k, mx), \<dots>]"} declares a new
- type constructors @{text "\<kappa>"} with @{text "k"} arguments and
+ \item @{ML Sign.add_types}~@{text "ctxt [(\<kappa>, k, mx), \<dots>]"} declares a
+ new type constructors @{text "\<kappa>"} with @{text "k"} arguments and
optional mixfix syntax.
- \item @{ML Sign.add_type_abbrev}~@{text "(\<kappa>, \<^vec>\<alpha>,
- \<tau>)"} defines a new type abbreviation @{text
- "(\<^vec>\<alpha>)\<kappa> = \<tau>"}.
+ \item @{ML Sign.add_type_abbrev}~@{text "ctxt (\<kappa>, \<^vec>\<alpha>, \<tau>)"}
+ defines a new type abbreviation @{text "(\<^vec>\<alpha>)\<kappa> = \<tau>"}.
\item @{ML Sign.primitive_class}~@{text "(c, [c\<^isub>1, \<dots>,
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 "\<beta>"}-conversion if @{text "t"} is an
abstraction.
- \item @{ML Sign.declare_const}~@{text "((c, \<sigma>), mx)"}
- declares a new constant @{text "c :: \<sigma>"} with optional mixfix
- syntax.
+ \item @{ML Sign.declare_const}~@{text "ctxt ((c, \<sigma>), mx)"} declares
+ a new constant @{text "c :: \<sigma>"} with optional mixfix syntax.
\item @{ML Sign.add_abbrev}~@{text "print_mode (c, t)"}
introduces a new term abbreviation @{text "c \<equiv> 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>\<tau>"}
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 \<equiv> 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>\<tau>
- \<^vec>d\<^isub>\<sigma>"} declares dependencies of a named specification
- for constant @{text "c\<^isub>\<tau>"}, relative to existing
- specifications for constants @{text "\<^vec>d\<^isub>\<sigma>"}.
+ \item @{ML Theory.add_deps}~@{text "ctxt name c\<^isub>\<tau> \<^vec>d\<^isub>\<sigma>"}
+ declares dependencies of a named specification for constant @{text
+ "c\<^isub>\<tau>"}, relative to existing specifications for constants @{text
+ "\<^vec>d\<^isub>\<sigma>"}.
\end{description}
*}
--- 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.
--- 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}%
--- 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.
--- 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
--- 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
--- 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"]
--- 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 " =>",
--- 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;
--- 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 **)
--- 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 **)
--- 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
--- 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''')
--- 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
--- 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
--- 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"
--- 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 =
--- 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;
--- 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;
--- 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) =
--- 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
--- 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";
--- 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",
--- 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))
--- 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 ();
--- 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 "<Top>" module false t gr))
+ (invoke_codegen thy mode defs "<Top>" 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) ["<Top>"]))
+ (output_code (fst gr') (if_library mode "" module) ["<Top>"]))
in
(code'', del_nodes ["<Top>"] 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))
--- 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;
--- 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 ("\\<struct>_", [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 _"),
--- 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;
--- /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;
--- 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
--- 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);
--- 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 *)