diff options
Diffstat (limited to 'plugins/funind/rawtermops.ml')
| -rw-r--r-- | plugins/funind/rawtermops.ml | 592 |
1 files changed, 296 insertions, 296 deletions
diff --git a/plugins/funind/rawtermops.ml b/plugins/funind/rawtermops.ml index 92396af59..502960a14 100644 --- a/plugins/funind/rawtermops.ml +++ b/plugins/funind/rawtermops.ml @@ -1,11 +1,11 @@ -open Pp +open Pp open Rawterm open Util open Names (* Ocaml 3.06 Map.S does not handle is_empty *) let idmap_is_empty m = m = Idmap.empty -(* +(* Some basic functions to rebuild rawconstr In each of them the location is Util.dummy_loc *) @@ -24,152 +24,152 @@ let mkRCast(b,t) = RCast(dummy_loc,b,CastConv (Term.DEFAULTcast,t)) Some basic functions to decompose rawconstrs These are analogous to the ones constrs *) -let raw_decompose_prod = - let rec raw_decompose_prod args = function - | RProd(_,n,k,t,b) -> - raw_decompose_prod ((n,t)::args) b +let raw_decompose_prod = + let rec raw_decompose_prod args = function + | RProd(_,n,k,t,b) -> + raw_decompose_prod ((n,t)::args) b | rt -> args,rt in raw_decompose_prod [] -let raw_decompose_prod_or_letin = - let rec raw_decompose_prod args = function - | RProd(_,n,k,t,b) -> - raw_decompose_prod ((n,None,Some t)::args) b - | RLetIn(_,n,t,b) -> - raw_decompose_prod ((n,Some t,None)::args) b +let raw_decompose_prod_or_letin = + let rec raw_decompose_prod args = function + | RProd(_,n,k,t,b) -> + raw_decompose_prod ((n,None,Some t)::args) b + | RLetIn(_,n,t,b) -> + raw_decompose_prod ((n,Some t,None)::args) b | rt -> args,rt in raw_decompose_prod [] -let raw_compose_prod = +let raw_compose_prod = List.fold_left (fun b (n,t) -> mkRProd(n,t,b)) -let raw_compose_prod_or_letin = +let raw_compose_prod_or_letin = List.fold_left ( - fun concl decl -> - match decl with + fun concl decl -> + match decl with | (n,None,Some t) -> mkRProd(n,t,concl) | (n,Some bdy,None) -> mkRLetIn(n,bdy,concl) | _ -> assert false) -let raw_decompose_prod_n n = - let rec raw_decompose_prod i args c = +let raw_decompose_prod_n n = + let rec raw_decompose_prod i args c = if i<=0 then args,c else match c with - | RProd(_,n,_,t,b) -> - raw_decompose_prod (i-1) ((n,t)::args) b + | RProd(_,n,_,t,b) -> + raw_decompose_prod (i-1) ((n,t)::args) b | rt -> args,rt in raw_decompose_prod n [] -let raw_decompose_prod_or_letin_n n = - let rec raw_decompose_prod i args c = +let raw_decompose_prod_or_letin_n n = + let rec raw_decompose_prod i args c = if i<=0 then args,c else match c with - | RProd(_,n,_,t,b) -> - raw_decompose_prod (i-1) ((n,None,Some t)::args) b - | RLetIn(_,n,t,b) -> - raw_decompose_prod (i-1) ((n,Some t,None)::args) b + | RProd(_,n,_,t,b) -> + raw_decompose_prod (i-1) ((n,None,Some t)::args) b + | RLetIn(_,n,t,b) -> + raw_decompose_prod (i-1) ((n,Some t,None)::args) b | rt -> args,rt in raw_decompose_prod n [] -let raw_decompose_app = +let raw_decompose_app = let rec decompose_rapp acc rt = (* msgnl (str "raw_decompose_app on : "++ Printer.pr_rawconstr rt); *) - match rt with - | RApp(_,rt,rtl) -> + match rt with + | RApp(_,rt,rtl) -> decompose_rapp (List.fold_left (fun y x -> x::y) acc rtl) rt | rt -> rt,List.rev acc in - decompose_rapp [] + decompose_rapp [] -(* [raw_make_eq t1 t2] build the rawconstr corresponding to [t2 = t1] *) -let raw_make_eq ?(typ= mkRHole ()) t1 t2 = +(* [raw_make_eq t1 t2] build the rawconstr corresponding to [t2 = t1] *) +let raw_make_eq ?(typ= mkRHole ()) t1 t2 = mkRApp(mkRRef (Lazy.force Coqlib.coq_eq_ref),[typ;t2;t1]) -(* [raw_make_neq t1 t2] build the rawconstr corresponding to [t1 <> t2] *) -let raw_make_neq t1 t2 = +(* [raw_make_neq t1 t2] build the rawconstr corresponding to [t1 <> t2] *) +let raw_make_neq t1 t2 = mkRApp(mkRRef (Lazy.force Coqlib.coq_not_ref),[raw_make_eq t1 t2]) -(* [raw_make_or P1 P2] build the rawconstr corresponding to [P1 \/ P2] *) +(* [raw_make_or P1 P2] build the rawconstr corresponding to [P1 \/ P2] *) let raw_make_or t1 t2 = mkRApp (mkRRef(Lazy.force Coqlib.coq_or_ref),[t1;t2]) -(* [raw_make_or_list [P1;...;Pn]] build the rawconstr corresponding - to [P1 \/ ( .... \/ Pn)] -*) -let rec raw_make_or_list = function +(* [raw_make_or_list [P1;...;Pn]] build the rawconstr corresponding + to [P1 \/ ( .... \/ Pn)] +*) +let rec raw_make_or_list = function | [] -> raise (Invalid_argument "mk_or") | [e] -> e | e::l -> raw_make_or e (raw_make_or_list l) - -let remove_name_from_mapping mapping na = - match na with - | Anonymous -> mapping + +let remove_name_from_mapping mapping na = + match na with + | Anonymous -> mapping | Name id -> Idmap.remove id mapping -let change_vars = - let rec change_vars mapping rt = - match rt with - | RRef _ -> rt - | RVar(loc,id) -> - let new_id = - try - Idmap.find id mapping - with Not_found -> id +let change_vars = + let rec change_vars mapping rt = + match rt with + | RRef _ -> rt + | RVar(loc,id) -> + let new_id = + try + Idmap.find id mapping + with Not_found -> id in RVar(loc,new_id) - | REvar _ -> rt - | RPatVar _ -> rt - | RApp(loc,rt',rtl) -> + | REvar _ -> rt + | RPatVar _ -> rt + | RApp(loc,rt',rtl) -> RApp(loc, change_vars mapping rt', List.map (change_vars mapping) rtl ) - | RLambda(loc,name,k,t,b) -> + | RLambda(loc,name,k,t,b) -> RLambda(loc, name, k, change_vars mapping t, change_vars (remove_name_from_mapping mapping name) b ) - | RProd(loc,name,k,t,b) -> + | RProd(loc,name,k,t,b) -> RProd(loc, name, k, change_vars mapping t, change_vars (remove_name_from_mapping mapping name) b ) - | RLetIn(loc,name,def,b) -> + | RLetIn(loc,name,def,b) -> RLetIn(loc, name, change_vars mapping def, change_vars (remove_name_from_mapping mapping name) b ) - | RLetTuple(loc,nal,(na,rto),b,e) -> - let new_mapping = List.fold_left remove_name_from_mapping mapping nal in + | RLetTuple(loc,nal,(na,rto),b,e) -> + let new_mapping = List.fold_left remove_name_from_mapping mapping nal in RLetTuple(loc, nal, - (na, Option.map (change_vars mapping) rto), - change_vars mapping b, + (na, Option.map (change_vars mapping) rto), + change_vars mapping b, change_vars new_mapping e ) - | RCases(loc,sty,infos,el,brl) -> + | RCases(loc,sty,infos,el,brl) -> RCases(loc,sty, infos, - List.map (fun (e,x) -> (change_vars mapping e,x)) el, + List.map (fun (e,x) -> (change_vars mapping e,x)) el, List.map (change_vars_br mapping) brl ) - | RIf(loc,b,(na,e_option),lhs,rhs) -> + | RIf(loc,b,(na,e_option),lhs,rhs) -> RIf(loc, change_vars mapping b, (na,Option.map (change_vars mapping) e_option), @@ -177,211 +177,211 @@ let change_vars = change_vars mapping rhs ) | RRec _ -> error "Local (co)fixes are not supported" - | RSort _ -> rt - | RHole _ -> rt - | RCast(loc,b,CastConv (k,t)) -> + | RSort _ -> rt + | RHole _ -> rt + | RCast(loc,b,CastConv (k,t)) -> RCast(loc,change_vars mapping b, CastConv (k,change_vars mapping t)) - | RCast(loc,b,CastCoerce) -> + | RCast(loc,b,CastCoerce) -> RCast(loc,change_vars mapping b,CastCoerce) | RDynamic _ -> error "Not handled RDynamic" - and change_vars_br mapping ((loc,idl,patl,res) as br) = - let new_mapping = List.fold_right Idmap.remove idl mapping in - if idmap_is_empty new_mapping - then br + and change_vars_br mapping ((loc,idl,patl,res) as br) = + let new_mapping = List.fold_right Idmap.remove idl mapping in + if idmap_is_empty new_mapping + then br else (loc,idl,patl,change_vars new_mapping res) in - change_vars + change_vars -let rec alpha_pat excluded pat = - match pat with - | PatVar(loc,Anonymous) -> - let new_id = Indfun_common.fresh_id excluded "_x" in +let rec alpha_pat excluded pat = + match pat with + | PatVar(loc,Anonymous) -> + let new_id = Indfun_common.fresh_id excluded "_x" in PatVar(loc,Name new_id),(new_id::excluded),Idmap.empty - | PatVar(loc,Name id) -> - if List.mem id excluded - then - let new_id = Nameops.next_ident_away id excluded in + | PatVar(loc,Name id) -> + if List.mem id excluded + then + let new_id = Nameops.next_ident_away id excluded in PatVar(loc,Name new_id),(new_id::excluded), (Idmap.add id new_id Idmap.empty) else pat,excluded,Idmap.empty - | PatCstr(loc,constr,patl,na) -> - let new_na,new_excluded,map = - match na with - | Name id when List.mem id excluded -> - let new_id = Nameops.next_ident_away id excluded in + | PatCstr(loc,constr,patl,na) -> + let new_na,new_excluded,map = + match na with + | Name id when List.mem id excluded -> + let new_id = Nameops.next_ident_away id excluded in Name new_id,new_id::excluded, Idmap.add id new_id Idmap.empty | _ -> na,excluded,Idmap.empty - in - let new_patl,new_excluded,new_map = - List.fold_left - (fun (patl,excluded,map) pat -> - let new_pat,new_excluded,new_map = alpha_pat excluded pat in + in + let new_patl,new_excluded,new_map = + List.fold_left + (fun (patl,excluded,map) pat -> + let new_pat,new_excluded,new_map = alpha_pat excluded pat in (new_pat::patl,new_excluded,Idmap.fold Idmap.add new_map map) ) ([],new_excluded,map) patl - in + in PatCstr(loc,constr,List.rev new_patl,new_na),new_excluded,new_map -let alpha_patl excluded patl = - let patl,new_excluded,map = - List.fold_left - (fun (patl,excluded,map) pat -> - let new_pat,new_excluded,new_map = alpha_pat excluded pat in +let alpha_patl excluded patl = + let patl,new_excluded,map = + List.fold_left + (fun (patl,excluded,map) pat -> + let new_pat,new_excluded,new_map = alpha_pat excluded pat in new_pat::patl,new_excluded,(Idmap.fold Idmap.add new_map map) ) ([],excluded,Idmap.empty) patl - in + in (List.rev patl,new_excluded,map) - -let raw_get_pattern_id pat acc = - let rec get_pattern_id pat = - match pat with + +let raw_get_pattern_id pat acc = + let rec get_pattern_id pat = + match pat with | PatVar(loc,Anonymous) -> assert false - | PatVar(loc,Name id) -> + | PatVar(loc,Name id) -> [id] - | PatCstr(loc,constr,patternl,_) -> - List.fold_right - (fun pat idl -> - let idl' = get_pattern_id pat in + | PatCstr(loc,constr,patternl,_) -> + List.fold_right + (fun pat idl -> + let idl' = get_pattern_id pat in idl'@idl ) - patternl + patternl [] in (get_pattern_id pat)@acc let get_pattern_id pat = raw_get_pattern_id pat [] - -let rec alpha_rt excluded rt = - let new_rt = - match rt with + +let rec alpha_rt excluded rt = + let new_rt = + match rt with | RRef _ | RVar _ | REvar _ | RPatVar _ -> rt - | RLambda(loc,Anonymous,k,t,b) -> - let new_id = Nameops.next_ident_away (id_of_string "_x") excluded in - let new_excluded = new_id :: excluded in - let new_t = alpha_rt new_excluded t in - let new_b = alpha_rt new_excluded b in + | RLambda(loc,Anonymous,k,t,b) -> + let new_id = Nameops.next_ident_away (id_of_string "_x") excluded in + let new_excluded = new_id :: excluded in + let new_t = alpha_rt new_excluded t in + let new_b = alpha_rt new_excluded b in RLambda(loc,Name new_id,k,new_t,new_b) - | RProd(loc,Anonymous,k,t,b) -> - let new_t = alpha_rt excluded t in - let new_b = alpha_rt excluded b in + | RProd(loc,Anonymous,k,t,b) -> + let new_t = alpha_rt excluded t in + let new_b = alpha_rt excluded b in RProd(loc,Anonymous,k,new_t,new_b) - | RLetIn(loc,Anonymous,t,b) -> - let new_t = alpha_rt excluded t in - let new_b = alpha_rt excluded b in + | RLetIn(loc,Anonymous,t,b) -> + let new_t = alpha_rt excluded t in + let new_b = alpha_rt excluded b in RLetIn(loc,Anonymous,new_t,new_b) - | RLambda(loc,Name id,k,t,b) -> - let new_id = Nameops.next_ident_away id excluded in - let t,b = - if new_id = id + | RLambda(loc,Name id,k,t,b) -> + let new_id = Nameops.next_ident_away id excluded in + let t,b = + if new_id = id then t,b - else - let replace = change_vars (Idmap.add id new_id Idmap.empty) in + else + let replace = change_vars (Idmap.add id new_id Idmap.empty) in (t,replace b) in - let new_excluded = new_id::excluded in - let new_t = alpha_rt new_excluded t in - let new_b = alpha_rt new_excluded b in + let new_excluded = new_id::excluded in + let new_t = alpha_rt new_excluded t in + let new_b = alpha_rt new_excluded b in RLambda(loc,Name new_id,k,new_t,new_b) - | RProd(loc,Name id,k,t,b) -> - let new_id = Nameops.next_ident_away id excluded in - let new_excluded = new_id::excluded in - let t,b = - if new_id = id + | RProd(loc,Name id,k,t,b) -> + let new_id = Nameops.next_ident_away id excluded in + let new_excluded = new_id::excluded in + let t,b = + if new_id = id then t,b - else - let replace = change_vars (Idmap.add id new_id Idmap.empty) in + else + let replace = change_vars (Idmap.add id new_id Idmap.empty) in (t,replace b) in - let new_t = alpha_rt new_excluded t in - let new_b = alpha_rt new_excluded b in + let new_t = alpha_rt new_excluded t in + let new_b = alpha_rt new_excluded b in RProd(loc,Name new_id,k,new_t,new_b) - | RLetIn(loc,Name id,t,b) -> - let new_id = Nameops.next_ident_away id excluded in - let t,b = - if new_id = id + | RLetIn(loc,Name id,t,b) -> + let new_id = Nameops.next_ident_away id excluded in + let t,b = + if new_id = id then t,b - else - let replace = change_vars (Idmap.add id new_id Idmap.empty) in + else + let replace = change_vars (Idmap.add id new_id Idmap.empty) in (t,replace b) in - let new_excluded = new_id::excluded in - let new_t = alpha_rt new_excluded t in - let new_b = alpha_rt new_excluded b in + let new_excluded = new_id::excluded in + let new_t = alpha_rt new_excluded t in + let new_b = alpha_rt new_excluded b in RLetIn(loc,Name new_id,new_t,new_b) - | RLetTuple(loc,nal,(na,rto),t,b) -> - let rev_new_nal,new_excluded,mapping = - List.fold_left - (fun (nal,excluded,mapping) na -> - match na with + | RLetTuple(loc,nal,(na,rto),t,b) -> + let rev_new_nal,new_excluded,mapping = + List.fold_left + (fun (nal,excluded,mapping) na -> + match na with | Anonymous -> (na::nal,excluded,mapping) - | Name id -> - let new_id = Nameops.next_ident_away id excluded in - if new_id = id - then - na::nal,id::excluded,mapping - else + | Name id -> + let new_id = Nameops.next_ident_away id excluded in + if new_id = id + then + na::nal,id::excluded,mapping + else (Name new_id)::nal,id::excluded,(Idmap.add id new_id mapping) ) ([],excluded,Idmap.empty) nal in - let new_nal = List.rev rev_new_nal in - let new_rto,new_t,new_b = + let new_nal = List.rev rev_new_nal in + let new_rto,new_t,new_b = if idmap_is_empty mapping then rto,t,b - else let replace = change_vars mapping in + else let replace = change_vars mapping in (Option.map replace rto, t,replace b) in - let new_t = alpha_rt new_excluded new_t in - let new_b = alpha_rt new_excluded new_b in + let new_t = alpha_rt new_excluded new_t in + let new_b = alpha_rt new_excluded new_b in let new_rto = Option.map (alpha_rt new_excluded) new_rto in RLetTuple(loc,new_nal,(na,new_rto),new_t,new_b) - | RCases(loc,sty,infos,el,brl) -> - let new_el = - List.map (function (rt,i) -> alpha_rt excluded rt, i) el - in - RCases(loc,sty,infos,new_el,List.map (alpha_br excluded) brl) - | RIf(loc,b,(na,e_o),lhs,rhs) -> + | RCases(loc,sty,infos,el,brl) -> + let new_el = + List.map (function (rt,i) -> alpha_rt excluded rt, i) el + in + RCases(loc,sty,infos,new_el,List.map (alpha_br excluded) brl) + | RIf(loc,b,(na,e_o),lhs,rhs) -> RIf(loc,alpha_rt excluded b, (na,Option.map (alpha_rt excluded) e_o), alpha_rt excluded lhs, alpha_rt excluded rhs ) | RRec _ -> error "Not handled RRec" - | RSort _ -> rt - | RHole _ -> rt - | RCast (loc,b,CastConv (k,t)) -> + | RSort _ -> rt + | RHole _ -> rt + | RCast (loc,b,CastConv (k,t)) -> RCast(loc,alpha_rt excluded b,CastConv(k,alpha_rt excluded t)) - | RCast (loc,b,CastCoerce) -> + | RCast (loc,b,CastCoerce) -> RCast(loc,alpha_rt excluded b,CastCoerce) | RDynamic _ -> error "Not handled RDynamic" - | RApp(loc,f,args) -> + | RApp(loc,f,args) -> RApp(loc, alpha_rt excluded f, List.map (alpha_rt excluded) args ) - in + in new_rt -and alpha_br excluded (loc,ids,patl,res) = - let new_patl,new_excluded,mapping = alpha_patl excluded patl in - let new_ids = List.fold_right raw_get_pattern_id new_patl [] in - let new_excluded = new_ids@excluded in - let renamed_res = change_vars mapping res in - let new_res = alpha_rt new_excluded renamed_res in +and alpha_br excluded (loc,ids,patl,res) = + let new_patl,new_excluded,mapping = alpha_patl excluded patl in + let new_ids = List.fold_right raw_get_pattern_id new_patl [] in + let new_excluded = new_ids@excluded in + let renamed_res = change_vars mapping res in + let new_res = alpha_rt new_excluded renamed_res in (loc,new_ids,new_patl,new_res) - -(* + +(* [is_free_in id rt] checks if [id] is a free variable in [rt] *) let is_free_in id = @@ -401,12 +401,12 @@ let is_free_in id = | RCases(_,_,_,el,brl) -> (List.exists (fun (e,_) -> is_free_in e) el) || List.exists is_free_in_br brl - | RLetTuple(_,nal,_,b,t) -> - let check_in_nal = - not (List.exists (function Name id' -> id'= id | _ -> false) nal) - in + | RLetTuple(_,nal,_,b,t) -> + let check_in_nal = + not (List.exists (function Name id' -> id'= id | _ -> false) nal) + in is_free_in t || (check_in_nal && is_free_in b) - + | RIf(_,cond,_,br1,br2) -> is_free_in cond || is_free_in br1 || is_free_in br2 | RRec _ -> raise (UserError("",str "Not handled RRec")) @@ -419,7 +419,7 @@ let is_free_in id = (not (List.mem id ids)) && is_free_in rt in is_free_in - + let rec pattern_to_term = function @@ -446,23 +446,23 @@ let rec pattern_to_term = function implicit_args@patl_as_term ) - -let replace_var_by_term x_id term = - let rec replace_var_by_pattern rt = - match rt with - | RRef _ -> rt + +let replace_var_by_term x_id term = + let rec replace_var_by_pattern rt = + match rt with + | RRef _ -> rt | RVar(_,id) when id_ord id x_id == 0 -> term - | RVar _ -> rt - | REvar _ -> rt - | RPatVar _ -> rt - | RApp(loc,rt',rtl) -> + | RVar _ -> rt + | REvar _ -> rt + | RPatVar _ -> rt + | RApp(loc,rt',rtl) -> RApp(loc, replace_var_by_pattern rt', List.map replace_var_by_pattern rtl ) | RLambda(_,Name id,_,_,_) when id_ord id x_id == 0 -> rt - | RLambda(loc,name,k,t,b) -> + | RLambda(loc,name,k,t,b) -> RLambda(loc, name, k, @@ -470,7 +470,7 @@ let replace_var_by_term x_id term = replace_var_by_pattern b ) | RProd(_,Name id,_,_,_) when id_ord id x_id == 0 -> rt - | RProd(loc,name,k,t,b) -> + | RProd(loc,name,k,t,b) -> RProd(loc, name, k, @@ -478,94 +478,94 @@ let replace_var_by_term x_id term = replace_var_by_pattern b ) | RLetIn(_,Name id,_,_) when id_ord id x_id == 0 -> rt - | RLetIn(loc,name,def,b) -> + | RLetIn(loc,name,def,b) -> RLetIn(loc, name, replace_var_by_pattern def, replace_var_by_pattern b ) - | RLetTuple(_,nal,_,_,_) - when List.exists (function Name id -> id = x_id | _ -> false) nal -> + | RLetTuple(_,nal,_,_,_) + when List.exists (function Name id -> id = x_id | _ -> false) nal -> rt - | RLetTuple(loc,nal,(na,rto),def,b) -> + | RLetTuple(loc,nal,(na,rto),def,b) -> RLetTuple(loc, nal, (na,Option.map replace_var_by_pattern rto), replace_var_by_pattern def, replace_var_by_pattern b ) - | RCases(loc,sty,infos,el,brl) -> + | RCases(loc,sty,infos,el,brl) -> RCases(loc,sty, infos, - List.map (fun (e,x) -> (replace_var_by_pattern e,x)) el, + List.map (fun (e,x) -> (replace_var_by_pattern e,x)) el, List.map replace_var_by_pattern_br brl ) - | RIf(loc,b,(na,e_option),lhs,rhs) -> + | RIf(loc,b,(na,e_option),lhs,rhs) -> RIf(loc, replace_var_by_pattern b, (na,Option.map replace_var_by_pattern e_option), replace_var_by_pattern lhs, replace_var_by_pattern rhs ) | RRec _ -> raise (UserError("",str "Not handled RRec")) - | RSort _ -> rt - | RHole _ -> rt - | RCast(loc,b,CastConv(k,t)) -> + | RSort _ -> rt + | RHole _ -> rt + | RCast(loc,b,CastConv(k,t)) -> RCast(loc,replace_var_by_pattern b,CastConv(k,replace_var_by_pattern t)) - | RCast(loc,b,CastCoerce) -> + | RCast(loc,b,CastCoerce) -> RCast(loc,replace_var_by_pattern b,CastCoerce) | RDynamic _ -> raise (UserError("",str "Not handled RDynamic")) - and replace_var_by_pattern_br ((loc,idl,patl,res) as br) = - if List.exists (fun id -> id_ord id x_id == 0) idl - then br + and replace_var_by_pattern_br ((loc,idl,patl,res) as br) = + if List.exists (fun id -> id_ord id x_id == 0) idl + then br else (loc,idl,patl,replace_var_by_pattern res) in - replace_var_by_pattern + replace_var_by_pattern -(* checking unifiability of patterns *) -exception NotUnifiable +(* checking unifiability of patterns *) +exception NotUnifiable -let rec are_unifiable_aux = function - | [] -> () - | eq::eqs -> - match eq with - | PatVar _,_ | _,PatVar _ -> are_unifiable_aux eqs - | PatCstr(_,constructor1,cpl1,_),PatCstr(_,constructor2,cpl2,_) -> - if constructor2 <> constructor1 +let rec are_unifiable_aux = function + | [] -> () + | eq::eqs -> + match eq with + | PatVar _,_ | _,PatVar _ -> are_unifiable_aux eqs + | PatCstr(_,constructor1,cpl1,_),PatCstr(_,constructor2,cpl2,_) -> + if constructor2 <> constructor1 then raise NotUnifiable - else - let eqs' = + else + let eqs' = try ((List.combine cpl1 cpl2)@eqs) - with _ -> anomaly "are_unifiable_aux" + with _ -> anomaly "are_unifiable_aux" in are_unifiable_aux eqs' - -let are_unifiable pat1 pat2 = - try + +let are_unifiable pat1 pat2 = + try are_unifiable_aux [pat1,pat2]; true with NotUnifiable -> false -let rec eq_cases_pattern_aux = function - | [] -> () - | eq::eqs -> - match eq with - | PatVar _,PatVar _ -> eq_cases_pattern_aux eqs - | PatCstr(_,constructor1,cpl1,_),PatCstr(_,constructor2,cpl2,_) -> - if constructor2 <> constructor1 +let rec eq_cases_pattern_aux = function + | [] -> () + | eq::eqs -> + match eq with + | PatVar _,PatVar _ -> eq_cases_pattern_aux eqs + | PatCstr(_,constructor1,cpl1,_),PatCstr(_,constructor2,cpl2,_) -> + if constructor2 <> constructor1 then raise NotUnifiable - else - let eqs' = + else + let eqs' = try ((List.combine cpl1 cpl2)@eqs) - with _ -> anomaly "eq_cases_pattern_aux" + with _ -> anomaly "eq_cases_pattern_aux" in eq_cases_pattern_aux eqs' | _ -> raise NotUnifiable -let eq_cases_pattern pat1 pat2 = +let eq_cases_pattern pat1 pat2 = try eq_cases_pattern_aux [pat1,pat2]; true @@ -573,25 +573,25 @@ let eq_cases_pattern pat1 pat2 = -let ids_of_pat = - let rec ids_of_pat ids = function - | PatVar(_,Anonymous) -> ids - | PatVar(_,Name id) -> Idset.add id ids +let ids_of_pat = + let rec ids_of_pat ids = function + | PatVar(_,Anonymous) -> ids + | PatVar(_,Name id) -> Idset.add id ids | PatCstr(_,_,patl,_) -> List.fold_left ids_of_pat ids patl in - ids_of_pat Idset.empty - -let id_of_name = function - | Names.Anonymous -> id_of_string "x" + ids_of_pat Idset.empty + +let id_of_name = function + | Names.Anonymous -> id_of_string "x" | Names.Name x -> x (* TODO: finish Rec caes *) -let ids_of_rawterm c = - let rec ids_of_rawterm acc c = +let ids_of_rawterm c = + let rec ids_of_rawterm acc c = let idof = id_of_name in match c with | RVar (_,id) -> id::acc - | RApp (loc,g,args) -> + | RApp (loc,g,args) -> ids_of_rawterm [] g @ List.flatten (List.map (ids_of_rawterm []) args) @ acc | RLambda (loc,na,k,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc | RProd (loc,na,k,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc @@ -599,101 +599,101 @@ let ids_of_rawterm c = | RCast (loc,c,CastConv(k,t)) -> ids_of_rawterm [] c @ ids_of_rawterm [] t @ acc | RCast (loc,c,CastCoerce) -> ids_of_rawterm [] c @ acc | RIf (loc,c,(na,po),b1,b2) -> ids_of_rawterm [] c @ ids_of_rawterm [] b1 @ ids_of_rawterm [] b2 @ acc - | RLetTuple (_,nal,(na,po),b,c) -> + | RLetTuple (_,nal,(na,po),b,c) -> List.map idof nal @ ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc - | RCases (loc,sty,rtntypopt,tml,brchl) -> + | RCases (loc,sty,rtntypopt,tml,brchl) -> List.flatten (List.map (fun (_,idl,patl,c) -> idl @ ids_of_rawterm [] c) brchl) | RRec _ -> failwith "Fix inside a constructor branch" | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> [] in (* build the set *) List.fold_left (fun acc x -> Idset.add x acc) Idset.empty (ids_of_rawterm [] c) - -let zeta_normalize = - let rec zeta_normalize_term rt = - match rt with - | RRef _ -> rt - | RVar _ -> rt - | REvar _ -> rt - | RPatVar _ -> rt - | RApp(loc,rt',rtl) -> + +let zeta_normalize = + let rec zeta_normalize_term rt = + match rt with + | RRef _ -> rt + | RVar _ -> rt + | REvar _ -> rt + | RPatVar _ -> rt + | RApp(loc,rt',rtl) -> RApp(loc, zeta_normalize_term rt', List.map zeta_normalize_term rtl ) - | RLambda(loc,name,k,t,b) -> + | RLambda(loc,name,k,t,b) -> RLambda(loc, name, k, zeta_normalize_term t, zeta_normalize_term b ) - | RProd(loc,name,k,t,b) -> + | RProd(loc,name,k,t,b) -> RProd(loc, - name, + name, k, zeta_normalize_term t, zeta_normalize_term b ) - | RLetIn(_,Name id,def,b) -> + | RLetIn(_,Name id,def,b) -> zeta_normalize_term (replace_var_by_term id def b) | RLetIn(loc,Anonymous,def,b) -> zeta_normalize_term b - | RLetTuple(loc,nal,(na,rto),def,b) -> + | RLetTuple(loc,nal,(na,rto),def,b) -> RLetTuple(loc, nal, (na,Option.map zeta_normalize_term rto), zeta_normalize_term def, zeta_normalize_term b ) - | RCases(loc,sty,infos,el,brl) -> + | RCases(loc,sty,infos,el,brl) -> RCases(loc,sty, infos, - List.map (fun (e,x) -> (zeta_normalize_term e,x)) el, + List.map (fun (e,x) -> (zeta_normalize_term e,x)) el, List.map zeta_normalize_br brl ) - | RIf(loc,b,(na,e_option),lhs,rhs) -> + | RIf(loc,b,(na,e_option),lhs,rhs) -> RIf(loc, zeta_normalize_term b, (na,Option.map zeta_normalize_term e_option), zeta_normalize_term lhs, zeta_normalize_term rhs ) | RRec _ -> raise (UserError("",str "Not handled RRec")) - | RSort _ -> rt - | RHole _ -> rt - | RCast(loc,b,CastConv(k,t)) -> + | RSort _ -> rt + | RHole _ -> rt + | RCast(loc,b,CastConv(k,t)) -> RCast(loc,zeta_normalize_term b,CastConv(k,zeta_normalize_term t)) - | RCast(loc,b,CastCoerce) -> + | RCast(loc,b,CastCoerce) -> RCast(loc,zeta_normalize_term b,CastCoerce) | RDynamic _ -> raise (UserError("",str "Not handled RDynamic")) - and zeta_normalize_br (loc,idl,patl,res) = + and zeta_normalize_br (loc,idl,patl,res) = (loc,idl,patl,zeta_normalize_term res) in - zeta_normalize_term + zeta_normalize_term -let expand_as = - - let rec add_as map pat = - match pat with - | PatVar _ -> map - | PatCstr(_,_,patl,Name id) -> +let expand_as = + + let rec add_as map pat = + match pat with + | PatVar _ -> map + | PatCstr(_,_,patl,Name id) -> Idmap.add id (pattern_to_term pat) (List.fold_left add_as map patl) | PatCstr(_,_,patl,_) -> List.fold_left add_as map patl - in - let rec expand_as map rt = - match rt with - | RRef _ | REvar _ | RPatVar _ | RSort _ | RHole _ -> rt - | RVar(_,id) -> + in + let rec expand_as map rt = + match rt with + | RRef _ | REvar _ | RPatVar _ | RSort _ | RHole _ -> rt + | RVar(_,id) -> begin - try + try Idmap.find id map - with Not_found -> rt + with Not_found -> rt end | RApp(loc,f,args) -> RApp(loc,expand_as map f,List.map (expand_as map) args) | RLambda(loc,na,k,t,b) -> RLambda(loc,na,k,expand_as map t, expand_as map b) @@ -712,7 +712,7 @@ let expand_as = | RCases(loc,sty,po,el,brl) -> RCases(loc, sty, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el, List.map (expand_as_br map) brl) - and expand_as_br map (loc,idl,cpl,rt) = + and expand_as_br map (loc,idl,cpl,rt) = (loc,idl,cpl, expand_as (List.fold_left add_as map cpl) rt) in - expand_as Idmap.empty + expand_as Idmap.empty |