(match s with
C.Prop -> "Prop"
| C.Set -> "Set"
- | C.Type _ -> "Type" (* TASSI: universe is not explicit *)
+ | 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 -> "(" ^ n ^ ":" ^ pp s l ^ ")" ^ pp t ((Some b)::l)
| C.Anonymous -> "(" ^ pp s l ^ "->" ^ pp t ((Some b)::l) ^ ")"
)
- | C.Cast (v,t) -> pp v l
+ | C.Cast (v,t) -> "(" ^ pp v l ^ ":" ^ pp t l ^ ")"
| C.Lambda (b,s,t) ->
"[" ^ ppname b ^ ":" ^ pp s l ^ "]" ^ pp t ((Some b)::l)
| C.LetIn (b,s,t) ->
UriManager.name_of_uri uri ^ pp_exp_named_subst exp_named_subst l
| C.MutInd (uri,n,exp_named_subst) ->
(try
- match CicEnvironment.get_obj uri with
- C.InductiveDefinition (dl,_,_) ->
+ match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
+ C.InductiveDefinition (dl,_,_,_) ->
let (name,_,_,_) = get_nth dl (n+1) in
name ^ pp_exp_named_subst exp_named_subst l
| _ -> raise CicPpInternalError
)
| C.MutConstruct (uri,n1,n2,exp_named_subst) ->
(try
- match CicEnvironment.get_obj uri with
- C.InductiveDefinition (dl,_,_) ->
+ 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
id ^ pp_exp_named_subst exp_named_subst l
)
| C.MutCase (uri,n1,ty,te,patterns) ->
let connames =
- (match CicEnvironment.get_obj uri with
- C.InductiveDefinition (dl,_,_) ->
+ (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
+ C.InductiveDefinition (dl,_,_,_) ->
let (_,_,_,cons) = get_nth dl (n1+1) in
List.map (fun (id,_) -> id) cons
| _ -> raise CicPpInternalError
let module C = Cic in
let module U = UriManager in
match obj with
- C.Constant (name, Some t1, t2, params) ->
+ C.Constant (name, Some t1, t2, params, _) ->
"Definition of " ^ name ^
"(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
")" ^ ":\n" ^ pp t1 [] ^ " : " ^ pp t2 []
- | C.Constant (name, None, ty, params) ->
+ | C.Constant (name, None, ty, params, _) ->
"Axiom " ^ name ^
"(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
"):\n" ^ pp ty []
- | C.Variable (name, bo, ty, params) ->
+ | 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) ->
+ | C.CurrentProof (name, conjectures, value, ty, params, _) ->
"Current Proof of " ^ name ^
"(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
")" ^ ":\n" ^
pp t name_context ^ "\n" ^ i
) conjectures "" ^
"\n" ^ pp value [] ^ " : " ^ pp ty []
- | C.InductiveDefinition (l, params, nparams) ->
+ | C.InductiveDefinition (l, params, nparams, _) ->
"Parameters = " ^
String.concat ";" (List.map UriManager.string_of_uri params) ^ "\n" ^
"NParams = " ^ string_of_int nparams ^ "\n" ^
List.fold_right (fun x i -> ppinductiveType x ^ i) l ""
;;
+
+let ppsort = function
+ | Cic.Prop -> "Prop"
+ | Cic.Set -> "Set"
+ | Cic.Type _ -> "Type"
+ | Cic.CProp -> "CProp"
+
+
+(* MATITA NAMING CONVENTION *)
+
+let check_name ctx name term =
+ let cut_off_name name string_name =
+ let len = String.length name in
+ let len1 = String.length string_name in
+ if len <= len1 then
+ begin
+ let head = String.sub string_name 0 len in
+ if ((String.compare head name)=0) ||
+ ((String.compare head (String.lowercase name))=0) then
+ begin
+ let diff = len1-len in
+ let tail = String.sub string_name len diff in
+ if ((diff > 0) && (String.rcontains_from tail 0 '_')) then
+ String.sub tail 1 (diff-1)
+ else tail
+ end
+ else string_name
+ end
+ else string_name in
+ let rec check_aux ctx string_name =
+ function
+ | Cic.Rel m ->
+ (match List.nth ctx (m-1) with
+ Cic.Name name ->
+ cut_off_name name string_name
+ | Cic.Anonymous -> string_name)
+ | Cic.Meta _ -> string_name
+ | Cic.Sort sort -> cut_off_name (ppsort sort) string_name
+ | Cic.Implicit _ -> string_name
+ | Cic.Cast (te,ty) -> check_aux ctx string_name te
+ | Cic.Prod (name,so,dest) ->
+ let string_name = check_aux ctx string_name so in
+ check_aux (name::ctx) string_name dest
+ | Cic.Lambda (name,so,dest) ->
+ let string_name =
+ match name with
+ Cic.Anonymous -> string_name
+ | Cic.Name name -> cut_off_name name string_name in
+ let string_name = check_aux ctx string_name so in
+ check_aux (name::ctx) string_name dest
+ | Cic.LetIn (name,so,dest) ->
+ let string_name = check_aux ctx string_name so in
+ check_aux (name::ctx) string_name dest
+ | Cic.Appl l ->
+ List.fold_left (check_aux ctx) string_name l
+ | Cic.Var (uri,exp_named_subst) ->
+ let name = UriManager.name_of_uri uri in
+ cut_off_name name string_name
+ | Cic.Const (uri,exp_named_subst) ->
+ let name = UriManager.name_of_uri uri in
+ cut_off_name name string_name
+ | Cic.MutInd (uri,_,exp_named_subst) ->
+ let name = UriManager.name_of_uri uri in
+ cut_off_name name string_name
+ | Cic.MutConstruct (uri,n,m,exp_named_subst) ->
+ let name =
+ (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
+ Cic.InductiveDefinition (dl,_,_,_) ->
+ let (_,_,_,cons) = get_nth dl (n+1) in
+ let (id,_) = get_nth cons m in
+ id
+ | _ -> assert false) in
+ cut_off_name name string_name
+ | Cic.MutCase (_,_,_,te,pl) ->
+ let strig_name = cut_off_name "match" string_name in
+ let string_name = check_aux ctx string_name te in
+ List.fold_right (fun t s -> check_aux ctx s t) pl string_name
+ | Cic.Fix (_,fl) ->
+ let strig_name = cut_off_name "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)
+ in
+ List.fold_right
+ (fun (_,_,_,bo) s -> check_aux (onames@ctx) s bo) fl string_name
+ | Cic.CoFix (_,fl) ->
+ let strig_name = cut_off_name "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)
+ in
+ List.fold_right
+ (fun (_,_,bo) s -> check_aux (onames@ctx) s bo) fl string_name
+ in
+ if (String.length (check_aux ctx name term) = 0) then true
+ else false
+
+let rec check_names ctx hyp_names conclusion_name t =
+ match t with
+ | Cic.Prod (name,s,t) ->
+ (match hyp_names with
+ [] -> check_names (name::ctx) hyp_names conclusion_name t
+ | hd::tl ->
+ if check_name ctx hd s then
+ check_names (name::ctx) tl conclusion_name t
+ else
+ check_names (name::ctx) hyp_names conclusion_name t)
+ | _ ->
+ hyp_names=[] && (check_name ctx conclusion_name t)
+
+let check name term =
+ let names = Str.split (Str.regexp_string "_to_") name in
+ let hyp_names,conclusion_name =
+ match List.rev names with
+ [] -> assert false
+ | hd::tl -> (List.rev tl),hd in
+ check_names [] hyp_names conclusion_name term
+;;
+
+
projects / helm.git / blobdiff