diff options
Diffstat (limited to 'contrib/funind/rawterm_to_relation.ml')
| -rw-r--r-- | contrib/funind/rawterm_to_relation.ml | 752 |
1 files changed, 467 insertions, 285 deletions
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml index b6f26dfd..dbf2f944 100644 --- a/contrib/funind/rawterm_to_relation.ml +++ b/contrib/funind/rawterm_to_relation.ml @@ -9,11 +9,11 @@ open Util open Rawtermops let observe strm = - if Tacinterp.get_debug () <> Tactic_debug.DebugOff && false + if do_observe () then Pp.msgnl strm else () let observennl strm = - if Tacinterp.get_debug () <> Tactic_debug.DebugOff &&false + if do_observe () then Pp.msg strm else () @@ -44,12 +44,8 @@ let compose_raw_context = (* The main part deals with building a list of raw constructor expressions from the rhs of a fixpoint equation. - - *) - - type 'a build_entry_pre_return = { context : raw_context; (* the binding context of the result *) @@ -62,7 +58,6 @@ type 'a build_entry_return = to_avoid : identifier list } - (* [combine_results combine_fun res1 res2] combine two results [res1] and [res2] w.r.t. [combine_fun]. @@ -113,8 +108,6 @@ let combine_args arg args = let ids_of_binder = function | LetIn Anonymous | Prod Anonymous | Lambda Anonymous -> [] | LetIn (Name id) | Prod (Name id) | Lambda (Name id) -> [id] -(* | LetTuple(nal,_) -> *) -(* map_succeed (function Name id -> id | _ -> failwith "ids_of_binder") nal *) let rec change_vars_in_binder mapping = function [] -> [] @@ -216,7 +209,6 @@ let combine_app f args = (* 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; } @@ -245,10 +237,9 @@ let mk_result ctxt value avoid = ; to_avoid = avoid } - - -let make_discr_match_el = - List.map (fun e -> (e,(Anonymous,None))) +(************************************************* + Some functions to deal with overlapping patterns +**************************************************) let coq_True_ref = lazy (Coqlib.gen_reference "" ["Init";"Logic"] "True") @@ -256,6 +247,25 @@ let coq_True_ref = 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,_) -> @@ -264,84 +274,28 @@ let make_discr_match_brl i = 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 rec make_pattern_eq_precond id e pat : identifier * (binder_type * Rawterm.rawconstr) list = - match pat with - | PatVar(_,Anonymous) -> assert false - | PatVar(_,Name x) -> - id,[Prod (Name x),mkRHole ();Prod Anonymous,raw_make_eq (mkRVar x) e] - | PatCstr(_,constr,patternl,_) -> - let new_id,new_patternl,patternl_eq_precond = - List.fold_right - (fun pat' (id,new_patternl,preconds) -> - match pat' with - | PatVar (_,Name id) -> (id,id::new_patternl,preconds) - | _ -> - let new_id = Nameops.lift_ident id in - let new_id',pat'_precond = - make_pattern_eq_precond new_id (mkRVar id) pat' - in - (new_id',id::new_patternl,preconds@pat'_precond) - ) - patternl - (id,[],[]) - in - 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 cst_as_term = - mkRApp(mkRRef(Libnames.ConstructRef constr), - implicit_args@(List.map mkRVar new_patternl) - ) - in - let precond' = - (Prod Anonymous, raw_make_eq cst_as_term e)::patternl_eq_precond - in - let precond'' = - List.fold_right - (fun id acc -> - (Prod (Name id),(mkRHole ()))::acc - ) - new_patternl - precond' - in - new_id,precond'' let pr_name = function | Name id -> Ppconstr.pr_id id | Anonymous -> str "_" -let make_pattern_eq_precond id e pat = - let res = make_pattern_eq_precond id e pat in - observe - (prlist_with_sep spc - (function (Prod na,t) -> - str "forall " ++ pr_name na ++ str ":" ++ pr_rawconstr t - | _ -> assert false - ) - (snd res) - ); - res - +(**********************************************************************) +(* functions used to build case expression from lettuple and if ones *) +(**********************************************************************) -let build_constructors_of_type msg ind' argl = +(* [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 _ -> @@ -366,21 +320,11 @@ let build_constructors_of_type msg ind' argl = let pat_as_term = mkRApp(mkRRef (ConstructRef(ind',i+1)),argl) in -(* Pp.msgnl (str "new constructor := " ++ Printer.pr_rawconstr pat_as_term); *) cases_pattern_of_rawconstr Anonymous pat_as_term ) ind.Declarations.mind_consnames -let find_constructors_of_raw_type msg t argl : Rawterm.cases_pattern array = - let ind,args = raw_decompose_app t in - match ind with - | RRef(_,IndRef ind') -> -(* let _,ind = Global.lookup_inductive ind' in *) - build_constructors_of_type msg ind' argl - | _ -> error msg - - - +(* [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,_ = raw_decompose_app b in match f with @@ -412,18 +356,145 @@ let rec find_type_of nb b = | _ -> raise (Invalid_argument "not a ref") -let rec build_entry_lc funnames avoid rt : rawconstr build_entry_return = -(* Pp.msgnl (str " Entering : " ++ Printer.pr_rawconstr rt); *) + + +(******************) +(* Main functions *) +(******************) + + + +let raw_push_named (na,raw_value,raw_typ) env = + match na with + | Anonymous -> env + | Name id -> + let value = Util.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(Libnames.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 rawconstr 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 : rawconstr build_entry_return = + observe (str " Entering : " ++ Printer.pr_rawconstr rt); match rt with | RRef _ | RVar _ | REvar _ | RPatVar _ | RSort _ | RHole _ -> - mk_result [] rt avoid + (* do nothing (except changing type of course) *) + mk_result [] rt avoid | RApp(_,_,_) -> let f,args = raw_decompose_app rt in let args_res : (rawconstr list) build_entry_return = - List.fold_right + List.fold_right (* create the arguments lists of constructors and combine them *) (fun arg ctxt_argsl -> - let arg_res = build_entry_lc funnames ctxt_argsl.to_avoid arg in - combine_results combine_args arg_res 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) @@ -431,6 +502,16 @@ let rec build_entry_lc funnames avoid rt : rawconstr build_entry_return = begin match f with | RVar(_,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 @@ -438,7 +519,7 @@ let rec build_entry_lc funnames avoid rt : rawconstr build_entry_return = List.map (fun arg_res -> let new_hyps = - [Prod (Name res),mkRHole (); + [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 } @@ -447,6 +528,11 @@ let rec build_entry_lc funnames avoid rt : rawconstr build_entry_return = in { result = new_result; to_avoid = new_avoid } | RVar _ | REvar _ | RPatVar _ | RHole _ | RSort _ | RRef _ -> + (* 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 = @@ -455,8 +541,12 @@ let rec build_entry_lc funnames avoid rt : rawconstr build_entry_return = {args_res with value = mkRApp(f,args_res.value)}) args_res.result } - | RApp _ -> assert false (* we have collected all the app *) + | RApp _ -> assert false (* we have collected all the app in [raw_decompose_app] *) | RLetIn(_,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 -> @@ -473,136 +563,169 @@ let rec build_entry_lc funnames avoid rt : rawconstr build_entry_return = | _ -> n,b,avoid in build_entry_lc + env funnames avoid (mkRLetIn(new_n,t,mkRApp(new_b,args))) | RCases _ | RLambda _ | RIf _ | RLetTuple _ -> - let f_res = build_entry_lc funnames args_res.to_avoid f in + (* 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 - | RDynamic _ ->error "Not handled RDynamic" + | RDynamic _ ->error "Not handled RDynamic" | RCast(_,b,_,_) -> - build_entry_lc funnames avoid (mkRApp(b,args)) + (* 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)) | RRec _ -> error "Not handled RRec" | RProd _ -> error "Cannot apply a type" - end + end (* end of the application treatement *) + | RLambda(_,n,t,b) -> - let b_res = build_entry_lc funnames avoid b in - let t_res = build_entry_lc funnames avoid t in + (* 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 | RProd(_,n,t,b) -> - let b_res = build_entry_lc funnames avoid b in - let t_res = build_entry_lc funnames avoid t in + (* 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 - | RLetIn(_,n,t,b) -> - let b_res = build_entry_lc funnames avoid b in - let t_res = build_entry_lc funnames avoid t in - combine_results (combine_letin n) t_res b_res + | RLetIn(_,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 | RCases(_,_,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 funnames make_discr el brl avoid + build_entry_lc_from_case env funnames make_discr el brl avoid | RIf(_,b,(na,e_option),lhs,rhs) -> - begin - match b with - | RCast(_,b,_,t) -> - let msg = "If construction must be used with cast" in - let case_pat = find_constructors_of_raw_type msg t [] in - assert (Array.length case_pat = 2); - let brl = - list_map_i - (fun i x -> (dummy_loc,[],[case_pat.(i)],x)) - 0 - [lhs;rhs] - in - let match_expr = - mkRCases(None,[(b,(Anonymous,None))],brl) - in -(* Pp.msgnl (str "new case := " ++ Printer.pr_rawconstr match_expr); *) - build_entry_lc funnames avoid match_expr - | _ -> - try - let ind = find_type_of 2 b in - let case_pat = build_constructors_of_type (str "") ind [] in - let brl = - list_map_i - (fun i x -> (dummy_loc,[],[case_pat.(i)],x)) - 0 - [lhs;rhs] - in - let match_expr = - mkRCases(None,[(b,(Anonymous,None))],brl) - in - (* Pp.msgnl (str "new case := " ++ Printer.pr_rawconstr match_expr); *) - build_entry_lc funnames avoid match_expr - with Invalid_argument s -> - let msg = "If construction must be used with cast : "^ s in - error msg - - end + 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_rawconstr b ++ str " in " ++ + Printer.pr_rawconstr 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_rawconstr match_expr); *) + build_entry_lc env funnames avoid match_expr | RLetTuple(_,nal,_,b,e) -> - begin - let nal_as_rawconstr = - List.map - (function - Name id -> mkRVar id + begin + let nal_as_rawconstr = + List.map + (function + Name id -> mkRVar id | Anonymous -> mkRHole () ) - nal + nal in - match b with - | RCast(_,b,_,t) -> - let case_pat = - find_constructors_of_raw_type - "LetTuple construction must be used with cast" t nal_as_rawconstr in - assert (Array.length case_pat = 1); - let br = - (dummy_loc,[],[case_pat.(0)],e) - in - let match_expr = mkRCases(None,[b,(Anonymous,None)],[br]) in - build_entry_lc funnames avoid match_expr - | _ -> - try - let ind = find_type_of 1 b in - let case_pat = - build_constructors_of_type - (str "LetTuple construction must be used with cast") ind nal_as_rawconstr in - let br = - (dummy_loc,[],[case_pat.(0)],e) - in - let match_expr = mkRCases(None,[b,(Anonymous,None)],[br]) in - build_entry_lc funnames avoid match_expr - with Invalid_argument s -> - let msg = "LetTuple construction must be used with cast : "^ s in - error msg - + 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_rawconstr b ++ str " in " ++ + Printer.pr_rawconstr rt ++ str ". try again with a cast") + in + let case_pats = build_constructors_of_type ind nal_as_rawconstr 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 | RRec _ -> error "Not handled RRec" | RCast(_,b,_,_) -> - build_entry_lc funnames avoid b + build_entry_lc env funnames avoid b | RDynamic _ -> error "Not handled RDynamic" -and build_entry_lc_from_case funname make_discr +and build_entry_lc_from_case env funname make_discr (el:tomatch_tuple) (brl:Rawterm.cases_clauses) avoid : rawconstr build_entry_return = match el with - | [] -> assert false (* matched on Nothing !*) + | [] -> assert false (* this case correspond to match <nothing> 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 funname avoid case_arg in + 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 + (****** The next works only if the match is not dependent ****) + 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 let results = List.map - (build_entry_lc_from_case_term funname (make_discr (List.map fst el)) [] brl case_resl.to_avoid) + (build_entry_lc_from_case_term + env types + funname (make_discr (* (List.map fst el) *)) + [] brl + case_resl.to_avoid) case_resl.result in { @@ -611,36 +734,54 @@ and build_entry_lc_from_case funname make_discr List.fold_left (fun acc r -> list_union acc r.to_avoid) [] results } -and build_entry_lc_from_case_term funname make_discr patterns_to_prevent brl avoid +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 -(* let e_ctxt,el = (matched_expr.context,matched_expr.value) in *) -(* if (List.length patl) <> (List.length el) *) -(* then error ("Pattern matching on product: not yet implemented"); *) + let 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 -> rawconstr -> rawconstr) list = - List.map - (fun pat -> + 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 - List.fold_right - (fun id acc -> mkRProd (Name id,mkRHole (),acc)) + 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 (raw_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) @@ -648,48 +789,63 @@ and build_entry_lc_from_case_term funname make_discr patterns_to_prevent brl avo avoid matched_expr in + (* We know 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.flatten ( - List.map2 - (fun pat e -> + 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),mkRHole ())::acc + 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,raw_make_eq pat_as_term e)] + [(Prod Anonymous,raw_make_eq ~typ pat_as_term e)] ) patl matched_expr.value + types + ) ) -) @ - (if List.exists (function (unifl,neql) -> - let (unif,eqs) = - 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 - [(Prod Anonymous,make_discr i )] - else - [] - ) + (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 - let return_res = build_entry_lc funname new_avoid return 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@ -(* ids@ *) - those_pattern_preconds@res.context ; + { context = matched_expr.context@those_pattern_preconds@res.context ; value = res.value} ) return_res.result @@ -702,7 +858,9 @@ let is_res id = String.sub (string_of_id id) 0 3 = "res" with Invalid_argument _ -> false -(* rebuild the raw constructors expression. +(* + The second phase which reconstruct the real type of the constructor. + rebuild the raw constructors expression. eliminates some meaningless equalities, applies some rewrites...... *) let rec rebuild_cons nb_args relname args crossed_types depth rt = @@ -722,6 +880,10 @@ let rec rebuild_cons nb_args relname args crossed_types depth rt = args new_crossed_types (depth + 1) b in + (*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 mkRProd(n,new_t,new_b), @@ -730,7 +892,7 @@ let rec rebuild_cons nb_args relname args crossed_types depth rt = assert false end | RApp(_,RRef(_,eq_as_ref),[_;RVar(_,id);rt]) - when eq_as_ref = Lazy.force Coqlib.coq_eq_ref + when eq_as_ref = Lazy.force Coqlib.coq_eq_ref && n = Anonymous -> let is_in_b = is_free_in id b in let _keep_eq = @@ -748,9 +910,11 @@ let rec rebuild_cons nb_args relname args crossed_types depth rt = (depth + 1) subst_b in mkRProd(n,t,new_b),id_to_exclude -(* if keep_eq then *) -(* mkRProd(n,t,new_b),id_to_exclude *) -(* else new_b, Idset.add id id_to_exclude *) + (* 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 + *) | _ -> let new_b,id_to_exclude = rebuild_cons @@ -766,18 +930,8 @@ let rec rebuild_cons nb_args relname args crossed_types depth rt = end | RLambda(_,n,t,b) -> begin -(* let not_free_in_t id = not (is_free_in id t) in *) -(* let new_crossed_types = t :: crossed_types in *) -(* let new_b,id_to_exclude = rebuild_cons relname args new_crossed_types b in *) -(* match n with *) -(* | Name id when Idset.mem id id_to_exclude -> *) -(* new_b, *) -(* Idset.remove id (Idset.filter not_free_in_t id_to_exclude) *) -(* | _ -> *) -(* RProd(dummy_loc,n,t,new_b),Idset.filter not_free_in_t id_to_exclude *) let not_free_in_t id = not (is_free_in id t) in let new_crossed_types = t :: crossed_types in -(* let new_b,id_to_exclude = rebuild_cons relname (args new_crossed_types b in *) match n with | Name id -> let new_b,id_to_exclude = @@ -838,15 +992,24 @@ let rec rebuild_cons nb_args relname args crossed_types depth rt = | _ -> mkRApp(mkRVar relname,args@[rt]),Idset.empty +(* debuging wrapper *) let rebuild_cons nb_args relname args crossed_types rt = - observennl (str "rebuild_cons : rt := "++ pr_rawconstr rt ++ - str "nb_args := " ++ str (string_of_int nb_args)); +(* observennl (str "rebuild_cons : rt := "++ pr_rawconstr rt ++ *) +(* str "nb_args := " ++ str (string_of_int nb_args)); *) let res = rebuild_cons nb_args relname args crossed_types 0 rt in - observe (str " leads to "++ pr_rawconstr (fst res)); +(* observe (str " leads to "++ pr_rawconstr (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 | RRef _ | RVar _ | REvar _ | RPatVar _ -> params | RApp(_,RVar(_,relname'),rtl) when Idset.mem relname' relnames -> @@ -900,13 +1063,6 @@ let compute_params_name relnames (args : (Names.name * Rawterm.rawconstr * bool) in List.rev !l -(* (Topconstr.CProdN - (dummy_loc, - [[(dummy_loc,Anonymous)],returned_types.(i)], - Topconstr.CSort(dummy_loc, RProp Null ) - ) - ) -*) let rec rebuild_return_type rt = match rt with | Topconstr.CProdN(loc,n,t') -> @@ -915,36 +1071,58 @@ let rec rebuild_return_type rt = 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, RProp Null)) + | _ -> Topconstr.CArrow(dummy_loc,rt,Topconstr.CSort(dummy_loc,RType None)) -let build_inductive parametrize funnames (funsargs: (Names.name * rawconstr * bool) list list) returned_types (rtl:rawconstr list) = +let build_inductive + parametrize funnames (funsargs: (Names.name * rawconstr * bool) list list) + returned_types + (rtl:rawconstr list) = let _time1 = System.get_time () in (* Pp.msgnl (prlist_with_sep fnl Printer.pr_rawconstr 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 -> (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 - let resa = Array.map (build_entry_lc funnames_as_set []) rta 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 (Tacinterp.constr_of_id env id)) env + ) + funnames + (Global.env ()) + in + let resa = Array.map (build_entry_lc env funnames_as_set []) rta in + (* and of the real constructors*) let constr i res = List.map (function result (* (args',concl') *) -> let rt = compose_raw_context result.context result.value in let nb_args = List.length funsargs.(i) in -(* Pp.msgnl (str "raw constr " ++ pr_rawconstr rt); *) +(* let old_implicit_args = Impargs.is_implicit_args () *) +(* and old_strict_implicit_args = Impargs.is_strict_implicit_args () *) +(* and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in *) +(* let old_rawprint = !Options.raw_print in *) +(* Options.raw_print := true; *) +(* Impargs.make_implicit_args false; *) +(* Impargs.make_strict_implicit_args false; *) +(* Impargs.make_contextual_implicit_args false; *) +(* Pp.msgnl (str "raw constr " ++ pr_rawconstr rt); *) +(* Impargs.make_implicit_args old_implicit_args; *) +(* Impargs.make_strict_implicit_args old_strict_implicit_args; *) +(* Impargs.make_contextual_implicit_args old_contextual_implicit_args; *) +(* Options.raw_print := old_rawprint; *) fst ( rebuild_cons nb_args relnames.(i) -(* (List.map *) -(* (function *) -(* (Anonymous,_,_) -> mkRVar(fresh_id res.to_avoid "x__") *) -(* | Name id, _,_ -> mkRVar id *) -(* ) *) -(* funsargs.(i) *) -(* ) *) [] [] rt @@ -952,15 +1130,21 @@ let build_inductive parametrize funnames (funsargs: (Names.name * rawconstr * bo ) res.result in - let next_constructor_id = ref (-1) 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*rawconstr) 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 = if parametrize then @@ -968,12 +1152,12 @@ let build_inductive parametrize funnames (funsargs: (Names.name * rawconstr * bo else [] in let nrel_params = List.length rels_params in - let rel_constructors = + 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 = + let rel_arity i funargs = (* Reduilding arities (with parameters) *) let rel_first_args :(Names.name * Rawterm.rawconstr * bool ) list = (snd (list_chop nrel_params funargs)) in @@ -992,13 +1176,11 @@ let build_inductive parametrize funnames (funsargs: (Names.name * rawconstr * bo ) rel_first_args (rebuild_return_type returned_types.(i)) -(* (Topconstr.CProdN *) -(* (dummy_loc, *) -(* [[(dummy_loc,Anonymous)],returned_types.(i)], *) -(* Topconstr.CSort(dummy_loc, RProp Null ) *) -(* ) *) -(* ) *) 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 old_rawprint = !Options.raw_print in Options.raw_print := true; @@ -1017,9 +1199,9 @@ let build_inductive parametrize funnames (funsargs: (Names.name * rawconstr * bo let ext_rels_constructors = Array.map (List.map (fun (id,t) -> - false,((dummy_loc,id),Constrextern.extern_rawtype Idset.empty t) + false,((dummy_loc,id),Constrextern.extern_rawtype Idset.empty ((* zeta_normalize *) t)) )) - rel_constructors + (rel_constructors) in let rel_ind i ext_rel_constructors = (dummy_loc,relnames.(i)), @@ -1030,26 +1212,26 @@ let build_inductive parametrize funnames (funsargs: (Names.name * rawconstr * bo in let ext_rel_constructors = (Array.mapi rel_ind ext_rels_constructors) in let rel_inds = Array.to_list ext_rel_constructors in - let _ = - 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 () ++ - 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 _ = *) +(* 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 old_implicit_args = Impargs.is_implicit_args () and old_strict_implicit_args = Impargs.is_strict_implicit_args () and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in |