1.1 --- a/NEWS Wed Apr 20 10:14:24 2011 +0200
1.2 +++ b/NEWS Wed Apr 20 11:21:12 2011 +0200
1.3 @@ -115,6 +115,9 @@
1.4 * Refined PARALLEL_GOALS tactical: degrades gracefully for schematic
1.5 goal states; body tactic needs to address all subgoals uniformly.
1.6
1.7 +* Slightly more special eq_list/eq_set, with shortcut involving
1.8 +pointer equality (assumes that eq relation is reflexive).
1.9 +
1.10
1.11
1.12 New in Isabelle2011 (January 2011)
2.1 --- a/doc-src/IsarImplementation/Thy/Logic.thy Wed Apr 20 10:14:24 2011 +0200
2.2 +++ b/doc-src/IsarImplementation/Thy/Logic.thy Wed Apr 20 11:21:12 2011 +0200
2.3 @@ -127,8 +127,10 @@
2.4 \begin{mldecls}
2.5 @{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\
2.6 @{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\
2.7 - @{index_ML Sign.add_types: "(binding * int * mixfix) list -> theory -> theory"} \\
2.8 - @{index_ML Sign.add_type_abbrev: "binding * string list * typ -> theory -> theory"} \\
2.9 + @{index_ML Sign.add_types: "Proof.context ->
2.10 + (binding * int * mixfix) list -> theory -> theory"} \\
2.11 + @{index_ML Sign.add_type_abbrev: "Proof.context ->
2.12 + binding * string list * typ -> theory -> theory"} \\
2.13 @{index_ML Sign.primitive_class: "binding * class list -> theory -> theory"} \\
2.14 @{index_ML Sign.primitive_classrel: "class * class -> theory -> theory"} \\
2.15 @{index_ML Sign.primitive_arity: "arity -> theory -> theory"} \\
2.16 @@ -164,13 +166,12 @@
2.17 \item @{ML Sign.of_sort}~@{text "thy (\<tau>, s)"} tests whether type
2.18 @{text "\<tau>"} is of sort @{text "s"}.
2.19
2.20 - \item @{ML Sign.add_types}~@{text "[(\<kappa>, k, mx), \<dots>]"} declares a new
2.21 - type constructors @{text "\<kappa>"} with @{text "k"} arguments and
2.22 + \item @{ML Sign.add_types}~@{text "ctxt [(\<kappa>, k, mx), \<dots>]"} declares a
2.23 + new type constructors @{text "\<kappa>"} with @{text "k"} arguments and
2.24 optional mixfix syntax.
2.25
2.26 - \item @{ML Sign.add_type_abbrev}~@{text "(\<kappa>, \<^vec>\<alpha>,
2.27 - \<tau>)"} defines a new type abbreviation @{text
2.28 - "(\<^vec>\<alpha>)\<kappa> = \<tau>"}.
2.29 + \item @{ML Sign.add_type_abbrev}~@{text "ctxt (\<kappa>, \<^vec>\<alpha>, \<tau>)"}
2.30 + defines a new type abbreviation @{text "(\<^vec>\<alpha>)\<kappa> = \<tau>"}.
2.31
2.32 \item @{ML Sign.primitive_class}~@{text "(c, [c\<^isub>1, \<dots>,
2.33 c\<^isub>n])"} declares a new class @{text "c"}, together with class
2.34 @@ -364,8 +365,8 @@
2.35 @{index_ML fastype_of: "term -> typ"} \\
2.36 @{index_ML lambda: "term -> term -> term"} \\
2.37 @{index_ML betapply: "term * term -> term"} \\
2.38 - @{index_ML Sign.declare_const: "(binding * typ) * mixfix ->
2.39 - theory -> term * theory"} \\
2.40 + @{index_ML Sign.declare_const: "Proof.context ->
2.41 + (binding * typ) * mixfix -> theory -> term * theory"} \\
2.42 @{index_ML Sign.add_abbrev: "string -> binding * term ->
2.43 theory -> (term * term) * theory"} \\
2.44 @{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\
2.45 @@ -412,9 +413,8 @@
2.46 "t u"}, with topmost @{text "\<beta>"}-conversion if @{text "t"} is an
2.47 abstraction.
2.48
2.49 - \item @{ML Sign.declare_const}~@{text "((c, \<sigma>), mx)"}
2.50 - declares a new constant @{text "c :: \<sigma>"} with optional mixfix
2.51 - syntax.
2.52 + \item @{ML Sign.declare_const}~@{text "ctxt ((c, \<sigma>), mx)"} declares
2.53 + a new constant @{text "c :: \<sigma>"} with optional mixfix syntax.
2.54
2.55 \item @{ML Sign.add_abbrev}~@{text "print_mode (c, t)"}
2.56 introduces a new term abbreviation @{text "c \<equiv> t"}.
2.57 @@ -640,15 +640,16 @@
2.58 @{index_ML Thm.implies_elim: "thm -> thm -> thm"} \\
2.59 @{index_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\
2.60 @{index_ML Thm.instantiate: "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"} \\
2.61 - @{index_ML Thm.add_axiom: "binding * term -> theory -> (string * thm) * theory"} \\
2.62 + @{index_ML Thm.add_axiom: "Proof.context ->
2.63 + binding * term -> theory -> (string * thm) * theory"} \\
2.64 @{index_ML Thm.add_oracle: "binding * ('a -> cterm) -> theory ->
2.65 (string * ('a -> thm)) * theory"} \\
2.66 - @{index_ML Thm.add_def: "bool -> bool -> binding * term -> theory ->
2.67 - (string * thm) * theory"} \\
2.68 + @{index_ML Thm.add_def: "Proof.context -> bool -> bool ->
2.69 + binding * term -> theory -> (string * thm) * theory"} \\
2.70 \end{mldecls}
2.71 \begin{mldecls}
2.72 - @{index_ML Theory.add_deps: "string -> string * typ -> (string * typ) list ->
2.73 - theory -> theory"} \\
2.74 + @{index_ML Theory.add_deps: "Proof.context -> string ->
2.75 + string * typ -> (string * typ) list -> theory -> theory"} \\
2.76 \end{mldecls}
2.77
2.78 \begin{description}
2.79 @@ -696,7 +697,7 @@
2.80 term variables. Note that the types in @{text "\<^vec>x\<^isub>\<tau>"}
2.81 refer to the instantiated versions.
2.82
2.83 - \item @{ML Thm.add_axiom}~@{text "(name, A) thy"} declares an
2.84 + \item @{ML Thm.add_axiom}~@{text "ctxt (name, A)"} declares an
2.85 arbitrary proposition as axiom, and retrieves it as a theorem from
2.86 the resulting theory, cf.\ @{text "axiom"} in
2.87 \figref{fig:prim-rules}. Note that the low-level representation in
2.88 @@ -706,17 +707,17 @@
2.89 oracle rule, essentially generating arbitrary axioms on the fly,
2.90 cf.\ @{text "axiom"} in \figref{fig:prim-rules}.
2.91
2.92 - \item @{ML Thm.add_def}~@{text "unchecked overloaded (name, c
2.93 + \item @{ML Thm.add_def}~@{text "ctxt unchecked overloaded (name, c
2.94 \<^vec>x \<equiv> t)"} states a definitional axiom for an existing constant
2.95 @{text "c"}. Dependencies are recorded via @{ML Theory.add_deps},
2.96 unless the @{text "unchecked"} option is set. Note that the
2.97 low-level representation in the axiom table may differ slightly from
2.98 the returned theorem.
2.99
2.100 - \item @{ML Theory.add_deps}~@{text "name c\<^isub>\<tau>
2.101 - \<^vec>d\<^isub>\<sigma>"} declares dependencies of a named specification
2.102 - for constant @{text "c\<^isub>\<tau>"}, relative to existing
2.103 - specifications for constants @{text "\<^vec>d\<^isub>\<sigma>"}.
2.104 + \item @{ML Theory.add_deps}~@{text "ctxt name c\<^isub>\<tau> \<^vec>d\<^isub>\<sigma>"}
2.105 + declares dependencies of a named specification for constant @{text
2.106 + "c\<^isub>\<tau>"}, relative to existing specifications for constants @{text
2.107 + "\<^vec>d\<^isub>\<sigma>"}.
2.108
2.109 \end{description}
2.110 *}
3.1 --- a/doc-src/IsarImplementation/Thy/Prelim.thy Wed Apr 20 10:14:24 2011 +0200
3.2 +++ b/doc-src/IsarImplementation/Thy/Prelim.thy Wed Apr 20 11:21:12 2011 +0200
3.3 @@ -1109,8 +1109,8 @@
3.4 @{index_ML_type Name_Space.T} \\
3.5 @{index_ML Name_Space.empty: "string -> Name_Space.T"} \\
3.6 @{index_ML Name_Space.merge: "Name_Space.T * Name_Space.T -> Name_Space.T"} \\
3.7 - @{index_ML Name_Space.declare: "bool -> Name_Space.naming -> binding -> Name_Space.T ->
3.8 - string * Name_Space.T"} \\
3.9 + @{index_ML Name_Space.declare: "Proof.context -> bool ->
3.10 + Name_Space.naming -> binding -> Name_Space.T -> string * Name_Space.T"} \\
3.11 @{index_ML Name_Space.intern: "Name_Space.T -> string -> string"} \\
3.12 @{index_ML Name_Space.extern: "Proof.context -> Name_Space.T -> string -> string"} \\
3.13 @{index_ML Name_Space.is_concealed: "Name_Space.T -> string -> bool"}
3.14 @@ -1173,7 +1173,7 @@
3.15 (\secref{sec:context-data}); @{text "kind"} is a formal comment
3.16 to characterize the purpose of a name space.
3.17
3.18 - \item @{ML Name_Space.declare}~@{text "strict naming bindings
3.19 + \item @{ML Name_Space.declare}~@{text "ctxt strict naming bindings
3.20 space"} enters a name binding as fully qualified internal name into
3.21 the name space, with external accesses determined by the naming
3.22 policy.
4.1 --- a/doc-src/IsarImplementation/Thy/document/Logic.tex Wed Apr 20 10:14:24 2011 +0200
4.2 +++ b/doc-src/IsarImplementation/Thy/document/Logic.tex Wed Apr 20 11:21:12 2011 +0200
4.3 @@ -138,8 +138,10 @@
4.4 \begin{mldecls}
4.5 \indexdef{}{ML}{Sign.subsort}\verb|Sign.subsort: theory -> sort * sort -> bool| \\
4.6 \indexdef{}{ML}{Sign.of\_sort}\verb|Sign.of_sort: theory -> typ * sort -> bool| \\
4.7 - \indexdef{}{ML}{Sign.add\_types}\verb|Sign.add_types: (binding * int * mixfix) list -> theory -> theory| \\
4.8 - \indexdef{}{ML}{Sign.add\_type\_abbrev}\verb|Sign.add_type_abbrev: binding * string list * typ -> theory -> theory| \\
4.9 + \indexdef{}{ML}{Sign.add\_types}\verb|Sign.add_types: Proof.context ->|\isasep\isanewline%
4.10 +\verb| (binding * int * mixfix) list -> theory -> theory| \\
4.11 + \indexdef{}{ML}{Sign.add\_type\_abbrev}\verb|Sign.add_type_abbrev: Proof.context ->|\isasep\isanewline%
4.12 +\verb| binding * string list * typ -> theory -> theory| \\
4.13 \indexdef{}{ML}{Sign.primitive\_class}\verb|Sign.primitive_class: binding * class list -> theory -> theory| \\
4.14 \indexdef{}{ML}{Sign.primitive\_classrel}\verb|Sign.primitive_classrel: class * class -> theory -> theory| \\
4.15 \indexdef{}{ML}{Sign.primitive\_arity}\verb|Sign.primitive_arity: arity -> theory -> theory| \\
4.16 @@ -172,11 +174,12 @@
4.17 \item \verb|Sign.of_sort|~\isa{thy\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{2C}{\isacharcomma}}\ s{\isaliteral{29}{\isacharparenright}}} tests whether type
4.18 \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} is of sort \isa{s}.
4.19
4.20 - \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
4.21 - type constructors \isa{{\isaliteral{5C3C6B617070613E}{\isasymkappa}}} with \isa{k} arguments and
4.22 + \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
4.23 + new type constructors \isa{{\isaliteral{5C3C6B617070613E}{\isasymkappa}}} with \isa{k} arguments and
4.24 optional mixfix syntax.
4.25
4.26 - \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}}}.
4.27 + \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}}}
4.28 + 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}}}.
4.29
4.30 \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
4.31 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}.
4.32 @@ -386,8 +389,8 @@
4.33 \indexdef{}{ML}{fastype\_of}\verb|fastype_of: term -> typ| \\
4.34 \indexdef{}{ML}{lambda}\verb|lambda: term -> term -> term| \\
4.35 \indexdef{}{ML}{betapply}\verb|betapply: term * term -> term| \\
4.36 - \indexdef{}{ML}{Sign.declare\_const}\verb|Sign.declare_const: (binding * typ) * mixfix ->|\isasep\isanewline%
4.37 -\verb| theory -> term * theory| \\
4.38 + \indexdef{}{ML}{Sign.declare\_const}\verb|Sign.declare_const: Proof.context ->|\isasep\isanewline%
4.39 +\verb| (binding * typ) * mixfix -> theory -> term * theory| \\
4.40 \indexdef{}{ML}{Sign.add\_abbrev}\verb|Sign.add_abbrev: string -> binding * term ->|\isasep\isanewline%
4.41 \verb| theory -> (term * term) * theory| \\
4.42 \indexdef{}{ML}{Sign.const\_typargs}\verb|Sign.const_typargs: theory -> string * typ -> typ list| \\
4.43 @@ -426,9 +429,8 @@
4.44 \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
4.45 abstraction.
4.46
4.47 - \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}}}
4.48 - declares a new constant \isa{c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}} with optional mixfix
4.49 - syntax.
4.50 + \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
4.51 + a new constant \isa{c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}} with optional mixfix syntax.
4.52
4.53 \item \verb|Sign.add_abbrev|~\isa{print{\isaliteral{5F}{\isacharunderscore}}mode\ {\isaliteral{28}{\isacharparenleft}}c{\isaliteral{2C}{\isacharcomma}}\ t{\isaliteral{29}{\isacharparenright}}}
4.54 introduces a new term abbreviation \isa{c\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t}.
4.55 @@ -673,15 +675,16 @@
4.56 \indexdef{}{ML}{Thm.implies\_elim}\verb|Thm.implies_elim: thm -> thm -> thm| \\
4.57 \indexdef{}{ML}{Thm.generalize}\verb|Thm.generalize: string list * string list -> int -> thm -> thm| \\
4.58 \indexdef{}{ML}{Thm.instantiate}\verb|Thm.instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm| \\
4.59 - \indexdef{}{ML}{Thm.add\_axiom}\verb|Thm.add_axiom: binding * term -> theory -> (string * thm) * theory| \\
4.60 + \indexdef{}{ML}{Thm.add\_axiom}\verb|Thm.add_axiom: Proof.context ->|\isasep\isanewline%
4.61 +\verb| binding * term -> theory -> (string * thm) * theory| \\
4.62 \indexdef{}{ML}{Thm.add\_oracle}\verb|Thm.add_oracle: binding * ('a -> cterm) -> theory ->|\isasep\isanewline%
4.63 \verb| (string * ('a -> thm)) * theory| \\
4.64 - \indexdef{}{ML}{Thm.add\_def}\verb|Thm.add_def: bool -> bool -> binding * term -> theory ->|\isasep\isanewline%
4.65 -\verb| (string * thm) * theory| \\
4.66 + \indexdef{}{ML}{Thm.add\_def}\verb|Thm.add_def: Proof.context -> bool -> bool ->|\isasep\isanewline%
4.67 +\verb| binding * term -> theory -> (string * thm) * theory| \\
4.68 \end{mldecls}
4.69 \begin{mldecls}
4.70 - \indexdef{}{ML}{Theory.add\_deps}\verb|Theory.add_deps: string -> string * typ -> (string * typ) list ->|\isasep\isanewline%
4.71 -\verb| theory -> theory| \\
4.72 + \indexdef{}{ML}{Theory.add\_deps}\verb|Theory.add_deps: Proof.context -> string ->|\isasep\isanewline%
4.73 +\verb| string * typ -> (string * typ) list -> theory -> theory| \\
4.74 \end{mldecls}
4.75
4.76 \begin{description}
4.77 @@ -726,7 +729,7 @@
4.78 term variables. Note that the types in \isa{\isaliteral{5C3C5E7665633E}{}\isactrlvec x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}}
4.79 refer to the instantiated versions.
4.80
4.81 - \item \verb|Thm.add_axiom|~\isa{{\isaliteral{28}{\isacharparenleft}}name{\isaliteral{2C}{\isacharcomma}}\ A{\isaliteral{29}{\isacharparenright}}\ thy} declares an
4.82 + \item \verb|Thm.add_axiom|~\isa{ctxt\ {\isaliteral{28}{\isacharparenleft}}name{\isaliteral{2C}{\isacharcomma}}\ A{\isaliteral{29}{\isacharparenright}}} declares an
4.83 arbitrary proposition as axiom, and retrieves it as a theorem from
4.84 the resulting theory, cf.\ \isa{axiom} in
4.85 \figref{fig:prim-rules}. Note that the low-level representation in
4.86 @@ -736,15 +739,14 @@
4.87 oracle rule, essentially generating arbitrary axioms on the fly,
4.88 cf.\ \isa{axiom} in \figref{fig:prim-rules}.
4.89
4.90 - \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
4.91 + \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
4.92 \isa{c}. Dependencies are recorded via \verb|Theory.add_deps|,
4.93 unless the \isa{unchecked} option is set. Note that the
4.94 low-level representation in the axiom table may differ slightly from
4.95 the returned theorem.
4.96
4.97 - \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
4.98 - for constant \isa{c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}}, relative to existing
4.99 - specifications for constants \isa{\isaliteral{5C3C5E7665633E}{}\isactrlvec d\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7369676D613E}{\isasymsigma}}}.
4.100 + \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}}}
4.101 + 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}}}.
4.102
4.103 \end{description}%
4.104 \end{isamarkuptext}%
5.1 --- a/doc-src/IsarImplementation/Thy/document/Prelim.tex Wed Apr 20 10:14:24 2011 +0200
5.2 +++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex Wed Apr 20 11:21:12 2011 +0200
5.3 @@ -1607,8 +1607,8 @@
5.4 \indexdef{}{ML type}{Name\_Space.T}\verb|type Name_Space.T| \\
5.5 \indexdef{}{ML}{Name\_Space.empty}\verb|Name_Space.empty: string -> Name_Space.T| \\
5.6 \indexdef{}{ML}{Name\_Space.merge}\verb|Name_Space.merge: Name_Space.T * Name_Space.T -> Name_Space.T| \\
5.7 - \indexdef{}{ML}{Name\_Space.declare}\verb|Name_Space.declare: bool -> Name_Space.naming -> binding -> Name_Space.T ->|\isasep\isanewline%
5.8 -\verb| string * Name_Space.T| \\
5.9 + \indexdef{}{ML}{Name\_Space.declare}\verb|Name_Space.declare: Proof.context -> bool ->|\isasep\isanewline%
5.10 +\verb| Name_Space.naming -> binding -> Name_Space.T -> string * Name_Space.T| \\
5.11 \indexdef{}{ML}{Name\_Space.intern}\verb|Name_Space.intern: Name_Space.T -> string -> string| \\
5.12 \indexdef{}{ML}{Name\_Space.extern}\verb|Name_Space.extern: Proof.context -> Name_Space.T -> string -> string| \\
5.13 \indexdef{}{ML}{Name\_Space.is\_concealed}\verb|Name_Space.is_concealed: Name_Space.T -> string -> bool|
5.14 @@ -1667,7 +1667,7 @@
5.15 (\secref{sec:context-data}); \isa{kind} is a formal comment
5.16 to characterize the purpose of a name space.
5.17
5.18 - \item \verb|Name_Space.declare|~\isa{strict\ naming\ bindings\ space} enters a name binding as fully qualified internal name into
5.19 + \item \verb|Name_Space.declare|~\isa{ctxt\ strict\ naming\ bindings\ space} enters a name binding as fully qualified internal name into
5.20 the name space, with external accesses determined by the naming
5.21 policy.
5.22
6.1 --- a/src/HOL/HOL.thy Wed Apr 20 10:14:24 2011 +0200
6.2 +++ b/src/HOL/HOL.thy Wed Apr 20 11:21:12 2011 +0200
6.3 @@ -1746,20 +1746,21 @@
6.4 setup {*
6.5 let
6.6
6.7 -fun eq_codegen thy defs dep thyname b t gr =
6.8 +fun eq_codegen thy mode defs dep thyname b t gr =
6.9 (case strip_comb t of
6.10 (Const (@{const_name HOL.eq}, Type (_, [Type ("fun", _), _])), _) => NONE
6.11 | (Const (@{const_name HOL.eq}, _), [t, u]) =>
6.12 let
6.13 - val (pt, gr') = Codegen.invoke_codegen thy defs dep thyname false t gr;
6.14 - val (pu, gr'') = Codegen.invoke_codegen thy defs dep thyname false u gr';
6.15 - val (_, gr''') = Codegen.invoke_tycodegen thy defs dep thyname false HOLogic.boolT gr'';
6.16 + val (pt, gr') = Codegen.invoke_codegen thy mode defs dep thyname false t gr;
6.17 + val (pu, gr'') = Codegen.invoke_codegen thy mode defs dep thyname false u gr';
6.18 + val (_, gr''') =
6.19 + Codegen.invoke_tycodegen thy mode defs dep thyname false HOLogic.boolT gr'';
6.20 in
6.21 SOME (Codegen.parens
6.22 (Pretty.block [pt, Codegen.str " =", Pretty.brk 1, pu]), gr''')
6.23 end
6.24 | (t as Const (@{const_name HOL.eq}, _), ts) => SOME (Codegen.invoke_codegen
6.25 - thy defs dep thyname b (Codegen.eta_expand t ts 2) gr)
6.26 + thy mode defs dep thyname b (Codegen.eta_expand t ts 2) gr)
6.27 | _ => NONE);
6.28
6.29 in
7.1 --- a/src/HOL/Int.thy Wed Apr 20 10:14:24 2011 +0200
7.2 +++ b/src/HOL/Int.thy Wed Apr 20 11:21:12 2011 +0200
7.3 @@ -2351,11 +2351,11 @@
7.4 fun strip_number_of (@{term "Int.number_of :: int => int"} $ t) = t
7.5 | strip_number_of t = t;
7.6
7.7 -fun numeral_codegen thy defs dep module b t gr =
7.8 +fun numeral_codegen thy mode defs dep module b t gr =
7.9 let val i = HOLogic.dest_numeral (strip_number_of t)
7.10 in
7.11 SOME (Codegen.str (string_of_int i),
7.12 - snd (Codegen.invoke_tycodegen thy defs dep module false HOLogic.intT gr))
7.13 + snd (Codegen.invoke_tycodegen thy mode defs dep module false HOLogic.intT gr))
7.14 end handle TERM _ => NONE;
7.15
7.16 in
8.1 --- a/src/HOL/List.thy Wed Apr 20 10:14:24 2011 +0200
8.2 +++ b/src/HOL/List.thy Wed Apr 20 11:21:12 2011 +0200
8.3 @@ -5207,13 +5207,13 @@
8.4
8.5 setup {*
8.6 let
8.7 - fun list_codegen thy defs dep thyname b t gr =
8.8 + fun list_codegen thy mode defs dep thyname b t gr =
8.9 let
8.10 val ts = HOLogic.dest_list t;
8.11 - val (_, gr') = Codegen.invoke_tycodegen thy defs dep thyname false
8.12 + val (_, gr') = Codegen.invoke_tycodegen thy mode defs dep thyname false
8.13 (fastype_of t) gr;
8.14 val (ps, gr'') = fold_map
8.15 - (Codegen.invoke_codegen thy defs dep thyname false) ts gr'
8.16 + (Codegen.invoke_codegen thy mode defs dep thyname false) ts gr'
8.17 in SOME (Pretty.list "[" "]" ps, gr'') end handle TERM _ => NONE;
8.18 in
8.19 fold (List_Code.add_literal_list) ["SML", "OCaml", "Haskell", "Scala"]
9.1 --- a/src/HOL/Product_Type.thy Wed Apr 20 10:14:24 2011 +0200
9.2 +++ b/src/HOL/Product_Type.thy Wed Apr 20 11:21:12 2011 +0200
9.3 @@ -336,7 +336,7 @@
9.4 | strip_abs_split i t =
9.5 strip_abs_split i (Abs ("x", hd (binder_types (fastype_of t)), t $ Bound 0));
9.6
9.7 -fun let_codegen thy defs dep thyname brack t gr =
9.8 +fun let_codegen thy mode defs dep thyname brack t gr =
9.9 (case strip_comb t of
9.10 (t1 as Const (@{const_name Let}, _), t2 :: t3 :: ts) =>
9.11 let
9.12 @@ -347,17 +347,17 @@
9.13 | dest_let t = ([], t);
9.14 fun mk_code (l, r) gr =
9.15 let
9.16 - val (pl, gr1) = Codegen.invoke_codegen thy defs dep thyname false l gr;
9.17 - val (pr, gr2) = Codegen.invoke_codegen thy defs dep thyname false r gr1;
9.18 + val (pl, gr1) = Codegen.invoke_codegen thy mode defs dep thyname false l gr;
9.19 + val (pr, gr2) = Codegen.invoke_codegen thy mode defs dep thyname false r gr1;
9.20 in ((pl, pr), gr2) end
9.21 in case dest_let (t1 $ t2 $ t3) of
9.22 ([], _) => NONE
9.23 | (ps, u) =>
9.24 let
9.25 val (qs, gr1) = fold_map mk_code ps gr;
9.26 - val (pu, gr2) = Codegen.invoke_codegen thy defs dep thyname false u gr1;
9.27 + val (pu, gr2) = Codegen.invoke_codegen thy mode defs dep thyname false u gr1;
9.28 val (pargs, gr3) = fold_map
9.29 - (Codegen.invoke_codegen thy defs dep thyname true) ts gr2
9.30 + (Codegen.invoke_codegen thy mode defs dep thyname true) ts gr2
9.31 in
9.32 SOME (Codegen.mk_app brack
9.33 (Pretty.blk (0, [Codegen.str "let ", Pretty.blk (0, flat
9.34 @@ -370,14 +370,14 @@
9.35 end
9.36 | _ => NONE);
9.37
9.38 -fun split_codegen thy defs dep thyname brack t gr = (case strip_comb t of
9.39 +fun split_codegen thy mode defs dep thyname brack t gr = (case strip_comb t of
9.40 (t1 as Const (@{const_name prod_case}, _), t2 :: ts) =>
9.41 let
9.42 val ([p], u) = strip_abs_split 1 (t1 $ t2);
9.43 - val (q, gr1) = Codegen.invoke_codegen thy defs dep thyname false p gr;
9.44 - val (pu, gr2) = Codegen.invoke_codegen thy defs dep thyname false u gr1;
9.45 + val (q, gr1) = Codegen.invoke_codegen thy mode defs dep thyname false p gr;
9.46 + val (pu, gr2) = Codegen.invoke_codegen thy mode defs dep thyname false u gr1;
9.47 val (pargs, gr3) = fold_map
9.48 - (Codegen.invoke_codegen thy defs dep thyname true) ts gr2
9.49 + (Codegen.invoke_codegen thy mode defs dep thyname true) ts gr2
9.50 in
9.51 SOME (Codegen.mk_app brack
9.52 (Pretty.block [Codegen.str "(fn ", q, Codegen.str " =>",
10.1 --- a/src/HOL/String.thy Wed Apr 20 10:14:24 2011 +0200
10.2 +++ b/src/HOL/String.thy Wed Apr 20 11:21:12 2011 +0200
10.3 @@ -227,10 +227,10 @@
10.4 setup {*
10.5 let
10.6
10.7 -fun char_codegen thy defs dep thyname b t gr =
10.8 +fun char_codegen thy mode defs dep thyname b t gr =
10.9 let
10.10 val i = HOLogic.dest_char t;
10.11 - val (_, gr') = Codegen.invoke_tycodegen thy defs dep thyname false
10.12 + val (_, gr') = Codegen.invoke_tycodegen thy mode defs dep thyname false
10.13 (fastype_of t) gr;
10.14 in SOME (Codegen.str (ML_Syntax.print_string (chr i)), gr')
10.15 end handle TERM _ => NONE;
11.1 --- a/src/HOL/Tools/Datatype/datatype_codegen.ML Wed Apr 20 10:14:24 2011 +0200
11.2 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Wed Apr 20 11:21:12 2011 +0200
11.3 @@ -151,7 +151,7 @@
11.4
11.5 (* datatype definition *)
11.6
11.7 -fun add_dt_defs thy defs dep module descr sorts gr =
11.8 +fun add_dt_defs thy mode defs dep module descr sorts gr =
11.9 let
11.10 val descr' = filter (can (map Datatype_Aux.dest_DtTFree o #2 o snd)) descr;
11.11 val rtnames = map (#1 o snd) (filter (fn (_, (_, _, cs)) =>
11.12 @@ -159,7 +159,7 @@
11.13
11.14 val (_, (tname, _, _)) :: _ = descr';
11.15 val node_id = tname ^ " (type)";
11.16 - val module' = Codegen.if_library (Codegen.thyname_of_type thy tname) module;
11.17 + val module' = Codegen.if_library mode (Codegen.thyname_of_type thy tname) module;
11.18
11.19 fun mk_dtdef prfx [] gr = ([], gr)
11.20 | mk_dtdef prfx ((_, (tname, dts, cs))::xs) gr =
11.21 @@ -169,7 +169,7 @@
11.22 val ((_, type_id), gr') = Codegen.mk_type_id module' tname gr;
11.23 val (ps, gr'') = gr' |>
11.24 fold_map (fn (cname, cargs) =>
11.25 - fold_map (Codegen.invoke_tycodegen thy defs node_id module' false)
11.26 + fold_map (Codegen.invoke_tycodegen thy mode defs node_id module' false)
11.27 cargs ##>>
11.28 Codegen.mk_const_id module' cname) cs';
11.29 val (rest, gr''') = mk_dtdef "and " xs gr''
11.30 @@ -309,11 +309,11 @@
11.31 Codegen.map_node node_id (K (NONE, module',
11.32 Codegen.string_of (Pretty.blk (0, separate Pretty.fbrk dtdef @
11.33 [Codegen.str ";"])) ^ "\n\n" ^
11.34 - (if member (op =) (! Codegen.mode) "term_of" then
11.35 + (if member (op =) mode "term_of" then
11.36 Codegen.string_of (Pretty.blk (0, separate Pretty.fbrk
11.37 (mk_term_of_def gr2 "fun " descr') @ [Codegen.str ";"])) ^ "\n\n"
11.38 else "") ^
11.39 - (if member (op =) (! Codegen.mode) "test" then
11.40 + (if member (op =) mode "test" then
11.41 Codegen.string_of (Pretty.blk (0, separate Pretty.fbrk
11.42 (mk_gen_of_def gr2 "fun " descr') @ [Codegen.str ";"])) ^ "\n\n"
11.43 else ""))) gr2
11.44 @@ -323,10 +323,10 @@
11.45
11.46 (* case expressions *)
11.47
11.48 -fun pretty_case thy defs dep module brack constrs (c as Const (_, T)) ts gr =
11.49 +fun pretty_case thy mode defs dep module brack constrs (c as Const (_, T)) ts gr =
11.50 let val i = length constrs
11.51 in if length ts <= i then
11.52 - Codegen.invoke_codegen thy defs dep module brack (Codegen.eta_expand c ts (i+1)) gr
11.53 + Codegen.invoke_codegen thy mode defs dep module brack (Codegen.eta_expand c ts (i+1)) gr
11.54 else
11.55 let
11.56 val ts1 = take i ts;
11.57 @@ -342,10 +342,10 @@
11.58 val xs = Name.variant_list names (replicate j "x");
11.59 val Us' = take j (binder_types U);
11.60 val frees = map2 (curry Free) xs Us';
11.61 - val (cp, gr0) = Codegen.invoke_codegen thy defs dep module false
11.62 + val (cp, gr0) = Codegen.invoke_codegen thy mode defs dep module false
11.63 (list_comb (Const (cname, Us' ---> dT), frees)) gr;
11.64 val t' = Envir.beta_norm (list_comb (t, frees));
11.65 - val (p, gr1) = Codegen.invoke_codegen thy defs dep module false t' gr0;
11.66 + val (p, gr1) = Codegen.invoke_codegen thy mode defs dep module false t' gr0;
11.67 val (ps, gr2) = pcase cs ts Us gr1;
11.68 in
11.69 ([Pretty.block [cp, Codegen.str " =>", Pretty.brk 1, p]] :: ps, gr2)
11.70 @@ -353,8 +353,8 @@
11.71
11.72 val (ps1, gr1) = pcase constrs ts1 Ts gr ;
11.73 val ps = flat (separate [Pretty.brk 1, Codegen.str "| "] ps1);
11.74 - val (p, gr2) = Codegen.invoke_codegen thy defs dep module false t gr1;
11.75 - val (ps2, gr3) = fold_map (Codegen.invoke_codegen thy defs dep module true) ts2 gr2;
11.76 + val (p, gr2) = Codegen.invoke_codegen thy mode defs dep module false t gr1;
11.77 + val (ps2, gr3) = fold_map (Codegen.invoke_codegen thy mode defs dep module true) ts2 gr2;
11.78 in ((if not (null ts2) andalso brack then Codegen.parens else I)
11.79 (Pretty.block (separate (Pretty.brk 1)
11.80 (Pretty.block ([Codegen.str "(case ", p, Codegen.str " of",
11.81 @@ -365,15 +365,15 @@
11.82
11.83 (* constructors *)
11.84
11.85 -fun pretty_constr thy defs dep module brack args (c as Const (s, T)) ts gr =
11.86 +fun pretty_constr thy mode defs dep module brack args (c as Const (s, T)) ts gr =
11.87 let val i = length args
11.88 in if i > 1 andalso length ts < i then
11.89 - Codegen.invoke_codegen thy defs dep module brack (Codegen.eta_expand c ts i) gr
11.90 + Codegen.invoke_codegen thy mode defs dep module brack (Codegen.eta_expand c ts i) gr
11.91 else
11.92 let
11.93 val id = Codegen.mk_qual_id module (Codegen.get_const_id gr s);
11.94 val (ps, gr') = fold_map
11.95 - (Codegen.invoke_codegen thy defs dep module (i = 1)) ts gr;
11.96 + (Codegen.invoke_codegen thy mode defs dep module (i = 1)) ts gr;
11.97 in
11.98 (case args of
11.99 _ :: _ :: _ => (if brack then Codegen.parens else I)
11.100 @@ -385,14 +385,14 @@
11.101
11.102 (* code generators for terms and types *)
11.103
11.104 -fun datatype_codegen thy defs dep module brack t gr =
11.105 +fun datatype_codegen thy mode defs dep module brack t gr =
11.106 (case strip_comb t of
11.107 (c as Const (s, T), ts) =>
11.108 (case Datatype_Data.info_of_case thy s of
11.109 SOME {index, descr, ...} =>
11.110 if is_some (Codegen.get_assoc_code thy (s, T)) then NONE
11.111 else
11.112 - SOME (pretty_case thy defs dep module brack
11.113 + SOME (pretty_case thy mode defs dep module brack
11.114 (#3 (the (AList.lookup op = descr index))) c ts gr)
11.115 | NONE =>
11.116 (case (Datatype_Data.info_of_constr thy (s, T), body_type T) of
11.117 @@ -406,28 +406,28 @@
11.118 if tyname <> tyname' then NONE
11.119 else
11.120 SOME
11.121 - (pretty_constr thy defs
11.122 + (pretty_constr thy mode defs
11.123 dep module brack args c ts
11.124 - (snd (Codegen.invoke_tycodegen thy defs dep module false U gr)))
11.125 + (snd (Codegen.invoke_tycodegen thy mode defs dep module false U gr)))
11.126 end
11.127 | _ => NONE))
11.128 | _ => NONE);
11.129
11.130 -fun datatype_tycodegen thy defs dep module brack (Type (s, Ts)) gr =
11.131 +fun datatype_tycodegen thy mode defs dep module brack (Type (s, Ts)) gr =
11.132 (case Datatype_Data.get_info thy s of
11.133 NONE => NONE
11.134 | SOME {descr, sorts, ...} =>
11.135 if is_some (Codegen.get_assoc_type thy s) then NONE else
11.136 let
11.137 val (ps, gr') = fold_map
11.138 - (Codegen.invoke_tycodegen thy defs dep module false) Ts gr;
11.139 - val (module', gr'') = add_dt_defs thy defs dep module descr sorts gr' ;
11.140 + (Codegen.invoke_tycodegen thy mode defs dep module false) Ts gr;
11.141 + val (module', gr'') = add_dt_defs thy mode defs dep module descr sorts gr' ;
11.142 val (tyid, gr''') = Codegen.mk_type_id module' s gr''
11.143 in SOME (Pretty.block ((if null Ts then [] else
11.144 [Codegen.mk_tuple ps, Codegen.str " "]) @
11.145 [Codegen.str (Codegen.mk_qual_id module tyid)]), gr''')
11.146 end)
11.147 - | datatype_tycodegen _ _ _ _ _ _ _ = NONE;
11.148 + | datatype_tycodegen _ _ _ _ _ _ _ _ = NONE;
11.149
11.150
11.151 (** theory setup **)
12.1 --- a/src/HOL/Tools/code_evaluation.ML Wed Apr 20 10:14:24 2011 +0200
12.2 +++ b/src/HOL/Tools/code_evaluation.ML Wed Apr 20 11:21:12 2011 +0200
12.3 @@ -150,8 +150,8 @@
12.4 | NONE => NONE)
12.5 | subst_termify t = subst_termify_app (strip_comb t)
12.6
12.7 -fun check_termify ts ctxt = map_default subst_termify ts
12.8 - |> Option.map (rpair ctxt)
12.9 +fun check_termify ctxt ts =
12.10 + the_default ts (map_default subst_termify ts);
12.11
12.12
12.13 (** evaluation **)
13.1 --- a/src/HOL/Tools/inductive_codegen.ML Wed Apr 20 10:14:24 2011 +0200
13.2 +++ b/src/HOL/Tools/inductive_codegen.ML Wed Apr 20 11:21:12 2011 +0200
13.3 @@ -239,9 +239,9 @@
13.4 end)
13.5 ps));
13.6
13.7 -fun use_random () = member (op =) (!Codegen.mode) "random_ind";
13.8 +fun use_random codegen_mode = member (op =) codegen_mode "random_ind";
13.9
13.10 -fun check_mode_clause thy arg_vs modes ((iss, is), rnd) (ts, ps) =
13.11 +fun check_mode_clause thy codegen_mode arg_vs modes ((iss, is), rnd) (ts, ps) =
13.12 let
13.13 val modes' = modes @ map_filter
13.14 (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [(([], js), false)]))
13.15 @@ -253,7 +253,7 @@
13.16 (rnd orelse needs_random m)
13.17 (filter_out (equal x) ps)
13.18 | (_, (_, vs') :: _) :: _ =>
13.19 - if use_random () then
13.20 + if use_random codegen_mode then
13.21 check_mode_prems (union (op =) vs (map (fst o fst) vs')) true ps
13.22 else NONE
13.23 | _ => NONE);
13.24 @@ -268,17 +268,17 @@
13.25 let val missing_vs = missing_vars vs ts
13.26 in
13.27 if null missing_vs orelse
13.28 - use_random () andalso monomorphic_vars missing_vs
13.29 + use_random codegen_mode andalso monomorphic_vars missing_vs
13.30 then SOME (rnd' orelse not (null missing_vs))
13.31 else NONE
13.32 end)
13.33 else NONE
13.34 end;
13.35
13.36 -fun check_modes_pred thy arg_vs preds modes (p, ms) =
13.37 +fun check_modes_pred thy codegen_mode arg_vs preds modes (p, ms) =
13.38 let val SOME rs = AList.lookup (op =) preds p
13.39 in (p, List.mapPartial (fn m as (m', _) =>
13.40 - let val xs = map (check_mode_clause thy arg_vs modes m) rs
13.41 + let val xs = map (check_mode_clause thy codegen_mode arg_vs modes m) rs
13.42 in case find_index is_none xs of
13.43 ~1 => SOME (m', exists (fn SOME b => b) xs)
13.44 | i => (Codegen.message ("Clause " ^ string_of_int (i+1) ^ " of " ^
13.45 @@ -290,8 +290,8 @@
13.46 let val y = f x
13.47 in if x = y then x else fixp f y end;
13.48
13.49 -fun infer_modes thy extra_modes arities arg_vs preds = fixp (fn modes =>
13.50 - map (check_modes_pred thy arg_vs preds (modes @ extra_modes)) modes)
13.51 +fun infer_modes thy codegen_mode extra_modes arities arg_vs preds = fixp (fn modes =>
13.52 + map (check_modes_pred thy codegen_mode arg_vs preds (modes @ extra_modes)) modes)
13.53 (map (fn (s, (ks, k)) => (s, map (rpair false) (cprod (cprods (map
13.54 (fn NONE => [NONE]
13.55 | SOME k' => map SOME (subsets 1 k')) ks),
13.56 @@ -358,34 +358,34 @@
13.57 separate (Pretty.brk 1) (Codegen.str s :: replicate k (Codegen.str "|> ???")) @
13.58 (if k = 0 then [] else [Codegen.str ")"])), Pretty.brk 1, p]);
13.59
13.60 -fun compile_expr thy defs dep module brack modes (NONE, t) gr =
13.61 - apfst single (Codegen.invoke_codegen thy defs dep module brack t gr)
13.62 - | compile_expr _ _ _ _ _ _ (SOME _, Var ((name, _), _)) gr =
13.63 +fun compile_expr thy codegen_mode defs dep module brack modes (NONE, t) gr =
13.64 + apfst single (Codegen.invoke_codegen thy codegen_mode defs dep module brack t gr)
13.65 + | compile_expr _ _ _ _ _ _ _ (SOME _, Var ((name, _), _)) gr =
13.66 ([Codegen.str name], gr)
13.67 - | compile_expr thy defs dep module brack modes (SOME (Mode ((mode, _), _, ms)), t) gr =
13.68 + | compile_expr thy codegen_mode defs dep module brack modes (SOME (Mode ((mode, _), _, ms)), t) gr =
13.69 (case strip_comb t of
13.70 (Const (name, _), args) =>
13.71 if name = @{const_name HOL.eq} orelse AList.defined op = modes name then
13.72 let
13.73 val (args1, args2) = chop (length ms) args;
13.74 val ((ps, mode_id), gr') = gr |> fold_map
13.75 - (compile_expr thy defs dep module true modes) (ms ~~ args1)
13.76 + (compile_expr thy codegen_mode defs dep module true modes) (ms ~~ args1)
13.77 ||>> modename module name mode;
13.78 val (ps', gr'') = (case mode of
13.79 ([], []) => ([Codegen.str "()"], gr')
13.80 | _ => fold_map
13.81 - (Codegen.invoke_codegen thy defs dep module true) args2 gr')
13.82 + (Codegen.invoke_codegen thy codegen_mode defs dep module true) args2 gr')
13.83 in ((if brack andalso not (null ps andalso null ps') then
13.84 single o Codegen.parens o Pretty.block else I)
13.85 (flat (separate [Pretty.brk 1]
13.86 ([Codegen.str mode_id] :: ps @ map single ps'))), gr')
13.87 end
13.88 else apfst (single o mk_funcomp brack "??" (length (binder_types (fastype_of t))))
13.89 - (Codegen.invoke_codegen thy defs dep module true t gr)
13.90 + (Codegen.invoke_codegen thy codegen_mode defs dep module true t gr)
13.91 | _ => apfst (single o mk_funcomp brack "??" (length (binder_types (fastype_of t))))
13.92 - (Codegen.invoke_codegen thy defs dep module true t gr));
13.93 + (Codegen.invoke_codegen thy codegen_mode defs dep module true t gr));
13.94
13.95 -fun compile_clause thy defs dep module all_vs arg_vs modes (iss, is) (ts, ps) inp gr =
13.96 +fun compile_clause thy codegen_mode defs dep module all_vs arg_vs modes (iss, is) (ts, ps) inp gr =
13.97 let
13.98 val modes' = modes @ map_filter
13.99 (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [(([], js), false)]))
13.100 @@ -399,7 +399,7 @@
13.101
13.102 fun compile_eq (s, t) gr =
13.103 apfst (Pretty.block o cons (Codegen.str (s ^ " = ")) o single)
13.104 - (Codegen.invoke_codegen thy defs dep module false t gr);
13.105 + (Codegen.invoke_codegen thy codegen_mode defs dep module false t gr);
13.106
13.107 val (in_ts, out_ts) = get_args is 1 ts;
13.108 val (in_ts', (all_vs', eqs)) = fold_map check_constrt in_ts (all_vs, []);
13.109 @@ -407,13 +407,13 @@
13.110 fun compile_prems out_ts' vs names [] gr =
13.111 let
13.112 val (out_ps, gr2) =
13.113 - fold_map (Codegen.invoke_codegen thy defs dep module false) out_ts gr;
13.114 + fold_map (Codegen.invoke_codegen thy codegen_mode defs dep module false) out_ts gr;
13.115 val (eq_ps, gr3) = fold_map compile_eq eqs gr2;
13.116 val (out_ts'', (names', eqs')) = fold_map check_constrt out_ts' (names, []);
13.117 val (out_ts''', nvs) =
13.118 fold_map distinct_v out_ts'' (names', map (fn x => (x, [x])) vs);
13.119 val (out_ps', gr4) =
13.120 - fold_map (Codegen.invoke_codegen thy defs dep module false) out_ts''' gr3;
13.121 + fold_map (Codegen.invoke_codegen thy codegen_mode defs dep module false) out_ts''' gr3;
13.122 val (eq_ps', gr5) = fold_map compile_eq eqs' gr4;
13.123 val vs' = distinct (op =) (flat (vs :: map term_vs out_ts'));
13.124 val missing_vs = missing_vars vs' out_ts;
13.125 @@ -425,7 +425,7 @@
13.126 final_p (exists (not o is_exhaustive) out_ts'''), gr5)
13.127 else
13.128 let
13.129 - val (pat_p, gr6) = Codegen.invoke_codegen thy defs dep module true
13.130 + val (pat_p, gr6) = Codegen.invoke_codegen thy codegen_mode defs dep module true
13.131 (HOLogic.mk_tuple (map Var missing_vs)) gr5;
13.132 val gen_p =
13.133 Codegen.mk_gen gr6 module true [] ""
13.134 @@ -445,7 +445,7 @@
13.135 val (out_ts', (names', eqs)) = fold_map check_constrt out_ts (names, []);
13.136 val (out_ts'', nvs) = fold_map distinct_v out_ts' (names', map (fn x => (x, [x])) vs);
13.137 val (out_ps, gr0) =
13.138 - fold_map (Codegen.invoke_codegen thy defs dep module false) out_ts'' gr;
13.139 + fold_map (Codegen.invoke_codegen thy codegen_mode defs dep module false) out_ts'' gr;
13.140 val (eq_ps, gr1) = fold_map compile_eq eqs gr0;
13.141 in
13.142 (case hd (select_mode_prem thy modes' vs' ps) of
13.143 @@ -454,13 +454,13 @@
13.144 val ps' = filter_out (equal p) ps;
13.145 val (in_ts, out_ts''') = get_args js 1 us;
13.146 val (in_ps, gr2) =
13.147 - fold_map (Codegen.invoke_codegen thy defs dep module true) in_ts gr1;
13.148 + fold_map (Codegen.invoke_codegen thy codegen_mode defs dep module true) in_ts gr1;
13.149 val (ps, gr3) =
13.150 if not is_set then
13.151 apfst (fn ps => ps @
13.152 (if null in_ps then [] else [Pretty.brk 1]) @
13.153 separate (Pretty.brk 1) in_ps)
13.154 - (compile_expr thy defs dep module false modes
13.155 + (compile_expr thy codegen_mode defs dep module false modes
13.156 (SOME mode, t) gr2)
13.157 else
13.158 apfst (fn p =>
13.159 @@ -468,7 +468,7 @@
13.160 Codegen.str "of", Codegen.str "Set", Codegen.str "xs", Codegen.str "=>",
13.161 Codegen.str "xs)"])
13.162 (*this is a very strong assumption about the generated code!*)
13.163 - (Codegen.invoke_codegen thy defs dep module true t gr2);
13.164 + (Codegen.invoke_codegen thy codegen_mode defs dep module true t gr2);
13.165 val (rest, gr4) = compile_prems out_ts''' vs' (fst nvs) ps' gr3;
13.166 in
13.167 (compile_match (snd nvs) eq_ps out_ps
13.168 @@ -479,7 +479,8 @@
13.169 | (p as Sidecond t, [(_, [])]) =>
13.170 let
13.171 val ps' = filter_out (equal p) ps;
13.172 - val (side_p, gr2) = Codegen.invoke_codegen thy defs dep module true t gr1;
13.173 + val (side_p, gr2) =
13.174 + Codegen.invoke_codegen thy codegen_mode defs dep module true t gr1;
13.175 val (rest, gr3) = compile_prems [] vs' (fst nvs) ps' gr2;
13.176 in
13.177 (compile_match (snd nvs) eq_ps out_ps
13.178 @@ -490,7 +491,8 @@
13.179 | (_, (_, missing_vs) :: _) =>
13.180 let
13.181 val T = HOLogic.mk_tupleT (map snd missing_vs);
13.182 - val (_, gr2) = Codegen.invoke_tycodegen thy defs dep module false T gr1;
13.183 + val (_, gr2) =
13.184 + Codegen.invoke_tycodegen thy codegen_mode defs dep module false T gr1;
13.185 val gen_p = Codegen.mk_gen gr2 module true [] "" T;
13.186 val (rest, gr3) = compile_prems
13.187 [HOLogic.mk_tuple (map Var missing_vs)] vs' (fst nvs) ps gr2
13.188 @@ -508,12 +510,12 @@
13.189 Codegen.str " :->", Pretty.brk 1, prem_p], gr')
13.190 end;
13.191
13.192 -fun compile_pred thy defs dep module prfx all_vs arg_vs modes s cls mode gr =
13.193 +fun compile_pred thy codegen_mode defs dep module prfx all_vs arg_vs modes s cls mode gr =
13.194 let
13.195 val xs = map Codegen.str (Name.variant_list arg_vs
13.196 (map (fn i => "x" ^ string_of_int i) (snd mode)));
13.197 val ((cl_ps, mode_id), gr') = gr |>
13.198 - fold_map (fn cl => compile_clause thy defs
13.199 + fold_map (fn cl => compile_clause thy codegen_mode defs
13.200 dep module all_vs arg_vs modes mode cl (mk_tuple xs)) cls ||>>
13.201 modename module s mode
13.202 in
13.203 @@ -527,9 +529,9 @@
13.204 flat (separate [Codegen.str " ++", Pretty.brk 1] (map single cl_ps))), (gr', "and "))
13.205 end;
13.206
13.207 -fun compile_preds thy defs dep module all_vs arg_vs modes preds gr =
13.208 +fun compile_preds thy codegen_mode defs dep module all_vs arg_vs modes preds gr =
13.209 let val (prs, (gr', _)) = fold_map (fn (s, cls) =>
13.210 - fold_map (fn (mode, _) => fn (gr', prfx') => compile_pred thy defs
13.211 + fold_map (fn (mode, _) => fn (gr', prfx') => compile_pred thy codegen_mode defs
13.212 dep module prfx' all_vs arg_vs modes s cls mode gr')
13.213 (((the o AList.lookup (op =) modes) s))) preds (gr, "fun ")
13.214 in
13.215 @@ -562,18 +564,19 @@
13.216 NONE => xs
13.217 | SOME xs' => inter (op = o apfst fst) xs' xs) :: constrain cs ys;
13.218
13.219 -fun mk_extra_defs thy defs gr dep names module ts =
13.220 +fun mk_extra_defs thy codegen_mode defs gr dep names module ts =
13.221 fold (fn name => fn gr =>
13.222 if member (op =) names name then gr
13.223 else
13.224 (case get_clauses thy name of
13.225 NONE => gr
13.226 | SOME (names, thyname, nparms, intrs) =>
13.227 - mk_ind_def thy defs gr dep names (Codegen.if_library thyname module)
13.228 + mk_ind_def thy codegen_mode defs gr dep names
13.229 + (Codegen.if_library codegen_mode thyname module)
13.230 [] (prep_intrs intrs) nparms))
13.231 (fold Term.add_const_names ts []) gr
13.232
13.233 -and mk_ind_def thy defs gr dep names module modecs intrs nparms =
13.234 +and mk_ind_def thy codegen_mode defs gr dep names module modecs intrs nparms =
13.235 Codegen.add_edge_acyclic (hd names, dep) gr handle
13.236 Graph.CYCLES (xs :: _) =>
13.237 error ("Inductive_Codegen: illegal cyclic dependencies:\n" ^ commas xs)
13.238 @@ -617,16 +620,16 @@
13.239 length Us)) arities)
13.240 end;
13.241
13.242 - val gr' = mk_extra_defs thy defs
13.243 + val gr' = mk_extra_defs thy codegen_mode defs
13.244 (Codegen.add_edge (hd names, dep)
13.245 (Codegen.new_node (hd names, (NONE, "", "")) gr)) (hd names) names module intrs;
13.246 val (extra_modes, extra_arities) = lookup_modes gr' (hd names);
13.247 val (clauses, arities) = fold add_clause intrs ([], []);
13.248 val modes = constrain modecs
13.249 - (infer_modes thy extra_modes arities arg_vs clauses);
13.250 + (infer_modes thy codegen_mode extra_modes arities arg_vs clauses);
13.251 val _ = print_arities arities;
13.252 val _ = print_modes modes;
13.253 - val (s, gr'') = compile_preds thy defs (hd names) module (terms_vs intrs)
13.254 + val (s, gr'') = compile_preds thy codegen_mode defs (hd names) module (terms_vs intrs)
13.255 arg_vs (modes @ extra_modes) clauses gr';
13.256 in
13.257 (Codegen.map_node (hd names)
13.258 @@ -639,7 +642,7 @@
13.259 ("No such mode for " ^ s ^ ": " ^ string_of_mode ([], is))
13.260 | mode => mode);
13.261
13.262 -fun mk_ind_call thy defs dep module is_query s T ts names thyname k intrs gr =
13.263 +fun mk_ind_call thy codegen_mode defs dep module is_query s T ts names thyname k intrs gr =
13.264 let
13.265 val (ts1, ts2) = chop k ts;
13.266 val u = list_comb (Const (s, T), ts1);
13.267 @@ -647,9 +650,9 @@
13.268 fun mk_mode (Const (@{const_name dummy_pattern}, _)) ((ts, mode), i) = ((ts, mode), i + 1)
13.269 | mk_mode t ((ts, mode), i) = ((ts @ [t], mode @ [i]), i + 1);
13.270
13.271 - val module' = Codegen.if_library thyname module;
13.272 - val gr1 = mk_extra_defs thy defs
13.273 - (mk_ind_def thy defs gr dep names module'
13.274 + val module' = Codegen.if_library codegen_mode thyname module;
13.275 + val gr1 = mk_extra_defs thy codegen_mode defs
13.276 + (mk_ind_def thy codegen_mode defs gr dep names module'
13.277 [] (prep_intrs intrs) k) dep names module' [u];
13.278 val (modes, _) = lookup_modes gr1 dep;
13.279 val (ts', is) =
13.280 @@ -658,8 +661,9 @@
13.281 val mode = find_mode gr1 dep s u modes is;
13.282 val _ = if is_query orelse not (needs_random (the mode)) then ()
13.283 else warning ("Illegal use of random data generators in " ^ s);
13.284 - val (in_ps, gr2) = fold_map (Codegen.invoke_codegen thy defs dep module true) ts' gr1;
13.285 - val (ps, gr3) = compile_expr thy defs dep module false modes (mode, u) gr2;
13.286 + val (in_ps, gr2) =
13.287 + fold_map (Codegen.invoke_codegen thy codegen_mode defs dep module true) ts' gr1;
13.288 + val (ps, gr3) = compile_expr thy codegen_mode defs dep module false modes (mode, u) gr2;
13.289 in
13.290 (Pretty.block (ps @ (if null in_ps then [] else [Pretty.brk 1]) @
13.291 separate (Pretty.brk 1) in_ps), gr3)
13.292 @@ -675,7 +679,7 @@
13.293 (list_comb (Const (s ^ "_aux", Ts @ [U] ---> HOLogic.boolT), ts @ [u]))))
13.294 end;
13.295
13.296 -fun mk_fun thy defs name eqns dep module module' gr =
13.297 +fun mk_fun thy codegen_mode defs name eqns dep module module' gr =
13.298 case try (Codegen.get_node gr) name of
13.299 NONE =>
13.300 let
13.301 @@ -693,7 +697,7 @@
13.302 Pretty.brk 1, Codegen.str "DSeq.hd", Pretty.brk 1,
13.303 Codegen.parens (Pretty.block (separate (Pretty.brk 1) (Codegen.str mode_id ::
13.304 vars)))]) ^ ";\n\n";
13.305 - val gr'' = mk_ind_def thy defs (Codegen.add_edge (name, dep)
13.306 + val gr'' = mk_ind_def thy codegen_mode defs (Codegen.add_edge (name, dep)
13.307 (Codegen.new_node (name, (NONE, module', s)) gr')) name [pname] module'
13.308 [(pname, [([], mode)])] clauses 0;
13.309 val (modes, _) = lookup_modes gr'' dep;
13.310 @@ -726,7 +730,7 @@
13.311 else p
13.312 end;
13.313
13.314 -fun inductive_codegen thy defs dep module brack t gr = (case strip_comb t of
13.315 +fun inductive_codegen thy codegen_mode defs dep module brack t gr = (case strip_comb t of
13.316 (Const (@{const_name Collect}, _), [u]) =>
13.317 let val (r, Ts, fs) = HOLogic.strip_psplits u
13.318 in case strip_comb r of
13.319 @@ -743,7 +747,7 @@
13.320 if null (duplicates op = ots) andalso
13.321 closed ts1 andalso closed its
13.322 then
13.323 - let val (call_p, gr') = mk_ind_call thy defs dep module true
13.324 + let val (call_p, gr') = mk_ind_call thy codegen_mode defs dep module true
13.325 s T (ts1 @ ts2') names thyname k intrs gr
13.326 in SOME ((if brack then Codegen.parens else I) (Pretty.block
13.327 [Codegen.str "Set", Pretty.brk 1, Codegen.str "(DSeq.list_of", Pretty.brk 1,
13.328 @@ -762,20 +766,21 @@
13.329 (case (get_clauses thy s, Codegen.get_assoc_code thy (s, T)) of
13.330 (SOME (names, thyname, k, intrs), NONE) =>
13.331 if length ts < k then NONE else SOME
13.332 - (let val (call_p, gr') = mk_ind_call thy defs dep module false
13.333 + (let val (call_p, gr') = mk_ind_call thy codegen_mode defs dep module false
13.334 s T (map Term.no_dummy_patterns ts) names thyname k intrs gr
13.335 in (mk_funcomp brack "?!"
13.336 (length (binder_types T) - length ts) (Codegen.parens call_p), gr')
13.337 - end handle TERM _ => mk_ind_call thy defs dep module true
13.338 + end handle TERM _ => mk_ind_call thy codegen_mode defs dep module true
13.339 s T ts names thyname k intrs gr )
13.340 | _ => NONE)
13.341 | SOME eqns =>
13.342 let
13.343 val (_, thyname) :: _ = eqns;
13.344 - val (id, gr') = mk_fun thy defs s (Codegen.preprocess thy (map fst (rev eqns)))
13.345 - dep module (Codegen.if_library thyname module) gr;
13.346 - val (ps, gr'') = fold_map
13.347 - (Codegen.invoke_codegen thy defs dep module true) ts gr';
13.348 + val (id, gr') =
13.349 + mk_fun thy codegen_mode defs s (Codegen.preprocess thy (map fst (rev eqns)))
13.350 + dep module (Codegen.if_library codegen_mode thyname module) gr;
13.351 + val (ps, gr'') =
13.352 + fold_map (Codegen.invoke_codegen thy codegen_mode defs dep module true) ts gr';
13.353 in SOME (Codegen.mk_app brack (Codegen.str id) ps, gr'')
13.354 end)
13.355 | _ => NONE);
13.356 @@ -830,8 +835,9 @@
13.357 val pred = HOLogic.mk_Trueprop (list_comb
13.358 (Const (Sign.intern_const thy' "quickcheckp", T),
13.359 map Term.dummy_pattern Ts));
13.360 - val (code, gr) = setmp_CRITICAL Codegen.mode ["term_of", "test", "random_ind"]
13.361 - (Codegen.generate_code_i thy' [] "Generated") [("testf", pred)];
13.362 + val (code, gr) =
13.363 + Codegen.generate_code_i thy' ["term_of", "test", "random_ind"] [] "Generated"
13.364 + [("testf", pred)];
13.365 val s = "structure TestTerm =\nstruct\n\n" ^
13.366 cat_lines (map snd code) ^
13.367 "\nopen Generated;\n\n" ^ Codegen.string_of
14.1 --- a/src/HOL/Tools/recfun_codegen.ML Wed Apr 20 10:14:24 2011 +0200
14.2 +++ b/src/HOL/Tools/recfun_codegen.ML Wed Apr 20 11:21:12 2011 +0200
14.3 @@ -70,7 +70,7 @@
14.4 if member (op =) xs x then xs
14.5 else fold (cycle g) (flat (Graph.all_paths (fst g) (x, x))) (x :: xs);
14.6
14.7 -fun add_rec_funs thy defs dep module eqs gr =
14.8 +fun add_rec_funs thy mode defs dep module eqs gr =
14.9 let
14.10 fun dest_eq t = (fst (const_of t) ^ mk_suffix thy defs (const_of t),
14.11 Logic.dest_equals (Codegen.rename_term t));
14.12 @@ -81,10 +81,10 @@
14.13 fun mk_fundef module fname first [] gr = ([], gr)
14.14 | mk_fundef module fname first ((fname' : string, (lhs, rhs)) :: xs) gr =
14.15 let
14.16 - val (pl, gr1) = Codegen.invoke_codegen thy defs dname module false lhs gr;
14.17 - val (pr, gr2) = Codegen.invoke_codegen thy defs dname module false rhs gr1;
14.18 + val (pl, gr1) = Codegen.invoke_codegen thy mode defs dname module false lhs gr;
14.19 + val (pr, gr2) = Codegen.invoke_codegen thy mode defs dname module false rhs gr1;
14.20 val (rest, gr3) = mk_fundef module fname' false xs gr2 ;
14.21 - val (ty, gr4) = Codegen.invoke_tycodegen thy defs dname module false T gr3;
14.22 + val (ty, gr4) = Codegen.invoke_tycodegen thy mode defs dname module false T gr3;
14.23 val num_args = (length o snd o strip_comb) lhs;
14.24 val prfx = if fname = fname' then " |"
14.25 else if not first then "and"
14.26 @@ -121,7 +121,7 @@
14.27 if not (member (op =) xs dep) then
14.28 let
14.29 val thmss as (_, thyname) :: _ = map (get_equations thy defs) cs;
14.30 - val module' = Codegen.if_library thyname module;
14.31 + val module' = Codegen.if_library mode thyname module;
14.32 val eqs'' = map (dest_eq o prop_of) (maps fst thmss);
14.33 val (fundef', gr3) = mk_fundef module' "" true eqs''
14.34 (Codegen.add_edge (dname, dep)
14.35 @@ -137,7 +137,7 @@
14.36 else if s = dep then gr else Codegen.add_edge (s, dep) gr))
14.37 end;
14.38
14.39 -fun recfun_codegen thy defs dep module brack t gr =
14.40 +fun recfun_codegen thy mode defs dep module brack t gr =
14.41 (case strip_comb t of
14.42 (Const (p as (s, T)), ts) =>
14.43 (case (get_equations thy defs p, Codegen.get_assoc_code thy (s, T)) of
14.44 @@ -145,12 +145,12 @@
14.45 | (_, SOME _) => NONE
14.46 | ((eqns, thyname), NONE) =>
14.47 let
14.48 - val module' = Codegen.if_library thyname module;
14.49 + val module' = Codegen.if_library mode thyname module;
14.50 val (ps, gr') = fold_map
14.51 - (Codegen.invoke_codegen thy defs dep module true) ts gr;
14.52 + (Codegen.invoke_codegen thy mode defs dep module true) ts gr;
14.53 val suffix = mk_suffix thy defs p;
14.54 val (module'', gr'') =
14.55 - add_rec_funs thy defs dep module' (map prop_of eqns) gr';
14.56 + add_rec_funs thy mode defs dep module' (map prop_of eqns) gr';
14.57 val (fname, gr''') = Codegen.mk_const_id module'' (s ^ suffix) gr''
14.58 in
14.59 SOME (Codegen.mk_app brack (Codegen.str (Codegen.mk_qual_id module fname)) ps, gr''')
15.1 --- a/src/Pure/IsaMakefile Wed Apr 20 10:14:24 2011 +0200
15.2 +++ b/src/Pure/IsaMakefile Wed Apr 20 11:21:12 2011 +0200
15.3 @@ -253,6 +253,7 @@
15.4 thm.ML \
15.5 type.ML \
15.6 type_infer.ML \
15.7 + type_infer_context.ML \
15.8 unify.ML \
15.9 variable.ML
15.10 @./mk
16.1 --- a/src/Pure/Isar/class.ML Wed Apr 20 10:14:24 2011 +0200
16.2 +++ b/src/Pure/Isar/class.ML Wed Apr 20 11:21:12 2011 +0200
16.3 @@ -462,7 +462,7 @@
16.4 handle Sorts.CLASS_ERROR e => error (Sorts.class_error ctxt e);
16.5 val inst = map_type_tvar
16.6 (fn (vi, sort) => TVar (vi, the_default sort (Vartab.lookup tvartab vi)));
16.7 - in if Vartab.is_empty tvartab then NONE else SOME ((map o map_types) inst ts) end;
16.8 + in if Vartab.is_empty tvartab then ts else (map o map_types) inst ts end;
16.9
16.10
16.11 (* target *)
16.12 @@ -535,10 +535,7 @@
16.13 val consts = Sign.consts_of thy;
16.14 val improve_constraints = AList.lookup (op =)
16.15 (map (fn (_, (class, (c, _))) => (c, [[class]])) class_params);
16.16 - fun resort_check ts ctxt =
16.17 - (case resort_terms ctxt algebra consts improve_constraints ts of
16.18 - NONE => NONE
16.19 - | SOME ts' => SOME (ts', ctxt));
16.20 + fun resort_check ctxt ts = resort_terms ctxt algebra consts improve_constraints ts;
16.21 val lookup_inst_param = AxClass.lookup_inst_param consts params;
16.22 fun improve (c, ty) =
16.23 (case lookup_inst_param (c, ty) of
17.1 --- a/src/Pure/Isar/class_declaration.ML Wed Apr 20 10:14:24 2011 +0200
17.2 +++ b/src/Pure/Isar/class_declaration.ML Wed Apr 20 11:21:12 2011 +0200
17.3 @@ -139,19 +139,18 @@
17.4 (fn T as TFree _ => T | T as TVar (vi, _) =>
17.5 if Type_Infer.is_param vi then Type_Infer.param 0 (Name.aT, sort') else T) Ts
17.6 end;
17.7 - fun add_typ_check level name f = Context.proof_map
17.8 - (Syntax.add_typ_check level name (fn Ts => fn ctxt =>
17.9 - let val Ts' = f Ts in if eq_list (op =) (Ts, Ts') then NONE else SOME (Ts', ctxt) end));
17.10
17.11 (* preprocessing elements, retrieving base sort from type-checked elements *)
17.12 - val raw_supexpr = (map (fn sup => (sup, (("", false),
17.13 - Expression.Positional []))) sups, []);
17.14 - val init_class_body = fold (Proof_Context.add_const_constraint o apsnd SOME) base_constraints
17.15 + val raw_supexpr =
17.16 + (map (fn sup => (sup, (("", false), Expression.Positional []))) sups, []);
17.17 + val init_class_body =
17.18 + fold (Proof_Context.add_const_constraint o apsnd SOME) base_constraints
17.19 #> Class.redeclare_operations thy sups
17.20 - #> add_typ_check 10 "reject_bcd_etc" reject_bcd_etc
17.21 - #> add_typ_check ~10 "singleton_fixate" singleton_fixate;
17.22 - val ((raw_supparams, _, raw_inferred_elems), _) = Proof_Context.init_global thy
17.23 - |> add_typ_check 5 "after_infer_fixate" after_infer_fixate
17.24 + #> Context.proof_map (Syntax.add_typ_check 10 "reject_bcd_etc" (K reject_bcd_etc))
17.25 + #> Context.proof_map (Syntax.add_typ_check ~10 "singleton_fixate" (K singleton_fixate));
17.26 + val ((raw_supparams, _, raw_inferred_elems), _) =
17.27 + Proof_Context.init_global thy
17.28 + |> Context.proof_map (Syntax.add_typ_check 5 "after_infer_fixate" (K after_infer_fixate))
17.29 |> prep_decl raw_supexpr init_class_body raw_elems;
17.30 fun filter_element (Element.Fixes []) = NONE
17.31 | filter_element (e as Element.Fixes _) = SOME e
17.32 @@ -165,7 +164,7 @@
17.33 fun fold_element_types f (Element.Fixes fxs) = fold (fn (_, SOME T, _) => f T) fxs
17.34 | fold_element_types f (Element.Constrains cnstrs) = fold (f o snd) cnstrs
17.35 | fold_element_types f (Element.Assumes assms) = fold (fold (fn (t, ts) =>
17.36 - fold_types f t #> (fold o fold_types) f ts) o snd) assms
17.37 + fold_types f t #> (fold o fold_types) f ts) o snd) assms;
17.38 val base_sort = if null inferred_elems then proto_base_sort else
17.39 case (fold o fold_element_types) Term.add_tfreesT inferred_elems []
17.40 of [] => error "No type variable in class specification"
18.1 --- a/src/Pure/Isar/overloading.ML Wed Apr 20 10:14:24 2011 +0200
18.2 +++ b/src/Pure/Isar/overloading.ML Wed Apr 20 11:21:12 2011 +0200
18.3 @@ -19,13 +19,13 @@
18.4 structure Overloading: OVERLOADING =
18.5 struct
18.6
18.7 -(** generic check/uncheck combinators for improvable constants **)
18.8 +(* generic check/uncheck combinators for improvable constants *)
18.9
18.10 type improvable_syntax = ((((string * typ) list * (string * typ) list) *
18.11 ((((string * typ -> (typ * typ) option) * (string * typ -> (typ * term) option)) * bool) *
18.12 (term * term) list)) * bool);
18.13
18.14 -structure ImprovableSyntax = Proof_Data
18.15 +structure Improvable_Syntax = Proof_Data
18.16 (
18.17 type T = {
18.18 primary_constraints: (string * typ) list,
18.19 @@ -47,16 +47,17 @@
18.20 };
18.21 );
18.22
18.23 -fun map_improvable_syntax f = ImprovableSyntax.map (fn { primary_constraints,
18.24 - secondary_constraints, improve, subst, consider_abbrevs, unchecks, passed } =>
18.25 +fun map_improvable_syntax f = Improvable_Syntax.map (fn {primary_constraints,
18.26 + secondary_constraints, improve, subst, consider_abbrevs, unchecks, passed} =>
18.27 let
18.28 val (((primary_constraints', secondary_constraints'),
18.29 (((improve', subst'), consider_abbrevs'), unchecks')), passed')
18.30 = f (((primary_constraints, secondary_constraints),
18.31 (((improve, subst), consider_abbrevs), unchecks)), passed)
18.32 - in { primary_constraints = primary_constraints', secondary_constraints = secondary_constraints',
18.33 + in
18.34 + {primary_constraints = primary_constraints', secondary_constraints = secondary_constraints',
18.35 improve = improve', subst = subst', consider_abbrevs = consider_abbrevs',
18.36 - unchecks = unchecks', passed = passed' }
18.37 + unchecks = unchecks', passed = passed'}
18.38 end);
18.39
18.40 val mark_passed = (map_improvable_syntax o apsnd) (K true);
18.41 @@ -65,8 +66,8 @@
18.42 let
18.43 val thy = Proof_Context.theory_of ctxt;
18.44
18.45 - val { secondary_constraints, improve, subst, consider_abbrevs, passed, ... } =
18.46 - ImprovableSyntax.get ctxt;
18.47 + val {secondary_constraints, improve, subst, consider_abbrevs, passed, ...} =
18.48 + Improvable_Syntax.get ctxt;
18.49 val is_abbrev = consider_abbrevs andalso Proof_Context.abbrev_mode ctxt;
18.50 val passed_or_abbrev = passed orelse is_abbrev;
18.51 fun accumulate_improvements (Const (c, ty)) =
18.52 @@ -87,38 +88,38 @@
18.53 | _ => NONE) t;
18.54 val ts'' = if is_abbrev then ts' else map apply_subst ts';
18.55 in
18.56 - if eq_list (op aconv) (ts, ts'') andalso passed_or_abbrev then NONE else
18.57 - if passed_or_abbrev then SOME (ts'', ctxt)
18.58 - else SOME (ts'', ctxt
18.59 - |> fold (Proof_Context.add_const_constraint o apsnd SOME) secondary_constraints
18.60 - |> mark_passed)
18.61 + if eq_list (op aconv) (ts, ts'') andalso passed_or_abbrev then NONE
18.62 + else if passed_or_abbrev then SOME (ts'', ctxt)
18.63 + else
18.64 + SOME (ts'', ctxt
18.65 + |> fold (Proof_Context.add_const_constraint o apsnd SOME) secondary_constraints
18.66 + |> mark_passed)
18.67 end;
18.68
18.69 fun rewrite_liberal thy unchecks t =
18.70 - case try (Pattern.rewrite_term thy unchecks []) t
18.71 - of NONE => NONE
18.72 - | SOME t' => if t aconv t' then NONE else SOME t';
18.73 + (case try (Pattern.rewrite_term thy unchecks []) t of
18.74 + NONE => NONE
18.75 + | SOME t' => if t aconv t' then NONE else SOME t');
18.76
18.77 fun improve_term_uncheck ts ctxt =
18.78 let
18.79 val thy = Proof_Context.theory_of ctxt;
18.80 - val unchecks = (#unchecks o ImprovableSyntax.get) ctxt;
18.81 + val {unchecks, ...} = Improvable_Syntax.get ctxt;
18.82 val ts' = map (rewrite_liberal thy unchecks) ts;
18.83 in if exists is_some ts' then SOME (map2 the_default ts ts', ctxt) else NONE end;
18.84
18.85 fun set_primary_constraints ctxt =
18.86 - let
18.87 - val { primary_constraints, ... } = ImprovableSyntax.get ctxt;
18.88 + let val {primary_constraints, ...} = Improvable_Syntax.get ctxt;
18.89 in fold (Proof_Context.add_const_constraint o apsnd SOME) primary_constraints ctxt end;
18.90
18.91 val activate_improvable_syntax =
18.92 Context.proof_map
18.93 - (Syntax.add_term_check 0 "improvement" improve_term_check
18.94 - #> Syntax.add_term_uncheck 0 "improvement" improve_term_uncheck)
18.95 + (Syntax.context_term_check 0 "improvement" improve_term_check
18.96 + #> Syntax.context_term_uncheck 0 "improvement" improve_term_uncheck)
18.97 #> set_primary_constraints;
18.98
18.99
18.100 -(** overloading target **)
18.101 +(* overloading target *)
18.102
18.103 structure Data = Proof_Data
18.104 (
18.105 @@ -129,16 +130,18 @@
18.106 val get_overloading = Data.get o Local_Theory.target_of;
18.107 val map_overloading = Local_Theory.target o Data.map;
18.108
18.109 -fun operation lthy b = get_overloading lthy
18.110 +fun operation lthy b =
18.111 + get_overloading lthy
18.112 |> get_first (fn ((c, _), (v, checked)) =>
18.113 if Binding.name_of b = v then SOME (c, (v, checked)) else NONE);
18.114
18.115 fun synchronize_syntax ctxt =
18.116 let
18.117 val overloading = Data.get ctxt;
18.118 - fun subst (c, ty) = case AList.lookup (op =) overloading (c, ty)
18.119 - of SOME (v, _) => SOME (ty, Free (v, ty))
18.120 - | NONE => NONE;
18.121 + fun subst (c, ty) =
18.122 + (case AList.lookup (op =) overloading (c, ty) of
18.123 + SOME (v, _) => SOME (ty, Free (v, ty))
18.124 + | NONE => NONE);
18.125 val unchecks =
18.126 map (fn (c_ty as (_, ty), (v, _)) => (Free (v, ty), Const c_ty)) overloading;
18.127 in
18.128 @@ -155,12 +158,13 @@
18.129 #-> (fn (_, def) => pair (Const (c, U), def))
18.130
18.131 fun foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
18.132 - case operation lthy b
18.133 - of SOME (c, (v, checked)) => if mx <> NoSyn
18.134 - then error ("Illegal mixfix syntax for overloaded constant " ^ quote c)
18.135 - else lthy |> define_overloaded (c, U) (v, checked) (b_def, rhs)
18.136 - | NONE => lthy |>
18.137 - Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
18.138 + (case operation lthy b of
18.139 + SOME (c, (v, checked)) =>
18.140 + if mx <> NoSyn
18.141 + then error ("Illegal mixfix syntax for overloaded constant " ^ quote c)
18.142 + else lthy |> define_overloaded (c, U) (v, checked) (b_def, rhs)
18.143 + | NONE => lthy
18.144 + |> Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params));
18.145
18.146 fun pretty lthy =
18.147 let
18.148 @@ -177,8 +181,8 @@
18.149 val _ =
18.150 if null overloading then ()
18.151 else
18.152 - error ("Missing definition(s) for parameter(s) " ^ commas (map (quote
18.153 - o Syntax.string_of_term lthy o Const o fst) overloading));
18.154 + error ("Missing definition(s) for parameter(s) " ^
18.155 + commas_quote (map (Syntax.string_of_term lthy o Const o fst) overloading));
18.156 in lthy end;
18.157
18.158 fun gen_overloading prep_const raw_overloading thy =
19.1 --- a/src/Pure/Isar/proof_context.ML Wed Apr 20 10:14:24 2011 +0200
19.2 +++ b/src/Pure/Isar/proof_context.ML Wed Apr 20 11:21:12 2011 +0200
19.3 @@ -76,7 +76,6 @@
19.4 val get_sort: Proof.context -> (indexname * sort) list -> indexname -> sort
19.5 val check_tvar: Proof.context -> indexname * sort -> indexname * sort
19.6 val check_tfree: Proof.context -> string * sort -> string * sort
19.7 - val standard_infer_types: Proof.context -> term list -> term list
19.8 val intern_skolem: Proof.context -> string -> string option
19.9 val read_term_pattern: Proof.context -> string -> term
19.10 val read_term_schematic: Proof.context -> string -> term
19.11 @@ -678,38 +677,27 @@
19.12 end;
19.13
19.14
19.15 -(* type checking/inference *)
19.16 +(* check/uncheck *)
19.17
19.18 fun def_type ctxt =
19.19 let val Mode {pattern, ...} = get_mode ctxt
19.20 in Variable.def_type ctxt pattern end;
19.21
19.22 -fun standard_infer_types ctxt =
19.23 - Type_Infer.infer_types ctxt (try (Consts.the_constraint (consts_of ctxt))) (def_type ctxt);
19.24 -
19.25 local
19.26
19.27 fun standard_typ_check ctxt =
19.28 map (cert_typ_mode (Type.get_mode ctxt) ctxt) #>
19.29 map (prepare_patternT ctxt);
19.30
19.31 -fun standard_term_check ctxt =
19.32 - standard_infer_types ctxt #>
19.33 - map (expand_abbrevs ctxt);
19.34 -
19.35 fun standard_term_uncheck ctxt =
19.36 map (contract_abbrevs ctxt);
19.37
19.38 -fun add eq what f = Context.>> (what (fn xs => fn ctxt =>
19.39 - let val xs' = f ctxt xs in if eq_list eq (xs, xs') then NONE else SOME (xs', ctxt) end));
19.40 -
19.41 in
19.42
19.43 -val _ = add (op =) (Syntax.add_typ_check 0 "standard") standard_typ_check;
19.44 -val _ = add (op aconv) (Syntax.add_term_check 0 "standard") standard_term_check;
19.45 -val _ = add (op aconv) (Syntax.add_term_check 100 "fixate") prepare_patterns;
19.46 -
19.47 -val _ = add (op aconv) (Syntax.add_term_uncheck 0 "standard") standard_term_uncheck;
19.48 +val _ = Context.>>
19.49 + (Syntax.add_typ_check 0 "standard" standard_typ_check #>
19.50 + Syntax.add_term_check 100 "fixate" prepare_patterns #>
19.51 + Syntax.add_term_uncheck 0 "standard" standard_term_uncheck);
19.52
19.53 end;
19.54
20.1 --- a/src/Pure/Isar/skip_proof.ML Wed Apr 20 10:14:24 2011 +0200
20.2 +++ b/src/Pure/Isar/skip_proof.ML Wed Apr 20 11:21:12 2011 +0200
20.3 @@ -7,6 +7,7 @@
20.4
20.5 signature SKIP_PROOF =
20.6 sig
20.7 + val make_thm_cterm: cterm -> thm
20.8 val make_thm: theory -> term -> thm
20.9 val cheat_tac: theory -> tactic
20.10 val prove: Proof.context -> string list -> term list -> term ->
20.11 @@ -20,14 +21,14 @@
20.12
20.13 (* oracle setup *)
20.14
20.15 -val (_, skip_proof) = Context.>>> (Context.map_theory_result
20.16 - (Thm.add_oracle (Binding.name "skip_proof", fn (thy, prop) => Thm.cterm_of thy prop)));
20.17 +val (_, make_thm_cterm) =
20.18 + Context.>>> (Context.map_theory_result (Thm.add_oracle (Binding.name "skip_proof", I)));
20.19 +
20.20 +fun make_thm thy prop = make_thm_cterm (Thm.cterm_of thy prop);
20.21
20.22
20.23 (* basic cheating *)
20.24
20.25 -fun make_thm thy prop = skip_proof (thy, prop);
20.26 -
20.27 fun cheat_tac thy st =
20.28 ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
20.29
21.1 --- a/src/Pure/Proof/extraction.ML Wed Apr 20 10:14:24 2011 +0200
21.2 +++ b/src/Pure/Proof/extraction.ML Wed Apr 20 11:21:12 2011 +0200
21.3 @@ -32,16 +32,17 @@
21.4
21.5 (**** tools ****)
21.6
21.7 -fun add_syntax thy =
21.8 - thy
21.9 - |> Theory.copy
21.10 - |> Sign.root_path
21.11 - |> Sign.add_types_global [(Binding.name "Type", 0, NoSyn), (Binding.name "Null", 0, NoSyn)]
21.12 - |> Sign.add_consts
21.13 - [(Binding.name "typeof", "'b::{} => Type", NoSyn),
21.14 - (Binding.name "Type", "'a::{} itself => Type", NoSyn),
21.15 - (Binding.name "Null", "Null", NoSyn),
21.16 - (Binding.name "realizes", "'a::{} => 'b::{} => 'b", NoSyn)];
21.17 +val typ = Simple_Syntax.read_typ;
21.18 +
21.19 +val add_syntax =
21.20 + Theory.copy
21.21 + #> Sign.root_path
21.22 + #> Sign.add_types_global [(Binding.name "Type", 0, NoSyn), (Binding.name "Null", 0, NoSyn)]
21.23 + #> Sign.add_consts_i
21.24 + [(Binding.name "typeof", typ "'b => Type", NoSyn),
21.25 + (Binding.name "Type", typ "'a itself => Type", NoSyn),
21.26 + (Binding.name "Null", typ "Null", NoSyn),
21.27 + (Binding.name "realizes", typ "'a => 'b => 'b", NoSyn)];
21.28
21.29 val nullT = Type ("Null", []);
21.30 val nullt = Const ("Null", nullT);
21.31 @@ -150,11 +151,13 @@
21.32 let
21.33 val vs = Term.add_vars t [];
21.34 val fs = Term.add_frees t [];
21.35 - in fn
21.36 - Var (ixn, _) => (case AList.lookup (op =) vs ixn of
21.37 + in
21.38 + fn Var (ixn, _) =>
21.39 + (case AList.lookup (op =) vs ixn of
21.40 NONE => error "get_var_type: no such variable in term"
21.41 | SOME T => Var (ixn, T))
21.42 - | Free (s, _) => (case AList.lookup (op =) fs s of
21.43 + | Free (s, _) =>
21.44 + (case AList.lookup (op =) fs s of
21.45 NONE => error "get_var_type: no such variable in term"
21.46 | SOME T => Free (s, T))
21.47 | _ => error "get_var_type: not a variable"
21.48 @@ -163,7 +166,7 @@
21.49 fun read_term thy T s =
21.50 let
21.51 val ctxt = Proof_Context.init_global thy
21.52 - |> Proof_Syntax.strip_sorts_consttypes
21.53 + |> Config.put Type_Infer_Context.const_sorts false
21.54 |> Proof_Context.set_defsort [];
21.55 val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term;
21.56 in parse ctxt s |> Type.constraint T |> Syntax.check_term ctxt end;
21.57 @@ -528,7 +531,7 @@
21.58 | corr d defs vs ts Ts hs cs (AbsP (s, SOME prop, prf)) (AbsP (_, _, prf')) t =
21.59 let
21.60 val T = etype_of thy' vs Ts prop;
21.61 - val u = if T = nullT then
21.62 + val u = if T = nullT then
21.63 (case t of SOME u => SOME (incr_boundvars 1 u) | NONE => NONE)
21.64 else (case t of SOME (Abs (_, _, u)) => SOME u | _ => NONE);
21.65 val (defs', corr_prf) =
22.1 --- a/src/Pure/Proof/proof_syntax.ML Wed Apr 20 10:14:24 2011 +0200
22.2 +++ b/src/Pure/Proof/proof_syntax.ML Wed Apr 20 11:21:12 2011 +0200
22.3 @@ -11,7 +11,6 @@
22.4 val proof_of_term: theory -> bool -> term -> Proofterm.proof
22.5 val term_of_proof: Proofterm.proof -> term
22.6 val cterm_of_proof: theory -> Proofterm.proof -> cterm * (cterm -> Proofterm.proof)
22.7 - val strip_sorts_consttypes: Proof.context -> Proof.context
22.8 val read_term: theory -> bool -> typ -> string -> term
22.9 val read_proof: theory -> bool -> bool -> string -> Proofterm.proof
22.10 val proof_syntax: Proofterm.proof -> theory -> theory
22.11 @@ -201,13 +200,6 @@
22.12 (cterm_of thy' (term_of_proof prf), proof_of_term thy true o Thm.term_of)
22.13 end;
22.14
22.15 -fun strip_sorts_consttypes ctxt =
22.16 - let val {constants = (_, tab), ...} = Consts.dest (Proof_Context.consts_of ctxt)
22.17 - in Symtab.fold (fn (s, (T, _)) =>
22.18 - Proof_Context.add_const_constraint (s, SOME (Type.strip_sorts T)))
22.19 - tab ctxt
22.20 - end;
22.21 -
22.22 fun read_term thy topsort =
22.23 let
22.24 val thm_names = filter_out (fn s => s = "") (map fst (Global_Theory.all_thms_of thy));
22.25 @@ -219,10 +211,7 @@
22.26 |> Proof_Context.init_global
22.27 |> Proof_Context.allow_dummies
22.28 |> Proof_Context.set_mode Proof_Context.mode_schematic
22.29 - |> (if topsort then
22.30 - strip_sorts_consttypes #>
22.31 - Proof_Context.set_defsort []
22.32 - else I);
22.33 + |> topsort ? (Config.put Type_Infer_Context.const_sorts false #> Proof_Context.set_defsort []);
22.34 in
22.35 fn ty => fn s =>
22.36 (if ty = propT then Syntax.parse_prop else Syntax.parse_term) ctxt s
23.1 --- a/src/Pure/ROOT.ML Wed Apr 20 10:14:24 2011 +0200
23.2 +++ b/src/Pure/ROOT.ML Wed Apr 20 11:21:12 2011 +0200
23.3 @@ -173,6 +173,7 @@
23.4 use "type_infer.ML";
23.5 use "Syntax/local_syntax.ML";
23.6 use "Isar/proof_context.ML";
23.7 +use "type_infer_context.ML";
23.8 use "Syntax/syntax_phases.ML";
23.9 use "Isar/local_defs.ML";
23.10
24.1 --- a/src/Pure/Syntax/syntax.ML Wed Apr 20 10:14:24 2011 +0200
24.2 +++ b/src/Pure/Syntax/syntax.ML Wed Apr 20 11:21:12 2011 +0200
24.3 @@ -31,18 +31,26 @@
24.4 val unparse_typ: Proof.context -> typ -> Pretty.T
24.5 val unparse_term: Proof.context -> term -> Pretty.T
24.6 val print_checks: Proof.context -> unit
24.7 - val add_typ_check: int -> string ->
24.8 + val context_typ_check: int -> string ->
24.9 (typ list -> Proof.context -> (typ list * Proof.context) option) ->
24.10 Context.generic -> Context.generic
24.11 - val add_term_check: int -> string ->
24.12 + val context_term_check: int -> string ->
24.13 (term list -> Proof.context -> (term list * Proof.context) option) ->
24.14 Context.generic -> Context.generic
24.15 - val add_typ_uncheck: int -> string ->
24.16 + val context_typ_uncheck: int -> string ->
24.17 (typ list -> Proof.context -> (typ list * Proof.context) option) ->
24.18 Context.generic -> Context.generic
24.19 - val add_term_uncheck: int -> string ->
24.20 + val context_term_uncheck: int -> string ->
24.21 (term list -> Proof.context -> (term list * Proof.context) option) ->
24.22 Context.generic -> Context.generic
24.23 + val add_typ_check: int -> string -> (Proof.context -> typ list -> typ list) ->
24.24 + Context.generic -> Context.generic
24.25 + val add_term_check: int -> string -> (Proof.context -> term list -> term list) ->
24.26 + Context.generic -> Context.generic
24.27 + val add_typ_uncheck: int -> string -> (Proof.context -> typ list -> typ list) ->
24.28 + Context.generic -> Context.generic
24.29 + val add_term_uncheck: int -> string -> (Proof.context -> term list -> term list) ->
24.30 + Context.generic -> Context.generic
24.31 val typ_check: Proof.context -> typ list -> typ list
24.32 val term_check: Proof.context -> term list -> term list
24.33 val typ_uncheck: Proof.context -> typ list -> typ list
24.34 @@ -224,13 +232,11 @@
24.35
24.36 (* context-sensitive (un)checking *)
24.37
24.38 -local
24.39 -
24.40 type key = int * bool;
24.41 -type 'a check = 'a list -> Proof.context -> ('a list * Proof.context) option;
24.42
24.43 structure Checks = Generic_Data
24.44 (
24.45 + type 'a check = 'a list -> Proof.context -> ('a list * Proof.context) option;
24.46 type T =
24.47 ((key * ((string * typ check) * stamp) list) list *
24.48 (key * ((string * term check) * stamp) list) list);
24.49 @@ -241,27 +247,6 @@
24.50 AList.join (op =) (K (Library.merge (eq_snd (op =)))) (term_checks1, term_checks2));
24.51 );
24.52
24.53 -fun gen_add which (key: key) name f =
24.54 - Checks.map (which (AList.map_default op = (key, []) (cons ((name, f), stamp ()))));
24.55 -
24.56 -fun check_stage fs = perhaps_loop (perhaps_apply (map uncurry fs));
24.57 -
24.58 -fun gen_check which uncheck ctxt0 xs0 =
24.59 - let
24.60 - val funs = which (Checks.get (Context.Proof ctxt0))
24.61 - |> map_filter (fn ((i, u), fs) => if uncheck = u then SOME (i, map (snd o fst) fs) else NONE)
24.62 - |> Library.sort (int_ord o pairself fst) |> map snd
24.63 - |> not uncheck ? map rev;
24.64 - val check_all = perhaps_apply (map check_stage funs);
24.65 - in #1 (perhaps check_all (xs0, ctxt0)) end;
24.66 -
24.67 -fun map_sort f S =
24.68 - (case f (TFree ("", S)) of
24.69 - TFree ("", S') => S'
24.70 - | _ => raise TYPE ("map_sort", [TFree ("", S)], []));
24.71 -
24.72 -in
24.73 -
24.74 fun print_checks ctxt =
24.75 let
24.76 fun split_checks checks =
24.77 @@ -283,15 +268,50 @@
24.78 pretty_checks "term_unchecks" term_unchecks
24.79 end |> Pretty.chunks |> Pretty.writeln;
24.80
24.81 -fun add_typ_check stage = gen_add apfst (stage, false);
24.82 -fun add_term_check stage = gen_add apsnd (stage, false);
24.83 -fun add_typ_uncheck stage = gen_add apfst (stage, true);
24.84 -fun add_term_uncheck stage = gen_add apsnd (stage, true);
24.85
24.86 -val typ_check = gen_check fst false;
24.87 -val term_check = gen_check snd false;
24.88 -val typ_uncheck = gen_check fst true;
24.89 -val term_uncheck = gen_check snd true;
24.90 +local
24.91 +
24.92 +fun context_check which (key: key) name f =
24.93 + Checks.map (which (AList.map_default op = (key, []) (cons ((name, f), stamp ()))));
24.94 +
24.95 +fun simple_check eq f xs ctxt =
24.96 + let val xs' = f ctxt xs
24.97 + in if eq_list eq (xs, xs') then NONE else SOME (xs', ctxt) end;
24.98 +
24.99 +in
24.100 +
24.101 +fun context_typ_check stage = context_check apfst (stage, false);
24.102 +fun context_term_check stage = context_check apsnd (stage, false);
24.103 +fun context_typ_uncheck stage = context_check apfst (stage, true);
24.104 +fun context_term_uncheck stage = context_check apsnd (stage, true);
24.105 +
24.106 +fun add_typ_check key name f = context_typ_check key name (simple_check (op =) f);
24.107 +fun add_term_check key name f = context_term_check key name (simple_check (op aconv) f);
24.108 +fun add_typ_uncheck key name f = context_typ_uncheck key name (simple_check (op =) f);
24.109 +fun add_term_uncheck key name f = context_term_uncheck key name (simple_check (op aconv) f);
24.110 +
24.111 +end;
24.112 +
24.113 +
24.114 +local
24.115 +
24.116 +fun check_stage fs = perhaps_loop (perhaps_apply (map uncurry fs));
24.117 +fun check_all fs = perhaps_apply (map check_stage fs);
24.118 +
24.119 +fun check which uncheck ctxt0 xs0 =
24.120 + let
24.121 + val funs = which (Checks.get (Context.Proof ctxt0))
24.122 + |> map_filter (fn ((i, u), fs) => if uncheck = u then SOME (i, map (snd o fst) fs) else NONE)
24.123 + |> Library.sort (int_ord o pairself fst) |> map snd
24.124 + |> not uncheck ? map rev;
24.125 + in #1 (perhaps (check_all funs) (xs0, ctxt0)) end;
24.126 +
24.127 +in
24.128 +
24.129 +val typ_check = check fst false;
24.130 +val term_check = check snd false;
24.131 +val typ_uncheck = check fst true;
24.132 +val term_uncheck = check snd true;
24.133
24.134 val check_typs = operation #check_typs;
24.135 val check_terms = operation #check_terms;
24.136 @@ -300,17 +320,30 @@
24.137 val check_typ = singleton o check_typs;
24.138 val check_term = singleton o check_terms;
24.139 val check_prop = singleton o check_props;
24.140 -val check_sort = map_sort o check_typ;
24.141
24.142 val uncheck_typs = operation #uncheck_typs;
24.143 val uncheck_terms = operation #uncheck_terms;
24.144 +
24.145 +end;
24.146 +
24.147 +
24.148 +(* derived operations for algebra of sorts *)
24.149 +
24.150 +local
24.151 +
24.152 +fun map_sort f S =
24.153 + (case f (TFree ("", S)) of
24.154 + TFree ("", S') => S'
24.155 + | _ => raise TYPE ("map_sort", [TFree ("", S)], []));
24.156 +
24.157 +in
24.158 +
24.159 +val check_sort = map_sort o check_typ;
24.160 val uncheck_sort = map_sort o singleton o uncheck_typs;
24.161
24.162 end;
24.163
24.164
24.165 -(* derived operations for classrel and arity *)
24.166 -
24.167 val uncheck_classrel = map o singleton o uncheck_sort;
24.168
24.169 fun unparse_classrel ctxt cs = Pretty.block (flat
24.170 @@ -590,7 +623,7 @@
24.171 (* basic syntax *)
24.172
24.173 val token_markers =
24.174 - ["_tfree", "_tvar", "_free", "_bound", "_var", "_numeral", "_inner_string"];
24.175 + ["_tfree", "_tvar", "_free", "_bound", "_loose", "_var", "_numeral", "_inner_string"];
24.176
24.177 val basic_nonterms =
24.178 (Lexicon.terminals @ ["logic", "type", "types", "sort", "classes",
25.1 --- a/src/Pure/Syntax/syntax_phases.ML Wed Apr 20 10:14:24 2011 +0200
25.2 +++ b/src/Pure/Syntax/syntax_phases.ML Wed Apr 20 11:21:12 2011 +0200
25.3 @@ -146,7 +146,7 @@
25.4 val c = get_type (Lexicon.str_of_token tok);
25.5 val _ = report (Lexicon.pos_of_token tok) (markup_type ctxt) c;
25.6 in [Ast.Constant (Lexicon.mark_type c)] end
25.7 - | asts_of (Parser.Node ("_constrain_position", [pt as Parser.Tip tok])) =
25.8 + | asts_of (Parser.Node ("_position", [pt as Parser.Tip tok])) =
25.9 if constrain_pos then
25.10 [Ast.Appl [Ast.Constant "_constrain", ast_of pt,
25.11 Ast.Variable (Term_Position.encode (Lexicon.pos_of_token tok))]]
25.12 @@ -464,7 +464,7 @@
25.13 | ast_of (t as _ $ _) =
25.14 let val (f, args) = strip_comb t
25.15 in Ast.mk_appl (ast_of f) (map ast_of args) end
25.16 - | ast_of (Bound i) = Ast.Variable ("B." ^ string_of_int i)
25.17 + | ast_of (Bound i) = Ast.Appl [Ast.Constant "_loose", Ast.Variable ("B." ^ string_of_int i)]
25.18 | ast_of (Abs _) = raise Fail "simple_ast_of: Abs";
25.19 in ast_of end;
25.20
25.21 @@ -610,6 +610,7 @@
25.22 | token_trans "_tvar" x = SOME (Pretty.mark_str (Markup.tvar, x))
25.23 | token_trans "_free" x = SOME (Pretty.marks_str (free_or_skolem ctxt x))
25.24 | token_trans "_bound" x = SOME (Pretty.mark_str (Markup.bound, x))
25.25 + | token_trans "_loose" x = SOME (Pretty.mark_str (Markup.malformed, x))
25.26 | token_trans "_var" x = SOME (Pretty.mark_str (var_or_skolem x))
25.27 | token_trans "_numeral" x = SOME (Pretty.mark_str (Markup.numeral, x))
25.28 | token_trans "_inner_string" x = SOME (Pretty.mark_str (Markup.inner_string, x))
26.1 --- a/src/Pure/Thy/thy_output.ML Wed Apr 20 10:14:24 2011 +0200
26.2 +++ b/src/Pure/Thy/thy_output.ML Wed Apr 20 11:21:12 2011 +0200
26.3 @@ -498,7 +498,7 @@
26.4
26.5 fun pretty_abbrev ctxt s =
26.6 let
26.7 - val t = Syntax.parse_term ctxt s |> singleton (Proof_Context.standard_infer_types ctxt);
26.8 + val t = Syntax.read_term (Proof_Context.set_mode Proof_Context.mode_abbrev ctxt) s;
26.9 fun err () = error ("Abbreviated constant expected: " ^ Syntax.string_of_term ctxt t);
26.10 val (head, args) = Term.strip_comb t;
26.11 val (c, T) = Term.dest_Const head handle TERM _ => err ();
27.1 --- a/src/Pure/codegen.ML Wed Apr 20 10:14:24 2011 +0200
27.2 +++ b/src/Pure/codegen.ML Wed Apr 20 11:21:12 2011 +0200
27.3 @@ -8,7 +8,6 @@
27.4 sig
27.5 val quiet_mode : bool Unsynchronized.ref
27.6 val message : string -> unit
27.7 - val mode : string list Unsynchronized.ref
27.8 val margin : int Unsynchronized.ref
27.9 val string_of : Pretty.T -> string
27.10 val str : string -> Pretty.T
27.11 @@ -31,9 +30,9 @@
27.12 val preprocess: theory -> thm list -> thm list
27.13 val preprocess_term: theory -> term -> term
27.14 val print_codegens: theory -> unit
27.15 - val generate_code: theory -> string list -> string -> (string * string) list ->
27.16 + val generate_code: theory -> string list -> string list -> string -> (string * string) list ->
27.17 (string * string) list * codegr
27.18 - val generate_code_i: theory -> string list -> string -> (string * term) list ->
27.19 + val generate_code_i: theory -> string list -> string list -> string -> (string * term) list ->
27.20 (string * string) list * codegr
27.21 val assoc_const: string * (term mixfix list *
27.22 (string * string) list) -> theory -> theory
27.23 @@ -46,9 +45,9 @@
27.24 val get_assoc_type: theory -> string ->
27.25 (typ mixfix list * (string * string) list) option
27.26 val codegen_error: codegr -> string -> string -> 'a
27.27 - val invoke_codegen: theory -> deftab -> string -> string -> bool ->
27.28 + val invoke_codegen: theory -> string list -> deftab -> string -> string -> bool ->
27.29 term -> codegr -> Pretty.T * codegr
27.30 - val invoke_tycodegen: theory -> deftab -> string -> string -> bool ->
27.31 + val invoke_tycodegen: theory -> string list -> deftab -> string -> string -> bool ->
27.32 typ -> codegr -> Pretty.T * codegr
27.33 val mk_id: string -> string
27.34 val mk_qual_id: string -> string * string -> string
27.35 @@ -62,7 +61,7 @@
27.36 val rename_term: term -> term
27.37 val new_names: term -> string list -> string list
27.38 val new_name: term -> string -> string
27.39 - val if_library: 'a -> 'a -> 'a
27.40 + val if_library: string list -> 'a -> 'a -> 'a
27.41 val get_defn: theory -> deftab -> string -> typ ->
27.42 ((typ * (string * thm)) * int option) option
27.43 val is_instance: typ -> typ -> bool
27.44 @@ -105,8 +104,6 @@
27.45 val quiet_mode = Unsynchronized.ref true;
27.46 fun message s = if !quiet_mode then () else writeln s;
27.47
27.48 -val mode = Unsynchronized.ref ([] : string list); (* FIXME proper functional argument *)
27.49 -
27.50 val margin = Unsynchronized.ref 80;
27.51
27.52 fun string_of p = Print_Mode.setmp [] (Pretty.string_of_margin (!margin)) p;
27.53 @@ -171,13 +168,14 @@
27.54 (* type of code generators *)
27.55
27.56 type 'a codegen =
27.57 - theory -> (* theory in which generate_code was called *)
27.58 - deftab -> (* definition table (for efficiency) *)
27.59 - string -> (* node name of caller (for recording dependencies) *)
27.60 - string -> (* module name of caller (for modular code generation) *)
27.61 - bool -> (* whether to parenthesize generated expression *)
27.62 - 'a -> (* item to generate code from *)
27.63 - codegr -> (* code dependency graph *)
27.64 + theory -> (* theory in which generate_code was called *)
27.65 + string list -> (* mode *)
27.66 + deftab -> (* definition table (for efficiency) *)
27.67 + string -> (* node name of caller (for recording dependencies) *)
27.68 + string -> (* module name of caller (for modular code generation) *)
27.69 + bool -> (* whether to parenthesize generated expression *)
27.70 + 'a -> (* item to generate code from *)
27.71 + codegr -> (* code dependency graph *)
27.72 (Pretty.T * codegr) option;
27.73
27.74
27.75 @@ -478,8 +476,8 @@
27.76 fun get_assoc_code thy (s, T) = Option.map snd (find_first (fn ((s', T'), _) =>
27.77 s = s' andalso is_instance T T') (#consts (CodegenData.get thy)));
27.78
27.79 -fun get_aux_code xs = map_filter (fn (m, code) =>
27.80 - if m = "" orelse member (op =) (!mode) m then SOME code else NONE) xs;
27.81 +fun get_aux_code mode xs = map_filter (fn (m, code) =>
27.82 + if m = "" orelse member (op =) mode m then SOME code else NONE) xs;
27.83
27.84 fun dest_prim_def t =
27.85 let
27.86 @@ -525,14 +523,14 @@
27.87 fun codegen_error (gr, _) dep s =
27.88 error (s ^ "\nrequired by:\n" ^ commas (Graph.all_succs gr [dep]));
27.89
27.90 -fun invoke_codegen thy defs dep module brack t gr = (case get_first
27.91 - (fn (_, f) => f thy defs dep module brack t gr) (#codegens (CodegenData.get thy)) of
27.92 +fun invoke_codegen thy mode defs dep module brack t gr = (case get_first
27.93 + (fn (_, f) => f thy mode defs dep module brack t gr) (#codegens (CodegenData.get thy)) of
27.94 NONE => codegen_error gr dep ("Unable to generate code for term:\n" ^
27.95 Syntax.string_of_term_global thy t)
27.96 | SOME x => x);
27.97
27.98 -fun invoke_tycodegen thy defs dep module brack T gr = (case get_first
27.99 - (fn (_, f) => f thy defs dep module brack T gr ) (#tycodegens (CodegenData.get thy)) of
27.100 +fun invoke_tycodegen thy mode defs dep module brack T gr = (case get_first
27.101 + (fn (_, f) => f thy mode defs dep module brack T gr ) (#tycodegens (CodegenData.get thy)) of
27.102 NONE => codegen_error gr dep ("Unable to generate code for type:\n" ^
27.103 Syntax.string_of_typ_global thy T)
27.104 | SOME x => x);
27.105 @@ -597,17 +595,17 @@
27.106
27.107 fun new_name t x = hd (new_names t [x]);
27.108
27.109 -fun if_library x y = if member (op =) (!mode) "library" then x else y;
27.110 +fun if_library mode x y = if member (op =) mode "library" then x else y;
27.111
27.112 -fun default_codegen thy defs dep module brack t gr =
27.113 +fun default_codegen thy mode defs dep module brack t gr =
27.114 let
27.115 val (u, ts) = strip_comb t;
27.116 - fun codegens brack = fold_map (invoke_codegen thy defs dep module brack)
27.117 + fun codegens brack = fold_map (invoke_codegen thy mode defs dep module brack)
27.118 in (case u of
27.119 Var ((s, i), T) =>
27.120 let
27.121 val (ps, gr') = codegens true ts gr;
27.122 - val (_, gr'') = invoke_tycodegen thy defs dep module false T gr'
27.123 + val (_, gr'') = invoke_tycodegen thy mode defs dep module false T gr'
27.124 in SOME (mk_app brack (str (s ^
27.125 (if i=0 then "" else string_of_int i))) ps, gr'')
27.126 end
27.127 @@ -615,7 +613,7 @@
27.128 | Free (s, T) =>
27.129 let
27.130 val (ps, gr') = codegens true ts gr;
27.131 - val (_, gr'') = invoke_tycodegen thy defs dep module false T gr'
27.132 + val (_, gr'') = invoke_tycodegen thy mode defs dep module false T gr'
27.133 in SOME (mk_app brack (str s) ps, gr'') end
27.134
27.135 | Const (s, T) =>
27.136 @@ -623,26 +621,26 @@
27.137 SOME (ms, aux) =>
27.138 let val i = num_args_of ms
27.139 in if length ts < i then
27.140 - default_codegen thy defs dep module brack (eta_expand u ts i) gr
27.141 + default_codegen thy mode defs dep module brack (eta_expand u ts i) gr
27.142 else
27.143 let
27.144 val (ts1, ts2) = args_of ms ts;
27.145 val (ps1, gr1) = codegens false ts1 gr;
27.146 val (ps2, gr2) = codegens true ts2 gr1;
27.147 val (ps3, gr3) = codegens false (quotes_of ms) gr2;
27.148 - val (_, gr4) = invoke_tycodegen thy defs dep module false
27.149 + val (_, gr4) = invoke_tycodegen thy mode defs dep module false
27.150 (funpow (length ts) (hd o tl o snd o dest_Type) T) gr3;
27.151 val (module', suffix) = (case get_defn thy defs s T of
27.152 - NONE => (if_library (thyname_of_const thy s) module, "")
27.153 + NONE => (if_library mode (thyname_of_const thy s) module, "")
27.154 | SOME ((U, (module', _)), NONE) =>
27.155 - (if_library module' module, "")
27.156 + (if_library mode module' module, "")
27.157 | SOME ((U, (module', _)), SOME i) =>
27.158 - (if_library module' module, " def" ^ string_of_int i));
27.159 + (if_library mode module' module, " def" ^ string_of_int i));
27.160 val node_id = s ^ suffix;
27.161 fun p module' = mk_app brack (Pretty.block
27.162 (pretty_mixfix module module' ms ps1 ps3)) ps2
27.163 in SOME (case try (get_node gr4) node_id of
27.164 - NONE => (case get_aux_code aux of
27.165 + NONE => (case get_aux_code mode aux of
27.166 [] => (p module, gr4)
27.167 | xs => (p module', add_edge (node_id, dep) (new_node
27.168 (node_id, (NONE, module', cat_lines xs ^ "\n")) gr4)))
27.169 @@ -654,7 +652,7 @@
27.170 NONE => NONE
27.171 | SOME ((U, (thyname, thm)), k) => (case prep_prim_def thy thm
27.172 of SOME (_, (_, (args, rhs))) => let
27.173 - val module' = if_library thyname module;
27.174 + val module' = if_library mode thyname module;
27.175 val suffix = (case k of NONE => "" | SOME i => " def" ^ string_of_int i);
27.176 val node_id = s ^ suffix;
27.177 val ((ps, def_id), gr') = gr |> codegens true ts
27.178 @@ -669,12 +667,12 @@
27.179 if not (null args) orelse null Ts then (args, rhs) else
27.180 let val v = Free (new_name rhs "x", hd Ts)
27.181 in ([v], betapply (rhs, v)) end;
27.182 - val (p', gr1) = invoke_codegen thy defs node_id module' false
27.183 + val (p', gr1) = invoke_codegen thy mode defs node_id module' false
27.184 rhs' (add_edge (node_id, dep)
27.185 (new_node (node_id, (NONE, "", "")) gr'));
27.186 val (xs, gr2) = codegens false args' gr1;
27.187 - val (_, gr3) = invoke_tycodegen thy defs dep module false T gr2;
27.188 - val (ty, gr4) = invoke_tycodegen thy defs node_id module' false U gr3;
27.189 + val (_, gr3) = invoke_tycodegen thy mode defs dep module false T gr2;
27.190 + val (ty, gr4) = invoke_tycodegen thy mode defs node_id module' false U gr3;
27.191 in (p, map_node node_id (K (NONE, module', string_of
27.192 (Pretty.block (separate (Pretty.brk 1)
27.193 (if null args' then
27.194 @@ -692,7 +690,7 @@
27.195 val t = strip_abs_body u
27.196 val bs' = new_names t bs;
27.197 val (ps, gr1) = codegens true ts gr;
27.198 - val (p, gr2) = invoke_codegen thy defs dep module false
27.199 + val (p, gr2) = invoke_codegen thy mode defs dep module false
27.200 (subst_bounds (map Free (rev (bs' ~~ Ts)), t)) gr1;
27.201 in
27.202 SOME (mk_app brack (Pretty.block (str "(" :: pretty_fn bs' p @
27.203 @@ -702,26 +700,26 @@
27.204 | _ => NONE)
27.205 end;
27.206
27.207 -fun default_tycodegen thy defs dep module brack (TVar ((s, i), _)) gr =
27.208 +fun default_tycodegen thy mode defs dep module brack (TVar ((s, i), _)) gr =
27.209 SOME (str (s ^ (if i = 0 then "" else string_of_int i)), gr)
27.210 - | default_tycodegen thy defs dep module brack (TFree (s, _)) gr =
27.211 + | default_tycodegen thy mode defs dep module brack (TFree (s, _)) gr =
27.212 SOME (str s, gr)
27.213 - | default_tycodegen thy defs dep module brack (Type (s, Ts)) gr =
27.214 + | default_tycodegen thy mode defs dep module brack (Type (s, Ts)) gr =
27.215 (case AList.lookup (op =) ((#types o CodegenData.get) thy) s of
27.216 NONE => NONE
27.217 | SOME (ms, aux) =>
27.218 let
27.219 val (ps, gr') = fold_map
27.220 - (invoke_tycodegen thy defs dep module false)
27.221 + (invoke_tycodegen thy mode defs dep module false)
27.222 (fst (args_of ms Ts)) gr;
27.223 val (qs, gr'') = fold_map
27.224 - (invoke_tycodegen thy defs dep module false)
27.225 + (invoke_tycodegen thy mode defs dep module false)
27.226 (quotes_of ms) gr';
27.227 - val module' = if_library (thyname_of_type thy s) module;
27.228 + val module' = if_library mode (thyname_of_type thy s) module;
27.229 val node_id = s ^ " (type)";
27.230 fun p module' = Pretty.block (pretty_mixfix module module' ms ps qs)
27.231 in SOME (case try (get_node gr'') node_id of
27.232 - NONE => (case get_aux_code aux of
27.233 + NONE => (case get_aux_code mode aux of
27.234 [] => (p module', gr'')
27.235 | xs => (p module', snd (mk_type_id module' s
27.236 (add_edge (node_id, dep) (new_node (node_id,
27.237 @@ -780,10 +778,10 @@
27.238 else [(module, implode (map (#3 o snd) code))]
27.239 end;
27.240
27.241 -fun gen_generate_code prep_term thy modules module xs =
27.242 +fun gen_generate_code prep_term thy mode modules module xs =
27.243 let
27.244 val _ = (module <> "" orelse
27.245 - member (op =) (!mode) "library" andalso forall (fn (s, _) => s = "") xs)
27.246 + member (op =) mode "library" andalso forall (fn (s, _) => s = "") xs)
27.247 orelse error "missing module name";
27.248 val graphs = get_modules thy;
27.249 val defs = mk_deftab thy;
27.250 @@ -800,7 +798,7 @@
27.251 | expand t = (case fastype_of t of
27.252 Type ("fun", [T, U]) => Abs ("x", T, t $ Bound 0) | _ => t);
27.253 val (ps, gr') = fold_map (fn (s, t) => fn gr => apfst (pair s)
27.254 - (invoke_codegen thy defs "<Top>" module false t gr))
27.255 + (invoke_codegen thy mode defs "<Top>" module false t gr))
27.256 (map (apsnd (expand o preprocess_term thy o prep_term thy)) xs) gr;
27.257 val code = map_filter
27.258 (fn ("", _) => NONE
27.259 @@ -809,12 +807,12 @@
27.260 val code' = space_implode "\n\n" code ^ "\n\n";
27.261 val code'' =
27.262 map_filter (fn (name, s) =>
27.263 - if member (op =) (!mode) "library" andalso name = module andalso null code
27.264 + if member (op =) mode "library" andalso name = module andalso null code
27.265 then NONE
27.266 else SOME (name, mk_struct name s))
27.267 ((if null code then I
27.268 else add_to_module module code')
27.269 - (output_code (fst gr') (if_library "" module) ["<Top>"]))
27.270 + (output_code (fst gr') (if_library mode "" module) ["<Top>"]))
27.271 in
27.272 (code'', del_nodes ["<Top>"] gr')
27.273 end;
27.274 @@ -873,8 +871,7 @@
27.275 fun test_term ctxt t =
27.276 let
27.277 val thy = Proof_Context.theory_of ctxt;
27.278 - val (code, gr) = setmp_CRITICAL mode ["term_of", "test"]
27.279 - (generate_code_i thy [] "Generated") [("testf", t)];
27.280 + val (code, gr) = generate_code_i thy ["term_of", "test"] [] "Generated" [("testf", t)];
27.281 val Ts = map snd (fst (strip_abs t));
27.282 val args = map_index (fn (i, T) => ("arg" ^ string_of_int i, T)) Ts;
27.283 val s = "structure TestTerm =\nstruct\n\n" ^
27.284 @@ -913,9 +910,9 @@
27.285 error "Term to be evaluated contains type variables";
27.286 val _ = (null (Term.add_vars t []) andalso null (Term.add_frees t [])) orelse
27.287 error "Term to be evaluated contains variables";
27.288 - val (code, gr) = setmp_CRITICAL mode ["term_of"]
27.289 - (generate_code_i thy [] "Generated")
27.290 - [("result", Abs ("x", TFree ("'a", []), t))];
27.291 + val (code, gr) =
27.292 + generate_code_i thy ["term_of"] [] "Generated"
27.293 + [("result", Abs ("x", TFree ("'a", []), t))];
27.294 val s = "structure EvalTerm =\nstruct\n\n" ^
27.295 cat_lines (map snd code) ^
27.296 "\nopen Generated;\n\n" ^ string_of
27.297 @@ -988,7 +985,7 @@
27.298 (const, (parse_mixfix (Syntax.read_term_global thy) mfx, aux)))) xs thy)));
27.299
27.300 fun parse_code lib =
27.301 - Scan.optional (Parse.$$$ "(" |-- Parse.enum "," Parse.xname --| Parse.$$$ ")") (!mode) --
27.302 + Scan.optional (Parse.$$$ "(" |-- Parse.enum "," Parse.xname --| Parse.$$$ ")") [] --
27.303 (if lib then Scan.optional Parse.name "" else Parse.name) --
27.304 Scan.option (Parse.$$$ "file" |-- Parse.name) --
27.305 (if lib then Scan.succeed []
27.306 @@ -996,10 +993,10 @@
27.307 Parse.$$$ "contains" --
27.308 ( Scan.repeat1 (Parse.name --| Parse.$$$ "=" -- Parse.term)
27.309 || Scan.repeat1 (Parse.term >> pair "")) >>
27.310 - (fn ((((mode', module), opt_fname), modules), xs) => Toplevel.theory (fn thy =>
27.311 + (fn ((((mode, module), opt_fname), modules), xs) => Toplevel.theory (fn thy =>
27.312 let
27.313 - val mode'' = (if lib then insert (op =) "library" else I) (remove (op =) "library" mode');
27.314 - val (code, gr) = setmp_CRITICAL mode mode'' (generate_code thy modules module) xs;
27.315 + val mode' = (if lib then insert (op =) "library" else I) (remove (op =) "library" mode);
27.316 + val (code, gr) = generate_code thy mode' modules module xs;
27.317 val thy' = thy |> Context.theory_map (ML_Context.exec (fn () =>
27.318 (case opt_fname of
27.319 NONE => ML_Context.eval_text false Position.none (cat_lines (map snd code))
28.1 --- a/src/Pure/library.ML Wed Apr 20 10:14:24 2011 +0200
28.2 +++ b/src/Pure/library.ML Wed Apr 20 11:21:12 2011 +0200
28.3 @@ -93,7 +93,7 @@
28.4 val find_first: ('a -> bool) -> 'a list -> 'a option
28.5 val get_index: ('a -> 'b option) -> 'a list -> (int * 'b) option
28.6 val get_first: ('a -> 'b option) -> 'a list -> 'b option
28.7 - val eq_list: ('a * 'b -> bool) -> 'a list * 'b list -> bool
28.8 + val eq_list: ('a * 'a -> bool) -> 'a list * 'a list -> bool
28.9 val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
28.10 val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
28.11 val fold_rev2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
28.12 @@ -168,7 +168,7 @@
28.13 val inter: ('a * 'b -> bool) -> 'b list -> 'a list -> 'a list
28.14 val merge: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list
28.15 val subset: ('a * 'b -> bool) -> 'a list * 'b list -> bool
28.16 - val eq_set: ('a * 'b -> bool) -> 'a list * 'b list -> bool
28.17 + val eq_set: ('a * 'a -> bool) -> 'a list * 'a list -> bool
28.18 val distinct: ('a * 'a -> bool) -> 'a list -> 'a list
28.19 val duplicates: ('a * 'a -> bool) -> 'a list -> 'a list
28.20 val has_duplicates: ('a * 'a -> bool) -> 'a list -> bool
28.21 @@ -396,10 +396,11 @@
28.22 (* basic list functions *)
28.23
28.24 fun eq_list eq (list1, list2) =
28.25 - let
28.26 - fun eq_lst (x :: xs, y :: ys) = eq (x, y) andalso eq_lst (xs, ys)
28.27 - | eq_lst _ = true;
28.28 - in length list1 = length list2 andalso eq_lst (list1, list2) end;
28.29 + pointer_eq (list1, list2) orelse
28.30 + let
28.31 + fun eq_lst (x :: xs, y :: ys) = eq (x, y) andalso eq_lst (xs, ys)
28.32 + | eq_lst _ = true;
28.33 + in length list1 = length list2 andalso eq_lst (list1, list2) end;
28.34
28.35 fun maps f [] = []
28.36 | maps f (x :: xs) = f x @ maps f xs;
29.1 --- a/src/Pure/pure_thy.ML Wed Apr 20 10:14:24 2011 +0200
29.2 +++ b/src/Pure/pure_thy.ML Wed Apr 20 11:21:12 2011 +0200
29.3 @@ -134,8 +134,8 @@
29.4 ("_struct", typ "index => logic", Mixfix ("\\<struct>_", [1000], 1000)),
29.5 ("_update_name", typ "idt", NoSyn),
29.6 ("_constrainAbs", typ "'a", NoSyn),
29.7 - ("_constrain_position", typ "id => id_position", Delimfix "_"),
29.8 - ("_constrain_position", typ "longid => longid_position", Delimfix "_"),
29.9 + ("_position", typ "id => id_position", Delimfix "_"),
29.10 + ("_position", typ "longid => longid_position", Delimfix "_"),
29.11 ("_type_constraint_", typ "'a", NoSyn),
29.12 ("_context_const", typ "id_position => logic", Delimfix "CONST _"),
29.13 ("_context_const", typ "id_position => aprop", Delimfix "CONST _"),
30.1 --- a/src/Pure/type_infer.ML Wed Apr 20 10:14:24 2011 +0200
30.2 +++ b/src/Pure/type_infer.ML Wed Apr 20 11:21:12 2011 +0200
30.3 @@ -1,13 +1,15 @@
30.4 (* Title: Pure/type_infer.ML
30.5 Author: Stefan Berghofer and Markus Wenzel, TU Muenchen
30.6
30.7 -Representation of type-inference problems. Simple type inference.
30.8 +Basic representation of type-inference problems.
30.9 *)
30.10
30.11 signature TYPE_INFER =
30.12 sig
30.13 val is_param: indexname -> bool
30.14 val is_paramT: typ -> bool
30.15 + val param_maxidx: term -> int -> int
30.16 + val param_maxidx_of: term list -> int
30.17 val param: int -> string * sort -> typ
30.18 val mk_param: int -> sort -> typ
30.19 val anyT: sort -> typ
30.20 @@ -16,10 +18,6 @@
30.21 val deref: typ Vartab.table -> typ -> typ
30.22 val finish: Proof.context -> typ Vartab.table -> typ list * term list -> typ list * term list
30.23 val fixate: Proof.context -> term list -> term list
30.24 - val prepare: Proof.context -> (string -> typ option) -> (string * int -> typ option) ->
30.25 - term list -> int * term list
30.26 - val infer_types: Proof.context -> (string -> typ option) -> (indexname -> typ option) ->
30.27 - term list -> term list
30.28 end;
30.29
30.30 structure Type_Infer: TYPE_INFER =
30.31 @@ -34,6 +32,12 @@
30.32 fun is_paramT (TVar (xi, _)) = is_param xi
30.33 | is_paramT _ = false;
30.34
30.35 +val param_maxidx =
30.36 + (Term.fold_types o Term.fold_atyps)
30.37 + (fn (TVar (xi as (_, i), _)) => if is_param xi then Integer.max i else I | _ => I);
30.38 +
30.39 +fun param_maxidx_of ts = fold param_maxidx ts ~1;
30.40 +
30.41 fun param i (x, S) = TVar (("?" ^ x, i), S);
30.42
30.43 fun mk_param i S = TVar (("?'a", i), S);
30.44 @@ -62,96 +66,6 @@
30.45
30.46
30.47
30.48 -(** prepare types/terms: create inference parameters **)
30.49 -
30.50 -(* prepare_typ *)
30.51 -
30.52 -fun prepare_typ typ params_idx =
30.53 - let
30.54 - val (params', idx) = fold_atyps
30.55 - (fn TVar (xi as (x, _), S) =>
30.56 - (fn ps_idx as (ps, idx) =>
30.57 - if is_param xi andalso not (Vartab.defined ps xi)
30.58 - then (Vartab.update (xi, mk_param idx S) ps, idx + 1) else ps_idx)
30.59 - | _ => I) typ params_idx;
30.60 -
30.61 - fun prepare (T as Type (a, Ts)) idx =
30.62 - if T = dummyT then (mk_param idx [], idx + 1)
30.63 - else
30.64 - let val (Ts', idx') = fold_map prepare Ts idx
30.65 - in (Type (a, Ts'), idx') end
30.66 - | prepare (T as TVar (xi, _)) idx =
30.67 - (case Vartab.lookup params' xi of
30.68 - NONE => T
30.69 - | SOME p => p, idx)
30.70 - | prepare (TFree ("'_dummy_", S)) idx = (mk_param idx S, idx + 1)
30.71 - | prepare (T as TFree _) idx = (T, idx);
30.72 -
30.73 - val (typ', idx') = prepare typ idx;
30.74 - in (typ', (params', idx')) end;
30.75 -
30.76 -
30.77 -(* prepare_term *)
30.78 -
30.79 -fun prepare_term ctxt const_type tm (vparams, params, idx) =
30.80 - let
30.81 - fun add_vparm xi (ps_idx as (ps, idx)) =
30.82 - if not (Vartab.defined ps xi) then
30.83 - (Vartab.update (xi, mk_param idx []) ps, idx + 1)
30.84 - else ps_idx;
30.85 -
30.86 - val (vparams', idx') = fold_aterms
30.87 - (fn Var (_, Type ("_polymorphic_", _)) => I
30.88 - | Var (xi, _) => add_vparm xi
30.89 - | Free (x, _) => add_vparm (x, ~1)
30.90 - | _ => I)
30.91 - tm (vparams, idx);
30.92 - fun var_param xi = the (Vartab.lookup vparams' xi);
30.93 -
30.94 - fun polyT_of T idx = apsnd snd (prepare_typ (paramify_vars T) (Vartab.empty, idx));
30.95 -
30.96 - fun constraint T t ps =
30.97 - if T = dummyT then (t, ps)
30.98 - else
30.99 - let val (T', ps') = prepare_typ T ps
30.100 - in (Type.constraint T' t, ps') end;
30.101 -
30.102 - fun prepare (Const ("_type_constraint_", T) $ t) ps_idx =
30.103 - let
30.104 - fun err () =
30.105 - error ("Malformed internal type constraint: " ^ Syntax.string_of_typ ctxt T);
30.106 - val A = (case T of Type ("fun", [A, B]) => if A = B then A else err () | _ => err ());
30.107 - val (A', ps_idx') = prepare_typ A ps_idx;
30.108 - val (t', ps_idx'') = prepare t ps_idx';
30.109 - in (Const ("_type_constraint_", A' --> A') $ t', ps_idx'') end
30.110 - | prepare (Const (c, T)) (ps, idx) =
30.111 - (case const_type c of
30.112 - SOME U =>
30.113 - let val (U', idx') = polyT_of U idx
30.114 - in constraint T (Const (c, U')) (ps, idx') end
30.115 - | NONE => error ("Undeclared constant: " ^ quote c))
30.116 - | prepare (Var (xi, Type ("_polymorphic_", [T]))) (ps, idx) =
30.117 - let val (T', idx') = polyT_of T idx
30.118 - in (Var (xi, T'), (ps, idx')) end
30.119 - | prepare (Var (xi, T)) ps_idx = constraint T (Var (xi, var_param xi)) ps_idx
30.120 - | prepare (Free (x, T)) ps_idx = constraint T (Free (x, var_param (x, ~1))) ps_idx
30.121 - | prepare (Bound i) ps_idx = (Bound i, ps_idx)
30.122 - | prepare (Abs (x, T, t)) ps_idx =
30.123 - let
30.124 - val (T', ps_idx') = prepare_typ T ps_idx;
30.125 - val (t', ps_idx'') = prepare t ps_idx';
30.126 - in (Abs (x, T', t'), ps_idx'') end
30.127 - | prepare (t $ u) ps_idx =
30.128 - let
30.129 - val (t', ps_idx') = prepare t ps_idx;
30.130 - val (u', ps_idx'') = prepare u ps_idx';
30.131 - in (t' $ u', ps_idx'') end;
30.132 -
30.133 - val (tm', (params', idx'')) = prepare tm (params, idx');
30.134 - in (tm', (vparams', params', idx'')) end;
30.135 -
30.136 -
30.137 -
30.138 (** results **)
30.139
30.140 (* dereferenced views *)
30.141 @@ -160,7 +74,7 @@
30.142 (case Vartab.lookup tye xi of
30.143 NONE => T
30.144 | SOME U => deref tye U)
30.145 - | deref tye T = T;
30.146 + | deref _ T = T;
30.147
30.148 fun add_parms tye T =
30.149 (case deref tye T of
30.150 @@ -211,148 +125,4 @@
30.151 val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) ([], used);
30.152 in (map o map_types) (Term_Subst.instantiateT inst) ts end;
30.153
30.154 -
30.155 -
30.156 -(** order-sorted unification of types **)
30.157 -
30.158 -exception NO_UNIFIER of string * typ Vartab.table;
30.159 -
30.160 -fun unify ctxt =
30.161 - let
30.162 - val thy = Proof_Context.theory_of ctxt;
30.163 - val arity_sorts = Type.arity_sorts (Context.pretty ctxt) (Sign.tsig_of thy);
30.164 -
30.165 -
30.166 - (* adjust sorts of parameters *)
30.167 -
30.168 - fun not_of_sort x S' S =
30.169 - "Variable " ^ x ^ "::" ^ Syntax.string_of_sort ctxt S' ^ " not of sort " ^
30.170 - Syntax.string_of_sort ctxt S;
30.171 -
30.172 - fun meet (_, []) tye_idx = tye_idx
30.173 - | meet (Type (a, Ts), S) (tye_idx as (tye, _)) =
30.174 - meets (Ts, arity_sorts a S handle ERROR msg => raise NO_UNIFIER (msg, tye)) tye_idx
30.175 - | meet (TFree (x, S'), S) (tye_idx as (tye, _)) =
30.176 - if Sign.subsort thy (S', S) then tye_idx
30.177 - else raise NO_UNIFIER (not_of_sort x S' S, tye)
30.178 - | meet (TVar (xi, S'), S) (tye_idx as (tye, idx)) =
30.179 - if Sign.subsort thy (S', S) then tye_idx
30.180 - else if is_param xi then
30.181 - (Vartab.update_new (xi, mk_param idx (Sign.inter_sort thy (S', S))) tye, idx + 1)
30.182 - else raise NO_UNIFIER (not_of_sort (Term.string_of_vname xi) S' S, tye)
30.183 - and meets (T :: Ts, S :: Ss) (tye_idx as (tye, _)) =
30.184 - meets (Ts, Ss) (meet (deref tye T, S) tye_idx)
30.185 - | meets _ tye_idx = tye_idx;
30.186 -
30.187 -
30.188 - (* occurs check and assignment *)
30.189 -
30.190 - fun occurs_check tye xi (TVar (xi', S)) =
30.191 - if xi = xi' then raise NO_UNIFIER ("Occurs check!", tye)
30.192 - else
30.193 - (case Vartab.lookup tye xi' of
30.194 - NONE => ()
30.195 - | SOME T => occurs_check tye xi T)
30.196 - | occurs_check tye xi (Type (_, Ts)) = List.app (occurs_check tye xi) Ts
30.197 - | occurs_check _ _ _ = ();
30.198 -
30.199 - fun assign xi (T as TVar (xi', _)) S env =
30.200 - if xi = xi' then env
30.201 - else env |> meet (T, S) |>> Vartab.update_new (xi, T)
30.202 - | assign xi T S (env as (tye, _)) =
30.203 - (occurs_check tye xi T; env |> meet (T, S) |>> Vartab.update_new (xi, T));
30.204 -
30.205 -
30.206 - (* unification *)
30.207 -
30.208 - fun show_tycon (a, Ts) =
30.209 - quote (Syntax.string_of_typ ctxt (Type (a, replicate (length Ts) dummyT)));
30.210 -
30.211 - fun unif (T1, T2) (env as (tye, _)) =
30.212 - (case pairself (`is_paramT o deref tye) (T1, T2) of
30.213 - ((true, TVar (xi, S)), (_, T)) => assign xi T S env
30.214 - | ((_, T), (true, TVar (xi, S))) => assign xi T S env
30.215 - | ((_, Type (a, Ts)), (_, Type (b, Us))) =>
30.216 - if a <> b then
30.217 - raise NO_UNIFIER
30.218 - ("Clash of types " ^ show_tycon (a, Ts) ^ " and " ^ show_tycon (b, Us), tye)
30.219 - else fold unif (Ts ~~ Us) env
30.220 - | ((_, T), (_, U)) => if T = U then env else raise NO_UNIFIER ("", tye));
30.221 -
30.222 - in unif end;
30.223 -
30.224 -
30.225 -
30.226 -(** simple type inference **)
30.227 -
30.228 -(* infer *)
30.229 -
30.230 -fun infer ctxt =
30.231 - let
30.232 - (* errors *)
30.233 -
30.234 - fun prep_output tye bs ts Ts =
30.235 - let
30.236 - val (Ts_bTs', ts') = finish ctxt tye (Ts @ map snd bs, ts);
30.237 - val (Ts', Ts'') = chop (length Ts) Ts_bTs';
30.238 - fun prep t =
30.239 - let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts'')))
30.240 - in Term.subst_bounds (map Syntax_Trans.mark_boundT xs, t) end;
30.241 - in (map prep ts', Ts') end;
30.242 -
30.243 - fun err_loose i = error ("Loose bound variable: B." ^ string_of_int i);
30.244 -
30.245 - fun unif_failed msg =
30.246 - "Type unification failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n\n";
30.247 -
30.248 - fun err_appl msg tye bs t T u U =
30.249 - let val ([t', u'], [T', U']) = prep_output tye bs [t, u] [T, U]
30.250 - in error (unif_failed msg ^ Type.appl_error ctxt t' T' u' U' ^ "\n") end;
30.251 -
30.252 -
30.253 - (* main *)
30.254 -
30.255 - fun inf _ (Const (_, T)) tye_idx = (T, tye_idx)
30.256 - | inf _ (Free (_, T)) tye_idx = (T, tye_idx)
30.257 - | inf _ (Var (_, T)) tye_idx = (T, tye_idx)
30.258 - | inf bs (Bound i) tye_idx =
30.259 - (snd (nth bs i handle Subscript => err_loose i), tye_idx)
30.260 - | inf bs (Abs (x, T, t)) tye_idx =
30.261 - let val (U, tye_idx') = inf ((x, T) :: bs) t tye_idx
30.262 - in (T --> U, tye_idx') end
30.263 - | inf bs (t $ u) tye_idx =
30.264 - let
30.265 - val (T, tye_idx') = inf bs t tye_idx;
30.266 - val (U, (tye, idx)) = inf bs u tye_idx';
30.267 - val V = mk_param idx [];
30.268 - val tye_idx'' = unify ctxt (U --> V, T) (tye, idx + 1)
30.269 - handle NO_UNIFIER (msg, tye') => err_appl msg tye' bs t T u U;
30.270 - in (V, tye_idx'') end;
30.271 -
30.272 - in inf [] end;
30.273 -
30.274 -
30.275 -(* main interfaces *)
30.276 -
30.277 -fun prepare ctxt const_type var_type raw_ts =
30.278 - let
30.279 - val get_type = the_default dummyT o var_type;
30.280 - val constrain_vars = Term.map_aterms
30.281 - (fn Free (x, T) => Type.constraint T (Free (x, get_type (x, ~1)))
30.282 - | Var (xi, T) => Type.constraint T (Var (xi, get_type xi))
30.283 - | t => t);
30.284 -
30.285 - val ts = burrow_types (Syntax.check_typs ctxt) raw_ts;
30.286 - val (ts', (_, _, idx)) =
30.287 - fold_map (prepare_term ctxt const_type o constrain_vars) ts
30.288 - (Vartab.empty, Vartab.empty, 0);
30.289 - in (idx, ts') end;
30.290 -
30.291 -fun infer_types ctxt const_type var_type raw_ts =
30.292 - let
30.293 - val (idx, ts) = prepare ctxt const_type var_type raw_ts;
30.294 - val (tye, _) = fold (snd oo infer ctxt) ts (Vartab.empty, idx);
30.295 - val (_, ts') = finish ctxt tye ([], ts);
30.296 - in ts' end;
30.297 -
30.298 end;
31.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
31.2 +++ b/src/Pure/type_infer_context.ML Wed Apr 20 11:21:12 2011 +0200
31.3 @@ -0,0 +1,267 @@
31.4 +(* Title: Pure/type_infer_context.ML
31.5 + Author: Stefan Berghofer and Markus Wenzel, TU Muenchen
31.6 +
31.7 +Type-inference preparation and standard type inference.
31.8 +*)
31.9 +
31.10 +signature TYPE_INFER_CONTEXT =
31.11 +sig
31.12 + val const_sorts: bool Config.T
31.13 + val prepare: Proof.context -> term list -> int * term list
31.14 + val infer_types: Proof.context -> term list -> term list
31.15 +end;
31.16 +
31.17 +structure Type_Infer_Context: TYPE_INFER_CONTEXT =
31.18 +struct
31.19 +
31.20 +(** prepare types/terms: create inference parameters **)
31.21 +
31.22 +(* constraints *)
31.23 +
31.24 +val const_sorts = Config.bool (Config.declare "const_sorts" (K (Config.Bool true)));
31.25 +
31.26 +fun const_type ctxt =
31.27 + try ((not (Config.get ctxt const_sorts) ? Type.strip_sorts) o
31.28 + Consts.the_constraint (Proof_Context.consts_of ctxt));
31.29 +
31.30 +fun var_type ctxt = the_default dummyT o Proof_Context.def_type ctxt;
31.31 +
31.32 +
31.33 +(* prepare_typ *)
31.34 +
31.35 +fun prepare_typ typ params_idx =
31.36 + let
31.37 + val (params', idx) = fold_atyps
31.38 + (fn TVar (xi, S) =>
31.39 + (fn ps_idx as (ps, idx) =>
31.40 + if Type_Infer.is_param xi andalso not (Vartab.defined ps xi)
31.41 + then (Vartab.update (xi, Type_Infer.mk_param idx S) ps, idx + 1) else ps_idx)
31.42 + | _ => I) typ params_idx;
31.43 +
31.44 + fun prepare (T as Type (a, Ts)) idx =
31.45 + if T = dummyT then (Type_Infer.mk_param idx [], idx + 1)
31.46 + else
31.47 + let val (Ts', idx') = fold_map prepare Ts idx
31.48 + in (Type (a, Ts'), idx') end
31.49 + | prepare (T as TVar (xi, _)) idx =
31.50 + (case Vartab.lookup params' xi of
31.51 + NONE => T
31.52 + | SOME p => p, idx)
31.53 + | prepare (TFree ("'_dummy_", S)) idx = (Type_Infer.mk_param idx S, idx + 1)
31.54 + | prepare (T as TFree _) idx = (T, idx);
31.55 +
31.56 + val (typ', idx') = prepare typ idx;
31.57 + in (typ', (params', idx')) end;
31.58 +
31.59 +
31.60 +(* prepare_term *)
31.61 +
31.62 +fun prepare_term ctxt tm (vparams, params, idx) =
31.63 + let
31.64 + fun add_vparm xi (ps_idx as (ps, idx)) =
31.65 + if not (Vartab.defined ps xi) then
31.66 + (Vartab.update (xi, Type_Infer.mk_param idx []) ps, idx + 1)
31.67 + else ps_idx;
31.68 +
31.69 + val (vparams', idx') = fold_aterms
31.70 + (fn Var (_, Type ("_polymorphic_", _)) => I
31.71 + | Var (xi, _) => add_vparm xi
31.72 + | Free (x, _) => add_vparm (x, ~1)
31.73 + | _ => I)
31.74 + tm (vparams, idx);
31.75 + fun var_param xi = the (Vartab.lookup vparams' xi);
31.76 +
31.77 + fun polyT_of T idx =
31.78 + apsnd snd (prepare_typ (Type_Infer.paramify_vars T) (Vartab.empty, idx));
31.79 +
31.80 + fun constraint T t ps =
31.81 + if T = dummyT then (t, ps)
31.82 + else
31.83 + let val (T', ps') = prepare_typ T ps
31.84 + in (Type.constraint T' t, ps') end;
31.85 +
31.86 + fun prepare (Const ("_type_constraint_", T) $ t) ps_idx =
31.87 + let
31.88 + fun err () =
31.89 + error ("Malformed internal type constraint: " ^ Syntax.string_of_typ ctxt T);
31.90 + val A = (case T of Type ("fun", [A, B]) => if A = B then A else err () | _ => err ());
31.91 + val (A', ps_idx') = prepare_typ A ps_idx;
31.92 + val (t', ps_idx'') = prepare t ps_idx';
31.93 + in (Const ("_type_constraint_", A' --> A') $ t', ps_idx'') end
31.94 + | prepare (Const (c, T)) (ps, idx) =
31.95 + (case const_type ctxt c of
31.96 + SOME U =>
31.97 + let val (U', idx') = polyT_of U idx
31.98 + in constraint T (Const (c, U')) (ps, idx') end
31.99 + | NONE => error ("Undeclared constant: " ^ quote c))
31.100 + | prepare (Var (xi, Type ("_polymorphic_", [T]))) (ps, idx) =
31.101 + let val (T', idx') = polyT_of T idx
31.102 + in (Var (xi, T'), (ps, idx')) end
31.103 + | prepare (Var (xi, T)) ps_idx = constraint T (Var (xi, var_param xi)) ps_idx
31.104 + | prepare (Free (x, T)) ps_idx = constraint T (Free (x, var_param (x, ~1))) ps_idx
31.105 + | prepare (Bound i) ps_idx = (Bound i, ps_idx)
31.106 + | prepare (Abs (x, T, t)) ps_idx =
31.107 + let
31.108 + val (T', ps_idx') = prepare_typ T ps_idx;
31.109 + val (t', ps_idx'') = prepare t ps_idx';
31.110 + in (Abs (x, T', t'), ps_idx'') end
31.111 + | prepare (t $ u) ps_idx =
31.112 + let
31.113 + val (t', ps_idx') = prepare t ps_idx;
31.114 + val (u', ps_idx'') = prepare u ps_idx';
31.115 + in (t' $ u', ps_idx'') end;
31.116 +
31.117 + val (tm', (params', idx'')) = prepare tm (params, idx');
31.118 + in (tm', (vparams', params', idx'')) end;
31.119 +
31.120 +
31.121 +
31.122 +(** order-sorted unification of types **)
31.123 +
31.124 +exception NO_UNIFIER of string * typ Vartab.table;
31.125 +
31.126 +fun unify ctxt =
31.127 + let
31.128 + val thy = Proof_Context.theory_of ctxt;
31.129 + val arity_sorts = Type.arity_sorts (Context.pretty ctxt) (Sign.tsig_of thy);
31.130 +
31.131 +
31.132 + (* adjust sorts of parameters *)
31.133 +
31.134 + fun not_of_sort x S' S =
31.135 + "Variable " ^ x ^ "::" ^ Syntax.string_of_sort ctxt S' ^ " not of sort " ^
31.136 + Syntax.string_of_sort ctxt S;
31.137 +
31.138 + fun meet (_, []) tye_idx = tye_idx
31.139 + | meet (Type (a, Ts), S) (tye_idx as (tye, _)) =
31.140 + meets (Ts, arity_sorts a S handle ERROR msg => raise NO_UNIFIER (msg, tye)) tye_idx
31.141 + | meet (TFree (x, S'), S) (tye_idx as (tye, _)) =
31.142 + if Sign.subsort thy (S', S) then tye_idx
31.143 + else raise NO_UNIFIER (not_of_sort x S' S, tye)
31.144 + | meet (TVar (xi, S'), S) (tye_idx as (tye, idx)) =
31.145 + if Sign.subsort thy (S', S) then tye_idx
31.146 + else if Type_Infer.is_param xi then
31.147 + (Vartab.update_new
31.148 + (xi, Type_Infer.mk_param idx (Sign.inter_sort thy (S', S))) tye, idx + 1)
31.149 + else raise NO_UNIFIER (not_of_sort (Term.string_of_vname xi) S' S, tye)
31.150 + and meets (T :: Ts, S :: Ss) (tye_idx as (tye, _)) =
31.151 + meets (Ts, Ss) (meet (Type_Infer.deref tye T, S) tye_idx)
31.152 + | meets _ tye_idx = tye_idx;
31.153 +
31.154 +
31.155 + (* occurs check and assignment *)
31.156 +
31.157 + fun occurs_check tye xi (TVar (xi', _)) =
31.158 + if xi = xi' then raise NO_UNIFIER ("Occurs check!", tye)
31.159 + else
31.160 + (case Vartab.lookup tye xi' of
31.161 + NONE => ()
31.162 + | SOME T => occurs_check tye xi T)
31.163 + | occurs_check tye xi (Type (_, Ts)) = List.app (occurs_check tye xi) Ts
31.164 + | occurs_check _ _ _ = ();
31.165 +
31.166 + fun assign xi (T as TVar (xi', _)) S env =
31.167 + if xi = xi' then env
31.168 + else env |> meet (T, S) |>> Vartab.update_new (xi, T)
31.169 + | assign xi T S (env as (tye, _)) =
31.170 + (occurs_check tye xi T; env |> meet (T, S) |>> Vartab.update_new (xi, T));
31.171 +
31.172 +
31.173 + (* unification *)
31.174 +
31.175 + fun show_tycon (a, Ts) =
31.176 + quote (Syntax.string_of_typ ctxt (Type (a, replicate (length Ts) dummyT)));
31.177 +
31.178 + fun unif (T1, T2) (env as (tye, _)) =
31.179 + (case pairself (`Type_Infer.is_paramT o Type_Infer.deref tye) (T1, T2) of
31.180 + ((true, TVar (xi, S)), (_, T)) => assign xi T S env
31.181 + | ((_, T), (true, TVar (xi, S))) => assign xi T S env
31.182 + | ((_, Type (a, Ts)), (_, Type (b, Us))) =>
31.183 + if a <> b then
31.184 + raise NO_UNIFIER
31.185 + ("Clash of types " ^ show_tycon (a, Ts) ^ " and " ^ show_tycon (b, Us), tye)
31.186 + else fold unif (Ts ~~ Us) env
31.187 + | ((_, T), (_, U)) => if T = U then env else raise NO_UNIFIER ("", tye));
31.188 +
31.189 + in unif end;
31.190 +
31.191 +
31.192 +
31.193 +(** simple type inference **)
31.194 +
31.195 +(* infer *)
31.196 +
31.197 +fun infer ctxt =
31.198 + let
31.199 + (* errors *)
31.200 +
31.201 + fun prep_output tye bs ts Ts =
31.202 + let
31.203 + val (Ts_bTs', ts') = Type_Infer.finish ctxt tye (Ts @ map snd bs, ts);
31.204 + val (Ts', Ts'') = chop (length Ts) Ts_bTs';
31.205 + fun prep t =
31.206 + let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts'')))
31.207 + in Term.subst_bounds (map Syntax_Trans.mark_boundT xs, t) end;
31.208 + in (map prep ts', Ts') end;
31.209 +
31.210 + fun err_loose i = error ("Loose bound variable: B." ^ string_of_int i);
31.211 +
31.212 + fun unif_failed msg =
31.213 + "Type unification failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n\n";
31.214 +
31.215 + fun err_appl msg tye bs t T u U =
31.216 + let val ([t', u'], [T', U']) = prep_output tye bs [t, u] [T, U]
31.217 + in error (unif_failed msg ^ Type.appl_error ctxt t' T' u' U' ^ "\n") end;
31.218 +
31.219 +
31.220 + (* main *)
31.221 +
31.222 + fun inf _ (Const (_, T)) tye_idx = (T, tye_idx)
31.223 + | inf _ (Free (_, T)) tye_idx = (T, tye_idx)
31.224 + | inf _ (Var (_, T)) tye_idx = (T, tye_idx)
31.225 + | inf bs (Bound i) tye_idx =
31.226 + (snd (nth bs i handle Subscript => err_loose i), tye_idx)
31.227 + | inf bs (Abs (x, T, t)) tye_idx =
31.228 + let val (U, tye_idx') = inf ((x, T) :: bs) t tye_idx
31.229 + in (T --> U, tye_idx') end
31.230 + | inf bs (t $ u) tye_idx =
31.231 + let
31.232 + val (T, tye_idx') = inf bs t tye_idx;
31.233 + val (U, (tye, idx)) = inf bs u tye_idx';
31.234 + val V = Type_Infer.mk_param idx [];
31.235 + val tye_idx'' = unify ctxt (U --> V, T) (tye, idx + 1)
31.236 + handle NO_UNIFIER (msg, tye') => err_appl msg tye' bs t T u U;
31.237 + in (V, tye_idx'') end;
31.238 +
31.239 + in inf [] end;
31.240 +
31.241 +
31.242 +(* main interfaces *)
31.243 +
31.244 +fun prepare ctxt raw_ts =
31.245 + let
31.246 + val constrain_vars = Term.map_aterms
31.247 + (fn Free (x, T) => Type.constraint T (Free (x, var_type ctxt (x, ~1)))
31.248 + | Var (xi, T) => Type.constraint T (Var (xi, var_type ctxt xi))
31.249 + | t => t);
31.250 +
31.251 + val ts = burrow_types (Syntax.check_typs ctxt) raw_ts;
31.252 + val idx = Type_Infer.param_maxidx_of ts + 1;
31.253 + val (ts', (_, _, idx')) =
31.254 + fold_map (prepare_term ctxt o constrain_vars) ts
31.255 + (Vartab.empty, Vartab.empty, idx);
31.256 + in (idx', ts') end;
31.257 +
31.258 +fun infer_types ctxt raw_ts =
31.259 + let
31.260 + val (idx, ts) = prepare ctxt raw_ts;
31.261 + val (tye, _) = fold (snd oo infer ctxt) ts (Vartab.empty, idx);
31.262 + val (_, ts') = Type_Infer.finish ctxt tye ([], ts);
31.263 + in ts' end;
31.264 +
31.265 +val _ =
31.266 + Context.>>
31.267 + (Syntax.add_term_check 0 "standard"
31.268 + (fn ctxt => infer_types ctxt #> map (Proof_Context.expand_abbrevs ctxt)));
31.269 +
31.270 +end;
32.1 --- a/src/Tools/adhoc_overloading.ML Wed Apr 20 10:14:24 2011 +0200
32.2 +++ b/src/Tools/adhoc_overloading.ML Wed Apr 20 11:21:12 2011 +0200
32.3 @@ -134,8 +134,8 @@
32.4 (* setup *)
32.5
32.6 val setup = Context.theory_map
32.7 - (Syntax.add_term_check 0 "adhoc_overloading" check
32.8 - #> Syntax.add_term_check 1 "adhoc_overloading_unresolved_check" reject_unresolved
32.9 - #> Syntax.add_term_uncheck 0 "adhoc_overloading" uncheck);
32.10 + (Syntax.context_term_check 0 "adhoc_overloading" check
32.11 + #> Syntax.context_term_check 1 "adhoc_overloading_unresolved_check" reject_unresolved
32.12 + #> Syntax.context_term_uncheck 0 "adhoc_overloading" uncheck);
32.13
32.14 end
33.1 --- a/src/Tools/nbe.ML Wed Apr 20 10:14:24 2011 +0200
33.2 +++ b/src/Tools/nbe.ML Wed Apr 20 11:21:12 2011 +0200
33.3 @@ -545,9 +545,9 @@
33.4 val ctxt = Syntax.init_pretty_global thy;
33.5 val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);
33.6 val ty' = typ_of_itype program vs0 ty;
33.7 - fun type_infer t = singleton
33.8 - (Type_Infer.infer_types ctxt (try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE))
33.9 - (Type.constraint ty' t);
33.10 + fun type_infer t =
33.11 + Syntax.check_term (Config.put Type_Infer_Context.const_sorts false ctxt)
33.12 + (Type.constraint ty' t);
33.13 fun check_tvars t =
33.14 if null (Term.add_tvars t []) then t
33.15 else error ("Illegal schematic type variables in normalized term: " ^ string_of_term t);
34.1 --- a/src/Tools/subtyping.ML Wed Apr 20 10:14:24 2011 +0200
34.2 +++ b/src/Tools/subtyping.ML Wed Apr 20 11:21:12 2011 +0200
34.3 @@ -6,13 +6,9 @@
34.4
34.5 signature SUBTYPING =
34.6 sig
34.7 - datatype variance = COVARIANT | CONTRAVARIANT | INVARIANT | INVARIANT_TO of typ;
34.8 val coercion_enabled: bool Config.T
34.9 - val infer_types: Proof.context -> (string -> typ option) -> (indexname -> typ option) ->
34.10 - term list -> term list
34.11 val add_type_map: term -> Context.generic -> Context.generic
34.12 val add_coercion: term -> Context.generic -> Context.generic
34.13 - val gen_coercion: Proof.context -> typ Vartab.table -> (typ * typ) -> term
34.14 val setup: theory -> theory
34.15 end;
34.16
34.17 @@ -520,8 +516,8 @@
34.18 | SOME S =>
34.19 SOME
34.20 (map nameT
34.21 - (filter_out Type_Infer.is_paramT (map (Type_Infer.deref tye) (get_bound G T))),
34.22 - S));
34.23 + (filter_out Type_Infer.is_paramT
34.24 + (map (Type_Infer.deref tye) (get_bound G T))), S));
34.25 val styps_and_sorts = distinct (op =) (map_filter to_fulfil raw_bound);
34.26 val assignment =
34.27 if null bound orelse null not_params then NONE
34.28 @@ -651,7 +647,8 @@
34.29 end
34.30 | insert bs (t $ u) =
34.31 let
34.32 - val (t', Type ("fun", [U, T])) = apsnd (Type_Infer.deref tye) (insert bs t);
34.33 + val (t', Type ("fun", [U, T])) =
34.34 + apsnd (Type_Infer.deref tye) (insert bs t);
34.35 val (u', U') = insert bs u;
34.36 in
34.37 if can (fn TU => strong_unify ctxt TU (tye, 0)) (U, U')
34.38 @@ -666,9 +663,9 @@
34.39
34.40 (** assembling the pipeline **)
34.41
34.42 -fun infer_types ctxt const_type var_type raw_ts =
34.43 +fun coercion_infer_types ctxt raw_ts =
34.44 let
34.45 - val (idx, ts) = Type_Infer.prepare ctxt const_type var_type raw_ts;
34.46 + val (idx, ts) = Type_Infer_Context.prepare ctxt raw_ts;
34.47
34.48 fun inf _ (t as (Const (_, T))) tye_idx = (t, T, tye_idx)
34.49 | inf _ (t as (Free (_, T))) tye_idx = (t, T, tye_idx)
34.50 @@ -714,20 +711,12 @@
34.51
34.52 (* term check *)
34.53
34.54 -fun coercion_infer_types ctxt =
34.55 - infer_types ctxt
34.56 - (try (Consts.the_constraint (Proof_Context.consts_of ctxt)))
34.57 - (Proof_Context.def_type ctxt);
34.58 -
34.59 -val (coercion_enabled, coercion_enabled_setup) = Attrib.config_bool "coercion_enabled" (K false);
34.60 +val (coercion_enabled, coercion_enabled_setup) =
34.61 + Attrib.config_bool "coercion_enabled" (K false);
34.62
34.63 val add_term_check =
34.64 Syntax.add_term_check ~100 "coercions"
34.65 - (fn xs => fn ctxt =>
34.66 - if Config.get ctxt coercion_enabled then
34.67 - let val xs' = coercion_infer_types ctxt xs
34.68 - in if eq_list (op aconv) (xs, xs') then NONE else SOME (xs', ctxt) end
34.69 - else NONE);
34.70 + (fn ctxt => Config.get ctxt coercion_enabled ? coercion_infer_types ctxt);
34.71
34.72
34.73 (* declarations *)