From 96e78e0d4ab9e2c2ccf1bb0565384e4e0d322904 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 22 Jun 2018 00:43:01 +0200 Subject: Move transparent_state to its own module. --- pretyping/reductionops.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'pretyping/reductionops.ml') diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 17003cd1dd..18b0bab892 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1305,13 +1305,13 @@ let test_trans_conversion (f: constr Reduction.extended_conversion_function) red with Reduction.NotConvertible -> false | e when is_anomaly e -> report_anomaly e -let is_conv ?(reds=full_transparent_state) env sigma = test_trans_conversion f_conv reds env sigma -let is_conv_leq ?(reds=full_transparent_state) env sigma = test_trans_conversion f_conv_leq reds env sigma -let is_fconv ?(reds=full_transparent_state) = function +let is_conv ?(reds=TranspState.full) env sigma = test_trans_conversion f_conv reds env sigma +let is_conv_leq ?(reds=TranspState.full) env sigma = test_trans_conversion f_conv_leq reds env sigma +let is_fconv ?(reds=TranspState.full) = function | Reduction.CONV -> is_conv ~reds | Reduction.CUMUL -> is_conv_leq ~reds -let check_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = +let check_conv ?(pb=Reduction.CUMUL) ?(ts=TranspState.full) env sigma x y = let f = match pb with | Reduction.CONV -> f_conv | Reduction.CUMUL -> f_conv_leq @@ -1345,7 +1345,7 @@ let sigma_univ_state = compare_cumul_instances = sigma_check_inductive_instances; } let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) - ?(ts=full_transparent_state) env sigma x y = + ?(ts=TranspState.full) env sigma x y = (** FIXME *) try let ans = match pb with @@ -1378,7 +1378,7 @@ let infer_conv = infer_conv_gen (fun pb ~l2r sigma -> Reduction.generic_conv pb ~l2r (safe_evar_value sigma)) (* This reference avoids always having to link C code with the kernel *) -let vm_infer_conv = ref (infer_conv ~catch_incon:true ~ts:full_transparent_state) +let vm_infer_conv = ref (infer_conv ~catch_incon:true ~ts:TranspState.full) let set_vm_infer_conv f = vm_infer_conv := f let vm_infer_conv ?(pb=Reduction.CUMUL) env t1 t2 = !vm_infer_conv ~pb env t1 t2 -- cgit v1.2.3 From ad5aea737ecc639c31dda84322b3550a4d380b47 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 22 Jun 2018 21:06:01 +0200 Subject: Proper record type and accessors for transparent states. This is documented in dev/doc/changes.md. --- pretyping/reductionops.ml | 23 ----------------------- 1 file changed, 23 deletions(-) (limited to 'pretyping/reductionops.ml') diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 18b0bab892..4fbbf20c1f 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -675,10 +675,6 @@ let apply_subst recfun env sigma refold cst_l t stack = let stacklam recfun env sigma t stack = apply_subst (fun _ _ s -> recfun s) env sigma false Cst_stack.empty t stack -let beta_app sigma (c,l) = - let zip s = Stack.zip sigma s in - stacklam zip [] sigma c (Stack.append_app l Stack.empty) - let beta_applist sigma (c,l) = let zip s = Stack.zip sigma s in stacklam zip [] sigma c (Stack.append_app_list l Stack.empty) @@ -1681,25 +1677,6 @@ let meta_reducible_instance evd b = if Metaset.is_empty fm then (* nf_betaiota? *) b.rebus else irec b.rebus - -let head_unfold_under_prod ts env sigma c = - let unfold (cst,u) = - let cstu = (cst, EInstance.kind sigma u) in - if Cpred.mem cst (snd ts) then - match constant_opt_value_in env cstu with - | Some c -> EConstr.of_constr c - | None -> mkConstU (cst, u) - else mkConstU (cst, u) in - let rec aux c = - match EConstr.kind sigma c with - | Prod (n,t,c) -> mkProd (n,aux t, aux c) - | _ -> - let (h,l) = decompose_app_vect sigma c in - match EConstr.kind sigma h with - | Const cst -> beta_app sigma (unfold cst, l) - | _ -> c in - aux c - let betazetaevar_applist sigma n c l = let rec stacklam n env t stack = if Int.equal n 0 then applist (substl env t, stack) else -- cgit v1.2.3 From 733cb74a2038ff92156b7209713fc2ea741ccca6 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 19 Nov 2018 08:12:28 +0100 Subject: Rename TranspState into TransparentState. --- pretyping/reductionops.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'pretyping/reductionops.ml') diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 4fbbf20c1f..e632976ae5 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1301,13 +1301,13 @@ let test_trans_conversion (f: constr Reduction.extended_conversion_function) red with Reduction.NotConvertible -> false | e when is_anomaly e -> report_anomaly e -let is_conv ?(reds=TranspState.full) env sigma = test_trans_conversion f_conv reds env sigma -let is_conv_leq ?(reds=TranspState.full) env sigma = test_trans_conversion f_conv_leq reds env sigma -let is_fconv ?(reds=TranspState.full) = function +let is_conv ?(reds=TransparentState.full) env sigma = test_trans_conversion f_conv reds env sigma +let is_conv_leq ?(reds=TransparentState.full) env sigma = test_trans_conversion f_conv_leq reds env sigma +let is_fconv ?(reds=TransparentState.full) = function | Reduction.CONV -> is_conv ~reds | Reduction.CUMUL -> is_conv_leq ~reds -let check_conv ?(pb=Reduction.CUMUL) ?(ts=TranspState.full) env sigma x y = +let check_conv ?(pb=Reduction.CUMUL) ?(ts=TransparentState.full) env sigma x y = let f = match pb with | Reduction.CONV -> f_conv | Reduction.CUMUL -> f_conv_leq @@ -1341,7 +1341,7 @@ let sigma_univ_state = compare_cumul_instances = sigma_check_inductive_instances; } let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) - ?(ts=TranspState.full) env sigma x y = + ?(ts=TransparentState.full) env sigma x y = (** FIXME *) try let ans = match pb with @@ -1374,7 +1374,7 @@ let infer_conv = infer_conv_gen (fun pb ~l2r sigma -> Reduction.generic_conv pb ~l2r (safe_evar_value sigma)) (* This reference avoids always having to link C code with the kernel *) -let vm_infer_conv = ref (infer_conv ~catch_incon:true ~ts:TranspState.full) +let vm_infer_conv = ref (infer_conv ~catch_incon:true ~ts:TransparentState.full) let set_vm_infer_conv f = vm_infer_conv := f let vm_infer_conv ?(pb=Reduction.CUMUL) env t1 t2 = !vm_infer_conv ~pb env t1 t2 -- cgit v1.2.3