]> matita.cs.unibo.it Git - helm.git/commitdiff
XXX this is the beginning of the metaocaml work XXX
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 25 Mar 2008 12:21:24 +0000 (12:21 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 25 Mar 2008 12:21:24 +0000 (12:21 +0000)
helm/software/components/cic_exportation/cicExportation.ml

index dd3be75721a55eb7f18705b89e586b5132945877..83b775eaea26f6ae6036463b53abc6cb4b8ade53 100644 (file)
 exception CicExportationInternalError;;
 exception NotEnoughElements;;
 
+(* *)
+
+let is_mcu_type u = 
+  UriManager.eq (UriManager.uri_of_string
+  "cic:/matita/freescale/opcode/mcu_type.ind") u
+;;
+
 (* Utility functions *)
 
 let analyze_term context t =
  match fst(CicTypeChecker.type_of_aux' [] context t CicUniv.oblivion_ugraph)with
-    Cic.Sort _ -> `Type
+  | Cic.Sort _ -> `Type
+  | Cic.MutInd (u,0,_) when is_mcu_type u -> `Optimize
   | ty -> 
      match
       fst (CicTypeChecker.type_of_aux' [] context ty CicUniv.oblivion_ugraph)
      with
-        Cic.Sort Cic.Prop -> `Proof
+     | Cic.Sort Cic.Prop -> `Proof
      | _ -> `Term
 ;;
 
@@ -45,11 +53,12 @@ let analyze_type context t =
  let rec aux =
   function
      Cic.Sort s -> `Sort s
+   | Cic.MutInd (u,0,_) when is_mcu_type u -> `Optimize
    | Cic.Prod (_,_,t) -> aux t
    | _ -> `SomethingElse
  in
  match aux t with
-    `Sort _ as res -> res
+    `Sort _ | `Optimize as res -> res
   | `SomethingElse ->
       match
        fst(CicTypeChecker.type_of_aux' [] context t CicUniv.oblivion_ugraph)
@@ -179,15 +188,17 @@ let rec pp ~in_type t context =
        (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
+         | `Optimize -> prerr_endline "XXX letin";assert false
+         | `Type
          | `Proof -> pp ~in_type t ((Some (b,Cic.Def (s,ty)))::context)
          | `Term ->
-            "(let " ^ ppname b ^ " : " ^ pp ~in_type:true ty context ^
+            "(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 ->
@@ -204,10 +215,10 @@ let rec pp ~in_type t context =
            C.InductiveDefinition (_,_,nparams,_) -> nparams
          | _ -> assert false in
        let hes = pp ~in_type he context in
-       let stl = String.concat "," (clean_args nparams context tl) 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) ^ ")"
+       "(" ^ String.concat " " (clean_args context li) ^ ")"
     | C.Const (uri,exp_named_subst) ->
        qualified_name_of_uri current_module_uri uri ^
         pp_exp_named_subst exp_named_subst context
@@ -260,13 +271,15 @@ let rec pp ~in_type t context =
                | [he] ->
                   pp ~in_type:false he context  (* singleton elimination *)
                | _ -> assert false)
+         | `Optimize 
          | `Term ->
             if patterns = [] then "assert false"
             else
-             (let connames_and_argsno =
+             (let connames_and_argsno, go_up, go_pu, go_down, go_nwod =
                (match fst(CicEnvironment.get_obj CicUniv.empty_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
@@ -284,6 +297,9 @@ let rec pp ~in_type t context =
                             (UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")),
                          count_prods paramsno ty
                       ) cons
+                    in
+                    if not (is_mcu_type uri) then rc, "","","",""
+                    else rc, "(.~(", "))", "( .< (", " ) >.)"
                  | _ -> raise CicExportationInternalError
                )
               in
@@ -296,6 +312,7 @@ let rec pp ~in_type t context =
                 in
                  combine (connames_and_argsno,patterns)
                in
+                go_up ^
                 "\n(match " ^ pp ~in_type:false te context ^ " with \n   " ^
                  (String.concat "\n | "
                   (List.map
@@ -312,7 +329,8 @@ let rec pp ~in_type t context =
                             bo
                           in
                            (match analyze_type context ty with
-                               `Statement
+                             | `Optimize -> prerr_endline "XXX contructor with l2 arg"; assert false
+                             | `Statement
                              | `Sort _ -> args,res
                              | `Type ->
                                  (match name with
@@ -331,13 +349,13 @@ let rec pp ~in_type t context =
                          x ^ (if sargs = "" then "" else "(" ^ sargs^ ")"),
                           body
                       in
-                       pattern ^ " -> " ^
-                        if needs_obj_magic then
+                       pattern ^ " -> " ^ go_down ^
+                        (if needs_obj_magic then
                          "Obj.magic (" ^ body ^ ")"
                         else
-                         body
+                         body) ^ go_nwod
                    ) connames_and_argsno_and_patterns)) ^
-                 ")\n")))
+                 ")\n"^go_pu)))
     | C.Fix (no, funs) ->
        let names,_ =
         List.fold_left
@@ -378,21 +396,43 @@ and pp_exp_named_subst exp_named_subst context =
      (function (uri,t) -> UriManager.name_of_uri uri ^ " \\Assign " ^ pp ~in_type:false t context)
      exp_named_subst
    ) ^ "]"
-and clean_args nparams context =
+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 -> 
+         "(.~(" :: pp ~in_type:false he context :: 
+                 pp ~in_type:false arg1 context :: ["))"], tl
+      | _ -> [], l
+    in
+    head_arg1 @ 
+    HExtlib.filter_map
+     (function t ->
+       match analyze_term context t with
+        | `Term -> Some (pp ~in_type:false t context)
+        | `Optimize -> 
+            prerr_endline "XXX function taking twice (or not as first) a l2 term"; assert false
+        | `Type
+        | `Proof -> None) rest
 and clean_args_for_ty context =
  HExtlib.filter_map
   (function t ->
     match analyze_term context t with
        `Type -> Some (pp ~in_type:true t context)
+     | `Optimize -> None
      | `Proof -> None
      | `Term -> None)
 in
@@ -411,7 +451,8 @@ let ppty current_module_uri =
         | Cic.Name n -> Cic.Name (String.uncapitalize n)
       in
        (match analyze_type context s with
-           `Statement
+         | `Optimize
+         | `Statement
          | `Sort Cic.Prop ->
              args (nparams - 1) ((Some (n,Cic.Decl s))::context) t
          | `Type when nparams > 0 ->
@@ -452,7 +493,8 @@ let pp_abstracted_ty current_module_uri =
         | Cic.Name n -> Cic.Name (String.uncapitalize n)
       in
        (match analyze_type context s with
-           `Statement
+         | `Optimize 
+         | `Statement
          | `Type
          | `Sort Cic.Prop ->
              args ((Some (n,Cic.Decl s))::context) t
@@ -470,7 +512,9 @@ let pp_abstracted_ty current_module_uri =
               res)
    | ty ->
      match analyze_type context ty with
-      `  Sort _
+      | `Optimize ->
+           prerr_endline "XXX abstracted l2 ty"; assert false
+      | `Sort _
       | `Statement -> raise DoNotExtract
       | `Type ->
           (* BUG HERE: this can be a real System F type *)
@@ -488,6 +532,7 @@ let ppinductiveType current_module_uri nparams (typename, inductive, arity, cons
 =
  match analyze_type [] arity with
     `Sort Cic.Prop -> ""
+  | `Optimize 
   | `Statement
   | `Type -> assert false
   | `Sort _ ->
@@ -519,12 +564,31 @@ let ppobj current_module_uri obj =
   match obj with
     C.Constant (name, Some t1, t2, params, _) ->
       (match analyze_type [] t2 with
-          `Sort Cic.Prop
+        | `Optimize -> prerr_endline "XXX definition of an l2 term"; assert false
+        | `Sort Cic.Prop
         | `Statement -> ""
-        | `Type -> "let " ^ ppid name ^ " =\n" ^ pp ~in_type:false t1 [] ^ "\n"
+        | `Type -> 
+            (match t1 with
+            | Cic.Lambda (Cic.Name arg, s, t) ->
+                            (match analyze_type [] s with
+                | `Optimize -> 
+                    "let " ^ ppid name ^ "__1 = function " ^ ppid arg 
+                    ^ " -> .< " ^ pp ~in_type:false t [Some (Cic.Name arg, Cic.Decl s)] 
+                    ^ " >. ;;\n"
+                    ^ "let " ^ ppid name ^ "__2 = ref ([] : (unit*unit) list);;\n"
+                    ^ "let " ^ ppid name ^ " = function " ^ ppid arg
+                    ^ " -> (try ignore (List.assoc "^ppid arg^"(Obj.magic  !"^ppid name
+                    ^"__2)) with Not_found -> "^ppid name^"__2 := ("
+                    ^ ppid arg^",Obj.magic (.! ("^ppid name^"__1 "^ppid arg^")))::!"
+                    ^ppid name^"__2); .< List.assoc "^ppid arg^" (Obj.magic (!"
+                    ^ppid name^"__2) >.\n"
+                | _ -> 
+                   "let " ^ ppid name ^ " =\n" ^ pp ~in_type:false t1 [] ^ "\n")
+            | _ -> "let " ^ ppid name ^ " =\n" ^ pp ~in_type:false t1 [] ^ "\n")
         | `Sort _ ->
             match analyze_type [] t1 with
                `Sort Cic.Prop -> ""
+             | `Optimize -> prerr_endline "XXX aliasing l2 type"; assert false
              | _ ->
                (try
                  let abstr,res = pp_abstracted_ty current_module_uri [] t1 in
@@ -538,6 +602,7 @@ let ppobj current_module_uri obj =
    | C.Constant (name, None, ty, params, _) ->
       (match analyze_type [] ty with
           `Sort Cic.Prop
+        | `Optimize -> prerr_endline "XXX axiom l2"; assert false
         | `Statement -> ""
         | `Sort _ -> "type " ^ ppid name ^ "\n"
         | `Type -> "let " ^ ppid name ^ " = assert false\n")