diff options
-rw-r--r-- | interp/constrextern.mli | 1 | ||||
-rw-r--r-- | parsing/ppconstr.ml | 79 | ||||
-rw-r--r-- | parsing/ppconstr.mli | 3 |
3 files changed, 0 insertions, 83 deletions
diff --git a/interp/constrextern.mli b/interp/constrextern.mli index f52ec8fd8..ac9ed5714 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -21,7 +21,6 @@ open Pattern open Topconstr open Notation -(** v7->v8 translation *) val check_same_type : constr_expr -> constr_expr -> unit (** Translation of pattern, cases pattern, rawterm and term into syntax diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index cd56bccb7..08ac7fd68 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -307,85 +307,6 @@ let split_product na' = function rename na na' t (CProdN(loc,(nal,bk,t)::bl,c)) | _ -> anomaly "ill-formed fixpoint body" -let merge_binders (na1,bk1,ty1) cofun (na2,bk2,ty2) codom = - let na = - match snd na1, snd na2 with - Anonymous, Name id -> - if occur_var_constr_expr id cofun then - failwith "avoid capture" - else na2 - | Name id, Anonymous -> - if occur_var_constr_expr id codom then - failwith "avoid capture" - else na1 - | Anonymous, Anonymous -> na1 - | Name id1, Name id2 -> - if id1 <> id2 then failwith "not same name" else na1 in - let ty = - match ty1, ty2 with - CHole _, _ -> ty2 - | _, CHole _ -> ty1 - | _ -> - Constrextern.check_same_type ty1 ty2; - ty2 in - (LocalRawAssum ([na],bk1,ty), codom) - -let rec strip_domain bvar cofun c = - match c with - | CArrow(loc,a,b) -> - merge_binders bvar cofun ((dummy_loc,Anonymous),default_binder_kind,a) b - | CProdN(loc,[([na],bk,ty)],c') -> - merge_binders bvar cofun (na,bk,ty) c' - | CProdN(loc,([na],bk,ty)::bl,c') -> - merge_binders bvar cofun (na,bk,ty) (CProdN(loc,bl,c')) - | CProdN(loc,(na::nal,bk,ty)::bl,c') -> - merge_binders bvar cofun (na,bk,ty) (CProdN(loc,(nal,bk,ty)::bl,c')) - | _ -> failwith "not a product" - -(* Note: binder sharing is lost *) -let rec strip_domains (nal,bk,ty) cofun c = - match nal with - [] -> assert false - | [na] -> - let bnd, c' = strip_domain (na,bk,ty) cofun c in - ([bnd],None,c') - | na::nal -> - let f = CLambdaN(dummy_loc,[(nal,bk,ty)],cofun) in - let bnd, c1 = strip_domain (na,bk,ty) f c in - (try - let bl, rest, c2 = strip_domains (nal,bk,ty) cofun c1 in - (bnd::bl, rest, c2) - with Failure _ -> ([bnd],Some (nal,bk,ty), c1)) - -(* Re-share binders *) -let rec factorize_binders = function - | ([] | [_] as l) -> l - | LocalRawAssum (nal,k,ty) as d :: (LocalRawAssum (nal',k',ty')::l as l') -> - (try - let _ = Constrextern.check_same_type ty ty' in - factorize_binders (LocalRawAssum (nal@nal',k,ty)::l) - with _ -> - d :: factorize_binders l') - | d :: l -> d :: factorize_binders l - -(* Extract lambdas when a type constraint occurs *) -let rec extract_def_binders c ty = - match c with - | CLambdaN(loc,bvar::lams,b) -> - (try - let f = CLambdaN(loc,lams,b) in - let bvar', rest, ty' = strip_domains bvar f ty in - let c' = - match rest, lams with - None,[] -> b - | None, _ -> f - | Some bvar,_ -> CLambdaN(loc,bvar::lams,b) in - let (bl,c2,ty2) = extract_def_binders c' ty' in - (factorize_binders (bvar'@bl), c2, ty2) - with Failure _ -> - ([],c,ty)) - | _ -> ([],c,ty) - let rec split_fix n typ def = if n = 0 then ([],typ,def) else diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli index f1bb49312..d2d44f245 100644 --- a/parsing/ppconstr.mli +++ b/parsing/ppconstr.mli @@ -24,9 +24,6 @@ val extract_lam_binders : constr_expr -> local_binder list * constr_expr val extract_prod_binders : constr_expr -> local_binder list * constr_expr -val extract_def_binders : - constr_expr -> constr_expr -> - local_binder list * constr_expr * constr_expr val split_fix : int -> constr_expr -> constr_expr -> local_binder list * constr_expr * constr_expr |