Enter HB.from (from factories)

Author: gares

HB/common/synthesis.elpi

@@ -74,6 +74,13 @@ infer-all-args-let Ps T GR X Diag :- std.do! [
   private.instantiate-all-args-let FT T X Diag,
 ].
 
+pred try-infer-all-args-let i:list term, i:term, i:gref, o:term.
+try-infer-all-args-let Ps T GR X :- std.do! [
+  coq.env.typeof GR Ty,
+  coq.mk-eta (-1) Ty (global GR) EtaF,
+  coq.subst-fun {std.append Ps [T]} EtaF FT,
+  private.try-instantiate-all-args-let FT T X,
+].
 
 % [assert!-infer-mixin TheType M Out] infers one mixin M on TheType and
 % aborts with an error message if the mixin cannot be inferred
@@ -271,6 +278,15 @@ instantiate-all-args-let (fun N Tm F) T (let N Tm X R) Diag :- !, std.do! [
 ].
 instantiate-all-args-let F _ F ok.
 
+pred try-instantiate-all-args-let i:term, i:term, o:term.
+try-instantiate-all-args-let (fun N Tm F) T (let N Tm X R) :- !, std.do! [
+  coq.safe-dest-app Tm (global TmGR) _,
+  factory-alias->gref TmGR M,
+  (mixin-for T M X ; true),
+  (@pi-def N Tm X m\ try-instantiate-all-args-let (F m) T (R m)),
+].
+try-instantiate-all-args-let F _ F.
+
 % [structure-instance->mixin-srcs TheType Structure] finds a CS instance for
 % Structure on TheType (if any) and builds mixin-src clauses for all the mixins
 % which can be candidates from that class instance. It finds instances which are

HB/pack.elpi

@@ -12,7 +12,6 @@ main Ty Args Instance :- std.do! [
   std.assert! (Args = [trm TSkel|FactoriesSkel]) "HB.pack: not enough arguments",
 
   get-constructor Class KC,
-  get-constructor Structure KS,
 
   std.assert-ok! (d\
     (coq.elaborate-ty-skeleton TSkel _ T d, d = ok) ;
@@ -29,30 +28,67 @@ main Ty Args Instance :- std.do! [
         (AllFactories = Factories)
       (AllFactories = Factories, Tkey = T), % it's a factory, won't add anything
 
-  private.synth-instance Params KC KS T Tkey AllFactories Instance,
+  private.synth-instance Params KC Tkey AllFactories ClassInstance,
+
+  get-constructor Structure KS,
+  std.append Params [T, ClassInstance] InstanceArgs,
+  Instance = app[global KS | InstanceArgs]
 
 ].
 
+pred main-use-factories i:term, i:list argument, o:term.
+main-use-factories Ty FactoriesSkel ClassInstance :- std.do! [
+  std.assert! (not(var Ty)) "HB.from: the class cannot be unknown",
+
+  factory? {unwind {whd Ty []}} (triple Class Params T),
+
+  std.assert! (class-def (class Class _ _)) "HB.from: not a class",
+
+  get-constructor Class KC,
+
+  private.elab-factories FactoriesSkel T Factories,
+
+  if (var T) (coq.error "HB.from: you must pass a type or at least one factory") true,
+
+  if2 (T = app[global (const SortProj)|ProjParams], structure-key SortProj ClassProj _)
+        (AllFactories = [app[global (const ClassProj)|ProjParams] | Factories], Tkey = T) % already existing class on T
+      (def T _ _ Tkey) % we unfold letins if we can, they may hide constants with CS instances
+        (AllFactories = Factories)
+      (AllFactories = Factories, Tkey = T), % it's a factory, won't add anything
+
+  private.try-synth-instance Params KC Tkey AllFactories ClassInstance,
+  
+].
+
+
 /* ------------------------------------------------------------------------- */
 /* ----------------------------- private code ------------------------------ */
 /* ------------------------------------------------------------------------- */
 
 namespace private {
 
-pred synth-instance i:list term, i:gref, i:gref, i:term, i:term, i:list term, o:term.
-synth-instance Params KC KS T Tkey [Factory|Factories] Instance :-
+pred synth-instance i:list term, i:gref, i:term, i:list term, o:term.
+synth-instance Params KC Tkey [Factory|Factories] ClassInstance :-
   synthesis.under-new-mixin-src-from-factory.do! Tkey Factory (_\
-    synth-instance Params KC KS T Tkey Factories Instance).
-synth-instance Params KC KS T Tkey [] Instance :- coq.safe-dest-app Tkey (global _) _, !,
+    synth-instance Params KC Tkey Factories ClassInstance).
+synth-instance Params KC Tkey [] ClassInstance :- coq.safe-dest-app Tkey (global _) _, !,
   synthesis.under-local-canonical-mixins-of.do! Tkey [
     std.assert-ok! (synthesis.infer-all-args-let Params Tkey KC ClassInstance) "HB.pack: cannot infer the instance",
-    std.append Params [T, ClassInstance] InstanceArgs,
-      Instance = app[global KS | InstanceArgs]
 ].
-synth-instance Params KC KS T Tkey [] Instance :- std.do! [
+synth-instance Params KC Tkey [] ClassInstance :- std.do! [
   std.assert-ok! (synthesis.infer-all-args-let Params Tkey KC ClassInstance) "HB.pack: cannot infer the instance",
-  std.append Params [T, ClassInstance] InstanceArgs,
-    Instance = app[global KS | InstanceArgs]
+].
+
+pred try-synth-instance i:list term, i:gref, i:term, i:list term, o:term.
+try-synth-instance Params KC Tkey [Factory|Factories] ClassInstance :-
+  synthesis.under-new-mixin-src-from-factory.do! Tkey Factory (_\
+    try-synth-instance Params KC Tkey Factories ClassInstance).
+try-synth-instance Params KC Tkey [] ClassInstance :- coq.safe-dest-app Tkey (global _) _, !,
+  synthesis.under-local-canonical-mixins-of.do! Tkey [
+    synthesis.try-infer-all-args-let Params Tkey KC ClassInstance,
+].
+try-synth-instance Params KC Tkey [] ClassInstance :- std.do! [
+  synthesis.try-infer-all-args-let Params Tkey KC ClassInstance,
 ].
 
 pred elab-factories i:list argument, i:term, o:list term.

structures.v

@@ -539,6 +539,29 @@ solve (goal _ _ Ty _ Args as G) GLS :- with-attributes (with-logging (std.do! [
 Elpi Typecheck.
 Elpi Export HB.pack.
 
+Elpi Tactic HB.from.
+Elpi Accumulate Db hb.db.
+Elpi Accumulate File "HB/common/stdpp.elpi".
+Elpi Accumulate File "HB/common/database.elpi".
+#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
+#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
+Elpi Accumulate File "HB/common/utils.elpi".
+Elpi Accumulate File "HB/common/log.elpi".
+Elpi Accumulate File "HB/common/synthesis.elpi".
+Elpi Accumulate File "HB/pack.elpi".
+Elpi Accumulate lp:{{
+
+solve (goal _ _ Ty _ Args as G) GLS :- with-attributes (with-logging (std.do! [
+  pack.main-use-factories Ty Args Instance,
+  refine Instance G GLS,
+])).
+
+}}.
+Elpi Typecheck.
+
+Tactic Notation "HB.from" open_constr_list(L) :=
+  elpi HB.from ltac_term_list:(L).
+
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)

theories/cat.v

@@ -1056,16 +1056,15 @@ split=> [] sq.
 
     pose red := @from _ (pb_terminal sq_ispb) blue_red_black_square.
 
-    
+    admit.
 
 
 
   have p2 : prepullback_isTerminal.axioms_ Q C B  (Cospan (h \; f) g) (Span w (z \; v)) p1.
     constructor. econstructor=> /=.
+    admit.
 
-  pose xx : Pullback.type (Cospan (h \; f) g) :=
-    HB.pack (Span w (z \; v)) p2 p1.
-  apply: Pullback.class xx.
+    by HB.from p1 p2.
 
 Admitted.
 
@@ -1079,7 +1078,8 @@ Variables (Q : precat) (A B : Q) (c : cospan A B).
 Variable (p : pullback c).
 Check pb_terminal p : terminal _.
 
-
+End test.
+End test.