From 530f6d29b866eb41b1a4195b15df8feaf6d5d6de Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 2 Nov 2007 18:05:40 +0000 Subject: [PATCH] *** Very experimental and not branched *** Exportation to OCaml partially implement in cic_exportation. It can already export several files from the freescale development (also not committed yet). Still to be implemented: a) erasure of term dependencies from types b) extraction of "open" statements [ I do not know how to implement this! ] c) extraction from CurrentProof d) extraction from Let-In e) extraction from CoFix f) extraction from mutually recursive inductive types and Fix Known bugs/missing features: 1) All the "classical" ones (described, for instance, in Letouzey's papers). In particular, terms may diverge, singleton elimination and false elimination not implemented in the correct way, Obj.magic not generated where needed, etc. 2) Name clashes can be generated by the extraction. OCaml keywords may be chosen. And so on. --- .../METAS/meta.helm-cic_exportation.src | 5 + components/Makefile | 1 + components/cic_exportation/.depend | 2 + components/cic_exportation/.depend.opt | 2 + components/cic_exportation/Makefile | 14 + components/cic_exportation/cicExportation.ml | 401 ++++++++++++++++++ components/cic_exportation/cicExportation.mli | 28 ++ configure.ac | 1 + 8 files changed, 454 insertions(+) create mode 100644 components/METAS/meta.helm-cic_exportation.src create mode 100644 components/cic_exportation/.depend create mode 100644 components/cic_exportation/.depend.opt create mode 100644 components/cic_exportation/Makefile create mode 100644 components/cic_exportation/cicExportation.ml create mode 100644 components/cic_exportation/cicExportation.mli diff --git a/components/METAS/meta.helm-cic_exportation.src b/components/METAS/meta.helm-cic_exportation.src new file mode 100644 index 000000000..97124f913 --- /dev/null +++ b/components/METAS/meta.helm-cic_exportation.src @@ -0,0 +1,5 @@ +requires="helm-cic_proof_checking" +version="0.0.1" +archive(byte)="cic_exportation.cma" +archive(native)="cic_exportation.cmxa" +linkopts="" diff --git a/components/Makefile b/components/Makefile index d30e63dcd..34020150a 100644 --- a/components/Makefile +++ b/components/Makefile @@ -19,6 +19,7 @@ MODULES = \ getter \ cic \ cic_proof_checking \ + cic_exportation \ cic_acic \ metadata \ library \ diff --git a/components/cic_exportation/.depend b/components/cic_exportation/.depend new file mode 100644 index 000000000..288ea5f6c --- /dev/null +++ b/components/cic_exportation/.depend @@ -0,0 +1,2 @@ +cicExportation.cmo: cicExportation.cmi +cicExportation.cmx: cicExportation.cmi diff --git a/components/cic_exportation/.depend.opt b/components/cic_exportation/.depend.opt new file mode 100644 index 000000000..288ea5f6c --- /dev/null +++ b/components/cic_exportation/.depend.opt @@ -0,0 +1,2 @@ +cicExportation.cmo: cicExportation.cmi +cicExportation.cmx: cicExportation.cmi diff --git a/components/cic_exportation/Makefile b/components/cic_exportation/Makefile new file mode 100644 index 000000000..3062749b6 --- /dev/null +++ b/components/cic_exportation/Makefile @@ -0,0 +1,14 @@ +PACKAGE = cic_exportation +PREDICATES = + +INTERFACE_FILES = \ + cicExportation.mli \ + $(NULL) +IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) + +# Metadata tools only need zeta-reduction +EXTRA_OBJECTS_TO_INSTALL = +EXTRA_OBJECTS_TO_CLEAN = + +include ../../Makefile.defs +include ../Makefile.common diff --git a/components/cic_exportation/cicExportation.ml b/components/cic_exportation/cicExportation.ml new file mode 100644 index 000000000..8acb873a9 --- /dev/null +++ b/components/cic_exportation/cicExportation.ml @@ -0,0 +1,401 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(* $Id: cicPp.ml 7413 2007-05-29 15:30:53Z tassi $ *) + +exception CicExportationInternalError;; +exception NotEnoughElements;; + +(* Utility functions *) + +let analyze_term context t = + match fst(CicTypeChecker.type_of_aux' [] context t CicUniv.oblivion_ugraph)with + Cic.Sort _ -> `Type + | ty -> + match + fst (CicTypeChecker.type_of_aux' [] context ty CicUniv.oblivion_ugraph) + with + Cic.Sort Cic.Prop -> `Proof + | _ -> `Term +;; + +let analyze_type context t = + let rec aux = + function + Cic.Sort _ -> `Sort + | Cic.Prod (_,_,t) -> aux t + | _ -> `SomethingElse + in + match aux t with + `Sort -> `Sort + | `SomethingElse -> + match + fst(CicTypeChecker.type_of_aux' [] context t CicUniv.oblivion_ugraph) + with + Cic.Sort Cic.Prop -> `Statement + | _ -> `Type +;; + +let ppid = + let reserved = + [ "to"; + "mod" + ] + in + 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 +;; + +(* pp t l *) +(* pretty-prints a term t of cic in an environment l where l is a list of *) +(* identifier names used to resolve DeBrujin indexes. The head of l is the *) +(* name associated to the greatest DeBrujin index in t *) +let pp ?metasenv = +let rec pp 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) -> + UriManager.name_of_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 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 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 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 -> "(\\forall " ^ n ^ ":" ^ pp s context ^ "." ^ pp t ((Some (b,Cic.Decl s))::context) ^ ")" + | C.Anonymous -> "(" ^ pp s context ^ "\\to " ^ pp t ((Some (b,Cic.Decl s))::context) ^ ")" + ) + | C.Cast (v,t) -> pp v context + | C.Lambda (b,s,t) -> + (match analyze_type context s with + `Sort + | `Statement -> pp t ((Some (b,Cic.Decl s))::context) + | `Type -> "(function " ^ ppname b ^ " -> " ^ pp t ((Some (b,Cic.Decl s))::context) ^ ")") + | C.LetIn (b,s,t) -> + let ty,_ = CicTypeChecker.type_of_aux' [] context t CicUniv.oblivion_ugraph in + "(let " ^ ppname b ^ " = " ^ pp s context ^ " in " ^ pp t ((Some (b,Cic.Def (s,Some ty)))::context) ^ ")" + | C.Appl (C.MutConstruct _ as he::tl) -> + let hes = pp he context in + let stl = String.concat "," (clean_args context tl) in + "(" ^ hes ^ (if stl = "" then "" else "(" ^ stl ^ ")") ^ ")" + | C.Appl li -> + "(" ^ String.concat " " (clean_args context li) ^ ")" + | C.Const (uri,exp_named_subst) -> + ppid (UriManager.name_of_uri uri) ^ pp_exp_named_subst exp_named_subst context + | C.MutInd (uri,n,exp_named_subst) -> + (try + match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with + C.InductiveDefinition (dl,_,_,_) -> + let (name,_,_,_) = get_nth dl (n+1) in + ppid name ^ 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.empty_ugraph uri) with + C.InductiveDefinition (dl,_,_,_) -> + let (_,_,_,cons) = get_nth dl (n1+1) in + let (id,_) = get_nth cons n2 in + String.capitalize id ^ 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) -> + 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 + String.capitalize id, 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 + 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 + (List.map + (function (name,_,ty,_) -> + Some (C.Name name,Cic.Decl ty)) funs) + in + "\nlet rec " ^ + List.fold_right + (fun (name,ind,ty,bo) i -> name ^ " = \n" ^ + pp bo (names@context) ^ i) + funs "" ^ + " in " ^ + (match get_nth names (no + 1) with + Some (Cic.Name n,_) -> n + | _ -> assert false) ^ "\n" + | C.CoFix (no,funs) -> + let names = + List.rev + (List.map + (function (name,ty,_) -> + Some (C.Name name,Cic.Decl ty)) funs) + in + "\nCoFix " ^ " {" ^ + List.fold_right + (fun (name,ty,bo) i -> "\n" ^ name ^ + " : " ^ pp ty context ^ " := \n" ^ + pp 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 uri ^ " \\Assign " ^ pp t context) + exp_named_subst + ) ^ "]" +and clean_args context = + HExtlib.filter_map + (function t -> + match analyze_term context t with + `Type -> None + | `Proof -> None + | `Term -> Some pp t context) +in + pp +;; + +(* ppinductiveType (typename, inductive, arity, cons) *) +(* pretty-prints a single inductive definition *) +(* (typename, inductive, arity, cons) *) +let ppinductiveType (typename, inductive, arity, cons) = + let abstr,scons = + List.fold_right + (fun (id,ty) (abstr,i) -> + let rec args context = + function + Cic.Prod (n,s,t) -> + (match analyze_type context s with + `Statement + | `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 + (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 s context::args) + | _ -> [],[] + in + let abstr',sargs = args [] 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 ^ ") " + in + "type " ^ abstr ^ typename ^ " =\n" ^ scons +;; + +(* ppobj obj returns a string with describing the cic object obj in a syntax *) +(* similar to the one used by Coq *) +let ppobj obj = + let module C = Cic in + let module U = UriManager in + match obj with + C.Constant (name, Some t1, t2, params, _) -> + (match analyze_type [] t2 with + `Statement -> "" + | `Type + | `Sort -> "let " ^ ppid name ^ " =\n" ^ pp t1 [] ^ "\n") + | C.Constant (name, None, ty, params, _) -> + (match analyze_type [] ty with + `Statement -> "" + | `Sort -> "type " ^ ppid name ^ "\n" + | `Type -> "let " ^ ppid name ^ " = assert false\n") + | C.Variable (name, bo, ty, params, _) -> + "Variable " ^ name ^ + "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^ + ")" ^ ":\n" ^ + pp ty [] ^ "\n" ^ + (match bo with None -> "" | Some bo -> ":= " ^ pp bo []) + | C.CurrentProof (name, conjectures, value, ty, params, _) -> + "Current Proof of " ^ name ^ + "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^ + ")" ^ ":\n" ^ + let separate s = if s = "" then "" else s ^ " ; " in + List.fold_right + (fun (n, context, t) i -> + let conjectures',name_context = + List.fold_right + (fun context_entry (i,name_context) -> + (match context_entry with + Some (n,C.Decl at) -> + (separate i) ^ + ppname n ^ ":" ^ + pp ~metasenv:conjectures at name_context ^ " ", + context_entry::name_context + | Some (n,C.Def (at,None)) -> + (separate i) ^ + ppname n ^ ":= " ^ pp ~metasenv:conjectures + at name_context ^ " ", + context_entry::name_context + | None -> + (separate i) ^ "_ :? _ ", context_entry::name_context + | _ -> assert false) + ) context ("",[]) + in + conjectures' ^ " |- " ^ "?" ^ (string_of_int n) ^ ": " ^ + pp ~metasenv:conjectures t name_context ^ "\n" ^ i + ) conjectures "" ^ + "\n" ^ pp ~metasenv:conjectures value [] ^ " : " ^ + pp ~metasenv:conjectures ty [] + | C.InductiveDefinition (l, params, nparams, _) -> + List.fold_right (fun x i -> ppinductiveType x ^ i) l "\n" +;; + +let ppobj obj = + let res = ppobj obj in + if res = "" then "" else res ^ ";;\n" +;; diff --git a/components/cic_exportation/cicExportation.mli b/components/cic_exportation/cicExportation.mli new file mode 100644 index 000000000..07c2b8845 --- /dev/null +++ b/components/cic_exportation/cicExportation.mli @@ -0,0 +1,28 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(* $Id: cicPp.ml 7413 2007-05-29 15:30:53Z tassi $ *) + +val ppobj : Cic.obj -> string diff --git a/configure.ac b/configure.ac index 3370b61b2..b2f218d0f 100644 --- a/configure.ac +++ b/configure.ac @@ -82,6 +82,7 @@ helm-acic_procedural \ helm-content_pres \ helm-hgdome \ helm-tactics \ +helm-cic_exportation \ " FINDLIB_CREQUIRES=" \ $FINDLIB_COMREQUIRES \ -- 2.39.2