Stefan pushed to branch master at Stefan / Typer
Commits: 966db6ac by n3f4s at 2016-06-10T21:30:58+02:00 add unification file
contains unify function and subustitution and constraints types
- - - - - 4d57b203 by n3f4s at 2016-06-10T21:32:31+02:00 add metavar to lexp
- - - - - ea777b41 by n3f4s at 2016-06-13T21:11:07+02:00 add unify_imm, add_substition and documentation
add unifyer for Imm (unify_imm), function for creating a metavar and adding a subsitution for that metavar and a lexp
- - - - - dcacfcfe by n3f4s at 2016-06-13T22:47:09+02:00 add unifier for imm and builtin
- - - - - 32a56ef6 by n3f4s at 2016-06-13T22:52:18+02:00 Use same unifier for (L, _) and (_, L)
- - - - - 44dc7a89 by n3f4s at 2016-06-13T23:28:52+02:00 better documentation
- - - - - 234cb197 by n3f4s at 2016-06-13T23:30:13+02:00 add unifier for let
- - - - - e8028bd9 by n3f4s at 2016-06-14T17:51:02+02:00 better doc and remove Node case of _unify_imm
- - - - - 8e2ad6b1 by n3f4s at 2016-06-14T17:51:32+02:00 add begining of _unify_var
- - - - - c9640b0a by n3f4s at 2016-06-14T18:44:14+02:00 update doc and refactoring
change parameter name for readability
- - - - - 42b80743 by n3f4s at 2016-06-14T18:45:15+02:00 add begining of unifier for Arrow
- - - - - 694e12b8 by n3f4s at 2016-06-14T18:45:35+02:00 add find_or_none: map.key -> map -> map.val option
- - - - - ed79848a by n3f4s at 2016-06-14T22:28:02+02:00 reformating, add missing bracket, debug some fun
_unify_imm -> missing parenthesis in match case find_or_none -> search use rigth type of key simplified _unify_arrow by splitting into smaller function
- - - - - 699cd9c7 by n3f4s at 2016-06-14T22:33:27+02:00 add .merlin file in .gitignore
- - - - - ed44b6ac by n3f4s at 2016-06-14T22:59:23+02:00 add substitution parameter to _unify_inner_arrow
- - - - - 7e92651e by n3f4s at 2016-06-15T21:14:08+02:00 add functions, better doc, reformating
add associate and _unify_metavar function update function's doc and unfication documentation
- - - - - 277976a0 by n3f4s at 2016-06-15T22:48:41+02:00 better documentation
- - - - - 3e11606b by n3f4s at 2016-06-15T22:49:30+02:00 add _unify_lambda
- - - - - 3145d351 by n3f4s at 2016-06-15T22:49:48+02:00 debug _unify_inner_arrow & _unify_arrow
_debug_inner_arrow -> change parameter order _unify_arrow -> add arrow to subst instead of subpart of arrow
- - - - - 06078742 by n3f4s at 2016-06-15T22:53:22+02:00 add right object to subst
- - - - - 0a6fd521 by n3f4s at 2016-06-16T16:10:09+02:00 add unification rule _unify_lambda
- - - - - 19805d1e by n3f4s at 2016-06-16T17:24:15+02:00 substitution : VMap.t -> (VMap.t, int)
change type of subsitituion from VMap.t to (VMap.t, int) where the int correspond to the max of the keys. Avoid iteratring over the map for Metavar generation
- - - - - 21b9691a by n3f4s at 2016-06-16T17:34:58+02:00 optimisation based on metavar generation
- - - - - 526c0adf by n3f4s at 2016-06-16T17:42:01+02:00 debug _unify_builtin returns
_unfiy_buitlin returns substitution with between a metavar and a Builtin instea of between a metavar and Builtin body
- - - - - 66a98dfe by n3f4s at 2016-06-16T18:17:54+02:00 dispatch to _unify_* emulate rule pattern matching
_unify_* function returns to unify with its first two parameters switched (except _unfiy_metavar which is the end rule)
- - - - - a891076d by n3f4s at 2016-06-16T18:20:27+02:00 correct return from nested call to unify
- - - - - 9d5bddff by n3f4s at 2016-06-17T17:56:30+02:00 push up utility function and debug expected type
- - - - - b2190434 by n3f4s at 2016-06-17T17:57:35+02:00 add call unifyer and debug unify
unify -> missing cons parameter in match
- - - - - 9a13dd1a by n3f4s at 2016-06-17T17:59:13+02:00 debug mutual recursion and cons param
cons param -> add missing cons parameter in match mutual recursion -> use 'and' instead of 'let' to allow mutual recusion
- - - - - 641cdaa1 by n3f4s at 2016-06-17T22:39:35+02:00 debug call to unify in _unify_builtin
change first parameter of call to unify in _unify_builtin to avoid calling unify with the same lexp
- - - - - 580f6053 by n3f4s at 2016-06-17T22:41:28+02:00 Merge branch 'master' into unification
- - - - - 64417ead by n3f4s at 2016-06-20T20:53:26+02:00 remove int of substitution, and add global metavar
- - - - - 68852c47 by n3f4s at 2016-06-20T20:55:20+02:00 add doc & corrected unifyer
- - - - - 978833c3 by n3f4s at 2016-06-20T20:56:19+02:00 add _unify_inner
_unify_inner -> generalisation of _unify_inner_arrow
- - - - - 97124603 by n3f4s at 2016-06-20T21:12:28+02:00 add combine and use _unify_inner in _unify_let
- - - - - 39aded24 by n3f4s at 2016-06-20T22:17:34+02:00 correct unifyer (Let & Metavar)
- - - - - 0e633789 by n3f4s at 2016-06-20T22:59:05+02:00 add unification for Call, Call
- - - - - a93fd019 by n3f4s at 2016-06-20T23:57:24+02:00 replace Metavar(_,_,_) by Metavar(int * vdef)
- - - - - 61129132 by n3f4s at 2016-06-20T23:58:04+02:00 add case Var, Imm in _unify_var
- - - - - 4943fc4f by n3f4s at 2016-06-21T21:19:24+02:00 add _unify_cons and correct infinite recursion
- - - - - ddece110 by n3f4s at 2016-06-22T18:16:07+02:00 add _unify_susp
- - - - - d92aa7f7 by n3f4s at 2016-06-22T22:54:54+02:00 swtich from _unify_inner_arrow to _unify_inner
_unify_inner is a generalized version of _unify_inner_arrow
- - - - - cabefe09 by n3f4s at 2016-06-23T00:10:43+02:00 add _unify_induction for induction -> induction
- - - - - 92c144b1 by n3f4s at 2016-06-23T18:20:25+02:00 add test for unification
- - - - - 2c96fe00 by n3f4s at 2016-06-23T18:20:59+02:00 add doc _unfiy_induct & refactoring
- - - - - af770325 by n3f4s at 2016-06-23T19:15:13+02:00 add test case to unify_test
- - - - - d1706192 by n3f4s at 2016-06-23T23:36:54+02:00 add printing of lexp type in _unify_test
- - - - - f2c80dc6 by n3f4s at 2016-06-24T20:44:39+02:00 add _unify_case and correct _unify_inner
make suer _unify_inner fail when one unification fail
- - - - - 674cb642 by n3f4s at 2016-06-24T20:54:29+02:00 add check of default in _unify_case
- - - - - e0141d3f by n3f4s at 2016-06-27T16:38:38+02:00 Merge branch 'master' into unification
- - - - - 716e4d39 by n3f4s at 2016-06-27T16:42:20+02:00 add naive unification for Sort & SortLevel
- - - - - c2f914ab by n3f4s at 2016-06-27T17:48:41+02:00 re-ordering code for readability
- - - - - 1a8f1f70 by n3f4s at 2016-06-27T17:49:21+02:00 add _unify_sort* to top level unify function
- - - - - 4e00bcc5 by n3f4s at 2016-06-27T22:54:55+02:00 add unification case for _unify_sort
- - - - - d50e1e6a by n3f4s at 2016-06-27T23:47:55+02:00 correct _unify_induct
- - - - - 8757daba by n3f4s at 2016-06-27T23:48:44+02:00 add unification for Var & Susp with Sort
- - - - - ba72e9be by n3f4s at 2016-06-28T16:22:56+02:00 Add Case, Let, and Susp to the first unifyed types
- - - - - b4776a7e by n3f4s at 2016-06-28T16:25:18+02:00 correct case unification
Unification with Case returns a constraint Check result of unification of the 'inside' of the Case for unification Case, Case
- - - - - 86e66e31 by n3f4s at 2016-06-28T16:27:39+02:00 Correct _unify_induct & _unify_sort
- - - - - 3950fd86 by n3f4s at 2016-06-28T20:48:58+02:00 move doc, error management with List.combine
switch from List.combine to zip to handle case where the two list have different size
- - - - - ee113a9e by n3f4s at 2016-06-28T21:43:38+02:00 add test case
- - - - - ddfe6931 by n3f4s at 2016-06-28T22:39:03+02:00 debug recursion on wrong variable
- - - - - 46aab474 by n3f4s at 2016-06-29T20:51:49+02:00 remove useless code & add test from typer code
add lexp generation from typer code in unification test add better printing system for unification test
- - - - - 57ff42c3 by n3f4s at 2016-06-29T22:48:00+02:00 add printing function for the lexp
- - - - - 107698ef by n3f4s at 2016-06-29T22:48:25+02:00 add printing function for debugging
- - - - - 476e08f2 by n3f4s at 2016-06-29T22:49:48+02:00 add print for debugging
- - - - - 490c9126 by n3f4s at 2016-06-29T22:50:06+02:00 change result of _unify_inner
_unify_inner returned None instead of non-error value, which caused the unification of the a let with himself to fail
- - - - - 48bc1748 by n3f4s at 2016-06-29T22:51:38+02:00 add test case for let
- - - - - 2f8bf17e by n3f4s at 2016-06-30T16:01:58+02:00 improved debug printing
- - - - - 156353fa by n3f4s at 2016-06-30T16:03:49+02:00 zip returns option for error handling & refactor
zip return an option for the case when the two list don't have the same size (-> error), and the empty list case (-> not an error)
extract some function for readability
- - - - - 817f5f19 by n3f4s at 2016-06-30T16:06:20+02:00 add debug printing, correct _unify_inner, add test
_unify_inner returns a substitution if it receive an empty list
change one of the case test to have more difference between the two case
- - - - - 9245f2c3 by n3f4s at 2016-06-30T17:54:13+02:00 improved debug logging
- - - - - 239ce526 by n3f4s at 2016-06-30T17:57:21+02:00 refactoring : extract function
extract inner match into function to avoid "arrow pattern" with multiple level of match
- - - - - 1fbfe683 by n3f4s at 2016-06-30T22:24:57+02:00 debug recursion on wrong lexp in _unify_call
- - - - - 3f93815b by n3f4s at 2016-06-30T22:26:01+02:00 better printing for debugging & test
- - - - - c520b3e9 by n3f4s at 2016-06-30T22:26:16+02:00 add test case
- - - - - 8a0ad87e by n3f4s at 2016-07-01T16:06:51+02:00 add test case
- - - - - 9652bc5e by n3f4s at 2016-07-04T21:54:46+02:00 add lexp S.subst to Metavar
- - - - - 96a7856a by n3f4s at 2016-07-04T21:55:54+02:00 change expected result of test for Lambda * Lambda
- - - - - 05aea4ec by n3f4s at 2016-07-04T21:57:05+02:00 add Metavar in unsusp
- - - - - e2e37a5c by n3f4s at 2016-07-06T16:04:59+02:00 add beginning of index substitution in _unify_meta
- - - - - 6bc9f1f9 by n3f4s at 2016-07-06T16:39:52+02:00 change unsusp for Susp(_,_)
- - - - - d9a44f1b by n3f4s at 2016-07-06T21:52:44+02:00 add first idea of finding inverse of substitution
- - - - - 357c3f5e by n3f4s at 2016-07-06T23:07:32+02:00 better printing for sort(level)
- - - - - f771c1f5 by n3f4s at 2016-07-06T23:08:03+02:00 add test for sort
- - - - - dcf7fce4 by n3f4s at 2016-07-06T23:08:19+02:00 add lexp_loc for metavar
- - - - - 8d0ea3b7 by n3f4s at 2016-07-07T16:36:11+02:00 compose s & s' in unsusp for metavar
- - - - - 81a12842 by n3f4s at 2016-07-07T16:36:40+02:00 use mkSusp instead of Susp(_, _) in _unify_metavar
- - - - - d18fac93 by n3f4s at 2016-07-14T22:24:26+02:00 add begining flattening function
- - - - - 9d83a8d4 by n3f4s at 2016-07-14T22:25:41+02:00 move inversion function out of unification
- - - - - 98dde635 by n3f4s at 2016-07-18T23:30:52+02:00 add test for substituttion inversion
- - - - - b8267fd7 by n3f4s at 2016-07-18T23:31:41+02:00 better output & first version of inversion
- - - - - 73772928 by n3f4s at 2016-07-18T23:58:57+02:00 add test
Inversion fail when the first variable is generated
- - - - - 93eb0302 by n3f4s at 2016-07-19T00:51:47+02:00 debug case where the first variable is generated
- - - - - e9223a23 by n3f4s at 2016-07-19T18:11:41+02:00 ocamldoc compliant documentation
- - - - - 8b9352ac by n3f4s at 2016-07-19T21:06:46+02:00 better printing for substitution
- - - - - ff8660c0 by n3f4s at 2016-07-19T21:12:30+02:00 better indentation for doc
- - - - - 801db020 by n3f4s at 2016-07-19T21:13:44+02:00 refactoring in fill function for readability
- - - - - 31a0d0d0 by n3f4s at 2016-07-19T21:14:13+02:00 add test for substitution inversion
- - - - - 27fc552d by n3f4s at 2016-07-19T22:13:47+02:00 Add function for creating test input
- - - - - 37f21f32 by n3f4s at 2016-07-20T16:58:41+02:00 Dummy variable have index shift+1 instead of -1
- - - - - 0461e108 by n3f4s at 2016-07-20T17:01:45+02:00 add generation of random test
- - - - - 2f8b27cf by n3f4s at 2016-07-21T21:36:56+02:00 better output for subst
- - - - - 692dd5bb by n3f4s at 2016-07-21T21:38:01+02:00 change subst transformation algo
- - - - - bf59e3c0 by n3f4s at 2016-07-21T21:38:58+02:00 re-indentation
- - - - - 28a0a1d9 by n3f4s at 2016-07-21T21:39:13+02:00 add better testing
- - - - - 629fa172 by n3f4s at 2016-07-21T23:54:36+02:00 better testing of inversion & tranformation
- - - - - 77068263 by n3f4s at 2016-07-25T17:02:43+02:00 better test output
- - - - - b72ea611 by n3f4s at 2016-07-25T17:03:08+02:00 debug substitution composed only with Cons
- - - - - 4282321b by n3f4s at 2016-07-26T17:50:38+02:00 sort substitutions during inversion
prevent inversion of substitution from returning an invalid substitution
- - - - - 3226d35e by n3f4s at 2016-07-26T21:51:37+02:00 apply the Shift on Id instead of the whole subst
- - - - - f4086ee1 by n3f4s at 2016-07-26T21:58:37+02:00 change implementation of sizeOf
- - - - - b1f5bca2 by n3f4s at 2016-07-26T21:59:15+02:00 add check for de Bruijn index
- - - - - f2514bb5 by n3f4s at 2016-07-27T18:08:04+02:00 sort (e_i, i) couples during inversion
- - - - - 18f3261b by n3f4s at 2016-07-27T18:09:45+02:00 remove dead code, add type hint and update doc
- - - - - 65bbe6d1 by n3f4s at 2016-07-27T18:37:49+02:00 update doc
- - - - - 03221c91 by n3f4s at 2016-07-27T23:25:05+02:00 add error in inverse for subst with same index
- - - - - ead6631f by n3f4s at 2016-07-27T23:26:20+02:00 better comparison against Id in tests
- - - - - 523c1f4d by n3f4s at 2016-07-27T23:26:58+02:00 better testing for INVERSE & TRANSFORMATION
- - - - - b291e84b by n3f4s at 2016-07-28T00:11:34+02:00 random (passing) test
- - - - - 4e504963 by Stefan Monnier at 2016-07-28T12:42:23-04:00 Tweak use of substitutions and unsusp
* src/inverse_subst.ml (mkFinalShift): Remove; use S.shift instead. (toIr): Use S.mkShift. (flattenIr.flattenCons): Remove unused `offset' arg. Simplify.
* src/lexp.ml (subst): Newtype. (mkSusp): Also apply eagerly to Metavar. (push_susp): Rename from unsusp. (nosusp): Rename from ususp_all. (_lexp_to_str): Use push_susp.
* src/unification.ml (unify.tmp): Use nosusp. (_unify_susp): Remove.
* tests/inverse_test.ml: Use S.shift/cons and friends.
- - - - - 93626d8b by Stefan Monnier at 2016-07-28T14:12:26-04:00 * tests/inverse_test.ml (is_identity.is_identity): Only shift 0 is identity.
- - - - - 293f20f6 by Stefan Monnier at 2016-07-28T14:15:34-04:00 * tests/inverse_test.ml (is_identity.is_identity): Forget it
* src/lexp.ml (push_susp): Don't be so picky.
- - - - - 79f26644 by n3f4s at 2016-07-28T23:28:58+02:00 fix non termination of test
- - - - - 2a02a1fb by n3f4s at 2016-07-28T23:48:06+02:00 add metavar in lexp_p_infer for default case
- - - - - ec33b98a by n3f4s at 2016-07-28T23:49:49+02:00 remove padding for random test
- - - - - 3b5313eb by n3f4s at 2016-07-28T23:50:48+02:00 add test for type checking
- - - - - 42608955 by n3f4s at 2016-07-29T18:22:00+02:00 debug inversion for Id ↑^X
- - - - - 05af83ee by n3f4s at 2016-07-29T20:44:49+02:00 begining of adding unification in type check
- - - - - 5d99315b by n3f4s at 2016-07-29T21:16:28+02:00 try to remove iteration
- - - - - a0b5b8d0 by n3f4s at 2016-07-29T21:23:55+02:00 fix transformation : change shift value in transfo
merge toIr, flattenIr and to_list in transfo
- - - - - 7798134b by n3f4s at 2016-07-29T21:47:14+02:00 add check for deBruijn indices >= shift offset
- - - - - 5acc8450 by n3f4s at 2016-07-29T21:48:22+02:00 remove useless code
- - - - - 946063a6 by n3f4s at 2016-07-29T21:48:36+02:00 adapt tests
- - - - - 8b249028 by n3f4s at 2016-07-29T23:18:37+02:00 merge fill with to_cons
- - - - - 304245b6 by n3f4s at 2016-07-29T23:20:23+02:00 remove useless code
- - - - - d0a20473 by n3f4s at 2016-08-01T21:25:00+02:00 add global (susbtitution * constraint) variable
- - - - - 68895a5c by n3f4s at 2016-08-01T21:44:36+02:00 add unification for default case of infer
- - - - - 8a15dbf9 by n3f4s at 2016-08-01T21:46:49+02:00 add unification for lambda in check
- - - - - d0a41841 by n3f4s at 2016-08-01T21:47:27+02:00 add unification for default case in check
- - - - - 910c29ef by n3f4s at 2016-08-05T23:51:10+02:00 change debug print from stdout to stderr
- - - - - 501fd9c5 by n3f4s at 2016-08-05T23:51:36+02:00 remove lambda case from infer
- - - - - 17e17516 by n3f4s at 2016-08-05T23:53:26+02:00 add None case for Plambda in check & refactoring
- - - - - 7051ef29 by n3f4s at 2016-08-05T23:54:21+02:00 add debug and idea of implicit argument in call
- - - - - 0e53c1ea by n3f4s at 2016-08-05T23:55:00+02:00 add test for inference
- - - - - 872b0143 by n3f4s at 2016-08-08T17:47:11+02:00 better debuging
- - - - - 76ecccda by n3f4s at 2016-08-08T18:12:05+02:00 better debug printing and add mkMetavar helper
- - - - - 0cb401ef by n3f4s at 2016-08-08T18:13:04+02:00 refactoring of Plambda case in check
- - - - - 34c98ba5 by n3f4s at 2016-08-10T17:46:09+02:00 better output
- - - - - d997582c by n3f4s at 2016-08-10T18:05:21+02:00 debug check for Plambda
- - - - - 98220426 by n3f4s at 2016-08-10T18:07:23+02:00 add a case for metavar in default case in check
avoid stack overflow caused by infinite recursion between infer and check
- - - - - f57a7c31 by n3f4s at 2016-08-10T18:09:00+02:00 add function that create metavar for implicit arg
- - - - - 284f6487 by n3f4s at 2016-08-10T18:09:45+02:00 use infer_implicit_arg to manage non Aexplicit
extract the part that check for non Aexplicit arg and create metavar for implicit arg to a function
- - - - - 484b86c8 by n3f4s at 2016-08-10T18:13:41+02:00 add test for non Aexplicit arg in function
- - - - - 98488b1a by n3f4s at 2016-08-10T18:14:00+02:00 remove type anotation in test
- - - - - 06c50bba by n3f4s at 2016-08-10T21:06:03+02:00 add mkMetavar wrapper
- - - - - 7d49d849 by n3f4s at 2016-08-10T21:13:30+02:00 replace metavar construction by call to wrapper
- - - - - 93ab8238 by n3f4s at 2016-08-10T21:15:00+02:00 replace metavar construction by call to wrapper
- - - - - 912c40d4 by n3f4s at 2016-08-10T21:24:32+02:00 extract unification with "new" arrow in a function
- - - - - 8b9efc77 by n3f4s at 2016-08-10T21:32:08+02:00 extract Lambda creation into a function
- - - - - e4b8d6d2 by n3f4s at 2016-08-10T21:34:29+02:00 better output for error in default case in check
- - - - - 257114e0 by n3f4s at 2016-08-10T21:59:07+02:00 default case of check return inferred_t
cause eval test to fail with an error : too many argument
- - - - - d16f8174 by n3f4s at 2016-08-10T22:03:55+02:00 move lambda case from infer to check
makes infinite recursion pass (infinte recursion failed in previous commit) but cause errors in unfication test : change result of lexp_decls_str
- - - - - a7e14366 by n3f4s at 2016-08-10T22:22:57+02:00 reduce lambda case in check
(do not resolve bugs)
- - - - - 8e08924e by n3f4s at 2016-08-10T23:32:06+02:00 better ouput
- - - - - c379c3cc by n3f4s at 2016-08-10T23:33:48+02:00 add test for lparse
- - - - - 22ffd69b by n3f4s at 2016-08-10T23:34:35+02:00 add implicit arg management
- - - - - 8554fb2a by n3f4s at 2016-08-10T23:35:07+02:00 add debug output when var/fun not found
- - - - - 1cb81d1c by n3f4s at 2016-08-10T23:52:21+02:00 debug infinite (mutual) recursion for check &infer
- - - - - eb7ee412 by n3f4s at 2016-08-11T21:19:35+02:00 add pexp formatting
- - - - - 3b603a9a by n3f4s at 2016-08-11T21:24:13+02:00 raise an error for non handled case in infer
- - - - - a9d89581 by n3f4s at 2016-08-11T21:26:48+02:00 remove metavar case in default case in check
- - - - - a9273fa2 by n3f4s at 2016-08-11T21:45:21+02:00 Merge branch 'tests' into unification
- - - - - 6fa48187 by n3f4s at 2016-08-12T23:12:22+02:00 add name in metavar creation
- - - - - eabcc167 by n3f4s at 2016-08-17T00:03:00+02:00 modify the test to make them pass
- stop lparse test from always failing - change the L-exp in unify_test according to decl_str output
- - - - - b520dda8 by n3f4s at 2016-08-17T00:05:28+02:00 change the output of infer_implicit_arg
fix throw in conversion from typer list to ocaml list but cause error regarding number of argument
- - - - - 77fef2c1 by n3f4s at 2016-08-17T00:07:32+02:00 add basic printing for metavar in _lexp_to_str
- - - - - 49d6e22d by n3f4s at 2016-08-17T00:20:18+02:00 add call to lambda with implicit arg, lparse test
- - - - - 5b0b03fe by n3f4s at 2016-08-17T21:45:55+02:00 remove unused code
- - - - - f2751880 by n3f4s at 2016-08-17T21:46:48+02:00 remove commented code
- - - - - 3172b157 by n3f4s at 2016-08-17T22:32:42+02:00 add Pmetavar case in lexp_p_infer
- - - - - d4c27327 by n3f4s at 2016-08-18T18:53:22+02:00 improve implicit/explicit argument handling
- - - - - 133f6fc1 by n3f4s at 2016-08-18T18:54:09+02:00 try to resolve not enough arg with metavar
- - - - - 80547416 by n3f4s at 2016-08-19T06:11:22+02:00 add arg_kind in lexp printing
- - - - - 4ef9006d by n3f4s at 2016-08-22T17:07:33+02:00 fix throw exception for partial application
- - - - - d00bf033 by n3f4s at 2016-08-22T20:17:04+02:00 remove useless printing
- - - - - da4bebac by n3f4s at 2016-08-23T23:15:52+02:00 remove debug printing
- - - - - 85c06461 by n3f4s at 2016-08-25T17:30:34+02:00 Merge branch 'master' into unification
- - - - - a964be1b by Stefan Monnier at 2016-08-26T23:54:31-04:00 Merge branch 'trunk' into unification
- - - - - 43003f8d by Stefan Monnier at 2016-08-27T18:04:58+02:00 Fix syntax of explicit-implicit args
* typer-mode.el (typer-smie-grammar): Fix grammar for `:=`. Add if/then/else to the grammar. Remove `:-` and `:≡`. * tests/sexp_test.ml: Add test for `:=` and if/then/else. * tests/eval_test.ml, tests/macro_test.ml: Use explicit implicit args. * src/grammar.ml (default_grammar): Update from type-mode.el. * doc/manual.texi (Core Syntax): Only keep `:=` for explicit args. * src/builtin.ml (get_attribute_impl, declexpr_impl) (is_builtin_macro): Silence compiler-warning. * btl/types.typer (length): Pass explicitly implicit parameter.
- - - - - 4b31963e by Stefan Monnier at 2016-08-27T18:08:13+02:00 * src/lparse.ml (lexp_call): Rewrite to work one-arg at a time
Add basic support for explicit-implicit args. Use lexp_whnf. (lexp_call.get_return_type): Remove. (_lexp_p_infer, lexp_read_pattern, lexp_decls_macro): Adjust to new env_lookup_expr. (_lexp_parse_all.loop): Don't use List.hd when not needed. * src/typecheck.ml (lexp_whnf): New function. * src/debruijn.ml (env_lookup_expr): Return an option. * src/builtin.ml (get_attribute_impl, declexpr_impl): Adjust accordingly. * btl/types.typer (length): One more explicit-implicit arg.
- - - - - 6637588f by n3f4s at 2016-08-27T18:08:13+02:00 merge
- - - - - ac470790 by n3f4s at 2016-08-27T18:08:13+02:00 merge
- - - - - 531da09a by n3f4s at 2016-08-31T17:03:56+02:00 remove code in comment
- - - - - 133522c1 by n3f4s at 2016-08-31T17:04:38+02:00 fix infinite recursion in push_susp
add check for Identity in Metavar/Var case in push_susp
- - - - - 465e8df3 by n3f4s at 2016-08-31T17:05:43+02:00 remove trailing space
- - - - - 36b6254a by n3f4s at 2016-09-06T21:51:02+02:00 change type of metavar type in Pmetavar (infer)
- - - - - 63b652c6 by n3f4s at 2016-09-06T21:53:45+02:00 change debug output
- - - - - c34bcc0a by n3f4s at 2016-09-07T19:39:45+02:00 add metavar management in lexp_whnf
- - - - - 913d45e4 by n3f4s at 2016-09-07T21:06:44+02:00 Merge branch 'master' into unification
- - - - - 1009a3c7 by n3f4s at 2016-09-07T22:29:34+02:00 add metavar handlind in lexp_whnf
- - - - - cd269106 by n3f4s at 2016-09-08T16:54:30+02:00 better lexp formatting
- - - - - 406ac0da by n3f4s at 2016-09-09T03:50:02+02:00 clean unification.ml
- better variable naming - unify formatting - move types to lexp.ml
- - - - - 1b57485f by n3f4s at 2016-09-09T03:52:55+02:00 add metavar context printing and clean code
- - - - - 59a7efc6 by n3f4s at 2016-09-09T03:54:41+02:00 add doc
- - - - - a7136734 by n3f4s at 2016-09-09T04:08:37+02:00 clean code and add doc
- - - - - 13b6dba7 by n3f4s at 2016-09-09T17:32:30+02:00 add doc
- - - - - c2e85c1e by n3f4s at 2016-09-09T18:12:36+02:00 add debug output
- - - - - ea747f75 by n3f4s at 2016-09-09T18:13:11+02:00 clean code && correct moved function
- - - - - 2bd4d49a by Stefan Monnier at 2016-09-12T17:06:17-04:00 * src/lexp.ml (push_susp): Use nosusp
* src/lparse.ml (get_type0, get_int): Remove (again). (_lexp_p_check.infer_lambda_body.ltp): Minor layout tweaks.
- - - - - 5faabc18 by Stefan Monnier at 2016-09-14T15:09:19-04:00 Merge branch 'trunk' into unification
- - - - - 92e904a6 by Stefan Monnier at 2016-09-14T15:10:06-04:00 Remove supurious thingy
- - - - - df72decc by Stefan Monnier at 2016-09-25T21:55:39-04:00 Merge branch 'trunk' into unification
- - - - - a761156c by Stefan Monnier at 2016-09-26T09:50:04-04:00 Merge branch 'trunk' into unification
- - - - - 6d7b4793 by Stefan Monnier at 2016-09-26T20:34:16-04:00 Merge branch 'trunk' into unification
- - - - - a84525ad by Stefan Monnier at 2016-10-01T23:11:33-04:00 Merge branch 'trunk' into unification
- - - - - 03807ed4 by n3f4s at 2016-10-05T11:42:24+02:00 add internship report tex file
- - - - - 9dab10b2 by n3f4s at 2016-10-05T11:42:24+02:00 add makefile for compiling report
- - - - - 6e100ad5 by n3f4s at 2016-10-05T11:42:24+02:00 update doc rule of main makefile for report
- - - - - 0bec5cff by Stefan Monnier at 2016-10-05T15:09:46-04:00 Merge branch 'trunk' into unification
- - - - - c2626ca7 by Stefan Monnier at 2016-10-05T19:03:01-04:00 Merge branch 'trunk' into unification
- - - - - 9ce6c688 by n3f4s at 2016-10-07T00:24:30+02:00 add debug output
- - - - - e71a2bde by n3f4s at 2016-10-07T00:24:30+02:00 update report
- - - - - fdf96490 by n3f4s at 2016-10-07T00:24:31+02:00 debug makefile
- - - - - 969e81a9 by n3f4s at 2016-10-07T09:58:56+02:00 try to undo some changes
- - - - - 6d9ca990 by n3f4s at 2016-10-07T10:01:53+02:00 try to undo bad changes to lparse.ml
- - - - - 4692b07f by n3f4s at 2016-10-07T10:03:42+02:00 add missing package for the report title
- - - - - 2ca60f54 by n3f4s at 2016-10-07T10:33:30+02:00 better formatting of expression in report
- - - - - 7afcdca9 by Stefan Monnier at 2016-10-07T18:21:16-04:00 * src/lparse.ml: Revert a few more reversions
* src/lparse.ml (ctx_define, ctx_define_rec, _lexp_p_infer) (_lexp_p_check, lexp_decls_1): Revert a few more reversions.
- - - - - 834fd729 by Stefan Monnier at 2016-10-07T18:28:13-04:00 Merge branch 'trunk' into unification
- - - - - 01457ebd by n3f4s at 2016-10-08T14:31:02+02:00 update report
- - - - - c02777f9 by Stefan Monnier at 2016-10-09T10:34:43-04:00 Fix thinko where List's type was used as its definition
* src/lparse.ml (lexp_p_infer_and_check): New function extracted from _lexp_p_check. Fix the "Some subst" case to return `e` rather than its type. (_lexp_p_check): Use it.
- - - - - d3a880af by n3f4s at 2016-10-11T16:11:56+02:00 fix nosusp bug in unfiy
result of nosusp wasn't used when dispatching to specialized unify functions.
- - - - - 117a72f7 by n3f4s at 2016-10-11T16:13:32+02:00 remove default case hiding "coding" error
- - - - - 521cad46 by n3f4s at 2016-10-11T16:13:59+02:00 add test number(in comment) in unification tests
- - - - - 6cb1661b by Stefan Monnier at 2016-10-17T23:38:03-04:00 Gut Fmt_lexp. Use lexp_string and lexp_print instead
* src/debug_fun.ml: Don't open Fmt_lexp. Don't enable debugging trace by default. Use lexp_string.
* src/fmt_lexp.ml: Strip it down to just the two padding functions.
* src/lexp.ml (subst_string): New function.
- - - - - fefc0753 by Stefan Monnier at 2016-10-19T14:38:16-04:00 Merge branch 'trunk' into unification
- - - - - df86998f by Stefan Monnier at 2016-10-19T14:46:07-04:00 Merge branch 'trunk' into unification
- - - - - 07f429b3 by Stefan Monnier at 2016-10-27T20:37:32-04:00 Merge branch 'trunk' into unification
- - - - - 89c67665 by Stefan Monnier at 2016-10-27T21:03:13-04:00 Fix some of the tests
- - - - - a707155b by Stefan Monnier at 2016-10-28T14:55:10-04:00 Infer implicit args; Give type to metavars
* src/lexp.ml (lexp): Add type to `Metavar`. (lexp_unparse): (somewhat) Handle Metavar and Sort.
* src/lparse.ml (global_substitution): Move, so elab_check_sort can use it. (mkMetavar): Add type arg. (mkMetalevel, mkMetatype): New functions. (elab_check_sort._lexp_p_infer): Use them. (_lexp_p_check.unify_with_arrow): Use the explicit arg type if present. (elab_check_sort.lexp_call.handle_fun_args): Infer missing implicit arg.
* src/opslexp.ml (lexp_whnf): Rewrite to reduce diff w.r.t `trunk`. (check): Add case of `Metavar`.
* src/unification.ml (mkMetavar): Remove.
* tests/eval_test.ml ("Lists"): Remove explicit-implicit args.
* tests/unify_test.ml: Remove unsupported `case` on integers.
* tests/utest_lib.ml (for_all_tests): Remove try/with which hides the better backtrace one gets with OCAMLRUNPARAM=b.
- - - - - 33d80b67 by Stefan Monnier at 2016-10-31T12:43:25-04:00 Merge branch 'trunk' into unification
- - - - - f4010f96 by Stefan Monnier at 2016-10-31T12:46:11-04:00 * lparse.ml: Move Pmetavar from infer to check
- - - - - aaad384e by Stefan Monnier at 2016-11-01T13:12:13-04:00 Merge branch 'trunk' into unification
- - - - - f762ac7e by Stefan Monnier at 2016-11-04T14:29:10-04:00 Merge branch 'trunk' into unification
- - - - - b6acb432 by Stefan Monnier at 2016-11-04T18:17:46-04:00 * src/lparse.ml (newMeta*, newMeta*, newMeta*): Renames
* src/lparse.ml (newMetavar, newMetatype, newMetalevel): Rename from mkMeta*. Use Lexp's mkMetavar to hash-cons the node.
- - - - - 989e999b by Stefan Monnier at 2016-11-07T14:28:18-05:00 Merge branch 'trunk' into unification
- - - - - 735256f3 by Stefan Monnier at 2016-11-07T15:04:27-05:00 Merge branch 'trunk' into unification
- - - - - 7f3c0935 by Stefan Monnier at 2016-11-08T14:17:52-05:00 Merge branch 'trunk' into unification
- - - - - e66bcd5b by Stefan Monnier at 2016-11-08T14:18:38-05:00 Missing changes in last commit
- - - - - 015fdd7e by Stefan Monnier at 2016-11-08T14:20:15-05:00 Merge branch 'trunk' into unification
- - - - - a3ff5fc5 by Stefan Monnier at 2016-11-08T15:57:04-05:00 * src/unification.ml (unify'): Don't fail if the args are conv_p.
- - - - - 663b82a1 by Stefan Monnier at 2016-11-08T17:38:34-05:00 * doc/rapport: Remove (split into the report/vincent branch)
- - - - - 29925bc1 by Stefan Monnier at 2016-11-08T18:24:24-05:00 * src/debug_fun.ml, src/fmt_lexp.ml: Remove
* src/util.ml (padding_right, padding_left): Move from fmt_lexp.ml. (utf8_head_p, string_width): New functions. * src/prelexer.ml (inc_cp): Use them.
- - - - - e0c03878 by Stefan Monnier at 2016-11-08T23:07:54-05:00 Make explicit args reordering work
* btl/types.typer (run-io): Make first operation of type Unit.
* src/lexp.ml (meta_subst): Rename from substitution. (empty_meta_subst): Rename from empty_meta_subst.
* src/lparse.ml (_lexp_p_infer): Un-comment out the Plambda case. (lexp_call): Improve handle_fun_args for re-ordering of explicit args.
- - - - - 794c962d by Stefan Monnier at 2016-11-08T23:16:18-05:00 * src/opslexp.ml (check): Add `meta_ctx` argument
- - - - - 604b0116 by Stefan Monnier at 2016-11-08T23:29:56-05:00 * tests/utest_lib.ml (for_all_tests): Re-enable backtrace catching.
- - - - - 962096c7 by Stefan Monnier at 2016-11-09T15:52:35-05:00 * GNUmakefile: Merge changes from Makefile
* Makefile: Remove.
- - - - - 0fc83c9b by Stefan Monnier at 2016-11-09T16:21:02-05:00 tests/{lparse,unify}_test.ml: Disable failing tests for now
- - - - - 3edbd09f by Stefan Monnier at 2016-11-10T15:54:02-05:00 Merge branch 'unification' into trunk
- - - - -
16 changed files:
- .gitignore - GNUmakefile - btl/types.typer - src/debug_util.ml - + src/inverse_subst.ml - src/lexp.ml - src/lparse.ml - src/opslexp.ml - src/prelexer.ml - + src/unification.ml - src/util.ml - tests/eval_test.ml - + tests/inverse_test.ml - + tests/lparse_test.ml - + tests/unify_test.ml - tests/utest_lib.ml
Changes:
===================================== .gitignore ===================================== --- a/.gitignore +++ b/.gitignore @@ -19,4 +19,5 @@ test.ml _temp_hack test__.typer *.orig -_tags \ No newline at end of file +_tags +.merlin
===================================== GNUmakefile ===================================== --- a/GNUmakefile +++ b/GNUmakefile @@ -1,4 +1,6 @@ RM=rm -f +MV=mv +OCAMLBUILD=ocamlbuild
BUILDDIR := _build
@@ -7,8 +9,15 @@ CPL_FILES := $(wildcard ./$(BUILDDIR)/src/*.cmo) TEST_FILES := $(wildcard ./tests/*_test.ml)
OBFLAGS = -lflags -g -cflags -g -build-dir $(BUILDDIR) +# OBFLAGS := -I $(SRCDIR) -build-dir $(BUILDDIR) -pkg str +# OBFLAGS_DEBUG := -tag debug -tag profile -tag "warn(+20)" +# OBFLAGS_RELEASE := -tag unsafe -tag inline +COMPILE_MODE = byte # COMPILE_MODE = native
+# DEBUG ?= 1 +# VERBOSE ?= 1 + all: typer debug tests-build
# ifeq ($(OS), Windows_NT) @@ -17,41 +26,50 @@ all: typer debug tests-build # OBFLAGS = $(OBFLAGS) -r # endif
-COMPILE_MODE = byte +# ifeq ($(DEBUG), 1) +# OBFLAGS += $(OBFLAGS_DEBUG) +# else +# OBFLAGS += $(OBFLAGS_RELEASE) +# endif + +help: ## Prints help for targets with comments + @grep -E '^[a-zA-Z_-]+:.*?## .*$$' $(MAKEFILE_LIST) \ + | { echo -e 'typer: ## Build Typer'; sort; } \ + | awk 'BEGIN {FS = ":.*?## "}; {printf "\033[36m%-30s\033[0m %s\n", $$1, $$2}'
# debug file eval debug: # ============================ # Build debug utils # ============================ - ocamlbuild src/debug_util.$(COMPILE_MODE) -I src $(OBFLAGS) - @mv $(BUILDDIR)/src/debug_util.$(COMPILE_MODE) $(BUILDDIR)/debug_util + $(OCAMLBUILD) src/debug_util.$(COMPILE_MODE) -I src $(OBFLAGS) + @$(MV) $(BUILDDIR)/src/debug_util.$(COMPILE_MODE) $(BUILDDIR)/debug_util
# interactive typer typer: # ============================ # Build typer # ============================ - ocamlbuild src/REPL.$(COMPILE_MODE) -I src $(OBFLAGS) - @mv $(BUILDDIR)/src/REPL.$(COMPILE_MODE) $(BUILDDIR)/typer + $(OCAMLBUILD) src/REPL.$(COMPILE_MODE) -I src $(OBFLAGS) + @$(MV) $(BUILDDIR)/src/REPL.$(COMPILE_MODE) $(BUILDDIR)/typer
tests-build: # ============================ # Build tests # ============================ @$(foreach test, $(TEST_FILES), \ - ocamlbuild $(subst ./,,$(subst .ml,.$(COMPILE_MODE) ,$(test))) \ + $(OCAMLBUILD) $(subst ./,,$(subst .ml,.$(COMPILE_MODE) ,$(test))) \ -I src $(OBFLAGS);) - @ocamlbuild tests/utest_main.$(COMPILE_MODE) -I src $(OBFLAGS) - @mv $(BUILDDIR)/tests/utest_main.$(COMPILE_MODE) \ + @$(OCAMLBUILD) tests/utest_main.$(COMPILE_MODE) -I src $(OBFLAGS) + @$(MV) $(BUILDDIR)/tests/utest_main.$(COMPILE_MODE) \ $(BUILDDIR)/tests/utests
tests-run: @./$(BUILDDIR)/tests/utests --verbose= 3
test-file: - ocamlbuild src/test.$(COMPILE_MODE) -I src $(OBFLAGS) - @mv $(BUILDDIR)/src/test.$(COMPILE_MODE) $(BUILDDIR)/test + $(OCAMLBUILD) src/test.$(COMPILE_MODE) -I src $(OBFLAGS) + @$(MV) $(BUILDDIR)/src/test.$(COMPILE_MODE) $(BUILDDIR)/test
# There is nothing here. I use this to test if opam integration works install: tests
===================================== btl/types.typer ===================================== --- a/btl/types.typer +++ b/btl/types.typer @@ -155,18 +155,15 @@ bind = Built-in "bind" ( % define a dummy type that supposed to represent a file FileHandle = Built-in "FileHandle";
-% define operation on file handle -%% runIO should have type IO Unit -> b -> b +%% `runIO` should have type IO Unit -> b -> b %% or IO a -> b -> b, which means "run the IO, throw away the result, %% and then return the second argument unchanged". The "dummy" b argument %% is actually crucial to make sure the result of runIO is used, otherwise %% the whole call would look like a dead function call and could be %% optimized away! -run-io = Built-in "run-io" ( - (a : Type) ≡> - (b : Type) ≡> - IO a -> b -> b); +run-io = Built-in "run-io" ((a : Type) ≡> IO Unit -> a -> a);
+% Define operations on file handle. open = Built-in "open" (String -> String -> IO FileHandle); write = Built-in "write" (FileHandle -> String -> IO Unit); read = Built-in "read" (FileHandle -> Int -> IO String);
===================================== src/debug_util.ml ===================================== --- a/src/debug_util.ml +++ b/src/debug_util.ml @@ -423,8 +423,9 @@ let main () =
let cctx = lctx_to_cctx ctx in (* run type check *) - List.iter (fun (_, lxp, _) -> - let _ = OL.check cctx lxp in ()) flexps; + List.iter (fun (_, lxp, _) + -> let _ = OL.check VMap.empty cctx lxp in ()) + flexps;
print_string (" " ^ (make_line '-' 76)); print_string "\n";));
===================================== src/inverse_subst.ml ===================================== --- /dev/null +++ b/src/inverse_subst.ml @@ -0,0 +1,129 @@ +(* inverse_subst.ml --- Computing the inverse of a substitution + +Copyright (C) 2016 Free Software Foundation, Inc. + +Author: Vincent Bonnevalle tiv.crb@gmail.com + +This file is part of Typer. + +Typer is free software; you can redistribute it and/or modify it under the +terms of the GNU General Public License as published by the Free Software +Foundation, either version 3 of the License, or (at your option) any +later version. + +Typer is distributed in the hope that it will be useful, but WITHOUT ANY +WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS +FOR A PARTICULAR PURPOSE. See the GNU General Public License for +more details. + +You should have received a copy of the GNU General Public License along with +this program. If not, see http://www.gnu.org/licenses/. *) + +open Lexp +open Util +module S = Subst + +(** Provide inverse function for computing the inverse of a substitution *) + +(* Transformation *) + +(** Convenience types and variables *) + +type inter_subst = lexp list (* Intermediate between "tree"-like substitution and fully flattened subsitution *) + +let dummy_var = Var((dummy_location, "DummyVar"), -1) + +type substIR = ((int * int) list * int) + +(** Transform a substitution to a more linear substitution + * makes the inversion easier + * Example of result : ((new_idx, old_position)::..., shift)*) +let transfo (s: lexp S.subst) : substIR option = + let rec transfo (s: lexp S.subst) (off_acc: int) (idx: int): substIR option = + let indexOf (v: lexp): int = (* Helper : return the index of a variabble *) + match v with + | Var (_, v) -> v + | _ -> assert false + in + let shiftVar (var: lexp) (offset: int): int = + indexOf (mkSusp var (S.shift offset)) (* Helper : shift the index of a var *) + in + match s with + | S.Cons (Var _ as v, s) -> + (match transfo s off_acc (idx + 1) with + | Some (tail, off) -> let newVar = shiftVar v off_acc + in if newVar >= off then None (* Error *) + else Some (((shiftVar v off_acc), idx)::tail, off) + | None -> None) + | S.Shift (s, offset) -> transfo s (offset + off_acc) idx + | S.Identity -> Some ([], off_acc) (* End of recursion *) + | _ -> None (* Error *) + in transfo s 0 0 + +(* Inverse *) + +(** Returns the number of element in a sequence of S.Cons +*) +let rec sizeOf (s: (int * int) list): int = List.length s + +(** Returns a dummy variable with the db_index idx +*) +let mkVar (idx: int): lexp = Var((U.dummy_location, ""), idx) + +(** Fill the gap between e_i in the list of couple (e_i, i) by adding + dummy variables. + With the exemple of the article : + should return <code>(1,1)::(2, X)::(3,2)::(4,3)::(5, Z)::[]</code> + + @param l list of (e_i, i) couples with gap between e_i + @param size size of the list to return + @param acc recursion accumulator +*) +let fill (l: (int * int) list) (nbVar: int) (shift: int): lexp S.subst option = + let rec genDummyVar (beg_: int) (end_: int) (l: lexp S.subst): lexp S.subst = (* Create the filler variables *) + if beg_ < end_ + then S.cons (mkVar (nbVar + 1)) (genDummyVar (beg_ + 1) end_ l) + else l + in + let fill_before (l: (int * int) list) (s: lexp S.subst) (nbVar: int): lexp S.subst option = (* Fill if the first var is not 0 *) + match l with + | [] -> Some (genDummyVar 0 nbVar S.identity) + | (i1, v1)::_ when i1 > 0 -> Some (genDummyVar 0 i1 s) + | _ -> Some s + in let rec fill_after (l: (int * int) list) (nbVar: int) (shift: int): lexp S.subst option = (* Fill gaps *) + match l with + | (idx1, val1)::(idx2, val2)::tail when (idx1 = idx2) -> None + + | (idx1, val1)::(idx2, val2)::tail when (idx2 - idx1) > 1 -> + (match fill_after ((idx2, val2)::tail) nbVar shift with + | None -> None + | Some s -> Some (S.cons (mkVar val1) (genDummyVar (idx1 + 1) idx2 s))) + + | (idx1, val1)::(idx2, val2)::tail -> + (match fill_after ((idx2, val2)::tail) nbVar shift with + | None -> None + | Some s -> Some (S.cons (mkVar val1) s)) + + | (idx1, val1)::[] when (idx1 + 1) < nbVar -> + Some (S.cons (mkVar val1) (genDummyVar (idx1 + 1) nbVar (S.shift shift))) + + | (idx1, val1)::[] -> + Some (S.cons (mkVar val1) (S.shift shift)) + + | [] -> + Some (S.shift shift) + in match fill_after l nbVar shift with + | None -> None + | Some s -> fill_before l s nbVar + +(** Compute the inverse, if there is one, of the substitution. + + <code>s:S.subst, l:lexp, s':S.subst</code> where <code>l[s][s'] = l</code> and <code> inverse s = s' </code> +*) +let inverse (s: lexp S.subst) : lexp S.subst option = + let sort = List.sort (fun (ei1, _) (ei2, _) -> compare ei1 ei2) + in match transfo s with + | None -> None + | Some (cons_lst, shift_val) -> + let size = sizeOf cons_lst + in fill (sort cons_lst) shift_val size
===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -76,6 +76,9 @@ type ltype = lexp * ltype (* The type of the return value of all branches *) * (U.location * (arg_kind * vdef option) list * lexp) SMap.t * (vdef option * lexp) option (* Default. *) + (* The `subst` only applies to the lexp associated + * with the metavar's index (i.e. its "value"), not to the ltype. *) + | Metavar of int * subst * vdef * ltype (* (* For logical metavars, there's no substitution. *) * | Metavar of (U.location * string) * metakind * metavar ref * and metavar = @@ -114,6 +117,11 @@ type varbind = | ForwardRef | LetDef of lexp
+module VMap = Map.Make (struct type t = int let compare = compare end) +type meta_subst = lexp VMap.t +type constraints = (lexp * lexp) list +let empty_meta_subst = VMap.empty + let builtin_size = ref 0
(********************** Hash-consing **********************) @@ -137,6 +145,7 @@ let mkCall (f, es) = hc (Call (f, es)) let mkInductive (l, n, a, cs) = hc (Inductive (l, n, a, cs)) let mkCons (t, n) = hc (Cons (t, n)) let mkCase (l, e, rt, bs, d) = hc (Case (l, e, rt, bs, d)) +let mkMetavar (n, s, v, t) = hc (Metavar (n, s, v, t))
(********* Helper functions to use the Subst operations *********) (* This basically "ties the knot" between Subst and Lexp. @@ -151,6 +160,7 @@ let rec mkSusp e s = match e with | Susp (e, s') -> mkSusp e (scompose s' s) | Var (l,v) -> slookup s l v + | Metavar (vn, s', vd, t) -> mkMetavar (vn, scompose s' s, vd, mkSusp t s) | _ -> hc (Susp (e, s)) and scompose s1 s2 = S.compose mkSusp s1 s2 and slookup s l v = S.lookup (fun l i -> mkVar (l, i)) @@ -175,8 +185,8 @@ let rec lexp_location e = | Cons (_,(l,_)) -> l | Case (l,_,_,_,_) -> l | Susp (e, _) -> lexp_location e - (* | Susp (_, e) -> lexp_location e - * | Metavar ((l,_),_,_) -> l *) + (* | Susp (_, e) -> lexp_location e *) + | Metavar (_,_,(l,_), _) -> l
(********* Normalizing a term *********) @@ -238,7 +248,7 @@ let rec push_susp e s = (* Push a suspension one level down. *) * But we still have to handle them here, since push_susp is called * in many other cases than just when we bump into a Susp. *) | Susp (e,s') -> push_susp e (scompose s' s) - | (Var _) -> nosusp (mkSusp e s) + | (Var _ | Metavar _) -> nosusp (mkSusp e s)
and nosusp e = (* Return `e` without `Susp`. *) match e with @@ -401,6 +411,8 @@ let rec lexp_unparse lxp = in Pcase (loc, lexp_unparse target, pbranch)
(* FIXME: The cases below are all broken! *) + | Metavar (idx, subst, (loc, name), _) + -> Pimm (Symbol (loc, "?<" ^ name ^ "-" ^ string_of_int idx ^ ">"))
| SortLevel (SLz) -> Pimm (Integer (U.dummy_location, 0)) | SortLevel (SLsucc sl) -> Pcall (Pimm (Symbol (U.dummy_location, "<S>")), @@ -410,7 +422,13 @@ let rec lexp_unparse lxp = | Sort (l, Stype sl) -> Pcall (Pimm (Symbol (l, "<Type>")), [pexp_unparse (lexp_unparse sl)])
+(* FIXME: ¡Unify lexp_print and lexp_string! *) let lexp_string lxp = sexp_string (pexp_unparse (lexp_unparse lxp)) + +let rec subst_string s = match s with + | S.Identity -> "Id" + | S.Shift (s, n) -> "(" ^ subst_string s ^ "↑" ^ string_of_int n ^ ")" + | S.Cons (l, s) -> lexp_string l ^ " · " ^ subst_string s (* * Printing * --------------------- *) @@ -514,6 +532,9 @@ and _lexp_to_str ctx exp =
| Var ((loc, name), idx) -> name ^ (index idx) ;
+ | Metavar (idx, subst, (loc, name), _) + -> "?" ^ name ^ (index idx) (*TODO : print subst*) + | Let (_, decls, body) -> (* Print first decls without indent *) let h1, decls, idt_lvl =
===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -48,6 +48,8 @@ open Eval open Grammar open Builtin
+module Unif = Unification + module OL = Opslexp module EL = Elexp module SU = Subst @@ -90,8 +92,12 @@ let pexp_fatal = debug_message fatal pexp_name pexp_string let pexp_error = debug_message error pexp_name pexp_string let value_fatal = debug_message fatal value_name value_string
+(* :-( *) +let global_substitution = ref (empty_meta_subst, []) + let elab_check_sort (ctx : elab_context) lsort var ltp = - match OL.lexp_whnf lsort (ectx_to_lctx ctx) with + let meta_ctx, _ = !global_substitution in + match OL.lexp_whnf lsort (ectx_to_lctx ctx) meta_ctx with | Sort (_, _) -> () (* All clear! *) | _ -> let typestr = lexp_string ltp ^ " : " ^ lexp_string lsort in match var with @@ -103,7 +109,8 @@ let elab_check_sort (ctx : elab_context) lsort var ltp = ^ typestr)
let elab_check_proper_type (ctx : elab_context) ltp var = - try elab_check_sort ctx (OL.check (ectx_to_lctx ctx) ltp) var ltp + let meta_ctx, _ = !global_substitution in + try elab_check_sort ctx (OL.check meta_ctx (ectx_to_lctx ctx) ltp) var ltp with e -> print_string "Exception while checking type `"; lexp_print ltp; (match var with @@ -117,18 +124,19 @@ let elab_check_def (ctx : elab_context) var lxp ltype = let lctx = ectx_to_lctx ctx in let loc = lexp_location lxp in
- let ltype' = try OL.check lctx lxp + let meta_ctx, _ = !global_substitution in + let ltype' = try OL.check meta_ctx lctx lxp with e -> lexp_error loc lxp "Error while type-checking"; print_lexp_ctx (ectx_to_lctx ctx); raise e in - if OL.conv_p (ectx_to_lctx ctx) ltype ltype' then + if OL.conv_p meta_ctx (ectx_to_lctx ctx) ltype ltype' then elab_check_proper_type ctx ltype (Some var) else (debug_messages fatal loc "Type check error: ¡¡ctx_define error!!" [ (lexp_string lxp) ^ "!: " ^ (lexp_string ltype); " because"; - (lexp_string (OL.check lctx lxp)) ^ "!= " ^ (lexp_string ltype);]) + (lexp_string (OL.check meta_ctx lctx lxp)) ^ "!= " ^ (lexp_string ltype);])
let ctx_extend (ctx: elab_context) (var : vdef option) def ltype = elab_check_proper_type ctx ltype var; @@ -190,6 +198,19 @@ let ctx_define_rec (ctx: elab_context) decls = *)
+let newMetavar t = + let meta = Unif.create_metavar () in + let name = "__metavar" (* ^ (string_of_int meta) *) in + mkMetavar (meta, S.Identity, (Util.dummy_location, name), t) + +let newMetalevel () = + let meta = Unif.create_metavar () in + let name = "__metalevel" (* ^ (string_of_int meta) *) in + mkMetavar (meta, S.Identity, (Util.dummy_location, name), + Sort (dummy_location, StypeLevel)) + +let newMetatype () = newMetavar (newMetalevel ()) + let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype =
let trace = ((OL.Pexp p)::trace) in @@ -269,13 +290,10 @@ let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype = let v = mkInductive(tloc, label, formal, map_ctor) in v, ltp
- (* This case can be inferred *) - | Plambda (kind, var, optype, body) - -> let ltp, _ = match optype with - | Some ptype -> lexp_infer ptype ctx - (* This case must have been lexp_p_check *) - | None -> pexp_error tloc p "Lambda require type annotation"; - dltype, dltype in + (* This case can be inferred. *) + | Plambda (kind, var, Some ptype, body) + -> let ltp, lasort = lexp_infer ptype ctx in + elab_check_sort ctx lasort (Some var) ltp;
let nctx = env_extend ctx var Variable ltp in let lbody, lbtp = lexp_infer body nctx in @@ -288,9 +306,11 @@ let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype = | Pcons(t, sym) -> let idt, _ = lexp_infer t ctx in let (loc, cname) = sym in + let meta_ctx, _ = !global_substitution in
(* Get constructor args. *) - let formal, args = match OL.lexp_whnf idt (ectx_to_lctx ctx) with + let formal, args = match OL.lexp_whnf idt + (ectx_to_lctx ctx) meta_ctx with | Inductive(_, _, formal, ctor_def) as lxp -> (try formal, (SMap.find cname ctor_def) with Not_found -> @@ -334,7 +354,10 @@ let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype = -> let ltp = lexp_type_infer ptp ctx None trace in (_lexp_p_check pxp ltp ctx trace), ltp
- | _ -> pexp_fatal tloc p "Unhandled Pexp" + | (Plambda _ | Pcase _ | Pmetavar _) + -> let t = newMetatype () in + let lxp = _lexp_p_check p t ctx trace in + (lxp, t)
and lexp_type_infer pexp ectx var trace = let t, s = _lexp_p_infer pexp ectx trace in @@ -357,30 +380,54 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : elab_context) trace: lexp = _global_lexp_ctx := ctx; _global_lexp_trace := trace;
+ let unify_with_arrow lxp kind var aty subst = + let body = newMetatype () in + let arg = match aty with + | None -> newMetatype () + | Some laty -> laty in + let arrow = mkArrow (kind, None, arg, Util.dummy_location, body) in + match Unif.unify arrow lxp (ectx_to_lctx ctx) subst with + | Some subst -> global_substitution := subst; arg, body + | None -> lexp_error tloc lxp ("Type " ^ lexp_string lxp + ^ " and " + ^ lexp_string arrow + ^ " does not match"); + dltype, dltype + + in + let infer_lambda_body kind var def_arg_type body subst = + (* Check argument type annotation, if any. *) + let def_arg_type = match def_arg_type with + | Some def_arg_type + -> let def_arg_type, lasort = lexp_infer def_arg_type ctx in + elab_check_sort ctx lasort (Some var) def_arg_type; + Some def_arg_type + | _ -> None in + + (* Read var type from the provided type *) + let meta_ctx, _ = !global_substitution in + let given_arg_type, given_body_type = + match OL.lexp_whnf t (ectx_to_lctx ctx) meta_ctx with + | Arrow(kind, _, ltp, _, lbtp) + -> (match def_arg_type with + | None -> () + | Some def_arg_type + -> if not (OL.conv_p meta_ctx (ectx_to_lctx ctx) def_arg_type ltp) then + lexp_error (lexp_location def_arg_type) def_arg_type + ("Type mismatch! Context expected `" + ^ lexp_string ltp ^ "`\n")); + ltp, lbtp + | lxp -> unify_with_arrow lxp kind var def_arg_type subst in + + let nctx = env_extend ctx var Variable given_arg_type in + let lbody = lexp_check body given_body_type nctx in + mkLambda (kind, var, given_arg_type, lbody) + + in + let subst, _ = !global_substitution in match p with - (* This case cannot be inferred *) | Plambda (kind, var, def_arg_type, body) - -> (* Read var type from the provided type *) - let given_arg_type, given_body_type = match OL.lexp_whnf t (ectx_to_lctx ctx) with - | Arrow(kind, _, ltp, _, lbtp) -> ltp, lbtp - | expr -> - lexp_fatal tloc expr "Expected Type Arrow ( _ -> _ )" in - - (* Check argument type *) - let _ = match def_arg_type with - | Some def_arg_type - -> let def_arg_type, lasort = _lexp_p_infer def_arg_type ctx trace in - elab_check_sort ctx lasort (Some var) def_arg_type; - if not (OL.conv_p (ectx_to_lctx ctx) def_arg_type given_arg_type) then - lexp_error (lexp_location def_arg_type) def_arg_type - ("Type mismatch! Context expected `" - ^ lexp_string given_arg_type ^ "`\n") - | _ -> () in - - let nctx = env_extend ctx var Variable given_arg_type in - let lbody = lexp_check body given_body_type nctx in - - mkLambda(kind, var, given_arg_type, lbody) + -> infer_lambda_body kind var def_arg_type body subst
(* This is mostly for the case where no branches are provided *) | Pcase (loc, target, branches) @@ -389,13 +436,21 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : elab_context) trace: lexp = (* FIXME: Handle *macro* pcalls here! *) (* | Pcall (fname, _args) -> *)
- | _ -> let (e, inferred_t) = lexp_infer p ctx in - if not (OL.conv_p (ectx_to_lctx ctx) inferred_t t) then - lexp_error (pexp_location p) e - ("Type mismatch! Context expected `" - ^ lexp_string t ^ "` but expression has type `" - ^ lexp_string inferred_t ^ "`\n"); - e + | Pmetavar _ -> newMetavar t + + | _ -> lexp_p_infer_and_check p ctx t trace + +and lexp_p_infer_and_check pexp ctx t i = + let (e, inferred_t) = _lexp_p_infer pexp ctx i in + let subst, _ = !global_substitution in + (match Unif.unify inferred_t t (ectx_to_lctx ctx) subst with + | Some subst -> global_substitution := subst + | None + -> lexp_error (pexp_location pexp) e + ("Type mismatch! Context expected `" + ^ lexp_string t ^ "` but expression has type `" + ^ lexp_string inferred_t ^ "`\n")); + e
(* Lexp.case can sometimes be inferred, but we prefer to always check. *) and lexp_case rtype (loc, target, ppatterns) ctx i = @@ -417,14 +472,15 @@ and lexp_case rtype (loc, target, ppatterns) ctx i =
(* get target and its type *) let tlxp, tltp = lexp_infer target ctx in + let meta_ctx, _ = !global_substitution in (* FIXME: We need to be careful with whnf: while the output is equivalent * to the input, it's not necessarily as readable. So try to reuse the * "non-whnf" form whenever possible. *) - let call_split e = match (OL.lexp_whnf e (ectx_to_lctx ctx)) with + let call_split e = match (OL.lexp_whnf e (ectx_to_lctx ctx) meta_ctx) with | Call (f, args) -> (f, args) | _ -> (e,[]) in let it, targs = call_split tltp in - let constructors = match OL.lexp_whnf it (ectx_to_lctx ctx) with + let constructors = match OL.lexp_whnf it (ectx_to_lctx ctx) meta_ctx with | Inductive (_, _, fargs, constructors) -> assert (List.length fargs = List.length targs); constructors @@ -447,9 +503,10 @@ and lexp_case rtype (loc, target, ppatterns) ctx i = let add_branch pctor pargs = let loc = pexp_location pctor in let lctor, _ = _lexp_p_infer pctor ctx i in - match OL.lexp_whnf lctor (ectx_to_lctx ctx) with + let meta_ctx, _ = !global_substitution in + match OL.lexp_whnf lctor (ectx_to_lctx ctx) meta_ctx with | Cons (it', (_, cons_name)) - -> let _ = if OL.conv_p (ectx_to_lctx ctx) it' it then () + -> let _ = if OL.conv_p meta_ctx (ectx_to_lctx ctx) it' it then () else lexp_error loc lctor ("Expected pattern of type `" ^ lexp_string it ^ "` but got `" @@ -502,7 +559,9 @@ and lexp_case rtype (loc, target, ppatterns) ctx i = | Ppatany _ -> add_default None | Ppatsym ((_, name) as var) -> (try let idx = senv_lookup name ctx in - match OL.lexp_whnf (mkVar (var, idx)) (ectx_to_lctx ctx) with + let meta_ctx, _ = !global_substitution in + match OL.lexp_whnf (mkVar (var, idx)) + (ectx_to_lctx ctx) meta_ctx with | Cons _ (* It's indeed a constructor! *) -> add_branch (Pvar var) [] | _ -> add_default (Some var) (* A named default branch. *) @@ -518,6 +577,7 @@ and lexp_case rtype (loc, target, ppatterns) ctx i = (* Identify Call Type and return processed call *) and lexp_call (func: pexp) (sargs: sexp list) ctx i = let loc = pexp_location func in + let meta_ctx, _ = !global_substitution in
let lexp_infer p ctx = _lexp_p_infer p ctx i in let lexp_check p ltp ctx = _lexp_p_check p ltp ctx i in @@ -531,45 +591,70 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = let body, ltp = lexp_infer func ctx in let ltp = nosusp ltp in
- let rec handle_fun_args largs sargs ltp = match sargs with - | [] -> largs, ltp - | (Node (Symbol (_, "_:=_"), [Symbol (_, aname); sarg])) :: sargs + let rec handle_fun_args largs sargs pending ltp = + let ltp' = OL.lexp_whnf ltp (ectx_to_lctx ctx) meta_ctx in + match sargs, ltp' with + | _, Arrow (ak, Some (_, aname'), arg_type, _, ret_type) + when SMap.mem aname' pending + -> let sarg = SMap.find aname' pending in + let parg = pexp_parse sarg in + let larg = lexp_check parg arg_type ctx in + handle_fun_args ((ak, larg) :: largs) sargs + (SMap.remove aname' pending) + (L.mkSusp ret_type (S.substitute larg)) + + | [], _ + -> (if not (SMap.is_empty pending) then + let pending = SMap.bindings pending in + let loc = match pending with (_, sarg)::_ -> sexp_location sarg in + pexp_error loc func + ("Explicit actual args `" + ^ String.concat ", " (List.map (fun (l, _) -> l) + pending) + ^ "` have no matching formal args")); + largs, ltp + + | (Node (Symbol (_, "_:=_"), [Symbol (_, aname); sarg])) :: sargs, + Arrow (ak, Some (_, aname'), arg_type, _, ret_type) + when (aname = aname' || aname = "_") (* Explicit-implicit argument. *) - (* check if a = b in (a : Type) -> ... and (b := val) *) - -> (match OL.lexp_whnf ltp (ectx_to_lctx ctx) with - | Arrow (ak, Some (_, aname'), arg_type, _, ret_type) - when (aname = aname' || aname = "_") - -> let parg = pexp_parse sarg in - let larg = lexp_check parg arg_type ctx in - handle_fun_args ((ak, larg) :: largs) sargs - (L.mkSusp ret_type (S.substitute larg)) - - | _ -> fatal (sexp_location sarg) - ("Explicit arg `" ^ aname ^ "` to non-function " ^ - "(type = " ^ (lexp_string ltp) ^ ")")) - | sarg :: sargs - (* Process Argument *) - -> (match OL.lexp_whnf ltp (ectx_to_lctx ctx) with - | Arrow (Aexplicit, _, arg_type, _, ret_type) - -> let parg = pexp_parse sarg in - let larg = _lexp_p_check parg arg_type ctx i in - handle_fun_args ((Aexplicit, larg) :: largs) sargs - (L.mkSusp ret_type (S.substitute larg)) - | Arrow _ as t -> - debug_messages fatal (sexp_location sarg) "Expected non-explicit arg" [ - "ltype : " ^ (lexp_string t); - "s-exp arg: " ^ (sexp_string sarg);] - - | t -> - print_lexp_ctx (ectx_to_lctx ctx); - lexp_fatal (sexp_location sarg) t - ("Explicit arg `" ^ sexp_string sarg ^ - "` to non-function (type = " ^ lexp_string ltp ^ ")")) in + -> let parg = pexp_parse sarg in + let larg = lexp_check parg arg_type ctx in + handle_fun_args ((ak, larg) :: largs) sargs pending + (L.mkSusp ret_type (S.substitute larg)) + + | (Node (Symbol (_, "_:=_"), [Symbol (l, aname); sarg])) :: sargs, + Arrow _ + -> if SMap.mem aname pending then + sexp_error l ("Duplicate explicit arg `" ^ aname ^ "`"); + handle_fun_args largs sargs (SMap.add aname sarg pending) ltp + + | (Node (Symbol (_, "_:=_"), Symbol (l, aname) :: _)) :: sargs, _ + -> sexp_error l + ("Explicit arg `" ^ aname ^ "` to non-function " + ^ "(type = " ^ (lexp_string ltp) ^ ")"); + handle_fun_args largs sargs pending ltp + + | sarg :: sargs, Arrow (Aexplicit, _, arg_type, _, ret_type) + -> let parg = pexp_parse sarg in + let larg = _lexp_p_check parg arg_type ctx i in + handle_fun_args ((Aexplicit, larg) :: largs) sargs pending + (L.mkSusp ret_type (S.substitute larg)) + | sarg :: sargs, Arrow (kind, _, arg_type, _, ret_type) + -> let larg = newMetavar arg_type in + handle_fun_args ((kind, larg) :: largs) (sarg::sargs) pending + (L.mkSusp ret_type (S.substitute larg)) + + | sarg :: sargs, t -> + print_lexp_ctx (ectx_to_lctx ctx); + lexp_fatal (sexp_location sarg) t + ("Explicit arg `" ^ sexp_string sarg ^ + "` to non-function (type = " ^ lexp_string ltp ^ ")") in
let handle_funcall () = (* Here we use lexp_whnf on actual code, but it's OK * because we only use the result when it's a "predefined constant". *) - match OL.lexp_whnf body (ectx_to_lctx ctx) with + match OL.lexp_whnf body (ectx_to_lctx ctx) meta_ctx with | Builtin((_, "Built-in"), _) -> ( (* ------ SPECIAL ------ *) @@ -588,90 +673,9 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = | false, _ -> error loc "Use of `Built-in` in user code"; dlxp, dltype)
- | _ -> - (* Process Arguments *) - - (* Extract correct ordering aargs: all args and eargs: explicit args*) - let rec extract_order ltp aargs eargs nctx = - match OL.lexp_whnf ltp nctx with - | Arrow (kind, Some (_, varname), ltp, _, ret) -> - extract_order ret ((kind, varname, ltp)::aargs) - (if kind = Aexplicit then (varname::eargs) else eargs) (lctx_extend nctx None (ForwardRef) ltp) - - | e -> (List.rev aargs), List.rev eargs in - - (* first list has all the arguments, second only holds explicit arguments *) - let order, eorder = extract_order ltp [] [] (ectx_to_lctx ctx) in - - (* - print_string "Type :"; lexp_print ltp; print_string "\n"; - print_string "Order:"; List.iter (fun (_, b, _) -> print_string (b ^ " ")) (order); print_string "\n"; - print_string "Sarg1: "; - List.iter (fun lxp -> sexp_print lxp; print_string ", ") sargs; - print_string "\n";*) - - - (* from arg order build a dictionnary that will hold the defined args *) - let args_dict = List.fold_left - (fun map (kind, key, _) -> SMap.add key (kind, None) map) SMap.empty order in - - let args_dict, eargs = List.fold_left (fun (map, eargs) sexp -> - match sexp with - | Node (Symbol (_, "_:=_"), [Symbol (_, aname); sarg]) -> - let kind, _ = try SMap.find aname map - with Not_found -> - print_string (aname ^ " was not found" ^ "\n"); - Aerasable, None in - (SMap.add aname (kind, Some sarg) map), - (if kind = Aexplicit then - (match eargs with - | _::tl -> tl - | _ -> []) else eargs) - - | _ -> (match eargs with - | name::tl -> (SMap.add name (Aexplicit, Some sexp) map), tl - | _ -> map, [])) - (args_dict, eorder) sargs in - - - (* Generate an argument list with the correct order *) - let sargs2 = List.map (fun (_, name, ltp) -> - try match SMap.find name args_dict with - | Aimplicit, (Some sexp) -> Node (Symbol (dloc, "_:=_"), [Symbol (dloc, name); sexp]) - | Aerasable, Some sexp -> Node (Symbol (dloc, "_:=_"), [Symbol (dloc, name); sexp]) - | Aexplicit, (Some sexp) -> sexp - | Aexplicit, None -> fatal dloc "Explicit argument expected" - | Aimplicit, None -> ( - (* get variable info *) - let vidx, vname = match ltp with - | Var ((_, name), idx) -> idx, name - | _ -> lexp_fatal loc ltp "Unable to find default attribute" in - - (* get default property *) - let pidx, pname = (senv_lookup "default" ctx), "default" in - - (* get macro *) - let default_macro = try get_property ctx (vidx, vname) (pidx, pname) - with _ -> dump_properties ctx; dltype in - - lexp_print default_macro; - - print_string ((lexp_name ltp) ^ ": "); - lexp_print ltp; print_string "\n"; - fatal dloc "Default Arg lookup not implemented") - - - with Not_found -> fatal dloc (name ^ " not found") - ) order in - - (* - print_string "\nSarg2: "; List.iter (fun lxp -> sexp_print lxp; print_string ", ") sargs2; - print_string "\n"; *) - - (* check if we had enough information to reorder args *) - let sargs = if (List.length order >= List.length sargs) then sargs2 else sargs in - - let largs, ret_type = handle_fun_args [] sargs ltp in + | e -> + (* Process Arguments. *) + let largs, ret_type = handle_fun_args [] sargs SMap.empty ltp in mkCall (body, List.rev largs), ret_type in
let handle_macro_call () = @@ -689,14 +693,15 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i =
(* This is the builtin Macro type *) let macro_type, macro_disp = match get_predef_option "Macro" ctx with - | Some lxp -> OL.lexp_whnf lxp (ectx_to_lctx ctx), true + | Some lxp -> OL.lexp_whnf lxp (ectx_to_lctx ctx) meta_ctx, true (* When type.typer is being parsed and the predef is not yet available *) | None -> dltype, false in
(* determine function type *) match func, ltp with | macro, _ when (macro_disp - && OL.conv_p (ectx_to_lctx ctx) ltp macro_type) -> ( + && OL.conv_p meta_ctx (ectx_to_lctx ctx) + ltp macro_type) -> ( match macro with | Pvar(l, name) when is_builtin_macro name -> let pargs = List.map pexp_parse sargs in
===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -85,7 +85,9 @@ let rec lexp_defs_subst l s defs = match defs with * but only on *types*. If you must use it on code, be sure to use its * return value as little as possible since WHNF will inherently introduce * call-by-name behavior. *) -let rec lexp_whnf e (ctx : DB.lexp_context) = match e with +let lexp_whnf e (ctx : DB.lexp_context) meta_ctx : lexp = + let rec lexp_whnf e (ctx : DB.lexp_context) : lexp = + match e with | Var v -> (match lookup_value ctx v with | None -> e (* We can do this blindly even for recursive definitions! @@ -130,6 +132,9 @@ let rec lexp_whnf e (ctx : DB.lexp_context) = match e with | Cons (_, (_, name)) -> reduce name [] | Call (Cons (_, (_, name)), aargs) -> reduce name aargs | _ -> mkCase (l, e, rt, branches, default)) + | Metavar (idx, s, _, _) + -> (try lexp_whnf (mkSusp (L.VMap.find idx meta_ctx) s) ctx + with Not_found -> e)
(* FIXME: I'd really prefer to use "native" recursive substitutions, using * ideally a trick similar to the db_offsets in lexp_context! *) @@ -138,6 +143,8 @@ let rec lexp_whnf e (ctx : DB.lexp_context) = match e with
| e -> e
+ in lexp_whnf e ctx +
(** A very naive implementation of sets of lexps. *) type set_lexp = lexp list @@ -159,9 +166,10 @@ let set_shift s : set_lexp = set_shift_n s 1 (********* Testing if two types are "convertible" aka "equivalent" *********)
(* Returns true if e₁ and e₂ are equal (upto alpha/beta/...). *) -let rec conv_p' (ctx : DB.lexp_context) (vs : set_lexp) e1 e2 : bool = - let e1' = lexp_whnf e1 ctx in - let e2' = lexp_whnf e2 ctx in +let rec conv_p' meta_ctx (ctx : DB.lexp_context) (vs : set_lexp) e1 e2 : bool = + let conv_p' = conv_p' meta_ctx in + let e1' = lexp_whnf e1 ctx meta_ctx in + let e2' = lexp_whnf e2 ctx meta_ctx in let stop1 = not (e1 == e1') && set_member_p vs e1' in let stop2 = not (e2 == e2') && set_member_p vs e2' in let vs' = if not (e1 == e1') && not stop1 then set_add vs e1' @@ -226,9 +234,9 @@ let rec conv_p' (ctx : DB.lexp_context) (vs : set_lexp) e1 e2 : bool = then conv_p'' e1 e2 else conv_p'' e1' e2'
-let conv_p (ctx : DB.lexp_context) e1 e2 +let conv_p meta_ctx (ctx : DB.lexp_context) e1 e2 = if e1 == e2 then true - else conv_p' ctx set_empty e1 e2 + else conv_p' meta_ctx ctx set_empty e1 e2
(********* Testing if a lexp is properly typed *********)
@@ -263,8 +271,8 @@ let sort_compose l s1 s2 = StypeOmega)
(* "check ctx e" should return τ when "Δ ⊢ e : τ" *) -let rec check ctx e = - (* let mustfind = assert_type e t in *) +let rec check meta_ctx ctx e = + let check = check meta_ctx in match e with | Imm (Float (_, _)) -> B.type_float | Imm (Integer (_, _)) -> B.type_int @@ -287,7 +295,7 @@ let rec check ctx e = | Let (_, defs, e) -> let tmp_ctx = List.fold_left (fun ctx (v, e, t) - -> (match lexp_whnf (check ctx t) ctx with + -> (match lexp_whnf (check ctx t) ctx meta_ctx with | Sort (_, Stype _) -> () | _ -> (U.msg_error "TC" (lexp_location t) "Def type is not a type!"; ())); @@ -304,7 +312,7 @@ let rec check ctx e = -> (let k1 = check ctx t1 in let nctx = DB.lexp_ctx_cons ctx 0 v Variable t1 in let k2 = check nctx t2 in - match lexp_whnf k1 ctx, lexp_whnf k2 nctx with + match lexp_whnf k1 ctx meta_ctx, lexp_whnf k2 nctx meta_ctx with | (Sort (_, s1), Sort (_, s2)) -> if ak == P.Aerasable && impredicative_erase then k2 else Sort (l, sort_compose l s1 s2) @@ -315,7 +323,7 @@ let rec check ctx e = "Not a proper type"; Sort (l, StypeOmega))) | Lambda (ak, ((l,_) as v), t, e) - -> ((match lexp_whnf (check ctx t) ctx with + -> ((match lexp_whnf (check ctx t) ctx meta_ctx with | Sort _ -> () | _ -> (U.msg_error "TC" (lexp_location t) "Formal arg type is not a type!"; ())); @@ -327,7 +335,7 @@ let rec check ctx e = -> let ft = check ctx f in List.fold_left (fun ft (ak,arg) -> let at = check ctx arg in - match lexp_whnf ft ctx with + match lexp_whnf ft ctx meta_ctx with | Arrow (ak', v, t1, l, t2) -> if not (ak == ak') then (U.msg_error "TC" (lexp_location arg) @@ -350,7 +358,7 @@ let rec check ctx e = let level, _ = List.fold_left (fun (level, ctx) (ak, v, t) -> - (match lexp_whnf (check ctx t) ctx with + (match lexp_whnf (check ctx t) ctx meta_ctx with | Sort _ when ak == P.Aerasable && impredicative_erase -> level | Sort (_, Stype level') @@ -379,9 +387,9 @@ let rec check ctx e = -> let rec call_split e = match e with | Call (f, args) -> (f, args) | _ -> (e,[]) in - let etype = lexp_whnf (check ctx e) ctx in + let etype = lexp_whnf (check ctx e) ctx meta_ctx in let it, aargs = call_split etype in - (match lexp_whnf it ctx, aargs with + (match lexp_whnf it ctx meta_ctx, aargs with | Inductive (_, _, fargs, constructors), aargs -> let rec mksubst s fargs aargs = match fargs, aargs with @@ -422,7 +430,7 @@ let rec check ctx e = | _,_ -> U.msg_error "TC" l "Case on a non-inductive type!"); ret | Cons (t, (_, name)) - -> (match lexp_whnf t ctx with + -> (match lexp_whnf t ctx meta_ctx with | Inductive (l, _, fargs, constructors) as it -> let fieldtypes = SMap.find name constructors in let rec indtype fargs start_index = @@ -447,6 +455,9 @@ let rec check ctx e = | _ -> (U.msg_error "TC" (lexp_location e) "Cons of a non-inductive type!"; B.type_int)) + | Metavar (idx, s, _, t) + -> try check ctx (push_susp (L.VMap.find idx meta_ctx) s) + with Not_found -> t
(*********** Type erasure, before evaluation. *****************)
===================================== src/prelexer.ml ===================================== --- a/src/prelexer.ml +++ b/src/prelexer.ml @@ -50,7 +50,7 @@ let string_sub str b e = String.sub str b (e - b)
let inc_cp (cp:charpos) (c:char) = (* Count char positions in utf-8: don't count the non-leading bytes. *) - if (Char.code c < 128 || Char.code c >= 192) then cp+1 else cp + if utf8_head_p c then cp+1 else cp
let rec prelex (file : string) (getline : unit -> string) ln ctx acc : pretoken list =
===================================== src/unification.ml ===================================== --- /dev/null +++ b/src/unification.ml @@ -0,0 +1,358 @@ +(* unification.ml --- Unification of Lexp terms + +Copyright (C) 2016 Free Software Foundation, Inc. + +Author: Vincent Bonnevalle tiv.crb@gmail.com + +This file is part of Typer. + +Typer is free software; you can redistribute it and/or modify it under the +terms of the GNU General Public License as published by the Free Software +Foundation, either version 3 of the License, or (at your option) any +later version. + +Typer is distributed in the hope that it will be useful, but WITHOUT ANY +WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS +FOR A PARTICULAR PURPOSE. See the GNU General Public License for +more details. + +You should have received a copy of the GNU General Public License along with +this program. If not, see http://www.gnu.org/licenses/. *) + +(* FIXME: Needs occurs-check. + * Also needs to add a notion of scope-level, as described in + * http://okmij.org/ftp/ML/generalization.html (aka ranks in + * ftp://ftp.inria.fr/INRIA/Projects/cristal/Didier.Remy/eq-theory-on-types.ps.gz) + *) + +open Lexp +(* open Sexp *) +(* open Inverse_subst *) +module OL = Opslexp +module DB = Debruijn + +(** Provide unify function for unifying two Lambda-Expression *) + +(* :-( *) +let global_last_metavar = ref (-1) (*The first metavar is 0*) + +let create_metavar () = global_last_metavar := !global_last_metavar + 1; + !global_last_metavar + +(* For convenience *) +type return_type = (meta_subst * constraints) option + +(** Alias for VMap.add*) +let associate (meta: int) (lxp: lexp) (subst: meta_subst) + : meta_subst = + (VMap.add meta lxp subst) + +(** If key is in map returns the value associated + else returns <code>None</code> +*) +let find_or_none (value: lexp) (map: meta_subst) : lexp option = + match value with + | Metavar (idx, _, _, _) + -> if VMap.mem idx map + then Some (VMap.find idx map) + else None + | _ -> None + +(** + lexp is equivalent to _ in ocaml + (Let , lexp) == (lexp , Let) + UNIFY -> recursive call or dispatching + OK -> add a substituion to the list of substitution + CONSTRAINT -> returns a constraint +*) + +let unify_and res op = match res with + | None -> None + | Some (subst, constraints1) + -> match op subst with + | None -> None + | Some (subst, constraints2) -> Some (subst, constraints2@constraints1) + +(****************************** Top level unify *************************************) + +(** Dispatch to the right unifyer. + + If (<code>_unify_X X Y</code>) don't handle the case <b>(X, Y)</b>, it call (<code>unify Y X</code>) + + The metavar unifyer is the end rule, it can't call unify with it's parameter (changing their order) +*) +let rec unify (e1: lexp) (e2: lexp) + (ctx : DB.lexp_context) (subst: meta_subst) + : return_type = + unify' e1 e2 ctx OL.set_empty subst + +and unify' (e1: lexp) (e2: lexp) + (ctx : DB.lexp_context) (vs : OL.set_lexp) (subst: meta_subst) + : return_type = + let e1' = OL.lexp_whnf e1 ctx subst in + let e2' = OL.lexp_whnf e2 ctx subst in + let stop1 = not (e1 == e1') && OL.set_member_p vs e1' in + let stop2 = not (e2 == e2') && OL.set_member_p vs e2' in + let vs' = if not (e1 == e1') && not stop1 then OL.set_add vs e1' + else if not (e2 == e2') && not stop2 then OL.set_add vs e2' + else vs in + match if stop1 || stop2 then (e1, e2) else (e1', e2') with + | ((Imm _, Imm _) | (Cons _, Cons _) | (Builtin _, Builtin _) + | (Var _, Var _) | (Inductive _, Inductive _)) + -> if OL.conv_p subst ctx e1' e2' then Some (subst, []) else None + | (l, (Metavar _ as r)) -> _unify_metavar r l subst + | (l, (Call _ as r)) -> _unify_call r l ctx vs' subst + (* | (l, (Case _ as r)) -> _unify_case r l subst *) + | (Arrow _ as l, r) -> _unify_arrow l r ctx vs' subst + | (Lambda _ as l, r) -> _unify_lambda l r ctx vs' subst + | (Metavar _ as l, r) -> _unify_metavar l r subst + | (Call _ as l, r) -> _unify_call l r ctx vs' subst + (* | (Case _ as l, r) -> _unify_case l r subst *) + (* | (Inductive _ as l, r) -> _unify_induct l r subst *) + | (Sort _ as l, r) -> _unify_sort l r ctx vs' subst + | (SortLevel _ as l, r) -> _unify_sortlvl l r ctx vs' subst + | _ -> Some (subst, + if OL.conv_p subst ctx e1' e2' then [] else [(e1, e2)]) + +(********************************* Type specific unify *******************************) + +(** Unify a Arrow and a lexp if possible + - (Arrow, Arrow) -> if var_kind = var_kind + then unify ltype & lexp (Arrow (var_kind, _, ltype, lexp)) + else None + - (Arrow, Var) -> Constraint + - (_, _) -> None +*) +and _unify_arrow (arrow: lexp) (lxp: lexp) ctx vs (subst: meta_subst) + : return_type = + match (arrow, lxp) with + | (Arrow (var_kind1, v1, ltype1, _, lexp1), + Arrow (var_kind2, _, ltype2, _, lexp2)) + -> if var_kind1 = var_kind2 + then unify_and (unify' ltype1 ltype2 ctx vs subst) + (unify' lexp1 lexp2 + (DB.lexp_ctx_cons ctx 0 v1 Variable ltype1) + (OL.set_shift vs)) + else None + | (Arrow _, Imm _) -> None + | (Arrow _, Var _) -> Some (subst, [(arrow, lxp)]) + | (Arrow _, _) -> unify' lxp arrow ctx vs subst + | (_, _) -> None + +(** Unify a Lambda and a lexp if possible + - Lamda , Lambda -> if var_kind = var_kind + then UNIFY ltype & lxp else ERROR + - Lambda , Var -> CONSTRAINT + - Lambda , Call -> Constraint + - Lambda , Let -> Constraint + - Lambda , lexp -> unify lexp lambda subst +*) +and _unify_lambda (lambda: lexp) (lxp: lexp) ctx vs (subst: meta_subst) : return_type = + match (lambda, lxp) with + | (Lambda (var_kind1, v1, ltype1, lexp1), + Lambda (var_kind2, _, ltype2, lexp2)) + -> if var_kind1 = var_kind2 + then unify_and (unify' ltype1 ltype2 ctx vs subst) + (unify' lexp1 lexp2 + (DB.lexp_ctx_cons ctx 0 (Some v1) Variable ltype1) + (OL.set_shift vs)) + else None + | (Lambda _, Var _) -> Some ((subst, [(lambda, lxp)])) + | (Lambda _, Let _) -> Some ((subst, [(lambda, lxp)])) + | (Lambda _, Arrow _) -> None + | (Lambda _, Call _) -> Some ((subst, [(lambda, lxp)])) + | (Lambda _, Imm _) -> None + | (Lambda _, _) -> unify' lxp lambda ctx vs subst + | (_, _) -> None + +(** Unify a Metavar and a lexp if possible + - lexp , {metavar <-> none} -> UNIFY + - lexp , {metavar <-> lexp} -> UNFIFY lexp subst[metavar] + - metavar , metavar -> if Metavar = Metavar then OK else ERROR + - metavar , lexp -> OK +*) +and _unify_metavar (meta: lexp) (lxp: lexp) (subst: meta_subst) : return_type = + let find_or_unify metavar value lxp s = + match find_or_none metavar s with + | Some (lxp_) -> assert false + | None -> (match metavar with + | Metavar (_, subst_, _, _) -> (match Inverse_subst.inverse subst_ with + | Some s' -> Some (associate value (mkSusp lxp s') s, []) + | None -> None) + | _ -> None) + in + match (meta, lxp) with + | (Metavar (val1, s1, _, _), Metavar (val2, s2, _, _)) when val1 = val2 + (* FIXME: handle the case where s1 != s2 !! *) + -> Some ((subst, [])) + | (Metavar (v, s1, _, _), _) -> find_or_unify meta v lxp subst + | (_, _) -> None + +(** Unify a Call (call) and a lexp (lxp) + - Call , Call -> UNIFY + - Call , lexp -> CONSTRAINT +*) +and _unify_call (call: lexp) (lxp: lexp) ctx vs (subst: meta_subst) + : return_type = + match (call, lxp) with + | (Call (lxp_left, lxp_list1), Call (lxp_right, lxp_list2)) + when OL.conv_p subst ctx lxp_left lxp_right + -> List.fold_left (fun op ((ak1, e1), (ak2, e2)) subst + -> if ak1 == ak2 then + unify_and (unify' e1 e2 ctx vs subst) op + else None) + (fun subst -> Some (subst, [])) + (List.combine lxp_list1 lxp_list2) + subst + | (Call _, _) -> Some ((subst, [(call, lxp)])) + | (_, _) -> None + +(** Unify a Case with a lexp + - Case, Case -> try to unify + - Case, _ -> Constraint +*) +(* and _unify_case (case: lexp) (lxp: lexp) (subst: meta_subst) : return_type = + * let merge (_, const) subst_res = match subst_res with + * | None -> None + * | Some (s', c') -> Some (s', const@c') + * in + * let match_unify_inner lst smap1 smap2 subst = + * match _unify_inner lst subst with + * | None -> None + * | Some (s, c) -> merge (s, c) (_unify_inner_case (zip (SMap.bindings smap1) (SMap.bindings smap2)) s) + * in + * let match_lxp_opt lxp_opt1 lxp_opt2 tail smap1 smap2 subst = + * match lxp_opt1, lxp_opt2 with + * | Some (_, lxp1), Some (_, lxp2) + * -> match_unify_inner ((lxp1, lxp2)::tail) smap1 smap2 subst + * | _, _ -> None + * in + * match (case, lxp) with + * | (Case (_, lxp, lt12, smap, lxpopt), Case (_, lxp2, lt22, smap2, lxopt2)) + * -> match_lxp_opt lxpopt lxopt2 ((lt12, lt22)::[]) smap smap2 subst + * | (Case _, _) -> Some (subst, [(case, lxp)]) + * | (_, _) -> None *) + +(** Unify a Inductive and a lexp + - Inductive, Inductive -> try unify + - Inductive, Var -> constraint + - Inductive, Call/Metavar/Case/Let -> constraint + - Inductive, _ -> None +*) +(* and _unify_induct (induct: lexp) (lxp: lexp) (subst: meta_subst) : return_type = + * let transform (a, b, c) (d, e, f) = ((a, Some b, c), (d, Some e, f)) + * and merge map1 map2 (subst, const) : return_type = + * match (_unify_induct_sub_list (SMap.bindings map1) (SMap.bindings map2) subst) with + * | Some (s', c') -> Some (s', const@c') + * | None -> None + * in + * let zip_unify lst subst map1 map2 : return_type = + * match _unify_inner_induct lst subst with + * | None -> None + * | Some (s, c) -> merge map1 map2 (s, c) + * in + * match (induct, lxp) with + * | (Inductive (_, lbl1, farg1, m1), Inductive (_, lbl2, farg2, m2)) when lbl1 = lbl2 -> + * (match zip_map farg1 farg2 transform with + * | Some [] -> Some (subst, []) + * | Some lst -> zip_unify lst subst m1 m2 + * | None -> None) + * | (Inductive _, Var _) -> Some (subst, [(induct, lxp)]) + * | (_, _) -> None *) + +(** Unify a SortLevel with a lexp + - SortLevel, SortLevel -> if SortLevel ~= SortLevel then OK else ERROR + - SortLevel, _ -> ERROR +*) +and _unify_sortlvl (sortlvl: lexp) (lxp: lexp) ctx vs (subst: meta_subst) : return_type = + match sortlvl, lxp with + | (SortLevel s, SortLevel s2) -> (match s, s2 with + | SLz, SLz -> Some (subst, []) + | SLsucc l1, SLsucc l2 -> unify' l1 l2 ctx vs subst + | _, _ -> None) + | _, _ -> None + +(** Unify a Sort and a lexp + - Sort, Sort -> if Sort ~= Sort then OK else ERROR + - Sort, Var -> Constraint + - Sort, lexp -> ERROR +*) +and _unify_sort (sort_: lexp) (lxp: lexp) ctx vs (subst: meta_subst) : return_type = + match sort_, lxp with + | (Sort (_, srt), Sort (_, srt2)) -> (match srt, srt2 with + | Stype lxp1, Stype lxp2 -> unify' lxp1 lxp2 ctx vs subst + | StypeOmega, StypeOmega -> Some (subst, []) + | StypeLevel, StypeLevel -> Some (subst, []) + | _, _ -> None) + | Sort _, Var _ -> Some (subst, [(sort_, lxp)]) + | _, _ -> None + +(************************ Helper function **************************************) + +(***** for Case *****) +(** Check arg_king in <code>(arg_kind * vdef option) list </code> in Case *) +and is_same arglist arglist2 = + match arglist, arglist2 with + | (akind, _)::t1, (akind2, _)::t2 when akind = akind2 -> is_same t1 t2 + | [], [] -> true + | _, _ -> false + +(** try to unify the SMap part of the case *) +(* and _unify_inner_case lst subst = + * let merge (_, c) res = + * match res with + * | Some (s', c') -> Some (s', c@c') + * | None -> None + * in + * let rec _unify_inner_case list_ subst = + * match list_ with + * | ((key, (_, arglist, lxp)), (key2, (_, arglist2, lxp2)))::tail when key = key2 -> + * (if is_same arglist arglist2 + * then ( match unify lxp lxp2 subst with + * | Some (s', c) -> merge (s', c) (_unify_inner_case tail s') + * | None -> None) + * else None) + * | [] -> Some (subst, []) + * | _ -> None + * in (match lst with + * | Some [] -> Some (subst, []) + * | None -> None + * | Some l -> _unify_inner_case l subst) *) + +(***** for Inductive *****) +(** for _unify_induct : unify the formal arg*) +(* and _unify_inner_induct lst subst : return_type = + * let test ((a1, _, l1), (a2, _, l2)) subst : return_type = + * if a1 = a2 then unify l1 l2 subst + * else None + * in + * List.fold_left (fun a e -> + * (match a with + * | Some (s, c) -> + * (match test e s with + * | Some (s1, c1) -> Some (s1, c1@c) + * | None -> Some (s, c)) + * | None -> test e subst) + * ) None lst *) + +(** unify the SMap of list in Inductive *) +(* and _unify_induct_sub_list l1 l2 subst = + * let test l1 l2 subst = + * let merge l1 l2 subst (s, c) = + * match (_unify_induct_sub_list l1 l2 subst) with + * | Some (s1, c1) -> Some (s1, c1@c) + * | None -> Some (s, c) + * in + * let unify_zip lst t1 t2 = match _unify_inner_induct lst subst with + * | Some (s, c) -> merge l1 l2 subst (s, c) + * | None -> (_unify_induct_sub_list t1 t2 subst) + * in + * match l1, l2 with + * | (k1, v1)::t1, (k2, v2)::t2 when k1 = k2 -> + * (match zip v1 v2 with + * | Some [] -> Some (subst, []) + * | Some lst -> unify_zip lst t1 t2 + * | None -> None) + * | _, _ -> None + * in test l1 l2 subst *) +
===================================== src/util.ml ===================================== --- a/src/util.ml +++ b/src/util.ml @@ -118,3 +118,27 @@ let str_split str sep = ret := (Buffer.contents buffer)::(!ret));
List.rev (!ret)) + +let utf8_head_p (c : char) : bool + = Char.code c < 128 || Char.code c >= 192 + +(* Display size of `str`, assuming the byte-sequence is UTF-8. + * Very naive: doesn't pay attention to LF, TABs, double-width chars, ... *) +let string_width (s : string) : int = + let rec width i w = + if i < 0 then w + else width (i - 1) + (if utf8_head_p (String.get s i) + then w + 1 + else w) in + width (String.length s - 1) 0 + +let padding_right (str: string ) (dim: int ) (char_: char) : string = + let diff = (dim - string_width str) + in let rpad = max diff 0 + in str ^ (String.make rpad char_) + +let padding_left (str: string ) (dim: int ) (char_: char) : string = + let diff = (dim - string_width str) + in let lpad = max diff 0 + in (String.make lpad char_) ^ str
===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -248,16 +248,16 @@ let _ = test_eval_eqv_named let _ = test_eval_eqv_named "Lists"
- "my_list = cons (a := Int) 1 - (cons (a := Int) 2 - (cons (a := Int) 3 - (cons (a := Int) 4 (nil (a := Int)))))" + "my_list = cons 1 + (cons 2 + (cons 3 + (cons 4 (nil (a := Int)))))"
- "length (a := Int) my_list; - head (a := Int) my_list; - head (a := Int) (tail (a := Int) my_list)" + "length my_list; + head my_list; + head (tail my_list)"
- "4; Some (a := Int) 1; Some (a := Int) 2" + "4; Some 1; Some 2"
(* * Special forms @@ -309,7 +309,7 @@ let _ = (add_test "EVAL" "Monads" (fun () ->
let rctx, lctx = eval_decl_str dcode lctx rctx in
- let rcode = "run-io (a := Unit) (b := Int) c 2" in + let rcode = "run-io c 2" in
(* Eval defined lambda *) let ret = eval_expr_str rcode lctx rctx in @@ -326,13 +326,12 @@ let _ = test_eval_eqv_named lambda (z : Int) -> x * y + z;"
"fun (x := 3) 2 1; - %% fun (x := 3) (z := 1) 2; + fun (x := 3) (z := 1) 4; fun (z := 3) (y := 2) (x := 1); fun (z := 1) (y := 2) (x := 3); fun (x := 3) (y := 2) (z := 1);"
- "7; %% 7; - 5; 7; 7" + "7; 13; 5; 7; 7"
let _ = test_eval_eqv_named
===================================== tests/inverse_test.ml ===================================== --- /dev/null +++ b/tests/inverse_test.ml @@ -0,0 +1,176 @@ +(* inverse_test.ml --- Test the substitution-inversion algorithm + * + * Copyright (C) 2016 Free Software Foundation, Inc. + * + * Author: Vincent Bonnevalle tiv.crb@gmail.com + * + * This file is part of Typer. + * + * Typer is free software; you can redistribute it and/or modify it under the + * terms of the GNU General Public License as published by the Free Software + * Foundation, either version 3 of the License, or (at your option) any + * later version. + * + * Typer is distributed in the hope that it will be useful, but WITHOUT ANY + * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS + * FOR A PARTICULAR PURPOSE. See the GNU General Public License for + * more details. + * + * You should have received a copy of the GNU General Public License along + * with this program. If not, see http://www.gnu.org/licenses/. + * + * -------------------------------------------------------------------------- *) + +open Sexp +open Pexp +open Lexp +open Unification +open Inverse_subst + +open Lparse (* add_def *) + +open Utest_lib + +open Fmt + +open Builtin +open Env + +open Str + +open Debug + +let mkShift2 shift subst = + S.mkShift subst shift + +let rec mkTestSubst lst = + match lst with + | (var, shift)::tail -> S.cons (mkVar var) + (mkShift2 shift (mkTestSubst tail)) + | [] -> S.identity + +(*TODO better checking of where it should fail*) +let input = + ((mkTestSubst ((0, 3)::(2, 2)::(3, 5)::[])), true):: + ((mkTestSubst ((1, 3)::(2, 2)::(3, 5)::[])), true):: + ((mkTestSubst ((1, 3)::(2, 2)::(4, 5)::[])), true):: + ((mkTestSubst ((0, 3)::(2, 2)::(4, 5)::[])), true):: + ((mkTestSubst ((0, 3)::(1, 2)::(4, 5)::[])), true):: + ((mkTestSubst ((0, 3)::(1, 2)::(4, 1)::(5, 5)::[])), false):: + ((S.cons (mkVar 1) (S.shift 3)), true):: + ((S.cons (mkVar 1) (S.cons (mkVar 3) (S.identity))), false):: + ((S.mkShift (S.shift 3) 4), true):: + ((S.mkShift (S.cons (mkVar 1) (S.identity)) 5), false):: + ((mkTestSubst ((4, 0)::(2, 2)::(3, 5)::[])), true):: + ((mkTestSubst ((1, 2)::(5, 1)::(3, 5)::[])), true):: + ((mkTestSubst ((1, 2)::(5, 2)::(3, 5)::[])), false):: + ((mkTestSubst ((0, 3)::(1, 2)::(4, 1)::(9, 5)::[])), false):: + [] + +let is_identity s = + let rec is_identity s acc = + match s with + | S.Cons(Var(_, idx), s1) when idx = acc -> is_identity s1 (acc + 1) + | S.Shift(S.Identity, shift) -> (acc = shift) + | S.Identity -> true + | _ -> false + in is_identity s 0 + +let generateRandInput shiftMax numberOfTest = + Random.self_init (); + let rec generateList shiftMax numberOfTest = + let rec generateRandInput shiftMax idx acc = + if idx < shiftMax + then (if Random.bool () + then ( let r = Random.int shiftMax in + let shift = (min (r + idx + 1) (shiftMax)) + in let shift = shift + (max 0 ((idx + shift) - acc)) + in (idx, shift)::(generateRandInput shiftMax (idx + 1) (shift + acc)) ) + else generateRandInput shiftMax (idx + 1) acc) + else [] + in if numberOfTest >= 0 + then (mkTestSubst (generateRandInput shiftMax 0 0))::(generateList shiftMax (numberOfTest - 1)) + else [] + in generateList shiftMax numberOfTest + +let lxp = mkVar 3 + +let test + (input_gen: (unit -> 'a list)) + (fmt: 'b list -> string list) + (tester: 'a -> ('b * bool)): (string * bool) list = + let input = List.map tester (input_gen ()) + in let str = List.map (fun (s, _) -> s ) input + in let b = List.map (fun (_, b) -> b) input + in List.combine (fmt str) b + +let generate_tests (name: string) + (input_gen: (unit -> 'a list)) + (fmt: 'b list -> string list) + (tester: 'a -> ('b * bool)) = + let idx = (ref 0) + in List.map (fun (sub, res) -> + idx := !idx + 1; + add_test name + ((U.padding_left (string_of_int (!idx)) 2 '0') ^ " - " ^ sub) + (fun () -> if res then success () else failure ())) + (test input_gen fmt tester) + + +let get_dim lst = + let max i s = max i (String.length s) + in + List.fold_left + (fun (acs, acs', acc) (s, s', comp) -> ((max acs s), (max acs' s'), (max acc comp))) + (0,0,0) + lst + +let fmt_res str = + let (ds, ds', dcomp) = get_dim str + in List.map (fun (s, s', com) -> (U.padding_right s ds ' ') ^ " -> " + ^ (U.padding_right s' ds' ' ') ^ " = " + ^ com) + str + +let get_dim lst = + let max i s = max i (String.length s) + in + List.fold_left + (fun (acs, acs', acc) (s, s', comp) -> ((max acs s), (max acs' s'), (max acc comp))) + (0,0,0) + lst + + +let _ = generate_tests "INVERSION" + (fun () -> input) + fmt_res + (fun (s, b) -> ( match inverse s with + | Some (s') -> (let comp = scompose s s' in + let ret = (is_identity comp) in + let str = (subst_string s, subst_string s', + subst_string comp) in + (str, ret)) + | None -> ((subst_string s, "None", "None"), not b) + ) + ) + +let fmt_res str = + List.map (fun (s, s', com) -> (s) ^ " -> " ^ + (s') ^ " = " ^ + (com) ) str + +(* TODO find a better way to check test*) +let _ = generate_tests "INVERSION-RAND" + (fun () -> generateRandInput 5 10) + fmt_res + (fun (s) -> ( match inverse s with + | Some (s') -> (let comp = scompose s s' in + let ret = (is_identity comp) in + let str = (subst_string s, + subst_string s', + subst_string comp) in + (str, ret)) + | None -> ((subst_string s , "None" , "None") , false) + )) + +let _ = run_all ()
===================================== tests/lparse_test.ml ===================================== --- /dev/null +++ b/tests/lparse_test.ml @@ -0,0 +1,141 @@ +(* lparse_test.ml --- + * + * Copyright (C) 2016 Free Software Foundation, Inc. + * + * Author: Vincent Bonnevalle tiv.crb@gmail.com + * + * This file is part of Typer. + * + * Typer is free software; you can redistribute it and/or modify it under the + * terms of the GNU General Public License as published by the Free Software + * Foundation, either version 3 of the License, or (at your option) any + * later version. + * + * Typer is distributed in the hope that it will be useful, but WITHOUT ANY + * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS + * FOR A PARTICULAR PURPOSE. See the GNU General Public License for + * more details. + * + * You should have received a copy of the GNU General Public License along + * with this program. If not, see http://www.gnu.org/licenses/. + * + * -------------------------------------------------------------------------- *) + + +open Lparse +open Utest_lib + +open Pexp +open Lexp + +open Builtin + +let test + (input_gen: (unit -> 'a list)) + (fmt: 'b list -> string list) + (tester: 'a -> ('b * bool)): (string * bool) list = + let input = List.map tester (input_gen ()) + in let str = List.map (fun (s, _) -> s ) input + in let b = List.map (fun (_, b) -> b) input + in List.combine (fmt str) b + +let generate_tests (name: string) + (input_gen: (unit -> 'a list)) + (fmt: 'b list -> string list) + (tester: 'a -> ('b * bool)) = + let idx = (ref 0) + in List.map (fun (sub, res) -> + idx := !idx + 1; + add_test name + ((U.padding_left (string_of_int (!idx)) 2 '0') ^ " - " ^ sub) + (fun () -> if res then success () else failure ())) + (test input_gen fmt tester) + +(* let input = "y = lambda x -> x + 1;" *) +let input = "id = lambda (α : Type) ≡> lambda (x : α) -> x; +res = id 3;" + +let generate_lexp_from_str str = + List.hd ((fun (lst, _) -> + (List.map + (fun (_, lxp, _) -> lxp)) + (List.flatten lst)) + (lexp_decl_str str default_lctx)) + +let _ = generate_tests + "TYPECHECK" + (fun () -> [generate_lexp_from_str input]) + (fun x -> List.map lexp_string x) + (fun x -> (x, true)) + +let lctx = default_lctx +(* let _ = (add_test "TYPECHEK_LEXP" "lexp_print" (fun () -> + * + * let dcode = " + * sqr = lambda (x) -> x * x; + * cube = lambda (x) -> x * (sqr x); + * + * mult = lambda (x) -> lambda (y) -> x * y; + * + * twice = (mult 2); + * + * let_fun = lambda (x) -> + * let a = (twice x); b = (mult 2 x); in + * a + b;" in + * + * let ret1, _ = lexp_decl_str dcode lctx in + * + * let to_str decls = + * let str = _lexp_str_decls (!compact_ppctx) (List.flatten ret1) in + * List.fold_left (fun str lxp -> str ^ lxp) "" str in + * + * (* Cast to string *) + * let str1 = to_str ret1 in + * + * print_string str1; + * + * (* read code again *) + * let ret2, _ = lexp_decl_str str1 lctx in + * + * (* Cast to string *) + * let str2 = to_str ret2 in + * + * if str1 = str2 then success () else failure () + * )) *) + +(* +let set_to_list s = + StringSet.fold (fun g a -> g::a) s [] + +let _ = (add_test "LEXP" "Free Variable" (fun () -> + + let dcode = " + a = 2; + b = 3; + f = lambda n -> (a + n); % a is a fv + g = lambda x -> ((f b) + a + x); % f,a,b are fv + " in + + let ret = pexp_decl_str dcode in + let g = match List.rev ret with + | (_, g, _)::_ -> g + | _ -> raise (Unexpected_result "Unexpected empty list") in + + let (bound, free) = free_variable g in + + let bound = set_to_list bound in + let (free, _) = free in + + match bound with + | ["x"] ->( + match free with + | ["_+_"; "f"; "b"; "a"] -> success () + | _ -> failure ()) + | _ -> failure () + +)) *) + +(* run all tests *) +let _ = run_all () + +let _ = run_all ()
===================================== tests/unify_test.ml ===================================== --- /dev/null +++ b/tests/unify_test.ml @@ -0,0 +1,231 @@ +(* unify_test.ml --- Test the unification algorithm + * + * Copyright (C) 2016 Free Software Foundation, Inc. + * + * Author: Vincent Bonnevalle tiv.crb@gmail.com + * + * This file is part of Typer. + * + * Typer is free software; you can redistribute it and/or modify it under the + * terms of the GNU General Public License as published by the Free Software + * Foundation, either version 3 of the License, or (at your option) any + * later version. + * + * Typer is distributed in the hope that it will be useful, but WITHOUT ANY + * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS + * FOR A PARTICULAR PURPOSE. See the GNU General Public License for + * more details. + * + * You should have received a copy of the GNU General Public License along + * with this program. If not, see http://www.gnu.org/licenses/. + * + * -------------------------------------------------------------------------- *) + +open Sexp +open Pexp +open Lexp +open Unification + +open Lparse (* add_def *) + +open Utest_lib + +open Fmt + +open Builtin +open Env + +open Str + +open Debug + +type result = + | Constraint + | Unification + | Equivalent + | Nothing + +type unif_res = (result * (meta_subst * constraints) option * lexp * lexp) + +type triplet = string * string * string + +let string_of_result r = + match r with + | Constraint -> "Constraint" + | Unification -> "Unification" + | Equivalent -> "Equivalent" + | Nothing -> "Nothing" + +let max_dim (lst: (string * string * string * string) list): (int * int * int *int) = + let max i l = max i (String.length l) + in List.fold_left + (fun (la, ca1, ca2, ra) (l, c1, c2, r) -> ((max la l), (max ca1 c1), (max ca2 c2), (max ra r))) + (0, 0, 0, 0) + lst + +let fmt (lst: (lexp * lexp * result * result) list): string list = + let str_lst = List.map + (fun (l1, l2, r1, r2) -> ((lexp_string l1), (lexp_string l2), (string_of_result r1), (string_of_result r2))) + lst + in let l, c1, c2, r = max_dim str_lst + in List.map (fun (l1, l2, r1, r2) -> (U.padding_right l1 l ' ') + ^ ", " + ^ (U.padding_right l2 c1 ' ') + ^ " -> got: " + ^ (U.padding_right r2 r ' ') + ^ " expected: " + ^ (U.padding_right r1 c2 ' ') + ) str_lst + +(* Inputs for the test *) +let str_induct = "Nat : Type; Nat = inductive_ (dNat) (zero) (succ Nat)" +let str_int_3 = "i = 3" +let str_int_4 = "i = 4" +let str_case = "i = case True +| True => 2 +| False => 42" +let str_case2 = "i = case nil(a := Int) +| nil => 12 +| _ => 24" +let str_let = "i = let a = 5 in a + 1" +let str_let2 = "j = let b = 5 in b" +let str_lambda = "sqr = lambda (x : Int) -> x * x;" +let str_lambda2 = "sqr = lambda (x : Int) -> x * x;" +let str_lambda3 = "sqr = lambda (x : Int) -> lambda (y : Int) -> x * y;" +let str_type = "i = let j = decltype(Type) in decltype(j);" +let str_type2 = "j = let i = Int -> Int in decltype(i);" + +let generate_ltype_from_str str = + List.hd ((fun (lst, _) -> + (List.map + (fun (_, _, ltype) -> ltype)) + (List.flatten lst)) + (lexp_decl_str str default_lctx)) + +let generate_lexp_from_str str = + List.hd ((fun (lst, _) -> + (List.map + (fun (_, lxp, _) -> lxp)) + (List.flatten lst)) + (lexp_decl_str str default_lctx)) + +let input_induct = generate_lexp_from_str str_induct +let input_int_4 = generate_lexp_from_str str_int_4 +let input_int_3 = generate_lexp_from_str str_int_3 +let input_case = generate_lexp_from_str str_case +let input_case2 = generate_lexp_from_str str_case2 +let input_let = generate_lexp_from_str str_let +let input_let2 = generate_lexp_from_str str_let +let input_lambda = generate_lexp_from_str str_lambda +let input_lambda2 = generate_lexp_from_str str_lambda2 +let input_lambda3 = generate_lexp_from_str str_lambda3 +let input_arrow = generate_ltype_from_str str_lambda +let input_arrow2 = generate_ltype_from_str str_lambda2 +let input_arrow3 = generate_ltype_from_str str_lambda3 +let input_type = generate_ltype_from_str str_type +let input_type_t = generate_ltype_from_str str_type2 + +let generate_testable (_: lexp list) : ((lexp * lexp * result) list) = + + ( Lambda ((Aexplicit), + (Util.dummy_location, "L1"), + Var((Util.dummy_location, "z"), 3), + Imm (Integer (Util.dummy_location, 3))), + Lambda ((Aexplicit), + (Util.dummy_location, "L2"), + Var((Util.dummy_location, "z"), 4), + Imm (Integer (Util.dummy_location, 3))), Nothing ) + + ::(input_induct , input_induct , Equivalent) (* 2 *) + ::(input_int_4 , input_int_4 , Equivalent) (* 3 *) + ::(input_int_3 , input_int_4 , Nothing) (* 4 *) + ::(input_case , input_int_4 , Constraint) (* 5 *) + ::(input_case , input_induct , Constraint) (* 6 *) + ::(input_case , input_case , Equivalent) (* 7 *) + ::(input_case , input_case2 , Nothing) (* 8 *) + + ::(input_let , input_induct , Constraint) (* 9 *) + ::(input_let , input_int_4 , Constraint) (* 10 *) + ::(input_let , input_case , Constraint) (* 11 *) + ::(input_let , input_let , Equivalent) (* 12 *) + ::(input_let2 , input_let , Equivalent) (* 13 *) + ::(input_let2 , input_let2 , Equivalent) (* 14 *) + + ::(input_lambda , input_int_4 , Nothing) (* 15 *) + ::(input_lambda , input_induct , Nothing) (* 16 *) + ::(input_lambda , input_case , Constraint) (* 17 *) + ::(input_lambda , input_case2 , Constraint) (* 18 *) + ::(input_lambda , input_let , Constraint) (* 19 *) + ::(input_lambda , input_induct , Nothing) (* 20 *) + ::(input_lambda , input_lambda , Equivalent) (* 21 *) + + ::(input_lambda2 , input_int_4 , Nothing) (* 22 *) + ::(input_lambda2 , input_induct , Nothing) (* 23 *) + ::(input_lambda2 , input_case , Constraint) (* 24 *) + ::(input_lambda2 , input_case2 , Constraint) (* 25 *) + ::(input_lambda2 , input_let , Constraint) (* 26 *) + ::(input_lambda2 , input_induct , Nothing) (* 27 *) + ::(input_lambda2 , input_lambda , Equivalent) (* 28 *) + ::(input_lambda2 , input_lambda2 , Equivalent) (* 29 *) + ::(input_lambda2 , input_lambda3 , Constraint) (* 30 *) + ::(input_lambda3 , input_lambda3 , Equivalent) (* 31 *) + + ::(input_arrow2 , input_int_4 , Unification) (* 32 *) + ::(input_arrow2 , input_induct , Unification) (* 33 *) + ::(input_arrow2 , input_case , Constraint) (* 34 *) + ::(input_arrow2 , input_case2 , Constraint) (* 35 *) + ::(input_arrow2 , input_let , Constraint) (* 36 *) + ::(input_arrow2 , input_induct , Unification) (* 37 *) + ::(input_arrow2 , input_lambda , Unification) (* 38 *) + ::(input_arrow2 , input_lambda2 , Unification) (* 39 *) + ::(input_arrow2 , input_arrow3 , Unification) (* 40 *) + ::(input_arrow3 , input_arrow , Unification) (* 41 *) + ::(input_arrow2 , input_arrow , Unification) (* 42 *) + ::(input_arrow3 , input_arrow3 , Equivalent) (* 43 *) + + ::(input_type , input_type_t , Equivalent) (* 44 *) + + ::(Metavar (0, S.Identity, (Util.dummy_location, "M"), type0), + Var ((Util.dummy_location, "x"), 3), Unification) (* 45 *) + + ::[] + +let test_input (lxp1: lexp) (lxp2: lexp) (subst: meta_subst): unif_res = + let res = unify lxp1 lxp2 Myers.nil subst in + let tmp = match res with + | Some (s, []) when s = empty_meta_subst -> (Equivalent, res, lxp1, lxp2) + | Some (_, []) -> (Unification, res, lxp1, lxp2) + | Some _ -> (Constraint, res, lxp1, lxp2) + | None -> (Nothing, res, lxp1, lxp2) + in tmp + +let check (lxp1: lexp) (lxp2: lexp) (res: result) (subst: meta_subst): bool = + let r, _, _, _ = test_input lxp1 lxp2 subst + in if r = res then true else false + +let test_if (input: lexp list) sample_generator checker : bool = + let rec test_if_ samples checker = + match samples with + | (l1, l2, res)::t -> if checker l1 l2 res empty_meta_subst then test_if_ t checker else false + | [] -> true + in test_if_ (sample_generator input) checker + +let unifications = List.map + (fun (l1, l2, res) -> + let r, _, _, _ = test_input l1 l2 empty_meta_subst + in (l1, l2, res, r)) + (* FIXME: Skip failure for now. *) + [] (* (generate_testable []) *) + +let idx = ref 0 +let _ = List.map + (fun (str, (l1, l2, expected, res)) -> + idx := !idx + 1; + add_test "UNIFICATION" + ((if !idx < 10 then "0" else "") ^ (string_of_int !idx) ^ " " ^ str ) + (fun () -> if expected = res then success () else failure ())) + (List.combine (fmt unifications) unifications ) + +let _ = run_all () + +
===================================== tests/utest_lib.ml ===================================== --- a/tests/utest_lib.ml +++ b/tests/utest_lib.ml @@ -117,6 +117,12 @@ let ut_string2 = ut_string 2 let unexpected_throw sk tk e = ut_string2 (red ^ "[ FAIL] " ^ sk ^ " - " ^ tk ^ "\n"); ut_string2 "[ ] UNEXPECTED THROW:\n"; + ut_string2 "[ ] ----------------------------- Callstack (20): -----------------------------------------\n"; + ut_string2 ("[ ] " ^ (Printexc.raw_backtrace_to_string (Printexc.get_callstack 20))); + ut_string2 "[ ] ---------------------------------------------------------------------------------------\n"; + ut_string2 "[ ] ----------------------------- Backtrace: ----------------------------------------------\n"; + ut_string2 ("[ ] " ^ (Printexc.get_backtrace ()) ^ "\n"); + ut_string2 "[ ] ---------------------------------------------------------------------------------------\n"; ut_string2 "[ ] "; ut_string2 ((Printexc.to_string e) ^ "\n" ^ reset)
let _expect_equal_t to_string value expect =
View it on GitLab: https://gitlab.com/monnier/typer/compare/1da5866c028f2e291202707233118edb05a...
Afficher les réponses par date