Interactive mode to complete instances in tactics mode

HB/common/utils-synterp.elpi

@@ -24,6 +24,7 @@ with-attributes P :-
     att "primitive" bool,
     att "non_forgetful_inheritance" bool,
     att "hnf" bool,
+    att "interactive" bool,
   ] Opts, !,
   Opts => (save-docstring, P).
 

HB/common/utils.elpi

@@ -117,6 +117,9 @@ gref->modname_short GR Sep IDS :-
 
 func avoid-name-collision string -> string.
 avoid-name-collision S S1 :-
+  if (var S)
+    (S = "unnamed")
+    (true),
   coq.locate-all S L,
   if (std.mem L (loc-gref GR), coq.gref->path GR P, coq.env.current-path P)
      (S1 is S ^ "__" ^ {std.any->string {new_int}})

HB/instance.elpi

@@ -34,7 +34,11 @@ declare-const Name BodySkel TyWPSkel CFL 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,
+     %FIXME : introduce a bug
+     %TODO re-allow local instances (test file local_instance.v) 
+     std.assert! (coq.next-synterp-action (begin-section SectionName)) "synterp code did not open section",
+    log.coq.env.begin-section SectionName
    ) (
     std.assert! (coq.next-synterp-action (begin-section SectionName)) "synterp code did not open section",
     log.coq.env.begin-section SectionName,
@@ -78,10 +82,11 @@ declare-const Name BodySkel TyWPSkel CFL CSL :- std.do! [
      true,
 
   % handle parameters via a section -- end
-  if (TyWP = arity _) true (
+  % FIXME 
+  % if (TyWP = arity _) true (
     if-verbose (coq.say {header} "closing instance section"),
-    log.coq.env.end-section-name SectionName
-  ),
+    log.coq.env.end-section-name SectionName,
+  % ),
 
   % we accumulate clauses now that the section is over
   acc-clauses current Clauses
@@ -295,10 +300,16 @@ declare-instance Factory T F Clauses CFL CSL :-
   !,
   declare-canonical-instances-from-factory-and-local-builders Factory
     T F TheFactory FGR Clauses CFL CSL.
-declare-instance Factory T F Clauses CFL CSL :-
+declare-instance Factory T F Clauses CFL CSL :- !,
   declare-canonical-instances-from-factory Factory T F Clauses1 CFL CSL,
   clauses-for-export {std.append CFL CSL} Clauses2,
   std.append Clauses1 Clauses2 Clauses.
+% declare-instance Factory T F Clauses CFL CSL :- !,
+%   if (get-option "program" tt)
+%       (coq.say "HB: declare-instance: program option detected") true,
+%   declare-canonical-instances-from-factory Factory T F Clauses1 CFL CSL,
+%   clauses-for-export {std.append CFL CSL} Clauses2,
+%   std.append Clauses1 Clauses2 Clauses.
 
 func clauses-for-export list (pair id constant) -> list prop.
 clauses-for-export CL ECL :-

HB/structures.v

@@ -1,3 +1,5 @@
+Set Warnings "-elpi.flex-clause".
+
 (* Support constants, to be kept in sync with shim/structures.v *)
 From Corelib Require Import ssreflect ssrfun.
 
@@ -771,6 +773,7 @@ HB.instance Definition N Params := Factory.Build Params T …
     - [#[verbose]] for a verbose output.
     - [#[hnf] to compute the head normal form of CS instances before declaring
       them
+    - [#[interactive]] to provide part of the instance in tactics mode.
 *)
 
 #[arguments(raw)] Elpi Command HB.instance.
@@ -792,23 +795,95 @@ main [const-decl Name (some BodySkel) TyWPSkel] :- !,
 main [T0, F0] :- !,
   coq.warning "HB" "HB.deprecated" "The syntax \"HB.instance Key FactoryInstance\" is deprecated, use \"HB.instance Definition\" instead",
   with-attributes (with-logging (instance.declare-existing T0 F0)).
-
+main-interp-proof [const-decl Name (some BodySkel) TyWPSkel] _ Body AllGoals (const-decl Name (some Body) TyWP) :- 
+  std.assert-ok! (coq.elaborate-arity-skeleton TyWPSkel _ TyWP) "Definition type illtyped",
+  coq.arity->term TyWP Ty,
+  std.assert-ok! (coq.elaborate-skeleton BodySkel Ty Body) "Definition illtyped",
+  coq.ltac.collect-goals Body Goal Shelved,
+  std.append Shelved Goal AllGoals. 
 }}.
+
 #[synterp] Elpi Accumulate lp:{{
 
 shorten coq.env.{ begin-section, end-section }.
 
-main [const-decl _ _ (arity _)] :- !.
-main [const-decl _ _ (parameter _ _ _ _)] :- !,
-  SectionName is "hb_instance_" ^ {std.any->string {new_int} },
-  begin-section SectionName, end-section.
-main [_, _] :- !.
+pred interactive-in-attributes i:list attribute. 
+  interactive-in-attributes [attribute "interactive" (leaf-str "") | _].
+  interactive-in-attributes [_ | Atts] :- interactive-in-attributes Atts.
 
-main _ :- coq.error "Usage: HB.instance Definition <Name> := <Builder> T ...".
+main _ :-
+  attributes A,
+  if (interactive-in-attributes A)
+    (true)
+    (SectionName is "hb_instance_" ^ {std.any->string {new_int} },
+     begin-section SectionName, end-section).
 }}.
+
 Elpi Typecheck.
+#[proof(begin_if="interactive")]
 Elpi Export HB.instance.
 
+
+
+#[arguments(raw)] Elpi Command HB.endinstance.
+Elpi Accumulate Db hb.db.
+Elpi Accumulate File "HB/common/stdpp.elpi".
+Elpi Accumulate File "HB/common/database.elpi".
+Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
+Elpi Accumulate File "HB/common/compat_add_secvar_all.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/context.elpi".
+Elpi Accumulate File "HB/instance.elpi".
+Elpi Accumulate lp:{{
+  func under term, list (pair term term) -> term.
+    under (fun N Ty F) Acc (fun N Ty F') :- 
+      @pi-decl N Ty x\ 
+        under (F x) [(pr x Ty)|Acc] (F' x). 
+    under (app L) Acc (app L') :- 
+      aux Acc L L'. 
+
+  func aux list (pair term term), list term -> list term.
+    aux _ [] [].
+    aux Acc [T|TS] [T|TS'] :- 
+      coq.typecheck T Ty ok,
+      coq.typecheck Ty TyTy ok,
+      %coq.typecheck-ty does not make coercions
+      (not (TyTy = {{Prop}}); T = global _), !,
+      aux Acc TS TS'.
+    aux Acc [T|TS] [T'|TS'] :- 
+      std.spy! (abstract Acc T TA), 
+      log.coq.env.add-const _ TA _ @opaque! C, 
+      T' = app [(global (const C))|{std.map Acc fst}],
+      aux Acc TS TS'. 
+
+  func abstract list (pair term term), term -> term.
+    abstract [] T T' :- 
+      copy T T'.
+    abstract [(pr V Ty) | A] T (fun `x` Ty F) :- 
+      pi w\ (copy V w :- !) => abstract A T (F w).
+
+  main-interp-qed _ _ P _GL (const-decl Name (some _Body) TyWP) :-
+    under P [] P',
+    with-attributes (with-logging (instance.declare-const Name P' TyWP _ _)).
+}}.
+
+#[synterp] Elpi Accumulate lp:{{
+
+shorten coq.env.{ begin-section, end-section }.
+
+main _ :- 
+  SectionName is "hb_instance_" ^ {std.any->string {new_int} },
+  begin-section SectionName, end-section.
+}}.
+
+#[proof="end"] 
+Elpi Export HB.endinstance.
+
+
+
+
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)