let string_of_sort_kind = function
| `Prop -> "Prop"
| `Set -> "Set"
- | `CProp -> "CProp"
+ | `CProp _ -> "CProp"
| `Type _ -> "Type"
let pp_ast0 t k =
space
]
in
- let mk_case_pattern (head, href, vars) =
- hbox true false (ident_w_href href head :: List.map aux_var vars)
+ let mk_case_pattern =
+ function
+ Ast.Pattern (head, href, vars) ->
+ hbox true false (ident_w_href href head :: List.map aux_var vars)
+ | Ast.Wildcard -> builtin_symbol "_"
in
let patterns' =
List.map
hvbox false true [
keyword "let"; space;
hvbox false true [
- aux_var var; space; builtin_symbol "\\def"; break; top_pos (k s) ];
+ aux_var var; space;
+ builtin_symbol "\\def"; break; top_pos (k s) ];
break; space; keyword "in" ];
break;
k t ])
in
aux true l1_pattern *)
+let counter = ref ~-1
+let reset () = counter := ~-1;;
let fresh_id =
- let counter = ref ~-1 in
fun () ->
incr counter;
!counter
| Ast.Case (term, indty, outty_opt, patterns) ->
Ast.Case (aux env term, indty, aux_opt env outty_opt,
List.map (aux_branch env) patterns)
- | Ast.LetIn (var, t1, t2) ->
- Ast.LetIn (aux_capture_var env var, aux env t1, aux env t2)
+ | 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)
and aux_capture_var env (name, ty_opt) = (aux env name, aux_opt env ty_opt)
and aux_branch env (pattern, term) =
(aux_pattern env pattern, aux env term)
- and aux_pattern env (head, hrefs, vars) =
- (head, hrefs, List.map (aux_capture_var env) vars)
+ and aux_pattern env =
+ function
+ 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_substs env substs =
let _ = load_patterns21 []
+
+