Adapt universe polymorphic branch to new handling of futures for delayed proofs.

5 files changed, 50 insertions, 282 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 1b329dbc4b..22262036e7 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -36,8 +36,8 @@ let start_proof (id : Id.t) str hyps c ?init_tac terminator =
 
 let cook_this_proof p =
   match p with
-  | { Proof_global.id;entries=[constr];persistence;constraints } ->
-      (id,(constr,constraints,persistence))
+  | { Proof_global.id;entries=[constr];persistence;universes } ->
+      (id,(constr,universes,persistence))
   | _ -> Errors.anomaly ~label:"Pfedit.cook_proof" (Pp.str "more than one proof term.")
 
 let cook_proof () =
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index b99bbe8723..3efc644e02 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -69,11 +69,11 @@ val start_proof :
 val cook_this_proof :
     Proof_global.proof_object ->
   (Id.t *
-    (Entries.definition_entry * Univ.constraints * goal_kind))
+    (Entries.definition_entry * Proof_global.proof_universes * goal_kind))
 
 val cook_proof : unit ->
   (Id.t *
-    (Entries.definition_entry * Univ.constraints * goal_kind))
+    (Entries.definition_entry * Proof_global.proof_universes * goal_kind))
 
 (** {6 ... } *)
 (** [get_pftreestate ()] returns the current focused pending proof.
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 29810eb9ac..9be159640b 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -63,12 +63,14 @@ let _ =
 
 (* Extra info on proofs. *)
 type lemma_possible_guards = int list list
+type proof_universes = Universes.universe_opt_subst Univ.in_universe_context
 
 type proof_object = {
   id : Names.Id.t;
   entries : Entries.definition_entry list;
   persistence : Decl_kinds.goal_kind;
-  constraints : Univ.constraints;
+  universes: proof_universes;
+  (* constraints : Univ.constraints; *)
 }
 
 type proof_ending =
@@ -79,10 +81,6 @@ type proof_ending =
 type proof_terminator = proof_ending -> unit
 type closed_proof = proof_object * proof_terminator
 
-type 'a proof_decl_hook =
-  Universes.universe_opt_subst Univ.in_universe_context -> 
-  Decl_kinds.locality -> Globnames.global_reference -> 'a
-
 type pstate = {
   pid : Id.t;
   terminator : proof_terminator Ephemeron.key;
@@ -266,65 +264,52 @@ let get_open_goals () =
     (List.map (fun (l1,l2) -> List.length l1 + List.length l2) gll) +
     List.length shelf
 
+let nf_body nf b =
+  let aux (c, t) = (nf c, t) in
+    Future.chain ~pure:true b aux
+
 let close_proof ?feedback_id ~now fpl =
   let { pid; section_vars; strength; proof; terminator } = cur_pstate () in
   let poly = pi2 strength (* Polymorphic *) in
   let initial_goals = Proof.initial_goals proof in
   let fpl, univs = Future.split2 fpl in
-  let () = if poly || now then ignore (Future.compute univs) in
-  let entries = Future.map2 (fun p (c, (t, octx)) ->
-    let compute_univs (usubst, uctx) = 
-      let nf x = Universes.nf_evars_and_universes_opt_subst (fun _ -> None) usubst x in
-      let compute_c_t (c, eff) =
-	let c, t = 
-	  if not now then nf c, nf t
-	  else (* Already normalized below *) c, nf t 
-	in
-	let univs =
-	  Univ.LSet.union (Universes.universes_of_constr c)
-	    (Universes.universes_of_constr t)
-	in
-	let ctx, subst = 
-	  Universes.simplify_universe_context (Univ.ContextSet.of_context uctx) univs 
-	in
-	let nf x = Vars.subst_univs_level_constr subst x in
-	  (nf c, eff), nf t, Univ.ContextSet.to_context ctx
-      in
-        Future.chain ~pure:true p compute_c_t
-    in
-    let ans = Future.chain ~pure:true univs compute_univs in
-    let ans = Future.join ans in
-    let p = Future.chain ~pure:true ans (fun (x, _, _) -> x) in
-    let t = Future.chain ~pure:true ans (fun (_, x, _) -> x) in
-    let univs = Future.chain ~pure:true ans (fun (_, _, x) -> x) in
-    let t = Future.force t in
-      { Entries.
-	const_entry_body = p;
-	const_entry_secctx = section_vars;
-	const_entry_type  = Some t;
-	const_entry_inline_code = false;
-	const_entry_opaque = true;
-	const_entry_universes = univs;
-        const_entry_feedback = None;
-	const_entry_polymorphic = pi2 strength;
-	const_entry_proj = None}) fpl initial_goals in
-  let globaluctx = 
-    if not poly then
-      List.fold_left (fun acc (c, (t, octx)) -> 
-	Univ.ContextSet.union octx acc)
-	Univ.ContextSet.empty initial_goals
-    else Univ.ContextSet.empty
-  in
-  let _ = 
+  let (subst, univs as univsubst), nf = 
     if poly || now then
-      List.iter (fun x -> ignore(Future.compute x.Entries.const_entry_body)) entries
+      let usubst, uctx = Future.force univs in
+      let ctx, subst = 
+	Universes.simplify_universe_context (Univ.ContextSet.of_context uctx) 
+      in
+      let nf x = 
+	let nf x = Universes.nf_evars_and_universes_opt_subst (fun _ -> None) usubst x in
+	  Vars.subst_univs_level_constr subst (nf x)
+      in
+      let subst = 
+	Univ.LMap.union usubst (Univ.LMap.map (fun v -> Some (Univ.Universe.make v)) subst)
+      in
+	(subst, Univ.ContextSet.to_context ctx), nf
+    else
+      let ctx = 
+	List.fold_left (fun acc (c, (t, octx)) -> 
+	  Univ.ContextSet.union octx acc)
+	  Univ.ContextSet.empty initial_goals
+      in
+	(Univ.LMap.empty, Univ.ContextSet.to_context ctx), (fun x -> x)
   in
-(*  let hook = Option.map (fun f -> 
-    if poly || now then f (Future.join univs) 
-    else f (Univ.LMap.empty,Univ.UContext.empty))
-    hook
-  in*) (* FIXME *)
-  { id = pid; entries = entries; persistence = strength; constraints = Univ.ContextSet.constraints globaluctx },
+  let entries =
+    Future.map2 (fun p (c, (t, octx)) -> { Entries.
+      const_entry_body = nf_body nf p;
+      const_entry_secctx = section_vars;
+      const_entry_feedback = feedback_id;
+      const_entry_type  = Some (nf t);
+      const_entry_inline_code = false;
+      const_entry_opaque = true;
+      const_entry_universes = univs;
+      const_entry_polymorphic = poly;
+      const_entry_proj = None})
+    fpl initial_goals in
+  if now then
+    List.iter (fun x ->ignore(Future.force x.Entries.const_entry_body)) entries;
+  { id = pid; entries = entries; persistence = strength; universes = univsubst },
   Ephemeron.get terminator
 
 type closed_proof_output = Entries.proof_output list * 
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 6c11ee9b48..1ad1cebf8c 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -46,10 +46,6 @@ exception NoCurrentProof
 val give_me_the_proof : unit -> Proof.proof
 (** @raise NoCurrentProof when outside proof mode. *)
 
-type 'a proof_decl_hook =
-  Universes.universe_opt_subst Univ.in_universe_context -> 
-  Decl_kinds.locality -> Globnames.global_reference -> 'a
-
 (** When a proof is closed, it is reified into a [proof_object], where
     [id] is the name of the proof, [entries] the list of the proof terms
     (in a form suitable for definitions). Together with the [terminator]
@@ -57,11 +53,13 @@ type 'a proof_decl_hook =
     (i.e. an proof ending command) and registers the appropriate
     values. *)
 type lemma_possible_guards = int list list
+type proof_universes = Universes.universe_opt_subst Univ.in_universe_context
 type proof_object = {
   id : Names.Id.t;
   entries : Entries.definition_entry list;
   persistence : Decl_kinds.goal_kind;
-  constraints : Univ.constraints;
+  universes: proof_universes;
+  (* constraints : Univ.constraints; *)
   (** guards : lemma_possible_guards; *)
 }
 
diff --git a/proofs/proofview_monad.ml b/proofs/proofview_monad.ml
index f6ba5341ee..ebbb040877 100644
--- a/proofs/proofview_monad.ml
+++ b/proofs/proofview_monad.ml
@@ -1,216 +1 @@
-module NonLogical =
-struct
-type 'a t = unit -> 'a
-
-type 'a ref = 'a Pervasives.ref
-
-let ret = fun a -> (); fun () -> a
-
-let bind = fun a k -> (); fun () -> k (a ()) ()
-
-let ignore = fun a -> (); fun () -> ignore (a ())
-
-let seq = fun a k -> (); fun () -> a (); k ()
-
-let new_ref = fun a -> (); fun () -> Pervasives.ref a
-
-let set = fun r a -> (); fun () -> Pervasives.(:=) r a
-
-let get = fun r -> (); fun () -> Pervasives.(!) r
-
-let raise = fun e -> (); fun () -> raise (Proof_errors.Exception e)
-
-let catch = fun s h -> (); fun () -> try s () with Proof_errors.Exception e -> h e ()
-
-let read_line = fun () -> try Pervasives.read_line () with e -> raise e ()
-
-let print_char = fun c -> (); fun () -> print_char c
-
-let print = fun s -> (); fun () -> try Pp.pp s; Pp.pp_flush () with e -> raise e ()
-
-let timeout = fun n t -> (); fun () ->
-  let timeout_handler _ = Pervasives.raise (Proof_errors.Exception Proof_errors.Timeout) in
-  let psh = Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in
-  Pervasives.ignore (Unix.alarm n);
-  let restore_timeout () =
-    Pervasives.ignore (Unix.alarm 0);
-    Sys.set_signal Sys.sigalrm psh
-  in
-  try
-    let res = t () in
-    restore_timeout ();
-    res
-  with
-  | e -> restore_timeout (); Pervasives.raise e
-
-let run = fun x -> try x () with Proof_errors.Exception e -> Pervasives.raise e
-
-end
-
-
-type ('a, 'b) list_view =
-| Nil of exn
-| Cons of 'a * 'b
-
-type proofview = { initial : (Term.constr*Term.types) list; solution : Evd.evar_map; comb : Goal.goal list }
-
-type logicalState = proofview
-
-type logicalMessageType = bool * (Goal.goal list * Goal.goal list)
-
-type logicalEnvironment = Environ.env
-
-type message = logicalMessageType
-type environment = logicalEnvironment
-type state = logicalState
-
-module Logical =
-struct
-
-type 'a ioT = 'a NonLogical.t
-
-type 'a logicT = { logic : 'r. ('a -> (exn -> 'r ioT) -> 'r ioT) -> (exn -> 'r ioT) -> 'r ioT }
-
-type 'a writerT = { writer : 'r. ('a -> message -> 'r logicT) -> 'r logicT }
-
-type 'a readerT = { reader : 'r. ('a -> 'r writerT) -> environment -> 'r writerT }
-
-type 'a stateT = { state : 'r. ('a -> state -> 'r readerT) -> state -> 'r readerT }
-
-type 'a t = 'a stateT
-
-let empty_message = (true, ([], []))
-
-let ret x = { state = fun k s -> k x s }
-
-let bind m f = { state = fun k s -> m.state (fun x s -> (f x).state k s) s }
-
-let ignore m = { state = fun k s -> m.state (fun _ s -> k () s) s }
-
-let seq m n =
-  { state = fun k s -> m.state (fun () s -> n.state k s) s }
-
-let set s =
-  { state = fun k _ -> k () s }
-
-let get = { state = fun k s -> k s s }
-
-let current = { state = fun k s -> { reader = fun kr e -> (k e s).reader kr e } }
-
-let join (b1, (l1, r1)) (b2, (l2, r2)) =
-  (b1 && b2, (List.append l1 l2, List.append r1 r2))
-
-let put msg =
-  { state = fun k s ->
-    let m = k () s in
-    { reader = fun kr e ->
-      let m = m.reader kr e in
-      { writer = fun kw -> m.writer
-        (fun x nmsg -> kw x (join msg nmsg))
-      }
-    }
-  }
-
-let zero err =
-  { state = fun k s ->
-    { reader = fun kr e ->
-      { writer = fun kw ->
-        { logic = fun sk fk -> fk err }
-      }
-    }
-  }
-
-let plus m f =
-  { state = fun k s ->
-    let m = m.state k s in
-    { reader = fun kr e ->
-      let m = m.reader kr e in
-      { writer = fun kw ->
-        let m = m.writer kw in
-        { logic = fun sk fk ->
-          let plus_fk err = ((((f err).state k s).reader kr e).writer kw).logic sk fk in
-          m.logic sk plus_fk
-        }
-      }
-    }
-  }
-
-let srun_state x s = { reader = fun kr _ -> kr (x, s) }
-let srun_reader x = { writer = fun kw -> kw x empty_message }
-let srun_writer x msg = { logic = fun sk fk -> sk (x, msg) fk }
-
-let srun_logic_sk x fk =
-  let next err =
-    let ans = fk err in { logic = fun sk fk ->
-    NonLogical.bind ans (function
-    | Nil err -> fk err
-    | Cons (y, n) -> sk x (fun err -> (n err).logic sk fk))
-  } in
-  let ans = Cons (x, next) in
-  NonLogical.ret ans
-
-let srun_logic_fk err = NonLogical.ret (Nil err)
-
-let split_next k s kr e kw sk fk = (); function
-| Nil _ as x ->
-  let m = k x s in
-  let m = m.reader kr e in
-  let m = m.writer kw in
-  m.logic sk fk
-| Cons (((x, s), msg), next) ->
-  let next err =
-    let next = next err in {
-    state = fun k s -> {
-      reader = fun kr e -> {
-        writer = fun kw -> {
-          logic = fun sk fk ->
-            let sk ((x, s), msg) fk =
-              let kw x nmsg = kw x (join msg nmsg) in
-              (((k x s).reader kr e).writer kw).logic sk fk
-            in
-            next.logic sk fk
-        }
-      }
-    }
-  } in
-  let m = k (Cons (x, next)) s in
-  let m = m.reader kr e in
-  let m = m.writer (fun x nmsg -> kw x (join msg nmsg)) in
-  m.logic sk fk
-
-let split m =
-  { state = fun k s ->
-    let m = m.state srun_state s in
-    { reader = fun kr e ->
-      let m = m.reader srun_reader e in
-      { writer = fun kw ->
-        let m = m.writer srun_writer in
-        { logic = fun sk fk ->
-          let m = m.logic srun_logic_sk srun_logic_fk in
-          NonLogical.bind m (split_next k s kr e kw sk fk)
-        }
-      }
-    }
-  }
-
-let lift m =
-  { state = fun k s ->
-    { reader = fun kr e ->
-      { writer = fun kw ->
-        { logic = fun sk fk ->
-          let lift x = (((k x s).reader kr e).writer kw).logic sk fk in
-          NonLogical.bind m lift
-        }
-      }
-    }
-  }
-
-let run m e s =
-  let m = m.state srun_state s in
-  let m = m.reader srun_reader e in
-  let m = m.writer srun_writer in
-  let run_fk err = NonLogical.raise (Proof_errors.TacticFailure err) in
-  let run_sk x _ = NonLogical.ret x in
-  m.logic run_sk run_fk
-
-end
+include Proofview_gen