quox/lib/quox-lib.ipkg

package quox-lib
version = 0

authors   = "rhiannon morris"
sourceloc = "https://git.rhiannon.website/rhi/quox"
license   = "acsl"

depends =
  base, contrib, elab-util, sop, snocvect, eff, prettier,
  pretty-show, parser-show

modules =
  Text.PrettyPrint.Bernardy.Core.Decorate,
  Control.Monad.ST.Extra,
  Quox.BoolExtra,
  Quox.CharExtra,
  Quox.NatExtra,
  Quox.EffExtra,
  Quox.PrettyValExtra,
  Quox.Decidable,
  Quox.No,
  Quox.Log,
  Quox.Loc,
  Quox.Semiring,
  Quox.Polynomial,
  Quox.Var,
  Quox.Scoped,
  Quox.OPE,
  Quox.Pretty,
  Quox.Syntax,
  Quox.Syntax.Builtin,
  Quox.Syntax.Dim,
  Quox.Syntax.DimEq,
  Quox.Syntax.Qty,
  Quox.Syntax.Shift,
  Quox.Syntax.Subst,
  Quox.Syntax.Term,
  Quox.Syntax.Term.TyConKind,
  Quox.Syntax.Term.Base,
  Quox.Syntax.Term.Tighten,
  Quox.Syntax.Term.Pretty,
  Quox.Syntax.Term.Subst,
  Quox.FreeVars,
  Quox.Displace,
  Quox.Definition,
  Quox.Whnf.Interface,
  Quox.Whnf.ComputeElimType,
  Quox.Whnf.TypeCase,
  Quox.Whnf.Coercion,
  Quox.Whnf.Main,
  Quox.Whnf,
  Quox.Context,
  Quox.Equal,
  Quox.Name,
  Quox.Typing.Context,
  Quox.Typing.EqMode,
  Quox.Typing.Error,
  Quox.Typing,
  Quox.Typechecker,
  Quox.CheckBuiltin,
  Quox.Parser.Lexer,
  Quox.Parser.Syntax,
  Quox.Parser.Parser,
  Quox.Parser.LoadFile,
  Quox.Parser.FromParser,
  Quox.Parser.FromParser.Error,
  Quox.Parser,
  Quox.Untyped.Syntax,
  Quox.Untyped.Erase,
  Quox.Untyped.Scheme
renamings 2022-05-04 20:13:56 +02:00			`package quox-lib`
wip nix 2022-05-04 17:09:49 +02:00			`version = 0`

			`authors = "rhiannon morris"`
			`sourceloc = "https://git.rhiannon.website/rhi/quox"`
			`license = "acsl"`

add PrettyVal stuff for parser AST 2023-10-20 04:53:20 +02:00			`depends =`
			`base, contrib, elab-util, sop, snocvect, eff, prettier,`
			`pretty-show, parser-show`
wip nix 2022-05-04 17:09:49 +02:00
			`modules =`
rewrite pretty printer 2023-05-14 19:58:46 +02:00			`Text.PrettyPrint.Bernardy.Core.Decorate,`
use ST from base 2023-09-19 00:41:47 +02:00			`Control.Monad.ST.Extra,`
add BoolExtra 2023-02-22 05:42:56 +01:00			`Quox.BoolExtra,`
lexer 2023-02-28 20:51:54 +01:00			`Quox.CharExtra,`
re-add tightening and use it when messing with scopes e.g. "coe [_ ⇒ A] @p @q s" should immediately reduce to "s", but if the "_ ⇒ A" happened to use an SY it didn't. this will still happen if a wrong SY sneaks in but the alternative is re-traversing the term over and over every time whnf runs 2023-04-17 20:56:31 +02:00			`Quox.NatExtra,`
mtl ⇒ eff 2023-03-31 19:23:30 +02:00			`Quox.EffExtra,`
add PrettyVal stuff for parser AST 2023-10-20 04:53:20 +02:00			`Quox.PrettyValExtra,`
add Decidable-related stuff 2023-01-09 23:43:23 +01:00			`Quox.Decidable,`
whnf actually reduces to whnf now (probably) 2023-01-23 00:53:34 +01:00			`Quox.No,`
add Q.Log 2024-04-04 18:11:26 +02:00			`Quox.Log,`
add file locations to Parser.Syntax they're immediately thrown away currently. but one step at a time 2023-04-26 02:47:42 +02:00			`Quox.Loc,`
add polynomials 2024-05-27 20:22:32 +02:00			`Quox.Semiring,`
			`Quox.Polynomial,`
move Quox.Syntax.Var to just Quox.Var 2023-09-20 21:56:59 +02:00			`Quox.Var,`
move Scoped to separate module 2023-09-20 21:58:04 +02:00			`Quox.Scoped,`
re-add tightening and use it when messing with scopes e.g. "coe [_ ⇒ A] @p @q s" should immediately reduce to "s", but if the "_ ⇒ A" happened to use an SY it didn't. this will still happen if a wrong SY sneaks in but the alternative is re-traversing the term over and over every time whnf runs 2023-04-17 20:56:31 +02:00			`Quox.OPE,`
wip nix 2022-05-04 17:09:49 +02:00			`Quox.Pretty,`
			`Quox.Syntax,`
add CheckBuiltin 2024-04-14 15:48:43 +02:00			`Quox.Syntax.Builtin,`
wip nix 2022-05-04 17:09:49 +02:00			`Quox.Syntax.Dim,`
			`Quox.Syntax.DimEq,`
			`Quox.Syntax.Qty,`
			`Quox.Syntax.Shift,`
			`Quox.Syntax.Subst,`
			`Quox.Syntax.Term,`
coercions and compositions 2023-04-15 15:13:01 +02:00			`Quox.Syntax.Term.TyConKind,`
wip nix 2022-05-04 17:09:49 +02:00			`Quox.Syntax.Term.Base,`
re-add tightening and use it when messing with scopes e.g. "coe [_ ⇒ A] @p @q s" should immediately reduce to "s", but if the "_ ⇒ A" happened to use an SY it didn't. this will still happen if a wrong SY sneaks in but the alternative is re-traversing the term over and over every time whnf runs 2023-04-17 20:56:31 +02:00			`Quox.Syntax.Term.Tighten,`
wip nix 2022-05-04 17:09:49 +02:00			`Quox.Syntax.Term.Pretty,`
			`Quox.Syntax.Term.Subst,`
add FreeVars, and split only on used dvars in Equal 2023-09-12 09:56:49 +02:00			`Quox.FreeVars,`
crude but effective stratification 2023-05-21 20:09:34 +02:00			`Quox.Displace,`
add Definitions module 2022-08-22 10:17:08 +02:00			`Quox.Definition,`
split up whnf module 2023-08-24 18:42:26 +02:00			`Quox.Whnf.Interface,`
			`Quox.Whnf.ComputeElimType,`
			`Quox.Whnf.TypeCase,`
			`Quox.Whnf.Coercion,`
			`Quox.Whnf.Main,`
			`Quox.Whnf,`
wip nix 2022-05-04 17:09:49 +02:00			`Quox.Context,`
			`Quox.Equal,`
			`Quox.Name,`
split up Quox.Typing 2023-03-13 21:41:57 +01:00			`Quox.Typing.Context,`
			`Quox.Typing.EqMode,`
			`Quox.Typing.Error,`
wip nix 2022-05-04 17:09:49 +02:00			`Quox.Typing,`
lexer 2023-02-28 20:51:54 +01:00			`Quox.Typechecker,`
add CheckBuiltin 2024-04-14 15:48:43 +02:00			`Quox.CheckBuiltin,`
more parser/FromParser stuff - top level semicolons optional - type optional [the def will need to be an elim] - `load` statement - namespaces 2023-03-12 18:28:37 +01:00			`Quox.Parser.Lexer,`
add module Parser.Syntax with PTerm and toPTerm 2023-03-05 14:55:04 +01:00			`Quox.Parser.Syntax,`
more parser/FromParser stuff - top level semicolons optional - type optional [the def will need to be an elim] - `load` statement - namespaces 2023-03-12 18:28:37 +01:00			`Quox.Parser.Parser,`
more effect stuff, incl. ST 2023-08-25 18:09:06 +02:00			`Quox.Parser.LoadFile,`
more parser/FromParser stuff - top level semicolons optional - type optional [the def will need to be an elim] - `load` statement - namespaces 2023-03-12 18:28:37 +01:00			`Quox.Parser.FromParser,`
printing for most of FromParserError 2023-03-31 19:27:38 +02:00			`Quox.Parser.FromParser.Error,`
untyped λ calculus syntax 2023-09-20 22:09:08 +02:00			`Quox.Parser,`
erasure to untyped syntax 2023-09-30 18:37:44 +02:00			`Quox.Untyped.Syntax,`
scheme output 2023-10-24 23:52:19 +02:00			`Quox.Untyped.Erase,`
			`Quox.Untyped.Scheme`