| `Prop -> "Prop"
| `Set -> "Set"
| `CProp -> "CProp"
- | `Type -> "Type"
+ | `Type _ -> "Type"
let pp_ast0 t k =
let rec aux =
Hashtbl.find term_info.sort id
with Not_found ->
prerr_endline (sprintf "warning: sort of id %s not found, using Type" id);
- `Type
+ `Type (CicUniv.fresh ())
in
let aux_substs substs =
Some
| Cic.AMeta (id,n,l) -> idref id (Ast.Meta (n, aux_context l))
| 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 _) -> idref id (Ast.Sort `Type)
+ | Cic.ASort (id,Cic.Type u) -> idref id (Ast.Sort (`Type u))
| Cic.ASort (id,Cic.CProp) -> idref id (Ast.Sort `CProp)
| Cic.AImplicit _ -> assert false
| Cic.AProd (id,n,s,t) ->
let binder_kind =
match sort_of_id id with
- | `Set | `Type -> `Pi
+ | `Set | `Type _ -> `Pi
| `Prop | `CProp -> `Forall
in
idref id (Ast.Binder (binder_kind,
let set_compiled21 f = compiled21 := Some f
let set_compiled32 f = compiled32 := Some f
-let instantiate21 env (* precedence associativity *) l1 =
+let instantiate21 env l1 =
let rec subst_singleton env t =
CicNotationUtil.group (subst env t)
and subst env = function
- | Ast.AttributedTerm (_, t) -> subst env t
+ | Ast.AttributedTerm (attr, t) -> subst env t
| Ast.Variable var ->
let name, expected_ty = CicNotationEnv.declaration_of_var var in
let ty, value =
List.map (fun (var, (ty, value)) -> (var, (ty, pp_value value))) env
in
(* prerr_endline ("pattern matching from 2 to 1 on term " ^ CicNotationPp.pp_term term); *)
- (match (get_compiled21 ()) term with
- | None -> pp_ast0 term pp_ast1
- | Some (env, pid) ->
- let prec, assoc, l1 =
- try
- Hashtbl.find level1_patterns21 pid
- with Not_found -> assert false
- in
- add_level_info prec assoc (instantiate21 (ast_env_of_env env) l1))
+ match term with
+ | Ast.AttributedTerm (attrs, term) -> Ast.AttributedTerm (attrs, pp_ast1 term)
+ | _ ->
+ (match (get_compiled21 ()) term with
+ | None -> pp_ast0 term pp_ast1
+ | Some (env, pid) ->
+ let prec, assoc, l1 =
+ try
+ Hashtbl.find level1_patterns21 pid
+ with Not_found -> assert false
+ in
+ add_level_info prec assoc (instantiate21 (ast_env_of_env env) l1))
let instantiate32 term_info env symbol args =
let rec instantiate_arg = function