From 345f329e767d0b4a1a87d10e08f92657a95c10ac Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 15 May 2008 09:24:19 +0000 Subject: [PATCH] height of constants properly handled --- .../components/ng_kernel/nCic2OCic.ml | 16 +-- .../components/ng_kernel/nCicEnvironment.ml | 10 +- helm/software/components/ng_kernel/nCicPp.ml | 8 +- .../components/ng_kernel/nCicReduction.ml | 102 +++++++++--------- .../components/ng_kernel/nCicTypeChecker.ml | 66 ++++++------ .../components/ng_kernel/nReference.ml | 51 +++++---- .../components/ng_kernel/nReference.mli | 6 +- .../components/ng_kernel/oCic2NCic.ml | 34 +++--- 8 files changed, 153 insertions(+), 140 deletions(-) diff --git a/helm/software/components/ng_kernel/nCic2OCic.ml b/helm/software/components/ng_kernel/nCic2OCic.ml index 57465b074..d78d5f3fe 100644 --- a/helm/software/components/ng_kernel/nCic2OCic.ml +++ b/helm/software/components/ng_kernel/nCic2OCic.ml @@ -13,7 +13,7 @@ let ouri_of_nuri u = UriManager.uri_of_string (NUri.string_of_uri u);; -let ouri_of_reference (NReference.Ref (_,u,_)) = ouri_of_nuri u;; +let ouri_of_reference (NReference.Ref (u,_)) = ouri_of_nuri u;; let nn_2_on = function | "_" -> Cic.Anonymous @@ -35,18 +35,18 @@ let convert_term uri n_fl t = | NCic.Sort NCic.CProp -> Cic.Sort Cic.CProp | NCic.Sort (NCic.Type _) -> Cic.Sort (Cic.Type (CicUniv.fresh ())) | NCic.Implicit _ -> assert false - | NCic.Const (NReference.Ref (_,u,NReference.Ind (_,i))) -> + | NCic.Const (NReference.Ref (u,NReference.Ind (_,i))) -> Cic.MutInd (ouri_of_nuri u,i,[]) - | NCic.Const (NReference.Ref (_,u,NReference.Con (i,j))) -> + | NCic.Const (NReference.Ref (u,NReference.Con (i,j))) -> Cic.MutConstruct (ouri_of_nuri u,i,j,[]) - | NCic.Const (NReference.Ref (_,u,NReference.Def)) - | NCic.Const (NReference.Ref (_,u,NReference.Decl)) -> + | NCic.Const (NReference.Ref (u,NReference.Def _)) + | NCic.Const (NReference.Ref (u,NReference.Decl)) -> Cic.Const (ouri_of_nuri u,[]) - | NCic.Match (NReference.Ref (_,u,NReference.Ind (_,i)),oty,t,pl) -> + | NCic.Match (NReference.Ref (u,NReference.Ind (_,i)),oty,t,pl) -> Cic.MutCase (ouri_of_nuri u,i, convert_term k oty, convert_term k t, List.map (convert_term k) pl) - | NCic.Const (NReference.Ref (_,u,NReference.Fix (i,_))) - | NCic.Const (NReference.Ref (_,u,NReference.CoFix i)) -> + | NCic.Const (NReference.Ref (u,NReference.Fix (i,_,_))) + | NCic.Const (NReference.Ref (u,NReference.CoFix i)) -> if NUri.eq u uri then Cic.Rel (n_fl - i + k) else diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml index b747dcd3f..2b98e8d4f 100644 --- a/helm/software/components/ng_kernel/nCicEnvironment.ml +++ b/helm/software/components/ng_kernel/nCicEnvironment.ml @@ -82,7 +82,7 @@ let get_checked_obj u = ;; let get_checked_def = function - | NReference.Ref (_, uri, NReference.Def) -> + | NReference.Ref (uri, NReference.Def _) -> (match get_checked_obj uri with | _,height,_,_, NCic.Constant (rlv,name,Some bo,ty,att) -> rlv,name,bo,ty,att,height @@ -93,7 +93,7 @@ let get_checked_def = function ;; let get_checked_indtys = function - | NReference.Ref (_, uri, (NReference.Ind (_,n)|NReference.Con (n,_))) -> + | NReference.Ref (uri, (NReference.Ind (_,n)|NReference.Con (n,_))) -> (match get_checked_obj uri with | _,_,_,_, NCic.Inductive (inductive,leftno,tys,att) -> inductive,leftno,tys,att,n @@ -102,7 +102,7 @@ let get_checked_indtys = function ;; let get_checked_fixes_or_cofixes = function - | NReference.Ref (_, uri, (NReference.Fix (fixno,_)|NReference.CoFix fixno))-> + | NReference.Ref (uri, (NReference.Fix (fixno,_,_)|NReference.CoFix fixno))-> (match get_checked_obj uri with | _,height,_,_, NCic.Fixpoint (_,funcs,att) -> funcs, att, height @@ -111,8 +111,8 @@ let get_checked_fixes_or_cofixes = function ;; let get_indty_leftno = function - | NReference.Ref (_, uri, NReference.Ind _) - | NReference.Ref (_, uri, NReference.Con _) -> + | NReference.Ref (uri, NReference.Ind _) + | NReference.Ref (uri, NReference.Con _) -> (match get_checked_obj uri with | _,_,_,_, NCic.Inductive (_,left,_,_) -> left | _ ->prerr_endline "get_indty_leftno called on a non ind 2";assert false) diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml index 8884621cb..a41057740 100644 --- a/helm/software/components/ng_kernel/nCicPp.ml +++ b/helm/software/components/ng_kernel/nCicPp.ml @@ -27,22 +27,22 @@ module R = NReference let r2s pp_fix_name r = try match r with - | R.Ref (_,u,R.Ind (_,i)) -> + | R.Ref (u,R.Ind (_,i)) -> (match NCicLibrary.get_obj u with | _,_,_,_, C.Inductive (_,_,itl,_) -> let _,name,_,_ = List.nth itl i in name | _ -> assert false) - | R.Ref (_,u,R.Con (i,j)) -> + | R.Ref (u,R.Con (i,j)) -> (match NCicLibrary.get_obj u with | _,_,_,_, C.Inductive (_,_,itl,_) -> let _,_,_,cl = List.nth itl i in let _,name,_ = List.nth cl (j-1) in name | _ -> assert false) - | R.Ref (_,u,(R.Decl | R.Def )) -> + | R.Ref (u,(R.Decl | R.Def _)) -> (match NCicLibrary.get_obj u with | _,_,_,_, C.Constant (_,name,_,_,_) -> name | _ -> assert false) - | R.Ref (_,u,(R.Fix (i,_)|R.CoFix i)) -> + | R.Ref (u,(R.Fix (i,_,_)|R.CoFix i)) -> (match NCicLibrary.get_obj u with | _,_,_,_, C.Fixpoint (_,fl,_) -> if pp_fix_name then diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml index 9cae8d409..5a8ba4164 100644 --- a/helm/software/components/ng_kernel/nCicReduction.ml +++ b/helm/software/components/ng_kernel/nCicReduction.ml @@ -396,15 +396,15 @@ module Reduction(RS : Strategy) = in aux (k, e, he, tl' @ s) | (_, _, NCic.Const - (NReference.Ref (height,_,NReference.Def) as refer), s) as config -> - if delta > height then config else + (NReference.Ref (_,NReference.Def height) as refer), s) as config -> + if delta >= height then config else let _,_,body,_,_,_ = NCicEnvironment.get_checked_def refer in aux (0, [], body, s) - | (_, _, NCic.Const (NReference.Ref (_,_, + | (_, _, NCic.Const (NReference.Ref (_, (NReference.Decl|NReference.Ind _|NReference.Con _|NReference.CoFix _))), _) as config -> config | (_, _, NCic.Const (NReference.Ref - (height,_,NReference.Fix (fixno,recindex)) as refer),s) as config -> - if delta > height then config else + (_,NReference.Fix (fixno,recindex,height)) as refer),s) as config -> + if delta >= height then config else (match try Some (RS.from_stack (List.nth s recindex)) with Failure _ -> None @@ -413,7 +413,7 @@ module Reduction(RS : Strategy) = | Some recparam -> let fixes,_,_ = NCicEnvironment.get_checked_fixes_or_cofixes refer in match reduce ~delta:0 ~subst context recparam with - | (_,_,NCic.Const (NReference.Ref (_,_,NReference.Con _)), _) as c -> + | (_,_,NCic.Const (NReference.Ref (_,NReference.Con _)), _) as c -> let new_s = replace recindex s (RS.compute_to_stack ~reduce:aux ~unwind c) in @@ -422,17 +422,17 @@ module Reduction(RS : Strategy) = | _ -> config) | (k, e, NCic.Match (_,_,term,pl),s) as config -> let decofix = function - | (_,_,NCic.Const(NReference.Ref(_,_,NReference.CoFix c)as refer),s)-> + | (_,_,NCic.Const(NReference.Ref(_,NReference.CoFix c)as refer),s)-> let cofixes,_,_ = NCicEnvironment.get_checked_fixes_or_cofixes refer in let _,_,_,_,body = List.nth cofixes c in reduce ~delta:0 ~subst context (0,[],body,s) | config -> config in (match decofix (reduce ~delta:0 ~subst context (k,e,term,[])) with - | (_, _, NCic.Const (NReference.Ref (_,_,NReference.Con (_,j))),[]) -> + | (_, _, NCic.Const (NReference.Ref (_,NReference.Con (_,j))),[]) -> aux (k, e, List.nth pl (j-1), s) | (_, _, NCic.Const - (NReference.Ref (_,_,NReference.Con (_,j)) as refer), s') -> + (NReference.Ref (_,NReference.Con (_,j)) as refer), s') -> let leftno = NCicEnvironment.get_indty_leftno refer in let _,params = HExtlib.split_nth leftno s' in aux (k, e, List.nth pl (j-1), params@s) @@ -489,26 +489,26 @@ module C = NCic (* t1, t2 must be well-typed *) let are_convertible whd ?(subst=[]) = - let rec aux test_equality_only context t1 t2 = - let rec aux2 test_equality_only t1 t2 = + let rec aux test_eq_only context t1 t2 = + let rec alpha_eq test_eq_only t1 t2 = if t1 === t2 then true else match (t1,t2) with | (C.Sort (C.Type a), C.Sort (C.Type b)) -> a <= b - | (C.Sort s1,C.Sort (C.Type _)) -> (not test_equality_only) + | (C.Sort s1,C.Sort (C.Type _)) -> (not test_eq_only) | (C.Sort s1, C.Sort s2) -> s1 = s2 | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) -> aux true context s1 s2 && - aux test_equality_only ((name1, C.Decl s1)::context) t1 t2 + aux test_eq_only ((name1, C.Decl s1)::context) t1 t2 | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) -> aux true context s1 s2 && - aux test_equality_only ((name1, C.Decl s1)::context) t1 t2 + aux test_eq_only ((name1, C.Decl s1)::context) t1 t2 | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) -> - aux test_equality_only context ty1 ty2 && - aux test_equality_only context s1 s2 && - aux test_equality_only ((name1, C.Def (s1,ty1))::context) t1 t2 + aux test_eq_only context ty1 ty2 && + aux test_eq_only context s1 s2 && + aux test_eq_only ((name1, C.Def (s1,ty1))::context) t1 t2 | (C.Meta (n1,(s1, C.Irl i1)), C.Meta (n2,(s2, C.Irl i2))) when n1 = n2 && s1 = s2 -> true @@ -516,7 +516,7 @@ let are_convertible whd ?(subst=[]) = let l1 = NCicUtils.expand_local_context l1 in let l2 = NCicUtils.expand_local_context l2 in (try List.for_all2 - (fun t1 t2 -> aux test_equality_only context + (fun t1 t2 -> aux test_eq_only context (NCicSubstitution.lift s1 t1) (NCicSubstitution.lift s2 t2)) l1 l2 @@ -526,68 +526,70 @@ let are_convertible whd ?(subst=[]) = (try let _,_,term,_ = NCicUtils.lookup_subst n1 subst in let term = NCicSubstitution.subst_meta l1 term in - aux test_equality_only context term t2 + aux test_eq_only context term t2 with NCicUtils.Subst_not_found _ -> false) | _, C.Meta (n2,l2) -> (try let _,_,term,_ = NCicUtils.lookup_subst n2 subst in let term = NCicSubstitution.subst_meta l2 term in - aux test_equality_only context t1 term + aux test_eq_only context t1 term with NCicUtils.Subst_not_found _ -> false) | (C.Appl l1, C.Appl l2) -> - (try List.for_all2 (aux test_equality_only context) l1 l2 + (try List.for_all2 (aux test_eq_only context) l1 l2 with Invalid_argument _ -> false) | (C.Match (ref1,outtype1,term1,pl1), C.Match (ref2,outtype2,term2,pl2)) -> NReference.eq ref1 ref2 && - aux test_equality_only context outtype1 outtype2 && - aux test_equality_only context term1 term2 && - (try List.for_all2 (aux test_equality_only context) pl1 pl2 + aux test_eq_only context outtype1 outtype2 && + aux test_eq_only context term1 term2 && + (try List.for_all2 (aux test_eq_only context) pl1 pl2 with Invalid_argument _ -> false) | (C.Implicit _, _) | (_, C.Implicit _) -> assert false | (_,_) -> false in - if aux2 test_equality_only t1 t2 then + if alpha_eq test_eq_only t1 t2 then true else let height_of = function - | NCic.Const (NReference.Ref (h,_,_)) -> h - | NCic.Appl (NCic.Const (NReference.Ref (h,_,_))::_) -> h + | NCic.Const (NReference.Ref (_,NReference.Def h)) -> h + | NCic.Const (NReference.Ref (_,NReference.Fix (_,_,h))) -> h + | NCic.Appl(NCic.Const(NReference.Ref(_,NReference.Def h))::_) -> h + | NCic.Appl(NCic.Const(NReference.Ref(_,NReference.Fix (_,_,h)))::_) -> h | _ -> 0 in - let min_delta (k1,env1,t1,s1) (k2,env2,t2,s2) = + let small_delta_step (k1,env1,t1,s1 as m1) (k2,env2,t2,s2 as m2) = let h1 = height_of t1 and h2 = height_of t2 in if h1 > h2 then - R.reduce ~delta:(h2+1) ~subst context (k1,env1,t1,s1), - (k2,env2,t2,s2), h2+1 + R.reduce ~delta:h2 ~subst context (k1,env1,t1,s1), m2, h2 else if h1 < h2 then - (k1,env1,t1,s1), - R.reduce ~delta:(h1+1) ~subst context (k2,env2,t2,s2), - h1+1 + m1, R.reduce ~delta:h1 ~subst context (k2,env2,t2,s2), h1 else - R.reduce ~delta:(max 0 (h1-1)) ~subst context (k1,env1,t1,s1), - R.reduce ~delta:(max 0 (h1-1)) ~subst context (k2,env2,t2,s2), - (max 0 (h1-1)) + let delta = max 0 (h1-1) in + R.reduce ~delta ~subst context (k1,env1,t1,s1), + R.reduce ~delta ~subst context (k2,env2,t2,s2), + delta in - let rec convert_machines ((k1,e1,t1,s1 as m1),(k2,e2,t2,s2 as m2),delta) todo = - (aux2 test_equality_only + let rec convert_machines ((k1,e1,t1,s1 as m1),(k2,e2,t2,s2 as m2),delta) = + (alpha_eq test_eq_only (R.unwind (k1,e1,t1,[])) (R.unwind (k2,e2,t2,[])) && - try - match List.combine s1 s2 @ todo with - | [] -> true - | (t1,t2) :: todo -> + try + List.for_all + (fun (t1,t2) -> let t1 = RS.from_stack t1 and t2 = RS.from_stack t2 in - convert_machines (min_delta t1 t2) todo - with Invalid_argument _ -> false) || - (delta > 0 && - let delta = delta - 1 in - let red = R.reduce ~delta ~subst context in - convert_machines (red m1,red m2,delta) todo) + convert_machines (small_delta_step t1 t2)) + (List.combine s1 s2) + with Invalid_argument _ -> false) || + (let red delta = R.reduce ~delta ~subst context in + if delta = 0 then + alpha_eq test_eq_only (R.unwind (red 0 m1)) (R.unwind (red 0 m2)) + else + let delta = delta - 1 in + convert_machines (red delta m1,red delta m2,delta)) in - convert_machines (min_delta (0,[],t1,[]) (0,[],t2,[])) [] + convert_machines (small_delta_step (0,[],t1,[]) (0,[],t2,[])) in aux false ;; @@ -603,7 +605,7 @@ let rec head_beta_reduce ?(delta=max_int) ?(upto=(-1)) t l = | _, C.Lambda(_,_,bo), arg::tl -> let bo = NCicSubstitution.subst arg bo in head_beta_reduce ~delta ~upto:(upto - 1) bo tl - | _, C.Const (NReference.Ref (height, _, NReference.Def) as re), _ + | _, C.Const (NReference.Ref (_, NReference.Def height) as re), _ when delta <= height -> let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def re in head_beta_reduce ~upto ~delta bo l diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index dea9d32c6..6ce59e263 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -104,8 +104,8 @@ let debruijn uri number_of_types context = let l1 = HExtlib.sharing_map (aux (k-s)) l in if l1 == l then t else C.Meta (i,(s,C.Ctx l1)) | C.Meta _ -> t - | C.Const (Ref.Ref (_,uri1,(Ref.Fix (no,_) | Ref.CoFix no))) - | C.Const (Ref.Ref (_,uri1,Ref.Ind (_,no))) when NUri.eq uri uri1 -> + | C.Const (Ref.Ref (uri1,(Ref.Fix (no,_,_) | Ref.CoFix no))) + | C.Const (Ref.Ref (uri1,Ref.Ind (_,no))) when NUri.eq uri uri1 -> C.Rel (k + number_of_types - no) | t -> U.map (fun _ k -> k+1) k aux t in @@ -182,8 +182,8 @@ let rec instantiate_parameters params c = let specialize_inductive_type_constrs ~subst context ty_term = match R.whd ~subst context ty_term with - | C.Const (Ref.Ref (_,uri,Ref.Ind (_,i)) as ref) - | C.Appl (C.Const (Ref.Ref (_,uri,Ref.Ind (_,i)) as ref) :: _ ) as ty -> + | C.Const (Ref.Ref (uri,Ref.Ind (_,i)) as ref) + | C.Appl (C.Const (Ref.Ref (uri,Ref.Ind (_,i)) as ref) :: _ ) as ty -> let args = match ty with C.Appl (_::tl) -> tl | _ -> [] in let is_ind, leftno, itl, attrs, i = E.get_checked_indtys ref in let left_args,_ = HExtlib.split_nth leftno args in @@ -268,14 +268,14 @@ let rec weakly_positive ~subst context n nn uri te = let dummy = C.Sort (C.Type ~-1) in (*CSC: mettere in cicSubstitution *) let rec subst_inductive_type_with_dummy _ = function - | C.Const (Ref.Ref (_,uri',Ref.Ind (true,0))) when NUri.eq uri' uri -> dummy - | C.Appl ((C.Const (Ref.Ref (_,uri',Ref.Ind (true,0))))::tl) + | C.Const (Ref.Ref (uri',Ref.Ind (true,0))) when NUri.eq uri' uri -> dummy + | C.Appl ((C.Const (Ref.Ref (uri',Ref.Ind (true,0))))::tl) when NUri.eq uri' uri -> dummy | t -> U.map (fun _ x->x) () subst_inductive_type_with_dummy t in match R.whd context te with - | C.Const (Ref.Ref (_,uri',Ref.Ind _)) - | C.Appl ((C.Const (Ref.Ref (_,uri',Ref.Ind _)))::_) + | C.Const (Ref.Ref (uri',Ref.Ind _)) + | C.Appl ((C.Const (Ref.Ref (uri',Ref.Ind _)))::_) when NUri.eq uri' uri -> true | C.Prod (name,source,dest) when does_not_occur ~subst ((name,C.Decl source)::context) 0 1 dest -> @@ -301,7 +301,7 @@ and strictly_positive ~subst context n nn te = strictly_positive ~subst ((name,C.Decl so)::context) (n+1) (nn+1) ta | C.Appl ((C.Rel m)::tl) when m > n && m <= nn -> List.for_all (does_not_occur ~subst context n nn) tl - | C.Appl (C.Const (Ref.Ref (_,uri,Ref.Ind (_,i)) as r)::tl) -> + | C.Appl (C.Const (Ref.Ref (uri,Ref.Ind (_,i)) as r)::tl) -> let _,paramsno,tyl,_,i = E.get_checked_indtys r in let _,name,ity,cl = List.nth tyl i in let ok = List.length tyl = 1 in @@ -435,7 +435,7 @@ let rec typeof ~subst ~metasenv context term = *) eat_prods ~subst ~metasenv context he ty_he args_with_ty | C.Appl _ -> raise (AssertFailure (lazy "Appl of length < 2")) - | C.Match (Ref.Ref (_,_,Ref.Ind (_,tyno)) as r,outtype,term,pl) -> + | C.Match (Ref.Ref (_,Ref.Ind (_,tyno)) as r,outtype,term,pl) -> let outsort = typeof_aux context outtype in let inductive,leftno,itl,_,_ = E.get_checked_indtys r in let constructorsno = @@ -445,8 +445,8 @@ let rec typeof ~subst ~metasenv context term = let ty = R.whd ~subst context (typeof_aux context term) in let r',tl = match ty with - C.Const (Ref.Ref (_,_,Ref.Ind _) as r') -> r',[] - | C.Appl (C.Const (Ref.Ref (_,_,Ref.Ind _) as r') :: tl) -> r',tl + C.Const (Ref.Ref (_,Ref.Ind _) as r') -> r',[] + | C.Appl (C.Const (Ref.Ref (_,Ref.Ind _) as r') :: tl) -> r',tl | _ -> raise (TypeCheckerFailure (lazy (Printf.sprintf @@ -512,8 +512,8 @@ let rec typeof ~subst ~metasenv context term = and type_of_branch ~subst context leftno outty cons tycons liftno = match R.whd ~subst context tycons with - | C.Const (Ref.Ref (_,_,Ref.Ind _)) -> C.Appl [S.lift liftno outty ; cons] - | C.Appl (C.Const (Ref.Ref (_,_,Ref.Ind _))::tl) -> + | C.Const (Ref.Ref (_,Ref.Ind _)) -> C.Appl [S.lift liftno outty ; cons] + | C.Appl (C.Const (Ref.Ref (_,Ref.Ind _))::tl) -> let _,arguments = HExtlib.split_nth leftno tl in C.Appl (S.lift liftno outty::arguments@[cons]) | C.Prod (name,so,de) -> @@ -756,7 +756,7 @@ and guarded_by_destructors r_uri r_len ~subst ~metasenv context recfuns t = | _,C.Decl _ -> () | _,C.Def (bo,_) -> aux k (S.lift m bo)) | C.Meta _ -> () - | C.Appl (C.Const ((Ref.Ref (_,uri,Ref.Fix (i,recno))) as r)::args) -> + | C.Appl (C.Const ((Ref.Ref (uri,Ref.Fix (i,recno,_))) as r)::args) -> if List.exists (fun t -> try aux k t;false with NotGuarded _ -> true) args then let fl,_,_ = E.get_checked_fixes_or_cofixes r in @@ -805,7 +805,7 @@ and guarded_by_destructors r_uri r_len ~subst ~metasenv context recfuns t = ) bos in List.iter (fun (bo,k) -> aux k bo) bos_and_ks - | C.Match (Ref.Ref (_,uri,Ref.Ind (true,_)),outtype,term,pl) as t -> + | C.Match (Ref.Ref (uri,Ref.Ind (true,_)),outtype,term,pl) as t -> (match R.whd ~subst context term with | C.Rel m | C.Appl (C.Rel m :: _ ) as t when is_safe m recfuns || m = x -> let ty = typeof ~subst ~metasenv context term in @@ -839,15 +839,15 @@ and guarded_by_constructors ~subst ~metasenv context t indURI indlen nn = | C.Sort _ | C.Implicit _ | C.Prod _ - | C.Const (Ref.Ref (_,_,Ref.Ind _)) + | C.Const (Ref.Ref (_,Ref.Ind _)) | C.LetIn _ -> raise (AssertFailure (lazy "17")) | C.Lambda (name,so,de) -> does_not_occur ~subst context n nn so && aux ((name,C.Decl so)::context) (n + 1) (nn + 1) h de | C.Appl ((C.Rel m)::tl) when m > n && m <= nn -> h && List.for_all (does_not_occur ~subst context n nn) tl - | C.Const (Ref.Ref (_,_,Ref.Con _)) -> true - | C.Appl (C.Const (Ref.Ref (_,uri, Ref.Con (_,j)) as ref) :: tl) as t -> + | C.Const (Ref.Ref (_,Ref.Con _)) -> true + | C.Appl (C.Const (Ref.Ref (uri, Ref.Con (_,j)) as ref) :: tl) as t -> let _, paramsno, _, _, _ = E.get_checked_indtys ref in let ty_t = typeof ~subst ~metasenv context t in let dc_ctx, dcl, start, stop = @@ -877,8 +877,8 @@ and guarded_by_constructors ~subst ~metasenv context t indURI indlen nn = does_not_occur ~subst context n nn out && does_not_occur ~subst context n nn te && List.for_all (aux context n nn h) pl - | C.Const (Ref.Ref (_,u,(Ref.Fix _| Ref.CoFix _)) as ref) - | C.Appl(C.Const (Ref.Ref(_,u,(Ref.Fix _| Ref.CoFix _)) as ref) :: _) as t -> + | C.Const (Ref.Ref (u,(Ref.Fix _| Ref.CoFix _)) as ref) + | C.Appl(C.Const (Ref.Ref(u,(Ref.Fix _| Ref.CoFix _)) as ref) :: _) as t -> let tl = match t with C.Appl (_::tl) -> tl | _ -> [] in let fl,_,_ = E.get_checked_fixes_or_cofixes ref in let len = List.length fl in @@ -923,11 +923,11 @@ and is_really_smaller | C.Appl (he::_) -> is_really_smaller r_uri r_len ~subst ~metasenv k he | C.Rel _ - | C.Const (Ref.Ref (_,_,Ref.Con _)) -> false + | C.Const (Ref.Ref (_,Ref.Con _)) -> false | C.Appl [] - | C.Const (Ref.Ref (_,_,Ref.Fix _)) -> assert false + | C.Const (Ref.Ref (_,Ref.Fix _)) -> assert false | C.Meta _ -> true - | C.Match (Ref.Ref (_,uri,_) as ref,outtype,term,pl) -> + | C.Match (Ref.Ref (uri,_) as ref,outtype,term,pl) -> (match term with | C.Rel m | C.Appl (C.Rel m :: _ ) when is_safe m recfuns || m = x -> (* TODO: add CoInd to references so that this call is useless *) @@ -949,26 +949,26 @@ and is_really_smaller and returns_a_coinductive ~subst context ty = match R.whd ~subst context ty with - | C.Const (Ref.Ref (_,uri,Ref.Ind (false,_)) as ref) - | C.Appl (C.Const (Ref.Ref (_,uri,Ref.Ind (false,_)) as ref)::_) -> + | C.Const (Ref.Ref (uri,Ref.Ind (false,_)) as ref) + | C.Appl (C.Const (Ref.Ref (uri,Ref.Ind (false,_)) as ref)::_) -> let _, _, itl, _, _ = E.get_checked_indtys ref in Some (uri,List.length itl) | C.Prod (n,so,de) -> returns_a_coinductive ~subst ((n,C.Decl so)::context) de | _ -> None -and type_of_constant ((Ref.Ref (_,uri,_)) as ref) = +and type_of_constant ((Ref.Ref (uri,_)) as ref) = match E.get_checked_obj uri, ref with - | (_,_,_,_,C.Inductive (_,_,tl,_)), Ref.Ref (_,_,Ref.Ind (_,i)) -> + | (_,_,_,_,C.Inductive (_,_,tl,_)), Ref.Ref (_,Ref.Ind (_,i)) -> let _,_,arity,_ = List.nth tl i in arity - | (_,_,_,_,C.Inductive (_,_,tl,_)), Ref.Ref (_,_,Ref.Con (i,j)) -> + | (_,_,_,_,C.Inductive (_,_,tl,_)), Ref.Ref (_,Ref.Con (i,j)) -> let _,_,_,cl = List.nth tl i in let _,_,arity = List.nth cl (j-1) in arity - | (_,_,_,_,C.Fixpoint (_,fl,_)), Ref.Ref (_,_,(Ref.Fix (i,_)|Ref.CoFix i)) -> + | (_,_,_,_,C.Fixpoint (_,fl,_)), Ref.Ref (_,(Ref.Fix (i,_,_)|Ref.CoFix i)) -> let _,_,_,arity,_ = List.nth fl i in arity - | (_,_,_,_,C.Constant (_,_,_,ty,_)), Ref.Ref (_,_,(Ref.Def |Ref.Decl)) -> ty + | (_,_,_,_,C.Constant (_,_,_,ty,_)), Ref.Ref (_,(Ref.Def _|Ref.Decl)) -> ty | _ -> raise (AssertFailure (lazy "type_of_constant: environment/reference")) ;; @@ -1077,8 +1077,8 @@ let typecheck_obj (uri,height,metasenv,subst,kind) = match List.hd context with _,C.Decl t -> t | _ -> assert false in match R.whd ~subst (List.tl context) he with - | C.Const (Ref.Ref (_,uri,Ref.Ind _) as ref) - | C.Appl (C.Const (Ref.Ref (_,uri,Ref.Ind _) as ref) :: _) -> + | C.Const (Ref.Ref (uri,Ref.Ind _) as ref) + | C.Appl (C.Const (Ref.Ref (uri,Ref.Ind _) as ref) :: _) -> let _,_,itl,_,_ = E.get_checked_indtys ref in uri, List.length itl | _ -> assert false diff --git a/helm/software/components/ng_kernel/nReference.ml b/helm/software/components/ng_kernel/nReference.ml index bdf4f98a7..1b2c0cc2b 100644 --- a/helm/software/components/ng_kernel/nReference.ml +++ b/helm/software/components/ng_kernel/nReference.ml @@ -15,13 +15,13 @@ exception IllFormedReference of string Lazy.t type spec = | Decl - | Def - | Fix of int * int (* fixno, recparamno *) + | Def of int (* height *) + | Fix of int * int * int (* fixno, recparamno, height *) | CoFix of int | Ind of bool * int (* inductive, indtyno *) | Con of int * int (* indtyno, constrno *) -type reference = Ref of int * NUri.uri * spec +type reference = Ref of NUri.uri * spec let eq = (==);; @@ -53,8 +53,17 @@ let uri_suffix_of_ref_suffix = function ;; let reference_of_string = - let counter = ref 0 in - let c () = incr counter; !counter in + let get3 s dot = + let comma2 = String.rindex s ',' in + let comma = String.rindex_from s (comma2-1) ',' in + let s_i = String.sub s (dot+5) (comma-dot-5) in + let s_j = String.sub s (comma+1) (comma2-comma-1) in + let s_h = String.sub s (comma2+1) (String.length s-comma2-2) in + let i = int_of_string s_i in + let j = int_of_string s_j in + let h = int_of_string s_h in + i,j,h + in let get2 s dot = let comma = String.rindex s ',' in let i = int_of_string (String.sub s (dot+5) (comma-dot-5)) in @@ -75,12 +84,12 @@ fun s -> let suffix = String.sub s (dot+1) 3 in let u = NUri.uri_of_string (prefix ^ uri_suffix_of_ref_suffix suffix) in match suffix with - | "dec" -> Ref (c (), u, Decl) - | "def" -> Ref (c (), u, Def) - | "fix" -> let i,j = get2 s dot in Ref (c (), u, Fix (i,j)) - | "cfx" -> let i = get1 s dot in Ref (c (), u, CoFix (i)) - | "ind" -> let b,i = get2 s dot in Ref (c (), u, Ind (b=1,i)) - | "con" -> let i,j = get2 s dot in Ref (c (), u, Con (i,j)) + | "dec" -> Ref (u, Decl) + | "def" -> let i = get1 s dot in Ref (u, Def i) + | "fix" -> let i,j,h = get3 s dot in Ref (u, Fix (i,j,h)) + | "cfx" -> let i = get1 s dot in Ref (u, CoFix (i)) + | "ind" -> let b,i = get2 s dot in Ref (u, Ind (b=1,i)) + | "con" -> let i,j = get2 s dot in Ref (u, Con (i,j)) | _ -> raise Not_found with Not_found -> raise (IllFormedReference (lazy s)) in @@ -88,33 +97,35 @@ fun s -> new_reference ;; -let string_of_reference (Ref (_,u,indinfo)) = +let string_of_reference (Ref (u,indinfo)) = let s = NUri.string_of_uri u in let dot = String.rindex s '.' in let s2 = String.sub s 0 dot in match indinfo with | Decl -> s2 ^ ".dec" - | Def -> s2 ^ ".def" - | Fix (i,j) -> s2 ^ ".fix(" ^ string_of_int i ^ "," ^ string_of_int j ^ ")" + | Def h -> s2 ^ ".def(" ^ string_of_int h ^ ")" + | Fix (i,j,h) -> + s2 ^ ".fix(" ^ string_of_int i ^ "," ^ + string_of_int j ^ "," ^ string_of_int h ^ ")" | CoFix i -> s2 ^ ".cfx(" ^ string_of_int i ^ ")" | Ind (b,i)->s2 ^".ind(" ^(if b then "1" else "0")^ "," ^ string_of_int i ^")" | Con (i,j) -> s2 ^ ".con(" ^ string_of_int i ^ "," ^ string_of_int j ^ ")" ;; let mk_constructor j = function - | Ref (d, u, Ind (_,i)) -> - reference_of_string (string_of_reference (Ref (d, u, Con (i,j)))) + | Ref (u, Ind (_,i)) -> + reference_of_string (string_of_reference (Ref (u, Con (i,j)))) | _ -> assert false ;; let mk_fix i j = function - | Ref (d, u, Fix _) -> - reference_of_string (string_of_reference (Ref (d, u, Fix (i,j)))) + | Ref (u, Fix (_,_,h)) -> + reference_of_string (string_of_reference (Ref (u, Fix (i,j,h)))) | _ -> assert false ;; let mk_cofix i = function - | Ref (d, u, CoFix _) -> - reference_of_string (string_of_reference (Ref (d, u, CoFix i))) + | Ref (u, CoFix _) -> + reference_of_string (string_of_reference (Ref (u, CoFix i))) | _ -> assert false ;; diff --git a/helm/software/components/ng_kernel/nReference.mli b/helm/software/components/ng_kernel/nReference.mli index 7f43c13e7..fcb12a995 100644 --- a/helm/software/components/ng_kernel/nReference.mli +++ b/helm/software/components/ng_kernel/nReference.mli @@ -15,13 +15,13 @@ exception IllFormedReference of string Lazy.t type spec = | Decl - | Def - | Fix of int * int (* fixno, recparamno *) + | Def of int (* height *) + | Fix of int * int * int (* fixno, recparamno, height *) | CoFix of int | Ind of bool * int (* inductive, indtyno *) | Con of int * int (* indtyno, constrno *) -type reference = private Ref of int * NUri.uri * spec +type reference = private Ref of NUri.uri * spec val eq: reference -> reference -> bool val string_of_reference: reference -> string diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml index 9f0bfc211..6a9dd715a 100644 --- a/helm/software/components/ng_kernel/oCic2NCic.ml +++ b/helm/software/components/ng_kernel/oCic2NCic.ml @@ -16,11 +16,11 @@ module Ref = NReference let nuri_of_ouri o = NUri.uri_of_string (UriManager.string_of_uri o);; (* porcatissima *) -type reference = Ref of int * NUri.uri * NReference.spec +type reference = Ref of NUri.uri * NReference.spec let reference_of_ouri u indinfo = let u = nuri_of_ouri u in NReference.reference_of_string - (NReference.string_of_reference (Obj.magic (Ref (max_int,u,indinfo)))) + (NReference.string_of_reference (Obj.magic (Ref (u,indinfo)))) ;; type ctx = @@ -323,10 +323,10 @@ let alpha t1 t2 ref ref' = | NCic.Prod (_,s1,t1), NCic.Prod (_,s2,t2) -> aux s1 s2; aux t1 t2 | NCic.LetIn (_,s1,ty1,t1), NCic.LetIn (_,s2,ty2,t2) -> aux s1 s2; aux ty1 ty2; aux t1 t2 - | NCic.Const (NReference.Ref (_,uu1,xp1)), - NCic.Const (NReference.Ref (_,uu2,xp2)) when - let NReference.Ref (_,u1,_) = ref in - let NReference.Ref (_,u2,_) = ref' in + | NCic.Const (NReference.Ref (uu1,xp1)), + NCic.Const (NReference.Ref (uu2,xp2)) when + let NReference.Ref (u1,_) = ref in + let NReference.Ref (u2,_) = ref' in NUri.eq uu1 u1 && NUri.eq uu2 u2 && xp1 = xp2 -> () | NCic.Const r1, NCic.Const r2 when NReference.eq r1 r2 -> () @@ -356,13 +356,13 @@ let find_in_cache name obj ref = (function (ref',obj') -> let recno, fixno = match ref with - NReference.Ref (_,_,NReference.Fix (fixno,recno)) -> recno,fixno - | NReference.Ref (_,_,NReference.CoFix (fixno)) -> ~-1,fixno + NReference.Ref (_,NReference.Fix (fixno,recno,_)) -> recno,fixno + | NReference.Ref (_,NReference.CoFix (fixno)) -> ~-1,fixno | _ -> assert false in let recno',fixno' = match ref' with - NReference.Ref (_,_,NReference.Fix (fixno',recno)) -> recno,fixno' - | NReference.Ref (_,_,NReference.CoFix (fixno')) -> ~-1,fixno' + NReference.Ref (_,NReference.Fix (fixno',recno,_)) -> recno,fixno' + | NReference.Ref (_,NReference.CoFix (fixno')) -> ~-1,fixno' | _ -> assert false in if recno = recno' && fixno = fixno' && same_obj ref ref' (obj,obj') then ( (* @@ -379,14 +379,14 @@ prerr_endline ("CACHE SAME NAME: " ^ NReference.string_of_reference ref ^ " <==> begin match obj, ref with | (_,_,_,_,NCic.Fixpoint (true,fl,_)) , - NReference.Ref (x,y,NReference.Fix _) -> + NReference.Ref (y,NReference.Fix _) -> ignore(List.fold_left (fun i (_,name,rno,_,_) -> let ref = NReference.mk_fix i rno ref in Hashtbl.add cache name (ref,obj); i+1 ) 0 fl) | (_,_,_,_,NCic.Fixpoint (false,fl,_)) , - NReference.Ref (x,y,NReference.CoFix _) -> + NReference.Ref (y,NReference.CoFix _) -> ignore(List.fold_left (fun i (_,name,rno,_,_) -> let ref = NReference.mk_cofix i ref in Hashtbl.add cache name (ref,obj); @@ -471,7 +471,7 @@ let convert_term uri t = (fun (name,recno,ty,_) (bctx, fixpoints, tys, idx) -> let ty, fixpoints_ty = aux true octx ctx n_fix uri ty in let r = (* recno is dummy here, must be lifted by the ctx len *) - reference_of_ouri buri (Ref.Fix (idx,recno)) + reference_of_ouri buri (Ref.Fix (idx,recno,1)) in bctx @ [Fix (lazy (r,name,ty))], fixpoints_ty@fixpoints,ty::tys,idx-1) @@ -481,9 +481,9 @@ let convert_term uri t = let free_decls = Lazy.force free_decls in let bctx = List.map (function ce -> match strictify ce with - | `Fix (Ref.Ref (_,_,Ref.Fix (idx, recno)),name, ty) -> + | `Fix (Ref.Ref (_,Ref.Fix (idx, recno,height)),name, ty) -> Fix (lazy (reference_of_ouri buri - (Ref.Fix (idx,recno+free_decls)),name,ty)) + (Ref.Fix (idx,recno+free_decls,height)),name,ty)) | _ -> assert false) bad_bctx @ ctx in let n_fl = List.length fl in @@ -509,7 +509,7 @@ let convert_term uri t = let obj = nuri_of_ouri buri,max_int,[],[], NCic.Fixpoint (true, fl, (`Generated, `Definition)) in - let r = reference_of_ouri buri (Ref.Fix (fixno,!rno_fixno)) in + let r = reference_of_ouri buri (Ref.Fix (fixno,!rno_fixno,1)) in let obj,r = let _,name,_,_,_ = List.nth fl fixno in match find_in_cache name obj r with @@ -587,7 +587,7 @@ let convert_term uri t = aux_ens k curi octx ctx n_fix uri ens (match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with | Cic.Constant (_,Some _,_,_,_) -> - NCic.Const (reference_of_ouri curi Ref.Def) + NCic.Const (reference_of_ouri curi (Ref.Def 1)) | Cic.Constant (_,None,_,_,_) -> NCic.Const (reference_of_ouri curi Ref.Decl) | _ -> assert false) -- 2.39.2