From 2dba88b48189af87669bcd427f0bf6c10840d680 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sat, 10 Nov 2007 13:16:57 +0000 Subject: [PATCH] More correct (but still bugged) implementation of type definition. --- .../cic_exportation/cicExportation.ml | 57 ++++++++++++++++--- 1 file changed, 50 insertions(+), 7 deletions(-) diff --git a/helm/software/components/cic_exportation/cicExportation.ml b/helm/software/components/cic_exportation/cicExportation.ml index f35cd0e1e..e591a1278 100644 --- a/helm/software/components/cic_exportation/cicExportation.ml +++ b/helm/software/components/cic_exportation/cicExportation.ml @@ -427,6 +427,47 @@ let ppty current_module_uri = args ;; +exception DoNotExtract;; + +let pp_abstracted_ty current_module_uri = + let rec args context = + function + Cic.Lambda (n,s,t) -> + let n = + match n with + Cic.Anonymous -> Cic.Anonymous + | Cic.Name n -> Cic.Name (String.uncapitalize n) + in + (match analyze_type context s with + `Statement + | `Type + | `Sort Cic.Prop -> + args ((Some (n,Cic.Decl s))::context) t + | `Sort _ -> + let n = + match n with + Cic.Anonymous -> Cic.Anonymous + | Cic.Name name -> Cic.Name ("'" ^ name) in + let abstr,res = + args ((Some (n,Cic.Decl s))::context) t + in + (match n with + Cic.Anonymous -> abstr + | Cic.Name name -> name::abstr), + res) + | ty -> + match analyze_type context ty with + ` Sort _ + | `Statement -> raise DoNotExtract + | `Type -> + (* BUG HERE: this can be a real System F type *) + let head = pp ~in_type:true current_module_uri ty context in + [],head + in + args +;; + + (* ppinductiveType (typename, inductive, arity, cons) *) (* pretty-prints a single inductive definition *) (* (typename, inductive, arity, cons) *) @@ -472,13 +513,15 @@ let ppobj current_module_uri obj = match analyze_type [] t1 with `Sort Cic.Prop -> "" | _ -> - let abstr,args = ppty current_module_uri 0 [] t1 in - let abstr = - let s = String.concat "," abstr in - if s = "" then "" else "(" ^ s ^ ") " - in - "type " ^ abstr ^ ppid name ^ " = " ^ String.concat "->" args ^ - "\n") + (try + let abstr,res = pp_abstracted_ty current_module_uri [] t1 in + let abstr = + let s = String.concat "," abstr in + if s = "" then "" else "(" ^ s ^ ") " + in + "type " ^ abstr ^ ppid name ^ " = " ^ res ^ "\n" + with + DoNotExtract -> "")) | C.Constant (name, None, ty, params, _) -> (match analyze_type [] ty with `Sort Cic.Prop -- 2.39.2