Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Module implicts #1241

Draft
wants to merge 153 commits into
base: dev
Choose a base branch
from
Draft
Changes from 1 commit
Commits
Show all changes
153 commits
Select commit Hold shift + click to select a range
1135c5c
copy module from let
gensofubi May 17, 2023
46cbc73
a try on module
gensofubi May 19, 2023
27c2d02
minor changes
gensofubi May 19, 2023
1c66f50
keyword module done
gensofubi May 19, 2023
e07aed2
formatted
gensofubi May 19, 2023
9845316
concrete module typing (but no typeann yet) and dot access operator
gensofubi May 21, 2023
29a4ffe
change the expected def pattern in module to Tag
gensofubi May 24, 2023
b261e45
change dot form to fit submodule
gensofubi May 24, 2023
2bb2e3f
detailed typing information for modules and auto hole-insert fixed
gensofubi May 31, 2023
e8ca644
type annotation for module
gensofubi Jun 1, 2023
4aba625
fit for module with 1 or 0 members
gensofubi Jun 2, 2023
85fa3bd
unsuccessful trial on fixing a bug
gensofubi Jun 7, 2023
3d26edd
partially solve
gensofubi Jun 7, 2023
e1563a6
adjust behavior when module typeann is not consistent with member typ…
gensofubi Jun 7, 2023
0a727c2
adjust the behavior when member names are not consistent with module …
gensofubi Jun 7, 2023
9c8d63e
Merge branch 'adt-defs-after' into haz3l-module
gensofubi Jun 10, 2023
403eac5
again change the expected def pattern in module to Tag
gensofubi Jun 11, 2023
3620771
basic type members
gensofubi Jun 14, 2023
e97369c
add comments
gensofubi Jun 15, 2023
3f7db25
basic type alias in module's annotation
gensofubi Jun 16, 2023
b1c3b6d
change precedence for sum type alias in module annotation
gensofubi Jun 17, 2023
9377765
fix for Tags in module
gensofubi Jun 17, 2023
fc8a9d5
in analitic mode, use constructors without prefix
gensofubi Jun 17, 2023
0a11c6f
differ module type member with type variable with same name
gensofubi Jun 18, 2023
9bb1796
fix minor problems
gensofubi Jun 18, 2023
0f11919
adjust typing information display for module type members
gensofubi Jun 18, 2023
45b8c80
Providing warnings for using type members that are not defined, and i…
gensofubi Jun 21, 2023
c9cbf2a
Merge remote-tracking branch 'origin/dev' into haz3l-module
gensofubi Jun 21, 2023
a6691dc
module langdoc copied from let
gensofubi Jun 28, 2023
09384db
module def langdoc
gensofubi Jun 29, 2023
477650a
Merge remote-tracking branch 'origin/adt-defs-after' into haz3l-module
gensofubi Jun 29, 2023
658e4f5
tyalias pat langdoc
gensofubi Jun 30, 2023
f097644
dot expression langdoc
gensofubi Jun 30, 2023
0f25baa
module type langdoc
gensofubi Jun 30, 2023
e247813
dot type langdoc
gensofubi Jul 1, 2023
449ac63
fit the problem on using member variable with member type
gensofubi Jul 2, 2023
a02f806
adjust type view: remove trailing comma, let the earlier definitions …
gensofubi Jul 2, 2023
9373f44
add tyalias for module having member type with same name
gensofubi Jul 2, 2023
d2034ba
change dot type to be a Typ postfix
gensofubi Jul 5, 2023
a57da2b
type view adjusted
gensofubi Jul 5, 2023
24f6748
Merge remote-tracking branch 'origin/adt-defs-after' into haz3l-module
gensofubi Jul 7, 2023
1513e98
fix exception when Applying Constructors defined in modules
gensofubi Jul 7, 2023
d8108d6
add comments in Statics.re and Module.re, remove unused function in C…
gensofubi Jul 10, 2023
14d5025
change error message for an invalid module name
gensofubi Jul 11, 2023
9285692
detailed member value in DHDoc_Exp
gensofubi Jul 12, 2023
c4c61b9
change dot to infix
gensofubi Jul 13, 2023
660d88b
Merge remote-tracking branch 'origin/adt-defs-after' into haz3l-module
gensofubi Jul 14, 2023
888ac62
rec type mem consistency
gensofubi Jul 14, 2023
1dc51e7
type member bug fix
gensofubi Jul 14, 2023
8aaa894
Merge remote-tracking branch 'origin/adt-defs-after' into haz3l-module
gensofubi Jul 31, 2023
483fc79
Merge remote-tracking branch 'origin/dev' into haz3l-module
gensofubi Aug 7, 2023
cc51001
change the cursor inspector print
gensofubi Aug 15, 2023
09aae62
langdoc modify
gensofubi Aug 15, 2023
4efc2e6
fix about ctrs in ana mode
gensofubi Aug 16, 2023
5f76744
change cls for capitalized var standing for modules
gensofubi Aug 16, 2023
abfe6db
langdoc for module vars(exp,pat,typ)
gensofubi Aug 17, 2023
2606648
Add: mold and forms of parameterized type
xzxzlala Aug 18, 2023
fe27614
Fix: the type in let works
xzxzlala Aug 21, 2023
e08f671
Fix: typeHole ann bug
xzxzlala Aug 22, 2023
13a0d20
Fix: castfailed bug
xzxzlala Aug 22, 2023
0bb43a6
merge in poly-adt
disconcision Feb 9, 2023
7e495cb
Fixed body_ctx of Forall and Rec in Statics
AlienKevin Feb 20, 2023
bc7e471
Allow Indet on the left of TypAp in Evaluator, similar to Ap
AlienKevin Feb 20, 2023
ceee07c
Fix mode of TypAp to Syn, not SynFun
AlienKevin Feb 20, 2023
8770d6e
Update is_fun and is_fun_var to recognize forall
AlienKevin Feb 20, 2023
031067e
Implement semantics of type function application as type substition o…
Crazycolorz5 May 1, 2023
d210f8f
Add synthesis mode for type function and add necessary casting cases.
Crazycolorz5 May 23, 2023
4d02ccb
Add rule for evaluation of type application on cast.
Crazycolorz5 May 23, 2023
b52560c
Some resolutions to conflicts from rebasing.
Crazycolorz5 Aug 25, 2023
7337f8f
Resolving issues in Statics and Elaborator.
Crazycolorz5 Aug 25, 2023
d78057e
Edit constructors in frontend.
Crazycolorz5 Aug 25, 2023
06cbf1d
Change dhexp substitution to use binding names rather than debrujin.
Crazycolorz5 Aug 25, 2023
749da41
Fix issue with looking up tvars in ctx.
Crazycolorz5 Aug 25, 2023
66870d3
Fix error in alpha equiv
Crazycolorz5 Aug 25, 2023
e63913d
Fix typechecking with mismatching type variable names.
Crazycolorz5 Aug 26, 2023
c3f44b4
Implement capture avoiding substitution.
Crazycolorz5 Aug 26, 2023
4ef0651
Add capture avoiding binding to recursive types.
Crazycolorz5 Aug 26, 2023
9d41608
Merge branch 'dev' into parameterized_types
xzxzlala Aug 26, 2023
c148a98
Merge remote-tracking branch 'origin/dev' into haz3l-module
gensofubi Aug 27, 2023
609997d
merge typFun and typAp
xzxzlala Aug 27, 2023
9ccf619
Add: parameterized-types, leave the case branch not working
xzxzlala Aug 27, 2023
93477bd
Add a comment to justify not needing capture avoidance in evaluator.
Crazycolorz5 Aug 28, 2023
57f725e
Revise info and evaluator pattern match to fix the case branch incons…
xzxzlala Aug 29, 2023
58e5cd7
Rmove debug print code
xzxzlala Aug 29, 2023
6442034
Fix: incorrect type of ctrs
xzxzlala Aug 29, 2023
3142ed3
Fix: typeann typehole cause case match failed
xzxzlala Aug 29, 2023
21e3365
Fix: ctr_ap type error
xzxzlala Aug 29, 2023
d6d8c17
Add parentheses to left type of functions when necessary. Lowercase f…
Crazycolorz5 Aug 30, 2023
ca727f2
Disallow shadowing with type variables.
Crazycolorz5 Aug 30, 2023
a140fa6
Add disallowing of shadowing for type variables.
Crazycolorz5 Aug 30, 2023
256a8fc
Use . (as opposed to ->) to delineate forall/rec binding from body.
Crazycolorz5 Aug 30, 2023
9c4403d
Make forall/rec bind tighter than sum to fix parsing bug.
Crazycolorz5 Aug 30, 2023
cb81911
Change display information to "type binding" instead of alias or vari…
Crazycolorz5 Aug 30, 2023
4e4b1cf
Make shadowing typfun use the same case as a hole in tvar name.
Crazycolorz5 Aug 30, 2023
3f95648
Add () around tuple output.
Crazycolorz5 Aug 30, 2023
1fe28e2
Add Example scratchpad for polymorphism and recursive types.
Crazycolorz5 Aug 30, 2023
3923e39
Correct minor error in is_tvar (should not affect anywhere where it's…
Crazycolorz5 Aug 30, 2023
084f414
Preserve binding names from synthetic to give more intuitive cursor i…
Crazycolorz5 Aug 30, 2023
c60ce33
Merge branch 'dev' into parameterized_types
xzxzlala Aug 30, 2023
d23540d
Merge branch 'dev' into haz3l-module
gensofubi Aug 31, 2023
c456b82
Merge branch 'dev' into poly-adt-after2
Crazycolorz5 Sep 4, 2023
6ea7f14
Fix: sort-inconsistent in mold/labels
xzxzlala Sep 10, 2023
0c421f2
Merge branch 'dev' into haz3l-module
gensofubi Sep 10, 2023
6069676
Allow type names to be lowercase.
Crazycolorz5 Sep 11, 2023
b0298ed
Improve clarity of type outputs by fixing some parentheses.
Crazycolorz5 Sep 12, 2023
6f62655
Add langdocs and examples for forall and rec.
Crazycolorz5 Sep 12, 2023
55b4952
Add langdoc for typfun and typap. TODO more cases for typfun.
Crazycolorz5 Sep 14, 2023
3d85639
Keep original variable name in alpha rename.
Crazycolorz5 Sep 15, 2023
709f6d0
Fix error in previous commit.
Crazycolorz5 Sep 17, 2023
663b719
Return forall delimiter to -> from .
Crazycolorz5 Sep 17, 2023
f8da1dc
Fix error.
Crazycolorz5 Sep 17, 2023
b41f68c
Merge remote-tracking branch 'origin/dev' into haz3l-module
gensofubi Sep 17, 2023
5aad869
Merge branch 'dev' into parameterized_types
xzxzlala Sep 25, 2023
d197606
format error
xzxzlala Sep 25, 2023
3f00366
Fix error in syntactix translation of types and address review comments.
Crazycolorz5 Sep 26, 2023
21d28f7
Exhaust case matching over using _ in Term
Crazycolorz5 Oct 3, 2023
7ab89b1
Remove unused code.
Crazycolorz5 Oct 3, 2023
cc463ff
Merge branch 'dev' into poly-adt-after2
cyrus- Oct 4, 2023
bf5b462
Merge branch 'dev' into haz3l-module
gensofubi Oct 14, 2023
d64aaed
fix double casting on dot accessing
gensofubi Nov 9, 2023
e5b514a
Merge remote-tracking branch 'origin/dev' into haz3l-module
gensofubi Nov 27, 2023
024dabe
change ModuleVal type to ClosureEnvironment
gensofubi Dec 4, 2023
4a084be
fix modules annotated with typevars
gensofubi Dec 4, 2023
a2aa908
Merge branch 'dev' into poly-adt-after2
Crazycolorz5 Dec 13, 2023
714a54f
Fix error with missing casts from inappropriate synthesis joining.
Crazycolorz5 Dec 13, 2023
b92bc48
Merge remote-tracking branch 'origin/dev' into haz3l-module
gensofubi Dec 24, 2023
010674d
regenerate Init.ml
cyrus- Jan 5, 2024
11e3b27
basic module alias
gensofubi Jan 8, 2024
4da0991
fix curly bracket problem
gensofubi Jan 8, 2024
82c8f61
fix dot parsing problem
gensofubi Jan 8, 2024
b371fbc
Merge branch 'haz3l-module' into module-alias
gensofubi Jan 8, 2024
715b677
evaluator merged
gensofubi Feb 17, 2024
fe99078
merged without stepper for module
gensofubi Feb 23, 2024
d0ad37c
Merge branch 'dev' into haz3l-module
gensofubi Feb 23, 2024
70688dc
Module alias (#1156)
cyrus- Mar 1, 2024
ff1ad0b
Merge remote-tracking branch 'origin/dev' into haz3l-module
gensofubi Mar 1, 2024
baca0d2
stepper partly done with a bug
gensofubi Mar 2, 2024
5684b0a
fix incorrect use of Mark
gensofubi Mar 2, 2024
3cd13bc
fix nested module bug
gensofubi Mar 2, 2024
ca00554
Merge branch 'dev' into poly-adt-after2.
Crazycolorz5 Mar 3, 2024
0bcaac9
Merge branch 'dev' into poly-adt-after2
Crazycolorz5 Mar 3, 2024
bb29147
remove redundant evaluator for module
gensofubi Mar 4, 2024
78661a9
signature correction
gensofubi Mar 4, 2024
6b57f29
cursor inspector message correction
gensofubi Mar 4, 2024
f7bdc10
context inspector of projections updated
gensofubi Mar 4, 2024
e711929
Merge branch 'poly-adt-after2' into parameterized_types
xzxzlala Mar 7, 2024
233f55a
Fix and merge ploy-adt-after2
xzxzlala Mar 7, 2024
946242b
fix documentation bugs
gensofubi Mar 18, 2024
c4a746c
Merge remote-tracking branch 'origin/dev' into haz3l-module
gensofubi Mar 18, 2024
80a547e
Merge branch 'dev' into parameterized_types
xzxzlala Mar 18, 2024
1d65d15
Merge branch 'haz3l-module' into module_implicts
xzxzlala Mar 18, 2024
212dbe9
Merge branch 'parameterized_types' into module_implicts
xzxzlala Mar 18, 2024
dc6d7cb
Remove: debug msg
xzxzlala Mar 18, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Fix: typeann typehole cause case match failed
xzxzlala committed Aug 29, 2023
commit 3142ed32af0876feb2a0ec45699b6f14f2477d07
4 changes: 0 additions & 4 deletions src/haz3lcore/dynamics/Evaluator.re
Original file line number Diff line number Diff line change
@@ -699,8 +699,6 @@ let rec evaluate: (ClosureEnvironment.t, DHExp.t) => m(EvaluatorResult.t) =
(env, d) => {
/* Increment number of evaluation steps (calls to `evaluate`). */
let* () = take_step;
//Printf.printf("env: %s\n", ClosureEnvironment.show(env));
//Printf.printf("d: %s\n", DHExp.show(d));
switch (d) {
| BoundVar(x) =>
let d =
@@ -751,9 +749,7 @@ let rec evaluate: (ClosureEnvironment.t, DHExp.t) => m(EvaluatorResult.t) =
| TypFun(_) => BoxedValue(Closure(env, d)) |> return

| TypAp(d1, tau) =>
//Printf.printf("TypAp, env: %s\n", ClosureEnvironment.show(env));
let* r1 = evaluate(env, d1);
//Printf.printf("r1: %s\n", EvaluatorResult.show(r1));
switch (r1) {
| BoxedValue(Closure(closure_env, TypFun({term: Var(name), _}, d2))) =>
// TODO: Maybe additional cases to be done?
1 change: 0 additions & 1 deletion src/haz3lcore/prog/Interface.re
Original file line number Diff line number Diff line change
@@ -56,7 +56,6 @@ let evaluate =
// };

let evaluate = (d: DHExp.t): ProgramResult.t => {
//Printf.printf("Evaluating: %s\n", DHExp.show(d));
let result =
try(evaluate(d)) {
| EvaluatorError.Exception(reason) =>
5 changes: 5 additions & 0 deletions src/haz3lcore/statics/TypBase.re
Original file line number Diff line number Diff line change
@@ -452,6 +452,11 @@ module rec Typ: {
Rec(name, normalize(Ctx.extend_dummy_tvar(ctx, name), ty))
| Forall(name, ty) =>
Forall(name, normalize(Ctx.extend_dummy_tvar(ctx, name), ty))
| Ap(Var(name), t2) =>
switch (Ctx.lookup_higher_kind(ctx, name)) {
| Some((arg, ty_out)) => normalize(ctx, subst(t2, arg, ty_out))
| None => Ap(Var(name), normalize(ctx, t2))
}
| Ap(t1, t2) => Ap(normalize(ctx, t1), normalize(ctx, t2))
};
};