From 7cfb1c359faf13cd55bd92cba21fb00ca8d2d0d2 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 26 Sep 2015 19:08:11 +0200 Subject: Adding a notion of monotonous evarmap. --- engine/sigma.ml | 83 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 83 insertions(+) create mode 100644 engine/sigma.ml (limited to 'engine/sigma.ml') diff --git a/engine/sigma.ml b/engine/sigma.ml new file mode 100644 index 0000000000..e6189e29ce --- /dev/null +++ b/engine/sigma.ml @@ -0,0 +1,83 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* ) = fun _ _ -> () + +type ('a, 'r) sigma = Sigma : 'a * 's t * ('r, 's) le -> ('a, 'r) sigma + +type 'a evar = Evar.t + +let lift_evar evk () = evk + +let to_evar_map evd = evd +let to_evar evk = evk + +(** API *) + +type 'r fresh = Fresh : 's evar * 's t * ('r, 's) le -> 'r fresh + +let new_evar sigma ?naming info = + let (sigma, evk) = Evd.new_evar sigma ?naming info in + Fresh (evk, sigma, ()) + +let define evk c sigma = + Sigma ((), Evd.define evk c sigma, ()) + +(** Run *) + +type 'a run = { run : 'r. 'r t -> ('a, 'r) sigma } + +let run sigma f : 'a * Evd.evar_map = + let Sigma (x, sigma, ()) = f.run sigma in + (x, sigma) + +(** Monotonic references *) + +type evdref = Evd.evar_map ref + +let apply evdref f = + let Sigma (x, sigma, ()) = f.run !evdref in + evdref := sigma; + x + +let purify f = + let f (sigma : Evd.evar_map) = + let evdref = ref sigma in + let ans = f evdref in + Sigma (ans, !evdref, ()) + in + { run = f } + +(** Unsafe primitives *) + +module Unsafe = +struct + +let le = () +let of_evar_map sigma = sigma +let of_evar evk = evk +let of_ref ref = ref +let of_pair (x, sigma) = Sigma (x, sigma, ()) + +end + +module Notations = +struct + type ('a, 'r) sigma_ = ('a, 'r) sigma = + Sigma : 'a * 's t * ('r, 's) le -> ('a, 'r) sigma_ + + let (+>) = fun _ _ -> () + + type 'a run_ = 'a run = { run : 'r. 'r t -> ('a, 'r) sigma } +end -- cgit v1.2.3 From 94502de7ecf7db3830b2e419f43627fa2c8c1c87 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 19 Oct 2015 18:47:50 +0200 Subject: Removing some unsafe uses of monotonicity. --- engine/sigma.ml | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'engine/sigma.ml') diff --git a/engine/sigma.ml b/engine/sigma.ml index e6189e29ce..e3e83b6024 100644 --- a/engine/sigma.ml +++ b/engine/sigma.ml @@ -23,6 +23,8 @@ let lift_evar evk () = evk let to_evar_map evd = evd let to_evar evk = evk +let here x s = Sigma (x, s, ()) + (** API *) type 'r fresh = Fresh : 's evar * 's t * ('r, 's) le -> 'r fresh @@ -34,6 +36,14 @@ let new_evar sigma ?naming info = let define evk c sigma = Sigma ((), Evd.define evk c sigma, ()) +let fresh_constructor_instance env sigma pc = + let (sigma, c) = Evd.fresh_constructor_instance env sigma pc in + Sigma (c, sigma, ()) + +let fresh_global ?rigid ?names env sigma r = + let (sigma, c) = Evd.fresh_global ?rigid ?names env sigma r in + Sigma (c, sigma, ()) + (** Run *) type 'a run = { run : 'r. 'r t -> ('a, 'r) sigma } -- cgit v1.2.3 From f02f64a21863ce03f2da4ff04cd003051f96801f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 29 Oct 2015 18:18:43 +0100 Subject: Removing some goal unsafeness in inductive schemes. --- engine/sigma.ml | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'engine/sigma.ml') diff --git a/engine/sigma.ml b/engine/sigma.ml index e3e83b6024..e886b0d1e7 100644 --- a/engine/sigma.ml +++ b/engine/sigma.ml @@ -36,6 +36,18 @@ let new_evar sigma ?naming info = let define evk c sigma = Sigma ((), Evd.define evk c sigma, ()) +let fresh_sort_in_family ?rigid env sigma s = + let (sigma, s) = Evd.fresh_sort_in_family ?rigid env sigma s in + Sigma (s, sigma, ()) + +let fresh_constant_instance env sigma cst = + let (sigma, cst) = Evd.fresh_constant_instance env sigma cst in + Sigma (cst, sigma, ()) + +let fresh_inductive_instance env sigma ind = + let (sigma, ind) = Evd.fresh_inductive_instance env sigma ind in + Sigma (ind, sigma, ()) + let fresh_constructor_instance env sigma pc = let (sigma, c) = Evd.fresh_constructor_instance env sigma pc in Sigma (c, sigma, ()) -- cgit v1.2.3 From 968dfdb15cc11d48783017b2a91147b25c854ad6 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 1 Dec 2015 19:45:01 +0100 Subject: Monotonizing the Evarutil module. Some functions were left in the old paradigm because they are only used by the unification algorithms, so they are not worthwhile to change for now. --- engine/sigma.ml | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'engine/sigma.ml') diff --git a/engine/sigma.ml b/engine/sigma.ml index e886b0d1e7..c25aac0c14 100644 --- a/engine/sigma.ml +++ b/engine/sigma.ml @@ -36,6 +36,18 @@ let new_evar sigma ?naming info = let define evk c sigma = Sigma ((), Evd.define evk c sigma, ()) +let new_univ_level_variable ?name ?predicative rigid sigma = + let (sigma, u) = Evd.new_univ_level_variable ?name ?predicative rigid sigma in + Sigma (u, sigma, ()) + +let new_univ_variable ?name ?predicative rigid sigma = + let (sigma, u) = Evd.new_univ_variable ?name ?predicative rigid sigma in + Sigma (u, sigma, ()) + +let new_sort_variable ?name ?predicative rigid sigma = + let (sigma, u) = Evd.new_sort_variable ?name ?predicative rigid sigma in + Sigma (u, sigma, ()) + let fresh_sort_in_family ?rigid env sigma s = let (sigma, s) = Evd.fresh_sort_in_family ?rigid env sigma s in Sigma (s, sigma, ()) -- cgit v1.2.3 From 8d0ff142913fc6351ff7f0a6b8eacc6c21d36000 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 19 Feb 2016 15:12:53 +0100 Subject: Allowing to attach location to universes in UState. --- engine/sigma.ml | 32 ++++++++++++++++---------------- 1 file changed, 16 insertions(+), 16 deletions(-) (limited to 'engine/sigma.ml') diff --git a/engine/sigma.ml b/engine/sigma.ml index c25aac0c14..c7b0bb5a50 100644 --- a/engine/sigma.ml +++ b/engine/sigma.ml @@ -36,36 +36,36 @@ let new_evar sigma ?naming info = let define evk c sigma = Sigma ((), Evd.define evk c sigma, ()) -let new_univ_level_variable ?name ?predicative rigid sigma = - let (sigma, u) = Evd.new_univ_level_variable ?name ?predicative rigid sigma in +let new_univ_level_variable ?loc ?name ?predicative rigid sigma = + let (sigma, u) = Evd.new_univ_level_variable ?loc ?name ?predicative rigid sigma in Sigma (u, sigma, ()) -let new_univ_variable ?name ?predicative rigid sigma = - let (sigma, u) = Evd.new_univ_variable ?name ?predicative rigid sigma in +let new_univ_variable ?loc ?name ?predicative rigid sigma = + let (sigma, u) = Evd.new_univ_variable ?loc ?name ?predicative rigid sigma in Sigma (u, sigma, ()) -let new_sort_variable ?name ?predicative rigid sigma = - let (sigma, u) = Evd.new_sort_variable ?name ?predicative rigid sigma in +let new_sort_variable ?loc ?name ?predicative rigid sigma = + let (sigma, u) = Evd.new_sort_variable ?loc ?name ?predicative rigid sigma in Sigma (u, sigma, ()) -let fresh_sort_in_family ?rigid env sigma s = - let (sigma, s) = Evd.fresh_sort_in_family ?rigid env sigma s in +let fresh_sort_in_family ?loc ?rigid env sigma s = + let (sigma, s) = Evd.fresh_sort_in_family ?loc ?rigid env sigma s in Sigma (s, sigma, ()) -let fresh_constant_instance env sigma cst = - let (sigma, cst) = Evd.fresh_constant_instance env sigma cst in +let fresh_constant_instance ?loc env sigma cst = + let (sigma, cst) = Evd.fresh_constant_instance ?loc env sigma cst in Sigma (cst, sigma, ()) -let fresh_inductive_instance env sigma ind = - let (sigma, ind) = Evd.fresh_inductive_instance env sigma ind in +let fresh_inductive_instance ?loc env sigma ind = + let (sigma, ind) = Evd.fresh_inductive_instance ?loc env sigma ind in Sigma (ind, sigma, ()) -let fresh_constructor_instance env sigma pc = - let (sigma, c) = Evd.fresh_constructor_instance env sigma pc in +let fresh_constructor_instance ?loc env sigma pc = + let (sigma, c) = Evd.fresh_constructor_instance ?loc env sigma pc in Sigma (c, sigma, ()) -let fresh_global ?rigid ?names env sigma r = - let (sigma, c) = Evd.fresh_global ?rigid ?names env sigma r in +let fresh_global ?loc ?rigid ?names env sigma r = + let (sigma, c) = Evd.fresh_global ?loc ?rigid ?names env sigma r in Sigma (c, sigma, ()) (** Run *) -- cgit v1.2.3