From b6b9cf860878bd39dafd1f1edb2d212eb67ba7a1 Mon Sep 17 00:00:00 2001 From: barras Date: Thu, 16 Oct 2003 20:35:47 +0000 Subject: nouvelle syntaxe de ltac git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4661 85f007b7-540e-0410-9357-904b9bb8a0f7 --- parsing/g_ltac.ml4 | 28 +++------------------------- parsing/g_ltacnew.ml4 | 24 +++++++++++++----------- parsing/pptactic.ml | 6 +----- parsing/q_coqast.ml4 | 7 ++----- 4 files changed, 19 insertions(+), 46 deletions(-) (limited to 'parsing') diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index b342d9716..41ee54ea4 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -31,7 +31,7 @@ open Q type let_clause_kind = | LETTOPCLAUSE of Names.identifier * constr_expr | LETCLAUSE of - (Names.identifier Util.located * (constr_expr, Libnames.reference) may_eval option * raw_tactic_arg) + (Names.identifier Util.located * raw_tactic_expr option * raw_tactic_arg) ifdef Quotify then module Prelude = struct @@ -82,7 +82,7 @@ GEXTEND Gram | id = base_ident; ":"; c = Constr.constr; ":="; "Proof" -> LETTOPCLAUSE (id, c) | id = identref; ":"; c = constrarg; ":="; te = tactic_letarg -> - LETCLAUSE (id, Some c, te) + LETCLAUSE (id, Some (TacArg(ConstrMayEval c)), te) | id = base_ident; ":"; c = Constr.constr -> LETTOPCLAUSE (id, c) ] ] ; @@ -150,35 +150,13 @@ GEXTEND Gram [IDENT "In" | "in"]; body = tactic_expr -> TacLetRecIn (rc::rcl,body) | IDENT "Let"; llc = LIST1 let_clause SEP "And"; IDENT "In"; u = tactic_expr -> TacLetIn (make_letin_clause loc llc,u) -(* Let cas LetCut est subsumé par "Assert id := c" tandis que le cas - StartProof ne fait pas vraiment de sens en tant que sous-expression - d'une tactique complexe... - | IDENT "Let"; llc = LIST1 let_clause SEP "And" -> - (match llc with - | [LETTOPCLAUSE (id,c)] -> - VernacStartProof ((NeverDischarge,false),id,c,true,(fun _ _ -> ())) - | l -> - let l = List.map (function - | LETCLAUSE (id,Some a,t) -> (id,a,t) - | _ -> user_err_loc (loc, "", str "Syntax Error")) l in - TacLetCut (loc, l)) -*) -(* - | IDENT "Let"; llc = LIST1 let_clause SEP "And"; - tb = Vernac_.theorem_body; "Qed" -> - (match llc with - | [LETTOPCLAUSE (id,c)] -> - EscapeVernac <:ast< (TheoremProof "LETTOP" $id $c $tb) >> - | _ -> - errorlabstrm "Gram.tactic_atom" (str "Not a LETTOPCLAUSE")) -*) | IDENT "Match"; IDENT "Context"; IDENT "With"; mrl = match_context_list -> TacMatchContext (false,mrl) | IDENT "Match"; IDENT "Reverse"; IDENT "Context"; IDENT "With"; mrl = match_context_list -> TacMatchContext (true,mrl) | IDENT "Match"; c = constrarg; IDENT "With"; mrl = match_list -> - TacMatch (c,mrl) + TacMatch (TacArg(ConstrMayEval c),mrl) (*To do: put Abstract in Refiner*) | IDENT "Abstract"; tc = tactic_expr -> TacAbstract (tc,None) | IDENT "Abstract"; tc = tactic_expr; "using"; s = base_ident -> diff --git a/parsing/g_ltacnew.ml4 b/parsing/g_ltacnew.ml4 index 9d8dea149..5a1f13132 100644 --- a/parsing/g_ltacnew.ml4 +++ b/parsing/g_ltacnew.ml4 @@ -31,7 +31,7 @@ open Q type let_clause_kind = | LETTOPCLAUSE of Names.identifier * constr_expr | LETCLAUSE of - (Names.identifier Util.located * (constr_expr, Libnames.reference) may_eval option * raw_tactic_arg) + (Names.identifier Util.located * raw_tactic_expr option * raw_tactic_arg) ifdef Quotify then module Prelude = struct @@ -99,7 +99,7 @@ GEXTEND Gram | "match"; IDENT "reverse"; IDENT "context"; "with"; mrl = match_context_list; "end" -> TacMatchContext (true,mrl) - | "match"; c = constrarg; "with"; mrl = match_list; "end" -> + | "match"; c = tactic_expr; "with"; mrl = match_list; "end" -> TacMatch (c,mrl) (*To do: put Abstract in Refiner*) | IDENT "abstract"; tc = tactic_expr -> TacAbstract (tc,None) @@ -116,7 +116,7 @@ GEXTEND Gram | st = simple_tactic -> TacAtom (loc,st) | IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr -> TacArg(ConstrMayEval (ConstrEval (rtc,c))) - | IDENT "inst"; id = identref; "["; c = Constr.lconstr; "]" -> + | IDENT "context"; id = identref; "["; c = Constr.lconstr; "]" -> TacArg(ConstrMayEval (ConstrContext (id,c))) | IDENT "check"; c = Constr.constr -> TacArg(ConstrMayEval (ConstrTypeOf c)) @@ -148,11 +148,13 @@ GEXTEND Gram let_clause: [ [ id = identref; ":="; te = tactic_expr -> LETCLAUSE (id, None, arg_of_expr te) - | (_,id) = identref; ":"; c = Constr.constr; ":="; IDENT "proof" -> + | id = identref; args = LIST1 input_fun; ":="; te = tactic_expr -> + LETCLAUSE (id, None, arg_of_expr (TacFun(args,te))) + | (_,id) = identref; ":"; c = Constr.lconstr; ":="; IDENT "proof" -> LETTOPCLAUSE (id, c) - | id = identref; ":"; c = constrarg; ":="; te = tactic_expr -> + | id = identref; ":"; c = tactic_expr; ":="; te = tactic_expr -> LETCLAUSE (id, Some c, arg_of_expr te) - | (_,id) = identref; ":"; c = Constr.lconstr -> + | (_,id) = identref; ":"; c = Constr.constr -> LETTOPCLAUSE (id, c) ] ] ; rec_clause: @@ -160,16 +162,16 @@ GEXTEND Gram (name,(it,body)) ] ] ; match_pattern: - [ [ id = Constr.lconstr_pattern; "["; pc = Constr.lconstr_pattern; "]" -> - let s = coerce_to_id id in Subterm (Some s, pc) - | "["; pc = Constr.lconstr_pattern; "]" -> Subterm (None,pc) + [ [ IDENT "context"; oid = OPT Constr.ident; + "["; pc = Constr.lconstr_pattern; "]" -> + Subterm (oid, pc) | pc = Constr.lconstr_pattern -> Term pc ] ] ; match_hyps: [ [ na = name; ":"; mp = match_pattern -> Hyp (na, mp) ] ] ; match_context_rule: - [ [ "["; largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern; "]"; + [ [ largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern; "=>"; te = tactic_expr -> Pat (largs, mp, te) | "_"; "=>"; te = tactic_expr -> All te ] ] ; @@ -178,7 +180,7 @@ GEXTEND Gram | "|"; mrl = LIST1 match_context_rule SEP "|" -> mrl ] ] ; match_rule: - [ [ "["; mp = match_pattern; "]"; "=>"; te = tactic_expr -> Pat ([],mp,te) + [ [ mp = match_pattern; "=>"; te = tactic_expr -> Pat ([],mp,te) | "_"; "=>"; te = tactic_expr -> All te ] ] ; match_list: diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 0d7230453..968415de1 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -631,12 +631,8 @@ and pr6 = function | TacLetIn (llc,u) -> v 0 (hv 0 (pr_let_clauses pr_tacarg0 llc ++ spc () ++ str "In") ++ fnl () ++ prtac u) - | TacLetCut llc -> - pr_let_clauses pr_tacarg0 - (List.map (fun (id,c,t) -> ((dummy_loc,id),Some c,t)) llc) - ++ fnl () | TacMatch (t,lrul) -> - hov 0 (str "Match" ++ spc () ++ pr_may_eval pr_constr pr_cst t ++ spc() + hov 0 (str "Match" ++ spc () ++ pr6 t ++ spc() ++ str "With" ++ prlist (fun r -> fnl () ++ str "|" ++ spc () ++ diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index 44e78462f..7dd14d87a 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -481,15 +481,12 @@ and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function let f = mlexpr_of_triple (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_ident) - (mlexpr_of_option (mlexpr_of_may_eval mlexpr_of_constr)) + (mlexpr_of_option mlexpr_of_tactic) mlexpr_of_tactic_arg in <:expr< Tacexpr.TacLetIn $mlexpr_of_list f l$ $mlexpr_of_tactic t$ >> -(* - | Tacexpr.TacLetCut of (identifier * t * tactic_expr) list -*) | Tacexpr.TacMatch (t,l) -> <:expr< Tacexpr.TacMatch - $mlexpr_of_may_eval mlexpr_of_constr t$ + $mlexpr_of_tactic t$ $mlexpr_of_list (mlexpr_of_match_rule mlexpr_of_tactic) l$>> | Tacexpr.TacMatchContext (lr,l) -> <:expr< Tacexpr.TacMatchContext -- cgit v1.2.3