Ekdohibs
/
ocaml
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
ocaml/typing
History
Gabriel Scherer e0b000527b format+gadts: make format types "relational" to fix %(...%) typing 
See the long comment in pervasives.ml for an explanation of the
change. The short summary is that we need to prove more elaborate
properties between the format types involved in the typing of %(...%),
and that proving things by writing GADT functions in OCaml reveals
that Coq's Ltac is a miracle of usability.

Proofs on OCaml GADTs are runtime functions that do have a runtime
semantics: it is legitimate to hope that those proof computations are
as simple as possible, but the current implementation was optimized
for feasability, not simplicity. François Bobot has some interesting
suggestions to simplify the reasoning part (with more equality
reasoning where I used transitivity and symmetry of the
relation profusely), which may make the code simpler in the future
(and possibly more efficient: the hope is that only %(...%) users will
pay a proof-related cost).

git-svn-id: http://caml.inria.fr/svn/ocaml/trunk@14897 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
 		2014-05-21 13:23:13 +00:00
..
annot.mli remove all $Id keywords 2012-10-15 17:50:56 +00:00
btype.ml PR#5584: merge open extensible types, extension-patch-4.0.2 2014-05-04 23:08:45 +00:00
btype.mli PR#5584: merge open extensible types, extension-patch-4.0.2 2014-05-04 23:08:45 +00:00
cmi_format.ml re-commit Leo's weak-dependencies pull request 2014-05-07 00:34:20 +00:00
cmi_format.mli re-commit Leo's weak-dependencies pull request 2014-05-07 00:34:20 +00:00
cmt_format.ml re-commit Leo's weak-dependencies pull request 2014-05-07 00:34:20 +00:00
cmt_format.mli re-commit Leo's weak-dependencies pull request 2014-05-07 00:34:20 +00:00
ctype.ml comment out Ctype.local_non_recursive_abbrev 2014-05-11 07:48:55 +00:00
ctype.mli PR#5584: merge open extensible types, extension-patch-4.0.2 2014-05-04 23:08:45 +00:00
datarepr.ml PR#5584: merge open extensible types, extension-patch-4.0.2 2014-05-04 23:08:45 +00:00
datarepr.mli PR#5584: merge open extensible types, extension-patch-4.0.2 2014-05-04 23:08:45 +00:00
env.ml avoid warning just before an error happens using -no-alias-deps 2014-05-12 12:42:15 +00:00
env.mli * split Typetexp.lookup_module and Typetexp.find_module 2014-05-12 12:02:26 +00:00
envaux.ml PR#5584: merge open extensible types, extension-patch-4.0.2 2014-05-04 23:08:45 +00:00
envaux.mli remove all $Id keywords 2012-10-15 17:50:56 +00:00
ident.ml Folllowup to PR#6359, great cleanup of switch actions sharing. 2014-04-07 15:43:20 +00:00
ident.mli Folllowup to PR#6359, great cleanup of switch actions sharing. 2014-04-07 15:43:20 +00:00
includeclass.ml Rename Pcty_fun to Pcty_arrow (and idem in Types, Typedtree, Outcometree) to be coherent with Ptyp_arrow. 2013-04-16 08:59:09 +00:00
includeclass.mli remove all $Id keywords 2012-10-15 17:50:56 +00:00
includecore.ml PR#5584: merge open extensible types, extension-patch-4.0.2 2014-05-04 23:08:45 +00:00
includecore.mli PR#5584: merge open extensible types, extension-patch-4.0.2 2014-05-04 23:08:45 +00:00
includemod.ml PR#5584: merge open extensible types, extension-patch-4.0.2 2014-05-04 23:08:45 +00:00
includemod.mli PR#5584: merge open extensible types, extension-patch-4.0.2 2014-05-04 23:08:45 +00:00
mtype.ml PR#5584: merge open extensible types, extension-patch-4.0.2 2014-05-04 23:08:45 +00:00
mtype.mli Fix PR#6307 2014-03-10 02:54:02 +00:00
oprint.ml PR#5584: merge open extensible types, extension-patch-4.0.2 2014-05-04 23:08:45 +00:00
oprint.mli PR#5584: merge open extensible types, extension-patch-4.0.2 2014-05-04 23:08:45 +00:00
outcometree.mli PR#5584: merge open extensible types, extension-patch-4.0.2 2014-05-04 23:08:45 +00:00
parmatch.ml apply patch for PR#6420: Bad error message for non-exhaustive matching on extensible types 2014-05-14 04:05:21 +00:00
parmatch.mli Synchronize with trunk. 2013-07-16 13:34:30 +00:00
path.ml remove all $Id keywords 2012-10-15 17:50:56 +00:00
path.mli remove all $Id keywords 2012-10-15 17:50:56 +00:00
predef.ml first part of Benoît Vaugon's format-gadts patch 2014-05-12 15:37:29 +00:00
predef.mli first part of Benoît Vaugon's format-gadts patch 2014-05-12 15:37:29 +00:00
primitive.ml remove all $Id keywords 2012-10-15 17:50:56 +00:00
primitive.mli remove all $Id keywords 2012-10-15 17:50:56 +00:00
printtyp.ml PR#5584: merge open extensible types, extension-patch-4.0.2 2014-05-04 23:08:45 +00:00
printtyp.mli PR#5584: merge open extensible types, extension-patch-4.0.2 2014-05-04 23:08:45 +00:00
printtyped.ml Minor tweak to raw dump of parsetree/typedtree. 2014-05-07 11:14:57 +00:00
printtyped.mli Merge branch 4.01 from branching point to 4.01.0+rc1 2013-09-04 15:12:37 +00:00
stypes.ml Merge branch 4.01 from branching point to 4.01.0+rc1 2013-09-04 15:12:37 +00:00
stypes.mli remove all $Id keywords 2012-10-15 17:50:56 +00:00
subst.ml PR#5584: merge open extensible types, extension-patch-4.0.2 2014-05-04 23:08:45 +00:00
subst.mli PR#5584: merge open extensible types, extension-patch-4.0.2 2014-05-04 23:08:45 +00:00
typeclass.ml #6399: protocol (based on a built-in ocaml.error extension node) to let ppx tools send located errors to be reported by the compiler (patch by Peter Zotov). 2014-05-07 08:26:17 +00:00
typeclass.mli #6399: protocol (based on a built-in ocaml.error extension node) to let ppx tools send located errors to be reported by the compiler (patch by Peter Zotov). 2014-05-07 08:26:17 +00:00
typecore.ml format+gadts: make format types "relational" to fix %(...%) typing 2014-05-21 13:23:13 +00:00
typecore.mli first part of Benoît Vaugon's format-gadts patch 2014-05-12 15:37:29 +00:00
typedecl.ml PR#5584: merge open extensible types, extension-patch-4.0.2 2014-05-04 23:08:45 +00:00
typedecl.mli PR#5584: merge open extensible types, extension-patch-4.0.2 2014-05-04 23:08:45 +00:00
typedtree.ml #6318: Extend match...with with exception cases. (Patch by Jeremy Yallop, backend part by A. Frisch). 2014-05-05 11:49:37 +00:00
typedtree.mli #6318: Extend match...with with exception cases. (Patch by Jeremy Yallop, backend part by A. Frisch). 2014-05-05 11:49:37 +00:00
typedtreeIter.ml #6318: Extend match...with with exception cases. (Patch by Jeremy Yallop, backend part by A. Frisch). 2014-05-05 11:49:37 +00:00
typedtreeIter.mli PR#5584: merge open extensible types, extension-patch-4.0.2 2014-05-04 23:08:45 +00:00
typedtreeMap.ml #6318: Extend match...with with exception cases. (Patch by Jeremy Yallop, backend part by A. Frisch). 2014-05-05 11:49:37 +00:00
typedtreeMap.mli PR#5584: merge open extensible types, extension-patch-4.0.2 2014-05-04 23:08:45 +00:00
typemod.ml avoid warning just before an error happens using -no-alias-deps 2014-05-12 12:42:15 +00:00
typemod.mli * split Typetexp.lookup_module and Typetexp.find_module 2014-05-12 12:02:26 +00:00
types.ml PR#5584: merge open extensible types, extension-patch-4.0.2 2014-05-04 23:08:45 +00:00
types.mli PR#5584: merge open extensible types, extension-patch-4.0.2 2014-05-04 23:08:45 +00:00
typetexp.ml avoid warning just before an error happens using -no-alias-deps 2014-05-12 12:42:15 +00:00
typetexp.mli avoid warning just before an error happens using -no-alias-deps 2014-05-12 12:42:15 +00:00