diff options
Diffstat (limited to 'contrib/funind')
| -rw-r--r-- | contrib/funind/indfun.ml | 32 | ||||
| -rw-r--r-- | contrib/funind/new_arg_principle.ml | 476 | ||||
| -rw-r--r-- | contrib/funind/rawterm_to_relation.ml | 180 | ||||
| -rw-r--r-- | contrib/funind/rawtermops.ml | 22 |
4 files changed, 401 insertions, 309 deletions
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml index d7c045a60..065eb1730 100644 --- a/contrib/funind/indfun.ml +++ b/contrib/funind/indfun.ml @@ -78,24 +78,28 @@ let compute_annot (name,annot,args,types,body) = | Some r -> (name,r,args,types,body) - let rec is_rec names = let names = List.fold_right Idset.add names Idset.empty in - let check_id id = Idset.mem id names in - let rec lookup = function - | RVar(_,id) -> check_id id + let check_id id names = Idset.mem id names in + let rec lookup names = function + | RVar(_,id) -> check_id id names | RRef _ | REvar _ | RPatVar _ | RSort _ | RHole _ | RDynamic _ -> false - | RCast(_,b,_,_) -> lookup b + | RCast(_,b,_,_) -> lookup names b | RRec _ -> assert false - | RIf _ -> failwith "Rif not implemented" - | RLetIn(_,_,t,b) | RLambda(_,_,t,b) | RProd(_,_,t,b) | RLetTuple(_,_,_,t,b) -> - lookup t || lookup b - | RApp(_,f,args) -> List.exists lookup (f::args) + | RIf(_,b,_,lhs,rhs) -> + (lookup names b) || (lookup names lhs) || (lookup names rhs) + | RLetIn(_,na,t,b) | RLambda(_,na,t,b) | RProd(_,na,t,b) -> + lookup names t || lookup (Nameops.name_fold Idset.remove na names) b + | RLetTuple(_,_,_,t,b) -> error "RLetTuple not handled" + | RApp(_,f,args) -> List.exists (lookup names) (f::args) | RCases(_,_,el,brl) -> - List.exists (fun (e,_) -> lookup e) el || - List.exists (fun (_,_,_,ret)-> lookup ret) brl + List.exists (fun (e,_) -> lookup names e) el || + List.exists (lookup_br names) brl + and lookup_br names (_,idl,_,rt) = + let new_names = List.fold_right Idset.remove idl names in + lookup new_names rt in - lookup + lookup names let prepare_body (name,annot,args,types,body) rt = let n = (Topconstr.local_binders_length args) in @@ -326,7 +330,7 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl = if is_one_rec recdef && List.length names > 1 then Util.user_err_loc (Util.dummy_loc,"GenFixpoint", - Pp.str "the recursive argument needs to be specified") + Pp.str "the recursive argument needs to be specified in GenFixpoint") else (name,(Some 0, Topconstr.CStructRec),args,types,body),(None:Vernacexpr.decl_notation) | (_,Some (Wf _),_,_,_),_ | (_,Some (Mes _),_,_,_),_-> @@ -367,8 +371,6 @@ let make_graph (id:identifier) = | Some b -> let env = Global.env () in let body = (force b) in - - let extern_body,extern_type = let old_implicit_args = Impargs.is_implicit_args () and old_strict_implicit_args = Impargs.is_strict_implicit_args () diff --git a/contrib/funind/new_arg_principle.ml b/contrib/funind/new_arg_principle.ml index 8ef23c482..12a43b5db 100644 --- a/contrib/funind/new_arg_principle.ml +++ b/contrib/funind/new_arg_principle.ml @@ -39,7 +39,7 @@ let do_observe_tac s tac g = with e -> let goal = begin try (Printer.pr_goal (sig_it g)) with _ -> assert false end in msgnl (str "observation "++str s++str " raised exception " ++ - Cerrors.explain_exn e ++ str "on goal " ++ goal ); + Cerrors.explain_exn e ++ str " on goal " ++ goal ); raise e;; @@ -51,7 +51,7 @@ let observe_tac s tac g = let tclTRYD tac = if !Options.debug || do_observe () - then (fun g -> try do_observe_tac "" tac g with _ -> tclIDTAC g) + then (fun g -> try (* do_observe_tac "" *)tac g with _ -> tclIDTAC g) else tac @@ -71,7 +71,8 @@ type static_fix_info = { idx : int; name : identifier; - types : types + types : types; + nb_realargs : int } type static_infos = @@ -393,61 +394,6 @@ let h_reduce_with_zeta = with Rawterm.rDelta = false; }) -(* -let rewrite_until_var arg_num : tactic = - let constr_eq = Lazy.force eq in - let replace_if_unify arg (pat,cl,id,lhs) : tactic = - fun g -> - try - let (evd,matched) = - Unification.w_unify_to_subterm - (pf_env g) ~mod_delta:false (pat,arg) cl.Clenv.env - in - let cl' = {cl with Clenv.env = evd } in - let c2 = Clenv.clenv_nf_meta cl' lhs in - (Equality.replace matched c2) g - with _ -> tclFAIL 0 (str "") g - in - let rewrite_on_step equalities : tactic = - fun g -> - match kind_of_term (pf_concl g) with - | App(_,args) when (not (test_var args arg_num)) -> -(* tclFIRST (List.map (fun a -> observe_tac (str "replace_if_unify") (replace_if_unify args.(arg_num) a)) equalities) g *) - tclFIRST (List.map (replace_if_unify args.(arg_num)) equalities) g - | _ -> - raise (Util.UserError("", (str "No more rewrite" ++ - pr_lconstr_env (pf_env g) (pf_concl g)))) - in - fun g -> - let equalities = - List.filter - ( - fun (_,_,id_t) -> - match kind_of_term id_t with - | App(f,_) -> eq_constr f constr_eq - | _ -> false - ) - (pf_hyps g) - in - let f (id,_,ctype) = - let c = mkVar id in - let eqclause = Clenv.make_clenv_binding g (c,ctype) Rawterm.NoBindings in - let clause_type = Clenv.clenv_type eqclause in - let f,args = decompose_app (clause_type) in - let rec split_last_two = function - | [c1;c2] -> (c1, c2) - | x::y::z -> - split_last_two (y::z) - | _ -> - error ("The term provided is not an equivalence") - in - let (c1,c2) = split_last_two args in - (c2,eqclause,id,c1) - in - let matching_hyps = List.map f equalities in - tclTRY (tclREPEAT (tclPROGRESS (rewrite_on_step matching_hyps))) g - -*) let rewrite_until_var arg_num eq_ids : tactic = @@ -700,6 +646,57 @@ let treat_new_case static_infos nb_prod continue_tac term dyn_infos = ] g + +let instanciate_hyps_with_args (do_prove:identifier list -> tactic) hyps args_id = + let args = Array.of_list (List.map mkVar args_id) in + let instanciate_one_hyp hid = + tclORELSE + ( (* we instanciate the hyp if possible *) + fun g -> + let prov_hid = pf_get_new_id hid g in + tclTHENLIST[ + forward None (Genarg.IntroIdentifier prov_hid) (mkApp(mkVar hid,args)); + thin [hid]; + h_rename prov_hid hid + ] g + ) + ( (* + if not then we are in a mutual function block + and this hyp is a recursive hyp on an other function. + + We are not supposed to use it while proving this + principle so that we can trash it + + *) + (fun g -> + observe (str "Instanciation: removing hyp " ++ Ppconstr.pr_id hid); + thin [hid] g + ) + ) + in + if args_id = [] + then + tclTHENLIST [ + tclMAP (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) hyps; + do_prove hyps + ] + else + tclTHENLIST + [ + tclMAP (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) hyps; + tclMAP instanciate_one_hyp hyps; + (fun g -> + let all_g_hyps_id = + List.fold_right Idset.add (pf_ids_of_hyps g) Idset.empty + in + let remaining_hyps = + List.filter (fun id -> Idset.mem id all_g_hyps_id) hyps + in + do_prove remaining_hyps g + ) + ] + + let do_prove_princ_for_struct (interactive_proof:bool) (fnames:constant list) @@ -754,7 +751,15 @@ let do_prove_princ_for_struct (mkApp(dyn_infos.info,[|mkVar id|])) in let new_infos = {dyn_infos with info = new_term} in - do_prove_princ_for_struct do_finalize new_infos g' + let do_prove new_hyps = + do_prove_princ_for_struct do_finalize + {new_infos with + rec_hyps = new_hyps; + nb_rec_hyps = List.length new_hyps + } + in + observe_tac "Lambda" (instanciate_hyps_with_args do_prove new_infos.rec_hyps [id]) g' + (* do_prove_princ_for_struct do_finalize new_infos g' *) ) g | _ -> do_finalize dyn_infos g @@ -767,7 +772,8 @@ let do_prove_princ_for_struct let f,args = decompose_app dyn_infos.info in begin match kind_of_term f with - | Var _ | Construct _ | Rel _ | Evar _ | Meta _ | Ind _ -> + | App _ -> assert false (* we have collected all the app in decompose_app *) + | Var _ | Construct _ | Rel _ | Evar _ | Meta _ | Ind _ | Sort _ | Prod _ -> let new_infos = { dyn_infos with info = (f,args) @@ -780,15 +786,39 @@ let do_prove_princ_for_struct info = (f,args) } in +(* Pp.msgnl (str "proving in " ++ pr_lconstr_env (pf_env g) dyn_infos.info); *) do_prove_princ_for_struct_args do_finalize new_infos g | Const _ -> do_finalize dyn_infos g - | _ -> -(* observe *) -(* (str "Applied binders not yet implemented: in "++ fnl () ++ *) -(* pr_lconstr_env (pf_env g) term ++ fnl () ++ *) -(* pr_lconstr_env (pf_env g) f ++ spc () ++ str "is applied") ; *) - tclFAIL 0 (str "TODO : Applied binders not yet implemented") g + | Lambda _ -> + let new_term = Reductionops.nf_beta dyn_infos.info in + do_prove_princ_for_struct do_finalize {dyn_infos with info = new_term} + g + | LetIn _ -> + let new_infos = + { dyn_infos with info = nf_betaoiotazeta dyn_infos.info } + in + + tclTHENLIST + [tclMAP + (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) + dyn_infos.rec_hyps; + h_reduce_with_zeta Tacticals.onConcl; + do_prove_princ_for_struct do_finalize new_infos + ] + g + | Cast(b,_,_) -> + do_prove_princ_for_struct do_finalize {dyn_infos with info = b } g + | Case _ | Fix _ | CoFix _ -> + let new_finalize dyn_infos = + let new_infos = + { dyn_infos with + info = dyn_infos.info,args + } + in + do_prove_princ_for_struct_args do_finalize new_infos + in + do_prove_princ_for_struct new_finalize {dyn_infos with info = f } g end | Fix _ | CoFix _ -> error ( "Anonymous local (co)fixpoints are not handled yet") @@ -808,13 +838,10 @@ let do_prove_princ_for_struct h_reduce_with_zeta Tacticals.onConcl; do_prove_princ_for_struct do_finalize new_infos ] g - | _ -> - errorlabstrm "" (str "in do_prove_princ_for_struct found : "(* ++ *) -(* pr_lconstr_env (pf_env g) term *) - ) + | Rel _ -> anomaly "Free var in goal conclusion !" and do_prove_princ_for_struct do_finalize dyn_infos g = (* observe (str "proving with "++Printer.pr_lconstr term++ str " on goal " ++ pr_gls g); *) - do_prove_princ_for_struct_aux do_finalize dyn_infos g + (do_prove_princ_for_struct_aux do_finalize dyn_infos) g and do_prove_princ_for_struct_args do_finalize dyn_infos (* f_args' args *) :tactic = fun g -> (* if Tacinterp.get_debug () <> Tactic_debug.DebugOff *) @@ -822,28 +849,34 @@ let do_prove_princ_for_struct (* pr_lconstr_env (pf_env g) f_args' *) (* ); *) let (f_args',args) = dyn_infos.info in - let tac = + let tac : tactic = + fun g -> match args with | [] -> - do_finalize {dyn_infos with info = f_args'} + do_finalize {dyn_infos with info = f_args'} g | arg::args -> + observe (str "do_prove_princ_for_struct_args with arg := "++ pr_lconstr_env (pf_env g) arg++ + fnl () ++ + pr_goal (Tacmach.sig_it g) + ); let do_finalize dyn_infos = let new_arg = dyn_infos.info in - tclTRYD - (do_prove_princ_for_struct_args - do_finalize - {dyn_infos with info = (mkApp(f_args',[|new_arg|])), args} - ) + (* tclTRYD *) + (do_prove_princ_for_struct_args + do_finalize + {dyn_infos with info = (mkApp(f_args',[|new_arg|])), args} + ) in do_prove_princ_for_struct do_finalize {dyn_infos with info = arg } + g in - tclTRYD(tac ) g - in - let do_finish_proof dyn_infos = - clean_goal_with_heq + observe_tac "do_prove_princ_for_struct_args" (tac ) g + in + let do_finish_proof dyn_infos = + (* tclTRYD *) (clean_goal_with_heq static_infos - finish_proof dyn_infos + finish_proof dyn_infos) in observe_tac "do_prove_princ_for_struct" (do_prove_princ_for_struct do_finish_proof dyn_infos) @@ -856,59 +889,6 @@ let is_pte (_,_,t) = is_pte_type t exception Not_Rec - -let instanciate_hyps_with_args (do_prove:identifier list -> tactic) hyps args_id = - let args = Array.of_list (List.map mkVar args_id) in - let instanciate_one_hyp hid = - tclORELSE - ( (* we instanciate the hyp if possible *) -(* tclTHENLIST *) -(* [h_generalize [mkApp(mkVar hid,args)]; *) -(* intro_erasing hid] *) - fun g -> - let prov_hid = pf_get_new_id hid g in - tclTHENLIST[ - forward None (Genarg.IntroIdentifier prov_hid) (mkApp(mkVar hid,args)); - thin [hid]; - h_rename prov_hid hid - ] g - ) - ( (* - if not then we are in a mutual function block - and this hyp is a recursive hyp on an other function. - - We are not supposed to use it while proving this - principle so that we can trash it - - *) - (fun g -> - observe (str "Instanciation: removing hyp " ++ Ppconstr.pr_id hid); - thin [hid] g - ) - ) - in - (* if no args then no instanciation ! *) - if args_id = [] - then - tclTHENLIST [ - tclMAP (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) hyps; - do_prove hyps - ] - else - tclTHENLIST - [ - tclMAP (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) hyps; - tclMAP instanciate_one_hyp hyps; - (fun g -> - let all_g_hyps_id = - List.fold_right Idset.add (pf_ids_of_hyps g) Idset.empty - in - let remaining_hyps = - List.filter (fun id -> Idset.mem id all_g_hyps_id) hyps - in - do_prove remaining_hyps g - ) - ] let prove_princ_for_struct interactive_proof fun_num fnames all_funs _naprams : tactic = @@ -962,6 +942,12 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _naprams : let this_fix_id = fresh_id !avoid "fix___" in avoid := this_fix_id::!avoid; (* let this_body = substl (List.rev fnames_as_constr) ca.(i) in *) + let realargs,_ = decompose_lam ca.(i) in + let n_realargs = List.length realargs - List.length params in + observe (str "n_realargs := " ++ str (string_of_int n_realargs)); + observe (str "n_fix := " ++ str (string_of_int(Array.length ca))); + observe (str "body := " ++ pr_lconstr ca.(i)); + let new_type = prod_applist typearray.(i) true_params in let new_type_args,_ = decompose_prod new_type in let nargs = List.length new_type_args in @@ -973,11 +959,13 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _naprams : in let app_pte = applist(mkVar pte_id,pte_args) in let new_type = compose_prod new_type_args app_pte in + let fix_info = { idx = idxs.(i) - offset + 1; name = this_fix_id; - types = new_type + types = new_type; + nb_realargs = n_realargs } in pte_to_fix := Idmap.add pte_id fix_info !pte_to_fix; @@ -1046,97 +1034,104 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _naprams : ptes_to_fixes [] } in - match kind_of_term (pf_concl g) with - | App(pte,pte_args) when isVar pte -> - begin - let pte = destVar pte in - try - if not (Idmap.mem pte ptes_to_fixes) then raise Not_Rec; - let nparams = List.length !params in - let args_as_constr = List.map mkVar args in - let rec_num,new_body = - let idx' = list_index pte (List.rev !predicates) - 1 in - let f = fnames.(idx') in - let body_with_params = match !fbody_with_params with Some f -> f | _ -> anomaly "" - in - let name_of_f = Name ( id_of_label (con_label f)) in - let ((rec_nums,_),(na,_,bodies)) = destFix body_with_params in - let idx'' = list_index name_of_f (Array.to_list na) - 1 in - let body = substl (List.rev (Array.to_list all_funs)) bodies.(idx'') in - let body = Reductionops.nf_beta (applist(body,(List.rev_map mkVar !params))) in - rec_nums.(idx'') - nparams ,body - in - let applied_body = - Reductionops.nf_beta - (applist(new_body,List.rev args_as_constr)) - in - let do_prove branches applied_body = - do_prove_princ_for_struct - interactive_proof - (Array.to_list fnames) - static_infos - branches - applied_body - in - let replace_and_prove = - tclTHENS - (fun g -> -(* observe (str "replacing " ++ *) -(* pr_lconstr_env (pf_env g) (array_last pte_args) ++ *) -(* str " with " ++ *) -(* pr_lconstr_env (pf_env g) applied_body ++ *) -(* str " rec_arg_num is " ++ str (string_of_int rec_num) *) -(* ); *) - (Equality.replace (array_last pte_args) applied_body) g - ) - [ - clean_goal_with_heq - static_infos do_prove - { - nb_rec_hyps = List.length branches; - rec_hyps = branches; - info = applied_body; - eq_hyps = []; - } ; - try - let id = List.nth (List.rev args_as_constr) (rec_num) in - (* observe (str "choosen var := "++ pr_lconstr id); *) - (tclTHENSEQ - [(h_simplest_case id); - Tactics.intros_reflexivity - ]) - with _ -> tclIDTAC - - ] - in - (observe_tac "doing replacement" ( replace_and_prove)) g - with Not_Rec -> - let fname = destConst (fst (decompose_app (array_last pte_args))) in - tclTHEN + let nb_intros_to_do = List.length (fst (Sign.decompose_prod_assum (pf_concl g))) in + observe (str "nb_intros_to_do " ++ str (string_of_int nb_intros_to_do)); + tclTHEN + (tclDO nb_intros_to_do intro) + (fun g -> + match kind_of_term (pf_concl g) with + | App(pte,pte_args) when isVar pte -> + begin + let pte = destVar pte in + try + if not (Idmap.mem pte ptes_to_fixes) then raise Not_Rec; + let nparams = List.length !params in + let args_as_constr = List.map mkVar args in + let other_args = fst (list_chop nb_intros_to_do (pf_ids_of_hyps g)) in + let other_args_as_constr = List.map mkVar other_args in + let rec_num,new_body = + let idx' = list_index pte (List.rev !predicates) - 1 in + let f = fnames.(idx') in + let body_with_params = match !fbody_with_params with Some f -> f | _ -> anomaly "" + in + let name_of_f = Name ( id_of_label (con_label f)) in + let ((rec_nums,_),(na,_,bodies)) = destFix body_with_params in + let idx'' = list_index name_of_f (Array.to_list na) - 1 in + let body = substl (List.rev (Array.to_list all_funs)) bodies.(idx'') in + let body = Reductionops.nf_beta (applist(body,(List.rev_map mkVar !params))) in + rec_nums.(idx'') - nparams ,body + in + let applied_body_with_real_args = + Reductionops.nf_beta + (applist(new_body,List.rev args_as_constr)) + in + let applied_body = + Reductionops.nf_beta + (applist(applied_body_with_real_args,List.rev other_args_as_constr)) + in + observe (str "applied_body_with_real_args := "++ pr_lconstr_env (pf_env g) applied_body_with_real_args); + observe (str "applied_body := "++ pr_lconstr_env (pf_env g) applied_body); + let do_prove branches applied_body = + do_prove_princ_for_struct + interactive_proof + (Array.to_list fnames) + static_infos + branches + applied_body + in + let replace_and_prove = + tclTHENS + (fun g -> (Equality.replace (array_last pte_args) applied_body) g) + [ + tclTHENLIST + [ + generalize other_args_as_constr; + thin other_args; + clean_goal_with_heq + static_infos do_prove + { + nb_rec_hyps = List.length branches; + rec_hyps = branches; + info = applied_body_with_real_args; + eq_hyps = []; + } ]; + let id = try List.nth (List.rev args_as_constr) (rec_num) with _ -> anomaly ("Cannot find recursive argument of function ! ") in + let id_as_induction_constr = Tacexpr.ElimOnConstr id in + (tclTHENSEQ + [Tactics.new_destruct [id_as_induction_constr] None Genarg.IntroAnonymous;(* (h_simplest_case id) *) + Tactics.intros_reflexivity + ]) + ] + in + (observe_tac "doing replacement" ( replace_and_prove)) g + with Not_Rec -> + let fname = destConst (fst (decompose_app (array_last pte_args))) in + tclTHEN (unfold_in_concl [([],Names.EvalConstRef fname)]) - (observe_tac "" - (fun g' -> - let body = array_last (snd (destApp (pf_concl g'))) in - let dyn_infos = - { nb_rec_hyps = List.length branches; - rec_hyps = branches; - info = body; - eq_hyps = [] - } - in - let do_prove = - do_prove_princ_for_struct + (observe_tac "" + (fun g' -> + let body = array_last (snd (destApp (pf_concl g'))) in + let dyn_infos = + { nb_rec_hyps = List.length branches; + rec_hyps = branches; + info = body; + eq_hyps = [] + } + in + let do_prove = + do_prove_princ_for_struct interactive_proof - (Array.to_list fnames) - static_infos - in - clean_goal_with_heq static_infos - do_prove dyn_infos g' - ) - ) - g - end - | _ -> assert false + (Array.to_list fnames) + static_infos + in + clean_goal_with_heq static_infos + do_prove dyn_infos g' + ) + ) + g + end + | _ -> assert false + ) g in tclTHENSEQ [ @@ -1145,21 +1140,26 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _naprams : (fun g -> observe_tac "introducing branches" (intro_with_remembrance branches princ_info.nbranches) g); (fun g -> observe_tac "declaring fix(es)" mk_fixes g); (fun g -> - let nb_prod_g = nb_prod (pf_concl g) in - tclTHENLIST [ - tclDO nb_prod_g intro; + let nb_real_args = + let pte_app = snd (Sign.decompose_prod_assum (pf_concl g)) in + let pte = fst (decompose_app pte_app) in + try + let fix_info = Idmap.find (destVar pte) !pte_to_fix in + fix_info.nb_realargs + with Not_found -> (* Not a recursive function *) + nb_prod (pf_concl g) + in + observe_tac "" (tclTHEN + (tclDO nb_real_args (observe_tac "intro" intro)) (fun g' -> - let args = - fst (list_chop ~msg:"args" nb_prod_g (pf_ids_of_hyps g')) - in + let realargs_ids = fst (list_chop ~msg:"args" nb_real_args (pf_ids_of_hyps g')) in let do_prove_on_branches branches : tactic = - observe_tac "proving" (do_prove !pte_to_fix args branches) + observe_tac "proving" (do_prove !pte_to_fix ( realargs_ids) branches) in - observe_tac "instanciating rec hyps" - (instanciate_hyps_with_args do_prove_on_branches !branches (List.rev args)) - g' - ) - ] + observe_tac "instanciating rec hyps" + (instanciate_hyps_with_args do_prove_on_branches !branches (List.rev realargs_ids)) + g' + )) g ) ] diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml index 327198b91..1234c7faa 100644 --- a/contrib/funind/rawterm_to_relation.ml +++ b/contrib/funind/rawterm_to_relation.ml @@ -145,37 +145,6 @@ let rec replace_var_by_term_in_binder x_id term = function let add_bt_names bt = List.append (ids_of_binder bt) -(* let rec replace_var_by_term_in_binder x_id term = function *) -(* | [] -> [] *) -(* | (bt,Name id,t)::l when id_ord id x_id = 0 -> *) -(* (bt,Name id,replace_var_by_term x_id term t)::l *) -(* | (bt,na,t)::l -> *) -(* (bt,na,replace_var_by_term x_id term t)::(replace_var_by_term_in_binder x_id term l) *) - -(* let rec change_vars_in_binder mapping = function *) -(* | [] -> [] *) -(* | (bt,(Name id as na),t)::l when Idmap.mem id mapping -> *) -(* (bt,na,change_vars mapping t):: l *) -(* | (bt,na,t)::l -> *) -(* (bt,na,change_vars mapping t):: *) -(* (change_vars_in_binder mapping l) *) - - -(* let alpha_ctxt avoid b = *) -(* let rec alpha_ctxt = function *) -(* | [] -> [],b *) -(* | (bt,n,t)::ctxt -> *) -(* let new_ctxt,new_b = alpha_ctxt ctxt in *) -(* match n with *) -(* | Name id when List.mem id avoid -> *) -(* let new_id = Nameops.next_ident_away id avoid in *) -(* let mapping = Idmap.add id new_id Idmap.empty in *) -(* (bt,Name new_id,t):: *) -(* (change_vars_in_binder mapping new_ctxt), *) -(* change_vars mapping new_b *) -(* | _ -> (bt,n,t)::new_ctxt,new_b *) -(* in *) -(* alpha_ctxt *) let apply_args ctxt body args = let need_convert_id avoid id = List.exists (is_free_in id) args || List.mem id avoid @@ -183,11 +152,6 @@ let apply_args ctxt body args = let need_convert avoid bt = List.exists (need_convert_id avoid) (ids_of_binder bt) in -(* let add_name na avoid = *) -(* match na with *) -(* | Anonymous -> avoid *) -(* | Name id -> id::avoid *) -(* in *) let next_name_away (na:name) (mapping: identifier Idmap.t) (avoid: identifier list) = match na with | Name id when List.mem id avoid -> @@ -206,17 +170,6 @@ let apply_args ctxt body args = | Lambda na -> let new_na,mapping,new_avoid = next_name_away na Idmap.empty avoid in Lambda new_na,mapping,new_avoid -(* | LetTuple (nal,na) -> *) -(* let rev_new_nal,mapping,new_avoid = *) -(* List.fold_left *) -(* (fun (nal,mapping,(avoid:identifier list)) na -> *) -(* let new_na,new_mapping,new_avoid = next_name_away na mapping avoid in *) -(* (new_na::nal,new_mapping,new_avoid) *) -(* ) *) -(* ([],Idmap.empty,avoid) *) -(* nal *) -(* in *) -(* (LetTuple(List.rev rev_new_nal,na),mapping,new_avoid) *) in let rec do_apply avoid ctxt body args = match ctxt,args with @@ -402,6 +355,73 @@ let make_pattern_eq_precond id e pat = res +let build_constructors_of_type msg ind' = + 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 pat_as_term = + mkRApp(mkRRef (ConstructRef(ind',i+1)), + Array.to_list + (Array.init (cst_narg - npar) (fun _ -> mkRHole ()) + ) + ) + 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 = + 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' + | _ -> error msg + + + +let rec find_type_of b = + let f,_ = raw_decompose_app b in + match f with + | RRef(_,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 = 2 ) + then raise (Invalid_argument "find_type_of : not an if inductive"); + ind_type + end + | RCast(_,b,_,_) -> find_type_of b + | RApp _ -> assert false (* we have decomposed any application via raw_decompose_app *) + | _ -> 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); *) match rt with @@ -466,13 +486,13 @@ let rec build_entry_lc funnames avoid rt : rawconstr build_entry_return = funnames avoid (mkRLetIn(new_n,t,mkRApp(new_b,args))) - | RCases _ | RLambda _ -> + | RCases _ | RLambda _ | RIf _ -> let f_res = build_entry_lc funnames args_res.to_avoid f in combine_results combine_app f_res args_res | RDynamic _ ->error "Not handled RDynamic" - | RCast _ -> error "Not handled RCast" + | RCast(_,b,_,_) -> + build_entry_lc funnames avoid (mkRApp(b,args)) | RRec _ -> error "Not handled RRec" - | RIf _ -> error "Not handled RIf" | RLetTuple _ -> error "Not handled RLetTuple" | RProd _ -> error "Cannot apply a type" end @@ -496,10 +516,49 @@ let rec build_entry_lc funnames avoid rt : rawconstr build_entry_return = | RCases(_,_,el,brl) -> let make_discr = make_discr_match brl in build_entry_lc_from_case funnames make_discr el brl avoid - | RIf _ -> error "Not handled RIf" + | 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 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 + | RLetTuple _ -> error "Not handled RLetTuple" | RRec _ -> error "Not handled RRec" - | RCast _ -> error "Not handled RCast" + | RCast(_,b,_,_) -> + build_entry_lc funnames avoid b | RDynamic _ -> error "Not handled RDynamic" and build_entry_lc_from_case funname make_discr (el:(Rawterm.rawconstr * @@ -839,6 +898,7 @@ let rec rebuild_return_type rt = 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 @@ -975,14 +1035,25 @@ let build_inductive parametrize funnames (funsargs: (Names.name * rawconstr * bo Impargs.make_implicit_args false; Impargs.make_strict_implicit_args false; Impargs.make_contextual_implicit_args false; + let _time2 = System.get_time () in +(* Pp.msgnl (str "Bulding Inductive : " ++ str (string_of_float (System.time_difference time1 time2))); *) try Options.silently (Command.build_mutual rel_inds) true; + let _time3 = System.get_time () in +(* Pp.msgnl (str "Bulding Done: "++ str (string_of_float (System.time_difference time2 time3))); *) +(* let msg = *) +(* str "while trying to define"++ spc () ++ *) +(* Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,rel_inds)) ++ fnl () *) +(* in *) +(* Pp.msgnl msg; *) 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; with - | UserError(s,msg) -> + | UserError(s,msg) -> + let _time3 = System.get_time () in +(* Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *) 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; @@ -996,6 +1067,8 @@ let build_inductive parametrize funnames (funsargs: (Names.name * rawconstr * bo raise (UserError(s, msg)) | e -> + let _time3 = System.get_time () in +(* Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *) 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; @@ -1010,3 +1083,4 @@ let build_inductive parametrize funnames (funsargs: (Names.name * rawconstr * bo (UserError("",msg)) + diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml index 99bf2bf1d..cd09fb5f2 100644 --- a/contrib/funind/rawtermops.ml +++ b/contrib/funind/rawtermops.ml @@ -123,7 +123,13 @@ let change_vars = List.map (fun (e,x) -> (change_vars mapping e,x)) el, List.map (change_vars_br mapping) brl ) - | RIf _ -> error "Not handled RIf" + | RIf(loc,b,(na,e_option),lhs,rhs) -> + RIf(loc, + change_vars mapping b, + (na,option_app (change_vars mapping) e_option), + change_vars mapping lhs, + change_vars mapping rhs + ) | RRec _ -> error "Not handled RRec" | RSort _ -> rt | RHole _ -> rt @@ -297,7 +303,12 @@ let rec alpha_rt excluded rt = List.map (function (rt,i) -> alpha_rt excluded rt, i) el in RCases(loc,infos,new_el,List.map (alpha_br excluded) brl) - | RIf _ -> error "Not handled RIf" + | RIf(loc,b,(na,e_o),lhs,rhs) -> + RIf(loc,alpha_rt excluded b, + (na,option_app (alpha_rt excluded) e_o), + alpha_rt excluded lhs, + alpha_rt excluded rhs + ) | RRec _ -> error "Not handled RRec" | RSort _ -> rt | RHole _ -> rt @@ -449,7 +460,12 @@ let replace_var_by_term x_id term = List.map (fun (e,x) -> (replace_var_by_pattern e,x)) el, List.map replace_var_by_pattern_br brl ) - | RIf _ -> raise (UserError("",str "Not handled RIf")) + | RIf(loc,b,(na,e_option),lhs,rhs) -> + RIf(loc, replace_var_by_pattern b, + (na,option_app replace_var_by_pattern e_option), + replace_var_by_pattern lhs, + replace_var_by_pattern rhs + ) | RRec _ -> raise (UserError("",str "Not handled RRec")) | RSort _ -> rt | RHole _ -> rt |