From c6d209785043d1dc2c5d315473dcbe6ff3f2067e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 25 Mar 2008 12:21:24 +0000 Subject: [PATCH] XXX this is the beginning of the metaocaml work XXX --- .../cic_exportation/cicExportation.ml | 103 ++++++++++++++---- 1 file changed, 84 insertions(+), 19 deletions(-) diff --git a/helm/software/components/cic_exportation/cicExportation.ml b/helm/software/components/cic_exportation/cicExportation.ml index dd3be7572..83b775eae 100644 --- a/helm/software/components/cic_exportation/cicExportation.ml +++ b/helm/software/components/cic_exportation/cicExportation.ml @@ -28,16 +28,24 @@ 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 0 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") -- 2.39.2