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

Replacing almost all locate in Hierarchy.v + refactoring #12

Merged
merged 1 commit into from
Jan 4, 2024
Merged

Replacing almost all locate in Hierarchy.v + refactoring #12

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
68 changes: 44 additions & 24 deletions elpi/param-class.elpi
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,36 +23,47 @@ type map2b map-class.
type map3 map-class.
type map4 map-class.

kind class-kind type.
type low class-kind.
type high class-kind.
type all class-kind.

pred map-classes o:class-kind, o:list map-class.
map-classes all [map0, map1, map2a, map2b, map3, map4].
map-classes low [map0, map1, map2a].
map-classes high [map2b, map3, map4].

pred sym-rel o:gref.
sym-rel {{:gref lib:trocq.sym_rel}}.

pred paths o:gref.
paths {{:gref lib:trocq.paths}}.

kind param-class type.
type pc map-class -> map-class -> param-class.

pred map->class o:map-class, o:gref.
map->class map0 {{:gref lib:trocq.map0}}.
map->class map1 {{:gref lib:trocq.map1}}.
map->class map2a {{:gref lib:trocq.map2a}}.
map->class map2b {{:gref lib:trocq.map2b}}.
map->class map3 {{:gref lib:trocq.map3}}.
map->class map4 {{:gref lib:trocq.map4}}.

pred map-class->indc-class o:map-class, o:gref.
map-class->indc-class map0 {{:gref lib:trocq.indc_map0}}.
map-class->indc-class map1 {{:gref lib:trocq.indc_map1}}.
map-class->indc-class map2a {{:gref lib:trocq.indc_map2a}}.
map-class->indc-class map2b {{:gref lib:trocq.indc_map2b}}.
map-class->indc-class map3 {{:gref lib:trocq.indc_map3}}.
map-class->indc-class map4 {{:gref lib:trocq.indc_map4}}.

pred map-class->term i:map-class, o:term.
map-class->term map0 (pglobal Map0 UI) :-
coq.locate "map0" Map0,
coq.univ-instance UI [].
map-class->term map1 (pglobal Map1 UI) :-
coq.locate "map1" Map1,
coq.univ-instance UI [].
map-class->term map2a (pglobal Map2a UI) :-
coq.locate "map2a" Map2a,
coq.univ-instance UI [].
map-class->term map2b (pglobal Map2b UI) :-
coq.locate "map2b" Map2b,
coq.univ-instance UI [].
map-class->term map3 (pglobal Map3 UI) :-
coq.locate "map3" Map3,
coq.univ-instance UI [].
map-class->term map4 (pglobal Map4 UI) :-
coq.locate "map4" Map4,
coq.univ-instance UI [].
map-class->term Class (pglobal Map UI) :- std.do! [
map-class->indc-class Class Map, coq.univ-instance UI [] ].

pred term->map-class i:term, o:map-class.
term->map-class (pglobal Map0 _) map0 :- coq.locate "map0" Map0.
term->map-class (pglobal Map1 _) map1 :- coq.locate "map1" Map1.
term->map-class (pglobal Map2a _) map2a :- coq.locate "map2a" Map2a.
term->map-class (pglobal Map2b _) map2b :- coq.locate "map2b" Map2b.
term->map-class (pglobal Map3 _) map3 :- coq.locate "map3" Map3.
term->map-class (pglobal Map4 _) map4 :- coq.locate "map4" Map4.
term->map-class (pglobal Map _) Class :- map-class->indc-class Class Map.

pred map-class->string i:map-class, o:string.
map-class->string map0 "0".
Expand All @@ -62,10 +73,19 @@ map-class->string map2b "2b".
map-class->string map3 "3".
map-class->string map4 "4".


pred param-class->string i:param-class, o:string.
param-class->string (pc M N) S :-
S is {map-class->string M} ^ {map-class->string N}.

pred param-class->add-suffix i:param-class, i:string, o:string.
param-class->add-suffix Class P S :- S is P ^ {param-class->string Class}.

pred param-class->add-2-suffix i:string,
i:param-class, i:param-class, i:string, o:string.
param-class->add-2-suffix Sep Class1 Class2 P S :-
S is P ^ {param-class->string Class1} ^ Sep ^ {param-class->string Class2}.

% names of the fields contained in a witness of a given level
pred map-class->fields i:map-class, o:list string.
map-class->fields map0 [].
Expand Down
8 changes: 8 additions & 0 deletions theories/Database.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,11 +20,18 @@ Set Universe Polymorphism.
Unset Universe Minimization ToSet.

Elpi Db trocq.db lp:{{

% trocq.db.rel (pc M N) {{ParamMN.Rel}} {{ParamMN.BuildRel}}
% {{ParamMN.R}} {{ParamMN.covariant}} {{ParamMN.contravariant}}
pred trocq.db.rel o:param-class, o:gref, o:gref,
o:gref, o:gref, o:gref.

pred trocq.db.r o:param-class, o:constant.
:name "default-r"
trocq.db.r C R :- var C, !,
declare_constraint (trocq.db.r C R) [C].

% subsummed by trocq.db.rel
pred trocq.db.gref->class o:gref, o:param-class.

pred trocq.db.ptype o:constant.
Expand Down Expand Up @@ -66,4 +73,5 @@ Elpi Db trocq.db lp:{{
:name "default-gref"
trocq.db.gref _ _ _ _ _ :- do-not-fail, !, false.
trocq.db.gref GR Out _ _ _ :- coq.error "cannot find" GR "at out class" Out.

}}.
Loading
Loading