X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicReductionMachine.ml;h=4b8099fed004c7e92ab152f190b5ca5599fde050;hb=a864255e782859e2b3b7da08297f5d3fe2ee710d;hp=8c1c5017daa6ee5b53877bc7269f49a45fca6675;hpb=a190039db6ffec0912f2a14086109b37396b5fdd;p=helm.git diff --git a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml index 8c1c5017d..4b8099fed 100644 --- a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml +++ b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml @@ -374,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) @@ -498,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 = @@ -542,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) -> @@ -654,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 @@ -722,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 = @@ -769,10 +773,10 @@ module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);; let whd = R.whd;; (* t1, t2 must be well-typed *) -let are_convertible = +let are_convertible ?(subst=[]) ?(metasenv=[]) = 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 @@ -787,34 +791,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 ) @@ -823,7 +840,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 @@ -835,7 +852,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 @@ -847,16 +864,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 @@ -864,8 +884,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 = @@ -874,23 +895,32 @@ 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 ;;