From 6ebd4c4ad28d46965623e72d8654c36fcc6fe9b0 Mon Sep 17 00:00:00 2001 From: glondu Date: Fri, 24 Dec 2010 23:49:17 +0000 Subject: Rename files in funind to respect new conventions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13755 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/funind/glob_term_to_relation.ml | 1419 ++++++++++++++++++++++++++++++ plugins/funind/glob_term_to_relation.mli | 16 + plugins/funind/glob_termops.ml | 718 +++++++++++++++ plugins/funind/glob_termops.mli | 126 +++ plugins/funind/indfun.ml | 2 +- plugins/funind/merge.ml | 2 +- plugins/funind/rawterm_to_relation.ml | 1419 ------------------------------ plugins/funind/rawterm_to_relation.mli | 16 - plugins/funind/rawtermops.ml | 718 --------------- plugins/funind/rawtermops.mli | 126 --- plugins/funind/recdef_plugin.mllib | 4 +- 11 files changed, 2283 insertions(+), 2283 deletions(-) create mode 100644 plugins/funind/glob_term_to_relation.ml create mode 100644 plugins/funind/glob_term_to_relation.mli create mode 100644 plugins/funind/glob_termops.ml create mode 100644 plugins/funind/glob_termops.mli delete mode 100644 plugins/funind/rawterm_to_relation.ml delete mode 100644 plugins/funind/rawterm_to_relation.mli delete mode 100644 plugins/funind/rawtermops.ml delete mode 100644 plugins/funind/rawtermops.mli diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml new file mode 100644 index 0000000000..ce224d1aac --- /dev/null +++ b/plugins/funind/glob_term_to_relation.ml @@ -0,0 +1,1419 @@ +open Printer +open Pp +open Names +open Term +open Glob_term +open Libnames +open Indfun_common +open Util +open Glob_termops + +let observe strm = + if do_observe () + then Pp.msgnl strm + else () +let observennl strm = + if do_observe () + then Pp.msg strm + else () + + +type binder_type = + | Lambda of name + | Prod of name + | LetIn of name + +type glob_context = (binder_type*glob_constr) list + +(* + compose_glob_context [(bt_1,n_1,t_1);......] rt returns + b_1(n_1,t_1,.....,bn(n_k,t_k,rt)) where the b_i's are the + binders corresponding to the bt_i's +*) +let compose_glob_context = + let compose_binder (bt,t) acc = + match bt with + | Lambda n -> mkRLambda(n,t,acc) + | Prod n -> mkRProd(n,t,acc) + | LetIn n -> mkRLetIn(n,t,acc) + in + List.fold_right compose_binder + + +(* + The main part deals with building a list of globalized constructor expressions + from the rhs of a fixpoint equation. +*) + +type 'a build_entry_pre_return = + { + context : glob_context; (* the binding context of the result *) + value : 'a; (* The value *) + } + +type 'a build_entry_return = + { + result : 'a build_entry_pre_return list; + to_avoid : identifier list + } + +(* + [combine_results combine_fun res1 res2] combine two results [res1] and [res2] + w.r.t. [combine_fun]. + + Informally, both [res1] and [res2] are lists of "constructors" [res1_1;...] + and [res2_1,....] and we need to produce + [combine_fun res1_1 res2_1;combine_fun res1_1 res2_2;........] +*) + +let combine_results + (combine_fun : 'a build_entry_pre_return -> 'b build_entry_pre_return -> + 'c build_entry_pre_return + ) + (res1: 'a build_entry_return) + (res2 : 'b build_entry_return) + : 'c build_entry_return + = + let pre_result = List.map + ( fun res1 -> (* for each result in arg_res *) + List.map (* we add it in each args_res *) + (fun res2 -> + combine_fun res1 res2 + ) + res2.result + ) + res1.result + in (* and then we flatten the map *) + { + result = List.concat pre_result; + to_avoid = list_union res1.to_avoid res2.to_avoid + } + + +(* + The combination function for an argument with a list of argument +*) + +let combine_args arg args = + { + context = arg.context@args.context; + (* Note that the binding context of [arg] MUST be placed before the one of + [args] in order to preserve possible type dependencies + *) + value = arg.value::args.value; + } + + +let ids_of_binder = function + | LetIn Anonymous | Prod Anonymous | Lambda Anonymous -> [] + | LetIn (Name id) | Prod (Name id) | Lambda (Name id) -> [id] + +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 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 bt = + List.exists (need_convert_id avoid) (ids_of_binder bt) + in + let next_name_away (na:name) (mapping: identifier Idmap.t) (avoid: identifier list) = + match na with + | Name id when List.mem id avoid -> + let new_id = Namegen.next_ident_away id avoid in + Name new_id,Idmap.add id new_id mapping,new_id::avoid + | _ -> na,mapping,avoid + in + 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 + in + let rec do_apply avoid ctxt body args = + match ctxt,args with + | _,[] -> (* No more args *) + (ctxt,body) + | [],_ -> (* no more fun *) + let f,args' = glob_decompose_app body in + (ctxt,mkRApp(f,args'@args)) + | (Lambda Anonymous,t)::ctxt',arg::args' -> + do_apply avoid ctxt' body args' + | (Lambda (Name id),t)::ctxt',arg::args' -> + let new_avoid,new_ctxt',new_body,new_id = + if need_convert_id avoid id + then + let new_avoid = id::avoid in + let new_id = Namegen.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 + new_avoid',new_ctxt',new_body,new_id + else + id::avoid,ctxt',body,id + in + 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,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_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,bt + in + let new_ctxt',new_body = + do_apply new_avoid new_ctxt' new_body args + in + (new_bt,t)::new_ctxt',new_body + in + do_apply [] ctxt body args + + +let combine_app f args = + let new_ctxt,new_value = apply_args f.context f.value args.value in + { + (* Note that the binding context of [args] MUST be placed before the one of + the applied value in order to preserve possible type dependencies + *) + context = args.context@new_ctxt; + value = new_value; + } + +let combine_lam n t b = + { + context = []; + value = mkRLambda(n, compose_glob_context t.context t.value, + compose_glob_context b.context b.value ) + } + + + +let combine_prod n t b = + { 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} + + +let mk_result ctxt value avoid = + { + result = + [{context = ctxt; + value = value}] + ; + to_avoid = avoid + } +(************************************************* + Some functions to deal with overlapping patterns +**************************************************) + +let coq_True_ref = + lazy (Coqlib.gen_reference "" ["Init";"Logic"] "True") + +let coq_False_ref = + lazy (Coqlib.gen_reference "" ["Init";"Logic"] "False") + +(* + [make_discr_match_el \[e1,...en\]] builds match e1,...,en with + (the list of expresions on which we will do the matching) + *) +let make_discr_match_el = + List.map (fun e -> (e,(Anonymous,None))) + +(* + [make_discr_match_brl i \[pat_1,...,pat_n\]] constructs a discrimination pattern matching on the ith expression. + that is. + match ?????? with \\ + | pat_1 => False \\ + | pat_{i-1} => False \\ + | pat_i => True \\ + | pat_{i+1} => False \\ + \vdots + | pat_n => False + end +*) +let make_discr_match_brl i = + list_map_i + (fun j (_,idl,patl,_) -> + if j=i + then (dummy_loc,idl,patl, mkRRef (Lazy.force coq_True_ref)) + else (dummy_loc,idl,patl, mkRRef (Lazy.force coq_False_ref)) + ) + 0 +(* + [make_discr_match brl el i] generates an hypothesis such that it reduce to true iff + brl_{i} is the first branch matched by [el] + + Used when we want to simulate the coq pattern matching algorithm +*) +let make_discr_match brl = + fun el i -> + mkRCases(None, + make_discr_match_el el, + make_discr_match_brl i brl) + +let pr_name = function + | Name id -> Ppconstr.pr_id id + | Anonymous -> str "_" + +(**********************************************************************) +(* functions used to build case expression from lettuple and if ones *) +(**********************************************************************) + +(* [build_constructors_of_type] construct the array of pattern of its inductive argument*) +let build_constructors_of_type ind' argl = + let (mib,ind) = Inductive.lookup_mind_specif (Global.env()) ind' in + let npar = mib.Declarations.mind_nparams in + Array.mapi (fun i _ -> + let construct = ind',i+1 in + let constructref = ConstructRef(construct) in + let _implicit_positions_of_cst = + Impargs.implicits_of_global constructref + in + let cst_narg = + Inductiveops.mis_constructor_nargs_env + (Global.env ()) + construct + in + let argl = + if argl = [] + then + Array.to_list + (Array.init (cst_narg - npar) (fun _ -> mkRHole ()) + ) + else argl + in + let pat_as_term = + mkRApp(mkRRef (ConstructRef(ind',i+1)),argl) + in + cases_pattern_of_glob_constr Anonymous pat_as_term + ) + ind.Declarations.mind_consnames + +(* [find_type_of] very naive attempts to discover the type of an if or a letin *) +let rec find_type_of nb b = + let f,_ = glob_decompose_app b in + match f with + | GRef(_,ref) -> + begin + let ind_type = + match ref with + | VarRef _ | ConstRef _ -> + let constr_of_ref = constr_of_global ref in + let type_of_ref = Typing.type_of (Global.env ()) Evd.empty constr_of_ref in + let (_,ret_type) = Reduction.dest_prod (Global.env ()) type_of_ref in + let ret_type,_ = decompose_app ret_type in + if not (isInd ret_type) then + begin +(* Pp.msgnl (str "not an inductive" ++ pr_lconstr ret_type); *) + raise (Invalid_argument "not an inductive") + end; + destInd ret_type + | IndRef ind -> ind + | ConstructRef c -> fst c + in + let _,ind_type_info = Inductive.lookup_mind_specif (Global.env()) ind_type in + if not (Array.length ind_type_info.Declarations.mind_consnames = nb ) + then raise (Invalid_argument "find_type_of : not a valid inductive"); + ind_type + end + | GCast(_,b,_) -> find_type_of nb b + | GApp _ -> assert false (* we have decomposed any application via glob_decompose_app *) + | _ -> raise (Invalid_argument "not a ref") + + + + +(******************) +(* Main functions *) +(******************) + + + +let raw_push_named (na,raw_value,raw_typ) env = + match na with + | Anonymous -> env + | Name id -> + let value = Option.map (Pretyping.Default.understand Evd.empty env) raw_value in + let typ = Pretyping.Default.understand_type Evd.empty env raw_typ in + Environ.push_named (id,value,typ) env + + +let add_pat_variables pat typ env : Environ.env = + let rec add_pat_variables env pat typ : Environ.env = + observe (str "new rel env := " ++ Printer.pr_rel_context_of env); + + match pat with + | PatVar(_,na) -> Environ.push_rel (na,None,typ) env + | PatCstr(_,c,patl,na) -> + let Inductiveops.IndType(indf,indargs) = + try Inductiveops.find_rectype env Evd.empty typ + with Not_found -> assert false + in + let constructors = Inductiveops.get_constructors env indf in + let constructor : Inductiveops.constructor_summary = List.find (fun cs -> cs.Inductiveops.cs_cstr = c) (Array.to_list constructors) in + let cs_args_types :types list = List.map (fun (_,_,t) -> t) constructor.Inductiveops.cs_args in + List.fold_left2 add_pat_variables env patl (List.rev cs_args_types) + in + let new_env = add_pat_variables env pat typ in + let res = + fst ( + Sign.fold_rel_context + (fun (na,v,t) (env,ctxt) -> + match na with + | Anonymous -> assert false + | Name id -> + let new_t = substl ctxt t in + let new_v = Option.map (substl ctxt) v in + observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++ + str "old type := " ++ Printer.pr_lconstr t ++ fnl () ++ + str "new type := " ++ Printer.pr_lconstr new_t ++ fnl () ++ + Option.fold_right (fun v _ -> str "old value := " ++ Printer.pr_lconstr v ++ fnl ()) v (mt ()) ++ + Option.fold_right (fun v _ -> str "new value := " ++ Printer.pr_lconstr v ++ fnl ()) new_v (mt ()) + ); + (Environ.push_named (id,new_v,new_t) env,mkVar id::ctxt) + ) + (Environ.rel_context new_env) + ~init:(env,[]) + ) + in + observe (str "new var env := " ++ Printer.pr_named_context_of res); + res + + + + +let rec pattern_to_term_and_type env typ = function + | PatVar(loc,Anonymous) -> assert false + | PatVar(loc,Name id) -> + mkRVar id + | PatCstr(loc,constr,patternl,_) -> + let cst_narg = + Inductiveops.mis_constructor_nargs_env + (Global.env ()) + constr + in + let Inductiveops.IndType(indf,indargs) = + try Inductiveops.find_rectype env Evd.empty typ + with Not_found -> assert false + in + let constructors = Inductiveops.get_constructors env indf in + let constructor = List.find (fun cs -> cs.Inductiveops.cs_cstr = constr) (Array.to_list constructors) in + let cs_args_types :types list = List.map (fun (_,_,t) -> t) constructor.Inductiveops.cs_args in + let _,cstl = Inductiveops.dest_ind_family indf in + let csta = Array.of_list cstl in + let implicit_args = + Array.to_list + (Array.init + (cst_narg - List.length patternl) + (fun i -> Detyping.detype false [] (Termops.names_of_rel_context env) csta.(i)) + ) + in + let patl_as_term = + List.map2 (pattern_to_term_and_type env) (List.rev cs_args_types) patternl + in + mkRApp(mkRRef(ConstructRef constr), + implicit_args@patl_as_term + ) + +(* [build_entry_lc funnames avoid rt] construct the list (in fact a build_entry_return) + of constructors corresponding to [rt] when replacing calls to [funnames] by calls to the + corresponding graphs. + + + The idea to transform a term [t] into a list of constructors [lc] is the following: + \begin{itemize} + \item if the term is a binder (bind x, body) then first compute [lc'] the list corresponding + to [body] and add (bind x. _) to each elements of [lc] + \item if the term has the form (g t1 ... ... tn) where g does not appears in (fnames) + then compute [lc1] ... [lcn] the lists of constructors corresponding to [t1] ... [tn], + then combine those lists and [g] as follows~: for each element [c1,...,cn] of [lc1\times...\times lcn], + [g c1 ... cn] is an element of [lc] + \item if the term has the form (f t1 .... tn) where [f] appears in [fnames] then + compute [lc1] ... [lcn] the lists of constructors corresponding to [t1] ... [tn], + then compute those lists and [f] as follows~: for each element [c1,...,cn] of [lc1\times...\times lcn] + create a new variable [res] and [forall res, R_f c1 ... cn res] is in [lc] + \item if the term is a cast just treat its body part + \item + if the term is a match, an if or a lettuple then compute the lists corresponding to each branch of the case + and concatenate them (informally, each branch of a match produces a new constructor) + \end{itemize} + + WARNING: The terms constructed here are only USING the glob_constr syntax but are highly bad formed. + We must wait to have complete all the current calculi to set the recursive calls. + At this point, each term [f t1 ... tn] (where f appears in [funnames]) is replaced by + a pseudo term [forall res, res t1 ... tn, res]. A reconstruction phase is done later. + We in fact not create a constructor list since then end of each constructor has not the expected form + but only the value of the function +*) + + +let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = + observe (str " Entering : " ++ Printer.pr_glob_constr rt); + match rt with + | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> + (* do nothing (except changing type of course) *) + mk_result [] rt avoid + | GApp(_,_,_) -> + let f,args = glob_decompose_app rt in + let args_res : (glob_constr list) build_entry_return = + List.fold_right (* create the arguments lists of constructors and combine them *) + (fun arg ctxt_argsl -> + let arg_res = build_entry_lc env funnames ctxt_argsl.to_avoid arg in + combine_results combine_args arg_res ctxt_argsl + ) + args + (mk_result [] [] avoid) + in + begin + match f with + | GLambda _ -> + let rec aux t l = + match l with + | [] -> t + | u::l -> + match t with + | GLambda(loc,na,_,nat,b) -> + GLetIn(dummy_loc,na,u,aux b l) + | _ -> + GApp(dummy_loc,t,l) + in + build_entry_lc env funnames avoid (aux f args) + | GVar(_,id) when Idset.mem id funnames -> + (* if we have [f t1 ... tn] with [f]$\in$[fnames] + then we create a fresh variable [res], + add [res] and its "value" (i.e. [res v1 ... vn]) to each + pseudo constructor build for the arguments (i.e. a pseudo context [ctxt] and + a pseudo value "v1 ... vn". + The "value" of this branch is then simply [res] + *) + let rt_as_constr = Pretyping.Default.understand Evd.empty env rt in + let rt_typ = Typing.type_of env Evd.empty rt_as_constr in + let res_raw_type = Detyping.detype false [] (Termops.names_of_rel_context env) rt_typ in + let res = fresh_id args_res.to_avoid "res" in + let new_avoid = res::args_res.to_avoid in + let res_rt = mkRVar res in + let new_result = + List.map + (fun arg_res -> + let new_hyps = + [Prod (Name res),res_raw_type; + Prod Anonymous,mkRApp(res_rt,(mkRVar id)::arg_res.value)] + in + {context = arg_res.context@new_hyps; value = res_rt } + ) + args_res.result + in + { result = new_result; to_avoid = new_avoid } + | GVar _ | GEvar _ | GPatVar _ | GHole _ | GSort _ | GRef _ -> + (* if have [g t1 ... tn] with [g] not appearing in [funnames] + then + foreach [ctxt,v1 ... vn] in [args_res] we return + [ctxt, g v1 .... vn] + *) + { + args_res with + result = + List.map + (fun args_res -> + {args_res with value = mkRApp(f,args_res.value)}) + args_res.result + } + | GApp _ -> assert false (* we have collected all the app in [glob_decompose_app] *) + | GLetIn(_,n,t,b) -> + (* if we have [(let x := v in b) t1 ... tn] , + we discard our work and compute the list of constructor for + [let x = v in (b t1 ... tn)] up to alpha conversion + *) + let new_n,new_b,new_avoid = + match n with + | Name id when List.exists (is_free_in id) args -> + (* need to alpha-convert the name *) + let new_id = Namegen.next_ident_away id avoid in + let new_avoid = id:: avoid in + let new_b = + replace_var_by_term + id + (GVar(dummy_loc,id)) + b + in + (Name new_id,new_b,new_avoid) + | _ -> n,b,avoid + in + build_entry_lc + env + funnames + avoid + (mkRLetIn(new_n,t,mkRApp(new_b,args))) + | GCases _ | GIf _ | GLetTuple _ -> + (* we have [(match e1, ...., en with ..... end) t1 tn] + we first compute the result from the case and + then combine each of them with each of args one + *) + let f_res = build_entry_lc env funnames args_res.to_avoid f in + combine_results combine_app f_res args_res + | GDynamic _ ->error "Not handled GDynamic" + | GCast(_,b,_) -> + (* for an applied cast we just trash the cast part + and restart the work. + + WARNING: We need to restart since [b] itself should be an application term + *) + build_entry_lc env funnames avoid (mkRApp(b,args)) + | GRec _ -> error "Not handled GRec" + | GProd _ -> error "Cannot apply a type" + end (* end of the application treatement *) + + | GLambda(_,n,_,t,b) -> + (* we first compute the list of constructor + corresponding to the body of the function, + then the one corresponding to the type + and combine the two result + *) + let t_res = build_entry_lc env funnames avoid t in + let new_n = + match n with + | Name _ -> n + | Anonymous -> Name (Indfun_common.fresh_id [] "_x") + in + let new_env = raw_push_named (new_n,None,t) env in + let b_res = build_entry_lc new_env funnames avoid b in + combine_results (combine_lam new_n) t_res b_res + | GProd(_,n,_,t,b) -> + (* we first compute the list of constructor + corresponding to the body of the function, + then the one corresponding to the type + and combine the two result + *) + let t_res = build_entry_lc env funnames avoid t in + let new_env = raw_push_named (n,None,t) env in + let b_res = build_entry_lc new_env funnames avoid b in + combine_results (combine_prod n) t_res b_res + | GLetIn(_,n,v,b) -> + (* we first compute the list of constructor + corresponding to the body of the function, + then the one corresponding to the value [t] + and combine the two result + *) + let v_res = build_entry_lc env funnames avoid v in + let v_as_constr = Pretyping.Default.understand Evd.empty env v in + let v_type = Typing.type_of env Evd.empty v_as_constr in + let new_env = + match n with + Anonymous -> env + | Name id -> Environ.push_named (id,Some v_as_constr,v_type) env + in + let b_res = build_entry_lc new_env funnames avoid b in + combine_results (combine_letin n) v_res b_res + | GCases(_,_,_,el,brl) -> + (* we create the discrimination function + and treat the case itself + *) + let make_discr = make_discr_match brl in + build_entry_lc_from_case env funnames make_discr el brl avoid + | GIf(_,b,(na,e_option),lhs,rhs) -> + let b_as_constr = Pretyping.Default.understand Evd.empty env b in + let b_typ = Typing.type_of env Evd.empty b_as_constr in + let (ind,_) = + try Inductiveops.find_inductive env Evd.empty b_typ + with Not_found -> + errorlabstrm "" (str "Cannot find the inductive associated to " ++ + Printer.pr_glob_constr b ++ str " in " ++ + Printer.pr_glob_constr rt ++ str ". try again with a cast") + in + let case_pats = build_constructors_of_type ind [] in + assert (Array.length case_pats = 2); + let brl = + list_map_i + (fun i x -> (dummy_loc,[],[case_pats.(i)],x)) + 0 + [lhs;rhs] + in + let match_expr = + mkRCases(None,[(b,(Anonymous,None))],brl) + in + (* Pp.msgnl (str "new case := " ++ Printer.pr_glob_constr match_expr); *) + build_entry_lc env funnames avoid match_expr + | GLetTuple(_,nal,_,b,e) -> + begin + let nal_as_glob_constr = + List.map + (function + Name id -> mkRVar id + | Anonymous -> mkRHole () + ) + nal + in + let b_as_constr = Pretyping.Default.understand Evd.empty env b in + let b_typ = Typing.type_of env Evd.empty b_as_constr in + let (ind,_) = + try Inductiveops.find_inductive env Evd.empty b_typ + with Not_found -> + errorlabstrm "" (str "Cannot find the inductive associated to " ++ + Printer.pr_glob_constr b ++ str " in " ++ + Printer.pr_glob_constr rt ++ str ". try again with a cast") + in + let case_pats = build_constructors_of_type ind nal_as_glob_constr in + assert (Array.length case_pats = 1); + let br = + (dummy_loc,[],[case_pats.(0)],e) + in + let match_expr = mkRCases(None,[b,(Anonymous,None)],[br]) in + build_entry_lc env funnames avoid match_expr + + end + | GRec _ -> error "Not handled GRec" + | GCast(_,b,_) -> + build_entry_lc env funnames avoid b + | GDynamic _ -> error "Not handled GDynamic" +and build_entry_lc_from_case env funname make_discr + (el:tomatch_tuples) + (brl:Glob_term.cases_clauses) avoid : + glob_constr build_entry_return = + match el with + | [] -> assert false (* this case correspond to match with .... !*) + | el -> + (* this case correspond to + match el with brl end + we first compute the list of lists corresponding to [el] and + combine them . + Then for each elemeent of the combinations, + we compute the result we compute one list per branch in [brl] and + finally we just concatenate those list + *) + let case_resl = + List.fold_right + (fun (case_arg,_) ctxt_argsl -> + let arg_res = build_entry_lc env funname avoid case_arg in + combine_results combine_args arg_res ctxt_argsl + ) + el + (mk_result [] [] avoid) + in + let types = + List.map (fun (case_arg,_) -> + let case_arg_as_constr = Pretyping.Default.understand Evd.empty env case_arg in + Typing.type_of env Evd.empty case_arg_as_constr + ) el + in + (****** The next works only if the match is not dependent ****) + let results = + List.map + (fun ca -> + let res = build_entry_lc_from_case_term + env types + funname (make_discr) + [] brl + case_resl.to_avoid + ca + in + res + ) + case_resl.result + in + { + result = List.concat (List.map (fun r -> r.result) results); + to_avoid = + List.fold_left (fun acc r -> list_union acc r.to_avoid) [] results + } + +and build_entry_lc_from_case_term env types funname make_discr patterns_to_prevent brl avoid + matched_expr = + match brl with + | [] -> (* computed_branches *) {result = [];to_avoid = avoid} + | br::brl' -> + (* alpha convertion to prevent name clashes *) + let _,idl,patl,return = alpha_br avoid br in + let new_avoid = idl@avoid in (* for now we can no more use idl as an indentifier *) + (* building a list of precondition stating that we are not in this branch + (will be used in the following recursive calls) + *) + let new_env = List.fold_right2 add_pat_variables patl types env in + let not_those_patterns : (identifier list -> glob_constr -> glob_constr) list = + List.map2 + (fun pat typ -> + fun avoid pat'_as_term -> + let renamed_pat,_,_ = alpha_pat avoid pat in + let pat_ids = get_pattern_id renamed_pat in + let env_with_pat_ids = add_pat_variables pat typ new_env in + List.fold_right + (fun id acc -> + let typ_of_id = + Typing.type_of env_with_pat_ids Evd.empty (mkVar id) + in + let raw_typ_of_id = + Detyping.detype false [] + (Termops.names_of_rel_context env_with_pat_ids) typ_of_id + in + mkRProd (Name id,raw_typ_of_id,acc)) + pat_ids + (glob_make_neq pat'_as_term (pattern_to_term renamed_pat)) + ) + patl + types + in + (* Checking if we can be in this branch + (will be used in the following recursive calls) + *) + 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 + (* + we first compute the other branch result (in ordrer to keep the order of the matching + as much as possible) + *) + let brl'_res = + build_entry_lc_from_case_term + env + types + funname + make_discr + ((unify_with_those_patterns,not_those_patterns)::patterns_to_prevent) + brl' + avoid + matched_expr + in + (* We now create the precondition of this branch i.e. + 1- the list of variable appearing in the different patterns of this branch and + the list of equation stating than el = patl (List.flatten ...) + 2- If there exists a previous branch which pattern unify with the one of this branch + then a discrimination precond stating that we are not in a previous branch (if List.exists ...) + *) + let those_pattern_preconds = + (List.flatten + ( + list_map3 + (fun pat e typ_as_constr -> + let this_pat_ids = ids_of_pat pat in + let typ = Detyping.detype false [] (Termops.names_of_rel_context new_env) typ_as_constr in + let pat_as_term = pattern_to_term pat in + List.fold_right + (fun id acc -> + if Idset.mem id this_pat_ids + then (Prod (Name id), + let typ_of_id = Typing.type_of new_env Evd.empty (mkVar id) in + let raw_typ_of_id = + Detyping.detype false [] (Termops.names_of_rel_context new_env) typ_of_id + in + raw_typ_of_id + )::acc + else acc + ) + idl + [(Prod Anonymous,glob_make_eq ~typ pat_as_term e)] + ) + patl + matched_expr.value + types + ) + ) + @ + (if List.exists (function (unifl,_) -> + let (unif,_) = + List.split (List.map2 (fun x y -> x y) unifl patl) + in + List.for_all (fun x -> x) unif) patterns_to_prevent + then + let i = List.length patterns_to_prevent in + let pats_as_constr = List.map2 (pattern_to_term_and_type new_env) types patl in + [(Prod Anonymous,make_discr pats_as_constr i )] + else + [] + ) + in + (* We compute the result of the value returned by the branch*) + let return_res = build_entry_lc new_env funname new_avoid return in + (* and combine it with the preconds computed for this branch *) + let this_branch_res = + List.map + (fun res -> + { context = matched_expr.context@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 + String.sub (string_of_id id) 0 3 = "res" + with Invalid_argument _ -> false + + +exception Continue +(* + The second phase which reconstruct the real type of the constructor. + rebuild the globalized constructors expression. + eliminates some meaningless equalities, applies some rewrites...... +*) +let rec rebuild_cons env nb_args relname args crossed_types depth rt = + observe (str "rebuilding : " ++ pr_glob_constr rt); + + match rt with + | GProd(_,n,k,t,b) -> + let not_free_in_t id = not (is_free_in id t) in + let new_crossed_types = t::crossed_types in + begin + match t with + | GApp(_,(GVar(_,res_id) as res_rt),args') when is_res res_id -> + begin + match args' with + | (GVar(_,this_relname))::args' -> + (*i The next call to mk_rel_id is + valid since we are constructing the graph + Ensures by: obvious + i*) + + let new_t = + mkRApp(mkRVar(mk_rel_id this_relname),args'@[res_rt]) + in + let t' = Pretyping.Default.understand Evd.empty env new_t in + let new_env = Environ.push_rel (n,None,t') env in + let new_b,id_to_exclude = + rebuild_cons new_env + nb_args relname + args new_crossed_types + (depth + 1) b + in + mkRProd(n,new_t,new_b), + Idset.filter not_free_in_t id_to_exclude + | _ -> (* the first args is the name of the function! *) + assert false + end + | GApp(loc1,GRef(loc2,eq_as_ref),[ty;GVar(loc3,id);rt]) + when eq_as_ref = Lazy.force Coqlib.coq_eq_ref && n = Anonymous + -> + begin + try + observe (str "computing new type for eq : " ++ pr_glob_constr rt); + let t' = + try Pretyping.Default.understand Evd.empty env t with _ -> raise Continue + in + let is_in_b = is_free_in id b in + let _keep_eq = + not (List.exists (is_free_in id) args) || is_in_b || + List.exists (is_free_in id) crossed_types + in + let new_args = List.map (replace_var_by_term id rt) args in + let subst_b = + if is_in_b then b else replace_var_by_term id rt b + in + let new_env = Environ.push_rel (n,None,t') env in + let new_b,id_to_exclude = + rebuild_cons + new_env + nb_args relname + new_args new_crossed_types + (depth + 1) subst_b + in + mkRProd(n,t,new_b),id_to_exclude + with Continue -> + let jmeq = Libnames.IndRef (destInd (jmeq ())) in + let ty' = Pretyping.Default.understand Evd.empty env ty in + let ind,args' = Inductive.find_inductive env ty' in + let mib,_ = Global.lookup_inductive ind in + let nparam = mib.Declarations.mind_nparams in + let params,arg' = + ((Util.list_chop nparam args')) + in + let rt_typ = + GApp(Util.dummy_loc, + GRef (Util.dummy_loc,Libnames.IndRef ind), + (List.map + (fun p -> Detyping.detype false [] + (Termops.names_of_rel_context env) + p) params)@(Array.to_list + (Array.make + (List.length args' - nparam) + (mkRHole ())))) + in + let eq' = + GApp(loc1,GRef(loc2,jmeq),[ty;GVar(loc3,id);rt_typ;rt]) + in + observe (str "computing new type for jmeq : " ++ pr_glob_constr eq'); + let eq'_as_constr = Pretyping.Default.understand Evd.empty env eq' in + observe (str " computing new type for jmeq : done") ; + let new_args = + match kind_of_term eq'_as_constr with + | App(_,[|_;_;ty;_|]) -> + let ty = Array.to_list (snd (destApp ty)) in + let ty' = snd (Util.list_chop nparam ty) in + List.fold_left2 + (fun acc var_as_constr arg -> + if isRel var_as_constr + then + let (na,_,_) = + Environ.lookup_rel (destRel var_as_constr) env + in + match na with + | Anonymous -> acc + | Name id' -> + (id',Detyping.detype false [] + (Termops.names_of_rel_context env) + arg)::acc + else if isVar var_as_constr + then (destVar var_as_constr,Detyping.detype false [] + (Termops.names_of_rel_context env) + arg)::acc + else acc + ) + [] + arg' + ty' + | _ -> assert false + in + let is_in_b = is_free_in id b in + let _keep_eq = + not (List.exists (is_free_in id) args) || is_in_b || + List.exists (is_free_in id) crossed_types + in + let new_args = + List.fold_left + (fun args (id,rt) -> + List.map (replace_var_by_term id rt) args + ) + args + ((id,rt)::new_args) + in + let subst_b = + if is_in_b then b else replace_var_by_term id rt b + in + let new_env = + let t' = Pretyping.Default.understand Evd.empty env eq' in + Environ.push_rel (n,None,t') env + in + let new_b,id_to_exclude = + rebuild_cons + new_env + nb_args relname + new_args new_crossed_types + (depth + 1) subst_b + in + mkRProd(n,eq',new_b),id_to_exclude + end + (* J.F:. keep this comment it explain how to remove some meaningless equalities + if keep_eq then + mkRProd(n,t,new_b),id_to_exclude + else new_b, Idset.add id id_to_exclude + *) + | _ -> + observe (str "computing new type for prod : " ++ pr_glob_constr rt); + let t' = Pretyping.Default.understand Evd.empty env t in + let new_env = Environ.push_rel (n,None,t') env in + let new_b,id_to_exclude = + rebuild_cons new_env + nb_args relname + args new_crossed_types + (depth + 1) b + in + match n with + | Name id when Idset.mem id id_to_exclude && depth >= nb_args -> + new_b,Idset.remove id + (Idset.filter not_free_in_t id_to_exclude) + | _ -> mkRProd(n,t,new_b),Idset.filter not_free_in_t id_to_exclude + end + | GLambda(_,n,k,t,b) -> + begin + let not_free_in_t id = not (is_free_in id t) in + let new_crossed_types = t :: crossed_types in + observe (str "computing new type for lambda : " ++ pr_glob_constr rt); + let t' = Pretyping.Default.understand Evd.empty env t in + match n with + | Name id -> + let new_env = Environ.push_rel (n,None,t') env in + let new_b,id_to_exclude = + rebuild_cons new_env + nb_args relname + (args@[mkRVar id])new_crossed_types + (depth + 1 ) b + in + if Idset.mem id id_to_exclude && depth >= nb_args + then + new_b, Idset.remove id (Idset.filter not_free_in_t id_to_exclude) + else + GProd(dummy_loc,n,k,t,new_b),Idset.filter not_free_in_t id_to_exclude + | _ -> anomaly "Should not have an anonymous function here" + (* We have renamed all the anonymous functions during alpha_renaming phase *) + + end + | GLetIn(_,n,t,b) -> + begin + let not_free_in_t id = not (is_free_in id t) in + let t' = Pretyping.Default.understand Evd.empty env t in + let type_t' = Typing.type_of env Evd.empty t' in + let new_env = Environ.push_rel (n,Some t',type_t') env in + let new_b,id_to_exclude = + rebuild_cons new_env + nb_args relname + args (t::crossed_types) + (depth + 1 ) b in + match n with + | Name id when Idset.mem id id_to_exclude && depth >= nb_args -> + new_b,Idset.remove id (Idset.filter not_free_in_t id_to_exclude) + | _ -> GLetIn(dummy_loc,n,t,new_b), + Idset.filter not_free_in_t id_to_exclude + end + | GLetTuple(_,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 env + nb_args + relname + args (crossed_types) + depth t + in + let t' = Pretyping.Default.understand Evd.empty env new_t in + let new_env = Environ.push_rel (na,None,t') env in + let new_b,id_to_exclude = + rebuild_cons new_env + nb_args relname + args (t::crossed_types) + (depth + 1) 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) *) +(* | _ -> *) + GLetTuple(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 + + +(* debuging wrapper *) +let rebuild_cons env nb_args relname args crossed_types rt = +(* observennl (str "rebuild_cons : rt := "++ pr_glob_constr rt ++ *) +(* str "nb_args := " ++ str (string_of_int nb_args)); *) + let res = + rebuild_cons env nb_args relname args crossed_types 0 rt + in +(* observe (str " leads to "++ pr_glob_constr (fst res)); *) + res + + +(* naive implementation of parameter detection. + + A parameter is an argument which is only preceded by parameters and whose + calls are all syntaxically equal. + + TODO: Find a valid way to deal with implicit arguments here! +*) +let rec compute_cst_params relnames params = function + | GRef _ | GVar _ | GEvar _ | GPatVar _ -> params + | GApp(_,GVar(_,relname'),rtl) when Idset.mem relname' relnames -> + compute_cst_params_from_app [] (params,rtl) + | GApp(_,f,args) -> + List.fold_left (compute_cst_params relnames) params (f::args) + | GLambda(_,_,_,t,b) | GProd(_,_,_,t,b) | GLetIn(_,_,t,b) | GLetTuple(_,_,_,t,b) -> + let t_params = compute_cst_params relnames params t in + compute_cst_params relnames t_params b + | GCases _ -> + params (* If there is still cases at this point they can only be + discriminitation ones *) + | GSort _ -> params + | GHole _ -> params + | GIf _ | GRec _ | GCast _ | GDynamic _ -> + raise (UserError("compute_cst_params", str "Not handled case")) +and compute_cst_params_from_app acc (params,rtl) = + match params,rtl with + | _::_,[] -> assert false (* the rel has at least nargs + 1 arguments ! *) + | ((Name id,_,is_defined) as param)::params',(GVar(_,id'))::rtl' + when id_ord id id' == 0 && not is_defined -> + compute_cst_params_from_app (param::acc) (params',rtl') + | _ -> List.rev acc + +let compute_params_name relnames (args : (Names.name * Glob_term.glob_constr * bool) list array) csts = + let rels_params = + Array.mapi + (fun i args -> + List.fold_left + (fun params (_,cst) -> compute_cst_params relnames params cst) + args + csts.(i) + ) + args + in + let l = ref [] in + let _ = + try + list_iter_i + (fun i ((n,nt,is_defined) as param) -> + if array_for_all + (fun l -> + let (n',nt',is_defined') = List.nth l i in + n = n' && Topconstr.eq_glob_constr nt nt' && is_defined = is_defined') + rels_params + then + l := param::!l + ) + rels_params.(0) + with _ -> + () + in + List.rev !l + +let rec rebuild_return_type rt = + match rt with + | Topconstr.CProdN(loc,n,t') -> + Topconstr.CProdN(loc,n,rebuild_return_type t') + | Topconstr.CArrow(loc,t,t') -> + Topconstr.CArrow(loc,t,rebuild_return_type t') + | Topconstr.CLetIn(loc,na,t,t') -> + Topconstr.CLetIn(loc,na,t,rebuild_return_type t') + | _ -> Topconstr.CArrow(dummy_loc,rt,Topconstr.CSort(dummy_loc,RType None)) + + +let do_build_inductive + funnames (funsargs: (Names.name * glob_constr * bool) list list) + returned_types + (rtl:glob_constr list) = + let _time1 = System.get_time () in +(* Pp.msgnl (prlist_with_sep fnl Printer.pr_glob_constr rtl); *) + 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 + let returned_types = Array.of_list returned_types in + (* alpha_renaming of the body to prevent variable capture during manipulation *) + let rtl_alpha = List.map (function rt -> expand_as (alpha_rt [] rt)) rtl in + let rta = Array.of_list rtl_alpha in + (*i The next call to mk_rel_id is valid since we are constructing the graph + Ensures by: obvious + i*) + let relnames = Array.map mk_rel_id funnames in + let relnames_as_set = Array.fold_right Idset.add relnames Idset.empty in + (* Construction of the pseudo constructors *) + let env = + Array.fold_right + (fun id env -> + Environ.push_named (id,None,Typing.type_of env Evd.empty (Constrintern.global_reference id)) env + ) + funnames + (Global.env ()) + in + let resa = Array.map (build_entry_lc env funnames_as_set []) rta in + let env_with_graphs = + let rel_arity i funargs = (* Reduilding arities (with parameters) *) + let rel_first_args :(Names.name * Glob_term.glob_constr * bool ) list = + funargs + in + List.fold_right + (fun (n,t,is_defined) acc -> + if is_defined + then + Topconstr.CLetIn(dummy_loc,(dummy_loc, n),Constrextern.extern_glob_constr Idset.empty t, + acc) + else + Topconstr.CProdN + (dummy_loc, + [[(dummy_loc,n)],Topconstr.default_binder_kind,Constrextern.extern_glob_constr Idset.empty t], + acc + ) + ) + rel_first_args + (rebuild_return_type returned_types.(i)) + in + (* We need to lift back our work topconstr but only with all information + We mimick a Set Printing All. + Then save the graphs and reset Printing options to their primitive values + *) + let rel_arities = Array.mapi rel_arity funsargs in + Util.array_fold_left2 (fun env rel_name rel_ar -> + Environ.push_named (rel_name,None, Constrintern.interp_constr Evd.empty env rel_ar) env) env relnames rel_arities + in + (* and of the real constructors*) + let constr i res = + List.map + (function result (* (args',concl') *) -> + let rt = compose_glob_context result.context result.value in + let nb_args = List.length funsargs.(i) in + (* with_full_print (fun rt -> Pp.msgnl (str "glob constr " ++ pr_glob_constr rt)) rt; *) + fst ( + rebuild_cons env_with_graphs nb_args relnames.(i) + [] + [] + rt + ) + ) + res.result + in + (* adding names to constructors *) + let next_constructor_id = ref (-1) in + let mk_constructor_id i = + incr next_constructor_id; + (*i The next call to mk_rel_id is valid since we are constructing the graph + Ensures by: obvious + i*) + id_of_string ((string_of_id (mk_rel_id funnames.(i)))^"_"^(string_of_int !next_constructor_id)) + in + let rel_constructors i rt : (identifier*glob_constr) list = + next_constructor_id := (-1); + List.map (fun constr -> (mk_constructor_id i),constr) (constr i rt) + in + let rel_constructors = Array.mapi rel_constructors resa in + (* Computing the set of parameters if asked *) + let rels_params = compute_params_name relnames_as_set funsargs rel_constructors in + let nrel_params = List.length rels_params in + let rel_constructors = (* Taking into account the parameters in constructors *) + Array.map (List.map + (fun (id,rt) -> (id,snd (chop_rprod_n nrel_params rt)))) + rel_constructors + in + let rel_arity i funargs = (* Reduilding arities (with parameters) *) + let rel_first_args :(Names.name * Glob_term.glob_constr * bool ) list = + (snd (list_chop nrel_params funargs)) + in + List.fold_right + (fun (n,t,is_defined) acc -> + if is_defined + then + Topconstr.CLetIn(dummy_loc,(dummy_loc, n),Constrextern.extern_glob_constr Idset.empty t, + acc) + else + Topconstr.CProdN + (dummy_loc, + [[(dummy_loc,n)],Topconstr.default_binder_kind,Constrextern.extern_glob_constr Idset.empty t], + acc + ) + ) + rel_first_args + (rebuild_return_type returned_types.(i)) + in + (* We need to lift back our work topconstr but only with all information + We mimick a Set Printing All. + Then save the graphs and reset Printing options to their primitive values + *) + let rel_arities = Array.mapi rel_arity funsargs in + let rel_params = + List.map + (fun (n,t,is_defined) -> + if is_defined + then + Topconstr.LocalRawDef((dummy_loc,n), Constrextern.extern_glob_constr Idset.empty t) + else + Topconstr.LocalRawAssum + ([(dummy_loc,n)], Topconstr.default_binder_kind, Constrextern.extern_glob_constr Idset.empty t) + ) + rels_params + in + let ext_rels_constructors = + Array.map (List.map + (fun (id,t) -> + false,((dummy_loc,id), + Flags.with_option + Flags.raw_print + (Constrextern.extern_glob_type Idset.empty) ((* zeta_normalize *) t) + ) + )) + (rel_constructors) + in + let rel_ind i ext_rel_constructors = + ((dummy_loc,relnames.(i)), + rel_params, + Some rel_arities.(i), + ext_rel_constructors),[] + in + let ext_rel_constructors = (Array.mapi rel_ind ext_rels_constructors) in + let rel_inds = Array.to_list ext_rel_constructors in +(* let _ = *) +(* Pp.msgnl (\* observe *\) ( *) +(* str "Inductive" ++ spc () ++ *) +(* prlist_with_sep *) +(* (fun () -> fnl ()++spc () ++ str "with" ++ spc ()) *) +(* (function ((_,id),_,params,ar,constr) -> *) +(* Ppconstr.pr_id id ++ spc () ++ *) +(* Ppconstr.pr_binders params ++ spc () ++ *) +(* str ":" ++ spc () ++ *) +(* Ppconstr.pr_lconstr_expr ar ++ spc () ++ str ":=" ++ *) +(* prlist_with_sep *) +(* (fun _ -> fnl () ++ spc () ++ str "|" ++ spc ()) *) +(* (function (_,((_,id),t)) -> *) +(* Ppconstr.pr_id id ++ spc () ++ str ":" ++ spc () ++ *) +(* Ppconstr.pr_lconstr_expr t) *) +(* constr *) +(* ) *) +(* rel_inds *) +(* ) *) +(* in *) + let _time2 = System.get_time () in + try + with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds)) true + with + | UserError(s,msg) as e -> + let _time3 = System.get_time () in +(* Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *) + let repacked_rel_inds = + List.map (fun ((a , b , c , l),ntn) -> ((false,a) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn ) + rel_inds + in + let msg = + str "while trying to define"++ spc () ++ + Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Decl_kinds.Finite,false,repacked_rel_inds)) + ++ fnl () ++ + msg + in + observe (msg); + raise e + | e -> + let _time3 = System.get_time () in +(* Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *) + let repacked_rel_inds = + List.map (fun ((a , b , c , l),ntn) -> ((false,a) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn ) + rel_inds + in + let msg = + str "while trying to define"++ spc () ++ + Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Decl_kinds.Finite,false,repacked_rel_inds)) + ++ fnl () ++ + Cerrors.explain_exn e + in + observe msg; + raise e + + + +let build_inductive funnames funsargs returned_types rtl = + try + do_build_inductive funnames funsargs returned_types rtl + with e -> raise (Building_graph e) + + diff --git a/plugins/funind/glob_term_to_relation.mli b/plugins/funind/glob_term_to_relation.mli new file mode 100644 index 0000000000..5c91292bad --- /dev/null +++ b/plugins/funind/glob_term_to_relation.mli @@ -0,0 +1,16 @@ + + + +(* + [build_inductive parametrize funnames funargs returned_types bodies] + constructs and saves the graphs of the functions [funnames] taking [funargs] as arguments + and returning [returned_types] using bodies [bodies] +*) + +val build_inductive : + Names.identifier list -> (* The list of function name *) + (Names.name*Glob_term.glob_constr*bool) list list -> (* The list of function args *) + Topconstr.constr_expr list -> (* The list of function returned type *) + Glob_term.glob_constr list -> (* the list of body *) + unit + diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml new file mode 100644 index 0000000000..0cf91f38c0 --- /dev/null +++ b/plugins/funind/glob_termops.ml @@ -0,0 +1,718 @@ +open Pp +open Glob_term +open Util +open Names +(* Ocaml 3.06 Map.S does not handle is_empty *) +let idmap_is_empty m = m = Idmap.empty + +(* + Some basic functions to rebuild glob_constr + In each of them the location is Util.dummy_loc +*) +let mkRRef ref = GRef(dummy_loc,ref) +let mkRVar id = GVar(dummy_loc,id) +let mkRApp(rt,rtl) = GApp(dummy_loc,rt,rtl) +let mkRLambda(n,t,b) = GLambda(dummy_loc,n,Explicit,t,b) +let mkRProd(n,t,b) = GProd(dummy_loc,n,Explicit,t,b) +let mkRLetIn(n,t,b) = GLetIn(dummy_loc,n,t,b) +let mkRCases(rto,l,brl) = GCases(dummy_loc,Term.RegularStyle,rto,l,brl) +let mkRSort s = GSort(dummy_loc,s) +let mkRHole () = GHole(dummy_loc,Evd.BinderType Anonymous) +let mkRCast(b,t) = GCast(dummy_loc,b,CastConv (Term.DEFAULTcast,t)) + +(* + Some basic functions to decompose glob_constrs + These are analogous to the ones constrs +*) +let glob_decompose_prod = + let rec glob_decompose_prod args = function + | GProd(_,n,k,t,b) -> + glob_decompose_prod ((n,t)::args) b + | rt -> args,rt + in + glob_decompose_prod [] + +let glob_decompose_prod_or_letin = + let rec glob_decompose_prod args = function + | GProd(_,n,k,t,b) -> + glob_decompose_prod ((n,None,Some t)::args) b + | GLetIn(_,n,t,b) -> + glob_decompose_prod ((n,Some t,None)::args) b + | rt -> args,rt + in + glob_decompose_prod [] + +let glob_compose_prod = + List.fold_left (fun b (n,t) -> mkRProd(n,t,b)) + +let glob_compose_prod_or_letin = + List.fold_left ( + fun concl decl -> + match decl with + | (n,None,Some t) -> mkRProd(n,t,concl) + | (n,Some bdy,None) -> mkRLetIn(n,bdy,concl) + | _ -> assert false) + +let glob_decompose_prod_n n = + let rec glob_decompose_prod i args c = + if i<=0 then args,c + else + match c with + | GProd(_,n,_,t,b) -> + glob_decompose_prod (i-1) ((n,t)::args) b + | rt -> args,rt + in + glob_decompose_prod n [] + + +let glob_decompose_prod_or_letin_n n = + let rec glob_decompose_prod i args c = + if i<=0 then args,c + else + match c with + | GProd(_,n,_,t,b) -> + glob_decompose_prod (i-1) ((n,None,Some t)::args) b + | GLetIn(_,n,t,b) -> + glob_decompose_prod (i-1) ((n,Some t,None)::args) b + | rt -> args,rt + in + glob_decompose_prod n [] + + +let glob_decompose_app = + let rec decompose_rapp acc rt = +(* msgnl (str "glob_decompose_app on : "++ Printer.pr_glob_constr rt); *) + match rt with + | GApp(_,rt,rtl) -> + decompose_rapp (List.fold_left (fun y x -> x::y) acc rtl) rt + | rt -> rt,List.rev acc + in + decompose_rapp [] + + + + +(* [glob_make_eq t1 t2] build the glob_constr corresponding to [t2 = t1] *) +let glob_make_eq ?(typ= mkRHole ()) t1 t2 = + mkRApp(mkRRef (Lazy.force Coqlib.coq_eq_ref),[typ;t2;t1]) + +(* [glob_make_neq t1 t2] build the glob_constr corresponding to [t1 <> t2] *) +let glob_make_neq t1 t2 = + mkRApp(mkRRef (Lazy.force Coqlib.coq_not_ref),[glob_make_eq t1 t2]) + +(* [glob_make_or P1 P2] build the glob_constr corresponding to [P1 \/ P2] *) +let glob_make_or t1 t2 = mkRApp (mkRRef(Lazy.force Coqlib.coq_or_ref),[t1;t2]) + +(* [glob_make_or_list [P1;...;Pn]] build the glob_constr corresponding + to [P1 \/ ( .... \/ Pn)] +*) +let rec glob_make_or_list = function + | [] -> raise (Invalid_argument "mk_or") + | [e] -> e + | e::l -> glob_make_or e (glob_make_or_list l) + + +let remove_name_from_mapping mapping na = + match na with + | Anonymous -> mapping + | Name id -> Idmap.remove id mapping + +let change_vars = + let rec change_vars mapping rt = + match rt with + | GRef _ -> rt + | GVar(loc,id) -> + let new_id = + try + Idmap.find id mapping + with Not_found -> id + in + GVar(loc,new_id) + | GEvar _ -> rt + | GPatVar _ -> rt + | GApp(loc,rt',rtl) -> + GApp(loc, + change_vars mapping rt', + List.map (change_vars mapping) rtl + ) + | GLambda(loc,name,k,t,b) -> + GLambda(loc, + name, + k, + change_vars mapping t, + change_vars (remove_name_from_mapping mapping name) b + ) + | GProd(loc,name,k,t,b) -> + GProd(loc, + name, + k, + change_vars mapping t, + change_vars (remove_name_from_mapping mapping name) b + ) + | GLetIn(loc,name,def,b) -> + GLetIn(loc, + name, + change_vars mapping def, + change_vars (remove_name_from_mapping mapping name) b + ) + | GLetTuple(loc,nal,(na,rto),b,e) -> + let new_mapping = List.fold_left remove_name_from_mapping mapping nal in + GLetTuple(loc, + nal, + (na, Option.map (change_vars mapping) rto), + change_vars mapping b, + change_vars new_mapping e + ) + | GCases(loc,sty,infos,el,brl) -> + GCases(loc,sty, + infos, + List.map (fun (e,x) -> (change_vars mapping e,x)) el, + List.map (change_vars_br mapping) brl + ) + | GIf(loc,b,(na,e_option),lhs,rhs) -> + GIf(loc, + change_vars mapping b, + (na,Option.map (change_vars mapping) e_option), + change_vars mapping lhs, + change_vars mapping rhs + ) + | GRec _ -> error "Local (co)fixes are not supported" + | GSort _ -> rt + | GHole _ -> rt + | GCast(loc,b,CastConv (k,t)) -> + GCast(loc,change_vars mapping b, CastConv (k,change_vars mapping t)) + | GCast(loc,b,CastCoerce) -> + GCast(loc,change_vars mapping b,CastCoerce) + | GDynamic _ -> error "Not handled GDynamic" + and change_vars_br mapping ((loc,idl,patl,res) as br) = + let new_mapping = List.fold_right Idmap.remove idl mapping in + if idmap_is_empty new_mapping + then br + else (loc,idl,patl,change_vars new_mapping res) + in + change_vars + + + +let rec alpha_pat excluded pat = + match pat with + | PatVar(loc,Anonymous) -> + let new_id = Indfun_common.fresh_id excluded "_x" in + PatVar(loc,Name new_id),(new_id::excluded),Idmap.empty + | PatVar(loc,Name id) -> + if List.mem id excluded + then + let new_id = Namegen.next_ident_away id excluded in + PatVar(loc,Name new_id),(new_id::excluded), + (Idmap.add id new_id Idmap.empty) + else pat,excluded,Idmap.empty + | PatCstr(loc,constr,patl,na) -> + let new_na,new_excluded,map = + match na with + | Name id when List.mem id excluded -> + let new_id = Namegen.next_ident_away id excluded in + Name new_id,new_id::excluded, Idmap.add id new_id Idmap.empty + | _ -> na,excluded,Idmap.empty + in + let new_patl,new_excluded,new_map = + List.fold_left + (fun (patl,excluded,map) pat -> + let new_pat,new_excluded,new_map = alpha_pat excluded pat in + (new_pat::patl,new_excluded,Idmap.fold Idmap.add new_map map) + ) + ([],new_excluded,map) + patl + in + PatCstr(loc,constr,List.rev new_patl,new_na),new_excluded,new_map + +let alpha_patl excluded patl = + let patl,new_excluded,map = + List.fold_left + (fun (patl,excluded,map) pat -> + let new_pat,new_excluded,new_map = alpha_pat excluded pat in + new_pat::patl,new_excluded,(Idmap.fold Idmap.add new_map map) + ) + ([],excluded,Idmap.empty) + patl + in + (List.rev patl,new_excluded,map) + + + + +let raw_get_pattern_id pat acc = + let rec get_pattern_id pat = + match pat with + | PatVar(loc,Anonymous) -> assert false + | PatVar(loc,Name id) -> + [id] + | PatCstr(loc,constr,patternl,_) -> + List.fold_right + (fun pat idl -> + let idl' = get_pattern_id pat in + idl'@idl + ) + patternl + [] + in + (get_pattern_id pat)@acc + +let get_pattern_id pat = raw_get_pattern_id pat [] + +let rec alpha_rt excluded rt = + let new_rt = + match rt with + | GRef _ | GVar _ | GEvar _ | GPatVar _ -> rt + | GLambda(loc,Anonymous,k,t,b) -> + let new_id = Namegen.next_ident_away (id_of_string "_x") excluded in + let new_excluded = new_id :: excluded in + let new_t = alpha_rt new_excluded t in + let new_b = alpha_rt new_excluded b in + GLambda(loc,Name new_id,k,new_t,new_b) + | GProd(loc,Anonymous,k,t,b) -> + let new_t = alpha_rt excluded t in + let new_b = alpha_rt excluded b in + GProd(loc,Anonymous,k,new_t,new_b) + | GLetIn(loc,Anonymous,t,b) -> + let new_t = alpha_rt excluded t in + let new_b = alpha_rt excluded b in + GLetIn(loc,Anonymous,new_t,new_b) + | GLambda(loc,Name id,k,t,b) -> + let new_id = Namegen.next_ident_away id excluded in + let t,b = + if new_id = id + then t,b + else + let replace = change_vars (Idmap.add id new_id Idmap.empty) in + (t,replace b) + in + let new_excluded = new_id::excluded in + let new_t = alpha_rt new_excluded t in + let new_b = alpha_rt new_excluded b in + GLambda(loc,Name new_id,k,new_t,new_b) + | GProd(loc,Name id,k,t,b) -> + let new_id = Namegen.next_ident_away id excluded in + let new_excluded = new_id::excluded in + let t,b = + if new_id = id + then t,b + else + let replace = change_vars (Idmap.add id new_id Idmap.empty) in + (t,replace b) + in + let new_t = alpha_rt new_excluded t in + let new_b = alpha_rt new_excluded b in + GProd(loc,Name new_id,k,new_t,new_b) + | GLetIn(loc,Name id,t,b) -> + let new_id = Namegen.next_ident_away id excluded in + let t,b = + if new_id = id + then t,b + else + let replace = change_vars (Idmap.add id new_id Idmap.empty) in + (t,replace b) + in + let new_excluded = new_id::excluded in + let new_t = alpha_rt new_excluded t in + let new_b = alpha_rt new_excluded b in + GLetIn(loc,Name new_id,new_t,new_b) + + + | GLetTuple(loc,nal,(na,rto),t,b) -> + let rev_new_nal,new_excluded,mapping = + List.fold_left + (fun (nal,excluded,mapping) na -> + match na with + | Anonymous -> (na::nal,excluded,mapping) + | Name id -> + let new_id = Namegen.next_ident_away id excluded in + if new_id = id + then + na::nal,id::excluded,mapping + else + (Name new_id)::nal,id::excluded,(Idmap.add id new_id mapping) + ) + ([],excluded,Idmap.empty) + nal + in + let new_nal = List.rev rev_new_nal in + let new_rto,new_t,new_b = + if idmap_is_empty mapping + then rto,t,b + else let replace = change_vars mapping in + (Option.map replace rto, t,replace b) + in + let new_t = alpha_rt new_excluded new_t in + let new_b = alpha_rt new_excluded new_b in + let new_rto = Option.map (alpha_rt new_excluded) new_rto in + GLetTuple(loc,new_nal,(na,new_rto),new_t,new_b) + | GCases(loc,sty,infos,el,brl) -> + let new_el = + List.map (function (rt,i) -> alpha_rt excluded rt, i) el + in + GCases(loc,sty,infos,new_el,List.map (alpha_br excluded) brl) + | GIf(loc,b,(na,e_o),lhs,rhs) -> + GIf(loc,alpha_rt excluded b, + (na,Option.map (alpha_rt excluded) e_o), + alpha_rt excluded lhs, + alpha_rt excluded rhs + ) + | GRec _ -> error "Not handled GRec" + | GSort _ -> rt + | GHole _ -> rt + | GCast (loc,b,CastConv (k,t)) -> + GCast(loc,alpha_rt excluded b,CastConv(k,alpha_rt excluded t)) + | GCast (loc,b,CastCoerce) -> + GCast(loc,alpha_rt excluded b,CastCoerce) + | GDynamic _ -> error "Not handled GDynamic" + | GApp(loc,f,args) -> + GApp(loc, + alpha_rt excluded f, + List.map (alpha_rt excluded) args + ) + in + new_rt + +and alpha_br excluded (loc,ids,patl,res) = + let new_patl,new_excluded,mapping = alpha_patl excluded patl in + let new_ids = List.fold_right raw_get_pattern_id new_patl [] in + let new_excluded = new_ids@excluded in + let renamed_res = change_vars mapping res in + let new_res = alpha_rt new_excluded renamed_res in + (loc,new_ids,new_patl,new_res) + +(* + [is_free_in id rt] checks if [id] is a free variable in [rt] +*) +let is_free_in id = + let rec is_free_in = function + | GRef _ -> false + | GVar(_,id') -> id_ord id' id == 0 + | GEvar _ -> false + | GPatVar _ -> false + | GApp(_,rt,rtl) -> List.exists is_free_in (rt::rtl) + | GLambda(_,n,_,t,b) | GProd(_,n,_,t,b) | GLetIn(_,n,t,b) -> + let check_in_b = + match n with + | Name id' -> id_ord id' id <> 0 + | _ -> true + in + is_free_in t || (check_in_b && is_free_in b) + | GCases(_,_,_,el,brl) -> + (List.exists (fun (e,_) -> is_free_in e) el) || + List.exists is_free_in_br brl + | GLetTuple(_,nal,_,b,t) -> + let check_in_nal = + not (List.exists (function Name id' -> id'= id | _ -> false) nal) + in + is_free_in t || (check_in_nal && is_free_in b) + + | GIf(_,cond,_,br1,br2) -> + is_free_in cond || is_free_in br1 || is_free_in br2 + | GRec _ -> raise (UserError("",str "Not handled GRec")) + | GSort _ -> false + | GHole _ -> false + | GCast (_,b,CastConv (_,t)) -> is_free_in b || is_free_in t + | GCast (_,b,CastCoerce) -> is_free_in b + | GDynamic _ -> raise (UserError("",str "Not handled GDynamic")) + and is_free_in_br (_,ids,_,rt) = + (not (List.mem id ids)) && is_free_in rt + in + is_free_in + + + +let rec pattern_to_term = function + | PatVar(loc,Anonymous) -> assert false + | PatVar(loc,Name id) -> + mkRVar id + | PatCstr(loc,constr,patternl,_) -> + let cst_narg = + Inductiveops.mis_constructor_nargs_env + (Global.env ()) + constr + in + let implicit_args = + Array.to_list + (Array.init + (cst_narg - List.length patternl) + (fun _ -> mkRHole ()) + ) + in + let patl_as_term = + List.map pattern_to_term patternl + in + mkRApp(mkRRef(Libnames.ConstructRef constr), + implicit_args@patl_as_term + ) + + + +let replace_var_by_term x_id term = + let rec replace_var_by_pattern rt = + match rt with + | GRef _ -> rt + | GVar(_,id) when id_ord id x_id == 0 -> term + | GVar _ -> rt + | GEvar _ -> rt + | GPatVar _ -> rt + | GApp(loc,rt',rtl) -> + GApp(loc, + replace_var_by_pattern rt', + List.map replace_var_by_pattern rtl + ) + | GLambda(_,Name id,_,_,_) when id_ord id x_id == 0 -> rt + | GLambda(loc,name,k,t,b) -> + GLambda(loc, + name, + k, + replace_var_by_pattern t, + replace_var_by_pattern b + ) + | GProd(_,Name id,_,_,_) when id_ord id x_id == 0 -> rt + | GProd(loc,name,k,t,b) -> + GProd(loc, + name, + k, + replace_var_by_pattern t, + replace_var_by_pattern b + ) + | GLetIn(_,Name id,_,_) when id_ord id x_id == 0 -> rt + | GLetIn(loc,name,def,b) -> + GLetIn(loc, + name, + replace_var_by_pattern def, + replace_var_by_pattern b + ) + | GLetTuple(_,nal,_,_,_) + when List.exists (function Name id -> id = x_id | _ -> false) nal -> + rt + | GLetTuple(loc,nal,(na,rto),def,b) -> + GLetTuple(loc, + nal, + (na,Option.map replace_var_by_pattern rto), + replace_var_by_pattern def, + replace_var_by_pattern b + ) + | GCases(loc,sty,infos,el,brl) -> + GCases(loc,sty, + infos, + List.map (fun (e,x) -> (replace_var_by_pattern e,x)) el, + List.map replace_var_by_pattern_br brl + ) + | GIf(loc,b,(na,e_option),lhs,rhs) -> + GIf(loc, replace_var_by_pattern b, + (na,Option.map replace_var_by_pattern e_option), + replace_var_by_pattern lhs, + replace_var_by_pattern rhs + ) + | GRec _ -> raise (UserError("",str "Not handled GRec")) + | GSort _ -> rt + | GHole _ -> rt + | GCast(loc,b,CastConv(k,t)) -> + GCast(loc,replace_var_by_pattern b,CastConv(k,replace_var_by_pattern t)) + | GCast(loc,b,CastCoerce) -> + GCast(loc,replace_var_by_pattern b,CastCoerce) + | GDynamic _ -> raise (UserError("",str "Not handled GDynamic")) + and replace_var_by_pattern_br ((loc,idl,patl,res) as br) = + if List.exists (fun id -> id_ord id x_id == 0) idl + then br + else (loc,idl,patl,replace_var_by_pattern res) + in + replace_var_by_pattern + + + + +(* checking unifiability of patterns *) +exception NotUnifiable + +let rec are_unifiable_aux = function + | [] -> () + | eq::eqs -> + match eq with + | PatVar _,_ | _,PatVar _ -> are_unifiable_aux eqs + | PatCstr(_,constructor1,cpl1,_),PatCstr(_,constructor2,cpl2,_) -> + if constructor2 <> constructor1 + then raise NotUnifiable + else + let eqs' = + try ((List.combine cpl1 cpl2)@eqs) + with _ -> anomaly "are_unifiable_aux" + in + are_unifiable_aux eqs' + +let are_unifiable pat1 pat2 = + try + are_unifiable_aux [pat1,pat2]; + true + with NotUnifiable -> false + + +let rec eq_cases_pattern_aux = function + | [] -> () + | eq::eqs -> + match eq with + | PatVar _,PatVar _ -> eq_cases_pattern_aux eqs + | PatCstr(_,constructor1,cpl1,_),PatCstr(_,constructor2,cpl2,_) -> + if constructor2 <> constructor1 + then raise NotUnifiable + else + let eqs' = + try ((List.combine cpl1 cpl2)@eqs) + with _ -> anomaly "eq_cases_pattern_aux" + in + eq_cases_pattern_aux eqs' + | _ -> raise NotUnifiable + +let eq_cases_pattern pat1 pat2 = + try + eq_cases_pattern_aux [pat1,pat2]; + true + with NotUnifiable -> false + + + +let ids_of_pat = + let rec ids_of_pat ids = function + | PatVar(_,Anonymous) -> ids + | PatVar(_,Name id) -> Idset.add id ids + | PatCstr(_,_,patl,_) -> List.fold_left ids_of_pat ids patl + in + ids_of_pat Idset.empty + +let id_of_name = function + | Names.Anonymous -> id_of_string "x" + | Names.Name x -> x + +(* TODO: finish Rec caes *) +let ids_of_rawterm c = + let rec ids_of_rawterm acc c = + let idof = id_of_name in + match c with + | GVar (_,id) -> id::acc + | GApp (loc,g,args) -> + ids_of_rawterm [] g @ List.flatten (List.map (ids_of_rawterm []) args) @ acc + | GLambda (loc,na,k,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc + | GProd (loc,na,k,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc + | GLetIn (loc,na,b,c) -> idof na :: ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc + | GCast (loc,c,CastConv(k,t)) -> ids_of_rawterm [] c @ ids_of_rawterm [] t @ acc + | GCast (loc,c,CastCoerce) -> ids_of_rawterm [] c @ acc + | GIf (loc,c,(na,po),b1,b2) -> ids_of_rawterm [] c @ ids_of_rawterm [] b1 @ ids_of_rawterm [] b2 @ acc + | GLetTuple (_,nal,(na,po),b,c) -> + List.map idof nal @ ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc + | GCases (loc,sty,rtntypopt,tml,brchl) -> + List.flatten (List.map (fun (_,idl,patl,c) -> idl @ ids_of_rawterm [] c) brchl) + | GRec _ -> failwith "Fix inside a constructor branch" + | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GDynamic _) -> [] + in + (* build the set *) + List.fold_left (fun acc x -> Idset.add x acc) Idset.empty (ids_of_rawterm [] c) + + + + + +let zeta_normalize = + let rec zeta_normalize_term rt = + match rt with + | GRef _ -> rt + | GVar _ -> rt + | GEvar _ -> rt + | GPatVar _ -> rt + | GApp(loc,rt',rtl) -> + GApp(loc, + zeta_normalize_term rt', + List.map zeta_normalize_term rtl + ) + | GLambda(loc,name,k,t,b) -> + GLambda(loc, + name, + k, + zeta_normalize_term t, + zeta_normalize_term b + ) + | GProd(loc,name,k,t,b) -> + GProd(loc, + name, + k, + zeta_normalize_term t, + zeta_normalize_term b + ) + | GLetIn(_,Name id,def,b) -> + zeta_normalize_term (replace_var_by_term id def b) + | GLetIn(loc,Anonymous,def,b) -> zeta_normalize_term b + | GLetTuple(loc,nal,(na,rto),def,b) -> + GLetTuple(loc, + nal, + (na,Option.map zeta_normalize_term rto), + zeta_normalize_term def, + zeta_normalize_term b + ) + | GCases(loc,sty,infos,el,brl) -> + GCases(loc,sty, + infos, + List.map (fun (e,x) -> (zeta_normalize_term e,x)) el, + List.map zeta_normalize_br brl + ) + | GIf(loc,b,(na,e_option),lhs,rhs) -> + GIf(loc, zeta_normalize_term b, + (na,Option.map zeta_normalize_term e_option), + zeta_normalize_term lhs, + zeta_normalize_term rhs + ) + | GRec _ -> raise (UserError("",str "Not handled GRec")) + | GSort _ -> rt + | GHole _ -> rt + | GCast(loc,b,CastConv(k,t)) -> + GCast(loc,zeta_normalize_term b,CastConv(k,zeta_normalize_term t)) + | GCast(loc,b,CastCoerce) -> + GCast(loc,zeta_normalize_term b,CastCoerce) + | GDynamic _ -> raise (UserError("",str "Not handled GDynamic")) + and zeta_normalize_br (loc,idl,patl,res) = + (loc,idl,patl,zeta_normalize_term res) + in + zeta_normalize_term + + + + +let expand_as = + + let rec add_as map pat = + match pat with + | PatVar _ -> map + | PatCstr(_,_,patl,Name id) -> + Idmap.add id (pattern_to_term pat) (List.fold_left add_as map patl) + | PatCstr(_,_,patl,_) -> List.fold_left add_as map patl + in + let rec expand_as map rt = + match rt with + | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> rt + | GVar(_,id) -> + begin + try + Idmap.find id map + with Not_found -> rt + end + | GApp(loc,f,args) -> GApp(loc,expand_as map f,List.map (expand_as map) args) + | GLambda(loc,na,k,t,b) -> GLambda(loc,na,k,expand_as map t, expand_as map b) + | GProd(loc,na,k,t,b) -> GProd(loc,na,k,expand_as map t, expand_as map b) + | GLetIn(loc,na,v,b) -> GLetIn(loc,na, expand_as map v,expand_as map b) + | GLetTuple(loc,nal,(na,po),v,b) -> + GLetTuple(loc,nal,(na,Option.map (expand_as map) po), + expand_as map v, expand_as map b) + | GIf(loc,e,(na,po),br1,br2) -> + GIf(loc,expand_as map e,(na,Option.map (expand_as map) po), + expand_as map br1, expand_as map br2) + | GRec _ -> error "Not handled GRec" + | GDynamic _ -> error "Not handled GDynamic" + | GCast(loc,b,CastConv(kind,t)) -> GCast(loc,expand_as map b,CastConv(kind,expand_as map t)) + | GCast(loc,b,CastCoerce) -> GCast(loc,expand_as map b,CastCoerce) + | GCases(loc,sty,po,el,brl) -> + GCases(loc, sty, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el, + List.map (expand_as_br map) brl) + and expand_as_br map (loc,idl,cpl,rt) = + (loc,idl,cpl, expand_as (List.fold_left add_as map cpl) rt) + in + expand_as Idmap.empty diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli new file mode 100644 index 0000000000..b6c407a240 --- /dev/null +++ b/plugins/funind/glob_termops.mli @@ -0,0 +1,126 @@ +open Glob_term + +(* Ocaml 3.06 Map.S does not handle is_empty *) +val idmap_is_empty : 'a Names.Idmap.t -> bool + + +(* [get_pattern_id pat] returns a list of all the variable appearing in [pat] *) +val get_pattern_id : cases_pattern -> Names.identifier list + +(* [pattern_to_term pat] returns a glob_constr corresponding to [pat]. + [pat] must not contain occurences of anonymous pattern +*) +val pattern_to_term : cases_pattern -> glob_constr + +(* + Some basic functions to rebuild glob_constr + In each of them the location is Util.dummy_loc +*) +val mkRRef : Libnames.global_reference -> glob_constr +val mkRVar : Names.identifier -> glob_constr +val mkRApp : glob_constr*(glob_constr list) -> glob_constr +val mkRLambda : Names.name * glob_constr * glob_constr -> glob_constr +val mkRProd : Names.name * glob_constr * glob_constr -> glob_constr +val mkRLetIn : Names.name * glob_constr * glob_constr -> glob_constr +val mkRCases : glob_constr option * tomatch_tuples * cases_clauses -> glob_constr +val mkRSort : rawsort -> glob_constr +val mkRHole : unit -> glob_constr (* we only build Evd.BinderType Anonymous holes *) +val mkRCast : glob_constr* glob_constr -> glob_constr +(* + Some basic functions to decompose glob_constrs + These are analogous to the ones constrs +*) +val glob_decompose_prod : glob_constr -> (Names.name*glob_constr) list * glob_constr +val glob_decompose_prod_or_letin : + glob_constr -> (Names.name*glob_constr option*glob_constr option) list * glob_constr +val glob_decompose_prod_n : int -> glob_constr -> (Names.name*glob_constr) list * glob_constr +val glob_decompose_prod_or_letin_n : int -> glob_constr -> + (Names.name*glob_constr option*glob_constr option) list * glob_constr +val glob_compose_prod : glob_constr -> (Names.name*glob_constr) list -> glob_constr +val glob_compose_prod_or_letin: glob_constr -> + (Names.name*glob_constr option*glob_constr option) list -> glob_constr +val glob_decompose_app : glob_constr -> glob_constr*(glob_constr list) + + +(* [glob_make_eq t1 t2] build the glob_constr corresponding to [t2 = t1] *) +val glob_make_eq : ?typ:glob_constr -> glob_constr -> glob_constr -> glob_constr +(* [glob_make_neq t1 t2] build the glob_constr corresponding to [t1 <> t2] *) +val glob_make_neq : glob_constr -> glob_constr -> glob_constr +(* [glob_make_or P1 P2] build the glob_constr corresponding to [P1 \/ P2] *) +val glob_make_or : glob_constr -> glob_constr -> glob_constr + +(* [glob_make_or_list [P1;...;Pn]] build the glob_constr corresponding + to [P1 \/ ( .... \/ Pn)] +*) +val glob_make_or_list : glob_constr list -> glob_constr + + +(* alpha_conversion functions *) + + + +(* Replace the var mapped in the glob_constr/context *) +val change_vars : Names.identifier Names.Idmap.t -> glob_constr -> glob_constr + + + +(* [alpha_pat avoid pat] rename all the variables present in [pat] s.t. + the result does not share variables with [avoid]. This function create + a fresh variable for each occurence of the anonymous pattern. + + Also returns a mapping from old variables to new ones and the concatenation of + [avoid] with the variables appearing in the result. +*) + val alpha_pat : + Names.Idmap.key list -> + Glob_term.cases_pattern -> + Glob_term.cases_pattern * Names.Idmap.key list * + Names.identifier Names.Idmap.t + +(* [alpha_rt avoid rt] alpha convert [rt] s.t. the result repects barendregt + conventions and does not share bound variables with avoid +*) +val alpha_rt : Names.identifier list -> glob_constr -> glob_constr + +(* same as alpha_rt but for case branches *) +val alpha_br : Names.identifier list -> + Util.loc * Names.identifier list * Glob_term.cases_pattern list * + Glob_term.glob_constr -> + Util.loc * Names.identifier list * Glob_term.cases_pattern list * + Glob_term.glob_constr + + +(* Reduction function *) +val replace_var_by_term : + Names.identifier -> + Glob_term.glob_constr -> Glob_term.glob_constr -> Glob_term.glob_constr + + + +(* + [is_free_in id rt] checks if [id] is a free variable in [rt] +*) +val is_free_in : Names.identifier -> glob_constr -> bool + + +val are_unifiable : cases_pattern -> cases_pattern -> bool +val eq_cases_pattern : cases_pattern -> cases_pattern -> bool + + + +(* + ids_of_pat : cases_pattern -> Idset.t + returns the set of variables appearing in a pattern +*) +val ids_of_pat : cases_pattern -> Names.Idset.t + +(* TODO: finish this function (Fix not treated) *) +val ids_of_rawterm: glob_constr -> Names.Idset.t + +(* + removing let_in construction in a rawterm +*) +val zeta_normalize : Glob_term.glob_constr -> Glob_term.glob_constr + + +val expand_as : glob_constr -> glob_constr diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 6e063d3c17..f23fcd6134 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -300,7 +300,7 @@ let generate_principle on_error let funs_types = List.map (function ((_,_,_,types,_),_) -> types) fix_rec_l in try (* We then register the Inductive graphs of the functions *) - Rawterm_to_relation.build_inductive names funs_args funs_types recdefs; + Glob_term_to_relation.build_inductive names funs_args funs_types recdefs; if do_built then begin diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index f757bafcbc..7c32c1d20c 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -21,7 +21,7 @@ open Termops open Declarations open Environ open Glob_term -open Rawtermops +open Glob_termops (** {1 Utilities} *) diff --git a/plugins/funind/rawterm_to_relation.ml b/plugins/funind/rawterm_to_relation.ml deleted file mode 100644 index 0616007950..0000000000 --- a/plugins/funind/rawterm_to_relation.ml +++ /dev/null @@ -1,1419 +0,0 @@ -open Printer -open Pp -open Names -open Term -open Glob_term -open Libnames -open Indfun_common -open Util -open Rawtermops - -let observe strm = - if do_observe () - then Pp.msgnl strm - else () -let observennl strm = - if do_observe () - then Pp.msg strm - else () - - -type binder_type = - | Lambda of name - | Prod of name - | LetIn of name - -type glob_context = (binder_type*glob_constr) list - -(* - compose_glob_context [(bt_1,n_1,t_1);......] rt returns - b_1(n_1,t_1,.....,bn(n_k,t_k,rt)) where the b_i's are the - binders corresponding to the bt_i's -*) -let compose_glob_context = - let compose_binder (bt,t) acc = - match bt with - | Lambda n -> mkRLambda(n,t,acc) - | Prod n -> mkRProd(n,t,acc) - | LetIn n -> mkRLetIn(n,t,acc) - in - List.fold_right compose_binder - - -(* - The main part deals with building a list of globalized constructor expressions - from the rhs of a fixpoint equation. -*) - -type 'a build_entry_pre_return = - { - context : glob_context; (* the binding context of the result *) - value : 'a; (* The value *) - } - -type 'a build_entry_return = - { - result : 'a build_entry_pre_return list; - to_avoid : identifier list - } - -(* - [combine_results combine_fun res1 res2] combine two results [res1] and [res2] - w.r.t. [combine_fun]. - - Informally, both [res1] and [res2] are lists of "constructors" [res1_1;...] - and [res2_1,....] and we need to produce - [combine_fun res1_1 res2_1;combine_fun res1_1 res2_2;........] -*) - -let combine_results - (combine_fun : 'a build_entry_pre_return -> 'b build_entry_pre_return -> - 'c build_entry_pre_return - ) - (res1: 'a build_entry_return) - (res2 : 'b build_entry_return) - : 'c build_entry_return - = - let pre_result = List.map - ( fun res1 -> (* for each result in arg_res *) - List.map (* we add it in each args_res *) - (fun res2 -> - combine_fun res1 res2 - ) - res2.result - ) - res1.result - in (* and then we flatten the map *) - { - result = List.concat pre_result; - to_avoid = list_union res1.to_avoid res2.to_avoid - } - - -(* - The combination function for an argument with a list of argument -*) - -let combine_args arg args = - { - context = arg.context@args.context; - (* Note that the binding context of [arg] MUST be placed before the one of - [args] in order to preserve possible type dependencies - *) - value = arg.value::args.value; - } - - -let ids_of_binder = function - | LetIn Anonymous | Prod Anonymous | Lambda Anonymous -> [] - | LetIn (Name id) | Prod (Name id) | Lambda (Name id) -> [id] - -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 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 bt = - List.exists (need_convert_id avoid) (ids_of_binder bt) - in - let next_name_away (na:name) (mapping: identifier Idmap.t) (avoid: identifier list) = - match na with - | Name id when List.mem id avoid -> - let new_id = Namegen.next_ident_away id avoid in - Name new_id,Idmap.add id new_id mapping,new_id::avoid - | _ -> na,mapping,avoid - in - 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 - in - let rec do_apply avoid ctxt body args = - match ctxt,args with - | _,[] -> (* No more args *) - (ctxt,body) - | [],_ -> (* no more fun *) - let f,args' = glob_decompose_app body in - (ctxt,mkRApp(f,args'@args)) - | (Lambda Anonymous,t)::ctxt',arg::args' -> - do_apply avoid ctxt' body args' - | (Lambda (Name id),t)::ctxt',arg::args' -> - let new_avoid,new_ctxt',new_body,new_id = - if need_convert_id avoid id - then - let new_avoid = id::avoid in - let new_id = Namegen.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 - new_avoid',new_ctxt',new_body,new_id - else - id::avoid,ctxt',body,id - in - 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,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_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,bt - in - let new_ctxt',new_body = - do_apply new_avoid new_ctxt' new_body args - in - (new_bt,t)::new_ctxt',new_body - in - do_apply [] ctxt body args - - -let combine_app f args = - let new_ctxt,new_value = apply_args f.context f.value args.value in - { - (* Note that the binding context of [args] MUST be placed before the one of - the applied value in order to preserve possible type dependencies - *) - context = args.context@new_ctxt; - value = new_value; - } - -let combine_lam n t b = - { - context = []; - value = mkRLambda(n, compose_glob_context t.context t.value, - compose_glob_context b.context b.value ) - } - - - -let combine_prod n t b = - { 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} - - -let mk_result ctxt value avoid = - { - result = - [{context = ctxt; - value = value}] - ; - to_avoid = avoid - } -(************************************************* - Some functions to deal with overlapping patterns -**************************************************) - -let coq_True_ref = - lazy (Coqlib.gen_reference "" ["Init";"Logic"] "True") - -let coq_False_ref = - lazy (Coqlib.gen_reference "" ["Init";"Logic"] "False") - -(* - [make_discr_match_el \[e1,...en\]] builds match e1,...,en with - (the list of expresions on which we will do the matching) - *) -let make_discr_match_el = - List.map (fun e -> (e,(Anonymous,None))) - -(* - [make_discr_match_brl i \[pat_1,...,pat_n\]] constructs a discrimination pattern matching on the ith expression. - that is. - match ?????? with \\ - | pat_1 => False \\ - | pat_{i-1} => False \\ - | pat_i => True \\ - | pat_{i+1} => False \\ - \vdots - | pat_n => False - end -*) -let make_discr_match_brl i = - list_map_i - (fun j (_,idl,patl,_) -> - if j=i - then (dummy_loc,idl,patl, mkRRef (Lazy.force coq_True_ref)) - else (dummy_loc,idl,patl, mkRRef (Lazy.force coq_False_ref)) - ) - 0 -(* - [make_discr_match brl el i] generates an hypothesis such that it reduce to true iff - brl_{i} is the first branch matched by [el] - - Used when we want to simulate the coq pattern matching algorithm -*) -let make_discr_match brl = - fun el i -> - mkRCases(None, - make_discr_match_el el, - make_discr_match_brl i brl) - -let pr_name = function - | Name id -> Ppconstr.pr_id id - | Anonymous -> str "_" - -(**********************************************************************) -(* functions used to build case expression from lettuple and if ones *) -(**********************************************************************) - -(* [build_constructors_of_type] construct the array of pattern of its inductive argument*) -let build_constructors_of_type ind' argl = - let (mib,ind) = Inductive.lookup_mind_specif (Global.env()) ind' in - let npar = mib.Declarations.mind_nparams in - Array.mapi (fun i _ -> - let construct = ind',i+1 in - let constructref = ConstructRef(construct) in - let _implicit_positions_of_cst = - Impargs.implicits_of_global constructref - in - let cst_narg = - Inductiveops.mis_constructor_nargs_env - (Global.env ()) - construct - in - let argl = - if argl = [] - then - Array.to_list - (Array.init (cst_narg - npar) (fun _ -> mkRHole ()) - ) - else argl - in - let pat_as_term = - mkRApp(mkRRef (ConstructRef(ind',i+1)),argl) - in - cases_pattern_of_glob_constr Anonymous pat_as_term - ) - ind.Declarations.mind_consnames - -(* [find_type_of] very naive attempts to discover the type of an if or a letin *) -let rec find_type_of nb b = - let f,_ = glob_decompose_app b in - match f with - | GRef(_,ref) -> - begin - let ind_type = - match ref with - | VarRef _ | ConstRef _ -> - let constr_of_ref = constr_of_global ref in - let type_of_ref = Typing.type_of (Global.env ()) Evd.empty constr_of_ref in - let (_,ret_type) = Reduction.dest_prod (Global.env ()) type_of_ref in - let ret_type,_ = decompose_app ret_type in - if not (isInd ret_type) then - begin -(* Pp.msgnl (str "not an inductive" ++ pr_lconstr ret_type); *) - raise (Invalid_argument "not an inductive") - end; - destInd ret_type - | IndRef ind -> ind - | ConstructRef c -> fst c - in - let _,ind_type_info = Inductive.lookup_mind_specif (Global.env()) ind_type in - if not (Array.length ind_type_info.Declarations.mind_consnames = nb ) - then raise (Invalid_argument "find_type_of : not a valid inductive"); - ind_type - end - | GCast(_,b,_) -> find_type_of nb b - | GApp _ -> assert false (* we have decomposed any application via glob_decompose_app *) - | _ -> raise (Invalid_argument "not a ref") - - - - -(******************) -(* Main functions *) -(******************) - - - -let raw_push_named (na,raw_value,raw_typ) env = - match na with - | Anonymous -> env - | Name id -> - let value = Option.map (Pretyping.Default.understand Evd.empty env) raw_value in - let typ = Pretyping.Default.understand_type Evd.empty env raw_typ in - Environ.push_named (id,value,typ) env - - -let add_pat_variables pat typ env : Environ.env = - let rec add_pat_variables env pat typ : Environ.env = - observe (str "new rel env := " ++ Printer.pr_rel_context_of env); - - match pat with - | PatVar(_,na) -> Environ.push_rel (na,None,typ) env - | PatCstr(_,c,patl,na) -> - let Inductiveops.IndType(indf,indargs) = - try Inductiveops.find_rectype env Evd.empty typ - with Not_found -> assert false - in - let constructors = Inductiveops.get_constructors env indf in - let constructor : Inductiveops.constructor_summary = List.find (fun cs -> cs.Inductiveops.cs_cstr = c) (Array.to_list constructors) in - let cs_args_types :types list = List.map (fun (_,_,t) -> t) constructor.Inductiveops.cs_args in - List.fold_left2 add_pat_variables env patl (List.rev cs_args_types) - in - let new_env = add_pat_variables env pat typ in - let res = - fst ( - Sign.fold_rel_context - (fun (na,v,t) (env,ctxt) -> - match na with - | Anonymous -> assert false - | Name id -> - let new_t = substl ctxt t in - let new_v = Option.map (substl ctxt) v in - observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++ - str "old type := " ++ Printer.pr_lconstr t ++ fnl () ++ - str "new type := " ++ Printer.pr_lconstr new_t ++ fnl () ++ - Option.fold_right (fun v _ -> str "old value := " ++ Printer.pr_lconstr v ++ fnl ()) v (mt ()) ++ - Option.fold_right (fun v _ -> str "new value := " ++ Printer.pr_lconstr v ++ fnl ()) new_v (mt ()) - ); - (Environ.push_named (id,new_v,new_t) env,mkVar id::ctxt) - ) - (Environ.rel_context new_env) - ~init:(env,[]) - ) - in - observe (str "new var env := " ++ Printer.pr_named_context_of res); - res - - - - -let rec pattern_to_term_and_type env typ = function - | PatVar(loc,Anonymous) -> assert false - | PatVar(loc,Name id) -> - mkRVar id - | PatCstr(loc,constr,patternl,_) -> - let cst_narg = - Inductiveops.mis_constructor_nargs_env - (Global.env ()) - constr - in - let Inductiveops.IndType(indf,indargs) = - try Inductiveops.find_rectype env Evd.empty typ - with Not_found -> assert false - in - let constructors = Inductiveops.get_constructors env indf in - let constructor = List.find (fun cs -> cs.Inductiveops.cs_cstr = constr) (Array.to_list constructors) in - let cs_args_types :types list = List.map (fun (_,_,t) -> t) constructor.Inductiveops.cs_args in - let _,cstl = Inductiveops.dest_ind_family indf in - let csta = Array.of_list cstl in - let implicit_args = - Array.to_list - (Array.init - (cst_narg - List.length patternl) - (fun i -> Detyping.detype false [] (Termops.names_of_rel_context env) csta.(i)) - ) - in - let patl_as_term = - List.map2 (pattern_to_term_and_type env) (List.rev cs_args_types) patternl - in - mkRApp(mkRRef(ConstructRef constr), - implicit_args@patl_as_term - ) - -(* [build_entry_lc funnames avoid rt] construct the list (in fact a build_entry_return) - of constructors corresponding to [rt] when replacing calls to [funnames] by calls to the - corresponding graphs. - - - The idea to transform a term [t] into a list of constructors [lc] is the following: - \begin{itemize} - \item if the term is a binder (bind x, body) then first compute [lc'] the list corresponding - to [body] and add (bind x. _) to each elements of [lc] - \item if the term has the form (g t1 ... ... tn) where g does not appears in (fnames) - then compute [lc1] ... [lcn] the lists of constructors corresponding to [t1] ... [tn], - then combine those lists and [g] as follows~: for each element [c1,...,cn] of [lc1\times...\times lcn], - [g c1 ... cn] is an element of [lc] - \item if the term has the form (f t1 .... tn) where [f] appears in [fnames] then - compute [lc1] ... [lcn] the lists of constructors corresponding to [t1] ... [tn], - then compute those lists and [f] as follows~: for each element [c1,...,cn] of [lc1\times...\times lcn] - create a new variable [res] and [forall res, R_f c1 ... cn res] is in [lc] - \item if the term is a cast just treat its body part - \item - if the term is a match, an if or a lettuple then compute the lists corresponding to each branch of the case - and concatenate them (informally, each branch of a match produces a new constructor) - \end{itemize} - - WARNING: The terms constructed here are only USING the glob_constr syntax but are highly bad formed. - We must wait to have complete all the current calculi to set the recursive calls. - At this point, each term [f t1 ... tn] (where f appears in [funnames]) is replaced by - a pseudo term [forall res, res t1 ... tn, res]. A reconstruction phase is done later. - We in fact not create a constructor list since then end of each constructor has not the expected form - but only the value of the function -*) - - -let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = - observe (str " Entering : " ++ Printer.pr_glob_constr rt); - match rt with - | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> - (* do nothing (except changing type of course) *) - mk_result [] rt avoid - | GApp(_,_,_) -> - let f,args = glob_decompose_app rt in - let args_res : (glob_constr list) build_entry_return = - List.fold_right (* create the arguments lists of constructors and combine them *) - (fun arg ctxt_argsl -> - let arg_res = build_entry_lc env funnames ctxt_argsl.to_avoid arg in - combine_results combine_args arg_res ctxt_argsl - ) - args - (mk_result [] [] avoid) - in - begin - match f with - | GLambda _ -> - let rec aux t l = - match l with - | [] -> t - | u::l -> - match t with - | GLambda(loc,na,_,nat,b) -> - GLetIn(dummy_loc,na,u,aux b l) - | _ -> - GApp(dummy_loc,t,l) - in - build_entry_lc env funnames avoid (aux f args) - | GVar(_,id) when Idset.mem id funnames -> - (* if we have [f t1 ... tn] with [f]$\in$[fnames] - then we create a fresh variable [res], - add [res] and its "value" (i.e. [res v1 ... vn]) to each - pseudo constructor build for the arguments (i.e. a pseudo context [ctxt] and - a pseudo value "v1 ... vn". - The "value" of this branch is then simply [res] - *) - let rt_as_constr = Pretyping.Default.understand Evd.empty env rt in - let rt_typ = Typing.type_of env Evd.empty rt_as_constr in - let res_raw_type = Detyping.detype false [] (Termops.names_of_rel_context env) rt_typ in - let res = fresh_id args_res.to_avoid "res" in - let new_avoid = res::args_res.to_avoid in - let res_rt = mkRVar res in - let new_result = - List.map - (fun arg_res -> - let new_hyps = - [Prod (Name res),res_raw_type; - Prod Anonymous,mkRApp(res_rt,(mkRVar id)::arg_res.value)] - in - {context = arg_res.context@new_hyps; value = res_rt } - ) - args_res.result - in - { result = new_result; to_avoid = new_avoid } - | GVar _ | GEvar _ | GPatVar _ | GHole _ | GSort _ | GRef _ -> - (* if have [g t1 ... tn] with [g] not appearing in [funnames] - then - foreach [ctxt,v1 ... vn] in [args_res] we return - [ctxt, g v1 .... vn] - *) - { - args_res with - result = - List.map - (fun args_res -> - {args_res with value = mkRApp(f,args_res.value)}) - args_res.result - } - | GApp _ -> assert false (* we have collected all the app in [glob_decompose_app] *) - | GLetIn(_,n,t,b) -> - (* if we have [(let x := v in b) t1 ... tn] , - we discard our work and compute the list of constructor for - [let x = v in (b t1 ... tn)] up to alpha conversion - *) - let new_n,new_b,new_avoid = - match n with - | Name id when List.exists (is_free_in id) args -> - (* need to alpha-convert the name *) - let new_id = Namegen.next_ident_away id avoid in - let new_avoid = id:: avoid in - let new_b = - replace_var_by_term - id - (GVar(dummy_loc,id)) - b - in - (Name new_id,new_b,new_avoid) - | _ -> n,b,avoid - in - build_entry_lc - env - funnames - avoid - (mkRLetIn(new_n,t,mkRApp(new_b,args))) - | GCases _ | GIf _ | GLetTuple _ -> - (* we have [(match e1, ...., en with ..... end) t1 tn] - we first compute the result from the case and - then combine each of them with each of args one - *) - let f_res = build_entry_lc env funnames args_res.to_avoid f in - combine_results combine_app f_res args_res - | GDynamic _ ->error "Not handled GDynamic" - | GCast(_,b,_) -> - (* for an applied cast we just trash the cast part - and restart the work. - - WARNING: We need to restart since [b] itself should be an application term - *) - build_entry_lc env funnames avoid (mkRApp(b,args)) - | GRec _ -> error "Not handled GRec" - | GProd _ -> error "Cannot apply a type" - end (* end of the application treatement *) - - | GLambda(_,n,_,t,b) -> - (* we first compute the list of constructor - corresponding to the body of the function, - then the one corresponding to the type - and combine the two result - *) - let t_res = build_entry_lc env funnames avoid t in - let new_n = - match n with - | Name _ -> n - | Anonymous -> Name (Indfun_common.fresh_id [] "_x") - in - let new_env = raw_push_named (new_n,None,t) env in - let b_res = build_entry_lc new_env funnames avoid b in - combine_results (combine_lam new_n) t_res b_res - | GProd(_,n,_,t,b) -> - (* we first compute the list of constructor - corresponding to the body of the function, - then the one corresponding to the type - and combine the two result - *) - let t_res = build_entry_lc env funnames avoid t in - let new_env = raw_push_named (n,None,t) env in - let b_res = build_entry_lc new_env funnames avoid b in - combine_results (combine_prod n) t_res b_res - | GLetIn(_,n,v,b) -> - (* we first compute the list of constructor - corresponding to the body of the function, - then the one corresponding to the value [t] - and combine the two result - *) - let v_res = build_entry_lc env funnames avoid v in - let v_as_constr = Pretyping.Default.understand Evd.empty env v in - let v_type = Typing.type_of env Evd.empty v_as_constr in - let new_env = - match n with - Anonymous -> env - | Name id -> Environ.push_named (id,Some v_as_constr,v_type) env - in - let b_res = build_entry_lc new_env funnames avoid b in - combine_results (combine_letin n) v_res b_res - | GCases(_,_,_,el,brl) -> - (* we create the discrimination function - and treat the case itself - *) - let make_discr = make_discr_match brl in - build_entry_lc_from_case env funnames make_discr el brl avoid - | GIf(_,b,(na,e_option),lhs,rhs) -> - let b_as_constr = Pretyping.Default.understand Evd.empty env b in - let b_typ = Typing.type_of env Evd.empty b_as_constr in - let (ind,_) = - try Inductiveops.find_inductive env Evd.empty b_typ - with Not_found -> - errorlabstrm "" (str "Cannot find the inductive associated to " ++ - Printer.pr_glob_constr b ++ str " in " ++ - Printer.pr_glob_constr rt ++ str ". try again with a cast") - in - let case_pats = build_constructors_of_type ind [] in - assert (Array.length case_pats = 2); - let brl = - list_map_i - (fun i x -> (dummy_loc,[],[case_pats.(i)],x)) - 0 - [lhs;rhs] - in - let match_expr = - mkRCases(None,[(b,(Anonymous,None))],brl) - in - (* Pp.msgnl (str "new case := " ++ Printer.pr_glob_constr match_expr); *) - build_entry_lc env funnames avoid match_expr - | GLetTuple(_,nal,_,b,e) -> - begin - let nal_as_glob_constr = - List.map - (function - Name id -> mkRVar id - | Anonymous -> mkRHole () - ) - nal - in - let b_as_constr = Pretyping.Default.understand Evd.empty env b in - let b_typ = Typing.type_of env Evd.empty b_as_constr in - let (ind,_) = - try Inductiveops.find_inductive env Evd.empty b_typ - with Not_found -> - errorlabstrm "" (str "Cannot find the inductive associated to " ++ - Printer.pr_glob_constr b ++ str " in " ++ - Printer.pr_glob_constr rt ++ str ". try again with a cast") - in - let case_pats = build_constructors_of_type ind nal_as_glob_constr in - assert (Array.length case_pats = 1); - let br = - (dummy_loc,[],[case_pats.(0)],e) - in - let match_expr = mkRCases(None,[b,(Anonymous,None)],[br]) in - build_entry_lc env funnames avoid match_expr - - end - | GRec _ -> error "Not handled GRec" - | GCast(_,b,_) -> - build_entry_lc env funnames avoid b - | GDynamic _ -> error "Not handled GDynamic" -and build_entry_lc_from_case env funname make_discr - (el:tomatch_tuples) - (brl:Glob_term.cases_clauses) avoid : - glob_constr build_entry_return = - match el with - | [] -> assert false (* this case correspond to match with .... !*) - | el -> - (* this case correspond to - match el with brl end - we first compute the list of lists corresponding to [el] and - combine them . - Then for each elemeent of the combinations, - we compute the result we compute one list per branch in [brl] and - finally we just concatenate those list - *) - let case_resl = - List.fold_right - (fun (case_arg,_) ctxt_argsl -> - let arg_res = build_entry_lc env funname avoid case_arg in - combine_results combine_args arg_res ctxt_argsl - ) - el - (mk_result [] [] avoid) - in - let types = - List.map (fun (case_arg,_) -> - let case_arg_as_constr = Pretyping.Default.understand Evd.empty env case_arg in - Typing.type_of env Evd.empty case_arg_as_constr - ) el - in - (****** The next works only if the match is not dependent ****) - let results = - List.map - (fun ca -> - let res = build_entry_lc_from_case_term - env types - funname (make_discr) - [] brl - case_resl.to_avoid - ca - in - res - ) - case_resl.result - in - { - result = List.concat (List.map (fun r -> r.result) results); - to_avoid = - List.fold_left (fun acc r -> list_union acc r.to_avoid) [] results - } - -and build_entry_lc_from_case_term env types funname make_discr patterns_to_prevent brl avoid - matched_expr = - match brl with - | [] -> (* computed_branches *) {result = [];to_avoid = avoid} - | br::brl' -> - (* alpha convertion to prevent name clashes *) - let _,idl,patl,return = alpha_br avoid br in - let new_avoid = idl@avoid in (* for now we can no more use idl as an indentifier *) - (* building a list of precondition stating that we are not in this branch - (will be used in the following recursive calls) - *) - let new_env = List.fold_right2 add_pat_variables patl types env in - let not_those_patterns : (identifier list -> glob_constr -> glob_constr) list = - List.map2 - (fun pat typ -> - fun avoid pat'_as_term -> - let renamed_pat,_,_ = alpha_pat avoid pat in - let pat_ids = get_pattern_id renamed_pat in - let env_with_pat_ids = add_pat_variables pat typ new_env in - List.fold_right - (fun id acc -> - let typ_of_id = - Typing.type_of env_with_pat_ids Evd.empty (mkVar id) - in - let raw_typ_of_id = - Detyping.detype false [] - (Termops.names_of_rel_context env_with_pat_ids) typ_of_id - in - mkRProd (Name id,raw_typ_of_id,acc)) - pat_ids - (glob_make_neq pat'_as_term (pattern_to_term renamed_pat)) - ) - patl - types - in - (* Checking if we can be in this branch - (will be used in the following recursive calls) - *) - 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 - (* - we first compute the other branch result (in ordrer to keep the order of the matching - as much as possible) - *) - let brl'_res = - build_entry_lc_from_case_term - env - types - funname - make_discr - ((unify_with_those_patterns,not_those_patterns)::patterns_to_prevent) - brl' - avoid - matched_expr - in - (* We now create the precondition of this branch i.e. - 1- the list of variable appearing in the different patterns of this branch and - the list of equation stating than el = patl (List.flatten ...) - 2- If there exists a previous branch which pattern unify with the one of this branch - then a discrimination precond stating that we are not in a previous branch (if List.exists ...) - *) - let those_pattern_preconds = - (List.flatten - ( - list_map3 - (fun pat e typ_as_constr -> - let this_pat_ids = ids_of_pat pat in - let typ = Detyping.detype false [] (Termops.names_of_rel_context new_env) typ_as_constr in - let pat_as_term = pattern_to_term pat in - List.fold_right - (fun id acc -> - if Idset.mem id this_pat_ids - then (Prod (Name id), - let typ_of_id = Typing.type_of new_env Evd.empty (mkVar id) in - let raw_typ_of_id = - Detyping.detype false [] (Termops.names_of_rel_context new_env) typ_of_id - in - raw_typ_of_id - )::acc - else acc - ) - idl - [(Prod Anonymous,glob_make_eq ~typ pat_as_term e)] - ) - patl - matched_expr.value - types - ) - ) - @ - (if List.exists (function (unifl,_) -> - let (unif,_) = - List.split (List.map2 (fun x y -> x y) unifl patl) - in - List.for_all (fun x -> x) unif) patterns_to_prevent - then - let i = List.length patterns_to_prevent in - let pats_as_constr = List.map2 (pattern_to_term_and_type new_env) types patl in - [(Prod Anonymous,make_discr pats_as_constr i )] - else - [] - ) - in - (* We compute the result of the value returned by the branch*) - let return_res = build_entry_lc new_env funname new_avoid return in - (* and combine it with the preconds computed for this branch *) - let this_branch_res = - List.map - (fun res -> - { context = matched_expr.context@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 - String.sub (string_of_id id) 0 3 = "res" - with Invalid_argument _ -> false - - -exception Continue -(* - The second phase which reconstruct the real type of the constructor. - rebuild the globalized constructors expression. - eliminates some meaningless equalities, applies some rewrites...... -*) -let rec rebuild_cons env nb_args relname args crossed_types depth rt = - observe (str "rebuilding : " ++ pr_glob_constr rt); - - match rt with - | GProd(_,n,k,t,b) -> - let not_free_in_t id = not (is_free_in id t) in - let new_crossed_types = t::crossed_types in - begin - match t with - | GApp(_,(GVar(_,res_id) as res_rt),args') when is_res res_id -> - begin - match args' with - | (GVar(_,this_relname))::args' -> - (*i The next call to mk_rel_id is - valid since we are constructing the graph - Ensures by: obvious - i*) - - let new_t = - mkRApp(mkRVar(mk_rel_id this_relname),args'@[res_rt]) - in - let t' = Pretyping.Default.understand Evd.empty env new_t in - let new_env = Environ.push_rel (n,None,t') env in - let new_b,id_to_exclude = - rebuild_cons new_env - nb_args relname - args new_crossed_types - (depth + 1) b - in - mkRProd(n,new_t,new_b), - Idset.filter not_free_in_t id_to_exclude - | _ -> (* the first args is the name of the function! *) - assert false - end - | GApp(loc1,GRef(loc2,eq_as_ref),[ty;GVar(loc3,id);rt]) - when eq_as_ref = Lazy.force Coqlib.coq_eq_ref && n = Anonymous - -> - begin - try - observe (str "computing new type for eq : " ++ pr_glob_constr rt); - let t' = - try Pretyping.Default.understand Evd.empty env t with _ -> raise Continue - in - let is_in_b = is_free_in id b in - let _keep_eq = - not (List.exists (is_free_in id) args) || is_in_b || - List.exists (is_free_in id) crossed_types - in - let new_args = List.map (replace_var_by_term id rt) args in - let subst_b = - if is_in_b then b else replace_var_by_term id rt b - in - let new_env = Environ.push_rel (n,None,t') env in - let new_b,id_to_exclude = - rebuild_cons - new_env - nb_args relname - new_args new_crossed_types - (depth + 1) subst_b - in - mkRProd(n,t,new_b),id_to_exclude - with Continue -> - let jmeq = Libnames.IndRef (destInd (jmeq ())) in - let ty' = Pretyping.Default.understand Evd.empty env ty in - let ind,args' = Inductive.find_inductive env ty' in - let mib,_ = Global.lookup_inductive ind in - let nparam = mib.Declarations.mind_nparams in - let params,arg' = - ((Util.list_chop nparam args')) - in - let rt_typ = - GApp(Util.dummy_loc, - GRef (Util.dummy_loc,Libnames.IndRef ind), - (List.map - (fun p -> Detyping.detype false [] - (Termops.names_of_rel_context env) - p) params)@(Array.to_list - (Array.make - (List.length args' - nparam) - (mkRHole ())))) - in - let eq' = - GApp(loc1,GRef(loc2,jmeq),[ty;GVar(loc3,id);rt_typ;rt]) - in - observe (str "computing new type for jmeq : " ++ pr_glob_constr eq'); - let eq'_as_constr = Pretyping.Default.understand Evd.empty env eq' in - observe (str " computing new type for jmeq : done") ; - let new_args = - match kind_of_term eq'_as_constr with - | App(_,[|_;_;ty;_|]) -> - let ty = Array.to_list (snd (destApp ty)) in - let ty' = snd (Util.list_chop nparam ty) in - List.fold_left2 - (fun acc var_as_constr arg -> - if isRel var_as_constr - then - let (na,_,_) = - Environ.lookup_rel (destRel var_as_constr) env - in - match na with - | Anonymous -> acc - | Name id' -> - (id',Detyping.detype false [] - (Termops.names_of_rel_context env) - arg)::acc - else if isVar var_as_constr - then (destVar var_as_constr,Detyping.detype false [] - (Termops.names_of_rel_context env) - arg)::acc - else acc - ) - [] - arg' - ty' - | _ -> assert false - in - let is_in_b = is_free_in id b in - let _keep_eq = - not (List.exists (is_free_in id) args) || is_in_b || - List.exists (is_free_in id) crossed_types - in - let new_args = - List.fold_left - (fun args (id,rt) -> - List.map (replace_var_by_term id rt) args - ) - args - ((id,rt)::new_args) - in - let subst_b = - if is_in_b then b else replace_var_by_term id rt b - in - let new_env = - let t' = Pretyping.Default.understand Evd.empty env eq' in - Environ.push_rel (n,None,t') env - in - let new_b,id_to_exclude = - rebuild_cons - new_env - nb_args relname - new_args new_crossed_types - (depth + 1) subst_b - in - mkRProd(n,eq',new_b),id_to_exclude - end - (* J.F:. keep this comment it explain how to remove some meaningless equalities - if keep_eq then - mkRProd(n,t,new_b),id_to_exclude - else new_b, Idset.add id id_to_exclude - *) - | _ -> - observe (str "computing new type for prod : " ++ pr_glob_constr rt); - let t' = Pretyping.Default.understand Evd.empty env t in - let new_env = Environ.push_rel (n,None,t') env in - let new_b,id_to_exclude = - rebuild_cons new_env - nb_args relname - args new_crossed_types - (depth + 1) b - in - match n with - | Name id when Idset.mem id id_to_exclude && depth >= nb_args -> - new_b,Idset.remove id - (Idset.filter not_free_in_t id_to_exclude) - | _ -> mkRProd(n,t,new_b),Idset.filter not_free_in_t id_to_exclude - end - | GLambda(_,n,k,t,b) -> - begin - let not_free_in_t id = not (is_free_in id t) in - let new_crossed_types = t :: crossed_types in - observe (str "computing new type for lambda : " ++ pr_glob_constr rt); - let t' = Pretyping.Default.understand Evd.empty env t in - match n with - | Name id -> - let new_env = Environ.push_rel (n,None,t') env in - let new_b,id_to_exclude = - rebuild_cons new_env - nb_args relname - (args@[mkRVar id])new_crossed_types - (depth + 1 ) b - in - if Idset.mem id id_to_exclude && depth >= nb_args - then - new_b, Idset.remove id (Idset.filter not_free_in_t id_to_exclude) - else - GProd(dummy_loc,n,k,t,new_b),Idset.filter not_free_in_t id_to_exclude - | _ -> anomaly "Should not have an anonymous function here" - (* We have renamed all the anonymous functions during alpha_renaming phase *) - - end - | GLetIn(_,n,t,b) -> - begin - let not_free_in_t id = not (is_free_in id t) in - let t' = Pretyping.Default.understand Evd.empty env t in - let type_t' = Typing.type_of env Evd.empty t' in - let new_env = Environ.push_rel (n,Some t',type_t') env in - let new_b,id_to_exclude = - rebuild_cons new_env - nb_args relname - args (t::crossed_types) - (depth + 1 ) b in - match n with - | Name id when Idset.mem id id_to_exclude && depth >= nb_args -> - new_b,Idset.remove id (Idset.filter not_free_in_t id_to_exclude) - | _ -> GLetIn(dummy_loc,n,t,new_b), - Idset.filter not_free_in_t id_to_exclude - end - | GLetTuple(_,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 env - nb_args - relname - args (crossed_types) - depth t - in - let t' = Pretyping.Default.understand Evd.empty env new_t in - let new_env = Environ.push_rel (na,None,t') env in - let new_b,id_to_exclude = - rebuild_cons new_env - nb_args relname - args (t::crossed_types) - (depth + 1) 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) *) -(* | _ -> *) - GLetTuple(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 - - -(* debuging wrapper *) -let rebuild_cons env nb_args relname args crossed_types rt = -(* observennl (str "rebuild_cons : rt := "++ pr_glob_constr rt ++ *) -(* str "nb_args := " ++ str (string_of_int nb_args)); *) - let res = - rebuild_cons env nb_args relname args crossed_types 0 rt - in -(* observe (str " leads to "++ pr_glob_constr (fst res)); *) - res - - -(* naive implementation of parameter detection. - - A parameter is an argument which is only preceded by parameters and whose - calls are all syntaxically equal. - - TODO: Find a valid way to deal with implicit arguments here! -*) -let rec compute_cst_params relnames params = function - | GRef _ | GVar _ | GEvar _ | GPatVar _ -> params - | GApp(_,GVar(_,relname'),rtl) when Idset.mem relname' relnames -> - compute_cst_params_from_app [] (params,rtl) - | GApp(_,f,args) -> - List.fold_left (compute_cst_params relnames) params (f::args) - | GLambda(_,_,_,t,b) | GProd(_,_,_,t,b) | GLetIn(_,_,t,b) | GLetTuple(_,_,_,t,b) -> - let t_params = compute_cst_params relnames params t in - compute_cst_params relnames t_params b - | GCases _ -> - params (* If there is still cases at this point they can only be - discriminitation ones *) - | GSort _ -> params - | GHole _ -> params - | GIf _ | GRec _ | GCast _ | GDynamic _ -> - raise (UserError("compute_cst_params", str "Not handled case")) -and compute_cst_params_from_app acc (params,rtl) = - match params,rtl with - | _::_,[] -> assert false (* the rel has at least nargs + 1 arguments ! *) - | ((Name id,_,is_defined) as param)::params',(GVar(_,id'))::rtl' - when id_ord id id' == 0 && not is_defined -> - compute_cst_params_from_app (param::acc) (params',rtl') - | _ -> List.rev acc - -let compute_params_name relnames (args : (Names.name * Glob_term.glob_constr * bool) list array) csts = - let rels_params = - Array.mapi - (fun i args -> - List.fold_left - (fun params (_,cst) -> compute_cst_params relnames params cst) - args - csts.(i) - ) - args - in - let l = ref [] in - let _ = - try - list_iter_i - (fun i ((n,nt,is_defined) as param) -> - if array_for_all - (fun l -> - let (n',nt',is_defined') = List.nth l i in - n = n' && Topconstr.eq_glob_constr nt nt' && is_defined = is_defined') - rels_params - then - l := param::!l - ) - rels_params.(0) - with _ -> - () - in - List.rev !l - -let rec rebuild_return_type rt = - match rt with - | Topconstr.CProdN(loc,n,t') -> - Topconstr.CProdN(loc,n,rebuild_return_type t') - | Topconstr.CArrow(loc,t,t') -> - Topconstr.CArrow(loc,t,rebuild_return_type t') - | Topconstr.CLetIn(loc,na,t,t') -> - Topconstr.CLetIn(loc,na,t,rebuild_return_type t') - | _ -> Topconstr.CArrow(dummy_loc,rt,Topconstr.CSort(dummy_loc,RType None)) - - -let do_build_inductive - funnames (funsargs: (Names.name * glob_constr * bool) list list) - returned_types - (rtl:glob_constr list) = - let _time1 = System.get_time () in -(* Pp.msgnl (prlist_with_sep fnl Printer.pr_glob_constr rtl); *) - 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 - let returned_types = Array.of_list returned_types in - (* alpha_renaming of the body to prevent variable capture during manipulation *) - let rtl_alpha = List.map (function rt -> expand_as (alpha_rt [] rt)) rtl in - let rta = Array.of_list rtl_alpha in - (*i The next call to mk_rel_id is valid since we are constructing the graph - Ensures by: obvious - i*) - let relnames = Array.map mk_rel_id funnames in - let relnames_as_set = Array.fold_right Idset.add relnames Idset.empty in - (* Construction of the pseudo constructors *) - let env = - Array.fold_right - (fun id env -> - Environ.push_named (id,None,Typing.type_of env Evd.empty (Constrintern.global_reference id)) env - ) - funnames - (Global.env ()) - in - let resa = Array.map (build_entry_lc env funnames_as_set []) rta in - let env_with_graphs = - let rel_arity i funargs = (* Reduilding arities (with parameters) *) - let rel_first_args :(Names.name * Glob_term.glob_constr * bool ) list = - funargs - in - List.fold_right - (fun (n,t,is_defined) acc -> - if is_defined - then - Topconstr.CLetIn(dummy_loc,(dummy_loc, n),Constrextern.extern_glob_constr Idset.empty t, - acc) - else - Topconstr.CProdN - (dummy_loc, - [[(dummy_loc,n)],Topconstr.default_binder_kind,Constrextern.extern_glob_constr Idset.empty t], - acc - ) - ) - rel_first_args - (rebuild_return_type returned_types.(i)) - in - (* We need to lift back our work topconstr but only with all information - We mimick a Set Printing All. - Then save the graphs and reset Printing options to their primitive values - *) - let rel_arities = Array.mapi rel_arity funsargs in - Util.array_fold_left2 (fun env rel_name rel_ar -> - Environ.push_named (rel_name,None, Constrintern.interp_constr Evd.empty env rel_ar) env) env relnames rel_arities - in - (* and of the real constructors*) - let constr i res = - List.map - (function result (* (args',concl') *) -> - let rt = compose_glob_context result.context result.value in - let nb_args = List.length funsargs.(i) in - (* with_full_print (fun rt -> Pp.msgnl (str "glob constr " ++ pr_glob_constr rt)) rt; *) - fst ( - rebuild_cons env_with_graphs nb_args relnames.(i) - [] - [] - rt - ) - ) - res.result - in - (* adding names to constructors *) - let next_constructor_id = ref (-1) in - let mk_constructor_id i = - incr next_constructor_id; - (*i The next call to mk_rel_id is valid since we are constructing the graph - Ensures by: obvious - i*) - id_of_string ((string_of_id (mk_rel_id funnames.(i)))^"_"^(string_of_int !next_constructor_id)) - in - let rel_constructors i rt : (identifier*glob_constr) list = - next_constructor_id := (-1); - List.map (fun constr -> (mk_constructor_id i),constr) (constr i rt) - in - let rel_constructors = Array.mapi rel_constructors resa in - (* Computing the set of parameters if asked *) - let rels_params = compute_params_name relnames_as_set funsargs rel_constructors in - let nrel_params = List.length rels_params in - let rel_constructors = (* Taking into account the parameters in constructors *) - Array.map (List.map - (fun (id,rt) -> (id,snd (chop_rprod_n nrel_params rt)))) - rel_constructors - in - let rel_arity i funargs = (* Reduilding arities (with parameters) *) - let rel_first_args :(Names.name * Glob_term.glob_constr * bool ) list = - (snd (list_chop nrel_params funargs)) - in - List.fold_right - (fun (n,t,is_defined) acc -> - if is_defined - then - Topconstr.CLetIn(dummy_loc,(dummy_loc, n),Constrextern.extern_glob_constr Idset.empty t, - acc) - else - Topconstr.CProdN - (dummy_loc, - [[(dummy_loc,n)],Topconstr.default_binder_kind,Constrextern.extern_glob_constr Idset.empty t], - acc - ) - ) - rel_first_args - (rebuild_return_type returned_types.(i)) - in - (* We need to lift back our work topconstr but only with all information - We mimick a Set Printing All. - Then save the graphs and reset Printing options to their primitive values - *) - let rel_arities = Array.mapi rel_arity funsargs in - let rel_params = - List.map - (fun (n,t,is_defined) -> - if is_defined - then - Topconstr.LocalRawDef((dummy_loc,n), Constrextern.extern_glob_constr Idset.empty t) - else - Topconstr.LocalRawAssum - ([(dummy_loc,n)], Topconstr.default_binder_kind, Constrextern.extern_glob_constr Idset.empty t) - ) - rels_params - in - let ext_rels_constructors = - Array.map (List.map - (fun (id,t) -> - false,((dummy_loc,id), - Flags.with_option - Flags.raw_print - (Constrextern.extern_glob_type Idset.empty) ((* zeta_normalize *) t) - ) - )) - (rel_constructors) - in - let rel_ind i ext_rel_constructors = - ((dummy_loc,relnames.(i)), - rel_params, - Some rel_arities.(i), - ext_rel_constructors),[] - in - let ext_rel_constructors = (Array.mapi rel_ind ext_rels_constructors) in - let rel_inds = Array.to_list ext_rel_constructors in -(* let _ = *) -(* Pp.msgnl (\* observe *\) ( *) -(* str "Inductive" ++ spc () ++ *) -(* prlist_with_sep *) -(* (fun () -> fnl ()++spc () ++ str "with" ++ spc ()) *) -(* (function ((_,id),_,params,ar,constr) -> *) -(* Ppconstr.pr_id id ++ spc () ++ *) -(* Ppconstr.pr_binders params ++ spc () ++ *) -(* str ":" ++ spc () ++ *) -(* Ppconstr.pr_lconstr_expr ar ++ spc () ++ str ":=" ++ *) -(* prlist_with_sep *) -(* (fun _ -> fnl () ++ spc () ++ str "|" ++ spc ()) *) -(* (function (_,((_,id),t)) -> *) -(* Ppconstr.pr_id id ++ spc () ++ str ":" ++ spc () ++ *) -(* Ppconstr.pr_lconstr_expr t) *) -(* constr *) -(* ) *) -(* rel_inds *) -(* ) *) -(* in *) - let _time2 = System.get_time () in - try - with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds)) true - with - | UserError(s,msg) as e -> - let _time3 = System.get_time () in -(* Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *) - let repacked_rel_inds = - List.map (fun ((a , b , c , l),ntn) -> ((false,a) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn ) - rel_inds - in - let msg = - str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Decl_kinds.Finite,false,repacked_rel_inds)) - ++ fnl () ++ - msg - in - observe (msg); - raise e - | e -> - let _time3 = System.get_time () in -(* Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *) - let repacked_rel_inds = - List.map (fun ((a , b , c , l),ntn) -> ((false,a) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn ) - rel_inds - in - let msg = - str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Decl_kinds.Finite,false,repacked_rel_inds)) - ++ fnl () ++ - Cerrors.explain_exn e - in - observe msg; - raise e - - - -let build_inductive funnames funsargs returned_types rtl = - try - do_build_inductive funnames funsargs returned_types rtl - with e -> raise (Building_graph e) - - diff --git a/plugins/funind/rawterm_to_relation.mli b/plugins/funind/rawterm_to_relation.mli deleted file mode 100644 index 5c91292bad..0000000000 --- a/plugins/funind/rawterm_to_relation.mli +++ /dev/null @@ -1,16 +0,0 @@ - - - -(* - [build_inductive parametrize funnames funargs returned_types bodies] - constructs and saves the graphs of the functions [funnames] taking [funargs] as arguments - and returning [returned_types] using bodies [bodies] -*) - -val build_inductive : - Names.identifier list -> (* The list of function name *) - (Names.name*Glob_term.glob_constr*bool) list list -> (* The list of function args *) - Topconstr.constr_expr list -> (* The list of function returned type *) - Glob_term.glob_constr list -> (* the list of body *) - unit - diff --git a/plugins/funind/rawtermops.ml b/plugins/funind/rawtermops.ml deleted file mode 100644 index 0cf91f38c0..0000000000 --- a/plugins/funind/rawtermops.ml +++ /dev/null @@ -1,718 +0,0 @@ -open Pp -open Glob_term -open Util -open Names -(* Ocaml 3.06 Map.S does not handle is_empty *) -let idmap_is_empty m = m = Idmap.empty - -(* - Some basic functions to rebuild glob_constr - In each of them the location is Util.dummy_loc -*) -let mkRRef ref = GRef(dummy_loc,ref) -let mkRVar id = GVar(dummy_loc,id) -let mkRApp(rt,rtl) = GApp(dummy_loc,rt,rtl) -let mkRLambda(n,t,b) = GLambda(dummy_loc,n,Explicit,t,b) -let mkRProd(n,t,b) = GProd(dummy_loc,n,Explicit,t,b) -let mkRLetIn(n,t,b) = GLetIn(dummy_loc,n,t,b) -let mkRCases(rto,l,brl) = GCases(dummy_loc,Term.RegularStyle,rto,l,brl) -let mkRSort s = GSort(dummy_loc,s) -let mkRHole () = GHole(dummy_loc,Evd.BinderType Anonymous) -let mkRCast(b,t) = GCast(dummy_loc,b,CastConv (Term.DEFAULTcast,t)) - -(* - Some basic functions to decompose glob_constrs - These are analogous to the ones constrs -*) -let glob_decompose_prod = - let rec glob_decompose_prod args = function - | GProd(_,n,k,t,b) -> - glob_decompose_prod ((n,t)::args) b - | rt -> args,rt - in - glob_decompose_prod [] - -let glob_decompose_prod_or_letin = - let rec glob_decompose_prod args = function - | GProd(_,n,k,t,b) -> - glob_decompose_prod ((n,None,Some t)::args) b - | GLetIn(_,n,t,b) -> - glob_decompose_prod ((n,Some t,None)::args) b - | rt -> args,rt - in - glob_decompose_prod [] - -let glob_compose_prod = - List.fold_left (fun b (n,t) -> mkRProd(n,t,b)) - -let glob_compose_prod_or_letin = - List.fold_left ( - fun concl decl -> - match decl with - | (n,None,Some t) -> mkRProd(n,t,concl) - | (n,Some bdy,None) -> mkRLetIn(n,bdy,concl) - | _ -> assert false) - -let glob_decompose_prod_n n = - let rec glob_decompose_prod i args c = - if i<=0 then args,c - else - match c with - | GProd(_,n,_,t,b) -> - glob_decompose_prod (i-1) ((n,t)::args) b - | rt -> args,rt - in - glob_decompose_prod n [] - - -let glob_decompose_prod_or_letin_n n = - let rec glob_decompose_prod i args c = - if i<=0 then args,c - else - match c with - | GProd(_,n,_,t,b) -> - glob_decompose_prod (i-1) ((n,None,Some t)::args) b - | GLetIn(_,n,t,b) -> - glob_decompose_prod (i-1) ((n,Some t,None)::args) b - | rt -> args,rt - in - glob_decompose_prod n [] - - -let glob_decompose_app = - let rec decompose_rapp acc rt = -(* msgnl (str "glob_decompose_app on : "++ Printer.pr_glob_constr rt); *) - match rt with - | GApp(_,rt,rtl) -> - decompose_rapp (List.fold_left (fun y x -> x::y) acc rtl) rt - | rt -> rt,List.rev acc - in - decompose_rapp [] - - - - -(* [glob_make_eq t1 t2] build the glob_constr corresponding to [t2 = t1] *) -let glob_make_eq ?(typ= mkRHole ()) t1 t2 = - mkRApp(mkRRef (Lazy.force Coqlib.coq_eq_ref),[typ;t2;t1]) - -(* [glob_make_neq t1 t2] build the glob_constr corresponding to [t1 <> t2] *) -let glob_make_neq t1 t2 = - mkRApp(mkRRef (Lazy.force Coqlib.coq_not_ref),[glob_make_eq t1 t2]) - -(* [glob_make_or P1 P2] build the glob_constr corresponding to [P1 \/ P2] *) -let glob_make_or t1 t2 = mkRApp (mkRRef(Lazy.force Coqlib.coq_or_ref),[t1;t2]) - -(* [glob_make_or_list [P1;...;Pn]] build the glob_constr corresponding - to [P1 \/ ( .... \/ Pn)] -*) -let rec glob_make_or_list = function - | [] -> raise (Invalid_argument "mk_or") - | [e] -> e - | e::l -> glob_make_or e (glob_make_or_list l) - - -let remove_name_from_mapping mapping na = - match na with - | Anonymous -> mapping - | Name id -> Idmap.remove id mapping - -let change_vars = - let rec change_vars mapping rt = - match rt with - | GRef _ -> rt - | GVar(loc,id) -> - let new_id = - try - Idmap.find id mapping - with Not_found -> id - in - GVar(loc,new_id) - | GEvar _ -> rt - | GPatVar _ -> rt - | GApp(loc,rt',rtl) -> - GApp(loc, - change_vars mapping rt', - List.map (change_vars mapping) rtl - ) - | GLambda(loc,name,k,t,b) -> - GLambda(loc, - name, - k, - change_vars mapping t, - change_vars (remove_name_from_mapping mapping name) b - ) - | GProd(loc,name,k,t,b) -> - GProd(loc, - name, - k, - change_vars mapping t, - change_vars (remove_name_from_mapping mapping name) b - ) - | GLetIn(loc,name,def,b) -> - GLetIn(loc, - name, - change_vars mapping def, - change_vars (remove_name_from_mapping mapping name) b - ) - | GLetTuple(loc,nal,(na,rto),b,e) -> - let new_mapping = List.fold_left remove_name_from_mapping mapping nal in - GLetTuple(loc, - nal, - (na, Option.map (change_vars mapping) rto), - change_vars mapping b, - change_vars new_mapping e - ) - | GCases(loc,sty,infos,el,brl) -> - GCases(loc,sty, - infos, - List.map (fun (e,x) -> (change_vars mapping e,x)) el, - List.map (change_vars_br mapping) brl - ) - | GIf(loc,b,(na,e_option),lhs,rhs) -> - GIf(loc, - change_vars mapping b, - (na,Option.map (change_vars mapping) e_option), - change_vars mapping lhs, - change_vars mapping rhs - ) - | GRec _ -> error "Local (co)fixes are not supported" - | GSort _ -> rt - | GHole _ -> rt - | GCast(loc,b,CastConv (k,t)) -> - GCast(loc,change_vars mapping b, CastConv (k,change_vars mapping t)) - | GCast(loc,b,CastCoerce) -> - GCast(loc,change_vars mapping b,CastCoerce) - | GDynamic _ -> error "Not handled GDynamic" - and change_vars_br mapping ((loc,idl,patl,res) as br) = - let new_mapping = List.fold_right Idmap.remove idl mapping in - if idmap_is_empty new_mapping - then br - else (loc,idl,patl,change_vars new_mapping res) - in - change_vars - - - -let rec alpha_pat excluded pat = - match pat with - | PatVar(loc,Anonymous) -> - let new_id = Indfun_common.fresh_id excluded "_x" in - PatVar(loc,Name new_id),(new_id::excluded),Idmap.empty - | PatVar(loc,Name id) -> - if List.mem id excluded - then - let new_id = Namegen.next_ident_away id excluded in - PatVar(loc,Name new_id),(new_id::excluded), - (Idmap.add id new_id Idmap.empty) - else pat,excluded,Idmap.empty - | PatCstr(loc,constr,patl,na) -> - let new_na,new_excluded,map = - match na with - | Name id when List.mem id excluded -> - let new_id = Namegen.next_ident_away id excluded in - Name new_id,new_id::excluded, Idmap.add id new_id Idmap.empty - | _ -> na,excluded,Idmap.empty - in - let new_patl,new_excluded,new_map = - List.fold_left - (fun (patl,excluded,map) pat -> - let new_pat,new_excluded,new_map = alpha_pat excluded pat in - (new_pat::patl,new_excluded,Idmap.fold Idmap.add new_map map) - ) - ([],new_excluded,map) - patl - in - PatCstr(loc,constr,List.rev new_patl,new_na),new_excluded,new_map - -let alpha_patl excluded patl = - let patl,new_excluded,map = - List.fold_left - (fun (patl,excluded,map) pat -> - let new_pat,new_excluded,new_map = alpha_pat excluded pat in - new_pat::patl,new_excluded,(Idmap.fold Idmap.add new_map map) - ) - ([],excluded,Idmap.empty) - patl - in - (List.rev patl,new_excluded,map) - - - - -let raw_get_pattern_id pat acc = - let rec get_pattern_id pat = - match pat with - | PatVar(loc,Anonymous) -> assert false - | PatVar(loc,Name id) -> - [id] - | PatCstr(loc,constr,patternl,_) -> - List.fold_right - (fun pat idl -> - let idl' = get_pattern_id pat in - idl'@idl - ) - patternl - [] - in - (get_pattern_id pat)@acc - -let get_pattern_id pat = raw_get_pattern_id pat [] - -let rec alpha_rt excluded rt = - let new_rt = - match rt with - | GRef _ | GVar _ | GEvar _ | GPatVar _ -> rt - | GLambda(loc,Anonymous,k,t,b) -> - let new_id = Namegen.next_ident_away (id_of_string "_x") excluded in - let new_excluded = new_id :: excluded in - let new_t = alpha_rt new_excluded t in - let new_b = alpha_rt new_excluded b in - GLambda(loc,Name new_id,k,new_t,new_b) - | GProd(loc,Anonymous,k,t,b) -> - let new_t = alpha_rt excluded t in - let new_b = alpha_rt excluded b in - GProd(loc,Anonymous,k,new_t,new_b) - | GLetIn(loc,Anonymous,t,b) -> - let new_t = alpha_rt excluded t in - let new_b = alpha_rt excluded b in - GLetIn(loc,Anonymous,new_t,new_b) - | GLambda(loc,Name id,k,t,b) -> - let new_id = Namegen.next_ident_away id excluded in - let t,b = - if new_id = id - then t,b - else - let replace = change_vars (Idmap.add id new_id Idmap.empty) in - (t,replace b) - in - let new_excluded = new_id::excluded in - let new_t = alpha_rt new_excluded t in - let new_b = alpha_rt new_excluded b in - GLambda(loc,Name new_id,k,new_t,new_b) - | GProd(loc,Name id,k,t,b) -> - let new_id = Namegen.next_ident_away id excluded in - let new_excluded = new_id::excluded in - let t,b = - if new_id = id - then t,b - else - let replace = change_vars (Idmap.add id new_id Idmap.empty) in - (t,replace b) - in - let new_t = alpha_rt new_excluded t in - let new_b = alpha_rt new_excluded b in - GProd(loc,Name new_id,k,new_t,new_b) - | GLetIn(loc,Name id,t,b) -> - let new_id = Namegen.next_ident_away id excluded in - let t,b = - if new_id = id - then t,b - else - let replace = change_vars (Idmap.add id new_id Idmap.empty) in - (t,replace b) - in - let new_excluded = new_id::excluded in - let new_t = alpha_rt new_excluded t in - let new_b = alpha_rt new_excluded b in - GLetIn(loc,Name new_id,new_t,new_b) - - - | GLetTuple(loc,nal,(na,rto),t,b) -> - let rev_new_nal,new_excluded,mapping = - List.fold_left - (fun (nal,excluded,mapping) na -> - match na with - | Anonymous -> (na::nal,excluded,mapping) - | Name id -> - let new_id = Namegen.next_ident_away id excluded in - if new_id = id - then - na::nal,id::excluded,mapping - else - (Name new_id)::nal,id::excluded,(Idmap.add id new_id mapping) - ) - ([],excluded,Idmap.empty) - nal - in - let new_nal = List.rev rev_new_nal in - let new_rto,new_t,new_b = - if idmap_is_empty mapping - then rto,t,b - else let replace = change_vars mapping in - (Option.map replace rto, t,replace b) - in - let new_t = alpha_rt new_excluded new_t in - let new_b = alpha_rt new_excluded new_b in - let new_rto = Option.map (alpha_rt new_excluded) new_rto in - GLetTuple(loc,new_nal,(na,new_rto),new_t,new_b) - | GCases(loc,sty,infos,el,brl) -> - let new_el = - List.map (function (rt,i) -> alpha_rt excluded rt, i) el - in - GCases(loc,sty,infos,new_el,List.map (alpha_br excluded) brl) - | GIf(loc,b,(na,e_o),lhs,rhs) -> - GIf(loc,alpha_rt excluded b, - (na,Option.map (alpha_rt excluded) e_o), - alpha_rt excluded lhs, - alpha_rt excluded rhs - ) - | GRec _ -> error "Not handled GRec" - | GSort _ -> rt - | GHole _ -> rt - | GCast (loc,b,CastConv (k,t)) -> - GCast(loc,alpha_rt excluded b,CastConv(k,alpha_rt excluded t)) - | GCast (loc,b,CastCoerce) -> - GCast(loc,alpha_rt excluded b,CastCoerce) - | GDynamic _ -> error "Not handled GDynamic" - | GApp(loc,f,args) -> - GApp(loc, - alpha_rt excluded f, - List.map (alpha_rt excluded) args - ) - in - new_rt - -and alpha_br excluded (loc,ids,patl,res) = - let new_patl,new_excluded,mapping = alpha_patl excluded patl in - let new_ids = List.fold_right raw_get_pattern_id new_patl [] in - let new_excluded = new_ids@excluded in - let renamed_res = change_vars mapping res in - let new_res = alpha_rt new_excluded renamed_res in - (loc,new_ids,new_patl,new_res) - -(* - [is_free_in id rt] checks if [id] is a free variable in [rt] -*) -let is_free_in id = - let rec is_free_in = function - | GRef _ -> false - | GVar(_,id') -> id_ord id' id == 0 - | GEvar _ -> false - | GPatVar _ -> false - | GApp(_,rt,rtl) -> List.exists is_free_in (rt::rtl) - | GLambda(_,n,_,t,b) | GProd(_,n,_,t,b) | GLetIn(_,n,t,b) -> - let check_in_b = - match n with - | Name id' -> id_ord id' id <> 0 - | _ -> true - in - is_free_in t || (check_in_b && is_free_in b) - | GCases(_,_,_,el,brl) -> - (List.exists (fun (e,_) -> is_free_in e) el) || - List.exists is_free_in_br brl - | GLetTuple(_,nal,_,b,t) -> - let check_in_nal = - not (List.exists (function Name id' -> id'= id | _ -> false) nal) - in - is_free_in t || (check_in_nal && is_free_in b) - - | GIf(_,cond,_,br1,br2) -> - is_free_in cond || is_free_in br1 || is_free_in br2 - | GRec _ -> raise (UserError("",str "Not handled GRec")) - | GSort _ -> false - | GHole _ -> false - | GCast (_,b,CastConv (_,t)) -> is_free_in b || is_free_in t - | GCast (_,b,CastCoerce) -> is_free_in b - | GDynamic _ -> raise (UserError("",str "Not handled GDynamic")) - and is_free_in_br (_,ids,_,rt) = - (not (List.mem id ids)) && is_free_in rt - in - is_free_in - - - -let rec pattern_to_term = function - | PatVar(loc,Anonymous) -> assert false - | PatVar(loc,Name id) -> - mkRVar id - | PatCstr(loc,constr,patternl,_) -> - let cst_narg = - Inductiveops.mis_constructor_nargs_env - (Global.env ()) - constr - in - let implicit_args = - Array.to_list - (Array.init - (cst_narg - List.length patternl) - (fun _ -> mkRHole ()) - ) - in - let patl_as_term = - List.map pattern_to_term patternl - in - mkRApp(mkRRef(Libnames.ConstructRef constr), - implicit_args@patl_as_term - ) - - - -let replace_var_by_term x_id term = - let rec replace_var_by_pattern rt = - match rt with - | GRef _ -> rt - | GVar(_,id) when id_ord id x_id == 0 -> term - | GVar _ -> rt - | GEvar _ -> rt - | GPatVar _ -> rt - | GApp(loc,rt',rtl) -> - GApp(loc, - replace_var_by_pattern rt', - List.map replace_var_by_pattern rtl - ) - | GLambda(_,Name id,_,_,_) when id_ord id x_id == 0 -> rt - | GLambda(loc,name,k,t,b) -> - GLambda(loc, - name, - k, - replace_var_by_pattern t, - replace_var_by_pattern b - ) - | GProd(_,Name id,_,_,_) when id_ord id x_id == 0 -> rt - | GProd(loc,name,k,t,b) -> - GProd(loc, - name, - k, - replace_var_by_pattern t, - replace_var_by_pattern b - ) - | GLetIn(_,Name id,_,_) when id_ord id x_id == 0 -> rt - | GLetIn(loc,name,def,b) -> - GLetIn(loc, - name, - replace_var_by_pattern def, - replace_var_by_pattern b - ) - | GLetTuple(_,nal,_,_,_) - when List.exists (function Name id -> id = x_id | _ -> false) nal -> - rt - | GLetTuple(loc,nal,(na,rto),def,b) -> - GLetTuple(loc, - nal, - (na,Option.map replace_var_by_pattern rto), - replace_var_by_pattern def, - replace_var_by_pattern b - ) - | GCases(loc,sty,infos,el,brl) -> - GCases(loc,sty, - infos, - List.map (fun (e,x) -> (replace_var_by_pattern e,x)) el, - List.map replace_var_by_pattern_br brl - ) - | GIf(loc,b,(na,e_option),lhs,rhs) -> - GIf(loc, replace_var_by_pattern b, - (na,Option.map replace_var_by_pattern e_option), - replace_var_by_pattern lhs, - replace_var_by_pattern rhs - ) - | GRec _ -> raise (UserError("",str "Not handled GRec")) - | GSort _ -> rt - | GHole _ -> rt - | GCast(loc,b,CastConv(k,t)) -> - GCast(loc,replace_var_by_pattern b,CastConv(k,replace_var_by_pattern t)) - | GCast(loc,b,CastCoerce) -> - GCast(loc,replace_var_by_pattern b,CastCoerce) - | GDynamic _ -> raise (UserError("",str "Not handled GDynamic")) - and replace_var_by_pattern_br ((loc,idl,patl,res) as br) = - if List.exists (fun id -> id_ord id x_id == 0) idl - then br - else (loc,idl,patl,replace_var_by_pattern res) - in - replace_var_by_pattern - - - - -(* checking unifiability of patterns *) -exception NotUnifiable - -let rec are_unifiable_aux = function - | [] -> () - | eq::eqs -> - match eq with - | PatVar _,_ | _,PatVar _ -> are_unifiable_aux eqs - | PatCstr(_,constructor1,cpl1,_),PatCstr(_,constructor2,cpl2,_) -> - if constructor2 <> constructor1 - then raise NotUnifiable - else - let eqs' = - try ((List.combine cpl1 cpl2)@eqs) - with _ -> anomaly "are_unifiable_aux" - in - are_unifiable_aux eqs' - -let are_unifiable pat1 pat2 = - try - are_unifiable_aux [pat1,pat2]; - true - with NotUnifiable -> false - - -let rec eq_cases_pattern_aux = function - | [] -> () - | eq::eqs -> - match eq with - | PatVar _,PatVar _ -> eq_cases_pattern_aux eqs - | PatCstr(_,constructor1,cpl1,_),PatCstr(_,constructor2,cpl2,_) -> - if constructor2 <> constructor1 - then raise NotUnifiable - else - let eqs' = - try ((List.combine cpl1 cpl2)@eqs) - with _ -> anomaly "eq_cases_pattern_aux" - in - eq_cases_pattern_aux eqs' - | _ -> raise NotUnifiable - -let eq_cases_pattern pat1 pat2 = - try - eq_cases_pattern_aux [pat1,pat2]; - true - with NotUnifiable -> false - - - -let ids_of_pat = - let rec ids_of_pat ids = function - | PatVar(_,Anonymous) -> ids - | PatVar(_,Name id) -> Idset.add id ids - | PatCstr(_,_,patl,_) -> List.fold_left ids_of_pat ids patl - in - ids_of_pat Idset.empty - -let id_of_name = function - | Names.Anonymous -> id_of_string "x" - | Names.Name x -> x - -(* TODO: finish Rec caes *) -let ids_of_rawterm c = - let rec ids_of_rawterm acc c = - let idof = id_of_name in - match c with - | GVar (_,id) -> id::acc - | GApp (loc,g,args) -> - ids_of_rawterm [] g @ List.flatten (List.map (ids_of_rawterm []) args) @ acc - | GLambda (loc,na,k,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc - | GProd (loc,na,k,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc - | GLetIn (loc,na,b,c) -> idof na :: ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc - | GCast (loc,c,CastConv(k,t)) -> ids_of_rawterm [] c @ ids_of_rawterm [] t @ acc - | GCast (loc,c,CastCoerce) -> ids_of_rawterm [] c @ acc - | GIf (loc,c,(na,po),b1,b2) -> ids_of_rawterm [] c @ ids_of_rawterm [] b1 @ ids_of_rawterm [] b2 @ acc - | GLetTuple (_,nal,(na,po),b,c) -> - List.map idof nal @ ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc - | GCases (loc,sty,rtntypopt,tml,brchl) -> - List.flatten (List.map (fun (_,idl,patl,c) -> idl @ ids_of_rawterm [] c) brchl) - | GRec _ -> failwith "Fix inside a constructor branch" - | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GDynamic _) -> [] - in - (* build the set *) - List.fold_left (fun acc x -> Idset.add x acc) Idset.empty (ids_of_rawterm [] c) - - - - - -let zeta_normalize = - let rec zeta_normalize_term rt = - match rt with - | GRef _ -> rt - | GVar _ -> rt - | GEvar _ -> rt - | GPatVar _ -> rt - | GApp(loc,rt',rtl) -> - GApp(loc, - zeta_normalize_term rt', - List.map zeta_normalize_term rtl - ) - | GLambda(loc,name,k,t,b) -> - GLambda(loc, - name, - k, - zeta_normalize_term t, - zeta_normalize_term b - ) - | GProd(loc,name,k,t,b) -> - GProd(loc, - name, - k, - zeta_normalize_term t, - zeta_normalize_term b - ) - | GLetIn(_,Name id,def,b) -> - zeta_normalize_term (replace_var_by_term id def b) - | GLetIn(loc,Anonymous,def,b) -> zeta_normalize_term b - | GLetTuple(loc,nal,(na,rto),def,b) -> - GLetTuple(loc, - nal, - (na,Option.map zeta_normalize_term rto), - zeta_normalize_term def, - zeta_normalize_term b - ) - | GCases(loc,sty,infos,el,brl) -> - GCases(loc,sty, - infos, - List.map (fun (e,x) -> (zeta_normalize_term e,x)) el, - List.map zeta_normalize_br brl - ) - | GIf(loc,b,(na,e_option),lhs,rhs) -> - GIf(loc, zeta_normalize_term b, - (na,Option.map zeta_normalize_term e_option), - zeta_normalize_term lhs, - zeta_normalize_term rhs - ) - | GRec _ -> raise (UserError("",str "Not handled GRec")) - | GSort _ -> rt - | GHole _ -> rt - | GCast(loc,b,CastConv(k,t)) -> - GCast(loc,zeta_normalize_term b,CastConv(k,zeta_normalize_term t)) - | GCast(loc,b,CastCoerce) -> - GCast(loc,zeta_normalize_term b,CastCoerce) - | GDynamic _ -> raise (UserError("",str "Not handled GDynamic")) - and zeta_normalize_br (loc,idl,patl,res) = - (loc,idl,patl,zeta_normalize_term res) - in - zeta_normalize_term - - - - -let expand_as = - - let rec add_as map pat = - match pat with - | PatVar _ -> map - | PatCstr(_,_,patl,Name id) -> - Idmap.add id (pattern_to_term pat) (List.fold_left add_as map patl) - | PatCstr(_,_,patl,_) -> List.fold_left add_as map patl - in - let rec expand_as map rt = - match rt with - | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> rt - | GVar(_,id) -> - begin - try - Idmap.find id map - with Not_found -> rt - end - | GApp(loc,f,args) -> GApp(loc,expand_as map f,List.map (expand_as map) args) - | GLambda(loc,na,k,t,b) -> GLambda(loc,na,k,expand_as map t, expand_as map b) - | GProd(loc,na,k,t,b) -> GProd(loc,na,k,expand_as map t, expand_as map b) - | GLetIn(loc,na,v,b) -> GLetIn(loc,na, expand_as map v,expand_as map b) - | GLetTuple(loc,nal,(na,po),v,b) -> - GLetTuple(loc,nal,(na,Option.map (expand_as map) po), - expand_as map v, expand_as map b) - | GIf(loc,e,(na,po),br1,br2) -> - GIf(loc,expand_as map e,(na,Option.map (expand_as map) po), - expand_as map br1, expand_as map br2) - | GRec _ -> error "Not handled GRec" - | GDynamic _ -> error "Not handled GDynamic" - | GCast(loc,b,CastConv(kind,t)) -> GCast(loc,expand_as map b,CastConv(kind,expand_as map t)) - | GCast(loc,b,CastCoerce) -> GCast(loc,expand_as map b,CastCoerce) - | GCases(loc,sty,po,el,brl) -> - GCases(loc, sty, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el, - List.map (expand_as_br map) brl) - and expand_as_br map (loc,idl,cpl,rt) = - (loc,idl,cpl, expand_as (List.fold_left add_as map cpl) rt) - in - expand_as Idmap.empty diff --git a/plugins/funind/rawtermops.mli b/plugins/funind/rawtermops.mli deleted file mode 100644 index b6c407a240..0000000000 --- a/plugins/funind/rawtermops.mli +++ /dev/null @@ -1,126 +0,0 @@ -open Glob_term - -(* Ocaml 3.06 Map.S does not handle is_empty *) -val idmap_is_empty : 'a Names.Idmap.t -> bool - - -(* [get_pattern_id pat] returns a list of all the variable appearing in [pat] *) -val get_pattern_id : cases_pattern -> Names.identifier list - -(* [pattern_to_term pat] returns a glob_constr corresponding to [pat]. - [pat] must not contain occurences of anonymous pattern -*) -val pattern_to_term : cases_pattern -> glob_constr - -(* - Some basic functions to rebuild glob_constr - In each of them the location is Util.dummy_loc -*) -val mkRRef : Libnames.global_reference -> glob_constr -val mkRVar : Names.identifier -> glob_constr -val mkRApp : glob_constr*(glob_constr list) -> glob_constr -val mkRLambda : Names.name * glob_constr * glob_constr -> glob_constr -val mkRProd : Names.name * glob_constr * glob_constr -> glob_constr -val mkRLetIn : Names.name * glob_constr * glob_constr -> glob_constr -val mkRCases : glob_constr option * tomatch_tuples * cases_clauses -> glob_constr -val mkRSort : rawsort -> glob_constr -val mkRHole : unit -> glob_constr (* we only build Evd.BinderType Anonymous holes *) -val mkRCast : glob_constr* glob_constr -> glob_constr -(* - Some basic functions to decompose glob_constrs - These are analogous to the ones constrs -*) -val glob_decompose_prod : glob_constr -> (Names.name*glob_constr) list * glob_constr -val glob_decompose_prod_or_letin : - glob_constr -> (Names.name*glob_constr option*glob_constr option) list * glob_constr -val glob_decompose_prod_n : int -> glob_constr -> (Names.name*glob_constr) list * glob_constr -val glob_decompose_prod_or_letin_n : int -> glob_constr -> - (Names.name*glob_constr option*glob_constr option) list * glob_constr -val glob_compose_prod : glob_constr -> (Names.name*glob_constr) list -> glob_constr -val glob_compose_prod_or_letin: glob_constr -> - (Names.name*glob_constr option*glob_constr option) list -> glob_constr -val glob_decompose_app : glob_constr -> glob_constr*(glob_constr list) - - -(* [glob_make_eq t1 t2] build the glob_constr corresponding to [t2 = t1] *) -val glob_make_eq : ?typ:glob_constr -> glob_constr -> glob_constr -> glob_constr -(* [glob_make_neq t1 t2] build the glob_constr corresponding to [t1 <> t2] *) -val glob_make_neq : glob_constr -> glob_constr -> glob_constr -(* [glob_make_or P1 P2] build the glob_constr corresponding to [P1 \/ P2] *) -val glob_make_or : glob_constr -> glob_constr -> glob_constr - -(* [glob_make_or_list [P1;...;Pn]] build the glob_constr corresponding - to [P1 \/ ( .... \/ Pn)] -*) -val glob_make_or_list : glob_constr list -> glob_constr - - -(* alpha_conversion functions *) - - - -(* Replace the var mapped in the glob_constr/context *) -val change_vars : Names.identifier Names.Idmap.t -> glob_constr -> glob_constr - - - -(* [alpha_pat avoid pat] rename all the variables present in [pat] s.t. - the result does not share variables with [avoid]. This function create - a fresh variable for each occurence of the anonymous pattern. - - Also returns a mapping from old variables to new ones and the concatenation of - [avoid] with the variables appearing in the result. -*) - val alpha_pat : - Names.Idmap.key list -> - Glob_term.cases_pattern -> - Glob_term.cases_pattern * Names.Idmap.key list * - Names.identifier Names.Idmap.t - -(* [alpha_rt avoid rt] alpha convert [rt] s.t. the result repects barendregt - conventions and does not share bound variables with avoid -*) -val alpha_rt : Names.identifier list -> glob_constr -> glob_constr - -(* same as alpha_rt but for case branches *) -val alpha_br : Names.identifier list -> - Util.loc * Names.identifier list * Glob_term.cases_pattern list * - Glob_term.glob_constr -> - Util.loc * Names.identifier list * Glob_term.cases_pattern list * - Glob_term.glob_constr - - -(* Reduction function *) -val replace_var_by_term : - Names.identifier -> - Glob_term.glob_constr -> Glob_term.glob_constr -> Glob_term.glob_constr - - - -(* - [is_free_in id rt] checks if [id] is a free variable in [rt] -*) -val is_free_in : Names.identifier -> glob_constr -> bool - - -val are_unifiable : cases_pattern -> cases_pattern -> bool -val eq_cases_pattern : cases_pattern -> cases_pattern -> bool - - - -(* - ids_of_pat : cases_pattern -> Idset.t - returns the set of variables appearing in a pattern -*) -val ids_of_pat : cases_pattern -> Names.Idset.t - -(* TODO: finish this function (Fix not treated) *) -val ids_of_rawterm: glob_constr -> Names.Idset.t - -(* - removing let_in construction in a rawterm -*) -val zeta_normalize : Glob_term.glob_constr -> Glob_term.glob_constr - - -val expand_as : glob_constr -> glob_constr diff --git a/plugins/funind/recdef_plugin.mllib b/plugins/funind/recdef_plugin.mllib index 31818c3992..ec1f5436ca 100644 --- a/plugins/funind/recdef_plugin.mllib +++ b/plugins/funind/recdef_plugin.mllib @@ -1,7 +1,7 @@ Indfun_common -Rawtermops +Glob_termops Recdef -Rawterm_to_relation +Glob_term_to_relation Functional_principles_proofs Functional_principles_types Invfun -- cgit v1.2.3