aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--test-suite/ltac2/constr.v4
-rw-r--r--user-contrib/Ltac2/Constr.v19
-rw-r--r--user-contrib/Ltac2/tac2core.ml73
-rw-r--r--user-contrib/Ltac2/tac2ffi.mli2
4 files changed, 42 insertions, 56 deletions
diff --git a/test-suite/ltac2/constr.v b/test-suite/ltac2/constr.v
index 39601d99a8..018596ed95 100644
--- a/test-suite/ltac2/constr.v
+++ b/test-suite/ltac2/constr.v
@@ -2,11 +2,11 @@ Require Import Ltac2.Constr Ltac2.Init Ltac2.Control.
Import Unsafe.
Ltac2 Eval match (kind '(nat -> bool)) with
- | Prod a b c => a
+ | Prod a c => a
| _ => throw Match_failure end.
Set Allow StrictProp.
Axiom something : SProp.
Ltac2 Eval match (kind '(forall x : something, bool)) with
- | Prod a b c => a
+ | Prod a c => a
| _ => throw Match_failure end.
diff --git a/user-contrib/Ltac2/Constr.v b/user-contrib/Ltac2/Constr.v
index e778a8d677..94d468e640 100644
--- a/user-contrib/Ltac2/Constr.v
+++ b/user-contrib/Ltac2/Constr.v
@@ -29,16 +29,16 @@ Ltac2 Type kind := [
| Evar (evar, constr array)
| Sort (sort)
| Cast (constr, cast, constr)
-| Prod (binder, constr, constr)
-| Lambda (binder, constr, constr)
-| LetIn (binder, constr, constr, constr)
+| Prod (binder, constr)
+| Lambda (binder, constr)
+| LetIn (binder, constr, constr)
| App (constr, constr array)
| Constant (constant, instance)
| Ind (inductive, instance)
| Constructor (constructor, instance)
| Case (case, constr, constr, constr array)
-| Fix (int array, int, binder array, constr array, constr array)
-| CoFix (int, binder array, constr array, constr array)
+| Fix (int array, int, binder array, constr array)
+| CoFix (int, binder array, constr array)
| Proj (projection, constr)
| Uint63 (uint63)
| Float (float)
@@ -72,13 +72,14 @@ End Unsafe.
Module Binder.
-Ltac2 Type relevance := [ Relevant | Irrelevant ].
-
-Ltac2 @ external make : ident option -> relevance -> binder := "ltac2" "constr_binder_make".
+Ltac2 @ external make : ident option -> constr -> binder := "ltac2" "constr_binder_make".
+(** Create a binder given the name and the type of the bound variable. *)
Ltac2 @ external name : binder -> ident option := "ltac2" "constr_binder_name".
+(** Retrieve the name of a binder. *)
-Ltac2 @ external relevance : binder -> relevance := "ltac2" "constr_binder_relevance".
+Ltac2 @ external type : binder -> constr := "ltac2" "constr_binder_type".
+(** Retrieve the type of a binder. *)
End Binder.
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index c6abbf11b1..38b05bed6b 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -82,17 +82,6 @@ open Core
let v_unit = Value.of_unit ()
let v_blk = Valexpr.make_block
-let of_relevance = function
- | Sorts.Relevant -> ValInt 0
- | Sorts.Irrelevant -> ValInt 1
-
-let to_relevance = function
- | ValInt 0 -> Sorts.Relevant
- | ValInt 1 -> Sorts.Irrelevant
- | _ -> assert false
-
-let relevance = make_repr of_relevance to_relevance
-
let of_binder b =
Value.of_ext Value.val_binder b
@@ -108,13 +97,14 @@ let to_instance u =
EConstr.EInstance.make (Univ.Instance.of_array u)
let of_rec_declaration (nas, ts, cs) =
- (Value.of_array of_binder nas,
- Value.of_array Value.of_constr ts,
+ let binders = Array.map2 (fun na t -> (na, t)) nas ts in
+ (Value.of_array of_binder binders,
Value.of_array Value.of_constr cs)
-let to_rec_declaration (nas, ts, cs) =
- (Value.to_array to_binder nas,
- Value.to_array Value.to_constr ts,
+let to_rec_declaration (nas, cs) =
+ let nas = Value.to_array to_binder nas in
+ (Array.map fst nas,
+ Array.map snd nas,
Value.to_array Value.to_constr cs)
let of_result f = function
@@ -397,21 +387,18 @@ let () = define1 "constr_kind" constr begin fun c ->
|]
| Prod (na, t, u) ->
v_blk 6 [|
- of_binder na;
- Value.of_constr t;
+ of_binder (na, t);
Value.of_constr u;
|]
| Lambda (na, t, c) ->
v_blk 7 [|
- of_binder na;
- Value.of_constr t;
+ of_binder (na, t);
Value.of_constr c;
|]
| LetIn (na, b, t, c) ->
v_blk 8 [|
- of_binder na;
+ of_binder (na, t);
Value.of_constr b;
- Value.of_constr t;
Value.of_constr c;
|]
| App (c, cl) ->
@@ -442,20 +429,18 @@ let () = define1 "constr_kind" constr begin fun c ->
Value.of_array Value.of_constr bl;
|]
| Fix ((recs, i), def) ->
- let (nas, ts, cs) = of_rec_declaration def in
+ let (nas, cs) = of_rec_declaration def in
v_blk 14 [|
Value.of_array Value.of_int recs;
Value.of_int i;
nas;
- ts;
cs;
|]
| CoFix (i, def) ->
- let (nas, ts, cs) = of_rec_declaration def in
+ let (nas, cs) = of_rec_declaration def in
v_blk 15 [|
Value.of_int i;
nas;
- ts;
cs;
|]
| Proj (p, c) ->
@@ -493,20 +478,17 @@ let () = define1 "constr_make" valexpr begin fun knd ->
let k = Value.to_ext Value.val_cast k in
let t = Value.to_constr t in
EConstr.mkCast (c, k, t)
- | (6, [|na; t; u|]) ->
- let na = to_binder na in
- let t = Value.to_constr t in
+ | (6, [|na; u|]) ->
+ let (na, t) = to_binder na in
let u = Value.to_constr u in
EConstr.mkProd (na, t, u)
- | (7, [|na; t; c|]) ->
- let na = to_binder na in
- let t = Value.to_constr t in
+ | (7, [|na; c|]) ->
+ let (na, t) = to_binder na in
let u = Value.to_constr c in
EConstr.mkLambda (na, t, u)
- | (8, [|na; b; t; c|]) ->
- let na = to_binder na in
+ | (8, [|na; b; c|]) ->
+ let (na, t) = to_binder na in
let b = Value.to_constr b in
- let t = Value.to_constr t in
let c = Value.to_constr c in
EConstr.mkLetIn (na, b, t, c)
| (9, [|c; cl|]) ->
@@ -531,14 +513,14 @@ let () = define1 "constr_make" valexpr begin fun knd ->
let t = Value.to_constr t in
let bl = Value.to_array Value.to_constr bl in
EConstr.mkCase (ci, c, t, bl)
- | (14, [|recs; i; nas; ts; cs|]) ->
+ | (14, [|recs; i; nas; cs|]) ->
let recs = Value.to_array Value.to_int recs in
let i = Value.to_int i in
- let def = to_rec_declaration (nas, ts, cs) in
+ let def = to_rec_declaration (nas, cs) in
EConstr.mkFix ((recs, i), def)
- | (15, [|i; nas; ts; cs|]) ->
+ | (15, [|i; nas; cs|]) ->
let i = Value.to_int i in
- let def = to_rec_declaration (nas, ts, cs) in
+ let def = to_rec_declaration (nas, cs) in
EConstr.mkCoFix (i, def)
| (16, [|p; c|]) ->
let p = Value.to_ext Value.val_projection p in
@@ -653,18 +635,21 @@ let () = define1 "constr_pretype" (repr_ext val_preterm) begin fun c ->
pf_apply pretype
end
-let () = define2 "constr_binder_make" (option ident) relevance begin fun na rel ->
+let () = define2 "constr_binder_make" (option ident) constr begin fun na ty ->
+ pf_apply begin fun env sigma ->
+ let rel = Retyping.relevance_of_type env sigma ty in
let na = match na with None -> Anonymous | Some id -> Name id in
- return (Value.of_ext val_binder (Context.make_annot na rel))
+ return (Value.of_ext val_binder (Context.make_annot na rel, ty))
+ end
end
-let () = define1 "constr_binder_name" (repr_ext val_binder) begin fun bnd ->
+let () = define1 "constr_binder_name" (repr_ext val_binder) begin fun (bnd, _) ->
let na = match bnd.Context.binder_name with Anonymous -> None | Name id -> Some id in
return (Value.of_option Value.of_ident na)
end
-let () = define1 "constr_binder_relevance" (repr_ext val_binder) begin fun bnd ->
- return (of_relevance bnd.Context.binder_relevance)
+let () = define1 "constr_binder_type" (repr_ext val_binder) begin fun (bnd, ty) ->
+ return (of_constr ty)
end
(** Patterns *)
diff --git a/user-contrib/Ltac2/tac2ffi.mli b/user-contrib/Ltac2/tac2ffi.mli
index 5138133360..c9aa50389e 100644
--- a/user-contrib/Ltac2/tac2ffi.mli
+++ b/user-contrib/Ltac2/tac2ffi.mli
@@ -180,7 +180,7 @@ val val_constant : Constant.t Val.tag
val val_constructor : constructor Val.tag
val val_projection : Projection.t Val.tag
val val_case : Constr.case_info Val.tag
-val val_binder : Name.t Context.binder_annot Val.tag
+val val_binder : (Name.t Context.binder_annot * types) Val.tag
val val_univ : Univ.Level.t Val.tag
val val_free : Id.Set.t Val.tag
val val_ltac1 : Geninterp.Val.t Val.tag
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:46:50 +0000