From:  <andrea.condoluci@unibo.it>
Date: Mon, 26 Jun 2017 09:37:07 +0000 (+0200)
Subject: Removed traces of lambda3
X-Git-Tag: weak-reduction-separation~75
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b609e8cfc37360748de4fcbc4e80bba556fadc87;p=fireball-separation.git

Removed traces of lambda3
---

diff --git a/ocaml/discriminator.mli b/ocaml/discriminator.mli
deleted file mode 100644
index 44ba167..0000000
--- a/ocaml/discriminator.mli
+++ /dev/null
@@ -1,6 +0,0 @@
-module type Discriminator = sig
-  type t
-  val magic: string list -> string list -> t
-  val magic_conv: div:(string option) -> conv:string list -> nums:string list -> string list -> t
-  val main: t list -> unit
-end
diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 25b951a..3e9f1ef 100644
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -453,8 +453,8 @@ let instantiate p x n =
  let zero = Listx.Nil zero in
  let args = if n = 0 then zero else Listx.append zero (Listx.from_list vars) in
  let bs = ref [] in
- let arity1 = (assert false; -666) in
- let arity2 = (assert false; -666) in
+ let arity1 = (*assert false; -666*) 0 in
+ let arity2 = (*assert false; -666*) 0 in
  let inst = `Lam(false,arity1,`Match(`I(0,Listx.map (lift 1) args),arity2,1,bs,[])) in
  let p = {p with deltas=bs::p.deltas} in
  subst_in_problem x inst p
diff --git a/ocaml/lambda4.mli b/ocaml/lambda4.mli
index cbaf41c..c8a571e 100644
--- a/ocaml/lambda4.mli
+++ b/ocaml/lambda4.mli
@@ -1 +1,4 @@
-include Discriminator.Discriminator
+type t
+val magic: string list -> string list -> t
+val magic_conv: div:(string option) -> conv:string list -> nums:string list -> string list -> t
+val main: t list -> unit
diff --git a/ocaml/problems.ml b/ocaml/problems.ml
index bf1b67a..a0ff453 100644
--- a/ocaml/problems.ml
+++ b/ocaml/problems.ml
@@ -1,8 +1,4 @@
-let use_lambda3 = Array.length Sys.argv = 1;;
-
-let discriminator = ( module Lambda4 : Discriminator.Discriminator );;
-module Pippo = (val discriminator);;
-open Pippo;;
+open Lambda4;;
 
 let p2 = magic [ "x y"; "x z" ; "x (y z)"] ["*"]
 
@@ -292,7 +288,7 @@ let m2 () = magic_conv None []
 main ([
  (* p2 ; p4 ; p5 ; p6 ; p7 ; p8 ; p9 ; p10 ; p11 ; p12 ; p13 ; p14 ; p15 ; p16 ; p17 ; p18 ; p19 ; p20 ; p21 ; p22 ; p23 ; p24 ; p25 ; p26 ; p27 ; p28 ; p29 ; p30 ; p31 ; p32 ; p33 ; p34 ; p35 ; p36 ; p37 ; *)
  p24 ; p25 ;
-] @ if use_lambda3 then [] else List.map ((|>) ()) [
+] @ List.map ((|>) ()) [
  q1 ; q2; q3; q4 ; q5 ; q6 ;
  (* q7 ; *)
  q8 ;
diff --git a/ocaml/test.ml b/ocaml/test.ml
index ed41f7a..93240b9 100644
--- a/ocaml/test.ml
+++ b/ocaml/test.ml
@@ -1,13 +1,4 @@
-let three = Array.length Sys.argv = 1;;
-
-let discriminator =
- (* if three *)
- (* then (module Lambda3 : Discriminator.Discriminator) *)
- (* else *)
- (module Lambda4 : Discriminator.Discriminator);;
-
-module Pippo = (val discriminator);;
-open Pippo;;
+open Lambda4;;
 
 let acaso l =
     let n = Random.int (List.length l) in