From 2c278a1d49aa0db5211821c1c9eec27212e5e53c Mon Sep 17 00:00:00 2001 From: acondolu Date: Fri, 14 Jul 2017 16:44:15 +0200 Subject: [PATCH] Moved parse' from Num to Parser (cherry picked from commit 123d64bb5ae7127f6a51cbf44b63341de001a187) --- ocaml/Makefile | 2 +- ocaml/lambda4.ml | 4 ++-- ocaml/num.ml | 14 -------------- ocaml/num.mli | 1 - ocaml/parser.ml | 37 +++++++++++++++++++++++++++---------- ocaml/parser.mli | 13 +++++++------ 6 files changed, 37 insertions(+), 34 deletions(-) diff --git a/ocaml/Makefile b/ocaml/Makefile index 198855f..430f159 100644 --- a/ocaml/Makefile +++ b/ocaml/Makefile @@ -1,6 +1,6 @@ OCAMLC = ocamlopt -g -rectypes LIB = unix.cmxa str.cmxa -UTILS = util.cmx parser.cmx console.cmx listx.cmx pure.cmx num.cmx +UTILS = util.cmx console.cmx listx.cmx pure.cmx num.cmx parser.cmx all: a.out test4.out # test.out diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml index c79cade..355380e 100644 --- a/ocaml/lambda4.ml +++ b/ocaml/lambda4.ml @@ -751,8 +751,8 @@ let append_zero = ;; let problem_of ~div ~conv ~nums = - let all_tms = (match div with None -> [] | Some div -> print_endline(div);[div]) @ nums @ conv in - let all_tms, var_names = parse' all_tms in + let all_tms = (match div with None -> [] | Some div -> [div]) @ nums @ conv in + let all_tms, var_names = Parser.parse' all_tms in let div, (tms, conv) = match div with | None -> None, list_cut (List.length nums, all_tms) | Some _ -> Some (List.hd all_tms), list_cut (List.length nums, List.tl all_tms) in diff --git a/ocaml/num.ml b/ocaml/num.ml index c88fa8d..f612def 100644 --- a/ocaml/num.ml +++ b/ocaml/num.ml @@ -239,20 +239,6 @@ prerr_endline ("subst l:" ^ string_of_int l ^ " delift_by_one:" ^ string_of_bool aux 0 where ;; -(************ Parsing ************************************) - -let parse' strs = - let fix_arity = function - | `I((n,_),args) -> `I((n,1+Listx.length args),args) - | _ -> assert false in - let rec aux = function - | Parser.Lam t -> `Lam (true, aux t) - | Parser.App (t1, t2) -> fix_arity (mk_app (aux t1) (aux t2)) - | Parser.Var v -> `Var(v,1) in - let (tms, free) = Parser.parse_many strs in - List.map aux tms, free -;; - (************** Algorithm(s) ************************) let eta_compare x y = diff --git a/ocaml/num.mli b/ocaml/num.mli index 9cf81cc..c7b3256 100644 --- a/ocaml/num.mli +++ b/ocaml/num.mli @@ -40,7 +40,6 @@ val mk_appl : nf -> nf list -> nf val mk_appx : nf -> nf Listx.listx -> nf val mk_match : nf i_num_var_ -> var -> int -> (int * nf) list ref -> nf list -> nf val subst : bool -> bool -> int -> nf -> nf -> nf -val parse' : string list -> nf list * string list val eta_compare : nf -> nf -> int val eta_eq : [< nf ] -> [< nf ] -> bool val eta_subterm : [< nf ] -> [< nf ] -> bool diff --git a/ocaml/parser.ml b/ocaml/parser.ml index b496070..d21f4c2 100644 --- a/ocaml/parser.ml +++ b/ocaml/parser.ml @@ -1,15 +1,9 @@ -type term = - | Var of int - | App of term * term - | Lam of term -;; - -let mk_app x y = App(x, y);; -let mk_lam x = Lam x;; -let mk_var x = Var x;; - exception ParsingError of string;; +let mk_app x y = Num.mk_app x y;; +let mk_lam x = `Lam(true, x);; +let mk_var x = `Var(x, -666);; + let isAlphaNum c = let n = Char.code c in (48 <= n && n <= 90) || (95 <= n && n <= 122) ;; let isSpace c = c = ' ' || c = '\n' || c = '\t' ;; @@ -147,3 +141,26 @@ let _ = prerr_endline (">>>" ^ string_of_term (parse "(\\x. x y z z1 k) z1 z j") **********************************************************************) + + let parse' strs = + let (tms, free) = parse_many strs in + (* Replace pacmans and bottoms *) + let n_bot = try Util.index_of "BOT" free with Not_found -> min_int in + let n_pac = try Util.index_of "PAC" free with Not_found -> min_int in + let n_bomb = try Util.index_of "BOMB" free with Not_found -> min_int in + let fix lev v = + if v = lev + n_bot then failwith "Example with `Bottom" + else if v = lev + n_pac then failwith "Example with `Pacman" + else if v = lev + n_bomb then failwith "Example with `Bomb" + else `Var(v,1) in (* 1 by default when variable not applied *) + (* Fix arity *) + let open Num in + let rec aux lev : nf -> nf = function + | `I((n,_), args) -> `I((n,1 + Listx.length args), Listx.map (fun t -> aux lev t) args) + | `Var(n,_) -> fix lev n + | `Lam(_,t) -> `Lam (true, aux (lev+1) t) + | `Match _ | `N _ -> assert false in + List.map (aux 0) (tms :> Num.nf list), free +;; + +let parse_problem s = failwith "TODO"; diff --git a/ocaml/parser.mli b/ocaml/parser.mli index c073c3a..c205cb2 100644 --- a/ocaml/parser.mli +++ b/ocaml/parser.mli @@ -1,9 +1,10 @@ -type term = - | Var of int - | App of term * term - | Lam of term +exception ParsingError of string (* parses a string to a term *) -val parse: string -> term +(* val parse: string -> Num.nf *) (* parse many strings/terms, and returns the list of parsed terms + the list of free variables; variable 0 is not used *) -val parse_many: string list -> term list * string list +val parse_many: string list -> Num.nf list * string list +val parse': string list -> Num.nf list * string list +val parse_problem: + string -> + Num.i_var option * Num.i_n_var list * Num.i_n_var list -- 2.39.2