Merge pull request #146 from math-comp/phant-params

inference of structures on paramters

Author: CohenCyril

.github/workflows/main.yml

@@ -27,6 +27,7 @@ jobs:
   opam:
     runs-on: ubuntu-latest
     strategy:
+      fail-fast: false
       matrix:
         coq_version:
           - '8.11'

_CoqProject

@@ -53,5 +53,6 @@ tests/instance_params_no_type.v
 tests/test_CS_db_filtering.v
 tests/subtype.v
 tests/exports.v
+tests/infer.v
 
 -R . HB

hb.elpi

@@ -82,17 +82,33 @@ under.do! Then LP :- Then (_\ std.do! LP) _.
 
 %%%%% HB Utils %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
+
+% HACK: move to coq-elpi proper, remove when coq-elpi > 1.9.2
+type attmap attribute-type.
+
 % runs P in a context where Coq #[attributes] are parsed
 pred with-attributes i:prop.
 with-attributes P :-
   attributes A,
+
+% HACK: move to coq-elpi proper, remove when coq-elpi > 1.9.2
+(pi S L AS Prefix R R1 Map PS\ 
+  parse-attributes.aux [attribute S (node L)|AS] Prefix R :-
+    if (Prefix = "") (PS = S) (PS is Prefix ^ "." ^ S), supported-attribute (att PS attmap), !,
+    parse-attributes.aux AS Prefix R1,
+    (pi x\ supported-attribute (att x string) :- !) => parse-attributes.aux L "" Map,
+    std.append R1 [get-option PS Map] R
+) =>
+
   coq.parse-attributes A [
     att "verbose" bool,
     att "mathcomp" bool,
     att "mathcomp.axiom" string,
+    att "infer" attmap,
   ] Opts, !,
   Opts => P.
 
+
 pred if-verbose i:prop.
 if-verbose P :- get-option "verbose" tt, !, P.
 if-verbose _.
@@ -646,6 +662,7 @@ type mterm list term -> term -> list mixinname -> term -> mterm.
 % - [id]             using [unify-arg]
 kind phant-arg type.
 type real-arg name -> phant-arg.
+type infer-type name -> phant-arg.
 type implicit-arg phant-arg.
 type unify-arg phant-arg.
 
@@ -920,15 +937,18 @@ mk-phant-abbrev.term K F [] K F.
 mk-phant-abbrev.term K F [real-arg N|AL] K'' (fun N _ AbbrevFx) :- !,
   pi x\ mk-phant-abbrev.term K {mk-app F [x]} AL K' (AbbrevFx x),
   K'' is K' + 1.
+mk-phant-abbrev.term K F [infer-type N|AL] K'' (fun N _ AbbrevFx) :- !,
+  pi x\ mk-phant-abbrev.term K {mk-app F [{{ lib:hb.Phant lp:x }}]} AL K' (AbbrevFx x),
+  K'' is K' + 1.
 mk-phant-abbrev.term K F [implicit-arg|AL] K' FAbbrev :- !,
   mk-phant-abbrev.term K {mk-app F [_]} AL K' FAbbrev.
 mk-phant-abbrev.term K F [unify-arg|AL] K' FAbbrev :- !,
   mk-phant-abbrev.term K {mk-app F [{{lib:@hb.id _ _}}]} AL K' FAbbrev.
 
 pred mk-phant-abbrev i:string, i:phant-term, o:constant, o:abbreviation.
-mk-phant-abbrev N (phant-term AL T) C Abbrev :- std.do! [
+mk-phant-abbrev N (phant-term AL T1) C Abbrev :- std.do! [
   NC is "phant_" ^ N,
-  std.assert-ok! (coq.typecheck T TTy) "mk-phant-abbrev: T illtyped",
+  std.assert-ok! (coq.elaborate-skeleton T1 TTy T) "mk-phant-abbrev: T illtyped",
   hb-add-const NC T TTy @transparent! C,
   mk-phant-abbrev.term 0 (global (const C)) AL NParams AbbrevT,
   @global! => coq.notation.add-abbreviation N NParams AbbrevT tt Abbrev,
@@ -1499,7 +1519,8 @@ synthesize-fields.body _Params T ML (record "axioms" {{ Type }} "Class" FS) :-
   synthesize-fields T ML FS.
 
 pred mk-record+sort-field i:name, i:term, i:(term -> record-decl), o:indt-decl.
-mk-record+sort-field _ T F (record "type" {{ Type }} "Pack" (field _ "sort" T F)).
+mk-record+sort-field _ T F (record RecordName {{ Type }} "Pack" (field _ "sort" T F)) :-
+  if (get-option "infer" _) (RecordName = "type_") (RecordName = "type").
 
 pred mk-class-field i:classname, i:list term, i:term, i:list (w-args mixinname), o:record-decl.
 mk-class-field ClassName Params T _ (field _ "class" (app [global ClassName|Args]) _\end-record) :-
@@ -1634,6 +1655,25 @@ pack-body ClassName PL T MLwA F :- std.do! [
   under-mixins.then MLwA mk-fun (pack-body.mixins PL T BuildC PackS) F
 ].
 
+pred declare-auto-infer-params-abbrev i:structure, i:list-w-params mixinname.
+declare-auto-infer-params-abbrev GR MLwP :- get-option "infer" Map, !,
+  Map => mk-infer (global GR) MLwP PHT,
+  mk-phant-abbrev "type" PHT _ _.
+declare-auto-infer-params-abbrev _ _.
+
+pred mk-infer i:term, i:list-w-params mixinname, o:phant-term.
+mk-infer T (w-params.nil _ _ _) (phant-term [] T).
+mk-infer T (w-params.cons N Ty W) (phant-term [implicit-arg, infer-type N|A] R1) :-
+  coq.name->id N ID, (get-option ID "Type" ; get-option ID ""), !,
+  R1 = (fun N Ty n\ fun `ph` {{ lib:@hb.phant lp:n }} _\ R n),
+  @pi-decl N Ty n\
+    mk-infer {mk-app T [n]} (W n) (phant-term A (R n)).
+mk-infer T (w-params.cons N Ty W) (phant-term [real-arg N|A] (fun N Ty R)) :-
+   coq.name->id N ID, not (get-option ID _), !,
+  @pi-decl N Ty x\  mk-infer {mk-app T [x]} (W x) (phant-term A (R x)).
+mk-infer _ (w-params.cons N _ _) _ :- coq.name->id N ID, get-option ID Infer,
+  coq.error "Automatic inference of paramter" N "from" Infer "not supported".
+
 % HB.structure Definition S P1 P2 := { T of F1 P1 T & F2 P1 (P2*P2) T }
 %  cons p1\ cons p2\ nil t\ [triple f1 [p1] t,triple f2 [p1, {{p1 * p2}}] t]
 pred main-declare-structure i:string, i:list-w-params gref, i:bool.
@@ -1668,6 +1708,8 @@ main-declare-structure Module GRFSwP ClosureCheck :- std.do! [
   ClassRequires = factory-requires (ClassName) NilwP,
   ClassAlias = (factory-alias->gref ClassName ClassName),
   CurrentClass = (class ClassName Structure MLwP),
+  
+  declare-auto-infer-params-abbrev Structure MLwP,
 
   if-verbose (coq.say "HB: declaring clone abbreviation"),
 
@@ -2213,4 +2255,4 @@ declare-mixin-or-factory Sort1 Fields GRFSwP Module TheType D TheParams :- std.d
   export Exports,
 
   declare-factory-abbrev Module FactAbbrev,
-].
+].

structures.v

@@ -18,6 +18,8 @@ Register Coq.Init.Datatypes.Some as hb.some.
 Register Coq.Init.Datatypes.pair as hb.pair.
 Register Coq.Init.Datatypes.prod as hb.prod.
 Register Coq.Init.Specif.sigT as hb.sigT.
+Register Coq.ssr.ssreflect.phant as hb.phant.
+Register Coq.ssr.ssreflect.Phant as hb.Phant.
 Definition indexed {T} (x : T) := x.
 Bind Scope type_scope with indexed.
 Register indexed as hb.indexed.

tests/infer.v

@@ -0,0 +1,28 @@
+From HB Require Import structures.
+
+HB.mixin Record foom T := {
+  op : T -> T -> T
+}.
+
+HB.structure Definition foo := { T of foom T }.
+
+HB.instance Definition i := foom.Build nat plus.
+
+HB.mixin Record barm (A : Type) (P : foo.type) (B: Type) (T : indexed Type) := {
+  law : P -> T -> A -> B
+}.
+
+#[infer(P)]
+HB.structure Definition bar A P B := { T of barm A P B T }.
+
+Fail Check bar.type_ bool nat bool.
+Print bar.phant_type.
+Print bar.type.
+Check bar.type bool nat bool.
+
+Fail #[infer(P = "whatever")]
+HB.structure Definition bar1 P := { T of barm bool P bool T & foom T }.
+
+#[infer(P = "Type")]
+HB.structure Definition bar1 P := { T of barm bool P bool T & foom T }.
+Check bar1.type nat.