From 4af41a12a0e7e6b17d25a71568641bd03d5e1f94 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 14 Feb 2018 06:57:40 +0100 Subject: [located] More work towards using CAst.t We continue with the work of #402 and #6745 and update most of the remaining parts of the AST: - module declarations - intro patterns - top-level sentences Now, parsed documents should be full annotated by `CAst` nodes. --- plugins/ltac/tacintern.ml | 58 +++++++++++++++++++++++------------------------ 1 file changed, 29 insertions(+), 29 deletions(-) (limited to 'plugins/ltac/tacintern.ml') diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 121075f72..45f4a45fc 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -93,7 +93,7 @@ let intern_string_or_var = intern_or_var (fun (s : string) -> s) let intern_global_reference ist = function | Ident (loc,id) when find_var id ist -> - ArgVar CAst.(make ?loc id) + ArgVar (make ?loc id) | r -> let loc,_ as lqid = qualid_of_reference r in try ArgArg (loc,locate_global_with_alias lqid) @@ -103,20 +103,20 @@ let intern_ltac_variable ist = function | Ident (loc,id) -> if find_var id ist then (* A local variable of any type *) - ArgVar CAst.(make ?loc id) + ArgVar (make ?loc id) else raise Not_found | _ -> raise Not_found let intern_constr_reference strict ist = function | Ident (_,id) as r when not strict && find_hyp id ist -> - (DAst.make @@ GVar id), Some (CAst.make @@ CRef (r,None)) + (DAst.make @@ GVar id), Some (make @@ CRef (r,None)) | Ident (_,id) as r when find_var id ist -> - (DAst.make @@ GVar id), if strict then None else Some (CAst.make @@ CRef (r,None)) + (DAst.make @@ GVar id), if strict then None else Some (make @@ CRef (r,None)) | r -> let loc,_ as lqid = qualid_of_reference r in DAst.make @@ GRef (locate_global_with_alias lqid,None), - if strict then None else Some (CAst.make @@ CRef (r,None)) + if strict then None else Some (make @@ CRef (r,None)) (* Internalize an isolated reference in position of tactic *) @@ -168,7 +168,7 @@ let intern_non_tactic_reference strict ist r = (* By convention, use IntroIdentifier for unbound ident, when not in a def *) match r with | Ident (loc,id) when not strict -> - let ipat = in_gen (glbwit wit_intro_pattern) (loc, IntroNaming (IntroIdentifier id)) in + let ipat = in_gen (glbwit wit_intro_pattern) (make ?loc @@ IntroNaming (IntroIdentifier id)) in TacGeneric ipat | _ -> (* Reference not found *) @@ -209,8 +209,8 @@ let intern_constr = intern_constr_gen false false let intern_type = intern_constr_gen false true (* Globalize bindings *) -let intern_binding ist (loc,(b,c)) = - (loc,(intern_binding_name ist b,intern_constr ist c)) +let intern_binding ist = map (fun (b,c) -> + intern_binding_name ist b,intern_constr ist c) let intern_bindings ist = function | NoBindings -> NoBindings @@ -223,12 +223,12 @@ let intern_constr_with_bindings ist (c,bl) = let intern_constr_with_bindings_arg ist (clear,c) = (clear,intern_constr_with_bindings ist c) -let rec intern_intro_pattern lf ist = function - | loc, IntroNaming pat -> - loc, IntroNaming (intern_intro_pattern_naming lf ist pat) - | loc, IntroAction pat -> - loc, IntroAction (intern_intro_pattern_action lf ist pat) - | loc, IntroForthcoming _ as x -> x +let rec intern_intro_pattern lf ist = map (function + | IntroNaming pat -> + IntroNaming (intern_intro_pattern_naming lf ist pat) + | IntroAction pat -> + IntroAction (intern_intro_pattern_action lf ist pat) + | IntroForthcoming _ as x -> x) and intern_intro_pattern_naming lf ist = function | IntroIdentifier id -> @@ -239,12 +239,12 @@ and intern_intro_pattern_naming lf ist = function and intern_intro_pattern_action lf ist = function | IntroOrAndPattern l -> - IntroOrAndPattern (intern_or_and_intro_pattern lf ist l) + IntroOrAndPattern (intern_or_and_intro_pattern lf ist l) | IntroInjection l -> - IntroInjection (List.map (intern_intro_pattern lf ist) l) + IntroInjection (List.map (intern_intro_pattern lf ist) l) | IntroWildcard | IntroRewrite _ as x -> x - | IntroApplyOn ((loc,c),pat) -> - IntroApplyOn ((loc,intern_constr ist c), intern_intro_pattern lf ist pat) + | IntroApplyOn ({loc;v=c},pat) -> + IntroApplyOn (make ?loc @@ intern_constr ist c, intern_intro_pattern lf ist pat) and intern_or_and_intro_pattern lf ist = function | IntroAndPattern l -> @@ -256,10 +256,10 @@ let intern_or_and_intro_pattern_loc lf ist = function | ArgVar {v=id} as x -> if find_var id ist then x else user_err Pp.(str "Disjunctive/conjunctive introduction pattern expected.") - | ArgArg (loc,l) -> ArgArg (loc,intern_or_and_intro_pattern lf ist l) + | ArgArg ll -> ArgArg (map (fun l -> intern_or_and_intro_pattern lf ist l) ll) -let intern_intro_pattern_naming_loc lf ist (loc,pat) = - (loc,intern_intro_pattern_naming lf ist pat) +let intern_intro_pattern_naming_loc lf ist = map (fun pat -> + intern_intro_pattern_naming lf ist pat) (* TODO: catch ltac vars *) let intern_destruction_arg ist = function @@ -268,15 +268,15 @@ let intern_destruction_arg ist = function | clear,ElimOnIdent {loc;v=id} -> if !strict_check then (* If in a defined tactic, no intros-until *) - let c, p = intern_constr ist (CAst.make @@ CRef (Ident (Loc.tag id), None)) in + let c, p = intern_constr ist (make @@ CRef (Ident (Loc.tag id), None)) in match DAst.get c with - | GVar id -> clear,ElimOnIdent CAst.(make ?loc:c.loc id) + | GVar id -> clear,ElimOnIdent (make ?loc:c.loc id) | _ -> clear,ElimOnConstr ((c, p), NoBindings) else - clear,ElimOnIdent CAst.(make ?loc id) + clear,ElimOnIdent (make ?loc id) let short_name = function - | AN (Ident (loc,id)) when not !strict_check -> Some CAst.(make ?loc id) + | AN (Ident (loc,id)) when not !strict_check -> Some (make ?loc id) | _ -> None let intern_evaluable_global_reference ist r = @@ -289,16 +289,16 @@ let intern_evaluable_global_reference ist r = let intern_evaluable_reference_or_by_notation ist = function | AN r -> intern_evaluable_global_reference ist r - | ByNotation (loc,(ntn,sc)) -> + | ByNotation {loc;v=(ntn,sc)} -> evaluable_of_global_reference ist.genv (Notation.interp_notation_as_global_reference ?loc (function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc) (* Globalize a reduction expression *) let intern_evaluable ist = function - | AN (Ident (loc,id)) when find_var id ist -> ArgVar CAst.(make ?loc id) + | AN (Ident (loc,id)) when find_var id ist -> ArgVar (make ?loc id) | AN (Ident (loc,id)) when not !strict_check && find_hyp id ist -> - ArgArg (EvalVarRef id, Some CAst.(make ?loc id)) + ArgArg (EvalVarRef id, Some (make ?loc id)) | r -> let e = intern_evaluable_reference_or_by_notation ist r in let na = short_name r in @@ -817,7 +817,7 @@ let notation_subst bindings tac = let fold id c accu = let loc = Glob_ops.loc_of_glob_constr (fst c) in let c = ConstrMayEval (ConstrTerm c) in - (CAst.make ?loc @@ Name id, c) :: accu + (make ?loc @@ Name id, c) :: accu in let bindings = Id.Map.fold fold bindings [] in (** This is theoretically not correct due to potential variable capture, but -- cgit v1.2.3