wip

Author: gares

HB/structure.elpi

@@ -180,10 +180,11 @@ declare Module BSkel Sort :- std.do! [
   log.coq.env.end-module-name ElpiOperationModName ElpiOperations,
   export.module ElpiOperationModName ElpiOperations,
 
-  % we need to filter the wrappers out of ML 
-  std.filter ML (x\ wrapper-mixin x _ _) WrapperML,
   % we need to assert locally the clauses in EX
-  EX => std.forall WrapperML private.reexport-wrapper-as-instance,
+  EX => std.forall ML private.reexport-wrapper-as-instance,
+  
+  %hack
+  hack,
 
   if-verbose (coq.say {header} "abbreviation factory-by-classname"),
 
@@ -196,6 +197,11 @@ declare Module BSkel Sort :- std.do! [
 %  NewClauses => instance.saturate-instances,
 ].
 
+pred hack.
+hack :- coq.next-synterp-action (begin-section X), coq.env.begin-section X, hack.
+hack :- coq.next-synterp-action end-section, coq.env.end-section, hack.
+hack.
+
 /* ------------------------------------------------------------------------- */
 /* ----------------------------- private code ------------------------------ */
 /* ------------------------------------------------------------------------- */
@@ -703,7 +709,7 @@ lift-to-the-subject.aux [factory-on-subject-lifter Expr _ _|_] _ _ :-
 % instance.declare-const (notably used in the API, i.e. in structures.v, 
 % HB.instance)
 pred reexport-wrapper-as-instance i:mixinname.
-reexport-wrapper-as-instance M :- std.do! [     
+reexport-wrapper-as-instance M :- wrapper-mixin M _ _, !, std.do! [     
 
     % need the body of the wrapper projection type  
      exported-op M _ C,
@@ -718,5 +724,11 @@ reexport-wrapper-as-instance M :- std.do! [
 
      get-option "wrapper" ff => instance.declare-const Str B Arity _
  ]. 
+reexport-wrapper-as-instance _ :-
+  std.assert! (coq.next-synterp-action (begin-section SectionName)) "synterp code did not open section",
+  coq.env.begin-section SectionName,
+  std.assert! (coq.next-synterp-action (end-section)) "synterp code did not close section",
+  coq.env.end-section.
+
 
 }}

Makefile.coq.local

@@ -1,5 +1,5 @@
 # Coq does not know about Elpi Accumulate File, so we declare the dependency here
-structures.vo : $(wildcard HB/*.elpi HB/common/*.elpi)
+theories/structures.vo : $(wildcard HB/*.elpi HB/common/*.elpi)
 
 clean::
 	$(SHOW)'CLEAN *.hb *.hb.old'

Makefile.test-suite.coq.local

@@ -7,7 +7,7 @@ output_for=`\
 	fi`
 
 DIFF=\
-	@if [ -z "$$COQ_ELPI_ATTRIBUTES" ]; then \
+	if [ -z "$$COQ_ELPI_ATTRIBUTES" ]; then \
 	echo OUTPUT DIFF $(1);\
 	$(COQTOP) $(COQFLAGS) $(COQLIBS) -topfile $(1) \
 	  < $(1) 2>/dev/null \

_CoqProject

@@ -1,10 +1,9 @@
-structures.v
+theories/structures.v
 theories/cat.v
 theories/encatD.v
 theories/encatI.v
 -arg -w -arg -elpi.accumulate-syntax
 -arg -w -arg +elpi.typecheck
--Q . HB
 
 -R tests HB.tests
 -R examples HB.examples

_CoqProject.test-suite

@@ -100,4 +100,4 @@ tests/tag_wrap.v
 -R tests HB.tests
 -R examples HB.examples
 
--Q . HB
+-R theories HB

tests/hnf.v.out

@@ -7,6 +7,3 @@ HB_unnamed_mixin_8 =
 Datatypes_bool__canonical__hnf_S =
 {| S.sort := bool; S.class := {| S.hnf_M_mixin := hnf_f__to__hnf_M__11 |} |}
      : S.type
-HB_unnamed_mixin_12 =
-Builders_1.HB_unnamed_factory_3 bool HB_unnamed_factory_9
-     : M.axioms_ bool