diff --git a/plugins/ltac2/tac2core.ml b/plugins/ltac2/tac2core.ml index 365f09917ab8..2354f772fbc3 100644 --- a/plugins/ltac2/tac2core.ml +++ b/plugins/ltac2/tac2core.ml @@ -19,6 +19,8 @@ open Tac2expr open Tac2entries.Pltac open Proofview.Notations +module GT = Tac2globals.Types + let ltac2_plugin = "coq-core.plugins.ltac2" let constr_flags = @@ -72,7 +74,10 @@ let preterm_flags = (** Standard values *) let val_format = Tac2print.val_format -let format = repr_ext val_format +let format_ = repr_ext val_format +let format t1 t2 t3 t4 = + typed format_ + Types.(! GT.format [t1; t2; t3; t4]) let core_prefix path n = KerName.make path (Label.of_id (Id.of_string_soft n)) @@ -125,7 +130,8 @@ let to_relevance = function Sorts.RelevanceVar qvar | _ -> assert false -let relevance = make_repr of_relevance to_relevance +let relevance_ = make_repr of_relevance to_relevance +let relevance = typed relevance_ Types.(!! GT.relevance) let of_binder b = Tac2ffi.of_ext Tac2ffi.val_binder b @@ -168,13 +174,11 @@ let to_case_invert = let open Constr in function CaseInvert {indices} | _ -> CErrors.anomaly Pp.(str "unexpected value shape") -let of_result f = function -| Inl c -> v_blk 0 [|f c|] -| Inr e -> v_blk 1 [|Tac2ffi.of_exn e|] - -let inductive = repr_ext val_inductive +let inductive_ = repr_ext val_inductive +let inductive = typed inductive_ Types.(!! GT.inductive) -let projection = repr_ext val_projection +let projection_ = repr_ext val_projection +let projection = typed projection_ Types.(!! GT.projection) (** Stdlib exceptions *) @@ -195,8 +199,6 @@ let err_division_by_zero = (** Helper functions *) -let thaw f = Tac2val.apply f [v_unit] - let fatal_flag : unit Exninfo.t = Exninfo.make "fatal_flag" let has_fatal_flag info = match Exninfo.get info fatal_flag with @@ -280,35 +282,44 @@ let () = let () = define "message_of_ident" (ident @-> ret pp) Id.print let () = - define "message_of_exn" (valexpr @-> eret pp) @@ fun v env sigma -> + define "message_of_exn" (valexpr_0 @-> eret pp) @@ fun v env sigma -> Tac2print.pr_valexpr env sigma v (GTypRef (Other Core.t_exn, [])) let () = define "message_concat" (pp @-> pp @-> ret pp) Pp.app -let () = define "format_stop" (ret format) [] +let () = define "format_stop" (ret Types.(format any any any any)) [] + +let format_linear_spec = + Types.(format (var 0) (var 1) (var 2) (var 3)) + +let format_one_arg_spec argty = + format_linear_spec + @-> ret Types.(format (argty @-> var 0) (var 1) (var 2) (var 3)) let () = - define "format_string" (format @-> ret format) @@ fun s -> + define "format_string" (format_one_arg_spec Types.(!! GT.string)) @@ fun s -> Tac2print.FmtString :: s let () = - define "format_int" (format @-> ret format) @@ fun s -> + define "format_int" (format_one_arg_spec Types.(!! GT.int)) @@ fun s -> Tac2print.FmtInt :: s let () = - define "format_constr" (format @-> ret format) @@ fun s -> + define "format_constr" (format_one_arg_spec Types.(!! GT.constr)) @@ fun s -> Tac2print.FmtConstr :: s let () = - define "format_ident" (format @-> ret format) @@ fun s -> + define "format_ident" (format_one_arg_spec Types.(!! GT.ident)) @@ fun s -> Tac2print.FmtIdent :: s let () = - define "format_literal" (string @-> format @-> ret format) @@ fun lit s -> + define "format_literal" (string @-> format_linear_spec @-> ret format_linear_spec) @@ fun lit s -> Tac2print.FmtLiteral lit :: s let () = - define "format_alpha" (format @-> ret format) @@ fun s -> + define "format_alpha" + (format_linear_spec + @-> ret Types.(format ((var 1 @-> var 4 @-> var 2) @-> var 4 @-> var 0) (var 1) (var 2) (var 3))) @@ fun s -> Tac2print.FmtAlpha :: s let arity_of_format fmt = @@ -321,13 +332,16 @@ let arity_of_format fmt = List.fold_left fold 0 fmt let () = - define "format_kfprintf" (closure @-> format @-> tac valexpr) @@ fun k fmt -> + define "format_kfprintf" + (fun1 pp (typed valexpr (Types.var 1)) + @-> Types.(format (var 0) (!! GT.unit) (!! GT.message) (var 1)) + @-> tac valexpr_0) @@ fun k fmt -> let open Tac2print in let pop1 l = match l with [] -> assert false | x :: l -> (x, l) in let pop2 l = match l with [] | [_] -> assert false | x :: y :: l -> (x, y, l) in let arity = arity_of_format fmt in let rec eval accu args fmt = match fmt with - | [] -> apply k [of_pp accu] + | [] -> k accu | tag :: fmt -> match tag with | FmtLiteral s -> @@ -361,7 +375,11 @@ let () = else return (Tac2ffi.of_closure (Tac2val.abstract arity eval)) let () = - define "format_ikfprintf" (closure @-> valexpr @-> format @-> tac valexpr) @@ fun k v fmt -> + define "format_ikfprintf" + (typed closure Types.(var 1 @-> var 2) + @-> typed valexpr (Types.var 1) + @-> Types.(format (var 0) (!! GT.unit) (var 1) (var 2)) + @-> tac valexpr_0) @@ fun k v fmt -> let arity = arity_of_format fmt in let eval _args = apply k [v] in if Int.equal arity 0 then eval [] @@ -369,36 +387,40 @@ let () = (** Array *) -let () = define "array_empty" (ret valexpr) (v_blk 0 [||]) +(* avoid using "array valexpr_0" to avoid useless Array.map in readers + and to avoid making writers write to a copied array *) +let array_ty_0 = Types.(! GT.array [var 0]) + +let () = define "array_empty" (ret (typed valexpr array_ty_0)) (v_blk 0 [||]) let () = - define "array_make" (int @-> valexpr @-> tac valexpr) @@ fun n x -> + define "array_make" (int @-> valexpr_0 @-> tac (typed valexpr array_ty_0)) @@ fun n x -> try return (v_blk 0 (Array.make n x)) with Invalid_argument _ -> throw err_outofbounds let () = - define "array_length" (block @-> ret int) @@ fun (_, v) -> Array.length v + define "array_length" (typed block array_ty_0 @-> ret int) @@ fun (_, v) -> Array.length v let () = - define "array_set" (block @-> int @-> valexpr @-> tac unit) @@ fun (_, v) n x -> + define "array_set" (typed block array_ty_0 @-> int @-> valexpr_0 @-> tac unit) @@ fun (_, v) n x -> try Array.set v n x; return () with Invalid_argument _ -> throw err_outofbounds let () = - define "array_get" (block @-> int @-> tac valexpr) @@ fun (_, v) n -> + define "array_get" (typed block array_ty_0 @-> int @-> tac @@ valexpr_0) @@ fun (_, v) n -> try return (Array.get v n) with Invalid_argument _ -> throw err_outofbounds let () = define "array_blit" - (block @-> int @-> block @-> int @-> int @-> tac unit) + (typed block array_ty_0 @-> int @-> typed block array_ty_0 @-> 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 () = - define "array_fill" (block @-> int @-> int @-> valexpr @-> tac unit) @@ fun (_, d) s l v -> + define "array_fill" (typed block array_ty_0 @-> int @-> int @-> valexpr_0 @-> tac unit) @@ fun (_, d) s l v -> try Array.fill d s l v; return () with Invalid_argument _ -> throw err_outofbounds let () = - define "array_concat" (list block @-> ret valexpr) @@ fun l -> + define "array_concat" (list (typed block array_ty_0) @-> ret (typed valexpr array_ty_0)) @@ fun l -> v_blk 0 (Array.concat (List.map snd l)) (** Ident *) @@ -476,10 +498,9 @@ let () = define "string_compare" (bytes @-> bytes @-> ret int) Bytes.compare (** constr -> constr *) let () = - define "constr_type" (constr @-> tac valexpr) @@ fun c -> + define "constr_type" (constr @-> tac constr) @@ fun c -> let get_type env sigma = let (sigma, t) = Typing.type_of env sigma c in - let t = Tac2ffi.of_constr t in Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclUNIT t in pf_apply ~catch_exceptions:true get_type @@ -490,7 +511,7 @@ let () = Proofview.tclEVARMAP >>= fun sigma -> return (EConstr.eq_constr sigma c1 c2) let () = - define "constr_kind" (constr @-> eret valexpr) @@ fun c env sigma -> + define "constr_kind" (constr @-> eret (typed valexpr Types.(!! GT.constr_kind))) @@ fun c env sigma -> let open Constr in match EConstr.kind sigma c with | Rel n -> @@ -593,7 +614,7 @@ let () = |] let () = - define "constr_make" (valexpr @-> eret constr) @@ fun knd env sigma -> + define "constr_make" (typed valexpr Types.(!! GT.constr_kind) @-> eret constr) @@ fun knd env sigma -> match Tac2ffi.to_block knd with | (0, [|n|]) -> let n = Tac2ffi.to_int n in @@ -681,15 +702,15 @@ let () = | _ -> assert false let () = - define "constr_check" (constr @-> tac valexpr) @@ fun c -> + define "constr_check" (constr @-> tac @@ result constr) @@ 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 Tac2ffi.of_constr (Inl c)) + return (Ok c) with e when CErrors.noncritical e -> let e = Exninfo.capture e in - return (of_result Tac2ffi.of_constr (Inr e)) + return (Error e) let () = define "constr_liftn" (int @-> int @-> constr @-> ret constr) @@ -715,21 +736,24 @@ let () = Proofview.tclEVARMAP >>= fun sigma -> return (EConstr.Vars.noccur_between sigma n m c) +let constr_case_ = repr_ext val_case +let constr_case = typed constr_case_ Types.(!! GT.constr_case) + let () = - define "constr_case" (inductive @-> tac valexpr) @@ fun ind -> + define "constr_case" (inductive @-> tac constr_case) @@ fun ind -> Proofview.tclENV >>= fun env -> try let ans = Inductiveops.make_case_info env ind Constr.RegularStyle in - return (Tac2ffi.of_ext Tac2ffi.val_case ans) + return ans with e when CErrors.noncritical e -> throw err_notfound -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 () = define "constr_cast_default" (ret cast) DEFAULTcast +let () = define "constr_cast_vm" (ret cast) VMcast +let () = define "constr_cast_native" (ret cast) NATIVEcast let () = - define "constr_in_context" (ident @-> constr @-> closure @-> tac constr) @@ fun id t c -> + define "constr_in_context" (ident @-> constr @-> thunk unit @-> tac constr) @@ fun id t c -> Proofview.Goal.goals >>= function | [gl] -> gl >>= fun gl -> @@ -766,50 +790,58 @@ let () = throw err_notfocussed (** preterm -> constr *) -let () = define "constr_flags" (ret (repr_ext val_pretype_flags)) constr_flags +let pretype_flags_ = repr_ext val_pretype_flags +let pretype_flags = typed pretype_flags_ Types.(!! GT.pretype_flags) + +let () = define "constr_flags" (ret pretype_flags) constr_flags -let () = define "open_constr_flags" (ret (repr_ext val_pretype_flags)) open_constr_use_classes_flags +let () = define "open_constr_flags" (ret pretype_flags) open_constr_use_classes_flags -let () = define "expected_istype" (ret (repr_ext val_expected_type)) IsType +let expected_type_ = repr_ext val_expected_type +let expected_type = typed expected_type_ Types.(!! GT.pretype_expected_type) -let () = define "expected_oftype" (constr @-> ret (repr_ext val_expected_type)) @@ fun c -> +let () = define "expected_istype" (ret expected_type) IsType + +let () = define "expected_oftype" (constr @-> ret expected_type) @@ fun c -> OfType c -let () = define "expected_without_type_constraint" (ret (repr_ext val_expected_type)) - WithoutTypeConstraint +let () = define "expected_without_type_constraint" (ret expected_type) WithoutTypeConstraint let () = - define "constr_pretype" (repr_ext val_pretype_flags @-> repr_ext val_expected_type @-> preterm @-> tac constr) @@ fun flags expected_type c -> + define "constr_pretype" (pretype_flags @-> expected_type @-> preterm @-> tac constr) @@ fun flags expected_type c -> let pretype env sigma = let sigma, t = Pretyping.understand_uconstr ~flags ~expected_type env sigma c in Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclUNIT t in pf_apply ~catch_exceptions:true pretype +let binder_ = repr_ext val_binder +let binder = typed binder_ Types.(!! GT.binder) + let () = - define "constr_binder_make" (option ident @-> constr @-> tac valexpr) @@ fun na ty -> + define "constr_binder_make" (option ident @-> constr @-> tac binder) @@ 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 (Tac2ffi.of_ext val_binder (Context.make_annot na rel, ty)) + return (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 () = define "constr_binder_unsafe_make" - (option ident @-> relevance @-> constr @-> ret valexpr) + (option ident @-> relevance @-> constr @-> ret binder) @@ fun na rel ty -> let na = match na with None -> Anonymous | Some id -> Name id in - Tac2ffi.of_ext val_binder (Context.make_annot na rel, ty) + (Context.make_annot na rel, ty) let () = - define "constr_binder_name" (repr_ext val_binder @-> ret (option ident)) @@ fun (bnd, _) -> + define "constr_binder_name" (binder @-> ret (option ident)) @@ fun (bnd, _) -> match bnd.Context.binder_name with Anonymous -> None | Name id -> Some id let () = - define "constr_binder_type" (repr_ext val_binder @-> ret constr) @@ fun (_, ty) -> ty + define "constr_binder_type" (binder @-> ret constr) @@ fun (_, ty) -> ty let () = define "constr_has_evar" (constr @-> tac bool) @@ fun c -> @@ -818,10 +850,12 @@ let () = (** Extra equalities *) +let meta = typed int_ Types.(!! GT.meta) + 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 "meta_equal" (meta @-> meta @-> ret bool) Int.equal let () = define "constr_cast_equal" (cast @-> cast @-> ret bool) Glob_ops.cast_kind_eq let () = @@ -829,24 +863,26 @@ let () = (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 -> + define "constr_case_equal" (constr_case @-> constr_case @-> ret bool) @@ fun x y -> Ind.UserOrd.equal x.ci_ind y.ci_ind let () = - let ty = repr_ext val_constructor in + let ty = typed (repr_ext val_constructor) Types.(!! GT.constructor) in define "constructor_equal" (ty @-> ty @-> ret bool) Construct.UserOrd.equal let () = define "projection_equal" (projection @-> projection @-> ret bool) Projection.UserOrd.equal (** Patterns *) +let matching_context_ = repr_ext val_matching_context +let matching_context = typed matching_context_ Types.(!! GT.matching_context) + let () = define "pattern_empty_context" - (ret (repr_ext val_matching_context)) + (ret matching_context) Constr_matching.empty_context let () = - define "pattern_matches" (pattern @-> constr @-> tac valexpr) @@ fun pat c -> + define "pattern_matches" (pattern @-> constr @-> tac (list (pair ident constr))) @@ fun pat c -> pf_apply @@ fun env sigma -> let ans = try Some (Constr_matching.matches env sigma pat c) @@ -856,35 +892,25 @@ let () = | None -> fail err_matchfailure | Some ans -> let ans = Id.Map.bindings ans in - let of_pair (id, c) = Tac2ffi.of_tuple [| Tac2ffi.of_ident id; Tac2ffi.of_constr c |] in - return (Tac2ffi.of_list of_pair ans) + return ans end let () = - define "pattern_matches_subterm" (pattern @-> constr @-> tac valexpr) @@ fun pat c -> + define "pattern_matches_subterm" (pattern @-> constr @-> tac (pair matching_context (list (pair ident constr)))) @@ fun pat c -> let open Constr_matching in - let rec of_ans s = match IStream.peek s with + let rec multireturn s = match IStream.peek s with | IStream.Nil -> fail err_matchfailure | IStream.Cons ({ m_sub = (_, sub); m_ctx }, s) -> let ans = Id.Map.bindings sub in - let of_pair (id, c) = - Tac2ffi.of_tuple [| Tac2ffi.of_ident id; Tac2ffi.of_constr c |] - in - let ans = - Tac2ffi.of_tuple [| - Tac2ffi.of_ext val_matching_context m_ctx; - Tac2ffi.of_list of_pair ans; - |] - in - Proofview.tclOR (return ans) (fun _ -> of_ans s) + Proofview.tclOR (return (m_ctx,ans)) (fun _ -> multireturn s) in 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 + multireturn ans let () = - define "pattern_matches_vect" (pattern @-> constr @-> tac valexpr) @@ fun pat c -> + define "pattern_matches_vect" (pattern @-> constr @-> tac (array constr)) @@ fun pat c -> pf_apply @@ fun env sigma -> let ans = try Some (Constr_matching.matches env sigma pat c) @@ -895,37 +921,43 @@ let () = | Some ans -> let ans = Id.Map.bindings ans in let ans = Array.map_of_list snd ans in - return (Tac2ffi.of_array Tac2ffi.of_constr ans) + return ans let () = - define "pattern_matches_subterm_vect" (pattern @-> constr @-> tac valexpr) @@ fun pat c -> + define "pattern_matches_subterm_vect" (pattern @-> constr @-> tac (pair matching_context (array constr))) @@ fun pat c -> let open Constr_matching in - let rec of_ans s = match IStream.peek s with + let rec multireturn s = match IStream.peek s with | IStream.Nil -> fail err_matchfailure | IStream.Cons ({ m_sub = (_, sub); m_ctx }, s) -> let ans = Id.Map.bindings sub in let ans = Array.map_of_list snd ans in - let ans = - Tac2ffi.of_tuple [| - Tac2ffi.of_ext val_matching_context m_ctx; - Tac2ffi.of_array Tac2ffi.of_constr ans; - |] - in - Proofview.tclOR (return ans) (fun _ -> of_ans s) + Proofview.tclOR (return (m_ctx, ans)) (fun _ -> multireturn s) in 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 + multireturn ans -let match_pattern = map_repr +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) + (pair_ bool_ pattern_) + +let match_pattern = typed match_pattern_ Types.(tuple [!! GT.match_kind; !! GT.pattern]) + +let pattern_matches_goal_return_ty = + let open Types in + let open GT in + tuple [! array [!! ident]; + ! array [!! matching_context]; + ! array [!! matching_context]; + ! array [!! constr]; + !! matching_context] let () = define "pattern_matches_goal" - (bool @-> list (pair (option match_pattern) match_pattern) @-> match_pattern @-> tac valexpr) + (bool @-> list (pair (option match_pattern) match_pattern) @-> match_pattern + @-> tac (typed valexpr pattern_matches_goal_return_ty)) @@ fun rev hp cp -> assert_focussed >>= fun () -> Proofview.Goal.enter_one @@ fun gl -> @@ -947,16 +979,16 @@ let () = let () = define "pattern_instantiate" - (repr_ext val_matching_context @-> constr @-> ret constr) + (matching_context @-> constr @-> ret constr) Constr_matching.instantiate_context (** Error *) let () = - define "throw" (exn @-> tac valexpr) @@ fun (e, info) -> throw ~info e + define "throw" (exn @-> tac valexpr_0) @@ fun (e, info) -> throw ~info e let () = - define "throw_bt" (exn @-> exninfo @-> tac valexpr) @@ fun (e,_) info -> + define "throw_bt" (exn @-> exninfo @-> tac valexpr_0) @@ fun (e,_) info -> Proofview.tclLIFT (Proofview.NonLogical.raise (e, info)) let () = @@ -966,64 +998,66 @@ let () = (** exn -> 'a *) let () = - define "zero" (exn @-> tac valexpr) @@ fun (e, info) -> fail ~info e + define "zero" (exn @-> tac valexpr_0) @@ fun (e, info) -> fail ~info e let () = - define "zero_bt" (exn @-> exninfo @-> tac valexpr) @@ fun (e,_) info -> + define "zero_bt" (exn @-> exninfo @-> tac valexpr_0) @@ fun (e,_) info -> Proofview.tclZERO ~info e (** (unit -> 'a) -> (exn -> 'a) -> 'a *) let () = - define "plus" (closure @-> closure @-> tac valexpr) @@ fun x k -> - Proofview.tclOR (thaw x) (fun e -> Tac2val.apply k [Tac2ffi.of_exn e]) + define "plus" + (thunk valexpr_0 + @-> fun1 exn valexpr_0 + @-> tac valexpr_0) @@ fun x k -> + Proofview.tclOR (thaw x) k let () = - define "plus_bt" (closure @-> closure @-> tac valexpr) @@ fun run handle -> - Proofview.tclOR (thaw run) - (fun e -> Tac2val.apply handle [Tac2ffi.of_exn e; of_exninfo (snd e)]) + define "plus_bt" + (thunk valexpr_0 @-> fun2 exn exninfo valexpr_0 @-> tac valexpr_0) @@ fun run handle -> + Proofview.tclOR (thaw run) + (fun e -> handle e (snd e)) (** (unit -> 'a) -> 'a *) let () = - define "once" (closure @-> tac valexpr) @@ fun f -> + define "once" (thunk valexpr_0 @-> tac valexpr_0) @@ fun f -> Proofview.tclONCE (thaw f) (** (unit -> unit) list -> unit *) let () = - define "dispatch" (list closure @-> tac unit) @@ fun l -> - let l = List.map (fun f -> Proofview.tclIGNORE (thaw f)) l in + define "dispatch" (list (thunk unit) @-> tac unit) @@ fun l -> + let l = List.map (fun f -> thaw f) l in Proofview.tclDISPATCH l (** (unit -> unit) list -> (unit -> unit) -> (unit -> unit) list -> unit *) 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 + define "extend" (list (thunk unit) @-> thunk unit @-> list (thunk unit) @-> tac unit) @@ fun lft tac rgt -> + let lft = List.map thaw lft in + let tac = thaw tac in + let rgt = List.map thaw rgt in Proofview.tclEXTEND lft tac rgt (** (unit -> unit) -> unit *) let () = - define "enter" (closure @-> tac unit) @@ fun f -> - let f = Proofview.tclIGNORE (thaw f) in - Proofview.tclINDEPENDENT f + define "enter" (thunk unit @-> tac unit) @@ fun f -> + Proofview.tclINDEPENDENT (thaw f) (** (unit -> 'a) -> ('a * ('exn -> 'a)) result *) let () = - define "case" (closure @-> tac valexpr) @@ fun f -> + define "case" (thunk valexpr_0 @-> tac (result (pair valexpr_0 (fun1 exn valexpr_0)))) @@ fun f -> Proofview.tclCASE (thaw f) >>= begin function | Proofview.Next (x, k) -> - let k = Tac2val.mk_closure arity_one begin fun e -> - let (e, info) = Tac2ffi.to_exn e in + let k (e,info) = set_bt info >>= fun info -> k (e, info) - end in - return (v_blk 0 [| Tac2ffi.of_tuple [| x; Tac2ffi.of_closure k |] |]) - | Proofview.Fail e -> return (v_blk 1 [| Tac2ffi.of_exn e |]) + in + return (Ok (x, k)) + | Proofview.Fail e -> return (Error e) end (** int -> int -> (unit -> 'a) -> 'a *) let () = - define "focus" (int @-> int @-> closure @-> tac valexpr) @@ fun i j tac -> + define "focus" (int @-> int @-> thunk valexpr_0 @-> tac valexpr_0) @@ fun i j tac -> Proofview.tclFOCUS i j (thaw tac) (** unit -> unit *) @@ -1058,64 +1092,58 @@ let () = (str "Hypothesis " ++ quote (Id.print id) ++ str " not found") (* FIXME: Do something more sensible *) let () = - define "hyps" (unit @-> tac valexpr) @@ fun _ -> + define "hyps" (unit @-> tac (list (triple ident (option constr) constr))) @@ 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 - Tac2ffi.of_tuple [| - Tac2ffi.of_ident id.binder_name; - Tac2ffi.of_option Tac2ffi.of_constr None; - Tac2ffi.of_constr t; - |] + (id.binder_name, None, t) | LocalDef (id, c, t) -> let c = EConstr.of_constr c in let t = EConstr.of_constr t in - Tac2ffi.of_tuple [| - Tac2ffi.of_ident id.binder_name; - Tac2ffi.of_option Tac2ffi.of_constr (Some c); - Tac2ffi.of_constr t; - |] + (id.binder_name, Some c, t) in - return (Tac2ffi.of_list map hyps) + let hyps = List.rev_map map (Environ.named_context env) in + return hyps (** (unit -> constr) -> unit *) let () = - define "refine" (closure @-> tac unit) @@ fun c -> - let c = thaw c >>= fun c -> Proofview.tclUNIT ((), Tac2ffi.to_constr c) in + define "refine" (thunk constr @-> tac unit) @@ fun c -> + let c = thaw c >>= fun c -> Proofview.tclUNIT ((), c) in Proofview.Goal.enter @@ fun gl -> Refine.generic_refine ~typecheck:true c gl let () = - define "with_holes" (closure @-> closure @-> tac valexpr) @@ fun x f -> + define "with_holes" + (thunk valexpr_0 @-> fun1 valexpr_0 (typed valexpr (Types.var 1)) + @-> tac (typed valexpr (Types.var 1))) @@ fun x f -> Proofview.tclEVARMAP >>= fun sigma0 -> thaw x >>= fun ans -> Proofview.tclEVARMAP >>= fun sigma -> Proofview.Unsafe.tclEVARS sigma0 >>= fun () -> - Tacticals.tclWITHHOLES false (Tac2val.apply f [ans]) sigma + Tacticals.tclWITHHOLES false (f ans) sigma let () = - define "progress" (closure @-> tac valexpr) @@ fun f -> + define "progress" (thunk valexpr_0 @-> tac valexpr_0) @@ fun f -> Proofview.tclPROGRESS (thaw f) let () = - define "abstract" (option ident @-> closure @-> tac unit) @@ fun id f -> - Abstract.tclABSTRACT id (Proofview.tclIGNORE (thaw f)) + define "abstract" (option ident @-> thunk unit @-> tac unit) @@ fun id f -> + Abstract.tclABSTRACT id (thaw f) let () = - define "time" (option string @-> closure @-> tac valexpr) @@ fun s f -> + define "time" (option string @-> thunk valexpr_0 @-> tac valexpr_0) @@ fun s f -> Proofview.tclTIME s (thaw f) let () = - define "timeout" (int @-> closure @-> tac valexpr) @@ fun i f -> + define "timeout" (int @-> thunk valexpr_0 @-> tac valexpr_0) @@ fun i f -> Proofview.tclTIMEOUT i (thaw f) let () = - define "timeoutf" (float @-> closure @-> tac valexpr) @@ fun f64 f -> - Proofview.tclTIMEOUTF (Float64.to_float f64) (thaw f) + define "timeoutf" (float @-> thunk valexpr_0 @-> tac valexpr_0) @@ fun f64 f -> + Proofview.tclTIMEOUTF (Float64.to_float f64) (f()) let () = define "check_interrupt" (unit @-> tac unit) @@ fun _ -> @@ -1123,16 +1151,18 @@ let () = (** Fresh *) +let free_ = repr_ext val_free +let free = typed free_ Types.(!! GT.free) + let () = - let ty = repr_ext val_free in - define "fresh_free_union" (ty @-> ty @-> ret ty) Id.Set.union + define "fresh_free_union" (free @-> free @-> ret free) Id.Set.union let () = - define "fresh_free_of_ids" (list ident @-> ret (repr_ext val_free)) @@ fun ids -> + define "fresh_free_of_ids" (list ident @-> ret free) @@ fun ids -> List.fold_right Id.Set.add ids Id.Set.empty let () = - define "fresh_free_of_constr" (constr @-> tac (repr_ext val_free)) @@ fun c -> + define "fresh_free_of_constr" (constr @-> tac free) @@ fun c -> Proofview.tclEVARMAP >>= fun sigma -> let rec fold accu c = match EConstr.kind sigma c with @@ -1142,7 +1172,7 @@ let () = return (fold Id.Set.empty c) let () = - define "fresh_fresh" (repr_ext val_free @-> ident @-> ret ident) @@ fun avoid id -> + define "fresh_fresh" (free @-> ident @-> ret ident) @@ fun avoid id -> Namegen.next_ident_away_from id (fun id -> Id.Set.mem id avoid) (** Env *) @@ -1187,12 +1217,15 @@ let () = (** Ind *) +let ind_data_ = repr_ext val_ind_data +let ind_data = typed ind_data_ Types.(!! GT.ind_data) + let () = define "ind_equal" (inductive @-> inductive @-> ret bool) Ind.UserOrd.equal let () = define "ind_data" - (inductive @-> tac (repr_ext val_ind_data)) + (inductive @-> tac ind_data) @@ fun ind -> Proofview.tclENV >>= fun env -> if Environ.mem_mind (fst ind) env then @@ -1200,28 +1233,31 @@ let () = else throw err_notfound -let () = define "ind_repr" (repr_ext val_ind_data @-> ret inductive) fst +let () = define "ind_repr" (ind_data @-> ret inductive) fst let () = define "ind_index" (inductive @-> ret int) snd let () = - define "ind_nblocks" (repr_ext val_ind_data @-> ret int) @@ fun (_, mib) -> + define "ind_nblocks" (ind_data @-> ret int) @@ fun (_, mib) -> Array.length mib.Declarations.mind_packets let () = - define "ind_nconstructors" (repr_ext val_ind_data @-> ret int) @@ fun ((_, n), mib) -> + define "ind_nconstructors" (ind_data @-> ret int) @@ fun ((_, n), mib) -> Array.length Declarations.(mib.mind_packets.(n).mind_consnames) let () = define "ind_get_block" - (repr_ext val_ind_data @-> int @-> tac (repr_ext val_ind_data)) + (ind_data @-> int @-> tac ind_data) @@ fun (ind, mib) n -> if 0 <= n && n < Array.length mib.Declarations.mind_packets then return ((fst ind, n), mib) else throw err_notfound +let constructor_ = repr_ext val_constructor +let constructor = typed constructor_ Types.(!! GT.constructor) + let () = define "ind_get_constructor" - (repr_ext val_ind_data @-> int @-> tac (repr_ext val_constructor)) + (ind_data @-> int @-> tac constructor) @@ fun ((mind, n), mib) i -> let open Declarations in let ncons = Array.length mib.mind_packets.(n).mind_consnames in @@ -1233,18 +1269,18 @@ let () = let () = define "constructor_inductive" - (repr_ext val_constructor @-> ret inductive) + (constructor @-> ret inductive) @@ fun (ind, _) -> ind let () = define "constructor_index" - (repr_ext val_constructor @-> ret int) + (constructor @-> ret int) @@ fun (_, i) -> (* WARNING: ML constructors are 1-indexed but Ltac2 constructors are 0-indexed *) i-1 let () = - define "ind_get_projections" (repr_ext val_ind_data @-> ret (option (array projection))) + define "ind_get_projections" (ind_data @-> ret (option (array projection))) @@ fun (ind,mib) -> Declareops.inductive_make_projections ind mib |> Option.map (Array.map (fun (p,_) -> Projection.make p false)) @@ -1283,13 +1319,17 @@ type tagged_map = TaggedMap : (_,_,'map) map_tag * 'map -> tagged_map let map_tag_ext : any_map_tag Tac2dyn.Val.tag = Tac2dyn.Val.create "fmap_tag" let map_tag_repr = Tac2ffi.repr_ext map_tag_ext +let map_tag_ty t = Types.(! GT.map_tag [t]) + +let map_tag_0 = typed map_tag_repr (map_tag_ty (Types.var 0)) + let set_ext : tagged_set Tac2dyn.Val.tag = Tac2dyn.Val.create "fset" let set_repr = Tac2ffi.repr_ext set_ext -let tag_set tag s = Tac2ffi.repr_of set_repr (TaggedSet (tag,s)) +let tag_set tag s = TaggedSet (tag,s) let map_ext : tagged_map Tac2dyn.Val.tag = Tac2dyn.Val.create "fmap" let map_repr = Tac2ffi.repr_ext map_ext -let tag_map tag m = Tac2ffi.repr_of map_repr (TaggedMap (tag,m)) +let tag_map tag m = TaggedMap (tag,m) module type MapType = sig (* to have less boilerplate we use S.elt rather than declaring a toplevel type t *) @@ -1297,11 +1337,14 @@ module type MapType = sig module M : CMap.ExtS with type key = S.elt and module Set := S type valmap val valmap_eq : (valmap, valexpr M.t) Util.eq - val repr : S.elt Tac2ffi.repr + val repr : S.elt repr + val typ : Types.t option end +type ('t,'set,'map) maptype = (module MapType with type S.elt = 't and type S.t = 'set and type valmap = 'map) + module MapTypeV = struct - type _ t = Map : (module MapType with type S.elt = 't and type S.t = 'set and type valmap = 'map) + type _ t = Map : ('t,'set,'map) maptype -> ('t * 'set * 'map) t end @@ -1309,10 +1352,13 @@ module MapMap = MapTagDyn.Map(MapTypeV) let maps = ref MapMap.empty -let register_map ?(plugin=ltac2_plugin) ~tag_name x = +let register_map (type t set map) ?(plugin=ltac2_plugin) ~tag_name (x:(t,set,map) maptype) + : (t * set * map) MapTagDyn.tag = let tag = MapTagDyn.create (plugin^":"^tag_name) in let () = maps := MapMap.add tag (Map x) !maps in - let () = define ~plugin tag_name (ret map_tag_repr) (Any tag) in + let module X = (val x) in + let ty = map_tag_ty (Types.default X.typ) in + let () = define ~plugin tag_name (ret (typed map_tag_repr ty)) (Any tag) in tag let get_map (type t s m) (tag:(t,s,m) map_tag) @@ -1331,7 +1377,7 @@ let assert_map_tag_eq t1 t2 = match map_tag_eq t1 t2 with let ident_map_tag : _ map_tag = register_map ~tag_name:"fmap_ident_tag" (module struct module S = Id.Set module M = Id.Map - let repr = Tac2ffi.ident + let repr, typ = Tac2ffi.ident type valmap = valexpr M.t let valmap_eq = Refl end) @@ -1339,7 +1385,7 @@ let ident_map_tag : _ map_tag = register_map ~tag_name:"fmap_ident_tag" (module let int_map_tag : _ map_tag = register_map ~tag_name:"fmap_int_tag" (module struct module S = Int.Set module M = Int.Map - let repr = Tac2ffi.int + let repr, typ = Tac2ffi.int type valmap = valexpr M.t let valmap_eq = Refl end) @@ -1347,7 +1393,7 @@ let int_map_tag : _ map_tag = register_map ~tag_name:"fmap_int_tag" (module stru let string_map_tag : _ map_tag = register_map ~tag_name:"fmap_string_tag" (module struct module S = String.Set module M = String.Map - let repr = Tac2ffi.string + let repr, typ = Tac2ffi.string type valmap = valexpr M.t let valmap_eq = Refl end) @@ -1355,7 +1401,7 @@ let string_map_tag : _ map_tag = register_map ~tag_name:"fmap_string_tag" (modul let inductive_map_tag : _ map_tag = register_map ~tag_name:"fmap_inductive_tag" (module struct module S = Indset_env module M = Indmap_env - let repr = inductive + let repr, typ = inductive type valmap = valexpr M.t let valmap_eq = Refl end) @@ -1363,7 +1409,7 @@ let inductive_map_tag : _ map_tag = register_map ~tag_name:"fmap_inductive_tag" let constructor_map_tag : _ map_tag = register_map ~tag_name:"fmap_constructor_tag" (module struct module S = Constrset_env module M = Constrmap_env - let repr = Tac2ffi.(repr_ext val_constructor) + let repr, typ = constructor type valmap = valexpr M.t let valmap_eq = Refl end) @@ -1371,151 +1417,163 @@ let constructor_map_tag : _ map_tag = register_map ~tag_name:"fmap_constructor_t let constant_map_tag : _ map_tag = register_map ~tag_name:"fmap_constant_tag" (module struct module S = Cset_env module M = Cmap_env - let repr = Tac2ffi.(repr_ext val_constant) + let repr, typ = constant type valmap = valexpr M.t let valmap_eq = Refl end) +let fset_0 = typed set_repr Types.(! GT.fset [var 0]) + let () = - define "fset_empty" (map_tag_repr @-> ret valexpr) @@ fun (Any tag) -> + define "fset_empty" (map_tag_0 @-> ret fset_0) @@ fun (Any tag) -> let (module V) = get_map tag in tag_set tag V.S.empty let () = - define "fset_is_empty" (set_repr @-> ret bool) @@ fun (TaggedSet (tag,s)) -> + define "fset_is_empty" (fset_0 @-> ret bool) @@ fun (TaggedSet (tag,s)) -> let (module V) = get_map tag in V.S.is_empty s let () = - define "fset_mem" (valexpr @-> set_repr @-> ret bool) @@ fun x (TaggedSet (tag,s)) -> + define "fset_mem" (valexpr_0 @-> fset_0 @-> ret bool) @@ fun x (TaggedSet (tag,s)) -> let (module V) = get_map tag in V.S.mem (repr_to V.repr x) s let () = - define "fset_add" (valexpr @-> set_repr @-> ret valexpr) @@ fun x (TaggedSet (tag,s)) -> + define "fset_add" (valexpr_0 @-> fset_0 @-> ret fset_0) @@ 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 () = - define "fset_remove" (valexpr @-> set_repr @-> ret valexpr) @@ fun x (TaggedSet (tag,s)) -> + define "fset_remove" (valexpr_0 @-> fset_0 @-> ret fset_0) @@ 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 () = - define "fset_union" (set_repr @-> set_repr @-> ret valexpr) + define "fset_union" (fset_0 @-> fset_0 @-> ret fset_0) @@ 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 () = - define "fset_inter" (set_repr @-> set_repr @-> ret valexpr) + define "fset_inter" (fset_0 @-> fset_0 @-> ret fset_0) @@ 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 () = - define "fset_diff" (set_repr @-> set_repr @-> ret valexpr) + define "fset_diff" (fset_0 @-> fset_0 @-> ret fset_0) @@ 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 () = - define "fset_equal" (set_repr @-> set_repr @-> ret bool) + define "fset_equal" (fset_0 @-> fset_0 @-> 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 () = - define "fset_subset" (set_repr @-> set_repr @-> ret bool) + define "fset_subset" (fset_0 @-> fset_0 @-> 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 () = - define "fset_cardinal" (set_repr @-> ret int) @@ fun (TaggedSet (tag,s)) -> + define "fset_cardinal" (fset_0 @-> ret int) @@ fun (TaggedSet (tag,s)) -> let (module V) = get_map tag in V.S.cardinal s let () = - define "fset_elements" (set_repr @-> ret valexpr) @@ fun (TaggedSet (tag,s)) -> + define "fset_elements" (fset_0 @-> ret (list valexpr_0)) @@ fun (TaggedSet (tag,s)) -> let (module V) = get_map tag in - Tac2ffi.of_list (repr_of V.repr) (V.S.elements s) + List.map (repr_of V.repr) (V.S.elements s) + +let fmap_0_1 = typed map_repr Types.(! GT.fmap [var 0; var 1]) let () = - define "fmap_empty" (map_tag_repr @-> ret valexpr) @@ fun (Any (tag)) -> + define "fmap_empty" (map_tag_0 @-> ret fmap_0_1) @@ fun (Any (tag)) -> let (module V) = get_map tag in let Refl = V.valmap_eq in tag_map tag V.M.empty let () = - define "fmap_is_empty" (map_repr @-> ret bool) @@ fun (TaggedMap (tag,m)) -> + define "fmap_is_empty" (fmap_0_1 @-> 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 () = - define "fmap_mem" (valexpr @-> map_repr @-> ret bool) @@ fun x (TaggedMap (tag,m)) -> + define "fmap_mem" (valexpr_0 @-> fmap_0_1 @-> 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 () = - define "fmap_add" (valexpr @-> valexpr @-> map_repr @-> ret valexpr) + define "fmap_add" (valexpr_0 @-> typed valexpr (Types.var 1) @-> fmap_0_1 @-> ret fmap_0_1) @@ 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 () = - define "fmap_remove" (valexpr @-> map_repr @-> ret valexpr) + define "fmap_remove" (valexpr_0 @-> fmap_0_1 @-> ret fmap_0_1) @@ 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 () = - define "fmap_find_opt" (valexpr @-> map_repr @-> ret (option valexpr)) + define "fmap_find_opt" (valexpr_0 @-> fmap_0_1 @-> ret (option (typed valexpr (Types.var 1)))) @@ 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 () = - define "fmap_mapi" (closure @-> map_repr @-> tac valexpr) + define "fmap_mapi" + (fun2 valexpr_0 (typed valexpr (Types.var 1)) (typed valexpr (Types.var 2)) + @-> fmap_0_1 @-> tac (typed map_repr Types.(! GT.fmap [var 0; var 2]))) @@ 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 -> + Monadic.mapi (fun k v -> f (repr_of V.repr k) v) m >>= fun m -> return (tag_map tag m) let () = - define "fmap_fold" (closure @-> map_repr @-> valexpr @-> tac valexpr) + define "fmap_fold" + (fun3 valexpr_0 (typed valexpr (Types.var 1)) (typed valexpr (Types.var 2)) + (typed valexpr (Types.var 2)) + @-> fmap_0_1 @-> typed valexpr (Types.var 2) @-> tac (typed valexpr (Types.var 2))) @@ 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 + Monadic.fold (fun k v acc -> f (repr_of V.repr k) v acc) m acc let () = - define "fmap_cardinal" (map_repr @-> ret int) @@ fun (TaggedMap (tag,m)) -> + define "fmap_cardinal" (fmap_0_1 @-> ret int) @@ fun (TaggedMap (tag,m)) -> let (module V) = get_map tag in let Refl = V.valmap_eq in V.M.cardinal m let () = - define "fmap_bindings" (map_repr @-> ret valexpr) @@ fun (TaggedMap (tag,m)) -> + define "fmap_bindings" + (fmap_0_1 @-> + ret (list (pair (typed valexpr (Types.var 0)) (typed valexpr (Types.var 1))))) + @@ fun (TaggedMap (tag,m)) -> let (module V) = get_map tag in let Refl = V.valmap_eq in - Tac2ffi.(of_list (of_pair (repr_of V.repr) identity) (V.M.bindings m)) + List.map (fun (k,v) -> repr_of V.repr k, v) (V.M.bindings m) let () = - define "fmap_domain" (map_repr @-> ret valexpr) @@ fun (TaggedMap (tag,m)) -> + define "fmap_domain" (fmap_0_1 @-> ret fset_0) @@ fun (TaggedMap (tag,m)) -> let (module V) = get_map tag in let Refl = V.valmap_eq in tag_set tag (V.M.domain m) diff --git a/plugins/ltac2/tac2core.mli b/plugins/ltac2/tac2core.mli index 1a2d44b888e4..a5bc673ac77a 100644 --- a/plugins/ltac2/tac2core.mli +++ b/plugins/ltac2/tac2core.mli @@ -44,6 +44,7 @@ module type MapType = sig type valmap val valmap_eq : (valmap, Tac2val.valexpr M.t) Util.eq val repr : S.elt Tac2ffi.repr + val typ : Tac2ffi.Types.t option end type ('a,'set,'map) map_tag diff --git a/plugins/ltac2/tac2env.mli b/plugins/ltac2/tac2env.mli index edbe81ecb173..c8614d4af866 100644 --- a/plugins/ltac2/tac2env.mli +++ b/plugins/ltac2/tac2env.mli @@ -157,6 +157,8 @@ val interp_ml_object : ('a, 'b) Tac2dyn.Arg.tag -> ('a, 'b) ml_object (** {5 Absolute paths} *) +(* TODO move this to tac2globals *) + val coq_prefix : ModPath.t (** Path where primitive datatypes are defined in Ltac2 plugin. *) diff --git a/plugins/ltac2/tac2externals.ml b/plugins/ltac2/tac2externals.ml index 3901d1284a43..e80518c4837b 100644 --- a/plugins/ltac2/tac2externals.ml +++ b/plugins/ltac2/tac2externals.ml @@ -8,6 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +open Util open Proofview open Tac2ffi @@ -21,52 +22,52 @@ type 'a with_env = Environ.env -> Evd.evar_map -> 'a to be give for this type definition to be accepted. If we remove it, we get an error: "a type variable cannot be deduced from the type parameters". *) type (_, _, _) spec_aux = - | T : 'r to_v -> (v tactic, 'r tactic, 'r) spec_aux - | V : 'r to_v -> (v tactic, 'r, 'r) spec_aux - | E : 'r to_v -> (v tactic, 'r with_env, 'r) spec_aux - | G : 'r to_v -> (v tactic, Goal.t -> 'r, 'r) spec_aux - | F : 'a of_v * ('t, 'f, 'r) spec_aux -> (v -> 't , 'a -> 'f, 'r) spec_aux + | T : 'r to_v annotated -> (v tactic, 'r tactic, 'r) spec_aux + | V : 'r to_v annotated -> (v tactic, 'r, 'r) spec_aux + | E : 'r to_v annotated -> (v tactic, 'r with_env, 'r) spec_aux + | G : 'r to_v annotated -> (v tactic, Goal.t -> 'r, 'r) spec_aux + | F : 'a of_v annotated * ('t, 'f, 'r) spec_aux -> (v -> 't , 'a -> 'f, 'r) spec_aux type (_,_) spec = S : ('v,'f,'r) spec_aux -> ('v,'f) spec [@@unboxed] -let tac : type r. r repr -> (v tactic, r tactic) spec = fun r -> - S (T (repr_of r)) +let tac : type r. r repr annotated -> (v tactic, r tactic) spec = fun r -> + S (T (on_fst repr_of r)) -let tac': type r. r to_v -> (v tactic, r tactic) spec = fun tr -> +let tac': type r. r to_v annotated -> (v tactic, r tactic) spec = fun tr -> S (T tr) -let ret : type r. r repr -> (v tactic, r) spec = fun r -> - S (V (repr_of r)) +let ret : type r. r repr annotated -> (v tactic, r) spec = fun r -> + S (V (on_fst repr_of r)) -let ret': type r. r to_v -> (v tactic, r) spec = fun tr -> +let ret': type r. r to_v annotated -> (v tactic, r) spec = fun tr -> S (V tr) -let eret : type r. r repr -> (v tactic, r with_env) spec = fun r -> - S (E (repr_of r)) +let eret : type r. r repr annotated -> (v tactic, r with_env) spec = fun r -> + S (E (on_fst repr_of r)) -let eret': type r. r to_v -> (v tactic, r with_env) spec = fun tr -> +let eret': type r. r to_v annotated -> (v tactic, r with_env) spec = fun tr -> S (E tr) -let gret : type r. r repr -> (v tactic, Goal.t -> r) spec = fun r -> - S (G (repr_of r)) +let gret : type r. r repr annotated -> (v tactic, Goal.t -> r) spec = fun r -> + S (G (on_fst repr_of r)) -let gret': type r. r to_v -> (v tactic, Goal.t -> r) spec = fun tr -> +let gret': type r. r to_v annotated -> (v tactic, Goal.t -> r) spec = fun tr -> S (G tr) -let (@->) : type a t f. a repr -> (t,f) spec -> (v -> t, a -> f) spec = - fun r (S ar) -> S (F (repr_to r, ar)) +let (@->) : type a t f. a repr annotated -> (t,f) spec -> (v -> t, a -> f) spec = + fun r (S ar) -> S (F (on_fst repr_to r, ar)) -let (@-->): type a t f. a of_v -> (t,f) spec -> (v -> t, a -> f) spec = +let (@-->): type a t f. a of_v annotated -> (t,f) spec -> (v -> t, a -> f) spec = fun of_v (S ar) -> S (F (of_v, ar)) let rec interp_spec : type v f. (v,f) spec -> f -> v = fun (S ar) f -> let open Proofview.Notations in match ar with - | T tr -> f >>= fun v -> tclUNIT (tr v) - | V tr -> tclUNIT (tr f) - | E tr -> tclENV >>= fun e -> tclEVARMAP >>= fun s -> tclUNIT (tr (f e s)) - | G tr -> Goal.enter_one @@ fun g -> tclUNIT (tr (f g)) - | F (tr,ar) -> fun v -> interp_spec (S ar) (f (tr v)) + | T tr -> f >>= fun v -> tclUNIT (fst tr v) + | V tr -> tclUNIT (fst tr f) + | E tr -> tclENV >>= fun e -> tclEVARMAP >>= fun s -> tclUNIT (fst tr (f e s)) + | G tr -> Goal.enter_one @@ fun g -> tclUNIT (fst tr (f g)) + | F (tr,ar) -> fun v -> interp_spec (S ar) (f (fst tr v)) let rec arity_of : type v f. (v,f) spec -> v Tac2val.arity = fun (S ar) -> match ar with @@ -77,13 +78,23 @@ let rec arity_of : type v f. (v,f) spec -> v Tac2val.arity = fun (S ar) -> | F (_, ar) -> Tac2val.arity_suc (arity_of (S ar)) | _ -> invalid_arg "Tac2def.arity_of: not a function spec" +let rec type_of_spec : type v f. (v,f) spec -> Types.t = fun (S ar) -> + let of_annot (_,t) = Option.default Types.any t in + match ar with + | T tr -> of_annot tr + | V tr -> of_annot tr + | E tr -> of_annot tr + | G tr -> of_annot tr + | F (tr,ar) -> Types.(of_annot tr @-> type_of_spec (S ar)) + let define : type v f. _ -> (v,f) spec -> f -> unit = fun n ar v -> let v = match ar with - | S (V tr) -> tr v + | S (V tr) -> fst tr v | S (F _) -> let cl = Tac2val.mk_closure (arity_of ar) (interp_spec ar v) in Tac2ffi.of_closure cl | _ -> invalid_arg "Tac2def.define: not a pure value" in - Tac2env.define_primitive n None v + let ty = Some (Types.as_scheme @@ type_of_spec ar) in + Tac2env.define_primitive n ty v diff --git a/plugins/ltac2/tac2externals.mli b/plugins/ltac2/tac2externals.mli index 982db311ff45..30762ca22690 100644 --- a/plugins/ltac2/tac2externals.mli +++ b/plugins/ltac2/tac2externals.mli @@ -24,36 +24,36 @@ type (_, _) spec (** [tac r] is the specification of a tactic (in the tactic monad sense) whose return type is specified (and converted into an Ltac2 value) via [r]. *) val tac : - 'r repr -> + 'r repr annotated -> (valexpr tactic, 'r tactic) spec (** [tac'] is similar to [tac], but only needs a conversion function. *) val tac' : - ('r -> valexpr) -> + ('r -> valexpr) annotated -> (valexpr tactic, 'r tactic) spec (** [ret r] is the specification of a pure tactic (i.e., a tactic defined as a pure OCaml value, not needing the tactic monad) whose return type is given by [r] (see [tac]). *) val ret : - 'r repr -> + 'r repr annotated -> (valexpr tactic, 'r) spec (** [ret'] is similar to [ret], but only needs a conversion function. *) val ret' : - ('r -> valexpr) -> + ('r -> valexpr) annotated -> (valexpr tactic, 'r) spec (** [eret] is similar to [ret], but for tactics that can be implemented with a pure OCaml value, provided extra arguments [env] and [sigma], computed via [tclENV] and [tclEVARMAP]. *) val eret : - 'r repr -> + 'r repr annotated -> (valexpr tactic, Environ.env -> Evd.evar_map -> 'r) spec (** [eret'] is similar to [eret], but only needs a conversion function. *) val eret' : - ('r -> valexpr) -> + ('r -> valexpr) annotated -> (valexpr tactic, Environ.env -> Evd.evar_map -> 'r) spec (** [gret] is similar to [ret], but for tactics that can be implemented with a @@ -62,24 +62,24 @@ val eret' : of using an Ltac2 value defined with this specification. Indeed, the value of [g] is computed using [Goal.enter_one]. *) val gret : - 'r repr -> + 'r repr annotated -> (valexpr tactic, Goal.t -> 'r) spec (** [gret'] is similar to [gret], but only needs a conversion function. *) val gret' : - ('r -> valexpr) -> + ('r -> valexpr) annotated -> (valexpr tactic, Goal.t -> 'r) spec (** [r @-> s] extends the specification [s] with a closure argument whose type is specified by (and converted from an Ltac2 value via) [r]. *) val (@->) : - 'a repr -> + 'a repr annotated -> ('t,'f) spec -> (valexpr -> 't, 'a -> 'f) spec (** [(@-->)] is similar to [(@->)], but only needs a conversion function. *) val (@-->) : - (valexpr -> 'a) -> + (valexpr -> 'a) annotated -> ('t,'f) spec -> (valexpr -> 't, 'a -> 'f) spec diff --git a/plugins/ltac2/tac2extffi.ml b/plugins/ltac2/tac2extffi.ml index b8690049a336..fd9586924737 100644 --- a/plugins/ltac2/tac2extffi.ml +++ b/plugins/ltac2/tac2extffi.ml @@ -24,7 +24,8 @@ let to_qhyp v = match Value.to_block v with | (1, [| id |]) -> NamedHyp (CAst.make (Value.to_ident id)) | _ -> assert false -let qhyp = make_to_repr to_qhyp +let qhyp_ = make_to_repr to_qhyp +let qhyp = typed qhyp_ Types.(!! Tac2globals.Types.hypothesis) let to_bindings = function | ValInt 0 -> NoBindings @@ -34,10 +35,7 @@ let to_bindings = function ExplicitBindings ((Value.to_list (fun p -> to_pair to_qhyp Value.to_constr p) vl)) | _ -> assert false -let bindings = make_to_repr to_bindings +let bindings_ = make_to_repr to_bindings +let bindings = typed bindings_ Types.(!! Tac2globals.Types.bindings) -let to_constr_with_bindings v = match Value.to_tuple v with -| [| c; bnd |] -> (Value.to_constr c, to_bindings bnd) -| _ -> assert false - -let constr_with_bindings = make_to_repr to_constr_with_bindings +let constr_with_bindings = pair constr bindings diff --git a/plugins/ltac2/tac2extffi.mli b/plugins/ltac2/tac2extffi.mli index 3c0d967a69dc..93c114333ced 100644 --- a/plugins/ltac2/tac2extffi.mli +++ b/plugins/ltac2/tac2extffi.mli @@ -11,8 +11,8 @@ open Tac2ffi open Tac2types -val qhyp : quantified_hypothesis repr +val qhyp : quantified_hypothesis repr annotated -val bindings : bindings repr +val bindings : bindings repr annotated -val constr_with_bindings : constr_with_bindings repr +val constr_with_bindings : constr_with_bindings repr annotated diff --git a/plugins/ltac2/tac2ffi.ml b/plugins/ltac2/tac2ffi.ml index 7e77a2d3e810..1506fc264317 100644 --- a/plugins/ltac2/tac2ffi.ml +++ b/plugins/ltac2/tac2ffi.ml @@ -50,7 +50,6 @@ let val_binder = Val.create "binder" let val_univ = Val.create "universe" let val_quality = Val.create "quality" let val_free : Names.Id.Set.t Val.tag = Val.create "free" -let val_ltac1 : Geninterp.Val.t Val.tag = Val.create "ltac1" let val_uint63 = Val.create "uint63" let val_float = Val.create "float" let val_ind_data : (Names.Ind.t * Declarations.mutual_inductive_body) Val.tag = Val.create "ind_data" @@ -67,6 +66,57 @@ match Val.eq tag tag' with exception LtacError of Names.KerName.t * valexpr array +(** Type annotation *) + +module Types = struct + open Tac2expr + + type t = Any | Var of int | Ref of type_constant * t list | Tuple of t list | Arrow of t * t + + let any = Any + + let default t = Option.default Any t + + let var x = Var x + + let (!) x l = Ref (x, l) + + let (!!) x = ! x [] + + let tuple l = Tuple l + + let (@->) x y = Arrow (x, y) + + let as_scheme t = + let (!) x = x.contents in + let var_cnt = ref 0 in + (* find max explicit variable *) + let rec iter = function + | Any -> () + | Var x -> var_cnt := max !var_cnt (x+1) + | Ref (_,l) | Tuple l -> List.iter iter l + | Arrow (x,y) -> iter x; iter y + in + let () = iter t in + (* assign each Any to different variables *) + let rec as_ty = function + | Any -> let x = !var_cnt in var_cnt := x+1; GTypVar x + | Var x -> GTypVar x + | Ref (kn, l) -> GTypRef (Other kn, List.map as_ty l) + | Tuple l -> GTypRef (Tuple (List.length l), List.map as_ty l) + | Arrow (x, y) -> GTypArrow (as_ty x, as_ty y) + in + let t = as_ty t in + !var_cnt, t +end +open Types +module T = Tac2globals.Types + +type 'a annotated = 'a * Types.t option + +let typed x (ty:Types.t) = (x,Some ty) +let untyped x = (x,None) + (** Conversion functions *) let valexpr = { @@ -74,27 +124,33 @@ let valexpr = { r_to = (fun obj -> obj); } +let valexpr_0 = typed valexpr (Types.var 0) + let of_unit () = ValInt 0 let to_unit = function | ValInt 0 -> () | _ -> assert false -let unit = { +let unit_ = { r_of = of_unit; r_to = to_unit; } +let unit = typed unit_ (!! T.unit) + let of_int n = ValInt n let to_int = function | ValInt n -> n | _ -> assert false -let int = { +let int_ = { r_of = of_int; r_to = to_int; } +let int = typed int_ (!! T.int) + let of_bool b = if b then ValInt 0 else ValInt 1 let to_bool = function @@ -102,38 +158,46 @@ let to_bool = function | ValInt 1 -> false | _ -> assert false -let bool = { +let bool_ = { r_of = of_bool; r_to = to_bool; } +let bool = typed bool_ (!! T.bool) + let of_char n = ValInt (Char.code n) let to_char = function | ValInt n -> Char.chr n | _ -> assert false -let char = { +let char_ = { r_of = of_char; r_to = to_char; } +let char = typed char_ (!! T.char) + let of_bytes s = ValStr s let to_bytes = function | ValStr s -> s | _ -> assert false -let bytes = { +let bytes_ = { r_of = of_bytes; r_to = to_bytes; } +let bytes = typed bytes_ (!! T.string) + let of_string s = of_bytes (Bytes.of_string s) let to_string s = Bytes.to_string (to_bytes s) -let string = { +let string_ = { r_of = of_string; r_to = to_string; } +let string = typed string_ (!! T.string) + let rec of_list f = function | [] -> ValInt 0 | x :: l -> ValBlk (0, [| f x; of_list f l |]) @@ -143,11 +207,13 @@ let rec to_list f = function | ValBlk (0, [|v; vl|]) -> f v :: to_list f vl | _ -> assert false -let list r = { +let list_ r = { r_of = (fun l -> of_list r.r_of l); r_to = (fun l -> to_list r.r_to l); } +let list (r,t) = typed (list_ r) (! T.list [default t]) + let of_closure cls = ValCls cls let to_closure = Tac2val.to_closure @@ -171,27 +237,33 @@ let repr_ext tag = { let of_constr c = of_ext val_constr c let to_constr c = to_ext val_constr c -let constr = repr_ext val_constr +let constr_ = repr_ext val_constr +let constr = typed constr_ (!! T.constr) let of_preterm c = of_ext val_preterm c let to_preterm c = to_ext val_preterm c -let preterm = repr_ext val_preterm +let preterm_ = repr_ext val_preterm +let preterm = typed preterm_ (!! T.preterm) let of_cast c = of_ext val_cast c let to_cast c = to_ext val_cast c -let cast = repr_ext val_cast +let cast_ = repr_ext val_cast +let cast = typed cast_ (!! T.cast) let of_ident c = of_ext val_ident c let to_ident c = to_ext val_ident c -let ident = repr_ext val_ident +let ident_ = repr_ext val_ident +let ident = typed ident_ (!! T.ident) let of_pattern c = of_ext val_pattern c let to_pattern c = to_ext val_pattern c -let pattern = repr_ext val_pattern +let pattern_ = repr_ext val_pattern +let pattern = typed pattern_ (!! T.pattern) let of_evar ev = of_ext val_evar ev let to_evar ev = to_ext val_evar ev -let evar = repr_ext val_evar +let evar_ = repr_ext val_evar +let evar = typed evar_ (!! T.evar) let internal_err = let open Names in @@ -203,14 +275,16 @@ let internal_err = let of_exninfo = of_ext val_exninfo let to_exninfo = to_ext val_exninfo -let exninfo = { +let exninfo_ = { r_of = of_exninfo; r_to = to_exninfo; } +let exninfo = typed exninfo_ (!! T.exninfo) let of_err e = of_ext val_exn e let to_err e = to_ext val_exn e -let err = repr_ext val_exn +let err_ = repr_ext val_exn +let err = typed err_ (!! T.err) (** FIXME: handle backtrace in Ltac2 exceptions *) let of_exn c = match fst c with @@ -225,11 +299,13 @@ let to_exn c = match c with (LtacError (kn, c), Exninfo.null) | _ -> assert false -let exn = { +let exn_ = { r_of = of_exn; r_to = to_exn; } +let exn = typed exn_ (!! T.exn) + let of_option f = function | None -> ValInt 0 | Some c -> ValBlk (0, [|f c|]) @@ -239,14 +315,17 @@ let to_option f = function | ValBlk (0, [|c|]) -> Some (f c) | _ -> assert false -let option r = { +let option_ r = { r_of = (fun l -> of_option r.r_of l); r_to = (fun l -> to_option r.r_to l); } +let option (r,t) = typed (option_ r) (! T.option [default t]) + let of_pp c = of_ext val_pp c let to_pp c = to_ext val_pp c -let pp = repr_ext val_pp +let pp_ = repr_ext val_pp +let pp = typed pp_ (!! T.message) let of_tuple cl = ValBlk (0, cl) let to_tuple = function @@ -257,28 +336,32 @@ let of_pair f g (x, y) = ValBlk (0, [|f x; g y|]) let to_pair f g = function | ValBlk (0, [|x; y|]) -> (f x, g y) | _ -> assert false -let pair r0 r1 = { +let pair_ r0 r1 = { r_of = (fun p -> of_pair r0.r_of r1.r_of p); r_to = (fun p -> to_pair r0.r_to r1.r_to p); } +let pair (r0,t0) (r1,t1) = typed (pair_ r0 r1) (tuple [default t0; default t1]) + let of_triple f g h (x, y, z) = ValBlk (0, [|f x; g y; h z|]) let to_triple f g h = function | ValBlk (0, [|x; y; z|]) -> (f x, g y, h z) | _ -> assert false -let triple r0 r1 r2 = { +let triple_ r0 r1 r2 = { r_of = (fun p -> of_triple r0.r_of r1.r_of r2.r_of p); r_to = (fun p -> to_triple r0.r_to r1.r_to r2.r_to p); } +let triple (r0,t0) (r1,t1) (r2,t2) = typed (triple_ r0 r1 r2) (tuple [default t0; default t1; default t2]) let of_array f vl = ValBlk (0, Array.map f vl) let to_array f = function | ValBlk (0, vl) -> Array.map f vl | _ -> assert false -let array r = { +let array_ r = { r_of = (fun l -> of_array r.r_of l); r_to = (fun l -> to_array r.r_to l); } +let array (r,t) = typed (array_ r) (! T.array [default t]) let of_block (n, args) = ValBlk (n, args) let to_block = function @@ -290,6 +373,21 @@ let block = { r_to = to_block; } +let of_result r = function + | Ok x -> of_block (0, [|r x|]) + | Error x -> of_block (1, [|of_exn x|]) + +let to_result r = function + | ValBlk (0, [|x|]) -> Ok (r x) + | ValBlk (1, [|x|]) -> Error (to_exn x) + | _ -> assert false + +let result_ r = { + r_of = of_result r.r_of; + r_to = to_result r.r_to; +} +let result (r,t) = typed (result_ r) (! T.result [default t]) + let of_open (kn, args) = ValOpn (kn, args) let to_open = function @@ -304,22 +402,25 @@ let open_ = { let of_uint63 n = of_ext val_uint63 n let to_uint63 x = to_ext val_uint63 x -let uint63 = { +let uint63_ = { r_of = of_uint63; r_to = to_uint63; } +let uint63 = typed uint63_ (!! T.uint63) let of_float f = of_ext val_float f let to_float x = to_ext val_float x -let float = { +let float_ = { r_of = of_float; r_to = to_float; } +let float = typed float_ (!! T.float) let of_constant c = of_ext val_constant c let to_constant c = to_ext val_constant c -let constant = repr_ext val_constant +let constant_ = repr_ext val_constant +let constant = typed constant_ (!! T.constant) let of_reference = let open Names.GlobRef in function | VarRef id -> ValBlk (0, [| of_ident id |]) @@ -334,16 +435,61 @@ let to_reference = let open Names.GlobRef in function | ValBlk (3, [| cstr |]) -> ConstructRef (to_ext val_constructor cstr) | _ -> assert false -let reference = { +let reference_ = { r_of = of_reference; r_to = to_reference; } +let reference = typed reference_ (!! T.reference) -type ('a, 'b) fun1 = closure +(* f is supposed to be pure (unit -> 'a tactic with any effects inside the tactic) *) +let thaw f = f () + +let to_fun1 r0 r' f = + let f x = + Proofview.Monad.map r' @@ Tac2val.apply (to_closure f) [r0 x] + in + f + +let of_fun1 r0 r' f = + of_closure @@ + Tac2val.abstract 1 (function + | [x] -> Proofview.Monad.map r' @@ f (r0 x) + | _ -> assert false) + +let fun1_ r r' = make_repr (of_fun1 r.r_to r'.r_of) (to_fun1 r.r_of r'.r_to) +let fun1 (r,t) (r',t') = fun1_ r r', Some Types.(default t @-> default t') + +let thunk r = fun1 unit r + +let to_fun2 r0 r1 r' f = + let f x y = + Proofview.Monad.map r' @@ + Tac2val.apply (to_closure f) [r0 x; r1 y] + in + f + +let of_fun2 r0 r1 r' f = + of_closure @@ + Tac2val.abstract 2 (function + | [x;y] -> Proofview.Monad.map r' @@ f (r0 x) (r1 y) + | _ -> assert false) + +let fun2_ r0 r1 r' = make_repr (of_fun2 r0.r_to r1.r_to r'.r_of) (to_fun2 r0.r_of r1.r_of r'.r_to) +let fun2 (r0,t0) (r1,t1) (r',t') = fun2_ r0 r1 r', Some Types.(default t0 @-> default t1 @-> default t') + +let to_fun3 r0 r1 r2 r' f = + let f x y z = + Proofview.Monad.map r' @@ + Tac2val.apply (to_closure f) [r0 x; r1 y; r2 z] + in + f -let fun1 (r0 : 'a repr) (r1 : 'b repr) : ('a, 'b) fun1 repr = closure -let to_fun1 r0 r1 f = to_closure f +let of_fun3 r0 r1 r2 r' f = + of_closure @@ + Tac2val.abstract 3 (function + | [x;y;z] -> Proofview.Monad.map r' @@ f (r0 x) (r1 y) (r2 z) + | _ -> assert false) -let app_fun1 cls r0 r1 x = - let open Proofview.Notations in - apply cls [r0.r_of x] >>= fun v -> Proofview.tclUNIT (r1.r_to v) +let fun3_ r0 r1 r2 r' = make_repr (of_fun3 r0.r_to r1.r_to r2.r_to r'.r_of) (to_fun3 r0.r_of r1.r_of r2.r_of r'.r_to) +let fun3 (r0,t0) (r1,t1) (r2,t2) (r',t') = + fun3_ r0 r1 r2 r', Some Types.(default t0 @-> default t1 @-> default t2 @-> default t') diff --git a/plugins/ltac2/tac2ffi.mli b/plugins/ltac2/tac2ffi.mli index ca5946e99410..903daca68d3a 100644 --- a/plugins/ltac2/tac2ffi.mli +++ b/plugins/ltac2/tac2ffi.mli @@ -24,66 +24,122 @@ val make_repr : ('a -> valexpr) -> (valexpr -> 'a) -> 'a repr val map_repr : ('a -> 'b) -> ('b -> 'a) -> 'a repr -> 'b repr +(** Type annotations. *) + +module Types : sig + + type t + (** Type of an argument of an external. This is basically + [int Tac2expr.glb_typexpr] but we may add some smart constructors + so that the user doesn't need to pick a number for variables used only once. *) + + val any : t + + val default : t option -> t + + val var : int -> t + + val tuple : t list -> t + + val (!) : Tac2expr.type_constant -> t list -> t + + val (!!) : Tac2expr.type_constant -> t + (** Alias of [(!)] for 0-ary type formers. *) + + val (@->) : t -> t -> t + + val as_scheme : t -> Tac2expr.type_scheme + +end + +type 'a annotated = 'a * Types.t option + +val typed : 'r -> Types.t -> 'r annotated +val untyped : 'r -> 'r annotated + (** These functions allow to convert back and forth between OCaml and Ltac2 data representation. The [to_*] functions raise an anomaly whenever the data - has not expected shape. *) + has not expected shape. + + Unless no default annotation is useful, [foo_] is the raw converter + and [foo] annotates it with types taking any necessary type arguments. +*) val of_unit : unit -> valexpr val to_unit : valexpr -> unit -val unit : unit repr +val unit : unit repr annotated +val unit_ : unit repr val of_int : int -> valexpr val to_int : valexpr -> int -val int : int repr +val int : int repr annotated +val int_ : int repr val of_bool : bool -> valexpr val to_bool : valexpr -> bool -val bool : bool repr +val bool : bool repr annotated +val bool_ : bool repr val of_char : char -> valexpr val to_char : valexpr -> char -val char : char repr +val char : char repr annotated +val char_ : char repr val of_bytes : Bytes.t -> valexpr val to_bytes : valexpr -> Bytes.t -val bytes : Bytes.t repr +val bytes : Bytes.t repr annotated +val bytes_ : Bytes.t repr (** WARNING these functions copy *) val of_string : string -> valexpr val to_string : valexpr -> string -val string : string repr +val string : string repr annotated +val string_ : string repr val of_list : ('a -> valexpr) -> 'a list -> valexpr val to_list : (valexpr -> 'a) -> valexpr -> 'a list -val list : 'a repr -> 'a list repr +val list : 'a repr annotated -> 'a list repr annotated +val list_ : 'a repr -> 'a list repr val of_constr : EConstr.t -> valexpr val to_constr : valexpr -> EConstr.t -val constr : EConstr.t repr +val constr : EConstr.t repr annotated +val constr_ : EConstr.t repr val of_preterm : Ltac_pretype.closed_glob_constr -> valexpr val to_preterm : valexpr -> Ltac_pretype.closed_glob_constr -val preterm : Ltac_pretype.closed_glob_constr repr +val preterm : Ltac_pretype.closed_glob_constr repr annotated +val preterm_ : Ltac_pretype.closed_glob_constr repr val of_cast : Constr.cast_kind -> valexpr val to_cast : valexpr -> Constr.cast_kind -val cast : Constr.cast_kind repr +val cast : Constr.cast_kind repr annotated +val cast_ : Constr.cast_kind repr val of_err : Exninfo.iexn -> valexpr val to_err : valexpr -> Exninfo.iexn -val err : Exninfo.iexn repr +val err : Exninfo.iexn repr annotated +val err_ : Exninfo.iexn repr val of_exn : Exninfo.iexn -> valexpr val to_exn : valexpr -> Exninfo.iexn -val exn : Exninfo.iexn repr +val exn : Exninfo.iexn repr annotated +val exn_ : Exninfo.iexn repr + +val of_result : ('a -> valexpr) -> ('a, Exninfo.iexn) result -> valexpr +val to_result : (valexpr -> 'a) -> valexpr -> ('a, Exninfo.iexn) result +val result_ : 'a repr -> ('a, Exninfo.iexn) result repr +val result : 'a repr annotated -> ('a, Exninfo.iexn) result repr annotated val of_exninfo : Exninfo.info -> valexpr val to_exninfo : valexpr -> Exninfo.info -val exninfo : Exninfo.info repr +val exninfo : Exninfo.info repr annotated +val exninfo_ : Exninfo.info repr val of_ident : Id.t -> valexpr val to_ident : valexpr -> Id.t -val ident : Id.t repr +val ident : Id.t repr annotated +val ident_ : Id.t repr val of_closure : closure -> valexpr val to_closure : valexpr -> closure @@ -95,42 +151,51 @@ val block : (int * valexpr array) repr val of_array : ('a -> valexpr) -> 'a array -> valexpr val to_array : (valexpr -> 'a) -> valexpr -> 'a array -val array : 'a repr -> 'a array repr +val array : 'a repr annotated -> 'a array repr annotated +val array_ : 'a repr -> 'a array repr val of_tuple : valexpr array -> valexpr val to_tuple : valexpr -> valexpr array val of_pair : ('a -> valexpr) -> ('b -> valexpr) -> 'a * 'b -> valexpr val to_pair : (valexpr -> 'a) -> (valexpr -> 'b) -> valexpr -> 'a * 'b -val pair : 'a repr -> 'b repr -> ('a * 'b) repr +val pair : 'a repr annotated -> 'b repr annotated -> ('a * 'b) repr annotated +val pair_ : 'a repr -> 'b repr -> ('a * 'b) repr val of_triple : ('a -> valexpr) -> ('b -> valexpr) -> ('c -> valexpr) -> 'a * 'b * 'c -> valexpr val to_triple : (valexpr -> 'a) -> (valexpr -> 'b) -> (valexpr -> 'c) -> valexpr -> 'a * 'b * 'c -val triple : 'a repr -> 'b repr -> 'c repr -> ('a * 'b * 'c) repr +val triple : 'a repr annotated -> 'b repr annotated -> 'c repr annotated -> ('a * 'b * 'c) repr annotated +val triple_ : 'a repr -> 'b repr -> 'c repr -> ('a * 'b * 'c) repr val of_option : ('a -> valexpr) -> 'a option -> valexpr val to_option : (valexpr -> 'a) -> valexpr -> 'a option -val option : 'a repr -> 'a option repr +val option : 'a repr annotated -> 'a option repr annotated +val option_ : 'a repr -> 'a option repr val of_pattern : Pattern.constr_pattern -> valexpr val to_pattern : valexpr -> Pattern.constr_pattern -val pattern : Pattern.constr_pattern repr +val pattern : Pattern.constr_pattern repr annotated +val pattern_ : Pattern.constr_pattern repr val of_evar : Evar.t -> valexpr val to_evar : valexpr -> Evar.t -val evar : Evar.t repr +val evar : Evar.t repr annotated +val evar_ : Evar.t repr val of_pp : Pp.t -> valexpr val to_pp : valexpr -> Pp.t -val pp : Pp.t repr +val pp : Pp.t repr annotated +val pp_ : Pp.t repr val of_constant : Constant.t -> valexpr val to_constant : valexpr -> Constant.t -val constant : Constant.t repr +val constant : Constant.t repr annotated +val constant_ : Constant.t repr val of_reference : GlobRef.t -> valexpr val to_reference : valexpr -> GlobRef.t -val reference : GlobRef.t repr +val reference : GlobRef.t repr annotated +val reference_ : GlobRef.t repr val of_ext : 'a Val.tag -> 'a -> valexpr val to_ext : 'a Val.tag -> valexpr -> 'a @@ -142,21 +207,39 @@ val open_ : (KerName.t * valexpr array) repr val of_uint63 : Uint63.t -> valexpr val to_uint63 : valexpr -> Uint63.t -val uint63 : Uint63.t repr +val uint63 : Uint63.t repr annotated +val uint63_ : Uint63.t repr val of_float : Float64.t -> valexpr val to_float : valexpr -> Float64.t -val float : Float64.t repr +val float : Float64.t repr annotated +val float_ : Float64.t repr + +val thaw : (unit -> 'a Proofview.tactic) -> 'a Proofview.tactic +(** The OCaml closure is suppoed to be pure, with any effects being inside the [tactic] value. *) -type ('a, 'b) fun1 +val to_fun1 : ('a -> valexpr) -> (valexpr -> 'r) -> valexpr -> 'a -> 'r Proofview.tactic +val of_fun1 : (valexpr -> 'a) -> ('r -> valexpr) -> ('a -> 'r Proofview.tactic) -> valexpr +val fun1_ : 'a repr -> 'r repr -> ('a -> 'r Proofview.tactic) repr +val fun1 : 'a repr annotated -> 'r repr annotated -> ('a -> 'r Proofview.tactic) repr annotated -val app_fun1 : ('a, 'b) fun1 -> 'a repr -> 'b repr -> 'a -> 'b Proofview.tactic +val thunk : 'a repr annotated -> (unit -> 'a Proofview.tactic) repr annotated -val to_fun1 : 'a repr -> 'b repr -> valexpr -> ('a, 'b) fun1 -val fun1 : 'a repr -> 'b repr -> ('a, 'b) fun1 repr +val to_fun2 : ('a -> valexpr) -> ('b -> valexpr) -> (valexpr -> 'r) -> valexpr -> 'a -> 'b -> 'r Proofview.tactic +val of_fun2 : (valexpr -> 'a) -> (valexpr -> 'b) -> ('r -> valexpr) -> ('a -> 'b -> 'r Proofview.tactic) -> valexpr +val fun2_ : 'a repr -> 'b repr -> 'r repr -> ('a -> 'b -> 'r Proofview.tactic) repr +val fun2 : 'a repr annotated -> 'b repr annotated -> 'r repr annotated -> ('a -> 'b -> 'r Proofview.tactic) repr annotated + +val to_fun3 : ('a -> valexpr) -> ('b -> valexpr) -> ('c -> valexpr) -> (valexpr -> 'r) -> valexpr -> 'a -> 'b -> 'c -> 'r Proofview.tactic +val of_fun3 : (valexpr -> 'a) -> (valexpr -> 'b) -> (valexpr -> 'c) -> ('r -> valexpr) -> ('a -> 'b -> 'c -> 'r Proofview.tactic) -> valexpr +val fun3_ : 'a repr -> 'b repr -> 'c repr -> 'r repr -> ('a -> 'b -> 'c -> 'r Proofview.tactic) repr +val fun3 : 'a repr annotated -> 'b repr annotated -> 'c repr annotated -> 'r repr annotated -> ('a -> 'b -> 'c -> 'r Proofview.tactic) repr annotated val valexpr : valexpr repr +(** Most common use of valexpr is at type var 0. *) +val valexpr_0 : valexpr repr annotated + (** {5 Dynamic tags} *) val val_constr : EConstr.t Val.tag @@ -180,7 +263,6 @@ val val_quality : Sorts.Quality.t Val.tag val val_free : Id.Set.t Val.tag val val_uint63 : Uint63.t Val.tag val val_float : Float64.t Val.tag -val val_ltac1 : Geninterp.Val.t Val.tag val val_pretype_flags : Pretyping.inference_flags Val.tag val val_expected_type : Pretyping.typing_constraint Val.tag diff --git a/plugins/ltac2/tac2globals.ml b/plugins/ltac2/tac2globals.ml new file mode 100644 index 000000000000..b01de29e8b64 --- /dev/null +++ b/plugins/ltac2/tac2globals.ml @@ -0,0 +1,96 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* MPdot (mp, s2l modname)) (MPfile dp) modules in + KerName.make mp (s2l label) + +let mk_init n = mk "Init" [] n + +let mk_std n = mk "Std" [] n + +module Types = struct + let unit = mk_init "unit" + let list = mk_init "list" + let int = mk_init "int" + let string = mk_init "string" + let char = mk_init "char" + let ident = mk_init "ident" + let uint63 = mk_init "uint63" + let float = mk_init "float" + let meta = mk_init "meta" + let evar = mk_init "evar" + let sort = mk_init "sort" + let cast = mk_init "cast" + let instance = mk_init "instance" + let constant = mk_init "constant" + let inductive = mk_init "inductive" + let constructor = mk_init "constructor" + let projection = mk_init "projection" + let pattern = mk_init "pattern" + let constr = mk_init "constr" + let preterm = mk_init "preterm" + let binder = mk_init "binder" + let message = mk_init "message" + let format = mk_init "format" + let exn = mk_init "exn" + let array = mk_init "array" + let option = mk_init "option" + let bool = mk_init "bool" + let result = mk_init "result" + let err = mk_init "err" + let exninfo = mk_init "exninfo" + + let reference = mk_std "reference" + let occurrences = mk_std "occurrences" + let intro_pattern = mk_std "intro_pattern" + let bindings = mk_std "bindings" + let assertion = mk_std "assertion" + let clause = mk_std "clause" + let induction_clause = mk_std "induction_clause" + let red_flags = mk_std "red_flags" + let rewriting = mk_std "rewriting" + let inversion_kind = mk_std "inversion_kind" + let destruction_arg = mk_std "destruction_arg" + let move_location = mk_std "move_location" + let hypothesis = mk_std "hypothesis" + let std_debug = mk_std "debug" + let std_strategy = mk_std "strategy" + let orientation = mk_std "orientation" + + let transparent_state = mk "TransparentState" [] "t" + + let relevance = mk "Constr" ["Binder"] "relevance" + + let constr_kind = mk "Constr" ["Unsafe"] "kind" + let constr_case = mk "Constr" ["Unsafe"] "case" + + let pretype_flags = mk "Constr" ["Pretype";"Flags"] "t" + + let pretype_expected_type = mk "Constr" ["Pretype"] "expected_type" + + let matching_context = mk "Pattern" [] "context" + + let match_kind = mk "Pattern" [] "match_kind" + + let free = mk "Fresh" ["Free"] "t" + + let ind_data = mk "Ind" [] "data" + + let map_tag = mk "FSet" ["Tags"] "tag" + + let fset = mk "FSet" [] "t" + let fmap = mk "FMap" [] "t" +end diff --git a/plugins/ltac2/tac2globals.mli b/plugins/ltac2/tac2globals.mli new file mode 100644 index 000000000000..37eaaa633efa --- /dev/null +++ b/plugins/ltac2/tac2globals.mli @@ -0,0 +1,88 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* assert false) f let return x = Proofview.tclUNIT x -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 + +let uthaw_ r f = to_fun1 of_unit (repr_to r) f () + +let uthaw (r,t) = typed (uthaw_ r) Types.(!! GT.unit @-> default t) let to_name c = match Value.to_option Value.to_ident c with | None -> Anonymous | Some id -> Name id -let name = make_to_repr to_name +let name_ = make_to_repr to_name +let name = name_, snd (option ident) let to_occurrences = function | ValInt 0 -> AllOccurrences @@ -40,7 +44,8 @@ let to_occurrences = function | ValBlk (1, [| vl |]) -> OnlyOccurrences (Value.to_list Value.to_int vl) | _ -> assert false -let occurrences = make_to_repr to_occurrences +let occurrences_ = make_to_repr to_occurrences +let occurrences = typed occurrences_ Types.(!! GT.occurrences) let to_hyp_location_flag v = match Value.to_int v with | 0 -> InHyp @@ -59,7 +64,8 @@ let to_clause v = match Value.to_tuple v with { onhyps = hyps; concl_occs = to_occurrences concl; } | _ -> assert false -let clause = make_to_repr to_clause +let clause_ = make_to_repr to_clause +let clause = typed clause_ Types.(!! GT.clause) let to_red_strength = function | ValInt 0 -> Norm @@ -80,7 +86,8 @@ let to_red_flag v = match Value.to_tuple v with } | _ -> assert false -let red_flags = make_to_repr to_red_flag +let red_flags_ = make_to_repr to_red_flag +let red_flags = typed red_flags_ Types.(!! GT.red_flags) let pattern_with_occs = pair pattern occurrences @@ -107,7 +114,7 @@ and to_intro_pattern_action = function let map ipat = to_intro_pattern ipat in IntroInjection (Value.to_list map inj) | ValBlk (2, [| c; ipat |]) -> - let c = Value.to_fun1 Value.unit Value.constr c in + let c = Value.to_fun1 of_unit to_constr c in IntroApplyOn (c, to_intro_pattern ipat) | ValBlk (3, [| b |]) -> IntroRewrite (Value.to_bool b) | _ -> assert false @@ -137,7 +144,7 @@ and of_intro_pattern_action = function | IntroOrAndPattern op -> of_block (0, [|of_or_and_intro_pattern op|]) | IntroInjection inj -> of_block (1, [|of_list of_intro_pattern inj|]) | IntroApplyOn (c, ipat) -> - let c = repr_of (fun1 unit constr) c in + let c = of_fun1 to_unit of_constr c in of_block (2, [|c; of_intro_pattern ipat|]) | IntroRewrite b -> of_block (3, [|of_bool b|]) @@ -147,19 +154,22 @@ and of_or_and_intro_pattern = function and of_intro_patterns il = of_list of_intro_pattern il -let intro_pattern = make_repr of_intro_pattern to_intro_pattern +let intro_pattern_ = make_repr of_intro_pattern to_intro_pattern -let intro_patterns = make_repr of_intro_patterns to_intro_patterns +let intro_pattern = typed intro_pattern_ Types.(!! GT.intro_pattern) + +let intro_patterns = list intro_pattern let to_destruction_arg v = match Value.to_block v with | (0, [| c |]) -> - let c = uthaw constr_with_bindings c in + let c = uthaw_ (fst constr_with_bindings) c in ElimOnConstr c | (1, [| id |]) -> ElimOnIdent (Value.to_ident id) | (2, [| n |]) -> ElimOnAnonHyp (Value.to_int n) | _ -> assert false -let destruction_arg = make_to_repr to_destruction_arg +let destruction_arg_ = make_to_repr to_destruction_arg +let destruction_arg = typed destruction_arg_ Types.(!! GT.destruction_arg) let to_induction_clause v = match Value.to_tuple v with | [| arg; eqn; as_; in_ |] -> @@ -171,11 +181,12 @@ let to_induction_clause v = match Value.to_tuple v with | _ -> assert false -let induction_clause = make_to_repr to_induction_clause +let induction_clause_ = make_to_repr to_induction_clause +let induction_clause = typed induction_clause_ Types.(!! GT.induction_clause) let to_assertion v = match Value.to_block v with | (0, [| ipat; t; tac |]) -> - let to_tac t = Value.to_fun1 Value.unit Value.unit t in + let to_tac t = Value.to_fun1 of_unit to_unit t in let ipat = Value.to_option to_intro_pattern ipat in let t = Value.to_constr t in let tac = Value.to_option to_tac tac in @@ -184,7 +195,8 @@ let to_assertion v = match Value.to_block v with AssertValue (Value.to_ident id, Value.to_constr c) | _ -> assert false -let assertion = make_to_repr to_assertion +let assertion_ = make_to_repr to_assertion +let assertion = typed assertion_ Types.(!! GT.assertion) let to_multi = function | ValBlk (0, [| n |]) -> Precisely (Value.to_int n) @@ -197,11 +209,12 @@ let to_rewriting v = match Value.to_tuple v with | [| orient; repeat; c |] -> let orient = Value.to_option Value.to_bool orient in let repeat = to_multi repeat in - let c = uthaw constr_with_bindings c in + let c = uthaw_ (fst constr_with_bindings) c in (orient, repeat, c) | _ -> assert false -let rewriting = make_to_repr to_rewriting +let rewriting_ = make_to_repr to_rewriting +let rewriting = typed rewriting_ Types.(!! GT.rewriting) let to_debug v = match Value.to_int v with | 0 -> Hints.Off @@ -209,14 +222,16 @@ let to_debug v = match Value.to_int v with | 2 -> Hints.Debug | _ -> assert false -let debug = make_to_repr to_debug +let debug_ = make_to_repr to_debug +let debug = typed debug_ Types.(!! GT.std_debug) let to_strategy v = match Value.to_int v with | 0 -> Class_tactics.Bfs | 1 -> Class_tactics.Dfs | _ -> assert false -let strategy = make_to_repr to_strategy +let strategy_ = make_to_repr to_strategy +let strategy = typed strategy_ Types.(!! GT.std_strategy) let to_inversion_kind v = match Value.to_int v with | 0 -> Inv.SimpleInversion @@ -224,7 +239,8 @@ let to_inversion_kind v = match Value.to_int v with | 2 -> Inv.FullInversionClear | _ -> assert false -let inversion_kind = make_to_repr to_inversion_kind +let inversion_kind_ = make_to_repr to_inversion_kind +let inversion_kind = typed inversion_kind_ Types.(!! GT.inversion_kind) let to_move_location = function | ValInt 0 -> Logic.MoveFirst @@ -233,14 +249,10 @@ let to_move_location = function | ValBlk (1, [|id|]) -> Logic.MoveBefore (Value.to_ident id) | _ -> assert false -let move_location = make_to_repr to_move_location - -let to_generalize_arg v = match Value.to_tuple v with -| [| c; occs; na |] -> - (Value.to_constr c, to_occurrences occs, to_name na) -| _ -> assert false +let move_location_ = make_to_repr to_move_location +let move_location = typed move_location_ Types.(!! GT.move_location) -let generalize_arg = make_to_repr to_generalize_arg +let generalize_arg = triple constr occurrences name (** Standard tactics sharing their implementation with Ltac1 *) @@ -283,7 +295,7 @@ let () = Tac2tactics.assert_ let tac_enough c tac ipat = - let tac = Option.map (fun o -> Option.map (fun f -> thaw unit f) o) tac in + let tac = Option.map (fun o -> Option.map (fun f -> thaw f) o) tac in Tac2tactics.forward false tac ipat c let () = define "tac_enough" @@ -298,7 +310,7 @@ let () = let tac_set ev p cl = Proofview.tclEVARMAP >>= fun sigma -> - thaw (pair name constr) p >>= fun (na, c) -> + thaw p >>= fun (na, c) -> Tac2tactics.letin_pat_tac ev None na (Some sigma, c) cl let () = define "tac_set" @@ -310,7 +322,7 @@ let tac_remember ev na c eqpat cl = match eqpat with | IntroNaming eqpat -> Proofview.tclEVARMAP >>= fun sigma -> - thaw constr c >>= fun c -> + thaw c >>= fun c -> Tac2tactics.letin_pat_tac ev (Some (true, eqpat)) na (Some sigma, c) cl | _ -> Tacticals.tclZEROMSG (Pp.str "Invalid pattern for remember") @@ -431,7 +443,7 @@ let () = let () = define "tac_setoid_rewrite" - (bool @-> uthaw constr_with_bindings @--> occurrences @-> option ident @-> tac unit) + (typed bool_ Types.(!! GT.orientation) @-> uthaw constr_with_bindings @--> occurrences @-> option ident @-> tac unit) Tac2tactics.setoid_rewrite let () = @@ -599,7 +611,8 @@ let () = (** Tactics for [Ltac2/TransparentState.v]. *) -let transparent_state = Tac2ffi.repr_ext Tac2ffi.val_transparent_state +let transparent_state_ = Tac2ffi.repr_ext Tac2ffi.val_transparent_state +let transparent_state = typed transparent_state_ Types.(!! GT.transparent_state) let () = define "current_transparent_state" diff --git a/plugins/ltac2/tac2stdlib.mli b/plugins/ltac2/tac2stdlib.mli index ce7dfc5db4b5..7b0311cafb15 100644 --- a/plugins/ltac2/tac2stdlib.mli +++ b/plugins/ltac2/tac2stdlib.mli @@ -10,4 +10,4 @@ (** Standard tactics sharing their implementation with Ltac1 *) -val intro_pattern : Tac2types.intro_pattern Tac2ffi.repr +val intro_pattern : Tac2types.intro_pattern Tac2ffi.repr Tac2ffi.annotated diff --git a/plugins/ltac2/tac2tactics.ml b/plugins/ltac2/tac2tactics.ml index 6b4ffc315bbe..bf5e6958e7fa 100644 --- a/plugins/ltac2/tac2tactics.ml +++ b/plugins/ltac2/tac2tactics.ml @@ -12,12 +12,10 @@ open Pp open Util open Names open Tac2types -open Tac2extffi open Genredexpr open Proofview.Notations let return = Proofview.tclUNIT -let thaw r f = Tac2ffi.app_fun1 f Tac2ffi.unit r () let tactic_infer_flags with_evar = Pretyping.{ use_coercions = true; @@ -38,7 +36,7 @@ let delayed_of_tactic tac env sigma = (sigma, c) let delayed_of_thunk r tac env sigma = - delayed_of_tactic (thaw r tac) env sigma + delayed_of_tactic (Tac2ffi.thaw tac) env sigma let mk_bindings = function | ImplicitBindings l -> Tactypes.ImplicitBindings l @@ -99,7 +97,7 @@ let intros_patterns ev ipat = let apply adv ev cb cl = let map c = - let c = thaw constr_with_bindings c >>= fun p -> return (mk_with_bindings p) in + let c = Tac2ffi.thaw c >>= fun p -> return (mk_with_bindings p) in None, CAst.make (delayed_of_tactic c) in let cb = List.map map cb in @@ -163,11 +161,10 @@ let specialize c pat = Tactics.specialize c pat let change pat c cl = - let open Tac2ffi in Proofview.Goal.enter begin fun gl -> let c subst env sigma = let subst = Array.map_of_list snd (Id.Map.bindings subst) in - delayed_of_tactic (Tac2ffi.app_fun1 c (array constr) constr subst) env sigma + delayed_of_tactic (c subst) env sigma in let cl = mk_clause cl in Tactics.change ~check:true pat c cl @@ -180,7 +177,7 @@ let rewrite ev rw cl by = in let rw = List.map map_rw rw in let cl = mk_clause cl in - let by = Option.map (fun tac -> Tacticals.tclCOMPLETE (thaw Tac2ffi.unit tac), Equality.Naive) by in + let by = Option.map (fun tac -> Tacticals.tclCOMPLETE (Tac2ffi.thaw tac), Equality.Naive) by in Equality.general_multi_rewrite ev rw cl by let setoid_rewrite orient c occs id = @@ -202,7 +199,7 @@ let assert_ = function Tactics.forward true None (Some ipat) c | AssertType (ipat, c, tac) -> let ipat = Option.map mk_intro_pattern ipat in - let tac = Option.map (fun tac -> thaw Tac2ffi.unit tac) tac in + let tac = Option.map (fun tac -> Tac2ffi.thaw tac) tac in Tactics.forward true (Some tac) ipat c let letin_pat_tac ev ipat na c cl = @@ -378,7 +375,7 @@ let autorewrite ~all by ids cl = match by with | None -> Autorewrite.auto_multi_rewrite ?conds ids cl | Some by -> - let by = thaw Tac2ffi.unit by in + let by = Tac2ffi.thaw by in Autorewrite.auto_multi_rewrite_with ?conds by ids cl (** Auto *) diff --git a/plugins/ltac2/tac2tactics.mli b/plugins/ltac2/tac2tactics.mli index 788918f403b1..f3a2cc55067f 100644 --- a/plugins/ltac2/tac2tactics.mli +++ b/plugins/ltac2/tac2tactics.mli @@ -41,7 +41,7 @@ val split_with_bindings : evars_flag -> bindings -> unit tactic val specialize : constr_with_bindings -> intro_pattern option -> unit tactic -val change : Pattern.constr_pattern option -> (constr array, constr) Tac2ffi.fun1 -> clause -> unit tactic +val change : Pattern.constr_pattern option -> (constr array -> constr Proofview.tactic) -> clause -> unit tactic val rewrite : evars_flag -> rewriting list -> clause -> unit thunk option -> unit tactic diff --git a/plugins/ltac2/tac2types.mli b/plugins/ltac2/tac2types.mli index 73570420c78a..5b4c71fe8710 100644 --- a/plugins/ltac2/tac2types.mli +++ b/plugins/ltac2/tac2types.mli @@ -17,7 +17,7 @@ open Proofview type evars_flag = bool type advanced_flag = bool -type 'a thunk = (unit, 'a) Tac2ffi.fun1 +type 'a thunk = unit -> 'a Proofview.tactic type quantified_hypothesis = Tactypes.quantified_hypothesis = | AnonHyp of int diff --git a/plugins/ltac2_ltac1/tac2core_ltac1.ml b/plugins/ltac2_ltac1/tac2core_ltac1.ml index 7d7e03e28e22..ce5fb03fd511 100644 --- a/plugins/ltac2_ltac1/tac2core_ltac1.ml +++ b/plugins/ltac2_ltac1/tac2core_ltac1.ml @@ -19,6 +19,7 @@ open Tac2env open Tac2expr open Proofview.Notations open Tac2externals +open Tac2ltac1_ffi let ltac2_ltac1_plugin = "coq-core.plugins.ltac2_ltac1" @@ -30,9 +31,6 @@ let return x = Proofview.tclUNIT x (** Ltac1 in Ltac2 *) -let ltac1 = Tac2ffi.repr_ext Tac2ffi.val_ltac1 -let of_ltac1 v = Tac2ffi.of_ext Tac2ffi.val_ltac1 v - let () = define "ltac1_ref" (list ident @-> ret ltac1) @@ fun ids -> let open Ltac_plugin in @@ -55,13 +53,10 @@ let () = Tacinterp.tactic_of_value (Tacinterp.default_ist ()) v let () = - define "ltac1_apply" (ltac1 @-> list ltac1 @-> closure @-> tac unit) @@ fun f args k -> + define "ltac1_apply" (ltac1 @-> list ltac1 @-> fun1 ltac1 unit @-> tac unit) @@ fun f args k -> let open Ltac_plugin in let open Tacexpr in let open Locus in - let k ret = - Proofview.tclIGNORE (Tac2val.apply k [Tac2ffi.of_ext val_ltac1 ret]) - in let fold arg (i, vars, lfun) = let id = Id.of_string ("x" ^ string_of_int i) in let x = Reference (ArgVar CAst.(make id)) in @@ -129,7 +124,7 @@ let () = let interp _ (ids, tac) = let clos args = let add lfun id v = - let v = Tac2ffi.to_ext val_ltac1 v in + let v = to_ltac1 v in Id.Map.add id v lfun in let lfun = List.fold_left2 add Id.Map.empty ids args in @@ -188,7 +183,7 @@ let () = let interp _ (ids, tac) = let clos args = let add lfun id v = - let v = Tac2ffi.to_ext val_ltac1 v in + let v = to_ltac1 v in Id.Map.add id v lfun in let lfun = List.fold_left2 add Id.Map.empty ids args in @@ -196,7 +191,7 @@ let () = let lfun = Tac2interp.set_env ist lfun in let ist = Ltac_plugin.Tacinterp.default_ist () in let ist = { ist with Geninterp.lfun = lfun } in - return (Tac2ffi.of_ext val_ltac1 (Tacinterp.Value.of_closure ist tac)) + return (of_ltac1 (Tacinterp.Value.of_closure ist tac)) in let len = List.length ids in if Int.equal len 0 then @@ -268,11 +263,11 @@ let () = let arg = Id.Map.get arg_id ist.Tacinterp.lfun in let tac = Tac2ffi.to_closure tac in Tac2val.apply tac [of_ltac1 arg] >>= fun ans -> - let ans = Tac2ffi.to_ext val_ltac1 ans in + let ans = to_ltac1 ans in Ftactic.return ans in let () = Geninterp.register_interp0 wit_ltac2_val interp_fun in - define "ltac1_lambda" (valexpr @-> ret ltac1) @@ fun f -> + define "ltac1_lambda" ((valexpr, (snd (fun1 ltac1 ltac1))) @-> ret ltac1) @@ fun f -> let body = Tacexpr.TacGeneric (Some ltac2_ltac1_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 @@ -293,7 +288,7 @@ let ltac2_eval = being the arguments it should be fed with *) let tac = cast_typ typ_ltac2 tac in let tac = Tac2ffi.to_closure tac in - let args = List.map (fun arg -> Tac2ffi.of_ext val_ltac1 arg) args in + let args = List.map (fun arg -> of_ltac1 arg) args in Proofview.tclIGNORE (Tac2val.apply tac args) in let () = Tacenv.register_ml_tactic ml_name [|eval_fun|] in @@ -332,7 +327,7 @@ let () = let interp ist tac = let ist = { env_ist = Id.Map.empty } in Tac2interp.interp ist tac >>= fun v -> - let v = repr_to ltac1 v in + let v = to_ltac1 v in Ftactic.return v in Geninterp.register_interp0 wit_ltac2in1_val interp diff --git a/plugins/ltac2_ltac1/tac2ltac1_ffi.ml b/plugins/ltac2_ltac1/tac2ltac1_ffi.ml new file mode 100644 index 000000000000..1991b7cd29c8 --- /dev/null +++ b/plugins/ltac2_ltac1/tac2ltac1_ffi.ml @@ -0,0 +1,25 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* Geninterp.Val.t +val of_ltac1 : Geninterp.Val.t -> valexpr +val ltac1 : Geninterp.Val.t repr annotated diff --git a/plugins/ltac2_ltac1/tac2stdlib_ltac1.ml b/plugins/ltac2_ltac1/tac2stdlib_ltac1.ml index aac9f63fb1a5..4b6c80511f49 100644 --- a/plugins/ltac2_ltac1/tac2stdlib_ltac1.ml +++ b/plugins/ltac2_ltac1/tac2stdlib_ltac1.ml @@ -17,6 +17,7 @@ open Tac2ffi open Tac2expr open Proofview.Notations open Tac2externals +open Tac2ltac1_ffi let ltac2_ltac1_plugin = "coq-core.plugins.ltac2_ltac1" @@ -24,8 +25,6 @@ let pname ?(plugin=ltac2_ltac1_plugin) s = { mltac_plugin = plugin; mltac_tactic let define ?plugin s = define (pname ?plugin s) -let ltac1 = Tac2ffi.repr_ext Tac2ffi.val_ltac1 - let val_tag wit = match val_tag wit with | Base t -> t | _ -> assert false @@ -69,7 +68,7 @@ and to_intro_pattern_action : Tactypes.delayed_open_constr Tactypes.intro_patter Proofview.Unsafe.tclEVARS sigma >>= fun () -> tclUNIT (of_constr c) in - let c = to_fun1 unit constr (mk_closure_val arity_one (fun _ -> c)) in + let c = to_fun1 of_unit to_constr (mk_closure_val arity_one (fun _ -> c)) in IntroApplyOn (c, to_intro_pattern ipat) | IntroRewrite b -> IntroRewrite b diff --git a/user-contrib/Ltac2/FMap.v b/user-contrib/Ltac2/FMap.v index b9056cdb236d..7d487733eedf 100644 --- a/user-contrib/Ltac2/FMap.v +++ b/user-contrib/Ltac2/FMap.v @@ -29,7 +29,7 @@ Ltac2 @ external find_opt : 'k -> ('k, 'v) t -> 'v option := "coq-core.plugins.l Ltac2 @ external mapi : ('k -> 'v -> 'r) -> ('k, 'v) t -> ('k, 'r) t := "coq-core.plugins.ltac2" "fmap_mapi". -Ltac2 @ external fold : ('k -> 'v -> 'acc) -> ('k, 'v) t -> 'acc -> 'acc := "coq-core.plugins.ltac2" "fmap_fold". +Ltac2 @ external fold : ('k -> 'v -> 'acc -> 'acc) -> ('k, 'v) t -> 'acc -> 'acc := "coq-core.plugins.ltac2" "fmap_fold". Ltac2 @ external cardinal : ('k, 'v) t -> int := "coq-core.plugins.ltac2" "fmap_cardinal".