https://github.com/EasyCrypt/easycrypt
Raw File
Tip revision: a79f9aeb6de046ca12210d26317fab59c175d0dd authored by Pierre-Yves Strub on 08 July 2014, 09:43:21 UTC
Fix bug w.r.t. _tools presence detection.
Tip revision: a79f9ae
ecAlgTactic.ml
(* Copyright (c) - 2012-2014 - IMDEA Software Institute and INRIA
 * Distributed under the terms of the CeCILL-B license *)

(* -------------------------------------------------------------------- *)
open EcUtils
open EcTypes
open EcFol
open EcDecl
open EcCoreGoal
open EcAlgebra

(* -------------------------------------------------------------------- *)
module Axioms = struct
  open EcDecl

  let tmod  = EcPath.fromqsymbol ([EcCoreLib.id_top; "AlgTactic"], "Requires")
  let tname = "domain"


  let tmod_and_deps =
    tmod :: [
      EcPath.fromqsymbol ([EcCoreLib.id_top; "Ring"], "Field")
    ]

  let zero  = "rzero"
  let one   = "rone"
  let add   = "add"
  let opp   = "opp"
  let sub   = "sub"
  let mul   = "mul"
  let inv   = "inv"
  let div   = "div"
  let expr  = "expr"
  let embed = "ofint"

  let core_add  = ["oner_neq0"; "addr0"; "addrA"; "addrC";]
  let core_mul  = [ "mulr1"; "mulrA"; "mulrC"; "mulrDl"]
  let core      = core_add @ "addrN" :: core_mul
  let core_bool = core_add @ "addrK" :: "mulrK" :: core_mul

  let ofoppbool = ["oppr_id"]
  let intpow    = ["expr0"; "exprS"]
  let ofint     = ["ofint0"; "ofint1"; "ofintS"; "ofintN"]
  let ofsub     = ["subrE"]
  let field     = ["mulrV"; "exprN"]
  let ofdiv     = ["divrE"]

  let ty0 ty = ty
  let ty1 ty = tfun ty (ty0 ty)
  let ty2 ty = tfun ty (ty1 ty)

  let ring_symbols env boolean ty =
    let symbols =
      [(zero, (true , ty0 ty));
       (one , (true , ty0 ty));
       (add , (true , ty2 ty));
       (opp , (not boolean, ty1 ty));
       (sub , (false, ty2 ty));
       (mul , (true , ty2 ty));
       (expr, (false, toarrow [ty; tint] ty))]
    in
      if   EcReduction.EqTest.for_type env ty tint
      then symbols
      else symbols @ [(embed, (false, tfun tint ty))]

  let field_symbols env ty =
    (ring_symbols env false ty)
      @ [(inv, (true , ty1 ty));
         (div, (false, ty2 ty))]

  let subst_of_ring (cr : ring) =
    let crcore = [(zero, cr.r_zero);
                  (one , cr.r_one );
                  (add , cr.r_add );
                  (mul , cr.r_mul ); ] in

    let xpath  = fun x -> EcPath.pqname tmod x in
    let add    = fun subst x p -> EcSubst.add_path subst (xpath x) p in
    
    let subst  = 
      EcSubst.add_tydef EcSubst.empty (xpath tname) ([], cr.r_type) in
    let subst  =
      List.fold_left (fun subst (x, p) -> add subst x p) subst crcore in
    let subst  = odfl subst (cr.r_opp |> omap (fun p -> add subst opp p)) in
    let subst  = odfl subst (cr.r_sub |> omap (fun p -> add subst sub p)) in
    let subst  = odfl subst (cr.r_exp |> omap (fun p -> add subst expr p)) in

    let subst  = 
      cr.r_embed |> 
          (function `Direct | `Default -> subst | `Embed p -> add subst embed p)
    in
      subst

  let subst_of_field (cr : field) =
    let xpath  = fun x -> EcPath.pqname tmod x in
    let add    = fun subst x p -> EcSubst.add_path subst (xpath x) p in

    let subst = subst_of_ring cr.f_ring in
    let subst = add subst inv cr.f_inv in
    let subst = odfl subst (cr.f_div |> omap (fun p -> add subst div p)) in
      subst

  (* FIXME: should use operators inlining when available *)
  let get cr env axs =
    let subst  =
      match cr with
      | `Ring  cr -> subst_of_ring  cr
      | `Field cr -> subst_of_field cr
    in

    let for1 axname =
      let ax = EcEnv.Ax.by_path (EcPath.pqname tmod axname) env in
        assert (ax.ax_tparams = [] && ax.ax_kind = `Axiom && ax.ax_spec <> None);
        (axname, EcSubst.subst_form subst (oget ax.ax_spec))
    in
      List.map for1 axs

  let getr env cr axs = get (`Ring cr) env axs
  let getf env cr axs = get (`Field cr) env axs 

  let ring_axioms env (cr : ring) =
    let axcore = 
      if cr.r_bool then getr env cr core_bool
      else getr env cr core in
    let axint  = 
      match cr.r_embed with 
      | `Direct | `Default -> [] | `Embed _ -> getr env cr ofint in
    let axopp = 
      match cr.r_opp with
      | Some _ when cr.r_bool -> getr env cr ofoppbool
      | _ -> [] in
    let axsub  = 
      match cr.r_sub with None -> [] | Some _ -> getr env cr ofsub in
    let axexp  = 
      match cr.r_exp with None -> [] | Some _ -> getr env cr intpow in

    List.flatten [axcore; axopp; axexp; axint; axsub]

  let field_axioms env (cr : field) =
    let axring = ring_axioms env cr.f_ring in
    let axcore = getf env cr field in
    let axdiv  = match cr.f_div with None -> [] | Some _ -> getf env cr ofdiv in
    List.flatten [axring; axcore; axdiv]

end

let ring_symbols  = Axioms.ring_symbols
let field_symbols = Axioms.field_symbols

let ring_axioms  = Axioms.ring_axioms
let field_axioms = Axioms.field_axioms

(* -------------------------------------------------------------------- *)
let is_module_loaded env =
  List.for_all
    (fun x -> EcEnv.Theory.by_path_opt x env <> None)
    Axioms.tmod_and_deps

(* -------------------------------------------------------------------- *)
let t_ring_simplify cr eqs (f1, f2) tc =
  let hyps = FApi.tc1_hyps tc in
  let cr = cring_of_ring cr in
  let f1 = ring_simplify hyps cr eqs f1 in
  let f2 = ring_simplify hyps cr eqs f2 in
  FApi.xmutate1 tc `Ring [f_eq f1 f2]

let t_ring r eqs (f1, f2) tc =
  let hyps = FApi.tc1_hyps tc in
  let cr = cring_of_ring r in
  let f  = ring_eq hyps cr eqs f1 f2 in
  if   EcReduction.is_conv hyps f (emb_rzero r)
  then FApi.xmutate1 tc `Ring []
  else FApi.xmutate1 tc `Ring [f_eq f (emb_rzero r)]

let t_ring_congr (cr:cring) (rm:RState.rstate) pe li lv tc =
  let rm' = RState.update rm li lv in
  let env = FApi.tc1_env tc in
  let mk_goal i =
    let r1 = oget (RState.get i rm) in
    let r2 = oget (RState.get i rm') in
    EcReduction.EqTest.for_type_exn env r1.f_ty r2.f_ty;
    f_eq r1 r2 in 
  let r = ring_of_cring cr in
  let f = ofring r rm pe in
  let f' = ofring r rm' pe in
  let concl = FApi.tc1_goal tc in
  if not (f_equal (f_eq f f') concl) then raise InvalidGoalShape;
  let sg = List.map mk_goal li in
  FApi.xmutate1 tc `Ring_congr sg 

let t_field_simplify r eqs (f1, f2) tc =
  let hyps = FApi.tc1_hyps tc in
  let cr = cfield_of_field r in
  let (c1, n1, d1) = field_simplify hyps cr eqs f1 in
  let (c2, n2, d2) = field_simplify hyps cr eqs f2 in

  let c = List.map (fun f -> f_not (f_eq f (emb_fzero r))) (c1 @ c2) in
  let f = f_eq (fdiv r n1 d1) (fdiv r n2 d2) in

  FApi.xmutate1 tc `Field (c @ [f])

let t_field r eqs (f1, f2) tc =
  let hyps = FApi.tc1_hyps tc in
  let cr = cfield_of_field r in
  let (c, (n1, n2), (d1, d2)) = field_eq hyps cr eqs f1 f2 in
  let c  = List.map (fun f -> f_not (f_eq f (emb_fzero r))) c in
  let c  = Sf.elements (Sf.of_list c) in
  let r1 = fmul r n1 d2
  and r2 = fmul r n2 d1 in
  let f  = ring_eq hyps (cring_of_ring r.f_ring) eqs r1 r2 in

  if   EcReduction.is_conv hyps f (emb_fzero r)
  then FApi.xmutate1 tc `Field c
  else FApi.xmutate1 tc `Field (c @ [f_eq f (emb_fzero r)])

let t_field_congr (cr:cfield) (rm:RState.rstate) pe li lv tc =
  let rm' = RState.update rm li lv in
  let env = FApi.tc1_env tc in
  let mk_goal i =
    let r1 = oget (RState.get i rm) in
    let r2 = oget (RState.get i rm') in
    EcReduction.EqTest.for_type_exn env r1.f_ty r2.f_ty;
    f_eq r1 r2 in 
  let r = field_of_cfield cr in
  let f = offield r rm pe in
  let f' = offield r rm' pe in
  let concl = FApi.tc1_goal tc in
  if not (f_equal (f_eq f f') concl) then raise InvalidGoalShape;
  let sg = List.map mk_goal li in
  FApi.xmutate1 tc `Field_congr sg 
back to top