Fixes and cleanups

Author: gares

.gitignore

@@ -58,4 +58,3 @@ _minted-*
 *.vtc
 
 *.dot
-*.json

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

@@ -1,7 +1,7 @@
 /*        Hierarchy Builder: algebraic hierarchies made easy
     This software is released under the terms of the MIT license              */
 
-shorten coq.{ term->gref, term-is-gref?, subst-fun, safe-dest-app, mk-app, mk-eta, subst-prod }.
+shorten coq.{ term->gref, subst-fun, safe-dest-app, mk-app, mk-eta, subst-prod }.
 
 %%%%%%%%% HB database %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
@@ -14,13 +14,6 @@ from_mixin (from _ X _) X.
 pred from_builder i:prop, o:term.
 from_builder (from _ _ X) (global X).
 
-% for a given clause mixin-src with eventually a condition, 
-% returns the type of the first argument
-pred mixin-src-w-cond_type i:prop, o:term.
-mixin-src-w-cond_type(mixin-src (global G) _ _ :- _) (global G).
-mixin-src-w-cond_type (mixin-src (app [T|_]) _ _ :- _) T.
-mixin-src-w-cond_type (pi x \ (C x)) T :- pi y \ mixin-src-w-cond_type (C y) T.
-
 pred mixin-src_mixin i:prop, o:mixinname.
 mixin-src_mixin (mixin-src _ M _) M.
 
@@ -146,16 +139,31 @@ undup-grefs  L UL :- std.do! [
   coq.gref.set.elements S UL,
 ].
 
-% remove duplicates from a list of terms, but all the terms have to be global references
-pred undup-terms  i:list term, o:list term.
-undup-terms L UL :- std.do! [
-  std.map L coq.term->gref LG,
-  undup-grefs LG ULG,
-  std.map ULG (coq.env.global ) 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).
@@ -220,10 +228,13 @@ 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.
-  
+
 pred findall-local-canonical o:list constant.
 findall-local-canonical CL :-
   std.map {std.findall (local-canonical C_)} local-canonical-gref CL.
@@ -300,7 +311,6 @@ assert-good-coverage! MLSortedRev CNL :- std.do! [
      true
 ].
 
-
 %%%%% Coq Database %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 % [get-structure-coercion S1 S2 F] finds the coecion F from the structure S1 to S2
@@ -359,72 +369,47 @@ mixin-src->has-mixin-instance (mixin-src (sort U) M I) (has-mixin-instance (cs-s
 % 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 mk-src-aux 
+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.
-mk-src-aux [] T M I Cond (mixin-src T M I :- Cond).
-mk-src-aux [A|Args] T M I Cond  (pi a \ C a) :-
+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,
-    mk-src-aux Args Ta M I [coq.unify-eq A a ok|Cond] (C a).
+    mixin-instance-type->mixin-src.aux Args Ta M I [coq.unify-eq A a ok|Cond] (C a).
 
 
-% transforms the has-mixin-instance clause arguments into a
-% mixin-src clause with eventuals conditions regarding its parameters
-pred mk-src
+% 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.
 
-mk-src (app [_|Args]) M I Cond C :-
-  std.last Args Last,
-  safe-dest-app Last Hd ArgsLast,
-  mk-src-aux ArgsLast Hd M I Cond C.
+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.
 
-mk-src (prod N_ _ F) M I Cond (pi a \ C a) :-
+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,
-    mk-src (F a) M Ia Cond (C a).
-
-
-% for a type T, create as many holes as there are foralls and returns that enriched type
-pred enrich-type i:term, o:term .
-enrich-type T ET :- 
-  coq.typecheck T TH ok,
-  coq.count-prods TH N,
-  if (N = 0) (ET = T) (coq.mk-app T {coq.mk-n-holes N} ET).
+    mixin-instance-type->mixin-src (F a) M Ia Cond (C a).
 
-% wrapper for mk-src so it can be called by a map on a list of clauses has-mixin-instance
-pred mk-src-map i:prop, o:prop.
-mk-src-map (has-mixin-instance _ M IHd) C :- std.do![
+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,
-  mk-src Ty M T [] C,
-  ].
-
-pred cs-pattern->term i:cs-pattern, o:term.
-cs-pattern->term (cs-gref GR) (global GR).
-cs-pattern->term (cs-sort U) (sort U).
-
-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.
+  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

@@ -251,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

@@ -375,3 +375,10 @@ 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.
+
+% 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/context.elpi

@@ -73,7 +73,7 @@ postulate-mixin TheType (triple M Ps T) (triple CL MSL MLwP) (triple OutCL [MC|M
 
   MC = mixin-src T M (global (const C)),
   MC => get-option "local" tt =>
-    instance.declare-all-generic-type TheType {findall-classes-for [M]} NewCSL,
+    instance.declare-all TheType {findall-classes-for [M]} NewCSL,
   std.map NewCSL snd NewCL,
   std.append CL NewCL OutCL
   ].