clanup

Author: gares

hb.elpi

@@ -204,9 +204,6 @@ gref->modname GR ModName :-
   coq.gref->path GR Path,
   if (std.rev Path [_,ModName|_]) true (coq.error "No enclosing module for " GR).
 
-pred term->modname i:structure, o:id.
-term->modname T ModName :- gref->modname {term->gref T} ModName.
-
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % function to predicate generic constructions %
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -375,6 +372,14 @@ pred mixin-src_src i:prop, o:term.
 mixin-src_src (mixin-src _ _ S) S.
 mixin-src_src (pi c\ mixin-src _ _ c :- F c) T :- F T. % this is a bit pulp...
 
+pred class_name i:class, o:classname.
+class_name (class N _ _) N.
+
+pred class-def_name i:prop, o:classname.
+class-def_name (class-def (class N _ _)) N.
+
+pred classname->def i:classname, o:class.
+classname->def CN (class CN S ML) :- class-def (class CN S ML), !.
 
 pred extract-builder i:prop, o:builder.
 extract-builder (builder-decl B) B.
@@ -466,20 +471,21 @@ toposort-proj.acc Proj ES Acc [A|In] Out :- std.do![
 ].
 
 % Classes can be topologically sorted according to the subclass relation
-pred toposort-classes.mk-class-edge i:prop, o:pair class class.
+pred toposort-classes.mk-class-edge i:prop, o:pair classname classname.
 toposort-classes.mk-class-edge (sub-class C1 C2) (pr C2 C1).
-pred toposort-classes i:list class, o:list class.
+pred toposort-classes i:list classname, o:list classname.
 toposort-classes In Out :- std.do! [
   std.findall (sub-class C1_ C2_) SubClasses,
   std.map SubClasses toposort-classes.mk-class-edge ES,
   toposort ES In Out,
 ].
 
 pred findall-classes o:list class.
-findall-classes CLSorted :- std.do! [
+findall-classes CLSortedDef :- std.do! [
   std.findall (class-def C_) All,
-  std.map All (x\r\ x = class-def r) CL,
-  toposort-classes CL CLSorted
+  std.map All class-def_name CL,
+  toposort-classes CL CLSorted,
+  std.map CLSorted classname->def CLSortedDef,
 ].
 
 pred findall-builders o:list builder.
@@ -534,55 +540,54 @@ findall-newjoins CurrentClass AllSuper TodoJoins :-
 
 % [get-structure-coercion S1 S2 F] finds the coecion F from the structure S1 to S2
 pred get-structure-coercion i:structure, i:structure, o:term.
-get-structure-coercion (global S _) (global T _) FU :-
+get-structure-coercion S T FU :-
   coq.coercion.db-for (grefclass S) (grefclass T) L,
   if (L = [pr F _]) true (coq.error "No one step coercion from" S "to" T),
   coq.env.global F FU.
 
-% TODO
 pred get-structure-sort-projection i:structure, o:term.
-get-structure-sort-projection T Proj :-
-  safe-dest-app T (global (indt S) _) Params,
+get-structure-sort-projection (indt S) Proj :- !,
   coq.CS.canonical-projections S L,
   if (L = [some P, _]) true (coq.error "No canonical sort projection for" S),
-  mk-app {coq.env.global (const P)} Params Proj.
+  coq.env.global (const P) Proj.
+get-structure-sort-projection S _ :- coq.error "get-structure-sort-projection: not a structure" S.
 
 pred get-structure-class-projection i:structure, o:term.
-get-structure-class-projection (global (indt S) _) T :-
+get-structure-class-projection (indt S) T :- !,
   coq.CS.canonical-projections S L,
   if (L = [_, some P]) true (coq.error "No canonical class projection for" S),
   coq.env.global (const P) T.
+get-structure-class-projection S _ :- coq.error "get-structure-class-projection: not a structure" S.
 
-pred get-constructor i:term, o:gref.
-get-constructor (global (indt R) UI as S) (indc K) :- !,
- if (coq.env.indt R UI _ _ _ _ [K] _) true (coq.error "Not a record" S).
+pred get-constructor i:gref, o:gref.
+get-constructor (indt R) (indc K) :- !,
+ if (coq.env.indt R _ _ _ _ _ [K] _) true (coq.error "Not a record" R).
+get-constructor I _ :- coq.error "get-constructor: not an inductive" I.
 
-pred safe-head i:term, o:term.
-safe-head (prod N T Body) Hd :-
-  @pi-decl N T x\
-    safe-head (Body x) (Hd' x),
-    std.assert! (Hd' x = Hd) "safe-head: the head symbol is a bound variable".
-safe-head T Hd :- whd1 T T', safe-head T' Hd.
-safe-head T Hd :- safe-dest-app T Hd _.
+pred head-gref-under-prods i:term, o:gref.
+head-gref-under-prods (prod N T Body) Hd :-
+  @pi-decl N T x\ head-gref-under-prods (Body x) Hd.
+head-gref-under-prods T Hd :- whd1 T T', head-gref-under-prods T' Hd.
+head-gref-under-prods T Hd :- safe-dest-app T (global Hd _) _.
 
 %% finding for locally defined structures
-pred get-cs-structure i:cs-instance, o:term.
-get-cs-structure (cs-instance _ _ (global Inst UI)) Struct :- std.do! [
-  coq.env.typeof Inst UI InstTy,
-  safe-head InstTy Struct
+pred get-cs-structure i:cs-instance, o:structure.
+get-cs-structure (cs-instance _ _ Inst) Struct :- std.do! [
+  coq.env.typeof Inst _ InstTy,
+  head-gref-under-prods InstTy Struct
 ].
 
 pred has-cs-instance i:gref, i:cs-instance.
 has-cs-instance GTy (cs-instance _ (cs-gref GTy) _).
 
-pred get-local-structures i:term, o:list term.
+pred get-local-structures i:term, o:list structure.
 get-local-structures TyTrm StructL :- std.do! [
   std.filter {coq.CS.db} (has-cs-instance {term->gref TyTrm}) DBGTyL,
   std.map DBGTyL get-cs-structure RecL,
   std.filter RecL is-structure StructL
 ].
 
-pred local-cs? i:term, i:term.
+pred local-cs? i:term, i:structure.
 local-cs? TyTerm Struct :-
   get-local-structures TyTerm StructL,
   std.mem! StructL Struct.
@@ -679,16 +684,17 @@ phant-fun-unify-mixin T N Ty PF Out :- !, std.do! [
   phant-fun-implicit N Ty PFM Out
 ].
 
-% [phant-fun-struct T SI PF PSF] states that PSF is a phant-term
+% [phant-fun-struct T SI SIParams PF PSF] states that PSF is a phant-term
 % which postulate a structure [s : SI] such that [T = sort s]
 % and then outputs [PF s]
-pred phant-fun-struct i:term, i:name, i:term, i:(term -> phant-term), o:phant-term.
-phant-fun-struct T Name SI PF Out :- std.do! [
+pred phant-fun-struct i:term, i:name, i:structure, i:list term, i:(term -> phant-term), o:phant-term.
+phant-fun-struct T Name SI Params PF Out :- std.do! [
   get-structure-sort-projection SI Sort,
+  mk-app {coq.env.global SI} Params SITerm,
   % Msg = {{lib:hb.nomsg}},
-  Msg = {{lib:hb.some (lib:hb.pair "is not canonically a"%string lp:SI)}},
-  (@pi-decl Name SI s\ phant-fun-unify Msg T {mk-app Sort [s]} (PF s) (UnifSI s)),
-  phant-fun-implicit Name SI UnifSI Out
+  Msg = {{lib:hb.some (lib:hb.pair "is not canonically a"%string lp:SITerm)}},
+  (@pi-decl Name SITerm s\ phant-fun-unify Msg T {mk-app Sort [s]} (PF s) (UnifSI s)),
+  phant-fun-implicit Name SITerm UnifSI Out
 ].
 
 % [builder->term Params T Src Tgt MF] provides a term which is
@@ -977,7 +983,7 @@ pred mk-phant-term.mixins i:term, i:classname, i:phant-term,
   i:list term, i:name, i:term, i:(term -> list (w-args mixinname)), o:phant-term.
 mk-phant-term.mixins T CN PF Params N Ty MLwA Out :- std.do! [
   class-def (class CN SI _),
-  mk-app SI Params SIParams,
+  mk-app {coq.env.global SI} Params SIParams,
   NoMsg = {{lib:hb.nomsg}},
   coq.name-suffix N "local" Nlocal,
   (@pi-decl Nlocal Ty t\ sigma SK KC ML\ std.do! [
@@ -989,12 +995,12 @@ mk-phant-term.mixins T CN PF Params N Ty MLwA Out :- std.do! [
        under-mixins.then (MLwA t) (phant-fun-unify-mixin T) (mk-phant-term.mixins.aux t Params c CN PF) PF2,
        phant-fun-unify NoMsg s {mk-app SKPT [c]} PF2 (PFU t s c)])
   ]),
-  Out = {phant-fun-struct T `s` SIParams s\
+  Out = {phant-fun-struct T `s` SI Params s\
           {phant-fun-implicit `c` ClassTy (PFU T s)}}
 ].
 
 mk-phant-term.mixins.aux T Params C CN PF X :- std.do![
-  get-constructor {coq.env.global CN} KC,
+  get-constructor CN KC,
   mgref->term Params T KC KCM,
   phant-fun-unify {{lib:hb.nomsg}} KCM C PF X,
 ].
@@ -1100,24 +1106,24 @@ params->holes (w-params.cons _ _ F) [_|PS] :- pi x\ params->holes (F x) PS.
 pred declare-instances i:term, i:list class.
 declare-instances T [class Class Struct MLwP|Rest] :-
   params->holes MLwP Params,
-  get-constructor {coq.env.global Class} KC,
+  get-constructor Class KC,
 
   if (not(local-cs? T Struct))
      true % we build it
      (if-verbose (coq.say "HB: skipping alreay existing"
-                    {coq.term->string Struct} "instance on"
+                    {nice-gref->string Struct} "instance on"
                     {coq.term->string T}),
       fail),
 
   if (mgref->term Params T KC KCApp)
-     (if-verbose (coq.say "HB: we can build a" {coq.term->string Struct} "on"
+     (if-verbose (coq.say "HB: we can build a" {nice-gref->string Struct} "on"
         {coq.term->string T}))
      fail,
 
   !,
   term->gref T TGR,
   coq.gref->id TGR TID,
-  Name is TID ^ "_is_a_" ^ {term->modname Struct},
+  Name is TID ^ "_is_a_" ^ {gref->modname Struct},
 
   if-verbose (coq.say "HB: declare canonical structure instance" Name),
 
@@ -1261,10 +1267,10 @@ clean-op-ty [exported-op _ Po C|Ops] S T1 T2 :-
 
   clean-op-ty Ops S T1 T2.
 
-pred operation-body-and-ty i:list prop, i:constant, i:term, i:term, i:term,
+pred operation-body-and-ty i:list prop, i:constant, i:structure, i:term, i:term,
   i:list term, i:term, i:w-args A, o:pair term term.
 operation-body-and-ty EXI Poperation Struct Psort Pclass Params _T (triple _ Params _) (pr Bo Ty) :- std.do! [
-  mk-app Struct Params StructType,
+  mk-app {coq.env.global Struct} Params StructType,
   mk-app Psort Params PsortP,
   mk-app Pclass Params PclassP,
   Bo = fun `s` StructType Body,
@@ -1285,7 +1291,7 @@ operation-body-and-ty EXI Poperation Struct Psort Pclass Params _T (triple _ Par
 % same operation out of the package structure (out of the class field of the
 % structure). We also provide all the other mixin dependencies (other misins)
 % of the package structure.
-pred export-1-operation i:mixinname, i:term, i:term, i:term, i:one-w-params mixinname, i:option constant, i:list prop, o:list prop.
+pred export-1-operation i:mixinname, i:structure, i:term, i:term, i:one-w-params mixinname, i:option constant, i:list prop, o:list prop.
 export-1-operation _ _ _ _ _ none EX EX :- !. % not a projection, no operation
 export-1-operation M Struct Psort Pclass MwP (some Poperation) EXI EXO :- !, std.do! [
   coq.gref->id (const Poperation) Name,
@@ -1304,7 +1310,7 @@ export-1-operation M Struct Psort Pclass MwP (some Poperation) EXI EXO :- !, std
 ].
 
 % Given a list of mixins, it exports all operations in there
-pred export-operations.aux i:term, i:term, i:term, i:one-w-params mixinname, i:list prop, o:list prop.
+pred export-operations.aux i:structure, i:term, i:term, i:one-w-params mixinname, i:list prop, o:list prop.
 export-operations.aux Struct ProjSort ProjClass MwP EX1 EX2 :- !, std.do! [
   w-params_1 MwP (indt M),
   coq.CS.canonical-projections M Poperations,
@@ -1315,7 +1321,7 @@ pred mixin-not-already-declared i:one-w-params mixinname.
 mixin-not-already-declared MwP :-
   w-params_1 MwP M, not(mixin-first-class M _), M = indt _.
 
-pred export-operations i:term, i:term, i:term, i:list-w-params mixinname, i:list prop, o:list prop, o:list mixinname.
+pred export-operations i:structure, i:term, i:term, i:list-w-params mixinname, i:list prop, o:list prop, o:list mixinname.
 export-operations Structure ProjSort ProjClass MLwP EX1 EX2 MLToExport :- std.do! [
   distribute-w-params MLwP LMwP,
   std.filter LMwP mixin-not-already-declared LMwPToExport,
@@ -1337,7 +1343,7 @@ mk-coe-class-body FC TC TMLwP Params T _ CoeBody :- std.do! [
   std.map TML (from FC) Builders,
   std.map Builders (x\r\sigma t\ coq.env.global x t, mk-app t Params r) BuildersP,
 
-  mk-app {coq.env.global {get-constructor {coq.env.global TC}}}
+  mk-app {coq.env.global {get-constructor TC}}
     {coq.mk-n-holes {factory-nparams TC}} KCHoles,
 
   (pi c\ sigma Mixes\
@@ -1360,10 +1366,10 @@ pred mk-coe-structure-body
 mk-coe-structure-body StructureF StructureT TC Coercion SortProjection ClassProjection
     Params _T _ SCoeBody :- std.do! [
 
-  mk-app StructureF      Params StructureP,
-  mk-app SortProjection  Params SortP,
-  mk-app ClassProjection Params ClassP,
-  mk-app Coercion        Params CoercionP,
+  mk-app {coq.env.global StructureF} Params StructureP,
+  mk-app             SortProjection  Params SortP,
+  mk-app             ClassProjection Params ClassP,
+  mk-app             Coercion        Params CoercionP,
 
   mk-app {coq.env.global {get-constructor StructureT}}
     {coq.mk-n-holes {factory-nparams TC}} PackPH,
@@ -1377,12 +1383,12 @@ mk-coe-structure-body StructureF StructureT TC Coercion SortProjection ClassProj
 % from C1 to C2 given P1 P2 the two projections from the structure of C1
 pred declare-coercion i:term, i:term, i:class, i:class.
 declare-coercion SortProjection ClassProjection
-    (class FC StructureF FMLwP as FCDef) (class TC StructureT TMLwP as TCDef) :- std.do! [
+    (class FC StructureF FMLwP) (class TC StructureT TMLwP) :- std.do! [
 
-  acc current (clause _ _ (sub-class FCDef TCDef)),
+  acc current (clause _ _ (sub-class FC TC)),
 
-  term->modname StructureF ModNameF,
-  term->modname StructureT ModNameT,
+  gref->modname StructureF ModNameF,
+  gref->modname StructureT ModNameT,
   CName is ModNameF ^ "_class_to_" ^ ModNameT ^ "_class",
   SName is ModNameF ^ "_to_" ^ ModNameT,
 
@@ -1408,15 +1414,15 @@ declare-coercion SortProjection ClassProjection
   if-verbose (coq.say "HB: declare unification hint" SName),
 
   hb-add-const SName SCoeBody STy @transparent! SC,
-  @global! => coq.coercion.declare (coercion (const SC) 0 {term->gref StructureF} (grefclass {term->gref StructureT})),
+  @global! => coq.coercion.declare (coercion (const SC) 0 StructureF (grefclass StructureT)),
   coq.CS.declare-instance (const SC), % TODO: API in Elpi, take a @constant instead of gref
 ].
 
-pred join-body i:int, i:int, i:term, i:term, i:term, i:term, i:term, i:term,
+pred join-body i:int, i:int, i:structure, i:term, i:term, i:term, i:term, i:term,
   i:list term, i:name, i:term, i:(term -> A), o:term.
 join-body N1 N2 S3 S2_Pack S1_sort S3_to_S1 S2_class S3_to_S2
   P N _Ty _F (fun N S3P Pack) :- !,
-  mk-app S3 P S3P, !,
+  mk-app {coq.env.global S3} P S3P, !,
   coq.mk-n-holes N2 Holes2, !,
   coq.mk-n-holes N1 Holes1, !,
   @pi-decl N S3P s\
@@ -1430,8 +1436,8 @@ join-body N1 N2 S3 S2_Pack S1_sort S3_to_S1 S2_class S3_to_S2
 
 pred declare-join i:class, i:pair class class, o:prop.
 declare-join (class C3 S3 MLwP3) (pr (class C1 S1 _) (class C2 S2 _)) (join C1 C2 C3) :-
-  Name is "join_" ^ {term->modname S3} ^
-    "_between_" ^ {term->modname S1} ^ "_and_" ^ {term->modname S2},
+  Name is "join_" ^ {gref->modname S3} ^
+    "_between_" ^ {gref->modname S1} ^ "_and_" ^ {gref->modname S2},
 
   get-structure-coercion S3 S2 S3_to_S2,
   get-structure-coercion S3 S1 S3_to_S1,
@@ -1493,8 +1499,8 @@ mk-class-field ClassName Params T _ (field _ "class" (app [C|Args]) _\end-record
 
 % Builds the axioms record and the factories from this class to each mixin
 % TODO params
-pred declare-class+structure i:list-w-params mixinname, o:factoryname, o:term, o:term, o:term, o:list prop.
-declare-class+structure MLwP (indt ClassInd) Structure SortProjection ClassProjection AllFactories :- std.do! [
+pred declare-class+structure i:list-w-params mixinname, o:factoryname, o:structure, o:term, o:term, o:list prop.
+declare-class+structure MLwP (indt ClassInd) (indt StructureInd) SortProjection ClassProjection AllFactories :- std.do! [
 
   if-verbose (coq.say "HB: declare axioms record"),
 
@@ -1517,17 +1523,16 @@ declare-class+structure MLwP (indt ClassInd) Structure SortProjection ClassProje
     (mk-class-field (indt ClassInd)) StructureDeclaration,
 
   std.assert-ok! (coq.typecheck-indt-decl StructureDeclaration) "declare-structure: illtyped",
-  coq.env.add-indt StructureDeclaration StructureName,
+  hb-add-indt StructureDeclaration StructureInd,
 
-  coq.CS.canonical-projections StructureName [some SortP, some ClassP],
-  coq.env.global (indt StructureName) Structure,
+  coq.CS.canonical-projections StructureInd [some SortP, some ClassP],
   coq.env.global (const SortP) SortProjection,
   coq.env.global (const ClassP) ClassProjection,
 ].
 
 % Declares "sort" as a coercion Structurename >-> Sortclass
-pred declare-sort-coercion i:term, i:term.
-declare-sort-coercion (global StructureName _) (global Proj _) :-
+pred declare-sort-coercion i:structure, i:term.
+declare-sort-coercion StructureName (global Proj _) :-
 
   if-verbose (coq.say "HB: declare sort coercion"),
 
@@ -1538,15 +1543,14 @@ if-class-already-exists-error _ [] _.
 if-class-already-exists-error N [class _ S ML1wP|CS] ML2 :-
   list-w-params_list ML1wP ML1,
   if (list-eq-set ML1 ML2)
-     (coq.error "Structure" {coq.term->string S} "contains the same mixins of" N)
+     (coq.error "Structure" {nice-gref->string S} "contains the same mixins of" N)
      (if-class-already-exists-error N CS ML2).
 
 pred export-mixin-coercion i:classname, i:option constant.
 export-mixin-coercion _ none.
 export-mixin-coercion ClassName (some C) :-
   coq.env.typeof (const C) _ CTy,
-  safe-dest-app {safe-head CTy} Mixin _,
-  coq.term->gref Mixin MixinGR,
+  head-gref-under-prods CTy MixinGR,
   if-verbose (coq.say "HB: export class to mixin coercion for mixin" {nice-gref->string MixinGR}),
   @global! =>
     coq.coercion.declare (coercion (const C) _ ClassName (grefclass MixinGR)).