Merge pull request #334 from math-comp/instance-before-structure

saturate instances on structure declaration

Author: gares

Changelog.md

@@ -3,6 +3,7 @@
 ## Unreleased
 
 - **Removed** the `#[primitive_class]` attribute, making it the default.
+- **New** `HB.saturate` to saturate instances w.r.t. the current hierarchy
 
 ## [1.6.0] - 2023-09-20
 

HB/common/database.elpi

@@ -133,6 +133,38 @@ factories-provide FLwP MLwP :- std.do! [
   w-params.map UnsortedMLwP (p\t\ toposort-mixins) MLwP,
 ].
 
+pred undup-grefs  i:list gref, o:list gref.
+undup-grefs  L UL :- std.do! [
+  coq.gref.list->set L S, 
+  coq.gref.set.elements S UL,
+].
+
+pred undup-sorts i:list sort, o:list sort.
+undup-sorts L R :- std.do! [
+  
+  if (std.mem L prop) (R1 = [prop]) (R1 = []),
+  if (std.mem L sprop) (R2 = [sprop]) (R2 = []),
+  if (std.mem L (typ _)) (R3 = [typ _]) (R3 = []),
+  
+  std.flatten [R1, R2, R3] R,
+].
+
+% also prunes cs-default
+pred undup-cs-patterns  i:list cs-pattern, o:list cs-pattern.
+undup-cs-patterns L R :- std.do! [
+  std.map-filter L (x\r\ x = cs-gref r) LGR,
+  undup-grefs LGR ULGR,
+  std.map ULGR (x\r\ r = cs-gref x) R1,
+
+  std.map-filter L (x\r\ x = cs-sort r) LS,
+  undup-sorts LS ULS,
+  std.map ULS (x\r\ r = cs-sort x) R2,
+
+  if (std.mem L cs-prod) (R3 = [cs-prod]) (R3 = []),
+
+  std.flatten [R1, R2, R3] R,
+].
+
 % Mixins can be topologically sorted according to their dependencies
 pred toposort-mixins i:list (w-args mixinname), o:list (w-args mixinname).
 toposort-mixins In Out :- std.do! [
@@ -192,6 +224,13 @@ findall-builders LFIL :-
   std.map {std.findall (builder-decl B_)} extract-builder LFILunsorted,
   std.bubblesort LFILunsorted leq-builder LFIL.
 
+pred findall-has-mixin-instance o:list prop.
+findall-has-mixin-instance CL :-
+   std.findall (has-mixin-instance  _ _ _) CL.
+
+pred has-mixin-instance_key i:prop, o:cs-pattern.
+has-mixin-instance_key (has-mixin-instance P _ _) P.
+
 pred findall-mixin-src i:term, o:list mixinname.
 findall-mixin-src T ML :-
   std.map {std.findall (mixin-src T M_ V_)} mixin-src_mixin ML.
@@ -299,7 +338,7 @@ get-constructor (indt R) (indc K) :- !,
  if (coq.env.indt R _ _ _ _ [K] _) true (coq.error "Not a record" R).
 get-constructor I _ :- coq.error "get-constructor: not an inductive" I.
 
-%% finding for locally defined structures
+% finding for locally defined structures
 pred get-cs-structure i:cs-instance, o:structure.
 get-cs-structure (cs-instance _ _ (const Inst)) Struct :- std.do! [
   coq.env.typeof (const Inst) InstTy,
@@ -313,17 +352,64 @@ get-cs-instance (cs-instance _ _ (const Inst)) Inst.
 pred has-cs-instance i:gref, i:cs-instance.
 has-cs-instance GTy (cs-instance _ (cs-gref GTy) _).
 
-pred term->cs-pattern i:term, o:cs-pattern.
-term->cs-pattern (prod _ _ _) cs-prod.
-term->cs-pattern (sort U) (cs-sort U).
-term->cs-pattern T (cs-gref GR) :- term->gref T GR.
-term->cs-pattern T _ :- coq.error T "HB database: is not a valid canonical key".
-
-pred cs-pattern->name i:cs-pattern, o:string.
-cs-pattern->name cs-prod "prod".
-cs-pattern->name (cs-sort _) "sort".
-cs-pattern->name cs-default "default".
-cs-pattern->name (cs-gref GR) Name :- gref->modname-label GR 1 "_" Name.
+
+pred mixin-src->has-mixin-instance i:prop, o:prop.
+mixin-src->has-mixin-instance  (mixin-src (global GR) M I) (has-mixin-instance (cs-gref GR) M IHd) :-
+  term->gref I IHd.
+
+mixin-src->has-mixin-instance (mixin-src (app [global GR|_] ) M I) (has-mixin-instance (cs-gref GR) M IHd) :-
+  term->gref I IHd.
+  
+mixin-src->has-mixin-instance (mixin-src (prod _ _ _ ) M I) (has-mixin-instance cs-prod M IHd):-
+  term->gref I IHd.
+
+mixin-src->has-mixin-instance (mixin-src (sort U) M I) (has-mixin-instance (cs-sort U) M IHd):-
+  term->gref I IHd.
+
+% this auxiliary function iterates over the list of arguments of an application,
+% and create the necessary unify condition for each arguments 
+% and at the end returns the mixin-src clause with all the conditions
+pred mixin-instance-type->mixin-src.aux 
+  i:list term, % list of arguments
+  i:term, % head of the original application
+  i:mixinname, % name of mixin
+  i:term, % instance body
+  i:list prop, % Cond list
+  o:prop.
+mixin-instance-type->mixin-src.aux [] T M I Cond (mixin-src T M I :- Cond).
+mixin-instance-type->mixin-src.aux [A|Args] T M I Cond  (pi a \ C a) :-
+  pi a \
+  sigma Ta\
+    coq.mk-app T [a] Ta,
+    mixin-instance-type->mixin-src.aux Args Ta M I [coq.unify-eq A a ok|Cond] (C a).
+
+
+% transforms the type of a mixin instance into a
+% mixin-src clause with eventual conditions regarding its parameters
+pred mixin-instance-type->mixin-src
+  i:term, % type of the instance Ty
+  i:mixinname, % name of mixin
+  i:term, % instance body I of type Ty
+  i:list prop, % Cond list
+  o:prop.
+
+mixin-instance-type->mixin-src (app _ as F) M I Cond C :-
+  factory? F (triple _ _ Subject),
+  safe-dest-app Subject Hd Args,
+  mixin-instance-type->mixin-src.aux Args Hd M I Cond C.
+
+mixin-instance-type->mixin-src (prod N_ _ F) M I Cond (pi a \ C a) :-
+  pi a\
+  sigma  Ia \
+  coq.mk-app I [a] Ia,
+    mixin-instance-type->mixin-src (F a) M Ia Cond (C a).
+
+pred has-mixin-instance->mixin-src i:prop, o:prop.
+has-mixin-instance->mixin-src (has-mixin-instance _ M IHd) C :- std.do![
+  T = global IHd,
+  coq.env.typeof IHd Ty,
+  mixin-instance-type->mixin-src Ty M T [] C,
+].
 
 pred get-canonical-structures i:term, o:list structure.
 get-canonical-structures TyTrm StructL :- std.do! [

HB/common/stdpp.elpi

@@ -123,6 +123,12 @@ pred coq.env.current-library o:string.
 coq.env.current-library L :- loc.fields {get-option "elpi.loc"} L _ _ _ _.
 coq.env.current-library "dummy.v".
 
+pred coq.term-is-gref? i:term, o:gref.
+coq.term-is-gref? (global GR) GR :- !.
+coq.term-is-gref? (pglobal GR _) GR :- !.
+coq.term-is-gref? (app [Hd|_]) GR :- !, coq.term-is-gref? Hd GR.
+coq.term-is-gref? (let _ _ T x\x) GR :- !, coq.term-is-gref? T GR.
+
 pred coq.prod-tgt->gref i:term, o:gref.
 coq.prod-tgt->gref T GR :- whd1 T T1, !, coq.prod-tgt->gref T1 GR.
 coq.prod-tgt->gref (prod N Src Tgt) GR :- !, @pi-decl N Src x\ coq.prod-tgt->gref (Tgt x) GR.
@@ -245,3 +251,86 @@ coq.fold-map (primitive _ as C) A C A :- !.
 coq.fold-map (uvar M L as X) A W A1 :- var X, !, std.fold-map L A coq.fold-map L1 A1, coq.mk-app-uvar M L1 W.
 % when used in CHR rules
 coq.fold-map (uvar X L) A (uvar X L1) A1 :- std.fold-map L A coq.fold-map L1 A1.
+
+pred cs-pattern->term i:cs-pattern, o:term.
+cs-pattern->term (cs-gref GR) T :- coq.env.global GR T.
+cs-pattern->term (cs-sort prop) (sort prop).
+cs-pattern->term (cs-sort sprop) (sort sprop).
+cs-pattern->term (cs-sort _) T :- coq.elaborate-skeleton {{ Type }} _ T ok.
+cs-pattern->term cs-prod T :- coq.elaborate-skeleton (prod `x` Ty_ x\ Bo_ x) _ T ok.
+
+pred term->cs-pattern i:term, o:cs-pattern.
+term->cs-pattern (prod _ _ _) cs-prod.
+term->cs-pattern (sort U) (cs-sort U).
+term->cs-pattern T (cs-gref GR) :- coq.term->gref T GR.
+term->cs-pattern T _ :- coq.error T "HB database: is not a valid canonical key".
+
+pred cs-pattern->name i:cs-pattern, o:string.
+cs-pattern->name cs-prod "prod".
+cs-pattern->name (cs-sort _) "sort".
+cs-pattern->name cs-default "default".
+cs-pattern->name (cs-gref GR) Name :- gref->modname-label GR 1 "_" Name.
+
+% ---------------------------------------------------------------------
+% kit for closing a term by abstracting evars with lambdas
+% we use constraints to attach to holes a number
+% and replace them by a special node, to later be bound
+% via a lambda
+
+namespace abstract-holes {
+
+% we add a new constructor to terms to represent terms to be abstracted
+type abs int -> term.
+
+% bind back abstracted subterms
+pred bind i:int, i:int, i:term, o:term.
+bind I M T T1 :- M > I, !,
+  T1 = {{ fun x => lp:(B x) }},   
+  N is I + 1,
+  pi x\                           % we allocate the fresh symbol for (abs M)
+    (copy (abs N) x :- !) =>      % we schedule the replacement (abs M) -> x
+    bind N M T (B x).
+bind M M T T1 :- copy T T1.         % we perform all the replacements
+
+% for a term with M holes, returns a term with M variables to fill these holes
+% the clause see is only generated for a term if it hasn't been seen before
+% the term might need to be typechecked first or main generates extra holes for the
+% type of the parameters
+pred main i:term, o:term.
+main T1 T3 :- std.do! [
+  % we put (abs N) in place of each occurrence of the same hole
+  (pi T Ty N N' M \ fold-map T N (abs M) M :- var T, not (seen? T _), !, coq.typecheck T Ty ok, fold-map Ty N _ N', M is N' + 1, seen! T M) =>
+  (pi T N M \ fold-map T N (abs M) N :- var T, seen? T M, !) =>
+    fold-map T1 0 T2 M,
+  % we abstract M holes (M abs nodes)
+  bind 0 M T2 T3,
+  % cleanup constraint store
+  purge-seen!,
+].
+
+% all constraints are also on _ so that they share
+% a variable with the constraint to purge the store
+
+% we query if the hole was seen before, and if so
+% we fetch its number
+pred seen? i:term, o:int.
+seen? X Y :- declare_constraint (seen? X Y) [X,_].  
+
+% we declare it is now seen and label it with a number
+pred seen! i:term, i:int.
+seen! X Y :- declare_constraint (seen! X Y) [X,_].
+
+% to empty the store
+pred purge-seen!.
+purge-seen! :- declare_constraint purge-seen! [_].
+
+constraint seen? seen! purge-seen!  {
+  % a succesful query, give the label back via M
+  rule (seen! X N) \ (seen? X M) <=> (M = N).
+  % an unsuccesful query
+  rule             \ (seen? X _) <=> false.
+
+  rule purge-seen! \ (seen! _ _).
+  rule \ purge-seen!.
+}
+}

HB/common/utils.elpi

@@ -374,4 +374,11 @@ prod-last X X :- !.
 
 pred prod-last-gref i:term, o:gref.
 prod-last-gref (prod N S X) GR :- !, @pi-decl N S x\ prod-last-gref (X x) GR.
-prod-last-gref X GR :- coq.term->gref X GR.
+prod-last-gref X GR :- coq.term->gref X GR.
+
+% saturate a type constructor with holes
+pred saturate-type-constructor i:term, o:term .
+saturate-type-constructor T ET :- 
+  coq.typecheck T TH ok,
+  coq.count-prods TH N,
+  coq.mk-app T {coq.mk-n-holes N} ET.

HB/factory.elpi

@@ -53,7 +53,7 @@ argument->w-mixins (ctx-decl Decl) (pr MLwP ArgwP) :- !, std.do! [
 pred argument-name i:argument, o:string.
 argument-name (const-decl Id _ _) Id :- !.
 argument-name (indt-decl (parameter _ _ _ R)) Id :- !,
-  argument-name (indt-decl (R (sort prop))) Id.
+argument-name (indt-decl (R (sort prop))) Id.
 argument-name (indt-decl (record Id _ _ _)) Id :- !.
 argument-name (indt-decl (inductive Id _ _ _)) Id :- !.
 argument-name (ctx-decl _) "_" :- !.
@@ -231,7 +231,6 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance
 
   abstract-over-section TheParams TheType MixinSrcClauses SectionCanonicalInstance coq.abstract-indt-decl RDecl RDeclClosed _,
 
-  % coq.say RDecl RDeclClosed,
 
   if (get-option "primitive" tt)
     (@primitive! => log.coq.env.add-indt RDeclClosed R)