From a7c0732eb33d06634007f1e53d6e9a7f537a8fec Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 31 Mar 2021 12:17:23 +0200 Subject: [PATCH] do not crash if the key has no name --- HB/common/database.elpi | 10 +++++++--- HB/common/synthesis.elpi | 15 +++++++++------ HB/instance.elpi | 29 ++++++++++++++++++++--------- _CoqProject.test-suite | 1 + tests/alias_f_instance.v | 8 ++++++++ 5 files changed, 45 insertions(+), 18 deletions(-) create mode 100644 tests/alias_f_instance.v diff --git a/HB/common/database.elpi b/HB/common/database.elpi index 2ab7bceb7..65be0cfb6 100644 --- a/HB/common/database.elpi +++ b/HB/common/database.elpi @@ -256,12 +256,16 @@ get-cs-structure (cs-instance _ _ (global Inst)) Struct :- std.do! [ coq.prod-tgt->gref InstTy Struct ]. -pred has-cs-instance i:gref, i:cs-instance. -has-cs-instance GTy (cs-instance _ (cs-gref GTy) _). +pred has-cs-instance i:term, i:cs-instance. +has-cs-instance (global GR) (cs-instance _ (cs-gref GR) _) :- !. +has-cs-instance (app[global GR|_]) (cs-instance _ (cs-gref GR) _) :- !. +has-cs-instance (prod _ _ _) (cs-instance _ cs-prod _) :- !. +has-cs-instance (sort U) (cs-instance _ (cs-sort U) _) :- !. +has-cs-instance _ (cs-instance _ cs-default _) :- !. pred get-local-structures i:term, o:list structure. get-local-structures TyTrm StructL :- std.do! [ - std.filter {coq.CS.db} (has-cs-instance {term->gref TyTrm}) DBGTyL, + std.filter {coq.CS.db} (has-cs-instance TyTrm) DBGTyL, std.map DBGTyL get-cs-structure RecL, std.filter RecL is-structure StructL ]. diff --git a/HB/common/synthesis.elpi b/HB/common/synthesis.elpi index 02b7ac58d..70e01fc9d 100644 --- a/HB/common/synthesis.elpi +++ b/HB/common/synthesis.elpi @@ -46,29 +46,32 @@ assert!-infer-mixin T M B :- % Given TheType it looks all canonical structure instances on it and makes % all their mixins available for inference pred under-local-canonical-mixins-of.do! i:term, i:list prop. -under-local-canonical-mixins-of.do! T P :- +under-local-canonical-mixins-of.do! T P :- std.do! [ get-local-structures T CS, std.map CS (private.structure-instance->mixin-srcs T) MSLL, std.flatten MSLL MSL, - MSL => std.do! P. + MSL => std.do! P, +]. % Given TheType and a factory instance (on it), makes all the mixins provided by % the factory available for inference. pred under-mixin-src-from-factory.do! i:term, i:term, i:list prop. -under-mixin-src-from-factory.do! TheType TheFactory LP :- +under-mixin-src-from-factory.do! TheType TheFactory LP :- std.do! [ private.factory-instance->new-mixins [] TheFactory ML, std.map ML (m\c\ c = mixin-src TheType m TheFactory) MLClauses, - MLClauses => std.do! LP. + MLClauses => std.do! LP, +]. % Given TheType and a factory instance (on it), builds all the *new* mixins % provided by the factory available for and passes them to the given % continuation pred under-new-mixin-src-from-factory.do! i:term, i:term, i:(list mixinname -> prop). -under-new-mixin-src-from-factory.do! TheType TheFactory LP :- +under-new-mixin-src-from-factory.do! TheType TheFactory LP :- std.do! [ findall-mixin-src TheType OldMixins, private.factory-instance->new-mixins OldMixins TheFactory NewML, std.map NewML (m\c\ c = mixin-src TheType m TheFactory) NewMLClauses, - NewMLClauses => std.do! [ LP NewML ]. + NewMLClauses => std.do! [ LP NewML ], +]. % [under-mixins.then MLwP Pred F] states that F has shape % fun p_1 .. p_k T, diff --git a/HB/instance.elpi b/HB/instance.elpi index d50f888c3..734db62c8 100644 --- a/HB/instance.elpi +++ b/HB/instance.elpi @@ -85,13 +85,7 @@ declare-all T [class Class Struct MLwP|Rest] [pr Name CS|L] :- fail, !, - coq.term->gref T TGR, - coq.gref->path TGR TPath, - std.rev TPath [TMod|_], - coq.gref->id TGR TID, - if (TMod = TID) - (Name is TID ^ "_canonical_" ^ {gref->modname Struct}) - (Name is TMod ^ "_" ^ TID ^ "_canonical_" ^ {gref->modname Struct}), + private.craft-instance-name T Struct Name, if-verbose (coq.say "HB: declare canonical structure instance" Name), @@ -122,10 +116,26 @@ declare-instance T F Clauses :- (std.map CS (x\r\ sigma i c\ x = pr i c, r = instance-to-export i c) Clauses) (Clauses = []). +pred craft-instance-name i:term, i:structure, o:id. +craft-instance-name (global TGR) Struct Name :- craft-instance-name.of-gref TGR Struct Name. +craft-instance-name (app[global TGR|_]) Struct Name :- craft-instance-name.of-gref TGR Struct Name. +craft-instance-name (fun _ _ _) Struct Name :- + Name is "Fun" ^ {std.any->string {new_int}} ^ "_canonical_" ^ {gref->modname Struct}. + +pred craft-instance-name.of-gref i:gref, i:structure, o:id. +craft-instance-name.of-gref TGR Struct Name :- + coq.gref->path TGR TPath, + std.rev TPath [TMod|_], + coq.gref->id TGR TID, + if (TMod = TID) + (Name is TID ^ "_canonical_" ^ {gref->modname Struct}) + (Name is TMod ^ "_" ^ TID ^ "_canonical_" ^ {gref->modname Struct}). + + % [add-mixin T F _ M Cl] adds a constant begin the mixin instance for M on type % T built from factory F pred add-mixin i:term, i:factoryname, i:bool, i:mixinname, o:list prop. -add-mixin T FGR MakeCanon MissinMixin [MixinSrcCl, BuiderDeclCl] :- +add-mixin T FGR MakeCanon MissinMixin [MixinSrcCl, BuiderDeclCl] :- std.do! [ synthesis.assert!-infer-mixin T MissinMixin Bo, MixinSrcCl = mixin-src T MixinName (global (const C)), BuiderDeclCl = builder-decl (builder N FGR MixinName (const C)), @@ -146,7 +156,8 @@ add-mixin T FGR MakeCanon MissinMixin [MixinSrcCl, BuiderDeclCl] :- if (MakeCanon = tt, whd (global (const C)) [] (global (indc _)) _) (if-verbose (coq.say "HB: declare canonical mixin instance" C), with-locality (log.coq.CS.declare-instance C)) - true. + true, +]. pred add-all-mixins i:term, i:factoryname, i:list mixinname, i:bool, o:list prop. add-all-mixins T FGR ML MakeCanon Clauses :- std.do! [ diff --git a/_CoqProject.test-suite b/_CoqProject.test-suite index 902d60200..ed35aa675 100644 --- a/_CoqProject.test-suite +++ b/_CoqProject.test-suite @@ -56,6 +56,7 @@ tests/log_impargs_record.v tests/compress_coe.v tests/funclass.v tests/local_instance.v +tests/alias_f_instance.v -R tests HB.tests -R examples HB.examples diff --git a/tests/alias_f_instance.v b/tests/alias_f_instance.v new file mode 100644 index 000000000..8d6b59ffc --- /dev/null +++ b/tests/alias_f_instance.v @@ -0,0 +1,8 @@ +From HB Require Import structures. + +HB.mixin Record IsPred (R : Type) (S : R -> bool) := {}. +HB.structure Definition Pred R := {S of IsPred R S}. + +Definition bool_pred := IsPred.Build bool (fun x => true). + +HB.instance Definition _ := bool_pred.