diff options
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 100 |
1 files changed, 0 insertions, 100 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 2cbef98e8..18f1d13ea 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -202,75 +202,6 @@ and check_same_fix_binder bl1 bl2 = let same c d = try check_same_type c d; true with _ -> false -(* Idem for rawconstr *) - -let array_iter2 f v1 v2 = - List.iter2 f (Array.to_list v1) (Array.to_list v2) - -let rec same_patt p1 p2 = - match p1, p2 with - PatVar(_,na1), PatVar(_,na2) -> if na1<>na2 then failwith "PatVar" - | PatCstr(_,c1,pl1,al1), PatCstr(_,c2,pl2,al2) -> - if c1<>c2 || al1 <> al2 then failwith "PatCstr"; - List.iter2 same_patt pl1 pl2 - | _ -> failwith "same_patt" - -let rec same_raw c d = - match c,d with - | RRef(_,gr1), RRef(_,gr2) -> if gr1<>gr2 then failwith "RRef" - | RVar(_,id1), RVar(_,id2) -> if id1<>id2 then failwith "RVar" - | REvar(_,e1,a1), REvar(_,e2,a2) -> - if e1 <> e2 then failwith "REvar"; - Option.iter2(List.iter2 same_raw) a1 a2 - | RPatVar(_,pv1), RPatVar(_,pv2) -> if pv1<>pv2 then failwith "RPatVar" - | RApp(_,f1,a1), RApp(_,f2,a2) -> - List.iter2 same_raw (f1::a1) (f2::a2) - | RLambda(_,na1,bk1,t1,m1), RLambda(_,na2,bk2,t2,m2) -> - if na1 <> na2 then failwith "RLambda"; - same_raw t1 t2; same_raw m1 m2 - | RProd(_,na1,bk1,t1,m1), RProd(_,na2,bk2,t2,m2) -> - if na1 <> na2 then failwith "RProd"; - same_raw t1 t2; same_raw m1 m2 - | RLetIn(_,na1,t1,m1), RLetIn(_,na2,t2,m2) -> - if na1 <> na2 then failwith "RLetIn"; - same_raw t1 t2; same_raw m1 m2 - | RCases(_,_,_,c1,b1), RCases(_,_,_,c2,b2) -> - List.iter2 - (fun (t1,(al1,oind1)) (t2,(al2,oind2)) -> - same_raw t1 t2; - if al1 <> al2 then failwith "RCases"; - Option.iter2(fun (_,i1,_,nl1) (_,i2,_,nl2) -> - if i1<>i2 || nl1 <> nl2 then failwith "RCases") oind1 oind2) c1 c2; - List.iter2 (fun (_,_,pl1,b1) (_,_,pl2,b2) -> - List.iter2 same_patt pl1 pl2; - same_raw b1 b2) b1 b2 - | RLetTuple(_,nl1,_,b1,c1), RLetTuple(_,nl2,_,b2,c2) -> - if nl1<>nl2 then failwith "RLetTuple"; - same_raw b1 b2; - same_raw c1 c2 - | RIf(_,b1,_,t1,e1),RIf(_,b2,_,t2,e2) -> - same_raw b1 b2; same_raw t1 t2; same_raw e1 e2 - | RRec(_,fk1,na1,bl1,ty1,def1), RRec(_,fk2,na2,bl2,ty2,def2) -> - if fk1 <> fk2 || na1 <> na2 then failwith "RRec"; - array_iter2 - (List.iter2 (fun (na1,bk1,bd1,ty1) (na2,bk2,bd2,ty2) -> - if na1<>na2 then failwith "RRec"; - Option.iter2 same_raw bd1 bd2; - same_raw ty1 ty2)) bl1 bl2; - array_iter2 same_raw ty1 ty2; - array_iter2 same_raw def1 def2 - | RSort(_,s1), RSort(_,s2) -> if s1<>s2 then failwith "RSort" - | RHole _, _ -> () - | _, RHole _ -> () - | RCast(_,c1,_),r2 -> same_raw c1 r2 - | r1, RCast(_,c2,_) -> same_raw r1 c2 - | RDynamic(_,d1), RDynamic(_,d2) -> if d1<>d2 then failwith"RDynamic" - | _ -> failwith "same_raw" - -let same_rawconstr c d = - try same_raw c d; true - with Failure _ | Invalid_argument _ -> false - (**********************************************************************) (* mapping patterns to cases_pattern_expr *) @@ -555,11 +486,6 @@ let rec flatten_application = function | RApp (loc,RApp(_,a,l'),l) -> flatten_application (RApp (loc,a,l'@l)) | a -> a -let rec rename_rawconstr_var id0 id1 = function - RRef(loc,VarRef id) when id=id0 -> RRef(loc,VarRef id1) - | RVar(loc,id) when id=id0 -> RVar(loc,id1) - | c -> map_rawconstr (rename_rawconstr_var id0 id1) c - (**********************************************************************) (* mapping rawterms to numerals (in presence of coercions, choose the *) (* one with no delimiter if possible) *) @@ -964,32 +890,6 @@ let rec raw_of_pat env = function | PCoFix c -> Detyping.detype false [] env (mkCoFix c) | PSort s -> RSort (loc,s) -and raw_of_eqn env constr construct_nargs branch = - let make_pat x env b ids = - let avoid = List.fold_right (name_fold (fun x l -> x::l)) env [] in - let id = next_name_away_with_default "x" x avoid in - PatVar (dummy_loc,Name id),(Name id)::env,id::ids - in - let rec buildrec ids patlist env n b = - if n=0 then - (dummy_loc, ids, - [PatCstr(dummy_loc, constr, List.rev patlist,Anonymous)], - raw_of_pat env b) - else - match b with - | PLambda (x,_,b) -> - let pat,new_env,new_ids = make_pat x env b ids in - buildrec new_ids (pat::patlist) new_env (n-1) b - - | PLetIn (x,_,b) -> - let pat,new_env,new_ids = make_pat x env b ids in - buildrec new_ids (pat::patlist) new_env (n-1) b - - | _ -> - error "Unsupported branch in case-analysis while printing pattern." - in - buildrec [] [] env construct_nargs branch - let extern_constr_pattern env pat = extern true (None,[]) Idset.empty (raw_of_pat env pat) |