Code

Module implicts#1241

Code

Draft

xzxzlala wants to merge 153 commits intodevhazelgrove/hazel:devfrom module_implictshazelgrove/hazel:module_implictsCopy head branch name to clipboard

+9,209-192

Commits

Commits on May 17, 2023

• copy module from let

  gensofubi

  committed
  1135c5c

Commits on May 19, 2023

• a try on module

  gensofubi

  committed
  46cbc73

• minor changes

  gensofubi

  committed
  27c2d02

• keyword module done

  gensofubi

  committed
  1c66f50

• formatted

  gensofubi

  committed
  e07aed2

Commits on May 21, 2023

• concrete module typing (but no typeann yet) and dot access operator

  gensofubi

  committed
  9845316

Commits on May 24, 2023

• change the expected def pattern in module to Tag

  gensofubi

  committed
  29a4ffe

• change dot form to fit submodule

  gensofubi

  committed
  b261e45

Commits on May 31, 2023

• detailed typing information for modules and auto hole-insert fixed

  gensofubi

  committed
  2bb2e3f

Commits on Jun 1, 2023

• type annotation for module

  gensofubi

  committed
  e8ca644

Commits on Jun 2, 2023

• fit for module with 1 or 0 members

  gensofubi

  committed
  4aba625

Commits on Jun 7, 2023

• unsuccessful trial on fixing a bug

  gensofubi

  committed
  85fa3bd

• partially solve

  gensofubi

  committed
  3d26edd

• adjust behavior when module typeann is not consistent with member typeann

  gensofubi

  committed
  e1563a6

• adjust the behavior when member names are not consistent with module typeann

  gensofubi

  committed
  0a727c2

Commits on Jun 10, 2023

• Merge branch 'adt-defs-after' into haz3l-module

  gensofubi

  committed
  9c8d63e

Commits on Jun 11, 2023

• again change the expected def pattern in module to Tag

  gensofubi

  committed
  403eac5

Commits on Jun 14, 2023

• basic type members

  gensofubi

  committed
  3620771

Commits on Jun 15, 2023

• add comments

  gensofubi

  committed
  e97369c

Commits on Jun 16, 2023

• basic type alias in module's annotation

  gensofubi

  committed
  3f7db25

Commits on Jun 17, 2023

• change precedence for sum type alias in module annotation

  gensofubi

  committed
  b1c3b6d

• fix for Tags in module

  gensofubi

  committed
  9377765

• in analitic mode, use constructors without prefix

  gensofubi

  committed
  fc8a9d5

Commits on Jun 18, 2023

• differ module type member with type variable with same name

  gensofubi

  committed
  0a11c6f

• fix minor problems

  gensofubi

  committed
  9bb1796

• adjust typing information display for module type members

  gensofubi

  committed
  0f11919

Commits on Jun 21, 2023

• Providing warnings for using type members that are not defined, and inconsistency for type members

  gensofubi

  committed
  45b8c80

• Merge remote-tracking branch 'origin/dev' into haz3l-module

  gensofubi

  committed
  c9cbf2a

Commits on Jun 28, 2023

• module langdoc copied from let

  gensofubi

  committed
  a6691dc

Commits on Jun 29, 2023

• module def langdoc

  gensofubi

  committed
  09384db

• Merge remote-tracking branch 'origin/adt-defs-after' into haz3l-module

  gensofubi

  committed
  477650a

Commits on Jun 30, 2023

• tyalias pat langdoc

  gensofubi

  committed
  658e4f5

• dot expression langdoc

  gensofubi

  committed
  f097644

• module type langdoc

  gensofubi

  committed
  0f25baa

Commits on Jul 1, 2023

• dot type langdoc

  gensofubi

  committed
  e247813

Commits on Jul 2, 2023

• fit the problem on using member variable with member type

  gensofubi

  committed
  449ac63

• adjust type view: remove trailing comma, let the earlier definitions to be displayed first

  gensofubi

  committed
  a02f806

• add tyalias for module having member type with same name

  gensofubi

  committed
  9373f44

Commits on Jul 5, 2023

• change dot type to be a Typ postfix

  gensofubi

  committed
  d2034ba

• type view adjusted

  gensofubi

  committed
  a57da2b

Commits on Jul 7, 2023

• Merge remote-tracking branch 'origin/adt-defs-after' into haz3l-module

  gensofubi

  committed
  24f6748

• fix exception when Applying Constructors defined in modules

  gensofubi

  committed
  1513e98

Commits on Jul 10, 2023

• add comments in Statics.re and Module.re, remove unused function in Ctx.re

  gensofubi

  committed
  d8108d6

Commits on Jul 11, 2023

• change error message for an invalid module name

  gensofubi

  committed
  14d5025

Commits on Jul 12, 2023

• detailed member value in DHDoc_Exp

  gensofubi

  committed
  9285692

Commits on Jul 13, 2023

• change dot to infix

  gensofubi

  committed
  c4c61b9

Commits on Jul 14, 2023

• Merge remote-tracking branch 'origin/adt-defs-after' into haz3l-module

  gensofubi

  committed
  660d88b

• rec type mem consistency

  gensofubi

  committed
  888ac62

• type member bug fix

  gensofubi

  committed
  1dc51e7

Commits on Jul 31, 2023

• Merge remote-tracking branch 'origin/adt-defs-after' into haz3l-module

  gensofubi

  committed
  8aaa894

Commits on Aug 7, 2023

• Merge remote-tracking branch 'origin/dev' into haz3l-module

  gensofubi

  committed
  483fc79

Commits on Aug 15, 2023

• change the cursor inspector print

  gensofubi

  committed
  cc51001

• langdoc modify

  gensofubi

  committed
  09aae62

Commits on Aug 16, 2023

• fix about ctrs in ana mode

  gensofubi

  committed
  4efc2e6

• change cls for capitalized var standing for modules

  gensofubi

  committed
  5f76744

Commits on Aug 17, 2023

• langdoc for module vars(exp,pat,typ)

  gensofubi

  committed
  abfe6db

Commits on Aug 18, 2023

• Add: mold and forms of parameterized type

  xzxzlala

  committed
  2606648

Commits on Aug 21, 2023

• Fix: the type in let works

  xzxzlala

  committed
  fe27614

Commits on Aug 22, 2023

• Fix: typeHole ann bug

  xzxzlala

  committed
  e08f671

• Fix: castfailed bug

  xzxzlala

  committed
  13a0d20

Commits on Aug 24, 2023

• merge in poly-adt

  

  disconcision

  authored and

  Crazycolorz5

  committed
  0bb43a6

• Fixed body_ctx of Forall and Rec in Statics

  

  AlienKevin

  authored and

  Crazycolorz5

  committed
  7e495cb

• Allow Indet on the left of TypAp in Evaluator, similar to Ap

  

  AlienKevin

  authored and

  Crazycolorz5

  committed
  bc7e471

• Fix mode of TypAp to Syn, not SynFun

  

  AlienKevin

  authored and

  Crazycolorz5

  committed
  ceee07c

• Update is_fun and is_fun_var to recognize forall

  

  AlienKevin

  authored and

  Crazycolorz5

  committed
  8770d6e

• Implement semantics of type function application as type substition on terms.

  Crazycolorz5

  committed
  031067e

• Add synthesis mode for type function and add necessary casting cases.

  Show description for d210f8f
  Crazycolorz5

  committed
  d210f8f

• Add rule for evaluation of type application on cast.

  Crazycolorz5

  committed
  4d02ccb

Commits on Aug 25, 2023

• Some resolutions to conflicts from rebasing.

  Crazycolorz5

  committed
  b52560c

• Resolving issues in Statics and Elaborator.

  Crazycolorz5

  committed
  7337f8f

• Edit constructors in frontend.

  Crazycolorz5

  committed
  d78057e

• Change dhexp substitution to use binding names rather than debrujin.

  Crazycolorz5

  committed
  06cbf1d

• Fix issue with looking up tvars in ctx.

  Crazycolorz5

  committed
  749da41

• Fix error in alpha equiv

  Crazycolorz5

  committed
  66870d3

Commits on Aug 26, 2023

• Fix typechecking with mismatching type variable names.

  Crazycolorz5

  committed
  e63913d

• Implement capture avoiding substitution.

  Crazycolorz5

  committed
  c3f44b4

• Add capture avoiding binding to recursive types.

  Crazycolorz5

  committed
  4ef0651

• Merge branch 'dev' into parameterized_types

  xzxzlala

  committed
  9d41608

Commits on Aug 27, 2023

• Merge remote-tracking branch 'origin/dev' into haz3l-module

  gensofubi

  committed
  c148a98

• merge typFun and typAp

  xzxzlala

  committed
  609997d

• Add: parameterized-types, leave the case branch not working

  xzxzlala

  committed
  9ccf619

Commits on Aug 28, 2023

• Add a comment to justify not needing capture avoidance in evaluator.

  Crazycolorz5

  committed
  93477bd

Commits on Aug 29, 2023

• Revise info and evaluator pattern match to fix the case branch inconsistent

  xzxzlala

  committed
  57f725e

• Rmove debug print code

  xzxzlala

  committed
  58e5cd7

• Fix: incorrect type of ctrs

  xzxzlala

  committed
  6442034

• Fix: typeann typehole cause case match failed

  xzxzlala

  committed
  3142ed3

• Fix: ctr_ap type error

  xzxzlala

  committed
  21e3365

Commits on Aug 30, 2023

• Add parentheses to left type of functions when necessary. Lowercase forall and rec.

  Crazycolorz5

  committed
  d6d8c17

• Disallow shadowing with type variables.

  Crazycolorz5

  committed
  ca727f2

• Add disallowing of shadowing for type variables.

  Crazycolorz5

  committed
  a140fa6

• Use . (as opposed to ->) to delineate forall/rec binding from body.

  Crazycolorz5

  committed
  256a8fc

• Make forall/rec bind tighter than sum to fix parsing bug.

  Crazycolorz5

  committed
  9c4403d

• Change display information to "type binding" instead of alias or variable.

  Crazycolorz5

  committed
  cb81911

• Make shadowing typfun use the same case as a hole in tvar name.

  Crazycolorz5

  committed
  4e4b1cf

• Add () around tuple output.

  Crazycolorz5

  committed
  3f95648

• Add Example scratchpad for polymorphism and recursive types.

  Crazycolorz5

  committed
  1fe28e2

• Correct minor error in is_tvar (should not affect anywhere where it's currently used)

  Crazycolorz5

  committed
  3923e39

• Preserve binding names from synthetic to give more intuitive cursor information.

  Crazycolorz5

  committed
  084f414

• Merge branch 'dev' into parameterized_types

  xzxzlala

  committed
  c60ce33

Commits on Aug 31, 2023

• Merge branch 'dev' into haz3l-module

  gensofubi

  committed
  d23540d

Commits on Sep 4, 2023

• Merge branch 'dev' into poly-adt-after2

  Crazycolorz5

  committed
  c456b82

Commits on Sep 10, 2023

• Fix: sort-inconsistent in mold/labels

  xzxzlala

  committed
  6ea7f14

• Merge branch 'dev' into haz3l-module

  gensofubi

  authored
  0c421f2

Commits on Sep 11, 2023

• Allow type names to be lowercase.

  Crazycolorz5

  committed
  6069676

Commits on Sep 12, 2023

• Improve clarity of type outputs by fixing some parentheses.

  Crazycolorz5

  committed
  b0298ed

• Add langdocs and examples for forall and rec.

  Crazycolorz5

  committed
  6f62655

Commits on Sep 14, 2023

• Add langdoc for typfun and typap. TODO more cases for typfun.

  Crazycolorz5

  committed
  55b4952

Commits on Sep 15, 2023

• Keep original variable name in alpha rename.

  Crazycolorz5

  committed
  3d85639

Commits on Sep 17, 2023

• Fix error in previous commit.

  Crazycolorz5

  committed
  709f6d0

• Return forall delimiter to -> from .

  Crazycolorz5

  committed
  663b719

• Fix error.

  Crazycolorz5

  committed
  f8da1dc

• Merge remote-tracking branch 'origin/dev' into haz3l-module

  gensofubi

  committed
  b41f68c

Commits on Sep 25, 2023

• Merge branch 'dev' into parameterized_types

  xzxzlala

  committed
  5aad869

• format error

  xzxzlala

  committed
  d197606

Commits on Sep 26, 2023

• Fix error in syntactix translation of types and address review comments.

  Crazycolorz5

  committed
  3f00366

Commits on Oct 3, 2023

• Exhaust case matching over using _ in Term

  Crazycolorz5

  committed
  21d28f7

• Remove unused code.

  Crazycolorz5

  committed
  7ab89b1

Commits on Oct 4, 2023

• Merge branch 'dev' into poly-adt-after2

  cyrus-

  authored
  cc463ff

Commits on Oct 14, 2023

• Merge branch 'dev' into haz3l-module

  gensofubi

  authored
  bf5b462

Commits on Nov 9, 2023

• fix double casting on dot accessing

  gensofubi

  committed
  d64aaed

Commits on Nov 27, 2023

• Merge remote-tracking branch 'origin/dev' into haz3l-module

  gensofubi

  committed
  e5b514a

Commits on Dec 4, 2023

• change ModuleVal type to ClosureEnvironment

  gensofubi

  committed
  024dabe

• fix modules annotated with typevars

  gensofubi

  committed
  4a084be

Commits on Dec 13, 2023

• Merge branch 'dev' into poly-adt-after2

  Crazycolorz5

  committed
  a2aa908

• Fix error with missing casts from inappropriate synthesis joining.

  Crazycolorz5

  committed
  714a54f

Commits on Dec 24, 2023

• Merge remote-tracking branch 'origin/dev' into haz3l-module

  gensofubi

  committed
  b92bc48

Commits on Jan 5, 2024

• regenerate Init.ml

  cyrus-

  committed
  010674d

Commits on Jan 8, 2024

• basic module alias

  gensofubi

  committed
  11e3b27

• fix curly bracket problem

  gensofubi

  committed
  4da0991

• fix dot parsing problem

  gensofubi

  committed
  82c8f61

• Merge branch 'haz3l-module' into module-alias

  gensofubi

  committed
  b371fbc

Commits on Feb 17, 2024

• evaluator merged

  gensofubi

  committed
  715b677

Commits on Feb 23, 2024

• merged without stepper for module

  gensofubi

  committed
  fe99078

• Merge branch 'dev' into haz3l-module

  gensofubi

  authored
  d0ad37c

Commits on Mar 1, 2024

• Module alias (#1156)

  cyrus-

  authored
  70688dc

• Merge remote-tracking branch 'origin/dev' into haz3l-module

  gensofubi

  committed
  ff1ad0b

Commits on Mar 2, 2024

• stepper partly done with a bug

  gensofubi

  committed
  baca0d2

• fix incorrect use of Mark

  gensofubi

  committed
  5684b0a

• fix nested module bug

  gensofubi

  committed
  3cd13bc

Commits on Mar 3, 2024

• Merge branch 'dev' into poly-adt-after2.

  Show description for ca00554
  Crazycolorz5

  committed
  ca00554

• Merge branch 'dev' into poly-adt-after2

  Crazycolorz5

  authored
  0bcaac9

Commits on Mar 4, 2024

• remove redundant evaluator for module

  gensofubi

  committed
  bb29147

• signature correction

  gensofubi

  committed
  78661a9

• cursor inspector message correction

  gensofubi

  committed
  6b57f29

• context inspector of projections updated

  gensofubi

  committed
  f7bdc10

Commits on Mar 7, 2024

• Merge branch 'poly-adt-after2' into parameterized_types

  xzxzlala

  committed
  e711929

• Fix and merge ploy-adt-after2

  xzxzlala

  committed
  233f55a

Commits on Mar 18, 2024

• fix documentation bugs

  gensofubi

  committed
  946242b

• Merge remote-tracking branch 'origin/dev' into haz3l-module

  gensofubi

  committed
  c4a746c

• Merge branch 'dev' into parameterized_types

  xzxzlala

  committed
  80a547e

• Merge branch 'haz3l-module' into module_implicts

  xzxzlala

  committed
  1d65d15

• Merge branch 'parameterized_types' into module_implicts

  xzxzlala

  committed
  212dbe9

• Remove: debug msg

  xzxzlala

  committed
  dc6d7cb