]> matita.cs.unibo.it Git - helm.git/commitdiff
*** Very experimental and not branched ***
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 2 Nov 2007 18:05:40 +0000 (18:05 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 2 Nov 2007 18:05:40 +0000 (18:05 +0000)
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.

helm/software/components/METAS/meta.helm-cic_exportation.src [new file with mode: 0644]
helm/software/components/Makefile
helm/software/components/cic_exportation/.depend [new file with mode: 0644]
helm/software/components/cic_exportation/.depend.opt [new file with mode: 0644]
helm/software/components/cic_exportation/Makefile [new file with mode: 0644]
helm/software/components/cic_exportation/cicExportation.ml [new file with mode: 0644]
helm/software/components/cic_exportation/cicExportation.mli [new file with mode: 0644]
helm/software/configure.ac

diff --git a/helm/software/components/METAS/meta.helm-cic_exportation.src b/helm/software/components/METAS/meta.helm-cic_exportation.src
new file mode 100644 (file)
index 0000000..97124f9
--- /dev/null
@@ -0,0 +1,5 @@
+requires="helm-cic_proof_checking"
+version="0.0.1"
+archive(byte)="cic_exportation.cma"
+archive(native)="cic_exportation.cmxa"
+linkopts=""
index d30e63dcdd84b116564fba3cbf06457c301201ea..34020150a7d746942017adff28502cd3606fbab2 100644 (file)
@@ -19,6 +19,7 @@ MODULES =                     \
        getter                  \
        cic                     \
        cic_proof_checking      \
+       cic_exportation         \
        cic_acic                \
        metadata                \
        library                 \
diff --git a/helm/software/components/cic_exportation/.depend b/helm/software/components/cic_exportation/.depend
new file mode 100644 (file)
index 0000000..288ea5f
--- /dev/null
@@ -0,0 +1,2 @@
+cicExportation.cmo: cicExportation.cmi 
+cicExportation.cmx: cicExportation.cmi 
diff --git a/helm/software/components/cic_exportation/.depend.opt b/helm/software/components/cic_exportation/.depend.opt
new file mode 100644 (file)
index 0000000..288ea5f
--- /dev/null
@@ -0,0 +1,2 @@
+cicExportation.cmo: cicExportation.cmi 
+cicExportation.cmx: cicExportation.cmi 
diff --git a/helm/software/components/cic_exportation/Makefile b/helm/software/components/cic_exportation/Makefile
new file mode 100644 (file)
index 0000000..3062749
--- /dev/null
@@ -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/helm/software/components/cic_exportation/cicExportation.ml b/helm/software/components/cic_exportation/cicExportation.ml
new file mode 100644 (file)
index 0000000..8acb873
--- /dev/null
@@ -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/helm/software/components/cic_exportation/cicExportation.mli b/helm/software/components/cic_exportation/cicExportation.mli
new file mode 100644 (file)
index 0000000..07c2b88
--- /dev/null
@@ -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
index 3370b61b29bc4503ffe7969abb9d3ddcff234383..b2f218d0ffede96bd7b79718e0bc13037b7da629 100644 (file)
@@ -82,6 +82,7 @@ helm-acic_procedural \
 helm-content_pres \
 helm-hgdome \
 helm-tactics \
+helm-cic_exportation \
 "
 FINDLIB_CREQUIRES=" \
 $FINDLIB_COMREQUIRES \