From 0d123890ef9c8124b2f96aa5626fcf4c97642b7b Mon Sep 17 00:00:00 2001 From: Enzo Crance Date: Fri, 12 Jan 2024 17:19:09 +0100 Subject: [PATCH] :memo: Documentation (elpi) --- elpi/annot.elpi | 4 +++- elpi/constraints/constraint-graph.elpi | 1 + elpi/param-class.elpi | 3 ++- elpi/param.elpi | 30 ++++++++++++++++---------- elpi/util.elpi | 2 ++ 5 files changed, 27 insertions(+), 13 deletions(-) diff --git a/elpi/annot.elpi b/elpi/annot.elpi index c33133b..cf8c230 100644 --- a/elpi/annot.elpi +++ b/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. diff --git a/elpi/constraints/constraint-graph.elpi b/elpi/constraints/constraint-graph.elpi index ca9947a..4d5ca30 100644 --- a/elpi/constraints/constraint-graph.elpi +++ b/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') diff --git a/elpi/param-class.elpi b/elpi/param-class.elpi index 26e8818..1250c15 100644 --- a/elpi/param-class.elpi +++ b/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, diff --git a/elpi/param.elpi b/elpi/param.elpi index 815a44e..eee90fe 100644 --- a/elpi/param.elpi +++ b/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,7 +64,7 @@ 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, !, @@ -71,7 +72,7 @@ param X T' X' (W XR) :- name X, !, 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, !, diff --git a/elpi/util.elpi b/elpi/util.elpi index eb48043..fb512f9 100644 --- a/elpi/util.elpi +++ b/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.