aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/reduction.ml
Commit message (Collapse)AuthorAge
* Remove Sorts.contentsGravatar Gaëtan Gilbert2018-06-26
|
* Define and use UGraph.enforce_leq_alg for subtyping inferenceGravatar Gaëtan Gilbert2018-06-22
| | | | Not sure if worth using in other places.
* Merge PR #7496: Fix #4403: insufficient handling of type-in-type in kernel.Gravatar Maxime Dénès2018-06-04
|\
* | Fix #7333: vm_compute segfaults / Anomaly with cofixGravatar Maxime Dénès2018-05-28
| | | | | | | | | | We eta-expand cofixpoints when needed, so that their call-by-need evaluation is correctly implemented by VM and native_compute.
* | Remove vm_conv hook and reorganize kernel filesGravatar Maxime Dénès2018-05-28
| |
* | Exporting Fun1 within Array so that Array.Fun1 and not only CArray.Fun1 works.Gravatar Hugo Herbelin2018-05-23
| |
| * Fix #4403: insufficient handling of type-in-type in kernel.Gravatar Gaëtan Gilbert2018-05-13
|/
* Fix expected number of arguments for cumulative constructors.Gravatar Gaëtan Gilbert2018-03-09
| | | | | | | We expected `nparams + nrealargs + consnrealargs` but the `nrealargs` should not be there. This breaks cumulativity of constructors for any inductive with indices (so records still work, explaining why the test case in #6747 works).
* Merge PR #6775: Allow using cumulativity without forcing strict constraints.Gravatar Maxime Dénès2018-03-09
|\
* \ Merge PR #6769: Split closure cache and remove whd_bothGravatar Maxime Dénès2018-03-09
|\ \
| | * Cumulativity: improve treatment of irrelevant universes.Gravatar Gaëtan Gilbert2018-03-09
| |/ |/| | | | | | | | | In Reductionops.infer_conv we did not have enough information to properly try to unify irrelevant universes. This requires changing the Reduction.universe_compare type a bit.
* | Relax conversion of constructors according to the pCuIC modelGravatar Matthieu Sozeau2018-03-08
| | | | | | | | | | | | - Nothing to check in conversion as they have a common supertype by typing. - In inference, enforce that one is lower than the other.
* | Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\ \
| | * Remove whd_both from the kernel.Gravatar Pierre-Marie Pédrot2018-03-04
| | | | | | | | | | | | | | | Now that the cache is distinct, there should be no nasty side-effects changing the value of one side while reducing the other.
| | * Pass the constant cache as a separate argument in kernel reduction.Gravatar Pierre-Marie Pédrot2018-03-04
| |/ |/|
* | Merge PR #6734: dest_{prod,lam}: no Cast case (it's removed by whd)Gravatar Maxime Dénès2018-02-28
|\ \
| | * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
| |/ |/|
* | Merge PR #1082: Fixing Print for inductive types with let-in in parametersGravatar Maxime Dénès2018-02-12
|\ \
* \ \ Merge PR #6128: Simplification: cumulativity information is variance ↵Gravatar Maxime Dénès2018-02-12
|\ \ \ | | | | | | | | | | | | information.
* \ \ \ Merge PR #6674: Delay computation of lifts in the reduction machine.Gravatar Maxime Dénès2018-02-12
|\ \ \ \
| | * | | Universe instance printer: add optional variance argument.Gravatar Gaëtan Gilbert2018-02-11
| | | | |
| | * | | Use specialized function for inductive subtyping inference.Gravatar Gaëtan Gilbert2018-02-11
| | | | | | | | | | | | | | | | | | | | | | | | | This ensures by construction that we never infer constraints outside the variance model.
| | | | * dest_{prod,lam}: no Cast case (it's removed by whd)Gravatar Gaëtan Gilbert2018-02-11
| |_|_|/ |/| | |
| | * | Simplification: cumulativity information is variance information.Gravatar Gaëtan Gilbert2018-02-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Since cumulativity of an inductive type is the universe constraints which make a term convertible with its universe-renamed copy, the only constraints we can get are between a universe and its copy. As such we do not need to be able to represent arbitrary constraints between universes and copied universes in a double-sized ucontext, instead we can just keep around an array describing whether a bound universe is covariant, invariant or irrelevant (CIC has no contravariant conversion rule). Printing is fairly obtuse and should be improved: when we print the CumulativityInfo we add marks to the universes of the instance: = for invariant, + for covariant and * for irrelevant. ie Record Foo@{i j k} := { foo : Type@{i} -> Type@{j} }. Print Foo. gives Cumulative Record Foo : Type@{max(i+1, j+1)} := Build_Foo { foo : Type@{i} -> Type@{j} } (* =i +j *k |= *)
| | * | [get_cumulativity_constraints] allowing further code sharing.Gravatar Gaëtan Gilbert2018-02-10
| | | |
| | * | Factorize code for comparing maybe-cumulative inductives.Gravatar Gaëtan Gilbert2018-02-10
| |/ / |/| | | | | | | | | | | | | | The part in Reduction should be semantics preserving, but Reductionops only tried cumulativity if equality fails. This is probably wrong so I changed it.
* | | Merge PR #6685: Use whd-all on rigid-flex conversion.Gravatar Maxime Dénès2018-02-07
|\ \ \
| * | | Respect the transparent state of the current conversion on strong weak-head.Gravatar Pierre-Marie Pédrot2018-02-05
| | | | | | | | | | | | | | | | | | | | This fixes the previous patch in rare corner-cases where unification code was relying on both kernel conversion and specific transparent state.
| | * | Delay computation of lifts in the reduction machine.Gravatar Pierre-Marie Pédrot2018-02-04
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This definitely qualifies as a micro-optimization, but it would not be performed by Flambda. Indeed, it is unsound in general w.r.t. OCaml semantics, as it involves a fixpoint and changes potential non-termination. In our case it doesn't matter semantically, but it is indeed observable on computation intensive developments like UniMath.
* | | | kernel: cleanup projection unfoldingGravatar Gaëtan Gilbert2018-02-02
| |/ / |/| | | | | | | | | | | - use Redflags.red_projection - share unfold_projection between CClosure and Reduction
| * | Use whd-all on rigid-flex conversion.Gravatar Pierre-Marie Pédrot2018-02-02
|/ / | | | | | | | | | | | | | | | | | | | | | | | | This heuristic is justified by the fact that during a conversion check between a flexible and a rigid term, the flexible one is eventually going to be fully weak-head normalized. So in this case instead of performing many small reduction steps on the flexible term, we perform full weak-head reduction, including delta. It is slightly more efficient in actual developments, and it fixes a corner case encountered by Jason Gross. Fixes #6667: Kernel conversion is much, much slower than `Eval lazy`.
| * Fixing a bug of Print for inductive types with let-ins in parameters.Gravatar Hugo Herbelin2017-12-14
| | | | | | | | | | | | | | Adding a "let-in"-sensitive function hnf_prod_applist_assum to instantiate parameters and using it for printing. Thanks to PMP for reporting.
* | Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.Gravatar Maxime Dénès2017-12-14
|\ \ | |/ |/|
* | [api] Remove yet another type alias.Gravatar Emilio Jesus Gallego Arias2017-12-09
| |
| * [lib] Rename Profile to CProfileGravatar Emilio Jesus Gallego Arias2017-12-09
|/ | | | | New module introduced in OCaml 4.05 I think, can create problems when linking with the OCaml toplevel for `Drop`.
* Make some functions on terms more robust w.r.t new term constructs.Gravatar Maxime Dénès2017-11-23
| | | | | | Extending terms is notoriously difficult. We try to get more help from the compiler by making sure such an extension will trigger non exhaustive pattern matching warnings.
* Merge PR #6058: Remove redundant env argument to Reduction.ccnvGravatar Maxime Dénès2017-11-15
|\
* | [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
| | | | | | | | We do up to `Term` which is the main bulk of the changes.
* | [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
| | | | | | | | This will allow to merge back `Names` with `API.Names`
| * Remove redundant env argument to Reduction.ccnvGravatar Gaëtan Gilbert2017-11-02
|/ | | | | The infos already contain the env. Note that it was only actually used in the 2 lookup_mind lines.
* Less footguns in universe handling: remove subst_instance_context.Gravatar Pierre-Marie Pédrot2017-07-11
| | | | | This function was lurking around, waiting to bite anybody willing to use it. We use instead a better API, correct and much less error-prone.
* Getting rid of simple calls to AUContext.instance.Gravatar Pierre-Marie Pédrot2017-07-11
| | | | | | This function breaks the abstraction barrier of abstract universe contexts, as it provides a way to observe the bound names of such a context. We remove all the uses that can be easily get rid of with the current API.
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* Fix a bug in cumulativityGravatar Amin Timany2017-06-16
|
* OptimizationGravatar Amin Timany2017-06-16
| | | | | Only try using cumulativity in conversion/subtyping if the universe instances are non-empty
* Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
|
* Fix bugs and add an option for cumulativityGravatar Amin Timany2017-06-16
|
* Fix bugsGravatar Amin Timany2017-06-16
|
* Squashed commit of the following:Gravatar Amin Timany2017-06-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Except I have disabled the minimization of universes after sections as it seems to interfere with the STM machinery causing files like test-suite/vio/print.v to loop when processed asynchronously. This is very peculiar and needs more investigation as the aforementioned file does not have any sections or any universe polymorphic definitions! commit fc785326080b9451eb4700b16ccd3f7df214e0ed Author: Amin Timany <amintimany@gmail.com> Date: Mon Apr 24 17:14:21 2017 +0200 Revert STL to monomorphic commit 62b573fb13d290d8fe4c85822da62d3e5e2a6996 Author: Amin Timany <amintimany@gmail.com> Date: Mon Apr 24 17:02:42 2017 +0200 Try unifying universes before apply subtyping commit ff393742c37b9241c83498e84c2274967a1a58dc Author: Amin Timany <amintimany@gmail.com> Date: Sun Apr 23 13:49:04 2017 +0200 Compile more of STL with universe polymorphism commit 5c831b41ebd1fc32e2dd976697c8e474f48580d6 Author: Amin Timany <amintimany@gmail.com> Date: Tue Apr 18 21:26:45 2017 +0200 Made more progress on compiling the standard library commit b8550ffcce0861794116eb3b12b84e1158c2b4f8 Author: Amin Timany <amintimany@gmail.com> Date: Sun Apr 16 22:55:19 2017 +0200 Make more number theoretic modules monomorphic commit 29d126d4d4910683f7e6aada2a25209151e41b10 Author: Amin Timany <amintimany@gmail.com> Date: Fri Apr 14 16:11:48 2017 +0200 WIP more of standard library compiles Also: Matthieu fixed a bug in rewrite system which was faulty when introducing new morphisms (Add Morphism) command. commit 23bc33b843f098acaba4c63c71c68f79c4641f8c Author: Amin Timany <amintimany@gmail.com> Date: Fri Apr 14 11:39:21 2017 +0200 WIP: more of the standard library compiles We have implemented convertibility of constructors up-to mutual subtyping of their corresponding inductive types. This is similar to the behavior of template polymorphism. commit d0abc5c50d593404fb41b98d588c3843382afd4f Author: Amin Timany <amintimany@gmail.com> Date: Wed Apr 12 19:02:39 2017 +0200 WIP: trying to get the standard library compile with universe polymorphism We are trying to prune universes after section ends. Sections add a load of universes that are not appearing in the body, type or the constraints.
* Fix cum/conv for inductive typesGravatar Amin Timany2017-06-16
| | | | | Fall back to the equating levels in case inductive is not fully applied instead of failing.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 00:29:48 +0000