diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 5 | ||||
| -rw-r--r-- | interp/constrintern.ml | 3 | ||||
| -rw-r--r-- | interp/implicit_quantifiers.ml | 42 | ||||
| -rw-r--r-- | interp/implicit_quantifiers.mli | 17 | ||||
| -rw-r--r-- | interp/reserve.ml | 1 | ||||
| -rw-r--r-- | interp/topconstr.ml | 16 | ||||
| -rw-r--r-- | interp/topconstr.mli | 2 |
7 files changed, 55 insertions, 31 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index add71a8b09..67946e3a28 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -676,6 +676,11 @@ let rec extern inctx scopes vars r = let t = extern_typ scopes vars (anonymize_if_reserved na t) in let (idl,c) = factorize_lambda inctx scopes (add_vname vars na) t c in CLambdaN (loc,[(dummy_loc,na)::idl,Default bk,t],c) + + | RRecord (loc,w,l) -> + let t' = Option.map (extern inctx scopes vars) w in + let l' = List.map (fun (id, c) -> (id, extern inctx scopes vars c)) l in + CRecord (loc, t', l') | RCases (loc,sty,rtntypopt,tml,eqns) -> let vars' = diff --git a/interp/constrintern.ml b/interp/constrintern.ml index cfa88f3cd0..ef7ad36f12 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -946,6 +946,9 @@ let internalise sigma globalenv env allow_patvar lvar c = (* Now compact "(f args') args" *) | RApp (loc', f', args') -> RApp (join_loc loc' loc, f',args'@args) | _ -> RApp (loc, c, args)) + | CRecord (loc, w, fs) -> + RRecord (loc, Option.map (intern env) w, + List.map (fun (id, c) -> (id, intern env c)) fs) | CCases (loc, sty, rtnpo, tms, eqns) -> let tms,env' = List.fold_right (fun citm (inds,env) -> diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 876af8f54b..0bfc109ab3 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -63,6 +63,24 @@ let free_vars_of_constr_expr c ?(bound=Idset.empty) l = | c -> fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux bdvars l c in aux bound l c +let ids_of_names l = + List.fold_left (fun acc x -> match snd x with Name na -> na :: acc | Anonymous -> acc) [] l + +let free_vars_of_binders ?(bound=Idset.empty) l (binders : local_binder list) = + let rec aux bdvars l c = match c with + ((LocalRawAssum (n, _, c)) :: tl) -> + let bound = ids_of_names n in + let l' = free_vars_of_constr_expr c ~bound:bdvars l in + aux (Idset.union (ids_of_list bound) bdvars) l' tl + + | ((LocalRawDef (n, c)) :: tl) -> + let bound = match snd n with Anonymous -> [] | Name n -> [n] in + let l' = free_vars_of_constr_expr c ~bound:bdvars l in + aux (Idset.union (ids_of_list bound) bdvars) l' tl + + | [] -> bdvars, l + in aux bound l binders + let add_name_to_ids set na = match na with | Anonymous -> set @@ -80,6 +98,8 @@ let free_vars_of_rawconstr ?(bound=Idset.empty) = let vs' = vars bound vs ty in let bound' = add_name_to_ids bound na in vars bound' vs' c + | RRecord (loc,w,l) -> List.fold_left (vars bound) vs + (Option.List.cons w (List.map snd l)) | RCases (loc,sty,rtntypopt,tml,pl) -> let vs1 = vars_option bound vs rtntypopt in let vs2 = List.fold_left (fun vs (tm,_) -> vars bound vs tm) vs1 tml in @@ -128,33 +148,11 @@ let free_vars_of_rawconstr ?(bound=Idset.empty) = in fun rt -> List.rev (vars bound [] rt) - -let ids_of_names l = - List.fold_left (fun acc x -> match snd x with Name na -> na :: acc | Anonymous -> acc) [] l - -let free_vars_of_binders ?(bound=Idset.empty) l (binders : local_binder list) = - let rec aux bdvars l c = match c with - ((LocalRawAssum (n, _, c)) :: tl) -> - let bound = ids_of_names n in - let l' = free_vars_of_constr_expr c ~bound:bdvars l in - aux (Idset.union (ids_of_list bound) bdvars) l' tl - - | ((LocalRawDef (n, c)) :: tl) -> - let bound = match snd n with Anonymous -> [] | Name n -> [n] in - let l' = free_vars_of_constr_expr c ~bound:bdvars l in - aux (Idset.union (ids_of_list bound) bdvars) l' tl - - | [] -> bdvars, l - in aux bound l binders - let rec make_fresh ids env x = if is_freevar ids env x then x else make_fresh ids env (Nameops.lift_ident x) let freevars_of_ids env ids = List.filter (is_freevar env (Global.env())) ids - -let binder_list_of_ids ids = - List.map (fun id -> LocalRawAssum ([dummy_loc, Name id], Default Implicit, CHole (dummy_loc, None))) ids let next_ident_away_from id avoid = make_fresh avoid (Global.env ()) id diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index 5934272091..dc83e2135c 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -28,19 +28,20 @@ val ids_of_list : identifier list -> Idset.t val destClassApp : constr_expr -> loc * reference * constr_expr list val destClassAppExpl : constr_expr -> loc * reference * (constr_expr * explicitation located option) list -val free_vars_of_constr_expr : Topconstr.constr_expr -> - ?bound:Idset.t -> - Names.identifier list -> Names.identifier list +(* Fragile, should be used only for construction a set of identifiers to avoid *) -val free_vars_of_rawconstr : ?bound:Idset.t -> rawconstr -> (Names.identifier * loc) list - -val binder_list_of_ids : identifier list -> local_binder list - -val make_fresh : Names.Idset.t -> Environ.env -> identifier -> identifier +val free_vars_of_constr_expr : constr_expr -> ?bound:Idset.t -> + identifier list -> identifier list val free_vars_of_binders : ?bound:Idset.t -> Names.identifier list -> local_binder list -> Idset.t * Names.identifier list +(* Returns the free ids in left-to-right order with the location of their first occurence *) + +val free_vars_of_rawconstr : ?bound:Idset.t -> rawconstr -> (Names.identifier * loc) list + +val make_fresh : Names.Idset.t -> Environ.env -> identifier -> identifier + val implicits_of_rawterm : Rawterm.rawconstr -> (Topconstr.explicitation * (bool * bool)) list val combine_params_freevar : diff --git a/interp/reserve.ml b/interp/reserve.ml index f49c42a55d..2479f1f04e 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -57,6 +57,7 @@ let rec unloc = function | RLambda (_,na,bk,ty,c) -> RLambda (dummy_loc,na,bk,unloc ty,unloc c) | RProd (_,na,bk,ty,c) -> RProd (dummy_loc,na,bk,unloc ty,unloc c) | RLetIn (_,na,b,c) -> RLetIn (dummy_loc,na,unloc b,unloc c) + | RRecord (_,w,l) -> RRecord (dummy_loc,w,l) | RCases (_,sty,rtntypopt,tml,pl) -> RCases (dummy_loc,sty, (Option.map unloc rtntypopt), diff --git a/interp/topconstr.ml b/interp/topconstr.ml index c0b81c90c3..3dc77dd604 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -37,6 +37,7 @@ type aconstr = | ALambda of name * aconstr * aconstr | AProd of name * aconstr * aconstr | ALetIn of name * aconstr * aconstr + | ARecord of aconstr option * (identifier * aconstr) list | ACases of case_style * aconstr option * (aconstr * (name * (inductive * int * name list) option)) list * (cases_pattern list * aconstr) list @@ -82,6 +83,8 @@ let rawconstr_of_aconstr_with_binders loc g f e = function let e,na = name_fold_map g e na in RProd (loc,na,Explicit,f e ty,f e c) | ALetIn (na,b,c) -> let e,na = name_fold_map g e na in RLetIn (loc,na,f e b,f e c) + | ARecord (b,l) -> + RRecord (loc, Option.map (f e) b, List.map (fun (id, x) -> ((loc,id),f e x)) l) | ACases (sty,rtntypopt,tml,eqnl) -> let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') -> let e',t' = match t with @@ -146,7 +149,7 @@ let compare_rawconstr f t1 t2 = match t1,t2 with f ty1 ty2 & f c1 c2 | RHole _, RHole _ -> true | RSort (_,s1), RSort (_,s2) -> s1 = s2 - | (RLetIn _ | RCases _ | RRec _ | RDynamic _ + | (RLetIn _ | RRecord _ | RCases _ | RRec _ | RDynamic _ | RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _),_ | _,(RLetIn _ | RCases _ | RRec _ | RDynamic _ | RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _) @@ -192,6 +195,7 @@ let aconstr_and_vars_of_rawconstr a = | RLambda (_,na,bk,ty,c) -> add_name found na; ALambda (na,aux ty,aux c) | RProd (_,na,bk,ty,c) -> add_name found na; AProd (na,aux ty,aux c) | RLetIn (_,na,b,c) -> add_name found na; ALetIn (na,aux b,aux c) + | RRecord (_,w,l) -> ARecord (Option.map aux w,List.map (fun ((_,id), x) -> id, aux x) l) | RCases (_,sty,rtntypopt,tml,eqnl) -> let f (_,idl,pat,rhs) = found := idl@(!found); (pat,aux rhs) in ACases (sty,Option.map aux rtntypopt, @@ -319,6 +323,12 @@ let rec subst_aconstr subst bound raw = if r1' == r1 && r2' == r2 then raw else ALetIn (n,r1',r2') + | ARecord (r1,r2) -> + let r1' = Option.smartmap (subst_aconstr subst bound) r1 + and r2' = list_smartmap (fun (id, x) -> id,subst_aconstr subst bound x) r2 in + if r1' == r1 && r2' == r2 then raw else + ARecord (r1',r2') + | ACases (sty,rtntypopt,rl,branches) -> let rtntypopt' = Option.smartmap (subst_aconstr subst bound) rtntypopt and rl' = list_smartmap @@ -637,6 +647,7 @@ type constr_expr = | CAppExpl of loc * (proj_flag * reference) * constr_expr list | CApp of loc * (proj_flag * constr_expr) * (constr_expr * explicitation located option) list + | CRecord of loc * constr_expr option * (identifier located * constr_expr) list | CCases of loc * case_style * constr_expr option * (constr_expr * (name option * constr_expr option)) list * (loc * cases_pattern_expr list located list * constr_expr) list @@ -709,6 +720,7 @@ let constr_loc = function | CLetIn (loc,_,_,_) -> loc | CAppExpl (loc,_,_) -> loc | CApp (loc,_,_) -> loc + | CRecord (loc,_,_) -> loc | CCases (loc,_,_,_,_) -> loc | CLetTuple (loc,_,_,_,_) -> loc | CIf (loc,_,_,_,_) -> loc @@ -806,6 +818,7 @@ let fold_constr_expr_with_binders g f n acc = function | CDelimiters (loc,_,a) -> f n acc a | CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CDynamic _ | CRef _ -> acc + | CRecord (loc,_,l) -> List.fold_left (fun acc (id, c) -> f n acc c) acc l | CCases (loc,sty,rtnpo,al,bl) -> let ids = ids_of_cases_tomatch al in let acc = Option.fold_left (f (List.fold_right g ids n)) acc rtnpo in @@ -919,6 +932,7 @@ let map_constr_expr_with_binders g f e = function | CDelimiters (loc,s,a) -> CDelimiters (loc,s,f e a) | CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CDynamic _ | CRef _ as x -> x + | CRecord (loc,p,l) -> CRecord (loc,p,List.map (fun (id, c) -> (id, f e c)) l) | CCases (loc,sty,rtnpo,a,bl) -> (* TODO: apply g on the binding variables in pat... *) let bl = List.map (fun (loc,pat,rhs) -> (loc,pat,f e rhs)) bl in diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 0064d238d1..b6e2927bbd 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -33,6 +33,7 @@ type aconstr = | ALambda of name * aconstr * aconstr | AProd of name * aconstr * aconstr | ALetIn of name * aconstr * aconstr + | ARecord of aconstr option * (identifier * aconstr) list | ACases of case_style * aconstr option * (aconstr * (name * (inductive * int * name list) option)) list * (cases_pattern list * aconstr) list @@ -133,6 +134,7 @@ type constr_expr = | CAppExpl of loc * (proj_flag * reference) * constr_expr list | CApp of loc * (proj_flag * constr_expr) * (constr_expr * explicitation located option) list + | CRecord of loc * constr_expr option * (identifier located * constr_expr) list | CCases of loc * case_style * constr_expr option * (constr_expr * (name option * constr_expr option)) list * (loc * cases_pattern_expr list located list * constr_expr) list |