From bf1a1070d6cd111385baf59569feea2e0db3eb7c Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 20 May 2016 16:21:42 +0200 Subject: Disable memoization rather than failing when files cannot be opened. Anomaly: Uncaught exception Unix.Unix_error(Unix.EACCES, "open", "lia.cache"). Please report. --- plugins/micromega/persistent_cache.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml index 6a03e2d61f..88b13abf9a 100644 --- a/plugins/micromega/persistent_cache.ml +++ b/plugins/micromega/persistent_cache.ml @@ -212,9 +212,11 @@ let find t k = res let memo cache f = - let tbl = lazy (open_in cache) in - fun x -> - let tbl = Lazy.force tbl in + let tbl = lazy (try Some (open_in cache) with _ -> None) in + fun x -> + match Lazy.force tbl with + | None -> f x + | Some tbl -> try find tbl x with -- cgit v1.2.3 From 265be83a546b0bec6d01f6650f7489442293cb0e Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 23 May 2016 18:02:08 +0200 Subject: Hints/Univs: fix bug #4628 anomalies Fix handling of non-polymorphic hints built from polymorphic values, or simply producing new universes. We have to record the side effects of global hints built from constrs which are not polymorphic when they declare global universes, which might need to be discharged at the end of sections too. Also issue a warning when a Hint is declared for a polymorphic reference but the Hint isn't polymorphic itself (this used to produce an anomaly). For [using] hints, treat all lemmas as polymorphic, refreshing their universes at each use, as is done for their existentials (also used to produce an anomaly). --- tactics/hints.ml | 63 ++++++++++++++++++++++++++++++++----------- test-suite/bugs/closed/4628.v | 46 +++++++++++++++++++++++++++++++ 2 files changed, 94 insertions(+), 15 deletions(-) create mode 100644 test-suite/bugs/closed/4628.v diff --git a/tactics/hints.ml b/tactics/hints.ml index 42e5067c9d..1da464e6f4 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -726,10 +726,43 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, c is a constr cty is the type of constr *) +let pr_hint_term env sigma ctx = function + | IsGlobRef gr -> pr_global gr + | IsConstr (c, ctx) -> + let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in + pr_constr_env env sigma c + +(** We need an object to record the side-effect of registering + global universes associated with a hint. *) +let cache_context_set (_,c) = + Global.push_context_set false c + +let input_context_set : Univ.ContextSet.t -> Libobject.obj = + let open Libobject in + declare_object + { (default_object "Global universe context") with + cache_function = cache_context_set; + load_function = (fun _ -> cache_context_set); + discharge_function = (fun (_,a) -> Some a); + classify_function = (fun a -> Keep a) } + let fresh_global_or_constr env sigma poly cr = - match cr with - | IsGlobRef gr -> Universes.fresh_global_instance env gr - | IsConstr (c, ctx) -> (c, ctx) + let isgr, (c, ctx) = + match cr with + | IsGlobRef gr -> + true, Universes.fresh_global_instance env gr + | IsConstr (c, ctx) -> false, (c, ctx) + in + if poly then (c, ctx) + else if Univ.ContextSet.is_empty ctx then (c, ctx) + else begin + if isgr then + msg_warning (str"Using polymorphic hint " ++ + pr_hint_term env sigma ctx cr ++ str" monomorphically" ++ + str" use Polymorphic Hint to use it polymorphically."); + Lib.add_anonymous_leaf (input_context_set ctx); + (c, Univ.ContextSet.empty) + end let make_resolves env sigma flags pri poly ?name cr = let c, ctx = fresh_global_or_constr env sigma poly cr in @@ -1094,7 +1127,7 @@ let prepare_hint check (poly,local) env init (sigma,c) = let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in if poly then IsConstr (c', diff) else if local then IsConstr (c', diff) - else (Global.push_context_set false diff; + else (Lib.add_anonymous_leaf (input_context_set diff); IsConstr (c', Univ.ContextSet.empty)) let interp_hints poly = @@ -1169,18 +1202,24 @@ let expand_constructor_hints env sigma lems = match kind_of_term lem with | Ind (ind,u) -> List.init (nconstructors ind) - (fun i -> IsConstr (mkConstructU ((ind,i+1),u), - Univ.ContextSet.empty)) + (fun i -> + let ctx = Univ.ContextSet.diff (Evd.universe_context_set evd) + (Evd.universe_context_set sigma) in + not (Univ.ContextSet.is_empty ctx), + IsConstr (mkConstructU ((ind,i+1),u),ctx)) | _ -> - [prepare_hint false (false,true) env sigma (evd,lem)]) lems - + [match prepare_hint false (false,true) env sigma (evd,lem) with + | IsConstr (c, ctx) -> + not (Univ.ContextSet.is_empty ctx), IsConstr (c, ctx) + | IsGlobRef _ -> assert false (* Impossible return value *) ]) lems (* builds a hint database from a constr signature *) (* typically used with (lid, ltyp) = pf_hyps_types *) let add_hint_lemmas env sigma eapply lems hint_db = let lems = expand_constructor_hints env sigma lems in let hintlist' = - List.map_append (make_resolves env sigma (eapply,true,false) None false) lems in + List.map_append (fun (poly, lem) -> + make_resolves env sigma (eapply,true,false) None poly lem) lems in Hint_db.add_list env sigma hintlist' hint_db let make_local_hint_db env sigma ts eapply lems = @@ -1193,12 +1232,6 @@ let make_local_hint_db env sigma ts eapply lems = add_hint_lemmas env sigma eapply lems (Hint_db.add_list env sigma hintlist (Hint_db.empty ts false)) -let make_local_hint_db = - if Flags.profile then - let key = Profile.declare_profile "make_local_hint_db" in - Profile.profile4 key make_local_hint_db - else make_local_hint_db - let make_local_hint_db env sigma ?ts eapply lems = make_local_hint_db env sigma ts eapply lems diff --git a/test-suite/bugs/closed/4628.v b/test-suite/bugs/closed/4628.v new file mode 100644 index 0000000000..7d4a15d689 --- /dev/null +++ b/test-suite/bugs/closed/4628.v @@ -0,0 +1,46 @@ +Module first. + Polymorphic Record BAR (A:Type) := + { foo: A->Prop; bar: forall (x y: A), foo x -> foo y}. + +Section A. +Context {A:Type}. + +Set Printing Universes. + +Hint Resolve bar. +Goal forall (P:BAR A) x y, foo _ P x -> foo _ P y. +intros. +eauto. +Qed. +End A. +End first. + +Module firstbest. + Polymorphic Record BAR (A:Type) := + { foo: A->Prop; bar: forall (x y: A), foo x -> foo y}. + +Section A. +Context {A:Type}. + +Set Printing Universes. + +Polymorphic Hint Resolve bar. +Goal forall (P:BAR A) x y, foo _ P x -> foo _ P y. +intros. +eauto. +Qed. +End A. +End firstbest. + +Module second. +Axiom foo: Set. +Axiom foo': Set. + +Polymorphic Record BAR (A:Type) := + { bar: foo' -> foo}. +Set Printing Universes. + +Lemma baz@{i}: forall (P:BAR@{Set} nat), foo' -> foo. + eauto using bar. +Qed. +End second. -- cgit v1.2.3 From 891a8a9f7ea3bb5b0b07dc5a2df51314135d8b53 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 23 May 2016 18:58:01 +0200 Subject: Extraction/Projections: Fix bug #4710 Use the compatibility match construction to extract the compatibility constant associated to a primitive projection. --- plugins/extraction/extraction.ml | 10 ++++++++-- test-suite/bugs/closed/4710.v | 12 ++++++++++++ 2 files changed, 20 insertions(+), 2 deletions(-) create mode 100644 test-suite/bugs/closed/4710.v diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 667721e670..bdf01e73b6 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -974,7 +974,10 @@ let extract_constant env kn cb = | (Info,TypeScheme) -> (match cb.const_body with | Undef _ -> warn_info (); mk_typ_ax () - | Def c -> mk_typ (Mod_subst.force_constr c) + | Def c -> + (match cb.const_proj with + | None -> mk_typ (Mod_subst.force_constr c) + | Some pb -> mk_typ pb.proj_body) | OpaqueDef c -> add_opaque r; if access_opaque () then @@ -983,7 +986,10 @@ let extract_constant env kn cb = | (Info,Default) -> (match cb.const_body with | Undef _ -> warn_info (); mk_ax () - | Def c -> mk_def (Mod_subst.force_constr c) + | Def c -> + (match cb.const_proj with + | None -> mk_def (Mod_subst.force_constr c) + | Some pb -> mk_def pb.proj_body) | OpaqueDef c -> add_opaque r; if access_opaque () then diff --git a/test-suite/bugs/closed/4710.v b/test-suite/bugs/closed/4710.v new file mode 100644 index 0000000000..fdc8501099 --- /dev/null +++ b/test-suite/bugs/closed/4710.v @@ -0,0 +1,12 @@ +Set Primitive Projections. +Record Foo' := Foo { foo : nat }. +Extraction foo. +Record Foo2 (a : nat) := Foo2c { foo2p : nat; foo2b : bool }. +Extraction Language Ocaml. +Extraction foo2p. + +Definition bla (x : Foo2 0) := foo2p _ x. +Extraction bla. + +Definition bla' (a : nat) (x : Foo2 a) := foo2b _ x. +Extraction bla'. -- cgit v1.2.3 From 9de5a59aa6994e8023b9e551b232a73aab3521fa Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 26 May 2016 11:32:51 +0200 Subject: rewrite/Univs: Fix bug # 4498. --- tactics/rewrite.ml | 23 ++++++++++++----------- test-suite/bugs/closed/4498.v | 24 ++++++++++++++++++++++++ 2 files changed, 36 insertions(+), 11 deletions(-) create mode 100644 test-suite/bugs/closed/4498.v diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 9d70c177b4..c7cfc4dc72 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1799,10 +1799,10 @@ let declare_projection n instance_id r = let poly = Global.is_polymorphic r in let env = Global.env () in let sigma = Evd.from_env env in - let evd,c = Evd.fresh_global env sigma r in + let sigma,c = Evd.fresh_global env sigma r in let ty = Retyping.get_type_of env sigma c in let term = proper_projection c ty in - let typ = Typing.unsafe_type_of env sigma term in + let sigma, typ = Typing.type_of env sigma term in let ctx, typ = decompose_prod_assum typ in let typ = let n = @@ -1831,9 +1831,7 @@ let declare_projection n instance_id r = ignore(Declare.declare_constant n (Entries.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition)) -let build_morphism_signature m = - let env = Global.env () in - let sigma = Evd.from_env env in +let build_morphism_signature env sigma m = let m,ctx = Constrintern.interp_constr env sigma m in let sigma = Evd.from_ctx ctx in let t = Typing.unsafe_type_of env sigma m in @@ -1858,8 +1856,10 @@ let build_morphism_signature m = in let morph = e_app_poly env evd PropGlobal.proper_type [| t; sig_; m |] in let evd = solve_constraints env !evd in - let m = Evarutil.nf_evar evd morph in - Evarutil.check_evars env Evd.empty evd m; m + let evd = Evd.nf_constraints evd in + let m = Evarutil.nf_evars_universes evd morph in + Evarutil.check_evars env Evd.empty evd m; + Evd.evar_universe_context evd, m let default_morphism sign m = let env = Global.env () in @@ -1896,12 +1896,13 @@ let add_morphism_infer glob m n = init_setoid (); let poly = Flags.is_universe_polymorphism () in let instance_id = add_suffix n "_Proper" in - let instance = build_morphism_signature m in - let evd = Evd.from_env (Global.env ()) in + let env = Global.env () in + let evd = Evd.from_env env in + let uctx, instance = build_morphism_signature env evd m in if Lib.is_modtype () then let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id (Entries.ParameterEntry - (None,poly,(instance,Univ.UContext.empty),None), + (None,poly,(instance,Evd.evar_context_universe_context uctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical) in add_instance (Typeclasses.new_instance @@ -1924,7 +1925,7 @@ let add_morphism_infer glob m n = let hook = Lemmas.mk_hook hook in Flags.silently (fun () -> - Lemmas.start_proof instance_id kind evd instance hook; + Lemmas.start_proof instance_id kind (Evd.from_ctx uctx) instance hook; ignore (Pfedit.by (Tacinterp.interp tac))) () let add_morphism glob binders m s n = diff --git a/test-suite/bugs/closed/4498.v b/test-suite/bugs/closed/4498.v new file mode 100644 index 0000000000..ccdb2dddda --- /dev/null +++ b/test-suite/bugs/closed/4498.v @@ -0,0 +1,24 @@ +Require Export Coq.Unicode.Utf8. +Require Export Coq.Classes.Morphisms. +Require Export Coq.Relations.Relation_Definitions. + +Set Universe Polymorphism. + +Reserved Notation "a ~> b" (at level 90, right associativity). + +Class Category := { + ob : Type; + uhom := Type : Type; + hom : ob → ob → uhom where "a ~> b" := (hom a b); + compose : ∀ {A B C}, (B ~> C) → (A ~> B) → (A ~> C); + equiv : ∀ {A B}, relation (A ~> B); + is_equiv : ∀ {A B}, @Equivalence (A ~> B) equiv; + comp_respects : ∀ {A B C}, + Proper (@equiv B C ==> @equiv A B ==> @equiv A C) (@compose A B C); +}. + +Require Export Coq.Setoids.Setoid. + +Add Parametric Morphism `{C : Category} {A B C} : (@compose _ A B C) with + signature equiv ==> equiv ==> equiv as compose_mor. +Proof. apply comp_respects. Qed. \ No newline at end of file -- cgit v1.2.3 From 7b1e94365bee6cc984e5f476864ac753e6f46e3a Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 26 May 2016 13:25:52 +0200 Subject: Pfedit.get_current_context refinement (fix #4523) Return the most appropriate evar_map for commands that can run on non-focused proofs (like Check, Show and debug printers) so that universes and existentials are printed correctly (they are global to the proof). The API is backwards compatible. --- dev/top_printers.ml | 4 +--- printing/printer.ml | 5 +---- proofs/pfedit.ml | 23 +++++++++++++++++------ proofs/pfedit.mli | 8 ++++++++ stm/lemmas.ml | 10 +--------- stm/lemmas.mli | 1 - 6 files changed, 28 insertions(+), 23 deletions(-) diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 6e5b048ccd..4c733dd4f7 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -485,9 +485,7 @@ let ppist ist = (* Vernac-level debugging commands *) let in_current_context f c = - let (evmap,sign) = - try Pfedit.get_current_goal_context () - with e when Logic.catchable_exception e -> (Evd.empty, Global.env()) in + let (evmap,sign) = Pfedit.get_current_context () in f (fst (Constrintern.interp_constr sign evmap c))(*FIXME*) (* We expand the result of preprocessing to be independent of camlp4 diff --git a/printing/printer.ml b/printing/printer.ml index 8469490f05..ac20eeb6f5 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -28,10 +28,7 @@ let delayed_emacs_cmd s = if !Flags.print_emacs then s () else str "" let get_current_context () = - try Pfedit.get_current_goal_context () - with e when Logic.catchable_exception e -> - let env = Global.env () in - (Evd.from_env env, env) + Pfedit.get_current_context () (**********************************************************************) (** Terms *) diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 2f5c1d1c2b..a515c9e750 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -71,23 +71,34 @@ let get_nth_V82_goal i = with Failure _ -> raise NoSuchGoal let get_goal_context_gen i = - try -let { it=goal ; sigma=sigma; } = get_nth_V82_goal i in -(sigma, Refiner.pf_env { it=goal ; sigma=sigma; }) - with Proof_global.NoCurrentProof -> Errors.error "No focused proof." + let { it=goal ; sigma=sigma; } = get_nth_V82_goal i in + (sigma, Refiner.pf_env { it=goal ; sigma=sigma; }) let get_goal_context i = try get_goal_context_gen i - with NoSuchGoal -> Errors.error "No such goal." + with Proof_global.NoCurrentProof -> Errors.error "No focused proof." + | NoSuchGoal -> Errors.error "No such goal." let get_current_goal_context () = try get_goal_context_gen 1 - with NoSuchGoal -> + with Proof_global.NoCurrentProof -> Errors.error "No focused proof." + | NoSuchGoal -> (* spiwack: returning empty evar_map, since if there is no goal, under focus, there is no accessible evar either *) let env = Global.env () in (Evd.from_env env, env) +let get_current_context () = + try get_goal_context_gen 1 + with Proof_global.NoCurrentProof -> + let env = Global.env () in + (Evd.from_env env, env) + | NoSuchGoal -> + (* No more focused goals ? *) + let p = get_pftreestate () in + let evd = Proof.in_proof p (fun x -> x) in + (evd, Global.env ()) + let current_proof_statement () = match Proof_global.V82.get_current_initial_conclusions () with | (id,([concl],strength)) -> id,strength,concl diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index cd89920151..cfab8bd630 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -93,6 +93,14 @@ val get_goal_context : int -> Evd.evar_map * env val get_current_goal_context : unit -> Evd.evar_map * env +(** [get_current_context ()] returns the context of the + current focused goal. If there is no focused goal but there + is a proof in progress, it returns the corresponding evar_map. + If there is no pending proof then it returns the current global + environment and empty evar_map. *) + +val get_current_context : unit -> Evd.evar_map * env + (** [current_proof_statement] *) val current_proof_statement : diff --git a/stm/lemmas.ml b/stm/lemmas.ml index fb64a10c6c..5b205e79ef 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -509,13 +509,5 @@ let save_proof ?proof = function (* Miscellaneous *) let get_current_context () = - try Pfedit.get_current_goal_context () - with e when Logic.catchable_exception e -> - try (* No more focused goals ? *) - let p = Pfedit.get_pftreestate () in - let evd = Proof.in_proof p (fun x -> x) in - (evd, Global.env ()) - with Proof_global.NoCurrentProof -> - let env = Global.env () in - (Evd.from_env env, env) + Pfedit.get_current_context () diff --git a/stm/lemmas.mli b/stm/lemmas.mli index 16e54e318e..ca6af9a3fa 100644 --- a/stm/lemmas.mli +++ b/stm/lemmas.mli @@ -60,4 +60,3 @@ val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> uni and the current global env *) val get_current_context : unit -> Evd.evar_map * Environ.env - -- cgit v1.2.3 From 34ba7e0d17c76c42a8ece4d195d280f7722f3bae Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 27 May 2016 13:13:25 +0200 Subject: STM: fix argument filtering for slaves Command line options to be dropped got outdated after vi -> vio renaming. This made the par: goal selector do not work in conjunction with -quick. --- stm/asyncTaskQueue.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 8649a14c54..1214fc4da9 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -125,7 +125,7 @@ module Make(T : Task) = struct "-async-proofs-worker-priority"; Flags.string_of_priority !Flags.async_proofs_worker_priority] | ("-ideslave"|"-emacs"|"-emacs-U"|"-batch")::tl -> set_slave_opt tl - | ("-async-proofs" |"-toploop" |"-vi2vo" + | ("-async-proofs" |"-toploop" |"-vio2vo" |"-load-vernac-source" |"-l" |"-load-vernac-source-verbose" |"-lv" |"-compile" |"-compile-verbose" |"-async-proofs-worker-priority" |"-worker-id") :: _ :: tl -> -- cgit v1.2.3 From 35fb7ad402fee1e3e247ccf37438d3a7a5230629 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 29 May 2016 15:58:21 +0200 Subject: Fix bug #4746: Anomaly: Evar ?X10 was not declared. Some dubious evarmap manipulation is going on in destruct because of the use of clenv primitives. Here, building a clenv was introducing new evars that were not taken into account in the remainder of the tactic. We plug them back using a local workaround. Eventually, this code should be replaced by an evar-based one, but meanwhile, we rely on what is probably a hack. --- tactics/tactics.ml | 2 ++ test-suite/bugs/closed/4746.v | 14 ++++++++++++++ 2 files changed, 16 insertions(+) create mode 100644 test-suite/bugs/closed/4746.v diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 63d3c694ea..4562e25184 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1224,6 +1224,8 @@ let general_elim with_evars clear_flag (c, lbindc) elim = let t = try snd (reduce_to_quantified_ind env sigma ct) with UserError _ -> ct in let elimtac = elimination_clause_scheme with_evars in let indclause = make_clenv_binding env sigma (c, t) lbindc in + let sigma = meta_merge sigma (clear_metas indclause.evd) in + Proofview.Unsafe.tclEVARS sigma <*> Tacticals.New.tclTHEN (general_elim_clause_gen elimtac indclause elim) (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c) diff --git a/test-suite/bugs/closed/4746.v b/test-suite/bugs/closed/4746.v new file mode 100644 index 0000000000..d64cc6fe68 --- /dev/null +++ b/test-suite/bugs/closed/4746.v @@ -0,0 +1,14 @@ +Variables P Q : nat -> Prop. +Variable f : nat -> nat. + +Goal forall (x:nat), (forall y, P y -> forall z, Q z -> y=f z -> False) -> False. +Proof. +intros. +ecase H with (3:=eq_refl). +Abort. + +Goal forall (x:nat), (forall y, y=x -> False) -> False. +Proof. +intros. +unshelve ecase H with (1:=eq_refl). +Qed. -- cgit v1.2.3 From cb31cd671a0ef4da0cf834dad5b67776098bb0d1 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Mon, 30 May 2016 17:16:25 +0200 Subject: Extraction : add a location in the error message about polyprop --- plugins/extraction/extraction.ml | 68 +++++++++++++++++++++++++++------------- plugins/extraction/table.ml | 10 ++++-- plugins/extraction/table.mli | 2 +- 3 files changed, 56 insertions(+), 24 deletions(-) diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index bdf01e73b6..0ac8e3c4cf 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -35,17 +35,18 @@ let current_fixpoints = ref ([] : constant list) let none = Evd.empty +(* NB: In OCaml, [type_of] and [get_of] might raise + [SingletonInductiveBecomeProp]. this exception will be catched + in late wrappers around the exported functions of this file, + in order to display the location of the issue. *) + let type_of env c = - try - let polyprop = (lang() == Haskell) in - Retyping.get_type_of ~polyprop env none (strip_outer_cast c) - with SingletonInductiveBecomesProp id -> error_singleton_become_prop id + let polyprop = (lang() == Haskell) in + Retyping.get_type_of ~polyprop env none (strip_outer_cast c) let sort_of env c = - try - let polyprop = (lang() == Haskell) in - Retyping.get_sort_family_of ~polyprop env none (strip_outer_cast c) - with SingletonInductiveBecomesProp id -> error_singleton_become_prop id + let polyprop = (lang() == Haskell) in + Retyping.get_sort_family_of ~polyprop env none (strip_outer_cast c) (*S Generation of flags and signatures. *) @@ -328,11 +329,22 @@ and extract_type_scheme env db c p = (*S Extraction of an inductive type. *) +(* First, a version with cache *) + and extract_ind env kn = (* kn is supposed to be in long form *) let mib = Environ.lookup_mind kn env in match lookup_ind kn mib with | Some ml_ind -> ml_ind | None -> + try + extract_really_ind env kn mib + with SingletonInductiveBecomesProp id -> + (* TODO : which inductive is concerned in the block ? *) + error_singleton_become_prop id (Some (IndRef (kn,0))) + +(* Then the real function *) + +and extract_really_ind env kn mib = (* First, if this inductive is aliased via a Module, we process the original inductive if possible. When at toplevel of the monolithic case, we cannot do much @@ -934,11 +946,13 @@ let extract_fixpoint env vkn (fi,ti,ci) = (* for replacing recursive calls [Rel ..] by the corresponding [Const]: *) let sub = List.rev_map mkConst kns in for i = 0 to n-1 do - if sort_of env ti.(i) != InProp then begin - let e,t = extract_std_constant env vkn.(i) (substl sub ci.(i)) ti.(i) in - terms.(i) <- e; - types.(i) <- t; - end + if sort_of env ti.(i) != InProp then + try + let e,t = extract_std_constant env vkn.(i) (substl sub ci.(i)) ti.(i) in + terms.(i) <- e; + types.(i) <- t; + with SingletonInductiveBecomesProp id -> + error_singleton_become_prop id (Some (ConstRef vkn.(i))) done; current_fixpoints := []; Dfix (Array.map (fun kn -> ConstRef kn) vkn, terms, types) @@ -968,7 +982,8 @@ let extract_constant env kn cb = let e,t = extract_std_constant env kn c typ in Dterm (r,e,t) in - match flag_of_type env typ with + try + match flag_of_type env typ with | (Logic,TypeScheme) -> warn_log (); Dtype (r, [], Tdummy Ktype) | (Logic,Default) -> warn_log (); Dterm (r, MLdummy Kprop, Tdummy Kprop) | (Info,TypeScheme) -> @@ -995,11 +1010,14 @@ let extract_constant env kn cb = if access_opaque () then mk_def (Opaqueproof.force_proof (Environ.opaque_tables env) c) else mk_ax ()) + with SingletonInductiveBecomesProp id -> + error_singleton_become_prop id (Some (ConstRef kn)) let extract_constant_spec env kn cb = let r = ConstRef kn in let typ = Typeops.type_of_constant_type env cb.const_type in - match flag_of_type env typ with + try + match flag_of_type env typ with | (Logic, TypeScheme) -> Stype (r, [], Some (Tdummy Ktype)) | (Logic, Default) -> Sval (r, Tdummy Kprop) | (Info, TypeScheme) -> @@ -1014,26 +1032,34 @@ let extract_constant_spec env kn cb = | (Info, Default) -> let t = snd (record_constant_type env kn (Some typ)) in Sval (r, type_expunge env t) + with SingletonInductiveBecomesProp id -> + error_singleton_become_prop id (Some (ConstRef kn)) let extract_with_type env c = - let typ = type_of env c in - match flag_of_type env typ with + try + let typ = type_of env c in + match flag_of_type env typ with | (Info, TypeScheme) -> let s,vl = type_sign_vl env typ in let db = db_from_sign s in let t = extract_type_scheme env db c (List.length s) in Some (vl, t) | _ -> None + with SingletonInductiveBecomesProp id -> + error_singleton_become_prop id None let extract_constr env c = reset_meta_count (); - let typ = type_of env c in - match flag_of_type env typ with + try + let typ = type_of env c in + match flag_of_type env typ with | (_,TypeScheme) -> MLdummy Ktype, Tdummy Ktype | (Logic,_) -> MLdummy Kprop, Tdummy Kprop | (Info,Default) -> - let mlt = extract_type env [] 1 typ [] in - extract_term env Mlenv.empty mlt c [], mlt + let mlt = extract_type env [] 1 typ [] in + extract_term env Mlenv.empty mlt c [], mlt + with SingletonInductiveBecomesProp id -> + error_singleton_become_prop id None let extract_inductive env kn = let ind = extract_ind env kn in diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index d7842e127d..5f83d2949e 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -391,9 +391,15 @@ let error_no_module_expr mp = ++ str "some Declare Module outside any Module Type.\n" ++ str "This situation is currently unsupported by the extraction.") -let error_singleton_become_prop id = +let error_singleton_become_prop id og = + let loc = + match og with + | Some g -> fnl () ++ str "in " ++ safe_pr_global g ++ + str " (or in its mutual block)" + | None -> mt () + in err (str "The informative inductive type " ++ pr_id id ++ - str " has a Prop instance.\n" ++ + str " has a Prop instance" ++ loc ++ str "." ++ fnl () ++ str "This happens when a sort-polymorphic singleton inductive type\n" ++ str "has logical parameters, such as (I,I) : (True * True) : Prop.\n" ++ str "The Ocaml extraction cannot handle this situation yet.\n" ++ diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 2b163610e9..62c20bd3a7 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -30,7 +30,7 @@ val error_inductive : global_reference -> 'a val error_nb_cons : unit -> 'a val error_module_clash : module_path -> module_path -> 'a val error_no_module_expr : module_path -> 'a -val error_singleton_become_prop : Id.t -> 'a +val error_singleton_become_prop : Id.t -> global_reference option -> 'a val error_unknown_module : qualid -> 'a val error_scheme : unit -> 'a val error_not_visible : global_reference -> 'a -- cgit v1.2.3 From 27dffdea5b46f6282c1584db0555213e744352fa Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 31 May 2016 13:33:01 +0200 Subject: Revert "Rename Lexer -> CLexer." This reverts commit a66b57ba4bba866bb626bde2b6fe3b762347eb3e. --- .gitignore | 2 +- dev/printers.mllib | 2 +- grammar/argextend.ml4 | 2 +- grammar/grammar.mllib | 2 +- parsing/cLexer.ml4 | 695 ------------------------------------------------- parsing/cLexer.mli | 38 --- parsing/compat.ml4 | 2 +- parsing/egramcoq.ml | 6 +- parsing/g_constr.ml4 | 2 +- parsing/g_prim.ml4 | 2 +- parsing/g_tactic.ml4 | 2 +- parsing/g_vernac.ml4 | 2 +- parsing/lexer.ml4 | 695 +++++++++++++++++++++++++++++++++++++++++++++++++ parsing/lexer.mli | 38 +++ parsing/parsing.mllib | 2 +- parsing/pcoq.ml4 | 4 +- tactics/tacinterp.ml | 2 +- toplevel/cerrors.ml | 2 +- toplevel/coqloop.ml | 2 +- toplevel/coqtop.ml | 4 +- toplevel/metasyntax.ml | 14 +- toplevel/vernac.ml | 8 +- 22 files changed, 764 insertions(+), 764 deletions(-) delete mode 100644 parsing/cLexer.ml4 delete mode 100644 parsing/cLexer.mli create mode 100644 parsing/lexer.ml4 create mode 100644 parsing/lexer.mli diff --git a/.gitignore b/.gitignore index 3f9856916a..7efa761300 100644 --- a/.gitignore +++ b/.gitignore @@ -127,7 +127,7 @@ grammar/tacextend.ml grammar/vernacextend.ml grammar/argextend.ml parsing/pcoq.ml -parsing/cLexer.ml +parsing/lexer.ml plugins/setoid_ring/newring.ml plugins/field/field.ml plugins/nsatz/nsatz.ml diff --git a/dev/printers.mllib b/dev/printers.mllib index e054c1bc70..ad9a5d75e6 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -151,7 +151,7 @@ States Genprint Tok -CLexer +Lexer Ppextend Pputils Ppannotation diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index b3c71a703c..cb0f7d2d31 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -287,7 +287,7 @@ EXTEND GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s)) | s = STRING -> if String.length s > 0 && Util.is_letter s.[0] then - CLexer.add_keyword s; + Lexer.add_keyword s; GramTerminal s ] ] ; diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib index 1864fae5fc..71e5b8ae2c 100644 --- a/grammar/grammar.mllib +++ b/grammar/grammar.mllib @@ -50,7 +50,7 @@ Constrexpr_ops Compat Tok -CLexer +Lexer Pcoq G_prim G_tactic diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4 deleted file mode 100644 index 5d96873f31..0000000000 --- a/parsing/cLexer.ml4 +++ /dev/null @@ -1,695 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* char -> int = compare end -module CharMap = Map.Make (CharOrd) - -type ttree = { - node : string option; - branch : ttree CharMap.t } - -let empty_ttree = { node = None; branch = CharMap.empty } - -let ttree_add ttree str = - let rec insert tt i = - if i == String.length str then - {node = Some str; branch = tt.branch} - else - let c = str.[i] in - let br = - match try Some (CharMap.find c tt.branch) with Not_found -> None with - | Some tt' -> - CharMap.add c (insert tt' (i + 1)) (CharMap.remove c tt.branch) - | None -> - let tt' = {node = None; branch = CharMap.empty} in - CharMap.add c (insert tt' (i + 1)) tt.branch - in - { node = tt.node; branch = br } - in - insert ttree 0 - -(* Search a string in a dictionary: raises [Not_found] - if the word is not present. *) - -let ttree_find ttree str = - let rec proc_rec tt i = - if i == String.length str then tt - else proc_rec (CharMap.find str.[i] tt.branch) (i+1) - in - proc_rec ttree 0 - -(* Removes a string from a dictionary: returns an equal dictionary - if the word not present. *) -let ttree_remove ttree str = - let rec remove tt i = - if i == String.length str then - {node = None; branch = tt.branch} - else - let c = str.[i] in - let br = - match try Some (CharMap.find c tt.branch) with Not_found -> None with - | Some tt' -> - CharMap.add c (remove tt' (i + 1)) (CharMap.remove c tt.branch) - | None -> tt.branch - in - { node = tt.node; branch = br } - in - remove ttree 0 - - -(* Errors occurring while lexing (explained as "Lexer error: ...") *) - -module Error = struct - - type t = - | Illegal_character - | Unterminated_comment - | Unterminated_string - | Undefined_token - | Bad_token of string - | UnsupportedUnicode of int - - exception E of t - - let to_string x = - "Syntax Error: Lexer: " ^ - (match x with - | Illegal_character -> "Illegal character" - | Unterminated_comment -> "Unterminated comment" - | Unterminated_string -> "Unterminated string" - | Undefined_token -> "Undefined token" - | Bad_token tok -> Format.sprintf "Bad token %S" tok - | UnsupportedUnicode x -> - Printf.sprintf "Unsupported Unicode character (0x%x)" x) - - (* Require to fix the Camlp4 signature *) - let print ppf x = Pp.pp_with ppf (Pp.str (to_string x)) - -end -open Error - -let err loc str = Loc.raise (Loc.make_loc loc) (Error.E str) - -let bad_token str = raise (Error.E (Bad_token str)) - -(* Lexer conventions on tokens *) - -type token_kind = - | Utf8Token of (Unicode.status * int) - | AsciiChar - | EmptyStream - -let error_unsupported_unicode_character n unicode cs = - let bp = Stream.count cs in - err (bp,bp+n) (UnsupportedUnicode unicode) - -let error_utf8 cs = - let bp = Stream.count cs in - Stream.junk cs; (* consume the char to avoid read it and fail again *) - err (bp, bp+1) Illegal_character - -let utf8_char_size cs = function - (* Utf8 leading byte *) - | '\x00'..'\x7F' -> 1 - | '\xC0'..'\xDF' -> 2 - | '\xE0'..'\xEF' -> 3 - | '\xF0'..'\xF7' -> 4 - | _ (* '\x80'..\xBF'|'\xF8'..'\xFF' *) -> error_utf8 cs - -let njunk n = Util.repeat n Stream.junk - -let check_utf8_trailing_byte cs c = - if not (Int.equal (Char.code c land 0xC0) 0x80) then error_utf8 cs - -(* Recognize utf8 blocks (of length less than 4 bytes) *) -(* but don't certify full utf8 compliance (e.g. no emptyness check) *) -let lookup_utf8_tail c cs = - let c1 = Char.code c in - if Int.equal (c1 land 0x40) 0 || Int.equal (c1 land 0x38) 0x38 then error_utf8 cs - else - let n, unicode = - if Int.equal (c1 land 0x20) 0 then - match Stream.npeek 2 cs with - | [_;c2] -> - check_utf8_trailing_byte cs c2; - 2, (c1 land 0x1F) lsl 6 + (Char.code c2 land 0x3F) - | _ -> error_utf8 cs - else if Int.equal (c1 land 0x10) 0 then - match Stream.npeek 3 cs with - | [_;c2;c3] -> - check_utf8_trailing_byte cs c2; check_utf8_trailing_byte cs c3; - 3, (c1 land 0x0F) lsl 12 + (Char.code c2 land 0x3F) lsl 6 + - (Char.code c3 land 0x3F) - | _ -> error_utf8 cs - else match Stream.npeek 4 cs with - | [_;c2;c3;c4] -> - check_utf8_trailing_byte cs c2; check_utf8_trailing_byte cs c3; - check_utf8_trailing_byte cs c4; - 4, (c1 land 0x07) lsl 18 + (Char.code c2 land 0x3F) lsl 12 + - (Char.code c3 land 0x3F) lsl 6 + (Char.code c4 land 0x3F) - | _ -> error_utf8 cs - in - try Unicode.classify unicode, n - with Unicode.Unsupported -> - njunk n cs; error_unsupported_unicode_character n unicode cs - -let lookup_utf8 cs = - match Stream.peek cs with - | Some ('\x00'..'\x7F') -> AsciiChar - | Some ('\x80'..'\xFF' as c) -> Utf8Token (lookup_utf8_tail c cs) - | None -> EmptyStream - -let unlocated f x = f x - (** FIXME: should we still unloc the exception? *) -(* try f x with Loc.Exc_located (_, exc) -> raise exc *) - -let check_keyword str = - let rec loop_symb = parser - | [< ' (' ' | '\n' | '\r' | '\t' | '"') >] -> bad_token str - | [< s >] -> - match unlocated lookup_utf8 s with - | Utf8Token (_,n) -> njunk n s; loop_symb s - | AsciiChar -> Stream.junk s; loop_symb s - | EmptyStream -> () - in - loop_symb (Stream.of_string str) - -let check_keyword_to_add s = - try check_keyword s - with Error.E (UnsupportedUnicode unicode) -> - Flags.if_verbose msg_warning - (strbrk (Printf.sprintf "Token '%s' contains unicode character 0x%x \ - which will not be parsable." s unicode)) - -let check_ident str = - let rec loop_id intail = parser - | [< ' ('a'..'z' | 'A'..'Z' | '_'); s >] -> - loop_id true s - | [< ' ('0'..'9' | ''') when intail; s >] -> - loop_id true s - | [< s >] -> - match unlocated lookup_utf8 s with - | Utf8Token (Unicode.Letter, n) -> njunk n s; loop_id true s - | Utf8Token (Unicode.IdentPart, n) when intail -> - njunk n s; - loop_id true s - | EmptyStream -> () - | Utf8Token _ | AsciiChar -> bad_token str - in - loop_id false (Stream.of_string str) - -let is_ident str = - try let _ = check_ident str in true with Error.E _ -> false - -(* Keyword and symbol dictionary *) -let token_tree = ref empty_ttree - -let is_keyword s = - try match (ttree_find !token_tree s).node with None -> false | Some _ -> true - with Not_found -> false - -let add_keyword str = - if not (is_keyword str) then - begin - check_keyword_to_add str; - token_tree := ttree_add !token_tree str - end - -let remove_keyword str = - token_tree := ttree_remove !token_tree str - -(* Freeze and unfreeze the state of the lexer *) -type frozen_t = ttree - -let freeze () = !token_tree -let unfreeze tt = (token_tree := tt) - -(* The string buffering machinery *) - -let buff = ref (String.create 80) - -let store len x = - if len >= String.length !buff then - buff := !buff ^ String.create (String.length !buff); - !buff.[len] <- x; - succ len - -let rec nstore n len cs = - if n>0 then nstore (n-1) (store len (Stream.next cs)) cs else len - -let get_buff len = String.sub !buff 0 len - -(* The classical lexer: idents, numbers, quoted strings, comments *) - -let rec ident_tail len = parser - | [< ' ('a'..'z' | 'A'..'Z' | '0'..'9' | ''' | '_' as c); s >] -> - ident_tail (store len c) s - | [< s >] -> - match lookup_utf8 s with - | Utf8Token ((Unicode.IdentPart | Unicode.Letter), n) -> - ident_tail (nstore n len s) s - | _ -> len - -let rec number len = parser - | [< ' ('0'..'9' as c); s >] -> number (store len c) s - | [< >] -> len - -let rec string in_comments bp len = parser - | [< ''"'; esc=(parser [<''"' >] -> true | [< >] -> false); s >] -> - if esc then string in_comments bp (store len '"') s else len - | [< ''('; s >] -> - (parser - | [< ''*'; s >] -> - string - (Option.map succ in_comments) - bp (store (store len '(') '*') - s - | [< >] -> - string in_comments bp (store len '(') s) s - | [< ''*'; s >] -> - (parser - | [< '')'; s >] -> - let () = match in_comments with - | Some 0 -> - msg_warning - (strbrk - "Not interpreting \"*)\" as the end of current \ - non-terminated comment because it occurs in a \ - non-terminated string of the comment.") - | _ -> () - in - let in_comments = Option.map pred in_comments in - string in_comments bp (store (store len '*') ')') s - | [< >] -> - string in_comments bp (store len '*') s) s - | [< 'c; s >] -> string in_comments bp (store len c) s - | [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_string - -(* Hook for exporting comment into xml theory files *) -let (f_xml_output_comment, xml_output_comment) = Hook.make ~default:ignore () - -(* Utilities for comments in beautify *) -let comment_begin = ref None -let comm_loc bp = match !comment_begin with -| None -> comment_begin := Some bp -| _ -> () - -let current = Buffer.create 8192 -let between_com = ref true - -type com_state = int option * string * bool -let restore_com_state (o,s,b) = - comment_begin := o; - Buffer.clear current; Buffer.add_string current s; - between_com := b -let dflt_com = (None,"",true) -let com_state () = - let s = (!comment_begin, Buffer.contents current, !between_com) in - restore_com_state dflt_com; s - -let real_push_char c = Buffer.add_char current c - -(* Add a char if it is between two commands, if it is a newline or - if the last char is not a space itself. *) -let push_char c = - if - !between_com || List.mem c ['\n';'\r'] || - (List.mem c [' ';'\t']&& - (Int.equal (Buffer.length current) 0 || - not (let s = Buffer.contents current in - List.mem s.[String.length s - 1] [' ';'\t';'\n';'\r']))) - then - real_push_char c - -let push_string s = Buffer.add_string current s - -let null_comment s = - let rec null i = - i<0 || (List.mem s.[i] [' ';'\t';'\n';'\r'] && null (i-1)) in - null (String.length s - 1) - -let comment_stop ep = - let current_s = Buffer.contents current in - if !Flags.xml_export && Buffer.length current > 0 && - (!between_com || not(null_comment current_s)) then - Hook.get f_xml_output_comment current_s; - (if Flags.do_beautify() && Buffer.length current > 0 && - (!between_com || not(null_comment current_s)) then - let bp = match !comment_begin with - Some bp -> bp - | None -> - msgerrnl(str "No begin location for comment '" - ++ str current_s ++str"' ending at " - ++ int ep); - ep-1 in - Pp.comments := ((bp,ep),current_s) :: !Pp.comments); - Buffer.clear current; - comment_begin := None; - between_com := false - -(* Does not unescape!!! *) -let rec comm_string bp = parser - | [< ''"' >] -> push_string "\"" - | [< ''\\'; _ = - (parser [< ' ('"' | '\\' as c) >] -> - let () = match c with - | '"' -> real_push_char c - | _ -> () - in - real_push_char c - | [< >] -> real_push_char '\\'); s >] - -> comm_string bp s - | [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_string - | [< 'c; s >] -> real_push_char c; comm_string bp s - -let rec comment bp = parser bp2 - | [< ''('; - _ = (parser - | [< ''*'; s >] -> push_string "(*"; comment bp s - | [< >] -> push_string "(" ); - s >] -> comment bp s - | [< ''*'; - _ = parser - | [< '')' >] -> push_string "*)"; - | [< s >] -> real_push_char '*'; comment bp s >] -> () - | [< ''"'; s >] -> - if Flags.do_beautify() then (push_string"\"";comm_string bp2 s) - else ignore (string (Some 0) bp2 0 s); - comment bp s - | [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_comment - | [< 'z; s >] -> real_push_char z; comment bp s - -(* Parse a special token, using the [token_tree] *) - -(* Peek as much utf-8 lexemes as possible *) -(* and retain the longest valid special token obtained *) -let rec progress_further last nj tt cs = - try progress_from_byte last nj tt cs (List.nth (Stream.npeek (nj+1) cs) nj) - with Failure _ -> last - -and update_longest_valid_token last nj tt cs = - match tt.node with - | Some _ as last' -> - stream_njunk nj cs; - progress_further last' 0 tt cs - | None -> - progress_further last nj tt cs - -(* nj is the number of char peeked since last valid token *) -(* n the number of char in utf8 block *) -and progress_utf8 last nj n c tt cs = - try - let tt = CharMap.find c tt.branch in - if Int.equal n 1 then - update_longest_valid_token last (nj+n) tt cs - else - match Util.List.skipn (nj+1) (Stream.npeek (nj+n) cs) with - | l when Int.equal (List.length l) (n - 1) -> - List.iter (check_utf8_trailing_byte cs) l; - let tt = List.fold_left (fun tt c -> CharMap.find c tt.branch) tt l in - update_longest_valid_token last (nj+n) tt cs - | _ -> - error_utf8 cs - with Not_found -> - last - -and progress_from_byte last nj tt cs c = - progress_utf8 last nj (utf8_char_size cs c) c tt cs - -let find_keyword id s = - let tt = ttree_find !token_tree id in - match progress_further tt.node 0 tt s with - | None -> raise Not_found - | Some c -> KEYWORD c - -let process_sequence bp c cs = - let rec aux n cs = - match Stream.peek cs with - | Some c' when c == c' -> Stream.junk cs; aux (n+1) cs - | _ -> BULLET (String.make n c), (bp, Stream.count cs) - in - aux 1 cs - -(* Must be a special token *) -let process_chars bp c cs = - let t = progress_from_byte None (-1) !token_tree cs c in - let ep = Stream.count cs in - match t with - | Some t -> (KEYWORD t, (bp, ep)) - | None -> - let ep' = bp + utf8_char_size cs c in - njunk (ep' - ep) cs; - err (bp, ep') Undefined_token - -let token_of_special c s = match c with - | '$' -> METAIDENT s - | '.' -> FIELD s - | _ -> assert false - -(* Parse what follows a dot / a dollar *) - -let parse_after_special c bp = - parser - | [< ' ('a'..'z' | 'A'..'Z' | '_' as d); len = ident_tail (store 0 d) >] -> - token_of_special c (get_buff len) - | [< s >] -> - match lookup_utf8 s with - | Utf8Token (Unicode.Letter, n) -> - token_of_special c (get_buff (ident_tail (nstore n 0 s) s)) - | AsciiChar | Utf8Token _ | EmptyStream -> fst (process_chars bp c s) - -(* Parse what follows a question mark *) - -let parse_after_qmark bp s = - match Stream.peek s with - | Some ('a'..'z' | 'A'..'Z' | '_') -> LEFTQMARK - | None -> KEYWORD "?" - | _ -> - match lookup_utf8 s with - | Utf8Token (Unicode.Letter, _) -> LEFTQMARK - | AsciiChar | Utf8Token _ | EmptyStream -> - fst (process_chars bp '?' s) - -let blank_or_eof cs = - match Stream.peek cs with - | None -> true - | Some (' ' | '\t' | '\n' |'\r') -> true - | _ -> false - -(* Parse a token in a char stream *) - -let rec next_token = parser bp - | [< '' ' | '\t' | '\n' |'\r' as c; s >] -> - comm_loc bp; push_char c; next_token s - | [< ''$' as c; t = parse_after_special c bp >] ep -> - comment_stop bp; (t, (ep, bp)) - | [< ''.' as c; t = parse_after_special c bp; s >] ep -> - comment_stop bp; - (* We enforce that "." should either be part of a larger keyword, - for instance ".(", or followed by a blank or eof. *) - let () = match t with - | KEYWORD ("." | "...") -> - if not (blank_or_eof s) then err (bp,ep+1) Undefined_token; - between_com := true; - | _ -> () - in - (t, (bp,ep)) - | [< ' ('-'|'+'|'*' as c); s >] -> - let t,new_between_com = - if !between_com then process_sequence bp c s,true - else process_chars bp c s,false - in - comment_stop bp; between_com := new_between_com; t - | [< ''?'; s >] ep -> - let t = parse_after_qmark bp s in comment_stop bp; (t, (ep, bp)) - | [< ' ('a'..'z' | 'A'..'Z' | '_' as c); - len = ident_tail (store 0 c); s >] ep -> - let id = get_buff len in - comment_stop bp; - (try find_keyword id s with Not_found -> IDENT id), (bp, ep) - | [< ' ('0'..'9' as c); len = number (store 0 c) >] ep -> - comment_stop bp; - (INT (get_buff len), (bp, ep)) - | [< ''\"'; len = string None bp 0 >] ep -> - comment_stop bp; - (STRING (get_buff len), (bp, ep)) - | [< ' ('(' as c); - t = parser - | [< ''*'; s >] -> - comm_loc bp; - push_string "(*"; - comment bp s; - next_token s - | [< t = process_chars bp c >] -> comment_stop bp; t >] -> - t - | [< s >] -> - match lookup_utf8 s with - | Utf8Token (Unicode.Letter, n) -> - let len = ident_tail (nstore n 0 s) s in - let id = get_buff len in - let ep = Stream.count s in - comment_stop bp; - (try find_keyword id s with Not_found -> IDENT id), (bp, ep) - | AsciiChar | Utf8Token ((Unicode.Symbol | Unicode.IdentPart), _) -> - let t = process_chars bp (Stream.next s) s in - let new_between_com = match t with - (KEYWORD ("{"|"}"),_) -> !between_com | _ -> false in - comment_stop bp; between_com := new_between_com; t - | EmptyStream -> - comment_stop bp; (EOI, (bp, bp + 1)) - -(* (* Debug: uncomment this for tracing tokens seen by coq...*) -let next_token s = - let (t,(bp,ep)) = next_token s in Printf.eprintf "[%s]\n%!" (Tok.to_string t); - (t,(bp,ep)) -*) - -(* Location table system for creating tables associating a token count - to its location in a char stream (the source) *) - -let locerr () = invalid_arg "Lexer: location function" - -let loct_create () = Hashtbl.create 207 - -let loct_func loct i = - try Hashtbl.find loct i with Not_found -> locerr () - -let loct_add loct i loc = Hashtbl.add loct i loc - -let current_location_table = ref (loct_create ()) - -type location_table = (int, CompatLoc.t) Hashtbl.t -let location_table () = !current_location_table -let restore_location_table t = current_location_table := t - -(** {6 The lexer of Coq} *) - -(** Note: removing a token. - We do nothing because [remove_token] is called only when removing a grammar - rule with [Grammar.delete_rule]. The latter command is called only when - unfreezing the state of the grammar entries (see GRAMMAR summary, file - env/metasyntax.ml). Therefore, instead of removing tokens one by one, - we unfreeze the state of the lexer. This restores the behaviour of the - lexer. B.B. *) - -IFDEF CAMLP5 THEN - -type te = Tok.t - -(** Names of tokens, for this lexer, used in Grammar error messages *) - -let token_text = function - | ("", t) -> "'" ^ t ^ "'" - | ("IDENT", "") -> "identifier" - | ("IDENT", t) -> "'" ^ t ^ "'" - | ("INT", "") -> "integer" - | ("INT", s) -> "'" ^ s ^ "'" - | ("STRING", "") -> "string" - | ("EOI", "") -> "end of input" - | (con, "") -> con - | (con, prm) -> con ^ " \"" ^ prm ^ "\"" - -let func cs = - let loct = loct_create () in - let ts = - Stream.from - (fun i -> - let (tok, loc) = next_token cs in - loct_add loct i (make_loc loc); Some tok) - in - current_location_table := loct; - (ts, loct_func loct) - -let lexer = { - Token.tok_func = func; - Token.tok_using = - (fun pat -> match Tok.of_pattern pat with - | KEYWORD s -> add_keyword s - | _ -> ()); - Token.tok_removing = (fun _ -> ()); - Token.tok_match = Tok.match_pattern; - Token.tok_comm = None; - Token.tok_text = token_text } - -ELSE (* official camlp4 for ocaml >= 3.10 *) - -module M_ = Camlp4.ErrorHandler.Register (Error) - -module Loc = CompatLoc -module Token = struct - include Tok (* Cf. tok.ml *) - module Loc = CompatLoc - module Error = Camlp4.Struct.EmptyError - module Filter = struct - type token_filter = (Tok.t * Loc.t) Stream.t -> (Tok.t * Loc.t) Stream.t - type t = unit - let mk _is_kwd = () - let keyword_added () kwd _ = add_keyword kwd - let keyword_removed () _ = () - let filter () x = x - let define_filter () _ = () - end -end - -let mk () _init_loc(*FIXME*) cs = - let loct = loct_create () in - let rec self = - parser i - [< (tok, loc) = next_token; s >] -> - let loc = make_loc loc in - loct_add loct i loc; - [< '(tok, loc); self s >] - | [< >] -> [< >] - in current_location_table := loct; self cs - -END - -(** Terminal symbols interpretation *) - -let is_ident_not_keyword s = - is_ident s && not (is_keyword s) - -let is_number s = - let rec aux i = - Int.equal (String.length s) i || - match s.[i] with '0'..'9' -> aux (i+1) | _ -> false - in aux 0 - -let strip s = - let len = - let rec loop i len = - if Int.equal i (String.length s) then len - else if s.[i] == ' ' then loop (i + 1) len - else loop (i + 1) (len + 1) - in - loop 0 0 - in - if len == String.length s then s - else - let s' = String.create len in - let rec loop i i' = - if i == String.length s then s' - else if s.[i] == ' ' then loop (i + 1) i' - else begin s'.[i'] <- s.[i]; loop (i + 1) (i' + 1) end - in - loop 0 0 - -let terminal s = - let s = strip s in - let () = match s with "" -> Errors.error "empty token." | _ -> () in - if is_ident_not_keyword s then IDENT s - else if is_number s then INT s - else KEYWORD s diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli deleted file mode 100644 index 24b0ec8471..0000000000 --- a/parsing/cLexer.mli +++ /dev/null @@ -1,38 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* unit -val remove_keyword : string -> unit -val is_keyword : string -> bool - -(* val location_function : int -> Loc.t *) - -(** for coqdoc *) -type location_table -val location_table : unit -> location_table -val restore_location_table : location_table -> unit - -val check_ident : string -> unit -val is_ident : string -> bool -val check_keyword : string -> unit - -type frozen_t -val freeze : unit -> frozen_t -val unfreeze : frozen_t -> unit - -type com_state -val com_state: unit -> com_state -val restore_com_state: com_state -> unit - -val xml_output_comment : (string -> unit) Hook.t - -val terminal : string -> Tok.t - -(** The lexer of Coq: *) - -include Compat.LexerSig diff --git a/parsing/compat.ml4 b/parsing/compat.ml4 index 1481c31f45..17038ab5fc 100644 --- a/parsing/compat.ml4 +++ b/parsing/compat.ml4 @@ -135,7 +135,7 @@ let to_coq_position = function END -(** Signature of CLexer *) +(** Signature of Lexer *) IFDEF CAMLP5 THEN diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 4c77433038..b0bbdd8136 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -317,9 +317,9 @@ let recover_constr_grammar ntn prec = (* Summary functions: the state of the lexer is included in that of the parser. Because the grammar affects the set of keywords when adding or removing grammar rules. *) -type frozen_t = (int * all_grammar_command) list * CLexer.frozen_t +type frozen_t = (int * all_grammar_command) list * Lexer.frozen_t -let freeze _ : frozen_t = (!grammar_state, CLexer.freeze ()) +let freeze _ : frozen_t = (!grammar_state, Lexer.freeze ()) (* We compare the current state of the grammar and the state to unfreeze, by computing the longest common suffixes *) @@ -335,7 +335,7 @@ let unfreeze (grams, lex) = remove_grammars n; remove_levels n; grammar_state := common; - CLexer.unfreeze lex; + Lexer.unfreeze lex; List.iter extend_grammar (List.rev_map snd redo) (** No need to provide an init function : the grammar state is diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 73b088b467..5edb7b8082 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -29,7 +29,7 @@ let constr_kw = "Prop"; "Set"; "Type"; ".("; "_"; ".."; "`{"; "`("; "{|"; "|}" ] -let _ = List.iter CLexer.add_keyword constr_kw +let _ = List.iter Lexer.add_keyword constr_kw let mk_cast = function (c,(_,None)) -> c diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index 20fbccb2db..5297c163bc 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -15,7 +15,7 @@ open Pcoq open Pcoq.Prim let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "'"] -let _ = List.iter CLexer.add_keyword prim_kw +let _ = List.iter Lexer.add_keyword prim_kw let local_make_qualid l id = make_qualid (DirPath.make l) id diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 8f3d04eeb6..2a00a17640 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -25,7 +25,7 @@ open Pcoq let all_with delta = Redops.make_red_flag [FBeta;FIota;FZeta;delta] let tactic_kw = [ "->"; "<-" ; "by" ] -let _ = List.iter CLexer.add_keyword tactic_kw +let _ = List.iter Lexer.add_keyword tactic_kw let err () = raise Stream.Failure diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index b19ad8807e..f3766a7d79 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -27,7 +27,7 @@ open Pcoq.Vernac_ open Pcoq.Module let vernac_kw = [ ";"; ","; ">->"; ":<"; "<:"; "where"; "at" ] -let _ = List.iter CLexer.add_keyword vernac_kw +let _ = List.iter Lexer.add_keyword vernac_kw (* Rem: do not join the different GEXTEND into one, it breaks native *) (* compilation on PowerPC and Sun architectures *) diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 new file mode 100644 index 0000000000..5d96873f31 --- /dev/null +++ b/parsing/lexer.ml4 @@ -0,0 +1,695 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* char -> int = compare end +module CharMap = Map.Make (CharOrd) + +type ttree = { + node : string option; + branch : ttree CharMap.t } + +let empty_ttree = { node = None; branch = CharMap.empty } + +let ttree_add ttree str = + let rec insert tt i = + if i == String.length str then + {node = Some str; branch = tt.branch} + else + let c = str.[i] in + let br = + match try Some (CharMap.find c tt.branch) with Not_found -> None with + | Some tt' -> + CharMap.add c (insert tt' (i + 1)) (CharMap.remove c tt.branch) + | None -> + let tt' = {node = None; branch = CharMap.empty} in + CharMap.add c (insert tt' (i + 1)) tt.branch + in + { node = tt.node; branch = br } + in + insert ttree 0 + +(* Search a string in a dictionary: raises [Not_found] + if the word is not present. *) + +let ttree_find ttree str = + let rec proc_rec tt i = + if i == String.length str then tt + else proc_rec (CharMap.find str.[i] tt.branch) (i+1) + in + proc_rec ttree 0 + +(* Removes a string from a dictionary: returns an equal dictionary + if the word not present. *) +let ttree_remove ttree str = + let rec remove tt i = + if i == String.length str then + {node = None; branch = tt.branch} + else + let c = str.[i] in + let br = + match try Some (CharMap.find c tt.branch) with Not_found -> None with + | Some tt' -> + CharMap.add c (remove tt' (i + 1)) (CharMap.remove c tt.branch) + | None -> tt.branch + in + { node = tt.node; branch = br } + in + remove ttree 0 + + +(* Errors occurring while lexing (explained as "Lexer error: ...") *) + +module Error = struct + + type t = + | Illegal_character + | Unterminated_comment + | Unterminated_string + | Undefined_token + | Bad_token of string + | UnsupportedUnicode of int + + exception E of t + + let to_string x = + "Syntax Error: Lexer: " ^ + (match x with + | Illegal_character -> "Illegal character" + | Unterminated_comment -> "Unterminated comment" + | Unterminated_string -> "Unterminated string" + | Undefined_token -> "Undefined token" + | Bad_token tok -> Format.sprintf "Bad token %S" tok + | UnsupportedUnicode x -> + Printf.sprintf "Unsupported Unicode character (0x%x)" x) + + (* Require to fix the Camlp4 signature *) + let print ppf x = Pp.pp_with ppf (Pp.str (to_string x)) + +end +open Error + +let err loc str = Loc.raise (Loc.make_loc loc) (Error.E str) + +let bad_token str = raise (Error.E (Bad_token str)) + +(* Lexer conventions on tokens *) + +type token_kind = + | Utf8Token of (Unicode.status * int) + | AsciiChar + | EmptyStream + +let error_unsupported_unicode_character n unicode cs = + let bp = Stream.count cs in + err (bp,bp+n) (UnsupportedUnicode unicode) + +let error_utf8 cs = + let bp = Stream.count cs in + Stream.junk cs; (* consume the char to avoid read it and fail again *) + err (bp, bp+1) Illegal_character + +let utf8_char_size cs = function + (* Utf8 leading byte *) + | '\x00'..'\x7F' -> 1 + | '\xC0'..'\xDF' -> 2 + | '\xE0'..'\xEF' -> 3 + | '\xF0'..'\xF7' -> 4 + | _ (* '\x80'..\xBF'|'\xF8'..'\xFF' *) -> error_utf8 cs + +let njunk n = Util.repeat n Stream.junk + +let check_utf8_trailing_byte cs c = + if not (Int.equal (Char.code c land 0xC0) 0x80) then error_utf8 cs + +(* Recognize utf8 blocks (of length less than 4 bytes) *) +(* but don't certify full utf8 compliance (e.g. no emptyness check) *) +let lookup_utf8_tail c cs = + let c1 = Char.code c in + if Int.equal (c1 land 0x40) 0 || Int.equal (c1 land 0x38) 0x38 then error_utf8 cs + else + let n, unicode = + if Int.equal (c1 land 0x20) 0 then + match Stream.npeek 2 cs with + | [_;c2] -> + check_utf8_trailing_byte cs c2; + 2, (c1 land 0x1F) lsl 6 + (Char.code c2 land 0x3F) + | _ -> error_utf8 cs + else if Int.equal (c1 land 0x10) 0 then + match Stream.npeek 3 cs with + | [_;c2;c3] -> + check_utf8_trailing_byte cs c2; check_utf8_trailing_byte cs c3; + 3, (c1 land 0x0F) lsl 12 + (Char.code c2 land 0x3F) lsl 6 + + (Char.code c3 land 0x3F) + | _ -> error_utf8 cs + else match Stream.npeek 4 cs with + | [_;c2;c3;c4] -> + check_utf8_trailing_byte cs c2; check_utf8_trailing_byte cs c3; + check_utf8_trailing_byte cs c4; + 4, (c1 land 0x07) lsl 18 + (Char.code c2 land 0x3F) lsl 12 + + (Char.code c3 land 0x3F) lsl 6 + (Char.code c4 land 0x3F) + | _ -> error_utf8 cs + in + try Unicode.classify unicode, n + with Unicode.Unsupported -> + njunk n cs; error_unsupported_unicode_character n unicode cs + +let lookup_utf8 cs = + match Stream.peek cs with + | Some ('\x00'..'\x7F') -> AsciiChar + | Some ('\x80'..'\xFF' as c) -> Utf8Token (lookup_utf8_tail c cs) + | None -> EmptyStream + +let unlocated f x = f x + (** FIXME: should we still unloc the exception? *) +(* try f x with Loc.Exc_located (_, exc) -> raise exc *) + +let check_keyword str = + let rec loop_symb = parser + | [< ' (' ' | '\n' | '\r' | '\t' | '"') >] -> bad_token str + | [< s >] -> + match unlocated lookup_utf8 s with + | Utf8Token (_,n) -> njunk n s; loop_symb s + | AsciiChar -> Stream.junk s; loop_symb s + | EmptyStream -> () + in + loop_symb (Stream.of_string str) + +let check_keyword_to_add s = + try check_keyword s + with Error.E (UnsupportedUnicode unicode) -> + Flags.if_verbose msg_warning + (strbrk (Printf.sprintf "Token '%s' contains unicode character 0x%x \ + which will not be parsable." s unicode)) + +let check_ident str = + let rec loop_id intail = parser + | [< ' ('a'..'z' | 'A'..'Z' | '_'); s >] -> + loop_id true s + | [< ' ('0'..'9' | ''') when intail; s >] -> + loop_id true s + | [< s >] -> + match unlocated lookup_utf8 s with + | Utf8Token (Unicode.Letter, n) -> njunk n s; loop_id true s + | Utf8Token (Unicode.IdentPart, n) when intail -> + njunk n s; + loop_id true s + | EmptyStream -> () + | Utf8Token _ | AsciiChar -> bad_token str + in + loop_id false (Stream.of_string str) + +let is_ident str = + try let _ = check_ident str in true with Error.E _ -> false + +(* Keyword and symbol dictionary *) +let token_tree = ref empty_ttree + +let is_keyword s = + try match (ttree_find !token_tree s).node with None -> false | Some _ -> true + with Not_found -> false + +let add_keyword str = + if not (is_keyword str) then + begin + check_keyword_to_add str; + token_tree := ttree_add !token_tree str + end + +let remove_keyword str = + token_tree := ttree_remove !token_tree str + +(* Freeze and unfreeze the state of the lexer *) +type frozen_t = ttree + +let freeze () = !token_tree +let unfreeze tt = (token_tree := tt) + +(* The string buffering machinery *) + +let buff = ref (String.create 80) + +let store len x = + if len >= String.length !buff then + buff := !buff ^ String.create (String.length !buff); + !buff.[len] <- x; + succ len + +let rec nstore n len cs = + if n>0 then nstore (n-1) (store len (Stream.next cs)) cs else len + +let get_buff len = String.sub !buff 0 len + +(* The classical lexer: idents, numbers, quoted strings, comments *) + +let rec ident_tail len = parser + | [< ' ('a'..'z' | 'A'..'Z' | '0'..'9' | ''' | '_' as c); s >] -> + ident_tail (store len c) s + | [< s >] -> + match lookup_utf8 s with + | Utf8Token ((Unicode.IdentPart | Unicode.Letter), n) -> + ident_tail (nstore n len s) s + | _ -> len + +let rec number len = parser + | [< ' ('0'..'9' as c); s >] -> number (store len c) s + | [< >] -> len + +let rec string in_comments bp len = parser + | [< ''"'; esc=(parser [<''"' >] -> true | [< >] -> false); s >] -> + if esc then string in_comments bp (store len '"') s else len + | [< ''('; s >] -> + (parser + | [< ''*'; s >] -> + string + (Option.map succ in_comments) + bp (store (store len '(') '*') + s + | [< >] -> + string in_comments bp (store len '(') s) s + | [< ''*'; s >] -> + (parser + | [< '')'; s >] -> + let () = match in_comments with + | Some 0 -> + msg_warning + (strbrk + "Not interpreting \"*)\" as the end of current \ + non-terminated comment because it occurs in a \ + non-terminated string of the comment.") + | _ -> () + in + let in_comments = Option.map pred in_comments in + string in_comments bp (store (store len '*') ')') s + | [< >] -> + string in_comments bp (store len '*') s) s + | [< 'c; s >] -> string in_comments bp (store len c) s + | [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_string + +(* Hook for exporting comment into xml theory files *) +let (f_xml_output_comment, xml_output_comment) = Hook.make ~default:ignore () + +(* Utilities for comments in beautify *) +let comment_begin = ref None +let comm_loc bp = match !comment_begin with +| None -> comment_begin := Some bp +| _ -> () + +let current = Buffer.create 8192 +let between_com = ref true + +type com_state = int option * string * bool +let restore_com_state (o,s,b) = + comment_begin := o; + Buffer.clear current; Buffer.add_string current s; + between_com := b +let dflt_com = (None,"",true) +let com_state () = + let s = (!comment_begin, Buffer.contents current, !between_com) in + restore_com_state dflt_com; s + +let real_push_char c = Buffer.add_char current c + +(* Add a char if it is between two commands, if it is a newline or + if the last char is not a space itself. *) +let push_char c = + if + !between_com || List.mem c ['\n';'\r'] || + (List.mem c [' ';'\t']&& + (Int.equal (Buffer.length current) 0 || + not (let s = Buffer.contents current in + List.mem s.[String.length s - 1] [' ';'\t';'\n';'\r']))) + then + real_push_char c + +let push_string s = Buffer.add_string current s + +let null_comment s = + let rec null i = + i<0 || (List.mem s.[i] [' ';'\t';'\n';'\r'] && null (i-1)) in + null (String.length s - 1) + +let comment_stop ep = + let current_s = Buffer.contents current in + if !Flags.xml_export && Buffer.length current > 0 && + (!between_com || not(null_comment current_s)) then + Hook.get f_xml_output_comment current_s; + (if Flags.do_beautify() && Buffer.length current > 0 && + (!between_com || not(null_comment current_s)) then + let bp = match !comment_begin with + Some bp -> bp + | None -> + msgerrnl(str "No begin location for comment '" + ++ str current_s ++str"' ending at " + ++ int ep); + ep-1 in + Pp.comments := ((bp,ep),current_s) :: !Pp.comments); + Buffer.clear current; + comment_begin := None; + between_com := false + +(* Does not unescape!!! *) +let rec comm_string bp = parser + | [< ''"' >] -> push_string "\"" + | [< ''\\'; _ = + (parser [< ' ('"' | '\\' as c) >] -> + let () = match c with + | '"' -> real_push_char c + | _ -> () + in + real_push_char c + | [< >] -> real_push_char '\\'); s >] + -> comm_string bp s + | [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_string + | [< 'c; s >] -> real_push_char c; comm_string bp s + +let rec comment bp = parser bp2 + | [< ''('; + _ = (parser + | [< ''*'; s >] -> push_string "(*"; comment bp s + | [< >] -> push_string "(" ); + s >] -> comment bp s + | [< ''*'; + _ = parser + | [< '')' >] -> push_string "*)"; + | [< s >] -> real_push_char '*'; comment bp s >] -> () + | [< ''"'; s >] -> + if Flags.do_beautify() then (push_string"\"";comm_string bp2 s) + else ignore (string (Some 0) bp2 0 s); + comment bp s + | [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_comment + | [< 'z; s >] -> real_push_char z; comment bp s + +(* Parse a special token, using the [token_tree] *) + +(* Peek as much utf-8 lexemes as possible *) +(* and retain the longest valid special token obtained *) +let rec progress_further last nj tt cs = + try progress_from_byte last nj tt cs (List.nth (Stream.npeek (nj+1) cs) nj) + with Failure _ -> last + +and update_longest_valid_token last nj tt cs = + match tt.node with + | Some _ as last' -> + stream_njunk nj cs; + progress_further last' 0 tt cs + | None -> + progress_further last nj tt cs + +(* nj is the number of char peeked since last valid token *) +(* n the number of char in utf8 block *) +and progress_utf8 last nj n c tt cs = + try + let tt = CharMap.find c tt.branch in + if Int.equal n 1 then + update_longest_valid_token last (nj+n) tt cs + else + match Util.List.skipn (nj+1) (Stream.npeek (nj+n) cs) with + | l when Int.equal (List.length l) (n - 1) -> + List.iter (check_utf8_trailing_byte cs) l; + let tt = List.fold_left (fun tt c -> CharMap.find c tt.branch) tt l in + update_longest_valid_token last (nj+n) tt cs + | _ -> + error_utf8 cs + with Not_found -> + last + +and progress_from_byte last nj tt cs c = + progress_utf8 last nj (utf8_char_size cs c) c tt cs + +let find_keyword id s = + let tt = ttree_find !token_tree id in + match progress_further tt.node 0 tt s with + | None -> raise Not_found + | Some c -> KEYWORD c + +let process_sequence bp c cs = + let rec aux n cs = + match Stream.peek cs with + | Some c' when c == c' -> Stream.junk cs; aux (n+1) cs + | _ -> BULLET (String.make n c), (bp, Stream.count cs) + in + aux 1 cs + +(* Must be a special token *) +let process_chars bp c cs = + let t = progress_from_byte None (-1) !token_tree cs c in + let ep = Stream.count cs in + match t with + | Some t -> (KEYWORD t, (bp, ep)) + | None -> + let ep' = bp + utf8_char_size cs c in + njunk (ep' - ep) cs; + err (bp, ep') Undefined_token + +let token_of_special c s = match c with + | '$' -> METAIDENT s + | '.' -> FIELD s + | _ -> assert false + +(* Parse what follows a dot / a dollar *) + +let parse_after_special c bp = + parser + | [< ' ('a'..'z' | 'A'..'Z' | '_' as d); len = ident_tail (store 0 d) >] -> + token_of_special c (get_buff len) + | [< s >] -> + match lookup_utf8 s with + | Utf8Token (Unicode.Letter, n) -> + token_of_special c (get_buff (ident_tail (nstore n 0 s) s)) + | AsciiChar | Utf8Token _ | EmptyStream -> fst (process_chars bp c s) + +(* Parse what follows a question mark *) + +let parse_after_qmark bp s = + match Stream.peek s with + | Some ('a'..'z' | 'A'..'Z' | '_') -> LEFTQMARK + | None -> KEYWORD "?" + | _ -> + match lookup_utf8 s with + | Utf8Token (Unicode.Letter, _) -> LEFTQMARK + | AsciiChar | Utf8Token _ | EmptyStream -> + fst (process_chars bp '?' s) + +let blank_or_eof cs = + match Stream.peek cs with + | None -> true + | Some (' ' | '\t' | '\n' |'\r') -> true + | _ -> false + +(* Parse a token in a char stream *) + +let rec next_token = parser bp + | [< '' ' | '\t' | '\n' |'\r' as c; s >] -> + comm_loc bp; push_char c; next_token s + | [< ''$' as c; t = parse_after_special c bp >] ep -> + comment_stop bp; (t, (ep, bp)) + | [< ''.' as c; t = parse_after_special c bp; s >] ep -> + comment_stop bp; + (* We enforce that "." should either be part of a larger keyword, + for instance ".(", or followed by a blank or eof. *) + let () = match t with + | KEYWORD ("." | "...") -> + if not (blank_or_eof s) then err (bp,ep+1) Undefined_token; + between_com := true; + | _ -> () + in + (t, (bp,ep)) + | [< ' ('-'|'+'|'*' as c); s >] -> + let t,new_between_com = + if !between_com then process_sequence bp c s,true + else process_chars bp c s,false + in + comment_stop bp; between_com := new_between_com; t + | [< ''?'; s >] ep -> + let t = parse_after_qmark bp s in comment_stop bp; (t, (ep, bp)) + | [< ' ('a'..'z' | 'A'..'Z' | '_' as c); + len = ident_tail (store 0 c); s >] ep -> + let id = get_buff len in + comment_stop bp; + (try find_keyword id s with Not_found -> IDENT id), (bp, ep) + | [< ' ('0'..'9' as c); len = number (store 0 c) >] ep -> + comment_stop bp; + (INT (get_buff len), (bp, ep)) + | [< ''\"'; len = string None bp 0 >] ep -> + comment_stop bp; + (STRING (get_buff len), (bp, ep)) + | [< ' ('(' as c); + t = parser + | [< ''*'; s >] -> + comm_loc bp; + push_string "(*"; + comment bp s; + next_token s + | [< t = process_chars bp c >] -> comment_stop bp; t >] -> + t + | [< s >] -> + match lookup_utf8 s with + | Utf8Token (Unicode.Letter, n) -> + let len = ident_tail (nstore n 0 s) s in + let id = get_buff len in + let ep = Stream.count s in + comment_stop bp; + (try find_keyword id s with Not_found -> IDENT id), (bp, ep) + | AsciiChar | Utf8Token ((Unicode.Symbol | Unicode.IdentPart), _) -> + let t = process_chars bp (Stream.next s) s in + let new_between_com = match t with + (KEYWORD ("{"|"}"),_) -> !between_com | _ -> false in + comment_stop bp; between_com := new_between_com; t + | EmptyStream -> + comment_stop bp; (EOI, (bp, bp + 1)) + +(* (* Debug: uncomment this for tracing tokens seen by coq...*) +let next_token s = + let (t,(bp,ep)) = next_token s in Printf.eprintf "[%s]\n%!" (Tok.to_string t); + (t,(bp,ep)) +*) + +(* Location table system for creating tables associating a token count + to its location in a char stream (the source) *) + +let locerr () = invalid_arg "Lexer: location function" + +let loct_create () = Hashtbl.create 207 + +let loct_func loct i = + try Hashtbl.find loct i with Not_found -> locerr () + +let loct_add loct i loc = Hashtbl.add loct i loc + +let current_location_table = ref (loct_create ()) + +type location_table = (int, CompatLoc.t) Hashtbl.t +let location_table () = !current_location_table +let restore_location_table t = current_location_table := t + +(** {6 The lexer of Coq} *) + +(** Note: removing a token. + We do nothing because [remove_token] is called only when removing a grammar + rule with [Grammar.delete_rule]. The latter command is called only when + unfreezing the state of the grammar entries (see GRAMMAR summary, file + env/metasyntax.ml). Therefore, instead of removing tokens one by one, + we unfreeze the state of the lexer. This restores the behaviour of the + lexer. B.B. *) + +IFDEF CAMLP5 THEN + +type te = Tok.t + +(** Names of tokens, for this lexer, used in Grammar error messages *) + +let token_text = function + | ("", t) -> "'" ^ t ^ "'" + | ("IDENT", "") -> "identifier" + | ("IDENT", t) -> "'" ^ t ^ "'" + | ("INT", "") -> "integer" + | ("INT", s) -> "'" ^ s ^ "'" + | ("STRING", "") -> "string" + | ("EOI", "") -> "end of input" + | (con, "") -> con + | (con, prm) -> con ^ " \"" ^ prm ^ "\"" + +let func cs = + let loct = loct_create () in + let ts = + Stream.from + (fun i -> + let (tok, loc) = next_token cs in + loct_add loct i (make_loc loc); Some tok) + in + current_location_table := loct; + (ts, loct_func loct) + +let lexer = { + Token.tok_func = func; + Token.tok_using = + (fun pat -> match Tok.of_pattern pat with + | KEYWORD s -> add_keyword s + | _ -> ()); + Token.tok_removing = (fun _ -> ()); + Token.tok_match = Tok.match_pattern; + Token.tok_comm = None; + Token.tok_text = token_text } + +ELSE (* official camlp4 for ocaml >= 3.10 *) + +module M_ = Camlp4.ErrorHandler.Register (Error) + +module Loc = CompatLoc +module Token = struct + include Tok (* Cf. tok.ml *) + module Loc = CompatLoc + module Error = Camlp4.Struct.EmptyError + module Filter = struct + type token_filter = (Tok.t * Loc.t) Stream.t -> (Tok.t * Loc.t) Stream.t + type t = unit + let mk _is_kwd = () + let keyword_added () kwd _ = add_keyword kwd + let keyword_removed () _ = () + let filter () x = x + let define_filter () _ = () + end +end + +let mk () _init_loc(*FIXME*) cs = + let loct = loct_create () in + let rec self = + parser i + [< (tok, loc) = next_token; s >] -> + let loc = make_loc loc in + loct_add loct i loc; + [< '(tok, loc); self s >] + | [< >] -> [< >] + in current_location_table := loct; self cs + +END + +(** Terminal symbols interpretation *) + +let is_ident_not_keyword s = + is_ident s && not (is_keyword s) + +let is_number s = + let rec aux i = + Int.equal (String.length s) i || + match s.[i] with '0'..'9' -> aux (i+1) | _ -> false + in aux 0 + +let strip s = + let len = + let rec loop i len = + if Int.equal i (String.length s) then len + else if s.[i] == ' ' then loop (i + 1) len + else loop (i + 1) (len + 1) + in + loop 0 0 + in + if len == String.length s then s + else + let s' = String.create len in + let rec loop i i' = + if i == String.length s then s' + else if s.[i] == ' ' then loop (i + 1) i' + else begin s'.[i'] <- s.[i]; loop (i + 1) (i' + 1) end + in + loop 0 0 + +let terminal s = + let s = strip s in + let () = match s with "" -> Errors.error "empty token." | _ -> () in + if is_ident_not_keyword s then IDENT s + else if is_number s then INT s + else KEYWORD s diff --git a/parsing/lexer.mli b/parsing/lexer.mli new file mode 100644 index 0000000000..24b0ec8471 --- /dev/null +++ b/parsing/lexer.mli @@ -0,0 +1,38 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* unit +val remove_keyword : string -> unit +val is_keyword : string -> bool + +(* val location_function : int -> Loc.t *) + +(** for coqdoc *) +type location_table +val location_table : unit -> location_table +val restore_location_table : location_table -> unit + +val check_ident : string -> unit +val is_ident : string -> bool +val check_keyword : string -> unit + +type frozen_t +val freeze : unit -> frozen_t +val unfreeze : frozen_t -> unit + +type com_state +val com_state: unit -> com_state +val restore_com_state: com_state -> unit + +val xml_output_comment : (string -> unit) Hook.t + +val terminal : string -> Tok.t + +(** The lexer of Coq: *) + +include Compat.LexerSig diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib index 0e1c79c91b..a0cb831931 100644 --- a/parsing/parsing.mllib +++ b/parsing/parsing.mllib @@ -1,6 +1,6 @@ Tok Compat -CLexer +Lexer Pcoq Egramml Egramcoq diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index f01e25c616..28dc74e81b 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -18,7 +18,7 @@ open Tok (* necessary for camlp4 *) (** The parser of Coq *) -module G = GrammarMake (CLexer) +module G = GrammarMake (Lexer) (* TODO: this is a workaround, since there isn't such [warning_verbose] in new camlp4. In camlp5, this ref @@ -51,7 +51,7 @@ ELSE | tok -> Stoken ((=) tok, to_string tok) END -let gram_token_of_string s = gram_token_of_token (CLexer.terminal s) +let gram_token_of_string s = gram_token_of_token (Lexer.terminal s) let camlp4_verbosity silent f x = let a = !warning_verbose in diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index a7acdf7594..5ecc46d670 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -491,7 +491,7 @@ let interp_fresh_id ist env sigma l = String.concat "" (List.map (function | ArgArg s -> s | ArgVar (_,id) -> Id.to_string (interp_ident ist env sigma id)) l) in - let s = if CLexer.is_keyword s then s^"0" else s in + let s = if Lexer.is_keyword s then s^"0" else s in Id.of_string s in Tactics.fresh_id_in_env avoid id env diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index d8ee5d90da..600683d359 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -35,7 +35,7 @@ let explain_exn_default = function (* Basic interaction exceptions *) | Stream.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".") | Compat.Token.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".") - | CLexer.Error.E err -> hov 0 (str (CLexer.Error.to_string err)) + | Lexer.Error.E err -> hov 0 (str (Lexer.Error.to_string err)) | Sys_error msg -> hov 0 (str "System error: " ++ guill msg) | Out_of_memory -> hov 0 (str "Out of memory.") | Stack_overflow -> hov 0 (str "Stack overflow.") diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 040c339249..063ed89643 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -288,7 +288,7 @@ let rec discard_to_dot () = try Gram.entry_parse parse_to_dot top_buffer.tokens with - | Compat.Token.Error _ | CLexer.Error.E _ -> discard_to_dot () + | Compat.Token.Error _ | Lexer.Error.E _ -> discard_to_dot () | End_of_input -> raise End_of_input | e when Errors.noncritical e -> () diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 08b38a7037..9e1a76bbd6 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -230,11 +230,11 @@ let compile_files () = | [vf] -> compile_file vf (* One compilation : no need to save init state *) | l -> let init_state = States.freeze ~marshallable:`No in - let coqdoc_init_state = CLexer.location_table () in + let coqdoc_init_state = Lexer.location_table () in List.iter (fun vf -> States.unfreeze init_state; - CLexer.restore_location_table coqdoc_init_state; + Lexer.restore_location_table coqdoc_init_state; compile_file vf) (List.rev l) diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index c33726550d..2ccd27acb9 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -31,7 +31,7 @@ open Nameops (**********************************************************************) (* Tokens *) -let cache_token (_,s) = CLexer.add_keyword s +let cache_token (_,s) = Lexer.add_keyword s let inToken : string -> obj = declare_object {(default_object "TOKEN") with @@ -428,7 +428,7 @@ let rec interp_list_parser hd = function (* To protect alphabetic tokens and quotes from being seen as variables *) let quote_notation_token x = let n = String.length x in - let norm = CLexer.is_ident x in + let norm = Lexer.is_ident x in if (n > 0 && norm) || (n > 2 && x.[0] == '\'') then "'"^x^"'" else x @@ -436,7 +436,7 @@ let rec raw_analyze_notation_tokens = function | [] -> [] | String ".." :: sl -> NonTerminal ldots_var :: raw_analyze_notation_tokens sl | String "_" :: _ -> error "_ must be quoted." - | String x :: sl when CLexer.is_ident x -> + | String x :: sl when Lexer.is_ident x -> NonTerminal (Names.Id.of_string x) :: raw_analyze_notation_tokens sl | String s :: sl -> Terminal (String.drop_simple_quotes s) :: raw_analyze_notation_tokens sl @@ -725,7 +725,7 @@ let rec define_keywords_aux = function | GramConstrNonTerminal(e,Some _) as n1 :: GramConstrTerminal(IDENT k) :: l when is_not_small_constr e -> Flags.if_verbose msg_info (str "Identifier '" ++ str k ++ str "' now a keyword"); - CLexer.add_keyword k; + Lexer.add_keyword k; n1 :: GramConstrTerminal(KEYWORD k) :: define_keywords_aux l | n :: l -> n :: define_keywords_aux l | [] -> [] @@ -734,7 +734,7 @@ let rec define_keywords_aux = function let define_keywords = function | GramConstrTerminal(IDENT k)::l -> Flags.if_verbose msg_info (str "Identifier '" ++ str k ++ str "' now a keyword"); - CLexer.add_keyword k; + Lexer.add_keyword k; GramConstrTerminal(KEYWORD k) :: define_keywords_aux l | l -> define_keywords_aux l @@ -763,12 +763,12 @@ let make_production etyps symbols = let typ = List.assoc m etyps in distribute [GramConstrNonTerminal (typ, Some m)] ll | Terminal s -> - distribute [GramConstrTerminal (CLexer.terminal s)] ll + distribute [GramConstrTerminal (Lexer.terminal s)] ll | Break _ -> ll | SProdList (x,sl) -> let tkl = List.flatten - (List.map (function Terminal s -> [CLexer.terminal s] + (List.map (function Terminal s -> [Lexer.terminal s] | Break _ -> [] | _ -> anomaly (Pp.str "Found a non terminal token in recursive notation separator")) sl) in match List.assoc x etyps with diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index a5f502503b..7c4920dfb8 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -164,17 +164,17 @@ let save_translator_coqdoc () = (* translator state *) let ch = !chan_beautify in let cl = !Pp.comments in - let cs = CLexer.com_state() in + let cs = Lexer.com_state() in (* end translator state *) - let coqdocstate = CLexer.location_table () in + let coqdocstate = Lexer.location_table () in ch,cl,cs,coqdocstate let restore_translator_coqdoc (ch,cl,cs,coqdocstate) = if !Flags.beautify_file then close_out !chan_beautify; chan_beautify := ch; Pp.comments := cl; - CLexer.restore_com_state cs; - CLexer.restore_location_table coqdocstate + Lexer.restore_com_state cs; + Lexer.restore_location_table coqdocstate (* For coqtop -time, we display the position in the file, and a glimpse of the executed command *) -- cgit v1.2.3 From 4c66c7f9c370d2088dfa064e77f45b869c672e98 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 31 May 2016 15:35:46 +0200 Subject: Fix potential race condition in vm_compute. If the second allocation causes a collection of the minor heap, the first allocation will be freed, thus causing a memory corruption. Note: it only happens when computing the native projection of an opaque value while the minor heap is almost full. --- kernel/byterun/coq_interp.c | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index dc571699ef..d634b726bf 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -911,10 +911,12 @@ value coq_interprete Alloc_small(block, 2, ATOM_PROJ_TAG); Field(block, 0) = Field(coq_global_data, *pc); Field(block, 1) = accu; - /* Create accumulator */ - Alloc_small(accu, 2, Accu_tag); - Code_val(accu) = accumulate; - Field(accu, 1) = block; + accu = block; + /* Create accumulator */ + Alloc_small(block, 2, Accu_tag); + Code_val(block) = accumulate; + Field(block, 1) = accu; + accu = block; } else { accu = Field(accu, *pc++); } -- cgit v1.2.3