package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file vmlambda.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
open Util
open Declarations
open Genlambda
open Vmvalues

type lval = int * structured_values (* keep the hash *)
type lambda = lval Genlambda.lambda

let get_lval (_, v) = v

(** Simplification of lambda expression *)

(*s Translation from [constr] to [lambda] *)

(* Translation of constructor *)

let is_value lc =
  match lc with
  | Lval _ | Lint _ | Luint _ | Lfloat _ -> true
  | _ -> false

let get_value lc =
  match lc with
  | Luint i -> val_of_uint i
  | Lval (_, v) -> v
  | Lint i -> val_of_int i
  | Lfloat f -> val_of_float f
  | _ -> assert false

let hash_block tag args =
  let open Hashset.Combine in
  let fold accu v =
    let h = match v with
    | Luint i -> Uint63.hash i
    | Lint i -> Hashtbl.hash (i : int)
    | Lfloat f -> Float64.hash f
    | Lval (h, _) -> h
    | _ -> assert false
    in
    combine accu h
  in
  combine tag (Array.fold_left fold 0 args)

module HashBlock =
struct
  type t = int * structured_values array * structured_values (* tag, block, value *)
  let eq (tag1, args1, _) (tag2, args2, _) =
    Int.equal tag1 tag2 && CArray.equal (==) args1 args2
end

module HashsetBlock = Hashset.Make(HashBlock)

let block_table = HashsetBlock.create 97

let as_value tag args =
  if Array.for_all is_value args then
    let h = hash_block tag args in
    (* Don't simplify this to Array.map because of flat float arrays *)
    let args =
      let dummy_val = Obj.magic 0 in
      let ans = Array.make (Array.length args) dummy_val in
      let () = Array.iteri (fun i v -> ans.(i) <- get_value v) args in
      ans
    in
    if tag < Obj.last_non_constant_constructor_tag then
      let block = val_of_block tag args in
      let (_, _, block) = HashsetBlock.repr h (tag, args, block) block_table in
      Some (h, block)
    else
      let args = Array.append [| val_of_int (tag - Obj.last_non_constant_constructor_tag) |] args in
      let block = val_of_block Obj.last_non_constant_constructor_tag args in
      let (_, _, block) = HashsetBlock.repr h (tag, args, block) block_table in
      Some (h, block)
  else None

module Val =
struct
  type value = int * structured_values
  let as_value = as_value
  let check_inductive (_, i) mb =
    let { mind_typename=name; mind_nb_args; mind_nb_constant; _ } = mb.mind_packets.(i) in
    Vmerrors.check_compilable_ind ~name ~mind_nb_args ~mind_nb_constant
end

module Lambda = Genlambda.Make(Val)

(*********************************)
let dump_lambda = ref false

let lambda_of_constr env sigma c =
  let lam = Lambda.lambda_of_constr env sigma c in
  let lam = optimize lam in
  if !dump_lambda then
    Feedback.msg_debug (pp_lam lam);
  lam
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct