From 2d7d478b1621bcb0dedd4efb123990907fc112ce Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 7 Feb 2023 13:02:19 +0100 Subject: [PATCH 01/37] test showing the problem --- tests/instance_before_structure.v | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) create mode 100644 tests/instance_before_structure.v diff --git a/tests/instance_before_structure.v b/tests/instance_before_structure.v new file mode 100644 index 000000000..661ed615b --- /dev/null +++ b/tests/instance_before_structure.v @@ -0,0 +1,28 @@ +From HB Require Import structures. + +HB.mixin Record m1 T := { default1 : T }. + +HB.mixin Record m2 T := { default2 : T }. + +HB.structure Definition s1 := { T of m1 T }. + +HB.instance Definition _ : m1 nat := m1.Build nat 1. + +HB.about nat. + +(* too early *) +HB.instance Definition _ : m2 nat := m2.Build nat 2. + +HB.about nat. (* only s1 on nat *) + +HB.structure Definition s2 := { T of m1 T & m2 T }. + +(* here it works *) +(* HB.instance Definition _ : m2 nat := m2.Build nat 2. *) + +HB.about nat. (* should be both s1 and s2 on nat *) + +Check @default1 nat. +Check @default2 nat. + + From 1e511637367ec368abaddd3eb903ce778044a28d Mon Sep 17 00:00:00 2001 From: thomas Date: Tue, 14 Feb 2023 16:04:28 +0100 Subject: [PATCH 02/37] first try on modifying HB --- HB/instance.elpi | 2 ++ _CoqProject.test-suite | 1 + instance.ipynb | 33 +++++++++++++++++++++++++++++++ structures.v | 16 +++++++++++++-- tests/instance_before_structure.v | 5 +++-- 5 files changed, 53 insertions(+), 4 deletions(-) create mode 100644 instance.ipynb diff --git a/HB/instance.elpi b/HB/instance.elpi index 0b793248c..2f2303566 100644 --- a/HB/instance.elpi +++ b/HB/instance.elpi @@ -76,6 +76,8 @@ declare-const Name BodySkel TyWPSkel CSL :- std.do! [ % we accumulate clauses now that the section is over acc-clauses current Clauses + if (!has-CS-instance TheType) + acc-clause current has-CS-instance TheType ]. % [declare-all T CL MCSTL] given a type T and a list of class definition diff --git a/_CoqProject.test-suite b/_CoqProject.test-suite index 98c20167e..0814acb8f 100644 --- a/_CoqProject.test-suite +++ b/_CoqProject.test-suite @@ -72,6 +72,7 @@ tests/not_same_key.v tests/hb_pack.v tests/declare.v tests/short.v +tests/instance_before_structure.v tests/primitive_records.v tests/non_forgetful_inheritance.v tests/fix_loop.v diff --git a/instance.ipynb b/instance.ipynb new file mode 100644 index 000000000..82aab6285 --- /dev/null +++ b/instance.ipynb @@ -0,0 +1,33 @@ +{ + "cells": [ + { + "attachments": {}, + "cell_type": "markdown", + "metadata": {}, + "source": [ + " Saturating instances on new structure declaration \n", + "\n", + "When a new structure S_new is created, the instances of factories that the new structure implements are not recorded in the database, instead they are in the coq databse. We want to get the list of factories attached to S_new and create properly the instances that implements those factories with the new structure.\n", + "\n", + "See the test file tests/instance_before_structure.v for an example\n", + "\n" + ] + }, + { + "attachments": {}, + "cell_type": "markdown", + "metadata": {}, + "source": [ + "functions get-canonical-instances and get canonical-structures let us interact with the coq database " + ] + } + ], + "metadata": { + "language_info": { + "name": "python" + }, + "orig_nbformat": 4 + }, + "nbformat": 4, + "nbformat_minor": 2 +} diff --git a/structures.v b/structures.v index 30c9015f4..04f010be8 100644 --- a/structures.v +++ b/structures.v @@ -192,6 +192,10 @@ pred mixin-class o:mixinname, o:classname. % Coq's CS database (which is just for structures). pred mixin-src o:term, o:mixinname, o:term. + +% states that a certain type has a canonical instance +pred has-CS-instance o:term. + %% database for HB.builders %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % [builder N TheFactory TheMixin S] is used to @@ -611,9 +615,17 @@ Elpi Accumulate Db hb.db. Elpi Accumulate lp:{{ main [const-decl N (some B) Arity] :- !, std.do! [ + % compute the universe for the structure (default ) prod-last {coq.arity->term Arity} Ty, - if (ground_term Ty) (Sort = Ty) (Sort = {{Type}}), sort Univ = Sort, - with-attributes (with-logging (structure.declare N B Univ)) + if (ground_term Ty) (Sort = Ty) (Sort = {{Type}}), sort Univ = Sort, + with-attributes (with-logging (structure.declare N B Univ)), + %with-attributes (with-logging (instance.declare-const N B )) + % coq.CS.db-for (coq-builtin) + % database.get-canonical-structures Ty + % database.get-canonical-instances Ty + % synthesis.under-local-canonical-mixins-of do! + % instance.declare-canonical-instances-from-factory +%get-canonical-structures Ty _ ]. main _ :- coq.error "Usage: HB.structure Definition := { A of A & … & A }". diff --git a/tests/instance_before_structure.v b/tests/instance_before_structure.v index 661ed615b..596dcbffe 100644 --- a/tests/instance_before_structure.v +++ b/tests/instance_before_structure.v @@ -3,8 +3,8 @@ From HB Require Import structures. HB.mixin Record m1 T := { default1 : T }. HB.mixin Record m2 T := { default2 : T }. - -HB.structure Definition s1 := { T of m1 T }. +#[verbose] +HB.structure Definition s1 := { T of m1 T }. HB.instance Definition _ : m1 nat := m1.Build nat 1. @@ -15,6 +15,7 @@ HB.instance Definition _ : m2 nat := m2.Build nat 2. HB.about nat. (* only s1 on nat *) + HB.structure Definition s2 := { T of m1 T & m2 T }. (* here it works *) From bd2a356ff56f699c0da1cec21defa2bccce892c1 Mon Sep 17 00:00:00 2001 From: thomas Date: Wed, 15 Feb 2023 11:17:06 +0100 Subject: [PATCH 03/37] fixing bug on issue #335 should work but no tests yet --- HB/instance.elpi | 8 ++++++-- _CoqProject.test-suite | 2 +- structures.v | 8 +------- tests/store_types_cs.v | 6 ++++++ 4 files changed, 14 insertions(+), 10 deletions(-) create mode 100644 tests/store_types_cs.v diff --git a/HB/instance.elpi b/HB/instance.elpi index 2f2303566..dacc0bb27 100644 --- a/HB/instance.elpi +++ b/HB/instance.elpi @@ -74,10 +74,14 @@ declare-const Name BodySkel TyWPSkel CSL :- std.do! [ log.coq.env.end-section-name SectionName ), + % if a clause describing this instance isn't in the database yet we add it + + if (has-CS-instance TheType) true (acc-clause current (has-CS-instance TheType)) , + % we accumulate clauses now that the section is over acc-clauses current Clauses - if (!has-CS-instance TheType) - acc-clause current has-CS-instance TheType + + ]. % [declare-all T CL MCSTL] given a type T and a list of class definition diff --git a/_CoqProject.test-suite b/_CoqProject.test-suite index 0814acb8f..1f551d438 100644 --- a/_CoqProject.test-suite +++ b/_CoqProject.test-suite @@ -81,7 +81,7 @@ tests/hnf.v tests/fun_instance.v tests/issue284.v tests/issue287.v - +tests/store_types_cs.v -R tests HB.tests -R examples HB.examples diff --git a/structures.v b/structures.v index 04f010be8..dac8f0be3 100644 --- a/structures.v +++ b/structures.v @@ -619,13 +619,7 @@ main [const-decl N (some B) Arity] :- !, std.do! [ prod-last {coq.arity->term Arity} Ty, if (ground_term Ty) (Sort = Ty) (Sort = {{Type}}), sort Univ = Sort, with-attributes (with-logging (structure.declare N B Univ)), - %with-attributes (with-logging (instance.declare-const N B )) - % coq.CS.db-for (coq-builtin) - % database.get-canonical-structures Ty - % database.get-canonical-instances Ty - % synthesis.under-local-canonical-mixins-of do! - % instance.declare-canonical-instances-from-factory -%get-canonical-structures Ty _ + ]. main _ :- coq.error "Usage: HB.structure Definition := { A of A & … & A }". diff --git a/tests/store_types_cs.v b/tests/store_types_cs.v new file mode 100644 index 000000000..35d80c486 --- /dev/null +++ b/tests/store_types_cs.v @@ -0,0 +1,6 @@ +From HB Require Import structures. +From elpi Require Import elpi. +HB.mixin Record m1 T := { default1 : T }. + +HB.instance Definition _ : m1 nat := m1.Build nat 1. +(*TODO inspect if a clause has_cs_instance was added in the elpi database *) From 90559fc46194833ef232b3bc0baa53c6fb3ad675 Mon Sep 17 00:00:00 2001 From: thomas Date: Wed, 15 Feb 2023 14:48:37 +0100 Subject: [PATCH 04/37] changing conflicting predicate name and completing the test for that issue #335 --- HB/instance.elpi | 4 ++-- _CoqProject | 1 + _CoqProject.test-suite | 1 + structures.v | 2 +- tests/store_types_cs.v | 7 +++++-- 5 files changed, 10 insertions(+), 5 deletions(-) diff --git a/HB/instance.elpi b/HB/instance.elpi index dacc0bb27..c55042814 100644 --- a/HB/instance.elpi +++ b/HB/instance.elpi @@ -74,9 +74,9 @@ declare-const Name BodySkel TyWPSkel CSL :- std.do! [ log.coq.env.end-section-name SectionName ), - % if a clause describing this instance isn't in the database yet we add it + % if a clause associated to this type isn't in the database yet we add it - if (has-CS-instance TheType) true (acc-clause current (has-CS-instance TheType)) , + if (has-db-instance TheType) true (acc-clause current (has-db-instance TheType)) , % we accumulate clauses now that the section is over acc-clauses current Clauses diff --git a/_CoqProject b/_CoqProject index b8cf8cf7e..86d5a53f2 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1,3 +1,4 @@ structures.v -arg -w -arg -elpi.accumulate-syntax +-arg -w -arg +elpi.typecheck -Q . HB \ No newline at end of file diff --git a/_CoqProject.test-suite b/_CoqProject.test-suite index 1f551d438..84f137f1b 100644 --- a/_CoqProject.test-suite +++ b/_CoqProject.test-suite @@ -3,6 +3,7 @@ -arg -w -arg -abstract-large-number -arg -w -arg -disj-pattern-notation -arg -w -arg -notation-overridden +arg -w -arg +elpi.typecheck examples/readme.v examples/hulk.v diff --git a/structures.v b/structures.v index dac8f0be3..6aa444aa8 100644 --- a/structures.v +++ b/structures.v @@ -194,7 +194,7 @@ pred mixin-src o:term, o:mixinname, o:term. % states that a certain type has a canonical instance -pred has-CS-instance o:term. +pred has-db-instance o:term. %% database for HB.builders %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% diff --git a/tests/store_types_cs.v b/tests/store_types_cs.v index 35d80c486..d1bb37723 100644 --- a/tests/store_types_cs.v +++ b/tests/store_types_cs.v @@ -1,6 +1,9 @@ From HB Require Import structures. From elpi Require Import elpi. HB.mixin Record m1 T := { default1 : T }. - HB.instance Definition _ : m1 nat := m1.Build nat 1. -(*TODO inspect if a clause has_cs_instance was added in the elpi database *) + +Elpi Query HB.instance lp:{{ + std.assert! (has-db-instance X) "no clause", + std.assert! (X = {{nat}}) "wrong type". +}}. \ No newline at end of file From 1dfc12c59fb9996d0ab63d1baba8cfd3134d452d Mon Sep 17 00:00:00 2001 From: thomas Date: Wed, 15 Feb 2023 15:24:39 +0100 Subject: [PATCH 05/37] completing the test --- tests/store_types_cs.v | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/tests/store_types_cs.v b/tests/store_types_cs.v index d1bb37723..20ba19e3c 100644 --- a/tests/store_types_cs.v +++ b/tests/store_types_cs.v @@ -1,6 +1,10 @@ From HB Require Import structures. From elpi Require Import elpi. HB.mixin Record m1 T := { default1 : T }. + +(* no clauses yet*) +Elpi Query HB.instance lp:{{std.assert! (not (has-db-instance X)) "already has an instance clause"}}. + HB.instance Definition _ : m1 nat := m1.Build nat 1. Elpi Query HB.instance lp:{{ From c7f0e3eb9bb4afaa80eb4886cca173e9fda0a254 Mon Sep 17 00:00:00 2001 From: thomas Date: Wed, 15 Feb 2023 17:33:26 +0100 Subject: [PATCH 06/37] starting to write the function for #336 --- HB/common/database.elpi | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/HB/common/database.elpi b/HB/common/database.elpi index 6ae022a1c..faaa28017 100644 --- a/HB/common/database.elpi +++ b/HB/common/database.elpi @@ -32,6 +32,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 +136,13 @@ factories-provide FLwP MLwP :- std.do! [ w-params.map UnsortedMLwP (p\t\ toposort-mixins) MLwP, ]. +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 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! [ @@ -268,6 +278,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 From a832dbf33f3ffd13dc973048b7bb8b4c3453f5d3 Mon Sep 17 00:00:00 2001 From: thomas Date: Thu, 16 Feb 2023 10:41:59 +0100 Subject: [PATCH 07/37] taking out duplicates for the function in #336 and including a test for it --- HB/common/database.elpi | 10 +++++++++- _CoqProject.test-suite | 2 ++ tests/findall_cs_type.v | 22 ++++++++++++++++++++++ 3 files changed, 33 insertions(+), 1 deletion(-) create mode 100644 tests/findall_cs_type.v diff --git a/HB/common/database.elpi b/HB/common/database.elpi index faaa28017..67ec932f7 100644 --- a/HB/common/database.elpi +++ b/HB/common/database.elpi @@ -136,10 +136,18 @@ factories-provide FLwP MLwP :- std.do! [ w-params.map UnsortedMLwP (p\t\ toposort-mixins) MLwP, ]. + +pred undup-terms i:term, i:list term, o:list term. + undup-terms _ [] []. + undup-terms T[T1|TN] TN :- T == T1. + undup-terms T [T1|TN] [T1|TL] :- undup-terms T TN TL. + +% finds all 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 TypeList, + std.map Clauses has-db-instance_type TypeListDup, + undup-terms _ TypeListDup TypeList, ]. diff --git a/_CoqProject.test-suite b/_CoqProject.test-suite index 84f137f1b..268088bf8 100644 --- a/_CoqProject.test-suite +++ b/_CoqProject.test-suite @@ -83,6 +83,8 @@ tests/fun_instance.v tests/issue284.v tests/issue287.v tests/store_types_cs.v +tests/findall_cs_types.v + -R tests HB.tests -R examples HB.examples diff --git a/tests/findall_cs_type.v b/tests/findall_cs_type.v new file mode 100644 index 000000000..8af63c4ae --- /dev/null +++ b/tests/findall_cs_type.v @@ -0,0 +1,22 @@ +From HB Require Import structures. +From elpi Require Import elpi. +HB.mixin Record m1 T := { default1 : T }. +HB.mixin Record m2 T := { default1 : T }. + +(* no types yet*) +Elpi Query HB.instance lp:{{std.assert! (findall-cs-types []) "a type was found"}}. + +HB.instance Definition _ : m1 nat := m1.Build nat 1. +HB.instance Definition _ : m2 nat := m2.Build nat 2. +(*no duplicates *) +Elpi Query HB.instance lp:{{ + std.assert! (findall-cs-types [X]) "no type", + std.assert! (X = {{nat}}) "wrong type". +}}. + +HB.instance Definition _ : m1 bool := m1.Build bool true. + +Elpi Query HB.instance lp:{{ + std.assert! (findall-cs-types [X,Y]) "no type", + std.assert! (Y = {{bool}}) "wrong type". +}}. \ No newline at end of file From 62378c1ed14a3a0c404b52611e9672134ff820cc Mon Sep 17 00:00:00 2001 From: thomas Date: Thu, 16 Feb 2023 11:47:24 +0100 Subject: [PATCH 08/37] starting to write function in #337 --- structures.v | 33 +++++++++++++++++++++++++++++++++ 1 file changed, 33 insertions(+) diff --git a/structures.v b/structures.v index 6aa444aa8..fd65d0709 100644 --- a/structures.v +++ b/structures.v @@ -682,6 +682,39 @@ Elpi Export HB.instance. (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) +(** [HB.saturate_instances] saturates all instances possible for a given structure *) + + +#[arguments(raw)] Elpi Command HB.saturate_instances. +#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi". +#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi". +Elpi Accumulate File "HB/common/stdpp.elpi". +Elpi Accumulate File "HB/common/database.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/common/structure.elpi". +Elpi Accumulate File "HB/context.elpi". +Elpi Accumulate File "HB/instance.elpi". +Elpi Accumulate Db hb.db. +Elpi Accumulate lp:{{ + +main [const-decl StructureName] :- !, std.do! [ +database.findall-cs-types InsTypes, +%TODO get the types StrucTypes the structure with name StructureName with which it can be instatiated +% saturate instances with the types in the intersection between InsTypes and StrucTypes +]. + +main _ :- coq.error "Usage: HB.saturate_instances StructureName". + +}}. +Elpi Typecheck. +Elpi Export HB.saturate_instances. + +(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) +(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) +(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) + (** [HB.factory] declares a factory. It has the same syntax of [HB.mixin] *) #[arguments(raw)] Elpi Command HB.factory. From 45153aa8d96cd51e007e0b030268f26475c2ec43 Mon Sep 17 00:00:00 2001 From: thomas Date: Fri, 17 Feb 2023 16:24:13 +0100 Subject: [PATCH 09/37] #335 --- HB/common/database.elpi | 2 +- HB/instance.elpi | 6 +++--- structures.v | 6 ++++-- 3 files changed, 8 insertions(+), 6 deletions(-) diff --git a/HB/common/database.elpi b/HB/common/database.elpi index 67ec932f7..e3fe1444a 100644 --- a/HB/common/database.elpi +++ b/HB/common/database.elpi @@ -142,7 +142,7 @@ pred undup-terms i:term, i:list term, o:list term. undup-terms T[T1|TN] TN :- T == T1. undup-terms T [T1|TN] [T1|TL] :- undup-terms T TN TL. -% finds all types for which an instance was created +% 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, diff --git a/HB/instance.elpi b/HB/instance.elpi index c55042814..15067e012 100644 --- a/HB/instance.elpi +++ b/HB/instance.elpi @@ -298,7 +298,7 @@ declare-canonical-instances-from-factory-and-local-builders % it uses all known builders to declare canonical instances of structures % on T pred declare-canonical-instances-from-factory - i:factoryname, i:term, i:term, o:list (pair id constant). + i:factoryname, i:term, i:term, o: list prop, o:list (pair id constant). declare-canonical-instances-from-factory Factory T F CSL :- std.do! [ % The order of the following two "under...do!" is crucial, % priority must be given to canonical mixins @@ -307,8 +307,8 @@ declare-canonical-instances-from-factory Factory T F CSL :- std.do! [ synthesis.under-mixin-src-from-factory.do! T F [ synthesis.under-local-canonical-mixins-of.do! T [ list-w-params_list {factory-provides Factory} ML, - add-all-mixins T Factory ML tt _ MCSL, - instance.declare-all T {findall-classes-for ML} CCSL, + add-all-mixins T Factory ML tt Clauses MCSL, + Clauses =>instance.declare-all T {findall-classes-for ML} CCSL, ] ], std.append MCSL CCSL CSL diff --git a/structures.v b/structures.v index fd65d0709..a91429f1a 100644 --- a/structures.v +++ b/structures.v @@ -693,7 +693,7 @@ Elpi Accumulate File "HB/common/database.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/common/structure.elpi". +Elpi Accumulate File "HB/structure.elpi". Elpi Accumulate File "HB/context.elpi". Elpi Accumulate File "HB/instance.elpi". Elpi Accumulate Db hb.db. @@ -701,6 +701,8 @@ Elpi Accumulate lp:{{ main [const-decl StructureName] :- !, std.do! [ database.findall-cs-types InsTypes, +findall-classes Classes. +mixin-src T _ _ %TODO get the types StrucTypes the structure with name StructureName with which it can be instatiated % saturate instances with the types in the intersection between InsTypes and StrucTypes ]. @@ -708,7 +710,7 @@ database.findall-cs-types InsTypes, main _ :- coq.error "Usage: HB.saturate_instances StructureName". }}. -Elpi Typecheck. +(* Elpi Typecheck.*) Elpi Export HB.saturate_instances. (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) From 77cc4381a4160f3a9a01a0ffa0b2f15b257e96ed Mon Sep 17 00:00:00 2001 From: thomas Date: Mon, 20 Feb 2023 17:37:26 +0100 Subject: [PATCH 10/37] #335 --- HB/common/database.elpi | 7 ++++ HB/instance.elpi | 4 +-- structures.v | 74 ++++++++++++++++++++++------------------- 3 files changed, 48 insertions(+), 37 deletions(-) diff --git a/HB/common/database.elpi b/HB/common/database.elpi index e3fe1444a..58d84fecb 100644 --- a/HB/common/database.elpi +++ b/HB/common/database.elpi @@ -14,6 +14,9 @@ from_mixin (from _ X _) X. pred from_builder i:prop, o:term. from_builder (from _ _ X) (global X). +pred mixin-src_type i:prop, o:term. +mixin-src_type (mixin-src T _ _ ) T. + pred mixin-src_mixin i:prop, o:mixinname. mixin-src_mixin (mixin-src _ M _) M. @@ -210,6 +213,10 @@ findall-builders LFIL :- std.map {std.findall (builder-decl B_)} extract-builder LFILunsorted, std.bubblesort LFILunsorted leq-builder LFIL. +pred findall-type-src i:term, o:list term. +findall-type-src S TL :- + std.map {std.findall (mixin-src T_ M_ S)} mixin-src_type 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. diff --git a/HB/instance.elpi b/HB/instance.elpi index 15067e012..c23dee13e 100644 --- a/HB/instance.elpi +++ b/HB/instance.elpi @@ -214,7 +214,7 @@ declare-instance Factory T F Clauses CSL :- declare-canonical-instances-from-factory-and-local-builders Factory T F TheFactory FGR Clauses CSL. declare-instance Factory T F Clauses CSL :- - declare-canonical-instances-from-factory Factory T F CSL, + declare-canonical-instances-from-factory Factory T F Clauses CSL, if (get-option "export" tt) (coq.env.current-library File, std.map CSL (x\r\ sigma i c\ x = pr i c, r = instance-to-export File i c) Clauses) @@ -299,7 +299,7 @@ declare-canonical-instances-from-factory-and-local-builders % on T pred declare-canonical-instances-from-factory i:factoryname, i:term, i:term, o: list prop, o:list (pair id constant). -declare-canonical-instances-from-factory Factory T F CSL :- std.do! [ +declare-canonical-instances-from-factory Factory T F Clauses CSL :- std.do! [ % The order of the following two "under...do!" is crucial, % priority must be given to canonical mixins % as they are the ones which guarantee forgetful inheritance diff --git a/structures.v b/structures.v index a91429f1a..29c3856ce 100644 --- a/structures.v +++ b/structures.v @@ -534,6 +534,44 @@ solve (goal _ _ Ty _ Args as G) GLS :- with-attributes (with-logging (std.do! [ }}. Elpi Typecheck. Elpi Export HB.pack. +(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) +(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) +(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) + +(** [HB.saturate_instances] saturates all instances possible for a given structure *) + + +#[arguments(raw)] Elpi Command HB.saturate_instances. +#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi". +#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi". +Elpi Accumulate File "HB/common/stdpp.elpi". +Elpi Accumulate File "HB/common/database.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/structure.elpi". +Elpi Accumulate File "HB/context.elpi". +Elpi Accumulate File "HB/instance.elpi". +Elpi Accumulate Db hb.db. +Elpi Accumulate lp:{{ + +main [id Struct] :- !, std.do! [ +topo-find Struct S, +database.findall-cs-types InsTypes, +findall-mixin-src-type S TL, +findall-classes Classes, +std.forall TL (t\ (instance.declare-all t Classes CLS)), + +%TODO get the types StrucTypes the structure with name StructureName with which it can be instatiated +% saturate instances with the types in the intersection between InsTypes and StrucTypes +]. + +main _ :- coq.error "Usage: HB.saturate_instances StructureName". + +}}. +Elpi Typecheck. +Elpi Export HB.saturate_instances. + (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) @@ -619,7 +657,7 @@ main [const-decl N (some B) Arity] :- !, std.do! [ prod-last {coq.arity->term Arity} Ty, if (ground_term Ty) (Sort = Ty) (Sort = {{Type}}), sort Univ = Sort, with-attributes (with-logging (structure.declare N B Univ)), - + saturate_instances N, ]. main _ :- coq.error "Usage: HB.structure Definition := { A of A & … & A }". @@ -678,40 +716,6 @@ main _ :- coq.error "Usage: HB.instance Definition := T ...". Elpi Typecheck. Elpi Export HB.instance. -(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) -(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) -(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) - -(** [HB.saturate_instances] saturates all instances possible for a given structure *) - - -#[arguments(raw)] Elpi Command HB.saturate_instances. -#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi". -#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi". -Elpi Accumulate File "HB/common/stdpp.elpi". -Elpi Accumulate File "HB/common/database.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/structure.elpi". -Elpi Accumulate File "HB/context.elpi". -Elpi Accumulate File "HB/instance.elpi". -Elpi Accumulate Db hb.db. -Elpi Accumulate lp:{{ - -main [const-decl StructureName] :- !, std.do! [ -database.findall-cs-types InsTypes, -findall-classes Classes. -mixin-src T _ _ -%TODO get the types StrucTypes the structure with name StructureName with which it can be instatiated -% saturate instances with the types in the intersection between InsTypes and StrucTypes -]. - -main _ :- coq.error "Usage: HB.saturate_instances StructureName". - -}}. -(* Elpi Typecheck.*) -Elpi Export HB.saturate_instances. (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) From 3a6341bb282b73716aa34c65d35365dcd21b7ba1 Mon Sep 17 00:00:00 2001 From: thomas Date: Wed, 22 Feb 2023 15:59:34 +0100 Subject: [PATCH 11/37] implements the new approach mentioned in #335 and adds the steps in #336 and #337, also updated the test for #338, it seems that the saturation doesn't work when called inside the structure command : the current structure isn't taken into account when saturating --- HB/common/database.elpi | 6 +-- HB/instance.elpi | 15 +++++-- structures.v | 68 ++++++++++++++----------------- tests/instance_before_structure.v | 16 ++++++-- 4 files changed, 57 insertions(+), 48 deletions(-) diff --git a/HB/common/database.elpi b/HB/common/database.elpi index 58d84fecb..b992ba852 100644 --- a/HB/common/database.elpi +++ b/HB/common/database.elpi @@ -213,9 +213,9 @@ findall-builders LFIL :- std.map {std.findall (builder-decl B_)} extract-builder LFILunsorted, std.bubblesort LFILunsorted leq-builder LFIL. -pred findall-type-src i:term, o:list term. -findall-type-src S TL :- - std.map {std.findall (mixin-src T_ M_ S)} mixin-src_type TL. +pred findall-type-src o:list term. +findall-type-src TL :- + std.map {std.findall (mixin-src T_ M_ S_)} mixin-src_type TL. pred findall-mixin-src i:term, o:list mixinname. findall-mixin-src T ML :- diff --git a/HB/instance.elpi b/HB/instance.elpi index c23dee13e..1dc1b3e8e 100644 --- a/HB/instance.elpi +++ b/HB/instance.elpi @@ -195,6 +195,14 @@ mk-factory-sort-factory AliasGR CSL :- std.do! [ declare-const "_" GCF (arity FGCF) CSL ]. +% create instances for all possible combinations of (simple) types and structure compatible +pred saturate-instances. +saturate-instances :- std.do! [ + findall-type-src TL, + findall-classes Classes, + std.forall TL (t\ (declare-all t Classes _)), +]. + /* ------------------------------------------------------------------------- */ /* ----------------------------- private code ------------------------------ */ /* ------------------------------------------------------------------------- */ @@ -214,11 +222,12 @@ declare-instance Factory T F Clauses CSL :- declare-canonical-instances-from-factory-and-local-builders Factory T F TheFactory FGR Clauses CSL. declare-instance Factory T F Clauses CSL :- - declare-canonical-instances-from-factory Factory T F Clauses CSL, + declare-canonical-instances-from-factory Factory T F Clauses1 CSL, if (get-option "export" tt) (coq.env.current-library File, - std.map CSL (x\r\ sigma i c\ x = pr i c, r = instance-to-export File i c) Clauses) - (Clauses = []). + std.map CSL (x\r\ sigma i c\ x = pr i c, r = instance-to-export File i c) Clauses2) + (Clauses2 = []), + std.append Clauses1 Clauses2 Clauses. % [add-mixin T F _ M Cl] adds a constant being the mixin instance for M on type % T built from factory F diff --git a/structures.v b/structures.v index 29c3856ce..6d2a68357 100644 --- a/structures.v +++ b/structures.v @@ -534,43 +534,6 @@ solve (goal _ _ Ty _ Args as G) GLS :- with-attributes (with-logging (std.do! [ }}. Elpi Typecheck. Elpi Export HB.pack. -(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) -(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) -(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) - -(** [HB.saturate_instances] saturates all instances possible for a given structure *) - - -#[arguments(raw)] Elpi Command HB.saturate_instances. -#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi". -#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi". -Elpi Accumulate File "HB/common/stdpp.elpi". -Elpi Accumulate File "HB/common/database.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/structure.elpi". -Elpi Accumulate File "HB/context.elpi". -Elpi Accumulate File "HB/instance.elpi". -Elpi Accumulate Db hb.db. -Elpi Accumulate lp:{{ - -main [id Struct] :- !, std.do! [ -topo-find Struct S, -database.findall-cs-types InsTypes, -findall-mixin-src-type S TL, -findall-classes Classes, -std.forall TL (t\ (instance.declare-all t Classes CLS)), - -%TODO get the types StrucTypes the structure with name StructureName with which it can be instatiated -% saturate instances with the types in the intersection between InsTypes and StrucTypes -]. - -main _ :- coq.error "Usage: HB.saturate_instances StructureName". - -}}. -Elpi Typecheck. -Elpi Export HB.saturate_instances. (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) @@ -657,7 +620,7 @@ main [const-decl N (some B) Arity] :- !, std.do! [ prod-last {coq.arity->term Arity} Ty, if (ground_term Ty) (Sort = Ty) (Sort = {{Type}}), sort Univ = Sort, with-attributes (with-logging (structure.declare N B Univ)), - saturate_instances N, + with-attributes (with-logging (instance.saturate-instances)),%TODO this call doesn't seem to work here ]. main _ :- coq.error "Usage: HB.structure Definition := { A of A & … & A }". @@ -669,6 +632,35 @@ Elpi Export HB.structure. (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) +(* [HB.saturate_instances] saturates all instances possible *) + + +#[arguments(raw)] Elpi Command HB.saturate_instances. +#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi". +#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi". +Elpi Accumulate File "HB/common/stdpp.elpi". +Elpi Accumulate File "HB/common/database.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/structure.elpi". +Elpi Accumulate File "HB/context.elpi". +Elpi Accumulate File "HB/instance.elpi". +Elpi Accumulate File "HB/common/phant-abbreviation.elpi". +Elpi Accumulate File "HB/factory.elpi". +Elpi Accumulate File "HB/export.elpi". +Elpi Accumulate Db hb.db. +Elpi Accumulate lp:{{ +main [] :- !, with-attributes (with-logging (instance.saturate-instances)). +main _ :- coq.error "Usage: HB.saturate_instances". +}}. +Elpi Typecheck. +Elpi Export HB.saturate_instances. + +(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) +(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) +(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) + (** [HB.instance] associates to a type all the structures that can be obtained from the provided factory inhabitant. diff --git a/tests/instance_before_structure.v b/tests/instance_before_structure.v index 596dcbffe..ec8300c90 100644 --- a/tests/instance_before_structure.v +++ b/tests/instance_before_structure.v @@ -3,7 +3,9 @@ From HB Require Import structures. HB.mixin Record m1 T := { default1 : T }. HB.mixin Record m2 T := { default2 : T }. -#[verbose] + +HB.mixin Record m3 T := { default3 : T }. + HB.structure Definition s1 := { T of m1 T }. HB.instance Definition _ : m1 nat := m1.Build nat 1. @@ -15,15 +17,21 @@ HB.instance Definition _ : m2 nat := m2.Build nat 2. HB.about nat. (* only s1 on nat *) +HB.instance Definition _ : m3 nat := m3.Build nat 3. HB.structure Definition s2 := { T of m1 T & m2 T }. +HB.about nat. (* s2 is not there yet *) -(* here it works *) -(* HB.instance Definition _ : m2 nat := m2.Build nat 2. *) +HB.structure Definition s3 := { T of m3 T }. +HB.about nat. (* s2 has been instanciated but not s3 *) -HB.about nat. (* should be both s1 and s2 on nat *) + +(* here it works *) +HB.saturate_instances. +HB.about nat. (* all there *) Check @default1 nat. Check @default2 nat. +Check @default3 nat. From fd7d32b437031d8e76d799adc4648c3bea306ed8 Mon Sep 17 00:00:00 2001 From: thomas Date: Wed, 22 Feb 2023 17:52:07 +0100 Subject: [PATCH 12/37] starting to work on the undup function for list of terms with sets --- HB/common/database.elpi | 22 ++++++++++++++++------ structures.v | 2 +- 2 files changed, 17 insertions(+), 7 deletions(-) diff --git a/HB/common/database.elpi b/HB/common/database.elpi index b992ba852..16992d0df 100644 --- a/HB/common/database.elpi +++ b/HB/common/database.elpi @@ -138,12 +138,22 @@ factories-provide FLwP MLwP :- std.do! [ list-w-params.flatten-map FLwP factory-provides UnsortedMLwP, w-params.map UnsortedMLwP (p\t\ toposort-mixins) MLwP, ]. - - -pred undup-terms i:term, i:list term, o:list term. - undup-terms _ [] []. - undup-terms T[T1|TN] TN :- T == T1. - undup-terms T [T1|TN] [T1|TL] :- undup-terms T TN TL. +pred gref-set-undup S US. + gref-set-undup [] []. + gref-set-undup [G RS] US :- + if (coq.gref.set.mem G RS) + (gref-set-undup RS US) + (std.do! [gref-set-undup RS US1, coq.gref.set.add G (gref-set-undup RS US1) US]). + +pred undup-terms i:list term, o:list term. +undup-terms TL UTL :- !, std.do! [ + coq.gref.list->set TL TS, + gref-set-undup TS UTS, + ] + +% undup-terms T [] [T]. + % undup-terms T[T1|TN] (undup-terms T TN) :- T == T1. + % undup-terms T [T1|TN] [T1|TL] :- undup-terms T TN TL. % finds all unique types for which an instance was created pred findall-cs-types o:list term. diff --git a/structures.v b/structures.v index 6d2a68357..b549876fe 100644 --- a/structures.v +++ b/structures.v @@ -620,7 +620,7 @@ main [const-decl N (some B) Arity] :- !, std.do! [ prod-last {coq.arity->term Arity} Ty, if (ground_term Ty) (Sort = Ty) (Sort = {{Type}}), sort Univ = Sort, with-attributes (with-logging (structure.declare N B Univ)), - with-attributes (with-logging (instance.saturate-instances)),%TODO this call doesn't seem to work here + with-attributes (with-logging (instance.saturate-instances)),%TODO this call doesn't seem to work for the structure declared here ]. main _ :- coq.error "Usage: HB.structure Definition := { A of A & … & A }". From 050163a13ad4cf5defdea0080411d0cd2102a898 Mon Sep 17 00:00:00 2001 From: thomas Date: Thu, 23 Feb 2023 17:21:55 +0100 Subject: [PATCH 13/37] working on undup function and starting to rewrite the test for it --- HB/common/database.elpi | 40 +++++++++++++++++++++------------------- tests/findall_cs_type.v | 13 +++++++++++-- 2 files changed, 32 insertions(+), 21 deletions(-) diff --git a/HB/common/database.elpi b/HB/common/database.elpi index 16992d0df..3bc1450bb 100644 --- a/HB/common/database.elpi +++ b/HB/common/database.elpi @@ -138,29 +138,31 @@ factories-provide FLwP MLwP :- std.do! [ list-w-params.flatten-map FLwP factory-provides UnsortedMLwP, w-params.map UnsortedMLwP (p\t\ toposort-mixins) MLwP, ]. -pred gref-set-undup S US. - gref-set-undup [] []. - gref-set-undup [G RS] US :- - if (coq.gref.set.mem G RS) - (gref-set-undup RS US) - (std.do! [gref-set-undup RS US1, coq.gref.set.add G (gref-set-undup RS US1) US]). - -pred undup-terms i:list term, o:list term. -undup-terms TL UTL :- !, std.do! [ - coq.gref.list->set TL TS, - gref-set-undup TS UTS, - ] - -% undup-terms T [] [T]. - % undup-terms T[T1|TN] (undup-terms T TN) :- T == T1. - % undup-terms T [T1|TN] [T1|TL] :- undup-terms T TN TL. - -% finds all unique types for which an instance was created + +% pred gref-set-undup i:list gref, i:coq.gref.set, o:coq.gref.set. +% gref-set-undup (Gr::LN) S US :- +% if (coq.gref.set.mem Gr S) +% (gref-set-undup LN S US) +% (std.do! [gref-set-undup LN S US1, coq.gref.set.add Gr (gref-set-undup LN S US1) US]). +% gref-set-undup [] E E1 :- E = E1. +% pred undup-terms i:list term, o:list term. +% undup-terms [T|TL] UTL :- +% filter TL (x\ coq.gref.list->set) UTL + +pred undup-gref i:list gref, o:list gref. +undup-gref [] []. +undup-gref [Te | Tl] Utl :- + (coq.gref.list->set Tl TS), (coq.gref.set.mem Te TS), !, std.append [Te] Utl Utl. + undup-gref [_ | TL] UTL :- (undup-gref TL UTL). +% % 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, + std.map TypeListDup coq.term->gref TGref, + undup-gref TGref UTgref, + std.map UTgref (coq.env.global ) TypeList, ]. diff --git a/tests/findall_cs_type.v b/tests/findall_cs_type.v index 8af63c4ae..000becd3a 100644 --- a/tests/findall_cs_type.v +++ b/tests/findall_cs_type.v @@ -1,5 +1,6 @@ From HB Require Import structures. From elpi Require Import elpi. + HB.mixin Record m1 T := { default1 : T }. HB.mixin Record m2 T := { default1 : T }. @@ -8,10 +9,18 @@ Elpi Query HB.instance lp:{{std.assert! (findall-cs-types []) "a type was found" HB.instance Definition _ : m1 nat := m1.Build nat 1. HB.instance Definition _ : m2 nat := m2.Build nat 2. + +HB.instance Definition _ : m1 bool := m1.Build bool true. + +HB.instance Definition _ : m1 bool := m1.Build bool true. +HB.instance Definition _ : m1 nat := m1.Build nat 1. +HB.instance Definition _ : m2 nat := m2.Build nat 2. + (*no duplicates *) Elpi Query HB.instance lp:{{ - std.assert! (findall-cs-types [X]) "no type", - std.assert! (X = {{nat}}) "wrong type". + undup-gref [m1,m2] L, + std.assert! (std.last L m2) "no type", + }}. HB.instance Definition _ : m1 bool := m1.Build bool true. From 051df0c9d82518af0f4a3164ce1d006ca56ea2be Mon Sep 17 00:00:00 2001 From: thomas Date: Fri, 24 Feb 2023 17:57:53 +0100 Subject: [PATCH 14/37] rewriting the function to remove duplicates and the test for it --- HB/common/database.elpi | 33 ++++++++++++++------------------- tests/findall_cs_type.v | 25 ++++++++++++------------- 2 files changed, 26 insertions(+), 32 deletions(-) diff --git a/HB/common/database.elpi b/HB/common/database.elpi index 3bc1450bb..6224db302 100644 --- a/HB/common/database.elpi +++ b/HB/common/database.elpi @@ -139,30 +139,25 @@ factories-provide FLwP MLwP :- std.do! [ w-params.map UnsortedMLwP (p\t\ toposort-mixins) MLwP, ]. -% pred gref-set-undup i:list gref, i:coq.gref.set, o:coq.gref.set. -% gref-set-undup (Gr::LN) S US :- -% if (coq.gref.set.mem Gr S) -% (gref-set-undup LN S US) -% (std.do! [gref-set-undup LN S US1, coq.gref.set.add Gr (gref-set-undup LN S US1) US]). -% gref-set-undup [] E E1 :- E = E1. -% pred undup-terms i:list term, o:list term. -% undup-terms [T|TL] UTL :- -% filter TL (x\ coq.gref.list->set) UTL - -pred undup-gref i:list gref, o:list gref. -undup-gref [] []. -undup-gref [Te | Tl] Utl :- - (coq.gref.list->set Tl TS), (coq.gref.set.mem Te TS), !, std.append [Te] Utl Utl. - undup-gref [_ | TL] UTL :- (undup-gref TL UTL). -% % finds all unique types for which an instance was created +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, - std.map TypeListDup coq.term->gref TGref, - undup-gref TGref UTgref, - std.map UTgref (coq.env.global ) TypeList, + undup-terms TypeListDup TypeList, ]. diff --git a/tests/findall_cs_type.v b/tests/findall_cs_type.v index 000becd3a..d1c5eed98 100644 --- a/tests/findall_cs_type.v +++ b/tests/findall_cs_type.v @@ -3,29 +3,28 @@ From elpi Require Import elpi. HB.mixin Record m1 T := { default1 : T }. HB.mixin Record m2 T := { default1 : T }. - +HB.mixin Record m3 T := { default2 : T }. +HB.mixin Record m4 T := { default3 : T }. +HB.mixin Record m5 T := { default4 : T }. (* no types yet*) Elpi Query HB.instance lp:{{std.assert! (findall-cs-types []) "a type was found"}}. -HB.instance Definition _ : m1 nat := m1.Build nat 1. -HB.instance Definition _ : m2 nat := m2.Build nat 2. -HB.instance Definition _ : m1 bool := m1.Build bool true. -HB.instance Definition _ : m1 bool := m1.Build bool true. HB.instance Definition _ : m1 nat := m1.Build nat 1. HB.instance Definition _ : m2 nat := m2.Build nat 2. - (*no duplicates *) Elpi Query HB.instance lp:{{ - undup-gref [m1,m2] L, - std.assert! (std.last L m2) "no type", - + std.assert! (findall-cs-types [X]) "no type", + std.assert! (X = {{nat}}) "wrong type". }}. -HB.instance Definition _ : m1 bool := m1.Build bool true. - +HB.instance Definition _ : m4 bool := m4.Build bool true. +HB.instance Definition _ : m5 nat := m5.Build nat 5. +HB.instance Definition _ : m3 bool := m3.Build bool false. Elpi Query HB.instance lp:{{ - std.assert! (findall-cs-types [X,Y]) "no type", - std.assert! (Y = {{bool}}) "wrong type". + findall-cs-types Clauses, + std.assert! (std.length Clauses 2) "wrong number of clauses", + std.assert! (X = {{bool}}) "wrong type", + std.assert! (Y = {{nat}}) "wrong type". }}. \ No newline at end of file From 6815e50f6e9878d12896e67feb9d70db60527bd5 Mon Sep 17 00:00:00 2001 From: thomas Date: Mon, 27 Feb 2023 14:30:54 +0100 Subject: [PATCH 15/37] typo --- structures.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/structures.v b/structures.v index b549876fe..93c542790 100644 --- a/structures.v +++ b/structures.v @@ -620,7 +620,7 @@ main [const-decl N (some B) Arity] :- !, std.do! [ prod-last {coq.arity->term Arity} Ty, if (ground_term Ty) (Sort = Ty) (Sort = {{Type}}), sort Univ = Sort, with-attributes (with-logging (structure.declare N B Univ)), - with-attributes (with-logging (instance.saturate-instances)),%TODO this call doesn't seem to work for the structure declared here + with-attributes (with-logging (instance.saturate-instances)),%TODO this call doesn't seem to work for the structure defined here ]. main _ :- coq.error "Usage: HB.structure Definition := { A of A & … & A }". From 0f428cb50f3d53081ecaf17eb4177a7c86eaac5b Mon Sep 17 00:00:00 2001 From: Thomas Date: Mon, 13 Mar 2023 17:18:07 +0100 Subject: [PATCH 16/37] first draft at modifying the mixin src clauses for type parameters --- HB/common/database.elpi | 29 +++++++++++++++++++++++++++++ HB/instance.elpi | 11 +++++++++-- 2 files changed, 38 insertions(+), 2 deletions(-) diff --git a/HB/common/database.elpi b/HB/common/database.elpi index 6224db302..0a488cbc2 100644 --- a/HB/common/database.elpi +++ b/HB/common/database.elpi @@ -220,6 +220,8 @@ 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. + pred findall-type-src o:list term. findall-type-src TL :- std.map {std.findall (mixin-src T_ M_ S_)} mixin-src_type TL. @@ -342,6 +344,33 @@ 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 has-mixin-instance o:cs-pattern, o:mixinname, o:gref. + +pred mixin-src->has-mixin-instance o:prop, o:prop. + +mixin-src->has-mixin-instance (mixin-src T M I) (has-mixin-instance (cs-gref G) M IHd) :- + term->gref T G, term->gref I IHd. + +mixin-src->has-mixin-instance (mixin-src (prod _ _ _) M I) (has-mixin-instance cs-prod M IHd):- + term->gref I IHd. + +mixin-src->has-mixin-instance (mixin-src (sort U) M I) (has-mixin-instance (cs-sort U) M IHd):- + term->gref I IHd. + + +pred mk-src i:term, i:mixinname, i:term, i:list prop,o:prop. + +mk-src (global GR as T) M I TODO (mixin-src T M I :- TODO) :- + has-mixin-instance (cs-gref GR) M IHd, term->gref I IHd. + +mk-src (app [global GR|_] as T) M I TODO (mixin-src T M I :- TODO) :- + has-mixin-instance (cs-gref GR) M IHd, term->gref I IHd. + +% mk-src (prod N S F) M I TODO (pi A B \ C A B) :- + +% is-structure S, +% pi a b \ mk-src (F a) M _ [has-cs-instance a b|TODO] (C a b). + pred term->cs-pattern i:term, o:cs-pattern. term->cs-pattern (prod _ _ _) cs-prod. term->cs-pattern (sort U) (cs-sort U). diff --git a/HB/instance.elpi b/HB/instance.elpi index 1dc1b3e8e..4f1fce404 100644 --- a/HB/instance.elpi +++ b/HB/instance.elpi @@ -199,8 +199,12 @@ mk-factory-sort-factory AliasGR CSL :- std.do! [ pred saturate-instances. saturate-instances :- std.do! [ findall-type-src TL, + % findall-has-mixin-instance ClausesHas, + % coq.say "clauses : "ClausesHas, + % std.map ClausesHas mk-src Clauses, findall-classes Classes, - std.forall TL (t\ (declare-all t Classes _)), + Clauses => std.forall TL (t\ (declare-all t Classes _)), + coq.say "clauses : "Clauses, ]. /* ------------------------------------------------------------------------- */ @@ -308,7 +312,7 @@ declare-canonical-instances-from-factory-and-local-builders % on T pred declare-canonical-instances-from-factory i:factoryname, i:term, i:term, o: list prop, o:list (pair id constant). -declare-canonical-instances-from-factory Factory T F Clauses CSL :- std.do! [ +declare-canonical-instances-from-factory Factory T F ClausesHas CSL :- std.do! [ % The order of the following two "under...do!" is crucial, % priority must be given to canonical mixins % as they are the ones which guarantee forgetful inheritance @@ -317,6 +321,9 @@ declare-canonical-instances-from-factory Factory T F Clauses CSL :- std.do! [ synthesis.under-local-canonical-mixins-of.do! T [ list-w-params_list {factory-provides Factory} ML, add-all-mixins T Factory ML tt Clauses MCSL, + std.map-filter Clauses mixin-src->has-mixin-instance ClausesHas, + + %std.map ClausesHas has-mixin-instance->mixin-src Clauses, Clauses =>instance.declare-all T {findall-classes-for ML} CCSL, ] ], From 071619a078b20677db83959fe704ba2b842fa4a3 Mon Sep 17 00:00:00 2001 From: Thomas Date: Tue, 14 Mar 2023 11:45:07 +0100 Subject: [PATCH 17/37] continuing the transformation of clauses --- HB/common/database.elpi | 12 +++++++++--- HB/instance.elpi | 9 +++++---- 2 files changed, 14 insertions(+), 7 deletions(-) diff --git a/HB/common/database.elpi b/HB/common/database.elpi index 0a488cbc2..a4a76dc72 100644 --- a/HB/common/database.elpi +++ b/HB/common/database.elpi @@ -221,6 +221,8 @@ findall-builders LFIL :- 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 term. findall-type-src TL :- @@ -366,10 +368,14 @@ mk-src (global GR as T) M I TODO (mixin-src T M I :- TODO) :- mk-src (app [global GR|_] as T) M I TODO (mixin-src T M I :- TODO) :- has-mixin-instance (cs-gref GR) M IHd, term->gref I IHd. -% mk-src (prod N S F) M I TODO (pi A B \ C A B) :- +mk-src (prod _ S F) M I_ TODO (pi A B \ C A B) :- + (term->gref S SG), is-structure SG, + pi a b pa pb \ + mk-src (F a) M _ [coq.unify-eq a pa ok|TODO] (C a b), + mk-src (F b) M _ [coq.unify-eq b pb ok|TODO] (C a b). -% is-structure S, -% pi a b \ mk-src (F a) M _ [has-cs-instance a b|TODO] (C a b). +pred mk-src-map i:prop, o:prop. +mk-src-map (has-mixin-instance _ M IHd) C :- mk-src _ M I [] C, term->gref I IHd. pred term->cs-pattern i:term, o:cs-pattern. term->cs-pattern (prod _ _ _) cs-prod. diff --git a/HB/instance.elpi b/HB/instance.elpi index 4f1fce404..859cf4bcb 100644 --- a/HB/instance.elpi +++ b/HB/instance.elpi @@ -199,12 +199,13 @@ mk-factory-sort-factory AliasGR CSL :- std.do! [ pred saturate-instances. saturate-instances :- std.do! [ findall-type-src TL, - % findall-has-mixin-instance ClausesHas, - % coq.say "clauses : "ClausesHas, - % std.map ClausesHas mk-src Clauses, + findall-has-mixin-instance ClausesHas, + coq.say "clauseshas : "ClausesHas, + std.map ClausesHas mk-src-map Clauses, findall-classes Classes, + coq.say "clausessrc : "Clauses, Clauses => std.forall TL (t\ (declare-all t Classes _)), - coq.say "clauses : "Clauses, + ]. /* ------------------------------------------------------------------------- */ From d2a8a5f9dd9a1f700282d7434887a50b651f9880 Mon Sep 17 00:00:00 2001 From: Thomas Date: Tue, 14 Mar 2023 17:59:55 +0100 Subject: [PATCH 18/37] working on saturating instances with types --- HB/common/database.elpi | 61 ++++++++++++++++++++++++--------- HB/instance.elpi | 10 ++++-- HB/structure.elpi | 5 ++- structures.v | 1 - tests/instance_params_no_type.v | 37 ++++++++++++++++++-- 5 files changed, 90 insertions(+), 24 deletions(-) diff --git a/HB/common/database.elpi b/HB/common/database.elpi index a4a76dc72..e255a9002 100644 --- a/HB/common/database.elpi +++ b/HB/common/database.elpi @@ -14,6 +14,9 @@ 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. @@ -224,9 +227,9 @@ 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 term. +pred findall-type-src o:list cs-pattern. findall-type-src TL :- - std.map {std.findall (mixin-src T_ M_ S_)} mixin-src_type TL. + std.map {std.findall (has-mixin-instance T_ M_ S_)} has-mixin-instance_cspat TL. pred findall-mixin-src i:term, o:list mixinname. findall-mixin-src T ML :- @@ -359,23 +362,47 @@ mixin-src->has-mixin-instance (mixin-src (prod _ _ _) M I) (has-mixin-instance c mixin-src->has-mixin-instance (mixin-src (sort U) M I) (has-mixin-instance (cs-sort U) M IHd):- term->gref I IHd. - -pred mk-src i:term, i:mixinname, i:term, i:list prop,o:prop. - -mk-src (global GR as T) M I TODO (mixin-src T M I :- TODO) :- - has-mixin-instance (cs-gref GR) M IHd, term->gref I IHd. - -mk-src (app [global GR|_] as T) M I TODO (mixin-src T M I :- TODO) :- - has-mixin-instance (cs-gref GR) M IHd, term->gref I IHd. - -mk-src (prod _ S F) M I_ TODO (pi A B \ C A B) :- - (term->gref S SG), is-structure SG, - pi a b pa pb \ - mk-src (F a) M _ [coq.unify-eq a pa ok|TODO] (C a b), - mk-src (F b) M _ [coq.unify-eq b pb ok|TODO] (C a b). +pred find-instance i:term, i:term, o:term. + +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 prop, % todo list + o:prop. + +% mk-src (global _ as T) M I TODO (mixin-src T M I :- TODO). % impossible + +mk-src (app [_|Args]) M I TODO (mixin-src T M I :- TODO) :- + std.last Args T', + . + +% coq.mk-app ---- avoids ----> app[ app[ I, a ], b] +% invariant: mk-src Ty _ I _ _ ---> I : Ty + +% mk-src I : A -> B +% create a : A +% I a : B +mk-src (prod N_ (sort _) F) M I TODO (pi A \ C A) :- !, + pi a\ + sigma Ia\ + coq.mk-app I [a] Ia, % Ia = app[I,a] + mk-src (F a) M Ia TODO (C a). + +mk-src (prod N_ S F) M I TODO (pi A pA \ C A pA) :- + term->gref S SG, is-structure SG, + pi a\ + sigma Ia\ + pi pa \ + coq.mk-app I [a] Ia, + mk-src (F a) M Ia [find-instance a S pa|TODO] (C a pa). pred mk-src-map i:prop, o:prop. -mk-src-map (has-mixin-instance _ M IHd) C :- mk-src _ M I [] C, term->gref I IHd. +mk-src-map (has-mixin-instance _ M IHd) C :- + T = global IHd, + /*coq.env.typeof IHd Ty,*/ + coq.typecheck T Ty ok, + std.spy(mk-src Ty M T [] C). pred term->cs-pattern i:term, o:cs-pattern. term->cs-pattern (prod _ _ _) cs-prod. diff --git a/HB/instance.elpi b/HB/instance.elpi index 859cf4bcb..61bb18836 100644 --- a/HB/instance.elpi +++ b/HB/instance.elpi @@ -198,16 +198,20 @@ mk-factory-sort-factory AliasGR CSL :- std.do! [ % create instances for all possible combinations of (simple) types and structure compatible pred saturate-instances. saturate-instances :- std.do! [ - findall-type-src TL, + findall-type-src PL, findall-has-mixin-instance ClausesHas, coq.say "clauseshas : "ClausesHas, - std.map ClausesHas mk-src-map Clauses, + std.map-filter ClausesHas mk-src-map Clauses, findall-classes Classes, - coq.say "clausessrc : "Clauses, + std.map-filter PL hack TL, + coq.say "clausessrc : " Clauses TL, Clauses => std.forall TL (t\ (declare-all t Classes _)), ]. +pred hack i:cs-pattern, o:term. +hack (cs-gref GR) (global GR). + /* ------------------------------------------------------------------------- */ /* ----------------------------- private code ------------------------------ */ /* ------------------------------------------------------------------------- */ diff --git a/HB/structure.elpi b/HB/structure.elpi index addf308a4..36be56e38 100644 --- a/HB/structure.elpi +++ b/HB/structure.elpi @@ -210,7 +210,10 @@ declare Module BSkel Sort :- std.do! [ NewClauses => factory.declare-abbrev Module (factory.by-classname ClassName), NewClauses => if-MC-compat (private.mc-compat-structure Module ModulePath MLToExport - {w-params.nparams MLwP} ClassProjection GRPack) + {w-params.nparams MLwP} ClassProjection GRPack), + + NewClauses => instance.saturate-instances, + ]. /* ------------------------------------------------------------------------- */ diff --git a/structures.v b/structures.v index 93c542790..8c1fc698e 100644 --- a/structures.v +++ b/structures.v @@ -620,7 +620,6 @@ main [const-decl N (some B) Arity] :- !, std.do! [ prod-last {coq.arity->term Arity} Ty, if (ground_term Ty) (Sort = Ty) (Sort = {{Type}}), sort Univ = Sort, with-attributes (with-logging (structure.declare N B Univ)), - with-attributes (with-logging (instance.saturate-instances)),%TODO this call doesn't seem to work for the structure defined here ]. main _ :- coq.error "Usage: HB.structure Definition := { A of A & … & A }". diff --git a/tests/instance_params_no_type.v b/tests/instance_params_no_type.v index 5220be111..476d97bb3 100644 --- a/tests/instance_params_no_type.v +++ b/tests/instance_params_no_type.v @@ -1,7 +1,40 @@ From HB Require Import structures. HB.mixin Record is_foo P A := { op : P -> A -> A }. + +HB.instance Definition nat_foo P := is_foo.Build P nat (fun _ x => x). +HB.instance Definition list_foo P := is_foo.Build P (list P) (fun _ x => x). + HB.structure Definition foo P := { A of is_foo P A }. -Axiom f : forall T, T -> nat -> nat. -HB.instance Definition bar P := is_foo.Build P nat (f P). \ No newline at end of file +Section try1. +Variable A : Type. +.... list A .... + +(fun A => {| + foo.sort := list..; + foo.class := + {| foo.instance_params_no_type_is_foo_mixin := list_foo A |} + |} ). + + +HB.about foo. + +(* Elpi Trace Browser. *) +Check nat_foo. +Check list_foo. +HB.mixin Record is_b A:= { default : A }. +Check foo.type. +Print foo.type. +Print Module foo. +Print foo.axioms_. +(*Elpi Trace Browser. *) +HB.structure Definition b := { A of is_b A}. +HB.instance Definition nat_b := is_b.Build nat 0. + +HB.mixin Record is_bar (P : b.type) A := { test : P -> A -> A }. + +HB.structure Definition bar P := { A of is_bar P A}. +HB.instance Definition list_bar P := is_bar.Build P (list P) (fun _ x => x). +Check list_bar. + From d79445bf8d5fa99e7ed5f4b8bf3e006f3fbd4e08 Mon Sep 17 00:00:00 2001 From: Thomas Date: Wed, 15 Mar 2023 17:41:53 +0100 Subject: [PATCH 19/37] starting to work on #347 --- HB/common/database.elpi | 51 ++++++++++++++-------- HB/instance.elpi | 1 + tests/instance_merge_with_distinct_param.v | 26 +++++++++++ tests/instance_params_no_type.v | 7 ++- 4 files changed, 64 insertions(+), 21 deletions(-) create mode 100644 tests/instance_merge_with_distinct_param.v diff --git a/HB/common/database.elpi b/HB/common/database.elpi index e255a9002..754688a1b 100644 --- a/HB/common/database.elpi +++ b/HB/common/database.elpi @@ -15,7 +15,7 @@ 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. +has-mixin-instance_cspat (has-mixin-instance P _ _ _) P. pred mixin-src_type i:prop, o:term. mixin-src_type (mixin-src T _ _ ) T. @@ -225,11 +225,11 @@ findall-builders LFIL :- pred findall-has-mixin-instance o:list prop. findall-has-mixin-instance CL :- - std.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_)} has-mixin-instance_cspat 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 :- @@ -349,18 +349,30 @@ 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 has-mixin-instance o:cs-pattern, o:mixinname, o:gref. +pred arg-is-instance i:term, i:term, o:bool. +arg-is-instance _ _ tt. + +pred args-is-instance i:term, o:list bool. +args-is-instance (app [_|[A|Args]] as T) [B|L] :- + arg-is-instance T A B, args-is-instance (app [_|Args]) L. +args-is-instance (sort _U) []. +args-is-instance (prod _N _S _F) []. + +pred has-mixin-instance o:cs-pattern, o:mixinname, o:gref, o:list bool. + +% change order of cases +% if I isn't gref ? pred mixin-src->has-mixin-instance o:prop, o:prop. -mixin-src->has-mixin-instance (mixin-src T M I) (has-mixin-instance (cs-gref G) M IHd) :- - term->gref T G, term->gref I IHd. +mixin-src->has-mixin-instance (mixin-src T M I) (has-mixin-instance (cs-gref G) M IHd A) :- + term->gref T G, term->gref I IHd, args-is-instance I A. -mixin-src->has-mixin-instance (mixin-src (prod _ _ _) M I) (has-mixin-instance cs-prod M IHd):- - term->gref I IHd. +mixin-src->has-mixin-instance (mixin-src (prod _ _ _) M I) (has-mixin-instance cs-prod M IHd A):- + term->gref I IHd, args-is-instance I A. -mixin-src->has-mixin-instance (mixin-src (sort U) M I) (has-mixin-instance (cs-sort U) M IHd):- - term->gref I IHd. +mixin-src->has-mixin-instance (mixin-src (sort U) M I) (has-mixin-instance (cs-sort U) M IHd A):- + term->gref I IHd, args-is-instance I A. pred find-instance i:term, i:term, o:term. @@ -368,14 +380,15 @@ 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, % todo list o:prop. % mk-src (global _ as T) M I TODO (mixin-src T M I :- TODO). % impossible -mk-src (app [_|Args]) M I TODO (mixin-src T M I :- TODO) :- - std.last Args T', - . +mk-src (app [_|Args]) M I _L TODO (mixin-src T M I :- TODO) :- + std.last Args T. + % std.last Args T', % coq.mk-app ---- avoids ----> app[ app[ I, a ], b] % invariant: mk-src Ty _ I _ _ ---> I : Ty @@ -383,26 +396,26 @@ mk-src (app [_|Args]) M I TODO (mixin-src T M I :- TODO) :- % mk-src I : A -> B % create a : A % I a : B -mk-src (prod N_ (sort _) F) M I TODO (pi A \ C A) :- !, +mk-src (prod N_ (sort _) F) M I L TODO (pi A \ C A) :- !, pi a\ sigma Ia\ coq.mk-app I [a] Ia, % Ia = app[I,a] - mk-src (F a) M Ia TODO (C a). + mk-src (F a) M Ia L TODO (C a). -mk-src (prod N_ S F) M I TODO (pi A pA \ C A pA) :- +mk-src (prod N_ S F) M I L TODO (pi A pA \ C A pA) :- term->gref S SG, is-structure SG, pi a\ sigma Ia\ pi pa \ coq.mk-app I [a] Ia, - mk-src (F a) M Ia [find-instance a S pa|TODO] (C a pa). + mk-src (F a) M Ia L [find-instance a S pa|TODO] (C a pa). pred mk-src-map i:prop, o:prop. -mk-src-map (has-mixin-instance _ M IHd) C :- +mk-src-map (has-mixin-instance _ M IHd []) C :- T = global IHd, /*coq.env.typeof IHd Ty,*/ coq.typecheck T Ty ok, - std.spy(mk-src Ty M T [] C). + std.spy(mk-src Ty M T [] [] C). pred term->cs-pattern i:term, o:cs-pattern. term->cs-pattern (prod _ _ _) cs-prod. diff --git a/HB/instance.elpi b/HB/instance.elpi index 61bb18836..936d12969 100644 --- a/HB/instance.elpi +++ b/HB/instance.elpi @@ -326,6 +326,7 @@ declare-canonical-instances-from-factory Factory T F ClausesHas CSL :- std.do! [ synthesis.under-local-canonical-mixins-of.do! T [ list-w-params_list {factory-provides Factory} ML, add-all-mixins T Factory ML tt Clauses MCSL, + coq.say "clausesbef : " Clauses, std.map-filter Clauses mixin-src->has-mixin-instance ClausesHas, %std.map ClausesHas has-mixin-instance->mixin-src Clauses, diff --git a/tests/instance_merge_with_distinct_param.v b/tests/instance_merge_with_distinct_param.v new file mode 100644 index 000000000..0f4d44921 --- /dev/null +++ b/tests/instance_merge_with_distinct_param.v @@ -0,0 +1,26 @@ +From HB Require Import structures. + +HB.mixin Record m1 T := { default1 : T }. + +HB.mixin Record m2 T := { default2 : T }. + +HB.structure Definition s1 := { T of m1 T }. +HB.structure Definition s2 := { T of m2 T }. + +HB.instance Definition _ (X : s1.type) : m1 (list X) := + m1.Build (list X) (cons default1 nil). +HB.instance Definition list_m2 (X : s2.type) : m2 (list X) := + m2.Build (list X) (cons default2 nil). + +HB.structure Definition s3 := { T of m1 T & m2 T }. + +HB.about list. (* should have s3 *) + +(* The s3 instance on list should be synthetized automatically, *) +(* this is nontrivial because the parameters are not the same *) +(* but there is a join in the hierarchy, so it can be defined. *) +(* Actually just recalling the list_m2 instance above suffices. *) +HB.instance Definition _ (X : s3.type) := list_m2 X. +HB.about list. + + diff --git a/tests/instance_params_no_type.v b/tests/instance_params_no_type.v index 476d97bb3..5fdd953e9 100644 --- a/tests/instance_params_no_type.v +++ b/tests/instance_params_no_type.v @@ -4,12 +4,15 @@ HB.mixin Record is_foo P A := { op : P -> A -> A }. HB.instance Definition nat_foo P := is_foo.Build P nat (fun _ x => x). HB.instance Definition list_foo P := is_foo.Build P (list P) (fun _ x => x). +HB.instance Definition list_foo' P A:= is_foo.Build P (list A) (fun _ x => x). + +About list_foo'. HB.structure Definition foo P := { A of is_foo P A }. Section try1. Variable A : Type. -.... list A .... +(* .... list A .... (fun A => {| foo.sort := list..; @@ -18,7 +21,7 @@ Variable A : Type. |} ). -HB.about foo. +HB.about foo. *) (* Elpi Trace Browser. *) Check nat_foo. From c4995139d42876507e19974a31192447d328687c Mon Sep 17 00:00:00 2001 From: Thomas Date: Fri, 17 Mar 2023 18:17:07 +0100 Subject: [PATCH 20/37] changing how the boolean list works : with section parameters --- HB/common/database.elpi | 58 ++++++++++++++++++++++++++--------------- HB/instance.elpi | 40 +++++++++++++++------------- 2 files changed, 59 insertions(+), 39 deletions(-) diff --git a/HB/common/database.elpi b/HB/common/database.elpi index 754688a1b..46bcec53d 100644 --- a/HB/common/database.elpi +++ b/HB/common/database.elpi @@ -20,12 +20,18 @@ 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_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. @@ -349,30 +355,40 @@ 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 arg-is-instance i:term, i:term, i:term, o:bool. + +% arg-is-instance (app [_] as T) I A tt :- +% extract-conclusion-params T I PL, std.mem! PL A. + +% arg-is-instance _ _ _ ff. -pred arg-is-instance i:term, i:term, o:bool. -arg-is-instance _ _ tt. +pred args-is-instance i:term, i:list constant, o:list bool. -pred args-is-instance i:term, o:list bool. -args-is-instance (app [_|[A|Args]] as T) [B|L] :- - arg-is-instance T A B, args-is-instance (app [_|Args]) L. -args-is-instance (sort _U) []. -args-is-instance (prod _N _S _F) []. +args-is-instance Ty SectionParams L :- + + safe-dest-app Ty _ _Args, + %factory-alias->gref GR F, factory-nparams F NP,std.split-at NP Args Params Args2, + % change std.mem! for something that checks if the parameters appears in the term + std.map SectionParams (x\ r \ (if (true) (r = tt) (r = ff))) L. pred has-mixin-instance o:cs-pattern, o:mixinname, o:gref, o:list bool. % change order of cases % if I isn't gref ? -pred mixin-src->has-mixin-instance o:prop, o:prop. +pred mixin-src->has-mixin-instance i:list constant, o:prop, o:prop. + + +mixin-src->has-mixin-instance SectionParams (mixin-src T M I) (has-mixin-instance (cs-gref G) M IHd A) :- + term->gref T G, term->gref I IHd, coq.typecheck T Ty ok, args-is-instance Ty SectionParams A. -mixin-src->has-mixin-instance (mixin-src T M I) (has-mixin-instance (cs-gref G) M IHd A) :- - term->gref T G, term->gref I IHd, args-is-instance I A. +mixin-src->has-mixin-instance _SectionParams(mixin-src (prod _ _ _ ) M I) (has-mixin-instance cs-prod M IHd []):- + term->gref I IHd. -mixin-src->has-mixin-instance (mixin-src (prod _ _ _) M I) (has-mixin-instance cs-prod M IHd A):- - term->gref I IHd, args-is-instance I A. +mixin-src->has-mixin-instance _SectionParams(mixin-src (sort U) M I) (has-mixin-instance (cs-sort U) M IHd []):- + term->gref I IHd. -mixin-src->has-mixin-instance (mixin-src (sort U) M I) (has-mixin-instance (cs-sort U) M IHd A):- - term->gref I IHd, args-is-instance I A. +% mixin-src->has-mixin-instance _SectionParams(mixin-src (app [_]as T) M I) (has-mixin-instance (cs-gref G) M IHd A) :- +% term->gref T G, term->gref I IHd, coq.typecheck T Ty ok, args-is-instance Ty A. pred find-instance i:term, i:term, o:term. @@ -386,7 +402,7 @@ pred mk-src % mk-src (global _ as T) M I TODO (mixin-src T M I :- TODO). % impossible -mk-src (app [_|Args]) M I _L TODO (mixin-src T M I :- TODO) :- +mk-src (app [_|Args]) M I _ TODO (mixin-src T M I :- TODO) :- std.last Args T. % std.last Args T', @@ -396,26 +412,26 @@ mk-src (app [_|Args]) M I _L TODO (mixin-src T M I :- TODO) :- % mk-src I : A -> B % create a : A % I a : B -mk-src (prod N_ (sort _) F) M I L TODO (pi A \ C A) :- !, +mk-src (prod N_ (sort _) F) M I [tt|Rest] TODO (pi A \ C A) :- !, pi a\ sigma Ia\ coq.mk-app I [a] Ia, % Ia = app[I,a] - mk-src (F a) M Ia L TODO (C a). + mk-src (F a) M Ia Rest TODO (C a). -mk-src (prod N_ S F) M I L TODO (pi A pA \ C A pA) :- +mk-src (prod N_ S F) M I [ff|Rest] TODO (pi A pA \ C A pA) :- term->gref S SG, is-structure SG, pi a\ sigma Ia\ pi pa \ coq.mk-app I [a] Ia, - mk-src (F a) M Ia L [find-instance a S pa|TODO] (C a pa). + mk-src (F a) M Ia Rest [find-instance a S pa|TODO] (C a pa). pred mk-src-map i:prop, o:prop. -mk-src-map (has-mixin-instance _ M IHd []) C :- +mk-src-map (has-mixin-instance _ M IHd L) C :- T = global IHd, /*coq.env.typeof IHd Ty,*/ coq.typecheck T Ty ok, - std.spy(mk-src Ty M T [] [] C). + std.spy(mk-src Ty M T L [] C). pred term->cs-pattern i:term, o:cs-pattern. term->cs-pattern (prod _ _ _) cs-prod. diff --git a/HB/instance.elpi b/HB/instance.elpi index 936d12969..7eed6db46 100644 --- a/HB/instance.elpi +++ b/HB/instance.elpi @@ -14,8 +14,8 @@ declare-existing T0 F0 :- std.do! [ std.assert! (coq.safe-dest-app FTy (global FactoryAlias) _) "The type of the instance is not a factory", factory-alias->gref FactoryAlias Factory, - private.declare-instance Factory T F Clauses _, - acc-clauses current Clauses + private.declare-instance Factory T F _ Clauses _, + acc-clauses current Clauses, ]. % [declare-const N B Ty] adds a Definition N : Ty := B where Ty is a factory @@ -33,11 +33,12 @@ declare-const Name BodySkel TyWPSkel CSL :- std.do! [ % A side effect of opening a section is loosing meta data associated % with instances, in particular builder tags are lost if-verbose (coq.say "HB: skipping section opening"), - SectionBody = Body + SectionBody = Body, + SectionParams = [] ) ( SectionName is "hb_instance_" ^ {std.any->string {new_int}}, log.coq.env.begin-section SectionName, - private.postulate-arity TyWP [] Body SectionBody SectionTy + private.postulate-arity TyWP [] Body SectionBody SectionTy SectionParams ), % identify the factory @@ -66,7 +67,7 @@ declare-const Name BodySkel TyWPSkel CSL :- std.do! [ private.check-non-forgetful-inheritance TheType Factory, - private.declare-instance Factory TheType TheFactory Clauses CSL, + private.declare-instance Factory TheType TheFactory SectionParams Clauses CSL, % handle parameters via a section -- end if (TyWP = arity _) true ( @@ -220,9 +221,9 @@ namespace private { shorten coq.{ term->gref, subst-fun, safe-dest-app, mk-app, mk-eta, subst-prod }. -pred declare-instance i:factoryname, i:term, i:term, +pred declare-instance i:factoryname, i:term, i:term, i:list constant, o:list prop, o:list (pair id constant). -declare-instance Factory T F Clauses CSL :- +declare-instance Factory T F _SectionParams Clauses CSL :- current-mode (builder-from T TheFactory FGR _), !, if (get-option "local" tt) (coq.error "HB: declare-instance: cannot make builders local. @@ -230,8 +231,8 @@ declare-instance Factory T F Clauses CSL :- !, declare-canonical-instances-from-factory-and-local-builders Factory T F TheFactory FGR Clauses CSL. -declare-instance Factory T F Clauses CSL :- - declare-canonical-instances-from-factory Factory T F Clauses1 CSL, +declare-instance Factory T F SectionParams Clauses CSL :- + declare-canonical-instances-from-factory Factory T F SectionParams Clauses1 CSL, if (get-option "export" tt) (coq.env.current-library File, std.map CSL (x\r\ sigma i c\ x = pr i c, r = instance-to-export File i c) Clauses2) @@ -283,18 +284,21 @@ add-all-mixins T FGR ML MakeCanon Clauses CSL :- std.do! [ % corresponding to parameters in arity A. TS is T applied % to all section variables (and hd-beta reduced). Acc should % be [] at call site. -pred postulate-arity i:arity, i:list term, i:term, o:term, o:term. -postulate-arity (parameter ID _ S A) Acc T T1 Ty :- +pred postulate-arity i:arity, i:list constant, i:term, o:term, o:term, o:list constant. +postulate-arity (parameter ID _ S A) Acc T T1 Ty Params :- std.assert-ok! (coq.typecheck-ty S _) "arity parameter illtyped", if-verbose (coq.say {header} "postulating" ID), if (var S) (coq.fresh-type S) true, log.coq.env.add-section-variable-noimplicits ID S C, Var = global (const C), - postulate-arity (A Var) [Var|Acc] T T1 Ty. -postulate-arity (arity Ty) ArgsRev X T Ty :- - hd-beta X {std.rev ArgsRev} X1 Stack1, + postulate-arity (A Var) [C|Acc] T T1 Ty Params. +postulate-arity (arity Ty) ParamsRev X T Ty Params :- + std.rev ParamsRev Params, + std.map Params (c\o\ o = global (const c)) Args, + hd-beta X Args X1 Stack1, unwind X1 Stack1 T. + % We find the new mixins that F build, we build them and shedule them % for becoming builders at section closing time. We also declare % all canonical instances these new mixins allow for, so that the user @@ -316,8 +320,8 @@ declare-canonical-instances-from-factory-and-local-builders % it uses all known builders to declare canonical instances of structures % on T pred declare-canonical-instances-from-factory - i:factoryname, i:term, i:term, o: list prop, o:list (pair id constant). -declare-canonical-instances-from-factory Factory T F ClausesHas CSL :- std.do! [ + i:factoryname, i:term, i:term, i:list constant, o: list prop, o:list (pair id constant). +declare-canonical-instances-from-factory Factory T F SectionParams ClausesHas CSL :- std.do! [ % The order of the following two "under...do!" is crucial, % priority must be given to canonical mixins % as they are the ones which guarantee forgetful inheritance @@ -327,10 +331,10 @@ declare-canonical-instances-from-factory Factory T F ClausesHas CSL :- std.do! [ list-w-params_list {factory-provides Factory} ML, add-all-mixins T Factory ML tt Clauses MCSL, coq.say "clausesbef : " Clauses, - std.map-filter Clauses mixin-src->has-mixin-instance ClausesHas, + std.map-filter Clauses (mixin-src->has-mixin-instance SectionParams) ClausesHas, %std.map ClausesHas has-mixin-instance->mixin-src Clauses, - Clauses =>instance.declare-all T {findall-classes-for ML} CCSL, + ClausesHas =>instance.declare-all T {findall-classes-for ML} CCSL, ] ], std.append MCSL CCSL CSL From 4025a2cdc6954da4e21be16b4e456627ada47387 Mon Sep 17 00:00:00 2001 From: Thomas Date: Wed, 22 Mar 2023 13:07:41 +0100 Subject: [PATCH 21/37] writing the boolean computing functions --- HB/common/database.elpi | 52 ++++++++++++++++++++++++----------------- 1 file changed, 30 insertions(+), 22 deletions(-) diff --git a/HB/common/database.elpi b/HB/common/database.elpi index 46bcec53d..3b51e696b 100644 --- a/HB/common/database.elpi +++ b/HB/common/database.elpi @@ -362,33 +362,41 @@ has-cs-instance GTy (cs-instance _ (cs-gref GTy) _). % arg-is-instance _ _ _ ff. -pred args-is-instance i:term, i:list constant, o:list bool. +pred param-in-term i:term, i:constant, o:bool. +param-in-term (app [global (const C)|_]) C tt. +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 T C B :- whd1 T T1, !, param-in-term T1 C B. -args-is-instance Ty SectionParams L :- + +pred sect-params-in-term i:list constant, i:term, o:list bool. + +sect-params-in-term SectionParams Ty L :- safe-dest-app Ty _ _Args, %factory-alias->gref GR F, factory-nparams F NP,std.split-at NP Args Params Args2, % change std.mem! for something that checks if the parameters appears in the term - std.map SectionParams (x\ r \ (if (true) (r = tt) (r = ff))) L. + std.map SectionParams (x\ o \ (param-in-term Ty x o)) L. pred has-mixin-instance o:cs-pattern, o:mixinname, o:gref, o:list bool. % change order of cases % if I isn't gref ? -pred mixin-src->has-mixin-instance i:list constant, o:prop, o:prop. - +pred mixin-src->has-mixin-instance i:list constant, i:prop, o:prop. -mixin-src->has-mixin-instance SectionParams (mixin-src T M I) (has-mixin-instance (cs-gref G) M IHd A) :- - term->gref T G, term->gref I IHd, coq.typecheck T Ty ok, args-is-instance Ty SectionParams A. +mixin-src->has-mixin-instance SectionParams (mixin-src (app [global GR|_] as T) M I) (has-mixin-instance (cs-gref GR) M IHd A) :- + term->gref I IHd, coq.typecheck T Ty ok, sect-params-in-term SectionParams Ty A. + +mixin-src->has-mixin-instance SectionParams (mixin-src (prod _ _ _ as T) M I) (has-mixin-instance cs-prod M IHd BL):- + term->gref I IHd, coq.typecheck T Ty ok, sect-params-in-term SectionParams Ty BL. -mixin-src->has-mixin-instance _SectionParams(mixin-src (prod _ _ _ ) M I) (has-mixin-instance cs-prod M IHd []):- - term->gref I IHd. + % mixin-src->has-mixin-instance SectionParams (mixin-src T M I) (has-mixin-instance (cs-gref G) M IHd A) :- + % term->gref T G, term->gref I IHd, coq.typecheck T Ty ok, sect-params-in-term SectionParams Ty A. -mixin-src->has-mixin-instance _SectionParams(mixin-src (sort U) M I) (has-mixin-instance (cs-sort U) M IHd []):- - term->gref I IHd. +% mixin-src->has-mixin-instance SectionParams (mixin-src (sort U) M I) (has-mixin-instance (cs-sort U) M (global I) BL):- +% term->gref I IHd, coq.env.typeof IHd Ty, sect-params-in-term SectionParams Ty BL. -% mixin-src->has-mixin-instance _SectionParams(mixin-src (app [_]as T) M I) (has-mixin-instance (cs-gref G) M IHd A) :- -% term->gref T G, term->gref I IHd, coq.typecheck T Ty ok, args-is-instance Ty A. pred find-instance i:term, i:term, o:term. @@ -397,12 +405,12 @@ pred mk-src 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, % todo list + i:list prop, % Cond list o:prop. -% mk-src (global _ as T) M I TODO (mixin-src T M I :- TODO). % impossible +% mk-src (global _ as T) M I Cond (mixin-src T M I :- Cond). % impossible -mk-src (app [_|Args]) M I _ TODO (mixin-src T M I :- TODO) :- +mk-src (app [_|Args]) M I _ Cond (mixin-src T M I :- Cond) :- std.last Args T. % std.last Args T', @@ -412,26 +420,26 @@ mk-src (app [_|Args]) M I _ TODO (mixin-src T M I :- TODO) :- % mk-src I : A -> B % create a : A % I a : B -mk-src (prod N_ (sort _) F) M I [tt|Rest] TODO (pi A \ C A) :- !, +mk-src (prod N_ (sort _) F) M I [tt|Rest] Cond (pi A \ C A) :- !, pi a\ sigma Ia\ coq.mk-app I [a] Ia, % Ia = app[I,a] - mk-src (F a) M Ia Rest TODO (C a). + mk-src (F a) M Ia Rest Cond (C a). -mk-src (prod N_ S F) M I [ff|Rest] TODO (pi A pA \ C A pA) :- +mk-src (prod N_ S F) M I [ff|Rest] Cond (pi A pA \ C A pA) :- term->gref S SG, is-structure SG, pi a\ sigma Ia\ pi pa \ coq.mk-app I [a] Ia, - mk-src (F a) M Ia Rest [find-instance a S pa|TODO] (C a pa). + mk-src (F a) M Ia Rest [find-instance a S pa|Cond] (C a pa). pred mk-src-map i:prop, o:prop. -mk-src-map (has-mixin-instance _ M IHd L) C :- +mk-src-map (has-mixin-instance _ M IHd L) C :- std.do![ T = global IHd, /*coq.env.typeof IHd Ty,*/ coq.typecheck T Ty ok, - std.spy(mk-src Ty M T L [] C). + std.spy!(mk-src Ty M T L [] C)]. pred term->cs-pattern i:term, o:cs-pattern. term->cs-pattern (prod _ _ _) cs-prod. From 3c7b01ad4318048bacbab880e847d0dc66ca8456 Mon Sep 17 00:00:00 2001 From: Thomas Date: Wed, 22 Mar 2023 18:05:58 +0100 Subject: [PATCH 22/37] fixing mixin-src->has-mixin-instance --- HB/common/database.elpi | 45 ++++++++++++++++++++++++++--------------- HB/common/stdpp.elpi | 6 ++++++ HB/factory.elpi | 2 +- 3 files changed, 36 insertions(+), 17 deletions(-) diff --git a/HB/common/database.elpi b/HB/common/database.elpi index 3b51e696b..e75b84117 100644 --- a/HB/common/database.elpi +++ b/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 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -374,10 +374,12 @@ pred sect-params-in-term i:list constant, i:term, o:list bool. sect-params-in-term SectionParams Ty L :- - safe-dest-app Ty _ _Args, - %factory-alias->gref GR F, factory-nparams F NP,std.split-at NP Args Params Args2, + safe-dest-app Ty (global GR) Args, + factory-alias->gref GR F, factory-nparams F NP, std.split-at NP Args Params _Args2, + TyP = app [global GR|Params], % change std.mem! for something that checks if the parameters appears in the term - std.map SectionParams (x\ o \ (param-in-term Ty x o)) L. + + 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. @@ -385,17 +387,17 @@ pred has-mixin-instance o:cs-pattern, o:mixinname, o:gref, o:list bool. % if I isn't gref ? pred mixin-src->has-mixin-instance i:list constant, i:prop, o:prop. -mixin-src->has-mixin-instance SectionParams (mixin-src (app [global GR|_] as T) M I) (has-mixin-instance (cs-gref GR) M IHd A) :- - term->gref I IHd, coq.typecheck T 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 _ _ _ as T) M I) (has-mixin-instance cs-prod M IHd BL):- - term->gref I IHd, coq.typecheck T Ty ok, sect-params-in-term SectionParams Ty BL. +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 T M I) (has-mixin-instance (cs-gref G) M IHd A) :- - % term->gref T G, term->gref I IHd, coq.typecheck T Ty ok, sect-params-in-term SectionParams Ty A. +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. -% mixin-src->has-mixin-instance SectionParams (mixin-src (sort U) M I) (has-mixin-instance (cs-sort U) M (global I) BL):- -% term->gref I IHd, coq.env.typeof IHd Ty, 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 find-instance i:term, i:term, o:term. @@ -408,11 +410,9 @@ pred mk-src i:list prop, % Cond list o:prop. -% mk-src (global _ as T) M I Cond (mixin-src T M I :- Cond). % impossible mk-src (app [_|Args]) M I _ Cond (mixin-src T M I :- Cond) :- std.last Args T. - % std.last Args T', % coq.mk-app ---- avoids ----> app[ app[ I, a ], b] % invariant: mk-src Ty _ I _ _ ---> I : Ty @@ -420,20 +420,33 @@ mk-src (app [_|Args]) M I _ Cond (mixin-src T M I :- Cond) :- % mk-src I : A -> B % create a : A % I a : B -mk-src (prod N_ (sort _) F) M I [tt|Rest] Cond (pi A \ C A) :- !, +% mk-src (prod N (sort _) F as T) M I [tt|Rest] Cond (C A) :- !, + +% sigma Ia\ +% coq.mk-app I [A] Ia, % Ia = app[I,a] +% mk-src (F A) M Ia Rest Cond (C A). + +mk-src (prod N_ (sort _) F) M I [ff|Rest] Cond (pi A \ C A) :- !, pi a\ sigma Ia\ coq.mk-app I [a] Ia, % Ia = app[I,a] mk-src (F a) M Ia Rest Cond (C a). mk-src (prod N_ S F) M I [ff|Rest] Cond (pi A pA \ C A pA) :- - term->gref S SG, is-structure SG, + term-is-gref? S SG, is-structure SG, pi a\ sigma Ia\ pi pa \ coq.mk-app I [a] Ia, mk-src (F a) M Ia Rest [find-instance a S pa|Cond] (C a pa). +mk-src (prod N_ _ F) M I [ff|Rest] Cond (pi A pA \ C A pA) :- + pi a\ + sigma Ia\ + pi pa \ + coq.mk-app I [a] Ia, + mk-src (F a) M Ia Rest Cond (C a pa). + pred mk-src-map i:prop, o:prop. mk-src-map (has-mixin-instance _ M IHd L) C :- std.do![ T = global IHd, diff --git a/HB/common/stdpp.elpi b/HB/common/stdpp.elpi index cd1ffaa4d..85366b424 100644 --- a/HB/common/stdpp.elpi +++ b/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. diff --git a/HB/factory.elpi b/HB/factory.elpi index 2b599df10..ee58687d2 100644 --- a/HB/factory.elpi +++ b/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 _) "_" :- !. From c167f78858a4f03a182203f3610b443838ab29c1 Mon Sep 17 00:00:00 2001 From: Thomas Date: Thu, 23 Mar 2023 18:14:48 +0100 Subject: [PATCH 23/37] writing the find instance function --- HB/common/database.elpi | 34 ++++++++++++++++++++++++++++------ instance.ipynb | 29 +++++++++++++++++++++++++++++ 2 files changed, 57 insertions(+), 6 deletions(-) diff --git a/HB/common/database.elpi b/HB/common/database.elpi index e75b84117..e6f5f9ad6 100644 --- a/HB/common/database.elpi +++ b/HB/common/database.elpi @@ -367,6 +367,7 @@ param-in-term (app [global (const C)|_]) C tt. 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. @@ -401,6 +402,26 @@ mixin-src->has-mixin-instance SectionParams (mixin-src (sort U) M I) (has-mixin- pred find-instance i:term, i:term, o:term. +find-instance T ST I :- std.do![ + term->gref ST S, + is-structure S, + structure-key SortProj _ S, + class-def (class (indt Class) S CMLwP), + structure-nparams S NParams, + coq.mk-n-holes NParams Holes, + std.append Holes [_] HolesST, + mk-app (global (const SortProj)) HolesST I, + coq.unify-eq T I ok, + get-constructor S KS, + coq.mk-app (global KS) {std.append Holes [T, CT]} KSHolesC, + coq.unify-eq ST KSHolesC ok, + % if the class instance is concrete, we take the parts + get-constructor (indt Class) KC, + std.length {list-w-params_list CMLwP} CMixinsN, + coq.mk-n-holes CMixinsN MIL, + coq.mk-app (global KC) {std.append Holes [T | MIL]} CBody, + coq.unify-eq CT CBody ok + ]. pred mk-src i:term, % type of the instance Ty @@ -420,18 +441,19 @@ mk-src (app [_|Args]) M I _ Cond (mixin-src T M I :- Cond) :- % mk-src I : A -> B % create a : A % I a : B -% mk-src (prod N (sort _) F as T) M I [tt|Rest] Cond (C A) :- !, - -% sigma Ia\ -% coq.mk-app I [A] Ia, % Ia = app[I,a] -% mk-src (F A) M Ia Rest Cond (C A). - mk-src (prod N_ (sort _) F) M I [ff|Rest] Cond (pi A \ C A) :- !, pi a\ sigma Ia\ coq.mk-app I [a] Ia, % Ia = app[I,a] mk-src (F a) M Ia Rest Cond (C a). +mk-src (prod N_ _ F) M I [tt|Rest] Cond (pi A pA \ C A pA) :- + pi a\ + sigma Ia\ + pi pa \ + coq.mk-app I [a] Ia, + mk-src (F a) M Ia Rest Cond (C a pa). + mk-src (prod N_ S F) M I [ff|Rest] Cond (pi A pA \ C A pA) :- term-is-gref? S SG, is-structure SG, pi a\ diff --git a/instance.ipynb b/instance.ipynb index 82aab6285..1f39606a1 100644 --- a/instance.ipynb +++ b/instance.ipynb @@ -20,6 +20,35 @@ "source": [ "functions get-canonical-instances and get canonical-structures let us interact with the coq database " ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": { + "vscode": { + "languageId": "plaintext" + } + }, + "outputs": [], + "source": [ + "1) has-mixin-instance CS-pattern mixinname inst.\n", + "2) mixin-src {{list lp:X}} {{hasmx}} {{i: eq I}} :- coq unification X eqType I (with X = sort I)\n", + "3) has-struct-instance CS-KEY class." + ] + }, + { + "attachments": {}, + "cell_type": "markdown", + "metadata": {}, + "source": [ + "To create the list of booleans we need to have the section paramaters from the instance definition passed down through the clauses, so the information is saved in the database. \n", + "\n", + "- This list of booleans is created by sect-params-in-term which given a list of section parameters SP and a term T, returns a list of boolean corresponding to whether or not a parameter in SP appears in T.\n", + "\n", + "- This information is crucial in creating the right clauses to saturate the right instances later.\n", + "\n", + "We'll also need later to add parameters from user-created section by interrogating the coq database." + ] } ], "metadata": { From 7a838090132c6c5f81100e77fea68eaf5f92f917 Mon Sep 17 00:00:00 2001 From: Thomas Date: Mon, 27 Mar 2023 18:26:24 +0200 Subject: [PATCH 24/37] reorganising declare all and working on mk-src --- HB/common/database.elpi | 26 +++++++++++++++++++++----- HB/instance.elpi | 38 +++++++++++++++++++++++++------------- tests/instance_merge.v | 21 +++++++++++++++++++++ 3 files changed, 67 insertions(+), 18 deletions(-) create mode 100644 tests/instance_merge.v diff --git a/HB/common/database.elpi b/HB/common/database.elpi index e6f5f9ad6..e2b10a31c 100644 --- a/HB/common/database.elpi +++ b/HB/common/database.elpi @@ -241,6 +241,10 @@ 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-mixin-src-c 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. @@ -431,6 +435,10 @@ pred mk-src i:list prop, % Cond list o:prop. +% mk-src (global GR) M I _ Cond (mixin-src T M I :- Cond) :- + +% coq.env.typeof GR Ty, +% . mk-src (app [_|Args]) M I _ Cond (mixin-src T M I :- Cond) :- std.last Args T. @@ -454,6 +462,7 @@ mk-src (prod N_ _ F) M I [tt|Rest] Cond (pi A pA \ C A pA) :- coq.mk-app I [a] Ia, mk-src (F a) M Ia Rest Cond (C a pa). + mk-src (prod N_ S F) M I [ff|Rest] Cond (pi A pA \ C A pA) :- term-is-gref? S SG, is-structure SG, pi a\ @@ -467,14 +476,21 @@ mk-src (prod N_ _ F) M I [ff|Rest] Cond (pi A pA \ C A pA) :- sigma Ia\ pi pa \ coq.mk-app I [a] Ia, - mk-src (F a) M Ia Rest Cond (C a pa). + mk-src (F a) M Ia Rest Cond (C a pa). + + + pred mk-src-map i:prop, o:prop. -mk-src-map (has-mixin-instance _ M IHd L) C :- std.do![ +mk-src-map (has-mixin-instance Pat M IHd L) C :- std.do![ + cs-pattern->term Pat Ty, T = global IHd, - /*coq.env.typeof IHd Ty,*/ - coq.typecheck T Ty ok, - std.spy!(mk-src Ty M T L [] C)]. + %coq.typecheck T Ty ok, + std.spy!(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. diff --git a/HB/instance.elpi b/HB/instance.elpi index 7eed6db46..ffea2b909 100644 --- a/HB/instance.elpi +++ b/HB/instance.elpi @@ -93,6 +93,19 @@ declare-const Name BodySkel TyWPSkel CSL :- std.do! [ % Each mixin used in order to fulfill a class is returned together with its name. pred declare-all i:term, i:list class, o:list (pair id constant). declare-all T [class Class Struct MLwP|Rest] [pr Name CS|L] :- + + infer_1 T Class Struct MLwP S Name STy Clauses, + + save_1 Name S STy CS, + + Clauses => declare-all T Rest L. + +declare-all T [_|Rest] L :- declare-all T Rest L. +declare-all _ [] []. + +pred infer_1 i:term, i:classname, i:gref, i:factories, o:term, o:string, o:term, o:list prop. +infer_1 T Class Struct MLwP S Name STy Clauses:- std.do![ + if (not(has-CS-instance? T Struct)) true % we build it (if-verbose (coq.say {header} "skipping already existing" @@ -108,30 +121,29 @@ declare-all T [class Class Struct MLwP|Rest] [pr Name CS|L] :- {coq.term->string T})) fail, - !, - Name is {cs-pattern->name {term->cs-pattern T}} ^ "__canonical__" ^ {gref->modname Struct 2 "_" }, if-verbose (coq.say {header} "declare canonical structure instance" Name), + get-constructor Struct KS, coq.safe-dest-app T THD _, private.optimize-class-body THD {std.length Params} KCApp KCAppNames Clauses, coq.mk-app (global KS) {std.append Params [T, KCAppNames]} S, if-verbose (coq.say {header} "structure instance for" Name "is" {coq.term->string S}), std.assert-ok! (coq.typecheck S STy) "declare-all: S illtyped", +]. + +pred save_1 i:string, i:term, i:term, i:constant. +save_1 Name S STy CS:- std.do![ log.coq.env.add-const-noimplicits Name S STy @transparent! CS, % Bug coq/coq#11155, could be a Let with-locality (log.coq.CS.declare-instance CS), % Bug coq/coq#11155, should be local - acc-clause current (local-canonical CS), - if-verbose (coq.say {header} "structure instance" Name "declared"), +]. - Clauses => declare-all T Rest L. -declare-all T [_|Rest] L :- declare-all T Rest L. -declare-all _ [] []. pred declare-factory-sort-deps i:gref. declare-factory-sort-deps GR :- std.do! [ @@ -204,14 +216,14 @@ saturate-instances :- std.do! [ coq.say "clauseshas : "ClausesHas, std.map-filter ClausesHas mk-src-map Clauses, findall-classes Classes, - std.map-filter PL hack TL, + std.map-filter PL (cs-pattern->term) TLD, + undup-terms TLD TL, coq.say "clausessrc : " Clauses TL, Clauses => std.forall TL (t\ (declare-all t Classes _)), - + ]. -pred hack i:cs-pattern, o:term. -hack (cs-gref GR) (global GR). + /* ------------------------------------------------------------------------- */ /* ----------------------------- private code ------------------------------ */ @@ -332,9 +344,9 @@ declare-canonical-instances-from-factory Factory T F SectionParams ClausesHas CS add-all-mixins T Factory ML tt Clauses MCSL, coq.say "clausesbef : " Clauses, std.map-filter Clauses (mixin-src->has-mixin-instance SectionParams) ClausesHas, - - %std.map ClausesHas has-mixin-instance->mixin-src Clauses, + coq.say "clauseshas ; sectionparams : " ClausesHas SectionParams, ClausesHas =>instance.declare-all T {findall-classes-for ML} CCSL, + coq.say "newclauses " CCSL, ] ], std.append MCSL CCSL CSL diff --git a/tests/instance_merge.v b/tests/instance_merge.v new file mode 100644 index 000000000..a47a6dce5 --- /dev/null +++ b/tests/instance_merge.v @@ -0,0 +1,21 @@ +From HB Require Import structures. + +HB.mixin Record m1 T := { default1 : T }. + +HB.mixin Record m2 T := { default2 : T }. + +HB.structure Definition s1 := { T of m1 T }. +HB.structure Definition s2 := { T of m2 T }. + +HB.instance Definition _ : m1 nat := m1.Build nat 1. +HB.instance Definition nat_m2 : m2 nat := m2.Build nat 2. + +HB.structure Definition s3 := { T of m1 T & m2 T }. + +HB.about nat. (* should have s3 *) + +(* The s3 instance on list should be synthetized automatically, *) +(* But since it's defined afterwards, it's not taken into account. *) +(* A simple recall suffices: *) +HB.instance Definition _ := nat_m2. +HB.about nat. From 5675a26aab1f72be8f8adc7b960014f152826652 Mon Sep 17 00:00:00 2001 From: Thomas Date: Tue, 28 Mar 2023 15:08:06 +0200 Subject: [PATCH 25/37] modifying how we get the first argument of mixin-src : it's pre-processed now. --- HB/common/database.elpi | 41 ++++++++++++++++++++--------------------- 1 file changed, 20 insertions(+), 21 deletions(-) diff --git a/HB/common/database.elpi b/HB/common/database.elpi index e2b10a31c..04ed3df4f 100644 --- a/HB/common/database.elpi +++ b/HB/common/database.elpi @@ -433,15 +433,12 @@ pred mk-src 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 + i:term, %the final term o:prop. -% mk-src (global GR) M I _ Cond (mixin-src T M I :- Cond) :- - -% coq.env.typeof GR Ty, -% . + -mk-src (app [_|Args]) M I _ Cond (mixin-src T M I :- Cond) :- - std.last Args T. +mk-src (app [_|_Args]) M I _ Cond FT (mixin-src FT M I :- Cond). % coq.mk-app ---- avoids ----> app[ app[ I, a ], b] % invariant: mk-src Ty _ I _ _ ---> I : Ty @@ -449,44 +446,46 @@ mk-src (app [_|Args]) M I _ Cond (mixin-src T M I :- Cond) :- % mk-src I : A -> B % create a : A % I a : B -mk-src (prod N_ (sort _) F) M I [ff|Rest] Cond (pi A \ C A) :- !, - pi a\ - sigma Ia\ - coq.mk-app I [a] Ia, % Ia = app[I,a] - mk-src (F a) M Ia Rest Cond (C a). -mk-src (prod N_ _ F) M I [tt|Rest] Cond (pi A pA \ C A pA) :- +mk-src (prod N_ _ F) M I [tt|Rest] Cond FT (pi A pA \ C A pA) :- pi a\ sigma Ia\ pi pa \ coq.mk-app I [a] Ia, - mk-src (F a) M Ia Rest Cond (C a pa). + mk-src (F a) M Ia Rest Cond FT (C a pa). -mk-src (prod N_ S F) M I [ff|Rest] Cond (pi A pA \ C A pA) :- +mk-src (prod N_ S F) M I [ff|Rest] Cond FT (pi A pA \ C A pA) :- term-is-gref? S SG, is-structure SG, pi a\ sigma Ia\ pi pa \ coq.mk-app I [a] Ia, - mk-src (F a) M Ia Rest [find-instance a S pa|Cond] (C a pa). + mk-src (F a) M Ia Rest [find-instance a S pa|Cond] FT (C a pa). -mk-src (prod N_ _ F) M I [ff|Rest] Cond (pi A pA \ C A pA) :- +mk-src (prod N_ _ F) M I [ff|Rest] Cond FT (pi A pA \ C A) :- pi a\ sigma Ia\ - pi pa \ coq.mk-app I [a] Ia, - mk-src (F a) M Ia Rest Cond (C a pa). + mk-src (F a) M Ia Rest Cond FT (C a). +pred enrich-type i:cs-pattern, o:term . +enrich-type C ET :- + cs-pattern->term C GH, + coq.typecheck GH TH ok, + coq.count-prods TH N, + if (N = 0) (ET is TH) (coq.mk-app TH {coq.mk-n-holes N} ET). pred mk-src-map i:prop, o:prop. mk-src-map (has-mixin-instance Pat M IHd L) C :- std.do![ - cs-pattern->term Pat Ty, + enrich-type Pat ET, T = global IHd, - %coq.typecheck T Ty ok, - std.spy!(mk-src Ty M T L [] C)]. + coq.typecheck T Ty ok, + std.spy!(mk-src Ty M T L [] ET C), + ]. + pred cs-pattern->term i:cs-pattern, o:term. cs-pattern->term (cs-gref GR) (global GR). From 3c04b9fa92911f7518a4fbb17c77f4e6d6a083d2 Mon Sep 17 00:00:00 2001 From: Thomas Date: Tue, 28 Mar 2023 18:27:18 +0200 Subject: [PATCH 26/37] using the right types to declare classes --- HB/common/database.elpi | 15 ++++----------- HB/instance.elpi | 8 ++++---- 2 files changed, 8 insertions(+), 15 deletions(-) diff --git a/HB/common/database.elpi b/HB/common/database.elpi index 04ed3df4f..fa1028b97 100644 --- a/HB/common/database.elpi +++ b/HB/common/database.elpi @@ -20,6 +20,10 @@ 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 T _ _) T. +mixin-src-w-cond_type (pi _ \ mixin-src T _ _ :- _Cond) T. + pred mixin-src_ty i:prop, o:term. mixin-src_ty (mixin-src T _ _ ) Ty :-coq.typecheck T Ty ok. @@ -240,10 +244,6 @@ findall-type-src 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-mixin-src-c 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 :- @@ -359,13 +359,6 @@ 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 arg-is-instance i:term, i:term, i:term, o:bool. - -% arg-is-instance (app [_] as T) I A tt :- -% extract-conclusion-params T I PL, std.mem! PL A. - -% arg-is-instance _ _ _ ff. - pred param-in-term i:term, i:constant, o:bool. param-in-term (app [global (const C)|_]) C tt. param-in-term (app [_|Args]) C B :- param-in-term (app Args) C B. diff --git a/HB/instance.elpi b/HB/instance.elpi index ffea2b909..2039fe495 100644 --- a/HB/instance.elpi +++ b/HB/instance.elpi @@ -85,6 +85,7 @@ declare-const Name BodySkel TyWPSkel CSL :- std.do! [ ]. + % [declare-all T CL MCSTL] given a type T and a list of class definition % CL in topological order (from least dep to most) looks for classes % for which all the dependencies (mixins) were postulated so far and skips the @@ -211,14 +212,13 @@ mk-factory-sort-factory AliasGR CSL :- std.do! [ % create instances for all possible combinations of (simple) types and structure compatible pred saturate-instances. saturate-instances :- std.do! [ - findall-type-src PL, findall-has-mixin-instance ClausesHas, coq.say "clauseshas : "ClausesHas, - std.map-filter ClausesHas mk-src-map Clauses, - findall-classes Classes, - std.map-filter PL (cs-pattern->term) TLD, + std.map ClausesHas mk-src-map Clauses, + std.map-filter Clauses mixin-src-w-cond_type TLD, undup-terms TLD TL, coq.say "clausessrc : " Clauses TL, + findall-classes Classes, Clauses => std.forall TL (t\ (declare-all t Classes _)), ]. From 9621cad0b95172faffe4198dc44c827a619effbe Mon Sep 17 00:00:00 2001 From: Thomas Date: Wed, 29 Mar 2023 09:40:27 +0200 Subject: [PATCH 27/37] fixing the list of type upon which we call declare-all --- HB/common/database.elpi | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/HB/common/database.elpi b/HB/common/database.elpi index fa1028b97..37d8fadd1 100644 --- a/HB/common/database.elpi +++ b/HB/common/database.elpi @@ -20,9 +20,12 @@ has-mixin-instance_cspat (has-mixin-instance P _ _ _) P. pred mixin-src_type i:prop, o:term. mixin-src_type (mixin-src T _ _ ) T. +%TODO rewrite this pred mixin-src-w-cond_type i:prop, o:term. -mixin-src-w-cond_type (mixin-src T _ _) T. -mixin-src-w-cond_type (pi _ \ mixin-src T _ _ :- _Cond) T. +mixin-src-w-cond_type (mixin-src T _ _ :- _) T. +mixin-src-w-cond_type (pi _ \ mixin-src T _ _ :- _) T. +mixin-src-w-cond_type (pi _ \ pi _ \ mixin-src T _ _ :- _) T. + pred mixin-src_ty i:prop, o:term. mixin-src_ty (mixin-src T _ _ ) Ty :-coq.typecheck T Ty ok. @@ -468,7 +471,7 @@ enrich-type C ET :- cs-pattern->term C GH, coq.typecheck GH TH ok, coq.count-prods TH N, - if (N = 0) (ET is TH) (coq.mk-app TH {coq.mk-n-holes N} ET). + if (N = 0) (ET is GH) (coq.mk-app GH {coq.mk-n-holes N} ET). pred mk-src-map i:prop, o:prop. From fdb2f58f58ff36b2b7b8e92f22c86f34077f8068 Mon Sep 17 00:00:00 2001 From: Thomas Date: Wed, 29 Mar 2023 17:46:58 +0200 Subject: [PATCH 28/37] starting to rewrite mk-src --- HB/common/database.elpi | 113 +++++++++++++++++++++++----------------- 1 file changed, 65 insertions(+), 48 deletions(-) diff --git a/HB/common/database.elpi b/HB/common/database.elpi index 37d8fadd1..f2417f08f 100644 --- a/HB/common/database.elpi +++ b/HB/common/database.elpi @@ -20,12 +20,9 @@ has-mixin-instance_cspat (has-mixin-instance P _ _ _) P. pred mixin-src_type i:prop, o:term. mixin-src_type (mixin-src T _ _ ) T. -%TODO rewrite this pred mixin-src-w-cond_type i:prop, o:term. mixin-src-w-cond_type (mixin-src T _ _ :- _) T. -mixin-src-w-cond_type (pi _ \ mixin-src T _ _ :- _) T. -mixin-src-w-cond_type (pi _ \ pi _ \ mixin-src 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. @@ -402,25 +399,9 @@ mixin-src->has-mixin-instance SectionParams (mixin-src (sort U) M I) (has-mixin- pred find-instance i:term, i:term, o:term. -find-instance T ST I :- std.do![ - term->gref ST S, - is-structure S, - structure-key SortProj _ S, - class-def (class (indt Class) S CMLwP), - structure-nparams S NParams, - coq.mk-n-holes NParams Holes, - std.append Holes [_] HolesST, - mk-app (global (const SortProj)) HolesST I, - coq.unify-eq T I ok, - get-constructor S KS, - coq.mk-app (global KS) {std.append Holes [T, CT]} KSHolesC, - coq.unify-eq ST KSHolesC ok, - % if the class instance is concrete, we take the parts - get-constructor (indt Class) KC, - std.length {list-w-params_list CMLwP} CMixinsN, - coq.mk-n-holes CMixinsN MIL, - coq.mk-app (global KC) {std.append Holes [T | MIL]} CBody, - coq.unify-eq CT CBody ok +find-instance T St I :- std.do![ + mk-app St [T] ST, + coq.unify-eq ST I ok, ]. pred mk-src @@ -429,12 +410,35 @@ pred mk-src 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 - i:term, %the final term o:prop. - -mk-src (app [_|_Args]) M I _ Cond FT (mixin-src FT M I :- Cond). + +pred last-app i:term, o:term. + +last-app (app[_|[(app Args)]]) T :- last-app (app Args) T. +last-app (app[G|_]) G. + +% pi c0 \ +% pi c1 \ +% mixin-src (app [global (indt «list»), c1]) (indt «m2.axioms_») +% (app [global (const «list_m2»), c0]) :- +% [find-instance c1 (global (indt «s2.type»)) c0]] +% find instance should expand into : +% coq.unify_eq (app s2.sort c0) c1 + +mk-src (app [global (const _)|Args]) M I _ Cond C :- +mk-src (app Args) M I [] Cond C. + + +mk-src (app [global G|_] as T) M I _ _Cond (mixin-src T' M Ia :- C ) :- + is-structure G, + pi a pa \ + last-app T L, + coq.mk-app I [a] Ia, + coq.mk-app (global G) [pa] T', + C is (find-instance a L pa). + % coq.mk-app ---- avoids ----> app[ app[ I, a ], b] % invariant: mk-src Ty _ I _ _ ---> I : Ty @@ -443,27 +447,27 @@ mk-src (app [_|_Args]) M I _ Cond FT (mixin-src FT M I :- Cond). % create a : A % I a : B -mk-src (prod N_ _ F) M I [tt|Rest] Cond FT (pi A pA \ C A pA) :- - pi a\ - sigma Ia\ - pi pa \ - coq.mk-app I [a] Ia, - mk-src (F a) M Ia Rest Cond FT (C a pa). +% mk-src (prod N_ _ F) M I [_tt|Rest] Cond (pi A pA \ C A pA) :- +% pi a\ +% sigma Ia\ +% pi pa \ +% coq.mk-app I [a] Ia, +% mk-src (F a) M Ia Rest Cond (C a pa). -mk-src (prod N_ S F) M I [ff|Rest] Cond FT (pi A pA \ C A pA) :- - term-is-gref? S SG, is-structure SG, - pi a\ - sigma Ia\ - pi pa \ - coq.mk-app I [a] Ia, - mk-src (F a) M Ia Rest [find-instance a S pa|Cond] FT (C a pa). +% mk-src (prod N_ S F) M I [ff|Rest] Cond (pi A pA \ C A pA) :- +% term-is-gref? S SG, is-structure SG, +% pi a\ +% sigma Ia\ +% pi pa \ +% coq.mk-app I [a] Ia, +% mk-src (F a) M Ia Rest [find-instance a S pa|Cond] (C a pa). -mk-src (prod N_ _ F) M I [ff|Rest] Cond FT (pi A pA \ C A) :- - pi a\ - sigma Ia\ - coq.mk-app I [a] Ia, - mk-src (F a) M Ia Rest Cond FT (C a). +% mk-src (prod N_ _ F) M I [ff|Rest] Cond (pi A pA \ C A) :- +% pi a\ +% sigma Ia\ +% coq.mk-app I [a] Ia, +% mk-src (F a) M Ia Rest Cond (C a). pred enrich-type i:cs-pattern, o:term . @@ -475,13 +479,26 @@ enrich-type C ET :- pred mk-src-map i:prop, o:prop. -mk-src-map (has-mixin-instance Pat M IHd L) C :- std.do![ - enrich-type Pat ET, +mk-src-map (has-mixin-instance _ M IHd L) C :- std.do![ T = global IHd, coq.typecheck T Ty ok, - std.spy!(mk-src Ty M T L [] ET C), + std.spy!(mk-src Ty M T L [] C), ]. - + +% pi c0 \ +% pi c1 \ +% mixin-src (app [global (indt «list»), c1]) (indt «m2.axioms_») +% (app [global (const «list_m2»), c0]) :- +% [find-instance c1 (global (indt «s2.type»)) c0]] +% find instance should expand into : +% coq.unify_eq (app s2.sort c0) c1 + +% list_m2 +% : forall X : s2.type, m2.phant_axioms (list (s2.sort X)) + +% coq.typecheck (app + Y) ...., +% coq.typecheck Y TY _ +% après ces deux commandes TY est instanciée à nat pred cs-pattern->term i:cs-pattern, o:term. cs-pattern->term (cs-gref GR) (global GR). From 3532146c20b4adef3b5cba6e79c29f91caf99a34 Mon Sep 17 00:00:00 2001 From: Thomas Date: Thu, 30 Mar 2023 19:00:12 +0200 Subject: [PATCH 29/37] fixing mk-src, still need to check find-instance --- HB/common/database.elpi | 67 ++++++++++++----------------------------- HB/common/utils.elpi | 5 ++- 2 files changed, 24 insertions(+), 48 deletions(-) diff --git a/HB/common/database.elpi b/HB/common/database.elpi index f2417f08f..016727bf1 100644 --- a/HB/common/database.elpi +++ b/HB/common/database.elpi @@ -400,10 +400,12 @@ mixin-src->has-mixin-instance SectionParams (mixin-src (sort U) M I) (has-mixin- pred find-instance i:term, i:term, o:term. find-instance T St I :- std.do![ - mk-app St [T] ST, - coq.unify-eq ST I ok, + coq.typecheck St Ty ok, + mk-app Ty [I] ST, + coq.unify-eq ST T ok, ]. + pred mk-src i:term, % type of the instance Ty i:mixinname, % name of mixin @@ -412,13 +414,6 @@ pred mk-src i:list prop, % Cond list o:prop. - - -pred last-app i:term, o:term. - -last-app (app[_|[(app Args)]]) T :- last-app (app Args) T. -last-app (app[G|_]) G. - % pi c0 \ % pi c1 \ % mixin-src (app [global (indt «list»), c1]) (indt «m2.axioms_») @@ -427,48 +422,26 @@ last-app (app[G|_]) G. % find instance should expand into : % coq.unify_eq (app s2.sort c0) c1 -mk-src (app [global (const _)|Args]) M I _ Cond C :- -mk-src (app Args) M I [] Cond C. -mk-src (app [global G|_] as T) M I _ _Cond (mixin-src T' M Ia :- C ) :- - is-structure G, - pi a pa \ - last-app T L, - coq.mk-app I [a] Ia, - coq.mk-app (global G) [pa] T', - C is (find-instance a L pa). - +mk-src (app [_|Args]) M (app [GI|_]) _ [] (pi A pA \ C A pA) :- + std.last Args (app [GR|Args2]), + std.last Args2 (app [GR2|_]), + coq.typecheck GR2 P ok, + prod-structure P S, + pi a pa\ + sigma Ia\ + coq.mk-app GI [a] Ia, + mk-src (app[GR|[pa]]) M Ia [] [(find-instance pa S a)] (C a pa). -% coq.mk-app ---- avoids ----> app[ app[ I, a ], b] -% invariant: mk-src Ty _ I _ _ ---> I : Ty - -% mk-src I : A -> B -% create a : A -% I a : B - -% mk-src (prod N_ _ F) M I [_tt|Rest] Cond (pi A pA \ C A pA) :- -% pi a\ -% sigma Ia\ -% pi pa \ -% coq.mk-app I [a] Ia, -% mk-src (F a) M Ia Rest Cond (C a pa). - - -% mk-src (prod N_ S F) M I [ff|Rest] Cond (pi A pA \ C A pA) :- -% term-is-gref? S SG, is-structure SG, -% pi a\ -% sigma Ia\ -% pi pa \ -% coq.mk-app I [a] Ia, -% mk-src (F a) M Ia Rest [find-instance a S pa|Cond] (C a pa). + +mk-src (app [_|_] as T) M I _ Cond (mixin-src T M I :- Cond). -% mk-src (prod N_ _ F) M I [ff|Rest] Cond (pi A pA \ 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 [ff|Rest] Cond C :- + sigma a Ia \ + coq.mk-app I [a] Ia, + mk-src (F _) M Ia Rest Cond C. pred enrich-type i:cs-pattern, o:term . enrich-type C ET :- @@ -481,7 +454,7 @@ enrich-type C ET :- pred mk-src-map i:prop, o:prop. mk-src-map (has-mixin-instance _ M IHd L) C :- std.do![ T = global IHd, - coq.typecheck T Ty ok, + coq.env.typeof IHd Ty, std.spy!(mk-src Ty M T L [] C), ]. diff --git a/HB/common/utils.elpi b/HB/common/utils.elpi index 000826a2a..de3993917 100644 --- a/HB/common/utils.elpi +++ b/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. \ No newline at end of file +prod-last-gref X GR :- coq.term->gref X GR. + +pred prod-structure i:term, o:term. +prod-structure (prod _ S _) S. \ No newline at end of file From 06268e3f34d9c6fe4cac20c4a79543ddfbee72ca Mon Sep 17 00:00:00 2001 From: Thomas Date: Fri, 31 Mar 2023 11:50:51 +0200 Subject: [PATCH 30/37] fixing clause generation --- HB/common/database.elpi | 73 +++++++++++++++++++++++++++-------------- HB/instance.elpi | 35 ++++++++++++++++++-- tests/instance_merge.v | 7 ++-- 3 files changed, 83 insertions(+), 32 deletions(-) diff --git a/HB/common/database.elpi b/HB/common/database.elpi index 016727bf1..1c078110a 100644 --- a/HB/common/database.elpi +++ b/HB/common/database.elpi @@ -21,7 +21,8 @@ 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 T _ _ :- _) T. +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. @@ -385,6 +386,9 @@ pred has-mixin-instance o:cs-pattern, o:mixinname, o:gref, o:list bool. % if I isn't gref ? 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. @@ -399,11 +403,11 @@ mixin-src->has-mixin-instance SectionParams (mixin-src (sort U) M I) (has-mixin- pred find-instance i:term, i:term, o:term. -find-instance T St I :- std.do![ - coq.typecheck St Ty ok, - mk-app Ty [I] ST, - coq.unify-eq ST T ok, - ]. +find-instance T Ty I :- + %coq.typecheck St Ty ok, + mk-app Ty [I] TYI, + coq.unify-eq TYI T ok + . pred mk-src @@ -424,31 +428,50 @@ pred mk-src -mk-src (app [_|Args]) M (app [GI|_]) _ [] (pi A pA \ C A pA) :- - std.last Args (app [GR|Args2]), - std.last Args2 (app [GR2|_]), - coq.typecheck GR2 P ok, - prod-structure P S, - pi a pa\ - sigma Ia\ - coq.mk-app GI [a] Ia, - mk-src (app[GR|[pa]]) M Ia [] [(find-instance pa S a)] (C a pa). +mk-src (global _GR as T) M I [] Cond (mixin-src T M I :- Cond). - -mk-src (app [_|_] as T) M I _ Cond (mixin-src T M I :- Cond). -mk-src (prod N_ _ F) M I [ff|Rest] Cond C :- +% mk-src (app [_|Args]) M (app [GI|_]) _ [] (pi A pA \ C A pA) :- +% std.last Args (app [GR|Args2]), +% std.last Args2 (app [GR2|_]), +% coq.typecheck GR2 P ok, +% prod-structure P S, +% pi a pa\ +% sigma Ia\ +% coq.mk-app GI [a] Ia, +% mk-src (app[GR|[pa]]) M Ia [] [(find-instance pa S a)] (C a pa). + +% +% % + + % pi a pa \ mixin-src T M Ia :- [(C a pa )|Cond] +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). + + +% mk-src (app [_|_] as T) M I _ Cond (mixin-src T M I :- Cond). + +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. - sigma a Ia \ +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 _) M Ia Rest Cond C. + mk-src (F a) M Ia Rest Cond (C a). -pred enrich-type i:cs-pattern, o:term . -enrich-type C ET :- - cs-pattern->term C GH, - coq.typecheck GH TH ok, +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 is GH) (coq.mk-app GH {coq.mk-n-holes N} ET). + if (N = 0) (ET is T) (coq.mk-app T {coq.mk-n-holes N} ET). pred mk-src-map i:prop, o:prop. diff --git a/HB/instance.elpi b/HB/instance.elpi index 2039fe495..8adf1a6b8 100644 --- a/HB/instance.elpi +++ b/HB/instance.elpi @@ -86,6 +86,28 @@ declare-const Name BodySkel TyWPSkel CSL :- std.do! [ ]. + +pred declare-all2 i:term, i:list class, o:list (pair id constant). +declare-all2 T [class Class Struct MLwP|Rest] [pr Name CS|L] :- + + enrich-type T Ty, + coq.say "Ty: " Ty, + coq.say "Class: " Class, + infer_1 Ty Class Struct MLwP S Name STy Clauses, + coq.say "Ty S : " Ty S, + % infer1 nous donne un term S = (app + Y) + % il faut fermer les trous de S + + % on doit générer un term coq : S' = (fun y => app + y) + + + save_1 Name S STy CS, + + Clauses => declare-all2 T Rest L. + +declare-all2 T [_|Rest] L :- declare-all2 T Rest L. +declare-all2 _ [] []. + % [declare-all T CL MCSTL] given a type T and a list of class definition % CL in topological order (from least dep to most) looks for classes % for which all the dependencies (mixins) were postulated so far and skips the @@ -95,8 +117,15 @@ declare-const Name BodySkel TyWPSkel CSL :- std.do! [ pred declare-all i:term, i:list class, o:list (pair id constant). declare-all T [class Class Struct MLwP|Rest] [pr Name CS|L] :- + % enrich_type T + infer_1 T Class Struct MLwP S Name STy Clauses, + % infer1 nous donne un term S = (app + Y) + % il faut fermer les trous de S + + % on doit générer un term coq : S' = (fun y => app + y) + save_1 Name S STy CS, Clauses => declare-all T Rest L. @@ -133,7 +162,7 @@ infer_1 T Class Struct MLwP S Name STy Clauses:- std.do![ private.optimize-class-body THD {std.length Params} KCApp KCAppNames Clauses, coq.mk-app (global KS) {std.append Params [T, KCAppNames]} S, if-verbose (coq.say {header} "structure instance for" Name "is" {coq.term->string S}), - std.assert-ok! (coq.typecheck S STy) "declare-all: S illtyped", + std.assert-ok! (coq.typecheck S STy) "infer1: S illtyped", ]. pred save_1 i:string, i:term, i:term, i:constant. @@ -219,8 +248,8 @@ saturate-instances :- std.do! [ undup-terms TLD TL, coq.say "clausessrc : " Clauses TL, findall-classes Classes, - Clauses => std.forall TL (t\ (declare-all t Classes _)), - + Clauses => std.forall TL (t\ (declare-all2 t Classes _)), + %Clauses => std.forall TL (t\ (infer_1 t Classes _)), ]. diff --git a/tests/instance_merge.v b/tests/instance_merge.v index a47a6dce5..9745a0ad1 100644 --- a/tests/instance_merge.v +++ b/tests/instance_merge.v @@ -12,10 +12,9 @@ HB.instance Definition nat_m2 : m2 nat := m2.Build nat 2. HB.structure Definition s3 := { T of m1 T & m2 T }. -HB.about nat. (* should have s3 *) - +Check nat:s3.type. (* The s3 instance on list should be synthetized automatically, *) (* But since it's defined afterwards, it's not taken into account. *) (* A simple recall suffices: *) -HB.instance Definition _ := nat_m2. -HB.about nat. +(* HB.instance Definition _ := nat_m2. +HB.about nat. *) From cc36c74c142d97069fa1a86ef27a8dbc6952af1c Mon Sep 17 00:00:00 2001 From: Thomas Date: Fri, 31 Mar 2023 18:46:18 +0200 Subject: [PATCH 31/37] saturating instance works ! --- HB/common/database.elpi | 67 ++++++++++------------------------------- HB/instance.elpi | 46 +++++++++++++++++++++++----- 2 files changed, 54 insertions(+), 59 deletions(-) diff --git a/HB/common/database.elpi b/HB/common/database.elpi index 1c078110a..cad3ca188 100644 --- a/HB/common/database.elpi +++ b/HB/common/database.elpi @@ -382,8 +382,7 @@ sect-params-in-term SectionParams Ty L :- pred has-mixin-instance o:cs-pattern, o:mixinname, o:gref, o:list bool. -% change order of cases -% if I isn't gref ? + 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) :- @@ -398,17 +397,14 @@ mixin-src->has-mixin-instance SectionParams (mixin-src (prod _ _ _ ) M I) (has-m 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. -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 find-instance i:term, i:term, o:term. -find-instance T Ty I :- - %coq.typecheck St Ty ok, - mk-app Ty [I] TYI, - coq.unify-eq TYI T ok - . +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). pred mk-src i:term, % type of the instance Ty @@ -418,44 +414,6 @@ pred mk-src i:list prop, % Cond list o:prop. -% pi c0 \ -% pi c1 \ -% mixin-src (app [global (indt «list»), c1]) (indt «m2.axioms_») -% (app [global (const «list_m2»), c0]) :- -% [find-instance c1 (global (indt «s2.type»)) c0]] -% find instance should expand into : -% coq.unify_eq (app s2.sort c0) c1 - - - -mk-src (global _GR as T) M I [] Cond (mixin-src T M I :- Cond). - - -% mk-src (app [_|Args]) M (app [GI|_]) _ [] (pi A pA \ C A pA) :- -% std.last Args (app [GR|Args2]), -% std.last Args2 (app [GR2|_]), -% coq.typecheck GR2 P ok, -% prod-structure P S, -% pi a pa\ -% sigma Ia\ -% coq.mk-app GI [a] Ia, -% mk-src (app[GR|[pa]]) M Ia [] [(find-instance pa S a)] (C a pa). - -% -% % - - % pi a pa \ mixin-src T M Ia :- [(C a pa )|Cond] -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). - - -% mk-src (app [_|_] as T) M I _ Cond (mixin-src T M I :- Cond). - mk-src (app [_|Args]) M I [] Cond C :- std.last Args Last, safe-dest-app Last Hd ArgsLast, @@ -467,13 +425,20 @@ mk-src (prod N_ _ F) M I [ff|Rest] Cond (pi a \ C a) :- coq.mk-app I [a] Ia, mk-src (F a) M Ia Rest Cond (C a). +% TODO Instance Param ? +mk-src (prod N_ _ F) M I [tt|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). + 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 is T) (coq.mk-app T {coq.mk-n-holes N} ET). - +% 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 L) C :- std.do![ T = global IHd, diff --git a/HB/instance.elpi b/HB/instance.elpi index 8adf1a6b8..e4d59a58b 100644 --- a/HB/instance.elpi +++ b/HB/instance.elpi @@ -85,23 +85,53 @@ declare-const Name BodySkel TyWPSkel CSL :- std.do! [ ]. +% 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:term, o:term. +bind M T T1 :- M > 0, + T1 = {{ fun x => lp:(B x) }}, % we build a Coq "fun .. => " + N is M - 1, + pi x\ % we allocate the fresh symbol for (abs M) + (copy (abs M) x :- !) => % we schedule the replacement (abs M) -> x + bind N T (B x). +bind 0 T T1 :- copy T T1. % we perform all the replacements + +% TODO remove see constraints at the end +% for a term with M holes, returns a term with M variables to fill these holes +pred close-hole-term i:term, o:term. +close-hole-term T1 T3 :- std.do! [ + (pi T N M \ fold-map T N (abs M) M :- var T, not (seen T _), !, M is N + 1, see T M) => + (pi T N M \ fold-map T N (abs M) N :- var T, seen T M, !) => + fold-map T1 0 T2 M, + bind M T2 T3, +]. + +pred seen i:term, o:int. +seen X Y :- declare_constraint (seen X Y) [X]. + +pred see i:term, o:int. +see X Y :- declare_constraint (see X Y) [X]. + +constraint seen see { + rule (see (uvar X _) N) \ (seen (uvar X _) M) <=> (M = N). + rule \ (seen (uvar X _) _) <=> false. +} pred declare-all2 i:term, i:list class, o:list (pair id constant). declare-all2 T [class Class Struct MLwP|Rest] [pr Name CS|L] :- enrich-type T Ty, - coq.say "Ty: " Ty, - coq.say "Class: " Class, - infer_1 Ty Class Struct MLwP S Name STy Clauses, - coq.say "Ty S : " Ty S, + infer_1 Ty Class Struct MLwP S Name _STy Clauses, % infer1 nous donne un term S = (app + Y) % il faut fermer les trous de S - % on doit générer un term coq : S' = (fun y => app + y) - - - save_1 Name S STy CS, + close-hole-term S SC, + coq.say "SC : " SC, + std.assert-ok! (coq.typecheck SC SCTy) "badly closed", + save_1 Name SC SCTy CS, Clauses => declare-all2 T Rest L. From 3febe7f8e7e8def53710b248c9b1130f9176129a Mon Sep 17 00:00:00 2001 From: Thomas Date: Wed, 5 Apr 2023 17:54:56 +0200 Subject: [PATCH 32/37] cleaning up code and adding comments and a unit test --- HB/common/database.elpi | 45 ++++++++++++++--------------------------- _CoqProject.test-suite | 3 +++ tests/enrich_type.v | 21 +++++++++++++++++++ tests/instance_merge.v | 2 +- 4 files changed, 40 insertions(+), 31 deletions(-) create mode 100644 tests/enrich_type.v diff --git a/HB/common/database.elpi b/HB/common/database.elpi index cad3ca188..61953d8e1 100644 --- a/HB/common/database.elpi +++ b/HB/common/database.elpi @@ -346,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, @@ -361,24 +361,23 @@ 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 C)|_]) C tt. +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 :- + coq.say "term T " T, -sect-params-in-term SectionParams Ty L :- - - safe-dest-app Ty (global GR) Args, + 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], - % change std.mem! for something that checks if the parameters appears in the term - - std.map SectionParams (x\ o \ (param-in-term TyP x o)) L. + std.map SectionParams (x\ o \ (std.spy!(param-in-term TyP x o))) L. pred has-mixin-instance o:cs-pattern, o:mixinname, o:gref, o:list bool. @@ -406,6 +405,8 @@ mk-src-aux [A|Rest] T M I Cond ( pi a \ C a) :- 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 @@ -426,19 +427,18 @@ mk-src (prod N_ _ F) M I [ff|Rest] Cond (pi a \ C a) :- mk-src (F a) M Ia Rest Cond (C a). % TODO Instance Param ? -mk-src (prod N_ _ F) M I [tt|Rest] Cond (pi a \ C a) :- +mk-src (prod N_ _ F) M I [tt|Rest] Cond C :- pi a\ - sigma Ia \ - coq.mk-app I [a] Ia, - mk-src (F a) M Ia Rest Cond (C a). + mk-src (F a) M I Rest Cond C. +% 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 is T) (coq.mk-app T {coq.mk-n-holes N} ET). + if (N = 0) (ET = T) (coq.mk-app T {coq.mk-n-holes N} ET). -% a wrapper for mk-src so it can be called by a map on a list of clauses has-mixin-instance +% 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, @@ -446,21 +446,6 @@ mk-src-map (has-mixin-instance _ M IHd L) C :- std.do![ std.spy!(mk-src Ty M T L [] C), ]. -% pi c0 \ -% pi c1 \ -% mixin-src (app [global (indt «list»), c1]) (indt «m2.axioms_») -% (app [global (const «list_m2»), c0]) :- -% [find-instance c1 (global (indt «s2.type»)) c0]] -% find instance should expand into : -% coq.unify_eq (app s2.sort c0) c1 - -% list_m2 -% : forall X : s2.type, m2.phant_axioms (list (s2.sort X)) - -% coq.typecheck (app + Y) ...., -% coq.typecheck Y TY _ -% après ces deux commandes TY est instanciée à nat - 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). diff --git a/_CoqProject.test-suite b/_CoqProject.test-suite index 268088bf8..f6ddf93fc 100644 --- a/_CoqProject.test-suite +++ b/_CoqProject.test-suite @@ -84,6 +84,9 @@ tests/issue284.v tests/issue287.v tests/store_types_cs.v tests/findall_cs_types.v +tests/instance_merge_with_distinct_param.v +tests/instance_merge.v +tests/enrich_type.v -R tests HB.tests -R examples HB.examples diff --git a/tests/enrich_type.v b/tests/enrich_type.v new file mode 100644 index 000000000..a39099c23 --- /dev/null +++ b/tests/enrich_type.v @@ -0,0 +1,21 @@ +From HB Require Import structures. +From elpi Require Import elpi. +From Coq Require Export Setoid. + +Elpi Query HB.structure lp:{{ + enrich-type {{nat}} X, + std.assert! (X = {{nat}}) "wrong enriched type" +}}. + +Elpi Query HB.structure lp:{{ + enrich-type {{list}} X, + std.assert! (X = app [{{list}}, Y]) "wrong enriched type". +}}. +Class Inj {A B} (R : relation A) (S : relation B) (f : A -> B) : Prop := +inj x y : S (f x) (f y) -> R x y. + +Elpi Query HB.structure lp:{{ + Y = {{Inj}}, + enrich-type Y X, + std.assert! (X = app [(global (const Inj)), A, B, R, S, F]) "wrong enriched type" +}}. diff --git a/tests/instance_merge.v b/tests/instance_merge.v index 9745a0ad1..9e48dff3d 100644 --- a/tests/instance_merge.v +++ b/tests/instance_merge.v @@ -13,7 +13,7 @@ HB.instance Definition nat_m2 : m2 nat := m2.Build nat 2. HB.structure Definition s3 := { T of m1 T & m2 T }. Check nat:s3.type. -(* The s3 instance on list should be synthetized automatically, *) +(* The s3 instance on nat should be synthetized automatically, *) (* But since it's defined afterwards, it's not taken into account. *) (* A simple recall suffices: *) (* HB.instance Definition _ := nat_m2. From c51263dffb2a9795739b1e1f664f06585dff75e7 Mon Sep 17 00:00:00 2001 From: Thomas Date: Fri, 7 Apr 2023 10:45:38 +0200 Subject: [PATCH 33/37] creating unit tests and cleaning up code --- .gitignore | 1 + HB/common/database.elpi | 4 +-- _CoqProject.test-suite | 2 ++ instance.ipynb | 62 ----------------------------------------- instance.md | 52 ++++++++++++++++++++++++++++++++++ tests/close_hole_term.v | 28 +++++++++++++++++++ tests/enrich_type.v | 12 ++++++-- 7 files changed, 93 insertions(+), 68 deletions(-) delete mode 100644 instance.ipynb create mode 100644 instance.md create mode 100644 tests/close_hole_term.v diff --git a/.gitignore b/.gitignore index 80a4d7d4e..b7897ed6e 100644 --- a/.gitignore +++ b/.gitignore @@ -58,3 +58,4 @@ _minted-* *.vtc *.dot +*.vscode/settings.json diff --git a/HB/common/database.elpi b/HB/common/database.elpi index 61953d8e1..40dc5a4ad 100644 --- a/HB/common/database.elpi +++ b/HB/common/database.elpi @@ -372,12 +372,10 @@ param-in-term T C B :- whd1 T T1, !, param-in-term T1 C B. % 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 :- - coq.say "term T " T, - 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 \ (std.spy!(param-in-term TyP x o))) L. + 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. diff --git a/_CoqProject.test-suite b/_CoqProject.test-suite index f6ddf93fc..f8d1be021 100644 --- a/_CoqProject.test-suite +++ b/_CoqProject.test-suite @@ -87,6 +87,8 @@ tests/findall_cs_types.v tests/instance_merge_with_distinct_param.v tests/instance_merge.v tests/enrich_type.v +tests/sect_params_in_terms.v +tests/close_hole_term.v -R tests HB.tests -R examples HB.examples diff --git a/instance.ipynb b/instance.ipynb deleted file mode 100644 index 1f39606a1..000000000 --- a/instance.ipynb +++ /dev/null @@ -1,62 +0,0 @@ -{ - "cells": [ - { - "attachments": {}, - "cell_type": "markdown", - "metadata": {}, - "source": [ - " Saturating instances on new structure declaration \n", - "\n", - "When a new structure S_new is created, the instances of factories that the new structure implements are not recorded in the database, instead they are in the coq databse. We want to get the list of factories attached to S_new and create properly the instances that implements those factories with the new structure.\n", - "\n", - "See the test file tests/instance_before_structure.v for an example\n", - "\n" - ] - }, - { - "attachments": {}, - "cell_type": "markdown", - "metadata": {}, - "source": [ - "functions get-canonical-instances and get canonical-structures let us interact with the coq database " - ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": { - "vscode": { - "languageId": "plaintext" - } - }, - "outputs": [], - "source": [ - "1) has-mixin-instance CS-pattern mixinname inst.\n", - "2) mixin-src {{list lp:X}} {{hasmx}} {{i: eq I}} :- coq unification X eqType I (with X = sort I)\n", - "3) has-struct-instance CS-KEY class." - ] - }, - { - "attachments": {}, - "cell_type": "markdown", - "metadata": {}, - "source": [ - "To create the list of booleans we need to have the section paramaters from the instance definition passed down through the clauses, so the information is saved in the database. \n", - "\n", - "- This list of booleans is created by sect-params-in-term which given a list of section parameters SP and a term T, returns a list of boolean corresponding to whether or not a parameter in SP appears in T.\n", - "\n", - "- This information is crucial in creating the right clauses to saturate the right instances later.\n", - "\n", - "We'll also need later to add parameters from user-created section by interrogating the coq database." - ] - } - ], - "metadata": { - "language_info": { - "name": "python" - }, - "orig_nbformat": 4 - }, - "nbformat": 4, - "nbformat_minor": 2 -} diff --git a/instance.md b/instance.md new file mode 100644 index 000000000..630ecd828 --- /dev/null +++ b/instance.md @@ -0,0 +1,52 @@ + Saturating instances on new structure declaration + +When a new structure S_new is created, the instances of factories that the new structure implements are not recorded in the database, instead they are in the coq databse. We want to get the list of factories attached to S_new and create properly the instances that implements those factories with the new structure. + +See the test file tests/instance_before_structure.v for an example + +functions get-canonical-instances and get canonical-structures let us interact with the coq database + +```coq +1. has-mixin-instance CS-pattern mixinname inst. +2. mixin-src {{list lp:X}} {{hasmx}} {{i: eq I}} :- coq unification X eqType I (with X = sort I) +3. has-struct-instance CS-KEY class. +``` + +To create the list of booleans we need to have the section paramaters from the instance definition passed down through the clauses, so the information is saved in the database. + +- This list of booleans is created by sect-params-in-term which given a list of section parameters SP and a term T, returns a list of boolean corresponding to whether or not a parameter in SP appears in T. + +- This information is crucial in creating the right clauses to saturate the right instances later. + +We'll also need later to add parameters from user-created section by interrogating the coq database. + + +Hierarchy builder is supposed to find links within the hierarchy of structures and instances (joins betweens elements). + + +For example, if we have an instance I1 for the structure S1 verifying a mixin M1 and similarly I2 S2 and M2, if we were to introduce a structure S3 which needs a type verifying both M1 and M2 for a type T compatible with I1 and I2, an instance for S3 and T should be generated automaically, and not only upon encountering a new instance. + +So order matters greatly as a new structure wouldn't care about all the previously defined instances. + + +Saturating instances works on instances with parameters this way : + +1. For each instance created by the user, we now put a clause in the database called has-mixin-instance, it links some concrete instance I with the mixins it satisfies +```coq +HB.instance Definition I1 : mixin1 nat ... . +``` +generates a clause in the database of the form +```coq +has-mixin-instance (cs-gref (indt «nat»)) (indt «mixin1.axioms_») (const «I1»)f +``` + +2. Later when we encounter a new structure S, we want to try to populate it with types already encountered at step 1. +To do so, we look for each possible key-types that satisfy the mixins for S in the has-mixin-instance database. + + For those, we create new clauses mixin-src on the fly from the clauses has-mixin-instance which contain the "blueprint" to have the right instance with parameters and the conditions on those parameters. + + From there if we can create an instance for S we do so by using the coq engine to unify types in the hierarchy. + + +saturate instances could be integrated into the normal program +test unitaires pour chaque fonction venant de la description complète de cette fonction \ No newline at end of file diff --git a/tests/close_hole_term.v b/tests/close_hole_term.v new file mode 100644 index 000000000..4dc58e747 --- /dev/null +++ b/tests/close_hole_term.v @@ -0,0 +1,28 @@ +From HB Require Import structures. +From elpi Require Import elpi. +From Coq Require Export Setoid. + +Elpi Query HB.instance lp:{{ + X = app [{{list}}, Y], + instance.close-hole-term X Z, + std.assert! (Z = {{fun x => lp:{{ app [{{list}}, _]}} }}) "term badly closed" +}}. + +Elpi Query HB.instance lp:{{ + instance.close-hole-term {{nat}} Z, + std.assert! (Z = {{nat}}) "term badly closed" +}}. +Class Inj {A B} (R : relation A) (S : relation B) (f : A -> B) : Prop := +inj x y : S (f x) (f y) -> R x y. + +Elpi Query HB.structure lp:{{ + Y = {{Inj}}, + enrich-type Y X, + instance.close-hole-term X Z, + std.assert! (Z = fun _n _t + (a \ fun _ _ + (b \ fun _ _ + (c \ fun _ _ + (d \ fun _ _ + (e \ app [(global (const(Inj))),e,d,c,b,a] ))))) ) "term badly closed". +}}. \ No newline at end of file diff --git a/tests/enrich_type.v b/tests/enrich_type.v index a39099c23..c7ee7bd16 100644 --- a/tests/enrich_type.v +++ b/tests/enrich_type.v @@ -9,13 +9,19 @@ Elpi Query HB.structure lp:{{ Elpi Query HB.structure lp:{{ enrich-type {{list}} X, - std.assert! (X = app [{{list}}, Y]) "wrong enriched type". + std.assert! (X = app [{{list}}, Y]) "wrong enriched type" }}. + +Elpi Query HB.structure lp:{{ + Y = (x \ (y \ {{(prod (list lp:x) (list lp:y))}})), + enrich-type (Y _ _) X, + std.assert! (X = (app [{{prod}}, (app[{{list}},X1]), app[{{list}},C]])) "wrong enriched type" +}}. + Class Inj {A B} (R : relation A) (S : relation B) (f : A -> B) : Prop := inj x y : S (f x) (f y) -> R x y. Elpi Query HB.structure lp:{{ - Y = {{Inj}}, - enrich-type Y X, + enrich-type {{Inj}} X, std.assert! (X = app [(global (const Inj)), A, B, R, S, F]) "wrong enriched type" }}. From 6450bf4d86d9f828e3cac44032bf5f66a69bd7c6 Mon Sep 17 00:00:00 2001 From: Thomas Date: Tue, 11 Apr 2023 17:35:17 +0200 Subject: [PATCH 34/37] more tests --- .gitignore | 3 ++- instance.md | 9 +++++---- tests/sect_params_in_term.v | 23 +++++++++++++++++++++++ 3 files changed, 30 insertions(+), 5 deletions(-) create mode 100644 tests/sect_params_in_term.v diff --git a/.gitignore b/.gitignore index b7897ed6e..8789b63b6 100644 --- a/.gitignore +++ b/.gitignore @@ -58,4 +58,5 @@ _minted-* *.vtc *.dot -*.vscode/settings.json + +.vscode/settings.json diff --git a/instance.md b/instance.md index 630ecd828..20de63e32 100644 --- a/instance.md +++ b/instance.md @@ -24,9 +24,10 @@ We'll also need later to add parameters from user-created section by interrogati Hierarchy builder is supposed to find links within the hierarchy of structures and instances (joins betweens elements). -For example, if we have an instance I1 for the structure S1 verifying a mixin M1 and similarly I2 S2 and M2, if we were to introduce a structure S3 which needs a type verifying both M1 and M2 for a type T compatible with I1 and I2, an instance for S3 and T should be generated automaically, and not only upon encountering a new instance. +Let's say we have an instance I1 for the structure S1 verifying a mixin M1 and similarly I2, S2, and M2. +If we were to introduce a structure S3 which needs a type verifying both M1 and M2 for a type T compatible with I1 and I2, an instance for S3 and T should be generated automatically, and not only upon encountering a new instance. -So order matters greatly as a new structure wouldn't care about all the previously defined instances. +So order matters greatly as a new structure wouldn't know about all the previously defined instances, until a new instace is created. Saturating instances works on instances with parameters this way : @@ -37,11 +38,11 @@ HB.instance Definition I1 : mixin1 nat ... . ``` generates a clause in the database of the form ```coq -has-mixin-instance (cs-gref (indt «nat»)) (indt «mixin1.axioms_») (const «I1»)f +has-mixin-instance (cs-gref (indt «nat»)) (indt «mixin1.axioms_») (const «I1») ``` 2. Later when we encounter a new structure S, we want to try to populate it with types already encountered at step 1. -To do so, we look for each possible key-types that satisfy the mixins for S in the has-mixin-instance database. +To do so, we look for each possible key-types which satisfy the mixins for S in the has-mixin-instance database. For those, we create new clauses mixin-src on the fly from the clauses has-mixin-instance which contain the "blueprint" to have the right instance with parameters and the conditions on those parameters. diff --git a/tests/sect_params_in_term.v b/tests/sect_params_in_term.v new file mode 100644 index 000000000..f46aa26ac --- /dev/null +++ b/tests/sect_params_in_term.v @@ -0,0 +1,23 @@ +From HB Require Import structures. +From elpi Require Import elpi. + +HB.mixin Record m1 T := { default1 : T }. +HB.mixin Record m2 T := { default2 : T }. + +HB.structure Definition s1 := { T of m1 T }. +HB.instance Definition i1 (X : s1.type) : m1 (list X) := +m1.Build (list X) (cons default1 nil). + +HB.instance Definition nat_m1 : m1 nat := m1.Build nat 1. +HB.instance Definition nat_m2 : m2 nat := m2.Build nat 1. + + +Elpi Query HB.instance lp:{{ +mixin-src->has-mixin-instance [] (mixin-src {{nat}} M1 {{nat_m1}}) Y, +Y = has-mixin-instance (cs-gref N) M1 I1 [], + coq.locate "nat" N, + coq.locate "m1.phant_axioms" M1, + coq.locate "nat_m1" I1. +}}. + + From 971749f1cbf3eca61e7e15314db0d9bdd0d41107 Mon Sep 17 00:00:00 2001 From: Thomas Date: Wed, 12 Apr 2023 16:27:56 +0200 Subject: [PATCH 35/37] more tests and fixing the instance parameters case --- .gitignore | 3 +- HB/common/database.elpi | 8 ++--- _CoqProject.test-suite | 8 +++-- tests/instance_merge_with_distinct_param.v | 12 +++----- tests/{ => unit}/close_hole_term.v | 13 ++++----- tests/{ => unit}/enrich_type.v | 0 .../mixin_src_has_mixin_instance.v} | 16 +++++++--- tests/unit/mk_src_map.v | 29 +++++++++++++++++++ tests/unit/sect_params_in_term.v | 16 ++++++++++ 9 files changed, 76 insertions(+), 29 deletions(-) rename tests/{ => unit}/close_hole_term.v (56%) rename tests/{ => unit}/enrich_type.v (100%) rename tests/{sect_params_in_term.v => unit/mixin_src_has_mixin_instance.v} (59%) create mode 100644 tests/unit/mk_src_map.v create mode 100644 tests/unit/sect_params_in_term.v diff --git a/.gitignore b/.gitignore index 8789b63b6..554a47d4b 100644 --- a/.gitignore +++ b/.gitignore @@ -58,5 +58,4 @@ _minted-* *.vtc *.dot - -.vscode/settings.json +*.json diff --git a/HB/common/database.elpi b/HB/common/database.elpi index 40dc5a4ad..359305dba 100644 --- a/HB/common/database.elpi +++ b/HB/common/database.elpi @@ -403,7 +403,7 @@ mk-src-aux [A|Rest] T M I Cond ( pi a \ C a) :- 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 +% 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 @@ -424,10 +424,10 @@ mk-src (prod N_ _ F) M I [ff|Rest] Cond (pi a \ C a) :- coq.mk-app I [a] Ia, mk-src (F a) M Ia Rest Cond (C a). -% TODO Instance Param ? mk-src (prod N_ _ F) M I [tt|Rest] Cond C :- - pi a\ - mk-src (F a) M I Rest Cond C. + sigma a Ia \ + coq.mk-app I [a] Ia, + mk-src (F a) M Ia Rest Cond C. % for a type T, create as many holes as there are foralls and returns that enriched type pred enrich-type i:term, o:term . diff --git a/_CoqProject.test-suite b/_CoqProject.test-suite index f8d1be021..aed606e4f 100644 --- a/_CoqProject.test-suite +++ b/_CoqProject.test-suite @@ -86,10 +86,12 @@ tests/store_types_cs.v tests/findall_cs_types.v tests/instance_merge_with_distinct_param.v tests/instance_merge.v -tests/enrich_type.v -tests/sect_params_in_terms.v -tests/close_hole_term.v +tests/unit/enrich_type.v +tests/unit/mixin_src_has_mixin_instance.v +tests/unit/mk_src_map.v +tests/unit/close_hole_term.v +tests/unit/sect_params_in_terms.v -R tests HB.tests -R examples HB.examples diff --git a/tests/instance_merge_with_distinct_param.v b/tests/instance_merge_with_distinct_param.v index 0f4d44921..169d5f7bf 100644 --- a/tests/instance_merge_with_distinct_param.v +++ b/tests/instance_merge_with_distinct_param.v @@ -14,13 +14,9 @@ HB.instance Definition list_m2 (X : s2.type) : m2 (list X) := HB.structure Definition s3 := { T of m1 T & m2 T }. -HB.about list. (* should have s3 *) - -(* The s3 instance on list should be synthetized automatically, *) -(* this is nontrivial because the parameters are not the same *) -(* but there is a join in the hierarchy, so it can be defined. *) -(* Actually just recalling the list_m2 instance above suffices. *) -HB.instance Definition _ (X : s3.type) := list_m2 X. -HB.about list. +Fail Check list nat:s3.type. +Fail Check fun t : s1.type => (list t : s3.type). +Fail Check fun t : s2.type => (list t : s3.type). +Check fun t : s3.type => (list t : s3.type). diff --git a/tests/close_hole_term.v b/tests/unit/close_hole_term.v similarity index 56% rename from tests/close_hole_term.v rename to tests/unit/close_hole_term.v index 4dc58e747..6798a79e9 100644 --- a/tests/close_hole_term.v +++ b/tests/unit/close_hole_term.v @@ -5,24 +5,21 @@ From Coq Require Export Setoid. Elpi Query HB.instance lp:{{ X = app [{{list}}, Y], instance.close-hole-term X Z, - std.assert! (Z = {{fun x => lp:{{ app [{{list}}, _]}} }}) "term badly closed" + std.assert! (Z = {{fun x => list x}} ) "term badly closed" }}. Elpi Query HB.instance lp:{{ instance.close-hole-term {{nat}} Z, std.assert! (Z = {{nat}}) "term badly closed" }}. + + Class Inj {A B} (R : relation A) (S : relation B) (f : A -> B) : Prop := inj x y : S (f x) (f y) -> R x y. Elpi Query HB.structure lp:{{ - Y = {{Inj}}, + Y = {{Inj}}, %Inj has 5 implicit arguments enrich-type Y X, instance.close-hole-term X Z, - std.assert! (Z = fun _n _t - (a \ fun _ _ - (b \ fun _ _ - (c \ fun _ _ - (d \ fun _ _ - (e \ app [(global (const(Inj))),e,d,c,b,a] ))))) ) "term badly closed". + std.assert! (Z = {{ fun a b c d e => @Inj e d c b a}}) "term badly closed". }}. \ No newline at end of file diff --git a/tests/enrich_type.v b/tests/unit/enrich_type.v similarity index 100% rename from tests/enrich_type.v rename to tests/unit/enrich_type.v diff --git a/tests/sect_params_in_term.v b/tests/unit/mixin_src_has_mixin_instance.v similarity index 59% rename from tests/sect_params_in_term.v rename to tests/unit/mixin_src_has_mixin_instance.v index f46aa26ac..fb4d74496 100644 --- a/tests/sect_params_in_term.v +++ b/tests/unit/mixin_src_has_mixin_instance.v @@ -14,10 +14,18 @@ HB.instance Definition nat_m2 : m2 nat := m2.Build nat 1. Elpi Query HB.instance lp:{{ mixin-src->has-mixin-instance [] (mixin-src {{nat}} M1 {{nat_m1}}) Y, -Y = has-mixin-instance (cs-gref N) M1 I1 [], - coq.locate "nat" N, - coq.locate "m1.phant_axioms" M1, - coq.locate "nat_m1" I1. +Y = has-mixin-instance (cs-gref {{:gref nat}}) {{:gref m1.phant_axioms}} {{:gref nat_m1}} []. + +}}. + +Section Test. +Variable X:s1.type. + +Elpi Query HB.instance lp:{{ +coq.env.section L, +mixin-src->has-mixin-instance L (mixin-src {{list X}} M1 {{i1 X}}) Y, +Y = has-mixin-instance (cs-gref {{:gref list}}) {{:gref m1.phant_axioms}} {{:gref i1}} [ff]. + }}. diff --git a/tests/unit/mk_src_map.v b/tests/unit/mk_src_map.v new file mode 100644 index 000000000..7029be225 --- /dev/null +++ b/tests/unit/mk_src_map.v @@ -0,0 +1,29 @@ +From HB Require Import structures. + +HB.mixin Record is_foo P A := { op : P -> A -> A }. + +HB.instance Definition nat_foo P := is_foo.Build P nat (fun _ x => x). + +HB.instance Definition list_foo P := is_foo.Build P (list P) (fun _ x => x). + +HB.instance Definition list_foo' P A := is_foo.Build P (list A) (fun _ x => x). +Check list_foo'. +Check list_foo. + +Elpi Query HB.structure lp:{{ + + +mk-src-map (has-mixin-instance (cs-gref{{:gref list}}) {{:gref is_foo.axioms_}} {{:gref list_foo}} [ff]) MS, + MS = (pi a b \ + mixin-src (app [{{list}}, b]) ({{:gref is_foo.axioms_}}) (app [{{list_foo}}, a]) + :- [coq.unify-eq a b ok]), + +mk-src-map (has-mixin-instance (cs-gref{{:gref list}}) {{:gref is_foo.axioms_}} {{:gref list_foo'}} [tt, ff]) MS', +MS' = (pi a b \ + mixin-src (app [{{list}}, b]) {{:gref is_foo.axioms_}} (app [{{list_foo'}}, X, a]) + :- [coq.unify-eq a b ok]). + +}}. + +HB.structure Definition foo P := { A of is_foo P A }. +HB.about list. diff --git a/tests/unit/sect_params_in_term.v b/tests/unit/sect_params_in_term.v new file mode 100644 index 000000000..08f915203 --- /dev/null +++ b/tests/unit/sect_params_in_term.v @@ -0,0 +1,16 @@ +From HB Require Import structures. +From elpi Require Import elpi. + +HB.mixin Record is_foo P A := { op : P -> A -> A }. + + +HB.instance Definition nat_foo P := is_foo.Build P nat (fun _ x => x). +HB.instance Definition list_foo' P A:= is_foo.Build P (list A) (fun _ x => x). +HB.instance Definition list_foo P := is_foo.Build P (list P) (fun _ x => x). + +Elpi Query HB.instance lp:{{ +has-mixin-instance (cs-gref{{:gref nat}}) M1 {{:gref nat_foo}} [tt], +has-mixin-instance (cs-gref{{:gref list}}) M {{:gref list_foo}} [tt], +has-mixin-instance (cs-gref{{:gref list}}) M {{:gref list_foo'}} [tt, ff] + +}}. \ No newline at end of file From 64b5ee988650f82e594b50e9a27fb2b0d03ffc16 Mon Sep 17 00:00:00 2001 From: Thomas Date: Thu, 13 Apr 2023 16:35:23 +0200 Subject: [PATCH 36/37] fixing coqproject and fixing a bug on mk-src --- HB/common/database.elpi | 6 ++++++ _CoqProject | 5 ++++- _CoqProject.test-suite | 7 ++++--- tests/unit/mixin_src_has_mixin_instance.v | 2 +- tests/unit/mk_src_map.v | 7 +++---- 5 files changed, 18 insertions(+), 9 deletions(-) diff --git a/HB/common/database.elpi b/HB/common/database.elpi index 359305dba..09f14d70d 100644 --- a/HB/common/database.elpi +++ b/HB/common/database.elpi @@ -429,6 +429,12 @@ mk-src (prod N_ _ F) M I [tt|Rest] Cond C :- 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 :- diff --git a/_CoqProject b/_CoqProject index 86d5a53f2..057e90014 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1,4 +1,7 @@ structures.v -arg -w -arg -elpi.accumulate-syntax -arg -w -arg +elpi.typecheck --Q . HB \ No newline at end of file +-Q . HB + +-R tests HB.tests +-R examples HB.examples \ No newline at end of file diff --git a/_CoqProject.test-suite b/_CoqProject.test-suite index aed606e4f..e2b4e7a55 100644 --- a/_CoqProject.test-suite +++ b/_CoqProject.test-suite @@ -3,7 +3,7 @@ -arg -w -arg -abstract-large-number -arg -w -arg -disj-pattern-notation -arg -w -arg -notation-overridden -arg -w -arg +elpi.typecheck +-arg -w -arg +elpi.typecheck examples/readme.v examples/hulk.v @@ -83,7 +83,7 @@ tests/fun_instance.v tests/issue284.v tests/issue287.v tests/store_types_cs.v -tests/findall_cs_types.v +tests/findall_cs_type.v tests/instance_merge_with_distinct_param.v tests/instance_merge.v @@ -91,7 +91,8 @@ tests/unit/enrich_type.v tests/unit/mixin_src_has_mixin_instance.v tests/unit/mk_src_map.v tests/unit/close_hole_term.v -tests/unit/sect_params_in_terms.v +tests/unit/sect_params_in_term.v + -R tests HB.tests -R examples HB.examples diff --git a/tests/unit/mixin_src_has_mixin_instance.v b/tests/unit/mixin_src_has_mixin_instance.v index fb4d74496..bee7d2be6 100644 --- a/tests/unit/mixin_src_has_mixin_instance.v +++ b/tests/unit/mixin_src_has_mixin_instance.v @@ -27,5 +27,5 @@ mixin-src->has-mixin-instance L (mixin-src {{list X}} M1 {{i1 X}}) Y, Y = has-mixin-instance (cs-gref {{:gref list}}) {{:gref m1.phant_axioms}} {{:gref i1}} [ff]. }}. - +End Test. diff --git a/tests/unit/mk_src_map.v b/tests/unit/mk_src_map.v index 7029be225..40d1451d3 100644 --- a/tests/unit/mk_src_map.v +++ b/tests/unit/mk_src_map.v @@ -11,18 +11,17 @@ Check list_foo'. Check list_foo. Elpi Query HB.structure lp:{{ - - mk-src-map (has-mixin-instance (cs-gref{{:gref list}}) {{:gref is_foo.axioms_}} {{:gref list_foo}} [ff]) MS, MS = (pi a b \ mixin-src (app [{{list}}, b]) ({{:gref is_foo.axioms_}}) (app [{{list_foo}}, a]) - :- [coq.unify-eq a b ok]), + :- [coq.unify-eq a b ok]) +}}. +Elpi Query HB.structure lp:{{ mk-src-map (has-mixin-instance (cs-gref{{:gref list}}) {{:gref is_foo.axioms_}} {{:gref list_foo'}} [tt, ff]) MS', MS' = (pi a b \ mixin-src (app [{{list}}, b]) {{:gref is_foo.axioms_}} (app [{{list_foo'}}, X, a]) :- [coq.unify-eq a b ok]). - }}. HB.structure Definition foo P := { A of is_foo P A }. From 7fd35ef0ebbebcf8365dd94f1ebafe3766c593ba Mon Sep 17 00:00:00 2001 From: Thomas Date: Thu, 13 Apr 2023 17:37:29 +0200 Subject: [PATCH 37/37] changing prints into warnings to allow test suite to work --- HB/common/database.elpi | 2 +- HB/instance.elpi | 38 +++++++++++++++++++------------------- 2 files changed, 20 insertions(+), 20 deletions(-) diff --git a/HB/common/database.elpi b/HB/common/database.elpi index 09f14d70d..3edc1a5ce 100644 --- a/HB/common/database.elpi +++ b/HB/common/database.elpi @@ -447,7 +447,7 @@ 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, - std.spy!(mk-src Ty M T L [] C), + mk-src Ty M T L [] C, ]. pred cs-pattern->term i:cs-pattern, o:term. diff --git a/HB/instance.elpi b/HB/instance.elpi index e4d59a58b..156774603 100644 --- a/HB/instance.elpi +++ b/HB/instance.elpi @@ -91,7 +91,7 @@ type abs int -> term. % bind back abstracted subterms pred bind i:int, i:term, o:term. bind M T T1 :- M > 0, - T1 = {{ fun x => lp:(B x) }}, % we build a Coq "fun .. => " + T1 = {{ fun x => lp:(B x) }}, N is M - 1, pi x\ % we allocate the fresh symbol for (abs M) (copy (abs M) x :- !) => % we schedule the replacement (abs M) -> x @@ -100,22 +100,31 @@ bind 0 T T1 :- copy T T1. % we perform all the replacements % TODO remove see constraints at the end % 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 +% pred close-hole-term i:term, o:term. close-hole-term T1 T3 :- std.do! [ (pi T N M \ fold-map T N (abs M) M :- var T, not (seen T _), !, M is N + 1, see T M) => (pi T N M \ fold-map T N (abs M) N :- var T, seen T M, !) => fold-map T1 0 T2 M, bind M T2 T3, - + % print_constraints, + % std.findall (seen _ _) C, + % std.forall C (s\ sigma T\ s = see T _, rm-evar T T), + % print_constraints, ]. + + pred seen i:term, o:int. -seen X Y :- declare_constraint (seen X Y) [X]. +% :name "hook1" +seen X Y :- declare_constraint (seen X Y) [X]. pred see i:term, o:int. see X Y :- declare_constraint (see X Y) [X]. constraint seen see { + % rule (remove X N ) \ (seen uvar X _ _) rule (see (uvar X _) N) \ (seen (uvar X _) M) <=> (M = N). rule \ (seen (uvar X _) _) <=> false. } @@ -129,7 +138,6 @@ declare-all2 T [class Class Struct MLwP|Rest] [pr Name CS|L] :- % il faut fermer les trous de S % on doit générer un term coq : S' = (fun y => app + y) close-hole-term S SC, - coq.say "SC : " SC, std.assert-ok! (coq.typecheck SC SCTy) "badly closed", save_1 Name SC SCTy CS, @@ -147,14 +155,7 @@ declare-all2 _ [] []. pred declare-all i:term, i:list class, o:list (pair id constant). declare-all T [class Class Struct MLwP|Rest] [pr Name CS|L] :- - % enrich_type T - infer_1 T Class Struct MLwP S Name STy Clauses, - % infer1 nous donne un term S = (app + Y) - % il faut fermer les trous de S - - % on doit générer un term coq : S' = (fun y => app + y) - save_1 Name S STy CS, @@ -272,14 +273,13 @@ mk-factory-sort-factory AliasGR CSL :- std.do! [ pred saturate-instances. saturate-instances :- std.do! [ findall-has-mixin-instance ClausesHas, - coq.say "clauseshas : "ClausesHas, + coq.warning "clauseshas : " "debug" ClausesHas, std.map ClausesHas mk-src-map Clauses, std.map-filter Clauses mixin-src-w-cond_type TLD, undup-terms TLD TL, - coq.say "clausessrc : " Clauses TL, + coq.warning "clausessrc : " "debug" Clauses TL, findall-classes Classes, Clauses => std.forall TL (t\ (declare-all2 t Classes _)), - %Clauses => std.forall TL (t\ (infer_1 t Classes _)), ]. @@ -383,7 +383,7 @@ declare-canonical-instances-from-factory-and-local-builders add-all-mixins T FGR NewMixins ff Clauses MCSL, ]), list-w-params_list {factory-provides Factory} ML, - Clauses => instance.declare-all T {findall-classes-for ML} CCSL, + Clauses => declare-all T {findall-classes-for ML} CCSL, std.append MCSL CCSL CSL ]. @@ -401,11 +401,11 @@ declare-canonical-instances-from-factory Factory T F SectionParams ClausesHas CS synthesis.under-local-canonical-mixins-of.do! T [ list-w-params_list {factory-provides Factory} ML, add-all-mixins T Factory ML tt Clauses MCSL, - coq.say "clausesbef : " Clauses, + coq.warning "clausesbef : " "" Clauses, std.map-filter Clauses (mixin-src->has-mixin-instance SectionParams) ClausesHas, - coq.say "clauseshas ; sectionparams : " ClausesHas SectionParams, - ClausesHas =>instance.declare-all T {findall-classes-for ML} CCSL, - coq.say "newclauses " CCSL, + coq.warning "clauseshas ; sectionparams : " "" ClausesHas SectionParams, + ClausesHas => declare-all T {findall-classes-for ML} CCSL, + coq.warning "newclauses " "" CCSL, ] ], std.append MCSL CCSL CSL