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
| C.Set -> "Set"
| C.Type _ -> "Type"
(*| C.Type u -> ("Type" ^ CicUniv.string_of_universe u)*)
- | C.CProp -> "CProp"
+ | C.CProp _ -> "CProp"
)
| C.Implicit (Some `Hole) -> "%"
| C.Implicit _ -> "?"
pp ~in_type t ((Some (b,Cic.Decl s))::context) ^ ")")
| C.LetIn (b,s,ty,t) ->
(match analyze_term context s with
- | `Optimize -> prerr_endline "XXX letin";assert false
| `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 " ^
(if stl = "" then "" else "(" ^ stl ^ ") ") ^ hes
| C.Appl (C.MutConstruct (uri,n,_,_) as he::tl) ->
let nparams =
- match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
+ 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
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
+ 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 current_module_uri
)
| C.MutConstruct (uri,n1,n2,exp_named_subst) ->
(try
- match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
+ 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
if in_type then
"unit (* TOO POLYMORPHIC TYPE *)"
else (
- let needs_obj_magic =
- (* BUG HERE: we should consider also the right parameters *)
+ let rec needs_obj_magic ty =
match CicReduction.whd context ty with
- Cic.Lambda (_,_,t) -> not (DoubleTypeInference.does_not_occur 1 t)
+ | 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 ->
if patterns = [] then "assert false"
else
(let connames_and_argsno, go_up, go_pu, go_down, go_nwod =
- (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
+ (match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
C.InductiveDefinition (dl,_,paramsno,_) ->
let (_,_,_,cons) = get_nth dl (n1+1) in
let rc =
) cons
in
if not (is_mcu_type uri) then rc, "","","",""
- else rc, "(.~(", "))", "( .< (", " ) >.)"
+ else rc, !current_go_up, "))", "( .< (", " ) >.)"
| _ -> raise CicExportationInternalError
)
in
let head_arg1, rest =
match analyze_term context arg1 with
| `Optimize ->
- "(.~(" :: pp ~in_type:false he context ::
+ !current_go_up :: pp ~in_type:false he context ::
pp ~in_type:false arg1 context :: ["))"], tl
| _ -> [], l
in
match obj with
C.Constant (name, Some t1, t2, params, _) ->
(match analyze_type [] t2 with
- | `Optimize -> prerr_endline "XXX definition of an l2 term"; assert false
| `Sort Cic.Prop
| `Statement -> ""
+ | `Optimize
| `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)]
+ ^ " -> .< " ^
+ at_level2 (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 ^ "__2 = ref ([] : (unit list*unit list) 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^")))::!"
+ ^ " -> (try ignore (List.assoc "^ppid arg^" (Obj.magic !"^ppid name
+ ^"__2)) with Not_found -> "^ppid name^"__2 := (Obj.magic ("
+ ^ ppid arg^",.! ("^ppid name^"__1 "^ppid arg^")))::!"
^ppid name^"__2); .< List.assoc "^ppid arg^" (Obj.magic (!"
- ^ppid name^"__2) >.\n"
+ ^ppid name^"__2)) >.\n;;\n"
+ ^" let xxx = prerr_endline \""^ppid name^"\"; .!("^ppid
+ name^" Matita_freescale_opcode.HCS08)"
| _ ->
"let " ^ ppid name ^ " =\n" ^ pp ~in_type:false t1 [] ^ "\n")
| _ -> "let " ^ ppid name ^ " =\n" ^ pp ~in_type:false t1 [] ^ "\n")