Added a reifiction function for modular reification without pmaps.

examples/PolyApply/Test.v

@@ -0,0 +1,117 @@
+Require Import ExtLib.Core.RelDec.
+
+Require Import MirrorCore.Reify.Reify.
+Require Import MirrorCore.Reify.ReifyClass.
+Require Import MirrorCore.Reify.ReifyView.
+Require Import MirrorCore.Lib.EqView.
+Require Import MirrorCore.CTypes.BaseType.
+Require Import MirrorCore.Lemma.
+(* Require Import MirrorCore.TCLemma. *)
+Require Import MirrorCore.PLemma.
+Require Import MirrorCore.Polymorphic.
+Require Import MirrorCore.Lambda.RewriteRelations.
+Require Import MirrorCore.ExprI.
+Require Import MirrorCore.CTypes.CoreTypes.
+
+
+Inductive my_forall (typ : Set) : Set :=
+| MyForall (t : typ)
+| MyEq (t : typ).
+
+Inductive my_types : nat -> Set :=
+| MyNat : my_types 0.
+
+Section MakeILogic.
+  Context {typ func : Set} {FV : PartialView func (my_forall typ)}.
+
+  Definition fForall t := f_insert (MyForall typ t).
+
+  Definition mkForall (t : typ) (f : expr typ func) := App (Inj (fForall t)) (Abs t f).
+
+End MakeILogic.
+
+(* TODO: Doesn't this exist somewhere?
+Definition IgnorePatterns (ls : list RPattern) (T : Set) : Set := T.
+Opaque IgnorePatterns.
+Section for_ignore.
+  Variable ls : list RPattern.
+  Variable T : Set.
+
+  Definition reify_IgnorePatterns {R : Reify T}
+  : Command T :=
+    let ignores :=
+        map (fun p => CPattern (ls:=(T : Type)::nil) p (fun (a : function (CRec 0)) => a)) ls
+    in
+    CFix (CFirst_ (ignores ++ CCall (@reify_scheme _ R) :: nil)).
+
+  Global Instance Reify_IgnorePatterns {R : Reify T} : Reify (IgnorePatterns ls T) :=
+  { reify_scheme := @reify_IgnorePatterns R }.
+
+End for_ignore.
+
+Typeclasses Opaque IgnorePatterns.
+
+Arguments reify_IgnorePatterns {_} _ {_}.
+*)
+
+Section Test.
+  Context {typ func : Set}.
+  Context {RType_typ : RType typ}.
+
+  Context {RelDec_eq_typ : RelDec (@eq typ)}.
+  Context {RelDec_eq_func : RelDec (@eq func)}.
+  Context {Expr_expr : Expr typ (expr typ func)}.
+  Context {Typ2_tyArr : Typ2 _ RFun}.
+  Context {Typ2Ok_tyArr : Typ2Ok Typ2_tyArr}.
+  Context {Typ0_tyProp : Typ0 _ Prop}.
+  Context {FV1 : PartialView func (eq_func typ)}.
+  Context {FV2 : PartialView func (my_forall typ)}.
+  Context {FV_typ : PartialView typ (base_typ 0)}.
+
+  Let tyProp : typ := @typ0 _ _ _ Typ0_tyProp.
+  Let tyArr : typ -> typ -> typ := @typ2 _ _ _ Typ2_tyArr.
+
+  Local Instance Reify_typ : Reify typ :=
+    Reify_typ typ (reify_base_typ typ :: nil).
+
+  Definition reify_pforall : Command@{Set} (expr typ func) :=
+    CPattern (ls := (typ : Type) :: (expr typ func : Type) :: nil)
+             (RPi (RGet 0 RIgnore) (RGet 1 RIgnore))
+             (fun (x : function (CCall (reify_scheme typ))) (y : function (CRec 0)) =>
+                mkForall x y).
+
+
+  Local Instance Reify_expr : Reify (expr typ func) :=
+    Reify_func_no_table typ func (reify_eq typ func :: reify_pforall :: nil).
+
+  Lemma Id {A} : forall P : A, True -> P = P.
+  Proof.
+    reflexivity.
+  Qed.
+
+  Definition reify_poly :=
+    reify_scheme@{Set}
+                (tc_lemma typ (expr typ func) (expr typ func)
+                          (RExact True :: nil)).
+  Ltac reify_poly e :=
+    let k e :=
+        pose e in
+    reify_expr reify_poly k
+               [[ True ]]
+               [[ e ]].
+
+  Goal True.
+    (* This reifies *)
+    reify_poly (forall x : nat, True -> True -> x = x -> x = x).
+    apply I.
+  Qed.
+
+  Definition lem_landexistsDL :
+    polymorphic typ 1
+                (tc_lemma typ (expr typ func)
+                             (rw_concl typ func (expr typ func))
+                             (RExact True :: nil)) :=
+    Eval unfold Lemma.add_var , Lemma.add_prem , Lemma.vars , Lemma.concl , Lemma.premises, app  in
+        <:: @Id ::>.
+
+End Test.

examples/PolyRewrite/QuantifierPuller/PolyQuantPullRtac.v

@@ -223,7 +223,7 @@ Proof. reflexivity. Qed.
 Definition lem_eq_refl' : polymorphic typ 1 (Lemma.lemma typ (expr typ func) (expr typ func)) :=
   Eval unfold Lemma.add_var, Lemma.add_prem , Lemma.vars , Lemma.concl , Lemma.premises in
     <:: @eq_refl' ::>.
-
+Print lem_eq_refl'.
 Require Import MirrorCore.PLemma.
 
 Definition plem_eq_refl' : PolyLemma typ (expr typ func) (expr typ func) :=
@@ -293,11 +293,12 @@ Definition lem_Proper_exists
   Eval unfold Lemma.add_var, Lemma.add_prem , Lemma.vars , Lemma.concl , Lemma.premises in
   <:: @Proper_exists ::>.
 
+Print lem_Proper_exists.
+
 Definition lem_Proper_forall
 : polymorphic typ 1 (Lemma.lemma typ (expr typ func) (Proper_concl typ func Rbase)) :=
   Eval unfold Lemma.add_var, Lemma.add_prem , Lemma.vars , Lemma.concl , Lemma.premises in
   <:: @Proper_forall ::>.
-
 (*
 Reify BuildPolyLemma 1 < reify_simple_typ reify_simple reify_proper_concl >
   lem_Proper_exists : @Proper_exists.
@@ -343,7 +344,8 @@ Ltac prove_prespectful :=
          | _ => red; simpl
          end.
 *)
-
+Locate ctyp.
+Check @ctyp.
 Theorem get_respectful_only_all_ex_sound
 : respectful_spec RbaseD get_respectful_only_all_ex.
 Proof.
@@ -468,7 +470,6 @@ Require Import MirrorCore.PLemma.
 Require Import MirrorCore.RTac.PApply.
 Require Import MirrorCore.Lambda.ExprUnify_simple.
 
-
 Definition PAPPLY (plem : PolyLemma typ (expr typ func) (expr typ func)) :=
   PAPPLY (RSym_func := RSym_func)
          (fun subst SS SU tus tvs n l r t s =>
@@ -509,8 +510,7 @@ Proof.
   apply Expr.ExprOk_expr.
   apply Expr.ExprOk_expr.
 Qed.
-
-
+Locate RewriteHintDb.
 Definition the_lemmas
 : RewriteHintDb Rbase :=
   @PRw _ _ _ 1 lem_pull_ex_and_left DO_REFL ::

src/reify_Lambda_shell.ml4

@@ -414,7 +414,7 @@ struct
 
     type syntax_data =
       { reify       : lazy_term -> Term.constr reifier
-      ; result_type : Term.constr
+      ; result_type : unit (* Term.constr *)
       }
 
     let reify_table : syntax_data CEphemeron.key Cmap.t ref =
@@ -814,43 +814,45 @@ struct
 	           init_function     = (fun () -> reify_table := Cmap.empty) })
 
     let cmd_Command  = resolve_poly_symbol_no_univs pattern_mod "Command"
-    let get_Command_type env evm cmd =
-      let (_,typ) =
-        try Typing.type_of env evm cmd
-        with _ ->
-          Errors.errorlabstrm "Type-error"
-            Pp.(   str "Reification command is ill-typed"
-                ++ fnl ()
-                ++ Printer.pr_constr_env env evm cmd)
-      in
-      try
-        Term_match.(matches ()
-                      [(apps (Glob_no_univ cmd_Command) [get 0],
-                        fun _ s -> Hashtbl.find s 0)]
-                      typ)
-      with
-        Term_match.Match_failure ->
-        Errors.anomaly Pp.(   str "Reification got non-Command"
-                           ++ fnl ()
-                           ++ Printer.pr_constr_env env evm cmd
-                           ++ fnl ()
-                           ++ str "has type" ++ fnl ()
-                           ++ Printer.pr_constr_env env evm typ)
+    (* let get_Command_type env evm cmd = *)
+    (*   let (_,typ) = *)
+    (*     try Typing.type_of env evm cmd *)
+    (*     with _ -> *)
+    (*       Errors.errorlabstrm "Type error" *)
+    (*         Pp.(   str "Reification command is ill-typed" *)
+    (*             ++ fnl () *)
+    (*             ++ Printer.pr_constr_env env evm cmd) *)
+    (*   in *)
+    (*   try *)
+    (*     Term_match.(matches () *)
+    (*                   [(apps (Glob_no_univ cmd_Command) [get 0], *)
+    (*                     fun _ s -> Hashtbl.find s 0)] *)
+    (*                   typ) *)
+    (*   with *)
+    (*     Term_match.Match_failure -> *)
+    (*     Errors.errorlabstrm "Type error" *)
+    (*       Pp.(   str "Reification got non-Command" *)
+    (*           ++ fnl () *)
+    (*           ++ Printer.pr_constr_env env evm cmd *)
+    (*           ++ fnl () *)
+    (*           ++ str "has type" ++ fnl () *)
+    (*           ++ Printer.pr_constr_env env evm typ) *)
 
     let compile_name (prg : Term.constr) =
       let (evm,env) = Lemmas.get_current_context () in
-      let typ = get_Command_type env evm prg in
+      (* let typ = get_Command_type env evm prg in *)
       let reduced = Reductionops.whd_betadeltaiota env evm prg in
       let program = parse_command env evm reduced in
       try
-        { result_type = typ
+        { result_type = () (* typ *)
         ; reify = compile_command [] program }
       with
       | _ ->
-        Errors.anomaly
+        Errors.errorlabstrm "Compilation error"
           Pp.(   str "Failed to compile" ++ fnl ()
               ++ Printer.pr_constr prg
-              ++ fnl ())
+              ++ fnl ()
+              ++ str "(Are your binders correct?)")
 
     let get_entry (name : Term.constr) =
       let name = drop_calls name in
@@ -876,9 +878,11 @@ struct
 
     let _ = set_reify_term reify_term
 
+(*
     let reify_type (name : Term.constr) =
       let data = get_entry name in
       data.result_type
+*)
 
     let declare_syntax (name : Names.identifier) env evm
 	(cmd : Term.constr) : unit =
@@ -896,7 +900,7 @@ struct
       in
       let program = parse_command env evm cmd in
       let _meta_reifier = compile_command [] program in
-      let data = { result_type = typ
+      let data = { result_type = () (* typ *)
                  ; reify = _meta_reifier } in
       let obj = decl_constant name evm cmd in
       reify_table := Cmap.add obj (CEphemeron.create data) !reify_table

theories/CTypes/BaseType.v

@@ -9,6 +9,7 @@ Require Import MirrorCore.Reify.ReifyClass.
 
 Require Import ExtLib.Core.RelDec.
 Require Import ExtLib.Data.POption.
+Require Import ExtLib.Data.Vector.
 
 Require Import Coq.Strings.String.
 
@@ -61,6 +62,19 @@ Definition base_typD {n} (t : base_typ n) : type_for_arity n :=
   | tProp => Prop
   end.
 
+Definition inhabited_base_typ {n : nat} 
+  : forall (t : base_typ n) (vs : vector Type@{Usmall} n),
+  inhabited (applyn (base_typD t) vs).
+Proof.
+  intros.
+  destruct n; [|inversion t].
+  destruct t; rewrite (vector_eta vs); simpl.
+  + apply (inhabits 0).
+  + apply (inhabits EmptyString).
+  + apply (inhabits true).
+  + apply (inhabits True).
+Defined.
+
 Section DepMatch_base_typ.
   Context {typ : Set}.
   Context {RType_typ : RType typ}.

theories/CTypes/CoreTypes.v

@@ -289,6 +289,43 @@ Section parametric.
   ; type_cast := ctyp_cast
   ; tyAcc := ctyp_acc }.
 
+  Program Fixpoint ctyp_noVar (c : ctyp) : Prop :=
+    match c with
+    | tyArr c1 c2 => ctyp_noVar c1 /\ ctyp_noVar c2
+    | tyBase0 _ => True
+    | tyBase1 _ c => ctyp_noVar c
+    | tyBase2 _ c1 c2 => ctyp_noVar c1 /\ ctyp_noVar c2
+    | tyApp _ vs => ForallV id (vector_map ctyp_noVar vs)
+    | tyProp => True
+    | tyVar _ => False
+    end.
+
+  Lemma inhabited_ctyp (c : ctyp) 
+        (NoVar : ctyp_noVar c) 
+        (H : forall (n : nat) (s : symbol n) (vs : vector Type@{Usmall} n), 
+            ForallV inhabited vs -> inhabited (applyn (symbolD s) vs)) : inhabited (typD c).
+  Proof.
+    induction c using ctyp_ind.
+    + destruct NoVar as [_ NoVar]. 
+      destruct (IHc2 NoVar). apply inhabits; intros _; apply X.
+    + simpl. specialize (H 0 s (Vnil _)); apply H; constructor.
+    + simpl; specialize (H 1 s (Vcons (ctypD c) (Vnil _))).
+      apply H; constructor; [apply IHc; apply NoVar | constructor].
+    + simpl; specialize (H 2 s (Vcons (ctypD c1) (Vcons (ctypD c2) (Vnil _)))).
+      destruct NoVar as [NoVar1 NoVar2].
+      apply H. constructor; [apply (IHc1 NoVar1) | 
+                             constructor; [apply (IHc2 NoVar2) | 
+                                           constructor]].
+    + simpl in *; apply H.
+      rewrite ForallV_map.
+      rewrite ForallV_map in NoVar; unfold id in NoVar.
+      repeat forallVE.
+      repeat (constructor; [tauto|]).
+      eapply ForallV_mp; [|eassumption]; assumption.
+    + apply (inhabits True).
+    + simpl in *. destruct NoVar.
+  Qed.
+
   Local Instance EqDec_symbol : forall n, EqDec (symbol n) (@eq (symbol n)).
   Proof.
     red. intros.

theories/CTypes/ListType.v

@@ -8,6 +8,7 @@ Require Import MirrorCore.Reify.ReifyClass.
 
 Require Import ExtLib.Core.RelDec.
 Require Import ExtLib.Data.PList.
+Require Import ExtLib.Data.Vector.
 
 Set Implicit Arguments.
 Set Strict Implicit.
@@ -31,6 +32,18 @@ Definition list_typD {n} (t : list_typ n) : type_for_arity n :=
   | tList => list
   end.
 
+Definition inhabited_list_typ {n : nat} (t : list_typ n) (vs : vector Type@{Usmall} n) :
+  inhabited (applyn (list_typD t) vs).
+Proof.
+  intros.
+  destruct n; [inversion t|].
+  destruct n; [|inversion t].
+  destruct t.
+  rewrite (vector_eta vs); simpl.
+  rewrite (vector_eta (vector_tl vs)).
+  apply inhabits; apply nil.
+Defined.
+
 Section FuncView_list_type.
   Context {typ : Set}.
   Context {FV : PartialView typ (list_typ 1 * typ)}.