From 219fb7c39077e9c82b3657ab067c176bb5b222ef Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 15 Jun 2005 11:38:55 +0000 Subject: [PATCH] are_convertible on MutCase was no longer checking the match arguments convertibility. --- helm/ocaml/cic_proof_checking/cicReduction.ml | 272 +++++++++--------- 1 file changed, 136 insertions(+), 136 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicReduction.ml b/helm/ocaml/cic_proof_checking/cicReduction.ml index 14b858491..8b9a0d22e 100644 --- a/helm/ocaml/cic_proof_checking/cicReduction.ml +++ b/helm/ocaml/cic_proof_checking/cicReduction.ml @@ -355,9 +355,9 @@ debug_print ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -> CicSubstitution.lift m (RS.from_ens (List.assq uri ens)) else let params = - let o,_ = - CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri - in + let o,_ = + CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri + in (match o with C.Constant _ -> raise ReferenceToConstant | C.Variable (_,_,_,params,_) -> params @@ -387,9 +387,9 @@ debug_print ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -> | C.Appl l -> C.Appl (List.map (unwind_aux m) l) | C.Const (uri,exp_named_subst) -> let params = - let o,_ = - CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri - in + let o,_ = + CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri + in (match o with C.Constant (_,_,_,params,_) -> params | C.Variable _ -> raise ReferenceToVariable @@ -403,9 +403,9 @@ debug_print ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -> C.Const (uri,exp_named_subst') | C.MutInd (uri,i,exp_named_subst) -> let params = - let o,_ = - CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri - in + let o,_ = + CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri + in (match o with C.Constant _ -> raise ReferenceToConstant | C.Variable _ -> raise ReferenceToVariable @@ -419,9 +419,9 @@ debug_print ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -> C.MutInd (uri,i,exp_named_subst') | C.MutConstruct (uri,i,j,exp_named_subst) -> let params = - let o,_ = - CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri - in + let o,_ = + CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri + in (match o with C.Constant _ -> raise ReferenceToConstant | C.Variable _ -> raise ReferenceToVariable @@ -546,8 +546,8 @@ if List.mem uri params then debug_print "---- OK2" ; reduce (0, [], [], RS.from_ens (List.assq uri ens), s) else ( let o,_ = - CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri - in + CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri + in match o with C.Constant _ -> raise ReferenceToConstant | C.CurrentProof _ -> raise ReferenceToCurrentProof @@ -562,9 +562,9 @@ if List.mem uri params then debug_print "---- OK2" ; ) | (k, e, ens, (C.Meta (n,l) as t), s) -> (try - let (_, term,_) = CicUtil.lookup_subst n subst in + let (_, term,_) = CicUtil.lookup_subst n subst in reduce (k, e, ens,CicSubstitution.subst_meta l term,s) - with CicUtil.Subst_not_found _ -> + with CicUtil.Subst_not_found _ -> let t' = unwind k e ens t in if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))) | (k, e, _, (C.Sort _ as t), s) -> t (* s should be empty *) @@ -607,9 +607,9 @@ if List.mem uri params then debug_print "---- OK2" ; if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s)) | (k, e, ens, (C.Const (uri,exp_named_subst) as t), s) -> (let o,_ = - CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri - in - match o with + CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri + in + match o with C.Constant (_,Some body,_,_,_) -> let ens' = push_exp_named_subst k e ens exp_named_subst in (* constants are closed *) @@ -664,13 +664,13 @@ if List.mem uri params then debug_print "---- OK2" ; reduce (k, e, ens, (List.nth pl (j-1)), s) | C.Appl (C.MutConstruct (_,_,j,_) :: tl) -> let (arity, r) = - let o,_ = - CicEnvironment.get_cooked_obj CicUniv.empty_ugraph mutind - in - match o with + let o,_ = + CicEnvironment.get_cooked_obj CicUniv.empty_ugraph mutind + in + match o with C.InductiveDefinition (tl,ingredients,r,_) -> - let (_,_,arity,_) = List.nth tl i in - (arity,r) + let (_,_,arity,_) = List.nth tl i in + (arity,r) | _ -> raise WrongUriToInductiveDefinition in let ts = @@ -685,7 +685,7 @@ if List.mem uri params then debug_print "---- OK2" ; in (* ts are already unwinded because they are a sublist of tl *) reduce (k, e, ens, (List.nth pl (j-1)), (RS.to_stack_list ts)@s) - | C.Cast _ | C.Implicit _ -> + | C.Cast _ | C.Implicit _ -> raise (Impossible 2) (* we don't trust our whd ;-) *) | _ -> let t' = unwind k e ens t in @@ -721,7 +721,7 @@ if List.mem uri params then debug_print "---- OK2" ; (name,recindex,unwind k e ens typ, unwind' leng k e ens body) in - List.map unwind_fl fl + List.map unwind_fl fl in let new_env = let counter = ref 0 in @@ -841,142 +841,142 @@ let are_convertible ?(subst=[]) ?(metasenv=[]) = with Invalid_argument _ -> false,ugraph ) - else - false,ugraph + else + false,ugraph | (C.Meta (n1,l1), C.Meta (n2,l2)) -> - if n1 = n2 then - let b2, ugraph1 = - let l1 = CicUtil.clean_up_local_context subst metasenv n1 l1 in - let l2 = CicUtil.clean_up_local_context subst metasenv n2 l2 in - List.fold_left2 - (fun (b,ugraph) t1 t2 -> - if b then - match t1,t2 with - None,_ - | _,None -> true,ugraph - | Some t1',Some t2' -> - aux test_equality_only context t1' t2' ugraph - else - false,ugraph - ) (true,ugraph) l1 l2 - in - if b2 then true,ugraph1 else false,ugraph - else - false,ugraph + if n1 = n2 then + let b2, ugraph1 = + let l1 = CicUtil.clean_up_local_context subst metasenv n1 l1 in + let l2 = CicUtil.clean_up_local_context subst metasenv n2 l2 in + List.fold_left2 + (fun (b,ugraph) t1 t2 -> + if b then + match t1,t2 with + None,_ + | _,None -> true,ugraph + | Some t1',Some t2' -> + aux test_equality_only context t1' t2' ugraph + else + false,ugraph + ) (true,ugraph) l1 l2 + in + if b2 then true,ugraph1 else false,ugraph + else + false,ugraph + (* TASSI: CONSTRAINTS *) + | (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only -> + true,(CicUniv.add_eq t2 t1 ugraph) + (* TASSI: CONSTRAINTS *) + | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> + true,(CicUniv.add_ge t2 t1 ugraph) + (* TASSI: CONSTRAINTS *) + | (C.Sort s1, C.Sort (C.Type _)) -> (not test_equality_only),ugraph (* TASSI: CONSTRAINTS *) - | (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only -> - true,(CicUniv.add_eq t2 t1 ugraph) - (* TASSI: CONSTRAINTS *) - | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> - true,(CicUniv.add_ge t2 t1 ugraph) - (* TASSI: CONSTRAINTS *) - | (C.Sort s1, C.Sort (C.Type _)) -> (not test_equality_only),ugraph - (* TASSI: CONSTRAINTS *) | (C.Sort s1, C.Sort s2) -> (s1 = s2),ugraph | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) -> - let b',ugraph' = aux true context s1 s2 ugraph in - if b' then + let b',ugraph' = aux true context s1 s2 ugraph in + if b' then aux test_equality_only ((Some (name1, (C.Decl s1)))::context) - t1 t2 ugraph' - else - false,ugraph + t1 t2 ugraph' + else + false,ugraph | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) -> let b',ugraph' = aux test_equality_only context s1 s2 ugraph in if b' then - aux test_equality_only ((Some (name1, (C.Decl s1)))::context) - t1 t2 ugraph' - else - false,ugraph + aux test_equality_only ((Some (name1, (C.Decl s1)))::context) + t1 t2 ugraph' + else + false,ugraph | (C.LetIn (name1,s1,t1), C.LetIn(_,s2,t2)) -> let b',ugraph' = aux test_equality_only context s1 s2 ugraph in - if b' then + if b' then aux test_equality_only ((Some (name1, (C.Def (s1,None))))::context) t1 t2 ugraph' - else - false,ugraph + else + false,ugraph | (C.Appl l1, C.Appl l2) -> (try List.fold_right2 (fun x y (b,ugraph) -> - if b then - aux test_equality_only context x y ugraph - else - false,ugraph) l1 l2 (true,ugraph) + if b then + aux test_equality_only context x y ugraph + else + false,ugraph) l1 l2 (true,ugraph) with Invalid_argument _ -> false,ugraph ) | (C.Const (uri1,exp_named_subst1), C.Const (uri2,exp_named_subst2)) -> let b' = U.eq uri1 uri2 in - if b' then + if b' then (try List.fold_right2 (fun (uri1,x) (uri2,y) (b,ugraph) -> - if b && U.eq uri1 uri2 then - aux test_equality_only context x y ugraph - else - false,ugraph + if b && U.eq uri1 uri2 then + aux test_equality_only context x y ugraph + else + false,ugraph ) exp_named_subst1 exp_named_subst2 (true,ugraph) with Invalid_argument _ -> false,ugraph ) - else - false,ugraph + else + false,ugraph | (C.MutInd (uri1,i1,exp_named_subst1), C.MutInd (uri2,i2,exp_named_subst2) ) -> let b' = U.eq uri1 uri2 && i1 = i2 in - if b' then + if b' then (try List.fold_right2 (fun (uri1,x) (uri2,y) (b,ugraph) -> if b && U.eq uri1 uri2 then - aux test_equality_only context x y ugraph - else - false,ugraph + aux test_equality_only context x y ugraph + else + false,ugraph ) exp_named_subst1 exp_named_subst2 (true,ugraph) with Invalid_argument _ -> false,ugraph ) - else - false,ugraph + else + false,ugraph | (C.MutConstruct (uri1,i1,j1,exp_named_subst1), C.MutConstruct (uri2,i2,j2,exp_named_subst2) ) -> let b' = U.eq uri1 uri2 && i1 = i2 && j1 = j2 in - if b' then + if b' then (try List.fold_right2 (fun (uri1,x) (uri2,y) (b,ugraph) -> - if b && U.eq uri1 uri2 then - aux test_equality_only context x y ugraph - else - false,ugraph + if b && U.eq uri1 uri2 then + aux test_equality_only context x y ugraph + else + false,ugraph ) exp_named_subst1 exp_named_subst2 (true,ugraph) with Invalid_argument _ -> false,ugraph ) - else - false,ugraph + else + false,ugraph | (C.MutCase (uri1,i1,outtype1,term1,pl1), C.MutCase (uri2,i2,outtype2,term2,pl2)) -> let b' = U.eq uri1 uri2 && i1 = i2 in - if b' then + if b' then let b'',ugraph''=aux test_equality_only context - outtype1 outtype2 ugraph in - if b'' then - let b''',ugraph'''= aux test_equality_only context - term1 term2 ugraph'' in - List.fold_right2 - (fun x y (b,ugraph) -> - if b then - aux test_equality_only context x y ugraph - else - false,ugraph) - pl1 pl2 (true,ugraph''') - else - false,ugraph - else - false,ugraph + outtype1 outtype2 ugraph in + if b'' then + let b''',ugraph'''= aux test_equality_only context + term1 term2 ugraph'' in + List.fold_right2 + (fun x y (b,ugraph) -> + if b then + aux test_equality_only context x y ugraph + else + false,ugraph) + pl1 pl2 (b''',ugraph''') + else + false,ugraph + else + false,ugraph | (C.Fix (i1,fl1), C.Fix (i2,fl2)) -> let tys = List.map (function (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1 @@ -985,17 +985,17 @@ let are_convertible ?(subst=[]) ?(metasenv=[]) = List.fold_right2 (fun (_,recindex1,ty1,bo1) (_,recindex2,ty2,bo2) (b,ugraph) -> if b && recindex1 = recindex2 then - let b',ugraph' = aux test_equality_only context ty1 ty2 - ugraph in - if b' then - aux test_equality_only (tys@context) bo1 bo2 ugraph' - else - false,ugraph - else - false,ugraph) - fl1 fl2 (true,ugraph) - else - false,ugraph + let b',ugraph' = aux test_equality_only context ty1 ty2 + ugraph in + if b' then + aux test_equality_only (tys@context) bo1 bo2 ugraph' + else + false,ugraph + else + false,ugraph) + fl1 fl2 (true,ugraph) + else + false,ugraph | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) -> let tys = List.map (function (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1 @@ -1003,18 +1003,18 @@ let are_convertible ?(subst=[]) ?(metasenv=[]) = if i1 = i2 then List.fold_right2 (fun (_,ty1,bo1) (_,ty2,bo2) (b,ugraph) -> - if b then - let b',ugraph' = aux test_equality_only context ty1 ty2 - ugraph in - if b' then - aux test_equality_only (tys@context) bo1 bo2 ugraph' - else - false,ugraph - else - false,ugraph) - fl1 fl2 (true,ugraph) - else - false,ugraph + if b then + let b',ugraph' = aux test_equality_only context ty1 ty2 + ugraph in + if b' then + aux test_equality_only (tys@context) bo1 bo2 ugraph' + else + false,ugraph + else + false,ugraph) + fl1 fl2 (true,ugraph) + else + false,ugraph | (C.Cast _, _) | (_, C.Cast _) | (C.Implicit _, _) | (_, C.Implicit _) -> assert false @@ -1025,11 +1025,11 @@ let are_convertible ?(subst=[]) ?(metasenv=[]) = debug t1 [t2] "PREWHD"; (* (match t1 with - Cic.Meta _ -> - debug_print (CicPp.ppterm t1); - debug_print (CicPp.ppterm (whd ~subst context t1)); - debug_print (CicPp.ppterm t2); - debug_print (CicPp.ppterm (whd ~subst context t2)) + Cic.Meta _ -> + debug_print (CicPp.ppterm t1); + debug_print (CicPp.ppterm (whd ~subst context t1)); + debug_print (CicPp.ppterm t2); + debug_print (CicPp.ppterm (whd ~subst context t2)) | _ -> ()); *) let t1' = whd ~subst context t1 in let t2' = whd ~subst context t2 in -- 2.39.2