(* Copyright (c) - 2012-2014 - IMDEA Software Institute and INRIA
* Distributed under the terms of the CeCILL-B license *)
(* -------------------------------------------------------------------- *)
open EcUtils
open EcMaps
open EcSymbols
open EcLocation
open EcPath
open EcParsetree
open EcTypes
open EcDecl
open EcModules
module Sid = EcIdent.Sid
module Mid = EcIdent.Mid
module MSym = EcSymbols.Msym
(* -------------------------------------------------------------------- *)
type action = {
for_loading : exn -> exn;
}
(* -------------------------------------------------------------------- *)
exception HiScopeError of EcLocation.t option * string
let pp_hi_scope_error fmt exn =
match exn with
| HiScopeError (None, s) ->
Format.fprintf fmt "%s" s
| HiScopeError (Some loc, s) ->
Format.fprintf fmt "%s: %s" (EcLocation.tostring loc) s
| _ -> raise exn
let _ = EcPException.register pp_hi_scope_error
let hierror ?loc fmt =
let buf = Buffer.create 127 in
let bfmt = Format.formatter_of_buffer buf in
Format.kfprintf
(fun _ ->
Format.pp_print_flush bfmt ();
raise (HiScopeError (loc, Buffer.contents buf)))
bfmt fmt
(* -------------------------------------------------------------------- *)
module type IOptions = sig
type option
val register : action -> exn -> option
val register_identity : exn -> option
type options
val init : unit -> options
val get : options -> option -> exn
val set : options -> option -> exn -> options
val for_loading : options -> options
val for_subscope : options -> options
end
(* -------------------------------------------------------------------- *)
module Options : IOptions = struct
type option = int
type options = (action * exn) Mint.t
let known_options : options ref = ref Mint.empty
let identity = {
for_loading = (fun x -> x);
}
let count = ref 0
let initialized = ref false
let register action exn =
if !initialized then assert false;
let opt = !count in
incr count;
known_options := Mint.add opt (action,exn) !known_options;
opt
let register_identity = register identity
let init () =
initialized := true;
!known_options
let get options opt =
snd (Mint.find opt options)
let set options opt exn =
Mint.change
(function None -> assert false | Some(act,_) -> Some (act, exn))
opt options
let for_loading options =
Mint.map (fun (act, exn) -> act, act.for_loading exn) options
let for_subscope options = options
end
(* -------------------------------------------------------------------- *)
module Notifier = struct
exception Verbose of [`ForLoading | `Verbose of bool]
let for_loading = function
| Verbose _ -> Verbose `ForLoading
| exn -> exn
let default = Verbose (`Verbose true)
let mode = Options.register { for_loading } default
let verbose options =
match Options.get options mode with
| Verbose b -> b
| _ -> assert false
let set options b =
match Options.get options mode with
| Verbose (`ForLoading) -> options
| Verbose (`Verbose _) -> Options.set options mode (Verbose (`Verbose b))
| _ -> assert false
end
(* -------------------------------------------------------------------- *)
module Check_mode = struct
exception Full_check (* Disable: checkproof off, i.e. check everything *)
exception Check of bool (* true check proofs, false do not check *)
let for_loading = function
| Check _ -> Check false
| exn -> exn
let default = Check true
let mode = Options.register { for_loading } default
let check options =
match Options.get options mode with
| Check b -> b
| _ -> true
let check_proof options b =
match Options.get options mode with
| Check b' when b <> b' ->
Options.set options mode (Check b')
| _ -> options
let full_check options =
Options.set options mode Full_check
end
(* -------------------------------------------------------------------- *)
module Prover_info = struct
exception PI of EcProvers.prover_infos
let npi = Options.register_identity (PI EcProvers.dft_prover_infos)
let set options pi =
Options.set options npi (PI pi)
let get options =
match Options.get options npi with
| PI pi -> pi
| _ -> assert false
end
(* -------------------------------------------------------------------- *)
type proof_uc = {
puc_active : proof_auc option;
puc_cont : proof_ctxt list * (EcEnv.env option);
}
and proof_auc = {
puc_name : string;
puc_mode : bool option;
puc_jdg : proof_state;
puc_flags : pucflags;
puc_crt : EcDecl.axiom;
}
and proof_ctxt = (symbol * EcDecl.axiom) * EcPath.path * EcEnv.env
and proof_state = PSNoCheck | PSCheck of EcCoreGoal.proof
and pucflags = {
puc_nosmt : bool;
puc_local : bool;
}
(* -------------------------------------------------------------------- *)
type scope = {
sc_name : symbol;
sc_env : EcEnv.env;
sc_top : scope option;
sc_loaded : (EcEnv.ctheory_w3 * symbol list) Msym.t;
sc_required : symbol list;
sc_pr_uc : proof_uc option;
sc_options : Options.options;
sc_section : EcSection.t;
}
(* -------------------------------------------------------------------- *)
let empty =
let env = EcEnv.initial in
{ sc_name = EcPath.basename (EcEnv.root env);
sc_env = EcEnv.initial;
sc_top = None;
sc_loaded = Msym.empty;
sc_required = [];
sc_pr_uc = None;
sc_options = Options.init ();
sc_section = EcSection.initial;
}
(* -------------------------------------------------------------------- *)
let name (scope : scope) =
scope.sc_name
(* -------------------------------------------------------------------- *)
let path (scope : scope) =
EcEnv.root scope.sc_env
(* -------------------------------------------------------------------- *)
let env (scope : scope) =
scope.sc_env
(* -------------------------------------------------------------------- *)
let attop (scope : scope) =
scope.sc_top = None
(* -------------------------------------------------------------------- *)
let goal (scope : scope) =
scope.sc_pr_uc |> obind (fun x -> x.puc_active)
(* -------------------------------------------------------------------- *)
let xgoal (scope : scope) =
scope.sc_pr_uc
(* -------------------------------------------------------------------- *)
type topmode = [`InProof | `InActiveProof | `InTop]
let check_state (mode : topmode) action (scope : scope) =
match mode with
| `InProof when scope.sc_pr_uc = None ->
hierror "cannot process [%s] outside a proof script" action
| `InActiveProof when scope.sc_pr_uc = None ->
hierror "cannot process [%s] outside a proof script" action
| `InTop when scope.sc_pr_uc <> None ->
hierror "cannot process [%s] inside a proof script" action
| _ -> ()
(* -------------------------------------------------------------------- *)
let verbose (scope : scope) =
match Notifier.verbose scope.sc_options with
| `ForLoading -> false
| `Verbose b -> b
(* -------------------------------------------------------------------- *)
let set_verbose (scope : scope) (b : bool) =
{ scope with sc_options = Notifier.set scope.sc_options b }
(* -------------------------------------------------------------------- *)
let for_loading (scope : scope) =
{ empty with
sc_loaded = scope.sc_loaded;
sc_options = Options.for_loading scope.sc_options; }
(* -------------------------------------------------------------------- *)
let subscope (scope : scope) (name : symbol) =
let env = EcEnv.Theory.enter name scope.sc_env in
{ sc_name = name;
sc_env = env;
sc_top = Some scope;
sc_loaded = scope.sc_loaded;
sc_required = scope.sc_required;
sc_pr_uc = None;
sc_options = Options.for_subscope scope.sc_options;
sc_section = scope.sc_section;
}
(* -------------------------------------------------------------------- *)
let maybe_add_to_section scope item =
match EcSection.opath scope.sc_section with
| None -> scope
| Some (_, sp) -> begin
match EcPath.p_equal sp (EcEnv.root scope.sc_env) with
| false -> scope
| true ->
let ec = EcSection.add_item item scope.sc_section in
{ scope with sc_section = ec }
end
(* -------------------------------------------------------------------- *)
module Prover = struct
exception Unknown_prover of string
let pp_error fmt exn =
match exn with
| Unknown_prover s ->
Format.fprintf fmt "Unknown prover %s" s
| _ -> raise exn
let _ = EcPException.register pp_error
let check_prover_name { pl_desc = name; pl_loc = loc } =
if not (EcProvers.is_prover_known name) then
EcLocation.locate_error loc (Unknown_prover name);
name
let set_wrapper scope wrapper =
let pi = Prover_info.get scope.sc_options in
let pi = { pi with EcProvers.pr_wrapper = wrapper } in
{ scope with sc_options = Prover_info.set scope.sc_options pi; }
let mk_prover_info scope maxprocs time ns =
let dft = Prover_info.get scope.sc_options in
let time = max 0 (odfl dft.EcProvers.pr_timelimit time) in
let provers = odfl dft.EcProvers.pr_provers ns in
let maxprocs = odfl dft.EcProvers.pr_maxprocs maxprocs in
{ EcProvers.pr_maxprocs = maxprocs;
EcProvers.pr_provers = provers;
EcProvers.pr_timelimit = time;
EcProvers.pr_wrapper = dft.EcProvers.pr_wrapper; }
let set_prover_info scope max time ns =
let pi = mk_prover_info scope max time ns in
{ scope with sc_options = Prover_info.set scope.sc_options pi }
let set_all scope =
let provers = EcProvers.known_provers () in
set_prover_info scope None None (Some provers)
let set_default scope ~timeout ~nprovers provers =
let provers =
match provers with
| None ->
let provers = EcProvers.dft_prover_names in
List.filter EcProvers.is_prover_known provers
| Some provers ->
List.iter
(fun name ->
if not (EcProvers.is_prover_known name) then
raise (Unknown_prover name)) provers;
provers
in
set_prover_info scope (Some nprovers) (Some timeout) (Some provers)
let process scope pi =
let max = pi.pprov_max in
let time = pi.pprov_time in
let ns = pi.pprov_names in
let ns = ns |> omap (List.map check_prover_name) in
set_prover_info scope max time ns
let mk_prover_info scope pi =
let max = pi.pprov_max in
let time = pi.pprov_time in
let ns = pi.pprov_names in
let ns = ns |> omap (List.map check_prover_name) in
mk_prover_info scope max time ns
let full_check scope =
{ scope with sc_options = Check_mode.full_check scope.sc_options }
let check_proof scope b =
{ scope with sc_options = Check_mode.check_proof scope.sc_options b }
end
(* -------------------------------------------------------------------- *)
module Tactics = struct
let pi scope pi = Prover.mk_prover_info scope pi
let proof (scope : scope) mode (strict : bool) =
check_state `InActiveProof "proof script" scope;
match (oget scope.sc_pr_uc).puc_active with
| None -> hierror "no active lemmas"
| Some pac ->
let pac =
match pac.puc_mode with
| None when not strict && mode = `WeakCheck -> begin
match pac.puc_jdg with
| PSNoCheck -> { pac with puc_mode = Some false; }
| PSCheck _ ->
let pac = { pac with puc_jdg = PSNoCheck } in
{ pac with puc_mode = Some false; }
end
| None -> { pac with puc_mode = Some strict }
| Some _ -> hierror "[proof] can only be used at beginning of a proof script"
in
{ scope with sc_pr_uc = Some { (oget scope.sc_pr_uc) with puc_active = Some pac; } }
let process_r mark mode (scope : scope) (tac : ptactic list) =
check_state `InProof "proof script" scope;
let scope =
match (oget scope.sc_pr_uc).puc_active with
| None -> hierror "no active lemma"
| Some pac ->
if mark && pac.puc_mode = None
then proof scope mode true
else scope
in
let puc = oget (scope.sc_pr_uc) in
let pac = oget (puc).puc_active in
match pac.puc_jdg with
| PSNoCheck -> scope
| PSCheck juc ->
let module TTC = EcHiTacticals in
let htmode =
match pac.puc_mode, mode with
| Some true , `WeakCheck -> `Admit
| _ , `WeakCheck -> hierror "cannot weak-check a non-strict proof script"
| Some true , `Check -> `Strict
| Some false, `Check -> `Standard
| _ , `Check -> `Strict
in
let ttenv = { EcHiGoal.tt_provers = pi scope; EcHiGoal.tt_smtmode = htmode; } in
let juc = TTC.process ttenv tac juc in
let pac = { pac with puc_jdg = PSCheck juc } in
{ scope with sc_pr_uc = Some { puc with puc_active = Some pac; } }
let process_core mark mode (scope : scope) (ts : ptactic_core list) =
let ts = List.map (fun t -> { pt_core = t; pt_intros = []; }) ts in
process_r mark mode scope ts
let process scope mode tac =
process_r true mode scope tac
end
(* -------------------------------------------------------------------- *)
module Ax = struct
open EcParsetree
open EcDecl
module TT = EcTyping
type mode = [`WeakCheck | `Check]
(* ------------------------------------------------------------------ *)
let bind (scope : scope) local ((x, ax) : _ * axiom) =
assert (scope.sc_pr_uc = None);
let scope = { scope with sc_env = EcEnv.Ax.bind x ax scope.sc_env; } in
let scope = maybe_add_to_section scope (EcTheory.CTh_axiom (x, ax)) in
let scope =
match EcSection.opath scope.sc_section with
| None -> scope
| Some _ ->
let lvl1 = if local then `Local else `Global in
let lvl2 = if ax.ax_kind = `Axiom then `Axiom else `Lemma in
if lvl2 = `Axiom && ax.ax_tparams <> [] then
hierror "axiom must be monomorphic in sections";
let axpath = EcPath.pqname (path scope) x in
let ec = EcSection.add_lemma axpath (lvl1, lvl2) scope.sc_section in
{ scope with sc_section = ec }
in
scope
(* ------------------------------------------------------------------ *)
let start_lemma scope (cont, axflags) check name axd =
let puc =
match check with
| false -> PSNoCheck
| true ->
let hyps = EcEnv.LDecl.init scope.sc_env axd.ax_tparams in
let proof = EcCoreGoal.start hyps (oget axd.ax_spec) in
PSCheck proof
in
let puc =
{ puc_active = Some {
puc_name = name;
puc_mode = None;
puc_jdg = puc;
puc_flags = axflags;
puc_crt = axd; };
puc_cont = cont; }
in
{ scope with sc_pr_uc = Some puc }
(* ------------------------------------------------------------------ *)
let rec add_r (scope : scope) mode (ax : paxiom located) =
assert (scope.sc_pr_uc = None);
let loc = ax.pl_loc and ax = ax.pl_desc in
let ue = TT.transtyvars scope.sc_env (loc, ax.pa_tyvars) in
if ax.pa_local && not (EcSection.in_section scope.sc_section) then
hierror "cannot declare a local lemma outside of a section";
let (pconcl, tintro) =
match ax.pa_vars with
| None -> (ax.pa_formula, [])
| Some vs ->
let pconcl = { pl_loc = loc; pl_desc = PFforall (vs, ax.pa_formula) } in
(pconcl, List.flatten (List.map fst vs))
in
let tintro =
List.map
(fun x -> IPCore (mk_loc x.pl_loc (`NoRename x.pl_desc)))
tintro in
let tintro = mk_loc loc (Plogic (Pintro tintro)) in
let concl = TT.trans_prop scope.sc_env ue pconcl in
if not (EcUnify.UniEnv.closed ue) then
hierror "the formula contains free type variables";
let concl = EcFol.Fsubst.uni (EcUnify.UniEnv.close ue) concl in
let tparams = EcUnify.UniEnv.tparams ue in
let axd =
let kind = match ax.pa_kind with PAxiom _ -> `Axiom | _ -> `Lemma in
{ ax_tparams = tparams;
ax_spec = Some concl;
ax_kind = kind;
ax_nosmt = ax.pa_nosmt; }
in
let check = Check_mode.check scope.sc_options in
let pucflags = { puc_nosmt = ax.pa_nosmt; puc_local = ax.pa_local; } in
let pucflags = (([], None), pucflags) in
if not ax.pa_local then begin
match EcSection.olocals scope.sc_section with
| None -> ()
| Some locals ->
if EcSection.form_use_local concl locals then
hierror "this lemma uses local modules and must be declared as local"
end;
if ax.pa_local && ax.pa_kind = (PAxiom `Axiom) then
hierror "an axiom cannot be local";
match ax.pa_kind with
| PILemma ->
let scope = start_lemma scope pucflags check (unloc ax.pa_name) axd in
let scope = Tactics.process_core false `Check scope [tintro] in
None, scope
| PLemma tc ->
let scope = start_lemma scope pucflags check (unloc ax.pa_name) axd in
let scope = Tactics.process_core false `Check scope [tintro] in
let scope = Tactics.proof scope mode (if tc = None then true else false) in
let tc =
match tc with
| Some tc -> tc
| None ->
let dtc = Plogic (Psmt (None, empty_pprover)) in
let dtc = { pl_loc = loc; pl_desc = dtc } in
let dtc = { pt_core = dtc; pt_intros = []; } in
dtc
in
let tc = { pl_loc = loc; pl_desc = Pby (Some [tc]) } in
let tc = { pt_core = tc; pt_intros = []; } in
let scope = Tactics.process_r false mode scope [tc] in
save scope loc
| PAxiom _ ->
Some (unloc ax.pa_name),
bind scope (snd pucflags).puc_local (unloc ax.pa_name, axd)
(* ------------------------------------------------------------------ *)
and add_for_cloning (scope : scope) proofs =
match proofs with
| [] -> scope
| _ ->
assert (scope.sc_pr_uc = None);
let puc = { puc_active = None; puc_cont = (proofs, Some scope.sc_env); } in
{ scope with sc_pr_uc = Some puc; }
(* ------------------------------------------------------------------ *)
and save scope _loc =
check_state `InProof "save" scope;
let puc = oget scope.sc_pr_uc in
let pac =
match puc.puc_active with
| None -> hierror "no active lemma"
| Some pac -> begin
match pac.puc_jdg with
| PSNoCheck -> ()
| PSCheck pf -> begin
if not (EcCoreGoal.closed pf) then
hierror "cannot save an incomplete proof"
end
end; pac
in
let scope = { scope with sc_pr_uc = Some { puc with puc_active = None; } } in
let scope =
match fst puc.puc_cont with
| [] -> { scope with sc_pr_uc = None; }
| _ -> scope
in
let scope =
match snd puc.puc_cont with
| Some e -> { scope with sc_env = e }
| None -> bind scope pac.puc_flags.puc_local (pac.puc_name, pac.puc_crt)
in
(Some pac.puc_name, scope)
(* ------------------------------------------------------------------ *)
let add (scope : scope) mode (ax : paxiom located) =
add_r scope mode ax
(* ------------------------------------------------------------------ *)
let activate (scope : scope) (qn : pqsymbol) =
check_state `InProof "activate" scope;
let qn = EcPath.fromqsymbol (unloc qn) in
let puc = oget scope.sc_pr_uc in
let _ =
match puc.puc_active with
| Some _ -> hierror "a lemma is already active"
| None -> ()
in
let (((x, ax), _, axenv), proofs) =
let rec doit past proofs =
match proofs with
| [] -> hierror "no such lemma: `%s'" (EcPath.tostring qn)
| (((_, _), p, _) as st) :: proofs ->
match EcPath.p_equal p qn with
| false -> doit (st :: past) proofs
| true -> (st, List.rev_append past proofs)
in
doit [] (fst puc.puc_cont)
in
let pucflags = { puc_nosmt = ax.ax_nosmt; puc_local = false; } in
let pucflags = ((proofs, snd puc.puc_cont), pucflags) in
let check = Check_mode.check scope.sc_options in
let scope = { scope with sc_env = axenv } in
let scope = start_lemma scope pucflags check x ax in
scope
end
(* -------------------------------------------------------------------- *)
module Op = struct
open EcTypes
open EcDecl
module TT = EcTyping
let bind (scope : scope) ((x, op) : _ * operator) =
assert (scope.sc_pr_uc = None);
let scope = { scope with sc_env = EcEnv.Op.bind x op scope.sc_env } in
let scope = maybe_add_to_section scope (EcTheory.CTh_operator (x, op)) in
scope
let add (scope : scope) (op : poperator located) =
assert (scope.sc_pr_uc = None);
let op = op.pl_desc and loc = op.pl_loc in
let ue = TT.transtyvars scope.sc_env (loc, op.po_tyvars) in
let tp = TT.tp_relax in
let (ty, body) =
match op.po_def with
| PO_abstr pty ->
(TT.transty tp scope.sc_env ue pty, `Abstract)
| PO_concr (bd, pty, pe) ->
let env = scope.sc_env in
let codom = TT.transty tp env ue pty in
let env, xs = TT.transbinding env ue bd in
let body = TT.transexpcast env `InOp ue codom pe in
let lam = EcTypes.e_lam xs body in
(lam.EcTypes.e_ty, `Plain lam)
| PO_case (bd, pty, pbs) ->
(* FIXME: move this to a dedicated module *)
let env = scope.sc_env in
let codom = TT.transty tp env ue pty in
let env, args = TT.transbinding env ue bd in
let ty = EcTypes.toarrow (List.map snd args) codom in
let opname = EcIdent.create (unloc op.po_name) in
let env = EcEnv.Var.bind_local opname ty env in
let mpty, pbsmap =
let pbsmap =
List.map (fun x ->
let nms = (fun pop -> (unloc pop.pop_name, pop)) in
let nms = List.map nms x.pop_patterns in
(x.pop_body, Msym.of_list nms))
pbs
in
match List.map snd pbsmap with
| [] -> hierror ~loc "this pattern matching has no branches"
| nm :: nms ->
if not (List.for_all (Msym.set_equal nm) nms) then
hierror ~loc "this pattern matching matches on different parameters";
let argsmap =
List.fold_lefti
(fun i m (x, xty) -> Msym.add (EcIdent.name x) (i, x, xty) m)
Msym.empty args
in
let _, mpty =
Msym.fold_left
(fun (seen, mpty) px _ ->
if Msym.mem px seen then
hierror ~loc "this pattern matching matches a parameter twice";
match Msym.find_opt px argsmap with
| None ->
hierror ~loc "this pattern matching matches an unbound parameter";
| Some (i, x, xty) -> (Ssym.add px seen, (i, x, xty) :: mpty))
(Ssym.empty, []) nm
in
(mpty, pbsmap)
in
let branches =
let pbs =
let trans_b ((body, pbmap) : _ * pop_pattern Msym.t) =
let trans1 ((_, x, xty) : _ * EcIdent.t * ty) =
let pb = oget (Msym.find_opt (EcIdent.name x) pbmap) in
let filter = fun op -> EcDecl.is_ctor op in
let cname = fst pb.pop_pattern in
let tvi = pb.pop_tvi |> omap (TT.transtvi env ue) in
let cts = EcUnify.select_op ~filter tvi env (unloc cname) ue [] in
match cts with
| [] -> hierror ~loc:cname.pl_loc "unknown constructor name"
| _ :: _ :: _ -> hierror ~loc:cname.pl_loc "ambiguous constructor name"
| [(cp, tvi), opty, subue] ->
let ctor = oget (EcEnv.Op.by_path_opt cp env) in
let (indp, ctoridx) = EcDecl.operator_as_ctor ctor in
let indty = oget (EcEnv.Ty.by_path_opt indp env) in
let ind = (EcDecl.tydecl_as_datatype indty).tydt_ctors in
let ctorsym, ctorty = List.nth ind ctoridx in
let args_exp = List.length ctorty in
let args_got = List.length (snd pb.pop_pattern) in
if args_exp <> args_got then
hierror ~loc:cname.pl_loc
"this constructor takes %d argument(s), got %d" args_exp args_got;
if not (List.uniq (List.map unloc (snd pb.pop_pattern))) then
hierror ~loc:cname.pl_loc "this pattern is non-linear";
EcUnify.UniEnv.restore ~src:subue ~dst:ue;
let ctorty =
let tvi = Some (EcUnify.TVIunamed tvi) in
fst (EcUnify.UniEnv.opentys ue indty.tyd_params tvi ctorty) in
let pty = EcUnify.UniEnv.fresh ue in
(try EcUnify.unify env ue (toarrow ctorty pty) opty
with EcUnify.UnificationFailure _ -> assert false);
TT.unify_or_fail env ue pb.pop_name.pl_loc pty xty;
let pvars = List.map (EcIdent.create |- unloc) (snd pb.pop_pattern) in
let pvars = List.combine pvars ctorty in
(pb, (indp, ind, (ctorsym, ctoridx)), pvars)
in
let ptns = List.map trans1 mpty in
let env =
List.fold_left (fun env (_, _, pvars) ->
EcEnv.Var.bind_locals pvars env)
env ptns
in
(ptns, TT.transexpcast env `InOp ue codom body)
in
List.map trans_b pbsmap
in
let module CaseMap : sig
type t
type locals = (EcIdent.t * ty) list
val create : EcPath.path list list -> t
val add : (int * locals) list -> expr -> t -> bool
val resolve : t -> opbranches option
end = struct
type locals = (EcIdent.t * ty) list
type t = [
| `Case of (EcPath.path * t) array
| `Leaf of (locals list * expr) option ref
]
let rec create (inds : path list list) =
match inds with
| [] -> `Leaf (ref None)
| ind :: inds ->
let ind = Array.of_list ind in
`Case (Array.map (fun x -> (x, create inds)) ind)
let add bs e (m : t) =
let r =
List.fold_left
(fun m (i, _) ->
match m with
| `Leaf _ -> assert false
| `Case t ->
assert (i >= 0 && i < Array.length t);
snd t.(i))
m bs
in
match r with
| `Case _ -> assert false
| `Leaf r -> begin
match !r with
| None -> r := Some (List.map snd bs, e); true
| Some _ -> false
end
let resolve =
let module E = struct exception NotFull end in
let rec resolve_r m =
match m with
| `Case t ->
let for1 i =
let (cp, bs) = snd_map resolve_r t.(i) in
{ opb_ctor = (cp, i); opb_sub = bs; }
in
OPB_Branch (Parray.init (Array.length t) for1)
| `Leaf r -> begin
match !r with
| None -> raise E.NotFull
| Some (x1, x2) -> OPB_Leaf (x1, x2)
end
in
fun m ->
try Some (resolve_r m)
with E.NotFull -> None
end in
let inds = (fun (_, (indp, ind, _), _) -> (indp, ind)) in
let inds = List.map inds (fst (oget (List.ohead pbs))) in
let inds =
List.map (fun (indp, ctors) ->
List.map
(fun (ctor, _) -> EcPath.pqoname (EcPath.prefix indp) ctor)
ctors)
inds
in
let casemap = CaseMap.create inds in
List.iter
(fun (ptns, be) ->
let ptns = List.map (fun (_, (_, _, (_, ctor)), pvars) ->
(ctor, pvars)) ptns
in
if not (CaseMap.add ptns be casemap) then
hierror ~loc "this pattern matching contains duplicated branch")
pbs;
match CaseMap.resolve casemap with
| None -> hierror ~loc "this pattern matching is non-exhaustive"
| Some x -> x
in
(ty, (`Fix ((opname, codom), (args, List.map proj3_1 mpty), branches)))
in
if not (EcUnify.UniEnv.closed ue) then
hierror ~loc "this operator type contains free type variables";
let uni = Tuni.offun (EcUnify.UniEnv.close ue) in
let ty = uni ty in
let tparams = EcUnify.UniEnv.tparams ue in
let body =
match body with
| `Abstract -> None
| `Plain e -> Some (OP_Plain (e_mapty uni e))
| `Fix ((opname, codom), (args, istruct), branches) ->
let codom = uni codom in
let opexpr = EcPath.pqname (path scope) (unloc op.po_name) in
let opexpr = e_op opexpr (List.map (tvar |- fst) tparams) codom in
let ebsubst = { e_subst_id with es_freshen = false; es_ty = uni; } in
let ebsubst = { ebsubst with es_loc = Mid.add opname opexpr ebsubst.es_loc; } in
let args = List.map (fun (x, xty) -> (x, uni xty)) args in
let branches =
let rec uni_branches = function
| OPB_Leaf (locals, e) ->
OPB_Leaf (List.map (List.map (snd_map uni)) locals,
e_subst ebsubst e)
| OPB_Branch bs ->
let for1 b =
{ opb_ctor = b.opb_ctor;
opb_sub = uni_branches b.opb_sub; }
in
OPB_Branch (Parray.map for1 bs)
in
uni_branches branches
in
Some (OP_Fix { opf_args = args;
opf_resty = codom;
opf_struct = (istruct, List.length args);
opf_branches = branches; })
in
let tyop = EcDecl.mk_op tparams ty body in
if op.po_nosmt && (is_none op.po_ax) then
hierror ~loc "[nosmt] is only supported for axiomatized operators";
if op.po_kind = `Const then begin
let tue = EcUnify.UniEnv.copy ue in
let ty, _ = EcUnify.UniEnv.openty tue tparams None ty in
let tdom = EcUnify.UniEnv.fresh tue in
let tcom = EcUnify.UniEnv.fresh tue in
let tfun = EcTypes.tfun tdom tcom in
try
EcUnify.unify (env scope) tue ty tfun;
let msg = "this operator type is (unifiable) to a function type" in
hierror ~loc "%s" msg
with EcUnify.UnificationFailure _ -> ()
end;
match op.po_ax with
| None -> bind scope (unloc op.po_name, tyop)
| Some ax -> begin
match tyop.op_kind with
| OB_oper (Some (OP_Plain bd)) ->
let axbd = EcFol.form_of_expr EcFol.mhr bd in
let axbd, axpm =
let bdpm = List.map fst tyop.op_tparams in
let axpm = List.map EcIdent.fresh bdpm in
(EcFol.Fsubst.subst_tvar
(EcTypes.Tvar.init bdpm (List.map tvar axpm))
axbd,
List.combine axpm (List.map snd tyop.op_tparams))
in
let axspec =
EcFol.f_eq
(EcFol.f_op
(EcPath.pqname (path scope) (unloc op.po_name))
(List.map (tvar |- fst) axpm)
axbd.EcFol.f_ty)
axbd
in
let tyop = { tyop with op_kind = OB_oper None } in
let axop = { ax_tparams = axpm;
ax_spec = Some axspec;
ax_kind = `Axiom;
ax_nosmt = op.po_nosmt; } in
let scope = bind scope (unloc op.po_name, tyop) in
Ax.bind scope false (unloc ax, axop)
| _ -> hierror ~loc "cannot axiomatized non-plain operators"
end
end
(* -------------------------------------------------------------------- *)
module Pred = struct
module TT = EcTyping
let add (scope : scope) (op : ppredicate located) =
assert (scope.sc_pr_uc = None);
let op = op.pl_desc and loc = op.pl_loc in
let ue = TT.transtyvars scope.sc_env (loc, op.pp_tyvars) in
let tp = TT.tp_relax in
let dom, body =
match op.pp_def with
| PPabstr ptys ->
List.map (TT.transty tp scope.sc_env ue) ptys, None
| PPconcr(bd,pe) ->
let env, xs = TT.transbinding scope.sc_env ue bd in
let body = TT.trans_prop env ue pe in
let dom = List.map snd xs in
let xs = List.map (fun (x,ty) -> x, EcFol.GTty ty) xs in
let lam = EcFol.f_lambda xs body in
(dom, Some lam)
in
if not (EcUnify.UniEnv.closed ue) then
hierror "this predicate type contains free type variables";
let uni = EcUnify.UniEnv.close ue in
let body = body |> omap (EcFol.Fsubst.uni uni) in
let dom = List.map (Tuni.offun uni) dom in
let tparams = EcUnify.UniEnv.tparams ue in
let tyop = EcDecl.mk_pred tparams dom body in
Op.bind scope (unloc op.pp_name, tyop)
end
(* -------------------------------------------------------------------- *)
module Mod = struct
module TT = EcTyping
let bind (scope : scope) (local : bool) (m : module_expr) =
assert (scope.sc_pr_uc = None);
let scope =
{ scope with
sc_env = EcEnv.Mod.bind m.me_name m scope.sc_env; }
in
let scope = maybe_add_to_section scope (EcTheory.CTh_module m) in
let scope =
match local with
| false -> scope
| true ->
let mpath = EcPath.pqname (path scope) m.me_name in
let env =
match m.me_body with
| ME_Alias _ | ME_Decl _ -> scope.sc_env
| ME_Structure _ ->
let env = scope.sc_env in
(* We keep only the internal part, i.e the inner global variables *)
(* TODO : using mod_use here to compute the set of inner global
variables is inefficient, change this algo *)
let mp = EcPath.mpath_crt mpath [] None in
let use = EcEnv.NormMp.mod_use env mp in
let rx =
let add x _ rx =
if EcPath.m_equal (EcPath.m_functor x.EcPath.x_top) mp then
Sx.add x rx
else rx in
Mx.fold add use.EcEnv.us_pv EcPath.Sx.empty in
EcEnv.Mod.add_restr_to_locals (rx,EcPath.Sm.empty) env in
let ec = EcSection.add_local_mod mpath scope.sc_section in
{ scope with sc_section = ec; sc_env = env }
in
scope
let add (scope : scope) (ptm : pmodule_def) =
assert (scope.sc_pr_uc = None);
if ptm.ptm_local && not (EcSection.in_section scope.sc_section) then
hierror "cannot declare a local module outside of a section";
let { ptm_name = name; ptm_body = m; } = ptm in
let m = TT.transmod scope.sc_env ~attop:true (unloc name) m in
if not ptm.ptm_local then begin
match EcSection.olocals scope.sc_section with
| None -> ()
| Some locals ->
if EcSection.module_use_local_or_abs m locals then
hierror "this module use local/abstracts modules and must be declared as local";
end;
bind scope ptm.ptm_local m
let declare (scope : scope) m =
if not (EcSection.in_section scope.sc_section) then
hierror "cannot declare an abstract module outside of a section";
let modty = m.ptmd_modty in
let tysig = fst (TT.transmodtype scope.sc_env (fst modty)) in
let restr = List.map (TT.trans_topmsymbol scope.sc_env) (snd modty) in
let name = EcIdent.create (unloc m.ptmd_name) in
let scope =
let restr = Sx.empty, Sm.of_list restr in
{ scope with
sc_env = EcEnv.Mod.declare_local
name tysig restr scope.sc_env;
sc_section = EcSection.add_abstract
name (tysig, restr) scope.sc_section }
in
scope
end
(* -------------------------------------------------------------------- *)
module ModType = struct
let bind (scope : scope) ((x, tysig) : _ * module_sig) =
assert (scope.sc_pr_uc = None);
let scope =
{ scope with
sc_env = EcEnv.ModTy.bind x tysig scope.sc_env; }
in
let scope = maybe_add_to_section scope (EcTheory.CTh_modtype (x, tysig)) in
scope
let add (scope : scope) (name : symbol) (i : pmodule_sig) =
assert (scope.sc_pr_uc = None);
let tysig = EcTyping.transmodsig scope.sc_env name i in
bind scope (name, tysig)
end
(* -------------------------------------------------------------------- *)
module Ty = struct
open EcDecl
open EcTyping
module TT = EcTyping
type tydname = (ptyparams * psymbol) located
(* ------------------------------------------------------------------ *)
let check_name_available scope x =
let pname = EcPath.pqname (EcEnv.root (env scope)) x.pl_desc in
if EcEnv.Ty .by_path_opt pname (env scope) <> None
|| EcEnv.TypeClass.by_path_opt pname (env scope) <> None then
hierror ~loc:x.pl_loc "duplicated type/type-class name `%s'" x.pl_desc
(* ------------------------------------------------------------------ *)
let bind (scope : scope) ((x, tydecl) : (_ * tydecl)) =
assert (scope.sc_pr_uc = None);
let scope = { scope with sc_env = EcEnv.Ty.bind x tydecl scope.sc_env; } in
let scope = maybe_add_to_section scope (EcTheory.CTh_type (x, tydecl)) in
scope
(* ------------------------------------------------------------------ *)
let add (scope : scope) info tcs =
assert (scope.sc_pr_uc = None);
let (args, name) = info.pl_desc and loc = info.pl_loc in
let tcs =
List.map
(fun tc -> fst (EcEnv.TypeClass.lookup (unloc tc) scope.sc_env))
tcs
in
let ue = TT.transtyvars scope.sc_env (loc, Some args) in
let tydecl = {
tyd_params = EcUnify.UniEnv.tparams ue;
tyd_type = `Abstract (Sp.of_list tcs);
} in
bind scope (unloc name, tydecl)
(* ------------------------------------------------------------------ *)
let define (scope : scope) info body =
assert (scope.sc_pr_uc = None);
let (args, name) = info.pl_desc and loc = info.pl_loc in
let ue = TT.transtyvars scope.sc_env (loc, Some args) in
let body = transty tp_tydecl scope.sc_env ue body in
let tydecl = {
tyd_params = EcUnify.UniEnv.tparams ue;
tyd_type = `Concrete body;
} in
bind scope (unloc name, tydecl)
(* ------------------------------------------------------------------ *)
let bindclass (scope : scope) (x, tc) =
assert (scope.sc_pr_uc = None);
let scope = { scope with sc_env = EcEnv.TypeClass.bind x tc scope.sc_env; } in
let scope = maybe_add_to_section scope (EcTheory.CTh_typeclass (x, tc)) in
scope
(* ------------------------------------------------------------------ *)
let add_class (scope : scope) { pl_desc = tcd } =
assert (scope.sc_pr_uc = None);
let name = unloc tcd.ptc_name in
let scenv = (env scope) in
check_name_available scope tcd.ptc_name;
let tclass =
let uptc =
tcd.ptc_inth |> omap
(fun { pl_loc = uploc; pl_desc = uptc } ->
match EcEnv.TypeClass.lookup_opt uptc scenv with
| None -> hierror ~loc:uploc "unknown type-class: `%s'"
(string_of_qsymbol uptc)
| Some (tcp, _) -> tcp)
in
let asty =
let body = ofold (fun p tc -> Sp.add p tc) Sp.empty uptc in
{ tyd_params = []; tyd_type = `Abstract body; } in
let scenv = EcEnv.Ty.bind name asty scenv in
(* Check for duplicated field names *)
Msym.odup unloc (List.map fst tcd.ptc_ops)
|> oiter (fun (x, y) -> hierror ~loc:y.pl_loc
"duplicated operator name: `%s'" x.pl_desc);
Msym.odup unloc (List.map fst tcd.ptc_axs)
|> oiter (fun (x, y) -> hierror ~loc:y.pl_loc
"duplicated axiom name: `%s'" x.pl_desc);
(* Check operators types *)
let operators =
let check1 (x, ty) =
let ue = EcUnify.UniEnv.create (Some []) in
let ty = transty tp_tydecl scenv ue ty in
let ty = Tuni.offun (EcUnify.UniEnv.close ue) ty in
(EcIdent.create (unloc x), ty)
in
tcd.ptc_ops |> List.map check1 in
(* Check axioms *)
let axioms =
let scenv = EcEnv.Var.bind_locals operators scenv in
let check1 (x, ax) =
let ue = EcUnify.UniEnv.create (Some []) in
let ax = trans_prop scenv ue ax in
let ax = EcFol.Fsubst.uni (EcUnify.UniEnv.close ue) ax in
(unloc x, ax)
in
tcd.ptc_axs |> List.map check1 in
(* Construct actual type-class *)
{ tc_prt = uptc; tc_ops = operators; tc_axs = axioms; }
in
bindclass scope (name, tclass)
(* ------------------------------------------------------------------ *)
let check_tci_operators env tcty ops reqs =
let ue = EcUnify.UniEnv.create (Some (fst tcty)) in
let rmap = Mstr.of_list reqs in
let ops =
let tt1 m (x, (tvi, op)) =
if not (Mstr.mem (unloc x) rmap) then
hierror ~loc:x.pl_loc "invalid operator name: `%s'" (unloc x);
let tvi = List.map (TT.transty tp_tydecl env ue) tvi in
let selected =
EcUnify.select_op ~filter:EcDecl.is_oper
(Some (EcUnify.TVIunamed tvi)) env (unloc op) ue []
in
let op =
match selected with
| [] -> hierror ~loc:op.pl_loc "unknown operator"
| op1::op2::_ ->
hierror ~loc:op.pl_loc
"ambiguous operator (%s / %s)"
(EcPath.tostring (fst (proj3_1 op1)))
(EcPath.tostring (fst (proj3_1 op2)))
| [((p, _), _, _)] ->
let op = EcEnv.Op.by_path p env in
let opty =
Tvar.subst
(Tvar.init (List.map fst op.op_tparams) tvi)
op.op_ty
in
(p, opty)
in
Mstr.change
(function
| None -> Some (x.pl_loc, op)
| Some _ -> hierror ~loc:(x.pl_loc)
"duplicated operator name: `%s'" (unloc x))
(unloc x) m
in
List.fold_left tt1 Mstr.empty ops
in
List.iter
(fun (x, (req, _)) ->
if req && not (Mstr.mem x ops) then
hierror "no definition for operator `%s'" x)
reqs;
List.fold_left
(fun m (x, (_, ty)) ->
match Mstr.find_opt x ops with
| None -> m
| Some (loc, (p, opty)) ->
if not (EcReduction.EqTest.for_type env ty opty) then
hierror ~loc "invalid type for operator `%s'" x;
Mstr.add x p m)
Mstr.empty reqs
(* ------------------------------------------------------------------ *)
let check_tci_axioms scope mode axs reqs =
let rmap = Mstr.of_list reqs in
let symbs, axs =
List.map_fold
(fun m (x, t) ->
if not (Mstr.mem (unloc x) rmap) then
hierror ~loc:x.pl_loc "invalid axiom name: `%s'" (unloc x);
if Sstr.mem (unloc x) m then
hierror ~loc:(x.pl_loc) "duplicated axiom name: `%s'" (unloc x);
(Sstr.add (unloc x) m, (unloc x, t, Mstr.find (unloc x) rmap)))
Sstr.empty axs
in
List.iter
(fun (x, _) ->
if not (Mstr.mem x symbs) then
hierror "no proof for axiom `%s'" x)
reqs;
List.iter
(fun (x, pt, f) ->
let x = "$" ^ x in
let t = { pt_core = pt; pt_intros = []; } in
let t = { pl_loc = pt.pl_loc; pl_desc = Pby (Some [t]) } in
let t = { pt_core = t; pt_intros = []; } in
let ax = { ax_tparams = [];
ax_spec = Some f;
ax_kind = `Axiom;
ax_nosmt = true; } in
let pucflags = { puc_nosmt = false; puc_local = false; } in
let pucflags = (([], None), pucflags) in
let check = Check_mode.check scope.sc_options in
let escope = scope in
let escope = Ax.start_lemma escope pucflags check x ax in
let escope = Tactics.proof escope mode true in
let escope = Tactics.process_r false mode escope [t] in
ignore (Ax.save escope pt.pl_loc))
axs
(* ------------------------------------------------------------------ *)
let p_zmod = EcPath.fromqsymbol ([EcCoreLib.id_top; "Ring"; "ZModule"], "zmodule")
let p_ring = EcPath.fromqsymbol ([EcCoreLib.id_top; "Ring"; "ComRing"], "ring" )
let p_idomain = EcPath.fromqsymbol ([EcCoreLib.id_top; "Ring"; "IDomain"], "idomain")
let p_field = EcPath.fromqsymbol ([EcCoreLib.id_top; "Ring"; "Field" ], "field" )
(* ------------------------------------------------------------------ *)
let ring_of_symmap env ty boolean symbols =
{ r_type = ty;
r_zero = oget (Mstr.find_opt "rzero" symbols);
r_one = oget (Mstr.find_opt "rone" symbols);
r_add = oget (Mstr.find_opt "add" symbols);
r_opp = (Mstr.find_opt "opp" symbols);
r_mul = oget (Mstr.find_opt "mul" symbols);
r_exp = (Mstr.find_opt "expr" symbols);
r_sub = (Mstr.find_opt "sub" symbols);
r_embed =
begin match Mstr.find_opt "ofint" symbols with
| None ->
if EcReduction.EqTest.for_type env ty tint then `Direct
else `Default
| Some p -> `Embed p
end;
r_bool = boolean;
}
let addring (scope : scope) mode (boolean, { pl_desc = tci; pl_loc = loc }) =
if not (EcAlgTactic.is_module_loaded scope.sc_env) then
hierror "load AlgTactic/Ring first";
let ty =
let ue = TT.transtyvars scope.sc_env (loc, Some (fst tci.pti_type)) in
let ty = transty tp_tydecl scope.sc_env ue (snd tci.pti_type) in
assert (EcUnify.UniEnv.closed ue);
(EcUnify.UniEnv.tparams ue, Tuni.offun (EcUnify.UniEnv.close ue) ty)
in
let symbols = EcAlgTactic.ring_symbols scope.sc_env boolean (snd ty) in
let symbols = check_tci_operators scope.sc_env ty tci.pti_ops symbols in
let cr = ring_of_symmap scope.sc_env (snd ty) boolean symbols in
let axioms = EcAlgTactic.ring_axioms scope.sc_env cr in
check_tci_axioms scope mode tci.pti_axs axioms;
{ scope with sc_env =
List.fold_left
(fun env p -> EcEnv.TypeClass.add_instance ty (`General p) env)
(EcEnv.Algebra.add_ring (snd ty) cr scope.sc_env)
[p_zmod; p_ring; p_idomain] }
(* ------------------------------------------------------------------ *)
let field_of_symmap env ty symbols =
{ f_ring = ring_of_symmap env ty false symbols;
f_inv = oget (Mstr.find_opt "inv" symbols);
f_div = Mstr.find_opt "div" symbols; }
let addfield (scope : scope) mode { pl_desc = tci; pl_loc = loc; } =
if not (EcAlgTactic.is_module_loaded scope.sc_env) then
hierror "load AlgTactic/Ring first";
let ty =
let ue = TT.transtyvars scope.sc_env (loc, Some (fst tci.pti_type)) in
let ty = transty tp_tydecl scope.sc_env ue (snd tci.pti_type) in
assert (EcUnify.UniEnv.closed ue);
(EcUnify.UniEnv.tparams ue, Tuni.offun (EcUnify.UniEnv.close ue) ty)
in
let symbols = EcAlgTactic.field_symbols scope.sc_env (snd ty) in
let symbols = check_tci_operators scope.sc_env ty tci.pti_ops symbols in
let cr = field_of_symmap scope.sc_env (snd ty) symbols in
let axioms = EcAlgTactic.field_axioms scope.sc_env cr in
check_tci_axioms scope mode tci.pti_axs axioms;
{ scope with sc_env =
List.fold_left
(fun env p -> EcEnv.TypeClass.add_instance ty (`General p) env)
(EcEnv.Algebra.add_field (snd ty) cr scope.sc_env)
[p_zmod; p_ring; p_idomain; p_field] }
(* ------------------------------------------------------------------ *)
let symbols_of_tc (_env : EcEnv.env) ty (tcp, tc) =
let subst = { ty_subst_id with ts_def = Mp.of_list [tcp, ([], ty)] } in
List.map (fun (x, opty) ->
(EcIdent.name x, (true, ty_subst subst opty)))
tc.tc_ops
(*
(* ------------------------------------------------------------------ *)
let add_generic_tc (scope : scope) _mode { pl_desc = tci; pl_loc = loc; } =
let ty =
let ue = TT.transtyvars scope.sc_env (loc, Some (fst tci.pti_type)) in
let ty = transty tp_tydecl scope.sc_env ue (snd tci.pti_type) in
assert (EcUnify.UniEnv.closed ue);
(EcUnify.UniEnv.tparams ue, Tuni.offun (EcUnify.UniEnv.close ue) ty)
in
let (tcp, tc) =
match EcEnv.TypeClass.lookup_opt (unloc tci.pti_name) (env scope) with
| None ->
hierror ~loc:tci.pti_name.pl_loc
"unknown type-class: %s" (string_of_qsymbol (unloc tci.pti_name))
| Some tc -> tc
in
let symbols = symbols_of_tc scope.sc_env (snd ty) (tcp, tc) in
let _symbols = check_tci_operators scope.sc_env ty tci.pti_ops symbols in
{ scope with
sc_env = EcEnv.TypeClass.add_instance ty (`General tcp) scope.sc_env }
(*
let ue = EcUnify.UniEnv.create (Some []) in
let ty = fst (EcUnify.UniEnv.openty ue (fst ty) None (snd ty)) in
try EcUnify.hastc scope.sc_env ue ty (Sp.singleton (fst tc)); tc
with EcUnify.UnificationFailure _ ->
hierror "type must be an instance of `%s'" (EcPath.tostring (fst tc))
*)
*)
(* ------------------------------------------------------------------ *)
let add_instance (scope : scope) mode ({ pl_desc = tci } as toptci) =
match unloc tci.pti_name with
| ([], "bring") -> addring scope mode (true , toptci)
| ([], "ring" ) -> addring scope mode (false, toptci)
| ([], "field") -> addfield scope mode toptci
| _ -> failwith "unsupported" (* FIXME *)
(* ------------------------------------------------------------------ *)
let add_datatype (scope : scope) (tydname : tydname) dt =
let { pl_loc = loc; pl_desc = (tyvars, name); } = tydname in
check_name_available scope name;
(* Check type-parameters / env0 is the env. augmented with an
* abstract type representing the currently processed datatype. *)
let ue = TT.transtyvars scope.sc_env (loc, Some tyvars) in
let tpath = EcPath.pqname (path scope) (unloc name) in
let env0 =
let myself = {
tyd_params = EcUnify.UniEnv.tparams ue;
tyd_type = `Abstract Sp.empty;
} in
EcEnv.Ty.bind (unloc name) myself scope.sc_env
in
(* Check for duplicated constructor names *)
Msym.odup unloc (List.map fst dt)
|> oiter (fun (x, y) -> hierror ~loc:y.pl_loc
"duplicated constructor name: `%s'" x.pl_desc);
(* Type-check constructor types *)
let ctors =
let for1 (cname, cty) =
let ue = EcUnify.UniEnv.copy ue in
let cty = cty |> List.map (TT.transty TT.tp_tydecl env0 ue) in
(unloc cname, cty)
in
dt |> List.map for1
in
let tparams = EcUnify.UniEnv.tparams ue in
(* Check for the positivity condition / emptyness *)
let (schelim, schcase) =
let module E = struct exception Fail end in
let rec scheme1 p (pred, fac) ty =
let ty = EcEnv.Ty.hnorm ty env0 in
match ty.ty_node with
| Tglob _ -> assert false
| Tunivar _ -> assert false
| Tvar _ -> None
| Ttuple tys -> begin
let xs = List.map (fun xty -> (fresh_id_of_ty xty, xty)) tys in
let sc1 = fun (x, xty) -> scheme1 p (pred, EcFol.f_local x xty) xty in
match List.pmap sc1 xs with
| [] -> None
| scs -> Some (EcFol.f_let (LTuple xs) fac (EcFol.f_ands scs))
end
| Tconstr (p', ts) ->
if List.exists (occurs p) ts then raise E.Fail;
if not (EcPath.p_equal p p') then None else
Some (EcFol.f_app pred [fac] tbool)
| Tfun (ty1, ty2) ->
if occurs p ty1 then raise E.Fail;
let x = fresh_id_of_ty ty1 in
scheme1 p (pred, EcFol.f_app fac [EcFol.f_local x ty1] ty2) ty2
|> omap (EcFol.f_forall [x, EcFol.GTty ty1])
and schemec mode (targs, p) pred (ctor, tys) =
let indty = tconstr p (List.map tvar targs) in
let ctor = EcPath.pqname (path scope) ctor in
let ctor = EcFol.f_op ctor (List.map tvar targs) indty in
let xs = List.map (fun xty -> (fresh_id_of_ty xty, xty)) tys in
let cargs = List.map (fun (x, xty) -> EcFol.f_local x xty) xs in
let form = EcFol.f_app pred [EcFol.f_app ctor cargs indty] tbool in
let form =
match mode with
| `Case -> form
| `Elim ->
let sc1 = fun (x, xty) -> scheme1 p (pred, EcFol.f_local x xty) xty in
let scs = List.pmap sc1 xs in
(EcFol.f_imps scs form)
in
let form =
let bds = List.map (fun (x, xty) -> (x, EcFol.GTty xty)) xs in
EcFol.f_forall bds form
in
form
and scheme mode (targs, p) ctors =
let indty = tconstr p (List.map tvar targs) in
let indx = fresh_id_of_ty indty in
let indfm = EcFol.f_local indx indty in
let predty = tfun indty tbool in
let predx = EcIdent.create "P" in
let pred = EcFol.f_local predx predty in
let scs = List.map (schemec mode (targs, p) pred) ctors in
let form = EcFol.f_app pred [indfm] tbool in
let form = EcFol.f_forall [indx, EcFol.GTty indty] form in
let form = EcFol.f_imps scs form in
let form = EcFol.f_forall [predx, EcFol.GTty predty] form in
form
and occurs p t =
let t = EcEnv.Ty.hnorm t env0 in
match t.ty_node with
| Tconstr (p', _) when EcPath.p_equal p p' -> true
| _ -> EcTypes.ty_sub_exists (occurs p) t
in
let (schelim, schcase) =
try
let schelim = scheme `Elim (List.map fst tparams, tpath) ctors in
let schcase = scheme `Case (List.map fst tparams, tpath) ctors in
(schelim, schcase)
with E.Fail ->
hierror ~loc "the datatype does not respect the positivity condition"
in
if List.for_all (fun (_, cty) -> List.exists (occurs tpath) cty) ctors then
hierror ~loc "this datatype is empty";
(schelim, schcase)
in
(* Add final datatype to environment *)
let tydecl = {
tyd_params = tparams;
tyd_type = `Datatype { tydt_ctors = ctors;
tydt_schcase = schcase;
tydt_schelim = schelim; };
} in
bind scope (unloc name, tydecl)
(* ------------------------------------------------------------------ *)
let add_record (scope : scope) (tydname : tydname) rt =
let { pl_loc = loc; pl_desc = (tyvars, name); } = tydname in
check_name_available scope name;
(* Check type-parameters *)
let ue = TT.transtyvars scope.sc_env (loc, Some tyvars) in
let tpath = EcPath.pqname (path scope) (unloc name) in
(* Check for duplicated field names *)
Msym.odup unloc (List.map fst rt)
|> oiter (fun (x, y) -> hierror ~loc:y.pl_loc
"duplicated field name: `%s'" x.pl_desc);
(* Type-check field types *)
let fields =
let for1 (fname, fty) =
let fty = TT.transty TT.tp_tydecl (env scope) ue fty in
(unloc fname, fty)
in
rt |> List.map for1
in
let tparams = EcUnify.UniEnv.tparams ue in
(* Generate induction scheme *)
let scheme =
let targs = List.map (tvar |- fst) tparams in
let recty = tconstr tpath targs in
let recx = fresh_id_of_ty recty in
let recfm = EcFol.f_local recx recty in
let predty = tfun recty tbool in
let predx = EcIdent.create "P" in
let pred = EcFol.f_local predx predty in
let ctor = EcPath.pqoname
(EcPath.prefix tpath)
(Printf.sprintf "mk_%s" (unloc name)) in
let ctor = EcFol.f_op ctor targs (toarrow (List.map snd fields) recty) in
let prem =
let ids = List.map (fun (_, fty) -> (fresh_id_of_ty fty, fty)) fields in
let vars = List.map (fun (x, xty) -> EcFol.f_local x xty) ids in
let bds = List.map (fun (x, xty) -> (x, EcFol.GTty xty)) ids in
let recv = EcFol.f_app ctor vars recty in
EcFol.f_forall bds (EcFol.f_app pred [recv] tbool) in
let form = EcFol.f_app pred [recfm] tbool in
let form = EcFol.f_forall [recx, EcFol.GTty recty] form in
let form = EcFol.f_imp prem form in
let form = EcFol.f_forall [predx, EcFol.GTty predty] form in
form
in
(* Add final record to environment *)
let tparams = EcUnify.UniEnv.tparams ue in
let tydecl = {
tyd_params = tparams;
tyd_type = `Record (scheme, fields);
} in
bind scope (unloc name, tydecl)
end
(* -------------------------------------------------------------------- *)
module Theory = struct
exception TopScope
(* ------------------------------------------------------------------ *)
let bind (scope : scope) ((x, cth) : _ * EcEnv.ctheory_w3) =
assert (scope.sc_pr_uc = None);
let scope =
{ scope with
sc_env = EcEnv.Theory.bind x cth scope.sc_env; }
in
maybe_add_to_section scope
(EcTheory.CTh_theory (x, EcEnv.ctheory_of_ctheory_w3 cth))
(* ------------------------------------------------------------------ *)
let required (scope : scope) (name : symbol) =
assert (scope.sc_pr_uc = None);
List.exists (fun x -> x = name) scope.sc_required
(* ------------------------------------------------------------------ *)
let enter (scope : scope) (name : symbol) =
assert (scope.sc_pr_uc = None);
subscope scope name
(* ------------------------------------------------------------------ *)
let rec require_loaded id scope =
if required scope id then
scope
else
match Msym.find_opt id scope.sc_loaded with
| Some (rth, ids) ->
let scope = List.fold_right require_loaded ids scope in
let env = EcEnv.Theory.require id rth scope.sc_env in
{ scope with
sc_env = env;
sc_required = id :: scope.sc_required; }
| None -> assert false
(* -------------------------------------------------------------------- *)
let exit_r (scope : scope) =
match scope.sc_top with
| None -> raise TopScope
| Some sup ->
begin
match EcSection.opath scope.sc_section with
| None -> ()
| Some (_, sp) ->
if p_equal sp (EcEnv.root scope.sc_env) then
hierror "cannot close a theory with active sections";
end;
let cth = EcEnv.Theory.close scope.sc_env in
let loaded = scope.sc_loaded in
let section = scope.sc_section in
let required = scope.sc_required in
let sup = { sup with sc_loaded = loaded; sc_section = section; } in
((cth, required), scope.sc_name, sup)
(* ------------------------------------------------------------------ *)
let exit (scope : scope) =
assert (scope.sc_pr_uc = None);
let ((cth, required), name, scope) = exit_r scope in
let scope = List.fold_right require_loaded required scope in
(name, bind scope (name, cth))
(* ------------------------------------------------------------------ *)
let import (scope : scope) (name : qsymbol) =
assert (scope.sc_pr_uc = None);
let path = fst (EcEnv.Theory.lookup name scope.sc_env) in
{ scope with
sc_env = EcEnv.Theory.import path scope.sc_env }
(* ------------------------------------------------------------------ *)
let export (scope : scope) (name : qsymbol) =
assert (scope.sc_pr_uc = None);
let path = fst (EcEnv.Theory.lookup name scope.sc_env) in
{ scope with
sc_env = EcEnv.Theory.export path scope.sc_env }
(* ------------------------------------------------------------------ *)
let check_end_required scope thname =
if scope.sc_name <> thname then
begin
let msg =
Printf.sprintf
"end-of-file while processing external theory %s %s"
scope.sc_name thname in
failwith msg
end;
if scope.sc_pr_uc <> None then
let msg =
Printf.sprintf
"end-of-file while processing proof %s" scope.sc_name
in
failwith msg
(* -------------------------------------------------------------------- *)
let require (scope : scope) (name : symbol) loader =
assert (scope.sc_pr_uc = None);
if required scope name then
scope
else
match Msym.find_opt name scope.sc_loaded with
| Some _ -> require_loaded name scope
| None ->
let imported = enter (for_loading scope) name in
let thname = imported.sc_name in
let imported = loader imported in
check_end_required imported thname;
let cthr, name, imported = exit_r imported in
let scope =
{ scope with
sc_loaded = Msym.add name cthr imported.sc_loaded; }
in
require_loaded name scope
(* ------------------------------------------------------------------ *)
let clone (scope : scope) mode (thcl : theory_cloning) =
let module C = EcThCloning in
assert (scope.sc_pr_uc = None);
if EcSection.in_section scope.sc_section then
hierror "cannot clone a theory while a section is active";
let (name, proofs, nth) = C.clone scope.sc_env thcl in
let proofs = List.pmap (fun axc ->
match axc.C.axc_tac with
| None -> Some (axc.C.axc_axiom, axc.C.axc_path, axc.C.axc_env)
| Some pt ->
let t = { pt_core = pt; pt_intros = []; } in
let t = { pl_loc = pt.pl_loc; pl_desc = Pby (Some [t]); } in
let t = { pt_core = t; pt_intros = []; } in
let (x, ax) = axc.C.axc_axiom in
let pucflags = { puc_nosmt = false; puc_local = false; } in
let pucflags = (([], None), pucflags) in
let check = Check_mode.check scope.sc_options in
let escope = { scope with sc_env = axc.C.axc_env; } in
let escope = Ax.start_lemma escope pucflags check x ax in
let escope = Tactics.proof escope mode true in
let escope = Tactics.process_r false mode escope [t] in
ignore (Ax.save escope pt.pl_loc); None)
proofs
in
let scope = bind scope (name, nth) in
let scope = Ax.add_for_cloning scope proofs in
(name, scope)
(* ------------------------------------------------------------------ *)
let import_w3 scope dir file renaming =
assert (scope.sc_pr_uc = None);
if EcSection.in_section scope.sc_section then
hierror "cannot import a Why3 theory while a section is active";
let mk_renaming (l,k,s) =
let k =
match k with
| RNty -> EcWhy3.RDts
| RNop -> EcWhy3.RDls
| RNpr -> EcWhy3.RDpr
in
(l, k, s)
in
let renaming = List.map mk_renaming renaming in
let env = fst (EcEnv.import_w3_dir scope.sc_env dir file renaming) in
{ scope with sc_env = env }
end
(* -------------------------------------------------------------------- *)
module Section = struct
module T = EcTheory
let enter (scope : scope) (name : psymbol option) =
assert (scope.sc_pr_uc = None);
{ scope with
sc_section =
EcSection.enter scope.sc_env
(omap unloc name) scope.sc_section; }
let exit (scope : scope) (name : psymbol option) =
match EcSection.opath scope.sc_section with
| None -> hierror "no section to close"
| Some (sname, sp) ->
if not (p_equal sp (EcEnv.root (scope.sc_env))) then
hierror "cannot close a section containing pending theories";
if sname <> (omap unloc name) then
hierror "expecting [%s], not [%s]"
(match sname with None -> "<empty>" | Some x -> x)
(match name with None -> "<empty>" | Some x -> unloc x);
let (locals, osc) = EcSection.exit scope.sc_section in
let oenv = EcSection.env_of_locals locals in
let oitems = EcSection.items_of_locals locals in
let scenv = scope.sc_env in
let scope = { scope with sc_env = oenv; sc_section = osc; } in
let rec bind1 scope item =
match item with
| T.CTh_type (x, ty) -> Ty.bind scope (x, ty)
| T.CTh_operator (x, op) -> Op.bind scope (x, op)
| T.CTh_modtype (x, mt) -> ModType.bind scope (x, mt)
| T.CTh_module me ->
let mep = EcPath.pqname (path scope) me.me_name in
if not (EcSection.is_local `Module mep locals) then
Mod.bind scope false me
else
scope
| T.CTh_axiom (x, ax) -> begin
match ax.ax_kind with
| `Axiom -> scope
| `Lemma ->
let axp = EcPath.pqname (path scope) x in
if not (EcSection.is_local `Lemma axp locals) then
Ax.bind scope false
(x, { ax with ax_spec =
ax.ax_spec |> omap (EcSection.generalize scenv locals) })
else
scope
end
| T.CTh_export p ->
{ scope with sc_env = EcEnv.Theory.export p scope.sc_env }
| T.CTh_theory (x, th) ->
let scope = Theory.enter scope x in
let scope = List.fold_left bind1 scope th.EcTheory.cth_struct in
let _, scope = Theory.exit scope in
scope
| T.CTh_typeclass (x, tc) -> Ty.bindclass scope (x, tc)
| T.CTh_instance (p, cr) ->
{ scope with
sc_env = EcEnv.TypeClass.add_instance p cr scope.sc_env }
| T.CTh_baserw x ->
{ scope with
sc_env = EcEnv.BaseRw.bind x scope.sc_env }
| T.CTh_addrw(p,l) ->
{ scope with
sc_env = EcEnv.BaseRw.bind_addrw p l scope.sc_env }
in
List.fold_left bind1 scope oitems
end
(* -------------------------------------------------------------------- *)
module Extraction = struct
let check_top scope =
if not (scope.sc_top = None) then
hierror "Extraction cannot be done inside a theory";
if EcSection.in_section scope.sc_section then
hierror "Extraction cannot be done inside a section"
let process scope todo =
check_top scope;
EcExtraction.process_extraction (env scope) scope.sc_required todo;
scope
end
(* -------------------------------------------------------------------- *)
module BaseRw = struct
let process scope x =
{ scope with
sc_env = EcEnv.BaseRw.bind x.pl_desc (env scope) }
let process_addrw scope (x,l) =
let env = env scope in
let env, base =
match EcEnv.BaseRw.lookup_opt x.pl_desc env with
| None ->
let pre, base = x.pl_desc in
if pre <> [] then
hierror ~loc:x.pl_loc
"cannot create a hint rewrite base outside a theory";
let p = EcPath.pqname (EcEnv.root env) base in
begin match EcEnv.Ax.by_path_opt p env with
| None -> ()
| Some _ ->
hierror ~loc:x.pl_loc
"an axiom with the same name already exists";
end;
let env = EcEnv.BaseRw.bind base env in
env, fst (EcEnv.BaseRw.lookup x.pl_desc env)
| Some (base, _) -> env, base in
let l = List.map (fun l -> EcEnv.Ax.lookup_path l.pl_desc env) l in
{ scope with
sc_env = EcEnv.BaseRw.bind_addrw base l env }
end