diff options
Diffstat (limited to 'vernac/auto_ind_decl.ml')
| -rw-r--r-- | vernac/auto_ind_decl.ml | 316 |
1 files changed, 164 insertions, 152 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index cc59a96834..f600432c80 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -193,48 +193,48 @@ let build_beq_scheme mode kn = let create_input c = let myArrow u v = mkArrow u Sorts.Relevant (lift 1 v) and eqName = function - | Name s -> Id.of_string ("eq_"^(Id.to_string s)) - | Anonymous -> Id.of_string "eq_A" + | Name s -> Id.of_string ("eq_"^(Id.to_string s)) + | Anonymous -> Id.of_string "eq_A" in let ext_rel_list = Context.Rel.to_extended_list mkRel 0 lnamesparrec in - let lift_cnt = ref 0 in - let eqs_typ = List.map (fun aa -> - let a = lift !lift_cnt aa in - incr lift_cnt; - myArrow a (myArrow a (bb ())) - ) ext_rel_list in - - let eq_input = List.fold_left2 - ( fun a b decl -> (* mkLambda(n,b,a) ) *) - (* here I leave the Naming thingy so that the type of + let lift_cnt = ref 0 in + let eqs_typ = List.map (fun aa -> + let a = lift !lift_cnt aa in + incr lift_cnt; + myArrow a (myArrow a (bb ())) + ) ext_rel_list in + + let eq_input = List.fold_left2 + ( fun a b decl -> (* mkLambda(n,b,a) ) *) + (* here I leave the Naming thingy so that the type of the function is more readable for the user *) - mkNamedLambda (map_annot eqName (RelDecl.get_annot decl)) b a ) - c (List.rev eqs_typ) lnamesparrec - in - List.fold_left (fun a decl ->(* mkLambda(n,t,a)) eq_input rel_list *) - (* Same here , hoping the auto renaming will do something good ;) *) - let x = map_annot - (function Name s -> s | Anonymous -> Id.of_string "A") - (RelDecl.get_annot decl) - in - mkNamedLambda x (RelDecl.get_type decl) a) eq_input lnamesparrec - in - let make_one_eq cur = - let u = Univ.Instance.empty in - let ind = (kn,cur),u (* FIXME *) in - (* current inductive we are working on *) - let cur_packet = mib.mind_packets.(snd (fst ind)) in - (* Inductive toto : [rettyp] := *) - let rettyp = Inductive.type_of_inductive ((mib,cur_packet),u) in - (* split rettyp in a list without the non rec params and the last -> + mkNamedLambda (map_annot eqName (RelDecl.get_annot decl)) b a ) + c (List.rev eqs_typ) lnamesparrec + in + List.fold_left (fun a decl ->(* mkLambda(n,t,a)) eq_input rel_list *) + (* Same here , hoping the auto renaming will do something good ;) *) + let x = map_annot + (function Name s -> s | Anonymous -> Id.of_string "A") + (RelDecl.get_annot decl) + in + mkNamedLambda x (RelDecl.get_type decl) a) eq_input lnamesparrec + in + let make_one_eq cur = + let u = Univ.Instance.empty in + let ind = (kn,cur),u (* FIXME *) in + (* current inductive we are working on *) + let cur_packet = mib.mind_packets.(snd (fst ind)) in + (* Inductive toto : [rettyp] := *) + let rettyp = Inductive.type_of_inductive ((mib,cur_packet),u) in + (* split rettyp in a list without the non rec params and the last -> e.g. Inductive vec (A:Set) : nat -> Set := ... will do [nat] *) - let rettyp_l = quick_chop nparrec (deconstruct_type rettyp) in + let rettyp_l = quick_chop nparrec (deconstruct_type rettyp) in (* give a type A, this function tries to find the equality on A declared previously *) (* nlist = the number of args (A , B , ... ) eqA = the de Bruijn index of the first eq param ndx = how much to translate due to the 2nd Case - *) + *) let compute_A_equality rel_list nlist eqA ndx t = let lifti = ndx in let rec aux c = @@ -243,47 +243,47 @@ let build_beq_scheme mode kn = match Constr.kind c with | Rel x -> mkRel (x-nlist+ndx) | Var x -> - (* Support for working in a context with "eq_x : x -> x -> bool" *) - let eid = Id.of_string ("eq_"^(Id.to_string x)) in - let () = - try ignore (Environ.lookup_named eid env) - with Not_found -> raise (ParameterWithoutEquality (GlobRef.VarRef x)) - in - mkVar eid + (* Support for working in a context with "eq_x : x -> x -> bool" *) + let eid = Id.of_string ("eq_"^(Id.to_string x)) in + let () = + try ignore (Environ.lookup_named eid env) + with Not_found -> raise (ParameterWithoutEquality (GlobRef.VarRef x)) + in + mkVar eid | Cast (x,_,_) -> aux (Term.applist (x,a)) | App _ -> assert false | Ind ((kn',i as ind'),u) (*FIXME: universes *) -> - if Environ.QMutInd.equal env kn kn' then mkRel(eqA-nlist-i+nb_ind-1) - else begin - try - let eq = match lookup_scheme (!beq_scheme_kind_aux()) ind' with - | Some c -> mkConst c - | None -> assert false - in - let eqa = Array.of_list @@ List.map aux a in - let args = - Array.append - (Array.of_list (List.map (fun x -> lift lifti x) a)) eqa in - if Int.equal (Array.length args) 0 then eq - else mkApp (eq, args) - with Not_found -> raise(EqNotFound (ind', fst ind)) - end + if Environ.QMutInd.equal env kn kn' then mkRel(eqA-nlist-i+nb_ind-1) + else begin + try + let eq = match lookup_scheme (!beq_scheme_kind_aux()) ind' with + | Some c -> mkConst c + | None -> assert false + in + let eqa = Array.of_list @@ List.map aux a in + let args = + Array.append + (Array.of_list (List.map (fun x -> lift lifti x) a)) eqa in + if Int.equal (Array.length args) 0 then eq + else mkApp (eq, args) + with Not_found -> raise(EqNotFound (ind', fst ind)) + end | Sort _ -> raise InductiveWithSort | Prod _ -> raise InductiveWithProduct | Lambda _-> raise (EqUnknown "abstraction") | LetIn _ -> raise (EqUnknown "let-in") | Const (kn, u) -> - (match Environ.constant_opt_value_in env (kn, u) with - | Some c -> aux (Term.applist (c,a)) - | None -> - (* Support for working in a context with "eq_x : x -> x -> bool" *) - (* Needs Hints, see test suite *) - let eq_lbl = Label.make ("eq_" ^ Label.to_string (Constant.label kn)) in - let kneq = Constant.change_label kn eq_lbl in - if Environ.mem_constant kneq env then - let _ = Environ.constant_opt_value_in env (kneq, u) in - Term.applist (mkConst kneq,a) - else raise (ParameterWithoutEquality (GlobRef.ConstRef kn))) + (match Environ.constant_opt_value_in env (kn, u) with + | Some c -> aux (Term.applist (c,a)) + | None -> + (* Support for working in a context with "eq_x : x -> x -> bool" *) + (* Needs Hints, see test suite *) + let eq_lbl = Label.make ("eq_" ^ Label.to_string (Constant.label kn)) in + let kneq = Constant.change_label kn eq_lbl in + if Environ.mem_constant kneq env then + let _ = Environ.constant_opt_value_in env (kneq, u) in + Term.applist (mkConst kneq,a) + else raise (ParameterWithoutEquality (GlobRef.ConstRef kn))) | Proj _ -> raise (EqUnknown "projection") | Construct _ -> raise (EqUnknown "constructor") | Case _ -> raise (EqUnknown "match") @@ -293,100 +293,112 @@ let build_beq_scheme mode kn = | Evar _ -> raise (EqUnknown "existential variable") | Int _ -> raise (EqUnknown "int") | Float _ -> raise (EqUnknown "float") - | Array _ -> raise (EqUnknown "array") - in + | Array _ -> raise (EqUnknown "array") + in aux t - in - (* construct the predicate for the Case part*) - let do_predicate rel_list n = - List.fold_left (fun a b -> mkLambda(make_annot Anonymous Sorts.Relevant,b,a)) - (mkLambda (make_annot Anonymous Sorts.Relevant, - mkFullInd ind (n+3+(List.length rettyp_l)+nb_ind-1), - (bb ()))) - (List.rev rettyp_l) in - (* make_one_eq *) - (* do the [| C1 ... => match Y with ... end + in + (* construct the predicate for the Case part*) + let do_predicate rel_list n = + List.fold_left (fun a b -> mkLambda(make_annot Anonymous Sorts.Relevant,b,a)) + (mkLambda (make_annot Anonymous Sorts.Relevant, + mkFullInd ind (n+3+(List.length rettyp_l)+nb_ind-1), + (bb ()))) + (List.rev rettyp_l) in + (* make_one_eq *) + (* do the [| C1 ... => match Y with ... end ... Cn => match Y with ... end |] part *) let rci = Sorts.Relevant in (* TODO relevance *) let ci = make_case_info env (fst ind) rci MatchStyle in - let constrs n = get_constructors env (make_ind_family (ind, - Context.Rel.to_extended_list mkRel (n+nb_ind-1) mib.mind_params_ctxt)) in + let constrs n = + let params = Context.Rel.to_extended_list mkRel (n+nb_ind-1) mib.mind_params_ctxt in + get_constructors env (make_ind_family (ind, params)) + in let constrsi = constrs (3+nparrec) in let n = Array.length constrsi in - let ar = Array.make n (ff ()) in - for i=0 to n-1 do - let nb_cstr_args = List.length constrsi.(i).cs_args in - let ar2 = Array.make n (ff ()) in - let constrsj = constrs (3+nparrec+nb_cstr_args) in - for j=0 to n-1 do - if Int.equal i j then - ar2.(j) <- let cc = (match nb_cstr_args with - | 0 -> tt () - | _ -> let eqs = Array.make nb_cstr_args (tt ()) in - for ndx = 0 to nb_cstr_args-1 do - let cc = RelDecl.get_type (List.nth constrsi.(i).cs_args ndx) in - let eqA = compute_A_equality rel_list - nparrec - (nparrec+3+2*nb_cstr_args) - (nb_cstr_args+ndx+1) - cc - in - Array.set eqs ndx - (mkApp (eqA, - [|mkRel (ndx+1+nb_cstr_args);mkRel (ndx+1)|] - )) - done; - Array.fold_left - (fun a b -> mkApp (andb(),[|b;a|])) - (eqs.(0)) - (Array.sub eqs 1 (nb_cstr_args - 1)) - ) - in - (List.fold_left (fun a decl -> mkLambda (RelDecl.get_annot decl, RelDecl.get_type decl, a)) cc - (constrsj.(j).cs_args) - ) - else ar2.(j) <- (List.fold_left (fun a decl -> - mkLambda (RelDecl.get_annot decl, RelDecl.get_type decl, a)) (ff ()) (constrsj.(j).cs_args) ) - done; - - ar.(i) <- (List.fold_left (fun a decl -> mkLambda (RelDecl.get_annot decl, RelDecl.get_type decl, a)) - (mkCase (Inductive.contract_case env ((ci,do_predicate rel_list nb_cstr_args, - NoInvert, mkVar (Id.of_string "Y") ,ar2)))) - (constrsi.(i).cs_args)) - done; - mkNamedLambda (make_annot (Id.of_string "X") Sorts.Relevant) (mkFullInd ind (nb_ind-1+1)) ( - mkNamedLambda (make_annot (Id.of_string "Y") Sorts.Relevant) (mkFullInd ind (nb_ind-1+2)) ( - mkCase (Inductive.contract_case env (ci, do_predicate rel_list 0,NoInvert,mkVar (Id.of_string "X"),ar)))) - in (* build_beq_scheme *) - let names = Array.make nb_ind (make_annot Anonymous Sorts.Relevant) and - types = Array.make nb_ind mkSet and - cores = Array.make nb_ind mkSet in - let u = Univ.Instance.empty in - for i=0 to (nb_ind-1) do - names.(i) <- make_annot (Name (Id.of_string (rec_name i))) Sorts.Relevant; - types.(i) <- mkArrow (mkFullInd ((kn,i),u) 0) Sorts.Relevant - (mkArrow (mkFullInd ((kn,i),u) 1) Sorts.Relevant (bb ())); - let c = make_one_eq i in - cores.(i) <- c; - done; - (Array.init nb_ind (fun i -> - let kelim = Inductive.elim_sort (mib,mib.mind_packets.(i)) in - if not (Sorts.family_leq InSet kelim) then - raise (NonSingletonProp (kn,i)); - let fix = match mib.mind_finite with - | CoFinite -> - raise NoDecidabilityCoInductive; - | Finite -> - mkFix (((Array.make nb_ind 0),i),(names,types,cores)) - | BiFinite -> - (* If the inductive type is not recursive, the fixpoint is + let ar = Array.init n (fun i -> + let nb_cstr_args = List.length constrsi.(i).cs_args in + let constrsj = constrs (3+nparrec+nb_cstr_args) in + let ar2 = Array.init n (fun j -> + if Int.equal i j then + let cc = match nb_cstr_args with + | 0 -> tt () + | _ -> + let eqs = Array.init nb_cstr_args (fun ndx -> + let cc = RelDecl.get_type (List.nth constrsi.(i).cs_args ndx) in + let eqA = compute_A_equality rel_list + nparrec + (nparrec+3+2*nb_cstr_args) + (nb_cstr_args+ndx+1) + cc + in + mkApp (eqA, [|mkRel (ndx+1+nb_cstr_args);mkRel (ndx+1)|])) + in + Array.fold_left + (fun a b -> mkApp (andb(),[|b;a|])) + eqs.(0) + (Array.sub eqs 1 (nb_cstr_args - 1)) + in + List.fold_left (fun a decl -> + mkLambda (RelDecl.get_annot decl, RelDecl.get_type decl, a)) + cc + constrsj.(j).cs_args + else + List.fold_left (fun a decl -> + mkLambda (RelDecl.get_annot decl, RelDecl.get_type decl, a)) + (ff ()) + (constrsj.(j).cs_args)) + in + let pred = EConstr.of_constr (do_predicate rel_list nb_cstr_args) in + let case = + simple_make_case_or_project env (Evd.from_env env) + ci pred NoInvert (EConstr.mkVar (Id.of_string "Y")) + (EConstr.of_constr_array ar2) + in + List.fold_left (fun a decl -> mkLambda (RelDecl.get_annot decl, RelDecl.get_type decl, a)) + (EConstr.Unsafe.to_constr case) + (constrsi.(i).cs_args)) + in + let pred = EConstr.of_constr (do_predicate rel_list 0) in + let case = + simple_make_case_or_project env (Evd.from_env env) + ci pred NoInvert (EConstr.mkVar (Id.of_string "X")) + (EConstr.of_constr_array ar) + in + mkNamedLambda (make_annot (Id.of_string "X") Sorts.Relevant) (mkFullInd ind (nb_ind-1+1)) ( + mkNamedLambda (make_annot (Id.of_string "Y") Sorts.Relevant) (mkFullInd ind (nb_ind-1+2)) ( + (EConstr.Unsafe.to_constr case))) + in (* build_beq_scheme *) + + let names = Array.make nb_ind (make_annot Anonymous Sorts.Relevant) and + types = Array.make nb_ind mkSet and + cores = Array.make nb_ind mkSet in + let u = Univ.Instance.empty in + for i=0 to (nb_ind-1) do + names.(i) <- make_annot (Name (Id.of_string (rec_name i))) Sorts.Relevant; + types.(i) <- mkArrow (mkFullInd ((kn,i),u) 0) Sorts.Relevant + (mkArrow (mkFullInd ((kn,i),u) 1) Sorts.Relevant (bb ())); + let c = make_one_eq i in + cores.(i) <- c; + done; + let res = Array.init nb_ind (fun i -> + let kelim = Inductive.elim_sort (mib,mib.mind_packets.(i)) in + if not (Sorts.family_leq InSet kelim) then + raise (NonSingletonProp (kn,i)); + let fix = match mib.mind_finite with + | CoFinite -> + raise NoDecidabilityCoInductive; + | Finite -> + mkFix (((Array.make nb_ind 0),i),(names,types,cores)) + | BiFinite -> + (* If the inductive type is not recursive, the fixpoint is not used, so let's replace it with garbage *) - let subst = List.init nb_ind (fun _ -> mkProp) in - Vars.substl subst cores.(i) - in - create_input fix), - UState.from_env (Global.env ())) + let subst = List.init nb_ind (fun _ -> mkProp) in + Vars.substl subst cores.(i) + in + create_input fix) + in + res, UState.from_env (Global.env ()) let beq_scheme_kind = declare_mutual_scheme_object "_beq" |