Stefan pushed to branch master at Stefan / Typer
Commits: 63fcf274 by Stefan Monnier at 2015-08-08T18:15:54-04:00 Initial commit
- - - - - 854501d8 by Stefan Monnier at 2015-09-21T21:57:46-04:00 Add some references to DESIGN
- - - - - 3a5410fe by Stefan Monnier at 2015-09-22T16:02:01-04:00 Add examples of macros.
- - - - - 0943a639 by Stefan Monnier at 2015-10-17T17:39:57-04:00 -
- - - - - 9d6567d8 by Stefan Monnier at 2015-11-05T11:31:32-05:00 Tweak DESIGN and add core-syntax to manual
- - - - - 43bd0261 by Stefan Monnier at 2015-11-05T11:43:04-05:00 -
- - - - - ddd5bc21 by Stefan Monnier at 2015-11-18T13:38:39-05:00 Explain implicit/ersable in manual
- - - - - bb1d1090 by Stefan Monnier at 2015-11-20T16:18:23-05:00 * manual.texi (Core Syntax): Tweak the syntax
* pexp.ml (ppat): New type. (pexp): Change Pinductive and Pcase according to the new syntax. Adjust the parsing/unparsing code accordingly.
* sexp.ml (sexp_p_list, sexp_u_list): New helper functions.
- - - - - a90614fc by Pierre Delaunay at 2016-01-18T11:54:44-05:00 new make file
- - - - - 908e455e by Pierre Delaunay at 2016-01-21T09:58:20-05:00 new make file
- - - - - a547bdb8 by Stefan Monnier at 2016-01-21T15:13:49-05:00 Minor followup updates due to the new syntax
* main.ml (default_stt): Avoid apparently obsolete "Array.create". (process_typer_file.process_decl): Use new names "pexp_[up]_*".
* manual.texi (Core Syntax): Tweak syntax.
* test.typer: Try to update code to new syntax.
- - - - - f509e8a2 by Pierre Delaunay at 2016-01-22T10:42:40-05:00 Merge remote-tracking branch 'origin/master' into work
- - - - - 6cb6f695 by Pierre Delaunay at 2016-01-22T13:34:33-05:00 utest_main + Makefile update
- - - - - 482a5aab by Pierre Delaunay at 2016-01-22T14:04:28-05:00 utest_main + Makefile update
- - - - - ad00ffbd by Pierre Delaunay at 2016-01-22T14:08:57-05:00 Merge branch 'work' of gitlab.com:monnier/typer into work
Conflicts: Makefile tests/utest_main.ml
- - - - - 4e901ec3 by Stefan Monnier at 2016-02-14T15:57:51-05:00 * .gitignore: Add ChangeLog.
- - - - - 7b2de3d5 by Stefan Monnier at 2016-02-14T16:03:18-05:00 * GNUmakefile: Rename since it uses GNU extensions
- - - - - f15cc0c5 by Stefan Monnier at 2016-02-15T10:19:55-05:00 Start changes to use deb-indices and drop type inference
* src/lexp.ml: Start changes to use deb-indices and simplify things. (vref): New type. (lexp): Var now uses debruijn-indices. Comment out metavars since we're not going to do inference for now. (type_eq, builtins, lexp_location): Adjust accordingly. (lexp_alpha): Remove since deb-indices don't need it. * typer-mode.el (typer-smie-grammar): Add an explicit level for "=".
- - - - - cb8b9b2f by Stefan Monnier at 2016-02-16T15:29:26-05:00 Fix various minor issues we saw while reading lexp.ml
* src/pexp.ml (pexp): Fix Pinductive definition. (pexp_parse): Fix "inductive-cons" name. * src/lexp.ml: Comment out most of the code.
- - - - - 59caf4c8 by Pierre Delaunay at 2016-02-18T17:04:36-05:00 sexp_parse_to_list + debugs in one files
- - - - - 2c1f85fe by Pierre Delaunay at 2016-02-19T17:42:47-05:00 pexp debug_print
- - - - - 1617fc49 by Pierre Delaunay at 2016-02-19T18:11:50-05:00 add pexp test file
- - - - - 3560cc78 by Stefan Monnier at 2016-02-20T00:13:57-05:00 * src/lexp.ml: Various tweaks to prepare for DeBruijn indices
(db_index, db_offset, db_revindex): New types. (vref): Use them. (lexp): Add Shift. (env_type): New type. (env_lookup_type): New function. (senv_type): New type. (senv_lookup): New function. (lexp_p_infer, lexp_p_check): New functions.
- - - - - f27e2fe6 by Pierre Delaunay at 2016-02-20T11:04:54-05:00 Pinductive fix
- - - - - 15297a8c by Pierre Delaunay at 2016-02-22T16:52:39-05:00 debuijn data structure
- - - - - d5019e4a by Pierre Delaunay at 2016-02-24T23:10:18-05:00 let/Arrow/Lambda lexp
- - - - - 24668c78 by Pierre Delaunay at 2016-02-24T23:47:20-05:00 comment cleaning
- - - - - fc20af3d by Pierre Delaunay at 2016-02-25T00:50:45-05:00 pexp_decls function node activated
- - - - - 4115d3ff by Pierre Delaunay at 2016-02-25T01:29:52-05:00 add 'Section' (sexp, pexp, lexp, ...) in error message
- - - - - a0c7ef21 by Pierre Delaunay at 2016-02-25T19:16:48-05:00 merging
- - - - - 25508a29 by Pierre Delaunay at 2016-02-25T20:41:14-05:00 add Debruijn index
- - - - - f9d3f518 by Pierre Delaunay at 2016-02-26T17:12:59-05:00 fix let declaration merging
- - - - - 0119ea77 by Pierre Delaunay at 2016-02-26T17:38:56-05:00 lexp PCall handling
- - - - - bb2cbbd5 by Pierre Delaunay at 2016-02-26T23:14:40-05:00 cleaning
- - - - - 57a4f589 by Stefan Monnier at 2016-02-26T23:18:43-05:00 * src/pexp.ml: Adjust to recent changes to Pinductive
* src/main.ml (process_typer_file.process_decl): Remove Lexp use since it's not ready yet.
* src/pexp.ml (pexp_p_actual_arg, pexp_p_formal_arg) (pexp_u_formal_arg): New functions. (pexp_unparse, pexp_parse.pcases): Use them to handle the formal args of inductive types. (pexp_p_decls): Rename from pexp_decls.
* .gitignore: Ignore *.byte files.
- - - - - 62596a77 by Pierre Delaunay at 2016-02-27T12:16:56-05:00 merging
- - - - - 573e2b5b by Pierre Delaunay at 2016-03-01T23:12:57-05:00 PCase
- - - - - 496106a8 by Pierre Delaunay at 2016-03-02T00:11:28-05:00 simple eval
- - - - - 81fa9435 by Pierre Delaunay at 2016-03-02T09:26:56-05:00 merged equivalent definition + moved inference routine to lparse
- - - - - 693aa3fa by Pierre Delaunay at 2016-03-02T15:39:55-05:00 simplified lexp_context
- - - - - 02f84cd7 by Pierre Delaunay at 2016-03-03T12:27:34-05:00 PCall improved, + use lexp_p_infer when needed
- - - - - 36520963 by Pierre Delaunay at 2016-03-04T20:31:09-05:00 prelex_string hack
- - - - - e8c42357 by Pierre Delaunay at 2016-03-04T23:44:41-05:00 call + lambda eval
- - - - - b3a7eafb by Pierre Delaunay at 2016-03-06T13:13:10-05:00 simple repl for interactive testing
- - - - - cd150174 by Pierre Delaunay at 2016-03-06T15:06:10-05:00 fix inductive pexp parsing
- - - - - bbeff6f8 by Pierre Delaunay at 2016-03-06T16:47:12-05:00 eval case
- - - - - c6d73fd5 by Pierre Delaunay at 2016-03-06T21:16:28-05:00 env_info fix
- - - - - 6b432d51 by Pierre Delaunay at 2016-03-09T20:37:20-05:00 correct declaration handling
- - - - - 772d8502 by Pierre Delaunay at 2016-03-09T22:31:08-05:00 fix nested lambda offset
- - - - - 2a292311 by Pierre Delaunay at 2016-03-11T10:17:24-05:00 declaration fix bis
- - - - - e594f7fe by Pierre Delaunay at 2016-03-13T12:49:23-04:00 Basic utest lib
- - - - - a37b8648 by Pierre Delaunay at 2016-03-13T14:31:28-04:00 tests
- - - - - 881f7888 by Pierre Delaunay at 2016-03-13T19:51:00-04:00 fix lexp_decl double decl
- - - - - 61f036c4 by Stefan Monnier at 2016-03-15T18:16:46-04:00 * src/lparse.ml (lexp_parse): Don't return a context
(lexp_parse_constructors, lexp_call): Same.
- - - - - 1a13cb32 by Pierre Delaunay at 2016-03-16T20:02:23-04:00 add new eval/lexp/pexp string
- - - - - 94117ebf by Pierre Delaunay at 2016-03-16T20:04:24-04:00 variable cascade
- - - - - d27dd338 by Pierre Delaunay at 2016-03-16T20:11:37-04:00 eval does not return ctx anymore
- - - - - 9bbc1472 by Pierre Delaunay at 2016-03-16T20:40:54-04:00 removed useless definitions
- - - - - 408e47b6 by Pierre Delaunay at 2016-03-16T20:44:38-04:00 fix double declarations
- - - - - bcc59cc4 by Pierre Delaunay at 2016-03-16T21:00:23-04:00 dbi info
- - - - - 86861d63 by Pierre Delaunay at 2016-03-16T21:11:55-04:00 lexp does not return ctx anymore
- - - - - eceb5ece by Pierre Delaunay at 2016-03-17T09:49:49-04:00 check
- - - - - 49bf1cb1 by Pierre Delaunay at 2016-03-19T17:56:51-04:00 utest check return code
- - - - - 48362db8 by Pierre Delaunay at 2016-03-19T18:07:41-04:00 Debruijn partial fix
- - - - - e502bfc8 by Pierre Delaunay at 2016-03-20T12:35:44-04:00 builtin type inference
- - - - - df91a4f1 by Pierre Delaunay at 2016-03-20T17:14:15-04:00 free var
- - - - - 6cd88359 by Stefan Monnier at 2016-03-20T22:12:22-04:00 Make the code compile
* src/eval.ml (_eval): Eval body with the extra vars bound from the pattern match.
* src/main.ml (default_grammar, default_stt): Remove; use Grammar instead..
* tests/REPL.ml (ipexp_parse): Reduce duplication. Fix `nod' ref. (ilexp_parse): Get it to type-check. (ilexp_parse_all.loop, ieval_all.loop): Fix use of ::. (ieval): Get it to type-check. (repl.loop.print_e): Fix arg names.
- - - - - 96867ec2 by U-SDM-9528\Etudiants at 2016-03-21T13:31:48-04:00 merging
- - - - - 7a0bb44f by U-SDM-9528\Etudiants at 2016-03-21T13:59:33-04:00 merging (compile)
- - - - - d14e36a4 by Pierre Delaunay at 2016-03-21T14:05:35-04:00 rollback
- - - - - 015c8a70 by Pierre Delaunay at 2016-03-21T14:26:42-04:00 merged
- - - - - a3eb218d by Pierre Delaunay at 2016-03-21T14:32:59-04:00 merge with experimental branch
- - - - - 932370de by Pierre Delaunay at 2016-03-21T14:46:09-04:00 merge again
- - - - - 74750a66 by Pierre Delaunay at 2016-03-21T23:22:08-04:00 ityper fix + remove trailling space for consistency
- - - - - 2e53f40d by Pierre Delaunay at 2016-03-22T18:41:03-04:00 bound is inside lexp_ctx
- - - - - db4f6c1e by Pierre Delaunay at 2016-03-22T19:51:41-04:00 ityper can interpret files before REPL
- - - - - aa416638 by Pierre Delaunay at 2016-03-23T11:41:25-04:00 add arg parsing for ityper and full_debug
Changes to be committed: * GNUmakefile : new option "make tests", build tests and run them * tests/REPL.ml : files can be interpreted to populate environments * tests/full_debug.ml : we can choose how much info we want to print
- - - - - cdec9d9a by Pierre Delaunay at 2016-03-23T23:37:17-04:00 eval removes old temporary variables from ctx between function calls
Changes to be committed: * src/debruijn.ml : rollback, old dbi were correct * src/eval.ml : - ctx is reinitialized between calls - new function debug_eval (equiv to old eval) - eval does not print call_trace and context if an error is raised * tests/eval_test.ml : test ctx reinit * tests/full_debug.ml: use debug_eval instead of eval
- - - - - bd7fd362 by Pierre Delaunay at 2016-03-23T23:47:47-04:00 All tests are passed - Recursion with case are working
Changes to be committed: * minor modifications
- - - - - 6fa07a98 by Stefan Monnier at 2016-03-24T17:15:11-04:00 Fix compilation yet again; Fix the "executable bit" in various files
* tests/REPL.ml (ieval): Fix type error. * src/eval.ml (eval_all): Reduce redundancy.
- - - - - bc4698bc by Stefan Monnier at 2016-03-24T22:22:01-04:00 Fix lexp's Induction to name fields. Fix lexp_context for real vars.
* src/debruijn.ml (db_idx, db_ridx): Re-introduce those type aliases. (senv_add_var): Remove redundancy. Change calling convention. (lexp_context): Make var's "value" optional. (env_extend): New function.
* src/eval.ml (nfirst_rte_var._eval.ctor_name): Fix confusion in constructor args.
* src/lexp.ml (lexp): Add optional name to constructor fields.
* src/lparse.ml (default_lctx): Adjust to new senv_add_var. (lexp_parse): Consolidate the two Plambda cases. Don't mess with local_scope here. (lexp_parse_inductive): Rename from lexp_parse_constructors. Adapt to lexp changes. Use List.fold_left. (lexp_decls): Adjust to new senv_add_var. (lexp_context_print): Handle vars without value.
- - - - - ec675623 by Pierre Delaunay at 2016-03-25T00:02:15-04:00 Improved debug/diagnostic routine of lexp_parse
Changes to be committed: * src/eval.ml : renamed global_rte/global_trace to _global_eval_ctx/_global_eval_trace * src/lparse.ml : - added a _global_lexp_ctx/_global_lexp_trace - renamed lexp_context_print to print_lexp_context * src/pexp.ml : new function pexp_to_string * src/util.ml : new function print_trace
- - - - - c3d32166 by Pierre Delaunay at 2016-03-25T12:22:44-04:00 Modification of lparse.lexp_decls and debruijn.env_lookup_type to accommodate type inference
lexp_decls was pushing var names before their type info which caused type inference to fail (idx <=> name mismatch). Now env_lookup compute the correct index if environments (env and senv) are not synchronised
Changes to be committed: * src/lparse.ml * src/debruijn.ml
- - - - - cd399c51 by Pierre Delaunay at 2016-03-26T20:33:29-04:00 Merging + added some type inference
Changes to be committed: * src/lparse.ml : added some type inference * tests/full_debug.ml : added lctx cmd arg (print lexp_context)
- - - - - 1b186a75 by Pierre Delaunay at 2016-03-26T20:41:21-04:00 moved non test related files to src/
Changes to be committed: * renamed: tests/REPL.ml -> src/REPL.ml * renamed: tests/debug.ml -> src/debug.ml * renamed: tests/full_debug.ml -> src/full_debug.ml * GNUmakefile: match new file name
- - - - - 988fbe6c by Pierre Delaunay at 2016-03-26T22:06:58-04:00 Added command lines argument to utest executable. --verbose/--samples
Changes to be committed: * src/REPL.ml: Shorter special commands * tests/eval_test.ml: use default_lctx (populated with builtin lexp) * tests/utest_lib.ml * tests/utest_main.ml - "--verbose" allow us to choose what to print - "--samples" is used if the test require files. This specifies where the test should look for them
- - - - - 33279ef6 by Pierre Delaunay at 2016-03-30T09:53:57-04:00 Allow restricted type aliasing during type inference
In 'Nat = inductive_' We want to use the alias 'Nat' instead of the full declaration during type inference. It is restricted aliasing because only inductive type can be aliased that way.
Changes to be committed: * GNUmakefile: tests don't run when using make all * src/eval.ml: Call eval check for constructor before evaluating (Test - Nat Plus Work) * src/lparse.ml: - Type inference: Allow restricted type aliasing - Type inference: Call now allow partial application - Type inference: Cons are typed as function * src/lexer.ml: added (lex_str) and (sexp_parse_str) * src/pexp.ml: removed useless declaration/include * tests/eval_test.ml: - Mutually rec decl tests - Partial Application test
new file: * tests/sexp_test.ml: test _*_ and _+_ precedence which both seems to be buggy
- - - - - 7cfabe06 by Pierre Delaunay at 2016-03-31T00:43:05-04:00 Fix mutually recursive definition lexp parsing
Changes to be committed: * src/lparse.ml: - rollback to old lexp_decls implementation - renamed (lexp_decls) to (lexp_p_decls) * tests/eval_test.ml: minor fixes * src/eval.ml: - new functions (eval_call)/(eval_case) - modified eval_call to support partial application
renamed: src/full_debug.ml -> src/debug_util.ml * GNUmakefile: adapted to renamed files
- - - - - b1ff2b13 by Pierre Delaunay at 2016-04-01T09:46:40-04:00 Improved eval_case and partial eval is working
eval.case, now, do check if the constructor exists. lparse.case check if name fields are constructors or not
Changes to be committed: * src/eval.ml: - case: ctor check - partial eval working - new function (is_free_var) * src/lparse.ml - Case: check uniqueness, print a warning if not unique * src/REPL.ml - ityper does not crash when an error is thrown - added support for repl command with arguments * src/debruijn.ml - new function (_env_lookup). (env_lookup_type) and (env_lookup_expr) are specialized version of (_env_lookup)
- - - - - 501075ff by Pierre Delaunay at 2016-04-02T02:17:29-04:00 Move things arround so lparse.ml can include eval.ml
Changes to be committed: * moved lparse.lexp_print to lexp.lexp_print * moved eval.eval_*_str to lparse * src/lparse: simplified _lexp_*_str * src/lexp: - new lexp_print, increased readability, + add console highlighting - new function (_lexp_to_str) * src/debug.ml - better debug_lexp_decls * src/debug_util.ml - added a typer-format mode to debug_util * tests/utest_lib.ml: added color
- - - - - e50902fe by Stefan Monnier at 2016-04-08T17:06:55-04:00 * src/typecheck.ml: New file.
* src/main.ml: Refer to Typecheck, tho it's not used yet. * src/lexp.ml (subst): New type. (lexp): Use it. Rename Shift to Susp. (lexp_location): Adjust accordingly.
- - - - - af573094 by Pierre Delaunay at 2016-04-08T19:58:03-04:00 Moved some definitions to avoid circular dependencies. Reordered/removed some 'includes'/open
Note to self: never convert Ocaml source file to UTF8
Changes to be committed: * src/builtin.ml: moved lexp.builtin definition to a new file * src/env.ml: moved runtime env definition to a new file * src/lparse.ml: removed function (free_variable) - eval string functions are now inside lparse
- - - - - 4f17a10c by Pierre Delaunay at 2016-04-08T21:16:15-04:00 Step toward correct builtin handling. Minor modifications to make it compile again.
Changes to be committed: * GNUmakefile: execution shortcut (run/typer) (run/debug_util) (run/tests) * src/builtin.ml: added (default_lctx) and (default_rctx) * src/lexp.ml: identifies call to builtin functions * src/eval.ml: call to builtin is a special case
- - - - - 72d74b56 by Stefan Monnier at 2016-04-09T23:28:42-04:00 * src/typecheck.ml: Actually implement a simple conv_p
* src/subst.ml: New file. * src/lexp.ml: Use it. (lexp): Remove UnknownType.
* src/util.ml (SMap): Move from grammar.ml * src/grammar.ml (SMap): Move to util.ml
* GNUmakefile (OBFLAGS): Rename from CFLAG. Remove -rectypes.
* src/lparse.ml (dlxp, dltype): Use arbitrary expression instead of UnknownType.
* src/main.ml: Use named import rather than `open`.
- - - - - 4bdbf044 by Pierre Delaunay at 2016-04-10T15:54:03-04:00 runtime_env use a ref cell
Changes to be committed: * src/env.ml: - runtime_env use a ref cell - new function (set_rte_variable) * src/eval.ml - take advantage of the ref cell to read all declarations before processing them
- - - - - 029fd6b8 by Pierre Delaunay at 2016-04-10T17:09:47-04:00 Merging
- - - - - 5c5f905d by Stefan Monnier at 2016-04-10T21:44:47-04:00 * src/typecheck.ml (check): Start filling the function
(varbind): New type.
- - - - - fbc37827 by Pierre Delaunay at 2016-04-11T09:54:32-04:00 Merging
- - - - - 6834711a by Pierre Delaunay at 2016-04-11T10:05:18-04:00 src/typecheck.ml: type declarations are now in builtin.ml
- - - - - 111770da by Pierre Delaunay at 2016-04-11T12:40:30-04:00 Makefile now works on cygwin windows
- - - - - 93af3589 by Pierre Delaunay at 2016-04-11T14:47:31-04:00 work
- - - - - 48cc9c28 by Pierre Delaunay at 2016-04-12T18:42:20-04:00 Modifed evaluation environment to support closures
Changes to be committed: * src/builtin.ml: - modified builtin +/* to match new implementation (more generic) - new function (get_builtin_impl) return an ocaml function which implements the requested operation * src/eval.ml: moved value_type to env.ml * src/env.ml: replaced lexp by value_type - added closure type to value_type * src/fmt.ml: new function (calign_print_*)
- - - - - ef5eb300 by Pierre Delaunay at 2016-04-13T12:01:50-04:00 Allow users to filter which test to run
Changes to be committed: * tests/utest_main.ml: - new supported arguments (--fsection=) and (--ftitle) * src/builtin.ml: - added some macro declarations
- - - - - a2c5628d by Pierre Delaunay at 2016-04-13T12:15:00-04:00 merging
- - - - - 9b02b6a7 by Pierre Delaunay at 2016-04-14T01:26:01-04:00 Added some macro making function implementation
Changes to be committed: * src/builtin.ml: - added (make_symbol) and (make_node) implementation - simplified (_generic_binary_iop) * src/env.ml: added Vsexp to value_type
- - - - - 0905ab89 by Pierre Delaunay at 2016-04-15T11:47:20-04:00 lexp_p_infer: Type propagation
Changes to be committed: * src/debruijn.ml: - lexp_context uses a ref cell (which solve all our synchronization problems between env and senv - new function (env_set_var_info) * src/lparse.ml: - started to propagate types and lexp_parsing at the same time - modified (_lexp_decls) to match the new environement
- - - - - c1e835ce by Pierre Delaunay at 2016-04-16T11:26:03-04:00 lexp_p_infer continued
Changes to be committed: * src/debug_util.ml: uses default runtime env * src/lparse.ml: - print_lexp_ctx, now, prints in order - lambda builds its type and returns it - cons, call return their type - replaced (lexp_parse) by (lexp_p_infer) * src/lexp.ml: lexp_print, now, prints builtin operators correctly * tests/eval_test.ml: - added some type annotations to remove some warnings * tests/lexp_test.ml: - new test: Does lexp_print print correct typer code ? (yes) * src/util.ml: - new function (msg_fatal) - added _typer_verbose which controls how much information is going to be printed out
- - - - - acbe9589 by Pierre Delaunay at 2016-04-17T20:09:54-04:00 minor changes
- - - - - b978cb6b by Stefan Monnier at 2016-04-18T08:21:44-04:00 * src/subst.ml: Rewrite completely, mostly following the λσ approach
* .gitignore: Add missing final newline. Fix #*# pattern.
* src/lexp.ml (lexp): Swap Susp's arguments, to match the order usually used in papers. Adjust all users accordingly.
* src/typecheck.ml (mkSusp, scompose, sapply, ssink): New helpers to use the new substitutions. (conv_p'): Adjust to new substitutions's type. (check): Check that Let's types are indeed types. Fix compilation.
- - - - - 66678b3b by Pierre Delaunay at 2016-04-18T10:42:21-04:00 Merge branch 'master' of https://gitlab.com/monnier/typer
- - - - - ccb4d1aa by Stefan Monnier at 2016-04-18T21:13:23-04:00 * src/typecheck.ml (check): Handle Susp and Call
* src/subst.ml (substitute): New function.
* src/typecheck.ml: Don't open Util any more. (unsusp, sort_compose): New functions. (check): Improve: add Call case, and half of Inductive.
- - - - - f1ee2eb8 by Pierre Delaunay at 2016-04-19T12:40:55-04:00 new implementations lexp_p_decls
Changes to be committed: * src/lparse.ml: - added type of types - added a new implementation of lexp_p_decls but commented it out as it requires handling shifting
- - - - - 6a2ba53d by Pierre Delaunay at 2016-04-19T15:12:23-04:00 Merge branch 'master' of https://gitlab.com/monnier/typer
- - - - - de90e983 by Pierre Delaunay at 2016-04-20T02:46:34-04:00 Added macro handling in lparse.ml
Changes to be committed: * src/builtin.ml: added (expand_) * src/eval.ml: new function (from_lctx) * src/lparse.ml: handle the macro case in lexp_call
- - - - - 70f86081 by Stefan Monnier at 2016-04-20T15:42:17-04:00 * src/subst.ml (compose): Simplify
(Shift): Switch argument order to better match the notation. (lookup): Rename from `apply`.
- - - - - 29bde6e0 by Pierre Delaunay at 2016-04-21T17:36:03-04:00 -
Changes to be committed: * new file: samples/BTL.typer (list implementation) * new file: samples/autodiff.typer simple symbolic diff example * src/lparse.ml: - improved lexp_decls (lexp_decls now lexp_p_check when it can) - handle Phas_type - lexp_p_check: handle Plambda - moved macro handling to lexp_p_check * tests/eval_test.ml: - added list test - added necessary type annotations
- - - - - 731e1482 by Stefan Monnier at 2016-04-26T21:58:46-04:00 * src/grammar.ml (default_grammar): Sync with typer-mode.el
- - - - - 5521e11a by Pierre Delaunay at 2016-04-27T11:02:03-04:00 fix little things
Changes to be committed: * GNUmakefile: compile to bytecote to avoid recompilation * src/pexp.ml: fix formal arg parsing * tests/sexp_test.ml: fix sexp_test
- - - - - 6967d92c by Pierre Delaunay at 2016-04-28T09:51:02-04:00 fix lexp_decls and Macro
Changes to be committed: * README.md: minor updates * src/lparse.ml: - add an error message when lambda does not habe type info - fix lexp.Arrow, its variable was not added to the environement * src/builtin.ml * btl/macro.typer: - added some ideas on how to define type built-in * src/lexp.ml: - fix lexp_print Inductive's formal args
- - - - - 4af18f1c by Pierre Delaunay at 2016-04-28T16:45:35-04:00 Continued Stefan `value_type` changes (Broke Macro Handling)
Changes to be committed: * src/env.ml : value_type definition - no more `Value of lexp`
- Adapted Files * src/eval.ml * src/builtin.ml * tests/*
- - - - - 3be5ffe6 by Pierre Delaunay at 2016-04-29T12:21:49-04:00 Fix Macro handling. Removed some dead code
Changes to be committed: * src/lparse.ml
- - - - - 8ec96e19 by Pierre Delaunay at 2016-05-02T08:19:48-04:00 Add the 'quasiquote' operator (`qquote`) Removed `temp_ctx` as it is not used anymore
Changes to be committed: * src/REPL.ml: temp_ctx - qquote handling: * src/builtin.ml * src/eval.ml * src/lparse.ml * src/sexp.ml: new function (sexp_to_st) * src/prelexer.ml: new function (pretoken_to_str) * src/lexp.ml: print (Imm(sexp)) correctly
- - - - - 7fa6faac by Stefan Monnier at 2016-05-05T20:36:48-04:00 * src/lexp.ml (lexp): Add return type to `Case`
(_lexp_to_str): * src/typecheck.ml (unsusp, check): * src/lparse.ml (_lexp_p_infer): * src/eval.ml (_eval): Adjust accordingly.
- - - - - c4c529a9 by Stefan Monnier at 2016-05-06T23:51:30-04:00 * src/typecheck.ml (check): Add missing cases (mostly, Case and Cons)
* src/lexp.ml: Move the subst helper functions and the unsusp here from typecheck.ml. (U): Use named import instead of `open` for Util. (Case): Change pattern args so they always have an arg_kind. (_lexp_to_str.arg_str): Change accordingly.
* src/lparse.ml: Remove all ";;": they are only meaningful to OCaml's interactive loop and don't belong in source files. (lexp_read_pattern, lexp_read_pattern_args): Adjust to new `Case` type.
* src/subst.ml (cons): New primitive.
* src/typecheck.ml: Move the subst helper functions and `unsusp` to lexp.ml. (lookup_value): New function. (check): Add missing cases (mostly, Case and Cons).
- - - - - 0c893907 by Pierre Delaunay at 2016-05-07T08:51:03-04:00 Modified Builtin
Changes to be committed: * src/util.ml Added `typer_unreachable` for impossible case branch raise an error if the branch is used * src/lexp.ml: New definition of builtin
- - - - - 26948fc1 by Pierre Delaunay at 2016-05-07T11:16:32-04:00 New builtin system
Builtin definition file everything is in a single file because we can't force file eval order yet (module system required)
Changes to be committed: * btl/types.typer:
- - - - - 227524e9 by Pierre Delaunay at 2016-05-07T11:20:05-04:00 merging
- - - - - 2f6cc831 by Pierre Delaunay at 2016-05-07T11:34:40-04:00 Add travis bot
- - - - - 72dee3e0 by Pierre Delaunay at 2016-05-07T17:28:16-04:00 Fix lexp_parse.cons arrow
Constructor arrow type with multiple args were built in reverse
Changes to be committed: * .travis.yml: tell travis to install opam * README.md: add build status * src/builtin.ml: added sexp_dispatch * src/lparse.ml: - fix lexp.parse.cons - new function (lexp_case) (lexp_case can check and infer) - Added lexp.case in `lexp_p_check` * tests/eval_test.ml: - remove failure message when failure is expected * src/lexp.ml: - made huge let expression printing more readable * src/typecheck.ml: - adaptation to new Builtin
- - - - - d4cfc3a4 by Pierre Delaunay at 2016-05-07T20:05:20-04:00 fix macro handling
Changes to be committed: * btl/types.typer: * src/builtin.ml: - make_node use typer list. typer list are converted to ocaml list - added `string_eq`, `int_eq` and `sexp_eq` those should help for `uquote` * src/lparse.ml: - Macro_ takes a function (List Sexp) -> Sexp to build a Macro. ocaml sexp list are converted to typer List Sexp during macro expansion.
- - - - - 343b33b5 by Pierre Delaunay at 2016-05-08T00:10:52-04:00 fix node_. 2 arguments instead of one
Changes to be committed: * btl/types.typer * samples/qquote_temp.typer - started to implement qquote in typer * src/builtin.ml * src/eval.ml: - moved `sexp_dispatch` from builtin.ml to eval.ml (circular dependency). The good news being: Lparse.ml only need type0, type_int, etc from builtin.ml which means eval.ml is not going to need builtin.ml for much longer.
- - - - - 90b0c510 by Pierre Delaunay at 2016-05-09T07:49:44-04:00 Added elexp.ml which erase types of lexp expr Fix macro handling
Changes to be committed: * new file: src/elexp.ml - (erase_type) convert lexp -> elexp - (elexp_location) - (elexp_print) * src/lparse.ml: - eval evaluated '(Macro_ fun)' instead of '(fun List)'
- - - - - e905eb9e by Stefan Monnier at 2016-05-10T21:15:41-04:00 Get rid of ;;
- - - - - d951e229 by Pierre Delaunay at 2016-05-11T10:01:39-04:00 Fix security issue with builtin
Changes to be committed: * src/lparse.ml: "Built-in" is only usable during lexp_parse of internal typer files * .travis.yml: try to make travis compile * opam: added opam package definition (travis might need it) * GNUmakefile: add a dummy (make install) for opam
- - - - - f66e4e42 by Pierre Delaunay at 2016-05-11T11:41:35-04:00 merge
- - - - - 73a0c47f by Pierre Delaunay at 2016-05-11T11:41:35-04:00 merge
- - - - - a93ade4b by Stefan Monnier at 2016-05-11T23:10:29-04:00 Rename ityper to typer
- - - - - 93040691 by Pierre Delaunay at 2016-05-12T10:53:14-04:00 Merge branch 'master' of https://gitlab.com/monnier/typer
- - - - - de9aad3d by Pierre Delaunay at 2016-05-12T10:53:14-04:00 Merge branch 'master' of https://gitlab.com/monnier/typer
- - - - - 9ff1a46a by Pierre Delaunay at 2016-05-13T10:51:22-04:00 Use TC.conv_p to check that inferred_t = t in lexp_p_check
Changes to be committed: * src/debug_util.ml * src/lparse.ml: - default_lctx is not a function anymore (avoid reading builtin files more than once) - builtin types are now built from the context * tests/* - adapted to changes * src/eval.ml - eval now uses elexp instead of lexp * src/util.ml - added `debug_msg` which eval whatever it has been given as argument if `_typer_verbose` is >= 4
- - - - - 2f9f95fa by Pierre Delaunay at 2016-05-13T10:56:42-04:00 Use TC.conv_p to check that inferred_t = t in lexp_p_check
Changes to be committed: * src/debug_util.ml * src/lparse.ml: - default_lctx is not a function anymore (avoid reading builtin files more than once) - builtin types are now built from the context * tests/* - adapted to changes * src/eval.ml - eval now uses elexp instead of lexp * src/util.ml - added `debug_msg` which eval whatever it has been given as argument if `_typer_verbose` is >= 4
- - - - - ca0b6e8d by Pierre Delaunay at 2016-05-15T08:57:03-04:00 Builtin now takes two arguments: function_name and function_type
Changes to be committed: * btl/types.typer: reflect "Builtin" change * src/elexp.ml: unsusp susp * src/REPL.ml: - reflected change linked to elexp.ml - file reading is now done with eval_file * src/builtin.ml - add predefined_table and get_predefine * src/lparse.ml: - simplified handle_call as it had a lot of legacy code - constructor now inherit inductive's formal_args as Aerasable arguments cons : (a : Type) ≡> (v : a) -> List a -> List - predef_table is populated in default_ctx right after builtin type definition were read * src/debug_util.ml: - added: -typecheck argument
- - - - - c00870ce by Pierre Delaunay at 2016-05-15T09:45:45-04:00 merge
- - - - - 3002bbb1 by Pierre Delaunay at 2016-05-17T21:38:50-04:00 Add pdecl
Changes to be committed: * src/pexp.ml: - new type `pdecl` * adapted files to new pdecl type - src/debug.ml - src/lparse.ml * src/REPL.ml: - The case `f arg1 arg2 = body` is now correctly identified as a declaration. * new file: - samples/macro_decls.typer * src/lparse.ml: - lexp_context ref cell anymore
- - - - - 25168277 by Pierre Delaunay at 2016-05-19T17:22:01-04:00 lexp_context use varbind
Changes to be committed: * lot of modified files
- - - - - 18d7aa8d by Pierre Delaunay at 2016-05-20T12:58:17-04:00 lexp_p_decls qui ne marche pas
- - - - - 9b332512 by Pierre Delaunay at 2016-05-21T09:11:50-04:00 Use Susp to shift when required.
I don't understand why:
sqr = lambda (x : Int) -> x * x; main = sqr 2; % sqr[0] 2; % failed to find sqr[0] found main
is not processed correctly sqr is not shifted by one as it should have been.
Changes to be committed: * src/lparse.ml * src/lexp.ml * src/debruijn.ml
- - - - - 38d418dc by Pierre Delaunay at 2016-05-23T17:48:02-04:00 fix eval order
Changes to be committed: * src/eval.ml * src/lparse.ml - add dummy type annotation if none present
- - - - - 3335b48a by Pierre Delaunay at 2016-05-23T18:10:47-04:00 Fix recursive definition handling
Changes to be committed: * src/debruijn.ml * src/lparse.ml
- - - - - e2a13504 by Pierre Delaunay at 2016-05-26T15:48:46-04:00 Trys to handle declaration parsing correctly. Function 'length' bug
Changes to be committed: * src/eval.ml: - new function eval_decls_toplevel * src/lparse.ml: - new function lexep_decls_toplevel
- - - - - 723db68b by Pierre Delaunay at 2016-05-26T16:24:59-04:00 All tests pass
Changes to be committed: - src/eval.ml - src/lparse.ml - fix builtin parsing as (lctx -> rctx) is not as straight forward as it was
- - - - - 781a872a by Pierre Delaunay at 2016-05-31T15:39:54-04:00 Macro are passing.
sqr = Macro_ (lambda (x : List Sexp) -> let hd = (head Sexp x) in (node_ (symbol_ "_*_") (cons hd (cons hd nil))));
This does not work, but if the lambda is declared separately, it works
Changes to be committed: * src/builtin.ml * src/debug_util.ml * src/env.ml * src/eval.ml * src/lparse.ml * tests/macro_test.ml
- - - - - 1d5459cf by Pierre Delaunay at 2016-05-31T18:19:26-04:00 fix lexp_parse of mutually recursive def
Changes to be committed: * src/lparse.ml: modified lexp_p_decls
- - - - - c36053c2 by Pierre at 2016-06-03T19:03:38+02:00 fix susp errors, added Monad type definition
- - - - - 053a0f36 by Pierre Delaunay at 2016-06-03T14:35:47-04:00 Added monads
Changes to be committed: * src/lparse.ml * src/eval.ml - added (bind impl) * src/builtin.ml - added (open/read/write _impl)
- - - - - d397b4c1 by Pierre at 2016-06-03T14:38:27-04:00 bugguy
- - - - - ac1f5998 by Pierre Delaunay at 2016-06-03T14:39:53-04:00 resolved file permission issue + merging
- - - - - 20316043 by Pierre Delaunay at 2016-06-03T16:05:02-04:00 Macro decls
Changes to be committed: * src/lparse.ml - partial macro-decls handling
- - - - - f14a2378 by Pierre Delaunay at 2016-06-06T13:13:55-04:00 add property map and remove some warnings
Changes to be committed: * src/debruijn.ml * src/env.ml * src/lparse.ml
- - - - - 207f7226 by Pierre Delaunay at 2016-06-06T13:40:55-04:00 added Builtin attribute type
Changes to be committed: * btl/types.typer * src/builtin.ml * new function (new_attribute)
- - - - - 11191bb7 by Pierre Delaunay at 2016-06-09T12:41:18-04:00 Remove dead code
Changes to be committed: * src/debruijn.ml: dead code removal * src/elexp.ml: fix type print * src/env.ml: modified property env * src/eval.ml: monads are lazily evaluated
- - - - - 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
- - - - - 2fb51647 by Pierre Delaunay at 2016-06-14T16:56:18-04:00 New way of merging and detecting mutually recursive definition in lexp)decls
Changes to be committed: * src/debug_util.ml * src/env.ml * src/lparse.ml * src/REPL.ml: fix typer REPL
- - - - - ed44b6ac by n3f4s at 2016-06-14T22:59:23+02:00 add substitution parameter to _unify_inner_arrow
- - - - - 29ba9a05 by Pierre Delaunay at 2016-06-14T17:05:37-04:00 remove dead code
- - - - - 1bf06575 by Pierre Delaunay at 2016-06-14T17:56:19-04:00 Handle macro decls
Changes to be committed: * src/debug_util.ml : added some debug options * src/lparse.ml : Handle macro decls * src/eval.ml : - added (run-io) - new function (get_predef_eval) retuns a evaluated predef * btl/types.typer : added (run-io)
- - - - - 7d78d71b by Pierre Delaunay at 2016-06-14T20:00:25-04:00 delete dead code + add macro decls test
Changes to be committed: * src/eval.ml : remove dead code * tests/macro_test.ml: new test * btl/types.typer : added properties * src/lparse.ml : added properties * src/debruijn.ml : * new function (add_property) * new function (dump_properties) * src/debug_util.ml: * new debug option (dump-prop)
- - - - - 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
- - - - - 642376ae by Pierre Delaunay at 2016-06-25T18:16:01-04:00 Context accessors and Monad handling. modified travis script
Changes to be committed: *.travis.yml * src/debruijn.ml: - new function (get_attribute) - new function (has_attribute) - modify calling convention of (add_attribute) (better consistency) * btl/types.typer - added builtin context accessors (decltype) and (declexpr) * src/eval.ml - fix monad handling * src/lparse.ml - added context accessor as builtin macro
- - - - - d5da7869 by Pierre Delaunay at 2016-06-25T18:35:09-04:00 new calling convention for builtin functions (location -> int -> value_type list -> runtime_env -> value_type) ^~~~^ new
This allows us to have a more accurate call trace when eval is called inside a builtin-function.
Changes to be committed: * btl/types.typer * src/builtin.ml * src/eval.ml
- - - - - f530a2dd by Pierre Delaunay at 2016-06-26T11:23:25-04:00 Moved builtin macro implementation
Changes to be committed: * btl/types.typer: change type of some accessors * src/builtin.ml : - fix predef shifting - moved builtin macro implementation there * src/debruijn.ml: remove dead code * src/lparse.ml - builtin macro are now recognized inside (handle_macro_call)
- - - - - 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
- - - - - 343fb9c2 by Stefan Monnier at 2016-08-23T20:26:42-04:00 * tests/sexp_test.ml (test_sexp_add): New function. Use it.
- - - - - 2331f785 by Stefan Monnier at 2016-08-23T20:28:44-04:00 * tests/sexp_test.ml (test_sexp_eqv): New fun. Add some tests
* src/sexp.ml (sexp_equal, sexp_eq_list): New funcs. * src/prelexer.ml (pretokens_equal, pretokens_eq_list): New funs.
- - - - - c9bd8ae0 by Stefan Monnier at 2016-08-23T20:30:22-04:00 * src/lexer.ml (nexttoken.lexsym): Fix __<something> handling
- - - - - e54bbd6d by Stefan Monnier at 2016-08-23T20:34:24-04:00 * src/grammar.ml (char_kind): New type
(token_env): Move here; use it. (default_stt): Adjust accordingly. Add entry for '.' tho not currently obeyed. * src/lexer.ml (token_env): Move to util.ml. (nexttoken, nexttoken.lexsym): Adjust to new token_env type. * src/lparse.ml (_lexp_expr_str): * src/pexp.ml (_pexp_expr_str): Use `token_type'. * src/debruijn.ml (has_property): Remove unused var.
- - - - - 85c06461 by n3f4s at 2016-08-25T17:30:34+02:00 Merge branch 'master' into unification
- - - - - c17b5a1f by Stefan Monnier at 2016-08-26T23:47:10-04:00 Tweak use of substitutions and unsusp
* 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.
- - - - - 536bba67 by Stefan Monnier at 2016-08-26T23:51:29-04:00 * src/lexp.ml (push_susp): Don't be so picky.
- - - - - a964be1b by Stefan Monnier at 2016-08-26T23:54:31-04:00 Merge branch 'trunk' into unification
- - - - - e5fa8b6d by Stefan Monnier at 2016-08-27T10:35:44-04: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.
- - - - - d05adcab by Stefan Monnier at 2016-08-27T10:50:37-04: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.
- - - - - 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
- - - - - 4647f3a4 by Stefan Monnier at 2016-08-28T01:04:54-04:00 Try and break some dependencies. Remove unnecessary "Type" builtin
* src/opslexp.ml: Rename from typecheck.ml. Add erasure code. * src/lparse.ml (get_type0): Remove. (empty_lctx): Remove. (default_lctx, default_rctx): Merge. Add "Type" and "Type1". * src/lexp.ml (vdef, vref): Move to util.ml. * src/util.ml (vdef, vref): Move from lexp.ml. * src/env.ml: Don't open Myers. Remove false dependency on Debruijn. * src/elexp.ml: Don't depend on Lexp. Move erasure code to opslexp.ml. * src/debruijn.ml (env_extend): Inline the functions it uses. (senv_add_var, env_add_var_info): Remove. * src/builtin.ml (type2): New var. (sexp_eq): Use sexp_equal. * btl/types.typer (Type): Remove.
- - - - - 277049a0 by Stefan Monnier at 2016-08-28T01:06:43-04:00 * src/lparse.ml (get_int): Remove
(_lexp_p_infer): Use type_int instead.
- - - - - f33ba8a5 by Stefan Monnier at 2016-08-28T22:27:46-04:00 * btl/types.typer (length, head, tail): Make type erasable
* src/opslexp.ml (erase_type): Adjust indices after removing an erasable formal argument.
- - - - - 89b8df07 by Stefan Monnier at 2016-08-28T22:58:52-04:00 * btl/types.typer (sexp_dispatch_): Generalize type
- - - - - 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
- - - - - bd6f086b by Pierre Delaunay at 2016-09-01T16:05:48-04:00 updated macro handling. implemented type_ macro. attributes are not working
Changes to be committed: * modified: btl/types.typer * modified: src/builtin.ml * modified: src/lparse.ml - updated macro handling * new file: samples/inductive.typer - type_ macro implementation
- - - - - 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
- - - - - 915ca70f by Stefan Monnier at 2016-09-07T12:37:50-04:00 * src/opslexp.ml (lexp_whnf): Add various missing cases.
- - - - - 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
- - - - - 49dad956 by Pierre Delaunay at 2016-09-07T15:13:34-04:00 finished type_ macro
Changes to be committed: * samples/inductive.typer - finished the type_ macro * samples/int_index_inconsistency.typer - type index are inconsistent * src/builtin.ml - improved error message
- - - - - 3ef3619c by Pierre Delaunay at 2016-09-07T15:15:21-04:00 Merge branch 'master' of gitlab.com:monnier/typer
- - - - - 1009a3c7 by n3f4s at 2016-09-07T22:29:34+02:00 add metavar handlind in lexp_whnf
- - - - - bae92e62 by Pierre Delaunay at 2016-09-08T09:50:00-04:00 updated the type_ macro. - Formal args were not processed correctly. - Added new examples - Modfied style
Changes to be committed: * samples/inductive.typer
- - - - - 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
- - - - - 713bde4f by Pierre Delaunay at 2016-09-11T09:58:49-04:00 Macro are now expanded by a builtin function.
Changes to be committed: * btl/types.typer: added `expand_macro_` builtin * src/builtin.ml: added `expand_macro_` as a predef * src/eval.ml: `expand_macro_` is a builtin function * src/lparse.ml: - updated `handle_macro_call` to call `expand_macro_` instead of expanding the macro by itself
- - - - - 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.
- - - - - 0ae8be8b by Pierre Delaunay at 2016-09-12T20:55:36-04:00 Changes to be committed: * src/lparse.ml: Fix `case` handling
`case` now looks up the pattern type and add them to the environement. Which allows us to write things like:
`case m | Macro_ f => f args;`
(before a dummy type was added, thus an error occured because f was not considered a function)
* src/util.ml: improved `print_trace` behavior print the last 50 call recorded instead of the first 50
* btl/types.typer * src/eval.ml - expand_macro is now defined in typer
- - - - - 010aa5dc by Pierre Delaunay at 2016-09-12T21:15:58-04:00 Remove dead code, and silence some warnings
Changes to be committed: * btl/types.typer * src/eval.ml * src/lparse.ml
- - - - - d5d7b301 by Pierre Delaunay at 2016-09-13T01:06:15-04:00 new function `lexp_to_pexp`
- - - - - ad319791 by Stefan Monnier at 2016-09-14T14:49:44-04:00 Type check values added via env_extend
* src/debruijn.ml (elab_context): New name. (ectx_to_lctx): New function. (ectx_extend_rec): New function. (env_extend): Use 0 as db_offset since these are non-recursive.
* src/lparse.ml (_shift_glob): Remove. (senv_lookup): Don't redefine. (ctx_define): New function. (lexp_call): Update to new arg type of lexp_whnf. (lexp_read_pattern): Use ctx_define. (_lexp_rec_decl.tctx): Rename `expr` -> `decl` since it's a declaration. (default_lctx): Use ctx_define.
* src/opslexp.ml (lookup_type, lookup_value): Move earlier. (conv_p'): Use structural equality for sorts. (lexp_whnf): Don't use elab_context since this is also used elsewhere..
- - - - - 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
- - - - - 1d2bbfca by Stefan Monnier at 2016-09-19T17:46:29-04:00 * src/debruijn.ml (elab_context): Rename from lexp_context.
- - - - - b0866ba1 by Stefan Monnier at 2016-09-19T17:52:08-04:00 * src/debruijn.ml (lexp_context): Rename from env_type.
- - - - - 222406c2 by Stefan Monnier at 2016-09-19T18:38:35-04:00 * src/debruijn.ml (lexp_ctx_cons): New fun. Test sanity of `offset`
(M): Alias for Myers, which we don't open any more. (lctx_extend, lctx_extend_rec): New functions. (env_extend): Use them. * src/opslexp.ml (check): Use lctx_extend(_rec).
- - - - - a6e1dc19 by Pierre Delaunay at 2016-09-20T13:07:36-04:00 Added a new way to make tests for eval using a similar mechanism that what is used for sexp
* src/env.ml - new functions (value_equal) and (value_eq_list) * tests/eval_test.ml - new function (test_eval_eqv) - modified tests to use the new mechanism - added 3 new tests on special forms (decltype) (declexpr) and (has-attribute)
- - - - - 2eb9aeee by Pierre Delaunay at 2016-09-20T16:53:19-04:00 Special forms are macros but conv_p does not recognize them as such (db index problem). I have implemented a temporary work around. - src/lparse.ml
- - - - - 66020e6c by Pierre Delaunay at 2016-09-20T16:53:37-04:00 Merge branch 'master' of gitlab.com:monnier/typer
- - - - - e314669e by Pierre Delaunay at 2016-09-25T13:39:35-04:00 Merge branch 'master' of gitlab.com:monnier/typer
- - - - - df72decc by Stefan Monnier at 2016-09-25T21:55:39-04:00 Merge branch 'trunk' into unification
- - - - - fac6cb52 by Stefan Monnier at 2016-09-26T09:30:40-04:00 Allow expressions as constructor names and inductive type refs
* src/lexp.ml (lexp): Allow an lexp for the inductive type arg of Cons. (lexp_unparse): Adjust accordingly. (push_susp): Adjust accordingly. Also merge fix from unification branch.
* src/lparse.ml (_lexp_p_infer): Adjust to new Pcons and Cons (lexp_get_inductive_type): Remove. (lexp_read_pattern): Adjust to new Ppatcons.
* src/opslexp.ml (conv_p', check): Adjust to new Cons.
* src/pexp.ml (ppat): Allow any exp as constructor. (pexp): Allow an exp for the inductive type arg of Cons.
- - - - - a761156c by Stefan Monnier at 2016-09-26T09:50:04-04:00 Merge branch 'trunk' into unification
- - - - - f83ee0b4 by Pierre Delaunay at 2016-09-26T12:05:47-04:00 Merge branch 'master' of github.com:Delaunay/typer
- - - - - 12a677ab by Pierre Delaunay at 2016-09-26T19:27:11-04:00 Try to fix our Macro_ index problem. Nevertheless, it does not work as a lot of index are not computed correctly anymore
* Moved (print_lexp_ctx) from lparse.ml to debruijn.ml to help debugging * src/lparse.ml: types and expression are processed in a different context
- - - - - db617a20 by Pierre Delaunay at 2016-09-26T19:54:32-04:00 Merge with master. Indices seem to be correct. Nevertheles, Macro are still not recognized as such (back to the original issue)
- - - - - e938c998 by Stefan Monnier at 2016-09-26T20:29:14-04:00 Make type levels more canonical
* src/lexp.ml (sort_level): Replace SLn with SLz. (lexp_location, _lexp_to_str): Adjust accordingly.
* src/opslexp.ml (sort_level_max): New function. (sort_compose): Use it. (impredicative_erase): New var. (check): Adjust for new SLz. Obey impredicative_erase. Fix level calculation for inductive types.
* src/builtin.ml (type0, type1, type2): Adjust.
- - - - - 5949b172 by Stefan Monnier at 2016-09-26T20:29:53-04:00 Missing changes in last commit
- - - - - 6d7b4793 by Stefan Monnier at 2016-09-26T20:34:16-04:00 Merge branch 'trunk' into unification
- - - - - 9bb74c93 by Stefan Monnier at 2016-09-29T00:10:31-04:00 * src/opslexp.ml (lookup_type, lookup_value): Move to debruijn.ml
* src/debruijn.ml (_get_env): Remove functions. (env_lookup_by_index, print_lexp_ctx): Change ctx type. (lctx_lookup): Rename from _env_lookup; change ctx type. (lctx_lookup_type, lctx_lookup_value): Move from opslexp.ml; use lctx_lookup. (env_lookup_type, env_lookup_expr): Use them.
- - - - - 6cdee9a8 by Pierre Delaunay at 2016-09-29T00:40:07-04:00 misc
- - - - - f49911fd by Stefan Monnier at 2016-09-29T00:41:49-04:00 * src/lparse.ml (_lexp_p_infer) <Parrow>: Also add anon vars to lctx
* src/debruijn.ml (ectx_extend_anon): New function.
* src/lparse.ml (_type_shift): Remove function. (_lexp_p_infer) <Parrow>: Also add anonymous vars to lctx.
- - - - - e244e3f3 by Pierre Delaunay at 2016-09-29T01:36:19-04:00 Merged
- - - - - 8458627d by Stefan Monnier at 2016-09-29T10:51:32-04:00 * src/lparse.ml (_lexp_rec_decl): Call lexp_p_infer with complete context
This fixes an assertion failure in "EVAL - Mutually Recursive Definition".
- - - - - 3a5fadd4 by Pierre Delaunay at 2016-09-29T11:49:27-04:00 Merge branch 'master' of gitlab.com:monnier/typer
- - - - - ba2917e2 by Pierre Delaunay at 2016-09-29T11:50:04-04:00 Merge branch 'master' of gitlab.com:monnier/typer
- - - - - 40b62b36 by Stefan Monnier at 2016-10-01T22:56:56-04:00 Various fixes to type inference and checking
* src/debruijn.ml (StringMap): Delete. Use util.ml's SMap instead. (ectx_extend_anon): Remove. (ectx_extend): New function to replace it. (ectx_extend_rec): Rewrite, using lctx_extend_rec. (print_lexp_ctx): Drop redundant first column. Improve handling of non-let bindings. (_name_error): Remove function, folded into its sole user.
* src/lexp.ml (push_susp): Fix incorrect handling of Inductive's `args` and reversal of field order. (_lexp_to_str): Add parens around arrows. Add missing cases.
* src/lparse.ml (elab_check_def): New function, extracted from ctx_define.. (ctx_define): Use it. (ctx_define_rec): New function. (_lexp_p_infer) <Pvar>: Don't blindly catch all exceptions. (_lexp_p_infer) <Parrow>: Use ectx_extend. (_lexp_p_infer) <Pinductive>: Fix ordering of args in the computed type. (_lexp_p_infer) <Pcons>: Fix ordering of return type. (lexp_call): Work around conv_p limitation. (lexp_parse_inductive.make_args.loop): Anonymous fields should also be added to the context.
* src/opslexp.ml (get_vardef): New function. (conv_p') <Arrow>: Use it to handle anonymous args. (sort_level_max): Handle Susp args. (check) [Let]: Bring each binding's type into the overall context. (check) [Call]: Reduce to whnf before checking if it's an Arrow. (check) [Inductive]: Check cases in the proper context.
- - - - - a84525ad by Stefan Monnier at 2016-10-01T23:11:33-04:00 Merge branch 'trunk' into unification
- - - - - a37dc44c by Pierre Delaunay at 2016-10-02T02:10:13-04:00 misc
- - - - - 145906d2 by Pierre Delaunay at 2016-10-02T02:10:21-04:00 Merge branch 'master' of gitlab.com:monnier/typer
- - - - - 6ebf2b5f by Pierre Delaunay at 2016-10-02T02:23:58-04:00 misc
- - - - - e134b211 by Stefan Monnier at 2016-10-04T21:04:33-04:00 * src/eval.ml (from_lctx): Rewrite to obey the db_offset
* src/debruijn.ml (lexp_ctx_cons): Tighten the check.
* src/env.ml (value_type): Use runtime_env. (runtime_env): Drop the extra two integers. (env_cell): Make the var's name immutable. (get_rte_variable, get_rte_size, add_rte_variable, print_rte_ctx): Adjust accordingly. (set_rte_variable): Adjust and make return type be unit. (get_rte_size, is_free_var, rte_shift): Remove.
* src/myers.ml (fold_left, fold_right, map, iteri): New functions.
* tests/env_test.ml: Don't use the return value of set_rte_variable.
- - - - - 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
- - - - - 1a68cffc by Stefan Monnier at 2016-10-05T12:42:41-04:00 * src/lparse.ml (_lexp_decls): Rewrite to fix scoping issues
* src/lparse.ml (elab_check_sort, elab_check_proper_type): New functions. (elab_check_def, ctx_define_rec._): Use them to check that the types are proper types. (lexp_detect_recursive, _lexp_rec_decl): Remove. (lexp_check_decls, lexp_decls_1): New functions. (_lexp_decls): Use them instead.
* src/opslexp.ml (check) <Arrow>: Fix incorrect context for target.
* src/util.ml (IntMap): New module.
* src/debug_util.ml (lexp_detect_recursive): Move from lparse.ml.
- - - - - 0bec5cff by Stefan Monnier at 2016-10-05T15:09:46-04:00 Merge branch 'trunk' into unification
- - - - - cee2f8e4 by Stefan Monnier at 2016-10-05T16:29:00-04:00 * src/prelexer.ml (prelex_string): Don't use a temp file
* src/prelexer.ml (prelex): Change input type. (prelex_file, prelex_string): Adjust accordingly.
- - - - - c2626ca7 by Stefan Monnier at 2016-10-05T19:03:01-04:00 Merge branch 'trunk' into unification
- - - - - 74435fef by Pierre Delaunay at 2016-10-05T19:17:45-04:00 * src/eval.ml, src/lparse.ml, src/elexp.ml Added new functions - (lexp_debug_message) - (elexp_debug_message) - (value_debug_message) which prints the type name followed by a value print and an exception. That code was runduntant in a lot of area
* src/lparse.ml New function: - (lexp_expand_macro) Expand a macro given a Lexp.Call (Macro_ fun) This can be used for standard macro as well as for macro declarations. Updated how macro and macro declarations are handled
- - - - - 894dd057 by Stefan Monnier at 2016-10-05T22:36:27-04:00 * src/lparse.ml (lexp_decls_1): Fix inf-loop on structural equality
- - - - - b09b7491 by Pierre Delaunay at 2016-10-05T22:54:29-04:00 * src/lparse.ml - added "add-attribute" implementation that was removed during debugging
- - - - - 53c41e25 by Stefan Monnier at 2016-10-05T23:16:26-04:00 Fix some context and whnf handling in `check`.
* src/debruijn.ml (lctx_extend): Change vdef arg to be an option.
* src/lparse.ml (lexp_decls_1): Fix inf-loop on structural equality. (elab_check_def): Add debug output. Don't call conv_p. (ctx_define_rec): Do check that it's properly typed.
* src/opslexp.ml (check) <Let>, <Lambda>, <Case>: Call lexp_whnf. (check) <Inductive>: Fix context computation for fields.
- - - - - e612a4c9 by Pierre Delaunay at 2016-10-06T15:38:31-04:00 Unified function name. (There were a lot of inconsistency)
* To retrieve the string representation of a tree node use: pretoken_string/sexp_string/pexp_string/lexp_string/elexp_string/value_string
* To retrieve the tree node name use: pretoken_name/sexp_name/pexp_name/lexp_name/elexp_name/value_name
- - - - - be8035b0 by Pierre Delaunay at 2016-10-06T16:10:24-04:00 Updated formating primitive to output a string instead of printing things. This was modified to allow them to be used when writing error messages
Changes to be committed: * src/fmt.ml * src/util.ml - new function (loc_string), changed (print_loc) to (loc_print) for consistency with what is done elsewhere.
- - - - - 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.
- - - - - b57544ca by Stefan Monnier at 2016-10-09T10:46:54-04:00 * src/debruijn.ml (replace_by): Remove, unused
* src/debug_util.ml (mdecl): Move from lparse.ml. * src/lparse.ml (mdecl): Move to debug_util.ml.
- - - - - 2ae5a5ce by Pierre Delaunay at 2016-10-10T16:45:19-04:00 * src/lparse.ml - Updated calltrace system. Eval and Lparse can use the same trace. - Added new debug_message primitive to help print helpful messages. Debugging info is provided as strings and not printed anymore which mean we can create messages we want without constraints. - elab trace is passed to eval when expanding macros.
* src/eval.ml - Moved evaluated builtin function from (src/builtin.ml) to (src/eval.ml)
* src/opslexp.ml - new type (pexporlexp)
* src/elexp.ml - removed old debug_message
* src/REPL.ml * src/debug.ml * src/debug_util.ml - updated to reflect modification
- - - - - 8c6311a9 by Pierre Delaunay at 2016-10-10T16:51:13-04:00 Merge branch 'master' of gitlab.com:monnier/typer
- - - - - 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
- - - - - 5496ae2c by Pierre Delaunay at 2016-10-12T02:10:14-04:00 * new file: samples/error.typer - Erroneous typer code to test out error messages
* src/lparse.ml * src/eval.ml: - tinking with error messages: replaced lexp_error/debruijn_error/eval_fatal/... by simple error/fatal/warning/... - added typer call trace - removed `reset_eval_trace`
* added new functions - value_fatal/elexp_fatal/pexp_fatal/pexp_warning/etc.. Those print an error message then print the expression causing the error. Example:
% [Ln 45, cl 12] ./samples/error.typer % [!] Error LPARSE Lambda require type annotation % > Plambda: (lambda_->_ n n) % > Root: (lambda_->_ n n)
* src/util.ml - removed unused print_trace (old code)
* src/opslexp.ml - Added `pol_string` and `pol_name`
* src/debruijn.ml * src/env.ml - `print_rte_ctx` and `print_lexp_ctx` skip builtins (shorter dump) `dump_rte_ctx` and `dump_lexp_ctx`can be used to print the whole context
* src/REPL.ml - added %typertrace option - `%who` and `%info` use print_..._ctx - `%who all` and `%info all` use dump_..._ctx
- - - - - 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
- - - - - ac07367f by Stefan Monnier at 2016-10-19T14:43:22-04:00 Always `check` rather than `infer` type of `case`
* src/lparse.ml (_lexp_p_infer): Don't try to infer `case`. (_lexp_p_check): Handle `lambda` even when it has a type annotation. Adjust to new `lexp_case` calling convention. (lexp_case): Only handle the `check` case. Simplify accordingly.
* tests/eval_test.ml (Inductive::Case): Move type annotation since `case` can't be inferred any more.
- - - - - df86998f by Stefan Monnier at 2016-10-19T14:46:07-04:00 Merge branch 'trunk' into unification
- - - - - 18f58429 by Stefan Monnier at 2016-10-19T16:15:43-04:00 Get rid of unused `it` field in Case; various extra type checks
* src/lparse.ml (_lexp_p_check): Check the lambda's type annotations are indeed types. (lexp_case): Check that the subject is indeed of inductive type. (lexp_call): Remove unused `from_lctx`. (lexp_read_pattern): Remove unused `exp` arg.
* src/lexp.ml (lexp): Remove unused "base inductive type" field from `Case`.
- - - - - a459a1ea by Stefan Monnier at 2016-10-20T15:28:17-04:00 Fix various typing and inference problems with `Case`
* GNUmakefile (OBFLAGS): Add debug info.
* src/elexp.ml (elexp): Add binding of scrutinee in the default branch. (elexp_string.maybe_str): Adjust print code accordingly.
* src/eval.ml (eval_case): Bind scrutinee in the default branch.
* src/lexp.ml (lexp): Add binding of scrutinee in the default branch. (push_susp, _lexp_to_str): Adjust accordingly. (lexp_unparse): Adjust to pexp changes.
* src/lparse.ml (elab_check_proper_type): Use lexp_print to get db indexes. (ctx_extend): New function. (_lexp_p_infer): Check that arrow's args are types. (lexp_case): Rewrite; fix problems with scoping. (lexp_read_pattern, lexp_read_pattern_args): Remove.
* src/opslexp.ml (lexp_whnf): Adjust to new `Case`. Preserve the non-whnf in the sub-parts we return. (check): Check that erasable inductive type fields have a proper type. Don't assume call_split returns whnf elements. Adjust to new `Case`. (clean_maybe): Adjust to new `Case`.
* src/pexp.ml (ppat): Rename Ppatvar to Ppatsym since it can be either a var or a constructor. Drop arg_kind from Ppatcons. (pexp_p_pat_arg): Only recognize := as explicit-implicit. (pexp_u_pat_arg): Only use := for explicit-implicit.
- - - - - 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.
- - - - - 815b8bce by Stefan Monnier at 2016-10-28T22:06:51-04:00 * src/lparse.ml (_lexp_p_infer): Mostly cosmetic changes
* src/lparse.ml (elab_check_sort, elab_check_proper_type): Make `var` into `option` type. (lexp_type_infer): New function. (_lexp_p_infer): Re-layout and indent. Don't use OL.check to detect user errors. Check that Phastype's annotation is a proper type. (lexp_let_decls): Use fold_right.
* GNUmakefile (BUILDDIR): New var. Use everywhere.
- - - - - 31c63489 by Stefan Monnier at 2016-10-28T23:55:25-04:00 * src/lparse.ml (_lexp_p_infer): Fix return type of `Let`
* src/opslexp.ml (lexp_defs_subst): New function. (lexp_whnf): Return original exp in `Case`. Complete commented out `Let` case.
* tests/eval_test.ml ("Let2"): New test.
- - - - - cf261607 by Stefan Monnier at 2016-10-29T20:18:55-04:00 * src/opslexp.ml (lexp_defs_subst): Fix definition
* src/lparse.ml (elab_check_sort): Improve error message. (elab_check_def): Use better location in error message. (build_var): Remove. (_lexp_p_infer): Improve error message.
- - - - - 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
- - - - - 5cd13387 by Pierre Delaunay at 2016-11-01T12:53:39-04:00 -
- - - - - aaad384e by Stefan Monnier at 2016-11-01T13:12:13-04:00 Merge branch 'trunk' into unification
- - - - - 876a022d by Stefan Monnier at 2016-11-04T13:24:13-04:00 Fix conv_p to unfold variable's definitions
* src/lexp.ml (hc_table, hc): Hash_consing function for lexp. (mkImm, mkSortLevel, mkSort, mkBuiltin, mkVar, mkLet, mkArrow) (mkLambda, mkCall, mkInductive, mkCons, mkCase): New "smart constructor" functions, which perform hash-consing. Use them everywhere. (mkSusp): Make it hash-consing.
* src/lparse.ml (elab_check_def): Do call conv_p now. (lexp_case): Adjust call to conv_p. (lexp_call): Don't bother calling lexp_whnf before conv_p any more.
* src/opslexp.ml (lexp_whnf): Move before conv_p. <Call>: Return e itself instead of reconstructing the same lexp node. <Let>: Handle it. (set_lexp): New type. (set_empty, set_member_p, set_add, set_shift): New functions. (conv_p, conv_p'): Rewrite.
* src/debruijn.ml (env_elem): Use Util.db_offset. (db_idx): Remove, unused.
- - - - - 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.
- - - - - 36b070f5 by Stefan Monnier at 2016-11-06T11:18:40-05:00 * src/lparse.ml (_lexp_p_check): Check inferred type with conv_p
* btl/types.typer (head): Make it total. (tail): Fix up minor type error.
* src/lexp.ml (lexp_unparse): Print `Sort` with more details.
* src/lparse.ml (_lexp_p_check): Check inferred type with conv_p.
* tests/eval_test.ml (Lists): Adjust to new `head` type. (Monads): Fix type arguments.
- - - - - b8dfa7da by Pierre Delaunay at 2016-11-07T13:21:31-05:00 * tests/eval_test.ml - added tests cases for argument reordering and implicit arguments
* src/lparse.ml - added argument reordering
- - - - - 8768911e by Pierre Delaunay at 2016-11-07T13:41:43-05:00 Merging
- - - - - 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
- - - - - 791587e6 by Pierre Delaunay at 2016-11-07T15:47:53-05:00 Changes to be committed: * btl/types.typer - added a new DMacro_ constructor to build declaration macro (DMacro_ : List Sexp -> List Sexp) (Macro_ : List Sexp -> Sexp)
* src/lparse.ml - Lambda Arrow type keep var name when possible (needed for arg re ordering)
* tests/macro_test.ml - Force case to use lexp_check instead of lexp_infer using hastype
- - - - - 07c8e75d by Pierre Delaunay at 2016-11-08T00:06:33-05:00 * src/lparse.ml - use lexp_lwhnf instead of nosusp - correctly renamed variables after some re-re-reading
- - - - - 8dd054b6 by Stefan Monnier at 2016-11-08T10:57:37-05:00 * src/lparse.ml (_lexp_p_check): Check function arg type annotation.
- - - - - 4ea22894 by Pierre Delaunay at 2016-11-08T11:38:22-05:00 fixing db issue when calling OL.lexp_whnf
- - - - - 3502c27e by Pierre Delaunay at 2016-11-08T11:38:59-05:00 Merge branch 'master' of gitlab.com:monnier/typer
- - - - - 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.
- - - - - 1da5866c by Stefan Monnier at 2016-11-09T16:10:48-05:00 * tests/eval_test.ml ("Argument Reordering"): Remove case that we don't want to handle, add case that we want to handle (but that fails now).
- - - - - 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
- - - - - 00232ca1 by Stefan Monnier at 2016-11-11T12:45:13-05:00 Misc minor changes, relating to var names and test names
* src/inverse_subst.ml (counter, impossible): New vars. (mkVar): Give vars a name. (fill.genDummyVar): Use `impossible`.
* src/lparse.ml (_lexp_p_check.unify_with_arrow): Give location and var name in arrow. (lexp_case.check_uniqueness): Use SMap.mem.
* tests/eval_test.ml ("Monads"): Take advantage of type inference.
* tests/inverse_test.ml (generate_tests): Shorten test names.
- - - - - e749bce3 by Stefan Monnier at 2016-11-11T14:05:21-05:00 Move old source files to src/old
- - - - - 3fb126a2 by Stefan Monnier at 2016-11-11T14:17:20-05:00 * src/lparse.ml: Fix missing type error detection after unify
* src/lparse.ml (_lexp_p_check.unify_with_arrow) (lexp_p_infer_and_check): Pay attention to the un-satisfied constraints returned by Unif.unify.
- - - - - db00a5fa by Stefan Monnier at 2016-11-11T15:59:22-05:00 Drop the `trace` arg in lparse
* src/REPL.ml (repl): Remove `%elabtrace`.
* src/debug_util.ml (main.lexps): Don't print elabtrace.
* src/eval.ml (eval_debug_info): Just use elexp rather than pexporlexp. (append_eval_trace, root_string, print_eval_result): Adjust accordingly.
* src/lparse.ml (root_string, _global_lexp_trace): Remove. (debug_message): Don't print "root string" any more. (infer): Rename from _lexp_p_infer. Drop `trace` arg. (infer_type): Rename from lexp_type_infer. (check): Rename from _lexp_p_check. Drop `trace' arg. (infer_and_check): Rename from lexp_p_infer_and_check. (check_case): Rename from lexp_case. (infer_call): Rename from lexp_call. (lexp_parse_inductive): Check that field types are indeed types. (lexp_p_decls): Rename from _lexp_decls. (lexp_decls_toplevel, print_lexp_trace, lexp_p_check, lexp_p_infer): Remove. (lexp_parse_all): Rename from _lexp_parse_all.
* src/opslexp.ml (pexporlexp): Remove type. (pol_string, pol_name): Remove.
- - - - - 0a167d0a by Stefan Monnier at 2016-11-11T17:33:42-05:00 Instantiate implicit args when there's no function call
* src/lexp.ml (mkCall): Canonicalize. * src/lparse.ml (infer.target): Simplify accordingly. (instantiate_implicit): New function. (infer_and_check): Use it.
* src/opslexp.ml (check.call_split): No need for recursion.
* btl/types.typer (length, head, tail): Remove unneeded explicit args.
- - - - - 108275af by Stefan Monnier at 2016-11-14T19:37:13-05:00 Switch metavars to use ?<name> instead of _
* DESIGN: Use org-mode to highlight URLs.
* src/builtin.ml: Don't open `Debruijn`. Hash-cons predefined sorts.
* src/debruijn.ml (level0): Move from src/builtin.ml. (type0): Hash-cons it.
* src/eval.ml (print_eval_result): Remove unused `lexp-trace` var.
* src/inverse_subst.ml (impossible): Silence compiler warning.
* src/lexp.ml (push_susp): Fix SortLevel induction. Fix missing hash-cons of `Let`. (clean): New function. (lexp_unparse): Print metavars with their substitution. (subst_string): Print shifts more like we used in the article.
* src/lparse.ml (elab_check_sort, elab_check_def): Use `clean` to replace instantiated metavars in error message. (newMetavar): Add `l` and `name` args. (newMetalevel, newMetatype): Update accordingly. (infer_type): Try to unify with `Sort` before signaling an error. (infer_call): Remove redundant `nosusp`.
* src/opslexp.ml (conv_p'): Minor simplification.
* src/pexp.ml (pexp_parse): Don't treat `_` as metavar. Treat any var starting with `?` as a metavar instead.
* tests/eval_test.ml ("Metavars"): New test.
- - - - - eb54a39b by Stefan Monnier at 2016-11-15T10:07:37-05:00 * src/lparse.ml (fold_fun.add_branch): Support explicit field patterns
* tests/eval_test.ml ("Explicit field patterns"): New test. (bool_decl): Remove.
- - - - - 9853ee47 by Stefan Monnier at 2016-11-15T15:44:44-05:00 Fix some issues with case handling in lparse and eval
* src/eval.ml (eval_case): Do add anonymous pattern args to context. Otherwise, deb-indices are wrong!
* src/lparse.ml (fold_fun.add_branch.make_nctx): Don't take unrelated explicit pattern arg when we expect a normal pattern arg. Detect when we don't have enough pattern args. (infer_call.handle_fun_args): Allow (_ := ...) also for anonymous normal args.
* tests/eval_test.ml ("Explicit field patterns"): Add more cases.
- - - - - a20dd18a by Pierre Delaunay at 2016-11-15T19:46:00-05:00 Modified how properties are handled
* src/lexp.ml - Added a new lexp `AttributeTable` - Modified multiple functions to handle the new lexp * src/lparse.ml - moved special forms implementation from builtin.ml to lparse.ml (circular reference issue) - probably that builtin.ml will be removed soon - finished the implicit arguments lookup * btl/types.typer - called our attribute table simply `Attribute` * src/opslexp.ml: - replace `AttributeTable` by a dummy during type erasure * src/debruijn.ml - removed old property_environment and related functions
- - - - - fdcdf103 by Stefan Monnier at 2016-11-15T23:04:44-05:00 Add support -escaping chars; drop _ stickiness
* doc/manual.texi (Lexing): Document 's new meaning.
* src/lexer.ml (unescape): New function. (nexttoken): Don't treat _ specially. Instead add support -escaping chars in symbols.
* src/prelexer.ml (prelex): Add support -escaping chars.
* tests/sexp_test.ml: Test handling of -escapes in symbols.
- - - - - 79483aee by Stefan Monnier at 2016-11-16T12:33:09-05:00 * tests/inverse_test.ml: Simplify and shorten output
* tests/inverse_test.ml (is_identity): Use S.identity_p. (generateRandInput): Return same type as `input`. (inv_add_test): New function.
- - - - - df369e18 by Stefan Monnier at 2016-11-16T13:40:14-05:00 (check): Check exhaustiveness of `Case`
* src/opslexp.ml (assert_type): Re-enable but move into `check`.
- - - - - 766a7745 by Pierre Delaunay at 2016-11-16T14:06:35-05:00 Merging, adapt implicit arg lookup to the new argument reordering algorithm
- - - - - 2fadd29b by Pierre Delaunay at 2016-11-16T14:08:39-05:00 Merge branch 'master' of gitlab.com:monnier/typer
- - - - - a93d6441 by Stefan Monnier at 2016-11-18T14:21:13-05:00 * src/lexer.ml (nexttoken.lexsym): Implement the CKinner feature
* tests/sexp_test.ml: Add tests for the CKinner feature. Fix non-escape backslash in tests.
- - - - - 651ff998 by Stefan Monnier at 2016-11-18T19:20:04-05:00 * src/opslexp.ml (check): Allow string constants.
- - - - - 7868f806 by Stefan Monnier at 2016-11-19T10:39:30-05:00 * src/opslexp.ml (check): Fix minor issues with hierarchy checks.
- - - - - 6be3fe06 by Pierre Delaunay at 2016-11-21T02:10:56-05:00 Minor changes
- - - - - 801d9547 by Pierre Delaunay at 2016-11-21T02:11:19-05:00 Merge branch 'master' of gitlab.com:monnier/typer
- - - - - 08bee479 by Pierre Delaunay at 2016-11-21T02:54:20-05:00 * src/util.ml: Fatal error messages are not printed twice anymore * src/lexp.ml: lexp.AttributeTable was merged with lexp.Builtin
- - - - - d75bf004 by Stefan Monnier at 2016-11-21T13:11:25-05:00 * src/opslexp.ml (check): Fix typo in last commit.
- - - - - 44f27a47 by Pierre Delaunay at 2016-11-21T14:40:37-05:00 Merge branch 'master' of gitlab.com:monnier/typer
- - - - - 9fea6e8c by Pierre Delaunay at 2016-11-22T13:08:30-05:00 * tests/eval_test.ml: delete infinite recursion failure test * src/lparse.ml: removed duplicate newlines
- - - - - 7d77e891 by Pierre Delaunay at 2016-11-23T01:24:42-05:00 * src/lexp.ml: push susp inside attribute table
- - - - - 79d18902 by Stefan Monnier at 2016-11-23T23:24:09-05:00 Typecheck non-recursive Plet, as well as interactive exps
* src/REPL.ml (ilexp_parse): Check exps before running them.
* src/inverse_subst.ml (impossible): Move to lexp.ml.
* src/lexp.ml (impossible): Move from inverse_subst.ml. (push_susp): Fix the "plain" Builtin, along the line of the recent fix for the attributemap case.
* src/builtin.ml (declexpr_impl, decltype_impl): Only return a lexp, not its type.
* src/lparse.ml (elab_check_sort, elab_check_def): Add some debug prints. (infer_call): Compute the type of get_macro_impl's returned lexps. (lexp_decls_1): Typecheck non-recursive let-bindings. (is_builtin_macro): Use SMap.mem. (new_attribute_impl, add_attribute_impl, get_attribute_impl) (has_attribute_impl): Only return a lexp, not its type.
* src/opslexp.ml (check): Fix return type of `Let`. Fix scoping of the computed type of `Arrow`. Fix DB indices of the return type of `Cons`.
- - - - - 183cf9cd by Stefan Monnier at 2016-11-24T10:45:13-05:00 * src/lparse.ml (_lexp_expr_str): Typecheck the expressions
* src/debug.ml (debug_pexp_print): Use pexp_name.
* src/lexp.ml (push_susp.): Fix longstanding typo.
* src/lparse.ml (default_rctx): Use from_lctx. (_lexp_expr_str): Typecheck the expressions.
- - - - - 2a56c805 by Stefan Monnier at 2016-11-24T11:03:43-05:00 (check): Check that eraseable args are indeed erasable (bugit#4)
* src/builtin.ml (level[012], type[012], type_omega, type_level) (type_float, type_int, type_string): Move to debruijn.ml.
* src/debruijn.ml (set): New type. (set_empty, set_mem, set_set, set_sink): New functions for it.
* src/opslexp.ml (dbset_push): New function. (check): Check that eraseable args are indeed erasable. Check proper types more systematically.
- - - - - f9a5b2f2 by Stefan Monnier at 2016-11-26T11:23:49-05:00 Add new ##... syntax to refer to existing builtins
* src/builtin.ml (lmap): New var. (add_builtin_cst): New function.
* src/lexp.ml (mkSusp): Don't bother suspending immediates. (lexp_unparse): Use Pbuiltin. (_lexp_to_str): Use the ##... syntax.
* src/lparse.ml (macromap): Adjust to earlier change. (make_macro_map): Use it. (infer): Handle Pbuiltin.
* src/pexp.ml (pexp): Add Pbuiltin constructor. (pexp_parse): Recognize new ##... syntax. (pexp_location, pexp_unparse): Handle it.
* src/prelexer.ml (string_sub): Move to util.ml.
- - - - - 02dabd43 by Stefan Monnier at 2016-11-28T10:01:45-05:00 Use ##... for types. Don't use `Macro` for special forms
* btl/unit.typer, btl/list.typer, btl/macro.typer: Remove, unused. * btl/builtins.typer: Rename from types.typer. (Unit): Define as inductive, rather than builtin. (unit): New predefined constant. (Int, Float, String, Sexp, Context, IO, FileHandle, Attribute): Remove built-in types, now declared in OCaml. (new-attribute, get-attribute, has-attribute, add-attribute, decltype) (declexpr): Remove special forms, now declared in OCaml.
* src/builtin.ml (predef_name): Remove "Attribute", unused. (add_builtin_type): New function. Add all builtin sorts and types.
* src/debruijn.ml (sort_level): Rename from type_level. (sort_omega): Rename from type_omega. (type_level): New type.
* src/lparse.ml (macromap): Move. (special_forms): Rename from make_macro_map; make it a ref cell rather than a function of no arguments. (type_special_form): New built-in type. (add_special_form): New function. (get_special_form): Rename from get_macro_impl, rewrite. (infer_call.handle_funcall): Use mkBuiltin. Remove the single-arg form of `Built-in`. (infer_call): Don't use the `Macro` to indicate a special form. (builtin_macro, is_builtin_macro): Remove. (<toplevel>): Register special forms. (default_lctx): Add entries predefined in BI.lmap. before loading types.typer.
* src/opslexp.ml (conv_p) <Inductive>: Fix scoping of fields. (sort_level_max): Hash-cons return value. (check'): Check the type provided to `Builtin`. Hash cons the sorts as well. (erase_type): Silence compiler warning.
- - - - - 1e05e7c1 by Stefan Monnier at 2016-11-28T11:42:57-05:00 Fix WHNF of Let and recognize negative integers
* src/lexer.ml (nexttoken): Recognize negative integer.
* src/opslexp.ml (lexp_whnf): Really return WHNF for `Let`.
* tests/eval_test.ml ("Let"): Use negative integer, to test them. ("Lists"): Add tests using a different definition of List.
- - - - - 7443ad30 by Stefan Monnier at 2016-11-28T13:14:13-05:00 Change special forms's args to be sexps rather than lexps
* src/builtin.ml (declexpr_impl, decltype_impl): Move to lparse.ml.
* src/lparse.ml (special_forms_map): Rename from macromap. Change special forms's args to be sexps rather than lexps. Adjust all users accordingly. (lexp_parse_all): Rewrite using List.map. (lexp_parse_sexp): New function.
- - - - - 7535ecf7 by Stefan Monnier at 2016-11-28T13:23:40-05:00 * src/lparse.ml (special_forms): Remove last arg, move context 1st
- - - - - 43ddd912 by Stefan Monnier at 2016-11-28T13:31:18-05:00 * src/lparse.ml: Rewrite "Built-in" as a special form
* src/lparse.ml (handle_funcall): Don't treat `Built-in` specially. (sform_built_in): New function. (special_forms): Use it. (default_lctx): Remove manual construction of "Built-in" builtin.
- - - - - 8396dc22 by Stefan Monnier at 2016-11-29T13:31:20-05:00 Make `Builtin`s be closed and available via ##... syntax
* src/builtin.ml (type_eq, olist2tlist_lexp): Add missing hashconsing.
* src/lexp.ml (mkSusp): Don't make a susp for Builtins. (push_susp): Builtins are closed, so there's nothing to push anything.. (eq, subst_eq): New functions.
* src/lparse.ml (newMetalevel): Add missing hashconsing. (sform_built_in, sform_new_attribute): Close type of builtin. (sform_built_in): Add to BI.lmap so it's available via the ##... syntax. (sform_add_attribute): Close attr before adding it to table.
* src/opslexp.ml (lctx_to_subst, lexp_close): New functions. (set_plexp): Rename from set_lexp, change it to hold pairs. (set_member_p, set_add): Rewrite. (conv_p'): Use a set of hypothetical equalities to break inf-loops. Add missing hashconsing. * src/unification.ml (unify'): Mirror change in OL.conv_p'.
- - - - - cee10e51 by Pierre Delaunay at 2016-11-29T14:10:27-05:00 Little modifications
- - - - - af1634f0 by Pierre Delaunay at 2016-11-29T14:11:03-05:00 Merge branch 'master' of gitlab.com:monnier/typer
- - - - - 96d9936b by Stefan Monnier at 2016-11-30T12:11:59-05:00 * src/eval.ml: Don't pass `ctx` to builtins
(none_fun): Remove, unused. (typer_eval): Remove function and corresponding builtin. (_builtin_lookup): Change type.
- - - - - cda68e29 by Stefan Monnier at 2016-11-30T13:43:14-05:00 Fix partial application of builtins
* src/eval.ml (builtin_functions): Rename from _builtin_lookup. Add arity info for each primitive. (add_builtin_function): New function. (_eval): Eval `Call` args before calling eval_call. (get_predef_eval): Remove unused. (eval_call): Rewrite. Signal an error if a builtin throws an exception: since Typer's language is total this should only happen if there's a bug in Typer's own code. (bind_impl): Use eval_call; simplify. (get_builtin_impl): Remove. Pre-fill builtin_functions instead.
* src/elexp.ml (elexp_string): Add deb-indices in output.
* tests/eval_test.ml ("Partial Application"): Also test partial application of builtins.
- - - - - 133a2261 by Stefan Monnier at 2016-11-30T17:28:01-05:00 Streamline the integer binary ops slightly
* btl/builtins.typer (_+_, _*_): Adapt to new builtin names. (_-_, _/_): New builtins.
* src/eval.ml (add_binary_iop): Rename from _generic_binary_iop; Rewrite. Register the primitive into builtin_functions. (iadd_impl, isub_impl, imult_impl, idiv_impl): Don't give them names. (typer_builtins_impl): Remove. (<toplevel>): Don't manually add _+_ and _*_ to builtin_functions.
* src/lparse.ml (sform_built_in): Check builtin_functions to make sure the built-in actually exists.
- - - - - d760340d by Pierre Delaunay at 2016-12-01T03:49:10-05:00 Merge branch 'master' of gitlab.com:monnier/typer
- - - - - d63348a8 by Pierre Delaunay at 2016-12-01T05:41:23-05:00 * src/eval.ml: fixed trace issue - when function calls were evaluated arguments trace evaluation was not kept which made trace very short and not representative of the work that has been made by the interpreter.
* src/lexp.ml: added missing `lexp_name` cases and removed catch-all case
- - - - - 0aa7e076 by Stefan Monnier at 2016-12-01T22:32:38-05:00 Simplify predef slightly
* src/builtin.ml (predef_table): Remove type. (default_predef_map): Remove variable. (predef_map): Change type. Pre-fill with `Macro`. (get_predef_raw, get_predef_option, dump_predef, is_lbuiltin): Remove functions. (get_predef): Catch errors. (set_predef): Rewrite.
* src/lexp.ml (lexp_unparse): Use Pbuiltins for Sorts. (_lexp_to_str): Improve handling of SLsucc and Stype.
* src/lparse.ml (infer_call): Use BI.get_predef. (default_lctx): Adjust to new set_predef.
* src/opslexp.ml (check'): Catch case of Cons of a wrong label.
- - - - - 49630b31 by Stefan Monnier at 2016-12-01T22:52:36-05:00 * src/lexp.ml (sort_level): Add SLlub
* src/opslexp.ml (level_canon, level_leq): New functions. (mkSLlub): New function, to replace sort_level_max. (sort_compose): Use it. Add ctx args. (check'): Use it as well.
* tests/eval_test.ml ("Partial Application"): Use negation to make sure the args are passed in the right order.
- - - - - afa9309b by Stefan Monnier at 2016-12-02T09:11:41-05:00 Rewrite inductive-cons as a special-form; rename to datacons
* src/lparse.ml (infer): Remove Pcons case. (sform_datacons, sform_type): New functions. (register_special_forms): Name the initialization code. Use the two new sform_* functions. (dynamic_bind): New function. (default_lctx): Use them.
* src/pexp.ml (pexp): Remove Pcons.
* src/lexp.ml (pdatacons): New var. (lexp_unparse, lexp_unparse): Use it.
- - - - - 65acc4ec by Stefan Monnier at 2016-12-02T10:21:43-05:00 Keep uppercase for types
* btl/builtins.typer (Void, False, True, Not, Decidable): New types. (true, false, some, none): Lowercase the name.
* samples/test.typer: Remove.
* src/builtin.ml (predef_name): Remove Unit and Bool. Adjust to new bool names. (o2l_bool): New function. (o2l_list): Rename from olist2tlist_lexp. Switch arg order. (o2v_list): Rename from olist2tlist_rte. (v2o_list): Rename from tlist2olist. Drop first arg.
* src/eval.ml (o2v_bool): Rename from btyper.
* src/lparse.ml (sform_has_attribute): Use `mem` and o2l_bool.
- - - - - 411ba805 by Stefan Monnier at 2016-12-02T11:23:22-05:00 Add Eq type
* btl/builtins.typer (Eq_refl, Eq_cast, Eq_comm): New definitions.
* src/builtin.ml (type_eq): Fix level of return value. (register_builtin_types): Add "Eq".
* src/eval.ml (arity0_fun, nop_fun): New functions. (register_built_functions): Use them for Eq.refl, Eq.cast.
* tests/eval_test.ml ("Equalities"): New test.
- - - - - 1a4d46c6 by Pierre Delaunay at 2016-12-04T11:26:57-05:00 updated quote and type_ example
- - - - - 40a83aac by Pierre Delaunay at 2016-12-04T12:39:43-05:00 * src/eval.ml: fixed sexp_dispatch implementation (was evaluating with the wrong context) * Merging
- - - - - 06bd99aa by Stefan Monnier at 2016-12-04T23:11:07-05:00 * src/lparse.ml: Fix handling of trailing explicit-implicit args
(infer_call.handle_fun_args): Fix handling of trailing explicit-implicit args.
* tests/eval_test.ml ("Equalities"): * btl/builtins.typer (Eq_comm): Remove unneeded explicit-implicits.
- - - - - 968b81e0 by Stefan Monnier at 2016-12-04T23:38:13-05:00 Make default attributes work for erasable args
* src/lparse.ml (get_implicit_arg): New fun, extracted from handle_fun_args. (instantiate_implicit, infer_call.handle_fun_args): Ue it. (get_attribute): Return an option. (sform_get_attribute): Explicitly handle failure.
- - - - - c8d9a873 by n3f4s at 2016-12-05T15:23:57+01:00 read CTRL-d (EOF) as "%quit" in REPL
makes the REPL always exit when typing C-d
- - - - - 42ae69a5 by Stefan Monnier at 2016-12-05T09:34:31-05:00 * src/lparse.ml (lexp_check_decls): Provide previous defs during elab
* src/myers.ml (set_nth): New function. * src/opslexp.ml (check'): Check `Let` defs within themselves!
- - - - - d81d6755 by Stefan Monnier at 2016-12-05T12:00:55-05:00 * src/lexp.ml (hc): Reimplement using a *weak* set
* emacs/typer-mode.el: Move to its own subdirectory. * src/tweak.ml: New file, copied from OCaml's distribution.
- - - - - 42923f80 by Stefan Monnier at 2016-12-05T20:52:17-05:00 Only evaluate closed expressions in from_lctx
* src/debruijn.ml (set_singleton, set_union): New functions.
* src/env.ml (value_type): Add `Vundefined`. (print_rte_ctx): Drop hardcoded magic number.
* src/eval.ml (from_lctx): Rewrite. (roname, ctx_memo, closed_dbset_p, closed_p): New functions. (from_ectx): New function to replace the old misnamed from_lctx.
* src/lparse.ml (default_ectx): Rename from default_lctx.
* src/opslexp.ml (mv_set): New type. (list_union, mv_set_empty, mv_set_add, mv_set_union, fv_memo) (fv_empty, fv_union, fv_sink, fv_hoist, fv): New functions.
* tests/macro_test.ml ("macros base"): Move macro call to within a function, to test the handling of variables in the context.
* .gitignore: Add patterns for ELPA files.
- - - - - c5c90c6f by Stefan Monnier at 2016-12-06T22:57:47-05:00 Fix types with multiple args; refine closedness test
* GNUmakefile (OBFLAGS): Use `-tag`.
* btl/builtins.typer (expand_dmacro_): Remove redundant explicit args. (sexp_dispatch_): Name the arguments.
* emacs/typer-mode.el (typer-smie-rules): Tweak rule for `=`.
* src/eval.ml (not_closed): Rename from closed_dbset_p. Return a list. (from_lctx): Add `meta_ctx` arg. `clean` exps before passing to `fv`.
* src/lexp.ml (push_susp) <Inductive>: Don't reverse type's args. <Case>: Don't skip unnamed fields. (clean) <Let>: Fix up typo. <Inductive>: Don't reverse type's args. <Case>: Don't skip unnamed fields.
* src/lparse.ml (check_case.add_branch): Substitution was built in the wrong order. (lexp_expand_macro_): Check closeness of the macro definition.
- - - - - 916549b4 by Stefan Monnier at 2016-12-06T23:19:43-05:00 Infer the inductive type of pattern constructors
* src/lparse.ml (check_case.add_branch): Unify rather than test inductive type of the pattern. (infer_call): Use get_type.
* src/opslexp.ml (get_type): New function.
* tests/eval_test.ml ("Generic-typed case"): New test.
* tests/macro_test.ml: Remove redundant explicit type args.
- - - - - f19ead0d by Stefan Monnier at 2016-12-07T15:33:18-05:00 Handle special forms and macros in `check` as well
* src/lparse.ml (dlxp, dltype): Remove. (sform_type): New datatype. (special_forms_map): Make the functions return it and optionally take the expected type as well. (get_special_form): Don't catch errors. (newMetatype): Take a `loc` argument as well. (mkDummy_type, mkDummy_check, mkDummy_infer): New functions. (infer) <Pcall>: Check the type a dispatch for special-forms or macros. (parse_special_form): New function, extracted from infer_call. (get_implicit_arg): Pass expected type to lexp_expand_macro. (check) <Pcall>: Handle it as well. (check_inferred): New function extracted from infer_and_check. (infer_and_check): Use it. (handle_macro_call): Extract from infer_call. (infer_call): Remove the macro and special-form handling. (lexp_parse_inductive.make_args.loop): Pass actual type to ectx_extend. (lexp_expand_macro): Add expected-type argument. (track_fv): New function. (lexp_expand_macro_): Use it to give more complete error message. (sform_*): Adjust to new calling convention. (default_rctx): Pass the actual meta_ctx!
* src/debruijn.ml (dltype): Remove.
- - - - - d377f901 by Pierre Delaunay at 2016-12-08T10:01:37-05:00 * src/eval.ml: fixed sexp_dispatch implementation (was evaluating with the wrong context) * Merging
- - - - - 461aff50 by Pierre Delaunay at 2016-12-08T10:03:19-05:00 Merge
- - - - - 9c9a1a0e by Stefan Monnier at 2016-12-13T13:09:11-05:00 Add the Y operator in a safe(?) way
* btl/builtins.typer (Y): Give its type.
* src/eval.ml (y_operator): New function. (register_built_functions): Add "Y" operator.
* tests/eval_test.ml ("Y"): New test.
- - - - - 409f7728 by Pierre Delaunay at 2016-12-15T00:12:39-05:00 Merge branch 'master' of gitlab.com:monnier/typer
- - - - - f4630a76 by Stefan Monnier at 2016-12-15T09:25:53-05:00 Rename `inductive_` to `typecons` and make it a special-form
* src/lexp.ml (ptypecons): New var. (lexp_unparse): Don't use Pinductive.
* src/lparse.ml (infer): Move Pinductive case to sform_typecons. (sform_typecons): New function. (register_special_forms): Add it.
* src/pexp.ml (pexp): Remove Pinductive. (pexp_parse): Don't recognize `inductive_` any more. (pexp_unparse): Move Pinductive case to lexp_unparse.
* src/tweak.ml (Make.create): Use new name Array.make.
- - - - - a2986fcc by Pierre Delaunay at 2016-12-17T12:34:53-05:00 * btl/builtins.typer: removed `DMacro_` as DMacro now retruns a single Sexp. * src/lparse.ml: removed `expand_dmacro` * tests/macro_test.ml: updated test * samples/inductive.typer: updated example * src/debruijn.ml: removed variable shadowing warning
- - - - - ce0dfdc4 by Pierre Delaunay at 2016-12-17T12:42:50-05:00 Merging
- - - - - e9d8852d by Pierre Delaunay at 2016-12-17T13:08:12-05:00 * src/lparse.ml: when an error occur during macro expansion (after getting the sexp but before pexp_parse) the generated sexp is printed
- - - - - 05b1ad07 by Pierre Delaunay at 2016-12-18T23:18:58-05:00 * src/lexp.ml: modified lexp_string so metavar's result is printed instead of metavar. Helps when debug printing * src/lparse.ml: moved `global_substitution` to `src/lexp.ml` so the context can be used when printing lexp * samples/dependent.typer: fixed some issues, the example is almost working (inference issue I think) * samples/acc.typer: new list functions
- - - - - 66730d6d by Stefan Monnier at 2016-12-19T11:30:12-05:00 * src/lparse.ml (lexp_expand_macro): Use `eval-call`.
The main purpose of this is to avoid converting the `sexp list` of args to a `lexp list` on its way to a `value_type list` since conversion from lexp to value_type doesn't always create a Vsexp.
* src/builtin.ml (o2l_list): Remove.
* src/lparse.ml (lexp_eval): New function, extracted from lexp_expand_macro. (lexp_expand_macro): Use it. Add `loc` argument. Use `eval_call`.
- - - - - 1fd2d612 by Stefan Monnier at 2016-12-19T13:34:24-05:00 * src/opslexp.ml (check'): Check Metavar's type annotation.
* src/opslexp.ml (conv_p'): Add partial support for SortLevel's SLlub.
* src/lparse.ml (newMetalevel, newMetatype): Fix thinko's. (lexp_decls_macro): Use pexp_p_decls.
* src/unification.ml (_unify_metavar): Also unify the var's type. Furthermore, when unifying two metavars, try it both ways.
- - - - - d919cdd9 by Pierre Delaunay at 2016-12-19T15:42:41-05:00 modified lexp_string so metavar's result is printed instead of (?a...). Helps when debug printing
* src/lexp.ml: modified lexp_string * src/lparse.ml: moved `global_substitution` to `src/lexp.ml` so the context can be used when printing lexp * samples/dependent.typer: fixed some issues * samples/acc.typer: new list functions
- - - - - 3a41b28f by Pierre Delaunay at 2016-12-19T15:43:05-05:00 Merge branch 'master' of gitlab.com:monnier/typer
- - - - - eaa9b404 by Pierre Delaunay at 2016-12-19T20:42:07-05:00 new printing context, easier to modify
* src/lexp.ml: new printing context
- - - - - bd953f6d by Pierre Delaunay at 2016-12-20T16:37:31-05:00 Moved `quote` `list` `type` to BTL as those will soon belong to the default context
* samples/dependent.typer: updated example (Eq_cast) * src/lexp.ml: fix printing bug that caused function's name to be printed as `__` - added the option to print or not erasable and implicit arguments * src/lparse.ml: tries to read multiple BTL files but it is buggy
- - - - - 8cc696db by Pierre Delaunay at 2016-12-20T16:43:45-05:00 Merge
- - - - - c7ec8cf2 by Pierre Delaunay at 2016-12-26T11:54:38-05:00 added a new example `samples/io.typer`
- - - - - 84313d0d by Stefan Monnier at 2017-02-10T23:48:01-05:00 Rename vdef to vname
- - - - - fbffe328 by Stefan Monnier at 2017-02-11T20:15:49-05:00 * src/debruijn.ml (lctx_view): New function
(lct_view): New type. * src/opslexp.ml (lctx_to_subst): * src/eval.ml (from_lctx): Use it.
- - - - - 0bd0dac5 by Stefan Monnier at 2017-02-13T15:40:25-05:00 * src/sexp.ml (sexp): Remove Epsilon. Use empty Symbol instead
(epsilon, dummy_epsilon): New definitions. (sexp_string, sexp_location, sexp_name, sexp_parse.mk_node) (sexp_p_list, sexp_u_list, sexp_equal): * src/pexp.ml (pexp_parse, pexp_p_decls): * src/opslexp.ml (check', get_type): * src/lexp.ml (impossible): * src/lexer.ml (nexttoken.lexsym.mksym, nexttoken.lexsym.lexsym'): * src/debug.ml (debug_sexp_print): Adjust users accordingly.
- - - - - 129d4b0e by Pierre Delaunay at 2017-02-19T10:49:29-05:00 Type aliasing `ListInt = Lis Int;` does not produce an (eval) error anymore
* tests/eval_test.ml: Added test for type aliasing * src/env.ml: Added a `Vinductive` value to detect type aliasing calls * src/eval.ml: type aliasing calls to constructor are recognized and not evaluated * src/REPL.ml: file provided using the command line are read in the correct order * samples/typer_proof.typer: Added a new example `samples/typer_proof.typer` which implements a Tree based interpreter and a Stack VM.
- - - - - a6aff881 by Pierre Delaunay at 2017-02-19T10:55:07-05:00 Merge branch 'master' of gitlab.com:monnier/typer
- - - - - 2b74a79a by Stefan Monnier at 2017-02-23T17:34:23-05:00 * src/env.ml (value_type) <Vtype>: New, replaces Vdummy and Vinductive
(value_equal): Adjust accordingly. Emit a warning for Vundefined.
* src/eval.ml (make_symbol, make_string, make_integer): Simplify. (make_float): Implement. (make_block): Comment out. (read_impl, write_impl): Simplify. (eval_call): Adjust Vinductive case to the new Vtype and tweak it so that the result can itself be passed to eval_call, in case the inductive type is applied to more than one argument. (_eval_decls, y_operator): Use Vundefined instead of Vdummy. (register_built_functions): Comment out `block_`.
* src/lexp.ml (_lexp_str): Remove unreachable case. (lexp_str.septp): Remove, unused.
* btl/builtins.typer (block_): Comment out, not implemented.
* src/elexp.ml (elexp): Unify Type and Inductive. Keep lexp in `Type`.
* tests/env_test.ml (_.rctx): Use Vundefined instead of Vdummy.
- - - - - f5cb3ff0 by Stefan Monnier at 2017-02-24T00:37:39-05:00 * btl/quote.typer: Simplify/rework
- - - - - dec52d81 by Stefan Monnier at 2017-02-24T09:49:52-05:00 * btl/pervasive.typer: New file, combining type.typer and quote.typer
* btl/quote.typer, btl/type.typer: Remove. * emacs/typer-mode.el (typer-outline-regexp): Change default. * src/lparse.ml (default_ectx): Read btl/pervasive.typer after builtins. (default_ectx.read_file): Don't bind _parsing_internals here any more..
- - - - - 36c64913 by Stefan Monnier at 2017-02-24T10:05:27-05:00 * emacs/typer-mode.el (typer-font-lock-keywords): Highlight section titles (typer--section-face): New function.
- - - - - 0bb921c9 by Stefan Monnier at 2017-02-24T15:04:21-05:00 Wholesale renaming
Try and follow the convention: - types and "modules" are capitalized. - functions and constructors are lower case. - in the absence of actual modules, use <module>_<name>.
- - - - - 53de7a6a by Stefan Monnier at 2017-02-24T20:04:28-05:00 * emacs/typer-mode.el (typer-smie-rules): Improve indentation of "type".
- - - - - 19d130e6 by Stefan Monnier at 2017-02-24T20:14:00-05:00 * src/elexp.ml (elexp): Add comments.
- - - - - a016490c by Stefan Monnier at 2017-02-26T08:20:29-05:00 Add various primitives; fix various monad bugs
- - - - - 117d4d4c by Stefan Monnier at 2017-02-27T16:19:00-05:00 Integrate misc changes from the ift3065 assignments
* btl/pervasive.typer (List_foldl): New function. * btl/list.typer: Remove.
* emacs/typer-mode.el (typer-font-lock-keywords): Highlight "keywords".
* src/REPL.ml (arg_batch): New var. (arg_defs): Add --batch arg. (main): Obey it.
* src/elexp.ml (elexp_string): Print data constructors more explicitly.
* src/env.ml (env_cell): Remove.
* src/eval.ml (_eval, io_run): Silence compiler warnings.
- - - - - 36afff9d by Stefan Monnier at 2017-02-27T20:42:38-05:00 * src/pexp.ml (pexp): Remove Pbuiltin
Use a Pvar starting ith "##" instead.
- - - - - 3a54a263 by Stefan Monnier at 2017-02-27T20:56:07-05:00 * src/pexp.ml (pexp): Remove Pmetavar
Use Pvar with a leading ? instead. Reserve identifiers starting with # for future use.
- - - - - fa5e92ad by Stefan Monnier at 2017-02-27T21:08:16-05:00 * src/lparse.ml (sform_hastype): New function
(register_special_forms): Record it. * src/pexp.ml (pexp): Remove Phastype.
- - - - - baf904f3 by Stefan Monnier at 2017-02-27T21:16:37-05:00 * src/pexp.ml (pexp): Remove Pvar
Use `Pimm (Symbol ..)` instead.
- - - - - b035fe3e by Stefan Monnier at 2017-02-27T21:33:29-05:00 * src/lparse.ml (sform_arrow): New special form
(register_special_forms): Register it under all three names.
* src/pexp.ml (pexp): Remove Parrow.
- - - - - b3b5b11f by Stefan Monnier at 2017-02-28T00:59:56-05:00 * src/lparse.ml (sform_lambda): New function
(parse_special_form): Pass `ot` to the special form. (elaborate): New function. (register_special_forms): Register it under all three names.
* src/pexp.ml (pexp): Remove Plambda.
- - - - - 5aff0bb4 by Stefan Monnier at 2017-02-28T01:11:29-05:00 * src/pexp.ml (pexp): Remove Pcall
Use `Pimm (Node ..)` instead.
- - - - - 61d04393 by Stefan Monnier at 2017-02-28T01:34:25-05:00 * src/lparse.ml (sform_case): New function
(register_special_forms): Register it.
* src/pexp.ml (pexp): Remove Pcase.
- - - - - 69727028 by Stefan Monnier at 2017-02-28T01:45:03-05:00 * src/lparse.ml (sform_letin): New function
(register_special_forms): Register it.
* src/pexp.ml (pexp): Remove Plet.
- - - - - 79cd9b86 by Stefan Monnier at 2017-02-28T02:08:42-05:00 * src/pexp.ml (pexp): Remove type
(pexp_location, pexp_name, pexp_parse, pexp_unparse, pexp_string) (pexp_print): Remove functions.
* src/lparse.ml (pexp_fatal, pexp_error): Remove functions.
- - - - - b10e7943 by Stefan Monnier at 2017-03-08T23:43:02-05:00 Improve type inference and add `.` macro.
For tuples and `.` macro to work, type inference needed to be improved. This improvement is to annotate metavars so they can't accidentally refer to local vars. IOW rather than "grafted", they're now "logical". This also refined slightly the inversion of substitutions, tho I'm not sure it makes an actual difference in the end.
* btl/pervasive.typer (BoolMod): Prototype of a Bool module. (Pair): New type. (__.__): New macro.
* emacs/typer-mode.el (typer-smie-rules): Add dangling `in` rule, as used in OCaml. Don't move up to the parent when indenting a `case` or `lambda` with a `case`'s branch.
* src/debruijn.ml (scope_level, lctx_length): New types. (elab_context): Add scope data. (make_elab_context): Rename to empty_elab_context. (ectx_new_scope, ectx_get_scope): New functions.
* src/debug_util.ml (main.ctx_to_cctx): Remove, use ectx_to_lctx instead.
* src/inverse_subst.ml (dummy_var): Remove. (substIR): Add destination count. (transfo.transfo): Refine the transformation so it is reversible. (inverse): Check success.
* src/lexp.ml (lexp_name): Move so we can use lexp_string for "trivial" cases. (subst_string): Use it to avoid pathological cases.
* src/lparse.ml (_global_lexp_ctx): Remove. (check): Shift metavars so they can't refer to vars from within the scope. (infer_call.handle_fun_args): Unify two branches. (lexp_decls_1, sform_letin): Introduce new scope for metavars.
* src/pexp.ml (pexp_p_actual_arg): Remove, unused. (pexp_p_decls): Use sexp_u_list.
* tests/eval_test.ml: Add test of the `.` notation.
- - - - - b2c05da9 by Stefan Monnier at 2017-03-10T21:33:38-05:00 * btl/pervasive.typer: Redefine lambda as a macro
* btl/pervasive.typer (List_foldr, List_find): New functions. (Sexp_error): Move. (Sexp_to_list, multiarg_lambda): New functions. (lambda_->_, lambda_=>_, lambda_≡>_): Redefine to add multiarg support via macros. (List_head, List_map, List_foldl): * btl/builtins.typer (Eq_comm, Macro_expand): Don't use multi-arg lambdas (yet).
- - - - - 0851032e by Stefan Monnier at 2017-03-16T11:34:54-04:00 * doc/primer.md: First cut at some user doc
- - - - - ed90728e by Christopher League at 2017-06-19T09:44:09-04:00 src/lparse: allow btl_folder to be read from environment
We can now use the environment variable `TYPER_BUILTINS` to specify the folder in which to find `builtins.typer` and `pervasive.typer`. Having this setting as a ref cell wasn't really helping, because it's used at the top level to bind `default_ectx`; once you hit `parse_args()` in `main`, it's too late to change it. So specifying as a command-line argument will require more changes.
- - - - - 07290652 by Stefan Monnier at 2017-06-29T17:49:56-04:00 * src/eval.ml (_eval): Add missing case for float constants.
- - - - - 900c37da by Stefan Monnier at 2017-06-29T17:51:32-04:00 Rename Lparse to Elab
- - - - - e060bdba by Stefan Monnier at 2017-07-01T00:18:01-04:00 Use sexps rather than pdecls
* src/lexp.ml (lexp_unparse.sdecls): Skip pexp_u_decls.
* src/elab.ml (instantiate_implicit): Use Eval.varname. (lexp_decls_macro): Don't return a new context any more. Return a sexp rather than a list of pdecls. (lexp_check_decls): Take a list of sexps rather than a list of pdecls. Simplify the macro call case since it can't return a new ctx any more.. (lexp_p_decls): Take a list of sexps rather than a list of pdecls. (sform_letin, default_ectx.read_file, _lexp_decl_str): Pass the sexps directly to lexp_p_decls.
* src/debug_util.ml (format_source): Pass the sexps directly to lexp_p_decls. (mdecl, lexp_detect_recursive): Remove rather than fix. (main): Remove "pexp" debugging because there's no pexp any more. Remove "merge-debug" debugging because it's broken and it's not clear how to fix it. Pass the sexps directly to lexp_p_decls.
* src/debug.ml (debug_pexp_decls): Remove; there's no pexp to debug any more. (debug_pexp_print_all): Remove unused.
* src/REPL.ml (ipexp_parse): Use sexp rather then pdecl. (_raw_eval): Pass the sexps directly to lexp_p_decls.
* src/pexp.ml (pdecl, pexp_p_decls, pexp_u_decl, pexp_u_decls) (pexp_decls_all, _pexp_decl_str, pexp_decl_str): Remove.
- - - - - 48b06933 by Stefan Monnier at 2017-07-07T15:49:10-04:00 * src/elab.ml (sform_lambda): Only handle a single arg
- - - - - 630b1bf0 by Stefan Monnier at 2017-07-07T15:54:37-04:00 * src/elab.el (sform_lambda): Improve error message
- - - - - 257dc966 by Stefan Monnier at 2017-07-07T16:04:55-04:00 * src/elab.el (sform_lambda): CPS refactor the end
- - - - - a2bd9afc by Stefan Monnier at 2017-07-07T16:22:32-04:00 * src/elab.ml (sform_lambda): Auto-add implicit lambda wrappers
(var_of_ovar): New function.
- - - - - fc6835a1 by Stefan Monnier at 2017-07-07T16:30:42-04:00 * btl/pervasive.typer: Let lambda_->_ infer the needed lambda_≡>_!
* btl/builtins.typer (Eq_comm): Same here.
- - - - - 09e86649 by Stefan Monnier at 2017-07-07T22:38:37-04:00 * src/elab.ml (lexp_check_decls): Drop unused `ltype` from `defs`
(lexp_decls_1): Drop corresponding info from pending_defs and pending_decls.
- - - - - 17f4f72a by Stefan Monnier at 2017-07-07T22:39:25-04:00 * btl/pervasive.typer: Move some defs to benefit from multiarg λ
- - - - - 31ee7094 by Stefan Monnier at 2017-07-12T00:07:13-04:00 * src/elab.ml (lexp_decls_1): Accept multiple decls for the same var
- - - - - 49ca7fdb by Stefan Monnier at 2017-07-18T18:09:10-04:00 Try and document the universe hierarchy
- - - - - ef053aac by Stefan Monnier at 2017-07-19T15:36:46-04:00 Force TypeLevel parameters to come first
- - - - - aaa414b2 by Stefan Monnier at 2017-07-27T10:29:18-04:00 Don't pass meta_ctx as arg any more
Instead, assign to global_substitution directly from unification.ml.
- - - - - fd033066 by Stefan Monnier at 2017-07-27T14:26:38-04:00 Don't pass meta_ctx as arg any more
Push the rest of last change, missed in last commit!
- - - - - 7b789287 by Stefan Monnier at 2017-07-27T14:43:23-04:00 Merge VMap and IntMap into IMap
- - - - - 5f814ec5 by Stefan Monnier at 2017-07-27T14:47:31-04:00 * opslexp.ml (level_canon): CSE
- - - - - 632d0b65 by Stefan Monnier at 2017-07-27T14:57:23-04:00 Provide scope_level to create_metavar
* src/debruijn.ml (get_size): Check that the two lengths are in sync. (ectx_to_scope_level, ectx_local_scope_size): New functions.
* src/elab.ml (newMetavar, newMetalevel, newMetatype): Take current scope_level as argument. (check): Use ectx_local_scope_size.
* src/lexp.ml (scope_level): Move from deruijn.ml. (dummy_scope_level): New var.
* src/unification.ml (create_metavar): Take current scope_level as argument.
- - - - - 73e53794 by Stefan Monnier at 2017-07-27T15:09:15-04:00 (metavar_info): Keep track of scope_level
* src/lexp.ml (metavar_info): Keep track of scope_level. (empty_meta_subst, empty_constraint): Remove. (metavar_lookup): Lookups should never fail now.
* src/unification.ml (create_metavar): Record the scope_level.
- - - - - c9eae130 by Stefan Monnier at 2017-07-29T22:43:16-04:00 * src/lexp.ml: Move the type info of metavars from lexp to metavar_info
(lexp): Don't carry the type of metavars any more. (scope_length): New type. (metavar_info): Rename MLevel to MVar and add type and ctx information.
- - - - - 27dd27dc by Stefan Monnier at 2017-08-03T14:25:36-04:00 * src/elab.ml: Make symbols into shorthands for `typer-identifier SYM`
(newMetalevel, newMetatype): Take a lexp_context i.s.o elab_context. (infer_varref): New function, extracted from `infer`. (infer): Make symbols into shorthands for `typer-identifier SYM` and blocks into shorthands for `typer-block BLOCK`. (check): Same rewrite for symbols. (sform_identifier): New functions, using code extracted from `infer` and `check`. (register_special_forms): Use it to implement `typer-identifier`.
- - - - - 5c157c20 by Stefan Monnier at 2017-08-03T15:36:36-04:00 * src/elab.ml: Make `elaborate` the core function
(elaborate): Rewrite, using code from `infer` and `check`. (infer): Rewrite, delegating to `elaborate`. (check): Rewrite, delegating to `elaborate`. (elab_varref): Rename from `infer_varref` and adjust return type. (elab_special_form): Rename from `parse_special_form`; adjust return type.. (elab_macro_call): Rename from `handle_macro_call`; adjust return type. (elab_call): Rename from `infer_call`; adjust return type. (sform_lambda): Adjust now that `elaborate` can return Lazy.
- - - - - f36cbd42 by Stefan Monnier at 2017-08-03T15:49:39-04:00 * src/elab.ml (sform_immediate): New special form
(register_special_forms): Register it. (elaborate): Use it for immediates.
- - - - - 2759acf9 by Stefan Monnier at 2017-08-03T16:45:57-04:00 * src/elab.ml (elaborate): Explain lack of typer-funcall
- - - - - b41d99a9 by Stefan Monnier at 2017-08-06T09:20:07-04:00 * src/opslexp.ml (check'): Fix handling of erasable datatype args.
- - - - - e5ac4157 by Stefan Monnier at 2017-08-22T13:10:07-04:00 Add `define-operator`
* src/elab.ml (sdform_define_operator): New function. (lexp_decls_macro): Adjust to extra value in context. (lexp_decls_1): Add case for `define-operator`. (elaborate): Treat blocks like immediates. (sform_immediate): Add case for blocks. * src/debruijn.ml (elab_context): Add grammar into the context. * btl/pervasive.typer (List_nth): New function. (quote1): Fix definition. (if_then_else_): Define as a macro. * src/grammar.ml (default_grammar): Move if/then/else... to pervasive.typer. * src/sexp.ml (token): New type alias.
* tests/sexp_test.ml: Remove if/then/else test. * tests/eval_test.ml ("Block", "define-operator"): New tests.
- - - - - 5ae615da by Stefan Monnier at 2017-09-06T07:58:55-04:00 -
- - - - - 1def0013 by Stefan Monnier at 2017-09-19T12:53:25-04:00 Use strings to specify operators
- - - - - 756bdbdf by Stefan Monnier at 2017-09-19T13:26:13-04:00 * emacs/typer-mode.el: Render comments as markdown
(typer--markdown-verbatim-block-re, typer--markdown-verbatim-face): New consts. (typer--markdown-p): New function. (typer-markdown-blockquote): New face. (typer-markdown-keywords): New var. (typer-font-lock-keywords): Use it. (typer-mode): Setup use of `invisible' property.
* btl/pervasive.typer: Make use of new comment style.
* src/subst.ml: Rework top-level comment.
- - - - - 91395fc2 by Stefan Monnier at 2017-09-19T16:07:58-04:00 Make define-operator's effect "immediately" visible
* src/debruijn.ml (ectx_get_grammar): New function.
* src/elab.ml (sform_immediate, default_ectx.read_file, lexp_expr_str) (lexp_decl_str)): Use it. (lexp_p_decls): Make new scope for body of `let`.
* tests/eval_test.ml (define-operator): No need for workaround any more.
* src/lexer.ml (unescape.split): Use string_sub.
* src/lexp.ml (_lexp_str): Avoid corner case bug. (get_binary_op_name): Catch corner case bug.
* src/opslexp.ml (clean_map): Prefer `map` when the `i` is not used.
* src/prelexer.ml (prelex_string.getline): Use string_sub.
- - - - - 494d60da by Stefan Monnier at 2017-09-19T16:30:58-04:00 Auto-generalize variable's type declarations
* btl/pervasive.typer: Simplify declarations, relying on generalization.
* src/debruijn.ml (scope): Remove. (meta_scope): New type alias. (elab_context): Use it to add a map of known metavar names. (empty_elab_context, ectx_new_scope): Handle the new metavar map. (get_size): Add sanity check.
* src/elab.ml (meta_to_var, infer_and_generalize_type): New functions. (lexp_decls_1): Use them to generalize var declarations. (sform_identifier): Use new metavar map to handle names metavars.
* src/inverse_subst.ml (invertible, lookup_inv_subst) (shift_inv_subst, compose_inv_subst, apply_inv_subst): New functions.
* src/lexp.ml (meta_id): New type alias. (lexp): Use it.
* src/opslexp.ml (mv_set): Keep track of types, names, and (meta)scope. (mv_set_union): Adjust accordingly.
* src/unification.ml (_unify_metavar): Use apply_inv_subst!
- - - - - ee53e868 by Stefan Monnier at 2017-09-24T22:21:00-04:00 Generalize non-recursive let-definitions
* btl/pervasive.typer (List_head, List_tail, Sexp_to_list.singleton): Let Typer generalize the definition's type.
* src/elab.ml (newMetalevel): Add a `loc` argument. (generalize): New function, extracted from infer_and_generalize_type. (track_fv): Adjust to new output of `OL.fv`. (infer_and_generalize_type): Use `generalize`. (infer_and_generalize_def): New function. (lexp_decls_1): Use it for non-recursive definitions.
* src/eval.ml (closed_p): Adjust to new output of `OL.fv`.
* src/opslexp.ml (mv_set): Add info to keep track of erasability. (mv_set_erase, fv_erase): New functions. (fv): Use them.
* src/unification.ml (_unify_metavar.unif): Return None in case of failure of inversion.
- - - - - 9ae0cbe3 by Stefan Monnier at 2017-09-25T11:30:10-04:00 Add preliminary support for big-ints
* GNUmakefile (OBFLAGS): Add `nums`. * src/debruijn.ml (type_integer): New type. * src/builtin.ml (register_builtin_csts): Register it. * src/env.ml (value_type): Add big-int constructor. * src/eval.ml (add_binary_biop, add_binary_bool_biop): New functions. Use them to setup new primitives. * btl/builtins.typer (Integer_*): Give them types.
- - - - - befa5609 by Stefan Monnier at 2017-09-25T13:46:34-04:00 * src/util.ml (msg_message): Use GNU standard format.
- - - - - 098ca889 by Stefan Monnier at 2017-09-25T22:15:31-04:00 Pretend we use bigints for Sexp integers
* btl/builtins.typer: Slight reorganisation. (Float->string): Rename from Float_to_string. (Int->Integer): Give it a type. (Sexp_integer): Change its type to be `Integer`. (Sexp_dispatch): Make matching change.
* src/eval.ml: Add new "Int->Integer" primitive. (make_integer): Make it take a bigint. (sexp_dispatch): Make it use a bigint for the integer case.
- - - - - 17853dd7 by Stefan Monnier at 2017-09-26T09:08:22-04:00 Finally implement the occurs check (and scope_level propagation)
* src/lexp.ml (ctx_length): Rename from scope_length.
* src/unification.ml (occurs_in): New function. (_unify_metavar.unif): Use it to avoid circular types and inconsistent generalization!
- - - - - 06c37fc5 by Stefan Monnier at 2017-09-29T00:53:28-04:00 Also apply generalization to inductive type constructors
* src/elab.ml (generalize): Change calling convention. (infer_and_generalize_type, infer_and_generalize_def): Adjust accordingly.. (lexp_parse_inductive.make_args): Generalize constructors. (var_of_ovar): Move to lexp.ml.
* src/opslexp.ml (check', get_type): Fix scoping of `level` in Inductive.
* btl/builtins.typer (Eq_comm): Take advantage of improvements in gneralization and unification.
* btl/pervasive.typer (BoolMod): Avoid `typecons`'s generalizing. (LList): New type, to test typecons's generalization.
* src/lexp.ml (var_of_ovar): Move from elab.ml. (lexp_unparse): Simplify.
* src/pexp.ml (pexp_u_ind_arg): Remove.
- - - - - 1e29f31a by Stefan Monnier at 2017-12-01T12:47:12-05:00 Provide type of Built-in via context, it's more flexible
* src/elab.ml (sform_built_in): Change to take the type from `ot` rather than from an argument.
* btl/builtins.typer: Adjust and simplify accordingly.
* src/builtin.ml (predef_names): Rename from `predef_name`.
- - - - - 7562d475 by Stefan Monnier at 2017-12-04T22:59:32-05:00 Verify and try to arrange that TypeLevel args come first
* btl/builtins.typer (Eq_cast): Simplify the type annotation yet a bit more.
* src/elab.ml (move_typelevel_to_front): New function. (generalize): Use it.
* src/opslexp.ml (sort_compose): Make it do more work. Properly enforce that TypeLevel args need to come first. (check', get_type): Adjust and simplify accordingly.
- - - - - 3a47ced1 by Stefan Monnier at 2018-05-01T12:20:42-04:00 Adjust to newer OCaml version
- - - - - 4a267fe6 by Stefan Monnier at 2018-05-03T16:03:37-04:00 * src/opslexp.ml (mktup, ctx2tup): New functions
- - - - - 2432cce1 by Jonathan Graveline at 2018-05-07T22:21:30+00:00 New sform_load. Work in progress. - - - - - 4a0ed5b5 by Jonathan Graveline at 2018-05-07T22:37:20+00:00 -lib nums to -pkg num - - - - - 905fc6f0 by Jonathan Graveline at 2018-05-10T01:08:36+00:00 Modification and use of susp within sform_load - - - - - 5aa903a9 by Jonathan Graveline at 2018-05-10T01:12:36+00:00 Modification of mktup and new function used in mktup - - - - - fc0bf4fa by Jonathan Graveline at 2018-05-10T15:15:35+00:00 Removed 'reset_intra_ref' - - - - - 34d24f66 by Jonathan Graveline at 2018-05-10T15:20:01+00:00 Correction in 'sform_load' and removed unused '_sform_default_rctx' - - - - - 83f93ecc by Jonathan Graveline at 2018-05-14T22:13:28+00:00 First draft - - - - - f0d1072f by Jonathan Graveline at 2018-05-14T22:15:06+00:00 First draft - - - - - a7dfcc1b by Jonathan Graveline at 2018-05-14T22:17:48+00:00 Added some built-in function for Int, Float, String - - - - - 3b80038f by Jonathan Graveline at 2018-05-14T22:19:39+00:00 Added some function for Int, Float, String - - - - - 00e86f25 by Jonathan Graveline at 2018-05-17T00:31:38+00:00 Use of predefined function `shift` - - - - - 3d4d9623 by Jonathan Graveline at 2018-05-17T00:33:20+00:00 Unfinished work on ctx2tup and mktup - - - - - 3fcfd932 by Stefan Monnier at 2018-05-17T13:37:14-04:00 Rewrite ctx2tup
* src/debruijn.ml (lct_view): Only allow LetDef in CVfix. (lctx_view): Adjust accordingly. * src/eval.ml (print_eval_result.from_lctx.from_lctx'): * src/opslexp.ml (lctx_to_subst.s2): Adjust accordingly. (mktup): Remove. (ctx2tup): Rewrite to build a let-nest with a (simpler) tuple inside.
- - - - - d84820f3 by Jonathan Graveline at 2018-05-17T22:07:55+00:00
From master
- - - - - bd6a3933 by Jonathan Graveline at 2018-05-17T22:09:07+00:00 Replace elab.ml - - - - - cdc94f8b by Jonathan Graveline at 2018-05-17T22:10:37+00:00 Change from master - - - - - 3da1ce59 by Jonathan Graveline at 2018-05-17T22:15:49+00:00 push_susp reverse let definition (not sure if it was an error) - - - - - bfa8bdcf by Jonathan Graveline at 2018-05-17T22:16:53+00:00 Change from master - - - - - 69659f54 by Jonathan Graveline at 2018-05-17T22:19:36+00:00 ctx2tup from master and different shift for tuple values - - - - - d6005a0c by Stefan Monnier at 2018-05-18T13:44:46-04:00 * src/lexp.ml (push_susp): Fix list inversion
Reported by Jonathan Graveline.
- - - - - 0c789e5d by Stefan Monnier at 2018-05-18T14:31:03-04:00 Move db_offset from env_elem to LetDef
* src/debruijn.ml (env_elem): Remove db_offset. * src/lexp.ml (varbind): Add db_offset to LetDef.
- - - - - a7ed6fa2 by Stefan Monnier at 2018-05-18T15:43:20-04:00 Merge branch 'trunk' into graveline
Also adds bool.typer and empty.typer for testing purposes, mostly.
- - - - - aaa4c5dc by Stefan Monnier at 2018-05-18T17:10:47-04:00 Add missing parts of last commit
- - - - - 891026a4 by Jonathan Graveline at 2018-05-25T03:30:19+00:00 Corrected String.sub String.concat - - - - - ae09719f by Jonathan Graveline at 2018-05-25T03:32:17+00:00 Better name, more function - - - - - 26df3634 by Jonathan Graveline at 2018-05-25T03:33:03+00:00 Better name - - - - - 7e8cd430 by Jonathan Graveline at 2018-05-25T03:34:45+00:00 do macro, first draft - - - - - 00a41105 by Jonathan Graveline at 2018-05-26T15:17:41+00:00 Syntax now using ";" and better use of IO_bind - - - - - eaca195c by Jonathan Graveline at 2018-05-26T15:23:04+00:00 Sexp_print for debugging - - - - - 588c02a6 by Jonathan Graveline at 2018-05-26T15:23:50+00:00 Sexp_print for debugging - - - - - df88126a by Jonathan Graveline at 2018-05-26T21:05:59+00:00 Renamed Sexp_print to Sexp_debug_print - - - - - 34da1bba by Jonathan Graveline at 2018-05-26T21:08:02+00:00 Renamed Sexp_print to Sexp_debug_print - - - - - 0259aaff by Jonathan Graveline at 2018-05-26T21:10:19+00:00 cleanup - - - - - 6045d6aa by Jonathan Graveline at 2018-05-30T20:22:24+00:00 Added make_block and Sexp_dispatch for Block - - - - - c096b10e by Jonathan Graveline at 2018-05-30T20:24:01+00:00 New Sexp_block - - - - - 338fd242 by Jonathan Graveline at 2018-05-30T20:25:26+00:00 New Sexp_block - - - - - 66f64c95 by Jonathan Graveline at 2018-05-30T20:27:21+00:00 action now use block - - - - - fe78c2da by Jonathan Graveline at 2018-05-31T18:55:38+00:00 Change to sexp_dispatch and added parse_default - - - - - a8779758 by Jonathan Graveline at 2018-05-31T18:56:37+00:00 Added Parser_default - - - - - bd3aa605 by Jonathan Graveline at 2018-05-31T18:57:59+00:00 Added Parser_default - - - - - 7884d73f by Jonathan Graveline at 2018-06-13T19:49:52+00:00 Renamed Parse_default to Parser_default, Corrected String.sub argument count - - - - - b46c9421 by Jonathan Graveline at 2018-06-13T19:55:28+00:00 Upload case.typer - - - - - 17fce738 by Jonathan Graveline at 2018-06-13T20:02:46+00:00 Added Int->String - - - - - d3100d5e by Jonathan Graveline at 2018-06-14T02:25:03+00:00 Added Ref as a built in type. - - - - - 1c406196 by Jonathan Graveline at 2018-06-14T02:26:12+00:00 Added Vref as a value_type - - - - - 6fbec92e by Jonathan Graveline at 2018-06-14T02:27:39+00:00 Added built in function Ref_make, Ref_read, Ref_write - - - - - ee004b1c by Jonathan Graveline at 2018-06-14T02:28:53+00:00 Added Ref_make, Ref_read, Ref_write - - - - - 2669433a by Jonathan Graveline at 2018-06-14T03:23:09+00:00 Ref_write affect when command is run - - - - - 56e7649d by Jonathan Graveline at 2018-06-15T18:47:16-04:00 New built-in gensym, changed macro signature to return IO Sexp
- - - - - 7896e300 by Stefan Monnier at 2018-06-20T21:28:09-04:00 Make all variable "names" optional
* src/util.ml (vname): Make the string optional. Change all `vname option` to `vname`.
- - - - - 203222b1 by Stefan Monnier at 2018-06-21T11:06:32-04:00 Merge branch 'trunk' into graveline
- - - - - abda0e39 by Jonathan Graveline at 2018-06-21T12:28:58-04:00 macro do in pervasive; test for macro do; some change on macro case
- - - - - eb8acb50 by Jonathan Graveline at 2018-06-21T12:30:52-04:00 Merge branch 'graveline' of https://gitlab.com/monnier/typer into graveline
- - - - - cec64f4a by Jonathan Graveline at 2018-06-21T12:57:44-04:00 After last merge symbol "_" in macro do need to be declared
- - - - - a8a77d78 by Jonathan Graveline at 2018-06-22T16:45:23-04:00 New type Elab_Context and functions Elab_getenv, Elab_isbound, Elab_isconstructor
- - - - - 46381fd8 by Jonathan Graveline at 2018-06-25T14:11:36-04:00 samples/list_n.typer, there must be some mistakes
- - - - - 246ba428 by Jonathan Graveline at 2018-06-25T17:22:00-04:00 macro "case" now use "do" and "Elab_isconstructor"; added tests/case_test.ml
- - - - - 9e9a8e89 by Jonathan Graveline at 2018-06-27T13:57:09-04:00 Correction of macro "do", dflt-sym need a symbol and not just "_"
- - - - - 4c682c42 by Jonathan Graveline at 2018-06-28T17:57:57-04:00 New type and value for Array with some functions
- - - - - af4ba9f6 by Jonathan Graveline at 2018-06-29T16:41:33-04:00 Correction of Array functions and simplification
- - - - - 9156b075 by Jonathan Graveline at 2018-07-02T17:08:22-04:00 New data structure "Table" (some kind of tree) (work in progress)
- - - - - 124601a5 by Jonathan Graveline at 2018-07-03T18:19:55-04:00 Corrected indentation in case.typer; table.typer rewriten with unit tests/table_test.ml
- - - - - e98cf539 by Jonathan Graveline at 2018-07-05T15:03:15-04:00 Using rlwrap to add auto-completion and history
- - - - - a0f050f7 by Jonathan Graveline at 2018-07-05T15:40:51-04:00 Stop compiler on first error
- - - - - ece77ad2 by Jonathan Graveline at 2018-07-05T15:43:43-04:00 Don't try to print value if there's none
- - - - - 72bfc552 by Jonathan Graveline at 2018-07-05T15:49:54-04:00 Added .directory to .gitignore
- - - - - f3667866 by Jonathan Graveline at 2018-07-05T23:03:52-04:00 Print similar name with error message when a variable isn't found
- - - - - 27f86f61 by nbos at 2018-07-07T00:41:05-04:00 Added draft file presenting the theory behind Typer plus the file's dependencies
- - - - - 1e7b80b3 by nbos at 2018-07-09T16:19:32-04:00 Prettified boxes; fixed PTS definition; added impredicative R; gave explanations on E- vs R- rules
- - - - - 0881ba77 by nbos at 2018-07-09T17:45:50-04:00 New macro
- - - - - a05b2179 by nbos at 2018-07-09T17:46:50-04:00 Started CCw to Typer translation
- - - - - 9887dcff by nbos at 2018-07-10T14:53:09-04:00 Corrected typos; moved some rules and renamed rule groups; fixed boxes around figures
- - - - - a89aa4f4 by Jonathan Graveline at 2018-07-11T15:39:36-04:00 Compile samples/* only once in some unit tests; New balanced bst (bbst.typer)
- - - - - 81821861 by Jonathan Graveline at 2018-07-11T15:57:31-04:00 Corrected macro type in default attribute and eval_test.ml
- - - - - 2110c130 by nbos at 2018-07-11T21:09:45-04:00 Changed some notation
- - - - - 488c0fde by nbos at 2018-07-11T23:01:36-04:00 Removed pmb style
- - - - - c39bd687 by Stefan Monnier at 2018-07-12T12:17:12-04:00 * src/sexp.ml (sexp_parse_all): Fail more gracefully when encountering a stray closing token.
- - - - - 9cbcda53 by nbos at 2018-07-17T11:56:58-04:00 Modified TypeLevel definition and notation; described CCw; finished skeleton of proof
- - - - - 6125b349 by nbos at 2018-07-17T13:42:40-04:00 Separated Case 1 of proof into two; introducing Erasable constructor
- - - - - abf28d5c by Stefan Monnier at 2018-07-18T13:27:27-04:00 Be more careful about which grammar to use while parsing
* src/REPL.ml (_ieval, _raw_eval): Use grammar from ctx. Rename arg to `ectx`. * src/debug_util.ml (format_source, main): Use grammar from pervasive.
- - - - - ec47c030 by Jonathan Graveline at 2018-07-18T16:13:11-04:00 Run macros in the IO monad
* btl/builtins.typer (Macro, Macro_expand): Return type is now `IO Sexp`.
* btl/pervasive.typer (multiarg_lambda, quote, __.__): Adjust accordingly..
* src/debruijn.ml (senv_lookup): No need to be recursive.
* src/elab.ml (get_implicit_arg, elab_macro_call, lexp_decls_macro): Macros are now run in the IO monad. (sexp_decls_macro_print): Comment out.
* src/opslexp.ml (ctx2tup.mk_lets_and_tup): Fix debindex.
* tests/eval_test.ml (test_eval_eqv_named): Don't burp on empty lists.. ("Implicit Arguments"): Adjust to new type. ("Generic-typed case"): Use our own `Pair` type.
* tests/macro_test.ml ("macros base", "macros decls"): Adjust to new type.
- - - - - c7d2bbfe by Stefan Monnier at 2018-07-18T17:01:03-04:00 Merge branch 'trunk' into graveline
- - - - - 33a23595 by Stefan Monnier at 2018-07-21T17:29:49-04:00 Make isconstructor pure and boolean; and ignore names in lctx
* btl/builtins.typer (Elab_isbound, Elab_isconstructor): Make pure and Bool. * samples/case.typer (is_ctor): Adjust accordingly.
* src/debruijn.ml (lctx_olookup, lctx_olookup_type) (lctx_olookup_value): Delete.
* src/elab.ml (elab_p_id): Not recursive. (check_case): Use Eval.constructor_p.
* src/eval.ml (sexp_dispatch): Remove dead code. (is_bound): Use senv_lookup. (constructor_p): New function, extracted from Elab.check_case. (is_constructor): Use it.
* tests/elabctx_test.ml (v2o_bool): New function. ("Elab_isbound", "Elab_isconstructor"): Adjust to new types of isbound and isconstructor. Add test case for alias to a constructor.
- - - - - 2abe090c by Stefan Monnier at 2018-07-23T20:25:35-04:00 Move String.uppercase to a single place
Don't use String.uppercase_ascii yet, since it's not available in Debian stable's OCaml package. Also get rid of some leading underscores.
* src/util.ml (string_uppercase): New function. * tests/utest_lib.ml (must_run_section, must_run_title): * tests/utest_main.ml (must_run): Use it and simplify.
- - - - - c08685e0 by Stefan Monnier at 2018-07-23T20:57:53-04:00 Merge branch 'trunk' into graveline
- - - - - ff69f5cf by Jonathan Graveline at 2018-07-23T21:55:12-04:00 more List functions
- - - - - 61fc705d by Jonathan Graveline at 2018-07-23T22:18:36-04:00 progression on the `case` macro
- - - - - 93aa39b9 by Stefan Monnier at 2018-07-23T22:19:08-04:00 Fix exponential blowup witnessed when loading a module
* src/lexp.ml (hcs_table): New memoization table. (mkSusp_memo): New function.
- - - - - 9f8cd189 by Stefan Monnier at 2018-07-23T22:19:28-04:00 Merge branch 'trunk' into graveline
- - - - - e3e9599b by Jonathan Graveline at 2018-07-23T22:22:13-04:00 Merge branch 'graveline' of https://gitlab.com/monnier/typer into graveline
- - - - - 16b5fb2e by nbos at 2018-07-24T03:13:51-04:00 Changed notation for CCw; added abbrevs for keyworkds (sans serif)
- - - - - 5a751a66 by nbos at 2018-07-24T03:18:02-04:00 Finished translation from CCw; changed presentation of CCw to be based on CC rather than ECC
- - - - - 7d665323 by nbos at 2018-07-24T04:18:21-04:00 Contextualized notation for Typer's compound terms and CCw
- - - - - c8fad518 by Jonathan Graveline at 2018-07-24T20:08:43-04:00 update on macro `case`
- - - - - d21c5eb6 by Stefan Monnier at 2018-07-25T15:13:16-04:00 Allow `let` vars to be erasable in some circumstances
* src/opslexp.ml (nerased_let): New function. (check'): Use it. * tests/eval_test.ml ("Let-erased"): New test.
- - - - - 450e86fa by Jonathan Graveline at 2018-07-25T16:28:33-04:00 *samples/list.typer, more consistent function's type declaration
- - - - - 5d4e2008 by Jonathan Graveline at 2018-07-25T16:35:26-04:00 Stop compilation on error in `check` and elab functions Also store all errors and warnings for future use
- - - - - 2b2bac1b by Jonathan Graveline at 2018-07-25T16:40:47-04:00 Print related name only when the name has underscore
- - - - - 26e9e4c2 by Jonathan Graveline at 2018-07-25T17:25:59-04:00 Add an exception for sform_load's context when in pervasive.typer
- - - - - a188451f by Jonathan Graveline at 2018-07-25T22:52:06-04:00 Merge branch 'master' of https://gitlab.com/monnier/typer into graveline
- - - - - be29169e by Jonathan Graveline at 2018-07-26T00:45:56-04:00 Change lost somewhere in previous commit *samples/case2.typer *samples/do.typer *samples/list.typer
- - - - - b0b911ec by Jonathan Graveline at 2018-07-26T00:55:06-04:00 Many change to use `load` in pervasive.typer and move some definition Temporary workaround for tuple access in macro `.`
renamed: samples/case2.typer -> btl/case.typer renamed: samples/do.typer -> btl/do.typer renamed: samples/list.typer -> btl/list.typer modified: btl/pervasive.typer deleted: samples/case.typer modified: src/opslexp.ml modified: tests/array_test.ml modified: tests/case_test.ml
- - - - - 26b5c9c8 by nbos at 2018-07-26T22:27:37-04:00 Cleaned text; fixed translation to account for new rules of CCw
- - - - - 572470f8 by Jonathan Graveline at 2018-07-27T01:30:17-04:00 `plain-let` (not recursive nor sequential) without grammar yet
- - - - - 84261c57 by Jonathan Graveline at 2018-07-27T02:20:33-04:00 keep count of `insert`/`remove` for faster `length` calculation
- - - - - 4d149272 by Jonathan Graveline at 2018-07-27T02:22:26-04:00 use `if ... then ... else ...` syntax where appropriate
- - - - - 0ab2e43c by Jonathan Graveline at 2018-07-27T08:39:23-04:00 Minimal built-in functions for unit tests in Typer
- - - - - 25024193 by nbos at 2018-07-30T04:11:16-04:00 New commands; removed unecesary math layer in sans keywords
- - - - - 618d6ae9 by nbos at 2018-07-30T04:15:13-04:00 Restructured whole proof of extention of CCω
- - - - - b2fdff75 by nbos at 2018-07-30T05:59:21-04:00 Added room for special case E-Lam
- - - - - 14f1aafb by Jonathan Graveline at 2018-07-30T16:57:35-04:00 Correction of some unit test primitive (put action in `Vcommand` and set to correct type)
New primitive Integer->String (useful with Sexp_dispatch)
- - - - - e1917e8b by Jonathan Graveline at 2018-07-30T17:05:01-04:00 Don't print related name with the single character symbol "_"
Added boolean operation from samples/bool.typer to pervasive.typer
- - - - - 35f6bc54 by Jonathan Graveline at 2018-07-30T17:09:57-04:00 *polyfun.typer: Implicit `case` at function definition level (macro not working if at top-level, but working in `let`)
- - - - - a9f1a0dd by Jonathan Graveline at 2018-07-30T17:13:49-04:00 macro for tuple creation and access (more to come) (`_,_` not working yet, temporarily using `_:_`)
- - - - - da1e981a by nbos at 2018-07-31T08:36:38-04:00 Add a few theorem-style environments; clean some unused commands
- - - - - 42ee60bb by nbos at 2018-07-31T08:39:09-04:00 Begin Lemma 3.1; clean translation format; add theorem-style environments where appropriate
- - - - - 2eb3b210 by nbos at 2018-07-31T11:55:21-04:00 Introduce translation operator; reduce number of assumptions in sec.3 and prove new lemmas instead
- - - - - b27dd3ea by Jonathan Graveline at 2018-07-31T13:28:32-04:00 `plain-let` with grammar setup
- - - - - 5c4ba829 by Jonathan Graveline at 2018-07-31T18:47:13-04:00 Add function syntax support in `plain-let`
- - - - - 4191f41f by Jonathan Graveline at 2018-07-31T22:22:54-04:00 new built-in function `Parser_*` and use it in do.typer
- - - - - 38b621d2 by Jonathan Graveline at 2018-08-01T12:12:25-04:00 use `if...then...else...` syntax where appropriate
udict and odict (from table and bbst) for convenience
- - - - - 28006ea4 by Jonathan Graveline at 2018-08-01T13:33:28-04:00 define operator `<-`, use it in do.typer and tuple.typer
tuple now working with `,` (needed escape: `_,_`)
- - - - - b3519661 by Jonathan Graveline at 2018-08-02T15:38:52-04:00 macro `case` should now work on tuple
use `sexp_name` in `Sexp_debug_print`
change in `is_binary_op` (I think it was a bug)
tuple constructor now has a `gensym` name
- - - - - d63644ec by Jonathan Graveline at 2018-08-03T15:12:23-04:00 samples/tuple_test.typer: Test written in Typer for tuple
Changed warning, info and fatal output in unit test primitive
- - - - - ce6c1ca9 by nbos at 2018-08-03T15:45:52-04:00 Define translation operator; stage the proof to be bidirectional; replace correspondance between PTS's with lemmas of injective maps between sorts and axioms of CCw and Typer
- - - - - 69c04c10 by nbos at 2018-08-03T16:12:04-04:00 Prove lemma 3.3 + 3.4
- - - - - 1599bd1c by nbos at 2018-08-03T16:25:50-04:00 Prove lemma 3.5
- - - - - bedf45c5 by Jonathan Graveline at 2018-08-03T16:45:49-04:00 Correction in polyfun.typer; unit test in Typer for macro `_|_`
- - - - - afe315b8 by Jonathan Graveline at 2018-08-06T11:52:15-04:00 `Env.value_equal`: using structural equality when comparing constructor name
- - - - - ffe322a7 by Jonathan Graveline at 2018-08-06T12:26:56-04:00 Rewrote unit test for `Bbst` and `Table` in Typer code
- - - - - e9a91eba by Jonathan Graveline at 2018-08-06T19:14:53-04:00 An attempt to fix a problem with `load_`
- - - - - 54fcd9b8 by nbos at 2018-08-06T19:33:22-04:00 Add labels and refs to figures in text
- - - - - cd8d5f59 by nbos at 2018-08-07T05:09:37-04:00 Add labels and refs to equations; add (Prop, Prop, Prop) axiom to Rcc; define translation on applications; prove (most of) lemma 3.6
- - - - - f4c0cfb7 by Jonathan Graveline at 2018-08-07T12:42:57-04:00 `tunit` in eval.ml is now `unit` rather than `()`
- - - - - 3d4035ac by Jonathan Graveline at 2018-08-07T14:25:12-04:00 Correction of bounds check in `array_get`
samples/array_test.typer: Unit test for `Array` rewritten in Typer
- - - - - 7f3a4233 by nbos at 2018-08-08T03:49:41-04:00 Finish proof of lemma 3.6; make it a case analysis on [M]* rather than [M]; make M -> M* definition a figure
- - - - - 58024bcd by nbos at 2018-08-08T06:40:51-04:00 Enhance layout of translation section; define soundness/completeness of translation; label lemmas; clean A-equiv lemma; add R-equiv lemma; complete completeness (=>) proof
- - - - - ab7b5700 by nbos at 2018-08-09T09:54:04-04:00 Clarified lem:S-equiv; boxed definition of translation in fig:[]
- - - - - af784c9b by nbos at 2018-08-09T10:45:56-04:00 Fix lemma lem:A-equiv
- - - - - d5a33c33 by nbos at 2018-08-09T11:27:31-04:00 Add feedback FIXME's
- - - - - f9d7cefc by Jonathan Graveline at 2018-08-09T13:30:04-04:00 New primitive for inductive type info
Temporary fix of macro `case` to pass unit tests
Commented incorrect `Metavar` case in `conv_p`
- - - - - 769d8856 by nbos at 2018-08-09T22:28:06-04:00 Fix and streamline lem:S-equiv and lem:A-equiv; split first part of lem:R-equiv into lem:Re-equiv
- - - - - e9edd7ec by nbos at 2018-08-09T23:40:34-04:00 Put theorems and lemmas on the same counter
- - - - - ab2c6d9b by Jonathan Graveline at 2018-08-10T12:59:38-04:00 New macro `Test_file` not working on multiple call
Unit test rewritten in Typer for `case`, `do`, `Elab_Context`
Correction of primitive `Elab.is-arg-erasable`
- - - - - a8b733a6 by Jonathan Graveline at 2018-08-13T13:05:25-04:00 Macro `Test_file` now return a command: `exec-test` from loaded file
File samples/batch_test.typer now working
Most unit test in Typer adapted for `Test_file` and batch_test.typer
- - - - - c11bb8a4 by Jonathan Graveline at 2018-08-13T16:52:32-04:00 New complementary primitive: `Elab_arg-pos`
Improved macro `case` on explicit field pattern
- - - - - 9b526a75 by nbos at 2018-08-14T00:21:58-04:00 Reduce margin; avoid undefined use of ∪ with CCω sorts; make eq:corresctness-translation a theorem; finish proof of lem:R-equiv; start proof of lem:Re-equiv
- - - - - 37d2e51b by nbos at 2018-08-14T02:02:11-04:00 Fix references to lemmas lem:S- lem:A- lem:R- and lem:Re-equiv in proof
- - - - - 998d77aa by nbos at 2018-08-14T02:22:00-04:00 Complete proof of lem:Re-equiv
- - - - - c42b26d7 by nbos at 2018-08-14T08:19:21-04:00 Move lem:E-Lam-FV to before completeness proof; generalize lem:E-Lam-FV out of only translations
- - - - - e7c3aa6b by nbos at 2018-08-14T11:28:52-04:00 Remove custom font
- - - - - 74dcbd9d by nbos at 2018-08-14T11:40:30-04:00 Add title and authors; setup cases for soundness of translation proof
- - - - - 1ee31754 by nbos at 2018-08-16T14:02:55-04:00 Populate soundness proof with typing rules; rephrase some sentences to be impersonal; add substitution in definition of translation
- - - - - 5bfe76e4 by nbos at 2018-08-17T17:55:44-04:00 Add 'pack' as an example
- - - - - cf4448de by Jonathan Graveline at 2018-08-20T17:58:13-04:00 Macro `Tuple` returning a type
Comment for `Test_file` in pervasive.typer
- - - - - 70fac346 by nbos at 2018-08-22T05:14:43-04:00 Fix part of lem:FV-E-Lam; expand on example Pack
- - - - - c52700fd by nbos at 2018-08-22T17:29:36-04:00 Finish fix lem:FV-E-Lam
- - - - - 57ed864b by nbos at 2018-08-22T18:36:04-04:00 Restructure sections and figures; correct some awkward phrasing
- - - - - 3981eea1 by Jonathan Graveline at 2018-08-22T19:29:34-04:00 New character '@' introducing docstring
New primitive `Elab.debug-doc` mostly for testing docstring
Replaced `load_` by `load`
- - - - - 451ead23 by Jonathan Graveline at 2018-08-23T16:56:11-04:00 Documentation, work in progress
Some more tests in samples/case_test.typer
- - - - - caa73195 by Jonathan Graveline at 2018-08-24T14:33:07-04:00 Revised comments, trying to be more clear
- - - - - cd2381bc by Jonathan Graveline at 2018-08-24T15:46:34-04:00 New unit test for `plain-let`
Revision of bbst.typer and table.typer
- - - - - 6ef13572 by Jonathan Graveline at 2018-08-27T15:01:33-04:00 More comments in samples/myers.typer
Basic unit tests on Myers list in samples/myers_test.typer
- - - - - 13cf5ad0 by Jonathan Graveline at 2018-08-29T16:49:39-04:00 Revised comments; commented more function in btl/builtins.typer
Rewrite tuple body; commented tuple unit tests (but they should work)
- - - - - 89aecbb1 by nbos at 2018-08-30T05:05:45-04:00 Rewrite a valid proof of lem:E-Lam-FV; start proof of soundness of translation; expand on guarded by destructors predicate D
- - - - - e25ebfb7 by nbos at 2018-08-30T15:00:52-04:00 Review of completeness of translation proof
- - - - - a1747386 by Jonathan Graveline at 2018-08-30T16:16:35-04:00 Removed "debug output" in `Ref_make` from src/eval.ml
samples/decltype.typer: another version of `decltype` implemented in Typer
samples/math.typer: a toy math library
- - - - - 9fd7015b by Jonathan Graveline at 2018-08-31T17:25:07-04:00 Revised comments and documentation from btl/ and samples/
- - - - - d374fc40 by nbos at 2018-09-01T05:22:40-04:00 Rephrase parts of completeness of translation proof; finish soundness of translation proof; finish example
- - - - - 576bfd64 by nbos at 2018-09-02T00:26:20-04:00 Add of sans-serif keyword command
- - - - - b15652de by nbos at 2018-09-02T00:29:15-04:00 Restructure some sentences; add recursive definition of free variables; define beta- and iota-reductions; add transitivity to congruence relation
- - - - - 0e695aca by Stefan Monnier at 2018-09-17T13:23:29-04:00 * src/elab.ml (sform_debruijn): New special form
(register_special_forms): Register it.
- - - - - 306196bf by Stefan Monnier at 2018-09-17T13:26:03-04:00 Merge remote-tracking branch 'remotes/gitlab/bosn' into trunk
- - - - - 90f98f10 by Stefan Monnier at 2018-09-17T15:29:27-04:00 * src/eval.ml: Add trivial comment
- - - - - 2269559a by Stefan Monnier at 2018-09-17T17:21:16-04:00 Merge remote-tracking branch 'remotes/gitlab/graveline' into trunk
- - - - - a7bdf1e6 by Stefan Monnier at 2018-09-18T19:04:14-04:00 Avoid the <foo>_opt functions not available in older OCaml
* src/util.ml (smap_find_opt): New function to replace SMap.find_opt.
* src/eval.ml (nth_ctor_arg.find_nth): Avoid List.nth_opt. (erasable_p2.is_erasable): Use List.exists.
- - - - - 32ef5ef1 by Stefan Monnier at 2018-09-20T22:10:39-04:00 Get rid of identifiers starting with underscore in *.ml
- - - - - 76a477f1 by Stefan Monnier at 2018-09-20T22:27:11-04:00 Get rid of identifiers starting with underscore in *.ml
- - - - - 2f9ed1b0 by Stefan Monnier at 2018-09-20T22:30:43-04:00 Rename Aexplicit to Anormal
- - - - - ae543b55 by Stefan Monnier at 2018-11-23T16:43:09-05:00 * samples/hurkens.typer: New file.
- - - - - 749381e0 by Stefan Monnier at 2018-11-23T17:51:34-05:00 * samples/hurkens.typer: Add a few comments.
- - - - - 5c39f5f8 by Stefan Monnier at 2018-12-04T19:32:16-05:00 Consolidate and rename Parser.* built-ins
* btl/builtins.typer (Parser_default, Parser_newest): Remove. (Reader_parse): Rename from Parser_custom.
* btl/do.typer (get-decl): Add `ctx` arg. Use Reader_parse. (do): Pass it Elab_getenv.
* src/eval.ml (parser_default, parser_newest): Remove. (reader_parse): Rename from parser_custom.
- - - - - 8061a7de by Stefan Monnier at 2019-02-16T10:15:19-05:00 * src/opslexp.ml (check'', get_type): Fix context confusion
When computing the level of an inductive type, we need to distinguish the current context of the current field and the external context in which the result is valid.
- - - - - c25f821e by Stefan Monnier at 2019-07-23T21:56:09-04:00 * src/subst.ml (subst): Fold a `Shift` into the `Identity`.
Generalize `Identity` with `Identity o` where the old `Identity` is now `Identity 0` and `Identity o` is like the old `Shift (Identity, o)`.
(mkShift): Use `Identity` when possible. (shift): Use `Identity`. (identity): Adjust to new `Identity`. (lookup, identity_p, compose): Generalize to the new `Identity o`. (substitute): Use `identity`.
* src/elab.ml (newMetavar): Use S.identity.
* src/inverse_subst.ml (is_identity): Take advantage of the new `Identity o`. (shift_inv_subst): Optimize the case when n is 0. (transfo, invertible, lookup_inv_subst, compose_inv_subst): Generalize to the new `Identity o`.
* src/lexp.ml (subst_string): Handle the new `Identity o`. (subst_eq): Generalize to the new `Identity o`.
* tests/inverse_test.ml (is_identity): Copy new def from inverse_subst.ml..
* tests/unify_test.ml (generate_testable): Use `identity`.
- - - - - 6c5475e1 by Stefan Monnier at 2019-07-24T00:40:25-04:00 * src/subst.ml (subst): Fold the remaining Shift into Cons.
Fold `Shift` into the `Cons`, and hence remove `Shift` since it's not needed as a separate constructor any more.
(sink, substitute): Use `cons` (lookup, mkShift, cons, compose): * src/lexp.ml (subst_string, subst_eq): * src/inverse_subst.ml (transfo, is_identity, invertible) (lookup_inv_subst, compose_inv_subst): Adjust accordingly.
* tests/inverse_test.ml (is_identity): Update from src/inverse_subst.ml.
* src/opslexp.ml (lexp_whnf): Use `S.cons`.
- - - - - d75ab820 by Stefan Monnier at 2019-07-26T23:38:33-04:00 Add comments from a Myers's subst experiment
* src/lexp.ml (lexp_unparse): Prefer S.cons to S.Cons.
* src/subst.ml (subst): Add Myers's optimization in a comment. It probably works, but it currently bumps into another performance problem. (lookup, compose): Add commented-out Myers's optimization.
* tests/inverse_test.ml (is_identity): Remove (lets the code use the version of Inverse_subst).
- - - - - ff16d3ba by Stefan Monnier at 2019-07-26T23:39:04-04:00 * samples/defmacro.typer (define-macro): New package and macro
- - - - - e3a0fe68 by Stefan Monnier at 2019-09-13T14:31:03-04:00 Avoid using Inverse_subst in core type checking
* src/lexp.ml (mkSLlub', mkSLsucc): New constructors with sanity checks. (sunshift): New function. * src/opslexp.ml (check'', get_type): Use it instead of Inverse_subst.
- - - - - cf67844d by Stefan Monnier at 2019-09-13T17:06:03-04:00 First tweak to try and handle parameterized inductives
* src/elab.ml (check_case.add_branch): Try and handle parameterized constructors. (elab_check_def): Slightly improve message.
* src/unification.ml (unify_inductive): New function. (unify'): Use it.
- - - - - 25bb77ab by Stefan Monnier at 2019-09-26T16:51:26-04:00 * lexp.ml (lexp): Typo
- - - - - 5c7f8365 by Stefan Monnier at 2019-09-26T16:52:00-04:00 Merge remote-tracking branch 'refs/remotes/gitlab/master' into trunk
- - - - - 9455fa18 by Jean-Alexandre Barszcz at 2019-10-03T21:46:06-04:00 Extract logging from util.ml
- - - - - c1458d9a by Jean-Alexandre Barszcz at 2019-10-03T21:46:06-04:00 Replace typer_unreachable exception with 'failwith'
- - - - - 82fa3593 by Jean-Alexandre Barszcz at 2019-10-03T21:46:06-04:00 Refactor logging
- - - - - 51251f1f by Jean-Alexandre Barszcz at 2019-10-03T21:46:06-04:00 Add optional color to logging
- - - - - 2a2afc56 by Jean-Alexandre Barszcz at 2019-10-10T02:52:31-04:00 Print errors/warnings all at once, after compilation stops
- - - - - 09952ed7 by Jean-Alexandre Barszcz at 2019-10-10T02:52:31-04:00 Print the log in default context
- - - - - c02e28bc by Jean-Alexandre Barszcz at 2019-10-10T02:52:31-04:00 Add an option to control the verbosity/logging level
- - - - - f41b8bb3 by Jean-Alexandre Barszcz at 2019-10-10T02:52:31-04:00 Always print the log after evaluation
If there are warnings (or other messages of lesser priority in the log), we want to print them. Similarly, errors for which we were able to recover might still exist in the log. Regardless of whether compilation has been stopped, we thus print the log.
- - - - - b948d4c9 by Jean-Alexandre Barszcz at 2019-10-10T02:52:31-04:00 Print test messages instead of logging them
- - - - - 71ec8850 by Stefan Monnier at 2019-10-22T16:41:34-04:00 * src/elab.ml (sform_lambda): Rename the type's var
This should fix some deBruijn errors for cases like:
x : (y : T1) -> T2 y; x z = e;
since the (dependent) type of `e` will use the name `z` rather than `y`. Apparently it doesn't fix all our deBruijn name check errors, tho :-(
* sample/hurkens.typer: Unrelated cosmetic changes.
- - - - - c3706c38 by Stefan Monnier at 2019-10-22T16:45:23-04:00 Merge branch 'master' of gitlab.com:monnier/typer into trunk
- - - - - 634f6df0 by Stefan Monnier at 2019-10-22T17:58:25-04:00 Allow "impredicative" universe polymorphism
* samples/hurkens.typer (𝓅): Make it universe-polymorphic.
* src/elab.ml (infer_level): New function. (sform_type): Use it.
* src/log.ml (log_fatal): Set print_at_log before calling log_msg so the message is printed before raising the exception, otherwise it's lost.
* src/opslexp.ml (deep_universe_poly): New const. (sort_compose): Add one more context for k2. Fix k2 scoping. Obey deep_universe_poly.
- - - - - 4bcb4b11 by Stefan Monnier at 2020-03-17T13:59:49-04:00 * src/env.ml (BI): Use `Z` rather than `Big_int`
* GNUmakefile (OBFLAGS): Use Zarith rather than Num
- - - - - 93c051db by Stefan Monnier at 2020-03-17T14:06:01-04:00 * samples/hott.typer: New file
- - - - - b4bacaf0 by Stefan Monnier at 2020-03-17T14:26:41-04:00 * src/opslexp.ml (impredicative_erase): Disable it
(impredicative_universe_poly): Rename from deep_universe_poly.
- - - - - 93cb1223 by Stefan Monnier at 2020-03-18T23:30:00-04:00 Fix up various issues with universe levels
* src/builtin.ml (type_eq): Use `mkVar`.
* src/elab.ml (elaborate): Use `mkVar`. (infer_level): Add suport for ∪ in type level expressions.
* src/lexp.ml (mkSLlub'): Add a crutch. (lexp_unparse, lexp_print): Clarify output of TypeLevel.
* src/opslexp.ml (level_canon, level_leq): Move earlier. (conv_p'): Use to fix handling of `SLlub`. (mkSLlub): Fix thinko. (check'', get_type): Use `mkVar`.
* src/unification.ml (unify): Improve unification of SLlub.
- - - - - c081c586 by Stefan Monnier at 2020-03-20T11:28:31-04:00 -
- - - - - 86d4a83d by Stefan Monnier at 2020-03-21T18:02:02-04:00 * unification.ml: Return just a list rather than an list option
Additionally, keep track of the ctx and annotate whether there's a possibility unification could succeed at some other time.
* src/lexp.ml (constraints): Move to unification.ml
* src/unification.ml (constraint_kind): New type. (constraints): Rewrite. (unify_and): Remove, use `@` instead.
- - - - - 402bdbe0 by Stefan Monnier at 2020-03-27T16:04:24-04:00 Infer type of `case` target from patterns
* src/elab.ml (check_case): Infer the type of the target from the patterns when applicable.
* src/opslexp.ml (check''): Be careful to always pass the inferred type and the expected type in the same order.
* src/unification.ml (create_metavar_1): New function extracted from create_metavar. (create_metavar): Use it. (common_subset, s_offset): New functions. (unify_metavar): Use them to properly handle the case of unifying a metavar with itself where the two substitutions are different.
* btl/builtins.typer (Eq_comm): Simplify type annotation a bit.
* btl/pervasive.typer (List_head1, List_head, List_tail, List_concat) (I, List_map-fst, List_map-snd): Remove unnecessary type annotation.
- - - - - 56ed1196 by Stefan Monnier at 2020-04-02T17:04:44-04:00 Misc tweaks; use a bit more universe polymorphism; improve some errors
* btl/builtins.typer: Make better use of generalization to avoid `≡`. (List): * btl/pervasive.typer (Option, Not): Make them universe-polymorphic.
* src/builtin.ml (register_builtin_csts): Add name `Type0`.
* src/debruijn.ml (type_level_sort): Rename from `sort_level`.
* src/elab.ml (check_inferred): Give more complete error info. (infer_level): Use `newMetalevel`.
* src/lexp.ml (lexp_head): New function. (mkSLlub', lexp_name): Use it. (lexp_unparse, lexp_print): Fix printout of `type_level_sort`.
* tests/eval_test.ml ("has-attribute", "Implicit Arguments"): Disable tests.
- - - - - f2b81386 by Stefan Monnier at 2020-04-02T19:31:41-04:00 * src/elab.ml (meta_to_var): Fix debruijn error.
* btl/pervasive.typer (Decidable): Make it universe-polymorphic. * src/builtin.ml (register_builtin_csts): Fix Type0 typo.
- - - - - 85d12bf5 by Stefan Monnier at 2020-04-07T22:21:39-04:00 * src/elab.ml (infer_and_generalize_type): Add more exceptions
Don't generalize over the level of the final return type if it doesn't appear elsewhere.
* btl/builtins.typer (Eq_cast): Give a name to the proof arg.
- - - - - 4993afa5 by Stefan Monnier at 2020-04-07T23:15:21-04:00 * src/lexp.ml (srename): New function
* src/unification.ml (unify): * src/opslexp.ml (conv_p'): * src/elab.ml (sform_lambda): Use it.
- - - - - 63f7644b by Stefan Monnier at 2020-04-07T23:21:05-04:00 * src/elab.ml (meta_to_var): Rework to be able to infer universe levels
(generalize): Adjust for new calling convention of `meta_to_var` and also for the fact that `meta_to_var` now takes care of the S.shift for us.
- - - - - 886a3589 by Stefan Monnier at 2020-04-08T18:07:18-04:00 Remove most uses of L.clean
* src/elab.ml (elab_check_sort, elab_check_def, infer_type): Skip `L.clean` since `lexp_string` already cleans up on the fly. (track_fv): Skip `L.clean` since `fv` already cleans up on the fly. (lexp_eval): Skip `L.clean` since `fv` and `erase_type` already clean up on the fly. (sform_new_attribute, sform_add_attribute, sform_built_in): Explicitly call `clean` now that `lexp_close` doesn't do it any more.
* src/eval.ml (from_lctx): Skip `L.clean` since `fv` and `erase_type` already clean up on the fly.
* src/lexp.ml (print_context_value): Remove `Expr` constructor. (pretty_ppctx): Remove unused `parent` and now unused `metavar`. (smap_lexp, pp_parent, pp_meta, set_parent, set_parent): Remove functions.. (lexp_str): Don't call `set_parent` any more. Rewrite metavar case to use `metavar_lookup` rather than `clean`.
* src/opslexp.ml (lexp_close): Don't call `clean` any more. (conv_p', mkSLlub): Skip `L.clean` since `level_canon` already cleans up on the fly. (check''.assert_type): Skip `L.clean` since `lexp_string` already cleans up on the fly. (erase_type): Clean up metavars on the fly.
* src/unification.ml (unify_metavar): Skip `L.clean` since `lexp_string` already cleans up on the fly.
- - - - - bf3c818e by Jean-Alexandre Barszcz at 2020-04-12T02:05:40-04:00 Add a nix shell
* shell.nix : When using nixpkgs/nixos, run `nix-shell` to get a shell with Typer's dependencies available.
- - - - - c39ff3d5 by Jean-Alexandre Barszcz at 2020-04-12T02:05:40-04:00 Improve the implementation of Sexp.dispatch
* src/elab.ml (sexp_dispatch) : Sexp.dispatch assumed that its arguments were closures. Instead, we use eval_call and also accept constructors, builtins, etc.
- - - - - 7b623a26 by Jean-Alexandre Barszcz at 2020-04-12T02:05:40-04:00 Add the inductive type `Sexp_wrapper` to match on sexps
* btl/pervasive.typer : Add the inductive type `Sexp_wrapper` to wrap the Sexp values in typer code, and the function `Sexp_wrap` to do the wrapping. This makes possible the use of pattern matching to destructure Sexps instead of the more verbose calls to `Sexp_dispatch`.
- - - - - 8419c419 by Jean-Alexandre Barszcz at 2020-04-12T02:05:40-04:00 Fix lexp_whnf when the case scrutinee is a call
* src/opslexp.ml (lexp_whnf) : Make sure that we take the WHNF of the function when the scrutinee of a case expression is a call, before checking that the function is a constructor. Otherwise, expressions like `case (let ... in (constructor ...))` fail to reduce, for example.
- - - - - cc20d841 by Jean-Alexandre Barszcz at 2020-04-12T02:05:40-04:00 Fix some lexp constructor calls where hash-consing has been forgotten
- - - - - 95330ac8 by Stefan Monnier at 2020-08-04T19:23:58-04:00 Add preliminary support for Dune
* src/tweak.ml: Remove, unused. * src/*.ml: Fix misc compiler warnings.
- - - - - 2bd6aa15 by Stefan Monnier at 2020-08-10T23:52:31-04:00 * btl/builtins.typer (Eq_comm): Update FIXME
- - - - - 28d16874 by irradiee at 2020-08-14T05:59:20-04:00 Add hash in Lexp's type (hash-consing). Lexp: type lexp is now a pair int * lexp' (interchangeable), profiling: add compilation with ocamlc & ocamlopt, collisions: add %cl command to get stats of hash-consing, Lexp tests: add tests and getters for some Lexp
- - - - - f04cab52 by Jean-Alexandre Barszcz at 2020-08-19T17:14:33-04:00 Delay parsing of declarations until elaboration for define-operator
* elab.ml (lexp_p_decls): Add a parameter for unparsed tokens, so that later declarations can be parsed in a context with newly declared operators
- - - - - 456370bc by Jean-Alexandre Barszcz at 2020-08-19T17:14:33-04:00 Remove the parsing error for tightly binding postfix operators
- - - - - 8beb9266 by Jean-Alexandre Barszcz at 2020-08-19T17:14:33-04:00 Dump the evaluation context when the variable names don't match
- - - - - 2e00884b by Jean-Alexandre Barszcz at 2020-08-19T17:14:33-04:00 Assign the builtins Int.+, etc to suitable variables Int_+, etc.
_+_ can be Int.+ by default, but we should also keep that value in Int_+ in case _+_ gets reassigned (with a num typeclass, for instance).
- - - - - ac4cc3a5 by Jean-Alexandre Barszcz at 2020-08-20T15:01:14-04:00 Apply the instantiated metavariable substs when displaying lexps
- - - - - f0b33b28 by Jean-Alexandre Barszcz at 2020-08-20T15:01:36-04:00 Replace instantiated metavars when checking syntactic equality
- - - - - 68f25184 by irradiee at 2020-08-24T13:11:01-04:00 Add hash in Lexp's type (hash-consing). Lexp: type lexp is now a pair int * lexp' (interchangeable), profiling: add compilation with ocamlc & ocamlopt, collisions: add %cl command to get stats of hash-consing, Lexp tests: add tests and getters for some Lexp
- - - - - 588b6327 by Jean-Alexandre Barszcz at 2020-09-04T23:06:53-04:00 Fix `lexp_whnf` for Case
A substitution built with `cons`es happens all at once, in the sense that the terms in such a list are substituted independently, and thus should not be shifted one relative to another.
This commit removes such a shift that was made by mistake in the computation of the WHNF of a `Case` redex. The shift caused debruijn indexing errors in the body of branches with multiple fields.
Additionnally, this commit removes the arguments to the inductive type from the substitution applied to the branch, since they are not bound by the case.
- - - - - 115d8b01 by Simon Génier at 2020-09-09T12:06:50-04:00 Make eval tests throw on a compilation failure.
- - - - - e8257259 by Simon Génier at 2020-09-09T12:06:59-04:00 Remove commented eval test.
- - - - - 940ade63 by Simon Génier at 2020-09-09T12:06:59-04:00 Do not print callstack of test handler.
This line always print the same callstack, that of the handler, which gives no information about why the test failed.
- - - - - 53c514f5 by Simon Génier at 2020-09-09T12:06:59-04:00 Actually record the backtrace of exceptions while testing.
- - - - - e0d4964e by Simon Génier at 2020-09-09T12:06:59-04:00 Print compiler log on a compilation error in tests.
- - - - - e290b701 by Simon Génier at 2020-09-09T12:06:59-04:00 Fix implicit arguments test.
- - - - - 5f740bf1 by Simon Génier at 2020-09-09T12:06:59-04:00 Fix case test with generic types.
- - - - - b6466a2b by Simon Génier at 2020-09-09T12:07:23-04:00 Fix the rest of the eval tests.
- - - - - 2041b4dd by Simon Génier at 2020-09-09T12:07:34-04:00 Remove = at the end of the flags to the test driver.
I think the intention was to have GNU style flags like --verbose=3, but that does not even work.
- - - - - 56e4fbed by Simon Génier at 2020-09-09T13:24:41-04:00 Easier elaboration tests.
I extracted these changes from another branch since I will need them for yet another. Ther should make elaboration tests easier to write. * New assertions reduce the amount of code to check the results. * Correctly restore state to be able to compare metavariables in two different code fragments.
- - - - - 9d41029c by Simon Génier at 2020-09-09T13:24:48-04:00 Rework add_test to avoid warnings.
- - - - - 10c27014 by Simon Génier at 2020-09-09T13:24:48-04:00 Make success and failure values.
- - - - - 18f49df0 by Simon Génier at 2020-09-09T13:31:55-04:00 Make expected an optional argument in elaboration tests.
- - - - - b7eb8f08 by Simon Génier at 2020-09-09T14:08:48-04:00 Fix safe head test.
- - - - - a8e2af1a by Simon Génier at 2020-09-10T09:38:07-04:00 Oops: add back running tests in the order they were inserted.
- - - - - a4540d14 by Simon Génier at 2020-09-10T15:47:53-04:00 Merge changes to elaboration and evaluation tests.
- - - - - 4eac6264 by Simon Génier at 2020-09-10T16:05:31-04:00 Get rid of warning by using String.uppercase_ascii.
This function is available since 4.03, and 4.05 is now on Debian stable so it is safe to use.
- - - - - a5a05e7b by Simon Génier at 2020-09-11T17:22:08-04:00 Merge branch 'string-uppercase' into master.
- - - - - c34d6d0c by Jean-Alexandre Barszcz at 2020-09-13T17:06:35-04:00 Fix an issue in the unification of metavariables
The issue was that unification was not idempotent in certain cases. In particular, when unifying a metavar that has a non-identity substitution (let's say lxp1) with a term (let's say lxp2) that refers to some metavariables, the corresponding metavariable references in the associated term (thus in lxp1 after association) could have different substitutions from the same references in lxp2. See the added comment for a more detailed example.
- - - - - 023ea461 by Jean-Alexandre Barszcz at 2020-09-13T17:06:35-04:00 Move the Eq builtin to debruijn.ml to make it available for elab.
- - - - - b4d53239 by Jean-Alexandre Barszcz at 2020-09-13T17:06:35-04:00 Make Eq.refl available to the ocaml code
* src/debruijn.ml : Add a definition of the lexp for Eq.refl
* src/builtin.ml : Register the constant Eq.refl
* btl/builtins.typer (Eq_refl) : Use the builtin variable ##Eq.refl instead of registering the builtin with the `Built-in` form. This ensures that we have the right variable and type, and might help to keep things in sync between the ocaml and typer code.
- - - - - efe2032d by Jean-Alexandre Barszcz at 2020-09-13T17:06:35-04:00 Make the case elaboration code more consistent
This commit doesn't substantially change the behavior of the case elaboration, but makes the code a bit more consistent and might save some unnecessary metavariables in some cases.
- - - - - 4c632a1f by Jean-Alexandre Barszcz at 2020-09-14T15:56:01-04:00 Add dependent elimination
This commit changes elaboration, conversion, typechecking, erasure, and the computation of free variables and WHNFs for case expressions, to account for the fact that the context of all the branches of case expressions is extended with a proof of equality between the branch's head and the case's target. Careful elimination of this equality proof with Eq_cast makes dependent elimination possible.
- - - - - b082a329 by Jean-Alexandre Barszcz at 2020-09-14T15:56:01-04:00 Conversion for metavariables
- - - - - fd990da1 by Jean-Alexandre Barszcz at 2020-09-14T15:56:01-04:00 Case conversion
- - - - - eb1741eb by Simon Génier at 2020-09-16T09:21:42-04:00 Update the requirements for building typer.
* Add tools and libraries. * Bump OCaml version to the latest one on Debian stable.
- - - - - bcb53b2c by Simon Génier at 2020-09-16T09:21:42-04:00 Use Map.S.find_opt.
- - - - - b36d30ac by Simon Génier at 2020-09-16T09:21:42-04:00 Oops: fix broken tests on OCaml 4.05.0.
- - - - - 1fb4ed6c by Simon Génier at 2020-09-16T09:23:33-04:00 Merge branch 'update-requirements' into HEAD
- - - - - d3a9e581 by Jean-Alexandre Barszcz at 2020-09-25T22:26:59-04:00 * src/eval.ml: Add overflow checking to the Int builtin operators
* tests/eval_test.ml: Test that overflows cause runtime errors
- - - - - 7e07d97d by Jean-Alexandre Barszcz at 2020-09-25T22:33:21-04:00 * src/sexp.ml (sexp): Use Zarith's big integers in sexps.
* btl/builtins.typer: Add the builtin `Integer->Int`. * src/eval.ml: Implement it. (sexp_dispatch): Fix the value passed to the integer handler.
- - - - - 043275cd by Jean-Alexandre Barszcz at 2020-09-25T23:18:39-04:00 * btl/pervasive.typer (quote1): Fix quoting for literals
- - - - - 8a7b7910 by Jean-Alexandre Barszcz at 2020-09-25T23:18:39-04:00 Add a macro for dependent elimination
* btl/depelim.typer: New file, implements the macro. * btl/pervasive.typer: Load the new macro. * tests/elab_test.ml: Test it.
- - - - - c722732e by Jean-Alexandre Barszcz at 2020-09-25T23:18:39-04:00 * src/unification.ml: Clarify the order of the handlers
Try and impose some logic on the order in which the various unification cases are handled.
(unify'): Shuffle. (unify_*): Simplify accordingly. (unify_call): Handle calls of different length.
* tests/unify_test.ml: Rewrite and enable the tests.
- - - - - ad090c1f by Jean-Alexandre Barszcz at 2020-09-25T23:18:39-04:00 * src/elab.ml (sform_lambda): Use unify instead of conv_p.
(unify_or_error): New function, extracted from check_inferred. (check_inferred): Use it.
- - - - - bc81cad7 by Jean-Alexandre Barszcz at 2020-11-05T14:13:57-05:00 * src/opslexp.ml (clean_map): Fix the erasure of Case expressions.
Substitute the erased variables in the branch bodies.
* tests/eval_test.ml: Test the fix.
- - - - - 9111345b by Jean-Alexandre Barszcz at 2020-11-05T14:15:56-05:00 * src/opslexp.ml: Name the substitute dummy used for erasure.
(erasure_dummy): The new dummy.
(erase_type, clean_default, clean_map): Use it.
- - - - - e04cd437 by Jean-Alexandre Barszcz at 2020-11-05T14:16:00-05:00 * tests/utest_main.ml (main): Quote arguments to system commands.
This make it possible to focus on tests that have spaces in their title.
- - - - - 44b54d2a by Jean-Alexandre Barszcz at 2020-11-05T14:16:00-05:00 * src/opslexp.ml (erase_type): Fail for all (even erased) metavars.
* btl/builtins.typer (Eq_comm): Correct the FIXME.
- - - - - 98183f18 by Jean-Alexandre Barszcz at 2020-11-05T14:16:00-05:00 * src/elab.ml (sform_load): Raise error when file is not found.
- - - - - eab5fa77 by Jean-Alexandre Barszcz at 2020-11-05T14:16:00-05:00 * src/elab.ml (move_typelevel_to_front -> sort_generalized_metavars)
Replace `move_typelevel_to_front` with the new function `sort_generalized_metavars`, which, in addition to bringing the typelevel parameters to the front, sorts the remaining generalized metavariables topologically so that later variables can depend on ealier ones, and ignores metavariables that are in lower scope levels.
(generalize): Call the new function.
- - - - - 7bcbc61e by Jean-Alexandre Barszcz at 2020-11-05T14:16:00-05:00 * src/lexp.ml (hc_eq, eq): Catch exception from `List.for_all2`.
- - - - - bb33116e by Jean-Alexandre Barszcz at 2020-11-05T14:20:44-05:00 * src/elab.ml (sform_identifier): Add error in elab of metavars.
Add a FIXME and an internal error instead of using a wrong substitution in the elaboration of a repeated metavariable.
- - - - - 0b414a46 by Jean-Alexandre Barszcz at 2020-11-05T14:20:44-05:00 * src/opslexp.ml (eq_cast_whnf): New, adds WHNF for `Eq.cast`.
(lexp_whnf_aux): Add the reduction of calls to builtins, for registered builtins.
* tests/elab_test.ml: Test the WHNF of `Eq.cast`.
- - - - - d74651cf by Simon Génier at 2020-11-25T10:59:52-05:00 Get rid of attributes on builtin.
- - - - - f73bc318 by Simon Génier at 2020-12-01T23:35:45-05:00 Merge branch 'remove-attributes' into HEAD
- - - - - c0df7b8b by Simon Génier at 2020-12-02T11:36:56-05:00 Cosmetic changes to utest_main.ml.
Some of these changes bring the style more in line with the GNU coding standard that is used for Typer. - Reindent file to 2 spaces. - Break lines before a operator. - Break lines before 80 columns.
Others are my attempts to improve readability. - Use functions specialized on refs in Arg. - Remove superfluous parenthesis. - Extract large fun expressions to local let bindings.
- - - - - 077b4494 by Simon Génier at 2020-12-02T12:05:43-05:00 Utest_main now also handle Windows paths.
- - - - - a4cc1ea7 by Simon Génier at 2020-12-03T12:13:32-05:00 Merge branch 'utests-main-windows'
- - - - - 1ce7599d by Simon Génier at 2020-12-04T09:56:45-05:00 Add opaque values for identifying data constructors.
This patch add a new primitive type, ##DataconsLabel, which uniquely identifies a data constructor within a type. Its inhabitants will be consumed by Low Level Typer to write the correct header for objects. The goal is to give an abstract type that is as useful on Typer on OCaml where the labels are strings than on a future backend which will be better for Low Level Typer and where labels will likely be integers.
Values are created through the primitive ##datacons-label<-string and there is also a macro datacons-label which allows us to write a symbol directly. I choosed to use a right pointing arrow its name, against the Lisp convention. I think it makes more sense in languages with an ML syntax because function composition is made like this
c<-b . b<-a
and it also goes in the same direction as the b_of_a convention in OCaml. I also though it was OK because there where no other primitives with arrows in their names so that convention does not clash with others.
Finally, I decided to go against the name ##Discriminent because it suggests it only applies to sum types, but ##DataconsLabel is also needed for product types.
- - - - - 5a31e992 by Simon Génier at 2020-12-05T14:46:49-05:00 Merge branch 'datacons-label'
- - - - - ffb8bf48 by Simon Génier at 2020-12-06T21:28:13-05:00 Add primitives for separate allocation and initialization.
- - - - - 955c3940 by Simon Génier at 2020-12-12T06:59:37-05:00 Fix a couple of warning 40.
- - - - - 085f3f58 by Simon Génier at 2020-12-22T12:40:18-05:00 Merge branch 'warning-40-be-gone'
- - - - - 5335bac8 by Simon Génier at 2020-12-22T12:40:34-05:00 Merge branch 'heap'
- - - - - 8741ee4f by Jean-Alexandre Barszcz at 2021-01-04T18:30:51-05:00 * src/opslexp.ml (clean_decls): Oops, make it check for metavars.
- - - - - 14d0ad7a by Jean-Alexandre Barszcz at 2021-01-04T18:30:51-05:00 * src/elab.ml (sform_letin): Remove unnecessary scope_level bump.
- - - - - 1c6e109b by Jean-Alexandre Barszcz at 2021-01-04T18:30:51-05:00 * src/elab.ml (sform_letin): Make `let` bidirectional.
- - - - - fecec539 by Jean-Alexandre Barszcz at 2021-01-04T18:30:51-05:00 * src/opslexp.ml (fv): Check that the memoized value is still ok.
- - - - - 77981fd4 by Stefan Monnier at 2021-02-09T18:04:24-05:00 * src/elab.ml (lexp_check_decls): Fix broken odd/even example.
* src/REPL.ml (main): Re-raise internal error, so OCAMLRUNPARAM=b gives a proper backtrace.
* samples/nat.typer (even1): Make it trickier to catch the previous error..
- - - - - d17622a1 by Simon Génier at 2021-03-08T12:46:52-05:00 Truncate the lexp context that is printed on error.
You can still opt in the whole thing by passing -Vfull-lctx.
- - - - - a2a6e95e by Simon Génier at 2021-03-08T13:24:54-05:00 Merge branch 'truncate-lctx'
- - - - - 73f177d8 by Stefan Monnier at 2021-03-10T11:10:11-05:00 Merge remote-tracking branch 'gitlab/dune' into trunk
- - - - - 9aef5033 by Simon Génier at 2021-03-10T13:30:23-05:00 Add information about the arity of data cons in Elexps.
This is not used with the AST interpreter, but pretty much any other backend would want that information.
- - - - - 6d930fcb by Simon Génier at 2021-03-10T15:30:17-05:00 Merge branch 'arity-of-cons'
- - - - - 952f92e3 by Simon Génier at 2021-03-19T09:45:17-04:00 [Myers] Add nth_opt and reverse.
- - - - - b3875d28 by Simon Génier at 2021-03-22T15:59:01-04:00 Introduce source objects.
Source objects abstract over the text of Typer code. Does it come from a file? A string? Only the source object knows.
I extracted it from my Typer to Scheme compiler patch. By itself, I think it makes for slightly nicer code, but the real advantages are * We no longer process source text line by line. Supporting multi-line string is now as easy as removing the error. * We keep the full source text around. We can add it to locations so we are able to print the original source along an error message.
- - - - - e3fb3f5e by Simon Génier at 2021-03-24T19:54:15-04:00 [Source] Do not buffer more than one line.
- - - - - 424af536 by Simon Génier at 2021-04-02T16:11:45-04:00 Merge branch 'source-object'
- - - - - 0590a584 by Simon Génier at 2021-04-04T21:50:28-04:00 Use the environment augmented with the new bindings for type erasure.
- - - - - b3886bc0 by Simon Génier at 2021-04-04T21:51:47-04:00 Remove a test testing incorrect code.
- - - - - 0e3dcf79 by Simon Génier at 2021-04-05T00:18:00-04:00 Merge branch 'broken-tests-2021-04'
- - - - - a8e4948d by Simon Génier at 2021-04-05T00:23:48-04:00 Dunify Typer tests.
- - - - - 6816e0aa by Simon Génier at 2021-04-07T15:35:15-04:00 Merge branch 'dunify-tests'
- - - - - ceed8e81 by Simon Génier at 2021-04-07T16:05:34-04:00 Move code related to command-line argument parsing out of REPL.
- - - - - e229996a by Simon Génier at 2021-04-09T13:41:26-04:00 Merge branch 'extract-args-from-repl'
- - - - - 252f6038 by Simon Génier at 2021-04-26T16:33:24-04:00 Introduce swappable backends for Typer.
The backends themselves are objects which must implement the new backend abstract class. I also shuffled some code, mostly in the module REPL, so that is it more focused on evaluating interactive code. Finally, I moved code that was more concerned with loading regular Typer code in typer.ml and elab.ml.
- - - - - 33b205c5 by Simon Génier at 2021-04-26T16:34:24-04:00 Add tests for the lexer.
In addition to the tests themselves, added a few functions that were necessary. In particular there is now Pretoken.equal in Prelexer and Location.equal in Source that are equality predicates on pretokens and locations.
I also added in Sexp.sexp_string support for printing the location along with its associated sexp. This is useful in tests, when we check that the locations are correct, otherwise we would print two identical sexps!
- - - - - ea5cae0f by Simon Génier at 2021-04-28T13:29:47-04:00 Merge branch 'lexer-tests'
- - - - - 9723f3cf by Simon Génier at 2021-04-28T13:30:29-04:00 Merge branch 'backend-object'
- - - - - 73ae25a9 by Simon Génier at 2021-04-28T13:34:46-04:00 Add a backend to compile Typer to Scheme.
- - - - - f8c0ef45 by Simon Génier at 2021-04-28T13:53:58-04:00 Consolidate location related code into Source.
The purpose of this changeset is to take all the Location related code and to move it into the Source module. I kept the aliases in Util for now to reduce the size of this changeset, but it was inevitable that I had to add a few `let open Source.Location in` because of how fields work in OCaml (not great). Fortunately, most of these will disappear as I move more and more location related code inside the source object.
I rewrote a few places to use printf instead of a series of prints, which I think are clearer. The only externally visible change is that I merged two functions that printed location in a different way. Some debug code used to print something like "Ln 32, cl 1", but now prints "foo.typer:32:1" like everywhere else.
- - - - - 965cc049 by Simon Génier at 2021-04-29T11:46:14-04:00 Merge branch 'gambit'
- - - - - 8ce3d27f by Simon Génier at 2021-05-10T15:14:17-04:00 Add code to check if a type declaration is positive.
- - - - - 4d0dff15 by Simon Génier at 2021-05-12T15:55:42-04:00 Merge branch 'origin/consolidate-location'
- - - - - f2d6d5df by Simon Génier at 2021-05-12T15:56:34-04:00 Merge branch positivity
- - - - - b8959e2f by Simon Génier at 2021-05-12T21:36:47-04:00 Have the source tell its own location.
Move the code that keeps track of the current line and column inside of the source object. Not only does this make sense conceptually since the source is a kind of cursor, but it will allow us to simplify the lexer code.
- - - - - e7d3ed86 by Simon Génier at 2021-05-28T19:51:54-04:00 Merge branch 'source-tells-its-own-location'
- - - - - c5ef2f59 by Simon Génier at 2021-05-28T20:30:37-04:00 Oops, fix tests on Windows.
The prelexer considered \r to be part of presymbols with catastrophic results.
- - - - - f289b62a by Simon Génier at 2021-05-29T12:12:42-04:00 Rewrite the Lexer module in terms of source objects.
This might not look useful, but it will simplify a great deal our next change of add and end point to location records since all the location related code will be in there source objects.
I ended up rewriting most of the Lexer. I tried to avoid doing that, but the offset handling code was so mixed up with the rest than that turned out to give worse code and a diff as unreadable. I'm pretty confident that that the changes are OK since we are still able to load pervasives.typer and I wrote a few tests for the trickier inner operators.
- - - - - 8e1be507 by Jean-Alexandre Barszcz at 2021-05-31T16:39:39-04:00 Fix nix shell and dune details
- - - - - dc07e915 by Jean-Alexandre Barszcz at 2021-05-31T16:39:39-04:00 * btl/pervasive.typer (type-impl): Accept implicit type params.
Also, allow type definitions at other type levels than 0, with an annotation.
- - - - - b8d1df5b by Jean-Alexandre Barszcz at 2021-05-31T16:39:39-04:00 * btl/pervasive.typer (type-impl): Keep the constructors in order.
- - - - - 8d9a2367 by Simon Génier at 2021-06-09T12:28:31-04:00 Merge branch 'lexer-with-source'
- - - - - 4fb0ccd3 by Simon Génier at 2021-06-09T12:40:18-04:00 Shorten the names of a few methods on source objects.
These names were redundants. For instance in `current_offset`, the `current` part is already hinted at by the fact that source objects are a kind of cursor. Overall I think the new names a clearer since they are more concise.
- - - - - a7ac505a by Jean-Alexandre Barszcz at 2021-08-10T14:58:56-04:00 * src/elab.ml (elaborate): `check_inferred` when a type is given.
Previously, `check_inferred` was mainly called from `check`, but some calls to `elaborate` play the same role as `check` (if an expected type is given), so we move this logic to `elaborate`. This allows implicit arguments to be instantiated in more places. For example, calls and variables are always inferred, but without `check_inferred`, the type provided to `elaborate` would be ignored.
- - - - - aff91a51 by Simon Génier at 2021-09-28T17:16:11-04:00 Merge branch 'shorten-source-methods'
- - - - - e8a59f86 by Simon Génier at 2021-09-28T17:25:19-04:00 Replace raw offsets with points which also track line and column.
- - - - - 87882dea by Simon Génier at 2021-09-28T17:45:35-04:00 Compute location inside the source from the given point.
- - - - - fce0fac4 by Simon Génier at 2021-09-28T18:16:00-04:00 Upgrade to OCaml 4.11.
* Update the README * Remove a few functions that are now part of the standard library.
- - - - - 01e6295a by Simon Génier at 2021-09-29T11:09:53-04:00 Remove doc strings from Typer.
Doc strings are a good idea, but the implementation that was in Typer was not. They should not be hardcoded in the syntax of the langague, but rather a good implementation would use the metaprogramming capabilities of Typer to make them part of the standard library.
- - - - - 8cfa2243 by Simon Génier at 2021-09-30T11:39:27-04:00 Locations now track their end points.
- - - - - db1cf4da by Stefan Monnier at 2021-10-06T09:38:32-04:00 Merge remote-tracking branch 'gitlab/ocaml-4.11' into trunk
- - - - - 8efdff37 by Stefan Monnier at 2021-10-06T10:01:02-04:00 Merge remote-tracking branch 'gitlab/purge-docstr' into trunk
- - - - - 89cc2432 by Stefan Monnier at 2021-10-06T10:01:55-04:00 Merge remote-tracking branch 'gitlab/source-spans-2' into trunk
- - - - - f832b339 by Simon Génier at 2021-10-28T10:43:05-04:00 Remove artisanal formatting functions in favour of printf.
- - - - - 7f6f32dd by Simon Génier at 2021-10-28T10:43:38-04:00 Printfify log functions.
- - - - - edf888bc by Simon Génier at 2021-10-28T11:00:18-04:00 Typer accepts subcommands (repl, compile, run) like git.
This will hopefully simplify option handling as I add more modes of operation with their own option for running Typer code in a Gambit subprocess.
- - - - - d3daf0a3 by Soilih BEN SOILIH at 2022-02-16T10:07:07-05:00 Add a `Proj` constructor to the `lexp` type
We add a projection constructor to the Lexp type in order to be able to offer the completion in a satisfactory manner for the LSP server. When we write MODULE.FIELD, if FIELD doesn't exist, we could not offer the completion because the AST could not be generated at all. So we add this case to be able to have an AST and be able to find the functions of a module, and also select specific functions thanks to the label of a projection.
* src/lexp.ml (lexp): Add `Proj` constructor. (lexp'_hash, lexp_head, lexp_location, push_susp, clean, lexp_unparse) (lexp_str): Adjust accordingly. (mkProj): new function. * src/elab.ml (adjust_subst.loop): Add `Proj` case for the loop substitution. (sform_proj): new special form. (register_special_forms): Register it. * src/opslexp.ml (pos_of_label): new function. (check'', get_type, fv, erase_type): * src/positivity.ml (positive'): Add new case for `Proj`. * src/eval.ml (eval): * src/apply_inv_subst.ml (apply_inv_subst): * src/elexp.ml (elexp, elexp_location, elexp_name, elexp_string): Add new case for `Proj`. * btl/pervasive.typer (__/.__): Delete macro.
- - - - - 29c8aded by Simon Génier at 2022-02-16T19:17:56-05:00 Add a flag to show macros, their arguments and the expanded code.
- - - - - 50069ddc by Shon Feder at 2022-03-11T20:42:03-05:00 Add Zarith dependency to opam file
Also adds "synopsis" and "description" fields, with content taken from https://www.iro.umontreal.ca/~monnier/
- - - - - 12c08fbb by Shon Feder at 2022-03-11T20:42:03-05:00 Ignore the opam switch directory
- - - - - 3a9417d8 by Stefan at 2022-08-26T19:24:00+00:00 Merge branch 'add-zarith-dependency' into 'master'
Add zarith dependency
See merge request monnier/typer!2 - - - - -
17 changed files:
- + .gitignore - + .travis.yml - + COPYING - + GNUmakefile - + README.md - + btl/builtins.typer - + btl/case.typer - + btl/depelim.typer - + btl/do.typer - + btl/dune - + btl/heap.typer - + btl/list.typer - + btl/pervasive.typer - + btl/plain-let.typer - + btl/polyfun.typer - + btl/tuple.typer - + debug_util.ml
The diff was not included because it is too large.
View it on GitLab: https://gitlab.com/monnier/typer/-/compare/f1727b0c61b851c1f7f9092b83befee1d...
Afficher les réponses par date
-
Stefan (＠monnier)