123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170(* Semantic verification *)openImportopenAstletadd_nameaccu=functionName(_,(_,k,_),_)->k::accu|_->acculetget_kind=functionSum_->`Sum|Record_->`Record|_->`Otherletcheck_inheritancetbl(t0:type_expr)=letnot_akind_=letmsg=sprintf"Cannot inherit from non-%s type"(matchkindwith`Sum->"variant"|`Record->"record"|_->assertfalse)inerror_at(loc_of_type_exprt0)msginletreccheckkindinherited(t:type_expr)=matchtwithSum(_,vl,_)whenkind=`Sum->List.iter(functionInherit(_,t)->checkkindinheritedt|Variant_->())vl|Record(_,fl,_)whenkind=`Record->List.iter(function`Inherit(_,t)->checkkindinheritedt|`Field_->())fl|Sum_|Record_|Tuple_|List_|Option_|Nullable_|Shared_|Wrap_asx->not_akindx|Name(_,(loc,k,_),_)->ifList.memkinheritedthenerror_at(loc_of_type_exprt0)"Cyclic inheritance"elselet(_arity,opt_def)=tryHashtbl.findtblkwithNot_found->error_atloc("Undefined type "^k)in(matchopt_defwithNone->()|Some(_,_,t)->checkkind(k::inherited)t)|Tvar_->error_at(loc_of_type_exprt0)"Cannot inherit from a type variable"incheck(get_kindt0)(add_name[]t0)t0letcheck_type_exprtbltvars(t:type_expr)=letreccheck:type_expr->unit=functionSum(_,vl,_)asx->List.iter(check_variant(Hashtbl.create10))vl;check_inheritancetblx|Record(_,fl,_)asx->List.iter(check_field(Hashtbl.create10))fl;check_inheritancetblx|Tuple(_,tl,_)->List.iter(fun(_,x,_)->checkx)tl|List(_,t,_)->checkt|Option(_,t,_)->checkt|Nullable(_,t,_)->checkt|Shared(loc,t,_)->ifAst.is_parametrizedtthenerror_atloc"Shared type cannot be polymorphic";checkt|Wrap(_,t,_)->checkt|Name(_,(loc,k,tal),_)->assert(k<>"list"&&k<>"option"&&k<>"nullable"&&k<>"shared"&&k<>"wrap");let(arity,_opt_def)=tryHashtbl.findtblkwithNot_found->error_atloc("Undefined type "^k)inletn=List.lengthtalinifarity<>nthenerror_atloc(sprintf"Type %s was defined to take %i parameters, \
but %i argument%s."karityn(ifn>1then"s are given"else" is given"));List.iterchecktal|Tvar(loc,s)->ifnot(List.memstvars)thenerror_atloc(sprintf"Unbound type variable '%s"s)andcheck_variantaccu=functionVariant(loc,(k,_),opt_t)->ifHashtbl.memaccukthenerror_atloc(sprintf"Multiple definitions of the same variant constructor %s"k);Hashtbl.addaccuk();(matchopt_twithNone->()|Somet->checkt)|Inherit(_,t)->(* overriding is allowed, for now without a warning *)checktandcheck_fieldaccu=function`Field(loc,(k,_,_),t)->ifHashtbl.memaccukthenerror_atloc(sprintf"Multiple definitions of the same field %s"k);Hashtbl.addaccuk();checkt|`Inherit(_,t)->(* overriding is allowed, for now without a warning *)checktinchecktletcheck(l:Ast.module_body)=letpredef=Predef.make_table()inlettbl=Hashtbl.copypredefin(* first pass: put all definitions in the table *)List.iter(functionType((loc,(k,pl,_),_)asx)->ifHashtbl.memtblkthenifHashtbl.mempredefkthenerror_atloc(sprintf"%s is a predefined type, it cannot be redefined."k)elseerror_atloc(sprintf"Type %s is defined for the second time."k)elseHashtbl.addtblk(List.lengthpl,Somex))l;(* second pass: check existence and arity of types in type expressions,
check that inheritance is not cyclic *)List.iter(function(Ast.Type(_,(_,tvars,_),t))->check_type_exprtbltvarst)l