]> matita.cs.unibo.it Git - fireball-separation.git/commitdiff
Removed traces of lambda3
author <andrea.condoluci@unibo.it> <>
Mon, 26 Jun 2017 09:37:07 +0000 (11:37 +0200)
committer <andrea.condoluci@unibo.it> <>
Mon, 26 Jun 2017 09:37:07 +0000 (11:37 +0200)
ocaml/discriminator.mli [deleted file]
ocaml/lambda4.ml
ocaml/lambda4.mli
ocaml/problems.ml
ocaml/test.ml

diff --git a/ocaml/discriminator.mli b/ocaml/discriminator.mli
deleted file mode 100644 (file)
index 44ba167..0000000
+++ /dev/null
@@ -1,6 +0,0 @@
-module type Discriminator = sig\r
-  type t\r
-  val magic: string list -> string list -> t\r
-  val magic_conv: div:(string option) -> conv:string list -> nums:string list -> string list -> t\r
-  val main: t list -> unit\r
-end\r
index 25b951a7e2a281714edf11c8986fbc9940dad377..3e9f1ef81c9e27fb96f7693baeb71c9b3da7b887 100644 (file)
@@ -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
index cbaf41c156e18d681b2c88de791812046f44347f..c8a571ea825781a0e9db687b3c9c8e868cf54270 100644 (file)
@@ -1 +1,4 @@
-include Discriminator.Discriminator\r
+type t\r
+val magic: string list -> string list -> t\r
+val magic_conv: div:(string option) -> conv:string list -> nums:string list -> string list -> t\r
+val main: t list -> unit\r
index bf1b67a0942bb9093cdf9be4343195269ea72f94..a0ff4536266a0739e760845589d1a8e643c57a36 100644 (file)
@@ -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 ;
index ed41f7ac684c6188b18fc25c84620fdae340939e..93240b9c867f897050b11bb3805c6cbb7f6a941d 100644 (file)
@@ -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