MetaCoq · mattam82 · Jun 14, 2019 · Jun 14, 2019 · Jun 17, 2019 · Jun 17, 2019
diff --git a/template-coq/Makefile b/template-coq/Makefile
@@ -1,4 +1,4 @@
-all: coq plugin
+all: coq # plugin
 
 coq: Makefile.coq
 	$(MAKE) -f Makefile.coq

diff --git a/template-coq/test-plugin/test.v b/template-coq/test-plugin/test.v
diff --git a/template-coq/theories/All.v b/template-coq/theories/All.v
@@ -8,7 +8,7 @@ From MetaCoq.Template Require Export
      uGraph        (* The graph of universes *)
      TemplateMonad (* The TemplateMonad *)
      AstUtils      (* Utilities on the AST *)
-     Loader        (* Declaration of the Template Coq plugin *)
+     (* Loader        (* Declaration of the Template Coq plugin *) *)
      Induction     (* Induction *)
      LiftSubst     (* Lifting and substitution for terms *)
      UnivSubst     (* Substitution of universe instances *)

diff --git a/template-coq/theories/AstUtils.v b/template-coq/theories/AstUtils.v
@@ -687,3 +687,113 @@ Coercion fst_ctx : global_env_ext >-> global_env.
 
 Definition empty_ext (Σ : global_env) : global_env_ext
   := (Σ, Monomorphic_ctx ContextSet.empty).
+
+Section ListSize.
+  Context {A} (size : A -> nat).
+
+  Fixpoint list_size (l : list A) : nat :=
+    match l with
+    | nil => 0
+    | cons a v => S (size a + list_size v)
+    end.
+
+  Lemma list_size_app (l l' : list A) : list_size (l ++ l') = list_size l + list_size l'.
+  Proof.
+    induction l; simpl; rewrite ?IHl; auto with arith.
+  Defined.
+
+  Lemma list_size_rev (l : list A) : list_size (List.rev l) = list_size l.
+  Proof.
+    induction l; simpl; rewrite ?IHl ?list_size_app; simpl; auto; try lia.
+  Defined.
+
+End ListSize.
+
+Section ListSizeMap.
+  Context {A} (sizeA : A -> nat).
+  Context {B} (sizeB : B -> nat).
+
+  Lemma list_size_mapi_rec_eq (l : list A) (f : nat -> A -> B) k :
+    (forall i x, sizeB (f i x) = sizeA x) ->
+    list_size sizeB (mapi_rec f l k) = list_size sizeA l.
+  Proof.
+    revert k.
+    induction l; simpl; intros; rewrite ?IHl ?list_size_app; simpl; auto; try lia.
+  Defined.
+
+  Lemma list_size_mapi_eq (l : list A) (f : nat -> A -> B) :
+    (forall i x, sizeB (f i x) = sizeA x) ->
+    list_size sizeB (mapi f l) = list_size sizeA l.
+  Proof.
+    unfold mapi. intros. now apply list_size_mapi_rec_eq.
+  Defined.
+
+  Lemma list_size_map_eq (l : list A) (f : A -> B) :
+    (forall x, sizeA x = sizeB (f x)) ->
+    list_size sizeB (map f l) = list_size sizeA l.
+  Proof.
+    intros.
+    induction l; simpl; auto.
+  Defined.
+
+  Lemma list_size_mapi_rec_le (l : list A) (f : nat -> A -> B) k :
+    (forall i x, sizeB (f i x) <= sizeA x) ->
+    list_size sizeB (mapi_rec f l k) <= list_size sizeA l.
+  Proof.
+    intros Hf. revert k.
+    induction l; simpl; intros; rewrite ?IHl ?list_size_app;
+      simpl; auto; try lia.
+    specialize (Hf k a).
+    specialize (IHl (S k)). lia.
+  Defined.
+
+  Lemma list_size_mapi_le (l : list A) (f : nat -> A -> B) :
+    (forall i x, sizeB (f i x) <= sizeA x) ->
+    list_size sizeB (mapi f l) <= list_size sizeA l.
+  Proof.
+    unfold mapi. intros. now apply list_size_mapi_rec_le.
+  Defined.
+
+  Lemma list_size_map_le (l : list A) (f : A -> B) :
+    (forall x, sizeB (f x) <= sizeA x) ->
+    list_size sizeB (map f l) <= list_size sizeA l.
+  Proof.
+    intros.
+    induction l; simpl; auto. specialize (H a).
+    lia.
+  Defined.
+
+End ListSizeMap.
+
+Lemma list_size_map_hom {A} (size : A -> nat) (l : list A) (f : A -> A) :
+  (forall x, size x = size (f x)) ->
+  list_size size (map f l) = list_size size l.
+Proof.
+  intros.
+  induction l; simpl; auto.
+Defined.
+
+Definition def_size (size : term -> nat) (x : def term) := size (dtype x) + size (dbody x).
+Definition mfixpoint_size (size : term -> nat) (l : mfixpoint term) :=
+  list_size (def_size size) l.
+
+Definition decl_size (size : term -> nat) (x : context_decl) :=
+  size (decl_type x) + option_default size (decl_body x) 0.
+
+Definition context_size (size : term -> nat) (l : context) :=
+  list_size (decl_size size) l.
+
+Fixpoint term_size t : nat :=
+  match t with
+  | tRel i => 1
+  | tEvar ev args => S (list_size term_size args)
+  | tLambda na T M => S (term_size T + term_size M)
+  | tApp u v => S (term_size u + list_size term_size v)
+  | tProd na A B => S (term_size A + term_size B)
+  | tLetIn na b t b' => S (term_size b + term_size t + term_size b')
+  | tCase ind p c brs => S (term_size p + term_size c + list_size (fun x => term_size (snd x)) brs)
+  | tProj p c => S (term_size c)
+  | tFix mfix idx => S (mfixpoint_size term_size mfix)
+  | tCoFix mfix idx => S (mfixpoint_size term_size mfix)
+  | x => 1
+  end.
diff --git a/template-coq/theories/Extraction.v b/template-coq/theories/Extraction.v
diff --git a/template-coq/theories/Loader.v b/template-coq/theories/Loader.v
diff --git a/template-coq/theories/Typing.v b/template-coq/theories/Typing.v
@@ -1042,7 +1042,6 @@ Notation wf_local Σ Γ := (All_local_env (lift_typing typing Σ) Γ).
 
 (** ** Typechecking of global environments *)
 
-
 Definition isType `{checker_flags} (Σ : global_env_ext) (Γ : context) (t : term) :=
   { s : _ & Σ ;;; Γ |- t : tSort s }.
 

diff --git a/template-coq/theories/Validity.v b/template-coq/theories/Validity.v
diff --git a/template-coq/theories/kernel/Checker.v b/template-coq/theories/kernel/Checker.v
@@ -27,17 +27,25 @@ Module RedFlags.
       zeta : bool;
       delta : bool;
       fix_ : bool;
-      cofix_ : bool }.
+      cofix_ : bool;
+      strong: bool;
+    }.
 
-  Definition default := mk true true true true true true.
+  Definition default := mk true true true true true true false.
 End RedFlags.
 
 Section Reduce.
   Context (flags : RedFlags.t) (Σ : global_env).
 
   Definition zip (t : term * list term) := mkApps (fst t) (snd t).
 
-  Fixpoint reduce_stack (Γ : context) (n : nat) (t : term) (stack : list term)
+  Definition reduce_aux (reduce_stack : term -> list term -> option (term * list term)) t :=
+    if RedFlags.strong flags then
+      t' <- reduce_stack t [];;
+       ret (zip t')
+    else ret t.
+
+  Fixpoint reduce_stack (Γ : context) (n : nat) (t : term) (stack : list term) {struct n}
     : option (term * list term) :=
   match n with 0 => None | S n =>
   match t with
@@ -66,20 +74,30 @@ Section Reduce.
       end
     else ret (t, stack)
 
-  | tApp f args => reduce_stack Γ n f (args ++ stack)
+  | tApp f args =>
+    args' <- monad_map (fun x => x' <- reduce_aux (reduce_stack Γ n) x;; ret x') args;;
+(*! *)
+    reduce_stack Γ n f (args' ++ stack)
+(*!! Wrong-Beta *)
+(*! reduce_stack Γ n f stack *)
 
   | tLambda na ty b =>
+    let strong stack :=
+      if RedFlags.strong flags then
+        x <- reduce_stack (vass na ty :: Γ) n b [];;
+          let '(b', stack') := x in
+          ret (tLambda na ty (zip (b', stack')), stack)
+      else ret (t, stack)
+    in
     if RedFlags.beta flags then
       match stack with
       | a :: args' =>
         (** CBN reduction: we do not reduce arguments before substitution *)
         (* a' <- reduce_stack Γ n a [] ;; *)
         reduce_stack Γ n (subst10 a b) args'
-      | _ => ret (t, stack)
-               (*  b' <- reduce_stack (Γ ,, vass na ty) n b stack ;; *)
-               (* ret (tLambda na ty (zip b'), stack) *)
+      | _ => strong stack
       end
-    else ret (t, stack)
+    else strong stack
 
   | tFix mfix idx =>
     if RedFlags.fix_ flags then
@@ -96,7 +114,13 @@ Section Reduce.
       end
     else ret (t, stack)
 
-  | tProd _ _ _ => ret (t, stack)
+  | tProd na dom codom =>
+    if RedFlags.strong flags then
+      dom' <- reduce_stack Γ n dom [];;
+      codom' <- reduce_stack (vass na dom :: Γ) n codom [];;
+      ret (tProd na (zip dom') (zip codom'), stack)
+    else
+      ret (t, stack)
 
     (* b' <- reduce_stack Γ n b [] ;; *)
     (* t' <- reduce_stack (Γ ,, vass na (zip b')) n t [] ;; *)
@@ -105,13 +129,16 @@ Section Reduce.
   | tCast c _ _ => reduce_stack Γ n c stack
 
   | tCase (ind, par) p c brs =>
+    brs' <- monad_map (fun '(nargs, br) => br' <- reduce_aux (reduce_stack Γ n) br;; ret (nargs, br')) brs;;
+    p' <- reduce_aux (reduce_stack Γ n) p;;
     if RedFlags.iota flags then
-      c' <- reduce_stack Γ n c [] ;;
+      c' <- reduce_stack Γ n c [];;
       match c' with
-      | (tConstruct ind c _, args) => reduce_stack Γ n (iota_red par c args brs) stack
-      | _ => ret (tCase (ind, par) p (zip c') brs, stack)
+      | (tConstruct ind c _, args) => reduce_stack Γ n (iota_red par c args brs') stack
+      | _ => ret (tCase (ind, par) p' (zip c') brs', stack)
       end
-    else ret (t, stack)
+    else c' <- reduce_aux (reduce_stack Γ n) c;;
+         ret (tCase (ind, par) p' c' brs', stack)
 
   | _ => ret (t, stack)
 
@@ -260,7 +287,7 @@ Section Conversion.
   Context `{checker_flags} (flags : RedFlags.t).
   Context (Σ : global_env) (G : universes_graph).
 
-  Definition nodelta_flags := RedFlags.mk true true true false true true.
+  Definition nodelta_flags : RedFlags.t := RedFlags.mk true true true false true true false.
 
   Definition unfold_one_fix n Γ mfix idx l :=
     unf <- unfold_fix mfix idx ;;
@@ -819,6 +846,7 @@ Section Typecheck2.
       (** TODO check branches *)
       let '(ind', u, args) := indargs in
       if eq_ind ind ind' then
+        (* FIXME for quickchick *)
         ret (tApp p (List.skipn par args ++ [c]))
       else
         let ind1 := tInd ind u in