... in the eye of the meta-vortex ...
... from Ravenna city
let opt_declaration (n, ty) = (n, OptType ty)
let list_declaration (n, ty) = (n, ListType ty)
+let declaration_of_var = function
+ | NumVar s -> s, NumType
+ | IdentVar s -> s, StringType
+ | TermVar s -> s, TermType
+ | _ -> assert false
+
+let value_of_term = function
+ | Num (s, _) -> NumValue s
+ | Ident (s, None) -> StringValue s
+ | t -> TermValue t
+
+let term_of_value = function
+ | NumValue s -> Num (s, 0)
+ | StringValue s -> Ident (s, None)
+ | TermValue t -> t
+ | _ -> assert false (* TO BE UNDERSTOOD *)
+
+let rec well_typed ty value =
+ match ty, value with
+ | TermType, TermValue _
+ | StringType, StringValue _
+ | OptType _, OptValue None
+ | NumType, NumValue _ -> true
+ | OptType ty', OptValue (Some value') -> well_typed ty' value'
+ | ListType ty', ListValue vl ->
+ List.for_all (fun value' -> well_typed ty' value') vl
+ | _ -> false
+
type binding = string * (value_type * value)
type t = binding list
+val declaration_of_var: CicNotationPt.pattern_variable -> declaration
+val value_of_term: CicNotationPt.term -> value
+val term_of_value: value -> CicNotationPt.term
+val well_typed: value_type -> value -> bool
+
(** {2 Environment lookup} *)
val lookup_value: t -> string -> value
| NoBinding :: tl ->
prerr_endline "aux: none";
Gramext.action (fun _ -> aux vl tl)
- (* LUCA: DEFCON 2 BEGIN *)
+ (* LUCA: DEFCON 5 BEGIN *)
| Binding (name, TermType) :: tl ->
prerr_endline "aux: term";
Gramext.action
- (fun (v:term) -> aux ((name, (TermType, (TermValue v)))::vl) tl)
+ (fun (v:term) -> aux ((name, (TermType, TermValue v))::vl) tl)
| Binding (name, StringType) :: tl ->
prerr_endline "aux: string";
Gramext.action
(fun (v:string) ->
- aux ((name, (StringType, (StringValue v))) :: vl) tl)
+ aux ((name, (StringType, StringValue v)) :: vl) tl)
| Binding (name, NumType) :: tl ->
prerr_endline "aux: num";
Gramext.action
- (fun (v:string) -> aux ((name, (NumType, (NumValue v))) :: vl) tl)
+ (fun (v:string) -> aux ((name, (NumType, NumValue v)) :: vl) tl)
| Binding (name, OptType t) :: tl ->
prerr_endline "aux: opt";
Gramext.action
(fun (v:'a option) ->
- aux ((name, (OptType t, (OptValue v))) :: vl) tl)
+ aux ((name, (OptType t, OptValue v)) :: vl) tl)
| Binding (name, ListType t) :: tl ->
prerr_endline "aux: list";
Gramext.action
(fun (v:'a list) ->
- aux ((name, (ListType t, (ListValue v))) :: vl) tl)
+ aux ((name, (ListType t, ListValue v)) :: vl) tl)
| Env _ :: tl ->
prerr_endline "aux: env";
Gramext.action (fun (v:CicNotationEnv.t) -> aux (v @ vl) tl)
- (* LUCA: DEFCON 2 END *)
+ (* LUCA: DEFCON 5 END *)
in
aux [] (List.rev bindings)
(* return 2 lists of rows, first one containing homogeneous rows according
* to "compatible" below *)
let horizontal_split t =
- let ap =
+ let ap, first_row, t' =
match t with
| [] -> assert false
| ([], _) :: _ ->
assert false (* are_empty should have been invoked in advance *)
- | (hd :: _ , _) :: _ -> hd
+ | ((hd :: _ , _) as row) :: tl -> hd, row, tl
in
let rec aux prev_t = function
| [] -> List.rev prev_t, []
aux (row :: prev_t) tl
| t -> List.rev prev_t, t
in
- aux [] t
+ aux [first_row] t'
(* return 2 lists, first one representing first column, second one
* representing rows stripped of the first element *)
match terms with
| hd :: tl ->
let envl' =
- List.map2 (fun var (env, pid) -> (var, hd) :: env, pid) vars envl
+ List.map2
+ (fun (name, ty) (env, pid) ->
+ (name, (ty, CicNotationEnv.value_of_term hd)) :: env, pid)
+ vars envl
in
k tl envl'
| _ -> assert false)
let vars =
List.map
(function
- | Ast.Variable v -> v
+ | Ast.Variable v -> CicNotationEnv.declaration_of_var v
| _ -> assert false)
first_column
in
let rec subst = function
| Ast.AttributedTerm (_, t) -> subst t
| Ast.Variable var ->
- (try List.assoc var env with Not_found -> assert false)
- | (Ast.Literal _
- | Ast.Magic _) as t -> t
+ let name, expected_ty = CicNotationEnv.declaration_of_var var in
+ let ty, value =
+ try
+ List.assoc name env
+ with Not_found -> assert false
+ in
+ assert (CicNotationEnv.well_typed ty value); (* INVARIANT *)
+ (* following assertion should be a conditional that makes this
+ * instantiation fail *)
+ assert (CicNotationEnv.well_typed expected_ty value);
+ CicNotationEnv.term_of_value value
+ | Ast.Magic _ -> assert false (* TO BE IMPLEMENTED *)
+ | Ast.Literal _ as t -> t
| Ast.Layout l -> Ast.Layout (subst_layout l)
| t -> CicNotationUtil.visit_ast subst t
and subst_layout l = CicNotationUtil.visit_layout subst l in
set_compiled32 compiled32
let load_patterns21 t =
+ let rec pp_value = function
+ | CicNotationEnv.NumValue _ as v -> v
+ | CicNotationEnv.StringValue _ as v -> v
+ | CicNotationEnv.TermValue t -> CicNotationEnv.TermValue (pp_ast1 t)
+ | CicNotationEnv.OptValue None as v -> v
+ | CicNotationEnv.OptValue (Some v) ->
+ CicNotationEnv.OptValue (Some (pp_value v))
+ | CicNotationEnv.ListValue vl ->
+ CicNotationEnv.ListValue (List.map pp_value vl)
+ in
let ast_env_of_env env =
- List.map (fun (var, term) -> (var, pp_ast1 term)) env
+ List.map (fun (var, (ty, value)) -> (var, (ty, pp_value value))) env
in
let fail_k term = pp_ast0 term pp_ast1 in
let success_k (env, pid) = instantiate21 (ast_env_of_env env) pid in
match t1, t2 with
| Variable _, Variable _ -> true
| Variable _, _
- | _, Variable _ -> false
- | Layout _, _
- | _, Layout _
+ | _, Variable _
| Magic _, _
- | _, Magic _ -> assert false
+ | _, Magic _ -> false
+ | Layout _, _
+ | _, Layout _ -> assert false
| _ -> true
projects / helm.git / commitdiff