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
ecProofTyping.ml
(* --------------------------------------------------------------------
* 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 EcUtils
open EcIdent
open EcTypes
open EcFol
open EcEnv
open EcCoreGoal
module Msym = EcSymbols.Msym
(* -------------------------------------------------------------------- *)
type ptnenv = ty Mid.t * EcUnify.unienv
(* ------------------------------------------------------------------ *)
let unienv_of_hyps hyps =
let tv = (LDecl.tohyps hyps).EcBaseLogic.h_tvar in
EcUnify.UniEnv.create (Some tv)
(* ------------------------------------------------------------------ *)
let process_form_opt hyps pf oty =
try
let ue = unienv_of_hyps hyps in
let ff = EcTyping.trans_form_opt (LDecl.toenv hyps) ue pf oty in
EcFol.Fsubst.uni (EcUnify.UniEnv.close ue) ff
with EcUnify.UninstanciateUni ->
EcTyping.tyerror pf.EcLocation.pl_loc
(LDecl.toenv hyps) EcTyping.FreeTypeVariables
let process_form hyps pf ty =
process_form_opt hyps pf (Some ty)
let process_formula hyps pf =
process_form hyps pf tbool
let process_exp hyps mode oty e =
let env = LDecl.toenv hyps in
let ue = unienv_of_hyps hyps in
let e = EcTyping.transexpcast_opt env mode ue oty e in
EcTypes.e_uni (EcUnify.UniEnv.close ue) e
let process_pattern hyps fp =
let ps = ref Mid.empty in
let ue = unienv_of_hyps hyps in
let fp = EcTyping.trans_pattern (LDecl.toenv hyps) (ps, ue) fp in
((!ps, ue), fp)
(* ------------------------------------------------------------------ *)
let pf_process_form_opt pe hyps oty pf =
Exn.recast_pe pe hyps (fun () -> process_form_opt hyps pf oty)
let pf_process_form pe hyps ty pf =
Exn.recast_pe pe hyps (fun () -> process_form hyps pf ty)
let pf_process_formula pe hyps pf =
Exn.recast_pe pe hyps (fun () -> process_formula hyps pf)
let pf_process_exp pe hyps mode oty e =
Exn.recast_pe pe hyps (fun () -> process_exp hyps mode oty e)
let pf_process_pattern pe hyps fp =
Exn.recast_pe pe hyps (fun () -> process_pattern hyps fp)
(* ------------------------------------------------------------------ *)
let tc1_process_form_opt tc oty pf =
Exn.recast_tc1 tc (fun hyps -> process_form_opt hyps pf oty)
let tc1_process_form tc ty pf =
Exn.recast_tc1 tc (fun hyps -> process_form hyps pf ty)
let tc1_process_formula tc pf =
Exn.recast_tc1 tc (fun hyps -> process_formula hyps pf)
let tc1_process_exp tc mode oty e =
Exn.recast_tc1 tc (fun hyps -> process_exp hyps mode oty e)
let tc1_process_pattern tc fp =
Exn.recast_tc1 tc (fun hyps -> process_pattern hyps fp)
(* ------------------------------------------------------------------ *)
let tc1_process_prhl_form_opt tc oty pf =
let hyps, concl = FApi.tc1_flat tc in
let ml, mr =
match concl.f_node with
| FequivS es -> (es.es_ml, es.es_mr)
| _ -> assert false
in
let hyps = LDecl.push_all [ml; mr] hyps in
pf_process_form_opt !!tc hyps oty pf
let tc1_process_prhl_form tc ty pf = tc1_process_prhl_form_opt tc (Some ty) pf
(* ------------------------------------------------------------------ *)
let tc1_process_prhl_formula tc pf =
tc1_process_prhl_form tc tbool pf
(* ------------------------------------------------------------------ *)
let tc1_process_stmt ?map tc mt c =
let hyps = FApi.tc1_hyps tc in
let hyps = LDecl.push_active (mhr,mt) hyps in
let env = LDecl.toenv hyps in
let ue = unienv_of_hyps hyps in
let c = Exn.recast_pe !!tc hyps (fun () -> EcTyping.transstmt ?map env ue c) in
let esub = Exn.recast_pe !!tc hyps (fun () -> Tuni.offun (EcUnify.UniEnv.close ue)) in
let esub = { e_subst_id with es_ty = esub; } in
EcModules.s_subst esub c
let tc1_process_prhl_stmt ?map tc side c =
let concl = FApi.tc1_goal tc in
let es = match concl.f_node with FequivS es -> es | _ -> assert false in
let mt = snd (match side with `Left -> es.es_ml | `Right -> es.es_mr) in
tc1_process_stmt tc mt ?map c
(* ------------------------------------------------------------------ *)
let tc1_process_Xhl_exp tc side ty e =
let hyps, concl = FApi.tc1_flat tc in
let m = fst (EcFol.destr_programS side concl) in
let hyps = LDecl.push_active m hyps in
pf_process_exp !!tc hyps `InProc ty e
(* ------------------------------------------------------------------ *)
let tc1_process_Xhl_form ?side tc ty pf =
let hyps, concl = FApi.tc1_flat tc in
let memory =
match concl.f_node, side with
| FhoareS hs, None -> hs.hs_m
| FbdHoareS hs, None -> hs.bhs_m
| FequivS es, Some `Left -> (mhr, snd es.es_ml)
| FequivS es, Some `Right -> (mhr, snd es.es_mr)
| _, _ -> raise (DestrError "destr_programS")
in
let hyps = LDecl.push_active memory hyps in
pf_process_form !!tc hyps ty pf
(* ------------------------------------------------------------------ *)
let tc1_process_Xhl_formula ?side tc pf =
tc1_process_Xhl_form ?side tc tbool pf
(* ------------------------------------------------------------------ *)
(* FIXME: factor out to typing module *)
(* FIXME: TC HOOK - check parameter constraints *)
(* ------------------------------------------------------------------ *)
let pf_check_tvi (pe : proofenv) typ tvi =
match tvi with
| None -> ()
| Some (EcUnify.TVIunamed tyargs) ->
if List.length tyargs <> List.length typ then
tc_error pe
"wrong number of type parameters (%d, expecting %d)"
(List.length tyargs) (List.length typ)
| Some (EcUnify.TVInamed tyargs) ->
let typnames = List.map (EcIdent.name |- fst) typ in
List.iter
(fun (x, _) ->
if not (List.mem x typnames) then
tc_error pe "unknown type variable: %s" x)
tyargs
(* -------------------------------------------------------------------- *)
exception NoMatch
type lazyred = [`Full | `NoDelta | `None]
let t_lazy_match ?(reduce = `Full) (tx : form -> FApi.backward) (tc : tcenv1) =
let hyps, concl = FApi.tc1_flat tc in
let rec do1 fp =
try tx fp tc
with
| NoMatch -> begin
let strategy =
match reduce with
| `None -> raise InvalidGoalShape
| `Full -> EcReduction.full_red
| `NoDelta -> EcReduction.nodelta in
match EcReduction.h_red_opt strategy hyps fp with
| None -> raise InvalidGoalShape
| Some fp -> do1 fp
end
in do1 concl
(* -------------------------------------------------------------------- *)
let rec lazy_destruct ?(reduce = true) hyps tx fp =
try Some (tx fp)
with
| NoMatch when not reduce -> None
| NoMatch ->
match EcReduction.h_red_opt EcReduction.full_red hyps fp with
| None -> None
| Some fp -> lazy_destruct ~reduce hyps tx fp
(* -------------------------------------------------------------------- *)
type dproduct = [
| `Imp of form * form
| `Forall of EcIdent.t * gty * form
]
let destruct_product ?(reduce = true) hyps fp : dproduct option =
let doit fp =
match EcFol.sform_of_form fp with
| SFquant (Lforall, (x, t), lazy f) -> `Forall (x, t, f)
| SFimp (f1, f2) -> `Imp (f1, f2)
| _ -> raise NoMatch
in
lazy_destruct ~reduce hyps doit fp
(* -------------------------------------------------------------------- *)
type dexists = [
| `Exists of EcIdent.t * gty * form
]
let destruct_exists ?(reduce = true) hyps fp : dexists option =
let doit fp =
match EcFol.sform_of_form fp with
| SFquant (Lexists, (x, t), lazy f) -> `Exists (x, t, f)
| _ -> raise NoMatch
in
lazy_destruct ~reduce hyps doit fp