declared sort and generic_type as coercions in HB/structures.v

HB/common/synthesis.elpi

@@ -154,7 +154,7 @@ infer-coercion-tgt (w-params.cons ID Ty F) CoeClass :-
   @pi-parameter ID Ty x\ infer-coercion-tgt (F x) CoeClass.
 infer-coercion-tgt (w-params.nil _ {{ Type }} _) sortclass.
 infer-coercion-tgt (w-params.nil _ {{ _ -> _ }} _) funclass.
-infer-coercion-tgt (w-params.nil _ T _) (grefclass GR) :- coq.term->gref T GR.
+infer-coercion-tgt (w-params.nil _ T _) (grefclass GR) :- coq.term-is-gref? T GR.
 
 pred w-args.check-key i:list term, i:term, i:list (w-args A), o:prop.
 w-args.check-key _PS _T [] true :- !.

HB/structure.elpi

@@ -75,6 +75,12 @@ declare Module BSkel Sort :- std.do! [
     log.coq.env.add-const-noimplicits "arg_sort" SortProjection SortProjTy ff ArgSortCst
   ),
 
+  if-verbose (coq.say {header} "declaring generic_type canonical constant"),
+  (ClassAlias => class-def CurrentClass => GRDepsClauses => MixinMems =>
+    w-params.then MLwP mk-fun mk-fun (private.generic-body ClassName) Generic),
+  if-verbose (coq.say {header} "declaring generic constant =" Generic),
+  log.coq.env.add-const-noimplicits "generic_type" Generic _ @transparent! ConstGeneric,
+
   if-verbose (coq.say {header} "start module Exports"),
 
   log.coq.env.begin-module "Exports" none,
@@ -105,10 +111,14 @@ declare Module BSkel Sort :- std.do! [
   %]),
 
   if-verbose (coq.say {header} "making coercion from type to target"),
-  synthesis.infer-coercion-tgt MLwP CoeClass,
-  if-arg-sort (private.declare-sort-coercion CoeClass Structure
-    (global (const ArgSortCst))),
-  private.declare-sort-coercion CoeClass Structure SortProjection,
+  if (synthesis.infer-coercion-tgt MLwP CoeClass)
+    (if-arg-sort (private.declare-sort-coercion CoeClass Structure
+      (global (const ArgSortCst))),
+    private.declare-sort-coercion CoeClass Structure SortProjection)
+    (if-arg-sort (private.declare-sort-coercion-elpi (global Structure) (global (const ArgSortCst))),
+    private.declare-sort-coercion-elpi (global Structure) SortProjection),
+
+  private.declare-generic-coercion-elpi (global Structure) (global (const ConstGeneric)),
 
   if-verbose (coq.say {header} "exporting unification hints"),
   ClassAlias => Factories => GRDepsClauses =>
@@ -123,6 +133,8 @@ declare Module BSkel Sort :- std.do! [
     ])
     (coq.say "declare:" ClassName "should be an inductive", fail),
 
+  coq.TC.declare-class ClassName,
+
   if-verbose (coq.say {header} "accumulating various props"),
   std.flatten [
       Factories, [ClassAlias], [is-structure Structure],
@@ -137,24 +149,26 @@ declare Module BSkel Sort :- std.do! [
 
   log.coq.env.import-module "Exports" Exports,
 
-  if-verbose (coq.say {header} "declaring on_ abbreviation"),
+  if (var CoeClass)
+    (if-verbose (coq.say {header} "could not declare the `on_`, `copy` and `on` abbreviations because the target of sort is not a coercion class"))
+    (if-verbose (coq.say {header} "declaring on_ abbreviation"),
 
-  private.mk-infer-key CoeClass ClassProjection NilwP (global Structure) PhClass,
+    private.mk-infer-key CoeClass ClassProjection NilwP (global Structure) PhClass,
 
-  phant.add-abbreviation "on_" PhClass _ ClassOfAbbrev,
-  (pi c\ coq.notation.abbreviation ClassOfAbbrev [c] (ClassOfAbbrev_ c)),
+    phant.add-abbreviation "on_" PhClass _ ClassOfAbbrev,
+    (pi c\ coq.notation.abbreviation ClassOfAbbrev [c] (ClassOfAbbrev_ c)),
 
-  if-verbose (coq.say {header} "declaring `copy` abbreviation"),
+    if-verbose (coq.say {header} "declaring `copy` abbreviation"),
 
-  coq.mk-app (global ClassName) {params->holes NilwP} AppClassHoles,
-  @global! => log.coq.notation.add-abbreviation "copy" 2
-    {{fun T C => (lp:(ClassOfAbbrev_ C) : (lp:AppClassHoles T)) }} tt _,
+    coq.mk-app (global ClassName) {params->holes NilwP} AppClassHoles,
+    @global! => log.coq.notation.add-abbreviation "copy" 2
+      {{fun T C => (lp:(ClassOfAbbrev_ C) : (lp:AppClassHoles T)) }} tt _,
 
-  if-verbose (coq.say {header} "declaring on abbreviation"),
+    if-verbose (coq.say {header} "declaring on abbreviation"),
 
-  @global! => log.coq.notation.add-abbreviation "on" 1
-    {{fun T => (lp:{{ ClassOfAbbrev_ {{_}} }} : (lp:AppClassHoles T)) }} tt
-    _OnAbbrev,
+    @global! => log.coq.notation.add-abbreviation "on" 1
+      {{fun T => (lp:{{ ClassOfAbbrev_ {{_}} }} : (lp:AppClassHoles T)) }} tt
+      _OnAbbrev),
 
   log.coq.env.end-module-name Module ModulePath,
 
@@ -276,6 +290,46 @@ export-operations Structure ProjSort ProjClass MLwP EX1 EX2 MLToExport :- std.do
   std.map LMwPToExport w-params_1 MLToExport,
 ].
 
+pred mk-sort-coercion-aux i:term, i:term, i:term, i:list term, o:prop.
+mk-sort-coercion-aux (prod _N _T Body) Structure P Args Clause :-
+  Clause = (pi x\ C x),
+  pi x\ mk-sort-coercion-aux (Body x) Structure P [x | Args] (C x).
+
+mk-sort-coercion-aux _ Structure P Args Clause :-
+  std.rev Args ArgsRev,
+  Clause =
+    (pi ctx v t e r argsAll w\ (coercion ctx v t e r :-
+      coq.unify-eq t (app [Structure | ArgsRev]) ok,
+      std.append ArgsRev [v] argsAll,
+      mk-app P argsAll w,
+      coq.elaborate-skeleton w e r ok,
+      coq.ltac.collect-goals r [] [])).
+
+pred mk-sort-coercion i:term, i:term, o:prop.
+mk-sort-coercion Structure P Clause :-
+  coq.typecheck Structure T ok,
+  mk-sort-coercion-aux T Structure P [] Clause.
+
+pred mk-generic-coercion-aux i:term, i:term, i:term, i:list term, o:prop.
+mk-generic-coercion-aux (prod _N _T Body) Structure G Args Clause :-
+  Clause = (pi x\ C x),
+  pi x\ mk-generic-coercion-aux (Body x) Structure G [x | Args] (C x).
+
+mk-generic-coercion-aux _ Structure G Args Clause :-
+  std.rev Args ArgsRev,
+  Clause =
+    (pi ctx v t e r c argsAll w\ (coercion ctx v t e r :-
+      coq.unify-eq e (app [Structure | ArgsRev]) ok,
+      std.append ArgsRev [v, c] argsAll,
+      mk-app G argsAll w,
+      coq.elaborate-skeleton w e r ok,
+      coq.ltac.collect-goals r [] [])).
+
+pred mk-generic-coercion i:term, i:term, o:prop.
+mk-generic-coercion Structure G Clause :-
+  coq.typecheck Structure T ok,
+  mk-generic-coercion-aux T Structure G [] Clause.
+
 pred mk-coe-class-body
   i:factoryname, % From class
   i:factoryname, % To class
@@ -428,18 +482,23 @@ declare-unification-hints SortProj ClassProj CurrentClass NewJoins :- std.do! [
 
 % For each mixin we declare a field and apply the mixin to its dependencies
 % (that are previously declared fields recorded via field-for-mixin)
-pred synthesize-fields i:term, i:list (w-args mixinname), o:record-decl.
-synthesize-fields _T []     end-record.
-synthesize-fields T  [triple M Args _|ML] (field _ Name MTy Fields) :- std.do! [
+% Keeps track of whether every field is in Prop
+pred synthesize-fields i:term, i:list (w-args mixinname), o:record-decl, o:bool.
+synthesize-fields _T []     end-record tt.
+synthesize-fields T  [triple M Args V|ML] (field _ Name MTy Fields) B :- std.do! [
+  if (coq.typecheck {mk-app (global M) {std.append Args [V]} } {{ Prop }} ok)
+    (B = B2)
+    (B = ff),
   Name is {gref->modname M 2 "_"} ^ "_mixin",
   if-verbose (coq.say {header} "typing class field" M),
   std.assert! (synthesis.infer-all-gref-deps Args T M MTy) "anomaly: a field type cannot be solved",
-  @pi-decl `m` MTy m\ mixin-src T M m => synthesize-fields T ML (Fields m)
+  @pi-decl `m` MTy m\ mixin-src T M m => synthesize-fields T ML (Fields m) B2
 ].
 
 pred synthesize-fields.body i:list term, i:term, i:list (w-args mixinname), o:indt-decl.
-synthesize-fields.body _Params T ML (record "axioms_" {{ Type }} "Class" FS) :-
-  synthesize-fields T ML FS.
+synthesize-fields.body _Params T ML (record "axioms_" Ty "Class" FS) :-
+  synthesize-fields T ML FS B,
+  if (B = tt) (Ty = {{ Prop }}) (Ty = {{ Type }}).
 
 pred mk-record+sort-field i:sort, i:name, i:term, i:(term -> record-decl), o:indt-decl.
 pred mk-record+sort-field i:universe, i:name, i:term, i:(term -> record-decl), o:indt-decl.
@@ -460,6 +519,7 @@ declare-class+structure MLwP Sort
 
   w-params.then MLwP (mk-parameter explicit) (mk-parameter explicit)
     synthesize-fields.body ClassDeclaration,
+  coq.say "ClassDeclaration" ClassDeclaration,
 
   std.assert-ok! (coq.typecheck-indt-decl ClassDeclaration) "declare-class: illtyped",
   (@primitive! => log.coq.env.add-indt ClassDeclaration ClassInd),
@@ -495,6 +555,27 @@ declare-sort-coercion CoeClass StructureName (global Proj) :-
 
   log.coq.coercion.declare (coercion Proj 0 StructureName CoeClass).
 
+% Declares "sort" as a Coercion in elpi's coercion db Proj : Structurename >-> CoeClass.
+pred declare-sort-coercion-elpi i:term, i:term.
+declare-sort-coercion-elpi Structure Proj :-
+
+  if-verbose (coq.say {header} "declare sort coercion in elpi"),
+
+  %TODO: log.coq.coercion-elpi.declare 
+  mk-sort-coercion Structure Proj Clause,
+  coq.elpi.accumulate _ "coercion.db" (clause _ _ Clause).
+
+% Declares "generic_type" as a Coercion in elpi's coercion db
+pred declare-generic-coercion-elpi i:term, i:term.
+declare-generic-coercion-elpi Structure G :-
+
+  if-verbose (coq.say {header} "declare `generic_type` coercion in elpi"),
+
+  %TODO: log.coq.coercion-elpi.declare 
+  mk-generic-coercion Structure G Clause,
+  coq.elpi.accumulate _ "coercion.db" (clause _ _ Clause).
+
+
 pred if-class-already-exists-error i:id, i:list class, i:list mixinname.
 if-class-already-exists-error _ [] _.
 if-class-already-exists-error N [class _ S ML1wP|CS] ML2 :-
@@ -583,6 +664,17 @@ pack-body.aux PL T BuildC PackS  Body :- !, std.do! [
   mk-app (global PackS) {std.append PL [T, Class]} Body
 ].
 
+% [generic-body ClassName P T MLwA B] asserts
+%  B = fun c => Pack P T c
+% under a context with P and T
+pred generic-body i:classname, i:list term, i:term, i:list (w-args mixinname), o:term.
+generic-body ClassName PL T _MLwA F :- std.do! [
+  class-def (class ClassName S _),
+  get-constructor S PackS,
+  F = fun {coq.string->name "C"} {mk-app (global ClassName) {std.append PL [T]} } (c\ {mk-app (global PackS) {std.append PL [T, c]} }),
+].
+
+
 pred mk-infer-key i:class, i:term, i:mixins, i:term, o:phant-term.
 mk-infer-key CoeClass K (w-params.nil ID _ _) St PhK :-
   @pi-parameter ID St t\ phant.init {mk-app K [t]} (PhKBo t),

structures.v

@@ -15,7 +15,7 @@ Definition ignore {T} (x: T) := x.
 Definition ignore_disabled {T T'} (x : T) (x' : T') := x'.
 
 (* ********************* structures ****************************** *)
-From elpi Require Import elpi.
+From elpi Require Import elpi coercion.
 
 Register unify as hb.unify.
 Register id_phant as hb.id.
@@ -619,6 +619,7 @@ HB.structure Definition StructureName params :=
 *)
 
 #[arguments(raw)] Elpi Command HB.structure.
+Elpi Accumulate Db coercion.db.
 Elpi Accumulate Db hb.db.
 Elpi Accumulate File "HB/common/stdpp.elpi".
 Elpi Accumulate File "HB/common/database.elpi".