Instance before structure

.gitignore

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

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, subst-fun, safe-dest-app, mk-app, mk-eta, subst-prod }.
+shorten coq.{ term->gref, term-is-gref?, subst-fun, safe-dest-app, mk-app, mk-eta, subst-prod }.
 
 %%%%%%%%% HB database %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
@@ -14,12 +14,29 @@ from_mixin (from _ X _) X.
 pred from_builder i:prop, o:term.
 from_builder (from _ _ X) (global X).
 
+pred has-mixin-instance_cspat i:prop, o:cs-pattern.
+has-mixin-instance_cspat (has-mixin-instance P _ _ _) P.
+
+pred mixin-src_type i:prop, o:term.
+mixin-src_type (mixin-src T _ _ ) T.
+
+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_ty i:prop, o:term.
+mixin-src_ty (mixin-src T _ _ ) Ty :-coq.typecheck T Ty ok.
+
 pred mixin-src_mixin i:prop, o:mixinname.
 mixin-src_mixin (mixin-src _ M _) M.
 
 pred mixin-src_src i:prop, o:term.
 mixin-src_src (mixin-src _ _ S) S.
 
+pred mixin-src_srcty i:prop, o:term.
+mixin-src_src (mixin-src _ _ S) Ty :- coq.env.typeof {coq.prod-tgt->gref S} Ty .
+
 pred local-canonical-gref i:prop, o:constant.
 local-canonical-gref (local-canonical C) C.
 
@@ -32,6 +49,9 @@ class_structure (class _ S _) S.
 pred class-def_name i:prop, o:classname.
 class-def_name (class-def (class N _ _)) N.
 
+pred  has-db-instance_type i:prop, o:term.
+ has-db-instance_type (has-db-instance TheType) TheType.
+
 pred mixin-class_class i:prop, o:classname.
 mixin-class_class (mixin-class _ C) C.
 
@@ -133,6 +153,28 @@ 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-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,
+].
+
+% % finds all unique types for which an instance was created
+pred findall-cs-types o:list term.
+findall-cs-types TypeList :- std.do![
+  std.findall (has-db-instance _) Clauses,
+  std.map Clauses has-db-instance_type TypeListDup,
+  undup-terms TypeListDup TypeList,
+].
+
+
 % 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,10 +234,18 @@ 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 findall-type-src o:list cs-pattern.
+findall-type-src TL :-
+  std.map {std.findall (has-mixin-instance T_ M_ S_ L_)} has-mixin-instance_cspat TL.
+
 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.
@@ -268,6 +318,7 @@ 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
@@ -295,7 +346,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,
@@ -309,6 +360,100 @@ 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 param-in-term i:term, i:constant, o:bool.
+param-in-term  (app [global (const F)]) C tt :- (coq.gref->id (const F) ID), (coq.gref->id (const C) ID).
+param-in-term (app [_|Args]) C B :- param-in-term (app Args) C B.
+param-in-term (app []) _ ff.
+param-in-term (prod _ _ F) C B :-  pi x\ param-in-term (F x) C B.
+param-in-term (sort _) _ ff.
+param-in-term T C B :- whd1 T T1, !, param-in-term  T1 C B.
+
+% given a list of section parameters SectionParams and a term T, 
+% returns a list of bool corresponding to whether or not each parameter appears in T.
+pred sect-params-in-term  i:list constant, i:term, o:list bool.
+sect-params-in-term SectionParams T L :-
+  safe-dest-app T (global GR) Args, 
+  factory-alias->gref GR F, factory-nparams F NP, std.split-at NP Args Params _Args2,
+  TyP = app [global GR|Params],
+  std.map SectionParams (x\ o \ param-in-term TyP x o) L.
+
+pred has-mixin-instance o:cs-pattern, o:mixinname, o:gref, o:list bool.
+
+
+pred mixin-src->has-mixin-instance i:list constant, i:prop, o:prop.
+
+mixin-src->has-mixin-instance SectionParams (mixin-src (global GR) M I) (has-mixin-instance (cs-gref GR) M IHd A) :-
+  term->gref I IHd,  coq.typecheck I Ty ok, sect-params-in-term SectionParams Ty A.
+
+mixin-src->has-mixin-instance SectionParams (mixin-src (app [global GR|_] ) M I) (has-mixin-instance (cs-gref GR) M IHd A) :-
+  term->gref I IHd,  coq.typecheck I Ty ok, sect-params-in-term SectionParams Ty A.
+
+mixin-src->has-mixin-instance SectionParams (mixin-src (prod _ _ _ ) M I) (has-mixin-instance cs-prod M IHd BL):-
+  term->gref I IHd, coq.typecheck I Ty ok, sect-params-in-term SectionParams Ty BL.
+
+mixin-src->has-mixin-instance SectionParams (mixin-src (sort U) M I) (has-mixin-instance (cs-sort U) M IHd BL):-
+  term->gref I IHd, coq.typecheck I Ty ok, sect-params-in-term SectionParams Ty BL.
+
+
+pred mk-src-aux i:list term, i:term, i:mixinname, i:term, i:list prop, o:prop.
+mk-src-aux [] T M I Cond (mixin-src T M I :- Cond).
+mk-src-aux [A|Rest] T M I Cond ( pi a \ C a) :-
+  pi a \
+  sigma Ta\
+    coq.mk-app T [a] Ta,
+    mk-src-aux Rest 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
+  i:term, % type of the instance Ty
+  i:mixinname, % name of mixin
+  i:term, % instance body I of type Ty
+  i:list bool, % list of bool for each param, true if they're instance parameters
+  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.
+
+mk-src (prod N_ _ F) M I [ff|Rest] Cond (pi a \ C a) :-
+  pi a\
+  sigma  Ia \
+  coq.mk-app I [a] Ia,
+    mk-src (F a) M Ia Rest Cond (C a).
+
+mk-src (prod N_ _ F) M I [tt|Rest] Cond C :-
+  sigma a Ia \
+  coq.mk-app I [a] Ia,
+    mk-src (F a) M Ia Rest Cond C.
+
+mk-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).
+
+% 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 L) C :- std.do![
+  T = global IHd,
+  coq.env.typeof IHd Ty,
+  mk-src Ty M T L [] 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).

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.

HB/common/utils.elpi

@@ -372,4 +372,7 @@ 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.
+
+pred prod-structure i:term, o:term.
+prod-structure (prod _ S _) S.

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 _) "_" :- !.