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}})
@@ -350,3 +353,36 @@ saturate-type-constructor T ET :-
   coq.typecheck T TH ok,
   coq.count-prods TH N,
   coq.mk-app T {coq.mk-n-holes N} ET.
+
+
+namespace abstract-props-as-lemmas {
+
+  func main term, list (triple name term term) -> term.
+    main (fun N Ty F) Acc (fun N Ty F') :- 
+      @pi-decl N Ty x\ 
+        main (F x) [(triple N x Ty)|Acc] (F' x). 
+    main (app L) Acc (app L') :- 
+      aux Acc L L'. 
+
+  func aux list (triple name term term), list term -> list term.
+    aux _ [] [].
+    aux Acc [(global _ as T)|TS] [T|TS'] :- !,
+      aux Acc TS TS'.
+    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}})), !,
+      aux Acc TS TS'.
+    aux Acc [T|TS] [T'|TS'] :- 
+      std.spy! (abstract Acc T TA), 
+      coq.env.add-const _ TA _ @opaque! C, 
+      T' = app [(global (const C))|{std.map Acc triple_2}],
+      aux Acc TS TS'. 
+
+  func abstract list (triple name term term), term -> term.
+    abstract [] T T' :- 
+      copy T T'.
+    abstract [(triple N V Ty) | A] T (fun N Ty F) :- 
+      pi w\ (copy V w :- !) => abstract A T (F w).
+}

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.
 
@@ -44,7 +46,7 @@
 Register eta as hb.eta.
 
 #[deprecated(since="HB 1.0.1", note="use #[key=...] instead")]
 Notation indexed T := T (only parsing).
 
 Declare Scope HB_scope.
 Notation "{  A  'of'  P  &  ..  &  Q  }" :=
@@ -771,6 +773,7 @@
     - [#[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,73 @@
 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,
+  coq.say "Once there are no more subgoals, use the command \"HB.end_instance.\" to conclude the instance". 
 }}.
+
+#[synterp] Elpi Accumulate File "HB/common/utils-synterp.elpi".
 #[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 _ :-
+  with-attributes (
+    if (get-option "interactive" _)
+      (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.end_instance.
+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:{{
+    main-interp-qed _ _ P _GL (const-decl Name (some _Body) TyWP) :-
+    abstract-props-as-lemmas.main 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.end_instance.
+
+
+
+
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
@@ -1215,9 +1268,9 @@
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
 
 (** Technical notations from /Canonical Structures for the working Coq user/ *)
 Notation "`Error_cannot_unify: t1 'with' t2" := (unify t1 t2 None)
   (at level 0, format "`Error_cannot_unify:  t1  'with'  t2", only printing) :
   form_scope.
   Notation "`Error: t `is_not_canonically_a T" := (unify t _ (Some (is_not_canonically_a, T)))
   (at level 0, T at level 0, format "`Error:  t  `is_not_canonically_a  T", only printing) :
   form_scope.