diff options
Diffstat (limited to 'plugins/funind/rawtermops.ml')
| -rw-r--r-- | plugins/funind/rawtermops.ml | 416 |
1 files changed, 208 insertions, 208 deletions
diff --git a/plugins/funind/rawtermops.ml b/plugins/funind/rawtermops.ml index e31f1452d..f372fb017 100644 --- a/plugins/funind/rawtermops.ml +++ b/plugins/funind/rawtermops.ml @@ -6,46 +6,46 @@ open Names let idmap_is_empty m = m = Idmap.empty (* - Some basic functions to rebuild rawconstr + Some basic functions to rebuild glob_constr In each of them the location is Util.dummy_loc *) -let mkRRef ref = RRef(dummy_loc,ref) -let mkRVar id = RVar(dummy_loc,id) -let mkRApp(rt,rtl) = RApp(dummy_loc,rt,rtl) -let mkRLambda(n,t,b) = RLambda(dummy_loc,n,Explicit,t,b) -let mkRProd(n,t,b) = RProd(dummy_loc,n,Explicit,t,b) -let mkRLetIn(n,t,b) = RLetIn(dummy_loc,n,t,b) -let mkRCases(rto,l,brl) = RCases(dummy_loc,Term.RegularStyle,rto,l,brl) -let mkRSort s = RSort(dummy_loc,s) -let mkRHole () = RHole(dummy_loc,Evd.BinderType Anonymous) -let mkRCast(b,t) = RCast(dummy_loc,b,CastConv (Term.DEFAULTcast,t)) +let mkRRef ref = GRef(dummy_loc,ref) +let mkRVar id = GVar(dummy_loc,id) +let mkRApp(rt,rtl) = GApp(dummy_loc,rt,rtl) +let mkRLambda(n,t,b) = GLambda(dummy_loc,n,Explicit,t,b) +let mkRProd(n,t,b) = GProd(dummy_loc,n,Explicit,t,b) +let mkRLetIn(n,t,b) = GLetIn(dummy_loc,n,t,b) +let mkRCases(rto,l,brl) = GCases(dummy_loc,Term.RegularStyle,rto,l,brl) +let mkRSort s = GSort(dummy_loc,s) +let mkRHole () = GHole(dummy_loc,Evd.BinderType Anonymous) +let mkRCast(b,t) = GCast(dummy_loc,b,CastConv (Term.DEFAULTcast,t)) (* - Some basic functions to decompose rawconstrs + Some basic functions to decompose glob_constrs 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 glob_decompose_prod = + let rec glob_decompose_prod args = function + | GProd(_,n,k,t,b) -> + glob_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 + glob_decompose_prod [] + +let glob_decompose_prod_or_letin = + let rec glob_decompose_prod args = function + | GProd(_,n,k,t,b) -> + glob_decompose_prod ((n,None,Some t)::args) b + | GLetIn(_,n,t,b) -> + glob_decompose_prod ((n,Some t,None)::args) b | rt -> args,rt in - raw_decompose_prod [] + glob_decompose_prod [] -let raw_compose_prod = +let glob_compose_prod = List.fold_left (fun b (n,t) -> mkRProd(n,t,b)) -let raw_compose_prod_or_letin = +let glob_compose_prod_or_letin = List.fold_left ( fun concl decl -> match decl with @@ -53,37 +53,37 @@ let raw_compose_prod_or_letin = | (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 glob_decompose_prod_n n = + let rec glob_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 + | GProd(_,n,_,t,b) -> + glob_decompose_prod (i-1) ((n,t)::args) b | rt -> args,rt in - raw_decompose_prod n [] + glob_decompose_prod n [] -let raw_decompose_prod_or_letin_n n = - let rec raw_decompose_prod i args c = +let glob_decompose_prod_or_letin_n n = + let rec glob_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 + | GProd(_,n,_,t,b) -> + glob_decompose_prod (i-1) ((n,None,Some t)::args) b + | GLetIn(_,n,t,b) -> + glob_decompose_prod (i-1) ((n,Some t,None)::args) b | rt -> args,rt in - raw_decompose_prod n [] + glob_decompose_prod n [] -let raw_decompose_app = +let glob_decompose_app = let rec decompose_rapp acc rt = -(* msgnl (str "raw_decompose_app on : "++ Printer.pr_rawconstr rt); *) +(* msgnl (str "glob_decompose_app on : "++ Printer.pr_glob_constr rt); *) match rt with - | RApp(_,rt,rtl) -> + | GApp(_,rt,rtl) -> decompose_rapp (List.fold_left (fun y x -> x::y) acc rtl) rt | rt -> rt,List.rev acc in @@ -92,24 +92,24 @@ let raw_decompose_app = -(* [raw_make_eq t1 t2] build the rawconstr corresponding to [t2 = t1] *) -let raw_make_eq ?(typ= mkRHole ()) t1 t2 = +(* [glob_make_eq t1 t2] build the glob_constr corresponding to [t2 = t1] *) +let glob_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 = - mkRApp(mkRRef (Lazy.force Coqlib.coq_not_ref),[raw_make_eq t1 t2]) +(* [glob_make_neq t1 t2] build the glob_constr corresponding to [t1 <> t2] *) +let glob_make_neq t1 t2 = + mkRApp(mkRRef (Lazy.force Coqlib.coq_not_ref),[glob_make_eq t1 t2]) -(* [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]) +(* [glob_make_or P1 P2] build the glob_constr corresponding to [P1 \/ P2] *) +let glob_make_or t1 t2 = mkRApp (mkRRef(Lazy.force Coqlib.coq_or_ref),[t1;t2]) -(* [raw_make_or_list [P1;...;Pn]] build the rawconstr corresponding +(* [glob_make_or_list [P1;...;Pn]] build the glob_constr corresponding to [P1 \/ ( .... \/ Pn)] *) -let rec raw_make_or_list = function +let rec glob_make_or_list = function | [] -> raise (Invalid_argument "mk_or") | [e] -> e - | e::l -> raw_make_or e (raw_make_or_list l) + | e::l -> glob_make_or e (glob_make_or_list l) let remove_name_from_mapping mapping na = @@ -120,70 +120,70 @@ let remove_name_from_mapping mapping na = let change_vars = let rec change_vars mapping rt = match rt with - | RRef _ -> rt - | RVar(loc,id) -> + | GRef _ -> rt + | GVar(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) -> - RApp(loc, + GVar(loc,new_id) + | GEvar _ -> rt + | GPatVar _ -> rt + | GApp(loc,rt',rtl) -> + GApp(loc, change_vars mapping rt', List.map (change_vars mapping) rtl ) - | RLambda(loc,name,k,t,b) -> - RLambda(loc, + | GLambda(loc,name,k,t,b) -> + GLambda(loc, name, k, change_vars mapping t, change_vars (remove_name_from_mapping mapping name) b ) - | RProd(loc,name,k,t,b) -> - RProd(loc, + | GProd(loc,name,k,t,b) -> + GProd(loc, name, k, change_vars mapping t, change_vars (remove_name_from_mapping mapping name) b ) - | RLetIn(loc,name,def,b) -> - RLetIn(loc, + | GLetIn(loc,name,def,b) -> + GLetIn(loc, name, change_vars mapping def, change_vars (remove_name_from_mapping mapping name) b ) - | RLetTuple(loc,nal,(na,rto),b,e) -> + | GLetTuple(loc,nal,(na,rto),b,e) -> let new_mapping = List.fold_left remove_name_from_mapping mapping nal in - RLetTuple(loc, + GLetTuple(loc, nal, (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, + | GCases(loc,sty,infos,el,brl) -> + GCases(loc,sty, infos, 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, + | GIf(loc,b,(na,e_option),lhs,rhs) -> + GIf(loc, change_vars mapping b, (na,Option.map (change_vars mapping) e_option), change_vars mapping lhs, change_vars mapping rhs ) - | RRec _ -> error "Local (co)fixes are not supported" - | 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,change_vars mapping b,CastCoerce) - | RDynamic _ -> error "Not handled RDynamic" + | GRec _ -> error "Local (co)fixes are not supported" + | GSort _ -> rt + | GHole _ -> rt + | GCast(loc,b,CastConv (k,t)) -> + GCast(loc,change_vars mapping b, CastConv (k,change_vars mapping t)) + | GCast(loc,b,CastCoerce) -> + GCast(loc,change_vars mapping b,CastCoerce) + | GDynamic _ -> error "Not handled GDynamic" 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 @@ -262,22 +262,22 @@ let get_pattern_id pat = raw_get_pattern_id pat [] let rec alpha_rt excluded rt = let new_rt = match rt with - | RRef _ | RVar _ | REvar _ | RPatVar _ -> rt - | RLambda(loc,Anonymous,k,t,b) -> + | GRef _ | GVar _ | GEvar _ | GPatVar _ -> rt + | GLambda(loc,Anonymous,k,t,b) -> let new_id = Namegen.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) -> + GLambda(loc,Name new_id,k,new_t,new_b) + | GProd(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) -> + GProd(loc,Anonymous,k,new_t,new_b) + | GLetIn(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) -> + GLetIn(loc,Anonymous,new_t,new_b) + | GLambda(loc,Name id,k,t,b) -> let new_id = Namegen.next_ident_away id excluded in let t,b = if new_id = id @@ -289,8 +289,8 @@ let rec alpha_rt excluded rt = 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) -> + GLambda(loc,Name new_id,k,new_t,new_b) + | GProd(loc,Name id,k,t,b) -> let new_id = Namegen.next_ident_away id excluded in let new_excluded = new_id::excluded in let t,b = @@ -302,8 +302,8 @@ let rec alpha_rt excluded rt = 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) -> + GProd(loc,Name new_id,k,new_t,new_b) + | GLetIn(loc,Name id,t,b) -> let new_id = Namegen.next_ident_away id excluded in let t,b = if new_id = id @@ -315,10 +315,10 @@ let rec alpha_rt excluded rt = 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) + GLetIn(loc,Name new_id,new_t,new_b) - | RLetTuple(loc,nal,(na,rto),t,b) -> + | GLetTuple(loc,nal,(na,rto),t,b) -> let rev_new_nal,new_excluded,mapping = List.fold_left (fun (nal,excluded,mapping) na -> @@ -345,28 +345,28 @@ let rec alpha_rt excluded rt = 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) -> + GLetTuple(loc,new_nal,(na,new_rto),new_t,new_b) + | GCases(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, + GCases(loc,sty,infos,new_el,List.map (alpha_br excluded) brl) + | GIf(loc,b,(na,e_o),lhs,rhs) -> + GIf(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)) -> - RCast(loc,alpha_rt excluded b,CastConv(k,alpha_rt excluded t)) - | RCast (loc,b,CastCoerce) -> - RCast(loc,alpha_rt excluded b,CastCoerce) - | RDynamic _ -> error "Not handled RDynamic" - | RApp(loc,f,args) -> - RApp(loc, + | GRec _ -> error "Not handled GRec" + | GSort _ -> rt + | GHole _ -> rt + | GCast (loc,b,CastConv (k,t)) -> + GCast(loc,alpha_rt excluded b,CastConv(k,alpha_rt excluded t)) + | GCast (loc,b,CastCoerce) -> + GCast(loc,alpha_rt excluded b,CastCoerce) + | GDynamic _ -> error "Not handled GDynamic" + | GApp(loc,f,args) -> + GApp(loc, alpha_rt excluded f, List.map (alpha_rt excluded) args ) @@ -386,35 +386,35 @@ and alpha_br excluded (loc,ids,patl,res) = *) let is_free_in id = let rec is_free_in = function - | RRef _ -> false - | RVar(_,id') -> id_ord id' id == 0 - | REvar _ -> false - | RPatVar _ -> false - | RApp(_,rt,rtl) -> List.exists is_free_in (rt::rtl) - | RLambda(_,n,_,t,b) | RProd(_,n,_,t,b) | RLetIn(_,n,t,b) -> + | GRef _ -> false + | GVar(_,id') -> id_ord id' id == 0 + | GEvar _ -> false + | GPatVar _ -> false + | GApp(_,rt,rtl) -> List.exists is_free_in (rt::rtl) + | GLambda(_,n,_,t,b) | GProd(_,n,_,t,b) | GLetIn(_,n,t,b) -> let check_in_b = match n with | Name id' -> id_ord id' id <> 0 | _ -> true in is_free_in t || (check_in_b && is_free_in b) - | RCases(_,_,_,el,brl) -> + | GCases(_,_,_,el,brl) -> (List.exists (fun (e,_) -> is_free_in e) el) || List.exists is_free_in_br brl - | RLetTuple(_,nal,_,b,t) -> + | GLetTuple(_,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) -> + | GIf(_,cond,_,br1,br2) -> is_free_in cond || is_free_in br1 || is_free_in br2 - | RRec _ -> raise (UserError("",str "Not handled RRec")) - | RSort _ -> false - | RHole _ -> false - | RCast (_,b,CastConv (_,t)) -> is_free_in b || is_free_in t - | RCast (_,b,CastCoerce) -> is_free_in b - | RDynamic _ -> raise (UserError("",str "Not handled RDynamic")) + | GRec _ -> raise (UserError("",str "Not handled GRec")) + | GSort _ -> false + | GHole _ -> false + | GCast (_,b,CastConv (_,t)) -> is_free_in b || is_free_in t + | GCast (_,b,CastCoerce) -> is_free_in b + | GDynamic _ -> raise (UserError("",str "Not handled GDynamic")) and is_free_in_br (_,ids,_,rt) = (not (List.mem id ids)) && is_free_in rt in @@ -451,69 +451,69 @@ let rec pattern_to_term = function 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) -> - RApp(loc, + | GRef _ -> rt + | GVar(_,id) when id_ord id x_id == 0 -> term + | GVar _ -> rt + | GEvar _ -> rt + | GPatVar _ -> rt + | GApp(loc,rt',rtl) -> + GApp(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, + | GLambda(_,Name id,_,_,_) when id_ord id x_id == 0 -> rt + | GLambda(loc,name,k,t,b) -> + GLambda(loc, name, k, replace_var_by_pattern t, replace_var_by_pattern b ) - | RProd(_,Name id,_,_,_) when id_ord id x_id == 0 -> rt - | RProd(loc,name,k,t,b) -> - RProd(loc, + | GProd(_,Name id,_,_,_) when id_ord id x_id == 0 -> rt + | GProd(loc,name,k,t,b) -> + GProd(loc, name, k, replace_var_by_pattern t, replace_var_by_pattern b ) - | RLetIn(_,Name id,_,_) when id_ord id x_id == 0 -> rt - | RLetIn(loc,name,def,b) -> - RLetIn(loc, + | GLetIn(_,Name id,_,_) when id_ord id x_id == 0 -> rt + | GLetIn(loc,name,def,b) -> + GLetIn(loc, name, replace_var_by_pattern def, replace_var_by_pattern b ) - | RLetTuple(_,nal,_,_,_) + | GLetTuple(_,nal,_,_,_) when List.exists (function Name id -> id = x_id | _ -> false) nal -> rt - | RLetTuple(loc,nal,(na,rto),def,b) -> - RLetTuple(loc, + | GLetTuple(loc,nal,(na,rto),def,b) -> + GLetTuple(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, + | GCases(loc,sty,infos,el,brl) -> + GCases(loc,sty, infos, 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, replace_var_by_pattern b, + | GIf(loc,b,(na,e_option),lhs,rhs) -> + GIf(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)) -> - RCast(loc,replace_var_by_pattern b,CastConv(k,replace_var_by_pattern t)) - | RCast(loc,b,CastCoerce) -> - RCast(loc,replace_var_by_pattern b,CastCoerce) - | RDynamic _ -> raise (UserError("",str "Not handled RDynamic")) + | GRec _ -> raise (UserError("",str "Not handled GRec")) + | GSort _ -> rt + | GHole _ -> rt + | GCast(loc,b,CastConv(k,t)) -> + GCast(loc,replace_var_by_pattern b,CastConv(k,replace_var_by_pattern t)) + | GCast(loc,b,CastCoerce) -> + GCast(loc,replace_var_by_pattern b,CastCoerce) + | GDynamic _ -> raise (UserError("",str "Not handled GDynamic")) 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 @@ -590,21 +590,21 @@ 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) -> + | GVar (_,id) -> id::acc + | GApp (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 - | RLetIn (loc,na,b,c) -> idof na :: ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc - | 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) -> + | GLambda (loc,na,k,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc + | GProd (loc,na,k,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc + | GLetIn (loc,na,b,c) -> idof na :: ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc + | GCast (loc,c,CastConv(k,t)) -> ids_of_rawterm [] c @ ids_of_rawterm [] t @ acc + | GCast (loc,c,CastCoerce) -> ids_of_rawterm [] c @ acc + | GIf (loc,c,(na,po),b1,b2) -> ids_of_rawterm [] c @ ids_of_rawterm [] b1 @ ids_of_rawterm [] b2 @ acc + | GLetTuple (_,nal,(na,po),b,c) -> List.map idof nal @ ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc - | RCases (loc,sty,rtntypopt,tml,brchl) -> + | GCases (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 _) -> [] + | GRec _ -> failwith "Fix inside a constructor branch" + | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GDynamic _) -> [] in (* build the set *) List.fold_left (fun acc x -> Idset.add x acc) Idset.empty (ids_of_rawterm [] c) @@ -616,59 +616,59 @@ let 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) -> - RApp(loc, + | GRef _ -> rt + | GVar _ -> rt + | GEvar _ -> rt + | GPatVar _ -> rt + | GApp(loc,rt',rtl) -> + GApp(loc, zeta_normalize_term rt', List.map zeta_normalize_term rtl ) - | RLambda(loc,name,k,t,b) -> - RLambda(loc, + | GLambda(loc,name,k,t,b) -> + GLambda(loc, name, k, zeta_normalize_term t, zeta_normalize_term b ) - | RProd(loc,name,k,t,b) -> - RProd(loc, + | GProd(loc,name,k,t,b) -> + GProd(loc, name, k, zeta_normalize_term t, zeta_normalize_term b ) - | RLetIn(_,Name id,def,b) -> + | GLetIn(_,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, + | GLetIn(loc,Anonymous,def,b) -> zeta_normalize_term b + | GLetTuple(loc,nal,(na,rto),def,b) -> + GLetTuple(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, + | GCases(loc,sty,infos,el,brl) -> + GCases(loc,sty, infos, 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, zeta_normalize_term b, + | GIf(loc,b,(na,e_option),lhs,rhs) -> + GIf(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)) -> - RCast(loc,zeta_normalize_term b,CastConv(k,zeta_normalize_term t)) - | RCast(loc,b,CastCoerce) -> - RCast(loc,zeta_normalize_term b,CastCoerce) - | RDynamic _ -> raise (UserError("",str "Not handled RDynamic")) + | GRec _ -> raise (UserError("",str "Not handled GRec")) + | GSort _ -> rt + | GHole _ -> rt + | GCast(loc,b,CastConv(k,t)) -> + GCast(loc,zeta_normalize_term b,CastConv(k,zeta_normalize_term t)) + | GCast(loc,b,CastCoerce) -> + GCast(loc,zeta_normalize_term b,CastCoerce) + | GDynamic _ -> raise (UserError("",str "Not handled GDynamic")) and zeta_normalize_br (loc,idl,patl,res) = (loc,idl,patl,zeta_normalize_term res) in @@ -688,29 +688,29 @@ let expand_as = in let rec expand_as map rt = match rt with - | RRef _ | REvar _ | RPatVar _ | RSort _ | RHole _ -> rt - | RVar(_,id) -> + | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> rt + | GVar(_,id) -> begin try Idmap.find id map 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) - | RProd(loc,na,k,t,b) -> RProd(loc,na,k,expand_as map t, expand_as map b) - | RLetIn(loc,na,v,b) -> RLetIn(loc,na, expand_as map v,expand_as map b) - | RLetTuple(loc,nal,(na,po),v,b) -> - RLetTuple(loc,nal,(na,Option.map (expand_as map) po), + | GApp(loc,f,args) -> GApp(loc,expand_as map f,List.map (expand_as map) args) + | GLambda(loc,na,k,t,b) -> GLambda(loc,na,k,expand_as map t, expand_as map b) + | GProd(loc,na,k,t,b) -> GProd(loc,na,k,expand_as map t, expand_as map b) + | GLetIn(loc,na,v,b) -> GLetIn(loc,na, expand_as map v,expand_as map b) + | GLetTuple(loc,nal,(na,po),v,b) -> + GLetTuple(loc,nal,(na,Option.map (expand_as map) po), expand_as map v, expand_as map b) - | RIf(loc,e,(na,po),br1,br2) -> - RIf(loc,expand_as map e,(na,Option.map (expand_as map) po), + | GIf(loc,e,(na,po),br1,br2) -> + GIf(loc,expand_as map e,(na,Option.map (expand_as map) po), expand_as map br1, expand_as map br2) - | RRec _ -> error "Not handled RRec" - | RDynamic _ -> error "Not handled RDynamic" - | RCast(loc,b,CastConv(kind,t)) -> RCast(loc,expand_as map b,CastConv(kind,expand_as map t)) - | RCast(loc,b,CastCoerce) -> RCast(loc,expand_as map b,CastCoerce) - | 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, + | GRec _ -> error "Not handled GRec" + | GDynamic _ -> error "Not handled GDynamic" + | GCast(loc,b,CastConv(kind,t)) -> GCast(loc,expand_as map b,CastConv(kind,expand_as map t)) + | GCast(loc,b,CastCoerce) -> GCast(loc,expand_as map b,CastCoerce) + | GCases(loc,sty,po,el,brl) -> + GCases(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) = (loc,idl,cpl, expand_as (List.fold_left add_as map cpl) rt) |