diff --git a/.gitignore b/.gitignore index 80a4d7d4..8fdd6bbf 100644 --- a/.gitignore +++ b/.gitignore @@ -58,3 +58,4 @@ _minted-* *.vtc *.dot +config.stamp diff --git a/HB/about.elpi b/HB/about.elpi index 0c2c2806..353043aa 100644 --- a/HB/about.elpi +++ b/HB/about.elpi @@ -3,14 +3,14 @@ namespace about { -pred main i:string. +func main string ->. main S :- coq.locate-all S All, - std.filter All (x\sigma gr a\x = loc-gref gr ; x = loc-abbreviation a) L, + std.filter All (x\sigma gr a\ std.once (x = loc-gref gr ; x = loc-abbreviation a)) L, if (L = []) (coq.error "HB: unable to locate" S) true, std.forall L (about.main-located S). -pred main-located i:string, i:located. +func main-located string, located ->. main-located S (loc-gref GR) :- class-def (class Class GR MLwP), !, private.main-structure S Class GR MLwP. @@ -20,10 +20,10 @@ main-located _ (loc-gref Class) :- class-def (class Class GR MLwP), !, S is M ^ "." ^ St, private.main-structure S Class GR MLwP. -main-located S (loc-gref (indt I)) :- factory-constructor (indt I) _, !, +main-located S (loc-gref (indt I)) :- factory->constructor (indt I) _, !, private.main-factory S I. -main-located S (loc-gref (const C)) :- factory-constructor (const C) _, !, +main-located S (loc-gref (const C)) :- factory->constructor (const C) _, !, private.main-factory-alias S C. main-located S (loc-gref (const C)) :- exported-op M _ C, !, @@ -32,8 +32,8 @@ main-located S (loc-gref (const C)) :- exported-op M _ C, !, main-located S (loc-gref GR) :- factory-alias->gref GR F ok, not (F = GR), !, main-located S (loc-gref F). -main-located S (loc-abbreviation A) :- phant-abbrev GR PhB A, factory-constructor (indt F) GR, !, - private.main-factory-constructor S F PhB GR. +main-located S (loc-abbreviation A) :- phant-abbrev GR PhB A, factory->constructor (indt F) GR, !, + private.main-factory->constructor S F PhB GR. main-located S (loc-abbreviation A) :- coq.notation.abbreviation-body A NArgs _, @@ -61,23 +61,23 @@ main-located S (loc-abbreviation _) :- coq.error "HB: unknown abbreviation" S. shorten coq.pp.{ v , h, hv, hov , spc , str , box , glue , brk , empty }. -pred bulletize1 i:(A -> coq.pp -> prop), i:A, o:coq.pp. +func bulletize1 (func A -> coq.pp), A -> coq.pp. bulletize1 F X (glue [str "- ", M]) :- F X M. -pred bulletize i:list A, i:(A -> coq.pp -> prop), o:coq.pp. -bulletize [] _ empty. +func bulletize list A, (func A -> coq.pp) -> coq.pp. +bulletize [] _ empty :- !. bulletize L F (glue [brk 0 0 | PLB]) :- std.map L (bulletize1 F) PL, std.intersperse (brk 0 0) PL PLB. % Print shortest qualified identifier of the module containing a gref -pred pp-module i:gref, o:coq.pp. +func pp-module gref -> coq.pp. pp-module GR (str ID) :- gref->modname_short GR "." ID. -pred unif-hint? i:cs-instance. +func unif-hint? cs-instance -> . unif-hint? (cs-instance _ (cs-gref GR) _) :- coq.CS.db-for GR _ [_|_]. -pred not1 i:(A -> prop), i:A. +func not1 (pred i:A), A. not1 P X :- not (P X). @@ -89,12 +89,12 @@ namespace private { shorten coq.pp.{ v , h, hv, hov , spc , str , box , glue , brk , empty }. -pred docstring-for-file i:string, o:prop. +func docstring-for-file string -> prop. docstring-for-file Rex (docstring Loc Doc) :- docstring Loc Doc, loc.fields Loc File _ _ _ _, - rex.match {calc(".*" ^ Rex)} File. + rex.match {calc(".*" ^ Rex)} File, !. -pred main-canonical-value i:string, i:list cs-instance. +func main-canonical-value string, list cs-instance ->. main-canonical-value S CanonicalValues :- group-by-loc CanonicalValues CanonicalValuesL, %format @@ -105,14 +105,14 @@ main-canonical-value S CanonicalValues :- coq.say {coq.pp->string PpCanonicalValues}, coq.say. -pred group-by-loc i:list cs-instance, o:list (pair (option loc) (list cs-instance)). +func group-by-loc list cs-instance -> list (pair (option loc) (list cs-instance)). group-by-loc [] []. group-by-loc [cs-instance P V GR|L] [pr (some Loc) [cs-instance P V GR|SameLoc]|Rest1] :- decl-location GR Loc, !, std.partition L (x\ sigma GR1\ x = cs-instance _ _ GR1, decl-location GR1 Loc) SameLoc Rest, group-by-loc Rest Rest1. group-by-loc [I|Rest] [pr none [I]|Rest1] :- group-by-loc Rest Rest1. -pred pp-canonical-solution-list i:pair (option loc) (list cs-instance), o:coq.pp. +func pp-canonical-solution-list pair (option loc) (list cs-instance) -> coq.pp. pp-canonical-solution-list (pr none [CS]) Pp :- pp-canonical-solution CS Pp. pp-canonical-solution-list (pr (some Loc) L) Pp :- @@ -120,14 +120,14 @@ pp-canonical-solution-list (pr (some Loc) L) Pp :- { std.append {std.intersperse spc {std.map L pp-canonical-solution}} [ spc, {pp-loc Loc} ] }. -pred pp-canonical-solution i:cs-instance, o:coq.pp. +func pp-canonical-solution cs-instance -> coq.pp. pp-canonical-solution (cs-instance _Proj _Pat GR) Pp :- coq.env.typeof GR T, coq.prod-tgt->gref T F, if (class-def (class _ F _)) (gref->modname_short F "." ID) (coq.gref->string F ID), Pp = box (hov 0) [ str ID ]. -pred main-canonical-projection i:string, i:gref, i:list cs-instance. +func main-canonical-projection string, gref, list cs-instance. main-canonical-projection S Proj CanonicalProjectionValues :- %format PpCanonicalProjectionOrigin = box (hov 4) [ @@ -141,12 +141,12 @@ main-canonical-projection S Proj CanonicalProjectionValues :- coq.say {coq.pp->string PpCanonicalProjectionValues}, coq.say. -pred pp-canonical-value i:cs-instance, o:coq.pp. +func pp-canonical-value cs-instance -> coq.pp. pp-canonical-value (cs-instance _Proj (cs-gref GR) _Sol) Pp :- coq.term->pp (global GR) V, Pp = box (hov 2) [ V , spc, {pp-loc-of GR} ]. -pred main-coercion i:string, i:list coercion. +func main-coercion string, list coercion. main-coercion S [coercion GR _ Src Tgt|_] :- % format if (class-def (class _ Src _) ; class-def (class Src _ _)) @@ -166,11 +166,11 @@ main-coercion S [coercion GR _ Src Tgt|_] :- coq.say {coq.pp->string PpCoercionOrigin}, coq.say. -pred main-operation i:string, i:mixinname, i:constant. +func main-operation string, mixinname, constant -> . main-operation S MixinSource _ :- % fetch - mixin-first-class MixinSource Class, - class-def (class Class Structure _), + mixin->first-class MixinSource Class, + class-def (class Class Structure _), !, % format PpOriginStructure = box (hov 4) [ str "HB:", spc, str S, spc, str "is an operation of structure", spc, @@ -183,12 +183,12 @@ main-operation S MixinSource _ :- coq.say {coq.pp->string PpOriginMixin}, coq.say. -pred main-structure i:string, i:classname, i:structure, i:mixins. +func main-structure string, classname, structure, mixins. main-structure S Class Structure MLwP :- % fetch list-w-params_list MLwP ML, std.map-filter ML (m\r\ sigma P O OPS\ - mixin-first-class m Class, + mixin->first-class m Class, std.findall (exported-op m P O) OPS, std.map OPS (c\out\ sigma p\ c = exported-op m p out) r) OPLL, std.flatten OPLL Operations, @@ -206,7 +206,7 @@ main-structure S Class Structure MLwP :- PpClass = box (v 4) [ str "HB: ", {pp-module Class}, str " is a factory for the following mixins:", {bulletize ML (m\r\ sigma tmp\ - if (mixin-first-class m Class) + if (mixin->first-class m Class) (pp-module m tmp, r = glue [tmp, str " (* new, not from inheritance *)"]) (pp-module m r))}], PpSubClasses = box (v 4) [ @@ -224,10 +224,10 @@ main-structure S Class Structure MLwP :- print-docstring Structure, coq.say. -pred main-factory-constructor i:string, i:inductive, i:gref, i:gref. -main-factory-constructor S F PhBuild Build :- +func main-factory->constructor string, inductive, gref, gref. +main-factory->constructor S F PhBuild Build :- % fetch - gref-deps Build DMLwP, + gref->deps Build DMLwP, list-w-params_list DMLwP DML, factory-provides (indt F) PMLwP, list-w-params_list PMLwP PML, @@ -263,14 +263,16 @@ main-factory-constructor S F PhBuild Build :- print-docstring Build, coq.say. -pred compute-arg-type i:list-w-params mixinname, i:list constant, i:list term, o:list id, o:id, o:list id, o:list (pair id coq.pp). +func compute-arg-type list-w-params mixinname, list constant, list term -> list id, id, list id, list (pair id coq.pp). compute-arg-type (w-params.cons ID Ty Rest) F Acc [ID|PN] TN FN [pr ID PPTy |Xs] :- coq.term->pp Ty PPTy, @pi-parameter ID Ty x\ compute-arg-type (Rest x) F [x|Acc] PN TN FN Xs. compute-arg-type (w-params.nil ID Ty Rest) F Acc [] ID FN [pr ID PPTy|Xs] :- coq.term->pp Ty PPTy, @pi-parameter ID Ty x\ compute-arg-type.fields F {std.length (Rest x)} {std.rev [x|Acc]} Xs FN. -pred compute-arg-type.fields i:list constant, i:int, i:list term, o:list (pair id coq.pp), o:list id. + +:index(1) +func compute-arg-type.fields list constant, int, list term -> list (pair id coq.pp), list id. compute-arg-type.fields [] _ _ [] []. compute-arg-type.fields [C|Cs] NDeps Args [pr ID PPTy|Xs] [ID|FN] :- exported-op _ C OP, !, coq.env.typeof (const OP) Ty, @@ -291,15 +293,15 @@ compute-arg-type.fields [OP|Cs] NDeps Args [pr ID PPTy|Xs] [ID|FN] :- (@pplevel! 200 => coq.term->pp TyArgsDepsRecord PPTy), @pi-parameter ID TyArgsDepsRecord op\ (pi L L1 X\ - copy (app[global(const OP)|L]) X :- std.drop ToDrop L L1, coq.mk-app op L1 X) => + copy (app[global(const OP)|L]) X :- std.drop ToDrop L L1, coq.mk-app op L1 X, !) => compute-arg-type.fields Cs NDeps Args Xs FN. -pred main-factory i:string, i:inductive. +func main-factory string, inductive. main-factory S Factory :- % fetch coq.env.projections Factory Ps, std.map-filter Ps (x\r\ x = some r) Fields, - gref-deps (indt Factory) DMLwP, + gref->deps (indt Factory) DMLwP, list-w-params_list DMLwP DML, factory-provides (indt Factory) PMLwP, list-w-params_list PMLwP PML, @@ -324,16 +326,16 @@ main-factory S Factory :- print-docstring (indt Factory), coq.say. -pred main-factory-alias i:string, i:constant. +func main-factory-alias string, constant. main-factory-alias S _Const :- coq.say "HB: todo HB.about for factory alias" S. -pred main-builder i:string, i:factoryname, i:mixinname. +func main-builder string, factoryname, mixinname. main-builder _S From To :- coq.say "HB: todo HB.about for builder from" {gref->modname_short From "."} "to" {gref->modname_short To "."}. -pred compute-field-info.aux i:list id, i:list implicit_kind, o:list coq.pp. +func compute-field-info.aux list id, list implicit_kind -> list coq.pp. compute-field-info.aux [] _ []. compute-field-info.aux [Name|NS] [explicit|IS] [str Name|PS] :- compute-field-info.aux NS IS PS. @@ -343,32 +345,34 @@ compute-field-info.aux [Name|NS] [maximal|IS] [glue[str"{",str Name,str"}"]|PS] compute-field-info.aux NS IS PS. compute-field-info.aux [Name|NS] [] [str Name|PS] :- compute-field-info.aux NS [] PS. -pred compute-field-info i:list id, i:list implicit_kind, o:list coq.pp. + +func compute-field-info list id, list implicit_kind -> list coq.pp. compute-field-info Names Impls O :- compute-field-info.aux {std.rev Names} {std.rev Impls} Pp, std.intersperse spc {std.rev Pp} O. -pred pp-const i:constant, o:coq.pp. +func pp-const constant -> coq.pp. pp-const F (str ID) :- coq.gref->id (const F) ID. -pred pp-arg-type i:pair id coq.pp, o:coq.pp. +func pp-arg-type pair id coq.pp -> coq.pp. pp-arg-type (pr ID PPTy) (box (hov 2) [str ID, str" :", spc, PPTy]). -pred pp-if-verbose o:coq.pp, i:(coq.pp -> prop). +:functional +pred pp-if-verbose o:coq.pp, i:(func -> coq.pp). pp-if-verbose V P :- get-option "verbose" tt, !, P V. pp-if-verbose empty _. -pred pp-loc-of i:gref, o:coq.pp. +func pp-loc-of gref -> coq.pp. pp-loc-of GR PP :- decl-location GR Loc, !, pp-loc Loc PP. pp-loc-of _ coq.pp.empty. -pred pp-loc i:loc, o:coq.pp. +func pp-loc loc -> coq.pp. pp-loc Loc (coq.pp.glue PP) :- loc.fields Loc File _ _ Line _, QFile is "\"" ^ File ^ "\", line " ^ {std.any->string Line}, PP = [str "(from ", str QFile, str")"]. -pred docstring->pp i:string, o:coq.pp. +func docstring->pp string -> coq.pp. docstring->pp Txt (glue Doc) :- rex.replace "\n" " " Txt PlainTxt, rex.split " " PlainTxt Words, @@ -376,15 +380,15 @@ docstring->pp Txt (glue Doc) :- std.map NEWords (w\r\ r = str w) PpWords, std.intersperse spc PpWords Doc. -pred docstring-of i:gref, o:option coq.pp. +func docstring-of gref -> option coq.pp. docstring-of GR (some Doc) :- decl-location GR Loc, docstring Loc Txt, !, docstring->pp Txt Doc. docstring-of _ none. -pred pp-docstring-of i:gref, o:coq.pp. +func pp-docstring-of gref -> coq.pp. pp-docstring-of GR D :- docstring-of GR (some D), !. pp-docstring-of _ coq.pp.empty. -pred print-docstring i:gref. +func print-docstring gref ->. print-docstring GR :- if (docstring-of GR (some Doc)) (coq.say {coq.pp->string (box (hov 5) [str"Doc: ",Doc])}) diff --git a/HB/builders.elpi b/HB/builders.elpi index 6606d2ef..831c2efa 100644 --- a/HB/builders.elpi +++ b/HB/builders.elpi @@ -3,8 +3,8 @@ namespace builders { -pred begin i:context-decl. -begin CtxSkel :- std.do! [ +func begin context-decl ->. +begin CtxSkel :- std.assert!(coq.next-synterp-action (begin-module Name)) "synterp code did not open module", if-verbose (coq.say {header} "begin module for builders"), log.coq.env.begin-module Name none, @@ -23,13 +23,13 @@ begin CtxSkel :- std.do! [ log.coq.env.begin-section Name, if-verbose (coq.say {header} "postulating factories"), - builders.private.postulate-factories Name IDF CtxSkel, -]. + builders.private.postulate-factories Name IDF CtxSkel +. } % "end" is a keyword, be put it in the namespace by hand -pred builders.end. +func builders.end. builders.end :- std.do! [ current-mode (builder-from _ _ _ ModName), @@ -68,14 +68,15 @@ builders.end :- std.do! [ /* ----------------------------- private code ------------------------------ */ /* ------------------------------------------------------------------------- */ -pred factory.cdecl->w-mixins i:context-decl, o:w-mixins context-decl. +func factory.cdecl->w-mixins context-decl -> w-mixins context-decl. namespace builders.private { % [declare-1-builder (builder _ F M B) From MoreFrom] Given B of type FB, it % declares all the new builders F to M via B. % From holds the (from F Mi Bi) new clauses during folding. -pred declare-1-builder i:builder, i:list prop, o:list prop. +:index (1) +func declare-1-builder builder, list prop -> list prop. declare-1-builder (builder _ SrcFactory TgtMixin _) FromClauses FromClauses :- (FromClauses => from SrcFactory TgtMixin _), !, if-verbose (coq.say {header} "skipping duplicate builder from" {nice-gref->string SrcFactory} "to" {nice-gref->string TgtMixin}). @@ -85,20 +86,22 @@ declare-1-builder (builder _ SrcFactory TgtMixin B) FromClauses [from SrcFactory % We add breviations for all constants what will be shadowed by projections % if the factory. -pred declare-shadowed-constant i:option constant. +:index (1) +func declare-shadowed-constant option constant ->. declare-shadowed-constant none. declare-shadowed-constant (some C) :- coq.gref->id (const C) Id, std.forall {coq.locate-all Id} (declare-shadowed-located Id). -pred declare-shadowed-located i:string, i:located. +:index (_ 1) +func declare-shadowed-located string, located. declare-shadowed-located Id (loc-gref GR) :- @global! => log.coq.notation.add-abbreviation Id 0 (global GR) ff _. declare-shadowed-located Id (loc-abbreviation Abbrev) :- coq.notation.abbreviation-body Abbrev NArgs T, @global! => log.coq.notation.add-abbreviation Id NArgs T ff _. -pred postulate-factory-abbrev i:term, i:list term, i:id, i:factoryname, o:term. +func postulate-factory-abbrev term, list term, id, factoryname -> term. postulate-factory-abbrev TheType Params Name Falias TheFactory :- std.do! [ std.assert-ok! (factory-alias->gref Falias F) "HB", phant-abbrev F _ Fabv, @@ -110,7 +113,8 @@ postulate-factory-abbrev TheType Params Name Falias TheFactory :- std.do! [ ]. % Only record fields can be exported as operations. -pred define-factory-operations i:term, i:list term, i:term, i:gref. +:index (1) +func define-factory-operations term, list term, term, gref. define-factory-operations TheType Params TheFactory (indt I) :- !, coq.env.indt I _ NIParams _ _ _ _, NHoles is NIParams - 1 - {std.length Params}, @@ -118,7 +122,8 @@ define-factory-operations TheType Params TheFactory (indt I) :- !, std.forall PL (define-factory-operation TheType Params TheFactory NHoles). define-factory-operations _ _ _ _. -pred define-factory-operation i:term, i:list term, i:term, i:int, i:option constant. +:index (_ _ _ _ 1) +func define-factory-operation term, list term, term, int, option constant. define-factory-operation _ _ _ _ none. define-factory-operation TheType Params TheFactory NHoles (some P) :- coq.mk-n-holes NHoles Holes, @@ -129,24 +134,23 @@ define-factory-operation TheType Params TheFactory NHoles (some P) :- coq.gref->id (const P) Name, @local! => log.coq.notation.add-abbreviation Name 0 T ff _. -pred factory i:context-decl, o:string, o:gref. +func factory context-decl -> string, gref. factory (context-item IDF _ T _ _\ context-end) IDF GR :- !, coq.safe-dest-app T (global GR) _. factory (context-item _ _ _ _ R) IDF GR :- !, pi x\ factory (R x) IDF GR. factory _ _ _ :- !, coq.error "the last context item is not a factory". -pred postulate-factories i:id, i:string, i:context-decl. -postulate-factories ModName IDF CDecl :- std.do! [ +func postulate-factories id, string, context-decl. +postulate-factories ModName IDF CDecl :- factory.cdecl->w-mixins CDecl (pr FLwP _), context.declare.params-key FLwP ParamsSection FKey FLwA, std.assert! (FLwA = [triple GRF _ _]) "HB: cannot declare builders for more than one factory at a time", - gref-deps GRF DepswPRaw, + gref->deps GRF DepswPRaw, context.declare.mixins FKey ParamsSection DepswPRaw _ _ _, std.map ParamsSection triple_2 FParams, postulate-factory-abbrev FKey FParams IDF GRF TheFactory, define-factory-operations FKey FParams TheFactory GRF, - acc-clause current (current-mode (builder-from FKey TheFactory GRF ModName)), -]. + acc-clause current (current-mode (builder-from FKey TheFactory GRF ModName)). } \ No newline at end of file diff --git a/HB/common/compat_acc_clauses_all.elpi b/HB/common/compat_acc_clauses_all.elpi index 02ffd758..381970f8 100644 --- a/HB/common/compat_acc_clauses_all.elpi +++ b/HB/common/compat_acc_clauses_all.elpi @@ -1,2 +1,3 @@ -pred acc-clauses i:scope, i:list prop. +:index (1) +func acc-clauses scope, list prop. acc-clauses Scope CL :- coq.elpi.accumulate-clauses Scope "hb.db" {std.map CL (c\r\ r = clause _ _ c)}. diff --git a/HB/common/compat_add_secvar_18_19.elpi b/HB/common/compat_add_secvar_18_19.elpi index 48b80625..c6f2f39e 100644 --- a/HB/common/compat_add_secvar_18_19.elpi +++ b/HB/common/compat_add_secvar_18_19.elpi @@ -1,8 +1,7 @@ -pred log.coq.env.add-section-variable-noimplicits i:id, i:term, o:constant. -log.coq.env.add-section-variable-noimplicits Name Ty C :- std.do! [ +func log.coq.env.add-section-variable-noimplicits id, term -> constant. +log.coq.env.add-section-variable-noimplicits Name Ty C :- if (Name = "_") (ID is "fresh_name_" ^ {std.any->string {new_int}}) (ID = Name), @local! => coq.env.add-section-variable ID Ty C, log.private.log-vernac (log.private.coq.vernac.variable ID Ty), - @local! => log.coq.arguments.set-implicit (const C) [[]], -]. + @local! => log.coq.arguments.set-implicit (const C) [[]]. diff --git a/HB/common/compat_add_secvar_all.elpi b/HB/common/compat_add_secvar_all.elpi index ca5cd454..923a4f70 100644 --- a/HB/common/compat_add_secvar_all.elpi +++ b/HB/common/compat_add_secvar_all.elpi @@ -1,5 +1,5 @@ -pred log.coq.env.add-section-variable-noimplicits i:id, i:term, o:constant. -log.coq.env.add-section-variable-noimplicits Name Ty C :- std.do! [ +func log.coq.env.add-section-variable-noimplicits id, term -> constant. +log.coq.env.add-section-variable-noimplicits Name Ty C :- if (Name = "_") (ID is "fresh_name_" ^ {std.any->string {new_int}}) (ID = Name), % elpi:if version coq-elpi < 2.4.0 @local! => coq.env.add-section-variable ID Ty C, @@ -8,6 +8,5 @@ log.coq.env.add-section-variable-noimplicits Name Ty C :- std.do! [ @local! => coq.env.add-section-variable ID _ Ty C, % elpi:endif log.private.log-vernac (log.private.coq.vernac.variable ID Ty), - @local! => log.coq.arguments.set-implicit (const C) [[]], -]. + @local! => log.coq.arguments.set-implicit (const C) [[]]. diff --git a/HB/common/database.elpi b/HB/common/database.elpi index 425a8b52..38c204b9 100644 --- a/HB/common/database.elpi +++ b/HB/common/database.elpi @@ -5,94 +5,95 @@ shorten coq.{ term->gref, subst-fun, safe-dest-app, mk-app, mk-eta, subst-prod } %%%%%%%%% HB database %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -pred from_factory i:prop, o:factoryname. +func from_factory prop -> factoryname. from_factory (from X _ _) X. -pred from_mixin i:prop, o:mixinname. +func from_mixin prop -> mixinname. from_mixin (from _ X _) X. -pred from_builder i:prop, o:term. +func from_builder prop -> term. from_builder (from _ _ X) (global X). -pred mixin-src_mixin i:prop, o:mixinname. +func mixin-src_mixin prop -> mixinname. mixin-src_mixin (mixin-src _ M _) M. -pred mixin-src_src i:prop, o:term. +func mixin-src_src prop -> term. mixin-src_src (mixin-src _ _ S) S. -pred local-canonical-gref i:prop, o:constant. +func local-canonical-gref prop -> constant. local-canonical-gref (local-canonical C) C. -pred class_name i:class, o:classname. +func class_name class -> classname. class_name (class N _ _) N. -pred class_structure i:class, o:structure. +func class_structure class -> structure. class_structure (class _ S _) S. -pred class-def_name i:prop, o:classname. +func class-def_name prop -> classname. class-def_name (class-def (class N _ _)) N. -pred mixin-class_class i:prop, o:classname. +func mixin-class_class prop -> classname. mixin-class_class (mixin-class _ C) C. -pred mixin-class_mixin i:prop, o:mixinname. +func mixin-class_mixin prop -> mixinname. mixin-class_mixin (mixin-class M _) M. -pred classname->def i:classname, o:class. -classname->def CN (class CN S ML) :- class-def (class CN S ML). +func classname->def classname -> class. +classname->def CN (class CN S ML) :- class-def (class CN S ML), !. -pred classname->mixins i:classname, o:mixins. -classname->mixins CN MLwP :- class-def (class CN _ MLwP). +func classname->mixins classname -> mixins. +classname->mixins CN MLwP :- class-def (class CN _ MLwP), !. -pred module-to-export_module i:prop, o:modpath. +func module-to-export_module prop -> modpath. module-to-export_module (module-to-export _ _ M) M. -pred module-to-export_module-nice i:prop, o:id. +func module-to-export_module-nice prop -> id. module-to-export_module-nice (module-to-export _ M _) M. -pred instance-to-export_instance i:prop, o:constant. +func instance-to-export_instance prop -> constant. instance-to-export_instance (instance-to-export _ _ M) M. -pred instance-to-export_instance-nice i:prop, o:id. +func instance-to-export_instance-nice prop -> id. instance-to-export_instance-nice (instance-to-export _ M _) M. -pred abbrev-to-export_name i:prop, o:id. +func abbrev-to-export_name prop -> id. abbrev-to-export_name (abbrev-to-export _ N _) N. -pred abbrev-to-export_body i:prop, o:term. +func abbrev-to-export_body prop -> term. abbrev-to-export_body (abbrev-to-export _ _ B) (global B). -pred clause-to-export_clause i:prop, o:prop. +func clause-to-export_clause prop -> prop. clause-to-export_clause (clause-to-export _ C) C. -pred extract-builder i:prop, o:builder. +func extract-builder prop -> builder. extract-builder (builder-decl B) B. -pred leq-builder i:builder, i:builder. +func leq-builder builder, builder ->. leq-builder (builder N _ _ _) (builder M _ _ _) :- N =< M. -pred sub-class? i:class, i:class. +func sub-class? class, class ->. sub-class? (class C1 _ ML1P) (class C2 _ ML2P) :- not (C1 = C2), list-w-params_list ML1P ML1, list-w-params_list ML2P ML2, - std.forall ML2 (m2\ std.exists ML1 (m1\ m1 = m2)). + std.forall ML2 (m2\ std.exists! ML1 (m1\ m1 = m2)). % [factory-provides F MLwP] computes the mixins MLwP generated by F -pred factory-provides i:factoryname, o:mixins. +func factory-provides factoryname -> mixins. factory-provides FactoryAlias MLwP :- std.do! [ std.assert-ok! (factory-alias->gref FactoryAlias Factory) "HB", - gref-deps Factory RMLwP, + gref->deps Factory RMLwP, w-params.map RMLwP (factory-provides.base Factory) MLwP ]. -pred mixin->factories i:mixinname, o:list factoryname. +func mixin->factories mixinname -> list factoryname. mixin->factories M FL :- std.do! [ std.findall (from F_ M B_) AllF, std.map AllF from_factory FL ]. -pred factory-provides.base i:factoryname, i:list term, i: term, - i:list (w-args mixinname), o:list (w-args mixinname). +:index(1) +func factory-provides.base factoryname, list term, term, + list (w-args mixinname) -> list (w-args mixinname). factory-provides.base Factory Params T _RMLwP MLwP :- std.do! [ std.findall (from Factory T_ F_) All, std.map All from_mixin ML, @@ -100,19 +101,19 @@ factory-provides.base Factory Params T _RMLwP MLwP :- std.do! [ std.map2 BL ML (factory-provides.one Params T) MLwP, ]. -pred factory-provides.one i:list term, i:term, i:term, i:mixinname, o:w-args mixinname. +func factory-provides.one list term, term, term, mixinname -> w-args mixinname. factory-provides.one Params T B M (triple M PL T) :- std.do! [ std.assert-ok! (coq.typecheck B Ty) "Builder illtyped", subst-prod [T] {subst-prod Params Ty} TyParams, std.assert! (extract-conclusion-params T TyParams PL) "The conclusion of a builder is a mixin whose parameters depend on other mixins", ]. -pred extract-conclusion-params i:term, i:term, o:list term. +func extract-conclusion-params term, term -> list term. extract-conclusion-params TheType (prod _ S T) R :- !, @pi-decl _ S x\ extract-conclusion-params TheType (T x) R. extract-conclusion-params TheType (app [global GR|Args]) R :- !, std.do! [ std.assert-ok! (factory-alias->gref GR Factory) "HB", - factory-nparams Factory NP, + factory->nparams Factory NP, std.map Args (copy-pack-holes TheType TheType) NewArgs, std.take NP NewArgs R]. extract-conclusion-params TheType T R :- whd1 T T1, !, extract-conclusion-params TheType T1 R. @@ -123,31 +124,28 @@ extract-conclusion-params TheType T R :- whd1 T T1, !, extract-conclusion-params % cons tp p\ nil t\ [pr f1 [p,t]] % f1 p t = m1 t, m2 p t % cons tp p\ nil t\ [pr m1 [t], pr m2 [p,t]] -pred factories-provide i:list-w-params factoryname, o:mixins. -factories-provide FLwP MLwP :- std.do! [ +func factories-provide list-w-params factoryname -> mixins. +factories-provide FLwP MLwP :- list-w-params.flatten-map FLwP factory-provides UnsortedMLwP, - w-params.map UnsortedMLwP (p\t\ toposort-mixins) MLwP, -]. + w-params.map UnsortedMLwP (p\t\ toposort-mixins) MLwP. -pred undup-grefs i:list gref, o:list gref. -undup-grefs L UL :- std.do! [ +func undup-grefs list gref -> list gref. +undup-grefs L UL :- coq.gref.list->set L S, - coq.gref.set.elements S UL, -]. + coq.gref.set.elements S UL. -pred undup-sorts i:list sort, o:list sort. -undup-sorts L R :- std.do! [ +func undup-sorts list sort -> list sort. +undup-sorts L R :- if (std.mem L prop) (R1 = [prop]) (R1 = []), if (std.mem L sprop) (R2 = [sprop]) (R2 = []), if (std.mem L (typ _)) (R3 = [typ _]) (R3 = []), - std.flatten [R1, R2, R3] R, -]. + std.flatten [R1, R2, R3] R. % also prunes cs-default -pred undup-cs-patterns i:list cs-pattern, o:list cs-pattern. -undup-cs-patterns L R :- std.do! [ +func undup-cs-patterns list cs-pattern -> list cs-pattern. +undup-cs-patterns L R :- std.map-filter L (x\r\ x = cs-gref r) LGR, undup-grefs LGR ULGR, std.map ULGR (x\r\ r = cs-gref x) R1, @@ -158,40 +156,38 @@ undup-cs-patterns L R :- std.do! [ if (std.mem L cs-prod) (R3 = [cs-prod]) (R3 = []), - std.flatten [R1, R2, R3] R, -]. + std.flatten [R1, R2, R3] R. % Mixins can be topologically sorted according to their dependencies -pred toposort-mixins i:list (w-args mixinname), o:list (w-args mixinname). -toposort-mixins In Out :- std.do! [ +func toposort-mixins list (w-args mixinname) -> list (w-args mixinname). +toposort-mixins In Out :- std.map In triple_1 ML, - std.map ML (m\r\sigma D D1\ gref-deps m D1, list-w-params_list D1 D, std.map D (d\r\r = pr d m) r) ES2, + std.map ML (m\r\sigma D D1\ gref->deps m D1, list-w-params_list D1 D, std.map D (d\r\r = pr d m) r) ES2, std.flatten ES2 ES, - toposort-proj triple_1 ES In Out, -]. + toposort-proj triple_1 ES In Out. -pred toposort-proj i:(A -> gref -> prop), i:list (pair gref gref), i:list A, o:list A. +func toposort-proj (func A -> gref), list (pair gref gref), list A -> list A. toposort-proj Proj ES In Out :- !, toposort-proj.acc Proj ES [] In Out. -pred topo-find i:B, o:A. -pred toposort-proj.acc i:(A -> gref -> prop), i:list (pair gref gref), i:list gref, i:list A, o:list A. +func topo-find B -> A. +func toposort-proj.acc (pred i:A, o:gref), list (pair gref gref), list gref, list A -> list A. toposort-proj.acc _ ES Acc [] Out :- !, - std.map {std.gref.toposort ES Acc} topo-find Out. + std.map {std.gref.toposort ES Acc} topo-find Out, !. toposort-proj.acc Proj ES Acc [A|In] Out :- std.do![ Proj A B, topo-find B A => toposort-proj.acc Proj ES [B|Acc] In Out ]. % Classes can be topologically sorted according to the subclass relation -pred toposort-classes.mk-class-edge i:prop, o:pair classname classname. +func toposort-classes.mk-class-edge prop -> pair classname classname. toposort-classes.mk-class-edge (sub-class C1 C2 _ _) (pr C2 C1). -pred toposort-classes i:list classname, o:list classname. +func toposort-classes list classname -> list classname. toposort-classes In Out :- std.do! [ std.findall (sub-class C1_ C2_ _ _) SubClasses, std.map SubClasses toposort-classes.mk-class-edge ES, std.gref.toposort ES In Out, ]. -pred findall-classes o:list class. +func findall-classes -> list class. findall-classes CLSortedDef :- std.do! [ std.findall (class-def C_) All, std.map All class-def_name CL, @@ -199,8 +195,8 @@ findall-classes CLSortedDef :- std.do! [ std.map CLSorted classname->def CLSortedDef, ]. -pred findall-classes-for.unsorted - i:list mixinname, i:list classname, o:list classname. +func findall-classes-for.unsorted + list mixinname, list classname -> list classname. findall-classes-for.unsorted [] CL CL :- !. findall-classes-for.unsorted [M|ML] CLAcc Out :- std.do! [ std.findall (mixin-class M C_) All, @@ -208,30 +204,39 @@ findall-classes-for.unsorted [M|ML] CLAcc Out :- std.do! [ findall-classes-for.unsorted ML {std.append CL CLAcc} Out ]. -pred findall-classes-for i:list mixinname, o:list class. +func findall-classes-for list mixinname -> list class. findall-classes-for ML CLSortedDef :- std.do! [ findall-classes-for.unsorted ML [] CL, toposort-classes CL CLSorted, std.map CLSorted classname->def CLSortedDef, ]. -pred findall-builders o:list builder. +func findall-builders -> list builder. findall-builders LFIL :- std.map {std.findall (builder-decl B_)} extract-builder LFILunsorted, std.bubblesort LFILunsorted leq-builder LFIL. -pred findall-has-mixin-instance i:cs-pattern, o:list prop. +func findall-has-mixin-instance cs-pattern -> list prop. findall-has-mixin-instance P CL :- std.findall (has-mixin-instance P _ _) CL. -pred has-mixin-instance_key i:prop, o:cs-pattern. +func has-mixin-instance_key prop -> cs-pattern. has-mixin-instance_key (has-mixin-instance P _ _) P. -pred findall-mixin-src i:term, o:list mixinname. +func findall-mixin-src term -> list mixinname. findall-mixin-src T ML :- std.map {std.findall (mixin-src T M_ V_)} mixin-src_mixin ML. -pred findall-local-canonical o:list constant. +func findall-factory->constructor -> list prop. +findall-factory->constructor L :- + std.map {std.findall (findall-factory->constructor.aux _)} findall-factory->constructor.make L. +func findall-factory->constructor.aux -> prop. +findall-factory->constructor.aux (factory->constructor F C) :- + is-factory F, !, factory->constructor F C. +func findall-factory->constructor.make prop -> prop. +findall-factory->constructor.make (findall-factory->constructor.aux P) P. + +func findall-local-canonical -> list constant. findall-local-canonical CL :- std.map {std.findall (local-canonical C_)} local-canonical-gref CL. @@ -279,21 +284,21 @@ assert-building-bottom-up CurrentClass C3n C1n C2n :- Msg2) true. -pred distinct-pairs_pair i:prop, o:pair class class. +func distinct-pairs_pair prop -> pair class class. distinct-pairs_pair (distinct-pairs-below _ _ X Y) (pr X Y). -pred findall-newjoins i:class, i:list class, o:list (pair class class). +func findall-newjoins class, list class -> list (pair class class). findall-newjoins CurrentClass AllSuper TodoJoins :- std.findall (distinct-pairs-below CurrentClass AllSuper C1_ C2_) JoinOf, std.map JoinOf distinct-pairs_pair TodoJoins. -pred class-coverage i:list classname, o:coq.gref.set. +func class-coverage list classname -> coq.gref.set. class-coverage CNL CSet :- std.map CNL classname->mixins CMLLwP, std.map CMLLwP list-w-params_list CMLL, coq.gref.list->set {std.flatten CMLL} CSet. -pred assert-good-coverage! i:list mixinname, i:list classname. +func assert-good-coverage! list mixinname, list classname ->. assert-good-coverage! MLSortedRev CNL :- std.do! [ coq.gref.list->set MLSortedRev MLSet, class-coverage CNL CMLSet, @@ -310,46 +315,46 @@ assert-good-coverage! MLSortedRev CNL :- std.do! [ %%%%% Coq Database %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % [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. +func get-structure-coercion structure, structure -> term. get-structure-coercion S T (global F) :- coq.coercion.db-for (grefclass S) (grefclass T) L, if (L = [pr F _]) true (coq.error "No one step coercion from" S "to" T). -pred get-structure-sort-projection i:structure, o:term. +func get-structure-sort-projection structure -> term. get-structure-sort-projection (indt S) Proj :- !, coq.env.projections S L, if (L = [some P, _]) true (coq.error "No canonical sort projection for" S), Proj = global (const P). get-structure-sort-projection S _ :- coq.error "get-structure-sort-projection: not a structure" S. -pred get-structure-class-projection i:structure, o:term. +func get-structure-class-projection structure -> term. get-structure-class-projection (indt S) T :- !, coq.env.projections S L, if (L = [_, some P]) true (coq.error "No canonical class projection for" S), T = global (const P). get-structure-class-projection S _ :- coq.error "get-structure-class-projection: not a structure" S. -pred get-constructor i:gref, o:gref. +func get-constructor gref -> 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. % finding for locally defined structures -pred get-cs-structure i:cs-instance, o:structure. +func get-cs-structure cs-instance -> structure. get-cs-structure (cs-instance _ _ (const Inst)) Struct :- std.do! [ coq.env.typeof (const Inst) InstTy, coq.prod-tgt->gref InstTy Struct, is-structure Struct, ]. -pred get-cs-instance i:cs-instance, o:constant. +func get-cs-instance cs-instance -> constant. get-cs-instance (cs-instance _ _ (const Inst)) Inst. -pred has-cs-instance i:gref, i:cs-instance. +func has-cs-instance gref, cs-instance ->. has-cs-instance GTy (cs-instance _ (cs-gref GTy) _). -pred mixin-src->has-mixin-instance i:prop, o:prop. +func mixin-src->has-mixin-instance prop -> prop. mixin-src->has-mixin-instance (mixin-src (global GR) M I) (has-mixin-instance (cs-gref GR) M IHd) :- term->gref I IHd. @@ -365,13 +370,13 @@ mixin-src->has-mixin-instance (mixin-src (sort U) M I) (has-mixin-instance (cs-s % this auxiliary function iterates over the list of arguments of an application, % and create the necessary unify condition for each arguments % and at the end returns the mixin-src clause with all the conditions -pred mixin-instance-type->mixin-src.aux - i:list term, % list of arguments - i:term, % head of the original application - i:mixinname, % name of mixin - i:term, % instance body - i:list prop, % Cond list - o:prop. +func mixin-instance-type->mixin-src.aux + list term, % list of arguments + term, % head of the original application + mixinname, % name of mixin + term, % instance body + list prop % Cond list + -> prop. mixin-instance-type->mixin-src.aux [] T M I Cond (mixin-src T M I :- Cond). mixin-instance-type->mixin-src.aux [A|Args] T M I Cond (pi a \ C a) :- pi a \ @@ -382,12 +387,13 @@ mixin-instance-type->mixin-src.aux [A|Args] T M I Cond (pi a \ C a) :- % transforms the type of a mixin instance into a % mixin-src clause with eventual conditions regarding its parameters -pred mixin-instance-type->mixin-src - i:term, % type of the instance Ty - i:mixinname, % name of mixin - i:term, % instance body I of type Ty - i:list prop, % Cond list - o:prop. +:index (1) +func mixin-instance-type->mixin-src + term, % type of the instance Ty + mixinname, % name of mixin + term, % instance body I of type Ty + list prop % Cond list + -> prop. mixin-instance-type->mixin-src (app _ as F) M I Cond C :- factory? F (triple _ _ Subject), @@ -400,46 +406,44 @@ mixin-instance-type->mixin-src (prod N_ _ F) M I Cond (pi a \ C a) :- coq.mk-app I [a] Ia, mixin-instance-type->mixin-src (F a) M Ia Cond (C a). -pred has-mixin-instance->mixin-src i:prop, o:prop. +func has-mixin-instance->mixin-src prop -> prop. has-mixin-instance->mixin-src (has-mixin-instance _ M IHd) C :- std.do![ T = global IHd, coq.env.typeof IHd Ty, mixin-instance-type->mixin-src Ty M T [] C, ]. -pred get-canonical-structures i:term, o:list structure. +func get-canonical-structures term -> list structure. get-canonical-structures TyTrm StructL :- std.do! [ term->cs-pattern TyTrm Pat, !, coq.CS.db-for _ Pat DBGTyL, std.map-filter DBGTyL get-cs-structure StructL, ]. -pred get-canonical-instances i:term, o:list constant. -get-canonical-instances TyTrm StructL :- std.do! [ - term->cs-pattern TyTrm Pat, !, +func get-canonical-instances term -> list constant. +get-canonical-instances TyTrm StructL :- + term->cs-pattern TyTrm Pat, coq.CS.db-for _ Pat DBGTyL, - std.map-filter DBGTyL get-cs-instance StructL, -]. + std.map-filter DBGTyL get-cs-instance StructL. -pred has-CS-instance? i:term, i:structure. -has-CS-instance? TyTerm (indt Struct) :- std.do! [ +func has-CS-instance? term, structure ->. +has-CS-instance? TyTerm (indt Struct) :- term->cs-pattern TyTerm Pat, coq.env.projections Struct [some Proj, _], coq.CS.db-for (const Proj) Pat L, - not(L = []) -]. + not(L = []). -pred structure-nparams i:structure, o:int. +func structure-nparams structure -> int. structure-nparams Structure NParams :- - class-def (class Class Structure _), - factory-nparams Class NParams. + class-def (class Class Structure _), !, + factory->nparams Class NParams. -pred factory? i:term, o:w-args factoryname. +func factory? term -> w-args factoryname. factory? S (triple F Params T) :- not (var S), !, safe-dest-app S (global GR) Args, factory-alias->gref GR F ok, - factory-nparams F NP, !, + factory->nparams F NP, !, std.split-at NP Args Params [T|_]. % [find-max-classes Mixins Classes] states that Classes is a list of classes @@ -451,7 +455,7 @@ factory? S (triple F Params T) :- pred find-max-classes i:list mixinname, o:list classname. find-max-classes [] []. find-max-classes [M|Mixins] [C|Classes] :- - mixin-first-class M C, + mixin->first-class M C, std.do! [ class-def (class C _ MLwP), list-w-params_list MLwP ML, diff --git a/HB/common/log.elpi b/HB/common/log.elpi index 134f9eec..6f123d15 100644 --- a/HB/common/log.elpi +++ b/HB/common/log.elpi @@ -10,25 +10,26 @@ namespace log.coq { -pred arguments.set-implicit i:gref, i:list (list implicit_kind). -arguments.set-implicit GR I :- std.do! [ +:index (1) +func arguments.set-implicit gref, list (list implicit_kind). +arguments.set-implicit GR I :- coq.arguments.set-implicit GR I, if (@local!) (Local = tt) (Local = ff), - log.private.log-vernac (log.private.coq.vernac.implicit Local {coq.gref->id GR} I), -]. + log.private.log-vernac (log.private.coq.vernac.implicit Local {coq.gref->id GR} I). -pred env.add-location i:gref. +func env.add-location gref ->. env.add-location GR :- if (get-option "elpi.loc" Loc) % remove when coq-elpi > 1.9 (acc-clause library (decl-location GR Loc)) true. -pred strategy.set i:list constant, i:conversion_strategy. +func strategy.set list constant, conversion_strategy ->. strategy.set CL S :- coq.strategy.set CL S, log.private.log-vernac (log.private.coq.vernac.strategy CL S). -pred env.add-const-noimplicits i:id, i:term, i:term, i:opaque?, o:constant. +:index (1) +func env.add-const-noimplicits id, term, term, opaque? -> constant. env.add-const-noimplicits Name Bo Ty Opaque C :- std.do! [ if (not(ground_term Ty ; ground_term Bo)) (coq.error "HB: cannot infer some information in" Name @@ -42,7 +43,8 @@ env.add-const-noimplicits Name Bo Ty Opaque C :- std.do! [ @local! => arguments.set-implicit (const C) [[]], ]. -pred env.add-const i:id, i:term, i:term, i:opaque?, o:constant. +:index (1) +func env.add-const id, term, term, opaque? -> constant. env.add-const Name Bo Ty Opaque C :- std.do! [ if (not(ground_term Ty ; ground_term Bo)) (coq.error "HB: cannot infer some information in" Name @@ -55,7 +57,7 @@ env.add-const Name Bo Ty Opaque C :- std.do! [ log.private.log-vernac (log.private.coq.vernac.definition Name1 Ty? Bo), ]. -pred env.add-const-noimplicits-failondup i:id, i:term, i:term, i:opaque?, o:constant. +func env.add-const-noimplicits-failondup id, term, term, opaque? -> constant. env.add-const-noimplicits-failondup Name Bo Ty Opaque C :- std.do! [ if (not(ground_term Ty ; ground_term Bo)) (coq.error "HB: cannot infer some information in" Name @@ -68,13 +70,13 @@ env.add-const-noimplicits-failondup Name Bo Ty Opaque C :- std.do! [ @local! => arguments.set-implicit (const C) [[]], ]. -pred env.add-parameter i:id, i:term, o:constant. +func env.add-parameter id, term -> constant. env.add-parameter ID Ty C :- std.do! [ @global! => coq.env.add-axiom ID Ty C, log.private.log-vernac (log.private.coq.vernac.parameter ID Ty), ]. -pred env.add-indt i:indt-decl, o:inductive. +func env.add-indt indt-decl -> inductive. env.add-indt Decl I :- std.do! [ if (not(coq.ground-indt-decl? Decl)) (coq.error "HB: cannot infer some information in" {coq.indt-decl->string Decl}) @@ -92,64 +94,63 @@ env.add-indt Decl I :- std.do! [ (p\ sigma c\ if (p = some c) (env.add-location (const c), log.private.log-implicits-of ff (const c)) true), ]. -pred env.begin-module i:id, i:option (pair modtypath id). -env.begin-module Name none :- std.do! [ +:index (_ 1) +func env.begin-module id, option (pair modtypath id) . +env.begin-module Name none :- coq.env.begin-module Name none, - log.private.log-vernac (log.private.coq.vernac.begin-module Name none), -]. + log.private.log-vernac (log.private.coq.vernac.begin-module Name none). env.begin-module Name (some (pr Sig SigName)) :- std.do! [ coq.env.begin-module Name (some Sig), log.private.log-vernac (log.private.coq.vernac.begin-module Name (some SigName)), ]. -pred env.begin-module-type i:id. +func env.begin-module-type id ->. env.begin-module-type Name :- std.do! [ coq.env.begin-module-type Name, log.private.log-vernac (log.private.coq.vernac.begin-module-type Name), ]. -pred env.end-module-name i:id, o:modpath. -env.end-module-name Name M :- std.do! [ +func env.end-module-name id -> modpath. +env.end-module-name Name M :- coq.env.end-module M, - log.private.log-vernac (log.private.coq.vernac.end-module Name), -]. -pred env.end-module-type-name i:id, o:modtypath. + log.private.log-vernac (log.private.coq.vernac.end-module Name). + +func env.end-module-type-name id -> modtypath. env.end-module-type-name Name M :- std.do! [ coq.env.end-module-type M, log.private.log-vernac (log.private.coq.vernac.end-module-type Name), ]. -pred env.begin-section i:id. +func env.begin-section id ->. env.begin-section Name :- std.do! [ coq.env.begin-section Name, log.private.log-vernac (log.private.coq.vernac.begin-section Name), ]. -pred env.end-section-name i:id. +func env.end-section-name id. env.end-section-name Name :- std.do! [ coq.env.end-section, log.private.log-vernac (log.private.coq.vernac.end-section Name), ]. -pred notation.add-abbreviation i:id, i:int, i:term, i:bool, o:abbreviation. -notation.add-abbreviation Name NArgs Body OnlyParsing O :- std.do! [ +func notation.add-abbreviation id, int, term, bool -> abbreviation. +notation.add-abbreviation Name NArgs Body OnlyParsing O :- coq.notation.add-abbreviation Name NArgs Body OnlyParsing O, - log.private.log-vernac (log.private.coq.vernac.abbreviation Name NArgs Body), -]. + log.private.log-vernac (log.private.coq.vernac.abbreviation Name NArgs Body). -pred env.export-module i:id, i:modpath. +func env.export-module id, modpath ->. env.export-module MPNice M :- std.do! [ coq.env.export-module M, log.private.log-vernac (log.private.coq.vernac.export-module MPNice), ]. -pred env.import-module i:id, i:modpath. +func env.import-module id, modpath ->. env.import-module MPNice M :- std.do! [ coq.env.import-module M, log.private.log-vernac (log.private.coq.vernac.import-module MPNice), ]. -pred coercion.declare i:coercion. +func coercion.declare coercion -> . coercion.declare C :- std.do! [ @global! => @reversible! => coq.coercion.declare C, C = coercion GR _ SRCGR TGTCL, @@ -162,7 +163,7 @@ coercion.declare C :- std.do! [ % Since CS.foo is not a valid predicate name we can't use it % in the namespace, so we just define it here with the full name -pred log.coq.CS.declare-instance i:constant. +func log.coq.CS.declare-instance constant ->. log.coq.CS.declare-instance C :- std.do! [ if (@local!) (Local = tt) (Local = ff), coq.CS.declare-instance (const C), @@ -173,22 +174,22 @@ log.coq.CS.declare-instance C :- std.do! [ log.private.log-vernac (log.private.coq.vernac.canonical Name Local), ]. -pred log.coq.check i:term, o:term, o:term, o:diagnostic. +func log.coq.check term -> term, term, diagnostic. log.coq.check Skel Ty T D :- std.do! [ coq.elaborate-skeleton Skel Ty T D, if (get-option "fail" tt) (Fail = tt) (Fail = ff), log.private.log-vernac (log.private.coq.vernac.check Skel Fail), ]. -pred refine i:term, i:goal, o:list sealed-goal. % to silence a warning, since this is only in tactics -pred log.refine i:term, i:goal, o:list sealed-goal. +func refine term, goal -> list sealed-goal. % to silence a warning, since this is only in tactics +func log.refine term, goal -> list sealed-goal. log.refine T G GL :- std.do! [ refine T G GL, G = goal _ _ _ Solution _, log.private.log-tactic Solution, ]. -pred refine.no_check i:term, i:goal, o:list sealed-goal. % to silence a warning, since this is only in tactics -pred log.refine.no_check i:term, i:goal, o:list sealed-goal. +func refine.no_check term, goal -> list sealed-goal. % to silence a warning, since this is only in tactics +func log.refine.no_check term, goal -> list sealed-goal. log.refine.no_check T G GL :- std.do! [ refine.no_check T G GL, G = goal _ _ _ Solution _, @@ -200,7 +201,7 @@ namespace log.private { %%%%% Logging Utils %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -pred log-implicits-of i:bool, i:gref. +func log-implicits-of bool, gref -> . log-implicits-of Local GR :- coq.arguments.implicit GR I, if (std.forall I (i\ std.forall i (x\ x = explicit))) (IMP = [[]]) (IMP = I), @@ -239,9 +240,9 @@ type coq.vernac.strategy list constant -> conversion_strategy -> coq.vernac } -pred with-logging i:prop. -pred log.private.log-vernac i:log.private.coq.vernac. -pred log.private.log-tactic i:term. +func with-logging (func) ->. +func log.private.log-vernac log.private.coq.vernac ->. +func log.private.log-tactic term ->. /* Hierarchy Builder: algebraic hierarchies made easy This software is released under the terms of the MIT license */ @@ -249,7 +250,7 @@ pred log.private.log-tactic i:term. % implementation of logging and vernac printing with-logging P :- (get-option "elpi.hb.log" _, NICE = tt ; get-option "elpi.hb.log.raw" _, NICE = ff), !, - get-option "elpi.loc" Loc, + get-option "elpi.loc" Loc, !, loc.fields Loc FILE Start Stop _ _, LocStr is "characters " ^ {std.any->string Start} ^ "-" ^ {std.any->string Stop}, FILENAME is FILE ^ ".hb", @@ -297,21 +298,22 @@ namespace log.private { pred logger o:list coq.pp, o:bool. -pred logger-extend i:list coq.pp, i:coq.pp. +:index (1) +func logger-extend list coq.pp, coq.pp ->. logger-extend [] _ :- coq.error "HB: logger was closed". logger-extend (uvar as X) V :- X = [V|FRESH_]. logger-extend [_|XS] V :- logger-extend XS V. -pred logger-close i:list coq.pp. +func logger-close list coq.pp ->. logger-close (uvar as X) :- X = []. logger-close [_|XS] :- logger-close XS. -pred coq.vernac->pp i:list coq.vernac, o:coq.pp. +func coq.vernac->pp list coq.vernac -> coq.pp. coq.vernac->pp L (box (v 0) L2) :- std.map L coq.vernac->pp1 L1, std.intersperse spc L1 L2. -pred coq.vernac->pp1 i:coq.vernac, o:coq.pp. +func coq.vernac->pp1 coq.vernac -> coq.pp. coq.vernac->pp1 (begin-module Name none) PP :- PP = box h [str "Module ", str Name, str "."]. coq.vernac->pp1 (begin-module Name (some TyName)) PP :- @@ -355,7 +357,7 @@ coq.vernac->pp1 (vernac.inductive I Primitive) (glue [str Start, PP, str Stop]) if (Primitive = tt) (Start = "Set Primitive Projections. ", Stop = "Unset Primitive Projections. ") (Start = "", Stop = ""). -coq.vernac->pp1 (vernac.implicit Local Name [[]]) (box h [Locality, str "Arguments ", str Name, str " : clear implicits."]) :- local->locality Local Locality. +coq.vernac->pp1 (vernac.implicit Local Name [[]]) (box h [Locality, str "Arguments ", str Name, str " : clear implicits."]) :- !, local->locality Local Locality. coq.vernac->pp1 (vernac.implicit Local Name [L]) (box h [Locality, str "Arguments ", str Name, spc, glue PP, str "."]) :- local->locality Local Locality, std.map L coq.vernac->ppimparg PP1, @@ -373,20 +375,21 @@ coq.vernac->pp1 (strategy L (level N)) (box (hov 2) [str"Strategy ",str NPP,str" std.any->string N NPP, std.map L (c\r\sigma id\coq.gref->id (const c) id, r = str id) LID, std.intersperse spc LID PPL. -pred local->locality i:bool, o:coq.pp. +func local->locality bool -> coq.pp. local->locality tt (str "Local "). local->locality ff (str "Global "). -pred fail->failure i:bool, o:coq.pp. +func fail->failure bool -> coq.pp. fail->failure tt (str "Fail "). fail->failure ff (str ""). -pred coq.vernac->ppimparg i:implicit_kind, o:coq.pp. +func coq.vernac->ppimparg implicit_kind -> coq.pp. coq.vernac->ppimparg explicit (str "_"). coq.vernac->ppimparg maximal (str "{_}"). coq.vernac->ppimparg implicit (str "[_]"). -pred coq.vernac->ppinductive i:indt-decl, i:list (pair implicit_kind term), o:coq.pp. +:index (3) +func coq.vernac->ppinductive indt-decl, list (pair implicit_kind term) -> coq.pp. coq.vernac->ppinductive (parameter ID IMPL TY I) Acc R :- @pi-parameter ID TY p\ coq.vernac->ppinductive (I p) [pr IMPL p|Acc] R. coq.vernac->ppinductive (record ID SORT KID RD) ParamsRev (box (v 0) [Hack1, PP, Hack2]) :- @@ -420,14 +423,14 @@ coq.vernac->ppinductive (inductive ID IsInd Arity Ks) ParamsRev PP :- coq.mk-app x ParamsAsArgs (X x), coq.vernac->ppinductiveconstructor (Ks (X x)) KsPp. -pred coq.vernac->ppinductiveconstructor i:list indc-decl, o:list coq.pp. +func coq.vernac->ppinductiveconstructor list indc-decl -> list coq.pp. coq.vernac->ppinductiveconstructor [] []. coq.vernac->ppinductiveconstructor [constructor ID Arity|Ks] PP :- PP = [str ID,{coq.arity->pp Arity},SEP|Rest], if (Ks = []) (SEP = str"") (SEP = glue [brk 1 0, str "| "]), coq.vernac->ppinductiveconstructor Ks Rest. -pred coq.vernac->ppinductiveparams i:list (pair implicit_kind term), o:list coq.pp. +func coq.vernac->ppinductiveparams list (pair implicit_kind term) -> list coq.pp. coq.vernac->ppinductiveparams [] []. coq.vernac->ppinductiveparams [pr Imp T|Rest] PP :- PP = [box (hov 2) [str A,ID,str " : ", TY,str B]|PPRest], @@ -437,13 +440,14 @@ coq.vernac->ppinductiveparams [pr Imp T|Rest] PP :- (A = "[", B = "]"), coq.vernac->ppinductiveparams Rest PPRest. -pred coq.vernac->pprecordfields i:record-decl, o:list coq.pp. +func coq.vernac->pprecordfields record-decl -> list coq.pp. coq.vernac->pprecordfields end-record []. coq.vernac->pprecordfields (field _ ID TY F) [ str ID, str " : ", TYPP, str ";", spc|FPP] :- % TODO attributes coq.term->pp TY TYPP, @pi-parameter ID TY p\ coq.vernac->pprecordfields (F p) FPP. -pred coq.vernac->ppabbrterm i:int, i:term, o:list coq.pp, o:coq.pp. +:index (1 1) +func coq.vernac->ppabbrterm int, term -> list coq.pp, coq.pp. coq.vernac->ppabbrterm 0 T [] B :- !, @holes! => coq.term->pp T B. coq.vernac->ppabbrterm N (fun _ _ F) [spc,str ID|StrParams] B :- ID is "X" ^ {std.any->string N}, diff --git a/HB/common/phant-abbreviation.elpi b/HB/common/phant-abbreviation.elpi index 943c30c7..1a4ddf94 100644 --- a/HB/common/phant-abbreviation.elpi +++ b/HB/common/phant-abbreviation.elpi @@ -19,7 +19,7 @@ namespace phant { % [add-abbreviation Name PhT C A] builds a definition "phant_Name" for the % term T and an abbreviation Name as per Ph. % Use the API below to build a PhT as you like. -pred add-abbreviation i:string, i:phant-term, o:constant, o:abbreviation. +func add-abbreviation string, phant-term -> constant, abbreviation. add-abbreviation N (private.phant-term AL T1) C Abbrev :- std.do! [ NC is "phant_" ^ N, std.assert-ok! (coq.elaborate-skeleton T1 TTy T) "add-abbreviation: T illtyped", @@ -35,9 +35,9 @@ add-abbreviation N (private.phant-term AL T1) C Abbrev :- std.do! [ % pass (instead of being inferred) % If WithCopy = tt, an extra argument is added after all the parameters % and before the source keu to replace the target key by a user chosen one. -pred of-gref i:bool, i:gref, i:list mixinname, o:phant-term. +func of-gref bool, gref, list mixinname -> phant-term. of-gref WithCopy GRF RealMixinArgs PhBody:- !, std.do! [ - std.assert! (gref-deps GRF MLwP) "mk-phant-term: unknown gref", + std.assert! (gref->deps GRF MLwP) "mk-phant-term: unknown gref", std.assert! (coq.env.typeof GRF FTy) "mk-phant-term: F illtyped", coq.mk-eta (-1) FTy (global GRF) EtaF, % toposort-mixins ML MLSorted, @@ -59,16 +59,16 @@ of-gref WithCopy GRF RealMixinArgs PhBody:- !, std.do! [ % API à la carte: start with a term and wrap it up ------------------------- % A term with no phantom arguments -pred init i:term, o:phant-term. +func init term -> phant-term. init T (private.phant-term [] T). % [fun-real N T Ph Ph1] Adds a real argument named N of type T around Ph -pred fun-real i:name, i:term, i:(term -> phant-term), o:phant-term. +func fun-real name, term, (term -> phant-term) -> phant-term. fun-real N T F Res :- !, private.phant-fun (private.real N) T F Res. % [fun-unify Msg X1 X2 Ph Ph1] Adds an argument that will foce the unification % of X1 with X2 and print Msg is case of error around Ph -pred fun-unify i:option term, i:term, i:term, i:phant-term, o:phant-term. +func fun-unify option term, term, term, phant-term -> phant-term. fun-unify OMsg X1 X2 (private.phant-term AL F) (private.phant-term [private.unify|AL] UF) :- std.assert-ok! (coq.typecheck X1 T1) "fun-unify: X1 illtyped", std.assert-ok! (coq.typecheck X2 T2) "fun-unify: X2 illtyped", @@ -76,14 +76,14 @@ fun-unify OMsg X1 X2 (private.phant-term AL F) (private.phant-term [private.unif UF = {{fun unif_arbitrary : lib:hb.unify lp:T1 lp:T2 lp:X1 lp:X2 lp:Msg => lp:F}}. % [fun-implicit N T Ph Ph1] Adds an implicit argument name N of type T areound Ph -pred fun-implicit i:name, i:term, i:(term -> phant-term), o:phant-term. +func fun-implicit name, term, (term -> phant-term) -> phant-term. fun-implicit N Ty (t\ private.phant-term AL (F t)) (private.phant-term [private.implicit|AL] (fun N Ty F)). % [fun-infer-type N T Ph Ph1] Adds an argument N of type T such that one passes % a value V of type {{ Type }} the corresponding canonical VC of type T is passed % for N , eg `fun T (phT : phant T) => Ph` -pred fun-infer-type i:class, i:name, i:term, i:(term -> phant-term), o:phant-term. +func fun-infer-type class, name, term, (term -> phant-term) -> phant-term. fun-infer-type sortclass N Ty (t\private.phant-term AL (Bo t)) Out :- coq.name-suffix N "ph" PhN, fun-implicit N Ty (t\private.phant-term [private.infer-type N sortclass|AL] @@ -98,7 +98,7 @@ fun-infer-type (grefclass Class) N Ty (t\private.phant-term AL (Bo t)) Out :- (fun PhN {{ lib:@hb.phantom lp:Pat lp:t }} _\ Bo t)) Out. % TODO: this looks like a hack to remove -pred append-fun-unify i:phant-term, o:phant-term. +func append-fun-unify phant-term -> phant-term. append-fun-unify (private.phant-term LP T) (private.phant-term LPU T) :- std.append LP [private.unify] LPU. @@ -127,7 +127,7 @@ shorten coq.{ mk-app }. pred this-mixin-is-real-arg o:mixinname. -pred phant-fun i:phant-arg, i:term, i:(term -> phant-term), o:phant-term. +func phant-fun phant-arg, term, (term -> phant-term) -> phant-term. phant-fun Arg Ty PhF (phant-term [Arg|ArgL] (fun N Ty F)) :- if (Arg = real N) true (N = `_`), @pi-decl N Ty x\ PhF x = phant-term ArgL (F x). @@ -136,14 +136,14 @@ phant-fun Arg Ty PhF (phant-term [Arg|ArgL] (fun N Ty F)) :- % which quantifies [PF x] over [x : Ty] (with name N) % Ty must be an (applied) mixin M, and the phantom status of this mixin % is determined by [this-mixin-is-real-arg M]. -pred phant-fun-mixin i:name, i:term, i:(term -> phant-term), o:phant-term. +func phant-fun-mixin name, term, (term -> phant-term) -> phant-term. phant-fun-mixin N Ty PF (private.phant-term [Status|AL] (fun N Ty F)) :- !, std.do! [ @pi-decl N Ty t\ PF t = private.phant-term AL (F t), coq.safe-dest-app Ty (global Mixin) _, if (this-mixin-is-real-arg Mixin) (Status = private.real N) (Status = private.implicit) ]. -pred fun-unify-mixin i:term, i:name, i:term, i:(term -> phant-term), o:phant-term. +func fun-unify-mixin term, name, term, (term -> phant-term) -> phant-term. fun-unify-mixin T N Ty PF Out :- !, std.do! [ coq.safe-dest-app Ty (global M) _, Msg is "fun-unify-mixin: No mixin-src on " ^ {coq.term->string T}, @@ -155,7 +155,7 @@ fun-unify-mixin T N Ty PF Out :- !, std.do! [ % [phant-fun-struct T S Params PF PSF] states that PSF is a phant-term % which postulate a structure [s : S Params] such that [T = sort s] % and then outputs [PF s] -pred phant-fun-struct i:term, i:name, i:structure, i:list term, i:(term -> phant-term), o:phant-term. +func phant-fun-struct term, name, structure, list term, (term -> phant-term) -> phant-term. phant-fun-struct T Name S Params PF Out :- std.do! [ get-structure-sort-projection S SortProj, mk-app (global S) Params SParams, @@ -172,7 +172,7 @@ phant-fun-struct T Name S Params PF Out :- std.do! [ % with name N using the data of the phant-term PT to reconstruct a notation % [Notation N x0 .. xn := C x0 _ _ id .. xi .. _ id _ _ id] % as described above. -pred build-abbreviation i:int, i:term, i:list phant-arg, o:int, o:term. +func build-abbreviation int, term, list phant-arg -> int, term. build-abbreviation K F [] K F. build-abbreviation K F [real N|AL] K'' (fun N _ AbbrevFx) :- !, pi x\ build-abbreviation K {mk-app F [x]} AL K' (AbbrevFx x), @@ -195,8 +195,9 @@ build-abbreviation K F [unify|AL] K' FAbbrev :- !, % [build-type-pattern GR Pat] cheks that GR : forall x_1 ... x_n, Type % and returns Pat = GR _ ... _ (that is GR applied to n holes). % Note that n can be 0 when GR : Type. -pred build-type-pattern i:gref, o:term. +func build-type-pattern gref -> term. build-type-pattern GR Pat :- build-type-pattern.aux GR {coq.env.typeof GR} Pat. +func build-type-pattern.aux gref, term -> term. build-type-pattern.aux GR T {{ lp:Pat _ }} :- coq.unify-eq T (prod N S T') ok, !, @pi-decl N S x\ build-type-pattern.aux GR (T' x) Pat. build-type-pattern.aux GR T (global GR) :- coq.unify-eq T {{ Type }} ok, !. @@ -233,8 +234,8 @@ build-type-pattern.aux _ _ _ :- coq.error "HB: wrong carrier type". % [find m'_{i_k_0}, .., m'_{i_k_nk} | c_0 ~ CK m'_{i_k_0} .. m'_{i_k_nk}] % fun of hb.unify m_{i_0_0} m'_{i_0_0} & ... & hb.unify m_{i_k_nk} m'_{i_k_nk} => % F p_1 ... p_k T m_i0_j0 .. m_il_jl}} -pred mk-phant-term.mixins i:term, i:term, i:classname, i:phant-term, - i:list term, i:name, i:term, i:(term -> list (w-args mixinname)), o:phant-term. +func mk-phant-term.mixins term, term, classname, phant-term, + list term, name, term, (term -> list (w-args mixinname)) -> phant-term. mk-phant-term.mixins Target Src CN PF Params N Ty MLwA Out :- std.do! [ class-def (class CN SI _), mk-app (global SI) Params SIParams, @@ -258,21 +259,21 @@ mk-phant-term.mixins Target Src CN PF Params N Ty MLwA Out :- std.do! [ mk-phant-term.mixins.aux T Params C CN PF X :- std.do![ get-constructor CN KC, - synthesis.infer-all-gref-deps Params T KC KCM, + synthesis.infer-all-gref->deps Params T KC KCM, fun-unify none KCM C PF X, ]. -pred mk-phant-term.class - i:term, i:term, i:classname, i:phant-term, o:phant-term. +func mk-phant-term.class + term, term, classname, phant-term -> phant-term. mk-phant-term.class Target Src CN PF CPF :- !, std.do! [ class-def (class CN _ CMLwP), w-params.fold CMLwP fun-implicit (mk-phant-term.mixins Target Src CN PF) CPF, ]. -pred mk-phant-term.classes - i:term, i:list classname, i:list term, i:term, i:term, - i:list (w-args mixinname), o:phant-term. +func mk-phant-term.classes + term, list classname, list term, term, term, + list (w-args mixinname) -> phant-term. mk-phant-term.classes EtaF CNF PL Target Src MLwA PhF :- !, std.do! [ std.map MLwA triple_1 ML, synthesis.under-mixins.then MLwA phant-fun-mixin (out\ sigma FPLTM\ std.do! [ @@ -280,9 +281,9 @@ mk-phant-term.classes EtaF CNF PL Target Src MLwA PhF :- !, std.do! [ std.fold CNF (phant-term [] FPLTM) (mk-phant-term.class Target Src) out]) PhF ]. -pred mk-phant-term-with-copy i:term, i:list classname, - i:list term, i:name, i:term, - i:(term -> list (w-args mixinname)), o:phant-term. +func mk-phant-term-with-copy term, list classname, + list term, name, term, + (term -> list (w-args mixinname)) -> phant-term. mk-phant-term-with-copy EtaF CNF PL N Ty MLwA PhF :- !, std.do! [ (@pi-decl N Ty target\ @pi-decl N Ty src\ sigma Body\ mk-phant-term.classes EtaF CNF PL target src (MLwA target) Body, diff --git a/HB/common/stdpp.elpi b/HB/common/stdpp.elpi index 9264603d..f40f94a4 100644 --- a/HB/common/stdpp.elpi +++ b/HB/common/stdpp.elpi @@ -9,53 +9,56 @@ kind triple type -> type -> type -> type. type triple A -> B -> C -> triple A B C. - pred triple_1 i:triple A B C, o:A. + func triple_1 triple A B C -> A. triple_1 (triple A _ _) A. - pred triple_2 i:triple A B C, o:B. + func triple_2 triple A B C -> B. triple_2 (triple _ B _) B. - pred triple_3 i:triple A B C, o:C. + func triple_3 triple A B C -> C. triple_3 (triple _ _ C) C. % elpi:endif namespace std { -pred nlist i:int, i:A, o: list A. +func nlist int, A -> list A. nlist N X L :- std.map {std.iota N} (_\ y\ y = X) L. -pred list-diff i:list A, i:list A, o:list A. +:index (_ 1) +func list-diff list A, list A -> list A. list-diff X [] X. list-diff L [D|DS] R :- std.filter L (x\ not(x = D)) L1, list-diff L1 DS R. -pred list-uniq i:list A, o:list A. +:index (1) +func prefixL list A, list A ->. +prefixL [] _. +prefixL [X|Xs] [X|Ys] :- prefixL Xs Ys. + +func list-uniq list A -> list A. pred list-uniq.seen i:A. list-uniq [] []. list-uniq [X|XS] YS :- list-uniq.seen X, !, list-uniq XS YS. list-uniq [X|XS] [X|YS] :- list-uniq.seen X => list-uniq XS YS. -pred list-eq-set i:list A, i:list A. +func list-eq-set list A, list A. list-eq-set L1 L2 :- list-diff L1 L2 [], list-diff L2 L1 []. -pred partition i:list A, i:(A -> prop), o:list A, o:list A. -partition [] _ [] []. -partition [X|XS] P [X|YS] ZS :- P X, !, partition XS P YS ZS. -partition [X|XS] P YS [X|ZS] :- partition XS P YS ZS. - pred under.do! i:((A -> prop) -> A -> prop), i:list prop. under.do! Then LP :- Then (_\ std.do! LP) _. -pred map-triple i:(A -> A1 -> prop), i:(B -> B1 -> prop), i:(C -> C1 -> prop), i:triple A B C, o:triple A1 B1 C1. +func map-triple (func A -> A1), (func B -> B1), (func C -> C1), triple A B C -> triple A1 B1 C1. map-triple F G H (triple X Y Z) (triple X1 Y1 Z1) :- F X X1, G Y Y1, H Z Z1. -pred sort.split i:list A, o:list A, o:list A. +func sort.split list A -> list A, list A. sort.split [] [] [] :- !. sort.split [X] [X] [] :- !. sort.split [X,Y|TL] [X|L1] [Y|L2] :- sort.split TL L1 L2. -pred sort.merge i:(A -> A -> prop), i:list A, i:list A, o:list A. +% sort.merge can take a relation but keeps only the first solution returned. +% There is a cut after the call to `Rel X1 X2`. +func sort.merge (pred i:A, i:A), list A, list A -> list A. sort.merge _ [] L L :- !. sort.merge _ L [] L :- !. sort.merge Rel [X1|L1] [X2|L2] [X1|M] :- Rel X1 X2, !, @@ -63,13 +66,14 @@ sort.merge Rel [X1|L1] [X2|L2] [X1|M] :- Rel X1 X2, !, sort.merge Rel [X1|L1] [X2|L2] [X2|M] :- sort.merge Rel [X1|L1] L2 M. -pred sort i:list A, i:(A -> A -> prop), o:list A. +:index(1) +func sort list A, (pred i:A, i:A) -> list A. sort [] _ [] :- !. sort [X] _ [X] :- !. sort L Rel M :- sort.split L L1 L2, sort L1 Rel S1, sort L2 Rel S2, sort.merge Rel S1 S2 M. -pred bubblesort i:list A, i:(A -> A -> prop), o:list A. +func bubblesort list A, (pred i:A, i:A) -> list A. bubblesort [] _ [] :- !. bubblesort [X] _ [X] :- !. bubblesort [X,Y|TL] Rel [X|Rest1] :- Rel X Y, !, bubblesort [Y|TL] Rel Rest1. @@ -78,47 +82,50 @@ bubblesort [X,Y|TL] Rel [Y|Rest1] :- bubblesort [X|TL] Rel Rest1. % TODO: pred toposort i:(A -> A -> prop), i:list A, o:list A. % pred edge? i:int, i:int. % toposort edge? [1,2,3,4] TopoList -pred topovisit i: list (pair A A), i: A, i: list A, i: list A, o: list A, o: list A. +func topovisit list (pair A A), A, list A, list A -> list A, list A. topovisit _ X VS PS VS PS :- std.mem PS X, !. topovisit _ X VS _ _ _ :- std.mem VS X, !, halt "cycle detected.". topovisit ES X VS PS VS' [X|PS'] :- toporec ES {std.map {std.filter ES (e\ fst e X)} snd} [X|VS] PS VS' PS'. -pred toporec i: list (pair A A), i: list A, i: list A, i: list A, o: list A, o: list A. +func toporec list (pair A A), list A, list A, list A -> list A, list A. toporec _ [] VS PS VS PS. toporec ES [X|XS] VS PS VS'' PS'' :- topovisit ES X VS PS VS' PS', toporec ES XS VS' PS' VS'' PS''. -pred toposort i: list (pair A A), i: list A, o: list A. +func toposort list (pair A A), list A -> list A. toposort ES XS XS'' :- toporec ES XS [] [] _ XS', - std.filter XS' (std.mem XS) XS''. + std.filter XS' (std.mem! XS) XS''. namespace gref { -pred topovisit i: coq.gref.map coq.gref.set, i: classname, i: coq.gref.set, i: list classname, i: coq.gref.set, o: coq.gref.set, o: list classname, o: coq.gref.set. +func topovisit coq.gref.map coq.gref.set, classname, coq.gref.set, list classname, coq.gref.set -> coq.gref.set, list classname, coq.gref.set. topovisit _ X VS PS PSS VS PS PSS :- coq.gref.set.mem X PSS, !. topovisit _ X VS _ _ _ _ _ :- coq.gref.set.mem X VS, !, halt "cycle detected.". topovisit ES X VS PS PSS VS' [X|PS'] PSS'' :- - (coq.gref.map.find X ES M ; coq.gref.set.empty M), + std.once (coq.gref.map.find X ES M ; coq.gref.set.empty M), toporec ES {coq.gref.set.elements M} {coq.gref.set.add X VS} PS PSS VS' PS' PSS', coq.gref.set.add X PSS' PSS''. -pred toporec i: coq.gref.map coq.gref.set, i: list classname, i: coq.gref.set, i: list classname, i: coq.gref.set, o: coq.gref.set, o: list classname, o: coq.gref.set. +:index (_ 1) +func toporec coq.gref.map coq.gref.set, list classname, coq.gref.set, list classname, coq.gref.set -> coq.gref.set, list classname, coq.gref.set. toporec _ [] VS PS PSS VS PS PSS. toporec ES [X|XS] VS PS PSS VS'' PS'' PSS'' :- topovisit ES X VS PS PSS VS' PS' PSS', toporec ES XS VS' PS' PSS' VS'' PS'' PSS''. -pred add-to-neighbours i:coq.gref.set, i:pair gref gref, i:coq.gref.map coq.gref.set, o:coq.gref.map coq.gref.set. +:index (1) +func add-to-neighbours coq.gref.set, pair gref gref, coq.gref.map coq.gref.set -> coq.gref.map coq.gref.set. add-to-neighbours VS (pr _ V) A A :- not(coq.gref.set.mem V VS), !. add-to-neighbours _ (pr K V) A A1 :- coq.gref.map.find K A L, !, coq.gref.map.add K {coq.gref.set.add V L} A A1. add-to-neighbours _ (pr K V) A A1 :- coq.gref.map.add K {coq.gref.set.add V {coq.gref.set.empty} } A A1. -pred toposort i:list (pair gref gref), i:list gref, o:list gref. -toposort ES XS XS'' :- !, std.do! [ +:index(1) +func toposort list (pair gref gref), list gref -> list gref. +toposort ES XS XS'' :- !, std.fold XS {coq.gref.set.empty} coq.gref.set.add VS, std.fold ES {coq.gref.map.empty} (add-to-neighbours VS) EM, toporec EM XS {coq.gref.set.empty} [] {coq.gref.set.empty} _ XS'' _ -]. +. } -pred time-do! i:list prop. +func time-do! list prop ->. time-do! []. time-do! [P|PS] :- std.time P Time, !, @@ -131,14 +138,15 @@ time-do! [P|PS] :- namespace compat { % TODO: replace with std.map-filter when coq-elpi > 1.9.2 -pred map-filter i:list A, i:(A -> B -> prop), o:list B. +:index (1) +func map-filter list A, (A -> B -> prop) -> list B. map-filter [] _ []. map-filter [X|XS] F [Y|YS] :- F X Y, !, map-filter XS F YS. map-filter [_|XS] F YS :- map-filter XS F YS. } -pred print-ctx. +func print-ctx. print-ctx :- declare_constraint print-ctx []. constraint print-ctx mixin-src { rule \ (G ?- print-ctx) | (coq.say "The context is:" G). @@ -146,19 +154,20 @@ constraint print-ctx mixin-src { %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -pred coq.term-is-gref? i:term, o:gref. -coq.term-is-gref? (global GR) GR :- !. -coq.term-is-gref? (pglobal GR _) GR :- !. -coq.term-is-gref? (app [Hd|_]) GR :- !, coq.term-is-gref? Hd GR. -coq.term-is-gref? (let _ _ T x\x) GR :- !, coq.term-is-gref? T GR. +func coq.term-is-gref? term -> gref. +coq.term-is-gref? (global GR) GR. +coq.term-is-gref? (pglobal GR _) GR. +coq.term-is-gref? (app [Hd|_]) GR :- coq.term-is-gref? Hd GR. +coq.term-is-gref? (let _ _ T x\x) GR :- coq.term-is-gref? T GR. -pred coq.prod-tgt->gref i:term, o:gref. +func coq.prod-tgt->gref term -> gref. coq.prod-tgt->gref T GR :- whd1 T T1, !, coq.prod-tgt->gref T1 GR. coq.prod-tgt->gref (prod N Src Tgt) GR :- !, @pi-decl N Src x\ coq.prod-tgt->gref (Tgt x) GR. coq.prod-tgt->gref End GR :- coq.term->gref End GR. % TODO: move to coq-elpi proper / move to coq.pp in coq-elpi >= 1.9 -pred coq.indt-decl->string i:indt-decl, o:string. +:index(1) +func coq.indt-decl->string indt-decl -> string. coq.indt-decl->string (parameter ID _ Ty D) S :- coq.id->name ID Name, (@pi-decl Name Ty x\ coq.indt-decl->string (D x) S1), @@ -167,13 +176,17 @@ coq.indt-decl->string (inductive _ _ _ _) "NYI". coq.indt-decl->string (record ID Ty KID RD) S :- coq.record-decl->string RD S1, S is ID ^ " : " ^ {coq.term->string Ty} ^ " := " ^ KID ^ " {\n" ^ S1 ^ "}". -pred coq.record-decl->string i:record-decl, o:string. + +:index(1) +func coq.record-decl->string record-decl -> string. coq.record-decl->string end-record "". coq.record-decl->string (field _ ID Ty D) S :- coq.id->name ID Name, (@pi-decl Name Ty x\ coq.record-decl->string (D x) S1), S is " " ^ ID ^ " : " ^ {coq.term->string Ty} ^ ";\n" ^ S1. -pred coq.ground-indt-decl? i:indt-decl. + +:index(1) +func coq.ground-indt-decl? indt-decl ->. coq.ground-indt-decl? (parameter ID _ Ty D) :- ground_term Ty, coq.id->name ID Name, (@pi-decl Name Ty x\ coq.ground-indt-decl? (D x)). @@ -181,40 +194,43 @@ coq.ground-indt-decl? (inductive _ _ _ _). coq.ground-indt-decl? (record _ Ty _ RD) :- ground_term Ty, coq.ground-record-decl? RD. -pred coq.ground-record-decl? i:record-decl. + +:index(1) +func coq.ground-record-decl? record-decl ->. coq.ground-record-decl? end-record. coq.ground-record-decl? (field _ ID Ty D) :- ground_term Ty, coq.id->name ID Name, (@pi-decl Name Ty x\ coq.ground-record-decl? (D x)). % TODO: remove when coq-elpi > 1.9.3 -pred copy-indt-decl i:indt-decl, o:indt-decl. -copy-indt-decl (parameter ID I Ty D) (parameter ID I Ty1 D1) :- - copy Ty Ty1, - @pi-parameter ID Ty1 x\ copy-indt-decl (D x) (D1 x). -copy-indt-decl (inductive ID CO A D) (inductive ID CO A1 D1) :- - copy-arity A A1, - coq.id->name ID N, coq.arity->term A1 T, @pi-decl N T i\ std.map (D i) copy-constructor (D1 i). - % @pi-inductive ID A1 i\ std.map (D i) copy-constructor (D1 i). % requires Coq-Elpi 1.9.x -copy-indt-decl (record ID T IDK F) (record ID T1 IDK F1) :- - copy T T1, - copy-fields F F1. -pred copy-fields i:record-decl, o:record-decl. -copy-fields end-record end-record. -copy-fields (field Att ID T F) (field Att ID T1 F1) :- - copy T T1, - @pi-parameter ID T1 x\ copy-fields (F x) (F1 x). -pred copy-constructor i:indc-decl, o:indc-decl. -copy-constructor (constructor ID A) (constructor ID A1) :- copy-arity A A1. +% func copy-indt-decl indt-decl -> indt-decl. +% copy-indt-decl (parameter ID I Ty D) (parameter ID I Ty1 D1) :- +% copy Ty Ty1, +% @pi-parameter ID Ty1 x\ copy-indt-decl (D x) (D1 x). +% copy-indt-decl (inductive ID CO A D) (inductive ID CO A1 D1) :- +% copy-arity A A1, +% coq.id->name ID N, coq.arity->term A1 T, @pi-decl N T i\ std.map (D i) copy-constructor (D1 i). +% % @pi-inductive ID A1 i\ std.map (D i) copy-constructor (D1 i). % requires Coq-Elpi 1.9.x +% copy-indt-decl (record ID T IDK F) (record ID T1 IDK F1) :- +% copy T T1, +% copy-fields F F1. +% func copy-fields record-decl -> record-decl. +% copy-fields end-record end-record. +% copy-fields (field Att ID T F) (field Att ID T1 F1) :- +% copy T T1, +% @pi-parameter ID T1 x\ copy-fields (F x) (F1 x). +% func copy-constructor indc-decl -> indc-decl. +% copy-constructor (constructor ID A) (constructor ID A1) :- copy-arity A A1. % TODO: move to coq-elpi proper -pred coq.gref.list->set i:list gref, o:coq.gref.set. +func coq.gref.list->set list gref -> coq.gref.set. coq.gref.list->set L S :- std.fold L {coq.gref.set.empty} coq.gref.set.add S. % [coq.abstract-indt-decl Section I AbsI] abstracts I over the Section variables % which becomes parameter nodes of the indt-decl type -pred coq.abstract-indt-decl i:list constant, i:indt-decl, o:indt-decl. +:index(1) +func coq.abstract-indt-decl list constant, indt-decl -> indt-decl. coq.abstract-indt-decl [] X X1 :- copy-indt-decl X X1. coq.abstract-indt-decl [C|CS] X (parameter ID explicit Ty1 X1) :- coq.gref->id (const C) ID, @@ -226,7 +242,8 @@ coq.abstract-indt-decl [C|CS] X (parameter ID explicit Ty1 X1) :- % [coq.abstract-const-decl Section I AbsI] abstracts I over the Section variables % which becomes fun nodes -pred coq.abstract-const-decl i:list constant, i:pair term term, o:pair term term. +:index (1) +func coq.abstract-const-decl list constant, pair term term -> pair term term. coq.abstract-const-decl [] (pr X Y) (pr X1 Y1) :- copy X X1, copy Y Y1. coq.abstract-const-decl [C|CS] X (pr (fun Name Ty1 X1) (prod Name Ty1 X2)) :- coq.gref->id (const C) ID, @@ -239,7 +256,8 @@ coq.abstract-const-decl [C|CS] X (pr (fun Name Ty1 X1) (prod Name Ty1 X2)) :- % [coq.copy-clauses-for-unfold CS CL] generates clauses for the copy predicate % to unfold all constants in CS -pred coq.copy-clauses-for-unfold i:list constant, o:list prop. +:index(1) +func coq.copy-clauses-for-unfold list constant -> list prop. coq.copy-clauses-for-unfold [] []. coq.copy-clauses-for-unfold [C|CS] [ClauseApp,Clause|L] :- coq.env.const C (some B) _, @@ -255,7 +273,7 @@ coq.copy-clauses-for-unfold [C|CS] [ClauseApp,Clause|L] :- % like fold-map, needed for coq-elpi < 1.9 -pred coq.fold-map i:term, i:A, o:term, o:A. +func coq.fold-map term, A -> term, A. coq.fold-map X A Y A :- name X, !, X = Y, !. % avoid loading "coq.fold-map x A x A" at binders coq.fold-map (global _ as C) A C A :- !. coq.fold-map (sort _ as C) A C A :- !. @@ -275,29 +293,19 @@ coq.fold-map (uvar M L as X) A W A1 :- var X, !, std.fold-map L A coq.fold-map L % when used in CHR rules coq.fold-map (uvar X L) A (uvar X L1) A1 :- std.fold-map L A coq.fold-map L1 A1. -pred cs-pattern->term i:cs-pattern, o:term. +func cs-pattern->term cs-pattern -> term. cs-pattern->term (cs-gref GR) T :- coq.env.global GR T. -cs-pattern->term (cs-sort prop) (sort prop). -cs-pattern->term (cs-sort sprop) (sort sprop). +cs-pattern->term (cs-sort prop) (sort prop) :- !. +cs-pattern->term (cs-sort sprop) (sort sprop) :- !. cs-pattern->term (cs-sort _) T :- coq.elaborate-skeleton {{ Type }} _ T ok. cs-pattern->term cs-prod T :- coq.elaborate-skeleton (prod `x` Ty_ x\ Bo_ x) _ T ok. -pred term->cs-pattern i:term, o:cs-pattern. -term->cs-pattern (prod _ _ _) cs-prod. -term->cs-pattern (sort U) (cs-sort U). -term->cs-pattern T (cs-gref GR) :- coq.term->gref T GR. +func term->cs-pattern term -> cs-pattern. +term->cs-pattern (prod _ _ _) cs-prod :- !. +term->cs-pattern (sort U) (cs-sort U) :- !. +term->cs-pattern T (cs-gref GR) :- coq.term->gref T GR, !. term->cs-pattern T _ :- coq.error T "HB database: is not a valid canonical key". - -% this one is in utils, maybe cs-pattern->name is not stdpp material -pred gref->modname-label i:gref, i:int, i:string, o:string. - -pred cs-pattern->name i:cs-pattern, o:string. -cs-pattern->name cs-prod "prod". -cs-pattern->name (cs-sort _) "sort". -cs-pattern->name cs-default "default". -cs-pattern->name (cs-gref GR) Name :- gref->modname-label GR 1 "_" Name. - % --------------------------------------------------------------------- % kit for closing a term by abstracting evars with lambdas % we use constraints to attach to holes a number @@ -310,7 +318,7 @@ namespace abstract-holes { type abs int -> term. % bind back abstracted subterms -pred bind i:int, i:int, i:term, o:term. +func bind int, int, term -> term. bind I M T T1 :- M > I, !, T1 = {{ fun x => lp:(B x) }}, N is I + 1, @@ -323,7 +331,7 @@ bind M M T T1 :- copy T T1. % we perform all the replacements % the clause see is only generated for a term if it hasn't been seen before % the term might need to be typechecked first or main generates extra holes for the % type of the parameters -pred main i:term, o:term. +func main term -> term. main T1 T3 :- std.do! [ % we put (abs N) in place of each occurrence of the same hole (pi T Ty N N' M \ fold-map T N (abs M) M :- var T, not (seen? T _), !, coq.typecheck T Ty ok, fold-map Ty N _ N', M is N' + 1, seen! T M) => @@ -340,15 +348,15 @@ main T1 T3 :- std.do! [ % we query if the hole was seen before, and if so % we fetch its number -pred seen? i:term, o:int. +func seen? term -> int. seen? X Y :- declare_constraint (seen? X Y) [X,_]. % we declare it is now seen and label it with a number -pred seen! i:term, i:int. +func seen! term, int ->. seen! X Y :- declare_constraint (seen! X Y) [X,_]. % to empty the store -pred purge-seen!. +func purge-seen!. purge-seen! :- declare_constraint purge-seen! [_]. constraint seen? seen! purge-seen! { diff --git a/HB/common/synthesis.elpi b/HB/common/synthesis.elpi index 6444e23c..7a06646d 100644 --- a/HB/common/synthesis.elpi +++ b/HB/common/synthesis.elpi @@ -15,7 +15,7 @@ namespace synthesis { % [infer-all-these-mixin-args Ps T ML F X] fills in all the arguments of F % which are misxins in ML, abstracts the others -pred infer-all-these-mixin-args i:list term, i:term, i:list mixinname, i:term, o:term. +func infer-all-these-mixin-args list term, term, list mixinname, term -> term. infer-all-these-mixin-args Ps T ML F SFX :- std.do! [ std.assert-ok! (coq.typecheck F Ty) "try-infer-these-mixin-args: F illtyped", coq.mk-eta (-1) Ty F EtaF, @@ -23,11 +23,11 @@ infer-all-these-mixin-args Ps T ML F SFX :- std.do! [ private.instantiate-all-these-mixin-args FT T ML SFX, ]. -% [infer-all-gref-deps Ps T GR X] fills in all the arguments of GR -% which are misxins in gref-deps GR, other arguments are abstracted -pred infer-all-gref-deps i:list term, i:term, i:gref, o:term. -infer-all-gref-deps Ps T GR X :- std.do! [ - std.assert! (gref-deps GR MLwP) "BUG: gref-deps should never fail", +% [infer-all-gref->deps Ps T GR X] fills in all the arguments of GR +% which are misxins in gref->deps GR, other arguments are abstracted +func infer-all-gref->deps list term, term, gref -> term. +infer-all-gref->deps Ps T GR X :- std.do! [ + std.assert! (gref->deps GR MLwP) "BUG: gref->deps should never fail", list-w-params_list MLwP ML, coq.env.typeof GR Ty, coq.mk-eta (-1) Ty (global GR) EtaF, @@ -37,22 +37,22 @@ infer-all-gref-deps Ps T GR X :- std.do! [ ]. % [infer-holes-depending-on-params TheType T NewT] -pred infer-holes-depending-on-params i:term, i:term, o:term. +func infer-holes-depending-on-params term, term -> term. infer-holes-depending-on-params T (app [global GR|Args]) (app [global GR|Args1]) :- !, std.map Args (infer-holes-depending-on-pack T) Args1. infer-holes-depending-on-params _ X X. -pred class-of-phant i:term, o:gref, o:gref, o:gref. +func class-of-phant term -> gref, gref, gref. class-of-phant (prod N T F) X Y Z :- @pi-decl N T x\ class-of-phant (F x) X Y Z. -class-of-phant (global GR) Y Z X :- class-def (class X GR _), get-constructor X Y, get-constructor GR Z. -class-of-phant (app[global GR|_]) Y Z X :- class-def (class X GR _), get-constructor X Y, get-constructor GR Z. +class-of-phant (global GR) Y Z X :- class-def (class X GR _), !, get-constructor X Y, get-constructor GR Z. +class-of-phant (app[global GR|_]) Y Z X :- class-def (class X GR _), !, get-constructor X Y, get-constructor GR Z. -pred infer-holes-depending-on-pack i:term, i:term, o:term. +func infer-holes-depending-on-pack term, term -> term. infer-holes-depending-on-pack T (app [global GR | Args]) S :- ((coq.gref->id GR GRS, rex.match "phant.*" GRS /*TODO: phant-clone? GR N*/); pack? GR _), coq.env.typeof GR Ty, class-of-phant Ty KC SC C, - factory-nparams C N, + factory->nparams C N, std.take N Args Params, !, std.do! [ infer-all-args-let Params T KC ClassInstance ok, @@ -66,7 +66,7 @@ infer-holes-depending-on-pack _ X X. % and generates a term % let `a1` ty1 t1 a1\ .... app[global GR, p1, .. pn, T, a1, .. , an] % if Diagnostic is ok, else X is unassigned -pred infer-all-args-let i:list term, i:term, i:gref, o:term, o:diagnostic. +func infer-all-args-let list term, term, gref -> term, diagnostic. infer-all-args-let Ps T GR X Diag :- std.do! [ coq.env.typeof GR Ty, coq.mk-eta (-1) Ty (global GR) EtaF, @@ -77,7 +77,7 @@ infer-all-args-let Ps T GR X Diag :- std.do! [ % [assert!-infer-mixin TheType M Out] infers one mixin M on TheType and % aborts with an error message if the mixin cannot be inferred -pred assert!-infer-mixin i:term, i:mixinname, o:term. +func assert!-infer-mixin term, mixinname -> term. assert!-infer-mixin T M B :- if (private.mixin-for T M B) true @@ -86,7 +86,8 @@ assert!-infer-mixin T M B :- % Given TheType it looks all canonical structure instances on it and makes % all their mixins available for inference -pred local-canonical-mixins-of.aux i:term, i:list structure, o:list prop. +:index (_ 1) +func local-canonical-mixins-of.aux term, list structure -> list prop. local-canonical-mixins-of.aux _ [] []. local-canonical-mixins-of.aux T [S|Ss] MSL'' :- std.do! [ private.structure-instance->mixin-srcs T S MSL, @@ -94,7 +95,7 @@ local-canonical-mixins-of.aux T [S|Ss] MSL'' :- std.do! [ std.append MSL MSL' MSL'', ]. -pred local-canonical-mixins-of i:term, o:list prop. +func local-canonical-mixins-of term -> list prop. local-canonical-mixins-of T MSL :- std.do! [ get-canonical-structures T CS, std.map CS (s\c\ sigma w\ class-def (class c s w)) Cl, @@ -105,22 +106,21 @@ local-canonical-mixins-of T MSL :- std.do! [ % Given TheType and a factory instance (on it), makes all the mixins provided by % the factory available for inference. -pred under-mixin-src-from-factory.do! i:term, i:term, i:list prop. -under-mixin-src-from-factory.do! TheType TheFactory LP :- std.do! [ +func under-mixin-src-from-factory.do! term, term, list prop. +under-mixin-src-from-factory.do! TheType TheFactory LP :- private.factory-instance->new-mixins [] TheFactory ML, std.map ML (m\c\ c = mixin-src TheType m TheFactory) MLClauses, - MLClauses => std.do! LP -]. + MLClauses => std.do! LP. % Given TheType and a factory instance (on it), builds all the *new* mixins % provided by the factory available for and passes them to the given % continuation -pred under-new-mixin-src-from-factory.do! i:term, i:term, i:(list mixinname -> prop). +func under-new-mixin-src-from-factory.do! term, term, (list mixinname -> prop). under-new-mixin-src-from-factory.do! TheType TheFactory LP :- findall-mixin-src TheType OldMixins, private.factory-instance->new-mixins OldMixins TheFactory NewML, std.map NewML (m\c\ c = mixin-src TheType m TheFactory) NewMLClauses, - NewMLClauses => std.do! [ LP NewML ]. + NewMLClauses => std.once (LP NewML). % [under-mixins.then MLwP Pred F] states that F has shape % fun p_1 .. p_k T, @@ -129,12 +129,12 @@ under-new-mixin-src-from-factory.do! TheType TheFactory LP :- % where MLwP contains M_0, .., M_n (under p_1 .. p_k) % and Body is such that [..,mixin-src T M_i m_i,..] => Pred Body % and ..p.. is a list of terms built using p_1 .. p_k and T -pred under-mixins.then i:list (w-args mixinname), - i:(name -> term -> (term -> A) -> A -> prop), - i:(A -> prop), o:A. +func under-mixins.then list (w-args mixinname), + (pred i:name, i:term, i:(term -> A), o:A), + (func A -> ) -> A. under-mixins.then [] _ Pred Body :- !, Pred Body. under-mixins.then [triple M Args T|ML] MkFun Pred Out :- std.do! [ - infer-all-gref-deps Args T M MTy, + infer-all-gref->deps Args T M MTy, (@pi-decl `m` MTy m\ mixin-src T M m => under-mixins.then ML MkFun Pred (Body m)), MkFun `m` MTy Body Out, @@ -147,30 +147,31 @@ under-mixins.then [triple M Args T|ML] MkFun Pred Out :- std.do! [ % where MLwP contains M_0, .., M_n (under p_1 .. p_k) % and Body is such that [..,mixin-src T M_i m_i,..] => Pred Body % and ..p.. is a list of terms built using p_1 .. p_k and T -pred mixins-w-params.fun i:mixins, i:(list term -> term -> term -> prop), o:term. +func mixins-w-params.fun mixins, (func list term, term -> term) -> term. mixins-w-params.fun L P Out :- !, w-params.then L mk-fun mk-fun (p\ t\ ml\ under-mixins.then ml mk-fun (P p t)) Out. % [mixins-w-params.length LwP N] states N is Nmixins+Nparams -pred mixins-w-params.length i:mixins, o:int. +func mixins-w-params.length mixins -> int. mixins-w-params.length MLwP N :- w-params.nparams MLwP Nparams, std.length {list-w-params_list MLwP} Nmixins, N is Nparams + Nmixins. -pred infer-coercion-tgt i:mixins, o:class. +func infer-coercion-tgt mixins -> class. 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 _ {{ forall x, _ }} _) funclass. % do not use {{ _ -> _ }} since Funclass can be a dependent function! +infer-coercion-tgt (w-params.nil _ {{ Type }} _) sortclass :- !. +infer-coercion-tgt (w-params.nil _ {{ forall x, _ }} _) funclass :- !. % do not use {{ _ -> _ }} since Funclass can be a dependent function! infer-coercion-tgt (w-params.nil _ T _) (grefclass GR) :- coq.term->gref T GR. -pred w-args.check-key i:list term, i:term, i:list (w-args A), o:prop. +:index (_ _ 2) +func w-args.check-key list term, term, list (w-args A) -> prop. w-args.check-key _PS _T [] true :- !. w-args.check-key PS T [triple _ _ T|LwA] P :- !, w-args.check-key PS T LwA P. w-args.check-key _PS _T _LwA false :- !, coq.error "HB: all mixins must have the same key". -pred list-w-params.check-key i:list-w-params A. +func list-w-params.check-key list-w-params A ->. list-w-params.check-key MLwP :- !, w-params.then MLwP ignore ignore w-args.check-key _. @@ -182,8 +183,8 @@ namespace private { % [mixin-for T M MI] synthesizes an instance of mixin M on type T using % the databases [mixin-src] and [from] -pred mixin-for i:term, i:mixinname, o:term. -mixin-for T M MICompressed :- mixin-src T M Tm, !, std.do! [ +func mixin-for term, mixinname -> term. +mixin-for T M MICompressed :- mixin-src T M Tm, !, %if-verbose (coq.say {header} "Trying to infer mixin for" M), std.assert-ok! (coq.typecheck Tm Ty) "mixin-for: Tm illtyped", @@ -197,14 +198,13 @@ mixin-for T M MICompressed :- mixin-src T M Tm, !, std.do! [ ), %if-verbose (coq.say {header} "Trying to compress mixin for" {coq.term->string MI}), - compress-coercion-paths MI MICompressed, -]. + compress-coercion-paths MI MICompressed. -pred drop i:int, i:list A, o:list A. +func drop int, list A -> list A. drop 0 L L :- !. drop N [_|XS] L :- !, N1 is N - 1, drop N1 XS L. -pred compress-copy o:term, o:term. +func compress-copy -> term, term. compress-copy (app [global (const C) | L]) R :- sub-class C2 C3 C NparamsC, drop NparamsC L [app [global (const C') | L']], @@ -219,23 +219,23 @@ compress-copy (app L) (app L1) :- !, std.map L compress-copy L1. compress-copy X X. -pred compress-coercion-paths i:term, o:term. +func compress-coercion-paths term -> term. compress-coercion-paths MI MICompressed :- if (get-option "compress_coercions" tt) (compress-copy MI MICompressed) (MI = MICompressed). -pred mixin-for_mixin-builder i:prop, o:term. +func mixin-for_mixin-builder prop -> term. mixin-for_mixin-builder (mixin-for _ _ B) B. % [builder->term Params TheType Src Tgt MF] finds a builder from Src to Tgt % and fills in all the mixins required by the builder using mixin-src, obtaining % a function (MF = Builder Params TheType InferredStuff : Src -> Tgt) -pred builder->term i:list term, i:term, i:factoryname, i:mixinname, o:term. +func builder->term list term, term, factoryname, mixinname -> term. builder->term Ps T Src Tgt B :- !, std.do! [ from Src Tgt FGR, F = global FGR, - gref-deps Src MLwP, + gref->deps Src MLwP, list-w-params_list MLwP ML, infer-all-these-mixin-args Ps T ML F B, ]. @@ -246,7 +246,7 @@ builder->term Ps T Src Tgt B :- !, std.do! [ % then TFX := fun xs m_0 .. m_{i-1} m_{i+1} .. m_n ys % => F xs m_0 .. m_{i-1} X_i m_{i+1} .. m_n ys % thus instanciating an abstraction on mixin M_i with X_i -pred instantiate-all-these-mixin-args i:term, i:term, i:list mixinname, o:term. +func instantiate-all-these-mixin-args term, term, list mixinname -> term. instantiate-all-these-mixin-args (fun _ Tm F) T ML R :- coq.safe-dest-app Tm (global TmGR) _, factory-alias->gref TmGR M ok, @@ -258,7 +258,7 @@ instantiate-all-these-mixin-args (fun N Ty F) T ML (fun N Ty FX) :- !, @pi-decl N Ty m\ instantiate-all-these-mixin-args (F m) T ML (FX m). instantiate-all-these-mixin-args F _ _ F. -pred instantiate-all-args-let i:term, i:term, o:term, o:diagnostic. +func instantiate-all-args-let term, term -> term, diagnostic. instantiate-all-args-let (fun N Tm F) T (let N Tm X R) Diag :- !, std.do! [ coq.safe-dest-app Tm (global TmGR) _, factory-alias->gref TmGR M ok, @@ -274,6 +274,7 @@ instantiate-all-args-let F _ F ok. % Structure on TheType (if any) and builds mixin-src clauses for all the mixins % which can be candidates from that class instance. It finds instances which are % concrete, that is not by projecting a rich type (a variable) to its class. +% NOTE: this predicate has a catchall (see below), i.e. it is not a function pred structure-instance->mixin-srcs i:term, i:structure, o:list prop. structure-instance->mixin-srcs T S MSLC :- std.do! [ structure-key SortProj _ S, @@ -305,6 +306,8 @@ structure-instance->mixin-srcs _ _ []. structure-instance->mixin-srcs.aux2 Params T Class (some P) M :- coq.mk-app (global (const P)) {std.append Params [T,Class]} M. + +func structure-instance->mixin-srcs.aux term, term -> list prop. structure-instance->mixin-srcs.aux T F CL :- factory-instance->new-mixins [] F ML, std.map-filter ML (m\c\ not (mixin-src T m _), c = mixin-src T m F) CL. @@ -312,8 +315,8 @@ structure-instance->mixin-srcs.aux T F CL :- % [factory-instance->new-mixins OldMixins FI MSL] find all the mixins % which can be generated by the factory instance FI which are not part of % OldMixins (that is, the contribution of FI to the current context) -pred factory-instance->new-mixins i:list mixinname, i:term, o:list mixinname. -factory-instance->new-mixins OldMixins X NewML :- std.do! [ +func factory-instance->new-mixins list mixinname, term -> list mixinname. +factory-instance->new-mixins OldMixins X NewML :- std.assert-ok! (coq.typecheck X XTy) "mixin-src: X illtyped", if (not (coq.safe-dest-app XTy (global _) _)) (coq.error "Term:\n" {coq.term->string X} @@ -323,7 +326,6 @@ factory-instance->new-mixins OldMixins X NewML :- std.do! [ coq.term->gref XTy Src, factory-provides Src MLwP, list-w-params_list MLwP ML, - std.filter ML (m\ not(std.mem! OldMixins m)) NewML, -]. + std.filter ML (m\ not(std.mem! OldMixins m)) NewML. }} diff --git a/HB/common/utils-synterp.elpi b/HB/common/utils-synterp.elpi index 73932c1a..014d513c 100644 --- a/HB/common/utils-synterp.elpi +++ b/HB/common/utils-synterp.elpi @@ -2,7 +2,7 @@ This software is released under the terms of the MIT license */ % runs P in a context where Coq #[attributes] are parsed -pred with-attributes i:prop. +func with-attributes (func). with-attributes P :- attributes A, coq.parse-attributes A [ @@ -27,29 +27,29 @@ with-attributes P :- ] Opts, !, Opts => (save-docstring, P). -pred if-verbose i:prop. +func if-verbose (func) -> . if-verbose P :- get-option "verbose" tt, !, P. if-verbose _. % header of if-verbose messages -pred header o:string. +func header -> string. header Msg :- Msg is "[" ^ {std.any->string {gettimeofday}} ^ "] HB: ". % approximation, it should be logical path, not the file name -pred coq.env.current-library o:string. -coq.env.current-library L :- loc.fields {get-option "elpi.loc"} L _ _ _ _. +func coq.env.current-library -> string. +coq.env.current-library L :- loc.fields {get-option "elpi.loc"} L _ _ _ _, !. coq.env.current-library "dummy.v". % this is only declared in hb.db, this declaration is only to avoid a warning pred docstring o:loc, o:string. -pred save-docstring. +func save-docstring. save-docstring :- if (get-option "elpi.loc" Loc, get-option "elpi.phase" "interp", get-option "doc" Txt) (coq.elpi.accumulate _ "hb.db" (clause _ _ (docstring Loc Txt))) true. -pred compute-filter i:option string, o:list string. +func compute-filter option string -> list string. compute-filter none []. compute-filter (some S) MFilter :- % S is a component of the current modpath coq.env.current-path P, @@ -58,16 +58,18 @@ compute-filter (some S) MFilter :- % S is a component of the current modpath compute-filter (some S) MFilter :- coq.locate-module S M, coq.modpath->path M MFilter. + +func compute-filter.aux list string, list string -> list string. compute-filter.aux [S|_] [S] [S] :- !. -compute-filter.aux [S|XS] [S|SS] [S|YS] :- compute-filter.aux XS SS YS. +compute-filter.aux [S|XS] [S|SS] [S|YS] :- !, compute-filter.aux XS SS YS. compute-filter.aux [X|XS] L [X|YS] :- compute-filter.aux XS L YS. -pred list-uniq i:list A, o:list A. +func list-uniq list A -> list A. pred list-uniq.seen i:A. list-uniq [] []. list-uniq [X|XS] YS :- list-uniq.seen X, !, list-uniq XS YS. list-uniq [X|XS] [X|YS] :- list-uniq.seen X => list-uniq XS YS. -pred record-decl->id i:indt-decl, o:id. +func record-decl->id indt-decl -> id. record-decl->id (parameter _ _ _ D) N :- pi p\ record-decl->id (D p) N. record-decl->id (record N _ _ _) N. diff --git a/HB/common/utils.elpi b/HB/common/utils.elpi index ae4216b6..9d053dbc 100644 --- a/HB/common/utils.elpi +++ b/HB/common/utils.elpi @@ -7,23 +7,23 @@ accumulate HB/common/utils-synterp. shorten coq.{ term->gref, subst-fun, safe-dest-app, mk-app, mk-eta, subst-prod }. -pred if-arg-sort i:prop. +func if-arg-sort (func) ->. if-arg-sort P :- get-option "arg_sort" tt, !, P. if-arg-sort _. -pred if-MC-compat i:(option gref -> prop). +func if-MC-compat (func option gref ->) ->. if-MC-compat P :- get-option "mathcomp" tt, !, P none. if-MC-compat P :- get-option "mathcomp.axiom" S, !, std.assert! (coq.locate S GR) "The name passed to the mathcomp.axiom attribute does not exist", P (some GR). if-MC-compat _. -pred with-locality i:prop. +func with-locality (func) ->. with-locality P :- if (get-option "local" tt) (A = @local!) (A = @global!), A => P. -pred acc-clause i:scope, i:prop. +func acc-clause scope, prop. acc-clause Scope C :- coq.elpi.accumulate Scope "hb.db" (clause _ _ C). /* Uncomment and remove HB/common/compat_acc_clauses_*.elpi once requiring coq-elpi >= 1.18.0, @@ -35,7 +35,8 @@ acc-clauses Scope CL :- coq.elpi.accumulate-clauses Scope "hb.db" {std.map CL (c % 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" % TODO: rename since this is HB specific and is expected to return a factory -pred located->gref i:string, i:list located, o:gref. +:index (_ 2) +func located->gref string, list located -> gref. located->gref _ [loc-gref GR|_] GR. located->gref _ [loc-abbreviation Abbrev|_] GR :- phant-abbrev GR _ Abbrev, !. located->gref S [loc-abbreviation _|_] _ :- coq.error S "is an abbreviation out of the control of HB". @@ -44,24 +45,24 @@ located->gref S [loc-modtypath _|_] _ :- coq.error S "should be a factory, but i located->gref S [] _ :- coq.error "Could not locate name" S. % TODO: generalize/rename when we support parameters -pred argument->gref i:argument, o:gref. -argument->gref (str S) GR :- located->gref S {coq.locate-all S} GR. +func argument->gref argument -> gref. +argument->gref (str S) GR :- !, located->gref S {coq.locate-all S} GR. argument->gref X _ :- coq.error "Argument" X "is expected to be a string". -pred argument->term i:argument, o:term. +func argument->term argument -> term. argument->term (str S) (global GR) :- !, argument->gref (str S) GR. argument->term (trm T) T1 :- !, std.assert-ok! (coq.elaborate-skeleton T _ T1) "not well typed term". argument->term X _ :- coq.error "Argument" X " is expected to be a term or a string". -pred argument->ty i:argument, o:term. +func argument->ty argument -> term. argument->ty (str S) T1 :- !, argument->gref (str S) GR, std.assert-ok! (coq.elaborate-ty-skeleton (global GR) _ T1) "global reference is not a type". argument->ty (trm T) T1 :- !, std.assert-ok! (coq.elaborate-ty-skeleton T _ T1) "not well typed type". argument->ty X _ :- coq.error "Argument" X " is expected to be a type or a string". -pred builder->string i:builder, o:string. +func builder->string builder -> string. builder->string (builder _ _ _ B) S :- coq.term->string (global B) S. -pred nice-gref->string i:gref, o:string. +func nice-gref->string gref -> string. nice-gref->string X Mod :- coq.gref->path X Path, std.rev Path [Mod1,Mod2|_], !, @@ -69,7 +70,7 @@ nice-gref->string X Mod :- nice-gref->string X S :- coq.term->string (global X) S. -pred gref->modname i:gref, i:int, i:string, o:string. +func gref->modname gref, int, string -> string. gref->modname GR NComp Sep ModName :- coq.gref->path GR Path, std.rev Path Mods, @@ -77,7 +78,7 @@ gref->modname GR NComp Sep ModName :- if (Len >= NComp) true (coq.error "Not enough enclosing modules for" {coq.gref->string GR}), std.take NComp Mods L, std.string.concat Sep {std.rev L} ModName. -pred gref->modname-label i:gref, i:int, i:string, o:string. +func gref->modname-label gref, int, string -> string. gref->modname-label GR NComp Sep ModName :- coq.gref->path GR Path, std.rev Path PathRev, @@ -86,28 +87,35 @@ gref->modname-label GR NComp Sep ModName :- std.take N PathRev L, std.string.concat Sep {std.rev [{coq.gref->id GR}|L]} ModName. -pred string->modpath i:string, o:modpath. +func cs-pattern->name cs-pattern -> string. +cs-pattern->name cs-prod "prod". +cs-pattern->name (cs-sort _) "sort". +cs-pattern->name cs-default "default". +cs-pattern->name (cs-gref GR) Name :- gref->modname-label GR 1 "_" Name. + + +func string->modpath string -> modpath. string->modpath S MP :- std.filter {coq.locate-all S} (l\l = loc-modpath _) L, L = [loc-modpath MP]. -pred gref->modname_short1 i:modpath, i:string, i:list string, o:string. -gref->modname_short1 _ S [] S. -gref->modname_short1 MP "" [X|L] L' :- gref->modname_short1 MP X L L'. -gref->modname_short1 MP S _ S :- string->modpath S MP. +func gref->modname_short1 modpath, string, list string -> string. +gref->modname_short1 _ S [] S :- !. +gref->modname_short1 MP "" [X|L] L' :- !, gref->modname_short1 MP X L L'. +gref->modname_short1 MP S _ S :- !, string->modpath S MP. gref->modname_short1 MP S [X|L] S' :- gref->modname_short1 MP {std.string.concat "." [X,S]} L S'. % Print shortest qualified identifier of the module containing a gref % Sep is used as separator -pred gref->modname_short i:gref, i:string, o:string. +func gref->modname_short gref, string -> string. gref->modname_short GR Sep IDS :- coq.gref->path GR Path, string->modpath {std.string.concat "." Path} MP, gref->modname_short1 MP "" {std.rev Path} ID, rex.replace "[.]" Sep ID IDS. -pred avoid-name-collision i:string, o:string. +func avoid-name-collision string -> string. avoid-name-collision S S1 :- coq.locate-all S L, if (std.mem L (loc-gref GR), coq.gref->path GR P, coq.env.current-path P) @@ -118,39 +126,41 @@ avoid-name-collision S S1 :- % function to predicate generic constructions % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -pred mk-nil o:list A. +func mk-nil -> list A. mk-nil []. -pred mk0 i:A, o:A. +func mk0 A -> A. mk0 F R :- constant R F []. -pred mk1 i:(A -> B), i:A, o:B. +func mk1 (A -> B), A -> B. mk1 F X1 R :- constant R F [X1]. -pred mk2 i:(A -> A -> C), i:A, i:A, o:C. +func mk2 (A -> A -> C), A, A -> C. mk2 F X1 X2 R :- constant R F [X1, X2]. -pred mk3 i:(A -> A -> A -> D), i:A, i:A, i:A, o:D. +func mk3 (A -> A -> A -> D), A, A, A -> D. mk3 F X1 X2 X3 R :- constant R F [X1, X2, X3]. -pred mk4 i:(A -> A -> A -> A -> E), i:A, i:A, i:A, i:A, o:E. +func mk4 (A -> A -> A -> A -> E), A, A, A, A -> E. mk4 F X1 X2 X3 X4 R :- constant R F [X1, X2, X3,X4]. -pred mk-fun i:name, i:term, i:(term -> term), o:term. +func mk-fun name, term, (term -> term) -> term. mk-fun N Ty Body (fun N Ty Body). % generic argument to pass to w-params -pred ignore i:name, i:term, i:(term -> A), o:A. +func ignore name, term, (term -> A) -> A. ignore _ _ F X :- (pi x y\ F x = F y), X = F (sort prop). % combining body and type -pred mk-fun-prod i:name, i:term, o:(term -> pair term term), o:pair term term. +func mk-fun-prod name, term -> (term -> pair term term), pair term term. mk-fun-prod N Ty (x\ pr (Body x) (Type x)) (pr (fun N Ty Body) (prod N Ty Type)). -pred mk-parameter i:implicit_kind, i:name, i:term, i:(term -> indt-decl), o:indt-decl. -pred mk-parameter i:implicit_kind, i:name, i:term, i:(term -> arity), o:arity. -mk-parameter IK Name X F Decl :- !, Decl = parameter {coq.name->id Name} IK X F. +func mk-parameter implicit_kind, name, term, (term -> indt-decl) -> indt-decl. +mk-parameter IK Name X F (Decl : indt-decl) :- !, Decl = parameter {coq.name->id Name} IK X F. + +func mk-parameter implicit_kind, name, term, (term -> arity) -> arity. +mk-parameter IK Name X F (Decl : arity) :- !, Decl = parameter {coq.name->id Name} IK X F. -pred params->holes i:list-w-params A, o:list term. +func params->holes list-w-params A -> list term. params->holes (w-params.nil _ _ _) []. params->holes (w-params.cons _ _ F) [_|PS] :- pi x\ params->holes (F x) PS. -pred fresh-type o:term. +func fresh-type -> term. fresh-type Ty :- Ty = {{Type}}, std.assert-ok! (coq.typecheck-ty Ty _) "impossible". @@ -159,27 +169,32 @@ fresh-type Ty :- % w-params interface % %%%%%%%%%%%%%%%%%%%%%% -pred apply-w-params i:w-params A, i:list term, i:term, o:A. +:index (1) +func apply-w-params w-params A, list term, term -> A. apply-w-params (w-params.cons _ _ PL) [P|PS] T R :- !, apply-w-params (PL P) PS T R. apply-w-params (w-params.nil _ _ L) [] T R :- !, R = L T. apply-w-params _ _ _ _ :- coq.error "apply-w-params". -pred w-params.nparams i:w-params A, o:int. +:index (1) +func w-params.nparams w-params A -> int. w-params.nparams (w-params.cons _ _ F) N :- pi x\ w-params.nparams (F x) M, N is M + 1. w-params.nparams (w-params.nil _ _ _) 0. % [w-params.fold AwP Cons Nil Out] states that Out has shape % Cons `x_1` T_1 p_1 \ .. \ Nil [p_1 .. p_n] `T` Ty F % where AwP = w-params.cons `x_1` T_1 p_1 \ ... \ w-params.nil `T` Ty F -pred w-params.fold i:w-params A, i:(name -> term -> (term -> B) -> B -> prop), - i:(list term -> name -> term -> (term -> A) -> B -> prop), o:B. +:index (1) +func w-params.fold w-params A, + (func name, term, (term -> B) -> B), + (func list term, name, term, (term -> A) -> B) -> B. w-params.fold L Cons Nil Out :- w-params.fold.params L Cons Nil [] Out. -pred w-params.fold.params i:w-params A, - i:(name -> term -> (term -> B) -> B -> prop), - i:(list term -> name -> term -> (term -> A) -> B -> prop), - i:list term, % accumulator - o:B. +:index (1) +func w-params.fold.params w-params A, + (func name, term, (term -> B) -> B), + (func list term, name, term, (term -> A) -> B), + list term % accumulator + -> B. w-params.fold.params (w-params.cons ID PTy F) Cons Nil RevPs Out :- !, std.do! [ coq.id->name ID N, (@pi-decl N PTy p\ w-params.fold.params (F p) Cons Nil [p|RevPs] (Body p)), @@ -194,55 +209,59 @@ w-params.fold.params (w-params.nil ID TTy F) _ Nil RevParams Out :- !, std.do! [ % Cons `x_1` T_1 p_1 \ .. \ Nil [p_1 .. p_n] `T` Ty t \ Body % where Pred [p_1 .. p_n] T Body % and AwP = w-params.cons `x_1` T_1 p_1 \ ... \ w-params.nil `T` Ty F -pred w-params.then i:w-params A, - i:(name -> term -> (term -> C) -> C -> prop), - i:(name -> term -> (term -> B) -> C -> prop), - i:(list term -> term -> A -> B -> prop), - o:C. +:index (1) +func w-params.then w-params A, + (func name, term, (term -> C) -> C), + (func name, term, (term -> B) -> C), + (func list term, term, A -> B) + -> C. w-params.then L Cons Nil Pred Out :- w-params.fold L Cons (ps\ n\ ty\ f\ out\ sigma Body\ (@pi-decl n ty t\ Pred ps t (f t) (Body t)), Nil n ty Body out) Out. -pred w-params.map i:w-params A, i:(list term -> term -> A -> B -> prop), o:w-params B. +func w-params.map w-params A, (func list term, term, A -> B) -> w-params B. w-params.map AL F BL :- w-params.then AL mk-w-params.cons-name mk-w-params.nil-name F BL. % TODO: make combinators pass id -type mk-w-params.cons-name name -> term -> (term -> w-params A) -> w-params A -> prop. +func mk-w-params.cons-name name, term, (term -> w-params A) -> w-params A. mk-w-params.cons-name N T F (w-params.cons ID T F):- coq.name->id N ID. -type mk-w-params.nil-name name -> term -> (term -> A) -> w-params A -> prop. +func mk-w-params.nil-name name, term, (term -> A) -> w-params A. mk-w-params.nil-name N T F (w-params.nil ID T F):- coq.name->id N ID. % on the fly abstraction -pred bind-nil i:id, i:term, i:term, i:A, o:w-params A. +func bind-nil id, term, term, A -> w-params A. bind-nil N T X V (w-params.nil N T A) :- V = A X. -pred bind-cons i:id, i:term, i:term, i:w-params A, o:w-params A. +func bind-cons id, term, term, w-params A -> w-params A. bind-cons N T X V (w-params.cons N T A) :- V = A X. % Specific to list-w-params -pred list-w-params_list i:list-w-params A, o:list A. +func list-w-params_list list-w-params A -> list A. list-w-params_list AwP R :- w-params.then AwP ignore ignore (p\ t\ x\ std.map x triple_1) R. -pred list-w-params.append i:list-w-params A, i:list-w-params A, o:list-w-params A. +:index (1) +func list-w-params.append list-w-params A, list-w-params A -> list-w-params A. list-w-params.append (w-params.nil N T ML1) (w-params.nil N T ML2) (w-params.nil N T ML) :- pi x\ std.append (ML1 x) (ML2 x) (ML x). list-w-params.append (w-params.cons N Ty ML1) (w-params.cons N Ty ML2) (w-params.cons N Ty ML) :- pi x\ list-w-params.append (ML1 x) (ML2 x) (ML x). -pred list-w-params.rcons i:list-w-params A, i:(list term -> term -> w-args A -> prop), o:list-w-params A. +:index (1) +func list-w-params.rcons list-w-params A, (func list term, term -> w-args A) -> list-w-params A. list-w-params.rcons LwP F R :- list-w-params.rcons.aux LwP F [] R. -pred list-w-params.rcons.aux i:list-w-params A, i:(list term -> term -> w-args A -> prop), i:list term, o:list-w-params A. +:index (1) +func list-w-params.rcons.aux list-w-params A, (func list term, term -> w-args A), list term -> list-w-params A. list-w-params.rcons.aux (w-params.nil N T ML1) F Acc (w-params.nil N T ML2) :- pi x\ sigma Last\ F {std.rev Acc} x Last, std.append (ML1 x) [Last] (ML2 x). list-w-params.rcons.aux (w-params.cons N Ty ML1) F Acc (w-params.cons N Ty ML2) :- pi x\ list-w-params.rcons.aux (ML1 x) F [x|Acc] (ML2 x). -pred list-w-params.flatten-map - i:list-w-params A, - i:(A -> list-w-params B -> prop), - o:list-w-params B. +func list-w-params.flatten-map + list-w-params A, + (func A -> list-w-params B) + -> list-w-params B. list-w-params.flatten-map (w-params.cons N T L) F (w-params.cons N T L1) :- @pi-parameter N T p\ list-w-params.flatten-map (L p) F (L1 p). @@ -250,8 +269,8 @@ list-w-params.flatten-map (w-params.nil N TTy L) F (w-params.nil N TTy L1) :- @pi-parameter N TTy t\ list-w-params.flatten-map.aux (L t) F (L1 t). -pred list-w-params.flatten-map.aux - i:list (w-args A), i:(A -> list-w-params B -> prop), o:list (w-args B). +func list-w-params.flatten-map.aux + list (w-args A), (func A -> list-w-params B) -> list (w-args B). list-w-params.flatten-map.aux [] _ []. list-w-params.flatten-map.aux [triple M Ps T|L] F Res1 :- F M MwP, @@ -263,7 +282,7 @@ list-w-params.flatten-map.aux [triple M Ps T|L] F Res1 :- % Params is a list of pairs (section variable, its type). % ListWParams has as many w-params.cons as TheParams and the terms % in Factories are abstracted wrt the first component of TheParams. -pred build-list-w-params i:list (triple id term term), i:term, i:list (w-args A), o: list-w-params A. +func build-list-w-params list (triple id term term), term, list (w-args A) -> list-w-params A. build-list-w-params [triple ID P Pty|PS] TheType Factories (w-params.cons ID Pty1 R) :- std.do! [ copy Pty Pty1, (@pi-parameter ID Pty1 p\ (copy P p :- !) => build-list-w-params PS TheType Factories (R p)), @@ -279,7 +298,8 @@ build-list-w-params [] TheType Factories (w-params.nil Name TT1 R) :- std.do! [ (copy-pack-holes TheType t)) (R t)), ]. -pred copy-pack-holes i:term, i:term, i:term, o:term. +:index (1) +func copy-pack-holes term, term, term -> term. copy-pack-holes TheType NewType Term Out :- std.do! [ (pi Args NewArgs CSInstance ParamsRev ParamsRevCopy Pack \ (copy (app[global Pack | Args]) (app[global Pack | NewArgs]) :- pack? Pack _, @@ -289,43 +309,43 @@ copy-pack-holes TheType NewType Term Out :- std.do! [ copy Term Out, ]. -pred pack? i:gref, o:classname. +func pack? gref -> classname. pack? (indc K) C :- coq.env.indc K _ _ _ KTy, prod-last-gref KTy (indt I), % TODO: use new API - class-def (class C (indt I) _). + std.once (class-def (class C (indt I) _)). -pred distribute-w-params i:list-w-params A, o:list (one-w-params A). +func distribute-w-params list-w-params A -> list (one-w-params A). distribute-w-params (w-params.cons N T F) L :- pi x\ distribute-w-params (F x) (L1 x), std.map (L1 x) (bind-cons N T x) L. distribute-w-params (w-params.nil N T F) L :- pi x\ std.map (F x) (bind-nil N T x) L. % Specific to one-w-params -pred w-params_1 i:one-w-params A, o:A. +func w-params_1 one-w-params A -> A. w-params_1 X Y :- w-params.then X ignore ignore (p\ t\ triple_1) Y. -pred disable-id-phant i:term, o:term. +func disable-id-phant term -> term. disable-id-phant T T1 :- (pi fresh fresh1 t v\ copy {{lib:@hb.id lp:t lp:v}} {{lib:@hb.id_disabled lp:t lp:fresh lp:v lp:fresh1}} :- !) => (pi fresh fresh1 t v\ copy {{lib:@hb.ignore lp:t lp:v}} {{lib:@hb.ignore_disabled lp:t lp:fresh lp:v lp:fresh1}} :- !) => copy T T1. -pred re-enable-id-phant i:term, o:term. +func re-enable-id-phant term -> term. re-enable-id-phant T T1 :- (pi f1 f2 t v\ copy {{lib:@hb.id_disabled lp:t lp:f1 lp:v lp:f2}} {{lib:@hb.id lp:t lp:v}} :- !) => (pi f1 f2 t v\ copy {{lib:@hb.ignore_disabled lp:t lp:f1 lp:v lp:f2}} {{lib:@hb.ignore lp:t lp:v}} :- !) => copy T T1. -pred prod-last i:term, o:term. +func prod-last term -> term. prod-last (prod N S X) Y :- !, @pi-decl N S x\ prod-last (X x) Y. prod-last X X :- !. -pred prod-last-gref i:term, o:gref. +func prod-last-gref term -> gref. prod-last-gref (prod N S X) GR :- !, @pi-decl N S x\ prod-last-gref (X x) GR. prod-last-gref X GR :- coq.term->gref X GR. % saturate a type constructor with holes -pred saturate-type-constructor i:term, o:term . +func saturate-type-constructor term -> term. saturate-type-constructor T ET :- coq.typecheck T TH ok, coq.count-prods TH N, diff --git a/HB/context.elpi b/HB/context.elpi index 4b04e5f0..53d5df32 100644 --- a/HB/context.elpi +++ b/HB/context.elpi @@ -3,7 +3,7 @@ namespace context { -pred declare i:factories, o:mixins, o:list term, o:term, o:list prop, o:list constant. +func declare factories -> mixins, list term, term, list prop, list constant. declare FLwP MLwP Params TheKey MSL CL :- !, std.do! [ factories-provide FLwP MLwPRaw, declare.params-key MLwPRaw ParamsSection TheKey _MLwA, @@ -11,7 +11,7 @@ declare FLwP MLwP Params TheKey MSL CL :- !, std.do! [ declare.mixins TheKey ParamsSection MLwPRaw MLwP MSL CL ]. -pred declare.params-key i:w-params A, o:list (triple id term term), o:term, o:A. +func declare.params-key w-params A -> list (triple id term term), term, A. declare.params-key MLwP Params TheKey Out :- !, std.do! [ if-verbose (coq.say {header} "declaring parameters and key as section variables"), declare.params MLwP Params KId KTy F, @@ -20,7 +20,7 @@ declare.params-key MLwP Params TheKey Out :- !, std.do! [ Out = F TheKey ]. -pred declare.params i:w-params A, o:list (triple id term term), o:id, o:term, o:(term -> A). +func declare.params w-params A -> list (triple id term term), id, term, (term -> A). declare.params (w-params.cons PId PTy F) [triple PId P PTy|Params] KId KTy Out :- !, std.do! [ log.coq.env.add-section-variable-noimplicits PId PTy C, P = global (const C), @@ -32,7 +32,8 @@ declare.params (w-params.nil KId KTy F) [] KId KTy F :- !. % (section) context with all the mixins provided by the factories and all % the structure instances we can derive on TheType from these. Clauses % contain mixin-src for each postulated mixin -pred declare.mixins i:term, i:list (triple id term term), i:mixins, o:mixins, o:list prop, o:list constant. +:index (1) +func declare.mixins term, list (triple id term term), mixins -> mixins, list prop, list constant. declare.mixins TheType TheParamsSection MLwPRaw MLwP MSL CL :- std.do! [ if-verbose (coq.say "Here is the list of mixins to declare (the order matters): " {list-w-params_list MLwPRaw}), @@ -55,14 +56,15 @@ namespace private { % a variable "mN" inhabiting M applied to T and % all its dependencies, previously postulated and associated % to the corresponding mixin using mixin-for -pred postulate-mixin i:term, i:w-args mixinname, i:triple (list constant) (list prop) (list (w-args mixinname)), - o:triple (list constant) (list prop) (list (w-args mixinname)). +:index (1) +func postulate-mixin term, w-args mixinname, triple (list constant) (list prop) (list (w-args mixinname)) + -> triple (list constant) (list prop) (list (w-args mixinname)). postulate-mixin TheType (triple M Ps T) (triple CL MSL MLwP) (triple OutCL [MC|MSL] [NewMwP|MLwP]) :- MSL => std.do! [ Name is "local_mixin_" ^ {gref->modname M 2 "_"}, if-verbose (coq.say "HB: postulate" Name "on" {coq.term->string T}), - synthesis.infer-all-gref-deps Ps T M TySkel, + synthesis.infer-all-gref->deps Ps T M TySkel, % was synthesis.infer-all-mixin-args Ps T M TySkel, % if-verbose (coq.say "HB: postulate-mixin checking" TySkel), % std.assert-ok! (coq.typecheck Ty _) "postulate-mixin: Ty illtyped", diff --git a/HB/export.elpi b/HB/export.elpi index 2fb15aa3..6139f8d3 100644 --- a/HB/export.elpi +++ b/HB/export.elpi @@ -1,36 +1,37 @@ /* Hierarchy Builder: algebraic hierarchies made easy This software is released under the terms of the MIT license */ -pred export.any i:id. +func export.any id ->. export.any S :- coq.locate-all S L, if (L = []) (coq.error "HB: cannot locate" S) true, if (L = [X]) (export.any.aux S X) (coq.error "HB:" S "is ambiguous:" L). -export.any.aux S (loc-gref GR) :- export.abbrev S GR. -export.any.aux S (loc-modpath MP) :- export.module S MP. +func export.any.aux id, located ->. +export.any.aux S (loc-gref GR) :- export.abbrev S GR, !. +export.any.aux S (loc-modpath MP) :- export.module S MP, !. export.any.aux S X :- coq.error "HB:" S "denotes" X "which is not supported for exporting". % [export.module Module] exports a Module now adds it to the collection of % modules to export in the end of the current enclosing module, % by the command HB.Exports % CAVEAT: "module" is a keyword, we put it in the namespace by hand -pred export.module i:id, i:modpath. +func export.module id, modpath ->. export.module NiceModule Module :- !, log.coq.env.export-module NiceModule Module, coq.env.current-library File, acc-clause current (module-to-export File NiceModule Module). -pred export.abbrev i:id, i:gref. +func export.abbrev id, gref ->. export.abbrev NiceName GR :- !, coq.env.current-library File, acc-clause current (abbrev-to-export File NiceName GR). -pred export.clause i:prop. +func export.clause prop ->. export.clause Clause :- !, coq.env.current-library File, acc-clauses current [Clause, clause-to-export File Clause]. -pred export.reexport-all-modules-and-CS i:option string. +func export.reexport-all-modules-and-CS option string ->. export.reexport-all-modules-and-CS Filter :- std.do! [ coq.env.current-library File, export.private.compute-filter Filter MFilter, @@ -72,22 +73,22 @@ export.reexport-all-modules-and-CS Filter :- std.do! [ namespace export.private { -pred abbrev-in-module i:list string, i:prop. +func abbrev-in-module list string, prop ->. abbrev-in-module PM (abbrev-to-export _ _ GR) :- coq.gref->path GR PC, - std.appendR PM _ PC. % sublist + std.prefixL PM PC. -pred module-in-module i:list string, i:prop. +func module-in-module list string, prop ->. module-in-module PM (module-to-export _ _ M) :- coq.modpath->path M PC, - std.appendR PM _ PC. % sublist + std.prefixL PM PC. -pred instance-in-module i:list string, i:prop. +func instance-in-module list string, prop ->. instance-in-module PM (instance-to-export _ _ C) :- coq.gref->path (const C) PC, - std.appendR PM _ PC. % sublist + std.prefixL PM PC. -pred compute-filter i:option string, o:list string. +func compute-filter option string -> list string. compute-filter none []. compute-filter (some S) MFilter :- % S is a component of the current modpath coq.env.current-path P, @@ -96,8 +97,10 @@ compute-filter (some S) MFilter :- % S is a component of the current modpath compute-filter (some S) MFilter :- coq.locate-module S M, coq.modpath->path M MFilter. + +func compute-filter.aux list string, list string -> list string. compute-filter.aux [S|_] [S] [S] :- !. -compute-filter.aux [S|XS] [S|SS] [S|YS] :- compute-filter.aux XS SS YS. +compute-filter.aux [S|XS] [S|SS] [S|YS] :- !, compute-filter.aux XS SS YS. compute-filter.aux [X|XS] L [X|YS] :- compute-filter.aux XS L YS. } diff --git a/HB/factory.elpi b/HB/factory.elpi index 98658b24..514b8bdc 100644 --- a/HB/factory.elpi +++ b/HB/factory.elpi @@ -3,26 +3,26 @@ namespace factory { -pred declare i:argument. +func declare argument ->. declare A :- private.declare-asset A private.asset-factory. -pred declare-mixin i:argument. +func declare-mixin argument ->. declare-mixin A :- private.declare-asset A private.asset-mixin. kind factory-abbrev type. type by-classname gref -> factory-abbrev. type by-phantabbrev abbreviation -> factory-abbrev. -pred declare-abbrev i:id, i:factory-abbrev, o:abbreviation. +:index (_ 1) +func declare-abbrev id, factory-abbrev -> abbreviation. declare-abbrev Name (by-classname GR) Abbrev :- % looks fishy (the parameters are not taken into account) @global! => log.coq.notation.add-abbreviation Name 1 (fun _ _ t\ app[global GR,t]) tt Abbrev. -declare-abbrev Name (by-phantabbrev Abbr) Abbrev :- std.do! [ +declare-abbrev Name (by-phantabbrev Abbr) Abbrev :- coq.notation.abbreviation-body Abbr Nargs AbbrTrm, - @global! => log.coq.notation.add-abbreviation Name Nargs AbbrTrm tt Abbrev, -]. + @global! => log.coq.notation.add-abbreviation Name Nargs AbbrTrm tt Abbrev. -pred argument->w-mixins i:argument, o:w-mixins argument. +func argument->w-mixins argument -> w-mixins argument. argument->w-mixins (indt-decl Decl) (pr MLwP ArgwP) :- !, std.do! [ pdecl->w-mixins Decl (pr MLwP DeclwP), w-params.map DeclwP (_\ _\ x\ y\ y = indt-decl x) ArgwP @@ -50,27 +50,37 @@ argument->w-mixins (ctx-decl Decl) (pr MLwP ArgwP) :- !, std.do! [ w-params.map DeclwP (_\ _\ x\ y\ y = ctx-decl x) ArgwP ]. -pred argument-name i:argument, o:string. -argument-name (const-decl Id _ _) Id :- !. -argument-name (indt-decl (parameter _ _ _ R)) Id :- !, -argument-name (indt-decl (R (sort prop))) Id. -argument-name (indt-decl (record Id _ _ _)) Id :- !. -argument-name (indt-decl (inductive Id _ _ _)) Id :- !. +func argument-name argument -> string. +argument-name (const-decl Id _ _) Id. +argument-name (indt-decl (parameter _ _ _ R)) Id :- + argument-name (indt-decl (R (sort prop))) Id. +argument-name (indt-decl (record Id _ _ _)) Id. +argument-name (indt-decl (inductive Id _ _ _)) Id. argument-name (ctx-decl _) "_" :- !. -pred pdecl->w-mixins i:indt-decl, o:w-mixins indt-decl. -pred pdecl->w-mixins i:arity, o:w-mixins arity. -pdecl->w-mixins (parameter ID _ TySkel Rest as Decl) Out :- +func pdecl->w-mixins indt-decl -> w-mixins indt-decl. +pdecl->w-mixins ((parameter ID _ TySkel Rest : indt-decl) as Decl) Out :- + private.is-key Decl, !, + private.key-decl-w-mixins "parameter" + ID TySkel Rest private.pdecl->w-mixins.mixins Out. +pdecl->w-mixins (parameter ID _ TySkel Rest : indt-decl) Out :- !, + private.param-decl-w-mixins "parameter" + ID TySkel Rest pdecl->w-mixins Out. +pdecl->w-mixins (_ : indt-decl) _ :- !, + coq.error "HB: declaration must have at least one parameter". + +func pdecl->w-mixins arity -> w-mixins arity. +pdecl->w-mixins ((parameter ID _ TySkel Rest : arity) as Decl) (Out:w-mixins arity) :- private.is-key Decl, !, private.key-decl-w-mixins "parameter" ID TySkel Rest private.pdecl->w-mixins.mixins Out. -pdecl->w-mixins (parameter ID _ TySkel Rest) Out :- !, +pdecl->w-mixins (parameter ID _ TySkel Rest : arity) (Out:w-mixins arity) :- !, private.param-decl-w-mixins "parameter" ID TySkel Rest pdecl->w-mixins Out. -pdecl->w-mixins _ _ :- !, +pdecl->w-mixins (_ : arity) _ :- !, coq.error "HB: declaration must have at least one parameter". -pred cdecl->w-mixins i:context-decl, o:w-mixins context-decl. +func cdecl->w-mixins context-decl -> w-mixins context-decl. cdecl->w-mixins (context-item _ _ _ (some _) _) _ :- !, coq.error "HB: local definition is not supported in this context". cdecl->w-mixins (context-item ID _ TySkel none Rest as Decl) Out :- @@ -96,30 +106,35 @@ kind asset type. type asset-mixin asset. type asset-factory asset. -pred check-key-attribute-consistency i:id. +func check-key-attribute-consistency id ->. check-key-attribute-consistency _ :- not(get-option "key" _), !. check-key-attribute-consistency ID :- get-option "key" ID, !. -check-key-attribute-consistency ID :- get-option "key" ID1, +check-key-attribute-consistency ID :- get-option "key" ID1, !, coq.error "HB:" {calc ("The #[key=\"" ^ ID1 ^ "\"] attribute")} "does not match the selected subject" ID. -pred is-key i:indt-decl. -pred is-key i:arity. -pred is-key i:context-decl. -is-key (parameter ID _ _ _\ record _ _ _ _) :- !, check-key-attribute-consistency ID. -is-key (parameter ID _ _ _\ inductive _ _ _ _) :- !, check-key-attribute-consistency ID. -is-key (parameter ID _ _ _\ arity _) :- !, check-key-attribute-consistency ID. -is-key (context-item ID _ _ _ _\ context-end) :- !, check-key-attribute-consistency ID. -is-key (parameter ID _ _ _) :- get-option "key" ID, !. -is-key (context-item ID _ _ _ _) :- get-option "key" ID, !. -is-key (parameter ID _ _ p\ parameter _ _ (M p) _) :- +func is-key indt-decl ->. +is-key (parameter ID _ _ _\ record _ _ _ _ : indt-decl) :- !, check-key-attribute-consistency ID. +is-key (parameter ID _ _ _\ inductive _ _ _ _ : indt-decl) :- !, check-key-attribute-consistency ID. +is-key (parameter ID _ _ _ : indt-decl) :- get-option "key" ID, !. +is-key (parameter ID _ _ p\ parameter _ _ (M p) _ : indt-decl) :- pi p\ factory? (M p) _, !, check-key-attribute-consistency ID. -is-key (context-item ID _ _ _ p\ context-item _ _ (M p) _ _) :- + +func is-key arity ->. +is-key (parameter ID _ _ _\ arity _ : arity) :- !, check-key-attribute-consistency ID. +is-key (parameter ID _ _ _ : arity) :- get-option "key" ID, !. +is-key (parameter ID _ _ p\ parameter _ _ (M p) _ : arity) :- + pi p\ factory? (M p) _, !, check-key-attribute-consistency ID. + +func is-key context-decl ->. +is-key ((context-item ID _ _ _ _\ context-end) : context-decl) :- !, check-key-attribute-consistency ID. +is-key (context-item ID _ _ _ _ : context-decl) :- get-option "key" ID, !. +is-key (context-item ID _ _ _ p\ context-item _ _ (M p) _ _ : context-decl) :- pi p\ factory? (M p) _, !, check-key-attribute-consistency ID. -pred mixin-decl-w-mixins i:string, i:string, i:term, i:(term -> A), - i:(A -> pair (list (w-args mixinname)) A -> prop), - o:pair (list (w-args mixinname)) A. +func mixin-decl-w-mixins string, string, term, (term -> A), + (pred i:A, o:pair (list (w-args mixinname)) A) + -> pair (list (w-args mixinname)) A. mixin-decl-w-mixins DeclKind ID TySkel Rest Conv Out :- std.do! [ if-verbose (coq.say {header} "processing mixin" DeclKind ID), std.assert! (not (var TySkel)) "HB: no type provided for mixin", @@ -134,9 +149,10 @@ mixin-decl-w-mixins DeclKind ID TySkel Rest Conv Out :- std.do! [ Dummy = sort prop, Conv (Rest Dummy) (pr MLwA R), Out = pr [triple F Ps T|MLwA] R ]. -pred key-decl-w-mixins i:string, i:string, i:term, i:(term -> A), - i:(A -> pair (list (w-args mixinname)) A -> prop), - o:pair mixins (w-params A). +:index(1) +func key-decl-w-mixins string, string, term, (term -> A), + (pred i:A, o:pair (list (w-args mixinname)) A) -> + pair mixins (w-params A). key-decl-w-mixins DeclKind ID TySkel Rest Conv Out :- std.do! [ if-verbose (coq.say {header} "processing key" DeclKind), std.assert-ok! (coq.elaborate-ty-skeleton TySkel _ Ty) "key illtyped", @@ -144,26 +160,30 @@ key-decl-w-mixins DeclKind ID TySkel Rest Conv Out :- std.do! [ if (var Ty) (fresh-type Ty) true, Out = pr (w-params.nil ID Ty MLwA) (w-params.nil ID Ty R) ]. -pred param-decl-w-mixins i:string, i:string, i:term, i:(term -> A), - i:(A -> pair mixins (w-params A) -> prop), o:pair mixins (w-params A). -param-decl-w-mixins DeclKind ID TySkel Rest Conv Out :- std.do! [ +:index (1) +func param-decl-w-mixins string, string, term, (term -> A), + (func A -> pair mixins (w-params A)) -> pair mixins (w-params A). +param-decl-w-mixins DeclKind ID TySkel Rest Conv Out :- if-verbose (coq.say {header} "processing param" DeclKind), std.assert-ok! (coq.elaborate-ty-skeleton TySkel _ Ty) "param illtyped", coq.string->name ID N, @pi-decl N Ty p\ Conv (Rest p) (pr (MLwP p) (R p)), if (var Ty) (fresh-type Ty) true, - Out = pr (w-params.cons ID Ty MLwP) (w-params.cons ID Ty R) -]. + Out = pr (w-params.cons ID Ty MLwP) (w-params.cons ID Ty R). -pred pdecl->w-mixins.mixins i:indt-decl, - o:pair (list (w-args mixinname)) indt-decl. -pred pdecl->w-mixins.mixins i:arity, - o:pair (list (w-args mixinname)) arity. -pdecl->w-mixins.mixins (parameter ID _ TySkel Rest) Out :- !, +func pdecl->w-mixins.mixins indt-decl + -> pair (list (w-args mixinname)) indt-decl. +pdecl->w-mixins.mixins (parameter ID _ TySkel Rest : indt-decl) Out :- !, mixin-decl-w-mixins "parameter" ID TySkel Rest pdecl->w-mixins.mixins Out. -pdecl->w-mixins.mixins R (pr [] R) :- !. +pdecl->w-mixins.mixins (R : indt-decl) (pr [] R) :- !. -pred cdecl->w-mixins.mixins i:context-decl, - o:pair (list (w-args mixinname)) context-decl. +func pdecl->w-mixins.mixins arity + -> pair (list (w-args mixinname)) arity. +pdecl->w-mixins.mixins (parameter ID _ TySkel Rest : arity) Out :- !, + mixin-decl-w-mixins "parameter" ID TySkel Rest pdecl->w-mixins.mixins Out. +pdecl->w-mixins.mixins (R : arity) (pr [] R) :- !. + +func cdecl->w-mixins.mixins context-decl + -> pair (list (w-args mixinname)) context-decl. cdecl->w-mixins.mixins context-end (pr [] context-end) :- !. cdecl->w-mixins.mixins (context-item _ _ _ (some _) _) _ :- !, coq.error "HB: local definition is not supported in this context". @@ -171,33 +191,32 @@ cdecl->w-mixins.mixins (context-item ID _ TySkel none Rest) Out :- !, mixin-decl-w-mixins "parameter" ID TySkel Rest cdecl->w-mixins.mixins Out. % The identity builder -pred declare-id-builder i:factoryname, o:prop. +func declare-id-builder factoryname -> prop. declare-id-builder GR (from GR GR (const C)) :- std.do! [ - gref-deps GR GRD, + gref->deps GR GRD, synthesis.mixins-w-params.fun GRD (declare-id-builder.aux GR) IDBodySkel, std.assert-ok! (coq.elaborate-skeleton IDBodySkel IDType IDBody) "identity builder illtyped", log.coq.env.add-const-noimplicits "identity_builder" IDBody IDType @transparent! C, ]. declare-id-builder.aux GR Params TheType (fun `x` Ty x\x) :- - synthesis.infer-all-gref-deps Params TheType GR Ty. + synthesis.infer-all-gref->deps Params TheType GR Ty. % [mk-factory-abbrev Str GR CL FactAbbrev] % creates an abbreviation for GR names Str and creates a phant-abbrev clause in CL. % FactAbbrev is the short name for the factory (either an alias of the class record) -pred mk-factory-abbrev i:string, i:gref, o:list prop, o:factory-abbrev. -mk-factory-abbrev Str GR Aliases FactAbbrev :- !, std.do! [ +func mk-factory-abbrev string, gref -> list prop, factory-abbrev. +mk-factory-abbrev Str GR Aliases FactAbbrev :- if (factory-alias->gref GR _ ok) (Aliases = [], FactAbbrev = by-classname GR) (phant.of-gref ff GR [] PhTerm, phant.add-abbreviation Str PhTerm PhC Abbrv, Aliases = [phant-abbrev GR (const PhC) Abbrv], - FactAbbrev = by-phantabbrev Abbrv), -]. + FactAbbrev = by-phantabbrev Abbrv). % [declare-asset Asset AssetKind] unifies the code paths for % mixins, factories (and alias factories) -pred declare-asset i:argument, i:asset. +func declare-asset argument, asset ->. declare-asset Arg AssetKind :- std.do! [ argument-name Arg Module, if-verbose (coq.say {header} "start module and section" Module), @@ -226,8 +245,9 @@ declare-asset Arg AssetKind :- std.do! [ ) ]. -pred declare-mixin-or-factory i:list prop, i:list constant, i:list term, i:term, - i:term, i:record-decl, i:list-w-params factoryname, i:id, i:asset. +:index(1) +func declare-mixin-or-factory list prop, list constant, list term, term, + term, record-decl, list-w-params factoryname, id, asset. declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance TheParams TheType Sort1 Fields GRFSwP Module D :- std.do! [ @@ -255,7 +275,7 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance factories-provide GRFSwP MLwP, w-params.nparams MLwP NParams, build-deps-for-projections R MLwP GRDepsClausesProjs, - GRDepsClauses = [gref-deps (indt R) MLwP, gref-deps (indc K) MLwP|GRDepsClausesProjs], + GRDepsClauses = [gref->deps (indt R) MLwP, gref->deps (indc K) MLwP|GRDepsClausesProjs], % GRDepsClauses => mk-factory-sort MLwP (indt R) _ FactorySortCoe, % FactorySortCoe = coercion GRFSort _ _ _, @@ -279,11 +299,11 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance log.coq.env.begin-module "Exports" none, std.flatten [Clauses, GRDepsClauses, [ - factory-constructor (indt R) GRK, - factory-nparams (indt R) NParams, - factory-builder-nparams BuildConst NParams, + is-factory (indt R), + factory->constructor (indt R) GRK, + factory->nparams (indt R) NParams, phant-abbrev GRK (const BuildConst) BuildAbbrev, - % gref-deps GRFSort MLwP, + % gref->deps GRFSort MLwP, % factory-sort FactorySortCoe, ]] NewClauses, acc-clauses current NewClauses, @@ -307,8 +327,9 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance ]. -pred declare-factory-alias i:list prop, i:list constant, i:list term, i:term, - i:term, i:list-w-params factoryname, i:id. +:index (1) +func declare-factory-alias list prop, list constant, list term, term, + term, list-w-params factoryname, id. declare-factory-alias MixinSrcClauses SectionCanonicalInstance TheParams TheType Ty1Skel GRFSwP Module :- std.do! [ @@ -320,9 +341,9 @@ declare-factory-alias MixinSrcClauses SectionCanonicalInstance std.assert! (safe-dest-app Ty1 (global PhF) _Args) "Argument must be a factory", std.assert-ok! (factory-alias->gref PhF F) "HB", - std.assert! (factory-constructor F FK) "BUG: Factory constructor missing", + std.assert! (factory->constructor F FK) "BUG: Factory constructor missing", - MixinSrcClauses => synthesis.infer-all-gref-deps TheParams TheType FK MFK, + MixinSrcClauses => synthesis.infer-all-gref->deps TheParams TheType FK MFK, std.assert-ok! (coq.typecheck MFK MFKTy) "BUG: typecking of former factory constructor failed", (pi Args\ copy (app[global F|Args]) (app[global (const C)|Section])) => copy MFKTy MFKTyC, @@ -336,16 +357,16 @@ declare-factory-alias MixinSrcClauses SectionCanonicalInstance @global! => log.coq.arguments.set-implicit GRK [[]], factories-provide GRFSwP MLwP, - GRDepsClauses = [gref-deps (const C) MLwP, gref-deps (const CK) MLwP], + GRDepsClauses = [gref->deps (const C) MLwP, gref->deps (const CK) MLwP], GRDepsClauses => phant.of-gref ff GRK [] PhGRK0, % GRDepsClauses => mk-factory-sort MLwP (const C) _ FactorySortCoe, % FactorySortCoe = coercion GRFSort _ _ _, - if (mixin-first-class F _) (PhGRK = PhGRK0) + if (mixin->first-class F _) (PhGRK = PhGRK0) (phant.append-fun-unify PhGRK0 PhGRK), - GRDepsClauses => phant.add-abbreviation "Build" PhGRK BuildConst _, + GRDepsClauses => phant.add-abbreviation "Build" PhGRK _ _, GRDepsClauses => mk-factory-abbrev "axioms" (const C) Clauses FactAbbrev, @@ -355,10 +376,10 @@ declare-factory-alias MixinSrcClauses SectionCanonicalInstance w-params.nparams MLwP NParams, std.flatten [ Clauses, GRDepsClauses, - [ factory-nparams (const C) NParams, - factory-constructor (const C) GRK, - factory-builder-nparams BuildConst NParams, - % gref-deps GRFSort MLwP, + [ is-factory (const C), + factory->nparams (const C) NParams, + factory->constructor (const C) GRK, + % gref->deps GRFSort MLwP, % factory-sort FactorySortCoe ] ] NewClauses, @@ -381,18 +402,19 @@ declare-factory-alias MixinSrcClauses SectionCanonicalInstance % [build-deps-for-projections I ML CL] builds a [gref-dep] for each projection P % of I such that P depends on "ML @ [I]" (each operation depends on the the % deps of the record plus the record itself) -pred build-deps-for-projections i:inductive, i:mixins, o:list prop. +func build-deps-for-projections inductive, mixins -> list prop. build-deps-for-projections R MLwP CL :- std.do! [ compat.map-filter {coq.env.projections R} (x\y\x = some y) MixinOps, list-w-params.rcons MLwP (pl\t\r\ r = triple (indt R) pl t) MLRwP, - std.map MixinOps (gr\r\ r = gref-deps (const gr) MLRwP) CL, + std.map MixinOps (gr\r\ r = gref->deps (const gr) MLRwP) CL, ]. % Section handling in Coq is smart, in the sense it it only abstracts over % variables that aoccur. We don't want that for mixin/factories, so we implement % our own discharging. Note that definitions (like canonical instance) have % to be abstracted too. -pred abstract-over-section i:list term, i:term, i:list prop, i:list constant, i:(list constant -> A -> A -> prop), i:A, o:A, o:list term. +:index (1) +func abstract-over-section list term, term, list prop, list constant, (func list constant, A -> A), A -> A, list term. abstract-over-section TheParams TheType MixinSrcClauses SectionCanonicalInstance F X X1 Section :- % compute section variables to be used for discharging std.map MixinSrcClauses mixin-src_src Mixins, @@ -403,7 +425,7 @@ abstract-over-section TheParams TheType MixinSrcClauses SectionCanonicalInstance coq.copy-clauses-for-unfold SectionCanonicalInstance CopyUnfold, CopyUnfold => F SectionVars X X1. -pred mk-factory-sort i:mixins, i:gref, o:gref, o:coercion. +func mk-factory-sort mixins, gref -> gref, coercion. mk-factory-sort MLwP GR (const FactorySortCst) Coe :- if-verbose (coq.say {header} "declaring tagged sort for GR=" GR), synthesis.mixins-w-params.fun MLwP (mk-factory-sort.term GR) FactorySort, @@ -414,8 +436,8 @@ mk-factory-sort MLwP GR (const FactorySortCst) Coe :- (@global! => log.coq.arguments.set-implicit (const FactorySortCst) [MLwPImplicits]), synthesis.infer-coercion-tgt MLwP CoeClass, Coe = coercion (const FactorySortCst) MLwPLength GR CoeClass. -pred mk-factory-sort.term i:gref, i:list term, i:term, o:term. -mk-factory-sort.term GR P T (fun `_` Ty _\ T) :- synthesis.infer-all-gref-deps P T GR Ty. +func mk-factory-sort.term gref, list term, term -> term. +mk-factory-sort.term GR P T (fun `_` Ty _\ T) :- synthesis.infer-all-gref->deps P T GR Ty. diff --git a/HB/graph.elpi b/HB/graph.elpi index b251c2f3..ead73a8b 100644 --- a/HB/graph.elpi +++ b/HB/graph.elpi @@ -3,7 +3,7 @@ namespace graph { -pred to-file i:string. +func to-file string ->. to-file File :- !, std.do! [ open_out File OC, output OC "digraph Hierarchy { ", @@ -18,7 +18,7 @@ to-file File :- !, std.do! [ namespace private { -pred pp-coercion-dot i:out_stream, i:coercion. +func pp-coercion-dot out_stream, coercion ->. pp-coercion-dot OC (coercion _ _ Src (grefclass Tgt)) :- class-def (class Src _ _), class-def (class Tgt _ _), !, std.do! [ output OC {gref->modname_short Tgt "_"}, output OC " -> ", diff --git a/HB/howto.elpi b/HB/howto.elpi index 7d6b6a23..9f65544f 100644 --- a/HB/howto.elpi +++ b/HB/howto.elpi @@ -3,13 +3,16 @@ namespace howto { -pred main-trm i:term, i:string, i:option int. +:index (1) +func main-trm term, string, option int ->. main-trm T STgt Depth :- coq.term->gref T GR, main-gref GR STgt Depth. -pred main-str i:string, i:string, i:option int. +:index (1) +func main-str string, string, option int ->. main-str S STgt Depth :- coq.locate S GR, main-gref GR STgt Depth. -pred main-gref i:gref, i:string, i:option int. +:index (1) +func main-gref gref, string, option int ->. main-gref GR STgt Depth :- class-def (class _ GR _), !, private.mixins-in-structures [GR] MLSrc, main-from MLSrc STgt Depth. @@ -18,15 +21,20 @@ main-gref GR STgt Depth :- private.mixins-in-structures SL MLSrc, main-from MLSrc STgt Depth. -pred main-from i:list mixinname, i:string, i:option int. +:index (1) +func main-from list mixinname, string, option int ->. main-from MLSrc STgt Depth :- private.mixins-in-structures [{coq.locate STgt}] MLTgt, private.list-diff MLTgt MLSrc ML, if (ML = []) (coq.say "HB: nothing to do.") (main-from.aux MLSrc ML Depth). + +:index (_ _ 1) +func main-from.aux list mixinname, list mixinname, option int ->. main-from.aux MLSrc ML (some Depth) :- main-increase-depth MLSrc ML Depth false. main-from.aux MLSrc ML none :- main-increase-depth MLSrc ML 3 true. -pred main-increase-depth i:list mixinname, i:list mixinname, i:int, i:prop. +:index (1) +func main-increase-depth list mixinname, list mixinname, int, prop. main-increase-depth MLSrc ML Depth AutoIncrease :- private.paths-from-for-step MLSrc ML Depth R, if (not (R = [])) (private.pp-solutions R) @@ -46,49 +54,58 @@ namespace private { shorten coq.pp.{ v , hov , spc , str , box , glue }. % L1 \subseteq L2 -pred incl i:list A, i:list A. -incl L1 L2 :- std.forall L1 (std.mem L2). +func incl list A, list A ->. +incl L1 L2 :- std.forall L1 (std.mem! L2). % R = L1 \ L2 -pred list-diff i:list A, i:list A, o:list A. +func list-diff list A, list A -> list A. list-diff L1 L2 R :- std.filter L1 (about.not1 (std.mem L2)) R. % R = L1 U L2 -pred union i:list A, i:list A, o:list A. +func union list A, list A -> list A. union L1 L2 R :- std.fold L2 L1 (x\l\l'\if (std.mem l x) (l' = l) (l' = [x|l])) R. -pred insert-sorted i:(A -> A -> prop), i:A, i:list A, o:list A. +func insert-sorted (func A, A ->), A, list A -> list A. insert-sorted _ X [] [X] :- !. insert-sorted Rel X [Y|T] [X,Y|T] :- Rel X Y, !. insert-sorted Rel X [Y|T] [Y|T'] :- insert-sorted Rel X T T', !. -pred lt-gref i:gref, i:gref. +func lt-gref gref, gref. lt-gref X Y :- gref->modname_short X "." SX, gref->modname_short Y "." SY, !, SX s< SY. -pred size-order i:(list A -> list A -> prop), i:list A, i:list A. +func size-order (pred i:list A, i:list A), list A, list A. size-order Rel L1 L2 :- - std.length L1 S1, std.length L2 S2, !, (S1 i< S2; (S1 = S2, !, Rel L1 L2)). + std.length L1 S1, std.length L2 S2, size-order.aux Rel L1 S1 L2 S2. + +func size-order.aux (pred i:list A, i:list A), list A, int, list A, int. +size-order.aux _ _L1 S1 _L2 S2 :- S1 i< S2, !. +size-order.aux Rel L1 S1 L2 S2 :- S1 = S2, Rel L1 L2, !. -pred lexi-order i:list gref, i:list gref. +:index (1 1) +func lexi-order list gref, list gref. lexi-order [] []. -lexi-order [X1|_] [X2|_] :- lt-gref X1 X2. +lexi-order [X1|_] [X2|_] :- lt-gref X1 X2, !. lexi-order [X|T1] [X|T2] :- lexi-order T1 T2. % [structures-on-gref GR ML] list structures [GR] is equipped with -pred structures-on-gref i:gref, o:list structure. +func structures-on-gref gref -> list structure. structures-on-gref GR SL :- std.filter {coq.CS.db-for _ (cs-gref GR)} (about.not1 about.unif-hint?) LV, std.map LV structures-on-gref.aux SL. + +func structures-on-gref.aux cs-instance -> structure. structures-on-gref.aux (cs-instance _ _ GR) F :- - coq.prod-tgt->gref {coq.env.typeof GR} F, class-def (class _ F _). + coq.prod-tgt->gref {coq.env.typeof GR} F, std.once (class-def (class _ F _)). % [mixins-in-structures SL ML] list mixins in structures [SL] -pred mixins-in-structures i:list structure, o:list mixinname. +func mixins-in-structures list structure -> list mixinname. mixins-in-structures SL ML :- std.fold SL [] mixins-in-structures.aux ML. + +func mixins-in-structures.aux structure, list mixinname -> list mixinname. mixins-in-structures.aux F L L' :- - class-def (class _ F MLWP), union L {list-w-params_list MLWP} L'. + std.once (class-def (class _ F MLWP)), union L {list-w-params_list MLWP} L'. % a type to store a factory along with the mixins it depends on % and the mixins it provides @@ -96,19 +113,20 @@ kind factory_deps_prov type. type fdp factoryname -> list mixinname -> list mixinname -> factory_deps_prov. % get all available factories in the above type -pred list_factories o:list factory_deps_prov. +func list_factories -> list factory_deps_prov. list_factories FL :- - std.map-filter {std.findall (factory-constructor _ _)} list_factories.aux FL. -list_factories.aux (factory-constructor F _) (fdp F DML PML) :- - gref-deps F FD, + std.map-filter {findall-factory->constructor} list_factories.aux FL. +func list_factories.aux prop -> howto.private.factory_deps_prov. +list_factories.aux (factory->constructor F _) (fdp F DML PML) :- + gref->deps F FD, list-w-params_list FD DML, list-w-params_list {factory-provides F} PML. % [paths-from-for-step MLSrc ML K R] returns in [R] a list of sequences % of at most [K] factories that could, starting from mixins [MLSrc], % build exactly the mixins [ML] -pred paths-from-for-step i:list mixinname, i:list mixinname, i:int, - o:list (list factoryname). +func paths-from-for-step list mixinname, list mixinname, int + -> list (list factoryname). paths-from-for-step MLSrc ML K R :- std.filter {list_factories} (fd\sigma pml\fd = fdp _ _ pml, incl pml ML) FL, paths-from-for-step-using MLSrc ML K [] [] FL _ R. @@ -117,10 +135,11 @@ paths-from-for-step MLSrc ML K R :- % same as [paths-from-for-step MLSrc ML K R] using only factories in [FL] % [Pre] is a (sorted) prefix that is looked into the list of known (sorted) % prefixes [KnownPre] to avoid generating identical solutions up to permutations -pred paths-from-for-step-using i:list mixinname, i:list mixinname, i:int, - i:list factoryname, i:list (list factoryname), i:list factory_deps_prov, - o:list (list factoryname), o:list (list factoryname). -paths-from-for-step-using _ _ K _ KnownPre _ KnownPre [] :- K i< 0. +:index (1) +func paths-from-for-step-using list mixinname, list mixinname, int, + list factoryname, list (list factoryname), list factory_deps_prov + -> list (list factoryname), list (list factoryname). +paths-from-for-step-using _ _ K _ KnownPre _ KnownPre [] :- K i< 0, !. paths-from-for-step-using _ _ _ Pre KnownPre _ KnownPre [] :- std.mem KnownPre Pre, !. paths-from-for-step-using _ [] _ Pre KnownPre _ [Pre|KnownPre] [[]] :- !. @@ -130,6 +149,11 @@ paths-from-for-step-using MLSrc ML K Pre KnownPre FL [Pre|KnownPre'] R :- std.fold FLdep (pr KnownPre []) (paths-from-for-step-using.aux MLSrc ML FL K' Pre) (pr KnownPre' R). + +func paths-from-for-step-using.aux list mixinname, list mixinname, + list factory_deps_prov -> + int, list factoryname, factory_deps_prov, + pair (list (list factoryname)) (list (list factoryname)), pair (list (list factoryname)) (list (list factoryname)). paths-from-for-step-using.aux MLSrc ML FL' K' Pre (fdp F _ MLF) (pr KnPre L) (pr KnPre' R) :- std.append MLSrc MLF MLSrc', @@ -140,7 +164,7 @@ paths-from-for-step-using.aux MLSrc ML FL' K' Pre (fdp F _ MLF) (pr KnPre L) std.map R' (l\r\r = [F|l]) R'', std.append L R'' R. -pred pp-solutions i:list (list factoryname). +func pp-solutions list (list factoryname) ->. pp-solutions LLF :- std.sort LLF (size-order lexi-order) SLLF, % format @@ -153,7 +177,7 @@ pp-solutions LLF :- coq.say "For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances", coq.say. -pred pp-solution i:list factoryname, o:coq.pp. +func pp-solution list factoryname -> coq.pp. pp-solution L (box (hov 0) PLS) :- std.map L about.pp-module PL, std.intersperse (glue [str ";", spc]) PL PLS. diff --git a/HB/instance.elpi b/HB/instance.elpi index c562ce6b..4eaf022a 100644 --- a/HB/instance.elpi +++ b/HB/instance.elpi @@ -5,7 +5,7 @@ namespace instance { % [declare-existing T F] equips T with all the canonical structures that can be % built using factory instance F -pred declare-existing i:argument, i:argument. +func declare-existing argument, argument ->. declare-existing T0 F0 :- std.do! [ argument->ty T0 T, % TODO: change this when supporting morphism hierarchies argument->term F0 F, @@ -22,7 +22,7 @@ declare-existing T0 F0 :- std.do! [ % and equips the type the factory is used on with all the canonical structures % that can be built using factory instance B. CFL contains the list of % factories being defined, CSL the list of canonical structures being defined. -pred declare-const i:id, i:term, i:arity, o:list (pair id constant), o:list (pair id constant). +func declare-const id, term, arity -> list (pair id constant), list (pair id constant). declare-const Name BodySkel TyWPSkel CFL CSL :- std.do! [ std.assert-ok! (coq.elaborate-arity-skeleton TyWPSkel _ TyWP) "Definition type illtyped", coq.arity->term TyWP Ty, @@ -44,7 +44,7 @@ declare-const Name BodySkel TyWPSkel CFL CSL :- std.do! [ % identify the factory std.assert! (coq.safe-dest-app SectionTy (global FactoryAlias) Args) "The type of the instance is not a factory", std.assert-ok! (factory-alias->gref FactoryAlias Factory) "HB", - std.assert! (factory-nparams Factory NParams) "Not a factory synthesized by HB", + std.assert! (factory->nparams Factory NParams) "Not a factory synthesized by HB", % declare the constant for the factory instance private.hack-section-discharging SectionBody SectionBodyHack, @@ -88,7 +88,7 @@ declare-const Name BodySkel TyWPSkel CFL CSL :- std.do! [ ]. % [not-subclass-of X C] holds if C does not inherit from X -pred not-subclass-of i:classname, i:class. +func not-subclass-of classname, class ->. not-subclass-of HasNoInstance (class C _ _) :- not(sub-class C HasNoInstance _ _). % [declare-all T CL MCSTL] given a type T and a list of class definition @@ -97,18 +97,13 @@ not-subclass-of HasNoInstance (class C _ _) :- not(sub-class C HasNoInstance _ _ % rest. For each fulfilled class it declares a local constant inhabiting the % corresponding structure and declares it canonical. % Each mixin used in order to fulfill a class is returned together with its name. -pred declare-all i:term, i:list class, o:list (pair id constant). +func declare-all term, list class -> list (pair id constant). declare-all _ [] []. declare-all T [class _ Struct _|Rest] L :- has-instance T Struct, !, declare-all T Rest L. declare-all T [class Class Struct MLwP|Rest] [pr Name CS|L] :- - - infer-class T Class Struct MLwP S Name STy Clauses, - - !, - + infer-class T Class Struct MLwP S Name STy Clauses, !, decl-const-in-struct Name S STy CS, - Clauses => declare-all T Rest L. declare-all T [class HasNoInstance _ _|Rest] L :- @@ -118,7 +113,8 @@ declare-all T [class HasNoInstance _ _|Rest] L :- % for generic types, we need first to instantiate them by giving them holes, % so they can be used to instantiate the classes -pred declare-all-on-type-constructor i:term, i:list class, o:list (pair id constant). +:index (_ 2) +func declare-all-on-type-constructor term, list class -> list (pair id constant). declare-all-on-type-constructor _ [] []. declare-all-on-type-constructor TK [class _ Struct _|Rest] L :- saturate-type-constructor TK T, has-instance T Struct, !, declare-all-on-type-constructor TK Rest L. @@ -127,16 +123,12 @@ declare-all-on-type-constructor TK [class Class Struct MLwP|Rest] [pr Name CS|L] %TODO: compute the arity of the Class subject and saturate up to that point % there may even be more than one possibility saturate-type-constructor TK T, - - infer-class T Class Struct MLwP S Name _STy Clauses, - - !, + infer-class T Class Struct MLwP S Name _STy Clauses, !, abstract-holes.main S SC, std.assert-ok! (coq.typecheck SC SCTy) "declare-all-on-type-constructor: badly closed", decl-const-in-struct Name SC SCTy CS, - Clauses => declare-all-on-type-constructor TK Rest L. declare-all-on-type-constructor TK [class HasNoInstance _ _|Rest] L :- @@ -144,7 +136,7 @@ declare-all-on-type-constructor TK [class HasNoInstance _ _|Rest] L :- std.filter Rest (not-subclass-of HasNoInstance) Rest1, declare-all-on-type-constructor TK Rest1 L. -pred has-instance i:term, i:structure. +func has-instance term, structure ->. has-instance T Struct :- if (has-CS-instance? T Struct) (if-verbose (coq.say {header} "skipping already existing" @@ -152,7 +144,7 @@ has-instance T Struct :- {coq.term->string T})) fail. % we build it -pred infer-class i:term, i:classname, i:gref, i:factories, o:term, o:string, o:term, o:list prop. +func infer-class term, classname, gref, factories -> term, string, term, list prop. infer-class T Class Struct MLwP S Name STy Clauses:- std.do![ params->holes MLwP Params, @@ -178,7 +170,7 @@ infer-class T Class Struct MLwP S Name STy Clauses:- std.do![ ]. -pred decl-const-in-struct i:string, i:term, i:term, i:constant. +func decl-const-in-struct string, term, term, constant ->. decl-const-in-struct Name S STy CS:- std.do![ if (ground_term S) (S1 = S, STy1 = STy) @@ -192,7 +184,7 @@ decl-const-in-struct Name S STy CS:- std.do![ ]. -pred declare-factory-sort-deps i:gref. +func declare-factory-sort-deps gref ->. declare-factory-sort-deps GR :- std.do! [ if-verbose (coq.say {header} "required instances on factory sort for" GR), Name is "SortInstances" ^ {std.any->string {new_int}}, @@ -204,7 +196,7 @@ declare-factory-sort-deps GR :- std.do! [ std.forall CSL (x\ sigma CS\ x = pr _ CS, log.coq.CS.declare-instance CS) ]. -pred declare-factory-sort-factory i:gref. +func declare-factory-sort-factory gref ->. declare-factory-sort-factory GR :- std.do! [ if-verbose (coq.say {header} "required instances on factory sort for" GR), Name is "SortInstances" ^ {std.any->string {new_int}}, @@ -218,16 +210,16 @@ declare-factory-sort-factory GR :- std.do! [ pred context.declare i:factories, o:mixins, o:list term, o:term, o:list prop, o:list constant. -pred mk-factory-sort-deps i:gref, o:list (pair id constant). +func mk-factory-sort-deps gref -> list (pair id constant). mk-factory-sort-deps AliasGR CSL :- std.do! [ std.assert-ok! (factory-alias->gref AliasGR GR) "HB: mk-factory-sort-deps", - gref-deps GR MLwPRaw, + gref->deps GR MLwPRaw, context.declare MLwPRaw MLwP SortParams SortKey SortMSL _, - SortMSL => synthesis.infer-all-gref-deps SortParams SortKey GR FSort, + SortMSL => synthesis.infer-all-gref->deps SortParams SortKey GR FSort, log.coq.env.add-section-variable-noimplicits "f" FSort CF, GCF = global (const CF), factory-sort (coercion GRFSort _ GR _), - SortMSL => synthesis.infer-all-gref-deps SortParams SortKey GRFSort KSort, + SortMSL => synthesis.infer-all-gref->deps SortParams SortKey GRFSort KSort, coq.mk-app KSort [GCF] KFSortEta, list-w-params_list MLwP ML, std.length ML NMLArgs, @@ -243,12 +235,12 @@ mk-factory-sort-deps AliasGR CSL :- std.do! [ [declare-all KFSort {findall-classes-for ML} CSL] ]. -pred mk-factory-sort-factory i:gref, o:list (pair id constant), o:list (pair id constant). +func mk-factory-sort-factory gref -> list (pair id constant), list (pair id constant). mk-factory-sort-factory AliasGR CFL CSL :- std.do! [ std.assert-ok! (factory-alias->gref AliasGR GR) "HB", - gref-deps GR MLwPRaw, + gref->deps GR MLwPRaw, context.declare MLwPRaw MLwP SortParams SortKey SortMSL _, - SortMSL => synthesis.infer-all-gref-deps SortParams SortKey GR FSort, + SortMSL => synthesis.infer-all-gref->deps SortParams SortKey GR FSort, log.coq.env.add-section-variable-noimplicits "f" FSort CF, std.length {list-w-params_list MLwP} NMLArgs, coq.mk-n-holes NMLArgs SortMLHoles, @@ -258,7 +250,7 @@ mk-factory-sort-factory AliasGR CFL CSL :- std.do! [ ]. % create instances for all possible combinations of types and structure compatible -pred saturate-instances i:cs-pattern. +func saturate-instances cs-pattern ->. saturate-instances Filter :- std.do! [ findall-has-mixin-instance Filter ClausesHas, @@ -276,7 +268,7 @@ saturate-instances Filter :- std.do! [ declare-all-on-type-constructor t Classes _), ]. -pred no-instance-for i:cs-pattern, i:class. +func no-instance-for cs-pattern, class ->. no-instance-for K (class _ S _) :- get-structure-sort-projection S (global Proj), coq.CS.db-for Proj K []. @@ -289,8 +281,8 @@ namespace private { shorten coq.{ term->gref, subst-fun, safe-dest-app, mk-app, mk-eta, subst-prod }. -pred declare-instance i:factoryname, i:term, i:term, - o:list prop, o:list (pair id constant), o:list (pair id constant). +func declare-instance factoryname, term, term + -> list prop, list (pair id constant), list (pair id constant). declare-instance Factory T F Clauses CFL CSL :- current-mode (builder-from T TheFactory FGR _), !, if (get-option "local" tt) @@ -309,8 +301,8 @@ declare-instance Factory T F Clauses CFL CSL :- % [add-mixin T F _ M Cl] adds a constant being the mixin instance for M on type % T built from factory F -pred add-mixin i:term, i:factoryname, i:bool, i:mixinname, - o:list prop, o:list (pair id constant). +func add-mixin term, factoryname, bool, mixinname + -> list prop, list (pair id constant). add-mixin T FGR MakeCanon MissingMixin [MixinSrcCl, BuilderDeclCl] CSL :- std.do! [ new_int N, % timestamp @@ -338,8 +330,8 @@ add-mixin T FGR MakeCanon MissingMixin [MixinSrcCl, BuilderDeclCl] CSL :- std.do ]) (CSL = []), ]. -pred add-all-mixins i:term, i:factoryname, i:list mixinname, i:bool, - o:list prop, o:list (pair id constant). +func add-all-mixins term, factoryname, list mixinname, bool + -> list prop, list (pair id constant). add-all-mixins T FGR ML MakeCanon Clauses CSL :- std.do! [ std.map ML (m\ o\ sigma ClL CSL\ add-mixin T FGR MakeCanon m ClL CSL, o = pr ClL CSL) ClLxCSL_L, @@ -352,7 +344,7 @@ add-all-mixins T FGR ML MakeCanon Clauses CSL :- std.do! [ % corresponding to parameters in arity A. TS is T applied % to all section variables (and hd-beta reduced). Acc should % be [] at call site. -pred postulate-arity i:arity, i:list term, i:term, o:term, o:term. +func postulate-arity arity, list term, term -> term, term. postulate-arity (parameter ID _ S A) Acc T T1 Ty :- std.assert-ok! (coq.typecheck-ty S _) "arity parameter illtyped", if-verbose (coq.say {header} "postulating" ID), @@ -369,9 +361,9 @@ postulate-arity (arity Ty) ArgsRev X T Ty :- % for becoming builders at section closing time. We also declare % all canonical instances these new mixins allow for, so that the user % can access their theory and notations -pred declare-canonical-instances-from-factory-and-local-builders - i:factoryname, i:term, i:term, i:term, i:factoryname, - o:list prop, o:list (pair id constant), o:list (pair id constant). +func declare-canonical-instances-from-factory-and-local-builders + factoryname, term, term, term, factoryname + -> list prop, list (pair id constant), list (pair id constant). declare-canonical-instances-from-factory-and-local-builders Factory T F _TheFactory FGR Clauses CFL CSL :- std.do! [ synthesis.under-new-mixin-src-from-factory.do! T F (NewMixins\ std.do! [ @@ -384,8 +376,8 @@ declare-canonical-instances-from-factory-and-local-builders % [declare-canonical-instances-from-factory T F] given a factory F % it uses all known builders to declare canonical instances of structures % on T -pred declare-canonical-instances-from-factory - i:factoryname, i:term, i:term, o: list prop, o:list (pair id constant), o:list (pair id constant). +func declare-canonical-instances-from-factory + factoryname, term, term -> list prop, list (pair id constant), list (pair id constant). declare-canonical-instances-from-factory Factory T F ClausesHas CFL CSL :- std.do! [ % The order of the following two "under...do!" is crucial, % priority must be given to canonical mixins @@ -404,7 +396,7 @@ declare-canonical-instances-from-factory Factory T F ClausesHas CFL CSL :- std.d % If you don't mention the factory in a builder, then Coq won't make % a lambda for it at section closing time. -pred hack-section-discharging i:term, o:term. +func hack-section-discharging term -> term. hack-section-discharging B B :- current-mode no-builder, !. hack-section-discharging B B1 :- current-mode (builder-from _ TheFactory _ _), !, std.assert-ok! (coq.typecheck TheFactory TheFactoryTy) "TheFactory is illtyped (BUG)", @@ -413,7 +405,7 @@ hack-section-discharging B B. % unfolds the constant used for the phant abbreviation to avoid storing all % the phantom abstrctions and idfun that were used to trigger inference -pred optimize-body i:term, o:term. +func optimize-body term -> term. optimize-body (app[global (const C)| Args]) Red :- (phant-abbrev _ (const C) _ ; (rex_match "phant_" {coq.gref->id (const C)})), !, coq.env.const C (some B) _, hd-beta B Args HD Stack, @@ -421,11 +413,12 @@ optimize-body (app[global (const C)| Args]) Red :- (phant-abbrev _ (const C) _ ; optimize-body (let _ _ T x\x) Red :- !, optimize-body T Red. optimize-body X X. -pred hnf i:term, o:term. +func hnf term -> term. hnf X R :- get-option "hnf" tt, !, unwind {whd X []} R. hnf X X. -pred optimize-class-body i:term, i:int, i:term, o:term, o:list prop. +:index (_ _ 1) +func optimize-class-body term, int, term -> term, list prop. optimize-class-body T NParams (let _ _ MBo R) R1 Clauses :- std.do! [ declare-mixin-name {hnf MBo} MC CL1, if (T = global (indt _), MC = global (const C), not(coq.env.opaque? C)) @@ -435,17 +428,17 @@ optimize-class-body T NParams (let _ _ MBo R) R1 Clauses :- std.do! [ ]. optimize-class-body _ _ (app L) (app L) []. -pred declare-mixin-name i:term, o:term, o:list prop. -declare-mixin-name (global _ as T) T []. -declare-mixin-name T (global GR) [] :- mixin-mem T GR. -declare-mixin-name T T [] :- coq.safe-dest-app T (global GR) _, not (from _ _ GR), not (get-option "hnf" tt). +func declare-mixin-name term -> term, list prop. +declare-mixin-name (global _ as T) T [] :- !. +declare-mixin-name T (global GR) [] :- mixin-mem T GR, !. +declare-mixin-name T T [] :- coq.safe-dest-app T (global GR) _, not (from _ _ GR), not (get-option "hnf" tt), !. declare-mixin-name T (global (const C)) [mixin-mem T (const C)] :- std.do! [ Name is "HB_unnamed_mixin_" ^ {std.any->string {new_int}}, if-verbose (coq.say {header} "Giving name" Name "to mixin instance" {coq.term->string T}), log.coq.env.add-const-noimplicits Name T _ @transparent! C, ]. -pred check-non-forgetful-inheritance i:term, i:gref. +func check-non-forgetful-inheritance term, gref. check-non-forgetful-inheritance _ _ :- get-option "non_forgetful_inheritance" tt, !. check-non-forgetful-inheritance T Factory :- std.do! [ diff --git a/HB/pack.elpi b/HB/pack.elpi index 3bd0d2cc..ef488f54 100644 --- a/HB/pack.elpi +++ b/HB/pack.elpi @@ -4,7 +4,7 @@ namespace pack { -pred main i:term, i:list argument, o:term. +func main term, list argument -> term. main Ty Args Instance :- std.do! [ std.assert! (not(var Ty)) "HB.pack: the structure to pack cannot be unknown, use HB.pack_for", std.assert! (coq.safe-dest-app {unwind {whd Ty []}} (global Structure) Params) "HB.pack: not a structure", @@ -39,7 +39,8 @@ main Ty Args Instance :- std.do! [ namespace private { -pred synth-instance.aux i:list term, i:gref, i:gref, i:term, i:term, i:list term, i:list prop, o:term. +:index (_ _ _ _ _ 1) +func synth-instance.aux list term, gref, gref, term, term, list term, list prop -> term. synth-instance.aux Params KC KS T Tkey [Factory|Factories] MLCano Instance :- synthesis.under-new-mixin-src-from-factory.do! Tkey Factory (_\ synth-instance.aux Params KC KS T Tkey Factories MLCano Instance). @@ -50,12 +51,13 @@ synth-instance.aux Params KC KS T Tkey [] MLCano Instance :- Instance = app[global KS | InstanceArgs] ]. -pred synth-instance i:list term, i:gref, i:gref, i:term, i:term, i:list term, o:term. +func synth-instance list term, gref, gref, term, term, list term -> term. synth-instance Params KC KS T Tkey Factories Instance :- if (coq.safe-dest-app Tkey (global _) _) (synthesis.local-canonical-mixins-of Tkey MLCano) (MLCano = []), synth-instance.aux Params KC KS T Tkey Factories MLCano Instance. -pred elab-factories i:list argument, i:term, o:list term. +:index (1) +func elab-factories list argument, term -> list term. elab-factories [] _ []. elab-factories [trm FactorySkel|More] T [Factory|Factories] :- std.assert-ok! (coq.elaborate-skeleton FactorySkel FTy MaybeFactory) "HB.pack: illtyped factory", diff --git a/HB/status.elpi b/HB/status.elpi index e6bf3684..fd971dca 100644 --- a/HB/status.elpi +++ b/HB/status.elpi @@ -3,7 +3,7 @@ namespace status { -pred print-hierarchy. +func print-hierarchy. print-hierarchy :- std.do! [ coq.say "--------------------- Hierarchy -----------------------------------", std.findall (class-def CL_) CL, @@ -42,15 +42,15 @@ print-hierarchy :- std.do! [ namespace private { -pred pp-from i:prop. +func pp-from prop ->. pp-from (from F M T) :- coq.say "From" {coq.term->string (global F)} "to" {coq.term->string (global M)}, coq.say " " {coq.term->string (global T)}, coq.say "". -pred pp-list-w-params i:mixins, i:term. -pred pp-list-w-params.list-triple i:list (w-args mixinname), i:term. -pred pp-list-w-params.triple i:w-args mixinname. +func pp-list-w-params mixins, term ->. +func pp-list-w-params.list-triple list (w-args mixinname), term ->. +func pp-list-w-params.triple w-args mixinname ->. pp-list-w-params (w-params.cons N Ty LwP) T :- @pi-parameter N Ty p\ pp-list-w-params (LwP p) {coq.mk-app T [p]}. pp-list-w-params (w-params.nil N TTy LwP) T :- @@ -61,22 +61,22 @@ pp-list-w-params.list-triple L S :- pp-list-w-params.triple (triple M Params T) :- coq.say " " {coq.term->string (app [global M|{std.append Params [T]}])}. -pred pp-class i:prop. +func pp-class prop ->. pp-class (class-def (class _ S MLwP)) :- pp-list-w-params MLwP (global S). -pred pp-mixin-src i:prop. +func pp-mixin-src prop ->. pp-mixin-src (mixin-src T M C) :- coq.say {coq.term->string T} "is a" {nice-gref->string M} "thanks to" {coq.term->string C}. -pred pp-builder-decl i:prop. +func pp-builder-decl prop ->. pp-builder-decl (builder-decl (builder N F M GR)) :- coq.say "builder" GR "with serial number" N "will build mixin" M "from factory" F. -pred pp-current-mode i:prop. +func pp-current-mode prop ->. pp-current-mode (current-mode (builder-from TheType TheFactory GRF Mod)) :- coq.say "The current key is" TheType "with factory" TheFactory "corresponding to Global Ref" GRF "in module" Mod. diff --git a/HB/structure.elpi b/HB/structure.elpi index 3702ce19..7449c01b 100644 --- a/HB/structure.elpi +++ b/HB/structure.elpi @@ -5,7 +5,7 @@ namespace structure { % 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 declare i:string, i:term, i:sort. +func declare string, term, sort ->. declare Module BSkel Sort :- std.do! [ disable-id-phant BSkel BSkelNoId, std.assert-ok! (coq.elaborate-skeleton BSkelNoId _ BNoId) "illtyped structure definition", @@ -14,7 +14,7 @@ declare Module BSkel Sort :- std.do! [ factories-provide GRFSwP PMLwP, - list-w-params.flatten-map GRFSwP gref-deps RMLwP, % TODO: extract code from factories-provide + list-w-params.flatten-map GRFSwP gref->deps RMLwP, % TODO: extract code from factories-provide list-w-params.append PMLwP RMLwP UnsortedMLwP, w-params.map UnsortedMLwP (p\t\ toposort-mixins) MLwP, @@ -45,10 +45,10 @@ declare Module BSkel Sort :- std.do! [ CurrentClass = (class ClassName Structure MLwP), ClassName = indt ClassInd, coq.env.indt ClassInd _ _ _ _ [ClassK] _, GRDepsClauses = - [gref-deps (indt ClassInd) NilwP, gref-deps (indc ClassK) MLwP], + [gref->deps (indt ClassInd) NilwP, gref->deps (indc ClassK) MLwP], std.map ML (m\ o\ o = mixin-class m ClassName) MixinMems, - std.filter ML (m\ not (mixin-first-class m _)) NewMixins, - std.map NewMixins (m\ r\ r = mixin-first-class m ClassName) MixinFirstClass, + std.filter ML (m\ not (mixin->first-class m _)) NewMixins, + std.map NewMixins (m\ r\ r = mixin->first-class m ClassName) MixinFirstClass, if-verbose (coq.say {header} "structure: new mixins" NewMixins), @@ -79,7 +79,7 @@ declare Module BSkel Sort :- std.do! [ log.coq.env.begin-module "Exports" none, %(ClassAlias => class-def CurrentClass => - % GRDepsClauses => MixinFirstClass => gref-deps GRPack MLwP => + % GRDepsClauses => MixinFirstClass => gref->deps GRPack MLwP => % phant.of-gref tt GRPack [] PhRepack), %if-verbose (coq.say {header} "declaring pack abbreviation =" PhRepack), % phant.add-abbreviation "pack" PhRepack _ PackAbbrev, @@ -126,7 +126,7 @@ declare Module BSkel Sort :- std.do! [ std.flatten [ Factories, [is-structure Structure], NewJoins, [class-def CurrentClass], GRDepsClauses, - [gref-deps GRPack MLwP], MixinMems, [StructKeyClause] + [gref->deps GRPack MLwP], MixinMems, [StructKeyClause] ] NewClauses, acc-clauses current NewClauses, @@ -198,23 +198,25 @@ shorten coq.{ term->gref, subst-fun, safe-dest-app, mk-app, mk-eta, subst-prod } % const Po : forall p1 .. pm T m1 .. mn, Extra (Eg Extra = forall x y, x + y = y + z) % const C : forall p1 .. pm s, Extra % Po P1 .. PM T M1 .. MN PoArgs -> C P1 .. PM S PoArgs -pred clean-op-ty i:list prop, i:term, i:term, o:term. +:index (1) +func clean-op-ty list prop, term, term -> term. clean-op-ty [] _ T1 T2 :- copy T1 T2. clean-op-ty [exported-op _ Po C|Ops] S T1 T2 :- - gref-deps (const Po) MLwP, + gref->deps (const Po) MLwP, w-params.nparams MLwP NParams, std.length {list-w-params_list MLwP} NMixins, (pi L L1 L2 Params Rest PoArgs\ - copy (app [global (const Po)| L]) (app [global (const C) | L2]) :- + copy (app [global (const Po)| L]) (app [global (const C) | L2]) :- !, std.split-at NParams L Params [_|Rest], std.drop NMixins Rest PoArgs, std.append Params [S|PoArgs] L1, std.map L1 copy L2) => clean-op-ty Ops S T1 T2. -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. +:index (1) +func operation-body-and-ty list prop, constant, structure, term, term, + list term, term, w-args A -> pair term term. operation-body-and-ty EXI Poperation Struct Psort Pclass Params _T (triple _ ParamsOp _) (pr Bo Ty) :- std.do! [ mk-app (global Struct) Params StructType, mk-app Psort Params PsortP, @@ -226,7 +228,7 @@ operation-body-and-ty EXI Poperation Struct Psort Pclass Params _T (triple _ Par mk-app PclassP [s] Class, synthesis.under-mixin-src-from-factory.do! Carrier Class [ % just in case.. - synthesis.infer-all-gref-deps ParamsOp Carrier (const Poperation) (Body s), + synthesis.infer-all-gref->deps ParamsOp Carrier (const Poperation) (Body s), std.assert-ok! (coq.typecheck (Body s) (DirtyTy s)) "export-1-operation: Body illtyped", clean-op-ty EXI s (DirtyTy s) (BodyTy s), ], @@ -237,9 +239,10 @@ 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: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! [ +:index (_ _ _ _ _ 1) +func export-1-operation mixinname, structure, term, term, one-w-params mixinname, option constant, list prop -> 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, w-params.then MwP mk-fun-prod ignore (operation-body-and-ty EXI Poperation Struct Psort Pclass) (pr Body BodyTy), @@ -257,18 +260,18 @@ 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:structure, i:term, i:term, i:one-w-params mixinname, i:list prop, o:list prop. +func export-operations.aux structure, term, term, one-w-params mixinname, list prop -> list prop. export-operations.aux Struct ProjSort ProjClass MwP EX1 EX2 :- !, std.do! [ w-params_1 MwP (indt M), coq.env.projections M Poperations, std.fold Poperations EX1 (export-1-operation (indt M) Struct ProjSort ProjClass MwP) EX2, ]. -pred mixin-not-already-declared i:one-w-params mixinname. +func mixin-not-already-declared one-w-params mixinname ->. mixin-not-already-declared MwP :- - w-params_1 MwP M, not(mixin-first-class M _), M = indt _. + w-params_1 MwP M, not(mixin->first-class M _), M = indt _. -pred export-operations i:structure, i:term, i:term, i:mixins, i:list prop, o:list prop, o:list mixinname. +func export-operations structure, term, term, mixins, list prop -> list prop, 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, @@ -276,13 +279,13 @@ export-operations Structure ProjSort ProjClass MLwP EX1 EX2 MLToExport :- std.do std.map LMwPToExport w-params_1 MLToExport, ]. -pred mk-coe-class-body - i:factoryname, % From class - i:factoryname, % To class - i:mixins, % To mixins - i:list term, i:term, % Params, T - i:list (w-args mixinname), - o:term. +func mk-coe-class-body + factoryname, % From class + factoryname, % To class + mixins, % To mixins + list term, term, % Params, T + list (w-args mixinname) + -> term. mk-coe-class-body FC TC TMLwP Params T _ CoeBody :- std.do! [ mk-app (global FC) {std.append Params [T]} Class, @@ -290,7 +293,7 @@ mk-coe-class-body FC TC TMLwP Params T _ CoeBody :- std.do! [ std.map TML (from FC) Builders, std.map Builders (x\r\mk-app (global x) Params r) BuildersP, - factory-nparams TC TCNP, + factory->nparams TC TCNP, mk-app (global {get-constructor TC}) {coq.mk-n-holes TCNP} KCHoles, @@ -301,16 +304,16 @@ mk-coe-class-body FC TC TMLwP Params T _ CoeBody :- std.do! [ CoeBody = {{ fun (c : lp:Class) => lp:(ClassCoercion c) }} ]. -pred mk-coe-structure-body - i:structure, % From structure - i:structure, % To structure - i:factoryname, % To factory (for nparams) - i:term, % class coercion - i:term, % sort projection - i:term, % class projection - i:list term, i:term, % Params, T - i:list (w-args mixinname), - o:term. +func mk-coe-structure-body + structure, % From structure + structure, % To structure + factoryname, % To factory (for nparams) + term, % class coercion + term, % sort projection + term, % class projection + list term, term, % Params, T + list (w-args mixinname) + -> term. mk-coe-structure-body StructureF StructureT TC Coercion SortProjection ClassProjection Params _T _ SCoeBody :- std.do! [ @@ -319,7 +322,7 @@ mk-coe-structure-body StructureF StructureT TC Coercion SortProjection ClassProj mk-app ClassProjection Params ClassP, mk-app Coercion Params CoercionP, - factory-nparams TC TCNP, + factory->nparams TC TCNP, mk-app (global {get-constructor StructureT}) {coq.mk-n-holes TCNP} PackPH, @@ -330,7 +333,7 @@ mk-coe-structure-body StructureF StructureT TC Coercion SortProjection ClassProj % [declare-coercion P1 P2 C1 C2] declares a structure and a class coercion % 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. +func declare-coercion term, term, class, class. declare-coercion SortProjection ClassProjection (class FC StructureF FMLwP) (class TC StructureT TMLwP) :- std.do! [ @@ -370,8 +373,9 @@ declare-coercion SortProjection ClassProjection acc-clause current (sub-class FC TC SC NparamsSC) ]. -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. +:index (1) +func join-body int, int, structure, term, term, term, term, term, + list term, name, term, (term -> A) -> 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 (global S3) P S3P, !, @@ -386,7 +390,7 @@ join-body N1 N2 S3 S2_Pack S1_sort S3_to_S1 S2_class S3_to_S2 mk-app S2_Pack {std.append Holes2 [S1_sortS3Ps, S2_classS3Ps]} (Pack s) ]. -pred declare-join i:class, i:pair class class, o:prop. +func declare-join class, pair class class -> prop. declare-join (class C3 S3 MLwP3) (pr (class C1 S1 _) (class C2 S2 _)) (join C1 C2 C3) :- Name is "join_" ^ {gref->modname S3 2 "_"} ^ "_between_" ^ {gref->modname S1 2 "_"} ^ "_and_" ^ {gref->modname S2 2 "_"}, @@ -397,8 +401,8 @@ declare-join (class C3 S3 MLwP3) (pr (class C1 S1 _) (class C2 S2 _)) (join C1 C get-structure-class-projection S2 S2_class, get-constructor S2 S2_Pack, - factory-nparams C1 N1, - factory-nparams C2 N2, + factory->nparams C1 N1, + factory->nparams C2 N2, if-verbose (coq.say {header} "declare unification hint" Name), w-params.fold MLwP3 mk-fun (join-body N1 N2 S3 @@ -414,7 +418,7 @@ declare-join (class C3 S3 MLwP3) (pr (class C1 S1 _) (class C2 S2 _)) (join C1 C % in the middle of existing ones. Possible fix: always declare all intermediate % possibilities but without proper names (requires the previous TODO about % aliasing already existing stuff). -pred declare-unification-hints i:term, i:term, i:class, o:list prop. +func declare-unification-hints term, term, class -> list prop. declare-unification-hints SortProj ClassProj CurrentClass NewJoins :- std.do! [ findall-classes All, @@ -428,35 +432,38 @@ 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. +:index (_ 1) +func synthesize-fields term, list (w-args mixinname) -> record-decl. synthesize-fields _T [] end-record. synthesize-fields T [triple M Args _|ML] (field _ Name MTy Fields) :- std.do! [ 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", + 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) ]. -pred synthesize-fields.body i:list term, i:term, i:list (w-args mixinname), o:indt-decl. +func synthesize-fields.body list term, term, list (w-args mixinname) -> indt-decl. synthesize-fields.body _Params T ML (record "axioms_" {{ Type }} "Class" FS) :- synthesize-fields T ML FS. -pred mk-record+sort-field i:sort, i:name, i:term, i:(term -> record-decl), o:indt-decl. +func mk-record+sort-field sort, name, term, (term -> record-decl) -> indt-decl. mk-record+sort-field Sort _ T F (record "type" (sort Sort) "Pack" (field _ "sort" T F)). -pred mk-class-field i:classname, i:list term, i:term, i:list (w-args mixinname), o:record-decl. +func mk-class-field classname, list term, term, list (w-args mixinname) -> record-decl. mk-class-field ClassName Params T _ (field [canonical ff] "class" (app [global ClassName|Args]) _\end-record) :- std.append Params [T] Args. % Builds the axioms record and the factories from this class to each mixin -pred declare-class+structure i:mixins, i:sort, o:factoryname, o:structure, o:term, o:term, o:list prop, o:prop. +func declare-class+structure mixins, sort -> factoryname, structure, term, term, list prop, prop. declare-class+structure MLwP Sort (indt ClassInd) (indt StructureInd) SortProjection ClassProjection AllFactories (structure-key SortP ClassP (indt StructureInd)):- std.do! [ if-verbose (coq.say {header} "declare axioms record"MLwP ), - w-params.then MLwP (mk-parameter explicit) (mk-parameter explicit) + % TODO: enhance elpi-typechecker to deduce the type of `mk-parameter explicit` from the argmuments + % passed to w-params.then + w-params.then MLwP (mk-parameter explicit : (pred i:name, i:term, i:(term -> indt-decl), o:indt-decl)) (mk-parameter explicit) synthesize-fields.body ClassDeclaration, std.assert-ok! (coq.typecheck-indt-decl ClassDeclaration) "declare-class: illtyped", @@ -468,11 +475,11 @@ declare-class+structure MLwP Sort std.map2 {list-w-params_list MLwP} Projs (m\ p\ r\ sigma P\ std.assert! (p = some P) "BUG: we build a class with an anonymous field", r = from (indt ClassInd) m (const P)) Factories, - AllFactories = [factory-nparams (indt ClassInd) NParams | Factories], + AllFactories = [factory->nparams (indt ClassInd) NParams | Factories], if-verbose (coq.say {header} "declare type record"), - w-params.then MLwP (mk-parameter explicit) (mk-record+sort-field Sort) + w-params.then MLwP (mk-parameter explicit : (pred i:name, i:term, i:(term -> indt-decl), o:indt-decl)) (mk-record+sort-field Sort) (mk-class-field (indt ClassInd)) StructureDeclaration, std.assert-ok! (coq.typecheck-indt-decl StructureDeclaration) "declare: illtyped", @@ -486,14 +493,15 @@ declare-class+structure MLwP Sort ]. % Declares "sort" as a Coercion Proj : Structurename >-> CoeClass. -pred declare-sort-coercion i:class, i:structure, i:term. +func declare-sort-coercion class, structure, term ->. declare-sort-coercion CoeClass StructureName (global Proj) :- if-verbose (coq.say {header} "declare sort coercion"), log.coq.coercion.declare (coercion Proj 0 StructureName CoeClass). -pred if-class-already-exists-error i:id, i:list class, i:list mixinname. +:index (_ 1) +func if-class-already-exists-error id, list class, list mixinname. if-class-already-exists-error _ [] _. if-class-already-exists-error N [class _ S ML1wP|CS] ML2 :- list-w-params_list ML1wP ML1, @@ -501,7 +509,8 @@ if-class-already-exists-error N [class _ S ML1wP|CS] ML2 :- (coq.error "Structure" {nice-gref->string S} "contains the same mixins as" N) (if-class-already-exists-error N CS ML2). -pred export-mixin-coercion i:classname, i:option constant. +:index (_ 1) +func export-mixin-coercion classname, option constant. export-mixin-coercion _ none. export-mixin-coercion ClassName (some C) :- coq.env.typeof (const C) CTy, @@ -509,7 +518,8 @@ export-mixin-coercion ClassName (some C) :- if-verbose (coq.say {header} "export class to mixin coercion for mixin" {nice-gref->string MixinGR}), log.coq.coercion.declare (coercion (const C) _ ClassName (grefclass MixinGR)). -pred mc-compat-structure i:string, i:modpath, i:list mixinname, i:int, i:term, i:gref, i:option gref. +:index(1) +func mc-compat-structure string, modpath, list mixinname, int, term, gref, option gref ->. mc-compat-structure ModuleName _Module NewMixins CNParams ClassProjection GRPack Axioms :- std.do! [ CompatModuleName is "MathCompCompat" ^ ModuleName, log.coq.env.begin-module CompatModuleName none, % to avoid collisions @@ -521,13 +531,13 @@ mc-compat-structure ModuleName _Module NewMixins CNParams ClassProjection GRPack if (NewMixins = [NewMixin]) (std.do! [ if-verbose (coq.say "mc-compat-structure: declaring notations 'axioms', 'mixin_of' and 'Mixin'"), - factory-nparams NewMixin NewMixinNP, + factory->nparams NewMixin NewMixinNP, MArgs is NewMixinNP + 1, mk-eta MArgs {coq.env.typeof NewMixin} (global NewMixin) EtaNewMixin, @global! => log.coq.notation.add-abbreviation "axioms" MArgs EtaNewMixin ff _, @deprecated! "mathcomp 2.0.0" "use the factory instead" => @global! => log.coq.notation.add-abbreviation "mixin_of" MArgs EtaNewMixin ff _, - std.assert! (factory-constructor NewMixin FK) "BUG: Factory constructor missing", + std.assert! (factory->constructor NewMixin FK) "BUG: Factory constructor missing", std.assert! (phant-abbrev FK _ PhAbb) "BUG: missing phant-abbrev", @deprecated! "mathcomp 2.0.0" "use the F.Build instead" => @global! => log.coq.notation.add-abbreviation "Mixin" 0 @@ -550,7 +560,7 @@ mc-compat-structure ModuleName _Module NewMixins CNParams ClassProjection GRPack %coq.env.import-module Module, ]. -pred clone-phant-body i:factoryname, i:term, i:structure, i:list term, i:term, i:list (w-args mixinname), o:phant-term. +func clone-phant-body factoryname, term, structure, list term, term, list (w-args mixinname) -> phant-term. clone-phant-body ClassName SortProjection ((indt I) as Structure) PL T _ PhF :- std.do! [ std.assert! (coq.env.indt I _ _ _ _ [PackC] _) "wtf", mk-app (global (indc PackC)) {std.append PL [T]} PackPLT, @@ -568,7 +578,7 @@ clone-phant-body ClassName SortProjection ((indt I) as Structure) PL T _ PhF :- % [pack-body ClassName P T MLwA B] asserts % B = fun m0 ... mn => Pack P T (Class P T m0 ... mn) % under a context with P and T -pred pack-body i:classname, i:list term, i:term, i:list (w-args mixinname), o:term. +func pack-body classname, list term, term, list (w-args mixinname) -> term. pack-body ClassName PL T MLwA F :- std.do! [ class-def (class ClassName S _), get-constructor ClassName BuildC, @@ -577,11 +587,11 @@ pack-body ClassName PL T MLwA F :- std.do! [ (pack-body.aux PL T BuildC PackS) F, ]. pack-body.aux PL T BuildC PackS Body :- !, std.do! [ - synthesis.infer-all-gref-deps PL T BuildC Class, + synthesis.infer-all-gref->deps PL T BuildC Class, mk-app (global PackS) {std.append PL [T, Class]} Body ]. -pred mk-infer-key i:class, i:term, i:mixins, i:term, o:phant-term. +func mk-infer-key class, term, mixins, term -> 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), phant.fun-infer-type CoeClass {coq.id->name ID} St PhKBo PhK. @@ -589,13 +599,13 @@ mk-infer-key CoeClass K (w-params.cons ID Ty W) St R :- @pi-parameter ID Ty t\ mk-infer-key CoeClass {mk-app K [t]} (W t) {mk-app St [t]} (PhT t), phant.fun-implicit {coq.id->name ID} Ty PhT R. -pred if-coverage-not-good-error i:list mixinname. +func if-coverage-not-good-error list mixinname ->. if-coverage-not-good-error ML :- coq.gref.list->set ML MS, std.forall ML (if-coverage-not-good-error.one MS). -pred if-coverage-not-good-error.one i:coq.gref.set, i:mixinname. -if-coverage-not-good-error.one MS M :- mixin-first-class M C, !, +func if-coverage-not-good-error.one coq.gref.set, mixinname. +if-coverage-not-good-error.one MS M :- mixin->first-class M C, !, class-coverage [C] CMS, if (coq.gref.set.subset CMS MS) true @@ -608,7 +618,8 @@ if-coverage-not-good-error.one MS M :- mixin-first-class M C, !, "which contains at most" {std.map {coq.gref.set.elements {coq.gref.set.inter CMS MS}} nice-gref->string}). if-coverage-not-good-error.one _ _. % new class is the first covering M -pred product->triples i:term, o:list (w-args factoryname), o:bool. +:index (5) +func product->triples term -> list (w-args factoryname), bool. product->triples {{ lib:hb.prod lp:A lp:B }} L ClosureCheck :- !, product->triples B GRB ClosureCheck, product->triples A GRA _, @@ -617,7 +628,7 @@ product->triples {{ True }} [] tt :- !. product->triples {{ False }} [] ff :- !. product->triples A [GR] tt :- std.assert! (factory? A GR) "A structure can only mention known factories". -pred sigT->list-w-params i:term, o:list-w-params factoryname, o:bool. +func sigT->list-w-params term -> list-w-params factoryname, bool. sigT->list-w-params (fun N T B) L C :- coq.name->id N ID, % TODO: we should read the ID from the definition type which is an arity containing ids L = w-params.cons ID T Rest, diff --git a/HB/structures.v b/HB/structures.v index e3a0b52e..e35e58a8 100644 --- a/HB/structures.v +++ b/HB/structures.v @@ -1,5 +1,5 @@ (* Support constants, to be kept in sync with shim/structures.v *) -From Corelib Require Import ssreflect ssrfun. +From Coq Require Import ssreflect ssrfun. Variant error_msg := NoMsg | IsNotCanonicallyA (x : Type). Definition unify T1 T2 (t1 : T1) (t2 : T2) (s : error_msg) := @@ -128,7 +128,7 @@ pred phant-abbrev o:gref, o:gref, o:abbreviation. % [factory-alias->gref X GR] when X is already a factory X = GR % however, when X is a phantom abbreviated gref, we find the underlying % factory gref GR associated to it. -pred factory-alias->gref i:gref, o:gref, o: diagnostic. +func factory-alias->gref gref -> gref, diagnostic. factory-alias->gref PhGR GR ok :- phant-abbrev GR PhGR _, !. factory-alias->gref GR GR ok :- phant-abbrev GR _ _, !. factory-alias->gref GR _ (error Msg) :- !, @@ -139,29 +139,27 @@ factory-alias->gref GR _ (error Msg) :- !, %%%%% Cache of known facts %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% [factory-constructor F K] means K is a constructor for +% [factory->constructor F K] means K is a constructor for % the factory F. -pred factory-constructor o:factoryname, o:gref. +func factory->constructor factoryname -> gref. -% [factory-nparams F N] says that F has N parameters -pred factory-nparams o:factoryname, o:int. +% [factory->nparams F N] says that F has N parameters +func factory->nparams factoryname -> int. % [is-structure GR] tests if GR is a known structure pred is-structure o:gref. -% [factory-builder-nparams Build N] states that when the user writes -% the [F.Build T] abbreviation the term behind it has N arguments before T -pred factory-builder-nparams o:constant, o:int. +% [is-factory GR] tests if GR is a known factory +pred is-factory o:gref. % [sub-class C1 C2 Coercion12 NparamsCoercion] C1 is a sub-class of C2, % see also sub-class? which computes it on the fly :index (2 2 1) pred sub-class o:classname, o:classname, o:constant, o:int. -% [gref-deps GR MLwP] is a (pre computed) list of dependencies of a know global +% [gref->deps GR MLwP] is a (pre computed) list of dependencies of a know global % constant. The list is topologically sorted -:index(2) -pred gref-deps o:gref, o:mixins. +func gref->deps gref -> mixins. % [join C1 C2 C3] means that C3 inherits from both C1 and C2 pred join o:classname, o:classname, o:classname. @@ -169,7 +167,7 @@ pred join o:classname, o:classname, o:classname. % Section local memory of names for mixins, so that we can reuse them % and build terms with simpler conversion problems (less unfolding % in order to discover two mixins are the same) -pred mixin-mem i:term, o:gref. +func mixin-mem term -> gref. %%%%%% Memory of exported mixins (HB.structure) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Operations (named mixin fields) need to be exported exactly once, @@ -178,9 +176,9 @@ pred mixin-mem i:term, o:gref. % Also we remember which is the first class/structure that includes % a given mixin, assuming the invariant that this first class is also % the minimal class that includes this mixin. -% [mixin-first-class M C] states that C is the first/minimal class +% [mixin->first-class M C] states that C is the first/minimal class % that contains the mixin M -pred mixin-first-class o:mixinname, o:classname. +func mixin->first-class mixinname -> classname. % memory of exported operations (TODO: document fiels) pred exported-op o:mixinname, o:constant, o:constant. @@ -480,7 +478,7 @@ main [A] :- with-attributes (with-logging (factory.declare-mixin A)). shorten coq.env.{ begin-module, end-module, begin-section, end-section, export-module }. -pred actions i:id. +func actions id ->. actions N :- begin-module N none, begin-section N, @@ -670,7 +668,7 @@ main [const-decl N (some B) Arity] :- std.do! [ shorten coq.env.{ begin-module, end-module, begin-section, end-section, import-module, export-module }. -pred actions i:id. +func actions id ->. actions N :- begin-module N none, begin-module "Exports" none, @@ -686,7 +684,7 @@ actions N :- coq.elpi.accumulate current "export.db" (clause _ _ (module-to-export File O)), if (get-option "mathcomp" tt ; get-option "mathcomp.axiom" _) (actions-compat N) true. -pred actions-compat i:id. +func actions-compat id ->. actions-compat ModuleName :- CompatModuleName is "MathCompCompat" ^ ModuleName, begin-module CompatModuleName none, @@ -842,7 +840,7 @@ main [A] :- with-attributes (with-logging (factory.declare A)). shorten coq.env.{ begin-module, end-module, begin-section, end-section, export-module }. -pred actions i:id. +func actions id ->. actions N :- begin-module N none, begin-section N, @@ -926,7 +924,7 @@ main [ctx-decl C] :- with-attributes (with-logging (builders.begin C)). shorten coq.env.{ begin-module, end-module, begin-section }. -pred actions i:id. +func actions id ->. actions N :- begin-module N none, begin-module "Super" none, @@ -967,7 +965,7 @@ main [] :- with-attributes (with-logging builders.end). shorten coq.env.{ end-module, end-section, begin-module, end-module, export-module }. -pred actions. +func actions. actions :- end-section, begin-module {calc ("Builders_Export_" ^ {std.any->string {new_int} })} none, @@ -1039,8 +1037,9 @@ main _ :- coq.error "Usage: HB.export M.". shorten coq.env.{ export-module }. -pred actions i:list located. -actions [loc-modpath MP] :- !, +:index (1) +func actions list located ->. +actions [loc-modpath MP] :- export-module MP, coq.env.current-library File, coq.elpi.accumulate current "export.db" (clause _ _ (module-to-export File MP)). @@ -1087,12 +1086,18 @@ main _ :- coq.error "Usage: HB.reexport.". shorten coq.env.{ export-module }. -pred module-in-module i:list string, i:prop. +% TODO: should be in stdlib? +:index (1) +func prefixL list A, list A ->. +prefixL [] _. +prefixL [X|Xs] [X|Ys] :- prefixL Xs Ys. + +func module-in-module list string, prop. module-in-module PM (module-to-export _ M) :- coq.modpath->path M PC, - std.appendR PM _ PC. % sublist + prefixL PM PC. % sublist -pred actions i:option id. +func actions option id ->. actions Filter :- coq.env.current-library File, compute-filter Filter MFilter, @@ -1199,11 +1204,11 @@ Elpi Accumulate lp:{{ main [trm Skel] :- !, with-attributes (with-logging (check-or-not Skel)). main _ :- coq.error "usage: HB.check (term).". -pred check-or-not i:term. +func check-or-not term ->. check-or-not Skel :- coq.version VersionString _ _ _, if (get-option "skip" R, rex_match R VersionString) - (coq.warning "HB" "HB.skip" {get-option "elpi.loc"} "Skipping test on Coq" VersionString "as requested") + (get-option "elpi.loc" Opt, !, coq.warning "HB" "HB.skip" Opt "Skipping test on Coq" VersionString "as requested") (log.coq.check Skel Ty T Result, if (Result = error Msg) (if (get-option "fail" tt) diff --git a/Makefile b/Makefile index f08aaa80..9d6b70c6 100644 --- a/Makefile +++ b/Makefile @@ -100,8 +100,19 @@ distclean: sub-distclean this-distclean .PHONY: this-config this-build this-only this-test-suite this-test-suite-stdlib this-distclean this-clean this-config:: __always__ - if command -v coqc > /dev/null && (coqc --version | grep -q '8.18\|8.19\|8.20') ; then \ - sed -i.bak HB/structures.v -e 's/From Corelib/From Coq/' ; \ + @command -v coqc >/dev/null || exit 1 + @if [ -e config.stamp -a "`coqc --print-version`" = "`cat config.stamp 2>/dev/null`" ] ; then \ + echo 'already configured';\ + else\ + coqc --print-version > config.stamp;\ + echo 'configuring for ' `coqc --print-version`;\ + if (coqc --version | grep -q '8.18\|8.19\|8.20') ; then \ + echo '*****************************************************************';\ + echo 'old coq version detected, double check the diff before committing';\ + echo '*****************************************************************';\ + sed -i.bak `find . -name \*.v` -e 's/From Corelib/From Coq/' ; \ + sed -i.bak `find . -name \*.v` -e 's/IntDef/ZArith/' ; \ + fi;\ fi this-build:: this-config Makefile.coq @@ -117,6 +128,7 @@ this-test-suite-stdlib:: build Makefile.test-suite-stdlib.coq +$(COQMAKE_TESTSUITE_STDLIB) this-distclean:: this-clean + rm -f config.stamp rm -f Makefile.coq Makefile.coq.conf rm -f Makefile.test-suite.coq Makefile.test-suite.coq.conf rm -f Makefile.test-suite-stdlib.coq Makefile.test-suite-stdlib.coq.conf diff --git a/_CoqProject b/_CoqProject index 89887ca1..d2b6ace7 100644 --- a/_CoqProject +++ b/_CoqProject @@ -2,6 +2,7 @@ HB/structures.v -arg -w -arg -elpi.accumulate-syntax -arg -w -arg +elpi.typecheck -arg -w -arg -elpi.typecheck-syntax +-arg -w -arg -elpi.flex-clause -Q HB HB -R tests HB.tests