aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/tac2core.ml131
-rw-r--r--src/tac2ffi.ml1
-rw-r--r--src/tac2ffi.mli1
3 files changed, 127 insertions, 6 deletions
diff --git a/src/tac2core.ml b/src/tac2core.ml
index 95fd29ec33..1f500352cf 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -61,15 +61,32 @@ let of_name c = match c with
| Anonymous -> Value.of_option Value.of_ident None
| Name id -> Value.of_option Value.of_ident (Some id)
-let of_instance sigma u =
- let u = Univ.Instance.to_array (EConstr.EInstance.kind sigma u) in
+let to_name c = match Value.to_option Value.to_ident c with
+| None -> Anonymous
+| Some id -> Name id
+
+let of_instance u =
+ let u = Univ.Instance.to_array (EConstr.Unsafe.to_instance u) in
Value.of_array (fun v -> Value.of_ext Value.val_univ v) u
+let to_instance u =
+ let u = Value.to_array (fun v -> Value.to_ext Value.val_univ v) u in
+ EConstr.EInstance.make (Univ.Instance.of_array u)
+
let of_rec_declaration (nas, ts, cs) =
(Value.of_array of_name nas,
Value.of_array Value.of_constr ts,
Value.of_array Value.of_constr cs)
+let to_rec_declaration (nas, ts, cs) =
+ (Value.to_array to_name nas,
+ Value.to_array Value.to_constr ts,
+ Value.to_array Value.to_constr cs)
+
+let of_result f = function
+| Inl c -> ValBlk (0, [|f c|])
+| Inr e -> ValBlk (1, [|Value.of_exn e|])
+
(** Stdlib exceptions *)
let err_notfocussed =
@@ -335,20 +352,21 @@ let () = define1 "constr_kind" begin fun c ->
| Const (cst, u) ->
ValBlk (10, [|
Value.of_constant cst;
- of_instance sigma u;
+ of_instance u;
|])
| Ind (ind, u) ->
ValBlk (11, [|
Value.of_ext Value.val_inductive ind;
- of_instance sigma u;
+ of_instance u;
|])
| Construct (cstr, u) ->
ValBlk (12, [|
Value.of_ext Value.val_constructor cstr;
- of_instance sigma u;
+ of_instance u;
|])
- | Case (_, c, t, bl) ->
+ | Case (ci, c, t, bl) ->
ValBlk (13, [|
+ Value.of_ext Value.val_case ci;
Value.of_constr c;
Value.of_constr t;
Value.of_array Value.of_constr bl;
@@ -378,6 +396,99 @@ let () = define1 "constr_kind" begin fun c ->
end
end
+let () = define1 "constr_make" begin fun knd ->
+ let open Constr in
+ let c = match knd with
+ | ValBlk (0, [|n|]) ->
+ let n = Value.to_int n in
+ EConstr.mkRel n
+ | ValBlk (1, [|id|]) ->
+ let id = Value.to_ident id in
+ EConstr.mkVar id
+ | ValBlk (2, [|n|]) ->
+ let n = Value.to_int n in
+ EConstr.mkMeta n
+ | ValBlk (3, [|evk; args|]) ->
+ let evk = Evar.unsafe_of_int (Value.to_int evk) in
+ let args = Value.to_array Value.to_constr args in
+ EConstr.mkEvar (evk, args)
+ | ValBlk (4, [|s|]) ->
+ let s = Value.to_ext Value.val_sort s in
+ EConstr.mkSort (EConstr.Unsafe.to_sorts s)
+ | ValBlk (5, [|c; k; t|]) ->
+ let c = Value.to_constr c in
+ let k = Value.to_ext Value.val_cast k in
+ let t = Value.to_constr t in
+ EConstr.mkCast (c, k, t)
+ | ValBlk (6, [|na; t; u|]) ->
+ let na = to_name na in
+ let t = Value.to_constr t in
+ let u = Value.to_constr u in
+ EConstr.mkProd (na, t, u)
+ | ValBlk (7, [|na; t; c|]) ->
+ let na = to_name na in
+ let t = Value.to_constr t in
+ let u = Value.to_constr c in
+ EConstr.mkLambda (na, t, u)
+ | ValBlk (8, [|na; b; t; c|]) ->
+ let na = to_name 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)
+ | ValBlk (9, [|c; cl|]) ->
+ let c = Value.to_constr c in
+ let cl = Value.to_array Value.to_constr cl in
+ EConstr.mkApp (c, cl)
+ | ValBlk (10, [|cst; u|]) ->
+ let cst = Value.to_constant cst in
+ let u = to_instance u in
+ EConstr.mkConstU (cst, u)
+ | ValBlk (11, [|ind; u|]) ->
+ let ind = Value.to_ext Value.val_inductive ind in
+ let u = to_instance u in
+ EConstr.mkIndU (ind, u)
+ | ValBlk (12, [|cstr; u|]) ->
+ let cstr = Value.to_ext Value.val_constructor cstr in
+ let u = to_instance u in
+ EConstr.mkConstructU (cstr, u)
+ | ValBlk (13, [|ci; c; t; bl|]) ->
+ let ci = Value.to_ext Value.val_case ci in
+ let c = Value.to_constr c in
+ let t = Value.to_constr t in
+ let bl = Value.to_array Value.to_constr bl in
+ EConstr.mkCase (ci, c, t, bl)
+ | ValBlk (14, [|recs; i; nas; ts; 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
+ EConstr.mkFix ((recs, i), def)
+ | ValBlk (15, [|i; nas; ts; cs|]) ->
+ let i = Value.to_int i in
+ let def = to_rec_declaration (nas, ts, cs) in
+ EConstr.mkCoFix (i, def)
+ | ValBlk (16, [|p; c|]) ->
+ let p = Value.to_ext Value.val_projection p in
+ let c = Value.to_constr c in
+ EConstr.mkProj (p, c)
+ | _ -> assert false
+ in
+ return (Value.of_constr c)
+end
+
+let () = define1 "constr_check" begin fun c ->
+ let c = Value.to_constr c in
+ pf_apply begin fun env sigma ->
+ try
+ let (sigma, _) = Typing.type_of env sigma c in
+ Proofview.Unsafe.tclEVARS sigma >>= fun () ->
+ return (of_result Value.of_constr (Inl c))
+ with e when CErrors.noncritical e ->
+ let e = CErrors.push e in
+ return (of_result Value.of_constr (Inr e))
+ end
+end
+
let () = define3 "constr_substnl" begin fun subst k c ->
let subst = Value.to_list Value.to_constr subst in
let k = Value.to_int k in
@@ -386,6 +497,14 @@ let () = define3 "constr_substnl" begin fun subst k c ->
return (Value.of_constr ans)
end
+let () = define3 "constr_closenl" begin fun ids k c ->
+ let ids = Value.to_list Value.to_ident ids in
+ let k = Value.to_int k in
+ let c = Value.to_constr c in
+ let ans = EConstr.Vars.substn_vars k ids c in
+ return (Value.of_constr ans)
+end
+
(** Patterns *)
let () = define2 "pattern_matches" begin fun pat c ->
diff --git a/src/tac2ffi.ml b/src/tac2ffi.ml
index 4d84da14ce..a1f9debdcb 100644
--- a/src/tac2ffi.ml
+++ b/src/tac2ffi.ml
@@ -26,6 +26,7 @@ let val_inductive = Val.create "inductive"
let val_constant = Val.create "constant"
let val_constructor = Val.create "constructor"
let val_projection = Val.create "projection"
+let val_case = Val.create "case"
let val_univ = Val.create "universe"
let val_kont : (Exninfo.iexn -> valexpr Proofview.tactic) Val.tag =
Val.create "kont"
diff --git a/src/tac2ffi.mli b/src/tac2ffi.mli
index cf1d7e81a1..e836319349 100644
--- a/src/tac2ffi.mli
+++ b/src/tac2ffi.mli
@@ -80,6 +80,7 @@ val val_inductive : inductive Val.tag
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_univ : Univ.universe_level Val.tag
val val_kont : (Exninfo.iexn -> valexpr Proofview.tactic) Val.tag
val val_free : Id.Set.t Val.tag
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-18 19:52:30 +0000