Expand the primitive functions on terms.

4 files changed, 141 insertions, 7 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
diff --git a/theories/Constr.v b/theories/Constr.v
index 801192d628..3e67a486cf 100644
--- a/theories/Constr.v
+++ b/theories/Constr.v
@@ -18,6 +18,8 @@ Module Unsafe.
 
 (** Low-level access to kernel terms. Use with care! *)
 
+Ltac2 Type case.
+
 Ltac2 Type kind := [
 | Rel (int)
 | Var (ident)
@@ -32,7 +34,7 @@ Ltac2 Type kind := [
 | Constant (constant, instance)
 | Ind (inductive, instance)
 | Constructor (constructor, instance)
-| Case (constr, constr, constr array)
+| Case (case, constr, constr, constr array)
 | Fix (int array, int, ident option array, constr array, constr array)
 | CoFix (int, ident option array, constr array, constr array)
 | Proj (projection, constr)
@@ -40,8 +42,19 @@ Ltac2 Type kind := [
 
 Ltac2 @ external kind : constr -> kind := "ltac2" "constr_kind".
 
+Ltac2 @ external make : kind -> constr := "ltac2" "constr_make".
+
+Ltac2 @ external check : constr -> constr result := "ltac2" "constr_check".
+(** Checks that a constr generated by unsafe means is indeed safe in the
+    current environment, and returns it, or the error otherwise. Panics if
+    not focussed. *)
+
 Ltac2 @ external substnl : constr list -> int -> constr -> constr := "ltac2" "constr_substnl".
 (** [substnl [r₁;...;rₙ] k c] substitutes in parallel [Rel(k+1); ...; Rel(k+n)] with
     [r₁;...;rₙ] in [c]. *)
 
+Ltac2 @ external closenl : ident list -> int -> constr -> constr := "ltac2" "constr_closenl".
+(** [closenl [x₁;...;xₙ] k c] abstracts over variables [x₁;...;xₙ] and replaces them with
+    [Rel(k); ...; Rel(k+n-1)] in [c]. If two names are identical, the one of least index is kept. *)
+
 End Unsafe.