From 6c593b6e83713bf493ad9e5e0688d9ec2fc9f768 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 4 Nov 2007 18:52:32 +0000 Subject: [PATCH] Empty types not in Prop and empty types elimination handled correctly. --- .../cic_exportation/cicExportation.ml | 159 ++++++++++-------- 1 file changed, 86 insertions(+), 73 deletions(-) diff --git a/helm/software/components/cic_exportation/cicExportation.ml b/helm/software/components/cic_exportation/cicExportation.ml index 4b10fe731..eeddc0949 100644 --- a/helm/software/components/cic_exportation/cicExportation.ml +++ b/helm/software/components/cic_exportation/cicExportation.ml @@ -224,64 +224,74 @@ let rec pp t context = | [he] -> pp he context (* singleton elimination *) | _ -> assert false) | `Term -> - let connames_and_argsno = - (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with - C.InductiveDefinition (dl,_,paramsno,_) -> - let (_,_,_,cons) = get_nth dl (n1+1) in - List.map - (fun (id,ty) -> - (* this is just an approximation since we do not have - reduction yet! *) - let rec count_prods toskip = - function - C.Prod (_,_,bo) when toskip > 0 -> - count_prods (toskip - 1) bo - | C.Prod (_,_,bo) -> 1 + count_prods 0 bo - | _ -> 0 - in - qualified_name_of_uri current_module_name ~capitalize:true - (UriManager.uri_of_string - (UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")), - count_prods paramsno ty - ) cons - | _ -> raise CicExportationInternalError - ) - in - let connames_and_argsno_and_patterns = - 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)) + if patterns = [] then "assert false" + else + (let connames_and_argsno = + (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with + C.InductiveDefinition (dl,_,paramsno,_) -> + let (_,_,_,cons) = get_nth dl (n1+1) in + List.map + (fun (id,ty) -> + (* this is just an approximation since we do not have + reduction yet! *) + let rec count_prods toskip = + function + C.Prod (_,_,bo) when toskip > 0 -> + count_prods (toskip - 1) bo + | C.Prod (_,_,bo) -> 1 + count_prods 0 bo + | _ -> 0 + in + qualified_name_of_uri current_module_name + ~capitalize:true + (UriManager.uri_of_string + (UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")), + count_prods paramsno ty + ) cons + | _ -> raise CicExportationInternalError + ) in - combine (connames_and_argsno,patterns) - in - "\n(match " ^ pp te context ^ " with \n" ^ - (String.concat "\n | " - (List.map - (fun (x,argsno,y) -> - let rec aux argsno context = - function - Cic.Lambda (name,ty,bo) when argsno > 0 -> - let args,res = aux (argsno - 1) (Some (name,Cic.Decl ty)::context) bo in - (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 - in - pattern ^ " -> " ^ body - ) connames_and_argsno_and_patterns)) ^ - ")\n") + let connames_and_argsno_and_patterns = + 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)) + in + combine (connames_and_argsno,patterns) + in + "\n(match " ^ pp te context ^ " with \n" ^ + (String.concat "\n | " + (List.map + (fun (x,argsno,y) -> + let rec aux argsno context = + function + Cic.Lambda (name,ty,bo) when argsno > 0 -> + let args,res = + aux (argsno - 1) (Some (name,Cic.Decl ty)::context) + bo + in + (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 + in + pattern ^ " -> " ^ body + ) connames_and_argsno_and_patterns)) ^ + ")\n")) | C.Fix (no, funs) -> let names = List.rev @@ -365,22 +375,25 @@ let ppinductiveType current_module_name (typename, inductive, arity, cons) = | `Statement | `Type -> assert false | `Sort _ -> - let abstr,scons = - List.fold_right - (fun (id,ty) (abstr,i) -> - let abstr',sargs = ppty current_module_name [] ty in - let sargs = String.concat " * " sargs in - abstr'@abstr, - String.capitalize id ^ - (if sargs = "" then "" else " of " ^ sargs) ^ - (if i = "" then "\n" else "\n | ") ^ i) - cons ([],"") - in - let abstr = - let s = String.concat "," abstr in - if s = "" then "" else "(" ^ s ^ ") " + if cons = [] then + "type " ^ String.uncapitalize typename ^ " = unit (* empty type *)\n" + else ( + let abstr,scons = + List.fold_right + (fun (id,ty) (abstr,i) -> + let abstr',sargs = ppty current_module_name [] ty in + let sargs = String.concat " * " sargs in + abstr'@abstr, + String.capitalize id ^ + (if sargs = "" then "" else " of " ^ sargs) ^ + (if i = "" then "" else "\n | ") ^ i) + cons ([],"") in - "type " ^ abstr ^ String.uncapitalize typename ^ " =\n" ^ scons ^ "\n" + let abstr = + let s = String.concat "," abstr in + if s = "" then "" else "(" ^ s ^ ") " + in + "type " ^ abstr ^ String.uncapitalize typename ^ " =\n" ^ scons ^ "\n") ;; let ppobj current_module_name obj = @@ -454,5 +467,5 @@ let ppobj current_module_name obj = let ppobj current_module_name obj = let res = ppobj current_module_name obj in - if res = "" then "" else res ^ ";;\n" + if res = "" then "" else res ^ ";;\n\n" ;; -- 2.39.2