diff --git a/HB/common/database.elpi b/HB/common/database.elpi index 2ecaf7ae..29940537 100644 --- a/HB/common/database.elpi +++ b/HB/common/database.elpi @@ -433,9 +433,9 @@ has-CS-instance? TyTerm (indt Struct) :- coq.CS.db-for (const Proj) Pat L, not(L = []). -pred structure-nparams i:structure, o:int. +func structure-nparams structure -> int. structure-nparams Structure NParams :- - class-def (class Class Structure _), + class-def (class Class Structure _), !, factory->nparams Class NParams. func factory? term -> w-args factoryname. diff --git a/HB/common/stdpp.elpi b/HB/common/stdpp.elpi index 1d56dac1..ff15b709 100644 --- a/HB/common/stdpp.elpi +++ b/HB/common/stdpp.elpi @@ -150,6 +150,12 @@ constraint print-ctx mixin-src { %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +func coq.mk-n-fun int, (func list term -> term), list term -> term. +coq.mk-n-fun 0 F L R :- !, F {std.rev L} R. +coq.mk-n-fun N F L (fun _ _ (x\ R x)) :- + calc (N - 1) N1, + pi x\ coq.mk-n-fun N1 F [x|L] (R x). + func coq.term-is-gref? term -> gref. coq.term-is-gref? (global GR) GR. coq.term-is-gref? (pglobal GR _) GR. @@ -364,4 +370,4 @@ constraint seen? seen! purge-seen! { rule purge-seen! \ (seen! _ _). rule \ purge-seen!. } -} \ No newline at end of file +} diff --git a/HB/factory.elpi b/HB/factory.elpi index cd8794b9..85759229 100644 --- a/HB/factory.elpi +++ b/HB/factory.elpi @@ -269,7 +269,6 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance coq.env.indt R tt _ _ _ [K] _, GRK = indc K, @global! => log.coq.arguments.set-implicit (indt R) [[]], - @global! => log.coq.arguments.set-implicit GRK [[]], factories-provide GRFSwP MLwP, w-params.nparams MLwP NParams, @@ -283,9 +282,11 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance if-verbose (coq.say {header} "declare notation Build"), + GRDepsClauses => coq.env.add-const "Axioms" (global GRK) _ ff GRK0, GRDepsClauses => phant.of-gref ff GRK [] PhGRK, - GRDepsClauses => phant.add-abbreviation "Build" PhGRK BuildConst BuildAbbrev, - + GRDepsClauses => phant.add-abbreviation "Build_" PhGRK BuildConst BuildAbbrev, + calc (NParams + 1) NParams1, + GRDepsClauses => coq.notation.add-abbreviation "Build" NParams1 {coq.mk-n-fun NParams1 (args\ coq.mk-app (global (const GRK0)) {std.append args {coq.mk-n-holes {std.length {list-w-params_list MLwP}}}}) []} tt _, if-verbose (coq.say {header} "declare notation axioms"), if (D = asset-mixin) @@ -297,6 +298,8 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance if-verbose (coq.say {header} "start module Exports"), log.coq.env.begin-module "Exports" none, + coq.TC.declare-class (indt R), + coq.TC.override-solver "TC.Solver" ["axioms_"], std.flatten [Clauses, GRDepsClauses, [ is-factory (indt R), factory->constructor (indt R) GRK, @@ -309,8 +312,19 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance list-w-params_list MLwP MLwoP, std.map MLwoP (_\ r\ r = maximal) Implicits, + std.map {std.iota NParams} (_\ r\ r = explicit) Explicits, /* std.map {list-w-params_list MLwP} (_\ r\ r = maximal) Implicits, */ @global! => log.coq.arguments.set-implicit GRK [[maximal|Implicits]], + + + NewImplicits = [explicit|{std.append Explicits Implicits}], + coq.arguments.set-default-implicit GRK, + coq.arguments.implicit GRK [GRKImplicits|_], + std.drop {std.length NewImplicits} GRKImplicits RImplicits, + + if (std.forall RImplicits(x\ x = explicit)) + (@global! => log.coq.arguments.set-implicit (const GRK0) [NewImplicits]) + (@global! => log.coq.arguments.set-implicit (const GRK0) [NewImplicits, {std.append NewImplicits RImplicits}]), % @global! => log.coq.coercion.declare FactorySortCoe, log.coq.env.end-module-name "Exports" Exports, @@ -351,6 +365,7 @@ declare-factory-alias MixinSrcClauses SectionCanonicalInstance log.coq.env.end-section-name Module, + % TODO: make the mixins implicit. @global! => log.coq.arguments.set-implicit GRK [[]], factories-provide GRFSwP MLwP, @@ -363,7 +378,8 @@ declare-factory-alias MixinSrcClauses SectionCanonicalInstance if (mixin->first-class F _) (PhGRK = PhGRK0) (phant.append-fun-unify PhGRK0 PhGRK), - GRDepsClauses => phant.add-abbreviation "Build" PhGRK _ _, + @global! => log.coq.arguments.set-implicit GRK [[]], + GRDepsClauses => coq.notation.add-abbreviation "Build" 0 (global GRK) tt _, GRDepsClauses => mk-factory-abbrev "axioms" (const C) Clauses FactAbbrev, @@ -436,4 +452,4 @@ mk-factory-sort.term GR P T (fun `_` Ty _\ T) :- synthesis.infer-all-gref->deps -}} \ No newline at end of file +}} diff --git a/HB/instance.elpi b/HB/instance.elpi index f7f6eb1a..ef5cc766 100644 --- a/HB/instance.elpi +++ b/HB/instance.elpi @@ -18,6 +18,24 @@ declare-existing T0 F0 :- std.do! [ acc-clauses current Clauses, ]. +func elaborate-w-tc term -> term, term, diagnostic. +elaborate-w-tc (fun N BTy Skel) (prod N BTy Ty) (fun N BTy Body) Diag :- + @pi-decl N BTy x\ elaborate-w-tc (Skel x) (Ty x) (Body x) Diag. +elaborate-w-tc (app [KFactory|Args]) Ty Body Diag :- + coq.typecheck KFactory TyFactory ok, + coq.prod-tgt->gref TyFactory Factory, + factory->nparams Factory NParams, + std.length {list-w-params_list {gref->deps Factory}} NDeps, + calc (NParams + NDeps + 1) N, + N =< {std.length Args}, + std.split-at N Args NArgs Rest, + std.assert-ok! (coq.elaborate-skeleton (app [KFactory|NArgs]) _ Head) "tc resolution of mixins failed", + coq.elaborate-skeleton {coq.mk-app Head Rest} Ty Body Diag. + + + + + % [declare-const N B Ty CFL CSL] adds a Definition N : Ty := B where Ty is a factory % and equips the type the factory is used on with all the canonical structures % that can be built using factory instance B. CFL contains the list of @@ -26,7 +44,7 @@ func declare-const id, term, arity -> list (pair id constant), list (pair id con declare-const Name BodySkel TyWPSkel CFL CSL :- std.do! [ std.assert-ok! (coq.elaborate-arity-skeleton TyWPSkel _ TyWP) "Definition type illtyped", coq.arity->term TyWP Ty, - std.assert-ok! (coq.elaborate-skeleton BodySkel Ty Body) "Definition illtyped", + std.assert-ok! (d\ elaborate-w-tc BodySkel Ty Body d; coq.elaborate-skeleton BodySkel Ty Body d) "Definition illtyped", % handle parameters via a section -- begin if (TyWP = arity SectionTy) ( diff --git a/HB/structure.elpi b/HB/structure.elpi index 52036dfd..a554967d 100644 --- a/HB/structure.elpi +++ b/HB/structure.elpi @@ -49,6 +49,8 @@ declare Module BSkel Sort :- std.do! [ std.map ML (m\ o\ o = mixin-class m ClassName) MixinMems, std.filter ML (m\ not (mixin->first-class m _)) NewMixins, std.map NewMixins (m\ r\ r = mixin->first-class m ClassName) MixinFirstClass, + [class-def CurrentClass, StructKeyClause | GRDepsClauses] => MixinFirstClass => Factories => std.map-i ML (private.mixin-clause Structure) OptMixinClauses, + std.map-filter OptMixinClauses (c\c'\ c = some c') MixinClauses, if-verbose (coq.say {header} "structure: new mixins" NewMixins), @@ -126,10 +128,12 @@ declare Module BSkel Sort :- std.do! [ std.flatten [ Factories, [is-structure Structure], NewJoins, [class-def CurrentClass], GRDepsClauses, - [gref->deps GRPack MLwP], MixinMems, [StructKeyClause] + [gref->deps GRPack MLwP], MixinMems, [StructKeyClause], ] NewClauses, acc-clauses current NewClauses, + std.map MixinClauses (c\ r\ r = clause _ _ c) MixinClauses0, + coq.elpi.accumulate-clauses current "tc.db" MixinClauses0, if-verbose (coq.say {header} "stop module Exports"), log.coq.env.end-module-name "Exports" Exports, @@ -195,6 +199,52 @@ namespace private { shorten coq.{ term->gref, subst-fun, safe-dest-app, mk-app, mk-eta, subst-prod }. +func clause.mk-n-pis int, list term, (func list term -> prop) -> prop. +clause.mk-n-pis 0 RArgs P Clause :- !, std.rev RArgs Args, P Args Clause. +clause.mk-n-pis N Args P (pi x\ Clause x) :- + calc (N - 1) N0, + pi x\ clause.mk-n-pis N0 [x|Args] P (Clause x). + +func mixin-clause structure, int, mixinname -> option prop. +mixin-clause S I M Clause :- + structure-key SortProj _ S, !, + get-constructor S KS, + class-def (class (indt Class) S CMLwP), !, + if (not (mixin->first-class M (indt Class))) (Clause = none) ( + get-constructor (indt Class) KC, + tc.gref->pred-name M PredName, + gref->deps M MDeps, + +% tc-...-NModule_isLSemiModule.tc-axioms_ R T isNModule Inst :- +% coq.unify-eq T (Sort R ST) ok, +% coq.unify-eq ST (S.Pack R T CT) ok, +% coq.unify-eq CT (C.Axioms_ R T isNModule NModule_isLSemiModule), +% std.nth 1 [isNModule, NModule_isLSemiModule] Inst. + clause.mk-n-pis {structure-nparams S} [] (Params\ clause\ + clause.mk-n-pis {factory->nparams M} [] (MParams\ clause\ + clause.mk-n-pis {std.length {list-w-params_list CMLwP}} [] (MIL\ clause\ + clause.mk-n-pis {std.length {list-w-params_list MDeps}} [] (MHDeps\ clause\ + sigma Clause' MILI\ + std.take I MIL MILI, + clause = (pi T ST CT Inst\ Clause' T ST CT Inst), + pi T ST CT Inst\ sigma ParamsST SortParamsST KSParamsC CBody C\ + std.append Params [ST] ParamsST, + coq.mk-app (global (const SortProj)) ParamsST SortParamsST, + coq.mk-app (global KS) {std.append Params [T, CT]} KSParamsC, + coq.mk-app (global KC) {std.append Params [T | MIL]} CBody, + coq.elpi.predicate PredName {std.append MParams {std.append [T | MHDeps] [Inst]}} C, + Clause' T ST CT Inst = (C :- + coq.unify-eq T SortParamsST ok, + coq.unify-eq ST KSParamsC ok, + coq.unify-eq CT CBody ok, + std.nth I MIL Inst) + ) clause) clause) clause) Clause', + Clause = some Clause'). + + + + + % const Po : forall p1 .. pm T m1 .. mn, Extra (Eg Extra = forall x y, x + y = y + z) % const C : forall p1 .. pm s, Extra % Po P1 .. PM T M1 .. MN PoArgs -> C P1 .. PM S PoArgs diff --git a/HB/structures.v b/HB/structures.v index 90fcb358..7bfdfc19 100644 --- a/HB/structures.v +++ b/HB/structures.v @@ -20,7 +20,11 @@ Definition ignore {T} (x: T) := x. Definition ignore_disabled {T T'} (x : T) (x' : T') := x'. (* ********************* structures ****************************** *) -From elpi Require Import elpi. +From elpi Require Import elpi tc. + +From elpi.apps.tc.elpi Extra Dependency "tc_aux.elpi" as tc_aux. + +Elpi TC Solver Override TC.Solver None. Register unify as hb.unify. Register id_phant as hb.id. @@ -306,6 +310,7 @@ Elpi Export HB.locate. #[arguments(raw)] Elpi Command HB.about. Elpi Accumulate Db hb.db. +Elpi Accumulate Db tc.db. Elpi Accumulate File "HB/common/stdpp.elpi". Elpi Accumulate File "HB/common/utils.elpi". Elpi Accumulate File "HB/common/database.elpi". @@ -340,6 +345,7 @@ Elpi Export HB.about. #[arguments(raw)] Elpi Command HB.howto. Elpi Accumulate Db hb.db. +Elpi Accumulate Db tc.db. Elpi Accumulate File "HB/common/stdpp.elpi". Elpi Accumulate File "HB/common/database.elpi". Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi". @@ -382,6 +388,7 @@ Elpi Export HB.howto. #[arguments(raw)] Elpi Command HB.status. Elpi Accumulate Db hb.db. +Elpi Accumulate Db tc.db. Elpi Accumulate File "HB/common/stdpp.elpi". Elpi Accumulate File "HB/common/database.elpi". Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi". @@ -412,6 +419,7 @@ tred file.dot | xdot - #[arguments(raw)] Elpi Command HB.graph. Elpi Accumulate Db hb.db. +Elpi Accumulate Db tc.db. Elpi Accumulate File "HB/common/stdpp.elpi". Elpi Accumulate File "HB/common/database.elpi". Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi". @@ -460,7 +468,10 @@ HB.mixin Record MixinName T & Factory1 T & … & FactoryN T := { *) #[arguments(raw)] Elpi Command HB.mixin. +Elpi Accumulate Plugin "tc-builtin.elpi". Elpi Accumulate Db hb.db. +Elpi Accumulate Db tc.db. +Elpi Accumulate File tc_aux. Elpi Accumulate File "HB/common/stdpp.elpi". Elpi Accumulate File "HB/common/database.elpi". Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi". @@ -543,6 +554,7 @@ Elpi Export HB.mixin. Elpi Tactic HB.pack_for. Elpi Accumulate Db hb.db. +Elpi Accumulate Db tc.db. Elpi Accumulate File "HB/common/stdpp.elpi". Elpi Accumulate File "HB/common/database.elpi". Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi". @@ -566,6 +578,7 @@ Elpi Export HB.pack_for. Elpi Tactic HB.pack. Elpi Accumulate Db hb.db. +Elpi Accumulate Db tc.db. Elpi Accumulate File "HB/common/stdpp.elpi". Elpi Accumulate File "HB/common/database.elpi". Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi". @@ -641,7 +654,10 @@ HB.structure Definition StructureName params := *) #[arguments(raw)] Elpi Command HB.structure. +Elpi Accumulate Plugin "tc-builtin.elpi". Elpi Accumulate Db hb.db. +Elpi Accumulate Db tc.db. +Elpi Accumulate File tc_aux. Elpi Accumulate File "HB/common/stdpp.elpi". Elpi Accumulate File "HB/common/database.elpi". Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi". @@ -724,7 +740,10 @@ Elpi Export HB.structure. *) #[arguments(raw)] Elpi Command HB.saturate. +Elpi Accumulate Plugin "tc-builtin.elpi". Elpi Accumulate Db hb.db. +Elpi Accumulate Db tc.db. +Elpi Accumulate File tc_aux. Elpi Accumulate File "HB/common/stdpp.elpi". Elpi Accumulate File "HB/common/database.elpi". Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi". @@ -775,6 +794,7 @@ HB.instance Definition N Params := Factory.Build Params T … #[arguments(raw)] Elpi Command HB.instance. Elpi Accumulate Db hb.db. +Elpi Accumulate Db tc.db. Elpi Accumulate File "HB/common/stdpp.elpi". Elpi Accumulate File "HB/common/database.elpi". Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi". @@ -816,7 +836,10 @@ Elpi Export HB.instance. (** [HB.factory] declares a factory. It has the same syntax of [HB.mixin] *) #[arguments(raw)] Elpi Command HB.factory. +Elpi Accumulate Plugin "tc-builtin.elpi". Elpi Accumulate Db hb.db. +Elpi Accumulate Db tc.db. +Elpi Accumulate File tc_aux. Elpi Accumulate File "HB/common/stdpp.elpi". Elpi Accumulate File "HB/common/database.elpi". Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi". @@ -899,7 +922,10 @@ HB.end. *) #[arguments(raw)] Elpi Command HB.builders. +Elpi Accumulate Plugin "tc-builtin.elpi". Elpi Accumulate Db hb.db. +Elpi Accumulate Db tc.db. +Elpi Accumulate File tc_aux. Elpi Accumulate File "HB/common/stdpp.elpi". Elpi Accumulate File "HB/common/database.elpi". Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi". @@ -941,6 +967,7 @@ Elpi Export HB.builders. #[arguments(raw)] Elpi Command HB.end. Elpi Accumulate Db hb.db. +Elpi Accumulate Db tc.db. Elpi Accumulate File "HB/common/stdpp.elpi". Elpi Accumulate File "HB/common/database.elpi". Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi". @@ -1015,6 +1042,7 @@ Export Algebra.Exports. #[arguments(raw)] Elpi Command HB.export. Elpi Accumulate Db hb.db. +Elpi Accumulate Db tc.db. Elpi Accumulate File "HB/common/stdpp.elpi". Elpi Accumulate File "HB/common/database.elpi". Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi". @@ -1061,6 +1089,7 @@ Elpi Export HB.export. #[arguments(raw)] Elpi Command HB.reexport. Elpi Accumulate Db hb.db. +Elpi Accumulate Db tc.db. Elpi Accumulate File "HB/common/stdpp.elpi". Elpi Accumulate File "HB/common/database.elpi". Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi". @@ -1143,7 +1172,10 @@ HB.instance Definition _ : Ml ... T := ml. *) #[arguments(raw)] Elpi Command HB.declare. +Elpi Accumulate Plugin "tc-builtin.elpi". Elpi Accumulate Db hb.db. +Elpi Accumulate Db tc.db. +Elpi Accumulate File tc_aux. Elpi Accumulate File "HB/common/stdpp.elpi". Elpi Accumulate File "HB/common/database.elpi". Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi". @@ -1180,6 +1212,7 @@ Elpi Export HB.declare. #[arguments(raw)] Elpi Command HB.check. Elpi Accumulate Db hb.db. +Elpi Accumulate Db tc.db. Elpi Accumulate File "HB/common/stdpp.elpi". Elpi Accumulate File "HB/common/database.elpi". Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".