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

[determinacy] big refactor #290

Draft
wants to merge 43 commits into
base: master
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
43 commits
Select commit Hold shift + click to select a range
8eb7038
[compiler+determinacy] no modes in AST + new check determinacy + uniq…
FissoreD Dec 16, 2024
a5e9000
remove dead code
FissoreD Nov 26, 2024
263d0d7
[determinacy] check output
FissoreD Nov 27, 2024
ca646dc
[determinacy] inference of parametric types like `pr (pred o:int) int…
FissoreD Nov 27, 2024
ae5ed1d
[dune] remove ppx_inline_test
FissoreD Nov 27, 2024
f98ae62
[spilling] spilling is done immediately after typechecking
FissoreD Nov 27, 2024
9f55359
[ScopedTerm.pretty] printing for infix symbols
FissoreD Nov 27, 2024
ba98f79
[determinacy] determine type of variable from typeassignment
FissoreD Dec 16, 2024
e5c7a06
[determinacy] type assignment to functionality check if Uvar is set
FissoreD Nov 27, 2024
366e2e6
[determinacy] move variable inference from infer to infer_outputs
FissoreD Nov 28, 2024
40c3cf3
[determinacy] update debug messages
FissoreD Nov 28, 2024
2cf31bd
[error_messages] make menhir-strip-errormsgs
FissoreD Nov 28, 2024
4740151
[spilling] add header to mli
FissoreD Nov 28, 2024
3902375
[determinacy] check symbol names (F.t) are global
FissoreD Nov 28, 2024
896c05e
[determinacy] again less print
FissoreD Nov 28, 2024
d096870
[determinacy] fold_left_partial and functionality_leq between Any and…
FissoreD Nov 28, 2024
426665e
[determinacy] varidic predicates and modes + all tests pass
FissoreD Nov 29, 2024
f3a972b
[determinacy] cmp + <<= + deduce functionality of unkown
FissoreD Nov 29, 2024
4314506
[union find] type assignment merge and union-find
FissoreD Dec 16, 2024
03ee23c
[union-find] version with persistent map instead of "persistent" Hashtbl
FissoreD Dec 16, 2024
c51aaf9
[type-checker] fix tyass when using cast
FissoreD Dec 4, 2024
64412f2
[type-assignment] add functional|relation on the prop constructor
FissoreD Dec 4, 2024
53a0e77
[union-find] rename Union_find in IdPosUF
FissoreD Dec 4, 2024
089e5f3
[compiler] modes refactor: typeAss's arrow has mode + remove pred fro…
FissoreD Dec 16, 2024
a3bde64
[type-checker] add test for mode inference of variable
FissoreD Dec 6, 2024
28f076b
wip
FissoreD Dec 10, 2024
1bc2d25
[compiler] remove unused type
FissoreD Dec 10, 2024
633a19c
[compiler] modes in SymbolMap + macro clone
FissoreD Dec 16, 2024
5d2ef89
[compiler] pp duplicate mode message
FissoreD Dec 12, 2024
86d017b
[compiler] clean code
FissoreD Dec 16, 2024
21aa782
minor fixes
gares Dec 13, 2024
5e9862e
[compiler_data] update pretty printer of type_assignment
FissoreD Dec 16, 2024
f13e98c
minor
FissoreD Dec 16, 2024
edcd2bd
clean code
FissoreD Dec 16, 2024
dfb001b
improve duplicate mode error message
gares Dec 16, 2024
95b5b07
we need to type check again
gares Dec 16, 2024
9ffb686
[compiler] start mode checking in type_checker
FissoreD Dec 16, 2024
cf08313
update mode signatures of tests
FissoreD Dec 16, 2024
8b54c7d
[type_checker] update test_typechecker.ml
FissoreD Dec 17, 2024
4bdb677
[compiler] pretty printer for types
FissoreD Dec 17, 2024
259241a
wip
FissoreD Dec 19, 2024
f9ffc4e
detach mode checker from type checker
FissoreD Dec 19, 2024
ccb0db7
comment
gares Dec 19, 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
1 change: 1 addition & 0 deletions src/API.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1353,6 +1353,7 @@ module Utils = struct
let map_acc = BuiltInData.map_acc

module type Show = Util.Show
module type ShowKey = Util.ShowKey
module type Show1 = Util.Show1
module Map = Util.Map
module Set = Util.Set
Expand Down
7 changes: 6 additions & 1 deletion src/API.mli
Original file line number Diff line number Diff line change
Expand Up @@ -859,7 +859,6 @@ module BuiltIn : sig

end


(* ************************************************************************* *)
(* ********************* Advanced Extension API **************************** *)
(* ************************************************************************* *)
Expand Down Expand Up @@ -1333,6 +1332,12 @@ module Utils : sig
val show : t -> string
end

module type ShowKey = sig
type key
val pp_key : Format.formatter -> key -> unit
val show_key : key -> string
end

module type Show1 = sig
type 'a t
val pp : (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> unit
Expand Down
6 changes: 3 additions & 3 deletions src/builtin.elpi
Original file line number Diff line number Diff line change
Expand Up @@ -359,7 +359,7 @@ external pred unix.process.close i:unix.process, o:diagnostic.
% -- Debugging --

% [term_to_string T S] prints T to S
external pred term_to_string i:any, o:string.
external pred term_to_string o:any, o:string.

% == Lambda Prolog builtins =====================================

Expand Down Expand Up @@ -693,11 +693,11 @@ map2-filter [] [] _ [].
map2-filter [X|XS] [Y|YS] F [Z|ZS] :- F X Y Z, !, map2-filter XS YS F ZS.
map2-filter [_|XS] [_|YS] F ZS :- map2-filter XS YS F ZS.

pred map-ok i:list A, i:(pred i:A, i:B, o:diagnostic), o:list B, o:diagnostic.
pred map-ok i:list A, i:(pred i:A, o:B, o:diagnostic), o:list B, o:diagnostic.
map-ok [X|L] P [Y|YS] S :- P X Y S0, if (S0 = ok) (map-ok L P YS S) (S = S0).
map-ok [] _ [] ok.

pred fold-map i:list A, i:B, i:(pred i:A, i:B, o:C, o:B), o:list C, o:B.
pred fold-map i:list A, i:B, i:(pred i:A, o:B, o:C, o:B), o:list C, o:B.
fold-map [] A _ [] A.
fold-map [X|XS] A F [Y|YS] A2 :- F X A Y A1, fold-map XS A1 F YS A2.

Expand Down
7 changes: 5 additions & 2 deletions src/builtin.ml
Original file line number Diff line number Diff line change
Expand Up @@ -596,15 +596,18 @@ This API only works reliably since OCaml 4.12.|}))))),
LPDoc " -- Debugging --";

MLCode(Pred("term_to_string",
In(any, "T",
InOut(ioarg_any, "T",
Out(string, "S",
Easy "prints T to S")),
(fun t _ ~depth ->
match t with
| NoData -> ?: None +! "_"
| Data t ->
let b = Buffer.create 1024 in
let fmt = Format.formatter_of_buffer b in
Format.fprintf fmt "%a" (RawPp.term depth) t ;
Format.pp_print_flush fmt ();
!:(Buffer.contents b))),
?: None +! (Buffer.contents b))),
DocAbove);

]
Expand Down
4 changes: 2 additions & 2 deletions src/builtin_stdlib.elpi
Original file line number Diff line number Diff line change
Expand Up @@ -159,11 +159,11 @@ map2-filter [] [] _ [].
map2-filter [X|XS] [Y|YS] F [Z|ZS] :- F X Y Z, !, map2-filter XS YS F ZS.
map2-filter [_|XS] [_|YS] F ZS :- map2-filter XS YS F ZS.

pred map-ok i:list A, i:(pred i:A, i:B, o:diagnostic), o:list B, o:diagnostic.
pred map-ok i:list A, i:(pred i:A, o:B, o:diagnostic), o:list B, o:diagnostic.
map-ok [X|L] P [Y|YS] S :- P X Y S0, if (S0 = ok) (map-ok L P YS S) (S = S0).
map-ok [] _ [] ok.

pred fold-map i:list A, i:B, i:(pred i:A, i:B, o:C, o:B), o:list C, o:B.
pred fold-map i:list A, i:B, i:(pred i:A, o:B, o:C, o:B), o:list C, o:B.
fold-map [] A _ [] A.
fold-map [X|XS] A F [Y|YS] A2 :- F X A Y A1, fold-map XS A1 F YS A2.

Expand Down
Loading
Loading