X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicReduction.ml;h=6e34360850caf0f2f5f48f85cee3c65e060833c7;hb=02ae6637b48f03db431e5722243235710957c5b6;hp=32ae57a4709a18ebd35690fbed84564238468ac2;hpb=cc23f034c9419186602d9250456241f2eba90d7c;p=helm.git diff --git a/helm/software/components/cic_proof_checking/cicReduction.ml b/helm/software/components/cic_proof_checking/cicReduction.ml index 32ae57a47..6e3436085 100644 --- a/helm/software/components/cic_proof_checking/cicReduction.ml +++ b/helm/software/components/cic_proof_checking/cicReduction.ml @@ -523,31 +523,7 @@ debug_print (lazy ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri, in C.CoFix (i, substitutedfl) and substaux_in_exp_named_subst params exp_named_subst' m = - (*CSC: Idea di Andrea di ordinare compatibilmente con l'ordine dei params - let ens' = - List.map (function (uri,t) -> uri, unwind_aux m t) exp_named_subst' @ - (*CSC: qui liftiamo tutti gli ens anche se magari me ne servono la meta'!!! *) - List.map (function (uri,t) -> uri, CicSubstitution.lift m t) ens - in - let rec filter_and_lift = - function - [] -> [] - | uri::tl -> - let r = filter_and_lift tl in - (try - (uri,(List.assq uri ens'))::r - with - Not_found -> r - ) - in - filter_and_lift params - *) - - (*CSC: invece di concatenare sarebbe meglio rispettare l'ordine dei params *) - (*CSC: e' vero???? una veloce prova non sembra confermare la teoria *) - - (*CSC: codice copiato e modificato dalla cicSubstitution.subst_vars *) - (*CSC: codice altamente inefficiente *) + (*CSC: codice copiato e modificato dalla cicSubstitution.subst_vars *) let rec filter_and_lift already_instantiated = function [] -> [] @@ -562,18 +538,24 @@ debug_print (lazy ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri, (uri,CicSubstitution.lift m (RS.from_ens_for_unwind ~unwind t)) :: (filter_and_lift (uri::already_instantiated) tl) | _::tl -> filter_and_lift already_instantiated tl -(* - | (uri,_)::tl -> -debug_print (lazy ("---- SKIPPO " ^ UriManager.string_of_uri uri)) ; -if List.for_all (function (uri',_) -> not (UriManager.eq uri uri')) -exp_named_subst' then debug_print (lazy "---- OK1") ; -debug_print (lazy ("++++ uri " ^ UriManager.string_of_uri uri ^ " not in " ^ String.concat " ; " (List.map UriManager.string_of_uri params))) ; -if List.mem uri params then debug_print (lazy "---- OK2") ; - filter_and_lift tl -*) in - List.map (function (uri,t) -> uri, unwind_aux m t) exp_named_subst' @ - (filter_and_lift [] (List.rev ens)) + let res = + List.map (function (uri,t) -> uri, unwind_aux m t) exp_named_subst' @ + (filter_and_lift [] (List.rev ens)) + in + let rec reorder = + function + [] -> [] + | uri::tl -> + let he = + try + [uri,List.assoc uri res] + with + Not_found -> [] + in + he@reorder tl + in + reorder params in unwind_aux m t @@ -887,19 +869,16 @@ prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1); *) aux test_equality_only context t1 term' ugraph with CicUtil.Subst_not_found _ -> false,ugraph) - (* TASSI: CONSTRAINTS *) - | (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only -> - (try - true,(CicUniv.add_eq t2 t1 ugraph) - with CicUniv.UniverseInconsistency _ -> false,ugraph) - (* TASSI: CONSTRAINTS *) - | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> - (try - true,(CicUniv.add_ge t2 t1 ugraph) - with CicUniv.UniverseInconsistency _ -> false,ugraph) - (* TASSI: CONSTRAINTS *) - | (C.Sort s1, C.Sort (C.Type _)) -> (not test_equality_only),ugraph - (* TASSI: CONSTRAINTS *) + | (C.Sort (C.CProp t1|C.Type t1), C.Sort (C.CProp t2|C.Type t2)) + when test_equality_only -> + (try true,(CicUniv.add_eq t2 t1 ugraph) + with CicUniv.UniverseInconsistency _ -> false,ugraph) + | (C.Sort (C.CProp t1|C.Type t1), C.Sort (C.CProp t2|C.Type t2)) + when not test_equality_only -> + (try true,(CicUniv.add_ge t2 t1 ugraph) + with CicUniv.UniverseInconsistency _ -> false,ugraph) + | (C.Sort s1, C.Sort (C.Type _)) + | (C.Sort s1, C.Sort (C.CProp _)) -> (not test_equality_only),ugraph | (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 @@ -909,7 +888,7 @@ prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1); else false,ugraph | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) -> - let b',ugraph' = aux test_equality_only context s1 s2 ugraph in + 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' @@ -927,13 +906,18 @@ prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1); else false,ugraph | (C.Appl l1, C.Appl l2) -> + let b, ugraph = + aux test_equality_only context (List.hd l1) (List.hd l2) ugraph + in + if not b then false, ugraph + else (try List.fold_right2 (fun x y (b,ugraph) -> if b then - aux test_equality_only context x y ugraph + aux true context x y ugraph else - false,ugraph) l1 l2 (true,ugraph) + false,ugraph) (List.tl l1) (List.tl l2) (true,ugraph) with Invalid_argument _ -> false,ugraph ) @@ -996,7 +980,7 @@ prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1); let b'',ugraph''=aux test_equality_only context outtype1 outtype2 ugraph in if b'' then - let b''',ugraph'''= aux test_equality_only context + let b''',ugraph'''= aux true context term1 term2 ugraph'' in List.fold_right2 (fun x y (b,ugraph) -> @@ -1081,7 +1065,7 @@ prerr_endline ("PREWHD: " ^ CicPp.ppterm t1 ^ " <===> " ^ CicPp.ppterm t2); let t2' = whd ?delta:(Some true) ?subst:(Some subst) context t2 in debug t1' [t2'] "POSTWHD"; *) -let rec convert_machines ugraph = +let rec convert_machines test_equality_only ugraph = function [] -> true,ugraph | ((k1,env1,ens1,h1,s1),(k2,env2,ens2,h2,s2))::tl -> @@ -1106,11 +1090,11 @@ let rec convert_machines ugraph = in match problems with None -> false,ugraph - | Some problems -> convert_machines ugraph problems + | Some problems -> convert_machines true ugraph problems else res in - convert_machines ugraph + convert_machines test_equality_only ugraph [R.reduce ~delta:true ~subst context (0,[],[],t1,[]), R.reduce ~delta:true ~subst context (0,[],[],t2,[])] (*prerr_endline ("POSTWH: " ^ CicPp.ppterm t1' ^ " <===> " ^ CicPp.ppterm t2');*)