diff --git a/docs/RefMan/Modules.rst b/docs/RefMan/Modules.rst index d8e992314..c20fc4fc3 100644 --- a/docs/RefMan/Modules.rst +++ b/docs/RefMan/Modules.rst @@ -370,6 +370,24 @@ other modules: x : [n] // A declarations of a constant +Interface module may contain ``type`` or ``type constraint`` synonyms: + +.. code-block:: cryptol + :caption: A nested interface module + + interface module I where + + type n : # // `n` is a numeric type + + type W = [n] // A type synonym, available when the interface is imported + + type constraint (fin n, n >= 1) + // Assumptions about the declared numeric type + + x : W // A declarations of a constant; uses type synonym. + + + Importing an Interface Module ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -582,7 +600,8 @@ an anonymous interface and using it straight away: The ``parameter`` block defines an interface module and uses it. Note that the parameters may not use things defined in ``M`` as -the interface is declared outside of ``M``. +the interface is declared outside of ``M``. The ``parameter`` +may contain the same sort of declarations that may appear in interfaces. Anonymous Instantiation Arguments diff --git a/docs/RefMan/_build/doctrees/Modules.doctree b/docs/RefMan/_build/doctrees/Modules.doctree index b1fb46f17..704333f90 100644 Binary files a/docs/RefMan/_build/doctrees/Modules.doctree and b/docs/RefMan/_build/doctrees/Modules.doctree differ diff --git a/docs/RefMan/_build/doctrees/environment.pickle b/docs/RefMan/_build/doctrees/environment.pickle index 86245cd3e..a63af4ead 100644 Binary files a/docs/RefMan/_build/doctrees/environment.pickle and b/docs/RefMan/_build/doctrees/environment.pickle differ diff --git a/docs/RefMan/_build/html/Modules.html b/docs/RefMan/_build/html/Modules.html index 19dee21b2..3877d2687 100644 --- a/docs/RefMan/_build/html/Modules.html +++ b/docs/RefMan/_build/html/Modules.html @@ -441,13 +441,29 @@

Interface Modulestype or type constraint synonyms:

+
+
A nested interface module
+
interface module I where
+
+  type n : #      // `n` is a numeric type
+
+  type W = [n]    // A type synonym, available when the interface is imported
+
+  type constraint (fin n, n >= 1)
+                  // Assumptions about the declared numeric type
+
+  x : W           // A declarations of a constant;  uses type synonym.
+
+
+

Importing an Interface Module

A module may be parameterized by importing an interface, instead of a concrete module

-
-
A parameterized module
+
+
A parameterized module
// The interface desribes the parmaeters
 interface module I where
   type n : #
@@ -470,8 +486,8 @@ 
Importing an Interface ModuleInstantiating a Parameterized Module.

-

-
Multiple interface parameters

+

+
Multiple interface parameters

 
interface module I where
   type n : #
   type constraint (fin n, n >= 1)
@@ -496,8 +512,8 @@ 
Interface ConstraintsWhen working with multiple interfaces, it is to useful
 to be able to impose additional constraints on the
 types imported from the interface.

-

-
Adding constraints to interface parameters

+

+
Adding constraints to interface parameters

 
interface module I where
   type n : #
   type constraint (fin n, n >= 1)
@@ -525,8 +541,8 @@ 
Interface ConstraintsTo use a parameterized module we need to provide concrete
 implementations for the interfaces that it uses, and provide
 a name for the resulting module.  This is done as follows:

-

-
Instantiating a parameterized module using a single interface.

+

+
Instantiating a parameterized module using a single interface.

 
interface module I where
   type n : #
   type constraint (fin n, n >= 1)
@@ -552,8 +568,8 @@ 
Interface ConstraintsIf a module is parameterized my multiple interfaces
 we need to provide an implementation module for each
 interface, using a slight variation on the previous notation.

-

-
Instantiating a parameterized module by name.

+

+
Instantiating a parameterized module by name.

 
// I is defined as above
 
 module F where
@@ -586,8 +602,8 @@ 
Interface Constraints
 
Modules defined by instantiation may be nested,
 just like any other module:

-

-
Nested module instantiation.

+

+
Nested module instantiation.

 
module M where
 
   import Somewhere // defines G
@@ -604,8 +620,8 @@ 
Interface Constraintssubmodule keyword.

 
To pass a nested module as the argument of a function,
 use submodule I like this:

-

Anonymous Instantiation Arguments

diff --git a/docs/RefMan/_build/html/_sources/Modules.rst.txt b/docs/RefMan/_build/html/_sources/Modules.rst.txt index d8e992314..c20fc4fc3 100644 --- a/docs/RefMan/_build/html/_sources/Modules.rst.txt +++ b/docs/RefMan/_build/html/_sources/Modules.rst.txt @@ -370,6 +370,24 @@ other modules: x : [n] // A declarations of a constant +Interface module may contain ``type`` or ``type constraint`` synonyms: + +.. code-block:: cryptol + :caption: A nested interface module + + interface module I where + + type n : # // `n` is a numeric type + + type W = [n] // A type synonym, available when the interface is imported + + type constraint (fin n, n >= 1) + // Assumptions about the declared numeric type + + x : W // A declarations of a constant; uses type synonym. + + + Importing an Interface Module ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -582,7 +600,8 @@ an anonymous interface and using it straight away: The ``parameter`` block defines an interface module and uses it. Note that the parameters may not use things defined in ``M`` as -the interface is declared outside of ``M``. +the interface is declared outside of ``M``. The ``parameter`` +may contain the same sort of declarations that may appear in interfaces. Anonymous Instantiation Arguments diff --git a/docs/RefMan/_build/html/searchindex.js b/docs/RefMan/_build/html/searchindex.js index 5a40b6437..751034bba 100644 --- a/docs/RefMan/_build/html/searchindex.js +++ b/docs/RefMan/_build/html/searchindex.js @@ -1 +1 @@ -Search.setIndex({docnames:["BasicSyntax","BasicTypes","Expressions","FFI","Modules","OverloadedOperations","RefMan","TypeDeclarations"],envversion:{"sphinx.domains.c":2,"sphinx.domains.changeset":1,"sphinx.domains.citation":1,"sphinx.domains.cpp":4,"sphinx.domains.index":1,"sphinx.domains.javascript":2,"sphinx.domains.math":2,"sphinx.domains.python":3,"sphinx.domains.rst":2,"sphinx.domains.std":2,"sphinx.ext.todo":2,sphinx:56},filenames:["BasicSyntax.rst","BasicTypes.rst","Expressions.rst","FFI.rst","Modules.rst","OverloadedOperations.rst","RefMan.rst","TypeDeclarations.rst"],objects:{},objnames:{},objtypes:{},terms:{"0":[0,1,2,3],"0254":0,"0b":0,"0b1010":0,"0b1010111":0,"0b11010":0,"0b11111110":0,"0b_0000_0010":0,"0o":0,"0o1234":0,"0o376":0,"0x":0,"0x00000003":3,"0x01":4,"0x02":4,"0x03":4,"0x04":4,"0x0f":3,"0x1234":0,"0x30":0,"0x_ffff_ffea":0,"0xaf":3,"0xf":3,"0xfe":0,"1":[0,1,2,3,4,7],"10":[0,1,3,4],"100":1,"11":4,"12":[0,4],"13":2,"15":1,"16":[0,3],"1p4":0,"2":[0,1,2,3,4,7],"20":[1,3],"22":2,"25":1,"254":0,"26":4,"2e3":0,"3":[0,1,2,4,7],"30":[1,4],"32":[3,4],"33":2,"4":[0,3],"5":[0,1,2,4],"6":[0,7],"64":[0,3],"7":[0,2,4],"8":[2,3,4],"9":2,"case":[3,4],"do":[0,2,3,4,7],"float":[0,6],"function":[0,4,6,7],"import":[0,1,2,6],"long":0,"new":[4,7],"public":4,"return":6,"static":[0,3],"true":[1,3],"try":[3,4],"void":3,"while":[0,1,3],A:[0,1,3,4,7],For:[0,1,2,3,4,7],If:[2,3,4],In:[3,4],It:[3,4],On:3,Such:[0,4],That:3,The:[0,1,2,3,4],Then:[3,4],There:[0,1],These:3,To:4,_:[0,1],a1:3,ab:5,abbrevi:1,abl:4,about:4,abov:[2,3,4],access:[2,3,6],accommod:2,across:[3,4],actual:[0,3],ad:[2,3,4],add:[3,4],addit:[0,4],adjac:3,after:3,ak:3,alias:0,all:[0,2,3,4,7],alloc:3,allow:[0,3,4,7],along:3,alphabet:1,alreadi:3,also:[0,1,3,4],alwai:3,an:[0,1,2,3,6],ani:[3,4,7],annot:6,anonym:6,anoth:4,appear:[1,7],appli:[0,3],applic:2,appropri:3,ar:[0,1,2,3,4,7],arbitrari:3,arbitrarili:0,argument:[3,6,7],arithmet:[1,6],arr:1,arrai:3,associ:0,assum:0,assumpt:[0,4],attempt:0,automat:[2,3],avoid:4,awai:4,b:[0,3,4,5,7],back:1,backtick:2,baddef:1,base:[0,2],basic:6,becaus:[0,3,4],befor:[3,4],begin:0,behav:3,behavior:[0,1,3],being:4,belong:0,between:[0,6],binari:[0,3],bind:[1,3],bit:[0,1,2,4,5,6],bitvector:1,block:[0,6],bodi:[3,7],both:[1,3,4],bound:[1,3],brace:1,branch:[0,2],bring:[4,7],built:[3,6],c1:3,c:6,call:[1,3,4,6],can:[0,1,2,3,4,7],cannot:[0,2],care:3,cc:3,ceil:[0,5],certain:3,chang:0,charact:0,check:[0,3],checker:[0,7],chosen:2,clash:4,claus:4,clear:3,close:0,closest:0,cmp:5,cn:3,code:[4,6],collect:[1,7],collis:4,combin:4,comma:1,command:3,comment:6,compar:1,comparison:6,compil:6,complement:5,complex:1,compon:[1,3],comprehens:1,comput:[0,1],concaten:1,concret:4,condit:6,consid:[0,4,7],consist:0,constant:[3,4],constrain:0,constraint:6,construct:[1,2,4],contain:[0,1,3,4],content:4,context:[0,2],contigu:3,control:0,conveni:4,convent:3,convers:3,convert:6,correct:3,correspond:[2,3],could:3,coupl:4,cours:4,creat:7,cry:[3,4],cryptol:[0,2,4],cryptolpath:4,cumbersom:[3,4],curli:1,current:3,curri:3,data:1,dealloc:3,decim:0,decis:0,declar:[3,4,6],defin:[0,1,3,4,7],definit:[0,1,2,4],defint:2,degre:0,demot:[0,6],depend:[0,3],deriv:4,describ:[3,4],descript:1,desrib:4,determin:[0,1],differ:[0,3,4],digit:0,dimens:3,dimension:1,directli:[3,7],directori:[3,4],distance2:1,distinct:7,divis:[0,6],dll:3,document:0,doe:[0,3],don:3,done:[3,4],doubl:3,down:[0,1],downward:1,drop:0,dylib:3,dynam:3,dynamiclib:3,e11:1,e12:1,e1:1,e21:1,e22:1,e2:1,e3:1,e:[0,1,4,5],each:[0,3,4,7],earlier:3,easi:4,easier:4,effect:0,either:[0,3,4],element:[1,2,3],els:[0,2,4],empti:3,enclos:[1,4],end:[0,4],english:0,enough:3,entri:1,enumer:1,environment:0,eq:5,equal:[0,1,6,7],equat:1,equival:4,error:[3,4],etc:0,evalu:[2,6],even:[0,7],everi:7,everyth:4,ex:1,exact:3,examin:1,exampl:[0,1,2,4,6],except:[0,3,4],exclus:1,exhaust:0,exist:[4,7],expand:3,explicit:[1,4,6],explicitli:[0,3],expon:0,exponenti:0,express:[0,1,4,6,7],extend:4,extens:3,extern:0,extra:3,extract:7,f1:3,f2:3,f:[0,1,2,3,4],fact:0,fals:[1,3],famili:0,few:4,ffi:3,field:[3,5,6,7],file:[3,4],fill:4,fin:[0,3,4],finit:[1,2],first:[0,1,3,4],fit:3,fix:[0,1,3],flatten:3,float32:3,float64:3,floor:5,fn:3,follow:[0,1,2,3,4],foo:3,foreign:6,form:7,fpic:3,fraction:0,from:[0,1,2,3,4],frominteg:5,front:1,fulli:3,functoin:0,functor:4,furthermor:3,g:[0,2,4],gener:[1,3],get:1,getfst:1,given:3,glu:4,gmp:3,good:4,group:[0,4,7],guard:6,h:[2,3,4],ha:[0,1,2,3],had:7,handi:1,handl:3,happen:4,hash:4,have:[0,1,2,3,4,7],header:3,help:[3,4],helper1:4,helper2:4,helper:4,here:[0,2,4],hexadecim:0,hide:[0,6],hierarch:6,high:3,highest:0,hold:[1,3],how:3,howev:3,i:[0,1,4],identifi:[1,4,6],ignor:3,impl1:4,impl2:4,impl:4,implement:[3,4],implicit:6,implict:0,impos:4,improv:[0,3],in0:3,in1_a:3,in1_b:3,includ:[0,3],indent:[0,4],independ:0,index:1,individu:3,inf:[1,5],infer:[0,2],inffrom:5,inffromthen:5,infinit:1,infix:[0,6],infixl:0,infixr:0,inform:1,init:3,input:3,instanc:3,instanti:6,instead:[0,3,4,7],insuffici:1,integ:[0,2,3,5,7],integr:[3,6],intend:4,interfac:[0,6],introduc:4,invalid:1,involv:3,irrelev:7,isposit:1,issu:0,its:[0,3,4],itself:[3,4],j:[1,4],just:[3,4,7],k:3,keword:4,keyword:[4,6],kind:[2,3],know:3,known:1,l:[1,3],label:1,lambda:[1,2],languag:[0,3],larg:[2,3],larger:3,last:[0,2,3],layout:[4,6],left:[0,1],len:0,length:[0,1],less:0,let:[0,3],letter:0,level:[4,6],lexicograph:1,lg2:0,libffi:3,librari:3,lift:1,like:[3,4,7],limit:3,line:[0,7],link:4,linux:3,list:[0,3,6],liter:[2,6],load:3,local:[0,4,6],locat:[1,4],logarithm:0,logic:6,longer_nam:0,longernam:0,look:[3,4],lowest:0,m:4,maco:3,mai:[0,1,2,3,4,7],main:3,make:4,manag:[3,6],mani:[3,4],manual:3,map:3,mark:0,match:[0,1,3],math:6,matter:3,max:[0,5],maximum:0,mayb:4,mean:[0,3],member:7,memori:6,mention:[3,7],might:4,min:[0,5],minimum:0,mirror:1,modifi:3,modul:[0,3,6],modulu:0,more:[0,4],moreov:7,most:[1,4],mpq_t:3,mpz_q:3,mpz_t:3,multidimension:3,multipl:[0,1,2,3,4],must:[0,3,4],my:4,myf:4,n1:3,n2:3,n:[0,1,3,4],name1:0,name2:0,name:[0,1,3,6,7],need:[0,2,3,4],negat:5,nest:[0,1,3,6],newt:7,newtyp:[0,4,6],ni:3,nk:3,non:[0,3],nonzero:3,notat:[0,1,2,4],note:[1,3,4],noth:4,notion:4,now:3,number:[0,1,2,3],numer:[3,4,6],o:3,obtain:[1,3,4],occasion:4,octal:0,often:1,old:1,onc:[3,4],one:[0,2,3,4],onli:[0,1,3,4,7],open:0,oper:[3,6],option:[0,7],order:[1,3,4],ordinari:4,organ:0,other:[0,3,4,7],otherwis:7,our:3,out:3,out_0:3,out_1:3,outer:4,output:3,outsid:4,over:0,overal:6,overload:[0,6],overview:2,ox:0,p11:1,p12:1,p1:1,p21:1,p22:1,p2:1,p3:1,p4:1,p:[0,1,4],packag:1,pad:[0,3],pair:2,paramet:[0,2,6],parameter:6,paren:2,parenthes:1,parmaet:4,pass:[2,3,6],pattern:[1,2],piec:3,place:4,platform:6,point:[1,6],pointer:3,pointwis:1,polymorph:[2,3],polynomi:0,portabl:3,posit:1,possibl:[2,3,4],practic:[3,4],pragma:0,pre:7,preced:[2,4],precis:[0,3],prefix:[0,4,6],presum:4,previou:[0,4],prime:0,primit:0,primtiv:2,principl:0,privat:[0,6],process:3,program:1,programm:0,project:7,properti:0,prototyp:3,prove:0,provid:[0,2,4],pt:1,purpos:[1,7],qualifi:6,quick:6,quickli:1,quit:[0,1,4],r:1,rather:0,ration:[0,3],read:3,readabl:[0,3],recip:5,record:[6,7],recurs:[3,4,7],reduc:4,refer:4,reject:0,rel:1,relat:4,remain:4,repl:1,repres:[0,3],represent:[0,3],requir:[0,3,4],respect:3,result:[0,1,2,3,4],right:[0,1],ring:5,rotat:1,round:[0,6],roundawai:5,roundtoeven:5,rule:3,runtim:3,s:[0,2,3,4],same:[0,1,3,4,7],satisfi:[0,3],scope:[2,4,7],search:4,section:[2,3,4],see:[0,4],selector:1,semant:4,separ:[1,4],seq:7,sequenc:[0,6],set:[0,1,3],sha256:4,shadow:4,shape:1,share:3,shift:1,should:[0,1,2,3],sign:[1,6],signatur:[3,6],signedcmp:5,similar:[0,3],similarli:1,simpl:[3,4],simpli:0,sinc:[3,4],singl:4,site:7,situat:4,size:[0,1,3],size_t:3,slight:4,smaller:3,so:[0,1,2,3,4],some:[0,4],someth:3,sometim:4,somewher:4,sourc:[3,4],special:0,specif:3,specifi:[0,2,4],split:[1,3],standard:3,start:[0,1],statement:0,step:[1,4],still:3,store:3,straight:4,stream:1,stride:1,structur:[4,6],sub:[1,4],submdul:4,submodul:[0,4],submould:4,subtract:0,suffici:[1,2],sugar:[2,4],suitabl:2,sum:7,sumbodul:4,support:[0,4,6],suppos:3,sure:4,symbol:[0,3,4],synonym:[4,6],syntact:4,syntax:[1,2,6],system:[3,4],t1:[1,3],t2:[1,3],t3:1,t:[0,1,2,3,4,7],tabl:[0,3],take:3,tend:4,term:0,termin:0,test:3,text:0,than:[0,3,4],thei:[0,1,3,4,7],them:4,themselv:3,thi:[0,1,2,3,4],thing:4,those:[1,4],though:7,three:1,through:[1,6],thu:[1,4],ti:3,time:4,tm:3,tn:3,togeth:[1,4],tointeg:5,too:3,top:[3,4],tr:3,translat:3,transpar:7,treat:[3,4,7],trunc:5,tupl:6,two:[0,1,2,4,7],typaram:2,type:[4,6],typecheck:7,typeclass:7,u1:3,u2:3,u:3,ui:3,uint16_t:3,uint32_t:3,uint64_t:3,uint8_t:3,un:3,unari:[0,2],undefin:3,underscor:0,understand:[3,4],unfold:7,uniniti:3,unlik:7,up:0,updat:6,updateend:1,updatesend:1,us:[0,1,2,3,4,7],usag:6,user:7,usual:2,v1:3,v2:3,valid:1,valu:[0,1,4,6,7],variabl:[2,3],variat:4,varieti:0,vector:6,version:3,vi:3,via:1,vn:3,wa:4,wai:[1,3,4],want:[3,4],warn:0,warnnonexhaustiveconstraintguard:0,we:[1,3,4],weakest:2,what:3,when:[0,1,2,3,4],where:[0,1,2,3,4],wherea:1,which:[0,2,3,4,7],whole:[2,3,4],width:[0,4],window:3,wise:1,withing:4,without:4,word:[1,3],work:[3,4],worth:3,would:[3,4,7],write:[0,1,3],written:[0,1,2,3,7],x:[0,1,2,3,4,7],xpo:1,xs:[0,1],y:[0,1,2,3,4],you:[2,3,4],your:3,ypo:1,z:[0,2,3,4],zero:[2,3,6]},titles:["Basic Syntax","Basic Types","Expressions","Foreign Function Interface","Modules","Overloaded Operations","Cryptol Reference Manual","Type Declarations"],titleterms:{"float":3,"function":[1,2,3],"import":4,"return":3,access:1,an:4,annot:2,anonym:4,argument:[2,4],arithmet:5,basic:[0,1,3,5],between:3,bit:3,block:[2,4],built:0,c:3,call:2,code:3,comment:0,comparison:5,compil:3,condit:2,constraint:[0,4],convert:3,cryptol:[3,6],declar:[0,2,7],demot:2,divis:5,equal:5,evalu:3,exampl:3,explicit:2,express:2,field:1,foreign:3,guard:0,hide:4,hierarch:4,identifi:0,implicit:4,infix:2,instanti:[2,4],integr:5,interfac:[3,4],keyword:0,layout:0,level:0,list:4,liter:0,local:2,logic:5,manag:4,manual:6,math:3,memori:3,modul:4,name:4,nest:4,newtyp:7,numer:[0,2],oper:[0,1,2,5],overal:3,overload:5,paramet:[3,4],parameter:4,pass:4,platform:3,point:3,preced:0,prefix:2,privat:4,qualifi:4,quick:3,record:[1,3],refer:[3,6],round:5,sequenc:[1,3],sign:5,signatur:0,structur:3,support:3,synonym:[3,7],syntax:0,through:4,todo:[0,2],tupl:[1,3],type:[0,1,2,3,7],updat:1,usag:3,valu:[2,3],vector:3,zero:5}}) \ No newline at end of file +Search.setIndex({docnames:["BasicSyntax","BasicTypes","Expressions","FFI","Modules","OverloadedOperations","RefMan","TypeDeclarations"],envversion:{"sphinx.domains.c":2,"sphinx.domains.changeset":1,"sphinx.domains.citation":1,"sphinx.domains.cpp":4,"sphinx.domains.index":1,"sphinx.domains.javascript":2,"sphinx.domains.math":2,"sphinx.domains.python":3,"sphinx.domains.rst":2,"sphinx.domains.std":2,"sphinx.ext.todo":2,sphinx:56},filenames:["BasicSyntax.rst","BasicTypes.rst","Expressions.rst","FFI.rst","Modules.rst","OverloadedOperations.rst","RefMan.rst","TypeDeclarations.rst"],objects:{},objnames:{},objtypes:{},terms:{"0":[0,1,2,3],"0254":0,"0b":0,"0b1010":0,"0b1010111":0,"0b11010":0,"0b11111110":0,"0b_0000_0010":0,"0o":0,"0o1234":0,"0o376":0,"0x":0,"0x00000003":3,"0x01":4,"0x02":4,"0x03":4,"0x04":4,"0x0f":3,"0x1234":0,"0x30":0,"0x_ffff_ffea":0,"0xaf":3,"0xf":3,"0xfe":0,"1":[0,1,2,3,4,7],"10":[0,1,3,4],"100":1,"11":4,"12":[0,4],"13":2,"15":1,"16":[0,3],"1p4":0,"2":[0,1,2,3,4,7],"20":[1,3],"22":2,"25":1,"254":0,"26":4,"2e3":0,"3":[0,1,2,4,7],"30":[1,4],"32":[3,4],"33":2,"4":[0,3],"5":[0,1,2,4],"6":[0,7],"64":[0,3],"7":[0,2,4],"8":[2,3,4],"9":2,"case":[3,4],"do":[0,2,3,4,7],"float":[0,6],"function":[0,4,6,7],"import":[0,1,2,6],"long":0,"new":[4,7],"public":4,"return":6,"static":[0,3],"true":[1,3],"try":[3,4],"void":3,"while":[0,1,3],A:[0,1,3,4,7],For:[0,1,2,3,4,7],If:[2,3,4],In:[3,4],It:[3,4],On:3,Such:[0,4],That:3,The:[0,1,2,3,4],Then:[3,4],There:[0,1],These:3,To:4,_:[0,1],a1:3,ab:5,abbrevi:1,abl:4,about:4,abov:[2,3,4],access:[2,3,6],accommod:2,across:[3,4],actual:[0,3],ad:[2,3,4],add:[3,4],addit:[0,4],adjac:3,after:3,ak:3,alias:0,all:[0,2,3,4,7],alloc:3,allow:[0,3,4,7],along:3,alphabet:1,alreadi:3,also:[0,1,3,4],alwai:3,an:[0,1,2,3,6],ani:[3,4,7],annot:6,anonym:6,anoth:4,appear:[1,4,7],appli:[0,3],applic:2,appropri:3,ar:[0,1,2,3,4,7],arbitrari:3,arbitrarili:0,argument:[3,6,7],arithmet:[1,6],arr:1,arrai:3,associ:0,assum:0,assumpt:[0,4],attempt:0,automat:[2,3],avail:4,avoid:4,awai:4,b:[0,3,4,5,7],back:1,backtick:2,baddef:1,base:[0,2],basic:6,becaus:[0,3,4],befor:[3,4],begin:0,behav:3,behavior:[0,1,3],being:4,belong:0,between:[0,6],binari:[0,3],bind:[1,3],bit:[0,1,2,4,5,6],bitvector:1,block:[0,6],bodi:[3,7],both:[1,3,4],bound:[1,3],brace:1,branch:[0,2],bring:[4,7],built:[3,6],c1:3,c:6,call:[1,3,4,6],can:[0,1,2,3,4,7],cannot:[0,2],care:3,cc:3,ceil:[0,5],certain:3,chang:0,charact:0,check:[0,3],checker:[0,7],chosen:2,clash:4,claus:4,clear:3,close:0,closest:0,cmp:5,cn:3,code:[4,6],collect:[1,7],collis:4,combin:4,comma:1,command:3,comment:6,compar:1,comparison:6,compil:6,complement:5,complex:1,compon:[1,3],comprehens:1,comput:[0,1],concaten:1,concret:4,condit:6,consid:[0,4,7],consist:0,constant:[3,4],constrain:0,constraint:6,construct:[1,2,4],contain:[0,1,3,4],content:4,context:[0,2],contigu:3,control:0,conveni:4,convent:3,convers:3,convert:6,correct:3,correspond:[2,3],could:3,coupl:4,cours:4,creat:7,cry:[3,4],cryptol:[0,2,4],cryptolpath:4,cumbersom:[3,4],curli:1,current:3,curri:3,data:1,dealloc:3,decim:0,decis:0,declar:[3,4,6],defin:[0,1,3,4,7],definit:[0,1,2,4],defint:2,degre:0,demot:[0,6],depend:[0,3],deriv:4,describ:[3,4],descript:1,desrib:4,determin:[0,1],differ:[0,3,4],digit:0,dimens:3,dimension:1,directli:[3,7],directori:[3,4],distance2:1,distinct:7,divis:[0,6],dll:3,document:0,doe:[0,3],don:3,done:[3,4],doubl:3,down:[0,1],downward:1,drop:0,dylib:3,dynam:3,dynamiclib:3,e11:1,e12:1,e1:1,e21:1,e22:1,e2:1,e3:1,e:[0,1,4,5],each:[0,3,4,7],earlier:3,easi:4,easier:4,effect:0,either:[0,3,4],element:[1,2,3],els:[0,2,4],empti:3,enclos:[1,4],end:[0,4],english:0,enough:3,entri:1,enumer:1,environment:0,eq:5,equal:[0,1,6,7],equat:1,equival:4,error:[3,4],etc:0,evalu:[2,6],even:[0,7],everi:7,everyth:4,ex:1,exact:3,examin:1,exampl:[0,1,2,4,6],except:[0,3,4],exclus:1,exhaust:0,exist:[4,7],expand:3,explicit:[1,4,6],explicitli:[0,3],expon:0,exponenti:0,express:[0,1,4,6,7],extend:4,extens:3,extern:0,extra:3,extract:7,f1:3,f2:3,f:[0,1,2,3,4],fact:0,fals:[1,3],famili:0,few:4,ffi:3,field:[3,5,6,7],file:[3,4],fill:4,fin:[0,3,4],finit:[1,2],first:[0,1,3,4],fit:3,fix:[0,1,3],flatten:3,float32:3,float64:3,floor:5,fn:3,follow:[0,1,2,3,4],foo:3,foreign:6,form:7,fpic:3,fraction:0,from:[0,1,2,3,4],frominteg:5,front:1,fulli:3,functoin:0,functor:4,furthermor:3,g:[0,2,4],gener:[1,3],get:1,getfst:1,given:3,glu:4,gmp:3,good:4,group:[0,4,7],guard:6,h:[2,3,4],ha:[0,1,2,3],had:7,handi:1,handl:3,happen:4,hash:4,have:[0,1,2,3,4,7],header:3,help:[3,4],helper1:4,helper2:4,helper:4,here:[0,2,4],hexadecim:0,hide:[0,6],hierarch:6,high:3,highest:0,hold:[1,3],how:3,howev:3,i:[0,1,4],identifi:[1,4,6],ignor:3,impl1:4,impl2:4,impl:4,implement:[3,4],implicit:6,implict:0,impos:4,improv:[0,3],in0:3,in1_a:3,in1_b:3,includ:[0,3],indent:[0,4],independ:0,index:1,individu:3,inf:[1,5],infer:[0,2],inffrom:5,inffromthen:5,infinit:1,infix:[0,6],infixl:0,infixr:0,inform:1,init:3,input:3,instanc:3,instanti:6,instead:[0,3,4,7],insuffici:1,integ:[0,2,3,5,7],integr:[3,6],intend:4,interfac:[0,6],introduc:4,invalid:1,involv:3,irrelev:7,isposit:1,issu:0,its:[0,3,4],itself:[3,4],j:[1,4],just:[3,4,7],k:3,keword:4,keyword:[4,6],kind:[2,3],know:3,known:1,l:[1,3],label:1,lambda:[1,2],languag:[0,3],larg:[2,3],larger:3,last:[0,2,3],layout:[4,6],left:[0,1],len:0,length:[0,1],less:0,let:[0,3],letter:0,level:[4,6],lexicograph:1,lg2:0,libffi:3,librari:3,lift:1,like:[3,4,7],limit:3,line:[0,7],link:4,linux:3,list:[0,3,6],liter:[2,6],load:3,local:[0,4,6],locat:[1,4],logarithm:0,logic:6,longer_nam:0,longernam:0,look:[3,4],lowest:0,m:4,maco:3,mai:[0,1,2,3,4,7],main:3,make:4,manag:[3,6],mani:[3,4],manual:3,map:3,mark:0,match:[0,1,3],math:6,matter:3,max:[0,5],maximum:0,mayb:4,mean:[0,3],member:7,memori:6,mention:[3,7],might:4,min:[0,5],minimum:0,mirror:1,modifi:3,modul:[0,3,6],modulu:0,more:[0,4],moreov:7,most:[1,4],mpq_t:3,mpz_q:3,mpz_t:3,multidimension:3,multipl:[0,1,2,3,4],must:[0,3,4],my:4,myf:4,n1:3,n2:3,n:[0,1,3,4],name1:0,name2:0,name:[0,1,3,6,7],need:[0,2,3,4],negat:5,nest:[0,1,3,6],newt:7,newtyp:[0,4,6],ni:3,nk:3,non:[0,3],nonzero:3,notat:[0,1,2,4],note:[1,3,4],noth:4,notion:4,now:3,number:[0,1,2,3],numer:[3,4,6],o:3,obtain:[1,3,4],occasion:4,octal:0,often:1,old:1,onc:[3,4],one:[0,2,3,4],onli:[0,1,3,4,7],open:0,oper:[3,6],option:[0,7],order:[1,3,4],ordinari:4,organ:0,other:[0,3,4,7],otherwis:7,our:3,out:3,out_0:3,out_1:3,outer:4,output:3,outsid:4,over:0,overal:6,overload:[0,6],overview:2,ox:0,p11:1,p12:1,p1:1,p21:1,p22:1,p2:1,p3:1,p4:1,p:[0,1,4],packag:1,pad:[0,3],pair:2,paramet:[0,2,6],parameter:6,paren:2,parenthes:1,parmaet:4,pass:[2,3,6],pattern:[1,2],piec:3,place:4,platform:6,point:[1,6],pointer:3,pointwis:1,polymorph:[2,3],polynomi:0,portabl:3,posit:1,possibl:[2,3,4],practic:[3,4],pragma:0,pre:7,preced:[2,4],precis:[0,3],prefix:[0,4,6],presum:4,previou:[0,4],prime:0,primit:0,primtiv:2,principl:0,privat:[0,6],process:3,program:1,programm:0,project:7,properti:0,prototyp:3,prove:0,provid:[0,2,4],pt:1,purpos:[1,7],qualifi:6,quick:6,quickli:1,quit:[0,1,4],r:1,rather:0,ration:[0,3],read:3,readabl:[0,3],recip:5,record:[6,7],recurs:[3,4,7],reduc:4,refer:4,reject:0,rel:1,relat:4,remain:4,repl:1,repres:[0,3],represent:[0,3],requir:[0,3,4],respect:3,result:[0,1,2,3,4],right:[0,1],ring:5,rotat:1,round:[0,6],roundawai:5,roundtoeven:5,rule:3,runtim:3,s:[0,2,3,4],same:[0,1,3,4,7],satisfi:[0,3],scope:[2,4,7],search:4,section:[2,3,4],see:[0,4],selector:1,semant:4,separ:[1,4],seq:7,sequenc:[0,6],set:[0,1,3],sha256:4,shadow:4,shape:1,share:3,shift:1,should:[0,1,2,3],sign:[1,6],signatur:[3,6],signedcmp:5,similar:[0,3],similarli:1,simpl:[3,4],simpli:0,sinc:[3,4],singl:4,site:7,situat:4,size:[0,1,3],size_t:3,slight:4,smaller:3,so:[0,1,2,3,4],some:[0,4],someth:3,sometim:4,somewher:4,sort:4,sourc:[3,4],special:0,specif:3,specifi:[0,2,4],split:[1,3],standard:3,start:[0,1],statement:0,step:[1,4],still:3,store:3,straight:4,stream:1,stride:1,structur:[4,6],sub:[1,4],submdul:4,submodul:[0,4],submould:4,subtract:0,suffici:[1,2],sugar:[2,4],suitabl:2,sum:7,sumbodul:4,support:[0,4,6],suppos:3,sure:4,symbol:[0,3,4],synonym:[4,6],syntact:4,syntax:[1,2,6],system:[3,4],t1:[1,3],t2:[1,3],t3:1,t:[0,1,2,3,4,7],tabl:[0,3],take:3,tend:4,term:0,termin:0,test:3,text:0,than:[0,3,4],thei:[0,1,3,4,7],them:4,themselv:3,thi:[0,1,2,3,4],thing:4,those:[1,4],though:7,three:1,through:[1,6],thu:[1,4],ti:3,time:4,tm:3,tn:3,togeth:[1,4],tointeg:5,too:3,top:[3,4],tr:3,translat:3,transpar:7,treat:[3,4,7],trunc:5,tupl:6,two:[0,1,2,4,7],typaram:2,type:[4,6],typecheck:7,typeclass:7,u1:3,u2:3,u:3,ui:3,uint16_t:3,uint32_t:3,uint64_t:3,uint8_t:3,un:3,unari:[0,2],undefin:3,underscor:0,understand:[3,4],unfold:7,uniniti:3,unlik:7,up:0,updat:6,updateend:1,updatesend:1,us:[0,1,2,3,4,7],usag:6,user:7,usual:2,v1:3,v2:3,valid:1,valu:[0,1,4,6,7],variabl:[2,3],variat:4,varieti:0,vector:6,version:3,vi:3,via:1,vn:3,w:4,wa:4,wai:[1,3,4],want:[3,4],warn:0,warnnonexhaustiveconstraintguard:0,we:[1,3,4],weakest:2,what:3,when:[0,1,2,3,4],where:[0,1,2,3,4],wherea:1,which:[0,2,3,4,7],whole:[2,3,4],width:[0,4],window:3,wise:1,withing:4,without:4,word:[1,3],work:[3,4],worth:3,would:[3,4,7],write:[0,1,3],written:[0,1,2,3,7],x:[0,1,2,3,4,7],xpo:1,xs:[0,1],y:[0,1,2,3,4],you:[2,3,4],your:3,ypo:1,z:[0,2,3,4],zero:[2,3,6]},titles:["Basic Syntax","Basic Types","Expressions","Foreign Function Interface","Modules","Overloaded Operations","Cryptol Reference Manual","Type Declarations"],titleterms:{"float":3,"function":[1,2,3],"import":4,"return":3,access:1,an:4,annot:2,anonym:4,argument:[2,4],arithmet:5,basic:[0,1,3,5],between:3,bit:3,block:[2,4],built:0,c:3,call:2,code:3,comment:0,comparison:5,compil:3,condit:2,constraint:[0,4],convert:3,cryptol:[3,6],declar:[0,2,7],demot:2,divis:5,equal:5,evalu:3,exampl:3,explicit:2,express:2,field:1,foreign:3,guard:0,hide:4,hierarch:4,identifi:0,implicit:4,infix:2,instanti:[2,4],integr:5,interfac:[3,4],keyword:0,layout:0,level:0,list:4,liter:0,local:2,logic:5,manag:4,manual:6,math:3,memori:3,modul:4,name:4,nest:4,newtyp:7,numer:[0,2],oper:[0,1,2,5],overal:3,overload:5,paramet:[3,4],parameter:4,pass:4,platform:3,point:3,preced:0,prefix:2,privat:4,qualifi:4,quick:3,record:[1,3],refer:[3,6],round:5,sequenc:[1,3],sign:5,signatur:0,structur:3,support:3,synonym:[3,7],syntax:0,through:4,todo:[0,2],tupl:[1,3],type:[0,1,2,3,7],updat:1,usag:3,valu:[2,3],vector:3,zero:5}}) \ No newline at end of file diff --git a/src/Cryptol/IR/TraverseNames.hs b/src/Cryptol/IR/TraverseNames.hs index 58f41207c..d9c289d29 100644 --- a/src/Cryptol/IR/TraverseNames.hs +++ b/src/Cryptol/IR/TraverseNames.hs @@ -249,4 +249,17 @@ instance TraverseNames FFIType where FFITuple ts -> FFITuple <$> traverseNamesIP ts FFIRecord mp -> FFIRecord <$> traverseRecordMap (\_ -> traverseNamesIP) mp +instance TraverseNames TySyn where + traverseNamesIP ts = mk <$> traverseNamesIP (tsName ts) + <*> traverseNamesIP (tsParams ts) + <*> traverseNamesIP (tsConstraints ts) + <*> traverseNamesIP (tsDef ts) + where mk n ps cs t = + TySyn { tsName = n + , tsParams = ps + , tsConstraints = cs + , tsDef = t + , tsDoc = tsDoc ts + } + diff --git a/src/Cryptol/ModuleSystem/Binds.hs b/src/Cryptol/ModuleSystem/Binds.hs index 737ca673d..80757bb9d 100644 --- a/src/Cryptol/ModuleSystem/Binds.hs +++ b/src/Cryptol/ModuleSystem/Binds.hs @@ -165,7 +165,7 @@ sigToMod mp sig = , modInstances = mempty , modMods = mempty , modDefines = env - , modPublic = mempty -- unused + , modPublic = namingEnvNames env , modState = () } @@ -240,6 +240,7 @@ signatureDefs :: ModPath -> Signature PName -> BuildNamingEnv signatureDefs m sig = mconcat [ namingEnv (InModule loc p) | p <- sigTypeParams sig ] <> mconcat [ namingEnv (InModule loc p) | p <- sigFunParams sig ] + <> mconcat [ namingEnv (InModule loc p) | p <- sigDecls sig ] where loc = Just m -------------------------------------------------------------------------------- @@ -395,6 +396,13 @@ instance BindsNames (InModule (Decl PName)) where do n <- mkName NSType ln f return (singletonNS NSType (thing ln) n) +instance BindsNames (InModule (SigDecl PName)) where + namingEnv (InModule m d) = + case d of + SigTySyn ts _ -> namingEnv (InModule m (DType ts)) + SigPropSyn ps _ -> namingEnv (InModule m (DProp ps)) + + -------------------------------------------------------------------------------- diff --git a/src/Cryptol/ModuleSystem/Env.hs b/src/Cryptol/ModuleSystem/Env.hs index db35f35d8..402a5be2d 100644 --- a/src/Cryptol/ModuleSystem/Env.hs +++ b/src/Cryptol/ModuleSystem/Env.hs @@ -198,6 +198,13 @@ data ModContextParams = | FunctorParams T.FunctorParams | NoParams +modContextParamNames :: ModContextParams -> T.ModParamNames +modContextParamNames mp = + case mp of + InterfaceParams ps -> ps + FunctorParams ps -> T.allParamNames ps + NoParams -> T.allParamNames mempty + -- | Contains enough information to browse what's in scope, -- or type check new expressions. data ModContext = ModContext diff --git a/src/Cryptol/ModuleSystem/NamingEnv.hs b/src/Cryptol/ModuleSystem/NamingEnv.hs index 97f15c068..dc4f931eb 100644 --- a/src/Cryptol/ModuleSystem/NamingEnv.hs +++ b/src/Cryptol/ModuleSystem/NamingEnv.hs @@ -236,7 +236,8 @@ modParamsNamingEnv :: T.ModParamNames -> NamingEnv modParamsNamingEnv T.ModParamNames { .. } = NamingEnv $ Map.fromList [ (NSValue, Map.fromList $ map fromFu $ Map.keys mpnFuns) - , (NSType, Map.fromList $ map fromTy $ Map.elems mpnTypes) + , (NSType, Map.fromList $ map fromTS (Map.elems mpnTySyn) ++ + map fromTy (Map.elems mpnTypes)) ] where toPName n = mkUnqual (nameIdent n) @@ -246,6 +247,8 @@ modParamsNamingEnv T.ModParamNames { .. } = fromFu f = (toPName f, One f) + fromTS ts = (toPName (T.tsName ts), One (T.tsName ts)) + -- | Generate a naming environment from a declaration interface, where none of -- the names are qualified. diff --git a/src/Cryptol/ModuleSystem/Renamer.hs b/src/Cryptol/ModuleSystem/Renamer.hs index c97d5deff..3ec6c6ea2 100644 --- a/src/Cryptol/ModuleSystem/Renamer.hs +++ b/src/Cryptol/ModuleSystem/Renamer.hs @@ -90,7 +90,7 @@ The Renamer Algorithm 3. Resolve imports and instantiations (see "Cryptol.ModuleSystem.Imports") - Resolves names in submodule imports - Resolves functor instantiations: - * generate new names for delcarations in the functors. + * generate new names for declarations in the functors. * this includes any nested modules, and things nested within them. - At this point we have enough information to know what's exported by each module. @@ -176,7 +176,7 @@ renameTopDecls :: ModName -> [TopDecl PName] -> RenameM (NamingEnv,[TopDecl Name]) renameTopDecls m ds0 = - do -- Step 1: add implicit importgs + do -- Step 1: add implicit imports let ds = addImplicitNestedImports ds0 -- Step 2: compute what's defined @@ -205,7 +205,7 @@ renameTopDecls m ds0 = pure (env,ds1) -------------------------------------------------------------------------------- --- Stuff below is related to Step 4 of the algorighm. +-- Stuff below is related to Step 4 of the algorithm. class Rename f where @@ -302,7 +302,6 @@ mkInstMap checkFun acc0 ogname iname - -- | This is used to rename local declarations (e.g. `where`) renameDecls :: [Decl PName] -> RenameM [Decl Name] renameDecls ds = @@ -325,6 +324,29 @@ renameDecls ds = pure [DRec bs] concat <$> mapM fromSCC ordered +-- | Rename declarations in a signature (i.e., type/prop synonyms) +renameSigDecls :: [SigDecl PName] -> RenameM [SigDecl Name] +renameSigDecls ds = + do (ds1,deps) <- depGroup (traverse rename ds) + let toNode d = let nm = case d of + SigTySyn ts _ -> thing (tsName ts) + SigPropSyn ps _ -> thing (psName ps) + x = NamedThing nm + in ((d,x), x, map NamedThing + $ Set.toList + $ Map.findWithDefault Set.empty x deps) + ordered = toList (stronglyConnComp (map toNode ds1)) + fromSCC x = + case x of + AcyclicSCC (d,_) -> pure [d] + CyclicSCC ds_xs -> + do let (rds,xs) = unzip ds_xs + recordError (InvalidDependency xs) + pure rds + + concat <$> mapM fromSCC ordered + + validRecursiveD :: Decl name -> Maybe (Bind name) validRecursiveD d = @@ -347,7 +369,7 @@ checkSameModule xs = -{- NOTE: Dependincies on Top Level Constraints +{- NOTE: Dependencies on Top Level Constraints =========================================== For the new module system, things using a parameter depend on the parameter @@ -356,7 +378,7 @@ so dependencies on constraints in there should be OK. However, we'd like to have a mechanism for declaring top level constraints in a functor, that can impose constraints across types from *different* -parameters. For the moment, we reuse `parameter type constrint C` for this. +parameters. For the moment, we reuse `parameter type constraint C` for this. Such constraints need to be: 1. After the signature import @@ -411,7 +433,7 @@ renameTopDecls' ds = ctrs = [ nm | (_,nm@(ConstratintAt {})) <- nameDs ] - {- See [NOTE: Dependincies on Top Level Constraints] -} + {- See [NOTE: Dependencies on Top Level Constraints] -} addCtr nm ctr = case nm of NamedThing x @@ -482,16 +504,18 @@ renameTopDecls' ds = where -- This indicates if a declaration might depend on the constraints in scope. - -- Since uses of contraints are not implicitly named, value declarations + -- Since uses of constraints are not implicitly named, value declarations -- are assumed to potentially use the constraints. - -- XXX: This is inacurate, and *I think* it amounts to checking that something + -- XXX: This is inaccurate, and *I think* it amounts to checking that something -- is in the value namespace. Perhaps the rule should be that a value - -- depends on a parameter constraint if it mentiones at least one + -- depends on a parameter constraint if it mentions at least one -- type parameter somewhere. -- XXX: Besides, types might need constraints for well-formedness... -- This is just bogus + -- Although not that type/prop synonyms may be defined wherever as they + -- keep the validity constraints they need and emit them at the *use* sites. usesCtrs td = case td of Decl tl -> isValDecl (tlValue tl) @@ -568,7 +592,7 @@ topDeclName topDecl = {- | Compute the names introduced by a module parameter. -This should be run in a context containg everything that's in scope +This should be run in a context containing everything that's in scope except for the module parameters. We don't need to compute a fixed point here because the signatures (and hence module parameters) cannot contain signatures. @@ -587,7 +611,7 @@ doModParam mp = (sigName',isFake) <- case thing sigName of ImpTop t -> pure (ImpTop t, False) - -- XXX: should we record a dpendency here? + -- XXX: should we record a dependency here? -- Not sure what the dependencies are for.. ImpNested n -> @@ -608,6 +632,10 @@ doModParam mp = (checkIsModule (srcRange sigName) sigName' ASignature) sigEnv <- if isFake then pure mempty else lookupDefines sigName' + + {- XXX: It seems a bit odd to use "newModParam" for the names to + be used for the instantiated type synonyms, + but what other name could we use? -} let newP x = do y <- lift (newModParam me (mpName mp) loc x) sets_ (Map.insert y x) pure y @@ -693,7 +721,7 @@ instance Rename ModParam where depsOf (ModParamName (srcRange (mpSignature mp)) (mpName mp)) do ren <- renModParamInstance <$> getModParam (mpName mp) - {- Here we add 2 "uses" to all type-level names intorduced, + {- Here we add 2 "uses" to all type-level names introduced, so that we don't get unused warnings for type parameters. -} mapM_ recordUse [ s | t <- Map.keys ren, nameNamespace t == NSType @@ -701,6 +729,7 @@ instance Rename ModParam where pure mp { mpSignature = x, mpRenaming = ren } + renameIfaceModule :: ImpName Name -> Signature PName -> RenameM (Signature Name) renameIfaceModule nm sig = do env <- rmodDefines <$> lookupResolved nm @@ -712,17 +741,23 @@ renameIfaceModule nm sig = do imps <- traverse renI (sigImports sig) tps <- traverse rename (sigTypeParams sig) + ds <- renameSigDecls (sigDecls sig) + cts <- traverse (rnLocated rename) (sigConstraints sig) + fun <- traverse rename (sigFunParams sig) + -- we record a use here to avoid getting a warning in interfaces -- that declare only types, and so appear "unused". forM_ tps \tp -> recordUse (thing (ptName tp)) + forM_ ds \d -> recordUse $ case d of + SigTySyn ts _ -> thing (tsName ts) + SigPropSyn ps _ -> thing (psName ps) - cts <- traverse (traverse rename) (sigConstraints sig) - fun <- traverse rename (sigFunParams sig) pure Signature - { sigImports = imps - , sigTypeParams = tps - , sigConstraints = cts - , sigFunParams = fun + { sigImports = imps + , sigTypeParams = tps + , sigDecls = ds + , sigConstraints = cts + , sigFunParams = fun } instance Rename ImpName where @@ -755,7 +790,7 @@ instance Rename NestedModule where nm = thing lnm n <- resolveName NameBind NSModule nm depsOf (NamedThing n) - do -- XXX: we should store in scope somehwere if we want to browse + do -- XXX: we should store in scope somewhere if we want to browse -- nested modules properly let m' = m { mName = ImpNested <$> mName m } (_inScope,m1) <- renameModule' (ImpNested n) m' @@ -771,7 +806,7 @@ instance Rename PrimType where -- Record an additional use for each parameter since we checked -- earlier that all the parameters are used exactly once in the - -- body of the signature. This prevents incorret warnings + -- body of the signature. This prevents incorrect warnings -- about unused names. mapM_ (recordUse . tpName) (fst cts) @@ -789,6 +824,12 @@ instance Rename ParameterFun where do sig' <- renameSchema (pfSchema a) return a { pfName = n', pfSchema = snd sig' } +instance Rename SigDecl where + rename decl = + case decl of + SigTySyn ts mb -> SigTySyn <$> rename ts <*> pure mb + SigPropSyn ps mb -> SigPropSyn <$> rename ps <*> pure mb + instance Rename Decl where rename d = case d of DBind b -> DBind <$> rename b diff --git a/src/Cryptol/Parser.y b/src/Cryptol/Parser.y index f2bb068d1..85ebe6ce2 100644 --- a/src/Cryptol/Parser.y +++ b/src/Cryptol/Parser.y @@ -342,8 +342,14 @@ par_decls :: { [ParamDecl PName] } par_decl :: { ParamDecl PName } : mbDoc name ':' schema { mkParFun $1 $2 $4 } | mbDoc 'type' name ':' kind {% mkParType $1 $3 $5 } - | mbDoc 'type' 'constraint' type {% fmap (DParameterConstraint . distrLoc) - (mkProp $4) } + | mbDoc 'type' 'constraint' '(' type ')' + {% fmap (DParameterConstraint . distrLoc) + (mkProp $5)} + | mbDoc 'type' 'constraint' '(' tuple_types ')' + {% fmap (DParameterConstraint . distrLoc) + (mkProp (at ($4,$6) (TTuple $5))) } + + | mbDoc typeOrPropSyn { mkIfacePropSyn (thing `fmap` $1) $2 } doc :: { Located Text } @@ -421,7 +427,16 @@ let_decl :: { Decl PName } | 'let' vars_comma ':' schema { at (head $2,$4) $ DSignature (reverse $2) $4 } - | 'type' name '=' type {% at ($1,$4) `fmap` mkTySyn $2 [] $4 } + | typeOrPropSyn { $1 } + + | 'infixl' NUM ops {% mkFixity LeftAssoc $2 (reverse $3) } + | 'infixr' NUM ops {% mkFixity RightAssoc $2 (reverse $3) } + | 'infix' NUM ops {% mkFixity NonAssoc $2 (reverse $3) } + + + +typeOrPropSyn :: { Decl PName } + : 'type' name '=' type {% at ($1,$4) `fmap` mkTySyn $2 [] $4 } | 'type' name tysyn_params '=' type {% at ($1,$5) `fmap` mkTySyn $2 (reverse $3) $5 } | 'type' tysyn_param op tysyn_param '=' type @@ -434,10 +449,6 @@ let_decl :: { Decl PName } | 'type' 'constraint' tysyn_param op tysyn_param '=' type {% at ($2,$7) `fmap` mkPropSyn $4 [$3, $5] $7 } - | 'infixl' NUM ops {% mkFixity LeftAssoc $2 (reverse $3) } - | 'infixr' NUM ops {% mkFixity RightAssoc $2 (reverse $3) } - | 'infix' NUM ops {% mkFixity NonAssoc $2 (reverse $3) } - diff --git a/src/Cryptol/Parser/AST.hs b/src/Cryptol/Parser/AST.hs index bce07979b..1571338a2 100644 --- a/src/Cryptol/Parser/AST.hs +++ b/src/Cryptol/Parser/AST.hs @@ -74,6 +74,7 @@ module Cryptol.Parser.AST , ParameterFun(..) , NestedModule(..) , Signature(..) + , SigDecl(..) , ModParam(..) , ParamDecl(..) , PropGuardCase(..) @@ -262,8 +263,11 @@ data ParamDecl name = | DParameterFun (ParameterFun name) -- ^ @parameter someVal : [256]@ -- (parser only) + | DParameterDecl (SigDecl name) -- ^ A delcaration in an interface + | DParameterConstraint [Located (Prop name)] -- ^ @parameter type constraint (fin T)@ + deriving (Show, Generic, NFData) @@ -354,7 +358,7 @@ data ParameterFun name = ParameterFun {- | Interface Modules (aka types of functor arguments) IMPORTANT: Interface Modules are a language construct and are different from -the notion of "interface" in the Cyrptol implementation. +the notion of "interface" in the Cryptol implementation. Note that the names *defined* in an interface module are only really used in the other members of the interface module. When an interface module is "imported" @@ -364,10 +368,19 @@ data Signature name = Signature { sigImports :: ![Located (ImportG (ImpName name))] -- ^ Add things in scope , sigTypeParams :: [ParameterType name] -- ^ Type parameters - , sigConstraints :: [Located (Prop name)] -- ^ Constraints on type params + , sigConstraints :: [Located (Prop name)] + -- ^ Constraints on the type parameters and type synonyms. + , sigDecls :: [SigDecl name] + -- ^ Type and constraint synonyms , sigFunParams :: [ParameterFun name] -- ^ Value parameters } deriving (Show,Generic,NFData) +-- | A constraint or type synonym declared in an interface. +data SigDecl name = + SigTySyn (TySyn name) (Maybe Text) + | SigPropSyn (PropSyn name) (Maybe Text) + deriving (Show,Generic,NFData) + {- | A module parameter declaration. > import interface A @@ -742,8 +755,15 @@ instance HasLoc (ParamDecl name) where case pd of DParameterType d -> getLoc d DParameterFun d -> getLoc d + DParameterDecl d -> getLoc d DParameterConstraint d -> getLoc d +instance HasLoc (SigDecl name) where + getLoc decl = + case decl of + SigTySyn ts _ -> getLoc ts + SigPropSyn ps _ -> getLoc ps + instance HasLoc (ModParam name) where getLoc mp = getLoc (mpSignature mp) @@ -776,6 +796,13 @@ instance HasLoc (Newtype name) where where locs = catMaybes ([ getLoc (nName n)] ++ map (Just . fst . snd) (displayFields (nBody n))) +instance HasLoc (TySyn name) where + getLoc (TySyn x _ _ _) = getLoc x + +instance HasLoc (PropSyn name) where + getLoc (PropSyn x _ _ _) = getLoc x + + -------------------------------------------------------------------------------- @@ -874,23 +901,29 @@ instance (Show name, PPName name) => PP (ParamDecl name) where case pd of DParameterFun d -> pp d DParameterType d -> pp d - DParameterConstraint d -> "type" <+> "constraint" <+> prop - where prop = case map (pp . thing) d of - [x] -> x - [] -> "()" - xs -> nest 1 (parens (commaSepFill xs)) + DParameterDecl d -> pp d + DParameterConstraint d -> + "type constraint" <+> parens (commaSep (map (pp . thing) d)) ppInterface :: (Show name, PPName name) => Doc -> Signature name -> Doc ppInterface kw sig = kw $$ indent 2 (vcat (is ++ ds)) where is = map pp (sigImports sig) + cs = case cs of + [] -> [] + _ -> ["type constraint" <+> + parens (commaSep (map (pp . thing) (sigConstraints sig)))] ds = map pp (sigTypeParams sig) - ++ case map (pp . thing) (sigConstraints sig) of - [x] -> ["type constraint" <+> x] - [] -> [] - xs -> ["type constraint" <+> parens (commaSep xs)] + ++ map pp (sigDecls sig) + ++ cs ++ map pp (sigFunParams sig) +instance (Show name, PPName name) => PP (SigDecl name) where + ppPrec p decl = + case decl of + SigTySyn ts _ -> ppPrec p ts + SigPropSyn ps _ -> ppPrec p ps + instance (Show name, PPName name) => PP (ModParam name) where ppPrec _ mp = vcat ( mbDoc @@ -1352,15 +1385,23 @@ instance NoPos (ParamDecl name) where case pd of DParameterFun d -> DParameterFun (noPos d) DParameterType d -> DParameterType (noPos d) + DParameterDecl d -> DParameterDecl (noPos d) DParameterConstraint d -> DParameterConstraint (noPos d) instance NoPos (Signature name) where noPos sig = Signature { sigImports = sigImports sig , sigTypeParams = map noPos (sigTypeParams sig) + , sigDecls = map noPos (sigDecls sig) , sigConstraints = map noPos (sigConstraints sig) , sigFunParams = map noPos (sigFunParams sig) } +instance NoPos (SigDecl name) where + noPos decl = + case decl of + SigTySyn ts mb -> SigTySyn (noPos ts) mb + SigPropSyn ps mb -> SigPropSyn (noPos ps) mb + instance NoPos (ModParam name) where noPos mp = ModParam { mpSignature = noPos (mpSignature mp) , mpAs = mpAs mp diff --git a/src/Cryptol/Parser/ParserUtils.hs b/src/Cryptol/Parser/ParserUtils.hs index 74b3bebc8..44bccb720 100644 --- a/src/Cryptol/Parser/ParserUtils.hs +++ b/src/Cryptol/Parser/ParserUtils.hs @@ -918,6 +918,7 @@ mkInterface is = foldl' add Signature { sigImports = is , sigTypeParams = [] + , sigDecls = [] , sigConstraints = [] , sigFunParams = [] } @@ -925,9 +926,18 @@ mkInterface is = where add s d = case d of - DParameterType pt -> s { sigTypeParams = pt : sigTypeParams s } + DParameterType pt -> s { sigTypeParams = pt : sigTypeParams s } DParameterConstraint ps -> s { sigConstraints = ps ++ sigConstraints s } - DParameterFun pf -> s { sigFunParams = pf : sigFunParams s } + DParameterDecl pd -> s { sigDecls = pd : sigDecls s } + DParameterFun pf -> s { sigFunParams = pf : sigFunParams s } + +mkIfacePropSyn :: Maybe Text -> Decl PName -> ParamDecl PName +mkIfacePropSyn mbDoc d = + case d of + DLocated d1 _ -> mkIfacePropSyn mbDoc d1 + DType ts -> DParameterDecl (SigTySyn ts mbDoc) + DProp ps -> DParameterDecl (SigPropSyn ps mbDoc) + _ -> panic "mkIfacePropSyn" [ "Unexpected declaration", show (pp d) ] -- | Make an unnamed module---gets the name @Main@. @@ -1102,7 +1112,7 @@ desugarMod mo = m : _ | InterfaceModule si <- mDef m , l : _ <- map (srcRange . ptName) (sigTypeParams si) ++ map (srcRange . pfName) (sigFunParams si) ++ - map srcRange (sigConstraints si) -> + [ srcRange (mName mo) ] -> errorMessage l [ "Instantiation of a parameterized module may not itself be " ++ "parameterized" ] @@ -1134,12 +1144,14 @@ desugarTopDs ownerName = go emptySig emptySig = Signature { sigImports = [] , sigTypeParams = [] + , sigDecls = [] , sigConstraints = [] , sigFunParams = [] } jnSig s1 s2 = Signature { sigImports = j sigImports , sigTypeParams = j sigTypeParams + , sigDecls = j sigDecls , sigConstraints = j sigConstraints , sigFunParams = j sigFunParams } diff --git a/src/Cryptol/REPL/Help.hs b/src/Cryptol/REPL/Help.hs index 2b2f70b62..f4fc4137c 100644 --- a/src/Cryptol/REPL/Help.hs +++ b/src/Cryptol/REPL/Help.hs @@ -234,7 +234,10 @@ showTypeHelp ctxparams env nameEnv name = where fromTySyn = - do ts <- Map.lookup name (M.ifTySyns env) + do ts <- msum [ Map.lookup name (M.ifTySyns env) + , Map.lookup name + (T.mpnTySyn (M.modContextParamNames ctxparams)) + ] return (doShowTyHelp nameEnv (pp ts) (T.tsDoc ts)) fromNewtype = diff --git a/src/Cryptol/TypeCheck/Infer.hs b/src/Cryptol/TypeCheck/Infer.hs index fd1f46c2b..eb853dfa0 100644 --- a/src/Cryptol/TypeCheck/Infer.hs +++ b/src/Cryptol/TypeCheck/Infer.hs @@ -1354,6 +1354,9 @@ checkTopDecls = mapM_ checkTopDecl ips <- lookupSignature (thing (P.mpSignature p)) let actualTys = [ mapNames actualName mp | mp <- Map.elems (mpnTypes ips) ] + actualTS = [ mapNames actualName ts + | ts <- Map.elems (mpnTySyn ips) + ] actualCtrs = [ mapNames actualName prop | prop <- mpnConstraints ips ] actualVals = [ mapNames actualName vp @@ -1367,7 +1370,8 @@ checkTopDecls = mapM_ checkTopDecl ModParamNames { mpnTypes = Map.fromList [ (mtpName tp, tp) | tp <- actualTys ] - + , mpnTySyn = Map.fromList [ (tsName ts, ts) + | ts <- actualTS ] , mpnConstraints = actualCtrs , mpnFuns = Map.fromList [ (mvpName vp, vp) | vp <- actualVals ] @@ -1378,6 +1382,7 @@ checkTopDecls = mapM_ checkTopDecl mapM_ addParamType actualTys addParameterConstraints actualCtrs mapM_ addParamFun actualVals + mapM_ addTySyn actualTS addModParam param P.DImport {} -> pure () @@ -1393,14 +1398,26 @@ checkSignature sig = do forM_ (P.sigTypeParams sig) \pt -> addParamType =<< checkParameterType pt + mapM_ checkSigDecl (P.sigDecls sig) + addParameterConstraints =<< - checkParameterConstraints (P.sigConstraints sig) + checkParameterConstraints (P.sigConstraints sig) forM_ (P.sigFunParams sig) \f -> addParamFun =<< checkParameterFun f proveModuleTopLevel +checkSigDecl :: P.SigDecl Name -> InferM () +checkSigDecl decl = + case decl of + + P.SigTySyn ts mbD -> + addTySyn =<< checkTySyn ts mbD + + P.SigPropSyn ps mbD -> + addTySyn =<< checkPropSyn ps mbD + checkDecl :: Bool -> P.Decl Name -> Maybe Text -> InferM () diff --git a/src/Cryptol/TypeCheck/ModuleInstance.hs b/src/Cryptol/TypeCheck/ModuleInstance.hs index ce42762b5..ddddd5a36 100644 --- a/src/Cryptol/TypeCheck/ModuleInstance.hs +++ b/src/Cryptol/TypeCheck/ModuleInstance.hs @@ -136,6 +136,7 @@ instance ModuleInstance ModParamNames where ModParamNames { mpnTypes = doMap (mpnTypes si) , mpnConstraints = moduleInstance (mpnConstraints si) , mpnFuns = doMap (mpnFuns si) + , mpnTySyn = doMap (mpnTySyn si) , mpnDoc = mpnDoc si } diff --git a/src/Cryptol/TypeCheck/Monad.hs b/src/Cryptol/TypeCheck/Monad.hs index 2a0e06f39..653b1b2f5 100644 --- a/src/Cryptol/TypeCheck/Monad.hs +++ b/src/Cryptol/TypeCheck/Monad.hs @@ -137,7 +137,8 @@ runInferM info m0 = , iExtModules = inpTopModules info , iExtSignatures = inpTopSignatures info , iExtScope = (emptyModule ExternalScope) - { mTySyns = inpTSyns info + { mTySyns = inpTSyns info <> + mpnTySyn allPs , mNewtypes = inpNewtypes info , mPrimTypes = inpAbstractTypes info , mParamTypes = mpnTypes allPs @@ -1082,6 +1083,7 @@ endSignature = { mpnTypes = mParamTypes x , mpnConstraints = mParamConstraints x , mpnFuns = mParamFuns x + , mpnTySyn = mTySyns x , mpnDoc = doc } _ -> panic "endSignature" [ "Not a signature scope" ] @@ -1095,6 +1097,7 @@ endTopSignature = { mpnTypes = mParamTypes x , mpnConstraints = mParamConstraints x , mpnFuns = mParamFuns x + , mpnTySyn = mTySyns x , mpnDoc = Nothing } , rw { iScope = [] } diff --git a/src/Cryptol/TypeCheck/Type.hs b/src/Cryptol/TypeCheck/Type.hs index 6271bfe13..417e341a8 100644 --- a/src/Cryptol/TypeCheck/Type.hs +++ b/src/Cryptol/TypeCheck/Type.hs @@ -53,6 +53,7 @@ allParamNames mps = { mpnTypes = Map.unions (map mpnTypes ps) , mpnConstraints = concatMap mpnConstraints ps , mpnFuns = Map.unions (map mpnFuns ps) + , mpnTySyn = Map.unions (map mpnTySyn ps) , mpnDoc = Nothing } where @@ -81,9 +82,13 @@ data ModParamNames = ModParamNames { mpnTypes :: Map Name ModTParam -- ^ Type parameters + , mpnTySyn :: !(Map Name TySyn) + -- ^ Type synonyms + , mpnConstraints :: [Located Prop] -- ^ Constraints on param. types + , mpnFuns :: Map.Map Name ModVParam -- ^ Value parameters @@ -1307,6 +1312,7 @@ instance PP ModParamNames where [ "type constraint" <+> parens (commaSep (map (pp . thing) (mpnConstraints ps))) ] ++ + [ pp t | t <- Map.elems (mpnTySyn ps) ] ++ map pp (Map.elems (mpnFuns ps)) instance PP ModTParam where diff --git a/tests/modsys/functors/T030.cry b/tests/modsys/functors/T030.cry new file mode 100644 index 000000000..c25757358 --- /dev/null +++ b/tests/modsys/functors/T030.cry @@ -0,0 +1,8 @@ +module T030 where + +import interface T030_I + +g : W -> X +g x = f + + diff --git a/tests/modsys/functors/T030.icry b/tests/modsys/functors/T030.icry new file mode 100644 index 000000000..67f654180 --- /dev/null +++ b/tests/modsys/functors/T030.icry @@ -0,0 +1,5 @@ +:load T030.cry +:help W +:t 1 : X +f +g diff --git a/tests/modsys/functors/T030.icry.stdout b/tests/modsys/functors/T030.icry.stdout new file mode 100644 index 000000000..11acf91f5 --- /dev/null +++ b/tests/modsys/functors/T030.icry.stdout @@ -0,0 +1,16 @@ +Loading module Cryptol +Loading module Cryptol +Loading interface module T030_I +Loading module T030 + +type W = X + +This is W's doc + +(1 : X) : X + +Expression depends on definitions from a parameterized module: + T030::T030_I::f + +Expression depends on definitions from a parameterized module: + T030::g diff --git a/tests/modsys/functors/T030_I.cry b/tests/modsys/functors/T030_I.cry new file mode 100644 index 000000000..347831256 --- /dev/null +++ b/tests/modsys/functors/T030_I.cry @@ -0,0 +1,10 @@ +interface module T030_I where + type n : # + + /** This is W's doc */ + type W = X + type X = [n] + type constraint P = fin n + type constraint (P, n >= 1) + f : X + diff --git a/tests/modsys/functors/T031.cry b/tests/modsys/functors/T031.cry new file mode 100644 index 000000000..62ff76b6f --- /dev/null +++ b/tests/modsys/functors/T031.cry @@ -0,0 +1,3 @@ +import T030 where + type n = 8 + f = 11 diff --git a/tests/modsys/functors/T031.icry b/tests/modsys/functors/T031.icry new file mode 100644 index 000000000..bef4e132c --- /dev/null +++ b/tests/modsys/functors/T031.icry @@ -0,0 +1,2 @@ +:load T031.cry +g 1 diff --git a/tests/modsys/functors/T031.icry.stdout b/tests/modsys/functors/T031.icry.stdout new file mode 100644 index 000000000..f10397c0e --- /dev/null +++ b/tests/modsys/functors/T031.icry.stdout @@ -0,0 +1,6 @@ +Loading module Cryptol +Loading module Cryptol +Loading interface module T030_I +Loading module T030 +Loading module Main +0x0b