diff options
Diffstat (limited to 'parsing/q_coqast.ml4')
| -rw-r--r-- | parsing/q_coqast.ml4 | 55 |
1 files changed, 30 insertions, 25 deletions
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index 24562459..a4cfe27a 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -8,7 +8,7 @@ (*i camlp4use: "q_MLast.cmo pa_macro.cmo" i*) -(* $Id: q_coqast.ml4 11094 2008-06-10 19:35:23Z herbelin $ *) +(* $Id: q_coqast.ml4 11309 2008-08-06 10:30:35Z herbelin $ *) open Util open Names @@ -62,6 +62,10 @@ let mlexpr_of_reference = function | Libnames.Qualid (loc,qid) -> <:expr< Libnames.Qualid $dloc$ $mlexpr_of_qualid qid$ >> | Libnames.Ident (loc,id) -> <:expr< Libnames.Ident $dloc$ $mlexpr_of_ident id$ >> +let mlexpr_of_located f (loc,x) = <:expr< ($dloc$, $f x$) >> + +let mlexpr_of_loc loc = <:expr< $dloc$ >> + let mlexpr_of_by_notation f = function | Genarg.AN x -> <:expr< Genarg.AN $f x$ >> | Genarg.ByNotation (loc,s) -> <:expr< Genarg.ByNotation $dloc$ $str:s$ >> @@ -85,10 +89,6 @@ let mlexpr_of_quantified_hypothesis = function | Rawterm.AnonHyp n -> <:expr< Rawterm.AnonHyp $mlexpr_of_int n$ >> | Rawterm.NamedHyp id -> <:expr< Rawterm.NamedHyp $mlexpr_of_ident id$ >> -let mlexpr_of_located f (loc,x) = <:expr< ($dloc$, $f x$) >> - -let mlexpr_of_loc loc = <:expr< $dloc$ >> - let mlexpr_of_or_var f = function | Rawterm.ArgArg x -> <:expr< Rawterm.ArgArg $f x$ >> | Rawterm.ArgVar id -> <:expr< Rawterm.ArgVar $mlexpr_of_located mlexpr_of_ident id$ >> @@ -139,7 +139,7 @@ let mlexpr_of_binding_kind = function let mlexpr_of_binder_kind = function | Topconstr.Default b -> <:expr< Topconstr.Default $mlexpr_of_binding_kind b$ >> - | Topconstr.TypeClass b -> <:expr< Topconstr.TypeClass $mlexpr_of_binding_kind b$ >> + | Topconstr.TypeClass (b,b') -> <:expr< Topconstr.TypeClass $mlexpr_of_pair mlexpr_of_binding_kind mlexpr_of_binding_kind (b,b')$ >> let rec mlexpr_of_constr = function | Topconstr.CRef (Libnames.Ident (loc,id)) when is_meta (string_of_id id) -> @@ -242,6 +242,11 @@ let mlexpr_of_binding = mlexpr_of_pair mlexpr_of_binding_kind mlexpr_of_constr let mlexpr_of_constr_with_binding = mlexpr_of_pair mlexpr_of_constr mlexpr_of_binding_kind +let mlexpr_of_move_location f = function + | Tacexpr.MoveAfter id -> <:expr< Tacexpr.MoveAfter $f id$ >> + | Tacexpr.MoveBefore id -> <:expr< Tacexpr.MoveBefore $f id$ >> + | Tacexpr.MoveToEnd b -> <:expr< Tacexpr.MoveToEnd $mlexpr_of_bool b$ >> + let mlexpr_of_induction_arg = function | Tacexpr.ElimOnConstr c -> <:expr< Tacexpr.ElimOnConstr $mlexpr_of_constr_with_binding c$ >> @@ -279,13 +284,13 @@ let mlexpr_of_message_token = function let rec mlexpr_of_atomic_tactic = function (* Basic tactics *) | Tacexpr.TacIntroPattern pl -> - let pl = mlexpr_of_list mlexpr_of_intro_pattern pl in + let pl = mlexpr_of_list (mlexpr_of_located mlexpr_of_intro_pattern) pl in <:expr< Tacexpr.TacIntroPattern $pl$ >> | Tacexpr.TacIntrosUntil h -> <:expr< Tacexpr.TacIntrosUntil $mlexpr_of_quantified_hypothesis h$ >> | Tacexpr.TacIntroMove (idopt,idopt') -> let idopt = mlexpr_of_ident_option idopt in - let idopt'=mlexpr_of_option (mlexpr_of_located mlexpr_of_ident) idopt' in + let idopt'= mlexpr_of_move_location mlexpr_of_hyp idopt' in <:expr< Tacexpr.TacIntroMove $idopt$ $idopt'$ >> | Tacexpr.TacAssumption -> <:expr< Tacexpr.TacAssumption >> @@ -296,7 +301,7 @@ let rec mlexpr_of_atomic_tactic = function | Tacexpr.TacVmCastNoCheck c -> <:expr< Tacexpr.TacVmCastNoCheck $mlexpr_of_constr c$ >> | Tacexpr.TacApply (b,false,cb) -> - <:expr< Tacexpr.TacApply $mlexpr_of_bool b$ False $mlexpr_of_constr_with_binding cb$ >> + <:expr< Tacexpr.TacApply $mlexpr_of_bool b$ False $mlexpr_of_list mlexpr_of_constr_with_binding cb$ >> | Tacexpr.TacElim (false,cb,cbo) -> let cb = mlexpr_of_constr_with_binding cb in let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in @@ -332,7 +337,7 @@ let rec mlexpr_of_atomic_tactic = function | Tacexpr.TacCut c -> <:expr< Tacexpr.TacCut $mlexpr_of_constr c$ >> | Tacexpr.TacAssert (t,ipat,c) -> - let ipat = mlexpr_of_intro_pattern ipat in + let ipat = mlexpr_of_located mlexpr_of_intro_pattern ipat in <:expr< Tacexpr.TacAssert $mlexpr_of_option mlexpr_of_tactic t$ $ipat$ $mlexpr_of_constr c$ >> | Tacexpr.TacGeneralize cl -> @@ -348,18 +353,18 @@ let rec mlexpr_of_atomic_tactic = function $mlexpr_of_bool b$ >> (* Derived basic tactics *) - | Tacexpr.TacSimpleInduction h -> - <:expr< Tacexpr.TacSimpleInduction ($mlexpr_of_quantified_hypothesis h$) >> - | Tacexpr.TacNewInduction (false,cl,cbo,ids,cls) -> - let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in - let ids = mlexpr_of_intro_pattern ids in - <:expr< Tacexpr.TacNewInduction False $mlexpr_of_list mlexpr_of_induction_arg cl$ $cbo$ $ids$ $mlexpr_of_option mlexpr_of_clause cls$ >> - | Tacexpr.TacSimpleDestruct h -> - <:expr< Tacexpr.TacSimpleDestruct $mlexpr_of_quantified_hypothesis h$ >> - | Tacexpr.TacNewDestruct (false,c,cbo,ids,cls) -> - let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in - let ids = mlexpr_of_intro_pattern ids in - <:expr< Tacexpr.TacNewDestruct False $mlexpr_of_list mlexpr_of_induction_arg c$ $cbo$ $ids$ $mlexpr_of_option mlexpr_of_clause cls$ >> + | Tacexpr.TacSimpleInductionDestruct (isrec,h) -> + <:expr< Tacexpr.TacSimpleInductionDestruct $mlexpr_of_bool isrec$ + $mlexpr_of_quantified_hypothesis h$ >> + | Tacexpr.TacInductionDestruct (isrec,ev,l) -> + <:expr< Tacexpr.TacInductionDestruct $mlexpr_of_bool isrec$ $mlexpr_of_bool ev$ + $mlexpr_of_list (mlexpr_of_quadruple + (mlexpr_of_list mlexpr_of_induction_arg) + (mlexpr_of_option mlexpr_of_constr_with_binding) + (mlexpr_of_pair + (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern)) + (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern))) + (mlexpr_of_option mlexpr_of_clause)) l$ >> (* Context management *) | Tacexpr.TacClear (b,l) -> @@ -371,7 +376,7 @@ let rec mlexpr_of_atomic_tactic = function | Tacexpr.TacMove (dep,id1,id2) -> <:expr< Tacexpr.TacMove $mlexpr_of_bool dep$ $mlexpr_of_hyp id1$ - $mlexpr_of_hyp id2$ >> + $mlexpr_of_move_location mlexpr_of_hyp id2$ >> (* Constructors *) | Tacexpr.TacLeft (ev,l) -> @@ -462,8 +467,8 @@ and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function $mlexpr_of_bool lz$ $mlexpr_of_tactic t$ $mlexpr_of_list (mlexpr_of_match_rule mlexpr_of_tactic) l$>> - | Tacexpr.TacMatchContext (lz,lr,l) -> - <:expr< Tacexpr.TacMatchContext + | Tacexpr.TacMatchGoal (lz,lr,l) -> + <:expr< Tacexpr.TacMatchGoal $mlexpr_of_bool lz$ $mlexpr_of_bool lr$ $mlexpr_of_list (mlexpr_of_match_rule mlexpr_of_tactic) l$>> |