diff options
Diffstat (limited to 'kernel/sign.ml')
| -rw-r--r-- | kernel/sign.ml | 82 |
1 files changed, 32 insertions, 50 deletions
diff --git a/kernel/sign.ml b/kernel/sign.ml index 0899cf5e6..c9da4ab65 100644 --- a/kernel/sign.ml +++ b/kernel/sign.ml @@ -26,17 +26,9 @@ type named_context = named_declaration list let add_named_decl = add let add_named_assum = add_decl let add_named_def = add_def -let rec lookup_id_type id = function - | (id',c,t) :: _ when id=id' -> t - | _ :: sign -> lookup_id_type id sign - | [] -> raise Not_found -let rec lookup_id_value id = function - | (id',c,t) :: _ when id=id' -> c - | _ :: sign -> lookup_id_value id sign - | [] -> raise Not_found -let rec lookup_id id = function - | (id',c,t) :: _ when id=id' -> (c,t) - | _ :: sign -> lookup_id id sign +let rec lookup_named id = function + | (id',_,_ as decl) :: _ when id=id' -> decl + | _ :: sign -> lookup_named id sign | [] -> raise Not_found let empty_named_context = [] let pop_named_decl id = function @@ -59,18 +51,13 @@ let fold_named_context_reverse = List.fold_left let fold_named_context_both_sides = list_fold_right_and_left let it_named_context_quantifier f = List.fold_left (fun c d -> f d c) -(*s Signatures of ordered section variables *) +let it_mkNamedProd_or_LetIn = + List.fold_left (fun c d -> mkNamedProd_or_LetIn d c) +let it_mkNamedLambda_or_LetIn = + List.fold_left (fun c d -> mkNamedLambda_or_LetIn d c) -type section_declaration = variable * constr option * constr -type section_context = section_declaration list -let instance_from_section_context sign = - let rec inst_rec = function - | (sp,None,_) :: sign -> mkVar (basename sp) :: inst_rec sign - | _ :: sign -> inst_rec sign - | [] -> [] in - Array.of_list (inst_rec sign) -let instance_from_section_context x = - instance_from_section_context x +(*s Signatures of ordered section variables *) +type section_context = named_context (*s Signatures of ordered optionally named variables, intended to be accessed by de Bruijn indices *) @@ -79,21 +66,20 @@ type rel_declaration = name * constr option * types type rel_context = rel_declaration list type rev_rel_context = rel_declaration list +let fold_rel_context = List.fold_right +let fold_rel_context_reverse = List.fold_left + +let it_mkProd_or_LetIn = List.fold_left (fun c d -> mkProd_or_LetIn d c) +let it_mkLambda_or_LetIn = List.fold_left (fun c d -> mkLambda_or_LetIn d c) + let add_rel_decl = add let add_rel_assum = add_decl let add_rel_def = add_def -let lookup_rel_type n sign = +let lookup_rel n sign = let rec lookrec = function - | (1, (na,_,t) :: _) -> (na,t) - | (n, _ :: sign) -> lookrec (n-1,sign) - | (_, []) -> raise Not_found - in - lookrec (n,sign) -let lookup_rel_value n sign = - let rec lookrec = function - | (1, (_,c,_) :: _) -> c - | (n, _ :: sign ) -> lookrec (n-1,sign) - | (_, []) -> raise Not_found + | (1, decl :: _) -> decl + | (n, _ :: sign) -> lookrec (n-1,sign) + | (_, []) -> raise Not_found in lookrec (n,sign) let rec lookup_rel_id id sign = @@ -127,10 +113,6 @@ let ids_of_rel_context sign = (fun (na,_,_) l -> match na with Name id -> id::l | Anonymous -> l) sign [] let names_of_rel_context = List.map (fun (na,_,_) -> na) -let assums_of_rel_context sign = - List.fold_right - (fun (na,c,t) l -> match c with Some _ -> l | None -> (na,body_of_type t)::l) - sign [] let map_rel_context = map let push_named_to_rel_context hyps ctxt = let rec push = function @@ -157,7 +139,7 @@ let instantiate_sign sign args = | ([],_) | (_,[]) -> anomaly "Signature and its instance do not match" in - instrec (sign,args) + instrec (sign,Array.to_list args) (*************************) (* Names environments *) @@ -185,9 +167,9 @@ let empty_names_context = [] let decompose_prod_assum = let rec prodec_rec l c = match kind_of_term c with - | IsProd (x,t,c) -> prodec_rec (add_rel_assum (x,t) l) c - | IsLetIn (x,b,t,c) -> prodec_rec (add_rel_def (x,b,t) l) c - | IsCast (c,_) -> prodec_rec l c + | Prod (x,t,c) -> prodec_rec (add_rel_assum (x,t) l) c + | LetIn (x,b,t,c) -> prodec_rec (add_rel_def (x,b,t) l) c + | Cast (c,_) -> prodec_rec l c | _ -> l,c in prodec_rec empty_rel_context @@ -197,9 +179,9 @@ let decompose_prod_assum = let decompose_lam_assum = let rec lamdec_rec l c = match kind_of_term c with - | IsLambda (x,t,c) -> lamdec_rec (add_rel_assum (x,t) l) c - | IsLetIn (x,b,t,c) -> lamdec_rec (add_rel_def (x,b,t) l) c - | IsCast (c,_) -> lamdec_rec l c + | Lambda (x,t,c) -> lamdec_rec (add_rel_assum (x,t) l) c + | LetIn (x,b,t,c) -> lamdec_rec (add_rel_def (x,b,t) l) c + | Cast (c,_) -> lamdec_rec l c | _ -> l,c in lamdec_rec empty_rel_context @@ -212,10 +194,10 @@ let decompose_prod_n_assum n = let rec prodec_rec l n c = if n=0 then l,c else match kind_of_term c with - | IsProd (x,t,c) -> prodec_rec (add_rel_assum(x,t) l) (n-1) c - | IsLetIn (x,b,t,c) -> + | Prod (x,t,c) -> prodec_rec (add_rel_assum(x,t) l) (n-1) c + | LetIn (x,b,t,c) -> prodec_rec (add_rel_def (x,b,t) l) (n-1) c - | IsCast (c,_) -> prodec_rec l n c + | Cast (c,_) -> prodec_rec l n c | c -> error "decompose_prod_n_assum: not enough assumptions" in prodec_rec empty_rel_context n @@ -228,10 +210,10 @@ let decompose_lam_n_assum n = let rec lamdec_rec l n c = if n=0 then l,c else match kind_of_term c with - | IsLambda (x,t,c) -> lamdec_rec (add_rel_assum (x,t) l) (n-1) c - | IsLetIn (x,b,t,c) -> + | Lambda (x,t,c) -> lamdec_rec (add_rel_assum (x,t) l) (n-1) c + | LetIn (x,b,t,c) -> lamdec_rec (add_rel_def (x,b,t) l) (n-1) c - | IsCast (c,_) -> lamdec_rec l n c + | Cast (c,_) -> lamdec_rec l n c | c -> error "decompose_lam_n_assum: not enough abstractions" in lamdec_rec empty_rel_context n |