From 054d2736c1c1b55cb7708ff0444af521cd0fe2ba Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 8 Apr 2017 23:19:35 +0200 Subject: [location] [ast] Switch Constrexpr AST to an extensible node type. Following @gasche idea, and the original intention of #402, we switch the main parsing AST of Coq from `'a Loc.located` to `'a CAst.ast` which is private and record-based. This provides significantly clearer code for the AST, and is robust wrt attributes. --- interp/constrextern.ml | 87 ++++++++++++++++++++++++++------------------------ 1 file changed, 46 insertions(+), 41 deletions(-) (limited to 'interp/constrextern.ml') diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 30b81ecc4..e8a5b5265 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -144,15 +144,15 @@ module PrintingConstructor = Goptions.MakeRefTable(PrintingRecordConstructor) let insert_delimiters e = function | None -> e - | Some sc -> Loc.tag @@ CDelimiters (sc,e) + | Some sc -> CAst.make @@ CDelimiters (sc,e) let insert_pat_delimiters ?loc p = function | None -> p - | Some sc -> Loc.tag ?loc @@ CPatDelimiters (sc,p) + | Some sc -> CAst.make ?loc @@ CPatDelimiters (sc,p) let insert_pat_alias ?loc p = function | Anonymous -> p - | Name id -> Loc.tag ?loc @@ CPatAlias (p,id) + | Name id -> CAst.make ?loc @@ CPatAlias (p,id) (**********************************************************************) (* conversion of references *) @@ -178,7 +178,7 @@ let extern_reference ?loc vars l = !my_extern_reference ?loc vars l let add_patt_for_params ind l = if !Flags.in_debugger then l else - Util.List.addn (Inductiveops.inductive_nparamdecls ind) (Loc.tag @@ CPatAtom None) l + Util.List.addn (Inductiveops.inductive_nparamdecls ind) (CAst.make @@ CPatAtom None) l let add_cpatt_for_params ind l = if !Flags.in_debugger then l else @@ -190,7 +190,7 @@ let drop_implicits_in_patt cst nb_expl args = let rec impls_fit l = function |[],t -> Some (List.rev_append l t) |_,[] -> None - |h::t,(_loc, CPatAtom None)::tt when is_status_implicit h -> impls_fit l (t,tt) + |h::t, { CAst.v = CPatAtom None }::tt when is_status_implicit h -> impls_fit l (t,tt) |h::_,_ when is_status_implicit h -> None |_::t,hh::tt -> impls_fit (hh::l) (t,tt) in let rec aux = function @@ -236,8 +236,8 @@ let expand_curly_brackets loc mknot ntn l = (* side effect *) mknot (loc,!ntn',l) -let destPrim = function _loc, CPrim t -> Some t | _ -> None -let destPatPrim = function _loc, CPatPrim t -> Some t | _ -> None +let destPrim = function { CAst.v = CPrim t } -> Some t | _ -> None +let destPatPrim = function { CAst.v = CPatPrim t } -> Some t | _ -> None let make_notation_gen loc ntn mknot mkprim destprim l = if has_curly_brackets ntn @@ -259,21 +259,21 @@ let make_notation_gen loc ntn mknot mkprim destprim l = let make_notation loc ntn (terms,termlists,binders as subst) = if not (List.is_empty termlists) || not (List.is_empty binders) then - Loc.tag ?loc @@ CNotation (ntn,subst) + CAst.make ?loc @@ CNotation (ntn,subst) else make_notation_gen loc ntn - (fun (loc,ntn,l) -> Loc.tag ?loc @@ CNotation (ntn,(l,[],[]))) - (fun (loc,p) -> Loc.tag ?loc @@ CPrim p) + (fun (loc,ntn,l) -> CAst.make ?loc @@ CNotation (ntn,(l,[],[]))) + (fun (loc,p) -> CAst.make ?loc @@ CPrim p) destPrim terms let make_pat_notation ?loc ntn (terms,termlists as subst) args = - if not (List.is_empty termlists) then (Loc.tag ?loc @@ CPatNotation (ntn,subst,args)) else + if not (List.is_empty termlists) then (CAst.make ?loc @@ CPatNotation (ntn,subst,args)) else make_notation_gen loc ntn - (fun (loc,ntn,l) -> Loc.tag ?loc @@ CPatNotation (ntn,(l,[]),args)) - (fun (loc,p) -> Loc.tag ?loc @@ CPatPrim p) + (fun (loc,ntn,l) -> CAst.make ?loc @@ CPatNotation (ntn,(l,[]),args)) + (fun (loc,p) -> CAst.make ?loc @@ CPatPrim p) destPatPrim terms -let mkPat ?loc qid l = Loc.tag ?loc @@ +let mkPat ?loc qid l = CAst.make ?loc @@ (* Normally irrelevant test with v8 syntax, but let's do it anyway *) if List.is_empty l then CPatAtom (Some qid) else CPatCstr (qid,None,l) @@ -295,7 +295,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = when !Flags.in_debugger||Inductiveops.constructor_has_local_defs cstrsp -> let c = extern_reference ?loc Id.Set.empty (ConstructRef cstrsp) in let args = List.map (extern_cases_pattern_in_scope scopes vars) args in - Loc.tag ?loc @@ CPatCstr (c, Some (add_patt_for_params (fst cstrsp) args), []) + CAst.make ?loc @@ CPatCstr (c, Some (add_patt_for_params (fst cstrsp) args), []) | _ -> try if !Flags.raw_print || !print_no_symbol then raise No_match; @@ -304,7 +304,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = | None -> raise No_match | Some key -> let loc = cases_pattern_loc pat in - insert_pat_alias ?loc (insert_pat_delimiters ?loc (Loc.tag ?loc @@ CPatPrim p) key) na + insert_pat_alias ?loc (insert_pat_delimiters ?loc (CAst.make ?loc @@ CPatPrim p) key) na with No_match -> try if !Flags.raw_print || !print_no_symbol then raise No_match; @@ -312,8 +312,8 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = (uninterp_cases_pattern_notations pat) with No_match -> match pat with - | loc, PatVar (Name id) -> Loc.tag ?loc @@ CPatAtom (Some (Ident (loc,id))) - | loc, PatVar (Anonymous) -> Loc.tag ?loc @@ CPatAtom None + | loc, PatVar (Name id) -> CAst.make ?loc @@ CPatAtom (Some (Ident (loc,id))) + | loc, PatVar (Anonymous) -> CAst.make ?loc @@ CPatAtom None | loc, PatCstr(cstrsp,args,na) -> let args = List.map (extern_cases_pattern_in_scope scopes vars) args in let p = @@ -327,24 +327,29 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = | Some c :: q -> match args with | [] -> raise No_match - | (_loc, CPatAtom(None)) :: tail -> ip q tail acc + + + + + + | { CAst.v = CPatAtom None } :: tail -> ip q tail acc (* we don't want to have 'x = _' in our patterns *) | head :: tail -> ip q tail ((extern_reference ?loc Id.Set.empty (ConstRef c), head) :: acc) in - Loc.tag ?loc @@ CPatRecord(List.rev (ip projs args [])) + CAst.make ?loc @@ CPatRecord(List.rev (ip projs args [])) with Not_found | No_match | Exit -> let c = extern_reference ?loc Id.Set.empty (ConstructRef cstrsp) in if !Topconstr.asymmetric_patterns then if pattern_printable_in_both_syntax cstrsp - then Loc.tag ?loc @@ CPatCstr (c, None, args) - else Loc.tag ?loc @@ CPatCstr (c, Some (add_patt_for_params (fst cstrsp) args), []) + then CAst.make ?loc @@ CPatCstr (c, None, args) + else CAst.make ?loc @@ CPatCstr (c, Some (add_patt_for_params (fst cstrsp) args), []) else let full_args = add_patt_for_params (fst cstrsp) args in match drop_implicits_in_patt (ConstructRef cstrsp) 0 full_args with - | Some true_args -> Loc.tag ?loc @@ CPatCstr (c, None, true_args) - | None -> Loc.tag ?loc @@ CPatCstr (c, Some full_args, []) + | Some true_args -> CAst.make ?loc @@ CPatCstr (c, None, true_args) + | None -> CAst.make ?loc @@ CPatCstr (c, Some full_args, []) in insert_pat_alias ?loc p na and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) (tmp_scope, scopes as allscopes) vars = @@ -401,8 +406,8 @@ and extern_notation_pattern (tmp_scope,scopes as allscopes) vars (loc, t) = func let p = apply_notation_to_pattern ?loc (ConstructRef cstr) (match_notation_constr_cases_pattern (loc, t) pat) allscopes vars keyrule in insert_pat_alias ?loc p na - | PatVar Anonymous -> Loc.tag ?loc @@ CPatAtom None - | PatVar (Name id) -> Loc.tag ?loc @@ CPatAtom (Some (Ident (loc,id))) + | PatVar Anonymous -> CAst.make ?loc @@ CPatAtom None + | PatVar (Name id) -> CAst.make ?loc @@ CPatAtom (Some (Ident (loc,id))) with No_match -> extern_notation_pattern allscopes vars (loc, t) rules @@ -422,7 +427,7 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args = if !Flags.in_debugger||Inductiveops.inductive_has_local_defs ind then let c = extern_reference vars (IndRef ind) in let args = List.map (extern_cases_pattern_in_scope scopes vars) args in - Loc.tag @@ CPatCstr (c, Some (add_patt_for_params ind args), []) + CAst.make @@ CPatCstr (c, Some (add_patt_for_params ind args), []) else try if !Flags.raw_print || !print_no_symbol then raise No_match; @@ -430,7 +435,7 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args = match availability_of_prim_token p sc scopes with | None -> raise No_match | Some key -> - insert_pat_delimiters (Loc.tag @@ CPatPrim p) key + insert_pat_delimiters (CAst.make @@ CPatPrim p) key with No_match -> try if !Flags.raw_print || !print_no_symbol then raise No_match; @@ -440,8 +445,8 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args = let c = extern_reference vars (IndRef ind) in let args = List.map (extern_cases_pattern_in_scope scopes vars) args in match drop_implicits_in_patt (IndRef ind) 0 args with - |Some true_args -> Loc.tag @@ CPatCstr (c, None, true_args) - |None -> Loc.tag @@ CPatCstr (c, Some args, []) + |Some true_args -> CAst.make @@ CPatCstr (c, None, true_args) + |None -> CAst.make @@ CPatCstr (c, Some args, []) let extern_cases_pattern vars p = extern_cases_pattern_in_scope (None,[]) vars p @@ -466,7 +471,7 @@ let is_projection nargs = function let is_hole = function CHole _ | CEvar _ -> true | _ -> false let is_significant_implicit a = - not (is_hole (snd a)) + not (is_hole (a.CAst.v)) let is_needed_for_correct_partial_application tail imp = List.is_empty tail && not (maximal_insertion_of imp) @@ -515,11 +520,11 @@ let explicitize inctx impl (cf,f) args = CApp ((ip,f),args1@args2) | None -> let args = exprec 1 (args,impl) in - if List.is_empty args then snd f else CApp ((None, f), args) + if List.is_empty args then f.CAst.v else CApp ((None, f), args) in try expl () with Expl -> - let f',us = match f with (_loc, CRef (f,us)) -> f,us | _ -> assert false in + let f',us = match f with { CAst.v = CRef (f,us) } -> f,us | _ -> assert false in let ip = if !print_projections then ip else None in CAppExpl ((ip, f', us), List.map Lazy.force args) @@ -546,7 +551,7 @@ let extern_app inctx impl (cf,f) us args = let args = List.map Lazy.force args in CAppExpl ((is_projection (List.length args) cf,f,us), args) else - explicitize inctx impl (cf, Loc.tag @@ CRef (f,us)) args + explicitize inctx impl (cf, CAst.make @@ CRef (f,us)) args let rec fill_arg_scopes args subscopes scopes = match args, subscopes with | [], _ -> [] @@ -600,7 +605,7 @@ let extern_possible_prim_token scopes r = let (sc,n) = uninterp_prim_token r in match availability_of_prim_token n sc scopes with | None -> None - | Some key -> Some (insert_delimiters (Loc.tag ?loc:(loc_of_glob_constr r) @@ CPrim n) key) + | Some key -> Some (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key) with No_match -> None @@ -608,7 +613,7 @@ let extern_optimal_prim_token scopes r r' = let c = extern_possible_prim_token scopes r in let c' = if r==r' then None else extern_possible_prim_token scopes r' in match c,c' with - | Some n, (Some ((_, CDelimiters _)) | None) | _, Some n -> n + | Some n, (Some ({ CAst.v = CDelimiters _}) | None) | _, Some n -> n | _ -> raise No_match (**********************************************************************) @@ -644,7 +649,7 @@ let rec extern inctx scopes vars r = let r'' = flatten_application r' in if !Flags.raw_print || !print_no_symbol then raise No_match; extern_notation scopes vars r'' (uninterp_notations r'') - with No_match -> Loc.map_with_loc (fun ?loc -> function + with No_match -> CAst.map_from_loc (fun ?loc -> function | GRef (ref,us) -> extern_global (select_stronger_impargs (implicits_of_global ref)) (extern_reference ?loc vars ref) (extern_universes us) @@ -824,7 +829,7 @@ and sub_extern inctx (_,scopes) = extern inctx (None,scopes) and factorize_prod scopes vars na bk aty c = let c = extern_typ scopes vars c in match na, c with - | Name id, (loc, CProdN ([nal,Default bk',ty],c)) + | Name id, { CAst.loc ; v = CProdN ([nal,Default bk',ty],c) } when binding_kind_eq bk bk' && constr_expr_eq aty ty && not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *) -> nal,c @@ -834,7 +839,7 @@ and factorize_prod scopes vars na bk aty c = and factorize_lambda inctx scopes vars na bk aty c = let c = sub_extern inctx scopes vars c in match c with - | loc, CLambdaN ([nal,Default bk',ty],c) + | { CAst.loc; v = CLambdaN ([nal,Default bk',ty],c) } when binding_kind_eq bk bk' && constr_expr_eq aty ty && not (occur_name na ty) (* avoid na in ty escapes scope *) -> nal,c @@ -943,12 +948,12 @@ and extern_notation (tmp_scope,scopes as allscopes) vars t = function extern true (scopt,scl@scopes) vars c, None) terms in let a = CRef (Qualid (loc, shortest_qualid_of_syndef vars kn),None) in - Loc.tag ?loc @@ if List.is_empty l then a else CApp ((None, Loc.tag a),l) in + CAst.make ?loc @@ if List.is_empty l then a else CApp ((None, CAst.make a),l) in if List.is_empty args then e else let args = fill_arg_scopes args argsscopes scopes in let args = extern_args (extern true) vars args in - Loc.tag ?loc @@ explicitize false argsimpls (None,e) args + CAst.make ?loc @@ explicitize false argsimpls (None,e) args with No_match -> extern_notation allscopes vars t rules -- cgit v1.2.3