https://github.com/EasyCrypt/easycrypt
Revision e00264462a3e0744c7bb76e0d8beb1092a4498f2 authored by Alley Stoughton on 20 November 2020, 08:05:03 UTC, committed by GitHub on 20 November 2020, 08:05:03 UTC
branches as the number of constructors in the datatype being matched, an exception was raised instead of the expected error message being issued. Example: type t = [A | B]. module M = { proc f(x : t) = { match x with | A => { } | A => { } end; } }.
1 parent 6c677e1
Tip revision: e00264462a3e0744c7bb76e0d8beb1092a4498f2 authored by Alley Stoughton on 20 November 2020, 08:05:03 UTC
When a match has duplicate constructors but the same number of (#47)
When a match has duplicate constructors but the same number of (#47)
Tip revision: e002644
ecSection.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 EcPath
open EcFol
open EcDecl
open EcModules
type locals
(* -------------------------------------------------------------------- *)
val env_of_locals : locals -> EcEnv.env
val items_of_locals : locals -> EcTheory.ctheory_item list
val is_local : [`Lemma | `Module] -> path -> locals -> bool
val is_mp_local : mpath -> locals -> bool
val form_use_local : form -> locals -> mpath option
val form_use_local_or_abs : form -> locals -> bool
val module_use_local_or_abs : module_expr -> locals -> bool
val opdecl_use_local_or_abs : operator -> locals -> bool
val tydecl_use_local_or_abs : tydecl -> locals -> bool
val abstracts : locals -> (EcIdent.t * (module_type * mod_restr)) list * Sid.t
val generalize : EcEnv.env -> locals -> form -> form
(* -------------------------------------------------------------------- *)
type t
exception NoSectionOpened
val initial : t
val in_section : t -> bool
val enter : EcEnv.env -> symbol option -> t -> t
val exit : t -> locals * t
val path : t -> symbol option * path
val opath : t -> (symbol option * path) option
val topenv : t -> EcEnv.env
val locals : t -> locals
val olocals : t -> locals option
type lvl = [`Local | `Global] * [`Axiom | `Lemma]
val add_local_mod : path -> t -> t
val add_lemma : path -> lvl -> t -> t
val add_item : EcTheory.ctheory_item -> t -> t
val add_abstract : EcIdent.t -> (module_type * mod_restr) -> t -> t
Computing file changes ...