diff options
Diffstat (limited to 'vendor/Ltac2/src/tac2stdlib.ml')
| -rw-r--r-- | vendor/Ltac2/src/tac2stdlib.ml | 578 |
1 files changed, 578 insertions, 0 deletions
diff --git a/vendor/Ltac2/src/tac2stdlib.ml b/vendor/Ltac2/src/tac2stdlib.ml new file mode 100644 index 0000000000..ffef2c05fd --- /dev/null +++ b/vendor/Ltac2/src/tac2stdlib.ml @@ -0,0 +1,578 @@ +(************************************************************************) +(* 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 Names +open Genredexpr +open Tac2expr +open Tac2ffi +open Tac2types +open Tac2extffi +open Proofview.Notations + +module Value = Tac2ffi + +(** Make a representation with a dummy from function *) +let make_to_repr f = Tac2ffi.make_repr (fun _ -> assert false) f + +let return x = Proofview.tclUNIT x +let v_unit = Value.of_unit () +let thaw r f = Tac2ffi.app_fun1 f unit r () +let uthaw r f = Tac2ffi.app_fun1 (to_fun1 unit r f) unit r () +let thunk r = fun1 unit r + +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 to_occurrences = function +| ValInt 0 -> AllOccurrences +| ValBlk (0, [| vl |]) -> AllOccurrencesBut (Value.to_list Value.to_int vl) +| ValInt 1 -> NoOccurrences +| ValBlk (1, [| vl |]) -> OnlyOccurrences (Value.to_list Value.to_int vl) +| _ -> assert false + +let occurrences = make_to_repr to_occurrences + +let to_hyp_location_flag v = match Value.to_int v with +| 0 -> InHyp +| 1 -> InHypTypeOnly +| 2 -> InHypValueOnly +| _ -> assert false + +let to_clause v = match Value.to_tuple v with +| [| hyps; concl |] -> + let cast v = match Value.to_tuple v with + | [| hyp; occ; flag |] -> + (Value.to_ident hyp, to_occurrences occ, to_hyp_location_flag flag) + | _ -> assert false + in + let hyps = Value.to_option (fun h -> Value.to_list cast h) hyps in + { onhyps = hyps; concl_occs = to_occurrences concl; } +| _ -> assert false + +let clause = make_to_repr to_clause + +let to_red_flag v = match Value.to_tuple v with +| [| beta; iota; fix; cofix; zeta; delta; const |] -> + { + rBeta = Value.to_bool beta; + rMatch = Value.to_bool iota; + rFix = Value.to_bool fix; + rCofix = Value.to_bool cofix; + rZeta = Value.to_bool zeta; + rDelta = Value.to_bool delta; + rConst = Value.to_list Value.to_reference const; + } +| _ -> assert false + +let red_flags = make_to_repr to_red_flag + +let pattern_with_occs = pair pattern occurrences + +let constr_with_occs = pair constr occurrences + +let reference_with_occs = pair reference occurrences + +let rec to_intro_pattern v = match Value.to_block v with +| (0, [| b |]) -> IntroForthcoming (Value.to_bool b) +| (1, [| pat |]) -> IntroNaming (to_intro_pattern_naming pat) +| (2, [| act |]) -> IntroAction (to_intro_pattern_action act) +| _ -> assert false + +and to_intro_pattern_naming = function +| ValBlk (0, [| id |]) -> IntroIdentifier (Value.to_ident id) +| ValBlk (1, [| id |]) -> IntroFresh (Value.to_ident id) +| ValInt 0 -> IntroAnonymous +| _ -> assert false + +and to_intro_pattern_action = function +| ValInt 0 -> IntroWildcard +| ValBlk (0, [| op |]) -> IntroOrAndPattern (to_or_and_intro_pattern op) +| ValBlk (1, [| inj |]) -> + 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 + IntroApplyOn (c, to_intro_pattern ipat) +| ValBlk (3, [| b |]) -> IntroRewrite (Value.to_bool b) +| _ -> assert false + +and to_or_and_intro_pattern v = match Value.to_block v with +| (0, [| ill |]) -> + IntroOrPattern (Value.to_list to_intro_patterns ill) +| (1, [| il |]) -> + IntroAndPattern (to_intro_patterns il) +| _ -> assert false + +and to_intro_patterns il = + Value.to_list to_intro_pattern il + +let intro_pattern = make_to_repr to_intro_pattern + +let intro_patterns = make_to_repr to_intro_patterns + +let to_destruction_arg v = match Value.to_block v with +| (0, [| c |]) -> + let c = uthaw 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 to_induction_clause v = match Value.to_tuple v with +| [| arg; eqn; as_; in_ |] -> + let arg = to_destruction_arg arg in + let eqn = Value.to_option to_intro_pattern_naming eqn in + let as_ = Value.to_option to_or_and_intro_pattern as_ in + let in_ = Value.to_option to_clause in_ in + (arg, eqn, as_, in_) +| _ -> + assert false + +let induction_clause = make_to_repr to_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 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 + AssertType (ipat, t, tac) +| (1, [| id; c |]) -> + AssertValue (Value.to_ident id, Value.to_constr c) +| _ -> assert false + +let assertion = make_to_repr to_assertion + +let to_multi = function +| ValBlk (0, [| n |]) -> Precisely (Value.to_int n) +| ValBlk (1, [| n |]) -> UpTo (Value.to_int n) +| ValInt 0 -> RepeatStar +| ValInt 1 -> RepeatPlus +| _ -> assert false + +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 + (orient, repeat, c) +| _ -> assert false + +let rewriting = make_to_repr to_rewriting + +let to_debug v = match Value.to_int v with +| 0 -> Hints.Off +| 1 -> Hints.Info +| 2 -> Hints.Debug +| _ -> assert false + +let debug = make_to_repr to_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 to_inversion_kind v = match Value.to_int v with +| 0 -> Inv.SimpleInversion +| 1 -> Inv.FullInversion +| 2 -> Inv.FullInversionClear +| _ -> assert false + +let inversion_kind = make_to_repr to_inversion_kind + +let to_move_location = function +| ValInt 0 -> Logic.MoveFirst +| ValInt 1 -> Logic.MoveLast +| ValBlk (0, [|id|]) -> Logic.MoveAfter (Value.to_ident id) +| 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 generalize_arg = make_to_repr to_generalize_arg + +(** Standard tactics sharing their implementation with Ltac1 *) + +let pname s = { mltac_plugin = "ltac2"; mltac_tactic = s } + +let lift tac = tac <*> return v_unit + +let define_prim0 name tac = + let tac _ = lift tac in + Tac2env.define_primitive (pname name) (mk_closure arity_one tac) + +let define_prim1 name r0 f = + let tac x = lift (f (Value.repr_to r0 x)) in + Tac2env.define_primitive (pname name) (mk_closure arity_one tac) + +let define_prim2 name r0 r1 f = + let tac x y = lift (f (Value.repr_to r0 x) (Value.repr_to r1 y)) in + Tac2env.define_primitive (pname name) (mk_closure (arity_suc arity_one) tac) + +let define_prim3 name r0 r1 r2 f = + let tac x y z = lift (f (Value.repr_to r0 x) (Value.repr_to r1 y) (Value.repr_to r2 z)) in + Tac2env.define_primitive (pname name) (mk_closure (arity_suc (arity_suc arity_one)) tac) + +let define_prim4 name r0 r1 r2 r3 f = + let tac x y z u = lift (f (Value.repr_to r0 x) (Value.repr_to r1 y) (Value.repr_to r2 z) (Value.repr_to r3 u)) in + Tac2env.define_primitive (pname name) (mk_closure (arity_suc (arity_suc (arity_suc arity_one))) tac) + +let define_prim5 name r0 r1 r2 r3 r4 f = + let tac x y z u v = lift (f (Value.repr_to r0 x) (Value.repr_to r1 y) (Value.repr_to r2 z) (Value.repr_to r3 u) (Value.repr_to r4 v)) in + Tac2env.define_primitive (pname name) (mk_closure (arity_suc (arity_suc (arity_suc (arity_suc arity_one)))) tac) + +(** Tactics from Tacexpr *) + +let () = define_prim2 "tac_intros" bool intro_patterns begin fun ev ipat -> + Tac2tactics.intros_patterns ev ipat +end + +let () = define_prim4 "tac_apply" bool bool (list (thunk constr_with_bindings)) (option (pair ident (option intro_pattern))) begin fun adv ev cb ipat -> + Tac2tactics.apply adv ev cb ipat +end + +let () = define_prim3 "tac_elim" bool constr_with_bindings (option constr_with_bindings) begin fun ev c copt -> + Tac2tactics.elim ev c copt +end + +let () = define_prim2 "tac_case" bool constr_with_bindings begin fun ev c -> + Tac2tactics.general_case_analysis ev c +end + +let () = define_prim1 "tac_generalize" (list generalize_arg) begin fun cl -> + Tac2tactics.generalize cl +end + +let () = define_prim1 "tac_assert" assertion begin fun ast -> + Tac2tactics.assert_ ast +end + +let () = define_prim3 "tac_enough" constr (option (option (thunk unit))) (option intro_pattern) begin fun c tac ipat -> + let tac = Option.map (fun o -> Option.map (fun f -> thaw unit f) o) tac in + Tac2tactics.forward false tac ipat c +end + +let () = define_prim2 "tac_pose" name constr begin fun na c -> + Tactics.letin_tac None na c None Locusops.nowhere +end + +let () = define_prim3 "tac_set" bool (thunk (pair name constr)) clause begin fun ev p cl -> + Proofview.tclEVARMAP >>= fun sigma -> + thaw (pair name constr) p >>= fun (na, c) -> + Tac2tactics.letin_pat_tac ev None na (sigma, c) cl +end + +let () = define_prim5 "tac_remember" bool name (thunk constr) (option intro_pattern) clause begin fun ev na c eqpat cl -> + let eqpat = Option.default (IntroNaming IntroAnonymous) eqpat in + match eqpat with + | IntroNaming eqpat -> + Proofview.tclEVARMAP >>= fun sigma -> + thaw constr c >>= fun c -> + Tac2tactics.letin_pat_tac ev (Some (true, eqpat)) na (sigma, c) cl + | _ -> + Tacticals.New.tclZEROMSG (Pp.str "Invalid pattern for remember") +end + +let () = define_prim3 "tac_destruct" bool (list induction_clause) (option constr_with_bindings) begin fun ev ic using -> + Tac2tactics.induction_destruct false ev ic using +end + +let () = define_prim3 "tac_induction" bool (list induction_clause) (option constr_with_bindings) begin fun ev ic using -> + Tac2tactics.induction_destruct true ev ic using +end + +let () = define_prim1 "tac_red" clause begin fun cl -> + Tac2tactics.reduce (Red false) cl +end + +let () = define_prim1 "tac_hnf" clause begin fun cl -> + Tac2tactics.reduce Hnf cl +end + +let () = define_prim3 "tac_simpl" red_flags (option pattern_with_occs) clause begin fun flags where cl -> + Tac2tactics.simpl flags where cl +end + +let () = define_prim2 "tac_cbv" red_flags clause begin fun flags cl -> + Tac2tactics.cbv flags cl +end + +let () = define_prim2 "tac_cbn" red_flags clause begin fun flags cl -> + Tac2tactics.cbn flags cl +end + +let () = define_prim2 "tac_lazy" red_flags clause begin fun flags cl -> + Tac2tactics.lazy_ flags cl +end + +let () = define_prim2 "tac_unfold" (list reference_with_occs) clause begin fun refs cl -> + Tac2tactics.unfold refs cl +end + +let () = define_prim2 "tac_fold" (list constr) clause begin fun args cl -> + Tac2tactics.reduce (Fold args) cl +end + +let () = define_prim2 "tac_pattern" (list constr_with_occs) clause begin fun where cl -> + Tac2tactics.pattern where cl +end + +let () = define_prim2 "tac_vm" (option pattern_with_occs) clause begin fun where cl -> + Tac2tactics.vm where cl +end + +let () = define_prim2 "tac_native" (option pattern_with_occs) clause begin fun where cl -> + Tac2tactics.native where cl +end + +(** Reduction functions *) + +let lift tac = tac >>= fun c -> Proofview.tclUNIT (Value.of_constr c) + +let define_red1 name r0 f = + let tac x = lift (f (Value.repr_to r0 x)) in + Tac2env.define_primitive (pname name) (mk_closure arity_one tac) + +let define_red2 name r0 r1 f = + let tac x y = lift (f (Value.repr_to r0 x) (Value.repr_to r1 y)) in + Tac2env.define_primitive (pname name) (mk_closure (arity_suc arity_one) tac) + +let define_red3 name r0 r1 r2 f = + let tac x y z = lift (f (Value.repr_to r0 x) (Value.repr_to r1 y) (Value.repr_to r2 z)) in + Tac2env.define_primitive (pname name) (mk_closure (arity_suc (arity_suc arity_one)) tac) + +let () = define_red1 "eval_red" constr begin fun c -> + Tac2tactics.eval_red c +end + +let () = define_red1 "eval_hnf" constr begin fun c -> + Tac2tactics.eval_hnf c +end + +let () = define_red3 "eval_simpl" red_flags (option pattern_with_occs) constr begin fun flags where c -> + Tac2tactics.eval_simpl flags where c +end + +let () = define_red2 "eval_cbv" red_flags constr begin fun flags c -> + Tac2tactics.eval_cbv flags c +end + +let () = define_red2 "eval_cbn" red_flags constr begin fun flags c -> + Tac2tactics.eval_cbn flags c +end + +let () = define_red2 "eval_lazy" red_flags constr begin fun flags c -> + Tac2tactics.eval_lazy flags c +end + +let () = define_red2 "eval_unfold" (list reference_with_occs) constr begin fun refs c -> + Tac2tactics.eval_unfold refs c +end + +let () = define_red2 "eval_fold" (list constr) constr begin fun args c -> + Tac2tactics.eval_fold args c +end + +let () = define_red2 "eval_pattern" (list constr_with_occs) constr begin fun where c -> + Tac2tactics.eval_pattern where c +end + +let () = define_red2 "eval_vm" (option pattern_with_occs) constr begin fun where c -> + Tac2tactics.eval_vm where c +end + +let () = define_red2 "eval_native" (option pattern_with_occs) constr begin fun where c -> + Tac2tactics.eval_native where c +end + +let () = define_prim3 "tac_change" (option pattern) (fun1 (array constr) constr) clause begin fun pat c cl -> + Tac2tactics.change pat c cl +end + +let () = define_prim4 "tac_rewrite" bool (list rewriting) clause (option (thunk unit)) begin fun ev rw cl by -> + Tac2tactics.rewrite ev rw cl by +end + +let () = define_prim4 "tac_inversion" inversion_kind destruction_arg (option intro_pattern) (option (list ident)) begin fun knd arg pat ids -> + Tac2tactics.inversion knd arg pat ids +end + +(** Tactics from coretactics *) + +let () = define_prim0 "tac_reflexivity" Tactics.intros_reflexivity + +let () = define_prim2 "tac_move" ident move_location begin fun id mv -> + Tactics.move_hyp id mv +end + +let () = define_prim2 "tac_intro" (option ident) (option move_location) begin fun id mv -> + let mv = Option.default Logic.MoveLast mv in + Tactics.intro_move id mv +end + +(* + +TACTIC EXTEND exact + [ "exact" casted_constr(c) ] -> [ Tactics.exact_no_check c ] +END + +*) + +let () = define_prim0 "tac_assumption" Tactics.assumption + +let () = define_prim1 "tac_transitivity" constr begin fun c -> + Tactics.intros_transitivity (Some c) +end + +let () = define_prim0 "tac_etransitivity" (Tactics.intros_transitivity None) + +let () = define_prim1 "tac_cut" constr begin fun c -> + Tactics.cut c +end + +let () = define_prim2 "tac_left" bool bindings begin fun ev bnd -> + Tac2tactics.left_with_bindings ev bnd +end +let () = define_prim2 "tac_right" bool bindings begin fun ev bnd -> + Tac2tactics.right_with_bindings ev bnd +end + +let () = define_prim1 "tac_introsuntil" qhyp begin fun h -> + Tactics.intros_until h +end + +let () = define_prim1 "tac_exactnocheck" constr begin fun c -> + Tactics.exact_no_check c +end + +let () = define_prim1 "tac_vmcastnocheck" constr begin fun c -> + Tactics.vm_cast_no_check c +end + +let () = define_prim1 "tac_nativecastnocheck" constr begin fun c -> + Tactics.native_cast_no_check c +end + +let () = define_prim1 "tac_constructor" bool begin fun ev -> + Tactics.any_constructor ev None +end + +let () = define_prim3 "tac_constructorn" bool int bindings begin fun ev n bnd -> + Tac2tactics.constructor_tac ev None n bnd +end + +let () = define_prim2 "tac_specialize" constr_with_bindings (option intro_pattern) begin fun c ipat -> + Tac2tactics.specialize c ipat +end + +let () = define_prim1 "tac_symmetry" clause begin fun cl -> + Tac2tactics.symmetry cl +end + +let () = define_prim2 "tac_split" bool bindings begin fun ev bnd -> + Tac2tactics.split_with_bindings ev bnd +end + +let () = define_prim1 "tac_rename" (list (pair ident ident)) begin fun ids -> + Tactics.rename_hyp ids +end + +let () = define_prim1 "tac_revert" (list ident) begin fun ids -> + Tactics.revert ids +end + +let () = define_prim0 "tac_admit" Proofview.give_up + +let () = define_prim2 "tac_fix" ident int begin fun ident n -> + Tactics.fix ident n +end + +let () = define_prim1 "tac_cofix" ident begin fun ident -> + Tactics.cofix ident +end + +let () = define_prim1 "tac_clear" (list ident) begin fun ids -> + Tactics.clear ids +end + +let () = define_prim1 "tac_keep" (list ident) begin fun ids -> + Tactics.keep ids +end + +let () = define_prim1 "tac_clearbody" (list ident) begin fun ids -> + Tactics.clear_body ids +end + +(** Tactics from extratactics *) + +let () = define_prim2 "tac_discriminate" bool (option destruction_arg) begin fun ev arg -> + Tac2tactics.discriminate ev arg +end + +let () = define_prim3 "tac_injection" bool (option intro_patterns) (option destruction_arg) begin fun ev ipat arg -> + Tac2tactics.injection ev ipat arg +end + +let () = define_prim1 "tac_absurd" constr begin fun c -> + Contradiction.absurd c +end + +let () = define_prim1 "tac_contradiction" (option constr_with_bindings) begin fun c -> + Tac2tactics.contradiction c +end + +let () = define_prim4 "tac_autorewrite" bool (option (thunk unit)) (list ident) clause begin fun all by ids cl -> + Tac2tactics.autorewrite ~all by ids cl +end + +let () = define_prim1 "tac_subst" (list ident) begin fun ids -> + Equality.subst ids +end + +let () = define_prim0 "tac_substall" (return () >>= fun () -> Equality.subst_all ()) + +(** Auto *) + +let () = define_prim3 "tac_trivial" debug (list (thunk constr)) (option (list ident)) begin fun dbg lems dbs -> + Tac2tactics.trivial dbg lems dbs +end + +let () = define_prim5 "tac_eauto" debug (option int) (option int) (list (thunk constr)) (option (list ident)) begin fun dbg n p lems dbs -> + Tac2tactics.eauto dbg n p lems dbs +end + +let () = define_prim4 "tac_auto" debug (option int) (list (thunk constr)) (option (list ident)) begin fun dbg n lems dbs -> + Tac2tactics.auto dbg n lems dbs +end + +let () = define_prim4 "tac_newauto" debug (option int) (list (thunk constr)) (option (list ident)) begin fun dbg n lems dbs -> + Tac2tactics.new_auto dbg n lems dbs +end + +let () = define_prim3 "tac_typeclasses_eauto" (option strategy) (option int) (option (list ident)) begin fun str n dbs -> + Tac2tactics.typeclasses_eauto str n dbs +end + +(** Firstorder *) + +let () = define_prim3 "tac_firstorder" (option (thunk unit)) (list reference) (list ident) begin fun tac refs ids -> + Tac2tactics.firstorder tac refs ids +end |