From 8392da1be43d50073e2d51bae917dcc570431a78 Mon Sep 17 00:00:00 2001 From: acondolu Date: Wed, 12 Jul 2017 18:52:57 +0200 Subject: [PATCH] Added second problem with bombs and pacmans: it works! --- ocaml/lambda4.ml | 10 +++++++++- ocaml/problems.ml | 7 ++----- 2 files changed, 11 insertions(+), 6 deletions(-) diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml index 927cfe6..8f080d5 100644 --- a/ocaml/lambda4.ml +++ b/ocaml/lambda4.ml @@ -147,6 +147,14 @@ let super_simplify ({div; ps; conv} as p) = List.hd divs) div in {p with div=option_map cast_to_i_var div; ps=List.map cast_to_i_n_var ps; conv=List.map cast_to_i_n_var conv} +let cast_to_ps = + function + #i_num_var as y -> (y : i_num_var) + | `Bottom | `Pacman -> raise (Backtrack "foo") + | t -> + prerr_endline (print (t :> nf)); + assert false (* algorithm failed *) + let subst_in_problem x inst ({freshno; div; conv; ps; sigma} as p) = let len_ps = List.length ps in (*(let l = Array.to_list (Array.init (freshno + 1) string_of_var) in @@ -195,7 +203,7 @@ prerr_endline ("# INST0: " ^ string_of_var x ^ " := " ^ print ~l inst));*) match u with | `N i -> acc_new_ps,i | _ -> - let ps = List.map (fun t -> cast_to_i_num_var (subst false false x inst (t:> nf))) (acc_ps@acc_new_ps) in + let ps = List.map (fun t -> cast_to_ps (subst false false x inst (t:> nf))) (acc_ps@acc_new_ps) in let super_simplified_ps = super_simplify_ps ps ps in (*prerr_endline ("CERCO u:" ^ print (fst u :> nf)); List.iter (fun x -> prerr_endline ("IN: " ^ print (fst x :> nf))) ps; diff --git a/ocaml/problems.ml b/ocaml/problems.ml index 15fe980..b604231 100644 --- a/ocaml/problems.ml +++ b/ocaml/problems.ml @@ -336,13 +336,10 @@ let n3 () = magic_conv (* ************************************************************************** *) -(* let o1 () = magic_conv (Some"BOT") [] [] ["*"];; *) - -let o1 () = magic_conv None [] ["x BOT"] ["*"];; - let o1 () = magic_conv None [] ["x a b"; "x (_. BOT) c"] ["*"];; +let o2 () = magic_conv None [] ["x (y (_. BOT) a) c"; "x (y a PAC) d"] ["*"];; -main [o1() ];; +main [o1() ; o2() ];; (* main ([ p2 ; p4 ; p5 ; p6 ; p7 ; p8 ; p9 ; p10 ; p11 ; p12 ; p13 ; -- 2.39.2