Fixing issue #6: singleton Prop remain in Prop

_CoqProject

@@ -1,11 +1,12 @@
 -R theories Forcing
 -I src
 
+src/fAux.ml
 src/fTranslate.ml
 src/fTranslate.mli
 src/fPlugin.ml
 src/fPlugin.mli
-src/g_forcing.ml4
+src/g_forcing.mlg
 src/forcing.mllib
 
 theories/Forcing.v

src/fAux.ml

@@ -0,0 +1,7 @@
+(** Utilities *)
+
+let clos_norm_flags flgs env t =
+  CClosure.norm_val
+    (CClosure.create_clos_infos flgs env)
+    (CClosure.create_tab ())
+    (CClosure.inject t)

src/fPlugin.mli

@@ -2,8 +2,8 @@ open Names
 open Libnames
 open Proofview
 
-val force_tac : FTranslate.category -> Constr.t -> unit tactic
+val force_tac : (EConstr.t * EConstr.t) -> EConstr.t -> unit tactic
 
-val force_translate : (reference * reference) -> reference -> Id.t list option -> unit
+val force_translate : (qualid * qualid) -> qualid -> Id.t list option -> unit
 
-val force_implement : (reference * reference) -> Id.t -> Constrexpr.constr_expr -> Id.t option -> unit
+val force_implement : (qualid * qualid) -> Id.t -> Constrexpr.constr_expr -> Id.t option -> Declare.Proof.t

src/fTranslate.ml

@@ -1,15 +1,13 @@
 open Names
 open Term
+open Constr
 open Declarations
 open Environ
-open Globnames
-open Pp
 
 module RelDecl = Context.Rel.Declaration
-module NamedDecl = Context.Named.Declaration
 
-type translator = global_reference Refmap.t
-exception MissingGlobal of global_reference
+type translator = GlobRef.t GlobRef.Map.t
+exception MissingGlobal of GlobRef.t
 
 (** Yoneda embedding *)
 
@@ -20,13 +18,13 @@ type category = {
   (** Morphisms. Must be of type [cat_obj -> cat_obj -> Type]. *)
 }
 
-let obj_name = Name (Id.of_string "R")
-let knt_name = Name (Id.of_string "k")
+let obj_name = Context.nameR (Id.of_string "R")
+let knt_name = Context.nameR (Id.of_string "k")
 
 let hom cat a b =
   let lft = mkApp (cat.cat_hom, [| Vars.lift 1 b; mkRel 1 |]) in
   let rgt = mkApp (cat.cat_hom, [| Vars.lift 2 a; mkRel 2 |]) in
-  let arr = mkArrow lft rgt in
+  let arr = Term.mkArrow lft Sorts.Relevant rgt in
   mkProd (obj_name, cat.cat_obj, arr)
 
 let refl cat a =
@@ -71,8 +69,8 @@ type forcing_context = {
 
 (** We assume that there is a hidden topmost variable [p : Obj] in the context *)
 
-let pos_name = Name (Id.of_string "p")
-let hom_name = Name (Id.of_string "α")
+let pos_name = Context.nameR (Id.of_string "p")
+let hom_name = Context.nameR (Id.of_string "α")
 
 let dummy = mkProp
 
@@ -131,36 +129,32 @@ let translate_var fctx n =
   let m = get_var_shift n fctx in
   mkApp (mkRel m, [| p; f |])
 
-let rec untranslate_rel n c = match Constr.kind c with
-| App (t, args) when isRel t && Array.length args >= 2 ->
-  c
-| _ -> Constr.map_with_binders succ untranslate_rel n c
-
 let get_inductive fctx ind =
-  let gr = IndRef ind in
+  let gr = GlobRef.IndRef ind in
   let gr_ =
-    try Refmap.find gr fctx.translator
+    try GlobRef.Map.find gr fctx.translator
     with Not_found -> raise (MissingGlobal gr)
   in
   match gr_ with
-  | IndRef ind_ -> ind_
+  | GlobRef.IndRef ind_ -> ind_
   | _ -> assert false
 
 let apply_global env sigma gr u fctx =
-  (** FIXME *)
+  (* FIXME *)
   let p' =
-    try Refmap.find gr fctx.translator
+    try GlobRef.Map.find gr fctx.translator
     with Not_found -> raise (MissingGlobal gr)
   in
   let (sigma, c) = Evd.fresh_global env sigma p' in
+  let c = EConstr.to_constr sigma c in
   let last = last_condition fctx in
   match gr with
-  | IndRef _ -> assert false
+  | GlobRef.IndRef _ -> assert false
   | _ -> (sigma, mkApp (c, [| mkRel last |]))
 
 (** Forcing translation core *)
 
-let rec otranslate env fctx sigma c = match kind_of_term c with
+let rec otranslate env fctx sigma c = match kind c with
 | Rel n ->
   let ans = translate_var fctx n in
   (sigma, ans)
@@ -182,19 +176,19 @@ let rec otranslate env fctx sigma c = match kind_of_term c with
   (sigma, ans)
 | Prod (na, t, u) ->
   let (ext0, fctx) = extend fctx in
-  (** Translation of t *)
+  (* Translation of t *)
   let (sigma, t_) = otranslate_boxed_type env fctx sigma t in
-  (** Translation of u *)
+  (* Translation of u *)
   let ufctx = add_variable fctx in
   let (sigma, u_) = otranslate_type env ufctx sigma u in
-  (** Result *)
+  (* Result *)
   let ans = mkProd (na, t_, u_) in
   let lam = it_mkLambda_or_LetIn ans ext0 in
   (sigma, lam)
 | Lambda (na, t, u) ->
-  (** Translation of t *)
+  (* Translation of t *)
   let (sigma, t_) = otranslate_boxed_type env fctx sigma t in
-  (** Translation of u *)
+  (* Translation of u *)
   let ufctx = add_variable fctx in
   let (sigma, u_) = otranslate env ufctx sigma u in
   let ans = mkLambda (na, t_, u_) in
@@ -211,37 +205,41 @@ let rec otranslate env fctx sigma c = match kind_of_term c with
 | App (t, args) ->
   let (sigma, t_) = otranslate env fctx sigma t in
   let fold sigma u = otranslate_boxed env fctx sigma u in
-  let (sigma, args_) = CArray.fold_map fold sigma args in
+  let (sigma, args_) = CArray.fold_left_map fold sigma args in
   let app = mkApp (t_, args_) in
   (sigma, app)
 | Var id ->
-  apply_global env sigma (VarRef id) Univ.Instance.empty fctx
+  apply_global env sigma (GlobRef.VarRef id) Univ.Instance.empty fctx
 | Const (p, u) ->
-  apply_global env sigma (ConstRef p) u fctx
+  apply_global env sigma (GlobRef.ConstRef p) u fctx
 | Ind (ind, u) ->
   otranslate_ind env fctx sigma ind u [||]
 | Construct (c, u) ->
-  apply_global env sigma (ConstructRef c) u fctx
-| Case (ci, r, c, p) ->
+  apply_global env sigma (GlobRef.ConstructRef c) u fctx
+| Case (ci, r, iv, c, p) ->
    let ind_ = get_inductive fctx ci.ci_ind in
-   let ci_ = Inductiveops.make_case_info env ind_ ci.ci_pp_info.style in
+   let ci_ = Inductiveops.make_case_info env ind_ Sorts.Relevant ci.ci_pp_info.style in
    let (sigma, c_) = otranslate env fctx sigma c in
    let fix_return_clause env fctx sigma r =
-     (** The return clause structure is fun indexes self => Q
+     (* The return clause structure is fun indexes self => Q
          All indices must be boxed, but self only needs to be translated *)
      let (args, r_) = decompose_lam_assum r in
      let (na, self, args) = match args with
        | RelDecl.LocalAssum (na, ty) :: t -> (na, ty, t)
        | _ -> assert false in
      let fold (sigma, fctx) decl =
        let (na, o, u) = RelDecl.to_tuple decl in
-      (** For every translated index, the corresponding variable is added
+      (* For every translated index, the corresponding variable is added
           to the forcing context *)
        let (sigma, u_) = otranslate_boxed_type env fctx sigma u in
+       let (sigma, o_) = match o with
+         | None -> (sigma, None)
+         | Some o -> let (sigma, o) = otranslate_boxed env fctx sigma o in (sigma, Some o) in
        let fctx = add_variable fctx in
-       (sigma, fctx), RelDecl.of_tuple (na, o, u_)
+       let decl = match o_ with None -> RelDecl.LocalAssum (na, u_) | Some o_ -> RelDecl.LocalDef (na, o_, u_) in
+       (sigma, fctx), decl
      in
-     let (sigma, fctx), args = CList.fold_map fold (sigma, fctx) args in
+     let (sigma, fctx), args = CList.fold_left_map fold (sigma, fctx) args in
      let (sigma, self_) = otranslate_type env fctx sigma self in
      let fctx_ = add_variable fctx in
      let (sigma, r_) = otranslate_type env fctx_ sigma r_ in
@@ -250,29 +248,34 @@ let rec otranslate env fctx sigma c = match kind_of_term c with
      let flags = let open CClosure in
        RedFlags.red_add betaiota RedFlags.fDELTA
      in
-     let r_ = Reductionops.clos_norm_flags flags env Evd.empty r_ in
+     let r_ = FAux.clos_norm_flags flags env r_ in
      let r_ = Vars.substnl [it_mkLambda_or_LetIn (mkVar selfid) ext] 1 (Vars.lift 1 r_) in
-     let r_ = Reductionops.nf_beta Evd.empty r_ in 
+     let r_ = FAux.clos_norm_flags CClosure.beta env r_ in
      let r_ = Vars.subst_var selfid r_ in
      let r_ = it_mkLambda_or_LetIn r_ (RelDecl.LocalAssum (na, self_) :: args) in
      (sigma, r_)       
    in
    let (sigma, r_) = fix_return_clause env fctx sigma r in
    let fold sigma u = otranslate env fctx sigma u in
-   let (sigma, p_) = CArray.fold_map fold sigma p in
-   (sigma, mkCase (ci_, r_, c_, p_))
+   let (sigma, p_) = CArray.fold_left_map fold sigma p in
+   (* Do not support "UIP" *)
+   let iv_ = NoInvert in
+   (sigma, mkCase (ci_, r_, iv_, c_, p_))
 | Fix f -> assert false
 | CoFix f -> assert false
 | Proj (p, c) -> assert false
 | Meta _ -> assert false
 | Evar _ -> assert false
+| Int _ -> assert false
+| Float _ -> assert false
+| Array _ -> assert false
 
 and otranslate_ind env fctx sigma ind u args =
   let ind_ = get_inductive fctx ind in
   let (_, oib) = Inductive.lookup_mind_specif env ind_ in
   let fold sigma u = otranslate_boxed env fctx sigma u in
-  let (sigma, args_) = CArray.fold_map fold sigma args in
-  (** First parameter is the toplevel forcing condition *)
+  let (sigma, args_) = CArray.fold_left_map fold sigma args in
+  (* First parameter is the toplevel forcing condition *)
   let _, paramtyp = CList.sep_last oib.mind_arity_ctxt in
   let nparams = List.length paramtyp in
   let last = last_condition fctx in
@@ -338,14 +341,13 @@ let translate_context ?(toplevel = true) ?lift translator cat env sigma ctx =
   let empty = empty translator cat lift env in
   let fold decl (sigma, fctx, ctx_) =
     let (na, body, t) = RelDecl.to_tuple decl in
-    let (sigma, body_) = match body with
-    | None -> (sigma, None)
-    | Some _ -> assert false
-    in
     let (ext, tfctx) = extend fctx in
     let (sigma, t_) = otranslate_type env tfctx sigma t in
     let t_ = it_mkProd_or_LetIn t_ ext in
-    let decl_ = RelDecl.of_tuple (na, body_, t_) in
+    let (sigma, decl_) = match body with
+    | None -> (sigma, RelDecl.LocalAssum (na, t_))
+    | Some _ -> assert false
+    in
     let fctx = add_variable fctx in
     (sigma, fctx, decl_ :: ctx_)
   in

src/fTranslate.mli

@@ -1,4 +1,4 @@
-open Globnames
+open Names
 
 type category = {
   cat_obj : Constr.t;
@@ -7,11 +7,11 @@ type category = {
   (** Morphisms. Must be a closed term of type [cat_obj -> cat_obj -> Type]. *)
 }
 
-exception MissingGlobal of global_reference
+exception MissingGlobal of GlobRef.t
 
-type translator = global_reference Refmap.t
+type translator = GlobRef.t GlobRef.Map.t
 
-val hom : category -> Constr.constr -> Constr.constr -> Term.types
+val hom : category -> Constr.constr -> Constr.constr -> Constr.types
 
 val translate : ?toplevel:bool ->  ?lift:int -> translator -> category ->
   Environ.env -> Evd.evar_map -> Constr.t -> Evd.evar_map * Constr.t
@@ -20,4 +20,4 @@ val translate_type : ?toplevel:bool -> ?lift:int -> translator -> category ->
   Environ.env -> Evd.evar_map -> Constr.t -> Evd.evar_map * Constr.t
 
 val translate_context : ?toplevel:bool -> ?lift:int -> translator -> category ->
-  Environ.env -> Evd.evar_map -> Context.Rel.t -> Evd.evar_map * Context.Rel.t
+  Environ.env -> Evd.evar_map -> Constr.rel_context -> Evd.evar_map * Constr.rel_context

src/forcing.mllib

@@ -1,3 +1,4 @@
+FAux
 FTranslate
 FPlugin
 G_forcing

src/g_forcing.mlg

@@ -0,0 +1,34 @@
+{
+
+open Ltac_plugin
+open Stdarg
+open Extraargs
+
+}
+
+DECLARE PLUGIN "forcing"
+
+TACTIC EXTEND force
+| [ "force" constr(obj) constr(hom) constr(c) ] ->
+  { FPlugin.force_tac (obj,hom) c }
+END
+
+VERNAC COMMAND EXTEND ForcingTranslation CLASSIFIED AS SIDEFF
+| [ "Forcing" "Translate" global(gr) "using" global(obj) global(hom) ] ->
+  { FPlugin.force_translate (obj, hom) gr None }
+| [ "Forcing" "Translate" global(gr) "as" ne_ident_list(id) "using" global(obj) global(hom) ] ->
+  { FPlugin.force_translate (obj, hom) gr (Some id) }
+END
+
+{
+
+let classify_impl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]))
+
+}
+
+VERNAC COMMAND EXTEND ForcingImplementation CLASSIFIED BY { classify_impl } STATE open_proof
+| [ "Forcing" "Definition" ident(id) ":" lconstr(typ) "using" global(obj) global(hom) ] ->
+  { FPlugin.force_implement (obj, hom) id typ None }
+| [ "Forcing" "Definition" ident(id) ":" lconstr(typ) "as" ident(id') "using" global(obj) global(hom) ] ->
+  { FPlugin.force_implement (obj, hom) id typ (Some id') }
+END

test/Test.v

@@ -27,4 +27,7 @@ _force (fun A n (v : vect A n) =>
             |consv _ _ x r => 1 
           end).
 exact I.
-Qed.
+Qed.
+
+Forcing Translate and using Obj Hom.
+Forcing Translate iff using Obj Hom.

theories/Forcing.v

@@ -1 +1,2 @@
+Declare ML Module "ltac_plugin".
 Declare ML Module "forcing".