From 515c95d5d339bc457772d3dd08765b55ad140054 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 7 Apr 2004 14:30:41 +0000 Subject: [PATCH] Added flag test_equality_only to are_convertible to better implement the <=_{\beta\delta\iota\zeta} relation. --- .../cic_proof_checking/cicReductionNaif.ml | 61 +++++++++++-------- 1 file changed, 34 insertions(+), 27 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml index 436200644..ea7fb4229 100644 --- a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml +++ b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml @@ -184,8 +184,8 @@ t in prerr_endline "DOPO WHD" ; flush stderr ; res (* t1, t2 must be well-typed *) let are_convertible = let module U = UriManager in - let rec aux context t1 t2 = - let aux2 t1 t2 = + let rec aux test_equality_only context t1 t2 = + let aux2 test_equality_only t1 t2 = (* this trivial euristic cuts down the total time of about five times ;-) *) (* this because most of the time t1 and t2 are "sintactically" the same *) if t1 = t2 then @@ -200,7 +200,7 @@ let are_convertible = (try List.fold_right2 (fun (uri1,x) (uri2,y) b -> - U.eq uri1 uri2 && aux context x y && b + U.eq uri1 uri2 && aux test_equality_only context x y && b ) exp_named_subst1 exp_named_subst2 true with Invalid_argument _ -> false @@ -213,21 +213,23 @@ let are_convertible = match t1,t2 with None,_ | _,None -> true - | Some t1',Some t2' -> aux context t1' t2' + | Some t1',Some t2' -> aux test_equality_only context t1' t2' ) true l1 l2 - | (C.Sort s1, C.Sort s2) -> true (*CSC da finire con gli universi *) + | (C.Sort s1, C.Sort s2) when s1 = s2 || s2 = C.Type -> true | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) -> - aux context s1 s2 && - aux ((Some (name1, (C.Decl s1)))::context) t1 t2 + aux true context s1 s2 && + aux test_equality_only ((Some (name1, (C.Decl s1)))::context) t1 t2 | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) -> - aux context s1 s2 && - aux ((Some (name1, (C.Decl s1)))::context) t1 t2 + aux test_equality_only context s1 s2 && + aux test_equality_only ((Some (name1, (C.Decl s1)))::context) t1 t2 | (C.LetIn (name1,s1,t1), C.LetIn(_,s2,t2)) -> - aux context s1 s2 && - aux ((Some (name1, (C.Def (s1,None))))::context) t1 t2 + aux test_equality_only context s1 s2 && + aux test_equality_only + ((Some (name1, (C.Def (s1,None))))::context) t1 t2 | (C.Appl l1, C.Appl l2) -> (try - List.fold_right2 (fun x y b -> aux context x y && b) l1 l2 true + List.fold_right2 + (fun x y b -> aux test_equality_only context x y && b) l1 l2 true with Invalid_argument _ -> false ) @@ -236,7 +238,7 @@ let are_convertible = (try List.fold_right2 (fun (uri1,x) (uri2,y) b -> - U.eq uri1 uri2 && aux context x y && b + U.eq uri1 uri2 && aux test_equality_only context x y && b ) exp_named_subst1 exp_named_subst2 true with Invalid_argument _ -> false @@ -248,7 +250,7 @@ let are_convertible = (try List.fold_right2 (fun (uri1,x) (uri2,y) b -> - U.eq uri1 uri2 && aux context x y && b + U.eq uri1 uri2 && aux test_equality_only context x y && b ) exp_named_subst1 exp_named_subst2 true with Invalid_argument _ -> false @@ -260,16 +262,19 @@ let are_convertible = (try List.fold_right2 (fun (uri1,x) (uri2,y) b -> - U.eq uri1 uri2 && aux context x y && b + U.eq uri1 uri2 && aux test_equality_only context x y && b ) exp_named_subst1 exp_named_subst2 true with Invalid_argument _ -> false ) | (C.MutCase (uri1,i1,outtype1,term1,pl1), C.MutCase (uri2,i2,outtype2,term2,pl2)) -> - U.eq uri1 uri2 && i1 = i2 && aux context outtype1 outtype2 && - aux context term1 term2 && - List.fold_right2 (fun x y b -> b && aux context x y) pl1 pl2 true + U.eq uri1 uri2 && i1 = i2 && + aux test_equality_only context outtype1 outtype2 && + aux test_equality_only context term1 term2 && + List.fold_right2 + (fun x y b -> b && aux test_equality_only context x y) + pl1 pl2 true | (C.Fix (i1,fl1), C.Fix (i2,fl2)) -> let tys = List.map (function (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1 @@ -277,8 +282,9 @@ let are_convertible = i1 = i2 && List.fold_right2 (fun (_,recindex1,ty1,bo1) (_,recindex2,ty2,bo2) b -> - b && recindex1 = recindex2 && aux context ty1 ty2 && - aux (tys@context) bo1 bo2) + b && recindex1 = recindex2 && + aux test_equality_only context ty1 ty2 && + aux test_equality_only (tys@context) bo1 bo2) fl1 fl2 true | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) -> let tys = @@ -287,23 +293,24 @@ let are_convertible = i1 = i2 && List.fold_right2 (fun (_,ty1,bo1) (_,ty2,bo2) b -> - b && aux context ty1 ty2 && aux (tys@context) bo1 bo2) + b && aux test_equality_only context ty1 ty2 && + aux test_equality_only (tys@context) bo1 bo2) fl1 fl2 true | (C.Cast _, _) | (_, C.Cast _) | (C.Implicit _, _) | (_, C.Implicit _) -> - raise (Impossible 3) (* we don't trust our whd ;-) *) + assert false | (_,_) -> false end in - if aux2 t1 t2 then true + if aux2 test_equality_only t1 t2 then true else begin debug t1 [t2] "PREWHD"; - let t1' = whd context t1 - and t2' = whd context t2 in + let t1' = whd context t1 in + let t2' = whd context t2 in debug t1' [t2'] "POSTWHD"; - aux2 t1' t2' + aux2 test_equality_only t1' t2' end in - aux + aux false ;; -- 2.39.2