Commit Graph

305 Commits (893a3bed368fb8faee0c2e8c07200e684a6237b9)

Author SHA1 Message Date
Jacques Garrigue a3aad303be do not fail when injectivity not proved in Pattern mode, use mcomp
git-svn-id: http://caml.inria.fr/svn/ocaml/trunk@11286 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2011-11-25 02:37:57 +00:00
Jacques Garrigue 6c78f42d36 merge branches/gadts-devel
git-svn-id: http://caml.inria.fr/svn/ocaml/trunk@11284 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2011-11-24 09:02:48 +00:00
Jacques Garrigue b1f8048f39 merge branches/located_errors
git-svn-id: http://caml.inria.fr/svn/ocaml/trunk@11228 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2011-10-21 03:26:35 +00:00
Jacques Garrigue 156fff1b8a Keep type variable names
git-svn-id: http://caml.inria.fr/svn/ocaml/trunk@11210 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2011-09-22 09:05:42 +00:00
Jacques Garrigue 9dc661c3bf merge branches/gadts
git-svn-id: http://caml.inria.fr/svn/ocaml/trunk@11160 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2011-07-29 10:32:43 +00:00
Jacques Garrigue 173c44001c finish fixing PR#5322
git-svn-id: http://caml.inria.fr/svn/ocaml/trunk@11158 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2011-07-29 01:44:00 +00:00
Damien Doligez 3b507dd1aa renaming of Objective Caml to OCaml and cleanup of copyright headers
git-svn-id: http://caml.inria.fr/svn/ocaml/trunk@11156 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2011-07-27 14:17:02 +00:00
Jacques Garrigue b7b719f6f0 fix bug reported by Polux Moon on 2011-07-26
git-svn-id: http://caml.inria.fr/svn/ocaml/trunk@11151 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2011-07-27 08:48:22 +00:00
Damien Doligez c91db736b1 merge changes from 3.12.0 to 3.12.1
git-svn-id: http://caml.inria.fr/svn/ocaml/trunk@11123 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2011-07-20 09:17:07 +00:00
Jacques Garrigue fab07a66c6 do not use unify_pat_types_gadts for normal constructors!
git-svn-id: http://caml.inria.fr/svn/ocaml/branches/gadts@11087 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2011-06-14 09:41:21 +00:00
Jacques Garrigue f70dbeb1b8 fix problem with constraints outside of matching, see typing-gadts/test.ml
git-svn-id: http://caml.inria.fr/svn/ocaml/branches/gadts@11068 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2011-06-05 15:00:04 +00:00
Jacques Garrigue ea15141d8a * make -principal stricter for gadts
* may also change behaviour without -principal
* propagate type constraints in let expressions to patterns


git-svn-id: http://caml.inria.fr/svn/ocaml/branches/gadts@11011 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2011-04-19 02:13:52 +00:00
Jacques Garrigue 04968cc2e6 fix principality by expanding local definitions when exporting a value
git-svn-id: http://caml.inria.fr/svn/ocaml/branches/gadts@10979 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2011-03-10 06:27:24 +00:00
Jacques Garrigue e88a3e9482 allow existentials in "as" patterns + report escaping newtypes + clean-up
git-svn-id: http://caml.inria.fr/svn/ocaml/branches/gadts@10901 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2010-12-14 06:33:06 +00:00
Jacques Garrigue 625ff1c969 make it work with omega07.ml
git-svn-id: http://caml.inria.fr/svn/ocaml/branches/gadts@10896 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2010-12-14 01:38:37 +00:00
Jacques Garrigue 052c8f93d1 fix some bugs found with omega07.ml
git-svn-id: http://caml.inria.fr/svn/ocaml/branches/gadts@10895 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2010-12-14 00:53:47 +00:00
Jacques Garrigue dd5535cfe6 pattern level is only for definitions + existentials too should use pattern level
git-svn-id: http://caml.inria.fr/svn/ocaml/branches/gadts@10891 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2010-12-13 02:59:58 +00:00
Jacques Le Normand 89f3b70c5e newtypes now have an explicit level
git-svn-id: http://caml.inria.fr/svn/ocaml/branches/gadts@10884 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2010-12-03 19:52:36 +00:00
Jacques Le Normand 981758ea76 existentials can no longer appear in let bindings. This is a temporary restriction until we add gadt support to type_let
git-svn-id: http://caml.inria.fr/svn/ocaml/branches/gadts@10882 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2010-12-03 16:13:01 +00:00
Jacques Le Normand d77b95fc56 fixed update_level bug
git-svn-id: http://caml.inria.fr/svn/ocaml/branches/gadts@10878 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2010-12-03 00:59:36 +00:00
Jacques Le Normand b623cdcf67 fixed duplicate error message bug
git-svn-id: http://caml.inria.fr/svn/ocaml/branches/gadts@10851 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2010-11-24 12:50:18 +00:00
Jacques Le Normand 9a97dd50c9 small cleanup
git-svn-id: http://caml.inria.fr/svn/ocaml/branches/gadts@10816 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2010-11-18 06:23:00 +00:00
Jacques Garrigue 800af0cf42 fix mcomp + untabify
git-svn-id: http://caml.inria.fr/svn/ocaml/branches/gadts@10813 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2010-11-17 09:00:58 +00:00
Jacques Le Normand 9713744542 undid changes in last commit. unify now uses the old mode when possible
git-svn-id: http://caml.inria.fr/svn/ocaml/branches/gadts@10812 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2010-11-17 08:14:00 +00:00
Jacques Le Normand 460226317d every function exported by ctype is now set to the correct mode
git-svn-id: http://caml.inria.fr/svn/ocaml/branches/gadts@10811 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2010-11-17 07:41:18 +00:00
Jacques Garrigue 8d643fc12d switch to Old in moregen too
git-svn-id: http://caml.inria.fr/svn/ocaml/branches/gadts@10807 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2010-11-16 06:46:34 +00:00
Jacques Le Normand 91a6a7c8b0 added change_mode function
git-svn-id: http://caml.inria.fr/svn/ocaml/branches/gadts@10806 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2010-11-16 06:35:29 +00:00
Jacques Le Normand 180d03ae93 big change as to how unification mode is handled
git-svn-id: http://caml.inria.fr/svn/ocaml/branches/gadts@10804 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2010-11-15 09:26:28 +00:00
Jacques Le Normand ac4fa5ae13 we must forget abbrevs when switching to the old method of unification. removed unify_old: unify now decides for itself whether to use the old or the new method
git-svn-id: http://caml.inria.fr/svn/ocaml/branches/gadts@10803 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2010-11-15 08:02:17 +00:00
Jacques Garrigue e9127a1d27 fix principality
git-svn-id: http://caml.inria.fr/svn/ocaml/branches/gadts@10789 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2010-11-11 05:42:14 +00:00
Jacques Le Normand 1680403fb9 clean up
git-svn-id: http://caml.inria.fr/svn/ocaml/branches/gadts@10784 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2010-11-10 06:01:27 +00:00
Jacques Le Normand 567c7e395b cleaned up ctype
git-svn-id: http://caml.inria.fr/svn/ocaml/branches/gadts@10781 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2010-11-09 08:41:54 +00:00
Jacques Le Normand e494cfa4c4 small cleanup in unify
git-svn-id: http://caml.inria.fr/svn/ocaml/branches/gadts@10777 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2010-11-09 06:49:21 +00:00
Jacques Garrigue 1bcd80bdf9 principality
git-svn-id: http://caml.inria.fr/svn/ocaml/branches/gadts@10775 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2010-11-09 06:23:53 +00:00
Jacques Garrigue f368f4e0d5 allow variance in GADTs
git-svn-id: http://caml.inria.fr/svn/ocaml/branches/gadts@10763 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2010-11-08 06:59:46 +00:00
Jacques Le Normand 916a46a4ad improved principal
git-svn-id: http://caml.inria.fr/svn/ocaml/branches/gadts@10760 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2010-11-05 04:15:22 +00:00
Jacques Le Normand 5244860f3f local_constraint flag now works
git-svn-id: http://caml.inria.fr/svn/ocaml/branches/gadts@10756 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2010-11-01 07:10:37 +00:00
Jacques Le Normand 6fd8a9a590 using old unification when there are no local constraints
git-svn-id: http://caml.inria.fr/svn/ocaml/branches/gadts@10755 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2010-11-01 05:33:29 +00:00
Jacques Le Normand 6f151a0f95 environment local constraint marker
git-svn-id: http://caml.inria.fr/svn/ocaml/branches/gadts@10754 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2010-11-01 05:09:36 +00:00
Jacques Le Normand 6a384f2536 fixed bug in mcomp and made it more refined
git-svn-id: http://caml.inria.fr/svn/ocaml/branches/gadts@10752 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2010-10-29 08:23:33 +00:00
Jacques Le Normand 3aa828735d existentials now created at the pattern level
git-svn-id: http://caml.inria.fr/svn/ocaml/branches/gadts@10751 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2010-10-29 06:54:24 +00:00
Jacques Le Normand c6f6312d36 fixed bug in unification
git-svn-id: http://caml.inria.fr/svn/ocaml/branches/gadts@10749 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2010-10-28 04:16:10 +00:00
Jacques Le Normand f75820792d mcomp is now smarter
git-svn-id: http://caml.inria.fr/svn/ocaml/branches/gadts@10748 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2010-10-27 11:16:21 +00:00
Jacques Le Normand fad8e4de6f fixed bug in exhaustiveness check
git-svn-id: http://caml.inria.fr/svn/ocaml/branches/gadts@10747 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2010-10-27 09:52:38 +00:00
Jacques Le Normand 4c86d56280 fixed bug
git-svn-id: http://caml.inria.fr/svn/ocaml/branches/gadts@10746 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2010-10-27 09:08:14 +00:00
Jacques Garrigue 7b77119b04 partial instances
git-svn-id: http://caml.inria.fr/svn/ocaml/branches/gadts@10745 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2010-10-27 08:04:14 +00:00
Jacques Le Normand 7f2fa29cf9 local unification now goes from oldest newtype to newest newtype; in practice this has little effect. Cleaned up unification a little
git-svn-id: http://caml.inria.fr/svn/ocaml/branches/gadts@10744 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2010-10-26 04:34:09 +00:00
Jacques Le Normand c2777a43d0 merged with trunk. specifically, merged with implicit unpack patch
git-svn-id: http://caml.inria.fr/svn/ocaml/branches/gadts@10742 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2010-10-25 08:19:48 +00:00
Jacques Le Normand 43ffa5d997 fixed recursive local constraints bug
git-svn-id: http://caml.inria.fr/svn/ocaml/branches/gadts@10741 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2010-10-25 06:37:29 +00:00
Jacques Le Normand a82f06e4c7 added recursive check for local constraint
git-svn-id: http://caml.inria.fr/svn/ocaml/branches/gadts@10740 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
2010-10-25 05:25:33 +00:00