From 4bf1b37a5f5c902369d9fe43be23f09a737f4dd0 Mon Sep 17 00:00:00 2001
From: favonia <favonia@gmail.com>
Date: Sat, 18 Aug 2018 11:37:45 +0800
Subject: [PATCH 1/6] Remove something that does not make sense.

---
 src/core/Val.ml | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

diff --git a/src/core/Val.ml b/src/core/Val.ml
index a414a66f0..7b01610e8 100644
--- a/src/core/Val.ml
+++ b/src/core/Val.ml
@@ -1358,15 +1358,14 @@ struct
 
   and rigid_ghcom dir ty cap sys : value =
     match unleash ty with
-    (* Who knows whether we can delay the expansion
-     * in `Up _`? Please move `Up _` to the second
-     * list if this does not work out. *)
-    | Pi _ | Sg _ | Up _ ->
+    | Pi _ | Sg _ ->
       make @@ GHCom {dir; ty; cap; sys}
 
     (* `Ext _`: the expansion will stop after a valid
-     * correction system, so it is not so bad. *)
-    | Ext _ | Univ _ | FHCom _ | V _ | Data _ ->
+     * correction system, so it is not so bad.
+     *
+     * `Up _`: perhaps we can have nghcom? *)
+    | Ext _ | Univ _ | FHCom _ | V _ | Data _ | Up _ ->
       let aux sys =
         match sys with
         | [] -> cap

From 78b6cfcffe087f6b55676f71fbdb2ba259144a88 Mon Sep 17 00:00:00 2001
From: favonia <favonia@gmail.com>
Date: Sat, 18 Aug 2018 13:19:44 +0800
Subject: [PATCH 2/6] Type-check fhcom in data types.

---
 src/core/Typing.ml | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/core/Typing.ml b/src/core/Typing.ml
index aab513f1e..11146df04 100644
--- a/src/core/Typing.ml
+++ b/src/core/Typing.ml
@@ -225,6 +225,9 @@ let rec check_ cx ty rst tm =
     let constr = Desc.lookup_constr clbl desc in
     check_constr cx dlbl constr args;
 
+  | [], D.Data dlbl, T.FHCom info ->
+    check_fhcom cx ty info.r info.r' info.cap info.sys
+
 
   | _, D.Pi {dom; cod}, T.Lam (T.B (nm, tm)) ->
     let cxx, x = Cx.ext_ty cx ~nm dom in

From 9f317387aab2ebf6c5954928ea4f83376467d5c3 Mon Sep 17 00:00:00 2001
From: favonia <favonia@gmail.com>
Date: Sat, 18 Aug 2018 13:20:29 +0800
Subject: [PATCH 3/6] Coersion in strict data types should be id.

---
 src/core/Val.ml | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

diff --git a/src/core/Val.ml b/src/core/Val.ml
index 7b01610e8..e72565a79 100644
--- a/src/core/Val.ml
+++ b/src/core/Val.ml
@@ -768,7 +768,7 @@ struct
       args
 
   (* Figure 8 of Part IV: https://arxiv.org/abs/1801.01568v3; specialized to non-indexed HITs. *)
-  and rigid_coe_data_intro dir abs ~dlbl ~clbl ~const_args ~rec_args ~rs =
+  and rigid_coe_nonstrict_data_intro dir abs ~dlbl ~clbl ~const_args ~rec_args ~rs =
     let x = Name.fresh () in
     let desc = Sig.lookup_datatype dlbl in
     let constr = Desc.lookup_constr clbl desc in
@@ -814,11 +814,11 @@ struct
         make_fhcom (`Ok dir) intro @@ force_abs_sys correction
     end
 
-  and rigid_coe_data dir abs el =
+  and rigid_coe_nonstrict_data dir abs el =
     let _, tyx = Abs.unleash1 abs in
     match unleash tyx, unleash el with
     | Data dlbl, Intro info ->
-      rigid_coe_data_intro dir abs ~dlbl ~clbl:info.clbl ~const_args:info.const_args ~rec_args:info.rec_args ~rs:info.rs
+      rigid_coe_nonstrict_data_intro dir abs ~dlbl ~clbl:info.clbl ~const_args:info.const_args ~rec_args:info.rec_args ~rs:info.rs
 
     | Data _, Up info ->
       rigid_ncoe_up dir abs info.neu ~rst_sys:info.sys
@@ -835,7 +835,7 @@ struct
       rigid_fhcom info.dir cap sys
 
     | _ ->
-      failwith "rigid_coe_data"
+      failwith "rigid_coe_nonstrict_data"
 
   and rigid_coe dir abs el =
     let x, tyx = Abs.unleash1 abs in
@@ -853,8 +853,10 @@ struct
     | Univ _ ->
       el
 
-    | Data _ ->
-      rigid_coe_data dir abs el
+    | Data dlbl ->
+      let desc = Sig.lookup_datatype dlbl in
+      if Desc.is_strict_set desc then el
+      else rigid_coe_nonstrict_data dir abs el
 
     | FHCom fhcom ->
       (* [F]: favonia 11.00100100001111110110101010001000100001011.

From 135c9ea68f850234c6516ab519aeb9682d37ac6e Mon Sep 17 00:00:00 2001
From: favonia <favonia@gmail.com>
Date: Sat, 18 Aug 2018 13:22:52 +0800
Subject: [PATCH 4/6] More progress on Omega1(S1).

---
 example/omega1s1-wip.red | 39 +++++++++++++++------------------------
 1 file changed, 15 insertions(+), 24 deletions(-)

diff --git a/example/omega1s1-wip.red b/example/omega1s1-wip.red
index 55fc638c0..705073d01 100644
--- a/example/omega1s1-wip.red
+++ b/example/omega1s1-wip.red
@@ -17,37 +17,28 @@ let loopn (n : int) : Path s1 base base =
   | pos n ⇒
     elim n [
     | zero ⇒ auto
-    | suc (n ⇒ loopn) ⇒ trans s1 (λ i → loop i) loopn
+    | suc (n ⇒ loopn) ⇒ trans s1 loopn (λ i → loop i)
     ]
   | negsuc n ⇒
     elim n [
     | zero ⇒ symm s1 (λ i → loop i)
-    | suc (n ⇒ loopn) ⇒ trans s1 (symm s1 (λ i → loop i)) loopn
+    | suc (n ⇒ loopn) ⇒ trans s1 loopn (symm s1 (λ i → loop i))
     ]
   ]
 
 let winding (l : Path s1 base base) : int =
   coe 0 1 (pos zero) in λ i → s1-univ-cover (l i)
 
-let two : int = pos (suc (suc zero))
-
-let winding-loop-testing0 : Path int two (winding (loopn two)) =
-  auto
-
-let nat/five : nat =
-  suc (suc (suc (suc (suc zero))))
-
-let nat/25 : nat =
-  plus nat/five (plus nat/five (plus nat/five (plus nat/five nat/five)))
-
-let int/50 : int =
-  pos (plus nat/25 nat/25)
-
-let int/5 : int = pos nat/five
-
-let winding-test/5 : Path int int/5 (winding (loopn int/5)) =
-  auto
-
-let winding-test/50 : Path int int/50 (winding (loopn int/50)) =
-  auto
-
+let winding-loopn (n : int) : Path int (winding (loopn n)) n =
+  elim n [
+  | pos n ⇒
+    elim n [
+    | zero ⇒ auto
+    | suc (n ⇒ loopn) ⇒ λ i → isuc (loopn i)
+    ]
+  | negsuc n ⇒
+    elim n [
+    | zero ⇒ auto
+    | suc (n ⇒ loopn) ⇒ λ i → pred (loopn i)
+    ]
+  ]

From bbd1b84375408c3b69c0400cae479fa976d564d2 Mon Sep 17 00:00:00 2001
From: favonia <favonia@gmail.com>
Date: Sat, 18 Aug 2018 16:12:57 +0800
Subject: [PATCH 5/6] Put the speed testing back.

---
 example/omega1s1-wip.red | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)

diff --git a/example/omega1s1-wip.red b/example/omega1s1-wip.red
index 705073d01..07042e976 100644
--- a/example/omega1s1-wip.red
+++ b/example/omega1s1-wip.red
@@ -42,3 +42,28 @@ let winding-loopn (n : int) : Path int (winding (loopn n)) n =
     | suc (n ⇒ loopn) ⇒ λ i → pred (loopn i)
     ]
   ]
+
+
+; speed test
+
+let two : int = pos (suc (suc zero))
+
+let winding-loop-testing0 : Path int two (winding (loopn two)) =
+  auto
+
+let nat/five : nat =
+  suc (suc (suc (suc (suc zero))))
+
+let nat/25 : nat =
+  plus nat/five (plus nat/five (plus nat/five (plus nat/five nat/five)))
+
+let int/50 : int =
+  pos (plus nat/25 nat/25)
+
+let int/5 : int = pos nat/five
+
+let winding-test/5 : Path int int/5 (winding (loopn int/5)) =
+  auto
+
+let winding-test/50 : Path int int/50 (winding (loopn int/50)) =
+  auto

From 8e034370257a382f93e4ec61a5069dce452e0d6a Mon Sep 17 00:00:00 2001
From: favonia <favonia@gmail.com>
Date: Mon, 20 Aug 2018 16:45:22 +0200
Subject: [PATCH 6/6] Revert "Put the speed testing back."

This reverts commit bbd1b84375408c3b69c0400cae479fa976d564d2.
---
 example/omega1s1-wip.red | 25 -------------------------
 1 file changed, 25 deletions(-)

diff --git a/example/omega1s1-wip.red b/example/omega1s1-wip.red
index 07042e976..705073d01 100644
--- a/example/omega1s1-wip.red
+++ b/example/omega1s1-wip.red
@@ -42,28 +42,3 @@ let winding-loopn (n : int) : Path int (winding (loopn n)) n =
     | suc (n ⇒ loopn) ⇒ λ i → pred (loopn i)
     ]
   ]
-
-
-; speed test
-
-let two : int = pos (suc (suc zero))
-
-let winding-loop-testing0 : Path int two (winding (loopn two)) =
-  auto
-
-let nat/five : nat =
-  suc (suc (suc (suc (suc zero))))
-
-let nat/25 : nat =
-  plus nat/five (plus nat/five (plus nat/five (plus nat/five nat/five)))
-
-let int/50 : int =
-  pos (plus nat/25 nat/25)
-
-let int/5 : int = pos nat/five
-
-let winding-test/5 : Path int int/5 (winding (loopn int/5)) =
-  auto
-
-let winding-test/50 : Path int int/50 (winding (loopn int/50)) =
-  auto