From 6338174fdaf790e52062f006c52c911bc5e58cbc Mon Sep 17 00:00:00 2001 From: ppedrot Date: Mon, 2 Sep 2013 22:37:19 +0000 Subject: Removing more association lists in Constrintern. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16757 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/funind/indfun.ml | 25 +++++++++++++++---------- 1 file changed, 15 insertions(+), 10 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index d1fa16c0a..993f3d5fb 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -491,11 +491,12 @@ let map_option f = function open Constrexpr open Topconstr -let make_assoc = List.fold_left2 (fun l a b -> -match a, b with - |(_,Name na), (_, Name id) -> (na, id)::l - |_,_ -> l -) +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 @@ -514,16 +515,20 @@ let rec rebuild_bl (aux,assoc) bl typ = let lnal' = List.length nal' in if lnal' >= lnal then - let old_nal',new_nal' = List.chop lnal nal' in - rebuild_bl ((LocalRawAssum(nal,bk,replace_vars_constr_expr assoc nal't)::aux),(make_assoc assoc old_nal' nal)) bl' + let old_nal',new_nal' = List.chop lnal nal' in + let nassoc = make_assoc assoc old_nal' nal in + let assum = LocalRawAssum(nal,bk,replace_vars_constr_expr assoc nal't) in + rebuild_bl ((assum :: aux), nassoc) bl' (if new_nal' = [] && rest = [] then typ' else if new_nal' = [] then CProdN(Loc.ghost,rest,typ') else CProdN(Loc.ghost,((new_nal',bk',nal't)::rest),typ')) else - let captured_nal,non_captured_nal = List.chop lnal' nal in - rebuild_nal ((LocalRawAssum(captured_nal,bk,replace_vars_constr_expr assoc nal't)::aux), (make_assoc assoc nal' captured_nal)) + let captured_nal,non_captured_nal = List.chop lnal' nal in + let nassoc = make_assoc assoc nal' captured_nal in + let assum = LocalRawAssum(captured_nal,bk,replace_vars_constr_expr assoc nal't) in + rebuild_nal ((assum :: aux), nassoc) bk bl' non_captured_nal (lnal - lnal') (CProdN(Loc.ghost,rest,typ')) | _ -> assert false @@ -537,7 +542,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 ([],[]) bl fix_typ in + let new_bl',new_ret_type,_ = rebuild_bl ([],Id.Map.empty) 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 -- cgit v1.2.3