Skip to content

Experiment: unboxed ints in ltac2 runtime #13

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.

Sign up for GitHub

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

Closed
Janno wants to merge 1 commit into from
Closed

Experiment: unboxed ints in ltac2 runtime #13

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
15 changes: 9 additions & 6 deletions doc/plugin_tutorial/tuto4/src/myexternals.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -96,12 +96,15 @@ let of_custom = function
This needs to look at the low-level valexpr data.
If an external is declared with an incorrect Ltac2 type it may be passed
invalid values, in which case we assert false. *)
let to_custom = let open Tac2val in function
| ValInt 0 -> A
| ValBlk (0, [|c|]) ->
(* [to_constr] is [Tac2ffi.to_constr] *)
B (to_constr c)
| _ -> assert false
let to_custom v = let open Tac2val in
if is_int v then
let () = assert (unsafe_to_int v = 0) in
A
else match unsafe_to_fat v with
| ValBlk (0, [|c|]) ->
(* [to_constr] is [Tac2ffi.to_constr] *)
B (to_constr c)
| _ -> assert false


(* Now we package both translation functions into a Tac2ffi.repr
Expand Down
26 changes: 16 additions & 10 deletions plugins/ltac2/tac2core.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -108,13 +108,16 @@ open Core
let v_blk = Valexpr.make_block

let of_relevance = function
| Sorts.Relevant -> ValInt 0
| Sorts.Irrelevant -> ValInt 1
| Sorts.RelevanceVar q -> ValBlk (0, [|of_qvar q|])

let to_relevance = function
| ValInt 0 -> Sorts.Relevant
| ValInt 1 -> Sorts.Irrelevant
| Sorts.Relevant -> of_int 0
| Sorts.Irrelevant -> of_int 1
| Sorts.RelevanceVar q -> of_fat @@ ValBlk (0, [|of_qvar q|])

let to_relevance v =
if is_int v then match unsafe_to_int v with
| 0 -> Sorts.Relevant
| 1 -> Sorts.Irrelevant
| _ -> assert false
else match unsafe_to_fat v with
| ValBlk (0, [|qvar|]) ->
let qvar = to_qvar qvar in
Sorts.RelevanceVar qvar
Expand All @@ -136,12 +139,15 @@ let to_rec_declaration (nas, cs) =
Tac2ffi.to_array Tac2ffi.to_constr cs)

let of_case_invert = let open Constr in function
| NoInvert -> ValInt 0
| NoInvert -> of_int 0
| CaseInvert {indices} ->
v_blk 0 [|of_array of_constr indices|]

let to_case_invert = let open Constr in function
| ValInt 0 -> NoInvert
let to_case_invert v = let open Constr in
if is_int v then
let () = assert (unsafe_to_int v = 0) in
NoInvert
else match unsafe_to_fat v with
| ValBlk (0, [|indices|]) ->
let indices = to_array to_constr indices in
CaseInvert {indices}
Expand Down
4 changes: 2 additions & 2 deletions plugins/ltac2/tac2env.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -143,8 +143,8 @@ module MLMap = Map.Make(ML)
let primitive_map = ref MLMap.empty

let define_primitive name f =
let f = match f with
| ValCls f -> ValCls (annotate_closure (FrPrim name) f)
let f = if is_int f then f else match force_to_fat f with
| ValCls f -> of_fat @@ ValCls (annotate_closure (FrPrim name) f)
| _ -> f
in
primitive_map := MLMap.add name f !primitive_map
Expand Down
17 changes: 10 additions & 7 deletions plugins/ltac2/tac2extffi.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,13 +26,16 @@ let to_qhyp v = match Value.to_block v with

let qhyp = make_to_repr to_qhyp

let to_bindings = function
| ValInt 0 -> NoBindings
| ValBlk (0, [| vl |]) ->
ImplicitBindings (Value.to_list Value.to_constr vl)
| ValBlk (1, [| vl |]) ->
ExplicitBindings ((Value.to_list (fun p -> to_pair to_qhyp Value.to_constr p) vl))
| _ -> assert false
let to_bindings v =
if is_int v then
let () = assert (unsafe_to_int v = 0) in
NoBindings
else match unsafe_to_fat v with
| ValBlk (0, [| vl |]) ->
ImplicitBindings (Value.to_list Value.to_constr vl)
| ValBlk (1, [| vl |]) ->
ExplicitBindings ((Value.to_list (fun p -> to_pair to_qhyp Value.to_constr p) vl))
| _ -> assert false

let bindings = make_to_repr to_bindings

Expand Down
152 changes: 96 additions & 56 deletions plugins/ltac2/tac2ffi.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -78,51 +78,45 @@ let valexpr = {
r_to = (fun obj -> obj);
}

let of_unit () = ValInt 0
let of_unit () = of_int 0

let to_unit = function
| ValInt 0 -> ()
| _ -> assert false
let to_unit v = assert (force_to_int v = 0)

let unit = {
r_of = of_unit;
r_to = to_unit;
}

let of_int n = ValInt n
let to_int = function
| ValInt n -> n
| _ -> assert false
let of_int = of_int
let to_int = force_to_int

let int = {
r_of = of_int;
r_to = to_int;
}

let of_bool b = if b then ValInt 0 else ValInt 1
let of_bool b = if b then of_int 0 else of_int 1

let to_bool = function
| ValInt 0 -> true
| ValInt 1 -> false
let to_bool v = match force_to_int v with
| 0 -> true
| 1 -> false
| _ -> assert false

let bool = {
r_of = of_bool;
r_to = to_bool;
}

let of_char n = ValInt (Char.code n)
let to_char = function
| ValInt n -> Char.chr n
| _ -> assert false
let of_char n = of_int (Char.code n)
let to_char v = Char.chr @@ force_to_int v

let char = {
r_of = of_char;
r_to = to_char;
}

let of_bytes s = ValStr s
let to_bytes = function
let of_bytes s = of_fat @@ ValStr s
let to_bytes v = match force_to_fat v with
| ValStr s -> s
| _ -> assert false

Expand All @@ -139,20 +133,23 @@ let string = {
}

let rec of_list f = function
| [] -> ValInt 0
| x :: l -> ValBlk (0, [| f x; of_list f l |])
| [] -> of_int 0
| x :: l -> of_fat @@ ValBlk (0, [| f x; of_list f l |])

let rec to_list f = function
| ValInt 0 -> []
| ValBlk (0, [|v; vl|]) -> f v :: to_list f vl
| _ -> assert false
let rec to_list f v =
if is_int v then
let () = assert (unsafe_to_int v = 0) in
[]
else match unsafe_to_fat v with
| ValBlk (0, [|v; vl|]) -> f v :: to_list f vl
| _ -> assert false

let list r = {
r_of = (fun l -> of_list r.r_of l);
r_to = (fun l -> to_list r.r_to l);
}

let of_closure cls = ValCls cls
let of_closure cls = of_fat @@ ValCls cls

let to_closure = Tac2val.to_closure

Expand Down Expand Up @@ -196,9 +193,9 @@ let fun2 arg1 arg2 res = {
}

let of_ext tag c =
ValExt (tag, c)
of_fat @@ ValExt (tag, c)

let to_ext tag = function
let to_ext tag v = match force_to_fat v with
| ValExt (tag', e) -> extract_val tag tag' e
| _ -> assert false

Expand Down Expand Up @@ -247,6 +244,8 @@ let of_rewstrategy ev = of_ext val_rewstrategy ev
let to_rewstrategy ev = to_ext val_rewstrategy ev
let rewstrategy = repr_ext val_rewstrategy

let rocq_core n = Names.(KerName.make Tac2env.rocq_prefix (Label.of_id @@ Id.of_string_soft n))

let internal_err =
let open Names in
let rocq_prefix =
Expand All @@ -269,10 +268,10 @@ let err = repr_ext val_exn

(** FIXME: handle backtrace in Ltac2 exceptions *)
let of_exn c = match fst c with
| LtacError (kn, c) -> ValOpn (kn, c)
| _ -> ValOpn (internal_err, [|of_err c|])
| LtacError (kn, c) -> of_fat @@ ValOpn (kn, c)
| _ -> of_fat @@ ValOpn (internal_err, [|of_err c|])

let to_exn c = match c with
let to_exn c = match force_to_fat c with
| ValOpn (kn, c) ->
if Names.KerName.equal kn internal_err then
to_err c.(0)
Expand All @@ -286,10 +285,10 @@ let exn = {
}

let of_result of_ok = function
| Ok v -> ValBlk (0, [|of_ok v|])
| Error e -> ValBlk (1, [|of_exn e|])
| Ok v -> of_fat @@ ValBlk (0, [|of_ok v|])
| Error e -> of_fat @@ ValBlk (1, [|of_exn e|])

let to_result to_ok = function
let to_result to_ok v = match force_to_fat v with
| ValBlk (0, [|v|]) -> Ok (to_ok v)
| ValBlk (1, [|e|]) -> Error (to_exn e)
| _ -> assert false
Expand All @@ -300,13 +299,16 @@ let result ok = {
}

let of_option f = function
| None -> ValInt 0
| Some c -> ValBlk (0, [|f c|])
| None -> of_int 0
| Some c -> of_fat @@ ValBlk (0, [|f c|])

let to_option f = function
| ValInt 0 -> None
| ValBlk (0, [|c|]) -> Some (f c)
| _ -> assert false
let to_option f v =
if is_int v then
let () = assert (unsafe_to_int v = 0) in
None
else match unsafe_to_fat v with
| ValBlk (0, [|c|]) -> Some (f c)
| _ -> assert false

let option r = {
r_of = (fun l -> of_option r.r_of l);
Expand All @@ -317,40 +319,40 @@ let of_pp c = of_ext val_pp c
let to_pp c = to_ext val_pp c
let pp = repr_ext val_pp

let of_tuple cl = ValBlk (0, cl)
let to_tuple = function
let of_tuple cl = of_fat @@ ValBlk (0, cl)
let to_tuple v = match force_to_fat v with
| ValBlk (0, cl) -> cl
| _ -> assert false

let of_pair f g (x, y) = ValBlk (0, [|f x; g y|])
let to_pair f g = function
let of_pair f g (x, y) = of_fat @@ ValBlk (0, [|f x; g y|])
let to_pair f g v = match force_to_fat v with
| ValBlk (0, [|x; y|]) -> (f x, g y)
| _ -> assert false
let pair r0 r1 = {
r_of = (fun p -> of_pair r0.r_of r1.r_of p);
r_to = (fun p -> to_pair r0.r_to r1.r_to p);
}

let of_triple f g h (x, y, z) = ValBlk (0, [|f x; g y; h z|])
let to_triple f g h = function
let of_triple f g h (x, y, z) = of_fat @@ ValBlk (0, [|f x; g y; h z|])
let to_triple f g h v = match force_to_fat v with
| ValBlk (0, [|x; y; z|]) -> (f x, g y, h z)
| _ -> assert false
let triple r0 r1 r2 = {
r_of = (fun p -> of_triple r0.r_of r1.r_of r2.r_of p);
r_to = (fun p -> to_triple r0.r_to r1.r_to r2.r_to p);
}

let of_array f vl = ValBlk (0, Array.map f vl)
let to_array f = function
let of_array f vl = of_fat @@ ValBlk (0, Array.map f vl)
let to_array f v = match force_to_fat v with
| ValBlk (0, vl) -> Array.map f vl
| _ -> assert false
let array r = {
r_of = (fun l -> of_array r.r_of l);
r_to = (fun l -> to_array r.r_to l);
}

let of_block (n, args) = ValBlk (n, args)
let to_block = function
let of_block (n, args) = of_fat @@ ValBlk (n, args)
let to_block v = match force_to_fat v with
| ValBlk (n, args) -> (n, args)
| _ -> assert false

Expand All @@ -359,9 +361,9 @@ let block = {
r_to = to_block;
}

let of_open (kn, args) = ValOpn (kn, args)
let of_open (kn, args) = of_fat @@ ValOpn (kn, args)

let to_open = function
let to_open v = match force_to_fat v with
| ValOpn (kn, args) -> (kn, args)
| _ -> assert false

Expand Down Expand Up @@ -451,12 +453,12 @@ let to_instance c = to_ext val_instance c
let instance = repr_ext val_instance

let of_reference = let open Names.GlobRef in function
| VarRef id -> ValBlk (0, [| of_ident id |])
| ConstRef cst -> ValBlk (1, [| of_constant cst |])
| IndRef ind -> ValBlk (2, [| of_inductive ind |])
| ConstructRef cstr -> ValBlk (3, [| of_constructor cstr |])
| VarRef id -> of_fat @@ ValBlk (0, [| of_ident id |])
| ConstRef cst -> of_fat @@ ValBlk (1, [| of_constant cst |])
| IndRef ind -> of_fat @@ ValBlk (2, [| of_inductive ind |])
| ConstructRef cstr -> of_fat @@ ValBlk (3, [| of_constructor cstr |])

let to_reference = let open Names.GlobRef in function
let to_reference v = let open Names.GlobRef in match force_to_fat v with
| ValBlk (0, [| id |]) -> VarRef (to_ident id)
| ValBlk (1, [| cst |]) -> ConstRef (to_constant cst)
| ValBlk (2, [| ind |]) -> IndRef (to_inductive ind)
Expand All @@ -467,3 +469,41 @@ let reference = {
r_of = of_reference;
r_to = to_reference;
}

let of_strategy_level = let open Conv_oracle in function
| Expand -> of_int 0
| Opaque -> of_int 1
| Level n -> of_fat @@ ValBlk (0, [| of_int n |])

let to_strategy_level v = let open Conv_oracle in
if is_int v then
match unsafe_to_int v with
| 0 -> Expand
| 1 -> Opaque
| _ -> assert false
else match unsafe_to_fat v with
| ValBlk (0, [| n |]) -> Level (to_int n)
| _ -> assert false

let strategy_level = {
r_of = of_strategy_level;
r_to = to_strategy_level;
}

let err_notfocussed =
LtacError (rocq_core "Not_focussed", [||])

let err_outofbounds =
LtacError (rocq_core "Out_of_bounds", [||])

let err_notfound =
LtacError (rocq_core "Not_found", [||])

let err_matchfailure =
LtacError (rocq_core "Match_failure", [||])

let err_division_by_zero =
LtacError (rocq_core "Division_by_zero", [||])

let err_invalid_arg msg =
LtacError (rocq_core "Invalid_argument", [|of_option of_pp (Some msg)|])
Loading