Merge pull request #135 from math-comp/fix-elab-params

Elaboration of parameters in HB.structure and HB.builders

Author: CohenCyril

hb.elpi

@@ -104,8 +104,6 @@ if-MC-compat P :- get-option "mathcomp.axiom" S, !,
   P (some GR).
 if-MC-compat _.
 
-
-
 % TODO: Should this only be used for gref that are factories? (and check in the first/second branch so?)
 % Should we make this an HO predicate, eg "located->gref S L is-factory? GR"
 pred located->gref i:string, i:list located, o:gref.
@@ -696,7 +694,7 @@ phant-fun-struct T Name S Params PF Out :- std.do! [
   mk-app (global S) Params SParams,
   mk-app SortProj Params SortProjParams,
   % Msg = {{lib:hb.nomsg}},
-  Msg = {{lib:hb.some (lib:hb.pair "is not canonically a"%string lp:SParams)}},
+  Msg = {{lib:hb.some (lib:hb.pair lib:hb.not_a_msg lp:SParams)}},
   (@pi-decl Name SParams s\ phant-fun-unify Msg T {mk-app SortProjParams [s]} (PF s) (UnifSI s)),
   phant-fun-implicit Name SParams UnifSI Out
 ].
@@ -1853,31 +1851,39 @@ declare-old-constant (some C) :-
   std.forall {coq.locate-all Id} (declare-old-located Id).
 declare-old-constant _ :- true.
 
-pred context->factory i:context-decl, o:factoryname.
-context->factory (context-item IDT _ TTySkel none t\ context-item _ _ (TF t) none _\ context-end) GRF :- !,
-  coq.id->name IDT NameT,
-  std.assert-ok! (coq.elaborate-ty-skeleton TTySkel _ TTy) "context entry illtyped",
-  @pi-decl NameT TTy t\
-    std.assert! (factory? (TF t) (triple GRF _Params t))
-      "the last argument must be a factory applied to the type variable".
-context->factory (context-item ID _ TSkel none Factories) GRF :- !,
-  coq.id->name ID Name,
-  std.assert-ok! (coq.elaborate-ty-skeleton TSkel _ T) "context entry illtyped",
-  @pi-decl Name T x\ context->factory (Factories x) GRF.
-context->factory (context-item ID _ _ (some _) _) _ :-
+pred elaborate-context-skel->factory i:context-decl, o:context-decl, o:factoryname, o:diagnostic.
+elaborate-context-skel->factory
+  (context-item IDT IT TTySkel none t\ context-item IDF IF (TFSkel t) none _\ context-end)
+  (context-item IDT IT TTy none t\ context-item IDF IF (TFSkel t) none _\ context-end) GRF Diag
+:- !, std.do-ok! Diag [
+  coq.elaborate-ty-skeleton TTySkel _ TTy,
+  (d\ coq.id->name IDT NameT),
+  (d\ @pi-decl NameT TTy t\ purge-id (TFSkel t) (TFSkel1 t), coq.elaborate-ty-skeleton (TFSkel1 t) _ (TF1 t) d),
+  (d\ @pi-decl NameT TTy t\ std.assert! (factory? (TF1 t) (triple GRF _Params t)) "the last argument must be a factory applied to the type variable"),
+].
+elaborate-context-skel->factory (context-item ID I TSkel none C) (context-item ID I T none C1) GRF Diag :- !, std.do-ok! Diag [
+  coq.elaborate-ty-skeleton TSkel _ T,
+  (d\ coq.id->name ID Name),
+  (d\ @pi-decl Name T x\ elaborate-context-skel->factory (C x) (C1 x) GRF d),
+].
+elaborate-context-skel->factory (context-item ID _ _ (some _) _) _ _ _ :-
   coq.error "context item cannot be given a body:" ID.
 
+pred purge-id i:term, o:term.
+purge-id T T1 :-
+  (pi fresh t v\ copy {{lib:@hb.id lp:t lp:v}} fresh :- !) => copy T T1.
+
 pred main-begin-declare-builders i:context-decl.
 main-begin-declare-builders CtxSkel :- std.do! [
   Name is "Builders_" ^ {term_to_string {new_int}}, % TODO?
-  context->factory CtxSkel GRF,
+  std.assert-ok! (elaborate-context-skel->factory CtxSkel Ctx GRF) "Context illtyped",
   coq.env.begin-module Name none,
   if (GRF = indt FRecord) (std.do! [
     coq.env.begin-module "Super" none,
     std.forall {coq.CS.canonical-projections FRecord} declare-old-constant,
     coq.env.end-module _]) (true),
   coq.env.begin-section Name,
-  builders-postulate-factories CtxSkel,
+  builders-postulate-factories Ctx,
 ].
 
 pred postulate-factory-abbrev i:term, i:list term, i:id, i:factoryname, o:term.
@@ -1936,7 +1942,7 @@ builders-postulate-factories (context-item IDT _ TySkel none t\ context-item IDF
 
 builders-postulate-factories (context-item ID _ TSkel none Factories) :- std.do! [
   if-verbose (coq.say "HB: postulating" ID),
-  std.assert-ok! (coq.elaborate-ty-skeleton TSkel _ T) "builders-postulate-factorie: illtyped context",
+  std.assert-ok! (coq.elaborate-ty-skeleton TSkel _ T) "builders-postulate-factories: illtyped context",
   if (var T) (coq.fresh-type T) true,
   @local! => hb-add-const ID _ T @opaque! P, % no body, local -> a variable
   TheParam = global (const P),

structures.v

@@ -7,11 +7,13 @@ Definition unify T1 T2 (t1 : T1) (t2 : T2) (s : option (string * Type)) :=
   phantom T1 t1 -> phantom T2 t2.
 Definition id_phant {T} {t : T} (x : phantom T t) := x.
 Definition nomsg : option (string * Type) := None.
+Definition is_not_canonically_a : string := "is not canonically a".
 
 Register unify as hb.unify.
 Register id_phant as hb.id.
 Register Coq.Init.Datatypes.None as hb.none.
 Register nomsg as hb.nomsg.
+Register is_not_canonically_a as hb.not_a_msg.
 Register Coq.Init.Datatypes.Some as hb.some.
 Register Coq.Init.Datatypes.pair as hb.pair.
 Register Coq.Init.Datatypes.prod as hb.prod.
@@ -290,7 +292,8 @@ sigT->list-w-params {{ lib:@hb.sigT _ lp:{{ fun N Ty B }} }} L C :-
     product->triples (B t) (Rest t) C.
 
 main [const-decl Module (some B) _] :- !, std.do! [
-  sigT->list-w-params B GRFS ClosureCheck, !,
+  purge-id B B1, std.assert-ok! (coq.elaborate-skeleton B1 _ B2) "illtyped structure definition",
+  sigT->list-w-params B2 GRFS ClosureCheck, !,
   with-attributes (main-declare-structure Module GRFS ClosureCheck),
 ].
 main _ :- coq.error "Usage: HB.structure Definition <ModuleName> := { A of <Factory1> A & … & <FactoryN> A }".
@@ -507,6 +510,9 @@ Elpi Typecheck.
 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.
 Notation "`Error: t msg T" := (unify t _ (Some (msg%string, T)))
   (at level 0, msg, T at level 0, format "`Error:  t  msg  T", only printing) :
   form_scope.

tests/subtype.v

@@ -22,7 +22,7 @@ SubK : forall x Px, val (@Sub x Px) = x
 
 HB.structure Definition SUB (T : Type) (P : pred T) := { S of is_SUB T P S }.
 
-HB.structure Definition SubInhab T P := { sT of is_inhab T & is_SUB T P sT }.
+HB.structure Definition SubInhab (T : Type) P := { sT of is_inhab T & is_SUB T P sT }.
 
 HB.structure Definition SubNontrivial T P := { sT of is_nontrivial sT & is_SUB T P sT }.