ic/term/
mod.rs

1#![allow(dead_code)]
2
3mod conversion;
4mod syntax;
5mod views;
6
7pub use self::conversion::*;
8pub use self::syntax::*;
9
10use std::collections::*;
11use inet::*;
12use std;
13
14// Terms of the Interaction Calculus.
15#[derive(Clone, Debug)]
16pub enum Term {
17  // Abstractions
18  Lam {nam: Vec<u8>, typ: Option<Box<Term>>, bod: Box<Term>},                
19
20  // Applications
21  App {fun: Box<Term>, arg: Box<Term>},
22
23  // Superpositions
24  Sup {tag: u32, fst: Box<Term>, snd: Box<Term>},
25
26  // Duplications
27  Dup {tag: u32, fst: Vec<u8>, snd: Vec<u8>, val: Box<Term>, nxt: Box<Term>},
28
29  // Annotations
30  Ann {val: Box<Term>, typ: Box<Term>},
31
32  // Variables
33  Var {nam: Vec<u8>}, 
34
35  // Erasure
36  Set
37}
38
39use self::Term::{*};
40
41// Source code is Ascii-encoded.
42pub type Str = [u8];
43pub type Chr = u8;
44
45// Converts an index to a name
46pub fn index_to_name(idx : u32) -> Vec<Chr> {
47  let mut name = Vec::new();
48  let mut idx = idx;
49  while idx > 0 {
50    idx = idx - 1;
51    name.push((97 + idx % 26) as u8);
52    idx = idx / 26;
53  }
54  return name;
55}
56
57// Converts a name to an index
58pub fn name_to_index(name : &Vec<Chr>) -> u32 {
59  let mut idx : u32 = 0;
60  for byte in name.iter().rev() {
61    idx = (idx * 26) + (*byte as u32 - 97) + 1;
62  }
63  return idx;
64}
65
66// A context is a vector of (name, value) assignments.
67type Context<'a> = Vec<(&'a Str, Option<Term>)>;
68
69// Extends a context with a (name, value) assignments.
70fn extend<'a,'b>(nam : &'a Str, val : Option<Term>, ctx : &'b mut Context<'a>) -> &'b mut Context<'a> {
71  ctx.push((nam,val));
72  ctx
73}
74
75// Removes an assignment from a context.
76fn narrow<'a,'b>(ctx : &'b mut Context<'a>) -> &'b mut Context<'a> {
77  ctx.pop();
78  ctx
79}
80
81pub fn namespace(space : &Vec<u8>, idx : u32, var : &Vec<u8>) -> Vec<u8> {
82  if var != b"*" {
83    let mut nam = space.clone();
84    nam.extend_from_slice(b"/");
85    nam.append(&mut idx.to_string().as_bytes().to_vec());
86    nam.extend_from_slice(b"/");
87    nam.append(&mut var.clone());
88    nam
89  } else {
90    var.clone()
91  }
92}
93
94// Makes a namespaced copy of a term
95pub fn copy(space : &Vec<u8>, idx : u32, term : &Term) -> Term {
96  match term {
97    Lam{nam, typ, bod} => {
98      let nam = namespace(space, idx, nam);
99      let typ = typ.as_ref().map(|typ| Box::new(copy(space, idx, typ)));
100      let bod = Box::new(copy(space, idx, bod));
101      Lam{nam, typ, bod}
102    },
103    App{fun, arg} => {
104      let fun = Box::new(copy(space, idx, fun));
105      let arg = Box::new(copy(space, idx, arg));
106      App{fun, arg}
107    },
108    Sup{tag, fst, snd} => {
109      let tag = *tag;
110      let fst = Box::new(copy(space, idx, fst));
111      let snd = Box::new(copy(space, idx, snd));
112      Sup{tag, fst, snd}
113    },
114    Dup{tag, fst, snd, val, nxt} => {
115      let tag = *tag;
116      let fst = namespace(space, idx, fst);
117      let snd = namespace(space, idx, snd);
118      let val = Box::new(copy(space, idx, val));
119      let nxt = Box::new(copy(space, idx, nxt));
120      Dup{tag, fst, snd, val, nxt}
121    },
122    Ann{val, typ} => {
123      let val = Box::new(copy(space, idx, val));
124      let typ = Box::new(copy(space, idx, typ));
125      Ann{val, typ}
126    },
127    Var{nam} => {
128      let nam = namespace(space, idx, nam);
129      Var{nam}
130    },
131    Set => Set
132  }
133}
134
135// Display macro.
136impl std::fmt::Display for Term {
137  fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
138    write!(f, "{}", String::from_utf8_lossy(&to_string(&self)))
139  }
140}
141
142// Reduces an Interaction Calculus term through Interaction Combinators.
143pub fn normal(term : &Term) -> Term {
144  let mut net : INet = to_net(&term);
145  ::inet::normal(&mut net);
146  from_net(&net)
147}
148
149pub fn normal_with_stats(term : &Term) -> (Term, u32) {
150  let mut net = to_net(&term);
151  ::inet::normal(&mut net);
152  let trm = from_net(&net);
153  (trm, net.rules)
154}
ic/term/mod.rs

ic/term/
mod.rs
