diff options
Diffstat (limited to 'src/tac2quote.ml')
| -rw-r--r-- | src/tac2quote.ml | 129 |
1 files changed, 65 insertions, 64 deletions
diff --git a/src/tac2quote.ml b/src/tac2quote.ml index 829f13344c..e986bfc393 100644 --- a/src/tac2quote.ml +++ b/src/tac2quote.ml @@ -9,6 +9,7 @@ open Pp open Names open Util +open CAst open Tac2dyn open Tac2expr open Tac2qexpr @@ -38,12 +39,12 @@ let control_core n = kername control_prefix n let pattern_core n = kername pattern_prefix n let global_ref ?loc kn = - Loc.tag ?loc @@ CTacRef (AbsKn (TacConstant kn)) + CAst.make ?loc @@ CTacRef (AbsKn (TacConstant kn)) let constructor ?loc kn args = - let cst = Loc.tag ?loc @@ CTacCst (AbsKn (Other kn)) in + let cst = CAst.make ?loc @@ CTacCst (AbsKn (Other kn)) in if List.is_empty args then cst - else Loc.tag ?loc @@ CTacApp (cst, args) + else CAst.make ?loc @@ CTacApp (cst, args) let std_constructor ?loc name args = constructor ?loc (std_core name) args @@ -53,44 +54,44 @@ let std_proj ?loc name = let thunk e = let t_unit = coq_core "unit" in - let loc = Tac2intern.loc_of_tacexpr e in - let ty = Loc.tag ?loc @@ CTypRef (AbsKn (Other t_unit), []) in - let pat = Loc.tag ?loc @@ CPatVar (Anonymous) in - let pat = Loc.tag ?loc @@ CPatCnv (pat, ty) in - Loc.tag ?loc @@ CTacFun ([pat], e) + let loc = e.loc in + let ty = CAst.make?loc @@ CTypRef (AbsKn (Other t_unit), []) in + let pat = CAst.make ?loc @@ CPatVar (Anonymous) in + let pat = CAst.make ?loc @@ CPatCnv (pat, ty) in + CAst.make ?loc @@ CTacFun ([pat], e) -let of_pair f g (loc, (e1, e2)) = - Loc.tag ?loc @@ CTacApp (Loc.tag ?loc @@ CTacCst (AbsKn (Tuple 2)), [f e1; g e2]) +let of_pair f g {loc;v=(e1, e2)} = + CAst.make ?loc @@ CTacApp (CAst.make ?loc @@ CTacCst (AbsKn (Tuple 2)), [f e1; g e2]) let of_tuple ?loc el = match el with | [] -> - Loc.tag ?loc @@ CTacCst (AbsKn (Tuple 0)) + CAst.make ?loc @@ CTacCst (AbsKn (Tuple 0)) | [e] -> e | el -> let len = List.length el in - Loc.tag ?loc @@ CTacApp (Loc.tag ?loc @@ CTacCst (AbsKn (Tuple len)), el) + CAst.make ?loc @@ CTacApp (CAst.make ?loc @@ CTacCst (AbsKn (Tuple len)), el) -let of_int (loc, n) = - Loc.tag ?loc @@ CTacAtm (AtmInt n) +let of_int {loc;v=n} = + CAst.make ?loc @@ CTacAtm (AtmInt n) let of_option ?loc f opt = match opt with | None -> constructor ?loc (coq_core "None") [] | Some e -> constructor ?loc (coq_core "Some") [f e] let inj_wit ?loc wit x = - Loc.tag ?loc @@ CTacExt (wit, x) + CAst.make ?loc @@ CTacExt (wit, x) -let of_variable (loc, id) = +let of_variable {loc;v=id} = let qid = Libnames.qualid_of_ident id in if Tac2env.is_constructor qid then CErrors.user_err ?loc (str "Invalid identifier") - else Loc.tag ?loc @@ CTacRef (RelId (Loc.tag ?loc qid)) + else CAst.make ?loc @@ CTacRef (RelId (CAst.make ?loc qid)) let of_anti f = function | QExpr x -> f x | QAnti id -> of_variable id -let of_ident (loc, id) = inj_wit ?loc wit_ident id +let of_ident {loc;v=id} = inj_wit ?loc wit_ident id let of_constr c = let loc = Constrexpr_ops.constr_loc c in @@ -109,11 +110,11 @@ let rec of_list ?loc f = function | e :: l -> constructor ?loc (coq_core "::") [f e; of_list ?loc f l] -let of_qhyp (loc, h) = match h with +let of_qhyp {loc;v=h} = match h with | QAnonHyp n -> std_constructor ?loc "AnonHyp" [of_int n] | QNamedHyp id -> std_constructor ?loc "NamedHyp" [of_ident id] -let of_bindings (loc, b) = match b with +let of_bindings {loc;v=b} = match b with | QNoBindings -> std_constructor ?loc "NoBindings" [] | QImplicitBindings tl -> @@ -124,7 +125,7 @@ let of_bindings (loc, b) = match b with let of_constr_with_bindings c = of_pair of_open_constr of_bindings c -let rec of_intro_pattern (loc, pat) = match pat with +let rec of_intro_pattern {loc;v=pat} = match pat with | QIntroForthcoming b -> std_constructor ?loc "IntroForthcoming" [of_bool b] | QIntroNaming iname -> @@ -132,7 +133,7 @@ let rec of_intro_pattern (loc, pat) = match pat with | QIntroAction iact -> std_constructor ?loc "IntroAction" [of_intro_pattern_action iact] -and of_intro_pattern_naming (loc, pat) = match pat with +and of_intro_pattern_naming {loc;v=pat} = match pat with | QIntroIdentifier id -> std_constructor ?loc "IntroIdentifier" [of_anti of_ident id] | QIntroFresh id -> @@ -140,7 +141,7 @@ and of_intro_pattern_naming (loc, pat) = match pat with | QIntroAnonymous -> std_constructor ?loc "IntroAnonymous" [] -and of_intro_pattern_action (loc, pat) = match pat with +and of_intro_pattern_action {loc;v=pat} = match pat with | QIntroWildcard -> std_constructor ?loc "IntroWildcard" [] | QIntroOrAndPattern pat -> @@ -150,13 +151,13 @@ and of_intro_pattern_action (loc, pat) = match pat with | QIntroRewrite b -> std_constructor ?loc "IntroRewrite" [of_bool ?loc b] -and of_or_and_intro_pattern (loc, pat) = match pat with +and of_or_and_intro_pattern {loc;v=pat} = match pat with | QIntroOrPattern ill -> std_constructor ?loc "IntroOrPattern" [of_list ?loc of_intro_patterns ill] | QIntroAndPattern il -> std_constructor ?loc "IntroAndPattern" [of_intro_patterns il] -and of_intro_patterns (loc, l) = +and of_intro_patterns {loc;v=l} = of_list ?loc of_intro_pattern l let of_hyp_location_flag ?loc = function @@ -164,7 +165,7 @@ let of_hyp_location_flag ?loc = function | Locus.InHypTypeOnly -> std_constructor ?loc "InHypTypeOnly" [] | Locus.InHypValueOnly -> std_constructor ?loc "InHypValueOnly" [] -let of_occurrences (loc, occ) = match occ with +let of_occurrences {loc;v=occ} = match occ with | QAllOccurrences -> std_constructor ?loc "AllOccurrences" [] | QAllOccurrencesBut occs -> let map occ = of_anti of_int occ in @@ -183,27 +184,27 @@ let of_hyp_location ?loc ((occs, id), flag) = of_hyp_location_flag ?loc flag; ] -let of_clause (loc, cl) = +let of_clause {loc;v=cl} = let hyps = of_option ?loc (fun l -> of_list ?loc of_hyp_location l) cl.q_onhyps in let concl = of_occurrences cl.q_concl_occs in - Loc.tag ?loc @@ CTacRec ([ + CAst.make ?loc @@ CTacRec ([ std_proj "on_hyps", hyps; std_proj "on_concl", concl; ]) -let of_destruction_arg (loc, arg) = match arg with +let of_destruction_arg {loc;v=arg} = match arg with | QElimOnConstr c -> let arg = thunk (of_constr_with_bindings c) in std_constructor ?loc "ElimOnConstr" [arg] | QElimOnIdent id -> std_constructor ?loc "ElimOnIdent" [of_ident id] | QElimOnAnonHyp n -> std_constructor ?loc "ElimOnAnonHyp" [of_int n] -let of_induction_clause (loc, cl) = +let of_induction_clause {loc;v=cl} = let arg = of_destruction_arg cl.indcl_arg in let eqn = of_option ?loc of_intro_pattern_naming cl.indcl_eqn in let as_ = of_option ?loc of_or_and_intro_pattern cl.indcl_as in let in_ = of_option ?loc of_clause cl.indcl_in in - Loc.tag ?loc @@ CTacRec ([ + CAst.make ?loc @@ CTacRec ([ std_proj "indcl_arg", arg; std_proj "indcl_eqn", eqn; std_proj "indcl_as", as_; @@ -238,24 +239,24 @@ let abstract_vars loc vars tac = | Anonymous -> (n + 1, accu) | Name _ -> let get = global_ref ?loc (kername array_prefix "get") in - let args = [of_variable (loc, id0); of_int (loc, n)] in - let e = Loc.tag ?loc @@ CTacApp (get, args) in - let accu = (Loc.tag ?loc @@ CPatVar na, e) :: accu in + let args = [of_variable CAst.(make ?loc id0); of_int CAst.(make ?loc n)] in + let e = CAst.make ?loc @@ CTacApp (get, args) in + let accu = (CAst.make ?loc @@ CPatVar na, e) :: accu in (n + 1, accu) in let (_, bnd) = List.fold_left build_bindings (0, []) vars in - let tac = Loc.tag ?loc @@ CTacLet (false, bnd, tac) in + let tac = CAst.make ?loc @@ CTacLet (false, bnd, tac) in (Name id0, tac) in - Loc.tag ?loc @@ CTacFun ([Loc.tag ?loc @@ CPatVar na], tac) + CAst.make ?loc @@ CTacFun ([CAst.make ?loc @@ CPatVar na], tac) let of_pattern p = inj_wit ?loc:p.CAst.loc wit_pattern p -let of_conversion (loc, c) = match c with +let of_conversion {loc;v=c} = match c with | QConvert c -> let pat = of_option ?loc of_pattern None in - let c = Loc.tag ?loc @@ CTacFun ([Loc.tag ?loc @@ CPatVar Anonymous], of_constr c) in + let c = CAst.make ?loc @@ CTacFun ([CAst.make ?loc @@ CPatVar Anonymous], of_constr c) in of_tuple ?loc [pat; c] | QConvertWith (pat, c) -> let vars = pattern_vars pat in @@ -266,7 +267,7 @@ let of_conversion (loc, c) = match c with let c = abstract_vars loc vars c in of_tuple [pat; c] -let of_repeat (loc, r) = match r with +let of_repeat {loc;v=r} = match r with | QPrecisely n -> std_constructor ?loc "Precisely" [of_int n] | QUpTo n -> std_constructor ?loc "UpTo" [of_int n] | QRepeatStar -> std_constructor ?loc "RepeatStar" [] @@ -276,14 +277,14 @@ let of_orient loc b = if b then std_constructor ?loc "LTR" [] else std_constructor ?loc "RTL" [] -let of_rewriting (loc, rew) = +let of_rewriting {loc;v=rew} = let orient = - let (loc, orient) = rew.rew_orient in + let {loc;v=orient} = rew.rew_orient in of_option ?loc (fun b -> of_orient loc b) orient in let repeat = of_repeat rew.rew_repeat in let equatn = thunk (of_constr_with_bindings rew.rew_equatn) in - Loc.tag ?loc @@ CTacRec ([ + CAst.make ?loc @@ CTacRec ([ std_proj "rew_orient", orient; std_proj "rew_repeat", repeat; std_proj "rew_equatn", equatn; @@ -291,42 +292,42 @@ let of_rewriting (loc, rew) = let of_hyp ?loc id = let hyp = global_ref ?loc (control_core "hyp") in - Loc.tag ?loc @@ CTacApp (hyp, [of_ident id]) + CAst.make ?loc @@ CTacApp (hyp, [of_ident id]) let of_exact_hyp ?loc id = let refine = global_ref ?loc (control_core "refine") in - Loc.tag ?loc @@ CTacApp (refine, [thunk (of_hyp ?loc id)]) + CAst.make ?loc @@ CTacApp (refine, [thunk (of_hyp ?loc id)]) let of_exact_var ?loc id = let refine = global_ref ?loc (control_core "refine") in - Loc.tag ?loc @@ CTacApp (refine, [thunk (of_variable id)]) + CAst.make ?loc @@ CTacApp (refine, [thunk (of_variable id)]) let of_dispatch tacs = - let (loc, _) = tacs in + let loc = tacs.loc in let default = function | Some e -> thunk e - | None -> thunk (Loc.tag ?loc @@ CTacCst (AbsKn (Tuple 0))) + | None -> thunk (CAst.make ?loc @@ CTacCst (AbsKn (Tuple 0))) in - let map e = of_pair default (fun l -> of_list ?loc default l) (Loc.tag ?loc e) in + let map e = of_pair default (fun l -> of_list ?loc default l) (CAst.make ?loc e) in of_pair (fun l -> of_list ?loc default l) (fun r -> of_option ?loc map r) tacs let make_red_flag l = let open Genredexpr in let rec add_flag red = function | [] -> red - | (_, flag) :: lf -> + | {v=flag} :: lf -> let red = match flag with | QBeta -> { red with rBeta = true } | QMatch -> { red with rMatch = true } | QFix -> { red with rFix = true } | QCofix -> { red with rCofix = true } | QZeta -> { red with rZeta = true } - | QConst (loc, l) -> + | QConst {loc;v=l} -> if red.rDelta then CErrors.user_err ?loc Pp.(str "Cannot set both constants to unfold and constants not to unfold"); { red with rConst = red.rConst @ l } - | QDeltaBut (loc, l) -> + | QDeltaBut {loc;v=l} -> if red.rConst <> [] && not red.rDelta then CErrors.user_err ?loc Pp.(str "Cannot set both constants to unfold and constants not to unfold"); @@ -348,10 +349,10 @@ let of_reference r = in of_anti of_ref r -let of_strategy_flag (loc, flag) = +let of_strategy_flag {loc;v=flag} = let open Genredexpr in let flag = make_red_flag flag in - Loc.tag ?loc @@ CTacRec ([ + CAst.make ?loc @@ CTacRec ([ std_proj "rBeta", of_bool ?loc flag.rBeta; std_proj "rMatch", of_bool ?loc flag.rMatch; std_proj "rFix", of_bool ?loc flag.rFix; @@ -361,7 +362,7 @@ let of_strategy_flag (loc, flag) = std_proj "rConst", of_list ?loc of_reference flag.rConst; ]) -let of_hintdb (loc, hdb) = match hdb with +let of_hintdb {loc;v=hdb} = match hdb with | QHintAll -> of_option ?loc (fun l -> of_list (fun id -> of_anti of_ident id) l) None | QHintDbs ids -> of_option ?loc (fun l -> of_list (fun id -> of_anti of_ident id) l) (Some ids) @@ -375,8 +376,8 @@ let extract_name ?loc oid = match oid with [(match_kind * pattern * (context -> constr array -> 'a))] where the function binds the names from the pattern to the contents of the constr array. *) -let of_constr_matching (loc, m) = - let map (loc, ((ploc, pat), tac)) = +let of_constr_matching {loc;v=m} = + let map {loc;v=({loc=ploc;v=pat}, tac)} = let (knd, pat, na) = match pat with | QConstrMatchPattern pat -> let knd = constructor ?loc (pattern_core "MatchPattern") [] in @@ -391,7 +392,7 @@ let of_constr_matching (loc, m) = let vars = Id.Set.elements vars in let vars = List.map (fun id -> Name id) vars in let e = abstract_vars loc vars tac in - let e = Loc.tag ?loc @@ CTacFun ([Loc.tag ?loc @@ CPatVar na], e) in + let e = CAst.make ?loc @@ CTacFun ([CAst.make ?loc @@ CPatVar na], e) in let pat = inj_wit ?loc:ploc wit_pattern pat in of_tuple [knd; pat; e] in @@ -401,8 +402,8 @@ let of_constr_matching (loc, m) = - a goal pattern: (constr_match list * constr_match) - a branch function (ident array -> context array -> constr array -> context -> 'a) *) -let of_goal_matching (loc, gm) = - let mk_pat (loc, p) = match p with +let of_goal_matching {loc;v=gm} = + let mk_pat {loc;v=p} = match p with | QConstrMatchPattern pat -> let knd = constructor ?loc (pattern_core "MatchPattern") [] in (Anonymous, pat, knd) @@ -411,7 +412,7 @@ let of_goal_matching (loc, gm) = let knd = constructor ?loc (pattern_core "MatchContext") [] in (na, pat, knd) in - let mk_gpat (loc, p) = + let mk_gpat {loc;v=p} = let concl_pat = p.q_goal_match_concl in let hyps_pats = p.q_goal_match_hyps in let (concl_ctx, concl_pat, concl_knd) = mk_pat concl_pat in @@ -433,9 +434,9 @@ let of_goal_matching (loc, gm) = let subst = List.map (fun id -> Name id) vars in (r, hyps, hctx, subst, concl_ctx) in - let map (loc, (pat, tac)) = + let map {loc;v=(pat, tac)} = let (pat, hyps, hctx, subst, cctx) = mk_gpat pat in - let tac = Loc.tag ?loc @@ CTacFun ([Loc.tag ?loc @@ CPatVar cctx], tac) in + let tac = CAst.make ?loc @@ CTacFun ([CAst.make ?loc @@ CPatVar cctx], tac) in let tac = abstract_vars loc subst tac in let tac = abstract_vars loc hctx tac in let tac = abstract_vars loc hyps tac in @@ -443,7 +444,7 @@ let of_goal_matching (loc, gm) = in of_list ?loc map gm -let of_move_location (loc, mv) = match mv with +let of_move_location {loc;v=mv} = match mv with | QMoveAfter id -> std_constructor ?loc "MoveAfter" [of_anti of_ident id] | QMoveBefore id -> std_constructor ?loc "MoveBefore" [of_anti of_ident id] | QMoveFirst -> std_constructor ?loc "MoveFirst" [] @@ -452,7 +453,7 @@ let of_move_location (loc, mv) = match mv with let of_pose p = of_pair (fun id -> of_option (fun id -> of_anti of_ident id) id) of_open_constr p -let of_assertion (loc, ast) = match ast with +let of_assertion {loc;v=ast} = match ast with | QAssertType (ipat, c, tac) -> let ipat = of_option of_intro_pattern ipat in let c = of_constr c in |