diff options
Diffstat (limited to 'parsing/q_coqast.ml4')
| -rw-r--r-- | parsing/q_coqast.ml4 | 476 |
1 files changed, 438 insertions, 38 deletions
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index 5670b2ce5..14bd4498b 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -8,19 +8,12 @@ (* $Id$ *) +open Q_util + let dummy_loc = (0,0) let is_meta s = String.length s > 0 && s.[0] == '$' -let not_impl name 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." ^ name ^ ", not impl: " ^ desc) - let purge_str s = if String.length s == 0 || s.[0] <> '$' then s else String.sub s 1 (String.length s - 1) @@ -31,11 +24,11 @@ let anti loc x = in <:expr< $anti:e$ >> -(* [expr_of_ast] contributes to translate g_*.ml4 files into g_*.ppo *) +(* [mlexpr_of_ast] contributes to translate g_*.ml4 files into g_*.ppo *) (* This is where $id's (and macros) in ast are translated in ML variables *) (* which will bind their actual ast value *) -let rec expr_of_ast = function +let rec mlexpr_of_ast = function | Coqast.Nmeta loc id -> anti loc id | Coqast.Id loc id when is_meta id -> <:expr< Coqast.Id loc $anti loc id$ >> | Coqast.Node _ "$VAR" [Coqast.Nmeta loc x] -> @@ -53,35 +46,36 @@ let rec expr_of_ast = function (* Obsolète | Coqast.Node _ "$SLAM" [Coqast.Nmeta loc idl; y] -> <:expr< - List.fold_right (Pcoq.slam_ast loc) $anti loc idl$ $expr_of_ast y$ >> + List.fold_right (Pcoq.slam_ast loc) $anti loc idl$ $mlexpr_of_ast y$ >> *) | Coqast.Node loc "$ABSTRACT" [Coqast.Str _ s; x; y] -> - <:expr< - Pcoq.abstract_binders_ast loc $str:s$ $expr_of_ast x$ $expr_of_ast y$ >> + let x = mlexpr_of_ast x in + let y = mlexpr_of_ast y in + <:expr< Ast.abstract_binders_ast loc $str:s$ $x$ $y$ >> | Coqast.Node loc nn al -> let e = expr_list_of_ast_list al in <:expr< Coqast.Node loc $str:nn$ $e$ >> | Coqast.Nvar loc id -> <:expr< Coqast.Nvar loc (Names.id_of_string $str:Names.string_of_id id$) >> | Coqast.Slam loc None a -> - <:expr< Coqast.Slam loc None $expr_of_ast a$ >> + <:expr< Coqast.Slam loc None $mlexpr_of_ast a$ >> | Coqast.Smetalam loc s a -> <:expr< match $anti loc s$ with - [ Coqast.Nvar _ id -> Coqast.Slam loc (Some id) $expr_of_ast a$ - | Coqast.Nmeta _ s -> Coqast.Smetalam loc s $expr_of_ast a$ + [ Coqast.Nvar _ id -> Coqast.Slam loc (Some id) $mlexpr_of_ast a$ + | Coqast.Nmeta _ s -> Coqast.Smetalam loc s $mlexpr_of_ast a$ | _ -> failwith "Slam expects a var or a metavar" ] >> | Coqast.Slam loc (Some s) a -> let se = <:expr< Names.id_of_string $str:Names.string_of_id s$ >> in - <:expr< Coqast.Slam loc (Some $se$) $expr_of_ast a$ >> + <:expr< Coqast.Slam loc (Some $se$) $mlexpr_of_ast a$ >> | Coqast.Num loc i -> <:expr< Coqast.Num loc $int:string_of_int i$ >> | Coqast.Id loc id -> <:expr< Coqast.Id loc $str:id$ >> | Coqast.Str loc str -> <:expr< Coqast.Str loc $str:str$ >> | Coqast.Path loc qid -> let l,a = Names.repr_path qid in - let expr_of_modid id = + let mlexpr_of_modid id = <:expr< Names.id_of_string $str:Names.string_of_id id$ >> in - let e = List.map expr_of_modid (Names.repr_dirpath l) in + let e = List.map mlexpr_of_modid (Names.repr_dirpath l) in let e = expr_list_of_var_list e in <:expr< Coqast.Path loc (Names.make_path (Names.make_dirpath $e$) (Names.id_of_string $str:Names.string_of_id a$)) >> @@ -98,7 +92,7 @@ and expr_list_of_ast_list al = then <:expr< $e1$ >> else <:expr< ( $lid:"@"$ $e1$ $e2$) >> | _ -> - let e1 = expr_of_ast a in + let e1 = mlexpr_of_ast a in let loc = (fst(MLast.loc_of_expr e1), snd(MLast.loc_of_expr e2)) in <:expr< [$e1$ :: $e2$] >> ) al (let loc = dummy_loc in <:expr< [] >>) @@ -110,31 +104,437 @@ and expr_list_of_var_list sl = let loc = (fst (MLast.loc_of_expr e1), snd (MLast.loc_of_expr e2)) in <:expr< [$e1$ :: $e2$] >>) sl <:expr< [] >> - -let rec patt_of_expr e = - let loc = MLast.loc_of_expr e in - match e with - | <:expr< $e1$.$e2$ >> -> <:patt< $patt_of_expr e1$.$patt_of_expr e2$ >> - | <:expr< $e1$ $e2$ >> -> <:patt< $patt_of_expr e1$ $patt_of_expr e2$ >> - | <:expr< loc >> -> <:patt< _ >> - | <:expr< $lid:s$ >> -> <:patt< $lid:s$ >> - | <:expr< $uid:s$ >> -> <:patt< $uid:s$ >> - | <:expr< $str:s$ >> -> <:patt< $str:s$ >> - | <:expr< $anti:e$ >> -> <:patt< $anti:patt_of_expr e$ >> - | _ -> not_impl "patt_of_expr" e + +(* We don't give location for tactic quotation! *) +let loc = 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.Names (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) = Nametab.repr_qualid qid in + <:expr< Nametab.make_qualid $mlexpr_of_dirpath dir$ $mlexpr_of_ident id$ >> + +let mlexpr_of_reference = function + | Tacexpr.RQualid (loc,qid) -> <:expr< Tacexpr.RQualid loc $mlexpr_of_qualid qid$ >> + | Tacexpr.RIdent (loc,id) -> <:expr< Tacexpr.RIdent loc $mlexpr_of_ident id$ >> + +let mlexpr_of_bool = function + | true -> <:expr< True >> + | false -> <:expr< False >> + +let mlexpr_of_intro_pattern = function + | Tacexpr.IntroOrAndPattern _ -> failwith "mlexpr_of_intro_pattern: TODO" + | Tacexpr.IntroWildcard -> <:expr< Tacexpr.IntroWildcard >> + | Tacexpr.IntroIdentifier id -> + <:expr< Tacexpr.IntroIdentifier (mlexpr_of_ident loc id) >> + +let mlexpr_of_ident_option = mlexpr_of_option (mlexpr_of_ident) + +let mlexpr_of_or_metanum f = function + | Rawterm.AN (_,a) -> <:expr< Rawterm.AN loc $f a$ >> + | Rawterm.MetaNum (_,n) -> + <:expr< Rawterm.MetaNum loc $mlexpr_of_int n$ >> + +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 + | 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< (loc, $f x$) >> + +let mlexpr_of_hyp_location = function + | Tacexpr.InHyp id -> + <:expr< Tacexpr.InHyp $mlexpr_of_or_metaid (mlexpr_of_located mlexpr_of_ident) id$ >> + | Tacexpr.InHypType id -> + <:expr< Tacexpr.InHypType $mlexpr_of_or_metaid (mlexpr_of_located mlexpr_of_ident) id$ >> + +(* +let mlexpr_of_red_mode = function + | Closure.UNIFORM -> <:expr< Closure.UNIFORM >> + | Closure.SIMPL -> <:expr< Closure.SIMPL >> + | Closure.WITHBACK -> <:expr< Closure.WITHBACK >> +*) + +let mlexpr_of_red_flags { + Rawterm.rBeta = bb; + Rawterm.rIota = bi; + Rawterm.rZeta = bz; + Rawterm.rDelta = bd; + Rawterm.rConst = l +} = <:expr< { + Rawterm.rBeta = $mlexpr_of_bool bb$; + Rawterm.rIota = $mlexpr_of_bool bi$; + Rawterm.rZeta = $mlexpr_of_bool bz$; + Rawterm.rDelta = $mlexpr_of_bool bd$; + Rawterm.rConst = $mlexpr_of_list (mlexpr_of_or_metanum mlexpr_of_qualid) l$ +} >> + +let mlexpr_of_constr = mlexpr_of_ast + +let mlexpr_of_red_expr = function + | Rawterm.Red b -> <:expr< Rawterm.Red $mlexpr_of_bool b$ >> + | Rawterm.Hnf -> <:expr< Rawterm.Hnf >> + | Rawterm.Simpl -> <:expr< Rawterm.Simpl >> + | Rawterm.Cbv f -> + <:expr< Rawterm.Cbv $mlexpr_of_red_flags f$ >> + | Rawterm.Lazy f -> + <:expr< Rawterm.Lazy $mlexpr_of_red_flags f$ >> + | Rawterm.Unfold l -> + let f1 = mlexpr_of_list mlexpr_of_int in + let f2 = mlexpr_of_or_metanum mlexpr_of_qualid in + let f = mlexpr_of_list (mlexpr_of_pair f1 f2) in + <:expr< Rawterm.Unfold $f l$ >> + | Rawterm.Fold l -> + <:expr< Rawterm.Fold $mlexpr_of_list mlexpr_of_constr l$ >> + | Rawterm.Pattern l -> + let f1 = mlexpr_of_list mlexpr_of_int in + let f = mlexpr_of_list (mlexpr_of_pair f1 mlexpr_of_constr) in + <:expr< Rawterm.Pattern $f l$ >> + | Rawterm.ExtraRedExpr (s,l) -> + let l = mlexpr_of_list mlexpr_of_constr l in + <:expr< Rawterm.ExtraRedExpr $mlexpr_of_string s$ $l$ >> + +let rec mlexpr_of_argtype loc = function + | Genarg.BoolArgType -> <:expr< Genarg.BoolArgType >> + | Genarg.IntArgType -> <:expr< Genarg.IntArgType >> + | Genarg.IntOrVarArgType -> <:expr< Genarg.IntOrVarArgType >> + | Genarg.QualidArgType -> <:expr< Genarg.QualidArgType >> + | Genarg.PreIdentArgType -> <:expr< Genarg.PreIdentArgType >> + | Genarg.IdentArgType -> <:expr< Genarg.IdentArgType >> + | Genarg.StringArgType -> <:expr< Genarg.StringArgType >> + | Genarg.QuantHypArgType -> <:expr< Genarg.QuantHypArgType >> + | Genarg.CastedOpenConstrArgType -> <:expr< Genarg.CastedOpenConstrArgType >> + | Genarg.ConstrWithBindingsArgType -> <:expr< Genarg.ConstrWithBindingsArgType >> + | Genarg.RedExprArgType -> <:expr< Genarg.RedExprArgType >> + | Genarg.TacticArgType -> <:expr< Genarg.TacticArgType >> + | 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 + | Rawterm.ConstrEval (r,c) -> + <:expr< Rawterm.ConstrEval $mlexpr_of_red_expr r$ $f c$ >> + | Rawterm.ConstrContext ((loc,id),c) -> + let id = mlexpr_of_ident id in + <:expr< Rawterm.ConstrContext (loc,$id$) $f c$ >> + | Rawterm.ConstrTypeOf c -> + <:expr< Rawterm.ConstrTypeOf $mlexpr_of_constr c$ >> + | Rawterm.ConstrTerm c -> + <:expr< Rawterm.ConstrTerm $mlexpr_of_constr c$ >> + +let mlexpr_of_binding_kind = function + | Rawterm.ExplicitBindings l -> + let l = mlexpr_of_list (mlexpr_of_pair mlexpr_of_quantified_hypothesis mlexpr_of_constr) l in + <:expr< Rawterm.ExplicitBindings $l$ >> + | Rawterm.ImplicitBindings l -> + let l = mlexpr_of_list mlexpr_of_constr l in + <:expr< Rawterm.ImplicitBindings $l$ >> + | Rawterm.NoBindings -> + <:expr< Rawterm.NoBindings >> + +let mlexpr_of_induction_arg = function + | Tacexpr.ElimOnConstr c -> + <:expr< Tacexpr.ElimOnConstr $mlexpr_of_constr c$ >> + | Tacexpr.ElimOnIdent (_,id) -> + <:expr< Tacexpr.ElimOnIdent loc $mlexpr_of_ident id$ >> + | Tacexpr.ElimOnAnonHyp n -> + <:expr< Tacexpr.ElimOnAnonHyp $mlexpr_of_int n$ >> + +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_clause_pattern _ = failwith "mlexpr_of_clause_pattern: TODO" + +let mlexpr_of_pattern_ast = mlexpr_of_ast + +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 (ido,t) -> + <:expr< Tacexpr.Subterm $mlexpr_of_option mlexpr_of_ident ido$ $mlexpr_of_pattern_ast t$ >> + +let mlexpr_of_match_context_hyps = function + | Tacexpr.NoHypId l -> <:expr< Tacexpr.NoHypId $mlexpr_of_match_pattern l$ >> + | Tacexpr.Hyp (id,l) -> + let f = mlexpr_of_located mlexpr_of_ident in + <:expr< Tacexpr.Hyp $f id$ $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 rec mlexpr_of_atomic_tactic = function + (* Basic tactics *) + | Tacexpr.TacIntroPattern pl -> + let pl = mlexpr_of_list 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 + <:expr< Tacexpr.TacIntroMove $idopt$ $idopt'$ >> + | Tacexpr.TacAssumption -> + <:expr< Tacexpr.TacAssumption >> + | Tacexpr.TacExact c -> + <:expr< Tacexpr.TacExact $mlexpr_of_constr c$ >> + | Tacexpr.TacApply cb -> + <:expr< Tacexpr.TacApply $mlexpr_of_constr_with_binding cb$ >> + | Tacexpr.TacElim (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 $cb$ $cbo$ >> + | Tacexpr.TacElimType c -> + <:expr< Tacexpr.TacElimType $mlexpr_of_constr c$ >> + | Tacexpr.TacCase cb -> + let cb = mlexpr_of_constr_with_binding cb in + <:expr< Tacexpr.TacCase $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 (id,n,l) -> + 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 $id$ $n$ $l$ >> + | Tacexpr.TacCofix ido -> + let ido = mlexpr_of_ident_option ido in + <:expr< Tacexpr.TacCofix $ido$ >> + | Tacexpr.TacMutualCofix (id,l) -> + 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 $id$ $l$ >> + + | Tacexpr.TacCut c -> + <:expr< Tacexpr.TacCut $mlexpr_of_constr c$ >> + | Tacexpr.TacTrueCut (ido,c) -> + let ido = mlexpr_of_ident_option ido in + <:expr< Tacexpr.TacTrueCut $ido$ $mlexpr_of_constr c$ >> + | Tacexpr.TacForward (b,na,c) -> + <:expr< Tacexpr.TacForward $mlexpr_of_bool b$ $mlexpr_of_name na$ $mlexpr_of_constr c$ >> + | Tacexpr.TacGeneralize cl -> + <:expr< Tacexpr.TacGeneralize $mlexpr_of_list mlexpr_of_constr cl$ >> + | Tacexpr.TacGeneralizeDep c -> + <:expr< Tacexpr.TacGeneralizeDep $mlexpr_of_constr c$ >> + | Tacexpr.TacLetTac (id,c,cl) -> + let id = mlexpr_of_ident id in + let cl = mlexpr_of_clause_pattern cl in + <:expr< Tacexpr.TacLetTac $id$ $mlexpr_of_constr c$ $cl$ >> + + (* Derived basic tactics *) + | Tacexpr.TacOldInduction h -> + <:expr< Tacexpr.TacOldInduction $mlexpr_of_quantified_hypothesis h$ >> + | Tacexpr.TacNewInduction c -> + <:expr< Tacexpr.TacNewInduction $mlexpr_of_induction_arg c$ >> + | Tacexpr.TacOldDestruct h -> + <:expr< Tacexpr.TacOldDestruct $mlexpr_of_quantified_hypothesis h$ >> + | Tacexpr.TacNewDestruct c -> + <:expr< Tacexpr.TacNewDestruct $mlexpr_of_induction_arg c$ >> + + (* Context management *) + | Tacexpr.TacClear l -> + let l = mlexpr_of_list (mlexpr_of_or_metanum mlexpr_of_ident) l in + <:expr< Tacexpr.TacClear $l$ >> + | Tacexpr.TacClearBody l -> + let l = mlexpr_of_list (mlexpr_of_or_metanum mlexpr_of_ident) l in + <:expr< Tacexpr.TacClearBody $l$ >> + | Tacexpr.TacMove (dep,id1,id2) -> + <:expr< Tacexpr.TacMove $mlexpr_of_bool dep$ + $mlexpr_of_located mlexpr_of_ident id1$ + $mlexpr_of_located mlexpr_of_ident id2$ >> + + (* Constructors *) + | Tacexpr.TacLeft l -> + <:expr< Tacexpr.TacLeft $mlexpr_of_binding_kind l$>> + | Tacexpr.TacRight l -> + <:expr< Tacexpr.TacRight $mlexpr_of_binding_kind l$>> + | Tacexpr.TacSplit l -> + <:expr< Tacexpr.TacSplit $mlexpr_of_binding_kind l$>> + | Tacexpr.TacAnyConstructor t -> + <:expr< Tacexpr.TacAnyConstructor $mlexpr_of_option mlexpr_of_tactic t$>> + | Tacexpr.TacConstructor (n,l) -> + let n = mlexpr_of_or_metaid mlexpr_of_int n in + <:expr< Tacexpr.TacConstructor $n$ $mlexpr_of_binding_kind l$>> + + (* Conversion *) + | Tacexpr.TacReduce (r,cl) -> + let l = mlexpr_of_list mlexpr_of_hyp_location cl in + <:expr< Tacexpr.TacReduce $mlexpr_of_red_expr r$ $l$ >> + | Tacexpr.TacChange (c,cl) -> + let l = mlexpr_of_list mlexpr_of_hyp_location cl in + <:expr< Tacexpr.TacChange $mlexpr_of_constr c$ $l$ >> + + (* Equivalence relations *) + | Tacexpr.TacReflexivity -> <:expr< Tacexpr.TacReflexivity >> + | Tacexpr.TacSymmetry -> <:expr< Tacexpr.TacSymmetry >> + | Tacexpr.TacTransitivity c -> <:expr< Tacexpr.TacTransitivity $mlexpr_of_constr c$ >> + + (* Automation tactics *) + | Tacexpr.TacAuto (n,l) -> + let n = mlexpr_of_option mlexpr_of_int n in + let l = mlexpr_of_option (mlexpr_of_list mlexpr_of_string) l in + <:expr< Tacexpr.TacAuto $n$ $l$ >> +(* + | Tacexpr.TacTrivial l -> + let l = mlexpr_of_option (mlexpr_of_list mlexpr_of_string) l in + <:expr< Tacexpr.TacTrivial $l$ >> +*) + +(* + | Tacexpr.TacExtend (s,l) -> + let l = mlexpr_of_list mlexpr_of_tactic_arg l in + let loc = MLast.loc_of_expr l in + <:expr< Tacexpr.TacExtend $mlexpr_of_string s$ $l$ >> +*) + | _ -> failwith "Quotation of atomic tactic expressions: TODO" + +and mlexpr_of_tactic = function + | Tacexpr.TacAtom (loc,t) -> + <:expr< Tacexpr.TacAtom loc $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 $int:string_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 -> let loc = dummy_loc in <:expr< Tacexpr.TacId >> + | Tacexpr.TacFail n -> + let loc = dummy_loc in <:expr< Tacexpr.TacFail $int:string_of_int n$ >> +(* + | 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 (l,t) -> + let f = + mlexpr_of_triple + (mlexpr_of_pair (fun _ -> <:expr< loc >>) mlexpr_of_ident) + (mlexpr_of_option (mlexpr_of_may_eval mlexpr_of_constr)) + 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 of t * (t * tactic_expr) list +*) + | Tacexpr.TacMatchContext (lr,l) -> + <:expr< Tacexpr.TacMatchContext + $mlexpr_of_bool lr$ + $mlexpr_of_list (mlexpr_of_match_rule mlexpr_of_tactic) l$>> +(* + | Tacexpr.TacFun of loc * tactic_fun_ast + | Tacexpr.TacFunRec of loc * identifier * tactic_fun_ast +*) +(* + | Tacexpr.TacArg (Tacexpr.AstTacArg (Coqast.Nmeta loc id)) -> anti loc id +*) + | Tacexpr.TacArg (Tacexpr.MetaIdArg (_,id)) -> anti loc id + | Tacexpr.TacArg t -> + <:expr< Tacexpr.TacArg $mlexpr_of_tactic_arg t$ >> + | _ -> failwith "Quotation of tactic expressions: TODO" + +and mlexpr_of_tactic_arg = function + | Tacexpr.MetaIdArg (loc,id) -> anti loc id + | Tacexpr.MetaNumArg (loc,n) -> + <:expr< Tacexpr.MetaNumArg loc $mlexpr_of_int n$ >> +(* + | Tacexpr.Identifier id -> + <:expr< Tacexpr.Identifier $mlexpr_of_ident id$ >> +*) +(* + | Tacexpr.AstTacArg t -> + <:expr< Tacexpr.AstTacArg $mlexpr_of_ast t$ >> +*) + | Tacexpr.TacCall (loc,t,tl) -> + <:expr< Tacexpr.TacCall loc $mlexpr_of_tactic_arg 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.Constr c -> + <:expr< Tacexpr.Constr $mlexpr_of_constr c$ >> +*) +(* + | Tacexpr.Qualid q -> + <:expr< Tacexpr.Qualid $mlexpr_of_qualid q$ >> +*) + | Tacexpr.Reference r -> + <:expr< Tacexpr.Reference $mlexpr_of_reference r$ >> +(* + | Tacexpr.TacArgGen q -> + <:expr< Tacexpr.TacArgGen $mlexpr_of_argtype q$ >> +*) + | _ -> failwith "mlexpr_of_tactic_arg: TODO" let f e = let ee s = - expr_of_ast (Pcoq.Gram.Entry.parse e + mlexpr_of_ast (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 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" (f Pcoq.Constr.constr_eoi); - Quotation.add "tactic" (f Pcoq.Tactic.tactic_eoi); - Quotation.add "vernac" (f Pcoq.Vernac_.vernac_eoi); + Quotation.add "constr" (fconstr Pcoq.Constr.constr_eoi); + Quotation.add "tactic" (ftac Pcoq.Tactic.tactic_eoi); +(* Quotation.add "vernac" (f Pcoq.Vernac_.vernac_eoi);*) Quotation.add "ast" (f Pcoq.Prim.ast_eoi); Quotation.default := "constr" - |