summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | blanchet |

Thu, 05 Dec 2013 13:22:00 +0100 | |

changeset 54632 | 7a14f831d02d |

parent 54631 | da88a625cce1 |

child 54633 | 86e0b402994c |

make sure acyclicity axiom gets generated in the case where the problem involves mutually recursive datatypes

NEWS | file | annotate | diff | comparison | revisions | |

src/HOL/Tools/Nitpick/nitpick_kodkod.ML | file | annotate | diff | comparison | revisions |

--- a/NEWS Thu Dec 05 09:23:59 2013 +0100 +++ b/NEWS Thu Dec 05 13:22:00 2013 +0100 @@ -520,6 +520,10 @@ sets ~> set IMCOMPATIBILITY. +* Nitpick: + - Fixed soundness bug whereby mutually recursive datatypes could take + infinite values. + *** ML ***

--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Dec 05 09:23:59 2013 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Dec 05 13:22:00 2013 +0100 @@ -1545,16 +1545,16 @@ |> Typ_Graph.strong_conn |> map (fn keys => filter (member (op =) keys o fst) nfa) -fun acyclicity_axiom_for_datatype (kk as {kk_no, kk_intersect, ...}) nfa - start_T = - kk_no (kk_intersect - (loop_path_rel_expr kk nfa (pull start_T (map fst nfa)) start_T) - KK.Iden) (* Cycle breaking in the bounds takes care of singly recursive datatypes, hence the first equation. *) -fun acyclicity_axioms_for_datatypes _ [_] = [] - | acyclicity_axioms_for_datatypes kk nfas = - maps (fn nfa => map (acyclicity_axiom_for_datatype kk nfa o fst) nfa) nfas +fun acyclicity_axioms_for_datatype _ [_] _ = [] + | acyclicity_axioms_for_datatype (kk as {kk_no, kk_intersect, ...}) nfa + start_T = + [kk_no (kk_intersect + (loop_path_rel_expr kk nfa (pull start_T (map fst nfa)) start_T) + KK.Iden)] +fun acyclicity_axioms_for_datatypes kk = + maps (fn nfa => maps (acyclicity_axioms_for_datatype kk nfa o fst) nfa) fun atom_equation_for_nut ofs kk (u, j) = let val dummy_u = RelReg (0, type_of u, rep_of u) in