diff options
Diffstat (limited to 'grammar/q_coqast.ml4')
-rw-r--r-- | grammar/q_coqast.ml4 | 568 |
1 files changed, 568 insertions, 0 deletions
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4 new file mode 100644 index 000000000..7467a32f0 --- /dev/null +++ b/grammar/q_coqast.ml4 @@ -0,0 +1,568 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Pp +open Names +open Q_util +open Compat + +let is_meta s = String.length s > 0 && s.[0] == '$' + +let purge_str s = + if String.length s == 0 || s.[0] <> '$' then s + else String.sub s 1 (String.length s - 1) + +let anti loc x = + expl_anti loc <:expr< $lid:purge_str x$ >> + +(* We don't give location for tactic quotation! *) +let loc = dummy_loc + +let dloc = <:expr< Pp.dummy_loc >> + +let mlexpr_of_ident id = + <:expr< Names.id_of_string $str:Names.string_of_id id$ >> + +let mlexpr_of_name = function + | Names.Anonymous -> <:expr< Names.Anonymous >> + | Names.Name id -> + <:expr< Names.Name (Names.id_of_string $str:Names.string_of_id id$) >> + +let mlexpr_of_dirpath dir = + let l = Names.repr_dirpath dir in + <:expr< Names.make_dirpath $mlexpr_of_list mlexpr_of_ident l$ >> + +let mlexpr_of_qualid qid = + let (dir, id) = Libnames.repr_qualid qid in + <:expr< Libnames.make_qualid $mlexpr_of_dirpath dir$ $mlexpr_of_ident id$ >> + +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 + | Misctypes.AN x -> <:expr< Misctypes.AN $f x$ >> + | Misctypes.ByNotation (loc,s,sco) -> + <:expr< Misctypes.ByNotation $dloc$ $str:s$ $mlexpr_of_option mlexpr_of_string sco$ >> + +let mlexpr_of_intro_pattern = function + | Misctypes.IntroWildcard -> <:expr< Misctypes.IntroWildcard >> + | Misctypes.IntroAnonymous -> <:expr< Misctypes.IntroAnonymous >> + | Misctypes.IntroFresh id -> <:expr< Misctypes.IntroFresh (mlexpr_of_ident $dloc$ id) >> + | Misctypes.IntroForthcoming b -> <:expr< Misctypes.IntroForthcoming (mlexpr_of_bool $dloc$ b) >> + | Misctypes.IntroIdentifier id -> + <:expr< Misctypes.IntroIdentifier (mlexpr_of_ident $dloc$ id) >> + | Misctypes.IntroOrAndPattern _ | Misctypes.IntroRewrite _ -> + failwith "mlexpr_of_intro_pattern: TODO" + +let mlexpr_of_ident_option = mlexpr_of_option (mlexpr_of_ident) + +let mlexpr_of_or_metaid f = function + | Tacexpr.AI a -> <:expr< Tacexpr.AI $f a$ >> + | Tacexpr.MetaId (_,id) -> <:expr< Tacexpr.AI $anti loc id$ >> + +let mlexpr_of_quantified_hypothesis = function + | Misctypes.AnonHyp n -> <:expr< Glob_term.AnonHyp $mlexpr_of_int n$ >> + | Misctypes.NamedHyp id -> <:expr< Glob_term.NamedHyp $mlexpr_of_ident id$ >> + +let mlexpr_of_or_var f = function + | Misctypes.ArgArg x -> <:expr< Misctypes.ArgArg $f x$ >> + | Misctypes.ArgVar id -> <:expr< Misctypes.ArgVar $mlexpr_of_located mlexpr_of_ident id$ >> + +let mlexpr_of_hyp = mlexpr_of_or_metaid (mlexpr_of_located mlexpr_of_ident) + +let mlexpr_of_occs = function + | Locus.AllOccurrences -> <:expr< Locus.AllOccurrences >> + | Locus.AllOccurrencesBut l -> + <:expr< Locus.AllOccurrencesBut + $mlexpr_of_list (mlexpr_of_or_var mlexpr_of_int) l$ >> + | Locus.NoOccurrences -> <:expr< Locus.NoOccurrences >> + | Locus.OnlyOccurrences l -> + <:expr< Locus.OnlyOccurrences + $mlexpr_of_list (mlexpr_of_or_var mlexpr_of_int) l$ >> + +let mlexpr_of_occurrences f = mlexpr_of_pair mlexpr_of_occs f + +let mlexpr_of_hyp_location = function + | occs, Locus.InHyp -> + <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Locus.InHyp) >> + | occs, Locus.InHypTypeOnly -> + <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Locus.InHypTypeOnly) >> + | occs, Locus.InHypValueOnly -> + <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Locus.InHypValueOnly) >> + +let mlexpr_of_clause cl = + <:expr< {Locus.onhyps= + $mlexpr_of_option (mlexpr_of_list mlexpr_of_hyp_location) + cl.Locus.onhyps$; + Locus.concl_occs= $mlexpr_of_occs cl.Locus.concl_occs$} >> + +let mlexpr_of_red_flags { + Genredexpr.rBeta = bb; + Genredexpr.rIota = bi; + Genredexpr.rZeta = bz; + Genredexpr.rDelta = bd; + Genredexpr.rConst = l +} = <:expr< { + Genredexpr.rBeta = $mlexpr_of_bool bb$; + Genredexpr.rIota = $mlexpr_of_bool bi$; + Genredexpr.rZeta = $mlexpr_of_bool bz$; + Genredexpr.rDelta = $mlexpr_of_bool bd$; + Genredexpr.rConst = $mlexpr_of_list (mlexpr_of_by_notation mlexpr_of_reference) l$ +} >> + +let mlexpr_of_explicitation = function + | Constrexpr.ExplByName id -> <:expr< Constrexpr.ExplByName $mlexpr_of_ident id$ >> + | Constrexpr.ExplByPos (n,_id) -> <:expr< Constrexpr.ExplByPos $mlexpr_of_int n$ >> + +let mlexpr_of_binding_kind = function + | Decl_kinds.Implicit -> <:expr< Decl_kinds.Implicit >> + | Decl_kinds.Explicit -> <:expr< Decl_kinds.Explicit >> + +let mlexpr_of_binder_kind = function + | Constrexpr.Default b -> <:expr< Constrexpr.Default $mlexpr_of_binding_kind b$ >> + | Constrexpr.Generalized (b,b',b'') -> + <:expr< Constrexpr.TypeClass $mlexpr_of_binding_kind b$ + $mlexpr_of_binding_kind b'$ $mlexpr_of_bool b''$ >> + +let rec mlexpr_of_constr = function + | Constrexpr.CRef (Libnames.Ident (loc,id)) when is_meta (string_of_id id) -> + anti loc (string_of_id id) + | Constrexpr.CRef r -> <:expr< Constrexpr.CRef $mlexpr_of_reference r$ >> + | Constrexpr.CFix (loc,_,_) -> failwith "mlexpr_of_constr: TODO" + | Constrexpr.CCoFix (loc,_,_) -> failwith "mlexpr_of_constr: TODO" + | Constrexpr.CProdN (loc,l,a) -> <:expr< Constrexpr.CProdN $dloc$ $mlexpr_of_list + (mlexpr_of_triple (mlexpr_of_list (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_name)) mlexpr_of_binder_kind mlexpr_of_constr) l$ $mlexpr_of_constr a$ >> + | Constrexpr.CLambdaN (loc,l,a) -> <:expr< Constrexpr.CLambdaN $dloc$ $mlexpr_of_list (mlexpr_of_triple (mlexpr_of_list (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_name)) mlexpr_of_binder_kind mlexpr_of_constr) l$ $mlexpr_of_constr a$ >> + | Constrexpr.CLetIn (loc,_,_,_) -> failwith "mlexpr_of_constr: TODO" + | Constrexpr.CAppExpl (loc,a,l) -> <:expr< Constrexpr.CAppExpl $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_reference a$ $mlexpr_of_list mlexpr_of_constr l$ >> + | Constrexpr.CApp (loc,a,l) -> <:expr< Constrexpr.CApp $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_constr a$ $mlexpr_of_list (mlexpr_of_pair mlexpr_of_constr (mlexpr_of_option (mlexpr_of_located mlexpr_of_explicitation))) l$ >> + | Constrexpr.CCases (loc,_,_,_,_) -> failwith "mlexpr_of_constr: TODO" + | Constrexpr.CHole (loc, None) -> <:expr< Constrexpr.CHole $dloc$ None >> + | Constrexpr.CHole (loc, Some _) -> failwith "mlexpr_of_constr: TODO CHole (Some _)" + | Constrexpr.CNotation(_,ntn,(subst,substl,[])) -> + <:expr< Constrexpr.CNotation $dloc$ $mlexpr_of_string ntn$ + ($mlexpr_of_list mlexpr_of_constr subst$, + $mlexpr_of_list (mlexpr_of_list mlexpr_of_constr) substl$,[]) >> + | Constrexpr.CPatVar (loc,n) -> + <:expr< Constrexpr.CPatVar $dloc$ $mlexpr_of_pair mlexpr_of_bool mlexpr_of_ident n$ >> + | _ -> failwith "mlexpr_of_constr: TODO" + +let mlexpr_of_occ_constr = + mlexpr_of_occurrences mlexpr_of_constr + +let mlexpr_of_red_expr = function + | Genredexpr.Red b -> <:expr< Genredexpr.Red $mlexpr_of_bool b$ >> + | Genredexpr.Hnf -> <:expr< Genredexpr.Hnf >> + | Genredexpr.Simpl o -> <:expr< Genredexpr.Simpl $mlexpr_of_option mlexpr_of_occ_constr o$ >> + | Genredexpr.Cbv f -> + <:expr< Genredexpr.Cbv $mlexpr_of_red_flags f$ >> + | Genredexpr.Lazy f -> + <:expr< Genredexpr.Lazy $mlexpr_of_red_flags f$ >> + | Genredexpr.Unfold l -> + let f1 = mlexpr_of_by_notation mlexpr_of_reference in + let f = mlexpr_of_list (mlexpr_of_occurrences f1) in + <:expr< Genredexpr.Unfold $f l$ >> + | Genredexpr.Fold l -> + <:expr< Genredexpr.Fold $mlexpr_of_list mlexpr_of_constr l$ >> + | Genredexpr.Pattern l -> + let f = mlexpr_of_list mlexpr_of_occ_constr in + <:expr< Genredexpr.Pattern $f l$ >> + | Genredexpr.CbvVm o -> <:expr< Genredexpr.CbvVm $mlexpr_of_option mlexpr_of_occ_constr o$ >> + | Genredexpr.ExtraRedExpr s -> + <:expr< Genredexpr.ExtraRedExpr $mlexpr_of_string s$ >> + +let rec mlexpr_of_argtype loc = function + | Genarg.BoolArgType -> <:expr< Genarg.BoolArgType >> + | Genarg.IntArgType -> <:expr< Genarg.IntArgType >> + | Genarg.IntOrVarArgType -> <:expr< Genarg.IntOrVarArgType >> + | Genarg.RefArgType -> <:expr< Genarg.RefArgType >> + | Genarg.PreIdentArgType -> <:expr< Genarg.PreIdentArgType >> + | Genarg.IntroPatternArgType -> <:expr< Genarg.IntroPatternArgType >> + | Genarg.IdentArgType b -> <:expr< Genarg.IdentArgType $mlexpr_of_bool b$ >> + | Genarg.VarArgType -> <:expr< Genarg.VarArgType >> + | Genarg.StringArgType -> <:expr< Genarg.StringArgType >> + | Genarg.QuantHypArgType -> <:expr< Genarg.QuantHypArgType >> + | Genarg.OpenConstrArgType b -> <:expr< Genarg.OpenConstrArgType $mlexpr_of_bool b$ >> + | Genarg.ConstrWithBindingsArgType -> <:expr< Genarg.ConstrWithBindingsArgType >> + | Genarg.BindingsArgType -> <:expr< Genarg.BindingsArgType >> + | Genarg.RedExprArgType -> <:expr< Genarg.RedExprArgType >> + | Genarg.SortArgType -> <:expr< Genarg.SortArgType >> + | Genarg.ConstrArgType -> <:expr< Genarg.ConstrArgType >> + | Genarg.ConstrMayEvalArgType -> <:expr< Genarg.ConstrMayEvalArgType >> + | Genarg.List0ArgType t -> <:expr< Genarg.List0ArgType $mlexpr_of_argtype loc t$ >> + | Genarg.List1ArgType t -> <:expr< Genarg.List1ArgType $mlexpr_of_argtype loc t$ >> + | Genarg.OptArgType t -> <:expr< Genarg.OptArgType $mlexpr_of_argtype loc t$ >> + | Genarg.PairArgType (t1,t2) -> + let t1 = mlexpr_of_argtype loc t1 in + let t2 = mlexpr_of_argtype loc t2 in + <:expr< Genarg.PairArgType $t1$ $t2$ >> + | Genarg.ExtraArgType s -> <:expr< Genarg.ExtraArgType $str:s$ >> + +let rec mlexpr_of_may_eval f = function + | Genredexpr.ConstrEval (r,c) -> + <:expr< Genredexpr.ConstrEval $mlexpr_of_red_expr r$ $f c$ >> + | Genredexpr.ConstrContext ((loc,id),c) -> + let id = mlexpr_of_ident id in + <:expr< Genredexpr.ConstrContext (loc,$id$) $f c$ >> + | Genredexpr.ConstrTypeOf c -> + <:expr< Genredexpr.ConstrTypeOf $mlexpr_of_constr c$ >> + | Genredexpr.ConstrTerm c -> + <:expr< Genredexpr.ConstrTerm $mlexpr_of_constr c$ >> + +let mlexpr_of_binding_kind = function + | Misctypes.ExplicitBindings l -> + let l = mlexpr_of_list (mlexpr_of_triple mlexpr_of_loc mlexpr_of_quantified_hypothesis mlexpr_of_constr) l in + <:expr< Misctypes.ExplicitBindings $l$ >> + | Misctypes.ImplicitBindings l -> + let l = mlexpr_of_list mlexpr_of_constr l in + <:expr< Misctypes.ImplicitBindings $l$ >> + | Misctypes.NoBindings -> + <:expr< Misctypes.NoBindings >> + +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 + | Misctypes.MoveAfter id -> <:expr< Misctypes.MoveAfter $f id$ >> + | Misctypes.MoveBefore id -> <:expr< Misctypes.MoveBefore $f id$ >> + | Misctypes.MoveFirst -> <:expr< Misctypes.MoveFirst >> + | Misctypes.MoveLast -> <:expr< Misctypes.MoveLast >> + +let mlexpr_of_induction_arg = function + | Tacexpr.ElimOnConstr c -> + <:expr< Tacexpr.ElimOnConstr $mlexpr_of_constr_with_binding c$ >> + | Tacexpr.ElimOnIdent (_,id) -> + <:expr< Tacexpr.ElimOnIdent $dloc$ $mlexpr_of_ident id$ >> + | Tacexpr.ElimOnAnonHyp n -> + <:expr< Tacexpr.ElimOnAnonHyp $mlexpr_of_int n$ >> + +let mlexpr_of_clause_pattern _ = failwith "mlexpr_of_clause_pattern: TODO" + +let mlexpr_of_pattern_ast = mlexpr_of_constr + +let mlexpr_of_entry_type = function + _ -> failwith "mlexpr_of_entry_type: TODO" + +let mlexpr_of_match_pattern = function + | Tacexpr.Term t -> <:expr< Tacexpr.Term $mlexpr_of_pattern_ast t$ >> + | Tacexpr.Subterm (b,ido,t) -> + <:expr< Tacexpr.Subterm $mlexpr_of_bool b$ $mlexpr_of_option mlexpr_of_ident ido$ $mlexpr_of_pattern_ast t$ >> + +let mlexpr_of_match_context_hyps = function + | Tacexpr.Hyp (id,l) -> + let f = mlexpr_of_located mlexpr_of_name in + <:expr< Tacexpr.Hyp $f id$ $mlexpr_of_match_pattern l$ >> + | Tacexpr.Def (id,v,l) -> + let f = mlexpr_of_located mlexpr_of_name in + <:expr< Tacexpr.Def $f id$ $mlexpr_of_match_pattern v$ $mlexpr_of_match_pattern l$ >> + +let mlexpr_of_match_rule f = function + | Tacexpr.Pat (l,mp,t) -> <:expr< Tacexpr.Pat $mlexpr_of_list mlexpr_of_match_context_hyps l$ $mlexpr_of_match_pattern mp$ $f t$ >> + | Tacexpr.All t -> <:expr< Tacexpr.All $f t$ >> + +let mlexpr_of_message_token = function + | Tacexpr.MsgString s -> <:expr< Tacexpr.MsgString $str:s$ >> + | Tacexpr.MsgInt n -> <:expr< Tacexpr.MsgInt $mlexpr_of_int n$ >> + | Tacexpr.MsgIdent id -> <:expr< Tacexpr.MsgIdent $mlexpr_of_hyp id$ >> + +let mlexpr_of_debug = function + | Tacexpr.Off -> <:expr< Tacexpr.Off >> + | Tacexpr.Debug -> <:expr< Tacexpr.Debug >> + | Tacexpr.Info -> <:expr< Tacexpr.Info >> + +let rec mlexpr_of_atomic_tactic = function + (* Basic tactics *) + | Tacexpr.TacIntroPattern pl -> + 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_move_location mlexpr_of_hyp idopt' in + <:expr< Tacexpr.TacIntroMove $idopt$ $idopt'$ >> + | Tacexpr.TacAssumption -> + <:expr< Tacexpr.TacAssumption >> + | Tacexpr.TacExact c -> + <:expr< Tacexpr.TacExact $mlexpr_of_constr c$ >> + | Tacexpr.TacExactNoCheck c -> + <:expr< Tacexpr.TacExactNoCheck $mlexpr_of_constr c$ >> + | Tacexpr.TacVmCastNoCheck c -> + <:expr< Tacexpr.TacVmCastNoCheck $mlexpr_of_constr c$ >> + | Tacexpr.TacApply (b,false,cb,None) -> + <:expr< Tacexpr.TacApply $mlexpr_of_bool b$ False $mlexpr_of_list mlexpr_of_constr_with_binding cb$ None >> + | 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 + <:expr< Tacexpr.TacElim False $cb$ $cbo$ >> + | Tacexpr.TacElimType c -> + <:expr< Tacexpr.TacElimType $mlexpr_of_constr c$ >> + | Tacexpr.TacCase (false,cb) -> + let cb = mlexpr_of_constr_with_binding cb in + <:expr< Tacexpr.TacCase False $cb$ >> + | Tacexpr.TacCaseType c -> + <:expr< Tacexpr.TacCaseType $mlexpr_of_constr c$ >> + | Tacexpr.TacFix (ido,n) -> + let ido = mlexpr_of_ident_option ido in + let n = mlexpr_of_int n in + <:expr< Tacexpr.TacFix $ido$ $n$ >> + | Tacexpr.TacMutualFix (b,id,n,l) -> + let b = mlexpr_of_bool b in + let id = mlexpr_of_ident id in + let n = mlexpr_of_int n in + let f =mlexpr_of_triple mlexpr_of_ident mlexpr_of_int mlexpr_of_constr in + let l = mlexpr_of_list f l in + <:expr< Tacexpr.TacMutualFix $b$ $id$ $n$ $l$ >> + | Tacexpr.TacCofix ido -> + let ido = mlexpr_of_ident_option ido in + <:expr< Tacexpr.TacCofix $ido$ >> + | Tacexpr.TacMutualCofix (b,id,l) -> + let b = mlexpr_of_bool b in + let id = mlexpr_of_ident id in + let f = mlexpr_of_pair mlexpr_of_ident mlexpr_of_constr in + let l = mlexpr_of_list f l in + <:expr< Tacexpr.TacMutualCofix $b$ $id$ $l$ >> + + | Tacexpr.TacCut c -> + <:expr< Tacexpr.TacCut $mlexpr_of_constr c$ >> + | Tacexpr.TacAssert (t,ipat,c) -> + let ipat = mlexpr_of_option (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 -> + <:expr< Tacexpr.TacGeneralize + $mlexpr_of_list + (mlexpr_of_pair mlexpr_of_occ_constr mlexpr_of_name) cl$ >> + | Tacexpr.TacGeneralizeDep c -> + <:expr< Tacexpr.TacGeneralizeDep $mlexpr_of_constr c$ >> + | Tacexpr.TacLetTac (na,c,cl,b) -> + let na = mlexpr_of_name na in + let cl = mlexpr_of_clause_pattern cl in + <:expr< Tacexpr.TacLetTac $na$ $mlexpr_of_constr c$ $cl$ + $mlexpr_of_bool b$ >> + + (* Derived basic tactics *) + | 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_pair (mlexpr_of_list (mlexpr_of_triple + (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) -> + let l = mlexpr_of_list (mlexpr_of_hyp) l in + <:expr< Tacexpr.TacClear $mlexpr_of_bool b$ $l$ >> + | Tacexpr.TacClearBody l -> + let l = mlexpr_of_list (mlexpr_of_hyp) l in + <:expr< Tacexpr.TacClearBody $l$ >> + | Tacexpr.TacMove (dep,id1,id2) -> + <:expr< Tacexpr.TacMove $mlexpr_of_bool dep$ + $mlexpr_of_hyp id1$ + $mlexpr_of_move_location mlexpr_of_hyp id2$ >> + + (* Constructors *) + | Tacexpr.TacLeft (ev,l) -> + <:expr< Tacexpr.TacLeft $mlexpr_of_bool ev$ $mlexpr_of_binding_kind l$>> + | Tacexpr.TacRight (ev,l) -> + <:expr< Tacexpr.TacRight $mlexpr_of_bool ev$ $mlexpr_of_binding_kind l$>> + | Tacexpr.TacSplit (ev,b,l) -> + <:expr< Tacexpr.TacSplit + ($mlexpr_of_bool ev$,$mlexpr_of_bool b$,$mlexpr_of_list mlexpr_of_binding_kind l$)>> + | Tacexpr.TacAnyConstructor (ev,t) -> + <:expr< Tacexpr.TacAnyConstructor $mlexpr_of_bool ev$ $mlexpr_of_option mlexpr_of_tactic t$>> + | Tacexpr.TacConstructor (ev,n,l) -> + let n = mlexpr_of_or_var mlexpr_of_int n in + <:expr< Tacexpr.TacConstructor $mlexpr_of_bool ev$ $n$ $mlexpr_of_binding_kind l$>> + + (* Conversion *) + | Tacexpr.TacReduce (r,cl) -> + let l = mlexpr_of_clause cl in + <:expr< Tacexpr.TacReduce $mlexpr_of_red_expr r$ $l$ >> + | Tacexpr.TacChange (p,c,cl) -> + let l = mlexpr_of_clause cl in + let g = mlexpr_of_option mlexpr_of_constr in + <:expr< Tacexpr.TacChange $g p$ $mlexpr_of_constr c$ $l$ >> + + (* Equivalence relations *) + | Tacexpr.TacReflexivity -> <:expr< Tacexpr.TacReflexivity >> + | Tacexpr.TacSymmetry ido -> <:expr< Tacexpr.TacSymmetry $mlexpr_of_clause ido$ >> + | Tacexpr.TacTransitivity c -> <:expr< Tacexpr.TacTransitivity $mlexpr_of_option mlexpr_of_constr c$ >> + + (* Automation tactics *) + | Tacexpr.TacAuto (debug,n,lems,l) -> + let d = mlexpr_of_debug debug in + let n = mlexpr_of_option (mlexpr_of_or_var mlexpr_of_int) n in + let lems = mlexpr_of_list mlexpr_of_constr lems in + let l = mlexpr_of_option (mlexpr_of_list mlexpr_of_string) l in + <:expr< Tacexpr.TacAuto $d$ $n$ $lems$ $l$ >> + | Tacexpr.TacTrivial (debug,lems,l) -> + let d = mlexpr_of_debug debug in + let l = mlexpr_of_option (mlexpr_of_list mlexpr_of_string) l in + let lems = mlexpr_of_list mlexpr_of_constr lems in + <:expr< Tacexpr.TacTrivial $d$ $lems$ $l$ >> + + | _ -> failwith "Quotation of atomic tactic expressions: TODO" + +and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function + | Tacexpr.TacAtom (loc,t) -> + <:expr< Tacexpr.TacAtom $dloc$ $mlexpr_of_atomic_tactic t$ >> + | Tacexpr.TacThen (t1,[||],t2,[||]) -> + <:expr< Tacexpr.TacThen $mlexpr_of_tactic t1$ [||] $mlexpr_of_tactic t2$ [||]>> + | Tacexpr.TacThens (t,tl) -> + <:expr< Tacexpr.TacThens $mlexpr_of_tactic t$ $mlexpr_of_list mlexpr_of_tactic tl$>> + | Tacexpr.TacFirst tl -> + <:expr< Tacexpr.TacFirst $mlexpr_of_list mlexpr_of_tactic tl$ >> + | Tacexpr.TacSolve tl -> + <:expr< Tacexpr.TacSolve $mlexpr_of_list mlexpr_of_tactic tl$ >> + | Tacexpr.TacTry t -> + <:expr< Tacexpr.TacTry $mlexpr_of_tactic t$ >> + | Tacexpr.TacOrelse (t1,t2) -> + <:expr< Tacexpr.TacOrelse $mlexpr_of_tactic t1$ $mlexpr_of_tactic t2$ >> + | Tacexpr.TacDo (n,t) -> + <:expr< Tacexpr.TacDo $mlexpr_of_or_var mlexpr_of_int n$ $mlexpr_of_tactic t$ >> + | Tacexpr.TacTimeout (n,t) -> + <:expr< Tacexpr.TacTimeout $mlexpr_of_or_var mlexpr_of_int n$ $mlexpr_of_tactic t$ >> + | Tacexpr.TacRepeat t -> + <:expr< Tacexpr.TacRepeat $mlexpr_of_tactic t$ >> + | Tacexpr.TacProgress t -> + <:expr< Tacexpr.TacProgress $mlexpr_of_tactic t$ >> + | Tacexpr.TacId l -> + <:expr< Tacexpr.TacId $mlexpr_of_list mlexpr_of_message_token l$ >> + | Tacexpr.TacFail (n,l) -> + <:expr< Tacexpr.TacFail $mlexpr_of_or_var mlexpr_of_int n$ $mlexpr_of_list mlexpr_of_message_token l$ >> +(* + | Tacexpr.TacInfo t -> TacInfo (loc,f t) + + | Tacexpr.TacRec (id,(idl,t)) -> TacRec (loc,(id,(idl,f t))) + | Tacexpr.TacRecIn (l,t) -> TacRecIn(loc,List.map (fun (id,t) -> (id,f t)) l,f t) +*) + | Tacexpr.TacLetIn (isrec,l,t) -> + let f = + mlexpr_of_pair + (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_ident) + mlexpr_of_tactic_arg in + <:expr< Tacexpr.TacLetIn $mlexpr_of_bool isrec$ $mlexpr_of_list f l$ $mlexpr_of_tactic t$ >> + | Tacexpr.TacMatch (lz,t,l) -> + <:expr< Tacexpr.TacMatch + $mlexpr_of_bool lz$ + $mlexpr_of_tactic t$ + $mlexpr_of_list (mlexpr_of_match_rule mlexpr_of_tactic) l$>> + | 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$>> + + | Tacexpr.TacFun (idol,body) -> + <:expr< Tacexpr.TacFun + ($mlexpr_of_list mlexpr_of_ident_option idol$, + $mlexpr_of_tactic body$) >> + | Tacexpr.TacArg (_,Tacexpr.MetaIdArg (_,true,id)) -> anti loc id + | Tacexpr.TacArg (_,t) -> + <:expr< Tacexpr.TacArg $dloc$ $mlexpr_of_tactic_arg t$ >> + | Tacexpr.TacComplete t -> + <:expr< Tacexpr.TacComplete $mlexpr_of_tactic t$ >> + | _ -> failwith "Quotation of tactic expressions: TODO" + +and mlexpr_of_tactic_arg = function + | Tacexpr.MetaIdArg (loc,true,id) -> anti loc id + | Tacexpr.MetaIdArg (loc,false,id) -> + <:expr< Tacexpr.ConstrMayEval (Genredexpr.ConstrTerm $anti loc id$) >> + | Tacexpr.TacCall (loc,t,tl) -> + <:expr< Tacexpr.TacCall $dloc$ $mlexpr_of_reference t$ $mlexpr_of_list mlexpr_of_tactic_arg tl$>> + | Tacexpr.Tacexp t -> + <:expr< Tacexpr.Tacexp $mlexpr_of_tactic t$ >> + | Tacexpr.ConstrMayEval c -> + <:expr< Tacexpr.ConstrMayEval $mlexpr_of_may_eval mlexpr_of_constr c$ >> + | Tacexpr.Reference r -> + <:expr< Tacexpr.Reference $mlexpr_of_reference r$ >> + | _ -> failwith "mlexpr_of_tactic_arg: TODO" + + +IFDEF CAMLP5 THEN + +let not_impl x = + let desc = + if Obj.is_block (Obj.repr x) then + "tag = " ^ string_of_int (Obj.tag (Obj.repr x)) + else "int_val = " ^ string_of_int (Obj.magic x) + in + failwith ("<Q_coqast.patt_of_expt, not impl: " ^ desc) + +(* The following function is written without quotation + in order to be parsable even by camlp4. The version with + quotation can be found in revision <= 12972 of [q_util.ml4] *) + +open MLast + +let rec patt_of_expr e = + let loc = loc_of_expr e in + match e with + | ExAcc (_, e1, e2) -> PaAcc (loc, patt_of_expr e1, patt_of_expr e2) + | ExApp (_, e1, e2) -> PaApp (loc, patt_of_expr e1, patt_of_expr e2) + | ExLid (_, x) when x = vala "loc" -> PaAny loc + | ExLid (_, s) -> PaLid (loc, s) + | ExUid (_, s) -> PaUid (loc, s) + | ExStr (_, s) -> PaStr (loc, s) + | ExAnt (_, e) -> PaAnt (loc, patt_of_expr e) + | _ -> not_impl e + +let fconstr e = + let ee s = + mlexpr_of_constr (Pcoq.Gram.entry_parse e + (Pcoq.Gram.parsable (Stream.of_string s))) + in + let ep s = patt_of_expr (ee s) in + Quotation.ExAst (ee, ep) + +let ftac e = + let ee s = + mlexpr_of_tactic (Pcoq.Gram.entry_parse e + (Pcoq.Gram.parsable (Stream.of_string s))) + in + let ep s = patt_of_expr (ee s) in + Quotation.ExAst (ee, ep) + +let _ = + Quotation.add "constr" (fconstr Pcoq.Constr.constr_eoi); + Quotation.add "tactic" (ftac Pcoq.Tactic.tactic_eoi); + Quotation.default := "constr" + +ELSE + +open Pcaml + +let expand_constr_quot_expr loc _loc_name_opt contents = + mlexpr_of_constr + (Pcoq.Gram.parse_string Pcoq.Constr.constr_eoi loc contents) + +let expand_tactic_quot_expr loc _loc_name_opt contents = + mlexpr_of_tactic + (Pcoq.Gram.parse_string Pcoq.Tactic.tactic_eoi loc contents) + +let _ = + (* FIXME: for the moment, we add quotations in expressions only, not pattern *) + Quotation.add "constr" Quotation.DynAst.expr_tag expand_constr_quot_expr; + Quotation.add "tactic" Quotation.DynAst.expr_tag expand_tactic_quot_expr; + Quotation.default := "constr" + +END |