- function n ->
- let n = String.uncapitalize n in
- if List.mem n reserved then n ^ "_" else n
-;;
-
-let ppname =
- function
- Cic.Name s -> ppid s
- | Cic.Anonymous -> "_"
-;;
-
-(* get_nth l n returns the nth element of the list l if it exists or *)
-(* raises NotEnoughElements if l has less than n elements *)
-let rec get_nth l n =
- match (n,l) with
- (1, he::_) -> he
- | (n, he::tail) when n > 1 -> get_nth tail (n-1)
- | (_,_) -> raise NotEnoughElements
-;;
-
-let qualified_name_of_uri status current_module_uri ?(capitalize=false) uri =
- let name =
- if capitalize then
- String.capitalize (UriManager.name_of_uri status uri)
- else
- ppid (UriManager.name_of_uri status uri) in
- let filename =
- let suri = UriManager.buri_of_uri uri in
- let s = String.sub suri 5 (String.length suri - 5) in
- let s = Pcre.replace ~pat:"/" ~templ:"_" s in
- String.uncapitalize s in
- if current_module_uri = UriManager.buri_of_uri uri then
- name
- else
- String.capitalize filename ^ "." ^ name
-;;
-
-let current_go_up = ref "(.!(";;
-let at_level2 f x =
- try
- current_go_up := "(.~(";
- let rc = f x in
- current_go_up := "(.!(";
- rc
- with exn ->
- current_go_up := "(.!(";
- raise exn
-;;
-
-let pp current_module_uri ?metasenv ~in_type =
-let rec pp ~in_type t context =
- let module C = Cic in
- match t with
- C.Rel n ->
- begin
- try
- (match get_nth context n with
- Some (C.Name s,_) -> ppid s
- | Some (C.Anonymous,_) -> "__" ^ string_of_int n
- | None -> "_hidden_" ^ string_of_int n
- )
- with
- NotEnoughElements -> string_of_int (List.length context - n)
- end
- | C.Var (uri,exp_named_subst) ->
- qualified_name_of_uri status current_module_uri uri ^
- pp_exp_named_subst exp_named_subst context
- | C.Meta (n,l1) ->
- (match metasenv with
- None ->
- "?" ^ (string_of_int n) ^ "[" ^
- String.concat " ; "
- (List.rev_map
- (function
- None -> "_"
- | Some t -> pp ~in_type:false t context) l1) ^
- "]"
- | Some metasenv ->
- try
- let _,context,_ = CicUtil.lookup_meta n metasenv in
- "?" ^ (string_of_int n) ^ "[" ^
- String.concat " ; "
- (List.rev
- (List.map2
- (fun x y ->
- match x,y with
- _, None
- | None, _ -> "_"
- | Some _, Some t -> pp ~in_type:false t context
- ) context l1)) ^
- "]"
- with
- CicUtil.Meta_not_found _
- | Invalid_argument _ ->
- "???" ^ (string_of_int n) ^ "[" ^
- String.concat " ; "
- (List.rev_map (function None -> "_" | Some t ->
- pp ~in_type:false t context) l1) ^
- "]"
- )
- | C.Sort s ->
- (match s with
- C.Prop -> "Prop"
- | C.Set -> "Set"
- | C.Type _ -> "Type"
- (*| C.Type u -> ("Type" ^ CicUniv.string_of_universe u)*)
- | C.CProp _ -> "CProp"
- )
- | C.Implicit (Some `Hole) -> "%"
- | C.Implicit _ -> "?"
- | C.Prod (b,s,t) ->
- (match b with
- C.Name n ->
- let n = "'" ^ String.uncapitalize n in
- "(" ^ pp ~in_type:true s context ^ " -> " ^
- pp ~in_type:true t ((Some (Cic.Name n,Cic.Decl s))::context) ^ ")"
- | C.Anonymous ->
- "(" ^ pp ~in_type:true s context ^ " -> " ^
- pp ~in_type:true t ((Some (b,Cic.Decl s))::context) ^ ")")
- | C.Cast (v,t) -> pp ~in_type v context
- | C.Lambda (b,s,t) ->
- (match analyze_type context s with
- `Sort _
- | `Statement -> pp ~in_type t ((Some (b,Cic.Decl s))::context)
- | `Optimize -> prerr_endline "XXX lambda";assert false
- | `Type ->
- "(function " ^ ppname b ^ " -> " ^
- pp ~in_type t ((Some (b,Cic.Decl s))::context) ^ ")")
- | C.LetIn (b,s,ty,t) ->
- (match analyze_term context s with
- | `Type
- | `Proof -> pp ~in_type t ((Some (b,Cic.Def (s,ty)))::context)
- | `Optimize
- | `Term ->
- "(let " ^ ppname b ^ (*" : " ^ pp ~in_type:true ty context ^*)
- " = " ^ pp ~in_type:false s context ^ " in " ^
- pp ~in_type t ((Some (b,Cic.Def (s,ty)))::context) ^ ")")
- | C.Appl (he::tl) when in_type ->
- let hes = pp ~in_type he context in
- let stl = String.concat "," (clean_args_for_ty context tl) in
- (if stl = "" then "" else "(" ^ stl ^ ") ") ^ hes
- | C.Appl (C.MutInd _ as he::tl) ->
- let hes = pp ~in_type he context in
- let stl = String.concat "," (clean_args_for_ty context tl) in
- (if stl = "" then "" else "(" ^ stl ^ ") ") ^ hes
- | C.Appl (C.MutConstruct (uri,n,_,_) as he::tl) ->
- let nparams =
- match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
- C.InductiveDefinition (_,_,nparams,_) -> nparams
- | _ -> assert false in
- let hes = pp ~in_type he context in
- let stl = String.concat "," (clean_args_for_constr nparams context tl) in
- "(" ^ hes ^ (if stl = "" then "" else "(" ^ stl ^ ")") ^ ")"
- | C.Appl li ->
- "(" ^ String.concat " " (clean_args context li) ^ ")"
- | C.Const (uri,exp_named_subst) ->
- qualified_name_of_uri status current_module_uri uri ^
- pp_exp_named_subst exp_named_subst context
- | C.MutInd (uri,n,exp_named_subst) ->
- (try
- match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
- C.InductiveDefinition (dl,_,_,_) ->
- let (name,_,_,_) = get_nth dl (n+1) in
- qualified_name_of_uri status current_module_uri
- (UriManager.uri_of_string
- (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con")) ^
- pp_exp_named_subst exp_named_subst context
- | _ -> raise CicExportationInternalError
- with
- Sys.Break as exn -> raise exn
- | _ -> UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n + 1)
- )
- | C.MutConstruct (uri,n1,n2,exp_named_subst) ->
- (try
- match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
- C.InductiveDefinition (dl,_,_,_) ->
- let _,_,_,cons = get_nth dl (n1+1) in
- let id,_ = get_nth cons n2 in
- qualified_name_of_uri status current_module_uri ~capitalize:true
- (UriManager.uri_of_string
- (UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")) ^
- pp_exp_named_subst exp_named_subst context
- | _ -> raise CicExportationInternalError
- with
- Sys.Break as exn -> raise exn
- | _ ->
- UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n1 + 1) ^ "/" ^
- string_of_int n2
- )
- | C.MutCase (uri,n1,ty,te,patterns) ->
- if in_type then
- "unit (* TOO POLYMORPHIC TYPE *)"
- else (
- let rec needs_obj_magic ty =
- match CicReduction.whd context ty with
- | Cic.Lambda (_,_,(Cic.Lambda(_,_,_) as t)) -> needs_obj_magic t
- | Cic.Lambda (_,_,t) -> not (DoubleTypeInference.does_not_occur 1 t)
- | _ -> false (* it can be a Rel, e.g. in *_rec *)
- in
- let needs_obj_magic = needs_obj_magic ty in
- (match analyze_term context te with
- `Type -> assert false
- | `Proof ->
- (match patterns with
- [] -> "assert false" (* empty type elimination *)
- | [he] ->
- pp ~in_type:false he context (* singleton elimination *)
- | _ -> assert false)
- | `Optimize
- | `Term ->
- if patterns = [] then "assert false"
- else
- (let connames_and_argsno, go_up, go_pu, go_down, go_nwod =
- (match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
- C.InductiveDefinition (dl,_,paramsno,_) ->
- let (_,_,_,cons) = get_nth dl (n1+1) in
- let rc =
- 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 status current_module_uri
- ~capitalize:true
- (UriManager.uri_of_string
- (UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")),
- count_prods paramsno ty
- ) cons
- in
- if not (is_mcu_type uri) then rc, "","","",""
- else rc, !current_go_up, "))", "( .< (", " ) >.)"
- | _ -> raise CicExportationInternalError
- )
- in
- let connames_and_argsno_and_patterns =
- let rec combine =
- function
- [],[] -> []
- | (x,no)::tlx,y::tly -> (x,no,y)::(combine (tlx,tly))
- | _,_ -> assert false
- in
- combine (connames_and_argsno,patterns)
- in
- go_up ^
- "\n(match " ^ pp ~in_type:false 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 name =
- match name with
- Cic.Anonymous -> Cic.Anonymous
- | Cic.Name n -> Cic.Name (ppid n) in
- let args,res =
- aux (argsno - 1) (Some (name,Cic.Decl ty)::context)
- bo
- in
- (match analyze_type context ty with
- | `Optimize -> prerr_endline "XXX contructor with l2 arg"; assert false
- | `Statement
- | `Sort _ -> args,res
- | `Type ->
- (match name with
- C.Anonymous -> "_"
- | C.Name s -> s)::args,res)
- | t when argsno = 0 -> [],pp ~in_type:false t context
- | t ->
- ["{" ^ string_of_int argsno ^ " args missing}"],
- pp ~in_type:false t context
- in
- let pattern,body =
- if argsno = 0 then x,pp ~in_type:false 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 ^ " -> " ^ go_down ^
- (if needs_obj_magic then
- "Obj.magic (" ^ body ^ ")"
- else
- body) ^ go_nwod
- ) connames_and_argsno_and_patterns)) ^
- ")\n"^go_pu)))
- | C.Fix (no, funs) ->
- let names,_ =
- List.fold_left
- (fun (types,len) (n,_,ty,_) ->
- (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
- len+1)
- ) ([],0) funs
- in
- "let rec " ^
- List.fold_right
- (fun (name,ind,ty,bo) i -> name ^ " = \n" ^
- pp ~in_type:false bo (names@context) ^ i)
- funs "" ^
- " in " ^
- (match get_nth names (no + 1) with
- Some (Cic.Name n,_) -> n
- | _ -> assert false)
- | C.CoFix (no,funs) ->
- let names,_ =
- List.fold_left
- (fun (types,len) (n,ty,_) ->
- (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
- len+1)
- ) ([],0) funs
- in
- "\nCoFix " ^ " {" ^
- List.fold_right
- (fun (name,ty,bo) i -> "\n" ^ name ^
- " : " ^ pp ~in_type:true ty context ^ " := \n" ^
- pp ~in_type:false bo (names@context) ^ i)
- funs "" ^
- "}\n"
-and pp_exp_named_subst exp_named_subst context =
- if exp_named_subst = [] then "" else
- "\\subst[" ^
- String.concat " ; " (
- List.map
- (function (uri,t) -> UriManager.name_of_uri status uri ^ " \\Assign " ^ pp ~in_type:false t context)
- exp_named_subst
- ) ^ "]"
-and clean_args_for_constr nparams context =
- let nparams = ref nparams in
- HExtlib.filter_map
- (function t ->
- decr nparams;
- match analyze_term context t with
- `Term when !nparams < 0 -> Some (pp ~in_type:false t context)
- | `Optimize
- | `Term
- | `Type
- | `Proof -> None)
-and clean_args context =
- function
- | [] | [_] -> assert false
- | he::arg1::tl as l ->
- let head_arg1, rest =
- match analyze_term context arg1 with
- | `Optimize ->
- !current_go_up :: pp ~in_type:false he context ::
- pp ~in_type:false arg1 context :: ["))"], tl
- | _ -> [], l