From 42448d31235767dc1eb1849e97f7b4ce2b276503 Mon Sep 17 00:00:00 2001 From: Rodolphe Lepigre Date: Mon, 17 Jul 2023 18:35:34 +0200 Subject: [PATCH] [ltac2] use the FFI tactic definition mechanism. --- plugins/ltac2/tac2core.ml | 1291 +++++++++++++++-------------------- plugins/ltac2/tac2stdlib.ml | 510 +++++++------- 2 files changed, 810 insertions(+), 991 deletions(-) diff --git a/plugins/ltac2/tac2core.ml b/plugins/ltac2/tac2core.ml index 5a3282f11257..1c2afbbda8f7 100644 --- a/plugins/ltac2/tac2core.ml +++ b/plugins/ltac2/tac2core.ml @@ -200,12 +200,6 @@ let fail ?(info = Exninfo.null) e = let return x = Proofview.tclUNIT x let pname ?(plugin=ltac2_plugin) s = { mltac_plugin = plugin; mltac_tactic = s } -let wrap f = - return () >>= fun () -> return (f ()) - -let wrap_unit f = - return () >>= fun () -> f (); return v_unit - let catchable_exception = function | Logic_monad.Exception _ -> false | e -> CErrors.noncritical e @@ -244,110 +238,60 @@ let pf_apply ?(catch_exceptions=false) f = | _ :: _ :: _ -> throw err_notfocussed -(** Primitives *) - -let define_primitive ?plugin name arity f = - Tac2env.define_primitive (pname ?plugin name) (mk_closure_val arity f) +open Tac2externals -let defineval ?plugin name v = Tac2env.define_primitive (pname ?plugin name) v - -let define0 ?plugin name f = define_primitive ?plugin name arity_one (fun _ -> f) - -let define1 name r0 f = define_primitive name arity_one begin fun x -> - f (Value.repr_to r0 x) -end - -let define2 name r0 r1 f = define_primitive name (arity_suc arity_one) begin fun x y -> - f (Value.repr_to r0 x) (Value.repr_to r1 y) -end - -let define_equality name r eq = define2 name r r begin fun x y -> - return (Value.of_bool (eq x y)) -end - -let define3 name r0 r1 r2 f = define_primitive name (arity_suc (arity_suc arity_one)) begin fun x y z -> - f (Value.repr_to r0 x) (Value.repr_to r1 y) (Value.repr_to r2 z) -end - -let define4 name r0 r1 r2 r3 f = define_primitive name (arity_suc (arity_suc (arity_suc arity_one))) begin fun x0 x1 x2 x3 -> - f (Value.repr_to r0 x0) (Value.repr_to r1 x1) (Value.repr_to r2 x2) (Value.repr_to r3 x3) -end - -let define5 name r0 r1 r2 r3 r4 f = define_primitive name (arity_suc (arity_suc (arity_suc (arity_suc arity_one)))) begin fun x0 x1 x2 x3 x4 -> - f (Value.repr_to r0 x0) (Value.repr_to r1 x1) (Value.repr_to r2 x2) (Value.repr_to r3 x3) (Value.repr_to r4 x4) -end +let define ?plugin s = define (pname ?plugin s) (** Printing *) -let () = define1 "print" pp begin fun pp -> - wrap_unit (fun () -> Feedback.msg_notice pp) -end +let () = define "print" (pp @-> ret unit) Feedback.msg_notice -let () = define1 "message_of_int" int begin fun n -> - return (Value.of_pp (Pp.int n)) -end +let () = define "message_of_int" (int @-> ret pp) Pp.int -let () = define1 "message_of_string" string begin fun s -> - return (Value.of_pp (str s)) -end - -let () = define1 "message_to_string" pp begin fun pp -> - return (Value.of_string (Pp.string_of_ppcmds pp)) -end +let () = define "message_of_string" (string @-> ret pp) Pp.str -let () = define1 "message_of_constr" constr begin fun c -> - pf_apply begin fun env sigma -> - let pp = Printer.pr_econstr_env env sigma c in - return (Value.of_pp pp) - end -end +let () = define "message_to_string" (pp @-> ret string) Pp.string_of_ppcmds -let () = define1 "message_of_ident" ident begin fun c -> - let pp = Id.print c in - return (Value.of_pp pp) -end +let () = + define "message_of_constr" (constr @-> tac pp) @@ fun c -> + pf_apply @@ fun env sigma -> return (Printer.pr_econstr_env env sigma c) -let () = define1 "message_of_exn" valexpr begin fun v -> - Proofview.tclENV >>= fun env -> - Proofview.tclEVARMAP >>= fun sigma -> - let pp = Tac2print.pr_valexpr env sigma v (GTypRef (Other Core.t_exn, [])) in - return (Value.of_pp pp) -end +let () = define "message_of_ident" (ident @-> ret pp) Id.print +let () = + define "message_of_exn" (valexpr @-> eret pp) @@ fun v env sigma -> + Tac2print.pr_valexpr env sigma v (GTypRef (Other Core.t_exn, [])) -let () = define2 "message_concat" pp pp begin fun m1 m2 -> - return (Value.of_pp (Pp.app m1 m2)) -end +let () = define "message_concat" (pp @-> pp @-> ret pp) Pp.app -let () = define0 "format_stop" begin - return (Value.of_ext val_format []) -end +let () = define "format_stop" (unit @-> ret format) (fun _ -> []) -let () = define1 "format_string" format begin fun s -> - return (Value.of_ext val_format (Tac2print.FmtString :: s)) -end +let () = + define "format_string" (format @-> ret format) @@ fun s -> + Tac2print.FmtString :: s -let () = define1 "format_int" format begin fun s -> - return (Value.of_ext val_format (Tac2print.FmtInt :: s)) -end +let () = + define "format_int" (format @-> ret format) @@ fun s -> + Tac2print.FmtInt :: s -let () = define1 "format_constr" format begin fun s -> - return (Value.of_ext val_format (Tac2print.FmtConstr :: s)) -end +let () = + define "format_constr" (format @-> ret format) @@ fun s -> + Tac2print.FmtConstr :: s -let () = define1 "format_ident" format begin fun s -> - return (Value.of_ext val_format (Tac2print.FmtIdent :: s)) -end +let () = + define "format_ident" (format @-> ret format) @@ fun s -> + Tac2print.FmtIdent :: s -let () = define2 "format_literal" string format begin fun lit s -> - return (Value.of_ext val_format (Tac2print.FmtLiteral lit :: s)) -end +let () = + define "format_literal" (string @-> format @-> ret format) @@ fun lit s -> + Tac2print.FmtLiteral lit :: s -let () = define1 "format_alpha" format begin fun s -> - return (Value.of_ext val_format (Tac2print.FmtAlpha :: s)) -end +let () = + define "format_alpha" (format @-> ret format) @@ fun s -> + Tac2print.FmtAlpha :: s -let () = define2 "format_kfprintf" closure format begin fun k fmt -> +let () = + define "format_kfprintf" (closure @-> format @-> tac valexpr) @@ fun k fmt -> let open Tac2print in let fold accu = function | FmtLiteral _ -> accu @@ -390,170 +334,128 @@ let () = define2 "format_kfprintf" closure format begin fun k fmt -> let eval v = eval (Pp.mt ()) v fmt in if Int.equal arity 0 then eval [] else return (Tac2ffi.of_closure (Tac2ffi.abstract arity eval)) -end (** Array *) -let () = define0 "array_empty" begin - return (v_blk 0 (Array.of_list [])) -end +let () = define "array_empty" (unit @-> ret valexpr) (fun _ -> v_blk 0 [||]) -let () = define2 "array_make" int valexpr begin fun n x -> - if n < 0 || n > Sys.max_array_length then throw err_outofbounds - else wrap (fun () -> v_blk 0 (Array.make n x)) -end +let () = + define "array_make" (int @-> valexpr @-> tac valexpr) @@ fun n x -> + try return (v_blk 0 (Array.make n x)) with Invalid_argument _ -> throw err_outofbounds -let () = define1 "array_length" block begin fun (_, v) -> - return (Value.of_int (Array.length v)) -end +let () = + define "array_length" (block @-> ret int) @@ fun (_, v) -> Array.length v -let () = define3 "array_set" block int valexpr begin fun (_, v) n x -> - if n < 0 || n >= Array.length v then throw err_outofbounds - else wrap_unit (fun () -> v.(n) <- x) -end +let () = + define "array_set" (block @-> int @-> valexpr @-> tac unit) @@ fun (_, v) n x -> + try Array.set v n x; return () with Invalid_argument _ -> throw err_outofbounds -let () = define2 "array_get" block int begin fun (_, v) n -> - if n < 0 || n >= Array.length v then throw err_outofbounds - else wrap (fun () -> v.(n)) -end +let () = + define "array_get" (block @-> int @-> tac valexpr) @@ fun (_, v) n -> + try return (Array.get v n) with Invalid_argument _ -> throw err_outofbounds -let () = define5 "array_blit" block int block int int begin fun (_, v0) s0 (_, v1) s1 l -> - if s0 < 0 || s0+l > Array.length v0 || s1 < 0 || s1+l > Array.length v1 || l<0 then throw err_outofbounds - else wrap_unit (fun () -> Array.blit v0 s0 v1 s1 l) -end +let () = + define "array_blit" + (block @-> int @-> block @-> int @-> int @-> tac unit) + @@ fun (_, v0) s0 (_, v1) s1 l -> + try Array.blit v0 s0 v1 s1 l; return () with Invalid_argument _ -> + throw err_outofbounds -let () = define4 "array_fill" block int int valexpr begin fun (_, d) s l v -> - if s < 0 || s+l > Array.length d || l<0 then throw err_outofbounds - else wrap_unit (fun () -> Array.fill d s l v) -end +let () = + define "array_fill" (block @-> int @-> int @-> valexpr @-> tac unit) @@ fun (_, d) s l v -> + try Array.fill d s l v; return () with Invalid_argument _ -> throw err_outofbounds -let () = define1 "array_concat" (list block) begin fun l -> - wrap (fun () -> v_blk 0 (Array.concat (List.map snd l))) -end +let () = + define "array_concat" (list block @-> ret valexpr) @@ fun l -> + v_blk 0 (Array.concat (List.map snd l)) (** Ident *) -let () = define2 "ident_equal" ident ident begin fun id1 id2 -> - return (Value.of_bool (Id.equal id1 id2)) -end +let () = define "ident_equal" (ident @-> ident @-> ret bool) Id.equal -let () = define1 "ident_to_string" ident begin fun id -> - return (Value.of_string (Id.to_string id)) -end +let () = define "ident_to_string" (ident @-> ret string) Id.to_string -let () = define1 "ident_of_string" string begin fun s -> - let id = try Some (Id.of_string s) with e when CErrors.noncritical e -> None in - return (Value.of_option Value.of_ident id) -end +let () = + define "ident_of_string" (string @-> ret (option ident)) @@ fun s -> + try Some (Id.of_string s) with e when CErrors.noncritical e -> None (** Int *) -let () = define2 "int_equal" int int begin fun m n -> - return (Value.of_bool (m == n)) -end +let () = define "int_equal" (int @-> int @-> ret bool) (==) -let unop n f = define1 n int begin fun m -> - return (Value.of_int (f m)) -end +let () = define "int_neg" (int @-> ret int) (~-) +let () = define "int_abs" (int @-> ret int) abs -let binop n f = define2 n int int begin fun m n -> - return (Value.of_int (f m n)) -end +let () = define "int_compare" (int @-> int @-> ret int) Int.compare +let () = define "int_add" (int @-> int @-> ret int) (+) +let () = define "int_sub" (int @-> int @-> ret int) (-) +let () = define "int_mul" (int @-> int @-> ret int) ( * ) -let () = binop "int_compare" Int.compare -let () = binop "int_add" (+) -let () = binop "int_sub" (-) -let () = binop "int_mul" ( * ) -let () = define2 "int_div" int int begin fun m n -> - if n == 0 then throw err_division_by_zero - else return (Value.of_int (m / n)) -end -let () = define2 "int_mod" int int begin fun m n -> - if n == 0 then throw err_division_by_zero - else return (Value.of_int (m mod n)) -end -let () = unop "int_neg" (~-) -let () = unop "int_abs" abs +let () = define "int_div" (int @-> int @-> tac int) @@ fun m n -> + if n == 0 then throw err_division_by_zero else return (m / n) +let () = define "int_mod" (int @-> int @-> tac int) @@ fun m n -> + if n == 0 then throw err_division_by_zero else return (m mod n) -let () = binop "int_asr" (asr) -let () = binop "int_lsl" (lsl) -let () = binop "int_lsr" (lsr) -let () = binop "int_land" (land) -let () = binop "int_lor" (lor) -let () = binop "int_lxor" (lxor) -let () = unop "int_lnot" lnot +let () = define "int_asr" (int @-> int @-> ret int) (asr) +let () = define "int_lsl" (int @-> int @-> ret int) (lsl) +let () = define "int_lsr" (int @-> int @-> ret int) (lsr) +let () = define "int_land" (int @-> int @-> ret int) (land) +let () = define "int_lor" (int @-> int @-> ret int) (lor) +let () = define "int_lxor" (int @-> int @-> ret int) (lxor) +let () = define "int_lnot" (int @-> ret int) lnot (** Char *) -let () = define1 "char_of_int" int begin fun n -> - wrap (fun () -> Value.of_char (Char.chr n)) -end - -let () = define1 "char_to_int" char begin fun n -> - wrap (fun () -> Value.of_int (Char.code n)) -end +let () = define "char_of_int" (int @-> ret char) Char.chr +let () = define "char_to_int" (char @-> ret int) Char.code (** String *) -let () = define2 "string_make" int char begin fun n c -> - if n < 0 || n > Sys.max_string_length then throw err_outofbounds - else wrap (fun () -> Value.of_bytes (Bytes.make n c)) -end +let () = + define "string_make" (int @-> char @-> tac bytes) @@ fun n c -> + try return (Bytes.make n c) with Invalid_argument _ -> throw err_outofbounds -let () = define1 "string_length" bytes begin fun s -> - return (Value.of_int (Bytes.length s)) -end +let () = define "string_length" (bytes @-> ret int) Bytes.length -let () = define3 "string_set" bytes int char begin fun s n c -> - if n < 0 || n >= Bytes.length s then throw err_outofbounds - else wrap_unit (fun () -> Bytes.set s n c) -end +let () = + define "string_set" (bytes @-> int @-> char @-> tac unit) @@ fun s n c -> + try Bytes.set s n c; return () with Invalid_argument _ -> throw err_outofbounds -let () = define2 "string_get" bytes int begin fun s n -> - if n < 0 || n >= Bytes.length s then throw err_outofbounds - else wrap (fun () -> Value.of_char (Bytes.get s n)) -end +let () = + define "string_get" (bytes @-> int @-> tac char) @@ fun s n -> + try return (Bytes.get s n) with Invalid_argument _ -> throw err_outofbounds -let () = define2 "string_concat" bytes (list bytes) begin fun sep l -> - return (Value.of_bytes (Bytes.concat sep l)) - end +let () = define "string_concat" (bytes @-> list bytes @-> ret bytes) Bytes.concat -let () = define2 "string_app" bytes bytes begin fun a b -> - return (Value.of_bytes (Bytes.concat Bytes.empty [a; b])) - end +let () = + define "string_app" (bytes @-> bytes @-> ret bytes) @@ fun a b -> + Bytes.concat Bytes.empty [a; b] -let () = define2 "string_equal" bytes bytes begin fun a b -> - return (Value.of_bool (Bytes.equal a b)) - end +let () = define "string_equal" (bytes @-> bytes @-> ret bool) Bytes.equal -let () = define2 "string_compare" bytes bytes begin fun a b -> - return (Value.of_int (Bytes.compare a b)) - end +let () = define "string_compare" (bytes @-> bytes @-> ret int) Bytes.compare (** Terms *) (** constr -> constr *) -let () = define1 "constr_type" constr begin fun c -> +let () = + define "constr_type" (constr @-> tac valexpr) @@ fun c -> let get_type env sigma = let (sigma, t) = Typing.type_of env sigma c in let t = Value.of_constr t in Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclUNIT t in pf_apply ~catch_exceptions:true get_type -end (** constr -> constr *) -let () = define2 "constr_equal" constr constr begin fun c1 c2 -> - Proofview.tclEVARMAP >>= fun sigma -> - let b = EConstr.eq_constr sigma c1 c2 in - Proofview.tclUNIT (Value.of_bool b) -end +let () = + define "constr_equal" (constr @-> constr @-> tac bool) @@ fun c1 c2 -> + Proofview.tclEVARMAP >>= fun sigma -> return (EConstr.eq_constr sigma c1 c2) -let () = define1 "constr_kind" constr begin fun c -> +let () = + define "constr_kind" (constr @-> eret valexpr) @@ fun c env sigma -> let open Constr in - Proofview.tclEVARMAP >>= fun sigma -> - Proofview.tclENV >>= fun env -> - return begin match EConstr.kind sigma c with + match EConstr.kind sigma c with | Rel n -> v_blk 0 [|Value.of_int n|] | Var id -> @@ -646,13 +548,10 @@ let () = define1 "constr_kind" constr begin fun c -> v_blk 18 [|Value.of_float f|] | Array(u,t,def,ty) -> v_blk 19 [|of_instance u; Value.of_array Value.of_constr t; Value.of_constr def; Value.of_constr ty|] - end -end -let () = define1 "constr_make" valexpr begin fun knd -> - Proofview.tclEVARMAP >>= fun sigma -> - Proofview.tclENV >>= fun env -> - let c = match Tac2ffi.to_block knd with +let () = + define "constr_make" (valexpr @-> eret constr) @@ fun knd env sigma -> + match Tac2ffi.to_block knd with | (0, [|n|]) -> let n = Value.to_int n in EConstr.mkRel n @@ -736,64 +635,57 @@ let () = define1 "constr_make" valexpr begin fun knd -> let u = to_instance u in EConstr.mkArray(u,t,def,ty) | _ -> assert false - in - return (Value.of_constr c) -end -let () = define1 "constr_check" constr begin fun c -> - 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 = Exninfo.capture e in - return (of_result Value.of_constr (Inr e)) - end -end +let () = + define "constr_check" (constr @-> tac valexpr) @@ fun c -> + pf_apply @@ 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 = Exninfo.capture e in + return (of_result Value.of_constr (Inr e)) -let () = define3 "constr_liftn" int int constr begin fun n k c -> - let ans = EConstr.Vars.liftn n k c in - return (Value.of_constr ans) -end +let () = + define "constr_liftn" (int @-> int @-> constr @-> ret constr) + EConstr.Vars.liftn -let () = define3 "constr_substnl" (list constr) int constr begin fun subst k c -> - let ans = EConstr.Vars.substnl subst k c in - return (Value.of_constr ans) -end +let () = + define "constr_substnl" (list constr @-> int @-> constr @-> ret constr) + EConstr.Vars.substnl -let () = define3 "constr_closenl" (list ident) int constr begin fun ids k c -> +let () = + define "constr_closenl" (list ident @-> int @-> constr @-> tac constr) + @@ fun ids k c -> Proofview.tclEVARMAP >>= fun sigma -> - let ans = EConstr.Vars.substn_vars sigma k ids c in - return (Value.of_constr ans) -end + return (EConstr.Vars.substn_vars sigma k ids c) -let () = define2 "constr_closedn" int constr begin fun n c -> +let () = + define "constr_closedn" (int @-> constr @-> tac bool) @@ fun n c -> Proofview.tclEVARMAP >>= fun sigma -> - let ans = EConstr.Vars.closedn sigma n c in - return (Value.of_bool ans) -end + return (EConstr.Vars.closedn sigma n c) -let () = define3 "constr_occur_between" int int constr begin fun n m c -> +let () = + define "constr_occur_between" (int @-> int @-> constr @-> tac bool) @@ fun n m c -> Proofview.tclEVARMAP >>= fun sigma -> - let ans = EConstr.Vars.noccur_between sigma n m c in - return (Value.of_bool (not ans)) -end + return (EConstr.Vars.noccur_between sigma n m c) -let () = define1 "constr_case" (repr_ext val_inductive) begin fun ind -> +let () = + define "constr_case" (repr_ext val_inductive @-> tac valexpr) @@ fun ind -> Proofview.tclENV >>= fun env -> try let ans = Inductiveops.make_case_info env ind Sorts.Relevant Constr.RegularStyle in return (Value.of_ext Value.val_case ans) with e when CErrors.noncritical e -> throw err_notfound -end -let () = defineval "constr_cast_default" (of_cast DEFAULTcast) -let () = defineval "constr_cast_vm" (of_cast VMcast) -let () = defineval "constr_cast_native" (of_cast NATIVEcast) +let () = define "constr_cast_default" (ret valexpr) (of_cast DEFAULTcast) +let () = define "constr_cast_vm" (ret valexpr) (of_cast VMcast) +let () = define "constr_cast_native" (ret valexpr) (of_cast NATIVEcast) -let () = define2 "constr_constructor" (repr_ext val_inductive) int begin fun (ind, i) k -> +let () = + define "constr_constructor" (repr_ext val_inductive @-> int @-> tac valexpr) @@ fun (ind, i) k -> Proofview.tclENV >>= fun env -> try let open Declarations in @@ -802,9 +694,9 @@ let () = define2 "constr_constructor" (repr_ext val_inductive) int begin fun (in return (Value.of_ext val_constructor ((ind, i), (k + 1))) with e when CErrors.noncritical e -> throw err_notfound -end -let () = define3 "constr_in_context" ident constr closure begin fun id t c -> +let () = + define "constr_in_context" (ident @-> constr @-> closure @-> tac constr) @@ fun id t c -> Proofview.Goal.goals >>= function | [gl] -> gl >>= fun gl -> @@ -836,109 +728,110 @@ let () = define3 "constr_in_context" ident constr closure begin fun id t c -> let args = EConstr.identity_subst_val (Environ.named_context_val env) in let args = SList.cons (EConstr.mkRel 1) args in let ans = EConstr.mkEvar (evk, args) in - let ans = EConstr.mkLambda (Context.make_annot (Name id) t_rel, t, ans) in - return (Value.of_constr ans) + return (EConstr.mkLambda (Context.make_annot (Name id) t_rel, t, ans)) | _ -> throw err_notfocussed -end (** preterm -> constr *) -let () = define1 "constr_pretype" (repr_ext val_preterm) begin fun c -> - let open Pretyping in - let open Ltac_pretype in - let pretype env sigma = - (* For now there are no primitives to create preterms with a non-empty - closure. I do not know whether [closed_glob_constr] is really the type - we want but it does not hurt in the meantime. *) - let { closure; term } = c in - let vars = { - ltac_constrs = closure.typed; - ltac_uconstrs = closure.untyped; - ltac_idents = closure.idents; - ltac_genargs = closure.genargs; - } in - let flags = constr_flags in - let sigma, t = understand_ltac flags env sigma vars WithoutTypeConstraint term in - let t = Value.of_constr t in - Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclUNIT t - in - pf_apply ~catch_exceptions:true pretype -end +let () = + define "constr_pretype" (repr_ext val_preterm @-> tac constr) @@ fun c -> + let open Pretyping in + let open Ltac_pretype in + let pretype env sigma = + (* For now there are no primitives to create preterms with a non-empty + closure. I do not know whether [closed_glob_constr] is really the type + we want but it does not hurt in the meantime. *) + let { closure; term } = c in + let vars = { + ltac_constrs = closure.typed; + ltac_uconstrs = closure.untyped; + ltac_idents = closure.idents; + ltac_genargs = closure.genargs; + } in + let flags = constr_flags in + let sigma, t = understand_ltac flags env sigma vars WithoutTypeConstraint term in + Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclUNIT t + in + pf_apply ~catch_exceptions:true pretype -let () = define2 "constr_binder_make" (option ident) constr begin fun na ty -> - pf_apply begin fun env sigma -> - match Retyping.relevance_of_type env sigma ty with - | rel -> - let na = match na with None -> Anonymous | Some id -> Name id in - return (Value.of_ext val_binder (Context.make_annot na rel, ty)) - | exception (Retyping.RetypeError _ as e) -> - let e, info = Exninfo.capture e in - fail ~info (CErrors.UserError Pp.(str "Not a type.")) - end -end +let () = + define "constr_binder_make" (option ident @-> constr @-> tac valexpr) @@ fun na ty -> + pf_apply @@ fun env sigma -> + match Retyping.relevance_of_type env sigma ty with + | rel -> + let na = match na with None -> Anonymous | Some id -> Name id in + return (Value.of_ext val_binder (Context.make_annot na rel, ty)) + | exception (Retyping.RetypeError _ as e) -> + let e, info = Exninfo.capture e in + fail ~info (CErrors.UserError Pp.(str "Not a type.")) -let () = define3 "constr_binder_unsafe_make" (option ident) relevance constr begin fun na rel ty -> +let () = + define "constr_binder_unsafe_make" + (option ident @-> relevance @-> constr @-> ret valexpr) + @@ fun na rel ty -> let na = match na with None -> Anonymous | Some id -> Name id in - return (Value.of_ext val_binder (Context.make_annot na rel, ty)) -end + Value.of_ext val_binder (Context.make_annot na rel, ty) -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 () = + define "constr_binder_name" (repr_ext val_binder @-> ret (option ident)) @@ fun (bnd, _) -> + match bnd.Context.binder_name with Anonymous -> None | Name id -> Some id -let () = define1 "constr_binder_type" (repr_ext val_binder) begin fun (bnd, ty) -> - return (of_constr ty) -end +let () = + define "constr_binder_type" (repr_ext val_binder @-> ret constr) @@ fun (_, ty) -> ty -let () = define1 "constr_has_evar" constr begin fun c -> +let () = + define "constr_has_evar" (constr @-> tac bool) @@ fun c -> Proofview.tclEVARMAP >>= fun sigma -> - let b = Evarutil.has_undefined_evars sigma c in - Proofview.tclUNIT (Value.of_bool b) -end + return (Evarutil.has_undefined_evars sigma c) (** Extra equalities *) -let () = define_equality "evar_equal" evar Evar.equal -let () = define_equality "float_equal" float Float64.equal -let () = define_equality "uint63_equal" uint63 Uint63.equal -let () = define_equality "meta_equal" int Int.equal -let () = define_equality "constr_cast_equal" cast Glob_ops.cast_kind_eq - -let () = define_equality "constant_equal" constant Constant.UserOrd.equal -let () = define_equality "constr_case_equal" (repr_ext val_case) begin fun x y -> - Ind.UserOrd.equal x.ci_ind y.ci_ind && Sorts.relevance_equal x.ci_relevance y.ci_relevance -end -let () = define_equality "constructor_equal" (repr_ext val_constructor) Construct.UserOrd.equal -let () = define_equality "projection_equal" (repr_ext val_projection) Projection.UserOrd.equal - +let () = define "evar_equal" (evar @-> evar @-> ret bool) Evar.equal +let () = define "float_equal" (float @-> float @-> ret bool) Float64.equal +let () = define "uint63_equal" (uint63 @-> uint63 @-> ret bool) Uint63.equal +let () = define "meta_equal" (int @-> int @-> ret bool) Int.equal +let () = define "constr_cast_equal" (cast @-> cast @-> ret bool) Glob_ops.cast_kind_eq +let () = + define "constant_equal" + (constant @-> constant @-> ret bool) + Constant.UserOrd.equal +let () = + let ty = repr_ext val_case in + define "constr_case_equal" (ty @-> ty @-> ret bool) @@ fun x y -> + Ind.UserOrd.equal x.ci_ind y.ci_ind && + Sorts.relevance_equal x.ci_relevance y.ci_relevance +let () = + let ty = repr_ext val_constructor in + define "constructor_equal" (ty @-> ty @-> ret bool) Construct.UserOrd.equal +let () = + let ty = repr_ext val_projection in + define "projection_equal" (ty @-> ty @-> ret bool) Projection.UserOrd.equal (** Patterns *) -let empty_context = Constr_matching.empty_context - -let () = define0 "pattern_empty_context" begin - return (Value.of_ext val_matching_context empty_context) -end +let () = + define "pattern_empty_context" + (unit @-> ret (repr_ext val_matching_context)) + (fun _ -> Constr_matching.empty_context) -let () = define2 "pattern_matches" pattern constr begin fun pat c -> - pf_apply begin fun env sigma -> - let ans = - try Some (Constr_matching.matches env sigma pat c) - with Constr_matching.PatternMatchingFailure -> None - in - begin match ans with - | None -> fail err_matchfailure - | Some ans -> - let ans = Id.Map.bindings ans in - let of_pair (id, c) = Value.of_tuple [| Value.of_ident id; Value.of_constr c |] in - return (Value.of_list of_pair ans) - end +let () = + define "pattern_matches" (pattern @-> constr @-> tac valexpr) @@ fun pat c -> + pf_apply @@ fun env sigma -> + let ans = + try Some (Constr_matching.matches env sigma pat c) + with Constr_matching.PatternMatchingFailure -> None + in + begin match ans with + | None -> fail err_matchfailure + | Some ans -> + let ans = Id.Map.bindings ans in + let of_pair (id, c) = Value.of_tuple [| Value.of_ident id; Value.of_constr c |] in + return (Value.of_list of_pair ans) end -end -let () = define2 "pattern_matches_subterm" pattern constr begin fun pat c -> +let () = + define "pattern_matches_subterm" (pattern @-> constr @-> tac valexpr) @@ fun pat c -> let open Constr_matching in let rec of_ans s = match IStream.peek s with | IStream.Nil -> fail err_matchfailure @@ -948,30 +841,27 @@ let () = define2 "pattern_matches_subterm" pattern constr begin fun pat c -> let ans = Value.of_tuple [| Value.of_ext val_matching_context m_ctx; Value.of_list of_pair ans |] in Proofview.tclOR (return ans) (fun _ -> of_ans s) in - pf_apply begin fun env sigma -> - let pat = Constr_matching.instantiate_pattern env sigma Id.Map.empty pat in - let ans = Constr_matching.match_subterm env sigma (Id.Set.empty,pat) c in - of_ans ans - end -end + pf_apply @@ fun env sigma -> + let pat = Constr_matching.instantiate_pattern env sigma Id.Map.empty pat in + let ans = Constr_matching.match_subterm env sigma (Id.Set.empty,pat) c in + of_ans ans -let () = define2 "pattern_matches_vect" pattern constr begin fun pat c -> - pf_apply begin fun env sigma -> - let ans = - try Some (Constr_matching.matches env sigma pat c) - with Constr_matching.PatternMatchingFailure -> None - in - begin match ans with - | None -> fail err_matchfailure - | Some ans -> - let ans = Id.Map.bindings ans in - let ans = Array.map_of_list snd ans in - return (Value.of_array Value.of_constr ans) - end - end -end +let () = + define "pattern_matches_vect" (pattern @-> constr @-> tac valexpr) @@ fun pat c -> + pf_apply @@ fun env sigma -> + let ans = + try Some (Constr_matching.matches env sigma pat c) + with Constr_matching.PatternMatchingFailure -> None + in + match ans with + | None -> fail err_matchfailure + | Some ans -> + let ans = Id.Map.bindings ans in + let ans = Array.map_of_list snd ans in + return (Value.of_array Value.of_constr ans) -let () = define2 "pattern_matches_subterm_vect" pattern constr begin fun pat c -> +let () = + define "pattern_matches_subterm_vect" (pattern @-> constr @-> tac valexpr) @@ fun pat c -> let open Constr_matching in let rec of_ans s = match IStream.peek s with | IStream.Nil -> fail err_matchfailure @@ -981,91 +871,87 @@ let () = define2 "pattern_matches_subterm_vect" pattern constr begin fun pat c - let ans = Value.of_tuple [| Value.of_ext val_matching_context m_ctx; Value.of_array Value.of_constr ans |] in Proofview.tclOR (return ans) (fun _ -> of_ans s) in - pf_apply begin fun env sigma -> - let pat = Constr_matching.instantiate_pattern env sigma Id.Map.empty pat in - let ans = Constr_matching.match_subterm env sigma (Id.Set.empty,pat) c in - of_ans ans - end -end + pf_apply @@ fun env sigma -> + let pat = Constr_matching.instantiate_pattern env sigma Id.Map.empty pat in + let ans = Constr_matching.match_subterm env sigma (Id.Set.empty,pat) c in + of_ans ans let match_pattern = map_repr (fun (b,pat) -> if b then Tac2match.MatchPattern pat else Tac2match.MatchContext pat) (function Tac2match.MatchPattern pat -> (true, pat) | MatchContext pat -> (false, pat)) (pair bool pattern) -let () = define3 "pattern_matches_goal" bool - (list (pair (option match_pattern) match_pattern)) - match_pattern - begin fun rev hp cp -> +let () = + define "pattern_matches_goal" + (bool @-> list (pair (option match_pattern) match_pattern) @-> match_pattern @-> tac valexpr) + @@ fun rev hp cp -> assert_focussed >>= fun () -> - Proofview.Goal.enter_one begin fun gl -> + Proofview.Goal.enter_one @@ fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let concl = Proofview.Goal.concl gl in Tac2match.match_goal env sigma concl ~rev (hp, cp) >>= fun (hyps, ctx, subst) -> - let of_ctxopt ctx = Value.of_ext val_matching_context (Option.default empty_context ctx) in - let hids = Value.of_array Value.of_ident (Array.map_of_list pi1 hyps) in - let hbctx = Value.of_array of_ctxopt - (Array.of_list (CList.filter_map (fun (_,bctx,_) -> bctx) hyps)) - in - let hctx = Value.of_array of_ctxopt (Array.map_of_list pi3 hyps) in - let subs = Value.of_array Value.of_constr (Array.map_of_list snd (Id.Map.bindings subst)) in - let cctx = of_ctxopt ctx in - let ans = Value.of_tuple [| hids; hbctx; hctx; subs; cctx |] in - Proofview.tclUNIT ans - end -end + let empty_context = Constr_matching.empty_context in + let of_ctxopt ctx = Value.of_ext val_matching_context (Option.default empty_context ctx) in + let hids = Value.of_array Value.of_ident (Array.map_of_list pi1 hyps) in + let hbctx = Value.of_array of_ctxopt + (Array.of_list (CList.filter_map (fun (_,bctx,_) -> bctx) hyps)) + in + let hctx = Value.of_array of_ctxopt (Array.map_of_list pi3 hyps) in + let subs = Value.of_array Value.of_constr (Array.map_of_list snd (Id.Map.bindings subst)) in + let cctx = of_ctxopt ctx in + let ans = Value.of_tuple [| hids; hbctx; hctx; subs; cctx |] in + Proofview.tclUNIT ans -let () = define2 "pattern_instantiate" (repr_ext val_matching_context) constr begin fun ctx c -> - let ans = Constr_matching.instantiate_context ctx c in - return (Value.of_constr ans) -end +let () = + define "pattern_instantiate" + (repr_ext val_matching_context @-> constr @-> ret constr) + Constr_matching.instantiate_context (** Error *) -let () = define1 "throw" exn begin fun (e, info) -> - throw ~info e -end +let () = + define "throw" (exn @-> tac valexpr) @@ fun (e, info) -> throw ~info e (** Control *) (** exn -> 'a *) -let () = define1 "zero" exn begin fun (e, info) -> - fail ~info e -end +let () = + define "zero" (exn @-> tac valexpr) @@ fun (e, info) -> fail ~info e (** (unit -> 'a) -> (exn -> 'a) -> 'a *) -let () = define2 "plus" closure closure begin fun x k -> +let () = + define "plus" (closure @-> closure @-> tac valexpr) @@ fun x k -> Proofview.tclOR (thaw x) (fun e -> Tac2ffi.apply k [Value.of_exn e]) -end (** (unit -> 'a) -> 'a *) -let () = define1 "once" closure begin fun f -> +let () = + define "once" (closure @-> tac valexpr) @@ fun f -> Proofview.tclONCE (thaw f) -end (** (unit -> unit) list -> unit *) -let () = define1 "dispatch" (list closure) begin fun l -> +let () = + define "dispatch" (list closure @-> tac unit) @@ fun l -> let l = List.map (fun f -> Proofview.tclIGNORE (thaw f)) l in - Proofview.tclDISPATCH l >>= fun () -> return v_unit -end + Proofview.tclDISPATCH l (** (unit -> unit) list -> (unit -> unit) -> (unit -> unit) list -> unit *) -let () = define3 "extend" (list closure) closure (list closure) begin fun lft tac rgt -> +let () = + define "extend" (list closure @-> closure @-> list closure @-> tac unit) @@ fun lft tac rgt -> let lft = List.map (fun f -> Proofview.tclIGNORE (thaw f)) lft in let tac = Proofview.tclIGNORE (thaw tac) in let rgt = List.map (fun f -> Proofview.tclIGNORE (thaw f)) rgt in - Proofview.tclEXTEND lft tac rgt >>= fun () -> return v_unit -end + Proofview.tclEXTEND lft tac rgt (** (unit -> unit) -> unit *) -let () = define1 "enter" closure begin fun f -> +let () = + define "enter" (closure @-> tac unit) @@ fun f -> let f = Proofview.tclIGNORE (thaw f) in - Proofview.tclINDEPENDENT f >>= fun () -> return v_unit -end + Proofview.tclINDEPENDENT f (** (unit -> 'a) -> ('a * ('exn -> 'a)) result *) -let () = define1 "case" closure begin fun f -> +let () = + define "case" (closure @-> tac valexpr) @@ fun f -> Proofview.tclCASE (thaw f) >>= begin function | Proofview.Next (x, k) -> let k = Tac2ffi.mk_closure arity_one begin fun e -> @@ -1076,247 +962,230 @@ let () = define1 "case" closure begin fun f -> return (v_blk 0 [| Value.of_tuple [| x; Value.of_closure k |] |]) | Proofview.Fail e -> return (v_blk 1 [| Value.of_exn e |]) end -end (** int -> int -> (unit -> 'a) -> 'a *) -let () = define3 "focus" int int closure begin fun i j tac -> +let () = + define "focus" (int @-> int @-> closure @-> tac valexpr) @@ fun i j tac -> Proofview.tclFOCUS i j (thaw tac) -end (** unit -> unit *) -let () = define0 "shelve" begin - Proofview.shelve >>= fun () -> return v_unit -end +let () = define "shelve" (unit @-> tac unit) @@ fun _ -> Proofview.shelve (** unit -> unit *) -let () = define0 "shelve_unifiable" begin - Proofview.shelve_unifiable >>= fun () -> return v_unit -end +let () = + define "shelve_unifiable" (unit @-> tac unit) @@ fun _ -> + Proofview.shelve_unifiable -let () = define1 "new_goal" evar begin fun ev -> +let () = + define "new_goal" (evar @-> tac unit) @@ fun ev -> Proofview.tclEVARMAP >>= fun sigma -> if Evd.mem sigma ev then - Proofview.Unsafe.tclNEWGOALS [Proofview.with_empty_state ev] <*> Proofview.tclUNIT v_unit + Proofview.Unsafe.tclNEWGOALS [Proofview.with_empty_state ev] <*> + Proofview.tclUNIT () else throw err_notfound -end (** unit -> constr *) -let () = define0 "goal" begin +let () = + define "goal" (unit @-> tac constr) @@ fun _ -> assert_focussed >>= fun () -> - Proofview.Goal.enter_one begin fun gl -> - let concl = Tacmach.pf_nf_concl gl in - return (Value.of_constr concl) - end -end + Proofview.Goal.enter_one @@ fun gl -> return (Tacmach.pf_nf_concl gl) (** ident -> constr *) -let () = define1 "hyp" ident begin fun id -> - pf_apply begin fun env _ -> - let mem = try ignore (Environ.lookup_named id env); true with Not_found -> false in - if mem then return (Value.of_constr (EConstr.mkVar id)) - else Tacticals.tclZEROMSG - (str "Hypothesis " ++ quote (Id.print id) ++ str " not found") (* FIXME: Do something more sensible *) - end -end +let () = + define "hyp" (ident @-> tac constr) @@ fun id -> + pf_apply @@ fun env _ -> + let mem = try ignore (Environ.lookup_named id env); true with Not_found -> false in + if mem then return (EConstr.mkVar id) + else Tacticals.tclZEROMSG + (str "Hypothesis " ++ quote (Id.print id) ++ str " not found") (* FIXME: Do something more sensible *) -let () = define0 "hyps" begin - pf_apply begin fun env _ -> - let open Context in - let open Named.Declaration in - let hyps = List.rev (Environ.named_context env) in - let map = function - | LocalAssum (id, t) -> - let t = EConstr.of_constr t in - Value.of_tuple [|Value.of_ident id.binder_name; Value.of_option Value.of_constr None; Value.of_constr t|] - | LocalDef (id, c, t) -> - let c = EConstr.of_constr c in - let t = EConstr.of_constr t in - Value.of_tuple [|Value.of_ident id.binder_name; Value.of_option Value.of_constr (Some c); Value.of_constr t|] - in - return (Value.of_list map hyps) - end -end +let () = + define "hyps" (unit @-> tac valexpr) @@ fun _ -> + pf_apply @@ fun env _ -> + let open Context in + let open Named.Declaration in + let hyps = List.rev (Environ.named_context env) in + let map = function + | LocalAssum (id, t) -> + let t = EConstr.of_constr t in + Value.of_tuple [|Value.of_ident id.binder_name; Value.of_option Value.of_constr None; Value.of_constr t|] + | LocalDef (id, c, t) -> + let c = EConstr.of_constr c in + let t = EConstr.of_constr t in + Value.of_tuple [|Value.of_ident id.binder_name; Value.of_option Value.of_constr (Some c); Value.of_constr t|] + in + return (Value.of_list map hyps) (** (unit -> constr) -> unit *) -let () = define1 "refine" closure begin fun c -> +let () = + define "refine" (closure @-> tac unit) @@ fun c -> let c = thaw c >>= fun c -> Proofview.tclUNIT ((), Value.to_constr c) in - Proofview.Goal.enter begin fun gl -> - Refine.generic_refine ~typecheck:true c gl - end >>= fun () -> return v_unit -end + Proofview.Goal.enter @@ fun gl -> + Refine.generic_refine ~typecheck:true c gl -let () = define2 "with_holes" closure closure begin fun x f -> +let () = + define "with_holes" (closure @-> closure @-> tac valexpr) @@ fun x f -> Proofview.tclEVARMAP >>= fun sigma0 -> thaw x >>= fun ans -> Proofview.tclEVARMAP >>= fun sigma -> Proofview.Unsafe.tclEVARS sigma0 >>= fun () -> Tacticals.tclWITHHOLES false (Tac2ffi.apply f [ans]) sigma -end -let () = define1 "progress" closure begin fun f -> +let () = + define "progress" (closure @-> tac valexpr) @@ fun f -> Proofview.tclPROGRESS (thaw f) -end -let () = define2 "abstract" (option ident) closure begin fun id f -> - Abstract.tclABSTRACT id (Proofview.tclIGNORE (thaw f)) >>= fun () -> - return v_unit -end +let () = + define "abstract" (option ident @-> closure @-> tac unit) @@ fun id f -> + Abstract.tclABSTRACT id (Proofview.tclIGNORE (thaw f)) -let () = define2 "time" (option string) closure begin fun s f -> +let () = + define "time" (option string @-> closure @-> tac valexpr) @@ fun s f -> Proofview.tclTIME s (thaw f) -end -let () = define0 "check_interrupt" begin - Proofview.tclCHECKINTERRUPT >>= fun () -> return v_unit -end +let () = + define "check_interrupt" (unit @-> tac unit) @@ fun _ -> + Proofview.tclCHECKINTERRUPT (** Fresh *) -let () = define2 "fresh_free_union" (repr_ext val_free) (repr_ext val_free) begin fun set1 set2 -> - let ans = Id.Set.union set1 set2 in - return (Value.of_ext Value.val_free ans) -end +let () = + let ty = repr_ext val_free in + define "fresh_free_union" (ty @-> ty @-> ret ty) Id.Set.union -let () = define1 "fresh_free_of_ids" (list ident) begin fun ids -> - let free = List.fold_right Id.Set.add ids Id.Set.empty in - return (Value.of_ext Value.val_free free) -end +let () = + define "fresh_free_of_ids" (list ident @-> ret (repr_ext val_free)) @@ fun ids -> + List.fold_right Id.Set.add ids Id.Set.empty -let () = define1 "fresh_free_of_constr" constr begin fun c -> +let () = + define "fresh_free_of_constr" (constr @-> tac (repr_ext val_free)) @@ fun c -> Proofview.tclEVARMAP >>= fun sigma -> - let rec fold accu c = match EConstr.kind sigma c with - | Constr.Var id -> Id.Set.add id accu - | _ -> EConstr.fold sigma fold accu c + let rec fold accu c = + match EConstr.kind sigma c with + | Constr.Var id -> Id.Set.add id accu + | _ -> EConstr.fold sigma fold accu c in - let ans = fold Id.Set.empty c in - return (Value.of_ext Value.val_free ans) -end + return (fold Id.Set.empty c) -let () = define2 "fresh_fresh" (repr_ext val_free) ident begin fun avoid id -> - let nid = Namegen.next_ident_away_from id (fun id -> Id.Set.mem id avoid) in - return (Value.of_ident nid) -end +let () = + define "fresh_fresh" (repr_ext val_free @-> ident @-> ret ident) @@ fun avoid id -> + Namegen.next_ident_away_from id (fun id -> Id.Set.mem id avoid) (** Env *) -let () = define1 "env_get" (list ident) begin fun ids -> - let r = match ids with +let () = + define "env_get" (list ident @-> ret (option reference)) @@ fun ids -> + match ids with | [] -> None | _ :: _ as ids -> let (id, path) = List.sep_last ids in let path = DirPath.make (List.rev path) in let fp = Libnames.make_path path id in try Some (Nametab.global_of_path fp) with Not_found -> None - in - return (Value.of_option Value.of_reference r) -end -let () = define1 "env_expand" (list ident) begin fun ids -> - let r = match ids with +let () = + define "env_expand" (list ident @-> ret (list reference)) @@ fun ids -> + match ids with | [] -> [] | _ :: _ as ids -> let (id, path) = List.sep_last ids in let path = DirPath.make (List.rev path) in let qid = Libnames.make_qualid path id in Nametab.locate_all qid - in - return (Value.of_list Value.of_reference r) -end -let () = define1 "env_path" reference begin fun r -> +let () = + define "env_path" (reference @-> tac (list ident)) @@ fun r -> match Nametab.path_of_global r with | fp -> let (path, id) = Libnames.repr_path fp in let path = DirPath.repr path in - return (Value.of_list Value.of_ident (List.rev_append path [id])) + return (List.rev_append path [id]) | exception Not_found -> throw err_notfound -end -let () = define1 "env_instantiate" reference begin fun r -> +let () = + define "env_instantiate" (reference @-> tac constr) @@ fun r -> Proofview.tclENV >>= fun env -> Proofview.tclEVARMAP >>= fun sigma -> let (sigma, c) = Evd.fresh_global env sigma r in Proofview.Unsafe.tclEVARS sigma >>= fun () -> - return (Value.of_constr c) -end + return c (** 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 () = + let ty = repr_ext val_inductive in + define "ind_equal" (ty @-> ty @-> ret bool) Ind.UserOrd.equal -let () = define1 "ind_data" (repr_ext val_inductive) begin fun ind -> +let () = + define "ind_data" + (repr_ext val_inductive @-> tac (repr_ext val_ind_data)) + @@ 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)) + return (ind, Environ.lookup_mind (fst ind) env) 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 () = define "ind_repr" (repr_ext val_ind_data @-> ret (repr_ext val_inductive)) fst +let () = define "ind_index" (repr_ext val_inductive @-> ret int) snd -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 () = + define "ind_nblocks" (repr_ext val_ind_data @-> ret int) @@ fun (_, mib) -> + Array.length mib.Declarations.mind_packets -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 () = + define "ind_nconstructors" (repr_ext val_ind_data @-> ret int) @@ fun ((_, n), mib) -> + Array.length Declarations.(mib.mind_packets.(n).mind_consnames) -let () = define2 "ind_get_block" (repr_ext val_ind_data) int begin fun (ind, mib) n -> +let () = + define "ind_get_block" + (repr_ext val_ind_data @-> int @-> tac (repr_ext val_ind_data)) + @@ 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)) + return ((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 () = + define "ind_get_constructor" + (repr_ext val_ind_data @-> int @-> tac (repr_ext val_constructor)) + @@ 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)) + return ((mind, n), i + 1) else throw err_notfound -end (** Ltac1 in Ltac2 *) let ltac1 = Tac2ffi.repr_ext Value.val_ltac1 let of_ltac1 v = Value.of_ext Value.val_ltac1 v -let () = define1 "ltac1_ref" (list ident) begin fun ids -> +let () = + define "ltac1_ref" (list ident @-> ret ltac1) @@ fun ids -> let open Ltac_plugin in - let r = match ids with - | [] -> raise Not_found - | _ :: _ as ids -> - let (id, path) = List.sep_last ids in - let path = DirPath.make (List.rev path) in - let fp = Libnames.make_path path id in - if Tacenv.exists_tactic fp then - List.hd (Tacenv.locate_extended_all_tactic (Libnames.qualid_of_path fp)) - else raise Not_found + let r = + match ids with + | [] -> raise Not_found + | _ :: _ as ids -> + let (id, path) = List.sep_last ids in + let path = DirPath.make (List.rev path) in + let fp = Libnames.make_path path id in + if Tacenv.exists_tactic fp then + List.hd (Tacenv.locate_extended_all_tactic (Libnames.qualid_of_path fp)) + else raise Not_found in - let tac = Tacinterp.Value.of_closure (Tacinterp.default_ist ()) (Tacenv.interp_ltac r) in - return (Value.of_ext val_ltac1 tac) -end + Tacinterp.Value.of_closure (Tacinterp.default_ist ()) (Tacenv.interp_ltac r) -let () = define1 "ltac1_run" ltac1 begin fun v -> +let () = + define "ltac1_run" (ltac1 @-> tac unit) @@ fun v -> let open Ltac_plugin in - Tacinterp.tactic_of_value (Tacinterp.default_ist ()) v >>= fun () -> - return v_unit -end + Tacinterp.tactic_of_value (Tacinterp.default_ist ()) v -let () = define3 "ltac1_apply" ltac1 (list ltac1) closure begin fun f args k -> +let () = + define "ltac1_apply" (ltac1 @-> list ltac1 @-> closure @-> tac unit) @@ fun f args k -> let open Ltac_plugin in let open Tacexpr in let open Locus in @@ -1332,39 +1201,31 @@ let () = define3 "ltac1_apply" ltac1 (list ltac1) closure begin fun f args k -> let lfun = Id.Map.add (Id.of_string "F") f lfun in let ist = { (Tacinterp.default_ist ()) with Tacinterp.lfun = lfun; } in let tac = CAst.make @@ TacArg (TacCall (CAst.make (ArgVar CAst.(make @@ Id.of_string "F"),args))) in - Tacinterp.val_interp ist tac k >>= fun () -> - return v_unit -end + Tacinterp.val_interp ist tac k -let () = define1 "ltac1_of_constr" constr begin fun c -> - let open Ltac_plugin in - return (Value.of_ext val_ltac1 (Tacinterp.Value.of_constr c)) -end +let () = + define "ltac1_of_constr" (constr @-> ret ltac1) + Ltac_plugin.Tacinterp.Value.of_constr -let () = define1 "ltac1_to_constr" ltac1 begin fun v -> - let open Ltac_plugin in - return (Value.of_option Value.of_constr (Tacinterp.Value.to_constr v)) -end +let () = + define "ltac1_to_constr" (ltac1 @-> ret (option constr)) + Ltac_plugin.Tacinterp.Value.to_constr -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 () = + define "ltac1_of_ident" (ident @-> ret ltac1) + Ltac_plugin.Taccoerce.Value.of_ident -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 () = + define "ltac1_to_ident" (ltac1 @-> ret (option ident)) + Ltac_plugin.Taccoerce.Value.to_ident -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)) -end +let () = + define "ltac1_of_list" (list ltac1 @-> ret ltac1) @@ fun l -> + Geninterp.Val.(inject (Base typ_list) l) -let () = define1 "ltac1_to_list" ltac1 begin fun v -> - let open Ltac_plugin in - return (Value.of_option (Value.of_list of_ltac1) (Tacinterp.Value.to_list v)) -end +let () = + define "ltac1_to_list" (ltac1 @-> ret (option (list ltac1))) + Ltac_plugin.Tacinterp.Value.to_list module MapTagDyn = Dyn.Make() @@ -1406,7 +1267,7 @@ let maps = ref MapMap.empty let register_map ?(plugin=ltac2_plugin) ~tag_name x = let tag = MapTagDyn.create (plugin^":"^tag_name) in let () = maps := MapMap.add tag (Map x) !maps in - let () = defineval ~plugin tag_name (repr_of map_tag_repr (Any tag)) in + let () = define ~plugin tag_name (ret map_tag_repr) (Any tag) in tag let get_map (type t s m) (tag:(t,s,m) map_tag) @@ -1470,174 +1331,149 @@ let constant_map_tag : _ map_tag = register_map ~tag_name:"fmap_constant_tag" (m let valmap_eq = Refl end) -let () = define1 "fset_empty" map_tag_repr begin fun (Any tag) -> - let module V = (val get_map tag) in - let open V in - return (tag_set tag S.empty) - end +let () = + define "fset_empty" (map_tag_repr @-> ret valexpr) @@ fun (Any tag) -> + let (module V) = get_map tag in + tag_set tag V.S.empty -let () = define1 "fset_is_empty" set_repr begin fun (TaggedSet (tag,s)) -> - let module V = (val get_map tag) in - let open V in - return (Value.of_bool (S.is_empty s)) - end +let () = + define "fset_is_empty" (set_repr @-> ret bool) @@ fun (TaggedSet (tag,s)) -> + let (module V) = get_map tag in + V.S.is_empty s -let () = define2 "fset_mem" valexpr set_repr begin fun x (TaggedSet (tag,s)) -> - let module V = (val get_map tag) in - let open V in - let x = repr_to repr x in - return (Value.of_bool (S.mem x s)) - end +let () = + define "fset_mem" (valexpr @-> set_repr @-> ret bool) @@ fun x (TaggedSet (tag,s)) -> + let (module V) = get_map tag in + V.S.mem (repr_to V.repr x) s -let () = define2 "fset_add" valexpr set_repr begin fun x (TaggedSet (tag,s)) -> - let module V = (val get_map tag) in - let open V in - let x = repr_to repr x in - return (tag_set tag (S.add x s)) - end +let () = + define "fset_add" (valexpr @-> set_repr @-> ret valexpr) @@ fun x (TaggedSet (tag,s)) -> + let (module V) = get_map tag in + tag_set tag (V.S.add (repr_to V.repr x) s) -let () = define2 "fset_remove" valexpr set_repr begin fun x (TaggedSet (tag,s)) -> - let module V = (val get_map tag) in - let open V in - let x = repr_to repr x in - return (tag_set tag (S.remove x s)) - end +let () = + define "fset_remove" (valexpr @-> set_repr @-> ret valexpr) @@ fun x (TaggedSet (tag,s)) -> + let (module V) = get_map tag in + tag_set tag (V.S.remove (repr_to V.repr x) s) -let () = define2 "fset_union" set_repr set_repr - begin fun (TaggedSet (tag,s1)) (TaggedSet (tag',s2)) -> - let Refl = assert_map_tag_eq tag tag' in - let module V = (val get_map tag) in - let open V in - return (tag_set tag (S.union s1 s2)) - end +let () = + define "fset_union" (set_repr @-> set_repr @-> ret valexpr) + @@ fun (TaggedSet (tag,s1)) (TaggedSet (tag',s2)) -> + let Refl = assert_map_tag_eq tag tag' in + let (module V) = get_map tag in + tag_set tag (V.S.union s1 s2) -let () = define2 "fset_inter" set_repr set_repr - begin fun (TaggedSet (tag,s1)) (TaggedSet (tag',s2)) -> - let Refl = assert_map_tag_eq tag tag' in - let module V = (val get_map tag) in - let open V in - return (tag_set tag (S.inter s1 s2)) - end +let () = + define "fset_inter" (set_repr @-> set_repr @-> ret valexpr) + @@ fun (TaggedSet (tag,s1)) (TaggedSet (tag',s2)) -> + let Refl = assert_map_tag_eq tag tag' in + let (module V) = get_map tag in + tag_set tag (V.S.inter s1 s2) -let () = define2 "fset_diff" set_repr set_repr - begin fun (TaggedSet (tag,s1)) (TaggedSet (tag',s2)) -> - let Refl = assert_map_tag_eq tag tag' in - let module V = (val get_map tag) in - let open V in - return (tag_set tag (S.diff s1 s2)) - end +let () = + define "fset_diff" (set_repr @-> set_repr @-> ret valexpr) + @@ fun (TaggedSet (tag,s1)) (TaggedSet (tag',s2)) -> + let Refl = assert_map_tag_eq tag tag' in + let (module V) = get_map tag in + tag_set tag (V.S.diff s1 s2) -let () = define2 "fset_equal" set_repr set_repr - begin fun (TaggedSet (tag,s1)) (TaggedSet (tag',s2)) -> - let Refl = assert_map_tag_eq tag tag' in - let module V = (val get_map tag) in - let open V in - return (Value.of_bool (S.equal s1 s2)) - end +let () = + define "fset_equal" (set_repr @-> set_repr @-> ret bool) + @@ fun (TaggedSet (tag,s1)) (TaggedSet (tag',s2)) -> + let Refl = assert_map_tag_eq tag tag' in + let (module V) = get_map tag in + V.S.equal s1 s2 -let () = define2 "fset_subset" set_repr set_repr - begin fun (TaggedSet (tag,s1)) (TaggedSet (tag',s2)) -> - let Refl = assert_map_tag_eq tag tag' in - let module V = (val get_map tag) in - let open V in - return (Value.of_bool (S.subset s1 s2)) - end +let () = + define "fset_subset" (set_repr @-> set_repr @-> ret bool) + @@ fun (TaggedSet (tag,s1)) (TaggedSet (tag',s2)) -> + let Refl = assert_map_tag_eq tag tag' in + let (module V) = get_map tag in + V.S.subset s1 s2 -let () = define1 "fset_cardinal" set_repr begin fun (TaggedSet (tag,s)) -> - let module V = (val get_map tag) in - let open V in - return (Value.of_int (S.cardinal s)) - end +let () = + define "fset_cardinal" (set_repr @-> ret int) @@ fun (TaggedSet (tag,s)) -> + let (module V) = get_map tag in + V.S.cardinal s -let () = define1 "fset_elements" set_repr begin fun (TaggedSet (tag,s)) -> - let module V = (val get_map tag) in - let open V in - return (Value.of_list (repr_of repr) (S.elements s)) - end +let () = + define "fset_elements" (set_repr @-> ret valexpr) @@ fun (TaggedSet (tag,s)) -> + let (module V) = get_map tag in + Value.of_list (repr_of V.repr) (V.S.elements s) -let () = define1 "fmap_empty" map_tag_repr begin fun (Any (tag)) -> - let module V = (val get_map tag) in - let open V in - let Refl = valmap_eq in - return (tag_map tag M.empty) - end +let () = + define "fmap_empty" (map_tag_repr @-> ret valexpr) @@ fun (Any (tag)) -> + let (module V) = get_map tag in + let Refl = V.valmap_eq in + tag_map tag V.M.empty -let () = define1 "fmap_is_empty" map_repr begin fun (TaggedMap (tag,m)) -> - let module V = (val get_map tag) in - let open V in - let Refl = valmap_eq in - return (Value.of_bool (M.is_empty m)) - end +let () = + define "fmap_is_empty" (map_repr @-> ret bool) @@ fun (TaggedMap (tag,m)) -> + let (module V) = get_map tag in + let Refl = V.valmap_eq in + V.M.is_empty m -let () = define2 "fmap_mem" valexpr map_repr begin fun x (TaggedMap (tag,m)) -> - let module V = (val get_map tag) in - let open V in - let Refl = valmap_eq in - let x = repr_to repr x in - return (Value.of_bool (M.mem x m)) - end +let () = + define "fmap_mem" (valexpr @-> map_repr @-> ret bool) @@ fun x (TaggedMap (tag,m)) -> + let (module V) = get_map tag in + let Refl = V.valmap_eq in + V.M.mem (repr_to V.repr x) m -let () = define3 "fmap_add" valexpr valexpr map_repr begin fun x v (TaggedMap (tag,m)) -> - let module V = (val get_map tag) in - let open V in - let Refl = valmap_eq in - let x = repr_to repr x in - return (tag_map tag (M.add x v m)) - end +let () = + define "fmap_add" (valexpr @-> valexpr @-> map_repr @-> ret valexpr) + @@ fun x v (TaggedMap (tag,m)) -> + let (module V) = get_map tag in + let Refl = V.valmap_eq in + tag_map tag (V.M.add (repr_to V.repr x) v m) -let () = define2 "fmap_remove" valexpr map_repr begin fun x (TaggedMap (tag,m)) -> - let module V = (val get_map tag) in - let open V in - let Refl = valmap_eq in - let x = repr_to repr x in - return (tag_map tag (M.remove x m)) - end +let () = + define "fmap_remove" (valexpr @-> map_repr @-> ret valexpr) + @@ fun x (TaggedMap (tag,m)) -> + let (module V) = get_map tag in + let Refl = V.valmap_eq in + tag_map tag (V.M.remove (repr_to V.repr x) m) -let () = define2 "fmap_find_opt" valexpr map_repr begin fun x (TaggedMap (tag,m)) -> - let module V = (val get_map tag) in - let open V in - let Refl = valmap_eq in - let x = repr_to repr x in - return (Value.of_option (fun v -> v) (M.find_opt x m)) - end +let () = + define "fmap_find_opt" (valexpr @-> map_repr @-> ret (option valexpr)) + @@ fun x (TaggedMap (tag,m)) -> + let (module V) = get_map tag in + let Refl = V.valmap_eq in + V.M.find_opt (repr_to V.repr x) m -let () = define2 "fmap_mapi" closure map_repr begin fun f (TaggedMap (tag,m)) -> - let module V = (val get_map tag) in - let open V in - let Refl = valmap_eq in - let module Monadic = M.Monad(Proofview.Monad) in - Monadic.mapi (fun k v -> apply f [repr_of repr k;v]) m >>= fun m -> - return (tag_map tag m) - end +let () = + define "fmap_mapi" (closure @-> map_repr @-> tac valexpr) + @@ fun f (TaggedMap (tag,m)) -> + let (module V) = get_map tag in + let Refl = V.valmap_eq in + let module Monadic = V.M.Monad(Proofview.Monad) in + Monadic.mapi (fun k v -> apply f [repr_of V.repr k;v]) m >>= fun m -> + return (tag_map tag m) -let () = define3 "fmap_fold" closure map_repr valexpr begin fun f (TaggedMap (tag,m)) acc -> - let module V = (val get_map tag) in - let open V in - let Refl = valmap_eq in - let module Monadic = M.Monad(Proofview.Monad) in - Monadic.fold (fun k v acc -> apply f [repr_of repr k;v;acc]) m acc - end +let () = + define "fmap_fold" (closure @-> map_repr @-> valexpr @-> tac valexpr) + @@ fun f (TaggedMap (tag,m)) acc -> + let (module V) = get_map tag in + let Refl = V.valmap_eq in + let module Monadic = V.M.Monad(Proofview.Monad) in + Monadic.fold (fun k v acc -> apply f [repr_of V.repr k;v;acc]) m acc -let () = define1 "fmap_cardinal" map_repr begin fun (TaggedMap (tag,m)) -> - let module V = (val get_map tag) in - let open V in - let Refl = valmap_eq in - return (Value.of_int (M.cardinal m)) - end +let () = + define "fmap_cardinal" (map_repr @-> ret int) @@ fun (TaggedMap (tag,m)) -> + let (module V) = get_map tag in + let Refl = V.valmap_eq in + V.M.cardinal m -let () = define1 "fmap_bindings" map_repr begin fun (TaggedMap (tag,m)) -> - let module V = (val get_map tag) in - let open V in - let Refl = valmap_eq in - return (Value.(of_list (of_pair (repr_of repr) identity) (M.bindings m))) - end +let () = + define "fmap_bindings" (map_repr @-> ret valexpr) @@ fun (TaggedMap (tag,m)) -> + let (module V) = get_map tag in + let Refl = V.valmap_eq in + Value.(of_list (of_pair (repr_of V.repr) identity) (V.M.bindings m)) -let () = define1 "fmap_domain" map_repr begin fun (TaggedMap (tag,m)) -> - let module V = (val get_map tag) in - let open V in - let Refl = valmap_eq in - return (tag_set tag (M.domain m)) - end +let () = + define "fmap_domain" (map_repr @-> ret valexpr) @@ fun (TaggedMap (tag,m)) -> + let (module V) = get_map tag in + let Refl = V.valmap_eq in + tag_set tag (V.M.domain m) (** ML types *) @@ -2066,14 +1902,13 @@ let () = Ftactic.return ans in let () = Geninterp.register_interp0 wit_ltac2_val interp_fun in - define1 "ltac1_lambda" valexpr begin fun f -> - let body = Tacexpr.TacGeneric (Some ltac2_plugin, in_gen (glbwit wit_ltac2_val) ()) in - let clos = CAst.make (Tacexpr.TacFun ([Name arg_id], CAst.make (Tacexpr.TacArg body))) in - let f = Geninterp.Val.inject (Geninterp.Val.Base typ_ltac2) f in - let lfun = Id.Map.singleton tac_id f in - let ist = { (Tacinterp.default_ist ()) with Tacinterp.lfun } in - Proofview.tclUNIT (of_ltac1 (Tacinterp.Value.of_closure ist clos)) - end + define "ltac1_lambda" (valexpr @-> ret ltac1) @@ fun f -> + let body = Tacexpr.TacGeneric (Some ltac2_plugin, in_gen (glbwit wit_ltac2_val) ()) in + let clos = CAst.make (Tacexpr.TacFun ([Name arg_id], CAst.make (Tacexpr.TacArg body))) in + let f = Geninterp.Val.inject (Geninterp.Val.Base typ_ltac2) f in + let lfun = Id.Map.singleton tac_id f in + let ist = { (Tacinterp.default_ist ()) with Tacinterp.lfun } in + Tacinterp.Value.of_closure ist clos let ltac2_eval = let open Ltac_plugin in diff --git a/plugins/ltac2/tac2stdlib.ml b/plugins/ltac2/tac2stdlib.ml index 708b0851e3ce..3d420bc122d2 100644 --- a/plugins/ltac2/tac2stdlib.ml +++ b/plugins/ltac2/tac2stdlib.ml @@ -22,7 +22,6 @@ module Value = Tac2ffi let make_to_repr f = Tac2ffi.make_repr (fun _ -> assert false) f let return x = Proofview.tclUNIT x -let v_unit = Value.of_unit () let thaw r f = Tac2ffi.app_fun1 f unit r () let uthaw r f = Tac2ffi.app_fun1 (to_fun1 unit r f) unit r () let thunk r = fun1 unit r @@ -213,76 +212,68 @@ let generalize_arg = make_to_repr to_generalize_arg (** Standard tactics sharing their implementation with Ltac1 *) -let pname s = { mltac_plugin = "coq-core.plugins.ltac2"; mltac_tactic = s } +open Tac2externals -let lift tac = tac <*> return v_unit - -let define_prim0 name tac = - let tac _ = lift tac in - Tac2env.define_primitive (pname name) (mk_closure_val arity_one tac) - -let define_prim1 name r0 f = - let tac x = lift (f (Value.repr_to r0 x)) in - Tac2env.define_primitive (pname name) (mk_closure_val arity_one tac) - -let define_prim2 name r0 r1 f = - let tac x y = lift (f (Value.repr_to r0 x) (Value.repr_to r1 y)) in - Tac2env.define_primitive (pname name) (mk_closure_val (arity_suc arity_one) tac) - -let define_prim3 name r0 r1 r2 f = - let tac x y z = lift (f (Value.repr_to r0 x) (Value.repr_to r1 y) (Value.repr_to r2 z)) in - Tac2env.define_primitive (pname name) (mk_closure_val (arity_suc (arity_suc arity_one)) tac) - -let define_prim4 name r0 r1 r2 r3 f = - let tac x y z u = lift (f (Value.repr_to r0 x) (Value.repr_to r1 y) (Value.repr_to r2 z) (Value.repr_to r3 u)) in - Tac2env.define_primitive (pname name) (mk_closure_val (arity_suc (arity_suc (arity_suc arity_one))) tac) - -let define_prim5 name r0 r1 r2 r3 r4 f = - let tac x y z u v = lift (f (Value.repr_to r0 x) (Value.repr_to r1 y) (Value.repr_to r2 z) (Value.repr_to r3 u) (Value.repr_to r4 v)) in - Tac2env.define_primitive (pname name) (mk_closure_val (arity_suc (arity_suc (arity_suc (arity_suc arity_one)))) tac) +let define s = + define { mltac_plugin = "coq-core.plugins.ltac2"; mltac_tactic = s } (** Tactics from Tacexpr *) -let () = define_prim2 "tac_intros" bool intro_patterns begin fun ev ipat -> - Tac2tactics.intros_patterns ev ipat -end +let () = + define "tac_intros" + (bool @-> intro_patterns @-> tac unit) + Tac2tactics.intros_patterns -let () = define_prim4 "tac_apply" bool bool (list (thunk constr_with_bindings)) (option (pair ident (option intro_pattern))) begin fun adv ev cb ipat -> - Tac2tactics.apply adv ev cb ipat -end +let () = + define "tac_apply" + (bool @-> bool @-> list (thunk constr_with_bindings) @-> + option (pair ident (option intro_pattern)) @-> tac unit) + Tac2tactics.apply -let () = define_prim3 "tac_elim" bool constr_with_bindings (option constr_with_bindings) begin fun ev c copt -> - Tac2tactics.elim ev c copt -end +let () = + define "tac_elim" + (bool @-> constr_with_bindings @-> option constr_with_bindings @-> tac unit) + Tac2tactics.elim -let () = define_prim2 "tac_case" bool constr_with_bindings begin fun ev c -> - Tac2tactics.general_case_analysis ev c -end +let () = + define "tac_case" + (bool @-> constr_with_bindings @-> tac unit) + Tac2tactics.general_case_analysis -let () = define_prim1 "tac_generalize" (list generalize_arg) begin fun cl -> - Tac2tactics.generalize cl -end +let () = + define "tac_generalize" + (list generalize_arg @-> tac unit) + Tac2tactics.generalize -let () = define_prim1 "tac_assert" assertion begin fun ast -> - Tac2tactics.assert_ ast -end +let () = + define "tac_assert" + (assertion @-> tac unit) + Tac2tactics.assert_ -let () = define_prim3 "tac_enough" constr (option (option (thunk unit))) (option intro_pattern) begin fun c tac ipat -> +let tac_enough c tac ipat = let tac = Option.map (fun o -> Option.map (fun f -> thaw unit f) o) tac in Tac2tactics.forward false tac ipat c -end +let () = + define "tac_enough" + (constr @-> option (option (thunk unit)) @-> option intro_pattern @-> tac unit) + tac_enough -let () = define_prim2 "tac_pose" name constr begin fun na c -> - Tactics.letin_tac None na c None Locusops.nowhere -end +let tac_pose na c = Tactics.letin_tac None na c None Locusops.nowhere +let () = + define "tac_pose" + (name @-> constr @-> tac unit) + tac_pose -let () = define_prim3 "tac_set" bool (thunk (pair name constr)) clause begin fun ev p cl -> +let tac_set ev p cl = Proofview.tclEVARMAP >>= fun sigma -> thaw (pair name constr) p >>= fun (na, c) -> Tac2tactics.letin_pat_tac ev None na (Some sigma, c) cl -end +let () = + define "tac_set" + (bool @-> thunk (pair name constr) @-> clause @-> tac unit) + tac_set -let () = define_prim5 "tac_remember" bool name (thunk constr) (option intro_pattern) clause begin fun ev na c eqpat cl -> +let tac_remember ev na c eqpat cl = let eqpat = Option.default (IntroNaming IntroAnonymous) eqpat in match eqpat with | IntroNaming eqpat -> @@ -291,144 +282,140 @@ let () = define_prim5 "tac_remember" bool name (thunk constr) (option intro_patt Tac2tactics.letin_pat_tac ev (Some (true, eqpat)) na (Some sigma, c) cl | _ -> Tacticals.tclZEROMSG (Pp.str "Invalid pattern for remember") -end +let () = + define "tac_remember" + (bool @-> name @-> thunk constr @-> option intro_pattern @-> clause @-> tac unit) + tac_remember -let () = define_prim3 "tac_destruct" bool (list induction_clause) (option constr_with_bindings) begin fun ev ic using -> - Tac2tactics.induction_destruct false ev ic using -end +let () = + define "tac_destruct" + (bool @-> list induction_clause @-> option constr_with_bindings @-> tac unit) + (Tac2tactics.induction_destruct false) -let () = define_prim3 "tac_induction" bool (list induction_clause) (option constr_with_bindings) begin fun ev ic using -> - Tac2tactics.induction_destruct true ev ic using -end +let () = + define "tac_induction" + (bool @-> list induction_clause @-> option constr_with_bindings @-> tac unit) + (Tac2tactics.induction_destruct true) -let () = define_prim1 "tac_red" clause begin fun cl -> - Tac2tactics.reduce (Red false) cl -end +let () = + define "tac_red" (clause @-> tac unit) (Tac2tactics.reduce (Red false)) -let () = define_prim1 "tac_hnf" clause begin fun cl -> - Tac2tactics.reduce Hnf cl -end +let () = + define "tac_hnf" (clause @-> tac unit) (Tac2tactics.reduce Hnf) -let () = define_prim3 "tac_simpl" red_flags (option pattern_with_occs) clause begin fun flags where cl -> - Tac2tactics.simpl flags where cl -end +let () = + define "tac_simpl" + (red_flags @-> option pattern_with_occs @-> clause @-> tac unit) + Tac2tactics.simpl -let () = define_prim2 "tac_cbv" red_flags clause begin fun flags cl -> - Tac2tactics.cbv flags cl -end +let () = + define "tac_cbv" (red_flags @-> clause @-> tac unit) Tac2tactics.cbv -let () = define_prim2 "tac_cbn" red_flags clause begin fun flags cl -> - Tac2tactics.cbn flags cl -end +let () = + define "tac_cbn" (red_flags @-> clause @-> tac unit) Tac2tactics.cbn -let () = define_prim2 "tac_lazy" red_flags clause begin fun flags cl -> - Tac2tactics.lazy_ flags cl -end +let () = + define "tac_lazy" (red_flags @-> clause @-> tac unit) Tac2tactics.lazy_ -let () = define_prim2 "tac_unfold" (list reference_with_occs) clause begin fun refs cl -> - Tac2tactics.unfold refs cl -end +let () = + define "tac_unfold" + (list reference_with_occs @-> clause @-> tac unit) + Tac2tactics.unfold -let () = define_prim2 "tac_fold" (list constr) clause begin fun args cl -> - Tac2tactics.reduce (Fold args) cl -end +let () = + define "tac_fold" + (list constr @-> clause @-> tac unit) + (fun args cl -> Tac2tactics.reduce (Fold args) cl) -let () = define_prim2 "tac_pattern" (list constr_with_occs) clause begin fun where cl -> - Tac2tactics.pattern where cl -end +let () = + define "tac_pattern" + (list constr_with_occs @-> clause @-> tac unit) + Tac2tactics.pattern -let () = define_prim2 "tac_vm" (option pattern_with_occs) clause begin fun where cl -> - Tac2tactics.vm where cl -end +let () = + define "tac_vm" + (option pattern_with_occs @-> clause @-> tac unit) + Tac2tactics.vm -let () = define_prim2 "tac_native" (option pattern_with_occs) clause begin fun where cl -> - Tac2tactics.native where cl -end +let () = + define "tac_native" + (option pattern_with_occs @-> clause @-> tac unit) + Tac2tactics.native (** Reduction functions *) -let lift tac = tac >>= fun c -> Proofview.tclUNIT (Value.of_constr c) - -let define_red1 name r0 f = - let tac x = lift (f (Value.repr_to r0 x)) in - Tac2env.define_primitive (pname name) (mk_closure_val arity_one tac) - -let define_red2 name r0 r1 f = - let tac x y = lift (f (Value.repr_to r0 x) (Value.repr_to r1 y)) in - Tac2env.define_primitive (pname name) (mk_closure_val (arity_suc arity_one) tac) - -let define_red3 name r0 r1 r2 f = - let tac x y z = lift (f (Value.repr_to r0 x) (Value.repr_to r1 y) (Value.repr_to r2 z)) in - Tac2env.define_primitive (pname name) (mk_closure_val (arity_suc (arity_suc arity_one)) tac) - -let () = define_red1 "eval_red" constr begin fun c -> - Tac2tactics.eval_red c -end +let () = define "eval_red" (constr @-> tac constr) Tac2tactics.eval_red -let () = define_red1 "eval_hnf" constr begin fun c -> - Tac2tactics.eval_hnf c -end +let () = define "eval_hnf" (constr @-> tac constr) Tac2tactics.eval_hnf -let () = define_red3 "eval_simpl" red_flags (option pattern_with_occs) constr begin fun flags where c -> - Tac2tactics.eval_simpl flags where c -end +let () = + define "eval_simpl" + (red_flags @-> option pattern_with_occs @-> constr @-> tac constr) + Tac2tactics.eval_simpl -let () = define_red2 "eval_cbv" red_flags constr begin fun flags c -> - Tac2tactics.eval_cbv flags c -end +let () = + define "eval_cbv" (red_flags @-> constr @-> tac constr) Tac2tactics.eval_cbv -let () = define_red2 "eval_cbn" red_flags constr begin fun flags c -> - Tac2tactics.eval_cbn flags c -end +let () = + define "eval_cbn" (red_flags @-> constr @-> tac constr) Tac2tactics.eval_cbn -let () = define_red2 "eval_lazy" red_flags constr begin fun flags c -> - Tac2tactics.eval_lazy flags c -end +let () = + define "eval_lazy" (red_flags @-> constr @-> tac constr) Tac2tactics.eval_lazy -let () = define_red2 "eval_unfold" (list reference_with_occs) constr begin fun refs c -> - Tac2tactics.eval_unfold refs c -end +let () = + define "eval_unfold" + (list reference_with_occs @-> constr @-> tac constr) + Tac2tactics.eval_unfold -let () = define_red2 "eval_fold" (list constr) constr begin fun args c -> - Tac2tactics.eval_fold args c -end +let () = + define "eval_fold" + (list constr @-> constr @-> tac constr) + Tac2tactics.eval_fold -let () = define_red2 "eval_pattern" (list constr_with_occs) constr begin fun where c -> - Tac2tactics.eval_pattern where c -end +let () = + define "eval_pattern" + (list constr_with_occs @-> constr @-> tac constr) + Tac2tactics.eval_pattern -let () = define_red2 "eval_vm" (option pattern_with_occs) constr begin fun where c -> - Tac2tactics.eval_vm where c -end +let () = + define "eval_vm" + (option pattern_with_occs @-> constr @-> tac constr) + Tac2tactics.eval_vm -let () = define_red2 "eval_native" (option pattern_with_occs) constr begin fun where c -> - Tac2tactics.eval_native where c -end +let () = + define "eval_native" + (option pattern_with_occs @-> constr @-> tac constr) + Tac2tactics.eval_native -let () = define_prim3 "tac_change" (option pattern) (fun1 (array constr) constr) clause begin fun pat c cl -> - Tac2tactics.change pat c cl -end +let () = + define "tac_change" + (option pattern @-> fun1 (array constr) constr @-> clause @-> tac unit) + Tac2tactics.change -let () = define_prim4 "tac_rewrite" bool (list rewriting) clause (option (thunk unit)) begin fun ev rw cl by -> - Tac2tactics.rewrite ev rw cl by -end +let () = + define "tac_rewrite" + (bool @-> list rewriting @-> clause @-> option (thunk unit) @-> tac unit) + Tac2tactics.rewrite -let () = define_prim4 "tac_inversion" inversion_kind destruction_arg (option intro_pattern) (option (list ident)) begin fun knd arg pat ids -> - Tac2tactics.inversion knd arg pat ids -end +let () = + define "tac_inversion" + (inversion_kind @-> destruction_arg @-> option intro_pattern @-> + option (list ident) @-> tac unit) + Tac2tactics.inversion (** Tactics from coretactics *) -let () = define_prim0 "tac_reflexivity" Tactics.intros_reflexivity +let () = + define "tac_reflexivity" (unit @-> tac unit) (fun _ -> Tactics.intros_reflexivity) -let () = define_prim2 "tac_move" ident move_location begin fun id mv -> - Tactics.move_hyp id mv -end +let () = + define "tac_move" (ident @-> move_location @-> tac unit) Tactics.move_hyp -let () = define_prim2 "tac_intro" (option ident) (option move_location) begin fun id mv -> +let tac_intro id mv = let mv = Option.default Logic.MoveLast mv in Tactics.intro_move id mv -end +let () = + define "tac_intro" (option ident @-> option move_location @-> tac unit) tac_intro (* @@ -438,162 +425,159 @@ END *) -let () = define_prim0 "tac_assumption" Tactics.assumption +let () = + define "tac_assumption" (unit @-> tac unit) (fun _ -> Tactics.assumption) -let () = define_prim1 "tac_transitivity" constr begin fun c -> - Tactics.intros_transitivity (Some c) -end +let () = + define "tac_transitivity" (constr @-> tac unit) + (fun c -> Tactics.intros_transitivity (Some c)) -let () = define_prim0 "tac_etransitivity" (Tactics.intros_transitivity None) +let () = + define "tac_etransitivity" (unit @-> tac unit) + (fun _ -> Tactics.intros_transitivity None) -let () = define_prim1 "tac_cut" constr begin fun c -> - Tactics.cut c -end +let () = + define "tac_cut" (constr @-> tac unit) Tactics.cut -let () = define_prim2 "tac_left" bool bindings begin fun ev bnd -> - Tac2tactics.left_with_bindings ev bnd -end -let () = define_prim2 "tac_right" bool bindings begin fun ev bnd -> - Tac2tactics.right_with_bindings ev bnd -end +let () = + define "tac_left" (bool @-> bindings @-> tac unit) Tac2tactics.left_with_bindings -let () = define_prim1 "tac_introsuntil" qhyp begin fun h -> - Tactics.intros_until h -end +let () = + define "tac_right" (bool @-> bindings @-> tac unit) Tac2tactics.right_with_bindings -let () = define_prim1 "tac_exactnocheck" constr begin fun c -> - Tactics.exact_no_check c -end +let () = + define "tac_introsuntil" (qhyp @-> tac unit) Tactics.intros_until -let () = define_prim1 "tac_vmcastnocheck" constr begin fun c -> - Tactics.vm_cast_no_check c -end +let () = + define "tac_exactnocheck" (constr @-> tac unit) Tactics.exact_no_check -let () = define_prim1 "tac_nativecastnocheck" constr begin fun c -> - Tactics.native_cast_no_check c -end +let () = + define "tac_vmcastnocheck" (constr @-> tac unit) Tactics.vm_cast_no_check -let () = define_prim1 "tac_constructor" bool begin fun ev -> - Tactics.any_constructor ev None -end +let () = + define "tac_nativecastnocheck" (constr @-> tac unit) Tactics.native_cast_no_check -let () = define_prim3 "tac_constructorn" bool int bindings begin fun ev n bnd -> - Tac2tactics.constructor_tac ev None n bnd -end +let () = + define "tac_constructor" (bool @-> tac unit) (fun ev -> Tactics.any_constructor ev None) -let () = define_prim2 "tac_specialize" constr_with_bindings (option intro_pattern) begin fun c ipat -> - Tac2tactics.specialize c ipat -end +let () = + define "tac_constructorn" (bool @-> int @-> bindings @-> tac unit) + (fun ev n bnd -> Tac2tactics.constructor_tac ev None n bnd) -let () = define_prim1 "tac_symmetry" clause begin fun cl -> - Tac2tactics.symmetry cl -end +let () = + define "tac_specialize" + (constr_with_bindings @-> option intro_pattern @-> tac unit) + Tac2tactics.specialize -let () = define_prim2 "tac_split" bool bindings begin fun ev bnd -> - Tac2tactics.split_with_bindings ev bnd -end +let () = + define "tac_symmetry" (clause @-> tac unit) Tac2tactics.symmetry -let () = define_prim1 "tac_rename" (list (pair ident ident)) begin fun ids -> - Tactics.rename_hyp ids -end +let () = + define "tac_split" (bool @-> bindings @-> tac unit) Tac2tactics.split_with_bindings -let () = define_prim1 "tac_revert" (list ident) begin fun ids -> - Generalize.revert ids -end +let () = + define "tac_rename" (list (pair ident ident) @-> tac unit) Tactics.rename_hyp -let () = define_prim0 "tac_admit" Proofview.give_up +let () = + define "tac_revert" (list ident @-> tac unit) Generalize.revert -let () = define_prim2 "tac_fix" ident int begin fun ident n -> - Tactics.fix ident n -end +let () = + define "tac_admit" (unit @-> tac unit) (fun _ -> Proofview.give_up) -let () = define_prim1 "tac_cofix" ident begin fun ident -> - Tactics.cofix ident -end +let () = + define "tac_fix" (ident @-> int @-> tac unit) Tactics.fix + +let () = + define "tac_cofix" (ident @-> tac unit) Tactics.cofix -let () = define_prim1 "tac_clear" (list ident) begin fun ids -> - Tactics.clear ids -end +let () = + define "tac_clear" (list ident @-> tac unit) Tactics.clear -let () = define_prim1 "tac_keep" (list ident) begin fun ids -> - Tactics.keep ids -end +let () = + define "tac_keep" (list ident @-> tac unit) Tactics.keep -let () = define_prim1 "tac_clearbody" (list ident) begin fun ids -> - Tactics.clear_body ids -end +let () = + define "tac_clearbody" (list ident @-> tac unit) Tactics.clear_body (** Tactics from extratactics *) -let () = define_prim2 "tac_discriminate" bool (option destruction_arg) begin fun ev arg -> - Tac2tactics.discriminate ev arg -end +let () = + define "tac_discriminate" + (bool @-> option destruction_arg @-> tac unit) + Tac2tactics.discriminate -let () = define_prim3 "tac_injection" bool (option intro_patterns) (option destruction_arg) begin fun ev ipat arg -> - Tac2tactics.injection ev ipat arg -end +let () = + define "tac_injection" + (bool @-> option intro_patterns @-> option destruction_arg @-> tac unit) + Tac2tactics.injection -let () = define_prim1 "tac_absurd" constr begin fun c -> - Contradiction.absurd c -end +let () = + define "tac_absurd" (constr @-> tac unit) Contradiction.absurd -let () = define_prim1 "tac_contradiction" (option constr_with_bindings) begin fun c -> - Tac2tactics.contradiction c -end +let () = + define "tac_contradiction" + (option constr_with_bindings @-> tac unit) + Tac2tactics.contradiction -let () = define_prim4 "tac_autorewrite" bool (option (thunk unit)) (list ident) clause begin fun all by ids cl -> - Tac2tactics.autorewrite ~all by ids cl -end +let () = + define "tac_autorewrite" + (bool @-> option (thunk unit) @-> list ident @-> clause @-> tac unit) + (fun all by ids cl -> Tac2tactics.autorewrite ~all by ids cl) -let () = define_prim1 "tac_subst" (list ident) begin fun ids -> - Equality.subst ids -end +let () = + define "tac_subst" (list ident @-> tac unit) Equality.subst -let () = define_prim0 "tac_substall" (return () >>= fun () -> Equality.subst_all ()) +let () = + define "tac_substall" + (unit @-> tac unit) + (fun _ -> return () >>= fun () -> Equality.subst_all ()) (** Auto *) -let () = define_prim3 "tac_trivial" debug (list (thunk constr)) (option (list ident)) begin fun dbg lems dbs -> - Tac2tactics.trivial dbg lems dbs -end +let () = + define "tac_trivial" + (debug @-> list (thunk constr) @-> option (list ident) @-> tac unit) + Tac2tactics.trivial -let () = define_prim4 "tac_eauto" debug (option int) (list (thunk constr)) (option (list ident)) begin fun dbg n lems dbs -> - Tac2tactics.eauto dbg n lems dbs -end +let () = + define "tac_eauto" + (debug @-> option int @-> list (thunk constr) @-> option (list ident) @-> tac unit) + Tac2tactics.eauto -let () = define_prim4 "tac_auto" debug (option int) (list (thunk constr)) (option (list ident)) begin fun dbg n lems dbs -> - Tac2tactics.auto dbg n lems dbs -end +let () = + define "tac_auto" + (debug @-> option int @-> list (thunk constr) @-> option (list ident) @-> tac unit) + Tac2tactics.auto -let () = define_prim3 "tac_typeclasses_eauto" (option strategy) (option int) (option (list ident)) begin fun str n dbs -> - Tac2tactics.typeclasses_eauto str n dbs -end +let () = + define "tac_typeclasses_eauto" + (option strategy @-> option int @-> option (list ident) @-> tac unit) + Tac2tactics.typeclasses_eauto -let () = define_prim1 "tac_resolve_tc" constr Class_tactics.resolve_tc +let () = + define "tac_resolve_tc" (constr @-> tac unit) Class_tactics.resolve_tc -let () = define_prim2 "tac_unify" constr constr begin fun x y -> - Tac2tactics.unify x y -end +let () = + define "tac_unify" (constr @-> constr @-> tac unit) Tac2tactics.unify (** Tactics for [Ltac2/TransparentState.v]. *) let transparent_state = Tac2ffi.repr_ext Tac2ffi.val_transparent_state let () = - let tac _ = - Tac2tactics.current_transparent_state () >>= fun ts -> - return (Tac2ffi.of_ext Tac2ffi.val_transparent_state ts) - in - Tac2env.define_primitive (pname "current_transparent_state") (mk_closure_val arity_one tac) + define "current_transparent_state" + (unit @-> tac transparent_state) + Tac2tactics.current_transparent_state let () = - let v = Tac2ffi.of_ext Tac2ffi.val_transparent_state TransparentState.full in - Tac2env.define_primitive (pname "full_transparent_state") v + define "full_transparent_state" (ret transparent_state) TransparentState.full let () = - let v = Tac2ffi.of_ext Tac2ffi.val_transparent_state TransparentState.empty in - Tac2env.define_primitive (pname "empty_transparent_state") v + define "empty_transparent_state" (ret transparent_state) TransparentState.empty (** Tactics around Evarconv unification (in [Ltac2/Unification.v]). *) -let () = define_prim3 "evarconv_unify" transparent_state constr constr Tac2tactics.evarconv_unify +let () = + define "evarconv_unify" + (transparent_state @-> constr @-> constr @-> tac unit) + Tac2tactics.evarconv_unify