Skip to main content

Browse the archive

https://github.com/EasyCrypt/easycrypt
05 April 2024, 19:20:55 UTC
Revision da719f05bd0e5199b1040c2bcbc97379aa4e7f8c authored by Alley Stoughton on 22 May 2020, 22:12:19 UTC, committed by Alley Stoughton on 22 May 2020, 22:12:19 UTC 
Allows nosmt with all operators other than pure, abstract ones - i.e.,
 
with plain, axiomatized (including : {t | phi} as ax) and cases operators.
When cloning, [op nosmt x = ...] is allowed, but nosmt can't be used
with inlining mode.
1 parent 170c443
Raw File
Tip revision: da719f05bd0e5199b1040c2bcbc97379aa4e7f8c authored by Alley Stoughton on 22 May 2020, 22:12:19 UTC
Allows nosmt with all operators other than pure, abstract ones - i.e.,
Tip revision: da719f0
ecUnify.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 EcUid
open EcSymbols
open EcPath
open EcTypes
open EcDecl

(* -------------------------------------------------------------------- *)
exception UnificationFailure of [`TyUni of ty * ty | `TcCtt of ty * Sp.t]
exception UninstanciateUni

type unienv

type tvar_inst =
| TVIunamed of ty list
| TVInamed  of (EcSymbols.symbol * ty) list

type tvi = tvar_inst option
type uidmap = uid -> ty option

module UniEnv : sig
  val create     : (EcIdent.t * Sp.t) list option -> unienv
  val copy       : unienv -> unienv                 (* constant time *)
  val restore    : dst:unienv -> src:unienv -> unit (* constant time *)
  val fresh      : ?tc:EcPath.Sp.t -> ?ty:ty -> unienv -> ty
  val getnamed   : unienv -> symbol -> EcIdent.t
  val repr       : unienv -> ty -> ty
  val opentvi    : unienv -> ty_params -> tvi -> ty EcIdent.Mid.t
  val openty     : unienv -> ty_params -> tvi -> ty -> ty * ty list
  val opentys    : unienv -> ty_params -> tvi -> ty list -> ty list * ty list
  val closed     : unienv -> bool
  val close      : unienv -> uidmap
  val assubst    : unienv -> uidmap
  val tparams    : unienv -> ty_params
end

val unify : EcEnv.env -> unienv -> ty -> ty -> unit
val hastc : EcEnv.env -> unienv -> ty -> Sp.t -> unit

val tfun_expected : unienv -> EcTypes.ty list -> EcTypes.ty

type sbody = ((EcIdent.t * ty) list * expr) Lazy.t

val select_op :
     ?filter:(operator -> bool) -> tvi -> EcEnv.env -> qsymbol -> unienv
  -> dom -> ((EcPath.path * ty list) * ty * unienv * sbody option) list
back to top