let add_level_info prec t = Ast.AttributedTerm (`Level prec, t)
-let rec top_pos t = add_level_info ~-1 t
+let top_pos t = add_level_info ~-1 t
let rec remove_level_info =
function
in
let match_box =
hvbox false false [
- hvbox false true [
+ hvbox false false [
hvbox false true [keyword "match"; space; break; top_pos (k what)];
break;
hvbox false true indty_box;
keyword "let"; space;
hvbox false true [
aux_var var; space;
- builtin_symbol "\\def"; break; top_pos (k s) ];
- break; space; keyword "in"; space ];
+ builtin_symbol "\\def"; break; top_pos (k s); space; keyword "in"; space ];
+ ];
break;
k t ])
+(*
| Ast.LetRec (rec_kind, funs, where) ->
let rec_op =
match rec_kind with `Inductive -> "rec" | `CoInductive -> "corec"
((hvbox false false
(fst_row :: List.flatten tl_rows
@ [ break; keyword "in"; break; k where ])))
+*)
| Ast.Implicit `JustOne -> builtin_symbol "?"
| Ast.Implicit `Vector -> builtin_symbol "…"
| Ast.Meta (n, l) ->
type db = {
level1_patterns21: NotationPt.term IntMap.t;
- compiled21: ((NotationPt.term -> (NotationEnv.t * NotationPt.term list * int) option)) Lazy.t option;
+ compiled21: ((NotationPt.term -> (NotationEnv.t * NotationPt.term list * int) option)) Lazy.t;
pattern21_matrix: (NotationPt.term * pattern_id) list;
counter: pattern_id
}
let initial_db = {
level1_patterns21 = IntMap.empty;
- compiled21 = None;
+ compiled21 = lazy (Content2presMatcher.Matcher21.compiler []);
pattern21_matrix = [];
counter = ~-1
}
end
let get_compiled21 status =
- match status#content_pres_db.compiled21 with
- | None -> assert false
- | Some f -> Lazy.force f
+ Lazy.force status#content_pres_db.compiled21
let set_compiled21 status f =
status#set_content_pres_db
- { status#content_pres_db with compiled21 = Some f }
+ { status#content_pres_db with compiled21 = f }
let add_idrefs =
List.fold_right (fun idref t -> Ast.AttributedTerm (`IdRef idref, t))
Ast.AttributedTerm (attr, subst_singleton pos env t)
| t -> NotationUtil.group (subst pos env t)
and subst pos env = function
- | Ast.AttributedTerm (attr, t) ->
+ | Ast.AttributedTerm (_attr, t) ->
(* prerr_endline ("loosing attribute " ^ NotationPp.pp_attribute attr); *)
subst pos env t
| Ast.Variable var ->
| Ast.Literal l as t ->
let t = add_idrefs idrefs t in
(match l with
- | `Keyword k -> [ add_keyword_attrs t ]
+ | `Keyword _k -> [ add_keyword_attrs t ]
| _ -> [ t ])
| Ast.Layout l -> [ Ast.Layout (subst_layout pos env l) ]
| t -> [ NotationUtil.visit_ast (subst_singleton pos env) t ]
in
let rec aux env term =
match term with
- | Ast.AttributedTerm (a, term) -> (*Ast.AttributedTerm (a, *)aux env term
+ | Ast.AttributedTerm (_a, term) -> (*Ast.AttributedTerm (a, *)aux env term
| Ast.Appl terms -> Ast.Appl (List.map (aux env) terms)
| Ast.Binder (binder, var, body) ->
Ast.Binder (binder, aux_capture_var env var, aux env body)
List.map (aux_branch env) patterns)
| Ast.LetIn (var, t1, t3) ->
Ast.LetIn (aux_capture_var env var, aux env t1, aux env t3)
+(*
| Ast.LetRec (kind, definitions, body) ->
Ast.LetRec (kind, List.map (aux_definition env) definitions,
aux env body)
+*)
| Ast.Uri (name, None) -> Ast.Uri (name, None)
| Ast.Uri (name, Some substs) ->
Ast.Uri (name, Some (aux_substs env substs))
Ast.Pattern (head, hrefs, vars) ->
Ast.Pattern (head, hrefs, List.map (aux_capture_var env) vars)
| Ast.Wildcard -> Ast.Wildcard
- and aux_definition env (params, var, term, i) =
- (List.map (aux_capture_var env) params, aux_capture_var env var, aux env term, i)
+ (*and aux_definition env (params, var, term, i) =
+ (List.map (aux_capture_var env) params, aux_capture_var env var, aux env term, i)*)
and aux_substs env substs =
List.map (fun (name, term) -> (name, aux env term)) substs
and aux_meta_substs env meta_substs = List.map (aux_opt env) meta_substs
| Ast.TermVar (name,(Ast.Level l|Ast.Self l)) ->
Ast.AttributedTerm (`Level l,Env.lookup_term env name)
| Ast.FreshVar name -> Ast.Ident (lookup_fresh_name name, None)
- | Ast.Ascription (term, name) -> assert false
+ | Ast.Ascription (_term, _name) -> assert false
and aux_magic env = function
| Ast.Default (some_pattern, none_pattern) ->
let some_pattern_names = NotationUtil.names_of_term some_pattern in
| _ -> assert false
in
instantiate_fold_right env)
- | Ast.If (_, p_true, p_false) as t ->
+ | Ast.If (_, _p_true, _p_false) as t ->
aux env (NotationUtil.find_branch (Ast.Magic t))
| Ast.Fail -> assert false
| _ -> assert false