| Ast.Sort `Set -> "Set"
| Ast.Sort `Prop -> "Prop"
| Ast.Sort (`Type _) -> "Type"
- | Ast.Sort `CProp -> "CProp"
+ | Ast.Sort (`CProp _)-> "CProp"
| Ast.Symbol (name, _) -> "'" ^ name
| Ast.UserInput -> ""
type binder_kind = [ `Lambda | `Pi | `Exists | `Forall ]
type induction_kind = [ `Inductive | `CoInductive ]
-type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp ]
+type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of CicUniv.universe]
type fold_kind = [ `Left | `Right ]
type location = Stdpp.location
| Cic.ASort (id,Cic.Prop) -> idref id (Ast.Sort `Prop)
| Cic.ASort (id,Cic.Set) -> idref id (Ast.Sort `Set)
| Cic.ASort (id,Cic.Type u) -> idref id (Ast.Sort (`Type u))
- | Cic.ASort (id,Cic.CProp) -> idref id (Ast.Sort `CProp)
+ | Cic.ASort (id,Cic.CProp u) -> idref id (Ast.Sort (`CProp u))
| Cic.AImplicit (id, Some `Hole) -> idref id Ast.UserInput
| Cic.AImplicit (id, _) -> idref id Ast.Implicit
| Cic.AProd (id,n,s,t) ->
let binder_kind =
match sort_of_id id with
| `Set | `Type _ -> `Pi
- | `Prop | `CProp -> `Forall
+ | `Prop | `CProp _ -> `Forall
in
idref id (Ast.Binder (binder_kind,
(CicNotationUtil.name_of_cic_name n, Some (k s)), k t))
let ext = match get_tail context (get_type context ty) with
| C.Sort C.Prop -> "_ind"
| C.Sort C.Set -> "_rec"
- | C.Sort C.CProp -> "_rec"
+ | C.Sort (C.CProp _) -> "_rect"
| C.Sort (C.Type _) -> "_rect"
| t ->
Printf.eprintf "CicPPP get_default_eliminator: %s\n" (Pp.ppterm t);
Prop
| Set
| Type of CicUniv.universe
- | CProp
+ | CProp of CicUniv.universe
type name =
| Name of string
let sort_of_string ctxt = function
| "Prop" -> Cic.Prop
- | "CProp" -> Cic.CProp
(* THIS CASE IS HERE ONLY TO ALLOW THE PARSING OF COQ LIBRARY
* THIS SHOULD BE REMOVED AS SOON AS univ_maker OR COQ'S EXPORTATION
* IS FIXED *)
+ | "CProp" -> Cic.CProp (CicUniv.fresh ~uri:ctxt.uri ())
| "Type" -> Cic.Type (CicUniv.fresh ~uri:ctxt.uri ())
| "Set" when !impredicative_set -> Cic.Set
| "Set" -> Cic.Type (CicUniv.fresh ~uri:ctxt.uri ())
| s ->
let len = String.length s in
- if not(len > 5) then parse_error ctxt "sort expected";
- if not(String.sub s 0 5 = "Type:") then parse_error ctxt "sort expected";
- let s = String.sub s 5 (len - 5) in
+ let sort_len, mk_sort =
+ if len > 5 && String.sub s 0 5 = "Type:" then 5,fun x -> Cic.Type x
+ else if len > 6 && String.sub s 0 6 = "CProp:" then 6,fun x->Cic.CProp x
+ else parse_error ctxt "sort expected"
+ in
+ let s = String.sub s sort_len (len - sort_len) in
let i = String.index s ':' in
let id = int_of_string (String.sub s 0 i) in
- let suri = String.sub s (i+1) (len - 5 - i - 1) in
+ let suri = String.sub s (i+1) (len - sort_len - i - 1) in
let uri = UriManager.uri_of_string suri in
- try Cic.Type (CicUniv.fresh ~uri ~id ())
+ try mk_sort (CicUniv.fresh ~uri ~id ())
with
| Failure "int_of_string"
| Invalid_argument _ -> parse_error ctxt "sort expected"
(* $Id$ *)
-type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp ]
+type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of CicUniv.universe ]
let string_of_sort = function
| `Prop -> "Prop"
| `Set -> "Set"
| `Type u -> "Type:" ^ string_of_int (CicUniv.univno u) ^ ":" ^ UriManager.string_of_uri (CicUniv.univuri u)
- | `CProp -> "CProp"
+ | `CProp u -> "CProp:" ^ string_of_int (CicUniv.univno u) ^ ":" ^ UriManager.string_of_uri (CicUniv.univuri u)
+
let sort_of_sort = function
| Cic.Prop -> `Prop
| Cic.Set -> `Set
| Cic.Type u -> `Type u
- | Cic.CProp -> `CProp
+ | Cic.CProp u -> `CProp u
(* let hashtbl_add_time = ref 0.0;; *)
| C.Sort C.Set -> `Set
| C.Sort (C.Type u) -> `Type u
| C.Meta _ -> `Type (CicUniv.fresh())
- | C.Sort C.CProp -> `CProp
+ | C.Sort (C.CProp u) -> `CProp u
| t ->
prerr_endline ("Cic2acic.sort_of applied to: " ^ CicPp.ppterm t) ;
assert false
{annsynthesized : Cic.annterm ; annexpected : Cic.annterm option}
;;
-type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp ]
+type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of CicUniv.universe]
val string_of_sort: sort_kind -> string
(*val sort_of_string: string -> sort_kind*)
let t1' = CicReduction.whd context t1 in
let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in
match (t1', t2') with
- (C.Sort _, C.Sort s2)
- when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
- (* different from Coq manual!!! *)
- C.Sort s2
- | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
- C.Sort (C.Type (CicUniv.fresh()))
- | (C.Sort _,C.Sort (C.Type t1)) ->
- (* TASSI: CONSRTAINTS: the same in cictypechecker,cicrefine *)
- C.Sort (C.Type t1) (* c'e' bisogno di un fresh? *)
+ | (C.Sort _, C.Sort s2) when (s2 = C.Prop || s2 = C.Set) -> C.Sort s2
+ | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->C.Sort(C.Type(CicUniv.fresh()))
+ | (C.Sort _,C.Sort (C.Type t1)) -> C.Sort (C.Type t1)
+ | (C.Sort _,C.Sort (C.CProp t1)) -> C.Sort (C.CProp t1)
| (C.Meta _, C.Sort _) -> t2'
| (C.Meta _, (C.Meta (_,_) as t))
| (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t ->
| CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop
| CicNotationPt.Sort `Set -> Cic.Sort Cic.Set
| CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u)
- | CicNotationPt.Sort `CProp -> Cic.Sort Cic.CProp
+ | CicNotationPt.Sort (`CProp u) -> Cic.Sort (Cic.CProp u)
| CicNotationPt.Symbol (symbol, instance) ->
resolve env (Symbol (symbol, instance)) ()
| _ -> assert false (* god bless Bologna *)
| 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.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 _ -> "?"
| Cic.Prop -> "Prop"
| Cic.Set -> "Set"
| Cic.Type _ -> "Type"
- | Cic.CProp -> "CProp"
+ | Cic.CProp _ -> "CProp"
(* MATITA NAMING CONVENTION *)
*)
aux test_equality_only context t1 term' ugraph
with CicUtil.Subst_not_found _ -> false,ugraph)
- (* TASSI: CONSTRAINTS *)
- | (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only ->
+ | (C.Sort (C.Type t1), C.Sort (C.Type t2))
+ | (C.Sort (C.CProp t1), C.Sort (C.CProp t2)) when test_equality_only ->
(try
true,(CicUniv.add_eq t2 t1 ugraph)
with CicUniv.UniverseInconsistency _ -> false,ugraph)
- (* TASSI: CONSTRAINTS *)
- | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
+ | (C.Sort (C.Type t1), C.Sort (C.Type t2))
+ | (C.Sort (C.CProp t1), C.Sort (C.CProp t2)) ->
(try
true,(CicUniv.add_ge t2 t1 ugraph)
with CicUniv.UniverseInconsistency _ -> false,ugraph)
- (* TASSI: CONSTRAINTS *)
- | (C.Sort s1, C.Sort (C.Type _)) -> (not test_equality_only),ugraph
- (* TASSI: CONSTRAINTS *)
+ | (C.Sort (C.CProp t1), C.Sort (C.Type t2)) when not test_equality_only ->
+ (try
+ true,(CicUniv.add_gt t2 t1 ugraph)
+ with CicUniv.UniverseInconsistency _ -> false,ugraph)
+ | (C.Sort (C.Type t1), C.Sort (C.CProp t2)) when not test_equality_only ->
+ (try
+ true,(CicUniv.add_ge t2 t1 ugraph)
+ with CicUniv.UniverseInconsistency _ -> false,ugraph)
+ | (C.Sort s1, C.Sort (C.Type _))
+ | (C.Sort s1, C.Sort (C.CProp _)) -> (not test_equality_only),ugraph
| (C.Sort s1, C.Sort s2) -> (s1 = s2),ugraph
| (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
let b',ugraph' = aux true context s1 s2 ugraph in
match
CicReduction.whd context con_sort, CicReduction.whd [] ty_sort
with
- Cic.Sort (Cic.Type u1), Cic.Sort (Cic.Type u2) ->
+ Cic.Sort (Cic.Type u1), Cic.Sort (Cic.Type u2)
+ | Cic.Sort (Cic.CProp u1), Cic.Sort (Cic.CProp u2)
+ | Cic.Sort (Cic.Type u1), Cic.Sort (Cic.CProp u2) ->
CicUniv.add_ge u2 u1 ugraph
+ | Cic.Sort (Cic.CProp u1), Cic.Sort (Cic.Type u2) ->
+ CicUniv.add_gt u2 u1 ugraph
| Cic.Sort _, Cic.Sort Cic.Prop
+ | Cic.Sort _, Cic.Sort Cic.CProp _
| Cic.Sort _, Cic.Sort Cic.Set
- | Cic.Sort Cic.CProp, Cic.Sort Cic.CProp
| Cic.Sort _, Cic.Sort Cic.Type _ -> ugraph
| a,b ->
raise
((Some (name,C.Decl so))::context) ta true
| (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true,ugraph
| (C.Sort C.Prop, C.Sort C.Set)
- | (C.Sort C.Prop, C.Sort C.CProp)
+ | (C.Sort C.Prop, C.Sort (C.CProp _))
| (C.Sort C.Prop, C.Sort (C.Type _) ) when need_dummy ->
(let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
UriManager.string_of_uri uri)))
)
| (C.Sort C.Set, C.Sort C.Prop) when need_dummy -> true , ugraph
- | (C.Sort C.CProp, C.Sort C.Prop) when need_dummy -> true , ugraph
| (C.Sort C.Set, C.Sort C.Set) when need_dummy -> true , ugraph
- | (C.Sort C.Set, C.Sort C.CProp) when need_dummy -> true , ugraph
- | (C.Sort C.CProp, C.Sort C.Set) when need_dummy -> true , ugraph
- | (C.Sort C.CProp, C.Sort C.CProp) when need_dummy -> true , ugraph
- | ((C.Sort C.Set, C.Sort (C.Type _)) | (C.Sort C.CProp, C.Sort (C.Type _)))
+ | (C.Sort C.Set, C.Sort (C.Type _))
+ | (C.Sort C.Set, C.Sort (C.CProp _))
when need_dummy ->
(let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
UriManager.string_of_uri uri)))
)
| (C.Sort (C.Type _), C.Sort _) when need_dummy -> true , ugraph
+ | (C.Sort (C.CProp _), C.Sort _) when need_dummy -> true , ugraph
| (_,_) -> false,ugraph
in
check_allowed_sort_elimination_aux ugraph context arity2 need_dummy
| (C.Sort s1, C.Sort (C.Prop | C.Set)) ->
(* different from Coq manual!!! *)
t2',ugraph
- | (C.Sort (C.Prop | C.Set | C.CProp), C.Sort C.CProp ) -> t2', ugraph
| (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
- (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
let t' = CicUniv.fresh() in
(try
let ugraph1 = CicUniv.add_ge t' t1 ugraph in
C.Sort (C.Type t'),ugraph2
with
CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg))
- | (C.Sort _,C.Sort (C.Type t1))
- | (C.Sort (C.Type t1), C.Sort C.CProp) ->
- (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
- C.Sort (C.Type t1),ugraph (* c'e' bisogno di un fresh? *)
+ | (C.Sort (C.CProp t1), C.Sort (C.CProp t2)) ->
+ let t' = CicUniv.fresh() in
+ (try
+ let ugraph1 = CicUniv.add_ge t' t1 ugraph in
+ let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
+ C.Sort (C.CProp t'),ugraph2
+ with
+ CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg))
+ | (C.Sort (C.Type t1), C.Sort (C.CProp t2)) ->
+ let t' = CicUniv.fresh() in
+ (try
+ let ugraph1 = CicUniv.add_ge t' t1 ugraph in
+ let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
+ C.Sort (C.CProp t'),ugraph2
+ with
+ CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg))
+ | (C.Sort (C.CProp t1), C.Sort (C.Type t2)) ->
+ let t' = CicUniv.fresh() in
+ (try
+ let ugraph1 = CicUniv.add_gt t' t1 ugraph in
+ let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
+ C.Sort (C.Type t'),ugraph2
+ with
+ CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg))
+ | (C.Sort _,C.Sort (C.Type t1)) -> C.Sort (C.Type t1),ugraph
+ | (C.Sort _,C.Sort (C.CProp t1)) -> C.Sort (C.CProp t1),ugraph
| (C.Meta _, C.Sort _) -> t2',ugraph
| (C.Meta _, (C.Meta (_,_) as t))
| (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t ->
let rec higher_name arity =
function
Cic.Sort Cic.Prop
- | Cic.Sort Cic.CProp ->
+ | Cic.Sort (Cic.CProp _) ->
if arity = 0 then "A" (* propositions *)
else if arity = 1 then "P" (* predicates *)
else "R" (*relations *)
in
(match ty with
C.Sort C.Prop
- | C.Sort C.CProp -> "H"
+ | C.Sort (C.CProp _) -> "H"
| _ -> guess_a_name context typ
)
with CicTypeChecker.TypeCheckerFailure _ -> "H"
let t1'' = CicReduction.whd ~subst context t1 in
let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
match (t1'', t2'') with
- (C.Sort s1, C.Sort s2)
- when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
+ | (C.Sort s1, C.Sort s2) when (s2 = C.Prop || s2 = C.Set) ->
(* different than Coq manual!!! *)
C.Sort s2,subst,metasenv,ugraph
| (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
C.Sort (C.Type t'),subst,metasenv,ugraph2
with
CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
+ | (C.Sort (C.CProp t1), C.Sort (C.CProp t2)) ->
+ let t' = CicUniv.fresh() in
+ (try
+ let ugraph1 = CicUniv.add_ge t' t1 ugraph in
+ let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
+ C.Sort (C.CProp t'),subst,metasenv,ugraph2
+ with
+ CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
+ | (C.Sort (C.Type t1), C.Sort (C.CProp t2)) ->
+ let t' = CicUniv.fresh() in
+ (try
+ let ugraph1 = CicUniv.add_ge t' t1 ugraph in
+ let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
+ C.Sort (C.CProp t'),subst,metasenv,ugraph2
+ with
+ CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
+ | (C.Sort (C.CProp t1), C.Sort (C.Type t2)) ->
+ let t' = CicUniv.fresh() in
+ (try
+ let ugraph1 = CicUniv.add_gt t' t1 ugraph in
+ let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
+ C.Sort (C.Type t'),subst,metasenv,ugraph2
+ with
+ CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
| (C.Sort _,C.Sort (C.Type t1)) ->
C.Sort (C.Type t1),subst,metasenv,ugraph
+ | (C.Sort _,C.Sort (C.CProp t1)) ->
+ C.Sort (C.CProp t1),subst,metasenv,ugraph
| (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
| (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
(* TODO how can we force the meta to become a sort? If we don't we
[ "Prop" -> `Prop
| "Set" -> `Set
| "Type" -> `Type (CicUniv.fresh ())
- | "CProp" -> `CProp
+ | "CProp" -> `CProp (CicUniv.fresh ())
]
];
explicit_subst: [
let string_of_sort_kind = function
| `Prop -> "Prop"
| `Set -> "Set"
- | `CProp -> "CProp"
+ | `CProp _ -> "CProp"
| `Type _ -> "Type"
let pp_ast0 t k =
let debug_print s =
if debug then prerr_endline (Lazy.force s);;
+let is_propositional context sort =
+ match CicReduction.whd context sort with
+ | Cic.Sort Cic.Prop
+ | Cic.Sort (Cic.CProp _) -> true
+ | _-> false
+;;
+
+
type auto_params = Cic.term list * (string * string) list
let elems = ref [] ;;
CicTypeChecker.type_of_aux' metasenv context mt
CicUniv.oblivion_ugraph
in
- let b, _ =
- CicReduction.are_convertible ~metasenv context
- sort (Cic.Sort Cic.Prop) u
- in
- if b then Some i else None
+ if is_propositional context sort then Some i else None
| _ -> assert false)
args
in
CicTypeChecker.type_of_aux' metasenv context mt
CicUniv.oblivion_ugraph
in
- let b, _ =
- CicReduction.are_convertible ~metasenv context
- sort (Cic.Sort Cic.Prop) u
- in
- if b then Some i else None
+ if is_propositional context sort then Some i else None
| _ -> assert false)
args
in
;;
let is_in_prop context subst metasenv ty =
let sort,u = typeof ~subst metasenv context ty CicUniv.oblivion_ugraph in
- fst (CicReduction.are_convertible context sort (Cic.Sort Cic.Prop) u)
+ is_propositional context sort
;;
let assert_proof_is_valid proof metasenv context goalty =
let _,context,ty = CicUtil.lookup_meta g metasenv in
try
let sort,u = typeof ~subst metasenv context ty ugraph in
- let b,_ =
- CicReduction.are_convertible
- ~subst ~metasenv context sort (Cic.Sort Cic.Prop) u in
- b
+ is_propositional context sort
with
| CicTypeChecker.AssertFailure s
| CicTypeChecker.TypeCheckerFailure s ->
(* roba seria ------------------------------------------------------------- *)
-let decompose_tac ?(sorts=[CicPp.ppsort C.Prop; CicPp.ppsort C.CProp])
+let decompose_tac ?(sorts=[CicPp.ppsort C.Prop; CicPp.ppsort (C.CProp (CicUniv.fresh ()))])
?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) () =
let decompose_tac status =
let (proof, goal) = status in
match ty_ty with
C.Sort C.Prop -> "_ind"
| C.Sort C.Set -> "_rec"
- | C.Sort C.CProp -> "_rec"
+ | C.Sort (C.CProp _) -> "_rect"
| C.Sort (C.Type _)-> "_rect"
| C.Meta (_,_) -> raise TheTypeOfTheCurrentGoalIsAMetaICannotChooseTheRightElimiantionPrinciple
| _ -> assert false
0.5.? - ?/?/? - ?
* refinement of match fixed to prevent useless unfolding,
head_beta_reduce is used instead of whd ~delta:true
+ * CProp hierarchy, interleaved with type (used to be a single universe)
0.5.1 - 29/5/2008 - minor bug fix release
* visualization of inductive types reports the number of fixed parameters
| Cic.Meta _ -> PT.Implicit
| Cic.Sort (Cic.Type u) -> PT.Sort (`Type u)
| Cic.Sort Cic.Set -> PT.Sort `Set
- | Cic.Sort Cic.CProp -> PT.Sort `CProp
+ | Cic.Sort (Cic.CProp u) -> PT.Sort (`CProp u)
| Cic.Sort Cic.Prop -> PT.Sort `Prop
| _ as t -> PT.Ident ("ERROR: "^CicPp.ppterm t, None)
in
projects / helm.git / commitdiff