From 64dfa70f4399d23fe4e37326e0adab0123d194a9 Mon Sep 17 00:00:00 2001 From: bertot Date: Fri, 17 Feb 2006 13:26:50 +0000 Subject: Julien: + Compatibility with new induction + Induction principle for general recursion preparation still continuing + Cleaning dead code ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8055 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/funind/rawterm_to_relation.ml | 382 ++++++++++++++++------------------ 1 file changed, 184 insertions(+), 198 deletions(-) (limited to 'contrib/funind/rawterm_to_relation.ml') diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml index 48cc2ce3a..6b3590dd6 100644 --- a/contrib/funind/rawterm_to_relation.ml +++ b/contrib/funind/rawterm_to_relation.ml @@ -9,12 +9,21 @@ open Util open Rawtermops -type binder_type = - | Lambda - | Prod - | LetIn +(* type binder_type = *) +(* | Lambda *) +(* | Prod *) +(* | LetIn *) + +(* type raw_context = (binder_type*name*rawconstr) list *) + +type binder_type = + | Lambda of name + | Prod of name + | LetIn of name +(* | LetTuple of name list * name *) + +type raw_context = (binder_type*rawconstr) list -type raw_context = (binder_type*name*rawconstr) list (* compose_raw_context [(bt_1,n_1,t_1);......] rt returns @@ -22,11 +31,13 @@ type raw_context = (binder_type*name*rawconstr) list binders corresponding to the bt_i's *) let compose_raw_context = - let compose_binder (bt,n,t) acc = + let compose_binder (bt,t) acc = match bt with - | Lambda -> mkRLambda(n,t,acc) - | Prod -> mkRProd(n,t,acc) - | LetIn -> mkRLetIn(n,t,acc) + | Lambda n -> mkRLambda(n,t,acc) + | Prod n -> mkRProd(n,t,acc) + | LetIn n -> mkRLetIn(n,t,acc) +(* | LetTuple (nal,na) -> *) +(* RLetTuple(dummy_loc,nal,(na,None),t,acc) *) in List.fold_right compose_binder @@ -100,27 +111,104 @@ let combine_args arg args = } +let ids_of_binder = function + | LetIn Anonymous | Prod Anonymous | Lambda Anonymous -> [] + | LetIn (Name id) | Prod (Name id) | Lambda (Name id) -> [id] +(* | LetTuple(nal,_) -> *) +(* map_succeed (function Name id -> id | _ -> failwith "ids_of_binder") nal *) + +let rec change_vars_in_binder mapping = function + [] -> [] + | (bt,t)::l -> + let new_mapping = List.fold_right Idmap.remove (ids_of_binder bt) mapping in + (bt,change_vars mapping t):: + (if Idmap.is_empty new_mapping + then l + else change_vars_in_binder new_mapping l + ) + +let rec replace_var_by_term_in_binder x_id term = function + | [] -> [] + | (bt,t)::l -> + (bt,replace_var_by_term x_id term t):: + if List.mem x_id (ids_of_binder bt) + then l + else replace_var_by_term_in_binder x_id term l + +let add_bt_names bt = List.append (ids_of_binder bt) + +(* let rec replace_var_by_term_in_binder x_id term = function *) +(* | [] -> [] *) +(* | (bt,Name id,t)::l when id_ord id x_id = 0 -> *) +(* (bt,Name id,replace_var_by_term x_id term t)::l *) +(* | (bt,na,t)::l -> *) +(* (bt,na,replace_var_by_term x_id term t)::(replace_var_by_term_in_binder x_id term l) *) + +(* let rec change_vars_in_binder mapping = function *) +(* | [] -> [] *) +(* | (bt,(Name id as na),t)::l when Idmap.mem id mapping -> *) +(* (bt,na,change_vars mapping t):: l *) +(* | (bt,na,t)::l -> *) +(* (bt,na,change_vars mapping t):: *) +(* (change_vars_in_binder mapping l) *) +(* let alpha_ctxt avoid b = *) +(* let rec alpha_ctxt = function *) +(* | [] -> [],b *) +(* | (bt,n,t)::ctxt -> *) +(* let new_ctxt,new_b = alpha_ctxt ctxt in *) +(* match n with *) +(* | Name id when List.mem id avoid -> *) +(* let new_id = Nameops.next_ident_away id avoid in *) +(* let mapping = Idmap.add id new_id Idmap.empty in *) +(* (bt,Name new_id,t):: *) +(* (change_vars_in_binder mapping new_ctxt), *) +(* change_vars mapping new_b *) +(* | _ -> (bt,n,t)::new_ctxt,new_b *) +(* in *) +(* alpha_ctxt *) let apply_args ctxt body args = let need_convert_id avoid id = List.exists (is_free_in id) args || List.mem id avoid in - let need_convert avoid = function - | Anonymous -> false - | Name id -> need_convert_id avoid id + let need_convert avoid bt = + List.exists (need_convert_id avoid) (ids_of_binder bt) in - let add_name na avoid = +(* let add_name na avoid = *) +(* match na with *) +(* | Anonymous -> avoid *) +(* | Name id -> id::avoid *) +(* in *) + let next_name_away (na:name) (mapping: identifier Idmap.t) (avoid: identifier list) = match na with - | Anonymous -> avoid - | Name id -> id::avoid + | Name id when List.mem id avoid -> + let new_id = Nameops.next_ident_away id avoid in + Name new_id,Idmap.add id new_id mapping,new_id::avoid + | _ -> na,mapping,avoid in - let next_name_away na avoid = - match na with - | Anonymous -> anomaly "next_name_away" - | Name id -> - let new_id = Nameops.next_ident_away id avoid in - Name new_id,Idmap.add id new_id Idmap.empty,new_id::avoid + let next_bt_away bt (avoid:identifier list) = + match bt with + | LetIn na -> + let new_na,mapping,new_avoid = next_name_away na Idmap.empty avoid in + LetIn new_na,mapping,new_avoid + | Prod na -> + let new_na,mapping,new_avoid = next_name_away na Idmap.empty avoid in + Prod new_na,mapping,new_avoid + | Lambda na -> + let new_na,mapping,new_avoid = next_name_away na Idmap.empty avoid in + Lambda new_na,mapping,new_avoid +(* | LetTuple (nal,na) -> *) +(* let rev_new_nal,mapping,new_avoid = *) +(* List.fold_left *) +(* (fun (nal,mapping,(avoid:identifier list)) na -> *) +(* let new_na,new_mapping,new_avoid = next_name_away na mapping avoid in *) +(* (new_na::nal,new_mapping,new_avoid) *) +(* ) *) +(* ([],Idmap.empty,avoid) *) +(* nal *) +(* in *) +(* (LetTuple(List.rev rev_new_nal,na),mapping,new_avoid) *) in let rec do_apply avoid ctxt body args = match ctxt,args with @@ -129,9 +217,9 @@ let apply_args ctxt body args = | [],_ -> (* no more fun *) let f,args' = raw_decompose_app body in (ctxt,mkRApp(f,args'@args)) - | (Lambda,Anonymous,t)::ctxt',arg::args' -> + | (Lambda Anonymous,t)::ctxt',arg::args' -> do_apply avoid ctxt' body args' - | (Lambda,Name id,t)::ctxt',arg::args' -> + | (Lambda (Name id),t)::ctxt',arg::args' -> let new_avoid,new_ctxt',new_body,new_id = if need_convert_id avoid id then @@ -139,12 +227,8 @@ let apply_args ctxt body args = let new_id = Nameops.next_ident_away id new_avoid in let new_avoid' = new_id :: new_avoid in let mapping = Idmap.add id new_id Idmap.empty in - let new_ctxt' = - (change_vars_in_binder mapping ctxt') - in - let new_body = - (change_vars mapping body) - in + let new_ctxt' = change_vars_in_binder mapping ctxt' in + let new_body = change_vars mapping body in new_avoid',new_ctxt',new_body,new_id else id::avoid,ctxt',body,id @@ -152,24 +236,24 @@ let apply_args ctxt body args = let new_body = replace_var_by_term new_id arg new_body in let new_ctxt' = replace_var_by_term_in_binder new_id arg new_ctxt' in do_apply avoid new_ctxt' new_body args' - | (bt,na,t)::ctxt',_ -> - let new_avoid,new_ctxt',new_body,new_na = - let new_avoid = add_name na avoid in - if need_convert avoid na + | (bt,t)::ctxt',_ -> + let new_avoid,new_ctxt',new_body,new_bt = + let new_avoid = add_bt_names bt avoid in + if need_convert avoid bt then - let new_na,mapping,new_avoid = next_name_away na new_avoid in - ( - new_avoid, - change_vars_in_binder mapping ctxt', - change_vars mapping body, - new_na + let new_bt,mapping,new_avoid = next_bt_away bt new_avoid in + ( + new_avoid, + change_vars_in_binder mapping ctxt', + change_vars mapping body, + new_bt ) - else new_avoid,ctxt',body,na + else new_avoid,ctxt',body,bt in let new_ctxt',new_body = do_apply new_avoid new_ctxt' new_body args in - (bt,new_na,t)::new_ctxt',new_body + (new_bt,t)::new_ctxt',new_body in do_apply [] ctxt body args @@ -195,10 +279,16 @@ let combine_lam n t b = let combine_prod n t b = - { context = t.context@((Prod,n,t.value)::b.context); value = b.value} + { context = t.context@((Prod n,t.value)::b.context); value = b.value} let combine_letin n t b = - { context = t.context@((LetIn,n,t.value)::b.context); value = b.value} + { context = t.context@((LetIn n,t.value)::b.context); value = b.value} + +(* let combine_tuple nal na b in_e = *) +(* { *) +(* context = b.context@(LetTuple(nal,na),b.value)::in_e.context; *) +(* value = in_e.value *) +(* } *) let mk_result ctxt value avoid = { @@ -235,7 +325,8 @@ let make_discr_match brl = make_discr_match_brl i brl) -let rec build_entry_lc funnames avoid rt : rawconstr build_entry_return (* (raw_context*rawconstr) list *)= +let rec build_entry_lc funnames avoid rt : rawconstr build_entry_return = +(* Pp.msgnl (str " Entering : " ++ Printer.pr_rawconstr rt); *) match rt with | RRef _ | RVar _ | REvar _ | RPatVar _ | RSort _ | RHole _ -> mk_result [] rt avoid @@ -260,8 +351,8 @@ let rec build_entry_lc funnames avoid rt : rawconstr build_entry_return (* (raw List.map (fun arg_res -> let new_hyps = - [Prod,Name res,mkRHole (); - Prod,Anonymous,mkRApp(res_rt,(mkRVar id)::arg_res.value)] + [Prod (Name res),mkRHole (); + Prod Anonymous,mkRApp(res_rt,(mkRVar id)::arg_res.value)] in {context = arg_res.context@new_hyps; value = res_rt } ) @@ -323,8 +414,8 @@ let rec build_entry_lc funnames avoid rt : rawconstr build_entry_return (* (raw | RCases(_,_,el,brl) -> let make_discr = make_discr_match brl in build_entry_lc_from_case funnames make_discr el brl avoid - | RLetTuple _ -> error "Not handled RLetTuple" | RIf _ -> error "Not handled RIf" + | RLetTuple _ -> error "Not handled RLetTuple" | RRec _ -> error "Not handled RRec" | RCast _ -> error "Not handled RCast" | RDynamic _ -> error "Not handled RDynamic" @@ -394,13 +485,13 @@ and build_entry_lc_from_case_term funname make_discr patterns_to_prevent brl avo avoid matched_expr in - let ids = List.map (fun id -> Prod,Name id,mkRHole ()) idl in + let ids = List.map (fun id -> Prod (Name id),mkRHole ()) idl in let those_pattern_preconds = ( List.map2 (fun pat e -> let pat_as_term = pattern_to_term pat in - (Prod,Anonymous,raw_make_eq pat_as_term e) + (Prod Anonymous,raw_make_eq pat_as_term e) ) patl matched_expr.value @@ -413,42 +504,10 @@ and build_entry_lc_from_case_term funname make_discr patterns_to_prevent brl avo List.for_all (fun x -> x) unif) patterns_to_prevent then let i = List.length patterns_to_prevent in - [(Prod,Anonymous,make_discr (List.map pattern_to_term patl) i )] + [(Prod Anonymous,make_discr (List.map pattern_to_term patl) i )] else [] ) -(* List.fold_right *) -(* (fun (unifl,neql) acc -> *) -(* let unif,eqs : bool list * bool list = *) -(* List.split (List.map2 (fun x y -> x y) unifl patl) *) -(* in *) -(* (\* all the pattern must be unifiables *\) *) -(* if List.for_all (fun x -> x) unif (\* List.for_all2 (fun unif pat -> unif pat) unifl patl *\) *) -(* then *) -(* let precond = *) -(* List.map2 *) -(* (fun neq pat -> *) -(* let pat_as_term = pattern_to_term pat in *) -(* (neq new_avoid pat_as_term) *) -(* ) *) -(* neql patl *) -(* in *) -(* let precond = *) -(* List.fold_right2 *) -(* (fun precond eq acc -> *) -(* if not eq then precond::acc else acc *) -(* ) *) -(* precond *) -(* eqs *) -(* [] *) -(* in *) -(* try *) -(* (Prod,Anonymous,raw_make_or_list precond)::acc *) -(* with Invalid_argument "mk_or" -> acc *) -(* else acc *) -(* ) *) -(* patterns_to_prevent *) -(* [] *) in let return_res = build_entry_lc funname new_avoid return in let this_branch_res = @@ -462,103 +521,6 @@ and build_entry_lc_from_case_term funname make_discr patterns_to_prevent brl avo in { brl'_res with result = this_branch_res@brl'_res.result } - - -(* and build_entry_lc_from_case_term funname patterns_to_prevent brl avoid *) -(* matched_expr = *) -(* match brl with *) -(* | [] -> (\* computed_branches *\) {result = [];to_avoid = avoid} *) -(* | br::brl' -> *) -(* let _,idl,patl,return = alpha_br avoid br in *) -(* let new_avoid = idl@avoid in *) -(* let e_ctxt,el = (matched_expr.context,matched_expr.value) in *) -(* if (List.length patl) <> (List.length el) *) -(* then error ("Pattern matching on product: not yet implemented"); *) -(* let not_those_patterns : (identifier list -> rawconstr -> rawconstr) list = *) -(* List.map *) -(* (fun pat -> *) -(* fun avoid pat'_as_term -> *) -(* let renamed_pat,_,_ = alpha_pat avoid pat in *) -(* let pat_ids = get_pattern_id renamed_pat in *) -(* List.fold_right *) -(* (fun id acc -> mkRProd (Name id,mkRHole (),acc)) *) -(* pat_ids *) -(* (raw_make_neq pat'_as_term (pattern_to_term renamed_pat)) *) -(* ) *) -(* patl *) -(* in *) -(* let unify_with_those_patterns : (cases_pattern -> bool*bool) list = *) -(* List.map (fun pat pat' -> are_unifiable pat pat',eq_cases_pattern pat pat') patl *) -(* in *) -(* let brl'_res = *) -(* build_entry_lc_from_case_term *) -(* funname *) -(* ((unify_with_those_patterns,not_those_patterns)::patterns_to_prevent) *) -(* brl' *) -(* avoid *) -(* matched_expr *) -(* in *) -(* let ids = List.map (fun id -> Prod,Name id,mkRHole ()) idl in *) -(* let those_pattern_preconds = *) -(* ( *) -(* List.map2 *) -(* (fun pat e -> *) -(* let pat_as_term = pattern_to_term pat in *) -(* (Prod,Anonymous,raw_make_eq pat_as_term e) *) -(* ) *) -(* patl *) -(* el *) -(* ) *) -(* @ *) -(* List.fold_right *) -(* (fun (unifl,neql) acc -> *) -(* let unif,eqs : bool list * bool list = *) -(* List.split (List.map2 (fun x y -> x y) unifl patl) *) -(* in *) -(* (\* all the pattern must be unifiables *\) *) -(* if List.for_all (fun x -> x) unif (\* List.for_all2 (fun unif pat -> unif pat) unifl patl *\) *) -(* then *) -(* let precond = *) -(* List.map2 *) -(* (fun neq pat -> *) -(* let pat_as_term = pattern_to_term pat in *) -(* (neq new_avoid pat_as_term) *) -(* ) *) -(* neql patl *) -(* in *) -(* let precond = *) -(* List.fold_right2 *) -(* (fun precond eq acc -> *) -(* if not eq then precond::acc else acc *) -(* ) *) -(* precond *) -(* eqs *) -(* [] *) -(* in *) -(* try *) -(* (Prod,Anonymous,raw_make_or_list precond)::acc *) -(* with Invalid_argument "mk_or" -> acc *) -(* else acc *) -(* ) *) -(* patterns_to_prevent *) -(* [] *) -(* in *) -(* let return_res = build_entry_lc funname new_avoid return in *) -(* let this_branch_res = *) -(* List.map *) -(* (fun res -> *) -(* { context = e_ctxt@ids@those_pattern_preconds@res.context ; *) -(* value=res.value} *) -(* ) *) -(* return_res.result *) -(* in *) -(* { brl'_res with result = this_branch_res@brl'_res.result } *) - - - - - - let is_res id = try @@ -625,13 +587,33 @@ let rec rebuild_cons relname args crossed_types rt = | RLetIn(_,n,t,b) -> begin let not_free_in_t id = not (is_free_in id t) in - let new_b,id_to_exclude = rebuild_cons relname args (t::crossed_types) b in + let new_b,id_to_exclude = + rebuild_cons relname args (t::crossed_types) b in match n with | Name id when Idset.mem id id_to_exclude -> new_b,Idset.remove id (Idset.filter not_free_in_t id_to_exclude) | _ -> RLetIn(dummy_loc,n,t,new_b), Idset.filter not_free_in_t id_to_exclude end + | RLetTuple(_,nal,(na,rto),t,b) -> + assert (rto=None); + begin + let not_free_in_t id = not (is_free_in id t) in + let new_t,id_to_exclude' = + rebuild_cons relname args (crossed_types) t + in + let new_b,id_to_exclude = + rebuild_cons relname args (t::crossed_types) b + in +(* match n with *) +(* | Name id when Idset.mem id id_to_exclude -> *) +(* new_b,Idset.remove id (Idset.filter not_free_in_t id_to_exclude) *) +(* | _ -> *) + RLetTuple(dummy_loc,nal,(na,None),t,new_b), + Idset.filter not_free_in_t (Idset.union id_to_exclude id_to_exclude') + + end + | _ -> mkRApp(mkRVar relname,args@[rt]),Idset.empty @@ -642,14 +624,14 @@ let rec compute_cst_params relnames params = function compute_cst_params_from_app [] (params,rtl) | RApp(_,f,args) -> List.fold_left (compute_cst_params relnames) params (f::args) - | RLambda(_,_,t,b) | RProd(_,_,t,b) | RLetIn(_,_,t,b) -> + | RLambda(_,_,t,b) | RProd(_,_,t,b) | RLetIn(_,_,t,b) | RLetTuple(_,_,_,t,b) -> let t_params = compute_cst_params relnames params t in compute_cst_params relnames t_params b | RCases _ -> params (* If there is still cases at this point they can only be discriminitation ones *) | RSort _ -> params | RHole _ -> params - | RLetTuple _ | RIf _ | RRec _ | RCast _ | RDynamic _ -> + | RIf _ | RRec _ | RCast _ | RDynamic _ -> raise (UserError("compute_cst_params", str "Not handled case")) and compute_cst_params_from_app acc (params,rtl) = match params,rtl with @@ -691,7 +673,7 @@ let compute_params_name relnames args csts = -let build_inductive funnames funsargs returned_types (rtl:rawconstr list) = +let build_inductive parametrize funnames funsargs returned_types (rtl:rawconstr list) = let funnames_as_set = List.fold_right Idset.add funnames Idset.empty in let funnames = Array.of_list funnames in let funsargs = Array.of_list funsargs in @@ -702,20 +684,21 @@ let build_inductive funnames funsargs returned_types (rtl:rawconstr list) = let relnames_as_set = Array.fold_right Idset.add relnames Idset.empty in let resa = Array.map (build_entry_lc funnames_as_set []) rta in let constr i res = - List.map (function result (* (args',concl') *) -> - let rt = compose_raw_context result.context result.value in -(* Pp.msgnl (str "raw constr " ++ pr_rawconstr rt); *) - fst ( - rebuild_cons relnames.(i) - (List.map (function - (Anonymous,_) -> mkRVar(fresh_id res.to_avoid "x__") - | Name id, _ -> mkRVar id - ) - funsargs.(i)) - [] - rt - ) - ) + List.map + (function result (* (args',concl') *) -> + let rt = compose_raw_context result.context result.value in +(* Pp.msgnl (str "raw constr " ++ pr_rawconstr rt); *) + fst ( + rebuild_cons relnames.(i) + (List.map (function + (Anonymous,_) -> mkRVar(fresh_id res.to_avoid "x__") + | Name id, _ -> mkRVar id + ) + funsargs.(i)) + [] + rt + ) + ) res.result in let next_constructor_id = ref (-1) in @@ -728,7 +711,10 @@ let build_inductive funnames funsargs returned_types (rtl:rawconstr list) = in let rel_constructors = Array.mapi rel_constructors resa in let rels_params = - compute_params_name relnames_as_set funsargs rel_constructors + if parametrize + then + compute_params_name relnames_as_set funsargs rel_constructors + else [] in let nrel_params = List.length rels_params in let rel_constructors = -- cgit v1.2.3