diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-05-03 09:54:17 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-05-03 09:54:17 +0000 |
| commit | bf352b0b29a8e3d55eaa986c4f493af48f8ddf52 (patch) | |
| tree | b0633f3a1ee73bd685327c2c988426d65de7a58a | |
| parent | c4a517927f148e0162d22cb7077fa0676d799926 (diff) | |
Changement de la structure des points fixes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1731 85f007b7-540e-0410-9357-904b9bb8a0f7
41 files changed, 579 insertions, 546 deletions
diff --git a/contrib/extraction/Extraction.v b/contrib/extraction/Extraction.v index e909d4511..b8d295aef 100644 --- a/contrib/extraction/Extraction.v +++ b/contrib/extraction/Extraction.v @@ -30,7 +30,7 @@ with mindnames : ast := mlconstr [ idorstring($id) "[" idorstring_list($idl) "]" ] -> [(VERNACARGLIST $id ($LIST $idl))] -with idorstring_list: List := +with idorstring_list: ast list := ids_nil [ ] -> [ ] | ids_cons [ idorstring($x) idorstring_list($l) ] -> [ $x ($LIST $l) ] diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml index 807c7d448..f08e69161 100644 --- a/contrib/extraction/extract_env.ml +++ b/contrib/extraction/extract_env.ml @@ -65,7 +65,7 @@ and visit_ast eenv a = | MLcons (r,l) -> visit_reference eenv r; List.iter visit l | MLcase (a,br) -> visit a; Array.iter (fun (r,_,a) -> visit_reference eenv r; visit a) br - | MLfix (_,_,l) -> List.iter visit l + | MLfix (_,_,l) -> Array.iter visit l | MLcast (a,t) -> visit a; visit_type eenv t | MLmagic a -> visit a | MLrel _ | MLprop | MLarity | MLexn _ -> () diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index 99dce2f00..f559857e9 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -525,10 +525,10 @@ and extract_term_info_with_type env ctx c t = abstract_n n (abstract [] 1 s) | IsMutCase ((ni,(ip,cnames,_,_,_)),p,c,br) -> extract_case env ctx ni ip cnames p c br - | IsFix ((_,i),(ti,fi,ci)) -> - extract_fix env ctx i ti fi ci - | IsCoFix (i,(ti,fi,ci)) -> - extract_fix env ctx i ti fi ci + | IsFix ((_,i),recd) -> + extract_fix env ctx i recd + | IsCoFix (i,recd) -> + extract_fix env ctx i recd | IsLetIn (n, c1, t1, c2) -> let id = id_of_name n in let env' = push_rel_def (n,c1,t1) env in @@ -591,11 +591,13 @@ and extract_case env ctx ni ip cnames p c br = assert (Array.length br = 1); snd (extract_branch_aux 0 br.(0))) -and extract_fix env ctx i ti fi ci = +and extract_fix env ctx i (fi,ti,ci as recd) = let n = Array.length ti in + let env' = push_rec_types recd env in let ti' = Array.mapi lift ti in - let lb = (List.combine fi (Array.to_list ti')) in - let env' = push_rels_assum (List.rev lb) env in + let lb = + Array.to_list + (array_map2_i (fun i na t -> (na, type_app (lift i) t)) fi ti) in let ctx' = lbinders_fold (fun _ _ v a -> (snd v = NotArity) :: a) ctx env lb in let extract_fix_body c t = @@ -603,8 +605,8 @@ and extract_fix env ctx i ti fi ci = | Emltype _ -> MLarity | Emlterm a -> a in - let ei = Array.to_list (array_map2 extract_fix_body ci ti) in - MLfix (i, List.map id_of_name fi, ei) + let ei = array_map2 extract_fix_body ci ti in + MLfix (i, Array.map id_of_name fi, ei) and extract_app env ctx (f,tyf,sf) args = let nargs = List.length args in diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli index 565932596..c2ed8e7a9 100644 --- a/contrib/extraction/miniml.mli +++ b/contrib/extraction/miniml.mli @@ -39,7 +39,7 @@ type ml_ast = | MLglob of global_reference | MLcons of global_reference * ml_ast list | MLcase of ml_ast * (global_reference * identifier list * ml_ast) array - | MLfix of int * identifier list * ml_ast list + | MLfix of int * identifier array * ml_ast array | MLexn of identifier | MLprop | MLarity diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml index 0bd5ec3a6..fafdcdd01 100644 --- a/contrib/extraction/mlutil.ml +++ b/contrib/extraction/mlutil.ml @@ -46,11 +46,13 @@ let rec occurs k = function (occurs k t) || (array_exists (fun (_,l,t') -> let k' = List.length l in occurs (k + k') t') pv) - | MLfix(_,l,cl) -> let k' = List.length l in occurs_list (k + k') cl + | MLfix(_,l,cl) -> let k' = Array.length l in occurs_vect (k + k') cl | _ -> false and occurs_list k l = List.exists (occurs k) l +and occurs_vect k v = array_exists (occurs k) v + (*s map over ML asts *) let rec ast_map f = function @@ -59,7 +61,7 @@ let rec ast_map f = function | MLletin (id,a,b) -> MLletin (id, f a, f b) | MLcons (c,al) -> MLcons (c, List.map f al) | MLcase (a,eqv) -> MLcase (f a, Array.map (ast_map_eqn f) eqv) - | MLfix (fi,ids,al) -> MLfix (fi, ids, List.map f al) + | MLfix (fi,ids,al) -> MLfix (fi, ids, Array.map f al) | MLcast (a,t) -> MLcast (f a, t) | MLmagic a -> MLmagic (f a) | MLrel _ | MLglob _ | MLexn _ | MLprop | MLarity as a -> a @@ -84,7 +86,7 @@ let ml_liftn k n c = (id, idl, liftrec (n+k) p)) pl) | MLfix (n0,idl,pl) -> MLfix (n0,idl, - let k = List.length idl in List.map (liftrec (n+k)) pl) + let k = Array.length idl in Array.map (liftrec (n+k)) pl) | a -> ast_map (liftrec n) a in if k = 0 then c else liftrec n c @@ -115,10 +117,10 @@ let rec ml_subst v = (id,ids,subst (n+k) (ml_lift k m) t)) pv) | MLfix (i,ids,cl) -> MLfix (i,ids, - let k = List.length ids in - List.map (subst (n+k) (ml_lift k m)) cl) - | a -> - ast_map (subst n m) a + let k = Array.length ids in + Array.map (subst (n+k) (ml_lift k m)) cl) + | a -> + ast_map (subst n m) a in subst 1 v @@ -145,7 +147,7 @@ let nb_occur a = count n t; Array.iter (fun (_,l,t) -> let k = List.length l in count (n + k) t) pv | MLfix (_,ids,cl) -> - let k = List.length ids in List.iter (count (n + k)) cl + let k = Array.length ids in Array.iter (count (n + k)) cl | MLapp (a,l) -> count n a; List.iter (count n) l | MLcons (_,l) -> List.iter (count n) l | MLmagic a -> count n a @@ -238,7 +240,7 @@ let rec ml_size = function | MLcons(_,l) -> ml_size_list l | MLcase(t,pv) -> 1 + ml_size t + (Array.fold_right (fun (_,_,t) a -> a + ml_size t) pv 0) - | MLfix(_,_,f) -> ml_size_list f + | MLfix(_,_,f) -> ml_size_array f | MLletin (_,_,t) -> ml_size t | MLcast (t,_) -> ml_size t | MLmagic t -> ml_size t @@ -246,6 +248,8 @@ let rec ml_size = function and ml_size_list l = List.fold_left (fun a t -> a + ml_size t) 0 l +and ml_size_array l = Array.fold_left (fun a t -> a + ml_size t) 0 l + let is_fix = function MLfix _ -> true | _ -> false let rec is_constr = function @@ -296,9 +300,9 @@ let rec non_stricts add cand = function let cand = non_stricts false cand t1 in pop 1 (non_stricts add (lift 1 cand) t2) | MLfix (_,i,f)-> - let n = List.length i in + let n = Array.length i in let cand = lift n cand in - let cand = List.fold_left (non_stricts false) cand f in + let cand = Array.fold_left (non_stricts false) cand f in pop n cand | MLcase (t,v) -> (* The only interesting case: for a variable to be non-strict, diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml index 0945b79cb..2fdc8c8ac 100644 --- a/contrib/extraction/ocaml.ml +++ b/contrib/extraction/ocaml.ml @@ -218,8 +218,8 @@ let rec pp_expr par env args = 'fNL; 'sTR " "; pp_pat env pv >]; if args <> [] then [< 'sTR ")" >] else close_par par >] | MLfix (i,ids,defs) -> - let ids',env' = push_vars (List.rev ids) env in - pp_fix par env' (Some i) (List.rev ids',defs) args + let ids',env' = push_vars (List.rev (Array.to_list ids)) env in + pp_fix par env' (Some i) (Array.of_list (List.rev ids'),defs) args | MLexn id -> [< open_par par; 'sTR "failwith"; 'sPC; 'qS (string_of_id id); close_par par >] @@ -256,14 +256,14 @@ and pp_pat env pv = and pp_fix par env in_p (ids,bl) args = [< open_par par; v 0 [< 'sTR "let rec " ; - prlist_with_sep + prvect_with_sep (fun () -> [< 'fNL; 'sTR "and " >]) (fun (fi,ti) -> pp_function env (pr_id fi) ti) - (List.combine ids bl); + (array_map2 (fun id b -> (id,b)) ids bl); 'fNL; match in_p with | Some j -> - hOV 2 [< 'sTR "in "; pr_id (List.nth ids j); + hOV 2 [< 'sTR "in "; pr_id (ids.(j)); if args <> [] then [< 'sTR " "; prlist_with_sep (fun () -> [<'sTR " ">]) @@ -351,10 +351,10 @@ let pp_decl = function hOV 0 [< 'sTR "type"; 'sPC; pp_parameters l; pp_type_global r; 'sPC; 'sTR "="; 'sPC; pp_type false t; 'fNL >] - | Dglob (r, MLfix (_,[_],[def])) -> + | Dglob (r, MLfix (_,[|_|],[|def|])) -> let id = P.rename_global r in let env' = ([id], !current_ids) in - [< hOV 2 (pp_fix false env' None ([id],[def]) []) >] + [< hOV 2 (pp_fix false env' None ([|id|],[|def|]) []) >] | Dglob (r, a) -> hOV 0 [< 'sTR "let "; pp_function (empty_env ()) (pp_global r) a; 'fNL >] diff --git a/contrib/field/Field.v b/contrib/field/Field.v index b3261d3ea..eb82846d7 100644 --- a/contrib/field/Field.v +++ b/contrib/field/Field.v @@ -14,14 +14,14 @@ Require Export Field_Tactic. Declare ML Module "field". -Grammar vernac opt_arg_list : List := +Grammar vernac opt_arg_list : ast list := | noal [] -> [] | minus [ "minus" ":=" constrarg($aminus) opt_arg_list($l) ] -> [ "minus" $aminus ($LIST $l) ] | div [ "div" ":=" constrarg($adiv) opt_arg_list($l) ] -> [ "div" $adiv ($LIST $l) ] -with extra_args : List := +with extra_args : ast list := | nea [] -> [] | with_a [ "with" opt_arg_list($l)] -> [ ($LIST $l) ] diff --git a/contrib/interface/Centaur.v b/contrib/interface/Centaur.v index 80142df4d..f2e168645 100644 --- a/contrib/interface/Centaur.v +++ b/contrib/interface/Centaur.v @@ -34,15 +34,15 @@ Grammar vernac vernac : ast := (* | show_dad_rules [ "Show" "Dad" "Rules" "." ] -> [(Show_dad_rules)] *) | start_pcoq [ "Start" "Pcoq" "Mode" "." ] -> [ (START_PCOQ) ] | start_pcoq [ "Start" "Pcoq" "Debug" "Mode" "." ] -> [ (START_PCOQ_DEBUG) ]. -Grammar vernac ne_id_list : List := +Grammar vernac ne_id_list : ast list := id_one [ identarg($id)] -> [$id] | id_more [identarg($id) ne_id_list($others)] -> [$id ($LIST $others)]. -Grammar tactic ne_num_list : List := +Grammar tactic ne_num_list : ast list := ne_last [ numarg($n) ] -> [ $n ] | ne_num_ste [ numarg($n) ne_num_list($ns) ] -> [ $n ($LIST $ns)]. -Grammar tactic two_numarg_list : List := +Grammar tactic two_numarg_list : ast list := two_single_and_ne [ numarg($n) "to" ne_num_list($ns)] -> [$n (TACTIC (to)) ($LIST $ns)] | two_rec [ numarg($n) two_numarg_list($ns)] -> [ $n ($LIST $ns)]. diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml index e4297ce85..7908af7ec 100644 --- a/contrib/ring/quote.ml +++ b/contrib/ring/quote.ml @@ -226,7 +226,7 @@ let compute_ivs gl f cs = let cst = try destConst f with _ -> i_can't_do_that () in let body = constant_value (Global.env()) cst in match decomp_term body with - | IsFix(([| len |], 0), ([| typ |], [ name ], [| body2 |])) -> + | IsFix(([| len |], 0), ([| name |], [| typ |], [| body2 |])) -> let (args3, body3) = decompose_lam body2 in let nargs3 = List.length args3 in begin match decomp_term body3 with diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index 392782727..573f4319b 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -446,7 +446,7 @@ let print_term inner_types l env csr = ) a [<>] >] ) - | T.IsFix ((ai,i),((t,f,b) as rec_decl)) -> + | T.IsFix ((ai,i),((f,t,b) as rec_decl)) -> X.xml_nempty "FIX" (add_sort_attribute true ["noFun", (string_of_int i) ; "id",next_id]) (force @@ -458,7 +458,7 @@ let print_term inner_types l env csr = [< term_display idradix false l env ti >] ; X.xml_nempty "body" [] [< term_display idradix false - ((List.rev f)@l) + ((Array.to_list f)@l) (E.push_rec_types rec_decl env) bi >] @@ -466,11 +466,11 @@ let print_term inner_types l env csr = i >] ) - (Array.mapi (fun j x -> (x,t.(j),b.(j),ai.(j)) ) (Array.of_list f) ) + (Array.mapi (fun j x -> (x,t.(j),b.(j),ai.(j)) ) f ) [<>] >] ) - | T.IsCoFix (i,((t,f,b) as rec_decl)) -> + | T.IsCoFix (i,((f,t,b) as rec_decl)) -> X.xml_nempty "COFIX" (add_sort_attribute true ["noFun", (string_of_int i) ; "id",next_id]) (force @@ -481,7 +481,7 @@ let print_term inner_types l env csr = [< term_display idradix false l env ti >] ; X.xml_nempty "body" [] [< term_display idradix false - ((List.rev f)@l) + ((Array.to_list f)@l) (E.push_rec_types rec_decl env) bi >] @@ -489,7 +489,7 @@ let print_term inner_types l env csr = i >] ) - (Array.mapi (fun j x -> (x,t.(j),b.(j)) ) (Array.of_list f) ) [<>] + (Array.mapi (fun j x -> (x,t.(j),b.(j)) ) f ) [<>] >] ) | T.IsEvar _ -> diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 7ea96f474..e2a91022f 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -108,17 +108,17 @@ let constr_display csr = | IsMutCase (ci,p,c,bl) -> "MutCase(<abs>,"^(term_display p)^","^(term_display c)^"," ^(array_display bl)^")" - | IsFix ((t,i),(tl,lna,bl)) -> + | IsFix ((t,i),(lna,tl,bl)) -> "Fix(([|"^(Array.fold_right (fun x i -> (string_of_int x)^(if not(i="") then (";"^i) else "")) t "")^"|],"^(string_of_int i)^")," ^(array_display tl)^"," - ^(List.fold_right (fun x i -> (name_display x)^(if not(i="") + ^(Array.fold_right (fun x i -> (name_display x)^(if not(i="") then (";"^i) else "")) lna "")^"," ^(array_display bl)^")" - | IsCoFix(i,(tl,lna,bl)) -> + | IsCoFix(i,(lna,tl,bl)) -> "CoFix("^(string_of_int i)^")," ^(array_display tl)^"," - ^(List.fold_right (fun x i -> (name_display x)^(if not(i="") + ^(Array.fold_right (fun x i -> (name_display x)^(if not(i="") then (";"^i) else "")) lna "")^"," ^(array_display bl)^")" @@ -208,33 +208,33 @@ let print_pure_constr csr = print_cut(); print_string "end"; close_box() - | IsFix ((t,i),(tl,lna,bl)) -> + | IsFix ((t,i),(lna,tl,bl)) -> print_string "Fix("; print_int i; print_string ")"; print_cut(); open_vbox 0; - let rec print_fix lna k = - match lna with [] -> () - | nf::ln -> open_vbox 0; - name_display nf; print_string "/"; - print_int t.(k); print_cut(); print_string ":"; - box_display tl.(k) ; print_cut(); print_string ":="; - box_display bl.(k); close_box (); - print_cut(); - print_fix ln (k+1) - in print_string"{"; print_fix lna 0; print_string"}" - | IsCoFix(i,(tl,lna,bl)) -> + let rec print_fix () = + for k = 0 to Array.length tl do + open_vbox 0; + name_display lna.(k); print_string "/"; + print_int t.(k); print_cut(); print_string ":"; + box_display tl.(k) ; print_cut(); print_string ":="; + box_display bl.(k); close_box (); + print_cut() + done + in print_string"{"; print_fix(); print_string"}" + | IsCoFix(i,(lna,tl,bl)) -> print_string "CoFix("; print_int i; print_string ")"; print_cut(); open_vbox 0; - let rec print_fix lna k = - match lna with [] -> () - | nf::ln -> open_vbox 1; - name_display nf; print_cut(); print_string ":"; - box_display tl.(k) ; print_cut(); print_string ":="; - box_display bl.(k); close_box (); - print_cut(); - print_fix ln (k+1) - in print_string"{"; print_fix lna 0; print_string"}" + let rec print_fix () = + for k = 0 to Array.length tl do + open_vbox 1; + name_display lna.(k); print_cut(); print_string ":"; + box_display tl.(k) ; print_cut(); print_string ":="; + box_display bl.(k); close_box (); + print_cut(); + done + in print_string"{"; print_fix (); print_string"}" and box_display c = open_hovbox 1; term_display c; close_box() diff --git a/kernel/closure.ml b/kernel/closure.ml index 714a8be3d..a09368fcd 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -438,9 +438,9 @@ and fterm = | FInd of inductive_path * fconstr array | FConstruct of constructor_path * fconstr array | FApp of fconstr * fconstr array - | FFix of (int array * int) * (fconstr array * name list * fconstr array) + | FFix of (int array * int) * (name array * fconstr array * fconstr array) * constr array * fconstr subs - | FCoFix of int * (fconstr array * name list * fconstr array) + | FCoFix of int * (name array * fconstr array * fconstr array) * constr array * fconstr subs | FCases of case_info * fconstr * fconstr * fconstr array | FLambda of name * fconstr * fconstr * constr * fconstr subs @@ -535,18 +535,20 @@ let mk_clos_deep clos_fun env t = { norm = Red; term = FCases (ci, clos_fun env p, clos_fun env c, Array.map (clos_fun env) v) } - | IsFix (op,(tys,lna,bds)) -> + | IsFix (op,(lna,tys,bds)) -> let env' = subs_liftn (Array.length bds) env in { norm = Cstr; - term = FFix (op, (Array.map (clos_fun env) tys, lna, - Array.map (clos_fun env') bds), - bds, env) } - | IsCoFix (op,(tys,lna,bds)) -> + term = FFix + (op,(lna, Array.map (clos_fun env) tys, + Array.map (clos_fun env') bds), + bds, env) } + | IsCoFix (op,(lna,tys,bds)) -> let env' = subs_liftn (Array.length bds) env in { norm = Cstr; - term = FCoFix (op, (Array.map (clos_fun env) tys, lna, - Array.map (clos_fun env') bds), - bds, env) } + term = FCoFix + (op,(lna, Array.map (clos_fun env) tys, + Array.map (clos_fun env') bds), + bds, env) } | IsLambda (n,t,c) -> { norm = Cstr; @@ -590,14 +592,14 @@ let rec to_constr constr_fun lfts v = mkMutCase (ci, constr_fun lfts p, constr_fun lfts c, Array.map (constr_fun lfts) ve) - | FFix (op,(tys,lna,bds),_,_) -> + | FFix (op,(lna,tys,bds),_,_) -> let lfts' = el_liftn (Array.length bds) lfts in - mkFix (op, (Array.map (constr_fun lfts) tys, lna, - Array.map (constr_fun lfts') bds)) - | FCoFix (op,(tys,lna,bds),_,_) -> + mkFix (op, (lna, Array.map (constr_fun lfts) tys, + Array.map (constr_fun lfts') bds)) + | FCoFix (op,(lna,tys,bds),_,_) -> let lfts' = el_liftn (Array.length bds) lfts in - mkCoFix (op, (Array.map (constr_fun lfts) tys, lna, - Array.map (constr_fun lfts') bds)) + mkCoFix (op, (lna, Array.map (constr_fun lfts) tys, + Array.map (constr_fun lfts') bds)) | FApp (f,ve) -> mkApp (constr_fun lfts f, Array.map (constr_fun lfts) ve) @@ -903,9 +905,9 @@ and down_then_up info m stk = FInd(ind, Array.map (kl info) args) | FConstruct(c,args) -> FConstruct(c, Array.map (kl info) args) - | FCoFix(n,(ftys,na,fbds),bds,e) -> - FCoFix(n,(Array.map (kl info) ftys, na, - Array.map (kl info) fbds),bds,e) + | FCoFix(n,(na,ftys,fbds),bds,e) -> + FCoFix(n,(na, Array.map (kl info) ftys, + Array.map (kl info) fbds),bds,e) | FFlex(FConst(sp,args)) -> FFlex(FConst(sp, Array.map (kl info) args)) | FFlex(FEvar((i,args),e)) -> diff --git a/kernel/closure.mli b/kernel/closure.mli index 45088b3ac..3d8fb71f3 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -145,9 +145,9 @@ type fterm = | FInd of inductive_path * fconstr array | FConstruct of constructor_path * fconstr array | FApp of fconstr * fconstr array - | FFix of (int array * int) * (fconstr array * name list * fconstr array) + | FFix of (int array * int) * (name array * fconstr array * fconstr array) * constr array * fconstr subs - | FCoFix of int * (fconstr array * name list * fconstr array) + | FCoFix of int * (name array * fconstr array * fconstr array) * constr array * fconstr subs | FCases of case_info * fconstr * fconstr * fconstr array | FLambda of name * fconstr * fconstr * constr * fconstr subs diff --git a/kernel/environ.ml b/kernel/environ.ml index ee4666a63..ac813e233 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -125,11 +125,11 @@ let push_rel_context_to_named_context env = env.env_context.env_rel_context ([],ids_of_named_context sign0,sign0) in subst, (named_context_app (fun _ -> sign) env) -let push_rec_types (typarray,names,_) env = - let vect_lift_type = Array.mapi (fun i t -> lift i t) in - let nlara = - List.combine (List.rev names) (Array.to_list (vect_lift_type typarray)) in - List.fold_left (fun env nvar -> push_rel_assum nvar env) env nlara +let push_rec_types (lna,typarray,_) env = + let ctxt = + array_map2_i (fun i na t -> (na, type_app (lift i) t)) lna typarray in + Array.fold_left + (fun e assum -> push_rel_assum assum e) env ctxt let reset_rel_context env = { env with @@ -252,11 +252,11 @@ let hdchar env c = | Name id,_ -> lowercase_first_char id | Anonymous,t -> hdrec 0 (lift (n-k) (body_of_type t)) with Not_found -> "y") - | IsFix ((_,i),(_,ln,_)) -> - let id = match List.nth ln i with Name id -> id | _ -> assert false in + | IsFix ((_,i),(lna,_,_)) -> + let id = match lna.(i) with Name id -> id | _ -> assert false in lowercase_first_char id - | IsCoFix (i,(_,ln,_)) -> - let id = match List.nth ln i with Name id -> id | _ -> assert false in + | IsCoFix (i,(lna,_,_)) -> + let id = match lna.(i) with Name id -> id | _ -> assert false in lowercase_first_char id | IsMeta _|IsEvar _|IsMutCase (_, _, _, _) -> "y" in diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 478ffa5a8..312ee83d2 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -803,7 +803,7 @@ and eqappr cv_pb infos appr1 appr2 cuniv = convert_stacks infos lft1 lft2 v1 v2 u1 else raise NotConvertible - | (FFix (op1,(tys1,_,cl1),_,_), FFix(op2,(tys2,_,cl2),_,_)) -> + | (FFix (op1,(_,tys1,cl1),_,_), FFix(op2,(_,tys2,cl2),_,_)) -> if op1 = op2 then let u1 = convert_vect infos el1 el2 tys1 tys2 cuniv in @@ -814,7 +814,7 @@ and eqappr cv_pb infos appr1 appr2 cuniv = convert_stacks infos lft1 lft2 v1 v2 u2 else raise NotConvertible - | (FCoFix (op1,(tys1,_,cl1),_,_), FCoFix(op2,(tys2,_,cl2),_,_)) -> + | (FCoFix (op1,(_,tys1,cl1),_,_), FCoFix(op2,(_,tys2,cl2),_,_)) -> if op1 = op2 then let u1 = convert_vect infos el1 el2 tys1 tys2 cuniv in diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index d1ca1a52f..7df425894 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -32,145 +32,139 @@ let vect_lift_type = Array.mapi (fun i t -> type_app (lift i) t) (* The typing machine without information. *) -let rec execute env cstr = - let cst0 = Constraint.empty in + (* ATTENTION : faudra faire le typage du contexte des Const, + MutInd et MutConstructsi un jour cela devient des constructions + arbitraires et non plus des variables *) + +let univ_combinator (cst,univ) (j,c') = + (j,(Constraint.union cst c', merge_constraints c' univ)) + +let rec execute env cstr cu = match kind_of_term cstr with | IsMeta _ -> anomaly "the kernel does not understand metas" | IsEvar _ -> anomaly "the kernel does not understand existential variables" - - | IsRel n -> - (relative env Evd.empty n, cst0) - - | IsVar id -> - (make_judge cstr (lookup_named_type id env), cst0) - - (* ATTENTION : faudra faire le typage du contexte des Const, - MutInd et MutConstructsi un jour cela devient des constructions - arbitraires et non plus des variables *) - | IsConst c -> - (make_judge cstr (type_of_constant env Evd.empty c), cst0) - - | IsMutInd ind -> - (make_judge cstr (type_of_inductive env Evd.empty ind), cst0) - - | IsMutConstruct c -> - (make_judge cstr (type_of_constructor env Evd.empty c), cst0) - - | IsMutCase (ci,p,c,lf) -> - let (cj,cst1) = execute env c in - let (pj,cst2) = execute env p in - let (lfj,cst3) = execute_array env lf in - let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in - (type_of_case env Evd.empty ci pj cj lfj, cst) - - | IsFix ((vn,i as vni),(lar,lfi,vdef)) -> - if array_exists (fun n -> n < 0) vn then - error "General Fixpoints not allowed"; - let (larjv,vdefv,cst) = execute_fix env lar lfi vdef in - let larv = Array.map body_of_type larjv in - let fix = (vni,(larv,lfi,vdefv)) in - check_fix env Evd.empty fix; - (make_judge (mkFix fix) larjv.(i), cst) - - | IsCoFix (i,(lar,lfi,vdef)) -> - let (larjv,vdefv,cst) = execute_fix env lar lfi vdef in - let larv = Array.map body_of_type larjv in - let cofix = (i,(larv,lfi,vdefv)) in - check_cofix env Evd.empty cofix; - (make_judge (mkCoFix cofix) larjv.(i), cst) - | IsSort (Prop c) -> - (judge_of_prop_contents c, cst0) + (judge_of_prop_contents c, cu) | IsSort (Type u) -> let inst_u = if u == dummy_univ then new_univ() else u in - judge_of_type inst_u - + univ_combinator cu (judge_of_type inst_u) + | IsApp (f,args) -> - let (j,cst1) = execute env f in - let (jl,cst2) = execute_array env args in - let (j,cst3) = - apply_rel_list env Evd.empty false (Array.to_list jl) j in - let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in - (j, cst) + let (j,cu1) = execute env f cu in + let (jl,cu2) = execute_array env args cu1 in + univ_combinator cu2 + (apply_rel_list env Evd.empty false (Array.to_list jl) j) | IsLambda (name,c1,c2) -> - let (j,cst1) = execute env c1 in + let (j,cu1) = execute env c1 cu in let var = assumption_of_judgment env Evd.empty j in let env1 = push_rel_assum (name,var) env in - let (j',cst2) = execute env1 c2 in - let (j,cst3) = abs_rel env1 Evd.empty name var j' in - let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in - (j, cst) + let (j',cu2) = execute env1 c2 cu1 in + univ_combinator cu2 (abs_rel env1 Evd.empty name var j') - | IsProd (name,c1,c2) -> - let (j,cst1) = execute env c1 in + | IsProd (name,c1,c2) -> + let (j,cu1) = execute env c1 cu in let varj = type_judgment env Evd.empty j in let env1 = push_rel_assum (name,varj.utj_val) env in - let (j',cst2) = execute env1 c2 in + let (j',cu2) = execute env1 c2 cu1 in let varj' = type_judgment env Evd.empty j' in - let (j,cst3) = gen_rel env1 Evd.empty name varj varj' in - let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in - (j, cst) - - | IsLetIn (name,c1,c2,c3) -> - let (j1,cst1) = execute env c1 in - let (j2,cst2) = execute env c2 in - let tj2 = assumption_of_judgment env Evd.empty j2 in - let ({uj_val = b; uj_type = t},cst0) = cast_rel env Evd.empty j1 tj2 in - let (j3,cst3) = execute (push_rel_def (name,b,t) env) c3 in - let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in - ({ uj_val = mkLetIn (name, j1.uj_val, tj2, j3.uj_val) ; - uj_type = type_app (subst1 j1.uj_val) j3.uj_type }, - Constraint.union cst cst0) + univ_combinator cu2 + (gen_rel env1 Evd.empty name varj varj') + + | IsLetIn (name,c1,c2,c3) -> + let (j,cu1) = execute env (mkCast(c1,c2)) cu in + let env1 = push_rel_def (name,j.uj_val,j.uj_type) env in + let (j',cu2) = execute env1 c3 cu1 in + univ_combinator cu2 + (judge_of_letin env1 Evd.empty name j j') | IsCast (c,t) -> - let (cj,cst1) = execute env c in - let (tj,cst2) = execute env t in + let (cj,cu1) = execute env c cu in + let (tj,cu2) = execute env t cu1 in let tj = assumption_of_judgment env Evd.empty tj in - let cst = Constraint.union cst1 cst2 in - let (j, cst0) = cast_rel env Evd.empty cj tj in - (j, Constraint.union cst cst0) + univ_combinator cu2 + (cast_rel env Evd.empty cj tj) + + | IsRel n -> + (relative env Evd.empty n, cu) + + | IsVar id -> + (make_judge cstr (lookup_named_type id env), cu) + + | IsConst c -> + (make_judge cstr (type_of_constant env Evd.empty c), cu) + + (* Inductive types *) + | IsMutInd ind -> + (make_judge cstr (type_of_inductive env Evd.empty ind), cu) + + | IsMutConstruct c -> + (make_judge cstr (type_of_constructor env Evd.empty c), cu) + + | IsMutCase (ci,p,c,lf) -> + let (cj,cu1) = execute env c cu in + let (pj,cu2) = execute env p cu1 in + let (lfj,cu3) = execute_array env lf cu2 in + univ_combinator cu3 + (judge_of_case env Evd.empty ci pj cj lfj) + + | IsFix ((vn,i as vni),recdef) -> + if array_exists (fun n -> n < 0) vn then + error "General Fixpoints not allowed"; + let ((_,tys,_ as recdef'),cu1) = execute_fix env recdef cu in + let fix = (vni,recdef') in + check_fix env Evd.empty fix; + (make_judge (mkFix fix) tys.(i), cu1) + + | IsCoFix (i,recdef) -> + let ((_,tys,_ as recdef'),cu1) = execute_fix env recdef cu in + let cofix = (i,recdef') in + check_cofix env Evd.empty cofix; + (make_judge (mkCoFix cofix) tys.(i), cu1) -and execute_fix env lar lfi vdef = - let (larj,cst1) = execute_array env lar in +and execute_fix env (names,lar,vdef) cu = + let (larj,cu1) = execute_array env lar cu in let lara = Array.map (assumption_of_judgment env Evd.empty) larj in - let nlara = - List.combine (List.rev lfi) (Array.to_list (vect_lift_type lara)) in - let env1 = - List.fold_left (fun env nvar -> push_rel_assum nvar env) env nlara in - let (vdefj,cst2) = execute_array env1 vdef in + let env1 = push_rec_types (names,lara,vdef) env in + let (vdefj,cu2) = execute_array env1 vdef cu1 in let vdefv = Array.map j_val vdefj in - let cst3 = type_fixpoint env1 Evd.empty lfi lara vdefj in - let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in - (lara,vdefv,cst) + let cst = type_fixpoint env1 Evd.empty names lara vdefj in + univ_combinator cu2 ((names,lara,vdefv),cst) -and execute_array env v = - let (jl,u1) = execute_list env (Array.to_list v) in - (Array.of_list jl, u1) +and execute_array env v cu = + let (jl,cu1) = execute_list env (Array.to_list v) cu in + (Array.of_list jl, cu1) -and execute_list env = function +and execute_list env l cu = + match l with | [] -> - ([], Constraint.empty) + ([], cu) | c::r -> - let (j,cst1) = execute env c in - let (jr,cst2) = execute_list env r in - (j::jr, Constraint.union cst1 cst2) + let (j,cu1) = execute env c cu in + let (jr,cu2) = execute_list env r cu1 in + (j::jr, cu2) (* The typed type of a judgment. *) -let execute_type env constr = - let (j,cst) = execute env constr in - (type_judgment env Evd.empty j, cst) +let execute_type env constr cu = + let (j,cu1) = execute env constr cu in + (type_judgment env Evd.empty j, cu1) -(* Renaming for the following. *) +(* Exported machines. *) -let safe_infer = execute +let safe_infer env constr = + let (j,(cst,_)) = + execute env constr (Constraint.empty, universes env) in + (j, cst) -let safe_infer_type = execute_type +let safe_infer_type env constr = + let (j,(cst,_)) = + execute_type env constr (Constraint.empty, universes env) in + (j, cst) (* Typing of several terms. *) @@ -474,7 +468,6 @@ let env_of_safe_env e = e let typing env c = let (j,cst) = safe_infer env c in - let _ = add_constraints cst env in j let typing_in_unsafe_env = typing diff --git a/kernel/term.ml b/kernel/term.ml index 5d7be75ee..65cb495cd 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -70,7 +70,7 @@ type existential = existential_key * constr array type constant = section_path * constr array type constructor = constructor_path * constr array type inductive = inductive_path * constr array -type rec_declaration = constr array * name list * constr array +type rec_declaration = name array * constr array * constr array type fixpoint = (int array * int) * rec_declaration type cofixpoint = int * rec_declaration @@ -134,7 +134,7 @@ type 'constr constant = constant_path * 'constr array type 'constr constructor = constructor_path * 'constr array type 'constr inductive = inductive_path * 'constr array type ('constr, 'types) rec_declaration = - 'types array * name list * 'constr array + name array * 'types array * 'constr array type ('constr, 'types) fixpoint = (int array * int) * ('constr, 'types) rec_declaration type ('constr, 'types) cofixpoint = @@ -170,7 +170,7 @@ type existential = existential_key * constr array type constant = constant_path * constr array type constructor = constructor_path * constr array type inductive = inductive_path * constr array -type rec_declaration = constr array * name list * constr array +type rec_declaration = name array * constr array * constr array type fixpoint = (int array * int) * rec_declaration type cofixpoint = int * rec_declaration @@ -197,15 +197,19 @@ let comp_term t1 t2 = c1 == c2 & array_for_all2 (==) l1 l2 | IsMutCase (ci1,p1,c1,bl1), IsMutCase (ci2,p2,c2,bl2) -> ci1 == ci2 & p1 == p2 & c1 == c2 & array_for_all2 (==) bl1 bl2 - | IsFix (ln1,(tl1,lna1,bl1)), IsFix (ln2,(tl2,lna2,bl2)) -> - lna1 == lna2 & ln1 = ln2 - & array_for_all2 (==) tl1 tl2 & array_for_all2 (==) bl1 bl2 - | IsCoFix(ln1,(tl1,lna1,bl1)), IsCoFix(ln2,(tl2,lna2,bl2)) -> - lna1 == lna2 & ln1 = ln2 - & array_for_all2 (==) tl1 tl2 & array_for_all2 (==) bl1 bl2 + | IsFix (ln1,(lna1,tl1,bl1)), IsFix (ln2,(lna2,tl2,bl2)) -> + ln1 = ln2 + & array_for_all2 (==) lna1 lna2 + & array_for_all2 (==) tl1 tl2 + & array_for_all2 (==) bl1 bl2 + | IsCoFix(ln1,(lna1,tl1,bl1)), IsCoFix(ln2,(lna2,tl2,bl2)) -> + ln1 = ln2 + & array_for_all2 (==) lna1 lna2 + & array_for_all2 (==) tl1 tl2 + & array_for_all2 (==) bl1 bl2 | _ -> false -let hash_term (sh_rec,(sh_sort,sh_sp,sh_na,sh_id,sh_str)) t = +let hash_term (sh_rec,(sh_sort,sh_sp,sh_na,sh_id)) t = match t with | IsRel _ | IsMeta _ -> t | IsVar x -> IsVar (sh_id x) @@ -222,10 +226,14 @@ let hash_term (sh_rec,(sh_sort,sh_sp,sh_na,sh_id,sh_str)) t = IsMutConstruct (((sh_sp sp,i),j), Array.map sh_rec l) | IsMutCase (ci,p,c,bl) -> (* TO DO: extract ind_sp *) IsMutCase (ci, sh_rec p, sh_rec c, Array.map sh_rec bl) - | IsFix (ln,(tl,lna,bl)) -> - IsFix (ln,(Array.map sh_rec tl,List.map sh_na lna,Array.map sh_rec bl)) - | IsCoFix(ln,(tl,lna,bl)) -> - IsCoFix (ln,(Array.map sh_rec tl,List.map sh_na lna,Array.map sh_rec bl)) + | IsFix (ln,(lna,tl,bl)) -> + IsFix (ln,(Array.map sh_na lna, + Array.map sh_rec tl, + Array.map sh_rec bl)) + | IsCoFix(ln,(lna,tl,bl)) -> + IsCoFix (ln,(Array.map sh_na lna, + Array.map sh_rec tl, + Array.map sh_rec bl)) module Hconstr = Hashcons.Make( @@ -233,15 +241,14 @@ module Hconstr = type t = constr type u = (constr -> constr) * ((sorts -> sorts) * (section_path -> section_path) - * (name -> name) * (identifier -> identifier) - * (string -> string)) + * (name -> name) * (identifier -> identifier)) let hash_sub = hash_term let equal = comp_term let hash = Hashtbl.hash end) -let hcons_term (hsorts,hsp,hname,hident,hstr) = - Hashcons.recursive_hcons Hconstr.f (hsorts,hsp,hname,hident,hstr) +let hcons_term (hsorts,hsp,hname,hident) = + Hashcons.recursive_hcons Hconstr.f (hsorts,hsp,hname,hident) (* Constructs a DeBrujin index with number n *) let mkRel n = IsRel n @@ -502,11 +509,11 @@ let destCase c = match kind_of_term c with | _ -> anomaly "destCase" let destFix c = match kind_of_term c with - | IsFix ((recindxs,i),(types,funnames,bodies) as fix) -> fix + | IsFix fix -> fix | _ -> invalid_arg "destFix" let destCoFix c = match kind_of_term c with - | IsCoFix (i,(types,funnames,bodies) as cofix) -> cofix + | IsCoFix cofix -> cofix | _ -> invalid_arg "destCoFix" (******************************************************************) @@ -562,10 +569,12 @@ let fold_constr f acc c = match kind_of_term c with | IsMutInd (_,l) -> Array.fold_left f acc l | IsMutConstruct (_,l) -> Array.fold_left f acc l | IsMutCase (_,p,c,bl) -> Array.fold_left f (f (f acc p) c) bl - | IsFix (_,(tl,_,bl)) -> - array_fold_left2 (fun acc b t -> f (f acc b) t) acc bl tl - | IsCoFix (_,(tl,_,bl)) -> - array_fold_left2 (fun acc b t -> f (f acc b) t) acc bl tl + | IsFix (_,(lna,tl,bl)) -> + let fd = array_map3 (fun na t b -> (na,t,b)) lna tl bl in + Array.fold_left (fun acc (na,t,b) -> f (f acc t) b) acc fd + | IsCoFix (_,(lna,tl,bl)) -> + let fd = array_map3 (fun na t b -> (na,t,b)) lna tl bl in + Array.fold_left (fun acc (na,t,b) -> f (f acc t) b) acc fd (* [fold_constr_with_binders g f n acc c] folds [f n] on the immediate subterms of [c] starting from [acc] and proceeding from left to @@ -586,12 +595,14 @@ let fold_constr_with_binders g f n acc c = match kind_of_term c with | IsMutInd (_,l) -> Array.fold_left (f n) acc l | IsMutConstruct (_,l) -> Array.fold_left (f n) acc l | IsMutCase (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl - | IsFix (_,(tl,_,bl)) -> + | IsFix (_,(lna,tl,bl)) -> let n' = iterate g (Array.length tl) n in - array_fold_left2 (fun acc b t -> f n (f n' acc b) t) acc bl tl - | IsCoFix (_,(tl,_,bl)) -> + let fd = array_map2 (fun t b -> (t,b)) tl bl in + Array.fold_left (fun acc (t,b) -> f n (f n' acc t) b) acc fd + | IsCoFix (_,(lna,tl,bl)) -> let n' = iterate g (Array.length tl) n in - array_fold_left2 (fun acc b t -> f n (f n' acc b) t) acc bl tl + let fd = array_map2 (fun t b -> (t,b)) tl bl in + Array.fold_left (fun acc (t,b) -> f n (f n' acc t) b) acc fd (* [iter_constr f c] iters [f] on the immediate subterms of [c]; it is not recursive and the order with which subterms are processed is @@ -609,8 +620,8 @@ let iter_constr f c = match kind_of_term c with | IsMutInd (_,l) -> Array.iter f l | IsMutConstruct (_,l) -> Array.iter f l | IsMutCase (_,p,c,bl) -> f p; f c; Array.iter f bl - | IsFix (_,(tl,_,bl)) -> Array.iter f tl; Array.iter f bl - | IsCoFix (_,(tl,_,bl)) -> Array.iter f tl; Array.iter f bl + | IsFix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl + | IsCoFix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl (* [iter_constr_with_binders g f n c] iters [f n] on the immediate subterms of [c]; it carries an extra data [n] (typically a lift @@ -630,10 +641,12 @@ let iter_constr_with_binders g f n c = match kind_of_term c with | IsMutInd (_,l) -> Array.iter (f n) l | IsMutConstruct (_,l) -> Array.iter (f n) l | IsMutCase (_,p,c,bl) -> f n p; f n c; Array.iter (f n) bl - | IsFix (_,(tl,_,bl)) -> - Array.iter (f n) tl; Array.iter (f (iterate g (Array.length tl) n)) bl - | IsCoFix (_,(tl,_,bl)) -> - Array.iter (f n) tl; Array.iter (f (iterate g (Array.length tl) n)) bl + | IsFix (_,(_,tl,bl)) -> + Array.iter (f n) tl; + Array.iter (f (iterate g (Array.length tl) n)) bl + | IsCoFix (_,(_,tl,bl)) -> + Array.iter (f n) tl; + Array.iter (f (iterate g (Array.length tl) n)) bl (* [map_constr f c] maps [f] on the immediate subterms of [c]; it is not recursive and the order with which subterms are processed is @@ -651,8 +664,10 @@ let map_constr f c = match kind_of_term c with | IsMutInd (c,l) -> mkMutInd (c, Array.map f l) | IsMutConstruct (c,l) -> mkMutConstruct (c, Array.map f l) | IsMutCase (ci,p,c,bl) -> mkMutCase (ci, f p, f c, Array.map f bl) - | IsFix (ln,(tl,lna,bl)) -> mkFix (ln,(Array.map f tl,lna,Array.map f bl)) - | IsCoFix(ln,(tl,lna,bl)) -> mkCoFix (ln,(Array.map f tl,lna,Array.map f bl)) + | IsFix (ln,(lna,tl,bl)) -> + mkFix (ln,(lna,Array.map f tl,Array.map f bl)) + | IsCoFix(ln,(lna,tl,bl)) -> + mkCoFix (ln,(lna,Array.map f tl,Array.map f bl)) (* [map_constr_with_binders g f n c] maps [f n] on the immediate subterms of [c]; it carries an extra data [n] (typically a lift @@ -672,12 +687,12 @@ let map_constr_with_binders g f l c = match kind_of_term c with | IsMutInd (c,al) -> mkMutInd (c, Array.map (f l) al) | IsMutConstruct (c,al) -> mkMutConstruct (c, Array.map (f l) al) | IsMutCase (ci,p,c,bl) -> mkMutCase (ci, f l p, f l c, Array.map (f l) bl) - | IsFix (ln,(tl,lna,bl)) -> + | IsFix (ln,(lna,tl,bl)) -> let l' = iterate g (Array.length tl) l in - mkFix (ln,(Array.map (f l) tl,lna,Array.map (f l') bl)) - | IsCoFix(ln,(tl,lna,bl)) -> + mkFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl)) + | IsCoFix(ln,(lna,tl,bl)) -> let l' = iterate g (Array.length tl) l in - mkCoFix (ln,(Array.map (f l) tl,lna,Array.map (f l') bl)) + mkCoFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl)) (* [map_constr_with_named_binders g f l c] maps [f l] on the immediate subterms of [c]; it carries an extra data [l] (typically a name @@ -697,12 +712,12 @@ let map_constr_with_named_binders g f l c = match kind_of_term c with | IsMutInd (c,al) -> mkMutInd (c, Array.map (f l) al) | IsMutConstruct (c,al) -> mkMutConstruct (c, Array.map (f l) al) | IsMutCase (ci,p,c,bl) -> mkMutCase (ci, f l p, f l c, Array.map (f l) bl) - | IsFix (ln,(tl,lna,bl)) -> - let l' = List.fold_right g lna l in - mkFix (ln,(Array.map (f l) tl,lna,Array.map (f l') bl)) - | IsCoFix(ln,(tl,lna,bl)) -> - let l' = List.fold_right g lna l in - mkCoFix (ln,(Array.map (f l) tl,lna,Array.map (f l') bl)) + | IsFix (ln,(lna,tl,bl)) -> + let l' = Array.fold_left (fun l na -> g na l) l lna in + mkFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl)) + | IsCoFix(ln,(lna,tl,bl)) -> + let l' = Array.fold_left (fun l na -> g na l) l lna in + mkCoFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl)) (* [map_constr_with_binders_left_to_right g f n c] maps [f n] on the immediate subterms of [c]; it carries an extra data [n] (typically @@ -752,14 +767,14 @@ let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with | IsMutCase (ci,p,c,bl) -> let p' = f l p in let c' = f l c in mkMutCase (ci, p', c', array_map_left (f l) bl) - | IsFix (ln,(tl,lna,bl)) -> + | IsFix (ln,(lna,tl,bl)) -> let l' = iterate g (Array.length tl) l in - let tl', bl' = array_map_left_pair (f l) tl (f l') bl in - mkFix (ln,(tl',lna,bl')) - | IsCoFix(ln,(tl,lna,bl)) -> + let (tl',bl') = array_map_left_pair (f l) tl (f l') bl in + mkFix (ln,(lna,tl',bl')) + | IsCoFix(ln,(lna,tl,bl)) -> let l' = iterate g (Array.length tl) l in - let tl', bl' = array_map_left_pair (f l) tl (f l') bl in - mkCoFix (ln,(tl',lna,bl')) + let (tl',bl') = array_map_left_pair (f l) tl (f l') bl in + mkCoFix (ln,(lna,tl',bl')) (* strong *) let map_constr_with_full_binders g f l c = match kind_of_term c with @@ -774,14 +789,14 @@ let map_constr_with_full_binders g f l c = match kind_of_term c with | IsMutInd (c,al) -> mkMutInd (c, Array.map (f l) al) | IsMutConstruct (c,al) -> mkMutConstruct (c, Array.map (f l) al) | IsMutCase (ci,p,c,bl) -> mkMutCase (ci, f l p, f l c, Array.map (f l) bl) - | IsFix (ln,(tl,lna,bl)) -> - let tll = Array.to_list tl in - let l' = List.fold_right2 (fun na t l -> g (na,None,t) l) lna tll l in - mkFix (ln,(Array.map (f l) tl,lna,Array.map (f l') bl)) - | IsCoFix(ln,(tl,lna,bl)) -> - let tll = Array.to_list tl in - let l' = List.fold_right2 (fun na t l -> g (na,None,t) l) lna tll l in - mkCoFix (ln,(Array.map (f l) tl,lna,Array.map (f l') bl)) + | IsFix (ln,(lna,tl,bl)) -> + let l' = + array_fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in + mkFix (ln,(lna,Array.map (f l) tl, Array.map (f l') bl)) + | IsCoFix(ln,(lna,tl,bl)) -> + let l' = + array_fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in + mkCoFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl)) (* [compare_constr f c1 c2] compare [c1] and [c2] using [f] to compare the immediate subterms of [c1] of [c2] if needed; Cast's, @@ -815,9 +830,9 @@ let compare_constr f t1 t2 = c1 = c2 & array_for_all2 f l1 l2 | IsMutCase (_,p1,c1,bl1), IsMutCase (_,p2,c2,bl2) -> f p1 p2 & f c1 c2 & array_for_all2 f bl1 bl2 - | IsFix (ln1,(tl1,_,bl1)), IsFix (ln2,(tl2,_,bl2)) -> + | IsFix (ln1,(_,tl1,bl1)), IsFix (ln2,(_,tl2,bl2)) -> ln1 = ln2 & array_for_all2 f tl1 tl2 & array_for_all2 f bl1 bl2 - | IsCoFix(ln1,(tl1,_,bl1)), IsCoFix(ln2,(tl2,_,bl2)) -> + | IsCoFix(ln1,(_,tl1,bl1)), IsCoFix(ln2,(_,tl2,bl2)) -> ln1 = ln2 & array_for_all2 f tl1 tl2 & array_for_all2 f bl1 bl2 | _ -> false @@ -1132,37 +1147,38 @@ let mkMutCase = mkMutCase let mkMutCaseL (ci, p, c, ac) = mkMutCase (ci, p, c, Array.of_list ac) (* If recindxs = [|i1,...in|] + funnames = [|f1,...fn|] typarray = [|t1,...tn|] - funnames = [f1,.....fn] + bodies = [|b1,...bn|] then - mkFix recindxs i typarray funnames bodies + mkFix ((recindxs,i),(funnames,typarray,bodies)) constructs the ith function of the block - Fixpoint f1 [ctx1] = b1 - with f2 [ctx2] = b2 + Fixpoint f1 [ctx1] : t1 := b1 + with f2 [ctx2] : t2 := b2 ... - with fn [ctxn] = bn. + with fn [ctxn] : tn := bn. where the lenght of the jth context is ij. *) let mkFix = mkFix -(* If typarray = [|t1,...tn|] - funnames = [f1,.....fn] - bodies = [b1,.....bn] - then +(* If funnames = [|f1,...fn|] + typarray = [|t1,...tn|] + bodies = [|b1,...bn|] + then - mkCoFix i typsarray funnames bodies + mkCoFix (i,(funnames,typsarray,bodies)) constructs the ith function of the block - CoFixpoint f1 = b1 - with f2 = b2 + CoFixpoint f1 : t1 := b1 + with f2 : t2 := b2 ... - with fn = bn. + with fn : tn := bn. *) let mkCoFix = mkCoFix @@ -1686,8 +1702,8 @@ let hsort _ _ s = s let hcons_constr (hspcci,hspfw,hname,hident,hstr) = let hsortscci = Hashcons.simple_hcons hsort hspcci in let hsortsfw = Hashcons.simple_hcons hsort hspfw in - let hcci = hcons_term (hsortscci,hspcci,hname,hident,hstr) in - let hfw = hcons_term (hsortsfw,hspfw,hname,hident,hstr) in + let hcci = hcons_term (hsortscci,hspcci,hname,hident) in + let hfw = hcons_term (hsortsfw,hspfw,hname,hident) in let htcci = Hashcons.simple_hcons Htype.f (hcci,hsortscci) in (hcci,hfw,htcci) @@ -1710,7 +1726,7 @@ type constr_operator = | OpMutInd of inductive_path | OpMutConstruct of constructor_path | OpMutCase of case_info - | OpRec of fix_kind * name list + | OpRec of fix_kind * name array let splay_constr c = match kind_of_term c with | IsRel n -> OpRel n, [||] @@ -1727,8 +1743,8 @@ let splay_constr c = match kind_of_term c with | IsMutInd (ind_sp, l) -> OpMutInd ind_sp, l | IsMutConstruct (cstr_sp,l) -> OpMutConstruct cstr_sp, l | IsMutCase (ci,p,c,bl) -> OpMutCase ci, Array.append [|p;c|] bl - | IsFix (fi,(tl,lna,bl)) -> OpRec (RFix fi,lna), Array.append tl bl - | IsCoFix (fi,(tl,lna,bl)) -> OpRec (RCoFix fi,lna), Array.append tl bl + | IsFix (fi,(lna,tl,bl)) -> OpRec (RFix fi,lna), Array.append tl bl + | IsCoFix (fi,(lna,tl,bl)) -> OpRec (RCoFix fi,lna), Array.append tl bl let gather_constr = function | OpRel n, [||] -> mkRel n @@ -1747,24 +1763,14 @@ let gather_constr = function | OpMutCase ci, v -> let p = v.(0) and c = v.(1) and bl = Array.sub v 2 (Array.length v -2) in mkMutCase (ci, p, c, bl) - | OpRec (RFix fi,lna), a -> + | OpRec (RFix fi,na), a -> let n = Array.length a / 2 in - mkFix (fi,(Array.sub a 0 n, lna, Array.sub a n n)) - | OpRec (RCoFix i,lna), a -> + mkFix (fi,(na, Array.sub a 0 n, Array.sub a n n)) + | OpRec (RCoFix i,na), a -> let n = Array.length a / 2 in - mkCoFix (i,(Array.sub a 0 n, lna, Array.sub a n n)) + mkCoFix (i,(na, Array.sub a 0 n, Array.sub a n n)) | _ -> errorlabstrm "Term.gather_term" [< 'sTR "ill-formed splayed constr">] -let rec mycombine l1 l3 = - match (l1, l3) with - ([], []) -> [] - | (a1::l1, a3::l3) -> (a1, None, a3) :: mycombine l1 l3 - | (_, _) -> invalid_arg "mycombine" - -let rec mysplit = function - [] -> ([], []) - | (x, _, z)::l -> let (rx, rz) = mysplit l in (x::rx, z::rz) - let splay_constr_with_binders c = match kind_of_term c with | IsRel n -> OpRel n, [], [||] | IsVar id -> OpVar id, [], [||] @@ -1774,25 +1780,25 @@ let splay_constr_with_binders c = match kind_of_term c with | IsProd (x, t1, t2) -> OpProd x, [x,None,t1], [|t2|] | IsLambda (x, t1, t2) -> OpLambda x, [x,None,t1], [|t2|] | IsLetIn (x, b, t1, t2) -> OpLetIn x, [x,Some b,t1], [|t2|] - | IsApp (f,v) -> OpApp, [], Array.append [|f|] v + | IsApp (f,v) -> OpApp, [], Array.append [|f|] v | IsConst (sp, a) -> OpConst sp, [], a | IsEvar (sp, a) -> OpEvar sp, [], a | IsMutInd (ind_sp, l) -> OpMutInd ind_sp, [], l | IsMutConstruct (cstr_sp,l) -> OpMutConstruct cstr_sp, [], l | IsMutCase (ci,p,c,bl) -> let v = Array.append [|p;c|] bl in OpMutCase ci, [], v - | IsFix (fi,(tl,lna,bl)) -> + | IsFix (fi,(na,tl,bl)) -> let n = Array.length bl in - let ctxt = mycombine - (List.rev lna) - (Array.to_list (Array.mapi lift tl)) in - OpRec (RFix fi,lna), ctxt, bl - | IsCoFix (fi,(tl,lna,bl)) -> + let ctxt = + Array.to_list + (array_map2_i (fun i x t -> (x,None,lift i t)) na tl) in + OpRec (RFix fi,na), ctxt, bl + | IsCoFix (fi,(na,tl,bl)) -> let n = Array.length bl in - let ctxt = mycombine - (List.rev lna) - (Array.to_list (Array.mapi lift tl)) in - OpRec (RCoFix fi,lna), ctxt, bl + let ctxt = + Array.to_list + (array_map2_i (fun i x t -> (x,None,lift i t)) na tl) in + OpRec (RCoFix fi,na), ctxt, bl let gather_constr_with_binders = function | OpRel n, [], [||] -> mkRel n @@ -1811,14 +1817,14 @@ let gather_constr_with_binders = function | OpMutCase ci, [], v -> let p = v.(0) and c = v.(1) and bl = Array.sub v 2 (Array.length v -2) in mkMutCase (ci, p, c, bl) - | OpRec (RFix fi,lna), ctxt, bl -> - let (lna, tl) = mysplit ctxt in - let tl = Array.mapi (fun i -> lift (-i)) (Array.of_list tl) in - mkFix (fi,(tl, List.rev lna, bl)) - | OpRec (RCoFix i,lna), ctxt, bl -> - let (lna, tl) = mysplit ctxt in - let tl = Array.mapi (fun i -> lift (-i)) (Array.of_list tl) in - mkCoFix (i,(tl, List.rev lna, bl)) + | OpRec (RFix fi,na), ctxt, bl -> + let tl = + Array.mapi (fun i (_,_,t) -> lift (-i) t) (Array.of_list ctxt) in + mkFix (fi,(na, tl, bl)) + | OpRec (RCoFix i,na), ctxt, bl -> + let tl = + Array.mapi (fun i (_,_,t) -> lift (-i) t) (Array.of_list ctxt) in + mkCoFix (i,(na, tl, bl)) | _ -> errorlabstrm "Term.gather_term" [< 'sTR "ill-formed splayed constr">] let generic_fold_left f acc bl tl = diff --git a/kernel/term.mli b/kernel/term.mli index c8f6ea4a1..e873525ce 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -48,7 +48,7 @@ type 'constr constant = constant_path * 'constr array type 'constr constructor = constructor_path * 'constr array type 'constr inductive = inductive_path * 'constr array type ('constr, 'types) rec_declaration = - 'types array * name list * 'constr array + name array * 'types array * 'constr array type ('constr, 'types) fixpoint = (int array * int) * ('constr, 'types) rec_declaration type ('constr, 'types) cofixpoint = @@ -124,7 +124,7 @@ type existential = existential_key * constr array type constant = constant_path * constr array type constructor = constructor_path * constr array type inductive = inductive_path * constr array -type rec_declaration = types array * name list * constr array +type rec_declaration = name array * types array * constr array type fixpoint = (int array * int) * rec_declaration type cofixpoint = int * rec_declaration @@ -561,7 +561,7 @@ type constr_operator = | OpMutInd of inductive_path | OpMutConstruct of constructor_path | OpMutCase of case_info - | OpRec of fix_kind * Names.name list + | OpRec of fix_kind * name array val splay_constr : constr -> constr_operator * constr array diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index 387b7a930..320a30369 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -49,8 +49,8 @@ type type_error = | CantApplyBadType of (int * constr * constr) * unsafe_judgment * unsafe_judgment list | CantApplyNonFunctional of unsafe_judgment * unsafe_judgment list - | IllFormedRecBody of guard_error * name list * int * constr array - | IllTypedRecBody of int * name list * unsafe_judgment array + | IllFormedRecBody of guard_error * name array * int * constr array + | IllTypedRecBody of int * name array * unsafe_judgment array * types array exception TypeError of path_kind * env * type_error diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index e022be01d..277e5ca4e 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -53,8 +53,8 @@ type type_error = | CantApplyBadType of (int * constr * constr) * unsafe_judgment * unsafe_judgment list | CantApplyNonFunctional of unsafe_judgment * unsafe_judgment list - | IllFormedRecBody of guard_error * name list * int * constr array - | IllTypedRecBody of int * name list * unsafe_judgment array + | IllFormedRecBody of guard_error * name array * int * constr array + | IllTypedRecBody of int * name array * unsafe_judgment array * types array exception TypeError of path_kind * env * type_error @@ -94,9 +94,9 @@ val error_cant_apply_bad_type : unsafe_judgment -> unsafe_judgment list -> 'b val error_ill_formed_rec_body : - path_kind -> env -> guard_error -> name list -> int -> constr array -> 'b + path_kind -> env -> guard_error -> name array -> int -> constr array -> 'b val error_ill_typed_rec_body : - path_kind -> env -> int -> name list -> unsafe_judgment array + path_kind -> env -> int -> name array -> unsafe_judgment array -> types array -> 'b diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 997db29c3..37106b200 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -170,6 +170,14 @@ let abs_rel env sigma name var j = uj_type = mkProd (name, var, j.uj_type) }, Constraint.empty +let judge_of_letin env sigma name defj j = + let v = match kind_of_term defj.uj_val with + IsCast(c,t) -> c + | _ -> defj.uj_val in + ({ uj_val = mkLetIn (name, v, defj.uj_type, j.uj_val) ; + uj_type = type_app (subst1 v) j.uj_type }, + Constraint.empty) + (* [gen_rel env sigma name (typ1,s1) (typ2,s2)] implements the rule env |- typ1:s1 env, name:typ |- typ2 : s2 @@ -282,38 +290,38 @@ let error_elim_expln env sigma kp ki = exception Arity of (constr * constr * string) option let is_correct_arity env sigma kelim (c,p) indf (pt,t) = - let rec srec (pt,t) = + let rec srec (pt,t) u = let pt' = whd_betadeltaiota env sigma pt in let t' = whd_betadeltaiota env sigma t in match kind_of_term pt', kind_of_term t' with | IsProd (_,a1,a2), IsProd (_,a1',a2') -> - if is_conv env sigma a1 a1' then - srec (a2,a2') - else - raise (Arity None) + let univ = + try conv env sigma a1 a1' + with NotConvertible -> raise (Arity None) in + srec (a2,a2') (Constraint.union u univ) | IsProd (_,a1,a2), _ -> let k = whd_betadeltaiota env sigma a2 in let ksort = (match kind_of_term k with IsSort s -> s | _ -> raise (Arity None)) in let ind = build_dependent_inductive indf in - if is_conv env sigma a1 ind then - if List.exists (base_sort_cmp CONV ksort) kelim then - (true,k) - else - raise (Arity (Some(k,t',error_elim_expln env sigma k t'))) - else - raise (Arity None) + let univ = + try conv env sigma a1 ind + with NotConvertible -> raise (Arity None) in + if List.exists (base_sort_cmp CONV ksort) kelim then + ((true,k), Constraint.union u univ) + else + raise (Arity (Some(k,t',error_elim_expln env sigma k t'))) | k, IsProd (_,_,_) -> raise (Arity None) | k, ki -> let ksort = (match k with IsSort s -> s | _ -> raise (Arity None)) in if List.exists (base_sort_cmp CONV ksort) kelim then - false, pt' + (false, pt'), u else raise (Arity (Some(pt',t',error_elim_expln env sigma pt' t'))) -in - try srec (pt,t) + in + try srec (pt,t) Constraint.empty with Arity kinds -> let listarity = (List.map (make_arity env true indf) kelim) @@ -327,8 +335,9 @@ let find_case_dep_nparams env sigma (c,p) (IndFamily (mis,_) as indf) typP = let kelim = mis_kelim mis in let arsign,s = get_arity indf in let glob_t = it_mkProd_or_LetIn (mkSort s) arsign in - let (dep,_) = is_correct_arity env sigma kelim (c,p) indf (typP,glob_t) in - dep + let ((dep,_),univ) = + is_correct_arity env sigma kelim (c,p) indf (typP,glob_t) in + (dep,univ) (* type_case_branches type un <p>Case c of ... end IndType (indf,realargs) = type de c @@ -338,37 +347,43 @@ let find_case_dep_nparams env sigma (c,p) (IndFamily (mis,_) as indf) typP = *) let type_case_branches env sigma (IndType (indf,realargs)) pt p c = - let dep = find_case_dep_nparams env sigma (c,p) indf pt in + let (dep,univ) = find_case_dep_nparams env sigma (c,p) indf pt in let constructs = get_constructors indf in let lc = Array.map (build_branch_type env dep p) constructs in if dep then - (lc, beta_applist (p,(realargs@[c]))) + (lc, beta_applist (p,(realargs@[c])), univ) else - (lc, beta_applist (p,realargs)) + (lc, beta_applist (p,realargs), univ) let check_branches_message env sigma (c,ct) (explft,lft) = let expn = Array.length explft and n = Array.length lft in if n<>expn then error_number_branches CCI env c ct expn; - for i = 0 to n-1 do - if not (is_conv_leq env sigma lft.(i) (explft.(i))) then + let univ = ref Constraint.empty in + (for i = 0 to n-1 do + try + univ := Constraint.union !univ + (conv_leq env sigma lft.(i) (explft.(i))) + with NotConvertible -> error_ill_formed_branch CCI env c i (nf_betaiota env sigma lft.(i)) (nf_betaiota env sigma explft.(i)) - done + done; + !univ) -let type_of_case env sigma ci pj cj lfj = +let judge_of_case env sigma ci pj cj lfj = let lft = Array.map (fun j -> body_of_type j.uj_type) lfj in let indspec = try find_rectype env sigma (body_of_type cj.uj_type) with Induc -> error_case_not_inductive CCI env cj.uj_val (body_of_type cj.uj_type) in - let (bty,rslty) = + let (bty,rslty,univ) = type_case_branches env sigma indspec (body_of_type pj.uj_type) pj.uj_val cj.uj_val in let kind = mysort_of_arity env sigma (body_of_type pj.uj_type) in - check_branches_message env sigma - (cj.uj_val,body_of_type cj.uj_type) (bty,lft); - { uj_val = mkMutCase (ci, pj.uj_val, cj.uj_val, Array.map j_val lfj); - uj_type = rslty } + let univ' = check_branches_message env sigma + (cj.uj_val,body_of_type cj.uj_type) (bty,lft) in + ({ uj_val = mkMutCase (ci, pj.uj_val, cj.uj_val, Array.map j_val lfj); + uj_type = rslty }, + Constraint.union univ univ') (* let tocasekey = Profile.declare_profile "type_of_case";; @@ -492,8 +507,8 @@ let is_subterm_specif env sigma lcx mind_recvec = if array_for_all (fun st -> st=stl0) stl then stl0 else None - | IsFix ((recindxs,i),(typarray,funnames,bodies as recdef)) -> - let nbfix = List.length funnames in + | IsFix ((recindxs,i),(_,typarray,bodies as recdef)) -> + let nbfix = Array.length typarray in let decrArg = recindxs.(i) in let theBody = bodies.(i) in let sign,strippedBody = decompose_lam_n_assum (decrArg+1) theBody in @@ -620,11 +635,11 @@ let rec check_subterm_rec_meta env sigma vectn k def = Eduardo 7/9/98 *) - | IsFix ((recindxs,i),(typarray,funnames,bodies as recdef)) -> + | IsFix ((recindxs,i),(_,typarray,bodies as recdef)) -> (List.for_all (check_rec_call env n lst) l) && (array_for_all (check_rec_call env n lst) typarray) && - let nbfix = List.length funnames - in let decrArg = recindxs.(i) + let nbfix = Array.length typarray in + let decrArg = recindxs.(i) and env' = push_rec_types recdef env and n' = n+nbfix and lst' = map_lift_fst_n nbfix lst @@ -696,8 +711,8 @@ let rec check_subterm_rec_meta env sigma vectn k def = (array_for_all (check_rec_call env n lst) la) && (List.for_all (check_rec_call env n lst) l) - | IsCoFix (i,(typarray,funnames,bodies as recdef)) -> - let nbfix = Array.length bodies in + | IsCoFix (i,(_,typarray,bodies as recdef)) -> + let nbfix = Array.length typarray in let env' = push_rec_types recdef env in (array_for_all (check_rec_call env n lst) typarray) && (List.for_all (check_rec_call env n lst) l) && @@ -735,12 +750,12 @@ nvect is [|n1;..;nk|] which gives for each recursive definition the inductive-decreasing index the function checks the convertibility of ti with Ai *) -let check_fix env sigma ((nvect,bodynum),(types,names,bodies as recdef)) = +let check_fix env sigma ((nvect,bodynum),(names,types,bodies as recdef)) = let nbfix = Array.length bodies in if nbfix = 0 or Array.length nvect <> nbfix or Array.length types <> nbfix - or List.length names <> nbfix + or Array.length names <> nbfix or bodynum < 0 or bodynum >= nbfix then anomaly "Ill-formed fix term"; @@ -750,7 +765,7 @@ let check_fix env sigma ((nvect,bodynum),(types,names,bodies as recdef)) = let _ = check_subterm_rec_meta fixenv sigma nvect nvect.(i) bodies.(i) in () with FixGuardError err -> - error_ill_formed_rec_body CCI fixenv err (List.rev names) i bodies + error_ill_formed_rec_body CCI fixenv err names i bodies done (* @@ -845,7 +860,7 @@ let check_guard_rec_meta env sigma nbfix def deftype = else raise (CoFixGuardError (RecCallInTypeOfAbstraction t)) - | IsCoFix (j,(varit,lna,vdefs as recdef)) -> + | IsCoFix (j,(_,varit,vdefs as recdef)) -> if (List.for_all (noccur_with_meta n nbfix) args) then let nbfix = Array.length vdefs in @@ -880,7 +895,7 @@ let check_guard_rec_meta env sigma nbfix def deftype = (* The function which checks that the whole block of definitions satisfies the guarded condition *) -let check_cofix env sigma (bodynum,(types,names,bodies as recdef)) = +let check_cofix env sigma (bodynum,(names,types,bodies as recdef)) = let nbfix = Array.length bodies in for i = 0 to nbfix-1 do let fixenv = push_rec_types recdef env in @@ -888,7 +903,7 @@ let check_cofix env sigma (bodynum,(types,names,bodies as recdef)) = let _ = check_guard_rec_meta fixenv sigma nbfix bodies.(i) types.(i) in () with CoFixGuardError err -> - error_ill_formed_rec_body CCI fixenv err (List.rev names) i bodies + error_ill_formed_rec_body CCI fixenv err names i bodies done (* Checks the type of a (co)fixpoint. @@ -918,11 +933,11 @@ let control_only_guard env sigma = let rec control_rec c = match kind_of_term c with | IsRel _ | IsVar _ -> () | IsSort _ | IsMeta _ -> () - | IsCoFix (_,(tys,_,bds) as cofix) -> + | IsCoFix (_,(_,tys,bds) as cofix) -> check_cofix env sigma cofix; Array.iter control_rec tys; Array.iter control_rec bds; - | IsFix (_,(tys,_,bds) as fix) -> + | IsFix (_,(_,tys,bds) as fix) -> check_fix env sigma fix; Array.iter control_rec tys; Array.iter control_rec bds; diff --git a/kernel/typeops.mli b/kernel/typeops.mli index aaa07142f..3008c87cb 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -50,6 +50,11 @@ val abs_rel : env -> 'a evar_map -> name -> types -> unsafe_judgment -> unsafe_judgment * constraints +(* s Type of a let in. *) +val judge_of_letin : + env -> 'a evar_map -> name -> unsafe_judgment -> unsafe_judgment + -> unsafe_judgment * constraints + (*s Type of application. *) val apply_rel_list : env -> 'a evar_map -> bool -> unsafe_judgment list -> unsafe_judgment @@ -75,21 +80,22 @@ val type_of_inductive : env -> 'a evar_map -> inductive -> types val type_of_constructor : env -> 'a evar_map -> constructor -> types (*s Type of Cases. *) -val type_of_case : env -> 'a evar_map -> case_info +val judge_of_case : env -> 'a evar_map -> case_info -> unsafe_judgment -> unsafe_judgment - -> unsafe_judgment array -> unsafe_judgment + -> unsafe_judgment array -> unsafe_judgment * constraints val find_case_dep_nparams : - env -> 'a evar_map -> constr * constr -> inductive_family -> constr -> bool + env -> 'a evar_map -> constr * constr -> inductive_family -> constr + -> bool * constraints val type_case_branches : env -> 'a evar_map -> Inductive.inductive_type -> constr -> types - -> constr -> types array * types + -> constr -> types array * types * constraints (*s Type of fixpoints and guard condition. *) val check_fix : env -> 'a evar_map -> fixpoint -> unit val check_cofix : env -> 'a evar_map -> cofixpoint -> unit -val type_fixpoint : env -> 'a evar_map -> name list -> types array +val type_fixpoint : env -> 'a evar_map -> name array -> types array -> unsafe_judgment array -> constraints val control_only_guard : env -> 'a evar_map -> constr -> unit diff --git a/kernel/univ.ml b/kernel/univ.ml index e8f692300..b3d5a9b0e 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -288,18 +288,18 @@ let enforce_univ_gt u v g = (match compare g v u with | NGE -> setgt g u v | _ -> error_inconsistency()) - +(* let enforce_univ_relation g = function | Equiv (u,v) -> enforce_univ_eq u v g | Canonical {univ=u; gt=gt; ge=ge} -> let g' = List.fold_right (enforce_univ_gt u) gt g in List.fold_right (enforce_univ_geq u) ge g' - - +*) (* Merging 2 universe graphs *) +(* let merge_universes sp u1 u2 = UniverseMap.fold (fun _ a g -> enforce_univ_relation g a) u1 u2 - +*) (* Constraints and sets of consrtaints. *) @@ -308,6 +308,13 @@ type constraint_type = Gt | Geq | Eq type univ_constraint = universe * constraint_type * universe +let enforce_constraint cst g = + match cst with + | (u,Gt,v) -> enforce_univ_gt u v g + | (u,Geq,v) -> enforce_univ_geq u v g + | (u,Eq,v) -> enforce_univ_eq u v g + + module Constraint = Set.Make( struct type t = univ_constraint @@ -324,12 +331,7 @@ let enforce_geq u v c = Constraint.add (u,Geq,v) c let enforce_eq u v c = Constraint.add (u,Eq,v) c let merge_constraints c g = - Constraint.fold - (fun cst g -> match cst with - | (u,Gt,v) -> enforce_univ_gt u v g - | (u,Geq,v) -> enforce_univ_geq u v g - | (u,Eq,v) -> enforce_univ_eq u v g) - c g + Constraint.fold enforce_constraint c g (* Returns a fresh universe, juste above u. Does not create new universes for Type_0 (the sort of Prop and Set). diff --git a/lib/util.ml b/lib/util.ml index 44b5ef08f..cd32737d2 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -322,6 +322,14 @@ let array_last v = let array_cons e v = Array.append [|e|] v +let array_fold_right_i f v a = + let rec fold a n = + if n=0 then a + else + let k = n-1 in + fold (f k v.(k) a) k in + fold a (Array.length v) + let array_fold_left_i f v a = let n = Array.length a in let rec fold i v = if i = n then v else fold (succ i) (f i v a.(i)) in diff --git a/lib/util.mli b/lib/util.mli index 893825789..5122df3e8 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -103,6 +103,8 @@ val array_hd : 'a array -> 'a val array_tl : 'a array -> 'a array val array_last : 'a array -> 'a val array_cons : 'a -> 'a array -> 'a array +val array_fold_right_i : + (int -> 'b -> 'a -> 'a) -> 'b array -> 'a -> 'a val array_fold_left_i : (int -> 'a -> 'b -> 'a) -> 'a -> 'b array -> 'a val array_fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a diff --git a/library/indrec.ml b/library/indrec.ml index c02cb35e2..36c9f884f 100644 --- a/library/indrec.ml +++ b/library/indrec.ml @@ -342,8 +342,8 @@ let mis_make_indrec env sigma listdepkind mispec = let fixn = Array.of_list (List.rev ln) in let fixtyi = Array.of_list (List.rev ltyp) in let fixdef = Array.of_list (List.rev ldef) in - let names = list_tabulate (fun _ -> Name(id_of_string "F")) nrec in - mkFix ((fixn,p),(fixtyi,names,fixdef)) + let names = Array.create nrec (Name(id_of_string "F")) in + mkFix ((fixn,p),(names,fixtyi,fixdef)) in mrec 0 [] [] [] in @@ -469,11 +469,12 @@ let build_indrec env sigma mispec = (***********************************) (* To interpret the Match operator *) +(* TODO: check that we can drop universe constraints ? *) let type_mutind_rec env sigma (IndType (indf,realargs) as ind) pt p c = let (mispec,params) = dest_ind_family indf in let tyi = mis_index mispec in if mis_is_recursive_subset [tyi] mispec then - let dep = find_case_dep_nparams env sigma (c,p) indf pt in + let (dep,_) = find_case_dep_nparams env sigma (c,p) indf pt in let init_depPvec i = if i = tyi then Some(dep,p) else None in let depPvec = Array.init (mis_ntypes mispec) init_depPvec in let vargs = Array.of_list params in @@ -485,11 +486,13 @@ let type_mutind_rec env sigma (IndType (indf,realargs) as ind) pt p c = if dep then applist(p,realargs@[c]) else applist(p,realargs) ) else - type_case_branches env sigma ind pt p c + let (p,ra,_) = type_case_branches env sigma ind pt p c in + (p,ra) let type_rec_branches recursive env sigma ind pt p c = if recursive then type_mutind_rec env sigma ind pt p c else - type_case_branches env sigma ind pt p c + let (p,ra,_) = type_case_branches env sigma ind pt p c in + (p,ra) diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index 414c8eb0a..9c50e1fcf 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -82,10 +82,6 @@ GEXTEND Gram entry_type: [[ ":"; IDENT "ast"; IDENT "list" -> let _ = set_default_action_parser astlist in Id(loc,"LIST") - | ":"; IDENT "List" -> (* For compatibility *) - let _ = set_default_action_parser astlist in Id(loc,"LIST") - | ":"; IDENT "list" -> (* For compatibility *) - let _ = set_default_action_parser astlist in Id(loc,"LIST") | ":"; IDENT "ast" -> let _ = set_default_action_parser ast in Id(loc,"AST") | ":"; IDENT "constr" -> diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 461100816..b864d1031 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -368,17 +368,18 @@ and cbv_norm_value info = function (* reduction under binders *) | LAM (x,a,b,env) -> mkLambda (x, cbv_norm_term info env a, cbv_norm_term info (subs_lift env) b) - | FIXP ((lij,(lty,lna,bds)),env,args) -> + | FIXP ((lij,(names,lty,bds)),env,args) -> applistc (mkFix (lij, - (Array.map (cbv_norm_term info env) lty, lna, + (names, + Array.map (cbv_norm_term info env) lty, Array.map (cbv_norm_term info (subs_liftn (Array.length lty) env)) bds))) (List.map (cbv_norm_value info) args) - | COFIXP ((j,(lty,lna,bds)),env,args) -> + | COFIXP ((j,(names,lty,bds)),env,args) -> applistc (mkCoFix (j, - (Array.map (cbv_norm_term info env) lty, lna, + (names,Array.map (cbv_norm_term info env) lty, Array.map (cbv_norm_term info (subs_liftn (Array.length lty) env)) bds))) (List.map (cbv_norm_value info) args) diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 877dca8c9..170de079b 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -333,8 +333,8 @@ let rec detype avoid env t = in RCases (dummy_loc,tag,pred,[tomatch],eqnl) - | IsFix (nvn,(cl,lfn,vt)) -> detype_fix (RFix nvn) avoid env cl lfn vt - | IsCoFix (n,(cl,lfn,vt)) -> detype_fix (RCoFix n) avoid env cl lfn vt + | IsFix (nvn,recdef) -> detype_fix avoid env (RFix nvn) recdef + | IsCoFix (n,recdef) -> detype_fix avoid env (RCoFix n) recdef and detype_reference avoid env ref args = let args = @@ -350,13 +350,13 @@ and detype_reference avoid env ref args = if args = [] then f else RApp (dummy_loc, f, List.map (detype avoid env) args) -and detype_fix fk avoid env cl lfn vt = - let lfi = List.map (fun id -> next_name_away id avoid) lfn in - let def_avoid = lfi@avoid in +and detype_fix avoid env fixkind (names,tys,bodies) = + let lfi = Array.map (fun id -> next_name_away id avoid) names in + let def_avoid = Array.to_list lfi@avoid in let def_env = - List.fold_left (fun env id -> add_name (Name id) env) env lfi in - RRec(dummy_loc,fk,Array.of_list lfi,Array.map (detype avoid env) cl, - Array.map (detype def_avoid def_env) vt) + Array.fold_left (fun env id -> add_name (Name id) env) env lfi in + RRec(dummy_loc,fixkind,lfi,Array.map (detype avoid env) tys, + Array.map (detype def_avoid def_env) bodies) and detype_eqn avoid env constr_id construct_nargs branch = diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 382fba7f0..3d8653da0 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -252,7 +252,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = & (array_for_all2 (evar_conv_x env isevars CONV) cl1 cl2) & (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2) - | IsFix (li1,(tys1,_,bds1 as recdef1)), IsFix (li2,(tys2,_,bds2)) -> + | IsFix (li1,(_,tys1,bds1 as recdef1)), IsFix (li2,(_,tys2,bds2)) -> li1=li2 & (array_for_all2 (evar_conv_x env isevars CONV) tys1 tys2) & (array_for_all2 @@ -260,7 +260,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = bds1 bds2) & (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2) - | IsCoFix (i1,(tys1,_,bds1 as recdef1)), IsCoFix (i2,(tys2,_,bds2)) -> + | IsCoFix (i1,(_,tys1,bds1 as recdef1)), IsCoFix (i2,(_,tys2,bds2)) -> i1=i2 & (array_for_all2 (evar_conv_x env isevars CONV) tys1 tys2) & (array_for_all2 diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 14ee93f26..166786750 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -47,7 +47,7 @@ let transform_rec loc env sigma (p,c,lf) (indt,pt) = error_number_branches_loc loc CCI env c (mkAppliedInd indt) (mis_nconstr mispec); if mis_is_recursive_subset [tyi] mispec then - let dep = find_case_dep_nparams env sigma (c,p) indf pt in + let (dep,_) = find_case_dep_nparams env sigma (c,p) indf pt in let init_depFvec i = if i = tyi then Some(dep,mkRel 1) else None in let depFvec = Array.init (mis_ntypes mispec) init_depFvec in (* build now the fixpoint *) @@ -90,10 +90,10 @@ let transform_rec loc env sigma (p,c,lf) (indt,pt) = else let args = extended_rel_list 1 lnames in whd_beta (applist (lift (nar+1) p, args))))) - lnames - in - let fix = mkFix (([|nar|],0), - ([|typPfix|],[Name(id_of_string "F")],[|deffix|])) in + lnames in + let fix = + mkFix (([|nar|],0), + ([|Name(id_of_string "F")|],[|typPfix|],[|deffix|])) in applist (fix,realargs@[c]) else let ci = make_default_case_info mispec in @@ -261,29 +261,29 @@ let rec pretype tycon env isevars lvar lmeta = function (loc,"pretype", [< 'sTR "Cannot infer a term for this placeholder" >]))) - | RRec (loc,fixkind,lfi,lar,vdef) -> - let larj = Array.map (pretype_type empty_valcon env isevars lvar lmeta) lar in + | RRec (loc,fixkind,names,lar,vdef) -> + let larj = + Array.map (pretype_type empty_valcon env isevars lvar lmeta) lar in let lara = Array.map (fun a -> a.utj_val) larj in - let nbfix = Array.length lfi in - let lfi = List.map (fun id -> Name id) (Array.to_list lfi) in - let newenv = - array_fold_left2 (fun env id ar -> (push_rel_assum (id,ar) env)) - env (Array.of_list lfi) (vect_lift_type lara) in + let nbfix = Array.length lar in + let names = Array.map (fun id -> Name id) names in + let newenv = push_rec_types (names,lara,[||]) env in let vdefj = Array.mapi (fun i def -> (* we lift nbfix times the type in tycon, because of * the nbfix variables pushed to newenv *) - pretype (mk_tycon (lift nbfix (larj.(i).utj_val))) newenv isevars lvar - lmeta def) vdef in - evar_type_fixpoint env isevars lfi lara vdefj; + pretype (mk_tycon (lift nbfix (larj.(i).utj_val))) + newenv isevars lvar lmeta def) + vdef in + evar_type_fixpoint env isevars names lara vdefj; let fixj = match fixkind with | RFix (vn,i as vni) -> - let fix = (vni,(lara,lfi,Array.map j_val vdefj)) in + let fix = (vni,(names,lara,Array.map j_val vdefj)) in check_fix env (evars_of isevars) fix; make_judge (mkFix fix) lara.(i) | RCoFix i -> - let cofix = (i,(lara,lfi,Array.map j_val vdefj)) in + let cofix = (i,(names,lara,Array.map j_val vdefj)) in check_cofix env (evars_of isevars) cofix; make_judge (mkCoFix cofix) lara.(i) in inh_conv_coerce_to_tycon loc env isevars fixj tycon @@ -299,7 +299,9 @@ let rec pretype tycon env isevars lvar lmeta = function | c::rest -> let argloc = loc_of_rawconstr c in let resj = inh_app_fun env isevars resj in - match kind_of_term (whd_betadeltaiota env (evars_of isevars) resj.uj_type) with + let resty = + whd_betadeltaiota env (evars_of isevars) resj.uj_type in + match kind_of_term resty with | IsProd (na,c1,c2) -> let hj = pretype (mk_tycon c1) env isevars lvar lmeta c in let newresj = @@ -398,7 +400,7 @@ let rec pretype tycon env isevars lvar lmeta = function let evalPt = nf_ise1 (evars_of isevars) pj.uj_type in - let dep = find_case_dep_nparams env (evars_of isevars) + let (dep,_) = find_case_dep_nparams env (evars_of isevars) (cj.uj_val,pj.uj_val) indf evalPt in let (p,pt) = diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 43e0a91f9..a2b98a6d8 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -45,8 +45,8 @@ let sort_of_atomic_type env sigma ft args = in concl_of_arity env ft let typeur sigma metamap = -let rec type_of env cstr= - match kind_of_term cstr with + let rec type_of env cstr= + match kind_of_term cstr with | IsMeta n -> (try strip_outer_cast (List.assoc n metamap) with Not_found -> anomaly "type_of: this is not a well-typed term") @@ -73,16 +73,16 @@ let rec type_of env cstr= mkProd (name, c1, type_of (push_rel_assum (name,c1) env) c2) | IsLetIn (name,b,c1,c2) -> subst1 b (type_of (push_rel_def (name,b,c1) env) c2) - | IsFix ((vn,i),(lar,lfi,vdef)) -> lar.(i) - | IsCoFix (i,(lar,lfi,vdef)) -> lar.(i) + | IsFix ((_,i),(_,tys,_)) -> tys.(i) + | IsCoFix (i,(_,tys,_)) -> tys.(i) | IsApp(f,args)-> - strip_outer_cast (subst_type env sigma (type_of env f) - (Array.to_list args)) + strip_outer_cast + (subst_type env sigma (type_of env f) (Array.to_list args)) | IsCast (c,t) -> t | IsSort _ | IsProd (_,_,_) | IsMutInd _ -> mkSort (sort_of env cstr) -and sort_of env t = - match kind_of_term t with + and sort_of env t = + match kind_of_term t with | IsCast (c,s) when isSort s -> destSort s | IsSort (Prop c) -> type_0 | IsSort (Type u) -> Type Univ.dummy_univ @@ -95,7 +95,7 @@ and sort_of env t = anomaly "sort_of: Not a type (1)" | _ -> outsort env sigma (type_of env t) -in type_of, sort_of + in type_of, sort_of let get_type_of env sigma c = fst (typeur sigma []) env c let get_sort_of env sigma t = snd (typeur sigma []) env t diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index f65176602..72ebb6626 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -76,7 +76,7 @@ let _ = == [yip:Bip]..[yi1:Bi1](Fix(f|t)[xi<-ai] (Rel 1)..(Rel p)) with bj=aj if j<>ik and bj=(Rel c) and Bic=Aic[xn..xic-1 <- an..aic-1] *) -let check_fix_reversibility labs args ((lv,i),(tys,_,bds)) = +let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) = let n = List.length labs in let nargs = List.length args in if nargs > n then raise Elimconst; @@ -156,13 +156,12 @@ let compute_consteval_mutual_fix sigma env ref = match kind_of_term c' with | IsLambda (na,t,g) when l=[] -> srec (push_rel_assum (na,t) env) (minarg+1) (t::labs) ref g - | IsFix ((lv,i),(_,names,_) as fix) -> + | IsFix ((lv,i),(names,_,_) as fix) -> (* Last known constant wrapping Fix is ref = [labs](Fix l) *) (match compute_consteval_direct sigma env ref with | NotAnElimination -> (*Above const was eliminable but this not!*) NotAnElimination | EliminationFix (minarg',infos) -> - let names = Array.of_list names in let refs = Array.map (invert_name labs l names.(i) env sigma ref) names in @@ -291,8 +290,7 @@ let reduce_mind_case_use_function (sp,args) env mia = let ncargs = (fst mia.mci).(i-1) in let real_cargs = list_lastn ncargs mia.mcargs in applist (mia.mlf.(i-1), real_cargs) - | IsCoFix (_,(_,names,_) as cofix) -> - let names = Array.of_list names in + | IsCoFix (_,(names,_,_) as cofix) -> let build_fix_name i = match names.(i) with | Name id -> diff --git a/pretyping/typing.ml b/pretyping/typing.ml index c39197af7..f78216336 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -59,23 +59,22 @@ let rec execute mf env sigma cstr = let cj = execute mf env sigma c in let pj = execute mf env sigma p in let lfj = execute_array mf env sigma lf in - type_of_case env sigma ci pj cj lfj + let (j,_) = judge_of_case env sigma ci pj cj lfj in + j - | IsFix ((vn,i as vni),(lar,lfi,vdef)) -> + | IsFix ((vn,i as vni),recdef) -> if (not mf.fix) && array_exists (fun n -> n < 0) vn then error "General Fixpoints not allowed"; - let larjv,vdefv = execute_fix mf env sigma lar lfi vdef in - let larv = Array.map body_of_type larjv in - let fix = vni,(larv,lfi,vdefv) in + let (_,tys,_ as recdef') = execute_fix mf env sigma recdef in + let fix = (vni,recdef') in check_fix env sigma fix; - make_judge (mkFix fix) larjv.(i) + make_judge (mkFix fix) tys.(i) - | IsCoFix (i,(lar,lfi,vdef)) -> - let (larjv,vdefv) = execute_fix mf env sigma lar lfi vdef in - let larv = Array.map body_of_type larjv in - let cofix = i,(larv,lfi,vdefv) in + | IsCoFix (i,recdef) -> + let (_,tys,_ as recdef') = execute_fix mf env sigma recdef in + let cofix = (i,recdef') in check_cofix env sigma cofix; - make_judge (mkCoFix cofix) larjv.(i) + make_judge (mkCoFix cofix) tys.(i) | IsSort (Prop c) -> judge_of_prop_contents c @@ -122,17 +121,17 @@ let rec execute mf env sigma cstr = let j, _ = cast_rel env sigma cj tj in j -and execute_fix mf env sigma lar lfi vdef = +and execute_fix mf env sigma (names,lar,vdef) = let larj = execute_array mf env sigma lar in let lara = Array.map (assumption_of_judgment env sigma) larj in - let nlara = - List.combine (List.rev lfi) (Array.to_list (vect_lift_type lara)) in + let ctxt = + array_map2_i (fun i na ty -> (na, type_app (lift i) ty)) names lara in let env1 = - List.fold_left (fun env nvar -> push_rel_assum nvar env) env nlara in + Array.fold_left (fun env nvar -> push_rel_assum nvar env) env ctxt in let vdefj = execute_array mf env1 sigma vdef in let vdefv = Array.map j_val vdefj in - let cst3 = type_fixpoint env1 sigma lfi lara vdefj in - (lara,vdefv) + let cst3 = type_fixpoint env1 sigma names lara vdefj in + (names,lara,vdefv) and execute_array mf env sigma v = let jl = execute_list mf env sigma (Array.to_list v) in diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 630f45007..06a85319c 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -740,13 +740,13 @@ let constrain_clenv_to_subterm clause (op,cl) = with ex when catchable_exception ex -> matchrec c2) - | IsFix(_,(types,_,terms)) -> + | IsFix(_,(_,types,terms)) -> (try iter_fail matchrec types with ex when catchable_exception ex -> iter_fail matchrec terms) - | IsCoFix(_,(types,_,terms)) -> + | IsCoFix(_,(_,types,terms)) -> (try iter_fail matchrec types with ex when catchable_exception ex -> diff --git a/proofs/logic.ml b/proofs/logic.ml index e26733a15..663b21a8a 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -171,7 +171,7 @@ and mk_casegoals sigma goal goalacc p c = let indspec = try find_rectype env sigma ct with Induc -> anomaly "mk_casegoals" in - let (lbrty,conclty) = type_case_branches env sigma indspec pt p c in + let (lbrty,conclty,_) = type_case_branches env sigma indspec pt p c in (acc'',lbrty,conclty) @@ -505,7 +505,7 @@ let prim_extractor subfun vl pft = | {ref=Some(Prim{name=Fix;newids=[f];params=[Num(_,n)]},[spf]) } -> let cty = subst_vars vl cl in let na = Name f in - mkFix (([|n-1|],0),([|cty|], [na], [|subfun (f::vl) spf|])) + mkFix (([|n-1|],0),([|na|], [|cty|], [|subfun (f::vl) spf|])) | {ref=Some(Prim{name=Fix;newids=lf;terms=lar;params=ln},spfl) } -> let lcty = List.map (subst_vars vl) (cl::lar) in @@ -514,17 +514,17 @@ let prim_extractor subfun vl pft = | _ -> anomaly "mutual_fix_refiner") ln) in - let lna = List.map (fun f -> Name f) lf in + let names = Array.map (fun f -> Name f) (Array.of_list lf) in let newvl = List.fold_left (fun vl id -> (id::vl)) vl lf in let lfix =Array.map (subfun newvl) (Array.of_list spfl) in - mkFix ((vn,0),(Array.of_list lcty,lna,lfix)) + mkFix ((vn,0),(names,Array.of_list lcty,lfix)) | {ref=Some(Prim{name=Cofix;newids=lf;terms=lar},spfl) } -> let lcty = List.map (subst_vars vl) (cl::lar) in - let lna = List.map (fun f -> Name f) lf in + let names = Array.map (fun f -> Name f) (Array.of_list lf) in let newvl = List.fold_left (fun vl id -> (id::vl)) vl lf in let lfix =Array.map (subfun newvl) (Array.of_list spfl) in - mkCoFix (0,(Array.of_list lcty,lna,lfix)) + mkCoFix (0,(names,Array.of_list lcty,lfix)) | {ref=Some(Prim{name=Refine;terms=[c]},spfl) } -> let mvl = collect_meta_variables c in diff --git a/tactics/EAuto.v b/tactics/EAuto.v index e1ac47ddd..ba233cdd3 100644 --- a/tactics/EAuto.v +++ b/tactics/EAuto.v @@ -43,7 +43,7 @@ Grammar tactic simple_tactic: ast := | eautod_with_star [ "EAutod" eautoarg($np) "with" "*" ] -> [(EAuto "debug" ($LIST $np) "*")] -with eautoarg : List := +with eautoarg : ast list := | eautoarg_mt [ ] -> [ ] | eautoarg_n [ numarg($n) ] -> [ $n ] | eautoarg_np [ numarg($n) numarg($p) ] -> [ $n $p ] diff --git a/tactics/equality.ml b/tactics/equality.ml index ca64a856e..2b1c9da35 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1147,6 +1147,7 @@ let bind_eq = function | (Name _,Name _) -> true | _ -> false +(* TODO: Fix and CoFix also contain bound names *) let eqop_mod_names = function | OpLambda n0, OpLambda n1 -> bind_eq (n0,n1) | OpProd n0, OpProd n1 -> bind_eq (n0,n1) diff --git a/tactics/refine.ml b/tactics/refine.ml index aecc7fbea..1de41c489 100644 --- a/tactics/refine.ml +++ b/tactics/refine.ml @@ -187,21 +187,19 @@ let rec compute_metamap env c = match kind_of_term c with end (* 5. Fix. *) - | IsFix ((ni,i),(ai,fi,v)) -> - let vi = List.rev (List.map (fresh env) fi) in - let env' = - List.fold_left (fun env (v,ar) -> push_named_assum (v, ar) env) env - (List.combine vi (Array.to_list ai)) - in + | IsFix ((ni,i),(fi,ai,v)) -> + (* TODO: use a fold *) + let vi = Array.map (fresh env) fi in + let fi' = Array.map (fun id -> Name id) vi in + let env' = push_rec_types (fi',ai,v) env in let a = Array.map (compute_metamap env') - (Array.map (substl (List.map mkVar vi)) v) + (Array.map (substl (List.map mkVar (Array.to_list vi))) v) in begin try let v',mm,sgp = replace_in_array env' a in - let fi' = List.rev (List.map (fun id -> Name id) vi) in - let fix = mkFix ((ni,i),(ai,fi',v')) in + let fix = mkFix ((ni,i),(fi',ai,v')) in TH (fix,mm,sgp) with NoMeta -> TH (c,[],[]) @@ -254,10 +252,13 @@ let rec tcc_aux (TH (c,mm,sgp) as th) gl = error "invalid abstraction passed to function tcc_aux !" (* fix => tactique Fix *) - | IsFix ((ni,_),(ai,fi,_)) , _ -> + | IsFix ((ni,_),(fi,ai,_)) , _ -> let ids = - List.map (function Name id -> id | _ -> - error "recursive functions must have names !") fi + Array.to_list + (Array.map + (function Name id -> id + | _ -> error "recursive functions must have names !") + fi) in tclTHENS (mutual_fix ids (List.map succ (Array.to_list ni)) diff --git a/toplevel/command.ml b/toplevel/command.ml index dd8b9fb50..49f28922e 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -140,16 +140,18 @@ let minductive_message = function | l -> hOV 0 [< prlist_with_sep pr_coma pr_id l; 'sPC; 'sTR "are defined">] -let recursive_message = function - | [] -> anomaly "no recursive definition" - | [sp] -> [< Printer.pr_global sp; 'sTR " is recursively defined">] - | l -> hOV 0 [< prlist_with_sep pr_coma Printer.pr_global l; +let recursive_message v = + match Array.length v with + | 0 -> anomaly "no recursive definition" + | 1 -> [< Printer.pr_global v.(0); 'sTR " is recursively defined">] + | _ -> hOV 0 [< prvect_with_sep pr_coma Printer.pr_global v; 'sPC; 'sTR "are recursively defined">] -let corecursive_message = function - | [] -> anomaly "no corecursive definition" - | [x] -> [< Printer.pr_global x; 'sTR " is corecursively defined">] - | l -> hOV 0 [< prlist_with_sep pr_coma Printer.pr_global l; +let corecursive_message v = + match Array.length v with + | 0 -> anomaly "no corecursive definition" + | 1 -> [< Printer.pr_global v.(0); 'sTR " is corecursively defined">] + | _ -> hOV 0 [< prvect_with_sep pr_coma Printer.pr_global v; 'sPC; 'sTR "are corecursively defined">] let interp_mutual lparams lnamearconstrs finite = @@ -249,7 +251,9 @@ let collect_non_rec = searchrec ((f,mkCast (def,body_of_type ar))::lnonrec) (lf1@lf2) (ldef1@ldef2) (lar1@lar2) newlnv with Failure "try_find_i" -> - (lnonrec, (lnamerec,ldefrec,larrec,nrec)) + (List.rev lnonrec, + (Array.of_list lnamerec, Array.of_list ldefrec, + Array.of_list larrec, Array.of_list nrec)) in searchrec [] @@ -272,8 +276,7 @@ let build_recursive lnameargsardef = (Environ.push_named_assum (recname,arity) env, (arity::arl))) (env0,[]) lnameargsardef with e -> - States.unfreeze fs; raise e - in + States.unfreeze fs; raise e in let arityl = List.rev arityl in let recdef = try @@ -285,30 +288,25 @@ let build_recursive lnameargsardef = States.unfreeze fs; raise e in States.unfreeze fs; - let (lnonrec,(lnamerec,ldefrec,larrec,nvrec)) = + let (lnonrec,(namerec,defrec,arrec,nvrec)) = collect_non_rec lrecnames recdef arityl (Array.to_list nv) in let n = NeverDischarge in - if lnamerec <> [] then begin - let recvec = - Array.map (subst_vars (List.rev lnamerec)) (Array.of_list ldefrec) in - let varrec = Array.of_list larrec in - let rec declare i = function - | fi::lf -> - let ce = - { const_entry_body = - mkFix ((Array.of_list nvrec,i), - (varrec,List.map (fun id -> Name id) lnamerec, - recvec)); - const_entry_type = None } - in - let sp = declare_constant fi (ConstantEntry ce, n, false) in - (ConstRef sp)::(declare (i+1) lf) - | _ -> [] - in - (* declare the recursive definitions *) - let lrefrec = declare 0 lnamerec in - if_verbose pPNL (recursive_message lrefrec) - end; + let recvec = + Array.map (subst_vars (List.rev (Array.to_list namerec))) defrec in + let rec declare i fi = + let ce = + { const_entry_body = + mkFix ((nvrec,i), + (Array.map (fun id -> Name id) namerec, + arrec, + recvec)); + const_entry_type = None } in + let sp = declare_constant fi (ConstantEntry ce, n, false) in + (ConstRef sp) + in + (* declare the recursive definitions *) + let lrefrec = Array.mapi declare namerec in + if_verbose pPNL (recursive_message lrefrec); (* The others are declared as normal definitions *) let var_subst id = (id, global_reference CCI id) in let _ = @@ -319,7 +317,7 @@ let build_recursive lnameargsardef = let _ = declare_constant f (ConstantEntry ce,n,false) in warning ((string_of_id f)^" is non-recursively defined"); (var_subst f) :: subst) - (List.map var_subst lnamerec) + (List.map var_subst (Array.to_list namerec)) lnonrec in () @@ -340,8 +338,8 @@ let build_corecursive lnameardef = (Environ.push_named_assum (recname,arity) env, (arity::arl))) (env0,[]) lnameardef with e -> - States.unfreeze fs; raise e - in + States.unfreeze fs; raise e in + let arityl = List.rev arityl in let recdef = try List.map (fun (_,arityc,def) -> @@ -352,31 +350,24 @@ let build_corecursive lnameardef = States.unfreeze fs; raise e in States.unfreeze fs; - let (lnonrec,(lnamerec,ldefrec,larrec,_)) = - collect_non_rec lrecnames recdef (List.rev arityl) [] in + let (lnonrec,(namerec,defrec,arrec,_)) = + collect_non_rec lrecnames recdef arityl [] in let n = NeverDischarge in - if lnamerec <> [] then begin - let recvec = - if lnamerec = [] then - [||] - else - Array.map (subst_vars (List.rev lnamerec)) (Array.of_list ldefrec) in - let varrec = Array.of_list larrec in - let rec declare i = function - | fi::lf -> - let ce = - { const_entry_body = - mkCoFix (i, (varrec,List.map (fun id -> Name id) lnamerec, - recvec)); - const_entry_type = None } - in - let sp = declare_constant fi (ConstantEntry ce,n,false) in - (ConstRef sp) :: declare (i+1) lf - | _ -> [] - in - let lrefrec = declare 0 lnamerec in - if_verbose pPNL (corecursive_message lrefrec) - end; + let recvec = + Array.map (subst_vars (List.rev (Array.to_list namerec))) defrec in + let rec declare i fi = + let ce = + { const_entry_body = + mkCoFix (i, (Array.map (fun id -> Name id) namerec, + arrec, + recvec)); + const_entry_type = None } + in + let sp = declare_constant fi (ConstantEntry ce,n,false) in + (ConstRef sp) + in + let lrefrec = Array.mapi declare namerec in + if_verbose pPNL (corecursive_message lrefrec); let var_subst id = (id, global_reference CCI id) in let _ = List.fold_left @@ -386,7 +377,7 @@ let build_corecursive lnameardef = let _ = declare_constant f (ConstantEntry ce,n,false) in warning ((string_of_id f)^" is non-recursively defined"); (var_subst f) :: subst) - (List.map var_subst lnamerec) + (List.map var_subst (Array.to_list namerec)) lnonrec in () @@ -420,7 +411,7 @@ let build_scheme lnamedepindsort = ConstRef sp :: lrecref in let lrecref = List.fold_right2 declare listdecl lrecnames [] in - if_verbose pPNL (recursive_message lrecref) + if_verbose pPNL (recursive_message (Array.of_list lrecref)) let start_proof_com sopt stre com = let env = Global.env () in diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 2942bd314..4daec6d52 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -174,8 +174,9 @@ let explain_not_product k ctx c = [< 'sTR"The type of this term is expected to be a product but it is"; 'bRK(1,1); pr; 'fNL >] +(* TODO: use the names *) (* (co)fixpoints *) -let explain_ill_formed_rec_body k ctx err lna i vdefs = +let explain_ill_formed_rec_body k ctx err names i vdefs = let str = match err with (* Fixpoint guard errors *) @@ -211,17 +212,17 @@ let explain_ill_formed_rec_body k ctx err lna i vdefs = [< 'sTR "Not allowed recursive call in the type of cases in" >] | NotGuardedForm -> [< 'sTR "Definition not in guarded form" >] -in + in let pvd = prterm_env ctx vdefs.(i) in let s = - match List.nth lna i with Name id -> string_of_id id | Anonymous -> "_" in + match names.(i) with Name id -> string_of_id id | Anonymous -> "_" in [< str; 'fNL; 'sTR"The "; if Array.length vdefs = 1 then [<>] else [<'iNT (i+1); 'sTR "-th ">]; 'sTR"recursive definition"; 'sPC; 'sTR s; 'sPC ; 'sTR":="; 'sPC ; pvd; 'sPC; 'sTR "is not well-formed" >] - -let explain_ill_typed_rec_body k ctx i lna vdefj vargs = + +let explain_ill_typed_rec_body k ctx i names vdefj vargs = let pvd,pvdt = prjudge_env ctx (vdefj.(i)) in let pv = prterm_env ctx (body_of_type vargs.(i)) in [< 'sTR"The " ; |