diff options
Diffstat (limited to 'plugins/subtac/subtac_command.ml')
| -rw-r--r-- | plugins/subtac/subtac_command.ml | 132 |
1 files changed, 66 insertions, 66 deletions
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml index 1095b143c..d1e890867 100644 --- a/plugins/subtac/subtac_command.ml +++ b/plugins/subtac/subtac_command.ml @@ -55,11 +55,11 @@ let evar_nf isevars c = let get_undefined_evars evd = Evd.fold (fun ev evi evd' -> - if evi.evar_body = Evar_empty then + if evi.evar_body = Evar_empty then Evd.add evd' ev (nf_evar_info evd evi) else evd') evd Evd.empty -let interp_gen kind isevars env +let interp_gen kind isevars env ?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[])) c = let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars ( !isevars) env c in @@ -67,16 +67,16 @@ let interp_gen kind isevars env evar_nf isevars c' let interp_constr isevars env c = - interp_gen (OfType None) isevars env c + interp_gen (OfType None) isevars env c let interp_type_evars isevars env ?(impls=([],[])) c = interp_gen IsType isevars env ~impls c let interp_casted_constr isevars env ?(impls=([],[])) c typ = - interp_gen (OfType (Some typ)) isevars env ~impls c + interp_gen (OfType (Some typ)) isevars env ~impls c let interp_casted_constr_evars isevars env ?(impls=([],[])) c typ = - interp_gen (OfType (Some typ)) isevars env ~impls c + interp_gen (OfType (Some typ)) isevars env ~impls c let interp_open_constr isevars env c = msgnl (str "Pretyping " ++ my_print_constr_expr c); @@ -85,17 +85,17 @@ let interp_open_constr isevars env c = evar_nf isevars c' let interp_constr_judgment isevars env c = - let j = + let j = SPretyping.understand_judgment_tcc isevars env - (Constrintern.intern_constr ( !isevars) env c) + (Constrintern.intern_constr ( !isevars) env c) in { uj_val = evar_nf isevars j.uj_val; uj_type = evar_nf isevars j.uj_type } let locate_if_isevar loc na = function - | RHole _ -> + | RHole _ -> (try match na with | Name id -> Reserve.find_reserved_type id - | Anonymous -> raise Not_found + | Anonymous -> raise Not_found with Not_found -> RHole (loc, Evd.BinderType na)) | x -> x @@ -103,7 +103,7 @@ let interp_binder sigma env na t = let t = Constrintern.intern_gen true ( !sigma) env t in SPretyping.understand_tcc_evars sigma env IsType (locate_if_isevar (loc_of_rawconstr t) na t) -let interp_context_evars evdref env params = +let interp_context_evars evdref env params = let bl = Constrintern.intern_context false ( !evdref) env params in let (env, par, _, impls) = List.fold_left @@ -113,7 +113,7 @@ let interp_context_evars evdref env params = let t' = locate_if_isevar (loc_of_rawconstr t) na t in let t = SPretyping.understand_tcc_evars evdref env IsType t' in let d = (na,None,t) in - let impls = + let impls = if k = Implicit then let na = match na with Name n -> Some n | Anonymous -> None in (ExplByPos (n, na), (true, true, true)) :: impls @@ -134,39 +134,39 @@ let list_chop_hd i l = match list_chop i l with | (x :: [], l2) -> ([], x, []) | _ -> assert(false) -let collect_non_rec env = - let rec searchrec lnonrec lnamerec ldefrec larrec nrec = +let collect_non_rec env = + let rec searchrec lnonrec lnamerec ldefrec larrec nrec = try - let i = + let i = list_try_find_i (fun i f -> if List.for_all (fun (_, def) -> not (occur_var env f def)) ldefrec then i else failwith "try_find_i") - 0 lnamerec + 0 lnamerec in let (lf1,f,lf2) = list_chop_hd i lnamerec in let (ldef1,def,ldef2) = list_chop_hd i ldefrec in let (lar1,ar,lar2) = list_chop_hd i larrec in - let newlnv = - try - match list_chop i nrec with + let newlnv = + try + match list_chop i nrec with | (lnv1,_::lnv2) -> (lnv1@lnv2) | _ -> [] (* nrec=[] for cofixpoints *) with Failure "list_chop" -> [] - in - searchrec ((f,def,ar)::lnonrec) + in + searchrec ((f,def,ar)::lnonrec) (lf1@lf2) (ldef1@ldef2) (lar1@lar2) newlnv - with Failure "try_find_i" -> + with Failure "try_find_i" -> (List.rev lnonrec, (Array.of_list lnamerec, Array.of_list ldefrec, Array.of_list larrec, Array.of_list nrec)) - in - searchrec [] + in + searchrec [] -let list_of_local_binders l = +let list_of_local_binders l = let rec aux acc = function Topconstr.LocalRawDef (n, c) :: tl -> aux ((n, Some c, None) :: acc) tl - | Topconstr.LocalRawAssum (nl, k, c) :: tl -> + | Topconstr.LocalRawAssum (nl, k, c) :: tl -> aux (List.fold_left (fun acc n -> (n, None, Some c) :: acc) acc nl) tl | [] -> List.rev acc in aux [] l @@ -201,7 +201,7 @@ let telescope = function | (n, None, t) :: tl -> let ty, tys, (k, constr) = List.fold_left - (fun (ty, tys, (k, constr)) (n, b, t) -> + (fun (ty, tys, (k, constr)) (n, b, t) -> let pred = mkLambda (n, t, ty) in let sigty = mkApp ((Lazy.force sigT).typ, [|t; pred|]) in let intro = mkApp ((Lazy.force sigT).intro, [|lift k t; lift k pred; mkRel k; constr|]) in @@ -215,14 +215,14 @@ let telescope = function (lift 1 proj2, (n, Some proj1, t) :: subst)) (List.rev tys) tl (mkRel 1, []) in ty, ((n, Some last, t) :: subst), constr - + | _ -> raise (Invalid_argument "telescope") let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed = Coqlib.check_required_library ["Coq";"Program";"Wf"]; let sigma = Evd.empty in let isevars = ref (Evd.create_evar_defs sigma) in - let env = Global.env() in + let env = Global.env() in let _pr c = my_print_constr env c in let _prr = Printer.pr_rel_context env in let _prn = Printer.pr_named_context env in @@ -235,8 +235,8 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed = let argtyp, letbinders, make = telescope binders_rel in let argname = id_of_string "recarg" in let arg = (Name argname, None, argtyp) in - let wrapper x = - if List.length binders_rel > 1 then + let wrapper x = + if List.length binders_rel > 1 then it_mkLambda_or_LetIn (mkApp (x, [|make|])) binders_rel else x in @@ -244,12 +244,12 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed = let binders_env = push_rel_context binders_rel env in let rel = interp_constr isevars env r in let relty = type_of env !isevars rel in - let relargty = + let relargty = let ctx, ar = Reductionops.splay_prod_n env !isevars 2 relty in match ctx, kind_of_term ar with - | [(_, None, t); (_, None, u)], Sort (Prop Null) + | [(_, None, t); (_, None, u)], Sort (Prop Null) when Reductionops.is_conv env !isevars t u -> t - | _, _ -> + | _, _ -> user_err_loc (constr_loc r, "Subtac_command.build_wellfounded", my_print_constr env rel ++ str " is not an homogeneous binary relation.") @@ -261,7 +261,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed = it_mkLambda_or_LetIn measure binders in let comb = constr_of_global (Lazy.force measure_on_R_ref) in - let wf_rel = mkApp (comb, [| argtyp; relargty; rel; measure |]) in + let wf_rel = mkApp (comb, [| argtyp; relargty; rel; measure |]) in let wf_rel_fun x y = mkApp (rel, [| subst1 x measure_body; subst1 y measure_body |]) @@ -280,13 +280,13 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed = let projection = (* in wfarg :: arg :: before *) mkApp (proj, [| argtyp ; wfargpred ; mkRel 1 |]) in - let top_arity_let = it_mkLambda_or_LetIn top_arity letbinders in + let top_arity_let = it_mkLambda_or_LetIn top_arity letbinders in let intern_arity = substl [projection] top_arity_let in (* substitute the projection of wfarg for something, now intern_arity is in wfarg :: arg *) let intern_fun_arity_prod = it_mkProd_or_LetIn intern_arity [wfarg 1] in let intern_fun_binder = (Name (add_suffix recname "'"), None, intern_fun_arity_prod) in - let curry_fun = + let curry_fun = let wfpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel (2 * len + 4))) in let arg = mkApp ((Lazy.force sig_).intro, [| argtyp; wfpred; lift 1 make; mkRel 1 |]) in let app = mkApp (mkRel (2 * len + 2 (* recproof + orig binders + current binders *)), [| arg |]) in @@ -298,22 +298,22 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed = in let fun_bl = intern_fun_binder :: [arg] in let lift_lets = Termops.lift_rel_context 1 letbinders in - let intern_body = + let intern_body = let ctx = (Name recname, None, pi3 curry_fun) :: binders_rel in let impls = Command.compute_interning_datas env Constrintern.Recursive [] [recname] [full_arity] [impls] in - let newimpls = + let newimpls = match snd impls with [(p, (r, l, impls, scopes))] -> [(p, (r, l, impls @ [Some (id_of_string "recproof", Impargs.Manual, (true, false))], scopes @ [None]))] | x -> x - in interp_casted_constr isevars ~impls:(fst impls,newimpls) + in interp_casted_constr isevars ~impls:(fst impls,newimpls) (push_rel_context ctx env) body (lift 1 top_arity) in let intern_body_lam = it_mkLambda_or_LetIn intern_body (curry_fun :: lift_lets @ fun_bl) in let prop = mkLambda (Name argname, argtyp, top_arity_let) in let fix_def = mkApp (constr_of_global (Lazy.force fix_sub_ref), - [| argtyp ; wf_rel ; + [| argtyp ; wf_rel ; make_existential dummy_loc ~opaque:(Define false) env isevars wf_proof ; prop ; intern_body_lam |]) in @@ -328,10 +328,10 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed = let evars, evars_def, evars_typ = Eterm.eterm_obligations env recname !isevars evm 0 fullcoqc fullctyp in Subtac_obligations.add_definition recname evars_def evars_typ ~implicits:impls evars -let nf_evar_context isevars ctx = - List.map (fun (n, b, t) -> +let nf_evar_context isevars ctx = + List.map (fun (n, b, t) -> (n, Option.map (Evarutil.nf_isevar isevars) b, Evarutil.nf_isevar isevars t)) ctx - + let interp_fix_context evdref env fix = interp_context_evars evdref env fix.Command.fix_binders @@ -350,7 +350,7 @@ let prepare_recursive_declaration fixnames fixtypes fixdefs = let names = List.map (fun id -> Name id) fixnames in (Array.of_list names, Array.of_list fixtypes, Array.of_list defs) -let rel_index n ctx = +let rel_index n ctx = list_index0 (Name n) (List.rev_map pi1 (List.filter (fun x -> pi2 x = None) ctx)) let rec unfold f b = @@ -359,16 +359,16 @@ let rec unfold f b = | None -> [] let compute_possible_guardness_evidences (n,_) (_, fixctx) fixtype = - match n with + match n with | Some (loc, n) -> [rel_index n fixctx] - | None -> + | None -> (* If recursive argument was not given by user, we try all args. An earlier approach was to look only for inductive arguments, - but doing it properly involves delta-reduction, and it finally - doesn't seem to worth the effort (except for huge mutual + but doing it properly involves delta-reduction, and it finally + doesn't seem to worth the effort (except for huge mutual fixpoints ?) *) let len = List.length fixctx in - unfold (function x when x = len -> None + unfold (function x when x = len -> None | n -> Some (n, succ n)) 0 let push_named_context = List.fold_right push_named @@ -402,11 +402,11 @@ let interp_recursive fixkind l boxed = let fixctxs, fiximps = List.split (List.map (interp_fix_context evdref env) fixl) in let fixccls = List.map2 (interp_fix_ccl evdref) fixctxs fixl in let fixtypes = List.map2 build_fix_type fixctxs fixccls in - let rec_sign = + let rec_sign = List.fold_left2 (fun env' id t -> let sort = Retyping.get_type_of env !evdref t in - let fixprot = - try mkApp (Lazy.force Subtac_utils.fix_proto, [|sort; t|]) + let fixprot = + try mkApp (Lazy.force Subtac_utils.fix_proto, [|sort; t|]) with e -> t in (id,None,fixprot) :: env') @@ -419,8 +419,8 @@ let interp_recursive fixkind l boxed = let notations = List.fold_right Option.List.cons ntnl [] in (* Interp bodies with rollback because temp use of notations/implicit *) - let fixdefs = - States.with_state_protection (fun () -> + let fixdefs = + States.with_state_protection (fun () -> List.iter (Command.declare_interning_data impls) notations; list_map3 (interp_fix_body evdref env_rec impls) fixctxs fixl fixccls) () in @@ -434,7 +434,7 @@ let interp_recursive fixkind l boxed = let fixdefs = List.map (nf_evar evd) fixdefs in let fixtypes = List.map (nf_evar evd) fixtypes in let rec_sign = nf_named_context_evar evd rec_sign in - + let recdefs = List.length rec_sign in List.iter (check_evars env_rec Evd.empty evd) fixdefs; List.iter (check_evars env Evd.empty evd) fixtypes; @@ -446,9 +446,9 @@ let interp_recursive fixkind l boxed = let isevars = Evd.undefined_evars evd in let evm = isevars in (* Solve remaining evars *) - let rec collect_evars id def typ imps = + let rec collect_evars id def typ imps = (* Generalize by the recursive prototypes *) - let def = + let def = Termops.it_mkNamedLambda_or_LetIn def rec_sign and typ = Termops.it_mkNamedProd_or_LetIn typ rec_sign @@ -457,14 +457,14 @@ let interp_recursive fixkind l boxed = let evm' = Subtac_utils.evars_of_term evm evm' typ in let evars, def, typ = Eterm.eterm_obligations env id isevars evm' recdefs def typ in (id, def, typ, imps, evars) - in + in let defs = list_map4 collect_evars fixnames fixdefs fixtypes fiximps in (match fixkind with | Command.IsFixpoint wfl -> let possible_indexes = list_map3 compute_possible_guardness_evidences wfl fixctxs fixtypes in - let fixdecls = Array.of_list (List.map (fun x -> Name x) fixnames), - Array.of_list fixtypes, + let fixdecls = Array.of_list (List.map (fun x -> Name x) fixnames), + Array.of_list fixtypes, Array.of_list (List.map (subst_vars (List.rev fixnames)) fixdefs) in let indexes = Pretyping.search_guard dummy_loc (Global.env ()) possible_indexes fixdecls in @@ -480,8 +480,8 @@ let build_recursive l b = let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in match g, l with [(n, CWfRec r)], [(((_,id),_,bl,typ,def),ntn)] -> - ignore(build_wellfounded (id, n, bl, typ, def) r - (match n with Some n -> mkIdentC (snd n) | None -> + ignore(build_wellfounded (id, n, bl, typ, def) r + (match n with Some n -> mkIdentC (snd n) | None -> errorlabstrm "Subtac_command.build_recursive" (str "Recursive argument required for well-founded fixpoints")) ntn false) @@ -491,15 +491,15 @@ let build_recursive l b = m ntn false) | _, _ when List.for_all (fun (n, ro) -> ro = CStructRec) g -> - let fixl = List.map (fun (((_,id),_,bl,typ,def),ntn) -> - ({Command.fix_name = id; Command.fix_binders = bl; Command.fix_body = def; Command.fix_type = typ},ntn)) l + let fixl = List.map (fun (((_,id),_,bl,typ,def),ntn) -> + ({Command.fix_name = id; Command.fix_binders = bl; Command.fix_body = def; Command.fix_type = typ},ntn)) l in interp_recursive (Command.IsFixpoint g) fixl b - | _, _ -> + | _, _ -> errorlabstrm "Subtac_command.build_recursive" (str "Well-founded fixpoints not allowed in mutually recursive blocks") let build_corecursive l b = - let fixl = List.map (fun (((_,id),bl,typ,def),ntn) -> + let fixl = List.map (fun (((_,id),bl,typ,def),ntn) -> ({Command.fix_name = id; Command.fix_binders = bl; Command.fix_body = def; Command.fix_type = typ},ntn)) l in interp_recursive Command.IsCoFixpoint fixl b |