| Cic.ASort (id,Cic.Type u) -> idref id (Ast.Sort (`Type u))
| Cic.ASort (id,Cic.CProp u) -> idref id (Ast.Sort (`CProp u))
| Cic.AImplicit (id, Some `Hole) -> idref id Ast.UserInput
| Cic.ASort (id,Cic.Type u) -> idref id (Ast.Sort (`Type u))
| Cic.ASort (id,Cic.CProp u) -> idref id (Ast.Sort (`CProp u))
| Cic.AImplicit (id, Some `Hole) -> idref id Ast.UserInput
| Cic.AProd (id,n,s,t) ->
let binder_kind =
match sort_of_id id with
| `Set | `Type _ | `NType _ -> `Pi
| Cic.AProd (id,n,s,t) ->
let binder_kind =
match sort_of_id id with
| `Set | `Type _ | `NType _ -> `Pi
in
idref id (Ast.Binder (binder_kind,
(CicNotationUtil.name_of_cic_name n, Some (k s)), k t))
in
idref id (Ast.Binder (binder_kind,
(CicNotationUtil.name_of_cic_name n, Some (k s)), k t))
else
idref aid (Ast.Appl (List.map k args)))
| Cic.AAppl (aid,args) ->
else
idref aid (Ast.Appl (List.map k args)))
| Cic.AAppl (aid,args) ->
with Not_found -> assert false
in
let ast = instantiate32 term_info idrefs env' symbol args in
Ast.AttributedTerm (`IdRef (CicUtil.id_of_annterm annterm), ast)
with Not_found -> assert false
in
let ast = instantiate32 term_info idrefs env' symbol args in
Ast.AttributedTerm (`IdRef (CicUtil.id_of_annterm annterm), ast)
let t =
HExtlib.filter_map (function (true, ap, id) -> Some (ap, id) | _ -> None) t
in
let t =
HExtlib.filter_map (function (true, ap, id) -> Some (ap, id) | _ -> None) t
in
let id = fresh_id () in
Hashtbl.add !level2_patterns32 id (dsc, symbol, args, appl_pattern);
pattern32_matrix := (true, appl_pattern, id) :: !pattern32_matrix;
let id = fresh_id () in
Hashtbl.add !level2_patterns32 id (dsc, symbol, args, appl_pattern);
pattern32_matrix := (true, appl_pattern, id) :: !pattern32_matrix;
with Not_found -> raise Interpretation_not_found);
pattern32_matrix :=
List.filter (fun (_, _, id') -> id <> id') !pattern32_matrix;
with Not_found -> raise Interpretation_not_found);
pattern32_matrix :=
List.filter (fun (_, _, id') -> id <> id') !pattern32_matrix;
| Ast.ImplicitPattern -> mk_implicit false
| Ast.VarPattern name -> lookup name
| Ast.ApplPattern terms -> mk_appl (List.map aux terms)
| Ast.ImplicitPattern -> mk_implicit false
| Ast.VarPattern name -> lookup name
| Ast.ApplPattern terms -> mk_appl (List.map aux terms)