Skip to content

Commit 141b6fe

Browse files
garesgares
authored
Merge pull request #353 from LPCIC/release
Release
2 parents aefda5d + 7dfac31 commit 141b6fe

File tree

9 files changed

+67
-51
lines changed

9 files changed

+67
-51
lines changed

‎CHANGES.md‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
# v3.1.0 UNRELEASED
1+
# v3.1.0 (August 2025)
22

33
Requires Menhir 20211230 and OCaml 4.13 or above.
44

@@ -13,7 +13,6 @@ Requires Menhir 20211230 and OCaml 4.13 or above.
1313
f N D Q R :- f N D Q, R is N mod D.
1414
```
1515
16-
1716
# v3.0.1 (July 2025)
1817
1918
Requires Menhir 20211230 and OCaml 4.13 or above.

‎src/builtin.elpi‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -435,7 +435,7 @@ rex_split Rx S L :- rex.split Rx S L.
435435

436436
% [var V ...] checks if the term V is a variable. When used with tree
437437
% arguments it relates an applied variable with its head and argument list.
438-
external type var any -> variadic any fprop.
438+
external func var -> any, any.. .
439439

440440

441441
% [prune V L] V is pruned to L (V is unified with a variable that only sees
@@ -468,11 +468,11 @@ external func cmp_term any, any -> cmp.
468468

469469
% [name T ...] checks if T is a eigenvariable. When used with tree arguments
470470
% it relates an applied name with its head and argument list.
471-
external type name any -> variadic any fprop.
471+
external func name -> any, any.. .
472472

473473
% [constant T ...] checks if T is a (global) constant. When used with tree
474474
% arguments it relates an applied constant with its head and argument list.
475-
external type constant any -> variadic any fprop.
475+
external func constant -> any, any.. .
476476

477477
external func names % generates the list of eigenvariable
478478
-> list any. % list of eigenvariables in order of age (young first)

‎src/compiler/spilling.ml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -160,8 +160,8 @@ let rec bc ctx t =
160160

161161
and bc_loc ctx { loc; ty; it } = { loc; ty; it = bc ctx it }
162162

163-
let not_from_pi (_,b) = b = false
164-
let from_pi (_,b) = b = true
163+
(* let not_from_pi (_,b) = b = false *)
164+
(* let from_pi (_,b) = b = true *)
165165

166166
let rec apply what v = function
167167
| App ({ scope = Bound l; name = f; ty = hd_ty } as n, xs) when l = elpi_language && List.exists (fun f' -> F.equal f f'.name) what ->

‎src/compiler/test_compiler_data.ml‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -42,9 +42,9 @@ open ScopedTerm
4242
let loc = Ast.Loc.initial "x"
4343
let ty = TypeAssignment.create (Prop Relation)
4444
let c3 = { loc; it = CData (Ast.cint.cin 3); ty };;
45-
let lam v t = { loc; ty; it = Lam(Some(ScopedTerm.mk_const "" (F.from_string v) loc),None,t)}
46-
let var v = { loc; ty; it = App(ScopedTerm.mk_const (Scope.Bound "") (F.from_string v) loc,[])}
47-
let app c l = { loc; ty; it = App(ScopedTerm.mk_const (Scope.mkGlobal ~escape_ns:true ()) (F.from_string c) loc,l)}
45+
let lam v t = { loc; ty; it = Lam(Some(ScopedTerm.mk_const ~scope:"" (F.from_string v) ~loc),None,t)}
46+
let var v = { loc; ty; it = App(ScopedTerm.mk_const ~scope:(Scope.Bound "") (F.from_string v) ~loc,[])}
47+
let app c l = { loc; ty; it = App(ScopedTerm.mk_const ~scope:(Scope.mkGlobal ~escape_ns:true ()) (F.from_string c) ~loc,l)}
4848

4949
let () = pp_t c3 "3";;
5050
let () = pp_t (app "f" [app "g" [var "x"]]) "f (g x)";;

‎src/compiler/test_type_checker.ml‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -9,15 +9,15 @@ module TA = TypeAssignment
99
let fs = F.from_string
1010
let dummy_loc = Loc.initial ""
1111
let dummy_str = F.dummyname
12-
let mk_global name = ScopedTerm.mk_const (Scope.mkGlobal ()) (fs name) dummy_loc
13-
let mk_bound name = ScopedTerm.mk_const (Scope.Bound elpi_language) (fs name) dummy_loc
14-
let mk_local name = ScopedTerm.mk_const elpi_language (fs name) dummy_loc
12+
let mk_global name = ScopedTerm.mk_const ~scope:(Scope.mkGlobal ()) (fs name) ~loc:dummy_loc
13+
let mk_bound name = ScopedTerm.mk_const ~scope:(Scope.Bound elpi_language) (fs name) ~loc:dummy_loc
14+
let mk_local name = ScopedTerm.mk_const ~scope:elpi_language (fs name) ~loc:dummy_loc
1515
let build_loc it = ST.{ loc = dummy_loc; ty = MutableOnce.make dummy_str; it }
1616
let app n ag ags = build_loc @@ ST.App (mk_global n, ag :: ags)
1717
let lam n bo = build_loc @@ ST.Lam (Some (mk_local n), None, bo)
1818
let const n = build_loc @@ ST.App (mk_global n,[])
1919
let local_const n = build_loc @@ ST.App (mk_bound n,[])
20-
let var n = build_loc @@ ST.Var (ST.mk_bound_const elpi_var (fs n) dummy_loc, [])
20+
let var n = build_loc @@ ST.Var (ST.mk_bound_const ~lang:elpi_var (fs n) ~loc:dummy_loc, [])
2121
let build_ta a = TA.Val a
2222
let rprop = TA.Prop Relation
2323
let bool = TA.Cons (fs "bool")

‎src/compiler/type_checker.ml‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -198,8 +198,8 @@ let error ~loc msg = error ~loc ("Typechecker: " ^ msg)
198198

199199
let error_not_a_function ~loc c tyc args x =
200200
let t =
201-
if args = [] then ScopedTerm.App(mk_const (Scope.mkGlobal ~escape_ns:true ()) c loc,[])
202-
else ScopedTerm.(App(mk_const (Scope.mkGlobal ~escape_ns:true ()) c loc,args)) in
201+
if args = [] then ScopedTerm.App(mk_const ~scope:(Scope.mkGlobal ~escape_ns:true ()) c ~loc,[])
202+
else ScopedTerm.(App(mk_const ~scope:(Scope.mkGlobal ~escape_ns:true ()) c ~loc,args)) in
203203
let msg = Format.asprintf "@[<hov>%a is not a function but it is passed the argument@ @[<hov>%a@].@ The type of %a is %a@]"
204204
ScopedTerm.pretty_ t ScopedTerm.pretty x F.pp c TypeAssignment.pretty_mut_once tyc in
205205
error ~loc msg
@@ -442,7 +442,7 @@ let checker ~type_abbrevs ~kinds ~types:env ~unknown :
442442
else error_bad_cdata_ety ~tyctx ~loc c ty ~ety
443443

444444
and check_lam ~positive ctx ~loc ~tyctx sc c_type_cast t ety =
445-
let { scope = name_lang; name = c; ty = c_type } = match sc with Some c -> c | None -> mk_const elpi_language (fresh_name ()) loc in
445+
let { scope = name_lang; name = c; ty = c_type } = match sc with Some c -> c | None -> mk_const ~scope:elpi_language (fresh_name ()) ~loc in
446446
let src = match c_type_cast with
447447
| None -> mk_uvar "Src"
448448
| Some x -> TypeAssignment.subst (fun f -> Some (UVar(MutableOnce.make f))) @@ check_loc_tye ~positive:true ~type_abbrevs ~kinds F.Set.empty x
@@ -509,7 +509,7 @@ let checker ~type_abbrevs ~kinds ~types:env ~unknown :
509509
(* Format.eprintf "%a: 1 option: %a@." F.pp c TypeAssignment.pretty_mut_once_raw ty; *)
510510
let err ty =
511511
if args = [] then error_bad_ety ~valid_mode ~loc ~tyctx ~ety F.pp c ty (* uvar *)
512-
else error_bad_ety ~valid_mode ~loc ~tyctx ~ety ScopedTerm.pretty_ (App(mk_const (Scope.mkGlobal ~escape_ns:true ()(* sucks *)) c loc,args)) ty in
512+
else error_bad_ety ~valid_mode ~loc ~tyctx ~ety ScopedTerm.pretty_ (App(mk_const ~scope:(Scope.mkGlobal ~escape_ns:true ()(* sucks *)) c ~loc,args)) ty in
513513
let monodirectional () =
514514
(* Format.eprintf "checking app mono %a\n" F.pp c; *)
515515
let tgt = check_app_single ~positive ctx ~loc (cid,c,tya) ty [] args in

‎src/runtime/data.ml‎

Lines changed: 19 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1638,6 +1638,23 @@ let pp_variadictype fmt name doc_pred ty args =
16381638
pp_comment doc name pp_ty_args args
16391639
;;
16401640
1641+
let pp_variadicpred fmt docspec name doc_pred ty args =
1642+
let rargs = List.rev ((false, ty ^ ".. ","...") :: args) in
1643+
if is_std_moded rargs then
1644+
match docspec with
1645+
| DocNext ->
1646+
Fmt.fprintf fmt "@[<v 2>external func %s %% %s@;%a@]@."
1647+
name doc_pred pp_tab_args rargs
1648+
| DocAbove ->
1649+
let doc =
1650+
"[" ^ String.concat " " (name :: List.map (fun (_,_,x) -> x) rargs) ^
1651+
"] " ^ doc_pred in
1652+
Fmt.fprintf fmt "@[<v>%% %[email protected] func %s@[<hov>%a.@]@]@.@."
1653+
pp_comment doc name pp_args rargs
1654+
else
1655+
pp_variadictype fmt name doc_pred ty args
1656+
;;
1657+
16411658
let document_pred fmt docspec name ffi =
16421659
let rec doc
16431660
: type i o h c. (bool * string * string) list -> (i,o,h,c) ffi -> unit
@@ -1653,8 +1670,8 @@ let document_pred fmt docspec name ffi =
16531670
| Full (_,s) -> pp_pred fmt docspec name s args
16541671
| FullHO (_,s) -> pp_pred fmt docspec name s args
16551672
| VariadicIn( _,{ ContextualConversion.ty }, s) -> pp_variadictype fmt name s (Conversion.show_ty_ast ty) args
1656-
| VariadicOut( _,{ ContextualConversion.ty }, s) -> pp_variadictype fmt name s (Conversion.show_ty_ast ty) args
1657-
| VariadicInOut( _,{ ContextualConversion.ty }, s) -> pp_variadictype fmt name s (Conversion.show_ty_ast ty) args
1673+
| VariadicOut( _,{ ContextualConversion.ty }, s) -> pp_variadicpred fmt docspec name s (Conversion.show_ty_ast ty) args
1674+
| VariadicInOut( _,{ ContextualConversion.ty }, s) -> pp_variadicpred fmt docspec name s (Conversion.show_ty_ast ty) args
16581675
in
16591676
doc [] ffi
16601677
;;

‎tests/sources/trace_w.elab.json‎

Lines changed: 20 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -2431,7 +2431,7 @@
24312431
"filename": "builtin.elpi",
24322432
"line": 526,
24332433
"column": 0,
2434-
"character": 13695
2434+
"character": 13662
24352435
}
24362436
]
24372437
}
@@ -2468,7 +2468,7 @@
24682468
"filename": "builtin.elpi",
24692469
"line": 526,
24702470
"column": 0,
2471-
"character": 13695
2471+
"character": 13662
24722472
}
24732473
]
24742474
}
@@ -2631,7 +2631,7 @@
26312631
"filename": "builtin.elpi",
26322632
"line": 526,
26332633
"column": 0,
2634-
"character": 13695
2634+
"character": 13662
26352635
}
26362636
]
26372637
}
@@ -2763,7 +2763,7 @@
27632763
"filename": "builtin.elpi",
27642764
"line": 526,
27652765
"column": 0,
2766-
"character": 13695
2766+
"character": 13662
27672767
}
27682768
]
27692769
}
@@ -2875,7 +2875,7 @@
28752875
"filename": "builtin.elpi",
28762876
"line": 527,
28772877
"column": 0,
2878-
"character": 13716
2878+
"character": 13683
28792879
}
28802880
]
28812881
}
@@ -2908,7 +2908,7 @@
29082908
"filename": "builtin.elpi",
29092909
"line": 527,
29102910
"column": 0,
2911-
"character": 13716
2911+
"character": 13683
29122912
}
29132913
]
29142914
}
@@ -3037,7 +3037,7 @@
30373037
"filename": "builtin.elpi",
30383038
"line": 527,
30393039
"column": 0,
3040-
"character": 13716
3040+
"character": 13683
30413041
}
30423042
]
30433043
}
@@ -3275,7 +3275,7 @@
32753275
"filename": "builtin.elpi",
32763276
"line": 526,
32773277
"column": 0,
3278-
"character": 13695
3278+
"character": 13662
32793279
}
32803280
]
32813281
}
@@ -3317,7 +3317,7 @@
33173317
"filename": "builtin.elpi",
33183318
"line": 526,
33193319
"column": 0,
3320-
"character": 13695
3320+
"character": 13662
33213321
}
33223322
]
33233323
}
@@ -3480,7 +3480,7 @@
34803480
"filename": "builtin.elpi",
34813481
"line": 526,
34823482
"column": 0,
3483-
"character": 13695
3483+
"character": 13662
34843484
}
34853485
]
34863486
}
@@ -3657,7 +3657,7 @@
36573657
"filename": "builtin.elpi",
36583658
"line": 526,
36593659
"column": 0,
3660-
"character": 13695
3660+
"character": 13662
36613661
}
36623662
]
36633663
}
@@ -3798,7 +3798,7 @@
37983798
"filename": "builtin.elpi",
37993799
"line": 527,
38003800
"column": 0,
3801-
"character": 13716
3801+
"character": 13683
38023802
}
38033803
]
38043804
}
@@ -3848,7 +3848,7 @@
38483848
"filename": "builtin.elpi",
38493849
"line": 526,
38503850
"column": 0,
3851-
"character": 13695
3851+
"character": 13662
38523852
}
38533853
]
38543854
}
@@ -4791,7 +4791,7 @@
47914791
"filename": "builtin.elpi",
47924792
"line": 526,
47934793
"column": 0,
4794-
"character": 13695
4794+
"character": 13662
47954795
}
47964796
]
47974797
}
@@ -4828,7 +4828,7 @@
48284828
"filename": "builtin.elpi",
48294829
"line": 526,
48304830
"column": 0,
4831-
"character": 13695
4831+
"character": 13662
48324832
}
48334833
]
48344834
}
@@ -4953,7 +4953,7 @@
49534953
"filename": "builtin.elpi",
49544954
"line": 526,
49554955
"column": 0,
4956-
"character": 13695
4956+
"character": 13662
49574957
}
49584958
]
49594959
}
@@ -5047,7 +5047,7 @@
50475047
"filename": "builtin.elpi",
50485048
"line": 526,
50495049
"column": 0,
5050-
"character": 13695
5050+
"character": 13662
50515051
}
50525052
]
50535053
}
@@ -5121,7 +5121,7 @@
51215121
"filename": "builtin.elpi",
51225122
"line": 527,
51235123
"column": 0,
5124-
"character": 13716
5124+
"character": 13683
51255125
}
51265126
]
51275127
}
@@ -5147,7 +5147,7 @@
51475147
"filename": "builtin.elpi",
51485148
"line": 527,
51495149
"column": 0,
5150-
"character": 13716
5150+
"character": 13683
51515151
}
51525152
]
51535153
}
@@ -5236,7 +5236,7 @@
52365236
"filename": "builtin.elpi",
52375237
"line": 527,
52385238
"column": 0,
5239-
"character": 13716
5239+
"character": 13683
52405240
}
52415241
]
52425242
}

0 commit comments

Comments
 (0)