From 6a248ceeb4ea05b211328d183fdc78462ee807ca Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 5 Nov 2007 14:20:20 +0000 Subject: [PATCH] Handling of left parameters of constructors/indutive type definitions improved. Bug fixed: arguments of sort Prop were not dropped from MutCase branches. --- .../cic_exportation/cicExportation.ml | 82 ++++++++++++------- 1 file changed, 51 insertions(+), 31 deletions(-) diff --git a/helm/software/components/cic_exportation/cicExportation.ml b/helm/software/components/cic_exportation/cicExportation.ml index dbb7194a9..7be9ea3d9 100644 --- a/helm/software/components/cic_exportation/cicExportation.ml +++ b/helm/software/components/cic_exportation/cicExportation.ml @@ -184,12 +184,16 @@ let rec pp t context = let hes = pp he context in let stl = String.concat "," (clean_args_for_ty context tl) in (if stl = "" then "" else "(" ^ stl ^ ") ") ^ hes - | C.Appl (C.MutConstruct _ as he::tl) -> + | C.Appl (C.MutConstruct (uri,n,_,_) as he::tl) -> + let nparams = + match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with + C.InductiveDefinition (_,_,nparams,_) -> nparams + | _ -> assert false in let hes = pp he context in - let stl = String.concat "," (clean_args context tl) in + let stl = String.concat "," (clean_args nparams context tl) in "(" ^ hes ^ (if stl = "" then "" else "(" ^ stl ^ ")") ^ ")" | C.Appl li -> - "(" ^ String.concat " " (clean_args context li) ^ ")" + "(" ^ String.concat " " (clean_args 0 context li) ^ ")" | C.Const (uri,exp_named_subst) -> qualified_name_of_uri current_module_uri uri ^ pp_exp_named_subst exp_named_subst context @@ -225,6 +229,10 @@ let rec pp t context = string_of_int n2 ) | C.MutCase (uri,n1,ty,te,patterns) -> + let paramsno = + match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with + C.InductiveDefinition (_,_,paramsno,_) -> paramsno + | _ -> assert false in (match analyze_term context te with `Type -> assert false | `Proof -> @@ -263,9 +271,8 @@ let rec pp t context = let rec combine = function [],[] -> [] - | [],l -> List.map (fun x -> "???",0,Some x) l - | l,[] -> List.map (fun (x,no) -> x,no,None) l - | (x,no)::tlx,y::tly -> (x,no,Some y)::(combine (tlx,tly)) + | (x,no)::tlx,y::tly -> (x,no,y)::(combine (tlx,tly)) + | _,_ -> assert false in combine (connames_and_argsno,patterns) in @@ -280,23 +287,25 @@ let rec pp t context = aux (argsno - 1) (Some (name,Cic.Decl ty)::context) bo in - (match name with C.Anonymous -> "_" | C.Name s -> s) - ::args, - res + (match analyze_type context ty with + `Statement + | `Sort _ -> args,res + | `Type -> + (match name with + C.Anonymous -> "_" + | C.Name s -> s)::args,res) | t when argsno = 0 -> [],pp t context | t -> ["{" ^ string_of_int argsno ^ " args missing}"], pp t context in let pattern,body = - match y with - None -> x,"" - | Some y when argsno = 0 -> x,pp y context - | Some y -> - let args,body = aux argsno context y in - let sargs = String.concat "," args in - x ^ (if sargs = "" then "" else "(" ^ sargs^ ")"), - body + if argsno = 0 then x,pp y context + else + let args,body = aux argsno context y in + let sargs = String.concat "," args in + x ^ (if sargs = "" then "" else "(" ^ sargs^ ")"), + body in pattern ^ " -> " ^ body ) connames_and_argsno_and_patterns)) ^ @@ -339,13 +348,16 @@ and pp_exp_named_subst exp_named_subst context = (function (uri,t) -> UriManager.name_of_uri uri ^ " \\Assign " ^ pp t context) exp_named_subst ) ^ "]" -and clean_args context = +and clean_args nparams context = + let nparams = ref nparams in HExtlib.filter_map (function t -> + decr nparams; match analyze_term context t with - `Type -> None - | `Proof -> None - | `Term -> Some pp t context) + `Term when !nparams < 0 -> Some pp t context + | `Term + | `Type + | `Proof -> None) and clean_args_for_ty context = HExtlib.filter_map (function t -> @@ -358,7 +370,9 @@ in ;; let ppty current_module_uri = - let rec args context = + (* nparams is the number of left arguments + left arguments should either become parameters or be skipped altogether *) + let rec args nparams context = function Cic.Prod (n,s,t) -> let n = @@ -367,21 +381,27 @@ let ppty current_module_uri = | Cic.Name n -> Cic.Name (String.uncapitalize n) in (match analyze_type context s with - `Sort Cic.Prop -> args ((Some (n,Cic.Decl s))::context) t - | `Statement + `Statement + | `Sort Cic.Prop -> + args (nparams - 1) ((Some (n,Cic.Decl s))::context) t + | `Type when nparams > 0 -> + args (nparams - 1) ((Some (n,Cic.Decl s))::context) t + | `Type -> + let abstr,args = + args (nparams - 1) ((Some (n,Cic.Decl s))::context) t in + abstr,pp current_module_uri s context::args | `Sort _ -> let n = match n with Cic.Anonymous -> Cic.Anonymous | Cic.Name name -> Cic.Name ("'" ^ name) in - let abstr,args = args ((Some (n,Cic.Decl s))::context) t in + let abstr,args = + args (nparams - 1) ((Some (n,Cic.Decl s))::context) t + in (match n with Cic.Anonymous -> abstr | Cic.Name name -> name::abstr), - args - | `Type -> - let abstr,args = args ((Some (n,Cic.Decl s))::context) t in - abstr,pp current_module_uri s context::args) + args) | _ -> [],[] in args @@ -403,7 +423,7 @@ let ppinductiveType current_module_uri nparams (typename, inductive, arity, cons let abstr,scons = List.fold_right (fun (id,ty) (_abstr,i) -> (* we should verify _abstr = abstr' *) - let abstr',sargs = ppty current_module_uri [] ty in + let abstr',sargs = ppty current_module_uri nparams [] ty in let sargs = String.concat " * " sargs in abstr', String.capitalize id ^ @@ -432,7 +452,7 @@ let ppobj current_module_uri obj = match analyze_type [] t1 with `Sort Cic.Prop -> "" | _ -> - let abstr,args = ppty current_module_uri [] t1 in + let abstr,args = ppty current_module_uri 0 [] t1 in let abstr = let s = String.concat "," abstr in if s = "" then "" else "(" ^ s ^ ") " -- 2.39.2