Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Coersion in strict data types and Omega1(S1). #250

Merged
merged 6 commits into from
Aug 20, 2018
Merged

Coersion in strict data types and Omega1(S1). #250

Show file tree
Hide file tree
Changes from 4 commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
4bf1b37
Remove something that does not make sense.
favonia Aug 18, 2018
78b6cfc
Type-check fhcom in data types.
favonia Aug 18, 2018
9f31738
Coersion in strict data types should be id.
favonia Aug 18, 2018
135c9ea
More progress on Omega1(S1).
favonia Aug 18, 2018
bbd1b84
Put the speed testing back.
favonia Aug 18, 2018
8e03437
Revert "Put the speed testing back."
favonia Aug 20, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
39 changes: 15 additions & 24 deletions example/omega1s1-wip.red
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This line and the similar line below seem to be causing the trouble.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Heh.. So the issue is that when it associates in one way it is fast, and in the other way infeasible? That's very interesting.

Copy link
Collaborator Author

@favonia favonia Aug 18, 2018 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It somewhat makes sense. I changed the order to make the lemma easier to prove. The new one produces isuc from the outside and is perfect for induction.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Shall we try a harder version of the lemma? I guess analogous to tail recursive function

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This performance asymmetry also exists in cubicaltt, btw.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I guess to prove the "fast" version, it will take some gnarly coercion. Sadly, the goals are tens of thousands of lines long, so it's a little hard to tell what needs to be done.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@favonia Can you elaborate on why it makes sense? I guess the performance of coe in fcom depends more on the complexity of the tubes than that of the cap?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@ecavallo I am not sure. I have to think harder.

]
| 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
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Does anyone miss this? I can put it back...

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Let's keep it, just to make sure we do my introduce some really bad performance degradation. We could even move to different file if you felt it was clutter

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Done.


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)
]
]
3 changes: 3 additions & 0 deletions src/core/Typing.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
25 changes: 13 additions & 12 deletions src/core/Val.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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.
Expand Down Expand Up @@ -1358,15 +1360,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 _ ->
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We need a neutral hcom or a neutral ghcom so that a potential eliminator knows how to deal with it.

let aux sys =
match sys with
| [] -> cap
Expand Down