diff options
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 85 |
1 files changed, 45 insertions, 40 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 26bf02aa25..f1506f5f59 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -47,21 +47,17 @@ let default_flags env = let ts = default_transparent_state env in default_flags_of ts -let debug_unification = ref (false) -let () = Goptions.(declare_bool_option { - optdepr = false; - optkey = ["Debug";"Unification"]; - optread = (fun () -> !debug_unification); - optwrite = (fun a -> debug_unification:=a); -}) - -let debug_ho_unification = ref (false) -let () = Goptions.(declare_bool_option { - optdepr = false; - optkey = ["Debug";"HO";"Unification"]; - optread = (fun () -> !debug_ho_unification); - optwrite = (fun a -> debug_ho_unification:=a); -}) +let debug_unification = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Debug";"Unification"] + ~value:false + +let debug_ho_unification = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Debug";"HO";"Unification"] + ~value:false (*******************************************) (* Functions to deal with impossible cases *) @@ -199,7 +195,7 @@ let occur_rigidly flags env evd (evk,_) t = | Evar (evk',l as ev) -> if Evar.equal evk evk' then Rigid true else if is_frozen flags ev then - Rigid (Array.exists (fun x -> rigid_normal_occ (aux x)) l) + Rigid (List.exists (fun x -> rigid_normal_occ (aux x)) l) else Reducible | Cast (p, _, _) -> aux p | Lambda (na, t, b) -> aux b @@ -355,6 +351,14 @@ let ise_array2 evd f v1 v2 = if Int.equal lv1 (Array.length v2) then allrec evd (pred lv1) else UnifFailure (evd,NotSameArgSize) +let rec ise_inst2 evd f l1 l2 = match l1, l2 with +| [], [] -> Success evd +| [], (_ :: _) | (_ :: _), [] -> assert false +| c1 :: l1, c2 :: l2 -> + match ise_inst2 evd f l1 l2 with + | Success evd' -> f evd' c1 c2 + | UnifFailure _ as x -> x + (* Applicative node of stack are read from the outermost to the innermost but are unified the other way. *) let rec ise_app_stack2 env f evd sk1 sk2 = @@ -767,7 +771,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty in let app_empty = match sk1, sk2 with [], [] -> true | _ -> false in (* Evar must be undefined since we have flushed evars *) - let () = if !debug_unification then + let () = if debug_unification () then let open Pp in Feedback.msg_debug (v 0 (pr_state env evd appr1 ++ cut () ++ pr_state env evd appr2 ++ cut ())) in match (flex_kind_of_term flags env evd term1 sk1, @@ -1023,7 +1027,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty if Evar.equal sp1 sp2 then match ise_stack2 false env evd (evar_conv_x flags) sk1 sk2 with |None, Success i' -> - ise_array2 i' (fun i' -> evar_conv_x flags env i' CONV) al1 al2 + ise_inst2 i' (fun i' -> evar_conv_x flags env i' CONV) al1 al2 |_, (UnifFailure _ as x) -> x |Some _, _ -> UnifFailure (evd,NotSameArgSize) else UnifFailure (evd,NotSameHead) @@ -1224,16 +1228,16 @@ let apply_on_subterm env evd fixedref f test c t = (fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c))) applyrec acc t else - (if !debug_ho_unification then + (if debug_ho_unification () then Feedback.msg_debug Pp.(str"Testing " ++ prc env !evdref c ++ str" against " ++ prc env !evdref t); let b, evd = try test env !evdref k c t with e when CErrors.noncritical e -> assert false in - if b then (if !debug_ho_unification then Feedback.msg_debug (Pp.str "succeeded"); + if b then (if debug_ho_unification () then Feedback.msg_debug (Pp.str "succeeded"); let evd', t' = f !evdref k t in evdref := evd'; t') else ( - if !debug_ho_unification then Feedback.msg_debug (Pp.str "failed"); + if debug_ho_unification () then Feedback.msg_debug (Pp.str "failed"); map_constr_with_binders_left_to_right !evdref (fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c))) applyrec acc t)) @@ -1245,6 +1249,7 @@ let filter_possible_projections evd c ty ctxt args = (* Since args in the types will be replaced by holes, we count the fv of args to have a well-typed filter; don't know how necessary it is however to have a well-typed filter here *) + let args = Array.of_list args in let fv1 = free_rels evd (mkApp (c,args)) (* Hack: locally untyped *) in let fv2 = collect_vars evd (mkApp (c,args)) in let len = Array.length args in @@ -1313,8 +1318,8 @@ let thin_evars env sigma sign c = match kind !sigma t with | Evar (ev, args) -> let evi = Evd.find_undefined !sigma ev in - let filter = Array.map (fun c -> Id.Set.subset (collect_vars !sigma c) ctx) args in - let filter = Filter.make (Array.to_list filter) in + let filter = List.map (fun c -> Id.Set.subset (collect_vars !sigma c) ctx) args in + let filter = Filter.make filter in let candidates = Option.map (List.map EConstr.of_constr) (evar_candidates evi) in let evd, ev = restrict_evar !sigma ev filter candidates in sigma := evd; whd_evar !sigma t @@ -1337,12 +1342,12 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = let env_evar = evar_filtered_env env_rhs evi in let sign = named_context_val env_evar in let ctxt = evar_filtered_context evi in - if !debug_ho_unification then + if debug_ho_unification () then (Feedback.msg_debug Pp.(str"env rhs: " ++ Termops.Internal.print_env env_rhs); Feedback.msg_debug Pp.(str"env evars: " ++ Termops.Internal.print_env env_evar)); - let args = Array.map (nf_evar evd) args in + let args = List.map (nf_evar evd) args in let vars = List.map NamedDecl.get_id ctxt in - let argsubst = List.map2 (fun id c -> (id, c)) vars (Array.to_list args) in + let argsubst = List.map2 (fun id c -> (id, c)) vars args in let instance = List.map mkVar vars in let rhs = nf_evar evd rhs in if not (noccur_evar env_rhs evd evk rhs) then raise (TypingFailed evd); @@ -1374,7 +1379,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = let rec set_holes env_rhs evd rhs = function | (id,idty,c,cty,evsref,filter,occs)::subst -> let c = nf_evar evd c in - if !debug_ho_unification then + if debug_ho_unification () then Feedback.msg_debug Pp.(str"set holes for: " ++ prc env_rhs evd (mkVar id.binder_name) ++ spc () ++ prc env_rhs evd c ++ str" in " ++ @@ -1382,7 +1387,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = let occ = ref 1 in let set_var evd k inst = let oc = !occ in - if !debug_ho_unification then + if debug_ho_unification () then (Feedback.msg_debug Pp.(str"Found one occurrence"); Feedback.msg_debug Pp.(str"cty: " ++ prc env_rhs evd c)); incr occ; @@ -1393,7 +1398,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = | Unspecified prefer_abstraction -> let evd, evty = set_holes env_rhs evd cty subst in let evty = nf_evar evd evty in - if !debug_ho_unification then + if debug_ho_unification () then Feedback.msg_debug Pp.(str"abstracting one occurrence " ++ prc env_rhs evd inst ++ str" of type: " ++ prc env_evar evd evty ++ str " for " ++ prc env_rhs evd c); @@ -1413,21 +1418,21 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = evd, ev in let evd, rhs' = apply_on_subterm env_rhs evd fixed set_var test c rhs in - if !debug_ho_unification then + if debug_ho_unification () then Feedback.msg_debug Pp.(str"abstracted: " ++ prc env_rhs evd rhs'); let () = check_selected_occs env_rhs evd c !occ occs in let env_rhs' = push_named (NamedDecl.LocalAssum (id,idty)) env_rhs in set_holes env_rhs' evd rhs' subst | [] -> evd, rhs in - let subst = make_subst (ctxt,Array.to_list args,argoccs) in + let subst = make_subst (ctxt,args,argoccs) in let evd, rhs' = set_holes env_rhs evd rhs subst in let rhs' = nf_evar evd rhs' in (* Thin evars making the term typable in env_evar *) let evd, rhs' = thin_evars env_evar evd ctxt rhs' in (* We instantiate the evars of which the value is forced by typing *) - if !debug_ho_unification then + if debug_ho_unification () then (Feedback.msg_debug Pp.(str"solve_evars on: " ++ prc env_evar evd rhs'); Feedback.msg_debug Pp.(str"evars: " ++ pr_evar_map (Some 0) env_evar evd)); let evd,rhs' = @@ -1437,7 +1442,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = raise (TypingFailed evd) in let rhs' = nf_evar evd rhs' in (* We instantiate the evars of which the value is forced by typing *) - if !debug_ho_unification then + if debug_ho_unification () then (Feedback.msg_debug Pp.(str"after solve_evars: " ++ prc env_evar evd rhs'); Feedback.msg_debug Pp.(str"evars: " ++ pr_evar_map (Some 0) env_evar evd)); @@ -1445,7 +1450,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = | (id,idty,c,cty,evsref,_,_)::l -> let id = id.binder_name in let c = nf_evar evd c in - if !debug_ho_unification then + if debug_ho_unification () then Feedback.msg_debug Pp.(str"abstracting: " ++ prc env_rhs evd (mkVar id) ++ spc () ++ prc env_rhs evd c); @@ -1476,7 +1481,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = | _ -> evd) with e -> user_err (Pp.str "Cannot find an instance") else - ((if !debug_ho_unification then + ((if debug_ho_unification () then let evi = Evd.find evd evk in let env = Evd.evar_env env_rhs evi in Feedback.msg_debug Pp.(str"evar is defined: " ++ @@ -1491,7 +1496,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = if Evd.is_defined evd evk then (* Can happen due to dependencies: instantiating evars in the arguments of evk might instantiate evk itself. *) - (if !debug_ho_unification then + (if debug_ho_unification () then begin let evi = Evd.find evd evk in let evenv = evar_env env_rhs evi in @@ -1504,13 +1509,13 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = let evi = Evd.find_undefined evd evk in let evenv = evar_env env_rhs evi in let rhs' = nf_evar evd rhs' in - if !debug_ho_unification then + if debug_ho_unification () then Feedback.msg_debug Pp.(str"abstracted type before second solve_evars: " ++ prc evenv evd rhs'); (* solve_evars is not commuting with nf_evar, because restricting an evar might provide a more specific type. *) let evd, _ = !solve_evars evenv evd rhs' in - if !debug_ho_unification then + if debug_ho_unification () then Feedback.msg_debug Pp.(str"abstracted type: " ++ prc evenv evd (nf_evar evd rhs')); let flags = default_flags_of TransparentState.full in Evarsolve.instantiate_evar evar_unify flags env_rhs evd evk rhs' @@ -1537,7 +1542,7 @@ let default_evar_selection flags evd (ev,args) = in spec :: aux args abs | l, [] -> List.map (fun _ -> default_occurrence_selection) l | [], _ :: _ -> assert false - in aux (Array.to_list args) evi.evar_abstract_arguments + in aux args evi.evar_abstract_arguments let second_order_matching_with_args flags env evd with_ho pbty ev l t = if with_ho then @@ -1564,7 +1569,7 @@ let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 = let t2 = apprec_nohdbeta flags env evd (whd_head_evar evd t2) in let (term1,l1 as appr1) = try destApp evd t1 with DestKO -> (t1, [||]) in let (term2,l2 as appr2) = try destApp evd t2 with DestKO -> (t2, [||]) in - let () = if !debug_unification then + let () = if debug_unification () then let open Pp in Feedback.msg_debug (v 0 (str "Heuristic:" ++ spc () ++ Termops.Internal.print_constr_env env evd t1 ++ cut () ++ |