From 123d64bb5ae7127f6a51cbf44b63341de001a187 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 --- ocaml/Makefile | 2 +- ocaml/lambda4.ml | 2 +- ocaml/num.ml | 22 ---------------------- ocaml/num.mli | 1 - ocaml/parser.ml | 44 ++++++++++++++++++++++++++++++++++---------- ocaml/parser.mli | 13 +++++++------ 6 files changed, 43 insertions(+), 41 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 ed43936..b0e4bc9 100644 --- a/ocaml/lambda4.ml +++ b/ocaml/lambda4.ml @@ -790,7 +790,7 @@ let append_zero = let problem_of ~div ~conv ~nums = let all_tms = (match div with None -> [] | Some div -> [div]) @ nums @ conv in - let all_tms, var_names = parse' all_tms 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 82c4b38..d9cdf37 100644 --- a/ocaml/num.ml +++ b/ocaml/num.ml @@ -266,28 +266,6 @@ prerr_endline ("subst l:" ^ string_of_int l ^ " delift_by_one:" ^ string_of_bool (************ Parsing ************************************) -let parse' strs = - let fix_arity = function - | `I((n,_),args) -> `I((n,1+Listx.length args),args) - | _ -> assert false in - let (tms, free) = Parser.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 `Bottom - else if v = lev + n_pac then `Pacman - else if v = lev + n_bomb then `Lam(true, `Bottom) - else `Var(v,1) in (* 1 by default when variable not applied *) - (* Fix arity *) - let rec aux lev = function - | Parser.Lam t -> `Lam (true, aux (lev+1) t) - | Parser.App (t1, t2) -> fix_arity (mk_app (aux lev t1) (aux lev t2)) - | Parser.Var v -> fix lev v in - List.map (aux 0) tms, free -;; - (************** Algorithm(s) ************************) let eta_compare x y = diff --git a/ocaml/num.mli b/ocaml/num.mli index 6de2645..33ea10f 100644 --- a/ocaml/num.mli +++ b/ocaml/num.mli @@ -34,7 +34,6 @@ val mk_appl : nf -> nf list -> nf val mk_appx : nf -> nf Listx.listx -> nf val mk_match : nf -> 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..d7a1b36 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,33 @@ 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 `Bottom + else if v = lev + n_pac then `Pacman + else if v = lev + n_bomb then `Lam(true, `Bottom) + else `Var(v,1) in (* 1 by default when variable not applied *) + (* Fix arity *) + let open Num in + let exclude_bottom = function + | #nf_nob as t -> t + | `Bottom -> raise (ParsingError "Input term not in normal form") in + let rec aux_nob lev : nf_nob -> nf = function + | `I((n,_), args) -> `I((n,1 + Listx.length args), Listx.map (fun t -> exclude_bottom (aux_nob lev t)) args) + | `Var(n,_) -> fix lev n + | `Lam(_,t) -> `Lam (true, aux (lev+1) t) + | `Match _ | `N _ -> assert false + | `Pacman -> assert false + and aux lev : Num.nf -> Num.nf = function + | #nf_nob as t -> aux_nob lev t + | `Bottom -> 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