Implementing the Constr.in_context function.

2 files changed, 37 insertions, 0 deletions

diff --git a/src/tac2core.ml b/src/tac2core.ml
index 0304286639..468fddaddf 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -494,6 +494,38 @@ let () = define3 "constr_closenl" (list ident) int constr begin fun ids k c ->
   return (Value.of_constr ans)
 end
 
+let () = define3 "constr_in_context" ident constr closure begin fun id t c ->
+  Proofview.Goal.goals >>= function
+  | [gl] ->
+    gl >>= fun gl ->
+    let env = Proofview.Goal.env gl in
+    let sigma = Proofview.Goal.sigma gl in
+    let has_var =
+      try
+        let _ = Environ.lookup_named_val id (Environ.named_context_val env) in
+        true
+      with Not_found -> false
+    in
+    if has_var then
+      Tacticals.New.tclZEROMSG (str "Variable already exists")
+    else
+      let open Context.Named.Declaration in
+      let nenv = EConstr.push_named (LocalAssum (id, t)) env in
+      let (sigma, (evt, _)) = Evarutil.new_type_evar nenv sigma Evd.univ_flexible in
+      let (sigma, evk) = Evarutil.new_pure_evar (Environ.named_context_val nenv) sigma evt in
+      Proofview.Unsafe.tclEVARS sigma >>= fun () ->
+      Proofview.Unsafe.tclSETGOALS [evk] >>= fun () ->
+      thaw c >>= fun _ ->
+      Proofview.Unsafe.tclSETGOALS [Proofview.Goal.goal (Proofview.Goal.assume gl)] >>= fun () ->
+      let args = List.map (fun d -> EConstr.mkVar (get_id d)) (EConstr.named_context env) in
+      let args = Array.of_list (EConstr.mkRel 1 :: args) in
+      let ans = EConstr.mkEvar (evk, args) in
+      let ans = EConstr.mkLambda (Name id, t, ans) in
+      return (Value.of_constr ans)
+  | _ ->
+    throw err_notfocussed
+end
+
 (** Patterns *)
 
 let () = define2 "pattern_matches" pattern constr begin fun pat c ->
diff --git a/theories/Constr.v b/theories/Constr.v
index 3e67a486cf..072c613920 100644
--- a/theories/Constr.v
+++ b/theories/Constr.v
@@ -58,3 +58,8 @@ Ltac2 @ external closenl : ident list -> int -> constr -> constr := "ltac2" "con
     [Rel(k); ...; Rel(k+n-1)] in [c]. If two names are identical, the one of least index is kept. *)
 
 End Unsafe.
+
+Ltac2 @ external in_context : ident -> constr -> (unit -> unit) -> constr := "ltac2" "constr_in_context".
+(** On a focussed goal [Γ ⊢ A], [in_context id c tac] evaluates [tac] in a
+    focussed goal [Γ, id : c ⊢ ?X] and returns [fun (id : c) => t] where [t] is
+    the proof built by the tactic. *)