(* 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 l =
let module C = Cic in
match t with
| C.Var (uri,exp_named_subst) ->
UriManager.string_of_uri (*UriManager.name_of_uri*) uri ^ pp_exp_named_subst exp_named_subst l
| C.Meta (n,l1) ->
- "?" ^ (string_of_int n) ^ "[" ^
- String.concat " ; "
- (List.rev_map (function None -> "_" | Some t -> pp t l) l1) ^
- "]"
+ (match metasenv with
+ None ->
+ "?" ^ (string_of_int n) ^ "[" ^
+ String.concat " ; "
+ (List.rev_map (function None -> "_" | Some t -> pp t l) 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 l
+ ) context l1)) ^
+ "]"
+ with
+ CicUtil.Meta_not_found _
+ | Invalid_argument _ ->
+ "???" ^ (string_of_int n) ^ "[" ^
+ String.concat " ; "
+ (List.rev_map (function None -> "_" | Some t -> pp t l) 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.CProp _ -> "CProp"
)
| C.Implicit (Some `Hole) -> "%"
| C.Implicit _ -> "?"
| C.Prod (b,s,t) ->
(match b with
- C.Name n -> "(" ^ n ^ ":" ^ pp s l ^ ")" ^ pp t ((Some b)::l)
- | C.Anonymous -> "(" ^ pp s l ^ "->" ^ pp t ((Some b)::l) ^ ")"
+ C.Name n -> "(\\forall " ^ n ^ ":" ^ pp s l ^ "." ^ pp t ((Some b)::l) ^ ")"
+ | C.Anonymous -> "(" ^ pp s l ^ "\\to " ^ pp t ((Some b)::l) ^ ")"
)
| C.Cast (v,t) -> "(" ^ pp v l ^ ":" ^ pp t l ^ ")"
| C.Lambda (b,s,t) ->
"(\\lambda " ^ ppname b ^ ":" ^ pp s l ^ "." ^ pp t ((Some b)::l) ^ ")"
- | C.LetIn (b,s,t) ->
- "[" ^ ppname b ^ ":=" ^ pp s l ^ "]" ^ pp t ((Some b)::l)
+ | C.LetIn (b,s,ty,t) ->
+ " let " ^ ppname b ^ ": " ^ pp ty l ^ " \\def " ^ pp s l ^ " in " ^ pp t ((Some b)::l)
| C.Appl li ->
"(" ^
(List.fold_right
name ^ pp_exp_named_subst exp_named_subst l
| _ -> raise CicPpInternalError
with
- _ -> UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n + 1)
+ 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
id ^ pp_exp_named_subst exp_named_subst l
| _ -> raise CicPpInternalError
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 =
+ let connames_and_argsno =
(match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
- C.InductiveDefinition (dl,_,_,_) ->
+ C.InductiveDefinition (dl,_,paramsno,_) ->
let (_,_,_,cons) = get_nth dl (n1+1) in
- List.map (fun (id,_) -> id) cons
+ 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
+ id, count_prods paramsno ty
+ ) cons
| _ -> raise CicPpInternalError
)
in
- let connames_and_patterns =
+ let connames_and_argsno_and_patterns =
let rec combine =
function
[],[] -> []
- | [],l -> List.map (fun x -> "???",Some x) l
- | l,[] -> List.map (fun x -> x,None) l
- | x::tlx,y::tly -> (x,Some y)::(combine (tlx,tly))
+ | [],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,patterns)
+ combine (connames_and_argsno,patterns)
in
- "\n<" ^ pp ty l ^ ">Cases " ^ pp te l ^ " of " ^
- List.fold_right
- (fun (x,y) i -> "\n " ^ x ^ " => " ^
- (match y with None -> "" | Some y -> pp y l) ^ i)
- connames_and_patterns "" ^
- "\nend"
+ "\nmatch " ^ pp te l ^ " return " ^ pp ty l ^ " with \n [ " ^
+ (String.concat "\n | "
+ (List.map
+ (fun (x,argsno,y) ->
+ let rec aux argsno l =
+ function
+ Cic.Lambda (name,ty,bo) when argsno > 0 ->
+ let args,res = aux (argsno - 1) (Some name::l) bo in
+ ("(" ^ (match name with C.Anonymous -> "_" | C.Name s -> s)^
+ ":" ^ pp ty l ^ ")")::args, res
+ | t when argsno = 0 -> [],pp t l
+ | t -> ["{" ^ string_of_int argsno ^ " args missing}"],pp t l
+ in
+ let pattern,body =
+ match y with
+ None -> x,""
+ | Some y when argsno = 0 -> x,pp y l
+ | Some y ->
+ let args,body = aux argsno l y in
+ "(" ^ x ^ " " ^ String.concat " " args ^ ")",body
+ in
+ pattern ^ " => " ^ body
+ ) connames_and_argsno_and_patterns)) ^
+ "\n]"
| C.Fix (no, funs) ->
let snames = List.map (fun (name,_,_,_) -> name) funs in
let names =
(function (uri,t) -> UriManager.name_of_uri uri ^ " \\Assign " ^ pp t l)
exp_named_subst
) ^ "]"
+in
+ pp
;;
-let ppterm t =
- pp t []
+let ppterm ?metasenv t =
+ pp ?metasenv t []
;;
(* ppinductiveType (typename, inductive, arity, cons) *)
cons ""
;;
-let ppcontext ?(sep = "\n") context =
+let ppcontext ?metasenv ?(sep = "\n") context =
let separate s = if s = "" then "" else s ^ sep in
fst (List.fold_right
(fun context_entry (i,name_context) ->
match context_entry with
Some (n,Cic.Decl t) ->
Printf.sprintf "%s%s : %s" (separate i) (ppname n)
- (pp t name_context), (Some n)::name_context
+ (pp ?metasenv t name_context), (Some n)::name_context
| Some (n,Cic.Def (bo,ty)) ->
Printf.sprintf "%s%s : %s := %s" (separate i) (ppname n)
- (match ty with
- None -> "_"
- | Some ty -> pp ty name_context)
- (pp bo name_context), (Some n)::name_context
+ (pp ?metasenv ty name_context)
+ (pp ?metasenv bo name_context), (Some n)::name_context
| None ->
Printf.sprintf "%s_ :? _" (separate i), None::name_context
) context ("",[]))
(fun context_entry (i,name_context) ->
(match context_entry with
Some (n,C.Decl at) ->
- (separate i) ^
- ppname n ^ ":" ^ pp at name_context ^ " ",
- (Some n)::name_context
- | Some (n,C.Def (at,None)) ->
- (separate i) ^
- ppname n ^ ":= " ^ pp at name_context ^ " ",
- (Some n)::name_context
- | None ->
- (separate i) ^ "_ :? _ ", None::name_context
- | _ -> assert false)
+ (separate i) ^
+ ppname n ^ ":" ^
+ pp ~metasenv:conjectures at name_context ^ " ",
+ (Some n)::name_context
+ | Some (n,C.Def (at,aty)) ->
+ (separate i) ^
+ ppname n ^ ": " ^
+ pp ~metasenv:conjectures aty name_context ^
+ ":= " ^ pp ~metasenv:conjectures
+ at name_context ^ " ",
+ (Some n)::name_context
+ | None ->
+ (separate i) ^ "_ :? _ ", None::name_context)
) context ("",[])
in
conjectures' ^ " |- " ^ "?" ^ (string_of_int n) ^ ": " ^
- pp t name_context ^ "\n" ^ i
+ pp ~metasenv:conjectures t name_context ^ "\n" ^ i
) conjectures "" ^
- "\n" ^ pp value [] ^ " : " ^ pp ty []
+ "\n" ^ pp ~metasenv:conjectures value [] ^ " : " ^
+ pp ~metasenv:conjectures ty []
| C.InductiveDefinition (l, params, nparams, _) ->
"Parameters = " ^
String.concat ";" (List.map UriManager.string_of_uri params) ^ "\n" ^
| Cic.Prop -> "Prop"
| Cic.Set -> "Set"
| Cic.Type _ -> "Type"
- | Cic.CProp -> "CProp"
+ | Cic.CProp _ -> "CProp"
(* MATITA NAMING CONVENTION *)
else None
let remove_prefix prefix (last,string) =
- if prefix="append" then
- begin
- prerr_endline last;
- prerr_endline string;
- end;
if string = "" then (last,string)
else
match is_prefix prefix string with
| Cic.Cast (te,ty) -> check_rec ctx string_name te
| Cic.Prod (name,so,dest) ->
let l_string_name = check_rec ctx string_name so in
- check_rec (name::ctx) string_name dest
+ check_rec (name::ctx) l_string_name dest
| Cic.Lambda (name,so,dest) ->
let string_name =
match name with
| Cic.Name name -> remove_prefix name string_name in
let l_string_name = check_rec ctx string_name so in
check_rec (name::ctx) l_string_name dest
- | Cic.LetIn (name,so,dest) ->
+ | Cic.LetIn (name,so,_,dest) ->
let string_name = check_rec ctx string_name so in
check_rec (name::ctx) string_name dest
| Cic.Appl l ->
| _ -> assert false) in
remove_prefix name string_name
| Cic.MutCase (_,_,_,te,pl) ->
- let strig_name = remove_prefix "match" string_name in
+ let string_name = remove_prefix "match" string_name in
let string_name = check_rec ctx string_name te in
List.fold_right (fun t s -> check_rec ctx s t) pl string_name
| Cic.Fix (_,fl) ->
- let strig_name = remove_prefix "fix" string_name in
+ let string_name = remove_prefix "fix" string_name in
let names = List.map (fun (name,_,_,_) -> name) fl in
let onames =
List.rev (List.map (function name -> Cic.Name name) names)
List.fold_right
(fun (_,_,_,bo) s -> check_rec (onames@ctx) s bo) fl string_name
| Cic.CoFix (_,fl) ->
- let strig_name = remove_prefix "cofix" string_name in
+ let string_name = remove_prefix "cofix" string_name in
let names = List.map (fun (name,_,_) -> name) fl in
let onames =
List.rev (List.map (function name -> Cic.Name name) names)
hyp_names=[] && check_name ~allow_suffix:true ctx conclusion_name t
let check name term =
-(* prerr_endline name;
- prerr_endline (ppterm term); *)
let names = Str.split (Str.regexp_string "_to_") name in
let hyp_names,conclusion_name =
match List.rev names with
projects / helm.git / blobdiff