From 54788df72ce79998ee27db362401a56bda4daceb Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 15 Mar 2020 17:52:16 -0400
Subject: [obligations] Functionalize Program state

In our quest to unify all the declaration paths, an important step
is to account for the state pertaining to `Program` declarations.

Whereas regular proofs keep are kept in a stack-like structure;
obligations for constants defined by `Program` are stored in a global
map which is manipulated by almost regular open/close proof primitives.

We make this manipulation explicit by handling the program state
functionally, in a similar way than we already do for lemmas.

This requires to extend the proof DSL a bit; but IMO changes are
acceptable given the gain.

Most of the PR is routine; only remarkable change is that the hook is
called explicitly in `finish_admitted` as it had to learn about the
different types of proof_endings.

Note that we could have gone deeper and use the type system to refine
the core proof type; IMO it is still too preliminary so it is better
to do this step as an intermediate one towards a deeper unification.
---
 vernac/comProgramFixpoint.ml | 29 ++++++++++++++---------------
 1 file changed, 14 insertions(+), 15 deletions(-)

(limited to 'vernac/comProgramFixpoint.ml')

diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 37615fa09c..55901fd604 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -109,7 +109,7 @@ let telescope env sigma l =
 let nf_evar_context sigma ctx =
   List.map (map_constr (fun c -> Evarutil.nf_evar sigma c)) ctx
 
-let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
+let build_wellfounded pm (recname,pl,bl,arityc,body) poly r measure notation =
   let open EConstr in
   let open Vars in
   let lift_rel_context n l = Termops.map_rel_context_with_binders (liftn n) l in
@@ -262,9 +262,9 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
   let uctx = Evd.evar_universe_context sigma in
   let cinfo = Declare.CInfo.make ~name:recname ~typ:evars_typ () in
   let info = Declare.Info.make ~udecl ~poly ~hook () in
-  let _ : Declare.Obls.progress =
-    Declare.Obls.add_definition ~cinfo ~info ~term:evars_def ~uctx evars in
-  ()
+  let pm, _ =
+    Declare.Obls.add_definition ~pm ~cinfo ~info ~term:evars_def ~uctx evars in
+  pm
 
 let out_def = function
   | Some def -> def
@@ -275,7 +275,7 @@ let collect_evars_of_term evd c ty =
   Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev))
   evars (Evd.from_ctx (Evd.evar_universe_context evd))
 
-let do_program_recursive ~scope ~poly fixkind fixl =
+let do_program_recursive ~pm ~scope ~poly fixkind fixl =
   let cofix = fixkind = Declare.Obls.IsCoFixpoint in
   let (env, rec_sign, udecl, evd), fix, info =
     interp_recursive ~cofix ~program_mode:true fixl
@@ -323,15 +323,15 @@ let do_program_recursive ~scope ~poly fixkind fixl =
   in
   let ntns = List.map_append (fun { Vernacexpr.notations } -> notations ) fixl in
   let info = Declare.Info.make ~poly ~scope ~kind ~udecl () in
-  Declare.Obls.add_mutual_definitions defs ~info ~uctx ~ntns fixkind
+  Declare.Obls.add_mutual_definitions ~pm defs ~info ~uctx ~ntns fixkind
 
-let do_fixpoint ~scope ~poly l =
+let do_fixpoint ~pm ~scope ~poly l =
   let g = List.map (fun { Vernacexpr.rec_order } -> rec_order) l in
     match g, l with
     | [Some { CAst.v = CWfRec (n,r) }],
       [ Vernacexpr.{fname={CAst.v=id}; univs; binders; rtype; body_def; notations} ] ->
         let recarg = mkIdentC n.CAst.v in
-        build_wellfounded (id, univs, binders, rtype, out_def body_def) poly r recarg notations
+        build_wellfounded pm (id, univs, binders, rtype, out_def body_def) poly r recarg notations
 
     | [Some { CAst.v = CMeasureRec (n, m, r) }],
       [Vernacexpr.{fname={CAst.v=id}; univs; binders; rtype; body_def; notations }] ->
@@ -344,7 +344,7 @@ let do_fixpoint ~scope ~poly l =
           user_err Pp.(str"Measure takes only two arguments in Program Fixpoint.")
         | _, _ -> r
       in
-        build_wellfounded (id, univs, binders, rtype, out_def body_def) poly
+        build_wellfounded pm (id, univs, binders, rtype, out_def body_def) poly
           (Option.default (CAst.make @@ CRef (lt_ref,None)) r) m notations
 
     | _, _ when List.for_all (fun ro -> match ro with None | Some { CAst.v = CStructRec _} -> true | _ -> false) g ->
@@ -352,12 +352,11 @@ let do_fixpoint ~scope ~poly l =
           Vernacexpr.(ComFixpoint.adjust_rec_order ~structonly:true fix.binders fix.rec_order)) l in
       let fixkind = Declare.Obls.IsFixpoint annots in
       let l = List.map2 (fun fix rec_order -> { fix with Vernacexpr.rec_order }) l annots in
-      do_program_recursive ~scope ~poly fixkind l
-
+      do_program_recursive ~pm ~scope ~poly fixkind l
     | _, _ ->
-        user_err ~hdr:"do_fixpoint"
-          (str "Well-founded fixpoints not allowed in mutually recursive blocks")
+      CErrors.user_err ~hdr:"do_fixpoint"
+        (str "Well-founded fixpoints not allowed in mutually recursive blocks")
 
-let do_cofixpoint ~scope ~poly fixl =
+let do_cofixpoint ~pm ~scope ~poly fixl =
   let fixl = List.map (fun fix -> { fix with Vernacexpr.rec_order = None }) fixl in
-  do_program_recursive ~scope ~poly Declare.Obls.IsCoFixpoint fixl
+  do_program_recursive ~pm ~scope ~poly Declare.Obls.IsCoFixpoint fixl
-- 
cgit v1.2.3