From f635df1a27defb6e7c0aa290b4d040a16f748bf2 Mon Sep 17 00:00:00 2001 From: acondolu Date: Thu, 13 Jul 2017 18:52:32 +0200 Subject: [PATCH] return type of simplify_match improved (no `Match in output) --- ocaml/lambda4.ml | 37 +++++++++++++++++++++++-------------- 1 file changed, 23 insertions(+), 14 deletions(-) diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml index ead0b54..9ed3394 100644 --- a/ocaml/lambda4.ml +++ b/ocaml/lambda4.ml @@ -144,18 +144,22 @@ let fixpoint f = ;; let rec super_simplify_ps ps = + fixpoint (List.map (fun x -> cast_to_i_n_var (simple_expand_match ps (x :> i_num_var)))) +;; + +let rec super_simplify_ps_with_match ps = fixpoint (List.map (cast_to_i_num_var ++ (simple_expand_match ps))) ;; let super_simplify ({div; ps; conv} as p) = - let ps = super_simplify_ps p.ps (p.ps :> i_num_var list) in - let conv = super_simplify_ps ps (p.conv :> i_num_var list) in + let ps = super_simplify_ps p.ps p.ps in + let conv = super_simplify_ps ps p.conv in let div = option_map (fun div -> - let divs = super_simplify_ps p.ps ([div] :> i_num_var list) in + let divs = super_simplify_ps p.ps ([div] :> i_n_var list) in 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 = +let cast_to_ps_with_match = function #i_num_var as y -> (y : i_num_var) | `Bottom | `Pacman -> raise (Backtrack "BOT/PAC in ps") @@ -201,12 +205,17 @@ prerr_endline ("# INST0: " ^ string_of_var x ^ " := " ^ print ~l inst));*) function | None -> freshno, None, acc_new_ps | Some t -> + let t = subst false false x inst (t :> nf) in try - let t = subst false false x inst (t :> nf) in let freshno,new_t,acc_new_ps = expand_match (freshno,ps,acc_new_ps) t in - freshno,Some(cast_to_i_var new_t),acc_new_ps - with Bottom -> freshno, None, acc_new_ps - | Pacman -> raise (Backtrack "Pacman in div") + (* backtrack if it is a number or a variable *) + match new_t with + | `N _ -> raise (Backtrack "div=`N") + | `Var _ + | `I _ as new_t -> freshno, Some(new_t), acc_new_ps + with + | Bottom -> freshno, None, acc_new_ps + | Pacman -> raise (Backtrack "div=PAC") and expand_match ((freshno,acc_ps,acc_new_ps) as acc) t = match t with @@ -216,12 +225,12 @@ 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_ps (subst false false x inst (t:> nf))) (acc_ps@acc_new_ps) in - let super_simplified_ps = super_simplify_ps ps ps in + let ps = List.map (fun t -> cast_to_ps_with_match (subst false false x inst (t:> nf))) (acc_ps@acc_new_ps) in + let super_simplified_ps = super_simplify_ps_with_match ps ps in (*prerr_endline ("CERCO u:" ^ print (fst u :> nf)); List.iter (fun x -> prerr_endline ("IN: " ^ print (fst x :> nf))) ps; List.iter (fun x -> prerr_endline ("IN2: " ^ print (fst x :> nf))) super_simplified_ps;*) - match index_of_opt ~eq:eta_eq super_simplified_ps u with + match index_of_opt ~eq:eta_eq super_simplified_ps (u :> i_num_var) with Some i -> acc_new_ps, i | None -> acc_new_ps@[u], len_ps + List.length acc_new_ps in @@ -241,10 +250,10 @@ List.iter (fun x -> prerr_endline ("IN2: " ^ print (fst x :> nf))) super_simplif | `Pacman -> raise Pacman | #i_n_var as x -> let x = simple_expand_match (acc_ps@acc_new_ps) x in - freshno,cast_to_i_num_var x,acc_new_ps in + freshno,cast_to_i_n_var x,acc_new_ps in - let freshno,old_ps,new_ps = aux_ps (freshno,[],[]) (ps :> i_num_var list) in - let freshno,conv,new_ps = aux_conv old_ps (freshno,[],new_ps) (conv :> i_num_var list) in + let freshno,old_ps,new_ps = aux_ps (freshno,[],[]) ps in + let freshno,conv,new_ps = aux_conv old_ps (freshno,[],new_ps) conv in let freshno,div,new_ps = aux_div old_ps (freshno,new_ps) (div :> i_num_var option) in let ps = List.map cast_to_i_n_var (old_ps @ new_ps) in -- 2.39.2