1 files changed, 93 insertions, 9 deletions
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index 948a359124..4758ecf5bd 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -755,6 +755,12 @@ let () = define1 "constr_binder_type" (repr_ext val_binder) begin fun (bnd, ty)
   return (of_constr ty)
 end
 
+let () = define1 "constr_has_evar" constr begin fun c ->
+  Proofview.tclEVARMAP >>= fun sigma ->
+  let b = Evarutil.has_undefined_evars sigma c in
+  Proofview.tclUNIT (Value.of_bool b)
+end
+
 (** Patterns *)
 
 let empty_context = EConstr.mkMeta Constr_matching.special_meta
@@ -1075,6 +1081,54 @@ let () = define1 "env_instantiate" reference begin fun r ->
   return (Value.of_constr c)
 end
 
+(** Ind *)
+
+let () = define2 "ind_equal" (repr_ext val_inductive) (repr_ext val_inductive) begin fun ind1 ind2 ->
+  return (Value.of_bool (Ind.UserOrd.equal ind1 ind2))
+end
+
+let () = define1 "ind_data" (repr_ext val_inductive) begin fun ind ->
+  Proofview.tclENV >>= fun env ->
+  if Environ.mem_mind (fst ind) env then
+    let mib = Environ.lookup_mind (fst ind) env in
+    return (Value.of_ext val_ind_data (ind, mib))
+  else
+    throw err_notfound
+end
+
+let () = define1 "ind_repr" (repr_ext val_ind_data) begin fun (ind, _) ->
+  return (Value.of_ext val_inductive ind)
+end
+
+let () = define1 "ind_index" (repr_ext val_inductive) begin fun (ind, n) ->
+  return (Value.of_int n)
+end
+
+let () = define1 "ind_nblocks" (repr_ext val_ind_data) begin fun (ind, mib) ->
+  return (Value.of_int (Array.length mib.Declarations.mind_packets))
+end
+
+let () = define1 "ind_nconstructors" (repr_ext val_ind_data) begin fun ((_, n), mib) ->
+  let open Declarations in
+  return (Value.of_int (Array.length mib.mind_packets.(n).mind_consnames))
+end
+
+let () = define2 "ind_get_block" (repr_ext val_ind_data) int begin fun (ind, mib) n ->
+  if 0 <= n && n < Array.length mib.Declarations.mind_packets then
+    return (Value.of_ext val_ind_data ((fst ind, n), mib))
+  else throw err_notfound
+end
+
+let () = define2 "ind_get_constructor" (repr_ext val_ind_data) int begin fun ((mind, n), mib) i ->
+  let open Declarations in
+  let ncons = Array.length mib.mind_packets.(n).mind_consnames in
+  if 0 <= i && i < ncons then
+    (* WARNING: In the ML API constructors are indexed from 1 for historical
+       reasons, but Ltac2 uses 0-indexing instead. *)
+    return (Value.of_ext val_constructor ((mind, n), i + 1))
+  else throw err_notfound
+end
+
 (** Ltac1 in Ltac2 *)
 
 let ltac1 = Tac2ffi.repr_ext Value.val_ltac1
@@ -1132,6 +1186,16 @@ let () = define1 "ltac1_to_constr" ltac1 begin fun v ->
   return (Value.of_option Value.of_constr (Tacinterp.Value.to_constr v))
 end
 
+let () = define1 "ltac1_of_ident" ident begin fun c ->
+  let open Ltac_plugin in
+  return (Value.of_ext val_ltac1 (Taccoerce.Value.of_ident c))
+end
+
+let () = define1 "ltac1_to_ident" ltac1 begin fun v ->
+  let open Ltac_plugin in
+  return (Value.of_option Value.of_ident (Taccoerce.Value.to_ident v))
+end
+
 let () = define1 "ltac1_of_list" (list ltac1) begin fun l ->
   let open Geninterp.Val in
   return (Value.of_ext val_ltac1 (inject (Base typ_list) l))
@@ -1388,24 +1452,35 @@ let () =
 (** Ltac2 in terms *)
 
 let () =
-  let interp ist poly env sigma concl (ids, tac) =
+  let interp ?loc ~poly env sigma tycon (ids, tac) =
     (* Syntax prevents bound notation variables in constr quotations *)
     let () = assert (Id.Set.is_empty ids) in
-    let ist = Tac2interp.get_env ist in
+    let ist = Tac2interp.get_env @@ GlobEnv.lfun env in
     let tac = Proofview.tclIGNORE (Tac2interp.interp ist tac) in
     let name, poly = Id.of_string "ltac2", poly in
-    let c, sigma = Proof.refine_by_tactic ~name ~poly env sigma concl tac in
-    (EConstr.of_constr c, sigma)
+    let sigma, concl = match tycon with
+    | Some ty -> sigma, ty
+    | None -> GlobEnv.new_type_evar env sigma ~src:(loc,Evar_kinds.InternalHole)
+    in
+    let c, sigma = Proof.refine_by_tactic ~name ~poly (GlobEnv.renamed_env env) sigma concl tac in
+    let j = { Environ.uj_val = EConstr.of_constr c; Environ.uj_type = concl } in
+    (j, sigma)
   in
   GlobEnv.register_constr_interp0 wit_ltac2_constr interp
 
 let () =
-  let interp ist poly env sigma concl id =
-    let ist = Tac2interp.get_env ist in
+  let interp ?loc ~poly env sigma tycon id =
+    let ist = Tac2interp.get_env @@ GlobEnv.lfun env in
     let c = Id.Map.find id ist.env_ist in
     let c = Value.to_constr c in
-    let sigma = Typing.check env sigma c concl in
-    (c, sigma)
+    let t = Retyping.get_type_of (GlobEnv.renamed_env env) sigma c in
+    match tycon with
+    | None ->
+      { Environ.uj_val = c; Environ.uj_type = t }, sigma
+    | Some ty ->
+      let sigma = Evarconv.unify_leq_delay (GlobEnv.renamed_env env) sigma t ty in
+      let j = { Environ.uj_val = c; Environ.uj_type = ty } in
+      j, sigma
   in
   GlobEnv.register_constr_interp0 wit_ltac2_quotation interp
 
@@ -1679,6 +1754,16 @@ let () = add_scope "constr" (fun arg ->
     Tac2entries.ScopeRule (Pcoq.Symbol.nterm Pcoq.Constr.constr, act)
   )
 
+let () = add_scope "open_constr" (fun arg ->
+    let delimiters = List.map (function
+        | SexprRec (_, { v = Some s }, []) -> s
+        | _ -> scope_fail "open_constr" arg)
+        arg
+    in
+    let act e = Tac2quote.of_open_constr ~delimiters e in
+    Tac2entries.ScopeRule (Pcoq.Symbol.nterm Pcoq.Constr.constr, act)
+  )
+
 let add_expr_scope name entry f =
   add_scope name begin function
   | [] -> Tac2entries.ScopeRule (Pcoq.Symbol.nterm entry, f)
@@ -1707,7 +1792,6 @@ let () = add_expr_scope "constr_matching" q_constr_matching Tac2quote.of_constr_
 let () = add_expr_scope "goal_matching" q_goal_matching Tac2quote.of_goal_matching
 let () = add_expr_scope "format" Pcoq.Prim.lstring Tac2quote.of_format
 
-let () = add_generic_scope "open_constr" Pcoq.Constr.constr Tac2quote.wit_open_constr
 let () = add_generic_scope "pattern" Pcoq.Constr.constr Tac2quote.wit_pattern
 
 (** seq scope, a bit hairy *)