aboutsummaryrefslogtreecommitdiff
path: root/src/tac2core.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/tac2core.ml')
-rw-r--r--src/tac2core.ml648
1 files changed, 648 insertions, 0 deletions
diff --git a/src/tac2core.ml b/src/tac2core.ml
new file mode 100644
index 0000000000..91a3bfa168
--- /dev/null
+++ b/src/tac2core.ml
@@ -0,0 +1,648 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open CSig
+open Pp
+open Names
+open Genarg
+open Geninterp
+open Tac2env
+open Tac2expr
+open Tac2interp
+open Proofview.Notations
+
+(** Standard values *)
+
+let coq_core n = KerName.make2 Tac2env.coq_prefix (Label.of_id (Id.of_string_soft n))
+
+let val_tag t = match val_tag t with
+| Val.Base t -> t
+| _ -> assert false
+
+let val_constr = val_tag (topwit Stdarg.wit_constr)
+let val_ident = val_tag (topwit Stdarg.wit_ident)
+let val_pp = Val.create "ltac2:pp"
+
+let extract_val (type a) (tag : a Val.typ) (Val.Dyn (tag', v)) : a =
+match Val.eq tag tag' with
+| None -> assert false
+| Some Refl -> v
+
+module Core =
+struct
+
+let t_int = coq_core "int"
+let t_string = coq_core "string"
+let t_array = coq_core "array"
+let t_unit = coq_core "unit"
+let t_list = coq_core "list"
+let t_constr = coq_core "constr"
+let t_ident = coq_core "ident"
+let t_option = coq_core "option"
+
+let c_nil = coq_core "[]"
+let c_cons = coq_core "::"
+
+let c_none = coq_core "None"
+let c_some = coq_core "Some"
+
+end
+
+open Core
+
+let v_unit = ValInt 0
+let v_nil = ValInt 0
+let v_cons v vl = ValBlk (0, [|v; vl|])
+
+module Value =
+struct
+
+let of_unit () = v_unit
+
+let to_unit = function
+| ValInt 0 -> ()
+| _ -> assert false
+
+let of_int n = ValInt n
+let to_int = function
+| ValInt n -> n
+| _ -> assert false
+
+let of_bool b = if b then ValInt 0 else ValInt 1
+
+let to_bool = function
+| ValInt 0 -> true
+| ValInt 1 -> false
+| _ -> assert false
+
+let of_char n = ValInt (Char.code n)
+let to_char = function
+| ValInt n -> Char.chr n
+| _ -> assert false
+
+let of_string s = ValStr s
+let to_string = function
+| ValStr s -> s
+| _ -> assert false
+
+let rec of_list = function
+| [] -> v_nil
+| x :: l -> v_cons x (of_list l)
+
+let rec to_list = function
+| ValInt 0 -> []
+| ValBlk (0, [|v; vl|]) -> v :: to_list vl
+| _ -> assert false
+
+let of_ext tag c =
+ ValExt (Val.Dyn (tag, c))
+
+let to_ext tag = function
+| ValExt e -> extract_val tag e
+| _ -> assert false
+
+let of_constr c = of_ext val_constr c
+let to_constr c = to_ext val_constr c
+
+let of_ident c = of_ext val_ident c
+let to_ident c = to_ext val_ident c
+
+(** FIXME: handle backtrace in Ltac2 exceptions *)
+let of_exn c = match fst c with
+| LtacError (kn, c) -> ValOpn (kn, c)
+| _ -> of_ext val_exn c
+
+let to_exn c = match c with
+| ValOpn (kn, c) -> (LtacError (kn, c), Exninfo.null)
+| _ -> to_ext val_exn c
+
+let of_pp c = of_ext val_pp c
+let to_pp c = to_ext val_pp c
+
+end
+
+let val_valexpr = Val.create "ltac2:valexpr"
+
+(** Stdlib exceptions *)
+
+let err_notfocussed =
+ LtacError (coq_core "Not_focussed", [||])
+
+let err_outofbounds =
+ LtacError (coq_core "Out_of_bounds", [||])
+
+let err_notfound =
+ LtacError (coq_core "Not_found", [||])
+
+(** Helper functions *)
+
+let thaw f = interp_app f [v_unit]
+let throw e = Proofview.tclLIFT (Proofview.NonLogical.raise e)
+
+let return x = Proofview.tclUNIT x
+let pname s = { mltac_plugin = "ltac2"; mltac_tactic = s }
+
+let wrap f =
+ return () >>= fun () -> return (f ())
+
+let wrap_unit f =
+ return () >>= fun () -> f (); return v_unit
+
+let pf_apply f =
+ Proofview.Goal.goals >>= function
+ | [] ->
+ Proofview.tclENV >>= fun env ->
+ Proofview.tclEVARMAP >>= fun sigma ->
+ f env sigma
+ | [gl] ->
+ gl >>= fun gl ->
+ f (Proofview.Goal.env gl) (Tacmach.New.project gl)
+ | _ :: _ :: _ ->
+ throw err_notfocussed
+
+(** Primitives *)
+
+(** Printing *)
+
+let prm_print : ml_tactic = function
+| [pp] -> wrap_unit (fun () -> Feedback.msg_notice (Value.to_pp pp))
+| _ -> assert false
+
+let prm_message_of_int : ml_tactic = function
+| [ValInt s] -> return (ValExt (Val.Dyn (val_pp, int s)))
+| _ -> assert false
+
+let prm_message_of_string : ml_tactic = function
+| [ValStr s] -> return (ValExt (Val.Dyn (val_pp, str (Bytes.to_string s))))
+| _ -> assert false
+
+let prm_message_of_constr : ml_tactic = function
+| [c] ->
+ pf_apply begin fun env sigma ->
+ let c = Value.to_constr c in
+ let pp = Printer.pr_econstr_env env sigma c in
+ return (ValExt (Val.Dyn (val_pp, pp)))
+ end
+| _ -> assert false
+
+let prm_message_concat : ml_tactic = function
+| [m1; m2] ->
+ let m1 = Value.to_pp m1 in
+ let m2 = Value.to_pp m2 in
+ return (Value.of_pp (Pp.app m1 m2))
+| _ -> assert false
+
+(** Array *)
+
+let prm_array_make : ml_tactic = function
+| [ValInt n; x] ->
+ if n < 0 || n > Sys.max_array_length then throw err_outofbounds
+ else wrap (fun () -> ValBlk (0, Array.make n x))
+| _ -> assert false
+
+let prm_array_length : ml_tactic = function
+| [ValBlk (_, v)] -> return (ValInt (Array.length v))
+| _ -> assert false
+
+let prm_array_set : ml_tactic = function
+| [ValBlk (_, v); ValInt n; x] ->
+ if n < 0 || n >= Array.length v then throw err_outofbounds
+ else wrap_unit (fun () -> v.(n) <- x)
+| _ -> assert false
+
+let prm_array_get : ml_tactic = function
+| [ValBlk (_, v); ValInt n] ->
+ if n < 0 || n >= Array.length v then throw err_outofbounds
+ else wrap (fun () -> v.(n))
+| _ -> assert false
+
+(** Int *)
+
+let prm_int_equal : ml_tactic = function
+| [m; n] ->
+ return (Value.of_bool (Value.to_int m == Value.to_int n))
+| _ -> assert false
+
+let binop f : ml_tactic = function
+| [m; n] -> return (Value.of_int (f (Value.to_int m) (Value.to_int n)))
+| _ -> assert false
+
+let prm_int_compare args = binop Int.compare args
+let prm_int_add args = binop (+) args
+let prm_int_sub args = binop (-) args
+let prm_int_mul args = binop ( * ) args
+
+let prm_int_neg : ml_tactic = function
+| [m] -> return (Value.of_int (~- (Value.to_int m)))
+| _ -> assert false
+
+(** String *)
+
+let prm_string_make : ml_tactic = function
+| [n; c] ->
+ let n = Value.to_int n in
+ let c = Value.to_char c in
+ if n < 0 || n > Sys.max_string_length then throw err_outofbounds
+ else wrap (fun () -> Value.of_string (Bytes.make n c))
+| _ -> assert false
+
+let prm_string_length : ml_tactic = function
+| [s] ->
+ return (Value.of_int (Bytes.length (Value.to_string s)))
+| _ -> assert false
+
+let prm_string_set : ml_tactic = function
+| [s; n; c] ->
+ let s = Value.to_string s in
+ let n = Value.to_int n in
+ let c = Value.to_char c in
+ if n < 0 || n >= Bytes.length s then throw err_outofbounds
+ else wrap_unit (fun () -> Bytes.set s n c)
+| _ -> assert false
+
+let prm_string_get : ml_tactic = function
+| [s; n] ->
+ let s = Value.to_string s in
+ let n = Value.to_int n in
+ if n < 0 || n >= Bytes.length s then throw err_outofbounds
+ else wrap (fun () -> Value.of_char (Bytes.get s n))
+| _ -> assert false
+
+(** Terms *)
+
+(** constr -> constr *)
+let prm_constr_type : ml_tactic = function
+| [c] ->
+ let c = Value.to_constr c in
+ let get_type env sigma =
+ Proofview.V82.wrap_exceptions begin fun () ->
+ let (sigma, t) = Typing.type_of env sigma c in
+ let t = Value.of_constr t in
+ Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclUNIT t
+ end in
+ pf_apply get_type
+| _ -> assert false
+
+(** constr -> constr *)
+let prm_constr_equal : ml_tactic = function
+| [c1; c2] ->
+ let c1 = Value.to_constr c1 in
+ let c2 = Value.to_constr c2 in
+ Proofview.tclEVARMAP >>= fun sigma ->
+ let b = EConstr.eq_constr sigma c1 c2 in
+ Proofview.tclUNIT (Value.of_bool b)
+| _ -> assert false
+
+(** Error *)
+
+let prm_throw : ml_tactic = function
+| [e] ->
+ let (e, info) = Value.to_exn e in
+ Proofview.tclLIFT (Proofview.NonLogical.raise ~info e)
+| _ -> assert false
+
+(** Control *)
+
+(** exn -> 'a *)
+let prm_zero : ml_tactic = function
+| [e] ->
+ let (e, info) = Value.to_exn e in
+ Proofview.tclZERO ~info e
+| _ -> assert false
+
+(** exn -> 'a *)
+let prm_plus : ml_tactic = function
+| [x; k] ->
+ Proofview.tclOR (thaw x) (fun e -> interp_app k [Value.of_exn e])
+| _ -> assert false
+
+(** (unit -> 'a) -> 'a *)
+let prm_once : ml_tactic = function
+| [f] -> Proofview.tclONCE (thaw f)
+| _ -> assert false
+
+(** (unit -> unit) list -> unit *)
+let prm_dispatch : ml_tactic = function
+| [l] ->
+ let l = Value.to_list l in
+ let l = List.map (fun f -> Proofview.tclIGNORE (thaw f)) l in
+ Proofview.tclDISPATCH l >>= fun () -> return v_unit
+| _ -> assert false
+
+(** (unit -> unit) list -> (unit -> unit) -> (unit -> unit) list -> unit *)
+let prm_extend : ml_tactic = function
+| [lft; tac; rgt] ->
+ let lft = Value.to_list lft in
+ let lft = List.map (fun f -> Proofview.tclIGNORE (thaw f)) lft in
+ let tac = Proofview.tclIGNORE (thaw tac) in
+ let rgt = Value.to_list rgt in
+ let rgt = List.map (fun f -> Proofview.tclIGNORE (thaw f)) rgt in
+ Proofview.tclEXTEND lft tac rgt >>= fun () -> return v_unit
+| _ -> assert false
+
+(** (unit -> unit) -> unit *)
+let prm_enter : ml_tactic = function
+| [f] ->
+ let f = Proofview.tclIGNORE (thaw f) in
+ Proofview.tclINDEPENDENT f >>= fun () -> return v_unit
+| _ -> assert false
+
+(** int -> int -> (unit -> 'a) -> 'a *)
+let prm_focus : ml_tactic = function
+| [i; j; tac] ->
+ let i = Value.to_int i in
+ let j = Value.to_int j in
+ Proofview.tclFOCUS i j (thaw tac)
+| _ -> assert false
+
+(** unit -> unit *)
+let prm_shelve : ml_tactic = function
+| [_] -> Proofview.shelve >>= fun () -> return v_unit
+| _ -> assert false
+
+(** unit -> unit *)
+let prm_shelve_unifiable : ml_tactic = function
+| [_] -> Proofview.shelve_unifiable >>= fun () -> return v_unit
+| _ -> assert false
+
+let prm_new_goal : ml_tactic = function
+| [ev] ->
+ let ev = Evar.unsafe_of_int (Value.to_int ev) in
+ Proofview.tclEVARMAP >>= fun sigma ->
+ if Evd.mem sigma ev then
+ Proofview.Unsafe.tclNEWGOALS [ev] <*> Proofview.tclUNIT v_unit
+ else throw err_notfound
+| _ -> assert false
+
+(** unit -> constr *)
+let prm_goal : ml_tactic = function
+| [_] ->
+ Proofview.Goal.enter_one begin fun gl ->
+ let concl = Tacmach.New.pf_nf_concl gl in
+ return (Value.of_constr concl)
+ end
+| _ -> assert false
+
+(** ident -> constr *)
+let prm_hyp : ml_tactic = function
+| [id] ->
+ let id = Value.to_ident id in
+ 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.New.tclZEROMSG
+ (str "Hypothesis " ++ quote (Id.print id) ++ str " not found") (** FIXME: Do something more sensible *)
+ end
+| _ -> assert false
+
+(** (unit -> constr) -> unit *)
+let prm_refine : ml_tactic = function
+| [c] ->
+ let c = thaw c >>= fun c -> Proofview.tclUNIT ((), Value.to_constr c) in
+ Proofview.Goal.nf_enter begin fun gl ->
+ Refine.generic_refine ~typecheck:true c gl
+ end >>= fun () -> return v_unit
+| _ -> assert false
+
+
+(** Registering *)
+
+let () = Tac2env.define_primitive (pname "print") prm_print
+let () = Tac2env.define_primitive (pname "message_of_string") prm_message_of_string
+let () = Tac2env.define_primitive (pname "message_of_int") prm_message_of_int
+let () = Tac2env.define_primitive (pname "message_of_constr") prm_message_of_constr
+let () = Tac2env.define_primitive (pname "message_concat") prm_message_concat
+
+let () = Tac2env.define_primitive (pname "array_make") prm_array_make
+let () = Tac2env.define_primitive (pname "array_length") prm_array_length
+let () = Tac2env.define_primitive (pname "array_get") prm_array_get
+let () = Tac2env.define_primitive (pname "array_set") prm_array_set
+
+let () = Tac2env.define_primitive (pname "string_make") prm_string_make
+let () = Tac2env.define_primitive (pname "string_length") prm_string_length
+let () = Tac2env.define_primitive (pname "string_get") prm_string_get
+let () = Tac2env.define_primitive (pname "string_set") prm_string_set
+
+let () = Tac2env.define_primitive (pname "constr_type") prm_constr_type
+let () = Tac2env.define_primitive (pname "constr_equal") prm_constr_equal
+
+let () = Tac2env.define_primitive (pname "int_equal") prm_int_equal
+let () = Tac2env.define_primitive (pname "int_compare") prm_int_compare
+let () = Tac2env.define_primitive (pname "int_neg") prm_int_neg
+let () = Tac2env.define_primitive (pname "int_add") prm_int_add
+let () = Tac2env.define_primitive (pname "int_sub") prm_int_sub
+let () = Tac2env.define_primitive (pname "int_mul") prm_int_mul
+
+let () = Tac2env.define_primitive (pname "throw") prm_throw
+
+let () = Tac2env.define_primitive (pname "zero") prm_zero
+let () = Tac2env.define_primitive (pname "plus") prm_plus
+let () = Tac2env.define_primitive (pname "once") prm_once
+let () = Tac2env.define_primitive (pname "dispatch") prm_dispatch
+let () = Tac2env.define_primitive (pname "extend") prm_extend
+let () = Tac2env.define_primitive (pname "enter") prm_enter
+
+let () = Tac2env.define_primitive (pname "focus") prm_focus
+let () = Tac2env.define_primitive (pname "shelve") prm_shelve
+let () = Tac2env.define_primitive (pname "shelve_unifiable") prm_shelve_unifiable
+let () = Tac2env.define_primitive (pname "new_goal") prm_new_goal
+let () = Tac2env.define_primitive (pname "goal") prm_goal
+let () = Tac2env.define_primitive (pname "hyp") prm_hyp
+let () = Tac2env.define_primitive (pname "refine") prm_refine
+
+(** ML types *)
+
+let constr_flags () =
+ let open Pretyping in
+ {
+ use_typeclasses = true;
+ solve_unification_constraints = true;
+ use_hook = Pfedit.solve_by_implicit_tactic ();
+ fail_evar = true;
+ expand_evars = true
+ }
+
+let open_constr_no_classes_flags () =
+ let open Pretyping in
+ {
+ use_typeclasses = false;
+ solve_unification_constraints = true;
+ use_hook = Pfedit.solve_by_implicit_tactic ();
+ fail_evar = false;
+ expand_evars = true
+ }
+
+(** Embed all Ltac2 data into Values *)
+let to_lvar ist =
+ let open Glob_ops in
+ let map e = Val.Dyn (val_valexpr, e) in
+ let lfun = Id.Map.map map ist in
+ { empty_lvar with Glob_term.ltac_genargs = lfun }
+
+let interp_constr flags ist (c, _) =
+ let open Pretyping in
+ pf_apply begin fun env sigma ->
+ Proofview.V82.wrap_exceptions begin fun () ->
+ let ist = to_lvar ist in
+ let (sigma, c) = understand_ltac flags env sigma ist WithoutTypeConstraint c in
+ let c = Val.Dyn (val_constr, c) in
+ Proofview.Unsafe.tclEVARS sigma >>= fun () ->
+ Proofview.tclUNIT c
+ end
+ end
+
+let () =
+ let interp ist c = interp_constr (constr_flags ()) ist c in
+ let obj = {
+ ml_type = t_constr;
+ ml_interp = interp;
+ } in
+ define_ml_object Stdarg.wit_constr obj
+
+let () =
+ let interp ist c = interp_constr (open_constr_no_classes_flags ()) ist c in
+ let obj = {
+ ml_type = t_constr;
+ ml_interp = interp;
+ } in
+ define_ml_object Stdarg.wit_open_constr obj
+
+let () =
+ let interp _ id = return (Val.Dyn (val_ident, id)) in
+ let obj = {
+ ml_type = t_ident;
+ ml_interp = interp;
+ } in
+ define_ml_object Stdarg.wit_ident obj
+
+let () =
+ let interp ist env sigma concl tac =
+ let fold id (Val.Dyn (tag, v)) (accu : environment) : environment =
+ match Val.eq tag val_valexpr with
+ | None -> accu
+ | Some Refl -> Id.Map.add id v accu
+ in
+ let ist = Id.Map.fold fold ist Id.Map.empty in
+ let tac = Proofview.tclIGNORE (interp ist tac) in
+ let c, sigma = Pfedit.refine_by_tactic env sigma concl tac in
+ (EConstr.of_constr c, sigma)
+ in
+ Pretyping.register_constr_interp0 wit_ltac2 interp
+
+(** Built-in notation scopes *)
+
+let add_scope s f =
+ Tac2entries.register_scope (Id.of_string s) f
+
+let scope_fail () = CErrors.user_err (str "Invalid parsing token")
+
+let dummy_loc = Loc.make_loc (-1, -1)
+
+let rthunk e =
+ let loc = Tac2intern.loc_of_tacexpr e in
+ let var = [Loc.tag ~loc Anonymous, Some (CTypRef (loc, AbsKn Core.t_unit, []))] in
+ CTacFun (loc, var, e)
+
+let add_generic_scope s entry arg =
+ let parse = function
+ | [] ->
+ let scope = Extend.Aentry entry in
+ let act x = rthunk (CTacExt (dummy_loc, in_gen (rawwit arg) x)) in
+ Tac2entries.ScopeRule (scope, act)
+ | _ -> scope_fail ()
+ in
+ add_scope s parse
+
+let () = add_scope "list0" begin function
+| [tok] ->
+ let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in
+ let scope = Extend.Alist0 scope in
+ let act l =
+ let l = List.map act l in
+ CTacLst (None, l)
+ in
+ Tac2entries.ScopeRule (scope, act)
+| [tok; SexprStr (_, str)] ->
+ let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in
+ let sep = Extend.Atoken (CLexer.terminal str) in
+ let scope = Extend.Alist0sep (scope, sep) in
+ let act l =
+ let l = List.map act l in
+ CTacLst (None, l)
+ in
+ Tac2entries.ScopeRule (scope, act)
+| _ -> scope_fail ()
+end
+
+let () = add_scope "list1" begin function
+| [tok] ->
+ let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in
+ let scope = Extend.Alist1 scope in
+ let act l =
+ let l = List.map act l in
+ CTacLst (None, l)
+ in
+ Tac2entries.ScopeRule (scope, act)
+| [tok; SexprStr (_, str)] ->
+ let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in
+ let sep = Extend.Atoken (CLexer.terminal str) in
+ let scope = Extend.Alist1sep (scope, sep) in
+ let act l =
+ let l = List.map act l in
+ CTacLst (None, l)
+ in
+ Tac2entries.ScopeRule (scope, act)
+| _ -> scope_fail ()
+end
+
+let () = add_scope "opt" begin function
+| [tok] ->
+ let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in
+ let scope = Extend.Aopt scope in
+ let act opt = match opt with
+ | None ->
+ CTacRef (AbsKn (TacConstructor Core.c_none))
+ | Some x ->
+ CTacApp (dummy_loc, CTacRef (AbsKn (TacConstructor Core.c_some)), [act x])
+ in
+ Tac2entries.ScopeRule (scope, act)
+| _ -> scope_fail ()
+end
+
+let () = add_scope "self" begin function
+| [] ->
+ let scope = Extend.Aself in
+ let act tac = rthunk tac in
+ Tac2entries.ScopeRule (scope, act)
+| _ -> scope_fail ()
+end
+
+let () = add_scope "next" begin function
+| [] ->
+ let scope = Extend.Anext in
+ let act tac = rthunk tac in
+ Tac2entries.ScopeRule (scope, act)
+| _ -> scope_fail ()
+end
+
+let () = add_scope "tactic" begin function
+| [] ->
+ (** Default to level 5 parsing *)
+ let scope = Extend.Aentryl (Tac2entries.Pltac.tac2expr, 5) in
+ let act tac = rthunk tac in
+ Tac2entries.ScopeRule (scope, act)
+| [SexprInt (loc, n)] ->
+ let () = if n < 0 || n > 5 then scope_fail () in
+ let scope = Extend.Aentryl (Tac2entries.Pltac.tac2expr, n) in
+ let act tac = rthunk tac in
+ Tac2entries.ScopeRule (scope, act)
+| _ -> scope_fail ()
+end
+
+let () = add_generic_scope "ident" Pcoq.Prim.ident Stdarg.wit_ident
+let () = add_generic_scope "constr" Pcoq.Constr.constr Stdarg.wit_constr
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-08 20:02:18 +0000