hvm_edu.ml

type term =
  | APP of term * term
  | VAR of var
  | FST of dup
  | SND of dup
  | SUP of term * term
  | LAM of var * term
  | NIL

and var = { mutable var : term }
and dup = { mutable fst_and_init : term; mutable snd_and_tag : term }

let itr = ref 0
let inc_itr () = incr itr

let rec reduce stack term =
  match (term, stack) with
  | APP (fun_, arg), stack ->
      let stack = `app arg :: stack in
      reduce stack fun_
  | FST dup, stack when dup.snd_and_tag = NIL ->
      let stack = `fst dup :: stack in
      reduce stack dup.fst_and_init
  | SND dup, stack when dup.snd_and_tag = NIL ->
      let stack = `snd dup :: stack in
      reduce stack dup.fst_and_init
  | FST dup, stack -> reduce stack dup.fst_and_init
  | SND dup, stack -> reduce stack dup.snd_and_tag
  | VAR ref, stack when ref.var = NIL ->
      (* TODO: this is incomplete, but the original is wrong *)
      assert (stack = []);
      term
  | VAR ref, stack -> reduce stack ref.var
  | LAM (ref, body), `app arg :: stack ->
      inc_itr ();
      ref.var <- arg;
      reduce stack body
  | SUP (fst, snd), `app arg :: stack ->
      inc_itr ();
      let data = { fst_and_init = arg; snd_and_tag = NIL } in
      let ap0 = APP (fst, FST data) in
      let ap1 = APP (snd, SND data) in
      let term = SUP (ap0, ap1) in
      reduce stack term
  | LAM (ref, body), ((`fst dup | `snd dup) as proj) :: stack ->
      inc_itr ();
      let node = { fst_and_init = body; snd_and_tag = NIL } in
      let lm0 = { var = NIL } in
      let fst = LAM (lm0, FST node) in
      let lm1 = { var = NIL } in
      let snd = LAM (lm1, SND node) in
      (* shared *)
      dup.fst_and_init <- fst;
      dup.snd_and_tag <- snd;
      ref.var <- SUP (VAR lm0, VAR lm1);
      let term = match proj with `fst _ -> fst | `snd _ -> snd in
      reduce stack term
  | SUP (fst, snd), ((`fst dup | `snd dup) as proj) :: stack ->
      inc_itr ();
      dup.fst_and_init <- fst;
      dup.snd_and_tag <- snd;
      let term = match proj with `fst _ -> fst | `snd _ -> snd in
      reduce stack term
  | (LAM _ | SUP _), [] -> term
  | NIL, _ -> failwith "unrecheable"

let rec normal term =
  let wnf = reduce [] term in
  match wnf with
  | VAR _ -> ()
  | LAM (var, body) ->
      (* TODO: what about lam.left? *)
      normal body
  | SUP (fst, snd) ->
      normal fst;
      normal snd
  | APP _ | FST _ | SND _ -> failwith "unreacheable, normal"
  | NIL -> failwith "unreacheable, normal, nil"

let demo =
  let rec t_0 = APP (t_1, t_2)
  and t_1 = APP (t_3, t_4)
  and v_237 = { var = NIL }
  and t_2 = LAM (v_237, t_238)
  and v_5 = { var = NIL }
  and t_3 = LAM (v_5, t_6)
  and v_223 = { var = NIL }
  and t_4 = LAM (v_223, t_224)
  and v_217 = { var = NIL }
  and t_6 = LAM (v_217, t_218)
  and t_9 = VAR v_5
  and v_13 = { var = NIL }
  and t_12 = LAM (v_13, t_14)
  and t_14 = APP (t_15, t_16)
  and t_15 = FST p_7
  and t_16 = APP (t_17, t_18)
  and t_17 = SND p_7
  and t_18 = VAR v_13
  and v_22 = { var = NIL }
  and t_21 = LAM (v_22, t_23)
  and t_23 = APP (t_24, t_25)
  and t_24 = FST p_10
  and t_25 = APP (t_26, t_27)
  and t_26 = SND p_10
  and t_27 = VAR v_22
  and v_31 = { var = NIL }
  and t_30 = LAM (v_31, t_32)
  and t_32 = APP (t_33, t_34)
  and t_33 = FST p_19
  and t_34 = APP (t_35, t_36)
  and t_35 = SND p_19
  and t_36 = VAR v_31
  and v_40 = { var = NIL }
  and t_39 = LAM (v_40, t_41)
  and t_41 = APP (t_42, t_43)
  and t_42 = FST p_28
  and t_43 = APP (t_44, t_45)
  and t_44 = SND p_28
  and t_45 = VAR v_40
  and v_49 = { var = NIL }
  and t_48 = LAM (v_49, t_50)
  and t_50 = APP (t_51, t_52)
  and t_51 = FST p_37
  and t_52 = APP (t_53, t_54)
  and t_53 = SND p_37
  and t_54 = VAR v_49
  and v_58 = { var = NIL }
  and t_57 = LAM (v_58, t_59)
  and t_59 = APP (t_60, t_61)
  and t_60 = FST p_46
  and t_61 = APP (t_62, t_63)
  and t_62 = SND p_46
  and t_63 = VAR v_58
  and v_67 = { var = NIL }
  and t_66 = LAM (v_67, t_68)
  and t_68 = APP (t_69, t_70)
  and t_69 = FST p_55
  and t_70 = APP (t_71, t_72)
  and t_71 = SND p_55
  and t_72 = VAR v_67
  and v_76 = { var = NIL }
  and t_75 = LAM (v_76, t_77)
  and t_77 = APP (t_78, t_79)
  and t_78 = FST p_64
  and t_79 = APP (t_80, t_81)
  and t_80 = SND p_64
  and t_81 = VAR v_76
  and v_85 = { var = NIL }
  and t_84 = LAM (v_85, t_86)
  and t_86 = APP (t_87, t_88)
  and t_87 = FST p_73
  and t_88 = APP (t_89, t_90)
  and t_89 = SND p_73
  and t_90 = VAR v_85
  and v_94 = { var = NIL }
  and t_93 = LAM (v_94, t_95)
  and t_95 = APP (t_96, t_97)
  and t_96 = FST p_82
  and t_97 = APP (t_98, t_99)
  and t_98 = SND p_82
  and t_99 = VAR v_94
  and v_103 = { var = NIL }
  and t_102 = LAM (v_103, t_104)
  and t_104 = APP (t_105, t_106)
  and t_105 = FST p_91
  and t_106 = APP (t_107, t_108)
  and t_107 = SND p_91
  and t_108 = VAR v_103
  and v_112 = { var = NIL }
  and t_111 = LAM (v_112, t_113)
  and t_113 = APP (t_114, t_115)
  and t_114 = FST p_100
  and t_115 = APP (t_116, t_117)
  and t_116 = SND p_100
  and t_117 = VAR v_112
  and v_121 = { var = NIL }
  and t_120 = LAM (v_121, t_122)
  and t_122 = APP (t_123, t_124)
  and t_123 = FST p_109
  and t_124 = APP (t_125, t_126)
  and t_125 = SND p_109
  and t_126 = VAR v_121
  and v_130 = { var = NIL }
  and t_129 = LAM (v_130, t_131)
  and t_131 = APP (t_132, t_133)
  and t_132 = FST p_118
  and t_133 = APP (t_134, t_135)
  and t_134 = SND p_118
  and t_135 = VAR v_130
  and v_139 = { var = NIL }
  and t_138 = LAM (v_139, t_140)
  and t_140 = APP (t_141, t_142)
  and t_141 = FST p_127
  and t_142 = APP (t_143, t_144)
  and t_143 = SND p_127
  and t_144 = VAR v_139
  and v_148 = { var = NIL }
  and t_147 = LAM (v_148, t_149)
  and t_149 = APP (t_150, t_151)
  and t_150 = FST p_136
  and t_151 = APP (t_152, t_153)
  and t_152 = SND p_136
  and t_153 = VAR v_148
  and v_157 = { var = NIL }
  and t_156 = LAM (v_157, t_158)
  and t_158 = APP (t_159, t_160)
  and t_159 = FST p_145
  and t_160 = APP (t_161, t_162)
  and t_161 = SND p_145
  and t_162 = VAR v_157
  and v_166 = { var = NIL }
  and t_165 = LAM (v_166, t_167)
  and t_167 = APP (t_168, t_169)
  and t_168 = FST p_154
  and t_169 = APP (t_170, t_171)
  and t_170 = SND p_154
  and t_171 = VAR v_166
  and v_175 = { var = NIL }
  and t_174 = LAM (v_175, t_176)
  and t_176 = APP (t_177, t_178)
  and t_177 = FST p_163
  and t_178 = APP (t_179, t_180)
  and t_179 = SND p_163
  and t_180 = VAR v_175
  and v_184 = { var = NIL }
  and t_183 = LAM (v_184, t_185)
  and t_185 = APP (t_186, t_187)
  and t_186 = FST p_172
  and t_187 = APP (t_188, t_189)
  and t_188 = SND p_172
  and t_189 = VAR v_184
  and v_193 = { var = NIL }
  and t_192 = LAM (v_193, t_194)
  and t_194 = APP (t_195, t_196)
  and t_195 = FST p_181
  and t_196 = APP (t_197, t_198)
  and t_197 = SND p_181
  and t_198 = VAR v_193
  and v_202 = { var = NIL }
  and t_201 = LAM (v_202, t_203)
  and t_203 = APP (t_204, t_205)
  and t_204 = FST p_190
  and t_205 = APP (t_206, t_207)
  and t_206 = SND p_190
  and t_207 = VAR v_202
  and v_211 = { var = NIL }
  and t_210 = LAM (v_211, t_212)
  and t_212 = APP (t_213, t_214)
  and t_213 = FST p_199
  and t_214 = APP (t_215, t_216)
  and t_215 = SND p_199
  and t_216 = VAR v_211
  and t_218 = APP (t_219, t_220)
  and t_219 = FST p_208
  and t_220 = APP (t_221, t_222)
  and t_221 = SND p_208
  and t_222 = VAR v_217
  and t_224 = APP (t_225, t_226)
  and t_225 = APP (t_227, t_228)
  and v_233 = { var = NIL }
  and t_226 = LAM (v_233, t_234)
  and t_227 = VAR v_223
  and v_229 = { var = NIL }
  and t_228 = LAM (v_229, t_230)
  and v_231 = { var = NIL }
  and t_230 = LAM (v_231, t_232)
  and t_232 = VAR v_231
  and v_235 = { var = NIL }
  and t_234 = LAM (v_235, t_236)
  and t_236 = VAR v_233
  and v_239 = { var = NIL }
  and t_238 = LAM (v_239, t_240)
  and t_240 = VAR v_237
  and p_7 = { fst_and_init = t_9; snd_and_tag = NIL }
  and p_10 = { fst_and_init = t_12; snd_and_tag = NIL }
  and p_19 = { fst_and_init = t_21; snd_and_tag = NIL }
  and p_28 = { fst_and_init = t_30; snd_and_tag = NIL }
  and p_37 = { fst_and_init = t_39; snd_and_tag = NIL }
  and p_46 = { fst_and_init = t_48; snd_and_tag = NIL }
  and p_55 = { fst_and_init = t_57; snd_and_tag = NIL }
  and p_64 = { fst_and_init = t_66; snd_and_tag = NIL }
  and p_73 = { fst_and_init = t_75; snd_and_tag = NIL }
  and p_82 = { fst_and_init = t_84; snd_and_tag = NIL }
  and p_91 = { fst_and_init = t_93; snd_and_tag = NIL }
  and p_100 = { fst_and_init = t_102; snd_and_tag = NIL }
  and p_109 = { fst_and_init = t_111; snd_and_tag = NIL }
  and p_118 = { fst_and_init = t_120; snd_and_tag = NIL }
  and p_127 = { fst_and_init = t_129; snd_and_tag = NIL }
  and p_136 = { fst_and_init = t_138; snd_and_tag = NIL }
  and p_145 = { fst_and_init = t_147; snd_and_tag = NIL }
  and p_154 = { fst_and_init = t_156; snd_and_tag = NIL }
  and p_163 = { fst_and_init = t_165; snd_and_tag = NIL }
  and p_172 = { fst_and_init = t_174; snd_and_tag = NIL }
  and p_181 = { fst_and_init = t_183; snd_and_tag = NIL }
  and p_190 = { fst_and_init = t_192; snd_and_tag = NIL }
  and p_199 = { fst_and_init = t_201; snd_and_tag = NIL }
  and p_208 = { fst_and_init = t_210; snd_and_tag = NIL } in
  t_0

let () =
  let _ = normal demo in
  Format.eprintf "Itrs : %d\n" !itr