📝 Documentation (elpi)

elpi/annot.elpi

@@ -54,7 +54,7 @@ typecheck T ATy :-
 
 % sub-typing predicate following the sub-typing rules in the article
 pred sub-type i:term, i:term.
-% SubUniv
+% SubSort
 sub-type (app [pglobal (const PType) _, M1, N1]) (app [pglobal (const PType) _, M2, N2]) :-
   trocq.db.ptype PType, !,
   cstr.univ-link C1 M1 N1,
@@ -100,6 +100,7 @@ eq _ _ :- fail.
 % of the output type of T, as an option basically returning some (A,B) for an output type PType A B,
 % and none for output types that are not sorts, because it means values of type T are not type
 % constructors, so their translation will be made at class (0,0)
+% TODO: duplicate code with type->class in param-class.elpi?
 pred classes i:term, o:list param-class, o:option param-class.
 classes T Cs' Out :-
   all-classes T Cs,
@@ -120,6 +121,7 @@ all-classes (app L) Cs :- !,
 all-classes X [] :- (name X ; X = global _ ; X = pglobal _ _), !.
 all-classes X _ :- coq.error "all-classes:" X.
 
+% TODO: discuss limitations
 pred out-class i:term, o:option param-class.
 out-class (app [pglobal (const PType) _, M, N]) (some C) :- trocq.db.ptype PType, !,
   cstr.univ-link C M N.

elpi/constraints/constraint-graph.elpi

@@ -80,6 +80,7 @@ pred add-dep-gref
 add-dep-gref ID GR T GR' GRR IDs (constraint-graph G) (constraint-graph G') :-
   % the classes C_i (IDs) are not really "higher" than the output class C (ID)
   % here, higher is a way to say that they must be instantiated later than the output class
+  % TODO: rename utility functions to add-earlier-node / add-later-node?
   util.map.update ID (internal.add-higher-node (node.var (ct.gref GR T GR' GRR) IDs)) G G1,
   std.fold IDs G1 (id\ g\ g'\
     util.map.update id (internal.add-lower-node (node.var (ct.gref _ _ _ _) [ID])) g g')

elpi/param-class.elpi

@@ -23,6 +23,7 @@ type map2b map-class.
 type map3  map-class.
 type map4  map-class.
 
+% high = axiom might be required (on product and universe)
 kind class-kind type.
 type low class-kind.
 type high class-kind.
@@ -73,7 +74,6 @@ 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}.
@@ -317,6 +317,7 @@ replace-out-ty OutC InT OutT :- std.do! [
 pred requires-axiom i:param-class.
 requires-axiom (pc M N) :- (std.mem! [map2b, map3, map4] M ; std.mem! [map2b, map3, map4] N).
 
+% find classes present in a term
 pred type->class i:term, o:list param-class, o:list term.
 type->class X [Class] Ts :-
   coq.safe-dest-app X HD Ts,

elpi/param.elpi

@@ -32,12 +32,14 @@ pred fresh-type.
 
 % ==================================================================================================
 
-% ParamSub + ParamConst
+% TrocqConv + TrocqConst
 param (global GR) T' (global GR') GrefR :- !,
   util.when-debug dbg.steps (coq.say "param/const" GR "@" T'),
   if (fresh-type) (
     % T' already comes from a call to annot.typecheck in the case for app
     % subtyping will be handled there
+    % (we do not want to annot.typecheck several times a same constant, because it creates
+    %  fresh class variables twice, which would split the information)
     cstr.dep-gref GR T' GR' GRR,
     GrefR = global GRR
   ) (
@@ -48,11 +50,10 @@ param (global GR) T' (global GR') GrefR :- !,
     GrefR = (W (global GRR))
   ).
 
+% universe-polymorphic case
 param (pglobal GR UI) T' (pglobal GR' UI) GrefR :- !,
   util.when-debug dbg.steps (coq.say "param/const" GR "@" T'),
   if (fresh-type) (
-    % T' already comes from a call to annot.typecheck in the case for app
-    % subtyping will be handled there
     cstr.dep-gref GR T' GR' GRR,
     GrefR = pglobal GRR UI
   ) (
@@ -63,15 +64,15 @@ param (pglobal GR UI) T' (pglobal GR' UI) GrefR :- !,
     GrefR = (W (pglobal GRR UI))
   ).
 
-% ParamSub + ParamVar
+% TrocqConv + TrocqVar
 param X T' X' (W XR) :- name X, !,
   util.when-debug dbg.steps (coq.say "param/var" X "@" T'),
   param.store X T X' XR, !,
   util.when-debug dbg.steps (coq.say "param/var: found" X "@" T "~" X' "by" XR),
   annot.sub-type T T', !,
   weakening T T' (wfun W).
 
-% ParamUniv
+% TrocqSort
 param
   (app [pglobal (const PType) UI, MR, NR] as Type) (app [pglobal (const PType) _, M, N])
   Type (app [pglobal (const PParamType) UI1|Args]) :- trocq.db.ptype PType, !, std.do! [
@@ -84,7 +85,7 @@ param
     util.when-debug dbg.full (coq.say "param/type: added dep-type from" C "to" CR),
     coq.univ-instance UI [L],
     coq.univ.variable U L,
-    coq.univ-instance UI1 [L, {coq.univ.variable {coq.univ.super U}}], % {coq.univ.new}
+    coq.univ-instance UI1 [L, {coq.univ.variable {coq.univ.super U}}],
     trocq.db.pparam-type C PParamType,
     util.when-debug dbg.full (coq.say "param/type: suspending proof on" C),
     util.if-suspend C (param-class.requires-axiom C) (
@@ -98,7 +99,11 @@ param
     )
   ].
 
-% ParamLam
+% NB: the calls prune UI [] make sure the universe instance UI does not depend on bound variables
+%     it makes sure they remain fresh variables and Coq-Elpi does not fail for technical reasons
+%     so that Coq can fill them in the end
+
+% TrocqLam
 param (fun N T F) FunTy (fun N' T' F') FunR :- !,
   util.when-debug dbg.steps (coq.say "param/fun" N ":" T "@" FunTy),
   std.assert-ok! (coq.unify-eq FunTy (prod _ T TF)) {std.string.concat " "
@@ -118,7 +123,7 @@ param (fun N T F) FunTy (fun N' T' F') FunR :- !,
   FunR =
     fun N T x\ fun N' T' x'\ fun NR (app [pglobal (const R) UI, T, T', TR, x, x']) xR\ FR x x' xR.
 
-% ParamArrow
+% TrocqArrow
 param
   (prod _ A (_\ B)) (app [pglobal (const PType) _, M, N])
   (prod `_` A' (_\ B')) (app [pglobal (const ParamArrow) UI|Args]) :-
@@ -150,7 +155,7 @@ param
       )
     ].
 
-% ParamPi
+% TrocqPi
 param
   (prod N A B) (app [pglobal (const PType) _, M1, M2])
   (prod N' A' B') (app [pglobal (const ParamForall) UI|Args']) :- trocq.db.ptype PType, !,
@@ -190,14 +195,15 @@ param
       Args' = Args
     ).
 
-% ParamSub for F (argument B in param.args) + ParamApp
+% TrocqConv for F (argument B in param.args) + TrocqApp
 param (app [F|Xs]) B (app [F'|Xs']) (W AppR) :- std.do! [
   util.when-debug dbg.steps (coq.say "param/app" F Xs "@" B),
   annot.typecheck F FTy,
   fresh-type => param F FTy F' FR,
   util.when-debug dbg.full (coq.say "param/app:" F "@" FTy "~" F' "by" FR),
   param.args FTy B Xs Xs' XsR W,
-  coq.subst-fun XsR FR AppR].
+  coq.subst-fun XsR FR AppR
+].
 
 pred param.args i:term, i:term, i:list term, o:list term, o:list term, o:term -> term.
 param.args T B [] [] [] W :- std.do! [
@@ -220,6 +226,8 @@ type wfun (term -> term) -> weakening.
 type wsuspend (term -> term) -> (term -> term) -> weakening.
 
 % generate the weakening function from a type to a sub-type
+% cf definition of weakening in the paper
+% TODO: document suspend
 pred weakening i:term, i:term, o:weakening.
 weakening (app [pglobal (const PType) _, M, N]) (app [pglobal (const PType) _, M', N']) W :-
   trocq.db.ptype PType, !,

elpi/util.elpi

@@ -14,6 +14,7 @@
 % utility predicates
 % -----------------------------------------------------------------------------
 
+% TODO: document
 pred do-not-fail.
 :before "term->gref:fail"
 coq.term->gref _ _ :- do-not-fail, !, false.
@@ -22,6 +23,7 @@ kind or type -> type -> type.
 type inl A -> or A B.
 type inr B -> or A B.
 
+% to set level of verbosity of the tool
 kind debug-level type.
 type dbg.none debug-level.
 type dbg.steps debug-level.