diff options
Diffstat (limited to 'pretyping')
| -rwxr-xr-x | pretyping/classops.ml | 32 | ||||
| -rw-r--r-- | pretyping/detyping.ml | 114 | ||||
| -rw-r--r-- | pretyping/detyping.mli | 3 | ||||
| -rw-r--r-- | pretyping/pattern.ml | 107 | ||||
| -rw-r--r-- | pretyping/rawterm.ml | 114 | ||||
| -rw-r--r-- | pretyping/rawterm.mli | 3 | ||||
| -rwxr-xr-x | pretyping/recordops.ml | 20 |
7 files changed, 205 insertions, 188 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml index aef35cd7cf..66ed81d021 100755 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -153,21 +153,35 @@ let lookup_pattern_path_between (s,t) = | Construct sp -> (sp, coe.coe_param) | _ -> raise Not_found) l +(* find_class_type : constr -> cl_typ * int *) + +let find_class_type t = + let t', args = decompose_app (Reductionops.whd_betaiotazeta t) in + match kind_of_term t' with + | Var id -> CL_SECVAR id, args + | Const sp -> CL_CONST sp, args + | Ind ind_sp -> CL_IND ind_sp, args + | Prod (_,_,_) -> CL_FUN, [] + | Sort _ -> CL_SORT, [] + | _ -> raise Not_found + let subst_cl_typ subst ct = match ct with CL_SORT | CL_FUN | CL_SECVAR _ -> ct | CL_CONST kn -> - let kn' = subst_con subst kn in + let kn',t = subst_con subst kn in if kn' == kn then ct else - CL_CONST kn' + fst (find_class_type t) | CL_IND (kn,i) -> let kn' = subst_kn subst kn in if kn' == kn then ct else CL_IND (kn',i) -let subst_coe_typ = subst_global +(*CSC: here we should change the datatype for coercions: it should be possible + to declare any term as a coercion *) +let subst_coe_typ subst t = fst (subst_global subst t) let subst_coe_info subst info = let jud = info.coe_value in @@ -209,18 +223,6 @@ let _ = (* classe d'un terme *) -(* find_class_type : constr -> cl_typ * int *) - -let find_class_type t = - let t', args = decompose_app (Reductionops.whd_betaiotazeta t) in - match kind_of_term t' with - | Var id -> CL_SECVAR id, args - | Const sp -> CL_CONST sp, args - | Ind ind_sp -> CL_IND ind_sp, args - | Prod (_,_,_) -> CL_FUN, [] - | Sort _ -> CL_SORT, [] - | _ -> raise Not_found - (* class_of : Term.constr -> int *) let class_of env sigma t = diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 6a0ea00602..880605313a 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -492,3 +492,117 @@ and detype_binder tenv bk avoid env na ty c = | BProd -> RProd (dummy_loc, na',detype tenv [] env ty, r) | BLambda -> RLambda (dummy_loc, na',detype tenv [] env ty, r) | BLetIn -> RLetIn (dummy_loc, na',detype tenv [] env ty, r) + +let rec subst_pat subst pat = + match pat with + | PatVar _ -> pat + | PatCstr (loc,((kn,i),j),cpl,n) -> + let kn' = subst_kn subst kn + and cpl' = list_smartmap (subst_pat subst) cpl in + if kn' == kn && cpl' == cpl then pat else + PatCstr (loc,((kn',i),j),cpl',n) + +let rec subst_raw subst raw = + match raw with + | RRef (loc,ref) -> + let ref',t = subst_global subst ref in + if ref' == ref then raw else + detype (false,Global.env ()) [] [] t + + | RVar _ -> raw + | REvar _ -> raw + | RPatVar _ -> raw + + | RApp (loc,r,rl) -> + let r' = subst_raw subst r + and rl' = list_smartmap (subst_raw subst) rl in + if r' == r && rl' == rl then raw else + RApp(loc,r',rl') + + | RLambda (loc,n,r1,r2) -> + let r1' = subst_raw subst r1 and r2' = subst_raw subst r2 in + if r1' == r1 && r2' == r2 then raw else + RLambda (loc,n,r1',r2') + + | RProd (loc,n,r1,r2) -> + let r1' = subst_raw subst r1 and r2' = subst_raw subst r2 in + if r1' == r1 && r2' == r2 then raw else + RProd (loc,n,r1',r2') + + | RLetIn (loc,n,r1,r2) -> + let r1' = subst_raw subst r1 and r2' = subst_raw subst r2 in + if r1' == r1 && r2' == r2 then raw else + RLetIn (loc,n,r1',r2') + + | RCases (loc,(ro,rtno),rl,branches) -> + let ro' = option_smartmap (subst_raw subst) ro + and rtno' = ref (option_smartmap (subst_raw subst) !rtno) + and rl' = list_smartmap (fun (a,x as y) -> + let a' = subst_raw subst a in + let (n,topt) = !x in + let topt' = option_smartmap + (fun (loc,(sp,i),x as t) -> + let sp' = subst_kn subst sp in + if sp == sp' then t else (loc,(sp',i),x)) topt in + if a == a' && topt == topt' then y else (a',ref (n,topt'))) rl + and branches' = list_smartmap + (fun (loc,idl,cpl,r as branch) -> + let cpl' = list_smartmap (subst_pat subst) cpl + and r' = subst_raw subst r in + if cpl' == cpl && r' == r then branch else + (loc,idl,cpl',r')) + branches + in + if ro' == ro && rl' == rl && branches' == branches then raw else + RCases (loc,(ro',rtno'),rl',branches') + + | ROrderedCase (loc,b,ro,r,ra,x) -> + let ro' = option_smartmap (subst_raw subst) ro + and r' = subst_raw subst r + and ra' = array_smartmap (subst_raw subst) ra in + if ro' == ro && r' == r && ra' == ra then raw else + ROrderedCase (loc,b,ro',r',ra',x) + + | RLetTuple (loc,nal,(na,po),b,c) -> + let po' = option_smartmap (subst_raw subst) po + and b' = subst_raw subst b + and c' = subst_raw subst c in + if po' == po && b' == b && c' == c then raw else + RLetTuple (loc,nal,(na,po'),b',c') + + | RIf (loc,c,(na,po),b1,b2) -> + let po' = option_smartmap (subst_raw subst) po + and b1' = subst_raw subst b1 + and b2' = subst_raw subst b2 + and c' = subst_raw subst c in + if c' == c & po' == po && b1' == b1 && b2' == b2 then raw else + RIf (loc,c',(na,po'),b1',b2') + + | RRec (loc,fix,ida,bl,ra1,ra2) -> + let ra1' = array_smartmap (subst_raw subst) ra1 + and ra2' = array_smartmap (subst_raw subst) ra2 in + let bl' = array_smartmap + (list_smartmap (fun (na,obd,ty as dcl) -> + let ty' = subst_raw subst ty in + let obd' = option_smartmap (subst_raw subst) obd in + if ty'==ty & obd'==obd then dcl else (na,obd',ty'))) + bl in + if ra1' == ra1 && ra2' == ra2 && bl'==bl then raw else + RRec (loc,fix,ida,bl',ra1',ra2') + + | RSort _ -> raw + + | RHole (loc,ImplicitArg (ref,i)) -> + let ref',_ = subst_global subst ref in + if ref' == ref then raw else + RHole (loc,InternalHole) + | RHole (loc, (BinderType _ | QuestionMark | CasesType | + InternalHole | TomatchTypeParameter _)) -> raw + + | RCast (loc,r1,r2) -> + let r1' = subst_raw subst r1 and r2' = subst_raw subst r2 in + if r1' == r1 && r2' == r2 then raw else + RCast (loc,r1',r2') + + | RDynamic _ -> raw + diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 15743e7bf8..e4aa8a6573 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -16,8 +16,11 @@ open Sign open Environ open Rawterm open Termops +open Mod_subst (*i*) +val subst_raw : substitution -> rawconstr -> rawconstr + (* [detype env avoid nenv c] turns [c], typed in [env], into a rawconstr. *) (* De Bruijn indexes are turned to bound names, avoiding names in [avoid] *) diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index b091d797ad..6e06f978f2 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -63,56 +63,11 @@ let rec occur_meta_pattern = function | PMeta _ | PSoApp _ -> true | PEvar _ | PVar _ | PRef _ | PRel _ | PSort _ | PFix _ | PCoFix _ -> false -let rec subst_pattern subst pat = match pat with - | PRef ref -> - let ref' = subst_global subst ref in - if ref' == ref then pat else - PRef ref' - | PVar _ - | PEvar _ - | PRel _ -> pat - | PApp (f,args) -> - let f' = subst_pattern subst f in - let args' = array_smartmap (subst_pattern subst) args in - if f' == f && args' == args then pat else - PApp (f',args') - | PSoApp (i,args) -> - let args' = list_smartmap (subst_pattern subst) args in - if args' == args then pat else - PSoApp (i,args') - | PLambda (name,c1,c2) -> - let c1' = subst_pattern subst c1 in - let c2' = subst_pattern subst c2 in - if c1' == c1 && c2' == c2 then pat else - PLambda (name,c1',c2') - | PProd (name,c1,c2) -> - let c1' = subst_pattern subst c1 in - let c2' = subst_pattern subst c2 in - if c1' == c1 && c2' == c2 then pat else - PProd (name,c1',c2') - | PLetIn (name,c1,c2) -> - let c1' = subst_pattern subst c1 in - let c2' = subst_pattern subst c2 in - if c1' == c1 && c2' == c2 then pat else - PLetIn (name,c1',c2') - | PSort _ - | PMeta _ -> pat - | PCase (cs,typ, c, branches) -> - let typ' = option_smartmap (subst_pattern subst) typ in - let c' = subst_pattern subst c in - let branches' = array_smartmap (subst_pattern subst) branches in - if typ' == typ && c' == c && branches' == branches then pat else - PCase(cs,typ', c', branches') - | PFix fixpoint -> - let cstr = mkFix fixpoint in - let fixpoint' = destFix (subst_mps subst cstr) in - if fixpoint' == fixpoint then pat else - PFix fixpoint' - | PCoFix cofixpoint -> - let cstr = mkCoFix cofixpoint in - let cofixpoint' = destCoFix (subst_mps subst cstr) in - if cofixpoint' == cofixpoint then pat else - PCoFix cofixpoint' +type constr_label = + | ConstNode of constant + | IndNode of inductive + | CstrNode of constructor + | VarNode of identifier exception BoundPattern;; @@ -177,6 +132,58 @@ let rec inst lvar = function | (PFix _ | PCoFix _ as r) -> error ("Not instantiable pattern") +let rec subst_pattern subst pat = match pat with + | PRef ref -> + let ref',t = subst_global subst ref in + if ref' == ref then pat else + pattern_of_constr t + | PVar _ + | PEvar _ + | PRel _ -> pat + | PApp (f,args) -> + let f' = subst_pattern subst f in + let args' = array_smartmap (subst_pattern subst) args in + if f' == f && args' == args then pat else + PApp (f',args') + | PSoApp (i,args) -> + let args' = list_smartmap (subst_pattern subst) args in + if args' == args then pat else + PSoApp (i,args') + | PLambda (name,c1,c2) -> + let c1' = subst_pattern subst c1 in + let c2' = subst_pattern subst c2 in + if c1' == c1 && c2' == c2 then pat else + PLambda (name,c1',c2') + | PProd (name,c1,c2) -> + let c1' = subst_pattern subst c1 in + let c2' = subst_pattern subst c2 in + if c1' == c1 && c2' == c2 then pat else + PProd (name,c1',c2') + | PLetIn (name,c1,c2) -> + let c1' = subst_pattern subst c1 in + let c2' = subst_pattern subst c2 in + if c1' == c1 && c2' == c2 then pat else + PLetIn (name,c1',c2') + | PSort _ + | PMeta _ -> pat + | PCase (cs,typ, c, branches) -> + let typ' = option_smartmap (subst_pattern subst) typ in + let c' = subst_pattern subst c in + let branches' = array_smartmap (subst_pattern subst) branches in + if typ' == typ && c' == c && branches' == branches then pat else + PCase(cs,typ', c', branches') + | PFix fixpoint -> + let cstr = mkFix fixpoint in + let fixpoint' = destFix (subst_mps subst cstr) in + if fixpoint' == fixpoint then pat else + PFix fixpoint' + | PCoFix cofixpoint -> + let cstr = mkCoFix cofixpoint in + let cofixpoint' = destCoFix (subst_mps subst cstr) in + if cofixpoint' == cofixpoint then pat else + PCoFix cofixpoint' + + let instantiate_pattern = inst let rec pat_of_raw metas vars = function diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index 054312ff34..b915313951 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -16,7 +16,6 @@ open Term open Libnames open Nametab open Evd -open Mod_subst (*i*) (* Untyped intermediate terms, after ASTs and before constr. *) @@ -196,119 +195,6 @@ let occur_rawconstr id = in occur -let rec subst_pat subst pat = - match pat with - | PatVar _ -> pat - | PatCstr (loc,((kn,i),j),cpl,n) -> - let kn' = subst_kn subst kn - and cpl' = list_smartmap (subst_pat subst) cpl in - if kn' == kn && cpl' == cpl then pat else - PatCstr (loc,((kn',i),j),cpl',n) - -let rec subst_raw subst raw = - match raw with - | RRef (loc,ref) -> - let ref' = subst_global subst ref in - if ref' == ref then raw else - RRef (loc,ref') - - | RVar _ -> raw - | REvar _ -> raw - | RPatVar _ -> raw - - | RApp (loc,r,rl) -> - let r' = subst_raw subst r - and rl' = list_smartmap (subst_raw subst) rl in - if r' == r && rl' == rl then raw else - RApp(loc,r',rl') - - | RLambda (loc,n,r1,r2) -> - let r1' = subst_raw subst r1 and r2' = subst_raw subst r2 in - if r1' == r1 && r2' == r2 then raw else - RLambda (loc,n,r1',r2') - - | RProd (loc,n,r1,r2) -> - let r1' = subst_raw subst r1 and r2' = subst_raw subst r2 in - if r1' == r1 && r2' == r2 then raw else - RProd (loc,n,r1',r2') - - | RLetIn (loc,n,r1,r2) -> - let r1' = subst_raw subst r1 and r2' = subst_raw subst r2 in - if r1' == r1 && r2' == r2 then raw else - RLetIn (loc,n,r1',r2') - - | RCases (loc,(ro,rtno),rl,branches) -> - let ro' = option_smartmap (subst_raw subst) ro - and rtno' = ref (option_smartmap (subst_raw subst) !rtno) - and rl' = list_smartmap (fun (a,x as y) -> - let a' = subst_raw subst a in - let (n,topt) = !x in - let topt' = option_smartmap - (fun (loc,(sp,i),x as t) -> - let sp' = subst_kn subst sp in - if sp == sp' then t else (loc,(sp',i),x)) topt in - if a == a' && topt == topt' then y else (a',ref (n,topt'))) rl - and branches' = list_smartmap - (fun (loc,idl,cpl,r as branch) -> - let cpl' = list_smartmap (subst_pat subst) cpl - and r' = subst_raw subst r in - if cpl' == cpl && r' == r then branch else - (loc,idl,cpl',r')) - branches - in - if ro' == ro && rl' == rl && branches' == branches then raw else - RCases (loc,(ro',rtno'),rl',branches') - - | ROrderedCase (loc,b,ro,r,ra,x) -> - let ro' = option_smartmap (subst_raw subst) ro - and r' = subst_raw subst r - and ra' = array_smartmap (subst_raw subst) ra in - if ro' == ro && r' == r && ra' == ra then raw else - ROrderedCase (loc,b,ro',r',ra',x) - - | RLetTuple (loc,nal,(na,po),b,c) -> - let po' = option_smartmap (subst_raw subst) po - and b' = subst_raw subst b - and c' = subst_raw subst c in - if po' == po && b' == b && c' == c then raw else - RLetTuple (loc,nal,(na,po'),b',c') - - | RIf (loc,c,(na,po),b1,b2) -> - let po' = option_smartmap (subst_raw subst) po - and b1' = subst_raw subst b1 - and b2' = subst_raw subst b2 - and c' = subst_raw subst c in - if c' == c & po' == po && b1' == b1 && b2' == b2 then raw else - RIf (loc,c',(na,po'),b1',b2') - - | RRec (loc,fix,ida,bl,ra1,ra2) -> - let ra1' = array_smartmap (subst_raw subst) ra1 - and ra2' = array_smartmap (subst_raw subst) ra2 in - let bl' = array_smartmap - (list_smartmap (fun (na,obd,ty as dcl) -> - let ty' = subst_raw subst ty in - let obd' = option_smartmap (subst_raw subst) obd in - if ty'==ty & obd'==obd then dcl else (na,obd',ty'))) - bl in - if ra1' == ra1 && ra2' == ra2 && bl'==bl then raw else - RRec (loc,fix,ida,bl',ra1',ra2') - - | RSort _ -> raw - - | RHole (loc,ImplicitArg (ref,i)) -> - let ref' = subst_global subst ref in - if ref' == ref then raw else - RHole (loc,ImplicitArg (ref',i)) - | RHole (loc, (BinderType _ | QuestionMark | CasesType | - InternalHole | TomatchTypeParameter _)) -> raw - - | RCast (loc,r1,r2) -> - let r1' = subst_raw subst r1 and r2' = subst_raw subst r2 in - if r1' == r1 && r2' == r2 then raw else - RCast (loc,r1',r2') - - | RDynamic _ -> raw - let loc_of_rawconstr = function | RRef (loc,_) -> loc | RVar (loc,_) -> loc diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index 127eb1dc6d..759e0adb6c 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -15,7 +15,6 @@ open Sign open Term open Libnames open Nametab -open Mod_subst (*i*) (* Untyped intermediate terms, after ASTs and before constr. *) @@ -100,8 +99,6 @@ val occur_rawconstr : identifier -> rawconstr -> bool val loc_of_rawconstr : rawconstr -> loc -val subst_raw : substitution -> rawconstr -> rawconstr - type 'a raw_red_flag = { rBeta : bool; rIota : bool; diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 4cbd02ca4d..cc53ae7f3f 100755 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -47,9 +47,12 @@ let cache_structure (_,(ind,struc)) = let subst_structure (_,subst,((kn,i),struc as obj)) = let kn' = subst_kn subst kn in - let proj' = list_smartmap - (option_smartmap (subst_con subst)) - struc.s_PROJ + let proj' = + (* invariant: struc.s_PROJ is an evaluable reference. Thus we can take *) + (* the first component of subst_con. *) + list_smartmap + (option_smartmap (fun kn -> fst (subst_con subst kn))) + struc.s_PROJ in if proj' == struc.s_PROJ && kn' == kn then obj else (kn',i),{struc with s_PROJ = proj'} @@ -120,14 +123,19 @@ let cache_canonical_structure (_,(cst,lo)) = object_table := x :: (!object_table)) lo let subst_object subst ((r1,r2),o as obj) = - let r1' = subst_global subst r1 in - let r2' = subst_global subst r2 in + (* invariant: r1 and r2 are evaluable references. Thus subst_global *) + (* cannot instantiate them. Hence we can use just the first component *) + (* of the answer. *) + let r1',_ = subst_global subst r1 in + let r2',_ = subst_global subst r2 in let o' = subst_obj subst o in if r1' == r1 && r2' == r2 && o' == o then obj else (r1',r2'),o' let subst_canonical_structure (_,subst,(cst,lo as obj)) = - let cst' = subst_con subst cst in + (* invariant: cst is an evaluable reference. Thus we can take *) + (* the first component of subst_con. *) + let cst' = fst (subst_con subst cst) in let lo' = list_smartmap (subst_object subst) lo in if cst' == cst & lo' == lo then obj else (cst',lo') |