From 9bebbb96e58b3c1b0f7f88ba2af45462eae69b0f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 10 Dec 2017 09:26:25 +0100 Subject: [ast] Improve precision of Ast location recognition in serialization. We follow the suggestions in #402 and turn uses of `Loc.located` in `vernac` into `CAst.t`. The impact should be low as this change mostly affects top-level vernaculars. With this change, we are even closer to automatically map a text document to its AST in a programmatic way. --- stm/stm.ml | 12 ++++++------ stm/vernac_classifier.ml | 44 +++++++++++++++++++++++--------------------- 2 files changed, 29 insertions(+), 27 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 92587b8ea..e7c371798 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -565,8 +565,8 @@ end = struct (* {{{ *) let reachable id = reachable !vcs id let mk_branch_name { expr = x } = Branch.make (match Vernacprop.under_control x with - | VernacDefinition (_,((_, Name i),_),_) -> Id.to_string i - | VernacStartTheoremProof (_,[((_,i),_),_]) -> Id.to_string i + | VernacDefinition (_,({CAst.v=Name i},_),_) -> Id.to_string i + | VernacStartTheoremProof (_,[({CAst.v=i},_),_]) -> Id.to_string i | _ -> "branch") let edit_branch = Branch.make "edit" let branch ?root ?pos name kind = vcs := branch !vcs ?root ?pos name kind @@ -1174,7 +1174,7 @@ end = struct (* {{{ *) match Vernacprop.under_control v with | VernacResetInitial -> Stateid.initial, VtNow - | VernacResetName (_,name) -> + | VernacResetName {CAst.v=name} -> let id = VCS.get_branch_pos (VCS.current_branch ()) in (try let oid = @@ -1236,7 +1236,7 @@ let set_compilation_hints file = let get_hint_ctx loc = let s = Aux_file.get ?loc !hints "context_used" in let ids = List.map Names.Id.of_string (Str.split (Str.regexp " ") s) in - let ids = List.map (fun id -> Loc.tag id) ids in + let ids = List.map (fun id -> CAst.make id) ids in match ids with | [] -> SsEmpty | x :: xs -> @@ -1956,8 +1956,8 @@ end = struct (* {{{ *) = let e, time, batch, fail = let rec find ~time ~batch ~fail = function - | VernacTime (batch,(_,e)) -> find ~time:true ~batch ~fail e - | VernacRedirect (_,(_,e)) -> find ~time ~batch ~fail e + | VernacTime (batch,{CAst.v=e}) -> find ~time:true ~batch ~fail e + | VernacRedirect (_,{CAst.v=e}) -> find ~time ~batch ~fail e | VernacFail e -> find ~time ~batch ~fail:true e | e -> e, time, batch, fail in find ~time:false ~batch:false ~fail:false e in diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index cbbb54e45..93d58b2a9 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -6,10 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Vernacexpr open CErrors open Util open Pp +open CAst +open Vernacexpr let default_proof_mode () = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"] @@ -87,13 +88,14 @@ let classify_vernac e = | VernacUnsetOption (["Default";"Proof";"Using"]) | VernacSetOption (["Default";"Proof";"Using"],_) -> VtSideff [], VtNow (* StartProof *) - | VernacDefinition ((Decl_kinds.DoDischarge,_),((_,i),_),ProveBody _) -> - VtStartProof(default_proof_mode (),Doesn'tGuaranteeOpacity, idents_of_name i), VtLater - | VernacDefinition (_,((_,i),_),ProveBody _) -> + | VernacDefinition ((Decl_kinds.DoDischarge,_),({v=i},_),ProveBody _) -> + VtStartProof(default_proof_mode (),Doesn'tGuaranteeOpacity, idents_of_name i), VtLater + + | VernacDefinition (_,({v=i},_),ProveBody _) -> let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in VtStartProof(default_proof_mode (),guarantee, idents_of_name i), VtLater | VernacStartTheoremProof (_,l) -> - let ids = List.map (fun (((_, i), _), _) -> i) l in + let ids = List.map (fun (({v=i}, _), _) -> i) l in let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in VtStartProof (default_proof_mode (),guarantee,ids), VtLater | VernacFixpoint (discharge,l) -> @@ -102,7 +104,7 @@ let classify_vernac e = else GuaranteesOpacity in let ids, open_proof = - List.fold_left (fun (l,b) ((((_,id),_),_,_,_,p),_) -> + List.fold_left (fun (l,b) ((({v=id},_),_,_,_,p),_) -> id::l, b || p = None) ([],false) l in if open_proof then VtStartProof (default_proof_mode (),guarantee,ids), VtLater @@ -113,29 +115,29 @@ let classify_vernac e = else GuaranteesOpacity in let ids, open_proof = - List.fold_left (fun (l,b) ((((_,id),_),_,_,p),_) -> + List.fold_left (fun (l,b) ((({v=id},_),_,_,p),_) -> id::l, b || p = None) ([],false) l in if open_proof then VtStartProof (default_proof_mode (),guarantee,ids), VtLater else VtSideff ids, VtLater (* Sideff: apply to all open branches. usually run on master only *) | VernacAssumption (_,_,l) -> - let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map (fun (id, _) -> snd id) l) l) in - VtSideff ids, VtLater - | VernacDefinition (_,((_,id),_),DefineBody _) -> VtSideff (idents_of_name id), VtLater + let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map (fun (id, _) -> id.v) l) l) in + VtSideff ids, VtLater + | VernacDefinition (_,({v=id},_),DefineBody _) -> VtSideff (idents_of_name id), VtLater | VernacInductive (_, _,_,l) -> - let ids = List.map (fun (((_,((_,id),_)),_,_,_,cl),_) -> id :: match cl with - | Constructors l -> List.map (fun (_,((_,id),_)) -> id) l - | RecordDecl (oid,l) -> (match oid with Some (_,x) -> [x] | _ -> []) @ + let ids = List.map (fun (((_,({v=id},_)),_,_,_,cl),_) -> id :: match cl with + | Constructors l -> List.map (fun (_,({v=id},_)) -> id) l + | RecordDecl (oid,l) -> (match oid with Some {v=x} -> [x] | _ -> []) @ CList.map_filter (function - | ((_,AssumExpr((_,Names.Name n),_)),_),_ -> Some n + | ((_,AssumExpr({v=Names.Name n},_)),_),_ -> Some n | _ -> None) l) l in VtSideff (List.flatten ids), VtLater | VernacScheme l -> - let ids = List.map snd (CList.map_filter (fun (x,_) -> x) l) in + let ids = List.map (fun {v}->v) (CList.map_filter (fun (x,_) -> x) l) in VtSideff ids, VtLater - | VernacCombinedScheme ((_,id),_) -> VtSideff [id], VtLater - | VernacBeginSection (_,id) -> VtSideff [id], VtLater + | VernacCombinedScheme ({v=id},_) -> VtSideff [id], VtLater + | VernacBeginSection {v=id} -> VtSideff [id], VtLater | VernacUniverse _ | VernacConstraint _ | VernacCanonical _ | VernacCoercion _ | VernacIdentityCoercion _ | VernacAddLoadPath _ | VernacRemoveLoadPath _ | VernacAddMLPath _ @@ -159,10 +161,10 @@ let classify_vernac e = (* (Local) Notations have to disappear *) | VernacEndSegment _ -> VtSideff [], VtNow (* Modules with parameters have to be executed: can import notations *) - | VernacDeclareModule (exp,(_,id),bl,_) - | VernacDefineModule (exp,(_,id),bl,_,_) -> + | VernacDeclareModule (exp,{v=id},bl,_) + | VernacDefineModule (exp,{v=id},bl,_,_) -> VtSideff [id], if bl = [] && exp = None then VtLater else VtNow - | VernacDeclareModuleType ((_,id),bl,_,_) -> + | VernacDeclareModuleType ({v=id},bl,_,_) -> VtSideff [id], if bl = [] then VtLater else VtNow (* These commands alter the parser *) | VernacOpenCloseScope _ | VernacDelimiters _ | VernacBindScope _ @@ -198,7 +200,7 @@ let classify_vernac e = ) poly f in static_classifier ~poly e | VernacTimeout (_,e) -> static_control_classifier ~poly e - | VernacTime (_,(_,e)) | VernacRedirect (_, (_,e)) -> + | VernacTime (_,{v=e}) | VernacRedirect (_, {v=e}) -> static_control_classifier ~poly e | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *) (match static_control_classifier ~poly e with -- cgit v1.2.3