https://github.com/EasyCrypt/easycrypt
Revision e4c545fc5c222c2c7f715137e546a5fb5d7fa72b authored by Pierre-Yves Strub on 07 July 2014, 14:20:08 UTC, committed by Pierre-Yves Strub on 07 July 2014, 14:20:08 UTC
1 parent 205e287
Raw File
Tip revision: e4c545fc5c222c2c7f715137e546a5fb5d7fa72b authored by Pierre-Yves Strub on 07 July 2014, 14:20:08 UTC
Explain restrictions errors (in UI)
Tip revision: e4c545f
ecInt.ml
(* Int.zero *)
let zero : int = 0
  
(* Int.one *)
let one : int = 1
  
(* Int.< *)
let ls (x:int) (y:int) = x < y

(* Int.> *)
let gt (x:int) (y:int) = x > y
  
(* Int.<= *)
let lseq (x:int) (y:int) = x <= y
 
(* Int.>= *)
let gteq (x:int) (y:int) = x >= y
 
(* Int.+ *)
let pl = (+)

(* Int.[-] *)
let lbmnrb = (~-)
  
(* Int.* *)
let as0 = ( * )

(* Int.- *)
let mn = (-)

(* Int.Abs *)
module Abs = struct
  
  (* Int.Abs.`|_| *)
  let bqbr_br = Pervasives.abs
  
end
  
(* Int.Extrema *)
module Extrema = struct

  (* Int.Extrema.min *)
  let min = fun a b -> (if ls a b then a else b)
  
  (* Int.Extrema.max *)
  let max = fun a b -> (if ls a b then b else a)
    
end
  
(* Int.EuclDiv *)
module EuclDiv = struct

  (* Int.EuclDiv./% *)
  let slpc = (/)  

  (* Int.EuclDiv.%% *)
  let pcpc = (mod)
  
end
  
(* Int.Power *)
module Power = struct
  
  (* Int.Power.^ *)
  let rec cf x p = 
    if p <= 0 then 1 
    else 
      let pow = cf x (p lsr 1) in
      if p land 1 = 0 then pow else pow * x
        
end

(* Int.ForLoop *)
module ForLoop = struct

  (* Int.ForLoop.range *)
  let range i j st f =
    let st = ref st in
    for k = i to (j - 1) do
      st := f k !st;
    done;
    !st
end
back to top