coq - The formal proof system

Age	Commit message (Collapse)	Author
2021-03-13	Minimize the set of multiple inheritance paths to check for conversion	Kazuhiko Sakaguchi
	The table of coercion classes (`class_tab`) has been extended with information about reachability. The conversion checking of a pair of multiple inheritance paths (of coercions) will be skipped if these paths can be reduced to smaller adjoining pairs of multiple inheritance paths, and this reduction will be determined based on that reachability information.
2021-03-09	Replace cl_index with cl_typ in coercionops.ml	Kazuhiko Sakaguchi
	The table of coercion classes `class_tab` is now indexed by `cl_typ` instead of integers (`cl_index`). All the uses of `cl_index` and `Bijint` have been replaced with `cl_typ` and `ClTypMap` respectively.
2019-12-20	Coherence checking for coercions	Kazuhiko Sakaguchi
	This change improves the relaxed ambiguous path condition of coercions (#9743) to check that any circular inheritance path of `C >-> C` is definitionally equal to the identity function of the class `C`. Moreover, for a new inheritance path `p : C >-> D` and existing (valid) one `q : C >-> D`, the new mechanism does not report the ambiguity of `p` and `q` if they have a common element, that is to say: `p = p1 @ [c] @ p2` and `q = q1 @ [c] @ q2` for some coercion `c` and inheritance paths `p1`, `p2`, `q1`, and `q2`. In that case, convertibility of `p1` and `q1`, also, `p2` and `q2` should be checked; thus, checking the ambiguity of `p` and `q` is redundant with them. If the new mechanism does not report any ambiguous path, the inheritance graph must be coherent [Barthe 1995, Sect. 3.2] [Saïbi 1997, Sect. 7]: 1. for any circular path `p : C >-> C`, `p` is definitionally equal to the identity function, and 2. for any two paths `p, q : C >-> D`, `p` and `q` are convertible. [Barthe 1995] Gilles Barthe, Implicit coercions in type systems, In: TYPES '95, LNCS, vol 1158, Springer, 1996, pp 1-15. [Saïbi 1997] Amokrane Saïbi, Typing algorithm in type theory with inheritance, In: POPL '97, ACM, 1997, pp 292-301.
2019-07-02	Improve the ambiguous paths warning to indicate which path is ambiguous with ↵	Kazuhiko Sakaguchi
	new one
2019-03-14	Relax the ambiguous path condition of coercion	Kazuhiko Sakaguchi
	The `Coercion` command did report many ambiguous paths when one declared multiple inheritances. This change makes the `Coercion` command to do not report them when 1. all the coercion in the potentially ambiguous paths respect the uniform inheritance condition and 2. functional compositions of the potentially ambiguous paths are convertible to each other. The first condition is not explicitly checked but is used to make the checking process of the second condition easy. The key idea of this change: Let us consider a sequence of coercion f_1 : C_1 >-> C_2, f_2 : C_2 >-> C_3, ..., f_n : C_n >-> C_(n+1) which respect the uniform inheritance condition and where the user-defined classes C_i have m_i parameters respectively (i <= n). The functional composition f_1 . ... . f_n can be expressed as follows: (fun x_1 ... x_(m_1) y => f_n _ ... _ (* m_n times repetition of holes ) (... (f_2 _ ... _ ( m_2 times repetition of holes *) (f_1 x_1 ... x_(m_1) y))...)), and the contents of all the holes can be determined (inferred) without leaving any existential variables in them thanks to the uniform inheritance condition. Misc: - A test case for this change: test-suite/output/relaxed_ambiguous_paths.v - Turn the ambiguous paths messages into warnings to do output test.