diff options
author | Julien Forest <forest@ensiie.fr> | 2017-06-23 15:06:49 +0200 |
---|---|---|
committer | Julien Forest <forest@ensiie.fr> | 2017-06-23 15:06:49 +0200 |
commit | 181cb78d09ba55c7a6d62b333b26595a4fbb360a (patch) | |
tree | 17661d26e5d36c169d1bf0432df2087e51492992 /plugins/funind | |
parent | 8d92701f1a017354504c84d60c9e76da50feaf49 (diff) |
closing bug #4250
Diffstat (limited to 'plugins/funind')
-rw-r--r-- | plugins/funind/indfun.ml | 78 |
1 files changed, 36 insertions, 42 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index ad04e430c..35f092958 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -576,50 +576,44 @@ let map_option f = function | Some v -> Some (f v) open Constrexpr -open Topconstr -let make_assoc assoc l1 l2 = - let fold assoc a b = match a, b with - | (_, Name na), (_, Name id) -> Id.Map.add na id assoc - | _, _ -> assoc - in - List.fold_left2 fold assoc l1 l2 - -let rec rebuild_bl (aux,assoc) bl typ = - match bl,typ with - | [], _ -> (List.rev aux,replace_vars_constr_expr assoc typ,assoc) - | (Constrexpr.CLocalAssum(nal,bk,_))::bl',typ -> - rebuild_nal (aux,assoc) bk bl' nal (List.length nal) typ - | (Constrexpr.CLocalDef(na,_,_))::bl',{ CAst.v = Constrexpr.CLetIn(_,nat,ty,typ') } -> - rebuild_bl ((Constrexpr.CLocalDef(na,replace_vars_constr_expr assoc nat,Option.map (replace_vars_constr_expr assoc) ty (* ??? *))::aux),assoc) +let rec rebuild_bl aux bl typ = + match bl,typ with + | [], _ -> List.rev aux,typ + | (CLocalAssum(nal,bk,_))::bl',typ -> + rebuild_nal aux bk bl' nal typ + | (CLocalDef(na,_,_))::bl',{ CAst.v = CLetIn(_,nat,ty,typ') } -> + rebuild_bl (Constrexpr.CLocalDef(na,nat,ty)::aux) bl' typ' | _ -> assert false - and rebuild_nal (aux,assoc) bk bl' nal lnal typ = - match nal, typ.CAst.v with - | [], _ -> rebuild_bl (aux,assoc) bl' typ - | _,CProdN([],typ) -> rebuild_nal (aux,assoc) bk bl' nal lnal typ - | _,CProdN((nal',bk',nal't)::rest,typ') -> - let lnal' = List.length nal' in - if lnal' >= lnal - then - let old_nal',new_nal' = List.chop lnal nal' in - let nassoc = make_assoc assoc old_nal' nal in - let assum = CLocalAssum(nal,bk,replace_vars_constr_expr assoc nal't) in - rebuild_bl ((assum :: aux), nassoc) bl' - (if List.is_empty new_nal' && List.is_empty rest - then typ' - else CAst.make @@ if List.is_empty new_nal' - then CProdN(rest,typ') - else CProdN(((new_nal',bk',nal't)::rest),typ')) - else - let captured_nal,non_captured_nal = List.chop lnal' nal in - let nassoc = make_assoc assoc nal' captured_nal in - let assum = CLocalAssum(captured_nal,bk,replace_vars_constr_expr assoc nal't) in - rebuild_nal ((assum :: aux), nassoc) - bk bl' non_captured_nal (lnal - lnal') (CAst.make @@ CProdN(rest,typ')) - | _ -> assert false - -let rebuild_bl (aux,assoc) bl typ = rebuild_bl (aux,assoc) bl typ +and rebuild_nal aux bk bl' nal typ = + match nal,typ with + | _,{ CAst.v = CProdN([],typ) } -> rebuild_nal aux bk bl' nal typ + | [], _ -> rebuild_bl aux bl' typ + | na::nal,{ CAst.v = CProdN((na'::nal',bk',nal't)::rest,typ') } -> + if Name.equal (snd na) (snd na') || Name.is_anonymous (snd na') + then + let assum = CLocalAssum([na],bk',nal't) in + let new_rest = if nal' = [] then rest else ((nal',bk',nal't)::rest) in + rebuild_nal + (assum::aux) + bk + bl' + nal + (CAst.make @@ CProdN(new_rest,typ')) + else + let assum = CLocalAssum([na'],bk',nal't) in + let new_rest = if nal' = [] then rest else ((nal',bk',nal't)::rest) in + rebuild_nal + (assum::aux) + bk + bl' + (na::nal) + (CAst.make @@ CProdN(new_rest,typ')) + | _ -> + assert false + +let rebuild_bl aux bl typ = rebuild_bl aux bl typ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = let fixl,ntns = Command.extract_fixpoint_components false fixpoint_exprl in @@ -629,7 +623,7 @@ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacex let fixpoint_exprl_with_new_bl = List.map2 (fun ((lna,(rec_arg_opt,rec_order),bl,ret_typ,opt_body),notation_list) fix_typ -> - let new_bl',new_ret_type,_ = rebuild_bl ([],Id.Map.empty) bl fix_typ in + let new_bl',new_ret_type = rebuild_bl [] bl fix_typ in (((lna,(rec_arg_opt,rec_order),new_bl',new_ret_type,opt_body),notation_list):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list)) ) fixpoint_exprl constr_expr_typel |