diff options
Diffstat (limited to 'stm/vernac_classifier.ml')
| -rw-r--r-- | stm/vernac_classifier.ml | 197 |
1 files changed, 90 insertions, 107 deletions
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index dc5be08a..f68c8b32 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -1,16 +1,20 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Vernacexpr open CErrors +open Util open Pp +open CAst +open Vernacexpr -let default_proof_mode () = Proof_global.get_default_proof_mode_name () +let default_proof_mode () = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"] let string_of_in_script b = if b then " (inside script)" else "" @@ -30,13 +34,8 @@ let string_of_vernac_type = function "ProofStep " ^ string_of_parallel parallel ^ Option.default "" proof_block_detection | VtProofMode s -> "ProofMode " ^ s - | VtQuery (b,(id,route)) -> - "Query " ^ string_of_in_script b ^ " report " ^ Stateid.to_string id ^ - " route " ^ string_of_int route - | VtStm ((VtFinish|VtJoinDocument|VtObserve _|VtPrintDag|VtWait), b) -> - "Stm " ^ string_of_in_script b - | VtStm (VtPG, b) -> "Stm PG " ^ string_of_in_script b - | VtStm (VtBack _, b) -> "Stm Back " ^ string_of_in_script b + | VtQuery (b, route) -> "Query " ^ string_of_in_script b ^ " route " ^ string_of_int route + | VtMeta -> "Meta " let string_of_vernac_when = function | VtLater -> "Later" @@ -52,65 +51,26 @@ let declare_vernac_classifier = classifiers := !classifiers @ [s,f] -let elide_part_of_script_and_now (a, _) = - match a with - | VtQuery (_,id) -> VtQuery (false,id), VtNow - | VtStm (x, _) -> VtStm (x, false), VtNow - | x -> x, VtNow - -let make_polymorphic (a, b as x) = - match a with - | VtStartProof (x, _, ids) -> - VtStartProof (x, Doesn'tGuaranteeOpacity, ids), b - | _ -> x +let idents_of_name : Names.Name.t -> Names.Id.t list = + function + | Names.Anonymous -> [] + | Names.Name n -> [n] -let undo_classifier = ref (fun _ -> assert false) -let set_undo_classifier f = undo_classifier := f - -let rec classify_vernac e = - let static_classifier e = match e with - (* PG compatibility *) - | VernacUnsetOption (["Silent"]|["Undo"]|["Printing";"Depth"]) - | VernacSetOption ((["Silent"]|["Undo"]|["Printing";"Depth"]),_) - when !Flags.print_emacs -> VtStm(VtPG,false), VtNow +let classify_vernac e = + let static_classifier ~poly e = match e with (* Univ poly compatibility: we run it now, so that we can just * look at Flags in stm.ml. Would be nicer to have the stm * look at the entire dag to detect this option. *) - | VernacSetOption (["Universe"; "Polymorphism"],_) - | VernacUnsetOption (["Universe"; "Polymorphism"]) -> VtSideff [], VtNow - (* Stm *) - | VernacStm Finish -> VtStm (VtFinish, true), VtNow - | VernacStm Wait -> VtStm (VtWait, true), VtNow - | VernacStm JoinDocument -> VtStm (VtJoinDocument, true), VtNow - | VernacStm PrintDag -> VtStm (VtPrintDag, true), VtNow - | VernacStm (Observe id) -> VtStm (VtObserve id, true), VtNow - | VernacStm (Command x) -> elide_part_of_script_and_now (classify_vernac x) - | VernacStm (PGLast x) -> fst (classify_vernac x), VtNow - (* Nested vernac exprs *) - | VernacProgram e -> classify_vernac e - | VernacLocal (_,e) -> classify_vernac e - | VernacPolymorphic (b, e) -> - if b || Flags.is_universe_polymorphism () (* Ok or not? *) then - make_polymorphic (classify_vernac e) - else classify_vernac e - | VernacTimeout (_,e) -> classify_vernac e - | VernacTime (_,e) | VernacRedirect (_, (_,e)) -> classify_vernac e - | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *) - (match classify_vernac e with - | ( VtQuery _ | VtProofStep _ | VtSideff _ - | VtStm _ | VtProofMode _ ), _ as x -> x - | VtQed _, _ -> - VtProofStep { parallel = `No; proof_block_detection = None }, - VtNow - | (VtStartProof _ | VtUnknown), _ -> VtUnknown, VtNow) + | ( VernacSetOption (_, l,_) | VernacUnsetOption (_, l)) + when CList.equal String.equal l Vernacentries.universe_polymorphism_option_name -> + VtSideff [], VtNow (* Qed *) | VernacAbort _ -> VtQed VtDrop, VtLater | VernacEndProof Admitted -> VtQed VtKeepAsAxiom, VtLater | VernacEndProof _ | VernacExactProof _ -> VtQed VtKeep, VtLater (* Query *) | VernacShow _ | VernacPrint _ | VernacSearch _ | VernacLocate _ - | VernacCheckMayEval _ -> - VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater + | VernacCheckMayEval _ -> VtQuery (true,Feedback.default_route), VtLater (* ProofStep *) | VernacProof _ | VernacFocus _ | VernacUnfocus @@ -127,51 +87,59 @@ let rec classify_vernac e = proof_block_detection = Some "curly" }, VtLater (* Options changing parser *) - | VernacUnsetOption (["Default";"Proof";"Using"]) - | VernacSetOption (["Default";"Proof";"Using"],_) -> VtSideff [], VtNow + | VernacUnsetOption (_, ["Default";"Proof";"Using"]) + | VernacSetOption (_, ["Default";"Proof";"Using"],_) -> VtSideff [], VtNow (* StartProof *) - | VernacDefinition ( - (Some Decl_kinds.Discharge,Decl_kinds.Definition),((_,i),_),ProveBody _) -> - VtStartProof(default_proof_mode (),Doesn'tGuaranteeOpacity,[i]), VtLater - | VernacDefinition (_,((_,i),_),ProveBody _) -> - VtStartProof(default_proof_mode (),GuaranteesOpacity,[i]), VtLater - | VernacStartTheoremProof (_,l,_) -> - let ids = - CList.map_filter (function (Some ((_,i),pl), _) -> Some i | _ -> None) l in - VtStartProof (default_proof_mode (),GuaranteesOpacity,ids), VtLater - | VernacGoal _ -> VtStartProof (default_proof_mode (),GuaranteesOpacity,[]), VtLater - | VernacFixpoint (_,l) -> + | 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 (({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) -> + let guarantee = + if discharge = Decl_kinds.DoDischarge || poly then Doesn'tGuaranteeOpacity + 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 (),GuaranteesOpacity,ids), VtLater + then VtStartProof (default_proof_mode (),guarantee,ids), VtLater else VtSideff ids, VtLater - | VernacCoFixpoint (_,l) -> + | VernacCoFixpoint (discharge,l) -> + let guarantee = + if discharge = Decl_kinds.DoDischarge || poly then Doesn'tGuaranteeOpacity + 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 (),GuaranteesOpacity,ids), VtLater + 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 [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.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 (((_,({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 _ @@ -181,7 +149,7 @@ let rec classify_vernac e = | VernacReserve _ | VernacGeneralizable _ | VernacSetOpacity _ | VernacSetStrategy _ - | VernacUnsetOption _ | VernacSetOption _ | VernacSetAppendOption _ + | VernacUnsetOption _ | VernacSetOption _ | VernacAddOption _ | VernacRemoveOption _ | VernacMemOption _ | VernacPrintOption _ | VernacGlobalCheck _ @@ -195,43 +163,58 @@ let rec 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 _ | VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _ - | VernacSyntaxExtension _ + | VernacSyntaxExtension _ | VernacSyntacticDefinition _ | VernacRequire _ | VernacImport _ | VernacInclude _ | VernacDeclareMLModule _ | VernacContext _ (* TASSI: unsure *) - | VernacProofMode _ + | VernacProofMode _ -> VtSideff [], VtNow (* These are ambiguous *) | VernacInstance _ -> VtUnknown, VtNow (* Stm will install a new classifier to handle these *) | VernacBack _ | VernacAbortAll | VernacUndoTo _ | VernacUndo _ | VernacResetName _ | VernacResetInitial - | VernacBacktrack _ | VernacBackTo _ | VernacRestart -> !undo_classifier e + | VernacBacktrack _ | VernacBackTo _ | VernacRestart -> VtMeta, VtNow (* What are these? *) | VernacToplevelControl _ | VernacRestoreState _ - | VernacWriteState _ -> VtUnknown, VtNow - | VernacError _ -> assert false + | VernacWriteState _ -> VtSideff [], VtNow (* Plugins should classify their commands *) | VernacExtend (s,l) -> try List.assoc s !classifiers l () - with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)) + with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".") + in + let rec static_control_classifier ~poly = function + | VernacExpr (f, e) -> + let poly = List.fold_left (fun poly f -> + match f with + | VernacPolymorphic b -> b + | (VernacProgram | VernacLocal _) -> poly + ) poly f in + static_classifier ~poly e + | VernacTimeout (_,e) -> static_control_classifier ~poly 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 + | ( VtQuery _ | VtProofStep _ | VtSideff _ + | VtProofMode _ | VtMeta), _ as x -> x + | VtQed _, _ -> + VtProofStep { parallel = `No; proof_block_detection = None }, + VtNow + | (VtStartProof _ | VtUnknown), _ -> VtUnknown, VtNow) in - let res = static_classifier e in - if Flags.is_universe_polymorphism () then - make_polymorphic res - else res + static_control_classifier ~poly:(Flags.is_universe_polymorphism ()) e -let classify_as_query = - VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater +let classify_as_query = VtQuery (true,Feedback.default_route), VtLater let classify_as_sideeff = VtSideff [], VtLater let classify_as_proofstep = VtProofStep { parallel = `No; proof_block_detection = None}, VtLater |