From f8967ca20669e181bcda5a6cdabbc3db0bfc4c44 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 4 Nov 2007 18:34:01 +0000 Subject: [PATCH] Empty and singleton type elimination are now handled properly. --- .../cic_exportation/cicExportation.ml | 122 ++++++++++-------- 1 file changed, 65 insertions(+), 57 deletions(-) diff --git a/helm/software/components/cic_exportation/cicExportation.ml b/helm/software/components/cic_exportation/cicExportation.ml index e5f1face1..4b10fe731 100644 --- a/helm/software/components/cic_exportation/cicExportation.ml +++ b/helm/software/components/cic_exportation/cicExportation.ml @@ -216,64 +216,72 @@ let rec pp t context = string_of_int n2 ) | C.MutCase (uri,n1,ty,te,patterns) -> - 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)) - 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 + (match analyze_term context te with + `Type -> assert false + | `Proof -> + (match patterns with + [] -> "assert false" (* empty type elimination *) + | [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)) 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" + 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 -- 2.39.2