Skip to content

Commit

Permalink
added predicates to handle cumulative output over forall, avoiding du…
Browse files Browse the repository at this point in the history 
…plicates in the association list (which was broken in DCIFF with std.forall)
  • Loading branch information
@ptorrx
ptorrx committed Jul 20, 2023
1 parent 6bdfd59 commit 790ca44
Showing 1 changed file with 128 additions and 17 deletions.
145 changes: 128 additions & 17 deletions HB/instance.elpi
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,14 +25,17 @@ pred declare-const i:id, i:term, i:arity, o:list (pair id constant).
declare-const Name BodySkel TyWPSkel CSL :- std.do! [

coq.say "DC************************* NOW RUNNING (entry point) declare-const Name BodySkel TyWPSkel CSL",
coq.say "DC!!!!!!!!!!!!! Name = " Name,
coq.say "DC!!!!!!!!!!!!! BodySkel = " BodySkel,
coq.say "DC!!!!!!!!!!!!! TyWPSkel = " TyWPSkel,
coq.say "DC!!!!!!!!!!!!! In Name = " Name,
coq.say "DC!!!!!!!!!!!!! In BodySkel = " BodySkel,
coq.say "DC!!!!!!!!!!!!! In TyWPSkel = " TyWPSkel,

std.assert-ok! (coq.elaborate-arity-skeleton TyWPSkel _ TyWP) "Definition type illtyped",
coq.arity->term TyWP Ty,
std.assert-ok! (coq.elaborate-skeleton BodySkel Ty Body) "Definition illtyped",

coq.say "DC!!!!!!!!!!!!! Ex Body = " Body,
coq.say "DC!!!!!!!!!!!!! Ex Ty = " Ty,

% handle parameters via a section -- begin
if (TyWP = arity SectionTy) (
% Do not open a section when it is not necessary (no parameters)
Expand All @@ -46,6 +49,9 @@ declare-const Name BodySkel TyWPSkel CSL :- std.do! [
private.postulate-arity TyWP [] Body SectionBody SectionTy
),

coq.say "DC!!!!!!!!!!!!! Ex SectionBody = " SectionBody,
coq.say "DC!!!!!!!!!!!!! Ex SectionTy = " SectionTy,

% identify the factory
std.assert! (coq.safe-dest-app SectionTy (global FactoryAlias) Args) "The type of the instance is not a factory",
factory-alias->gref FactoryAlias Factory,
Expand All @@ -63,6 +69,8 @@ declare-const Name BodySkel TyWPSkel CSL :- std.do! [
UnfoldClauses => copy SectionTy SectionTyUnfolded,
]) (SectionTy = SectionTyUnfolded),

coq.say "DC!!!!!!!!!!!!! Ex UnfoldClauses = " UnfoldClauses,

log.coq.env.add-const-noimplicits-failondup RealName OptimizedBody
SectionTyUnfolded @transparent! C,
TheFactory = (global (const C)),
Expand All @@ -72,6 +80,7 @@ declare-const Name BodySkel TyWPSkel CSL :- std.do! [

private.check-non-forgetful-inheritance TheType Factory,

% Clauses and CSL are outputs. QUESTION: what is the context here?
private.declare-instance Factory TheType TheFactory Clauses CSL,

% handle parameters via a section -- end
Expand All @@ -81,7 +90,10 @@ declare-const Name BodySkel TyWPSkel CSL :- std.do! [
),

% we accumulate clauses now that the section is over
acc-clauses current Clauses
% QUESTION - what is this really accumulating? appears to be always empty
acc-clauses current Clauses,

coq.say "DC!!!!!!!!!!!!! Out Clauses = " Clauses,
].

% [declare-all T CL MCSTL] given a type T and a list of class definition
Expand All @@ -94,6 +106,10 @@ pred declare-all i:term, i:list class, o:list (pair id constant).
declare-all T [class Class Struct MLwP|Rest] [pr Name CS|L] :-

coq.say "NOW RUNNING!!!!!!!!!!!!!! declare-all",
coq.say "DALL!!!!!!!!!! In T = " T,
coq.say "DALL!!!!!!!!!! In Class = " Class,
coq.say "DALL!!!!!!!!!! In Struct = " Struct,
coq.say "DALL!!!!!!!!!! In MLwP = " MLwP,

if (not(has-CS-instance? T Struct))
true % we build it
Expand All @@ -105,13 +121,17 @@ declare-all T [class Class Struct MLwP|Rest] [pr Name CS|L] :-
params->holes MLwP Params,
get-constructor Class KC,

coq.say "DALL!!!!!!!!!!!!!! Exec1 ",

if (synthesis.infer-all-args-let Params T KC KCApp ok)
(if-verbose (coq.say {header} "we can build a" {nice-gref->string Struct} "on"
{coq.term->string T}))
fail,

!,

coq.say "DALL!!!!!!!!!!!!!! Exec2 ",

Name is {cs-pattern->name {term->cs-pattern T}}
^ "__canonical__" ^ {gref->modname Struct 2 "_" },

Expand All @@ -131,6 +151,10 @@ declare-all T [class Class Struct MLwP|Rest] [pr Name CS|L] :-

if-verbose (coq.say {header} "structure instance" Name "declared"),

coq.say "DALL!!!!!!!!!! Out Name = " Name,
coq.say "DALL!!!!!!!!!! Out CS = " CS,
coq.say "DALL!!!!!!!!!! Env Clauses = " Clauses,

Clauses => declare-all T Rest L.

/*
Expand Down Expand Up @@ -256,16 +280,18 @@ declare-instance Factory T F Clauses CSL :-
T F TheFactory FGR Clauses CSL.
declare-instance Factory T F Clauses CSL :-

coq.say "DI!!!!!!!!!!!!!!! NOW RUNNING (C2) private.declare-instance Factory T F Clauses CSL",
coq.say "DI!!!!!!!!! Factory = " Factory,
coq.say "DI!!!!!!!!! T = " T,
coq.say "DI!!!!!!!!! F = " F,
coq.say "DI!!!!!!!!!!!!!!!! NOW RUNNING (C2) private.declare-instance Factory T F Clauses CSL",
coq.say "DI!!!!!!!!! In Factory = " Factory,
coq.say "DI!!!!!!!!! In T = " T,
coq.say "DI!!!!!!!!! In F = " F,

declare-canonical-instances-from-factory Factory T F CSL,
if (get-option "export" tt)
(coq.env.current-library File,
std.map CSL (x\r\ sigma i c\ x = pr i c, r = instance-to-export File i c) Clauses)
(Clauses = []).
(Clauses = []),

coq.say "DI!!!!!!!!! In Clauses = " Clauses.

% [add-mixin T F _ M Cl] adds a constant being the mixin instance for M on type
% T built from factory F
Expand All @@ -275,7 +301,7 @@ add-mixin T FGR MakeCanon MissingMixin [MixinSrcCl, BuilderDeclCl] CSL :- std.do

coq.say "AM!!!!!!!!!!!!!!!!!!!! NOW RUNNING add-mixin",
coq.say "AM!!!!!!!!!! In T (for the subject) = " T,
coq.say "AM!!!!!!!!!! In MissingMixin (might be a base one) = " MissingMixin,
coq.say "AM!!!!!!!!!! In MissingMixin (the mixin, might be a base one) = " MissingMixin,

new_int N, % timestamp

Expand All @@ -289,6 +315,10 @@ add-mixin T FGR MakeCanon MissingMixin [MixinSrcCl, BuilderDeclCl] CSL :- std.do

std.assert! (MissingMixin = MixinName) "HB: anomaly: we built the wrong mixin",

coq.say "AM!!!!!!!!!! Ex Bo = " Bo,
coq.say "AM!!!!!!!!!! Ex Ty = " Ty,
coq.say "AM!!!!!!!!!! Ex MixinName = " MixinName,

% If the mixin instance is already a constant there is no need to
% alias it.
if (Bo = global (const C)) true
Expand All @@ -303,9 +333,60 @@ add-mixin T FGR MakeCanon MissingMixin [MixinSrcCl, BuilderDeclCl] CSL :- std.do
]) (CSL = []),

coq.say "AM!!!!!!!!!! Out C (instance name) = " C,
coq.say "AM!!!!!!!!!! Out MixinSrcCl = " MixinSrcCl,
coq.say "AM!!!!!!!!!! Out BuilderDeclCl = " BuilderDeclCl,
coq.say "AM!!!!!!!!!! Out CSL = " 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-mixinW i:term, i:factoryname, i:bool, i:mixinname,
o:list prop, o:list (pair id constant).
add-mixinW T FGR MakeCanon MissingMixin [MixinSrcCl, BuilderDeclCl] CSL :- std.do! [

coq.say "AM!!!!!!!!!!!!!!!!!!!! NOW RUNNING add-mixin",
coq.say "AM!!!!!!!!!! In T (for the subject) = " T,
coq.say "AM!!!!!!!!!! In MissingMixin (the mixin, might be a base one) = " MissingMixin,

new_int N, % timestamp

synthesis.assert!-infer-mixin T MissingMixin Bo,
MixinSrcCl = mixin-src T MixinName (global (const C)),
BuilderDeclCl = builder-decl (builder N FGR MixinName (const C)),

std.assert-ok! (coq.typecheck Bo Ty) "declare-instances: mixin illtyped",
safe-dest-app Ty (global MixinNameAlias) _,
factory-alias->gref MixinNameAlias MixinName,

std.assert! (MissingMixin = MixinName) "HB: anomaly: we built the wrong mixin",

coq.say "AM!!!!!!!!!! Ex Bo = " Bo,
coq.say "AM!!!!!!!!!! Ex Ty = " Ty,
coq.say "AM!!!!!!!!!! Ex MixinName = " MixinName,

% If the mixin instance is already a constant there is no need to
% alias it.
if (Bo = global (const C)) true
(Name is {gref->modname FGR 2 "_"} ^"__to__" ^ {gref->modname MixinName 2 "_"},
if-verbose (coq.say {header} "declare mixin instance" Name),
log.coq.env.add-const-noimplicits Name Bo Ty @transparent! C),
if (MakeCanon = tt, whd (global (const C)) [] (global (indc _)) _)
(std.do! [
if-verbose (coq.say {header} "declare canonical mixin instance" C),
with-locality (log.coq.CS.declare-instance C),
CSL = [pr "_" C],
]) (CSL = []),

coq.say "AM!!!!!!!!!! Out C (instance name) = " C,
coq.say "AM!!!!!!!!!! Out MixinSrcCl = " MixinSrcCl,
coq.say "AM!!!!!!!!!! Out BuilderDeclCl = " BuilderDeclCl,
coq.say "AM!!!!!!!!!! Out CSL = " CSL,

].



pred add-all-mixins i:term, i:factoryname, i:list mixinname, i:bool,
o:list prop, o:list (pair id constant), o:list term.
add-all-mixins T FGR ML MakeCanon Clauses CSL Sbjs:- std.do! [
Expand Down Expand Up @@ -409,6 +490,32 @@ declare-canonical-instances-from-factory-and-local-builders
std.append MCSL CCSL CSL
].

%%%%%%%%%%%%%%

% cumulates output over forall
pred cumul-forall i:list A, i:(A -> B -> prop), o:list B.
cumul-forall [] _ [].
cumul-forall [X|L] P [Y|M] :- P X Y, cumul-forall L P M.

% flattens cumulated list output
pred flat-cumul-forall i:list A, i:(A -> list B -> prop), o:list B.
flat-cumul-forall X P Y :- cumul-forall X P W, flatten W Y.

% merges list1 and list2 so that list1 doesn't introduce k-duplicates
pred hmerge i:list (pair B C), i:list (pair B C), o:list (pair B C).
hmerge [] A A.
hmerge [(pr K _)|LA] LX LY :- coq.lookup! LX K _, hmerge LA LX LY.
hmerge [(pr K V)|LA] LX [(pr K V)|LY] :- hmerge LA LX LY.
%hmerge [(pr K1 V1)|LA] LX LY1 :- if (coq.lookup! LX K1 _) (LY1 = LY0) (LY1 = [(pr K1 V1)|LY0),
% hmerge LA LX LY0.

% cumulates without k-duplicates
pred hcumul-forall i:list A, i:(A -> list (pair B C) -> prop), o:list (pair B C).
hcumul-forall [] _ [].
hcumul-forall [X|L] P M2 :- P X M1, hmerge M1 M0 M2, hcumul-forall L P M0.

%%%%%%%%%%%%%%%%%

% [declare-canonical-instances-from-factory T F] given a factory F
% it uses all known builders to declare canonical instances of structures
% on T
Expand All @@ -429,19 +536,20 @@ declare-canonical-instances-from-factory Factory T F CSL :- std.do! [
synthesis.under-mixin-src-from-factory.do! T F [
synthesis.under-local-canonical-mixins-of.do! T [
list-w-params_list {factory-provides Factory} ML,
coq.say "DCIFF!!!!!!! In ML (mixin names) = " ML,
coq.say "DCIFF!!!!!!! Ex ML (mixin names) = " ML,

% currently, AllSubjects = [T]
% Clauses, MCSL and AllSubjects are outputs. currently, AllSubjects = [T]
add-all-mixins T Factory ML tt Clauses MCSL AllSubjects,
coq.say "DCIFF!!!!!!!!!! Ex AllSubjects = " AllSubjects,
% old (Clauses not used)
instance.declare-all T {findall-classes-for ML} CCSL,
% std.forall AllSubjects (s \ instance.declare-all s {findall-classes-for ML} CCSL),
% instance.declare-all T {findall-classes-for ML} CCSL,
% hcumul-forall AllSubjects (s \ instance.declare-all s {findall-classes-for ML}) CCSL,
]
],

% Clauses => instance.declare-all T {findall-classes-for ML} CCSL,
% new (should use Clauses and AllSubjects)
% Clauses => std.forall AllSubjects (s \ instance.declare-all s {findall-classes-for ML} CCSL),
Clauses => hcumul-forall AllSubjects (s \ instance.declare-all s {findall-classes-for ML}) CCSL,

/*
%% New code:
Expand All @@ -455,10 +563,13 @@ declare-canonical-instances-from-factory Factory T F CSL :- std.do! [
(s \ instance.declare-all s {findall-classes-for ML} CCSL),
%%
*/
coq.say "DCIFF!!!!!!!!!! Ex Clauses = " Clauses,
coq.say "DCIFF!!!!!!!!!! Ex CCSL = " CCSL,

std.append MCSL CCSL CSL,
coq.say "DCIFF!!!!!!!!!! Out CSL = " CSL,
coq.say "DCIFF!!!!!!!!!! Out CSL = " CSL,
].

% 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.
Expand Down

0 comments on commit 790ca44

Please sign in to comment.