diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/g_ltac2.ml4 | 37 | ||||
| -rw-r--r-- | src/tac2core.ml | 1 | ||||
| -rw-r--r-- | src/tac2entries.ml | 1 | ||||
| -rw-r--r-- | src/tac2entries.mli | 1 | ||||
| -rw-r--r-- | src/tac2qexpr.mli | 2 | ||||
| -rw-r--r-- | src/tac2quote.ml | 3 | ||||
| -rw-r--r-- | src/tac2quote.mli | 2 | ||||
| -rw-r--r-- | src/tac2stdlib.ml | 7 |
8 files changed, 49 insertions, 5 deletions
diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4 index 7295f31181..dfd586d5ef 100644 --- a/src/g_ltac2.ml4 +++ b/src/g_ltac2.ml4 @@ -40,6 +40,27 @@ let test_lpar_idnum_coloneq = | _ -> err ()) | _ -> err ()) +(* Hack to recognize "(x := t)" and "($x := t)" *) +let test_lpar_coloneq = + Gram.Entry.of_parser "test_coloneq" + (fun strm -> + match stream_nth 0 strm with + | KEYWORD "(" -> + (match stream_nth 1 strm with + | IDENT _ -> + (match stream_nth 2 strm with + | KEYWORD ":=" -> () + | _ -> err ()) + | KEYWORD "$" -> + (match stream_nth 2 strm with + | IDENT _ -> + (match stream_nth 3 strm with + | KEYWORD ":=" -> () + | _ -> err ()) + | _ -> err ()) + | _ -> err ()) + | _ -> err ()) + (* Hack to recognize "(x)" *) let test_lpar_id_rpar = Gram.Entry.of_parser "lpar_id_coloneq" @@ -369,7 +390,7 @@ GEXTEND Gram GLOBAL: q_ident q_bindings q_intropattern q_intropatterns q_induction_clause q_rewriting q_clause q_dispatch q_occurrences q_strategy_flag q_destruction_arg q_reference q_with_bindings q_constr_matching - q_hintdb q_move_location; + q_hintdb q_move_location q_pose; anti: [ [ "$"; id = Prim.ident -> QAnti (Loc.tag ~loc:!@loc id) ] ] ; @@ -702,6 +723,20 @@ GEXTEND Gram q_move_location: [ [ mv = move_location -> mv ] ] ; + as_name: + [ [ -> None + | "as"; id = ident_or_anti -> Some id + ] ] + ; + pose: + [ [ test_lpar_coloneq; "("; id = ident_or_anti; ":="; c = Constr.lconstr; ")" -> + Loc.tag ~loc:!@loc (Some id, c) + | c = Constr.constr; na = as_name -> Loc.tag ~loc:!@loc (na, c) + ] ] + ; + q_pose: + [ [ p = pose -> p ] ] + ; END (** Extension of constr syntax *) diff --git a/src/tac2core.ml b/src/tac2core.ml index 7bd0164b4d..bb6578090d 100644 --- a/src/tac2core.ml +++ b/src/tac2core.ml @@ -1118,6 +1118,7 @@ let () = add_expr_scope "dispatch" q_dispatch Tac2quote.of_dispatch let () = add_expr_scope "strategy" q_strategy_flag Tac2quote.of_strategy_flag let () = add_expr_scope "reference" q_reference Tac2quote.of_reference let () = add_expr_scope "move_location" q_move_location Tac2quote.of_move_location +let () = add_expr_scope "pose" q_pose Tac2quote.of_pose let () = add_expr_scope "constr_matching" q_constr_matching Tac2quote.of_constr_matching let () = add_generic_scope "constr" Pcoq.Constr.constr Tac2quote.wit_constr diff --git a/src/tac2entries.ml b/src/tac2entries.ml index 26f96f7d72..d622aaba69 100644 --- a/src/tac2entries.ml +++ b/src/tac2entries.ml @@ -40,6 +40,7 @@ let q_strategy_flag = Pcoq.Gram.entry_create "tactic:q_strategy_flag" let q_constr_matching = Pcoq.Gram.entry_create "tactic:q_constr_matching" let q_hintdb = Pcoq.Gram.entry_create "tactic:q_hintdb" let q_move_location = Pcoq.Gram.entry_create "tactic:q_move_location" +let q_pose = Pcoq.Gram.entry_create "tactic:q_pose" end (** Tactic definition *) diff --git a/src/tac2entries.mli b/src/tac2entries.mli index 7c71130402..55e658884b 100644 --- a/src/tac2entries.mli +++ b/src/tac2entries.mli @@ -79,6 +79,7 @@ val q_strategy_flag : strategy_flag Pcoq.Gram.entry val q_constr_matching : constr_matching Pcoq.Gram.entry val q_hintdb : hintdb Pcoq.Gram.entry val q_move_location : move_location Pcoq.Gram.entry +val q_pose : pose Pcoq.Gram.entry end (** {5 Hooks} *) diff --git a/src/tac2qexpr.mli b/src/tac2qexpr.mli index 7d02022e07..580039afe5 100644 --- a/src/tac2qexpr.mli +++ b/src/tac2qexpr.mli @@ -139,3 +139,5 @@ type move_location_r = | QMoveLast type move_location = move_location_r located + +type pose = (Id.t located or_anti option * Constrexpr.constr_expr) located diff --git a/src/tac2quote.ml b/src/tac2quote.ml index f14612d58f..466c1f5094 100644 --- a/src/tac2quote.ml +++ b/src/tac2quote.ml @@ -370,3 +370,6 @@ let of_move_location (loc, mv) = match mv with | QMoveBefore id -> std_constructor ?loc "MoveBefore" [of_anti of_ident id] | QMoveFirst -> std_constructor ?loc "MoveFirst" [] | QMoveLast -> std_constructor ?loc "MoveLast" [] + +let of_pose p = + of_pair (fun id -> of_option (fun id -> of_anti of_ident id) id) of_open_constr p diff --git a/src/tac2quote.mli b/src/tac2quote.mli index 9f42c60042..ccb832535a 100644 --- a/src/tac2quote.mli +++ b/src/tac2quote.mli @@ -75,6 +75,8 @@ val of_dispatch : dispatch -> raw_tacexpr val of_strategy_flag : strategy_flag -> raw_tacexpr +val of_pose : pose -> raw_tacexpr + val of_constr_matching : constr_matching -> raw_tacexpr (** {5 Generic arguments} *) diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml index 28bcd6a1cf..0db71fb293 100644 --- a/src/tac2stdlib.ml +++ b/src/tac2stdlib.ml @@ -294,13 +294,12 @@ let () = define_prim2 "tac_pose" begin fun idopt c -> Tactics.letin_tac None na c None Locusops.nowhere end -let () = define_prim4 "tac_set" begin fun ev idopt c cl -> +let () = define_prim3 "tac_set" begin fun ev p cl -> let ev = Value.to_bool ev in - let na = to_name idopt in let cl = to_clause cl in Proofview.tclEVARMAP >>= fun sigma -> - thaw c >>= fun c -> - let c = Value.to_constr c in + thaw p >>= fun p -> + let (na, c) = to_pair to_name Value.to_constr p in Tactics.letin_pat_tac ev None na (sigma, c) cl end |