| C.Var _
| C.Meta _
| C.Sort _
- | C.Implicit
+ | C.Implicit _
| C.Cast _ -> []
| C.Prod (n,s,t) when t == term -> [Some (n,C.Decl s)]
| C.Prod _ -> []
C.Rel _ -> []
| C.Meta (n,_) -> [n]
| C.Sort _
- | C.Implicit -> []
+ | C.Implicit _ -> []
| C.Cast (te,ty) -> (aux te) @ (aux ty)
| C.Prod (_,s,t) -> (aux s) @ (aux t)
| C.Lambda (_,s,t) -> (aux s) @ (aux t)
type id = string (* the abstract type of the (annotated) node identifiers *)
type 'term explicit_named_substitution = (UriManager.uri * 'term) list
+type implicit_annotation = [ `Closed | `Type ]
+
type anntarget =
Object of annobj (* if annobj is a Constant, this is its type *)
| ConstantBody of annobj
| Meta of int * (term option) list (* numeric id, *)
(* local context *)
| Sort of sort (* sort *)
- | Implicit (* *)
+ | Implicit of implicit_annotation option (* *)
| Cast of term * term (* value, type *)
| Prod of name * term * term (* binder, source, target *)
| Lambda of name * term * term (* binder, source, target *)
| AMeta of id * int * (annterm option) list (* numeric id, *)
(* local context *)
| ASort of id * sort (* sort *)
- | AImplicit of id (* *)
+ | AImplicit of id * implicit_annotation option (* *)
| ACast of id * annterm * annterm (* value, type *)
| AProd of id * name * annterm * annterm (* binder, source, target *)
| ALambda of id * name * annterm * annterm (* binder, source, target *)
assert (exp_named_subst = []) ;
let n = self#node in
let id = string_of_xml_attr (n#attribute "id") in
- Cic.AImplicit id
+ Cic.AImplicit (id, None)
end
;;
in
C.Meta (n, l')
| C.ASort (_,s) -> C.Sort s
- | C.AImplicit _ -> C.Implicit
+ | C.AImplicit (_, annotation) -> C.Implicit annotation
| C.ACast (_,va,ty) -> C.Cast (deannotate_term va, deannotate_term ty)
| C.AProd (_,name,so,ta) ->
C.Prod (name, deannotate_term so, deannotate_term ta)
C.ARel (id,_,_,_)
| C.AMeta (id,_,_)
| C.ASort (id,_)
- | C.AImplicit id ->
+ | C.AImplicit (id, _) ->
set_target id (C.Term t)
| C.ACast (id,va,ty) ->
set_target id (C.Term t) ;
let cic_body = do_branch' (name :: context) tl in
let typ =
match typ with
- | None -> Cic.Implicit
+ | None -> Cic.Implicit (Some `Type)
| Some typ -> aux loc context typ
in
Cic.Lambda (name, typ, cic_body)
let (indtype_uri, indtype_no) =
match resolve env (Id indty_ident) () with
| Cic.MutInd (uri, tyno, _) -> uri, tyno
- | Cic.Implicit -> raise Try_again
+ | Cic.Implicit _ -> raise Try_again
| _ -> raise DisambiguateChoices.Invalid_choice
in
Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
"Explicit substitutions not allowed here";
Cic.Rel index
with Not_found -> resolve env (Id name) ())
- | CicAst.Implicit -> Cic.Implicit
+ | CicAst.Implicit -> Cic.Implicit None
| CicAst.Num (num, i) -> resolve env (Num i) ~num ()
| CicAst.Meta (index, subst) ->
let cic_subst =
| CicAst.Symbol (symbol, instance) ->
resolve env (Symbol (symbol, instance)) ()
and aux_option loc context = function
- | None -> Cic.Implicit
+ | None -> Cic.Implicit (Some `Type)
| Some term -> aux loc context term
in
match ast with
let filled_env =
List.fold_left
(fun env item ->
- Environment.add item ("Implicit", fun _ _ _ -> Cic.Implicit) env)
+ Environment.add item
+ ("Implicit",
+ (match item with
+ | Id _ | Num _ -> (fun _ _ _ -> Cic.Implicit (Some `Closed))
+ | Symbol _ -> (fun _ _ _ -> Cic.Implicit None))) env)
current_env todo_dom
in
try
in
Cic.Appl [
Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []);
- Cic.Implicit; t1; t2
+ Cic.Implicit (Some `Type); t1; t2
]))
| Some _, None -> assert false (* due to typing rules *))
canonical_context l))
| C.Sort s -> C.ASort (fresh_id'', s)
- | C.Implicit -> C.AImplicit (fresh_id'')
+ | C.Implicit annotation -> C.AImplicit (fresh_id'', annotation)
| C.Cast (v,t) ->
xxx_add ids_to_inner_sorts fresh_id'' innersort ;
if innersort = "Prop" then
| C.Var _ -> false
| C.Meta _ -> false
| C.Sort _ -> false
- | C.Implicit -> raise NotImplemented
+ | C.Implicit _ -> assert false
| C.Prod (_,s,t) -> (occur uri s) or (occur uri t)
| C.Cast (te,ty) -> (occur uri te)
| C.Lambda (_,s,t) -> (occur uri s) or (occur uri t) (* or false ?? *)
| C.Rel _
| C.Meta _
| C.Sort _
- | C.Implicit -> true
+ | C.Implicit _ -> true
| C.Cast (te,ty) ->
does_not_occur n te && does_not_occur n ty
| C.Prod (name,so,dest) ->
(function None -> None | Some t -> Some (head_beta_reduce t)) l
)
| C.Sort _ as t -> t
- | C.Implicit -> assert false
+ | C.Implicit _ -> assert false
| C.Cast (te,ty) ->
C.Cast (head_beta_reduce te, head_beta_reduce ty)
| C.Prod (n,s,t) ->
(* Checks suppressed *)
CicSubstitution.lift_meta l ty
| C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
- | C.Implicit -> raise (Impossible 21)
+ | C.Implicit _ -> raise (Impossible 21)
| C.Cast (te,ty) ->
(* Let's visit all the subterms that will not be visited later *)
let _ = type_of_aux context te (Some (head_beta_reduce ty)) in
if does_not_occur 1 t_typ then
(* since [Rel 1] does not occur in typ, substituting any term *)
(* in place of [Rel 1] is equivalent to delifting once *)
- CicSubstitution.subst C.Implicit t_typ
+ CicSubstitution.subst (C.Implicit None) t_typ
else
C.LetIn (n,s,t_typ)
| C.Appl (he::tl) when List.length tl > 0 ->
in
C.Meta (n,l')
| C.Sort s -> C.Sort s
- | C.Implicit -> C.Implicit
+ | C.Implicit _ as t -> t
| C.Cast (v,t) -> C.Cast (eta_fix' context v, eta_fix' context t)
| C.Prod (n,s,t) ->
C.Prod
in
C.Meta(i,l')
| C.Sort _ as t -> t
- | C.Implicit as t -> t
+ | C.Implicit _ as t -> t
| C.Cast (te,ty) -> C.Cast (restore_in_term te, restore_in_term ty)
| C.Prod (n,s,t) -> C.Prod (n, restore_in_term s, restore_in_term t)
| C.Lambda (n,s,t) -> C.Lambda (n, restore_in_term s, restore_in_term t)
C.Var (uri,exp_named_subst')
| C.Meta _ as t -> t
| C.Sort _ as t -> t
- | C.Implicit as t -> t
+ | C.Implicit _ as t -> t
| C.Cast (te,ty) -> C.Cast (letin_nf te, letin_nf ty)
| C.Prod (n,s,t) -> C.Prod (n, letin_nf s, letin_nf t)
| C.Lambda (n,s,t) -> C.Lambda (n, letin_nf s, letin_nf t)
| C.Type -> "Type"
| C.CProp -> "CProp"
)
- | C.Implicit -> "?"
+ | C.Implicit _ -> "?"
| C.Prod (b,s,t) ->
(match b with
C.Name n -> "(" ^ n ^ ":" ^ pp s l ^ ")" ^ pp t ((Some b)::l)
in
C.Meta (i, l')
| C.Sort _ as t -> t
- | C.Implicit as t -> t
+ | C.Implicit _ as t -> t
| C.Cast (te,ty) -> C.Cast (unwind_aux m te, unwind_aux m ty) (*CSC ???*)
| C.Prod (n,s,t) -> C.Prod (n, unwind_aux m s, unwind_aux (m + 1) t)
| C.Lambda (n,s,t) -> C.Lambda (n, unwind_aux m s, unwind_aux (m + 1) t)
let t' = unwind k e ens t in
if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
| (k, e, _, (C.Sort _ as t), s) -> t (* s should be empty *)
- | (k, e, _, (C.Implicit as t), s) -> t (* s should be empty *)
+ | (k, e, _, (C.Implicit _ as t), s) -> t (* s should be empty *)
| (k, e, ens, (C.Cast (te,ty) as t), s) ->
reduce (k, e, ens, te, s) (* s should be empty *)
| (k, e, ens, (C.Prod _ as t), s) ->
in
(* ts are already unwinded because they are a sublist of tl *)
reduce (k, e, ens, (List.nth pl (j-1)), (RS.to_stack_list ts)@s)
- | C.Cast _ | C.Implicit ->
+ | C.Cast _ | C.Implicit _ ->
raise (Impossible 2) (* we don't trust our whd ;-) *)
| _ ->
let t' = unwind k e ens t in
b && aux context ty1 ty2 && aux (tys@context) bo1 bo2)
fl1 fl2 true
| (C.Cast _, _) | (_, C.Cast _)
- | (C.Implicit, _) | (_, C.Implicit) ->
+ | (C.Implicit _, _) | (_, C.Implicit _) ->
assert false
| (_,_) -> false
end
)
| C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
| C.Sort _ as t -> t (* l should be empty *)
- | C.Implicit as t -> t
+ | C.Implicit _ as t -> t
| C.Cast (te,ty) -> whdaux l te (*CSC E' GIUSTO BUTTARE IL CAST? *)
| C.Prod _ as t -> t (* l should be empty *)
| C.Lambda (name,s,t) as t' ->
eat_first (r,tl)
in
whdaux (ts@l) (List.nth pl (j-1))
- | C.Cast _ | C.Implicit ->
+ | C.Cast _ | C.Implicit _ ->
raise (Impossible 2) (* we don't trust our whd ;-) *)
| _ -> if l = [] then t else C.Appl (t::l)
)
b && aux context ty1 ty2 && aux (tys@context) bo1 bo2)
fl1 fl2 true
| (C.Cast _, _) | (_, C.Cast _)
- | (C.Implicit, _) | (_, C.Implicit) ->
+ | (C.Implicit _, _) | (_, C.Implicit _) ->
raise (Impossible 3) (* we don't trust our whd ;-) *)
| (_,_) -> false
end
in
C.Meta(i,l')
| C.Sort _ as t -> t
- | C.Implicit as t -> t
+ | C.Implicit _ as t -> t
| C.Cast (te,ty) -> C.Cast (liftaux k te, liftaux k ty)
| C.Prod (n,s,t) -> C.Prod (n, liftaux k s, liftaux (k+1) t)
| C.Lambda (n,s,t) -> C.Lambda (n, liftaux k s, liftaux (k+1) t)
in
C.Meta(i,l')
| C.Sort _ as t -> t
- | C.Implicit as t -> t
+ | C.Implicit _ as t -> t
| C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
| C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t)
| C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t)
in
C.Meta(i,l')
| C.Sort _ as t -> t
- | C.Implicit as t -> t
+ | C.Implicit _ as t -> t
| C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
| C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t)
| C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t)
in
C.Meta(i,l')
| C.Sort _ as t -> t
- | C.Implicit as t -> t
+ | C.Implicit _ as t -> t
| C.Cast (te,ty) -> C.Cast (aux k te, aux k ty) (*CSC ??? *)
| C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k + 1) t)
| C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k + 1) t)
C.Var (uri,exp_named_subst')
| C.Meta _ -> assert false
| C.Sort _
- | C.Implicit as t -> t
+ | C.Implicit _ as t -> t
| C.Cast (te,ty) -> C.Cast (aux k te, aux k ty)
| C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k+1) t)
| C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k+1) t)
| C.Rel _
| C.Meta _
| C.Sort _
- | C.Implicit -> true
+ | C.Implicit _ -> true
| C.Cast (te,ty) ->
does_not_occur context n nn te && does_not_occur context n nn ty
| C.Prod (name,so,dest) ->
| C.Var _
| C.Meta _
| C.Sort _
- | C.Implicit
+ | C.Implicit _
| C.Cast _ (*CSC ??? *) ->
raise (AssertFailure "3") (* due to type-checking *)
| C.Prod (name,so,de) ->
| C.Var _
| C.Meta _
| C.Sort _
- | C.Implicit
+ | C.Implicit _
| C.Cast _
(* | C.Cast (te,ty) ->
check_is_really_smaller_arg n nn kl x safes te &&
)
| C.Meta _
| C.Sort _
- | C.Implicit -> true
+ | C.Implicit _ -> true
| C.Cast (te,ty) ->
guarded_by_destructors context n nn kl x safes te &&
guarded_by_destructors context n nn kl x safes ty
| C.Rel _ -> true
| C.Meta _
| C.Sort _
- | C.Implicit
+ | C.Implicit _
| C.Cast _
| C.Prod _
| C.LetIn _ ->
| C.Var _
| C.Sort _ ->
does_not_occur context n nn te
- | C.Implicit
+ | C.Implicit _
| C.Cast _ ->
raise (AssertFailure "24")(* due to type-checking *)
| C.Prod (name,so,de) ->
| C.Var _
| C.Meta _
| C.Sort _
- | C.Implicit
+ | C.Implicit _
| C.Cast _ -> raise (AssertFailure "29")(* due to type-checking *)
| C.Prod (name,so,de) ->
begin
check_metasenv_consistency metasenv context canonical_context l;
CicSubstitution.lift_meta l ty
| C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
- | C.Implicit -> raise (AssertFailure "21")
+ | C.Implicit _ -> raise (AssertFailure "21")
| C.Cast (te,ty) as t ->
let _ = type_of_aux context ty in
if R.are_convertible context (type_of_aux context te) ty then
in
C.Meta (i,l'))
| C.Sort _ as t -> t
- | C.Implicit -> assert false
+ | C.Implicit _ -> assert false
| C.Cast (te,ty) -> C.Cast (um_aux te, um_aux ty)
| C.Prod (n,s,t) -> C.Prod (n, um_aux s, um_aux t)
| C.Lambda (n,s,t) -> C.Lambda (n, um_aux s, um_aux t)
C.Rel r when List.mem (r - k) to_be_restricted -> raise Occur
| C.Rel _
| C.Sort _ as t -> t
- | C.Implicit -> assert false
+ | C.Implicit _ -> assert false
| C.Meta (n, l) ->
(* we do not retrieve the term associated to ?n in subst since *)
(* in this way we can restrict if something goes wrong *)
let l' = deliftl 1 l1 in
C.Meta(i,l')
| C.Sort _ as t -> t
- | C.Implicit as t -> t
+ | C.Implicit _ as t -> t
| C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty)
| C.Prod (n,s,t) -> C.Prod (n, deliftaux k s, deliftaux (k+1) t)
| C.Lambda (n,s,t) -> C.Lambda (n, deliftaux k s, deliftaux (k+1) t)
| Cic.Meta (n,l) ->
let metasenv', l' = do_local_context metasenv context l in
metasenv', Cic.Meta (n, l')
- | Cic.Implicit ->
+ | Cic.Implicit (Some `Type) ->
+ let (metasenv', idx) = mk_implicit_type metasenv context in
+ let irl = identity_relocation_list_for_metavariable context in
+ metasenv', Cic.Meta (idx, irl)
+ | Cic.Implicit (Some `Closed) ->
+ let (metasenv', idx) = mk_implicit metasenv [] in
+ metasenv', Cic.Meta (idx, [])
+ | Cic.Implicit None ->
let (metasenv', idx) = mk_implicit metasenv context in
let irl = identity_relocation_list_for_metavariable context in
metasenv', Cic.Meta (idx, irl)
| C.Sort s ->
C.Sort C.Type, (*CSC manca la gestione degli universi!!! *)
subst,metasenv
- | C.Implicit -> raise (Impossible 21)
+ | C.Implicit _ -> raise (Impossible 21)
| C.Cast (te,ty) ->
let _,subst',metasenv' =
type_of_aux subst metasenv context ty in
raise (UnificationFailure (sprintf
"Can't unify %s with %s due to different inductive constructors"
(CicPp.ppterm t1) (CicPp.ppterm t1)))
- | (C.Implicit, _) | (_, C.Implicit) -> assert false
+ | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
| (C.Cast (te,ty), t2) -> fo_unif_subst subst context metasenv te t2
| (t1, C.Cast (te,ty)) -> fo_unif_subst subst context metasenv t1 te
| (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
in
C.Meta(i,l'),rels
| C.Sort _ as t -> t,[]
- | C.Implicit as t -> t,[]
+ | C.Implicit _ as t -> t,[]
| C.Cast (te,ty) ->
let te',rels1 = aux k te in
let ty',rels2 = aux k ty in
Cic.Rel _ -> l
| Cic.Meta _ -> l
| Cic.Sort _ -> l
- | Cic.Implicit -> l
+ | Cic.Implicit _ -> l
| Cic.Var (u,exp_named_subst) ->
let l' = inspect_uri main l u [] v term in
inspect_exp_named_subst l' (succ v) exp_named_subst
[],[],[!!kind,s']
| _ -> [],[],[])
| C.Meta _
- | C.Implicit -> assert false
+ | C.Implicit _ -> assert false
| C.Cast (te,_) ->
(* type ignored *)
process_type_aux kind te
C.Var (uri,exp_named_subst')
| C.Meta _
| C.Sort _
- | C.Implicit as t -> t
+ | C.Implicit _ as t -> t
| C.Cast (te,ty) -> C.Cast (aux n te, aux n ty)
| C.Prod (nn,s,t) -> C.Prod (nn, aux n s, aux (n+1) t)
| C.Lambda (nn,s,t) -> C.Lambda (nn, aux n s, aux (n+1) t)
C.Var (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
| C.Meta _ -> t
| C.Sort _ -> t
- | C.Implicit as t -> t
+ | C.Implicit _ as t -> t
| C.Cast (te,ty) -> C.Cast (aux te, aux ty)
| C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
| C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
in
C.Meta(i,l')
| C.Sort _ as t -> t
- | C.Implicit as t -> t
+ | C.Implicit _ as t -> t
| C.Cast (te,ty) -> C.Cast (substaux k what te, substaux k what ty)
| C.Prod (n,s,t) ->
C.Prod
in
C.Meta(i,l')
| C.Sort _ as t -> t
- | C.Implicit as t -> t
+ | C.Implicit _ as t -> t
| C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
| C.Prod (n,s,t) ->
C.Prod (n, substaux k s, substaux (k + 1) t)
)
| C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
| C.Sort _ as t -> t (* l should be empty *)
- | C.Implicit as t -> t
+ | C.Implicit _ as t -> t
| C.Cast (te,ty) ->
C.Cast (reduceaux context l te, reduceaux context l ty)
| C.Prod (name,s,t) ->
eat_first (r,tl)
in
reduceaux context (ts@l) (List.nth pl (j-1))
- | C.Cast _ | C.Implicit ->
+ | C.Cast _ | C.Implicit _ ->
raise (Impossible 2) (* we don't trust our whd ;-) *)
| _ ->
let outtype' = reduceaux context [] outtype in
)
| C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
| C.Sort _ as t -> t (* l should be empty *)
- | C.Implicit as t -> t
+ | C.Implicit _ as t -> t
| C.Cast (te,ty) ->
C.Cast (reduceaux context l te, reduceaux context l ty)
| C.Prod (name,s,t) ->
eat_first (r,tl)
in
reduceaux context (ts@l) (List.nth pl (j-1))
- | C.Cast _ | C.Implicit ->
+ | C.Cast _ | C.Implicit _ ->
raise (Impossible 2) (* we don't trust our whd ;-) *)
| _ ->
let outtype' = reduceaux context [] outtype in
projects / helm.git / commitdiff