https://github.com/EasyCrypt/easycrypt
Tip revision: 846710a2a656834065e745d19416ebdc83158f55 authored by Benjamin Gregoire on 14 July 2019, 06:50:07 UTC
Start restructuration of the code to be able to avant mutual dependency between type and mpath
Start restructuration of the code to be able to avant mutual dependency between type and mpath
Tip revision: 846710a
ecHiInductive.mli
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2016 - IMDEA Software Institute
* Copyright (c) - 2012--2018 - Inria
* Copyright (c) - 2012--2018 - Ecole Polytechnique
*
* Distributed under the terms of the CeCILL-C-V1 license
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
open EcSymbols
open EcIdent
open EcParsetree
open EcInductive
open EcEnv
(* -------------------------------------------------------------------- *)
type rcerror =
| RCE_TypeError of EcTyping.tyerror
| RCE_DuplicatedField of symbol
| RCE_InvalidFieldType of symbol * EcTyping.tyerror
| RCE_Empty
type dterror =
| DTE_TypeError of EcTyping.tyerror
| DTE_DuplicatedCtor of symbol
| DTE_InvalidCTorType of symbol * EcTyping.tyerror
| DTE_NonPositive
| DTE_Empty
type fxerror =
| FXE_TypeError of EcTyping.tyerror
| FXE_EmptyMatch
| FXE_MatchParamsMixed
| FXE_MatchParamsDup
| FXE_MatchParamsUnk
| FXE_MatchNonLinear
| FXE_MatchDupBranches
| FXE_MatchPartial
| FXE_CtorUnk
| FXE_CtorAmbiguous
| FXE_CtorInvalidArity of (symbol * int * int)
(* -------------------------------------------------------------------- *)
exception RcError of EcLocation.t * EcEnv.env * rcerror
exception DtError of EcLocation.t * EcEnv.env * dterror
exception FxError of EcLocation.t * EcEnv.env * fxerror
(* -------------------------------------------------------------------- *)
val rcerror : EcLocation.t -> EcEnv.env -> rcerror -> 'a
val dterror : EcLocation.t -> EcEnv.env -> dterror -> 'a
val fxerror : EcLocation.t -> EcEnv.env -> fxerror -> 'a
(* -------------------------------------------------------------------- *)
val trans_record : env -> ptydname -> precord -> record
(* -------------------------------------------------------------------- *)
val trans_datatype : env -> ptydname -> pdatatype -> datatype
(* -------------------------------------------------------------------- *)
type matchfix_t = {
mf_name : ident;
mf_codom : EcTypes.ty;
mf_args : (ident * EcTypes.ty) list;
mf_recs : int list;
mf_branches : EcDecl.opbranches;
}
val trans_matchfix :
?close:bool
-> EcEnv.env
-> EcUnify.unienv
-> psymbol
-> ptybindings * pty * pop_branch list
-> EcTypes.ty * matchfix_t