X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicReductionMachine.ml;h=f53471414b660a53e7e4c04310c1c0b0383ef54d;hb=ac7687ce66526f905874ed99a845223c853c558a;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..f53471414 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) @@ -501,7 +498,7 @@ if List.mem uri params then prerr_endline "---- OK2" ; unwind' 0 ;; - let reduce context : config -> Cic.term = + let reduce ?(subst = []) context : config -> Cic.term = let module C = Cic in let module S = CicSubstitution in let rec reduce = @@ -545,11 +542,15 @@ if List.mem uri params then prerr_endline "---- OK2" ; let ens' = push_exp_named_subst k e ens exp_named_subst in reduce (0, [], ens', body, s) ) - | (k, e, ens, (C.Meta _ as t), s) -> - let t' = unwind k e ens t in - if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s)) + | (k, e, ens, (C.Meta (n,l) as t), s) -> + (try + let (_, term,_) = CicUtil.lookup_subst n subst in + reduce (k, e, ens,CicSubstitution.lift_meta l term,s) + 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 *) - | (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 +658,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 @@ -725,10 +726,10 @@ if List.mem uri params then prerr_endline "---- OK2" ; | (uri,t)::tl -> push_exp_named_subst k e ((uri,RS.to_ens (unwind k e ens t))::ens) tl in - reduce + reduce ;; - let rec whd context t = reduce context (0, [], [], t, []);; + let rec whd ?(subst=[]) context t = reduce ~subst context (0, [], [], t, []);; (* DEBUGGING ONLY let whd context t = @@ -768,17 +769,21 @@ module R = Reduction ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;; *) module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);; +module U = UriManager;; let whd = R.whd;; + (* mimic ocaml (<< 3.08) "=" behaviour. Tests physical equality first then + * fallbacks to structural equality *) +let (===) x y = (Pervasives.compare x y = 0) + (* 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 are_convertible ?(subst=[]) ?(metasenv=[]) = + 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 + if t1 === t2 then true else begin @@ -790,34 +795,47 @@ 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.Meta (n1,l1), C.Meta (n2,l2)) -> + | (C.Meta (n1,l1), C.Meta (n2,l2)) -> n1 = n2 && + 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 t1 t2 -> b && 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 +844,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 +856,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 +868,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 +888,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 +899,34 @@ 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 +*) + begin debug t1 [t2] "PREWHD"; - let t1' = whd context t1 in - let t2' = whd context t2 in + (* + (match t1 with + Cic.Meta _ -> + prerr_endline (CicPp.ppterm t1); + prerr_endline (CicPp.ppterm (whd ~subst context t1)); + prerr_endline (CicPp.ppterm t2); + prerr_endline (CicPp.ppterm (whd ~subst context t2)) + | _ -> ()); *) + let t1' = whd ~subst context t1 in + let t2' = whd ~subst context t2 in debug t1' [t2'] "POSTWHD"; - aux2 t1' t2' + aux2 test_equality_only t1' t2' end in - aux + aux false ;;