diff options
| -rw-r--r-- | lib/future.ml | 2 | ||||
| -rw-r--r-- | lib/future.mli | 3 | ||||
| -rw-r--r-- | library/declare.ml | 13 |
3 files changed, 13 insertions, 5 deletions
diff --git a/lib/future.ml b/lib/future.ml index 690255edd..77386a1a9 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -90,6 +90,8 @@ let uuid kx = let id, _, _ = get kx in id let from_val ?(fix_exn=id) v = create fix_exn (Val (v, None)) let from_here ?(fix_exn=id) v = create fix_exn (Val (v, Some (!freeze ()))) +let fix_exn_of ck = let _, fix_exn, _ = get ck in fix_exn + let default_force () = raise NotReady let assignement ck = fun v -> let _, fix_exn, c = get ck in diff --git a/lib/future.mli b/lib/future.mli index 09d18ff26..b4eced06a 100644 --- a/lib/future.mli +++ b/lib/future.mli @@ -84,6 +84,9 @@ val from_val : ?fix_exn:fix_exn -> 'a -> 'a computation the value is not just the 'a but also the global system state *) val from_here : ?fix_exn:fix_exn -> 'a -> 'a computation +(* To get the fix_exn of a computation *) +val fix_exn_of : 'a computation -> fix_exn + (* Run remotely, returns the function to assign. Optionally tekes a function that is called when forced. The default one is to raise NotReady. The assignement function does not change the uuid. *) diff --git a/library/declare.ml b/library/declare.ml index e92225637..4364461ef 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -208,7 +208,7 @@ let definition_entry ?(opaque=false) ?(inline=false) ?types let declare_scheme = ref (fun _ _ -> assert false) let set_declare_scheme f = declare_scheme := f -let declare_sideff se = +let declare_sideff fix_exn se = let cbl, scheme = match se with | SEsubproof (c, cb) -> [c, cb], None | SEscheme (cbl, k) -> @@ -229,7 +229,7 @@ let declare_sideff se = let pt, opaque = pt_opaque_of cb in let ty = ty_of cb in { cst_decl = ConstantEntry (DefinitionEntry { - const_entry_body = Future.from_here (pt, Declareops.no_seff); + const_entry_body = Future.from_here ~fix_exn (pt, Declareops.no_seff); const_entry_secctx = Some cb.Declarations.const_hyps; const_entry_type = ty; const_entry_opaque = opaque; @@ -259,12 +259,15 @@ let declare_constant ?(internal = UserVerbose) ?(local = false) id (cd, kind) = | Entries.DefinitionEntry ({ const_entry_polymorphic = true; const_entry_body = bo } as de) -> - let pt, seff = Future.force bo in + let _, seff = Future.force bo in if Declareops.side_effects_is_empty seff then cd else begin - Declareops.iter_side_effects declare_sideff seff; + let seff = Declareops.uniquize_side_effects seff in + Declareops.iter_side_effects + (declare_sideff (Future.fix_exn_of bo)) seff; Entries.DefinitionEntry { de with - const_entry_body = Future.from_val (pt, Declareops.no_seff) } + const_entry_body = Future.chain ~pure:true bo (fun (pt, _) -> + pt, Declareops.no_seff) } end | _ -> cd in |