hvm 1.0.11-beta

A massively parallel functional runtime.
Documentation 
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
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179

use crate::runtime::{*};
use std::sync::atomic::{Ordering};

#[inline(always)]
pub fn visit(ctx: ReduceCtx, sidxs: &[u64]) -> bool {
  let len = sidxs.len() as u64;
  if len == 0 {
    return false;
  } else {
    let mut vlen = 0;
    let vbuf = unsafe { ctx.heap.vbuf.get_unchecked(ctx.tid) };
    for sidx in sidxs {
      if !is_whnf(load_arg(ctx.heap, ctx.term, *sidx)) {
        unsafe { vbuf.get_unchecked(vlen) }.store(get_loc(ctx.term, *sidx), Ordering::Relaxed);
        vlen += 1;
      }
    }
    if vlen == 0 {
      return false;
    } else {
      let goup = ctx.redex.insert(ctx.tid, new_redex(*ctx.host, *ctx.cont, vlen as u64));
      for i in 0 .. vlen - 1 {
        ctx.visit.push(new_visit(unsafe { vbuf.get_unchecked(i).load(Ordering::Relaxed) }, ctx.hold, goup));
      }
      *ctx.cont = goup;
      *ctx.host = unsafe { vbuf.get_unchecked(vlen - 1).load(Ordering::Relaxed) };
      return true;
    }
  }
  //OLD_VISITER:
  //let len = sidxs.len() as u64;
  //if len == 0 {
    //return false;
  //} else {
    //let goup = ctx.redex.insert(ctx.tid, new_redex(*ctx.host, *ctx.cont, sidxs.len() as u64));
    //for (i, arg_idx) in sidxs.iter().enumerate() {
      //if i < sidxs.len() - 1 {
        //ctx.visit.push(new_visit(get_loc(ctx.term, *arg_idx), goup));
      //} else {
        //*ctx.cont = goup;
        //*ctx.host = get_loc(ctx.term, *arg_idx);
        //return true;
      //}
    //}
    //return true;
  //}
}

#[inline(always)]
pub fn apply(ctx: ReduceCtx, fid: u64, visit: &VisitObj, apply: &ApplyObj) -> bool {
  // Reduces function superpositions
  for (n, is_strict) in visit.strict_map.iter().enumerate() {
    let n = n as u64;
    if *is_strict && get_tag(load_arg(ctx.heap, ctx.term, n)) == SUP {
      superpose(ctx.heap, &ctx.prog.aris, ctx.tid, *ctx.host, ctx.term, load_arg(ctx.heap, ctx.term, n), n);
      return true;
    }
  }

  // For each rule condition vector
  let mut matched;
  for (r, rule) in apply.rules.iter().enumerate() {
    // Check if the rule matches
    matched = true;
    
    // Tests each rule condition (ex: `get_tag(args[0]) == SUCC`)
    for (i, cond) in rule.cond.iter().enumerate() {
      let i = i as u64;
      match get_tag(*cond) {
        U60 => {
          let same_tag = get_tag(load_arg(ctx.heap, ctx.term, i)) == U60;
          let same_val = get_num(load_arg(ctx.heap, ctx.term, i)) == get_num(*cond);
          matched = matched && same_tag && same_val;
        }
        F60 => {
          let same_tag = get_tag(load_arg(ctx.heap, ctx.term, i)) == F60;
          let same_val = get_num(load_arg(ctx.heap, ctx.term, i)) == get_num(*cond);
          matched = matched && same_tag && same_val;
        }
        CTR => {
          let same_tag = get_tag(load_arg(ctx.heap, ctx.term, i)) == CTR;
          let same_ext = get_ext(load_arg(ctx.heap, ctx.term, i)) == get_ext(*cond);
          matched = matched && same_tag && same_ext;
        }
        VAR => {
          // If this is a strict argument, then we're in a default variable
          if unsafe { *visit.strict_map.get_unchecked(i as usize) } {

            // This is a Kind2-specific optimization.
            if rule.hoas && r != apply.rules.len() - 1 {

              // Matches number literals
              let is_num
                =  get_tag(load_arg(ctx.heap, ctx.term, i)) == U60
                || get_tag(load_arg(ctx.heap, ctx.term, i)) == F60;

              // Matches constructor labels
              let is_ctr
                =  get_tag(load_arg(ctx.heap, ctx.term, i)) == CTR
                && arity_of(&ctx.prog.aris, load_arg(ctx.heap, ctx.term, i)) == 0;

              // Matches KIND_ctx.term numbers and constructors
              let is_hoas_ctr_num
                =  get_tag(load_arg(ctx.heap, ctx.term, i)) == CTR
                && get_ext(load_arg(ctx.heap, ctx.term, i)) >= KIND_TERM_CT0
                && get_ext(load_arg(ctx.heap, ctx.term, i)) <= KIND_TERM_F60;

              matched = matched && (is_num || is_ctr || is_hoas_ctr_num);

            // Only match default variables on CTRs and NUMs
            } else {
              let is_ctr = get_tag(load_arg(ctx.heap, ctx.term, i)) == CTR;
              let is_u60 = get_tag(load_arg(ctx.heap, ctx.term, i)) == U60;
              let is_f60 = get_tag(load_arg(ctx.heap, ctx.term, i)) == F60;
              matched = matched && (is_ctr || is_u60 || is_f60);
            }
          }
        }
        _ => {}
      }
    }

    // If all conditions are satisfied, the rule matched, so we must apply it
    if matched {
      // Increments the gas count
      inc_cost(ctx.heap, ctx.tid);

      // Builds the right-hand side ctx.term
      let done = alloc_body(ctx.heap, ctx.prog, ctx.tid, ctx.term, &rule.vars, &rule.body);

      // Links the *ctx.host location to it
      link(ctx.heap, *ctx.host, done);

      // Collects unused variables
      for var @ RuleVar { param: _, field: _, erase } in rule.vars.iter() {
        if *erase {
          collect(ctx.heap, &ctx.prog.aris, ctx.tid, get_var(ctx.heap, ctx.term, var));
        }
      }

      // free the matched ctrs
      for (i, arity) in &rule.free {
        free(ctx.heap, ctx.tid, get_loc(load_arg(ctx.heap, ctx.term, *i as u64), 0), *arity);
      }
      free(ctx.heap, ctx.tid, get_loc(ctx.term, 0), arity_of(&ctx.prog.aris, fid));

      return true;
    }
  }

  return false;
}

#[inline(always)]
pub fn superpose(heap: &Heap, aris: &Aris, tid: usize, host: u64, term: Ptr, argn: Ptr, n: u64) -> Ptr {
  inc_cost(heap, tid);
  let arit = arity_of(aris, term);
  let func = get_ext(term);
  let fun0 = get_loc(term, 0);
  let fun1 = alloc(heap, tid, arit);
  let par0 = get_loc(argn, 0);
  for i in 0 .. arit {
    if i != n {
      let leti = alloc(heap, tid, 3);
      let argi = take_arg(heap, term, i);
      link(heap, fun0 + i, Dp0(get_ext(argn), leti));
      link(heap, fun1 + i, Dp1(get_ext(argn), leti));
      link(heap, leti + 2, argi);
    } else {
      link(heap, fun0 + i, take_arg(heap, argn, 0));
      link(heap, fun1 + i, take_arg(heap, argn, 1));
    }
  }
  link(heap, par0 + 0, Fun(func, fun0));
  link(heap, par0 + 1, Fun(func, fun1));
  let done = Sup(get_ext(argn), par0);
  link(heap, host, done);
  done
}