X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicReductionMachine.ml;h=e963ddce9b5062a941a45ff2b6e3cf44c89b8707;hb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;hp=4e92e6ebc9f2586b4356befdb71927cdb3a926a1;hpb=250550c3280e5afd3220fc1ba2a6b0c3d5a8ec47;p=helm.git diff --git a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml index 4e92e6ebc..e963ddce9 100644 --- a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml +++ b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml @@ -41,10 +41,7 @@ let debug t env s = CicPp.ppobj (C.Variable ("DEBUG", None, t, [])) ^ "\n" ^ i in if !fdebug = 0 then - begin - print_endline (s ^ "\n" ^ List.fold_right debug_aux (t::env) "") ; - flush stdout - end + prerr_endline (s ^ "\n" ^ List.fold_right debug_aux (t::env) "") ;; module type Strategy = @@ -377,7 +374,7 @@ prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) - in C.Meta (i, l') | C.Sort _ as t -> t - | C.Implicit as t -> t + | C.Implicit _ as t -> t | C.Cast (te,ty) -> C.Cast (unwind_aux m te, unwind_aux m ty) (*CSC ???*) | C.Prod (n,s,t) -> C.Prod (n, unwind_aux m s, unwind_aux (m + 1) t) | C.Lambda (n,s,t) -> C.Lambda (n, unwind_aux m s, unwind_aux (m + 1) t) @@ -549,7 +546,7 @@ if List.mem uri params then prerr_endline "---- OK2" ; 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 *) - | (k, e, _, (C.Implicit as t), s) -> t (* s should be empty *) + | (k, e, _, (C.Implicit _ as t), s) -> t (* s should be empty *) | (k, e, ens, (C.Cast (te,ty) as t), s) -> reduce (k, e, ens, te, s) (* s should be empty *) | (k, e, ens, (C.Prod _ as t), s) -> @@ -657,7 +654,7 @@ if List.mem uri params then prerr_endline "---- 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 @@ -774,8 +771,8 @@ let whd = R.whd;; (* 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 @@ -790,7 +787,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 @@ -803,21 +800,32 @@ 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.Prod (name1,s1,t1), C.Prod(_,s2,t2)) -> - aux context s1 s2 && - aux ((Some (name1, (C.Decl s1)))::context) t1 t2 + (* TASSI: CONSTRAINTS *) + | (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only -> + CicUniv.add_eq t2 t1 + (* TASSI: CONSTRAINTS *) + | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> + CicUniv.add_ge t2 t1 + (* TASSI: CONSTRAINTS *) + | (C.Sort s1, C.Sort (C.Type _)) -> not test_equality_only + (* TASSI: CONSTRAINTS *) + | (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 ((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 ) @@ -826,7 +834,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 @@ -838,7 +846,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 @@ -850,16 +858,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 @@ -867,8 +878,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 = @@ -877,23 +889,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) -> + | (C.Implicit _, _) | (_, C.Implicit _) -> 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 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 ;;